Septidon: a circuit for Poseidon septuple rounds

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;
 

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;

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::<Fp>::constants();
+            permute::<Fp, P128Pow5T3<Fp>, 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::<Fp>::constants();
+            permute::<Fp, P128Pow5T3CompactSpec<Fp>, 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);
+    }
 }

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<Fp> {
+    _marker: PhantomData<Fp>,
+}
+
+impl<Fp: P128Pow5T3Constants> Spec<Fp, 3, 2> for P128Pow5T3CompactSpec<Fp> {
+    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<Fp, 3>, Mds<Fp, 3>) {
+        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<Fp: FieldExt, const T: usize>(mat: &Mds<Fp, T>, 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<Fp: FieldExt, const T: usize>(a: &mut [Fp; T], b: &[Fp; T]) {
+    for i in 0..T {
+        a[i] += b[i];
+    }
+}
+
+fn vec_remove_tail<Fp: FieldExt, const T: usize>(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
+}

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;

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.