Repository navigation
Self-host compile-obligation activation, complexity first: a new authority src/v2/compiler/self_host/compile_obligation_activation.dag (shared compile door + one explicit node per required compile lens, complexity and determinism bundles carrying their supporting obligations), identity-bearing requi - #11160
Closed
briansrls wants to merge 27 commits into
Closed
briansrls wants to merge 27 commits into
briansrls wants to merge 27 commits into
Conversation
…n/observation join at the compile door
Step 1 of the compile-obligation activation brief: make the required-lens
roster name its lenses, so "the required lenses ran" stops being a claim
about a list length.
- One registration roster (required_compile_lens_roster), partitioned by
grain through required_lenses_at_grain, replaces the two lists
always_required_lenses / always_required_root_lenses. Each row carries
the DeclarationRef of the gate authority that decides it plus its grain.
- LensGateWitness carries the lens identity and the grain it was produced
at, so every observation names its producer.
- join_required_lens_coverage closes the join bidirectionally and refuses
by name: RequiredLensRosterEmpty, RegistrationDuplicated,
RegistrationUnobserved, ObservationUnregistered, ObservedAtWrongGrain,
RootLensObservedMoreThanOnce. Root grain states exactly-one; subtree
grain is at-least-one, because subtree registrations are observed once
per node by construction.
- validate_then_compile runs each lens at its registered grain (caller
lenses included, which previously ran at root whatever they declared),
derives the coverage from the witnesses it actually collected, and
refuses the compile when it is not closed. Validated carries the
receipt with the roster digest.
Divergence from the brief, stated: one CompileLens carrier gains the two
fields rather than a second RequiredCompileLens type. Requiredness is
membership in the roster, not a property of the carrier, and a caller
lens must stamp its witnesses the same way for the join to be closed.
Evidence, by execution (claim_batch, local release build):
- v2.test.lens_application.required_lens_coverage_join: 7 witnesses green
- one positive control over the real roster,
- one control that runs all eight registered gates through the door's
own two runners and joins the witnesses they actually stamped,
- five discriminating REDs, one per refusal arm, each asserting the
cause AND the lens identity.
- the eight touched pre-existing lens witnesses: all green.
Not established, and not claimed: an Accepted validate_then_compile
carrying the receipt. No fixture in this corpus reaches Accepted through
that door today (measured on fixture_add_resolved_tree in TranslateTo and
Eval; the refusal is upstream of the lens rosters). That frontier is
recorded in the test module's header.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…iminates (test-only) door_root_roster_runs_and_passes_clean_tree called validate_then_compile and accepted EITHER an Accepted compile OR any Rejected whose diagnostics lacked the poly2 suspect. Measured: the door REFUSES this fixture, so the check was green on a refusal and would have stayed green if the root roster had stopped running altogether — a permanently-green check cited as coverage (DESIGN §4b). The refusal is now located, and it is neither infer nor the root roster: infer Accepts fixture_add_resolved_tree, the root-required roster Accepts the inferred tree, and the SUBTREE-grain roster refuses it. So the control becomes door_root_roster_accepts_clean_inferred_tree: infer must Accept and every root-registered gate must Accept the real inferred tree, with no tolerance for an unrelated refusal. The module header's claim that the fixture "passes through the root-required roster ... proving the roster RUNS on every door call" is corrected to the root-roster claim it actually supports, and the now-unused stub target and its imports are removed. The door-grain positive control (an Accepted validate_then_compile carrying its coverage receipt) stays a declared frontier in v2.test.lens_application.required_lens_coverage_join. Evidence: door_root_roster_accepts_clean_inferred_tree PASS. The module's other three witnesses (gate_red_quadratic_rejects, gate_green_identity_accepts_clean, gate_refusal_ledger_counted_not_gating) fail on the interpreted path with "no field 'kind' on type 'NormalizedTree'" BEFORE this change as well — verified by running them on the committed file — so they are untouched by it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
gunbc.witness_deferral_freeze names (entry, function) pairs at identity grain and REFUSES a row naming a witness the tree no longer carries as a stale freeze row. Renaming door_root_roster_runs_and_passes_clean_tree in the previous commit made its row stale, so the roster's own wall would fire on this branch. One field, the new name. This also explains why the re-scoped control's three sibling witnesses in the same entry were red without anyone noticing: the whole entry is a LegacyFrozenPathDeferral, i.e. admitted by path policy with no executing consumer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…prohibition forward (review 63457)
Two findings, both real, both verified against the current tree.
1. STALE CITATIONS. required_lens_grain_note was re-asserted verbatim while
both symbols it is about — always_required_lenses and
always_required_root_lenses — were deleted in the same diff, and five more
prose sites named them too. A replacement migration that cuts over at the
root owes the citation cut-over in the same motion (DESIGN §3 standing
rule). The note is rewritten to carry the same cost argument in terms of
what survives — a CompileLensSubtree registration runs per subtree node, a
CompileLensRoot registration runs once at the root, grain is a FIELD and
required_lenses_at_grain derives each execution's list — and it now also
records that a caller-supplied lens runs at its own declared grain. The
other five: v2.lens.determinism, v2.lens.mandatory_tag,
v2.lens.mandatory_tag.corpus_scan, v2.lens.machine_shape,
v2.lens.undecidable_verdict_collapse, v1.compiler.emit_rust,
gunbc.declaration_index_seed_growth, and
test.claim.computation_demand_duplication_witness.
2. DROPPED PROHIBITION. The lens_module_gate de-enrollment rationale was
deleted with the old root roster and nothing carried it forward — a standing
prohibition tied to a named red class (lying_substrate_inputs_only_stamp_census,
31 stamps). Worse, the replacement text invited the regression it warned
about ("Adding a lens is one row") with no eligibility statement. It is
carried forward in force beside the roster, plus the eligibility rule it
implies: a row must be a PURE FOLD OVER THE TREE BEING COMPILED at its
declared grain; a nullary gate, a corpus scan, or any gate reading the live
tree rather than its InferredTree argument is ineligible at either grain.
Not done, and stated rather than left silent: three test MODULES still carry
the deleted symbol in their own names
(lens_fact_density.hollow_alias_blocked_via_always_required_lenses and the two
lens_unit_modeling siblings). Renaming them is a file-and-module rename whose
citations include gunbc.live_deploy.srv1_residue_rehearsal — a RECORDED PATH
WIRE, i.e. an observation receipt — and dag/gunbc/witness/witness_row_cost_basis.tsv.
Editing a recorded observation to match a rename is not a citation repair, so
that cut is its own change.
Evidence: the coverage-join witnesses re-run green after the edits
(required_lens_coverage_closes_over_executed_gates_holds,
required_lens_coverage_refuses_unobserved_registration_holds).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
git add -A in the citation-cutover commit swept two untracked 4a files that had followed a branch switch into the worktree: dag/std/realization_cost_fidelity.dag and dag/test/claim/realization_cost_fidelity_witness_test.dag. Neither belongs here — 4a's design was still undecided when they were committed, and this PR is registration plus the citation cutover plus the de-enrollment prohibition and nothing else. They move to their own branch and land after their own closure receipt. The other three files in that commit stay: declaration_index_seed_growth, computation_demand_duplication_witness_test and v1.compiler.emit_rust are one-to-three-line citation cutovers of the deleted roster symbols, which is exactly what review 63457 asked for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Both verified; both were real. - v2.test.long.mandatory_tag_gate_witness: the file is already in this diff (its import moved to required_lenses_at_grain / CompileLensRoot), so its prose and its code disagreed inside one file. Now "the CompileLensRoot partition of required_compile_lens_roster". - docs/plans/determinism-boundary-relative.md: the citation sits inside a block the file's own header declares "preserved verbatim" from a DESIGN.md row deleted on operator ruling. Rewriting a symbol inside a quotation falsifies the quotation, so the quoted sentence is left as authored and the current symbol is named beside it in brackets — the same reason the three test-module renames are not folded into this PR. Remaining hits are src/v1/stage0/**, the seed's own mirror of this module, addressed on the PR rather than edited here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…, not documentation (review 63517) I argued the opposite an hour ago and I was wrong, for a reason worth writing down: I reasoned from a general principle — do not edit the independent oracle in the same push as its subject — without checking whether anything ASSERTS EQUALITY on the string. Something does. dag/gunbc/instruments/self_host_00_compile_shims/witness_main.rs compares emitted::required_lens_grain_note() against seed::required_lens_grain_note() and makes equality the Gate-A behavioral receipt. So this literal is not a mirror of the authority for a reader's benefit; it is the value the self-host equivalence claim is made of. Changing the .dag without it does not preserve the oracle's independence — it falsifies the receipt my own change is supposed to keep true. The reviewer measured the divergence (1288 vs 934) that I had asserted away. The seed literal is DERIVED from the .dag line rather than retyped, and byte-equality verified programmatically: equal? True, 1288 == 1288. cargo check on the seed lib is clean. The oracle's header now says what it actually is — the compared value, which cuts over with the authority — so the next reader does not repeat my reasoning about independence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…L, CITED-DECLARATION-ABSENT) required-ci: declarations FAIL CITED-DECLARATION-ABSENT dag/gunbc/recurring_failure_mode/stale_present_tense_coverage_claim_in_the_authority_consulted_first.dag:47:5 cites v2.compiler.compile always_required_root_lenses, which that module does not declare Mine, and the same class I swept eight sites of in this PR: a replacement migration owes the citation cut-over. The reason this one was missed is worth recording — the row did not exist when I swept. It landed on main afterwards with #10942 (the compile-obligation census), citing a symbol this PR deletes at its root, so the break appeared in the merge rather than in either change. Neither lane could have seen it alone: the census cited a declaration that was live on main, and my sweep covered every citation that existed at the time. - The evidence decl_ref now names required_compile_lens_roster, which is what replaced it and what the row's argument is actually about. - The row's prose cited the same symbol in its specimen sentence and cuts over with it. - gunbc.v2_compile_obligation_census names the deleted symbol in two annotations; both now name the surviving roster, and the one about staleness says explicitly that the argument does not turn on there having been two lists. Deliberately untouched: the census's entry/function/module_path rows for hollow_alias_blocked_via_always_required_lenses and its two siblings. Those are module and function IDENTITIES that still resolve, not symbol citations — their rename is the separate cut whose citations include a recorded path wire. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
… cuts over (review 63812) 1. MY OWN HEADER CLAIMED SOMETHING FALSE. The module said "one discriminating RED per refusal arm" and the PR body said "five discriminating REDs, one per refusal arm", while RequiredLensJoinCause has SIX arms. RegistrationDuplicated — the arm whose whole job is catching a roster that acquired a second row for one identity — had no control asserting it ever fires. The "unreachable at the door" defence does not hold, and §4b decides it at the fixture rather than at the door: a state unrepresentable in the accepted corpus may still be representable as source handed to the join by a fixture, and where the refusal is authorable there, declining it is specification without execution. The sibling REDs already hand the join synthetic rosters, so it was one call — append a repeated row — which is what makes the omission indefensible rather than a judgement call. Eight controls now, and the header claim is true. 2. THE THIRD MERGE-ONLY CITATION TODAY. v2_compile_obligation_census_witness_test names both deleted symbols in its "what is still not checked" annotation. That file arrived with #10942 AFTER my citation sweep, so the break exists only in the merge, exactly like the two the declarations phase caught. It now names required_compile_lens_roster, and records that the gap it describes never turned on how many lists there were. Left alone deliberately, again: the entry/function/module_path rows for hollow_alias_blocked_via_always_required_lenses. Those are identities that still resolve, not symbol citations. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
… 63827) The rename in this PR (always_required_root_lenses -> required_compile_lens_roster) updated seven sibling citations and missed one: the mandatory-tag scaffold comment in the seed's cli_run.rs still named the deleted symbol as where the modeled lens is enrolled. At this head it was the only surviving live citation -- the remaining grep hits are witness function names and module paths, which are not citations of the symbol. It now names the registration as it actually stands: required_compile_lens_roster at CompileLensRoot grain, the mandatory_tag_lens row. That is the point of the rename -- the grain is a field on the row rather than a fact about which of two lists a lens was written into -- so the citation has to say the row, not the list. This is the class the PR itself edits (DESIGN 3: a stale name is decidable and enforceable). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…ed import goes Review 63842. The distinction the review draws is the right one and I am keeping it: the JOIN is consumed by execution in this change -- validate_then_compile refuses a compile whose coverage is not closed -- so the gate was never the dangling part. The receipt CARRIED on Validated is a separate declaration with a separate consumer, and nothing outside this module reads it today. The prose that was there named a consumer (the obligation census) and stated no trigger, which is a half-classification: DESIGN section 3c admits a frontier only with the trigger beside it, precisely so that "a later change will read this" cannot be said indefinitely. The field now carries consumer, route and trigger, with the trigger stated as a CAPABILITY -- the promotion path routing its candidate through this door and refusing on a named uncovered lens, sufficient that a candidate cannot be promoted without its coverage having been observed on the same compile that produced it. It also states the kill condition, because a frontier that cannot expire is not a classification: if that capability does not land, the field is redundant work and the honest move is to DELETE it, since the refusal is already the gate. WholeDeclaration was imported and never used; removed. 8 join controls green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
MEASURED FIRST, because the cut I was about to make was aimed at the wrong thing. claim_batch over this module's four witnesses in one remote dispatch: the three source-path rows cost 534-680ms of CPU against a 500ms per-claim ceiling, while door_root_roster_accepts_clean_inferred_tree -- same gate area, hand-built node fixture, no front end -- costs 50ms. Three DIFFERENT four-line snippets spread only ~150ms over a ~530ms base, so the base is the front end itself, not the snippets. Shrinking the planted ledger could not have moved a 680ms witness under 500ms when its two ledger-free siblings pay 534 and 618 for the same prefix. The consequence that matters more than the one failing row: ALL THREE source-path witnesses here are at or over the ceiling on an unloaded runner. gate_refusal_ledger_counted_not_gating is not defective beside three healthy ones; it is the one 80ms above its nearest sibling. Host thrash is why it trips today, the budget is why it would trip anyway. THE CUT KEEPS THE SOURCE PATH. The three claims are now nullary producers enrolled WARM in v2.workflow.floor_pure_producer_share, so the floor forces each once during strict preparation, outside every per-claim budget, exactly as v2.test.claim.parse.d1_declaration_grammar_parse does for the identical defect (seven of its eight rows were interrupted at this same ceiling). Nothing about what executes changes: same source, same tokenize, same parse, same normalize, same tree, paid once. The alternative -- moving the ledger assertion onto a hand-built fixture -- would have bought the budget by trading what the witness proves, ledger behaviour on a tree the real front end produced. DESIGN 4b(1) prices that as a rung drop, not a cost fix. SEAM CHOICE, and it differs from the d1 precedent deliberately: that module shares at the PARSE tree because some of its claims name normalize as their subject, and sharing normalize would stop them executing the stage they claim. No witness here names any front-end stage -- all three branch on the normalized root and assert about accumulator_copy_compile_gate -- so the whole front end is upstream of every subject in this file and the honest seam is its output. VERIFICATION BOUND, stated because it is real: claim_batch under my invocation refuses this module with "no field 'kind' on type 'NormalizedTree'" inside normalize while the floor accepts it (3625 passed, 0 failed at this head), so I cannot execute these three witnesses locally at all. What I verified is that both modules parse in a whole-corpus index and the roster fold evaluates with the three rows present. Whether the NormalizedProbe value reifies portably is decided by the floor, and a warm row that refuses to store STOPS THE LINE rather than degrading -- the precedent shares Outcome<Node>, the same shape class. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…rved value did not survive MY PREVIOUS COMMIT BROKE THREE PASSING WITNESSES, and this withdraws it. The floor at 540c92c reports all three accumulator-gate claims failing with "no field 'kind' on type 'NormalizedTree'", cause=claim_failed. They pass when each claim derives its own tree. That is a regression I introduced, and a budget refusal traded for three failing witnesses is strictly worse than the budget refusal. WHAT THE EXPERIMENT ESTABLISHED, because it is not nothing. The netting worked exactly as ruled: disposition=Stored for all three producers during strict preparation, 868ms, 496ms and 571ms of front end paid outside every per-claim budget. That is the diagnosis confirmed by execution rather than by argument -- the front end IS the per-claim cost in this module, and the shared-producer tier does move it. AND IT RESOLVED THE EARLIER MYSTERY IN THE OTHER DIRECTION. I had reported the claim_batch-vs-floor disagreement on this module as an instrument quirk, because the floor was green on the same witnesses my instrument refused. It is not the instrument: the floor now reports the SAME error the moment the normalized tree is produced outside the frame that consumes it. Two observations, one mechanism -- a normalized tree does not survive being handed across that boundary. The instrument was never the variable, and I said it was. WHAT RETURNS THE ROWS, as a capability: a normalized tree that survives the cross-claim serve boundary, so the value a claim is handed is the value it would have derived. The producers stay as plain helpers -- each claim calls one and derives its own tree, exactly as before the share -- so this file is now behaviourally identical to the pre-cut state with the measurement recorded in it. The per-claim front end therefore stands, and the budget question it raises is a budget question rather than a witness question. No witness here should be moved onto a fixture to buy it: that trades what these witnesses prove. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Semantic-neutral by construction: only names shrank -- module names, the list binder, the lambda binders. The RED still copies the accumulator through list_append inside the fold, the GREEN is still its non-copying twin, and the ledger probe still calls a combiner no registry knows. No arm, type annotation or call shape was touched, because each of those is what the gate reads. So the run measures cost and nothing else. THE PREDICTION IS STATED BEFORE THE MEASUREMENT, so it can be wrong rather than fitted afterwards. Two points from the earlier lower-bound measurement -- 88 bytes at 534ms, 116 bytes at 618ms -- put the marginal cost near 3ms/byte and imply about 285ms paid per claim BEFORE a single byte of snippet exists. These cuts remove 9, 10 and 19 bytes, so the predicted saving is tens of milliseconds against a worst row that needs 180. Projected: ~591, ~504, ~623 against a 500ms budget. If the floor lands them clearly under 500, this model is wrong in the useful direction -- the front end is superlinear in source size rather than mostly fixed -- and the sources were the defect after all. If they land near the projection, the sources were never the defect and the budget grain is, which is a declared-drop question rather than a witness question. The floor decides either way: claim_batch cannot measure this module at all, because it fails at the same serve boundary that broke the withdrawn share. THE FIXED COST IS THE FINDING, not the saving. ~285ms of front end per claim before any snippet exists is a section-6 bare-minimum-cost defect in its own right, and it is the same subject as the serve-boundary work item: netting that survives consumption is exactly what would delete it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Review 63901. The note asserted "Witness accumulation on the subtree fold uses prepend-then-reverse, not append-in-step" while the fold does exactly append-in-step: list_append(left: child_ws, right: ws) inside step copies the child's whole accumulated list every step, with one list_reverse at the end. TWO THINGS COMPOUND AND THE SECOND IS THE ACUTE ONE. The cost shape is real, and it is the accumulator-copy shape THIS DOOR'S OWN LENS EXISTS TO REFUSE. But the note is not prose: this PR's own annotation states it is the COMPARED VALUE that the Gate-A witness asserts byte-equality on. So a false cost claim was green by equality on both sides -- a check certifying its own wrong description. I DID NOT "FIX" THE FOLD, and that is a decision rather than an omission. list_append costs its LEFT operand; the carrier's rc_list_concat copies its RIGHT one (dag/std/nat.dag already records that asymmetry as a measured cost shape). Neither the accumulator nor a child's subtree accumulation is reliably the shorter, so no argument order makes a fold over a tree linear -- it needs a concat that copies neither operand, which is carrier work. Swapping the operands would have moved the copy while letting me report the defect fixed, which is the same species as the claim I am deleting. So the note now states what the code does, names the shape, says why the repair is carrier work and not an argument order, and says why it is stated in a compared value at all. DESIGN section 6 root-causes to the language layer rather than patching locally; section 5 forbids the fabricated claim regardless. Byte-equality preserved: both sides carry the identical 2088-byte note, verified by extracting the .dag string and asserting containment in the oracle rather than by eye. gunbc compile --entry 00_compile.dag --target dag: 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…verts Review 63922, plus the revert the measurement earned. THE COUNT COULD NOT FAIL. Both coverage assertions checked `length(rows) == length(roster())`, and both sides derive from the same fold inside join_required_lens_coverage, which emits exactly one row per registration by construction. The conjunct was structurally green and said nothing about WHICH lenses were covered -- while the comment beside it claimed the closed rows are the roster's own identities, which is more than a count establishes. DESIGN section 5: completeness is an identity join, not a count equality. The case a count cannot see is concrete: a join that DROPS one registration and DUPLICATES another keeps the count exactly equal. rows_join_the_roster_exactly runs the join at (identity, grain) in BOTH directions, because the directions fail differently -- a registration with no row is a lens that never ran, and a row naming no registration is coverage claimed for something the roster does not require. Grain is part of the key rather than a separate assertion: the join's own ObservedAtWrongGrain arm exists because covered-at-the-wrong-grain is a different fact from covered. THE SNIPPET CUT REVERTS BECAUSE IT WAS MEASURED AND BOUGHT NOTHING. Paired before/after on the same three witnesses: two of the three got SLOWER after bytes were removed, and the third's gain is the same size as the noise. The prediction in that commit -- a marginal cost near 3ms/byte -- is refuted, and cross-sectionally too, since the shortest source is the slowest of the three. The sources are restored to the forms that read clearly, and the annotation now carries the measured outcome instead of the prediction: the per-claim cost is a fixed front end, invariant to the subject-specific work, and it is closed by the FLOOR-CHANGED-COST-0 long-home arm rather than here. Both modules compile with 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
# Conflicts: # dag/gunbc/recurring_failure_mode/stale_present_tense_coverage_claim_in_the_authority_consulted_first.dag
Review 64177, both findings. No behaviour change. 1. `CompileLens.identity` is authored on the row beside `gate` and bound to it by nothing, so swapping two rows' gates leaves the join closed and the roster digest unchanged. The module claimed more than that in two places -- "registration and observation form one closed, machine-checkable join" and a digest that "does not cover the gate function, which is named by the identity it is registered under". The second sentence asserted precisely the pairing nothing verifies. Both now state the honest claim: a gate REGISTERED UNDER this identity ran at this grain. The residual is recorded at MITIGATION grain with its ceiling and its next-rung trigger beside the field, per section 4b(2). No discriminating RED is authorable today and the annotation says why: a control would have to recover a declaration identity FROM an opaque function value, and one comparing the authored identity to itself would be the permanently-green decoration section 4b warns about at the top rung -- worse than absent, because it would be cited as coverage of the gap it does not close. The trigger is a reified declaration identity for function values, which makes the field derived rather than authored and collapses the pair to one fact. The witness module's own "what this does not establish" roster now names it too, which the reviewer noted it omitted. 2. `first_root_registration` returned the LAST root-grain row: the fold overwrites `acc` on every `CompileLensRoot`. The controls were unaffected (they call it on both sides), but the name asserted a position the code did not have. Renamed to `a_root_grain_registration`, claiming no position at all, because the contract does not care -- and NOT repaired by returning the first, since `unregistered_placeholder_lens()` is itself `CompileLensRoot` and a keep-the-first fold would latch onto the sentinel and never reach a real row. Evidence: claim_batch over required_lens_coverage_join, rc=0, 8 PASS; gunbc compile of v2.compiler.compile, the witness module and the amended failure-mode row, 0 blocking errors each; docs_projection_gate regen is a no-op against the committed projection. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Review 64196, both findings. No behaviour change. 1. The annotation above validate_then_compile said "an obligation that silently stopped executing stops the line". That is false AT THIS DOOR, and the reviewer is right about why: both sides of the join come from required_compile_lens_roster() inside one call. run_required_lens_gates folds the roster and stamps each witness with the identity and grain of the row it is folding, so the observation list is a structural image of the roster rather than an independent reading of it; required_lens_observations then drops any witness that is not a registration before the join is asked. RegistrationUnobserved, ObservedAtWrongGrain, RootLensObservedMoreThanOnce and ObservationUnregistered therefore have no authorable RED here. What can fire is RegistrationDuplicated and RequiredLensRosterEmpty. An obligation stops executing by LEAVING THE ROSTER, and a join whose both sides are the roster cannot see that by construction. The arms are not decoration -- they are discriminated where their REDs are authorable, in the fixture-grain suite, which section 4b explicitly sanctions as the place a compiler's invalid states get expressed. So the honest statement is about GRAIN: fixture-grain the join discriminates six ways, door-grain it catches a duplicated or empty roster. The trigger for the stronger claim is named: an independent observation channel, a receipt carried out of the runner rather than a list re-derived from the roster it is compared against. This is the second inflated claim in this file found by review rather than by me, after the identity/gate binding. Both have the same shape -- a sentence describing what the mechanism would catch if its two sides were independent, when they are not. 2. grain_key was a byte-identical copy of compile_lens_grain_name, and the test hand-rolled equality as a string compare where compile_lens_grain_eq exists -- both in a module this test already imports from (section 3 nicknaming). The copy is deleted and the authority's comparison consumed; the roster digest's grain spelling and the test's can no longer drift. Evidence: claim_batch over required_lens_coverage_join, rc=0, 8 PASS, including refuses_wrong_grain_observation, which is the arm that exercises the swapped comparison; gunbc compile of v2.compiler.compile and the witness module, 0 blocking errors each. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Reviews 64177 and 64196 found two claims in `v2.compiler.compile` that described what a mechanism would catch if its two sides were independent, when they are not. One class, two specimens, so it gets a row rather than two annotations that each explain themselves. `gunbc.recurring_failure_mode comparison_whose_operands_share_a_producer`. The discriminator is one sentence: the comparison's two operands have a common producer. It is decidable by reading each operand back to its source, and it is worth asking before the check is written rather than after it greens. Checked the directory before filing rather than assuming, and the four nearest rows are excluded BY NAME in the row itself. Not `roster_is_its_own_denominator`: there is no second statement there at all and the repair is to obtain one; here two exist and are compared, and the repair is to make one independent. Not `population_selector_that_cannot_admit_a_counterexample`: that is a defect in how a population was constructed by a lexical proxy; here the population is correct and stable and the defect is the second operand. Not `corroboration_without_an_independent_derivation_axis`: that is a property of the relationship between two human readers, which no artifact records, so it carries ceiling 1 and no trigger; this one is mechanical, visible in source at both call sites, and decidable. Not `a_positive_control_certifies_the_defect_it_exists_to_catch`: there the control reads the right accessor against a wrong subject, so a correct subject fixes it; here the subject is right and the comparison still cannot fail. The general form, and the reason it is a control-shaped class rather than a compiler one: it is DESIGN section 5's oracle rule applied to a control instead of to a literal. "A measurement copied from the same current tree is not an oracle" becomes "a list re-derived from the roster it is compared against is not an observation". RUNG FOUND AT is mitigation by review, and an earlier draft got this wrong in a way worth recording: it said `mitigatable` and justified that by pointing at the join's refusal arms firing at fixture grain. Those arms discriminate a malformed observation set; none of them can detect that a comparison's operands share a producer, so that was a fact about the specimen and not containment of the class. Nothing in the corpus asks the question, so the honest rung is what a human reading two call sites established. Ceiling is structurally guaranteed, because operand provenance is a declaration-grain question the Node tree already answers. Class trigger is provenance-aware comparison analysis; the specimen's own trigger - an independent observation channel - is recorded separately and explicitly does NOT discharge the class. Both annotations in `00_compile.dag` now cite the row. Evidence: gunbc compile of the row and of v2.compiler.compile, 0 blocking errors each; docs_projection_gate regen renders the row into the combined view (the roster and that projection are both gitignored, so the row file is the entire committed change). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Review 64245. The grain note admitted a cost defect in this door's own witness fold and disposed of it with "tracked as its own cost defect rather than patched locally here", naming no carrier, row or symbol. Nothing tracked it, so the sentence asserted a disposition that did not exist -- section 4b(2)'s untracked stall, stated in the authority a reader consults first. Filed `gunbc.recurring_failure_mode enforcement_exhibits_the_shape_it_refuses` and cited it from the sentence. The class is the machinery that enforces an invariant being written in the shape that invariant refuses -- DESIGN section 7's self-application obligation failing in the direction nobody looks, because the enforcement's own code reads as infrastructure rather than as a subject. The specimen is half repaired and half standing, which is what makes it worth a row: the subtree fold was already rewritten to prepend-then-reverse, while the concat stands, because `list_append` costs its LEFT operand and `rc_list_concat` copies its RIGHT one and neither accumulation is reliably shorter. The trigger is named as a CAPABILITY and the falsified experiment is recorded beside it: a concat that copies neither operand, which is carrier work in the list algebra and explicitly NOT a rewrite of call sites -- docs/plans/emit-type-surface-traversal-cost.md tried exactly that substitution at 215 sites plus rc_list_concat and measured byte-identical output with no measurable change at the emit seam. That is evidence about that seam and not this one, and it is written down so the next author does not re-run a falsified experiment believing it is the repair. The row's own next rung is the required-lens gates applied to the compiler's own modules as ordinary subjects, which is section 7's claim made executable. The seed mirror moves in lockstep: both sides of the self-host behavioral receipt are byte-identical at 2556 characters, asserted by comparing the extracted strings rather than by inspection. Evidence: gunbc compile of v2.compiler.compile, the new row and the cause-swap witness, 0 blocking errors each; claim_batch over claim_entailing_evidence_cause_swap_witness, rc=0, 8 PASS -- that suite carries the transcript fixtures that mention this declaration, and its `seed_len` figures are authored specimens of transcript SHAPE rather than live measurements of the string, so they are unaffected by its length changing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
…t hold
Review 64262, plus the dark row gunbc#11073's long-home arm exposed.
WHAT THE ARM FOUND. v2.test.long.accumulator_copy_compile_gate
gate_red_quadratic_rejects failed on its FIRST REAL EXECUTION (srv3-02, no
thrash). It is not a regression: run with one binary against origin/main and
against this head, it FAILS on both while both sibling controls PASS on
both. It had simply never run, because its home test/claim/long/ is a
witness_exclusion_frontier pattern and no required lane plans it.
AND THE FAILURE IS THE WORST OF THE THREE AVAILABLE. A three-way
discriminator separates them: the specimen normalizes fine, the gate does
not reject with a wrong reason -- accumulator_copy_compile_gate ACCEPTS it.
accumulator_copy_findings returns NO suspect for
fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) }),
which is the textbook shape the lens exists to refuse.
Three consequences, all here, none of them the analyzer repair (that is its
own lane, starting from the discriminator posted on the PR):
1. RUNG HONESTY. accumulator_copy_obligation claimed MechanicallyPreventable
on the strength of that control. Executed evidence says the invalid state is
not prevented, so the claim is downgraded to Mitigatable -- the gate is
total and returns a typed outcome, so harm is contained and nothing above
that is established. DESIGN 4b(1) admits only the rung executed evidence
supports, and the restoration is the analyzer trigger rather than the
witness greening by any other route.
2. THE CLASS. gunbc.recurring_failure_mode
required_lens_red_control_never_executes_from_its_home: a lens enrolled as
required, reporting a mechanical rung, whose discriminating red lives where
the floor never plans. The discriminator is a JOIN -- the cited red and the
planned population do not intersect -- which is why neither roster looks
wrong alone. Ceiling structurally guaranteed, because that join is over two
rosters this tree already declares.
3. THE KNOWN RED, without which the floor stays red on every future head.
Admitted in gunbc.explicit_witness_admission with a dissolution naming the
CAPABILITY: accumulator_copy_findings returns a non-empty suspects list for
the fold-append specimen and the gate refuses that tree. That fact is false
today and was MEASURED false by execution on both trees, so the trigger
cannot be satisfied by editing the specimen or the control -- which is
exactly the defect that roster's own note records two lanes failing.
REVIEW 64262. The expanded grain note restated the body of the row this PR
files, and transcribed a 215-site measurement into two files including the
Rust oracle mirror. Both are right: the prose was the duplicate rather than
the carrier, and section 6 says name the instrument, never transcribe it.
The note now cites the row instead of restating it; both sides byte-identical
at 2117 characters, asserted by extracting and comparing.
Evidence: compile 0 blocking on all four touched authorities and the new
row; v2_compile_obligation_census_witness 9 PASS. exact_witness_admission
carries three failures that are IDENTICAL on origin/main (18 PASS 3 FAIL
both sides) and my row satisfies explicit_witness_admission_well_formed by
inspection of the predicate -- QuarantineProbeExpectRed executes, entry
non-empty -- and shares kind and budget with an existing row in that batch.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f
Contributor
|
Closing: spurious duplicate. This was auto-attached from Its content is already on main: all three failure-mode rows ( Worth stating why this mattered rather than just closing it: the branch is also 38k lines behind main, so a merge of this PR would have re-applied landed work and reverted everything main gained since. Resetting the branch to main so it stops re-proposing. — sent from calm-crane-722 |
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.
Auto-opened by session-dashboard for session
calm-crane-722.Pushing to
session/calm-crane-722advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan