Skip to main content

Preconditions with requires

The requires clause specifies conditions that must be true when a function is called. These are caller obligations: whoever calls the function must ensure the precondition holds.

For public actor methods, pair caller-controlled requires clauses with entry_requires so external messages are checked at runtime before entering the verified body.

Basic Syntax​

public func increment(n : Nat) : async Nat
  entry_requires n <= 1000;
  requires n <= 1000;
  ensures result == n + 1;
{
  n + 1
}

The verifier proves that every internal call site satisfies n <= 1000. For a public actor method, entry_requires is the runtime guard that admits external calls into the logical precondition. Inside the function, you can assume the precondition is true.

What Preconditions Mean​

A precondition is a contract between caller and function:

  • Caller's obligation: Ensure the precondition holds before calling
  • Function's assumption: The precondition is true at entry

If verified code calls a function without satisfying its precondition, verification fails at the call site, not inside the callee. For external calls into public actor methods, entry_requires is the runtime admission check that prevents invalid messages from entering the verified body.

public func double(x : Nat) : async Nat
  entry_requires x < 1000;
  requires x < 1000;
  ensures result == x * 2;
{
  x * 2
}

public func test() : async Nat {
  // double(5000)    // ERROR: precondition x < 1000 not satisfied
  double(500)        // OK: 500 < 1000
}

Common Use Cases​

Preventing Division by Zero​

public func divide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
  ensures result == a / b;
{
  a / b
}

Ensuring Array Bounds​

persistent actor {
  var data : [var Int] = [var 1, 2, 3];

  public func get(i : Nat) : async Int
    reads data
    entry_requires i < data.size();
    requires i < data.size();
    ensures result == data[i];
  {
    data[i]
  }
}

Guarding Option Unwrapping​

public func unwrap(opt : ?Nat) : async Nat
  entry_requires opt != null;
  requires opt != null;
{
  switch opt {
    case (?v) v;
    case null { 0 };  // Unreachable, but needed for type
  }
}

Preventing Overflow​

persistent actor {
  var counter : Nat64 = 0;

  public func increment() : async Nat64
    modifies counter
    entry_requires counter < 18446744073709551615;
    requires counter < 18446744073709551615;
    ensures result == counter;
  {
    counter += 1;
    counter
  }
}

Structural Constraints​

public func clamp(x : Int, lo : Int, hi : Int) : async Int
  entry_requires lo <= hi;
  requires lo <= hi;
  ensures result >= lo;
  ensures result <= hi;
{
  if (x < lo) { lo }
  else if (x > hi) { hi }
  else { x }
}

Multiple Preconditions​

You can write multiple requires clauses. They are conjoined (AND-ed together):

public func safeOp(a : Int, b : Int) : async Int
  entry_requires a > 0;
  entry_requires b > 0;
  entry_requires a < 100;
  entry_requires b < 100;
  requires a > 0;
  requires b > 0;
  requires a < 100;
  requires b < 100;
  ensures result > 0;
{
  a + b
}

This is equivalent to requires (a > 0) and (b > 0) and (a < 100) and (b < 100).

What Can Appear in Preconditions​

Allowed​

  • Parameters: Any function parameter
  • State: Actor fields (when function has access)
  • Comparisons: ==, !=, <, <=, >, >=
  • Logical operators: and, or, not
  • Implication: ==>
  • Arithmetic: +, -, *, / (with guards for division)
  • Array operations: size(), element access (with bounds)
  • Pure function calls: Calls to pure functions
  • Quantifiers: forall, exists
public func complexPre(arr : [Nat], x : Nat, y : Nat) : async Nat
  entry_requires arr.size() > 0;
  entry_requires x < arr.size();
  entry_requires y != 0;
  entry_requires x / y > 0;
  requires arr.size() > 0;
  requires x < arr.size();
  requires y != 0;
  requires x / y > 0;
  ensures result == arr[x];
{
  arr[x]
}

Not Allowed​

ExpressionReason
old(x)old() captures pre-state; makes no sense before execution
resultReturn value doesn't exist yet
Local variablesNot visible at call sites
Body-local ghost variablesNot visible to callers
Method callsSide effects not allowed in specifications

Division in Preconditions​

Division and modulo in preconditions require explicit guards:

// WRONG - verifier can't prove b != 0 at division point
public func bad(a : Nat, b : Nat) : async Nat
  requires a / b > 0;
{ a / b }

// CORRECT - guard before division
public func good(a : Nat, b : Nat) : async Nat
  entry_requires b != 0;
  entry_requires a / b > 0;
  requires b != 0;
  requires a / b > 0;
{ a / b }

The guard must appear before or alongside the division in the requires order.

Preconditions with Trusted Functions​

When you call a trusted function, you must still satisfy its preconditions:

public trusted func safeDivide(a : Nat, b : Nat) : Nat
  requires b > 0;
  ensures result == a / b;
{
  a / b
}

public func average(x : Nat, y : Nat) : Nat
  ensures result == (x + y) / 2;
{
  safeDivide(x + y, 2)  // OK: 2 > 0 always holds
}

The verifier checks that callers satisfy preconditions even when the function body is trusted.

Preconditions vs Assertions​

Featurerequiresassert
LocationFunction headerFunction body
Checked atCall sitesPoint in code
Visible toCallersFunction only
PurposeCaller obligationsInternal proof steps

Use requires for conditions callers must ensure. Use assert for intermediate proof obligations within the function body.

Preconditions and Invariants​

Actor invariants hold at method boundaries. Preconditions add method-specific constraints:

persistent actor {
  var balance : Nat = 0;
  invariant balance >= 0;

  // Invariant: balance >= 0 (always)
  // Precondition: amount <= balance (for this method)
  public func withdraw(amount : Nat) : async ()
    entry_requires amount <= balance;
    requires amount <= balance;
    modifies balance
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
  }
}

Pure Functions with Preconditions​

Pure functions can have preconditions:

pure func safeSub(a : Int, b : Int) : Int
  requires a >= b;
  ensures result == a - b;
{
  a - b
}

Note: Pure functions cannot use old() in any contract clause.

Verification vs Runtime​

requires is a logical proof construct. For private/internal helpers, there is no runtime entry check; callers must prove the precondition before calling. For exported actor methods, add a matching entry_requires guard for client-controlled obligations:

func divideInternal(a : Int, b : Int) : Int
  requires b != 0;  // Internal callers must prove this
{
  a / b
}

For exported methods, use entry_requires:

public func divide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
{
  a / b
}

Common Mistakes​

Using old() in Preconditions​

// WRONG - old() not allowed in requires
public func bad(delta : Int) : async Int modifies counter
  requires old(counter) >= 0;  // ERROR
{ counter += delta; counter }

// CORRECT - use current value
public func good(delta : Int) : async Int modifies counter
  entry_requires counter >= 0;
  requires counter >= 0;
  ensures counter == old(counter) + delta;
{ counter += delta; counter }

Placing Requires in Function Body​

// WRONG - syntax error
public func bad(n : Nat) : async Nat {
  requires n > 0;  // ERROR: unexpected token
  n
}

// CORRECT - requires in header
public func good(n : Nat) : async Nat
  entry_requires n > 0;
  requires n > 0;
{
  n
}

Referencing Locals in Preconditions​

// WRONG - locals not visible to callers
public func bad(n : Nat) : async Nat {
  let local = n + 1;
  requires local > n;  // ERROR
  n
}

Summary​

  • requires specifies caller obligations that must hold when a function is called
  • Preconditions appear in function headers, between signature and body
  • Multiple requires clauses are conjoined (AND-ed)
  • Allowed: parameters, state, comparisons, logic, pure calls, quantifiers
  • Not allowed: old(), result, locals, ghost variables, method calls
  • Division in preconditions requires explicit non-zero guards
  • For exported actor methods, pair nontrivial requires with entry_requires
  • Use for bounds checking, null guards, overflow prevention, and structural constraints