Skip to main content

pattern/SimpleLedger

Reference for mo:core/pattern/SimpleLedger in the core library.

Import​

mo:core/pattern/SimpleLedger

Status​

  • Ghost pattern module
  • Provides reusable balance-model transitions for ledgers keyed by Principal

Purpose​

SimpleLedger is a small proof-model helper for ledger-like canisters. It standardizes the common ghost model:

Map<Principal, Nat>

Missing principals have balance 0. Mint and transfer helpers produce receipt records and updated ghost maps that contracts can refer to in postconditions.

Public API​

Types​

  • MintReceipt - { minted : Nat; before : Nat; after : Nat }.
  • TransferReceipt - Records requested amount, moved amount, and sender/recipient balances before and after a transfer.

Ghost Functions​

  • modelBalance(model : Map<Principal, Nat>, user : Principal) : Nat - Reads a balance from the ghost model, defaulting to 0.
  • mintReceipt(model : Map<Principal, Nat>, user : Principal, amount : Nat) : MintReceipt - Computes the expected mint receipt for a user.
  • mintModel(model : Map<Principal, Nat>, user : Principal, amount : Nat) : Map<Principal, Nat> - Returns the model after minting.
  • transferReceipt(model : Map<Principal, Nat>, from : Principal, to : Principal, amount : Nat) : TransferReceipt - Computes the expected transfer receipt. It moves 0 if from == to or the sender lacks funds.
  • transferModel(model : Map<Principal, Nat>, from : Principal, to : Principal, amount : Nat) : Map<Principal, Nat> - Returns the model after applying the receipt.

Pure Predicates​

  • mintReceiptShape(receipt : MintReceipt, amount : Nat) : Bool - Checks that a mint receipt is internally consistent.
  • transferReceiptShape(receipt : TransferReceipt, amount : Nat) : Bool - Checks that a transfer receipt conserves the moved amount and never moves more than requested.

Usage​

Use this module to keep implementation-specific ledger code separate from the abstract proof model:

let next = SimpleLedger.transferModel(model, caller, to, amount);
let receipt = SimpleLedger.transferReceipt(model, caller, to, amount);

Summary​

  • Use SimpleLedger for ghost ledger models keyed by Principal.
  • Missing users are treated as zero-balance users.
  • Transfers that are self-transfers or underfunded attempts move 0 in the model.