# Chapter 6: Contracts

## 6.1 Overview

Contracts are the mechanism by which Vera ensures that code is checkable. Every function declares what it requires from its callers and what it guarantees to them. The compiler verifies these contracts statically where possible and inserts runtime checks where it cannot.

Contracts serve as executable specifications. They are the source of truth about what a function does — the implementation must satisfy them.

## 6.2 Contract Forms

### 6.2.1 Preconditions (`requires`)

A precondition is a predicate that MUST hold when the function is called. It is the caller's responsibility to ensure preconditions are met.

```
public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}
```

At every call site of `safe_divide`, the compiler verifies that the first argument is non-zero — `@Int.1` is the first parameter under most-recent-first indexing (Chapter 3). If it cannot prove this statically, it inserts a runtime check.

### 6.2.2 Postconditions (`ensures`)

A postcondition is a predicate that MUST hold when the function returns. It is the function's responsibility to ensure postconditions are met.

```
public fn absolute_value(@Int -> @Nat)
  requires(true)
  ensures(@Nat.result >= 0)
  ensures(@Nat.result == @Int.0 || @Nat.result == -@Int.0)
  effects(pure)
{
  if @Int.0 >= 0 then {
    @Int.0
  } else {
    -@Int.0
  }
}
```

The special reference `@T.result` (where `T` is the return type) refers to the function's return value within `ensures` clauses.

Postconditions on stateful functions also have `old(State<T>)` and `new(State<T>)`, which name an effect's state before and after the call. Both are specified in Chapter 7, Section 7.9.2. Like `@T.result`, both are valid only inside `ensures` clauses.

### 6.2.3 Invariants (`invariant`)

> **Status: Not yet implemented.** The `invariant(...)` clause on `data` declarations is specified here but is not currently working in the reference compiler — every documented form fails with `[E130] no <DataName> bindings in scope`, because the slot environment for the invariant predicate is not yet wired up.  Tracked in [#686](https://github.com/aallan/vera/issues/686) (successor to the now-closed #560 — that earlier issue was about removing the broken spec examples; the feature implementation is the remaining work).  Until the implementation lands, refinement types (Chapter 2, Section 2.6) are the working alternative for expressing constraints on data values.

An invariant is a predicate declared on a data type that MUST hold for all values of that type:

<!-- vera:skip-check category="INCOMPLETE" reason="is_sorted_impl in SortedArray" -->
```
private data SortedArray
  invariant(is_sorted_impl(@SortedArray.0))
{
  Mk(Array<Int>)
}
```

The compiler verifies the invariant at every construction site. If a value of type `SortedArray` exists, the invariant holds.

Invariants on built-in types are expressed as refinement types (Chapter 2) rather than as `invariant` declarations.

### 6.2.4 Termination Measures (`decreases`)

A `decreases` clause specifies an expression that strictly decreases on each recursive call (see Chapter 5, Section 5.6.1):

```
private fn sum_to(@Nat -> @Nat)
  requires(true)
  ensures(@Nat.result == @Nat.0 * (@Nat.0 + 1) / 2)
  decreases(@Nat.0)
  effects(pure)
{
  if @Nat.0 == 0 then {
    0
  } else {
    @Nat.0 + sum_to(@Nat.0 - 1)
  }
}
```

### 6.2.5 Assertions (`assert`)

An assertion is a predicate that MUST hold at the point where it appears in the function body:

```
fn(@Int, @Int -> @Int)
  requires(@Int.0 > 0 && @Int.1 > 0)
  ensures(@Int.result > @Int.0)
  effects(pure)
{
  let @Int = @Int.0 + @Int.1;
  assert(@Int.0 > @Int.1);     -- compiler verifies this holds
  @Int.0
}
```

Assertions serve two purposes:
1. They document intermediate invariants for human readers.
2. They provide "stepping stones" for the verifier, breaking complex proofs into smaller steps.

### 6.2.6 Assumptions (`assume`)

An assumption is a predicate that the compiler MUST accept as true without proof:

```
fn(@Int -> @Int)
  requires(true)
  ensures(@Int.result > 0)
  effects(pure)
{
  let @Int = external_library_call(@Int.0);
  assume(@Int.0 > 0);   -- trust that the library returns positive
  @Int.0
}
```

The compiler MUST emit a warning for every `assume` statement:

```
WARNING: unverified assumption at line 7: @Int.0 > 0
```

`assume` is an escape hatch. It is unsound — if the assumption is false, the program may have undefined behaviour. It should be used only when interfacing with verified external code or when a proof is beyond the verifier's capability.

## 6.3 Contract Predicate Language

Contract predicates use the same expression syntax as Vera programs, with the following restrictions and extensions.

### 6.3.1 Allowed in All Contracts

Everything allowed in the decidable fragment (Chapter 2, Section 2.6.1):
- Integer literals and slot references
- Float64 literals and values (`1.5`, `-0.5`) — Z3's IEEE-754 binary64 FloatingPoint sort (`FPSort(11, 53)`, round-nearest-ties-to-even), so Tier-1 proofs respect `NaN` / `±Inf` / signed zero / rounding and match the runtime; `==`/`!=` are IEEE `fpEQ`/`fpNEQ` and `%` is the truncated remainder (C `fmod`) (added [#667](https://github.com/aallan/vera/issues/667), made IEEE-sound in [#797](https://github.com/aallan/vera/issues/797)).  Equality on an ADT whose fields transitively include `Float64` decomposes per-field — same-constructor recognizers plus fieldwise `fpEQ` for Float64 fields, recursing into nested Float64-containing ADTs — so the Tier-1 model matches the runtime's structural per-field `f64.eq` (Chapter 9, Section 9.8.2) rather than Z3's structural datatype `=` (under which `NaN = NaN` holds and `+0.0 = -0.0` does not, both wrong at runtime); a *recursive* Float64-containing ADT has no finite decomposition, so its equality falls to Tier 3 ([#871](https://github.com/aallan/vera/issues/871))
- String literals
- Linear arithmetic (`+`, `-`, `*` with literal multiplier)
- Comparisons (`==`, `!=`, `<`, `>`, `<=`, `>=`)
- The `Eq` / `Ord` ability operations `eq(a, b)` and `compare(a, b)` (Chapter 9, Section 9.8) — the generic-programming spelling of `==` and the three-way `Ordering` comparison.  A contract predicate may use either form; `eq(a, b)` is verified and compiled *as* `a == b`, and `compare(a, b)` *as* the canonical `Ordering` if-chain (`if a < b then Less else if a == b then Equal else Greater`).  The two spellings are semantically identical and share one internal representation (one canonical form, Section 0.2.3), so a contract written with the ability op enjoys the same Tier-1 reasoning and runtime enforcement as its operator form ([#874](https://github.com/aallan/vera/issues/874))
- Boolean connectives (`&&`, `||`, `!`)
- `array_length()` on arrays, `string_length()` on strings
- Array index expressions (`@Array<T>.0[i]`) — uninterpreted `index_<T>(arr, i)` function; sound for relational facts but doesn't reason about element structure beyond what explicit predicates assert (added [#667](https://github.com/aallan/vera/issues/667))
- Array literals (`[a, b, c]`) — fresh `Array_<T>` constant with `length(lit) == N` and per-element `index(lit, i) == elt_i` axioms asserted (added [#667](https://github.com/aallan/vera/issues/667))
- Logical implication (`==>`)
- `true`, `false`
- The `@T.result` reference (in `ensures` only)
- Conditional expressions (`if ... then ... else ...`)
- Calls to `pure` functions that have their own contracts — the verifier inlines the callee's contract at the call site

### 6.3.2 Additionally Allowed in Contracts (Tier 2)

> **Status: Not yet implemented.** Tier 2 (Z3-guided) is specified here but not implemented in the reference compiler. Tracked in [#427](https://github.com/aallan/vera/issues/427). Contracts using these constructs currently fall to Tier 3 (runtime check).

Beyond the decidable fragment, contracts may also use:
- Quantified expressions (limited, see below) — `forall` / `exists` fall to Tier 3 today

Note that array element access (`@Array<T>.0[i]`) and array literals (`[a, b, c]`) are NOT Tier 2 — both are Tier 1 with the uninterpreted-function encoding described in §6.3.1 (added [#667](https://github.com/aallan/vera/issues/667)).  Tier 2 is reserved for predicates that the decidable fragment can't decide on its own and need user-provided lemmas (#427).

### 6.3.3 Quantified Expressions

Vera supports bounded quantification in contracts:

```
forall(@Nat, array_length(@Array<Int>.0), fn(@Nat -> @Bool) effects(pure) {
  @Array<Int>.0[@Nat.0] > 0
})
```

This reads: "for all `@Nat.0` in `[0, array_length(@Array<Int>.0))`, the array element at that index is positive."

The syntax is:

```
forall(@IndexType, @BoundExpr, @PredicateFn)
```

The bound is an **integer count** — the quantified index runs over `0 .. bound-1`.  An `@Int`/`@Nat` (or a refinement over one) is required; any other domain type — an array, a string — is a check-time error (**E128**).  To quantify over an array's elements, pass `array_length(arr)` as the bound and index the array inside the predicate.

Where:
- `@IndexType` is the type of the bound variable (must be `Nat` or `Int`)
- `@BoundExpr` is the exclusive upper bound (inclusive lower bound is always 0)
- `@PredicateFn` is an anonymous function returning `Bool`

Bounded quantification with concrete literal bounds is decidable via finite unrolling, and symbolic bounds are decidable via inductive reasoning — but **both reach the decidable fragment only via Tier 2 (Z3-guided)**, which is [not yet implemented](https://github.com/aallan/vera/issues/427). At present every `forall` / `exists` in a contract falls to Tier 3 (runtime check) regardless of whether its bound is a literal, a length expression, or symbolic.

The `exists` quantifier uses the same syntax and asserts that at least one value in the range satisfies the predicate:

```
exists(@Nat, array_length(@Array<Int>.0), fn(@Nat -> @Bool) effects(pure) {
  @Array<Int>.0[@Nat.0] == 0
})
```

This reads: "there exists some `@Nat.0` in `[0, array_length(@Array<Int>.0))` such that the array element at that index is zero."

The syntax is:

```
exists(@IndexType, @BoundExpr, @PredicateFn)
```

Where the parameters have the same meaning as for `forall`. Like `forall`, bounded existential quantification reaches the decidable fragment only via Tier 2 (Z3 with finite unrolling for small bounds, or Skolemization for symbolic bounds), which is [not yet implemented](https://github.com/aallan/vera/issues/427). At present every `exists` in a contract falls to Tier 3 (runtime check).

## 6.4 Verification Architecture

### 6.4.1 Verification Condition (VC) Generation

For each function, the compiler generates verification conditions — logical formulas that, if valid, imply the function satisfies its contract.

The VC generation follows a weakest-precondition calculus:

1. Start with the postcondition.
2. Traverse the function body backward, computing the weakest precondition at each step.
3. At the function entry, check that the declared precondition implies the computed weakest precondition.

For each statement type:

| Statement | WP transformation |
|-----------|-------------------|
| `let @T = expr;` | Substitute `expr` for `@T.0` in the current WP |
| `if @Bool.0 then { e1 } else { e2 }` | `(@Bool.0 ==> WP(e1)) && (!@Bool.0 ==> WP(e2))` |
| `assert(P)` | `P && WP(rest)` |
| `assume(P)` | `P ==> WP(rest)` |
| Function call `f(args)` | Verify `f`'s precondition holds with `args`, then assume `f`'s postcondition |
| `match` | One VC per arm, conjoined |

### 6.4.2 Call Site Verification

At each call site, the compiler generates two VCs:

1. **Precondition check**: the caller's current context implies the callee's precondition (with actual arguments substituted).
2. **Postcondition assumption**: after the call, the callee's postcondition (with actual arguments and return value substituted) is assumed to hold.

This means the verifier is modular: each function is verified independently, assuming its callees satisfy their contracts.

The precondition VC is discharged at **Tier 1** when the actual arguments and the callee's precondition both translate to the decidable fragment.  When an argument or the precondition uses a construct outside that fragment — an ADT field of a host-handle type such as `Map`, or a precondition over a non-modelled builtin — the obligation cannot be checked statically.  Rather than let it vanish (which would make `vera verify` overstate coverage), the verifier degrades it **loudly** to a runtime-guarded **Tier 3** obligation with an **E532** warning ([#882](https://github.com/aallan/vera/issues/882)), counted in `vera verify --json`; the codegen precondition guard still enforces the contract at runtime.  This holds for calls in every position — statement, `requires`, and `ensures` predicates alike.

A practical implication: if a function `bad` has an implementation that doesn't satisfy its own `ensures(...)` clause, the verifier reports E500 on `bad`'s body — but a caller `main` that uses `bad`'s declared contract is still verified.  The bug is contained to `bad`'s body-vs-contract mismatch; `main`'s reasoning is sound under the assumption that `bad` honours its declared postcondition.  This is intentional — it keeps verification compositional and bounded by per-function complexity, rather than requiring whole-program reasoning at every call site.  The cost is that an E500 on `bad` is a real failure that downstream consumers (`vera test`, `vera verify`) MUST surface; silently classifying `bad` as verified while `main` reads its contract would break the soundness chain.

**Opaque effect values.** A `let` whose value is an effect operation's result (`let @Int = random_int(0, 9);`) binds a fresh *opaque* constant of the value's type in the verification model, and translation of the body continues past it ([#764](https://github.com/aallan/vera/issues/764), [#1199](https://github.com/aallan/vera/issues/1199)); the same applies per-component to a tuple destructure whose source cannot be projected.  Two rules govern how obligations over an opaque value classify:

- **Preconditions stay strict.**  A call precondition that cannot be proven — because the argument is opaque — is reported (**E501**), exactly as for an opaque function result: establishing the precondition is the caller's obligation, and the repair is an `assert`/`assume` on the value, whose fact flows into the check ([#804](https://github.com/aallan/vera/issues/804)).
- **Refutations over opaque values are not violations.**  A postcondition, refined return, or primitive-operation obligation that *fails* to prove where the goal mentions an opaque constant demotes to a runtime-checked **Tier 3** obligation (`E522` for a postcondition) rather than reporting a definite violation — a countermodel over an unconstrained stand-in says nothing about the value the effect actually produces (`random_int(1, 9)` never returns `0`, but its stand-in would "witness" a zero divisor).  A proof that *succeeds* despite the opacity is kept at Tier 1: it holds for every value the constant could take.  The demotion is per-obligation, not per-function — a genuine violation elsewhere in the same body is still reported.

Distinct effect-op bindings are distinct constants — two `random_int` results are never provably equal.  The variadic `Tuple` pseudo-constructor participates in the decidable fragment: a tuple literal in expression position, and a destructured tuple's components, translate via an on-demand single-constructor datatype sort keyed on the component types ([#747](https://github.com/aallan/vera/issues/747)), so tuple construction and projection are Tier-1-decidable when every component's type and value translate to the decidable fragment (a component of an unsupported type — a function value, for instance — leaves the tuple unmodelled, and the enclosing obligations fall to Tier 3 as before).

### 6.4.3 Primitive Operation Safety

The verifier checks the contracts the programmer wrote, and **auto-synthesises** a proof obligation at every primitive operation whose well-definedness depends on operand values.  Each is discharged from the surrounding preconditions and path conditions exactly like a call-site precondition check (§6.4.2):

| Operation | Obligation | Code |
|---|---|---|
| `a - b` (Nat) | `a >= b` — no underflow | E502 |
| `@Int` value into a `@Nat` slot | `value >= 0` | E503 |
| `a / b`, `a % b` (Int / Nat) | `b != 0` | E526 |
| `arr[i]` (`Array<T>`) | `0 <= i < array_length(arr)` | E527 |
| `a + b`, `a * b` (Int / Nat); `a - b` (Int) | result within i64 / u64 range — no overflow | E528 |
| `float_to_int(x)` | `x` finite (not NaN / Inf) and `trunc(x)` within i64 range | E529 |

To discharge an operation obligation, the programmer encodes the constraint in a precondition (`requires(@Int.0 != 0)`), a guarding `if` (whose path condition holds in the relevant branch), or a refinement type (`{ @Int | @Int.0 != 0 }`).  A function that performs `@Int.1 / @Int.0` with `requires(true)` therefore does not verify cleanly: the unguarded divisor is a compile error (E526).

**Division and modulo** are Tier-1-decidable — the divisor is a concrete integer term — so an unguarded `a / b` whose Tier-1-translatable divisor admits a zero counterexample is a compile error (E526); a divisor beyond the translatable fragment (a fresh-scope slot in a closure or handler clause, an opaque effect result, a solver timeout) degrades to a runtime-guarded Tier-3 obligation instead, while a manifest zero divisor is E526 in any position.  (Float division is exempt: `f64.div` by zero yields inf/NaN, not a trap.)  **Array indexing** depends on `array_length`, which the SMT layer models as an *uninterpreted* function (§6.3.2), so bounds reasoning is in general beyond Tier 1.  The verifier therefore tiers the obligation honestly: it proves the bound at **Tier 1** when a literal length, refinement, precondition, or path condition pins the length; reports a compile error (**E527**) when the index provably exceeds a statically-known length (e.g. `[1, 2, 3][5]`); and otherwise — a dynamic, opaque length — degrades to a runtime-guarded **Tier 3** obligation (counted in `vera verify --json`, never a silent pass).  An index inside a closure body, quantifier predicate, or handler-clause body is walked under a fresh (empty) slot scope; one that depends on a captured length or fresh slot is reported as a runtime-guarded **Tier 3** obligation — beyond the fresh scope's decidable fragment, with the codegen bounds-check backing it — while a literal-only shape still classifies exactly (a manifest out-of-bounds literal is a loud E527) — while an index in a quantifier *domain* or a handler *body* (enclosing-scope positions) is tiered at full precision like any direct-position index; lifting the fresh-scope sites to a Tier-1 proof is the Tier 2 work in [#427](https://github.com/aallan/vera/issues/427).  Indexing applies to `Array<T>` only; indexing a `String` is a type error (E161).

The `@Nat` obligations (E502 / E503) carry the most nuance, spanning many binding sites.  The verifier emits an E502 obligation `lhs >= rhs` at every `@Nat - @Nat` subtraction site (see [#520](https://github.com/aallan/vera/issues/520)), and an E503 obligation `value >= 0` where an `@Int` value narrows into a `@Nat` **binding** slot — `let`, call-argument, effect-operation-argument, constructor-field, top-level match-bind, and literal-tuple-destructure sites (see [#552](https://github.com/aallan/vera/issues/552)), plus the generic-instantiation, ADT sub-pattern, non-literal-destructure, and cross-module imported-constructor sites (see [#747](https://github.com/aallan/vera/issues/747)), and the function **return** position — an `@Int` value (including an `if`/`match` tail) narrowing into a `@Nat` return is obligated `result >= 0` under the body's path conditions, the dual of the [#813](https://github.com/aallan/vera/issues/813) `@Nat -> @Int` widen-return obligation (see [#758](https://github.com/aallan/vera/issues/758)).  The codegen mirrors the subtraction obligation and the `@Nat` binding and return sites with runtime guards — every concrete site (`let`, destructure, match-bind, sub-pattern, concrete constructor field, concrete call-argument) plus **generic function-formal calls**, which guard on the monomorphised callee (the mangled instance `pick$Nat` carries concrete `@Nat` flags).  Three sites stay unguarded, all still obligated statically, so a Tier-3 narrowing the solver cannot discharge at any of them surfaces an E504 warning: a **user-declared effect operation's argument**, whose runtime guard is deferred (see [#754](https://github.com/aallan/vera/issues/754)); the **generic-instantiated constructor field**, since constructor layouts carry no per-field `@Nat` metadata to monomorphise; and a **tuple component at construction**, since the built-in `Tuple` carrier's layout has no per-field `@Nat` metadata either — the component's target type is recovered from the threaded target-type table for the `@Nat` -> `@Int` *widening* guard ([#813](https://github.com/aallan/vera/issues/813)), but the narrowing direction is not guarded there. Tuple *destructuring* is guarded, so a tuple that is taken apart is checked on the way out rather than on the way in; one that is only returned or passed on is not checked at all.  The built-in effects' operation arguments are guarded at their op-call sites: the `State` write boundaries (see [#1203](https://github.com/aallan/vera/issues/1203)) and the `Exn` `throw` payload, which also carries the §2.6.5 refinement-predicate guard (see [#1268](https://github.com/aallan/vera/issues/1268)).  Division, modulo, and array indexing now follow the same auto-synthesis pattern ([#680](https://github.com/aallan/vera/issues/680)); lifting dynamic or closure-captured array bounds from a runtime-guarded Tier 3 to a Tier-1 proof is part of the Tier 2 verification work in [#427](https://github.com/aallan/vera/issues/427).

**Integer overflow** ([#798](https://github.com/aallan/vera/issues/798)).  `@Int` is a signed 64-bit machine integer and `@Nat` an unsigned one; `+` / `-` / `*` wrap at the i64 / u64 boundary.  Like `@Nat` underflow and signed-division `MIN / -1`, an overflowing operation is a *partial* operation that **traps** at runtime rather than silently wrapping, so each `@Int` / `@Nat` `+` / `-` / `*` carries an obligation that the result stays in range.  It is classified at the operands' **common (coerced) type** — `@Int` if either operand is `@Int` (since `@Nat <: @Int`), else `@Nat` — not one operand's self-type (a non-negative literal is `@Nat`, but `5 + @Int.0` is an i64 add) nor the possibly-narrowed result type (an `@Int.0 + 1` stored into a `@Nat` slot is still an i64 add).  A two-check mirrors array indexing: the result provably in range → **Tier 1**; provably out of range (e.g. a literal `u64.MAX + 1`, or `@Int.0 + 1` under `requires(@Int.0 == i64.MAX)`) → a compile error (**E528**); otherwise — dynamic operands — a runtime-guarded **Tier 3** trap.  `@Nat` subtraction is excluded — it is the underflow obligation (E502) above, never a high-overflow.

**String length** ([#802](https://github.com/aallan/vera/issues/802)).  Vera strings are UTF-8 byte sequences and `string_length` returns the **byte** count, but Z3's string theory (SMT-LIB 2.6) models strings as sequences of Unicode **code points** — its `Length` counts code points, which disagrees with the runtime on every multibyte character (`string_length("é")` is `2`, not `1`).  `string_length` is therefore modeled at **Tier 1** only for a string **literal**, whose exact byte length is known; on any non-literal argument it defers to a runtime-guarded **Tier 3** obligation (Z3's string theory has no byte-length operator).  The boolean predicates `string_contains` / `string_starts_with` / `string_ends_with` stay **Tier 1**: UTF-8 is self-synchronizing, so a valid substring / prefix / suffix matches at the byte level exactly when it matches at the code-point level.  The other byte/offset-sensitive string builtins (`string_slice`, `string_index_of`, `string_char_code`, `string_chars`) are not translated to Z3 and already fall to **Tier 3**.  Two further deferrals keep the predicates honest.  Z3's string-sort alphabet only reaches U+2FFFF, and its Python binding silently stores any higher code point as the literal's *escape text* rather than the character — so a literal containing a code point **above U+2FFFF** is unusable in the `z3.StringVal`-based predicate translation (`string_contains` / `string_starts_with` / `string_ends_with`) and defers to **Tier 3** there, instead of letting a predicate match phantom escape bytes the runtime never sees.  `string_length` is unaffected by this one — it byte-counts the *decoded* literal, so an astral literal's length stays **Tier 1**.  A **lone surrogate** (U+D800–U+DFFF) defers on **both** paths: `z3.StringVal` stores it as phantom escape text just like the astral case, and — since it has no UTF-8 encoding at all — `string_length`'s byte count cannot be taken either.

**Numeric type conversions** ([#807](https://github.com/aallan/vera/issues/807)).  Three Float64 builtins are modeled at **Tier 1**.  `float_clamp(v, lo, hi)` is pure Float64 and modeled **unconditionally** as the faithful WASM `f64.min(f64.max(v, lo), hi)` — NaN-propagating and ±0-correct.  Z3's own `fp.min` / `fp.max` *diverge* from WASM here (SMT-LIB returns the non-NaN operand and leaves ±0 implementation-defined, whereas WASM propagates NaN and pins the ±0 sign), so a naive `fpMin` / `fpMax` model would be **unsound** — it would prove `!float_is_nan(float_clamp(NaN, …))`, which the runtime refutes.  `float_clamp` is total, so it carries no obligation.  `int_to_float(n)` and `float_to_int(x)` cross the Int↔Float boundary, and Z3's *symbolic* Int↔Real↔FP reasoning is **unreliable** — it returns spurious counterexamples that do not satisfy their own constraints, non-deterministically across timeouts.  These are therefore modeled at Tier 1 **only for a concrete (constant-foldable) argument**, where Z3 is merely constant-folding; a symbolic argument defers to a sound **Tier 3** (the guiding principle: defer to Tier 3 what Z3 cannot soundly model).  `int_to_float` is total (`f64.convert_i64_s` never traps).  `float_to_int` is **partial** — `i64.trunc_f64_s` traps on NaN / ±Inf / out-of-i64-range — so a concrete argument additionally carries the domain obligation above (a provable violation is a loud **E529**), and a symbolic argument's Tier-3 obligation is guarded by the codegen trunc trap.  (The four format/parse Float64 builtins — `float_to_string`, `parse_float64`, `decimal_from_float`, `decimal_to_float` — remain **Tier 3** by necessity: Z3's string theory cannot format or parse a float, and `Decimal` is an opaque host handle.)

Runtime traps for unguarded primitives are Vera-native: each trap carries a kind label (`divide_by_zero`, `out_of_bounds`, etc.), a per-kind Fix paragraph naming the precondition that would have prevented it, and a source backtrace — so a missing static guarantee is still a recoverable signal.

### 6.4.4 SMT Solver Integration

VCs are translated to SMT-LIB format and solved by Z3:

1. **Tier 1 VCs** (decidable fragment): sent directly to Z3. Z3 returns `unsat` (VC is valid), `sat` (VC is invalid, with counterexample), or `unknown`. Each invocation is bounded to **10 seconds** by default to prevent pathological blowup on adversarially crafted contracts. Tier 1 contracts that time out fall to Tier 3.
2. **Tier 2 VCs** (with hints, not yet implemented — [#427](https://github.com/aallan/vera/issues/427)): the compiler provides additional axioms from `assert` statements and lemma functions. Z3 has a timeout of 10 seconds. Currently, contracts requiring hints fall to Tier 3.
3. **Tier 3 fallback**: if Z3 returns `unknown` or times out, the VC is compiled as a runtime check.

### 6.4.5 Counterexample Reporting

When Z3 finds a counterexample (a VC is invalid), the compiler reports the specific input values that violate the contract:

```
ERROR: Contract violation in function foo (line 5)

    private fn foo(@Int -> @Int)
      requires(true)
      ensures(@Int.result > @Int.0)
      ...

  Postcondition: @Int.result > @Int.0
  Counterexample:
    @Int.0 = 0
    @Int.result = 0

  The postcondition @Int.result > @Int.0 does not hold when @Int.0 = 0.
  Consider strengthening the precondition (e.g., requires(@Int.0 > 0))
  or weakening the postcondition (e.g., ensures(@Int.result >= @Int.0)).
```

## 6.5 Runtime Contract Checking

When a contract cannot be verified statically (Tier 3), the compiler inserts a runtime check:

```
-- For a requires clause:
if !precondition {
  trap("Precondition violation in function_name: requires(@Int.0 > 0)")
}

-- For an ensures clause:
let @ReturnType = body_result;
if !postcondition {
  trap("Postcondition violation in function_name: ensures(@Int.result > 0)")
}
@ReturnType.0
```

Runtime contract violations cause a WASM trap with a diagnostic message.

The compiler MUST emit a warning for each runtime-checked contract:

```
WARNING: Cannot statically verify contract at line 3: requires(@Int.0 > 0)
  Reason: Z3 timeout after 10s
  Inserting runtime check.
```

## 6.6 Lemma Functions

> **Status: Not yet implemented.** Lemma functions are part of Tier 2 verification ([#427](https://github.com/aallan/vera/issues/427)) and are not yet supported by the reference compiler.

A lemma function is a `pure` function whose sole purpose is to establish a fact for the verifier. Its body must type-check and its contract must verify, but it is never called at runtime:

```
private fn lemma_sum_positive(@Nat, @Nat -> @Unit)
  requires(@Nat.0 > 0 && @Nat.1 > 0)
  ensures(@Nat.0 + @Nat.1 > @Nat.0)
  effects(pure)
{
  ()
}
```

Lemma functions are declared with the same syntax as regular functions. The compiler recognises that a function whose body is `()` and whose return type is `Unit` with non-trivial contracts is a lemma, and does not emit code for it.

To use a lemma, call it in an `assert`:

```
assert(lemma_sum_positive(@Nat.0, @Nat.1) == ());
```

After this point, the verifier knows that `@Nat.0 + @Nat.1 > @Nat.0`.

## 6.7 Contract Inheritance

When a function type is used as a parameter, the caller can rely on the contracts of the concrete function passed:

<!-- vera:skip-parse category="FRAGMENT" reason="type SafeDiv = fn(...) + fn apply_div" -->
```
type SafeDiv = fn(Int, { @Int | @Int.0 != 0 } -> Int) effects(pure);

private fn apply_div(@Int, @Int, @SafeDiv -> @Int)
  requires(@Int.1 != 0)
  ensures(true)
  effects(pure)
{
  @SafeDiv.0(@Int.0, @Int.1)
}
```

The refinement on `SafeDiv`'s **second** parameter serves as the contract. The call passes `@Int.1` into that refined position, so the compiler verifies `@Int.1 != 0` at the call site — `apply_div`'s first `@Int` parameter, which follows from the precondition.

## 6.8 Summary of Verification Tiers

![Three-tier verification: each contract obligation goes to Z3 with a ten-second budget — unsat is verified (Tier 1), sat is a compile error with a counterexample, unknown or timeout defers to a Tier 3 runtime guard whose violation traps with a kind, a Fix paragraph, and a backtrace. Tier 2 (hints) is not yet implemented and also falls to Tier 3.](../assets/diagrams/tiers.svg)

| Tier | Scope | Solver | Timeout | Failure mode |
|------|-------|--------|---------|--------------|
| 1 | Z3 quantifier-free decidable fragment: linear integer + real arithmetic, bool, strings (Z3 `String` sort), uninterpreted sorts/functions (length, **array literals and indexing via `index_<T>` functions** — #667).  No single SMT-LIB logic name covers all of these — QF_UFLIRA is the closest standard logic (integer + real + uninterpreted functions, without strings); strings are a Z3-specific extension. | Z3 | 10 seconds | Compile error with counterexample; falls to Tier 3 on unknown or timeout |
| 2 | Extended: quantifiers, lemma/assert hints — [not yet implemented](https://github.com/aallan/vera/issues/427) | Z3 with hints | 10 seconds | Falls to Tier 3 |
| 3 | Runtime | None (checks emitted as code) | N/A | Runtime trap |

The ten-second figure is the DEFAULT per-query budget, not a fixed property of the
language: `vera verify --timeout-ms N` sets it for one run and `VERA_Z3_TIMEOUT_MS`
for an environment, in that precedence. This matters for reading a Tier 3: an
obligation whose proof lands near the budget is Tier 1 on a fast host and Tier 3 on
a slow one, so raising the budget is what distinguishes a claim that needed more
time from one the solver can never see through.

A fully Tier 1-verified program has the strongest guarantee: if it compiles, the contracts hold for all inputs. A program with Tier 3 contracts may fail at runtime if the contracts are violated.

`vera verify` reports a one-line summary:

```text
$ vera verify tests/conformance/ch06_assert_assume.vera
OK: tests/conformance/ch06_assert_assume.vera
Verification: 8 verified (Tier 1), 3 runtime checks (Tier 3)
```

That program contains an `assume` statement, and the summary does not mention it: assumptions reach no tier and are counted nowhere (see the table below). The warning this chapter requires for every `assume` is not emitted either — tracked in [#1345](https://github.com/aallan/vera/issues/1345).

### 6.8.1 Obligation Vocabulary

Every obligation this chapter describes ends in exactly one of the first four states below; the remaining rows name adjacent concepts that are easily mistaken for them. The middle column is the `status` field `vera verify --json` reports for that obligation, so the words used in prose and the machine output are the same set.

| Word | `--json` status | Meaning |
|------|-----------------|---------|
| **proved** | `verified` | Tier 1. Z3 discharged the obligation; it holds for every input. Counted in `tier1_verified`. |
| **runtime-guarded** | `tier3`, `timeout` | Tier 3. Not proved, but the compiler emitted a guard that traps on violation. Counted in `tier3_runtime`. |
| **unguarded** | `tier3_unguarded` | Neither proved nor guarded. Reported as a warning (`E504`, `E506`, `E531`) and counted in no tier. |
| **refuted or unprovable** | `violated` | The obligation did not discharge and the compiler refuses the program. Two ways in: Z3 returned a concrete counterexample, or — for a call precondition over an opaque value (Section 6.4.2) — it could not establish the goal at all. Both report `violated`, which is why the diagnostic says a call *may* violate the precondition rather than that it does. A compile error (`E500`, `E501`, `E502`, `E505`, …), counted in no tier. |
| **assumed** | — | An `assume` statement (Section 6.2.6), not an obligation: the fact is taken on trust rather than discharged, so it reaches no tier and is counted nowhere. It is an unsound escape hatch. |
| **tested** | — | `vera test` generates inputs from the contracts and runs them through WASM. A distinct activity rather than a tier: it samples inputs, it does not quantify over them. |
| **specified, not implemented** | — | Carried by the `Status:` callouts in this specification and collected in the [implementation-status appendix](../docs/implementation-status.md). |

The counts partition accordingly: `total == tier1_verified + tier3_runtime`. A `violated` or `tier3_unguarded` obligation is discharged to no tier, so it appears in the `obligations` array and in the diagnostics, but in neither count.

## 6.9 Limitations

| Limitation | Issue |
|-----------|-------|
| Tier 2 verification (Z3-guided with `assert`/lemma hints) is specified in §6.3.2 and §6.6 but not implemented; contracts requiring hints fall to Tier 3 | [#427](https://github.com/aallan/vera/issues/427) |
| The `invariant(...)` clause on `data` declarations is specified in §6.2.3 but not implemented; every documented form fails with `[E130] no <DataName> bindings in scope`.  Use refinement types (Chapter 2, §2.6) for the same effect on constraint-bearing data values. | [#686](https://github.com/aallan/vera/issues/686) |