Panic freemdom for AVX2 and NEON SHA-3 backends

.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-intrinsics/src/arm64_extract.rs

@@ -68,6 +68,7 @@ pub fn _vst1q_u64(out: &mut [u64], v: _uint64x2_t) {
 }
 
 #[inline(always)]
+#[hax_lib::ensures(|_| future(out).len() == out.len())]
 pub fn _vst1q_bytes_u64(out: &mut [_int16x8_t], v: _uint64x2_t) {
     unimplemented!()
 }

libcrux-intrinsics/src/avx2.rs

@@ -13,6 +13,9 @@ pub type Vec128 = __m128i;
 pub type Vec256Float = __m256;
 
 #[hax_lib::opaque]
+#[hax_lib::ensures(|_|
+    future(output).len() == output.len()
+)]
 #[inline(always)]
 pub fn mm256_storeu_si256_u8(output: &mut [u8], vector: Vec256) {
     // Note: in this module the `debug_assert_eq!` are essentially sanity

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/avx2.rs

@@ -4,6 +4,20 @@ pub mod x4 {
 
     /// Perform 4 SHAKE256 operations in parallel
     #[allow(clippy::too_many_arguments)]
+    #[hax_lib::requires(
+        input0.len() == input1.len() &&
+        input0.len() == input2.len() &&
+        input0.len() == input3.len() &&
+        out0.len() == out1.len() &&
+        out0.len() == out2.len() &&
+        out0.len() == out3.len()
+    )]
+    #[hax_lib::ensures(|_|
+        future(out0).len() == out0.len() &&
+        future(out1).len() == out1.len() &&
+        future(out2).len() == out2.len() &&
+        future(out3).len() == out3.len()
+    )]
     #[inline(always)]
     pub fn shake256(
         input0: &[u8],
@@ -20,10 +34,14 @@ pub mod x4 {
 
     /// An incremental API to perform 4 operations in parallel
     pub mod incremental {
+        #[cfg(hax)]
+        use hax_lib::ToInt;
+
         use crate::generic_keccak::KeccakState as GenericState;
         use libcrux_intrinsics::avx2::*;
 
         /// The Keccak state for the incremental API.
+        #[hax_lib::fstar::before("noeq")]
         pub struct KeccakState {
             state: GenericState<4, Vec256>,
         }
@@ -37,6 +55,12 @@ pub mod x4 {
         }
 
         /// Absorb
+        #[hax_lib::requires(
+            data0.len().to_int() < hax_lib::int!(168) &&
+            data0.len() == data1.len() &&
+            data0.len() == data2.len() &&
+            data0.len() == data3.len()
+        )]
         #[inline(always)]
         pub fn shake128_absorb_final(
             s: &mut KeccakState,
@@ -51,6 +75,12 @@ pub mod x4 {
 
         /// Absorb
         #[inline(always)]
+        #[hax_lib::requires(
+            data0.len().to_int() < hax_lib::int!(136) &&
+            data0.len() == data1.len() &&
+            data0.len() == data2.len() &&
+            data0.len() == data3.len()
+        )]
         pub fn shake256_absorb_final(
             s: &mut KeccakState,
             data0: &[u8],
@@ -64,6 +94,18 @@ pub mod x4 {
 
         /// Squeeze block
         #[inline(always)]
+        #[hax_lib::requires(
+            out0.len().to_int() >= hax_lib::int!(136) &&
+            out0.len() == out1.len() &&
+            out0.len() == out2.len() &&
+            out0.len() == out3.len()
+        )]
+        #[hax_lib::ensures(|_|
+            future(out0).len() == out0.len() &&
+            future(out1).len() == out1.len() &&
+            future(out2).len() == out2.len() &&
+            future(out3).len() == out3.len()
+        )]
         pub fn shake256_squeeze_first_block(
             s: &mut KeccakState,
             out0: &mut [u8],
@@ -76,6 +118,18 @@ pub mod x4 {
 
         /// Squeeze next block
         #[inline(always)]
+        #[hax_lib::requires(
+            out0.len().to_int() >= hax_lib::int!(136) &&
+            out0.len() == out1.len() &&
+            out0.len() == out2.len() &&
+            out0.len() == out3.len()
+        )]
+        #[hax_lib::ensures(|_|
+            future(out0).len() == out0.len() &&
+            future(out1).len() == out1.len() &&
+            future(out2).len() == out2.len() &&
+            future(out3).len() == out3.len()
+        )]
         pub fn shake256_squeeze_next_block(
             s: &mut KeccakState,
             out0: &mut [u8],
@@ -88,6 +142,18 @@ pub mod x4 {
 
         /// Squeeze three blocks
         #[inline(always)]
+        #[hax_lib::requires(
+            out0.len().to_int() >= hax_lib::int!(504) && // 3 * 168 = 504
+            out0.len() == out1.len() &&
+            out0.len() == out2.len() &&
+            out0.len() == out3.len()
+        )]
+        #[hax_lib::ensures(|_|
+            future(out0).len() == out0.len() &&
+            future(out1).len() == out1.len() &&
+            future(out2).len() == out2.len() &&
+            future(out3).len() == out3.len()
+        )]
         pub fn shake128_squeeze_first_three_blocks(
             s: &mut KeccakState,
             out0: &mut [u8],
@@ -114,6 +180,18 @@ pub mod x4 {
 
         /// Squeeze another block
         #[inline(always)]
+        #[hax_lib::requires(
+            out0.len().to_int() >= hax_lib::int!(168) &&
+            out0.len() == out1.len() &&
+            out0.len() == out2.len() &&
+            out0.len() == out3.len()
+        )]
+        #[hax_lib::ensures(|_|
+            future(out0).len() == out0.len() &&
+            future(out1).len() == out1.len() &&
+            future(out2).len() == out2.len() &&
+            future(out3).len() == out3.len()
+        )]
         pub fn shake128_squeeze_next_block(
             s: &mut KeccakState,
             out0: &mut [u8],