SequenceInstructionTable and SequenceExecutionConfig (#1259)

* rebase to upstream Signed-off-by: noelwei <[email protected]> * wip of addrtable Signed-off-by: noelwei <[email protected]> * all gates Signed-off-by: noelwei <[email protected]> * change the lookup purpose Signed-off-by: noelwei <[email protected]> * fix according to reviews * purge unused seqvaluetable Signed-off-by: noelwei <[email protected]> * change zero testing to corresponding gadget complete assignment Signed-off-by: noelwei <[email protected]> * trivial fixing Signed-off-by: noelwei <[email protected]> * purge the duplicated works Signed-off-by: noelwei <[email protected]> * unit test (WIP) Signed-off-by: noelwei <[email protected]> * seq exec circuit (WIP) Signed-off-by: noelwei <[email protected]> * seq exec circuit (WIP) Signed-off-by: noelwei <[email protected]> * seq exec circuit (WIP) Signed-off-by: noelwei <[email protected]> * output region: gates and lookups (WIP) Signed-off-by: noelwei <[email protected]> * pass unittest for seqinst table Signed-off-by: noelwei <[email protected]> * seq exec: complete the seq num lookup Signed-off-by: noelwei <[email protected]> * add seq exec info in witgen Signed-off-by: noelwei <[email protected]> * assign and unit tests (WIP) Signed-off-by: noelwei <[email protected]> * refactor for better assignment Signed-off-by: noelwei <[email protected]> * assignments and unit tests (WIP) Signed-off-by: noelwei <[email protected]> * induce debug utilities in AddressRow Signed-off-by: noelwei <[email protected]> * pass first unit test (WIP) Signed-off-by: noelwei <[email protected]> * chore: integrate seq-inst-table and seq-exec-config into decoder-config * refactor to low degree Signed-off-by: noelwei <[email protected]> * more unittest for seq exec (WIP) Signed-off-by: noelwei <[email protected]> * pass unit tests Signed-off-by: noelwei <[email protected]> * add assign entry Signed-off-by: noelwei <[email protected]> * update some witgens, pass decoder's unit test Signed-off-by: noelwei <[email protected]> * integrate seq exec into decoder (WIP) Signed-off-by: noelwei <[email protected]> * temporary disable 3 lookups and unit test pass for the rest Signed-off-by: noelwei <[email protected]> * all of the unit test passed Signed-off-by: noelwei <[email protected]> * trivial updates: head condition in seq exec and exported cells Signed-off-by: noelwei <[email protected]> * clear the warnings Signed-off-by: noelwei <[email protected]> * chore: fmt --------- Signed-off-by: noelwei <[email protected]> Co-authored-by: Rohit Narurkar <[email protected]>
scroll-tech · May 14, 2024 · 7895743 · 7895743
1 parent 284acfe
commit 7895743
Show file tree

Hide file tree

Showing 8 changed files with 2,649 additions and 130 deletions.
diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs
@@ -1,3 +1,4 @@
+mod seq_exec;
 mod tables;
 pub mod witgen;
 use witgen::*;
@@ -28,16 +29,23 @@ use zkevm_circuits::{
 };
 
 use self::{
-    tables::{BitstringTable, FixedTable, FseTable, LiteralsHeaderTable},
+    tables::{
+        BitstringTable, FixedTable, FseTable, LiteralsHeaderTable,
+        SeqInstTable as SequenceInstructionTable,
+    },
     util::value_bits_le,
     witgen::{
         FseTableKind, ZstdTag, N_BITS_PER_BYTE, N_BITS_REPEAT_FLAG, N_BITS_ZSTD_TAG,
         N_BLOCK_HEADER_BYTES,
     },
 };
 
+use seq_exec::{LiteralTable, SeqExecConfig as SequenceExecutionConfig, SequenceConfig};
+
 #[derive(Clone, Debug)]
 pub struct DecoderConfig {
+    /// TODO(check): const col.
+    const_col: Column<Fixed>,
     /// Fixed column to mark all the usable rows.
     q_enable: Column<Fixed>,
     /// Fixed column to mark the first row in the layout.
@@ -82,10 +90,11 @@ pub struct DecoderConfig {
     fse_table: FseTable,
 
     // witgen_debug
-    // /// Helper table for sequences as instructions.
-    // /// TODO(enable): sequence_instruction_table: SequenceInstructionTable,
+    /// Helper table for sequences as instructions.
+    sequence_instruction_table: SequenceInstructionTable<Fr>,
     // /// Helper table in the "output" region for accumulating the result of executing sequences.
-    // /// TODO(enable): sequence_execution_table: SequenceExecutionTable,
+    sequence_execution_config: SequenceExecutionConfig<Fr>,
+
     /// Fixed lookups table.
     fixed_table: FixedTable,
 }
@@ -972,7 +981,9 @@ impl DecoderConfig {
             pow2_table,
             bitwise_op_table,
         );
-        // TODO(enable): let sequence_instruction_table = SequenceInstructionTable::configure(meta);
+        let sequence_instruction_table = SequenceInstructionTable::configure(meta);
+
+        debug_assert!(meta.degree() <= 9);
 
         // Peripheral configs
         let tag_config = TagConfig::configure(meta, q_enable);
@@ -982,24 +993,34 @@ impl DecoderConfig {
         let bitstream_decoder = BitstreamDecoder::configure(meta, q_enable, q_first, u8_table);
         let fse_decoder = FseDecoder::configure(meta, q_enable);
         let sequences_data_decoder = SequencesDataDecoder::configure(meta);
+        let sequence_execution_config = SequenceExecutionConfig::configure(
+            meta,
+            challenges,
+            &LiteralTable::construct([
+                q_enable.into(),
+                tag_config.tag.into(),
+                block_config.block_idx.into(),
+                tag_config.tag_idx.into(),
+                byte.into(),
+                tag_config.is_change.into(),
+                is_padding.into(),
+            ]),
+            &sequence_instruction_table,
+            &SequenceConfig::construct([
+                q_enable.into(),
+                block_config.is_block.into(),
+                block_config.block_idx.into(),
+                block_config.num_sequences.into(),
+            ]),
+        );
 
-        // TODO(enable):
-        // let literals_table = [
-        //     tag_config.tag,
-        //     block_config.block_idx,
-        //     byte_idx,
-        //     byte,
-        //     is_padding,
-        // ];
-        // let sequence_execution_table = SequenceExecutionTable::configure(
-        //     meta,
-        //     challenges,
-        //     &literals_table,
-        //     &sequence_instruction_table,
-        // );
+        debug_assert!(meta.degree() <= 9);
 
         // Main config
+        let const_col = meta.fixed_column();
+        meta.enable_constant(const_col);
         let config = Self {
+            const_col,
             q_enable,
             q_first,
             byte_idx,
@@ -1025,8 +1046,8 @@ impl DecoderConfig {
             bitstring_table,
             fse_table,
 
-            // TODO(enable): sequence_instruction_table,
-            // TODO(enable): sequence_execution_table,
+            sequence_instruction_table,
+            sequence_execution_config,
             fixed_table,
         };
 
@@ -2009,30 +2030,30 @@ impl DecoderConfig {
             cb.gate(condition)
         });
 
-        // TODO: lookup(SeqInstTable) for seq_count_lookup
-        // meta.lookup_any(
-        //     "DecoderConfig: tag ZstdBlockSequenceHeader (sequence count)",
-        //     |meta| {
-        //         let condition = and::expr([
-        //             is_zb_sequence_header(meta),
-        //             meta.query_advice(config.tag_config.is_change, Rotation::cur()),
-        //         ]);
-        //         let (block_idx, num_sequences) = (
-        //             meta.query_advice(config.block_config.block_idx, Rotation::cur()),
-        //             meta.query_advice(config.block_config.num_sequences, Rotation::cur()),
-        //         );
-        //         [
-        //             1.expr(), // q_enabled
-        //             block_idx,
-        //             1.expr(), // s_beginning
-        //             num_sequences,
-        //         ]
-        //         .into_iter()
-        //         .zip_eq(config.sequence_instruction_table.seq_count_exprs(meta))
-        //         .map(|(arg, table)| (condition.expr() * arg, table))
-        //         .collect()
-        //     },
-        // );
+        meta.lookup_any(
+            "DecoderConfig: tag ZstdBlockSequenceHeader (sequence count)",
+            |meta| {
+                let condition = and::expr([
+                    meta.query_fixed(config.q_enable, Rotation::cur()),
+                    is_zb_sequence_header(meta),
+                    meta.query_advice(config.tag_config.is_change, Rotation::cur()),
+                ]);
+                let (block_idx, num_sequences) = (
+                    meta.query_advice(config.block_config.block_idx, Rotation::cur()),
+                    meta.query_advice(config.block_config.num_sequences, Rotation::cur()),
+                );
+                [
+                    1.expr(), // q_enabled
+                    block_idx,
+                    1.expr(), // s_beginning
+                    num_sequences,
+                ]
+                .into_iter()
+                .zip_eq(config.sequence_instruction_table.seq_count_exprs(meta))
+                .map(|(arg, table)| (condition.expr() * arg, table))
+                .collect()
+            },
+        );
 
         debug_assert!(meta.degree() <= 9);
 
@@ -3178,44 +3199,45 @@ impl DecoderConfig {
             },
         );
 
-        // TODO(enable): lookup(SeqInstTable) at code-to-value for seq_values_lookup
-        // meta.lookup_any(
-        //     "DecoderConfig: tag ZstdBlockSequenceData (sequence instructions table)",
-        //     |meta| {
-        //         // At the row where we compute the code-to-value of LLT, we have the values for
-        //         // all of match offset, match length and literal length.
-        //         let condition = and::expr([
-        //             meta.query_advice(config.tag_config.is_sequence_data, Rotation::cur()),
-        //             config.bitstream_decoder.is_not_nil(meta, Rotation::cur()),
-        //             config.fse_decoder.is_llt(meta, Rotation::cur()),
-        //             config
-        //                 .sequences_data_decoder
-        //                 .is_code_to_value(meta, Rotation::cur()),
-        //         ]);
-        //         let (block_idx, sequence_idx) = (
-        //             meta.query_advice(config.block_config.block_idx, Rotation::cur()),
-        //             meta.query_advice(config.sequences_data_decoder.idx, Rotation::cur()),
-        //         );
-        //         let (literal_length_value, match_offset_value, match_length_value) = (
-        //             meta.query_advice(config.sequences_data_decoder.values[0], Rotation::cur()),
-        //             meta.query_advice(config.sequences_data_decoder.values[2], Rotation::cur()),
-        //             meta.query_advice(config.sequences_data_decoder.values[1], Rotation::cur()),
-        //         );
-        //         [
-        //             1.expr(), // q_enabled
-        //             block_idx,
-        //             0.expr(), // s_beginning
-        //             sequence_idx,
-        //             literal_length_value,
-        //             match_offset_value,
-        //             match_length_value,
-        //         ]
-        //         .into_iter()
-        //         .zip_eq(config.sequence_instruction_table.seq_values_exprs(meta))
-        //         .map(|(arg, table)| (condition.expr() * arg, table))
-        //         .collect()
-        //     },
-        // );
+        meta.lookup_any(
+            "DecoderConfig: tag ZstdBlockSequenceData (sequence instructions table)",
+            |meta| {
+                // At the row where we compute the code-to-value of LLT, we have the values for
+                // all of match offset, match length and literal length.
+                let condition = and::expr([
+                    meta.query_fixed(config.q_enable, Rotation::cur()),
+                    meta.query_advice(config.tag_config.is_sequence_data, Rotation::cur()),
+                    not::expr(meta.query_advice(config.tag_config.is_change, Rotation::cur())),
+                    config.bitstream_decoder.is_not_nil(meta, Rotation::cur()),
+                    config.fse_decoder.is_llt(meta, Rotation::cur()),
+                    config
+                        .sequences_data_decoder
+                        .is_code_to_value(meta, Rotation::cur()),
+                ]);
+                let (block_idx, sequence_idx) = (
+                    meta.query_advice(config.block_config.block_idx, Rotation::cur()),
+                    meta.query_advice(config.sequences_data_decoder.idx, Rotation::cur()),
+                );
+                let (literal_length_value, match_offset_value, match_length_value) = (
+                    meta.query_advice(config.sequences_data_decoder.values[0], Rotation::cur()),
+                    meta.query_advice(config.sequences_data_decoder.values[2], Rotation::cur()),
+                    meta.query_advice(config.sequences_data_decoder.values[1], Rotation::cur()),
+                );
+                [
+                    1.expr(), // q_enabled
+                    block_idx,
+                    0.expr(), // s_beginning
+                    sequence_idx,
+                    literal_length_value,
+                    match_offset_value,
+                    match_length_value,
+                ]
+                .into_iter()
+                .zip_eq(config.sequence_instruction_table.seq_values_exprs(meta))
+                .map(|(arg, table)| (condition.expr() * arg, table))
+                .collect()
+            },
+        );
 
         meta.lookup_any(
             "DecoderConfig: tag ZstdBlockSequenceData (FseTable)",
@@ -4062,11 +4084,16 @@ impl DecoderConfig {
     pub fn assign<F: Field>(
         &self,
         layouter: &mut impl Layouter<Fr>,
+        raw_bytes: &[u8],
+        compressed_bytes: &[u8],
         witness_rows: Vec<ZstdWitnessRow<Fr>>,
+        literal_datas: Vec<Vec<u64>>,
         _aux_data: Vec<u64>,
         fse_aux_tables: Vec<FseAuxiliaryTableData>,
         block_info_arr: Vec<BlockInfo>,
         sequence_info_arr: Vec<SequenceInfo>,
+        address_table_arr: Vec<Vec<AddressTableRow>>,
+        sequence_exec_info_arr: Vec<Vec<SequenceExec>>,
         challenges: &Challenges<Value<Fr>>,
         k: u32,
         // witgen_debug
@@ -4077,6 +4104,11 @@ impl DecoderConfig {
         assert!(block_info_arr.len() > 0, "Must have at least 1 block");
         assert!(sequence_info_arr.len() > 0, "Must have at least 1 block");
 
+        assert!(address_table_arr.len() == 1, "TODO: multi-block");
+        assert!(sequence_exec_info_arr.len() == 1, "TODO: multi-block");
+        //let address_table_rows = &address_table_arr[0];
+        let sequence_exec_info = &sequence_exec_info_arr[0];
+
         let mut curr_block_info = block_info_arr[0];
         let mut curr_sequence_info = sequence_info_arr[0];
 
@@ -4142,10 +4174,30 @@ impl DecoderConfig {
                 ),
             ));
         }
-
         self.literals_header_table
             .assign(layouter, literal_headers)?;
 
+        /////////////////////////////////////////
+        //// Assign Sequence-related Configs ////
+        /////////////////////////////////////////
+        self.sequence_instruction_table.assign(
+            layouter,
+            address_table_arr.iter().map(|rows| rows.iter()),
+            (1 << k) - self.unusable_rows(),
+        )?;
+        // TODO: use equality constraint for the exported_len and exported_rlc cell
+        let (_exported_len, _exported_rlc) = self.sequence_execution_config.assign(
+            layouter,
+            challenges,
+            literal_datas
+                .iter()
+                .zip(&sequence_info_arr)
+                .zip(&sequence_exec_info_arr)
+                .map(|((lit, seq_info), exec)| (lit.as_slice(), seq_info, exec.as_slice())),
+            raw_bytes,
+            (1 << k) - self.unusable_rows(),
+        )?;
+
         /////////////////////////////////////////
         ///// Assign Decompression Region  //////
         /////////////////////////////////////////
@@ -4334,7 +4386,6 @@ impl DecoderConfig {
                         i,
                         || Value::known(Fr::from(row.state.tag_idx as u64)),
                     )?;
-
                     let is_sequence_data = row.state.tag == ZstdTag::ZstdBlockSequenceData;
                     region.assign_advice(
                         || "tag_config.is_sequence_data",
@@ -4764,6 +4815,7 @@ mod tests {
 
     #[derive(Clone, Debug, Default)]
     struct DecoderConfigTester {
+        raw: Vec<u8>,
         compressed: Vec<u8>,
         k: u32,
     }
@@ -4826,23 +4878,44 @@ mod tests {
 
             let (
                 witness_rows,
-                _decoded_literals,
+                decoded_literals,
                 aux_data,
                 fse_aux_tables,
                 block_info_arr,
                 sequence_info_arr,
+                address_table_arr,
+                sequence_exec_result,
             ) = process(&self.compressed, challenges.keccak_input());
 
+            let (recovered_bytes, sequence_exec_info_arr) = sequence_exec_result.into_iter().fold(
+                (Vec::new(), Vec::new()),
+                |(mut out_byte, mut out_exec), res| {
+                    out_byte.extend(res.recovered_bytes);
+                    out_exec.push(res.exec_trace);
+                    (out_byte, out_exec)
+                },
+            );
+
+            assert_eq!(
+                std::str::from_utf8(&recovered_bytes),
+                std::str::from_utf8(&self.raw),
+            );
+
             u8_table.load(&mut layouter)?;
             bitwise_op_table.load(&mut layouter)?;
             pow_rand_table.assign(&mut layouter, &challenges, 1 << (self.k - 1))?;
             config.assign::<Fr>(
                 &mut layouter,
+                &self.raw,
+                &self.compressed,
                 witness_rows,
+                decoded_literals,
                 aux_data,
                 fse_aux_tables,
                 block_info_arr,
                 sequence_info_arr,
+                address_table_arr,
+                sequence_exec_info_arr,
                 &challenges,
                 self.k,
             )?;
@@ -4893,7 +4966,7 @@ mod tests {
         };
 
         let k = 18;
-        let decoder_config_tester = DecoderConfigTester { compressed, k };
+        let decoder_config_tester = DecoderConfigTester { raw, compressed, k };
         let mock_prover = MockProver::<Fr>::run(k, &decoder_config_tester, vec![]).unwrap();
         mock_prover.assert_satisfied_par();
     }