Repository navigation
regen's copy loop skipped a declared row naming nothing; a corrupt row was inert, now it refuses - #9096
Merged
Conversation
…w was inert, now it refuses `copy_hand_maintained_support` iterated HAND_MAINTAINED_STAGE0_FILES and HAND_MAINTAINED_STAGE0_DIRS with a bare `if exists` / `if is_dir` and no else, so a declared crate-layout row naming a path that is not on disk was silently skipped. That is an absorbing fallback in DESIGN §5's exact shape: the failure arm widened (copy what resolves, ignore what does not) instead of refusing, so the deficit's frequency was zero by construction. WHAT IT MADE INERT, with a live specimen. On integration/namespace-cut, dag/gunbc/stage0_crate_layout_generated.dag carries a stray `"rs",` row between "shared_typecheck_store.rs" and "recorded_fixture.rs" — 37 entries against main's 36 — introduced by merge commit ebda683 ("Integrate main (#8788)"), where a line split and its tail survived as its own list element. Nothing named `rs` is on disk, so the copy loop skipped it without a word, and because the emitted mirror faithfully reproduces the corrupted authority, regen's fixed point reports green over it (that branch's own 6d9f239: "regen fixed point green (exit 0)"). Regen compares mirror to authority and has no operand for whether the authority is right — but the authority CAN be joined to the tree, every declared basename either resolves or does not, and this is the one place that join already happened and its result was discarded. BOTH LOOPS, and the second is not a copy of the first. The file loop's absence is absence from disk, which is never legitimate. Note the contrast with `verify_hand_maintained`, which iterates the same list and also continues on absence: its absence is absence from the EMITTED population, the ordinary case for 35 of the 36 entries. Two functions, one list, two different absences, and only one of them is normal. EVIDENCE, per DESIGN §5 — green by execution plus a discriminating red. The new test plants every declared row on disk and accepts, then removes exactly one file and one directory, so control and refusal differ by a single row and the refusal must name it. Verified red without the wall by two independently constructed controls (the impl arms removed; and origin/main's body carrying only the new test), both failing with "a declared row naming no file must refuse". Verified against main's live population first: all 36 declared files and both declared dirs resolve on origin/main, so the wall is green on main by measurement rather than by assumption. Rung: mechanically preventable — `basename: String` and `List<String>` throughout, so `"rs"` is a well-formed inhabitant and no type error is available. Next-rung trigger: a Stage0Filename carrier minted only from a path that resolves, which would make the corrupt row unwritable rather than refused. v1 admission: the seed is semantics-frozen and maintenance-active, and this serves the v2 self-host program — a corrupt crate-layout authority silently accepted is a self-host correctness gap. Same class as the bare-`Err(_)` arms swift-lynx-327 is converting in gunbc#9087, ~14k lines away in this file.
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.
copy_hand_maintained_supportiterated HAND_MAINTAINED_STAGE0_FILES andHAND_MAINTAINED_STAGE0_DIRS with a bare
if exists/if is_dirand no else, so adeclared crate-layout row naming a path that is not on disk was silently skipped. That
is an absorbing fallback in DESIGN §5's exact shape: the failure arm widened (copy what
resolves, ignore what does not) instead of refusing, so the deficit's frequency was zero
by construction.
WHAT IT MADE INERT, with a live specimen. On integration/namespace-cut,
dag/gunbc/stage0_crate_layout_generated.dag carries a stray
"rs",row between"shared_typecheck_store.rs" and "recorded_fixture.rs" — 37 entries against main's 36 —
introduced by merge commit ebda683 ("Integrate main (#8788)"), where a line split and
its tail survived as its own list element. Nothing named
rsis on disk, so the copyloop skipped it without a word, and because the emitted mirror faithfully reproduces the
corrupted authority, regen's fixed point reports green over it (that branch's own
6d9f239: "regen fixed point green (exit 0)"). Regen compares mirror to authority and
has no operand for whether the authority is right — but the authority CAN be joined to
the tree, every declared basename either resolves or does not, and this is the one place
that join already happened and its result was discarded.
BOTH LOOPS, and the second is not a copy of the first. The file loop's absence is absence
from disk, which is never legitimate. Note the contrast with
verify_hand_maintained,which iterates the same list and also continues on absence: its absence is absence from
the EMITTED population, the ordinary case for 35 of the 36 entries. Two functions, one
list, two different absences, and only one of them is normal.
EVIDENCE, per DESIGN §5 — green by execution plus a discriminating red. The new test
plants every declared row on disk and accepts, then removes exactly one file and one
directory, so control and refusal differ by a single row and the refusal must name it.
Verified red without the wall by two independently constructed controls (the impl arms
removed; and origin/main's body carrying only the new test), both failing with "a
declared row naming no file must refuse". Verified against main's live population first:
all 36 declared files and both declared dirs resolve on origin/main, so the wall is green
on main by measurement rather than by assumption.
Rung: mechanically preventable —
basename: StringandList<String>throughout, so"rs"is a well-formed inhabitant and no type error is available. Next-rung trigger: aStage0Filename carrier minted only from a path that resolves, which would make the corrupt
row unwritable rather than refused.
v1 admission: the seed is semantics-frozen and maintenance-active, and this serves the v2
self-host program — a corrupt crate-layout authority silently accepted is a self-host
correctness gap. Same class as the bare-
Err(_)arms swift-lynx-327 is converting ingunbc#9087, ~14k lines away in this file.