diff --git a/aggregator/src/aggregation.rs b/aggregator/src/aggregation.rs index ccff10ecdb..e937899828 100644 --- a/aggregator/src/aggregation.rs +++ b/aggregator/src/aggregation.rs @@ -18,7 +18,7 @@ pub(crate) use barycentric::{ }; pub(crate) use batch_data::BatchDataConfig; pub(crate) use blob_data::BlobDataConfig; -pub(crate) use decoder::DecoderConfig; +pub(crate) use decoder::{DecoderConfig, DecoderConfigArgs}; pub(crate) use rlc::RlcConfig; pub use circuit::AggregationCircuit; diff --git a/aggregator/src/aggregation/config.rs b/aggregator/src/aggregation/config.rs index 08ba7bcb91..dc54510a50 100644 --- a/aggregator/src/aggregation/config.rs +++ b/aggregator/src/aggregation/config.rs @@ -12,14 +12,15 @@ use snark_verifier::{ }; use zkevm_circuits::{ keccak_circuit::{KeccakCircuitConfig, KeccakCircuitConfigArgs}, - table::{KeccakTable, PowOfRandTable, RangeTable, U8Table}, + table::{BitwiseOpTable, KeccakTable, Pow2Table, PowOfRandTable, RangeTable, U8Table}, util::{Challenges, SubCircuitConfig}, }; use crate::{ constants::{BITS, LIMBS}, param::ConfigParams, - BarycentricEvaluationConfig, BatchDataConfig, BlobDataConfig, DecoderConfig, RlcConfig, + BarycentricEvaluationConfig, BatchDataConfig, BlobDataConfig, DecoderConfig, DecoderConfigArgs, + RlcConfig, }; #[derive(Debug, Clone)] @@ -126,15 +127,21 @@ impl AggregationConfig { // Zstd decoder. let pow_rand_table = PowOfRandTable::construct(meta, &challenges_expr); + let pow2_table = Pow2Table::construct(meta); let range8 = RangeTable::construct(meta); let range16 = RangeTable::construct(meta); + let bitwise_op_table = BitwiseOpTable::construct(meta); let decoder_config = DecoderConfig::configure( meta, &challenges_expr, - pow_rand_table, - u8_table, - range8, - range16, + DecoderConfigArgs { + pow_rand_table, + pow2_table, + u8_table, + range8, + range16, + bitwise_op_table, + }, ); // Instance column stores public input column @@ -145,6 +152,7 @@ impl AggregationConfig { meta.enable_equality(instance); println!("meta degree = {:?}", meta.degree()); + debug_assert!(meta.degree() <= 9); Self { base_field_config, diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 1be8593efd..1005241b17 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -6,7 +6,7 @@ use gadgets::{ comparator::{ComparatorChip, ComparatorConfig}, is_equal::{IsEqualChip, IsEqualConfig}, less_than::{LtChip, LtConfig}, - util::{and, not, select, Expr}, + util::{and, not, select, sum, Expr}, }; use halo2_proofs::{ circuit::{AssignedCell, Layouter}, @@ -17,19 +17,18 @@ use halo2_proofs::{ poly::Rotation, }; use itertools::Itertools; -use witgen::{ZstdTag, N_BITS_PER_BYTE, N_BITS_ZSTD_TAG}; use zkevm_circuits::{ evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, - table::{LookupTable, PowOfRandTable, RangeTable, U8Table}, + table::{BitwiseOpTable, LookupTable, Pow2Table, PowOfRandTable, RangeTable, U8Table}, util::Challenges, }; use self::{ tables::{ - BitstringAccumulationTable, LiteralLengthCodes, LiteralsHeaderTable, MatchLengthCodes, - MatchOffsetCodes, RomSequenceCodes, RomTagTable, + BitstringTable, FseTable, LiteralLengthCodes, LiteralsHeaderTable, MatchLengthCodes, + MatchOffsetCodes, RomFseOrderTable, RomSequenceCodes, RomTagTable, }, - witgen::{N_BITS_REPEAT_FLAG, N_BLOCK_HEADER_BYTES}, + witgen::{ZstdTag, N_BITS_PER_BYTE, N_BITS_REPEAT_FLAG, N_BITS_ZSTD_TAG, N_BLOCK_HEADER_BYTES}, }; #[derive(Clone, Debug)] @@ -64,6 +63,8 @@ pub struct DecoderConfig { sequences_header_decoder: SequencesHeaderDecoder, /// Config for reading and decoding bitstreams. bitstream_decoder: BitstreamDecoder, + /// Config established while recovering the FSE table. + fse_decoder: FseDecoder, /// Range Table for [0, 8). range8: RangeTable<8>, /// Range Table for [0, 16). @@ -71,9 +72,13 @@ pub struct DecoderConfig { /// Helper table for decoding the regenerated size from LiteralsHeader. literals_header_table: LiteralsHeaderTable, /// Helper table for decoding bitstreams. - bitstring_accumulation_table: BitstringAccumulationTable, + bitstring_table: BitstringTable, + /// Helper table for decoding FSE tables. + fse_table: FseTable, /// ROM table for validating tag transition. rom_tag_table: RomTagTable, + /// ROM table for the correct order in which FSE tables are described in the sequences section. + rom_fse_order_table: RomFseOrderTable, /// ROM table for Literal Length Codes. rom_llc_table: RomSequenceCodes, /// ROM table for Match Length Codes. @@ -122,6 +127,8 @@ struct TagConfig { is_frame_content_size: Column, /// Degree reduction: BlockHeader is_block_header: Column, + /// Degree reduction: SequenceFseCode + is_fse_code: Column, } impl TagConfig { @@ -153,6 +160,7 @@ impl TagConfig { // degree reduction. is_frame_content_size: meta.advice_column(), is_block_header: meta.advice_column(), + is_fse_code: meta.advice_column(), } } } @@ -363,13 +371,15 @@ pub struct BitstreamDecoder { bitstring_value_eq_1: IsEqualConfig, /// Helper config as per the above doc. bitstring_value_eq_3: IsEqualConfig, - /// Boolean that is set for the special case that we don't read from the bitstream, i.e. we - /// read 0 number of bits. We can witness such a case while applying an FSE table to bitstream, - /// where the number of bits to be read from the bitstream is 0. + /// Boolean that is set for two special cases: + /// + /// 1. We don't read from the bitstream, i.e. we read 0 number of bits. We can witness such a + /// case while applying an FSE table to bitstream, where the number of bits to be read from + /// the bitstream is 0. This can happen when we decode sequences + /// 2. The bitstring that we have read in the current row is byte-aligned up to the next or the + /// next-to-next byte. In this case, the next or the next-to-next following row(s) should + /// have the is_nil field set. is_nil: Column, - /// The symbol that this bitstring decodes to. While applying an FSE table, this translates to - /// the symbol emitted from the FSE state before reading NB bits from bitstream. - decoded_symbol: Column, } impl BitstreamDecoder { @@ -418,17 +428,22 @@ impl BitstreamDecoder { |_| 3.expr(), ), is_nil: meta.advice_column(), - decoded_symbol: meta.advice_column(), } } } impl BitstreamDecoder { - /// Whether the number of bits to be read from bitstream is 0, i.e. no bits to be read. + /// Whether the number of bits to be read from bitstream (at this row) is 0, i.e. no bits to be + /// read. fn is_nil(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { meta.query_advice(self.is_nil, rotation) } + /// True when a bitstream is read from the current row. + fn is_not_nil(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { + not::expr(self.is_nil(meta, rotation)) + } + /// While reconstructing the FSE table, indicates whether a value=1 was found, i.e. prob=0. In /// this case, the symbol is followed by 2-bits repeat flag instead. fn is_prob0(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { @@ -467,6 +482,17 @@ impl BitstreamDecoder { lt + eq } + /// A bitstring spans 1 byte and is byte-aligned: + /// - bit_index_end == 7. + fn aligned_one_byte( + &self, + meta: &mut VirtualCells, + rotation: Option, + ) -> Expression { + let (_lt, eq) = self.bit_index_end_cmp_7.expr(meta, rotation); + eq + } + /// A bitstring strictly spans 2 bytes if the bit_index at which it ends is such that: /// - 8 <= bit_index_end < 15. fn strictly_spans_two_bytes( @@ -481,6 +507,7 @@ impl BitstreamDecoder { /// A bitstring spans 2 bytes if the bit_index at which it ends is such that: /// - 8 <= bit_index_end <= 15. + #[allow(dead_code)] fn spans_two_bytes( &self, meta: &mut VirtualCells, @@ -491,6 +518,17 @@ impl BitstreamDecoder { not::expr(spans_one_byte) * (lt2 + eq2) } + /// A bitstring spans 2 bytes and is byte-aligned: + /// - bit_index_end == 15. + fn aligned_two_bytes( + &self, + meta: &mut VirtualCells, + rotation: Option, + ) -> Expression { + let (_lt, eq) = self.bit_index_end_cmp_15.expr(meta, rotation); + eq + } + /// A bitstring strictly spans 3 bytes if the bit_index at which it ends is such that: /// - 16 <= bit_index_end < 23. fn strictly_spans_three_bytes( @@ -498,19 +536,64 @@ impl BitstreamDecoder { meta: &mut VirtualCells, rotation: Option, ) -> Expression { - let spans_two_bytes = self.spans_two_bytes(meta, rotation); + let (lt2, eq2) = self.bit_index_end_cmp_15.expr(meta, rotation); let (lt3, _eq3) = self.bit_index_end_cmp_23.expr(meta, rotation); - not::expr(spans_two_bytes) * lt3 + not::expr(lt2 + eq2) * lt3 } /// A bitstring spans 3 bytes if the bit_index at which it ends is such that: /// - 16 <= bit_index_end <= 23. + #[allow(dead_code)] fn spans_three_bytes( &self, meta: &mut VirtualCells, rotation: Option, ) -> Expression { - not::expr(self.spans_two_bytes(meta, rotation)) + let (lt2, eq2) = self.bit_index_end_cmp_15.expr(meta, rotation); + not::expr(lt2 + eq2) + } + + /// A bitstring spans 3 bytes and is byte-aligned: + /// - bit_index_end == 23. + fn aligned_three_bytes( + &self, + meta: &mut VirtualCells, + rotation: Option, + ) -> Expression { + let (_lt, eq) = self.bit_index_end_cmp_23.expr(meta, rotation); + eq + } +} + +#[derive(Clone, Debug)] +pub struct FseDecoder { + /// The byte_idx at which the FSE table is described at. + byte_offset: Column, + /// The FSE table that is being decoded in this tag. Possible values are: + /// - LLT = 0, MOT = 1, MLT = 2 + table_kind: Column, + /// The number of states in the FSE table. table_size == 1 << AL, where AL is the accuracy log + /// of the FSE table. + table_size: Column, + /// The incremental symbol for which probability is decoded. + symbol: Column, + /// An accumulator of the number of states allocated to each symbol as we decode the FSE table. + /// This is the normalised probability for the symbol. + probability_acc: Column, + /// Whether we are in the repeat bits loop. + is_repeat_bits_loop: Column, +} + +impl FseDecoder { + fn configure(meta: &mut ConstraintSystem) -> Self { + Self { + byte_offset: meta.advice_column(), + table_kind: meta.advice_column(), + table_size: meta.advice_column(), + symbol: meta.advice_column(), + probability_acc: meta.advice_column(), + is_repeat_bits_loop: meta.advice_column(), + } } } @@ -521,24 +604,45 @@ pub struct AssignedDecoderConfigExports { pub decoded_rlc: AssignedCell, } +pub struct DecoderConfigArgs { + /// Power of randomness table. + pub pow_rand_table: PowOfRandTable, + /// Power of 2 lookup table, up to exponent=20. + pub pow2_table: Pow2Table<20>, + /// Range table for lookup: [0, 256). + pub u8_table: U8Table, + /// Range table for lookup: [0, 8). + pub range8: RangeTable<8>, + /// Range table for lookup: [0, 16). + pub range16: RangeTable<16>, + /// Bitwise operation lookup table. + pub bitwise_op_table: BitwiseOpTable, +} + impl DecoderConfig { pub fn configure( meta: &mut ConstraintSystem, challenges: &Challenges>, - pow_rand_table: PowOfRandTable, - u8_table: U8Table, - range8: RangeTable<8>, - range16: RangeTable<16>, + DecoderConfigArgs { + pow_rand_table, + pow2_table, + u8_table, + range8, + range16, + bitwise_op_table, + }: DecoderConfigArgs, ) -> Self { // Fixed tables let rom_tag_table = RomTagTable::construct(meta); + let rom_fse_order_table = RomFseOrderTable::construct(meta); let rom_llc_table = RomSequenceCodes::::construct(meta); let rom_mlc_table = RomSequenceCodes::::construct(meta); let rom_moc_table = RomSequenceCodes::::construct(meta); // Helper tables let literals_header_table = LiteralsHeaderTable::configure(meta, range8, range16); - let bitstring_accumulation_table = BitstringAccumulationTable::configure(meta); + let bitstring_table = BitstringTable::configure(meta); + let fse_table = FseTable::configure(meta, u8_table, range8, pow2_table, bitwise_op_table); // Peripheral configs let tag_config = TagConfig::configure(meta); @@ -547,6 +651,7 @@ impl DecoderConfig { let sequences_header_decoder = SequencesHeaderDecoder::configure(meta, byte, is_padding, u8_table); let bitstream_decoder = BitstreamDecoder::configure(meta, is_padding, u8_table); + let fse_decoder = FseDecoder::configure(meta); // Main config let config = Self { @@ -568,11 +673,14 @@ impl DecoderConfig { block_config, sequences_header_decoder, bitstream_decoder, + fse_decoder, range8, range16, literals_header_table, - bitstring_accumulation_table, + bitstring_table, + fse_table, rom_tag_table, + rom_fse_order_table, rom_llc_table, rom_mlc_table, rom_moc_table, @@ -596,6 +704,7 @@ impl DecoderConfig { is_tag!(is_zb_literals_header, ZstdBlockLiteralsHeader); is_tag!(is_zb_raw_block, ZstdBlockLiteralsRawBytes); is_tag!(is_zb_sequence_header, ZstdBlockSequenceHeader); + is_tag!(is_zb_sequence_fse, ZstdBlockFseCode); meta.lookup("DecoderConfig: 0 <= encoded byte < 256", |meta| { vec![( @@ -741,6 +850,7 @@ impl DecoderConfig { is_frame_content_size(meta) ); degree_reduction_check!(config.tag_config.is_block_header, is_block_header(meta)); + degree_reduction_check!(config.tag_config.is_fse_code, is_zb_sequence_fse(meta)); cb.gate(condition) }); @@ -1463,6 +1573,705 @@ impl DecoderConfig { debug_assert!(meta.degree() <= 9); + /////////////////////////////////////////////////////////////////////////////////////////// + /////////////////////////// ZstdTag::ZstdBlockSequenceFseCode ///////////////////////////// + /////////////////////////////////////////////////////////////////////////////////////////// + meta.create_gate( + "DecoderConfig: tag ZstdBlockSequenceFseCode (first row)", + |meta| { + // The first row of a ZstdBlockSequenceFseCode tag. + let condition = and::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + meta.query_advice(config.tag_config.is_change, Rotation::cur()), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // At this tag=ZstdBlockSequenceFseCode we are not processing bits instead of + // bytes. The first bitstring is the 4-bits bitstring that encodes the accuracy log + // of the FSE table. + cb.require_zero( + "fse(al): bit_index_start == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + ); + + cb.require_equal( + "fse(al): bit_index_end == 3", + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + 3.expr(), + ); + + cb.require_equal( + "fse: byte_offset", + meta.query_advice(config.byte_idx, Rotation::cur()), + meta.query_advice(config.fse_decoder.byte_offset, Rotation::cur()), + ); + + cb.require_zero( + "fse(init): probability_acc=0", + meta.query_advice(config.fse_decoder.probability_acc, Rotation::cur()), + ); + + // The symbol=0 is handled immediately after the AL 4-bits. + cb.require_zero( + "fse(init): symbol=0", + meta.query_advice(config.fse_decoder.symbol, Rotation::next()), + ); + + // The is_repeat_bits_loop inits at 0 after the AL 4-bits. + cb.require_zero( + "fse(init): is_repeat_bits_loop=0", + meta.query_advice(config.fse_decoder.is_repeat_bits_loop, Rotation::next()), + ); + + // We will always start reading bits from the bitstream for the first symbol. + cb.require_zero( + "fse(init): is_nil=0", + config.bitstream_decoder.is_nil(meta, Rotation::next()), + ); + + cb.gate(condition) + }, + ); + + meta.lookup_any( + "DecoderConfig: tag ZstdBlockSequenceFseCode (table kind)", + |meta| { + let condition = and::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + meta.query_advice(config.tag_config.is_change, Rotation::cur()), + ]); + + [ + meta.query_advice(config.tag_config.tag, Rotation::prev()), // tag_prev + meta.query_advice(config.tag_config.tag, Rotation::cur()), // tag_cur + meta.query_advice(config.tag_config.tag_next, Rotation::cur()), // tag_next + meta.query_advice(config.fse_decoder.table_kind, Rotation::cur()), // table_kind + ] + .into_iter() + .zip_eq(config.rom_fse_order_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + + meta.lookup_any( + "DecoderConfig: tag ZstdBlockSequenceFseCode (table size)", + |meta| { + let condition = and::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + meta.query_advice(config.tag_config.is_change, Rotation::cur()), + ]); + + // accuracy_log == 4bits + 5 + let al = meta + .query_advice(config.bitstream_decoder.bitstring_value, Rotation::cur()) + + 5.expr(); + let table_size = meta.query_advice(config.fse_decoder.table_size, Rotation::cur()); + + // table_size == 1 << al + [al, table_size] + .into_iter() + .zip_eq(pow2_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + + meta.create_gate( + "DecoderConfig: tag ZstdBlockSequenceFseCode (other rows)", + |meta| { + let condition = and::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + not::expr(meta.query_advice(config.tag_config.is_change, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // FseDecoder columns that remain unchanged. + for column in [ + config.fse_decoder.byte_offset, + config.fse_decoder.table_kind, + config.fse_decoder.table_size, + ] { + cb.require_equal( + "fse_decoder column unchanged", + meta.query_advice(column, Rotation::cur()), + meta.query_advice(column, Rotation::prev()), + ); + } + + // FSE tables are decoded for Literal Length (LLT), Match Offset (MOT) and Match + // Length (MLT). + // + // The maximum permissible accuracy log for the above are: + // - LLT: 9 + // - MOT: 8 + // - MLT: 9 + // + // Which means, at the most we would be reading a bitstring up to length=9. Note + // that an FSE table would exist only if there are more than one symbols and in + // that case, we wouldn't actually reserve ALL possibly states for a single symbol, + // indirectly meaning that we would be reading bitstrings of at the most length=9. + // + // The only scenario in which we would skip reading bits from a byte altogether is + // if the bitstring is ``aligned_two_bytes``. + cb.require_zero( + "fse: bitstrings cannot span 3 bytes", + config + .bitstream_decoder + .spans_three_bytes(meta, Some(Rotation::cur())), + ); + + // If the bitstring read at the current row is ``aligned_two_bytes`` then the one + // on the next row is nil (not read). + cb.condition( + config + .bitstream_decoder + .aligned_two_bytes(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "fse: aligned_two_bytes is followed by is_nil", + config.bitstream_decoder.is_nil(meta, Rotation::next()), + 1.expr(), + ); + }, + ); + + // We now tackle the scenario of observing value=1 (prob=0) which is then followed + // by 2-bits repeat bits. + // + // If we are not in a repeat-bits loop and encounter a value=1 (prob=0) bitstring, + // then we enter a repeat bits loop. + let is_repeat_bits_loop = + meta.query_advice(config.fse_decoder.is_repeat_bits_loop, Rotation::cur()); + cb.condition( + and::expr([ + not::expr(is_repeat_bits_loop.expr()), + config.bitstream_decoder.is_prob0(meta, Rotation::cur()), + ]), + |cb| { + cb.require_equal( + "fse: enter repeat-bits loop", + meta.query_advice( + config.fse_decoder.is_repeat_bits_loop, + Rotation::next(), + ), + 1.expr(), + ); + }, + ); + + // If we are in a repeat-bits loop and the repeat-bits are [1, 1], then continue + // the repeat-bits loop. + let is_rb_flag3 = config.bitstream_decoder.is_rb_flag3(meta, Rotation::cur()); + cb.condition( + and::expr([is_repeat_bits_loop.expr(), is_rb_flag3.expr()]), + |cb| { + cb.require_equal( + "fse: continue repeat-bits loop", + meta.query_advice( + config.fse_decoder.is_repeat_bits_loop, + Rotation::next(), + ), + 1.expr(), + ); + }, + ); + + // If we are in a repeat-bits loop and the repeat-bits are not [1, 1] then break + // out of the repeat-bits loop. + cb.condition( + and::expr([is_repeat_bits_loop.expr(), not::expr(is_rb_flag3)]), + |cb| { + cb.require_zero( + "fse: break out of repeat-bits loop", + meta.query_advice( + config.fse_decoder.is_repeat_bits_loop, + Rotation::next(), + ), + ); + }, + ); + + // We not tackle the normalised probability of symbols in the FSE table, their + // updating and the FSE symbol itself. + // + // If no bitstring was read, even the symbol value is carried forward. + let (prob_acc_cur, prob_acc_prev, fse_symbol_cur, fse_symbol_prev, value) = ( + meta.query_advice(config.fse_decoder.probability_acc, Rotation::cur()), + meta.query_advice(config.fse_decoder.probability_acc, Rotation::prev()), + meta.query_advice(config.fse_decoder.symbol, Rotation::cur()), + meta.query_advice(config.fse_decoder.symbol, Rotation::prev()), + meta.query_advice(config.bitstream_decoder.bitstring_value, Rotation::cur()), + ); + cb.condition( + config.bitstream_decoder.is_nil(meta, Rotation::cur()), + |cb| { + cb.require_equal( + "fse: probability_acc continues", + prob_acc_cur.expr(), + prob_acc_prev.expr(), + ); + cb.require_equal( + "fse: symbol continues", + fse_symbol_cur.expr(), + fse_symbol_prev.expr(), + ); + }, + ); + + // As we decode the normalised probability for each symbol in the FSE table, we + // update the probability accumulator. It should be updated as long as we are + // reading a bitstring and we are not in the repeat-bits loop. + cb.condition( + and::expr([ + config.bitstream_decoder.is_not_nil(meta, Rotation::cur()), + not::expr(is_repeat_bits_loop.expr()), + ]), + |cb| { + // prob_acc_cur == prob_acc_prev + (value - 1) + cb.require_equal( + "fse: probability_acc is updated correctly", + prob_acc_cur.expr() + 1.expr(), + prob_acc_prev.expr() + value.expr(), + ); + cb.require_equal( + "fse: symbol increments", + fse_symbol_cur.expr(), + fse_symbol_prev.expr() + 1.expr(), + ); + }, + ); + + // If we are in the repeat-bits loop, then the normalised probability accumulator + // does not change, as the repeat-bits loop is for symbols that are not emitted + // through the FSE table. However, the symbol value itself increments by the value + // in the 2 repeat bits. + cb.condition(is_repeat_bits_loop.expr(), |cb| { + let bit_index_start = meta + .query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()); + let bit_index_end = + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()); + cb.require_equal( + "fse: repeat-bits read N_BITS_REPEAT_FLAG=2 bits", + bit_index_end - bit_index_start + 1.expr(), + N_BITS_REPEAT_FLAG.expr(), + ); + cb.require_equal( + "fse: repeat-bits do not change probability_acc", + prob_acc_cur, + prob_acc_prev, + ); + cb.require_equal( + "fse: repeat-bits increases by the 2-bit value", + fse_symbol_cur, + fse_symbol_prev + value, + ); + }); + + cb.gate(condition) + }, + ); + + meta.lookup_any( + "DecoderConfig: tag ZstdBlockSequenceFseCode (normalised probability of symbol)", + |meta| { + // At every row where a non-nil bitstring is read: + // - except the AL bits + // - except when the value=1, i.e. prob=0 + // - except when we are in repeat-bits loop + let condition = and::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + config.bitstream_decoder.is_not_nil(meta, Rotation::cur()), + not::expr(meta.query_advice(config.tag_config.is_change, Rotation::cur())), + not::expr(config.bitstream_decoder.is_prob0(meta, Rotation::cur())), + not::expr( + meta.query_advice(config.fse_decoder.is_repeat_bits_loop, Rotation::cur()), + ), + ]); + + let (fse_byte_offset, fse_table_size, fse_symbol, bitstring_value) = ( + meta.query_advice(config.fse_decoder.byte_offset, Rotation::cur()), + meta.query_advice(config.fse_decoder.table_size, Rotation::cur()), + meta.query_advice(config.fse_decoder.symbol, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bitstring_value, Rotation::cur()), + ); + let norm_prob = bitstring_value - 1.expr(); + + [ + fse_byte_offset, + fse_table_size, + fse_symbol, + norm_prob.expr(), + norm_prob.expr(), + 0.expr(), // is_padding + ] + .into_iter() + .zip_eq(config.fse_table.table_exprs_by_symbol(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + + debug_assert!(meta.degree() <= 9); + + /////////////////////////////////////////////////////////////////////////////////////////// + ////////////////////////////////// Bitstream Decoding ///////////////////////////////////// + /////////////////////////////////////////////////////////////////////////////////////////// + meta.create_gate("DecoderConfig: Bitstream Decoder (nil)", |meta| { + // Bitstream decoder when the bitstring to be read is nil. + let condition = and::expr([ + config.bitstream_decoder.is_nil(meta, Rotation::cur()), + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + cb.require_equal( + "bit_index_start == bit_index_end", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + ); + + cb.require_equal( + "bit_index_start' == bit_index_start", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::next()), + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + ); + + cb.require_equal( + "byte_idx' == byte_idx", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()), + ); + + cb.gate(condition) + }); + + meta.create_gate("DecoderConfig: Bitstream Decoder (not nil)", |meta| { + // Bitstream decoder when the bitstring to be read is not nil. + let condition = and::expr([ + not::expr(config.bitstream_decoder.is_nil(meta, Rotation::cur())), + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // We process bits instead of bytes for a few tags, namely, ZstdBlockSequenceFseCode + // and ZstdBlockSequenceData. In these tags, over adjacent rows we may experience: + // - byte_idx' == byte_idx + // - byte_idx' == byte_idx + 1 + // depending on whether or not the bitstring read was byte-aligned. + // + // The maximum length of bitstring we expect at the moment is N=17, which means the + // bitstring accumulation table supports bitstring accumulation up to 3 contiguous + // bytes. + // + // We have the following scenarios: + // - bitstring strictly spans over 1 byte: 0 <= bit_index_end < 7. + // - bitstring is byte aligned: bit_index_end == 7. + // - bitstring strictly spans over 2 bytes: 8 <= bit_index_end < 15. + // - bitstring is byte aligned: bit_index_end == 15. + // - bitstring strictly spans over 3 bytes: 16 <= bit_index_end < 23. + // - bitstring is byte aligned: bit_index_end == 23. + // + // Every row is reserved for a bitstring read from the bitstream. That is, we have: + // - bitstring_len == bit_index_end - bit_index_start + 1 + // + // On some rows we may not be reading a bitstring. This can occur when: + // - The number of bits to be read is 0, i.e. NB_fse == 0. + // - The previous row read a bitstring that spanned over 2 bytes and was byte-aligned. + // - No bitstring is read on the current row. + // - The previous row read a bitstring that spanned over 3 bytes. + // - No bitstring is read on the current row. + // - The previous row read a bitstring that spanned over 3 bytes and was byte-aligned. + // - No bitstring is read on the current and next row. + + // 1. bitstring strictly spans over 1 byte: 0 <= bit_index_end < 7. + cb.condition( + config + .bitstream_decoder + .strictly_spans_one_byte(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case1): byte_idx' == byte_idx", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()), + ); + cb.require_equal( + "(case1): bit_index_start' == bit_index_end + 1", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()) + + 1.expr(), + ); + }, + ); + + // 2. bitstring is byte-aligned: bit_index_end == 7. + cb.condition( + config + .bitstream_decoder + .aligned_one_byte(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case2): byte_idx' == byte_idx + 1", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()) + 1.expr(), + ); + cb.require_zero( + "(case2): bit_index_start' == 0", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ), + ); + }, + ); + + // 3. bitstring strictly spans over 2 bytes: 8 <= bit_index_end < 15. + cb.condition( + config + .bitstream_decoder + .strictly_spans_two_bytes(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case3): byte_idx' == byte_idx + 1", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()) + 1.expr(), + ); + cb.require_equal( + "(case3): bit_index_start' == bit_index_end - 7", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ) + 7.expr(), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + ); + }, + ); + + // 4. bitstring is byte-aligned: bit_index_end == 15. + cb.condition( + config + .bitstream_decoder + .aligned_two_bytes(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case4): byte_idx' == byte_idx + 1", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()) + 1.expr(), + ); + cb.require_equal( + "(case4): byte_idx'' == byte_idx + 2", + meta.query_advice(config.byte_idx, Rotation(2)), + meta.query_advice(config.byte_idx, Rotation::cur()) + 2.expr(), + ); + cb.require_equal( + "(case4): bitstring decoder skipped next row", + config.bitstream_decoder.is_nil(meta, Rotation::next()), + 1.expr(), + ); + cb.require_zero( + "(case4): bit_index_start' == 0", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ), + ); + cb.require_zero( + "(case4): bit_index_start'' == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation(2)), + ); + }, + ); + + // 5. bitstring strictly spans over 3 bytes: 16 <= bit_index_end < 23. + cb.condition( + config + .bitstream_decoder + .strictly_spans_three_bytes(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case5): byte_idx' == byte_idx + 1", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()) + 1.expr(), + ); + cb.require_equal( + "(case5): byte_idx'' == byte_idx + 2", + meta.query_advice(config.byte_idx, Rotation(2)), + meta.query_advice(config.byte_idx, Rotation::cur()) + 2.expr(), + ); + cb.require_equal( + "(case5): bitstring decoder skipped next row", + config.bitstream_decoder.is_nil(meta, Rotation::next()), + 1.expr(), + ); + cb.require_equal( + "(case5): bit_index_start' == bit_index_start''", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ), + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation(2)), + ); + cb.require_equal( + "(case5): bit_index_start'' == bit_index_end - 15", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation(2)) + + 15.expr(), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + ); + }, + ); + + // 6. bitstring is byte-aligned: bit_index_end == 23. + cb.condition( + config + .bitstream_decoder + .aligned_three_bytes(meta, Some(Rotation::cur())), + |cb| { + cb.require_equal( + "(case6): byte_idx' == byte_idx + 1", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()) + 1.expr(), + ); + cb.require_equal( + "(case6): byte_idx'' == byte_idx + 2", + meta.query_advice(config.byte_idx, Rotation(2)), + meta.query_advice(config.byte_idx, Rotation::cur()) + 2.expr(), + ); + cb.require_equal( + "(case6): byte_idx''' == byte_idx + 3", + meta.query_advice(config.byte_idx, Rotation(3)), + meta.query_advice(config.byte_idx, Rotation::cur()) + 3.expr(), + ); + cb.require_equal( + "(case6): bitstring decoder skipped next row", + config.bitstream_decoder.is_nil(meta, Rotation::next()), + 1.expr(), + ); + cb.require_equal( + "(case6): bitstring decoder skipped next-to-next row", + config.bitstream_decoder.is_nil(meta, Rotation(2)), + 1.expr(), + ); + cb.require_zero( + "(case6): bit_index_start' == 0", + meta.query_advice( + config.bitstream_decoder.bit_index_start, + Rotation::next(), + ), + ); + cb.require_zero( + "(case6): bit_index_start'' == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation(2)), + ); + cb.require_zero( + "(case6): bit_index_start''' == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation(3)), + ); + }, + ); + + cb.gate(condition) + }); + + meta.lookup_any( + "DecoderConfig: Bitstream Decoder (bitstring start)", + |meta| { + let condition = and::expr([ + not::expr(config.bitstream_decoder.is_nil(meta, Rotation::cur())), + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), + ]); + + let (byte_idx0, byte_idx1, byte_idx2) = ( + meta.query_advice(config.byte_idx, Rotation(0)), + meta.query_advice(config.byte_idx, Rotation(1)), + meta.query_advice(config.byte_idx, Rotation(2)), + ); + let (byte0, byte1, byte2) = ( + meta.query_advice(config.byte, Rotation(0)), + meta.query_advice(config.byte, Rotation(1)), + meta.query_advice(config.byte, Rotation(2)), + ); + let (bit_index_start, _bit_index_end, bitstring_value) = ( + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bitstring_value, Rotation::cur()), + ); + let is_reverse = meta.query_advice(config.tag_config.is_reverse, Rotation::cur()); + + [ + byte_idx0, + byte_idx1, + byte_idx2, + byte0, + byte1, + byte2, + bitstring_value, + 1.expr(), // bitstring_len at start + bit_index_start, + 1.expr(), // from_start + 1.expr(), // until_end + is_reverse, + 0.expr(), // is_padding + ] + .into_iter() + .zip_eq(config.bitstring_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + + meta.lookup_any("DecoderConfig: Bitstream Decoder (bitstring end)", |meta| { + let condition = and::expr([ + not::expr(config.bitstream_decoder.is_nil(meta, Rotation::cur())), + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), + ]); + + let (byte_idx0, byte_idx1, byte_idx2) = ( + meta.query_advice(config.byte_idx, Rotation(0)), + meta.query_advice(config.byte_idx, Rotation(1)), + meta.query_advice(config.byte_idx, Rotation(2)), + ); + let (byte0, byte1, byte2) = ( + meta.query_advice(config.byte, Rotation(0)), + meta.query_advice(config.byte, Rotation(1)), + meta.query_advice(config.byte, Rotation(2)), + ); + let (bit_index_start, bit_index_end, bitstring_value) = ( + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + meta.query_advice(config.bitstream_decoder.bitstring_value, Rotation::cur()), + ); + let is_reverse = meta.query_advice(config.tag_config.is_reverse, Rotation::cur()); + + [ + byte_idx0, + byte_idx1, + byte_idx2, + byte0, + byte1, + byte2, + bitstring_value, + bit_index_end.expr() - bit_index_start + 1.expr(), // bitstring_len at end + bit_index_end, + 1.expr(), // from_start + 1.expr(), // until_end + is_reverse, + 0.expr(), // is_padding + ] + .into_iter() + .zip_eq(config.bitstring_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }); + + debug_assert!(meta.degree() <= 9); + config } diff --git a/aggregator/src/aggregation/decoder/tables.rs b/aggregator/src/aggregation/decoder/tables.rs index 39922c6185..271ae758fa 100644 --- a/aggregator/src/aggregation/decoder/tables.rs +++ b/aggregator/src/aggregation/decoder/tables.rs @@ -1,13 +1,21 @@ /// Since bitstrings to decode can be spanned over more than one byte from the encoded bytes, we /// construct a table to accumulate the binary values of the byte-unaligned bitstrings for decoding /// convenience. -mod bitstring_accumulation; -pub use bitstring_accumulation::BitstringAccumulationTable; +mod bitstring; +pub use bitstring::BitstringTable; + +/// FSE table. +mod fse; +pub use fse::FseTable; /// Decode the regenerated size from the literals header. mod literals_header; pub use literals_header::LiteralsHeaderTable; +/// Validate the assignment of FSE table kind while decoding FSE tables in the sequences section. +mod rom_fse_order; +pub use rom_fse_order::RomFseOrderTable; + /// The fixed code to Baseline/NumBits for Literal Length. mod rom_sequence_codes; pub use rom_sequence_codes::{ diff --git a/aggregator/src/aggregation/decoder/tables/bitstring_accumulation.rs b/aggregator/src/aggregation/decoder/tables/bitstring.rs similarity index 96% rename from aggregator/src/aggregation/decoder/tables/bitstring_accumulation.rs rename to aggregator/src/aggregation/decoder/tables/bitstring.rs index 71fbccb15c..9f53e985f3 100644 --- a/aggregator/src/aggregation/decoder/tables/bitstring_accumulation.rs +++ b/aggregator/src/aggregation/decoder/tables/bitstring.rs @@ -58,7 +58,7 @@ use crate::aggregation::decoder::witgen::ZstdWitnessRow; /// the bits of interest where "from_start == until_end == 1". Over these rows, we accumulate the /// binary value and the bitstring's length. #[derive(Clone, Debug)] -pub struct BitstringAccumulationTable { +pub struct BitstringTable { /// Fixed column that is enabled only for the first row. pub q_first: Column, /// The byte offset of byte_1. @@ -102,7 +102,7 @@ pub struct BitstringAccumulationTable { pub is_padding: Column, } -impl BitstringAccumulationTable { +impl BitstringTable { /// Construct the bitstring accumulation table. pub fn configure(meta: &mut ConstraintSystem) -> Self { let config = Self { @@ -365,6 +365,19 @@ impl BitstringAccumulationTable { }, ); + meta.create_gate("BitstringTable: first row", |meta| { + let condition = meta.query_fixed(config.q_first, Rotation::cur()); + + let mut cb = BaseConstraintBuilder::default(); + + cb.require_zero( + "cannot start with padding", + meta.query_advice(config.is_padding, Rotation::cur()), + ); + + cb.gate(condition) + }); + meta.create_gate("BitstringAccumulationTable: padding", |meta| { let condition = not::expr(meta.query_fixed(config.q_first, Rotation::cur())); @@ -384,6 +397,8 @@ impl BitstringAccumulationTable { cb.gate(condition) }); + debug_assert!(meta.degree() <= 9); + config } @@ -399,7 +414,7 @@ impl BitstringAccumulationTable { } } -impl LookupTable for BitstringAccumulationTable { +impl LookupTable for BitstringTable { fn columns(&self) -> Vec> { vec![ self.byte_idx_1.into(), @@ -414,6 +429,7 @@ impl LookupTable for BitstringAccumulationTable { self.from_start.into(), self.until_end.into(), self.is_reverse.into(), + self.is_padding.into(), ] } @@ -431,6 +447,7 @@ impl LookupTable for BitstringAccumulationTable { String::from("from_start"), String::from("until_end"), String::from("is_reverse"), + String::from("is_padding"), ] } } diff --git a/aggregator/src/aggregation/decoder/tables/fse.rs b/aggregator/src/aggregation/decoder/tables/fse.rs new file mode 100644 index 0000000000..27c7ce40f5 --- /dev/null +++ b/aggregator/src/aggregation/decoder/tables/fse.rs @@ -0,0 +1,496 @@ +use gadgets::{ + comparator::{ComparatorChip, ComparatorConfig}, + is_equal::{IsEqualChip, IsEqualConfig}, + util::{and, not, select, Expr}, +}; +use halo2_proofs::{ + halo2curves::bn256::Fr, + plonk::{Advice, Column, ConstraintSystem, Expression, Fixed, VirtualCells}, + poly::Rotation, +}; +use itertools::Itertools; +use zkevm_circuits::{ + evm_circuit::{BaseConstraintBuilder, ConstrainBuilderCommon}, + table::{BitwiseOp, BitwiseOpTable, LookupTable, Pow2Table, RangeTable, U8Table}, +}; + +/// An auxiliary table used to ensure that the FSE table was reconstructed appropriately. Contrary +/// to the FseTable where the state is incremental, in the Auxiliary table we club together rows by +/// symbol. Which means, we will have rows with symbol s0 (and varying, but not necessarily +/// incremental states) clubbed together, followed by symbol s1 and so on. +/// +/// | State | Symbol | Baseline | Nb | Baseline Mark | +/// |-------|--------|----------|-----|---------------| +/// | 0x00 | s0 | ... | ... | 0 | <- q_start +/// | 0x01 | s0 | ... | ... | 0 | +/// | 0x02 | s0 | ... | ... | 0 | +/// | ... | s0 | ... | ... | ... | +/// | 0x1d | s0 | ... | ... | 0 | +/// | 0x03 | s1 -> | 0x10 | ... | 0 | +/// | 0x0c | s1 -> | 0x18 | ... | 0 | +/// | 0x11 | s1 -> | 0x00 | ... | 1 | +/// | 0x15 | s1 -> | 0x04 | ... | 1 | +/// | 0x1a | s1 -> | 0x08 | ... | 1 | +/// | 0x1e | s1 -> | 0x0c | ... | 1 | +/// | 0x08 | s2 | ... | ... | 0 | +/// | ... | ... | ... | ... | 0 | +/// | 0x09 | s6 | ... | ... | 0 | +/// | 0x00 | 0 | 0 | 0 | 0 | <- is_padding +/// | ... | ... | ... | ... | ... | <- is_padding +/// | 0x00 | 0 | 0 | 0 | 0 | <- is_padding +/// +/// Above is a representation of this table. Primarily we are interested in verifying that: +/// - next state (for the same symbol) was assigned correctly +/// - the number of times this symbol appears is assigned correctly +/// +/// For more details, refer the [FSE reconstruction][doclink] section. +/// +/// [doclink]: https://nigeltao.github.io/blog/2022/zstandard-part-5-fse.html#fse-reconstruction +#[derive(Clone, Debug)] +pub struct FseTable { + /// Fixed column to mark the first row of the FSE table layout. We reserve the first row to + /// populate all 0s. q_start=1 starts from the second row onwards. + q_first: Column, + /// Fixed column to mark the start of a new FSE table. FSE tables for LLT, MOT and MLT have a + /// maximum possible accuracy log of AL=9, i.e. we will have at the most 2^9=256 states in the + /// FSE table. From the second row onwards, every 256th row will be marked with q_start=1 to + /// indicate the start of a new FSE table. Within an FSE table, we will only have rows up to + /// table_size (1 << AL), and the rest of the rows will be marked with is_padding=1. + q_start: Column, + /// Boolean column to mark whether the row is a padded row. + is_padding: Column, + /// The byte_idx at which the FSE table's decoding started in the encoded data. + byte_offset: Column, + /// The size of the FSE table. + table_size: Column, + /// Helper column for (table_size >> 1). + table_size_rs_1: Column, + /// Helper column for (table_size >> 3). + table_size_rs_3: Column, + /// The FSE symbol, starting at symbol=0. + symbol: Column, + /// Helper gadget to know whether the symbol is the same or not. + symbol_cmp: ComparatorConfig, + /// Boolean column to tell us when symbol is changing. + is_symbol_change: Column, + /// Represents the number of times this symbol appears in the FSE table. This value does not + /// change while the symbol in the table remains the same. + symbol_count: Column, + /// An accumulator that resets to 1 each time we encounter a new symbol in the FSE table. + /// It increments while the symbol remains the same. At the row where we encounter a symbol + /// change, such that: symbol' != symbol, we have: symbol_count == symbol_count_acc. + symbol_count_acc: Column, + /// The state in FSE. In the Auxiliary table, it does not increment by 1. Instead, it follows: + /// - state'' == state + table_size_rs_1 + table_size_rs_3 + 3 + /// - state' == state'' & (table_size - 1) + /// + /// where state' is the next row's state. + state: Column, + /// Denotes the baseline field. + baseline: Column, + /// Helper gadget to compute whether baseline==0x00. + baseline_0x00: IsEqualConfig, + /// Helper column to mark the baseline observed at the last state allocated to a symbol. + last_baseline: Column, + /// The number of bits to be read from bitstream at this state. + nb: Column, + /// The smaller power of two assigned to this state. The following must hold: + /// - 2 ^ nb == SPoT. + spot: Column, + /// An accumulator over SPoT value. + spot_acc: Column, + /// Helper column to remember the smallest spot for that symbol. + smallest_spot: Column, + /// Helper boolean column which is set only from baseline == 0x00. + baseline_mark: Column, +} + +impl FseTable { + /// Configure the FSE table. + pub fn configure( + meta: &mut ConstraintSystem, + u8_table: U8Table, + range8_table: RangeTable<8>, + pow2_table: Pow2Table<20>, + bitwise_op_table: BitwiseOpTable, + ) -> Self { + let (is_padding, symbol, baseline) = ( + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + ); + let config = Self { + q_first: meta.fixed_column(), + q_start: meta.fixed_column(), + is_padding: meta.advice_column(), + byte_offset: meta.advice_column(), + table_size: meta.advice_column(), + table_size_rs_1: meta.advice_column(), + table_size_rs_3: meta.advice_column(), + symbol, + is_symbol_change: meta.advice_column(), + symbol_cmp: ComparatorChip::configure( + meta, + |meta| not::expr(meta.query_advice(is_padding, Rotation::prev())), + |meta| meta.query_advice(symbol, Rotation::prev()), + |meta| meta.query_advice(symbol, Rotation::cur()), + u8_table.into(), + ), + symbol_count: meta.advice_column(), + symbol_count_acc: meta.advice_column(), + state: meta.advice_column(), + baseline, + baseline_0x00: IsEqualChip::configure( + meta, + |meta| not::expr(meta.query_advice(is_padding, Rotation::cur())), + |meta| meta.query_advice(baseline, Rotation::cur()), + |_| 0.expr(), + ), + last_baseline: meta.advice_column(), + nb: meta.advice_column(), + spot: meta.advice_column(), + spot_acc: meta.advice_column(), + smallest_spot: meta.advice_column(), + baseline_mark: meta.advice_column(), + }; + + meta.lookup_any("FseTable: spot == 1 << nb", |meta| { + let condition = not::expr(meta.query_advice(config.is_padding, Rotation::cur())); + + [ + meta.query_advice(config.nb, Rotation::cur()), + meta.query_advice(config.spot, Rotation::cur()), + ] + .into_iter() + .zip_eq(pow2_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }); + + meta.lookup("FseTable: table_size >> 3", |meta| { + // We only check on the starting row. We have a custom gate to check that the + // table_size_rs_3 column's value does not change over the rest of the rows for a + // particular instance of FSE table. + let condition = and::expr([ + meta.query_fixed(config.q_start, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let range_value = meta.query_advice(config.table_size, Rotation::cur()) + - (meta.query_advice(config.table_size_rs_3, Rotation::cur()) * 8.expr()); + + vec![(condition * range_value, range8_table.into())] + }); + + meta.lookup("FseTable: symbol in [0, 256)", |meta| { + vec![( + meta.query_advice(config.symbol, Rotation::cur()), + u8_table.into(), + )] + }); + + meta.create_gate("FseTable: start row", |meta| { + let condition = and::expr([ + meta.query_fixed(config.q_start, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + cb.require_zero( + "state inits at 0", + meta.query_advice(config.state, Rotation::cur()), + ); + + // table_size_rs_1 == table_size >> 1. + cb.require_boolean( + "table_size >> 1", + meta.query_advice(config.table_size, Rotation::cur()) + - (meta.query_advice(config.table_size_rs_1, Rotation::cur()) * 2.expr()), + ); + + // The start row is a new symbol. + cb.require_equal( + "is_symbol_change == 1", + meta.query_advice(config.is_symbol_change, Rotation::cur()), + 1.expr(), + ); + + cb.gate(condition) + }); + + meta.create_gate("FseTable: other rows", |meta| { + let condition = not::expr(meta.query_fixed(config.q_start, Rotation::cur())); + + let mut cb = BaseConstraintBuilder::default(); + + // FSE table's columns that remain unchanged. + for column in [ + config.byte_offset, + config.table_size, + config.table_size_rs_1, + config.table_size_rs_3, + ] { + cb.require_equal( + "FseTable: columns that remain unchanged", + meta.query_advice(column, Rotation::cur()), + meta.query_advice(column, Rotation::prev()), + ); + } + + // If the symbol comparator says that the current symbol is the same as the previous + // symbol, then the current row cannot be marked as a is_symbol_change row. + let (prev_lt_cur, prev_eq_cur) = config.symbol_cmp.expr(meta, Some(Rotation::cur())); + let is_symbol_change = meta.query_advice(config.is_symbol_change, Rotation::cur()); + cb.condition(prev_eq_cur.expr(), |cb| { + cb.require_zero("is_symbol_change == 0", is_symbol_change.expr()); + }); + cb.condition(prev_lt_cur.expr(), |cb| { + cb.require_equal("is_symbol_change == 1", is_symbol_change.expr(), 1.expr()); + }); + + // If symbol is changing on the current row, then the symbol has increased from the + // previous row. + cb.condition(is_symbol_change.expr(), |cb| { + cb.require_equal("symbol::prev < symbol::cur", prev_lt_cur, 1.expr()); + }); + cb.condition(not::expr(is_symbol_change.expr()), |cb| { + cb.require_equal("symbol::prev == symbol::cur", prev_eq_cur, 1.expr()); + }); + + // Once we enter padding territory, we stay in padding territory, i.e. + // is_padding transitions from 0 -> 1 only once. + let (is_padding_curr, is_padding_prev) = ( + meta.query_advice(config.is_padding, Rotation::cur()), + meta.query_advice(config.is_padding, Rotation::prev()), + ); + let is_padding_delta = is_padding_curr - is_padding_prev; + cb.require_boolean("is_padding_delta is boolean", is_padding_delta); + + cb.gate(condition) + }); + + meta.create_gate("FseTable: symbol changes", |meta| { + let condition = and::expr([ + meta.query_advice(config.is_symbol_change, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // We first do validations for the previous symbol. + // + // - symbol_count_acc accumulated to symbol_count. + // - spot_acc accumulated to table_size. + // - the last state has the smallest spot value. + // - the last state's baseline is in fact last_baseline. + cb.require_equal( + "symbol_count == symbol_count_acc", + meta.query_advice(config.symbol_count, Rotation::prev()), + meta.query_advice(config.symbol_count_acc, Rotation::prev()), + ); + cb.require_equal( + "spot_acc == table_size", + meta.query_advice(config.spot_acc, Rotation::prev()), + meta.query_advice(config.table_size, Rotation::prev()), + ); + cb.require_equal( + "spot == smallest_spot", + meta.query_advice(config.spot, Rotation::prev()), + meta.query_advice(config.smallest_spot, Rotation::prev()), + ); + cb.require_equal( + "baseline == last_baseline", + meta.query_advice(config.baseline, Rotation::prev()), + meta.query_advice(config.last_baseline, Rotation::prev()), + ); + + // When the symbol changes, we wish to check in case the baseline==0x00 or not. If it + // is, then the baseline_mark should be turned on from this row onwards (while the + // symbol continues). If it is not, the baseline_mark should stay turned off until we + // encounter baseline==0x00. + let is_baseline_mark = meta.query_advice(config.baseline_mark, Rotation::cur()); + let is_baseline_0x00 = config.baseline_0x00.expr(); + cb.condition(is_baseline_0x00.expr(), |cb| { + cb.require_equal( + "baseline_mark set at baseline==0x00", + is_baseline_mark.expr(), + 1.expr(), + ); + }); + cb.condition(not::expr(is_baseline_0x00.expr()), |cb| { + cb.require_zero( + "baseline_mark not set at baseline!=0x00", + is_baseline_mark.expr(), + ); + }); + + // We repeat the above constraints to make sure witness to baseline mark are set + // correctly. + // + // When a symbol changes and the baseline is not marked, then the baseline is + // calculated from the baseline and nb at the last state allocated to this symbol. + cb.condition(is_baseline_mark.expr(), |cb| { + cb.require_zero( + "baseline=0x00 at baseline mark", + meta.query_advice(config.baseline, Rotation::cur()), + ); + }); + cb.condition(not::expr(is_baseline_mark.expr()), |cb| { + cb.require_equal( + "baseline == last_baseline + smallest_spot", + meta.query_advice(config.baseline, Rotation::cur()), + meta.query_advice(config.last_baseline, Rotation::cur()) + + meta.query_advice(config.smallest_spot, Rotation::cur()), + ); + }); + + // The spot accumulation inits at spot. + cb.require_equal( + "spot_acc == spot", + meta.query_advice(config.spot_acc, Rotation::cur()), + meta.query_advice(config.spot, Rotation::cur()), + ); + + // The symbol_count_acc inits at 1. + cb.require_equal( + "symbol_count_acc inits at 1", + meta.query_advice(config.symbol_count_acc, Rotation::cur()), + 1.expr(), + ); + + cb.gate(condition) + }); + + meta.create_gate("FseTable: symbol continues", |meta| { + let condition = and::expr([ + not::expr(meta.query_advice(config.is_symbol_change, Rotation::cur())), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // While we allocate more states to the same symbol: + // + // - symbol_count does not change + // - smallest_spot does not change + // - last_baseline does not change + // - symbol_count_acc increments by +1 + // - spot_acc accumlates based on the current spot + // - baseline_mark can transition from 0 -> 1 only once + // - baseline==0x00 if baseline_mark is set + // - baseline==baseline::prev+spot::prev if baseline_mark is not set + for column in [ + config.symbol_count, + config.smallest_spot, + config.last_baseline, + ] { + cb.require_equal( + "unchanged columns", + meta.query_advice(column, Rotation::cur()), + meta.query_advice(column, Rotation::prev()), + ); + } + + cb.require_equal( + "symbol_count_acc increments", + meta.query_advice(config.symbol_count_acc, Rotation::cur()), + meta.query_advice(config.symbol_count_acc, Rotation::prev()) + 1.expr(), + ); + + cb.require_equal( + "spot_acc accumlates", + meta.query_advice(config.spot_acc, Rotation::cur()), + meta.query_advice(config.spot_acc, Rotation::prev()) + + meta.query_advice(config.spot, Rotation::cur()), + ); + + let (baseline_mark_curr, baseline_mark_prev) = ( + meta.query_advice(config.baseline_mark, Rotation::cur()), + meta.query_advice(config.baseline_mark, Rotation::prev()), + ); + let baseline_mark_delta = baseline_mark_curr.expr() - baseline_mark_prev; + cb.require_boolean("baseline_mark_delta is boolean", baseline_mark_delta); + + // baseline == baseline_mark_curr == 1 ? 0x00 : baseline_prev + spot_prev + let (baseline_curr, baseline_prev, spot_prev) = ( + meta.query_advice(config.baseline, Rotation::cur()), + meta.query_advice(config.baseline, Rotation::prev()), + meta.query_advice(config.spot, Rotation::prev()), + ); + cb.require_equal( + "baseline calculation", + baseline_curr, + select::expr(baseline_mark_curr, 0x00.expr(), baseline_prev + spot_prev), + ); + + cb.gate(condition) + }); + + // Constraint for state' calculation. We wish to constrain: + // + // - state' == state'' & (table_size - 1) + // - state'' == state + (table_size >> 3) + (table_size >> 1) + 3 + meta.lookup_any("FseTable: state transition", |meta| { + let condition = and::expr([ + not::expr(meta.query_fixed(config.q_start, Rotation::cur())), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let state_prime = meta.query_advice(config.state, Rotation::cur()); + let state_prime_prime = meta.query_advice(config.state, Rotation::prev()) + + meta.query_advice(config.table_size_rs_3, Rotation::cur()) + + meta.query_advice(config.table_size_rs_1, Rotation::cur()) + + 3.expr(); + let table_size_minus_one = + meta.query_advice(config.table_size, Rotation::cur()) - 1.expr(); + + [ + BitwiseOp::AND.expr(), // op + state_prime_prime, // operand1 + table_size_minus_one, // operand2 + state_prime, // result + ] + .into_iter() + .zip_eq(bitwise_op_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }); + + debug_assert!(meta.degree() <= 9); + + config + } +} + +impl FseTable { + /// Lookup table expressions for (state, symbol, baseline, nb) tuple check. + /// + /// This check can be done on any row within the FSE table. + pub fn table_exprs_by_state(&self, meta: &mut VirtualCells) -> Vec> { + vec![ + meta.query_advice(self.byte_offset, Rotation::cur()), + meta.query_advice(self.table_size, Rotation::cur()), + meta.query_advice(self.state, Rotation::cur()), + meta.query_advice(self.symbol, Rotation::cur()), + meta.query_advice(self.baseline, Rotation::cur()), + meta.query_advice(self.nb, Rotation::cur()), + meta.query_advice(self.is_padding, Rotation::cur()), + ] + } + + /// Lookup table expressions for (symbol, symbol_count) tuple check. + /// + /// This check is only done on the last occurence of a particular symbol, i.e. where: + /// - symbol_count == symbol_count_acc + pub fn table_exprs_by_symbol(&self, meta: &mut VirtualCells) -> Vec> { + vec![ + meta.query_advice(self.byte_offset, Rotation::cur()), + meta.query_advice(self.table_size, Rotation::cur()), + meta.query_advice(self.symbol, Rotation::cur()), + meta.query_advice(self.symbol_count, Rotation::cur()), + meta.query_advice(self.symbol_count_acc, Rotation::cur()), + meta.query_advice(self.is_padding, Rotation::cur()), + ] + } +} diff --git a/aggregator/src/aggregation/decoder/tables/literals_header.rs b/aggregator/src/aggregation/decoder/tables/literals_header.rs index 8bb7ca3803..0f9ed53bab 100644 --- a/aggregator/src/aggregation/decoder/tables/literals_header.rs +++ b/aggregator/src/aggregation/decoder/tables/literals_header.rs @@ -111,6 +111,8 @@ impl LiteralsHeaderTable { vec![(condition * range_value, range16.into())] }); + debug_assert!(meta.degree() <= 9); + config } } diff --git a/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs b/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs new file mode 100644 index 0000000000..3778134291 --- /dev/null +++ b/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs @@ -0,0 +1,121 @@ +use halo2_proofs::{ + circuit::{Layouter, Value}, + halo2curves::bn256::Fr, + plonk::{Column, ConstraintSystem, Error, Fixed}, +}; +use zkevm_circuits::table::LookupTable; + +use crate::aggregation::decoder::witgen::ZstdTag::{ + // TODO: update to the correct tags once witgen code is merged. + ZstdBlockFseCode as ZstdBlockSequenceFseCode, + ZstdBlockLstream as ZstdBlockSequenceData, + ZstdBlockSequenceHeader, +}; + +/// Read-only table that allows us to check the correct assignment of FSE table kind. +/// +/// The possible orders are: +/// - [ZstdBlockSequenceHeader, ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, LLT] +/// - [ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, MOT] +/// - [ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, ZstdBlockSequenceData, MLT] +#[derive(Clone, Debug)] +pub struct RomFseOrderTable { + /// The tag that occurred previously. + tag_prev: Column, + /// The current tag, expected to be ZstdBlockSequenceFseCode. + tag_cur: Column, + /// The tag that follows the current tag. + tag_next: Column, + /// The FSE table kind, possible values: LLT=1, MOT=2, MLT=3. + table_kind: Column, +} + +impl RomFseOrderTable { + pub fn construct(meta: &mut ConstraintSystem) -> Self { + Self { + tag_prev: meta.fixed_column(), + tag_cur: meta.fixed_column(), + tag_next: meta.fixed_column(), + table_kind: meta.fixed_column(), + } + } + + /// Load the FSE order ROM table. + pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { + layouter.assign_region( + || "(ROM): FSE order table", + |mut region| { + for (offset, row) in [ + ( + ZstdBlockSequenceHeader, + ZstdBlockSequenceFseCode, + ZstdBlockSequenceFseCode, + 1u64, + ), + ( + ZstdBlockSequenceFseCode, + ZstdBlockSequenceFseCode, + ZstdBlockSequenceFseCode, + 2u64, + ), + ( + ZstdBlockSequenceFseCode, + ZstdBlockSequenceFseCode, + ZstdBlockSequenceData, + 3u64, + ), + ] + .iter() + .enumerate() + { + region.assign_fixed( + || format!("tag_prev at offset={offset}"), + self.tag_prev, + offset, + || Value::known(Fr::from(row.0 as u64)), + )?; + region.assign_fixed( + || format!("tag_cur at offset={offset}"), + self.tag_cur, + offset, + || Value::known(Fr::from(row.1 as u64)), + )?; + region.assign_fixed( + || format!("tag_next at offset={offset}"), + self.tag_next, + offset, + || Value::known(Fr::from(row.2 as u64)), + )?; + region.assign_fixed( + || format!("table_kind at offset={offset}"), + self.table_kind, + offset, + || Value::known(Fr::from(row.3)), + )?; + } + + Ok(()) + }, + ) + } +} + +impl LookupTable for RomFseOrderTable { + fn columns(&self) -> Vec> { + vec![ + self.tag_prev.into(), + self.tag_cur.into(), + self.tag_next.into(), + self.table_kind.into(), + ] + } + + fn annotations(&self) -> Vec { + vec![ + String::from("tag_prev"), + String::from("tag_cur"), + String::from("tag_next"), + String::from("table_kind"), + ] + } +} diff --git a/zkevm-circuits/src/table.rs b/zkevm-circuits/src/table.rs index 3d13d5b1cd..73b556d9a6 100644 --- a/zkevm-circuits/src/table.rs +++ b/zkevm-circuits/src/table.rs @@ -26,7 +26,7 @@ use eth_types::{sign_types::SignData, Field, ToLittleEndian, ToScalar, ToWord, W use ethers_core::utils::keccak256; use gadgets::{ binary_number::{BinaryNumberChip, BinaryNumberConfig}, - util::{and, not, split_u256, split_u256_limb64, Expr}, + util::{and, not, pow_of_two, split_u256, split_u256_limb64, Expr}, }; use halo2_proofs::{ circuit::{AssignedCell, Layouter, Region, Value}, @@ -3187,6 +3187,62 @@ impl From> for TableColumn { } } +/// Lookup table for powers of 2. +#[derive(Clone, Copy, Debug)] +pub struct Pow2Table { + exponent: Column, + exponentiation: Column, +} + +impl Pow2Table { + /// Construct the Pow2 table. + pub fn construct(meta: &mut ConstraintSystem) -> Self { + Self { + exponent: meta.fixed_column(), + exponentiation: meta.fixed_column(), + } + } + + /// Assign values to the Pow2 table. + pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { + layouter.assign_region( + || "Pow2 table", + |mut region| { + for i in 0..N { + let exponentiation: F = pow_of_two(i); + region.assign_fixed( + || format!("Pow2: exponent at offset = {i}"), + self.exponent, + i, + || Value::known(F::from(i as u64)), + )?; + region.assign_fixed( + || format!("Pow2: exponentiation at offset = {i}"), + self.exponentiation, + i, + || Value::known(exponentiation), + )?; + } + + Ok(()) + }, + ) + } +} + +impl LookupTable for Pow2Table { + fn columns(&self) -> Vec> { + vec![self.exponent.into(), self.exponentiation.into()] + } + + fn annotations(&self) -> Vec { + vec![ + String::from("pow2table: exponent"), + String::from("pow2table: exponentiation"), + ] + } +} + #[derive(Clone, Copy, Debug)] /// Bitwise operation types. pub enum BitwiseOp {