Add full type check for SHA3 portable

.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

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 = "+**"

libcrux-sha3/src/generic_keccak.rs

@@ -5,6 +5,12 @@ use core::ops::Index;
 
 use crate::traits::*;
 
+#[cfg(hax)]
+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;
 
@@ -96,33 +102,47 @@ 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)]
-    #[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 +151,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 +204,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,21 +248,40 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
     }
 
     #[inline(always)]
-    fn absorb_block<const RATE: usize>(&mut self, blocks: &[&[u8]; N], start: usize)
+    #[hax_lib::requires(
+      from_bool(
+        N != 0 &&
+        valid_rate(RATE) &&
+        start.to_int() + RATE.to_int() <= input[0].len().to_int()
+      ).and(
+        slices_same_len(input)
+      )
+    )]
+    fn absorb_block<const RATE: usize>(&mut self, input: &[&[u8]; N], start: usize)
     where
         Self: Absorb<N>,
     {
-        #[cfg(not(eurydice))]
-        debug_assert!(blocks.iter().all(|buf| buf.len() == blocks[0].len()));
+        #[cfg(not(any(eurydice, hax)))]
+        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(
+      from_bool(
+        N != 0 &&
+        valid_rate(RATE) &&
+        len < RATE &&
+        start.to_int() + len.to_int() <= input[0].len().to_int()
+      ).and(
+        slices_same_len(input)
+      )
+    )]
     pub(crate) fn absorb_final<const RATE: usize, const DELIM: u8>(
         &mut self,
-        last: &[&[u8]; N],
+        input: &[&[u8]; N],
         start: usize,
         len: usize,
     ) where
@@ -219,10 +290,10 @@ impl<const N: usize, T: KeccakItem<N>> KeccakState<N, T> {
         #[cfg(not(eurydice))]
         debug_assert!(N > 0 && len < RATE);
 
-        #[cfg(not(eurydice))]
-        debug_assert!(last.iter().all(|buf| buf.len() == last[0].len()));
+        #[cfg(not(any(eurydice, hax)))]
+        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()
     }
 }

libcrux-sha3/src/generic_keccak/portable.rs

@@ -1,18 +1,41 @@
 use super::*;
 
+#[cfg(hax)]
+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(
+        valid_rate(RATE) &&
+        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(
+        valid_rate(RATE) &&
+        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(
+        valid_rate(RATE) &&
+        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 +47,11 @@ impl KeccakState<1, u64> {
     }
 
     #[inline(always)]
+    #[hax_lib::requires(
+        valid_rate(RATE) &&
+        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,31 +69,43 @@ impl KeccakState<1, u64> {
     }
 }
 
+#[hax_lib::requires(valid_rate(RATE))]
+#[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 {
-        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 {
+        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);
         }
     }
 }