Synthetic demo datademo

Every block, transaction, address and hash on this chain is generated from a fixed seed. None of them exists on any network, and none of these values can be looked up anywhere else. The execution trace is real — it is a recorded Noir program — but it is not the execution of the transaction it is published under.

Home/demo/0xe94e…31c5/code

Verified source

0xe94e…31c5

0xe94e51c6559200ab5b4bf9a083b48c2944ff31c5

Verification

Code hash: 0xe8f00ea3188fd4b75f8383ca071121c8f3c4ad17
Status: full match
Provider: demo-vendored
Compiler: nargo 1.0.0-beta.26
Language: noir
Bundle: sha1:616e94b1327a459db332c9a18b4f78b407d5a78a

Sources

Nargo.toml Prover.toml src/ledger.nr src/main.nr

Nargo.toml7 lines

[package]
name = "tour_constraints"
type = "bin"
authors = ["BlockTracer capability tour"]
[dependencies]

Prover.toml3 lines

opening = "120"
transfer_amount = "30"

src/ledger.nr24 lines

// 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
    }
}

src/main.nr77 lines

// 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
}

This is a circuit, not a contract. It declares no ABI and no storage layout, so there is no interface list and no slot mapping to show. The source above is the whole of what it publishes.

Deployments

This code is deployed at one address. Any other address running the same bytecode would appear here too, already verified.