diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 45113ad20a..d3d825a144 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -1,5 +1,5 @@ -mod tables; mod seq_exec; +mod tables; pub mod witgen; use witgen::*; @@ -29,7 +29,10 @@ use zkevm_circuits::{ }; use self::{ - tables::{BitstringTable, FixedTable, FseTable, LiteralsHeaderTable, SeqInstTable as SequenceInstructionTable}, + 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, @@ -37,7 +40,7 @@ use self::{ }, }; -use seq_exec::{LiteralTable, SequenceConfig, SeqExecConfig as SequenceExecutionConfig}; +use seq_exec::{LiteralTable, SeqExecConfig as SequenceExecutionConfig, SequenceConfig}; #[derive(Clone, Debug)] pub struct DecoderConfig { @@ -959,9 +962,6 @@ impl DecoderConfig { // Fixed table let fixed_table = FixedTable::construct(meta); - // // TODO (enable later): - // let sequence_instruction_table = SeqInstTable::configure(meta); - let (q_enable, q_first, byte_idx, byte, is_padding) = ( meta.fixed_column(), meta.fixed_column(), @@ -993,7 +993,6 @@ 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, @@ -4183,29 +4182,22 @@ impl DecoderConfig { ///////////////////////////////////////// self.sequence_instruction_table.assign( layouter, - address_table_arr.iter().map( - |rows|rows.iter() - ), + address_table_arr.iter().map(|rows| rows.iter()), (1 << k) - self.unusable_rows(), )?; - // let literal_bytes = witness_rows.iter().filter(|row| row.state.tag == ZstdTag::ZstdBlockLiteralsRawBytes).map(|row| row.encoded_data.value_byte).collect::>(); // 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(), - )), + 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 ////// ///////////////////////////////////////// @@ -4895,17 +4887,17 @@ mod tests { 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|{ + 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(&recovered_bytes), std::str::from_utf8(&self.raw), ); diff --git a/aggregator/src/aggregation/decoder/seq_exec.rs b/aggregator/src/aggregation/decoder/seq_exec.rs index 56d18e513f..66edc56c4e 100644 --- a/aggregator/src/aggregation/decoder/seq_exec.rs +++ b/aggregator/src/aggregation/decoder/seq_exec.rs @@ -1,52 +1,57 @@ - +use super::tables; +use crate::aggregation::decoder::witgen; use eth_types::Field; use gadgets::util::{and, not, select, Expr}; use halo2_proofs::{ - circuit::{Value, Region, Layouter, AssignedCell}, - plonk::{Advice, Any, Column, ConstraintSystem, VirtualCells, Error, Expression, Fixed, SecondPhase}, + circuit::{AssignedCell, Layouter, Region, Value}, + plonk::{ + Advice, Any, Column, ConstraintSystem, Error, Expression, Fixed, SecondPhase, VirtualCells, + }, poly::Rotation, }; use itertools::Itertools; +use tables::SeqInstTable; +use witgen::{SequenceExec, SequenceExecInfo, SequenceInfo, ZstdTag}; use zkevm_circuits::{ - evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, + evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, util::Challenges, }; -use crate::aggregation::decoder::witgen; -use witgen::{ZstdTag, SequenceInfo, SequenceExec, SequenceExecInfo}; -use super::tables; -use tables::SeqInstTable; /// TODO: This is in fact part of the `BlockConfig` in -/// Decoder, we can use BlockConfig if it is decoupled +/// Decoder, we can use BlockConfig if it is decoupled /// from Decoder module later -#[derive(Clone)] +#[derive(Clone)] pub struct SequenceConfig { // the enabled flag - q_enabled: Column, + q_enabled: Column, // the `is_block` flag in `BlockConfig` flag: Column, // the index of block which the literal section is in block_index: Column, // Number of sequences decoded from the sequences section header in the block. - num_sequences: Column, + num_sequences: Column, } impl SequenceConfig { - #[cfg(test)] pub fn mock_assign( &self, layouter: &mut impl Layouter, - seq_cfg: &SequenceInfo, - ) -> Result<(), Error>{ - - layouter.assign_region(||"seq cfg mock", - |mut region|{ + seq_cfg: &SequenceInfo, + ) -> Result<(), Error> { + layouter.assign_region( + || "seq cfg mock", + |mut region| { let mut offset = 0usize; - for col in [self.flag, self.block_index, self.num_sequences]{ - region.assign_advice(||"flush for non lookup", col, offset, ||Value::known(F::zero()))?; + for col in [self.flag, self.block_index, self.num_sequences] { + region.assign_advice( + || "flush for non lookup", + col, + offset, + || Value::known(F::zero()), + )?; } offset += 1; @@ -54,17 +59,27 @@ impl SequenceConfig { (self.flag, F::one()), (self.block_index, F::from(seq_cfg.block_idx as u64)), (self.num_sequences, F::from(seq_cfg.num_sequences as u64)), - ]{ - region.assign_advice(||"flush mock table", col, offset, ||Value::known(val))?; + ] { + region.assign_advice( + || "flush mock table", + col, + offset, + || Value::known(val), + )?; } - region.assign_fixed(||"enable mock table", self.q_enabled, offset, ||Value::known(F::one()))?; + region.assign_fixed( + || "enable mock table", + self.q_enabled, + offset, + || Value::known(F::one()), + )?; Ok(()) - } + }, ) } /// construct table for rows: [enabled, blk_index, num_seq] - pub fn construct(cols: [Column;4]) -> Self { + pub fn construct(cols: [Column; 4]) -> Self { Self { q_enabled: cols[0].try_into().unwrap(), flag: cols[1].try_into().unwrap(), @@ -74,15 +89,12 @@ impl SequenceConfig { } /// export the exps for literal copying lookup: [tag, blk_ind, byte_ind, char, padding] - pub fn lookup_tbl( - &self, - meta: &mut VirtualCells<'_, F> - ) -> [Expression; 4]{ + pub fn lookup_tbl(&self, meta: &mut VirtualCells<'_, F>) -> [Expression; 4] { [ meta.query_fixed(self.q_enabled, Rotation::cur()), meta.query_advice(self.flag, Rotation::cur()), - meta.query_advice(self.block_index, Rotation::cur()), - meta.query_advice(self.num_sequences, Rotation::cur()), + meta.query_advice(self.block_index, Rotation::cur()), + meta.query_advice(self.num_sequences, Rotation::cur()), ] } } @@ -108,52 +120,93 @@ pub struct LiteralTable { } impl LiteralTable { - #[cfg(test)] pub fn mock_assign( &self, layouter: &mut impl Layouter, - literals: &[u64], - ) -> Result<(), Error>{ - - layouter.assign_region(||"literal tbl mock", - |mut region|{ + literals: &[u64], + ) -> Result<(), Error> { + layouter.assign_region( + || "literal tbl mock", + |mut region| { let mut offset = 0usize; - for col in [self.tag, self.block_index, self.byte_index, self.char, self.last_flag, self.padding_flag]{ - region.assign_advice(||"flush for non lookup", col, offset, ||Value::known(F::zero()))?; + for col in [ + self.tag, + self.block_index, + self.byte_index, + self.char, + self.last_flag, + self.padding_flag, + ] { + region.assign_advice( + || "flush for non lookup", + col, + offset, + || Value::known(F::zero()), + )?; } offset += 1; // TODO: ensure the index in literal table is 0 or 1 indexed for (i, char) in literals.iter().copied().enumerate() { - region.assign_fixed(||"enable mock table", self.q_enabled, offset, ||Value::known(F::one()))?; + region.assign_fixed( + || "enable mock table", + self.q_enabled, + offset, + || Value::known(F::one()), + )?; for (col, val) in [ (self.tag, F::from(ZstdTag::ZstdBlockLiteralsRawBytes as u64)), (self.block_index, F::one()), - (self.byte_index, F::from(i as u64 +1)), + (self.byte_index, F::from(i as u64 + 1)), (self.char, F::from(char)), (self.last_flag, F::zero()), (self.padding_flag, F::zero()), - ]{ - region.assign_advice(||"flush mock table", col, offset, ||Value::known(val))?; + ] { + region.assign_advice( + || "flush mock table", + col, + offset, + || Value::known(val), + )?; } offset += 1; } - for col in [self.byte_index, self.char, self.padding_flag]{ - region.assign_advice(||"flush dummy row for border", col, offset, ||Value::known(F::zero()))?; + for col in [self.byte_index, self.char, self.padding_flag] { + region.assign_advice( + || "flush dummy row for border", + col, + offset, + || Value::known(F::zero()), + )?; } - region.assign_advice(||"set dummy border", self.tag, offset, ||Value::known(F::from(ZstdTag::ZstdBlockLiteralsRawBytes as u64)))?; - region.assign_advice(||"set dummy border", self.block_index, offset, ||Value::known(F::from(2 as u64)))?; - region.assign_advice(||"set dummy border", self.last_flag, offset, ||Value::known(F::one()))?; + region.assign_advice( + || "set dummy border", + self.tag, + offset, + || Value::known(F::from(ZstdTag::ZstdBlockLiteralsRawBytes as u64)), + )?; + region.assign_advice( + || "set dummy border", + self.block_index, + offset, + || Value::known(F::from(2 as u64)), + )?; + region.assign_advice( + || "set dummy border", + self.last_flag, + offset, + || Value::known(F::one()), + )?; Ok(()) - } + }, ) } /// construct table for rows: [q_enable, tag, blk_index, byte_index, char, last, padding] - pub fn construct(cols: [Column;7]) -> Self { + pub fn construct(cols: [Column; 7]) -> Self { Self { q_enabled: cols[0].try_into().unwrap(), tag: cols[1].try_into().unwrap(), @@ -168,32 +221,32 @@ impl LiteralTable { /// export the exps for literal copying lookup: [tag, blk_ind, byte_ind, char, padding] pub fn lookup_tbl_for_lit_cp( &self, - meta: &mut VirtualCells<'_, F> - ) -> [Expression; 6]{ + meta: &mut VirtualCells<'_, F>, + ) -> [Expression; 6] { [ meta.query_fixed(self.q_enabled, Rotation::cur()), meta.query_advice(self.tag, Rotation::cur()), - meta.query_advice(self.block_index, Rotation::cur()), - meta.query_advice(self.byte_index, Rotation::cur()), - meta.query_advice(self.char, Rotation::cur()), - meta.query_advice(self.padding_flag, Rotation::cur()), + meta.query_advice(self.block_index, Rotation::cur()), + meta.query_advice(self.byte_index, Rotation::cur()), + meta.query_advice(self.char, Rotation::cur()), + meta.query_advice(self.padding_flag, Rotation::cur()), ] } /// export the exps for literal size lookup: [tag, blk_ind, byte_ind, flag, padding] pub fn lookup_tbl_for_lit_size( &self, - meta: &mut VirtualCells<'_, F> - ) -> [Expression; 6]{ + meta: &mut VirtualCells<'_, F>, + ) -> [Expression; 6] { [ meta.query_fixed(self.q_enabled, Rotation::cur()), meta.query_advice(self.tag, Rotation::cur()), - meta.query_advice(self.block_index, Rotation::cur()), - meta.query_advice(self.byte_index, Rotation::cur()), + meta.query_advice(self.block_index, Rotation::cur()), + meta.query_advice(self.byte_index, Rotation::cur()), meta.query_advice(self.last_flag, Rotation::next()), - meta.query_advice(self.padding_flag, Rotation::cur()), + meta.query_advice(self.padding_flag, Rotation::cur()), ] - } + } } /// SeqExecConfig handling the sequences in each block and output the @@ -205,7 +258,7 @@ pub struct SeqExecConfig { // 1-index for each block, keep the same for each row // until all sequenced has been handled block_index: Column, - // the 1-indexed seq number (1..=n_seq) for each + // the 1-indexed seq number (1..=n_seq) for each // sequence. seq_index: Column, // the decoded length of output byte so it is start @@ -218,7 +271,7 @@ pub struct SeqExecConfig { /// An incremental accumulator of the number of bytes decoded so far. // decoded_len_acc: Column, - // the flag indicate current seq is the special one + // the flag indicate current seq is the special one // (copying the rest bytes in literal section) s_last_lit_cp_phase: Column, // the flag indicate the execution is under @@ -227,10 +280,10 @@ pub struct SeqExecConfig { // the flag indicate the execution is under // back reference phase s_back_ref_phase: Column, - // the copied index in literal section + // the copied index in literal section literal_pos: Column, - // the back-ref pos - backref_offset: Column, + // the back-ref pos + backref_offset: Column, // counting the progress of back ref bytes backref_progress: Column, _marker: std::marker::PhantomData, @@ -239,7 +292,6 @@ pub struct SeqExecConfig { type ExportedCell = AssignedCell; impl SeqExecConfig { - /// Construct the sequence instruction table /// the maxium rotation is prev(2), next(1) pub fn configure( @@ -269,47 +321,45 @@ impl SeqExecConfig { // need to export the final rlc and len meta.enable_equality(decoded_rlc); // the flag indicate current row is the beginning of - // a new block + // a new block meta.enable_equality(decoded_len); // the flag indicate the execution has ended and rows // are filled by padding data let mut is_inst_begin = 0.expr(); - // the flag exp indicate current row is the beginning + // the flag exp indicate current row is the beginning // of a new instruction, it is also the beginning of - // a literal copying + // a literal copying let mut is_block_begin = 0.expr(); let mut is_padding = 0.expr(); - meta.create_gate("borders", |meta|{ + meta.create_gate("borders", |meta| { let mut cb = BaseConstraintBuilder::default(); // boolean constraint that index is increment cb.require_boolean("instruction border is boolean", is_inst_begin.expr()); is_block_begin = meta.query_advice(block_index, Rotation::cur()) - - meta.query_advice(block_index, Rotation::prev()); - + - meta.query_advice(block_index, Rotation::prev()); + cb.require_boolean("block border is boolean", is_block_begin.expr()); is_inst_begin = select::expr( is_block_begin.expr(), 1.expr(), meta.query_advice(seq_index, Rotation::cur()) - - meta.query_advice(seq_index, Rotation::prev()), + - meta.query_advice(seq_index, Rotation::prev()), ); cb.require_boolean("inst border is boolean", is_inst_begin.expr()); - cb.gate( - meta.query_fixed(q_enabled, Rotation::cur()) - ) + cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); debug_assert!(meta.degree() <= 9); - meta.create_gate("phases", |meta|{ + meta.create_gate("phases", |meta| { let mut cb = BaseConstraintBuilder::default(); let s_lit_cp_phase_next = meta.query_advice(s_lit_cp_phase, Rotation::next()); @@ -327,97 +377,111 @@ impl SeqExecConfig { // i.e. two phases can not be enabled at the same time cb.require_boolean("padding is boolean", is_padding.expr()); - cb.condition(and::expr([ + cb.condition( + and::expr([ not::expr(is_inst_begin.expr()), not::expr(s_lit_cp_phase_prev.expr()), ]), - |cb|{ - cb.require_equal("inside a inst, cp phase keep 0 once it changed to 0", + |cb| { + cb.require_equal( + "inside a inst, cp phase keep 0 once it changed to 0", s_lit_cp_phase.expr(), 0.expr(), - ); - }); + ); + }, + ); - cb.condition(and::expr([ - not::expr(is_inst_begin.expr()), - s_back_ref_phase_prev.expr(), - ]), - |cb|{ - cb.require_equal("inside a inst, backref phase keep 1 once it changed to 1", + cb.condition( + and::expr([ + not::expr(is_inst_begin.expr()), s_back_ref_phase_prev.expr(), - 1.expr(), - ); - }); + ]), + |cb| { + cb.require_equal( + "inside a inst, backref phase keep 1 once it changed to 1", + s_back_ref_phase_prev.expr(), + 1.expr(), + ); + }, + ); - let is_padding_next = 1.expr() - s_lit_cp_phase_next.expr() - s_back_ref_phase_next.expr(); - cb.condition(is_padding.expr(), |cb|{ - cb.require_equal("padding never change once actived", - is_padding_next.expr(), + let is_padding_next = + 1.expr() - s_lit_cp_phase_next.expr() - s_back_ref_phase_next.expr(); + cb.condition(is_padding.expr(), |cb| { + cb.require_equal( + "padding never change once actived", + is_padding_next.expr(), is_padding.expr(), ); }); - cb.gate( - meta.query_fixed(q_enabled, Rotation::cur()) - ) + cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); debug_assert!(meta.degree() <= 9); - meta.create_gate("last literal cp phase", |meta|{ + meta.create_gate("last literal cp phase", |meta| { let mut cb = BaseConstraintBuilder::default(); let s_last_lit_cp_phase_prev = meta.query_advice(s_last_lit_cp_phase, Rotation::prev()); let s_last_lit_cp_phase = meta.query_advice(s_last_lit_cp_phase, Rotation::cur()); cb.require_boolean("last lit_cp phase is boolean", s_last_lit_cp_phase.expr()); - cb.condition(and::expr([ - s_last_lit_cp_phase.expr(), - not::expr(s_last_lit_cp_phase_prev.expr()), - ]), |cb|{ - cb.require_equal("phase can only be actived in inst border", - is_inst_begin.expr(), - 1.expr(), - ); - }); + cb.condition( + and::expr([ + s_last_lit_cp_phase.expr(), + not::expr(s_last_lit_cp_phase_prev.expr()), + ]), + |cb| { + cb.require_equal( + "phase can only be actived in inst border", + is_inst_begin.expr(), + 1.expr(), + ); + }, + ); - cb.condition(and::expr([ - s_last_lit_cp_phase_prev.expr(), - not::expr(is_block_begin.expr()), - ]), |cb|{ - cb.require_equal("phase must keep actived until block end", + cb.condition( + and::expr([ s_last_lit_cp_phase_prev.expr(), - s_last_lit_cp_phase.expr(), - ); - }); + not::expr(is_block_begin.expr()), + ]), + |cb| { + cb.require_equal( + "phase must keep actived until block end", + s_last_lit_cp_phase_prev.expr(), + s_last_lit_cp_phase.expr(), + ); + }, + ); - cb.condition(s_last_lit_cp_phase.expr(), |cb|{ - cb.require_equal("lit cp must actived if last lit cp is actived", - meta.query_advice(s_lit_cp_phase, Rotation::cur()), + cb.condition(s_last_lit_cp_phase.expr(), |cb| { + cb.require_equal( + "lit cp must actived if last lit cp is actived", + meta.query_advice(s_lit_cp_phase, Rotation::cur()), 1.expr(), ); }); - cb.gate( - meta.query_fixed(q_enabled, Rotation::cur()) - ) + cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); debug_assert!(meta.degree() <= 9); - meta.create_gate("phase pos", |meta|{ + meta.create_gate("phase pos", |meta| { let mut cb = BaseConstraintBuilder::default(); let literal_pos_prev = meta.query_advice(literal_pos, Rotation::prev()); let literal_pos = meta.query_advice(literal_pos, Rotation::cur()); let s_lit_cp_phase = meta.query_advice(s_lit_cp_phase, Rotation::cur()); - cb.require_equal("lit cp is increment in one block", + cb.require_equal( + "lit cp is increment in one block", select::expr( is_block_begin.expr(), // so we start at 1 if first row is lit cp // or 0 if not s_lit_cp_phase.expr(), literal_pos_prev.expr() + s_lit_cp_phase.expr(), - ), + ), literal_pos.expr(), ); @@ -426,36 +490,35 @@ impl SeqExecConfig { let s_back_ref_phase = meta.query_advice(s_back_ref_phase, Rotation::cur()); - cb.require_equal("backref progress is increment in one inst", + cb.require_equal( + "backref progress is increment in one inst", select::expr( is_inst_begin.expr(), // so we start at 1 if first row is lit cp // or 0 if not s_back_ref_phase.expr(), backref_progress_prev.expr() + s_back_ref_phase.expr(), - ), + ), backref_progress.expr(), ); let backref_offset_prev = meta.query_advice(backref_offset, Rotation::prev()); let backref_offset = meta.query_advice(backref_offset, Rotation::cur()); - cb.condition( - not::expr(is_inst_begin.expr()), - |cb|cb.require_equal("backref offset kee the same in one inst", - backref_offset.expr(), + cb.condition(not::expr(is_inst_begin.expr()), |cb| { + cb.require_equal( + "backref offset kee the same in one inst", + backref_offset.expr(), backref_offset_prev.expr(), ) - ); + }); - cb.gate( - meta.query_fixed(q_enabled, Rotation::cur()) - ) + cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); debug_assert!(meta.degree() <= 9); - meta.create_gate("output and paddings", |meta|{ + meta.create_gate("output and paddings", |meta| { let mut cb = BaseConstraintBuilder::default(); let decoded_len_prev = meta.query_advice(decoded_len, Rotation::prev()); @@ -465,7 +528,7 @@ impl SeqExecConfig { let decoded_byte = meta.query_advice(decoded_byte, Rotation::cur()); cb.require_equal( - "decoded len increase 1 in next row until paddings", + "decoded len increase 1 in next row until paddings", select::expr( is_padding.expr(), decoded_len_prev.expr(), @@ -473,60 +536,58 @@ impl SeqExecConfig { ), decoded_len.expr(), ); - cb.condition( - is_padding.expr(), - |cb|cb.require_zero( - "while padding, byte is always zero", - decoded_byte.expr(), - ), - ); + cb.condition(is_padding.expr(), |cb| { + cb.require_zero("while padding, byte is always zero", decoded_byte.expr()) + }); - cb.require_equal("rlc accumulate", - decoded_rlc_prev.expr() * - select::expr( - decoded_len.expr() - decoded_len_prev.expr(), - challenges.evm_word(), - 1.expr(), - ) - + decoded_byte.expr(), + cb.require_equal( + "rlc accumulate", + decoded_rlc_prev.expr() + * select::expr( + decoded_len.expr() - decoded_len_prev.expr(), + challenges.evm_word(), + 1.expr(), + ) + + decoded_byte.expr(), decoded_rlc.expr(), ); cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); - meta.lookup_any("the instruction from inst table", |meta|{ - + meta.lookup_any("the instruction from inst table", |meta| { let q_enabled = meta.query_fixed(q_enabled, Rotation::prev()); let block_index = meta.query_advice(block_index, Rotation::prev()); let seq_index = meta.query_advice(seq_index, Rotation::prev()); - let not_last_lit_cp = not::expr(meta.query_advice(s_last_lit_cp_phase, Rotation::prev())); + let not_last_lit_cp = + not::expr(meta.query_advice(s_last_lit_cp_phase, Rotation::prev())); let literal_pos_at_inst_end = meta.query_advice(literal_pos, Rotation::prev()); let backref_offset_at_inst_end = meta.query_advice(backref_offset, Rotation::prev()); let backref_len_at_inst_end = meta.query_advice(backref_progress, Rotation::prev()); - inst_table.instructions().into_iter().zip( - [ + inst_table + .instructions() + .into_iter() + .zip([ block_index, seq_index, backref_offset_at_inst_end, literal_pos_at_inst_end, - backref_len_at_inst_end - ] - ).map(|(lookup_col, src_expr)|{ - let lookup_expr = meta.query_advice(lookup_col, Rotation::cur()); - let src_expr = src_expr - * is_inst_begin.expr() - * not_last_lit_cp.expr() - * q_enabled.expr(); - assert!(src_expr.degree() <= 5); - (src_expr, lookup_expr) - }).collect() + backref_len_at_inst_end, + ]) + .map(|(lookup_col, src_expr)| { + let lookup_expr = meta.query_advice(lookup_col, Rotation::cur()); + let src_expr = + src_expr * is_inst_begin.expr() * not_last_lit_cp.expr() * q_enabled.expr(); + assert!(src_expr.degree() <= 5); + (src_expr, lookup_expr) + }) + .collect() }); debug_assert!(meta.degree() <= 9); - meta.lookup_any("lit cp char", |meta|{ + meta.lookup_any("lit cp char", |meta| { let enabled = meta.query_fixed(q_enabled, Rotation::cur()) * meta.query_advice(s_lit_cp_phase, Rotation::cur()); @@ -535,22 +596,22 @@ impl SeqExecConfig { let cp_byte = meta.query_advice(decoded_byte, Rotation::cur()); let tbl_exprs = literal_table.lookup_tbl_for_lit_cp(meta); - tbl_exprs.into_iter().zip_eq( - [ + tbl_exprs + .into_iter() + .zip_eq([ 1.expr(), ZstdTag::ZstdBlockLiteralsRawBytes.expr(), block_index, literal_pos, cp_byte, - 0.expr(), - ] - ).map(|(lookup_expr, src_expr)|{ - (src_expr * enabled.expr(), lookup_expr) - }).collect() + 0.expr(), + ]) + .map(|(lookup_expr, src_expr)| (src_expr * enabled.expr(), lookup_expr)) + .collect() }); debug_assert!(meta.degree() <= 9); - meta.lookup_any("back ref char", |meta|{ + meta.lookup_any("back ref char", |meta| { let enabled = meta.query_fixed(q_enabled, Rotation::cur()); let backref_pos = meta.query_advice(backref_offset, Rotation::cur()); @@ -558,69 +619,69 @@ impl SeqExecConfig { let decode_pos = meta.query_advice(decoded_len, Rotation::cur()); let ref_pos = decode_pos.expr() - backref_pos.expr(); - let tbl_exprs = [ - enabled.expr(), - decode_pos.expr(), - cp_byte.expr(), - ]; - tbl_exprs.into_iter().zip( - [ - 1.expr(), - ref_pos, - cp_byte, - ] - ).map(|(lookup_expr, src_expr)|{( - src_expr - * enabled.expr() - * meta.query_advice(s_back_ref_phase, Rotation::cur()), - lookup_expr, - ) - }).collect() + let tbl_exprs = [enabled.expr(), decode_pos.expr(), cp_byte.expr()]; + tbl_exprs + .into_iter() + .zip([1.expr(), ref_pos, cp_byte]) + .map(|(lookup_expr, src_expr)| { + ( + src_expr + * enabled.expr() + * meta.query_advice(s_back_ref_phase, Rotation::cur()), + lookup_expr, + ) + }) + .collect() }); debug_assert!(meta.degree() <= 9); - meta.lookup_any("actual literal byte", |meta|{ + meta.lookup_any("actual literal byte", |meta| { let q_enabled = meta.query_fixed(q_enabled, Rotation::prev()); let block_index = meta.query_advice(block_index, Rotation::prev()); let literal_pos_at_block_end = meta.query_advice(literal_pos, Rotation::prev()); let tbl_exprs = literal_table.lookup_tbl_for_lit_size(meta); - tbl_exprs.into_iter().zip_eq( - [ + tbl_exprs + .into_iter() + .zip_eq([ 1.expr(), ZstdTag::ZstdBlockLiteralsRawBytes.expr(), block_index, literal_pos_at_block_end, 1.expr(), 0.expr(), - ] - ).map(|(lookup_expr, src_expr)|{ - (src_expr * is_block_begin.expr() * q_enabled.expr(), lookup_expr) - }).collect() + ]) + .map(|(lookup_expr, src_expr)| { + ( + src_expr * is_block_begin.expr() * q_enabled.expr(), + lookup_expr, + ) + }) + .collect() }); debug_assert!(meta.degree() <= 9); - meta.lookup_any("instruction counts", |meta|{ + meta.lookup_any("instruction counts", |meta| { let q_enabled = meta.query_fixed(q_enabled, Rotation::prev()); let block_index = meta.query_advice(block_index, Rotation::prev()); - let seq_index_at_block_end = - meta.query_advice(seq_index, Rotation::prev()) + let seq_index_at_block_end = meta.query_advice(seq_index, Rotation::prev()) // if we have a additional literal copying phase, we // in fact has one extra instruction - meta.query_advice(s_last_lit_cp_phase, Rotation::prev()); - seq_config.lookup_tbl(meta).into_iter().zip_eq( - [ - 1.expr(), - 1.expr(), - block_index, - seq_index_at_block_end, - ] - ).map(|(lookup_expr, src_expr)|{ - (src_expr * is_block_begin.expr() * q_enabled.expr(), lookup_expr) - }).collect() + seq_config + .lookup_tbl(meta) + .into_iter() + .zip_eq([1.expr(), 1.expr(), block_index, seq_index_at_block_end]) + .map(|(lookup_expr, src_expr)| { + ( + src_expr * is_block_begin.expr() * q_enabled.expr(), + lookup_expr, + ) + }) + .collect() }); - + debug_assert!(meta.degree() <= 9); Self { q_enabled, @@ -642,22 +703,21 @@ impl SeqExecConfig { /// fill the rest region with padding rows pub fn paddings<'a>( &self, - region: &mut Region, + region: &mut Region, offset: usize, till_offset: usize, decoded_len: usize, decoded_rlc: Value, padded_block_ind: u64, - ) -> Result<(ExportedCell, ExportedCell), Error>{ - + ) -> Result<(ExportedCell, ExportedCell), Error> { for offset in offset..=till_offset { // flush one more row for rotation next() if offset != till_offset { region.assign_fixed( - ||"enable padding row", - self.q_enabled, - offset, - ||Value::known(F::one()) + || "enable padding row", + self.q_enabled, + offset, + || Value::known(F::one()), )?; } @@ -665,12 +725,8 @@ impl SeqExecConfig { (self.block_index, Value::known(F::from(padded_block_ind))), (self.decoded_len, Value::known(F::from(decoded_len as u64))), (self.decoded_rlc, decoded_rlc), - ]{ - region.assign_advice(||"set padding rows", - col, - offset, - ||val, - )?; + ] { + region.assign_advice(|| "set padding rows", col, offset, || val)?; } for col in [ @@ -683,28 +739,30 @@ impl SeqExecConfig { self.literal_pos, self.seq_index, ] { - region.assign_advice(||"flush padding rows", - col, + region.assign_advice( + || "flush padding rows", + col, offset, - ||Value::known(F::zero()), + || Value::known(F::zero()), )?; } } - let len_export = region.assign_advice(||"export len", - self.decoded_len, + let len_export = region.assign_advice( + || "export len", + self.decoded_len, till_offset, - ||Value::known(F::from(decoded_len as u64)), + || Value::known(F::from(decoded_len as u64)), )?; - let rlc_export = region.assign_advice(||"export rlc", - self.decoded_rlc, + let rlc_export = region.assign_advice( + || "export rlc", + self.decoded_rlc, till_offset, - ||decoded_rlc, + || decoded_rlc, )?; Ok((len_export, rlc_export)) - } /// assign a single block from current offset / byte decompression @@ -717,19 +775,17 @@ impl SeqExecConfig { mut decoded_len: usize, mut decoded_rlc: Value, seq_info: &SequenceInfo, - seq_exec_infos: impl Iterator, + seq_exec_infos: impl Iterator, literals: &[u64], // all of the decompressed bytes, not only current block decompressed_bytes: &[u8], - ) -> Result<(usize, usize, Value), Error>{ - + ) -> Result<(usize, usize, Value), Error> { let block_ind = seq_info.block_idx; let mut cur_literal_cp = 0usize; let mut inst_begin_offset = offset; - let mut cur_inst : Option = None; + let mut cur_inst: Option = None; for SequenceExec(inst_ind, exec_info) in seq_exec_infos { - let inst_ind = *inst_ind + 1; if let Some(old_ind) = cur_inst.replace(inst_ind) { if old_ind != inst_ind { @@ -741,10 +797,10 @@ impl SeqExecConfig { (self.block_index, F::from(block_ind as u64)), (self.seq_index, F::from(inst_ind as u64)), ( - self.s_last_lit_cp_phase, - if inst_ind > seq_info.num_sequences { + self.s_last_lit_cp_phase, + if inst_ind > seq_info.num_sequences { F::one() - }else { + } else { F::zero() }, ), @@ -755,30 +811,30 @@ impl SeqExecConfig { assert_eq!(cur_literal_cp, r.start); cur_literal_cp = r.end; (true, r.clone()) - }, + } SequenceExecInfo::BackRef(r) => (false, r.clone()), }; for (i, pos) in r.clone().enumerate() { - decoded_len += 1; - let out_byte = F::from( - if is_literal { - literals[pos as usize] - } else { - decompressed_bytes[pos as usize] as u64 - } - ); + decoded_len += 1; + let out_byte = F::from(if is_literal { + literals[pos as usize] + } else { + decompressed_bytes[pos as usize] as u64 + }); decoded_rlc = decoded_rlc * chng + Value::known(out_byte); - //println!("set row at {}, output {}:{:x}", offset, decoded_len, out_byte.get_lower_32()); + //println!("set row at {}, output {}:{:x}", offset, decoded_len, + // out_byte.get_lower_32()); region.assign_advice( - ||"set output region", - self.decoded_rlc, offset, - ||decoded_rlc, + || "set output region", + self.decoded_rlc, + offset, + || decoded_rlc, )?; - // all of the "pos" is 1-index for lookup since the + // all of the "pos" is 1-index for lookup since the // bytes_output is 1-indexed let pos = pos + 1; let ref_offset = if is_literal { @@ -788,38 +844,34 @@ impl SeqExecConfig { }; // for back-ref part, we refill the backref_pos in the whole // instruction - if !is_literal && i == 0{ - //println!("fill-back match offset {} in {}..{}", ref_offset.unwrap(), inst_begin_offset, offset); + if !is_literal && i == 0 { + //println!("fill-back match offset {} in {}..{}", ref_offset.unwrap(), + // inst_begin_offset, offset); for back_offset in inst_begin_offset..offset { region.assign_advice( - ||"set output region", - self.backref_offset, back_offset, - ||Value::known(F::from(ref_offset.expect("backref set") as u64)), - )?; + || "set output region", + self.backref_offset, + back_offset, + || Value::known(F::from(ref_offset.expect("backref set") as u64)), + )?; } } let decodes = [ - ( - self.decoded_len, - F::from(decoded_len as u64), - - ), - ( - self.decoded_byte, - out_byte, - ), + (self.decoded_len, F::from(decoded_len as u64)), + (self.decoded_byte, out_byte), ( self.backref_offset, F::from(ref_offset.unwrap_or_default() as u64), ), ]; - for (col, val) in base_rows.clone() - .into_iter() - .chain(decodes) - .chain( - if is_literal { + for (col, val) in + base_rows + .clone() + .into_iter() + .chain(decodes) + .chain(if is_literal { //println!("inst {}: literal cp {}-{}", inst_ind, pos, 0); [ (self.s_lit_cp_phase, F::one()), @@ -835,21 +887,21 @@ impl SeqExecConfig { (self.literal_pos, F::from(cur_literal_cp as u64)), (self.backref_progress, F::from(i as u64 + 1)), ] - } - ){ - region.assign_advice( - ||"set output region", - col, offset, - ||Value::known(val), - )?; - - } + }) + { + region.assign_advice( + || "set output region", + col, + offset, + || Value::known(val), + )?; + } region.assign_fixed( - ||"enable row", - self.q_enabled, - offset, - ||Value::known(F::one()) + || "enable row", + self.q_enabled, + offset, + || Value::known(F::one()), )?; offset += 1; } @@ -858,14 +910,14 @@ impl SeqExecConfig { debug_assert_eq!(cur_literal_cp, literals.len()); Ok((offset, decoded_len, decoded_rlc)) - } + } - /// assign the top row + /// assign the top row pub fn init_top_row( &self, region: &mut Region, from_offset: Option, - ) -> Result{ + ) -> Result { let offset = from_offset.unwrap_or_default(); for col in [ @@ -881,7 +933,7 @@ impl SeqExecConfig { self.literal_pos, self.backref_progress, ] { - region.assign_advice(||"top row fluash", col, offset, ||Value::known(F::zero()))?; + region.assign_advice(|| "top row fluash", col, offset, || Value::known(F::zero()))?; } for (col, val) in [ @@ -889,43 +941,36 @@ impl SeqExecConfig { (self.decoded_rlc, F::zero()), (self.block_index, F::zero()), ] { - region.assign_advice_from_constant(||"top row constraint", - col, - offset, - val)?; + region.assign_advice_from_constant(|| "top row constraint", col, offset, val)?; } - region.assign_advice_from_constant(||"blk index begin constraint", + region.assign_advice_from_constant( + || "blk index begin constraint", self.block_index, - offset + 1, + offset + 1, F::one(), )?; - Ok(offset+1) + Ok(offset + 1) } - /// assign with multiple blocks and export the cell at - /// final row (specified by `eanbled_rows`) for + /// assign with multiple blocks and export the cell at + /// final row (specified by `eanbled_rows`) for /// (decoded_len, decoded_rlc) pub fn assign<'a>( &self, layouter: &mut impl Layouter, chng: &Challenges>, // per-block inputs: (literal, seq_info, seq_exec_trace) - per_blk_inputs: impl IntoIterator + Clone, + per_blk_inputs: impl IntoIterator + + Clone, // all of the decompressed bytes, not only current block decompressed_bytes: &[u8], enabled_rows: usize, - ) -> Result<(ExportedCell, ExportedCell), Error>{ - + ) -> Result<(ExportedCell, ExportedCell), Error> { layouter.assign_region( || "output region", - |mut region|{ - + |mut region| { let mut offset = self.init_top_row(&mut region, None)?; let mut decoded_len = 0usize; let mut decoded_rlc = Value::known(F::zero()); @@ -936,24 +981,25 @@ impl SeqExecConfig { &mut region, chng.evm_word(), offset, - decoded_len, - decoded_rlc, - seq_info, - exec_trace.iter(), + decoded_len, + decoded_rlc, + seq_info, + exec_trace.iter(), literals, - decompressed_bytes + decompressed_bytes, )?; } - self.paddings(&mut region, - offset, - enabled_rows, - decoded_len, - decoded_rlc, + self.paddings( + &mut region, + offset, + enabled_rows, + decoded_len, + decoded_rlc, blk_ind as u64 + 1, ) - } - ) + }, + ) } #[cfg(test)] @@ -967,56 +1013,54 @@ impl SeqExecConfig { // all of the decompressed bytes, not only current block decompressed_bytes: &[u8], enabled_rows: usize, - ) -> Result<(), Error>{ - - let literals = literals.iter().copied().map(|b|b as u64).collect::>(); + ) -> Result<(), Error> { + let literals = literals + .iter() + .copied() + .map(|b| b as u64) + .collect::>(); layouter.assign_region( || "output region", - |mut region|{ - + |mut region| { let offset = self.init_top_row(&mut region, None)?; let (offset, decoded_len, decoded_rlc) = self.assign_block( &mut region, chng.evm_word(), offset, - 0, - Value::known(F::zero()), + 0, + Value::known(F::zero()), &SequenceInfo { block_idx: 1, num_sequences: n_seq, ..Default::default() - }, - seq_exec_infos.iter(), + }, + seq_exec_infos.iter(), &literals, - decompressed_bytes + decompressed_bytes, )?; - self.paddings(&mut region, - offset, - enabled_rows, - decoded_len, - decoded_rlc, - 2 + self.paddings( + &mut region, + offset, + enabled_rows, + decoded_len, + decoded_rlc, + 2, )?; Ok(()) - } + }, ) } - } - #[cfg(test)] mod tests { + use super::*; use halo2_proofs::{ - circuit::SimpleFloorPlanner, - dev::MockProver, - halo2curves::bn256::Fr, - plonk::Circuit, + circuit::SimpleFloorPlanner, dev::MockProver, halo2curves::bn256::Fr, plonk::Circuit, }; - use super::*; use witgen::AddressTableRow; use zkevm_circuits::util::MockChallenges; @@ -1046,39 +1090,33 @@ mod tests { let new_literal_pos = current_literal_pos + (inst.literal_length as usize); if new_literal_pos > current_literal_pos { let r = current_literal_pos..new_literal_pos; - exec_trace.push( - SequenceExec( - inst.instruction_idx as usize, - SequenceExecInfo::LiteralCopy(r.clone()), - ) - ); + exec_trace.push(SequenceExec( + inst.instruction_idx as usize, + SequenceExecInfo::LiteralCopy(r.clone()), + )); outputs.extend_from_slice(&literals[r]); } - + let match_pos = outputs.len() - (inst.actual_offset as usize); if inst.match_length > 0 { let r = match_pos..(inst.match_length as usize + match_pos); - exec_trace.push( - SequenceExec( - inst.instruction_idx as usize, - SequenceExecInfo::BackRef(r.clone()), - ) - ); + exec_trace.push(SequenceExec( + inst.instruction_idx as usize, + SequenceExecInfo::BackRef(r.clone()), + )); let matched_bytes = Vec::from(&outputs[r]); outputs.extend(matched_bytes); } current_literal_pos = new_literal_pos; } - + // Add remaining literal bytes if current_literal_pos < literals.len() { let r = current_literal_pos..literals.len(); - exec_trace.push( - SequenceExec( - seq_conf.num_sequences, - SequenceExecInfo::LiteralCopy(r.clone()), - ) - ); + exec_trace.push(SequenceExec( + seq_conf.num_sequences, + SequenceExecInfo::LiteralCopy(r.clone()), + )); outputs.extend_from_slice(&literals[r]); } @@ -1107,32 +1145,27 @@ mod tests { fn without_witnesses(&self) -> Self { unimplemented!() } - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { let const_col = meta.fixed_column(); meta.enable_constant(const_col); - let literal_tbl = LiteralTable::construct( - [ - meta.fixed_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - ] - ); - - let seq_cfg = SequenceConfig::construct( - [ - meta.fixed_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - meta.advice_column().into(), - ] - ); + let literal_tbl = LiteralTable::construct([ + meta.fixed_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + ]); + + let seq_cfg = SequenceConfig::construct([ + meta.fixed_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + meta.advice_column().into(), + ]); let inst_tbl = SeqInstTable::configure(meta); @@ -1141,7 +1174,7 @@ mod tests { let config = SeqExecConfig::configure(meta, &chng, &literal_tbl, &inst_tbl, &seq_cfg); - Self::Config{ + Self::Config { config, literal_tbl, inst_tbl, @@ -1149,30 +1182,37 @@ mod tests { chng_mock, } } - + fn synthesize( &self, config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - - config.literal_tbl.mock_assign(&mut layouter, - self.literals.iter().copied() - .map(|b|b as u64).collect::>().as_slice())?; + config.literal_tbl.mock_assign( + &mut layouter, + self.literals + .iter() + .copied() + .map(|b| b as u64) + .collect::>() + .as_slice(), + )?; config.seq_cfg.mock_assign(&mut layouter, &self.seq_conf)?; - config.inst_tbl.mock_assign(&mut layouter, &self.insts, 15)?; + config + .inst_tbl + .mock_assign(&mut layouter, &self.insts, 15)?; let chng_val = config.chng_mock.values(&mut layouter); config.config.mock_assign( - &mut layouter, + &mut layouter, &chng_val, - self.insts.len(), - &self.exec_trace, - &self.literals, - &self.outputs, + self.insts.len(), + &self.exec_trace, + &self.literals, + &self.outputs, 50, )?; @@ -1181,61 +1221,51 @@ mod tests { } #[test] - fn seq_exec_literal_only(){ - + fn seq_exec_literal_only() { // no instructions, we only copy literals to output - let circuit = SeqExecMock::mock_generate( - Vec::from("abcd".as_bytes()), - Vec::new(), - ); + let circuit = SeqExecMock::mock_generate(Vec::from("abcd".as_bytes()), Vec::new()); assert_eq!(circuit.outputs, Vec::from("abcd".as_bytes())); let k = 12; - let mock_prover = MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); + let mock_prover = + MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); mock_prover.verify().unwrap(); - } #[test] - fn seq_exec_simple(){ - + fn seq_exec_simple() { // no instructions, we only copy literals to output let circuit = SeqExecMock::mock_generate( Vec::from("abcdef".as_bytes()), AddressTableRow::mock_samples_full([ - [1,4,1,1,4,8], - [9,1,3,6,1,4], - [3,0,4,5,6,1], + [1, 4, 1, 1, 4, 8], + [9, 1, 3, 6, 1, 4], + [3, 0, 4, 5, 6, 1], ]), ); assert_eq!(circuit.outputs, Vec::from("abcddeabcdeabf".as_bytes())); let k = 12; - let mock_prover = MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); + let mock_prover = + MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); mock_prover.verify().unwrap(); - } #[test] - fn seq_exec_no_tail_cp(){ - + fn seq_exec_no_tail_cp() { // no instructions, we only copy literals to output let circuit = SeqExecMock::mock_generate( Vec::from("abcde".as_bytes()), - AddressTableRow::mock_samples_full([ - [1,4,1,1,4,8], - [9,1,3,6,1,4], - ]), + AddressTableRow::mock_samples_full([[1, 4, 1, 1, 4, 8], [9, 1, 3, 6, 1, 4]]), ); assert_eq!(circuit.outputs, Vec::from("abcddeabc".as_bytes())); let k = 12; - let mock_prover = MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); + let mock_prover = + MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); mock_prover.verify().unwrap(); - } - } diff --git a/aggregator/src/aggregation/decoder/tables/seqinst_table.rs b/aggregator/src/aggregation/decoder/tables/seqinst_table.rs index 42497332fa..3bc01a78ee 100644 --- a/aggregator/src/aggregation/decoder/tables/seqinst_table.rs +++ b/aggregator/src/aggregation/decoder/tables/seqinst_table.rs @@ -1,4 +1,4 @@ - +use crate::aggregation::decoder::witgen; use eth_types::Field; use gadgets::{ is_equal::*, @@ -6,30 +6,29 @@ use gadgets::{ util::{and, not, select, Expr}, }; use halo2_proofs::{ - circuit::{Value, Region, Layouter}, - plonk::{Advice, Any, Column, ConstraintSystem, Error, Fixed, VirtualCells, Expression}, + circuit::{Layouter, Region, Value}, + plonk::{Advice, Any, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}, poly::Rotation, }; +use witgen::AddressTableRow; use zkevm_circuits::{ - evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, + evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, table::LookupTable, }; -use crate::aggregation::decoder::witgen; -use witgen::AddressTableRow; /// Table used carry the raw sequence instructions parsed from sequence section /// and would be later transformed as the back-reference instructions -/// -/// For every block, one row in the table represent a single sequence instruction +/// +/// For every block, one row in the table represent a single sequence instruction /// in the sequence section, and handle all data parsed from the same sequence. -/// The 'block_index' is a 1-index for each block with n sequences in its +/// The 'block_index' is a 1-index for each block with n sequences in its /// sequence section, the parsed value from bitstream for current sequence is put /// in the 'input cols' section (`literal_len`, `match_offset` and `match_len`) /// The transformed sequence instructions is put in 'output cols' section ( /// `acc_literal_len`, `offset` and `match_len`), /// notice we can use `match_len` without transformation. -/// -/// | enabled |block_index| n_seq |seq_index|s_beginning||| +/// +/// | enabled |block_index| n_seq |seq_index|s_beginning||| /// |---------|-----------|-------|---------|-----------|------------|-------------| /// | 1 | 1 | 30 | 0 | 1 | | | /// | 1 | 1 | 30 | 1 | 0 | (4,2,4) | (4,4,4) | @@ -45,15 +44,15 @@ use witgen::AddressTableRow; /// | ... | ... | ... | ... | ... | | | /// | 1 | 998 | 0 | 0 | 1 | | | /// | 1 | 999 | 0 | 0 | 1 | | | -/// +/// /// When all sequences from compressed data has been handled, the rest rows being enabled -/// (q_enabled is true) has to be padded with increased block index, with `n_seq` is 0 +/// (q_enabled is true) has to be padded with increased block index, with `n_seq` is 0 /// and `s_beginning` is true -/// +/// /// The transform from 'input cols' to 'output cols' according to zstd's spec /// include following steps: /// 1. accumulate the copied literal bytes in one section -/// 2. for match offset > 3, set the actual offset val is -=3, else we refer it +/// 2. for match offset > 3, set the actual offset val is -=3, else we refer it /// from the reference tables represented by 'repeated_offset_1/2/3' cols /// 3. After each sequence, the reference tables is updated according to the /// value of cooked offset and whether `literal_len` is zero @@ -65,11 +64,9 @@ use witgen::AddressTableRow; /// | 1 | 5 | 5 | 5 | 2 | 5 | 4 | 1 | 0 | /// | 0 | 2 | 5 | 1 | 1 | 1 | 5 | 4 | 0 | /// | | | | | | | | | 0 | -/// #[derive(Clone, Debug)] pub struct SeqInstTable { - // active flag, one active row parse q_enabled: Column, @@ -79,20 +76,20 @@ pub struct SeqInstTable { // the count of sequences in one block, keey the same // for each row when block index is not changed n_seq: Column, - // the 1-indexed seq number (1..=n_seq) for each + // the 1-indexed seq number (1..=n_seq) for each // sequence. We have extra row at the beginning of // each block with seq_index is 0 seq_index: Column, // the flag for the first row in each block (i.e. seq_index is 0) s_beginning: Column, - // the value directly decoded from bitstream, one row + // the value directly decoded from bitstream, one row // for one sequence literal_len: Column, match_offset: Column, match_len: Column, - // exported instructions for one sequence, + // exported instructions for one sequence, // note the match_len would be exported as-is // updated offset offset: Column, @@ -114,7 +111,6 @@ pub struct SeqInstTable { // 4: special case of offset = 3 (if lt_len == 0) ref_update_mode_4: Column, - // detect if literal_len is zero literal_is_zero: IsZeroConfig, // detect if seq_index in current row equal @@ -124,7 +120,7 @@ pub struct SeqInstTable { offset_is_1: IsEqualConfig, offset_is_2: IsEqualConfig, offset_is_3: IsEqualConfig, - + // detect if rep_offset_1 is 0 (indicate the data // is corrupt) ref_offset_1_is_zero: IsZeroConfig, @@ -155,7 +151,7 @@ impl LookupTable for SeqInstTable { String::from("match_offset"), String::from("match_len"), ] - } + } } #[derive(Clone, Debug)] @@ -170,7 +166,6 @@ struct ChipContext { impl ChipContext { fn construct(config: &SeqInstTable) -> Self { - let literal_is_zero_chip = IsZeroChip::construct(config.literal_is_zero.clone()); let ref_offset_1_is_zero_chip = IsZeroChip::construct(config.ref_offset_1_is_zero.clone()); let seq_index_chip = IsEqualChip::construct(config.seq_index_is_n_seq.clone()); @@ -186,19 +181,17 @@ impl ChipContext { offset_is_2_chip, offset_is_3_chip, } - } } impl SeqInstTable { - /// The sequence count should be lookuped by parsed bitstream, - /// used the block index and value for sequnce count tag to - /// lookup (`true`, `block_index`, 1, `value`) + /// used the block index and value for sequnce count tag to + /// lookup (`true`, `block_index`, 1, `value`) /// The table would be padded by increased block index to /// fill all rows being enabled - /// - /// | enabled |block_index| flag | n_seq | + /// + /// | enabled |block_index| flag | n_seq | /// |---------|-----------|-------|-------| /// | 1 | 1 | 1 | 30 | /// | 1 | ... | ... | 30 | @@ -207,7 +200,7 @@ impl SeqInstTable { /// | 1 | 3 | 1 | 4 | /// | ... | ... | ... | ... | /// | 1 | 999 | 1 | 0 | - pub fn seq_count_exprs(&self, meta: &mut VirtualCells) -> Vec>{ + pub fn seq_count_exprs(&self, meta: &mut VirtualCells) -> Vec> { vec![ meta.query_fixed(self.q_enabled, Rotation::cur()), meta.query_advice(self.block_index, Rotation::cur()), @@ -219,9 +212,9 @@ impl SeqInstTable { /// The sequence values should be lookuped by parsed bitstream, /// used the block index and value with each sequence tag for /// multiple lookup (`true`, `block_index`, 0, `seq_index`, `value`) on - /// corresponding value column (literal len, offset, match len) + /// corresponding value column (literal len, offset, match len) /// , or a lookup with suitable rotations - /// | enabled |block_index|s_beginning|seq_index| literal | offset | match | + /// | enabled |block_index|s_beginning|seq_index| literal | offset | match | /// |---------|-----------|-----------|---------|---------|--------|-------| /// | 1 | 1 | 0 | 1 | 4 | 2 | 4 | /// | 1 | 1 | 0 | 2 | 1 | 5 | 2 | @@ -230,7 +223,6 @@ impl SeqInstTable { /// | 1 | 1 | 0 | 30 | 1 | 50 | 11 | /// | 1 | 2 | 0 | 1 | 3 | 52 | 13 | /// | 1 | ... | 0 | ... | ... | ... | ... | - /// pub fn seq_values_exprs(&self, meta: &mut VirtualCells) -> Vec> { vec![ meta.query_fixed(self.q_enabled, Rotation::cur()), @@ -244,7 +236,7 @@ impl SeqInstTable { } /// Obtian the instruction table cols - pub fn instructions(&self) -> [Column;5]{ + pub fn instructions(&self) -> [Column; 5] { [ self.block_index, self.seq_index, @@ -256,9 +248,7 @@ impl SeqInstTable { /// Construct the sequence instruction table /// the maxium rotation is prev(1), next(1) - pub fn configure( - meta: &mut ConstraintSystem, - ) -> Self { + pub fn configure(meta: &mut ConstraintSystem) -> Self { let q_enabled = meta.fixed_column(); let block_index = meta.advice_column(); let n_seq = meta.advice_column(); @@ -277,73 +267,64 @@ impl SeqInstTable { let ref_update_mode_3 = meta.advice_column(); let ref_update_mode_4 = meta.advice_column(); - let [literal_is_zero, ref_offset_1_is_zero] = - [literal_len, rep_offset_1].map(|col|{ + let [literal_is_zero, ref_offset_1_is_zero] = [literal_len, rep_offset_1].map(|col| { let inv_col = meta.advice_column(); IsZeroChip::configure( - meta, - |meta|meta.query_fixed(q_enabled, Rotation::cur()), - |meta|meta.query_advice(col, Rotation::cur()), - inv_col + meta, + |meta| meta.query_fixed(q_enabled, Rotation::cur()), + |meta| meta.query_advice(col, Rotation::cur()), + inv_col, ) }); - let [offset_is_1, offset_is_2, offset_is_3] = - [1,2,3].map(|val|{ + let [offset_is_1, offset_is_2, offset_is_3] = [1, 2, 3].map(|val| { IsEqualChip::configure( - meta, - |meta|meta.query_fixed(q_enabled, Rotation::cur()), - |meta|meta.query_advice(match_offset, Rotation::cur()), - |_|val.expr() + meta, + |meta| meta.query_fixed(q_enabled, Rotation::cur()), + |meta| meta.query_advice(match_offset, Rotation::cur()), + |_| val.expr(), ) }); let seq_index_is_n_seq = IsEqualChip::configure( - meta, - |meta|meta.query_fixed(q_enabled, Rotation::cur()), - |meta|meta.query_advice(seq_index, Rotation::cur()), - |meta|meta.query_advice(n_seq, Rotation::cur()), + meta, + |meta| meta.query_fixed(q_enabled, Rotation::cur()), + |meta| meta.query_advice(seq_index, Rotation::cur()), + |meta| meta.query_advice(n_seq, Rotation::cur()), ); // seq_index must increment and compare with n_seq for seq border - meta.create_gate("seq index and section borders", |meta|{ + meta.create_gate("seq index and section borders", |meta| { let mut cb = BaseConstraintBuilder::default(); let seq_index_next = meta.query_advice(seq_index, Rotation::next()); let seq_index = meta.query_advice(seq_index, Rotation::cur()); let is_seq_border = &seq_index_is_n_seq; - cb.require_equal("seq index must increment or 0 in s_beginning", - select::expr( - is_seq_border.expr(), - 0.expr(), - seq_index.expr() + 1.expr(), - ), seq_index_next.expr() + cb.require_equal( + "seq index must increment or 0 in s_beginning", + select::expr(is_seq_border.expr(), 0.expr(), seq_index.expr() + 1.expr()), + seq_index_next.expr(), ); let s_beginning = meta.query_advice(s_beginning, Rotation::next()); - cb.require_boolean("s_beginning is boolean", - s_beginning.expr(), - ); + cb.require_boolean("s_beginning is boolean", s_beginning.expr()); - cb.condition(not::expr(is_seq_border.expr()), - |cb|{ - cb.require_zero("s_beginning on enabled after seq border", - s_beginning.expr(), - ) - } - ); + cb.condition(not::expr(is_seq_border.expr()), |cb| { + cb.require_zero( + "s_beginning on enabled after seq border", + s_beginning.expr(), + ) + }); - cb.gate( - meta.query_fixed(q_enabled, Rotation::next()) - ) + cb.gate(meta.query_fixed(q_enabled, Rotation::next())) }); - + debug_assert!(meta.degree() <= 9); // block index must be increment at seq border, so section for each // block index can occur once // and the lookup from seq_table enforce valid block / seq / s_beginning - // must be put - meta.create_gate("block index", |meta|{ + // must be put + meta.create_gate("block index", |meta| { let mut cb = BaseConstraintBuilder::default(); let block_index_next = meta.query_advice(block_index, Rotation::next()); @@ -351,65 +332,65 @@ impl SeqInstTable { let is_seq_border = &seq_index_is_n_seq; - cb.require_equal("block can only increase in seq border", + cb.require_equal( + "block can only increase in seq border", select::expr( is_seq_border.expr(), block_index.expr() + 1.expr(), block_index.expr(), - ), + ), block_index_next, ); cb.gate(meta.query_fixed(q_enabled, Rotation::next())) }); // so, we enforce s_beginning enabled for valid block index - meta.create_gate("border constaints", |meta|{ + meta.create_gate("border constaints", |meta| { let mut cb = BaseConstraintBuilder::default(); let s_beginning = meta.query_advice(s_beginning, Rotation::cur()); - let repeated_offset_pairs = [ - rep_offset_1, - rep_offset_2, - rep_offset_3, - ].map(|col| - (meta.query_advice(col, Rotation::cur()), - meta.query_advice(col, Rotation::prev())) - ); + let repeated_offset_pairs = [rep_offset_1, rep_offset_2, rep_offset_3].map(|col| { + ( + meta.query_advice(col, Rotation::cur()), + meta.query_advice(col, Rotation::prev()), + ) + }); for (repeated_offset, repeated_offset_prev) in repeated_offset_pairs { - cb.condition(s_beginning.expr(), |cb|{ - - cb.require_equal("offset must be inherited in border", - repeated_offset, + cb.condition(s_beginning.expr(), |cb| { + cb.require_equal( + "offset must be inherited in border", + repeated_offset, repeated_offset_prev, ) }); } let literal_len = meta.query_advice(literal_len, Rotation::cur()); - cb.require_equal("literal len accumulation", - select::expr(s_beginning.expr(), - literal_len.expr(), + cb.require_equal( + "literal len accumulation", + select::expr( + s_beginning.expr(), + literal_len.expr(), literal_len.expr() + meta.query_advice(acc_literal_len, Rotation::prev()), - ), + ), meta.query_advice(acc_literal_len, Rotation::cur()), ); cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); - meta.create_gate("offset update mode", |meta|{ + meta.create_gate("offset update mode", |meta| { let mut cb = BaseConstraintBuilder::default(); - cb.require_equal("ref update mode 1", - and::expr([ - not::expr(literal_is_zero.expr()), - offset_is_1.expr(), - ]), + cb.require_equal( + "ref update mode 1", + and::expr([not::expr(literal_is_zero.expr()), offset_is_1.expr()]), meta.query_advice(ref_update_mode_1, Rotation::cur()), ); - cb.require_equal("ref update mode 2", + cb.require_equal( + "ref update mode 2", select::expr( literal_is_zero.expr(), offset_is_1.expr(), @@ -418,7 +399,8 @@ impl SeqInstTable { meta.query_advice(ref_update_mode_2, Rotation::cur()), ); - cb.require_equal("ref update mode 3", + cb.require_equal( + "ref update mode 3", select::expr( literal_is_zero.expr(), offset_is_2.expr(), @@ -427,37 +409,29 @@ impl SeqInstTable { meta.query_advice(ref_update_mode_3, Rotation::cur()), ); - cb.require_equal("ref update mode 4", - and::expr([ - literal_is_zero.expr(), - offset_is_3.expr(), - ]), + cb.require_equal( + "ref update mode 4", + and::expr([literal_is_zero.expr(), offset_is_3.expr()]), meta.query_advice(ref_update_mode_4, Rotation::cur()), - ); + ); cb.gate(meta.query_fixed(q_enabled, Rotation::cur())) }); // offset is in-section (not s_beginning) - meta.create_gate("offset reference", |meta|{ + meta.create_gate("offset reference", |meta| { let mut cb = BaseConstraintBuilder::default(); let offset_val = meta.query_advice(offset, Rotation::cur()); let offset = meta.query_advice(match_offset, Rotation::cur()); - let [rep_offset_1_prev, rep_offset_2_prev, rep_offset_3_prev] - = [ - rep_offset_1, - rep_offset_2, - rep_offset_3, - ].map(|col|meta.query_advice(col, Rotation::prev())); - - let [rep_offset_1, rep_offset_2, rep_offset_3] - = [ - rep_offset_1, - rep_offset_2, - rep_offset_3, - ].map(|col|meta.query_advice(col, Rotation::cur())); + let [rep_offset_1_prev, rep_offset_2_prev, rep_offset_3_prev] = + [rep_offset_1, rep_offset_2, rep_offset_3] + .map(|col| meta.query_advice(col, Rotation::prev())); + + let [rep_offset_1, rep_offset_2, rep_offset_3] = + [rep_offset_1, rep_offset_2, rep_offset_3] + .map(|col| meta.query_advice(col, Rotation::cur())); let ref_update_mode_1 = meta.query_advice(ref_update_mode_1, Rotation::cur()); let ref_update_mode_2 = meta.query_advice(ref_update_mode_2, Rotation::cur()); @@ -471,9 +445,10 @@ impl SeqInstTable { // should not need this since all ref update modes are exclusive // cb.require_boolean("is offset is boolean", s_is_offset_ref.expr()); - // and ref in offset_1 is updated by current value - cb.require_equal("set offset 0 to offset val", - offset_val.expr(), + // and ref in offset_1 is updated by current value + cb.require_equal( + "set offset 0 to offset val", + offset_val.expr(), rep_offset_1.expr(), ); @@ -481,101 +456,102 @@ impl SeqInstTable { // for no-ref ref offset table 2/3 is // updated with a "shift" nature, and 1 is cooked_offset - 3 - cb.condition(not::expr(s_is_offset_ref.expr()),|cb|{ - cb.require_equal("offset is cooked_val - 3", + cb.condition(not::expr(s_is_offset_ref.expr()), |cb| { + cb.require_equal( + "offset is cooked_val - 3", offset.expr() - 3.expr(), rep_offset_1.expr(), ); - cb.require_equal("shift 1 -> 2", - rep_offset_1_prev.expr(), + cb.require_equal( + "shift 1 -> 2", + rep_offset_1_prev.expr(), rep_offset_2.expr(), ); - cb.require_equal("shift 2 -> 3", - rep_offset_2_prev.expr(), + cb.require_equal( + "shift 2 -> 3", + rep_offset_2_prev.expr(), rep_offset_3.expr(), - ); + ); }); // update mode 1 (offset == 1 and lit_len != 0) - cb.condition( - ref_update_mode_1.expr(), - |cb|{ - cb.require_equal("copy offset 1 for ref 1", - rep_offset_1_prev.expr(), - rep_offset_1.expr(), - ); - cb.require_equal("copy offset 2 for ref 1", - rep_offset_2_prev.expr(), - rep_offset_2.expr(), - ); - cb.require_equal("copy offset 3 for ref 1", - rep_offset_3_prev.expr(), - rep_offset_3.expr(), - ); - } - ); + cb.condition(ref_update_mode_1.expr(), |cb| { + cb.require_equal( + "copy offset 1 for ref 1", + rep_offset_1_prev.expr(), + rep_offset_1.expr(), + ); + cb.require_equal( + "copy offset 2 for ref 1", + rep_offset_2_prev.expr(), + rep_offset_2.expr(), + ); + cb.require_equal( + "copy offset 3 for ref 1", + rep_offset_3_prev.expr(), + rep_offset_3.expr(), + ); + }); // update mode 2 (offset == 2 / offet == 1 while lit_len != 0) - cb.condition( - ref_update_mode_2.expr(), - |cb|{ - cb.require_equal("swap 1&2 for ref 2", - rep_offset_2_prev.expr(), - rep_offset_1.expr(), - ); - cb.require_equal("swap 1&2 for ref 2", - rep_offset_1_prev.expr(), - rep_offset_2.expr(), - ); - cb.require_equal("copy offset 3 for ref 2", - rep_offset_3_prev.expr(), - rep_offset_3.expr(), - ); - } - ); + cb.condition(ref_update_mode_2.expr(), |cb| { + cb.require_equal( + "swap 1&2 for ref 2", + rep_offset_2_prev.expr(), + rep_offset_1.expr(), + ); + cb.require_equal( + "swap 1&2 for ref 2", + rep_offset_1_prev.expr(), + rep_offset_2.expr(), + ); + cb.require_equal( + "copy offset 3 for ref 2", + rep_offset_3_prev.expr(), + rep_offset_3.expr(), + ); + }); // update mode 3 (offset == 3 / offet == 2 while lit_len != 0) - cb.condition( - ref_update_mode_3.expr(), - |cb|{ - cb.require_equal("rotate 3-1 for ref 3", - rep_offset_3_prev.expr(), - rep_offset_1.expr(), - ); - cb.require_equal("rotate 3-1 for ref 3", - rep_offset_1_prev.expr(), - rep_offset_2.expr(), - ); - cb.require_equal("rotate 3-1 for ref 3", - rep_offset_2_prev.expr(), - rep_offset_3.expr(), - ); - } - ); + cb.condition(ref_update_mode_3.expr(), |cb| { + cb.require_equal( + "rotate 3-1 for ref 3", + rep_offset_3_prev.expr(), + rep_offset_1.expr(), + ); + cb.require_equal( + "rotate 3-1 for ref 3", + rep_offset_1_prev.expr(), + rep_offset_2.expr(), + ); + cb.require_equal( + "rotate 3-1 for ref 3", + rep_offset_2_prev.expr(), + rep_offset_3.expr(), + ); + }); // update mode 4 (offset == 3 while lit_len == 0) - cb.condition( - ref_update_mode_4.expr(), - |cb|{ - cb.require_zero("data must not corrupt", - ref_offset_1_is_zero.expr(), - ); - cb.require_equal("take ref 1 and minus 1 for ref 4", - rep_offset_1_prev.expr() - 1.expr(), - rep_offset_1.expr(), - ); - cb.require_equal("rotate 3-1 for ref 4", - rep_offset_1_prev.expr(), - rep_offset_2.expr(), - ); - cb.require_equal("rotate 3-1 for ref 4", - rep_offset_2_prev.expr(), - rep_offset_3.expr(), - ); - } - ); + cb.condition(ref_update_mode_4.expr(), |cb| { + cb.require_zero("data must not corrupt", ref_offset_1_is_zero.expr()); + cb.require_equal( + "take ref 1 and minus 1 for ref 4", + rep_offset_1_prev.expr() - 1.expr(), + rep_offset_1.expr(), + ); + cb.require_equal( + "rotate 3-1 for ref 4", + rep_offset_1_prev.expr(), + rep_offset_2.expr(), + ); + cb.require_equal( + "rotate 3-1 for ref 4", + rep_offset_2_prev.expr(), + rep_offset_3.expr(), + ); + }); cb.gate( - meta.query_fixed(q_enabled, Rotation::cur())* - not::expr(meta.query_advice(s_beginning, Rotation::cur())), + meta.query_fixed(q_enabled, Rotation::cur()) + * not::expr(meta.query_advice(s_beginning, Rotation::cur())), ) }); @@ -621,12 +597,12 @@ impl SeqInstTable { block_ind: u64, n_seq: usize, chip_ctx: &ChipContext, - offset_table: &[u64;3], - ) -> Result{ - + offset_table: &[u64; 3], + ) -> Result { region.assign_fixed( - ||"enable row", - self.q_enabled, offset, + || "enable row", + self.q_enabled, + offset, || Value::known(F::one()), )?; @@ -645,10 +621,7 @@ impl SeqInstTable { self.ref_update_mode_3, self.ref_update_mode_4, ] { - region.assign_advice( - ||"padding values", - col, offset, ||Value::known(F::zero()) - )?; + region.assign_advice(|| "padding values", col, offset, || Value::known(F::zero()))?; } for (col, val) in [ @@ -656,35 +629,42 @@ impl SeqInstTable { (self.rep_offset_2, offset_table[1]), (self.rep_offset_3, offset_table[2]), (self.block_index, block_ind), - (self.n_seq, n_seq as u64) - ]{ + (self.n_seq, n_seq as u64), + ] { region.assign_advice( - ||"header block fill", - col, offset, - ||Value::known(F::from(val)) - )?; + || "header block fill", + col, + offset, + || Value::known(F::from(val)), + )?; } - chip_ctx.literal_is_zero_chip.assign(region, offset, Value::known(F::zero()))?; - chip_ctx.ref_offset_1_is_zero_chip.assign(region, offset, Value::known(F::from(offset_table[0])))?; + chip_ctx + .literal_is_zero_chip + .assign(region, offset, Value::known(F::zero()))?; + chip_ctx.ref_offset_1_is_zero_chip.assign( + region, + offset, + Value::known(F::from(offset_table[0])), + )?; for (chip, val) in [ (&chip_ctx.offset_is_1_chip, F::from(1u64)), (&chip_ctx.offset_is_2_chip, F::from(2u64)), (&chip_ctx.offset_is_3_chip, F::from(3u64)), (&chip_ctx.seq_index_chip, F::from(n_seq as u64)), - ]{ + ] { chip.assign(region, offset, Value::known(F::zero()), Value::known(val))?; } - region.assign_advice(||"set beginning flag", + region.assign_advice( + || "set beginning flag", self.s_beginning, offset, - ||Value::known(F::one()), + || Value::known(F::one()), )?; - Ok(offset+1) - + Ok(offset + 1) } // padding for the rest row @@ -695,19 +675,12 @@ impl SeqInstTable { till_offset: usize, mut blk_index: u64, chip_ctx: &ChipContext, - offset_table: &[u64;3], - ) -> Result<(), Error>{ - + offset_table: &[u64; 3], + ) -> Result<(), Error> { // pad the rest rows until final row while offset < till_offset { - offset = self.assign_heading_row( - region, - offset, - blk_index, - 0, - chip_ctx, - offset_table, - )?; + offset = + self.assign_heading_row(region, offset, blk_index, 0, chip_ctx, offset_table)?; blk_index += 1; } @@ -723,29 +696,46 @@ impl SeqInstTable { mut offset: usize, block_ind: u64, n_seq: usize, - table_rows: impl Iterator, + table_rows: impl Iterator, chip_ctx: &ChipContext, - offset_table: &mut [u64;3], - ) -> Result{ - + offset_table: &mut [u64; 3], + ) -> Result { let mut seq_index = 0u64; let mut acc_literal_len = 0u64; for table_row in table_rows { - seq_index += 1; region.assign_fixed( - ||"enable row", - self.q_enabled, offset, + || "enable row", + self.q_enabled, + offset, || Value::known(F::one()), )?; let ref_update_mode = match table_row.cooked_match_offset { 0 => panic!("invalid cooked offset"), - 1 => if table_row.literal_length == 0 {2} else {1}, - 2 => if table_row.literal_length == 0 {3} else {2}, - 3 => if table_row.literal_length == 0 {4} else {3}, + 1 => { + if table_row.literal_length == 0 { + 2 + } else { + 1 + } + } + 2 => { + if table_row.literal_length == 0 { + 3 + } else { + 2 + } + } + 3 => { + if table_row.literal_length == 0 { + 4 + } else { + 3 + } + } _ => 0, }; @@ -759,46 +749,109 @@ impl SeqInstTable { for (name, col, val) in [ ("beginning flag", self.s_beginning, F::zero()), - ("offset table 1", self.rep_offset_1, F::from(offset_table[0])), - ("offset table 2", self.rep_offset_2, F::from(offset_table[1])), - ("offset table 3", self.rep_offset_3, F::from(offset_table[2])), + ( + "offset table 1", + self.rep_offset_1, + F::from(offset_table[0]), + ), + ( + "offset table 2", + self.rep_offset_2, + F::from(offset_table[1]), + ), + ( + "offset table 3", + self.rep_offset_3, + F::from(offset_table[2]), + ), ("mlen", self.match_len, F::from(table_row.match_length)), - ("moff", self.match_offset, F::from(table_row.cooked_match_offset)), + ( + "moff", + self.match_offset, + F::from(table_row.cooked_match_offset), + ), ("llen", self.literal_len, F::from(table_row.literal_length)), ("llen_acc", self.acc_literal_len, F::from(acc_literal_len)), ("offset", self.offset, F::from(table_row.actual_offset)), ("seq ind", self.seq_index, F::from(seq_index)), ("block ind", self.block_index, F::from(block_ind)), ("n_seq", self.n_seq, F::from(n_seq as u64)), - ("ref update mode", self.ref_update_mode_1, if ref_update_mode == 1 { F::one()} else {F::zero()}), - ("ref update mode", self.ref_update_mode_2, if ref_update_mode == 2 { F::one()} else {F::zero()}), - ("ref update mode", self.ref_update_mode_3, if ref_update_mode == 3 { F::one()} else {F::zero()}), - ("ref update mode", self.ref_update_mode_4, if ref_update_mode == 4 { F::one()} else {F::zero()}), + ( + "ref update mode", + self.ref_update_mode_1, + if ref_update_mode == 1 { + F::one() + } else { + F::zero() + }, + ), + ( + "ref update mode", + self.ref_update_mode_2, + if ref_update_mode == 2 { + F::one() + } else { + F::zero() + }, + ), + ( + "ref update mode", + self.ref_update_mode_3, + if ref_update_mode == 3 { + F::one() + } else { + F::zero() + }, + ), + ( + "ref update mode", + self.ref_update_mode_4, + if ref_update_mode == 4 { + F::one() + } else { + F::zero() + }, + ), ] { - region.assign_advice( - ||name, col, offset, ||Value::known(val) - )?; + region.assign_advice(|| name, col, offset, || Value::known(val))?; } for (chip, val) in [ - (&chip_ctx.literal_is_zero_chip, F::from(table_row.literal_length)), - (&chip_ctx.ref_offset_1_is_zero_chip, F::from(offset_table[0])), + ( + &chip_ctx.literal_is_zero_chip, + F::from(table_row.literal_length), + ), + ( + &chip_ctx.ref_offset_1_is_zero_chip, + F::from(offset_table[0]), + ), ] { chip.assign(region, offset, Value::known(val))?; } for (chip, val_l, val_r) in [ - (&chip_ctx.offset_is_1_chip, F::from(table_row.cooked_match_offset), F::from(1u64)), - (&chip_ctx.offset_is_2_chip, F::from(table_row.cooked_match_offset), F::from(2u64)), - (&chip_ctx.offset_is_3_chip, F::from(table_row.cooked_match_offset), F::from(3u64)), - (&chip_ctx.seq_index_chip, F::from(seq_index), F::from(n_seq as u64)), - ]{ - chip.assign( - region, - offset, - Value::known(val_l), - Value::known(val_r) - )?; + ( + &chip_ctx.offset_is_1_chip, + F::from(table_row.cooked_match_offset), + F::from(1u64), + ), + ( + &chip_ctx.offset_is_2_chip, + F::from(table_row.cooked_match_offset), + F::from(2u64), + ), + ( + &chip_ctx.offset_is_3_chip, + F::from(table_row.cooked_match_offset), + F::from(3u64), + ), + ( + &chip_ctx.seq_index_chip, + F::from(seq_index), + F::from(n_seq as u64), + ), + ] { + chip.assign(region, offset, Value::known(val_l), Value::known(val_r))?; } offset += 1; } @@ -808,12 +861,12 @@ impl SeqInstTable { Ok(offset) } - // assign the top row + // assign the top row fn init_top_row( &self, region: &mut Region, from_offset: Option, - ) -> Result{ + ) -> Result { let offset = from_offset.unwrap_or_default(); // top row constraint for (col, val) in [ @@ -821,61 +874,53 @@ impl SeqInstTable { (self.rep_offset_2, F::from(4u64)), (self.rep_offset_3, F::from(8u64)), ] { - region.assign_advice_from_constant(||"top row", col, offset, val)?; + region.assign_advice_from_constant(|| "top row", col, offset, val)?; } - for col in [ - self.block_index, - self.seq_index, - self.acc_literal_len, - ] { - region.assign_advice(||"top row flush", col, offset, ||Value::known(F::zero()))?; + for col in [self.block_index, self.seq_index, self.acc_literal_len] { + region.assign_advice(|| "top row flush", col, offset, || Value::known(F::zero()))?; } - for (col, val) in [ - (self.block_index, F::one()), - (self.seq_index, F::zero()), - ] { - region.assign_advice_from_constant(||"begin row constraint", col, offset+1, val)?; + for (col, val) in [(self.block_index, F::one()), (self.seq_index, F::zero())] { + region.assign_advice_from_constant(|| "begin row constraint", col, offset + 1, val)?; } - Ok(offset+1) + Ok(offset + 1) } - /// assign with multiple blocks, known the number of + /// assign with multiple blocks, known the number of /// sequences in advance pub fn assign<'a, R: ExactSizeIterator>( &self, layouter: &mut impl Layouter, table_rows: impl IntoIterator + Clone, enabled_rows: usize, - ) -> Result<(), Error>{ + ) -> Result<(), Error> { let chip_ctx = ChipContext::construct(self); layouter.assign_region( || "addr table", - |mut region|{ - let mut offset_table : [u64;3]= [1,4,8]; + |mut region| { + let mut offset_table: [u64; 3] = [1, 4, 8]; let mut blk_id = 0u64; let mut offset = self.init_top_row(&mut region, None)?; - for (i, rows_in_blk) in table_rows.clone() - .into_iter().enumerate(){ - blk_id = (i+1) as u64; + for (i, rows_in_blk) in table_rows.clone().into_iter().enumerate() { + blk_id = (i + 1) as u64; let n_seqs = rows_in_blk.len(); offset = self.assign_heading_row( - &mut region, - offset, - blk_id, - n_seqs, - &chip_ctx, + &mut region, + offset, + blk_id, + n_seqs, + &chip_ctx, &mut offset_table, )?; offset = self.assign_block( - &mut region, - offset, - blk_id, + &mut region, + offset, + blk_id, n_seqs, - rows_in_blk, - &chip_ctx, + rows_in_blk, + &chip_ctx, &mut offset_table, )?; assert!(offset < enabled_rows); @@ -883,15 +928,15 @@ impl SeqInstTable { self.padding_rows( &mut region, - offset, + offset, enabled_rows, - blk_id+1, - &chip_ctx, + blk_id + 1, + &chip_ctx, &offset_table, )?; Ok(()) - } + }, ) } @@ -901,61 +946,57 @@ impl SeqInstTable { layouter: &mut impl Layouter, table_rows: &[AddressTableRow], enabled_rows: usize, - ) -> Result<(), Error>{ + ) -> Result<(), Error> { let chip_ctx = ChipContext::construct(self); layouter.assign_region( || "addr table", - |mut region|{ - let mut offset_table : [u64;3]= [1,4,8]; + |mut region| { + let mut offset_table: [u64; 3] = [1, 4, 8]; let offset = self.init_top_row(&mut region, None)?; let offset = self.assign_heading_row( - &mut region, - offset, - 1, - table_rows.len(), - &chip_ctx, + &mut region, + offset, + 1, + table_rows.len(), + &chip_ctx, &mut offset_table, )?; let offset = self.assign_block( - &mut region, - offset, - 1, - table_rows.len(), - table_rows.iter(), - &chip_ctx, + &mut region, + offset, + 1, + table_rows.len(), + table_rows.iter(), + &chip_ctx, &mut offset_table, )?; assert!(offset < enabled_rows); self.padding_rows( &mut region, - offset, + offset, enabled_rows, - 2, - &chip_ctx, + 2, + &chip_ctx, &offset_table, )?; Ok(()) - } + }, ) } - } #[cfg(test)] mod tests { + use super::*; use halo2_proofs::{ - circuit::SimpleFloorPlanner, - dev::MockProver, - halo2curves::bn256::Fr, - plonk::Circuit, + circuit::SimpleFloorPlanner, dev::MockProver, halo2curves::bn256::Fr, plonk::Circuit, }; - use super::*; #[derive(Clone, Debug)] - struct SeqTable (Vec); + struct SeqTable(Vec); impl Circuit for SeqTable { type Config = SeqInstTable; @@ -963,54 +1004,43 @@ mod tests { fn without_witnesses(&self) -> Self { unimplemented!() } - - fn configure(meta: &mut ConstraintSystem) -> Self::Config { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { let const_col = meta.fixed_column(); meta.enable_constant(const_col); Self::Config::configure(meta) } - + fn synthesize( &self, config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - - config.mock_assign( - &mut layouter, - &self.0, - 15, - )?; + config.mock_assign(&mut layouter, &self.0, 15)?; Ok(()) } } #[test] - fn seqinst_table_gates(){ - + fn seqinst_table_gates() { // example comes from zstd's spec - let circuit = SeqTable( - AddressTableRow::mock_samples( - &[ - [1114, 11, 1111, 1, 4], - [1, 22, 1111, 1, 4], - [2225, 22, 2222, 1111, 1], - [1114, 111, 1111, 2222, 1111], - [3336, 33, 3333, 1111, 2222], - [2, 22, 1111, 3333, 2222], - [3, 33, 2222, 1111, 3333], - [3, 0, 2221, 2222, 1111], - [1, 0, 2222, 2221, 1111], - ], - ), - ); + let circuit = SeqTable(AddressTableRow::mock_samples(&[ + [1114, 11, 1111, 1, 4], + [1, 22, 1111, 1, 4], + [2225, 22, 2222, 1111, 1], + [1114, 111, 1111, 2222, 1111], + [3336, 33, 3333, 1111, 2222], + [2, 22, 1111, 3333, 2222], + [3, 33, 2222, 1111, 3333], + [3, 0, 2221, 2222, 1111], + [1, 0, 2222, 2221, 1111], + ])); let k = 12; - let mock_prover = MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); + let mock_prover = + MockProver::::run(k, &circuit, vec![]).expect("failed to run mock prover"); mock_prover.verify().unwrap(); - } }