diff --git a/halo2-base/src/utils/halo2.rs b/halo2-base/src/utils/halo2.rs index 510f7d25..463b128f 100644 --- a/halo2-base/src/utils/halo2.rs +++ b/halo2-base/src/utils/halo2.rs @@ -3,6 +3,8 @@ use crate::halo2_proofs::{ circuit::{AssignedCell, Cell, Region, Value}, plonk::{Advice, Assigned, Column, Fixed}, }; +use crate::virtual_region::copy_constraints::{CopyConstraintManager, SharedCopyConstraintManager}; +use crate::AssignedValue; /// Raw (physical) assigned cell in Plonkish arithmetization. #[cfg(feature = "halo2-axiom")] @@ -71,3 +73,43 @@ pub fn raw_constrain_equal(region: &mut Region, left: Cell, right: #[cfg(not(feature = "halo2-axiom"))] region.constrain_equal(left, right).unwrap(); } + +/// Assign virtual cell to raw halo2 cell in column `column` at row offset `offset` within the `region`. +/// Stores the mapping between `virtual_cell` and the raw assigned cell in `copy_manager`, if provided. +/// +/// `copy_manager` **must** be provided unless you are only doing witness generation +/// without constraints. +pub fn assign_virtual_to_raw<'v, F: Field + Ord>( + region: &mut Region, + column: Column, + offset: usize, + virtual_cell: AssignedValue, + copy_manager: Option<&SharedCopyConstraintManager>, +) -> Halo2AssignedCell<'v, F> { + let raw = raw_assign_advice(region, column, offset, Value::known(virtual_cell.value)); + if let Some(copy_manager) = copy_manager { + let mut copy_manager = copy_manager.lock().unwrap(); + let cell = virtual_cell.cell.unwrap(); + copy_manager.assigned_advices.insert(cell, raw.cell()); + drop(copy_manager); + } + raw +} + +/// Constrains that `virtual` is equal to `external`. The `virtual` cell must have +/// **already** been raw assigned, with the raw assigned cell stored in `copy_manager`. +/// +/// This should only be called when `witness_gen_only` is false, otherwise it will panic. +/// +/// ## Panics +/// If witness generation only mode is true. +pub fn constrain_virtual_equals_external( + region: &mut Region, + virtual_cell: AssignedValue, + external_cell: Cell, + copy_manager: &CopyConstraintManager, +) { + let ctx_cell = virtual_cell.cell.unwrap(); + let acell = copy_manager.assigned_advices.get(&ctx_cell).expect("cell not assigned"); + region.constrain_equal(*acell, external_cell); +} diff --git a/halo2-base/src/virtual_region/lookups.rs b/halo2-base/src/virtual_region/lookups.rs index e41875d4..fa7ec02d 100644 --- a/halo2-base/src/virtual_region/lookups.rs +++ b/halo2-base/src/virtual_region/lookups.rs @@ -8,7 +8,7 @@ use crate::halo2_proofs::{ circuit::{Region, Value}, plonk::{Advice, Column}, }; -use crate::utils::halo2::raw_assign_advice; +use crate::utils::halo2::{constrain_virtual_equals_external, raw_assign_advice}; use crate::{AssignedValue, ContextTag}; use super::copy_constraints::SharedCopyConstraintManager; @@ -125,6 +125,7 @@ impl VirtualRegionManager type Config = Vec<[Column; ADVICE_COLS]>; fn assign_raw(&self, config: &Self::Config, region: &mut Region) { + let copy_manager = (!self.witness_gen_only).then(|| self.copy_manager().lock().unwrap()); let cells_to_lookup = self.cells_to_lookup.lock().unwrap(); // Copy the cells to the config columns, going left to right, then top to bottom. // Will panic if out of rows @@ -138,12 +139,8 @@ impl VirtualRegionManager for (advice, &column) in advices.iter().zip(config[lookup_col].iter()) { let bcell = raw_assign_advice(region, column, lookup_offset, Value::known(advice.value)); - if !self.witness_gen_only { - let ctx_cell = advice.cell.unwrap(); - let copy_manager = self.copy_manager.lock().unwrap(); - let acell = - copy_manager.assigned_advices.get(&ctx_cell).expect("cell not assigned"); - region.constrain_equal(*acell, bcell.cell()); + if let Some(copy_manager) = copy_manager.as_ref() { + constrain_virtual_equals_external(region, *advice, bcell.cell(), copy_manager); } } diff --git a/halo2-base/src/virtual_region/lookups/basic.rs b/halo2-base/src/virtual_region/lookups/basic.rs index 018fced4..6c2422b2 100644 --- a/halo2-base/src/virtual_region/lookups/basic.rs +++ b/halo2-base/src/virtual_region/lookups/basic.rs @@ -1,18 +1,20 @@ +use std::iter::zip; + use crate::{ halo2_proofs::{ circuit::{Layouter, Region, Value}, halo2curves::ff::Field, - plonk::{Advice, Column, ConstraintSystem, Phase}, + plonk::{Advice, Column, ConstraintSystem, Fixed, Phase}, poly::Rotation, }, utils::{ - halo2::{raw_assign_advice, Halo2AssignedCell}, + halo2::{ + assign_virtual_to_raw, constrain_virtual_equals_external, raw_assign_advice, + raw_assign_fixed, + }, ScalarField, }, - virtual_region::{ - copy_constraints::SharedCopyConstraintManager, lookups::LookupAnyManager, - manager::VirtualRegionManager, - }, + virtual_region::copy_constraints::SharedCopyConstraintManager, AssignedValue, }; @@ -24,12 +26,27 @@ use crate::{ /// /// We can have multiple sets of dedicated columns to be looked up: these can be specified /// when calling `new`, but typically we just need 1 set. +/// +/// The `table` consists of advice columns. Since this table may have poisoned rows (blinding factors), +/// we use a fixed column `table_selector` which is default 0 and only 1 on enabled rows of the table. +/// The dynamic lookup will check that for `(key, key_is_enabled)` in `to_lookup` we have `key` matches one of +/// the rows in `table` where `table_selector == key_is_enabled`. +/// Reminder: the Halo2 lookup argument will ignore the poisoned rows in `to_lookup` +/// (see [https://zcash.github.io/halo2/design/proving-system/lookup.html#zero-knowledge-adjustment]), but it will +/// not ignore the poisoned rows in `table`. +/// +/// Part of this design consideration is to allow a key of `[F::ZERO; KEY_COL]` to still be used as a valid key +/// in the lookup argument. By default, unfilled rows in `to_lookup` will be all zeros; we require +/// at least one row in `table` where `table_is_enabled = 0` and the rest of the row in `table` are also 0s. #[derive(Clone, Debug)] pub struct BasicDynLookupConfig { - /// Columns for cells to be looked up. - pub to_lookup: Vec<[Column; KEY_COL]>, + /// Columns for cells to be looked up. Consists of `(key, key_is_enabled)`. + pub to_lookup: Vec<([Column; KEY_COL], Column)>, /// Table to look up against. pub table: [Column; KEY_COL], + /// Selector to enable a row in `table` to actually be part of the lookup table. This is to prevent + /// blinding factors in `table` advice columns from being used in the lookup. + pub table_is_enabled: Column, } impl BasicDynLookupConfig { @@ -42,44 +59,95 @@ impl BasicDynLookupConfig { num_lu_sets: usize, ) -> Self { let mut make_columns = || { - [(); KEY_COL].map(|_| { + let advices = [(); KEY_COL].map(|_| { let advice = meta.advice_column_in(phase()); meta.enable_equality(advice); advice - }) + }); + let is_enabled = meta.fixed_column(); + (advices, is_enabled) }; - let table = make_columns(); + let (table, table_is_enabled) = make_columns(); let to_lookup: Vec<_> = (0..num_lu_sets).map(|_| make_columns()).collect(); - for to_lookup in &to_lookup { + for (key, key_is_enabled) in &to_lookup { meta.lookup_any("dynamic lookup table", |meta| { let table = table.map(|c| meta.query_advice(c, Rotation::cur())); - let to_lu = to_lookup.map(|c| meta.query_advice(c, Rotation::cur())); - to_lu.into_iter().zip(table).collect() + let table_is_enabled = meta.query_fixed(table_is_enabled, Rotation::cur()); + let key = key.map(|c| meta.query_advice(c, Rotation::cur())); + let key_is_enabled = meta.query_fixed(*key_is_enabled, Rotation::cur()); + zip(key, table).chain([(key_is_enabled, table_is_enabled)]).collect() }); } - Self { table, to_lookup } + Self { table_is_enabled, table, to_lookup } } /// Assign managed lookups - pub fn assign_managed_lookups( + /// + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_to_lookup_to_raw( &self, mut layouter: impl Layouter, - lookup_manager: &LookupAnyManager, + keys: impl IntoIterator; KEY_COL]>, + copy_manager: Option<&SharedCopyConstraintManager>, ) { + #[cfg(not(feature = "halo2-axiom"))] + let keys = keys.into_iter().collect::>(); layouter .assign_region( - || "Managed lookup advice", + || "[BasicDynLookupConfig] Advice cells to lookup", |mut region| { - lookup_manager.assign_raw(&self.to_lookup, &mut region); + self.assign_virtual_to_lookup_to_raw_from_offset( + &mut region, + keys, + 0, + copy_manager, + ); Ok(()) }, ) .unwrap(); } - /// Assign virtual table to raw + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_to_lookup_to_raw_from_offset( + &self, + region: &mut Region, + keys: impl IntoIterator; KEY_COL]>, + mut offset: usize, + copy_manager: Option<&SharedCopyConstraintManager>, + ) { + let copy_manager = copy_manager.map(|c| c.lock().unwrap()); + // Copied from `LookupAnyManager::assign_raw` but modified to set `key_is_enabled` to 1. + // Copy the cells to the config columns, going left to right, then top to bottom. + // Will panic if out of rows + let mut lookup_col = 0; + for key in keys { + if lookup_col >= self.to_lookup.len() { + lookup_col = 0; + offset += 1; + } + let (key_col, key_is_enabled_col) = self.to_lookup[lookup_col]; + // set key_is_enabled to 1 + raw_assign_fixed(region, key_is_enabled_col, offset, F::ONE); + for (advice, column) in zip(key, key_col) { + let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value)); + if let Some(copy_manager) = copy_manager.as_ref() { + constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager); + } + } + + lookup_col += 1; + } + } + + /// Assign virtual table to raw. + /// + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. pub fn assign_virtual_table_to_raw( &self, mut layouter: impl Layouter, @@ -90,7 +158,7 @@ impl BasicDynLookupConfig { let rows = rows.into_iter().collect::>(); layouter .assign_region( - || "Dynamic Lookup Table", + || "[BasicDynLookupConfig] Dynamic Lookup Table", |mut region| { self.assign_virtual_table_to_raw_from_offset( &mut region, @@ -113,33 +181,21 @@ impl BasicDynLookupConfig { &self, region: &mut Region, rows: impl IntoIterator; KEY_COL]>, - offset: usize, + mut offset: usize, copy_manager: Option<&SharedCopyConstraintManager>, ) { - for (i, row) in rows.into_iter().enumerate() { + for row in rows { + // Enable this row in the table + raw_assign_fixed(region, self.table_is_enabled, offset, F::ONE); for (col, virtual_cell) in self.table.into_iter().zip(row) { - assign_virtual_to_raw(region, col, offset + i, virtual_cell, copy_manager); + assign_virtual_to_raw(region, col, offset, virtual_cell, copy_manager); } + offset += 1; + } + // always assign one disabled row with all 0s, so disabled to_lookup works for sure + raw_assign_fixed(region, self.table_is_enabled, offset, F::ZERO); + for col in self.table { + raw_assign_advice(region, col, offset, Value::known(F::ZERO)); } } } - -/// Assign virtual cell to raw halo2 cell. -/// `copy_manager` **must** be provided unless you are only doing witness generation -/// without constraints. -pub fn assign_virtual_to_raw<'v, F: ScalarField>( - region: &mut Region, - column: Column, - offset: usize, - virtual_cell: AssignedValue, - copy_manager: Option<&SharedCopyConstraintManager>, -) -> Halo2AssignedCell<'v, F> { - let raw = raw_assign_advice(region, column, offset, Value::known(virtual_cell.value)); - if let Some(copy_manager) = copy_manager { - let mut copy_manager = copy_manager.lock().unwrap(); - let cell = virtual_cell.cell.unwrap(); - copy_manager.assigned_advices.insert(cell, raw.cell()); - drop(copy_manager); - } - raw -} diff --git a/halo2-base/src/virtual_region/tests/lookups/memory.rs b/halo2-base/src/virtual_region/tests/lookups/memory.rs index 66df4085..8ccb4a70 100644 --- a/halo2-base/src/virtual_region/tests/lookups/memory.rs +++ b/halo2-base/src/virtual_region/tests/lookups/memory.rs @@ -1,11 +1,17 @@ -use crate::halo2_proofs::{ - arithmetic::Field, - circuit::{Layouter, SimpleFloorPlanner, Value}, - dev::MockProver, - halo2curves::bn256::Fr, - plonk::{keygen_pk, keygen_vk, Advice, Circuit, Column, ConstraintSystem, Error}, - poly::Rotation, +use std::any::TypeId; + +use crate::{ + halo2_proofs::{ + arithmetic::Field, + circuit::{Layouter, SimpleFloorPlanner}, + dev::MockProver, + halo2curves::bn256::Fr, + plonk::{keygen_pk, keygen_vk, Assigned, Circuit, ConstraintSystem, Error}, + }, + virtual_region::lookups::basic::BasicDynLookupConfig, + AssignedValue, ContextCell, }; +use halo2_proofs_axiom::plonk::FirstPhase; use rand::{rngs::StdRng, Rng, SeedableRng}; use test_log::test; @@ -16,25 +22,22 @@ use crate::{ }, utils::{ fs::gen_srs, - halo2::raw_assign_advice, testing::{check_proof, gen_proof}, ScalarField, }, - virtual_region::{lookups::LookupAnyManager, manager::VirtualRegionManager}, + virtual_region::manager::VirtualRegionManager, }; #[derive(Clone, Debug)] struct RAMConfig { cpu: FlexGateConfig, - copy: Vec<[Column; 2]>, - // dynamic lookup table - memory: [Column; 2], + memory: BasicDynLookupConfig<2>, } #[derive(Clone, Default)] struct RAMConfigParams { cpu: FlexGateConfigParams, - copy_columns: usize, + num_lu_sets: usize, } struct RAMCircuit { @@ -44,7 +47,7 @@ struct RAMCircuit { ptrs: [usize; CYCLES], cpu: SinglePhaseCoreManager, - ram: LookupAnyManager, + mem_access: Vec<[AssignedValue; 2]>, params: RAMConfigParams, } @@ -57,8 +60,8 @@ impl RAMCircuit { witness_gen_only: bool, ) -> Self { let cpu = SinglePhaseCoreManager::new(witness_gen_only, Default::default()); - let ram = LookupAnyManager::new(witness_gen_only, cpu.copy_manager.clone()); - Self { memory, ptrs, cpu, ram, params } + let mem_access = vec![]; + Self { memory, ptrs, cpu, mem_access, params } } fn compute(&mut self) { @@ -67,9 +70,9 @@ impl RAMCircuit { let mut sum = ctx.load_constant(F::ZERO); for &ptr in &self.ptrs { let value = self.memory[ptr]; - let ptr = ctx.load_witness(F::from(ptr as u64 + 1)); + let ptr = ctx.load_witness(F::from(ptr as u64)); let value = ctx.load_witness(value); - self.ram.add_lookup((ctx.type_id(), ctx.id()), [ptr, value]); + self.mem_access.push([ptr, value]); sum = gate.add(ctx, sum, value); } } @@ -89,30 +92,12 @@ impl Circuit for RAMCircuit { } fn configure_with_params(meta: &mut ConstraintSystem, params: Self::Params) -> Self::Config { - let k = params.cpu.k; - let mut cpu = FlexGateConfig::configure(meta, params.cpu); - let copy: Vec<_> = (0..params.copy_columns) - .map(|_| { - [(); 2].map(|_| { - let advice = meta.advice_column(); - meta.enable_equality(advice); - advice - }) - }) - .collect(); - let mem = [meta.advice_column(), meta.advice_column()]; - - for copy in © { - meta.lookup_any("dynamic memory lookup table", |meta| { - let mem = mem.map(|c| meta.query_advice(c, Rotation::cur())); - let copy = copy.map(|c| meta.query_advice(c, Rotation::cur())); - vec![(copy[0].clone(), mem[0].clone()), (copy[1].clone(), mem[1].clone())] - }); - } + let memory = BasicDynLookupConfig::new(meta, || FirstPhase, params.num_lu_sets); + let cpu = FlexGateConfig::configure(meta, params.cpu); + log::info!("Poisoned rows: {}", meta.minimum_rows()); - cpu.max_rows = (1 << k) - meta.minimum_rows(); - RAMConfig { cpu, copy, memory: mem } + RAMConfig { cpu, memory } } fn configure(_: &mut ConstraintSystem) -> Self::Config { @@ -124,21 +109,48 @@ impl Circuit for RAMCircuit { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { + // Make purely virtual cells so we can raw assign them + let memory = self.memory.iter().enumerate().map(|(i, value)| { + let idx = Assigned::Trivial(F::from(i as u64)); + let idx = AssignedValue { + value: idx, + cell: Some(ContextCell::new(TypeId::of::>(), 0, i)), + }; + let value = Assigned::Trivial(*value); + let value = AssignedValue { + value, + cell: Some(ContextCell::new(TypeId::of::>(), 1, i)), + }; + [idx, value] + }); + + let copy_manager = (!self.cpu.witness_gen_only()).then_some(&self.cpu.copy_manager); + + config.memory.assign_virtual_table_to_raw( + layouter.namespace(|| "memory"), + memory, + copy_manager, + ); + layouter.assign_region( - || "RAM Circuit", + || "cpu", |mut region| { - // Raw assign the private memory inputs - for (i, &value) in self.memory.iter().enumerate() { - // I think there will always be (0, 0) in the table so we index starting from 1 - let idx = Value::known(F::from(i as u64 + 1)); - raw_assign_advice(&mut region, config.memory[0], i, idx); - raw_assign_advice(&mut region, config.memory[1], i, Value::known(value)); - } self.cpu.assign_raw( &(config.cpu.basic_gates[0].clone(), config.cpu.max_rows), &mut region, ); - self.ram.assign_raw(&config.copy, &mut region); + Ok(()) + }, + )?; + config.memory.assign_virtual_to_lookup_to_raw( + layouter.namespace(|| "memory accesses"), + self.mem_access.clone(), + copy_manager, + ); + // copy constraints at the very end for safety: + layouter.assign_region( + || "copy constraints", + |mut region| { self.cpu.copy_manager.assign_raw(&config.cpu.constants, &mut region); Ok(()) }, @@ -155,7 +167,6 @@ fn test_ram_mock() { let memory: Vec<_> = (0..mem_len).map(|_| Fr::random(&mut rng)).collect(); let ptrs = [(); CYCLES].map(|_| rng.gen_range(0..memory.len())); let usable_rows = 2usize.pow(k) - 11; // guess - let copy_columns = CYCLES / usable_rows + 1; let params = RAMConfigParams::default(); let mut circuit = RAMCircuit::new(memory, ptrs, params, false); circuit.compute(); @@ -166,10 +177,43 @@ fn test_ram_mock() { num_advice_per_phase: vec![num_advice], num_fixed: 1, }; - circuit.params.copy_columns = copy_columns; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; MockProver::run(k, &circuit, vec![]).unwrap().assert_satisfied(); } +#[test] +#[should_panic = "called `Result::unwrap()` on an `Err` value: [Lookup dynamic lookup table(index: 2) is not satisfied in Region 2 ('[BasicDynLookupConfig] Advice cells to lookup') at offset 16]"] +fn test_ram_mock_failed_access() { + let k = 5u32; + const CYCLES: usize = 50; + let mut rng = StdRng::seed_from_u64(0); + let mem_len = 16usize; + let memory: Vec<_> = (0..mem_len).map(|_| Fr::random(&mut rng)).collect(); + let ptrs = [(); CYCLES].map(|_| rng.gen_range(0..memory.len())); + let usable_rows = 2usize.pow(k) - 11; // guess + let params = RAMConfigParams::default(); + let mut circuit = RAMCircuit::new(memory, ptrs, params, false); + circuit.compute(); + + // === PRANK === + // Try to claim memory[0] = 0 + let ctx = circuit.cpu.main(); + let ptr = ctx.load_witness(Fr::ZERO); + let value = ctx.load_witness(Fr::ZERO); + circuit.mem_access.push([ptr, value]); + // === end prank === + + // auto-configuration stuff + let num_advice = circuit.cpu.total_advice() / usable_rows + 1; + circuit.params.cpu = FlexGateConfigParams { + k: k as usize, + num_advice_per_phase: vec![num_advice], + num_fixed: 1, + }; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; + MockProver::run(k, &circuit, vec![]).unwrap().verify().unwrap(); +} + #[test] fn test_ram_prover() { let k = 10u32; @@ -182,7 +226,6 @@ fn test_ram_prover() { let ptrs = [0; CYCLES]; let usable_rows = 2usize.pow(k) - 11; // guess - let copy_columns = CYCLES / usable_rows + 1; let params = RAMConfigParams::default(); let mut circuit = RAMCircuit::new(memory, ptrs, params, false); circuit.compute(); @@ -192,7 +235,7 @@ fn test_ram_prover() { num_advice_per_phase: vec![num_advice], num_fixed: 1, }; - circuit.params.copy_columns = copy_columns; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; let params = gen_srs(k); let vk = keygen_vk(¶ms, &circuit).unwrap();