# Exploring the execution proof **URL:** \ **Category:** Execution proof\ **Created:** [July 15, 2025, 10:36am UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788 "2025-07-15T10:36:22Z")\ **Posts on this page:** 7\ **Page:** 1
**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\ **Post date:** [July 15, 2025, 10:36am UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/1 "2025-07-15T10:36:22Z")
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](https://forum.anoma.net/t/state-change-verification-a-probably-wrong-sketch/1652). #### 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 - [Reckle Trees: Updatable Merkle Batch Proofs with Applications](https://eprint.iacr.org/2024/493?utm_source=chatgpt.com) - [Vector Commitments Study](https://eprint.iacr.org/2011/495.pdf) - [Zero-Knowledge Sets](https://people.csail.mit.edu/silvio/Selected%20Scientific%20Papers/Zero%20Knowledge/Zero-Knowledge_Sets.pdf) - [MPT](https://ethereum.org/en/developers/docs/data-structures-and-encoding/patricia-merkle-trie/) - [Taiko rollup](https://github.com/taikoxyz/raiko/tree/main/lib/src) - [Scroll rollup](https://github.com/scroll-tech/scroll/tree/develop/crates) - [Starknet SNOS](https://docs.starknet.io/architecture/os/) - [ZKSync](https://github.com/matter-labs/zksync) * * * 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 ---
**Author:** ![xuyang](https://avatars.discourse-cdn.com/v4/letter/x/c68b51/32.png) [@xuyang](https://forum.anoma.net/u/xuyang)\ **Post date:** [July 16, 2025, 5:35pm UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/2 "2025-07-16T17:35:22Z")
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. > [@vveiln](#): > > - Action.consumed are disjoint for all actions in TX\_i > - CU.consumed are disjoint for all CUs for all actions in TX\_i The two constraints can be simplified into one: no duplicate nullifiers in TX\_i. > [@vveiln](#): > > Find a more efficient way to verify non-inclusion for nullifiers 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? ---
**Author:** ![ArtemG](https://avatars.discourse-cdn.com/v4/letter/a/45deac/32.png) [@ArtemG](https://forum.anoma.net/u/ArtemG)\ **Post date:** [July 21, 2025, 5:12pm UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/3 "2025-07-21T17:12:04Z")
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). ---
**Author:** ![xuyang](https://avatars.discourse-cdn.com/v4/letter/x/c68b51/32.png) [@xuyang](https://forum.anoma.net/u/xuyang)\ **Post date:** [March 17, 2026, 11:37am UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/4 "2026-03-17T11:37:44Z")
# 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: ```auto branch[0] branch[1] branch[2] ... branch[d-1] ``` Each entry represents the latest subtree root at that level. Example for depth = 4: ```auto branch[0] = last leaf branch[1] = last pair subtree branch[2] = last 4-leaf subtree branch[3] = last 8-leaf subtree ``` Also store: ```auto 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** ```auto count = 0 branch[0] = L1 ``` #### **Insert L2** Binary carry: ```auto hash(L1, L2) ``` Update: ```auto branch[1] = H(L1, L2) ``` #### **Insert L3** ```auto branch[0] = L3 ``` #### **Insert L4** Carry again: ```auto H(L3, L4) H(H(L1,L2), H(L3,L4)) ``` So: ```auto branch[2] = H(H(L1,L2), H(L3,L4)) ``` ### **4. Pseudocode** Typical IMT insertion: ```auto 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 | ---
**Author:** ![xuyang](https://avatars.discourse-cdn.com/v4/letter/x/c68b51/32.png) [@xuyang](https://forum.anoma.net/u/xuyang)\ **Post date:** [March 17, 2026, 1:57pm UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/5 "2026-03-17T13:57:43Z")
# **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: ```auto (value, next_value) ``` Example set: ```auto {10, 20, 35, 50} ``` Leaves become: ```auto (10 → 20) (20 → 35) (35 → 50) (50 → ∞) ``` The tree commits to these records. ## **Proving non-membership** To prove: ```auto 25 ∉ set ``` Show the leaf where it would belong and provide the leaf ```auto (20 → 35) ``` Then prove: ```auto 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: ```auto (20 → 35) ``` Update into two leaves: ```auto (20 → 25) (25 → 35) ``` Only one path update is required to regenerate the new root. ---
**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\ **Post date:** [March 27, 2026, 1:59pm UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/6 "2026-03-27T13:59:41Z")
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? ---
**Author:** ![xuyang](https://avatars.discourse-cdn.com/v4/letter/x/c68b51/32.png) [@xuyang](https://forum.anoma.net/u/xuyang)\ **Post date:** [March 30, 2026, 1:55pm UTC](https://forum.anoma.net/t/exploring-the-execution-proof/1788/7 "2026-03-30T13:55:59Z")
# 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 | ⭐ Excellent | ❌ Not optimized | ⚠ Moderate | | Membership proof | O(log n) | O(log N) | O(log n) | | ZK friendliness | ⭐ Excellent | ⭐ Good (but deep) | ⚠ 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