commit new page

Author: kmurphypolygon

docs/cdk/architecture/type-1-prover/intro-t1-prover.md

@@ -27,4 +27,4 @@ The figure below gives a visual summary of the types, contrasting compatibility
 
 Ultimately, choosing which type of ZK-EVM to develop involves a trade-off between EVM-equivalence and performance.
 
-The challenge this poses for developers who favor exact Ethereum-equivalence is to devise ingenious designs and clever techniques to implement faster zk-provers. Vitalik mentions one mitigation strategy to improve proof generation times: Cleverly engineered, and massively parallelized provers.
+The challenge this poses for developers who favor exact Ethereum-equivalence is to devise ingenious designs and clever techniques to implement faster zk-provers. Vitalik mentions one mitigation strategy to improve proof generation times: cleverly engineered, and massively parallelized provers.

docs/cdk/architecture/type-1-prover/t1-cpu-component.md

@@ -1,17 +1,16 @@
-The CPU is the central component of Polygon Zero zkEVM. Like any central processing unit, it reads instructions, executes them, and modifies the state (registers and the memory) accordingly. 
+The CPU is the central component of the Polygon CDK type-1 prover. Like any central processing unit, it reads instructions, executes them, and modifies the state (registers and the memory) accordingly. 
 
 Other complex instructions, such as Keccak hashing, are delegated to specialized STARK tables. 
 
 This section briefly presents the CPU and its columns. However, details on the CPU logic can be found [here](https://github.com/0xPolygonZero/plonky2/blob/main/evm/spec/cpulogic.tex).
 
-
-### CPU flow
+## CPU flow
 
 CPU execution can be decomposed into two distinct phases; CPU cycles, and padding.
 
 This first phase of the CPU execution is a lot bulkier than the second, more so that padding comes only at the end of the execution.
 
-#### CPU cycles
+### CPU cycles
 
 In each row, the CPU reads code at a given program counter (PC) address, executes it, and writes outputs to memory. The code could be kernel code or any context-based code.
 
@@ -28,23 +27,21 @@ Subsequent contexts are created when executing user code.
 
 Syscalls, which are specific instructions written in the kernel, may be executed in a non-zero user context. They don't change the context but the code context, which is where the instructions are read from.
 
-#### Padding
+### Padding
 
 At the end of any execution, the length of the CPU trace is padded to the next power of two.
 
 When the program counter reaches the special halting label in the kernel, execution halts. And that's when padding should follow.
 
 There are special constraints responsible for ensuring that every row subsequent to execution halting is a padded row, and that execution does not automatically resume. That is, execution cannot resume without further instructions.
 
+## CPU columns
 
-
-### CPU columns
-
-This document discusses CPU columns as they relate to all relevant operations being executed, as well as how some of the constraints are checked.  
+We now have a look at CPU columns as they relate to all relevant operations being executed, as well as how some of the constraints are checked.  
 
 These are the register columns, operation flags, memory columns, and general columns.  
 
-#### Registers
+### Registers
 
 - $\texttt{context}$: Indicates the current context at any given time. So, $\texttt{context}\ 0$ is for the kernel, while any context specified with a positive integer indicates a user context. A user context is incremented by $1$ at every call.
 - $\texttt{code_context}$: Indicates the context in which the executed code resides.   
@@ -55,7 +52,7 @@ These are the register columns, operation flags, memory columns, and general col
 - $\texttt{clock}$: Monotonic counter which starts at 0 and is incremented by 1 at each row. It is used to enforce correct ordering of memory accesses.
 - $\texttt{opcode_bits}$  These are 8 boolean columns, indicating the bit decomposition of the opcode being read at the current PC.
 
-#### Operation flags
+### Operation flags
 
 Operation flags are boolean flags indicating whether an operation is executed or not.
 
@@ -85,8 +82,7 @@ $$
   \texttt{eq_iszero * opcode_bits[0]}
 $$
 
-
-#### Memory columns
+### Memory columns
 
 The CPU interacts with the EVM memory via its memory channels. 
 
@@ -101,7 +97,7 @@ A full memory channel is composed of the following:
 
 The last memory channel is a partial channel. It doesn't have its own $\texttt{value}$ columns but shares them with the first full memory channel. This allows saving eight columns.
 
-#### General columns
+### General columns
 
 There are eight ($8$) shared general columns. Depending on the instruction, they are used differently:
 
@@ -126,5 +122,4 @@ The `popping-only` instruction uses the $\text{Stack}$ columns to check if the S
 While the `pushing-only` instruction uses the $\text{Stack}$ columns to check if the Stack is empty before the instruction.
 
 $\texttt{stack_len_bounds_aux}$ is used to check that the Stack doesn't overflow in user mode. The last four columns are used to prevent conflicts with other general columns.
-See the $\text{Stack Handling}$ subsection of this [document](https://github.com/0xPolygonZero/plonky2/blob/main/evm/spec/cpulogic.tex) for more details.
-
+See the $\text{Stack Handling}$ subsection of this [document](https://github.com/0xPolygonZero/plonky2/blob/main/evm/spec/cpulogic.tex) for more details.

docs/cdk/architecture/type-1-prover/t1-ctl-protocol.md

@@ -4,11 +4,11 @@ For each STARK table, ordinary STARK proof and verification are used to check if
 
 However, there are input and output values shared among the tables. These values need to be checked for possible alterations while being shared among tables. For this purpose, _cross-table lookups_ (CTLs) are used in verifying that the shared values are not tampered with.
 
-### How CTLs work
+## How CTLs work
 
-The CLT protocol is based on the [logUP argment](https://eprint.iacr.org/2022/1530.pdf), which works similar to how range-checks work. Range-checks are discussed in a subsequent document to this one.
+The CTL protocol is based on the [logUP argment](https://eprint.iacr.org/2022/1530.pdf), which works similar to how range-checks work. Range-checks are discussed in a subsequent document to this one.
 
-#### Example (CTL)
+### Example (CTL)
 
 Consider the following scenario as an example. Suppose STARK $S_2$ requires an operation -- say $Op$ -- that is carried out by another STARK $S_1$.
 
@@ -26,8 +26,7 @@ And thus, this check is tantamount to ensuring that the rows of the $S_1$ table
 
 ![Figure: CTL permutation check](../../../img/cdk/t1-prover-ctl-perm-check.png)
 
-
-### How the CLT proof works
+## How the CTL proof works
 
 As outlined in the above example, verifying that shared values among STARK tables are not tampered with amounts to proving that rows of reduced STARK tables are permutations of each other.
 
@@ -40,7 +39,7 @@ The proof therefore is achieved in three steps;
    - Checking correct construction and equality of 'running sums'.
 
 
-#### Table filtering
+### Table filtering
 
 Define filters $f^1$ and $f^2$ for STARK tables $S_1$ and $S_2$ , respectively, such that
 
@@ -65,8 +64,7 @@ Next create subtables $S_1'$ and $S_2'$ of STARK tables $S_1$ and $S_2$ , respec
 
     Filters are limited to (at most) degree 2 combinations of columns.
 
-
-#### Computing running sums
+### Computing running sums
 
 For each $i \in \{0,1\}$, let $\{ c^{i,j} \}$ denote the columns of $S_i'$.
 
@@ -86,7 +84,7 @@ for $0 < l < n-1$.
 
 Note that $Z_l^{S_i}$ is computed backwards. i.e., It starts with $Z_{n-1}^{S_i}$ and goes down to $Z_0^{S_i}$ as the final sum.
 
-#### Checking running sums
+### Checking running sums
 
 After computing running sums, check equality of the final sums $Z_0^{S_1} =?\ Z_0^{S_2}$ and whether the running sums were correctly constructed.
 
@@ -97,8 +95,7 @@ The above three steps turn the CTL argument into a [LogUp lookup argument](https
 
 which checks for equality between $S_1'$ and $S_2'$.
 
-
-### CTL protocol summary
+## CTL protocol summary
 
 The cross-table protocol can be summarized as follows. 
 
@@ -113,5 +110,4 @@ On the other side, and for the same STARK table $S$, the verifier:
 
 - Computes the sum $Z = \sum_j Z_{j}^l$.
 - Checks equality, $Z =?\ Z_0^S$.
-- Checks whether each of the running sums $Z_{j}^l$ and $Z^S$ were correctly constructed. 
-
+- Checks whether each of the running sums $Z_{j}^l$ and $Z^S$ were correctly constructed. 

docs/cdk/architecture/type-1-prover/t1-design-challenge.md

@@ -2,27 +2,35 @@ The EVM wasn't designed with zero-knowledge proving and verification in mind, an
 
 Some of the challenges stem from the way the EVM is implemented. Here are some of the discrepancies that occur when deploying the most common zero-knowledge primitives to the EVM.
 
-  1. **Word size**: The native EVM word size is 256 bits long, whereas the chosen SNARK Plonky2, operates internally over 64-bit field elements.
+## Word size
 
-    Matching these word sizes requires a work-around where word operations are performed in multiples of smaller limbs for proper handling internally.
+The native EVM word size is 256 bits long, whereas the chosen SNARK Plonky2, operates internally over 64-bit field elements.
 
-    This unfortunately incurs overheads, even for simple operations like the ADD opcode.
+Matching these word sizes requires a work-around where word operations are performed in multiples of smaller limbs for proper handling internally.
+
+This unfortunately incurs overheads, even for simple operations like the ADD opcode.
 
-  2. **Supported fields:** Selecting a field for the most efficient proving scheme can become complicated.
+## Supported fields 
+
+Selecting a field for the most efficient proving scheme can become complicated.
 
-    Ethereum transactions are signed over the [secp256k1 curve](https://secg.org/sec2-v2.pdf), which involves a specific prime field $\mathbb{F}_p$, where $p = 2^{256} - 2^{32} - 2^9 - 2^8 -2^7 - 2^6 - 2^4 - 1$. The EVM also supports precompiles for [BN254 curve](https://github.com/ethereum/EIPs/blob/master/EIPS/eip-197.md) operations, where the computations are carried out in an entirely different field arithmetic.
+Ethereum transactions are signed over the [secp256k1 curve](https://secg.org/sec2-v2.pdf), which involves a specific prime field $\mathbb{F}_p$, where $p = 2^{256} - 2^{32} - 2^9 - 2^8 -2^7 - 2^6 - 2^4 - 1$. The EVM also supports precompiles for [BN254 curve](https://github.com/ethereum/EIPs/blob/master/EIPS/eip-197.md) operations, where the computations are carried out in an entirely different field arithmetic.
 
-    This adds a major overhead when it comes to proving modular arithmetic, as there is a need to deal with modular reductions in the field of the proving system.
+This adds a major overhead when it comes to proving modular arithmetic, as there is a need to deal with modular reductions in the field of the proving system.
 
-    Such incongruous modular arithmetic is not uncommon. Recursive proving schemes like [Halo](https://electriccoin.co/wp-content/uploads/2019/09/Halo.pdf) resorted to utilising two pairing-friendly elliptic curves where proving and verification are instantiated in two different field arithmetics.
+Such incongruous modular arithmetic is not uncommon. Recursive proving schemes like [Halo](https://electriccoin.co/wp-content/uploads/2019/09/Halo.pdf) resorted to utilising two pairing-friendly elliptic curves where proving and verification are instantiated in two different field arithmetics.
 
-    Other curves, such as the pairing-friendly [BLS12-381](https://eips.ethereum.org/EIPS/eip-2537) popularly used in recursive proving systems, are yet to be EVM-supported in the form of precompiled contracts.
+Other curves, such as the pairing-friendly [BLS12-381](https://eips.ethereum.org/EIPS/eip-2537) popularly used in recursive proving systems, are yet to be EVM-supported in the form of precompiled contracts.
 
-  3. **Hash functions**: The EVM uses [Keccak](https://keccak.team/keccak_specs_summary.html) as its native hash function both for state representation and arbitrary hashing requests, through the `Keccak256` opcode.
+## Hash functions
 
-    While Keccak is fairly efficient on a CPU, since Plonky2 implements polynomials of degree 3, Keccak operations would need to be expressed as constraints of degree 3. This results in an extremely heavy Algebraic Intermediate Representation (AIR) compared to some of the most recent [STARK-friendly](https://eprint.iacr.org/2020/948.pdf) hash functions, tailored specifically for zero-knowledge proving systems.
+The EVM uses [Keccak](https://keccak.team/keccak_specs_summary.html) as its native hash function both for state representation and arbitrary hashing requests, through the `Keccak256` opcode.
 
-    Although the EVM supports precompiles of hash functions such as SHA2-256, RIPEMD-160, and Blake2f, they are all quite heavy for a ZK proving system.
+While Keccak is fairly efficient on a CPU, since Plonky2 implements polynomials of degree 3, Keccak operations would need to be expressed as constraints of degree 3. This results in an extremely heavy Algebraic Intermediate Representation (AIR) compared to some of the most recent [STARK-friendly](https://eprint.iacr.org/2020/948.pdf) hash functions, tailored specifically for zero-knowledge proving systems.
+
+Although the EVM supports precompiles of hash functions such as SHA2-256, RIPEMD-160, and Blake2f, they are all quite heavy for a ZK proving system.
 
-  4. **State representation**: Ethereum uses Merkle Patricia Tries with RLP encoding. Both of these are not zero-knowledge-friendly primitives, and incur huge overheads on transaction processing within a ZK-EVM context.
+## State representation 
+
+Ethereum uses Merkle Patricia Tries with RLP encoding. Both of these are not zero-knowledge-friendly primitives, and incur huge overheads on transaction processing within a ZK-EVM context.
 

docs/cdk/architecture/type-1-prover/testing-and-proving-costs.md

@@ -1,14 +1,14 @@
-### Testing Polygon type-1 zkEVM 
+### Testing the prover
 
-Find a parser and test runner for testing compatible and common Ethereum full node tests against Polygon type-1 zkEVM [here](https://github.com/0xPolygonZero/evm-tests).
+Find a parser and test runner for testing compatible and common Ethereum full node tests against the Polygon CDK type-1 prover [here](https://github.com/0xPolygonZero/evm-tests).
 
-Polygon type-1 zkEVM passes all relevant and official [Ethereum tests](https://github.com/ethereum/tests/).
+The prover passes all relevant and official [Ethereum tests](https://github.com/ethereum/tests/).
 
 ### Proving costs
 
-Instead of presenting gas costs, we focus on the cost of proving EVM transactions with Polygon type-1 prover.
+Instead of presenting gas costs, we focus on the cost of proving EVM transactions with the Polygon CDK type-1 prover.
 
-Since Polygon type-1 zkEVM is more like a 'CPU' for the EVM, it makes sense to look at proving costs per VM instance used, as opposed to TPS or other benchmarks.
+Since the prover is more like a 'CPU' for the EVM, it makes sense to look at proving costs per VM instance used, as opposed to TPS or other benchmarks.
 
 Consider the table below for prices of GCP's specific instances, taken from [here](https://cloud.google.com/compute/all-pricing), and webpage accessed on the 29th January, 2024. 
 
@@ -19,8 +19,7 @@ Take the example of a t2d-standard-60 GCP instance, where each vCPU has 4GB memo
 - 0.00346 USD / vCPU hour
 - 0.000463 USD / GB hour
 
-We obtain the following hourly cost, $(60 \times 0.00346) + (240 \times 0.000463) = 0.31872$ USD per hour. 
-The total cost per block is given by: $\texttt{(Proving time per hr)} \times 0.31872$ USD.
+We obtain the following hourly cost, $(60 \times 0.00346) + (240 \times 0.000463) = 0.31872$ USD per hour. The total cost per block is given by: $\texttt{(Proving time per hr)} \times 0.31872$ USD.
 
 The table below displays proving costs per transaction per hour.