Skip to main content

Update Semantics

Spec collections (Map, Set, Seq, Multiset) are ghost value models in verification. Operations such as Map.update, Set.union, Seq.concat, and Multiset.minus return new values and do not consume the old version. Aliasing is allowed.

Older Sector9 builds treated some collection operations as linear moves. That is no longer the user-facing model: the old value remains available after an update. The implementation still contains legacy linearity error codes, but the collection linearity predicate is disabled for these spec collections.

Updates Return New Values​

ghost {
  let m0 : Map<Nat, Int> = Map.empty();
  let m1 = Map.update(m0, 1, 10);
  assert Map.contains(1, m1);
  assert not Map.contains(1, m0);
}

You can keep both the old and new versions and reason about each separately. This is especially useful when proving postconditions that compare a current ghost field with old(field).

Read-Only Operations​

Read-only operations (Map.get, Map.getOr, Map.contains, Map.domain, Map.range, Map.card, Set.contains, Seq.len, Multiset.count, and similar queries) never consume their inputs and can be called repeatedly.

No Linearity Errors​

The frontend no longer enforces linear consumption for spec collections, so linearity errors like M0243 and M0244 are not emitted for Map, Set, Seq, or Multiset usage.

That does not remove the element type restrictions. Collection keys and elements still need to be spec-immutable in verification mode, and violations are reported as M0242.

Summary​

  • Updates return new values and do not consume inputs
  • Aliasing of collection values is allowed
  • Read-only operations remain pure queries
  • The remaining hard restriction is spec-immutable key/value/element types