Implement constraints in state circuit spec (scroll-tech#462)

* Refactor StateCircuit + add lexicographic ordering constraints

* Implement first_access method and fix stack change constraint

* Cleanup and comment out failing constraint

* Fix failing tests by correctly getting limbs in be order in lexicographic ordering

* fix clippy

* Rename test files for clippy

* Cleanup benchmarks

* fix build

* Assign diff_inverse correctly

* Fix instance function and convert it to a method

* Fix storage_key_be_limbs method

* Add degree test

* Have StateCircuit use Vec<Rw> instead of RwMap

* Compute first_access correctly

* wip, but tests pass

* Fix diff_2 assignment

* cleanup

* Use verify_at_rows to speed up tests and derive EnumIter

* Add cleanup and explain diff_1 and diff_2

* cleanup

* fmt

* Add newline to fix cargo fmt

* Fix degree test and TxLog table assignment

* Cleanup and change index type to u8 from usize

* Rename to diff_1->upper_limb_difference and diff_2->lower_limb_difference

* Explain assignment in comments

* fix conflicts

* lint

* fix rebase

* fix build and tests from rebase

* make change to rerun tests

Co-authored-by: z2trillion <[email protected]>
Co-authored-by: Zhang Zhuo <[email protected]>

circuit-benchmarks/build.rs

@@ -10,23 +10,9 @@ fn main() {
         .unwrap_or_else(|_| "11".to_string())
         .parse()
         .expect("Cannot parse DEGREE env var as usize");
-    let memory_address_max: usize = var("MEMORY_ADDRESS_MAX")
-        .unwrap_or_else(|_| "2000".to_string())
-        .parse()
-        .expect("Cannot parse MEMORY_ADDRESS_MAX env var as usize");
-    let stack_address_max: usize = var("STACK_ADDRESS_MAX")
-        .unwrap_or_else(|_| "1300".to_string())
-        .parse()
-        .expect("Cannot parse STACK_ADDRESS_MAX env var as usize");
 
     // Add state_circuit module to `lib.rs`
-    let consts = format!(
-        "pub(crate) const DEGREE: usize = {};
-pub(crate) const MEMORY_ADDRESS_MAX: usize = {};
-pub(crate) const STACK_ADDRESS_MAX: usize = {};
-",
-        degree, memory_address_max, stack_address_max
-    );
+    let consts = format!("pub(crate) const DEGREE: usize = {};\n", degree);
 
     let mut state_file =
         File::create("src/bench_params.rs").expect("Error generating bench_params.rs file");

circuit-benchmarks/src/state_circuit.rs

@@ -2,7 +2,7 @@
 
 #[cfg(test)]
 mod tests {
-    use crate::bench_params::{DEGREE, MEMORY_ADDRESS_MAX, STACK_ADDRESS_MAX};
+    use crate::bench_params::DEGREE;
     use ark_std::{end_timer, start_timer};
     use halo2_proofs::plonk::{create_proof, keygen_pk, keygen_vk, verify_proof, SingleVerifier};
     use halo2_proofs::{
@@ -14,20 +14,10 @@ mod tests {
     use rand_xorshift::XorShiftRng;
     use zkevm_circuits::state_circuit::StateCircuit;
 
-    const RW_COUNTER_MAX: usize = 1 << DEGREE;
-    const ROWS_MAX: usize = 1 << DEGREE;
-
     #[cfg_attr(not(feature = "benches"), ignore)]
     #[test]
     fn bench_state_circuit_prover() {
-        let empty_circuit = StateCircuit::<
-            Fr,
-            true,
-            RW_COUNTER_MAX,
-            MEMORY_ADDRESS_MAX,
-            STACK_ADDRESS_MAX,
-            ROWS_MAX,
-        >::default();
+        let empty_circuit = StateCircuit::<Fr>::default();
 
         // Initialize the polynomial commitment parameters
         let rng = XorShiftRng::from_seed([

integration-tests/tests/circuits.rs

@@ -41,30 +41,21 @@ async fn test_state_circuit_block(block_num: u64) {
     let storage_ops = builder.block.container.sorted_storage();
     trace!("storage_ops: {:#?}", storage_ops);
 
-    const DEGREE: usize = 16;
-    const MEMORY_ADDRESS_MAX: usize = 2000;
-    const STACK_ADDRESS_MAX: usize = 1024;
-
-    const RW_COUNTER_MAX: usize = 1 << DEGREE;
-    const ROWS_MAX: usize = 1 << DEGREE;
+    const DEGREE: usize = 17;
 
     let rw_map = RwMap::from(&OperationContainer {
         memory: memory_ops,
         stack: stack_ops,
         storage: storage_ops,
         ..Default::default()
     });
-    let circuit = StateCircuit::<
-        Fr,
-        true,
-        RW_COUNTER_MAX,
-        MEMORY_ADDRESS_MAX,
-        STACK_ADDRESS_MAX,
-        ROWS_MAX,
-    >::new(Fr::rand(), &rw_map);
+
+    let randomness = Fr::rand();
+    let circuit = StateCircuit::<Fr>::new(randomness, rw_map);
+    let power_of_randomness = circuit.instance();
 
     use halo2_proofs::pairing::bn256::Fr as Fp;
-    let prover = MockProver::<Fp>::run(DEGREE as u32, &circuit, vec![]).unwrap();
+    let prover = MockProver::<Fp>::run(DEGREE as u32, &circuit, power_of_randomness).unwrap();
     prover.verify().expect("state_circuit verification failed");
 }
 

prover/Cargo.toml

@@ -15,5 +15,6 @@ log = "0.4.14"
 rand = "0.8.4"
 serde = { version = "1.0.136", features = ["derive"] }
 serde_json = "1.0.78"
+strum = "0.24"
 tokio = { version = "1.16.1", features = ["macros", "rt-multi-thread"] }
 zkevm-circuits = { path = "../zkevm-circuits", features = ["test"] }

prover/src/compute_proof.rs

@@ -10,6 +10,7 @@ use halo2_proofs::{
 use rand::SeedableRng;
 use rand_xorshift::XorShiftRng;
 use std::str::FromStr;
+use strum::IntoEnumIterator;
 use zkevm_circuits::evm_circuit::{
     table::FixedTableTag, test::TestCircuit, witness::block_convert,
 };
@@ -37,7 +38,7 @@ pub async fn compute_proof(
     let block = block_convert(&builder.block, &builder.code_db);
     {
         // generate evm_circuit proof
-        let circuit = TestCircuit::<Fr>::new(block.clone(), FixedTableTag::iterator().collect());
+        let circuit = TestCircuit::<Fr>::new(block.clone(), FixedTableTag::iter().collect());
 
         // TODO: can this be pre-generated to a file?
         // related
@@ -60,23 +61,7 @@ pub async fn compute_proof(
 
     {
         // generate state_circuit proof
-        //
-        // TODO: this should be configurable
-        const MEMORY_ADDRESS_MAX: usize = 2000;
-        const STACK_ADDRESS_MAX: usize = 1300;
-        const MEMORY_ROWS_MAX: usize = 16384;
-        const STACK_ROWS_MAX: usize = 16384;
-        const STORAGE_ROWS_MAX: usize = 16384;
-        const GLOBAL_COUNTER_MAX: usize = MEMORY_ROWS_MAX + STACK_ROWS_MAX + STORAGE_ROWS_MAX;
-
-        let circuit = StateCircuit::<
-            Fr,
-            true,
-            GLOBAL_COUNTER_MAX,
-            MEMORY_ADDRESS_MAX,
-            STACK_ADDRESS_MAX,
-            GLOBAL_COUNTER_MAX,
-        >::new(block.randomness, &block.rws);
+        let circuit = StateCircuit::new(block.randomness, block.rws);
 
         // TODO: same quest like in the first scope
         let vk = keygen_vk(params, &circuit)?;

zkevm-circuits/Cargo.toml

@@ -20,6 +20,8 @@ eth-types = { path = "../eth-types" }
 gadgets = { path = "../gadgets" }
 ethers-core = "0.6"
 serde_json = "1.0.66"
+strum = "0.24"
+strum_macros = "0.24"
 rand_xorshift = "0.3"
 rand = "0.8"
 itertools = "0.10.3"

zkevm-circuits/src/evm_circuit.rs

@@ -141,7 +141,6 @@ impl<F: Field> EvmCircuit<F> {
 
 #[cfg(any(feature = "test", test))]
 pub mod test {
-
     use crate::{
         evm_circuit::{
             table::FixedTableTag,
@@ -165,6 +164,7 @@ pub mod test {
         distributions::uniform::{SampleRange, SampleUniform},
         random, thread_rng, Rng,
     };
+    use strum::IntoEnumIterator;
 
     pub(crate) fn rand_range<T, R>(range: R) -> T
     where
@@ -500,6 +500,6 @@ pub mod test {
     pub fn run_test_circuit_complete_fixed_table<F: Field>(
         block: Block<F>,
     ) -> Result<(), Vec<VerifyFailure>> {
-        run_test_circuit(block, FixedTableTag::iterator().collect())
+        run_test_circuit(block, FixedTableTag::iter().collect())
     }
 }

zkevm-circuits/src/evm_circuit/execution/copy_to_log.rs

@@ -261,7 +261,7 @@ pub mod test {
                         tx_id,
                         log_id,
                         field_tag: TxLogFieldTag::Data,
-                        index: idx,
+                        index: idx.try_into().unwrap(),
                         value: Word::from(byte),
                     });
                     rw_offset += 1;

zkevm-circuits/src/evm_circuit/execution/end_tx.rs

@@ -22,6 +22,7 @@ use crate::{
 };
 use eth_types::{evm_types::MAX_REFUND_QUOTIENT_OF_GAS_USED, Field, ToScalar};
 use halo2_proofs::plonk::Error;
+use strum::EnumCount;
 
 #[derive(Clone, Debug)]
 pub(crate) struct EndTxGadget<F> {
@@ -255,7 +256,7 @@ impl<F: Field> ExecutionGadget<F> for EndTxGadget<F> {
         } else {
             let rw = &block.rws[(
                 RwTableTag::TxReceipt,
-                (tx.id - 1) * TxReceiptFieldTag::amount() - 1,
+                (tx.id - 1) * TxReceiptFieldTag::COUNT - 1,
             )];
             rw.receipt_value()
         };

zkevm-circuits/src/evm_circuit/execution/logs.rs

@@ -382,7 +382,7 @@ mod test {
                     tx_id,
                     log_id: log_id.try_into().unwrap(),
                     field_tag: TxLogFieldTag::Topic,
-                    index: idx,
+                    index: idx.try_into().unwrap(),
                     value: *topic,
                 });
             }