halo2_base/virtual_region/lookups/basic.rs
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 layouter
94 .assign_region(
95 || "[BasicDynLookupConfig] Advice cells to lookup",
96 |mut region| {
97 self.assign_virtual_to_lookup_to_raw_from_offset(
98 &mut region,
99 keys,
100 0,
101 copy_manager,
102 );
103 Ok(())
104 },
105 )
106 .unwrap();
107 }
108
109 /// Assign managed lookups. The `keys` must have already been raw assigned beforehand.
110 ///
111 /// `copy_manager` **must** be provided unless you are only doing witness generation
112 /// without constraints.
113 pub fn assign_virtual_to_lookup_to_raw_from_offset<F: ScalarField>(
114 &self,
115 region: &mut Region<F>,
116 keys: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
117 mut offset: usize,
118 copy_manager: Option<&SharedCopyConstraintManager<F>>,
119 ) {
120 let mut copy_manager = copy_manager.map(|c| c.lock().unwrap());
121 // Copied from `LookupAnyManager::assign_raw` but modified to set `key_is_enabled` to 1.
122 // Copy the cells to the config columns, going left to right, then top to bottom.
123 // Will panic if out of rows
124 let mut lookup_col = 0;
125 for key in keys {
126 if lookup_col >= self.to_lookup.len() {
127 lookup_col = 0;
128 offset += 1;
129 }
130 let (key_col, key_is_enabled_col) = self.to_lookup[lookup_col];
131 // set key_is_enabled to 1
132 raw_assign_fixed(region, key_is_enabled_col, offset, F::ONE);
133 for (advice, column) in zip(key, key_col) {
134 let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value));
135 if let Some(copy_manager) = copy_manager.as_mut() {
136 constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager);
137 }
138 }
139
140 lookup_col += 1;
141 }
142 }
143
144 /// Assign virtual table to raw. The `rows` must have already been raw assigned beforehand.
145 ///
146 /// `copy_manager` **must** be provided unless you are only doing witness generation
147 /// without constraints.
148 pub fn assign_virtual_table_to_raw<F: ScalarField>(
149 &self,
150 mut layouter: impl Layouter<F>,
151 rows: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
152 copy_manager: Option<&SharedCopyConstraintManager<F>>,
153 ) {
154 layouter
155 .assign_region(
156 || "[BasicDynLookupConfig] Dynamic Lookup Table",
157 |mut region| {
158 self.assign_virtual_table_to_raw_from_offset(
159 &mut region,
160 rows,
161 0,
162 copy_manager,
163 );
164 Ok(())
165 },
166 )
167 .unwrap();
168 }
169
170 /// Assign virtual table to raw. The `rows` must have already been raw assigned beforehand.
171 ///
172 /// `copy_manager` **must** be provided unless you are only doing witness generation
173 /// without constraints.
174 pub fn assign_virtual_table_to_raw_from_offset<F: ScalarField>(
175 &self,
176 region: &mut Region<F>,
177 rows: impl IntoIterator<Item = [AssignedValue<F>; KEY_COL]>,
178 mut offset: usize,
179 copy_manager: Option<&SharedCopyConstraintManager<F>>,
180 ) {
181 let mut copy_manager = copy_manager.map(|c| c.lock().unwrap());
182 for row in rows {
183 // Enable this row in the table
184 raw_assign_fixed(region, self.table_is_enabled, offset, F::ONE);
185 for (advice, column) in zip(row, self.table) {
186 let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value));
187 if let Some(copy_manager) = copy_manager.as_mut() {
188 constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager);
189 }
190 }
191 offset += 1;
192 }
193 // always assign one disabled row with all 0s, so disabled to_lookup works for sure
194 raw_assign_fixed(region, self.table_is_enabled, offset, F::ZERO);
195 for col in self.table {
196 raw_assign_advice(region, col, offset, Value::known(F::ZERO));
197 }
198 }
199}