Skip to main content

Threading Updates (Optional)

Threading is the practice of chaining updates through sequential variable bindings. It is optional, but still a clear way to show the evolution of a collection value in specs.

The Threading Pattern​

ghost {
  let m0 : Map<Nat, Int> = Map.empty();
  let m1 = Map.update(m0, 1, 100);
  let m2 = Map.update(m1, 2, 200);
  assert Map.card(m2) == 2;
  assert Map.card(m0) == 0;
}

Unlike the old linear model, m0 and m1 remain valid after each update. Threading is just a clarity pattern, not a requirement. Use it when the names make the proof easier to read: before, debited, credited, final.

Ghost Fields​

For actor/module ghost fields, the idiom is still:

ghost {
  field := Map.update(field, key, value);
}

This rebinds the field to the new version while leaving previous versions available in local variables. Public methods that rebind ghost fields still need accurate modifies clauses.

Best Practices​

Use descriptive names for intermediate bindings. Instead of m0, m1, m2, use names that reflect the state:

ghost {
  let empty = Map.empty<Text, Nat>();
  let withAlice = Map.update(empty, "alice", 100);
  let withBob = Map.update(withAlice, "bob", 50);
  let final = Map.update(withBob, "charlie", 75);
}

Keep update chains short. If you have many updates, consider grouping related updates or using ghost functions with contracts that state the exact collection transformation.

Use old() at method boundaries. Inside a method, named bindings are often clearer. In postconditions, use old(field) to describe the method-entry value.

Summary​

  • Threading is optional; updates do not consume inputs
  • Old versions remain valid after updates
  • Rebinding ghost fields is still the clearest style in specs
  • Helper ghost functions can package repeated update chains