docs: Add Continuation VM doc to continuations.md (#1055)

* docs: Add Continuation VM doc to continuations.md

* Update language

* comments

* fix agg-2 image

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 <span style="color:green">MERKLE_BUS</
 - Receive <span style="color:green">**(-1, 0, (as - AS_OFFSET) \* 2^L, node_label, hash_final)**</span>
 
 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