Merge pull request #2 from zksecurity/kata/proof-splitter

proof splitter

src/starkex/proof-splitter.md

@@ -0,0 +1,65 @@
+Due to the gas limitations when verifying an original STARK proof, the proof generated by the Stone Prover should be split into three types: the main proof, Trace Merkle proof, and FRI proof. Typically, this includes one Main Proof accompanied by several Trace Merkle Proofs and FRI Proofs.
+
+This process depends on the [fact registry](https://zksecurity.github.io/stark-book/starkex/facts.html), which serves as verification snapshots. This allows the Main Proof to be verified based on earlier snapshots obtained from the Merkle Proofs and FRI Proofs, thereby circumventing the bottleneck caused by gas limitations in a single EVM transaction.
+
+This section aims to clarify the roles of the various proof types, showing how the split proof works with references to the source code in [Cairo verifier contracts](https://github.com/starkware-libs/starkex-contracts), [Stone Prover](https://github.com/starkware-libs/stone-prover) and  [Stark EVM Adapter](https://github.com/zksecurity/stark-evm-adapter).
+
+### Main proof
+
+The Main Proof performs two key functions:
+1. Deriving a deep composition polynomial $p_0$
+2. Checking FRI layers for $p_0$
+
+> This explanation reuses the notations from the [ethSTARK paper](https://eprint.iacr.org/2021/582.pdf).
+
+The Main Proof contains the commitments [for](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout6/StarkVerifier.sol#L513) [the](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout6/StarkVerifier.sol#L524) [traces](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout6/StarkVerifier.sol#L534) and [FRI](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout6/StarkVerifier.sol#L553), as well as the trace values for deriving the polynomial $p_0$.
+
+These trace values, also referred to as mask values, can be categorized into two types:
+
+1. Trace values involved in expressing $C_j(x)$ in the following composition polynomial:
+
+
+$$h(x) = \sum_{j=1}^{k} C_j(x) (\alpha_j x^{D-D_j^{-1}} + \beta_j)$$
+
+
+
+2. Evaluations of the polynomials $h_i(x)$ decomposed from the $h(x)$: 
+
+
+$$h(x) = \sum_{i=0}^{M_2-1} x^i h_i(x^{M_2})
+$$
+
+By invoking the [CpuConstraintPoly](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout5/CpuVerifier.sol#L364) contract to evaluate the $h(x)$ with the trace mask values, it checks the out-of-domain-sampling (oods) consistency among these provided trace values and the evaluations of decomposed composition polynomial.
+
+After completing the OODS consistency check, it proceeds to prepares and verifies the FRI layers for $p_0​$.
+
+Conducting the FRI test requires the evaluation domain of $p_0$ to be within the expected domain for low degree linear extension instead of the out of domain (todo: maybe it is more appropriate to say field extension for the out of domain here?). The FRI protocol cannot process queries for out-of-domain evaluation points due to computational feasibility constraints for the prover.
+
+Therefore, the trace values and evaluations of the decomposed composition polynomial should be induced from a domain aligned with a low-degree extension. These newly induced values, as opposed to those used for the OODS consistency check, are utilized to derive the [deep composition polynomial](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout5/StarkVerifier.sol#L429) $p_0$ through the [CpuOods contract](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout5/CpuOods.sol#L36):
+
+$$p_0(x) = \sum_{\ell=0}^{M_1-1} \frac{\gamma_\ell \cdot (f_{j\ell}(x) - y_\ell)}{x - z g_\ell^e} + \sum_{i=0}^{M_2-1} \frac{\gamma_{M_1+i} \cdot (h_i(x) - \hat{y}_i)}{x - z^{M_2}}
+$$
+
+Here $f_j$ is the trace polynomial and $h_i$ is the decomposed composition polynomial, corresponding to the same polynomials resulting in the OODS values but in different evaluation domains.
+
+In the first FRI layer computation stage, the contract reads these induced values based on FRI queries and decommits them from the main proof. Three traces are required for the Cairo verifier: [execution trace](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/StarkVerifier.sol#L395), [interaction trace](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/StarkVerifier.sol#L405) and [composition trace](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/StarkVerifier.sol#L415). Each decommitment checks against a [trace commitment](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/StarkVerifier.sol#L400), which should have been verified and registered as [a fact](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/MerkleStatementVerifier.sol#L47) in the Merkle fact registry. 
+
+These facts serve as verification [snapshots](https://zksecurity.github.io/stark-book/starkex/facts.html), which are crucial when it is needed to split a verification into multiple stages. This approach is necessary due to various reasons, such as circumventing gas cost limitations or conserving gas costs for transaction retries based on a verified snapshot.
+
+Similarly, the process of checking the FRI layers depends on the FRI Merkle verification snapshots obtained earlier. It involves verifying whether the [fact is registered](https://github.com/starkware-libs/starkex-contracts/blob/f4ed79bb04b56d587618c24312e87d81e4efc56b/evm-verifier/solidity/contracts/cpu/layout5/Fri.sol#L93) with the FRI layer's commitment.
+
+### Other split proofs
+In order to provide the verfication snapshots for the Main Proof, it is essential to first complete both the Trace Merkle Proofs and the FRI Merkle Proofs. These preliminary steps are necessary to generate the verification snapshots required for the Main Proof.
+
+The [MerkleStatementContract](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/MerkleStatementContract.sol#L15) and [FriStatementContract](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/FriStatementContract.sol#L23) are specifically designed for verifying the Trace Merkle Proofs and FRI Merkle Proofs, respectively. Upon successful verification, [these](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/FriStatementContract.sol#L85) [facts](https://github.com/starkware-libs/starkex-contracts/blob/f81ba5fdbd68516db50ea9679de9d0ac2f8049d8/evm-verifier/solidity/contracts/MerkleStatementContract.sol#L104) will be registered as verification snapshots.
+
+### Proof annotations
+With the original proof file obtained from the Stone Prover, it is necessary to run its CPU verifier to [generate the annotations](https://github.com/starkware-libs/stone-prover/blob/a78ff37c1402dc9c3e3050a1090cd98b7ff123b3/src/starkware/main/verifier_main_helper.cc#L36-L45). This process is akin to operating an offline simulator, which verifies the proof and simulates the required proof data as annotations. These annotations are then utilized by verifiers in other locations, such as the EVM Cairo verifier.
+
+The primary reason for generating these annotations, rather than extracting directly from the original proof, would be to facilitate the restructuring of the data in the original proof into a clearer format. This restructuring is particularly beneficial for other verification procedures, such as those employed by EVM Cairo verifiers.
+
+[Here](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L2) is an example of an annotated proof. This example showcases how annotations are combined with the original proof into a single JSON file for further processing. The annotations themselves represent various data points, including [different](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L5) [trace](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L12) [commitments](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L14), the [challenges](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L6-L11) [from](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L13) [verifier](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L15), the [mask values](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L16-L30) for out-of-domain (OODS) consistency checks, FRI [commitments](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L288-L301) and corresponding [trace decommitments](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L335-L349) for [queries](https://github.com/zksecurity/stark-evm-adapter/blob/f4f2c88bd30c157423f67564d9ea3481b70c0a3c/tests/fixtures/annotated_proof.json#L302-L334).
+
+
+### Open source library
+The [Stark EVM Adapter](https://github.com/zksecurity/stark-evm-adapter) provides an API to facilitate the splitting of original proofs from the Stone Prover into these segmented proofs. This library is particularly useful for developers working with STARK proofs in EVM environments. Included in the repository is a demo script that illustrates the complete process of [splitting a Stone proof](https://github.com/zksecurity/stark-evm-adapter/blob/20cb1a83ddcbbd092f8aa6cf3382383b1c0e9814/examples/verify_stone_proof.rs#L68). This script demonstrates not only how to split the proof but also how to [submit the resultant proofs to the Cairo verifier contracts](https://github.com/zksecurity/stark-evm-adapter/blob/20cb1a83ddcbbd092f8aa6cf3382383b1c0e9814/examples/verify_stone_proof.rs#L71-L96).