Restrictions

The old() expression is restricted to specific contexts where it makes semantic sense. This page explains where old() can and cannot appear, and why.

Quick Reference

Context	Allowed	Reason
ensures clauses	Yes	Primary use case
assert statements	Yes	Proof steps in ghost context
Ghost blocks	Yes	Ghost context permits old()
Lemma bodies	Yes	Verification-only code
requires clauses	No	No previous state at entry
entry_requires clauses	No	Runtime entry guards cannot mention ghost snapshots
Actor invariants	No	Must hold at all states
Pure function contracts	No	Pure functions have no state
Runtime code	No	old() is verification-only
Nested old()	No	Semantically undefined

Allowed Contexts

Postconditions (ensures)

The primary use of old() is in postconditions:

public func increment(delta : Int) : async Int
  modifies counter
  ensures counter == old(counter) + delta;
{
  counter += delta;
  counter
};

Static Assertions (assert)

You can use old() in assert statements to establish intermediate proof facts:

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

Ghost Blocks

Ghost blocks create a verification-only context where old() is permitted:

public func example() : async ()
  modifies total
  ensures total == old(total) + 1;
{
  ghost {
    let prev = old(total);
    // Use prev for proof reasoning
  };
  total += 1;
};

Lemma Bodies

Lemmas are verification-only functions that can reference old():

lemma proveChange()
  ensures total == old(total) + 1;
{
  // Lemma body can use old()
};

Forbidden Contexts

Preconditions (requires)

old() is not allowed in requires clauses:

// WRONG - rejected by verifier
public func bad(delta : Int) : async Int
  modifies counter
  requires old(counter) >= 0;  // Error: old() not allowed in requires
{
  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
};

Why: Preconditions describe the state at method entry. At entry, there is no prior method state to reference because the method has not yet executed. The current value is the entry value.

Error message: old() is not allowed in requires clauses

Entry Preconditions (entry_requires)

old() is also rejected in entry_requires clauses:

// WRONG - entry guards are runtime checks
public func bad(delta : Int) : async Int
  modifies counter
  entry_requires old(counter) >= 0;
  requires counter >= 0;
{
  counter += delta;
  counter
};

Why: entry_requires is exported runtime code. It runs before the body and must use concrete entry values, not verification-only snapshots.

Error message: old() is not allowed in entry_requires clauses

Actor Invariants

old() cannot appear in actor invariants:

// WRONG - rejected by verifier
persistent actor Bad {
  var counter : Int = 0;

  invariant counter >= old(counter);  // Error: old() not allowed in invariants

  public func increment() : async ()
    modifies counter
  {
    counter += 1;
  };
}

Why: Invariants must hold at all observable states of the actor. An invariant describes a property of the current state, not a relationship between states. If you need to express monotonicity or change bounds, use ghost state instead.

Error message: old() is not allowed in invariants

Pure Function Contracts

Pure functions cannot use old() in their contracts:

// WRONG - rejected by verifier
public pure func pureWithOld(x : Nat) : Nat
  ensures result == old(x);  // Error: old() not allowed in pure contracts
{
  x
};

// CORRECT - pure functions reference parameters directly
public pure func pureCorrect(x : Nat) : Nat
  ensures result == x;
{
  x
};

Why: Pure functions have no side effects and cannot access or modify state. Since there is no state change, old() has no meaning. Pure functions operate only on their inputs and produce outputs.

Error message: old() is not allowed in pure function contracts

Runtime Code

old() is a verification construct and cannot appear in runtime code:

// WRONG - rejected by type checker
public func badRuntime() : async Int
  modifies counter
{
  let prev = old(counter);  // Error: old() only in ghost context
  counter += 1;
  prev
};

// CORRECT - save value in local variable
public func goodRuntime() : async Int
  modifies counter
  ensures result == old(counter);
{
  let prev = counter;  // Save current value manually
  counter += 1;
  prev
};

Why: old() is erased during compilation and does not exist at runtime. The verification model uses old() for proofs, but runtime code must use explicit local variables to save previous values.

Error message: old() expression can only be used in ghost context (ghost let/block, verification assertions, or lemma) (Error M0313)

Nested old() Expressions

You cannot nest old() inside another old():

// WRONG - rejected by verifier
public func nestedOld() : async Int
  modifies counter
  ensures counter == old(old(counter)) + 1;  // Error: nested old() not supported
{
  counter += 1;
  counter
};

// CORRECT - single level of old()
public func singleOld() : async Int
  modifies counter
  ensures counter == old(counter) + 1;
{
  counter += 1;
  counter
};

Why: old(old(expr)) is semantically undefined. The old() expression takes a single snapshot at method entry. Nesting it would imply capturing the snapshot of a snapshot, which has no clear meaning.

Error message: nested old() is not supported

Runtime Assertions

The runtime:assert construct cannot use old():

// WRONG - old() not allowed in runtime:assert
public func badRuntimeAssert() : async ()
  modifies x
{
  let prev = x;
  x := x + 1;
  runtime:assert x == old(x) + 1;  // Error: old() not in runtime
};

// CORRECT - use local variable
public func goodRuntimeAssert() : async ()
  modifies x
{
  let prev = x;
  x := x + 1;
  runtime:assert x == prev + 1;  // Works
};

Why: runtime:assert executes at runtime, and old() is a verification-only construct. Use local variables to capture values you need to check at runtime.

Await Boundaries

While old() is allowed in async functions, it always refers to method entry, not per-await state:

persistent actor AsyncExample {
  var x : Nat = 1;

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

  // old(x) refers to entry value, not pre-await value
  public func example(n : Nat) : async Nat
    modifies x
    entry_requires n > 0;
    requires n > 0;
    ensures result == old(x);
  {
    let entry = x;     // Must save if you need entry value at runtime
    x += n;            // x changes
    try { await tick(); } catch (_) {};  // old(x) still refers to entry, not this point
    entry              // Return saved entry value
  };
}

This is not technically a restriction, but a clarification: old() does not reset at await points. See Basic Usage for details.

Summary

• old() works in ensures, assert, ghost blocks, and lemma bodies
• old() is forbidden in requires and entry_requires, invariants (must hold always), pure function contracts, and runtime code
• Nested old(old(...)) is not supported
• Use local variables when you need to capture previous values at runtime

Related Topics

• old() basics for method-entry snapshot semantics
• runtime:assert for runtime checks that must use concrete values
• entry_requires for exported runtime guards
• Async commit points for the difference between method entry and pre-await state