From dc8db813ec830331848567ef05add831af55094a Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Mon, 29 Apr 2024 10:59:28 +0100 Subject: [PATCH 1/5] fix: tag_idx == tag_len check on prev row --- aggregator/src/aggregation/decoder.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 1005241b17..400d372180 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -884,8 +884,15 @@ impl DecoderConfig { // If the previous tag was done processing, verify that the is_change boolean was // set. - let tag_idx_eq_tag_len = config.tag_config.tag_idx_eq_tag_len.expr(); - cb.condition(and::expr([byte_idx_delta, tag_idx_eq_tag_len]), |cb| { + let tag_idx_prev = meta.query_advice(config.tag_config.tag_idx, Rotation::prev()); + let tag_len_prev = meta.query_advice(config.tag_config.tag_len, Rotation::prev()); + let tag_idx_eq_tag_len_prev = config.tag_config.tag_idx_eq_tag_len.expr_at( + meta, + Rotation::prev(), + tag_idx_prev, + tag_len_prev, + ); + cb.condition(and::expr([byte_idx_delta, tag_idx_eq_tag_len_prev]), |cb| { cb.require_equal( "is_change is set", meta.query_advice(config.tag_config.is_change, Rotation::cur()), From 20ecb5f8bfdb633e434b4cefb77055e233f6b82c Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Mon, 29 Apr 2024 11:00:50 +0100 Subject: [PATCH 2/5] impr: literals header table to use block_idx --- aggregator/src/aggregation/decoder.rs | 3 +- .../decoder/tables/literals_header.rs | 60 +++++++++++++++++-- 2 files changed, 57 insertions(+), 6 deletions(-) diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 400d372180..4319d7d0c6 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -1485,8 +1485,9 @@ impl DecoderConfig { ), ); + let block_idx = meta.query_advice(config.block_config.block_idx, Rotation::cur()); [ - meta.query_advice(config.byte_idx, Rotation::cur()), + block_idx, byte0, byte1, byte2, diff --git a/aggregator/src/aggregation/decoder/tables/literals_header.rs b/aggregator/src/aggregation/decoder/tables/literals_header.rs index 0f9ed53bab..8760d5d1b3 100644 --- a/aggregator/src/aggregation/decoder/tables/literals_header.rs +++ b/aggregator/src/aggregation/decoder/tables/literals_header.rs @@ -1,7 +1,7 @@ use gadgets::util::{not, select, Expr}; use halo2_proofs::{ halo2curves::bn256::Fr, - plonk::{Advice, Any, Column, ConstraintSystem}, + plonk::{Advice, Any, Column, ConstraintSystem, Fixed}, poly::Rotation, }; use zkevm_circuits::{ @@ -12,8 +12,12 @@ use zkevm_circuits::{ /// Helper table to decode the regenerated size from the Literals Header. #[derive(Clone, Debug)] pub struct LiteralsHeaderTable { - /// The byte_idx at which this literals header is located. - pub byte_offset: Column, + /// Fixed column to mark the first row of the table. + q_first: Column, + /// The block index in which we find this literals header. Since every block will have a + /// literals header, and block_idx in 1..=n, we know that on the first row block_idx=1 and on + /// subsequent rows, block_idx increments by 1. + pub block_idx: Column, /// The first byte of the literals header. pub byte0: Column, /// The second byte. @@ -42,7 +46,8 @@ impl LiteralsHeaderTable { range16: RangeTable<16>, ) -> Self { let config = Self { - byte_offset: meta.advice_column(), + q_first: meta.fixed_column(), + block_idx: meta.advice_column(), byte0: meta.advice_column(), byte1: meta.advice_column(), byte2: meta.advice_column(), @@ -54,6 +59,25 @@ impl LiteralsHeaderTable { is_padding: meta.advice_column(), }; + meta.create_gate("LiteralsHeaderTable: first row", |meta| { + let condition = meta.query_fixed(config.q_first, Rotation::cur()); + + let mut cb = BaseConstraintBuilder::default(); + + cb.require_zero( + "is_padding=0 on first row", + meta.query_advice(config.is_padding, Rotation::cur()), + ); + + cb.require_equal( + "block_idx=1 on first row", + meta.query_advice(config.block_idx, Rotation::cur()), + 1.expr(), + ); + + cb.gate(condition) + }); + meta.create_gate("LiteralsHeaderTable: main gate", |meta| { let condition = not::expr(meta.query_advice(config.is_padding, Rotation::cur())); @@ -93,6 +117,31 @@ impl LiteralsHeaderTable { cb.gate(condition) }); + meta.create_gate("LiteralsHeaderTable: padding check", |meta| { + let condition = not::expr(meta.query_fixed(config.q_first, Rotation::cur())); + + let mut cb = BaseConstraintBuilder::default(); + + // padding transitions from 0 -> 1 only once. + let is_padding_cur = meta.query_advice(config.is_padding, Rotation::cur()); + let is_padding_prev = meta.query_advice(config.is_padding, Rotation::prev()); + let is_padding_delta = is_padding_cur.expr() - is_padding_prev; + + cb.require_boolean("is_padding is boolean", is_padding_cur.expr()); + cb.require_boolean("is_padding delta is boolean", is_padding_delta); + + // if this is not a padding row, then block_idx has incremented. + cb.condition(not::expr(is_padding_cur), |cb| { + cb.require_equal( + "block_idx increments by 1", + meta.query_advice(config.block_idx, Rotation::cur()), + meta.query_advice(config.block_idx, Rotation::prev()) + 1.expr(), + ); + }); + + cb.gate(condition) + }); + meta.lookup("LiteralsHeaderTable: byte0 >> 3", |meta| { let condition = 1.expr(); @@ -120,7 +169,7 @@ impl LiteralsHeaderTable { impl LookupTable for LiteralsHeaderTable { fn columns(&self) -> Vec> { vec![ - self.byte_offset.into(), + self.block_idx.into(), self.byte0.into(), self.byte1.into(), self.byte2.into(), @@ -133,6 +182,7 @@ impl LookupTable for LiteralsHeaderTable { fn annotations(&self) -> Vec { vec![ + String::from("block_idx"), String::from("byte_offset"), String::from("byte0"), String::from("byte1"), From 5cce61c86e9ff30a48f705a311886b6be943cdef Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Mon, 29 Apr 2024 12:02:57 +0100 Subject: [PATCH 3/5] impr: fse table also uses (block_idx, table_kind) identifier --- aggregator/src/aggregation/decoder.rs | 8 +- .../src/aggregation/decoder/tables/fse.rs | 116 ++++++++++++++- .../decoder/tables/rom_fse_order.rs | 139 +++++++++++++++++- 3 files changed, 247 insertions(+), 16 deletions(-) diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 4319d7d0c6..271feb61ae 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -1899,8 +1899,9 @@ impl DecoderConfig { ), ]); - let (fse_byte_offset, fse_table_size, fse_symbol, bitstring_value) = ( - meta.query_advice(config.fse_decoder.byte_offset, Rotation::cur()), + let (block_idx, fse_table_kind, fse_table_size, fse_symbol, bitstring_value) = ( + meta.query_advice(config.block_config.block_idx, Rotation::cur()), + meta.query_advice(config.fse_decoder.table_kind, 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()), @@ -1908,7 +1909,8 @@ impl DecoderConfig { let norm_prob = bitstring_value - 1.expr(); [ - fse_byte_offset, + block_idx, + fse_table_kind, fse_table_size, fse_symbol, norm_prob.expr(), diff --git a/aggregator/src/aggregation/decoder/tables/fse.rs b/aggregator/src/aggregation/decoder/tables/fse.rs index 27c7ce40f5..4e47e728ac 100644 --- a/aggregator/src/aggregation/decoder/tables/fse.rs +++ b/aggregator/src/aggregation/decoder/tables/fse.rs @@ -14,6 +14,8 @@ use zkevm_circuits::{ table::{BitwiseOp, BitwiseOpTable, LookupTable, Pow2Table, RangeTable, U8Table}, }; +use crate::aggregation::decoder::tables::rom_fse_order::{FseTableKind, RomFseTableTransition}; + /// 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 @@ -59,14 +61,18 @@ pub struct FseTable { 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 block index in which this FSE table is found. + block_idx: Column, + /// The table kind, i.e. LLT=1, MOT=2 or MLT=3. + table_kind: 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, + /// Incremental index given to a state, idx in 1..=table_size. + idx: Column, /// The FSE symbol, starting at symbol=0. symbol: Column, /// Helper gadget to know whether the symbol is the same or not. @@ -103,6 +109,8 @@ pub struct FseTable { smallest_spot: Column, /// Helper boolean column which is set only from baseline == 0x00. baseline_mark: Column, + /// ROM table for verifying FSE table kind and block_idx transition. + rom_fse_transition: RomFseTableTransition, } impl FseTable { @@ -114,6 +122,9 @@ impl FseTable { pow2_table: Pow2Table<20>, bitwise_op_table: BitwiseOpTable, ) -> Self { + // Fixed table to check the transition of table kinds and block idx. + let rom_fse_transition = RomFseTableTransition::construct(meta); + let (is_padding, symbol, baseline) = ( meta.advice_column(), meta.advice_column(), @@ -123,10 +134,12 @@ impl FseTable { q_first: meta.fixed_column(), q_start: meta.fixed_column(), is_padding: meta.advice_column(), - byte_offset: meta.advice_column(), + block_idx: meta.advice_column(), + table_kind: meta.advice_column(), table_size: meta.advice_column(), table_size_rs_1: meta.advice_column(), table_size_rs_3: meta.advice_column(), + idx: meta.advice_column(), symbol, is_symbol_change: meta.advice_column(), symbol_cmp: ComparatorChip::configure( @@ -152,6 +165,7 @@ impl FseTable { spot_acc: meta.advice_column(), smallest_spot: meta.advice_column(), baseline_mark: meta.advice_column(), + rom_fse_transition, }; meta.lookup_any("FseTable: spot == 1 << nb", |meta| { @@ -189,6 +203,57 @@ impl FseTable { )] }); + meta.create_gate("FseTable: first row", |meta| { + let condition = meta.query_fixed(config.q_first, Rotation::cur()); + + let mut cb = BaseConstraintBuilder::default(); + + // The first row is all 0s. This is then followed by a q_start==1 fixed column. We want + // to make sure the first FSE table belongs to block_idx=1. + cb.require_equal( + "block_idx == 1 for the first FSE table", + meta.query_advice(config.block_idx, Rotation::next()), + 1.expr(), + ); + + // The first FSE table described should be the LLT table. + cb.require_equal( + "table_kind == LLT for the first FSE table", + meta.query_advice(config.table_kind, Rotation::next()), + FseTableKind::LLT.expr(), + ); + + cb.gate(condition) + }); + + meta.lookup_any( + "FseTable: start row (FSE table kind and block_idx transition)", + |meta| { + let condition = and::expr([ + meta.query_fixed(config.q_start, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let (block_idx_prev, block_idx_curr, table_kind_prev, table_kind_curr) = ( + meta.query_advice(config.block_idx, Rotation::prev()), + meta.query_advice(config.block_idx, Rotation::cur()), + meta.query_advice(config.table_kind, Rotation::prev()), + meta.query_advice(config.table_kind, Rotation::cur()), + ); + + [ + block_idx_prev, + block_idx_curr, + table_kind_prev, + table_kind_curr, + ] + .into_iter() + .zip_eq(config.rom_fse_transition.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + meta.create_gate("FseTable: start row", |meta| { let condition = and::expr([ meta.query_fixed(config.q_start, Rotation::cur()), @@ -202,6 +267,12 @@ impl FseTable { meta.query_advice(config.state, Rotation::cur()), ); + cb.require_equal( + "idx == 1", + meta.query_advice(config.idx, Rotation::cur()), + 1.expr(), + ); + // table_size_rs_1 == table_size >> 1. cb.require_boolean( "table_size >> 1", @@ -219,14 +290,15 @@ impl FseTable { cb.gate(condition) }); - meta.create_gate("FseTable: other rows", |meta| { + meta.create_gate("FseTable: other rows in the same FSE table", |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.block_idx, + config.table_kind, config.table_size, config.table_size_rs_1, config.table_size_rs_3, @@ -264,9 +336,33 @@ impl FseTable { 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; + let is_padding_delta = is_padding_curr.expr() - is_padding_prev.expr(); + cb.require_boolean("is_padding is boolean", is_padding_curr.expr()); cb.require_boolean("is_padding_delta is boolean", is_padding_delta); + // While we have not entered the padding region in this table, the idx should + // increment. + cb.condition(not::expr(is_padding_curr.expr()), |cb| { + cb.require_equal( + "idx increments", + meta.query_advice(config.idx, Rotation::cur()), + meta.query_advice(config.idx, Rotation::prev()) + 1.expr(), + ); + }); + + // If we are entering the padding region on this row, the idx on the previous row must + // equal the table size, i.e. all states must be generated. + cb.condition( + and::expr([not::expr(is_padding_prev), is_padding_curr]), + |cb| { + cb.require_equal( + "idx == table_size on the last state", + meta.query_advice(config.idx, Rotation::prev()), + meta.query_advice(config.table_size, Rotation::prev()), + ); + }, + ); + cb.gate(condition) }); @@ -469,7 +565,9 @@ impl FseTable { /// 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_fixed(self.q_first, Rotation::cur()), + meta.query_advice(self.block_idx, Rotation::cur()), + meta.query_advice(self.table_kind, Rotation::cur()), meta.query_advice(self.table_size, Rotation::cur()), meta.query_advice(self.state, Rotation::cur()), meta.query_advice(self.symbol, Rotation::cur()), @@ -485,7 +583,9 @@ impl FseTable { /// - 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_fixed(self.q_first, Rotation::cur()), + meta.query_advice(self.block_idx, Rotation::cur()), + meta.query_advice(self.table_kind, 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()), diff --git a/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs b/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs index 3778134291..67a4cd5c2c 100644 --- a/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs +++ b/aggregator/src/aggregation/decoder/tables/rom_fse_order.rs @@ -1,7 +1,9 @@ +use eth_types::Field; +use gadgets::impl_expr; use halo2_proofs::{ circuit::{Layouter, Value}, halo2curves::bn256::Fr, - plonk::{Column, ConstraintSystem, Error, Fixed}, + plonk::{Column, ConstraintSystem, Error, Expression, Fixed}, }; use zkevm_circuits::table::LookupTable; @@ -12,6 +14,20 @@ use crate::aggregation::decoder::witgen::ZstdTag::{ ZstdBlockSequenceHeader, }; +/// FSE table variants that we observe in the sequences section. +#[derive(Clone, Copy)] +#[allow(clippy::upper_case_acronyms)] +pub enum FseTableKind { + /// Literal length FSE table. + LLT = 1, + /// Match offset FSE table. + MOT, + /// Match length FSE table. + MLT, +} + +impl_expr!(FseTableKind); + /// Read-only table that allows us to check the correct assignment of FSE table kind. /// /// The possible orders are: @@ -50,19 +66,19 @@ impl RomFseOrderTable { ZstdBlockSequenceHeader, ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, - 1u64, + FseTableKind::LLT, ), ( ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, - 2u64, + FseTableKind::MOT, ), ( ZstdBlockSequenceFseCode, ZstdBlockSequenceFseCode, ZstdBlockSequenceData, - 3u64, + FseTableKind::MLT, ), ] .iter() @@ -90,7 +106,7 @@ impl RomFseOrderTable { || format!("table_kind at offset={offset}"), self.table_kind, offset, - || Value::known(Fr::from(row.3)), + || Value::known(Fr::from(row.3 as u64)), )?; } @@ -119,3 +135,116 @@ impl LookupTable for RomFseOrderTable { ] } } + +#[derive(Clone, Debug)] +pub struct RomFseTableTransition { + /// The block index on the previous FSE table. + block_idx_prev: Column, + /// The block index on the current FSE table. + block_idx_curr: Column, + /// The FSE table previously decoded. + table_kind_prev: Column, + /// The FSE table currently decoded. + table_kind_curr: Column, +} + +impl RomFseTableTransition { + pub fn construct(meta: &mut ConstraintSystem) -> Self { + Self { + block_idx_prev: meta.fixed_column(), + block_idx_curr: meta.fixed_column(), + table_kind_prev: meta.fixed_column(), + table_kind_curr: meta.fixed_column(), + } + } + + pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { + layouter.assign_region( + || "ROM: fse table transition", + |mut region| { + // assign for the preliminary transition. + region.assign_fixed( + || "block_idx_prev", + self.block_idx_prev, + 0, + || Value::known(Fr::zero()), + )?; + region.assign_fixed( + || "block_idx_curr", + self.block_idx_curr, + 0, + || Value::known(Fr::one()), + )?; + region.assign_fixed( + || "table_kind_prev", + self.table_kind_prev, + 0, + || Value::known(Fr::zero()), + )?; + region.assign_fixed( + || "table_kind_curr", + self.table_kind_curr, + 0, + || Value::known(Fr::from(FseTableKind::LLT as u64)), + )?; + + // assign for the other transitons. + for (i, &(block_idx_prev, block_idx_curr, table_kind_prev, table_kind_curr)) in [ + (1, 1, FseTableKind::LLT, FseTableKind::MOT), + (1, 1, FseTableKind::MOT, FseTableKind::MLT), + // TODO: add more for multi-block scenario + ] + .iter() + .enumerate() + { + region.assign_fixed( + || "block_idx_prev", + self.block_idx_prev, + i + 1, + || Value::known(Fr::from(block_idx_prev)), + )?; + region.assign_fixed( + || "block_idx_curr", + self.block_idx_curr, + i + 1, + || Value::known(Fr::from(block_idx_curr)), + )?; + region.assign_fixed( + || "table_kind_prev", + self.table_kind_prev, + i + 1, + || Value::known(Fr::from(table_kind_prev as u64)), + )?; + region.assign_fixed( + || "table_kind_curr", + self.table_kind_curr, + i + 1, + || Value::known(Fr::from(table_kind_curr as u64)), + )?; + } + + Ok(()) + }, + ) + } +} + +impl LookupTable for RomFseTableTransition { + fn columns(&self) -> Vec> { + vec![ + self.block_idx_prev.into(), + self.block_idx_curr.into(), + self.table_kind_prev.into(), + self.table_kind_curr.into(), + ] + } + + fn annotations(&self) -> Vec { + vec![ + String::from("block_idx_prev"), + String::from("block_idx_curr"), + String::from("table_kind_prev"), + String::from("table_kind_curr"), + ] + } +} From 3bab54bbf0ec5d5289ea0b68e43e84c15febfbd7 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Mon, 29 Apr 2024 12:37:06 +0100 Subject: [PATCH 4/5] fix: handle is_nil and is_nb0 separately in bitstrream decoder --- aggregator/src/aggregation/decoder.rs | 592 ++++++++++++++++---------- 1 file changed, 359 insertions(+), 233 deletions(-) diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 271feb61ae..609ee7b863 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -371,15 +371,18 @@ 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 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. + /// Boolean that is set for a special case: + /// - 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, + /// Boolean that is set for a special case: + /// - 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 in the SequencesData tag. + is_nb0: Column, + /// Helper gadget to check when bit_index_start == bit_index_end. + start_eq_end: IsEqualConfig, } impl BitstreamDecoder { @@ -388,10 +391,11 @@ impl BitstreamDecoder { is_padding: Column, u8_table: U8Table, ) -> Self { + let bit_index_start = meta.advice_column(); let bit_index_end = meta.advice_column(); let bitstring_value = meta.advice_column(); Self { - bit_index_start: meta.advice_column(), + bit_index_start, bit_index_end, bit_index_end_cmp_7: ComparatorChip::configure( meta, @@ -428,22 +432,35 @@ impl BitstreamDecoder { |_| 3.expr(), ), is_nil: meta.advice_column(), + is_nb0: meta.advice_column(), + start_eq_end: IsEqualChip::configure( + meta, + |meta| not::expr(meta.query_advice(is_padding, Rotation::cur())), + |meta| meta.query_advice(bit_index_start, Rotation::cur()), + |meta| meta.query_advice(bit_index_end, Rotation::cur()), + ), } } } impl BitstreamDecoder { - /// Whether the number of bits to be read from bitstream (at this row) is 0, i.e. no bits to be - /// read. + /// If we skip reading any bitstring at this row, because of byte-alignment over multiple bytes + /// from the previously read bitstring. 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. + /// If we expect to read a bitstring at this row. fn is_not_nil(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { not::expr(self.is_nil(meta, rotation)) } + /// If the number of bits to be read from the bitstream is nb=0. This scenario occurs in the + /// SequencesData tag section, when we are applying the FSE tables to decode sequences. + fn is_nb0(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { + meta.query_advice(self.is_nb0, 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 { @@ -563,6 +580,16 @@ impl BitstreamDecoder { let (_lt, eq) = self.bit_index_end_cmp_23.expr(meta, rotation); eq } + + /// bit_index_start == bit_index_end. + fn start_eq_end(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { + let (bit_index_start, bit_index_end) = ( + meta.query_advice(self.bit_index_start, Rotation::cur()), + meta.query_advice(self.bit_index_end, Rotation::cur()), + ); + self.start_eq_end + .expr_at(meta, rotation, bit_index_start, bit_index_end) + } } #[derive(Clone, Debug)] @@ -1929,12 +1956,49 @@ impl DecoderConfig { /////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////// 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())]), - ]); + meta.create_gate("DecoderConfig: Bitstream Decoder (is_nil)", |meta| { + // Bitstream decoder when we skip reading a bitstring at a row. + let condition = config.bitstream_decoder.is_nil(meta, Rotation::cur()); + + let mut cb = BaseConstraintBuilder::default(); + + cb.require_zero( + "bit_index_start == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::cur()), + ); + cb.require_zero( + "bit_index_end == 0", + meta.query_advice(config.bitstream_decoder.bit_index_end, Rotation::cur()), + ); + cb.require_zero( + "bit_index_start' == 0", + meta.query_advice(config.bitstream_decoder.bit_index_start, Rotation::next()), + ); + cb.require_equal( + "if is_nil: byte_idx' == byte_idx", + meta.query_advice(config.byte_idx, Rotation::next()), + meta.query_advice(config.byte_idx, Rotation::cur()), + ); + + cb.require_zero( + "if is_nil is True then is_nb0 is False", + config.bitstream_decoder.is_nb0(meta, Rotation::cur()), + ); + cb.require_equal( + "bitstream(is_nil) can occur in [FseCode, SequencesData] tags", + sum::expr([ + meta.query_advice(config.tag_config.is_fse_code, Rotation::cur()), + // TODO: add SequencesData tag once ready. + ]), + 1.expr(), + ); + + cb.gate(condition) + }); + + meta.create_gate("DecoderConfig: Bitstream Decoder (is_nb0)", |meta| { + // Bitstream decoder when we read nb=0 bits from the bitstream. + let condition = config.bitstream_decoder.is_nb0(meta, Rotation::cur()); let mut cb = BaseConstraintBuilder::default(); @@ -1943,246 +2007,306 @@ impl DecoderConfig { 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", + "if is_nb0: byte_idx' == byte_idx", meta.query_advice(config.byte_idx, Rotation::next()), meta.query_advice(config.byte_idx, Rotation::cur()), ); + cb.require_zero( + "if is_nb0 is True then is_nil is False", + config.bitstream_decoder.is_nil(meta, Rotation::cur()), + ); + // TODO: this can only occur in the SequqencesData tag. + // cb.require_equal( + // "bitstream(is_nb0) can occur in SequencesData", + // meta.query_advice(config.tag_config.is_sequences_data, Rotation::cur()), + // 1.expr(), + // ); + 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())]), - ]); + meta.create_gate( + "DecoderConfig: Bitstream Decoder (read from bitstream)", + |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())), + not::expr(config.bitstream_decoder.is_nb0(meta, Rotation::cur())), + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), + ]); - let mut cb = BaseConstraintBuilder::default(); + 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(), - ); - }, - ); + // 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(), - ), - ); - }, - ); + // 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()), - ); - }, - ); + // 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)), - ); - }, - ); + // 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()), - ); - }, - ); + // 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.create_gate("DecoderConfig: Bitstream Decoder", |meta| { + let condition = + sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]); + + let mut cb = BaseConstraintBuilder::default(); - // 6. bitstring is byte-aligned: bit_index_end == 23. cb.condition( - config - .bitstream_decoder - .aligned_three_bytes(meta, Some(Rotation::cur())), + config.bitstream_decoder.start_eq_end(meta, 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)), + "if start == end: is_nil=1 or is_nb0=1", + sum::expr([ + config.bitstream_decoder.is_nil(meta, Rotation::cur()), + config.bitstream_decoder.is_nb0(meta, Rotation::cur()), + ]), 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)), - ); }, ); @@ -2194,6 +2318,7 @@ impl DecoderConfig { |meta| { let condition = and::expr([ not::expr(config.bitstream_decoder.is_nil(meta, Rotation::cur())), + not::expr(config.bitstream_decoder.is_nb0(meta, Rotation::cur())), sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), ]); @@ -2239,6 +2364,7 @@ impl DecoderConfig { meta.lookup_any("DecoderConfig: Bitstream Decoder (bitstring end)", |meta| { let condition = and::expr([ not::expr(config.bitstream_decoder.is_nil(meta, Rotation::cur())), + not::expr(config.bitstream_decoder.is_nb0(meta, Rotation::cur())), sum::expr([meta.query_advice(config.tag_config.is_fse_code, Rotation::cur())]), ]); From 3950a4d344b985bb3a29471d55a4bce50e2e6fb8 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Mon, 29 Apr 2024 12:42:43 +0100 Subject: [PATCH 5/5] fix: add q_first=0 to fse table lookup --- aggregator/src/aggregation/decoder.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index 609ee7b863..49e4d67a0b 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -1936,6 +1936,7 @@ impl DecoderConfig { let norm_prob = bitstring_value - 1.expr(); [ + 0.expr(), // skip first row block_idx, fse_table_kind, fse_table_size,