Skip to main content

Contracts

Contracts attach preconditions, postconditions, and invariants to functions and loops. They are the bridge between "I think this holds" and "the compiler proved this holds."

note
verum check does not run the SMT obligation pass

verum check type-checks and, for anything it can't dispatch statically, falls back to a runtime assertion — it does not invoke the solver, so it cannot report a contract failure of any kind. verum verify is the dedicated entry point that discharges requires/ensures/refinement obligations through SMT and can fail on them. If you're trying to see a contract violation and verum check reports nothing, that's expected — reach for verum verify.

Clause syntax at a glance​

Verum accepts contract clauses in two equivalent shapes.

Bare form — each clause keyword stands alone on its own signature line. Each precondition takes its own requires; each postcondition takes its own ensures. This is the form used throughout the stdlib and the VCS conformance specs under vcs/specs/L1-core/proof/contracts/:

fn foo(...) -> T
    requires pre1
    requires pre2
    ensures  post1
    ensures  post2
{
    body
}

where form — accepted for single-line signatures with one ensures:

fn abs(x: Int) -> Int where ensures result >= 0 {
    if x >= 0 { x } else { -x }
}

Two gotchas the compiler enforces today:

  1. where requires does not parse — use the bare requires keyword on its own signature line.
  2. Each precondition / postcondition takes its own keyword; comma-joining on one line (e.g. requires a, b, c or ensures x, y) fails to parse. Repeat the keyword per clause.

requires — preconditions​

fn divide(a: Int, b: Int) -> Int
    requires b != 0
{
    a / b
}

Multiple preconditions: repeat the requires keyword (no comma-joining on a single line).

fn middle(xs: &List<Int>, i: Int) -> Int
    requires i >= 0
    requires i < xs.len()
{
    xs[i]
}

Every caller must establish the conjunction of all requires clauses — that's the claim this section makes, and it does not currently hold as tested. fn divide(a: Int, b: Int) -> Int requires b != 0 { a / b } called with a literal 0 argument was checked directly with verum verify: both divide and its caller reported Proved, not a failure. The transcript that was here has been removed rather than corrected — it never matched real verum verify output in shape (a per-function report with a raw counter-example, not a source-anchored error[...] block), and given the claim itself doesn't reproduce, showing a "corrected" transcript would misrepresent a passing check as a failing one. Whether caller-side precondition establishment is enforced at all is an open question, not a documentation gap.

Preconditions compose naturally with refinement types. The above is equivalent to:

fn divide(a: Int, b: Int { self != 0 }) -> Int { a / b }

Prefer the refinement form when the precondition concerns a single parameter; prefer the requires clause when it spans several parameters or references external state:

fn transfer(from: &mut Account, to: &mut Account, amount: Money)
    requires from.balance >= amount,
             from != to
{ ... }

ensures — postconditions​

fn abs(x: Int) -> Int
    ensures result >= 0
    ensures result == x || result == -x
{
    if x >= 0 { x } else { -x }
}

Each ensures keyword takes one boolean expression; multiple clauses are conjoined by repeating the keyword. result refers to the return value.

Loop invariant and decreases​

while lo < hi
    invariant 0 <= lo && hi <= xs.len()
    invariant forall i in 0..lo. xs[i] < key
    invariant forall i in hi..xs.len(). xs[i] > key
    decreases hi - lo
{
    ...
}
  • invariant holds at entry and after every iteration.
  • decreases is a well-founded measure that strictly decreases each iteration — proves termination.

Without an explicit decreases, the compiler tries to infer one from the loop shape (while i < n with i += 1). When inference fails, you supply it.

throw and the error frame​

A function with throws(E) commits to a contract on its error cases:

fn parse_u32(s: Text) -> Int throws(ParseError)
    ensures result >= 0
    ensures result <= U32_MAX
{
    let n: Int64 = s.parse()?;
    if n < 0 || n > U32_MAX {
        throw ParseError.OutOfRange;
    }
    n
}

forall / exists in contracts​

Bounded quantifiers are first class:

fn all_positive(xs: &List<Int>) -> Bool
    ensures result == (forall i in 0..xs.len(). xs[i] > 0)
{
    xs.iter().all(|x| *x > 0)
}

Unbounded quantifiers (forall i: Int. ...) are allowed but may degrade proof performance; the solver will often need triggers.

old() — referring to prior state​

In postconditions of methods that mutate, old(self.field) refers to the field's value at call-entry:

fn push(&mut self, x: T)
    ensures self.len() == old(self.len()) + 1
    ensures self[old(self.len())] == x
{ ... }

Contract inheritance​

A protocol can declare contracts; implementations must satisfy them:

type Stack<T> is protocol {
    fn push(&mut self, x: T)
        ensures self.len() == old(self.len()) + 1;

    fn pop(&mut self) -> Maybe<T>
        ensures match result {
            Some(_) => self.len() == old(self.len()) - 1,
            None    => self.len() == 0 && old(self.len()) == 0,
        };
};

Every implement Stack<T> for X is required to satisfy the contracts; the compiler emits one obligation per method per implementation.

Contracts as documentation​

Contracts that pass verification double as documentation. The docgen tool (verum doc) extracts them into the generated reference:

/// Transfers `amount` from `from` to `to`, assuming both accounts
/// are distinct and `from` has sufficient balance.
fn transfer(from: &mut Account, to: &mut Account, amount: Money)
    requires from.balance >= amount
    requires from != to
    ensures  from.balance == old(from.balance) - amount
    ensures  to.balance   == old(to.balance)   + amount
{ ... }

Separation logic (selected cases)​

When contracts need to talk about disjoint memory regions, Verum uses a lightweight separation-logic fragment. This is handled under the hood by verum_verification::separation_logic — user-facing cases are limited to array partitioning and disjointness of mutable references:

fn swap_regions<'a>(a: &'a mut [Int], b: &'a mut [Int])
    requires disjoint(a, b)
{ ... }

Most code does not need this; the common case is covered by mutable- reference aliasing rules.

See also​