Postconditions with ensures

The ensures clause specifies conditions that must be true when a function returns. These are function guarantees: the function promises to make the postcondition hold.

Basic Syntax

public func add(a : Int, b : Int) : async Int
  ensures result == a + b;
{
  a + b
}

The verifier proves that every successful return establishes the postcondition. The result keyword refers to the returned value on that successful path.

What Postconditions Mean

A postcondition is a contract between function and caller:

• Function's obligation: Ensure the postcondition holds when returning
• Caller's assumption: The postcondition is true after the call

If a function cannot establish its postcondition, verification fails inside the function, not at call sites.

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

public func test() : async Nat {
  let x = try { await increment(5) } catch (_) { 6 };
  assert x == 6;  // Success postcondition plus matching fallback
  x
}

Common Use Cases

Specifying Return Values

public func max(a : Int, b : Int) : async Int
  ensures result >= a;
  ensures result >= b;
  ensures result == a or result == b;
{
  if (a >= b) { a } else { b }
}

State Change Guarantees

Use old() to capture pre-state and relate it to post-state:

persistent actor {
  var counter : Nat = 0;

  public func increment() : async Nat
    modifies counter
    ensures counter == old(counter) + 1;
    ensures result == counter;
  {
    counter += 1;
    counter
  }
}

Conditional Postconditions

Use ==> (implication) for case-by-case guarantees:

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

Bounds Guarantees

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 }
}

Preservation Properties

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;
  }
}

Option Return Values

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

  public func find(key : Nat) : async ?Nat
    reads data
    ensures key < data.size() ==> result == ?data[key];
    ensures key >= data.size() ==> result == null;
  {
    if (key < data.size()) { ?data[key] } else { null }
  }
}

Multiple Postconditions

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

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

This is equivalent to writing all conditions in a single ensures with and.

What Can Appear in Postconditions

Allowed

• Parameters: Any function parameter
• Result: The result keyword (return value)
• State with old(): Pre-state values via old(field)
• State (current): Current field values
• 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
• Switch expressions: Pattern matching in postconditions

public func complexPost(arr : [Nat], x : Nat) : async Nat
  entry_requires arr.size() > 0;
  entry_requires x < arr.size();
  requires arr.size() > 0;
  requires x < arr.size();
  ensures result >= 0;
  ensures result == arr[x];
  ensures result <= arr.size() * 100;
{
  arr[x]
}

Not Allowed

Expression	Reason
Local variables	Not visible to callers
Body-local ghost variables	Not visible to callers
Method calls	Side effects not allowed in specifications
Await expressions	Not allowed in specifications

Pattern Matching in Postconditions

You can use switch expressions in ensures clauses:

type Color = { #red; #blue : Nat; #green : (Nat, Nat) };

public func pick(c : Color) : async Nat
  ensures switch (c) {
    case (#red) result == 4;
    case (#blue x) result == x;
    case (#green (a, b)) result == a + b;
  }
{
  switch (c) {
    case (#red) 4;
    case (#blue x) x;
    case (#green (a, b)) a + b;
  }
}

For options with nested pattern matching:

public func shift(opt : ??Nat) : async ??Nat
  ensures switch (opt, result) {
    case (null, null) true;
    case (?null, ?null) true;
    case (??n, ??m) m == n + 2;
    case (_, _) false;
  }
{
  switch (opt) {
    case (null) null;
    case (?inner) {
      switch (inner) {
        case (null) ?null;
        case (?n) ??(n + 2);
      }
    };
  }
}

Postconditions with Footprints

When using modifies and reads, postconditions can reference those fields:

persistent actor {
  var fieldA : Int = 0;
  var fieldB : Int = 0;

  public func updateA(newVal : Int) : async ()
    modifies fieldA
    reads fieldB
    ensures fieldA == newVal;
    ensures fieldB == old(fieldB);  // Framed by reads
  {
    fieldA := newVal;
  }
}

Fields in reads are implicitly framed (unchanged). The postcondition fieldB == old(fieldB) is automatically ensured by the frame axiom.

Postconditions and Invariants

Actor invariants hold at method boundaries. Postconditions add method-specific guarantees:

persistent actor {
  var balance : Nat = 0;

  invariant balance >= 0;

  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  }

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures not result ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  }
}

The invariant balance >= 0 is maintained by both methods. Postconditions specify the method-specific behavior.

Postconditions in Async Functions

In async functions, old() captures state at method entry and remains stable across await:

persistent actor {
  var counter : Int = 0;

  private func bump() : async ()
    modifies counter
  {
    counter += 1;
  }

  public func snapshot() : async Int
    modifies counter
    ensures result == old(counter);
  {
    let before = counter;
    try { await bump(); } catch (_) {};  // old(counter) still refers to entry value
    before
  }
}

The old(counter) in the postcondition captures the value at method entry, before any await executes. It is not a pre-await snapshot.

Verification vs Runtime

ensures is a verification-only construct. There is no runtime check:

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

For defense-in-depth, you can add runtime checks that the verifier also proves:

public func abs(x : Int) : async Int
  ensures result >= 0;
{
  let r = if (x >= 0) { x } else { -x };
  runtime:assert r >= 0;  // Runtime trap if violated
  r
}

Common Mistakes

Always-False Postconditions

// WRONG - verifier reports unsat
public func impossible() : async Nat
  ensures false;
{
  0
}

A postcondition of false can never be satisfied.

Contradicting Implementation

// WRONG - postcondition contradicts body
public func add(a : Int, b : Int) : async Int
  ensures not (result == a + b);  // Negates what the body does
{
  a + b
}

The verifier reports that the postcondition cannot be established.

Using Body-Local Ghost Variables in Postconditions

// WRONG - ghost variables not visible to callers
public func bad(n : Nat) : async Nat {
  ghost var g : Nat = 0;
  ensures result == g;  // ERROR: ghost var cannot appear in contract
  ghost { g := n; };
  n
}

Body-local ghost variables are internal to the function body. Use parameters, result, actor fields, or documented ghost actor state instead.

Placing Ensures in Function Body

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

// CORRECT - ensures in header
public func good(n : Nat) : async Nat
  ensures result == n;
{
  n
}

Mismatched Return Types

// WRONG - verification fails
public func getPositive() : async Nat
  ensures result == -1;  // Nat cannot be negative
{
  1
}

Postconditions vs Assertions

Feature	ensures	assert
Location	Function header	Function body
Checked at	Function exit	Point in code
Visible to	Callers	Function only
Purpose	Function guarantees	Internal proof steps
Uses result	Yes	No
Uses old()	Yes	Yes

Use ensures for guarantees callers can rely on. Use assert for intermediate proof obligations within the function body.

Summary

• ensures specifies function guarantees that must hold when a function returns
• Postconditions appear in function headers, between signature and body
• Multiple ensures clauses are conjoined (AND-ed)
• Allowed: parameters, result, old(), state, comparisons, logic, pure calls, quantifiers
• Not allowed: local variables, body-local ghost variables, impure method calls
• Use old() to capture pre-state and compare with post-state
• Use ==> (implication) for conditional guarantees
• Pattern matching with switch is allowed in postconditions
• Verification-only: no runtime check unless you add runtime:assert
• Postconditions work with modifies/reads footprints for framing

Related Topics

• The result keyword for return-value specifications
• Old expressions for method-entry snapshots
• Footprints for state referenced in postconditions
• Trap specifications for declared trap paths