pure/BMap

Reference for mo:core/pure/BMap in the core library.

BMap is the preferred immutable ordered map for application code that needs structural sharing plus a proof model. Most mutating operations return a new map and preserve the old one; this is persistent data-structure behavior, not actor persistence. Spec.model connects the tree to ghost Map<K, V> facts.

When V is an opaque/token handle, BMap stores the handle identity. Its model can prove key-to-handle facts and let code recover a handle for an owner API call, but it does not grant access to the owner's sealed payload or prove that Owner.model(h) stayed unchanged after a possible owner mutation.

Import

mo:core/pure/BMap

Status

• Pure immutable collection module

Public API

Types

• BMap, Order, Node, Leaf, Internal, SearchResult, InsertResult, DeleteResult, DeleteTopResult, GrowResult, SplitResult, BorrowResult, MergeResult, NodeCursor, IterDirection, IterState, Bound, XSeq, Builder

Values

• btreeOrder
• maxKeys
• minKeys
• maxChildren
• minChildren

Modules

• Spec

Functions

iterKeysXSeq<K, V>(iter : Types.Iter<(K, V)>) : XSeq<K>

Collects iterator or map keys into a persistent BSeq sequence.

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

iterValuesXSeq<K, V>(iter : Types.Iter<(K, V)>) : XSeq<V>

Collects iterator or map values into a persistent BSeq sequence.

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

orderedBy<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : Bool

Checks the predicate described by the return contract.

Contract

ensures size<K, V>(map) <= 1 ==> result;
ensures result == BSeq.sortedBy<K>(iterKeysXSeq<K, V>(entries<K, V>(map)), compare);
ensures result == BSeq.sortedByDesc<K>(iterKeysXSeq<K, V>(reverseEntries<K, V>(map)), compare);

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

isMinKey<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : Bool

Checks the predicate described by the return contract.

Contract

ensures switch (minEntry<K, V>(map)) {
case null { true };
case (?kv) { key == kv.0 ==> result }
};

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

isMaxKey<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : Bool

Checks the predicate described by the return contract.

Contract

ensures switch (maxEntry<K, V>(map)) {
case null { true };
case (?kv) { key == kv.0 ==> result }
};

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

empty<K, V>() : BMap<K, V>

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

Contract

ensures Spec.model(result) == Map.empty<K, V>();
ensures size<K, V>(result) == 0;

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

singleton<K, V>(key : K, value : V) : BMap<K, V>

Constructs a value containing exactly the supplied element or entry.

Contract

ensures Spec.model(result) == Map.update<K, V>(Map.empty<K, V>(), key, value);
ensures size<K, V>(result) == 1;

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

size<K, V>(map : BMap<K, V>) : Nat

Returns the length or cardinality represented by the value.

Contract

ensures result == map.size;

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

isEmpty<K, V>(map : BMap<K, V>) : Bool

Checks the predicate described by the return contract.

Contract

ensures result == (size<K, V>(map) == 0);

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

containsKey<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : Bool

Checks the predicate described by the return contract.

Contract

ensures result == Map.contains<K, V>(key, Spec.model(map));

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

get<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : ?V

Reads the requested value from the structure.

Contract

ensures Map.contains<K, V>(key, Spec.model(map)) ==> result == ?Map.get<K, V>(Spec.model(map), key);
ensures Map.contains<K, V>(key, Spec.model(map)) == false ==> result == null;

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

add<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : BMap<K, V>

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

Contract

requires orderedBy<K, V>(map, compare);
ensures Spec.model(result) == Map.update<K, V>(Spec.model(map), key, value);
ensures size<K, V>(result) ==
(if (Map.contains<K, V>(key, Spec.model(map))) { size<K, V>(map) } else { size<K, V>(map) + 1 });
ensures orderedBy<K, V>(result, compare);

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

insert<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : (BMap<K, V>, Bool)

Returns or applies the corresponding update to the structure.

Contract

requires orderedBy<K, V>(map, compare);
ensures Spec.model(result.0) == Map.update<K, V>(Spec.model(map), key, value);
ensures result.1 == not Map.contains<K, V>(key, Spec.model(map));
ensures size<K, V>(result.0) ==
(if (Map.contains<K, V>(key, Spec.model(map))) { size<K, V>(map) } else { size<K, V>(map) + 1 });
ensures orderedBy<K, V>(result.0, compare);

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

swap<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : (BMap<K, V>, ?V)

Returns or applies the corresponding update to the structure.

Contract

requires orderedBy<K, V>(map, compare);
ensures Spec.model(result.0) == Map.update<K, V>(Spec.model(map), key, value);
ensures result.1 == get<K, V>(map, compare, key);
ensures size<K, V>(result.0) ==
(if (Map.contains<K, V>(key, Spec.model(map))) { size<K, V>(map) } else { size<K, V>(map) + 1 });
ensures orderedBy<K, V>(result.0, compare);

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

replace<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : (BMap<K, V>, ?V)

Returns or applies the corresponding update to the structure.

Contract

requires orderedBy<K, V>(map, compare);
ensures result.1 == get<K, V>(map, compare, key);
ensures result.1 == null ==> Spec.model(result.0) == Spec.model(map);
ensures result.1 != null ==> Spec.model(result.0) == Map.update<K, V>(Spec.model(map), key, value);
ensures size<K, V>(result.0) == size<K, V>(map);
ensures orderedBy<K, V>(result.0, compare);

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

remove<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : BMap<K, V>

Returns the updated collection or value described by the contract.

Contract

requires orderedBy<K, V>(map, compare);
ensures Map.contains<K, V>(key, Spec.model(result)) == false;
ensures Map.contains<K, V>(key, Spec.model(map)) == false ==> Spec.model(result) == Spec.model(map);
ensures size<K, V>(result) == (if (Map.contains<K, V>(key, Spec.model(map))) { size<K, V>(map) - 1 } else { size<K, V>(map) });
ensures orderedBy<K, V>(result, compare);

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

delete<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : (BMap<K, V>, Bool)

Returns the updated collection or value described by the contract.

Contract

requires orderedBy<K, V>(map, compare);
ensures result.1 == Map.contains<K, V>(key, Spec.model(map));
ensures Map.contains<K, V>(key, Spec.model(result.0)) == false;
ensures result.1 == false ==> Spec.model(result.0) == Spec.model(map);
ensures size<K, V>(result.0) == (if (Map.contains<K, V>(key, Spec.model(map))) { size<K, V>(map) - 1 } else { size<K, V>(map) });
ensures orderedBy<K, V>(result.0, compare);

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

take<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : (BMap<K, V>, ?V)

Returns the updated collection or value described by the contract.

Contract

requires orderedBy<K, V>(map, compare);
ensures result.1 == (if (Map.contains<K, V>(key, Spec.model(map))) {
?Map.get<K, V>(Spec.model(map), key)
} else {
null
});
ensures Map.contains<K, V>(key, Spec.model(result.0)) == false;
ensures result.1 == null ==> Spec.model(result.0) == Spec.model(map);
ensures orderedBy<K, V>(result.0, compare);

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

entries<K, V>(map : BMap<K, V>) : Types.Iter<(K, V)>

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

Contract

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

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

reverseEntries<K, V>(map : BMap<K, V>) : Types.Iter<(K, V)>

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

Contract

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

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

keys<K, V>(map : BMap<K, V>) : Types.Iter<K>

Creates an iterator over the map keys or values.

Contract

ensures Spec.iterSet<K>(result) == Map.domain<K, V>(Spec.model(map));

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

values<K, V>(map : BMap<K, V>) : Types.Iter<V>

Creates an iterator over the map keys or values.

Contract

ensures Spec.iterSet<V>(result) == Map.range<K, V>(Spec.model(map));

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

valuesXSeq<K, V>(map : BMap<K, V>) : XSeq<V>

Collects iterator or map values into a persistent BSeq sequence.

Contract

ensures result == iterValuesXSeq<K, V>(entries<K, V>(map));

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

foldValues<K, V, A>(map : BMap<K, V>, base : A, combine : (A, V) -> A) : A

Folds the structure by applying the supplied accumulator function.

Contract

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

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

entriesFrom<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : Types.Iter<(K, V)>

Creates an iterator starting from a key boundary.

Contract

ensures Set.subset<K>(Spec.iterKeys<K, V>(result), Map.domain<K, V>(Spec.model(map)));
ensures Spec.iterKeysLowerBound<K, V>(result, key, compare);
ensures Spec.iterKeysAtOrAbove<K, V>(result, key, compare);

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

reverseEntriesFrom<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : Types.Iter<(K, V)>

Creates an iterator starting from a key boundary.

Contract

ensures Set.subset<K>(Spec.iterKeys<K, V>(result), Map.domain<K, V>(Spec.model(map)));
ensures Spec.iterKeysLowerBound<K, V>(result, key, compare);
ensures Spec.iterKeysAtOrBelow<K, V>(result, key, compare);

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

entriesInRange<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, from : Bound<K>, to : Bound<K>) : Types.Iter<(K, V)>

Creates an iterator restricted to the supplied key range.

Contract

ensures Set.subset<K>(Spec.iterKeys<K, V>(result), Map.domain<K, V>(Spec.model(map)));
ensures Spec.iterKeysInRange<K, V>(result, from, to, compare);

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

reverseEntriesInRange<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, from : Bound<K>, to : Bound<K>) : Types.Iter<(K, V)>

Creates an iterator restricted to the supplied key range.

Contract

ensures Set.subset<K>(Spec.iterKeys<K, V>(result), Map.domain<K, V>(Spec.model(map)));
ensures Spec.iterKeysInRange<K, V>(result, from, to, compare);

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

minEntry<K, V>(map : BMap<K, V>) : ?(K, V)

Returns the smallest or largest map entry when the map is non-empty.

Contract

ensures (size<K, V>(map) == 0) == (result == null);
ensures switch (result) {
case null { true };
case (?kv) {
Map.contains<K, V>(kv.0, Spec.model(map)) and Map.get<K, V>(Spec.model(map), kv.0) == kv.1
}
};

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

maxEntry<K, V>(map : BMap<K, V>) : ?(K, V)

Returns the smallest or largest map entry when the map is non-empty.

Contract

ensures (size<K, V>(map) == 0) == (result == null);
ensures switch (result) {
case null { true };
case (?kv) {
Map.contains<K, V>(kv.0, Spec.model(map)) and Map.get<K, V>(Spec.model(map), kv.0) == kv.1
}
};

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

mapNode<K, V1, V2>(node : Node<K, V1>, f : (K, V1) -> V2) : Node<K, V2>

Transforms the contained values with the supplied function while preserving the documented shape.

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

map<K, V1, V2>(map : BMap<K, V1>, f : (K, V1) -> V2) : BMap<K, V2>

Transforms the contained values with the supplied function while preserving the documented shape.

Contract

ensures size<K, V2>(result) == size<K, V1>(map);

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

foldLeft<K, V, A>(map : BMap<K, V>, base : A, combine : (A, K, V) -> A) : A

Folds the structure by applying the supplied accumulator function.

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

foldRight<K, V, A>(map : BMap<K, V>, base : A, combine : (K, V, A) -> A) : A

Folds the structure by applying the supplied accumulator function.

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

forEach<K, V>(map : BMap<K, V>, operation : (K, V) -> ()) : ()

Runs the supplied callback only for the matching contained value.

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

addList<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, list : Types.Pure.List<(K, V)>) : BMap<K, V>

Returns or applies the corresponding update to the structure.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(result, compare);

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

filter<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, predicate : (K, V) -> Bool) : BMap<K, V>

Keeps or transforms entries according to the supplied predicate/function.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(result, compare);

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

filterMap<K, V1, V2>(map : BMap<K, V1>, compare : (K, K) -> Order, f : (K, V1) -> ?V2) : BMap<K, V2>

Keeps or transforms entries according to the supplied predicate/function.

Contract

requires orderedBy<K, V1>(map, compare);
ensures orderedBy<K, V2>(result, compare);

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

all<K, V>(map : BMap<K, V>, predicate : (K, V) -> Bool) : Bool

Implements the all helper described by its signature and contract.

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

any<K, V>(map : BMap<K, V>, predicate : (K, V) -> Bool) : Bool

Implements the any helper described by its signature and contract.

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

equal<K, V>(map1 : BMap<K, V>, map2 : BMap<K, V>, compareKey : (K, K) -> Order, equalValue : (V, V) -> Bool) : Bool

Compares the supplied values and relates the result to the underlying order.

Use when: code or contracts need an explicit comparison helper instead of an operator.

compare<K, V>(map1 : BMap<K, V>, map2 : BMap<K, V>, compareKey : (K, K) -> Order, compareValue : (V, V) -> Order) : Order

Compares the supplied values and relates the result to the underlying order.

Use when: code or contracts need an explicit comparison helper instead of an operator.

clone<K, V>(map : BMap<K, V>) : BMap<K, V>

Converts or copies the persistent builder/tree representation.

Contract

ensures Spec.model(result) == Spec.model(map);

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

toText<K, V>(map : BMap<K, V>, keyFormat : K -> Text, valueFormat : V -> Text) : Text

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

thaw<K, V>() : Builder<K, V>

Converts or copies the persistent builder/tree representation.

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

thawAppend<K, V>(builder : Builder<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()

Converts or copies the persistent builder/tree representation.

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

freeze<K, V>(builder : Builder<K, V>) : BMap<K, V>

Converts or copies the persistent builder/tree representation.

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

fromIter<K, V>(iter : Types.Iter<(K, V)>, compare : (K, K) -> Order) : BMap<K, V>

Converts between the module type and the target representation.

Contract

ensures orderedBy<K, V>(result, compare);

Use when: crossing between this module's value and another representation.

toArray<K, V>(map : BMap<K, V>) : [(K, V)]

Converts between the module type and the target representation.

For V values that are opaque/token handles, this operation is not currently accepted by the verifier. BMap.toArray over handle values needs a dedicated immutable array element identity model; until that exists, handle-carrying calls reject at source lowering.

Contract

ensures result.size() == map.size;

Use when: crossing between this module's value and another representation.

fromArray<K, V>(array : [(K, V)], compare : (K, K) -> Order) : BMap<K, V>

Converts between the module type and the target representation.

Contract

ensures orderedBy<K, V>(result, compare);

Use when: crossing between this module's value and another representation.

assertValid<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : ()

Provides a diagnostic helper for validating or inspecting the B+tree structure.

Contract

ensures orderedBy<K, V>(map, compare);

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

debugPrint<K, V>(map : BMap<K, V>, keyFormat : K -> Text, valueFormat : V -> Text) : ()

Provides a diagnostic helper for validating or inspecting the B+tree structure.

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

treeDepth<K, V>(map : BMap<K, V>) : Nat

Provides a diagnostic helper for validating or inspecting the B+tree structure.

Contract

ensures result >= 1;

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

nodeCount<K, V>(map : BMap<K, V>) : Nat

Provides a diagnostic helper for validating or inspecting the B+tree structure.

Contract

ensures result >= 1;

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

Lemmas

sortedBy_take<K>(seq : XSeq<K>, compare : (K, K) -> Order, n : Int) : ()

Establishes BSeq.sortedBy<K>(BSeq.take<K>(seq, n), compare) in the current proof context.

Contract

requires n >= 0;
requires BSeq.sortedBy<K>(seq, compare);
ensures BSeq.sortedBy<K>(BSeq.take<K>(seq, n), compare);

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

sortedByDesc_take<K>(seq : XSeq<K>, compare : (K, K) -> Order, n : Int) : ()

Establishes BSeq.sortedByDesc<K>(BSeq.take<K>(seq, n), compare) in the current proof context.

Contract

requires n >= 0;
requires BSeq.sortedByDesc<K>(seq, compare);
ensures BSeq.sortedByDesc<K>(BSeq.take<K>(seq, n), compare);

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

orderedBy_empty<K, V>(compare : (K, K) -> Order) : ()

Establishes orderedBy<K, V>(empty<K, V>(), compare) in the current proof context.

Contract

ensures orderedBy<K, V>(empty<K, V>(), compare);

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

orderedBy_singleton<K, V>(compare : (K, K) -> Order, key : K, value : V) : ()

Establishes orderedBy<K, V>(singleton<K, V>(key, value), compare) in the current proof context.

Contract

ensures orderedBy<K, V>(singleton<K, V>(key, value), compare);

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

remove_preserves_get<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, other : K) : ()

Establishes get<K, V>(remove<K, V>(map, compare, key), compare, other) == get<K, V>(map, compare, other) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
requires other != key;
ensures get<K, V>(remove<K, V>(map, compare, key), compare, other) ==
get<K, V>(map, compare, other);

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

delete_preserves_get<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, other : K) : ()

Establishes get<K, V>(delete<K, V>(map, compare, key).0, compare, other) == get<K, V>(map, compare, other) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
requires other != key;
ensures get<K, V>(delete<K, V>(map, compare, key).0, compare, other) ==
get<K, V>(map, compare, other);

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

orderedBy_add<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()

Establishes orderedBy<K, V>(add<K, V>(map, compare, key, value), compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(add<K, V>(map, compare, key, value), compare);

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

orderedBy_insert<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()

Establishes orderedBy<K, V>(insert<K, V>(map, compare, key, value).0, compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(insert<K, V>(map, compare, key, value).0, compare);

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

orderedBy_swap<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()

Establishes orderedBy<K, V>(swap<K, V>(map, compare, key, value).0, compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(swap<K, V>(map, compare, key, value).0, compare);

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

orderedBy_replace<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K, value : V) : ()

Establishes orderedBy<K, V>(replace<K, V>(map, compare, key, value).0, compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(replace<K, V>(map, compare, key, value).0, compare);

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

orderedBy_remove<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : ()

Establishes orderedBy<K, V>(remove<K, V>(map, compare, key), compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(remove<K, V>(map, compare, key), compare);

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

orderedBy_delete<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : ()

Establishes orderedBy<K, V>(delete<K, V>(map, compare, key).0, compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(delete<K, V>(map, compare, key).0, compare);

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

orderedBy_take<K, V>(map : BMap<K, V>, compare : (K, K) -> Order, key : K) : ()

Establishes orderedBy<K, V>(take<K, V>(map, compare, key).0, compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures orderedBy<K, V>(take<K, V>(map, compare, key).0, compare);

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

entries_sorted<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : ()

Establishes BSeq.sortedBy<K>(iterKeysXSeq<K, V>(entries<K, V>(map)), compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures BSeq.sortedBy<K>(iterKeysXSeq<K, V>(entries<K, V>(map)), compare);

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

reverseEntries_sorted<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : ()

Establishes BSeq.sortedByDesc<K>(iterKeysXSeq<K, V>(reverseEntries<K, V>(map)), compare) in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures BSeq.sortedByDesc<K>(iterKeysXSeq<K, V>(reverseEntries<K, V>(map)), compare);

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

entries_xseq_in_domain<K, V>(map : BMap<K, V>) : ()

Establishes the listed proof facts in the current verification context.

Contract

ensures Spec.xseqInDomain<K, V>(iterKeysXSeq<K, V>(entries<K, V>(map)), map);
ensures Spec.xseqInDomain<K, V>(iterKeysXSeq<K, V>(reverseEntries<K, V>(map)), map);

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

entrySnapshot_len<K, V>(keys : XSeq<K>, values : XSeq<V>, map : BMap<K, V>) : ()

Establishes that an exact entry snapshot has one key and one value for each map entry.

Contract

requires Spec.entrySnapshot<K, V>(keys, values, map);
ensures BSeq.len<K>(keys) == size<K, V>(map);
ensures BSeq.len<V>(values) == size<K, V>(map);

Use when: a proof needs cardinality from a previously produced entries or reverseEntries snapshot.

entrySnapshot_get<K, V>(keys : XSeq<K>, values : XSeq<V>, map : BMap<K, V>, i : Int) : ()

Establishes the key/value pairing for one index of an exact entry snapshot.

Contract

requires Spec.entrySnapshot<K, V>(keys, values, map);
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), Spec.model(map));
ensures Map.get<K, V>(Spec.model(map), BSeq.get<K>(keys, i)) ==
  BSeq.get<V>(values, i);

Use when: a proof needs to connect an enumerated value to Map.get(model, key).

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

Establishes duplicate-free keys for two distinct indices in an exact 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 map entries.

minEntry_is_min<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : ()

Establishes switch (minEntry<K, V>(map)) { case null { true }; case (?kv) { isMinKey<K, V>(map, compare, kv.0) } } in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures switch (minEntry<K, V>(map)) {
case null { true };
case (?kv) { isMinKey<K, V>(map, compare, kv.0) }
};

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

maxEntry_is_max<K, V>(map : BMap<K, V>, compare : (K, K) -> Order) : ()

Establishes switch (maxEntry<K, V>(map)) { case null { true }; case (?kv) { isMaxKey<K, V>(map, compare, kv.0) } } in the current proof context.

Contract

requires orderedBy<K, V>(map, compare);
ensures switch (maxEntry<K, V>(map)) {
case null { true };
case (?kv) { isMaxKey<K, V>(map, compare, kv.0) }
};

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

Spec Module

Spec Functions

iterSet<T>(iter : Types.Iter<T>) : Set<T>

Returns a ghost abstraction of the iterator for use in specifications.

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

iterKeys<K, V>(iter : Types.Iter<(K, V)>) : Set<K>

Returns a ghost abstraction of the iterator for use in specifications.

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

iterValues<K, V>(iter : Types.Iter<(K, V)>) : Set<V>

Returns a ghost abstraction of the iterator for use in specifications.

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

xseqInDomain<K, V>(seq : XSeq<K>, map : BMap<K, V>) : Bool

Provides a ghost/spec-only abstraction for contracts and proofs.

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

entrySnapshot<K, V>(keys : XSeq<K>, values : XSeq<V>, map : BMap<K, V>) : Bool

Names an exact key/value entry snapshot produced by entries or reverseEntries. It is an identity/value snapshot of the map entries, not authority over opaque payloads stored as values.

Use when: pair this predicate with entrySnapshot_len and entrySnapshot_get.

entryKeysNoDuplicates<K>(keys : XSeq<K>) : Bool

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

Use when: pair this predicate with entrySnapshot_unique_keys.

model<K, V>(map : BMap<K, V>) : Map<K, V>

Returns the abstract ghost model used by contracts and lemmas.

For handle values, this is an identity model: it records which handles are in the map, not a snapshot of each handle owner's payload.

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

iterKeysLowerBound<K, V>(iter : Types.Iter<(K, V)>, key : K, compare : (K, K) -> Order) : Bool

Returns a ghost abstraction of the iterator for use in specifications.

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

iterKeysAtOrAbove<K, V>(iter : Types.Iter<(K, V)>, key : K, compare : (K, K) -> Order) : Bool

Returns a ghost abstraction of the iterator for use in specifications.

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

iterKeysAtOrBelow<K, V>(iter : Types.Iter<(K, V)>, key : K, compare : (K, K) -> Order) : Bool

Returns a ghost abstraction of the iterator for use in specifications.

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

iterKeysInRange<K, V>(iter : Types.Iter<(K, V)>, from : Bound<K>, to : Bound<K>, compare : (K, K) -> Order) : Bool

Returns a ghost abstraction of the iterator for use in specifications.

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

Summary

• Pure immutable collection module under mo:core/pure/BMap.
• Exposes 54 public functions.
• Exposes 18 trusted lemmas.
• Includes 9 spec helpers in Spec.