Skip to main content

Ghost and Axiom Modules

Spec-only modules provide abstract collections and trusted arithmetic lemmas for verification. Use them to state and prove properties; do not treat them as runtime storage or runtime control-flow helpers.

Ghost Collections (mo:core/ghost/*)​

These modules are pure, spec-only wrappers around the verifier's collection theory. Their sizes use verifier integers: Map.card, Set.card, Seq.len, and Multiset.card return Int, so runtime Nat sizes usually need an explicit bridge such as Prim.abs(...).

The collection functions have intentionally specific argument order: Map.get(m, k) reads from a map, while Map.contains(k, m) checks membership. Keeping that order consistent prevents subtle proof failures when moving between ghost collections and runtime collection models.

See the module reference pages for full APIs with types and descriptions:

Axiom Modules (mo:core/axiom/*)​

Axiom modules provide trusted lemmas for arithmetic reasoning. They are intended for proofs, not runtime logic. Calling an axiom lemma adds its ensures fact to the verification context once its requires clauses are proven; it is part of the trusted base, not an independently verified proof.

See the module reference pages for full lemma lists with types and descriptions:

The wrap axiom modules cover conversion laws for fixed-width types even when a matching public runtime numeric module is not part of the current core surface.

Summary​

  • Ghost modules model collections for specs and ghost code.
  • Axiom modules provide trusted arithmetic lemmas for proofs.
  • Treat these APIs as verification-only; they are not intended for runtime logic.