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/primitives.rs b/src/poseidon/primitives.rs index dc7865d..112b0ae 100644 --- a/src/poseidon/primitives.rs +++ b/src/poseidon/primitives.rs @@ -24,6 +24,8 @@ pub(crate) mod pasta; //pub(crate) mod test_vectors; mod p128pow5t3; +pub(crate) mod p128pow5t3_compact; + pub use p128pow5t3::P128Pow5T3; use grain::SboxType; diff --git a/src/poseidon/primitives/bn256/mod.rs b/src/poseidon/primitives/bn256/mod.rs index 3c49ab5..ace9e18 100644 --- a/src/poseidon/primitives/bn256/mod.rs +++ b/src/poseidon/primitives/bn256/mod.rs @@ -26,7 +26,8 @@ mod tests { use std::marker::PhantomData; 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::*; @@ -112,4 +113,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/p128pow5t3_compact.rs b/src/poseidon/primitives/p128pow5t3_compact.rs new file mode 100644 index 0000000..7b2caab --- /dev/null +++ b/src/poseidon/primitives/p128pow5t3_compact.rs @@ -0,0 +1,82 @@ +use std::marker::PhantomData; + +use halo2_proofs::arithmetic::FieldExt; + +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 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..a746716 --- /dev/null +++ b/src/septidon.rs @@ -0,0 +1,16 @@ +//! An implementation using septuple rounds. +//! See: src/README.md + +mod control; +mod full_round; +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..239269a --- /dev/null +++ b/src/septidon/full_round.rs @@ -0,0 +1,48 @@ +use super::loop_chip::LoopBody; +use super::params::mds; +use super::state::{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) + } + + /// 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/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..37b3950 --- /dev/null +++ b/src/septidon/septidon_chip.rs @@ -0,0 +1,146 @@ +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 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 + } + + /// 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..8cdd4ec --- /dev/null +++ b/src/septidon/transition_round.rs @@ -0,0 +1,124 @@ +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. + 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)) + } +}