apply feedback

Author: Parrot7483

libcrux-intrinsics/src/avx2.rs

@@ -1,5 +1,3 @@
-#![allow(unused_unsafe)]
-
 #[cfg(all(target_arch = "x86", not(hax)))]
 pub use core::arch::x86::*;
 #[cfg(all(target_arch = "x86_64", not(hax)))]

libcrux-sha3/Cargo.toml

@@ -32,7 +32,6 @@ harness = false
 
 [dev-dependencies]
 criterion = "0.7.0"
-hax-lib.workspace = true
 hex = "0.4.3"
 rand = "0.9"
 cavp = { version = "0.0.2", path = "../cavp" }

libcrux-sha3/hax.py

@@ -116,7 +116,7 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             "--interfaces",
             interface_include,
         ]
-        hax_env = {"RUSTFLAGS": "-C debug-assertions=off"}
+        hax_env = {}
         shell(
             cargo_hax_into,
             cwd=".",

libcrux-sha3/src/generic_keccak/xof.rs

@@ -1,6 +1,6 @@
 use crate::{
     generic_keccak::KeccakState,
-    traits::{Absorb, KeccakItem, Squeeze1},
+    traits::{Absorb, KeccakItem, Squeeze},
 };
 
 /// The internal keccak state that can also buffer inputs to absorb.
@@ -131,28 +131,24 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
     /// If `consumed > 0` is returned, `self.buf` contains a full block to be
     /// loaded.
     // Note: consciously not inlining this function to avoid using too much stack
-    #[hax_lib::requires(PARALLEL_LANES > 0 && self.buf_len < RATE)]
     pub(crate) fn fill_buffer(&mut self, inputs: &[&[u8]; PARALLEL_LANES]) -> usize {
         let input_len = inputs[0].len();
-
-        // Nothing buffered, buffer full, or no input
-        if self.buf_len == 0 || self.buf_len >= RATE || input_len == 0 {
-            return 0;
-        }
-
-        // Remaining space to complete a full block
-        let need = RATE - self.buf_len;
-        if input_len < need {
-            return 0;
-        }
-
-        let end = RATE; // buf_len + need == RATE
-        #[allow(clippy::needless_range_loop)]
-        for i in 0..PARALLEL_LANES {
-            self.buf[i][self.buf_len..end].copy_from_slice(&inputs[i][..need]);
+        let mut consumed = 0;
+        if self.buf_len > 0 {
+            // There's something buffered internally to consume.
+            if self.buf_len + input_len >= RATE {
+                // We have enough data when combining the internal buffer and
+                // the input.
+                consumed = RATE - self.buf_len;
+
+                #[allow(clippy::needless_range_loop)]
+                for i in 0..PARALLEL_LANES {
+                    self.buf[i][self.buf_len..].copy_from_slice(&inputs[i][..consumed]);
+                }
+                self.buf_len += consumed;
+            }
         }
-        self.buf_len = end;
-        need
+        consumed
     }
 
     /// Absorb a final block.
@@ -187,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>: Squeeze1<STATE>,
+        KeccakState<1, STATE>: Squeeze<STATE>,
     {
         if self.sponge {
             // If we called `squeeze` before, call f1600 first.

libcrux-sha3/src/simd/portable.rs

@@ -5,7 +5,7 @@ use crate::{generic_keccak::KeccakState, traits::*};
 #[inline(always)]
 fn rotate_left<const LEFT: i32, const RIGHT: i32>(x: u64) -> u64 {
     debug_assert!(LEFT + RIGHT == 64);
-    u64::rotate_left(x, LEFT as u32)
+    x.rotate_left(LEFT as u32)
 }
 
 #[inline(always)]
@@ -142,7 +142,7 @@ impl Absorb<1> for KeccakState<1, u64> {
     }
 }
 
-impl Squeeze1<u64> for KeccakState<1, u64> {
+impl Squeeze<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_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
+class t_Squeeze (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,10 +84,14 @@ class t_Squeeze1 (v_Self: Type0) (v_T: Type0) = {
 }
 "
 )]
-pub(crate) trait Squeeze1<T: KeccakItem<1>> {
+pub(crate) trait Squeeze<T: KeccakItem<1>> {
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize);
 }
 
+// TODO: Renaming the squeeze functions of the Squeeze2 and Squeeze4 Trait is currently
+// necessary because F* will not find the correct pre conditions otherwise. This is
+// most likely fixed when doing full type checking.
+
 /// Trait to squeeze bytes out of the state.
 ///
 /// Note that this is implemented for each platform (1, 2, 4) because hax can't