# Study of proof recursion/aggregation techniques among VMs of the market ## Binius M3 arithmetization In their [documentation](https://main.d2jgg24nzml7oa.amplifyapp.com/basics/arithmetization/), Binius team describes in great details how they thought and handle the arithmetization problem. ### Basic Arithmetization Technique SNARK arithmetization organizes the program's execution into a **computational trace table**, which records how data (stored in registers) changes over time: - **Rows**: Represent each clock cycle of the program. - **Columns**: Represent the registers. At each clock cycle, the program updates the registers based on the instructions it follows. #### Validating the Trace To ensure the computational trace is valid, we need to verify that the register updates between rows are correct: 1. Compare each row to the one before it. 2. Check that the register values follow the rules of the instruction executed during that cycle. 3. Use **polynomial constraints** to mathematically encode these rules for each instruction. #### Using Selectors for Constraints Since each cycle may involve different instructions, a **selector** column is used to "activate" the correct constraint for the current instruction: - A **selector** is a special column that acts as a switch. - It assigns a value (e.g., 1 or 0) to indicate which constraint should be applied. This allows multiple constraints to coexist efficiently while ensuring only the relevant one is enforced for each row. --- ### Advanced Techniques #### Subtables Explained Polygon introduces subtables as a method to validate specific operations within a main computational trace. Let us explain this concept with an example assuming that the cryptographic backend only allows defining constraints with additions and multiplications. An exponentiation operation (EXP) can be broken down and validated using subtables. #### Main Execution Trace The **main execution trace** records all operations, including EXP. Each EXP operation is represented by a single row. For instance: - Inputs 2 and 5 yield 32 in the main table. - The **EXP column** flags when an EXP operation occurs (value = 1), signaling that the result in column C must be validated. | A | B | C | EXP | | --- | --- | --- | --- | | ... | ... | ... | 0 | | **2** | **5** | **32** | **1** | | ... | ... | ... | 0 | | **3** | **2** | **9** | **1** | | ... | ... | ... | 0 | The complex exponentiation calculation is then deferred into the subtable which obtains each required result in many steps, as opposed to in just one. #### Secondary Execution Trace The **secondary execution trace** validates the EXP operation step-by-step, using multiple rows to compute the result iteratively: - **A**: Base remains constant, $a_{i+1} = a_i$. - **B**: Exponent remains constant, $b_{i+1} = b_i$. - **C**: Intermediate result is updated: $c_{i+1} = c_i \cdot a_i$. - **D**: Counter decreases with each step, starting from the exponent until it reaches 1. - **EXP**: Flags when the operation finishes (value = 1). | A | B | C | D | EXP | | --- | --- | --- | --- | --- | | 2 | 5 | 2 | 5 | 0 | | 2 | 5 | 4 | 4 | 0 | | 2 | 5 | 8 | 3 | 0 | | 2 | 5 | 16 | 2 | 0 | | **2** | **5** | **32** | **1** | **1** | | 3 | 2 | 3 | 2 | 0 | | **3** | **2** | **9** | **1** | **1** | #### Validation with Lookup Argument - When the **EXP column** in the main trace is 1, a lookup is performed in the secondary trace. - Only rows in the secondary trace with **EXP = 1** are checked. - If a row in the secondary trace matches the values in columns A, B, and C of the main trace, the EXP operation is validated. - This ensures consistency between the main and secondary traces and proves the correctness of the operation. By linking rows with matching values, the EXP operation in the main trace is confirmed. --- #### Bus argument Explained Bus argument technique is present is both SP1 and Valida technical specifications. SP1’s zkVM employs a virtual bus system to enable communication between different components (referred to as "chips") in its architecture. This design ensures that complex computations can be split among specialized chips while maintaining consistency and validity across operations. Key components are: 1. CPU (Main Chip): - Responsible for processing RISC-V instructions. - Acts as the "central hub," delegating specific tasks (e.g., arithmetic or memory operations) to specialized chips. - The CPU table has no constraints for the proper execution of the RISC-V instruction, nor does the table itself check that the values in the a, b, and c columns come from the memory addresses specified in the instruction; these are handled by lookups to the other tables and the memory argument, respectively. 2. Specialized Chips handle tasks like: - Arithmetic and logic operations (ALU). - Memory management. - Range-checking. - Precompiled operations for cryptographic functions (e.g., Keccak, SHA-2). The bus acts as a shared communication channel between the CPU and other chips. Every computational event involves: - Sending: the CPU sends an event (e.g., an ADD operation) to the bus. - Receiving: a specialized chip (e.g., ALU) "receives" the event from the bus. ##### Example: Integer Addition 1. **Event Sent**: - The CPU encounters an ADD instruction (e.g., `2 + 3`). - It sends an **ADD event** to the bus, specifying the operands and expected result. 2. **Event Received**: - The ALU chip receives the ADD event from the bus. - The ALU verifies the operation (checks that `2 + 3 = 5`). - If valid, the ALU effectively confirms the correctness of the operation. Tasks are delegated to specialized chips, improving efficiency and clarity. The bus ensures that all operations are correctly verified by the responsible chips. Complex proofs can be distributed across multiple chips without overwhelming the CPU. --- ### Drawbacks of These Techniques and propositions The Binius team identified key drawbacks of these advanced techniques: - **Single Table Approach**: - Using a single table leads to a **complex master constraint polynomial** with many variables and a high degree, as it must account for all possible instructions the VM can execute. - This approach is inefficient since every cycle incurs the cost of all instructions, even though only one is used per cycle. - **Subtables or Subchips**: - Introducing subtables reduces complexity but adds overhead. The main trace table must use **selectors** to indicate which rows to validate against subtables or send to chips. - When multiple subtables exist, selectors must differentiate between them. - All of this increases the cost of lookups because the columns being validated are "selected" rather than plain. By going further, the team proposed some characteristics that an ideal arithmetization scheme should have: - **Separation of Concerns**: Break functionality into separate tables, each with its own polynomial constraints. - **Eliminate Overhead**: Remove multiplexing and selectors to reduce constraint polynomial degrees and simplify lookups. - **Flexibility**: Avoid tying the scheme to a specific CPU/VM architecture; instead, use a meta-template to efficiently arithmetize diverse problems. --- ### A New Arithmetization Paradigm: Multi-Multiset Matching (M3) #### Key Features - **No Main Trace**: The framework does not rely on a centralized execution trace. - **No Temporality**: M3 instances are purely declarative, allowing tables to be freely permuted without any concept of time or sequence. - **Flexible Table Lengths**: Provers can populate prearranged tables with as many rows as needed, without restrictions on size. #### M3 Framework Overview In the M3 paradigm: - The **verifier** sets up a channel, modeled as an abstract bidirectional data stream. - The **prover** must populate tables with rows that satisfy specific constraints to balance the channel. - The process is **incremental and unsupervised**, allowing the prover to: - Make progress toward the goal step by step. - Choose their path and the order of operations freely, as the framework is nondeterministic. This flexibility makes the M3 paradigm highly adaptable, empowering the prover to determine their approach while maintaining soundness through the constraints. #### Channels A channel provides two methods, **push** and **pull**, both accepting a tuple with a fixed number of components, each having predefined bit-widths. The tuple’s structure (arity and type signature) is a permanent property of the channel. For example, a channel with the type signature $(\mathcal{T}_4, \mathcal{T}_5)$ allows both methods to handle tuples like (0xd9de, 0x86cd91f4), where the first element is a \(\mathcal{T}_4\)-element, and the second is a \(\mathcal{T}_5\)-element. **Push and Pull** serve distinct purposes: - **Pushing** registers a tuple as a new, unresolved **liability**. - **Pulling** declares a tuple as **resolved**, balancing a previously registered liability. - Together, they maintain a channel as a **ledger**, with pushes recorded as liabilities and pulls as assets. A channel is considered **balanced** when the sets of pushed and pulled elements are identical, ignoring order but accounting for multiplicity. **Example:** The following table represents a balanced channel: | **Pushes** | **Pulls** | |------------------------|----------------------| | (0xd9de, 0x86cd91f4) | (0xd9de, 0x86cd91f4) | | (0xd9de, 0x86cd91f4) | (0xbd8f, 0x00000000) | | (0xd9de, 0x0000d9de) | (0xd9de, 0x86cd91f4) | | (0xbd8f, 0x00000000) | (0xd9de, 0x0000d9de) | Any mismatch in the table—for example, altering a character or adding an extra push or pull—would result in the channel becoming **unbalanced**. #### Tables and constraints - Tables in M3 are ordered lists of rows with fixed column types and widths, defined by a table's signature. - Each table is associated with polynomial constraints that must vanish for every row, ensuring validity. - For example, a table with three columns—John, Mary, and Fred—might enforce the constraint $\text{John} \cdot \text{Mary} = \text{Fred}$. While the prover can freely populate the tables, every row must adhere to these constraints, ensuring correctness without direct access to channels. #### Flushing rules - **Flushing rules** define how tables interact with channels by specifying which columns (explicit or derived) are bundled into tuples and pushed or pulled into a channel. - Each rule ensures that the column tuple matches the channel's type (width and component types). - For example, a rule might push $(\text{John}, \text{Fred})$ to a channel expecting tuples of type $(\mathcal{T}_4, \mathcal{T}_5)$, or pull a derived tuple like $(g \cdot \text{Mary} + \text{John}, \text{Fred})$, where $g \in \mathcal{T}_4$. Type mismatches, such as pushing $(\text{John}, \text{Mary}, \text{Fred})$ to a 2-component channel, are invalid. - Flushing rules can involve **statement columns**, representing the prover's claim, or **witness columns**, which are auxiliary and ensure channels balance. #### Boundary conditions - **Boundary conditions** allow channels to be initialized with statement-dependent data before tables are populated and flushing rules are applied. - For instance, in the an example where the prover has to show that he knows the prime factorization of some integer 3135, the verifier preloaded the channel by pushing 3135 (the statement) and pulling 1 (the terminal value). #### Instances and Attempts - An **M3 instance** defines the specification for channels, tables, flushing rules, and boundary conditions. It includes the number and type signatures of channels and tables, the constraints on table data (e.g., polynomials), and how data flows between tables and channels via flushing rules. Additionally, instances describe how channels are pre-seeded with statement-dependent data. - An **attempt** refers to a specific statement value and the actual population of the instance's tables with values that satisfy the constraints. Satisfaction in M3 instances means that an attempt fulfills the instance's requirements by balancing all channels. 1. Starting with empty channels, statement-dependent data may prepopulate them. 2. Tables are then flushed into channels according to the instance's rules, using specified column values to push or pull data. 3. If all channels are balanced—meaning their pushed and pulled values match—the attempt satisfies the instance, verifying correctness without exposing intermediate steps. --- ## SP1 Recursion Proving System The SP1 RISC-V zkVM supports recursive proof aggregation, enabling users to verify one SP1 proof within another. This capability is critical for constructing layered, scalable proofs while minimizing computational overhead. Below, I detail each component of this system, offering insights into its structure and function. --- ### Core Components of the SP1 Proving System The [`SP1Prover`](https://github.com/succinctlabs/sp1/blob/main/crates/prover/src/lib.rs#L122-L159) is the primary orchestrator for the proving process. It encapsulates multiple stages of proof generation, each serving a distinct role: 1. **Core Prover**: - Generates base proofs for SP1 program executions. - These proofs serve as the foundation for all higher-level recursive operations. 2. **Compression Prover**: - Aggregates multiple shard proofs into a single proof using recursive techniques. - Reduces computational complexity and proof size by combining intermediate results. 3. **Shrink Prover**: - Condenses the compressed proofs into a smaller form for further optimization. - This step leverages the properties of SNARK-friendly fields to maintain integrity while reducing data size. 4. **Wrap Prover**: - Converts the shrunken proofs into SNARK-friendly field elements, enabling efficient verification. - Supports integration with external proof systems like Plonk or Groth16. These provers are integrated into the `SP1Prover` structure, which coordinates their operations to produce an end-to-end proof. --- ### Prover Configuration Options #### **SP1ProverOpts** [`SP1ProverOpts`](https://github.com/succinctlabs/sp1/blob/main/crates/stark/src/opts.rs#L14-L21) defines global options for the SP1Prover, affecting both core and recursive proving operations. Key configurations include: - **Core Shard Size**: Determines the number of cycles per shard. - **Trace Generation Workers**: Specifies the number of worker threads for generating execution traces. - **Deferred Events**: Manages how deferred events are split and handled across recursion layers. #### **SP1CoreOpts** [`SP1CoreOpts`](https://github.com/succinctlabs/sp1/blob/main/crates/stark/src/opts.rs#L97-L112) configures options specific to the core proving stage. Key settings include: - Capacities for checkpoints and records, optimizing resource usage during proof generation. - Parameters for shard sizes and batch configurations. --- ### Recursive Proofs: Compression and Execution The [`compress`](https://github.com/succinctlabs/sp1/blob/main/crates/prover/src/lib.rs#L386) function lies at the heart of SP1's recursion capabilities. Its purpose is to take multiple shard proofs and reduce them into a single shard proof using recursive proving techniques. This is achieved in several steps: #### 1. **Setup and Configuration**: - Initializes workers based on [`SP1ProverOpts`](https://github.com/succinctlabs/sp1/blob/main/crates/stark/src/opts.rs#L14-L21) to handle recursive tasks in parallel. - Prepares the proving keys and recursion programs required for compression. #### 2. **Runtime Initialization**: - The recursive execution is managed by a [`Runtime`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L70-L122) object, built from a [`RecursionProgram`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/program.rs#L13-L16). - This `Runtime` encapsulates the program's instructions, memory, and execution record. #### 3. **Instruction Execution**: - Instructions for the recursion are executed in the [`run`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L613-L631) method. This method iterates over the program instructions, delegating their execution to the [`execute_raw`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L561-L611) method. - Each instruction is processed in [`execute_one`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L203-L559), which updates the [`ExecutionRecord`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/record.rs#L12-L31) and the [`ExecEnv`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L692-L696). Key components involved in this process include: - [`RecursionProgram`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/program.rs#L13-L16): Defines the instructions and logic for the recursive proof system. - [`ExecEnv`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/mod.rs#L692-L696): Represents the execution environment, including memory. - [`ExecutionRecord`](https://github.com/succinctlabs/sp1/blob/main/crates/recursion/core/src/runtime/record.rs#L12-L31): Tracks the progress and results of the recursive proof computation. --- ### Instruction Processing in Detail #### **Instruction Types**: Instructions in the recursion program fall into several categories, including: 1. **Base Field Operations**: `BaseAluInstr` supports addition, subtraction, multiplication, and division in the base field. 2. **Extension Field Operations**: `ExtAluInstr` performs similar operations in the extension field. 3. **Poseidon Hashing**: `Poseidon2Instr` handles cryptographic hashing using the Poseidon2 permutation. 4. **Memory Operations**: `MemInstr` provides read/write functionality for virtual memory. 5. **Control Flow**: Instructions like `SelectInstr` manage branching and conditional execution. #### **Execution Workflow**: - **Sequential Blocks**: Executed linearly, processing one instruction at a time. - **Parallel Blocks**: Distributed across threads for simultaneous execution, reducing runtime for independent operations. #### **Error Handling**: - Division errors (e.g., division by zero) are carefully handled with domain-specific rules. - Witness streams ensure deterministic execution, even in parallel contexts. --- ### End-to-End Proof Generation The entire proof generation process involves: 1. **Core Proof Generation**: - Produces proofs for individual program shards. - Includes verification steps to ensure validity before proceeding. 2. **Proof Compression**: - Aggregates core proofs into a recursive proof. - Leverages multithreading for efficient execution of compression tasks. 3. **Proof Shrinking**: - Minimizes the size of the compressed proof while preserving its validity. 4. **Proof Wrapping**: - Converts the proof into a SNARK-friendly form, enabling efficient verification in other contexts. --- ### Performance and Parallelism SP1 leverages parallelism extensively to optimize performance: - **Trace Generation**: Multiple workers generate execution traces concurrently. - **Parallel Instruction Execution**: Instructions within independent blocks are distributed across threads. - **Efficient Memory Access**: Uses a high-performance memory model with caching to reduce overhead. Additionally, SP1 monitors runtime performance, providing detailed statistics on the number of cryptographic operations, memory accesses, and control flow events. These insights enable users to identify bottlenecks and optimize their configurations. --- ### Applications and Use Cases - **Proof Aggregation**: Combines multiple SP1 proofs into a single proof for batch verification. - **Recursive Verification**: Embeds proofs within proofs, supporting scalable and composable proof systems. - **Integration with External Systems**: Converts SP1 proofs into formats compatible with SNARK verifiers like Plonk and Groth16. --- ## Polygon zkEVM recursion process Polygon talks about the way they handle proof recursion and proof aggregation in their [documentation](https://docs.polygon.technology/zkEVM/architecture/zkprover/stark-recursion/composition-recursion-aggregation/). ### Proof composition The proof composition in the Polygon framework can then be described as: ![image](https://hackmd.io/_uploads/SJklbrCv1x.png) To simplify verification, instead of directly validating the STARK proof (which can be computationally expensive), the process is delegated to a verification circuit. This circuit validates the STARK proof, and the Prover generates a second proof attesting to the correctness of this verification. The Verifier then checks only the proof of the verification circuit, bypassing the need to verify the original computation directly. ### Proof recursion The proof recursion can be described with recursion steps that can be applied as many times as desired: ![image](https://hackmd.io/_uploads/Hkl9MHRwyl.png) We alternate a set of two sub-processes: - converting a STARK proof to a Verifier circuit (S2C), - converting a Verifier circuit to a STARK proof (C2S). Each step will compress the proof, making it more efficient to be verified but at the expense of increased Prover complexity. In summary, the process works as follows: the first proof is generated by providing the initial STARK Prover with the appropriate inputs and public values. The resulting proof is then used as an input for the next STARK Prover, along with its respective public inputs. This recursive process is repeated for subsequent STARK Provers, chaining the proofs together. ![image](https://hackmd.io/_uploads/SkruOSRvJe.png) #### S2C: converting a given STARK into its verifier circuit This is a generic conversion with `pil`, `constants` and `starkinfo` as input parameters. CIRCOM is used as an intermediate representation language for the description of circuits. ![image](https://hackmd.io/_uploads/Bk6fLSRwye.png) #### C2S: converting a circuit Verifier into a STARK proof The circuit definition in the form of R1CS is taken and automatically translated into a new STARK definition. In this pre-processing phase, new `pil`, `constants` and `starkinfo` are generated for setting up a new STARK proof. ![image](https://hackmd.io/_uploads/rkxmvrCvJl.png) #### Intermediate proof steps Each intermediate STARK proof is generated using the witness values provided by the execution of the associated circuit witness calculator program, which in turn takes as inputs the `publics` and the values of the previous proof. ![image](https://hackmd.io/_uploads/B1poYB0wyg.png) ### Proof aggregation In addition to supporting Composition and Recursion, the Polygon zkProver architecture also enables Aggregation during proof generation. Aggregation is a specialized form of proof composition where multiple valid proofs are combined into a single proof, known as the Aggregated Proof. Verifying this Aggregated Proof is equivalent to individually verifying all the proofs that were combined, providing a more efficient validation process. ![image](https://hackmd.io/_uploads/BJtfqS0vyl.png) --- ## Cairo proof recursion In the whitepaper of [Cairo](https://eprint.iacr.org/2021/1063.pdf), especially in section 2.2, they mention how their Von Neumann architecture can be seen as an advantage for recursive proving. Cairo uses a CPU approach, which simulates a von Neumann architecture: - The program bytecode and data are stored in memory. - A program counter (PC) points to the current instruction in memory. - The CPU fetches the instruction, executes it, updates memory or registers, and moves to the next instruction. The CPU approach has significant advantages for recursive proofs: 1. **Fixed Constraint Set:** The CPU is described by a fixed set of constraints (30–40 constraints in Cairo). This simplicity is key for recursive proofs, as the verifier doesn't need to be modified for each program. 2. **Bootloading Programs by Hash:** Cairo allows a program to be represented by its hash. This eliminates the need to include the full bytecode in the proof, reducing size and improving privacy. By representing both the verifier and the program under verification using the same CPU constraints, recursive proofs become straightforward because there is no dependency between the program being verified and the verifier itself. ### How Recursive Proofs Work in Cairo The process of creating recursive proofs in Cairo involves several key steps: 1. **Encoding the Verifier as a Cairo Program** The verifier's algorithm (the process of verifying a proof) is expressed as a Cairo program. Since Cairo's CPU constraints are general-purpose, the verifier can be treated like any other program. 2. **Bootloading the Verifier** Using Cairo's bootloading mechanism (Section 2.2.1), the verifier can: - Load its own code from memory (as a hash). - Start verifying another proof. This is crucial because it allows the verifier program to be compactly represented as a hash and passed into the next level of recursion without requiring the full program or proof. 3. **Breaking the Circular Dependency** Many proof systems face a challenge: the verifier depends on the program, which in turn depends on the verifier. Cairo's CPU approach breaks this dependency because: - The verifier does not depend on the program under verification. - The constraints for the CPU are independent of the computation. This decoupling simplifies recursive proofs, as the same verifier can handle any computation without modification. ### Before and after recursive proving The importance of recursive proving for StarkNet is well-articulated in this [article](https://medium.com/starkware/recursive-starks-78f8dd401025). Below is a concise explanation of how recursive proving transformed the process. #### Before recursive proving Before recursive proving, SHARP followed a non-recursive flow for generating proofs: ![image](https://hackmd.io/_uploads/SypaNrlOkl.png) In this framework: - Transactions were “rolled up” into a single proof that was submitted to Ethereum. - Incoming statements (or transactions) were collected over time, and when a threshold (based on capacity or time) was reached, a combined statement — referred to as a "Train" — was generated. - The Train was only proven after all individual statements had been collected. This approach faced significant challenges: - **Proving time:** The proof generation process required summing up the time to prove each individual statement, leading to long delays. - **Resource limits:** Generating proofs for extremely large statements was constrained by available computational resources, such as memory. These limitations imposed a scalability barrier on STARK proving at the time, leading to the idea of recursive proving. #### With recursive proving Recursive proving fundamentally changes this process by leveraging Cairo’s ability to express general computational statements that can verify other STARK proofs. With recursion: - Instead of waiting for all statements to arrive, SHARP generates individual proofs as soon as statements are received. - These proofs are merged recursively into higher-level proofs, eventually producing a single proof that encompasses all statements. The updated flow now looks like this: ![image](https://hackmd.io/_uploads/S1toHSedkl.png) Here’s how it works: 1. **Parallel proof generation:** Statements are proven independently and in parallel, producing individual proofs. 2. **Recursive verification:** A Recursive Verifier statement — a Cairo program designed to verify STARK proofs — validates each pair of proofs. These validations themselves produce new proofs. 3. **Iterative merging:** The process of merging proofs continues recursively until all proofs are aggregated into one final proof. 4. **On-Chain submission:** The final aggregated proof is submitted on-chain to a Solidity verifier smart contract for validation. --- ## RISC0 recursive proving The RISC Zero zkVM leverages [recursive proving](https://dev.risczero.com/api/recursion) to enable efficient verification of unbounded computations, proof aggregation, and proof composition. ### Recursive Proving Process ![image](https://hackmd.io/_uploads/By-TV4xdye.png) The recursive proving mechanism can be understood as a pipeline involving the following steps: 1. **Execution and segmentation** - A program (referred to as a "guest program") is executed in the zkVM. - The execution trace is divided into smaller **segments**. Each segment represents a chunk of the computation. The `CompositeReceipt` is a receipt composed of one or more `SegmentReceipt` structures proving a single execution with continuations. - This segmentation helps manage memory usage and makes proof generation feasible for large computations. 2. **Proving each Segment** - Each segment is independently proven by the zkVM, resulting in a `SegmentReceipt`. This is essentially a proof of correct execution for that specific segment. 3. **Lifting `SegmentReceipts`** - Each `SegmentReceipt` is passed through a program called `lift`, which verifies the STARK proof of the segment using the **Recursion Circuit**. This produces a `SuccinctReceipt`. - The `SuccinctReceipt` is smaller and represents a compressed proof for the segment. 4. **Joining `SuccinctReceipts`** - The `join` program aggregates two SuccinctReceipts into a single SuccinctReceipt. - This process is repeated iteratively, combining proofs from all segments until only one SuccinctReceipt remains. This aggregated proof represents the entire computation session. 5. **Preparing for Groth16** - The final `SuccinctReceipt` is passed through the `identity_p254` program, which uses the Poseidon254 hash function to prepare the proof for SNARK-style compression. 6. **STARK-to-SNARK Compression** - The `compress` program wraps the final SuccinctReceipt into a `Groth16Receipt` using the **STARK-to-SNARK Circuit**. - This `Groth16Receipt` is compact and optimized for on-chain verification due to the small size of Groth16 proof when compared to STARK proofs. ### Recursive Circuit Architecture ![image](https://hackmd.io/_uploads/HJPtUEluyx.png) The RISC Zero zkVM employs three key circuits to implement recursive proving: 1. **RISC-V circuit** - This is the core circuit that proves the correct execution of RISC-V programs. - It generates the initial STARK proofs (`SegmentReceipts`) for program execution. 2. **Recursion circuit** - A dedicated STARK circuit optimized for verifying and aggregating STARK proofs. - Supports cryptographic operations like hashing and polynomial evaluations, making it efficient for recursion. - Programs for the Recursion Circuit include: - **`lift`**: Verifies a single STARK proof and outputs a `SuccinctReceipt`. - **`join`**: Aggregates two STARK proofs into one `SuccinctReceipt`. - **`identity_p254`**: Prepares a proof for Groth16 compression. - **`resolve`**: Removes assumptions from a receipt claim during proof composition. 3. **STARK-to-SNARK circuit** - An R1CS circuit that compresses STARK proofs into a `Groth16Receipt`. - This enables small proof sizes suitable for blockchain applications. ### Recursive Proving Programs The programs executed within the Recursion Circuit are critical for the recursive proving process: - [`lift`](https://github.com/risc0/risc0/blob/ba4f13458ef0e69b0709eb1d8e7dc3cb8b129ec2/risc0/zkvm/src/host/recursion/prove/mod.rs#L72) - Verifies a STARK proof from the RISC-V Prover. - Outputs a `SuccinctReceipt` with constant-time verification, regardless of the original segment length. - [`join`](https://github.com/risc0/risc0/blob/ba4f13458ef0e69b0709eb1d8e7dc3cb8b129ec2/risc0/zkvm/src/host/recursion/prove/mod.rs#L100) - Combines two `SuccinctReceipts` into one. - Used iteratively to aggregate multiple receipts into a single proof for an entire session. - [`identity_p254`](https://github.com/risc0/risc0/blob/ba4f13458ef0e69b0709eb1d8e7dc3cb8b129ec2/risc0/zkvm/src/host/recursion/prove/mod.rs#L214) - Verifies a STARK proof using the Poseidon254 hash function. - Prepares the proof for Groth16 compression, enabling on-chain verification. - [`resolve`](https://github.com/risc0/risc0/blob/ba4f13458ef0e69b0709eb1d8e7dc3cb8b129ec2/risc0/zkvm/src/host/recursion/prove/mod.rs#L143) - Removes assumptions from a receipt claim. - Allows for flexible proof composition by verifying conditional proofs.