diff --git a/aggregator/src/aggregation/decoder.rs b/aggregator/src/aggregation/decoder.rs index ce5dcc471c..5ff0d2615f 100644 --- a/aggregator/src/aggregation/decoder.rs +++ b/aggregator/src/aggregation/decoder.rs @@ -371,6 +371,11 @@ pub struct BitstreamDecoder { bit_index_end_cmp_23: ComparatorConfig, /// The value of the binary bitstring. bitstring_value: Column, + /// Helper gadget to know when the bitstring value is 0. This contributes to an edge-case in + /// decoding and reconstructing the FSE table from normalised distributions, where a value=0 + /// implies prob=-1 ("less than 1" probability). In this case, the symbol is allocated a state + /// at the end of the FSE table, with baseline=0x00 and nb=AL, i.e. reset state. + bitstring_value_eq_0: IsEqualConfig, /// Helper gadget to know when the bitstring value is 1 or 3. This is useful in the case /// of decoding/reconstruction of FSE table, where a value=1 implies a special case of /// prob=0, where the symbol is instead followed by a 2-bit repeat flag. The repeat flag @@ -427,6 +432,12 @@ impl BitstreamDecoder { u8_table.into(), ), bitstring_value, + bitstring_value_eq_0: IsEqualChip::configure( + meta, + |meta| not::expr(meta.query_advice(is_padding, Rotation::cur())), + |meta| meta.query_advice(bitstring_value, Rotation::cur()), + |_| 0.expr(), + ), bitstring_value_eq_1: IsEqualChip::configure( meta, |meta| not::expr(meta.query_advice(is_padding, Rotation::cur())), @@ -469,6 +480,22 @@ impl BitstreamDecoder { meta.query_advice(self.is_nb0, rotation) } + /// If we have read a bitstring of length > 0. + fn is_not_nb0(&self, meta: &mut VirtualCells, rotation: Rotation) -> Expression { + not::expr(self.is_nb0(meta, rotation)) + } + + /// If the bitstring value is 0. + fn is_prob_less_than1( + &self, + meta: &mut VirtualCells, + rotation: Rotation, + ) -> Expression { + let bitstring_value = meta.query_advice(self.bitstring_value, rotation); + self.bitstring_value_eq_0 + .expr_at(meta, rotation, bitstring_value, 1.expr()) + } + /// 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 { @@ -2183,7 +2210,14 @@ impl DecoderConfig { 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(); + let is_prob_less_than1 = config + .bitstream_decoder + .is_prob_less_than1(meta, Rotation::cur()); + let norm_prob = select::expr( + is_prob_less_than1.expr(), + 1.expr(), + bitstring_value - 1.expr(), + ); [ 0.expr(), // skip first row @@ -2193,6 +2227,7 @@ impl DecoderConfig { fse_symbol, norm_prob.expr(), norm_prob.expr(), + is_prob_less_than1.expr(), 0.expr(), // is_padding ] .into_iter() @@ -2683,6 +2718,7 @@ impl DecoderConfig { [ 0.expr(), // q_first + 1.expr(), // q_start block_idx, table_kind, table_size, @@ -2775,6 +2811,7 @@ impl DecoderConfig { symbol, baseline, nb, + 0.expr(), // is_skipped_state 0.expr(), // is_padding ] .into_iter() diff --git a/aggregator/src/aggregation/decoder/tables/fse.rs b/aggregator/src/aggregation/decoder/tables/fse.rs index 7e3800f0a0..e5e3ef3a8c 100644 --- a/aggregator/src/aggregation/decoder/tables/fse.rs +++ b/aggregator/src/aggregation/decoder/tables/fse.rs @@ -1,5 +1,4 @@ use gadgets::{ - comparator::{ComparatorChip, ComparatorConfig}, is_equal::{IsEqualChip, IsEqualConfig}, util::{and, not, select, Expr}, }; @@ -16,13 +15,741 @@ use zkevm_circuits::{ 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 -/// incremental states) clubbed together, followed by symbol s1 and so on. +/// The FSE table verifies that given the symbols and the states allocated to those symbols, the +/// baseline and number of bits (nb) are assigned correctly to them. +/// +/// The FSE table's layout is setup in a specific order, so that we cannot specify multiple FSE +/// table's of the same kind at the same block index. Every block has 3 FSE tables, namely for +/// Literal Length (LLT), Match Offset (MOT) and Match Length (MLT). They appear in the below +/// order: +/// +/// - block_idx=1, table_kind=LLT +/// - block_idx=1, table_kind=MOT +/// - block_idx=1, table_kind=MLT +/// - block_idx=2, table_kind=LLT +/// - ... and so on +/// +/// Each table spans over a maximum of 1024 rows, and the start of an FSE table is marked by the +/// fixed column ``q_start``. Upon finishing the FSE table, remaining rows are marked with the +/// ``is_padding`` column. +/// +/// Each table begins with symbols that have a "less than 1" probability, whereby the state +/// allocated to them is at the end of the table (highest state) and retreating. For example, if +/// the symbol=3 has a normalised probability of prob==-1, then it is allocated the state 0x3f (63) +/// in an FSE table of accuracy_log=6. For subsequent symbols that have a prob>1, the state=0x3f is +/// skipped and we continue the same computation for the next successive state: +/// +/// - state' == state'' & (table_size - 1) +/// - state'' == state + (table_size >> 3) + (table_size >> 1) + 3 +/// +/// where state' signifies the next state. +/// +/// We cannot anticipate how many times we end up on such a "skipped" (or pre-allocated) state +/// while computing the states for a symbol, so we mark such rows with the boolean column +/// ``is_skipped_state``. On these rows, the ``state`` should have been taken by a +/// ``is_prob_less_than1`` symbol that reads AL number of bits at a baseline of 0x00. +/// +/// | State | Symbol | is_prob_less_than1 | +/// |-------|--------|--------------------| +/// | 0 | 0 | 0 | <- q_first +/// |-------|--------|--------------------| +/// | 0x3f | 3 | 1 | <- q_start +/// | 0x3e | 4 | 1 | +/// | 0x00 | 0 | 0 | +/// | ... | 0 | 0 | +/// | 0x1d | 0 | 0 | +/// | 0x03 | 1 -> | 0 | +/// | 0x0c | 1 -> | 0 | +/// | 0x11 | 1 -> | 0 | +/// | 0x15 | 1 -> | 0 | +/// | 0x1a | 1 -> | 0 | +/// | 0x1e | 1 -> | 0 | +/// | 0x08 | 2 | 0 | +/// | ... | ... | 0 | +/// | 0x09 | 6 | 0 | +/// | 0x00 | 0 | 0 | <- is_padding +/// | ... | ... | 0 | <- is_padding +/// | 0x00 | 0 | 0 | <- is_padding +/// |-------|--------|--------------------| +/// | ... | ... | ... | <- q_start +/// |-------|--------|--------------------| +/// +/// 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 { + /// The helper table to validate that the (baseline, nb) were assigned correctly to each state. + fse_sorted_states_table: FseSortedStatesTable, + /// A boolean to mark whether this row represents a symbol with probability "less than 1". + is_prob_less_than1: Column, + /// Boolean column to mark whether the row is a padded row. + is_padding: 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, + /// Boolean column to tell us when symbol is changing. + is_new_symbol: 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 if we are not skipping the state. When we + /// encounter a new symbol, we validate that on the previous row, symbol_count equaled + /// 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, + /// Boolean column to mark if the computed state must be "skipped" because it was + /// pre-allocated to one of the symbols with a "less than 1" probability. + is_skipped_state: Column, + /// The assigned baseline for this state. + baseline: Column, + /// The number of bits to read from bitstream when at this state. + nb: Column, + /// ROM table for verifying FSE table kind and block_idx transition. + rom_fse_transition: RomFseTableTransition, +} + +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 { + // Fixed table to check the transition of table kinds and block idx. + let rom_fse_transition = RomFseTableTransition::construct(meta); + + // Auxiliary table to validate that (baseline, nb) were assigned correctly to the states + // allocated to a symbol. + let fse_sorted_states_table = FseSortedStatesTable::configure(meta, pow2_table, u8_table); + + let config = Self { + fse_sorted_states_table, + is_prob_less_than1: meta.advice_column(), + is_padding: meta.advice_column(), + table_size_rs_1: meta.advice_column(), + table_size_rs_3: meta.advice_column(), + idx: meta.advice_column(), + symbol: meta.advice_column(), + is_new_symbol: meta.advice_column(), + symbol_count: meta.advice_column(), + symbol_count_acc: meta.advice_column(), + state: meta.advice_column(), + is_skipped_state: meta.advice_column(), + baseline: meta.advice_column(), + nb: meta.advice_column(), + rom_fse_transition, + }; + + // Check that on the starting row of each FSE table, i.e. q_start=true: + // - table_size_rs_3 == table_size >> 3. + meta.lookup("FseTable: table_size >> 3", |meta| { + let condition = and::expr([ + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let range_value = meta + .query_advice(config.fse_sorted_states_table.table_size, Rotation::cur()) + - (meta.query_advice(config.table_size_rs_3, Rotation::cur()) * 8.expr()); + + vec![(condition * range_value, range8_table.into())] + }); + + // Every FSE symbol is a byte. + meta.lookup("FseTable: symbol in [0, 256)", |meta| { + vec![( + meta.query_advice(config.symbol, Rotation::cur()), + u8_table.into(), + )] + }); + + // The first row of the FseTable layout, i.e. q_first=true. + meta.create_gate("FseTable: first row", |meta| { + let condition = + meta.query_fixed(config.fse_sorted_states_table.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.fse_sorted_states_table.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.fse_sorted_states_table.table_kind, Rotation::next()), + FseTableKind::LLT.expr(), + ); + + cb.gate(condition) + }); + + // Check that on the starting row of every FSE table, i.e. q_start=true: + // + // - tuple (block_idx::prev, block_idx::cur, table_kind::prev, table_kind::cur) + // + // is in fact a valid transition. All valid transitions are provided in the fixed-table + // RomFseTableTransition. + meta.lookup_any( + "FseSortedStatesTable: start row (ROM block_idx and table_kind transition)", + |meta| { + let condition = and::expr([ + meta.query_fixed(config.fse_sorted_states_table.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.fse_sorted_states_table.block_idx, Rotation::prev()), + meta.query_advice(config.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_kind, Rotation::prev()), + meta.query_advice(config.fse_sorted_states_table.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() + }, + ); + + // The starting row of every FSE table, i.e. q_start=true. + meta.create_gate("FseTable: start row", |meta| { + let condition = and::expr([ + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + let is_prob_less_than1 = meta.query_advice(config.is_prob_less_than1, Rotation::cur()); + cb.require_boolean("prob=-1 is boolean", is_prob_less_than1.expr()); + + // 1. If we start with a symbol that has prob "less than 1" + cb.condition(is_prob_less_than1.expr(), |cb| { + cb.require_equal( + "prob=-1: state inits at table_size - 1", + meta.query_advice(config.state, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_size, Rotation::cur()) + - 1.expr(), + ); + }); + + // 2. If no symbol has a prob "less than 1" + cb.condition(not::expr(is_prob_less_than1), |cb| { + cb.require_zero( + "state inits at 0", + 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", + meta.query_advice(config.fse_sorted_states_table.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_new_symbol==true", + meta.query_advice(config.is_new_symbol, Rotation::cur()), + 1.expr(), + ); + + cb.gate(condition) + }); + + // For every symbol that has a normalised probability prob=-1. + meta.lookup_any("FseTable: all symbols with prob=-1 (nb==AL)", |meta| { + let condition = meta.query_advice(config.is_prob_less_than1, Rotation::cur()); + + // for a symbol with prob=-1, we do a full state reset, i.e. + // read nb=AL bits, i.e. 1 << nb == table_size. + [ + meta.query_advice(config.nb, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_size, Rotation::cur()), + ] + .into_iter() + .zip_eq(pow2_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }); + + // For every symbol that has a normalised probability prob=-1. + meta.create_gate("FseTable: all symbols with prob=-1", |meta| { + let condition = meta.query_advice(config.is_prob_less_than1, Rotation::cur()); + + let mut cb = BaseConstraintBuilder::default(); + + // Each such row is a new symbol. + cb.require_equal( + "prob=-1: is_new_symbol==true", + meta.query_advice(config.is_new_symbol, Rotation::cur()), + 1.expr(), + ); + + // prob=-1 indicates a baseline==0x00. + cb.require_zero( + "prob=-1: baseline==0x00", + meta.query_advice(config.baseline, Rotation::cur()), + ); + + // prob=-1 symbol cannot be padding. + cb.require_zero( + "prob=-1: is_padding==false", + meta.query_advice(config.is_padding, Rotation::cur()), + ); + + // prob=-1 symbol is not a skipped state. + cb.require_zero( + "prob=-1: is_skipped_state=false", + meta.query_advice(config.is_skipped_state, Rotation::cur()), + ); + + cb.gate(condition) + }); + + // Symbols with prob=-1 are in increasing order. + meta.lookup( + "FseTable: subsequent symbols with prob=-1 (symbol increasing)", + |meta| { + let condition = and::expr([ + not::expr( + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + ), + meta.query_advice(config.is_prob_less_than1, Rotation::cur()), + ]); + + // Symbols with prob=-1 are assigned cells from the end (state==table_size-1) and + // retreating. However those symbols are processed in natural order, i.e. symbols + // are in increasing order. + // + // - symbol::cur - symbol::prev > 0 + // + // We check that (symbol - symbol_prev - 1) lies in the [0, 256) range. + let (symbol_curr, symbol_prev) = ( + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::prev()), + ); + let delta = symbol_curr - symbol_prev - 1.expr(); + + vec![(condition * delta, u8_table.into())] + }, + ); + + // Symbols with prob=-1 are assigned states from the end and retreating. + meta.create_gate( + "FseTable: subsequent symbols with prob=-1 (state retreating)", + |meta| { + let condition = and::expr([ + not::expr( + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + ), + meta.query_advice(config.is_prob_less_than1, Rotation::cur()), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // While prob=-1, state is retreating, i.e. decrements by 1. + cb.require_equal( + "state == state::prev - 1", + meta.query_advice(config.state, Rotation::cur()), + meta.query_advice(config.state, Rotation::prev()) - 1.expr(), + ); + + cb.gate(condition) + }, + ); + + // Symbols with prob>=1 are also in increasing order. We skip this check if this is the + // first symbol with prob>=1. + meta.lookup( + "FseTable: symbols with prob>=1 (symbol increasing)", + |meta| { + let condition = and::expr([ + not::expr( + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + ), + not::expr(meta.query_advice(config.is_prob_less_than1, Rotation::prev())), + meta.query_advice(config.is_new_symbol, Rotation::cur()), + ]); + + // Whenever we move to a new symbol (is_new_symbol=true), excluding the first symbol + // with prob>=1, the symbol is increasing. + // + // - symbol::cur - symbol::prev > 0 + // + // We check that (symbol - symbol_prev - 1) lies in the [0, 256) range. + let (symbol_curr, symbol_prev) = ( + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::prev()), + ); + let delta = symbol_curr - symbol_prev - 1.expr(); + + vec![(condition * delta, u8_table.into())] + }, + ); + + // Symbols with prob>=1 continue the same symbol if not a new symbol. + meta.create_gate("FseTable: symbols with prob>=1", |meta| { + let condition = and::expr([ + not::expr( + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + ), + not::expr(meta.query_advice(config.is_prob_less_than1, Rotation::cur())), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let mut cb = BaseConstraintBuilder::default(); + + // When we are not seeing a new symbol, make sure the symbol is equal to the symbol on + // the previous row. + let is_not_new_symbol = + not::expr(meta.query_advice(config.is_new_symbol, Rotation::cur())); + cb.condition(is_not_new_symbol, |cb| { + cb.require_equal( + "prob>=1: same symbol", + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::prev()), + ); + }); + + cb.gate(condition) + }); + + // All rows in an instance of FSE table, except the starting row (q_start=true). + meta.create_gate("FseTable: every FSE table (except q_start=1)", |meta| { + let condition = not::expr( + meta.query_fixed(config.fse_sorted_states_table.q_start, Rotation::cur()), + ); + + let mut cb = BaseConstraintBuilder::default(); + + // FSE table's columns that remain unchanged. + for column in [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()), + ); + } + + // The symbols with prob "less than 1" are assigned at the starting rows of the FSE + // table with maximum (and retreating) state values. + let (is_prob_less_than1_prev, is_prob_less_than1_curr) = ( + meta.query_advice(config.is_prob_less_than1, Rotation::prev()), + meta.query_advice(config.is_prob_less_than1, Rotation::cur()), + ); + let delta = is_prob_less_than1_prev - is_prob_less_than1_curr.expr(); + cb.require_boolean("prob=-1 is boolean", is_prob_less_than1_curr); + cb.require_boolean("prob=-1 symbols occur in the start of the layout", delta); + + // 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.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); + + // If we are not in the padding region and don't skip state on this row, then this is a + // new state in the FSE table, i.e. idx increments. + let is_skipped_state = meta.query_advice(config.is_skipped_state, Rotation::cur()); + cb.require_equal( + "idx increments in non-padding region if we don't skip state", + meta.query_advice(config.idx, Rotation::cur()), + select::expr( + and::expr([ + not::expr(is_padding_curr.expr()), + not::expr(is_skipped_state), + ]), + meta.query_advice(config.idx, Rotation::prev()) + 1.expr(), + meta.query_advice(config.idx, Rotation::prev()), + ), + ); + + // 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.fse_sorted_states_table.table_size, + Rotation::prev(), + ), + ); + }, + ); + + cb.gate(condition) + }); + + // A state is skipped only if that state was pre-allocated to a symbol with prob=-1. + meta.lookup_any("FseTable: skipped state", |meta| { + let condition = meta.query_advice(config.is_skipped_state, Rotation::cur()); + + // A state can be skipped only if it was pre-allocated to a symbol with prob=-1. So we + // check that there exists a row with the same block_idx, table_kind and the skipped + // state with a prob=-1. + let fse_table_exprs = [ + meta.query_advice(config.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(config.state, Rotation::cur()), + meta.query_advice(config.is_prob_less_than1, Rotation::cur()), + ]; + + [ + meta.query_advice(config.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(config.state, Rotation::cur()), + 1.expr(), // prob=-1 + ] + .into_iter() + .zip_eq(fse_table_exprs) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }); + + // For every symbol with prob>=1 and a valid state allocated, we check that the baseline + // and nb fields were assigned correctly. + meta.lookup_any( + "FseTable: assigned state (baseline, nb) validation", + |meta| { + let condition = and::expr([ + not::expr(meta.query_advice(config.is_prob_less_than1, Rotation::cur())), + not::expr(meta.query_advice(config.is_skipped_state, Rotation::cur())), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); + + let (block_idx, table_kind, table_size, state, symbol, symbol_count, baseline, nb) = ( + meta.query_advice(config.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(config.fse_sorted_states_table.table_size, Rotation::cur()), + meta.query_advice(config.state, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol_count, Rotation::cur()), + meta.query_advice(config.baseline, Rotation::cur()), + meta.query_advice(config.nb, Rotation::cur()), + ); + + [ + block_idx, + table_kind, + table_size, + state, + symbol, + symbol_count, + baseline, + nb, + 0.expr(), + ] + .into_iter() + .zip_eq(config.fse_sorted_states_table.table_exprs(meta)) + .map(|(arg, table)| (condition.expr() * arg, table)) + .collect() + }, + ); + + // For every new symbol detected. + meta.create_gate("FseTable: new symbol", |meta| { + let condition = and::expr([ + meta.query_advice(config.is_new_symbol, 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. + // + // This is also expected to pass on the starting row of each FSE table, since the + // previous row is either q_first=true or is_padding=true, where in both + // cases we expect: + // - symbol_count == symbol_count_acc == 0. + 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()), + ); + + // 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) + }); + + // Whenever we continue allocating states to the same symbol. + meta.create_gate("FseTable: same symbol, transitioned state", |meta| { + let condition = and::expr([ + not::expr(meta.query_advice(config.is_new_symbol, 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 + cb.require_equal( + "if symbol continues: symbol_count unchanged", + meta.query_advice(config.symbol_count, Rotation::cur()), + meta.query_advice(config.symbol_count, Rotation::prev()), + ); + + // symbol count accumulator increments if the state is not skipped. + cb.require_equal( + "symbol_count_acc increments if state not skipped", + meta.query_advice(config.symbol_count_acc, Rotation::cur()), + select::expr( + meta.query_advice(config.is_skipped_state, Rotation::cur()), + meta.query_advice(config.symbol_count_acc, Rotation::prev()), + meta.query_advice(config.symbol_count_acc, Rotation::prev()) + 1.expr(), + ), + ); + + 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.fse_sorted_states_table.q_start, Rotation::cur()), + ), + not::expr(meta.query_advice(config.is_prob_less_than1, 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.fse_sorted_states_table.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_fixed(self.fse_sorted_states_table.q_first, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.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_skipped_state, 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_fixed(self.fse_sorted_states_table.q_first, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.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_prob_less_than1, Rotation::cur()), + meta.query_advice(self.is_padding, Rotation::cur()), + ] + } + + /// Lookup table expressions for (table_kind, table_size) to know that the FSE decoder values + /// were correctly populated even at the "init-state" stage. + pub fn table_exprs_metadata(&self, meta: &mut VirtualCells) -> Vec> { + vec![ + meta.query_fixed(self.fse_sorted_states_table.q_first, Rotation::cur()), + meta.query_fixed(self.fse_sorted_states_table.q_start, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.block_idx, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.table_kind, Rotation::cur()), + meta.query_advice(self.fse_sorted_states_table.table_size, Rotation::cur()), + meta.query_advice(self.is_padding, Rotation::cur()), + ] + } +} + +/// Contrary to the FSE table where states are allocated as per the state transition rules, in the +/// FseSortedStatesTable, for every symbol with prob>=1 we sort its states in increasing order to +/// appropriately compute the (baseline, nb) fields assigned to those states. /// /// | State | Symbol | Baseline | Nb | Baseline Mark | /// |-------|--------|----------|-----|---------------| +/// | 0 | 0 | 0 | 0 | 0 | <- q_first +/// |-------|--------|----------|-----|---------------| /// | 0x00 | s0 | ... | ... | 0 | <- q_start /// | 0x01 | s0 | ... | ... | 0 | /// | 0x02 | s0 | ... | ... | 0 | @@ -40,16 +767,15 @@ use crate::aggregation::decoder::tables::rom_fse_order::{FseTableKind, RomFseTab /// | 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 +/// |-------|--------|----------|-----|---------------| +/// | ... | ... | ... | ... | ... | <- q_start +/// |-------|--------|----------|-----|---------------| /// /// 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 { +struct FseSortedStatesTable { /// 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, @@ -59,47 +785,35 @@ pub struct FseTable { /// 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 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. + /// The number of states in the FSE table, i.e. 1 << AL. 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. + /// The FSE symbol, starting at the first symbol with prob>=1. 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, + /// Boolean column to mark if we are moving to the next symbol. + is_new_symbol: 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. + /// It increments while the symbol remains the same. When we encounter a new symbol, we + /// validate that on the previous row, symbol_count equaled 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. + /// The state in FSE. In this table the state is in increasing order for each symbol. state: Column, /// Denotes the baseline field. baseline: Column, + /// The number of bits to be read from bitstream at this state. + nb: Column, + /// Boolean column to mark whether the row is a padded row. + is_padding: 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, @@ -109,50 +823,30 @@ 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 { - /// Configure the FSE table. - pub fn configure( +impl FseSortedStatesTable { + fn configure( meta: &mut ConstraintSystem, - u8_table: U8Table, - range8_table: RangeTable<8>, pow2_table: Pow2Table<20>, - bitwise_op_table: BitwiseOpTable, + u8_table: U8Table, ) -> Self { - // Fixed table to check the transition of table kinds and block idx. - let rom_fse_transition = RomFseTableTransition::construct(meta); + let (is_padding, baseline) = (meta.advice_column(), meta.advice_column()); - 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(), 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( - 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: meta.advice_column(), + is_new_symbol: meta.advice_column(), symbol_count: meta.advice_column(), symbol_count_acc: meta.advice_column(), state: meta.advice_column(), baseline, + nb: meta.advice_column(), + is_padding, baseline_0x00: IsEqualChip::configure( meta, |meta| not::expr(meta.query_advice(is_padding, Rotation::cur())), @@ -160,15 +854,14 @@ impl FseTable { |_| 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(), - rom_fse_transition, }; - meta.lookup_any("FseTable: spot == 1 << nb", |meta| { + // For every non-padded row, the SPoT is 2^nb. + meta.lookup_any("FseSortedStatesTable: spot == 1 << nb", |meta| { let condition = not::expr(meta.query_advice(config.is_padding, Rotation::cur())); [ @@ -181,29 +874,8 @@ impl FseTable { .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: first row", |meta| { + // The first row of the FseTable layout, i.e. q_first=true. + meta.create_gate("FseSortedStatesTable: first row", |meta| { let condition = meta.query_fixed(config.q_first, Rotation::cur()); let mut cb = BaseConstraintBuilder::default(); @@ -226,149 +898,134 @@ impl FseTable { cb.gate(condition) }); - meta.lookup_any( - "FseTable: start row (FSE table kind and block_idx transition)", + // The starting row of every FSE table, i.e. q_start=true. + meta.create_gate("FseSortedStatesTable: 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(); + + // The start row is a new symbol. + cb.require_equal( + "is_new_symbol==true", + meta.query_advice(config.is_new_symbol, Rotation::cur()), + 1.expr(), + ); + + cb.gate(condition) + }); + + // Symbols are in increasing order. + meta.lookup( + "FseSortedStatesTable: symbols are in increasing order", |meta| { let condition = and::expr([ - meta.query_fixed(config.q_start, Rotation::cur()), - not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + not::expr(meta.query_fixed(config.q_start, Rotation::cur())), + meta.query_advice(config.is_new_symbol, 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()), + // Whenever we move to a new symbol (is_new_symbol=true), excluding the first symbol + // with prob>=1, the symbol is increasing. + // + // - symbol::cur - symbol::prev > 0 + // + // We check that (symbol - symbol_prev - 1) lies in the [0, 256) range. + let (symbol_curr, symbol_prev) = ( + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::prev()), ); + let delta = symbol_curr - symbol_prev - 1.expr(); - [ - 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() + vec![(condition * delta, u8_table.into())] }, ); - meta.create_gate("FseTable: start row", |meta| { + // We continue the same symbol if not a new symbol. + meta.create_gate("FseSortedStatesTable: same symbol", |meta| { let condition = and::expr([ - meta.query_fixed(config.q_start, Rotation::cur()), + not::expr(meta.query_fixed(config.q_first, Rotation::cur())), + not::expr(meta.query_fixed(config.q_start, Rotation::cur())), + not::expr(meta.query_advice(config.is_new_symbol, 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()), - ); - - 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", - 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. + // When we are not seeing a new symbol, make sure the symbol is equal to the symbol on + // the previous row. cb.require_equal( - "is_symbol_change == 1", - meta.query_advice(config.is_symbol_change, Rotation::cur()), - 1.expr(), + "prob>=1: same symbol", + meta.query_advice(config.symbol, Rotation::cur()), + meta.query_advice(config.symbol, Rotation::prev()), ); cb.gate(condition) }); - 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(); + // While continuing the same symbol, states are in increasing order. + meta.lookup( + "FseSortedStatesTable: states are in increasing order", + |meta| { + let condition = and::expr([ + not::expr(meta.query_fixed(config.q_first, Rotation::cur())), + not::expr(meta.query_fixed(config.q_start, Rotation::cur())), + not::expr(meta.query_advice(config.is_new_symbol, Rotation::cur())), + not::expr(meta.query_advice(config.is_padding, Rotation::cur())), + ]); - // FSE table's columns that remain unchanged. - for column in [ - config.block_idx, - config.table_kind, - 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()), + // While traversing the same symbol (is_new_symbol=false), the states allocated to + // it in the FseSortedStatesTable are in increasing order. So we check that: + // + // - state::cur - state::prev > 0 + // + // We check that (state::cur - state::prev - 1) lies in the [0, 256) range. + let (state_curr, state_prev) = ( + meta.query_advice(config.state, Rotation::cur()), + meta.query_advice(config.state, 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()); - }); + let delta = state_curr - state_prev - 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()); - }); + vec![(condition * delta, u8_table.into())] + }, + ); - // 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.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); + // All rows in an instance of FSE table, except the starting row (q_start=true). + meta.create_gate( + "FseSortedStatesTable: every FSE table (except q_start=1)", + |meta| { + let condition = not::expr(meta.query_fixed(config.q_start, Rotation::cur())); - // 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(), - ); - }); + let mut cb = BaseConstraintBuilder::default(); - // 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| { + // FSE table's columns that remain unchanged. + for column in [config.block_idx, config.table_kind, config.table_size] { 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()), + "FseSortedStatesTable: columns that remain unchanged", + meta.query_advice(column, Rotation::cur()), + meta.query_advice(column, Rotation::prev()), ); - }, - ); + } - cb.gate(condition) - }); + // 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.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); + + cb.gate(condition) + }, + ); - meta.create_gate("FseTable: symbol changes", |meta| { + // For every new symbol detected. + meta.create_gate("FseSortedStatesTable: new symbol", |meta| { let condition = and::expr([ - meta.query_advice(config.is_symbol_change, Rotation::cur()), + meta.query_advice(config.is_new_symbol, Rotation::cur()), not::expr(meta.query_advice(config.is_padding, Rotation::cur())), ]); @@ -407,6 +1064,8 @@ impl FseTable { // encounter baseline==0x00. let is_baseline_mark = meta.query_advice(config.baseline_mark, Rotation::cur()); let is_baseline_0x00 = config.baseline_0x00.expr(); + + cb.require_boolean("is_baseline_mark is boolean", is_baseline_mark.expr()); cb.condition(is_baseline_0x00.expr(), |cb| { cb.require_equal( "baseline_mark set at baseline==0x00", @@ -458,9 +1117,10 @@ impl FseTable { cb.gate(condition) }); - meta.create_gate("FseTable: symbol continues", |meta| { + // Whenever we continue allocating states to the same symbol. + meta.create_gate("FseSortedStatesTable: same symbol, new state", |meta| { let condition = and::expr([ - not::expr(meta.query_advice(config.is_symbol_change, Rotation::cur())), + not::expr(meta.query_advice(config.is_new_symbol, Rotation::cur())), not::expr(meta.query_advice(config.is_padding, Rotation::cur())), ]); @@ -482,7 +1142,7 @@ impl FseTable { config.last_baseline, ] { cb.require_equal( - "unchanged columns", + "FseSortedStatesTable: unchanged columns (same symbol)", meta.query_advice(column, Rotation::cur()), meta.query_advice(column, Rotation::prev()), ); @@ -495,7 +1155,7 @@ impl FseTable { ); cb.require_equal( - "spot_acc accumlates", + "spot_acc accumulates", meta.query_advice(config.spot_acc, Rotation::cur()), meta.query_advice(config.spot_acc, Rotation::prev()) + meta.query_advice(config.spot, Rotation::cur()), @@ -506,9 +1166,10 @@ impl FseTable { 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); + cb.require_boolean("baseline_mark is boolean", baseline_mark_curr); + cb.require_boolean("baseline_mark_delta is boolean", baseline_mark_delta.expr()); - // baseline == baseline_mark_curr == 1 ? 0x00 : baseline_prev + spot_prev + // baseline == baseline_mark_delta == 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()), @@ -517,92 +1178,42 @@ impl FseTable { cb.require_equal( "baseline calculation", baseline_curr, - select::expr(baseline_mark_curr, 0x00.expr(), baseline_prev + spot_prev), + select::expr(baseline_mark_delta, 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_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()), - 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> { +impl LookupTable for FseSortedStatesTable { + fn columns(&self) -> Vec> { vec![ - 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()), - meta.query_advice(self.symbol_count_acc, Rotation::cur()), - meta.query_advice(self.is_padding, Rotation::cur()), + self.block_idx.into(), + self.table_kind.into(), + self.table_size.into(), + self.symbol.into(), + self.symbol_count.into(), + self.state.into(), + self.baseline.into(), + self.nb.into(), + self.is_padding.into(), ] } - /// Lookup table expressions for (table_kind, table_size) to know that the FSE decoder values - /// were correctly populated even at the "init-state" stage. - pub fn table_exprs_metadata(&self, meta: &mut VirtualCells) -> Vec> { + fn annotations(&self) -> Vec { vec![ - 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.is_padding, Rotation::cur()), + String::from("block_idx"), + String::from("table_kind"), + String::from("table_size"), + String::from("symbol"), + String::from("symbol_count"), + String::from("state"), + String::from("baseline"), + String::from("nb"), + String::from("is_padding"), ] } } diff --git a/aggregator/src/aggregation/decoder/witgen/types.rs b/aggregator/src/aggregation/decoder/witgen/types.rs index 6e403e905d..c3bb20a0d1 100644 --- a/aggregator/src/aggregation/decoder/witgen/types.rs +++ b/aggregator/src/aggregation/decoder/witgen/types.rs @@ -608,17 +608,20 @@ impl FseAuxiliaryTableData { offset += n_bits_read; bit_boundaries.push((offset, value)); + let N = match value { + 0 => 1, + _ => value - 1, + }; + if value == 0 { unimplemented!("value=0 => prob=-1: scenario unimplemented"); } - let N = value - 1; - // When a symbol has a probability of zero, it is followed by a 2-bits repeat flag. This // repeat flag tells how many probabilities of zeroes follow the current one. It // provides a number ranging from 0 to 3. If it is a 3, another 2-bits repeat flag // follows, and so on. - if N == 0 { + if value == 1 { sym_to_states.insert(symbol, vec![]); symbol += 1; @@ -638,7 +641,7 @@ impl FseAuxiliaryTableData { } } - if N >= 1 { + if value >= 2 { let states = std::iter::once(state) .chain((1..N).map(|_| { state += (table_size >> 1) + (table_size >> 3) + 3;