Token Systems

Proving conservation laws, mint/burn accounting, and transfer safety for token contracts.

Token systems are among the most critical smart contracts to verify. A bug that creates tokens from nothing or destroys them incorrectly can have catastrophic financial consequences. Sector9 provides powerful tools to prove these properties statically.

If you want module-owned token types and verified cross-canister calls, see Digital Asset System Overview.

For exported actor methods, put caller-controlled guards in both entry_requires and requires: entry_requires is the runtime entry check, while requires is the logical verifier precondition. A public method with nontrivial requires but no entry_requires is rejected in Viper mode.

Conservation Laws

The fundamental property of any token system is conservation: tokens cannot be created or destroyed except through explicit mint and burn operations. You express this using persistent state and invariants.

Basic Conservation Pattern

Track total deposits and withdrawals with persistent variables that survive upgrades:

token-conservation-basic.sr9

// Basic token conservation pattern
persistent actor {
  var balance : Nat = 0;
  var totalMinted : Nat = 0;
  var totalBurned : Nat = 0;

  // Conservation invariant: minted tokens are either live or burned
  invariant balance + totalBurned == totalMinted;

  public func mint(amount : Nat) : async ()
    modifies balance, totalMinted
    reads totalBurned
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;
    ensures totalMinted == old(totalMinted) + amount;
  {
    balance += amount;
    totalMinted += amount;
  };

  public func burn(amount : Nat) : async ()
    modifies balance, totalBurned
    reads totalMinted
    entry_requires amount > 0;
    entry_requires amount <= balance;
    requires amount > 0;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
    ensures totalBurned == old(totalBurned) + amount;
  {
    balance -= amount;
    totalBurned += amount;
  };
}

The invariant balance + totalBurned == totalMinted states the conservation law without relying on a Nat subtraction in the invariant itself: every minted token is either live or burned. The verifier checks this after every public function using the same actor invariant preservation rule as any other persistent state.

Why Persistent State?

Variables like totalSupply, totalMinted, totalBurned, and balances are essential runtime data that must:

• Persist across canister upgrades
• Be queryable by users and other canisters
• Accurately reflect the actual token accounting

These should always be regular persistent variables, not ghost state. Ghost state is appropriate for verification-only quantities that don't need to exist at runtime.

Mint and Burn Operations

Minting creates new tokens; burning destroys them. Both operations update the accounting state to maintain conservation.

Mint Pattern

token-mint.sr9

// Token minting pattern with supply tracking
persistent actor {
  var balance : Nat = 0;
  var totalSupply : Nat = 0;

  invariant balance == totalSupply;

  public func mint(amount : Nat) : async ()
    modifies balance, totalSupply
    entry_requires amount > 0;
    entry_requires amount <= 1_000_000;
    requires amount > 0;
    requires amount <= 1_000_000;  // Reasonable upper bound
    ensures balance == old(balance) + amount;
    ensures totalSupply == old(totalSupply) + amount;
  {
    balance += amount;
    totalSupply += amount;
  };

  public func getSupply() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  };
}

The postcondition ensures totalSupply == old(totalSupply) + amount proves that minting increases supply by exactly the minted amount. Because verified arithmetic runs in checked mode, production mint APIs should also bound amount when a fixed-width or business cap matters. The old(totalSupply) expression is the method-entry snapshot described in old expressions.

Burn Pattern

token-burn.sr9

// Token burning pattern with supply tracking
persistent actor {
  var balance : Nat = 100;
  var totalSupply : Nat = 100;

  invariant balance == totalSupply;

  public func burn(amount : Nat) : async ()
    modifies balance, totalSupply
    entry_requires amount > 0;
    entry_requires amount <= balance;
    requires amount > 0;
    requires amount <= balance;  // Cannot burn more than exists
    ensures balance == old(balance) - amount;
    ensures totalSupply == old(totalSupply) - amount;
  {
    balance -= amount;
    totalSupply -= amount;
  };

  public func getSupply() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  };
}

The entry_requires amount <= balance guard is the runtime check that prevents burning more than exists. The matching requires clause is the logical precondition used in the proof. The postcondition proves supply decreases by exactly the burned amount.

Sector9 may still warn that a Nat subtraction can trap; that warning is a frontend caution. In the Viper lane, the matching requires amount <= balance is the proof obligation that makes the subtraction safe. See numeric verification for bounds and underflow proofs.

Transfer Safety

Transfers move tokens between accounts without changing total supply. The minimal example below uses two runtime balances; production multi-account ledgers should use runtime collections plus proof models.

token-transfer.sr9

// Token transfer pattern with two runtime balances
persistent actor {
  var senderBalance : Nat = 1000;
  var receiverBalance : Nat = 0;

  public func transfer(amount : Nat) : async ()
    modifies senderBalance, receiverBalance
    entry_requires amount > 0;
    entry_requires amount <= senderBalance;
    requires amount > 0;
    requires amount <= senderBalance;
    ensures senderBalance == old(senderBalance) - amount;
    ensures receiverBalance == old(receiverBalance) + amount;
  {
    senderBalance := senderBalance - amount;
    receiverBalance := receiverBalance + amount;
  };
}

The postconditions prove:

1. Sender balance decreases by exactly amount
2. Receiver balance increases by exactly amount
3. No tokens are created or destroyed in the transfer

For a real ledger, add a conservation invariant over all balances or maintain a ghost summary that mirrors the runtime ledger. The two-balance example keeps the arithmetic local so the transfer proof is visible.

Multi-Account Conservation

For systems with multiple accounts, runtime balances should live in runtime collections. Spec collections (Map, Set, Seq, Multiset) are useful as ghost models for conservation proofs, but they are proof-only and cannot be the deployed account database. A common pattern is: update the runtime collection, update the ghost model in a ghost {} block, and prove the two stay related. See spec collections and collection restrictions before using a proof model for account balances.

AMM Liquidity Tokens

Automated Market Makers (AMMs) issue LP (liquidity provider) tokens when users deposit assets. The LP supply must track deposits correctly.

Minting LP Tokens

When users add liquidity, they receive LP tokens proportional to their contribution:

public func addLiquidity(user : Nat, dx : Nat, dy : Nat) : async Nat
  modifies pools, lpBalances, balancesX, balancesY
  entry_requires dx > 0 and dy > 0;
  entry_requires hasPool(pools, pid);
  entry_requires balanceX(balancesX, user) >= dx;
  entry_requires balanceY(balancesY, user) >= dy;
  requires dx > 0 and dy > 0;
  requires hasPool(pools, pid);
  requires balanceX(balancesX, user) >= dx;
  requires balanceY(balancesY, user) >= dy;
  ensures lpSupply(pools, pid) == old(lpSupply(pools, pid)) + result;
  ensures lpBalance(lpBalances, pid, user) == old(lpBalance(lpBalances, pid, user)) + result;
{
  let minted = calcMinted(p.lpSupply, p.reserveX, p.reserveY, dx, dy);
  // ... update state ...
  minted
}

Burning LP Tokens

When users remove liquidity, their LP tokens are burned and they receive proportional assets:

public func removeLiquidity(user : Nat, lp : Nat) : async (Nat, Nat)
  modifies pools, lpBalances, balancesX, balancesY
  entry_requires lp > 0;
  entry_requires lpBalance(lpBalances, pid, user) >= lp;
  requires lp > 0;
  requires lpBalance(lpBalances, pid, user) >= lp;
  ensures lpSupply(pools, pid) == old(lpSupply(pools, pid)) - lp;
  ensures lpBalance(lpBalances, pid, user) == old(lpBalance(lpBalances, pid, user)) - lp;
{
  let dx = p.reserveX * lp / p.lpSupply;
  let dy = p.reserveY * lp / p.lpSupply;
  // ... update state ...
  (dx, dy)
}

Backing Invariants

For wrapped tokens or stablecoins, prove that circulating supply never exceeds backing reserves:

invariant totalReserves >= circulatingSupply;

This guarantees 1:1 (or better) backing at all times.

Common Mistakes

Missing Preconditions

Always guard against impossible operations:

// Wrong - can burn more than exists
public func burn(amount : Nat) : async () {
  balance -= amount;  // Underflow possible
}

// Correct - precondition prevents underflow
public func burn(amount : Nat) : async ()
  entry_requires amount <= balance;
  requires amount <= balance;
{
  balance -= amount;
}

Incomplete Footprints

List all modified fields in the modifies clause:

// Wrong - missing field in modifies
public func mint(amount : Nat) : async () modifies balance {
  balance += amount;
  totalMinted += amount;  // Error: totalMinted not in modifies
}

// Correct - all fields listed
public func mint(amount : Nat) : async () modifies balance, totalMinted {
  balance += amount;
  totalMinted += amount;
}

Summary

• Use persistent variables to track token accounting (totalMinted, totalBurned, totalSupply, balances) - these survive upgrades
• Express conservation laws as invariants: balance + totalBurned == totalMinted
• Mint operations increase supply; prove with ensures totalSupply == old(totalSupply) + amount
• Burn operations decrease supply; guard public APIs with entry_requires amount <= balance plus the matching logical requires
• Transfers preserve total supply; prove sender decreases and receiver increases by the same amount
• Use runtime collection state for multi-account systems, with ghost Map/Set models for proofs when useful
• Link token authorization to access control and async-sensitive flows to async verification