Skip to main content

mutable/MBMap

Reference for mo:core/mutable/MBMap in the core library.

MBMap is a mutable facade over the immutable B+tree map. Its contracts keep a ghost Map<K, V> model attached to the mutable memory object, so updates can be verified while implementation code uses in-place-style operations.

When V is an opaque/token handle, MBMap stores and returns handle identities. Its model tracks map structure and key-to-handle facts; it does not grant payload access or prove that the owner model of a stored handle is stable after an owner-module mutation.

Import​

mo:core/mutable/MBMap

Status​

  • Mutable module

Public API​

Types​

  • Order, Iter, MapMem

Modules​

  • Spec

Functions​

model<K, V>(m : MapMem<K, V>) : Map<K, V>​

Returns the abstract ghost model used by contracts and lemmas.

For handle values, this is an identity model over the stored handles, not a snapshot of each handle owner's payload.

Contract

ensures result == m.model;

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

orderedBy<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order) : Bool​

Checks the predicate described by the return contract.

Contract

ensures result == PureMap.orderedBy<K, V>(m.root, compare);
ensures model<K, V>(m) == Map.empty<K, V>() ==> result;

Use when: code or specifications need this operation with the documented contract.

empty<K, V>() : MapMem<K, V>​

Constructs the empty value for this module's data structure.

Contract

ensures model<K, V>(result) == Map.empty<K, V>();
ensures Map.card<K, V>(model<K, V>(result)) == 0;
ensures forall<K>(func (k : K) : Bool =
Map.contains<K, V>(k, model<K, V>(result)) == false);
ensures Prim.abs(Map.card<K, V>(model<K, V>(result))) == 0;

Use when: code or specifications need this operation with the documented contract.

size<K, V>(m : MapMem<K, V>) : Nat​

Returns the length or cardinality represented by the value.

Contract

ensures result == PureMap.size<K, V>(m.root);
ensures result == Prim.abs(Map.card<K, V>(model<K, V>(m)));

Use when: code or specifications need this operation with the documented contract.

isEmpty<K, V>(m : MapMem<K, V>) : Bool​

Checks the predicate described by the return contract.

Contract

ensures result == PureMap.isEmpty<K, V>(m.root);
ensures result == (Prim.abs(Map.card<K, V>(model<K, V>(m))) == 0);

Use when: a branch condition or contract needs this predicate as a named fact.

get<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K) : ?V​

Reads the requested value from the structure.

Contract

requires orderedBy<K, V>(m, compare);
ensures Map.contains<K, V>(key, model<K, V>(m)) == true ==>
result == ?Map.get<K, V>(model<K, V>(m), key);
ensures Map.contains<K, V>(key, model<K, V>(m)) == false ==> result == null;
ensures model<K, V>(m) == old(model<K, V>(m));
ensures orderedBy<K, V>(m, compare);

Use when: reading this value is part of an implementation or postcondition.

contains<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K) : Bool​

Checks the predicate described by the return contract.

Contract

requires orderedBy<K, V>(m, compare);
ensures result == Map.contains<K, V>(key, model<K, V>(m));
ensures model<K, V>(m) == old(model<K, V>(m));
ensures orderedBy<K, V>(m, compare);

Use when: a branch condition or contract needs this predicate as a named fact.

getOr<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K, default : V) : V​

Reads the requested value from the structure.

Contract

requires orderedBy<K, V>(m, compare);
ensures result == Map.getOr<K, V>(model<K, V>(m), key, default);
ensures model<K, V>(m) == old(model<K, V>(m));
ensures orderedBy<K, V>(m, compare);

Use when: reading this value is part of an implementation or postcondition.

getPresent<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K, default : V) : V​

Reads the requested value from the structure.

Contract

requires orderedBy<K, V>(m, compare);
requires Map.contains<K, V>(key, model<K, V>(m));
ensures result == Map.get<K, V>(model<K, V>(m), key);
ensures model<K, V>(m) == old(model<K, V>(m));
ensures orderedBy<K, V>(m, compare);

Use when: reading this value is part of an implementation or postcondition.

add<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()​

Inserts or replaces the key/value entry while preserving the map model.

Contract

requires orderedBy<K, V>(m, compare);
ensures model<K, V>(m) == Map.update<K, V>(old(model<K, V>(m)), key, value);
ensures Map.contains<K, V>(key, model<K, V>(m));
ensures forall<K>(func (k : K) : Bool =
k != key ==> Map.contains<K, V>(k, model<K, V>(m))
== Map.contains<K, V>(k, old(model<K, V>(m))));
ensures forall<K>(func (k : K) : Bool =
(k != key and Map.contains<K, V>(k, old(model<K, V>(m)))) ==>
Map.get<K, V>(model<K, V>(m), k) == Map.get<K, V>(old(model<K, V>(m)), k));
ensures Map.contains<K, V>(key, old(model<K, V>(m))) == false ==>
Prim.abs(Map.card<K, V>(model<K, V>(m))) ==
Prim.abs(Map.card<K, V>(old(model<K, V>(m)))) + 1;
ensures Map.contains<K, V>(key, old(model<K, V>(m))) == true ==>
Prim.abs(Map.card<K, V>(model<K, V>(m))) ==
Prim.abs(Map.card<K, V>(old(model<K, V>(m))));
ensures orderedBy<K, V>(m, compare);

Use when: the postcondition must relate the updated value to the previous one.

remove<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K) : ()​

Returns the updated collection or value described by the contract.

Contract

requires orderedBy<K, V>(m, compare);
ensures model<K, V>(m) == Spec.modelRemove<K, V>(old(model<K, V>(m)), key);
ensures Map.contains<K, V>(key, model<K, V>(m)) == false;
ensures forall<K>(func (k : K) : Bool =
k != key ==> Map.contains<K, V>(k, model<K, V>(m))
== Map.contains<K, V>(k, old(model<K, V>(m))));
ensures forall<K>(func (k : K) : Bool =
(k != key and Map.contains<K, V>(k, old(model<K, V>(m)))) ==>
Map.get<K, V>(model<K, V>(m), k) == Map.get<K, V>(old(model<K, V>(m)), k));
ensures Map.contains<K, V>(key, old(model<K, V>(m))) == false ==>
model<K, V>(m) == old(model<K, V>(m));
ensures Map.contains<K, V>(key, old(model<K, V>(m))) == true ==>
Prim.abs(Map.card<K, V>(old(model<K, V>(m)))) ==
Prim.abs(Map.card<K, V>(model<K, V>(m))) + 1;
ensures Map.contains<K, V>(key, old(model<K, V>(m))) == false ==>
Prim.abs(Map.card<K, V>(model<K, V>(m))) ==
Prim.abs(Map.card<K, V>(old(model<K, V>(m))));
ensures orderedBy<K, V>(m, compare);

Use when: the postcondition must relate the updated value to the previous one.

putOption<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order, key : K, next : ?V) : ()​

Returns or applies the corresponding update to the structure.

Contract

requires orderedBy<K, V>(m, compare);
ensures model<K, V>(m) == Spec.modelPutOption<K, V>(old(model<K, V>(m)), key, next);
ensures switch (next) {
case null { Map.contains<K, V>(key, model<K, V>(m)) == false };
case (? value) {
Map.contains<K, V>(key, model<K, V>(m)) and
Map.get<K, V>(model<K, V>(m), key) == value
}
};
ensures forall<K>(func (k : K) : Bool =
k != key ==> Map.contains<K, V>(k, model<K, V>(m))
== Map.contains<K, V>(k, old(model<K, V>(m))));
ensures forall<K>(func (k : K) : Bool =
(k != key and Map.contains<K, V>(k, old(model<K, V>(m)))) ==>
Map.get<K, V>(model<K, V>(m), k) == Map.get<K, V>(old(model<K, V>(m)), k));
ensures orderedBy<K, V>(m, compare);

Use when: the postcondition must relate the updated value to the previous one.

entries<K, V>(m : MapMem<K, V>) : Iter<(K, V)>​

Creates an iterator over map entries in forward or reverse order.

Contract

ensures PureMap.Spec.iterKeys<K, V>(result) == Map.domain<K, V>(model<K, V>(m));
ensures PureMap.Spec.iterValues<K, V>(result) == Map.range<K, V>(model<K, V>(m));
ensures Spec.entrySnapshot<K, V>(
  PureMap.iterKeysXSeq<K, V>(result),
  PureMap.iterValuesXSeq<K, V>(result),
  model<K, V>(m)
);
ensures Spec.entryKeysNoDuplicates<K>(PureMap.iterKeysXSeq<K, V>(result));
ensures BSeq.len<K>(PureMap.iterKeysXSeq<K, V>(result)) == size<K, V>(m);
ensures BSeq.len<V>(PureMap.iterValuesXSeq<K, V>(result)) == size<K, V>(m);
ensures model<K, V>(m) == old(model<K, V>(m));

Use when: code or specifications need this operation with the documented contract.

keysXSeq<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order) : BSeq.XSeq<K>​

Collects iterator or map keys into a persistent BSeq sequence.

Contract

requires orderedBy<K, V>(m, compare);
ensures result == PureMap.iterKeysXSeq<K, V>(PureMap.entries<K, V>(m.root));
ensures model<K, V>(m) == old(model<K, V>(m));
ensures orderedBy<K, V>(m, compare);

Use when: code or specifications need this operation with the documented contract.

valuesXSeq<K, V>(m : MapMem<K, V>) : BSeq.XSeq<V>​

Collects iterator or map values into a persistent BSeq sequence.

Contract

ensures result == PureMap.valuesXSeq<K, V>(m.root);

Use when: code or specifications need this operation with the documented contract.

foldLeft<K, V, A>(m : MapMem<K, V>, base : A, combine : (A, K, V) -> A) : A​

Folds the structure by applying the supplied accumulator function.

Contract

ensures result == PureMap.foldLeft<K, V, A>(m.root, base, combine);
ensures size<K, V>(m) == 0 ==> result == base;

Use when: code or specifications need this operation with the documented contract.

foldValues<K, V, A>(m : MapMem<K, V>, base : A, combine : (A, V) -> A) : A​

Folds the structure by applying the supplied accumulator function.

Contract

ensures result == PureMap.foldValues<K, V, A>(m.root, base, combine);
ensures result == BSeq.foldLeft<V, A>(valuesXSeq<K, V>(m), base, combine);
ensures size<K, V>(m) == 0 ==> result == base;

Use when: code or specifications need this operation with the documented contract.

Lemmas​

orderedBy_model_empty<K, V>(m : MapMem<K, V>, compare : (K, K) -> Order) : ()​

Establishes the listed proof facts in the current verification context.

Contract

requires model<K, V>(m) == Map.empty<K, V>();
ensures orderedBy<K, V>(m, compare);
ensures model<K, V>(m) == old(model<K, V>(m));

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

entrySnapshot_len<K, V>(keys : PureMap.XSeq<K>, values : PureMap.XSeq<V>, snapshot : Map<K, V>) : ()​

Establishes the cardinality of a mutable-map entry snapshot against the call-time model value that produced it.

Contract

requires Spec.entrySnapshot<K, V>(keys, values, snapshot);
ensures BSeq.len<K>(keys) == Prim.abs(Map.card<K, V>(snapshot));
ensures BSeq.len<V>(values) == Prim.abs(Map.card<K, V>(snapshot));

Use when: a proof needs the snapshot epoch explicitly instead of the live mutable object.

entrySnapshot_get<K, V>(keys : PureMap.XSeq<K>, values : PureMap.XSeq<V>, snapshot : Map<K, V>, i : Int) : ()​

Establishes the key/value pairing for one index of a mutable-map entry snapshot.

Contract

requires Spec.entrySnapshot<K, V>(keys, values, snapshot);
requires i >= 0;
requires i < BSeq.len<K>(keys);
requires i < BSeq.len<V>(values);
ensures Map.contains<K, V>(BSeq.get<K>(keys, i), snapshot);
ensures Map.get<K, V>(snapshot, BSeq.get<K>(keys, i)) ==
  BSeq.get<V>(values, i);

Use when: a proof needs to relate enumerated entries to the call-time model.

entrySnapshot_unique_keys<K, V>(keys : PureMap.XSeq<K>, i : Int, j : Int) : ()​

Establishes duplicate-free keys for two distinct indices in an entry snapshot.

Contract

requires Spec.entryKeysNoDuplicates<K>(keys);
requires i >= 0;
requires j >= 0;
requires i < BSeq.len<K>(keys);
requires j < BSeq.len<K>(keys);
requires i != j;
ensures BSeq.get<K>(keys, i) != BSeq.get<K>(keys, j);

Use when: a proof needs no-duplicate-key reasoning over enumerated mutable-map entries.

Spec Module​

Spec Functions​

modelRemove<K, V>(m : Map<K, V>, key : K) : Map<K, V>​

Returns the abstract ghost model used by contracts and lemmas.

Contract

ensures Map.contains<K, V>(key, result) == false;
ensures Map.contains<K, V>(key, m) == false ==> result == m;
ensures forall<K>(func (k : K) : Bool =
k != key ==> Map.contains<K, V>(k, result) == Map.contains<K, V>(k, m));
ensures forall<K>(func (k : K) : Bool =
(k != key and Map.contains<K, V>(k, m)) ==>
Map.get<K, V>(result, k) == Map.get<K, V>(m, k));

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

modelPutOption<K, V>(m : Map<K, V>, key : K, next : ?V) : Map<K, V>​

Returns the abstract ghost model used by contracts and lemmas.

Contract

ensures switch (next) {
case null { result == modelRemove<K, V>(m, key) };
case (? value) { result == Map.update<K, V>(m, key, value) }
};
ensures switch (next) {
case null { Map.contains<K, V>(key, result) == false };
case (? value) {
Map.contains<K, V>(key, result) and
Map.get<K, V>(result, key) == value
}
};
ensures forall<K>(func (k : K) : Bool =
k != key ==> Map.contains<K, V>(k, result) == Map.contains<K, V>(k, m));
ensures forall<K>(func (k : K) : Bool =
(k != key and Map.contains<K, V>(k, m)) ==>
Map.get<K, V>(result, k) == Map.get<K, V>(m, k));

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

entrySnapshot<K, V>(keys : PureMap.XSeq<K>, values : PureMap.XSeq<V>, snapshot : Map<K, V>) : Bool​

Names an exact entry snapshot for the specific call-time Map<K, V> model captured by MBMap.entries.

Use when: keep mutable-map snapshot facts tied to an explicit model epoch.

entryKeysNoDuplicates<K>(keys : PureMap.XSeq<K>) : Bool​

Names the duplicate-free key property of a mutable-map entry snapshot.

Use when: pair this predicate with entrySnapshot_unique_keys.

Summary​

  • Mutable module under mo:core/mutable/MBMap.
  • Exposes 20 public functions and lemmas.
  • Includes 4 spec helpers in Spec.