Skip to main content

old() with Collections

Referring to previous collection state in postconditions.

When verifying code that modifies spec collections, you often need to compare the collection's state before and after the method executes. The old() expression captures the collection's value at method entry, enabling postconditions that describe how the collection changed.

Capturing Collection State​

The old(collection) expression captures a snapshot of the entire collection at method entry. You can then use collection operations on this snapshot to compare with the current state.

seq-ghost-field.sr9
// Using Seq as a ghost field for event logging
persistent actor {
  ghost var events : Seq<Nat> = Seq.empty();

  invariant Seq.len(events) >= 0;

  public func log(eventId : Nat) : async ()
    modifies events
    ensures Seq.len(events) == Seq.len(old(events)) + 1;
    ensures Seq.get(events, Seq.len(events) - 1) == eventId;
  {
    ghost {
      events := Seq.concat(events, Seq.singleton(eventId));
    };
  };
}

In this example:

  • old(events) captures the sequence at method entry
  • Seq.len(old(events)) queries the length of that snapshot
  • The postcondition proves the sequence grew by exactly one element

old() Is Read-Only​

old(collection) provides a read-only snapshot of the collection at method entry. You can reference it multiple times without any special tracking.

old-collection-no-consume.sr9
// Demonstrating that old() does not consume the collection
persistent actor {
  ghost var log : Seq<Nat> = Seq.empty();

  public func append(value : Nat) : async ()
    modifies log
    // old(log) can be referenced multiple times - no consumption
    ensures Seq.len(log) == Seq.len(old(log)) + 1;
    ensures Seq.get(log, Seq.len(log) - 1) == value;
    // All previous elements are unchanged
    ensures forall<Nat>(pure func (i : Nat) : Bool =
      i < Seq.len(old(log)) ==> Seq.get(log, i) == Seq.get(old(log), i));
  {
    ghost {
      log := Seq.concat(log, Seq.singleton(value));
    };
  };
}

Notice that old(log) is referenced three times in the postconditions. This is valid because old() is a read-only snapshot and spec collections are not linear values.

Comparing Map State​

Maps commonly need postconditions that describe which keys changed and which remained the same:

old-collection-map.sr9
// Using old() with Map to compare state before and after updates
persistent actor {
  ghost var counts : Map<Nat, Nat> = Map.empty();

  public func increment(id : Nat) : async ()
    modifies counts
    // After increment, the count for id is one more than before
    ensures Map.get(counts, id) == Map.getOr(old(counts), id, 0) + 1;
    // All other keys remain unchanged
    ensures forall<Nat>(pure func (k : Nat) : Bool =
      k != id ==> Map.getOr(counts, k, 0) == Map.getOr(old(counts), k, 0));
  {
    ghost {
      let prev = Map.getOr(counts, id, 0);
      counts := Map.update(counts, id, prev + 1);
    };
  };
}

Key patterns for Map:

  • Map.get(counts, id) == Map.getOr(old(counts), id, 0) + 1 - compare values at a specific key
  • Map.getOr(old(counts), k, 0) - use getOr to handle keys that may not exist in the old state
  • forall over keys to state that all non-target keys are unchanged; see quantifier patterns

Comparing Set State​

Sets support postconditions about membership changes:

old-collection-set.sr9
// Using old() with Set to verify membership changes
persistent actor {
  ghost var allocated : Set<Nat> = Set.empty();

  public func allocate(id : Nat) : async ()
    modifies allocated
    // After allocation, id is a member of the ghost set.
    ensures Set.contains(id, allocated);
    // Existing members remain members after the union update.
    ensures forall<Nat>(pure func (k : Nat) : Bool =
      Set.contains(k, old(allocated)) ==> Set.contains(k, allocated));
  {
    ghost {
      allocated := Set.union(allocated, Set.singleton(id));
    };
  };
}

Key patterns for Set:

  • Set.contains(id, old(allocated)) - check if element was in the old set
  • forall<Nat>(...) over old(allocated) - prove existing members remain present after an update
  • allocated == old(allocated) - assert the set is unchanged when no modification occurred

Comparing Multiset State​

Multisets track element counts, making old() useful for proving count changes:

multiset-ghost-field.sr9
// Ghost Multiset fields track multiplicities
persistent actor {
  ghost var inventory : Multiset<Nat> = Multiset.empty();

  invariant Multiset.card(inventory) >= 0;

  public func stock(item : Nat) : async ()
    modifies inventory
  {
    ghost {
      inventory := Multiset.union(inventory, Multiset.singleton(item));
      assert Multiset.contains(item, inventory);
    };
  };

  public func sell(item : Nat) : async ()
    modifies inventory
  {
    ghost {
      inventory := Multiset.minus(inventory, Multiset.singleton(item));
    };
  };
}

Key patterns for Multiset:

  • Multiset.count(inventory, item) == Multiset.count(old(inventory), item) + 1 - prove count increased
  • Multiset.count(inventory, item) == Multiset.count(old(inventory), item) - 1 - prove count decreased

Conservation Laws​

A common verification pattern is proving that some aggregate property is preserved across an operation. Use old() to express conservation laws:

old-collection-conservation.sr9
// Conservation law: cardinality is preserved when moving between sets
persistent actor {
  ghost var setA : Set<Nat> = Set.empty();
  ghost var setB : Set<Nat> = Set.empty();

  // Move an element from A to B, conserving total cardinality
  func transfer(id : Nat) : async ()
    modifies setA, setB
    requires Set.contains(id, setA);
    requires not Set.contains(id, setB);
    // Total cardinality is preserved
    ensures Set.card(setA) + Set.card(setB) == Set.card(old(setA)) + Set.card(old(setB));
    // Element moved correctly
    ensures not Set.contains(id, setA);
    ensures Set.contains(id, setB);
  {
    ghost {
      setA := Set.minus(setA, Set.singleton(id));
      setB := Set.union(setB, Set.singleton(id));
    };
  };
}

The postcondition Set.card(setA) + Set.card(setB) == Set.card(old(setA)) + Set.card(old(setB)) proves that the total cardinality is preserved when transferring an element.

For larger conservation proofs, introduce a domain-specific lemma or trusted summary function instead of repeating the whole algebra in every public method.

Collection Operations in old()​

All read-only collection operations work inside old():

CollectionOperations with old()
MapMap.get(old(m), k), Map.getOr(old(m), k, default), Map.contains(k, old(m)), Map.domain(old(m)), Map.range(old(m)), Map.card(old(m))
SetSet.contains(x, old(s)), Set.subset(old(s1), old(s2)), Set.card(old(s))
SeqSeq.get(old(s), i), Seq.len(old(s)), Seq.contains(x, old(s))
MultisetMultiset.count(old(ms), x), Multiset.contains(x, old(ms)), Multiset.card(old(ms))

You can also compare entire collections for equality: old(collection) == collection to assert no change occurred.

Common Patterns​

Only Specified Keys Changed​

Prove that all keys except specific ones remain unchanged:

ensures forall<K>(pure func (k : K) : Bool =
  k != targetKey ==> Map.getOr(m, k, 0) == Map.getOr(old(m), k, 0))

Element Was Added​

Prove a new element was added to a set:

ensures Set.contains(newId, result);
ensures not Set.contains(newId, old(set));

Element Was Removed​

Prove an element was removed from a set:

ensures not Set.contains(removedId, result);
ensures Set.contains(removedId, old(set));

Sequence Append​

Prove an element was appended to the end:

ensures Seq.len(log) == Seq.len(old(log)) + 1;
ensures Seq.get(log, Seq.len(log) - 1) == newValue;
ensures forall<Nat>(pure func (i : Nat) : Bool =
  i < Seq.len(old(log)) ==> Seq.get(log, i) == Seq.get(old(log), i));

Cardinality Change​

Prove the size changed by a specific amount:

ensures Set.card(set) == Set.card(old(set)) + 1  // one element added
ensures Map.card(map) == Map.card(old(map)) - 1  // one key removed

Restrictions​

The old() expression has the same restrictions with collections as with other types:

  • Allowed in: ensures clauses, assert statements, ghost blocks, lemma bodies
  • Not allowed in: requires clauses, actor invariants, pure function contracts, runtime code

See old() Restrictions for the full list.

Summary​

  • old(collection) captures the collection's state at method entry
  • old() does not consume the collection (read-only snapshot)
  • You can reference old(collection) multiple times in postconditions
  • Use old() for comparing before/after state, proving conservation laws, and describing what changed
  • All read-only collection operations work with old(): get, contains, card, len, etc.
  • Update-style operations are pure. Applying one to an old() value constructs another spec value and does not mutate the snapshot. In postconditions, prefer direct comparisons against old(collection) unless a derived updated value makes the contract clearer.