Skip to content

Ingestion-time per-module declaration index: land import-member claim integrity, the cited-symbol wall, and module authorship facts on ONE construction, as DESIGN's two next-rung triggers require, instead of three corpus walks - #9211

Merged
gunbai-bot[bot] merged 22 commits into
mainfrom
session/bright-raven-296
Aug 26, 2026

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 25, 2026 •

Copy link
Copy Markdown
Contributor

Builds one per-module declaration index at ingestion, where the module is already
parsed, and derives three facts from that single construction instead of from
three separate corpus walks: import-member claim integrity, cited-symbol
resolution, and module authorship. This discharges the two next-rung triggers
DESIGN names for exactly this — §6's "an authorship fact belongs on the module's
own declaration, checked at ingestion where the module is parsed anyway"
and the
§3 cited-symbol rung-drop row's "re-derived ... checked at ingestion, on the
module whose source carries the citation, from that module's own text, rather
than reconstructed corpus-wide by a second job"
— which that row explicitly asks
to land together rather than each rebuilding a walk.

What the wall measures, on the required path

Green in CI on this head, and identical to the local run:

required-ci: lane=witnesses phases_run=2 failed=0
required-ci: parse OK 3997 file(s) parse-clean
required-ci: declarations modules=3997 declared=76950 import_members=80221
             citations=1496 debt=42 in_fixtures=161 outside_index=134
             kernel_named=1948 lens_modules=71

No findings. This is stated first because the branch also carries a regen repair
below, and a reader who meets the red first will take it as a verdict on the wall
rather than on a projection the branch forgot to regenerate.

The three facts

  • Import-member claim integrity. Every import member is checked against the
    target module's declared surface. kernel_named=1944 counts the escape hatch
    rather than closing it: a member naming a kernel type resolves without the
    target declaring it, so the counter splits declared from undeclared — the
    order of the two predicates is what makes it a measurement rather than a
    restatement of the kernel set.
  • The cited-symbol wall. DeclarationRef citations are resolved against the
    cited module's own declarations at ingestion. debt=42 is a monotone debt
    contract over a closed, independently discovered universe, at identity grain,
    with a typed disposition per row — not a count copied from the current tree.
  • Module authorship. lens_modules=71, read from each module's own
    declarations, replacing the corpus-wide reconstruction §6 deleted.

Evidence, at the fixture boundary

cargo test -p v1-compiler --test declaration_index_integrity — 18 passed, 0
failed
. Every planted red carries a positive control asserted on the plant
before the guard's verdict is consulted, so a fixture that fails to plant what it
meant to plant fails as a fixture rather than passing as a guard.

Two construction rules the suite exists to hold, both learned from defects found
in this branch and both now asserted rather than observed:

  • A policy roster passed as a parameter defaults to the identity element of the
    judgment, never to the production value.
    A roster read from a module-scope
    constant makes the check's own RED unauthorable. Found first on the refusal
    side, where review 55817 caught it as 38 unplanted findings per fixture (1 passed; 8 failed, verified by execution); then found again on the
    suppression side, which is the quiet direction — a spurious suppression
    leaves every fixture green, including ones written to prove the arm works.
    Both rosters are now parameters.
  • Paired inverse arms must run in one report over one subject set. A single
    roster row carrying the wrong field name desynchronized both arms at once: the
    suppression missed and the staleness arm fired, about the same citation, in the
    same run. The row is corrected and the rule is now a test.

Generated-artifact repair

declaration_index.rs is a hand-written seed file. The branch registered it in
both authorities (seed_retention_frontier, stage0_crate_layout) but did not
regenerate the projection they feed, so the regen phase saw a committed mirror
the emitter does not produce and the two crate-layout witnesses went red. Fixed
by running the emitters, not by hand-matching the expected output — the files say
do not hand-edit, and a hand-written file that happens to equal what the emitter
would produce passes the gate while leaving the emitter unproven.

Three artifacts, two emitters. main_wet produces the .dag projection, the
bootstrap mirror and DESIGN.md; the regen emitter produces
src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs. Iterating main_wet
to a fixed point and hash-verifying its outputs could never surface the third —
a fixed point is only a fixed point of the operator you iterated, and the two
Rust mirrors sit in one directory under nearly the same name. Regen was repaired
by the documented recipe (install the candidate, rebuild from the installed
seed
, verify again), since the first pass runs a binary predating the change it
emits and can self-verify at divergence 0 for the wrong reason: pass 1
first_generation_equal=false, pass 2 first_generation_equal=true.

Declared residue

The wall covers symbol resolution, not claim truth: it establishes that a
cited symbol exists, never that the cited declaration says what the citing prose
claims it says. Trigger for that rung: a citation carrying a typed proposition
the cited declaration can be joined against, rather than a bare reference.

Admission

v1 is frozen-semantics / maintenance-active; the admission test is PURPOSE, and
this change serves the v2 self-host program by moving three checks off corpus
walks and onto ingestion. gunbc.declaration_index_seed_growth carries the
justification and the per-class refusal reasoning.

gunbc-ci-auto-heal added 3 commits August 25, 2026 19:08
…ted-symbol row, take main's updated emit-stage row
…f hiding it

v1.compiler.resolve get_exported_names appends every kernel_type_set key to
every module's export surface, so `import m { Int }` is admitted whatever `m`
declares. Measured against the installed compiler: a module whose whole body is
one fn returning Int, imported as `{ Int, String, Bool }`, compiles to 6 files
with 0 diagnostics -- readable because the same root with a bogus member refuses
with a located MissingExport.

The index mirrored that with a bare `continue`, which zeroes the deficit's
frequency by construction and is why nothing ever ranked it for repair. It
cannot be refused here: editing get_exported_names is NewLanguageBehavior and
the v1 freeze refuses it. So it is now counted as import_members_kernel_named
and printed beside every other denominator.

Kernel-named and declared are independent axes: over std.types, five of the
eight keys are genuinely declared (Bool, Secret, Json, Unit, Bytes) and three
are not (Int, String, Float). The predicate splits them by asking
import_surface_has first, and the fixture now asserts that behaviour rather
than leaving it to the ordering.

Also records why the authorship arm is not a second MandatoryTagRegion: that
door does not fire on the gunbc compile path, measured at 5 files 0 diagnostics
against a positive control. And answers the debt contract's four conditions,
including the two-directional typed disposition that separates 'repaired the
citation' from 'deleted a row to buy a green'.
…own red authorable (review 55817)

index_findings folded in citation_debt_findings, which joins the 38-row
production roster against whatever index it is handed. A fixture tree holds a
handful of probe.* modules, so all 38 rows were trivially absent and every
fixture received 38 CitationDebtRowStale findings it never planted. Measured:
1 passed, 8 failed -- every planted-red and every positive control in the file,
i.e. the whole of this change's DESIGN 4b evidence, was non-executing.

The repair is a denominator fix rather than a gate. The four index-derived arms
ask questions about the modules in front of them and are meaningful over any
tree; the debt roster is a fact about ONE corpus. So it moves to corpus_findings,
which the required run and the standalone sweep call, and index_findings keeps
the four. Gating the arm on a corpus-shape signal was the other available repair
and would have been a smuggled heuristic (DESIGN 4).

The arm's own red was also unauthorable, which the review did not say and which
is the finding underneath it: the roster was read from inside the function, so
no fixture could hand it one. The join now takes its roster as a parameter and
both directions of the contract are planted -- a row whose citation still
refuses is live and suppresses that citation's finding, a row whose citation
stopped refusing is spent and refuses by name -- plus a regression control
asserting the arm is absent from index_findings and present in corpus_findings.
@gunbai-bot

gunbai-bot Bot commented Aug 25, 2026

Copy link
Copy Markdown
Contributor Author

Adopted this PR — the session that opened it (bright-raven-296) is archived, so it was an orphan; the work item was redispatched to me. I closed #9219, which the dashboard had auto-opened on my adoption branch, so this stays the one PR.

review 55817 is correct, and I have the execution receipt

I did not take it on reading. I ran it:

test result: FAILED. 1 passed; 8 failed; 0 ignored

The one that passed was a counter assertion I had just added. Every one of this PR's original fixture-boundary tests failed — the planted reds and the positive controls alike. So the DESIGN §4b evidence this change rests on was authored and not executing, which is specification-without-execution in the form that survives review.

The mechanism is exactly as described: index_findings folded in citation_debt_findings, which joins the 38-row PRE_EXISTING_CITATION_DEBT roster against whatever index it is handed. A fixture tree holds a handful of probe.* modules, so all 38 rows are trivially absent and every fixture received 38 CitationDebtRowStale findings it never planted.

The repair, and why it is not the gate the review offered as an alternative

The review suggested either scoping debt-row liveness to a real-corpus run or gating citation_debt_findings on a corpus-shape signal. I took the first and deliberately not the second: a corpus-shape signal is a smuggled heuristic, and DESIGN §4 rules a heuristic never necessary in a closed system.

It is a denominator fix. The other four arms ask questions about the modules in front of them — does this import member exist, does this citation resolve, does this lens carry its authorship fact — so they are meaningful over any tree. The debt roster is a fact about one corpus, this repository's; joining it against another tree does not give a weaker answer, it answers a question nobody asked. So:

  • index_findings — the four index-derived arms, meaningful over any swept tree.
  • corpus_findings — those plus the debt arm. The required-CI phase and the standalone sweep call this; nothing else should.

The finding underneath the finding: the debt arm's own RED was unauthorable

The roster was a constant read from inside the function, so no fixture could ever hand it one. The debt contract — whose entire justification is that it refuses in both directions — had zero executing evidence that it refused in either. That is the §4b question asked one level down, and it had not been asked.

citation_debt_findings_against(index, roster) now takes the roster as a parameter, and both directions are planted at the fixture boundary:

  • a one-row roster whose citation still refuses → live, no finding, and that citation's own finding correctly suppressed;
  • the same roster with nothing citing it → spent, exactly one CitationDebtRowStale naming the row;
  • plus a regression control asserting the arm is absent from index_findings and present in corpus_findings, so this failure cannot return silently.

Two other things this push carries

The kernel-type escape was a silent, uncounted continue. v1.compiler.resolve get_exported_names appends every kernel_type_set key to every module's export surface, so import m { Int } is admitted whatever m declares. Measured against the installed compiler: a module whose whole body is one fn returning Int, imported as { Int, String, Bool }, compiles to 6 files with 0 diagnostics — readable because the same root with a bogus member refuses with a located MissingExport. The live specimen is std.types, which declares no Int, String or Float anywhere (they are string keys of that map) while modules across the corpus import them from it. I cannot refuse it here — editing get_exported_names is NewLanguageBehavior and the v1 freeze refuses it — but a bare continue zeroes the deficit's frequency by construction, so it is now counted as import_members_kernel_named and printed beside every other denominator. Kernel-named and declared are independent axes: over std.types five of the eight keys are genuinely declared (Bool, Secret, Json, Unit, Bytes) and three are not, and a fixture now asserts the counter splits them rather than leaving it to the predicate's conjunct order.

Why the authorship arm is not a second MandatoryTagRegion. v2.lens.mandatory_tag models this exact shape and its law says a violating module fails compilation; mandatory_tag_lens is enrolled in always_required_root_lenses. It does not fire: an extdeps. module with no anchor, matched by none of that region's three exemption lists, compiles to 5 files with 0 diagnostics. The v2 compile door is not on the gunbc compile path. Recorded as a note on the carrier, not filed against mandatory_tag, whose fold is fine — the point is that enrolling the arm there would be green by construction.

Still open, and I will not flip to ready before it

The re-run is in flight; I will post the green. I also owe one correction I am holding until I have a corpus measurement rather than an inference: the roster's doc comment says four rows at the end are not debt — the deleted census's planted controls, and enumerating all 38 rows finds no such row. Either the prose is stale or those citations are excluded some other way, and main's 2026-08-25 rehome moved those controls into v2.lens.cited_symbol_resolution, which this branch has now merged. I will fix it once, against the measurement.

Also merged main in — the branch base predated #9205, so cargo build --bins was failing on an unrelated TypeEnv field and my first run reported that break rather than these tests. That also clears the merge conflict the dashboard flagged.

— sent from royal-dove-799

gunbc-ci-auto-heal added 6 commits August 25, 2026 19:18
…rameters, defaulting empty

review 55817 found citation_debt_findings reading PRE_EXISTING_CITATION_DEBT
from module scope, which made its own RED unauthorable. Asking the same question
of the other four arms found a second instance, and a worse one:
cited_symbol_findings SUPPRESSED citations against the same constant. A spurious
refusal is loud; a spurious suppression is a citation the wall quietly declines
to judge, so that arm could have stopped enrolling an entire class with every
fixture green.

Both rosters are now parameters and both default to EMPTY rather than the
production constant, so index_findings judges every citation in whatever tree it
is handed and the roster is reachable from exactly one place, corpus_findings.

This also corrects an assertion I added in the previous commit: it claimed an
enrolled debt row suppresses its citation's finding while calling index_findings,
which reads the production roster and does not contain the fixture's row. It now
uses the parameterized form and pairs it with the empty-roster case, because
'suppressed' means nothing unless the same tree refuses when unenrolled.

The other two arms were checked and are not this class: import_member_findings
reads kernel_type_set, a language fact whose behaviour the fixture exercises with
a real kernel name, and lens_authorship_findings reads the decl name it checks
for. Both REDs are authorable.
…wo fixture bugs

SEAM: both rosters now enter from one place, corpus_findings, which makes the
WIRING a fact needing evidence -- unreachable-from-index_findings is proven by
construction, but reachable-from-corpus_findings was an assertion about a call
site. Pass an empty roster there and the suppression arm would be perfectly
evidenced at the fixture boundary and silently disabled where it matters.
corpus_findings_is_wired_to_the_production_suppression_roster declares a module
the production roster names and requires the same tree refused unenrolled and
suppressed enrolled.

RULE: a policy roster passed as a parameter defaults to the IDENTITY ELEMENT OF
THE JUDGMENT, never to the production value. Empty means judge everything, the
strictest answer, so a forgetful caller gets MORE refusals. Defaulting to the
production roster would give a forgetful caller silent suppression -- the defect
the parameter exists to close, reintroduced through the default.

FIXTURE BUGS, both mine, both found by execution rather than by reading:
- kernel_named_counter_splits_declared_from_undeclared authored its
  declares-nothing module with the wrong module header, so the import target did
  not exist and the claim was skipped as target-absent: counted 0, expected 1.
- the same fixture used a single-variant coproduct, which needs a leading pipe;
  it now uses a two-variant form that parses unambiguously.
- a_debt_row_whose_citation_still_refuses_is_live asserted suppression through
  index_findings, which reads no roster (fixed in the previous commit).
…rd's verdict

Two fixture defects in this file produced EXACTLY the observation a broken guard
produces:

  wrong module header      -> import target absent -> claim SKIPPED  -> no finding
  single-variant coproduct -> parse question       -> not admitted   -> no finding

A malformed plant and a broken guard are indistinguishable at the assertion, so
'no finding' was a three-way ambiguity -- fixture malformed, plant never reached,
guard broken -- and the repair pressure points at the production predicate. That
is how a correct guard nearly got 'fixed' to satisfy a bad fixture. It is the
not-applicable-versus-malformed conflation DESIGN names, arrived at from the
fixture side: SKIPPED and ADMITTED are different states and the assertion could
not see the difference.

plant / plant_declares / plant_import_target_resolves / plant_cites assert the
fixture is well-formed and that the claim REACHED the admit-or-refuse decision,
before any assertion about the verdict. Then the guard's answer is the only
remaining variable, and a failure says which of the three it was.
… wrong

MEASURED, one dispatch, 3993 files parse-clean:
  modules=3993 declared=76851 import_members=80076 citations=1496 debt=41
  in_fixtures=161 outside_index=134 kernel_named=1944 lens_modules=71

Two defects, both in the inherited roster, both found by running the wall rather
than by reading it.

1. THE PROSE WAS FALSE. The roster's doc comment claimed four rows at its end
were the deleted census's planted controls. Enumerating all 38 rows finds no such
row -- the rows were never added, only described -- and the corpus run duly
reported all four controls as ordinary refusals. They are deliberately false
citations, the discriminating evidence that a resolver refuses; a wall that
refuses them refuses the evidence for its own mechanism.

They are NOT enrolled as debt, because debt is a monotone contract that may only
shrink and these never retire (DESIGN 4b(4): an expecting-red probe that greens
flips to a permanent regression control). PLANTED_CONTROL_CITATIONS is a separate
carrier whose staleness arm is INVERTED: a debt row refuses when its citation
stops refusing; a control row refuses when its citation stops refusing too, but
because the control has lost its discriminating power. Same trigger, opposite
meaning, so two carriers rather than one with a flag.

The false claim is recorded as false rather than silently corrected. A stale
statement inside the carrier built to stop stale statements is the specimen.

2. ONE ROSTER ROW'S FIELD WAS WRONG, and it produced two CONTRADICTORY findings
about one citation in one run: extdeps.tcgplayer.store cites UpdateSkuPrice with
field NamedField { price }, while its roster row carried an empty field. So the
suppression missed it (reported CITED-DECLARATION-ABSENT) and the staleness arm
saw no live row for the empty-field identity (reported CITATION-DEBT-ROW-STALE).
One identity error, both arms wrong, in opposite directions.
…ion instead of noticing it

One roster row carrying an empty field where its citation carries
NamedField { price } made the two arms report CONTRADICTORY findings about ONE
citation in ONE run: the suppression arm called it unenrolled debt, the staleness
arm called its row spent. Both locally correct, both wrong.

NEITHER ARM CAN DETECT THAT ALONE -- each is right about its own half -- so the
only observable is the two answers being present together and disagreeing. That
was caught by a human reading two lines of a report, which is not a mechanism.

Two things follow, and neither is the row fix (already landed):

1. THE RULE, recorded on corpus_findings because that is where a future split
   would be decided: paired inverse arms must run in one report over one subject
   set. Splitting them across jobs, cadences or roster arguments does not weaken
   the pair, it destroys it, and the reasons for splitting are usually good ones
   about job granularity. Someone will propose it; the receipt is there for them.

2. THE WALL: a_roster_row_on_the_wrong_identity_desynchronizes_both_arms plants
   the exact identity mismatch and requires BOTH findings to appear, then repairs
   the row to the citation's real identity and requires NEITHER. That converts a
   lucky catch into something that fails by execution.
The plant-precondition and planted-control commits added helpers using index_get,
DeclarationIndex, ModuleDeclarationRecord and planted_control_findings_against,
and the edits meant to add them to the use block were plain string replaces
against a form cargo fmt had already reflowed. They matched nothing and said so
to nobody, so the test target stopped compiling: E0425 cannot find function
index_get, E0425 cannot find type DeclarationIndex, 7 errors.

Caught by execution, not by review: the corpus half of that dispatch ran and
printed its findings while the suite half never compiled, which is exactly the
shape where a run looks productive and one of its two questions was never asked.

Every other edit in this branch asserted its match count; the import edits did
not, which is the whole difference. Rewritten by matching the use block as a
unit with an assertion on the match count, and every symbol the file references
was checked as exported before committing.
@gunbai-bot

gunbai-bot Bot commented Aug 25, 2026

Copy link
Copy Markdown
Contributor Author

Receipt — both halves, one dispatch, one state (b5348bf)

=== SUITE ===
test result: ok. 18 passed; 0 failed; 0 ignored

=== CORPUS ===
v1_src_dag_parse: 3993 file(s) parse-clean; declarations modules=3993 declared=76851
  import_members=80076 citations=1496 debt=42 in_fixtures=161 outside_index=134
  kernel_named=1944 lens_modules=71

Zero findings over the live tree, exit 0. The corpus half reproduced identically across three separate runs before this one, so that measurement is settled independently of the suite.

What the wall found on its first execution, and what each fix actually was

Six findings. None were adjusted away; each cleared for a nameable reason.

Four planted controls were about to red the wall on the evidence for its own mechanism. v2.lens.cited_symbol_resolution authors citations that must not resolve — one per refusal arm. The roster's doc comment claimed four rows at its end covered them. Enumerating all 38 rows finds no such row: they were described, never added. So prose describing rows that do not exist produced a real, imminent, wrong red.

They are not enrolled as debt, and that refusal is the substance. PRE_EXISTING_CITATION_DEBT is a monotone contract that may only shrink; these never retire (DESIGN §4b(4) — an expecting-red probe that greens flips to a permanent regression control). Four permanent members would falsify its central claim about a tenth of its rows. PLANTED_CONTROL_CITATIONS is a separate carrier whose staleness arm is inverted: a debt row refuses when its citation stops refusing; a control row refuses on the same trigger because a control that resolves has lost its discriminating power. Same trigger, opposite meaning — two carriers rather than one with a flag, which would be the §3 fork. Both directions planted at the fixture boundary.

The false claim is recorded as false rather than silently corrected. A stale statement inside the carrier built to stop stale statements is the specimen.

One roster row on the wrong identity made the two arms contradict each other. extdeps.tcgplayer.store cites UpdateSkuPrice with field: NamedField { "price" }; its row carried an empty field. So the suppression arm reported the citation as unenrolled debt while the staleness arm reported its row as spent — contradictory answers about one citation in one run. Both arms locally correct. Both wrong. Neither can detect it alone, because each is right about its own half; the only observable is the two answers being present together and disagreeing. (debt 41→42 is exactly that citation joining the enrolled set.)

That produced a rule, recorded on corpus_findings where a future split would be decided:

Paired inverse arms must run in one report over one subject set. Splitting them across jobs, cadences or roster arguments does not weaken the pair, it destroys it — and the reasons for splitting are usually good ones about job granularity.

And a wall, so it is not a human noticing two lines: a_roster_row_on_the_wrong_identity_desynchronizes_both_arms plants the exact mismatch, requires both findings, then repairs the row and requires neither.

Numbers, stated at the grain they support

citations=1496 against the deleted lens's 390. That lens's population was five hand-listed carriers, so enrollment was opt-in and it could never have seen DESIGN's own worked example (gunbc.tailscale_acl_phase2_credential citing the orphan gunbc.auth.credentials). Reading citations off each module's own parsed source makes the population structural. The roster is deleted, and --required-cited-symbol with it, so the replacement has one route and not two.

kernel_named=1944 is the count of import-member claims whose target declares nothing — the true claims are already excluded, which is the split the counter had to prove it could make. Over std.types, five of the eight kernel_type_set keys are genuinely declared (Bool, Secret, Json, Unit, Bytes) and three are not (Int, String, Float), so import std.types { Bool } is true and { Int } is false. Asserted at the fixture boundary rather than left to the predicate's conjunct order.

IMPORT-MEMBER-ABSENT found 0 over 80,076 live members, and that zero is not evidence the arm works. The fixture suite is. The corpus is clean on that arm because MissingExport already enforces it inside compile closures — which is precisely why the arm's value is the orphan module no closure reaches, and why the discriminating pair holds the same false claim in a module the resolver sees and one it never gets asked about.

Corrections to my own work in this branch, since the receipts caught them

  • An assertion I added claimed an enrolled debt row suppresses its citation while calling index_findings, which reads no roster. False; it now uses the parameterized form paired with the empty-roster case, because "suppressed" means nothing unless the same tree refuses when unenrolled.
  • A fixture authored its declares-nothing module with the wrong module header, so the claim was skipped as target-absent and counted 0 where I asserted 1 — failing in the direction that looks like the mechanism is broken. Every planted red now asserts its own plant is well-formed before the guard's verdict, because a malformed plant and a broken guard produce the same observation.
  • Two edits meant to extend the test's use block were plain string replaces against a form cargo fmt had reflowed. They matched nothing, said nothing, and the target stopped compiling. Every other edit in this branch asserted its match count; those did not, and that was the entire difference.

— sent from royal-dove-799

gunbc-ci-auto-heal added 3 commits August 25, 2026 19:50
… by the required run

The seed-growth carrier said the corpus-walk half of the DESIGN triggers is
discharged and 'decl_facts is no longer consulted by any required check'. The
first half is right for the three questions this change answers; the second half
is false and I wrote it without checking.

decl_facts has live .dag consumers, and several are floor-discovered witness
modules -- decl_facts_reflection_witness_test, record_construction_census_witness_test,
floor_expected_red_coherence_witness_test among them -- so the corpus walk still
executes inside the required floor for their sake. What IS true is narrower and
still worth the change: the citation wall no longer reaches decl_facts at all,
because --required-cited-symbol and its lens are off the required path entirely,
and the three integrity questions now come from one construction instead of three
walks. Retiring the remaining consumers is a separate cut.

Caught by re-reading the request against the carrier rather than by a checker,
which is the same failure this PR exists to make mechanical: a claim about a
population nobody had counted.
…tion, not claim truth

A citation wall answers 'does this name exist'. Nothing in this construction
answers 'is this count right', and the two halves are independent. Named as
declared residue so the next reader finds the gap instead of assuming the wall
covers it.

The distinction is measured, not hypothetical -- twice on this branch, both times
inside typed carriers, both times a population claim nobody had counted:

  the debt roster's doc comment  'four rows at the end are the planted controls'
                                 -> the rows were never added, only described
  this carrier, same author      'decl_facts is no longer consulted by any
                                 required check' -> three live floor-discovered
                                 consumers

Why the wall cannot reach either: decl_facts is a REAL SYMBOL that RESOLVES. The
sentence claiming nothing consults it would pass a cited-symbol census cleanly,
because every name in it is true and only the QUANTIFIER is false. DESIGN 4c
states the general form -- prose is unfalsifiable by construction, which is why a
count belongs in a typed carrier and not in a sentence.

Rung stated honestly: one was caught by running the wall, the other by re-reading
the carrier before merge. The second is review diligence, so the class sits at
MITIGATABLE and nothing here climbs it. NEXT-RUNG TRIGGER: a quantified claim in
a carrier is DERIVED rather than AUTHORED, so the sentence cannot disagree with
the corpus because it is not a sentence.
…hen the dead lens is cut

Review 55841 asked to confirm v2.lens.cited_symbol_resolution is retired rather
than left as dead parallel representation. Measured rather than asserted, because
'it is dead' is the claim shape this branch already got wrong once: of the 27
symbols unique to that lens, the only references outside it are one prose row in
gunbc.roster_registry, two prose mentions in fast witnesses (a String note and a
// comment), and nine real uses in the long/ witness, which is declined before the
fold and never executes. NO EXECUTING witness calls any function it declares.

So it is dead, not competing. But this change does add a second copy of the four
planted-control identities, and the duplication needed a named terminus rather
than an assurance. Recorded: when the lens is cut, these identities are the
SURVIVING authority -- the deletion removes the dead copy, never the evidence.
DESIGN 4b(4) keeps a discriminating control enrolled when its machinery goes, and
a cut that swept the lens's controls into the funeral would erase the four probes
that prove this wall's refusal arms are real.
@gunbai-bot

gunbai-bot Bot commented Aug 25, 2026 •

Copy link
Copy Markdown
Contributor Author

Follow-up from review 55841: confirming the old lens is retired, by measurement

The review asked to confirm v2.lens.cited_symbol_resolution is retired rather than left as dead parallel-representation. I counted rather than repeated the carrier's word, because "it is dead" is the exact claim shape this branch already got wrong once — the carrier said decl_facts is no longer consulted by any required check and that was false.

Method matters here: grepping imports is unsound in this substrate, since a name absent from every import list still resolves by global uniqueness. So the census is over the 27 symbols unique to that lens (excluding shared names like construction_justification, which every lens declares and which produces a false positive in 20 files).

Result — every reference outside the lens, enumerated:

site what it is
gunbc.roster_registry one prose row (cited_symbol_roster_registry_widening_note)
test.claim.cited_symbol_resolution_witness_test prose only — a data … String note
test.claim.doc_reachability_witness_test prose only — a // comment
test.claim.long.cited_symbol_resolution_witness_test 9 real uses — but a long/ home, declined before the fold, never executes

Stripping comment lines and String prose rows from the two fast witnesses and asking which lens functions their executable code calls: NONE, both files. So no executing witness reaches the lens, its resolver is invoked by nothing, and §3's attractor argument does not bite — it is dead, not competing.

What the review's question surfaced that the carrier did not say

This PR does add a second representation of four identities the lens also carries: its cited_symbol_planted_controls and my PLANTED_CONTROL_CITATIONS name the same four controls. That duplication is real, and it needed a named terminus rather than an assurance, so it now has one in the code:

When the lens is cut, these four identities are the surviving authority. The deletion removes the dead copy, never the evidence.

That is worth stating explicitly because the failure mode is live: DESIGN §4b(4) keeps a discriminating control enrolled when its machinery goes, and a cut that swept the lens's controls into the funeral alongside it would erase the four probes that prove this wall's refusal arms are real — the same probes whose absence from the debt roster was about to red this wall on its first execution.

The lens's own deletion stays the separate cut the carrier already declares (sixteen witnesses, the lens registry, the deferral freeze, the doc-graph population). Nothing here changes that boundary; it just makes the cut safe to perform.

— sent from royal-dove-799

(Edited: two literals in the sentence above were eaten by shell command substitution when this comment was posted — backticked tokens inside a double-quoted argument. The measurement is unchanged; only that sentence's wording was damaged.)

gunbc-ci-auto-heal and others added 8 commits August 25, 2026 21:52
…s move

declaration_index.rs is a hand-written seed file. The branch registered it in
both authorities -- seed_retention_frontier and stage0_crate_layout -- and never
regenerated the projection those authorities feed, so the regen phase saw a
committed mirror the emitter does not produce ("committed mirror is no longer
emitted") and the two crate-layout witnesses that join frontier to generated
filenames both went red. One missing regeneration, three CI failures.

DESIGN.md is the third projection and was invisible from the failure list: this
branch edits gunbc.design_document (the fired §6 construction-justification
trigger, the retired cited-symbol row), so its projection was stale too and would
have been the next cycle's red from a different file.

Produced by running the emitter to a FIXED POINT -- dag/tools/generated_artifact_gate.dag
main_wet, looped until git status stopped changing, which took two rounds -- not
by hand-matching the expected output. The files say do not hand-edit, and a
hand-written file that happens to equal what the emitter would produce passes the
gate while leaving the emitter unproven.

Every installed byte verified against the emitter's own sha256 on the runner
before any confirming run:

  261489671103b4d8c1cce69934cbaaf23fd401a379e0de0eb941a42b48ca92bc  dag/gunbc/stage0_crate_layout_generated.dag
  698a52094e48cdf3964a5c2a5df4266a5892de49f4f0516521beaf041fef2d79  src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs
  8d075c7cd37af217326c689bbbcefbbe1c3024c7b53cad5f93eec75e91cc652f  DESIGN.md

A second dispatch re-emitted over the installed copies and reproduced them
unchanged, which is the independent half of that check.

The declaration index itself was already green on the required path at the
previous head and is untouched here: modules=3993 declared=76852 citations=1496
debt=42 kernel_named=1944 lens_modules=71, no findings.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three conflicts, resolved on three different principles, plus one near-miss worth
recording because the merge produced it rather than any author.

src/v1/stage0/src/bin/claim_executor.rs, two hunks with an EMPTY ours side. Main
added lane-based phase selection next to lines this branch had DELETED -- the
--required-cited-symbol mode and its parse arm. Git renders "ours deleted, theirs
touched nearby" identically to "theirs added something new", so taking theirs
would have RESTORED the flag this change exists to remove, producing exactly the
two-routes state the seed-growth carrier claims is gone: a clean compile, a green
wall, and the deleted census quietly back. Resolved by keeping main's new
RequiredCiLane additions and keeping the deletion; required_cited_symbol_mode now
has zero occurrences in the tree.

Same file, third hunk, structural. Main wrapped each phase in
required_ci_phase_selected(RequiredCiPhase::Parse, lane); this branch changed
run_dag_parse_sweep to return a struct carrying the index rather than a count.
Union: this branch's body nested inside main's conditional, so the declaration
checks ride the parse phase wherever the lane routes it.

THE NEAR-MISS. That union initially dropped one line -- the Err arm's
phase_failures.push(format!("parse ({} error(s))", errors.len())), which sat on
main's side of the conflict region while the eprintln! sat on ours. Had the
braces balanced, the result would have compiled and printed "parse FAIL" WITHOUT
FAILING THE PHASE: a fail-open arm authored by a three-way merge rather than by
anyone. It did not balance, so the pre-commit hook refused, which is the only
reason it was caught. Restored and verified.

DESIGN.md, a generated projection. The merge driver refused rather than picking a
side, correctly: both sides changed it since the merge base, so neither side's
bytes are the projection of the merged authorities. Regenerated from the merged
carrier (dag/gunbc/design_document.dag auto-merged clean, which is what makes
that safe) and verified byte-grain against the emitter's own sha256 on the
runner:

  ba373e57eb6e2e772cfe732908b31952a088134cd20eb51dec1e07d45688f6a1  DESIGN.md

The two crate-layout projections re-emitted UNCHANGED across this merge
(261489671103b4d8..., 698a52094e48cdf3...), so the fixed point installed in the
previous commit still holds against main's new content. main_wet ran twice in one
dispatch to check that rather than assume it.

VERIFIED ON THE MERGED TREE, and named at the right subject: an earlier dispatch
reported `cargo build --bin gunbc` Finished, which does not compile this file at
all and established nothing about the hand-merged code.

  cargo build --release -p v1-compiler --bin claim_executor   Finished, 5m21s
  cargo test -p v1-compiler --test declaration_index_integrity  18 passed; 0 failed

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…er (review 55899)

dag/gunbc/declaration_index_seed_growth.dag cited
v1_compiler.declaration_index citation_is_pre_existing_debt. That predicate was
RENAMED to citation_in_roster earlier on this branch, by the repair that made the
debt roster a parameter defaulted to the identity element. The code and every
caller moved; the roster row did not. So the carrier declaring this PR's
hand-Rust obligation cited a symbol this PR had deleted -- the exact DESIGN §3
stale-citation class this PR exists to close, inside the PR's own authority.

WHY THE WALL DID NOT REFUSE IT. The wall resolves a citation against the index,
and the index is built from swept .dag modules. v1_compiler is a hand-Rust
namespace root no swept module declares, so citation_is_outside_index COUNTS it
rather than refusing -- exactly as the carrier's disclosed boundary says. What
that disclosure did not say, and now does: the seed-growth carriers are precisely
the rosters that name hand-Rust items, so they are the one population where a
rename in the same commit silently rots its own citation. The wall's coverage and
the rosters that most need covering are disjoint.

CHECKED AT CLASS GRAIN, NOT AT THE REPORTED INSTANCE. All 55 roster rows resolved
against a definition in the five hand-Rust files the carrier enumerates: 54
resolved, 1 did not -- the row review found. The "+55, all enumerated" claim was
therefore true of the COUNT while false of one row's CONTENT, which patching only
the reported line would have left unmeasured.

Recorded as a specimen row rather than silently corrected -- the same discipline
the false-quantifier row already applies to its two specimens -- with its
next-rung trigger (resolve hand-Rust citations against an index of hand-Rust
declarations, strictly larger than this PR and not attempted here) and an honest
rung: mitigatable, review diligence.

VERIFIED: v1_src_dag_parse over the merged tree, 3997 file(s) parse-clean, zero
findings, declarations modules=3997 declared=76950 import_members=80221
citations=1496 debt=42 in_fixtures=161 outside_index=134 kernel_named=1948
lens_modules=71.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…not produce

CI: required-ci: regen FAIL generated surface drift:
gunbc_stage0_crate_layout_generated.rs

ONE AUTHORITY, TWO EMITTERS, AND I HAD ONLY RUN ONE. Editing
dag/gunbc/stage0_crate_layout_generated.dag moves THREE artifacts, produced by
two different emitters:

  main_wet (dag/tools/generated_artifact_gate.dag)
    dag/gunbc/stage0_crate_layout_generated.dag
    src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs
    DESIGN.md

  regen (claim_executor --required-regen)
    src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs

The previous commit iterated main_wet to a FIXED POINT and hash-verified every
byte of its outputs. That was correct and could never have surfaced this file,
because main_wet does not produce it. A FIXED POINT IS ONLY A FIXED POINT OF THE
OPERATOR YOU ITERATED. The two Rust mirrors sit in the same directory with nearly
the same name -- bootstrap_stage0_... and gunbc_stage0_..., one per emitter -- so
the missed one reads as a duplicate of the checked one.

REPRODUCED RATHER THAN INFERRED, which mattered: main at efc880a ALSO fails
witnesses.yml in the BUILD lane with floor green, so every surface signal said
inherited. Running the exact lane
(claim_executor --required-ci --required-lane build) named a file that exists
only on this branch. main's build job died before its steps reported a
conclusion at all -- an infrastructure death wearing a lane name, which could not
have produced this symptom. Two reds, one lane name, unrelated causes.

REPAIRED BY THE DOCUMENTED RECIPE, not one pass, because the first pass runs a
binary that PREDATES the change it emits and can self-verify at divergence 0 for
the wrong reason:

  pass 1  first_generation_equal=false  FAIL generated surface drift
  install target/stage0-regen-candidate/src/gunbc_stage0_crate_layout_generated.rs
  rebuild from the installed seed        Finished in 4m12s
  pass 2  first_generation_equal=true    no failure

Installed bytes verified against the runner's sha256:

  e70d37012c0ee094583ed0dc3c1098cb55f06008e90867ba1a894059980e6a6a

The diff is one insertion, "declaration_index.rs".to_string(), which confirms the
diagnosis rather than merely clearing the gate.

THE FLOOR LANE IS ALREADY GREEN ON THE PARENT COMMIT (run 32907180281):
phases_run=2 failed=0, parse OK 3997 file(s) parse-clean, declarations
modules=3997 declared=76950 citations=1496 debt=42 kernel_named=1948
lens_modules=71 -- so the two crate-layout witnesses that failed on ea31e92
now pass, and the declaration index matches the runner measurement digit for
digit. This commit closes the last of the three original failures.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI on 45270ab: both lanes died at "Build the witness fold" with the lane steps
SKIPPED, so nothing was checked -- one compile failure reported three times, not
three failures.

  error: unused imports: `make_eval_context`, `resolve_entry_graph_shared`, and `run_value`
  error: unused imports: `ExecutionMode`, `InterpContext`, and `Value`
  error: could not compile `v1-compiler` (bin "claim_executor") due to 2 previous errors

NEITHER BRANCH HAS THIS DEFECT ALONE. main's #9228 ("Delete the plan/walk surface
nothing could reach", claim_executor 21,366 -> 11,508) removed the last callers
of all six; this branch kept the import list. The imports go dead only in the
merge, and CI evaluates the merge ref, which is why the head built clean here and
failed there. Every surviving use is fully qualified
(v1_compiler::cli_run::make_eval_context), and `Value` is re-imported locally at
its one use site, so the removals are safe.

TWO DEFECTS IN MY OWN INSTRUMENT, named because both fail toward a green:

1. CI builds with -D warnings and the workflow never says so --
   actions-rust-lang/setup-rust-toolchain@v1.16.0 sets RUSTFLAGS: -D warnings by
   default. Local dispatches built without it, so unused imports were warnings
   here and errors there. Reproduced with RUSTFLAGS forwarded: BUILD-RC=0.

2. My build checks grepped `^error`, but cargo emits ANSI escapes, so the real
   line is \e[1m\e[91merror and never matches at column 0. Every "no errors" I
   reported from those dispatches read a filter that COULD NOT MATCH AN ERROR.
   That is the worse of the two: it would have hidden any compile failure, not
   just this class.

VERIFIED ON THE MERGED TREE, under CI's own strictness:
  cargo build --release --bin claim_executor --bin gunbc, RUSTFLAGS=-D warnings  rc=0
  claim_executor --required-regen   first_generation_equal=true, no drift
  main_wet x2, all three projections byte-IDENTICAL before and after:
    ba373e57...  DESIGN.md
    26148967...  dag/gunbc/stage0_crate_layout_generated.dag
    698a5209...  src/v1/stage0/src/bootstrap_stage0_crate_layout_generated.rs
  so the text-merged DESIGN.md IS the projection of the merged authorities and
  owes no regeneration.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ation grain (review 55939)

Both citation arms skipped every citation in a module module_is_fixture_carrier
answered true for. The justification was real and still is -- a witness proving
the resolver refuses an absent symbol has to AUTHOR an absent symbol, so its
false citation is its evidence rather than its defect. The defect was that the
EXEMPTION WAS KEYED ON THE MODULE while the justification is a property of the
CITATION.

WHAT SETTLED IT WAS THE MEASUREMENT, NOT THE ARGUMENT. Of 161 citations authored
inside fixture carriers, 128 RESOLVE: ordinary citations of real authorities that
happen to live in a test module. The skip was shielding 128 real citations to
protect 33 sites, and reporting the rest as in_fixtures did not restore
integrity. A counted hole is still a hole.

THE HOLE WAS OCCUPIED, which is what separates a defect from a disclosed
boundary. Two enrolled identities are ordinary staleness with nothing to do with
fixture intent:
  - dag.test.claim.witness_purpose_taxonomy_witness -- a dag.-prefixed module
    path no module declares; the real module is test.claim.*. A plain typo.
  - std.disposition Disposition field marker -- a real authority and a real
    declaration with an absent field, cited twice.

THE REPAIR. Both arms now judge fixture carriers, and
FIXTURE_CARRIER_CITATION_EXEMPTIONS enumerates 31 identities at (module,
declaration, field) grain. It is NOT a debt contract and does not claim to be:
§5's condition 3 wants a terminal state of empty and this one's is not -- a
planted control such as NoSuchDecl_G1_RED is permanent by design. What it shares
with the debt roster is what makes either safe rather than a suppression list:
MONOTONE, and REFUSES WHEN SPENT through the same inverse arm. Also fixed a
diagnostic that would have named PRE_EXISTING_CITATION_DEBT for a row held by a
different roster -- a spent-row message naming the wrong list sends the reader to
a file that does not contain the row.

HOW THE ROWS WERE OBTAINED, because the first attempt was wrong AND THE MECHANISM
CAUGHT ITS AUTHOR. Extracting identities by parsing rendered diagnostics silently
dropped the FIELD -- a CitedDeclarationAbsent message never prints one -- so rows
for citations carrying a NamedField whose DECLARATION is absent matched nothing.
The corpus run then reported the same citation as BOTH refusing AND its row as
spent: the paired-inverse-arm desynchronization this module documents and tests
for, firing on me, inside one run. Rows are now derived from the index, from the
same CitedSymbol values the matcher compares. Five further refusing identities
are deliberately excluded -- already enrolled in PRE_EXISTING_CITATION_DEBT or
PLANTED_CONTROL_CITATIONS, and a second row for one citation is duplicate
authority with a double stale-arm report.

RUNG: unchanged at mechanically preventable. This is a WIDENING of the enrolled
population, not a climb -- 128 citations that were never judged now are.

VERIFIED, under CI's own strictness (RUSTFLAGS=-D warnings):
  cargo test --test declaration_index_integrity   21 passed; 0 failed
  v1_src_dag_parse over the corpus                rc=0, ZERO findings
    3997 file(s) parse-clean; modules=3997 declared=76981 import_members=80186
    citations=1493 debt=42 in_fixtures=161 outside_index=134 kernel_named=1947
    lens_modules=71

Three new fixture-boundary tests, each asserting its plant before the guard's
verdict: a refusing citation inside a carrier is judged; exempting one citation
leaves its sibling in the same module refusing; an exemption over a resolving
citation refuses as spent and names its roster.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…boundary

The fixture roster enrolls 31 identities. Two are decidable by inspection and are
named in the carrier prose as ordinary staleness. THE OTHER 29 ARE NOT
CLASSIFIED, and leaving that as prose would let them read as settled -- which is
exactly where a real defect sits unseen, demonstrated rather than hypothesised,
because two were found sitting there.

Not deciding them is still right: deciding what another author MEANT across 29
rows is the judgement §5 warns turns a stale citation into a confidently wrong
one. The repair is to DECLARE the stall rather than to resolve it, which is the
difference between a boundary disclosed and one merely not crossed.

declaration_index_fixture_exemption_classification_stall, a GuaranteeStall:

  current      Mitigatable
  ceiling      MechanicallyPreventable      (below ceiling, so it reads as a
                                             stall rather than a class that
                                             already arrived)
  blocker      AwaitsOneGrounding           NOT ClimbableButUnbuilt: what is
                                             missing is a DECIDABLE CRITERION,
                                             not effort. Nothing distinguishes a
                                             citation its author meant to refuse
                                             from one that rotted; the
                                             distinction lives in authoring
                                             intent, which no Accepted program
                                             can read.
  population   BoundedPopulation, 29 members at identity grain -- genuinely
               bounded, so UncountedNotEnumerable would be the
               empty-observation narrow.
  trigger      a witness declares each citation it plants to refuse as a typed
               row beside the citation, at which point the deliberate half is
               DERIVED, this roster shrinks to the genuinely stale remainder,
               and that remainder becomes ordinary debt with a terminal state of
               empty.

The 29 is derived by subtracting the two named specimens from the 31, not
asserted, so the number in the prose and the number in the row are one fact.

VERIFIED: 3997 file(s) parse-clean, rc=0, ZERO findings. The new
gunbc.guarantee_rung_drop import members resolve -- import_members 80186 -> 80191
with no IMPORT-MEMBER-ABSENT finding, which is this change's own wall checking
this change's own edit.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot merged commit da11de6 into main Aug 26, 2026
3 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/bright-raven-296 branch August 26, 2026 02:41
gunbai-bot Bot pushed a commit that referenced this pull request Aug 26, 2026
…enty-seven witnesses that were never its

DESIGN authorised this cut and got its population wrong, which is the finding rather than
a footnote. The row read "v2.lens.cited_symbol_resolution and its sixteen witnesses are not
deleted -- they are unreachable from any required check and are dead rather than competing".
Both halves of that population claim are false, and this change corrects the row in the same
diff that falsifies it.

SIXTEEN WAS THE COUNT AT #7707, when the lens landed. The file grew twice after
(#8673 enrolled roster_registry, #8775 the two instance-gap carriers) and held 27 `test fn`
identities. `gunbc.ci_layer_roots` said "eighteen". Three numbers, three snapshots of a
growing file, none of them current -- the transcribed-measurement class the standing rule
already names. The replacement rows name their subject and no number.

AND "DEAD" WAS TRUE OF THE LENS AND FALSE OF A THIRD OF ITS WITNESSES. Measured against the
seven symbols that file imported FROM the lens, 6 of the 27 touch one. The other 21 do not.
"The lens and its witnesses" was never one population, and the three-way split is:

  6  LENS-BOUND -- die with it. The census-green claim, the three planted-control rows, the
     enrolled-population exemption identity, the ambiguous control. `declaration_index`
     re-derives this machinery as PLANTED_CONTROL_CITATIONS plus PlantedControlNoLongerRefuses.

  6  RESOLVER-BOUND -- MOVED, not deleted, to test.claim.long.decl_ref_resolution_witness_test.
     They call `resolve_declaration_ref`, which lives in `v2.std.decl_ref_resolution` -- a
     module that SURVIVES with four other consumers -- and they are the only rows in the tree
     that execute its five-arm refusal. Deleting them because they sat in a file named for
     the lens would be the §4b(4) failure exactly: a climb deletes the redundant PRODUCTION
     machinery, never the discriminating RED and positive control.

  15 CARRIER-BOUND -- MOVED to test.claim.long.carrier_reference_integrity_witness_test.
     Population and projection claims about the four carriers that PROJECT DeclarationRefs.
     Their resolution half is subsumed; their population half is subsumed by nothing.

SUBSUMPTION IS SCOPED, not general: `declaration_index` extracts TYPED-LITERAL citations --
DeclarationRef record literals and the decl_ref/decl_field_ref constructors -- and reports
computed reference fields as a coverage boundary. A prose reference inside a String is
covered by nothing, before or after, and this change does not claim otherwise.

THE PER-PR WITNESS IS RENAMED, NOT DELETED. test.claim.cited_symbol_resolution_witness_test
never imported the lens; its one claim is a three-term bucket partition over
gunbc.doc_graph_roots. Two readers independently concluded from its NAME that the resolution
law was enforced per-PR -- it was not, a bucket identity was -- and after this cut it would
have been the only cited-symbol-named thing left in the tree, reading as the law's residue.
It is now test.claim.doc_graph_reference_partition_witness_test. Same borrowed-authority
shape as #9252's fixture rehome, one layer up: there the home was borrowed, here the name.

WHAT THE WALL ITSELF NAMED, because this was cut delete-first and the census is the deletion.
The first corpus run after the cut reported six refusals: two IMPORT-MEMBER-ABSENT for a
`CitedSymbolResolution` lens-id the registry no longer declares, and four
PLANTED-CONTROL-RESOLVES for the exact rows #9211 declared as this cut's residue ("they
delete with the lens, not before it"). Every one predicted, none discovered by reading.

AND ONE GAP THE ROSTER DELETION WOULD HAVE OPENED, which is why those four rows are not
simply removed. Each named one refusal arm of the cited-symbol wall. Three of the four arms
already had controlled fixtures in tests/declaration_index_integrity.rs. THE FOURTH DID NOT:
measured, the string `CitedFieldAbsent` did not occur in that file at all, so its only
evidence anywhere was the planted row I was deleting. Deleting it would have left a refusal
arm with nothing executing against it -- §4b(4) again, one level up from where I first hit it.
`citation_to_an_absent_field_is_refused_and_a_present_field_is_not` is authored here, with
its positive control, and a controlled fixture is the stronger oracle anyway (§5): the
planted row only ever asserted that one hand-authored citation still refuses.

PLANTED_CONTROL_CITATIONS is left EMPTY rather than deleted. Mechanism reachable, join
reachable, occupancy zero -- a healthy guard being quiet, not a dead one.

EVIDENCE, by execution (remote, release binaries):
                              before        after
  parse-clean files           4012          4011      the lens module
  modules                     4012          4011
  citations                   1470          1466      the lens's four planted citations
  lens_modules                71            70
  debt                        42            42        UNCHANGED
  corpus findings             0             0
  declaration_index_integrity 21 passed     22 passed the new field-absent pair

THE DEBT COUNTS RECONCILE, and the brief's "46" is none of them. 38 = roster rows, counted.
46 = citation SITES at the time the roster's doc comment was written. 42 = citations
currently suppressed by a row, the live measurement. debt is 42 before and after, and a row
that stopped reproducing refuses as CitationDebtRowStale -- none did, which is the executable
form of "the defects are still found".

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 26, 2026
…ction, cli_invoke builders, walk_plan_stage fixture family) (#9286)

* Delete the .dag residue of the plan/walk CLI surface, and give the scope-disposition witness a fixture home it owns

#9228 deleted claim_executor's plan/walk surface and named its .dag residue rather
than sweeping it. This is that cut, plus one repair the census surfaced.

WHAT WENT, AT THE ROOT:

  PlanFunction and the plan argv builders. The coproduct modelled a closed roster of
  --plan-function targets; the flag no longer parses and the entry every variant named
  (src/v2/workflow/ci_floor_plan.dag) was deleted by the 2026-08-15 floor cut. Gone with
  it: claim_executor_run_plan_transport_argv, claim_executor_run_plan_shell, the
  notice-title normalizer and shell suffix that existed only to feed them,
  claim_executor.Executor.RunPlan, ci_spec's scheduler_invoke/scheduler_invoke_with/
  floor_plan_entry/floor_plan_function/plan_artifact_plan_function, and
  gunbc_ci_floor_only_script.

  The --verify-build-artifacts half is UNTOUCHED and deliberately so: it is a live mode
  (fleet-converge.yml), so claim_executor_verify_artifacts_shell, claim_executor_bin_shell,
  release_bin_shell_path and SourceRootShellStyle all stay. cli_invoke's dissolve trigger is
  NARROWED to name only what survives rather than deleted, since the shell-vs-argv fork it
  records is still open for that one spelling.

  gunbc_ci_run_script emitted the release build AND a claim_executor --plan-entry line. The
  second half is deleted, not repointed at --required-ci: witnesses.yml already invokes that,
  and a second route to it here is the parallel authority the floor cut removed.

  The walk_plan_stage fixture family, whole: 11 fixture modules, the 379-line #[ignore]
  harness, its scaffold row and witness, and the seed_retention_frontier retained_test_harness
  row. Their sole driver was the plan.dag recipes #9228 deleted.

  v2.workflow.required_floor fixture_home_prefixes() and RequiredFloorDisposition::
  DeclinedFixtureMember, with the cli_run.rs decode, branch, counter and TSV column. That
  arm's roster was one prefix and the family above was its entire population; its own header
  said "DISSOLVES when the fixture stops authoring test fns", and this is that condition.
  Coordinated with sleek-carp-211, who is modelling the enum in #9246 and asked for both
  sides deleted here.

  The pre-push witness-corpus gate. Not on the brief, found by the flag census:
  pre_push.rs built claim_executor and invoked --plan-entry/--plan-function on the deleted
  floor plan entry. Its EMISSION died 2026-07-25 when the operator made the hook fmt-only;
  its INVOCATION died 2026-08-25 with the flags. Two witness rows asserting "a .dag push arms
  a gate" are deleted rather than weakened -- measured against the roster, the corpus binding
  was the only thing making them true, so they were green against the plan and false about the
  hook anyone runs.

THE REPAIR THE CENSUS SURFACED (tools.dag_compile_clean_scope):

  Three walk_plan_stage files were pinned as the roster and pool of the SCOPE DISPOSITION
  witness, which has nothing to do with plan/walk. Its own note records that these same
  specimens already moved once for exactly this reason -- from test/fixture/floor_skip, which
  died with affected-set selection. This would have been the third home.

  They are rehomed to src/v2/test/fixture/compile_clean_scope/, a home this witness owns:
  three modules, no test fn, no effects, one consumer. No discovery exclusion is needed
  because there is nothing to discover, which is a stronger construction than the dir-grain
  exclusion the old home required.

  AND THE PROPERTY THE NOTE CLAIMED IS NOW ASSERTED. The expectation was
  ExpectScopedContaining -- MEMBERSHIP -- so a selector returning the whole roster satisfied
  every row and the "strict-subset proof" the note describes was checked by nothing.
  ExpectScopedExactly compares the selected list to the expected list.

EVIDENCE, by execution on a release gunbc (remote, one dispatch):
  control    witness_touched_path_dispositions_hold -> true
  mutation   give scope_isolated an import edge to scope_shared -> false
  The mutation is exactly the strict-subset violation; the old assertion could not see it.

Rust: cargo check -p v1-compiler --bins clean, fmt clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Repair the scope-disposition witness's per-PR half, which the floor caught

dag/test/claim/dag_compile_clean_scope_witness_test.dag imports ExpectScopedContaining
and pins the disposition row count. Both moved with the rehoming and I checked only the
long-lane witness, so strict preparation refused with a name-resolution error before any
site ran. Fixed at both ends: the import drops the deleted variant (ExpectSkip went with
it -- it was imported and never used), and the pin goes 7 -> 8, which is the roster
growing by one row because the strict-subset proof needs three specimens where the old
home carried two.

The pin doing its job here is the argument for keeping it: a count that had to be updated
by hand is exactly what stopped this rehoming from silently shipping a roster of a
different size than the one the note describes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Delete the `gunbc ci` verb rather than leave a command named ci that greens without running CI

REQUEST_CHANGES from codex/gpt-5.6-sol (review 56054), and the finding is correct.

WHAT I BROKE. This branch narrowed gunbc_ci_run_script to ci_release_build_script()
alone, because its other half emitted a `claim_executor --plan-entry` line naming an
entry the floor cut deleted. But `gunbc ci` is a real CLI subcommand, so what survived
was a callable verb that builds the release binaries, verifies the artifacts, and exits
0 -- under a name that says it ran CI. That is fail-open semantic dilution: the failure
mode is not a wrong answer, it is a CORRECT answer to a much smaller question, reported
under the name of the larger one. §5's absorbing-fallback rule is about a failure arm
that widens; this is its mirror at the success arm, a green that narrowed.

WHY DELETED AND NOT REBOUND. Binding the verb to `claim_executor --required-ci` was the
reviewer's other option and I am not taking it, on the grounds this branch already
argued in the commit that caused the defect: witnesses.yml invokes --required-ci, and a
second route to it is the parallel authority the floor cut removed. The verb also has no
distinct job left -- "build the release binaries and verify the artifacts" already has a
name, ci_release_build_script, and fleet-converge.yml already calls it. So the verb is
not an authority that lost its body; it is a name with nothing left to denote.

THE CENSUS, cut at the root and followed where it led:
  dag/tools/gunbc_ci.dag                     the entry module, deleted
  main.rs Commands::Ci + its arm             the CLI verb
  gunbc.cli_dispatch_surface "ci" row        the modeled CLI surface
  gunbc_cli_dispatch_surface.rs              its generated mirror
  v2.workflow.ci_release_build_emit          gunbc_ci_run_script, the wrapper
  std.emit_on_demand gunbc_ci_emission_surface   the wet-surface row naming tools.gunbc_ci main
  emit_on_demand_kernel_witness_test         its enrollment assertion
  wall_residue_live_test residue_gunbc_ci_clean  a test fn whose subject was the deleted file

ci_release_build_script itself is UNTOUCHED and still has three consumers
(ci_materialization, fleet_workflow_steps, fleet-converge.yml). Only the wrapper goes.

EVIDENCE, build lane on this tree (remote, one dispatch):
  required-ci: lane=build phases_run=2 failed=0
  regen first_generation_equal=true    -- the mirror edit is byte-equal to the emitter's
                                          own output, established by the gate rather than
                                          by my reading of the diff
  v2-emission blocking=0, census 3792 -> 3791, the one deleted module

The emitter-gap witness still holds: gap_is_non_empty_while_the_divergence_row_stands
needs at least one AbsentFromEmitMainRs row and 17 remain after this one goes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Delete v2.lens.cited_symbol_resolution, and keep the twelve of its twenty-seven witnesses that were never its

DESIGN authorised this cut and got its population wrong, which is the finding rather than
a footnote. The row read "v2.lens.cited_symbol_resolution and its sixteen witnesses are not
deleted -- they are unreachable from any required check and are dead rather than competing".
Both halves of that population claim are false, and this change corrects the row in the same
diff that falsifies it.

SIXTEEN WAS THE COUNT AT #7707, when the lens landed. The file grew twice after
(#8673 enrolled roster_registry, #8775 the two instance-gap carriers) and held 27 `test fn`
identities. `gunbc.ci_layer_roots` said "eighteen". Three numbers, three snapshots of a
growing file, none of them current -- the transcribed-measurement class the standing rule
already names. The replacement rows name their subject and no number.

AND "DEAD" WAS TRUE OF THE LENS AND FALSE OF A THIRD OF ITS WITNESSES. Measured against the
seven symbols that file imported FROM the lens, 6 of the 27 touch one. The other 21 do not.
"The lens and its witnesses" was never one population, and the three-way split is:

  6  LENS-BOUND -- die with it. The census-green claim, the three planted-control rows, the
     enrolled-population exemption identity, the ambiguous control. `declaration_index`
     re-derives this machinery as PLANTED_CONTROL_CITATIONS plus PlantedControlNoLongerRefuses.

  6  RESOLVER-BOUND -- MOVED, not deleted, to test.claim.long.decl_ref_resolution_witness_test.
     They call `resolve_declaration_ref`, which lives in `v2.std.decl_ref_resolution` -- a
     module that SURVIVES with four other consumers -- and they are the only rows in the tree
     that execute its five-arm refusal. Deleting them because they sat in a file named for
     the lens would be the §4b(4) failure exactly: a climb deletes the redundant PRODUCTION
     machinery, never the discriminating RED and positive control.

  15 CARRIER-BOUND -- MOVED to test.claim.long.carrier_reference_integrity_witness_test.
     Population and projection claims about the four carriers that PROJECT DeclarationRefs.
     Their resolution half is subsumed; their population half is subsumed by nothing.

SUBSUMPTION IS SCOPED, not general: `declaration_index` extracts TYPED-LITERAL citations --
DeclarationRef record literals and the decl_ref/decl_field_ref constructors -- and reports
computed reference fields as a coverage boundary. A prose reference inside a String is
covered by nothing, before or after, and this change does not claim otherwise.

THE PER-PR WITNESS IS RENAMED, NOT DELETED. test.claim.cited_symbol_resolution_witness_test
never imported the lens; its one claim is a three-term bucket partition over
gunbc.doc_graph_roots. Two readers independently concluded from its NAME that the resolution
law was enforced per-PR -- it was not, a bucket identity was -- and after this cut it would
have been the only cited-symbol-named thing left in the tree, reading as the law's residue.
It is now test.claim.doc_graph_reference_partition_witness_test. Same borrowed-authority
shape as #9252's fixture rehome, one layer up: there the home was borrowed, here the name.

WHAT THE WALL ITSELF NAMED, because this was cut delete-first and the census is the deletion.
The first corpus run after the cut reported six refusals: two IMPORT-MEMBER-ABSENT for a
`CitedSymbolResolution` lens-id the registry no longer declares, and four
PLANTED-CONTROL-RESOLVES for the exact rows #9211 declared as this cut's residue ("they
delete with the lens, not before it"). Every one predicted, none discovered by reading.

AND ONE GAP THE ROSTER DELETION WOULD HAVE OPENED, which is why those four rows are not
simply removed. Each named one refusal arm of the cited-symbol wall. Three of the four arms
already had controlled fixtures in tests/declaration_index_integrity.rs. THE FOURTH DID NOT:
measured, the string `CitedFieldAbsent` did not occur in that file at all, so its only
evidence anywhere was the planted row I was deleting. Deleting it would have left a refusal
arm with nothing executing against it -- §4b(4) again, one level up from where I first hit it.
`citation_to_an_absent_field_is_refused_and_a_present_field_is_not` is authored here, with
its positive control, and a controlled fixture is the stronger oracle anyway (§5): the
planted row only ever asserted that one hand-authored citation still refuses.

PLANTED_CONTROL_CITATIONS is left EMPTY rather than deleted. Mechanism reachable, join
reachable, occupancy zero -- a healthy guard being quiet, not a dead one.

EVIDENCE, by execution (remote, release binaries):
                              before        after
  parse-clean files           4012          4011      the lens module
  modules                     4012          4011
  citations                   1470          1466      the lens's four planted citations
  lens_modules                71            70
  debt                        42            42        UNCHANGED
  corpus findings             0             0
  declaration_index_integrity 21 passed     22 passed the new field-absent pair

THE DEBT COUNTS RECONCILE, and the brief's "46" is none of them. 38 = roster rows, counted.
46 = citation SITES at the time the roster's doc comment was written. 42 = citations
currently suppressed by a row, the live measurement. debt is 42 before and after, and a row
that stopped reproducing refuses as CitationDebtRowStale -- none did, which is the executable
form of "the defects are still found".

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants