Vera version: vera 0.0.138
Origin: Friction surfaced while writing terminal Tetris on Vera 0.0.138.

Problem

Programs maintaining Nat counters (Tetris had a "lines cleared" counter) can't add two Nats without a five-line round-trip:

let @Int = nat_to_int(@Nat.1) + nat_to_int(@Nat.0);
let @Nat = match int_to_nat(@Int.0) {
  Some(@Nat) -> @Nat.0,
  None -> 0    -- unreachable for Nat+Nat, but the compiler can't see that
};

Five lines and an unreachable arm to add two non-negative integers. Most painful gap by frequency.

Proposed (revised after design review)

Two new total built-ins:

• nat_add(@Nat, @Nat) -> @Nat — addition. Result is provably >= 0, so totality is direct.
• nat_mul(@Nat, @Nat) -> @Nat — multiplication. Same.

Both are total (no preconditions, no error path) and the verifier discharges totality directly via the Nat refinement.

Rejected: saturating nat_sub_sat

The friction document proposed a third built-in, nat_sub_sat(@Nat, @Nat) -> @Nat, with saturating semantics (clamp to 0 on underflow). Rejected on design-principle grounds:

Design anchor

Vera's design principles (DESIGN.md) commit to:

5. Contracts as the source of truth. Every function declares what it requires and guarantees. The compiler verifies statically where possible.

and in the technical-decisions table:

Refinement types — { @T | predicate } checked by Z3 — Encode value-level constraints in the type system; rejected statically or at runtime.

The whole point of the Nat refinement is that any narrowing from Int carries a non-negativity obligation that has to be discharged — currently via the explicit int_to_nat match. A saturating nat_sub_sat papers over that obligation by silently losing data on underflow. That trades a writer-visible signal for a runtime-invisible one and inverts the contract-as-source-of-truth principle: the contract no longer reflects what actually happens at runtime when the precondition is violated.

This also runs against principle 2. Explicitness over convenience ("All state changes declared. ... No implicit behaviour") — saturating subtraction is implicit data loss.

Where the right fix lives

#552 generalises the @Nat invariant check to all binding sites — once that lands, narrowing into a @Nat-typed let binding becomes obligation-checked statically (rather than requiring the explicit int_to_nat match), and the @Nat - @Nat case can be reduced to a thin compile-time check. That preserves the obligation's visibility while removing the boilerplate.

If a real driver emerges for nat_sub specifically (rather than for all narrowing positions), it should be a nat_sub_checked(@Nat, @Nat) -> @Option<Nat> — total, signal-preserving — not a saturating variant.

Verification

Both proposed built-ins are total — the verifier discharges totality via the Nat refinement at codegen time.

Origin

Friction document from terminal Tetris experiment; reframed after design review against Vera's refinement-type principle.