formatting and renaming

Author: Parrot7483

libcrux-sha3/Cargo.toml

@@ -18,10 +18,6 @@ libcrux-platform = { version = "0.0.2", path = "../sys/platform" }
 libcrux-intrinsics = { version = "0.0.3", path = "../libcrux-intrinsics" }
 hax-lib.workspace = true
 
-# This is only required for verification.
-# The hax config is set by the hax toolchain.
-[target.'cfg(hax)'.dependencies]
-
 [features]
 simd128 = ["libcrux-intrinsics/simd128"]
 simd256 = ["libcrux-intrinsics/simd256"]

libcrux-sha3/hax.py

@@ -57,7 +57,7 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             cargo_args = []
         else:
             cargo_args = ["-C", "--features", "simd128,simd256", ";"]
-        
+
         cargo_hax_into = [
             "cargo",
             "hax",

libcrux-sha3/src/generic_keccak.rs

@@ -104,21 +104,25 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
         self.set(2, 0, T::xor_and_rotate::<3, 61>(self[(2, 0)], t[0]));
         self.set(3, 0, T::xor_and_rotate::<41, 23>(self[(3, 0)], t[0]));
         self.set(4, 0, T::xor_and_rotate::<18, 46>(self[(4, 0)], t[0]));
+
         self.set(0, 1, T::xor_and_rotate::<1, 63>(self[(0, 1)], t[1]));
         self.set(1, 1, T::xor_and_rotate::<44, 20>(self[(1, 1)], t[1]));
         self.set(2, 1, T::xor_and_rotate::<10, 54>(self[(2, 1)], t[1]));
         self.set(3, 1, T::xor_and_rotate::<45, 19>(self[(3, 1)], t[1]));
         self.set(4, 1, T::xor_and_rotate::<2, 62>(self[(4, 1)], t[1]));
+
         self.set(0, 2, T::xor_and_rotate::<62, 2>(self[(0, 2)], t[2]));
         self.set(1, 2, T::xor_and_rotate::<6, 58>(self[(1, 2)], t[2]));
         self.set(2, 2, T::xor_and_rotate::<43, 21>(self[(2, 2)], t[2]));
         self.set(3, 2, T::xor_and_rotate::<15, 49>(self[(3, 2)], t[2]));
         self.set(4, 2, T::xor_and_rotate::<61, 3>(self[(4, 2)], t[2]));
+
         self.set(0, 3, T::xor_and_rotate::<28, 36>(self[(0, 3)], t[3]));
         self.set(1, 3, T::xor_and_rotate::<55, 9>(self[(1, 3)], t[3]));
         self.set(2, 3, T::xor_and_rotate::<25, 39>(self[(2, 3)], t[3]));
         self.set(3, 3, T::xor_and_rotate::<21, 43>(self[(3, 3)], t[3]));
         self.set(4, 3, T::xor_and_rotate::<56, 8>(self[(4, 3)], t[3]));
+
         self.set(0, 4, T::xor_and_rotate::<27, 37>(self[(0, 4)], t[4]));
         self.set(1, 4, T::xor_and_rotate::<20, 44>(self[(1, 4)], t[4]));
         self.set(2, 4, T::xor_and_rotate::<39, 25>(self[(2, 4)], t[4]));

libcrux-sha3/src/generic_keccak/xof.rs

@@ -1,6 +1,6 @@
 use crate::{
     generic_keccak::KeccakState,
-    traits::{Absorb, KeccakItem, Squeeze},
+    traits::{Absorb, KeccakItem, Squeeze1},
 };
 
 /// The internal keccak state that can also buffer inputs to absorb.
@@ -183,7 +183,7 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
     #[inline(always)]
     pub(crate) fn squeeze(&mut self, out: &mut [u8])
     where
-        KeccakState<1, STATE>: Squeeze<STATE>,
+        KeccakState<1, STATE>: Squeeze1<STATE>,
     {
         if self.sponge {
             // If we called `squeeze` before, call f1600 first.

libcrux-sha3/src/simd/portable.rs

@@ -142,7 +142,7 @@ impl Absorb<1> for KeccakState<1, u64> {
     }
 }
 
-impl Squeeze<u64> for KeccakState<1, u64> {
+impl Squeeze1<u64> for KeccakState<1, u64> {
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize) {
         store_block::<RATE>(&self.st, out, start, len);
     }

libcrux-sha3/src/traits.rs

@@ -74,7 +74,7 @@ pub(crate) trait Absorb<const N: usize> {
 #[hax_lib::fstar::replace(
     interface,
     "
-class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
+class t_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
   f_squeeze_pre:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> Type0;
   f_squeeze_post:v_RATE: usize -> v_Self -> t_Slice u8 -> usize -> usize -> t_Slice u8 -> Type0;
   f_squeeze:v_RATE: usize -> x0: v_Self -> x1: t_Slice u8 -> x2: usize -> x3: usize
@@ -84,7 +84,7 @@ class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
 }
 "
 )]
-pub(crate) trait Squeeze<T: KeccakItem<1>> {
+pub(crate) trait Squeeze1<T: KeccakItem<1>> {
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize);
 }