Multiple Contracts

You can write multiple requires and ensures clauses on the same function. All clauses of the same type are conjoined (AND-ed together).

On exported actor methods, mirror nontrivial caller-controlled requires clauses with entry_requires guards. Private helpers, module helpers, and pure functions use ordinary requires without runtime entry guards.

Basic Syntax

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;
  ensures result < 200;
{
  a + b
}

The verifier treats this exactly as if you wrote:

• requires (a > 0) and (b > 0) and (a < 100) and (b < 100)
• ensures (result > 0) and (result < 200)

Why Use Multiple Clauses

Multiple clauses improve readability when you have several conditions:

// Hard to read - one long line
public func clamp(x : Int, lo : Int, hi : Int) : async Int
  entry_requires lo <= hi and x >= -1000 and x <= 1000 and lo >= -1000 and hi <= 1000;
  requires lo <= hi and x >= -1000 and x <= 1000 and lo >= -1000 and hi <= 1000;
  ensures result >= lo and result <= hi and (x >= lo and x <= hi ==> result == x);
{ ... }

// Easier to read - separate clauses
public func clamp(x : Int, lo : Int, hi : Int) : async Int
  entry_requires lo <= hi;
  entry_requires x >= -1000;
  entry_requires x <= 1000;
  entry_requires lo >= -1000;
  entry_requires hi <= 1000;
  requires lo <= hi;
  requires x >= -1000;
  requires x <= 1000;
  requires lo >= -1000;
  requires hi <= 1000;
  ensures result >= lo;
  ensures result <= hi;
  ensures (x >= lo and x <= hi) ==> result == x;
{ ... }

Each clause expresses one logical constraint. Readers can scan the list to understand all requirements.

Multiple Requires Patterns

Bounds Checking

public func processRange(start : Nat, end : Nat, max : Nat) : async Nat
  entry_requires start <= end;
  entry_requires end <= max;
  entry_requires max <= 1000;
  requires start <= end;
  requires end <= max;
  requires max <= 1000;
  ensures result == end - start;
{
  end - start
}

Input Validation

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

Structural Constraints

public func binarySearch(arr : [Nat], target : Nat) : async ?Nat
  entry_requires arr.size() > 0;
  entry_requires arr.size() <= 10000;
  requires arr.size() > 0;
  requires arr.size() <= 10000;
{
  // Search implementation
  null
}

Multiple Ensures Patterns

Return Value Bounds

public func clampedAdd(a : Nat, b : Nat) : async Nat
  entry_requires a <= 100;
  entry_requires b <= 100;
  requires a <= 100;
  requires b <= 100;
  ensures result >= a;
  ensures result >= b;
  ensures result <= 200;
{
  a + b
}

State Change Guarantees

persistent actor {
  var x : Int = 0;
  var y : Int = 0;

  public func swap() : async ()
    modifies x, y
    ensures x == old(y);
    ensures y == old(x);
  {
    let tmp = x;
    x := y;
    y := tmp;
  }
}

Conditional Postconditions

Use ==> (implication) to express case-by-case guarantees:

public func sign(n : Int) : async Int
  ensures n > 0 ==> result == 1;
  ensures n < 0 ==> result == -1;
  ensures n == 0 ==> result == 0;
{
  if (n > 0) { 1 }
  else if (n < 0) { -1 }
  else { 0 }
}

Each ensures handles one case. All three are verified together.

Combining Requires and Ensures

A complete function contract often has multiple of both:

persistent actor {
  var balance : Nat = 0;

  public func transfer(amount : Nat, fee : Nat) : async Nat
    modifies balance
    entry_requires amount > 0;
    entry_requires amount + fee <= balance;
    requires amount > 0;
    requires amount + fee <= balance;
    ensures balance == old(balance) - amount - fee;
    ensures result == amount;
  {
    balance -= amount + fee;
    amount
  }
}

The preconditions ensure the transfer is valid. The postconditions guarantee correct state updates.

Clause Order

For total expressions, clause order does not change the final logical meaning. These are equivalent:

// Order A
public func example(n : Nat) : async Nat
  entry_requires n > 0;
  entry_requires n < 100;
  requires n > 0;
  requires n < 100;
  ensures result > 0;
  ensures result == n * 2;
{ n * 2 }

// Order B
public func example(n : Nat) : async Nat
  entry_requires n < 100;
  entry_requires n > 0;
  requires n < 100;
  requires n > 0;
  ensures result == n * 2;
  ensures result > 0;
{ n * 2 }

Choose the order that reads most naturally. When a later contract expression uses a partial operation such as division, put the guard first so the expression is well-defined.

Redundant Clauses

Redundant clauses are allowed and do not cause errors:

public func example(n : Int) : async Int
  entry_requires n > 0;
  requires n > 0;
  requires n >= 1;   // Redundant: implied by n > 0
  requires n > -1;   // Redundant: also implied
  ensures result == n;
{
  n
}

The verifier simply treats all clauses as one conjunction. Redundancy adds no overhead to verification. However, avoid unnecessary clauses for clarity.

Contradictory Clauses

Contradictory requires make a function uncallable:

// WRONG - no valid call site exists
public func impossible(n : Int) : async Int
  entry_requires n > 10;
  entry_requires n < 5;
  requires n > 10;
  requires n < 5;   // Contradicts n > 10
  ensures result == n;
{
  n
}

The verifier detects this and reports the function as uncallable (vacuously true).

Contradictory ensures indicate a bug:

// WRONG - postcondition can never be satisfied
public func broken(n : Nat) : async Nat
  ensures result > 0;
  ensures result == 0;   // Contradicts result > 0
{
  n
}

The verifier reports that the postcondition cannot be established.

With Actor Invariants

Multiple contracts work with actor invariants. The invariant is implicitly conjoined with all public method contracts:

persistent actor {
  var balance : Nat = 0;

  invariant balance >= 0;

  public func deposit(amount : Nat) : async ()
    modifies balance
    entry_requires amount > 0;
    entry_requires amount <= 10000;
    requires amount > 0;
    requires amount <= 10000;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  }
}

The verifier checks:

• Precondition: amount > 0 and amount <= 10000 (explicit) plus balance >= 0 (invariant)
• Postcondition: balance == old(balance) + amount (explicit) plus balance >= 0 (invariant)

With Footprints

Multiple contracts integrate with reads and modifies:

persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  var c : Int = 0;

  public func updatePair(newA : Int, newB : Int) : async ()
    modifies a, b
    reads c
    entry_requires newA >= 0;
    entry_requires newB >= 0;
    requires newA >= 0;
    requires newB >= 0;
    ensures a == newA;
    ensures b == newB;
    ensures c == old(c);   // Framed by reads
  {
    a := newA;
    b := newB;
  }
}

Fields in reads but not modifies are automatically framed (unchanged).

With Pure Functions

Pure functions can have multiple contracts:

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

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

Verification Process

The verifier processes contracts as follows:

1. Collect: Gather all requires and ensures clauses from the function header
2. Conjoin: Combine same-type clauses with AND
3. Add invariants: For actor methods, add invariant to both pre and post
4. Add frame conditions: For fields in reads, add field == old(field) to postconditions
5. Verify: Prove that the body establishes all postconditions given all preconditions

Common Mistakes

Missing Guard for Division

// WRONG - division before guard
public func bad(a : Nat, b : Nat) : async Nat
  requires a / b > 0;   // Division happens before checking b != 0
  requires b != 0;
{ a / b }

// CORRECT - guard first
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 }

For division in contracts, the non-zero guard should appear in a separate clause.

Mixing Different Clause Types

// Avoid - interleaved requires and ensures are harder to scan
public func bad(n : Nat) : async Nat
  requires n > 0;
  ensures result > 0;
  requires n < 100;   // Put all requires together
{ n }

// CORRECT - group by clause type
public func good(n : Nat) : async Nat
  entry_requires n > 0;
  entry_requires n < 100;
  requires n > 0;
  requires n < 100;
  ensures result > 0;
{ n }

While the parser accepts interleaved clauses, grouping by type improves readability.

Overly Specific Contracts

// WRONG - too many trivial clauses
public func add(a : Nat, b : Nat) : async Nat
  ensures result >= 0;   // Nat is always >= 0
  ensures result >= a;   // True by definition of addition
  ensures result >= b;   // True by definition of addition
  ensures result == a + b;
{ a + b }

// CORRECT - just the essential contract
public func add(a : Nat, b : Nat) : async Nat
  ensures result == a + b;
{ a + b }

Include only clauses that add meaningful constraints.

Summary

• Multiple requires clauses are conjoined (AND-ed) into a single precondition
• Multiple ensures clauses are conjoined (AND-ed) into a single postcondition
• Clause order does not change the final logical meaning for total expressions, but guards should precede partial operations
• Use multiple clauses for readability when you have several conditions
• Group clauses by type (requires first, then ensures)
• Redundant clauses are allowed but avoid them for clarity
• Contradictory clauses cause verification to fail or make functions uncallable
• Contracts integrate with invariants, footprints, and pure functions
• For division in contracts, place the non-zero guard in a separate clause

Related Topics

• Preconditions and postconditions for individual clause meanings
• Entry guards for mirrored runtime checks
• Logical implication for case-by-case guarantees