Skip to main content

Common Patterns

This page presents practical patterns for using old() in real verification scenarios. These patterns appear frequently when proving properties about state-changing methods.

Conditional State Changes​

Use old() with implications to specify different behaviors based on the pre-state:

public func updateWithCount(newVal : Int) : async () modifies value, count
  ensures newVal != old(value) ==> count == old(count) + 1;
  ensures newVal == old(value) ==> count == old(count);
  ensures value == newVal;
{
  if (newVal != value) {
    count += 1;
  };
  value := newVal;
};

The pattern old(x) > 0 ==> ... lets you express different guarantees depending on the entry state. Each branch of your implementation must satisfy the corresponding postcondition.

Clamping with Change Detection​

A common pattern is clamping a value to bounds while returning whether clamping occurred:

public func clampTo(lo : Int, hi : Int) : async Bool modifies value
  entry_requires lo <= hi;
  requires lo <= hi;
  ensures old(value) < lo ==> (value == lo and result == true);
  ensures old(value) > hi ==> (value == hi and result == true);
  ensures (old(value) >= lo and old(value) <= hi) ==> (value == old(value) and result == false);
{
  if (value < lo) {
    value := lo;
    true
  } else if (value > hi) {
    value := hi;
    true
  } else {
    false
  };
};

Each case specifies exactly what happens based on where old(value) falls relative to the bounds.

Conservation Laws​

Use old() to express that a quantity is conserved across operations:

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 states the sum is preserved. This pattern is essential for token systems, balance tracking, and any scenario where resources move between locations. When the values are stored in collections, combine old() with the collection model rather than only tracking scalar fields.

Monotonicity​

Prove that a value only increases (or only decreases):

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

For strict monotonicity where the value must increase:

public func strictIncrement() : async ()
  modifies counter
  ensures counter > old(counter);
{
  counter += 1;
};

Bounded Change​

Specify upper and lower bounds on how much a value can change:

public func incrementBounded(n : Int) : async ()
  modifies counter
  entry_requires n >= 0 and n <= 10;
  requires n >= 0 and n <= 10;
  ensures counter >= old(counter);
  ensures counter <= old(counter) + 10;
{
  counter += n;
};

Record Field Patterns​

Apply old() to record field access to track changes in structured data:

type Point = { x : Int; y : Int };

var position : Point = { x = 0; y = 0 };

public func move(dx : Int, dy : Int) : async ()
  modifies position
  ensures position.x == old(position.x) + dx;
  ensures position.y == old(position.y) + dy;
{
  position := { x = position.x + dx; y = position.y + dy }
};

Each field is captured independently at method entry. You can also swap fields:

public func swapCoords() : async ()
  modifies position
  ensures position.x == old(position.y);
  ensures position.y == old(position.x);
{
  let oldX = position.x;
  position := { x = position.y; y = oldX }
};

Return Old Value While Resetting​

A useful pattern is returning the previous state while setting a new value:

public func resetAndReturn() : async Point
  modifies position
  ensures result.x == old(position.x);
  ensures result.y == old(position.y);
  ensures position.x == 0;
  ensures position.y == 0;
{
  let old_pos = position;
  position := { x = 0; y = 0 };
  old_pos
}

Loop Invariants with old()​

In loops, old() still refers to method entry. Use it in loop invariants to track cumulative progress:

public func countup(n : Int) : async Int
  modifies counter
  entry_requires n >= 0;
  requires n >= 0;
  ensures result == n;
  ensures counter == old(counter) + n;
{
  var i = 0;
  while (i < n) {
    loop:invariant i >= 0 and i <= n;
    loop:invariant counter == old(counter) + i;
    counter := counter + 1;
    i := i + 1;
  };
  i
};

The invariant counter == old(counter) + i expresses that after i iterations, the counter has increased by exactly i from its entry value. When the loop terminates with i == n, the postcondition follows.

Countdown Pattern​

For loops that count down:

public func countdown(n : Int) : async Int
  modifies counter
  entry_requires n >= 0;
  requires n >= 0;
  ensures result == 0;
  ensures counter == old(counter) + n;
{
  var i = n;
  while (i > 0) {
    loop:invariant i >= 0 and i <= n;
    loop:invariant counter == old(counter) + (n - i);
    counter := counter + 1;
    i := i - 1;
  };
  i
};

The key insight is that old(counter) + (n - i) tracks progress as i decreases from n to 0.

Async Patterns​

In async functions, old() captures method entry state and remains stable across await boundaries. It does not capture the last pre-await value, so async proofs often combine entry locals, invariants, and careful footprints.

Capture Before Await​

When you need the pre-await value at runtime, save it to a local:

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 (_) {};
  before
};

The local before preserves the entry value because locals are unaffected by await. The postcondition result == old(counter) is provable because before equals the entry value.

Invariant Protection​

Use actor invariants to protect fields across await:

var pinned : Int = 7;
var counter : Int = 0;

invariant pinned == 7;

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

public func protected() : async () reads pinned modifies counter
  ensures pinned == old(pinned);
{
  try { await bump(); } catch (_) {};
};

The invariant guarantees pinned cannot change, even across await. Without the invariant, this postcondition would fail because state can change during async calls.

Common Async Mistake​

Remember that old() refers to method entry, not pre-await state:

// INCORRECT - will fail verification
public func bad(n : Nat) : async Nat
  modifies x
  entry_requires n > 0;
  requires n > 0;
  ensures old(x) == x;  // Fails: x changed before await
{
  x += n;
  try { await tick(); } catch (_) {};
  x
};

After x += n, the current value of x differs from old(x). The postcondition compares method entry value to exit value, so it fails.

Combining Patterns​

Real contracts often combine multiple patterns:

public func transferWithLog(from : Int, to : Int, amount : Int) : async ()
  modifies balanceA, balanceB, transferCount
  entry_requires amount >= 0;
  entry_requires from != to;
  requires amount >= 0;
  requires from != to;
  ensures balanceA + balanceB == old(balanceA) + old(balanceB);  // Conservation
  ensures amount > 0 ==> transferCount == old(transferCount) + 1; // Conditional count
  ensures amount == 0 ==> transferCount == old(transferCount);
  ensures amount > 0 ==> balanceA != old(balanceA);              // Conditional change
{
  if (amount > 0) {
    balanceA -= amount;
    balanceB += amount;
    transferCount += 1;
  };
};

Summary​

  • Use old() with implications for conditional postconditions based on entry state
  • Express conservation laws as a + b == old(a) + old(b)
  • Prove monotonicity with x >= old(x) or x > old(x)
  • Apply old() to record fields for structured data: old(record.field)
  • In loop invariants, old() refers to method entry, enabling cumulative progress tracking
  • For async functions, capture entry values in locals and use invariants to protect fields across await
  • Combine patterns for complex contracts involving multiple properties