halo2_base/virtual_region/lookups/
basic.rs

Help
1use std::iter::zip;
2
3use crate::{
4    halo2_proofs::{
5        circuit::{Layouter, Region, Value},
6        halo2curves::ff::Field,
7        plonk::{Advice, Column, ConstraintSystem, Fixed, Phase},
8        poly::Rotation,
9    },
10    utils::{
11        halo2::{constrain_virtual_equals_external, raw_assign_advice, raw_assign_fixed},
12        ScalarField,
13    },
14    virtual_region::copy_constraints::SharedCopyConstraintManager,
15    AssignedValue,
16};
17
18/// A simple dynamic lookup table for when you want to verify some length `KEY_COL` key
19/// is in a provided (dynamic) table of the same format.
20///
21/// Note that you can also use this to look up (key, out) pairs, where you consider the whole
22/// pair as the new key.
23///
24/// We can have multiple sets of dedicated columns to be looked up: these can be specified
25/// when calling `new`, but typically we just need 1 set.
26///
27/// The `table` consists of advice columns. Since this table may have poisoned rows (blinding factors),
28/// we use a fixed column `table_selector` which is default 0 and only 1 on enabled rows of the table.
29/// The dynamic lookup will check that for `(key, key_is_enabled)` in `to_lookup` we have `key` matches one of
30/// the rows in `table` where `table_selector == key_is_enabled`.
31/// Reminder: the Halo2 lookup argument will ignore the poisoned rows in `to_lookup`
32/// (see [https://zcash.github.io/halo2/design/proving-system/lookup.html#zero-knowledge-adjustment]), but it will
33/// not ignore the poisoned rows in `table`.
34///
35/// Part of this design consideration is to allow a key of `[F::ZERO; KEY_COL]` to still be used as a valid key
36/// in the lookup argument. By default, unfilled rows in `to_lookup` will be all zeros; we require
37/// at least one row in `table` where `table_is_enabled = 0` and the rest of the row in `table` are also 0s.
38#[derive(Clone, Debug)]
39pub struct BasicDynLookupConfig<const KEY_COL: usize> {
40    /// Columns for cells to be looked up. Consists of `(key, key_is_enabled)`.
41    pub to_lookup: Vec<([Column<Advice>; KEY_COL], Column<Fixed>)>,
42    /// Table to look up against.
43    pub table: [Column<Advice>; KEY_COL],
44    /// Selector to enable a row in `table` to actually be part of the lookup table. This is to prevent
45    /// blinding factors in `table` advice columns from being used in the lookup.
46    pub table_is_enabled: Column<Fixed>,
47}
48
49impl<const KEY_COL: usize> BasicDynLookupConfig<KEY_COL> {
50    /// Assumes all columns are in the same phase `P` to make life easier.
51    /// We enable equality on all columns because we envision both the columns to lookup
52    /// and the table will need to talk to halo2-lib.
53    pub fn new<P: Phase, F: Field>(
54        meta: &mut ConstraintSystem<F>,
55        phase: impl Fn() -> P,
56        num_lu_sets: usize,
57    ) -> Self {
58        let mut make_columns = || {
59            let advices = [(); KEY_COL].map(|_| {
60                let advice = meta.advice_column_in(phase());
61                meta.enable_equality(advice);
62                advice
63            });
64            let is_enabled = meta.fixed_column();
65            (advices, is_enabled)
66        };
67        let (table, table_is_enabled) = make_columns();
68        let to_lookup: Vec<_> = (0..num_lu_sets).map(|_| make_columns()).collect();
69
70        for (key, key_is_enabled) in &to_lookup {
71            meta.lookup_any("dynamic lookup table", |meta| {
72                let table = table.map(|c| meta.query_advice(c, Rotation::cur()));
73                let table_is_enabled = meta.query_fixed(table_is_enabled, Rotation::cur());
74                let key = key.map(|c| meta.query_advice(c, Rotation::cur()));
75                let key_is_enabled = meta.query_fixed(*key_is_enabled, Rotation::cur());
76                zip(key, table).chain([(key_is_enabled, table_is_enabled)]).collect()
77            });
78        }
79
80        Self { table_is_enabled, table, to_lookup }
81    }
82
83    /// Assign managed lookups. The `keys` must have already been raw assigned beforehand.
84    ///
85    /// `copy_manager` **must** be provided unless you are only doing witness generation
86    /// without constraints.
87    pub fn assign_virtual_to_lookup_to_raw<F: ScalarField>(
88        &self,
89        mut layouter: impl Layouter<F>,
90        keys: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
91        copy_manager: Option<&SharedCopyConstraintManager<F>>,
92    ) {
93        #[cfg(not(feature = "halo2-axiom"))]
94        let keys = keys.into_iter().collect::<Vec<_>>();
95        layouter
96            .assign_region(
97                || "[BasicDynLookupConfig] Advice cells to lookup",
98                |mut region| {
99                    self.assign_virtual_to_lookup_to_raw_from_offset(
100                        &mut region,
101                        #[cfg(feature = "halo2-axiom")]
102                        keys,
103                        #[cfg(not(feature = "halo2-axiom"))]
104                        keys.clone(),
105                        0,
106                        copy_manager,
107                    );
108                    Ok(())
109                },
110            )
111            .unwrap();
112    }
113
114    /// Assign managed lookups. The `keys` must have already been raw assigned beforehand.
115    ///
116    /// `copy_manager` **must** be provided unless you are only doing witness generation
117    /// without constraints.
118    pub fn assign_virtual_to_lookup_to_raw_from_offset<F: ScalarField>(
119        &self,
120        region: &mut Region<F>,
121        keys: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
122        mut offset: usize,
123        copy_manager: Option<&SharedCopyConstraintManager<F>>,
124    ) {
125        let mut copy_manager = copy_manager.map(|c| c.lock().unwrap());
126        // Copied from `LookupAnyManager::assign_raw` but modified to set `key_is_enabled` to 1.
127        // Copy the cells to the config columns, going left to right, then top to bottom.
128        // Will panic if out of rows
129        let mut lookup_col = 0;
130        for key in keys {
131            if lookup_col >= self.to_lookup.len() {
132                lookup_col = 0;
133                offset += 1;
134            }
135            let (key_col, key_is_enabled_col) = self.to_lookup[lookup_col];
136            // set key_is_enabled to 1
137            raw_assign_fixed(region, key_is_enabled_col, offset, F::ONE);
138            for (advice, column) in zip(key, key_col) {
139                let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value));
140                if let Some(copy_manager) = copy_manager.as_mut() {
141                    constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager);
142                }
143            }
144
145            lookup_col += 1;
146        }
147    }
148
149    /// Assign virtual table to raw. The `rows` must have already been raw assigned beforehand.
150    ///
151    /// `copy_manager` **must** be provided unless you are only doing witness generation
152    /// without constraints.
153    pub fn assign_virtual_table_to_raw<F: ScalarField>(
154        &self,
155        mut layouter: impl Layouter<F>,
156        rows: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
157        copy_manager: Option<&SharedCopyConstraintManager<F>>,
158    ) {
159        #[cfg(not(feature = "halo2-axiom"))]
160        let rows = rows.into_iter().collect::<Vec<_>>();
161        layouter
162            .assign_region(
163                || "[BasicDynLookupConfig] Dynamic Lookup Table",
164                |mut region| {
165                    self.assign_virtual_table_to_raw_from_offset(
166                        &mut region,
167                        #[cfg(feature = "halo2-axiom")]
168                        rows,
169                        #[cfg(not(feature = "halo2-axiom"))]
170                        rows.clone(),
171                        0,
172                        copy_manager,
173                    );
174                    Ok(())
175                },
176            )
177            .unwrap();
178    }
179
180    /// Assign virtual table to raw. The `rows` must have already been raw assigned beforehand.
181    ///
182    /// `copy_manager` **must** be provided unless you are only doing witness generation
183    /// without constraints.
184    pub fn assign_virtual_table_to_raw_from_offset<F: ScalarField>(
185        &self,
186        region: &mut Region<F>,
187        rows: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
188        mut offset: usize,
189        copy_manager: Option<&SharedCopyConstraintManager<F>>,
190    ) {
191        let mut copy_manager = copy_manager.map(|c| c.lock().unwrap());
192        for row in rows {
193            // Enable this row in the table
194            raw_assign_fixed(region, self.table_is_enabled, offset, F::ONE);
195            for (advice, column) in zip(row, self.table) {
196                let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value));
197                if let Some(copy_manager) = copy_manager.as_mut() {
198                    constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager);
199                }
200            }
201            offset += 1;
202        }
203        // always assign one disabled row with all 0s, so disabled to_lookup works for sure
204        raw_assign_fixed(region, self.table_is_enabled, offset, F::ZERO);
205        for col in self.table {
206            raw_assign_advice(region, col, offset, Value::known(F::ZERO));
207        }
208    }
209}
halo2_base/virtual_region/lookups/basic.rs

halo2_base/virtual_region/lookups/
basic.rs
