Start of SMT implementation for Type 2 zkEVM (#1315)

* Add SMT types * Progress * Progress * Working smt hashing * Minor * Fix hash * Working insert * Minor * Add insert test for storage trie * Add missing constraints for DUP/SWAP (#1310) * Refactor wcopy syscalls * Refactor memcpy * Working test_simple_transfer * Modify add11_yml.rs * Refactor codecopy * Fix * Fix calldatacopy * Fix test on interpreter side * Remove new_stack_top_channel from StackBehavior (#1296) * Working add11_yml.rs * All tests compile * Working test_balance * Minor * Working test_extcodesize * All non-ignored tests pass * Fix test_empty_txn_list * Clippy * smt_utils point to github * Comments * Fix kexit_info in test * Review * Update Cargo.toml * Move empty check inside final iteration * Remerge context flags (#1292) * Remerge context flags * Apply comments and revert some unwanted changes * Merge NOT and POP flags. (#1257) * Merge NOT and POP flags * Add comments * Disable remaining memory channels for POP * Apply comments * Fix stack * More of memcpy_bytes * Add some documentation in EVM crate (#1295) Co-authored-by: Linda Guiga <[email protected]> * Combine PUSH0 and PC flags. (#1256) * PR feedback * Add context constraints (#1260) * Combine JUMPDEST and KECCAK_GENERAL flags. (#1259) * Combine JUMPDEST and KECCAK_GENERAL flags. * Apply comments * Fix merging of jumpdest and keccak_general. * Add test for selfdestruct (#1321) * Add test for selfdestruct * Comment * Fix test --------- Co-authored-by: Hamy Ratoanina <[email protected]> Co-authored-by: Robin Salen <[email protected]> Co-authored-by: Linda Guiga <[email protected]> Co-authored-by: Robin Salen <[email protected]> Co-authored-by: Linda Guiga <[email protected]> Co-authored-by: Linda Guiga <[email protected]>
0xPolygonZero · Nov 3, 2023 · c70a785 · c70a785
1 parent 44af80f
commit c70a785
Show file tree

Hide file tree

Showing 116 changed files with 2,988 additions and 2,197 deletions.
diff --git a/evm/Cargo.toml b/evm/Cargo.toml
@@ -37,6 +37,7 @@ static_assertions = "1.1.0"
 hashbrown = { version = "0.14.0" }
 tiny-keccak = "2.0.2"
 serde_json = "1.0"
+smt_utils = { git = "https://github.com/0xPolygonZero/smt_utils" }
 
 [target.'cfg(not(target_env = "msvc"))'.dependencies]
 jemallocator = "0.5.0"

diff --git a/evm/spec/tables.tex b/evm/spec/tables.tex
@@ -3,6 +3,7 @@ \section{Tables}
 
 \input{tables/cpu}
 \input{tables/arithmetic}
+\input{tables/byte-packing}
 \input{tables/logic}
 \input{tables/memory}
 \input{tables/keccak-f}

diff --git a/evm/spec/tables/byte-packing.tex b/evm/spec/tables/byte-packing.tex
@@ -0,0 +1,4 @@
+\subsection{Byte Packing}
+\label{byte-packing}
+
+TODO
diff --git a/evm/spec/zkevm.pdf b/evm/spec/zkevm.pdf
diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs
@@ -23,6 +23,7 @@ use crate::memory::memory_stark;
 use crate::memory::memory_stark::MemoryStark;
 use crate::stark::Stark;
 
+/// Structure containing all STARKs and the cross-table lookups.
 #[derive(Clone)]
 pub struct AllStark<F: RichField + Extendable<D>, const D: usize> {
     pub arithmetic_stark: ArithmeticStark<F, D>,
@@ -36,6 +37,7 @@ pub struct AllStark<F: RichField + Extendable<D>, const D: usize> {
 }
 
 impl<F: RichField + Extendable<D>, const D: usize> Default for AllStark<F, D> {
+    /// Returns an `AllStark` containing all the STARKs initialized with default values.
     fn default() -> Self {
         Self {
             arithmetic_stark: ArithmeticStark::default(),
@@ -64,6 +66,7 @@ impl<F: RichField + Extendable<D>, const D: usize> AllStark<F, D> {
     }
 }
 
+/// Associates STARK tables with a unique index.
 #[derive(Debug, Copy, Clone, Eq, PartialEq)]
 pub enum Table {
     Arithmetic = 0,
@@ -75,9 +78,11 @@ pub enum Table {
     Memory = 6,
 }
 
+/// Number of STARK tables.
 pub(crate) const NUM_TABLES: usize = Table::Memory as usize + 1;
 
 impl Table {
+    /// Returns all STARK table indices.
     pub(crate) fn all() -> [Self; NUM_TABLES] {
         [
             Self::Arithmetic,
@@ -91,6 +96,7 @@ impl Table {
     }
 }
 
+/// Returns all the `CrossTableLookups` used for proving the EVM.
 pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
     vec![
         ctl_arithmetic(),
@@ -103,13 +109,15 @@ pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
     ]
 }
 
+/// `CrossTableLookup` for `ArithmeticStark`, to connect it with the `Cpu` module.
 fn ctl_arithmetic<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(
         vec![cpu_stark::ctl_arithmetic_base_rows()],
         arithmetic_stark::ctl_arithmetic_rows(),
     )
 }
 
+/// `CrossTableLookup` for `BytePackingStark`, to connect it with the `Cpu` module.
 fn ctl_byte_packing<F: Field>() -> CrossTableLookup<F> {
     let cpu_packing_looking = TableWithColumns::new(
         Table::Cpu,
@@ -132,9 +140,9 @@ fn ctl_byte_packing<F: Field>() -> CrossTableLookup<F> {
     )
 }
 
-// We now need two different looked tables for `KeccakStark`:
-// one for the inputs and one for the outputs.
-// They are linked with the timestamp.
+/// `CrossTableLookup` for `KeccakStark` inputs, to connect it with the `KeccakSponge` module.
+/// `KeccakStarkSponge` looks into `KeccakStark` to give the inputs of the sponge.
+/// Its consistency with the 'output' CTL is ensured through a timestamp column on the `KeccakStark` side.
 fn ctl_keccak_inputs<F: Field>() -> CrossTableLookup<F> {
     let keccak_sponge_looking = TableWithColumns::new(
         Table::KeccakSponge,
@@ -149,6 +157,8 @@ fn ctl_keccak_inputs<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(vec![keccak_sponge_looking], keccak_looked)
 }
 
+/// `CrossTableLookup` for `KeccakStark` outputs, to connect it with the `KeccakSponge` module.
+/// `KeccakStarkSponge` looks into `KeccakStark` to give the outputs of the sponge.
 fn ctl_keccak_outputs<F: Field>() -> CrossTableLookup<F> {
     let keccak_sponge_looking = TableWithColumns::new(
         Table::KeccakSponge,
@@ -163,6 +173,7 @@ fn ctl_keccak_outputs<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(vec![keccak_sponge_looking], keccak_looked)
 }
 
+/// `CrossTableLookup` for `KeccakSpongeStark` to connect it with the `Cpu` module.
 fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
     let cpu_looking = TableWithColumns::new(
         Table::Cpu,
@@ -177,6 +188,7 @@ fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(vec![cpu_looking], keccak_sponge_looked)
 }
 
+/// `CrossTableLookup` for `LogicStark` to connect it with the `Cpu` and `KeccakSponge` modules.
 fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
     let cpu_looking = TableWithColumns::new(
         Table::Cpu,
@@ -197,6 +209,7 @@ fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(all_lookers, logic_looked)
 }
 
+/// `CrossTableLookup` for `MemoryStark` to connect it with all the modules which need memory accesses.
 fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
     let cpu_memory_code_read = TableWithColumns::new(
         Table::Cpu,

diff --git a/evm/src/arithmetic/addcy.rs b/evm/src/arithmetic/addcy.rs
@@ -149,7 +149,7 @@ pub(crate) fn eval_packed_generic_addcy<P: PackedField>(
     }
 }
 
-pub fn eval_packed_generic<P: PackedField>(
+pub(crate) fn eval_packed_generic<P: PackedField>(
     lv: &[P; NUM_ARITH_COLUMNS],
     yield_constr: &mut ConstraintConsumer<P>,
 ) {
@@ -236,7 +236,7 @@ pub(crate) fn eval_ext_circuit_addcy<F: RichField + Extendable<D>, const D: usiz
     }
 }
 
-pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
+pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     lv: &[ExtensionTarget<D>; NUM_ARITH_COLUMNS],
     yield_constr: &mut RecursiveConstraintConsumer<F, D>,

diff --git a/evm/src/arithmetic/arithmetic_stark.rs b/evm/src/arithmetic/arithmetic_stark.rs
@@ -22,8 +22,8 @@ use crate::evaluation_frame::{StarkEvaluationFrame, StarkFrame};
 use crate::lookup::Lookup;
 use crate::stark::Stark;
 
-/// Link the 16-bit columns of the arithmetic table, split into groups
-/// of N_LIMBS at a time in `regs`, with the corresponding 32-bit
+/// Creates a vector of `Columns` to link the 16-bit columns of the arithmetic table,
+/// split into groups of N_LIMBS at a time in `regs`, with the corresponding 32-bit
 /// columns of the CPU table. Does this for all ops in `ops`.
 ///
 /// This is done by taking pairs of columns (x, y) of the arithmetic
@@ -57,7 +57,8 @@ fn cpu_arith_data_link<F: Field>(
     res
 }
 
-pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
+/// Returns the `TableWithColumns` for `ArithmeticStark` rows where one of the arithmetic operations has been called.
+pub(crate) fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
     // We scale each filter flag with the associated opcode value.
     // If an arithmetic operation is happening on the CPU side,
     // the CTL will enforce that the reconstructed opcode value
@@ -102,6 +103,7 @@ pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
     )
 }
 
+/// Structure representing the `Arithmetic` STARK, which carries out all the arithmetic operations.
 #[derive(Copy, Clone, Default)]
 pub struct ArithmeticStark<F, const D: usize> {
     pub f: PhantomData<F>,
@@ -204,11 +206,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
         let range_max = P::Scalar::from_canonical_u64((RANGE_MAX - 1) as u64);
         yield_constr.constraint_last_row(rc1 - range_max);
 
+        // Evaluate constraints for the MUL operation.
         mul::eval_packed_generic(lv, yield_constr);
+        // Evaluate constraints for ADD, SUB, LT and GT operations.
         addcy::eval_packed_generic(lv, yield_constr);
+        // Evaluate constraints for DIV and MOD operations.
         divmod::eval_packed(lv, nv, yield_constr);
+        // Evaluate constraints for ADDMOD, SUBMOD, MULMOD and for FP254 modular operations.
         modular::eval_packed(lv, nv, yield_constr);
+        // Evaluate constraints for the BYTE operation.
         byte::eval_packed(lv, yield_constr);
+        // Evaluate constraints for SHL and SHR operations.
         shift::eval_packed_generic(lv, nv, yield_constr);
     }
 
@@ -223,6 +231,9 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
         let nv: &[ExtensionTarget<D>; NUM_ARITH_COLUMNS] =
             vars.get_next_values().try_into().unwrap();
 
+        // Check the range column: First value must be 0, last row
+        // must be 2^16-1, and intermediate rows must increment by 0
+        // or 1.
         let rc1 = lv[columns::RANGE_COUNTER];
         let rc2 = nv[columns::RANGE_COUNTER];
         yield_constr.constraint_first_row(builder, rc1);
@@ -234,11 +245,17 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for ArithmeticSta
         let t = builder.sub_extension(rc1, range_max);
         yield_constr.constraint_last_row(builder, t);
 
+        // Evaluate constraints for the MUL operation.
         mul::eval_ext_circuit(builder, lv, yield_constr);
+        // Evaluate constraints for ADD, SUB, LT and GT operations.
         addcy::eval_ext_circuit(builder, lv, yield_constr);
+        // Evaluate constraints for DIV and MOD operations.
         divmod::eval_ext_circuit(builder, lv, nv, yield_constr);
+        // Evaluate constraints for ADDMOD, SUBMOD, MULMOD and for FP254 modular operations.
         modular::eval_ext_circuit(builder, lv, nv, yield_constr);
+        // Evaluate constraints for the BYTE operation.
         byte::eval_ext_circuit(builder, lv, yield_constr);
+        // Evaluate constraints for SHL and SHR operations.
         shift::eval_ext_circuit(builder, lv, nv, yield_constr);
     }
 

diff --git a/evm/src/arithmetic/byte.rs b/evm/src/arithmetic/byte.rs
@@ -197,7 +197,7 @@ pub(crate) fn generate<F: PrimeField64>(lv: &mut [F], idx: U256, val: U256) {
     );
 }
 
-pub fn eval_packed<P: PackedField>(
+pub(crate) fn eval_packed<P: PackedField>(
     lv: &[P; NUM_ARITH_COLUMNS],
     yield_constr: &mut ConstraintConsumer<P>,
 ) {
@@ -293,7 +293,7 @@ pub fn eval_packed<P: PackedField>(
     }
 }
 
-pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
+pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     lv: &[ExtensionTarget<D>; NUM_ARITH_COLUMNS],
     yield_constr: &mut RecursiveConstraintConsumer<F, D>,
@@ -306,6 +306,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     let idx_decomp = &lv[AUX_INPUT_REGISTER_0];
     let tree = &lv[AUX_INPUT_REGISTER_1];
 
+    // low 5 bits of the first limb of idx:
     let mut idx0_lo5 = builder.zero_extension();
     for i in 0..5 {
         let bit = idx_decomp[i];
@@ -316,13 +317,19 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
         let scale = builder.constant_extension(scale);
         idx0_lo5 = builder.mul_add_extension(bit, scale, idx0_lo5);
     }
+    // Verify that idx0_hi is the high (11) bits of the first limb of
+    // idx (in particular idx0_hi is at most 11 bits, since idx[0] is
+    // at most 16 bits).
     let t = F::Extension::from(F::from_canonical_u64(32));
     let t = builder.constant_extension(t);
     let t = builder.mul_add_extension(idx_decomp[5], t, idx0_lo5);
     let t = builder.sub_extension(idx[0], t);
     let t = builder.mul_extension(is_byte, t);
     yield_constr.constraint(builder, t);
 
+    // Verify the layers of the tree
+    // NB: Each of the bit values is negated in place to account for
+    // the reversed indexing.
     let one = builder.one_extension();
     let bit = idx_decomp[4];
     for i in 0..8 {
@@ -362,6 +369,8 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     let t = builder.mul_extension(is_byte, t);
     yield_constr.constraint(builder, t);
 
+    // Check byte decomposition of last limb:
+
     let base8 = F::Extension::from(F::from_canonical_u64(1 << 8));
     let base8 = builder.constant_extension(base8);
     let lo_byte = lv[BYTE_LAST_LIMB_LO];
@@ -380,19 +389,29 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     yield_constr.constraint(builder, t);
     let expected_out_byte = tree[15];
 
+    // Sum all higher limbs; sum will be non-zero iff idx >= 32.
     let mut hi_limb_sum = lv[BYTE_IDX_DECOMP_HI];
     for i in 1..N_LIMBS {
         hi_limb_sum = builder.add_extension(hi_limb_sum, idx[i]);
     }
+    // idx_is_large is 0 or 1
     let idx_is_large = lv[BYTE_IDX_IS_LARGE];
     let t = builder.mul_sub_extension(idx_is_large, idx_is_large, idx_is_large);
     let t = builder.mul_extension(is_byte, t);
     yield_constr.constraint(builder, t);
 
+    // If hi_limb_sum is nonzero, then idx_is_large must be one.
     let t = builder.sub_extension(idx_is_large, one);
     let t = builder.mul_many_extension([is_byte, hi_limb_sum, t]);
     yield_constr.constraint(builder, t);
 
+    // If idx_is_large is 1, then hi_limb_sum_inv must be the inverse
+    // of hi_limb_sum, hence hi_limb_sum is non-zero, hence idx is
+    // indeed "large".
+    //
+    // Otherwise, if idx_is_large is 0, then hi_limb_sum * hi_limb_sum_inv
+    // is zero, which is only possible if hi_limb_sum is zero, since
+    // hi_limb_sum_inv is non-zero.
     let base16 = F::from_canonical_u64(1 << 16);
     let hi_limb_sum_inv = builder.mul_const_add_extension(
         base16,
@@ -414,6 +433,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     let t = builder.mul_extension(is_byte, check);
     yield_constr.constraint(builder, t);
 
+    // Check that the rest of the output limbs are zero
     for i in 1..N_LIMBS {
         let t = builder.mul_extension(is_byte, out[i]);
         yield_constr.constraint(builder, t);

diff --git a/evm/src/arithmetic/columns.rs b/evm/src/arithmetic/columns.rs
@@ -109,4 +109,5 @@ pub(crate) const RANGE_COUNTER: usize = START_SHARED_COLS + NUM_SHARED_COLS;
 /// The frequencies column used in logUp.
 pub(crate) const RC_FREQUENCIES: usize = RANGE_COUNTER + 1;
 
+/// Number of columns in `ArithmeticStark`.
 pub const NUM_ARITH_COLUMNS: usize = START_SHARED_COLS + NUM_SHARED_COLS + 2;
diff --git a/evm/src/arithmetic/divmod.rs b/evm/src/arithmetic/divmod.rs
@@ -1,3 +1,7 @@
+//! Support for EVM instructions DIV and MOD.
+//!
+//! The logic for verifying them is detailed in the `modular` submodule.
+
 use std::ops::Range;
 
 use ethereum_types::U256;