fmt

cryspen · Nov 5, 2024 · e542ac3 · e542ac3
1 parent dac387a
commit e542ac3
Show file tree

Hide file tree

Showing 4 changed files with 25 additions and 16 deletions.
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti
@@ -24,19 +24,19 @@ val shake256_x4
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256x4)
+val squeeze_first_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128x4)
+val squeeze_next_block (state: t_Shake128x4)
     : Prims.Pure
       (t_Shake128x4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -140,7 +140,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256x4)
+val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti
@@ -21,6 +21,9 @@ val t_Shake256Absorb:Type0
 
 val t_Shake256Squeeze:Type0
 
+val init_absorb__init_absorb (input: t_Slice u8)
+    : Prims.Pure Libcrux_sha3.Portable.t_KeccakState Prims.l_True (fun _ -> Prims.l_True)
+
 val init_absorb (input0 input1 input2 input3: t_Slice u8)
     : Prims.Pure t_Shake128X4 Prims.l_True (fun _ -> Prims.l_True)
 
@@ -69,22 +72,22 @@ val shake256_init: Prims.unit -> Prims.Pure t_Shake256Absorb Prims.l_True (fun _
 val shake256_squeeze (st: t_Shake256Squeeze) (out: t_Slice u8)
     : Prims.Pure (t_Shake256Squeeze & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_first_block_shake256 (x: t_Shake256)
+val squeeze_first_block_shake256 (state: t_Shake256)
     : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256X4)
+val squeeze_first_block_x4 (state: t_Shake256X4)
     : Prims.Pure
       (t_Shake256X4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128X4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128X4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128X4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128X4)
+val squeeze_next_block (state: t_Shake128X4)
     : Prims.Pure
       (t_Shake128X4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -188,7 +191,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128X4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_shake256 (x: t_Shake256)
+val squeeze_next_block_shake256 (state: t_Shake256)
     : Prims.Pure (t_Shake256 & t_Array u8 (sz 136)) Prims.l_True (fun _ -> Prims.l_True)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
@@ -238,7 +241,7 @@ let impl_2: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof t_Shake256 =
       self, hax_temp_output <: (t_Shake256 & t_Array u8 (sz 136))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256X4)
+val squeeze_next_block_x4 (state: t_Shake256X4)
     : Prims.Pure
       (t_Shake256X4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti
@@ -27,19 +27,19 @@ val shake256_x4
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_block_x4 (x: t_Shake256x4)
+val squeeze_first_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val squeeze_first_five_blocks (x: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
+val squeeze_first_five_blocks (state: t_Shake128x4) (out0 out1 out2 out3: t_Array u8 (sz 840))
     : Prims.Pure
       (t_Shake128x4 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) &
         t_Array u8 (sz 840)) Prims.l_True (fun _ -> Prims.l_True)
 
-val squeeze_next_block (x: t_Shake128x4)
+val squeeze_next_block (state: t_Shake128x4)
     : Prims.Pure
       (t_Shake128x4 &
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
@@ -143,7 +143,7 @@ let impl: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 =
         (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168)))
   }
 
-val squeeze_next_block_x4 (x: t_Shake256x4)
+val squeeze_next_block_x4 (state: t_Shake256x4)
     : Prims.Pure
       (t_Shake256x4 &
         (t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136) & t_Array u8 (sz 136)))

diff --git a/libcrux-ml-dsa/src/hash_functions.rs b/libcrux-ml-dsa/src/hash_functions.rs
@@ -76,9 +76,9 @@ pub(crate) mod shake128 {
 
 /// A portable implementation of [`shake128::Xof`] and [`shake256::Xof`].
 pub(crate) mod portable {
+    use super::{shake128, shake256};
     use libcrux_sha3::portable::incremental;
     use libcrux_sha3::portable::KeccakState;
-    use super::{shake128, shake256};
 
     /// Portable SHAKE 128 x4 state.
     ///
@@ -405,7 +405,13 @@ pub(crate) mod simd256 {
         out2: &mut [u8; shake128::FIVE_BLOCKS_SIZE],
         out3: &mut [u8; shake128::FIVE_BLOCKS_SIZE],
     ) {
-        x4::incremental::shake128_squeeze_first_five_blocks(&mut state.state, out0, out1, out2, out3);
+        x4::incremental::shake128_squeeze_first_five_blocks(
+            &mut state.state,
+            out0,
+            out1,
+            out2,
+            out3,
+        );
     }
 
     fn squeeze_next_block(