Patterns, Tokens, and Protocol Schema

The core library includes higher-level modules for reusable proof patterns, token values, and protocol metadata. These modules are not basic language primitives, but they are part of core/src and should be preferred over ad hoc copies in examples.

Import Paths

import MapSummary "mo:core/pattern/MapSummary";
import SimpleLedger "mo:core/pattern/SimpleLedger";
import ICRCLedger "mo:core/pattern/ICRCLedger";
import Token "mo:core/token/Fungible";
import Protocol "mo:core/protocol/lib";

Pattern Modules

Pattern modules provide reusable ghost models for common verification tasks:

• MapSummary summarizes Map<K, Nat> proof models with a trusted ghost sum and lemmas for updates. Use it when many contracts need the same "sum of balances" argument.
• SimpleLedger models principal-keyed balances, mint receipts, transfer receipts, and ledger-model transitions. It gives ledger examples a shared vocabulary for supply and transfer invariants.
• ICRCLedger defines the typed actor interface for external ICRC-1/ICRC-2 ledgers and a fromPrincipal helper for client canisters.

Example: Ledger Summary Proof

patterns.sr9

import MapSummary "mo:core/pattern/MapSummary";
import SimpleLedger "mo:core/pattern/SimpleLedger";
import Principal "mo:core/Principal";

module {
  public ghost func credit(
    model : Map<Principal, Nat>,
    user : Principal,
    amount : Nat
  ) : Map<Principal, Nat>
    requires true;
    ensures MapSummary.sum<Principal>(result) ==
      MapSummary.sum<Principal>(model) -
      SimpleLedger.modelBalance(model, user) +
      SimpleLedger.modelBalance(result, user);
  {
    let next = SimpleLedger.mintModel(model, user, amount);
    MapSummary.sum_update<Principal>(
      model,
      user,
      SimpleLedger.modelBalance(next, user)
    );
    next
  };
}

Token Module

token/Fungible defines a runtime token value with identity metadata and mutable balance. Contracts preserve token identity across mint, transfer, and burn operations. Mint authority is based on Runtime.callingModuleId(), not on a caller principal argument, so token-bearing shared APIs must respect the shared-boundary token rules.

Example: Token Metadata Helper

fungible-token.sr9

import Token "mo:core/token/Fungible";

module {
  public func metadata(id : Token.Id) : Nat
    requires true;
    ensures result == Token.unitOfId(id);
  {
    Token.unitOfId(id)
  };
}

Protocol Schema

protocol/lib defines typed records and builders for protocol declarations: roles, trust classes, endpoints, endpoint modes, state bindings, call bindings, companion bindings, temporal properties, and quorum helpers. It is a schema layer for extraction and analysis; it does not prove temporal properties by itself.

Example: Protocol Endpoints

protocol-schema.sr9

import Protocol "mo:core/protocol/lib";

module {
  public type AppRole = { #wallet; #ledger };
  public type AppAction = { #transfer; #balance };

  public func majority(n : Nat) : Nat
    requires true;
    ensures result == Protocol.majorityThreshold(n);
  {
    Protocol.majorityThreshold(n)
  };

  public func endpoints() : [Protocol.Endpoint<AppRole, AppAction>]
    requires true;
    ensures true;
  {
    [
      Protocol.endpoint<AppRole, AppAction>(#wallet, true, #transfer),
      Protocol.endpoint<AppRole, AppAction>(#ledger, false, #balance)
    ]
  };
}

Summary

• Use mo:core/pattern/* for shared ghost proof models instead of repeating custom model helpers.
• Use mo:core/token/Fungible for verified fungible-token values and identity-preserving balance operations.
• Use mo:core/protocol/lib to declare protocol metadata in a stable shape for extraction and analysis.