Context

The README's lead example (line 38) states:

Division by zero is not a runtime error — it is a type error. The compiler checks every call site to prove the divisor is non-zero.

The implementation does not match this unqualified claim. Given:

public fn divide(@Int, @Int -> @Int)
  requires(true)
  ensures(true)
  effects(pure)
{
  @Int.1 / @Int.0
}

vera verify reports OK: divide.vera. Verification: 2 verified (Tier 1) — both trivial contracts pass and the unguarded division stands. The trap fires at runtime, not at verify time.

The same applies to % (modulo) by zero, array indexing past the end, and any other primitive operation whose well-definedness depends on operand values.

The mental model in user-facing docs is "if it compiles, the divisor is provably non-zero." The actual mental model is "the verifier checks the contracts you wrote. If a primitive operation can trap and you have not guarded it with a contract or refinement type, the verifier will not synthesise a guard for you."

What this issue tracks

The implementation work of making the docs claim true: auto-inject latent preconditions on primitive operations.

For every @Int.a / @Int.b in a function body, the verifier should add @Int.b != 0 as an implicit obligation discharged from the function's precondition or by Tier 1 reasoning. Same for %, array indexing, and any other potentially-trapping primitive.

The docs-only fix (softening the README/spec language to match the current implementation) will land in a separate immediate docs PR. This issue tracks the ambitious version.

Scope

Primitive operations whose well-definedness depends on operand values:

Related

• Implement Tier 2 verification (Z3-guided with hints from assert/lemma) #427 — Tier 2 verification (this work is Tier-2-adjacent; the obligation discharge often requires reasoning beyond the current Tier 1 decidable fragment, particularly for array indexing where the index expression involves a function call)
• Nat subtraction silently underflows to negative i64 — refinement-type soundness hole #520 — @Nat subtraction underflow obligation (the existing precedent for this pattern; the codegen guard + verifier obligation discharge is already in place for Nat subtraction)
• Generalize @Nat invariant check to all binding sites (broader generalisation of #520) #552 — Generalise @Nat invariant check to all binding sites (related; both items are about auto-discharging obligations the user didn't write)

Suggested approach

Extend the obligation-discharge infrastructure used by #520 (vera/verifier.py::_walk_for_subtraction_obligations) to handle the other primitive operations. Each one gets its own obligation collector. The discharge path is the same: try Tier 1 with the local context (preconditions, decreases, in-scope path conditions); if that fails, emit E501-class or new E5xx codes pointing at the missing precondition.

The codegen-side guards already exist for many of these (division/modulo trap on hardware; array index trap is checked at compile time when index is a literal, runtime otherwise). What's missing is the static obligation.

Estimated effort

Open-ended. Single-primitive prototypes (just division) are 1–2 days following the #520 template. The full sweep is 1–2 weeks of careful work + spec language.

Origin

Surfaced by a strategic compiler review on 2026-05-18 (v0.0.155). The README claim has been load-bearing marketing for the language differentiation from "normal contract languages"; making the implementation match is the principled long-term move. The docs-softening fix lands separately to avoid the worst-of-both state.