From 5468e18ccce4b6a56df4980f8e27d8709537a5ce Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Thu, 18 Sep 2025 13:06:10 +0200
Subject: [PATCH 1/6] Add full type check for SHA3 portable

---
 .github/workflows/sha3-hax.yml              |  26 +-
 libcrux-sha3/src/generic_keccak.rs          |  75 ++++-
 libcrux-sha3/src/generic_keccak/portable.rs |  54 ++++
 libcrux-sha3/src/generic_keccak/xof.rs      | 295 +++++++++++++++-----
 libcrux-sha3/src/lib.rs                     |  47 +++-
 libcrux-sha3/src/portable.rs                |  90 +++++-
 libcrux-sha3/src/simd/portable.rs           |  78 +++++-
 libcrux-sha3/src/traits.rs                  |  67 ++++-
 8 files changed, 638 insertions(+), 94 deletions(-)

diff --git a/.github/workflows/sha3-hax.yml b/.github/workflows/sha3-hax.yml
index 8cc14ad6e..16a7abd5d 100644
--- a/.github/workflows/sha3-hax.yml
+++ b/.github/workflows/sha3-hax.yml
@@ -103,6 +103,28 @@ jobs:
         working-directory: libcrux-sha3
         run: ./hax.py prove --admit
 
+  type-check-portable:
+    runs-on: ubuntu-latest
+    needs:
+      - get-hax-ref
+      - extract-portable
+    if: ${{ github.event_name != 'merge_group' }}
+    steps:
+      - uses: actions/checkout@v5
+      - uses: hacspec/hax-actions@main
+        with:
+          hax_reference: ${{ github.event.inputs.hax_ref || needs.get-hax-ref.outputs.hax_ref }}
+          fstar: v2025.02.17
+
+      - uses: actions/download-artifact@v5
+        with:
+          name: fstar-extractions-portable
+          path: .
+
+      - name: 🏃 Full type check SHA3 crate (portable)
+        working-directory: libcrux-sha3
+        run: ./hax.py prove
+
   sha3-extract-hax-status:
     if: ${{ always() }}
     needs: [get-hax-ref, extract]
@@ -115,9 +137,9 @@ jobs:
         if: ${{ (contains(needs.*.result, 'failure')) }}
         run: exit 1
 
-  sha3-lax-portable-hax-status:
+  sha3-type-check-portable-hax-status:
     if: ${{ always() }}
-    needs: [get-hax-ref, lax-portable]
+    needs: [get-hax-ref, lax-portable, type-check-portable]
     runs-on: ubuntu-latest
     steps:
       - name: Successful
diff --git a/libcrux-sha3/src/generic_keccak.rs b/libcrux-sha3/src/generic_keccak.rs
index d1e75dab2..70587c9db 100644
--- a/libcrux-sha3/src/generic_keccak.rs
+++ b/libcrux-sha3/src/generic_keccak.rs
@@ -5,6 +5,9 @@ use core::ops::Index;
 
 use crate::traits::*;
 
+#[cfg(hax)]
+use hax_lib::int::*;
+
 /// A generic Xof API.
 pub(crate) mod xof;
 
@@ -97,32 +100,43 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
-    #[hax_lib::fstar::replace_body("assert true")]
-    fn rho(&mut self, t: [T; 5]) {
+    fn rho_0(&mut self, t: [T; 5]) {
         self.set(0, 0, T::xor(self[(0, 0)], t[0]));
         self.set(1, 0, T::xor_and_rotate::<36, 28>(self[(1, 0)], t[0]));
         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]));
+    }
 
+    #[inline(always)]
+    fn rho_1(&mut self, t: [T; 5]) {
         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]));
+    }
 
+    #[inline(always)]
+    fn rho_2(&mut self, t: [T; 5]) {
         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]));
+    }
 
+    #[inline(always)]
+    fn rho_3(&mut self, t: [T; 5]) {
         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]));
+    }
 
+    #[inline(always)]
+    fn rho_4(&mut self, t: [T; 5]) {
         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]));
@@ -131,29 +145,51 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
-    #[hax_lib::fstar::replace_body("assert true")]
-    fn pi(&mut self) {
-        let old = *self;
+    fn rho(&mut self, t: [T; 5]) {
+        self.rho_0(t);
+        self.rho_1(t);
+        self.rho_2(t);
+        self.rho_3(t);
+        self.rho_4(t);
+    }
 
+    #[inline(always)]
+    fn pi_0(&mut self, old: KeccakState<N, T>) {
         self.set(1, 0, old[(0, 3)]);
         self.set(2, 0, old[(0, 1)]);
         self.set(3, 0, old[(0, 4)]);
         self.set(4, 0, old[(0, 2)]);
+    }
+
+    #[inline(always)]
+    fn pi_1(&mut self, old: KeccakState<N, T>) {
         self.set(0, 1, old[(1, 1)]);
         self.set(1, 1, old[(1, 4)]);
         self.set(2, 1, old[(1, 2)]);
         self.set(3, 1, old[(1, 0)]);
         self.set(4, 1, old[(1, 3)]);
+    }
+
+    #[inline(always)]
+    fn pi_2(&mut self, old: KeccakState<N, T>) {
         self.set(0, 2, old[(2, 2)]);
         self.set(1, 2, old[(2, 0)]);
         self.set(2, 2, old[(2, 3)]);
         self.set(3, 2, old[(2, 1)]);
         self.set(4, 2, old[(2, 4)]);
+    }
+
+    #[inline(always)]
+    fn pi_3(&mut self, old: KeccakState<N, T>) {
         self.set(0, 3, old[(3, 3)]);
         self.set(1, 3, old[(3, 1)]);
         self.set(2, 3, old[(3, 4)]);
         self.set(3, 3, old[(3, 2)]);
         self.set(4, 3, old[(3, 0)]);
+    }
+
+    #[inline(always)]
+    fn pi_4(&mut self, old: KeccakState<N, T>) {
         self.set(0, 4, old[(4, 4)]);
         self.set(1, 4, old[(4, 2)]);
         self.set(2, 4, old[(4, 0)]);
@@ -162,7 +198,17 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
-    #[hax_lib::fstar::replace_body("assert true")]
+    fn pi(&mut self) {
+        let old: KeccakState<N, T> = *self;
+
+        self.pi_0(old);
+        self.pi_1(old);
+        self.pi_2(old);
+        self.pi_3(old);
+        self.pi_4(old);
+    }
+
+    #[inline(always)]
     fn chi(&mut self) {
         let old = *self;
 
@@ -196,11 +242,17 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        N > 0 &&
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        start.to_int() + RATE.to_int() <= blocks[0].len().to_int()
+    )]
     fn absorb_block<const RATE: usize>(&mut self, blocks: &[&[u8]; N], start: usize)
     where
         Self: Absorb<N>,
     {
-        #[cfg(not(eurydice))]
+        #[cfg(not(any(eurydice, hax)))]
         debug_assert!(blocks.iter().all(|buf| buf.len() == blocks[0].len()));
 
         self.load_block::<RATE>(blocks, start);
@@ -208,6 +260,13 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        N > 0 &&
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        len < RATE &&
+        start.to_int() + len.to_int() <= last[0].len().to_int()
+    )]
     pub(crate) fn absorb_final<const RATE: usize, const DELIM: u8>(
         &mut self,
         last: &[&[u8]; N],
@@ -219,7 +278,7 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
         #[cfg(not(eurydice))]
         debug_assert!(N > 0 && len < RATE);
 
-        #[cfg(not(eurydice))]
+        #[cfg(not(any(eurydice, hax)))]
         debug_assert!(last.iter().all(|buf| buf.len() == last[0].len()));
 
         self.load_last::<RATE, DELIM>(last, start, len);
diff --git a/libcrux-sha3/src/generic_keccak/portable.rs b/libcrux-sha3/src/generic_keccak/portable.rs
index 04a12c0b5..eee6341d1 100644
--- a/libcrux-sha3/src/generic_keccak/portable.rs
+++ b/libcrux-sha3/src/generic_keccak/portable.rs
@@ -1,18 +1,40 @@
 use super::*;
 
+#[hax_lib::attributes]
 impl KeccakState<1, u64> {
     #[inline(always)]
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        start.to_int() + RATE.to_int() <= out.len().to_int()
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub(crate) fn squeeze_next_block<const RATE: usize>(&mut self, out: &mut [u8], start: usize) {
         self.keccakf1600();
         self.squeeze::<RATE>(out, start, RATE);
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        RATE <= out.len()
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub(crate) fn squeeze_first_block<const RATE: usize>(&self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        3 * RATE <= out.len()
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub(crate) fn squeeze_first_three_blocks<const RATE: usize>(&mut self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
 
@@ -24,6 +46,13 @@ impl KeccakState<1, u64> {
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        5 * RATE <= out.len()
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub(crate) fn squeeze_first_five_blocks<const RATE: usize>(&mut self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
 
@@ -41,11 +70,34 @@ impl KeccakState<1, u64> {
     }
 }
 
+#[hax_lib::fstar::before(
+    r#"
+let rec mul_succ_le (k n d: nat)
+  : Lemma
+    (requires k < n && d > 0)
+    (ensures k * d + d <= n * d)
+    (decreases n) =
+  if n = 0 then ()
+  else if k = n - 1 then ()
+  else mul_succ_le k (n - 1) d
+"#
+)]
+#[hax_lib::requires(
+    RATE != 0 &&
+    RATE <= 200 &&
+    RATE % 8 == 0 /* &&
+    data.len() + RATE <= usize::MAX */
+)]
+#[hax_lib::ensures(|_|
+    future(out).len() == out.len())
+]
+#[hax_lib::fstar::options("--split_queries always --query_stats --z3rlimit 300")]
 #[inline]
 pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(data: &[u8], out: &mut [u8]) {
     let mut s = KeccakState::<1, u64>::new();
     let data_len = data.len();
     for i in 0..data_len / RATE {
+        hax_lib::fstar!("mul_succ_le (v i) (v (data_len /! v_RATE)) (v v_RATE)");
         s.absorb_block::<RATE>(&[data], i * RATE);
     }
     let rem = data_len % RATE;
@@ -60,6 +112,8 @@ pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(data: &[u8], out: &mut
     } else {
         s.squeeze::<RATE>(out, 0, RATE);
         for i in 1..blocks {
+            hax_lib::loop_invariant!(|_: usize| out.len() == outlen);
+            hax_lib::fstar!("mul_succ_le (v i) (v blocks) (v v_RATE)");
             s.keccakf1600();
             s.squeeze::<RATE>(out, i * RATE, RATE);
         }
diff --git a/libcrux-sha3/src/generic_keccak/xof.rs b/libcrux-sha3/src/generic_keccak/xof.rs
index 320769960..d5ef61e93 100644
--- a/libcrux-sha3/src/generic_keccak/xof.rs
+++ b/libcrux-sha3/src/generic_keccak/xof.rs
@@ -1,10 +1,51 @@
+use hax_lib::int::*;
+
 use crate::{
     generic_keccak::KeccakState,
-    traits::{Absorb, KeccakItem, Squeeze1},
+    traits::{Absorb, KeccakItem, Squeeze},
 };
 
+// Helper lemma for F* verification in the `absorb_full` loop.
+//
+// Proves that for any a, i, n, rate > 0 with i < n,
+// we have a + i * rate + rate ≤ a + n * rate,
+// i.e. each block‐offset stays within the total input length.
+#[hax_lib::fstar::before(
+    r#"
+let rec lemma_offset_plus_rate_le_total (a i n rate: nat)
+    : Lemma
+        (requires i < n && rate > 0)
+        (ensures a + i * rate + rate <= a + n * rate)
+        (decreases n) =
+    if n = 0 then ()
+    else if i = n - 1 then ()
+    else lemma_offset_plus_rate_le_total a i (n - 1) rate
+"#
+)]
+// Helper lemma for F* verification in the 'squeeze' function.
+//
+// Proves the division‐multiplication‐modulo identity:
+//   for any a, b with b != 0,
+//   (a / b) * b + (a % b) = a.
+#[hax_lib::fstar::before(
+    r#"
+let lemma_div_mul_mod (a b: usize)
+    : Lemma
+        (requires b <>. mk_usize 0)
+        (ensures (a /! b) *! b +! (a %! b) =. a)
+    = ()
+"#
+)]
+// TODO: Should not be needed. Use hax_lib::fstar::options("")
+#[hax_lib::fstar::before(
+    r#"
+#push-options "--split_queries always --z3rlimit 300"
+"#
+)]
+
 /// The internal keccak state that can also buffer inputs to absorb.
 /// This is used in the general xof APIs.
+#[hax_lib::attributes]
 pub(crate) struct KeccakXofState<
     const PARALLEL_LANES: usize,
     const RATE: usize,
@@ -22,7 +63,19 @@ pub(crate) struct KeccakXofState<
     sponge: bool,
 }
 
+#[cfg(hax)]
+pub(crate) fn keccak_xof_state_inv<
+    const PARALLEL_LANES: usize,
+    const RATE: usize,
+    STATE: KeccakItem<PARALLEL_LANES>,
+>(
+    xof: &KeccakXofState<PARALLEL_LANES, RATE, STATE>,
+) -> bool {
+    RATE != 0 && RATE <= 200 && RATE % 8 == 0 && xof.buf_len <= RATE
+}
+
 #[hax_lib::attributes]
+#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] // TODO: Has no effect
 impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_LANES>>
     KeccakXofState<PARALLEL_LANES, RATE, STATE>
 {
@@ -32,6 +85,15 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
     }
 
     /// Generate a new keccak xof state.
+    #[hax_lib::requires(
+        PARALLEL_LANES == 1 && // TODO: Generalize for the parallel case
+        RATE != 0 &&
+        RATE <= 200 &&
+        RATE % 8 == 0
+    )]
+    #[hax_lib::ensures(|result|
+        keccak_xof_state_inv(&result)
+    )]
     pub(crate) fn new() -> Self {
         Self {
             inner: KeccakState::new(),
@@ -41,51 +103,82 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         }
     }
 
-    /// Absorb
-    ///
-    /// This function takes any number of bytes to absorb and buffers if it's not enough.
-    /// The function assumes that all input slices in `inputs` have the same length.
+    /// Try to complete the internal partial buffer by consuming the minimum required
+    /// number of bytes from the provided `inputs` so that `self.buf` becomes exactly
+    /// one full block of size `RATE`.
     ///
-    /// Only a multiple of `RATE` blocks are absorbed.
-    /// For the remaining bytes [`absorb_final`] needs to be called.
+    /// Behaviour:
+    /// - If `self.buf_len` is 0 (no buffered bytes) or already equal to `RATE`
+    ///   (already a full block), or if the combined available bytes in `inputs` are
+    ///   not enough to reach `RATE`, the function does nothing and returns 0.
+    /// - If `0 < self.buf_len < RATE` and `inputs[..]` contain at least
+    ///   `RATE - self.buf_len` bytes, the function copies exactly
+    ///   `consumed = RATE - self.buf_len` bytes from each lane `inputs[i]` into
+    ///   `self.buf[i]` starting at the current `self.buf_len` offset, sets
+    ///   `self.buf_len = RATE`, and returns `consumed`.
     ///
-    /// This works best with relatively small `inputs`.
-    #[inline(always)]
-    pub(crate) fn absorb(&mut self, inputs: &[&[u8]; PARALLEL_LANES])
-    where
-        KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
-    {
-        let input_remainder_len = self.absorb_full(inputs);
+    /// Returns the `consumed` bytes from `inputs` if there's enough buffered
+    /// content to consume, and `0` otherwise.
+    /// 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::fstar::options("--fuel 5")]
+    #[hax_lib::requires(
+        PARALLEL_LANES == 1 &&
+        keccak_xof_state_inv(self)
+    )]
+    #[hax_lib::ensures(|consumed|
+        keccak_xof_state_inv(future(self)) &&
+        if consumed == 0 {
+            future(self).buf_len == self.buf_len && (
+                self.buf_len == 0 ||
+                self.buf_len == RATE ||
+                self.buf_len.to_int() + inputs[0].len().to_int() < RATE.to_int()
+            )
+        } else {
+            future(self).buf_len == RATE &&
+            consumed == RATE - self.buf_len
+        }
+    )]
+    pub(crate) fn fill_buffer(&mut self, inputs: &[&[u8]; PARALLEL_LANES]) -> usize {
+        let input_len = inputs[0].len();
 
-        // ... buffer the rest if there's not enough input (left).
-        if input_remainder_len > 0 {
-            #[cfg(not(eurydice))]
-            debug_assert!(
-                self.buf_len == 0  // We consumed everything (or it was empty all along).
-                 || self.buf_len + input_remainder_len <= RATE
-            );
+        // Check if we have enough data when combining the internal buffer and the input.
+        if self.buf_len != 0 && self.buf_len != RATE && input_len >= RATE - self.buf_len {
+            let consumed = RATE - self.buf_len;
 
-            let input_len = inputs[0].len();
+            #[cfg(hax)]
+            let self_buf_len = self.buf_len; // ghost variable for F* proof
 
             #[allow(clippy::needless_range_loop)]
             for i in 0..PARALLEL_LANES {
-                self.buf[i][self.buf_len..self.buf_len + input_remainder_len]
-                    .copy_from_slice(&inputs[i][input_len - input_remainder_len..]);
+                hax_lib::loop_invariant!(|_: usize| { self.buf_len == self_buf_len });
+                self.buf[i][self.buf_len..].copy_from_slice(&inputs[i][..consumed]);
             }
-            self.buf_len += input_remainder_len;
+
+            self.buf_len = RATE;
+            consumed
+        } else {
+            0
         }
     }
 
     // Note: consciously not inlining this function to avoid using too much stack
+    #[hax_lib::requires(
+        PARALLEL_LANES == 1 &&
+        keccak_xof_state_inv(self)
+    )]
+    #[hax_lib::ensures(|remainder|
+        keccak_xof_state_inv(future(self)) &&
+        future(self).buf_len.to_int() + remainder.to_int() <= RATE.to_int()
+    )]
     pub(crate) fn absorb_full(&mut self, inputs: &[&[u8]; PARALLEL_LANES]) -> usize
     where
         KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
     {
-        #[cfg(not(eurydice))]
         debug_assert!(PARALLEL_LANES > 0);
-        #[cfg(not(eurydice))]
-        debug_assert!(self.buf_len < RATE);
-        #[cfg(all(debug_assertions, not(hax), not(eurydice)))]
+        debug_assert!(self.buf_len <= RATE);
+        #[cfg(all(debug_assertions, not(hax)))]
         {
             for block in inputs {
                 debug_assert!(block.len() == inputs[0].len());
@@ -95,7 +188,16 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         // Check if there are buffered bytes to absorb first and consume them.
         let input_consumed = self.fill_buffer(inputs);
 
-        if input_consumed > 0 {
+        // We only need to consume the rest of the input.
+        let input_to_consume = inputs[0].len() - input_consumed;
+
+        // Consume the (rest of the) input ...
+        let num_blocks = input_to_consume / RATE;
+        let remainder = input_to_consume % RATE;
+
+        if input_consumed > 0 || self.buf_len == RATE {
+            // We have a full block in the local buffer now.
+            // Convert self.buf to the right type for load_block
             let borrowed: [&[u8]; PARALLEL_LANES] =
                 core::array::from_fn(|i| self.buf[i].as_slice());
 
@@ -106,48 +208,80 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             self.buf_len = 0;
         }
 
-        // We only need to consume the rest of the input.
-        let input_to_consume = inputs[0].len() - input_consumed;
+        #[cfg(hax)]
+        let self_buf_len = self.buf_len;
+
+        #[cfg(hax)]
+        let end = input_consumed + num_blocks * RATE;
+
+        #[cfg(hax)]
+        hax_lib::assert!(end <= inputs[0].len());
 
-        // Consume the (rest of the) input ...
-        let num_blocks = input_to_consume / RATE;
-        let remainder = input_to_consume % RATE;
         for i in 0..num_blocks {
-            // We only get in here if `input_len / RATE > 0`.
-            self.inner
-                .load_block::<RATE>(inputs, input_consumed + i * RATE);
+            hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
+
+            hax_lib::fstar!("lemma_offset_plus_rate_le_total (v input_consumed) (v i) (v num_blocks) (v v_RATE)");
+            let start = i * RATE + input_consumed;
+
+            // TODO: The cfg should not be needed here
+            #[cfg(hax)]
+            hax_lib::assert!(start + RATE <= end);
+
+            self.inner.load_block::<RATE>(inputs, start);
             self.inner.keccakf1600();
         }
 
         remainder
     }
 
-    /// Consume the internal buffer and the required amount of the input to pad to
-    /// `RATE`.
+    /// Absorb
     ///
-    /// Returns the `consumed` bytes from `inputs` if there's enough buffered
-    /// content to consume, and `0` otherwise.
-    /// 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
-    pub(crate) fn fill_buffer(&mut self, inputs: &[&[u8]; PARALLEL_LANES]) -> usize {
-        let input_len = inputs[0].len();
-        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;
+    /// This function takes any number of bytes to absorb and buffers if it's not enough.
+    /// The function assumes that all input slices in `inputs` have the same length.
+    ///
+    /// Only a multiple of `RATE` blocks are absorbed.
+    /// For the remaining bytes [`absorb_final`] needs to be called.
+    ///
+    /// This works best with relatively small `inputs`.
+    #[inline(always)]
+    #[hax_lib::requires(
+        PARALLEL_LANES == 1 &&
+        keccak_xof_state_inv(self)
+    )]
+    #[hax_lib::ensures(|_|
+        keccak_xof_state_inv(future(self))
+    )]
+    pub(crate) fn absorb(&mut self, inputs: &[&[u8]; PARALLEL_LANES])
+    where
+        KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
+    {
+        let input_remainder_len = self.absorb_full(inputs);
+
+        // ... buffer the rest if there's not enough input (left).
+        if input_remainder_len > 0 {
+            #[cfg(not(eurydice))]
+            debug_assert!(
+                // self.buf_len == 0 || // We consumed everything (or it was empty all along).
+                self.buf_len + input_remainder_len <= RATE
+            );
+
+            hax_lib::assert!(input_remainder_len.to_int() + self.buf_len.to_int() <= RATE.to_int());
+
+            let input_len = inputs[0].len();
+
+            #[cfg(hax)]
+            let self_buf_len = self.buf_len;
+
+            #[allow(clippy::needless_range_loop)]
+            for i in 0..PARALLEL_LANES {
+                hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
+
+                self.buf[i][self.buf_len..self.buf_len + input_remainder_len]
+                    .copy_from_slice(&inputs[i][input_len - input_remainder_len..input_len]);
             }
+
+            self.buf_len += input_remainder_len;
         }
-        consumed
     }
 
     /// Absorb a final block.
@@ -155,18 +289,20 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
     /// The `inputs` block may be empty. Everything in the `inputs` block beyond
     /// `RATE` bytes is ignored.
     #[inline(always)]
+    #[hax_lib::requires(
+        PARALLEL_LANES == 1 &&
+        keccak_xof_state_inv(self)
+    )]
+    #[hax_lib::ensures(|_|
+        keccak_xof_state_inv(future(self))
+    )]
     pub(crate) fn absorb_final<const DELIMITER: u8>(&mut self, inputs: &[&[u8]; PARALLEL_LANES])
     where
         KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
     {
         self.absorb(inputs);
 
-        let mut borrowed = [[0u8; RATE].as_slice(); PARALLEL_LANES];
-
-        #[allow(clippy::needless_range_loop)]
-        for i in 0..PARALLEL_LANES {
-            borrowed[i] = &self.buf[i];
-        }
+        let borrowed: [&[u8]; PARALLEL_LANES] = core::array::from_fn(|i| &self.buf[i][..]);
 
         self.inner
             .load_last::<RATE, DELIMITER>(&borrowed, 0, self.buf_len);
@@ -177,12 +313,18 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
 /// Squeeze we only implement for N = 1 right now.
 /// This is because it's not needed for N > 1 right now, but also because hax
 /// can't handle the required mutability for it.
+#[hax_lib::attributes]
 impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
     /// Squeeze `N` x `LEN` bytes. Only `N = 1` for now.
     #[inline(always)]
+    #[hax_lib::requires(keccak_xof_state_inv(self))]
+    #[hax_lib::ensures(|_|
+        keccak_xof_state_inv(future(self)) &&
+        future(out).len() == out.len()
+    )]
     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.
@@ -200,16 +342,33 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
                 // How many blocks do we need to squeeze out?
                 let blocks = out_len / RATE;
 
+                #[cfg(hax)]
+                let self_buf_len = self.buf_len;
+
                 for i in 0..blocks {
+                    hax_lib::loop_invariant!(
+                        |_: usize| out.len() == out_len && self_buf_len == self.buf_len
+                    );
+                    hax_lib::fstar!("assert (v i * v v_RATE <= v out_len)");
+
+                    #[cfg(hax)]
+                    hax_lib::assert!(i.to_int() * RATE.to_int() <= out.len().to_int());
+
                     // Here we know that we always have full blocks to write out.
                     self.inner.keccakf1600();
                     self.inner.squeeze::<RATE>(out, i * RATE, RATE);
                 }
 
+                // For a and b with b < a
+                // (a / b) * b + a % b = a
+
                 let remaining = out_len % RATE;
                 if remaining > 0 {
                     // Squeeze out the last partial block
                     self.inner.keccakf1600();
+
+                    hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
+                    hax_lib::fstar!("assert (v blocks * v v_RATE + v remaining == v out_len)");
                     self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
                 }
             }
diff --git a/libcrux-sha3/src/lib.rs b/libcrux-sha3/src/lib.rs
index 0bfeee313..69e1cb59b 100644
--- a/libcrux-sha3/src/lib.rs
+++ b/libcrux-sha3/src/lib.rs
@@ -15,6 +15,9 @@ mod impl_digest_trait;
 #[cfg(not(any(hax, eurydice)))]
 pub use impl_digest_trait::*;
 
+#[cfg(hax)]
+use hax_lib::int::*;
+
 mod traits;
 
 /// Size in bytes of a SHA3 244 digest.
@@ -43,16 +46,18 @@ pub enum Algorithm {
     Sha512 = 4,
 }
 
+// TODO: Verification fails because of the panic
+#[hax_lib::fstar::replace("")]
 #[hax_lib::attributes]
 impl From<u32> for Algorithm {
-    #[hax_lib::requires(v <= 4)]
+    #[hax_lib::requires(v == 1 || v == 2 || v == 3 || v == 4)]
     fn from(v: u32) -> Algorithm {
         match v {
             1 => Algorithm::Sha224,
             2 => Algorithm::Sha256,
             3 => Algorithm::Sha384,
             4 => Algorithm::Sha512,
-            _ => panic!(),
+            _ => panic!("Invalid SHA3 Algorithm code"),
         }
     }
 }
@@ -79,6 +84,8 @@ pub const fn digest_size(mode: Algorithm) -> usize {
 }
 
 /// SHA3
+#[hax_lib::fstar::options("--split_queries always")]
+#[hax_lib::requires(payload.len().to_int() <= u32::MAX.to_int())]
 pub fn hash<const LEN: usize>(algorithm: Algorithm, payload: &[u8]) -> [u8; LEN] {
     #[cfg(not(eurydice))]
     debug_assert!(payload.len() <= u32::MAX as usize);
@@ -98,6 +105,10 @@ pub use hash as sha3;
 
 /// SHA3 224
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    data.len().to_int() <= u32::MAX.to_int()
+)]
+#[inline(always)]
 pub fn sha224(data: &[u8]) -> [u8; SHA3_224_DIGEST_SIZE] {
     let mut out = [0u8; 28];
     sha224_ema(&mut out, data);
@@ -109,6 +120,11 @@ pub fn sha224(data: &[u8]) -> [u8; SHA3_224_DIGEST_SIZE] {
 /// Preconditions:
 /// - `digest.len() == 28`
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    payload.len().to_int() <= u32::MAX.to_int() &&
+    digest.len().to_int() == int!(28)
+)]
+#[inline(always)]
 pub fn sha224_ema(digest: &mut [u8], payload: &[u8]) {
     debug_assert!(payload.len() <= u32::MAX as usize);
     debug_assert!(digest.len() == 28);
@@ -118,6 +134,10 @@ pub fn sha224_ema(digest: &mut [u8], payload: &[u8]) {
 
 /// SHA3 256
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    data.len().to_int() <= u32::MAX.to_int()
+)]
+#[inline(always)]
 pub fn sha256(data: &[u8]) -> [u8; SHA3_256_DIGEST_SIZE] {
     let mut out = [0u8; 32];
     sha256_ema(&mut out, data);
@@ -126,6 +146,11 @@ pub fn sha256(data: &[u8]) -> [u8; SHA3_256_DIGEST_SIZE] {
 
 /// SHA3 256
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    payload.len().to_int() <= u32::MAX.to_int() &&
+    digest.len().to_int() == int!(32)
+)]
+#[inline(always)]
 pub fn sha256_ema(digest: &mut [u8], payload: &[u8]) {
     debug_assert!(payload.len() <= u32::MAX as usize);
     debug_assert!(digest.len() == 32);
@@ -135,6 +160,10 @@ pub fn sha256_ema(digest: &mut [u8], payload: &[u8]) {
 
 /// SHA3 384
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    data.len().to_int() <= u32::MAX.to_int()
+)]
+#[inline(always)]
 pub fn sha384(data: &[u8]) -> [u8; SHA3_384_DIGEST_SIZE] {
     let mut out = [0u8; 48];
     sha384_ema(&mut out, data);
@@ -143,6 +172,11 @@ pub fn sha384(data: &[u8]) -> [u8; SHA3_384_DIGEST_SIZE] {
 
 /// SHA3 384
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    payload.len().to_int() <= u32::MAX.to_int() &&
+    digest.len().to_int() == int!(48)
+)]
+#[inline(always)]
 pub fn sha384_ema(digest: &mut [u8], payload: &[u8]) {
     debug_assert!(payload.len() <= u32::MAX as usize);
     debug_assert!(digest.len() == 48);
@@ -152,6 +186,10 @@ pub fn sha384_ema(digest: &mut [u8], payload: &[u8]) {
 
 /// SHA3 512
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    data.len().to_int() <= u32::MAX.to_int()
+)]
+#[inline(always)]
 pub fn sha512(data: &[u8]) -> [u8; SHA3_512_DIGEST_SIZE] {
     let mut out = [0u8; 64];
     sha512_ema(&mut out, data);
@@ -160,6 +198,11 @@ pub fn sha512(data: &[u8]) -> [u8; SHA3_512_DIGEST_SIZE] {
 
 /// SHA3 512
 #[cfg_attr(not(eurydice), inline(always))]
+#[hax_lib::requires(
+    payload.len().to_int() <= u32::MAX.to_int() &&
+    digest.len().to_int() == int!(64)
+)]
+#[inline(always)]
 pub fn sha512_ema(digest: &mut [u8], payload: &[u8]) {
     debug_assert!(payload.len() <= u32::MAX as usize);
     debug_assert!(digest.len() == 64);
diff --git a/libcrux-sha3/src/portable.rs b/libcrux-sha3/src/portable.rs
index 99fbc0820..4685570f1 100644
--- a/libcrux-sha3/src/portable.rs
+++ b/libcrux-sha3/src/portable.rs
@@ -1,11 +1,13 @@
 use crate::generic_keccak::{self, portable::keccak1};
 use hax_lib;
 
+#[cfg(hax)]
+use hax_lib::int::*;
+
 use generic_keccak::KeccakState as GenericState;
 
 /// The Keccak state for the incremental API.
 #[derive(Clone, Copy)]
-#[hax_lib::fstar::before(interface, "open Libcrux_sha3.Simd.Portable")]
 pub struct KeccakState {
     state: GenericState<1, u64>,
 }
@@ -49,6 +51,10 @@ pub fn shake256(digest: &mut [u8], data: &[u8]) {
 /// An incremental API for SHAKE
 pub mod incremental {
     use generic_keccak::xof::KeccakXofState;
+
+    #[cfg(hax)]
+    use generic_keccak::xof::keccak_xof_state_inv;
+
     mod private {
         pub trait Sealed {}
 
@@ -94,30 +100,57 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
         fn squeeze(&mut self, out: &mut [u8]);
     }
 
+    #[hax_lib::attributes]
     impl Xof<168> for Shake128Xof {
+        #[hax_lib::ensures(|result|
+            keccak_xof_state_inv(&result.state)
+        )]
         fn new() -> Self {
             Self {
                 state: KeccakXofState::<1, 168, u64>::new(),
             }
         }
 
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&future(self).state)
+        )]
         fn absorb(&mut self, input: &[u8]) {
             self.state.absorb(&[input]);
         }
 
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&future(self).state)
+        )]
         fn absorb_final(&mut self, input: &[u8]) {
             self.state.absorb_final::<0x1fu8>(&[input]);
         }
 
         /// Shake128 squeeze
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&self.state) &&
+            future(out).len() == out.len()
+        )]
         fn squeeze(&mut self, out: &mut [u8]) {
             self.state.squeeze(out);
         }
     }
 
     /// Shake256 XOF in absorb state
+    #[hax_lib::attributes]
     impl Xof<136> for Shake256Xof {
         /// Shake256 new state
+        #[hax_lib::ensures(|result|
+            keccak_xof_state_inv(&result.state)
+        )]
         fn new() -> Self {
             Self {
                 state: KeccakXofState::<1, 136, u64>::new(),
@@ -125,16 +158,35 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
         }
 
         /// Shake256 absorb
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&future(self).state)
+        )]
         fn absorb(&mut self, input: &[u8]) {
             self.state.absorb(&[input]);
         }
 
         /// Shake256 absorb final
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&future(self).state)
+        )]
         fn absorb_final(&mut self, input: &[u8]) {
             self.state.absorb_final::<0x1fu8>(&[input]);
         }
 
         /// Shake256 squeeze
+        #[hax_lib::requires(
+            keccak_xof_state_inv(&self.state)
+        )]
+        #[hax_lib::ensures(|_|
+            keccak_xof_state_inv(&self.state) &&
+            future(out).len() == out.len()
+        )]
         fn squeeze(&mut self, out: &mut [u8]) {
             self.state.squeeze(out);
         }
@@ -150,6 +202,9 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
 
     /// Absorb
     #[inline(always)]
+    #[hax_lib::requires(
+        data0.len().to_int() < hax_lib::int!(168)
+    )]
     pub fn shake128_absorb_final(s: &mut KeccakState, data0: &[u8]) {
         s.state
             .absorb_final::<168, 0x1fu8>(&[data0], 0, data0.len());
@@ -157,18 +212,36 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
 
     /// Squeeze three blocks
     #[inline(always)]
+    #[hax_lib::requires(
+        out0.len().to_int() >= hax_lib::int!(504) // 3 * 168 = 504
+    )]
+    #[hax_lib::ensures(
+        |_| future(out0).len() == out0.len()
+    )]
     pub fn shake128_squeeze_first_three_blocks(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_first_three_blocks::<168>(out0);
     }
 
     /// Squeeze five blocks
     #[inline(always)]
+    #[hax_lib::requires(
+        out0.len().to_int() >= hax_lib::int!(840) // 5 * 168 = 840
+    )]
+    #[hax_lib::ensures(
+        |_| future(out0).len() == out0.len()
+    )]
     pub fn shake128_squeeze_first_five_blocks(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_first_five_blocks::<168>(out0);
     }
 
     /// Squeeze another block
     #[inline(always)]
+    #[hax_lib::requires(
+        out0.len().to_int() >= hax_lib::int!(168)
+    )]
+    #[hax_lib::ensures(
+        |_| future(out0).len() == out0.len()
+    )]
     pub fn shake128_squeeze_next_block(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_next_block::<168>(out0, 0)
     }
@@ -183,18 +256,33 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
 
     /// Absorb some data for SHAKE-256 for the last time
     #[inline(always)]
+    #[hax_lib::requires(
+        data.len().to_int() < hax_lib::int!(136)
+    )]
     pub fn shake256_absorb_final(s: &mut KeccakState, data: &[u8]) {
         s.state.absorb_final::<136, 0x1fu8>(&[data], 0, data.len());
     }
 
     /// Squeeze the first SHAKE-256 block
     #[inline(always)]
+    #[hax_lib::requires(
+        out.len().to_int() >= hax_lib::int!(136)
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub fn shake256_squeeze_first_block(s: &mut KeccakState, out: &mut [u8]) {
         s.state.squeeze_first_block::<136>(out);
     }
 
     /// Squeeze the next SHAKE-256 block
     #[inline(always)]
+    #[hax_lib::requires(
+        out.len().to_int() >= hax_lib::int!(136)
+    )]
+    #[hax_lib::ensures(
+        |_| future(out).len() == out.len()
+    )]
     pub fn shake256_squeeze_next_block(s: &mut KeccakState, out: &mut [u8]) {
         s.state.squeeze_next_block::<136>(out, 0);
     }
diff --git a/libcrux-sha3/src/simd/portable.rs b/libcrux-sha3/src/simd/portable.rs
index 127aca78f..ba8c287d0 100644
--- a/libcrux-sha3/src/simd/portable.rs
+++ b/libcrux-sha3/src/simd/portable.rs
@@ -1,8 +1,15 @@
 //! A portable SHA3 implementation using the generic implementation.
 
+#[cfg(hax)]
+use hax_lib::int::*;
+
 use crate::{generic_keccak::KeccakState, traits::*};
 
 #[inline(always)]
+#[hax_lib::requires(
+    LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
+    RIGHT >= 0
+)]
 fn rotate_left<const LEFT: i32, const RIGHT: i32>(x: u64) -> u64 {
     #[cfg(not(eurydice))]
     debug_assert!(LEFT + RIGHT == 64);
@@ -20,6 +27,10 @@ fn _vrax1q_u64(a: u64, b: u64) -> u64 {
 }
 
 #[inline(always)]
+#[hax_lib::requires(
+    LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
+    RIGHT >= 0
+)]
 fn _vxarq_u64<const LEFT: i32, const RIGHT: i32>(a: u64, b: u64) -> u64 {
     rotate_left::<LEFT, RIGHT>(a ^ b)
 }
@@ -35,9 +46,17 @@ fn _veorq_n_u64(a: u64, c: u64) -> u64 {
 }
 
 #[inline(always)]
+#[hax_lib::requires(
+    RATE <= 200 &&
+    RATE % 8 == 0 &&
+    start.to_int() + RATE.to_int() <= blocks.len().to_int()
+)]
 pub(crate) fn load_block<const RATE: usize>(state: &mut [u64; 25], blocks: &[u8], start: usize) {
     #[cfg(not(eurydice))]
-    debug_assert!(start + RATE <= blocks.len() && RATE % 8 == 0);
+    {
+        debug_assert!(start + RATE <= blocks.len());
+        debug_assert!(RATE % 8 == 0);
+    }
 
     // First load the block, then xor it with the state
     // Note: combining the two loops below reduces performance for large inputs,
@@ -62,6 +81,12 @@ pub(crate) fn load_block<const RATE: usize>(state: &mut [u64; 25], blocks: &[u8]
 }
 
 #[inline(always)]
+#[hax_lib::requires(
+    RATE <= 200 &&
+    RATE % 8 == 0 &&
+    len < RATE &&
+    start.to_int() + len.to_int() <= blocks.len().to_int()
+)]
 pub(crate) fn load_last<const RATE: usize, const DELIMITER: u8>(
     state: &mut [u64; 25],
     blocks: &[u8],
@@ -80,6 +105,13 @@ pub(crate) fn load_last<const RATE: usize, const DELIMITER: u8>(
 }
 
 #[inline(always)]
+#[hax_lib::requires(
+    len <= 200 &&
+    start.to_int() + len.to_int() <= out.len().to_int()
+)]
+#[hax_lib::ensures(|_|
+    future(out).len() == out.len()
+)]
 pub(crate) fn store_block<const RATE: usize>(
     s: &[u64; 25],
     out: &mut [u8],
@@ -87,18 +119,28 @@ pub(crate) fn store_block<const RATE: usize>(
     len: usize,
 ) {
     let octets = len / 8;
+
+    #[cfg(hax)]
+    let out_len = out.len(); // ghost variable
+
     for i in 0..octets {
-        out[start + 8 * i..start + 8 * i + 8]
-            .copy_from_slice(&get_ij(s, i / 5, i % 5).to_le_bytes());
+        hax_lib::loop_invariant!(|i: usize| out.len() == out_len);
+        let value = get_ij(s, i / 5, i % 5);
+        let bytes = value.to_le_bytes();
+        let out_pos = start + 8 * i;
+        out[out_pos..out_pos + 8].copy_from_slice(&bytes);
     }
 
     let remaining = len % 8;
     if remaining > 0 {
-        out[start + len - remaining..start + len]
-            .copy_from_slice(&get_ij(s, octets / 5, octets % 5).to_le_bytes()[0..remaining]);
+        let value = get_ij(s, octets / 5, octets % 5);
+        let bytes = value.to_le_bytes();
+        let out_pos = start + len - remaining;
+        out[out_pos..out_pos + remaining].copy_from_slice(&bytes[..remaining]);
     }
 }
 
+#[hax_lib::attributes]
 impl KeccakItem<1> for u64 {
     #[inline(always)]
     fn zero() -> Self {
@@ -113,6 +155,10 @@ impl KeccakItem<1> for u64 {
         _vrax1q_u64(a, b)
     }
     #[inline(always)]
+    #[hax_lib::requires(
+        LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
+        RIGHT >= 0
+    )]
     fn xor_and_rotate<const LEFT: i32, const RIGHT: i32>(a: Self, b: Self) -> Self {
         _vxarq_u64::<LEFT, RIGHT>(a, b)
     }
@@ -130,11 +176,23 @@ impl KeccakItem<1> for u64 {
     }
 }
 
+#[hax_lib::attributes]
 impl Absorb<1> for KeccakState<1, u64> {
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        start.to_int() + RATE.to_int() <= input[0].len().to_int()
+    )]
     fn load_block<const RATE: usize>(&mut self, input: &[&[u8]; 1], start: usize) {
         load_block::<RATE>(&mut self.st, input[0], start);
     }
 
+    #[hax_lib::requires(
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        len < RATE &&
+        start.to_int() + len.to_int() <= input[0].len().to_int()
+    )]
     fn load_last<const RATE: usize, const DELIMITER: u8>(
         &mut self,
         input: &[&[u8]; 1],
@@ -145,7 +203,15 @@ impl Absorb<1> for KeccakState<1, u64> {
     }
 }
 
-impl Squeeze1<u64> for KeccakState<1, u64> {
+#[hax_lib::attributes]
+impl Squeeze<u64> for KeccakState<1, u64> {
+    #[hax_lib::requires(
+        len <= 200 &&
+        start.to_int() + len.to_int() <= out.len().to_int()
+    )]
+    #[hax_lib::ensures(|_|
+        future(out).len() == out.len()
+    )]
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize) {
         store_block::<RATE>(&self.st, out, start, len);
     }
diff --git a/libcrux-sha3/src/traits.rs b/libcrux-sha3/src/traits.rs
index 1cf0fc5a3..edd54533b 100644
--- a/libcrux-sha3/src/traits.rs
+++ b/libcrux-sha3/src/traits.rs
@@ -1,5 +1,8 @@
 use hax_lib;
 
+#[cfg(hax)]
+use hax_lib::int::*;
+
 // XXX: These should be default functions on `KeccakItem`, but hax doesn't
 //      support that yet. cryspen/hax#888
 #[hax_lib::requires(i < 5 && j < 5)]
@@ -35,7 +38,10 @@ pub(crate) trait KeccakItem<const N: usize>: Clone + Copy {
     fn rotate_left1_and_xor(a: Self, b: Self) -> Self;
 
     /// `(a ^ b) <<< LEFT`
-    #[hax_lib::requires(true)]
+    #[hax_lib::requires(
+        LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
+        RIGHT >= 0
+    )]
     fn xor_and_rotate<const LEFT: i32, const RIGHT: i32>(a: Self, b: Self) -> Self;
 
     /// `a ^ (b & !c)`
@@ -52,11 +58,25 @@ pub(crate) trait KeccakItem<const N: usize>: Clone + Copy {
 }
 
 /// Trait to load new bytes into the state.
+#[hax_lib::attributes]
 pub(crate) trait Absorb<const N: usize> {
     /// Absorb a block
+    #[hax_lib::requires(
+        N != 0 &&
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        start.to_int() + RATE.to_int() <= input[0].len().to_int()
+    )]
     fn load_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize);
 
     /// Absorb the last block (may be partial)
+    #[hax_lib::requires(
+        N != 0 &&
+        RATE <= 200 &&
+        RATE % 8 == 0 &&
+        len < RATE &&
+        start.to_int() + len.to_int() <= input[0].len().to_int()
+    )]
     fn load_last<const RATE: usize, const DELIMITER: u8>(
         &mut self,
         input: &[&[u8]; N],
@@ -72,19 +92,52 @@ pub(crate) trait Absorb<const N: usize> {
 ///
 /// Store blocks `N = 1`
 #[hax_lib::fstar::replace(
-    interface,
-    "
-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;
+    interface, "
+class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
+  // TODO: This super variable is problematic and makes typecheck fail
+  // [@@@ FStar.Tactics.Typeclasses.no_method]_super_18390613159176269294:t_KeccakItem v_T (mk_usize 1);
+  f_squeeze_pre:v_RATE: usize -> self_: v_Self -> out: t_Slice u8 -> start: usize -> len: usize
+    -> pred:
+      Type0
+        { len <=. mk_usize 200 &&
+          ((Rust_primitives.Hax.Int.from_machine start <: Hax_lib.Int.t_Int) +
+            (Rust_primitives.Hax.Int.from_machine len <: Hax_lib.Int.t_Int)
+            <:
+            Hax_lib.Int.t_Int) <=
+          (Rust_primitives.Hax.Int.from_machine (Core.Slice.impl__len #u8 out <: usize)
+            <:
+            Hax_lib.Int.t_Int) ==>
+          pred };
+  f_squeeze_post:
+      v_RATE: usize ->
+      self_: v_Self ->
+      out: t_Slice u8 ->
+      start: usize ->
+      len: usize ->
+      out_future: t_Slice u8
+    -> pred:
+      Type0
+        { pred ==>
+          (Core.Slice.impl__len #u8 out_future <: usize) =. (Core.Slice.impl__len #u8 out <: usize)
+        };
   f_squeeze:v_RATE: usize -> x0: v_Self -> x1: t_Slice u8 -> x2: usize -> x3: usize
     -> Prims.Pure (t_Slice u8)
         (f_squeeze_pre v_RATE x0 x1 x2 x3)
         (fun result -> f_squeeze_post v_RATE x0 x1 x2 x3 result)
 }
+
+// TODO: See above
+// [@@ FStar.Tactics.Typeclasses.tcinstance]
+// let _ = fun (v_Self:Type0) (v_T:Type0) {|i: t_Squeeze v_Self v_T|} -> i._super_18390613159176269294
 "
 )]
-pub(crate) trait Squeeze1<T: KeccakItem<1>> {
+#[hax_lib::attributes]
+pub(crate) trait Squeeze<T: KeccakItem<1>> {
+    #[hax_lib::requires(
+        len <= 200 &&
+        start.to_int() + len.to_int() <= out.len().to_int()
+    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize);
 }
 

From 5d0e51d768f6004683119073d907b313df94d234 Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Wed, 12 Nov 2025 12:40:48 +0100
Subject: [PATCH 2/6] apply feedback from franziskuskiefer

---
 libcrux-sha3/src/generic_keccak/portable.rs | 21 ++++------
 libcrux-sha3/src/generic_keccak/xof.rs      | 42 ++++----------------
 libcrux-sha3/src/lemmas.rs                  | 44 +++++++++++++++++++++
 libcrux-sha3/src/lib.rs                     | 32 +++++++++------
 4 files changed, 79 insertions(+), 60 deletions(-)
 create mode 100644 libcrux-sha3/src/lemmas.rs

diff --git a/libcrux-sha3/src/generic_keccak/portable.rs b/libcrux-sha3/src/generic_keccak/portable.rs
index eee6341d1..8ed75408b 100644
--- a/libcrux-sha3/src/generic_keccak/portable.rs
+++ b/libcrux-sha3/src/generic_keccak/portable.rs
@@ -1,5 +1,9 @@
 use super::*;
 
+#[cfg(hax)]
+#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
+const _: () = ();
+
 #[hax_lib::attributes]
 impl KeccakState<1, u64> {
     #[inline(always)]
@@ -70,23 +74,10 @@ impl KeccakState<1, u64> {
     }
 }
 
-#[hax_lib::fstar::before(
-    r#"
-let rec mul_succ_le (k n d: nat)
-  : Lemma
-    (requires k < n && d > 0)
-    (ensures k * d + d <= n * d)
-    (decreases n) =
-  if n = 0 then ()
-  else if k = n - 1 then ()
-  else mul_succ_le k (n - 1) d
-"#
-)]
 #[hax_lib::requires(
     RATE != 0 &&
     RATE <= 200 &&
-    RATE % 8 == 0 /* &&
-    data.len() + RATE <= usize::MAX */
+    RATE % 8 == 0
 )]
 #[hax_lib::ensures(|_|
     future(out).len() == out.len())
@@ -98,6 +89,7 @@ pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(data: &[u8], out: &mut
     let data_len = data.len();
     for i in 0..data_len / RATE {
         hax_lib::fstar!("mul_succ_le (v i) (v (data_len /! v_RATE)) (v v_RATE)");
+
         s.absorb_block::<RATE>(&[data], i * RATE);
     }
     let rem = data_len % RATE;
@@ -114,6 +106,7 @@ pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(data: &[u8], out: &mut
         for i in 1..blocks {
             hax_lib::loop_invariant!(|_: usize| out.len() == outlen);
             hax_lib::fstar!("mul_succ_le (v i) (v blocks) (v v_RATE)");
+
             s.keccakf1600();
             s.squeeze::<RATE>(out, i * RATE, RATE);
         }
diff --git a/libcrux-sha3/src/generic_keccak/xof.rs b/libcrux-sha3/src/generic_keccak/xof.rs
index d5ef61e93..1f630613c 100644
--- a/libcrux-sha3/src/generic_keccak/xof.rs
+++ b/libcrux-sha3/src/generic_keccak/xof.rs
@@ -5,37 +5,10 @@ use crate::{
     traits::{Absorb, KeccakItem, Squeeze},
 };
 
-// Helper lemma for F* verification in the `absorb_full` loop.
-//
-// Proves that for any a, i, n, rate > 0 with i < n,
-// we have a + i * rate + rate ≤ a + n * rate,
-// i.e. each block‐offset stays within the total input length.
-#[hax_lib::fstar::before(
-    r#"
-let rec lemma_offset_plus_rate_le_total (a i n rate: nat)
-    : Lemma
-        (requires i < n && rate > 0)
-        (ensures a + i * rate + rate <= a + n * rate)
-        (decreases n) =
-    if n = 0 then ()
-    else if i = n - 1 then ()
-    else lemma_offset_plus_rate_le_total a i (n - 1) rate
-"#
-)]
-// Helper lemma for F* verification in the 'squeeze' function.
-//
-// Proves the division‐multiplication‐modulo identity:
-//   for any a, b with b != 0,
-//   (a / b) * b + (a % b) = a.
-#[hax_lib::fstar::before(
-    r#"
-let lemma_div_mul_mod (a b: usize)
-    : Lemma
-        (requires b <>. mk_usize 0)
-        (ensures (a /! b) *! b +! (a %! b) =. a)
-    = ()
-"#
-)]
+#[cfg(hax)]
+#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
+const _: () = ();
+
 // TODO: Should not be needed. Use hax_lib::fstar::options("")
 #[hax_lib::fstar::before(
     r#"
@@ -153,6 +126,7 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             #[allow(clippy::needless_range_loop)]
             for i in 0..PARALLEL_LANES {
                 hax_lib::loop_invariant!(|_: usize| { self.buf_len == self_buf_len });
+
                 self.buf[i][self.buf_len..].copy_from_slice(&inputs[i][..consumed]);
             }
 
@@ -219,11 +193,10 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
 
         for i in 0..num_blocks {
             hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
+            hax_lib::fstar!("mul_succ_le (v i) (v num_blocks) (v v_RATE)");
 
-            hax_lib::fstar!("lemma_offset_plus_rate_le_total (v input_consumed) (v i) (v num_blocks) (v v_RATE)");
             let start = i * RATE + input_consumed;
 
-            // TODO: The cfg should not be needed here
             #[cfg(hax)]
             hax_lib::assert!(start + RATE <= end);
 
@@ -261,7 +234,7 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         if input_remainder_len > 0 {
             #[cfg(not(eurydice))]
             debug_assert!(
-                // self.buf_len == 0 || // We consumed everything (or it was empty all along).
+                self.buf_len == 0 || // We consumed everything (or it was empty all along).
                 self.buf_len + input_remainder_len <= RATE
             );
 
@@ -369,6 +342,7 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
 
                     hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
                     hax_lib::fstar!("assert (v blocks * v v_RATE + v remaining == v out_len)");
+
                     self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
                 }
             }
diff --git a/libcrux-sha3/src/lemmas.rs b/libcrux-sha3/src/lemmas.rs
new file mode 100644
index 000000000..28dc28096
--- /dev/null
+++ b/libcrux-sha3/src/lemmas.rs
@@ -0,0 +1,44 @@
+//! F* verification lemmas for SHA3/Keccak implementation.
+//!
+//! This module contains lemmas used for F* verification across
+//! the libcrux-sha3 crate. These lemmas are only used during
+//! formal verification with hax and F*, and have no runtime behavior.
+
+/// Lemma proving the division-multiplication-modulo identity.
+///
+/// For any `a`, `b` with `b != 0`,
+/// proves that `(a / b) * b + (a % b) = a`.
+///
+/// This is used in the `squeeze` function to verify correct buffer indexing
+/// when squeezing multiple blocks.
+#[hax_lib::fstar::replace(
+    r#"
+let lemma_div_mul_mod (a b: usize)
+    : Lemma
+        (requires b <>. mk_usize 0)
+        (ensures (a /! b) *! b +! (a %! b) =. a)
+    = ()
+"#
+)]
+const _LEMMA_DIV_MUL_MOD: () = ();
+
+/// Lemma proving multiplication bounds for successive elements.
+///
+/// For any `k < n`,
+/// proves that `k * d + d ≤ n * d`.
+///
+/// This is used in the `keccak` functions to verify that block iterations
+/// stay within bounds.
+#[hax_lib::fstar::replace(
+    r#"
+let rec mul_succ_le (k n d: nat)
+  : Lemma
+    (requires k < n)
+    (ensures k * d + d <= n * d)
+    (decreases n) =
+  if n = 0 then ()
+  else if k = n - 1 then ()
+  else mul_succ_le k (n - 1) d
+"#
+)]
+const _LEMMA_MUL_SUCC_LE: () = ();
diff --git a/libcrux-sha3/src/lib.rs b/libcrux-sha3/src/lib.rs
index 69e1cb59b..7b98e8423 100644
--- a/libcrux-sha3/src/lib.rs
+++ b/libcrux-sha3/src/lib.rs
@@ -12,6 +12,7 @@ mod generic_keccak;
 
 #[cfg(not(any(hax, eurydice)))]
 mod impl_digest_trait;
+use cavp::Sha3;
 #[cfg(not(any(hax, eurydice)))]
 pub use impl_digest_trait::*;
 
@@ -20,14 +21,21 @@ use hax_lib::int::*;
 
 mod traits;
 
-/// Size in bytes of a SHA3 244 digest.
-pub const SHA3_224_DIGEST_SIZE: usize = 28;
-/// Size in bytes of a SHA3 256 digest.
-pub const SHA3_256_DIGEST_SIZE: usize = 32;
-/// Size in bytes of a SHA3 2384 digest.
-pub const SHA3_384_DIGEST_SIZE: usize = 48;
-/// Size in bytes of a SHA3 512 digest.
-pub const SHA3_512_DIGEST_SIZE: usize = 64;
+/// F* verification lemmas
+#[cfg(hax)]
+pub(crate) mod lemmas;
+
+/// A SHA3 224 Digest
+pub type Sha3_224Digest = [u8; 28];
+
+/// A SHA3 256 Digest
+pub type Sha3_256Digest = [u8; 32];
+
+/// A SHA3 384 Digest
+pub type Sha3_384Digest = [u8; 48];
+
+/// A SHA3 512 Digest
+pub type Sha3_512Digest = [u8; 64];
 
 /// The Digest Algorithm.
 #[cfg_attr(not(eurydice), derive(Clone, Copy, Debug, PartialEq))]
@@ -109,7 +117,7 @@ pub use hash as sha3;
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha224(data: &[u8]) -> [u8; SHA3_224_DIGEST_SIZE] {
+pub fn sha224(data: &[u8]) -> Sha3_224Digest {
     let mut out = [0u8; 28];
     sha224_ema(&mut out, data);
     out
@@ -138,7 +146,7 @@ pub fn sha224_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha256(data: &[u8]) -> [u8; SHA3_256_DIGEST_SIZE] {
+pub fn sha256(data: &[u8]) -> Sha3_256Digest {
     let mut out = [0u8; 32];
     sha256_ema(&mut out, data);
     out
@@ -164,7 +172,7 @@ pub fn sha256_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha384(data: &[u8]) -> [u8; SHA3_384_DIGEST_SIZE] {
+pub fn sha384(data: &[u8]) -> Sha3_384Digest {
     let mut out = [0u8; 48];
     sha384_ema(&mut out, data);
     out
@@ -190,7 +198,7 @@ pub fn sha384_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha512(data: &[u8]) -> [u8; SHA3_512_DIGEST_SIZE] {
+pub fn sha512(data: &[u8]) -> Sha3_512Digest {
     let mut out = [0u8; 64];
     sha512_ema(&mut out, data);
     out

From e5a2098c937b728670acbb9357e29b9615bdca96 Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Wed, 12 Nov 2025 13:05:12 +0100
Subject: [PATCH 3/6] light refactor and correct trait preconditions

---
 libcrux-sha3/src/generic_keccak.rs          | 42 +++++++++----
 libcrux-sha3/src/generic_keccak/portable.rs | 68 ++++++++++-----------
 libcrux-sha3/src/generic_keccak/xof.rs      | 57 +++++++++--------
 libcrux-sha3/src/lib.rs                     | 11 ++--
 libcrux-sha3/src/portable.rs                | 68 ++++++---------------
 libcrux-sha3/src/simd/portable.rs           |  9 +--
 libcrux-sha3/src/traits.rs                  | 24 +++++++-
 7 files changed, 136 insertions(+), 143 deletions(-)

diff --git a/libcrux-sha3/src/generic_keccak.rs b/libcrux-sha3/src/generic_keccak.rs
index 70587c9db..b3d9dac50 100644
--- a/libcrux-sha3/src/generic_keccak.rs
+++ b/libcrux-sha3/src/generic_keccak.rs
@@ -6,7 +6,7 @@ use core::ops::Index;
 use crate::traits::*;
 
 #[cfg(hax)]
-use hax_lib::int::*;
+use hax_lib::{constructors::from_bool, forall, implies, int::ToInt};
 
 /// A generic Xof API.
 pub(crate) mod xof;
@@ -243,33 +243,53 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
 
     #[inline(always)]
     #[hax_lib::requires(
-        N > 0 &&
+      from_bool(
+        N != 0 &&
         RATE <= 200 &&
         RATE % 8 == 0 &&
-        start.to_int() + RATE.to_int() <= blocks[0].len().to_int()
+        (RATE % 32 == 8 || RATE % 32 == 16) &&
+        start.to_int() + RATE.to_int() <= input[0].len().to_int()
+      ).and(
+        forall(|i: usize|
+          implies(
+            i < N,
+            input[0].len() == input[i].len()
+          )
+        )
+      )
     )]
-    fn absorb_block<const RATE: usize>(&mut self, blocks: &[&[u8]; N], start: usize)
+    fn absorb_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize)
     where
         Self: Absorb<N>,
     {
         #[cfg(not(any(eurydice, hax)))]
-        debug_assert!(blocks.iter().all(|buf| buf.len() == blocks[0].len()));
+        debug_assert!(input.iter().all(|buf| buf.len() == input[0].len()));
 
-        self.load_block::<RATE>(blocks, start);
+        self.load_block::<RATE>(input, start);
         self.keccakf1600()
     }
 
     #[inline(always)]
     #[hax_lib::requires(
-        N > 0 &&
+      from_bool(
+        N != 0 &&
         RATE <= 200 &&
         RATE % 8 == 0 &&
+        (RATE % 32 == 8 || RATE % 32 == 16) &&
         len < RATE &&
-        start.to_int() + len.to_int() <= last[0].len().to_int()
+        start.to_int() + len.to_int() <= input[0].len().to_int()
+      ).and(
+        forall(|i: usize|
+          implies(
+            i < N,
+            input[0].len() == input[i].len()
+          )
+        )
+      )
     )]
     pub(crate) fn absorb_final<const RATE: usize, const DELIM: u8>(
         &mut self,
-        last: &[&[u8]; N],
+        input: &[&[u8]; N],
         start: usize,
         len: usize,
     ) where
@@ -279,9 +299,9 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
         debug_assert!(N > 0 && len < RATE);
 
         #[cfg(not(any(eurydice, hax)))]
-        debug_assert!(last.iter().all(|buf| buf.len() == last[0].len()));
+        debug_assert!(input.iter().all(|buf| buf.len() == input[0].len()));
 
-        self.load_last::<RATE, DELIM>(last, start, len);
+        self.load_last::<RATE, DELIM>(input, start, len);
         self.keccakf1600()
     }
 }
diff --git a/libcrux-sha3/src/generic_keccak/portable.rs b/libcrux-sha3/src/generic_keccak/portable.rs
index 8ed75408b..1a0e5cc44 100644
--- a/libcrux-sha3/src/generic_keccak/portable.rs
+++ b/libcrux-sha3/src/generic_keccak/portable.rs
@@ -11,9 +11,7 @@ impl KeccakState<1, u64> {
         RATE <= 200 &&
         start.to_int() + RATE.to_int() <= out.len().to_int()
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub(crate) fn squeeze_next_block<const RATE: usize>(&mut self, out: &mut [u8], start: usize) {
         self.keccakf1600();
         self.squeeze::<RATE>(out, start, RATE);
@@ -24,9 +22,7 @@ impl KeccakState<1, u64> {
         RATE <= 200 &&
         RATE <= out.len()
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub(crate) fn squeeze_first_block<const RATE: usize>(&self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
     }
@@ -36,9 +32,7 @@ impl KeccakState<1, u64> {
         RATE <= 200 &&
         3 * RATE <= out.len()
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub(crate) fn squeeze_first_three_blocks<const RATE: usize>(&mut self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
 
@@ -54,9 +48,7 @@ impl KeccakState<1, u64> {
         RATE <= 200 &&
         5 * RATE <= out.len()
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub(crate) fn squeeze_first_five_blocks<const RATE: usize>(&mut self, out: &mut [u8]) {
         self.squeeze::<RATE>(out, 0, RATE);
 
@@ -79,40 +71,42 @@ impl KeccakState<1, u64> {
     RATE <= 200 &&
     RATE % 8 == 0
 )]
-#[hax_lib::ensures(|_|
-    future(out).len() == out.len())
-]
-#[hax_lib::fstar::options("--split_queries always --query_stats --z3rlimit 300")]
+#[hax_lib::ensures(|_| future(output).len() == output.len())]
+#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")]
 #[inline]
-pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(data: &[u8], out: &mut [u8]) {
+pub(crate) fn keccak1<const RATE: usize, const DELIM: u8>(input: &[u8], output: &mut [u8]) {
+    // Initialize Keccak state
     let mut s = KeccakState::<1, u64>::new();
-    let data_len = data.len();
-    for i in 0..data_len / RATE {
-        hax_lib::fstar!("mul_succ_le (v i) (v (data_len /! v_RATE)) (v v_RATE)");
 
-        s.absorb_block::<RATE>(&[data], i * RATE);
-    }
-    let rem = data_len % RATE;
-    s.absorb_final::<RATE, DELIM>(&[data], data_len - rem, rem);
-
-    let outlen = out.len();
-    let blocks = outlen / RATE;
-    let last = outlen - (outlen % RATE);
+    // Absorb input
+    let input_len = input.len();
+    let input_blocks = input_len / RATE;
+    let input_rem = input_len % RATE;
+    for i in 0..input_blocks {
+        hax_lib::fstar!("mul_succ_le (v i) (v input_blocks) (v v_RATE)");
 
-    if blocks == 0 {
-        s.squeeze::<RATE>(out, 0, outlen);
+        s.absorb_block::<RATE>(&[input], i * RATE);
+    }
+    s.absorb_final::<RATE, DELIM>(&[input], input_len - input_rem, input_rem);
+
+    // Squeeze output
+    let output_len = output.len();
+    let output_blocks = output_len / RATE;
+    let output_rem = output_len % RATE;
+    if output_blocks == 0 {
+        s.squeeze::<RATE>(output, 0, output_len);
     } else {
-        s.squeeze::<RATE>(out, 0, RATE);
-        for i in 1..blocks {
-            hax_lib::loop_invariant!(|_: usize| out.len() == outlen);
-            hax_lib::fstar!("mul_succ_le (v i) (v blocks) (v v_RATE)");
+        s.squeeze::<RATE>(output, 0, RATE);
+        for i in 1..output_blocks {
+            hax_lib::loop_invariant!(|_: usize| output.len() == output_len);
+            hax_lib::fstar!("mul_succ_le (v i) (v output_blocks) (v v_RATE)");
 
             s.keccakf1600();
-            s.squeeze::<RATE>(out, i * RATE, RATE);
+            s.squeeze::<RATE>(output, i * RATE, RATE);
         }
-        if last < outlen {
+        if output_rem != 0 {
             s.keccakf1600();
-            s.squeeze::<RATE>(out, last, outlen - last);
+            s.squeeze::<RATE>(output, output_len - output_rem, output_rem);
         }
     }
 }
diff --git a/libcrux-sha3/src/generic_keccak/xof.rs b/libcrux-sha3/src/generic_keccak/xof.rs
index 1f630613c..7b07db43a 100644
--- a/libcrux-sha3/src/generic_keccak/xof.rs
+++ b/libcrux-sha3/src/generic_keccak/xof.rs
@@ -44,7 +44,11 @@ pub(crate) fn keccak_xof_state_inv<
 >(
     xof: &KeccakXofState<PARALLEL_LANES, RATE, STATE>,
 ) -> bool {
-    RATE != 0 && RATE <= 200 && RATE % 8 == 0 && xof.buf_len <= RATE
+    RATE != 0
+        && RATE <= 200
+        && RATE % 8 == 0
+        && (RATE % 32 == 8 || RATE % 32 == 16)
+        && xof.buf_len <= RATE
 }
 
 #[hax_lib::attributes]
@@ -64,9 +68,7 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         RATE <= 200 &&
         RATE % 8 == 0
     )]
-    #[hax_lib::ensures(|result|
-        keccak_xof_state_inv(&result)
-    )]
+    #[hax_lib::ensures(|result| keccak_xof_state_inv(&result))]
     pub(crate) fn new() -> Self {
         Self {
             inner: KeccakState::new(),
@@ -117,7 +119,8 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         let input_len = inputs[0].len();
 
         // Check if we have enough data when combining the internal buffer and the input.
-        if self.buf_len != 0 && self.buf_len != RATE && input_len >= RATE - self.buf_len {
+        // If the internal buffer is empty and we have enough to absorb do not use.
+        if self.buf_len != 0 && input_len >= RATE - self.buf_len {
             let consumed = RATE - self.buf_len;
 
             #[cfg(hax)]
@@ -160,16 +163,9 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         }
 
         // Check if there are buffered bytes to absorb first and consume them.
-        let input_consumed = self.fill_buffer(inputs);
-
-        // We only need to consume the rest of the input.
-        let input_to_consume = inputs[0].len() - input_consumed;
+        let consumed = self.fill_buffer(inputs);
 
-        // Consume the (rest of the) input ...
-        let num_blocks = input_to_consume / RATE;
-        let remainder = input_to_consume % RATE;
-
-        if input_consumed > 0 || self.buf_len == RATE {
+        if self.buf_len == RATE {
             // We have a full block in the local buffer now.
             // Convert self.buf to the right type for load_block
             let borrowed: [&[u8]; PARALLEL_LANES] =
@@ -182,11 +178,18 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             self.buf_len = 0;
         }
 
+        // We only need to consume the rest of the input.
+        let input_to_consume = inputs[0].len() - consumed;
+
+        // Consume the (rest of the) input ...
+        let num_blocks = input_to_consume / RATE;
+        let remainder = input_to_consume % RATE;
+
         #[cfg(hax)]
         let self_buf_len = self.buf_len;
 
         #[cfg(hax)]
-        let end = input_consumed + num_blocks * RATE;
+        let end = consumed + num_blocks * RATE;
 
         #[cfg(hax)]
         hax_lib::assert!(end <= inputs[0].len());
@@ -195,7 +198,7 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
             hax_lib::fstar!("mul_succ_le (v i) (v num_blocks) (v v_RATE)");
 
-            let start = i * RATE + input_consumed;
+            let start = i * RATE + consumed;
 
             #[cfg(hax)]
             hax_lib::assert!(start + RATE <= end);
@@ -221,24 +224,22 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         PARALLEL_LANES == 1 &&
         keccak_xof_state_inv(self)
     )]
-    #[hax_lib::ensures(|_|
-        keccak_xof_state_inv(future(self))
-    )]
+    #[hax_lib::ensures(|_| keccak_xof_state_inv(future(self)))]
     pub(crate) fn absorb(&mut self, inputs: &[&[u8]; PARALLEL_LANES])
     where
         KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
     {
-        let input_remainder_len = self.absorb_full(inputs);
+        let remainder = self.absorb_full(inputs);
 
         // ... buffer the rest if there's not enough input (left).
-        if input_remainder_len > 0 {
+        if remainder > 0 {
             #[cfg(not(eurydice))]
             debug_assert!(
                 self.buf_len == 0 || // We consumed everything (or it was empty all along).
-                self.buf_len + input_remainder_len <= RATE
+                self.buf_len + remainder <= RATE
             );
 
-            hax_lib::assert!(input_remainder_len.to_int() + self.buf_len.to_int() <= RATE.to_int());
+            hax_lib::assert!(remainder.to_int() + self.buf_len.to_int() <= RATE.to_int());
 
             let input_len = inputs[0].len();
 
@@ -249,11 +250,11 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             for i in 0..PARALLEL_LANES {
                 hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
 
-                self.buf[i][self.buf_len..self.buf_len + input_remainder_len]
-                    .copy_from_slice(&inputs[i][input_len - input_remainder_len..input_len]);
+                self.buf[i][self.buf_len..self.buf_len + remainder]
+                    .copy_from_slice(&inputs[i][input_len - remainder..input_len]);
             }
 
-            self.buf_len += input_remainder_len;
+            self.buf_len += remainder;
         }
     }
 
@@ -266,9 +267,7 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         PARALLEL_LANES == 1 &&
         keccak_xof_state_inv(self)
     )]
-    #[hax_lib::ensures(|_|
-        keccak_xof_state_inv(future(self))
-    )]
+    #[hax_lib::ensures(|_| keccak_xof_state_inv(future(self)))]
     pub(crate) fn absorb_final<const DELIMITER: u8>(&mut self, inputs: &[&[u8]; PARALLEL_LANES])
     where
         KeccakState<PARALLEL_LANES, STATE>: Absorb<PARALLEL_LANES>,
diff --git a/libcrux-sha3/src/lib.rs b/libcrux-sha3/src/lib.rs
index 7b98e8423..e00362cb4 100644
--- a/libcrux-sha3/src/lib.rs
+++ b/libcrux-sha3/src/lib.rs
@@ -55,8 +55,7 @@ pub enum Algorithm {
 }
 
 // TODO: Verification fails because of the panic
-#[hax_lib::fstar::replace("")]
-#[hax_lib::attributes]
+#[cfg(not(any(hax, eurydice)))]
 impl From<u32> for Algorithm {
     #[hax_lib::requires(v == 1 || v == 2 || v == 3 || v == 4)]
     fn from(v: u32) -> Algorithm {
@@ -84,10 +83,10 @@ impl From<Algorithm> for u32 {
 /// Returns the output size of a digest.
 pub const fn digest_size(mode: Algorithm) -> usize {
     match mode {
-        Algorithm::Sha224 => SHA3_224_DIGEST_SIZE,
-        Algorithm::Sha256 => SHA3_256_DIGEST_SIZE,
-        Algorithm::Sha384 => SHA3_384_DIGEST_SIZE,
-        Algorithm::Sha512 => SHA3_512_DIGEST_SIZE,
+        Algorithm::Sha224 => 28,
+        Algorithm::Sha256 => 32,
+        Algorithm::Sha384 => 48,
+        Algorithm::Sha512 => 64,
     }
 }
 
diff --git a/libcrux-sha3/src/portable.rs b/libcrux-sha3/src/portable.rs
index 4685570f1..01b088d4f 100644
--- a/libcrux-sha3/src/portable.rs
+++ b/libcrux-sha3/src/portable.rs
@@ -102,39 +102,27 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
 
     #[hax_lib::attributes]
     impl Xof<168> for Shake128Xof {
-        #[hax_lib::ensures(|result|
-            keccak_xof_state_inv(&result.state)
-        )]
+        #[hax_lib::ensures(|result|keccak_xof_state_inv(&result.state))]
         fn new() -> Self {
             Self {
                 state: KeccakXofState::<1, 168, u64>::new(),
             }
         }
 
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
-        #[hax_lib::ensures(|_|
-            keccak_xof_state_inv(&future(self).state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
+        #[hax_lib::ensures(|_| keccak_xof_state_inv(&future(self).state))]
         fn absorb(&mut self, input: &[u8]) {
             self.state.absorb(&[input]);
         }
 
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
-        #[hax_lib::ensures(|_|
-            keccak_xof_state_inv(&future(self).state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
+        #[hax_lib::ensures(|_| keccak_xof_state_inv(&future(self).state))]
         fn absorb_final(&mut self, input: &[u8]) {
             self.state.absorb_final::<0x1fu8>(&[input]);
         }
 
         /// Shake128 squeeze
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
         #[hax_lib::ensures(|_|
             keccak_xof_state_inv(&self.state) &&
             future(out).len() == out.len()
@@ -148,9 +136,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::attributes]
     impl Xof<136> for Shake256Xof {
         /// Shake256 new state
-        #[hax_lib::ensures(|result|
-            keccak_xof_state_inv(&result.state)
-        )]
+        #[hax_lib::ensures(|result| keccak_xof_state_inv(&result.state))]
         fn new() -> Self {
             Self {
                 state: KeccakXofState::<1, 136, u64>::new(),
@@ -158,31 +144,21 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
         }
 
         /// Shake256 absorb
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
-        #[hax_lib::ensures(|_|
-            keccak_xof_state_inv(&future(self).state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
+        #[hax_lib::ensures(|_| keccak_xof_state_inv(&future(self).state))]
         fn absorb(&mut self, input: &[u8]) {
             self.state.absorb(&[input]);
         }
 
         /// Shake256 absorb final
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
-        #[hax_lib::ensures(|_|
-            keccak_xof_state_inv(&future(self).state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
+        #[hax_lib::ensures(|_| keccak_xof_state_inv(&future(self).state))]
         fn absorb_final(&mut self, input: &[u8]) {
             self.state.absorb_final::<0x1fu8>(&[input]);
         }
 
         /// Shake256 squeeze
-        #[hax_lib::requires(
-            keccak_xof_state_inv(&self.state)
-        )]
+        #[hax_lib::requires(keccak_xof_state_inv(&self.state))]
         #[hax_lib::ensures(|_|
             keccak_xof_state_inv(&self.state) &&
             future(out).len() == out.len()
@@ -215,9 +191,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::requires(
         out0.len().to_int() >= hax_lib::int!(504) // 3 * 168 = 504
     )]
-    #[hax_lib::ensures(
-        |_| future(out0).len() == out0.len()
-    )]
+    #[hax_lib::ensures(|_| future(out0).len() == out0.len())]
     pub fn shake128_squeeze_first_three_blocks(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_first_three_blocks::<168>(out0);
     }
@@ -227,9 +201,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::requires(
         out0.len().to_int() >= hax_lib::int!(840) // 5 * 168 = 840
     )]
-    #[hax_lib::ensures(
-        |_| future(out0).len() == out0.len()
-    )]
+    #[hax_lib::ensures(|_| future(out0).len() == out0.len())]
     pub fn shake128_squeeze_first_five_blocks(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_first_five_blocks::<168>(out0);
     }
@@ -239,9 +211,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::requires(
         out0.len().to_int() >= hax_lib::int!(168)
     )]
-    #[hax_lib::ensures(
-        |_| future(out0).len() == out0.len()
-    )]
+    #[hax_lib::ensures(|_| future(out0).len() == out0.len())]
     pub fn shake128_squeeze_next_block(s: &mut KeccakState, out0: &mut [u8]) {
         s.state.squeeze_next_block::<168>(out0, 0)
     }
@@ -268,9 +238,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::requires(
         out.len().to_int() >= hax_lib::int!(136)
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub fn shake256_squeeze_first_block(s: &mut KeccakState, out: &mut [u8]) {
         s.state.squeeze_first_block::<136>(out);
     }
@@ -280,9 +248,7 @@ let impl__from__private: t_Sealed t_Shake256Xof = { __marker_trait_t_Sealed = ()
     #[hax_lib::requires(
         out.len().to_int() >= hax_lib::int!(136)
     )]
-    #[hax_lib::ensures(
-        |_| future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     pub fn shake256_squeeze_next_block(s: &mut KeccakState, out: &mut [u8]) {
         s.state.squeeze_next_block::<136>(out, 0);
     }
diff --git a/libcrux-sha3/src/simd/portable.rs b/libcrux-sha3/src/simd/portable.rs
index ba8c287d0..9a7d6e2a9 100644
--- a/libcrux-sha3/src/simd/portable.rs
+++ b/libcrux-sha3/src/simd/portable.rs
@@ -109,9 +109,7 @@ pub(crate) fn load_last<const RATE: usize, const DELIMITER: u8>(
     len <= 200 &&
     start.to_int() + len.to_int() <= out.len().to_int()
 )]
-#[hax_lib::ensures(|_|
-    future(out).len() == out.len()
-)]
+#[hax_lib::ensures(|_| future(out).len() == out.len())]
 pub(crate) fn store_block<const RATE: usize>(
     s: &[u64; 25],
     out: &mut [u8],
@@ -125,6 +123,7 @@ pub(crate) fn store_block<const RATE: usize>(
 
     for i in 0..octets {
         hax_lib::loop_invariant!(|i: usize| out.len() == out_len);
+
         let value = get_ij(s, i / 5, i % 5);
         let bytes = value.to_le_bytes();
         let out_pos = start + 8 * i;
@@ -209,9 +208,7 @@ impl Squeeze<u64> for KeccakState<1, u64> {
         len <= 200 &&
         start.to_int() + len.to_int() <= out.len().to_int()
     )]
-    #[hax_lib::ensures(|_|
-        future(out).len() == out.len()
-    )]
+    #[hax_lib::ensures(|_| future(out).len() == out.len())]
     fn squeeze<const RATE: usize>(&self, out: &mut [u8], start: usize, len: usize) {
         store_block::<RATE>(&self.st, out, start, len);
     }
diff --git a/libcrux-sha3/src/traits.rs b/libcrux-sha3/src/traits.rs
index edd54533b..7c4aac58a 100644
--- a/libcrux-sha3/src/traits.rs
+++ b/libcrux-sha3/src/traits.rs
@@ -1,7 +1,5 @@
-use hax_lib;
-
 #[cfg(hax)]
-use hax_lib::int::*;
+use hax_lib::{self, constructors::from_bool, forall, implies, int::ToInt};
 
 // XXX: These should be default functions on `KeccakItem`, but hax doesn't
 //      support that yet. cryspen/hax#888
@@ -62,20 +60,40 @@ pub(crate) trait KeccakItem<const N: usize>: Clone + Copy {
 pub(crate) trait Absorb<const N: usize> {
     /// Absorb a block
     #[hax_lib::requires(
+      from_bool(
         N != 0 &&
         RATE <= 200 &&
         RATE % 8 == 0 &&
+        (RATE % 32 == 8 || RATE % 32 == 16) &&
         start.to_int() + RATE.to_int() <= input[0].len().to_int()
+      ).and(
+        forall(|i: usize|
+          implies(
+            i < N,
+            input[0].len() == input[i].len()
+          )
+        )
+      )
     )]
     fn load_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize);
 
     /// Absorb the last block (may be partial)
     #[hax_lib::requires(
+      from_bool(
         N != 0 &&
         RATE <= 200 &&
         RATE % 8 == 0 &&
+        (RATE % 32 == 8 || RATE % 32 == 16) &&
         len < RATE &&
         start.to_int() + len.to_int() <= input[0].len().to_int()
+      ).and(
+        forall(|i: usize|
+          implies(
+            i < N,
+            input[0].len() == input[i].len()
+          )
+        )
+      )
     )]
     fn load_last<const RATE: usize, const DELIMITER: u8>(
         &mut self,

From 8dd8df70dd854fc57cd8f7c027164a2ee96499d3 Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Thu, 13 Nov 2025 13:23:51 +0100
Subject: [PATCH 4/6] Extract Core Models on build and Fix portable extraction

---
 libcrux-sha3/hax.py | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/libcrux-sha3/hax.py b/libcrux-sha3/hax.py
index 7bbf03b92..27c51849d 100755
--- a/libcrux-sha3/hax.py
+++ b/libcrux-sha3/hax.py
@@ -94,10 +94,24 @@ def __call__(self, parser, args, values, option_string=None) -> None:
             env=hax_env,
         )
 
+        # Extract Core models
+        cargo_hax_into = [
+            "cargo",
+            "hax",
+            "into",
+            "fstar",
+        ]
+        hax_env = {}
+        shell(
+            cargo_hax_into,
+            cwd="../fstar-helpers/core-models",
+            env=hax_env,
+        )
+
         # Extract sha3
         if args.portable:
             # For portable-only: exclude all SIMD implementations
-            include_str = "+** -**::avx2::** -**::neon::** -**::simd::** -**::simd128::** -**::simd256::** +**::simd::portable::**"
+            include_str = "+** -**::avx2::** -**::neon::** -**::simd128::** -**::simd256::**"
             cargo_args = []
         else:
             include_str = "+**"

From 153b00374fe9f25ab247b0f9967958584a450a4e Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Wed, 19 Nov 2025 13:26:05 +0100
Subject: [PATCH 5/6] apply feedback from franziskuskiefer 2

---
 libcrux-sha3/src/generic_keccak.rs          |  30 +++---
 libcrux-sha3/src/generic_keccak/portable.rs |  19 ++--
 libcrux-sha3/src/generic_keccak/xof.rs      | 101 ++++++++++----------
 libcrux-sha3/src/lemmas.rs                  |  44 ---------
 libcrux-sha3/src/lib.rs                     |   7 +-
 libcrux-sha3/src/proof_utils.rs             |  60 ++++++++++++
 libcrux-sha3/src/simd/portable.rs           |  33 ++++---
 libcrux-sha3/src/traits.rs                  |  41 ++++----
 8 files changed, 166 insertions(+), 169 deletions(-)
 delete mode 100644 libcrux-sha3/src/lemmas.rs
 create mode 100644 libcrux-sha3/src/proof_utils.rs

diff --git a/libcrux-sha3/src/generic_keccak.rs b/libcrux-sha3/src/generic_keccak.rs
index b3d9dac50..a87a6adad 100644
--- a/libcrux-sha3/src/generic_keccak.rs
+++ b/libcrux-sha3/src/generic_keccak.rs
@@ -6,7 +6,10 @@ use core::ops::Index;
 use crate::traits::*;
 
 #[cfg(hax)]
-use hax_lib::{constructors::from_bool, forall, implies, int::ToInt};
+use crate::proof_utils::{slices_same_len, valid_rate};
+
+#[cfg(hax)]
+use hax_lib::{constructors::from_bool, int::ToInt};
 
 /// A generic Xof API.
 pub(crate) mod xof;
@@ -99,6 +102,9 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
         ]
     }
 
+    // Splitting rho and pi into multiple functions is needed for formal verification in F*.
+    // Having to many manipulations of the keccak state in a single function causes the
+    // verification condition explode exponentially and never completes.
     #[inline(always)]
     fn rho_0(&mut self, t: [T; 5]) {
         self.set(0, 0, T::xor(self[(0, 0)], t[0]));
@@ -245,17 +251,10 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     #[hax_lib::requires(
       from_bool(
         N != 0 &&
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
-        (RATE % 32 == 8 || RATE % 32 == 16) &&
+        valid_rate(RATE) &&
         start.to_int() + RATE.to_int() <= input[0].len().to_int()
       ).and(
-        forall(|i: usize|
-          implies(
-            i < N,
-            input[0].len() == input[i].len()
-          )
-        )
+        slices_same_len(input)
       )
     )]
     fn absorb_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize)
@@ -273,18 +272,11 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     #[hax_lib::requires(
       from_bool(
         N != 0 &&
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
-        (RATE % 32 == 8 || RATE % 32 == 16) &&
+        valid_rate(RATE) &&
         len < RATE &&
         start.to_int() + len.to_int() <= input[0].len().to_int()
       ).and(
-        forall(|i: usize|
-          implies(
-            i < N,
-            input[0].len() == input[i].len()
-          )
-        )
+        slices_same_len(input)
       )
     )]
     pub(crate) fn absorb_final<const RATE: usize, const DELIM: u8>(
diff --git a/libcrux-sha3/src/generic_keccak/portable.rs b/libcrux-sha3/src/generic_keccak/portable.rs
index 1a0e5cc44..d1b328787 100644
--- a/libcrux-sha3/src/generic_keccak/portable.rs
+++ b/libcrux-sha3/src/generic_keccak/portable.rs
@@ -1,14 +1,17 @@
 use super::*;
 
 #[cfg(hax)]
-#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
+use crate::proof_utils::valid_rate;
+
+#[cfg(hax)]
+#[hax_lib::fstar::replace("open Libcrux_sha3.Proof_utils.Lemmas")]
 const _: () = ();
 
 #[hax_lib::attributes]
 impl KeccakState<1, u64> {
     #[inline(always)]
     #[hax_lib::requires(
-        RATE <= 200 &&
+        valid_rate(RATE) &&
         start.to_int() + RATE.to_int() <= out.len().to_int()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -19,7 +22,7 @@ impl KeccakState<1, u64> {
 
     #[inline(always)]
     #[hax_lib::requires(
-        RATE <= 200 &&
+        valid_rate(RATE) &&
         RATE <= out.len()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -29,7 +32,7 @@ impl KeccakState<1, u64> {
 
     #[inline(always)]
     #[hax_lib::requires(
-        RATE <= 200 &&
+        valid_rate(RATE) &&
         3 * RATE <= out.len()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -45,7 +48,7 @@ impl KeccakState<1, u64> {
 
     #[inline(always)]
     #[hax_lib::requires(
-        RATE <= 200 &&
+        valid_rate(RATE) &&
         5 * RATE <= out.len()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -66,11 +69,7 @@ impl KeccakState<1, u64> {
     }
 }
 
-#[hax_lib::requires(
-    RATE != 0 &&
-    RATE <= 200 &&
-    RATE % 8 == 0
-)]
+#[hax_lib::requires(valid_rate(RATE))]
 #[hax_lib::ensures(|_| future(output).len() == output.len())]
 #[hax_lib::fstar::options("--split_queries always --z3rlimit 300")]
 #[inline]
diff --git a/libcrux-sha3/src/generic_keccak/xof.rs b/libcrux-sha3/src/generic_keccak/xof.rs
index 7b07db43a..1152dae1c 100644
--- a/libcrux-sha3/src/generic_keccak/xof.rs
+++ b/libcrux-sha3/src/generic_keccak/xof.rs
@@ -6,10 +6,14 @@ use crate::{
 };
 
 #[cfg(hax)]
-#[hax_lib::fstar::replace("open Libcrux_sha3.Lemmas")]
+use crate::proof_utils::valid_rate;
+
+#[cfg(hax)]
+#[hax_lib::fstar::replace("open Libcrux_sha3.Proof_utils.Lemmas")]
 const _: () = ();
 
-// TODO: Should not be needed. Use hax_lib::fstar::options("")
+// TODO: Should not be needed. Use hax_lib::fstar::options("") below.
+// Known bug: https://github.com/cryspen/hax/issues/1698
 #[hax_lib::fstar::before(
     r#"
 #push-options "--split_queries always --z3rlimit 300"
@@ -18,7 +22,6 @@ const _: () = ();
 
 /// The internal keccak state that can also buffer inputs to absorb.
 /// This is used in the general xof APIs.
-#[hax_lib::attributes]
 pub(crate) struct KeccakXofState<
     const PARALLEL_LANES: usize,
     const RATE: usize,
@@ -44,15 +47,11 @@ pub(crate) fn keccak_xof_state_inv<
 >(
     xof: &KeccakXofState<PARALLEL_LANES, RATE, STATE>,
 ) -> bool {
-    RATE != 0
-        && RATE <= 200
-        && RATE % 8 == 0
-        && (RATE % 32 == 8 || RATE % 32 == 16)
-        && xof.buf_len <= RATE
+    valid_rate(RATE) && xof.buf_len <= RATE
 }
 
 #[hax_lib::attributes]
-#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] // TODO: Has no effect
+#[hax_lib::fstar::options("--split_queries always --z3rlimit 300")] // TODO: Has no effect. See above.
 impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_LANES>>
     KeccakXofState<PARALLEL_LANES, RATE, STATE>
 {
@@ -63,10 +62,8 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
 
     /// Generate a new keccak xof state.
     #[hax_lib::requires(
-        PARALLEL_LANES == 1 && // TODO: Generalize for the parallel case
-        RATE != 0 &&
-        RATE <= 200 &&
-        RATE % 8 == 0
+        PARALLEL_LANES == 1 &&
+        valid_rate(RATE)
     )]
     #[hax_lib::ensures(|result| keccak_xof_state_inv(&result))]
     pub(crate) fn new() -> Self {
@@ -97,7 +94,6 @@ 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::fstar::options("--fuel 5")]
     #[hax_lib::requires(
         PARALLEL_LANES == 1 &&
         keccak_xof_state_inv(self)
@@ -186,13 +182,11 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         let remainder = input_to_consume % RATE;
 
         #[cfg(hax)]
-        let self_buf_len = self.buf_len;
-
-        #[cfg(hax)]
-        let end = consumed + num_blocks * RATE;
-
-        #[cfg(hax)]
-        hax_lib::assert!(end <= inputs[0].len());
+        let (self_buf_len, end) = {
+            let end = consumed + num_blocks * RATE;
+            hax_lib::assert!(end <= inputs[0].len());
+            (self.buf_len, end)
+        };
 
         for i in 0..num_blocks {
             hax_lib::loop_invariant!(|_: usize| self.buf_len == self_buf_len);
@@ -298,6 +292,12 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
     where
         KeccakState<1, STATE>: Squeeze<STATE>,
     {
+        let out_len = out.len();
+
+        if out_len == 0 {
+            return;
+        }
+
         if self.sponge {
             // If we called `squeeze` before, call f1600 first.
             // We do it this way around so that we don't call f1600 at the end
@@ -305,47 +305,42 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
             self.inner.keccakf1600();
         }
 
-        let out_len = out.len();
-
-        if out_len > 0 {
-            if out_len <= RATE {
-                self.inner.squeeze::<RATE>(out, 0, out_len);
-            } else {
-                // How many blocks do we need to squeeze out?
-                let blocks = out_len / RATE;
+        if out_len <= RATE {
+            self.inner.squeeze::<RATE>(out, 0, out_len);
+        } else {
+            // How many blocks do we need to squeeze out?
+            let blocks = out_len / RATE;
+            let remaining = out_len % RATE;
 
-                #[cfg(hax)]
-                let self_buf_len = self.buf_len;
+            #[cfg(hax)]
+            let self_buf_len = self.buf_len;
 
-                for i in 0..blocks {
-                    hax_lib::loop_invariant!(
-                        |_: usize| out.len() == out_len && self_buf_len == self.buf_len
-                    );
-                    hax_lib::fstar!("assert (v i * v v_RATE <= v out_len)");
+            for i in 0..blocks {
+                hax_lib::loop_invariant!(
+                    |_: usize| out.len() == out_len && self_buf_len == self.buf_len
+                );
+                hax_lib::assert!(i.to_int() * RATE.to_int() <= out.len().to_int());
 
-                    #[cfg(hax)]
-                    hax_lib::assert!(i.to_int() * RATE.to_int() <= out.len().to_int());
+                // Here we know that we always have full blocks to write out.
+                self.inner.keccakf1600();
+                self.inner.squeeze::<RATE>(out, i * RATE, RATE);
+            }
 
-                    // Here we know that we always have full blocks to write out.
-                    self.inner.keccakf1600();
-                    self.inner.squeeze::<RATE>(out, i * RATE, RATE);
-                }
+            if remaining > 0 {
+                // Squeeze out the last partial block
+                self.inner.keccakf1600();
 
                 // For a and b with b < a
                 // (a / b) * b + a % b = a
+                hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
+                hax_lib::assert!(
+                    blocks.to_int() * RATE.to_int() + remaining.to_int() == out.len().to_int()
+                );
 
-                let remaining = out_len % RATE;
-                if remaining > 0 {
-                    // Squeeze out the last partial block
-                    self.inner.keccakf1600();
-
-                    hax_lib::fstar!("lemma_div_mul_mod out_len v_RATE");
-                    hax_lib::fstar!("assert (v blocks * v v_RATE + v remaining == v out_len)");
-
-                    self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
-                }
+                self.inner.squeeze::<RATE>(out, blocks * RATE, remaining);
             }
-            self.sponge = true;
         }
+
+        self.sponge = true;
     }
 }
diff --git a/libcrux-sha3/src/lemmas.rs b/libcrux-sha3/src/lemmas.rs
deleted file mode 100644
index 28dc28096..000000000
--- a/libcrux-sha3/src/lemmas.rs
+++ /dev/null
@@ -1,44 +0,0 @@
-//! F* verification lemmas for SHA3/Keccak implementation.
-//!
-//! This module contains lemmas used for F* verification across
-//! the libcrux-sha3 crate. These lemmas are only used during
-//! formal verification with hax and F*, and have no runtime behavior.
-
-/// Lemma proving the division-multiplication-modulo identity.
-///
-/// For any `a`, `b` with `b != 0`,
-/// proves that `(a / b) * b + (a % b) = a`.
-///
-/// This is used in the `squeeze` function to verify correct buffer indexing
-/// when squeezing multiple blocks.
-#[hax_lib::fstar::replace(
-    r#"
-let lemma_div_mul_mod (a b: usize)
-    : Lemma
-        (requires b <>. mk_usize 0)
-        (ensures (a /! b) *! b +! (a %! b) =. a)
-    = ()
-"#
-)]
-const _LEMMA_DIV_MUL_MOD: () = ();
-
-/// Lemma proving multiplication bounds for successive elements.
-///
-/// For any `k < n`,
-/// proves that `k * d + d ≤ n * d`.
-///
-/// This is used in the `keccak` functions to verify that block iterations
-/// stay within bounds.
-#[hax_lib::fstar::replace(
-    r#"
-let rec mul_succ_le (k n d: nat)
-  : Lemma
-    (requires k < n)
-    (ensures k * d + d <= n * d)
-    (decreases n) =
-  if n = 0 then ()
-  else if k = n - 1 then ()
-  else mul_succ_le k (n - 1) d
-"#
-)]
-const _LEMMA_MUL_SUCC_LE: () = ();
diff --git a/libcrux-sha3/src/lib.rs b/libcrux-sha3/src/lib.rs
index e00362cb4..7a07b4263 100644
--- a/libcrux-sha3/src/lib.rs
+++ b/libcrux-sha3/src/lib.rs
@@ -21,9 +21,9 @@ use hax_lib::int::*;
 
 mod traits;
 
-/// F* verification lemmas
+/// F* verification helper
 #[cfg(hax)]
-pub(crate) mod lemmas;
+pub(crate) mod proof_utils;
 
 /// A SHA3 224 Digest
 pub type Sha3_224Digest = [u8; 28];
@@ -54,10 +54,9 @@ pub enum Algorithm {
     Sha512 = 4,
 }
 
-// TODO: Verification fails because of the panic
+// Verification fails because of the panic
 #[cfg(not(any(hax, eurydice)))]
 impl From<u32> for Algorithm {
-    #[hax_lib::requires(v == 1 || v == 2 || v == 3 || v == 4)]
     fn from(v: u32) -> Algorithm {
         match v {
             1 => Algorithm::Sha224,
diff --git a/libcrux-sha3/src/proof_utils.rs b/libcrux-sha3/src/proof_utils.rs
new file mode 100644
index 000000000..e2017b718
--- /dev/null
+++ b/libcrux-sha3/src/proof_utils.rs
@@ -0,0 +1,60 @@
+use hax_lib::{forall, implies, Prop};
+
+/// Checks if all slices in an array have the same length.
+pub(crate) fn slices_same_len<const N: usize>(slices: &[&[u8]; N]) -> Prop {
+    forall(|i: usize| implies(i < N, slices[0].len() == slices[i].len()))
+}
+
+pub(crate) fn valid_rate(rate: usize) -> bool {
+    // This is could be changed to checking against the specific valid rates
+    // corresponding to: SHA3-512, SHA3-384, SHA3-256/SHAKE256, SHA3-224, SHAKE128
+    // rate == 72 || rate == 104 || rate == 136 || rate == 144 || rate == 168
+    rate != 0 && rate <= 200 && rate % 8 == 0 && (rate % 32 == 8 || rate % 32 == 16)
+}
+
+mod lemmas {
+    //! F* verification lemmas for SHA3/Keccak implementation.
+    //!
+    //! This module contains lemmas used for F* verification across
+    //! the libcrux-sha3 crate. These lemmas are only used during
+    //! formal verification with hax and F*, and have no runtime behavior.
+
+    /// Lemma proving the division-multiplication-modulo identity.
+    ///
+    /// For any `a`, `b` with `b != 0`,
+    /// proves that `(a / b) * b + (a % b) = a`.
+    ///
+    /// This is used in the `squeeze` function to verify correct buffer indexing
+    /// when squeezing multiple blocks.
+    #[hax_lib::fstar::replace(
+        r#"
+let lemma_div_mul_mod (a b: usize)
+    : Lemma
+        (requires b <>. mk_usize 0)
+        (ensures (a /! b) *! b +! (a %! b) =. a)
+    = ()
+"#
+    )]
+    const _LEMMA_DIV_MUL_MOD: () = ();
+
+    /// Lemma proving multiplication bounds for successive elements.
+    ///
+    /// For any `k < n`,
+    /// proves that `k * d + d ≤ n * d`.
+    ///
+    /// This is used in the `keccak` functions to verify that block iterations
+    /// stay within bounds.
+    #[hax_lib::fstar::replace(
+        r#"
+let rec mul_succ_le (k n d: nat)
+  : Lemma
+    (requires k < n)
+    (ensures k * d + d <= n * d)
+    (decreases n) =
+  if n = 0 then ()
+  else if k = n - 1 then ()
+  else mul_succ_le k (n - 1) d
+"#
+    )]
+    const _LEMMA_MUL_SUCC_LE: () = ();
+}
diff --git a/libcrux-sha3/src/simd/portable.rs b/libcrux-sha3/src/simd/portable.rs
index 9a7d6e2a9..fa57b797f 100644
--- a/libcrux-sha3/src/simd/portable.rs
+++ b/libcrux-sha3/src/simd/portable.rs
@@ -3,12 +3,15 @@
 #[cfg(hax)]
 use hax_lib::int::*;
 
+#[cfg(hax)]
+use crate::proof_utils::valid_rate;
+
 use crate::{generic_keccak::KeccakState, traits::*};
 
 #[inline(always)]
 #[hax_lib::requires(
     LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
-    RIGHT >= 0
+    RIGHT > 0
 )]
 fn rotate_left<const LEFT: i32, const RIGHT: i32>(x: u64) -> u64 {
     #[cfg(not(eurydice))]
@@ -29,7 +32,7 @@ fn _vrax1q_u64(a: u64, b: u64) -> u64 {
 #[inline(always)]
 #[hax_lib::requires(
     LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
-    RIGHT >= 0
+    RIGHT > 0
 )]
 fn _vxarq_u64<const LEFT: i32, const RIGHT: i32>(a: u64, b: u64) -> u64 {
     rotate_left::<LEFT, RIGHT>(a ^ b)
@@ -47,8 +50,7 @@ fn _veorq_n_u64(a: u64, c: u64) -> u64 {
 
 #[inline(always)]
 #[hax_lib::requires(
-    RATE <= 200 &&
-    RATE % 8 == 0 &&
+    valid_rate(RATE) &&
     start.to_int() + RATE.to_int() <= blocks.len().to_int()
 )]
 pub(crate) fn load_block<const RATE: usize>(state: &mut [u64; 25], blocks: &[u8], start: usize) {
@@ -82,8 +84,7 @@ pub(crate) fn load_block<const RATE: usize>(state: &mut [u64; 25], blocks: &[u8]
 
 #[inline(always)]
 #[hax_lib::requires(
-    RATE <= 200 &&
-    RATE % 8 == 0 &&
+    valid_rate(RATE) &&
     len < RATE &&
     start.to_int() + len.to_int() <= blocks.len().to_int()
 )]
@@ -106,7 +107,8 @@ pub(crate) fn load_last<const RATE: usize, const DELIMITER: u8>(
 
 #[inline(always)]
 #[hax_lib::requires(
-    len <= 200 &&
+    valid_rate(RATE) &&
+    len <= RATE &&
     start.to_int() + len.to_int() <= out.len().to_int()
 )]
 #[hax_lib::ensures(|_| future(out).len() == out.len())]
@@ -124,16 +126,14 @@ pub(crate) fn store_block<const RATE: usize>(
     for i in 0..octets {
         hax_lib::loop_invariant!(|i: usize| out.len() == out_len);
 
-        let value = get_ij(s, i / 5, i % 5);
-        let bytes = value.to_le_bytes();
+        let bytes = get_ij(s, i / 5, i % 5).to_le_bytes();
         let out_pos = start + 8 * i;
         out[out_pos..out_pos + 8].copy_from_slice(&bytes);
     }
 
     let remaining = len % 8;
     if remaining > 0 {
-        let value = get_ij(s, octets / 5, octets % 5);
-        let bytes = value.to_le_bytes();
+        let bytes = get_ij(s, octets / 5, octets % 5).to_le_bytes();
         let out_pos = start + len - remaining;
         out[out_pos..out_pos + remaining].copy_from_slice(&bytes[..remaining]);
     }
@@ -156,7 +156,7 @@ impl KeccakItem<1> for u64 {
     #[inline(always)]
     #[hax_lib::requires(
         LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
-        RIGHT >= 0
+        RIGHT > 0
     )]
     fn xor_and_rotate<const LEFT: i32, const RIGHT: i32>(a: Self, b: Self) -> Self {
         _vxarq_u64::<LEFT, RIGHT>(a, b)
@@ -178,8 +178,7 @@ impl KeccakItem<1> for u64 {
 #[hax_lib::attributes]
 impl Absorb<1> for KeccakState<1, u64> {
     #[hax_lib::requires(
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
+        valid_rate(RATE) &&
         start.to_int() + RATE.to_int() <= input[0].len().to_int()
     )]
     fn load_block<const RATE: usize>(&mut self, input: &[&[u8]; 1], start: usize) {
@@ -187,8 +186,7 @@ impl Absorb<1> for KeccakState<1, u64> {
     }
 
     #[hax_lib::requires(
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
+        valid_rate(RATE) &&
         len < RATE &&
         start.to_int() + len.to_int() <= input[0].len().to_int()
     )]
@@ -205,7 +203,8 @@ impl Absorb<1> for KeccakState<1, u64> {
 #[hax_lib::attributes]
 impl Squeeze<u64> for KeccakState<1, u64> {
     #[hax_lib::requires(
-        len <= 200 &&
+        valid_rate(RATE) &&
+        len <= RATE &&
         start.to_int() + len.to_int() <= out.len().to_int()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]
diff --git a/libcrux-sha3/src/traits.rs b/libcrux-sha3/src/traits.rs
index 7c4aac58a..99b9328d0 100644
--- a/libcrux-sha3/src/traits.rs
+++ b/libcrux-sha3/src/traits.rs
@@ -1,5 +1,8 @@
 #[cfg(hax)]
-use hax_lib::{self, constructors::from_bool, forall, implies, int::ToInt};
+use hax_lib::{self, constructors::from_bool, int::ToInt};
+
+#[cfg(hax)]
+use crate::proof_utils::{slices_same_len, valid_rate};
 
 // XXX: These should be default functions on `KeccakItem`, but hax doesn't
 //      support that yet. cryspen/hax#888
@@ -38,7 +41,8 @@ pub(crate) trait KeccakItem<const N: usize>: Clone + Copy {
     /// `(a ^ b) <<< LEFT`
     #[hax_lib::requires(
         LEFT.to_int() + RIGHT.to_int() == 64.to_int() &&
-        RIGHT >= 0
+        RIGHT > 0 &&
+        RIGHT < 64
     )]
     fn xor_and_rotate<const LEFT: i32, const RIGHT: i32>(a: Self, b: Self) -> Self;
 
@@ -62,17 +66,10 @@ pub(crate) trait Absorb<const N: usize> {
     #[hax_lib::requires(
       from_bool(
         N != 0 &&
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
-        (RATE % 32 == 8 || RATE % 32 == 16) &&
+        valid_rate(RATE) &&
         start.to_int() + RATE.to_int() <= input[0].len().to_int()
       ).and(
-        forall(|i: usize|
-          implies(
-            i < N,
-            input[0].len() == input[i].len()
-          )
-        )
+        slices_same_len(input)
       )
     )]
     fn load_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize);
@@ -81,18 +78,11 @@ pub(crate) trait Absorb<const N: usize> {
     #[hax_lib::requires(
       from_bool(
         N != 0 &&
-        RATE <= 200 &&
-        RATE % 8 == 0 &&
-        (RATE % 32 == 8 || RATE % 32 == 16) &&
+        valid_rate(RATE) &&
         len < RATE &&
         start.to_int() + len.to_int() <= input[0].len().to_int()
       ).and(
-        forall(|i: usize|
-          implies(
-            i < N,
-            input[0].len() == input[i].len()
-          )
-        )
+        slices_same_len(input)
       )
     )]
     fn load_last<const RATE: usize, const DELIMITER: u8>(
@@ -103,6 +93,11 @@ pub(crate) trait Absorb<const N: usize> {
     );
 }
 
+// HAX does not support the &[mut &[u8]; N] Type. Because of that we have to
+// implement the Squeeze trait for each N separately. This complicates the
+// implementation in other files as well. Refactor when HAX supports it.
+// https://github.com/cryspen/hax/issues/420
+
 /// Trait to squeeze bytes out of the state.
 ///
 /// Note that this is implemented for each platform (1, 2, 4) because hax can't
@@ -113,11 +108,12 @@ pub(crate) trait Absorb<const N: usize> {
     interface, "
 class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
   // TODO: This super variable is problematic and makes typecheck fail
+  // https://github.com/cryspen/hax/issues/1554
   // [@@@ FStar.Tactics.Typeclasses.no_method]_super_18390613159176269294:t_KeccakItem v_T (mk_usize 1);
   f_squeeze_pre:v_RATE: usize -> self_: v_Self -> out: t_Slice u8 -> start: usize -> len: usize
     -> pred:
       Type0
-        { len <=. mk_usize 200 &&
+        { Libcrux_sha3.Proof_utils.valid_rate v_RATE && len <=. v_RATE &&
           ((Rust_primitives.Hax.Int.from_machine start <: Hax_lib.Int.t_Int) +
             (Rust_primitives.Hax.Int.from_machine len <: Hax_lib.Int.t_Int)
             <:
@@ -152,7 +148,8 @@ class t_Squeeze (v_Self: Type0) (v_T: Type0) = {
 #[hax_lib::attributes]
 pub(crate) trait Squeeze<T: KeccakItem<1>> {
     #[hax_lib::requires(
-        len <= 200 &&
+        valid_rate(RATE) &&
+        len <= RATE &&
         start.to_int() + len.to_int() <= out.len().to_int()
     )]
     #[hax_lib::ensures(|_| future(out).len() == out.len())]

From 589ff18c9a9445d040fe192c45ef1d57d4d87603 Mon Sep 17 00:00:00 2001
From: Parrot7483 <47054801+Parrot7483@users.noreply.github.com>
Date: Wed, 19 Nov 2025 16:28:07 +0100
Subject: [PATCH 6/6] revert auto lib.rs changes

---
 libcrux-sha3/src/lib.rs | 46 +++++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 25 deletions(-)

diff --git a/libcrux-sha3/src/lib.rs b/libcrux-sha3/src/lib.rs
index 7a07b4263..f50cd87a4 100644
--- a/libcrux-sha3/src/lib.rs
+++ b/libcrux-sha3/src/lib.rs
@@ -12,7 +12,6 @@ mod generic_keccak;
 
 #[cfg(not(any(hax, eurydice)))]
 mod impl_digest_trait;
-use cavp::Sha3;
 #[cfg(not(any(hax, eurydice)))]
 pub use impl_digest_trait::*;
 
@@ -21,22 +20,19 @@ use hax_lib::int::*;
 
 mod traits;
 
+/// Size in bytes of a SHA3 224 digest.
+pub const SHA3_224_DIGEST_SIZE: usize = 28;
+/// Size in bytes of a SHA3 256 digest.
+pub const SHA3_256_DIGEST_SIZE: usize = 32;
+/// Size in bytes of a SHA3 2384 digest.
+pub const SHA3_384_DIGEST_SIZE: usize = 48;
+/// Size in bytes of a SHA3 512 digest.
+pub const SHA3_512_DIGEST_SIZE: usize = 64;
+
 /// F* verification helper
 #[cfg(hax)]
 pub(crate) mod proof_utils;
 
-/// A SHA3 224 Digest
-pub type Sha3_224Digest = [u8; 28];
-
-/// A SHA3 256 Digest
-pub type Sha3_256Digest = [u8; 32];
-
-/// A SHA3 384 Digest
-pub type Sha3_384Digest = [u8; 48];
-
-/// A SHA3 512 Digest
-pub type Sha3_512Digest = [u8; 64];
-
 /// The Digest Algorithm.
 #[cfg_attr(not(eurydice), derive(Clone, Copy, Debug, PartialEq))]
 #[repr(u32)]
@@ -82,10 +78,10 @@ impl From<Algorithm> for u32 {
 /// Returns the output size of a digest.
 pub const fn digest_size(mode: Algorithm) -> usize {
     match mode {
-        Algorithm::Sha224 => 28,
-        Algorithm::Sha256 => 32,
-        Algorithm::Sha384 => 48,
-        Algorithm::Sha512 => 64,
+        Algorithm::Sha224 => SHA3_224_DIGEST_SIZE,
+        Algorithm::Sha256 => SHA3_256_DIGEST_SIZE,
+        Algorithm::Sha384 => SHA3_384_DIGEST_SIZE,
+        Algorithm::Sha512 => SHA3_512_DIGEST_SIZE,
     }
 }
 
@@ -115,8 +111,8 @@ pub use hash as sha3;
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha224(data: &[u8]) -> Sha3_224Digest {
-    let mut out = [0u8; 28];
+pub fn sha224(data: &[u8]) -> [u8; SHA3_224_DIGEST_SIZE] {
+    let mut out = [0u8; SHA3_224_DIGEST_SIZE];
     sha224_ema(&mut out, data);
     out
 }
@@ -144,8 +140,8 @@ pub fn sha224_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha256(data: &[u8]) -> Sha3_256Digest {
-    let mut out = [0u8; 32];
+pub fn sha256(data: &[u8]) -> [u8; SHA3_256_DIGEST_SIZE] {
+    let mut out = [0u8; SHA3_256_DIGEST_SIZE];
     sha256_ema(&mut out, data);
     out
 }
@@ -170,8 +166,8 @@ pub fn sha256_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha384(data: &[u8]) -> Sha3_384Digest {
-    let mut out = [0u8; 48];
+pub fn sha384(data: &[u8]) -> [u8; SHA3_384_DIGEST_SIZE] {
+    let mut out = [0u8; SHA3_384_DIGEST_SIZE];
     sha384_ema(&mut out, data);
     out
 }
@@ -196,8 +192,8 @@ pub fn sha384_ema(digest: &mut [u8], payload: &[u8]) {
     data.len().to_int() <= u32::MAX.to_int()
 )]
 #[inline(always)]
-pub fn sha512(data: &[u8]) -> Sha3_512Digest {
-    let mut out = [0u8; 64];
+pub fn sha512(data: &[u8]) -> [u8; SHA3_512_DIGEST_SIZE] {
+    let mut out = [0u8; SHA3_512_DIGEST_SIZE];
     sha512_ema(&mut out, data);
     out
 }