Skip to main content

pattern/MapSummary

Reference for mo:core/pattern/MapSummary in the core library.

Import​

mo:core/pattern/MapSummary

Status​

  • Ghost pattern module
  • Provides reusable summaries for Map<K, Nat> proof models

Purpose​

MapSummary is for specifications that model balances, counters, inventory, voting weight, or other natural-number values in a ghost Map<K, Nat>. It gives proofs a stable aggregate view of the map without forcing each contract to define its own map-sum lemmas.

The module works over the verifier's ghost Map, not the runtime B+tree map in mo:core/pure/BMap.

Public API​

Types​

  • NatSummary - Record with sum : Nat and count : Nat.

Ghost Functions​

  • sum<K>(m : Map<K, Nat>) : Nat - Trusted ghost aggregate for the sum of all values in the map. Empty maps summarize to 0.
  • summary<K>(m : Map<K, Nat>) : NatSummary - Returns both sum(m) and the absolute cardinality of the map.

Lemmas​

  • sum_update<K>(m : Map<K, Nat>, key : K, next : Nat) : () - Relates the sum after Map.update to the previous value at key and the replacement value.
  • sum_bound<K>(m : Map<K, Nat>, key : K) : () - Proves sum(m) is at least the value stored at a present key.
  • summary_update<K>(m : Map<K, Nat>, key : K, next : Nat) : () - Relates both sum and count after an update.

Usage​

Use sum_update when a transition replaces one map entry and your postcondition needs a total-supply or total-balance fact:

let next = Map.update<Principal, Nat>(model, user, newBalance);
MapSummary.sum_update<Principal>(model, user, newBalance);

Summary​

  • Use MapSummary for aggregate facts over ghost Map<K, Nat> models.
  • sum is a trusted ghost abstraction; use the exported lemmas to connect it to map updates.
  • For runtime maps, use mo:core/pure/BMap or mo:core/mutable/MBMap and keep a separate ghost model when you need aggregate proofs.