diff --git a/src/hash.rs b/src/hash.rs index d179d0d..c06db7b 100644 --- a/src/hash.rs +++ b/src/hash.rs @@ -3,8 +3,8 @@ use crate::poseidon::primitives::{ ConstantLengthIden3, Domain, Hash, P128Pow5T3, Spec, VariableLengthIden3, }; -use halo2_proofs::arithmetic::FieldExt; use halo2_proofs::halo2curves::bn256::Fr; +use halo2_proofs::{arithmetic::FieldExt, circuit::AssignedCell}; /// indicate an field can be hashed in merkle tree (2 Fields to 1 Field) pub trait Hashable: FieldExt { @@ -56,7 +56,7 @@ impl MessageHashable for Fr { } } -use crate::poseidon::{PoseidonInstructions, Pow5Chip, Pow5Config, StateWord, Var}; +use crate::poseidon::{PermuteChip, PoseidonInstructions}; use halo2_proofs::{ circuit::{Chip, Layouter, Region, Value}, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, TableColumn}, @@ -65,19 +65,19 @@ use halo2_proofs::{ /// The config for poseidon hash circuit #[derive(Clone, Debug)] -pub struct PoseidonHashConfig { - permute_config: Pow5Config, +pub struct PoseidonHashConfig> { + permute_config: PC::Config, hash_table: [Column; 5], hash_table_aux: [Column; 6], control_aux: Column, s_sponge_continue: Column, - constants: [Column; 6], + constants: [Column; 1], control_step_range: TableColumn, s_table: Selector, s_custom: Selector, } -impl PoseidonHashConfig { +impl> PoseidonHashConfig { /// obtain the commitment index of hash table pub fn commitment_index(&self) -> [usize; 5] { self.hash_table.map(|col| col.index()) @@ -94,9 +94,8 @@ impl PoseidonHashConfig { hash_table: [Column; 5], step: usize, ) -> Self { - let state = [0; 3].map(|_| meta.advice_column()); - let partial_sbox = meta.advice_column(); - let constants = [0; 6].map(|_| meta.fixed_column()); + // TODO: remove this "constants". + let constants = [0; 1].map(|_| meta.fixed_column()); let s_table = meta.selector(); let s_custom = meta.selector(); @@ -236,13 +235,7 @@ impl PoseidonHashConfig { }); Self { - permute_config: Pow5Chip::configure::( - meta, - state, - partial_sbox, - constants[..3].try_into().unwrap(), //rc_a - constants[3..].try_into().unwrap(), //rc_b - ), + permute_config: PC::configure(meta), hash_table, hash_table_aux, control_aux, @@ -332,20 +325,26 @@ impl PoseidonHashTable { /// Represent the chip for Poseidon hash table #[derive(Debug)] -pub struct PoseidonHashChip<'d, Fp: FieldExt, const STEP: usize> { +pub struct PoseidonHashChip<'d, Fp: FieldExt, const STEP: usize, PC: PermuteChip> { calcs: usize, nil_msg_hash: Option, mpt_only: bool, data: &'d PoseidonHashTable, - config: PoseidonHashConfig, + config: PoseidonHashConfig, } -type PermutedState = Vec<[StateWord; 3]>; +type PermutedState = Vec<[Word; 3]>; -impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { +impl< + 'd, + Fp: Hashable, + const STEP: usize, + PC: PermuteChip + PoseidonInstructions, + > PoseidonHashChip<'d, Fp, STEP, PC> +{ ///construct the chip pub fn construct( - config: PoseidonHashConfig, + config: PoseidonHashConfig, data: &'d PoseidonHashTable, calcs: usize, mpt_only: bool, @@ -426,7 +425,7 @@ impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { &self, region: &mut Region<'_, Fp>, begin_offset: usize, - ) -> Result<(PermutedState, PermutedState), Error> { + ) -> Result<(PermutedState, PermutedState), Error> { let config = &self.config; let data = self.data; @@ -569,9 +568,9 @@ impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { //we directly specify the init state of permutation let c_start_arr: [_; 3] = c_start.try_into().expect("same size"); - states_in.push(c_start_arr.map(StateWord::from)); + states_in.push(c_start_arr.map(PC::Word::from)); let c_end_arr: [_; 3] = c_end.try_into().expect("same size"); - states_out.push(c_end_arr.map(StateWord::from)); + states_out.push(c_end_arr.map(PC::Word::from)); } // set the last row is "custom", a row both enabled and customed @@ -610,12 +609,11 @@ impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { let mut chip_finals = Vec::new(); for state in states_in { - let chip = Pow5Chip::construct(config.permute_config.clone()); + let chip = PC::construct(config.permute_config.clone()); - let final_state = - as PoseidonInstructions>::permute( - &chip, layouter, &state, - )?; + let final_state = >::permute( + &chip, layouter, &state, + )?; chip_finals.push(final_state); } @@ -625,6 +623,8 @@ impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { |mut region| { for (state, final_state) in states_out.iter().zip(chip_finals.iter()) { for (s_cell, final_cell) in state.iter().zip(final_state.iter()) { + let s_cell: AssignedCell = s_cell.clone().into(); + let final_cell: AssignedCell = final_cell.clone().into(); region.constrain_equal(s_cell.cell(), final_cell.cell())?; } } @@ -635,8 +635,10 @@ impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { } } -impl Chip for PoseidonHashChip<'_, Fp, STEP> { - type Config = PoseidonHashConfig; +impl> Chip + for PoseidonHashChip<'_, Fp, STEP, PC> +{ + type Config = PoseidonHashConfig; type Loaded = PoseidonHashTable; fn config(&self) -> &Self::Config { @@ -649,6 +651,11 @@ impl Chip for PoseidonHashChip<'_, Fp, STEP #[cfg(test)] mod tests { + use std::marker::PhantomData; + + use crate::poseidon::Pow5Chip; + use crate::septidon::SeptidonChip; + use super::*; use halo2_proofs::halo2curves::group::ff::PrimeField; use halo2_proofs::{circuit::SimpleFloorPlanner, plonk::Circuit}; @@ -701,19 +708,33 @@ mod tests { const TEST_STEP: usize = 32; // test circuit derived from table data - impl Circuit for PoseidonHashTable { - type Config = (PoseidonHashConfig, usize); + //#[derive(Clone, Default, Debug)] + struct TestCircuit> { + table: PoseidonHashTable, + _phantom: PhantomData, + } + + impl> TestCircuit { + pub fn new(table: PoseidonHashTable) -> Self { + TestCircuit { + table, + _phantom: PhantomData, + } + } + } + + impl + PoseidonInstructions::SpecType, 3, 2>> + Circuit for TestCircuit + { + type Config = (PoseidonHashConfig, usize); type FloorPlanner = SimpleFloorPlanner; fn without_witnesses(&self) -> Self { - Self { - ..Default::default() - } + Self::new(Default::default()) } - fn configure(meta: &mut ConstraintSystem) -> Self::Config { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { let hash_tbl = [0; 5].map(|_| meta.advice_column()); - ( PoseidonHashConfig::configure_sub(meta, hash_tbl, TEST_STEP), 4, @@ -723,14 +744,14 @@ mod tests { fn synthesize( &self, (config, max_rows): Self::Config, - mut layouter: impl Layouter, + mut layouter: impl Layouter, ) -> Result<(), Error> { - let chip = PoseidonHashChip::::construct( + let chip = PoseidonHashChip::::construct( config, - &self, + &self.table, max_rows, false, - Some(Fp::from(42u64)), + Some(Fr::from(42u64)), ); chip.load(&mut layouter) } @@ -770,6 +791,13 @@ mod tests { #[test] fn poseidon_hash_circuit() { + poseidon_hash_circuit_impl::>(); + poseidon_hash_circuit_impl::(); + } + + fn poseidon_hash_circuit_impl< + PC: PermuteChip + PoseidonInstructions::SpecType, 3, 2>, + >() { let message1 = [ Fr::from_str_vartime("1").unwrap(), Fr::from_str_vartime("2").unwrap(), @@ -781,16 +809,23 @@ mod tests { ]; let k = 8; - let circuit = PoseidonHashTable { + let circuit = TestCircuit::::new(PoseidonHashTable { inputs: vec![message1, message2], ..Default::default() - }; + }); let prover = MockProver::run(k, &circuit, vec![]).unwrap(); assert_eq!(prover.verify(), Ok(())); } #[test] fn poseidon_var_len_hash_circuit() { + poseidon_var_len_hash_circuit_impl::>(); + poseidon_var_len_hash_circuit_impl::(); + } + + fn poseidon_var_len_hash_circuit_impl< + PC: PermuteChip + PoseidonInstructions::SpecType, 3, 2>, + >() { let message1 = [ Fr::from_str_vartime("1").unwrap(), Fr::from_str_vartime("2").unwrap(), @@ -799,35 +834,34 @@ mod tests { let message2 = [Fr::from_str_vartime("50331648").unwrap(), Fr::zero()]; let k = 8; - let circuit = PoseidonHashTable { + let circuit = TestCircuit::::new( PoseidonHashTable { inputs: vec![message1, message2], controls: vec![Fr::from_u128(45), Fr::from_u128(13)], checks: vec![None, Some(Fr::from_str_vartime("15002881182751877599173281392790087382867290792048832034781070831698029191486").unwrap())], ..Default::default() - }; + }); let prover = MockProver::run(k, &circuit, vec![]).unwrap(); assert_eq!(prover.verify(), Ok(())); - let circuit = PoseidonHashTable { + let circuit = TestCircuit::::new(PoseidonHashTable { inputs: vec![message1, message2, message1], controls: vec![Fr::from_u128(64), Fr::from_u128(32), Fr::zero()], checks: Vec::new(), ..Default::default() - }; + }); let prover = MockProver::run(k, &circuit, vec![]).unwrap(); assert_eq!(prover.verify(), Ok(())); - let circuit = PoseidonHashTable:: { + let circuit = TestCircuit::::new(PoseidonHashTable:: { inputs: vec![message2], controls: vec![Fr::from_u128(13)], ..Default::default() - }; + }); let prover = MockProver::run(k, &circuit, vec![]).unwrap(); assert_eq!(prover.verify(), Ok(())); - - let circuit = PoseidonHashTable:: { + let circuit = TestCircuit::::new(PoseidonHashTable:: { ..Default::default() - }; + }); let prover = MockProver::run(k, &circuit, vec![]).unwrap(); assert_eq!(prover.verify(), Ok(())); } diff --git a/src/lib.rs b/src/lib.rs index 6543edd..dc69c08 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -8,6 +8,8 @@ pub mod hash; pub mod poseidon; +pub mod septidon; + pub use halo2_proofs::halo2curves::bn256::Fr as Bn256Fr; pub use hash::Hashable; diff --git a/src/poseidon.rs b/src/poseidon.rs index 83daae5..b346ee0 100644 --- a/src/poseidon.rs +++ b/src/poseidon.rs @@ -7,7 +7,7 @@ use std::marker::PhantomData; use halo2_proofs::{ arithmetic::{Field, FieldExt}, circuit::{AssignedCell, Chip, Layouter}, - plonk::Error, + plonk::{ConstraintSystem, Error}, }; mod pow5; @@ -15,6 +15,7 @@ pub use pow5::{Pow5Chip, Pow5Config, StateWord, Var}; pub mod primitives; use primitives::{Absorbing, ConstantLength, Domain, Spec, SpongeMode, Squeezing, State}; +use std::fmt::Debug as DebugT; /// A word from the padded input to a Poseidon sponge. #[derive(Clone, Debug)] @@ -25,6 +26,15 @@ pub enum PaddedWord { Padding(F), } +/// This trait is the interface to chips that implement a permutation. +pub trait PermuteChip: Chip + Clone + DebugT { + /// Configure the permutation chip. + fn configure(meta: &mut ConstraintSystem) -> Self::Config; + + /// Get a chip from its config. + fn construct(config: Self::Config) -> Self; +} + /// The set of circuit instructions required to use the Poseidon permutation. pub trait PoseidonInstructions, const T: usize, const RATE: usize>: Chip diff --git a/src/poseidon/pow5.rs b/src/poseidon/pow5.rs index 25ec79a..64dc8b4 100644 --- a/src/poseidon/pow5.rs +++ b/src/poseidon/pow5.rs @@ -8,9 +8,11 @@ use halo2_proofs::{ poly::Rotation, }; +use crate::Hashable; + use super::{ primitives::{Absorbing, Domain, Mds, Spec, Squeezing, State}, - PaddedWord, PoseidonInstructions, PoseidonSpongeInstructions, + PaddedWord, PermuteChip, PoseidonInstructions, PoseidonSpongeInstructions, }; /// Trait for a variable in the circuit. @@ -56,7 +58,7 @@ pub struct Pow5Config { /// /// The chip is implemented using a single round per row for full rounds, and two rounds /// per row for partial rounds. -#[derive(Debug)] +#[derive(Clone, Debug)] pub struct Pow5Chip { config: Pow5Config, } @@ -258,6 +260,26 @@ impl Chip for Pow5Chip PermuteChip for Pow5Chip { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let state = [0; 3].map(|_| meta.advice_column()); + let partial_sbox = meta.advice_column(); + let constants = [0; 6].map(|_| meta.fixed_column()); + + Pow5Chip::configure::( + meta, + state, + partial_sbox, + constants[..3].try_into().unwrap(), //rc_a + constants[3..].try_into().unwrap(), //rc_b + ) + } + + fn construct(config: Self::Config) -> Self { + Self::construct(config) + } +} + impl, const WIDTH: usize, const RATE: usize> PoseidonInstructions for Pow5Chip { @@ -455,7 +477,7 @@ impl< /// A word in the Poseidon state. #[derive(Clone, Debug)] -pub struct StateWord(AssignedCell); +pub struct StateWord(pub AssignedCell); impl From> for AssignedCell { fn from(state_word: StateWord) -> AssignedCell { diff --git a/src/poseidon/primitives.rs b/src/poseidon/primitives.rs index dee0464..bf189ef 100644 --- a/src/poseidon/primitives.rs +++ b/src/poseidon/primitives.rs @@ -24,7 +24,7 @@ pub(crate) mod pasta; //pub(crate) mod test_vectors; mod p128pow5t3; -mod p128pow5t3_compact; +pub(crate) mod p128pow5t3_compact; pub use p128pow5t3::P128Pow5T3; pub use p128pow5t3_compact::P128Pow5T3CompactSpec as P128Pow5T3Compact; diff --git a/src/poseidon/primitives/p128pow5t3_compact.rs b/src/poseidon/primitives/p128pow5t3_compact.rs index d5bd1e8..f6db10c 100644 --- a/src/poseidon/primitives/p128pow5t3_compact.rs +++ b/src/poseidon/primitives/p128pow5t3_compact.rs @@ -2,7 +2,7 @@ use std::marker::PhantomData; use halo2_proofs::arithmetic::FieldExt; -use super::p128pow5t3::P128Pow5T3Constants; +pub use super::p128pow5t3::P128Pow5T3Constants; use super::{Mds, Spec}; /// Poseidon-128 using the $x^5$ S-box, with a width of 3 field elements, and the diff --git a/src/septidon.rs b/src/septidon.rs new file mode 100644 index 0000000..ae497f6 --- /dev/null +++ b/src/septidon.rs @@ -0,0 +1,17 @@ +//! An implementation using septuple rounds. +//! See: src/README.md + +mod control; +mod full_round; +mod instruction; +mod loop_chip; +mod params; +mod septidon_chip; +mod septuple_round; +mod state; +#[cfg(test)] +mod tests; +mod transition_round; +mod util; + +pub use septidon_chip::SeptidonChip; diff --git a/src/septidon/README.md b/src/septidon/README.md new file mode 100644 index 0000000..2b62c6d --- /dev/null +++ b/src/septidon/README.md @@ -0,0 +1,150 @@ +# A Poseidon Chip with Septuple Rounds + +This is a circuit for a Poseidon permutation. It uses 8 rows per permutation. It exposes pairs of input/output at fixed +locations, to use with a sponge circuit. It is designed as a set of chips, that can be rearranged to obtain 4, 2, or +even 1 rows per permutation. It can potentially be configured with a max gate degree of 5 for faster proving. + + +**[Design Diagrams](https://miro.com/app/board/uXjVPLsk0oU=/?moveToWidget=3458764546593848776&cot=14)** + +![diagram](./Septidon.png) + + +# Spec + +## S-box + +- Config: + - 1 advice column A. + - 1 fixed column C. +- get_input() -> Expr: + Return an expression of degree 1 of the input A. +- get_output() -> Expr: + Return an expression of degree 5 of the output B. + B = (A + C)**5 + +### Partial State = SBox +### Full State = [SBox; 3] + +## Full Round + +- Config: 3 S-boxes +- get_input() -> [Expr; 3]: + Return an expression of degree 1 of the full state before the round. +- get_output() -> [Expr; 3]: + Return an expression of degree 5 of the full state after the round. + MDS . [outputs of the S-boxes] + +## Loop + +Iterate rounds on consecutive rows, with the ability to break the loop. + +- Config: + - A Round config (Full or Partial) where the iteration takes place. + - A Full State where to hold the result after break. [Expr; 3] + - A selector expression indicating when to break. Expr +- get_constraint() -> Expr + An expression that must equal zero. + +The degrees of the result and selector expressions must add up to at most 5. +The loop must break at the end of the circuit. + + +## Full Rounds Layout + +A layout of 4 Full Rounds and the output of the 4th round. The output is stored vertically in a given column, parallel to the round executions. For the first 4 full rounds, the output is the input of the first partial round. For the last 4 full rounds, the output is the final state. + +Layout: + +Selector | Rounds | Output +---------|-----------|---------- + 0 | [State 0] | (untouched) + 0 | [State 1] | output.0 + 0 | [State 2] | output.1 + 1 | [State 3] | output.2 + +- Config: + - A selector expression indicating when to output and restart. Expr. + - A Full Round Loop config for initial and intermediate states. + - A column where to hold the output state. + + +## First Partial Round + +An implementation of the first partial round, with support for a selector. + +- Config: + - A selector indicating where this specific round is enabled. + - 3 cells holding a full state as input. + - The S-Box type is not appropriate here because this works differently. + - 1 cell to hold an intermediate result a_square. + - A Full State where to hold the output. + + a = state.0 + round_constants[4] + a_square = a * a + b = a_square * a_square * a + [output] = MDS . [b, state.1, state.2] + + +## Transition Layout + +A layout of the first partial round inside of a column. + +Selector | Input | Output +---------|--------------|--------- + 0 | a_square | [output] + 0 | state.0 | (untouched) + 0 | state.1 | (untouched) + 1 | state.2 | (untouched) + + +## Septuple Round + +A batch of seven partial rounds, without selectors. + +- Config: 1 Full State, 6 Partial States. +- get_input() -> [Expr; 3]: + Return an expression of degree 1 of the full state before the rounds. +- get_output() -> [Expr; 3]: + Return an expression of degree 5 of the full state after the rounds. + + +## Septuple Rounds Layout + +A layout of 8 chained Septuple Rounds. Similar to Full Rounds Loop/Layout. +The output is the input of the next Full Rounds Layout. + + +## Control Chip + +The control chip generates signals for the selectors and switches of other chips. + +- Config: 1 fixed column +- full_rounds_break() -> the signal to interrupt the loops of full rounds. +- partial_rounds_break() -> the signal to interrupt the loops of partial rounds. +- transition_round() -> the signal to run the first partial round. + + +## Permutation Chip + +A permutation of an initial state into a final state. + +- Config: + - 2 Full States + - 6 Partial States + - 1 Column for the transition to partial rounds, and the final state. +- get_input() -> [Expr; 3]: + Return an expression of degree 1 of the initial full state. +- get_output() -> [Expr; 3]: + Return an expression of degree 1 of the final full state. + + +## Alternative: 14x-Round + +A batch of 14 partial rounds, without selectors. + +- Config: 1 Full State, 13 Partial States + +## Alternative: 14x-Rounds Layout + +A layout of 4 chained 14-Rounds. Similar to Full Rounds Loop/Layout. diff --git a/src/septidon/Septidon.png b/src/septidon/Septidon.png new file mode 100755 index 0000000..4ad3138 Binary files /dev/null and b/src/septidon/Septidon.png differ diff --git a/src/septidon/control.rs b/src/septidon/control.rs new file mode 100644 index 0000000..368afc0 --- /dev/null +++ b/src/septidon/control.rs @@ -0,0 +1,63 @@ +use super::util::query; +use crate::septidon::params::GATE_DEGREE_5; +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells}; +use halo2_proofs::poly::Rotation; + +#[derive(Clone, Debug)] +pub struct ControlChip { + is_last: Column, +} + +pub struct ControlSignals { + // Signals that control the switches between steps of the permutation. + pub break_full_rounds: Expression, + pub transition_round: Expression, + pub break_partial_rounds: Expression, + + // A selector that can disable all chips on all rows. + pub selector: Expression, +} + +impl ControlChip { + pub fn configure(cs: &mut ConstraintSystem) -> (Self, ControlSignals) { + let is_last = cs.fixed_column(); + + let signals = query(cs, |meta| { + let signal_middle = meta.query_fixed(is_last, Rotation(4)); // Seen from the middle row. + let signal_last = meta.query_fixed(is_last, Rotation::cur()); + let middle_or_last = signal_middle.clone() + signal_last.clone(); // Assume no overlap. + + ControlSignals { + break_full_rounds: middle_or_last, + transition_round: signal_middle, + break_partial_rounds: signal_last, + selector: Self::derive_selector(is_last, meta), + } + }); + + let chip = Self { is_last }; + (chip, signals) + } + + /// Assign the fixed positions of the last row of permutations. + pub fn assign(&self, region: &mut Region<'_, F>) -> Result<(), Error> { + region.assign_fixed(|| "", self.is_last, 7, || Value::known(F::one()))?; + Ok(()) + } + + fn derive_selector(is_last: Column, meta: &mut VirtualCells<'_, F>) -> Expression { + if GATE_DEGREE_5 { + // Variant with no selector. Do not disable gates, do not increase the gate degree. + Expression::Constant(F::one()) + } else { + // Variant with a selector enabled on all rows of valid permutations. + // Detect is_last=1, seen from its own row or up to 7 rows below. + (0..8_i32) + .map(|i| meta.query_fixed(is_last, Rotation(i))) + .reduce(|acc, x| acc + x) + .unwrap() // Boolean any. + } + } +} diff --git a/src/septidon/full_round.rs b/src/septidon/full_round.rs new file mode 100644 index 0000000..e26f755 --- /dev/null +++ b/src/septidon/full_round.rs @@ -0,0 +1,52 @@ +use super::loop_chip::LoopBody; +use super::params::mds; +use super::state::{Cell, FullState, SBox}; +use super::util::matmul; +use super::util::query; +use crate::septidon::util::{join_values, split_values}; +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ConstraintSystem, Error, Expression, VirtualCells}; + +#[derive(Clone, Debug)] +pub struct FullRoundChip(pub FullState); + +impl FullRoundChip { + pub fn configure(cs: &mut ConstraintSystem) -> (Self, LoopBody) { + let chip = Self(FullState::configure(cs)); + + let loop_body = query(cs, |meta| { + let next_state = chip.0.map(|sbox| sbox.input.query(meta, 1)); + let output = chip.full_round_expr(meta); + LoopBody { next_state, output } + }); + + (chip, loop_body) + } + + fn full_round_expr(&self, meta: &mut VirtualCells<'_, F>) -> [Expression; 3] { + let sbox_out = self.0.map(|sbox: &SBox| sbox.output_expr(meta)); + matmul::expr(&mds(), sbox_out) + } + + pub fn input_cells(&self) -> [Cell; 3] { + self.0.map(|sbox| sbox.input.clone()) + } + + /// Assign the witness. + pub fn assign( + &self, + region: &mut Region<'_, F>, + offset: usize, + round_constants: [F; 3], + input: [Value; 3], + ) -> Result<[Value; 3], Error> { + let mut sbox_out = [Value::unknown(); 3]; + for i in 0..3 { + let sbox: &SBox = &self.0 .0[i]; + sbox_out[i] = sbox.assign(region, offset, round_constants[i], input[i])?; + } + let output = join_values(sbox_out).map(|sbox_out| matmul::value(&mds(), sbox_out)); + Ok(split_values(output)) + } +} diff --git a/src/septidon/instruction.rs b/src/septidon/instruction.rs new file mode 100644 index 0000000..ca9e7bd --- /dev/null +++ b/src/septidon/instruction.rs @@ -0,0 +1,95 @@ +use super::{params::F, util::map_array, SeptidonChip}; +use crate::poseidon::{ + primitives::{Spec, State}, + PermuteChip, PoseidonInstructions, StateWord, Var, +}; +use halo2_proofs::{ + circuit::{Chip, Layouter}, + plonk::{ConstraintSystem, Error}, +}; + +const WIDTH: usize = 3; +const RATE: usize = 2; + +impl PermuteChip for SeptidonChip { + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let chip = Self::configure(meta); + + // Enable equality on the input/output columns, required by the function permute. + for cell in chip.initial_state_cells() { + meta.enable_equality(cell.column); + } + for cell in chip.final_state_cells() { + meta.enable_equality(cell.column); + } + + chip + } + + fn construct(config: Self::Config) -> Self { + config + } +} + +impl> PoseidonInstructions for SeptidonChip { + type Word = StateWord; + + fn permute( + &self, + layouter: &mut impl Layouter, + initial_state: &State, + ) -> Result, Error> { + layouter.assign_region( + || "permute state", + |mut region| { + let region = &mut region; + + // Copy the given initial_state into the permutation chip. + let chip_input = self.initial_state_cells(); + for i in 0..WIDTH { + initial_state[i].0.copy_advice( + || format!("load state_{}", i), + region, + chip_input[i].column, + chip_input[i].offset as usize, + )?; + } + + // Assign the internal witness of the permutation. + let initial_values = map_array(&initial_state, |word| word.value()); + let final_values = self.assign_permutation(region, initial_values)?; + + // Return the cells containing the final state. + let chip_output = self.final_state_cells(); + let final_state: Vec> = (0..WIDTH) + .map(|i| { + region + .assign_advice( + || format!("output {i}"), + chip_output[i].column, + chip_output[i].offset as usize, + || final_values[i], + ) + .map(StateWord) + }) + .collect::, _>>()?; + + Ok(final_state.try_into().unwrap()) + }, + ) + } +} + +impl Chip for SeptidonChip { + type Config = Self; + + type Loaded = (); + + fn config(&self) -> &Self::Config { + self + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} diff --git a/src/septidon/loop_chip.rs b/src/septidon/loop_chip.rs new file mode 100644 index 0000000..db977e4 --- /dev/null +++ b/src/septidon/loop_chip.rs @@ -0,0 +1,41 @@ +use super::state::Cell; +use super::util::select; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ConstraintSystem, Constraints, Expression}; + +#[derive(Clone, Debug)] +pub struct LoopChip {} + +pub struct LoopBody { + pub next_state: [Expression; 3], + /// Cells where the output is, relative to the break signal. + pub output: [Expression; 3], +} + +impl LoopChip { + pub fn configure( + cs: &mut ConstraintSystem, + q: Expression, + body: LoopBody, + break_signal: Expression, + output: [Cell; 3], + ) -> Self { + cs.create_gate("loop", |meta| { + let constraints = (0..3) + .map(|i| { + let destination = select::expr( + break_signal.clone(), + output[i].query(meta, 0), + body.next_state[i].clone(), + ); + + destination - body.output[i].clone() + }) + .collect::>(); + + Constraints::with_selector(q, constraints) + }); + + Self {} + } +} diff --git a/src/septidon/params.rs b/src/septidon/params.rs new file mode 100644 index 0000000..1293472 --- /dev/null +++ b/src/septidon/params.rs @@ -0,0 +1,49 @@ +use crate::poseidon::primitives::p128pow5t3_compact::{P128Pow5T3CompactSpec, P128Pow5T3Constants}; +use crate::poseidon::primitives::Mds as MdsT; +use crate::poseidon::primitives::Spec; +use lazy_static::lazy_static; + +/// This implementation can be limited to gate degree 5. However, this mode will not work with +/// blinding or inactive rows. Enable only with a prover that supports assignments to all n rows. +pub const GATE_DEGREE_5: bool = false; + +/// This implementation supports only the scalar field of BN254 at the moment. +/// +/// To implement for the Pasta curves, adjust the parameters below, and replace the transition round +/// by a copy, to get 56 rounds instead of 57. +pub use halo2_proofs::halo2curves::bn256::Fr as F; + +pub mod sbox { + use super::super::util::pow_5; + use super::F; + use halo2_proofs::plonk::Expression; + + pub fn expr(input: Expression, round_constant: Expression) -> Expression { + pow_5::expr(input + round_constant) + } + + pub fn value(input: F, round_constant: F) -> F { + pow_5::value(input + round_constant) + } +} + +pub type Mds = MdsT; + +lazy_static! { + static ref MDS: Mds = F::mds(); +} + +pub fn mds() -> &'static Mds { + &MDS +} + +lazy_static! { + static ref ROUND_CONSTANTS: Vec<[F; 3]> = { + let (rc, _, _) = P128Pow5T3CompactSpec::::constants(); + rc + }; +} + +pub fn round_constant(index: usize) -> [F; 3] { + ROUND_CONSTANTS[index] +} diff --git a/src/septidon/septidon_chip.rs b/src/septidon/septidon_chip.rs new file mode 100644 index 0000000..720b3bd --- /dev/null +++ b/src/septidon/septidon_chip.rs @@ -0,0 +1,166 @@ +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ConstraintSystem, Error}; + +use super::control::ControlChip; +use super::full_round::FullRoundChip; +use super::loop_chip::LoopChip; +use super::septuple_round::SeptupleRoundChip; +use super::state::Cell; +use super::transition_round::TransitionRoundChip; +use super::util::map_array; +use crate::septidon::params::round_constant; + +/// The configuration of the permutation chip. +/// +/// ``` +/// use halo2_proofs::halo2curves::bn256::Fr as F; +/// use halo2_proofs::plonk::ConstraintSystem; +/// use poseidon_circuit::septidon::SeptidonChip; +/// +/// let mut cs = ConstraintSystem::::default(); +/// let config = SeptidonChip::configure(&mut cs); +/// ``` +#[derive(Clone, Debug)] +pub struct SeptidonChip { + control_chip: ControlChip, + + transition_chip: TransitionRoundChip, + + full_round_chip: FullRoundChip, + + partial_round_chip: SeptupleRoundChip, +} + +impl SeptidonChip { + /// Create a new chip. + pub fn configure(cs: &mut ConstraintSystem) -> Self { + let (control_chip, signals) = ControlChip::configure(cs); + let q = || signals.selector.clone(); + + let (full_round_chip, full_round_loop_body) = FullRoundChip::configure(cs); + + let (partial_round_chip, partial_round_loop_body) = SeptupleRoundChip::configure(cs, q()); + + let transition_chip = { + // The output of the transition round is the input of the partial rounds loop. + let output = partial_round_chip.input(); + TransitionRoundChip::configure(cs, signals.transition_round, output) + }; + + { + // The output of full rounds go into the transition round. + let output = transition_chip.input(); + + LoopChip::configure( + cs, + q(), + full_round_loop_body, + signals.break_full_rounds, + output, + ) + }; + + { + // The output of partial rounds go horizontally into the second loop of full rounds, + // which runs parallel to the last 4 partials rounds (indexed [-3; 0]). + let full_round_sboxes = &full_round_chip.0 .0; + let output: [Cell; 3] = [ + full_round_sboxes[0].input.rotated(-3), + full_round_sboxes[1].input.rotated(-3), + full_round_sboxes[2].input.rotated(-3), + ]; + + LoopChip::configure( + cs, + q(), + partial_round_loop_body, + signals.break_partial_rounds, + output, + ) + }; + + let chip = Self { + control_chip, + transition_chip, + full_round_chip, + partial_round_chip, + }; + + chip + } + + /// How many rows are used per permutation. + pub fn height_per_permutation() -> usize { + 8 + } + + fn final_offset() -> usize { + Self::height_per_permutation() - 1 + } + + /// Return the cells containing the initial state. The parent chip must constrain these cells. + /// Cells are relative to the row 0 of a region of a permutation. + pub fn initial_state_cells(&self) -> [Cell; 3] { + self.full_round_chip.input_cells() + } + + /// Return the cells containing the final state. The parent chip must constrain these cells. + /// Cells are relative to the row 0 of a region of a permutation. + pub fn final_state_cells(&self) -> [Cell; 3] { + let relative_cells = self.transition_chip.input(); + map_array(&relative_cells, |cell| { + cell.rotated(Self::final_offset() as i32) + }) + } + + /// Assign the witness of a permutation into the given region. + pub fn assign_permutation( + &self, + region: &mut Region<'_, F>, + initial_state: [Value; 3], + ) -> Result<[Value; 3], Error> { + self.control_chip.assign(region)?; + + let mut state = initial_state; + + // First half of full rounds. + for offset in 0..4 { + state = self + .full_round_chip + .assign(region, offset, round_constant(offset), state)?; + } + + // First partial round. + // Its round constant is part of the gate (not a fixed column). + let middle_offset = 3; + state = self + .transition_chip + .assign_first_partial_state(region, middle_offset, state)?; + + // The rest of partial rounds. + for offset in 0..8 { + let round_index = 5 + offset * 7; + let round_constants = (round_index..round_index + 7) + .map(|idx| round_constant(idx)[0]) + .collect::>(); + state = self + .partial_round_chip + .assign(region, offset, &round_constants, state)?; + } + + // The second half of full rounds. + for offset in 4..8 { + state = + self.full_round_chip + .assign(region, offset, round_constant(offset + 57), state)?; + } + + // Put the final state into its place. + let final_offset = 7; + self.transition_chip + .assign_final_state(region, final_offset, state)?; + + Ok(state) + } +} diff --git a/src/septidon/septuple_round.rs b/src/septidon/septuple_round.rs new file mode 100644 index 0000000..ab80498 --- /dev/null +++ b/src/septidon/septuple_round.rs @@ -0,0 +1,124 @@ +use super::loop_chip::LoopBody; +use super::state::{Cell, SBox}; +use super::util::query; +use crate::septidon::params::mds; +use crate::septidon::util::{join_values, matmul, split_values}; +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ConstraintSystem, Constraints, Error, Expression, VirtualCells}; + +#[derive(Clone, Debug)] +pub struct SeptupleRoundChip { + first_sbox: SBox, + first_linears: [Cell; 2], + following_sboxes: [SBox; 6], +} + +impl SeptupleRoundChip { + pub fn configure(cs: &mut ConstraintSystem, q: Expression) -> (Self, LoopBody) { + let chip = Self { + first_sbox: SBox::configure(cs), + first_linears: [Cell::configure(cs), Cell::configure(cs)], + following_sboxes: (0..6) + .map(|_| SBox::configure(cs)) + .collect::>() + .try_into() + .unwrap(), + }; + + let input = chip.input(); + let (input_state, next_state) = query(cs, |meta| { + ( + [ + input[0].query(meta, 0), // Not read directly but via first_sbox.output_expr. + input[1].query(meta, 0), + input[2].query(meta, 0), + ], + [ + input[0].query(meta, 1), + input[1].query(meta, 1), + input[2].query(meta, 1), + ], + ) + }); + + let output = { + // The input state is constrained by another chip (TransitionRoundChip). + let mut checked_sbox = &chip.first_sbox; + let mut state = input_state; + + cs.create_gate("septuple_round", |meta| { + let mut constraints = vec![]; + + for sbox_to_check in &chip.following_sboxes { + // Calculate the expression of the next state. + state = Self::partial_round_expr(meta, checked_sbox, &state); + + // Compare the high-degree expression of the state with the equivalent witness. + let witness = sbox_to_check.input_expr(meta); + constraints.push(state[0].clone() - witness.clone()); + // We validated the S-Box input, so we can use next_sbox.output_expr. + checked_sbox = sbox_to_check; + } + + // Output the last round as an expression. + state = Self::partial_round_expr(meta, checked_sbox, &state); + + Constraints::with_selector(q, constraints) + }); + state + }; + + let loop_body = LoopBody { next_state, output }; + + (chip, loop_body) + } + + fn partial_round_expr( + meta: &mut VirtualCells<'_, F>, + sbox: &SBox, + input: &[Expression; 3], + ) -> [Expression; 3] { + let sbox_out = [sbox.output_expr(meta), input[1].clone(), input[2].clone()]; + matmul::expr(&mds(), sbox_out) + } + + pub fn input(&self) -> [Cell; 3] { + [ + self.first_sbox.input.clone(), + self.first_linears[0].clone(), + self.first_linears[1].clone(), + ] + } + + /// Assign the witness. + pub fn assign( + &self, + region: &mut Region<'_, F>, + offset: usize, + round_constants: &[F], + input: [Value; 3], + ) -> Result<[Value; 3], Error> { + // Assign the first non-S-Box cells. + for i in 0..2 { + self.first_linears[i].assign(region, offset, input[1 + i])?; + } + + let mut state = input; + let mut assign_partial_round = |i: usize, sbox: &SBox| -> Result<(), Error> { + // Assign the following S-Boxes. + state[0] = sbox.assign(region, offset, round_constants[i], state[0])?; + // Apply the matrix. + state = split_values(join_values(state).map(|s| matmul::value(&mds(), s))); + Ok(()) + }; + + assign_partial_round(0, &self.first_sbox)?; + + for (i, sbox) in self.following_sboxes.iter().enumerate() { + assign_partial_round(1 + i, sbox)?; + } + + Ok(state) + } +} diff --git a/src/septidon/state.rs b/src/septidon/state.rs new file mode 100644 index 0000000..72f11a4 --- /dev/null +++ b/src/septidon/state.rs @@ -0,0 +1,133 @@ +use crate::septidon::params; +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ + Advice, Column, ConstraintSystem, Error, Expression, Fixed, VirtualCells, +}; +use halo2_proofs::poly::Rotation; + +/// Cell remembers the relative position of a cell in the region of a permutation. +/// It can be used in configuration and synthesis. +#[derive(Clone, Debug)] +pub struct Cell { + pub column: Column, + /// An offset relative to the owner of this Cell. + pub offset: i32, +} + +impl Cell { + pub fn configure(cs: &mut ConstraintSystem) -> Self { + Cell { + column: cs.advice_column(), + offset: 0, + } + } + + pub fn new(column: Column, offset: i32) -> Self { + Self { column, offset } + } + + pub fn rotated(&self, offset: i32) -> Self { + Self { + column: self.column, + offset: self.offset + offset, + } + } + + pub fn query(&self, meta: &mut VirtualCells, offset: i32) -> Expression { + meta.query_advice(self.column, Rotation(self.offset + offset)) + } + + pub fn region_offset(&self) -> usize { + assert!(self.offset >= 0); + self.offset as usize + } + + pub fn assign( + &self, + region: &mut Region<'_, F>, + origin_offset: usize, + input: Value, + ) -> Result<(), Error> { + let offset = origin_offset as i32 + self.offset; + assert!(offset >= 0, "cannot assign to a cell outside of its region"); + region.assign_advice(|| "cell", self.column, offset as usize, || input)?; + Ok(()) + } +} + +#[derive(Clone, Debug)] +pub struct SBox { + pub input: Cell, + round_constant: Column, +} + +impl SBox { + pub fn configure(cs: &mut ConstraintSystem) -> Self { + SBox { + input: Cell::configure(cs), + round_constant: cs.fixed_column(), + } + } + + /// Assign the witness of the input. + pub fn assign( + &self, + region: &mut Region<'_, F>, + offset: usize, + round_constant: F, + input: Value, + ) -> Result, Error> { + region.assign_fixed( + || "round_constant", + self.round_constant, + offset + self.input.region_offset(), + || Value::known(round_constant), + )?; + region.assign_advice( + || "initial_state", + self.input.column, + offset + self.input.region_offset(), + || input, + )?; + let output = input.map(|i| params::sbox::value(i, round_constant)); + Ok(output) + } + + pub fn input_expr(&self, meta: &mut VirtualCells<'_, F>) -> Expression { + self.input.query(meta, 0) + } + + pub fn rc_expr(&self, meta: &mut VirtualCells<'_, F>) -> Expression { + meta.query_fixed(self.round_constant, Rotation(self.input.offset)) + } + + pub fn output_expr(&self, meta: &mut VirtualCells<'_, F>) -> Expression { + let input = self.input_expr(meta); + let round_constant = self.rc_expr(meta); + params::sbox::expr(input, round_constant) + } +} + +#[derive(Clone, Debug)] +pub struct FullState(pub [SBox; 3]); + +impl FullState { + pub fn configure(cs: &mut ConstraintSystem) -> Self { + Self([ + SBox::configure(cs), + SBox::configure(cs), + SBox::configure(cs), + ]) + } + + pub fn map(&self, mut f: F) -> [T; 3] + where + F: FnMut(&SBox) -> T, + { + let a = f(&self.0[0]); + let b = f(&self.0[1]); + let c = f(&self.0[2]); + [a, b, c] + } +} diff --git a/src/septidon/tests.rs b/src/septidon/tests.rs new file mode 100644 index 0000000..e0af700 --- /dev/null +++ b/src/septidon/tests.rs @@ -0,0 +1,66 @@ +use halo2_proofs::circuit::{Layouter, Region, SimpleFloorPlanner, Value}; +use halo2_proofs::dev::MockProver; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{Circuit, ConstraintSystem, Error}; + +use super::SeptidonChip; +use crate::septidon::util::join_values; + +#[test] +fn septidon_permutation() { + let k = 5; + let inactive_rows = 6; // Assume default in this test. + + let circuit = TestCircuit { + height: (1 << k) - inactive_rows, + }; + let prover = MockProver::run(k as u32, &circuit, vec![]).unwrap(); + prover.verify_at_rows(0..1, 0..0).unwrap(); +} + +#[derive(Clone)] +struct TestCircuit { + height: usize, +} + +impl Circuit for TestCircuit { + type Config = SeptidonChip; + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + self.clone() + } + + fn configure(cs: &mut ConstraintSystem) -> Self::Config { + SeptidonChip::configure(cs) + } + + fn synthesize( + &self, + config: SeptidonChip, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + let num_permutations = self.height / 8; + + for _ in 0..num_permutations { + let initial_state = [ + Value::known(F::from(0)), + Value::known(F::from(1)), + Value::known(F::from(2)), + ]; + + let final_state = layouter.assign_region( + || "SeptidonChip", + |mut region: Region<'_, F>| config.assign_permutation(&mut region, initial_state), + )?; + + let got = format!("{:?}", join_values(final_state).inner.unwrap()); + + // For input 0,1,2. + let expect = "[0x115cc0f5e7d690413df64c6b9662e9cf2a3617f2743245519e19607a4417189a, 0x0fca49b798923ab0239de1c9e7a4a9a2210312b6a2f616d18b5a87f9b628ae29, 0x0e7ae82e40091e63cbd4f16a6d16310b3729d4b6e138fcf54110e2867045a30c]"; + assert_eq!(got, expect); + } + + Ok(()) + } +} diff --git a/src/septidon/transition_round.rs b/src/septidon/transition_round.rs new file mode 100644 index 0000000..7d6c1f5 --- /dev/null +++ b/src/septidon/transition_round.rs @@ -0,0 +1,125 @@ +use super::state::Cell; +use crate::septidon::params; +use crate::septidon::params::{mds, round_constant}; +use crate::septidon::util::{join_values, matmul, split_values}; +use halo2_proofs::circuit::{Region, Value}; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Expression}; + +#[derive(Clone, Debug)] +pub struct TransitionRoundChip { + column: Column, +} + +impl TransitionRoundChip { + pub fn configure( + cs: &mut ConstraintSystem, + signal: Expression, + next_state: [Cell; 3], + ) -> Self { + let chip = Self { + column: cs.advice_column(), + }; + + cs.create_gate("transition round", |meta| { + // The input cells are relative to the signal. + let input = chip.input(); + let input = [ + input[0].query(meta, 0), + input[1].query(meta, 0), + input[2].query(meta, 0), + ]; + + let output = Self::first_partial_round_expr(&input); + + // Get the next_state from the point of view of the signal. + let next_state = [ + next_state[0].query(meta, -3), + next_state[1].query(meta, -3), + next_state[2].query(meta, -3), + ]; + + let constraints = vec![ + output[0].clone() - next_state[0].clone(), + output[1].clone() - next_state[1].clone(), + output[2].clone() - next_state[2].clone(), + ]; + + Constraints::with_selector(signal, constraints) + }); + + chip + } + + // Return an expression of the state after the first partial round given the state before. + // TODO: implement with with degree <= 5 using the helper cell. + fn first_partial_round_expr(input: &[Expression; 3]) -> [Expression; 3] { + let rc = Expression::Constant(Self::round_constant()); + let sbox_out = [ + params::sbox::expr(input[0].clone(), rc), + input[1].clone(), + input[2].clone(), + ]; + matmul::expr(&mds(), sbox_out) + } + + fn round_constant() -> F { + round_constant(4)[0] + } + + /// Return the input cells of this round, relative to the signal. + // TODO: rename because it is also used as final state. + pub fn input(&self) -> [Cell; 3] { + // The input to the transition round is vertical in the transition column. + [ + Cell::new(self.column, -2), + Cell::new(self.column, -1), + Cell::new(self.column, 0), + ] + } + + pub fn helper_cell(&self) -> Cell { + Cell::new(self.column, -3) + } + + /// Assign the state of the first partial round, and return the round output. + pub fn assign_first_partial_state( + &self, + region: &mut Region<'_, F>, + middle_break_offset: usize, + input: [Value; 3], + ) -> Result<[Value; 3], Error> { + let output = Self::first_partial_round(&input); + for (value, cell) in input.into_iter().zip(self.input()) { + cell.assign(region, middle_break_offset, value)?; + } + self.helper_cell() + .assign(region, middle_break_offset, Value::known(F::zero()))?; + Ok(output) + } + + fn first_partial_round(input: &[Value; 3]) -> [Value; 3] { + let sbox_out = [ + input[0].map(|f| params::sbox::value(f, Self::round_constant())), + input[1], + input[2], + ]; + let output = join_values(sbox_out).map(|s| matmul::value(&mds(), s)); + split_values(output) + } + + /// Assign the final state. This has the same layout as the first partial state, at another offset. + pub fn assign_final_state( + &self, + region: &mut Region<'_, F>, + final_break_offset: usize, + input: [Value; 3], + ) -> Result<(), Error> { + for (value, cell) in input.into_iter().zip(self.input()) { + cell.assign(region, final_break_offset, value)?; + } + self.helper_cell() + .assign(region, final_break_offset, Value::known(F::zero()))?; + Ok(()) + } +} diff --git a/src/septidon/util.rs b/src/septidon/util.rs new file mode 100644 index 0000000..847e0ab --- /dev/null +++ b/src/septidon/util.rs @@ -0,0 +1,130 @@ +use halo2_proofs::circuit::Value; +use halo2_proofs::halo2curves::bn256::Fr as F; +use halo2_proofs::plonk::{ConstraintSystem, Expression, VirtualCells}; + +pub fn map_array(array: &[IN; 3], mut f: FN) -> [OUT; 3] +where + FN: FnMut(&IN) -> OUT, +{ + let a = f(&array[0]); + let b = f(&array[1]); + let c = f(&array[2]); + [a, b, c] +} + +/// Helper to make queries to a ConstraintSystem. Escape the "create_gate" closures. +pub fn query(cs: &mut ConstraintSystem, f: impl FnOnce(&mut VirtualCells<'_, F>) -> T) -> T { + let mut queries: Option = None; + cs.create_gate("query", |meta| { + queries = Some(f(meta)); + [Expression::Constant(F::zero())] + }); + queries.unwrap() +} + +pub fn join_values(values: [Value; 3]) -> Value<[F; 3]> { + values[0] + .zip(values[1]) + .zip(values[2]) + .map(|((v0, v1), v2)| [v0, v1, v2]) +} + +pub fn split_values(values: Value<[F; 3]>) -> [Value; 3] { + [ + values.map(|v| v[0]), + values.map(|v| v[1]), + values.map(|v| v[2]), + ] +} + +pub mod pow_5 { + use super::super::params::F; + use halo2_proofs::plonk::Expression; + + pub fn expr(v: Expression) -> Expression { + let v2 = v.clone() * v.clone(); + v2.clone() * v2 * v + } + + pub fn value(v: F) -> F { + let v2 = v * v; + v2 * v2 * v + } +} + +/// Matrix multiplication expressions and values. +pub mod matmul { + use super::super::params::{Mds, F}; + use halo2_proofs::plonk::Expression; + use std::convert::TryInto; + + /// Multiply a vector of expressions by a constant matrix. + pub fn expr(matrix: &Mds, vector: [Expression; 3]) -> [Expression; 3] { + (0..3) + .map(|next_idx| { + (0..3) + .map(|idx| vector[idx].clone() * matrix[next_idx][idx]) + .reduce(|acc, term| acc + term) + .unwrap() + }) + .collect::>() + .try_into() + .unwrap() + } + + /// Multiply a vector of values by a constant matrix. + pub fn value(matrix: &Mds, vector: [F; 3]) -> [F; 3] { + (0..3) + .map(|next_idx| { + (0..3) + .map(|idx| vector[idx] * matrix[next_idx][idx]) + .reduce(|acc, term| acc + term) + .unwrap() + }) + .collect::>() + .try_into() + .unwrap() + } +} + +/// Returns `when_true` when `selector == 1`, and returns `when_false` when +/// `selector == 0`. `selector` needs to be boolean. +pub mod select { + use halo2_proofs::{arithmetic::FieldExt, plonk::Expression}; + + /// Returns the `when_true` expression when the selector is true, else + /// returns the `when_false` expression. + pub fn expr( + selector: Expression, + when_true: Expression, + when_false: Expression, + ) -> Expression { + let one = Expression::Constant(F::from(1)); + selector.clone() * when_true + (one - selector) * when_false + } + + /// Returns the `when_true` value when the selector is true, else returns + /// the `when_false` value. + pub fn value(selector: F, when_true: F, when_false: F) -> F { + selector * when_true + (F::one() - selector) * when_false + } +} + +/// Gadget for boolean OR. +pub mod or { + use halo2_proofs::{arithmetic::FieldExt, plonk::Expression}; + + /// Return (a OR b), assuming a and b are boolean expressions. + pub fn expr(a: Expression, b: Expression) -> Expression { + let one = Expression::Constant(F::from(1)); + // a OR b <=> !(!a AND !b) + one.clone() - ((one.clone() - a) * (one.clone() - b)) + } + + /// Return (a OR b), assuming a and b are boolean values. + pub fn value(a: F, b: F) -> F { + let one = F::one(); + // a OR b <=> !(!a AND !b) + one - ((one - a) * (one - b)) + } +} diff --git a/tests/hash_proving.rs b/tests/hash_proving.rs index fad83b6..8c1cd24 100644 --- a/tests/hash_proving.rs +++ b/tests/hash_proving.rs @@ -17,6 +17,7 @@ use halo2_proofs::{ circuit::{Layouter, SimpleFloorPlanner}, plonk::{Circuit, ConstraintSystem, Error}, }; +use poseidon_circuit::poseidon::Pow5Chip; use poseidon_circuit::{hash::*, DEFAULT_STEP}; use rand::SeedableRng; use rand_chacha::ChaCha8Rng; @@ -25,7 +26,7 @@ struct TestCircuit(PoseidonHashTable, usize); // test circuit derived from table data impl Circuit for TestCircuit { - type Config = PoseidonHashConfig; + type Config = PoseidonHashConfig>; type FloorPlanner = SimpleFloorPlanner; fn without_witnesses(&self) -> Self { @@ -42,7 +43,7 @@ impl Circuit for TestCircuit { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - let chip = PoseidonHashChip::::construct( + let chip = PoseidonHashChip::>::construct( config, &self.0, self.1,