Repository navigation
Seed-honesty verdict + acceptance receipt; sweep the stale gunbc_ci_floor_batches citations - #7688
Conversation
…he acceptance receipt The verdict greened v1_seed_honesty_decision_closing_contract_holds, which left seed_honesty_undecided_keeps_closing_contract_red asserting a state that no longer exists -- it could only go red or be deleted, and DESIGN 4b(4) forbids deleting the evidence with the machinery. The conjunction is now a function of the decision, applied to the live constant by the contract and to SeedHonestyUndecided by a permanent control. Receipt digest 1717cfe258d9afe1 derived by execution via node_criteria_digest; the probe reproduced f1c76111c83a0a60 for v2-emitter-producer-provenance, byte-matching the receipt already stored for that node, and returned three distinct values for three nodes. Green by execution under claim_batch on this tree: all three of v1_seed_honesty_decision_closing_contract_holds, seed_honesty_undecided_would_keep_closing_contract_red and seed_honesty_check_four_poles_hold_before_decision PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… DeclarationRefs The function was renamed to gunbc_ci_floor_plan. One note recorded the rename; the references were never swept. Found by execution -- running DESIGN's own documented CI command refuses: no such function gunbc_ci_floor_batches. Repaired: - DESIGN.md + gunbc.design_document -- the documented claim_executor command did not run. ci.yml passes gunbc_ci_floor_plan, which is what the seven-hit sweep confirms is live. - gunbc.doc_graph_roots -- TWO typed DeclarationRef rows naming a declaration that does not exist. These are the sharpest instances: structured citations, in the carrier built to hold machine-checkable references, resolving to nothing, with no gate reporting it. - gunbc.ci_spec clamp note and gunbc.roster_registry -- live index-alignment and membership claims. NOT substituted blindly: the clamp rows align to the batch list gunbc_ci_floor_ordinary_batches, not to the plan function, per witness_scoped_batch_is_singleton_and_outside_positional_clamps. Substituting the plan function would have replaced one false citation with another. Deliberately NOT changed: gunbc_ci_floor_batch_wall_budget_note, which says 'named gunbc_ci_floor_batches through the static era this note records'. That is a correctly framed historical mention and the only place the rename was recorded. DESIGN.md is generated; the documented regen (generated_artifact_gate main_wet) refuses locally at stage0_emission_source_identities_host, and that refusal reproduces on pristine origin/main, so it is not introduced here. The DESIGN.md edit is the character-identical substitution the generator would produce from the corrected carrier, verified by comparing the rendered line to the carrier literal; the drift gate is the independent check on that claim. This is the class DESIGN 3 predicts and has not walled -- feature:cited-symbol-resolution would have caught all seven. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Operator ruling: #7681 merged before design review completed. Not reverted -- it is document-only and no promoted generation depends on it -- but its non-authoritative status is made explicit rather than left to be inferred. The banner states what the document does NOT authorize (promotion, warm reuse, recovery-anchor release, deletion of a prior generation) and lists the nine outstanding corrections, three blocking. The sign-off bar is retained rather than deleted, as the record of what it asked for, and annotated with why it did not catch this: every item it names is satisfiable while the highest-stakes concepts stay undefined. A bar that checks whether cited symbols resolve and whether sections exist cannot detect that FixForwardProof and StageStamp are names without models. Full amendment is G0 (proud-fox-809). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Bugbot is not enabled for your account, so this pull request was not reviewed. Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs. |
… 47620) The review is correct and this was a real defect in my own change. Deleting the seed-honesty QuarantineProbeExpectRed enrollment removed the only thing scheduling the file. It sat in src/v2/test/claim/execution/, which carries a DIRECTORY-grain OfflineLocalRecipe exclusion (stated reason: the emit-vs-eval execution corpus home) and is not in witness_discovery_scan_dirs at all. So both the closing contract AND the permanent DESIGN 4b(4) control were left executing nowhere on the merge-gating path -- a one-time RedControlExecuted receipt backing a regression wall that never runs again. That is specification-without-execution for the exact wall the change claims to keep, and the PR body asserted the opposite: that this run would be the claim_executor verification. It would not have been. These witnesses are hermetic -- constructed DiverseCompilationRun fixtures, no host read -- so they never belonged in an emit-vs-eval execution home. Moving them is the construction fix; an explicit witness_entries row would have been a second exception layered on a wrong classification. Verified on BOTH halves, which is the part that matters: dag/test/claim IS a discovery scan dir (positive membership), and NO exclusion pattern matches the new path. Checking only the exclusion roster is how a sibling lane produced a false zero the same day. Green by execution under claim_batch from the new location: all three of v1_seed_honesty_decision_closing_contract_holds, seed_honesty_undecided_would_keep_closing_contract_red and seed_honesty_check_four_poles_hold_before_decision PASS. Receipt witness_module and both handback/entry paths repointed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in c539f41. Review 47620 was correct and this was a real defect in my own change, not a scoping disagreement. The finding, restated so the record is unambiguous: deleting the seed-honesty QuarantineProbeExpectRed enrollment removed the only thing scheduling that file. It lived in src/v2/test/claim/execution/, which carries a DIRECTORY-grain OfflineLocalRecipe exclusion (stated reason: the emit-vs-eval execution corpus home) and is not listed in witness_discovery_scan_dirs at all. So both the closing contract and the permanent DESIGN 4b(4) control were left executing nowhere on the merge-gating path. Worse, the PR body asserted the opposite -- that this run would be the claim_executor verification. It would not have been. The fix is the move, not an enrollment exception. These witnesses are hermetic (constructed DiverseCompilationRun fixtures, no host read anywhere), so they never belonged in an emit-vs-eval execution home; they were there incidentally. They now live in dag/test/claim/. Adding an explicit witness_entries row instead would have layered a second exception on top of a wrong classification. Verified on BOTH halves rather than one, which is the part I want on the record: dag/test/claim IS a discovery scan dir (positive membership), and NO exclusion pattern in ci_layer_roots matches the new path. Checking only the exclusion roster is precisely how a sibling lane produced a false zero the same day -- absence of exclusion is not presence of scheduling. Green by execution under claim_batch from the new location: v1_seed_honesty_decision_closing_contract_holds, seed_honesty_undecided_would_keep_closing_contract_red, and seed_honesty_check_four_poles_hold_before_decision all PASS. Naming the executor deliberately -- claim_batch, claim_executor and gunbc run are three separate binaries and only claim_executor gates a merge. The acceptance receipt witness_module and both handback/entry paths are repointed, and the file note and PR body now record what was wrong rather than quietly reading correct. — sent from still-bat-561 |
… not scan_dirs Read claim_executor rather than trusting the roster name. invoke_floor_discovery_ producer_over_corpus uses scan_dirs ONLY for the discover_owned_data_decls loop; the witness producer discover_floor_corpus_rows_from_host_facts receives source_roots and exclude_substrings and never sees scan_dirs. So witness discovery is a source-root walk for *_test.dag minus exclusions, and witness_discovery_scan_ dirs is the owned-data-decl scope, not the witness scope. Consequence for this PR: the file move is STILL the correct repair, but not for the reason given. The old location was already reachable by the walk; what excluded it was the exclusion substring test/claim/execution/, which the walk does honor. The operative repair is leaving an excluded path. The scan-dir half of the previous justification named a mechanism that does not govern witnesses at all. Fix unchanged, reason corrected. Credit to deep-swift-442, who read the executor and refuted both their model and mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/ci_layer_roots.dag
Remove duplicate gunbc_ci_floor_batches→plan edits (#7688 carries them). Long witness records the derived census: two declaration_absent HandAuthoredDocBind refs on main-equivalent tree, zero other arms. Co-authored-by: Cursor <cursoragent@cursor.com>
# Conflicts: # docs/plans/emission-admission-stage-aware-pipeline-design.md
Production gate excludes three enrolled ProbeDoc binds (declaration-absent, module-absent, field-absent) plus a lens-module ambiguous fixture so a zero production population cannot pass vacuously after #7688 merges. Co-authored-by: Cursor <cursoragent@cursor.com>
…xclusion/probe_red dual representation
One operational fact was represented twice, in two hand-synchronized rows: a
`WitnessExclusionRow { pattern: FILE.dag, classification: QuarantineProbeExpectRed }`
saying the FILE must not run through green-only discovery, beside a
`probe_red(entry, f)` row saying that exact FUNCTION must execute on the
expected-red lane. Neither derived from the other, and the reconciliation
guarding them was weaker than its name: it asked only whether SOME scheduled
row's entry CONTAINED the exclusion pattern as a substring. It proved neither
exact identity, nor one schedule row per exclusion, nor reverse coverage, nor
that every function hidden by the file-level exclusion had a consumer, nor
that the pair deleted atomically.
The bad state that remained expressible: a file holds an expected-red function
and an ordinary green one, the file-level exclusion hides both, the schedule
names only the red one, and the green one executes nowhere while the check
still passes. MEASURED on the pre-change tree, it had exactly one live
instance: seed_honesty_discharge_unavailable_test.dag, 8 of whose 9 functions
had no probe row while the file's classification named the whole file
QuarantineProbeExpectRed. Everywhere else the file-grain roster form or the
Phase 0(b) orphan refusal already covered it. The same imprecision forced a
documented workaround: self_host_03_normalize's exclusion row records that
QuarantineProbeExpectRed on the file would orphan its sibling, so the file was
downgraded to OfflineLocalRecipe in prose instead.
ROOT FIX - `gunbc.explicit_witness_admission`, one row per admitted witness:
ExplicitWitnessAdmission { witness: ScheduleWitnessEntry,
cadence: WitnessConsumerCadence,
reason: NonEmptyStr, dissolve_on: NonEmptyStr }
Everything else derives from it. `known_red_probe_roster()` is its
CorpusWitnessKind projection; `seed_emitter_behavioral_wet_known_red_entries`
is its ExecutionWitnessKind projection (its hand rows are deleted, the decl
name kept so no consumer changed); the discovery exclusion is read straight
off the rows by `floor_discovery_producer` at exact (entry, function) grain,
per test declaration rather than per file; the consumer manifest and the
admission reconciliation read the same rows. 13 pattern rows are deleted.
A deletion now removes admission, roster entry and exclusion in one edit -
the merge hazard #7688 paid for by hand.
SEPARATION. `witness_exclusion_frontier` is now a PATH POLICY carrier
(`test/claim/long/` is a home, `test/manual/` is offline). Exact admission and
broad path policy no longer share a substring representation:
`witness_exclusion_row_well_formed` REFUSES a QuarantineProbeExpectRed row
there outright, so the fused shape is unwritable rather than reconciled.
Precedence is total - exact admission decides the functions it covers, path
policy applies only to functions with none - which is why a path-offline file
may legitimately contain an exact-admitted function without either fact
restating the other. The four remaining executing cadences still author a path
row beside their rosters; that residue is named and counted in
`explicit_witness_admission_separation_note` with its dissolve-on, and it is
not the bad state today (each is file-grain or fully enumerated, measured).
WALLS, all executing: exactly one admission per witness; every admission names
a cadence that executes (DiscoverySelection / OfflineLocalRecipe /
FixtureExplicitRoster / NoConsumer refused, so an admission cannot satisfy the
has-a-consumer rule while running nowhere); every admission is reached by its
cadence's derived roster; every admission is excluded by derivation; no
admission is restated as a path-policy row. Admitted witnesses stay COUNTED in
the deferred-discovery receipt - with the pattern rows gone they would
otherwise have vanished from it, the uncounted degradation DESIGN 5 forbids in
the mechanism whose job is making deferral visible.
Evidence, by execution:
- dag/test/claim/exact_witness_admission_witness_test.dag - 9/9 PASS. The
discriminating RED asserts the admission reaches the admitted function and
NOT the named sibling (false by construction under the old shape), with a
file-grain control proving that shape does reach the sibling so the claim
cannot pass vacuously; plus duplicate-row and non-executing-cadence controls.
- cli_run.rs `explicit_witness_admission_is_exact_not_file_grain` - the same
discriminator on the host side; 5/5 witness_admission unit tests PASS.
- witness_exclusion_reconciliation_test 8/8, witness_admission_test 15/15,
ci_floor_plan_witness_test 31/31, floor_discovery_hand_rust_equivalence
23/23, proactive_verification_ledger_witness_test 1/1.
- whole-tree `--target dag` compile: 4 hard diagnostics, byte-identical to the
same compile on main (434e217) in a clean worktree - pre-existing, unchanged.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nforcement lens inventory TWO CLIMBS CARRIED ACROSS. #7709 landed the emit repair that greens cross_module_same_leaf_emits_qualifier_module_not_registry_winner, so main deleted its QuarantineProbeExpectRed exclusion row and its probe_red row — the same §4b(4) climb #7688 performed for seed-honesty one merge earlier. On this branch each of those pairs is ONE explicit_witness_admissions row, so each climb is one deletion. Known-red admissions go 18 -> 17 (11 CorpusWitnessKind + 6 ExecutionWitnessKind). Both conflict hunks are again the pre-migration shape versus the migrated one, so the representation comes from this side while main's substance is carried by hand — which is the hazard this lane exists to remove, and it is now the third merge in a row where taking a side wholesale would have silently dropped or resurrected admission rows. BROKEN CALLER, found by review (review 47781), verified and fixed. `witness_row_excluded_from_discovery` gained a `function` parameter so it can consult the admission authority at the grain the authority is written in. `v2.lens.enforcement.inventory` `cadence_scheduling_rows_for_witness` still called it with `entry:` alone — an arity mismatch that refuses at typecheck, and worse than that: it would have left the lens inventory disagreeing with `floor_discovery_producer` about grain, which is precisely what wall (4) says cannot happen. `function` was already in scope there and is now threaded through, so both readers ask the same question. WHY MY OWN CHECKS MISSED IT, recorded so the next person does not assume the gate covers this. `src/v2/lens/enforcement/inventory.dag` is outside the compiled import closure — the whole-tree `--target dag` compile reports it in the 1180 census-only modules, which are name-censused and not typechecked — and its witness, `enforcement_inventory_witness_test.dag`, is corpus-denominated and path-excluded from per-PR discovery (enforcement_coverage_exclusion_note). So neither the compile I ran nor the floor would have caught it; an offline witness plus a census-only module is a blind spot for exactly the re-signature class, and here the reviewer was the only mechanism that saw it. Green by execution after the fix, including the witness that reaches the repaired caller: enforcement_inventory_witness_test 10/10, exact_witness_admission_witness_test 9/9, witness_exclusion_reconciliation_test 8/8, witness_admission_test 15/15. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…/v1). HandAuthoredDocBind anchors cite v1.compiler.* modules outside witness_layer_roots; use compile_clean_source_roots for production census and gate so post-#7688 zero holds. Co-authored-by: Cursor <cursoragent@cursor.com>
…xclusion/probe_red dual representation (#7719) * Exact witness admission: one function-grain authority replacing the exclusion/probe_red dual representation One operational fact was represented twice, in two hand-synchronized rows: a `WitnessExclusionRow { pattern: FILE.dag, classification: QuarantineProbeExpectRed }` saying the FILE must not run through green-only discovery, beside a `probe_red(entry, f)` row saying that exact FUNCTION must execute on the expected-red lane. Neither derived from the other, and the reconciliation guarding them was weaker than its name: it asked only whether SOME scheduled row's entry CONTAINED the exclusion pattern as a substring. It proved neither exact identity, nor one schedule row per exclusion, nor reverse coverage, nor that every function hidden by the file-level exclusion had a consumer, nor that the pair deleted atomically. The bad state that remained expressible: a file holds an expected-red function and an ordinary green one, the file-level exclusion hides both, the schedule names only the red one, and the green one executes nowhere while the check still passes. MEASURED on the pre-change tree, it had exactly one live instance: seed_honesty_discharge_unavailable_test.dag, 8 of whose 9 functions had no probe row while the file's classification named the whole file QuarantineProbeExpectRed. Everywhere else the file-grain roster form or the Phase 0(b) orphan refusal already covered it. The same imprecision forced a documented workaround: self_host_03_normalize's exclusion row records that QuarantineProbeExpectRed on the file would orphan its sibling, so the file was downgraded to OfflineLocalRecipe in prose instead. ROOT FIX - `gunbc.explicit_witness_admission`, one row per admitted witness: ExplicitWitnessAdmission { witness: ScheduleWitnessEntry, cadence: WitnessConsumerCadence, reason: NonEmptyStr, dissolve_on: NonEmptyStr } Everything else derives from it. `known_red_probe_roster()` is its CorpusWitnessKind projection; `seed_emitter_behavioral_wet_known_red_entries` is its ExecutionWitnessKind projection (its hand rows are deleted, the decl name kept so no consumer changed); the discovery exclusion is read straight off the rows by `floor_discovery_producer` at exact (entry, function) grain, per test declaration rather than per file; the consumer manifest and the admission reconciliation read the same rows. 13 pattern rows are deleted. A deletion now removes admission, roster entry and exclusion in one edit - the merge hazard #7688 paid for by hand. SEPARATION. `witness_exclusion_frontier` is now a PATH POLICY carrier (`test/claim/long/` is a home, `test/manual/` is offline). Exact admission and broad path policy no longer share a substring representation: `witness_exclusion_row_well_formed` REFUSES a QuarantineProbeExpectRed row there outright, so the fused shape is unwritable rather than reconciled. Precedence is total - exact admission decides the functions it covers, path policy applies only to functions with none - which is why a path-offline file may legitimately contain an exact-admitted function without either fact restating the other. The four remaining executing cadences still author a path row beside their rosters; that residue is named and counted in `explicit_witness_admission_separation_note` with its dissolve-on, and it is not the bad state today (each is file-grain or fully enumerated, measured). WALLS, all executing: exactly one admission per witness; every admission names a cadence that executes (DiscoverySelection / OfflineLocalRecipe / FixtureExplicitRoster / NoConsumer refused, so an admission cannot satisfy the has-a-consumer rule while running nowhere); every admission is reached by its cadence's derived roster; every admission is excluded by derivation; no admission is restated as a path-policy row. Admitted witnesses stay COUNTED in the deferred-discovery receipt - with the pattern rows gone they would otherwise have vanished from it, the uncounted degradation DESIGN 5 forbids in the mechanism whose job is making deferral visible. Evidence, by execution: - dag/test/claim/exact_witness_admission_witness_test.dag - 9/9 PASS. The discriminating RED asserts the admission reaches the admitted function and NOT the named sibling (false by construction under the old shape), with a file-grain control proving that shape does reach the sibling so the claim cannot pass vacuously; plus duplicate-row and non-executing-cadence controls. - cli_run.rs `explicit_witness_admission_is_exact_not_file_grain` - the same discriminator on the host side; 5/5 witness_admission unit tests PASS. - witness_exclusion_reconciliation_test 8/8, witness_admission_test 15/15, ci_floor_plan_witness_test 31/31, floor_discovery_hand_rust_equivalence 23/23, proactive_verification_ledger_witness_test 1/1. - whole-tree `--target dag` compile: 4 hard diagnostics, byte-identical to the same compile on main (434e217) in a clean worktree - pre-existing, unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Remove dag/gunbc/witness_quarantine.dag — a superseded draft of the admission authority that a stash cycle resurrected into the branch It was the first-round shape of this lane's carrier (known-red rows only, no cadence field, no path-policy separation) and was replaced by gunbc.explicit_witness_admission before any consumer referenced it. Nothing imports it. Leaving it would have shipped a second copy of the authority whose whole purpose is that there is one — the violation this PR closes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Re-anchor the discriminating RED to a synthetic fixture — a live-anchored assertion loses its subject when the wall works Review caught a real defect before merge: the discriminating assertion was anchored to live rows that gunbc#7688 deletes tonight. It hardcoded the seed-honesty entry, its admitted function and a named green sibling, and read the live roster — so when the operator's verdict lands, the closing contract greens and the quarantine climbs out under DESIGN 4b(4), the assertion would have had no subject left: passing vacuously, or redding for a reason with nothing to do with the wall. The instinct behind it was the right one in general — a wall is better evidenced by a defect that actually happened than by a synthetic one — but it binds the evidence to the defect's CONTINUED EXISTENCE, which is precisely what the wall exists to end. 4b(4) says a climb deletes the production machinery and keeps the evidence enrolled; a live-anchored assertion cannot satisfy that clause, because the machinery and the subject are the same rows. Same shape as the vacuous-green trap a sibling lane hit on G1 an hour ago: a gate whose population reached zero could not be distinguished from a predicate returning true unconditionally. So the primary assertion now runs against a fixture this witness authors itself — one admission over a fixture entry holding an expected-red function and an ordinary green one — asserting the admission reaches the first and not the second, with the file-grain control running the SAME predicate over the file-grain shape to show it DOES reach the sibling. Both arms are synthetic, so neither can lose its subject. The Rust discriminator is re-anchored the same way, against synthetic source rather than the live authority, and gains a population-independent companion: no live known-red admission uses the file-grain form. The three remaining live-row claims are universals and a projection identity — true at any roster size including zero — and a note says so explicitly, so nobody later mistakes them for where the discrimination lives. The seed-honesty instance survives as a past-tense provenance note in the witness and on the row itself, stating that no evidence is anchored to it and it deletes cleanly. That keeps the measurement that justifies the wall without making the wall depend on it. Evidence: witness 9/9 PASS after re-anchoring; 6/6 Rust witness_admission unit tests PASS (one new). 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>
Remove duplicate gunbc_ci_floor_batches→plan edits (#7688 carries them). Long witness records the derived census: two declaration_absent HandAuthoredDocBind refs on main-equivalent tree, zero other arms. Co-authored-by: Cursor <cursoragent@cursor.com>
Production gate excludes three enrolled ProbeDoc binds (declaration-absent, module-absent, field-absent) plus a lens-module ambiguous fixture so a zero production population cannot pass vacuously after #7688 merges. Co-authored-by: Cursor <cursoragent@cursor.com>
…/v1). HandAuthoredDocBind anchors cite v1.compiler.* modules outside witness_layer_roots; use compile_clean_source_roots for production census and gate so post-#7688 zero holds. Co-authored-by: Cursor <cursoragent@cursor.com>
Remove duplicate gunbc_ci_floor_batches→plan edits (#7688 carries them). Long witness records the derived census: two declaration_absent HandAuthoredDocBind refs on main-equivalent tree, zero other arms. Co-authored-by: Cursor <cursoragent@cursor.com>
Production gate excludes three enrolled ProbeDoc binds (declaration-absent, module-absent, field-absent) plus a lens-module ambiguous fixture so a zero production population cannot pass vacuously after #7688 merges. Co-authored-by: Cursor <cursoragent@cursor.com>
…/v1). HandAuthoredDocBind anchors cite v1.compiler.* modules outside witness_layer_roots; use compile_clean_source_roots for production census and gate so post-#7688 zero holds. Co-authored-by: Cursor <cursoragent@cursor.com>
…exactly one declaration, or refuses (#7707) * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * G1: five-arm cited-symbol resolution over containment tree Replace the text-scan declaration_refs_in_corpus path with a structural resolver (decl_facts + module_declaration_facts) and five typed refusal arms. Gate hand-authored doc binds, fix stale gunbc_ci_floor_plan refs, and drop unused host builtin code so cargo fmt passes. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix decl_ref_resolution parse error: avoid fn as bind name Binding NamedField.field_name to `fn` made the parser expect a function definition (expected LParen, found Ident). Use `f` and list_map. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix CI: enroll cited_symbol lens and move slow witnesses to long/ Register v2.lens.cited_symbol_resolution in lens_registry_v0, cache witness-layer decl_facts once for fast per-PR RED controls, and move corpus-scale resolution witnesses to dag/test/claim/long/. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix cited_symbol witness parse error: single-line data binding Multi-line data initializer after `=` is invalid surface syntax (expected expression, found Newline). Co-authored-by: Cursor <cursoragent@cursor.com> * Add CitedSymbolResolution to lens_module_gate surface table Completes exhaustive LensIdV0 match required when enrolling the new cited-symbol-resolution lens in lens_registry_v0. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * Drop doc_graph stale-ref repair; add pre-7688 census witness Remove duplicate gunbc_ci_floor_batches→plan edits (#7688 carries them). Long witness records the derived census: two declaration_absent HandAuthoredDocBind refs on main-equivalent tree, zero other arms. Co-authored-by: Cursor <cursoragent@cursor.com> * Add permanent planted controls for cited-symbol resolution gate. Production gate excludes three enrolled ProbeDoc binds (declaration-absent, module-absent, field-absent) plus a lens-module ambiguous fixture so a zero production population cannot pass vacuously after #7688 merges. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix cited_symbol witness parse error: newline before ==. CI regen/heal failed with 'expected expression, found EqEq' on multiline equality in cited_symbol_resolution_witness_test.dag. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix CI: recursion in ambiguous witness; move slow tests to long lane. The fast-lane test shadowed the lens fn and recursed to depth 100k. decl_facts-heavy mutation witnesses move to long/ per the 5s operator rule. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix ambiguous planted control: resolve via resolver, not shadowed wrapper. Test fn name collision caused unbounded self-recursion. Witnesses now call resolve_declaration_ref on planted duplicate decl_facts fixtures; document bounded DeclarationRefAmbiguous path and shadowing hazard in authority note. Co-authored-by: Cursor <cursoragent@cursor.com> * Record witness import-shadowing finding in G1 witness carrier note. Documents same-named test fn shadowing imported helper (depth 100k self-call) as namespace-resolution relative hazard; not a resolver ambiguity defect. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * Resolve doc-graph cited symbols over compile_clean pool (includes src/v1). HandAuthoredDocBind anchors cite v1.compiler.* modules outside witness_layer_roots; use compile_clean_source_roots for production census and gate so post-#7688 zero holds. Co-authored-by: Cursor <cursoragent@cursor.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * fix(ci): sync regen fixed-point and ci.yml for G1 witness exclusion row The WitnessExclusionRow for long/cited_symbol_resolution_witness_test.dag required regenerating ci.yml merge-conflict excludes and running regen_stage0 so RegenVerifyGate passes on CI. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * Fix regen drift: restore compiler_tests sidecar assertions and lib dispatch. Rebuild regen_stage0 so compiler_tests.rs matches compiler_tests_rust.dag authority (rebuilt_left/expected_left), and regen emits v1_interpreter_dispatch_generated in lib.rs again. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: G1: cited-symbol resolution — every typed DeclarationRef resolves to exa * Note OfflineLocalRecipe exclusion row on fast cited-symbol witness. Cross-reference ci_layer_roots long-lane exclusion from the fast enrollment witness carrier (review 47883 observational note). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Summary
Records the operator's seed-honesty verdict, greens the closing validation that was deliberately red without it, and files the acceptance receipt for
v1-seed-honesty-decision.The node's handback was two things — a check that can fail, plus the decision recorded either way. Only the first half existed. The decision procedure (
seed_self_verify_check) landed earlier and is genuinely discriminating: a reflexive claim/check refuses withbootstrap_self_verify_same_artifact, a planted divergence withbootstrap_self_verify_diverged, mismatched provenance withbootstrap_self_verify_provenance_mismatch, and a distinct equal-content pair with equal provenance admits, so none of the three refusals is a blanket red. Butseed_honesty_decisionwasSeedHonestyUndecided, so the aggregate stayed red and was enrolledQuarantineProbeExpectRedrather than reported done over the missing half.The verdict is
FixedPointTrustSufficient, and the name undersells its conditions. It does not say a fixed point is trustworthy. It says v1 deletion does not require an independently implemented second compiler, and requires instead an explicit generation-admission pipeline — each stage executes against a declared requirement revision and binds its exact inputs, outputs, producer and verdict; a candidate generation may be produced and inspected but cannot promote itself; promotion requires declared requirement changes, complete stage and behavioral receipts, no undeclared v1 fallback, and a retained known-good recovery path; breaking requirement changes require an expand-migrate-contract bridge; and the previous generation stays available until the promoted compiler produces a valid changed successor rather than merely reproducing itself. That program is designed indocs/plans/emission-admission-stage-aware-pipeline-design.md— the corrected revision, which confers no promotion or merge authority of its own — and is unbuilt. This receipt accepts the decision, not the pipeline the decision requires.What the verdict explicitly does not protect
Carried on the rationale itself so a later reader cannot infer safety from the node being green:
seed_self_verify_checkis not the live trust-path authority. The realized-comparison and regen paths do not route their artifact identities through it. This change does not wire that path.An earlier draft of the rationale argued DDC was unnecessary because the seed's source is readable. That argument is wrong and is corrected here: the classic attack is a binary miscompiling readable source, so readability is not the defense. The narrower claim that survives is a mitigation, not a proof — the emitted Rust is committed as plain text and re-compared by the regen gate, so a perpetuated defect must appear in a readable diff and survive review of it.
The expect-red probe was flipped, not deleted
seed_honesty_undecided_keeps_closing_contract_redread the live decision constant, so the verdict landing left it able to assert only a state that no longer exists — it had to go red or be deleted, and DESIGN §4b(4) forbids deleting the evidence along with the machinery.The conjunction is now a function of the decision,
seed_honesty_closing_contract_over, applied to the live constant by the contract and toSeedHonestyUndecidedby the permanent controlseed_honesty_undecided_would_keep_closing_contract_red. That control is what keeps the fifth conjunct load-bearing: weaken the decision arm so an undecided value satisfies the contract and the contract stays green while only the control reds.Handback
src/v2/workflow/bootstrap.dag— the recorded verdict.src/v2/test/claim/execution/seed_honesty_discharge_unavailable_test.dag— contract parameterized over the decision; expect-red probe flipped to a permanent control.dag/gunbc/ci_layer_roots.dag—QuarantineProbeExpectRedenrollment and witness exclusion deleted (the climb dissolves the quarantine).dag/gunbc/roadmap_authority.dag— the acceptance receipt, plus the stale half ofv1_seed_honesty_decision_contract_notecorrected.Test plan
Naming the executor, because there are at least three and they are not interchangeable.
gunbc run,claim_batch, andclaim_executorare separate binaries with separate entry points, and onlyclaim_executorgates a merge. A local green names which one produced it or it is not a receipt.Green by execution under
claim_batchon this tree, binary rebuilt at this head — all three PASS:v1_seed_honesty_decision_closing_contract_holds— the bound closing validation.seed_honesty_undecided_would_keep_closing_contract_red— the permanent control.seed_honesty_check_four_poles_hold_before_decision— the four refusal/admission poles, unchanged.The witnesses are moved into a home CI actually scans, and that correction is the substance of review 47620. My first cut deleted the seed-honesty
QuarantineProbeExpectRedenrollment and claimed this PR's own CI run would therefore be theclaim_executorverification. That was false. The file sat insrc/v2/test/claim/execution/, which (a) carries a directory-grainOfflineLocalRecipeexclusion whose stated reason is the emit-vs-eval execution corpus, and (b) is not inwitness_discovery_scan_dirsat all. So removing the enrollment removed the only thing scheduling the file, leaving both the closing contract and the permanent §4b(4) control executing nowhere on the merge-gating path — specification-without-execution for the very regression wall this PR says it is keeping.These witnesses are hermetic (constructed
DiverseCompilationRunfixtures, no host read), so they never belonged in an emit-vs-eval execution home. They now live indag/test/claim/.Correction to this PR's own earlier justification, made after reading the executor rather than the roster names. An earlier revision claimed the move worked by gaining positive membership in
witness_discovery_scan_dirs. That was wrong.claim_executor'sinvoke_floor_discovery_producer_over_corpususesscan_dirsfor exactly one thing — thediscover_owned_data_declsloop — and hands the witness producerdiscover_floor_corpus_rows_from_host_factsonlysource_rootsandexclude_substrings. Witness discovery is a source-root walk for*_test.dagminus exclusions;witness_discovery_scan_dirsis the owned-data-decl scope, not the witness scope. The old location was already reachable by the walk. What excluded it was the exclusion substringtest/claim/execution/, which the walk does honor — so the operative repair is leaving an excluded path, and the scan-dir half of the earlier justification named a mechanism that does not govern witnesses at all. The fix is unchanged and still correct; only the reason is.Green by execution under
claim_batchfrom the new location, all three PASS.The criteria digest
1717cfe258d9afe1was derived by execution (node_criteria_digestagainst the live node), not transcribed. The probe carried its own control: it reproducedf1c76111c83a0a60forv2-emitter-producer-provenance, byte-matching the receipt an unrelated change had already stored for that node, and returned three distinct values for three nodes — so it computes the criteria rather than answering with a constant.Also in this PR: the
gunbc_ci_floor_batchescitation sweepBundled rather than split, per the operator's standing preference on PR boundaries. Named here so it is not smuggled.
gunbc_ci_floor_batcheswas renamed togunbc_ci_floor_plan. One note recorded the rename; the references were never swept. Found by execution — running DESIGN's own documented CI command refuses withno such function: gunbc_ci_floor_batches.Repaired:
DESIGN.md+gunbc.design_document— the documentedclaim_executorcommand did not run.ci.ymlpassesgunbc_ci_floor_plan.gunbc.doc_graph_roots, two typedDeclarationRefrows — the sharpest instances: structured citations, in the carrier built to hold machine-checkable references, resolving to nothing, with no gate reporting it.gunbc.ci_specclamp note andgunbc.roster_registry— live index-alignment and membership claims. Not substituted blindly: the clamp rows align to the batch listgunbc_ci_floor_ordinary_batches, not to the plan function, perwitness_scoped_batch_is_singleton_and_outside_positional_clamps. Substituting the plan function would have replaced one false citation with another.Deliberately unchanged:
gunbc_ci_floor_batch_wall_budget_note, which reads "namedgunbc_ci_floor_batchesthrough the static era this note records" — a correctly framed historical mention, and the only place the rename was recorded.DESIGN.mdis generated. The documented regen (generated_artifact_gatemain_wet) refuses locally atstage0_emission_source_identities_host, and that refusal reproduces on pristineorigin/main, so it is not introduced here. TheDESIGN.mdedit is the character-identical substitution the generator would produce from the corrected carrier, verified against the carrier literal; the drift gate is the independent check on that claim, and CI's auto-heal is the corrective if I got it wrong.This is the class DESIGN §3 predicts and has not yet walled.
Corrected — an earlier revision of this body claimed
feature:cited-symbol-resolution"would have caught all seven." It would have caught two.crisp-owl-732re-derived the gate's population by execution againstwitness_layer_roots(2026-08-03) rather than inheriting my list, and the result is narrower than my claim: the G1 gate reads the typedHandAuthoredDocBindcarrier —primary_workplusadditional_works— not a corpus text scan and not prose. Its unresolvable population on the pre-repair tree is 2, bothDeclarationRefDeclarationAbsentonv2.workflow.ci_floor_plan/gunbc_ci_floor_batches(slugswitness-realization-planandprogress-observation-design). Zero module-absent, zero field-absent, zero ambiguous.The other five repairs in this PR —
DESIGN.md,gunbc.design_document,gunbc.ci_spec,gunbc.roster_registry, and the seed-honesty test path — are prose and plan-function citations that sit outside the typed carrier the gate reads, so no gate in flight covers them. That is worth stating plainly rather than letting the stronger sentence stand: a structural gate over typedDeclarationRefrows is not a wall against stale citations generally, and five of the seven defects repaired here would still be writable after G1 lands. Closing that remainder is the open half offeature:cited-symbol-resolution, not something this PR or G1 finishes.Main integrated (merge commit
5618739fe9) — and why the earlier red was not this PR'sThe run at
3502b1afailed, and the failure was inherited, not introduced. The job log names it exactly:1 of 6420 discovery witness(es) failed: cross_module_same_leaf_emits_qualifier_module_not_registry_winner (dag/test/claim/qualified_leaf_registry_collision_emit_witness_test.dag). That file is not in this PR's diff. It is the bare discriminating RED that #7705 landed on main, which redded main itself and every open PR built on it — #7704 and #7710 failed on the identical single witness, 1-of-6411.I verified this rather than inferring it from the coincidence, because I made exactly that mistake earlier today and mis-attributed a failure to an unrelated PR.
#7711 merged the quarantine, so main is repaired at
bd3968ad1d.origin/mainis merged in here.The conflict was in
dag/gunbc/ci_layer_roots.dag, and it is the one place a careless resolution would have done real damage. Both sides edit the quarantine roster: this branch deletes the seed-honestyQuarantineProbeExpectRedrow and its pairedprobe_redentry (that deletion is the §4b(4) climb this PR exists to make), while main adds two new pairs —qualified_leaf_registry_collision_emit_witness_test.dag(#7711) andv2_emitter_direct_rust_door_acceptance_test.dag(#7680). Taking either side wholesale would have either resurrected the quarantine this PR dissolves or dropped a quarantine main depends on to stay green.Resolution checked structurally, not by eye: the resulting exclusion-pattern set and
probe_redentry set differ fromorigin/mainby exactly one element each —seed_honesty_discharge_unavailable_test.dag— which is precisely this PR's intent and nothing else. Pairing was re-verified: everyQuarantineProbeExpectRedrow still has its matchingprobe_redentry, and the six rows that do not are the unchanged pre-existing main baseline, identical before and after.