Skip to main content

Basic Usage

The old() expression captures the value of a field or expression at method entry. It lets postconditions and proof-only assertions relate the state you started with to the state you return.

Syntax​

ensures field == old(field) + delta;

The old(expr) expression evaluates expr using the state at method entry, not the current state. This snapshot is stable for the whole method, including across await boundaries.

When to Use old()​

Use old() when you need to:

  • Prove a value changed by a specific amount
  • Show two values were swapped
  • Verify a sum or invariant is preserved
  • Compare the return value to the original state

Basic Example​

persistent actor Counter {
  var total : Int = 0;

  public func add(delta : Int) : async Int
    modifies total
    ensures total == old(total) + delta;
    ensures result == total;
  {
    total += delta;
    total
  };
}

The postcondition total == old(total) + delta states that the new value of total equals the old value plus delta. The verifier proves this holds for all possible calls.

Multiple Fields with old()​

Each field has its own snapshot. You can use old() on multiple fields in the same postcondition:

persistent actor TwoFields {
  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;
  };
}

Here, old(x) and old(y) capture the entry values independently. The postconditions prove that x and y are swapped.

Preservation Properties​

Use old() to express that a property is preserved across a modification:

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

  public func transfer(amount : Int) : async ()
    modifies x, y
    ensures x + y == old(x) + old(y);
    ensures x == old(x) - amount;
    ensures y == old(y) + amount;
  {
    x -= amount;
    y += amount;
  };
}

The first postcondition proves the sum is preserved. The other two specify exactly how each field changes.

Arithmetic with old()​

You can use old() in any arithmetic expression:

persistent actor Math {
  var value : Int = 0;

  public func double() : async ()
    modifies value
    ensures value == old(value) * 2;
  {
    value := value * 2;
  };

  public func square() : async ()
    modifies value
    entry_requires value >= 0;
    requires value >= 0;
    ensures value == old(value) * old(value);
  {
    value := value * value;
  };

  public func negate() : async ()
    modifies value
    ensures value == 0 - old(value);
    ensures value + old(value) == 0;
  {
    value := 0 - value;
  };
}

Note that square() uses old(value) twice in the same postcondition.

old() with result​

Combine old() with result to relate the return value to the previous state:

persistent actor Snapshot {
  var counter : Int = 0;

  public func incrementAndGetOld() : async Int
    modifies counter
    ensures result == old(counter);
    ensures counter == old(counter) + 1;
  {
    let prev = counter;
    counter += 1;
    prev
  };
}

The function returns the old value while also incrementing the counter.

What old() Captures​

The old() expression captures values at method entry:

  • Actor fields (the primary use case)
  • Array elements (e.g., old(arr[i]))
  • Record fields (e.g., old(point.x))

For heap values like arrays and mutable records, old() refers to the entry snapshot of the logical value you mention. For large mutable structures, prefer precise expressions such as old(arr[i]) or collection model functions over broad snapshots when possible.

Method Entry, Not Per-Await​

In async functions with await, old() still refers to method entry, not the state before each await:

persistent actor AsyncOld {
  var x : Nat = 1;

  private func tick() : async () { () };

  public func example(n : Nat) : async Nat
    modifies x
    ensures result == old(x);
  {
    let entry = x;     // Save entry value
    x += n;            // Modify x
    try { await tick(); } catch (_) {};  // old(x) still refers to entry value
    entry              // Return entry value, matches postcondition
  };
}

The postcondition result == old(x) compares result to the value of x when the method was called, regardless of any await statements or modifications in between.

Where old() Is Allowed​

old() is allowed in:

  • ensures clauses (postconditions)
  • Static assert statements (verification-only proof checkpoints)
  • Ghost blocks (ghost { ... })
  • Lemma bodies

old() is not allowed in:

  • requires clauses (preconditions have no previous state)
  • Actor invariants
  • Pure function contracts
  • Runtime code

See Restrictions for details, including why runtime:assert cannot use old().

Common Patterns​

Increment by N​

ensures counter == old(counter) + n;

No Change (Framing)​

ensures field == old(field);

This is often implied by reads clauses for fields outside a callee's modification footprint, but can be stated explicitly when the unchanged value is part of the API contract.

Bounded Change​

ensures counter >= old(counter);
ensures counter <= old(counter) + max;

Percentage Increase​

public func incrementByPercent(pct : Int) : async ()
  modifies value
  entry_requires pct >= 0;
  requires pct >= 0;
  ensures value == old(value) + (old(value) * pct) / 100;
{
  let increment = (value * pct) / 100;
  value += increment;
};

Summary​

  • old(expr) captures the value of expr at method entry
  • Use in ensures clauses to relate pre-state to post-state
  • Each field is captured independently
  • Works with arithmetic, multiple fields, and arrays
  • In async functions, old() refers to method entry, not per-await state
  • Allowed in postconditions and ghost contexts; not allowed in preconditions or invariants