Make libcrux-ml-kem lax check in F*

.github/workflows/hax.yml

@@ -40,7 +40,7 @@ jobs:
       - name: ⤵ Clone hax repository
         uses: actions/checkout@v4
         with:
-          repository: hacspec/hacspec-v2
+          repository: hacspec/hax
           path: hax
 
       - name: ⤵ Install & confiure Cachix
@@ -53,11 +53,14 @@ jobs:
           nix profile install ./hax
 
       - name: 🏃 Extract ML-KEM crate
+        working-directory: libcrux-ml-kem
+        run: ./hax.py extract
+
+      - name: 🏃 Lax ML-KEM crate
+        working-directory: libcrux-ml-kem
         run: |
-          cd libcrux-ml-kem
-          ./hax.py extract
-          # env FSTAR_HOME=${{ github.workspace }}/fstar \
-          #     HACL_HOME=${{ github.workspace }}/hacl-star \
-          #     HAX_HOME=${{ github.workspace }}/hax \
-          #     PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
-          #     ./hax.py prove --admit
+          env FSTAR_HOME=${{ github.workspace }}/fstar \
+              HACL_HOME=${{ github.workspace }}/hacl-star \
+              HAX_HOME=${{ github.workspace }}/hax \
+              PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
+              ./hax.py prove --admit

libcrux-intrinsics/Cargo.toml

@@ -17,3 +17,6 @@ simd128 = []
 simd256 = []
 
 [dev-dependencies]
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)', 'cfg(eurydice)'] }

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti

@@ -0,0 +1,160 @@
+module Libcrux_intrinsics.Arm64_extract
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+val v__vaddq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vaddq_u32 (compressed half: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vaddv_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vaddvq_s16 (a: u8) : Prims.Pure i16 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vaddvq_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vandq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vandq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vandq_u32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vbicq_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vcgeq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vcleq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vdupq_n_s16 (i: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vdupq_n_u16 (value: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vdupq_n_u32 (value: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vdupq_n_u64 (i: u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__veorq_s16 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__veorq_u64 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vget_high_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vget_low_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vget_low_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vld1q_bytes_u64 (array: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vld1q_s16 (array: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vld1q_u16 (ptr: t_Slice u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vld1q_u64 (array: t_Slice u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vld1q_u8 (ptr: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmlal_high_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmlal_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmull_high_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmull_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmulq_n_s16 (v: u8) (c: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmulq_n_u16 (v: u8) (c: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmulq_n_u32 (a: u8) (b: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vmulq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vqdmulhq_n_s16 (k: u8) (b: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vqdmulhq_n_s32 (a: u8) (b: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vqdmulhq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vqtbl1q_u8 (t idx: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s16_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s16_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s16_u16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s16_u32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s32_u32 (compressed: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s64_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_s64_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u16_s16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u32_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u8_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vreinterpretq_u8_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshlq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshlq_n_u32 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshlq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshlq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshlq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshrq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshrq_n_u16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshrq_n_u32 (v_N: i32) (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vshrq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vsliq_n_s32 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vsliq_n_s64 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vst1q_bytes_u64 (out: t_Slice u8) (v: u8)
+    : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vst1q_s16 (out: t_Slice i16) (v: u8)
+    : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vst1q_u64 (out: t_Slice u64) (v: u8)
+    : Prims.Pure (t_Slice u64) Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vst1q_u8 (out: t_Slice u8) (v: u8)
+    : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vsubq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn1q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn1q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn1q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn1q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn2q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn2q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn2q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val v__vtrn2q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti

@@ -0,0 +1,152 @@
+module Libcrux_intrinsics.Avx2_extract
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+val mm256_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_add_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_and_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_andnot_si256 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_blend_epi16 (v_CONTROL: i32) (lhs rhs: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_castsi128_si256 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_castsi256_si128 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_cmpgt_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_cvtepi16_epi32 (vector: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_extracti128_si256 (v_CONTROL: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_inserti128_si256 (v_CONTROL: i32) (vector vector_i128: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_loadu_si256_i16 (input: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_loadu_si256_u8 (input: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_madd_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_mul_epu32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_mulhi_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_mullo_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_mullo_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_packs_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_permute2x128_si256 (v_IMM8: i32) (a b: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_permute4x64_epi64 (v_CONTROL: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_permutevar8x32_epi32 (vector control: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set1_epi16 (constant: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set1_epi32 (constant: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set1_epi64x (a: i64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set_epi16
+      (input15 input14 input13 input12 input11 input10 input9 input8 input7 input6 input5 input4 input3 input2 input1 input0:
+          i16)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set_epi32 (input7 input6 input5 input4 input3 input2 input1 input0: i32)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_set_epi8
+      (byte31 byte30 byte29 byte28 byte27 byte26 byte25 byte24 byte23 byte22 byte21 byte20 byte19 byte18 byte17 byte16 byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0:
+          i8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_setzero_si256: Prims.unit -> Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_shuffle_epi32 (v_CONTROL: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_slli_epi16 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_slli_epi32 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_slli_epi64 (v_LEFT: i32) (x: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_sllv_epi32 (vector counts: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_srai_epi16 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_srai_epi32 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_srli_epi16 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_srli_epi32 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_srli_epi64 (v_SHIFT_BY: i32) (vector: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_storeu_si256_i16 (output: t_Slice i16) (vector: u8)
+    : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_storeu_si256_u8 (output: t_Slice u8) (vector: u8)
+    : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_unpackhi_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_unpackhi_epi64 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_unpacklo_epi32 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_unpacklo_epi64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm256_xor_si256 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_add_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_loadu_si128 (input: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_movemask_epi8 (vector: u8) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_mulhi_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_mullo_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_packs_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_set1_epi16 (constant: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_set_epi8
+      (byte15 byte14 byte13 byte12 byte11 byte10 byte9 byte8 byte7 byte6 byte5 byte4 byte3 byte2 byte1 byte0:
+          u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_shuffle_epi8 (vector control: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_storeu_bytes_si128 (output: t_Slice u8) (vector: u8)
+    : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_storeu_si128 (output: t_Slice i16) (vector: u8)
+    : Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)
+
+val mm_sub_epi16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)