Minimizing old()

The old() expression captures heap state at method entry. While essential for relating pre-state to post-state, large old() expressions on heap structures are a primary solver performance stressor. This page covers why old() is expensive and practical patterns to reduce its usage.

Why old() Affects Performance

When you write old(arr[i].field), the verifier must relate the current heap to the method-entry heap snapshot. This usually involves:

1. Snapshot function generation: Pure domain functions summarize the relevant heap structure
2. Axiom instantiation: Injectivity and accessor axioms link snapshots to heap reads
3. Solver overhead: Each old() expression adds terms the SMT solver must reason about

For simple scalar fields like old(counter), the overhead is minimal. For arrays and mutable records, the cost grows with data structure complexity.

Expression	Relative Cost	Why
old(counter)	Low	Single field snapshot
old(record.field)	Low	Simple field projection
old(arr.size())	Medium	Array metadata access
old(arr[i])	Medium-High	Indexed heap read
old(arr[i].field)	High	Mutable record in array
Quantified old()	Very High	Multiplies instantiation

Diagnosing old() Performance Issues

Symptoms of expensive old() usage:

• Verification times out on methods with large arrays
• Simple-looking postconditions take unexpectedly long
• Adding more ensures clauses causes disproportionate slowdown

Check the generated Viper:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper --deterministic myfile.mo > output.vpr

Look for patterns like:

old($snap_rec_HASH(data, $size(data)))

Multiple snapshot calls in postconditions indicate potential performance issues.

Pattern 1: Use Local Snapshots

Instead of old() in postconditions, capture values in local variables before modification:

Expensive

old-expensive-array.sr9

// Expensive: old() on large array creates heap snapshot

persistent actor {
  var data : [var Int] = [var 0, 0, 0];
  var processed : Nat = 0;

  invariant processed <= data.size();

  // EXPENSIVE: old(data) snapshots entire array
  public func storeNext(value : Int) : async ()
    modifies data, processed
    entry_requires processed < data.size();
    requires processed < data.size();
    ensures processed == old(processed) + 1;
    ensures data[old(processed)] == value;
    ensures old(processed) > 0 ==> data[0] == old(data[0]);
  {
    data[processed] := value;
    processed += 1;
  };
}

Cheaper

old-local-snapshot.sr9

// Alternative: use local snapshot instead of old()

persistent actor {
  var data : [var Int] = [var 0, 0, 0];
  var processed : Nat = 0;

  invariant processed <= data.size();

  // CHEAPER: capture size in local before modification
  public func storeNext(value : Int) : async Nat
    modifies data, processed
    entry_requires processed < data.size();
    requires processed < data.size();
    ensures processed == result + 1;
    ensures data[result] == value;
  {
    let index = processed;  // Local snapshot
    data[index] := value;
    processed += 1;
    index  // Return old index for caller if needed
  };
}

Why this helps: Local primitives are stack values, not heap reads. The verifier tracks them directly without snapshot machinery. If the method exposes the snapshot to callers, return the captured value or store it in ghost state rather than repeating a deep old() expression.

When to use: When you only need to compare a single value or small number of values to their pre-state.

Pattern 2: Ghost History Tracking

Replace old() comparisons with ghost variables that track cumulative state:

old-ghost-history.sr9

// Alternative: ghost history tracking avoids old() entirely

persistent actor {
  var balance : Int = 0;
  ghost var totalDeposits : Int = 0;
  ghost var totalWithdrawals : Int = 0;

  invariant balance == totalDeposits - totalWithdrawals;
  invariant totalDeposits >= 0;
  invariant totalWithdrawals >= 0;

  // No old() needed: ghost variables track cumulative state
  public func deposit(amount : Int) : async ()
    modifies balance, totalDeposits
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;  // still valid if needed
  {
    balance += amount;
    ghost { totalDeposits := totalDeposits + amount; };
  };

  // Conservation proof via ghost state, not old()
  public func withdraw(amount : Int) : async ()
    modifies balance, totalWithdrawals
    entry_requires amount > 0 and balance >= amount;
    requires amount > 0;
    requires balance >= amount;
  {
    balance -= amount;
    ghost { totalWithdrawals := totalWithdrawals + amount; };
  };

  // Postcondition uses invariant relationship, not old()
  public func getBalance() : async Int reads balance, totalDeposits, totalWithdrawals
    ensures result == totalDeposits - totalWithdrawals;
  {
    balance
  };
}

Why this helps: The invariant balance == totalDeposits - totalWithdrawals captures the conservation property directly. Callers verify postconditions through the invariant relationship rather than repeated heap-entry comparisons.

When to use: For conservation laws, monotonicity properties, or any property where cumulative tracking replaces pre/post comparison.

Pattern 3: Rely on Frame Conditions

Fields not listed in modifies automatically get frame postconditions. Use this instead of explicit old(); remember that a method still needs reads for fields it reads in its body or specification:

old-frame-implicit.sr9

// Frame conditions provide implicit old() guarantees

persistent actor {
  var counter : Nat = 0;
  var limit : Nat = 100;
  var _tag : Text = "default";

  private func bumpCounter() : ()
    modifies counter
    ensures counter == old(counter) + 1;
  {
    counter += 1;
  };

  // Only counter is modified; limit and tag are framed
  public func increment() : async ()
    modifies counter
    // Implicit postconditions generated by verifier:
    //   ensures limit == old(limit)
    //   ensures _tag == old(_tag)
    ensures counter == old(counter) + 1;
  {
    bumpCounter();
  };

  // Caller can rely on framing without explicit old()
  public func safeIncrement() : async Bool
    reads limit
    modifies counter
  {
    let limitBefore = limit;  // Not needed for proof
    bumpCounter();
    // Frame condition guarantees limit unchanged
    assert limit == limitBefore;  // Verified via implicit frame
    counter <= limit
  };
}

Why this helps: The verifier generates ensures field == old(field) implicitly for all fields not in modifies. You get the guarantee without the syntax.

When to use: Always. Proper modifies declarations eliminate the need for explicit unchanged-field postconditions.

Pattern 4: Step Lemmas for Loops

Avoid old() in loop invariants by using ghost summary functions and step lemmas:

old-step-lemma.sr9

// Step lemmas avoid old() in loop invariants

module {
  public ghost abstract func triangular(n : Nat) : Nat
    requires true;
    ensures result == n * (n + 1) / 2;

  public lemma triangularStep(i : Nat) : ()
    ensures triangular(i) + (i + 1) == triangular(i + 1);
  {};

  // Loop invariant uses pure function, not old()
  public func sumTo(n : Nat) : Nat
    ensures result == triangular(n);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant acc == triangular(i);  // No old() needed

      triangularStep(i);
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

Why this helps: The loop invariant acc == triangular(i) is a closed-form relationship that doesn't reference method entry state. The step lemma establishes how to maintain the invariant at each iteration.

When to use: When loop invariants would otherwise compare accumulated state to entry state.

Pattern 5: Invariants Instead of old() Across Await

Actor invariants preserve guarantees across await without treating old() as a per-await snapshot. In Sector9, old() still means method entry, so invariants are the right tool for facts that must be re-established after interleaving:

old-invariant-pin.sr9

// Use invariants to pin values across await instead of old()

persistent actor {
  var counter : Int = 0;
  var maxValue : Int = 1000;

  // Invariant pins maxValue - no old() needed across await
  invariant maxValue == 1000;

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

  public func process() : async Int
    reads maxValue
    modifies counter
    ensures result <= maxValue;
  {
    let startMax = maxValue;
    counter += 1;

    try {
      await externalCall();
    } catch (_) {};

    // Without invariant, would need: ensures maxValue == old(maxValue)
    // With invariant, maxValue stability is guaranteed
    assert maxValue == startMax;  // Verified by invariant

    counter
  };
}

Why this helps: Invariants are re-established after every await. An invariant like maxValue == 1000 guarantees stability more efficiently than postconditions using old().

When to use: For values that should never change or that have fixed relationships to other state.

When old() Is Necessary

Some properties genuinely require old():

State transition proofs:

ensures status == #completed and old(status) == #pending

Delta specifications:

ensures counter == old(counter) + 1

Swap verification:

ensures x == old(y) and y == old(x)

For these cases, keep old() expressions minimal:

• Prefer old(scalar) over old(complex.path)
• Avoid old() inside quantifiers when possible
• Use the simplest expression that captures the relationship

Performance Checklist

1. Avoid old() on arrays - Use local snapshots or ghost tracking instead
2. Leverage frame conditions - Proper modifies eliminates explicit unchanged postconditions
3. Use ghost variables for history - Track cumulative state instead of comparing to entry
4. Prefer invariants across await - More efficient than old() for async stability
5. Keep old() expressions simple - Scalar fields over complex paths
6. Minimize quantified old() - Each bound variable multiplies snapshot cost
7. Check Viper output - Look for multiple snapshot calls in generated code

See Also

• Basic old() Usage - When and how to use old()
• old() Restrictions - Where old() is allowed
• Ghost Variables - History tracking alternative
• Frame Conditions - Implicit unchanged guarantees
• Trigger Management - Related quantifier performance issues

Summary

• old() creates heap snapshots that stress the SMT solver
• Local variables capture pre-state without snapshot overhead
• Ghost history tracking replaces pre/post comparison with cumulative state
• Frame conditions provide implicit old() guarantees for unchanged fields
• Step lemmas eliminate old() from loop invariants
• Actor invariants preserve values across await more efficiently than old()
• When old() is necessary, keep expressions minimal and avoid quantification