Summary

@Nat subtraction silently underflows to a negative i64. The type system accepts @Nat - @Nat : @Nat and the codegen emits a plain i64.sub — no runtime check, no promotion to @Int. A @Nat local can hold a negative value at runtime despite the type's claim that it represents non-negative integers. This is a soundness issue with the refinement type system, not just a documentation gap.

Reproducer

public fn test_underflow_trap(@Nat -> @Nat)
  requires(true) ensures(true) effects(pure)
{
  @Nat.0 - 1
}

public fn main(@Unit -> @Int)
  requires(true) ensures(true) effects(pure)
{
  -- Pass 0 to underflow-prone subtraction; type system allows it,
  -- runtime returns -1 bound to a @Nat local.
  let @Nat = test_underflow_trap(0);
  nat_to_int(@Nat.0)
}

vera check ✅
vera verify ✅ (the requires(true) ensures no contract objection)
vera compile ✅
vera run prints -1.

The @Nat local holds a negative value. Any downstream code that relied on the Nat >= 0 invariant to reason about correctness now has a silent bug.

Why this matters

Vera's core selling point is contract-verified code with refinement types that the compiler checks at the border between user code and helpers. When a type system promises "this value is non-negative" and the runtime produces a negative value in that slot, every contract that transitively depends on that invariant is undermined — including contracts the verifier proved sound under the (now violated) assumption.

Concretely: an ensures(@Nat.result < array_length(arr)) contract on a helper that internally does @Nat.0 - k with an insufficient precondition can pass the verifier (Tier 1), compile, and still produce an out-of-bounds access at runtime via the negative-@Nat path. The Array.[...] indexing operator trusts its @Nat index not to be negative; a negative @Nat therefore becomes a memory-safety concern on top of a logical correctness one.

Discussion: which semantics should Vera adopt?

Four reasonable choices, each with precedent:

1. Runtime trap on underflow (Rust u64::checked_sub + panic, or .unwrap() default). Straightforward; minimal compile-time disruption; programs crash loudly on the bug instead of silently. Adds one compare-and-branch per @Nat subtraction.

2. Saturating semantics (a - b = max(0, a - b)). Documented, still type-safe, cheaper than a trap at run time. Surprising to the reader unless clearly stated.

3. Promote to @Int (@Nat - @Nat : @Int). Reflects the mathematical reality that Nat isn't closed under subtraction. The callee has to handle the signed result explicitly, often via a contract or conversion. Maximally safe but invasive — every subtraction site needs to be re-typed.

4. Reject without a proof that the result is non-negative. The verifier would need to prove @Nat.b <= @Nat.a at each subtraction site or the compile fails with a Tier-1 contract error. Closest to Vera's existing contract philosophy; closes the soundness hole at compile time rather than runtime; forces the user to think about the subtraction at every site.

Option 4 feels the most Vera-native — contract-driven, compile-time, no runtime cost. Option 1 is a reasonable Tier-3 fallback for cases where the verifier can't discharge the proof.

Related edge cases to decide alongside

• @Nat division by zero currently traps at WASM level (wasm trap: integer divide by zero). Documented here for context — same class of "refinement invariant not checked at run time" issue, different direction (here the type doesn't promise anything, but the trap is opaque; see Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516).
• @Int overflow: probably WASM wrap but undocumented.
• Float64 NaN / infinity in contracts: already handled (Tier 3 runtime check).

Scope

• Language-level decision: pick one of the four options above. Probably worth a spec section discussing the trade-offs.
• Checker change: implement the chosen enforcement.
• Test: conformance test that pins the chosen semantics.
• SKILL.md: document the chosen semantics under "Arithmetic edge cases" (see SKILL.md documentation gap inventory (follow-up to #518) #519 item 5).

Not in scope

• @Int overflow semantics (same class of question but different direction; separate decision).
• The divide by zero error message (that's Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516).