diff --git a/assets/agg-2.png b/assets/agg-2.png new file mode 100644 index 0000000000..11fcc8de81 Binary files /dev/null and b/assets/agg-2.png differ diff --git a/assets/agg.png b/assets/agg.png new file mode 100644 index 0000000000..2e03723445 Binary files /dev/null and b/assets/agg.png differ diff --git a/docs/specs/aggregation.md b/docs/specs/aggregation.md deleted file mode 100644 index 4c2c1f83cc..0000000000 --- a/docs/specs/aggregation.md +++ /dev/null @@ -1,103 +0,0 @@ -# Aggregation - -We describe our strategy for aggregating STARK proofs at a high-level. - - - -## Static Aggregation - -Assume that we have a static (i.e., known ahead of time) list `allowed_vks` of STARK verifying keys (unique identifiers for STARK circuits). - -Suppose we have a variable-length list of proofs `proofs` where `proofs.len()` is independent of `allowed_vks.len()`. The goal is to produce a single STARK proof that asserts that `proofs[i]` verifies with respect verifying key `vk[i]` where `allowed_vks` contains `vk[i]`, for all `i`. Additionally, there should be the optionality to store a commitment to the ordered list of `(hash(vk[i]), public_values[i])` where `public_values[i]` are the public values of proof `i`. - -We aggregate `proofs` using a tree-structure. The arity of the tree can be adjusted for performance; -by default it is 2. The height of the tree is variable and equal to $\lceil \log{n} \rceil$ where $n$ is the number of proofs and the base of logarithm is the arity. - -We distinguish between three types of nodes in the tree: - -- Leaf -- Internal -- Root - -Each node of the tree will be a STARK VM circuit, _without continuations_, proving a VM program that runs STARK verification on an `arity` number of proofs. We make the distinction that each type of node in the tree may be a **different** VM circuit, meaning with different chip configurations. All VM circuits must support the opcodes necessary to do STARK verification. - -For each node type, a different program is run in the VM circuit: - -- Leaf: the program verifies `<=leaf_arity` proofs, where each proof is verified with respect to one of the verification keys in `allowed_vks`. The leaf program will have the proof, public values, and verifying keys of each proof in program memory, and the program can be augmented with additional checks (for example, state transitions checks are necessary for continuations). -- Internal: the program verifies `<= internal_arity` proofs, where all proofs are verified with respect to the same verifying key. This verifying key is either that of a leaf circuit or that of an internal circuit (the present circuit itself). The circuit cannot know the verifying key of itself, so to avoid a circular dependency, the hash of the verifying key is made a public value. -- Root: this program _may_ just be the same as the Internal program, but for the purposes of optimizing [on-chain aggregation](#on-chain-aggregation), there is the possiblity for it to be different. The root program verifies `<= root_arity` proofs, where all proofs are of the internal circuit. Note that `root_arity` may be `1`. - -### STARK Configurations - -Before proceeding, we must discuss the topic of STARK configurations: any STARK proof depends on at least three configuration parameters: - -- `F` the base field of the AIRs -- `EF` the extension field of the AIRs used for challenge values -- the hash function used for the FRI PCS. This hash function must be able to hash `F` and `EF` elements, where elements can be packed before hashing. - -For all Leaf and Internal circuits [above](#static-aggregation), we use an **Inner Config**. Example Inner Configs are: - -- `F` is BabyBear, `EF` is quartic extension of BabyBear, hash is BabyBearPoseidon2 -- `F` is BabyBear, `EF` is quartic extension of BabyBear, hash is SHA256 -- `F` is Mersenne31, `EF` is quartic extension of Mersenne31, hash is Mersenne31Poseidon2 -- `F` is Mersenne31, `EF` is quartic extension of Mersenne31, hash is SHA256 - -We discuss considerations for choice of hash below. - -On the other hand, the Root circuit will use an **Outer Config**. Example Outer Configs are: - -- `F` is BabyBear, `EF` is quartic extension of BabyBear, hash is BN254FrPoseidon2 (or BN254FrPoseidon1) -- ~~`F` is BabyBear, `EF` is quartic extension of BabyBear, hash is SHA256~~ -- `F` is BN254Fr, `EF` is BN254Fr, hash is BN254FrPoseidon2 (or BN254FrPoseidon1) -- ~~`F` is BN254Fr, `EF` is BN254Fr, hash is SHA256~~ -- Analogous configurations with BabyBear replaced with Mersenne31. - -To explain, since `31 * 8 < 254`, eight BabyBear field elements can be packed together and embedded (non-algebraically) into a BN254Fr field element. In this way BN254FrPoseidon2 can be used to hash BabyBear elements. - -The choice of hash function in the Outer Config only affects what hash must be verified in the Halo2 circuit for on-chain aggregation (see [below](#on-chain-aggregation)). For performance, it is therefore always better to use BN254FrPoseidon2 for the Outer Config. - -### On-chain Aggregation - -The Root circuit above is the last STARK circuit, whose single proof will in turn verify all initial `proofs`. Due to the size of STARK proofs, for on-chain verification we must wrap this proof inside an elliptic curve based SNARK proof so that the final SNARK proof can be verified on-chain (where on-chain currently means within an Ethereum Virtual Machine). - -We create a Halo2 circuit that verifies any proof of the Root STARK circuit. This is a non-universal circuit whose verifying key depends on the specific STARK circuit to be verified. The majority of the verification logic can be code-generated into the `halo2-lib` eDSL which uses a special vertical custom gate specialized for cheap on-chain verification cost. There are two main performance considerations: - -#### 1. Hash - -To perform FRI verification in the Halo2 circuit, the circuit must constrain calculations of STARK Outer Config hashes. As mentioned above, this hash will be BN254FrPoseidon2. The constraints for this hash can either be implemented directly using the `halo2-base` vertical gate, or with a custom gate. The custom gate will be faster but with higher verification cost. There are two approaches to consider: - -Approach A - -- Use a single Halo2 circuit with only thinnest `halo2-base` vertical gate to verify the Root STARK circuit proof. - -Approach B - -- Use a first Halo2 circuit with custom gate for BN254FrPoseidon2 to verify the Root STARK circuit proof. -- Use a second Halo2 circuit with only the thinnest `halo2-base` vertical gate to verify the previous Halo2 circuit. - -Approach B is likely better, provided that the time to generate both proofs is faster than the time to generate the single proof in Approach A. - -#### 2. Outer Config Base Field - -The Outer Config base field `F` can be either a 31-bit field or BN254Fr. - -When `F` is 31-bit field: - -- For FRI folding and other arithmetic in STARK verification, the Halo2 circuit must perform BabyBear prime field arithmetic and extension field arithmetic inside the halo2 circuit. These are non-native arithmetic operations. - -When `F` is BN254Fr and `EF` is BN254Fr: - -- Halo2 circuit only needs to perform native field arithmetic inside the halo2 circuit. -- The Root STARK circuit must now perform non-native BabyBear field arithmetic and extension field arithmetic inside the STARK to support the verification of the STARKs with the Inner Config. This non-native arithmetic is still expected to be much faster in the STARK than in Halo2, but the added chip complexity may also increase verifier cost in the Halo2 circuit. -- If the Inner Config hash is BabyBearPoseidon2, now the Root STARK circuit must constrain BabyBearPoseidon2 inside a circuit with base field BN254Fr. This is definitely not efficient. **Therefore it is not possible for the Outer Config base field to be BN254Fr if the Inner Config hash is BabyBearPoseidon2.** -- This Outer Config is only possible if the Inner Config hash is a hash that does not depend on the native field (e.g., SHA256 or Blake2b or Blake3). - - **Observation:** even if the hash used for the Internal circuit is SHA256, the Leaf circuit can still be proven using BabyBearPoseidon2. Likewise, it is even possible to have the Internal circuits use BabyBearPoseidon2 at higher depths in the tree (away from the root). The only requirement is that the last Internal circuit proof, which will be verified by the Root circuit, needs to be proven with SHA256 as the hash. - -TODO: to determine which Outer Config is best, we will: - -- Instrument the cost of non-native small field arithmetic in the Halo2 circuit. -- Benchmark an aggregation VM with Inner Config hash BabyBearPoseidon2 proven over BabyBearPoseidon2 versus one with Inner Config hash SHA256 proven over SHA256. - -## Dynamic Aggregation - -TODO diff --git a/docs/specs/continuations.md b/docs/specs/continuations.md index f45c847eaf..65f518fe65 100644 --- a/docs/specs/continuations.md +++ b/docs/specs/continuations.md @@ -1,3 +1,201 @@ +# Aggregation + +Given the execution segments of a program, each segment will be proven in parallel within a **Application VM** (App VM). +These proofs are subsequently aggregated into an aggregation tree by a **leaf aggregation +program**. This segment aggregation program runs inside _a different VM_, referred to as the **Aggregation VM** (Agg +VM), which operates without continuations enabled. + +The aggregation program takes a variable number of consecutive segment proofs and consolidates them into a single proof +that captures the entire range of segments. + +![Aggregation example](../../assets/agg.png) + +The following figure shows that the shape of the aggregation tree is not fixed. + +![Another aggregation example](../../assets/agg-2.png) + +We will now give an overview of the steps of the overall aggregation, starting from the final smart contract verifier +and going down to the application proof. + +## Smart Contract + +A smart contract is deployed by on-chain, which provides a function to verify a Halo2 proof. + +## Static Verifier Wrapper + +The **Static Verifier Wrapper** is a Halo2 SNARK verifier circuit generated by OpenVM. The static verifier +wrapper is determined by the following parameters: + +* Number of public values +* The Aggregation VM chip constraints (but **not** the App VM chips) + +## Continuation Verifier + +The continuation verifier is a Halo2 circuit (static verifier) together with some single segment VM circuits (Agg VM). +The continuation verifier depends on the specific circuit design of the static verifier and Aggregation VM, as well as +the number of user public values, but it does not depend on the App VM's circuit. + +The continuation verifier ensures that a set of ordered App VM segment proofs collectively validates the execution of a +specific `VmExe` on a specific App VM, with given inputs. + +### Static Verifier + +The Static Verifier is a Halo2 verifier circuit that validates a Root VM Verifier proof and exposes its public values. + +Static Verifier Requirements: + +* The height of each trace is fixed. +* Trace heights are in a descending order. + +Public Values Exposed: + +* Exe commit encoded in Bn254 +* Leaf commit encoded in Bn254 +* User public values in BabyBear + +Parameters (which could result in a different circuit): + +* Number of public values (from upper stream) +* k in Halo2 +* Determines the number of columns of the circuit. + +* Number of public values (from upstream) +* k in Halo2 (determines the number of columns in the circuit) +* Root VM verifier + * VK (including the heights of all traces) + * Root verifier program commitment + +### Aggregation VM + +The Aggregation VM organizes proofs into an aggregation tree, where nodes include: + +* Root VM Verifier +* Internal VM Verifier +* Leaf VM Verifier + +Each node can have an arbitrary number of children, enabling flexible tree structures to optimize for cost reduction +(more children) or latency reduction (less children) during proving. + +### Root VM Verifier + +The Root VM Verifier is proven in RootConfig, using commitments via Bn254Poseidon2. All traces are padded to a constant +height for verification. + +The Root VM Verifier verifies 1 or more proofs of: + +- Leaf VM Verifier +- Internal VM Verifier + +In practice, Root VM verifier only verifies one proof to guarantee constant heights. + +Logical Input: + +* Root input + +Cached Trace Commit: + +* `ProgramAir`: commits the root verifier program + +Public values: + +* `RootVmVerifierPvs` + * Note: exe_commit is the commitment of the executable. The way to compute it can be found here. + +Parameters: + +* For circuit: + * Root VM Config +* For root verifier program: + * Root FRI parameters to compute its commitment + * Internal verifier circuit \+ program commitment + * Leaf verifier circuit \+ program commitment + +### Internal VM Verifier + +The Internal VM Verifier validates one or more proofs of: + +* Leaf VM Verifier +* Internal VM Verifier + +Logical Input: + +* `InternalVmVerifierInput` + +Cached Trace Commit: + +* `ProgramAir`: commits the internal verifier program. `agg_vm_pk` contains it. + +Public values: + +* `InternalVmVerifierPvs` + +Parameters: + +* For circuit: + * Internal VM Config +* For root verifier program: + * Internal FRI parameters to compute its commitment + * Internal verifier circuit \+ program commitment + * Leaf verifier circuit \+ program commitment + +### Leaf VM Verifier + +Verify 1 or more proofs of: + +* segment circuits + +Logical Input: + +* `LeafVmVerifierInput` + +Cached Trace Commit: + +* ProgramAir: commits the leaf verifier program. The leaf verifier program commits . + +Public values: + +* `VmVerifierPvs` + +Parameters: + +* For circuit: + * Leaf VM Config +* For leaf verifier program: + * It’s not a part of the Continuation Verifier because it depends on the VK of the App VM and it doesn’t affect the VK + of the static verifier. + +### App VM + +App VM executes an executable with inputs and returns a list of segment proofs. + +## Segment + +Logical Input: + +* App VM input stream + +Cached Trace Commit: + +* ProgramAir: commits the program the App VM executed. + +Public values: + +* `VmConnectorPvs` +* `MemoryMerklePvs` + +User Public Values: + +* Up to `num_public_values` public values in a dedicated memory space. These public values are not exposed as public + values of segment circuits, but will be exposed by the final proof. + +Parameters: + +* Number of public values (from upstream) +* For circuit: + * App VM Config +* For App program: + * App FRI parameters to compute its commitment. + # Continuations Our high-level continuations framework follows previous standard designs (Starkware, Risc0), but uses a novel persistent @@ -82,9 +280,4 @@ and has the following interactions on the MERKLE_BUS**(-1, 0, (as - AS_OFFSET) \* 2^L, node_label, hash_final)** It receives `values` from the `MEMORY_BUS` and constrains `hash = compress(values, 0)` via the `POSEIDON2_DIRECT_BUS`. - -## Aggregation - -Given the execution segments of a program, we will prove each segment in a VM segment circuit in parallel. These proofs will then be aggregated in an [aggregation tree](../aggregation.md) by a segment aggregation program. This segment aggregation program will be run inside **a different VM** which **does not** have continuations turned on. The latter VM is called an **Aggregation VM**. - -See [Aggregation](../aggregation.md) for more details. +The aggregation program takes a variable number of consecutive segment proofs and consolidates them into a single proof