Update F* output with latest hax (after merging new naming).

cryspen · Jan 30, 2025 · 9f8e772 · 9f8e772
1 parent 0ca79fc
commit 9f8e772
Show file tree

Hide file tree

Showing 100 changed files with 1,628 additions and 1,620 deletions.
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst
@@ -435,7 +435,7 @@ let make_hint
   let hax_temp_output:usize = true_hints in
   hint, hax_temp_output <: (t_Slice (t_Array i32 (mk_usize 256)) & usize)
 
-let use_hint
+let uuse_hint
       (#v_SIMDUnit: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
           i1:
@@ -493,7 +493,7 @@ let use_hint
                     Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp
                         .Libcrux_ml_dsa.Polynomial.f_simd_units
                       j
-                      (Libcrux_ml_dsa.Simd.Traits.f_use_hint #v_SIMDUnit
+                      (Libcrux_ml_dsa.Simd.Traits.f_uuse_hint #v_SIMDUnit
                           #FStar.Tactics.Typeclasses.solve
                           gamma2
                           ((re_vector.[ i ]

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fsti
@@ -55,7 +55,7 @@ val make_hint
       (hint: t_Slice (t_Array i32 (mk_usize 256)))
     : Prims.Pure (t_Slice (t_Array i32 (mk_usize 256)) & usize) Prims.l_True (fun _ -> Prims.l_True)
 
-val use_hint
+val uuse_hint
       (#v_SIMDUnit: Type0)
       {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
       (gamma2: i32)

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fst
@@ -5,8 +5,8 @@ open FStar.Mul
 
 let t_Eta_cast_to_repr (x: t_Eta) =
   match x <: t_Eta with
-  | Eta_Two  -> discriminant_Eta_Two
-  | Eta_Four  -> discriminant_Eta_Four
+  | Eta_Two  -> anon_const_Eta_Two__anon_const_0
+  | Eta_Four  -> anon_const_Eta_Four__anon_const_0
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 assume

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fsti
@@ -48,9 +48,9 @@ type t_Eta =
   | Eta_Two : t_Eta
   | Eta_Four : t_Eta
 
-let discriminant_Eta_Two: isize = mk_isize 2
+let anon_const_Eta_Two__anon_const_0: isize = mk_isize 2
 
-let discriminant_Eta_Four: isize = mk_isize 4
+let anon_const_Eta_Four__anon_const_0: isize = mk_isize 4
 
 val t_Eta_cast_to_repr (x: t_Eta) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True)
 

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst
@@ -31,21 +31,21 @@ let serialize
           let i, simd_unit:(usize & v_SIMDUnit) = temp_1_ in
           Rust_primitives.Hax.Monomorphized_update_at.update_at_range serialized
             ({
-                Core.Ops.Range.f_start = i *! serialize__OUTPUT_BYTES_PER_SIMD_UNIT <: usize;
+                Core.Ops.Range.f_start = i *! serialize__v_OUTPUT_BYTES_PER_SIMD_UNIT <: usize;
                 Core.Ops.Range.f_end
                 =
-                (i +! mk_usize 1 <: usize) *! serialize__OUTPUT_BYTES_PER_SIMD_UNIT <: usize
+                (i +! mk_usize 1 <: usize) *! serialize__v_OUTPUT_BYTES_PER_SIMD_UNIT <: usize
               }
               <:
               Core.Ops.Range.t_Range usize)
             (Libcrux_ml_dsa.Simd.Traits.f_t1_serialize #v_SIMDUnit
                 #FStar.Tactics.Typeclasses.solve
                 simd_unit
                 (serialized.[ {
-                      Core.Ops.Range.f_start = i *! serialize__OUTPUT_BYTES_PER_SIMD_UNIT <: usize;
+                      Core.Ops.Range.f_start = i *! serialize__v_OUTPUT_BYTES_PER_SIMD_UNIT <: usize;
                       Core.Ops.Range.f_end
                       =
-                      (i +! mk_usize 1 <: usize) *! serialize__OUTPUT_BYTES_PER_SIMD_UNIT <: usize
+                      (i +! mk_usize 1 <: usize) *! serialize__v_OUTPUT_BYTES_PER_SIMD_UNIT <: usize
                     }
                     <:
                     Core.Ops.Range.t_Range usize ]
@@ -90,10 +90,10 @@ let deserialize
               (Libcrux_ml_dsa.Simd.Traits.f_t1_deserialize #v_SIMDUnit
                   #FStar.Tactics.Typeclasses.solve
                   (serialized.[ {
-                        Core.Ops.Range.f_start = i *! deserialize__WINDOW <: usize;
+                        Core.Ops.Range.f_start = i *! deserialize__v_WINDOW <: usize;
                         Core.Ops.Range.f_end
                         =
-                        (i +! mk_usize 1 <: usize) *! deserialize__WINDOW <: usize
+                        (i +! mk_usize 1 <: usize) *! deserialize__v_WINDOW <: usize
                       }
                       <:
                       Core.Ops.Range.t_Range usize ]

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fsti
@@ -9,7 +9,7 @@ let _ =
   let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
-let serialize__OUTPUT_BYTES_PER_SIMD_UNIT: usize = mk_usize 10
+let serialize__v_OUTPUT_BYTES_PER_SIMD_UNIT: usize = mk_usize 10
 
 val serialize
       (#v_SIMDUnit: Type0)
@@ -18,7 +18,7 @@ val serialize
       (serialized: t_Slice u8)
     : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-let deserialize__WINDOW: usize = mk_usize 10
+let deserialize__v_WINDOW: usize = mk_usize 10
 
 val deserialize
       (#v_SIMDUnit: Type0)

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst
@@ -17,7 +17,7 @@ let _ =
   let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
-let generate_key_pair___inner
+let generate_key_pair__e_inner
       (randomness: t_Array u8 (mk_usize 32))
       (signing_key verification_key: t_Slice u8)
      =
@@ -42,14 +42,14 @@ let generate_key_pair
       (signing_key verification_key: t_Slice u8)
      =
   let tmp0, tmp1:(t_Slice u8 & t_Slice u8) =
-    generate_key_pair___inner randomness signing_key verification_key
+    generate_key_pair__e_inner randomness signing_key verification_key
   in
   let signing_key:t_Slice u8 = tmp0 in
   let verification_key:t_Slice u8 = tmp1 in
   let _:Prims.unit = () in
   signing_key, verification_key <: (t_Slice u8 & t_Slice u8)
 
-let sign___inner
+let sign__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -65,9 +65,9 @@ let sign
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
-     = sign___inner signing_key message context randomness
+     = sign__e_inner signing_key message context randomness
 
-let sign_mut___inner
+let sign_mut__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -97,15 +97,15 @@ let sign_mut
      =
   let tmp0, out:(t_Array u8 (mk_usize 2420) &
     Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError) =
-    sign_mut___inner signing_key message context randomness signature
+    sign_mut__e_inner signing_key message context randomness signature
   in
   let signature:t_Array u8 (mk_usize 2420) = tmp0 in
   let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError = out in
   signature, hax_temp_output
   <:
   (t_Array u8 (mk_usize 2420) & Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError)
 
-let sign_pre_hashed_shake128___inner
+let sign_pre_hashed_shake128__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context pre_hash_buffer: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -140,7 +140,7 @@ let sign_pre_hashed_shake128
   let tmp0, out:(t_Slice u8 &
     Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 2420))
       Libcrux_ml_dsa.Types.t_SigningError) =
-    sign_pre_hashed_shake128___inner signing_key message context pre_hash_buffer randomness
+    sign_pre_hashed_shake128__e_inner signing_key message context pre_hash_buffer randomness
   in
   let pre_hash_buffer:t_Slice u8 = tmp0 in
   let hax_temp_output:Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 2420))
@@ -153,7 +153,7 @@ let sign_pre_hashed_shake128
     Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 2420))
       Libcrux_ml_dsa.Types.t_SigningError)
 
-let verify___inner
+let verify__e_inner
       (verification_key: t_Array u8 (mk_usize 1312))
       (message context: t_Slice u8)
       (signature: t_Array u8 (mk_usize 2420))
@@ -172,9 +172,9 @@ let verify
       (verification_key: t_Array u8 (mk_usize 1312))
       (message context: t_Slice u8)
       (signature: t_Array u8 (mk_usize 2420))
-     = verify___inner verification_key message context signature
+     = verify__e_inner verification_key message context signature
 
-let verify_pre_hashed_shake128___inner
+let verify_pre_hashed_shake128__e_inner
       (verification_key: t_Array u8 (mk_usize 1312))
       (message context pre_hash_buffer: t_Slice u8)
       (signature: t_Array u8 (mk_usize 2420))
@@ -203,7 +203,7 @@ let verify_pre_hashed_shake128
      =
   let tmp0, out:(t_Slice u8 &
     Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
-    verify_pre_hashed_shake128___inner verification_key message context pre_hash_buffer signature
+    verify_pre_hashed_shake128__e_inner verification_key message context pre_hash_buffer signature
   in
   let pre_hash_buffer:t_Slice u8 = tmp0 in
   let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError =

diff --git a/...proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fsti b/...proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fsti
@@ -18,7 +18,7 @@ let _ =
   ()
 
 /// Key Generation.
-val generate_key_pair___inner
+val generate_key_pair__e_inner
       (randomness: t_Array u8 (mk_usize 32))
       (signing_key verification_key: t_Slice u8)
     : Prims.Pure (t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
@@ -28,7 +28,7 @@ val generate_key_pair
       (signing_key verification_key: t_Slice u8)
     : Prims.Pure (t_Slice u8 & t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)
 
-val sign___inner
+val sign__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -45,7 +45,7 @@ val sign
       (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 2420))
           Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True)
 
-val sign_mut___inner
+val sign_mut__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -68,7 +68,7 @@ val sign_mut
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val sign_pre_hashed_shake128___inner
+val sign_pre_hashed_shake128__e_inner
       (signing_key: t_Array u8 (mk_usize 2560))
       (message context pre_hash_buffer: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -87,7 +87,7 @@ val sign_pre_hashed_shake128
         Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 2420))
           Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True)
 
-val verify___inner
+val verify__e_inner
       (verification_key: t_Array u8 (mk_usize 1312))
       (message context: t_Slice u8)
       (signature: t_Array u8 (mk_usize 2420))
@@ -104,7 +104,7 @@ val verify
       Prims.l_True
       (fun _ -> Prims.l_True)
 
-val verify_pre_hashed_shake128___inner
+val verify_pre_hashed_shake128__e_inner
       (verification_key: t_Array u8 (mk_usize 1312))
       (message context pre_hash_buffer: t_Slice u8)
       (signature: t_Array u8 (mk_usize 2420))

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst
@@ -17,7 +17,7 @@ let _ =
   let open Libcrux_ml_dsa.Simd.Traits in
   ()
 
-let generate_key_pair___inner
+let generate_key_pair__e_inner
       (randomness: t_Array u8 (mk_usize 32))
       (signing_key verification_key: t_Slice u8)
      =
@@ -42,14 +42,14 @@ let generate_key_pair
       (signing_key verification_key: t_Slice u8)
      =
   let tmp0, tmp1:(t_Slice u8 & t_Slice u8) =
-    generate_key_pair___inner randomness signing_key verification_key
+    generate_key_pair__e_inner randomness signing_key verification_key
   in
   let signing_key:t_Slice u8 = tmp0 in
   let verification_key:t_Slice u8 = tmp1 in
   let _:Prims.unit = () in
   signing_key, verification_key <: (t_Slice u8 & t_Slice u8)
 
-let sign___inner
+let sign__e_inner
       (signing_key: t_Array u8 (mk_usize 4032))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -65,9 +65,9 @@ let sign
       (signing_key: t_Array u8 (mk_usize 4032))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
-     = sign___inner signing_key message context randomness
+     = sign__e_inner signing_key message context randomness
 
-let sign_mut___inner
+let sign_mut__e_inner
       (signing_key: t_Array u8 (mk_usize 4032))
       (message context: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -97,15 +97,15 @@ let sign_mut
      =
   let tmp0, out:(t_Array u8 (mk_usize 3309) &
     Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError) =
-    sign_mut___inner signing_key message context randomness signature
+    sign_mut__e_inner signing_key message context randomness signature
   in
   let signature:t_Array u8 (mk_usize 3309) = tmp0 in
   let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError = out in
   signature, hax_temp_output
   <:
   (t_Array u8 (mk_usize 3309) & Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_SigningError)
 
-let sign_pre_hashed_shake128___inner
+let sign_pre_hashed_shake128__e_inner
       (signing_key: t_Array u8 (mk_usize 4032))
       (message context pre_hash_buffer: t_Slice u8)
       (randomness: t_Array u8 (mk_usize 32))
@@ -140,7 +140,7 @@ let sign_pre_hashed_shake128
   let tmp0, out:(t_Slice u8 &
     Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 3309))
       Libcrux_ml_dsa.Types.t_SigningError) =
-    sign_pre_hashed_shake128___inner signing_key message context pre_hash_buffer randomness
+    sign_pre_hashed_shake128__e_inner signing_key message context pre_hash_buffer randomness
   in
   let pre_hash_buffer:t_Slice u8 = tmp0 in
   let hax_temp_output:Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 3309))
@@ -153,7 +153,7 @@ let sign_pre_hashed_shake128
     Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (mk_usize 3309))
       Libcrux_ml_dsa.Types.t_SigningError)
 
-let verify___inner
+let verify__e_inner
       (verification_key: t_Array u8 (mk_usize 1952))
       (message context: t_Slice u8)
       (signature: t_Array u8 (mk_usize 3309))
@@ -172,9 +172,9 @@ let verify
       (verification_key: t_Array u8 (mk_usize 1952))
       (message context: t_Slice u8)
       (signature: t_Array u8 (mk_usize 3309))
-     = verify___inner verification_key message context signature
+     = verify__e_inner verification_key message context signature
 
-let verify_pre_hashed_shake128___inner
+let verify_pre_hashed_shake128__e_inner
       (verification_key: t_Array u8 (mk_usize 1952))
       (message context pre_hash_buffer: t_Slice u8)
       (signature: t_Array u8 (mk_usize 3309))
@@ -203,7 +203,7 @@ let verify_pre_hashed_shake128
      =
   let tmp0, out:(t_Slice u8 &
     Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
-    verify_pre_hashed_shake128___inner verification_key message context pre_hash_buffer signature
+    verify_pre_hashed_shake128__e_inner verification_key message context pre_hash_buffer signature
   in
   let pre_hash_buffer:t_Slice u8 = tmp0 in
   let hax_temp_output:Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError =