diff --git a/Cargo.toml b/Cargo.toml index 2e16b7b..df6c725 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,7 +9,7 @@ edition = "2021" halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", tag = "v2022_09_10" } lazy_static = "1.4.0" thiserror = "1.0" -bitvec = "0.22" +bitvec = "1" [patch."https://github.com/privacy-scaling-explorations/halo2.git"] halo2_proofs = { git = "https://github.com/scroll-tech/halo2.git", branch = "halo2-ecc-snark-verifier-0220" } @@ -24,10 +24,6 @@ poseidon = { git = "https://github.com/scroll-tech/poseidon.git", branch = "halo [patch."https://github.com/privacy-scaling-explorations/halo2curves.git"] halo2curves = { git = "https://github.com/scroll-tech/halo2curves.git", branch = "halo2-ecc-snark-verifier-0220" } -[patch.crates-io] -# temporary solution to funty@1.2.0 being yanked, tracking issue: https://github.com/ferrilab/funty/issues/7 -funty = { git = "https://github.com/ferrilab/funty/", rev = "7ef0d890fbcd8b3def1635ac1a877fc298488446" } - [features] # printout the layout of circuits for demo and some unittests # print_layout = ["halo2_proofs/dev-graph"] diff --git a/rust-toolchain b/rust-toolchain index 07ade69..60d6790 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1 +1 @@ -nightly \ No newline at end of file +nightly-2022-12-10 \ No newline at end of file diff --git a/spec/hash-table.md b/spec/hash-table.md index c9d6588..91d9e56 100644 --- a/spec/hash-table.md +++ b/spec/hash-table.md @@ -14,17 +14,17 @@ ## Interface Table -The hash circuit exposes a table containing multiple inputs/output pairs. This table can be looked up by the MPT and codehash circuits. The table has four columns: 2 inputs, 1 digest output, and 1 for control flags. +The hash circuit exposes a table containing multiple inputs/output pairs. This table can be looked up by the MPT and codehash circuits. The table has four columns: 2 inputs, 1 digest output, 2 for control flags and additional marking. -| 0: Hash index | 1: Message | 2: Message | 3: Control flag | -| --------------- | ---------------- | --------------- | --------------- | -| MPT digest | MPT input 1 | MPT input 2 | 0 | -| | | | | -| var-len digest | word 0 | word 1 | 2000 | -| var-len digest | word 2 | word 3 | 1968 | -| ... | ... | ... | ... | -| var-len digest | word W-2 | word W-1 | 16 | -| | | | | +| 0: Hash index | 1: Message | 2: Message | 3: Control flag | 4: Head flag | +| --------------- | ---------------- | --------------- | --------------- | ------------ | +| MPT digest | MPT input 1 | MPT input 2 | 0 | 1 | +| | | | | | +| var-len digest | word 0 | word 1 | 2000 | 1 | +| var-len digest | word 2 | word 3 | 1968 | 0 | +| ... | ... | ... | ... | 0 | +| var-len digest | word W-2 | word W-1 | 16 | 0 | +| | | | | | The hash circuit supports two modes: @@ -49,6 +49,17 @@ Compute the digest of a variable-length message. One such entry is composed of c Specifically, `STEP = 32`. +### Head flag + +The head flag is set at each beginning of message, i.e each row under MPT mode and the first row of message in Var-Len mode would be set to 1 + +### Custom row + +2 Additional row is put at the beginning of hash table: + +1. A row being filled with 0 for any lookup which is not enabled +2. A row with `control` and `Message` field being set to 0 and the hash is set to a customed value for representing +the hash of empty message. Currently it is set to equal to `keccak256(nil)` and the indexed hash value must be properly set under challenge API ## Internal Table (hash_table_aux) diff --git a/src/hash.rs b/src/hash.rs index aa03cb3..d0c1c94 100644 --- a/src/hash.rs +++ b/src/hash.rs @@ -3,6 +3,7 @@ use crate::poseidon::primitives::{ ConstantLengthIden3, Domain, Hash, P128Pow5T3, Spec, VariableLengthIden3, }; +use halo2_proofs::circuit::AssignedCell; use halo2_proofs::ff::{FromUniformBytes, PrimeField}; use halo2_proofs::halo2curves::bn256::Fr; @@ -56,53 +57,59 @@ impl MessageHashable for Fr { } } -use crate::poseidon::{PoseidonInstructions, Pow5Chip, Pow5Config, StateWord, Var}; +use crate::poseidon::{PermuteChip, PoseidonInstructions}; use halo2_proofs::{ - circuit::{Chip, Layouter, Value}, + circuit::{Chip, Layouter, Region, Value}, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, TableColumn}, poly::Rotation, }; /// The config for poseidon hash circuit #[derive(Clone, Debug)] -pub struct PoseidonHashConfig { - permute_config: Pow5Config, - hash_table: [Column; 4], +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; 4] { + pub fn commitment_index(&self) -> [usize; 5] { self.hash_table.map(|col| col.index()) } /// obtain the hash_table columns - pub fn hash_tbl_cols(&self) -> [Column; 4] { + pub fn hash_tbl_cols(&self) -> [Column; 5] { self.hash_table } /// build configure for sub circuit pub fn configure_sub( meta: &mut ConstraintSystem, - hash_table: [Column; 4], + 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()); - let s_table = meta.complex_selector(); - - let hash_table_aux = [0; 6].map(|_| meta.advice_column()); + // TODO: remove this "constants". + let constants = [0; 1].map(|_| meta.fixed_column()); + let s_table = meta.selector(); + let s_custom = meta.selector(); + + let hash_table_aux = [0, 1, 2, 3, 4, 5].map(|idx| { + if idx < 5 { + meta.advice_column() + } else { + meta.advice_column_in(halo2_proofs::plonk::SecondPhase) + } + }); for col in hash_table_aux.iter().chain(hash_table[0..1].iter()) { meta.enable_equality(*col); } - meta.enable_equality(constants[0]); let control = hash_table[3]; let s_sponge_continue = meta.advice_column(); @@ -115,41 +122,66 @@ impl PoseidonHashConfig { let hash_out = hash_table_aux[5]; let hash_inp = &hash_table[1..3]; let hash_index = hash_table[0]; + let header_mark = hash_table[4]; + + meta.create_gate("custom row", |meta| { + let s_enable = meta.query_selector(s_custom); + + vec![ + s_enable.clone() * meta.query_advice(hash_inp[0], Rotation::cur()), + s_enable.clone() * meta.query_advice(hash_inp[1], Rotation::cur()), + s_enable * meta.query_advice(control, Rotation::cur()), + ] + }); meta.create_gate("control constrain", |meta| { + /* + s_continue must be bool + s_continue must be false on each row which control is 0 (MPT mode) + header_mark is just not(s_continue) + */ let s_enable = meta.query_selector(s_table); let ctrl = meta.query_advice(control, Rotation::cur()); let ctrl_bool = ctrl.clone() * meta.query_advice(control_aux, Rotation::cur()); let s_continue = meta.query_advice(s_sponge_continue, Rotation::cur()); vec![ + s_enable.clone() + * s_continue.clone() + * (Expression::Constant(Fp::ONE) - s_continue.clone()), s_enable.clone() * ctrl * (Expression::Constant(Fp::ONE) - ctrl_bool.clone()), - s_enable * s_continue * (Expression::Constant(Fp::ONE) - ctrl_bool), + s_enable.clone() * s_continue.clone() * (Expression::Constant(Fp::ONE) - ctrl_bool), + s_enable + * (Expression::Constant(Fp::ONE) + - s_continue + - meta.query_advice(header_mark, Rotation::cur())), ] }); meta.create_gate("control step", |meta| { - let s_enable = meta.query_selector(s_table); + /* + when s_continue is true, it trigger a RANGE checking on the ctrl_prev + to less than or equal to **step** + and current ctrl can not be 0 + */ let s_continue = meta.query_advice(s_sponge_continue, Rotation::cur()); + let s_enable = meta.query_selector(s_table) * s_continue; let ctrl = meta.query_advice(control, Rotation::cur()); let ctrl_prev = meta.query_advice(control, Rotation::prev()); + let ctrl_bool = ctrl.clone() * meta.query_advice(control_aux, Rotation::cur()); vec![ - s_enable - * s_continue + s_enable.clone() * (ctrl + Expression::Constant(Fp::from_u128(step as u128)) - ctrl_prev), + s_enable * (Expression::Constant(Fp::ONE) - ctrl_bool), ] }); meta.lookup("control range check", |meta| { - let s_enable = meta.query_selector(s_table); - let s_continue = meta.query_advice(s_sponge_continue, Rotation::cur()); + let s_enable = meta.query_advice(header_mark, Rotation::cur()); let ctrl = meta.query_advice(control, Rotation::prev()); - vec![( - s_enable * (Expression::Constant(Fp::ONE) - s_continue) * ctrl, - control_step_range, - )] + vec![(s_enable * ctrl, control_step_range)] }); meta.create_gate("hash index constrain", |meta| { @@ -202,19 +234,14 @@ 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, constants, control_step_range, s_table, + s_custom, s_sponge_continue, } } @@ -229,6 +256,8 @@ pub struct PoseidonHashTable { pub controls: Vec, /// the expected hash output for checking pub checks: Vec>, + /// the custom hash for nil message + pub nil_msg_hash: Option, } impl PoseidonHashTable { @@ -249,6 +278,7 @@ impl PoseidonHashTable { for (a, b, c) in src { self.inputs.push([*a, *b]); self.checks.push(Some(*c)); + self.controls.push(Fp::ZERO); } } @@ -274,286 +304,315 @@ impl PoseidonHashTable { assert_eq!(new_inps.len(), ctrl_series.len()); self.inputs.append(&mut new_inps); self.controls.append(&mut ctrl_series); + assert_eq!(self.inputs.len(), self.controls.len()); + } + + /// return the row which poseidon table use (notice it maybe much smaller + /// than the actual circuit row required) + pub fn table_size(&self) -> usize { + self.inputs.len() + } +} + +impl PoseidonHashTable { + /// return minimum required the circuit rows\ + /// (size of hashes * rows required by each hash) + pub fn minimum_row_require(&self) -> usize { + self.inputs.len() * Fp::hash_block_size() } } /// Represent the chip for Poseidon hash table #[derive(Debug)] -pub struct PoseidonHashChip<'d, Fp: PrimeField, const STEP: usize> { +pub struct PoseidonHashChip<'d, Fp: PrimeField, const STEP: usize, PC: PermuteChip> { calcs: usize, + nil_msg_hash: Option, + mpt_only: bool, data: &'d PoseidonHashTable, - config: PoseidonHashConfig, + config: PoseidonHashConfig, } -impl<'d, Fp: Hashable, const STEP: usize> PoseidonHashChip<'d, Fp, STEP> { +type PermutedState = Vec<[Word; 3]>; + +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, + nil_msg_hash: Option, ) -> Self { Self { calcs, + mpt_only, + nil_msg_hash, data, config, } } - /// load the table into circuit under the specified config - pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { + fn fill_hash_tbl_custom(&self, region: &mut Region<'_, Fp>) -> Result { let config = &self.config; - let constants_cell = layouter.assign_region( - || "constant heading", - |mut region| { - let c0 = region.assign_fixed( - || "constant zero", - config.constants[0], - 0, - || Value::known(Fp::ZERO), - )?; - - Ok([c0]) - }, - )?; - - layouter.assign_table( - || "STEP range check", - |mut table| { - (0..STEP + 1).into_iter().try_for_each(|i| { - table - .assign_cell( - || "STEP range check", - config.control_step_range, - i, - || Value::known(Fp::from_u128(i as u128)), - ) - .map(|_| ()) - }) - }, - )?; - let data = self.data; - let (states_in, states_out) = layouter.assign_region( - || "hash table", - |mut region| { - let mut states_in = Vec::new(); - let mut states_out = Vec::new(); - let hash_helper = Fp::hasher(); - - let dummy_input: [Option<&[Fp; 2]>; 1] = [None]; - let dummy_item: [Option<&Fp>; 1] = [None]; - let inputs_i = data - .inputs - .iter() - .map(Some) - .chain(dummy_input.into_iter().cycle()) - .take(self.calcs); - let controls_i = data - .controls - .iter() - .map(Some) - .chain(dummy_item.into_iter().cycle()) - .take(self.calcs); - - let checks_i = data - .checks - .iter() - .map(|i| i.as_ref()) - .chain(dummy_item.into_iter().cycle()) - .take(self.calcs); - - // notice our hash table has a (0, 0, 0) at the beginning - for col in config.hash_table { - region.assign_advice(|| "dummy inputs", col, 0, || Value::known(Fp::ZERO))?; - } + config.s_custom.enable(region, 0)?; + // all zero row + for (tip, cols) in [ + ("dummy inputs", config.hash_table.as_slice()), + ("dummy aux inputs", config.hash_table_aux.as_slice()), + ("control aux head", [config.control_aux].as_slice()), + ( + "control sponge continue head", + [config.s_sponge_continue].as_slice(), + ), + ] { + for col in cols { + region.assign_advice(|| tip, *col, 0, || Value::known(Fp::ZERO))?; + } + } - for col in config.hash_table_aux { - region.assign_advice( - || "dummy aux inputs", - col, - 0, - || Value::known(Fp::ZERO), - )?; - } + config.s_custom.enable(region, 1)?; + if self.mpt_only { + return Ok(1); + } - region.assign_advice( - || "control aux head", - config.control_aux, - 0, - || Value::known(Fp::ZERO), - )?; + // custom + for (tip, cols) in [ + ("custom inputs", &config.hash_table[1..4]), + ("custom aux inputs", config.hash_table_aux.as_slice()), + ("control aux head custom", [config.control_aux].as_slice()), + ( + "control sponge continue head custom", + [config.s_sponge_continue].as_slice(), + ), + ] { + for col in cols { + region.assign_advice(|| tip, *col, 1, || Value::known(Fp::ZERO))?; + } + } - let c_ctrl = region.assign_advice( - || "control sponge continue head", - config.s_sponge_continue, - 0, - || Value::known(Fp::ZERO), - )?; + // input, notice hash index constrain require we also assign hash_out col + for col in [config.hash_table_aux[5], config.hash_table[0]] { + region.assign_advice( + || "custom hash for nil", + col, + 1, + || { + self.nil_msg_hash + .map(Value::known) + .unwrap_or_else(Value::unknown) + }, + )?; + } + region.assign_advice( + || "custom mark", + config.hash_table[4], + 1, + || Value::known(Fp::ONE), + )?; - // contraint 0 to zero constant - region.constrain_equal(c_ctrl.cell(), constants_cell[0].cell())?; + Ok(2) + } - let mut is_new_sponge = true; - let mut process_start = 0; - let mut offset = 1; - let mut state: [Fp; 3] = [Fp::ZERO; 3]; + fn fill_hash_tbl_body( + &self, + region: &mut Region<'_, Fp>, + begin_offset: usize, + ) -> Result<(PermutedState, PermutedState), Error> { + let config = &self.config; + let data = self.data; - for (i, ((inp, control), check)) in - inputs_i.zip(controls_i).zip(checks_i).enumerate() - { - let control = control.copied().unwrap_or(Fp::ZERO); - offset = i + 1; + let mut states_in = Vec::new(); + let mut states_out = Vec::new(); + let hash_helper = Fp::hasher(); + + let inputs_i = data + .inputs + .iter() + .map(Some) + .chain(std::iter::repeat(None)) + .take(self.calcs); + let controls_i = data + .controls + .iter() + .map(Some) + .chain(std::iter::repeat(None)) + .take(self.calcs); + + let checks_i = data + .checks + .iter() + .map(|i| i.as_ref()) + .chain(std::iter::repeat(None)) + .take(self.calcs); + + let mut is_new_sponge = true; + let mut process_start = 0; + let mut state: [Fp; 3] = [Fp::ZERO; 3]; + let mut last_offset = 0; + + for (i, ((inp, control), check)) in inputs_i.zip(controls_i).zip(checks_i).enumerate() { + let control = control.copied().unwrap_or(Fp::ZERO); + let offset = i + begin_offset; + last_offset = offset; + + if is_new_sponge { + state[0] = control; + process_start = offset; + } - if is_new_sponge { - state[0] = control; - process_start = offset; - } + let inp = inp + .map(|[a, b]| [*a, *b]) + .unwrap_or_else(|| [Fp::ZERO, Fp::ZERO]); - let inp = inp - .map(|[a, b]| [*a, *b]) - .unwrap_or_else(|| [Fp::ZERO, Fp::ZERO]); + state.iter_mut().skip(1).zip(inp).for_each(|(s, inp)| { + if is_new_sponge { + *s = inp; + } else { + *s += inp; + } + }); - state.iter_mut().skip(1).zip(inp).for_each(|(s, inp)| { - if is_new_sponge { - *s = inp; - } else { - *s += inp; - } - }); + let state_start = state; + hash_helper.permute(&mut state); //here we calculate the hash - let state_start = state; - hash_helper.permute(&mut state); //here we calculate the hash + //and sanity check ... + if let Some(ck) = check { + assert_eq!( + *ck, state[0], + "hash output not match with expected at {offset}" + ); + } - //and sanity check ... - if let Some(ck) = check { - assert_eq!(*ck, state[0]); - } + let current_hash = state[0]; - config.s_table.enable(&mut region, offset)?; - - let c_start = [ - region.assign_advice( - || format!("state input 0_{}", i), - config.hash_table_aux[0], - offset, - || Value::known(state_start[0]), - )?, - region.assign_advice( - || format!("state input 1_{}", i), - config.hash_table_aux[1], - offset, - || Value::known(state_start[1]), - )?, - region.assign_advice( - || format!("state input 2_{}", i), - config.hash_table_aux[2], - offset, - || Value::known(state_start[2]), - )?, - ]; - - let current_hash = state[0]; - let c_end = [ - region.assign_advice( - || format!("state output hash_{}", i), - config.hash_table_aux[5], - offset, - || Value::known(state[0]), - )?, - region.assign_advice( - || format!("state output 1_{}", i), - config.hash_table_aux[3], - offset, - || Value::known(state[1]), - )?, - region.assign_advice( - || format!("state output 2_{}", i), - config.hash_table_aux[4], - offset, - || Value::known(state[2]), - )?, - ]; + //assignment ... + config.s_table.enable(region, offset)?; + let c_start = [0; 3] + .into_iter() + .enumerate() + .map(|(i, _)| { region.assign_advice( - || format!("state input control_{}", i), - config.hash_table[3], + || format!("state input {i}_{offset}"), + config.hash_table_aux[i], offset, - || Value::known(control), - )?; + || Value::known(state_start[i]), + ) + }) + .collect::, _>>()?; + let c_end = [5, 3, 4] + .into_iter() + .enumerate() + .map(|(i, j)| { region.assign_advice( - || format!("state input control_aux_{}", i), - config.control_aux, + || format!("state output {i}_{offset}"), + config.hash_table_aux[j], offset, - || Value::known(control.invert().unwrap_or(Fp::ZERO)), - )?; + || Value::known(state[i]), + ) + }) + .collect::, _>>()?; + + for (tip, col, val) in [ + ("hash input first", config.hash_table[1], inp[0]), + ("hash input second", config.hash_table[2], inp[1]), + ("state input control", config.hash_table[3], control), + ( + "state beginning flag", + config.hash_table[4], + if is_new_sponge { Fp::ONE } else { Fp::ZERO }, + ), + ( + "state input control_aux", + config.control_aux, + control.invert().unwrap_or(Fp::ZERO), + ), + ( + "state continue control", + config.s_sponge_continue, + if is_new_sponge { Fp::ZERO } else { Fp::ONE }, + ), + ] { + region.assign_advice( + || format!("{tip}_{offset}"), + col, + offset, + || Value::known(val), + )?; + } - region.assign_advice( - || format!("state continue control_{}", i), - config.s_sponge_continue, - offset, - || Value::known(if is_new_sponge { Fp::ZERO } else { Fp::ONE }), - )?; + is_new_sponge = control <= Fp::from_u128(STEP as u128); + + //fill all the hash_table[0] with result hash + if is_new_sponge { + (process_start..=offset).try_for_each(|ith| { + region + .assign_advice( + || format!("hash index_{ith}"), + config.hash_table[0], + ith, + || Value::known(current_hash), + ) + .map(|_| ()) + })?; + } - region.assign_advice( - || format!("hash input first_{}", i), - config.hash_table[1], - offset, - || Value::known(inp[0]), - )?; + //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(PC::Word::from)); + let c_end_arr: [_; 3] = c_end.try_into().expect("same size"); + states_out.push(c_end_arr.map(PC::Word::from)); + } - region.assign_advice( - || format!("hash input second_{}", i), - config.hash_table[2], - offset, - || Value::known(inp[1]), - )?; - - is_new_sponge = control <= Fp::from_u128(STEP as u128); - - //fill all the hash_table[0] with result hash - if is_new_sponge { - (process_start..offset + 1).try_for_each(|ith| { - region - .assign_advice( - || format!("hash index_{}", ith), - config.hash_table[0], - ith, - || Value::known(current_hash), - ) - .map(|_| ()) - })?; - } + // set the last row is "custom", a row both enabled and customed + // can only fill a padding row ([0, 0] in MPT mode) + config.s_custom.enable(region, last_offset)?; + Ok((states_in, states_out)) + } - //we directly specify the init state of permutation - states_in.push(c_start.map(StateWord::from)); - states_out.push(c_end.map(StateWord::from)); - } + /// load the table into circuit under the specified config + pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { + let config = &self.config; - // enforce the last row is "not continue", so user can not put a variable - // message till the last row but this should be acceptable (?) - let c_last_ctrl = region.assign_advice( - || "control sponge continue last", - config.s_sponge_continue, - offset, - || Value::known(Fp::ZERO), - )?; + layouter.assign_table( + || "STEP range check", + |mut table| { + (0..STEP + 1).into_iter().try_for_each(|i| { + table + .assign_cell( + || "STEP range check", + config.control_step_range, + i, + || Value::known(Fp::from_u128(i as u128)), + ) + .map(|_| ()) + }) + }, + )?; - // contraint 0 to tail line - region.constrain_equal(c_last_ctrl.cell(), constants_cell[0].cell())?; - Ok((states_in, states_out)) + let (states_in, states_out) = layouter.assign_region( + || "hash table", + |mut region| { + let offset = self.fill_hash_tbl_custom(&mut region)?; + self.fill_hash_tbl_body(&mut region, offset) }, )?; 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); } @@ -563,6 +622,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())?; } } @@ -573,8 +634,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 { @@ -587,6 +650,11 @@ impl Chip for PoseidonHashChip<'_, Fp, ST #[cfg(test)] mod tests { + use std::marker::PhantomData; + + use crate::poseidon::Pow5Chip; + use crate::septidon::SeptidonChip; + use super::*; use halo2_proofs::ff::Field; use halo2_proofs::halo2curves::group::ff::PrimeField; @@ -640,18 +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 { - let hash_tbl = [0; 4].map(|_| meta.advice_column()); + 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, @@ -661,9 +744,15 @@ mod tests { fn synthesize( &self, (config, max_rows): Self::Config, - mut layouter: impl Layouter, + mut layouter: impl Layouter, ) -> Result<(), Error> { - let chip = PoseidonHashChip::::construct(config, self, max_rows); + let chip = PoseidonHashChip::::construct( + config, + &self.table, + max_rows, + false, + Some(Fr::from(42u64)), + ); chip.load(&mut layouter) } } @@ -679,18 +768,36 @@ mod tests { .titled("Hash circuit Layout", ("sans-serif", 60)) .unwrap(); - let circuit = HashCircuit { - calcs: 2, + let message1 = [ + Fr::from_str_vartime("1").unwrap(), + Fr::from_str_vartime("2").unwrap(), + ]; + + let message2 = [ + Fr::from_str_vartime("2").unwrap(), + Fr::from_str_vartime("3").unwrap(), + ]; + + let k = 8; + let circuit = PoseidonHashTable { + inputs: vec![message1, message2], ..Default::default() }; halo2_proofs::dev::CircuitLayout::default() .show_equality_constraints(true) - .render(7, &circuit, &root) + .render(k, &circuit, &root) .unwrap(); } #[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(), @@ -702,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(), @@ -720,19 +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 = 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 = 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 ef67986..b558aee 100644 --- a/src/poseidon.rs +++ b/src/poseidon.rs @@ -6,8 +6,8 @@ use std::marker::PhantomData; use halo2_proofs::{ circuit::{AssignedCell, Chip, Layouter}, - ff::{Field, FromUniformBytes}, - plonk::Error, + ff::{Field, FromUniformBytes, PrimeField}, + 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< F: FromUniformBytes<64> + Ord, @@ -291,7 +301,7 @@ impl< .enumerate() { self.sponge - .absorb(layouter.namespace(|| format!("absorb_{}", i)), value)?; + .absorb(layouter.namespace(|| format!("absorb_{i}")), value)?; } self.sponge .finish_absorbing(layouter.namespace(|| "finish absorbing"))? diff --git a/src/poseidon/pow5.rs b/src/poseidon/pow5.rs index ec11919..e652f5a 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, } @@ -260,6 +262,26 @@ impl Chip for Pow5Chip< } } +impl 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< F: FromUniformBytes<64> + Ord, S: Spec, @@ -349,7 +371,7 @@ impl< let mut state = Vec::with_capacity(WIDTH); let mut load_state_word = |i: usize, value: F| -> Result<_, Error> { let var = region.assign_advice_from_constant( - || format!("state_{}", i), + || format!("state_{i}"), config.state[i], 0, value, @@ -388,7 +410,7 @@ impl< initial_state[i] .0 .copy_advice( - || format!("load state_{}", i), + || format!("load state_{i}"), &mut region, config.state[i], 0, @@ -404,7 +426,7 @@ impl< let constraint_var = match input.0[i].clone() { Some(PaddedWord::Message(word)) => word, Some(PaddedWord::Padding(padding_value)) => region.assign_fixed( - || format!("load pad_{}", i), + || format!("load pad_{i}"), config.rc_b[i], 1, || Value::known(padding_value), @@ -413,7 +435,7 @@ impl< }; constraint_var .copy_advice( - || format!("load input_{}", i), + || format!("load input_{i}"), &mut region, config.state[i], 1, @@ -427,7 +449,7 @@ impl< let constrain_output_word = |i: usize| { region .assign_advice( - || format!("load output_{}", i), + || format!("load output_{i}"), config.state[i], 2, || { @@ -461,7 +483,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 { @@ -574,7 +596,7 @@ impl Pow5State { let r: Vec<_> = Some(r_0).into_iter().chain(r_i).collect(); region.assign_advice( - || format!("round_{} partial_sbox", round), + || format!("round_{round} partial_sbox"), config.partial_sbox, offset, || r[0], @@ -635,7 +657,7 @@ impl Pow5State { let load_state_word = |i: usize| { initial_state[i] .0 - .copy_advice(|| format!("load state_{}", i), region, config.state[i], 0) + .copy_advice(|| format!("load state_{i}"), region, config.state[i], 0) .map(StateWord) }; @@ -657,7 +679,7 @@ impl Pow5State { // Load the round constants. let mut load_round_constant = |i: usize| { region.assign_fixed( - || format!("round_{} rc_{}", round, i), + || format!("round_{round} rc_{i}"), config.rc_a[i], offset, || Value::known(config.round_constants[round][i]), @@ -673,7 +695,7 @@ impl Pow5State { let next_state_word = |i: usize| { let value = next_state[i]; let var = region.assign_advice( - || format!("round_{} state_{}", next_round, i), + || format!("round_{next_round} state_{i}"), config.state[i], offset + 1, || value, diff --git a/src/poseidon/primitives.rs b/src/poseidon/primitives.rs index 3eadbab..def7a1b 100644 --- a/src/poseidon/primitives.rs +++ b/src/poseidon/primitives.rs @@ -25,7 +25,10 @@ pub(crate) mod pasta; //pub(crate) mod test_vectors; mod p128pow5t3; +pub(crate) mod p128pow5t3_compact; + pub use p128pow5t3::P128Pow5T3; +pub use p128pow5t3_compact::P128Pow5T3CompactSpec as P128Pow5T3Compact; use grain::SboxType; @@ -336,7 +339,7 @@ impl Domain for Const type Padding = iter::Take>; fn name() -> String { - format!("ConstantLength<{}>", L) + format!("ConstantLength<{L}>") } fn initial_capacity_element() -> F { @@ -364,7 +367,7 @@ impl Domain for Const type Padding = as Domain>::Padding; fn name() -> String { - format!("ConstantLength<{}> in iden3's style", L) + format!("ConstantLength<{L}> in iden3's style") } // iden3's scheme do not set any capacity mark @@ -523,7 +526,7 @@ mod tests { use super::pasta::Fp; use halo2_proofs::ff::PrimeField; - use super::{permute, ConstantLength, Hash, P128Pow5T3, Spec}; + use super::{permute, ConstantLength, Hash, P128Pow5T3, P128Pow5T3Compact, Spec}; type OrchardNullifier = P128Pow5T3; #[test] @@ -555,4 +558,15 @@ mod tests { let result = hasher.hash(message); assert_eq!(state[0], result); } + + #[test] + fn spec_equivalence() { + let message = [Fp::from(6), Fp::from(42)]; + let hasher1 = Hash::<_, P128Pow5T3, ConstantLength<2>, 3, 2>::init(); + let hasher2 = Hash::<_, P128Pow5T3Compact, ConstantLength<2>, 3, 2>::init(); + + let result1 = hasher1.hash(message.clone()); + let result2 = hasher2.hash(message.clone()); + assert_eq!(result1, result2); + } } diff --git a/src/poseidon/primitives/bn256/mod.rs b/src/poseidon/primitives/bn256/mod.rs index 594dec7..20ee3e2 100644 --- a/src/poseidon/primitives/bn256/mod.rs +++ b/src/poseidon/primitives/bn256/mod.rs @@ -28,7 +28,8 @@ mod tests { use halo2_proofs::ff::{Field, FromUniformBytes}; use crate::poseidon::primitives::p128pow5t3::P128Pow5T3; - use crate::poseidon::primitives::Spec; + use crate::poseidon::primitives::p128pow5t3_compact::P128Pow5T3CompactSpec; + use crate::poseidon::primitives::{permute, Spec}; use super::*; @@ -114,4 +115,57 @@ mod tests { } } } + + #[test] + fn test_compact_constants() { + let input = [ + Fp::from_raw([ + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + ]), + Fp::from_raw([ + 0x0000_0000_0000_0001, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + ]), + Fp::from_raw([ + 0x0000_0000_0000_0002, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + 0x0000_0000_0000_0000, + ]), + ]; + + let output = { + let mut state = input.clone(); + + let (rc, mds, _inv) = P128Pow5T3::::constants(); + permute::, 3, 2>(&mut state, &mds, &rc[..]); + + // This is the raw form with 3 constants per round. + assert_ne!(rc[4][1], Fp::zero()); + + state + }; + + let output_compact = { + let mut state = input.clone(); + + let (rc, mds, _inv) = P128Pow5T3CompactSpec::::constants(); + permute::, 3, 2>(&mut state, &mds, &rc[..]); + + // This is the compact form with 1 constant per partial round. + for i in 4..4 + 57 { + assert_eq!(rc[i][1], Fp::zero()); + assert_eq!(rc[i][2], Fp::zero()); + } + + state + }; + + assert_eq!(output, output_compact); + } } diff --git a/src/poseidon/primitives/grain.rs b/src/poseidon/primitives/grain.rs index 2412258..f191762 100644 --- a/src/poseidon/primitives/grain.rs +++ b/src/poseidon/primitives/grain.rs @@ -44,7 +44,7 @@ impl SboxType { } pub(super) struct Grain + Ord> { - state: BitArr!(for 80, in Msb0, u8), + state: BitArr!(for 80, in u8, Msb0), next_bit: usize, _field: PhantomData, } @@ -52,7 +52,7 @@ pub(super) struct Grain + Ord> { impl + Ord> Grain { pub(super) fn new(sbox: SboxType, t: u16, r_f: u16, r_p: u16) -> Self { // Initialize the LFSR state. - let mut state = bitarr![Msb0, u8; 1; STATE]; + let mut state = bitarr![u8, Msb0; 1; STATE]; let mut set_bits = |offset: usize, len, value| { // Poseidon reference impl sets initial state bits in MSB order. for i in 0..len { diff --git a/src/poseidon/primitives/p128pow5t3.rs b/src/poseidon/primitives/p128pow5t3.rs index 95f59e5..03d2759 100644 --- a/src/poseidon/primitives/p128pow5t3.rs +++ b/src/poseidon/primitives/p128pow5t3.rs @@ -33,7 +33,7 @@ impl + Ord> Spec for P1 } fn sbox(val: Fp) -> Fp { - val.pow_vartime(&[5]) + val.pow_vartime([5]) } fn secure_mds() -> usize { diff --git a/src/poseidon/primitives/p128pow5t3_compact.rs b/src/poseidon/primitives/p128pow5t3_compact.rs new file mode 100644 index 0000000..d669525 --- /dev/null +++ b/src/poseidon/primitives/p128pow5t3_compact.rs @@ -0,0 +1,83 @@ +use halo2_proofs::ff::{FromUniformBytes, PrimeField}; +use std::marker::PhantomData; + +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 +/// standard number of rounds for 128-bit security "with margin". +/// +#[derive(Debug)] +pub struct P128Pow5T3CompactSpec { + _marker: PhantomData, +} + +impl + Ord> Spec + for P128Pow5T3CompactSpec +{ + fn full_rounds() -> usize { + 8 + } + + fn partial_rounds() -> usize { + Fp::partial_rounds() + } + + fn sbox(val: Fp) -> Fp { + val.pow_vartime([5]) + } + + fn secure_mds() -> usize { + unimplemented!() + } + + fn constants() -> (Vec<[Fp; 3]>, Mds, Mds) { + let (mut rc, mds, inv) = (Fp::round_constants(), Fp::mds(), Fp::mds_inv()); + + let first_partial = Self::full_rounds() / 2; + let after_partials = first_partial + Self::partial_rounds(); + + // Propagate the constants of each partial round into the next. + for i in first_partial..after_partials { + // Extract the constants rc[i][1] and rc[i][2] that do not pass through the S-box. + // Leave the value 0 in their place. + // rc[i][0] stays in place. + let rc_tail = vec_remove_tail(&mut rc[i]); + + // Pass forward through the MDS matrix. + let rc_carry = mat_mul(&mds, &rc_tail); + + // Accumulate the carried constants into the next round. + vec_accumulate(&mut rc[i + 1], &rc_carry); + } + // Now constants have accumulated into the next full round. + + (rc, mds, inv) + } +} + +fn mat_mul(mat: &Mds, input: &[Fp; T]) -> [Fp; T] { + let mut out = [Fp::ZERO; T]; + #[allow(clippy::needless_range_loop)] + for i in 0..T { + for j in 0..T { + out[i] += mat[i][j] * input[j]; + } + } + out +} + +fn vec_accumulate(a: &mut [Fp; T], b: &[Fp; T]) { + for i in 0..T { + a[i] += b[i]; + } +} + +fn vec_remove_tail(a: &mut [Fp; T]) -> [Fp; T] { + let mut tail = [Fp::ZERO; T]; + for i in 1..T { + tail[i] = a[i]; + a[i] = Fp::ZERO; + } + tail +} 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..f7df926 --- /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::{ff::PrimeField, 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::{ff::PrimeField, 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 b519e13..d513028 100644 --- a/tests/hash_proving.rs +++ b/tests/hash_proving.rs @@ -18,6 +18,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; @@ -26,7 +27,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 { @@ -34,7 +35,7 @@ impl Circuit for TestCircuit { } fn configure(meta: &mut ConstraintSystem) -> Self::Config { - let hash_tbl = [0; 4].map(|_| meta.advice_column()); + let hash_tbl = [0; 5].map(|_| meta.advice_column()); PoseidonHashConfig::configure_sub(meta, hash_tbl, DEFAULT_STEP) } @@ -43,7 +44,13 @@ impl Circuit for TestCircuit { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - let chip = PoseidonHashChip::::construct(config, &self.0, self.1); + let chip = PoseidonHashChip::>::construct( + config, + &self.0, + self.1, + false, + Some(Fp::from(42u64)), + ); chip.load(&mut layouter) } } @@ -121,10 +128,12 @@ fn proof_and_verify() { Fp::from_str_vartime("2").unwrap(), ], [ - Fp::from_str_vartime("0").unwrap(), + Fp::from_str_vartime("30").unwrap(), Fp::from_str_vartime("1").unwrap(), ], + [Fp::from_str_vartime("65536").unwrap(), Fp::zero()], ], + controls: vec![Fp::zero(), Fp::from(46u64), Fp::from(14u64)], ..Default::default() }, 4,