ship/u6 0cd dig binding#5620
Merged
Merged
Conversation
matthewevans
commented
Jul 11, 2026
matthewevans
commented
Member
- fix(parser): watch the arena's identity assert go red, and delete the parent guess (U6-0c)
- fix(parser): close the terminal-clause assert blind spot (U6-0d)
- fix(parser): make the DigOrMill binding actually cause its output (U6-C3 corrected)
… parent guess (U6-0c) Addresses rev-u60's four follow-ups on 92790d3ca0. (1) The identity assert (`order[i]` names the def actually at `defs[i]`) guards the mid-vector-removal defect — and that defect is LATENT on today's pool: both `FoldSearchIntoElse` removals land on the tail, where a tail pop mirrors them correctly by accident. So nothing had ever watched this assert go red, which is the same gap class U6-0 exists to close: a guard nobody has seen fail is a guard nobody should trust. Two synthetic `Arena` tests now drive it. The red one removes `defs[1]` and mirrors it with `sync_len`'s tail pop — note that every COUNT stays balanced (3 defs / 3 nodes -> 2 / 2), which is exactly why the old count-only assert accepted it; only IDENTITY diverges. The green twin models the same removal with `remove_at` and the same assert accepts it. The pair is the point: `should_panic` alone would prove the assert CAN fail, not that it DISCRIMINATES. (2) `settle`'s `order.last()` parent inference is gone, not special-cased. Every absorbing handler now names its parent (`DigAlt`, `Instead`, `FoldSearchIntoElse`; `EntersTappedAttacking` re-lives its def via `reinstate` instead), so whatever is left detached was removed with no parent to name and is honestly `Dropped`. Emission order is not a parenthood oracle. `pushed_since_detach` existed only to feed the guess and is deleted with it. (3) `def_tree_contains` walks `sub_ability`/`else_ability` and NOT `mode_abilities`. That is deliberate — assembly never writes that slot (verified: the parser only reads it) — and the comment now says so, because it previously implied only two slots exist. If a future handler nests there, the parenthood assert goes red: the safe direction. (4) `live_root_index` returned `None` on loop exhaustion, which would have made the parenthood assert pass VACUOUSLY for that node — a self-inflicted false green. An `Absorbed` cycle looks unconstructible, so it is now `unreachable!` rather than quiet. Evidence: full-pool export byte-identical to base a61e7fd — sha256 5eded903cd5fd5d534b3d581d57d089d7c14f30d5bc35b5c0a17335d4953be28, 98,187,284 B, exit 0. Both asserts and the new cycle bail were LIVE across ~35k faces and none fired, so the explicit-absorb migration and the `Dropped` semantics hold on the real corpus. 16,180 lib tests pass; clippy -D warnings clean.
Addresses rev-u60's items 5 and 6 on 4b13adab9c. (5) The loop-top assert validates a clause's mutations on the NEXT iteration — so a card's FINAL clause has no iteration after it, and drift it introduced was asserted by nothing at all. Brainstealer Dragon's trailing mana rider is the witness: it corrupted the arena and only an output diff caught it. This also makes my own full-pool claim from U6-0b precise. I said the sweep "confirms the five rider paths leave the arena in sync across ~35k faces". That was over-broad: it held for every rider with a clause after it, and asserted NOTHING about a rider that is the last clause on the card. The Phase-1/Phase-2 boundary assert added here — the last moment the mirror still means anything, since Phase 2 never touches `env` — makes the claim true as stated. The settle-time assert goes away with it: loop-top + boundary already cover every clause's mutations, and asserting in `settle` only duplicated loop-top on every non-rider path. Same-or-better coverage at half the calls. `settle` now only classifies. A third `Arena` test pins it red on the broken shape — a terminal clause that mutates `defs` and never tells the arena. That is also precisely the shape `sync_len` SELF-HEALS if allowed to run first (it pushes a fresh node carrying the wrong provenance and hands it to role membership), which is why the drift must be caught rather than reconciled. (6) The "strictly stronger" claim on the F6 count assert was imprecise, and is now stated correctly: standalone the count is INCOMPARABLE to the membership scan it replaced — it catches a duplicate id in `order` that the scan waved through, and is blind to a duplicate exactly compensated by an orphaned Live node. That blind spot is covered by the identity assert, which pins `order[i]` to `defs[i]` by witness. The SET of asserts is what holds, not that one line. Evidence: full-pool export byte-identical to base a61e7fd — sha256 5eded903cd5fd5d534b3d581d57d089d7c14f30d5bc35b5c0a17335d4953be28, 98,187,284 B, exit 0, boundary assert live across ~35k faces, none fired. 16,181 lib tests; clippy clean.
…-C3 corrected)
The C3 arena binding was OUTPUT-INERT on all but 2 cards, and the "427 binds"
non-vacuity figure that justified it measured the wrong thing.
`dig_pos` was resolved by role at the top of the `DigFromAmong` arm, but consumed ONLY
inside the intervening-sacrifice branch, which returns. Every other path — a `Mill`
anchor, or a `Dig` with no intervening sacrifice — fell through to a surviving raw
backward scan that re-derived the antecedent live. So forcing `dig_pos` wrong could not
change the export on those paths: the fallthrough silently recomputed the right answer.
A probe that perturbs a value downstream code recomputes measures NOTHING.
Two changes, in the order the derivation requires:
1. `AntecedentRole::DigOrMill` becomes a LIVE predicate (`def_is_dig_or_mill`) instead
of a cached registry. This is the precondition for deleting the scan, not a
cleanup: the cached registry is refreshed only by `observe` (i.e. only when
`defs.len()` changes), while the assembler performs LENGTH-PRESERVING in-place
effect rewrites (`*previous.effect = Effect::ExileTop { .. }`) that turn a `Dig`
into something else with no length change. Cached, the role would go on naming a def
that is no longer a `Dig`/`Mill`. Live, `LastWithRole(DigOrMill)` IS the scan —
`(0..len).rev().find(|i| is_dig_or_mill(&defs[i]))` — so the deletion is equivalent
by construction rather than by inspection.
Membership mirrors where the scan STOPPED (the effect variant alone). The caller's
later narrowing to `Dig` is the MUTATION's precondition, not the selector's; folding
it into the role would resume the walk past a `Mill` and bind an earlier def the old
code never reached.
2. The fallthrough consumes `dig_pos`. The raw scan is gone.
Non-vacuity, anchored to the EXPORT rather than to a code path being taken. Forcing
`dig_pos -> None` (probe observed applied: 446 `FORCED` markers, on both trees), over
the full 35,396-face pool:
| tree | cards whose export diverges |
|------------------|-----------------------------|
| OLD (pre-fix) | 2 (birthing ritual, preferred selection) |
| NEW (fixed) | 425 |
| newly causal | 423 (were output-inert) |
| coverage lost | 0 |
446 reachable call sites; 2 of them caused output. That is the gap between reachability
and causality, measured. The real load-bearing count was 2 — the same as `Between` —
and it is now 425.
Unforced, the fixed tree is byte-identical to base a61e7fd: sha256
5eded903cd5fd5d534b3d581d57d089d7c14f30d5bc35b5c0a17335d4953be28, 98,187,284 B, exit 0.
16,181 lib tests pass; clippy -D warnings clean; no probe residue.
Retracts the false claims in the C3 and C2b commit messages ("every positional scan in
that arm is gone" / "ONE positional scan now remains"). With this, that arm has none.
Contributor
|
Warning You have reached your daily quota limit. Please wait up to 24 hours and I will start processing your requests again! |
Parse changes introduced by this PR✓ No card-parse changes detected. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.