Exploring the execution proof

RM Execution proof
1

The execution proof performs local and global checks expected from the execution in a verifiable manner by producing a succinct proof of knowledge. This post aims to further develop the idea described here.

Proof stages

We can differentiate between three proof stages characterized by their relationship with the RM:

  • Raw RM proofs - the proofs produced directly by RM for each transaction. Include compliance proofs, logic proofs, and the delta proof
  • Aggregated proof - combines the raw RM proofs into a fixed number of proofs [1]. It can either be a part of internal RM functionality or performed over an RM transaction with raw proofs. For simplicity we assume it is a part of the RM functionality.
  • Execution proof - a proof over multiple transactions that verifies the global execution checks in a verifiable manner

The table below compares some properties of these proofs.

Raw proofs Aggregated proof Execution proof
Scope CU, Action, Transaction Transaction Multiple transactions
Recursive No Yes Yes
Created by RM RM* Not RM
Created by Users, Solvers Users, Solvers Controller

Resource Plasma Assumptions

We discuss the execution proof in the context of Resource Plasma. For the rest of the post we assume the following:

  • Commitments are stored in a Merkle tree CM
  • Nullifiers are stored in a sorted Merkle tree NF
  • The Anoma Contract stores the hash of the current root of the commitment and nullifier trees: currentState = hash(CMroot, NFroot)[2]
  • The underlying RM is the RISC0 RM

The execution circuit

The circuit is parametrised over n - the number of transaction it processes at once. For each transaction, it performs the out-of-circuit RM checks and then verifies the total state transition induced by applying these transactions.

Out-of-circuit checks required by RM

The following out-of-circuit checks are required in addition to in-circuit checks to ensure that the state transition is computed correctly:

  1. currentState is a valid historical state – guaranteed by receiving it from the Anoma Contract [3][4]
  2. CU are disjoint within an Action:
    1. The same resource is not consumed in two different CUs
    2. The same resource is not created in two different CUs [5]
  3. Actions are disjoint within a Transaction:
    1. The same resource is not consumed in two different actions of the transaction
    2. The same resource is not created in two different actions of the transaction [6]
  4. RM proofs are valid:
    1. The aggregated SNARK proof are valid
    2. Delta proof is valid
  5. Nullifier non-existence proof for consumed resources
  6. Commitment non-existence proof for created resources [7]
Global checks in a circuit

Out-of-circuit RM checks include both local and global checks that require access to global structures. By definition, it isn’t possible to put global checks in a circuit, therefore we assume that the global state doesn’t change between the moment of proving against the currentState value and applying the changes associated with the created execution proof.

Inputs

Instance:
  • currentState - a commitment to the current state stored in the Anoma Contract
  • newState - a commitment to the proposed state
Witness:
  • n transactions TX_i
  • n + 1 CM root (init state → tx_1 updated state → tx_2 updated state → … → tx_n updated state) CR_i
  • n + 1 NF root NR_i

Constraints

The execution circuit constraints verify each transaction individually and ensure that they correctly update the current state into the new proposed state.

  1. hash(CR_0, NR_0) = currentState
  2. hash(CR_n, NR_n) = newState

For each transaction:

  1. Action.consumed are disjoint for all actions in TX_i
  2. CU.consumed are disjoint for all CUs for all actions in TX_i
  3. Verify RM proofs:
    1. Aggregator.verify(TX_i)
    2. ECDSA.verify(TX_i.deltaProof, deltaVerifyingKey)[8]
  4. Non-inclusion proof for consumed in TX_i resources and NR_{i - 1}
  5. CR_{i+1} = CR_i + TX_i.created – CR_{i+1} is produced from CR_i by adding commitments of resources created in TX_i
  6. NR_{i+1} = NR_i + TX_i.consumed – NR_{i+1} is produced from NR_i by adding commitments of resources created in TX_i

Questions

  1. Find a more efficient way to verify non-inclusion for nullifiers
  2. Currently the tree update constraint is underspecified. It has to be specified further and the list of inputs might have to be possibly updated

Potentially relevant links

  1. Currently two: compliance and logic proofs are aggregated into one and the delta proof is left as is ↩︎

  2. The hash function used to compute it must have a binding property ↩︎

  3. Strictly speaking, the specification requires the CMtree root to be a valid historical root, but in the context of Resource Plasma, we have two trees and store their hash ↩︎

  4. When verifying the execution proof from the past, the validity of the historical state can be verified by checking the history and making sure that the state used to prove the statement against is indeed valid ↩︎

  5. This statement follows from 2.1 and the fact that we use the nullifier of the old resource as a nonce of the new resource ↩︎

  6. This follows from 3.1 and the fact the same resources have the same nonces ↩︎

  7. Implicitly follows from the fact that all consumed resources are unique (points 2, 3, and 5 ensure that) ↩︎

  8. Delta verifying key is computed from the transaction components ↩︎

3 Likes
2

The cm root existence check is missing from the Out-of-circuit checks required by RM and its constraints. We also need to ensure that each root in the CU instance exists in the historical cm root set. This may require another Merkle tree to provide an existence proof.

The two constraints can be simplified into one: no duplicate nullifiers in TX_i.

Yes, I assume we want to use a 256-depth Merkle tree as discussed. Let’s first benchmark it in a circuit. Exploring other non-inclusion algorithms is worth considering. While I understand the non-inclusion circuit, it may not that trivial for others. Could you briefly explain it or share a link?

1 Like
3

I agree with Xuyang that the disjointedness can be granted by the ZCash-style compliance proof.

However, what we also need is to check that for each resource in an action there is a relevant compliance proof, i.e. that the CUs cover the Action.

Otherwise I can submit a transaction to burn a token without ever checking that it historically existed and it will be counted as valid (as there are no CUs to check).

1 Like
4

Update the Commitment Tree in the Execution Proof Circuit

We usually store commitments using a Merkle tree. In PA/AnomaPay’s case, it’s a variable-depth one. Now, inside the Execution Proof circuit, we need to verify that the state transition when processing transactions, including updating the commitment tree. But obviously, we can’t just load all the leaves into the circuit and recompute the whole root; that’d be way too expensive. So we can adopt one of two approaches commonly use in zk circuits.

Sparse Merkle Trees

A Sparse Merkle Tree represents a 2^k sized tree but stores only non-empty nodes.

Example:
depth = 256
index = commitment(is exactly 256 bits over a hash)

Properties:

  • constant depth
  • easy proofs
  • good for circuits

Update cost: 256 hashes (still kind of costly)

We never need all leaves to update a Merkle root, instead we only need the leaf and siblings. And inside zk circuits, the proof simply recomputes the path twice to prove the transition: old_root → new_root

Incremental Merkle Trees (IMT)

It is designed for efficient append-only updates. Instead of storing the entire tree, it stores just enough intermediate nodes so that each new leaf can be inserted in O(log n) time without recomputing everything.

1. Core idea

An Incremental Merkle Tree keeps only:

  • the root
  • the frontier nodes (rightmost nodes at each level)

These frontier nodes are sometimes called the “filled subtrees”.

2. What the tree stores internally

For a tree of depth d, the IMT stores:

branch[0]
branch[1]
branch[2]
...
branch[d-1]

Each entry represents the latest subtree root at that level.
Example for depth = 4:

branch[0] = last leaf
branch[1] = last pair subtree
branch[2] = last 4-leaf subtree
branch[3] = last 8-leaf subtree

Also store:

count = number_of_leaves

3. Insertion/Append algorithm

Insertion behaves like binary addition.

When inserting leaf L, look at the binary representation of count.

Example:

count binary action
0 000 store leaf
1 001 merge level 0
2 010 store level 0
3 011 merge twice
4 100 store level 0

Step-by-step example

Insert leaves sequentially:

Insert L1

count = 0
branch[0] = L1

Insert L2

Binary carry:

hash(L1, L2)

Update:

branch[1] = H(L1, L2)

Insert L3

branch[0] = L3

Insert L4

Carry again:

H(L3, L4)
H(H(L1,L2), H(L3,L4))

So:

branch[2] = H(H(L1,L2), H(L3,L4))

4. Pseudocode

Typical IMT insertion:

node = new_leaf
index = count

for level in 0..depth-1:

    if index % 2 == 0:
        branch[level] = node
        break
    else:
        node = H(branch[level], node)
        index = index / 2

count += 1

5. Complexity

Operation Cost
Insert O(log n) hashes
Storage O(log n)
Proof size O(log n)

** IMT vs Sparse Merkle Tree**

Feature IMT Sparse Merkle Tree
Use case append-only key-value map
tree depth small usually 256
storage log(n) many default nodes
insertion sequential arbitrary index
5

Indexed Merkle Trees and Non-membership Merkle proofs

We need an efficient way to prove nullifier non-existence and update the nullifier set in the execution proof circuit. While a depth-256 Sparse Merkle Tree can prove non-existence by verifying a default leaf at a given index, I’ll propose Indexed Merkle Trees as a more direct solution.

Idea behind Indexed Merkle Trees

An Indexed Merkle Tree stores leaves in sorted order and links neighbors.

Each leaf stores:

(value, next_value)

Example set:

{10, 20, 35, 50}

Leaves become:

(10 → 20)
(20 → 35)
(35 → 50)
(50 → ∞)

The tree commits to these records.

Proving non-membership

To prove:

25 ∉ set

Show the leaf where it would belong and provide the leaf

(20 → 35)

Then prove:

20 < 25 < 35

Since the set is sorted, 25 cannot exist between them.
The proof consists of:

  1. Existence proof for ( 20 → 35)
  2. Range proof for (20 < 25 < 35)

This proves non-membership.

Update operation

When inserting a new element:
Example inserting 25.

Current leaf:

(20 → 35)

Update into two leaves:

(20 → 25)
(25 → 35)

Only one path update is required to regenerate the new root.

6

Thank you for the writeup! Some questions:

  • how do the costs for IMT and sparse merke trees compare to each other and to the regular approach? Would be handy to have a table with a direct comparison, including the operations out of circuit such as tree appends and in-circuit cost change
  • Do I understand correctly that the sparse tree allows deletion? How would we ensure that it doesn’t happen if we use sparse trees?
  • As far as I understand, the descriptions here work for one transition new → old. How do they change if we process ‘n’ transitions at once? Do they just multiply or are there extra costs?
  • I assume, changing these data structures implies the changes on the protocol adapter as well, so we just change them everywhere. Is that a correct assumption?
7

Commitment Merkle Tree comparison

Feature Incremental Merkle Tree (IMT) Sparse Merkle Tree (SMT) Regular Merkle Tree
Primary use Append-only sets Key–value maps Static / general-purpose
Indexing Sequential (0,1,2,…) Fixed (e.g. hash(key)) Flexible / positional
Tree depth Small (log n) Fixed (e.g. 256) log n
Storage O(log n) (branch only) O(#non-empty nodes) + defaults O(n)
Insert cost O(log n) O(log N) (N = full key space) O(log n)
Update existing leaf Not typical (append-only) O(log N) O(log n)
Append efficiency :star: Excellent :cross_mark: Not optimized :warning: Moderate
Membership proof O(log n) O(log N) O(log n)
ZK friendliness :star: Excellent :star: Good (but deep) :warning: Depends
Circuit cost Low (shallow tree) Higher (deep tree) Medium
Ordering guarantee Implicit (insertion order) None None

Do I understand correctly that the sparse tree allows deletion? How would we ensure that it doesn’t happen if we use sparse trees?

Yes, it enables efficient updates of existing leaves (including setting it a default value as the deletion) in an SMT. In our scenario, only append operations are needed, no updates or deletions, since each commitment and nullifier is unique.

As far as I understand, the descriptions here work for one transition new → old. How do they change if we process ‘n’ transitions at once? Do they just multiply or are there extra costs?

Currently, at worst, it’s O(n). I’m considering batch updates/insertions for Merkle trees to improve performance

I assume, changing these data structures implies the changes on the protocol adapter as well, so we just change them everywhere. Is that a correct assumption?

Yes, some checks are moved into the circuit and trees are maintained off-chain. And it will simplify the current PA in both data and logic. The controller/backend and indexer will do more work