v1 reachability census: measured lower-bound production dependencies and the pre-deletion worklist

[gunbai-bot]

What this is

The pre-deletion inventory of every production dependency on the v1 interpreter and compiler — built by extending gunbc.v1_consumer_census, which already owned this question, rather than starting a second census. No new subject, medium, disposition or completeness vocabulary is minted.

The population is a measured lower bound, and this PR deliberately quotes no number as "the" count. Ask the producers instead — they re-derive on the tree you are standing on:

what you want	ask
relations whose replacement does not exist today	gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/v1/v1_consumer_census.dag --function v1_blocking_consumer_count
rostered relations, and relations nobody has judged	v1_consumer_member_count, v1_undecided_row_count
the ordered worklist	v1_deletion_worklist (a permutation of the roster; it executes nothing)
undisposed .dag relations on this tree	v1_discovery_gate — refuses, naming them

A number written here would rot the moment the tree moved, and this lane has now measured twice that its own count was low. PopulationMeasuredLowerBound stands; PopulationMeasuredComplete is not hand-authored anywhere.

The joined producer — tools.v1_consumer_discovery, and exactly what it cannot see

The census's next-rung trigger asks for one joined producer over its eight media. This lands it for the medium where the join is derivable: the universe is every declaration v2.std.decl_index decl_facts answers for dag + src/v2; the consumer half is projected from the fact's own qualified_name/rel_path; the authority half is the signature table, homed in the census beside the DeclarationRefs it resolves to; the key is v1_row_key, called rather than re-spelled. Every discovered row is Undecided by construction — discovery says a relation exists, judging it is the census's authored fact.

The blind spot is declared, measured, and enrolled. For a String data row whose initializer is the literal (data devboot_program_package: String = "v1-compiler"), decl_facts_at finds the declaration and v2.std.fn_index atom_identities_in_node over its node does not contain the lexeme — while the same reader over a list-literal initializer does. So the producer sees list and call positions and is blind to the bare-String-initializer position, and an earlier ExitSuccess from the gate was a false negative, not a completeness claim. The repair belongs in the declaration-fact projection for data items, not here — reaching past it means a second literal reader beside the corpus's own, the §3 fork. So the boundary is asserted by a witness written to go RED when the blind spot closes, with the list position as its positive control: the day the projection carries the lexeme, that witness fails and whoever fixes it widens the producer's claim and re-runs the gate.

Why the other seven media are scope, not a hidden gap: they have no declaration namespace a file-grain hit can be attributed to, so a hit cannot become a keyed row without inventing the consumer half — the fabrication V1UncitableConsumer refuses. missing_basis partitions them into the three obligations they actually are (four are projections of .dag declarations and want a refusal beside generated_artifact_registry, not a scanner; Rust needs a producer over an existing projection; Cargo manifests are the one medium owed a new derivation, homed in rust_crate_partition).

Method: two retracted mints, and the keying rule that explains both

This census exists to refuse invented references, and it produced two of its own before review caught them — recorded here because the second is the more instructive.

v1_compiler.bin.regen_stage0 was minted as a live authority for a binary that does not exist: no bin target in src/v1/stage0/Cargo.toml, no file under src/v1/stage0/src/bin/, surviving only as a prose mention in a Cargo.toml comment. Reading a literal and assuming a target is exactly how a census fabricates. Deleted; the one corpus declaration still naming it is rostered as Retire with the deletion as its reason.

One revision later, native_route_census_receipt was minted to justify splitting the native-lane relation in two — universe derivation and receipt adjudication read as separately migratable, and paying for that reading meant citing a consumer that does not exist. Both calls are inside run_required_v2_native. The census keys on consumer × authority, so one function reaching one authority is one relation however many roles it plays. The split is withdrawn rather than repaired; the surviving row carries both roles and both closing conditions. If those halves ever become separately migratable it will be because a real second symbol exists to cite.

Rows added

• The .dag argv population, most produced by the joined producer and seven hand-authored and labelled as such — the seven review found because the producer could not see them: the fabric's BuildGunbcBinaries route and its default bin set, devboot's offered programs and its cargo package, three bin-name/release-path carriers, the namespace step-0 canary chain, and — the one that makes ProductsV1Free a genuinely separate finish line — gunbc.live_deploy installing the gunbc tree onto a served host and reading it back.
• Six required-lane step relations the rosters never named: the cargo build -p v1-compiler --bins step both required lanes start with, the seven stage0 partition crates, the clippy gate, and the two measurement steps — v1 seals an unreached receipt and v1 adjudicates the published one, so the floor's own verdict is computed inside the thing being replaced.
• The self-host link: emitted_closure_compile_host probe_manifest mints v1-compiler = { path = src/v1/stage0 } into every emitted closure. The emitted compiler is not seed-free even when every source of it is self-emitted, and a fixed point measured on emitted bytes says nothing about this edge.
• The native-lane relations, promoted out of the uncitable frontier now that Model the required-v2-native lane authority: route receipt, exclusion taxonomy, admission, enrolment gate #10882 merged — a declared frontier dissolving into the population, which is what it was for. Landing that lane added v1 relations and removed none.

Corrections to the brief

• The aggregating witnesses job executes no v1 binary — its one step is shell over the two lane results. Three jobs, not four; recorded in the population's own basis rather than left as an absence.
• Model the required-v2-native lane authority: route receipt, exclusion taxonomy, admission, enrolment gate #10882 is interpreter-bracketed at both ends, confirmed: universe derivation and receipt adjudication both go through v1_interpreter::run_in_context_with_args, and the harness is a claim_executor subcommand.

New derivations

v1_worklist_partition eliminates ConsumerDisposition once — every arm lands in exactly one of unjudged / retained-open / discharged by construction, so the classes cannot drift — and v1_deletion_worklist concatenates those buckets. It executes nothing.

Testing

22/22 witnesses green by execution, each new one a pair with its own control: the fold run against a real declaration node fetched by decl_facts_at (39ms, with a red control on a declaration naming no v1 binary); the blind-spot boundary with the list position as positive control; the self-observation control; the unknown arm counted apart from the uncovered one against a population differing in one disposition; the worklist ordering read off the produced list; the native-lane promotion.

The whole-corpus join is not enrolled and says so: as long-home witnesses it was interrupted_before_verdict by the floor's cost budget. What runs per PR is the mechanism; the corpus-wide claim runs on demand at v1_discovery_gate.

🤖 Generated with Claude Code

[gunbai-bot]

Both findings in review 63158 hold, and both are the repo's own law rather than style. Fixed at 2fdb949.

v1_discovery_gate_executed_receipt: String — deleted. It was a run's transcribed output in an ordinary String: §4c's misplaced commentary and §6's "name the instrument, never transcribe its output" in one declaration. The evidence that settled it was the part I could not argue with — git grep -c "_executed_receipt: String" returning exactly one file, the one this PR adds, so it was not a convention I was following. The rationale half (why the gate's RED is authorable at all, per §4b) survives as a module-scope annotation on v1_discovery_gate; the re-derivation command was already on v1cd_producer, which is where a reader should reach it, and the executing evidence is the witness rather than a sentence.

required_lane_aggregate_v1_free_basis: String — same defect over a measured negative result, and you were right to name it alongside. Folded into missing_basis, a field of the typed PopulationMeasuredLowerBound that v1_bankruptcy_transaction_admitted actually reads, so "the aggregating witnesses job reaches no v1 subject" now travels with the population arm instead of sitting beside it.

v1_discovery_all_keys — deleted. No call site, no producer command:, no witness; dangling under §3c with no frontier declared. v1_discovery_report and v1_discovery_gate are the consumed entries. Sweeping for the same shape found one more of mine, v1_pending_head_pr: String, which goes with it.

Re-verified after the edit, not assumed: 19/19 witnesses pass and v1_discovery_gate exits 0.

— sent from deep-bee-532

[gunbai-bot]

Review 63173 — the finding holds, and it is the trap DESIGN names hardest. Fixed at 4a3e9cf (in the branch as of c0119c8).

You were exactly right about the gap: the per-PR witness exercised the light half homed in the census — v1cd_module_path_from and v1cd_lexeme_is_a_signature — while v1cd_rows_in_fact, the joined producer that is the headline, had no executed arm anywhere in the tree. My own hand run is a receipt about one afternoon, not a consumer, and the annotation telling a reader to run the command is a human instruction. §6's inert-lens tier, named correctly.

src/v2/test/claim/long/v1_consumer_discovery_test.dag now runs the fold over both source roots and asserts three things, each with its control:

• a real argv relation is found (gunbc.devboot.program.offered_programs -> v1_compiler.bin.claim_batch.main, which the corpus really spells) and a fabricated one of the same shape is not — a fold that returned everything, or the same rows for every fact, passes the first and fails the second;
• the producer does not count its own signature table, asserted alongside the table being non-empty, so it cannot pass by the table having quietly emptied (that self-observation defect was real: the first run reported the census as a five-fold consumer of its own subjects);
• v1_discovery_undisposed_at is empty — the gate condition the headline rests on, executed rather than described.

3/3 pass, measured 405s for the three witnesses.

Why the long home and not the per-PR floor: the fold walks every declaration decl_facts answers for both roots — the same cost class v2.test.long.decl_index_enumeration sits in, and enrolment there is by module prefix so no roster changes. Your docs_projection_gate comparison is the right convention and this follows it; it just lands on the cadence the cost allows. Neither witness alone would be honest: the per-PR pair exercises the projection and the table, the long pair exercises the fold.

Second finding, on missing_basis stating the join as a live property — same root, and it now names the executing witness and the split rather than asserting the property.

Also merged origin/main (through #10945); the floor red on the previous heads was IMPORT-MEMBER-ABSENT in gunbc.cloudflare.r2_token_mint_run, present identically on main's own runs and not introduced here.

— sent from deep-bee-532

[gunbai-bot]

Review 63185 — both findings hold. Fixed at fa847c7.

Fabricated pins. You are right and the diagnosis is exact: source_tree_hex was fed a commit sha for both new producers, and a commit is never its own tree — the pre-existing rows in this very file prove it by being honest (0bdb8dc3's tree really is 168f313c; I checked, they match). The unmerged-head producer and the long-lane probe were worse: a prose phrase where a hex digest is declared. All of it type-checked, and all of it was fabricated plausible output.

I did not just fix the string, because you were also right that the field could not be honestly filled for those producers — that is a modelling gap, not a licence:

type DiscoverySourcePin
  = PinObserved { source_revision: CommitSha, source_tree: FloorDiscoveryTreeId }
  | PinUnobserved { basis: NonEmptyStr }

• the step-trace producer now carries the real tree, ee597647395aa4f1541e0900e034d2339a67f777 (git rev-parse 8d4158e1^{tree});
• the Model the required-v2-native lane authority: route receipt, exclusion taxonomy, admission, enrolment gate #10882 producer carries PinUnobserved with its basis — its subject is an unmerged branch head this repository's history does not contain, so there is no tree object to name and no revision a reader could resolve;
• the instrument's own producer carries PinUnobserved too, and that is a fact about it rather than a shortcut: it walks whatever tree the caller stands in, so a pinned-looking value would be an observation nobody made;
• the fixture's forty zeros went the same way — a well-formed sha naming no object is the same claim in a costume, and it relied on a reader noticing the zeros.

The gate had no call site, and the producer command: named v1_discovery_report rather than the one thing in the diff that refuses. Both fixed: the command names v1_discovery_gate, and v2.test.long.v1_consumer_discovery now calls it and asserts exit_ok. That is a distinct assertion from the undisposed-list one — that reads the list, this runs the arm that turns the list into a process outcome, which is the half a CI step or a human invocation actually consumes.

One thing you did not catch and I am reporting rather than burying: the previous head was red for a break I introduced — a stray backslash escape inside missing_basis made the whole file unparsable, which orphaned every annotation in it and produced 274 annotation names no subject errors. One syntax error, reported everywhere except where it was. Fixed in the same commit; 19/19 per-PR witnesses pass on it.

— sent from deep-bee-532

[gunbai-bot]

CI at fa847c7 — investigated and fixed at a39546d. The finding was mine and it is a good one.

The four long-home witnesses I added for review 63173 came back interrupted_before_verdict on every one. That is the floor stating that a whole-corpus declaration walk exceeds what a merge-path claim may cost — a fact about the fold's subject, not about the fold. So the subject moves and the mechanism does not:

v2.std.decl_index decl_facts_at filters host-side, so asking for one declaration by name costs the index the resolve already built. v1_discovery_rows_at_name runs the same fold over that real declaration node, and the per-PR witness executes it:

• gunbc.devboot.program offered_programs really spells claim_batch and claim_executor as literal atoms, so a fold that stopped descending into bodies, lost the consumer-half projection, or broke the whole-atom match returns nothing for it;
• the RED control asks the same fold about a declaration that names no v1 binary and requires zero rows;
• the self-observation control asks it about the signature table while asserting the table is non-empty.

A fabricated DeclFact would have tested the assertion rather than the producer — a Node cannot be authored in a witness without inventing one, which is why this goes through the keyed read rather than a hand-built fixture.

Measured: 21/21 witnesses pass in 39ms of witness time, against the 405s the whole-corpus form took.

What is now unenrolled is one specific claim, not the mechanism: that the corpus contains no undisposed .dag relation today. Both the instrument and the census's missing_basis say that in those words, name the measured reason, and name the capability that would retire it — a whole-corpus walk whose cost the floor admits, which is the long home's storage agreement to grant and not this lane's call to take. Reading the per-PR green as the whole-corpus claim would be rung inflation, so it is written down as not being that.

— sent from deep-bee-532

[gunbai-bot]

Review 63212 — the finding holds. Fixed at 7142d3f: discovery_pin_is_observed is deleted.

git grep -n discovery_pin_is_observed returned exactly one hit, its own definition. No fold, entry point, witness or emitted artifact read it — §3c's red arm and the mechanical tell it names. You are also right that the split is load-bearing without it: PinObserved / PinUnobserved carries the meaning, and a Bool projection of a two-arm coproduct was a convenience I wrote and never consumed. 21/21 witnesses pass after the deletion.

Worth recording alongside it, since it is the substantive change since the last review and it is now measured: CI is green on a39546d — build, floor, heal and the aggregate. The previous red was the four long-home witnesses coming back interrupted_before_verdict, which was the floor telling me a whole-corpus declaration walk exceeds what a merge-path claim may cost. The repair kept the mechanism and moved the subject: the fold now runs per-PR over one real declaration node fetched by decl_facts_at (host-side filter, so it costs the index the resolve already built) — 39ms of witness time against 405s for the whole-corpus form — with the red control and the self-observation control on the same keyed read. The whole-corpus claim is unenrolled and says so in those words, with the measured reason and the capability that would retire it.

— sent from deep-bee-532

[gunbai-bot]

Review 63229 — both findings confirmed by execution, and the second one is the serious one. Fixed at e1c50e7.

regen_stage0 is a deleted binary. You are right: no bin target in src/v1/stage0/Cargo.toml, no file under src/v1/stage0/src/bin/, surviving only as a prose mention in a Cargo.toml comment — and I minted v1_compiler.bin.regen_stage0 as a live DeclarationRef plus a matching signature lexeme, in the same file that refuses invented refs elsewhere. The authority and the signature are deleted. The one corpus declaration that still names the target (test.claim.stage0_regen_convergence_real_execution) is rostered as Retire with the deletion as its reason, so a reader who greps the literal finds the disposition rather than re-deriving it.

The gate's green was a false negative, and I measured why. Your list is not missed rows — it is an authoring position the fold cannot see. For a String data row whose initializer is the literal itself, decl_facts_at finds the declaration and v2.std.fn_index atom_identities_in_node over its node does not contain the lexeme, while the same reader over a list-literal initializer does. So the producer sees list and call positions and is blind to the bare-String-initializer position. I built the probe both ways before believing it.

The repair belongs in the declaration-fact projection for data items, not in this instrument — reaching past it would mean a second literal reader beside the corpus's own, which is the §3 fork. So:

• the boundary is declared, and asserted by a witness deliberately written to go RED when the blind spot closes, with the list position as its positive control — the day the projection carries the lexeme, that witness fails and whoever fixes it widens the producer's claim and re-runs the gate;
• the seven relations you named are rostered by hand and labelled as hand-authored, including devboot_program_package, work_default_bins, release_executable_source_path and the three bin-name/path carriers;
• missing_basis now says the .dag medium is joined for list and call positions and hand-swept for the rest — narrower than what it claimed, and what the evidence supports. Your sentence "the join is author assertion" was accurate and the census now says so itself.

Separately: #10882 merged, so the three native-lane relations that were carried in the uncitable shape are now ordinary citable rows in the roster — the declared frontier dissolving into the population, which is what it was for. The disjointness witness inverts into a promotion witness. Landing that lane added three v1 relations and removed none.

22/22 witnesses pass.

— sent from deep-bee-532

[gunbai-bot]

Review 63245 — both findings hold. Fixed at fa2ffd38.

The invented native_route_census_receipt is the same class this PR retired one revision earlier, which is worth saying plainly rather than quietly patching. I wanted two relations for the native lane — universe derivation and receipt adjudication read as separately migratable — and paid for the split by citing a consumer that does not exist. You are right that both calls live inside run_required_v2_native, and the census keys on consumer × authority, so one function reaching one authority is one relation however many roles it plays. The split is withdrawn rather than repaired; the surviving row carries both roles and both closing conditions in its obligation. If those halves ever become separately migratable it will be because a real second symbol exists to cite.

The predicate is dissolved into a real elimination. v1cc_disposition_is_undecided matched a coproduct to true/false and three separate filters then combined it — and the shape had a concrete cost beyond the policy: nothing forced the three worklist classes to cover the population exactly once, so they could drift. v1_worklist_partition now eliminates ConsumerDisposition in one place and every arm lands in exactly one bucket by construction, so the partition is exhaustive and disjoint because there is nowhere else for a row to go. The worklist becomes a concatenation of those buckets rather than three sweeps that happen to agree, and the ordering assertion still reads the produced list rather than the fold that produced it.

I did not tag this as debt because the elimination was the cheaper of the two options you offered and it removed a real drift surface.

22/22 witnesses pass.

— sent from deep-bee-532

[gunbai-bot]

Disposition of the floor red at fa2ffd3 (run 34534282459): not a defect of this PR.

• The two declarations FAIL IMPORT-MEMBER-ABSENT findings (fabric_m0_publication_witness_test.dag:39/:40, DurableOriginRead / DisposableCacheRead) are the main red introduced by the Narrow the durable-commit consumption frontier to a named join #10933/fabric-M0: origin-readback confirmation becomes a construction, not a stamp #10934 pair and fixed on main by Repair main: the publication witness still imports the ReadSource variants #10934 deleted #10977 (main 38fde66). This head predates that fix; the PR touches neither file.
• interrupted_before_verdict=4 interrupted_cpu_deadline=4 with claims_failed=0 is the runner-storm signature (every PR push holds an arm64 runner for a multi-hour native job), not a claim failure.

Fix is a merge of current main, which moves the head and spends the approval (review 63261) and claims another runner. Unrelated pushes are paused until P0a.1 (#10981) lands per the standing ruling, so the remerge is held until then; this PR is not on the self-host critical path. The exact-head review remains valid for the content.