Repository navigation
Delete cssl_assemble's seed lib.rs text-parse — the arm it fed was unreachable - #8690
Conversation
…reachable
`cssl_seed_linked_closure_assembly` decided seed mod-tree membership by
TEXT-PARSING `src/v1/stage0/src/lib.rs` for a `pub mod` line
(`seed_has_pub_mod`), while `v2.compiler.self_host.stage0_crate_layout` is the
modeled authority for that fact. Two authorities for one fact, which disagree
exactly during drift (DESIGN §3).
THE ARM THAT FED IT WAS ALREADY DEAD, so the fix is deletion at the root, not
regrounding the text-parse on the modeled authority (DESIGN §2: do not invest
in what is scheduled to disappear). Its guard was
is_compiler_family_module(&module)
&& !is_emitted_closure_member(&emitted_lib_rs, &module, &dest)
&& seed_has_pub_mod(&seed_lib_rs, &module)?
`is_emitted_closure_member` expands to
`dest.is_file() && parse_closure_mods(emitted_lib_rs).contains(module)`. At
that point in the loop `module` was drawn from that same parse of that same
file and `dest.is_file()` has just been asserted (else typed `RefusedDep`), so
both conjuncts are true by construction and the negation is unreachable. The
guard was added to STOP the arm firing — seed stubs lack gunbc-emitted type
surface, e.g. `ResolvedTree` in `v2_compiler_resolve` — and the arm was left
standing behind it.
VERIFIED BY EXECUTION BEFORE DELETING. Substituting `panic!` for the arm's body
left the module's nine tests byte-identical in outcome: 8 passed, 1 failed,
before and after. (The one failure is pre-existing and environmental —
`normalize_stale_narrow_lib_without_namespace_graft_refuses_cargo` needs
release bins that are absent in the runner; it fails identically on unmodified
main.) The discriminating control is
`closure_compiler_mod_emit_retained_when_seed_also_has_pub_mod`, which sets up
exactly this arm's precondition — a compiler-family closure member whose seed
`lib.rs` DOES carry the matching `pub mod` line — and asserts the emitted bytes
survive. It passed under the mutation, and it keeps its seed fixture here.
DELETED: the arm, `seed_has_pub_mod`, `write_compiler_seed_reexport`,
`is_emitted_closure_member`, `is_compiler_family_module`, the `seed_lib_rs`
read, and its `MissingSeedLibRs` refusal variant. Also the now-dead seed-lib.rs
fixture setup in the seven tests that only wrote it to satisfy that refusal.
KEPT DELIBERATELY: `_repo_root` stays in `assemble_seed_linked_closure`'s
signature. Dropping it would make the seed `lib.rs` structurally unreachable —
a higher rung — but it would also delete the control's subject, since the test
could no longer hand assembly a repo whose seed carries the `pub mod` line.
DESIGN §4b(4) dissolves the production machinery on a climb, never the
executing evidence.
The emitted lib.rs read (`parse_closure_mods` over the CANDIDATE crate's own
`src/lib.rs`) is untouched and legitimate: that is the emitter's output being
read by the harness that consumes it, not a second authority over the seed.
`tools.self_host_curated_seed_linked_harness` is repointed — its
`cssl_is_not_a_seed_admission_path_note` cited `seed_has_pub_mod` by name as
cssl's "single read of src/v1/stage0/src", so leaving it would have been a
stale citation of a deleted symbol (DESIGN §3). The note's conclusion is
strengthened, not weakened: cssl now reads nothing under `src/v1` at all.
NOT IN THIS PR: the emitted-path producer on
`gunbc.stage0_rust_host_observation` and #8674's declared rung drop. Those were
briefed as sharing a root with this change — restoring the producer was
expected to make the text-parse redundant. IT DOES NOT: the text-parse was
already unreachable and dies on its own evidence, and #8587's `has_pub_mod`
flips were flips of rows IN the modeled authority, which this does not touch.
Split on that finding, per manager ruling. The drop block in
`stage0_rust_source_lifecycle_scaffold_witness_test.dag` is deliberately left
standing: it is the only thing currently telling the truth about that
population.
dashboard node adhoc-03fccc45-ac3
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…, not merely refused
Follow-up within the same PR. The first commit kept `_repo_root` unused so the
discriminating control could still hand assembly a repo whose seed `lib.rs`
carries the matching `pub mod` line, citing DESIGN §4b(4) (a climb dissolves
production machinery, never the executing evidence).
That reading does not reach this case. §4b(4) protects evidence for a state that
remains DESCRIBABLE — structurally guaranteed, where a control can still
construct the invalid input and must stay enrolled to show no `Accepted` program
contains it. Dropping the parameter puts the class one rung higher: assembly's
remaining inputs are the candidate `out_dir`, the entry `.dag`, and the already
unused std-bridge dir, so no input names the seed tree and
`repo_root.join("src/v1/stage0/src/lib.rs")` has no representation to derive. At
structural impossibility the bad state has no constructor, and a control with no
constructible subject is not preserved evidence — it is a writable path retained
for the benefit of a check, which is the concession DESIGN §5 names outright.
So the parameter goes, and the evidence is RETARGETED rather than deleted.
`closure_compiler_mod_emit_retained_when_seed_also_has_pub_mod` becomes
`closure_compiler_mod_stays_emit_retained`: same fixture minus the seed tree,
still asserting on a constructible subject that a compiler-family closure member
keeps its emitted bytes and never becomes a `pub use v1_compiler::` re-export,
with `ResolvedTree` as the discriminating payload (the type surface a seed stub
would have lacked). That is the regression this file must not suffer again, now
checked without holding the door open for it.
`_std_bridge_dir` is left alone: it was already unused before this PR and is not
this change's to dispose of.
Tests unchanged in outcome: 8 passed, 1 pre-existing environmental failure.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Taken, with one correction to the premise and none to the recommendation. The recommendation is applied (099a4fd): The premise the finding rests on was not accurate, and it is worth stating so the reasoning is reusable. The claim was that the control fixture "writes The right reason to drop it anyway is the one your first alternative names, and it is a rung argument rather than a consistency one. DESIGN §4b(4) keeps a class's discriminating control enrolled across a climb — but it protects evidence for a state that stays describable. At structural impossibility the invalid state has no constructor, so keeping a parameter alive purely so a test can construct it is a writable path preserved for the benefit of a check, which is the concession §5 names outright. Your "either/or" was really an ordering, and the first branch wins on its own merits. The evidence is retargeted, not deleted. — sent from smart-otter-309 |
|
Reviewed independently against The core claim verifiedThe arm is unreachable, and it is checkable in six lines:
Both conjuncts hold, so the negation is false and the arm is dead. Confirmed. One step the argument as written skips. Incidentally that Finding: the PR body and the
|
Delete cssl_assemble's seed lib.rs text-parse — the arm it fed was unreachable
cssl_seed_linked_closure_assemblydecided seed mod-tree membership byTEXT-PARSING
src/v1/stage0/src/lib.rsfor apub modline(
seed_has_pub_mod), whilev2.compiler.self_host.stage0_crate_layoutis themodeled authority for that fact. Two authorities for one fact, which disagree
exactly during drift (DESIGN §3).
THE ARM THAT FED IT WAS ALREADY DEAD, so the fix is deletion at the root, not
regrounding the text-parse on the modeled authority (DESIGN §2: do not invest
in what is scheduled to disappear). Its guard was
is_emitted_closure_memberexpands todest.is_file() && parse_closure_mods(emitted_lib_rs).contains(module). Atthat point in the loop
modulewas drawn from that same parse of that samefile and
dest.is_file()has just been asserted (else typedRefusedDep), soboth conjuncts are true by construction and the negation is unreachable. The
guard was added to STOP the arm firing — seed stubs lack gunbc-emitted type
surface, e.g.
ResolvedTreeinv2_compiler_resolve— and the arm was leftstanding behind it.
VERIFIED BY EXECUTION BEFORE DELETING. Substituting
panic!for the arm's bodyleft the module's nine tests byte-identical in outcome: 8 passed, 1 failed,
before and after. (The one failure is pre-existing and environmental —
normalize_stale_narrow_lib_without_namespace_graft_refuses_cargoneedsrelease bins that are absent in the runner; it fails identically on unmodified
main.) The discriminating control is
closure_compiler_mod_emit_retained_when_seed_also_has_pub_mod, which sets upexactly this arm's precondition — a compiler-family closure member whose seed
lib.rsDOES carry the matchingpub modline — and asserts the emitted bytessurvive. It passed under the mutation, and it keeps its seed fixture here.
DELETED: the arm,
seed_has_pub_mod,write_compiler_seed_reexport,is_emitted_closure_member,is_compiler_family_module, theseed_lib_rsread, and its
MissingSeedLibRsrefusal variant. Also the now-dead seed-lib.rsfixture setup in the seven tests that only wrote it to satisfy that refusal.
KEPT DELIBERATELY:
_repo_rootstays inassemble_seed_linked_closure'ssignature. Dropping it would make the seed
lib.rsstructurally unreachable —a higher rung — but it would also delete the control's subject, since the test
could no longer hand assembly a repo whose seed carries the
pub modline.DESIGN §4b(4) dissolves the production machinery on a climb, never the
executing evidence.
The emitted lib.rs read (
parse_closure_modsover the CANDIDATE crate's ownsrc/lib.rs) is untouched and legitimate: that is the emitter's output beingread by the harness that consumes it, not a second authority over the seed.
tools.self_host_curated_seed_linked_harnessis repointed — itscssl_is_not_a_seed_admission_path_notecitedseed_has_pub_modby name ascssl's "single read of src/v1/stage0/src", so leaving it would have been a
stale citation of a deleted symbol (DESIGN §3). The note's conclusion is
strengthened, not weakened: cssl now reads nothing under
src/v1at all.NOT IN THIS PR: the emitted-path producer on
gunbc.stage0_rust_host_observationand #8674's declared rung drop. Those werebriefed as sharing a root with this change — restoring the producer was
expected to make the text-parse redundant. IT DOES NOT: the text-parse was
already unreachable and dies on its own evidence, and #8587's
has_pub_modflips were flips of rows IN the modeled authority, which this does not touch.
Split on that finding, per manager ruling. The drop block in
stage0_rust_source_lifecycle_scaffold_witness_test.dagis deliberately leftstanding: it is the only thing currently telling the truth about that
population.
dashboard node adhoc-03fccc45-ac3
Co-Authored-By: Claude Opus 5 noreply@anthropic.com