Leave ntrace.

import { PoolReader, RpcClient, loadPoolDeployment } from "@topi/sdk";

const rpc = new RpcClient("https://rpc1.privacy.ethrex.xyz");
const deployment = loadPoolDeployment("deployments/8141/pool.json");
const pool = new PoolReader(rpc, deployment.pool);

// Rebuild the pool's trees from its public events.
const view = await pool.chainView(deployment);
console.log(view.next_leaf, "notes in the pool");

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.28;

import { IShieldedPool } from "topi/interfaces/IShieldedPool.sol";

contract Depositor {
    IShieldedPool immutable pool;

    constructor(IShieldedPool pool_) {
        pool = pool_;
    }

    function deposit(uint256[8] calldata note) external payable {
        pool.deposit{ value: msg.value }(note);
    }
}

cargo build --release

# one key per node, then start the gateway
target/release/topi-node keygen keys/gateway.key
target/release/topi-node run gateway \
  --topology topology.json --key keys/gateway.key

# send a ping through all three hops and back
target/release/topi-client ping \
  --topology topology.json --identity member.id

theorem run_distinct {rootOf : List Nat → Nat} :
    ∀ (s : State) (txs : List (Bool × Bool × Spend × Spend)),
      Distinct s.spent → Distinct (run rootOf s txs).spent
  | _, [], h => h
  | s, (p, q, a, b) :: rest, h =>
    run_distinct _ rest (step_distinct (a := a) (b := b) (p := p) (q := q) h)