Token Form
The Token form defines a fungible token with three state fields — balance (Nat per Address), supply (Nat), and owner (Address) — and proves the conservation invariant sum(balance) == supply at compile time. Every transition (transfer, mint, burn) preserves this invariant by algebraic identity: the compiler extracts arithmetic cancellations and co-variance relationships, verifying that no execution path can create or destroy value outside authorized mint/burn operations. The proven invariant is erased from the WASM output, producing zero-overhead verified contracts deployable to CosmWasm, Near, Stylus, and Polkadot.
form Token { state { balance : Nat per Address supply : Nat owner : Address } invariant conservation : sum(balance) == supply transition transfer(from, to, amount) { require balance[from] >= amount balance[from] -= amount balance[to] += amount } -- conservation proven by arithmetic identity -- sum(balance') = sum(balance) - amount + amount = supply transition mint(to, amount) { require msg.sender == owner balance[to] += amount supply += amount } -- sum(balance') = sum(balance) + amount = supply + amount = supply' transition burn(from, amount) { require balance[from] >= amount balance[from] -= amount supply -= amount } -- sum(balance') = sum(balance) - amount = supply - amount = supply' }
State Fields
balance : Nat per Address — maps each address to its token balance. The per keyword declares a mapping over the Address domain.
supply : Nat — the total supply scalar. Must always equal the sum of all balances.
owner : Address — the address authorized to mint new tokens.
Invariant: Conservation
The conservation invariant sum(balance) == supply asserts that the total of all balances across every address equals the supply variable. The compiler proves this holds for every reachable state by analyzing each transition algebraically:
Transfer: balance[from] decreases by amount, balance[to] increases by amount, supply unchanged. Net change to sum(balance) is zero. Conservation holds.
Mint: balance[to] increases by amount, supply increases by amount. Both sides of the equation increase equally. Conservation holds.
Burn: balance[from] decreases by amount, supply decreases by amount. Both sides decrease equally. Conservation holds.
Transitions
transfer(from, to, amount) — moves tokens between addresses. The require clause ensures the sender has sufficient balance. The compiler proves conservation without runtime checks.
mint(to, amount) — creates new tokens. Restricted to the owner address. Supply and balance co-vary to maintain the invariant.
burn(from, amount) — destroys tokens. Requires sufficient balance. Supply and balance co-vary downward.
Frequently Asked Questions
- What invariants does a Token form prove?
- The Token form proves supply conservation: sum(balance) == supply. This guarantees that no tokens can appear or disappear through any sequence of transitions. The compiler verifies this algebraically for transfer, mint, and burn, ensuring conservation holds for all possible execution paths — not just tested ones.
- How does Formagine verify supply conservation for transfers?
- The compiler extracts the algebraic identity sum(balance') = sum(balance) - amount + amount = sum(balance) = supply from the transfer transition. Since supply is unchanged and the subtraction and addition cancel in the sum, conservation holds by arithmetic identity. This proof is performed at compile time and erased from the output — zero runtime cost.
- How does the Token form handle mint and burn while preserving conservation?
- For mint: balance[to] increases by amount and supply increases by amount, so sum(balance') = sum(balance) + amount = supply + amount = supply'. For burn: both decrease by amount. The compiler verifies this algebraic co-variance automatically — both sides of the invariant equation change by the same delta, preserving equality.
- What chains can the Token form compile to?
- The Token form compiles to optimized WASM targeting CosmWasm (Cosmos ecosystem), Near Protocol, Arbitrum Stylus (Ethereum L2), and Polkadot (ink! contracts). The same form definition produces verified contracts for all targets with identical invariant guarantees.