Proving state operations

StateSync-GKR proves three operations on a sparse Merkle tree: membership, non-membership and a single-leaf update. Each request carries the operation, a private witness from your state store and the public inputs that the proof is bound to. This guide explains how to fill in each part correctly and ends with one complete program that takes a registry slot through its whole lifecycle.

Before you begin#

• Run the Quickstart once, so that you know the build and toolchain work.
• Read Sparse Merkle state if empty, occupied and tombstone leaves are new to you.
• Have a state store that returns a trusted root and the sibling path of any key. The store must hash its tree with the conventions in Tree conventions; otherwise its roots will not match the roots that the verifier recomputes.

Choose an operation#

Membership and non-membership leave the tree unchanged, so their old and new roots are equal. An update changes at most one leaf: both roots are computed from the same sibling path, so the proof also shows that every other slot is unchanged, assuming the hash is collision resistant.

Anatomy of a request#

/// One state-sync proving request handed to the prover stack.
#[derive(Clone, Debug)]
pub struct SyncRequest {
    /// The SMT operation to prove.
    pub operation: SmtOperation,
    /// Private witness (leaf + path) as known by the host state store.
    pub witness: SmtWitness,
    /// Public inputs asserted by the host.
    pub public_inputs: PublicInputs,
}

The operation and witness types come from statesync_gkr::compiler. This abridged listing omits derives and documentation comments:

pub struct AssetId(pub u64);

pub struct LeafPayload {
    pub sync_state: Vec<BaseField>,
    pub identity_digest: KeccakDigestBytes,
}

pub enum LeafState {
    Empty,
    Occupied(LeafPayload),
    Tombstone,
}

pub struct MerklePath {
    pub siblings: Vec<Digest<BaseField>>,
}

pub enum SmtOperation {
    Membership { key: AssetId, payload: LeafPayload },
    NonMembership { key: AssetId },
    Update { key: AssetId, old_leaf: LeafState, new_leaf: LeafState },
}

pub struct SmtWitness {
    pub leaf: LeafState,
    pub path: MerklePath,
}

KeccakDigestBytes is [u8; 32].

Public inputs#

The verifier compares the result's public inputs with the request's, and the transcript absorbs the fields in declaration order. The field set and its order are a frozen interface.

Witness#

Tree conventions#

The engine recomputes roots from the witness, so your state store must build its tree the same way:

• Leaf digest. hash_leaf(&leaf.encode()) on a Poseidon2Gadget created for the instance's leaf bound: Poseidon2Gadget::new(params.leaf_max_fields as usize). The bound sets the width of the zero-padded pre-image: the bound plus one, rounded up to a multiple of eight. A gadget whose bound rounds to a different width hashes the same leaf differently, and a gadget with a smaller bound rejects longer leaves.
• Node digest. compress(&left, &right) on the same gadget.
• Path order. siblings[0] is the sibling at the leaf level, and the last entry is the sibling just below the root. A path has exactly depth entries.
• Position at each level. At level l, bit l of the key, counted from the least significant bit, places the running node. A 0 bit makes it the left child and a 1 bit makes it the right child.
• Unused slots. A never-used slot is the leaf LeafState::Empty, hashed like any other leaf. The engine has no other placeholder for unused slots, so a store that represents them differently cannot produce non-membership proofs that verify.

Key 5 in a tree of depth 3 (binary 101) climbs like this:

The first node is the leaf digest, and the node after the last level is the root. MerklePath::compute_root performs exactly this computation, so you can use it to check what your store returns.

Depth and keys#

SmtParams::depth fixes the tree depth for a prover. The default is 24, which gives 2^24 (16,777,216) slots. The controlled measurements used depths 24, 28 and 32, and the Quickstart uses 4. AssetId wraps a u64, and for a depth below 64 a key must be less than 2^depth: compute_root returns SmtError::KeyOutOfRange for a key at or above 2^depth, and the verifier rejects it. Proof generation does not check the key range, so do not rely on it to catch the error. Keep the depth between 1 and 64; compilation rejects a depth of 0.

Leaf payloads#

LeafState::encode() produces the field elements that are hashed. It starts with a tag (0 for Empty, 1 for Occupied, 2 for Tombstone); for an occupied leaf, the sync-state fields follow, then the 32-byte identity digest packed little-endian into nine 30-bit limbs. The whole encoding must fit within leaf_max_fields, which defaults to 31: one tag, up to 21 sync-state fields and nine limbs. A longer payload fails with SmtError::LeafEncoding. An occupied leaf with zero sync-state fields is valid and still differs from Empty.

Sync-state fields are elements of the KoalaBear field, with modulus p = 2^31 - 2^24 + 1 = 2130706433, and encoding your application's values into them is your responsibility. Use an encoding that cannot map two different values to the same element: inputs at or above p are reduced and can collide. The library packs the identity digest into 30-bit limbs for this reason. The circuit treats the identity digest as opaque bytes. Your application computes it outside the circuit (the source describes it as a Keccak-256 identity digest), and the circuit does not recompute it.

Raising leaf_max_fields allows larger payloads, but it changes every leaf digest and the circuit, so it defines a new configuration with new roots.

A complete program#

The program below keeps a registry of depth 4 whose leaves are all Empty except slot 5, and takes slot 5 through its lifecycle: absent, issued, held, deleted, and absent again. Because every other leaf is Empty, the sibling at each level is the digest of an empty subtree, and one path serves every state of slot 5. The store_root helper stands in for your state store; in production, roots and paths come from the store you trust.

Add the dependency as Installation shows, then save this as src/main.rs:

use std::process::ExitCode;

use statesync_gkr::compiler::{
    AssetId, LayerStrategy, LeafPayload, LeafState, MerklePath, PublicInputs, SmtOperation,
    SmtParams, SmtWitness,
};
use statesync_gkr::primitives::field::{BaseField, PrimeCharacteristicRing};
use statesync_gkr::primitives::hash::{Digest, HashGadget, Poseidon2Gadget};
use statesync_gkr::{StateSyncGkrConfig, StateSyncProver, SyncRequest, SyncResult};

/// Tree depth for this walkthrough. The controlled measurements used 24, 28 and 32.
const DEPTH: u32 = 4;

fn field(value: u32) -> BaseField {
    BaseField::from_u32(value)
}

/// Digest of one leaf state, computed exactly as the circuit computes it.
fn leaf_digest(hasher: &Poseidon2Gadget, leaf: &LeafState) -> Result<Digest<BaseField>, String> {
    hasher
        .hash_leaf(&leaf.encode())
        .map_err(|error| format!("leaf hashing failed: {error:?}"))
}

/// Sibling path of any key in a tree whose other leaves are all `Empty`.
/// Entry 0 is the leaf-level sibling; each level up compresses two copies
/// of the empty subtree below it.
fn empty_tree_path(hasher: &Poseidon2Gadget, depth: u32) -> Result<MerklePath, String> {
    let mut subtree = leaf_digest(hasher, &LeafState::Empty)?;
    let mut siblings = Vec::with_capacity(depth as usize);
    for _ in 0..depth {
        siblings.push(subtree);
        subtree = hasher.compress(&subtree, &subtree);
    }
    Ok(MerklePath { siblings })
}

/// Stand-in for your state store: the root after placing `leaf` at `key`.
fn store_root(
    hasher: &Poseidon2Gadget,
    params: &SmtParams,
    key: AssetId,
    leaf: &LeafState,
    path: &MerklePath,
) -> Result<Digest<BaseField>, String> {
    path.compute_root(hasher, params, key, leaf)
        .map_err(|error| format!("root computation failed: {error:?}"))
}

fn membership_request(
    hasher: &Poseidon2Gadget,
    key: AssetId,
    payload: LeafPayload,
    path: MerklePath,
    root: Digest<BaseField>,
) -> Result<SyncRequest, String> {
    let leaf = LeafState::Occupied(payload.clone());
    let value_digest = leaf_digest(hasher, &leaf)?;
    let operation = SmtOperation::Membership { key, payload };
    let op_kind_tag = PublicInputs::kind_tag(operation.kind());
    Ok(SyncRequest {
        operation,
        witness: SmtWitness { leaf, path },
        public_inputs: PublicInputs {
            old_root: root,
            new_root: root,
            op_kind_tag,
            asset_id: key,
            value_digest,
        },
    })
}

fn non_membership_request(
    hasher: &Poseidon2Gadget,
    key: AssetId,
    stored: LeafState,
    path: MerklePath,
    root: Digest<BaseField>,
) -> Result<SyncRequest, String> {
    if !matches!(stored, LeafState::Empty | LeafState::Tombstone) {
        return Err("non-membership needs the stored Empty or Tombstone leaf".to_owned());
    }
    let value_digest = leaf_digest(hasher, &stored)?;
    let operation = SmtOperation::NonMembership { key };
    let op_kind_tag = PublicInputs::kind_tag(operation.kind());
    Ok(SyncRequest {
        operation,
        witness: SmtWitness { leaf: stored, path },
        public_inputs: PublicInputs {
            old_root: root,
            new_root: root,
            op_kind_tag,
            asset_id: key,
            value_digest,
        },
    })
}

fn update_request(
    hasher: &Poseidon2Gadget,
    key: AssetId,
    old_leaf: LeafState,
    new_leaf: LeafState,
    path: MerklePath,
    old_root: Digest<BaseField>,
    new_root: Digest<BaseField>,
) -> Result<SyncRequest, String> {
    let value_digest = leaf_digest(hasher, &new_leaf)?;
    let operation = SmtOperation::Update {
        key,
        old_leaf: old_leaf.clone(),
        new_leaf,
    };
    let op_kind_tag = PublicInputs::kind_tag(operation.kind());
    Ok(SyncRequest {
        operation,
        witness: SmtWitness { leaf: old_leaf, path },
        public_inputs: PublicInputs {
            old_root,
            new_root,
            op_kind_tag,
            asset_id: key,
            value_digest,
        },
    })
}

/// Prove, then return the result only if the verifier accepts it.
fn prove_checked(prover: &StateSyncProver, request: &SyncRequest) -> Result<SyncResult, String> {
    let result = prover
        .prove_sync_op(request)
        .map_err(|error| format!("proving failed: {error:?}"))?;
    if !prover.verify_sync_op(request, &result) {
        return Err("the proof or its request binding was rejected".to_owned());
    }
    Ok(result)
}

fn run() -> Result<(), String> {
    let params = SmtParams {
        depth: DEPTH,
        ..Default::default()
    };
    let prover = StateSyncProver::new(StateSyncGkrConfig {
        smt: params,
        layer_strategy: LayerStrategy::A,
        ..Default::default()
    });
    let hasher = Poseidon2Gadget::new(params.leaf_max_fields as usize);

    let key = AssetId(5);
    let path = empty_tree_path(&hasher, params.depth)?;
    let empty_root = store_root(&hasher, &params, key, &LeafState::Empty, &path)?;

    // 1. Slot 5 has never been used.
    let absent = non_membership_request(&hasher, key, LeafState::Empty, path.clone(), empty_root)?;
    prove_checked(&prover, &absent)?;
    println!("non-membership (never used): accepted");

    // 2. Issue a bond into slot 5: Empty to Occupied.
    let bond = LeafPayload {
        sync_state: vec![field(1_000_000), field(1)], // outstanding units, status code
        identity_digest: [7_u8; 32],                 // computed off-circuit by the registry
    };
    let issued = LeafState::Occupied(bond.clone());
    let issued_root = store_root(&hasher, &params, key, &issued, &path)?;
    let insert = update_request(
        &hasher,
        key,
        LeafState::Empty,
        issued.clone(),
        path.clone(),
        empty_root,
        issued_root,
    )?;
    prove_checked(&prover, &insert)?;
    println!("update (insertion): accepted");

    // 3. Slot 5 holds exactly this record.
    let held = membership_request(&hasher, key, bond, path.clone(), issued_root)?;
    prove_checked(&prover, &held)?;
    println!("membership: accepted");

    // 4. Redeem the bond: Occupied to Tombstone.
    let deleted_root = store_root(&hasher, &params, key, &LeafState::Tombstone, &path)?;
    let delete = update_request(
        &hasher,
        key,
        issued,
        LeafState::Tombstone,
        path.clone(),
        issued_root,
        deleted_root,
    )?;
    prove_checked(&prover, &delete)?;
    println!("update (deletion): accepted");

    // 5. Slot 5 is absent again; the witness is the stored Tombstone.
    let gone = non_membership_request(&hasher, key, LeafState::Tombstone, path, deleted_root)?;
    prove_checked(&prover, &gone)?;
    println!("non-membership (tombstone): accepted");
    Ok(())
}

fn main() -> ExitCode {
    match run() {
        Ok(()) => ExitCode::SUCCESS,
        Err(error) => {
            eprintln!("state-operations=FAIL: {error}");
            ExitCode::FAILURE
        }
    }
}

Run it with cargo run --release. It prints one line for each request that the verifier accepted:

non-membership (never used): accepted
update (insertion): accepted
membership: accepted
update (deletion): accepted
non-membership (tombstone): accepted

prove_checked follows the rule from the Quickstart: a request counts as proved only after verify_sync_op returns true. The program uses the fresh path to stay short. A service that proves requests repeatedly should prepare each operation kind once; see Prepared execution.

Operation details#

Membership#

Set operation to SmtOperation::Membership { key, payload }, witness.leaf to LeafState::Occupied with the same payload, value_digest to the digest of that occupied leaf, and both roots to the trusted root. The payload therefore appears three times: in the operation, in the witness leaf and, through its digest, in the public inputs. The verifier rejects the request unless all three agree.

Non-membership#

Set operation to SmtOperation::NonMembership { key } and witness.leaf to the leaf your store actually holds: Empty if the slot was never used, Tombstone if it was deleted. value_digest must be the digest of that same state; computing it for Empty while the store holds Tombstone, or the reverse, makes verification fail. Both roots are the trusted root.

The circuit itself checks that the leaf's tag belongs to Empty or Tombstone, so an occupied leaf cannot pass as absent. Both states satisfy non-membership, but they hash differently, so a deleted slot leaves a different root from a never-used one. Because value_digest is public and the digests of Empty and Tombstone are fixed for a given leaf bound, the public inputs also reveal which of the two states the slot is in.

Update#

Set operation to SmtOperation::Update { key, old_leaf, new_leaf }, witness.leaf to old_leaf, witness.path to the siblings (unchanged by the update), old_root and new_root to the roots before and after, and value_digest to the digest of new_leaf.

The operation accepts any pair of leaf states. Insertion (Empty to Occupied), replacement (Occupied to Occupied), deletion (Occupied to Tombstone) and restoration (Tombstone to Occupied) are all uses of this one operation. The engine does not enforce a lifecycle policy: it also proves transitions that your application may forbid, such as Occupied to Empty, which makes a deleted slot look never used, or an update whose old and new leaves are equal. Apply your transition rules before you build the request.

One proof covers one leaf. To prove a sequence of updates to the same tree, build each request against the root that the previous update produced; the engine neither orders requests nor commits them to a store. An atomic change to several leaves under one root transition is not provided.

Check semantics without a proof#

compiler::smt_valid_native evaluates an operation's native semantics directly: the path guards, the leaf condition and the root equations. It compiles no circuit and produces no proof, which makes it a cheap way to turn away a malformed request before you spend time proving it:

use statesync_gkr::SyncRequest;
use statesync_gkr::compiler::{SmtParams, smt_valid_native};
use statesync_gkr::primitives::hash::Poseidon2Gadget;

/// Native semantics check: no circuit and no proof.
pub fn semantics_hold(params: &SmtParams, request: &SyncRequest) -> Result<bool, String> {
    let hasher = Poseidon2Gadget::new(params.leaf_max_fields as usize);
    smt_valid_native(
        &hasher,
        params,
        &request.operation,
        &request.public_inputs.old_root,
        &request.public_inputs.new_root,
        &request.witness,
    )
    .map_err(|error| format!("malformed request: {error:?}"))
}

It returns Ok(false) when the statement does not hold, and an error when the path length, key range or leaf encoding is out of bounds. It does not read op_kind_tag, asset_id or value_digest; only the verifier binds those. A true result does not replace verifying the proof.

Common mistakes#

Errors lists every error type and variant.

Checklist#

• The hash gadget is created for params.leaf_max_fields.
• Roots come from your trusted store, never from a witness that someone sent you.
• op_kind_tag comes from PublicInputs::kind_tag(operation.kind()).
• asset_id equals the operation's key, and the key is below 2^depth.
• Membership and non-membership use the same root for old_root and new_root.
• value_digest hashes the asserted occupied leaf, the stored absent leaf, or the new leaf.
• An update's witness leaf equals its old_leaf.
• Your transition policy runs before you build an update.
• A request is accepted only after verification returns true.

Next steps#

• Prepared execution: prove repeated requests without recompiling the circuit.
• Batching and parallelism: prove many requests on a worker pool.
• Encoding and transport: send a proof to a verifier in another process.
• Production integration: connect the prover to a real state store.