Skip to main content

Core Library Overview

The core library provides the standard modules that Sector9 programs use for basic types, collections, system APIs, reusable proof patterns, and verified runtime helpers.

Import Paths​

Core modules are imported with the mo:core prefix:

import Nat "mo:core/Nat";
import Text "mo:core/Text";
import Runtime "mo:core/Runtime";
import Token "mo:core/token/Fungible";

Subdirectories map to paths such as:

  • mo:core/pure/BMap
  • mo:core/mutable/MBMap
  • mo:core/ghost/Seq
  • mo:core/axiom/Nat
  • mo:core/pattern/MapSummary
  • mo:core/pattern/ICRCLedger
  • mo:core/token/Fungible
  • mo:core/protocol/lib

Runtime vs Spec-Only​

  • Runtime modules are usable in normal code (for example, Nat, Text, Runtime).
  • Spec-only modules are meant for contracts, ghost code, and proofs. These live under mo:core/ghost and mo:core/axiom.
  • Pattern modules combine reusable ghost models and lemmas for common proof shapes, such as ledgers and map summaries. They are useful when a contract needs a stable model instead of re-deriving collection facts in every module.

Many runtime modules also provide a nested Spec module with trusted functions for specifications. Treat those functions like proof interfaces: they describe the model that verification uses, while runtime code continues to use the ordinary module API.

When running the examples directly from the repository, include the core package:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --package core ./core/src --check docs/examples/08-core-library/nat-int.sr9

Module Map​

Use these pages as entry points:

Summary​

  • Import core modules with mo:core/<Module>.
  • Spec-only APIs live under mo:core/ghost and mo:core/axiom.
  • Higher-level helpers live under mo:core/pattern, mo:core/token, and mo:core/protocol.
  • The pages below group modules by responsibility for fast lookup.