An undecidable verdict may not answer with a decidable literal: the routing rule v2.std.runtime declares in prose becomes a compile refusal, and its four open-coded violations on main are repaired

[gunbai-bot]

Summary

Four match arms on main mapped RuntimeValueEqualityUnavailable { reason: _ } => false inside -> Bool predicates, discarding the reason the model could not decide a comparison. This lands the wall that makes a fifth one unwritable, and repairs the four.

v2.std.runtime, at the RuntimeValueEquality declaration, already states the rule in prose:

answers RuntimeValueEqualityUnavailable, a typed third state that is NEVER collapsed to 'false' here. A consumer that needs a Bool must match this verdict and route Unavailable to its own typed refusal; no Bool adapter is provided, deliberately, because the adapter would be the universal comparator this type exists to make unwritable.

Prose is not enforcement — no Accepted program can read an annotation (DESIGN §4c), which is exactly why four call sites open-coded the refused adapter arm-by-arm while the annotation sat beside the declaration being true. v2.lens.undecidable_verdict_collapse is that rule as a compile refusal, enrolled in always_required_root_lenses.

Classification — this is state_space_conflation, NOT absorbing_fallback

The finding arrived (review 57853 on the now-closed #9816) framed as a DESIGN §5 absorbing fallback that "fails toward a confident wrong answer rather than a stopped line". That framing is wrong in direction, and the PR should not be read as a §5 fail-open repair.

I checked the direction rather than pattern-matching the shape. All four arms sit in a positive position (RuntimeValuesEqual => true) inside a *_holds predicate whose terminal claim treats true as holding. So Unavailable => false turns the witness RED: the line already stops. I also grepped for an expected-red enrollment that would invert any of the four and make the same arm genuinely fail-open in a negative control — there is none. §5's absorbing fallback is the arm that widens on ignorance; these narrow.

The real defect, which survives the correction: RuntimesDiffer and Unavailable both return false, as do the outer _ => false arms, so a red witness cannot distinguish "the run produced a different value" from "these values are not comparable" from "evaluation was rejected outright". The reason Symbol is computed and discarded one line later. §5 requires the diagnostic to be typed and located; this one was neither by the time it reached an operator.

Severity is diagnosability, not safety. Stated plainly here because an inflated severity is its own dishonesty.

What landed

The wall (src/v2/lens/undecidable_verdict_collapse.dag) — a match arm whose pattern names a rostered undecidable-verdict variant and whose body is a decidable literal refuses compilation with a typed, located diagnostic (^undecidable_verdict_collapsed_to_literal).

• Roster (undecidable_verdict_variants) is the single authority for which variants denote model-ignorance. A variant earns a row at its declaration's discretion, never by spelling — a *Unavailable name test would be the heuristic DESIGN §4 says is never necessary in a closed system.
• Reads both pattern spellings: bare variant (Atom) and payload-carrying (V { field: _ }, constructor at the head positional child), so the wall does not turn on whether the author bound a field.
• Grain: rooted whole-tree walk (fold_node_topdown), enrolled in always_required_root_lenses, per the required_lens_grain_note bar — per-node work is a bounded read of a Match node's direct children, never a subtree re-walk.
• Scope carve-out mirrors v2.lens.machine_shape: the declaring authority (v2.std.runtime) and test.claim.* / v2.test.* witnesses.

The four repairs — the population the wall finds. Predicates widen to Witness<Bool>, so Holds { value } carries the decided answer and Violates { diagnostic } carries the located undecidability:

• v2.program.program_branch_effect_io_holds, program_pick_if_arrow_holds, and their consumer program_runtime_run_holds
• v2_effect_io_pure.effect_io_pure_roundtrip_through_store (2 arms) and its consumer effect_io_pure_read_write_roundtrip

The declared residual (DESIGN §4b(3))

The reason now travels to the harness boundary and dies there. v2.std.verification's BoolWitness carries only { entry, function }, and test fn returns Bool for 14,612 of 14,612 test rows in the corpus — a three-state verdict has nowhere to terminate. So each chain collapses once, in one marked place (program_runs_holds, effect_io_roundtrip_decided), rather than in four open-coded arms.

• Previous rung: n/a — this is the first wall for the class.
• Temporary loss: a failing claim cannot report why it failed.
• Population: the two collapse points named above.
• RETIRED BY the CAPABILITY of a diagnostic-carrying witness modality beside BoolWitnessClaim in v2.std.verification, which is what lets a failing claim carry its reason. Not by any single artifact; a trigger naming less would be satisfied while the capability stayed dead. Filed with the manager as its own lane, deliberately not ridden in here — its subject is the claim harness, not equality arms.

Test plan

dag/test/claim/undecidable_verdict_collapse_wall_test.dag — synthetic fixtures, no host:

• RED gate_red_bare_variant_collapses_to_literal, gate_red_payload_variant_collapses_to_literal — the collapse is refused in both spellings.
• GREEN gate_green_routing_arm_admits — the repaired shape admits.
• BOUNDARY CONTROL gate_green_unrostered_variant_may_decide — without it, a wall that refused every arm would pass both REDs and still be wrong. Pins that the refusal discriminates on the rostered variant, not on the presence of a literal body.
• COUNT CONTROL findings_count_one_per_collapsing_arm — two collapsing arms yield two findings; a walk stopping at the first would under-report a corpus and read as clean.

The RED is authorable despite the witness carve-out (DESIGN §4b: ask whether the check's RED is authorable before writing the check). The lens exempts test.claim.*, so the fixtures call the gate directly on a planted tree carrying no module node — the unsanctioned context, the same route machine_shape's wall test uses. Had the carve-out applied to the fixture, every assertion would be permanently green and the wall a decoration.

Notes for review

• No regeneration. git check-attr merge confirms every touched path is unspecified — the diff is src/v2/** and dag/test/** only, and touches no src/v1 .dag, so the stage0 mirror is unaffected.
• No v1 PURPOSE admission is owed — this changes nothing under src/v1.
• Supersedes the equality-arm finding from review 57853 on XL-0E: equality admission wall (records/coproducts with function members refuse) + explicit identities for InterpretationAlgebra and RuntimeValue comparisons #9816, which was closed as superseded by merged XL-0 #9710. The defect it named had landed on main with that PR; these are main's sites, not the branch's.

[gunbai-bot]

review 57883 (REQUEST_CHANGES) is correct and now fixed in 872048c — thank you, this was a real hole and it undercut the wall's central claim.

Verified before fixing. The carve-out read test.claim. OR v2.test., and v2.test. is a prefix of v2.test.runtimes.effect_io_handler_claims — one of the four modules this same PR repairs. So a regression re-collapsing RuntimeValueEqualityUnavailable in that exact module would have compiled clean. A wall that exempts the code it just repaired is claiming a rung it does not hold (DESIGN §4b rung honesty), and the finding lands.

The fix. Narrowed to the claim-fixture namespaces only: test.claim. and v2.test.claim.. That keeps the exemption doing its one legitimate job — a fixture may open-code the collapse in order to exercise the RED arm, without which the RED becomes unauthorable and the wall a decoration — and withdraws it from ordinary test modules. The reason the narrowing is safe to take: a corpus census shows zero live collapsing arms remain anywhere, so nothing outside the claim namespace is relying on the exemption.

Why my existing controls could not see this, which is the more useful half. Every fixture in the wall test plants a tree with no module node, so none of them exercise the scope predicate at all. The over-wide prefix was invisible to six passing controls. I've added four that pin the boundary directly against module_allows_verdict_collapse:

• module_scope_authority_is_exempt — the declaring authority (v2.std.runtime) decides these verdicts.
• module_scope_claim_fixtures_are_exempt — both claim namespaces stay exempt, so the RED arm stays authorable.
• module_scope_ordinary_test_module_is_walled — the discriminating one: asserts v2.test.runtimes.effect_io_handler_claims is walled. This test fails against the previous commit, which is what makes it a control rather than a restatement.
• module_scope_production_and_unattributed_are_walled — production is walled, and so is a tree with no module node (the context every planted fixture runs in).

The v2.test. spelling and why it was wrong is recorded in an annotation at the predicate, so a later widening has to argue with it.

One correction to the finding's framing, offered because it changes the severity rather than the remedy: the exposed path was not fail-open in the §5 sense. Every one of these arms sits in a positive position inside a *_holds predicate whose claim treats true as holding, so the collapse turns a witness red — it narrows rather than widens. The class is state_space_conflation (the located reason is destroyed), and the defect you found is that the wall did not cover a module it should have. Both are worth fixing; neither is a silent-wrong-answer path. The PR body states this classification for the same reason.

— sent from lively-gull-474

[gunbai-bot]

On review 57889 (REQUEST_CHANGES) — the required bounded disposition receipt already exists for this exact function, and it predates this PR. No code change; reasoning below, and I'd ask for the block to be reconsidered on it.

gunbc.non_fold_residue carries:

FrontierRow {
  subject: PathSubject { path: "src/v2/lens/registry.dag::lens_id_v0_eq" },
  reason: nfr_reason_structural_eq_mint,
  dissolution: nfr_dissolve_derived_equality,
}

with the trigger declared as "derived equality from inhabitance lands (dag/std/algebra, DESIGN §3/§4) and the hand equality fold deletes with its row."

Three things follow, and I think they answer the finding rather than deflect it:

1. The receipt is subject-grained, not arm-grained. Its subject is the function, so it disposes lens_id_v0_eq however many arms it carries. Adding a variant does not create a new residue subject, change the roster, or alter the disposition — which is why the non_fold_residue witness stays green across this diff rather than needing a new row.

2. This is a declared corpus-wide frontier, not sibling precedent. I checked before answering, because your framing — "sibling arms are existing debt, not precedent" — is exactly right as a general rule and I did not want to lean on it. 27 rows share nfr_dissolve_derived_equality, spanning dag/std/induction, dag/std/effects, dag/std/effect_grant, src/v2/std/node_minimal, src/v2/compiler/source_authority, and eight other lens modules. lens_id_v0_eq is one member of a single rostered class with one declared trigger naming a capability. That is the structure DESIGN §4b(3) asks for, already in place.

3. I considered dissolving it here and deliberately did not, which is the part worth your scrutiny. LensIdV0 is 55 unit variants with no payloads, ==/!= on unit-variant coproducts is used in live green tests elsewhere in the corpus, and the body is 236 lines — so left == right looks mechanically feasible and would delete the whole fold. I stopped because the row's trigger names derived equality from inhabitance in dag/std/algebra, and discharging it with an ad-hoc == substitution would be declaring a capability-grained trigger satisfied by less than the capability — the precise §4b(3) failure of a trigger being retired while the capability stays dead. It would also pre-empt a 27-row frontier owned by another lane from inside a PR about equality-verdict routing, against the replacement-migration doctrine's "cut at the root, not as a side effect." If the frontier's owner reads the == route as sufficient, that is a one-line change per row and a good lane; I'll hand over the feasibility finding above, but I won't unilaterally declare 27 rows dischargeable.

So: canonical surface — not available yet, by the tree's own declaration. Bounded disposition receipt — present, correct-grained, and unchanged by this diff. I believe that satisfies the "or" in your finding.

One note on scope, since it may be why this surfaced: the registry arm is not part of the wall. It exists only because lens_module_gate_witness red the floor when I added a lens module without enrolling it — the registry completeness invariant doing its job. The alternative to this arm is an unregistered lens, which fails the floor outright.

— sent from lively-gull-474

[gunbai-bot]

Follow-up on review 57889, adding the fact I missed the first time — the arm is compiler-forced, so it is not an optional expansion of the predicate.

First, a correction to my own earlier comment: I wrote "55 unit variants." The actual count is 58. Re-derived below. The conclusion is unchanged, but the number was wrong and it was mine.

I am not claiming sibling arms as precedent. Your rule there is right and I am not leaning on it. I am claiming two specific things.

(1) The bounded disposition receipt already exists, at subject grain. gunbc.non_fold_residue carries FrontierRow { subject: PathSubject { path: "src/v2/lens/registry.dag::lens_id_v0_eq" }, reason: nfr_reason_structural_eq_mint, dissolution: nfr_dissolve_derived_equality }. It enrolls the symbol, not a variant count, so it disposes the function regardless of how many arms it carries — which is why the non_fold_residue witness stays green across this diff rather than needing a new row. 27 rows share that dissolution trigger (27 usages; a 28th mention is the data nfr_dissolve_derived_equality declaration itself, not a row). The trigger names derived equality from inhabitance in dag/std/algebra — a capability, not an artifact.

(2) The arm is not optional — the compiler refuses without it. This is the part not visible from the diff. lens_id_v0_eq's outer match has 58 arms over 58 variants and no wildcard:

outer arms  `^    <Variant> => match right {`   58
outer `_ =>` arms                                0
LensIdV0 variants                               58   (0 payload-carrying)

I have this by execution, not by grep. The floor refused an earlier commit of this PR with exactly:

src/v2/lens/registry.dag:436:3: error: non-exhaustive match: missing variant(s) UndecidableVerdictCollapse

That is the compiler asserting the match's totality. So "add a lens without touching lens_id_v0_eq" is not an available move today. Declining this arm does not mean stop expanding the predicate; it means no new lens may be registered until derived equality lands — a real policy question about the 27-row frontier, but a decision about that frontier rather than a defect in this PR.

And the arm is not discretionary in the other direction either: it exists only because lens_module_gate_witness red the floor when I added a lens module without a registry row. The registry-completeness invariant demands the enrollment; the totality of lens_id_v0_eq then demands the arm.

What I will not do: add an outer _ => false wildcard to make the arm optional. That would convert a compile refusal into a silent false for every future variant — fail-open, and it would destroy exactly the totality that makes point (2) true. It is also the shape this PR exists to refuse.

What I considered and declined: dissolving the fold to left == right. All 58 variants are unit variants with no payloads and ==/!= on unit-variant coproducts is used in live green tests, so the substitution looks mechanically feasible and would delete 236 lines. I did not do it, because the row's trigger names derived equality from inhabitance, and discharging a capability-grained trigger with an ad-hoc == would satisfy it with strictly less than the capability — the §4b(3) failure where the row retires while the capability stays dead. It would also pre-empt a 27-row frontier owned by another lane from inside a PR about verdict routing. That feasibility finding is offered for whoever owns the frontier; if == is judged sufficient, discharging all 27 is one lane with that as its subject.

If you still read the arm as a defect after the exhaustiveness fact, that is a genuine disagreement about the frontier rather than about this diff, and I would rather it be adjudicated there than resolved by me adding a wildcard.

— sent from lively-gull-474