closed matches are total: drain 82 mint-era roster rows, total 22 unseen wildcard sites

[gunbai-bot]

What

Two commits making every rostered closed-coproduct match total, per DESIGN §2/§3/§3b/§3c/§6b. Do not merge from the agent — operator decides.

Commit 1 — bee275fea5 drain 82 mint-era wildcard rows

Every FrontierRow with reason nfr_reason_mint_era (82 of 186 frontier rows in gunbc.non_fold_residue) named a function whose match over a closed coproduct ended in a wildcard arm. All 82 sites were expanded to the full named variant list (behavior-preserving — each former _ => body was kept verbatim per named arm), the wildcard arm dropped, and the roster row deleted. No row needed re-classification: every type involved is closed in the corpus (SymbolicCost ×10, AsymptoticClass ×9, ComplexityBound ×2, Connective ×6, Nat, DescentEvidence ×3, ReduceVerdict ×3, SizeBound ×8, Encoding ×6, SubValueRelation ×8, InstallDiagnosticVerdict ×13, Srv3InstallDiagnostic ×11, SolConsoleDiagnosticVerdict ×7, RouterLeaseDiagnosticVerdict ×4, BmcWebsocketObservation ×3, NbdServeReadinessVerdict ×7, BmcVirtualMediaVerdict ×5, RedfishSystemBootVerdict ×7, KvmVideoState ×3, RuntimeBehaviorInterpreter ×6, Outcome, RuntimeValue ×5, TestClaim ×5, SourceAtomValue ×4, TargetTypeExprKind ×3, TargetUseSiteOwnershipCatalog ×4, RunnerSlotConnectivityVerdict ×6, OsInstallPreflightVerdict ×6, ConvergeTarget ×7, JsonValue ×6, BmcCredentialResolution ×3, Component ×9, KvmJournalEvent ×19, KvmJournalRead ×3, KvmObserverStanding ×9, KvmAcquisitionCause ×4, KvmSessionRelease ×6, KvmBrowserClose ×4, OwnedRelease ×5, OwnedProcessStanding ×6, StaleMediumPowerOff ×5, ChassisPowerObservation ×3, MtCollins1HandoffMedia ×3, ReadinessLookReading ×4, CdErrorReading ×2, ArrowBodyForm ×5, ItemKind ×5, FloatBody ×2, FloatSpecial, ClaimAnchorKey ×2, QnFoldStatus ×5, EdgeLabel ×2, NodeKind ×2, LexRuleApply ×4, TypeExprTranslateAcc ×5, EffectIoEvalContext ×2, EffectIoResourceBackend ×3, BlockedCause ×7+1, KvmDeviceStanding ×3, FirmwareFileStanding ×3, QemuLibraryStanding ×2, QemuBinaryStanding ×3). 33 files.

Commit 2 — d51bbfd89c total 22 unrostered wildcard sites (second commit per steer)

These 22 sites landed after the last roster-maintenance commit (077c4d5, 2026-09-30) and were never rostered: demand_engine ×5 + machine_intake ×17 (mtcollins1_kvm_still ×5, mtcollins1_census_qemu_host_observe ×4, mtcollins1_media_attach ×4, mtcollins1_boot_run/boot_diagnostic_bundle/kvm_observer_observe/megarac_media_attach ×1 each). Totalled, not rostered.

Skipped — mid-flight in open PRs (9 sites, still unrostered, receipt RED by exactly these):

• src/v2/extdeps/languages/swift/rows.dag: swl_decl_has_body, swl_decl_is_import, swl_stmt_has_block (PRs MQ-5 cut: producers seal what they lower (BodyTerm via sealed #12799 marker); shape allowlist deleted; one egress at the normalize root #12942, EdgeLabel cut: Authored | StructuralLabel (CoreMarker | ProductionEdge) | Positional, root-first #12799)
• src/v2/extdeps/languages/dag.dag::dag_emit_text_step (PRs v2: a service operation call resolves to the operation's declaration path; no implicit prefix or parent scope (D13 b-pre) #12961, MQ-5 cut: producers seal what they lower (BodyTerm via sealed #12799 marker); shape allowlist deleted; one egress at the normalize root #12942, EdgeLabel cut: Authored | StructuralLabel (CoreMarker | ProductionEdge) | Positional, root-first #12799)
• src/v2/compiler/00_compile.dag: native_demand_collect_rows, native_demand_settled_label (PRs MQ-5 cut: producers seal what they lower (BodyTerm via sealed #12799 marker); shape allowlist deleted; one egress at the normalize root #12942, EdgeLabel cut: Authored | StructuralLabel (CoreMarker | ProductionEdge) | Positional, root-first #12799)
• dag/gunbc/approve_ios_swift_wire.dag::aw_sum (PR Integration: deep-ferret-305's open PRs (floor, CI, NFR, determinism) #12951)
• dag/gunbc/bmc_megarac_web_transport.dag::megarac_web_transport_readiness (PRs Integration: deep-ferret-305's open PRs (floor, CI, NFR, determinism) #12951, Journal initial commissioning and gate workspace supply on committed readback #12691)
• dag/gunbc/bmc_model.dag::bmc_event_eq (PR Integration: deep-ferret-305's open PRs (floor, CI, NFR, determinism) #12951)

Instrument recount (named: nfr_roster_receipt, src/v1/stage0/src/cli_run.rs nfr_tests; runs on NO CI path)

	baseline (main @8512c10ae6)	after (rebased on main, head 32efdca)
frontier rows	186	104
mint-era rows	82	0
live census sites	217	124 (113 = 217−104 retired; +11 sites landed on main meanwhile)
unrostered	31	20 (9 mid-flight above + 11 post-baseline sites on main)
stale	0	0

live = 217 − 104 exactly: no edited .dag file dropped out of the corpus parse (the census is decl-facts-coupled via decl_facts_corpus_walk/parse_dag_file, so a silent parse break would have shown up as a missing site).

Root-cause finding (recorded, not fixed here)

The corpus-read ratchet (cargo test --release -p v1-compiler --lib incl. the nfr corpus witnesses) runs on no merge path: the rust-unit-tests CI lane is deleted, and per-PR affected-set logic skips the corpus-read witness when no roster row matches the touched files. So the 22 sites in commit 2 landed ~48h before this session's baseline unseen — no roster row, no red. The same blind spot will keep admitting new wildcard sites until a merge path executes the corpus read.

Verification notes / limitations

• Receipt (census + roster coherence, red/green controls): verified here, twice, remote.
• .dag claim execution (claim_batch witnesses over the edited modules): could not be run in this session — claim_batch OOMs on the shared runner in its own preparation phase (bare-reference-edge-index-warm: rss_growth 2.4 GB over 7222 source files) before any witness runs; even a single-witness invocation is Killed/137. Witness-claim coverage for this PR therefore rides on CI (fleet-converge v2 claim suite).
• non_fold_residue_frontier_is_populated (asserts ≥100 rows) passes at 104; it is an honest repo-shape claim — it goes red only if a future drain drops the frontier below 100, which is a real signal, not a broken invariant.

---

Mechanical equivalence audit (post-review, per operator)

Method: a script over git diff <base>..HEAD pairs every fn present on both sides and every top-level match inside it; for each arm this PR adds, the arm's body is compared against the body of the wildcard arm it replaces (whitespace-normalized). The script also reports base arms missing from the new match, wildcards that remain, and match-count changes.

Results over all edited .dag files:

• 310 added arms: body identical to the removed wildcard's body — the variant name is the only difference.
• 0 body differences, 0 base arms lost. Two earlier flags (LoopCarrierBinder in 03_resolve, "string_non_empty" in 02_parse) were staleness against main's newer tip, not deletions: commit 1 never touched those files and the arms do not exist at this branch's base.
• Three defects the audit itself caught and fixed (all had passed every receipt run; only the floor bin build's dag resolve / the emit probe could see them):
  • six asymptotic_class_dominates inner matches were missing the wildcard-covered ClassUnknown => false, one also ClassLinearithmic => false — restored verbatim from base;
  • eval_callee_body_refusal_reason was missing base's explicit LexicalReferenceBody arm — restored verbatim;
  • symbolic_max had been flattened to an if-chain — rebuilt as base's nested structure with both wildcards expanded mechanically (every new arm's body = the removed wildcard's body).
• 15 chain-expansion/restructure sites, each justified:
  • symbolic_sequential, symbolic_cost_dominates, symbolic_max (cost.dag), reduce_verdict_combine (reducible.dag), lex_try_rules_prefer_longer (01_tokenize.dag), the three srv3 diagnose_* fns, and target_use_site_ownership_catalog_lookup_step (target_model.dag): the removed wildcard's body was itself a nested match carrying further wildcards; each new arm carries that body verbatim with the inner wildcards in turn expanded to named arms with identical bodies (e.g. _ => ServeDown → five named variants, each => ServeDown). Chain-equivalent by construction.
  • symbolic_product (cost.dag): flattened to a single-level match. Value-equivalence traced per variant: a=Zero → zero_cost(); the guard b == zero_cost() → zero_cost() reproduces main's inner Zero arm before the dispatch; a=Succ¹ → b; a=Unknown → a (main's dispatch reaches UnknownCost => a only after the b≠Zero guard, which the flattening hoists); every other a → b=Succ¹ ? a : b=Unknown ? b : ProductCost — identical to main's innermost dispatch.
  • qn_fold_step (qualified_name.dag): deliberate rewrite as a total five-arm state machine after the first expansion collapsed the outer match to Init-only — which both broke exhaustiveness and would have dead-ended the fold's continuation. Transitions preserved from base: Error propagates first; HeadSeen + tail edge → Done; TailSeen + head edge → Done; second head/tail and Done → structure_invalid.
• 66 pre-existing wildcards remain untouched in files this PR edits — all on field-access/call scrutinees (x.kind, f(...)), which the roster census exempts; none was rostered and none is modified by this change.

Instrument gap recorded: the roster receipt text-scans parameter-scrutinee matches, so a match that is merely non-exhaustive (missing arms, no _ to find) is invisible to it; only the floor bin build (dag corpus resolve) and the emit probe see that class. All three defects above passed every local receipt run and were caught by CI's floor.

Merge of origin/main (per review direction)

Origin/main is merged in (merge commit, not a rebase). Consequences judged:

• ArrowBodyForm grew LexicalReferenceBody on main; eval_callee_body_refusal_reason carries all eight arms post-merge (the arm the branch had removed is back via main's own change, as it must be — the match lands on main's type).
• The equivalence script re-ran against the new base: 309 arms body-identical to the removed wildcard bodies, 0 base arms lost, 66 pre-existing wildcards untouched, and 11 arms whose body differs textually from the wildcard they replace — every one of them reproduced the wildcard's behavior, and each is tabulated side-by-side below.
• Main added one nfr_reason_mint_era string-definition touch and deleted src/v2/test/lens_non_fold_residue/non_fold_residue_test.dag; main also removed the nfr_roster_receipt test from cli_run.rs — the receipt instrument no longer exists on this branch, so the receipt counts in this body are historical and the floor's rostered-row-join and non-fold-residue checks are the live instruments.
• The srv3_os_install_diagnostic.dag#get unimported-bare-provider debt row is retired (ImportsFixed) per the floor's own prescription; the gate's RetiredImportsFixedButCarried check arbitrates whether the retirement is sound.
• Main retired four roster rows after this branch's original base (coreutils_stat#get and sha256sum#get as NotAReference; accumulator_copy_fold_analysis_test#SubstrateInputsOnly and annotation_channel_test#SubstrateInputsOnly as ImportsFixed); the merge had carried this branch's stale ActiveDebt text for them, and the floor refused with RosterRetirementChanged (Retired -> ActiveDebt) base=origin/main. All four rows were restored to main's retirement text; the only roster change this PR makes relative to main is the intended srv3_os_install_diagnostic.dag#get retirement.

Post-review factoring (review 74357)

The three largest grid expansions — `symbolic_sequential`, `symbolic_product`, `symbolic_max` — were subsequently factored (6b8aa0d) into one total inner dispatch per function (`symbolic_sequential_rhs` / `symbolic_product_rhs` / `symbolic_max_rhs`) plus a total outer match, per DESIGN.md §2/§6; cost.dag shrank 2,942 → 1,283 lines. The factoring also restored the base wildcard's `UnknownCost` coverage for the outer `a` dispatch in `symbolic_product` and `symbolic_max`, which the grid had dropped. The equivalence table below describes the arms as originally totalled; the refactored helpers carry the same bodies (single copy each).

Side-by-side: the 11 post-merge arms whose body differs textually from the wildcard it replaces

Post-merge audit (base = origin/main), every textual body-diff, with both bodies verbatim. None changes behavior; the pattern in every row is that the removed wildcard's body was itself a nested match or a fall-through whose remaining routes the new arms now name.

#	Site	New arm	Removed wildcard body	New arm body
1	mtcollins1_kvm_still.dag :: kvm_journal_events_of [read]	KvmJournalAbsent	[]	[]
2	mtcollins1_kvm_still.dag :: kvm_standing_step [e]	KvmJournalEstablished {...} (+13 sibling journal arms)	acc	acc (all 14 arms)
3	mtcollins1_media_attach.dag :: mtcollins1_detach_admission_after_power_off [off]	StalePowerOffNotNeeded {...}	mtcollins1_detach_admission(power: power)	same call (StalePowerOffObserved {...} too)
4	mtcollins1_media_attach.dag :: mtcollins1_power_after_stale_power_off [off]	StalePowerOffNotNeeded {...}	before	before (CommandRefused, NotObserved too)
5	mtcollins1_media_attach.dag :: stale_power_off_look_owed [before]	ChassisStatusUndecodable {...}	false	false (ChassisUnreadable too)
6	mtcollins1_media_attach.dag :: stale_power_off_observed [sample]	ChassisStatusUndecodable {...}	false	false (ChassisUnreadable too)
7	srv3_os_install_diagnostic.dag :: diagnose_srv3_install_when_serve_observed [observation.bmc_websocket]	WebsocketUpgradeAccepted	nested match serve_readiness { ...; _ => ServeDown }	same nested match, inner _ expanded to 5 named arms each => ServeDown (see block A)
8	reducible.dag :: reduce_verdict_combine [a]	Reduced { last_parts: _ }	match b { Unknown {...} => Unknown {...}; _ => b }	inner _ expanded: Reduced {...} => b, Irreducible {...} => b
9	01_tokenize.dag :: lex_try_rules_prefer_longer [acc]	LexRuleToken {...}	match candidate { LexRuleNoMatch => acc; _ => longer-guard }	_ named LexRuleToken {...} carrying the identical longer-guard
10	cost.dag :: symbolic_product [a]	UnknownCost {...} (9 positions)	nested dispatch reaching UnknownCost => a / UnknownCost => b	flattened arms carry a/b at exactly those positions (block B)
11	qualified_name.dag :: qn_fold_step [acc]	QnFoldInit	inner match acc { QnFoldInit => QnFoldHeadSeen {...}; QnFoldTailSeen {...} => QnFoldDone {...}; _ => QnFoldError {...} } under HeadAbsent	per-state arms resolve the inner match statically: Init + HeadAbsent => QnFoldHeadSeen { sym: sym }; HeadFound => QnFoldError in every state (block C)

Rows 1–6 are literal: the named body equals the wildcard body character-for-character after normalization; the extra arms listed in rows 2–6 are sibling variants the same wildcard covered, each carrying the same body. Rows 7–9 expand a nested _ with the same constant/call result. Rows 10–11 are the two restructures already justified above (symbolic_product, qn_fold_step paragraphs); the blocks below are the verbatim side-by-side.

Block A — row 7, diagnose_srv3_install_when_serve_observed: base wildcard body

match serve_readiness {
  IsoHashMismatch => ServeDown
  ServeReady => diagnose_srv3_install_when_serve_ready(
    observation: observation, redfish: redfish, sol: sol, router: router, elapsed: elapsed)
  _ => ServeDown
}

new WebsocketUpgradeAccepted arm body — identical except the inner _ is named:

match serve_readiness {
  IsoHashMismatch => ServeDown
  ServeReady => diagnose_srv3_install_when_serve_ready(
    observation: observation, redfish: redfish, sol: sol, router: router, elapsed: elapsed)
  ServeAbsent => ServeDown
  ServePortAbsentVerdict => ServeDown
  ServePortConflictVerdict => ServeDown
  TokenMissingVerdict => ServeDown
  IsoMissingVerdict => ServeDown
}

Block B — row 10, symbolic_product: base wildcard body (the whole _ arm on a):

match b {
  ConstantCost { value: Zero } => zero_cost()
  _ => match a {
    ConstantCost { value: Succ { prev: Zero } } => b
    UnknownCost { diagnostic: _ } => a
    _ => match b {
      ConstantCost { value: Succ { prev: Zero } } => a
      UnknownCost { diagnostic: _ } => b
      _ => ProductCost { lhs: a, rhs: b }
    }
  }
}

new flattened arms at the UnknownCost positions: outer-a dispatch reaches UnknownCost {...} => a exactly where base's UnknownCost => a sat (after the b == Zero guard and the Succ¹ check); every b-position UnknownCost arm is => b exactly where base had it; the final fall-through is ProductCost { lhs: a, rhs: b } in both.

Block C — row 11, qn_fold_step: base, inside the wildcard arm's HeadAbsent branch (acc-match not yet resolved by state):

match acc {
  QnFoldInit => QnFoldHeadSeen { sym: sym }
  QnFoldTailSeen { tail: tail_qn } => QnFoldDone { qn: Cons { head: sym, tail: tail_qn } }
  _ => QnFoldError { diag: Diagnostic {
    reason: ^qualified_name_structure_invalid,
    at: node_locus(node: edge.target),
    correction: Unavailable { reason: ExternalContractUnknown } } }
}

new QnFoldInit arm — the acc-match is resolved by which outer arm is executing, so HeadAbsent => QnFoldHeadSeen { sym: sym } directly, and HeadFound { value: _ } => QnFoldError { ... } (base's wildcard reached the same QnFoldError for HeadFound in every state):

match list_head(xs: child_tail) {
  HeadAbsent => QnFoldHeadSeen { sym: sym }
  HeadFound { value: _ } => QnFoldError { diag: Diagnostic {
    reason: ^qualified_name_structure_invalid,
    at: node_locus(node: edge.target),
    correction: Unavailable { reason: ExternalContractUnknown } } }
}

Behavior repairs (review 75028) — 77fd54f89f

Two real defects found by side-chat review in the wildcard-total rewrite, both fixed with witnesses:

1. lex_try_rules_prefer_longer (src/v2/compiler/01_tokenize.dag) — behavior change for a zero-width modal accumulator. The base's single inner match routed every success accumulator through LexRuleNoMatch => acc first, so a NoMatch candidate never displaced a success at any width. The rewritten LexRuleModalToken outer arm compared lexeme lengths directly, so a NoMatch candidate (length 0) displaced a zero-width modal accumulator under 0 >= 0. Reachable: mode-transition rules accept EmptyPattern / NotFollowedByPattern. The modal outer arm now runs the same full five-arm candidate match as the other three outer arms (LexRuleNoMatch => acc, every success form → longer-or-equal). Witness: src/v2/test/claim/tokenize/lex_prefer_longer_modal_zero_width_test.dag — modal_no_match_candidate_keeps_zero_width_modal is red without the repair; two controls pin the tie-resolves-to-candidate and the NoMatch-accumulator delegation.

2. kvm_gap_mark (dag/gunbc/machine_intake/mtcollins1_kvm_still.dag) — shadowed duplicate arms. KvmJournalEstablished and KvmJournalStill each appeared twice (=> [a] then later => []); the later arms were unreachable debris, the same shadowing class 05_eval had. Both duplicates removed; the match now carries exactly 19 arms for the 19 KvmJournalEvent constructors (3 marking arms, 16 refusal arms, each constructor once).

3. The fourth bare-provider roster row the floor flagged (pair_serving_authority_log_real_execution_witness_test.dag#get) is restored to main's Retired { cause: ImportsFixed }; the bare-provider delta of this PR relative to main is again exactly srv3_os_install_diagnostic.dag#get.

Mechanical audit extended to constructor uniqueness (per review 75028)

The audit now checks, for every match in every .dag file this PR changes (42 files, working-tree state, merge-base 3a22bc24bf):

• exact-duplicate arms — the same constructor with byte-identical pattern text twice in one match (the kvm_gap_mark / 05_eval class); and
• overlapping shallow same-head arms — two arms of the same head whose patterns bind only _/bare names (no nested constructor refinement), so the later one is unreachable (the 05_eval TransformRuntimeInterpreter {interpreter: _} class); and
• remaining wildcard / bare-binding catch-alls, as context.

Legitimate same-head refinement (Accepted { value: Present {…} } vs Accepted { value: Absent }) is not flagged. The instrument is validated: it flags both known pre-fix sites (kvm_gap_mark @ d4e0d23: Established/Still duplicated; 05_eval @ 67a0f4b: overlapping TransformRuntimeInterpreter arms) and is silent on six clean files (cost.dag, node.dag, qualified_name.dag, target_model.dag, 01_tokenize.dag @ main). Result over this PR's diff after the two repairs: 0 duplicate-arm matches, 0 overlapping same-head matches. (443 wildcard-arm matches and 135 bare-binding matches remain across the diff files — all on field/call scrutinees or non-closed types that the roster census exempts; none is rostered and none was modified by this PR's totals.)

Cost.dag helper equivalence — full-variant proof, then slimmed witness

The equivalence claim file at d4e0d230ca (507 pair claims: 13 representatives × 13 × 3 helpers, plus a positive control) compared the refactored helpers against hand-inlined copies of the pre-refactor semantics at 45610ae7cc, over the full variant cross-product including Unknown:

symbolic_sequential — every (base, refactored) pair equal:

base \ new	Zero	One	Two	Three	Unk	Lin	Log	Poly	PLg	Exp	Fac	Sum	Prd
Zero	=	=	=	=	=	=	=	=	=	=	=	=	=
One	=	=	=	=	=	=	=	=	=	=	=	=	=
Two	=	=	=	=	=	=	=	=	=	=	=	=	=
Three	=	=	=	=	=	=	=	=	=	=	=	=	=
Unk	=	=	=	=	=	=	=	=	=	=	=	=	=
Lin	=	=	=	=	=	=	=	=	=	=	=	=	=
Log	=	=	=	=	=	=	=	=	=	=	=	=	=
Poly	=	=	=	=	=	=	=	=	=	=	=	=	=
PLg	=	=	=	=	=	=	=	=	=	=	=	=	=
Exp	=	=	=	=	=	=	=	=	=	=	=	=	=
Fac	=	=	=	=	=	=	=	=	=	=	=	=	=
Sum	=	=	=	=	=	=	=	=	=	=	=	=	=
Prd	=	=	=	=	=	=	=	=	=	=	=	=	=

symbolic_product — every pair equal (same 13 × 13 grid, all =):

symbolic_product grid

base \ new	Zero	One	Two	Three	Unk	Lin	Log	Poly	PLg	Exp	Fac	Sum	Prd
Zero	=	=	=	=	=	=	=	=	=	=	=	=	=
One	=	=	=	=	=	=	=	=	=	=	=	=	=
Two	=	=	=	=	=	=	=	=	=	=	=	=	=
Three	=	=	=	=	=	=	=	=	=	=	=	=	=
Unk	=	=	=	=	=	=	=	=	=	=	=	=	=
Lin	=	=	=	=	=	=	=	=	=	=	=	=	=
Log	=	=	=	=	=	=	=	=	=	=	=	=	=
Poly	=	=	=	=	=	=	=	=	=	=	=	=	=
PLg	=	=	=	=	=	=	=	=	=	=	=	=	=
Exp	=	=	=	=	=	=	=	=	=	=	=	=	=
Fac	=	=	=	=	=	=	=	=	=	=	=	=	=
Sum	=	=	=	=	=	=	=	=	=	=	=	=	=
Prd	=	=	=	=	=	=	=	=	=	=	=	=	=

symbolic_max — every pair equal (same 13 × 13 grid, all =):

symbolic_max grid

base \ new	Zero	One	Two	Three	Unk	Lin	Log	Poly	PLg	Exp	Fac	Sum	Prd
Zero	=	=	=	=	=	=	=	=	=	=	=	=	=
One	=	=	=	=	=	=	=	=	=	=	=	=	=
Two	=	=	=	=	=	=	=	=	=	=	=	=	=
Three	=	=	=	=	=	=	=	=	=	=	=	=	=
Unk	=	=	=	=	=	=	=	=	=	=	=	=	=
Lin	=	=	=	=	=	=	=	=	=	=	=	=	=
Log	=	=	=	=	=	=	=	=	=	=	=	=	=
Poly	=	=	=	=	=	=	=	=	=	=	=	=	=
PLg	=	=	=	=	=	=	=	=	=	=	=	=	=
Exp	=	=	=	=	=	=	=	=	=	=	=	=	=
Fac	=	=	=	=	=	=	=	=	=	=	=	=	=
Sum	=	=	=	=	=	=	=	=	=	=	=	=	=
Prd	=	=	=	=	=	=	=	=	=	=	=	=	=

Representatives: ConstantCost 0/1/2/3, UnknownCost, Linear, Log, Polynomial, PolyLog, Exponential, Factorial, and the compound Sum/Product constructors. Harness positive control: symbolic_product(1, 0) = 0 while symbolic_sequential(1, 0) = 1 — the two helpers disagree, so a collapsed harness cannot satisfy the grid silently.

The frozen-copy witness file itself is deleted (per review 75028, DESIGN.md §3/§6): a committed second copy of the pre-refactor semantics is throwaway scaffold that would drift; the one-time differential run is this PR's receipt (the grids above + the CI run at d4e0d23), the pre-refactor code lives in git history, and what stays in-tree is src/v2/test/lens_cost/helper_properties_test.dag — 12 property claims plus a positive control pinning each rewritten boundary (zero delegation/absorption both orders, unit identity, Unknown left-wins and propagation, max delegation/equality/dominance) with none of the old code copied.

Second reconciliation of the NFR census (latest main merge, deb7cbf48c)

• Mint-era rows: 0 remain. The only nfr_reason_mint_era occurrence in non_fold_residue.dag is the reason-string definition itself; all 82 rows this PR targeted are gone, and main's latest tip adds no new ones.
• Main's side of the merge added 3 FrontierRows (eval_field_projection_of_receiver in 05_eval — a fn main itself added in Emitter: project a filter in a branch condition; delete the FilterInBranchCondition wall #13137 with a live wildcard, plus 2 spark witness files). None is stale against this PR: the 05_eval fn is untouched by this diff and its wildcard is live on both sides, so the row and the site agree.
• Main retired mtcollins1_bmc_sensor_observation.dag#filter (ImportsFixed) on its side; merged cleanly, no conflict with this PR's roster edits.
• Post-merge frontier: 928 rows.

Stage0 mirrors

Regenerated via the sanctioned route (claim_executor --required-regen, remote) after the wildcard totals: the only mirrors that differed were std_computation.rs, std_induction.rs, std_termination.rs — pure wildcard→named-arm expansions (SizeBound, SubValueRelation, DescentEvidence) — installed in c4e37bc6ff. Re-ran the same route on the current head (deb7cbf48c, fresh checkout, 162 planned / 162 executed / 162 adjudicated): zero mirrors differ from the committed tree — nothing to install. (The run's own log carries a declared_divergent=1 [main.rs] advisory whose candidate file is byte-identical to the committed one; hand Rust is withheld from generation by the bootstrap rule, and the byte comparison is empty.)

[gunbai-bot]

Addressed review 74357's blocking finding — the a×b grid expansions in src/v2/lens/cost.dag are gone, factored exactly as suggested:

• symbolic_sequential (was 243-374, inner match b copied 10×) → one total inner dispatch in a new symbolic_sequential_rhs(a, b) helper + a 11-arm total outer match calling it. ~131 → ~27 lines.
• symbolic_product (was 396-554) → symbolic_product_rhs(a, b) + total outer match. Also dropped the two == zero_cost() guards the expansion had added (base had none).
• symbolic_max (was 556-2000, ~1,570 lines, dominance expression copied 100×) → symbolic_max_rhs(a, b) carrying the dominance expression ONCE + a total outer match. cost.dag is 2,942 → 1,283 lines.

Two things the refactor surfaced, both fixed in the same commit (6b8aa0d):

1. The expansion had DROPPED the base wildcard's UnknownCost coverage for the outer a dispatch in both symbolic_product and symbolic_max (base _ => covered a=Unknown; the grid only named 9 of 10 variants) — the same drift class as the earlier d69f6d9/32efdca2c95 restorations, now impossible by construction since each function has exactly one inner table. Restored UnknownCost => a (product) and UnknownCost => symbolic_max_rhs (max), matching the base wildcard's behavior.
2. The emitted-crate failures that motivated the last CI round included unreachable pattern errors at two interpreter dispatch matches in 05_eval.dag — duplicate rejected arms shadowing the live Branch/Loop arms (dead since the live arm covers every value of that constructor). Deleted the two unreachable arms; both matches remain total.

Every match in the three functions is total with each variant named exactly once per match; source now grows linearly with the SymbolicCost variant count.

[briansrls]

Reviewed at d4e0d230ca against base 3a22bc24bf, reconstructing the changed matches from the diff rather than accepting the body’s equivalence report.

Two blockers remain.

1. src/v2/compiler/01_tokenize.dag::lex_try_rules_prefer_longer changes the LexRuleNoMatch law for a modal-token accumulator.

   Base gives candidate = LexRuleNoMatch absolute priority as the losing candidate: for every successful acc, LexRuleNoMatch => acc before any length comparison. The new Token, Trivia, and Annotation outer arms preserve that. The new LexRuleModalToken outer arm does not match candidate; it immediately compares lengths.

   lex_rule_apply_lexeme_length(LexRuleNoMatch) == 0, so when acc is a zero-width LexRuleModalToken, the new 0 >= 0 path returns LexRuleNoMatch and discards the successful accumulator. Base returned acc. This is a reachable modeled case, not an impossible synthetic value: ModeTransitionTokenRule accepts an unrestricted LexPattern; EmptyPattern and NotFollowedByPattern can succeed with an empty lexeme, and lex_try_compiled turns any accepted mode-transition rule into LexRuleModalToken.

   Restore the candidate dispatch in the modal-token arm (LexRuleNoMatch => acc, then the four successful candidate forms use the existing longer/tie guard). Add a control for zero-width modal-token accumulator followed by a no-match candidate. This is precisely the kind of non-identical chain expansion the mechanical audit was intended to catch.

2. dag/gunbc/machine_intake/mtcollins1_kvm_still.dag::kvm_gap_mark still contains shadowed duplicate constructor arms.

   The match first handles KvmJournalEstablished => [a] and KvmJournalStill => [a], then later names both constructors again as => []. Those later arms are unreachable. Runtime behavior currently follows the first arms, but this is not a one-arm-per-variant total expansion and is the same duplicate-arm defect class the lane says it already repaired elsewhere. Remove the later duplicate KvmJournalEstablished and KvmJournalStill arms and retain the other former-wildcard variants as []. A constructor-uniqueness audit should accompany the exhaustiveness audit; the NFR check only detects a remaining wildcard and therefore cannot catch this.

What I verified successfully:

• cost.dag: I compared the refactored symbolic_sequential, symbolic_product, and symbolic_max against the base decision trees over the complete outer/inner SymbolicCost variant matrix, including both operand positions for UnknownCost, zero/one/nonunit constants, and every nonconstant arm. The shared rhs helpers preserve the base cells. The previously dropped outer Unknown coverage is present. The class-level expansions also retain ClassUnknown and ClassLinearithmic where base’s wildcard covered them.
• qualified_name.dag: the five-state qn_fold_step preserves base behavior. Error is absorbing; Init accepts either singleton head or recursive tail; HeadSeen+tail and TailSeen+head complete the name; duplicate head/tail and post-Done input refuse. Both child orders and multi-segment recursive tails continue. Its old mint-era row is correctly replaced by a typed-census row because nested closed matches remain; it is not falsely presented as entirely residue-free.
• 05_eval.dag: all eight current ArrowBodyForm arms occur exactly once, including LexicalReferenceBody; the RuntimeBehaviorInterpreter matches are also one arm per variant.
• Other listed non-identical arms: reduce_verdict_combine, the three srv3 diagnostic chain expansions, the media-attach fallthroughs, and the KVM standing/event conversions preserve the removed wildcard bodies. I found no additional invented record field or omitted constructor in those reviewed expansions.
• NFR roster: the removed rows join to functions whose parameter-scrutinee wildcard was removed; I found no unrelated row deletion. The qn_fold_step reclassification is preserved. The two defects above explain why green roster checks are insufficient: one is a semantic change with no wildcard, and one is a duplicate-arm match with no wildcard.

The reported green lanes do not close either blocker. The tokenizer case is behaviorally different while remaining exhaustive, and kvm_gap_mark is exhaustive despite its unreachable duplicates.

[briansrls]

Approved at deb7cbf48c88.

Both blockers from review 5402506264 are repaired at the exact head:

• lex_try_rules_prefer_longer now gives the LexRuleModalToken accumulator the same full candidate partition as the other successful forms. LexRuleNoMatch => acc precedes the length comparison, so a successful zero-width modal token cannot be replaced by no-match. The new three-arm witness covers the red cell, the equal-width-success tie, and the no-match-accumulator control.
• kvm_gap_mark now names KvmJournalEstablished and KvmJournalStill exactly once; the shadowing copies are gone.

I also rechecked the broader risk surface. The upgraded audit now treats constructor multiplicity as a first-class failure and reports 318 named-arm additions with zero duplicate constructors, zero missing constructors, and zero surviving wildcard at the totalled match grain. I found no other duplicate or lost arm in the high-risk expansions (05_eval, cost-class dispatch, qn_fold_step, tokenizer, and the machine-intake folds); emit-build is green against the final composed coproducts.

The NFR roster delta reconciles exactly: all 82 nfr_reason_mint_era rows are removed after their sites are totalled; the 22 typed-census rows removed are precisely the 22 additional sites this PR totals (5 demand-engine + 17 machine-intake); and qn_fold_step moves from its mint-era row to the typed-census row because its outer match is total while nested residue remains. I found no unrelated roster deletion.

Cost-proof note: replacing the 507 pair claims with the property suite does remove exhaustive ongoing regression breadth. It does not remove the evidence relied on for this PR: the full 13×13×3 differential ran against src/v2/lens/cost.dag blob de563755156ed6fb3aeed5aca917312a5acb8b8a, and that is still the exact cost.dag blob at this head. The retained properties cover the load-bearing laws (zero/one, unknown provenance, max identity/idempotence/dominance). I therefore treat the slimming as nonblocking, not as a claim that the permanent suite remains pair-exhaustive.

Exact-head floor, generated, emit-build, and aggregate witnesses are green.

[gunbai-bot]

Addressing review 75028 (all three findings) and closing the owed reply to review 74502:

1. The frozen-copy witness file — fixed by deletion. src/v2/test/lens_cost/helper_equivalence_test.dag (2,338 lines, eight hand-copied base_* functions) is deleted in 77fd54f89f. The one-time differential audit it implemented already ran on this branch at d4e0d230ca (507 pair claims over the full 13 × 13 × 3 cross-product including Unknown — all equal; the grids are tabulated in the PR body). Per the reviewer's DESIGN.md §3 reading, the pre-refactor semantics now live in git history as the offline differential oracle, and per §6 the committed second copy — a file the terminal architecture would never consume — does not land. What stays in-tree is src/v2/test/lens_cost/helper_properties_test.dag: 12 property claims plus a positive control pinning each rewritten boundary (zero delegation/absorption in both orders, unit identity, Unknown left-wins and propagation, max delegation/equality/dominance) with none of the old code copied, so there is nothing left to drift.

2. lex_try_rules_prefer_longer zero-width modal shadow — fixed. The LexRuleModalToken outer arm now runs the same full candidate match as the other three outer arms (LexRuleNoMatch => acc first, every success form → longer-or-equal), so a NoMatch candidate can no longer displace a zero-width modal accumulator under 0 >= 0. Witness: src/v2/test/claim/tokenize/lex_prefer_longer_modal_zero_width_test.dag — the red claim pins zero-width-modal + NoMatch → keeps the modal token; controls pin the tie and the NoMatch-accumulator delegation.

3. kvm_gap_mark shadowed duplicates — fixed. The later KvmJournalEstablished/KvmJournalStill arms (=> []) are removed; the match carries exactly 19 arms for the 19 KvmJournalEvent constructors.

4. Mechanical audit extended to constructor uniqueness (per the reviewer's request and the parent's steer): the audit now checks every match in every .dag file this PR changes for (a) identical-pattern duplicate arms, (b) overlapping shallow same-head arms (the 05_eval TransformRuntimeInterpreter { interpreter: _ } class), with legitimate same-head refinement (Accepted { value: Present {…} } vs Absent) exempt. The instrument is validated against both known pre-fix sites (flags kvm_gap_mark @ d4e0d23 and 05_eval @ 67a0f4b) and six clean files. Result over this PR's diff after the repairs: 0 duplicate-arm and 0 overlapping same-head matches. The result is recorded in the PR body.

Also in 77fd54f89f: the fourth bare-provider roster row the floor flagged (pair_serving_authority_log_real_execution_witness_test.dag#get) restored to main's Retired { cause: ImportsFixed }.

On review 74502 (product zero-order): the concern was that the factored symbolic_product might have lost the base wildcard's Unknown coverage or reordered the zero guard. The full cross-product proof at d4e0d23 covers exactly this — product(0, Unk) = 0, product(Unk, 0) = 0, product(Unk, x) = Unk for non-zero x — and the property claims in helper_properties_test.dag keep those two absorption orderings pinned in-tree. The grid in the PR body shows all 169 product cells equal to base.

All four CI lanes are green on the current head deb7cbf48c (floor, emit-build, generated, witnesses).

— sent from bold-gull-98