Exact witness admission: one function-grain authority replacing the exclusion/probe_red dual representation

[gunbai-bot]

What this does

One operational fact was represented twice in dag/gunbc/ci_layer_roots.dag, 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.

gunbc.explicit_witness_admission is now the single function-grain authority:

ExplicitWitnessAdmission { witness: ScheduleWitnessEntry,
                           cadence: WitnessConsumerCadence,
                           reason: NonEmptyStr, dissolve_on: NonEmptyStr }

Everything else derives from it — known_red_probe_roster() (CorpusWitnessKind projection), seed_emitter_behavioral_wet_known_red_entries (ExecutionWitnessKind projection; hand rows deleted, decl name kept so no consumer changed), the discovery exclusion (read off the rows by floor_discovery_producer per test declaration rather than per file), the consumer manifest, and the reconciliation. 13 pattern rows deleted. A deletion now removes admission, roster entry and exclusion in one edit.

witness_exclusion_frontier becomes a path-policy carrier and witness_exclusion_row_well_formed REFUSES QuarantineProbeExpectRed there, 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.

Status

DONE and green by execution. The known-red cadence is fully migrated; all walls execute. Nothing in this PR is a stub or a placeholder.

IN FLIGHT: nothing. All work is committed and pushed. There is no local state.

BLOCKED: nothing. No question is outstanding for the parent or the operator.

CI: on the pre-merge head, build, regen (10m2s — the self-host fixed point) and heal_generated_artifacts all passed; the floor ci job had not finished before main moved and the branch had to be re-merged. It needs a fresh run on the current head. If it is red, the surfaces to look at first are the seven files that re-enter the discovery walk now that their path rows are gone — logic_ground_truth_test.dag, english_emit_add_test.dag, and the five self_host_*_behavioral_witness_test.dag files — where the producer now reads each file and drops only the admitted functions rather than skipping the file wholesale.

What I would do next if I continued: resolve the expected ci_layer_roots.dag conflict with #7688 (see below), then nothing else on this lane. The remaining migration is deliberately not next; see the residue section.

Two findings that the diff does not show

1. The bad state had exactly ONE live instance, and only under a specific condition.

Window: the pre-change tree at 434e217. Denominator: all 13 QuarantineProbeExpectRed pattern rows and all 33 exclusion rows carrying an executing cadence (BinWitnessWet 23, QuarantineProbeExpectRed 13, FalsifierSubstrateLongLane 4, FalsifierRehomedBinWet 3). Method: for each such pattern, expand it against every *_test.dag in the tree, enumerate that file's test fn/test data declarations, and subtract the (entry, function) pairs covered by any function-grain roster — treating the empty-function form as covering every declaration in its entry, which is what expand_explicit_entries does at execution time.

Result: 8 unscheduled functions, all in one file — 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. They were absorbed as OfflineLocalRecipe by the test/claim/execution/ path policy, which is why the Phase 0(b) orphan refusal never saw them.

The condition matters more than the count: absorption happens only where an explicit-cadence file exclusion also sits under a broad path policy. That is the exact-admission/path-policy fusion, confirmed by measurement rather than assumed. Everywhere else the file-grain roster form or the Phase 0(b) refusal already covered it.

2. A hypothesis I was handed, refuted. I was told six quarantine patterns had no matching probe_red and asked to establish whether they were the bad state or a different classification. They are a different classification, not a defect: five self_host_*_behavioral_witness_test.dag files plus 03_normalize are SelfEmitted wet assemble-red receipts whose function-grain roster is falsifier_self_host_wet_known_red_entries, not known_red_probe_entries. Each of those files carries exactly one test fn and it is on that roster, so no orphan exists. They are the same dual representation at a different WitnessKind, which is why this PR migrates them in beside the hermetic rows rather than leaving them.

3. A design mistake, caught in review, worth not re-deriving. My first discriminating RED was anchored to the real live defect above — hardcoded entry, admitted function, named green sibling, reading the live roster. Anchoring to a real defect is normally the stronger move, and here it was wrong: it binds the evidence to the defect's continued existence, which is the one thing a wall exists to end. #7688 dissolves that quarantine, which would have left the assertion with no subject — passing vacuously, or redding for a reason unrelated to the wall. DESIGN §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. Re-anchored to a synthetic fixture, with a file-grain control running the same predicate to show it DOES reach the sibling, so the false is a decision about grain and not a predicate that never matches. Same fix on the Rust side. The live instance survives as a past-tense provenance note.

Note for whoever reads the approvals: one review praised the live anchor as "a real green→red flip, not a synthetic". It reviewed the commit before the re-anchoring, and that praise was for precisely the property that had to be removed.

Residue I deliberately did not close

BinWitnessWet, FalsifierRehomedBinWet, FalsifierSubstrateLongLane and FalsifierSelfHostWet still author a path row beside their function-grain rosters. Measured on this change's tree, none of them is the bad state — every one is either a file-grain roster row or fully enumerated. Migrating ~70 more rows through the load-bearing floor in one PR is where I judged risk to outrun benefit. It is carried as a counted frontier with a dissolve-on in explicit_witness_admission_separation_note, not left silent: when each cadence's roster moves to the admission authority, witness_exclusion_row_well_formed widens to refuse that cadence too, and the last enum arm that can appear in the path carrier is gone.

Merge hazard — encountered three times, resolved

main is merged in (through #7709). The conflict predicted here happened on every merge and always in the same shape: main holds the pre-migration dual representation, this branch holds it migrated, so the representation comes from this side while main's substance is carried by hand. Taking either side wholesale would have silently dropped or resurrected admission rows with no conflict marker — the hazard that motivated this lane, met three times in one evening.

Two §4b(4) climbs landed on main while this was open and are carried across, each as a single row deletion where main needed two:

• Seed-honesty verdict + acceptance receipt; sweep the stale gunbc_ci_floor_batches citations #7688 — the operator recorded the seed-honesty verdict, the closing contract greened, the quarantine dissolved.
• Fix leaf-keyed qualified lookup collision in Rust emit #7709 — the emit repair greened cross_module_same_leaf_emits_qualifier_module_not_registry_winner.

Known-red admissions: 19 → 17 (11 CorpusWitnessKind + 6 ExecutionWitnessKind). No evidence moved with either climb — the discriminating RED was re-anchored to a synthetic fixture in b353eb9 precisely so a climb could not take the witness's subject with it, which is the anchoring fix paying for itself twice within the hour.

The inherited main breakage — diagnosed here, repaired on main, now merged in

For a period this PR's build failed with error[E0061]: v1_compiler_emit_rust.rs:14088 called v1_generic_params_needing_clone_bound with 6 arguments where v1_compiler_trait_derive_emit.rs:321 declares 9. It was never caused here — both files were byte-identical to origin/main, and main's own runs failed identically.

Cause, and it is worth keeping: a generated-artifact merge collision. #7708 changed that function from 6 params to 9 and updated its one call site, touching both the hand file and the generated v1_compiler_emit_rust.rs. #7709 then rewrote 372 lines of that same generated file, regenerated from a base predating #7708, reverting the call site to 6 args. Git merged both without a conflict because the hunks were textually disjoint. There is exactly one call site in the file, which forecloses the missed-second-caller reading: this was one lane's regen output silently clobbering another lane's substance inside a derived artifact. Two changes to one generated file, merged clean, one dropping the other, no marker and no gate. Structurally the same hazard as the roster hazard above — which is what this PR removes for admission rows.

A finding that outlives the incident: the heal path has a hole exactly where it is needed. heal_generated_artifacts is the job that would regenerate a drifted artifact, but it is gated behind build. So it repairs every class of generated-artifact drift except the one that breaks compilation — the one case where build cannot pass to let it run. On this PR's failing run, build failed at 1m8s and ci, regen and heal_generated_artifacts all showed skipping. A regen cannot rescue it either, because regen runs the seed binary and the seed binary is what fails to build. That makes this class of break permanently manual. It is a property of the heal wiring, not of this PR, and is recorded separately for the operator.

Repaired on main by #7733 (main 19cc776d4e, run 30787387741 with build and regen both success), and merged into this branch at 6c6a7b4. Verified rather than assumed:

• Clean merge, zero conflicts.
• git diff origin/main...HEAD -- src/v1/stage0/src/v1_compiler_emit_rust.rs is empty — this branch contributes no change to that generated file, so the merge cannot have reverted the repair. (The three-dot merge-base diff is the right oracle; a direct compare against main produces false alarms when a branch is merely behind.)
• No file this branch touches is regen-owned: checked every changed path against the 118 entries of gunbc.stage0_emit_plan_generated.generated_stage0_files; cli_run.rs and claim_executor.rs are hand-Rust and appear in neither.
• The exact gate that had been failing, cargo check -p v1-compiler-tests --tests, now passes locally on the merged tree.

No content changed in this merge — the approvals stand against the same work, and CI reruns on the new head.

A blind spot this PR found the hard way

review 47781 caught a broken caller I had missed: v2.lens.enforcement.inventory still called witness_row_excluded_from_discovery with entry: alone after it gained its function parameter. Fixed in f8029b9 by threading function through (it was already in scope), verified by enforcement_inventory_witness_test.dag 10/10 PASS.

The part worth keeping is why no automated check would have caught it. src/v2/lens/enforcement/inventory.dag is outside the compiled import closure — the whole-tree --target dag compile reports it among the 1180 census-only modules, which are name-censused and not typechecked — and its only witness is corpus-denominated and path-excluded from per-PR discovery under enforcement_coverage_exclusion_note. A census-only module whose only witness is offline is a structural blind spot for the re-signature class: neither the compile nor the floor sees it. On this PR the review was the only mechanism that did.

Evidence, by execution

• dag/test/claim/exact_witness_admission_witness_test.dag — 9/9 PASS. Discriminating RED plus a file-grain control so the sibling claim cannot pass vacuously; duplicate-row and non-executing-cadence controls.
• cli_run.rs witness_admission unit tests — 6/6 PASS, including the host-side discriminator against synthetic source and a population-independent companion (no live known-red admission uses the file-grain form).
• witness_exclusion_reconciliation_test 8/8 · witness_admission_test 15/15 · ci_floor_plan_witness_test 31/31 · floor_discovery_hand_rust_equivalence_witness_test 23/23 · proactive_verification_ledger_witness_test 1/1.
• Whole-tree --target dag compile: 4 hard diagnostics, identical to the same compile on main (434e217) run in a clean worktree with the same binary — pre-existing unresolved type 'Empty' rows in 06_translate.dag, unchanged by this PR.

— sent from calm-bee-513

[gunbai-bot]

review 47781 — confirmed and fixed in f8029b9.

v2.lens.enforcement.inventory cadence_scheduling_rows_for_witness was calling witness_row_excluded_from_discovery(entry: entry) after the function gained its function parameter. function was already in scope there; it is now threaded through, so the lens inventory and floor_discovery_producer ask the same question at the same grain. You were right that this is wall (4)'s own invariant, not just an arity slip — two readers disagreeing about grain is the thing the wall says cannot happen.

Verified by execution rather than by typecheck alone: enforcement_inventory_witness_test.dag 10/10 PASS, which is the witness that actually reaches the repaired caller.

Worth recording why neither my whole-tree compile nor CI would have caught it. src/v2/lens/enforcement/inventory.dag sits outside the compiled import closure — the --target dag compile reports it among the 1180 census-only modules, which are name-censused and not typechecked — and its witness is corpus-denominated and path-excluded from per-PR discovery under enforcement_coverage_exclusion_note. A census-only module whose only witness is offline is a blind spot for exactly the re-signature class. On this PR the review was the only mechanism that saw it.

Also in the same push: main's #7709 climbed the qualified-leaf quarantine out, so its admission row is deleted here (known-red admissions 18 → 17), the same one-row deletion #7688's seed-honesty climb needed one merge earlier.

— sent from calm-bee-513