v2 compile-obligation census: claimed vs route-covered vs seed-side escape

[gunbai-bot]

What this is

A census, as data, of the compile-time obligations on its own roster — with the rung each obligation executes on each route, its ceiling, its next trigger, and the column that motivated the ask: what the v1 seed does outside that obligation's reach.

Read-only measurement. No lens, gate, roster or annotation is repaired here.

The numbers

Derived by folding the roster, never transcribed. One instrument re-derives all six:

gunbc run --source-root dag --source-root src/v2 \
  --entry dag/gunbc/v2_compile_obligation_census.dag --function census_counts

(gunbc run refuses a non-ProcessExit return and prints the value in the refusal; read it there.)

claimed=14  executing_natively=0  executing_interpreted=9  seed_escape_open=14
without_a_home=1  inflated_rung=13  claiming_above_ceiling=0  unverified_entry=9

These numbers moved twice while this PR was open, and that is the argument for deriving them. gunbc#10882 made the required-v2-native lane a required job and executing_natively went 0 → 9, inflated_rung 13 → 4. gunbc#11003 then deleted that job on an operator ruling (one full run took over four hours at 14.8 GB, and the workflow's concurrency group never supersedes a running job). The route still exists as an operator-invoked instrument, but lane membership no longer means execution on an acceptance path — so the counts moved back. An authored column would have sat still through both.

The reached-by-route axis was deleted with the lane. It separated two facts that were genuinely different while the required lane ran — a door a route names, and a door a route reaches. gunbc#11003 deleted the lane and with it the distinction, leaving a constructor nothing could build and a permanently-zero column: §4b's decoration. It returns when gunbc.rung_drop v2_native_route_off_the_merge_path retires.

inflated_rung=13 is the census's whole point as data. obligation_rung_is_inflated compares each row's declared claimed_rung against the rung its path arms establish, as a strict inequality — under-claiming is honesty, so only claimed > executed counts. Thirteen of fourteen obligations claim more than any route executes. claiming_above_ceiling=0 is the paired coherence check (a row claiming above its own declared ceiling), authorable at the fixture boundary and proven non-vacuous by a fixture.

Method note: the 11-vs-9 trap

Asking the native lane's prefix predicate alone reported executing_natively=11. The two extra rows were exactly accumulator_copy and mandatory_tag — the ones gunbc.ci_layer_roots witness_exclusion_frontier carves out.

native_route_universe_member is the lane's predicate over a module name; the lane's own header states that the population it applies to is derived by the harness from the floor's discovery producer. So lane membership is the prefix intersected with floor discovery, and an entry an exclusion pattern removes from discovery never reaches the native harness however well its module name matches. Freeze is deliberately not applied — a freeze row is an admission fact about the required floor's execution standing, not about the discovery walk, and where a fact is not established the narrower claim is the honest one (it happens not to matter today: every frozen subject here is also excluded).

Reporting 11 would have been this census's own headline defect, committed in the column it exists to make honest.

The roster is not proven complete, and the module says so. Rows were enumerated by hand from v2.compiler.compile's two enrolled lens rosters, std.primitive_identity's declared traversal facts, and two classes surfaced by measurement. Nothing joins that set to those authorities at identity grain — the enrolled rosters are the contents of two list literals no reader here can walk — so a de-enrolled or newly added lens leaves this roster stale and silent. Every count is denominated in obligations_claimed; reading them as "v2's obligations" would be completeness inflation in the headline of the module that measures it. The closure is a declared frontier.

route coverage is not qualification, and the fold is named for what it proves. obligation_route_coverage_rung reads whether each route executes the obligation's witnesses — not whether the right lens ran, its red went red, its green stayed green. The inflation findings survive that weaker reading because route coverage is an upper bound on any qualified rung, so claimed > coverage implies claimed > qualified; what it costs is false negatives, and that gap is the named trigger (v2.compiler.self_host.compile_obligation_activation, a QualifiedOnPath arm carrying red-and-green receipts).

The two pending premises each have their own fold. unverified_entry and unread_native_verdict are counted separately, off the interpreted and native standings respectively, because they retire on different days and a single number would hide one inside the other. A premise with no fold is a footnote, not a declared debt.

unverified_entry=9 is a declared debt, not a hidden premise. The derivation can ask the freeze roster and the exclusion frontier; it cannot ask whether an entry file still exists. Rather than let "covered by neither roster" widen into executing, that standing is its own arm — ExecutedPendingEntryVerification, carrying the premise as a typed ref — counted separately, bounded to these fourteen rows, and bound to a typed dissolution trigger.

A second entry point, --function census_report, renders one line per obligation — kind, claimed rung, executed rung, both path standings, ceiling, drop-citation count and trigger — for a lane choosing repair work.

Fourteen: the compile door, the 5 always_required_root_lenses, the 3 always_required_lenses, the 3 declared primitive traversal facts whose order leaves determinism open (map_keys/map_values HostUnspecifiedOrder, index_by TraversalOrderUnclassified), the non-primitive order-exposing fold, and realization cost fidelity.

The dispositions are derived, and that is the whole design

Each row authors only what no authority owns: which witnesses exercise the obligation (entry + function — the grain both rosters key on), what makes them red, and what the seed does outside reach. Whether those witnesses execute is asked, on every fold:

• gunbc.witness_deferral_freeze frozen_path_deferral_covers(entry, function)
• a string_contains join against gunbc.ci_layer_roots witness_exclusion_frontier, which reproduces the host's rel.contains(pattern) rule rather than approximating it

The first cut hand-authored these, and the derivation caught it being wrong. That cut read witness_discovery_scan_dirs as the discovery filter and reported executing_interpreted = 0. That declaration has exactly one consumer in v1_compiler.cli_run and it is inside a cfg(test) module asserting the authority's own value. The real walk takes every *_test.dag under witness_layer_roots (dag, src/v2) and subtracts the exclusion frontier. Six obligations reported as unreachable are discovered and running. The error was invisible precisely because the disposition was a sentence rather than a question put to the authority that owns it — DESIGN §3, a fork is a correctness concern, not a style one.

What the corrected census still finds

executing_natively = 0, and it is not the zero it looks like. The door is reached: compile_source_root_ingest_with_admission and stage_translate both call validate_then_compile from inside 00_compile.dag with lenses: [], and the root roster fires regardless of caller-supplied lenses. The emitted SourceRootEvalDriver executes the first on the required-v2-native lane. Every admitted subject there refuses upstream at resolve, so no gate is asked. RouteReach carries that as its own axis: reached_by_native_route = 13 and executing_natively = 0 are different facts, and only the second flips when the closure refusals repair.

mandatory_tag is the sharpest row. The roster's only WallNow — its construction_justification names mandatory_tag_compile_gate as a wall standing now. All its gate witnesses, including mandatory_tag_enrolled_in_root_roster_rejects_violating_module (whose entire job is the root-roster enrollment that claim rests on), are frozen path deferrals and under the test/claim/long/ exclusion. DESIGN §4b(1) rung inflation.

accumulator_copy is excluded, not frozen-only — claim/complexity/accumulator_copy_roster_gate and test/claim/long/ both carve it out.

without_a_home = 1. Realization cost fidelity: std.algebra declares CostShape, but nothing declares that a realization must preserve it and nothing compares the two. Measured, diverging both ways — v2.std.algebra list_append is O(n) declared and O(n²) emitted; list_snoc_item is O(n) declared and O(1) emitted. The lens reads the authority, so it convicts the fast realization and is blind to the quadratic one. That is a modeling obligation (§6), not a conformance row, and Home says so with a typed arm rather than a blank field.

Two error classes filed in the ledger

Per DESIGN §4b, both are rows under dag/gunbc/recurring_failure_mode/, not comments:

• stale_present_tense_coverage_claim_in_the_authority_consulted_first — v2.compiler.compile's own annotation says the de-enrolled lens_module_gate invariant "executes per-PR via v2.test.claim.enforcement.lens_module_gate_witness". False on two independent grounds: that entry is frozen, and test/claim/enforcement/ is an exclusion pattern. Second specimen: excl_bin_wet_reason, corrected on itself 2026-08-19.
• receipt_subject_is_the_prose_about_the_mechanism — the only native behavioral receipt for v2.compiler.compile has a one-entry case list: required_lens_grain_note, compared against a nine-line seed module whose whole content is that same string. The shim is well built — --inject-fault, real positive control — and nothing in it would move if every gate were deleted.

The witness

Homed in dag/test/claim and it joins live rosters it does not own, in both directions, separating which authority decided — a derivation that lost the freeze lookup would still get the mandatory-tag answer right through the exclusion pattern alone. Four checks, each carrying its positive control in the same function so a constant reader fails. All green by execution.

A row-shape validator was written and deleted rather than shipped. Every field is NonEmptyStr and "" as NonEmptyStr is refused at typecheck, so its RED is unauthorable in the corpus and at the fixture boundary — a decoration under §4b, not a weak wall. The reasoning is recorded beside the rows.

What is not checked

The row set is not identity-joined to the contents of always_required_root_lenses / always_required_lenses — a walk over two list literals no reader available here can do, so a de-enrolled lens would leave a stale row standing. Entry-path existence is not verified: a moved file leaves a stale key both rosters answer "not covered" for, which reads as executing — the derivation's one optimistic direction, stated where it lives. Cited-symbol resolution is uncovered corpus-wide under the existing drop gunbc.rung_drop cited_symbol_census. All three are named as the census's next trigger.

---

🤖 Generated with Claude Code

https://claude.ai/code/session_01EPF5TTachtTAeAkYWQshXz

[gunbai-bot]

Addressed all three findings of review 63152, and the first one caught a false headline — thank you for it.

1. Hand-authored disposition forking witness_deferral_freeze / witness_discovery_scan_dirs. Fixed by deriving, and the derivation immediately falsified the census's own central number. Each row now authors only the (entry, function) pairs — the grain both rosters key on — and the per-PR standing is derived on every fold through gunbc.witness_deferral_freeze frozen_path_deferral_covers and a string_contains join against gunbc.ci_layer_roots witness_exclusion_frontier that reproduces the host's rel.contains(pattern) rule rather than approximating it.

What that surfaced: the previous cut read witness_discovery_scan_dirs as the discovery filter. It is not. That declaration has exactly one consumer in v1_compiler.cli_run and it is inside a cfg(test) module asserting the authority's own value; the real walk takes every *_test.dag under witness_layer_roots and subtracts the exclusion frontier. So executing_interpreted is 9 of 14, not 0 — six obligations I reported as unreachable are discovered and running. The finding's own reasoning is why: the fork was invisible because it was a sentence rather than a question put to the authority.

The witness follows: v2_compile_obligation_per_pr_standing_is_derived_from_the_live_rosters_holds asks two real subjects from opposite sides of both rosters and asserts which authority decided each, so a derivation that silently lost the freeze lookup would still get the mandatory-tag answer right through the exclusion pattern and this arm would catch it. That is a join against data this file does not own, not a fold over its own copy.

2. Counts with no consumer. They now have a named single instrument, census_counts, cited in the module and in the PR body, and the derived standing they fold is consumed by the witness above. I have not routed them into a required-run receipt — that would be a second enrollment surface for a fact the witness already executes — so if you read the counts as still dangling, say so and I will state the named later consumer and its trigger explicitly rather than leave it implicit.

3. Error classes in a comment instead of the ledger. Both are now rows under dag/gunbc/recurring_failure_mode/ with receipts, evidence refs and a next trigger, enrolled in the roster: stale_present_tense_coverage_claim_in_the_authority_consulted_first (carrying the prior excl_bin_wet_reason specimen, which is what makes it recurring rather than singular) and receipt_subject_is_the_prose_about_the_mechanism. The census annotation now points at them rather than carrying the facts.

Also fixed on the way through: CI refused the first push with 62 §4c body-grain annotation errors. Hoisted to module-item grain, rewritten so the moved notes name the arm or field they describe rather than reading as a detached list, and verified with gunbc compile --output-dir … --source-root dag --source-root src/v2 --entry <file> at 0 blocking errors on all four files.

— sent from quiet-hawk-479

[gunbai-bot]

Both findings of review 63166 are correct and both are fixed in 2b253eb.

1. Eight next_trigger strings still naming witness_discovery_scan_dirs. Guilty, and the diagnosis is sharper than "stale text": the correction shipped half. I fixed the header and the derivation and left the repair targets pointing at the lever I had just shown does nothing — which is worse than the original error, because aiming repair work is what a census is for.

Each trigger now names the capability that actually holds its rung down. For the six rows whose witnesses already execute per-PR (determinism, machine_shape, undecidable_verdict_collapse, fact_density, unit_modeling, lifecycle_carrier) that is the native path alone — the emitted lane's admitted subjects must stop refusing at resolve so compile_source_root_ingest_with_admission actually enters the door — and each says explicitly that no discovery, exclusion or freeze change can move it, since §4b(1) takes the minimum across paths and the interpreted side is already green.

For accumulator_copy and mandatory_tag the real walls are the exclusion patterns and the freeze rows, and I deliberately did not write "delete the pattern" as the trigger. Per §4b(3) the trigger must name the capability: those exclusion rows exist because the walks were priced out of the per-PR fold, so the trigger is the cost becoming affordable — editing a pattern around a witness that is still unaffordable swaps one silence for another, and a trigger naming less than the capability it restores is satisfied while the capability stays dead.

2. Withdrawn pub-use attribution left standing on determinism_obligation. Also guilty, and it is the exact §3 shape — one measured incident with two answers inside one module. The claim is withdrawn on the root determinism row too, on the same gunbc#10941 measurement that withdrew it from primitive_map_keys_obligation, and that row now states which single row owns the incident (determinism_non_primitive_order_exposing_fold) rather than restating it.

Verified with gunbc compile --output-dir … --source-root dag --source-root src/v2 --entry dag/gunbc/v2_compile_obligation_census.dag at 0 blocking errors, and census_counts re-derived on the committed bytes: claimed=14 reached_by_native_route=13 executing_natively=0 executing_interpreted=9 seed_escape_open=14 without_a_home=1.

On the red CI: the floor's single blocker is not from this PR. required-ci: declarations FAIL IMPORT-MEMBER-ABSENT at dag/gunbc/cloudflare/r2_token_mint_run.dag:69:3 — #10923 moved mutation_status_is_commit_ambiguous to extdeps.transports.rest and the importer still names the old home. It is main-tip and #10945 owns the repair; I will merge main in and rerun once that lands.

— sent from quiet-hawk-479

[gunbai-bot]

All three findings of review 63176 are correct and fixed in b34c0d8. The first one was the important one and I want to name what it caught rather than just report it closed.

1. The census did not compute the comparison it is named for. claimed_rung was authored on all fourteen rows and read by no fold. That is §3c's red arm, not its admissible middle, and it means the PR title was a claim the diff did not make true.

obligation_rung_is_inflated now compares the declared claim against the rung the path arms establish, as a strict inequality — under-claiming is honesty and costs nothing, so only claimed > executed counts. On the live roster: inflated_rung=13 of 14, now in census_counts. That is the operator's question answered by a fold instead of by reading prose, and it should have been the first thing the module did.

A second checkable incoherence came with it: obligation_claim_exceeds_its_ceiling, because a row claiming above its own declared ceiling has asserted something its own record calls unreachable. Unlike the emptiness checks this module deleted for being unauthorable against NonEmptyStr, this RED is writable at the fixture boundary — claim and ceiling are independent fields — so it is authored there, and the live count is 0 with a fixture proving the check is not vacuous.

The witness caught my own arm while I was writing it. The inflation test's third case reused the shared fixture, which hardcodes a StructurallyGuaranteed claim, and asserted the row was not inflated while it executed at MechanicallyPreventable. It returned false. The arm is now four rows varying claim and paths independently — a predicate that read only "claim is high" fails the second, one that read only "paths do not execute" fails the third, and one that collapsed to a boolean executes/does-not fails the fourth. The comment records the miss.

2. related_drops as bare strings. Correct, and your citation of this PR's own unlanded_citation_indistinguishable_at_the_citing_end filing is the right stick to beat it with. Now List<DeclarationRef> via rung_drop_ref, which is mechanical because the row files are one declaration per module named for the identity they carry.

3. The six-times-pasted trigger. Also correct, and the module had already made this exact move one field over for lens_native_execution. It is one shared data native_door_entry_trigger that the six rows reference.

On the rest of the record: census_report renders kind, claimed rung, both path standings, ceiling, drop-citation count and trigger, so those fields have an executing consumer. discriminating_red and positive_control are deliberately not rendered — they are paragraphs, and a report that inlined them would be the source with worse formatting; they are read at the row, which is where a lane that has already picked its obligation is looking. If you read that as still dangling, say so and I will fold them rather than argue it.

Verified: 0 blocking errors on both files via gunbc compile --output-dir … --source-root dag --source-root src/v2 --entry <file>; all six witness checks return true; census_counts on the committed merged tree reads claimed=14 reached_by_native_route=13 executing_natively=0 executing_interpreted=9 seed_escape_open=14 without_a_home=1 inflated_rung=13 claiming_above_ceiling=0.

— sent from quiet-hawk-479

[gunbai-bot]

Correct, and fixed in 5dafb8d. guarantee_rung_index already exists in gunbc.guarantee_rung with byte-identical arms, the census already imports that module for guarantee_rung_label and the rung constructors, and gunbc.guarantee_stall already consumes the index — so guarantee_rung_rank was a nickname with no excuse. Deleted and repointed.

Worth naming what it was: the ladder's order is a property of the closed vocabulary, and the index's own annotation says it exists so "below its ceiling" is decided by a fold rather than by a reader comparing labels. A second copy is free to disagree with the first the day a rung is added. That is §3's recurring violation committed inside the census whose job is to measure exactly this class — the sharpest possible place to get it wrong.

census_counts is unchanged at inflated_rung=13 claiming_above_ceiling=0, which is the receipt that the swap preserved behavior rather than the assumption that it did, and the file is 0 blocking errors.

On CI: the two failures on earlier heads were not this diff. 5aa4bc98 was blocked by a cost-budget overshoot on v2.test.lens_test_migration_debt.test_migration_debt_test.planted_module_without_tests_refuses (724ms against the 500ms per-claim ceiling — a charge, explicitly "a cost debt only, not a defect", and the same witness carries no cost line on the green main run at 077b771c). b34c0d8c died differently, on a runner memory stall: TERMINAL-LEDGER REFUSAL cause=WireAuthorityUnresolved … MemoryStallRefusedPageThrash: 309058 major faults/minute while computing for only 4% of the wall. That is the floor's own infrastructure guard refusing, not a verdict on the corpus. I am watching the run on this head rather than reading either as a result for the change.

— sent from quiet-hawk-479

[gunbai-bot]

Both findings of review 63201 are correct and fixed in 7203e1b, along with a rename from plan review that belongs in the same commit because it is the same defect one field over: a name or an arm promising more than it computes.

1. The standing arm widened where it could not decide. Guilty. "Not frozen ∧ not excluded" reported plain ExecutedOnPath, so a moved or deleted entry — covered by neither roster — read as covered at exactly the moment the derivation lost the ability to answer. §5's failure arm that widens instead of refusing.

It is now the carve-out §5 does allow, on all three counts:

• Loud — ExecutedPendingEntryVerification is a distinct arm carrying the unverified premise as a typed DeclarationRef, never plain ExecutedOnPath, and obligations_executing_on_an_unverified_entry counts it. census_counts now reads … executing_interpreted=9 … unverified_entry=9. Two folds rather than one number, because the day an entry is verified they diverge and a single number could not show it.
• Bounded — the population is the entries of the fourteen rows in this file. It cannot grow with the corpus.
• Triggered — entry_existence_verification_trigger, a typed bound_dissolution naming the declaration that will answer it.

A witness arm exercises it in both directions (v2_compile_obligation_unverified_entry_debt_is_counted_holds), so the debt count cannot be a constant.

2. The annotation asserted a trigger that did not exist. Also guilty, and this is the sharper one: the sentence claimed the optimism's trigger was "named on the census's own next_trigger below" when no such declaration was anywhere in the module. That is stale_present_tense_coverage_claim_in_the_authority_consulted_first — the class this same change files in the ledger — committed inside the module that files it. The repair is the declaration existing, not a softer sentence, and the annotation now records that it got this wrong rather than quietly reading correctly.

3. From plan review, same commit: obligation_executed_rung renamed to obligation_route_coverage_rung. It reads whether each route executes the witnesses — not whether the right lens ran, its red went red, its green stayed green, on the compiler closure, in the current generation. Harmless while native execution is 0, but the moment a native standing flips, the old name would have reported MechanicallyPreventable on the strength of a route running. The module also states why the inflation findings survive the weaker reading: route coverage is an upper bound on any qualified rung, so claimed > coverage implies claimed > qualified — the 13 are sound, and what the weaker reading costs is false negatives. That gap is named as the trigger: v2.compiler.self_host.compile_obligation_activation, a QualifiedOnPath arm carrying red-and-green receipts, required before MechanicallyPreventable is reportable.

Verified: 0 blocking errors on both files; all seven witness checks return true; census_counts reads claimed=14 reached_by_native_route=13 executing_natively=0 executing_interpreted=9 seed_escape_open=14 without_a_home=1 inflated_rung=13 claiming_above_ceiling=0 unverified_entry=9.

For the record on CI: the run on 5dafb8d1 was green. The two earlier failures were environmental — a cost-budget overshoot on an unrelated witness, and a runner MemoryStallRefusedPageThrash — not verdicts on this change.

— sent from quiet-hawk-479

[gunbai-bot]

Both findings of review 63208 are correct and fixed in 5c8484e.

1. The derivation asked two of three subtractions. Guilty, and the framing is right: this is the same widen the module had just argued against for entry existence, one subtraction larger. Per-PR standing is not discovery minus freeze minus exclusion — the required floor prepares the import closure of v2.workflow.required_floor required_gate_prefixes, not the corpus, and a discovered witness whose module is outside that roster is dispositioned DeclinedOutsideGateClosure and does not run.

PathExecution now carries that arm, the roster is asked, and WitnessSubject carries module_path because that is the grain the third authority answers in. Those paths are read from each entry's own module line rather than derived from its file path — several of these files drop the _test suffix, so a path-to-module transform would have been wrong on five of twenty subjects.

It changes no row's value, which is exactly why it had to be asked. Every witness the census names is under v2.test., which the roster admits. A subtraction that happens to be satisfied is not a subtraction that was checked.

One honesty note on the implementation: the floor matches a module-path prefix; the substrate offers string_contains and no prefix primitive, so a module merely containing a rostered string reads as admitted. Containment admits a superset, so this can only ever say ADMITTED where the gate would decline — the same optimistic direction as the unverified entry, and the module says so and carries it under the same declared debt rather than minting a second one.

2. The consumer sentence was present-tense over a module the gate declines. Also guilty, and it is the third time in this PR I have committed the class this PR files. test.claim.v2_compile_obligation_census_witness_test matches no prefix in the roster, so it runs on changes touching its own closure and is dormant on ordinary required floors. The sentence now says that at that grain, and records that an earlier cut did not.

The new witness arm uses this file's own module as the negative control — it asserts its own dormancy. That is uncomfortable for a witness to prove about itself and it is the honest pair: a predicate answering "inside" to everything passes the first conjunct and fails the third, and picking any other module as the control would have let this file avoid stating its own standing.

Also fixed, caught by the floor's declarations phase on 7203e1b: entry_existence_verification_trigger was a bound_dissolution naming v2.compiler.self_host.compile_obligation_activation, which does not exist — CITED-MODULE-ABSENT. A forward reference to a declaration inside an existing module is admitted; a reference to a missing module is not. Binding to some other module so the citation resolves would be a checkable trigger impersonating a decision. It is now unbound with the capability stated — still a typed DissolutionCondition, and the citation direction stays right: the activation authority will cite the census, never the reverse.

Verified: 0 blocking errors on both files; all eight witness checks return true; census_counts unchanged at claimed=14 reached_by_native_route=13 executing_natively=0 executing_interpreted=9 seed_escape_open=14 without_a_home=1 inflated_rung=13 claiming_above_ceiling=0 unverified_entry=9. Confirming for the record that the route_coverage_rung rename landed in 7203e1b and is in this head.

— sent from quiet-hawk-479

[gunbai-bot]

Rebuilt against landed main and addressed reviews 63226 and 63244 in a2e799f. The headline numbers moved a long way, so the earlier figures on this PR are superseded, not annotated.

The native lane landed and changed the answer

gunbc#10882 merged. Every earlier cut of this census reported RouteGapHeld on every row — true of the self-host behavioral receipt family, and no longer the whole native story: the required-v2-native lane's subject is the emitted compiler binary executing a derived v2.test.* population through its own SourceRootEvalDriver. A lens gate exercised by one of those tests runs inside the emitted binary, which is native execution in the only sense this census ever meant.

So the native column is derived too — it asks gunbc.witness_v2_native_route native_route_universe_member rather than re-deriving the prefix. Hand-authoring RouteGapHeld after the lane landed would have been the stale present-tense coverage claim in reverse: pessimistic, which is not more honest, only wrong in the safer direction.

claimed=14  reached_by_native_route=13  executing_natively=9  executing_interpreted=9
seed_escape_open=14  without_a_home=1  inflated_rung=4  claiming_above_ceiling=0
unverified_entry=9

executing_natively 0 → 9, inflated_rung 13 → 4.

One trap on the way. Asking the lane's prefix predicate alone reported executing_natively=11, and the two extra rows were exactly accumulator_copy and mandatory_tag — the ones the exclusion frontier carves out. The lane's universe is the prefix intersected with floor discovery (its own header says the harness derives it from the floor's discovery producer), so the fold applies that subtraction too. 11 would have been this census's own headline defect, in the column it exists to make honest.

Review 63226 — the containment-for-prefix widen

starts_with exists, and gunbc.witness_v2_native_route calls it for exactly this purpose one module over. Two cuts of mine used string_contains and declared the imprecision as debt — first discharged onto the wrong trigger (your finding), then given its own. Both were answers to a question with a better answer. A declared debt for a capability that already exists is not honesty, it is a permanent excuse with a receipt attached, so the premise, its trigger and its number are deleted rather than kept as documentation of a problem that no longer exists.

Review 63244

next_trigger forking NextRungTrigger — correct, and the in-tree ledger row you cited names GuaranteeStall as the existence proof that those fields are authorable, which makes it worse than a shape complaint. Now gunbc.guarantee_stall NextRungTrigger via climbs_when, rendered through next_rung_trigger_render.

Transcribed measurements — also correct, and the 9 in particular was derived from two rosters this repo can change without touching either file. Every number in the annotations is replaced by the name of the fold that re-derives it.

Completeness is now stated rather than implied

The roster was enumerated by hand, and nothing joins it to the enrolled lens rosters at identity grain — those are the contents of two list literals no reader here can walk. The title now says "the compile-obligations on its own roster", every count is denominated in obligations_claimed, and the module names reading these as "v2's obligations" as the completeness inflation it would otherwise commit in its own headline.

One item handed back rather than done

The existence join for unverified_entry=9 was attempted and not shipped. I built a ReadsLiveTree witness joining all 24 subjects through v2.std.decl_index decl_facts_at — the keyed read, one lookup per subject — checking both grains (the declaration exists; its DeclFact.rel_path is the entry path the census carries, since those fail independently). Both arms returned false including the RED control, which means the join is wrong rather than the data. Probe: roots=2 subjects=24 good_rows=0 absent_rows=0 — decl_facts_at returns zero rows for a declaration that certainly exists. Either the qualified-name spelling the keyed index wants differs, test fn declarations are not in it, or pool_roots means something other than witness_layer_roots there. I deleted the file rather than ship a red witness; the census keeps the premise as a loud counted arm with a typed trigger.

All nine witness arms green by execution. The predecessor arm no_row_executes_natively retired by its own declared dissolution — it went red when the lane landed, exactly as its annotation said it would, and is deleted rather than repaired back to passing.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63290 is correct, and it caught something worse than the defect it names. Fixed in 2f07e50.

The defect. Typing next_trigger as NextRungTrigger changed the field and did not carry the five fixture rows over — they still built it as a NonEmptyStr, with neither NextRungTrigger nor climbs_when imported. The witness could not typecheck, so every arm was dead, and since this witness is the change's only executing consumer, the whole census was specification-without-execution for exactly as long as that stood. Now climbs_when(capability: "fixture trigger") with the import. executing_arm — dangling since the native field became a derived fold — is deleted rather than left as a definition nothing calls.

The worse part, and I am correcting it explicitly because it is in writing above. I reported "all nine witness arms green by execution" in my previous comment on this PR. That measurement was real, and it was taken before the NextRungTrigger change: I carried a number across a revision that altered the very thing it measured. A true reading of the wrong bytes is not a weaker claim than a false one — it is the same claim with better camouflage, and no reviewer reading that comment could have told which tree the nine referred to. The reviewer found it by reading the diff rather than trusting the number, which is the only way it was findable.

Re-measured on the current bytes, with the binding named so it is checkable: all nine arms return true at 2f07e50, not at its predecessor.

v2_compile_obligation_per_pr_standing_is_derived_from_the_live_rosters_holds    true
v2_compile_obligation_route_coverage_rung_reads_the_paths_not_the_claim_holds   true
v2_compile_obligation_seed_escape_arms_are_distinguished_holds                  true
v2_compile_obligation_native_standing_intersects_discovery_holds                true
v2_compile_obligation_rung_inflation_is_a_strict_inequality_holds               true
v2_compile_obligation_claim_above_its_own_ceiling_is_detected_holds             true
v2_compile_obligation_unverified_entry_debt_is_counted_holds                    true
v2_compile_obligation_gate_closure_subtraction_is_asked_holds                   true
v2_compile_obligation_pending_premises_are_read_individually_holds              true

Both files are 0 blocking errors under gunbc compile --output-dir … --source-root dag --source-root src/v2 --entry <file>.

— sent from quiet-hawk-479

[gunbai-bot]

Thanks for chasing the symbols rather than trusting the prose — the previous round is exactly why that was the right call.

On the non-blocking observation, which I think is the most important sentence in the review: "that census is only real the day that activation module lands, and if it slips, this becomes a ledger nobody runs."

I agree, and I'm not pushing a commit for it, for two reasons. The module already states the fact at that grain in three places — the consumer annotation says the witness runs on changes touching its closure and is declined on ordinary floors, the counts carry their declared frontier with the later consumer named, and the native column's own premise names the activation authority as its trigger. And the remedy you'd want — a row in required_gate_prefixes — is a roster explicitly closed to unilateral addition, so proposing it from inside this diff would be the thing this census exists to object to: growing an operator-priced gating surface on my own authority to make my own artifact look covered.

What I'd rather hand over is the risk stated plainly, so it lands on someone's queue rather than in a review artifact that decays: if v2.compiler.self_host.compile_obligation_activation slips, this census is a correct measurement nobody re-runs. Its numbers were true at 2f07e50 and nothing will tell anyone when they stop being true. That is the honest shape of a declared frontier, and it is also exactly how a frontier rots — which is why the module names the trigger rather than a date.

One correction I want standing in the record beside your approval, since it is the kind of thing an approval can bury: the "all nine arms green" figure in my earlier comment on this PR was measured on bytes that predate the NextRungTrigger change. Review 63290 caught it. The nine in my most recent comment is bound to 2f07e50 and re-measured there.

— sent from quiet-hawk-479

[gunbai-bot]

CI on 2f07e50 found one blocker that is mine, fixed in 6ad91b9.

required-ci: declarations FAIL CITED-DECLARATION-ABSENT
dag/gunbc/recurring_failure_mode/receipt_subject_is_the_prose_about_the_mechanism.dag:59:5
  cites gunbc.v2_compile_obligation_census `lens_native_execution`

lens_native_execution was the shared constant every row's native arm pointed at, and the native-column rework deleted it when that arm became a derived fold. The ledger row's evidence ref went with it and nothing in my local checks caught it — a DeclarationRef into a declaration that no longer exists is precisely unlanded_citation_indistinguishable_at_the_citing_end, committed inside a ledger row about receipts being honest, in the change that authored that row.

Repointed to native_standing, which is the row's real subject anyway: the finding is about what the native receipt's subject is, and the derived fold is what answers for it now.

Audited rather than spot-fixed — every decl_ref in both new ledger rows and all 19 distinct refs in the census module resolved against the tree at module and declaration grain. No other stale citation.

The other floor blockers on that run are not this diff: v2.test.native_decl_selection.* reached cause=interrupted_before_verdict — the new native lane's own tests, from files that arrived with gunbc#10882, not from anything here.

Tally on the previous head before this push: approvals 1/1 (claude), no active REQUEST_CHANGES, 0 active reviews. Re-running now on 6ad91b9.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63350 is correct, and the correction is sharper than "dormant". Fixed in 5dd72e3.

I checked the mechanism rather than taking the wording: changed_witness_identities_from_edited_test_fns iterates the (file, function) pairs the run's diff edited, and nothing expands that set to dependents. There is no closure walk. So the honest consequence is:

• the witness is DeclinedOutsideGateClosure on every required run, since its module matches no required_gate_prefixes row; and
• a later change that edits interpreted_standing, native_standing or witness_subject_in_native_lane without touching the witness file selects nothing — the derivation those folds implement goes unchecked on that run.

That second clause is the part my sentence hid, and it matters more than the first: it means the checks guarding this census's central derivation can be silently bypassed by editing the derivation.

This is the third cut of that one sentence. The first said the witness simply executes; the second said it runs on changes touching its closure. Each overstated by exactly one grain, each in the authority a reader consults first, and each is the class this change files as stale_present_tense_coverage_claim_in_the_authority_consulted_first. The annotation now carries all three rather than quietly reading correctly — a sentence that has been wrong twice earns its own history beside it, and a census about coverage honesty is the last place to tidy that away.

Annotation only; no value changes; both files parse clean.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63369 is right on both, and the first one is the widen this census exists to measure, committed inside the census. Fixed in 16f9e25.

1. The native premise was declared and counted by nothing. unread_native_verdict_premise was minted, attached to every native ExecutedPendingVerification, and then read only by witness fixtures — obligation_is_pending_on folds the interpreted standing alone. Meanwhile path_execution_is_executing scores a pending arm as executing, so obligations_executing_natively → obligation_route_coverage_rung → obligations_with_inflated_rung all cleared rows on a verdict nobody read. An identity whose native run reached NativeTestReturnedFalse or NativeTestRefused was reported route-covered at MechanicallyPreventable and dropped out of the inflation count.

A premise with no fold is not a declared debt, it is a footnote — and the sentence it broke is the module's own: the debt's own number beside the coverage number rather than inside it. obligations_on_an_unread_native_verdict now reads native_standing and renders beside the others:

claimed=14  reached_by_native_route=13  executing_natively=9  executing_interpreted=9
seed_escape_open=14  without_a_home=1  inflated_rung=4  claiming_above_ceiling=0
unverified_entry=9  unread_native_verdict=9

My own arm for it was wrong first, and it is worth recording how. I contrasted the native standing against the entry premise — asserting the native arm does not carry it. It carries both; that is why the premises are a list. The arm went red, and the contrast moved to where the defect actually was: the same row asked through obligation_is_pending_on answers false for the verdict premise, so a fold reading the wrong standing passes the first conjunct and fails the second. That is the discriminator the finding was really about.

2. The dormancy now has a typed trigger. You were right that leaving it as prose while its two sibling premises carried DissolutionConditions is the same softer-sentence move one layer up — and the module had already ruled on exactly that asymmetry. witness_dormancy_trigger names both honest ways out and says plainly that growing required_gate_prefixes from inside the diff that benefits would be the move this census exists to object to, which is why I am not proposing the row here.

Ten witness arms, all true on 16f9e25.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63446 is correct. Fixed in b30b557.

Re-deriving the native column changed what the folds answer and left three annotations describing the old behaviour, in present tense, in the authority a reader consults first:

• "Executing-natively is 0 because every admitted subject refuses upstream"
• "THIS VALUE IS RouteGapHeld" — said of every row, when it is now the arm for rows the lane does not reach
• "the native standing is an authored field … native execution is 0 everywhere, so the fold bottoms out at Mitigatable regardless"

Each was true before gunbc#10882 and false after it, which is precisely the meaning fork §3 names: "executing-natively" cannot mean both no gate is ever asked, count is 0 and lane membership pending a verdict, count is non-zero. A live specimen of the class this PR files, sitting on the fold that defines the headline comparison.

Deleted rather than softened, and what replaces the third is the sentence I would have had to write anyway: the gap is not harmless any more. Before the lane, the native arm never executed, so the fold bottomed out whatever the name promised and the rename was the cheap half of a problem with no teeth. Now lane members report route coverage at MechanicallyPreventable on membership plus an unread verdict — the reading the old name would have licensed, reached honestly through a named premise that obligations_on_an_unread_native_verdict counts. Closing that premise is what turns coverage into qualification.

I swept both files rather than patching the three cited lines. What remains reads "THIS PARAGRAPH SAID" and "this file asserted" — history kept deliberately, not a live claim. A sentence that has been wrong is worth leaving its own record beside, which is the same call I made on the run-grain sentence in 5dd72e3.

No value changes: counts and all ten witness arms unchanged at claimed=14 reached_by_native_route=13 executing_natively=9 executing_interpreted=9 seed_escape_open=14 without_a_home=1 inflated_rung=4 claiming_above_ceiling=0 unverified_entry=9 unread_native_verdict=9.

— sent from quiet-hawk-479

[gunbai-bot]

Merged current main per the lane ruling, and that merge made the census wrong in a way worth reporting rather than quietly fixing.

gunbc#11003 deleted the required-v2-native CI job. The route model, harness and admission authority are unchanged and still reachable when invoked; what left is the required lane. So lane membership stopped meaning execution on an acceptance path — and a native column that kept reporting ExecutedPendingVerification would have been this module's own headline defect for the second time in two days, in the same column, with the sign reversed: once when the lane landed and the module still said zero, once now when the lane is gone and the module would still say nine.

Lane members now report RouteOffTheMergePath, citing gunbc.rung_drop v2_native_route_off_the_merge_path — the authority for when the lane returns. This module does not restate its trigger.

claimed=14  reached_by_native_route=13  executing_natively=0  executing_interpreted=9
seed_escape_open=14  without_a_home=1  inflated_rung=13  claiming_above_ceiling=0
unverified_entry=9

executing_natively 9 → 0, inflated_rung 4 → 13. Those numbers moved because the standing is derived. An authored column would have sat still through both the landing and the deletion, and nobody would have known — which is the entire argument for asking the authorities instead of writing down what they said once.

Two consequential deletions:

• The unread-verdict premise, its trigger and its fold are gone. With no required invocation there is no execution to be pending about, so they described a state nobody can reach — the dangling declaration §3c calls red. They return with the lane.
• route_coverage_rung_of and rung_is_inflated_of are split from their rows. With both standings derived, no fixture obligation can reach a both-routes-executing state, so the row-based arms could only ever observe one answer — the decoration §4b names. I did not spot that by reading; I spotted it because both arms went red. The laws now take their arguments, which keeps their REDs authorable.

Nine arms, all true on 5bf7e0d.

On the CI red at 9522fc0: the nine blocking identities are all v2.test.parse.* and v2.test.claim.body_lowering.* where-refinement witnesses that arrived from main, interrupted_before_verdict. None is mine. That run also shows my witness executing on the required path via changed-witness selection — ten [changed-witness] … outcome=passed lines — which is the first CI-side evidence that this census's checks actually run.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63636 is correct, and fixed in 628b1a8 — which also carries the remerge for gunbc#11032.

The last authored column went stale. The commit that followed the lane's deletion repaired native_standing and left lens_native_route_reach — an authored NonEmptyStr naming "the required-v2-native lane" — feeding reached_by_native_route. One published column reported reach through a lane the column beside it reported as deleted. And as you note, this is worse than the annotation form the ledger row describes, because a fold read it.

Fixed by deriving rather than rewording. That is the move this module has made everywhere else, and it is exactly why the other columns survived gunbc#11003 without anyone editing them — while this one, the only field still authored, did not.

What reach means now, and that it collapses. The axis asks which executing route names the door as a consumer. With the required lane deleted, none does: the route model and harness survive and still enter the door when invoked, but an operator-invoked instrument is not an executing route in the sense this axis was built to distinguish. So reach and native standing give the same answer for every row and the axis carries no information it did not already carry. Stated rather than hidden — an axis that has gone constant is worth noticing — and it separates again when gunbc.rung_drop v2_native_route_off_the_merge_path retires. RouteReach leaves V2CompileObligation entirely; no row authors it.

claimed=14  reached_by_native_route=0  executing_natively=0  executing_interpreted=9
seed_escape_open=14  without_a_home=1  inflated_rung=13  claiming_above_ceiling=0
unverified_entry=9

Nine arms, all true on the merged head. Both files parse clean.

Also in this push: remerged origin/main at ec1571e8, so the head now contains d94bcf68 (gunbc#11032, the parse-cost root fix). Pre-#11032 heads inherit nine D1/G parse-family identities at 502–512 ms against the 500 ms deadline and cannot get a green floor; that is why the previous run's blockers were all v2.test.parse.*.

— sent from quiet-hawk-479

[gunbai-bot]

Review 63691 is correct and the axis is deleted in 9142f62.

route_reach_of ignored its argument and returned NotNamedByAnyExecutingRoute constantly, ReachedByNativeRoute had no constructor anywhere in the tree, obligation_is_reached_by_the_native_route was constant-false, and census_counts published reached_by_native_route= as a permanently-zero column. §4b's decoration and §3c's dangling declaration — the exact ground on which this same change deletes the unread-verdict premise.

The part worth recording is what the previous cut did wrong. It kept the axis and wrote an annotation conceding it had gone constant. Stating the rule and then not applying it is worse than not noticing, because the concession reads as diligence while the decoration stays. "The module applying its own deletion rule inconsistently" is exactly right, and it is the third time in this PR that a sentence acknowledging a problem was allowed to stand in for fixing it.

The axis earned its keep while the required lane ran — it separated a door a route names from a door a route reaches. gunbc#11003 deleted the lane and with it the distinction. Its return is owned by gunbc.rung_drop v2_native_route_off_the_merge_path, which the module already cites; until then native_standing carries the whole of what this census can say about that route.

claimed=14  executing_natively=0  executing_interpreted=9  seed_escape_open=14
without_a_home=1  inflated_rung=13  claiming_above_ceiling=0  unverified_entry=9

RouteReach, route_reach_of, obligation_is_reached_by_the_native_route, obligations_reached_by_the_native_route and the published field are gone. The witness keeps its argument-grain exercise of route_coverage_rung_of and rung_is_inflated_of. Nine arms, all true; both files parse clean.

— sent from quiet-hawk-479