Skip to content
This repository has been archived by the owner on Nov 4, 2024. It is now read-only.

Commit

Permalink
Require the import of Halo2 table columns to be separate from general…
Browse files Browse the repository at this point in the history
… fixed columns
  • Loading branch information
alxkzmn committed Jul 22, 2024
1 parent 4b077b2 commit b36689c
Show file tree
Hide file tree
Showing 7 changed files with 74 additions and 49 deletions.
8 changes: 7 additions & 1 deletion src/frontend/dsl/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -82,6 +82,12 @@ impl<F, TG: TraceGenerator<F>> CircuitContext<F, TG> {
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<F> {
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.
Expand Down
1 change: 1 addition & 0 deletions src/frontend/python/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
47 changes: 6 additions & 41 deletions src/plonkish/backend/halo2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
},
},
Expand Down Expand Up @@ -205,7 +205,7 @@ impl<F: PrimeField + From<u64> + Hash> ChiquitoHalo2<F> {
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
}
Expand Down Expand Up @@ -270,8 +270,8 @@ impl<F: PrimeField + From<u64> + Hash> ChiquitoHalo2<F> {
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,
Expand Down Expand Up @@ -357,7 +357,7 @@ impl<F: PrimeField + From<u64> + Hash> ChiquitoHalo2<F> {

meta.query_advice(*c, Rotation(rotation))
}
cFixed | Halo2Fixed => {
cFixed | Halo2Fixed | Halo2Table => {
let c = self
.fixed_columns
.get(&column.uuid())
Expand Down Expand Up @@ -403,7 +403,7 @@ impl<F: PrimeField + From<u64> + Hash> ChiquitoHalo2<F> {
.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 {
Expand Down Expand Up @@ -884,38 +884,3 @@ pub(crate) fn chiquito2Halo2<F: PrimeField + From<u64> + Hash>(
) -> ChiquitoHalo2<F> {
ChiquitoHalo2::new(circuit)
}

impl<F> ExpressionWithColumn for Expression<F> {
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
}
}
13 changes: 13 additions & 0 deletions src/plonkish/compiler/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -587,8 +587,21 @@ fn add_halo2_columns<F, TG: TraceGenerator<F>>(
})
.collect();

let halo2_table_columns: Vec<Column> = 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)]
Expand Down
3 changes: 3 additions & 0 deletions src/plonkish/compiler/unit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,7 @@ impl<F: Clone, TG: TraceGenerator<F>> From<&astCircuit<F, TG>> for CompilationUn
ctype: ColumnType::Fixed,
halo2_advice: None,
halo2_fixed: None,
halo2_table: None,
phase: 0,
id: uuid(),
})
Expand All @@ -240,6 +241,7 @@ impl<F: Clone, TG: TraceGenerator<F>> From<&astCircuit<F, TG>> for CompilationUn
ctype: ColumnType::Fixed,
halo2_advice: None,
halo2_fixed: None,
halo2_table: None,
phase: 0,
id: uuid(),
},
Expand All @@ -253,6 +255,7 @@ impl<F: Clone, TG: TraceGenerator<F>> From<&astCircuit<F, TG>> for CompilationUn
ctype: ColumnType::Fixed,
halo2_advice: None,
halo2_fixed: None,
halo2_table: None,
phase: 0,
id: uuid(),
},
Expand Down
26 changes: 24 additions & 2 deletions src/plonkish/ir/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ pub enum ColumnType {
Fixed,
Halo2Advice,
Halo2Fixed,
Halo2Table,
}

#[derive(Clone, Debug)]
Expand All @@ -76,6 +77,7 @@ pub struct Column {
pub ctype: ColumnType,
pub halo2_advice: Option<ImportedHalo2Advice>,
pub halo2_fixed: Option<ImportedHalo2Fixed>,
pub halo2_table: Option<ImportedHalo2Fixed>,

pub phase: usize,

Expand All @@ -91,6 +93,7 @@ impl Column {
phase,
halo2_advice: None,
halo2_fixed: None,
halo2_table: None,
}
}

Expand All @@ -102,6 +105,7 @@ impl Column {
phase: 0,
halo2_advice: None,
halo2_fixed: None,
halo2_table: None,
}
}

Expand All @@ -116,6 +120,7 @@ impl Column {
ctype: ColumnType::Halo2Advice,
halo2_advice: Some(halo2_advice),
halo2_fixed: None,
halo2_table: None,
}
}

Expand All @@ -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<A: Into<String>>(
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),
}
}

Expand Down Expand Up @@ -191,8 +212,9 @@ impl<F> ExpressionWithColumn for PolyExpr<F> {
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, _) => {
Expand Down
25 changes: 20 additions & 5 deletions src/sbpir/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -27,6 +27,7 @@ pub struct SBPIR<F, TG: TraceGenerator<F> = DSLTraceGenerator<F>> {
pub fixed_signals: Vec<FixedSignal>,
pub halo2_advice: Vec<ImportedHalo2Advice>,
pub halo2_fixed: Vec<ImportedHalo2Fixed>,
pub halo2_table: Vec<ImportedHalo2Fixed>,
pub exposed: Vec<(Queriable<F>, ExposeOffset)>,

pub annotations: HashMap<UUID, String>,
Expand All @@ -51,6 +52,7 @@ impl<F: Debug, TG: TraceGenerator<F>> Debug for SBPIR<F, TG> {
.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)
Expand All @@ -71,6 +73,7 @@ impl<F, TG: TraceGenerator<F>> Default for SBPIR<F, TG> {
fixed_signals: Default::default(),
halo2_advice: Default::default(),
halo2_fixed: Default::default(),
halo2_table: Default::default(),
exposed: Default::default(),

num_steps: Default::default(),
Expand Down Expand Up @@ -160,12 +163,21 @@ impl<F, TG: TraceGenerator<F>> SBPIR<F, TG> {
name: &str,
column: Halo2Column<Fixed>,
) -> 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<N: Into<String>>(&mut self, handler: StepTypeHandler, name: N) {
Expand Down Expand Up @@ -196,6 +208,7 @@ impl<F, TG: TraceGenerator<F>> SBPIR<F, TG> {
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.
Expand All @@ -217,6 +230,7 @@ impl<F, TG: TraceGenerator<F>> SBPIR<F, TG> {
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,
Expand Down Expand Up @@ -254,6 +268,7 @@ impl<F: Clone + Field, TG: TraceGenerator<F>> SBPIR<F, TG> {
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.
Expand Down

0 comments on commit b36689c

Please sign in to comment.