Skip to content

Two failure-mode rows from the compile-door measurement, and the one-line repair one of them specifies - #11025

Merged
gunbai-bot[bot] merged 5 commits into
mainfrom
session/calm-crane-722-step2
Sep 11, 2026
Merged

gunbai-bot[bot] merged 5 commits into
mainfrom
session/calm-crane-722-step2

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 11, 2026

Copy link
Copy Markdown
Contributor

Step 2a of the compile-obligation activation brief. Both classes were found by running things during the required-lens registration work (#11004); they are filed here rather than there because a ledger append and a compiler change are separate merge surfaces.

mandatory_gate_refuses_the_corpus_it_is_mandatory_on

A gate registered as mandatory on a door refuses the very corpus that door exists to admit, so the door is unreachable and the obligation reads enforced while nothing passes through it.

Specimen, measured rather than argued — on v2.test.manual.infer_ground_add fixture_add_resolved_tree:

  • infer accepts
  • the root-grain required roster accepts the inferred tree
  • the subtree-grain roster (fact_density + unit_modeling + lifecycle_carrier, per node) refuses it

in both TranslateTo (stub target) and Eval. So no fixture in this corpus reaches Accepted through the v2 compile door. This is the wall behind the declared frontier in v2.test.lens_application.required_lens_coverage_join (#11004), and it is named as one class with it so that retiring the frontier and repairing this are the same act.

Rung found at 1 (typed, located, line stops). Ceiling 2 — a per-gate accepting-traversal control, generated per registration. Next trigger: the lens-semantics repair.

sole_constructor_wrapper_satisfies_a_typecheck_declared_for_its_payload

A single-field wrapper value passes a typecheck written for its payload and then dies at evaluation on a field the payload has and the wrapper does not. Acceptance coerces; evaluation does not. Rung 1; ceiling 4, because whether a sole-constructor carrier may stand where its payload type is declared is decidable from the declaration alone. Next trigger: the compiler treating carrier and payload identically at both ends — refuse the wrapper where the payload is declared, or coerce it at evaluation as acceptance already does.

Distinguished from modifier_accepted_on_a_shape_its_check_cannot_see and sealing_property_erases_structure: those are about the sole_constructor modifier at a declaration site; this is a value at a use site, on a well-formed declaration.

The site repair lands with the row

normalized_of stored the NormalizedTree that normalize returns into a field declared Node, so three witnesses in v2.test.long.accumulator_copy_compile_gate failed at eval with no field 'kind' on type 'NormalizedTree'. root: normalized.root turns all three green — verified red on the committed file before the change, green after. Row and fix land together deliberately: a fix alone hides the acceptance hole, a row alone leaves a red nobody executes.

Why nobody noticed (recorded in the row as a second, separate finding): that entry is a LegacyFrozenPathDeferral in gunbc.witness_deferral_freeze — admitted by path policy with no executing consumer — so all four of its witnesses execute nowhere in any required lane.

Evidence

  • claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag --functions gate_red_quadratic_rejects,gate_green_identity_accepts_clean,gate_refusal_ledger_counted_not_gating — three FAIL before, three PASS after.
  • gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/docs_projection_gate.dag --function regen — both rows render through the real projection.

recurring_failure_mode/roster.dag is generated and gitignored; it picks both rows up from the directory.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f

Brian Searls and others added 2 commits September 11, 2026 04:15
…line repair one of them specifies

Both classes were found by running things during the required-lens
registration work (#11004), and both are filed here rather than there
because a ledger append and a compiler change are separate merge surfaces.

mandatory_gate_refuses_the_corpus_it_is_mandatory_on — a gate registered
as mandatory on a door refuses the very corpus that door exists to admit,
so the door is unreachable and the obligation reads enforced while nothing
passes through it. Specimen, measured: on fixture_add_resolved_tree, infer
ACCEPTS, the root-grain required roster ACCEPTS the inferred tree, and the
subtree-grain roster (fact_density + unit_modeling + lifecycle_carrier)
REFUSES it — in both TranslateTo and Eval. So no fixture in this corpus
reaches Accepted through the v2 compile door. This is the wall behind the
declared frontier in v2.test.lens_application.required_lens_coverage_join,
named as one class so retiring the frontier and repairing this are the same
act. Rung 1, ceiling 2, trigger: the lens-semantics repair.

sole_constructor_wrapper_satisfies_a_typecheck_declared_for_its_payload —
a single-field wrapper value passes a typecheck written for its payload and
then dies at evaluation on a field the payload has and the wrapper does not.
Acceptance coerces, evaluation does not. Rung 1, ceiling 4 (the question is
decidable from the declaration), trigger: the compiler treating carrier and
payload identically at BOTH ends.

The site repair that row specifies lands with it: normalized_of stored the
NormalizedTree normalize returns into a field declared Node, so three
witnesses in v2.test.long.accumulator_copy_compile_gate failed at eval with
"no field 'kind' on type 'NormalizedTree'". `root: normalized.root` turns
all three green — verified red before, green after. The row and the fix land
together deliberately: a fix alone would hide the acceptance hole, a row
alone leaves a red nobody executes.

Why nobody noticed: that entry is a LegacyFrozenPathDeferral in
gunbc.witness_deferral_freeze — admitted by path policy with no executing
consumer — recorded in the row as a second, separate finding.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…465)

The SPECIMEN receipt named v2.test.lens_application.required_lens_coverage_join
as the home of the door-grain frontier. That module is declared in #11004,
which is not merged, so on this branch and on base the citation resolves to
nothing — the exact defect DESIGN §3's standing rule exists to prevent, and it
was load-bearing for the row's "wall behind that frontier" claim.

The row now states the CONSEQUENCE instead of pointing at a file: while a
mandatory gate refuses the corpus its door must admit, a door-grain positive
control is not authorable at all, so any coverage receipt attached to that
door necessarily lands with its positive control declared as a frontier. The
link is the class, not the file name, and the row says explicitly why it does
not cite the module. Nothing else changes; every remaining citation in both
rows resolves on main.

Verified: the module resolves and evaluates (gunbc run reaching `authored`'s
arity check, i.e. past parse and typecheck).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
@gunbai-bot

gunbai-bot Bot commented Sep 11, 2026

Copy link
Copy Markdown
Contributor Author

Fixed in 8ce19e6f1b5. review 63465's finding is correct and I verified it the same way: git grep -ln "required_lens_coverage" on this branch and on base returns only the row itself, because the module that declares that frontier is in #11004 and #11004 is not merged. A citation that resolves to nothing is exactly the defect DESIGN §3's standing rule exists to prevent, and it was load-bearing — it was the link for the row's "this is the wall behind that frontier" claim.

The repair is to state the consequence rather than point at a file, because the class is the link and the file name was never the thing that made the two one finding. The receipt now says: while a mandatory gate refuses the corpus its door must admit, a door-grain positive control — an Accepted compile whose receipt says every required obligation ran — is not authorable at all, so any coverage receipt attached to that door necessarily lands with its positive control declared as a frontier rather than executed. The row also says explicitly that it is not citing the module carrying that frontier, and why. The "same act" sentence is generalised to any such frontier, with the addition that a frontier retired any other way has been retired by something other than its trigger.

The alternative — landing this after #11004 so the symbol resolves — would have worked too, but it makes a ledger append wait on a compiler change for a link the row does not need.

Every remaining citation in both rows resolves on main: v2.compiler.compile validate_then_compile, v2.test.manual.infer_ground_add fixture_add_resolved_tree, infer, v2.compiler.normalize normalize, NormalizedTree, normalized_of, v2.test.long.accumulator_copy_compile_gate, gunbc.witness_deferral_freeze LegacyFrozenPathDeferral.

Verified the edited module still resolves and typechecks (a gunbc run reaching authored's arity check, i.e. past parse and resolution).

Thanks for checking the one-line repair against the declarations rather than taking the report — sole_constructor { root: Node } against ProbeNormalized { root: Node } is exactly the unwrap that was missing.

— sent from calm-crane-722

@gunbai-bot

gunbai-bot Bot commented Sep 11, 2026

Copy link
Copy Markdown
Contributor Author

CI on 8ce19e6f1b5 failed the floor, and it is not this diff. The cause is located precisely, so I have re-run the failed jobs rather than pushing a change.

What refused: required-floor: LOCAL-REPO-WET REFUSAL test.claim.self_host_logic_behavioral_witness.self_host_logic_behavioral_receipt_holds: WetTerminalVerdictNotExpected — expected passed, observed failed.

Why it observed failed — from the same log, upstream of the verdict:

could not execute process `…/_temp/rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/rustc …`
Caused by: No such file or directory (os error 2)
❌ gunbc.WitnessBin.Run failed: … /target/release/witness (exit=127)

The witness emits dag/std/logic.dag, compiles the emitted Rust, and runs the binary. rustc was absent when it tried to compile, so no binary existed and both arms exited 127.

The joined reading from the workflow's own toolchain_filesystem_probe confirms it was a mid-run race rather than a missing install:

  • phase=start (05:43:41): …/bin/rustc exists=no
  • witness attempts to compile at 06:15:57 → ENOENT
  • phase=end (06:26:28): …/bin/rustc exists=yes size=2319968 mtime=2026-09-11 06:24:39

The toolchain was (re)installed at 06:24:39, nine minutes after the witness needed it. That is exactly the condition that probe's dissolve-on names ("the fleet fixes the toolchain deleter"), on host=srv3 runner=srv3-15, with loadavg rising from 38 to 74 across the job.

Why it cannot be this PR: the diff is two RecurringFailureMode rows under dag/gunbc/ plus one line inside src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag. It does not touch dag/std/logic.dag, the emitter, the seed crate, or any toolchain wiring. The same witness reads expected=passed observed=passed on main at c047472bf4f, and the only two commits between this branch's base and that head touch none of those paths.

Worth noting for whoever owns the lane: the refusal reports a semantic verdict ("observed failed") for an infrastructure failure (compiler binary absent). Those are different facts and the lane's vocabulary currently collapses them, which is what made a runner race look like a red witness.

Re-run of the failed jobs is queued.

— sent from calm-crane-722

Brian Searls and others added 2 commits September 11, 2026 08:33
The "WHY IT SURVIVED" receipt described a class that already has a home —
witness_module_absent_from_the_executed_set — from inside a row whose subject is
a coercion hole at a use site. §4b says a newly discovered class files or updates
ONE row; I updated the wrong one. The inconsistency was internal to this PR: its
other row cites [[witness_module_absent_from_the_executed_set]] by name.

The receipt moves there, and carries two things that row did not have:

- A SECOND HARM. Every instance it holds is a correct check whose green is
  wrongly cited as coverage. But a module outside the executed set is equally
  free to BREAK and stay broken: three witnesses in this PR's own subject had
  been failing at eval with "no field 'kind' on type 'NormalizedTree'" for an
  unknown length of time — loud when run, invisible because nothing runs them.
  The repair was one field; the reason it survived was membership.
- A DIFFERENT ADMISSION MECHANISM, which changes detection. The existing
  instances are modules nobody scheduled — a gap, found by joining
  modules-on-disk to modules-scheduled. This one was scheduled OUT, deliberately,
  by path policy, and the roster recording it is honest about what it is. Same
  consequence, but a deferral roster is already a written list of modules whose
  reds nobody will see, and can be read directly rather than derived.

The coercion row keeps only the acceptance hole and links the sibling, with one
line on why they compose: one made the mistake writable, the other made it
invisible, and keeping both in one row buries a membership finding behind a
coercion class where nobody looking for it would read it.

Verified the edited row resolves and typechecks.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
@gunbai-bot

gunbai-bot Bot commented Sep 11, 2026

Copy link
Copy Markdown
Contributor Author

review 63679 is right, and the inconsistency was internal to this PR: its other row cites [[witness_module_absent_from_the_executed_set]] by name while this receipt described that same class from inside a row whose subject is a coercion hole at a use site. §4b says a newly discovered class files or updates one row; I updated the wrong one. Fixed in 6db10cd264c.

The receipt moves to witness_module_absent_from_the_executed_set, and I made it carry two things that row did not already have, so the append is worth its space:

  • A second harm. Every instance that row holds is a correct check whose green is wrongly cited as coverage — the danger being that nobody learns the class is unchecked. But a module outside the executed set is equally free to break and stay broken. This PR's own subject is the proof: three witnesses failing at eval with no field 'kind' on type 'NormalizedTree', loud when run, invisible because nothing runs them, for an unknown length of time. The repair was one field; the reason it survived was membership.
  • A different admission mechanism, which changes detection. The existing instances are modules nobody scheduled — a gap, found by joining modules-on-disk to modules-scheduled. This one was scheduled out, deliberately, by path policy, and the roster that records it is honest about what it is. Same consequence, but a deferral roster is already a written list of modules whose reds nobody will see, and can be read directly rather than derived.

The coercion row keeps only the acceptance hole and links the sibling, with one line on why they compose: one made the mistake writable, the other made it invisible.

Your consequence paragraph is the part I'd underline — the three witnesses this PR turns green sit on a path with no executing consumer, so nothing stops them going red again, and the class that owns "nobody would notice" is exactly the one that had not received the receipt. That is now filed where someone hunting that failure mode will find it.

Verified the edited row resolves and typechecks. Head is 6db10cd264c, on a base that contains d94bcf68 (the parse-cost root fix), so this run is the first observation of this content against a floor that can go green.

— sent from calm-crane-722

…ed to

Required repair from the landing ruling. The row said "no fixture in this corpus
reaches Accepted through the v2 compile door" on the evidence of ONE fixture in
TWO modes. That is an existential result promoted to a universal: what was
measured is that the compiler's own clean resolved add fixture is refused
upstream of emission on both paths, and the corpus was never enumerated.

THE IRONY IS THE POINT AND THE ROW NOW SAYS SO. This is the claim-wider-than-its
-evidence defect committed inside a row about evidence, in a ledger whose whole
job is to catch it. A row that overstates its own reach is worse than a missing
row, because it will be cited at the reach it claims.

WHAT THE TEXT NOW STATES, at the grain it was measured at: this fixture is
refused on both paths, and NO ACCEPTED POSITIVE CONTROL HAS BEEN PRODUCED for
the door. What it explicitly does NOT claim: that no fixture can reach Accepted.
What the universal would need is named rather than assumed -- a derived, closed
fixture population with the door executed over all of it -- and recorded as
missing measurement, which is the honest state.

The consequence sentence inherited the same over-reach and is scoped with it:
"not authorable at all" and "any coverage receipt NECESSARILY lands" become what
happened -- the obvious candidate does not produce a positive control, so the
coverage receipt attached to that door landed with its positive control declared
as a frontier rather than executed.

The ceiling and the next-rung trigger are unchanged: both were already stated
over the per-gate accepting-traversal control and the lens-semantics repair,
neither of which rested on the universal. The second row on this PR is untouched.

0 blocking errors. The run at the prior head came back success before this push.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
@gunbai-bot
gunbai-bot Bot merged commit 37e643d into main Sep 11, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/calm-crane-722-step2 branch September 11, 2026 20:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants