From b36689c3b4cc8450d55d611ba782c4e8e9e2b8dc Mon Sep 17 00:00:00 2001 From: Alex Kuzmin Date: Mon, 22 Jul 2024 19:03:43 +0200 Subject: [PATCH] Require the import of Halo2 table columns to be separate from general fixed columns --- src/frontend/dsl/mod.rs | 8 +++++- src/frontend/python/mod.rs | 1 + src/plonkish/backend/halo2.rs | 47 +++++------------------------------ src/plonkish/compiler/mod.rs | 13 ++++++++++ src/plonkish/compiler/unit.rs | 3 +++ src/plonkish/ir/mod.rs | 26 +++++++++++++++++-- src/sbpir/mod.rs | 25 +++++++++++++++---- 7 files changed, 74 insertions(+), 49 deletions(-) diff --git a/src/frontend/dsl/mod.rs b/src/frontend/dsl/mod.rs index ac1708f1..edf37251 100644 --- a/src/frontend/dsl/mod.rs +++ b/src/frontend/dsl/mod.rs @@ -5,7 +5,7 @@ use crate::{ wit_gen::{FixedGenContext, StepInstance, TraceGenerator}, }; -use halo2_proofs::plonk::{Advice, Column as Halo2Column, Fixed}; +use halo2_proofs::plonk::{Advice, Column as Halo2Column, Fixed, TableColumn}; use trace::{DSLTraceGenerator, TraceContext}; use core::{fmt::Debug, hash::Hash}; @@ -82,6 +82,12 @@ impl> CircuitContext { Queriable::Halo2FixedQuery(self.circuit.add_halo2_fixed(name, column), 0) } + /// Imports a halo2 table column with a name string into the circuit and returns a + /// `Queriable` instance representing the imported column. + pub fn import_halo2_table(&mut self, name: &str, column: TableColumn) -> Queriable { + Queriable::Halo2FixedQuery(self.circuit.add_halo2_table(name, column), 0) + } + /// Adds a new step type with the specified name to the circuit and returns a /// `StepTypeHandler` instance. The `StepTypeHandler` instance can be used to define the /// step type using the `step_type_def` function. diff --git a/src/frontend/python/mod.rs b/src/frontend/python/mod.rs index 5323a838..0e4c1dfc 100644 --- a/src/frontend/python/mod.rs +++ b/src/frontend/python/mod.rs @@ -356,6 +356,7 @@ impl<'de> Visitor<'de> for CircuitVisitor { fixed_signals, halo2_advice: Default::default(), halo2_fixed: Default::default(), + halo2_table: Default::default(), exposed, num_steps, annotations, diff --git a/src/plonkish/backend/halo2.rs b/src/plonkish/backend/halo2.rs index 3cd76763..283fe1b5 100644 --- a/src/plonkish/backend/halo2.rs +++ b/src/plonkish/backend/halo2.rs @@ -48,7 +48,7 @@ use crate::{ assignments::Assignments, sc::{SuperAssignments, SuperCircuit}, Circuit, Column as cColumn, - ColumnType::{Advice as cAdvice, Fixed as cFixed, Halo2Advice, Halo2Fixed}, + ColumnType::{Advice as cAdvice, Fixed as cFixed, Halo2Advice, Halo2Fixed, Halo2Table}, ExpressionWithColumn, PolyExpr, }, }, @@ -205,7 +205,7 @@ impl + Hash> ChiquitoHalo2 { advice_columns.insert(column.uuid(), halo2_column); cs.annotate_lookup_any_column(halo2_column, || column.annotation.clone()); } - cFixed | Halo2Fixed => { + cFixed | Halo2Fixed | Halo2Table => { // Fixed columns require special handling regarding the type of query that is // only possible to determine by analyzing all subscircuits } @@ -270,8 +270,8 @@ impl + Hash> ChiquitoHalo2 { for (idx, (_, dest)) in lookup.exprs.iter().enumerate() { match dest { PolyExpr::Query((column, _, _), _) => { - if column.ctype == cFixed - || column.ctype == Halo2Fixed && self.has_single_fixed_query(column) + if column.ctype == cFixed && self.has_single_fixed_query(column) + || column.ctype == Halo2Table { single_fixed_queries.push(( lookup.exprs[idx].clone().0, @@ -357,7 +357,7 @@ impl + Hash> ChiquitoHalo2 { meta.query_advice(*c, Rotation(rotation)) } - cFixed | Halo2Fixed => { + cFixed | Halo2Fixed | Halo2Table => { let c = self .fixed_columns .get(&column.uuid()) @@ -403,7 +403,7 @@ impl + Hash> ChiquitoHalo2 { .for_each(|(row, (column, offset))| { let col_type: Columns = match column.ctype { cAdvice | Halo2Advice => Columns::Advice, - cFixed | Halo2Fixed => Columns::Fixed, + cFixed | Halo2Fixed | Halo2Table => Columns::Fixed, }; let index = if col_type == Columns::Advice { @@ -884,38 +884,3 @@ pub(crate) fn chiquito2Halo2 + Hash>( ) -> ChiquitoHalo2 { ChiquitoHalo2::new(circuit) } - -impl ExpressionWithColumn for Expression { - fn involves(&self, column: &cColumn) -> bool { - let mut is_in_expr = false; - match self { - Expression::Constant(_) => todo!(), - Expression::Selector(_) => todo!(), - Expression::Fixed(q) => { - if column.halo2_fixed.is_some() { - return column.halo2_fixed.as_ref().unwrap().column.index == q.column_index; - } - } - Expression::Advice(q) => { - if column.halo2_advice.is_some() { - return column.halo2_advice.as_ref().unwrap().column.index == q.column_index; - } - } - Expression::Instance(_) => {} - Expression::Challenge(_) => {} - Expression::Negated(e) => { - is_in_expr = e.involves(column); - } - Expression::Sum(e1, e2) => { - is_in_expr = e1.involves(column) || e2.involves(column); - } - Expression::Product(e1, e2) => { - is_in_expr = e1.involves(column) || e2.involves(column); - } - Expression::Scaled(e, _) => { - is_in_expr = e.involves(column); - } - } - is_in_expr - } -} diff --git a/src/plonkish/compiler/mod.rs b/src/plonkish/compiler/mod.rs index 50a14d05..d0d9b896 100644 --- a/src/plonkish/compiler/mod.rs +++ b/src/plonkish/compiler/mod.rs @@ -587,8 +587,21 @@ fn add_halo2_columns>( }) .collect(); + let halo2_table_columns: Vec = ast + .halo2_table + .iter() + .map(|signal| { + if let Some(annotation) = unit.annotations.get(&signal.uuid()) { + Column::new_halo2_table(format!("halo2 table {}", annotation), *signal) + } else { + Column::new_halo2_table("halo2 table", *signal) + } + }) + .collect(); + unit.columns.extend(halo2_advice_columns); unit.columns.extend(halo2_fixed_columns); + unit.columns.extend(halo2_table_columns); } #[cfg(test)] diff --git a/src/plonkish/compiler/unit.rs b/src/plonkish/compiler/unit.rs index cbd27888..924407d5 100644 --- a/src/plonkish/compiler/unit.rs +++ b/src/plonkish/compiler/unit.rs @@ -226,6 +226,7 @@ impl> From<&astCircuit> for CompilationUn ctype: ColumnType::Fixed, halo2_advice: None, halo2_fixed: None, + halo2_table: None, phase: 0, id: uuid(), }) @@ -240,6 +241,7 @@ impl> From<&astCircuit> for CompilationUn ctype: ColumnType::Fixed, halo2_advice: None, halo2_fixed: None, + halo2_table: None, phase: 0, id: uuid(), }, @@ -253,6 +255,7 @@ impl> From<&astCircuit> for CompilationUn ctype: ColumnType::Fixed, halo2_advice: None, halo2_fixed: None, + halo2_table: None, phase: 0, id: uuid(), }, diff --git a/src/plonkish/ir/mod.rs b/src/plonkish/ir/mod.rs index 96554901..cf288320 100644 --- a/src/plonkish/ir/mod.rs +++ b/src/plonkish/ir/mod.rs @@ -67,6 +67,7 @@ pub enum ColumnType { Fixed, Halo2Advice, Halo2Fixed, + Halo2Table, } #[derive(Clone, Debug)] @@ -76,6 +77,7 @@ pub struct Column { pub ctype: ColumnType, pub halo2_advice: Option, pub halo2_fixed: Option, + pub halo2_table: Option, pub phase: usize, @@ -91,6 +93,7 @@ impl Column { phase, halo2_advice: None, halo2_fixed: None, + halo2_table: None, } } @@ -102,6 +105,7 @@ impl Column { phase: 0, halo2_advice: None, halo2_fixed: None, + halo2_table: None, } } @@ -116,6 +120,7 @@ impl Column { ctype: ColumnType::Halo2Advice, halo2_advice: Some(halo2_advice), halo2_fixed: None, + halo2_table: None, } } @@ -130,6 +135,22 @@ impl Column { ctype: ColumnType::Halo2Fixed, halo2_advice: None, halo2_fixed: Some(halo2_fixed), + halo2_table: None, + } + } + + pub fn new_halo2_table>( + annotation: A, + halo2_table: ImportedHalo2Fixed, + ) -> Column { + Column { + annotation: annotation.into(), + id: uuid(), + phase: 0, + ctype: ColumnType::Halo2Table, + halo2_advice: None, + halo2_fixed: None, + halo2_table: Some(halo2_table), } } @@ -191,8 +212,9 @@ impl ExpressionWithColumn for PolyExpr { PolyExpr::Neg(e, _) | PolyExpr::Pow(e, _, _) => { is_in_expr = e.involves(column); } - PolyExpr::Halo2Expr(e, _) => { - is_in_expr = e.involves(column); + PolyExpr::Halo2Expr(_, _) => { + // No need for this check because we can distinguish by the imported Halo2 column + // type (simple fixed vs table) } PolyExpr::Const(_, _) => {} PolyExpr::MI(e, _) => { diff --git a/src/sbpir/mod.rs b/src/sbpir/mod.rs index 16935166..b81952b2 100644 --- a/src/sbpir/mod.rs +++ b/src/sbpir/mod.rs @@ -13,7 +13,7 @@ use crate::{ wit_gen::{FixedAssignment, FixedGenContext, NullTraceGenerator, TraceGenerator}, }; -use halo2_proofs::plonk::{Advice, Column as Halo2Column, ColumnType, Fixed}; +use halo2_proofs::plonk::{Advice, Column as Halo2Column, ColumnType, Fixed, TableColumn}; use self::query::Queriable; @@ -27,6 +27,7 @@ pub struct SBPIR = DSLTraceGenerator> { pub fixed_signals: Vec, pub halo2_advice: Vec, pub halo2_fixed: Vec, + pub halo2_table: Vec, pub exposed: Vec<(Queriable, ExposeOffset)>, pub annotations: HashMap, @@ -51,6 +52,7 @@ impl> Debug for SBPIR { .field("fixed_signals", &self.fixed_signals) .field("halo2_advice", &self.halo2_advice) .field("halo2_fixed", &self.halo2_fixed) + .field("halo2_table", &self.halo2_table) .field("exposed", &self.exposed) .field("annotations", &self.annotations) .field("fixed_assignments", &self.fixed_assignments) @@ -71,6 +73,7 @@ impl> Default for SBPIR { fixed_signals: Default::default(), halo2_advice: Default::default(), halo2_fixed: Default::default(), + halo2_table: Default::default(), exposed: Default::default(), num_steps: Default::default(), @@ -160,12 +163,21 @@ impl> SBPIR { name: &str, column: Halo2Column, ) -> ImportedHalo2Fixed { - let advice = ImportedHalo2Fixed::new(column, name.to_string()); + let fixed = ImportedHalo2Fixed::new(column, name.to_string()); - self.halo2_fixed.push(advice); - self.annotations.insert(advice.uuid(), name.to_string()); + self.halo2_fixed.push(fixed); + self.annotations.insert(fixed.uuid(), name.to_string()); - advice + fixed + } + + pub fn add_halo2_table(&mut self, name: &str, column: TableColumn) -> ImportedHalo2Fixed { + let fixed = ImportedHalo2Fixed::new(column.inner(), name.to_string()); + + self.halo2_table.push(fixed); + self.annotations.insert(fixed.uuid(), name.to_string()); + + fixed } pub fn add_step_type>(&mut self, handler: StepTypeHandler, name: N) { @@ -196,6 +208,7 @@ impl> SBPIR { fixed_signals: self.fixed_signals, halo2_advice: self.halo2_advice, halo2_fixed: self.halo2_fixed, + halo2_table: self.halo2_table, exposed: self.exposed, annotations: self.annotations, trace_generator: None, // Remove the trace. @@ -217,6 +230,7 @@ impl> SBPIR { fixed_signals: self.fixed_signals, halo2_advice: self.halo2_advice, halo2_fixed: self.halo2_fixed, + halo2_table: self.halo2_table, exposed: self.exposed, annotations: self.annotations, fixed_assignments: self.fixed_assignments, @@ -254,6 +268,7 @@ impl> SBPIR { fixed_signals: self.fixed_signals.clone(), halo2_advice: self.halo2_advice.clone(), halo2_fixed: self.halo2_fixed.clone(), + halo2_table: self.halo2_table.clone(), exposed: self.exposed.clone(), annotations: self.annotations.clone(), trace_generator: None, // Remove the trace.