Issue #1022: Prover: what a match guard gives its arm (ADR-361 D9)

ready · opened 2026-10-31 · updated 2026-11-03 · 1 comment

Brief. The prover (ADR-361 D9, built for match by cf5bb6f1, #1021) gives each match arm what its pattern says of the matched value. An arm with a guard (n if n < 10 =>) gets nothing from its guard, and the arms below a guarded arm get nothing from it either. ADR-361 D9 says “as the branch it took says” but does not say what a guard contributes. Found by the yaml lane’s y7c report (docs/briefs/yaml/y7c-match-join.md.report.md).

Introduction. A guard is a condition that must hold too, after the pattern matches, for an arm to be taken:

let mut w = 0
match n {
    k if k < 10 => { w = k }      // today: the prover does not know k < 10 here
    _ => { w = 9 }
}
assert(w < 10)                    // today: checked at run time, not proved

Today the guard is walked for its calls only, and a guarded arm’s scope is not exact, so it ends what the arms below learn by elimination. That is safe: it only leaves claims unproved (they stay run-time checks, ADR-361 D4); it never proves something false.

Who needs it now. Nothing. No program in packages/, tools/ or the tests needs a guard’s fact to prove a claim; the yaml lane met it while building #1021, not as a blocker.

Options.

As today, until someone needs more. Pro: no work, no risk. Contra: a guarded match proves less than the same code written as if/else if, an asymmetry a reader may trip on.
The guard holds in its arm (the prover reads it as the if condition of that arm: pattern fact AND guard). Arms below learn nothing from a guarded arm (as today). Pro: matches if; small (the guard is already walked; add it to the arm’s scope the way prover_if adds its condition). Contra: a little more prover work per guarded arm, paid only when a claim reads the names (D2).
Option 2 plus elimination: arms below a guarded arm also get “not (pattern and guard)”. Pro: complete. Contra: a disjunction for non-exact patterns; more prover cost and more code for a case nobody has asked for.

Recommendation. 1 now, recorded as a sentence in ADR-361 D9 (“a guard gives its arm nothing yet”); 2 when a program needs it. If the owner prefers symmetry with if now, 2 (one brief, about an hour of building, a test pair under tests/compiler/tests/prove_*).

To build (option 2, if chosen).

ADR-361 D9 and Part III 14.2: one sentence on what a guard gives.
prover_match in crates/nikaia-std/src/tools/prover_walk.nika: add the guard as a fact of its arm, where the prover reads it; lower the file.
Tests: a guarded arm proves a claim (stdout); a guard the prover cannot read leaves it a run-time check.

Generated by Claude Code

Comments

keywan-ghadami, 2026-11-03

Owner, 2026-11-03: option 3 is the goal, built step by step.

ADR-361 D9 records option 3 as the rule.

To build

A guard holds in its arm (option 2).
- ADR-361 D9 and Part III 14.2: in a guarded arm, the prover knows the pattern fact and the guard. The arms below a guarded arm get “not (pattern and guard)” (step 2); until step 2 is built, they get nothing from it.
- prover_match in crates/nikaia-std/src/tools/prover_walk.nika adds the guard to its arm’s facts, the way prover_if adds its condition. Lower the file.
- Tests under tests/compiler/: a guarded arm proves a claim (stdout), and a guard the prover cannot read leaves the claim a run-time check.
Elimination (option 3).
- The arms below a guarded arm get “not (pattern and guard)”. For an exact pattern this is “not guard”. For a non-exact pattern it is a disjunction, which the prover reads where it can; where it cannot, it reads nothing.
- Tests: an arm proved by the guard above it, and a non-exact pattern that stays a run-time check without a wrong proof.

Generated by Claude Code

Back to Open Issues