restored error prop

cryspen · Oct 31, 2024 · bc2b3ad · bc2b3ad
1 parent 91cefaf
commit bc2b3ad
Show file tree

Hide file tree

Showing 25 changed files with 625 additions and 1,051 deletions.
diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Arm64_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti b/libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fsti
@@ -1,5 +1,5 @@
 module Libcrux_intrinsics.Avx2_extract
-#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
 open Core
 open FStar.Mul
 

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fst
@@ -33,14 +33,6 @@ let derive_message_representative
         Libcrux_ml_dsa.Hash_functions.Portable.shake256_absorb shake
           ((let list =
                 [
-                  cast (Core.Option.impl__is_some #(t_Array u8 (sz 11))
-                        (Libcrux_ml_dsa.Pre_hash.impl_1__pre_hash_oid domain_separation_context
-                          <:
-                          Core.Option.t_Option (t_Array u8 (sz 11)))
-                      <:
-                      bool)
-                  <:
-                  u8
                 ]
               in
               FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
@@ -604,10 +596,9 @@ let sign_pre_hashed
         (Core.Option.Option_Some d
           <:
           Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) randomness
-    | Core.Result.Result_Err (Libcrux_ml_dsa.Pre_hash.DomainSeparationError_ContextTooLongError ) ->
-      Core.Result.Result_Err
-      (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError)
-      <:
+    | Core.Result.Result_Err (err) ->
+      Core.Result.Result_Err (Core.Convert.f_from err)
+        <:
       Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE)
         Libcrux_ml_dsa.Types.t_SigningError
 

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fst
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Arithmetic.fsti
@@ -3,43 +3,28 @@ module Libcrux_ml_dsa.Simd.Avx2.Arithmetic
 open Core
 open FStar.Mul
 
-val add (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val add (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val compute_hint (v_GAMMA2: i32) (low high: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure (usize & Libcrux_intrinsics.Avx2_extract.t_Vec256)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+val compute_hint (v_GAMMA2: i32) (low high: u8)
+    : Prims.Pure (usize & u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val infinity_norm_exceeds (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) (bound: i32)
+val infinity_norm_exceeds (simd_unit: u8) (bound: i32)
     : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)
 
-val subtract (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val subtract (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val shift_left_then_reduce (v_SHIFT_BY: i32) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val shift_left_then_reduce (v_SHIFT_BY: i32) (simd_unit: u8)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val to_unsigned_representatives (t: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val to_unsigned_representatives (t: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val power2round (r: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure
-      (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+val power2round (r: u8) : Prims.Pure (u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val montgomery_multiply (lhs rhs: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val montgomery_multiply (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val montgomery_multiply_by_constant (lhs: Libcrux_intrinsics.Avx2_extract.t_Vec256) (constant: i32)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val montgomery_multiply_by_constant (lhs: u8) (constant: i32)
+    : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
 
-val decompose (v_GAMMA2: i32) (r: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure
-      (Libcrux_intrinsics.Avx2_extract.t_Vec256 & Libcrux_intrinsics.Avx2_extract.t_Vec256)
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+val decompose (v_GAMMA2: i32) (r: u8) : Prims.Pure (u8 & u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val use_hint (v_GAMMA2: i32) (r hint: Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    : Prims.Pure Libcrux_intrinsics.Avx2_extract.t_Vec256 Prims.l_True (fun _ -> Prims.l_True)
+val use_hint (v_GAMMA2: i32) (r hint: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fst
@@ -3,34 +3,30 @@ module Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment
 open Core
 open FStar.Mul
 
-let serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256) =
+let serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8) =
   let serialized:t_Array u8 (sz 19) = Rust_primitives.Hax.repeat 0uy (sz 19) in
   match cast (v_OUTPUT_SIZE <: usize) <: u8 with
   | 4uy ->
-    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_2_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l
-          <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 28l 0l 28l 0l 28l 0l 28l <: u8)
     in
-    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_2_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 28l adjacent_2_combined
     in
-    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_4_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_permutevar8x32_epi32 adjacent_2_combined
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l
-          <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 0l 6l 2l 4l 0l <: u8)
     in
-    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
+    let adjacent_4_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_4_combined
     in
-    let adjacent_4_combined:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
+    let adjacent_4_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm_shuffle_epi8 adjacent_4_combined
         (Libcrux_intrinsics.Avx2_extract.mm_set_epi8 240uy 240uy 240uy 240uy 240uy 240uy 240uy 240uy
             240uy 240uy 240uy 240uy 12uy 4uy 8uy 0uy
           <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec128)
+          u8)
     in
     let serialized:t_Array u8 (sz 19) =
       Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
@@ -62,39 +58,33 @@ let serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract
         <:
         Core.Result.t_Result (t_Array u8 v_OUTPUT_SIZE) Core.Array.t_TryFromSliceError)
   | 6uy ->
-    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_2_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_sllv_epi32 simd_unit
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 26l 0l 26l 0l 26l 0l 26l
-          <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 26l 0l 26l 0l 26l 0l 26l <: u8)
     in
-    let adjacent_2_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_2_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_srli_epi64 26l adjacent_2_combined
     in
-    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_3_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_shuffle_epi8 adjacent_2_combined
         (Libcrux_intrinsics.Avx2_extract.mm256_set_epi8 (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
             (-1y) (-1y) (-1y) (-1y) (-1y) 9y 8y 1y 0y (-1y) (-1y) (-1y) (-1y) (-1y) (-1y) (-1y)
             (-1y) (-1y) (-1y) (-1y) (-1y) 9y 8y 1y 0y
           <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+          u8)
     in
-    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_3_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_mullo_epi16 adjacent_3_combined
         (Libcrux_intrinsics.Avx2_extract.mm256_set_epi16 1s 1s 1s 1s 1s 1s 1s (1s <<! 4l <: i16) 1s
             1s 1s 1s 1s 1s 1s (1s <<! 4l <: i16)
           <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
+          u8)
     in
-    let adjacent_3_combined:Libcrux_intrinsics.Avx2_extract.t_Vec256 =
+    let adjacent_3_combined:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_srlv_epi32 adjacent_3_combined
-        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 4l 0l 0l 0l 4l
-          <:
-          Libcrux_intrinsics.Avx2_extract.t_Vec256)
-    in
-    let lower_3_:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
-      Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_3_combined
+        (Libcrux_intrinsics.Avx2_extract.mm256_set_epi32 0l 0l 0l 4l 0l 0l 0l 4l <: u8)
     in
+    let lower_3_:u8 = Libcrux_intrinsics.Avx2_extract.mm256_castsi256_si128 adjacent_3_combined in
     let serialized:t_Array u8 (sz 19) =
       Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
         ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 16 }
@@ -112,7 +102,7 @@ let serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract
           <:
           t_Slice u8)
     in
-    let upper_3_:Libcrux_intrinsics.Avx2_extract.t_Vec128 =
+    let upper_3_:u8 =
       Libcrux_intrinsics.Avx2_extract.mm256_extracti128_si256 1l adjacent_3_combined
     in
     let serialized:t_Array u8 (sz 19) =

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment.fsti
@@ -3,5 +3,5 @@ module Libcrux_ml_dsa.Simd.Avx2.Encoding.Commitment
 open Core
 open FStar.Mul
 
-val serialize (v_OUTPUT_SIZE: usize) (simd_unit: Libcrux_intrinsics.Avx2_extract.t_Vec256)
+val serialize (v_OUTPUT_SIZE: usize) (simd_unit: u8)
     : Prims.Pure (t_Array u8 v_OUTPUT_SIZE) Prims.l_True (fun _ -> Prims.l_True)