doc.md

Starknet Proof Aggregation via Applicative Recursion

Introduction

Starknet processes transactions in sequential blocks. To efficiently prove the integrity of the entire chain on L1 (e.g., Ethereum), Starknet aggregates the STARK proofs of individual block executions into a single, cumulative STARK proof. This is achieved using a technique called "applicative recursion," where proofs verify computations that themselves include proof verifications.

This document details the end-to-end flow, clarifies how the outputs of verified programs are linked, and provides specific references to the relevant Cairo source code files.

Core Goal: Combine N individual block proofs (P_1, ..., P_N) into a single proof (P_final) that attests to the valid execution and sequential linking of all N blocks.

Key Components and Code References

1. Starknet OS Execution: (Implicit) Executes transactions for a single block i, producing, once proven:

   • A STARK proof P_i.
   • The public output data OsOutput_i (inside the proof).

2. OS Output (OsOutput): Defines the public output structure of a Starknet block execution. Crucial for linking blocks.

   • Definition: struct OsOutput, struct OsOutputHeader in src/starkware/starknet/core/os/output.cairo
   • Key Fields: initial_root, final_root, prev_block_number, new_block_number, prev_block_hash, new_block_hash.

3. Cairo Verifier Program: A Cairo program that verifies a STARK proof (P_i) generated by another Cairo program (like the Starknet OS).

   • Source: src/starkware/cairo/cairo_verifier/layouts/all_cairo/cairo_verifier.cairo
   • Functionality:
     • Takes a StarkProof as input (main function hint).
     • Calls verify_proof for core STARK verification.
     • Processes public input in _verify_public_input.
     • Calculates program_hash from the program segment data.
     • Calculates output_hash (Poseidon hash of the output segment data).
     • Outputs CairoVerifierOutput { program_hash, output_hash }.

4. Aggregator Program: A Cairo program designed to combine the OsOutput data from multiple blocks (N) and check their sequential consistency.

   • Main Logic: src/starkware/starknet/core/aggregator/main.cairo
   • Combining & Linking Logic: combine_blocks_inner function in src/starkware/starknet/core/aggregator/combine_blocks.cairo
   • Functionality:
     • Receives claimed OsOutput data for N tasks via hints (main.cairo).
     • Calls combine_blocks which uses combine_blocks_inner to assert sequential consistency (state roots, block hashes/numbers).
     • Outputs a serialization of its claimed inputs (output_blocks in main.cairo).
     • Outputs the final combined OsOutput (serialize_os_output in main.cairo).

5. Simple Bootloader: A Cairo program responsible for executing individual "tasks" (which can be running a regular Cairo program or running the Cairo Verifier program).

   • Runner: src/starkware/cairo/bootloaders/simple_bootloader/run_simple_bootloader.cairo
   • Task Execution: execute_task function in src/starkware/cairo/bootloaders/simple_bootloader/execute_task.cairo
   • Functionality:
     • Takes a list of tasks as input.
     • For each task, it loads the specified program (load_program hint in execute_task).
     • Computes the program_hash of the task's program (compute_program_hash in execute_task).
     • Executes the task's main function (call abs program_entry_point in execute_task).
     • Validates builtin usage (validate_builtins in execute_task).
     • Outputs the task's result prefixed with TaskOutputHeader { size, program_hash }.

6. Bootloader (run_bootloader): Orchestrates running multiple tasks using the Simple Bootloader, potentially handling nested/composite tasks (like verifications).

   • Source: src/starkware/cairo/bootloaders/bootloader/run_bootloader.cairo
   • Functionality:
     • Calls run_simple_bootloader to execute direct subtasks.
     • Parses the output of the simple bootloader (parse_tasks).
     • Handles PlainPackedOutput (direct program output) and CompositePackedOutput (output of a verifier task). See unpack_plain_packed_task and unpack_composite_packed_task.
     • Collects and formats the outputs of the verified tasks into a single contiguous memory segment.

7. Applicative Bootloader: The top-level program for a single aggregation step. It orchestrates the verification of sub-proofs and the execution of the Aggregator program.

   • Source: src/starkware/cairo/bootloaders/applicative_bootloader/applicative_bootloader.cairo
   • Functionality:
     • Runs the Aggregator program as a task using run_simple_bootloader.
     • Runs the recursive verification of the N individual block proofs using run_bootloader.
     • Performs the crucial memcpy check to ensure the Aggregator's claimed inputs match the verified outputs from run_bootloader.
     • Generates the final aggregated output.

The output_hash Verification (Question 2 Clarified)

This was a key point of confusion. Here's the precise relationship and verification mechanism:

1. OS Run (Block i): Produces proof P_i and data OsOutput_i. The data OsOutput_i exists in the output segment of the execution trace corresponding to P_i.

2. Cairo Verifier Run: When the Cairo Verifier program (from cairo_verifier.cairo) is executed as a task by the Simple Bootloader with proof P_i as input:

   • It verifies P_i.
   • It extracts the output segment data (which is the OsOutput_i data) from P_i's public input (extract_range in _verify_public_input).
   • It computes the Poseidon hash of this extracted data, resulting in output_hash_i (poseidon_hash_many in _verify_public_input).
   • The output of this Verifier task execution is CairoVerifierOutput { program_hash_verifier, output_hash_i }.

3. Bootloader's Role (run_bootloader):

   • The run_bootloader function receives the list of original tasks (e.g., N OS runs) and the structure (packed_outputs) indicating how proofs should be verified and potentially nested.
   • When processing a step that involves verifying proof P_i, it invokes the Simple Bootloader to run the Cairo Verifier task.
   • The run_bootloader then processes the output of this Verifier task. Inside functions like unpack_composite_packed_task, it implicitly uses the output_hash_i produced by the verifier.
   • The crucial link: The system relies on the fact that the output_hash_i generated by the verifier is the cryptographic commitment to the OsOutput_i data associated with the original block i. While the Cairo code in run_bootloader.cairo doesn't explicitly show hashing the original OsOutput_i data and comparing it to the verifier's output_hash_i, the overall structure ensures this consistency. The packed_outputs hint likely guides this process, ensuring that the OsOutput_i data associated with P_i is correctly linked to the output_hash_i obtained from its verification. If the proof P_i was invalid or tampered with, the Cairo Verifier would fail or produce the wrong output_hash_i, breaking the chain.
   • Once validated (implicitly or explicitly at the layer constructing the inputs), the run_bootloader serializes the validated OsOutput_i data (along with its program_hash and size) into its final output stream (bootloader_tasks_output_ptr used later by applicative_bootloader).

In essence: The output_hash produced by the Cairo Verifier serves as the ground truth hash for the output data (OsOutput) of the program execution it verified. The bootloader infrastructure ensures this link is maintained when propagating the OsOutput data.

End-to-End Aggregation Flow (Question 3)

Here's the step-by-step process for aggregating N block proofs (P_1, ..., P_N):

Initial State:

• N Starknet OS executions completed for blocks 1 to N.
• We have N STARK proofs: P_1, ..., P_N.
• We have the corresponding claimed public outputs: OsOutput_1, ..., OsOutput_N.
• We have the Aggregator program and the Bootloader programs (Simple, Bootloader, Applicative).

Aggregation Step (Executed within the Applicative Bootloader):

1. Run Recursive Verification (run_bootloader):

   • The Applicative Bootloader invokes run_bootloader.
   • Input: The list of N original tasks (implicitly, proofs P_1..P_N and their associated claimed OsOutput_1..N data), bootloader configuration, and the packed_outputs structure describing the verification hierarchy.

     // In applicative_bootloader.cairo
     // ... prepare bootloader_input containing tasks, config, packed_outputs ...
     run_bootloader{output_ptr=bootloader_output_ptr}();

   • Process:
     • run_bootloader calls run_simple_bootloader.
     • run_simple_bootloader iterates through tasks. For tasks requiring verification (based on packed_outputs), it calls execute_task to run the Cairo Verifier program with the relevant proof P_i as input.
     • The Cairo Verifier (cairo_verifier.cairo) verifies P_i and outputs CairoVerifierOutput { program_hash, output_hash_i }.
     • run_bootloader (in parse_tasks / unpack_composite_packed_task) processes this verifier output, implicitly confirming the integrity of OsOutput_i via output_hash_i.
     • run_bootloader concatenates the validated outputs (e.g., TaskOutputHeader { size, program_hash_os } followed by the serialized OsOutput_i data) for all N tasks into a single memory segment.
   • Output: A memory segment starting at bootloader_output_start, containing bootloader config, total task count, and the concatenated verified task outputs (pointed to by bootloader_tasks_output_ptr).

   graph TD
       subgraph run_bootloader Phase
           A["Input: P_1..N, OsOutput_1..N (claimed)"] --> B{For each task i};
           B --> C{Run SimpleBootloader Task: Verify P_i};
           C --> D[CairoVerifier Output: output_hash_i];
           D --> E["Validate OsOutput_i against output_hash_i (Implicit Check)"];
           E -- Success --> F[Append validated OsOutput_i to output stream];
           F --> B;
           B -- Done --> G[Output: Concatenated Verified Outputs];
       end
   

   Loading

2. Run Aggregator Program:

   • The Applicative Bootloader invokes run_simple_bootloader again, this time with only the Aggregator program task.
   • Input: The Aggregator program code and its specific inputs (which include the claimed OsOutput_1..N passed via hints).

     // In applicative_bootloader.cairo
     // ... prepare simple_bootloader_input for aggregator_task ...
     run_simple_bootloader{output_ptr=aggregator_output_ptr}();

   • Process:
     • The Aggregator program (aggregator/main.cairo) parses the claimed OsOutput_1..N from hints.
     • It calls combine_blocks (aggregator/combine_blocks.cairo), which iterates through the OsOutput data and performs assert checks for sequential consistency:

       // In combine_blocks_inner
       assert current.header.state_update_output.initial_root = aggregated.header.state_update_output.final_root;
       assert current.header.prev_block_hash = aggregated.header.new_block_hash;
       // ... other checks ...

     • The Aggregator calculates the final CombinedOutput.
     • It serializes its claimed inputs (output_blocks in main.cairo) into its output stream (at aggregator_input_ptr).
     • It serializes the CombinedOutput into its output stream (at aggregated_output_ptr).
   • Output: A memory segment (from aggregator_output_start to aggregator_output_end) containing the header, the serialized claimed inputs, and the serialized combined output. A proof P_agg is generated for this execution.

   graph TD
       subgraph Aggregator Execution Phase
           H["Input: Claimed OsOutput_1..N (via hints)"] --> I{combine_blocks_inner Loop};
           I --> J["Assert OsOutput_i links to OsOutput_{i+1}"];
           J -- Success --> I;
           I -- Done --> K[Compute CombinedOutput];
           J -- Failure --> L[Error];
           K --> M[Output: Serialized Claimed Inputs & CombinedOutput];
       end
   

   Loading

3. The Final Link (memcpy Check):

   • This happens within the Applicative Bootloader after both Step 1 and Step 2 have completed.

   • It compares the memory segment containing the verified outputs from run_bootloader (Step 1) with the memory segment where the Aggregator claimed its inputs were (Step 2).

     // In applicative_bootloader.cairo
     let bootloader_tasks_output_ptr = &bootloader_output_start[2]; // Points to verified outputs from Step 1
     let bootloader_tasks_output_length = bootloader_output_end - bootloader_tasks_output_ptr;
     
     // aggregator_input_ptr points into the Aggregator's output stream (Step 2)
     // where it wrote its *claimed* inputs.
     memcpy(
         dst=aggregator_input_ptr,
         src=bootloader_tasks_output_ptr,
         len=bootloader_tasks_output_length,
     );

   • Significance: This memcpy acts as a powerful assertion. It fails if the number of tasks, program hashes, or any byte of the serialized OsOutput data differs between what run_bootloader produced (verified) and what the Aggregator claimed it used. This cryptographically links the Aggregator's computation (including its internal consistency checks) to the outputs derived from the verified proofs P_1...P_N.

4. Final Output and Proof:

   • The Applicative Bootloader takes the CombinedOutput part from the Aggregator's output stream (now proven to be based on verified inputs) and places it in its own final output stream.

     // In applicative_bootloader.cairo
     let aggregated_output_ptr = aggregator_input_ptr + bootloader_tasks_output_length;
     let aggregated_output_length = aggregator_output_end - aggregated_output_ptr;
     memcpy(dst=output_ptr, src=aggregated_output_ptr, len=aggregated_output_length);

   • A STARK proof, P_app_boot, is generated for the entire execution of the Applicative Bootloader program.

   graph TD
       subgraph Applicative Bootloader Orchestration
           N["Input: P_1..N, OsOutput_1..N (claimed), Aggregator Task"] --> O["Step 1: Run `run_bootloader`"];
           O --> P["Verified Outputs Stream @ `bootloader_tasks_output_ptr`"];
           N --> Q["Step 2: Run Aggregator Task"];
           Q --> R["Aggregator Output Stream (contains claimed inputs @ `aggregator_input_ptr`, combined output @ `aggregated_output_ptr`)"];
           P & R --> S["Step 3: `memcpy` Check"];
           S -- Success --> T["Step 4: Copy Combined Output"];
           T --> U["Final Output Stream"];
           S -- Failure --> V["Error"];
       end
       W["Final Proof: P_app_boot (proves entire Applicative Bootloader execution)"]
   

   Loading

Result: Verifying the single proof P_app_boot guarantees:

• The Aggregator program executed correctly (P_agg was implicitly verified).
• The Aggregator's internal chain-linking assertions held (combine_blocks_inner checks).
• All individual block proofs P_1, ..., P_N were valid (verified by the recursive run_bootloader).
• The data the Aggregator actually used for its checks was identical to the verified outputs corresponding to proofs P_1, ..., P_N (guaranteed by the memcpy check).

This P_app_boot can then be used as an input to a subsequent aggregation step, allowing for hierarchical proof combination.

Conclusion

Starknet's proof aggregation leverages multiple Cairo programs working in concert. The Cairo Verifier provides the core proof-check capability. The Simple Bootloader executes tasks (like verification). The Bootloader (run_bootloader) orchestrates verification of multiple proofs and prepares a verified output stream. The Aggregator checks the logical consistency between block outputs. Finally, the Applicative Bootloader ties everything together, running the verification and aggregation steps and performing a critical memcpy check to ensure the Aggregator operated on the genuinely verified data. The resulting single proof encapsulates the validity and sequential integrity of all aggregated blocks.