Execution Proof Circuit

RM Execution proof
1

Overview

The execution proof is a RISC0 zkVM circuit that verifies a batch of
ARM transactions against a shared commitment tree and nullifier tree. Its output —
the ExecutionProofInstance — is a succinct commitment to the state transition and
to the application data of every resource touched by the batch.

Downstream proofs chain state transitions by matching the new_commitment_root /
new_nullifier_tree_root of one execution proof to the old_commitment_tree_root /
old_nullifier_tree_root of the next.

Witness (ExecutionProofWitness)

The witness is the private input read by the circuit from the RISC0 guest environment.

Field Type Description
transactions Vec<Transaction> Ordered batch of transactions to execute. Each transaction holds one or more Actions, each holding one or more ComplianceUnits and a corresponding set of LogicVerifierInputs.
commitment_tree IncrementalMerkleTree The append-only commitment tree before the batch. Its root is bound to the instance as old_commitment_tree_root.
old_nullifier_tree_root Digest Root of the indexed nullifier tree before the batch.
nullifier_witnesses Vec<InsertionWitness> One InsertionWitness per compliance unit across the entire batch, in tx → action → CU order. Each witness simultaneously proves that its nullifier was absent from the tree and derives the post-insertion root.
batch_aggregation_vk Digest Verifying key for the batch aggregation circuit.
compliance_vk Digest Verifying key for the compliance circuit.

InsertionWitness — embeds a predecessor leaf (lo → hi in the sorted linked-list
structure of the indexed nullifier tree), its Merkle authentication path, and a path for the
new leaf. apply(value, root) proves lo < value < hi (non-membership), rewrites the
predecessor link to (lo → value), inserts (value → hi), and returns the updated root.

Instance (ExecutionProofInstance)

The instance is the public output committed to the RISC0 journal.

Field Type Description
old_commitment_tree_root Digest Commitment tree root before the batch.
old_nullifier_tree_root Digest Nullifier tree root before the batch.
new_commitment_root Digest Commitment tree root after inserting all created commitments.
new_nullifier_tree_root Digest Nullifier tree root after inserting all consumed nullifiers.
consumed_resource_app_data Vec<ResourceAppData> Application data for every consumed resource, in tx → action → CU order.
created_resource_app_data Vec<ResourceAppData> Application data for every created resource, in tx → action → CU order.
batch_aggregation_vk Digest The batch aggregation VK used during verification (forwarded from witness).
compliance_vk Digest The compliance VK used during verification (forwarded from witness).

Each ResourceAppData carries:

Field Description
tag Nullifier (consumed) or commitment (created) digest identifying the resource.
vk Verifying key of the resource’s logic proof.
app_data AppData with resource, discovery, external, and application payload blobs.

Constraints

The circuit enforces five groups of constraints.

1. Batch-wide Nullifier Uniqueness

All consumed nullifiers across all transactions are collected into a flat list in
tx → action → CU order. A sorted copy is checked for adjacent duplicates:

∀ i:  sorted_nullifiers[i] ≠ sorted_nullifiers[i+1]

This prevents double-spends within the batch before any tree update occurs.

Sorting uses only integer comparisons on the [u32; 8] words of each Digest,
which is cheaper in the zkVM than hash-based membership structures (SipHash, used
by HashSet, has no RISC0 hardware accelerator).

2. Delta Proof (per transaction)

For each transaction the circuit verifies that the net value change across all
compliance units is zero:

DeltaProof::verify(delta_msg, proof, delta_instance)

where delta_msg is the concatenation of each compliance unit’s delta_msg and
delta_instance is the elliptic-curve sum of all compliance unit deltas.

3. Batch Aggregation Proof (per transaction)

The aggregation proof asserts that every compliance proof and every logic proof in
the transaction was verified by the batch aggregation circuit. The circuit:

  1. Reconstructs the aggregation instance — for each action:

    a. Builds the ordered tag / logic-ref pairs:
    [consumed_nullifier, created_commitment, …] per compliance unit,
    with corresponding [consumed_logic_ref, created_logic_ref, …].

    b. Computes the action tree root from the tags via a binary Merkle tree.

    c. For each (tag, logic_ref) pair, looks up the matching LogicVerifierInputs and asserts:

    input.verifying_key == logic_ref

    This binds the logic proof VK to what is committed inside the compliance instance.

    d. Serialises a LogicInstance { tag, is_consumed, root, app_data } for each
    resource. is_consumed is true for even-indexed entries (consumed resources)
    and false for odd-indexed entries (created resources).

    e. Combines all compliance instances (as ComplianceInstanceWords) and the logic
    instances / VKs with compliance_vk into the aggregation journal tuple.

  2. Verifies the proof — calls env::verify(batch_aggregation_vk, agg_words),
    which succeeds only if a valid RISC0 receipt produced exactly agg_words as its
    journal under batch_aggregation_vk.

As a by-product of step (d), the circuit collects consumed_resource_app_data and
created_resource_app_data for the instance in the same pass.

4. Nullifier Non-membership and Insertion (per compliance unit)

Using the pre-collected nullifiers and witness.nullifier_witnesses in lock-step:

nullifier_root ← InsertionWitness::apply(nf, nullifier_root)

apply enforces, in sequence:

  1. predecessor.value < nf < predecessor.next_value — proves nf ∉ tree.
  2. The predecessor’s Merkle path authenticates against the current nullifier_root.
  3. The predecessor is rewritten from (lo → hi) to (lo → nf).
  4. A new leaf (nf → hi) is inserted at the correct slot.
  5. The returned digest becomes the new nullifier_root for the next step.

The final value after all compliance units becomes new_nullifier_tree_root.

5. Commitment Insertion (per compliance unit)

For each compliance unit (in the same loop as constraint 4):

commitment_tree.insert(commitment)

insert appends the commitment to the incremental Merkle tree using a
binary-addition carry algorithm on the frontier nodes, growing the tree
automatically if at capacity. After all compliance units,
commitment_tree.root() becomes new_commitment_root.

Data Flow

ExecutionProofWitness
│
├─ step 2 ──► collect nullifiers + commitments (tx → action → CU order)
│              └─ sort-and-dedup check (constraint 1)
│
├─ step 3 ──► for each tx:
│              ├─ delta proof verification          (constraint 2)
│              └─ aggregation_instance_words(tx)
│                  └─ for each action:
│                      collect_action_logic(action)
│                      ├─ action tree root
│                      ├─ verifying_key == logic_ref check  (constraint 3)
│                      ├─ LogicInstance serialisation
│                      └─ ResourceAppData split (consumed / created)
│                  └─ env::verify(batch_aggregation_vk, …)  (constraint 3)
│
├─ step 3c ─► for each (nullifier, commitment, nf_witness):
│              ├─ InsertionWitness::apply   → new nullifier_root  (constraint 4)
│              └─ IncrementalMerkleTree::insert                   (constraint 5)
│
└─ step 4 ──► env::commit(ExecutionProofInstance)

Code is on this branch: GitHub - anoma/arm-risc0 at xuyang/execution_proof · GitHub

cc @vveiln @cwgoes @ArtemG @adrian

1 Like
2

could you open a PR for it

3

sure, execution proof by XuyangSong · Pull Request #217 · anoma/arm-risc0 · GitHub