fix(parser): make the assembly arena's model true, and its assert able to see when it isn't (U6-0)#5611
Merged
Merged
Conversation
…e to see when it isn't (U6-0)
The arena carried TWO provenance stores and role membership read the wrong one.
`arena.nodes[id].prov` is keyed by IDENTITY and preserved across `mem::take` by
`reinstate()`. `AssemblyEnv::prov` was keyed by POSITION and rebuilt by `observe`
with `truncate` + re-push. `refresh` — which builds ALL role membership — read the
POSITIONAL one. So the identity machinery C1/C2 built was faithfully preserving a
store that role membership never consulted, and the two silently disagreed after any
move (`Instead` re-stamped `prov[0]` with the override clause's id while the arena
still held clause 0's). Delete the positional store; read provenance through the
arena. That removes the disagreement CLASS, not just its instances, and makes
`reinstate` load-bearing for the first time.
`assert_mirrors` could not have caught it. It took `defs_len` — a scalar — so it
could only ever compare the arena to ITSELF, and all four of its asserts are
maintained by the same two writes that establish them (`sync_len` reconciles
`order.len()` TO `defs_len`, then the assert compares them). It was a tautology: it
proved the assert was wired, never that it could discriminate a wrong model. Two real
modelling defects shipped underneath it.
It now takes `&[AbilityDefinition]` and adds two asserts that compare the arena to
something outside itself, using a stable identity witness (the address of a def's
boxed `Effect` — invariant under `Vec` moves and in-place effect rewrites, fresh for
a genuinely new def):
* `order[i]` must still name the def ACTUALLY at `defs[i]`.
* an `Absorbed { into }` node must really BE inside the tree of the parent it names.
The second one goes RED on the unfixed tree — 3 existing tests (Analyze the Pollen,
Aang's Journey) — which is what a non-vacuous assert looks like.
Two model defects, both at `FoldSearchIntoElse`:
* `defs.remove(bound_index)` is a MID-VECTOR removal, but every arena shrink
primitive is tail-only (`sync_len` pops `order`; `observe`'s own doc comment
states the precondition the code then violates). Add `Arena::remove_at`.
Measured: this fold fires twice on the ~35k-face pool and both are currently
TAIL removals, so the divergence is LATENT, not live — fixed structurally anyway,
because correctness must not rest on a coincidence about today's card pool.
* `settle` INFERRED the absorbing parent as `order.last()`, but this handler runs an
intrinsic continuation that pushes a node AFTER the real parent — so the arena
recorded the continuation's node as the parent. The nesting site now names the
parent explicitly (`Arena::absorb`). This one was live.
Evidence: full-pool export (~35,396 faces) byte-identical to base a61e7fd —
sha256 5eded903cd5fd5d534b3d581d57d089d7c14f30d5bc35b5c0a17335d4953be28, 98,187,284 B.
`[profile.tool] inherits = "dev"`, so both new asserts were LIVE across that sweep and
held. 16,178 lib tests pass; clippy -D warnings clean.
Contributor
|
Warning You have reached your daily quota limit. Please wait up to 24 hours and I will start processing your requests again! |
matthewevans
enabled auto-merge
July 11, 2026 20:59
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
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.
The arena carried TWO provenance stores and role membership read the wrong one.
arena.nodes[id].provis keyed by IDENTITY and preserved acrossmem::takebyreinstate().AssemblyEnv::provwas keyed by POSITION and rebuilt byobservewith
truncate+ re-push.refresh— which builds ALL role membership — read thePOSITIONAL one. So the identity machinery C1/C2 built was faithfully preserving a
store that role membership never consulted, and the two silently disagreed after any
move (
Insteadre-stampedprov[0]with the override clause's id while the arenastill held clause 0's). Delete the positional store; read provenance through the
arena. That removes the disagreement CLASS, not just its instances, and makes
reinstateload-bearing for the first time.assert_mirrorscould not have caught it. It tookdefs_len— a scalar — so itcould only ever compare the arena to ITSELF, and all four of its asserts are
maintained by the same two writes that establish them (
sync_lenreconcilesorder.len()TOdefs_len, then the assert compares them). It was a tautology: itproved the assert was wired, never that it could discriminate a wrong model. Two real
modelling defects shipped underneath it.
It now takes
&[AbilityDefinition]and adds two asserts that compare the arena tosomething outside itself, using a stable identity witness (the address of a def's
boxed
Effect— invariant underVecmoves and in-place effect rewrites, fresh fora genuinely new def):
order[i]must still name the def ACTUALLY atdefs[i].Absorbed { into }node must really BE inside the tree of the parent it names.The second one goes RED on the unfixed tree — 3 existing tests (Analyze the Pollen,
Aang's Journey) — which is what a non-vacuous assert looks like.
Two model defects, both at
FoldSearchIntoElse:defs.remove(bound_index)is a MID-VECTOR removal, but every arena shrinkprimitive is tail-only (
sync_lenpopsorder;observe's own doc commentstates the precondition the code then violates). Add
Arena::remove_at.Measured: this fold fires twice on the ~35k-face pool and both are currently
TAIL removals, so the divergence is LATENT, not live — fixed structurally anyway,
because correctness must not rest on a coincidence about today's card pool.
settleINFERRED the absorbing parent asorder.last(), but this handler runs anintrinsic continuation that pushes a node AFTER the real parent — so the arena
recorded the continuation's node as the parent. The nesting site now names the
parent explicitly (
Arena::absorb). This one was live.Evidence: full-pool export (~35,396 faces) byte-identical to base a61e7fd —
sha256 5eded903cd5fd5d534b3d581d57d089d7c14f30d5bc35b5c0a17335d4953be28, 98,187,284 B.
[profile.tool] inherits = "dev", so both new asserts were LIVE across that sweep andheld. 16,178 lib tests pass; clippy -D warnings clean.