opening = "120"transfer_amount = "30"// The module holding the account type and the solvency check whose constraint// the recording ends on.pub struct Account { pub id: u32, pub balance: u64,}// Returns the amount by which the two accounts together exceed `floor`.//// `main` calls this with a floor no pair of accounts in that program can reach,// so the assertion on its result is unsatisfiable BY CONSTRUCTION. That is the// point: a reader who steps into this frame can see the two balances and the// floor side by side, and work out for themselves why the next line stops the// execution — rather than being told.pub unconstrained fn solvency_margin(a: Account, b: Account, floor: u64) -> u64 { let combined = a.balance + b.balance; if combined > floor { combined - floor } else { 0 }}// TOUR: constraints, and an execution that fails one//// The subject is what a recording looks like when the program does NOT finish.// This is the case a zero-knowledge debugger exists for: a constraint did not// hold, and the question is which one, on which values, reached from where.//// The recording therefore ENDS at the failing assertion. Everything before it// is ordinary stepping; the last thing in the event log is the assertion's own// message. A tour that only ever showed successful executions would leave the// most useful thing this product does undemonstrated.//// Assertions that HOLD come first and are stepped over normally, so the// contrast between "checked and passed" and "checked and stopped" is visible// inside one recording.mod ledger;use ledger::Account;unconstrained fn transfer(from: Account, to: Account, amount: u64) -> (Account, Account) { // These three hold for every call below, so a reader sees an assertion // being satisfied and stepped past before they see one that is not. assert(amount > 0, "transfer amount must be positive"); assert(from.id != to.id, "cannot transfer to the same account"); assert(from.balance >= amount, "insufficient balance"); let debited = Account { id: from.id, balance: from.balance - amount }; let credited = Account { id: to.id, balance: to.balance + amount }; // The invariant that makes this a ledger: no value is created or destroyed. let before = from.balance + to.balance; let after = debited.balance + credited.balance; assert(before == after, "transfer must conserve the total balance"); (debited, credited)}unconstrained fn main(opening: u64, transfer_amount: pub u64) -> pub u64 { let alice = Account { id: 1, balance: opening }; let bob = Account { id: 2, balance: 50 }; // A format string interpolates bindings, not field accesses, so each // balance is bound before it is printed. let a0 = alice.balance; let b0 = bob.balance; println(f"opening: alice={a0} bob={b0}"); // Two transfers that succeed. Every assertion in `transfer` is evaluated // and holds, twice. let (alice2, bob2) = transfer(alice, bob, transfer_amount); let a1 = alice2.balance; let b1 = bob2.balance; println(f"after 1: alice={a1} bob={b1}"); let (bob3, alice3) = transfer(bob2, alice2, 10); let a2 = alice3.balance; let b2 = bob3.balance; println(f"after 2: alice={a2} bob={b2}"); let total = alice3.balance + bob3.balance; assert(total == opening + 50, "the ledger total is unchanged by transfers"); // ── the failing constraint ──────────────────────────────────────────── // // `ledger::solvency_margin` returns the amount by which the accounts // exceed the reserve floor. The floor is set higher than the accounts can // possibly hold, so this assertion CANNOT hold — it is not a bug that // happens to be here, it is the subject of this program. // // The recording stops on the next line. Its last event log entry is this // message, and the position where the session ends is this assertion's. let margin = ledger::solvency_margin(alice3, bob3, 1_000_000); assert(margin > 0, "accounts must clear the reserve floor"); total}[package]name = "tour_constraints"type = "bin"authors = ["BlockTracer capability tour"][dependencies]The recorded event stream is in the published recording. Reading it needs the replay engine, which this page has not started.
The call structure is in the published recording. Reading it needs the replay engine, which this page has not started.
The recorded values are in the published recording. Reading them needs the replay engine, which this page has not started.