Skip to main content

Map Operations

Maps are specification-only key-value collections for verification reasoning. They let you model abstract state like account balances, permissions, or configuration without affecting runtime code.

The core Map module is a ghost API over Sector9's trusted primitive collection model. Maps are proof vocabulary, not deployed storage. Use runtime collections such as BMap or mutable maps when the program needs to store and iterate data, and connect them to Map through their Spec.model contracts. For proofs that connect runtime enumeration back to a model, use the descriptor-backed routes in Collection Snapshots.

Creating Maps​

Create an empty Map with Map.empty<K, V>():

map-basic.sr9
// Basic Map operations: empty, update, get, contains
persistent actor {
  public func demo() : async () {
    ghost {
      // Create an empty Map
      let m0 : Map<Nat, Int> = Map.empty();

      // Update adds a key-value pair, returns a new Map
      let m1 = Map.update(m0, 1, 10);
      let m2 = Map.update(m1, 2, 20);

      // Check membership
      assert Map.contains(1, m2);
      assert Map.contains(2, m2);
      assert not Map.contains(3, m2);

      // Get values
      assert Map.get(m2, 1) == 10;
      assert Map.get(m2, 2) == 20;
    };
  };
}

Maps are typed with key type K and value type V. Both must be spec-immutable types, except opaque/token handles by identity.

Core Operations​

Map.update(m, k, v)​

Adds or updates a key-value pair, returning a new Map:

let m1 = Map.update(Map.empty<Nat, Int>(), 1, 100);
let m2 = Map.update(m1, 2, 200);  // m1 remains available

Map.update is a ghost, side-effect-free operation: it returns a new map and does not consume the input. Threading updates through fresh names is still a clear style, but it is not a linearity requirement. See Threading Updates.

Map.get(m, k)​

Returns the value for key k:

let m = Map.update(Map.empty<Nat, Int>(), 1, 42);
assert Map.get(m, 1) == 42;

Use Map.get when you have already established membership, or when your model intentionally treats missing keys through the underlying map semantics. For explicit missing-key behavior, prefer Map.getOr.

Map.getOr(m, k, default)​

Returns the value for key k, or default if the key is missing:

map-getOr.sr9
// Map.getOr: safe retrieval with a default value
persistent actor {
  public func demo() : async () {
    ghost {
      let m = Map.update(Map.empty<Nat, Int>(), 1, 100);

      // Key exists: returns stored value
      let found = Map.getOr(m, 1, -1);
      assert found == 100;

      // Key missing: returns default
      let missing = Map.getOr(m, 999, -1);
      assert missing == -1;
    };
  };
}

Use getOr when you need explicit control over the default value.

Map.contains(k, m)​

Returns true if key k exists in the Map:

let m = Map.update(Map.empty<Nat, Int>(), 1, 10);
assert Map.contains(1, m);       // true
assert not Map.contains(2, m);   // true

Note the argument order: key first, then map.

Map.domain(m)​

Returns a Set of all keys in the Map:

map-domain-card.sr9
// Map.domain and Map.card: extracting keys and size
persistent actor {
  public func demo() : async () {
    ghost {
      let m0 = Map.empty<Nat, Int>();
      assert Map.card(m0) == 0;

      let m1 = Map.update(m0, 1, 10);
      let m2 = Map.update(m1, 2, 20);
      let m3 = Map.update(m2, 3, 30);

      // Cardinality is the number of keys
      assert Map.card(m3) == 3;

      // Domain returns a Set of all keys
      let keys = Map.domain(m3);
      assert Set.contains(1, keys);
      assert Set.contains(2, keys);
      assert Set.contains(3, keys);
      assert not Set.contains(4, keys);
    };
  };
}

The domain integrates with Set operations and quantifiers. This is the usual bridge from key-value models to "for every known key" properties.

Map.card(m)​

Returns the number of key-value pairs (cardinality) as an Int:

let m = Map.update(Map.update(Map.empty<Nat, Int>(), 1, 10), 2, 20);
assert Map.card(m) == 2;

Update Semantics​

Map.update returns a new Map. The old Map remains valid, so rebinding is optional and used mainly for clarity:

map-threading.sr9
// Correct Map threading: rebind after each update
persistent actor {
  public func demo() : async () {
    ghost {
      // Each update returns a new Map value; earlier values remain usable.
      let m0 : Map<Nat, Int> = Map.empty();
      let m1 = Map.update(m0, 1, 10);
      let m2 = Map.update(m1, 2, 20);
      let m3 = Map.update(m2, 3, 30);

      // All versions remain valid; m3 is the final threaded value.
      assert Map.contains(1, m3);
      assert Map.contains(2, m3);
      assert Map.contains(3, m3);
    };
  };
}

After calling Map.update(m0, ...), you can still use m0 to refer to the old state.

Read-Only Operations​

All operations except update are read-only. Updates return new values without consuming inputs:

ghost {
  let m = Map.update(Map.empty<Nat, Int>(), 1, 10);
  let c1 = Map.contains(1, m);   // m still valid
  let c2 = Map.contains(2, m);   // m still valid
  let v = Map.get(m, 1);         // m still valid
  let dom = Map.domain(m);       // m still valid
  assert c1;
};

You can read from a Map as many times as needed.

Ghost Map Fields​

Declare ghost Map fields at actor level to track abstract state:

map-ghost-field.sr9
// Ghost Map field for tracking runtime state
persistent actor {
  var balances : [var Nat] = [var 0, 0, 0];
  ghost var balanceMap : Map<Nat, Nat> = Map.empty();

  invariant Map.card(balanceMap) >= 0;

  public func setBalance(id : Nat, amount : Nat) : async ()
    modifies balances, balanceMap
    entry_requires id < balances.size();
    requires id < balances.size();
    ensures Map.get(balanceMap, id) == amount;
  {
    balances[id] := amount;
    ghost {
      balanceMap := Map.update(balanceMap, id, amount);
    };
  };

  public func getBalance(id : Nat) : async Nat
    reads balances
    entry_requires id < balances.size();
    requires id < balances.size();
    ensures result == balances[id];
  {
    balances[id]
  };
}

Ghost Maps are updated inside ghost { } blocks using the assignment := operator. Include ghost fields in modifies clauses when a public method changes them.

Using Maps in Invariants​

Maps work well in actor invariants for conservation laws and aggregate properties:

persistent actor {
  ghost var permissions : Map<Nat, Bool> = Map.empty();

  invariant Map.card(permissions) >= 0;

  public func grant(user : Nat) : async ()
    modifies permissions
    ensures Map.contains(user, permissions);
  {
    ghost {
      permissions := Map.update(permissions, user, true);
    };
  };
}

Quantifiers with Maps​

Combine Maps with quantifiers for expressive specifications:

map-quantifiers.sr9
// Using quantifiers with Maps
persistent actor {
  public func demo() : async () {
    ghost {
      let m = Map.update(Map.update(Map.empty<Nat, Int>(), 1, 10), 2, 20);
      let dom = Map.domain(m);

      // All keys in domain are in the Map
      assert forall<Nat>(pure func (k : Nat) : Bool =
        Set.contains(k, dom) ==> Map.contains(k, m));

      // There exists a key with value 10
      assert exists<Nat>(pure func (k : Nat) : Bool =
        Map.contains(k, m) and Map.get(m, k) == 10);
    };
  };
}

Common patterns:

  • Use forall over Map.domain(m) to express properties of all keys.
  • Use exists when at least one key must satisfy a condition.
  • Guard Map.get facts with Map.contains when missing keys should not matter.
  • Keep quantified map predicates small; if solver performance degrades, review trigger patterns.

Element Type Restrictions​

Map keys and values must be spec-immutable types. The following are rejected:

  • Mutable records (with var fields)
  • Mutable arrays ([var T])
  • Functions (T -> U)
  • Actors and modules
  • Async types

Opaque/token handles may be map values by identity. A Map<K,H> fact says which handles are present; it does not prove Owner.model(h) stayed unchanged after an owner-module mutator.

map-immutable-reject_reject.sr9
// REJECT: Map keys and values must be immutable types
persistent actor {
  public func demo() : async () {
    ghost {
      // This is rejected: mutable record as Map value
      type MutableBox = { var x : Nat };
      let m : Map<Nat, MutableBox> = Map.empty();
    };
  };
}

Allowed types include primitives (Nat, Int, Bool, Text), immutable records, tuples, variants, and options with immutable element types.

Operation Reference​

OperationSignatureMutates/Consumes InputDescription
Map.empty<K, V>()Map<K, V>-Create empty Map
Map.update(m, k, v)Map<K, V>NoReturn a new Map with key updated
Map.get(m, k)VNoGet value for key
Map.getOr(m, k, d)VNoGet value or default
Map.contains(k, m)BoolNoCheck key membership
Map.domain(m)Set<K>NoGet all keys as Set
Map.range(m)Set<V>NoGet all values as Set
Map.card(m)IntNoCount of entries
Map.remove(m, k)Map<K, V>NoReturn a new Map without key
Map.delete(m, k)(Map<K, V>, Bool)NoRemove key and report whether it existed
Map.take(m, k)(Map<K, V>, ?V)NoRemove key and return the old value if present

The exported operations are ghost trusted wrappers. Their contracts are part of the trusted base, so prefer the documented operations and avoid inventing parallel trusted map APIs unless you need a domain-specific abstraction.

Common Patterns​

Balance Tracking​

ghost {
  var balances : Map<Nat, Nat> = Map.empty();
  let from : Nat = 1;
  let to : Nat = 2;
  let amt : Nat = 10;

  let seeded = Map.update(balances, from, 25);
  let fromBal = Map.getOr(seeded, from, 0);
  let toBal = Map.getOr(seeded, to, 0);
  assert fromBal >= amt;

  let debited = Map.update(seeded, from, fromBal - amt);
  balances := Map.update(debited, to, toBal + amt);
}

Permission Sets​

ghost {
  let admin : Nat = 1;
  let allowed = Map.update(Map.empty<Nat, Bool>(), admin, true);

  assert Map.contains(admin, allowed);
  assert Map.getOr(allowed, admin, false);
}

Counting Occurrences​

ghost var counts : Map<Nat, Nat> = Map.empty();

public func record(id : Nat) : async ()
  modifies counts
  ensures Map.get(counts, id) == Map.getOr(old(counts), id, 0) + 1
{
  ghost {
    let prev = Map.getOr(counts, id, 0);
    counts := Map.update(counts, id, prev + 1);
  };
}

Summary​

  • Maps are specification-only key-value collections
  • Map operations are ghost proof operations over a trusted primitive collection model
  • Create with Map.empty<K, V>(), update with Map.update(m, k, v)
  • Query with Map.get, Map.getOr, Map.contains, Map.domain, Map.card
  • Map.update returns a new Map; all operations leave their input Maps usable
  • Keys and values must be spec-immutable (no mutable fields, arrays, or functions), except opaque/token handles by identity
  • Use ghost Map fields with modifies clauses for actor-level tracking
  • Combine with quantifiers for expressive invariants and postconditions