diff --git a/keccak256/src/permutation/circuit.rs b/keccak256/src/permutation/circuit.rs index 8b1a8a62d0..4a12953305 100644 --- a/keccak256/src/permutation/circuit.rs +++ b/keccak256/src/permutation/circuit.rs @@ -85,7 +85,13 @@ impl KeccakFConfig { // Mixing will make sure that the flag is binary constrained and that // the out state matches the expected result. - let mixing_config = MixingConfig::configure(meta, &from_b9_table, state, generic.clone()); + let mixing_config = MixingConfig::configure( + meta, + &from_b9_table, + state, + generic.clone(), + stackable.clone(), + ); // Allocate the `out state correctness` gate selector let q_out = meta.selector(); diff --git a/keccak256/src/permutation/mixing.rs b/keccak256/src/permutation/mixing.rs index 0a6290ae54..37e9e3f268 100644 --- a/keccak256/src/permutation/mixing.rs +++ b/keccak256/src/permutation/mixing.rs @@ -1,13 +1,13 @@ use super::super::arith_helpers::*; use super::generic::GenericConfig; -use super::tables::FromBase9TableConfig; +use super::tables::{FromBase9TableConfig, StackableTable}; use super::{absorb::AbsorbConfig, base_conversion::BaseConversionConfig, iota::IotaConstants}; use crate::common::*; use crate::keccak_arith::KeccakFArith; use eth_types::Field; use halo2_proofs::{ circuit::{AssignedCell, Layouter, Region}, - plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector}, + plonk::{Advice, Column, ConstraintSystem, Error, Selector}, poly::Rotation, }; use std::convert::TryInto; @@ -19,9 +19,9 @@ pub struct MixingConfig { base_conv_config: BaseConversionConfig, state: [Column; 25], flag: Column, - q_flag: Selector, q_out_copy: Selector, generic: GenericConfig, + stackable: StackableTable, } impl MixingConfig { @@ -30,43 +30,10 @@ impl MixingConfig { table: &FromBase9TableConfig, state: [Column; 25], generic: GenericConfig, + stackable: StackableTable, ) -> MixingConfig { - // Allocate space for the flag column from which we will copy to all of - // the sub-configs. let flag = meta.advice_column(); meta.enable_equality(flag); - - let q_flag = meta.selector(); - - meta.create_gate("Ensure flag consistency", |meta| { - let q_flag = meta.query_selector(q_flag); - - let negated_flag = meta.query_advice(flag, Rotation::next()); - let flag = meta.query_advice(flag, Rotation::cur()); - // We do a trick which consists on multiplying an internal selector - // which is always active by the actual `negated_flag` - // which will then enable or disable the gate. - // - // Force that `flag + negated_flag = 1`. - // This ensures that flag = !negated_flag. - let flag_consistency = - (flag.clone() + negated_flag.clone()) - Expression::Constant(F::one()); - - // Define bool constraint for flags. - // Based on: `(1-flag) * flag = 0` only if `flag` is boolean. - let bool_constraint = |flag: Expression| -> Expression { - (Expression::Constant(F::one()) - flag.clone()) * flag - }; - - // Add a constraint that sums up the results of the two branches - // constraining it to be equal to `out_state`. - [ - q_flag.clone() * flag_consistency, - q_flag.clone() * bool_constraint(flag), - q_flag * bool_constraint(negated_flag), - ] - }); - // We mix -> Flag = true let absorb_config = AbsorbConfig::configure(meta, state); @@ -107,43 +74,12 @@ impl MixingConfig { base_conv_config, state, flag, - q_flag, q_out_copy, generic, + stackable, } } - /// Enforce flag constraints - pub fn enforce_flag_consistency( - &self, - layouter: &mut impl Layouter, - flag_bool: bool, - ) -> Result<(AssignedCell, AssignedCell), Error> { - layouter.assign_region( - || "Flag and Negated flag assignation", - |mut region| { - self.q_flag.enable(&mut region, 0)?; - // Witness `is_mixing` flag - let flag = region.assign_advice( - || "witness is_mixing", - self.flag, - 0, - || Ok(F::from(flag_bool as u64)), - )?; - - // Witness negated `is_mixing` flag - let negated_flag = region.assign_advice( - || "witness negated is_mixing", - self.flag, - 1, - || Ok(F::from(!flag_bool as u64)), - )?; - - Ok((flag, negated_flag)) - }, - ) - } - /// Enforce flag constraints pub fn assign_out_mixing_states( &self, @@ -203,7 +139,9 @@ impl MixingConfig { next_mixing: Option<[F; NEXT_INPUTS_LANES]>, ) -> Result<[AssignedCell; 25], Error> { // Enforce flag constraints and witness them. - let (flag, negated_flag) = self.enforce_flag_consistency(layouter, flag_bool)?; + let (flag, negated_flag) = self + .stackable + .assign_boolean_flag(layouter, Some(flag_bool))?; // If we don't mix: // IotaB9 @@ -291,10 +229,12 @@ impl MixingConfig { mod tests { use super::*; use crate::common::{State, ROUND_CONSTANTS}; - use halo2_proofs::circuit::Layouter; - use halo2_proofs::pairing::bn256::Fr as Fp; - use halo2_proofs::plonk::{ConstraintSystem, Error}; - use halo2_proofs::{circuit::SimpleFloorPlanner, dev::MockProver, plonk::Circuit}; + use halo2_proofs::{ + circuit::{Layouter, SimpleFloorPlanner}, + dev::MockProver, + pairing::bn256::Fr as Fp, + plonk::{Circuit, ConstraintSystem, Error, TableColumn}, + }; use itertools::Itertools; use pretty_assertions::assert_eq; use std::convert::TryInto; @@ -314,6 +254,7 @@ mod tests { struct MyConfig { mixing_conf: MixingConfig, table: FromBase9TableConfig, + stackable: StackableTable, } impl Circuit for MyCircuit { @@ -339,10 +280,20 @@ mod tests { let fixed = meta.fixed_column(); let generic = GenericConfig::configure(meta, state[0..3].try_into().unwrap(), fixed); + let table_cols: [TableColumn; 3] = (0..3) + .map(|_| meta.lookup_table_column()) + .collect_vec() + .try_into() + .unwrap(); + let stackable = + StackableTable::configure(meta, state[0..3].try_into().unwrap(), table_cols); + let mixing_conf = + MixingConfig::configure(meta, &table, state, generic, stackable.clone()); MyConfig { - mixing_conf: MixingConfig::configure(meta, &table, state, generic), + mixing_conf, table, + stackable, } } @@ -353,6 +304,7 @@ mod tests { ) -> Result<(), Error> { // Load the table config.table.load(&mut layouter)?; + config.stackable.load(&mut layouter)?; let offset: usize = 0; let in_state = layouter.assign_region( diff --git a/keccak256/src/permutation/tables.rs b/keccak256/src/permutation/tables.rs index ff8d8fcc4a..e73f07468a 100644 --- a/keccak256/src/permutation/tables.rs +++ b/keccak256/src/permutation/tables.rs @@ -24,6 +24,7 @@ enum TableTags { Range12 = 0, Range169, SpecialChunk, + BooleanFlag, } #[derive(Debug, Clone)] @@ -121,6 +122,22 @@ impl StackableTable { } Ok(offset) } + + fn load_boolean_flag(&self, table: &mut Table, offset: usize) -> Result { + let mut offset = offset; + for (left, right) in [(true, false), (false, true)] { + table.assign_cell( + || "tag boolean flag", + self.tag.1, + offset, + || Ok(F::from(TableTags::BooleanFlag as u64)), + )?; + table.assign_cell(|| "left", self.col1.1, offset, || Ok(F::from(left)))?; + table.assign_cell(|| "right", self.col2.1, offset, || Ok(F::from(right)))?; + offset += 1; + } + Ok(offset) + } pub(crate) fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { layouter.assign_table( || "stackable", @@ -134,7 +151,8 @@ impl StackableTable { { offset = self.load_range(&mut table, offset, tag, k)?; } - self.load_special_chunks(&mut table, offset)?; + offset = self.load_special_chunks(&mut table, offset)?; + self.load_boolean_flag(&mut table, offset)?; Ok(()) }, ) @@ -199,6 +217,40 @@ impl StackableTable { }, ) } + /// Output two boolean cells. Prover can choose to enable one and disable + /// another, but not both. + pub(crate) fn assign_boolean_flag( + &self, + layouter: &mut impl Layouter, + is_left: Option, + ) -> Result<(AssignedCell, AssignedCell), Error> { + layouter.assign_region( + || "lookup for boolean flag", + |mut region| { + let offset = 0; + self.q_enable.enable(&mut region, offset)?; + region.assign_advice_from_constant( + || "tag", + self.tag.0, + offset, + F::from(TableTags::BooleanFlag as u64), + )?; + let left = region.assign_advice( + || "left", + self.col1.0, + offset, + || is_left.map(|flag| F::from(flag)).ok_or(Error::Synthesis), + )?; + let right = region.assign_advice( + || "right", + self.col2.0, + offset, + || is_left.map(|flag| F::from(!flag)).ok_or(Error::Synthesis), + )?; + Ok((left, right)) + }, + ) + } } #[derive(Debug, Clone)]