ghost/Map

Reference for mo:core/ghost/Map in the core library.

This module is ghost-only: values are mathematical proof objects for contracts, ghost code, and lemmas. Operations are persistent and do not consume previous values; cardinalities and sequence lengths use verifier Int, so bridge to runtime Nat sizes explicitly when needed.

Import

mo:core/ghost/Map

Status

• Spec-only module

Public API

Functions

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

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

Contract

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

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

get<K, V>(m : Map<K, V>, k : K) : V

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

Contract

ensures result == Prim.Map.get<K, V>(m, k);

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

getOr<K, V>(m : Map<K, V>, k : K, d : V) : V

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

Contract

ensures result == Prim.Map.getOr<K, V>(m, k, d);
ensures result == (if (Prim.Map.contains<K, V>(k, m)) { Prim.Map.get<K, V>(m, k) } else { d });

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

update<K, V>(m : Map<K, V>, k : K, v : V) : Map<K, V>

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

Contract

ensures result == Prim.Map.update<K, V>(m, k, v);
ensures Prim.Map.contains<K, V>(k, result);
ensures Prim.Map.get<K, V>(result, k) == v;
ensures Prim.Map.card<K, V>(result) ==
(if (Prim.Map.contains<K, V>(k, m)) { Prim.Map.card<K, V>(m) } else { Prim.Map.card<K, V>(m) + 1 });
ensures forall<K>(func (other : K) : Bool =
other != k ==> Prim.Map.contains<K, V>(other, result) == Prim.Map.contains<K, V>(other, m));
ensures forall<K>(func (other : K) : Bool =
(other != k and Prim.Map.contains<K, V>(other, m)) ==>
Prim.Map.get<K, V>(result, other) == Prim.Map.get<K, V>(m, other));

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

contains<K, V>(k : K, m : Map<K, V>) : Bool

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

Contract

ensures result == Prim.Map.contains<K, V>(k, m);

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

domain<K, V>(m : Map<K, V>) : Set<K>

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

Contract

ensures result == Prim.Map.domain<K, V>(m);
ensures forall<K>(func (k : K) : Bool =
Prim.Set.contains<K>(k, result) == Prim.Map.contains<K, V>(k, m));

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

range<K, V>(m : Map<K, V>) : Set<V>

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

Contract

ensures result == Prim.Map.range<K, V>(m);

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

card<K, V>(m : Map<K, V>) : Int

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

Contract

ensures result == Prim.Map.card<K, V>(m);
ensures result >= 0;

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

remove<K, V>(m : Map<K, V>, key : K) : Map<K, V>

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

Contract

ensures Prim.Map.contains<K, V>(key, result) == false;
ensures Prim.Map.contains<K, V>(key, m) == false ==> result == m;
ensures Prim.Map.card<K, V>(result) ==
(if (Prim.Map.contains<K, V>(key, m)) { Prim.Map.card<K, V>(m) - 1 } else { Prim.Map.card<K, V>(m) });
ensures forall<K>(func (k : K) : Bool =
k != key ==> Prim.Map.contains<K, V>(k, result) == Prim.Map.contains<K, V>(k, m));
ensures forall<K>(func (k : K) : Bool =
(k != key and Prim.Map.contains<K, V>(k, m)) ==>
Prim.Map.get<K, V>(result, k) == Prim.Map.get<K, V>(m, k));

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

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

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

Contract

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

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

delete<K, V>(m : Map<K, V>, key : K) : (Map<K, V>, Bool)

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

Contract

ensures result.0 == remove<K, V>(m, key);
ensures result.1 == Prim.Map.contains<K, V>(key, m);
ensures Prim.Map.contains<K, V>(key, result.0) == false;
ensures result.1 == false ==> result.0 == m;

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

take<K, V>(m : Map<K, V>, key : K) : (Map<K, V>, ?V)

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

Contract

ensures result.0 == remove<K, V>(m, key);
ensures result.1 == (if (Prim.Map.contains<K, V>(key, m)) { ?Prim.Map.get<K, V>(m, key) } else { null });
ensures Prim.Map.contains<K, V>(key, result.0) == false;
ensures result.1 == null ==> result.0 == m;

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

Summary

• Spec-only module under mo:core/ghost/Map.
• Exposes 12 public functions.