Exploring the execution proof

Resource Machine Stuff 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