Merge pull request #750 from cryspen/remove-double-return-workarounds

Remove double return workarounds.
cryspen · Jan 15, 2025 · 4f470c8 · 4f470c8
2 parents 195b6c6 + 8374870
commit 4f470c8
Show file tree

Hide file tree

Showing 104 changed files with 306 additions and 921 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
@@ -126,7 +126,6 @@ let decompose_vector
           (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
             t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   low, high
   <:
   (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
@@ -242,7 +241,6 @@ let power2round_vector
           (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
             t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   t, t1
   <:
   (t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
@@ -289,7 +287,6 @@ let shift_left_then_reduce
           <:
           Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   re
 
 let use_hint
@@ -372,7 +369,6 @@ let use_hint
           in
           re_vector)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   re_vector
 
 let vector_infinity_norm_exceeds

diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst
@@ -57,7 +57,6 @@ let serialize
           <:
           t_Slice u8)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   serialized
 
 let serialize_vector
@@ -110,5 +109,4 @@ let serialize_vector
           let offset:usize = offset +! ring_element_size in
           offset, serialized <: (usize & t_Slice u8))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst
@@ -65,7 +65,6 @@ let deserialize
           <:
           Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   result
 
 let deserialize_to_vector_then_ntt
@@ -117,7 +116,6 @@ let deserialize_to_vector_then_ntt
           in
           ring_elements)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   ring_elements
 
 let serialize
@@ -168,5 +166,4 @@ let serialize
           <:
           t_Slice u8)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst
@@ -61,7 +61,7 @@ let deserialize
           <:
           Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
+  let _:Prims.unit = () <: Prims.unit in
   result
 
 let serialize
@@ -113,5 +113,5 @@ let serialize
           <:
           t_Slice u8)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
+  let _:Prims.unit = () <: Prims.unit in
   serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst
@@ -10,8 +10,7 @@ let _ =
   ()
 
 let set_hint (out_hint: t_Slice (t_Array i32 (sz 256))) (i j: usize) =
-  let hax_temp_output, out_hint:(Prims.unit & t_Slice (t_Array i32 (sz 256))) =
-    (),
+  let out_hint:t_Slice (t_Array i32 (sz 256)) =
     Rust_primitives.Hax.Monomorphized_update_at.update_at_usize out_hint
       i
       (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (out_hint.[ i ]
@@ -21,8 +20,6 @@ let set_hint (out_hint: t_Slice (t_Array i32 (sz 256))) (i j: usize) =
           1l
         <:
         t_Array i32 (sz 256))
-    <:
-    (Prims.unit & t_Slice (t_Array i32 (sz 256)))
   in
   out_hint
 
@@ -467,5 +464,4 @@ let serialize
           in
           signature, true_hints_seen <: (t_Slice u8 & usize))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   signature
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst
@@ -186,5 +186,4 @@ let generate_serialized
           let offset:usize = offset +! Libcrux_ml_dsa.Constants.v_RING_ELEMENT_OF_T0S_SIZE in
           offset, signing_key_serialized <: (usize & t_Slice u8))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   signing_key_serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst
@@ -59,7 +59,6 @@ let deserialize
           <:
           Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   result
 
 let deserialize_to_vector_then_ntt
@@ -108,7 +107,6 @@ let deserialize_to_vector_then_ntt
           in
           ring_elements)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   ring_elements
 
 let serialize
@@ -156,5 +154,4 @@ let serialize
           <:
           t_Slice u8)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   serialized
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
@@ -57,7 +57,6 @@ let deserialize
           <:
           Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   result
 
 let serialize
@@ -107,5 +106,4 @@ let serialize
           <:
           t_Slice u8)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst
@@ -63,7 +63,6 @@ let deserialize
           <:
           t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   t1
 
 let generate_serialized
@@ -140,5 +139,4 @@ let generate_serialized
           in
           verification_key_serialized)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   verification_key_serialized
diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst
@@ -53,7 +53,6 @@ let vector_times_ring_element
           in
           vector)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   vector
 
 let add_vectors
@@ -85,7 +84,6 @@ let add_vectors
           <:
           t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   lhs
 
 let compute_as1_plus_s2
@@ -187,7 +185,6 @@ let compute_as1_plus_s2
           in
           result)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   result
 
 let compute_matrix_x_mask
@@ -264,7 +261,6 @@ let compute_matrix_x_mask
           in
           result)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   result
 
 let compute_w_approx
@@ -366,7 +362,6 @@ let compute_w_approx
           in
           t1)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   t1
 
 let subtract_vectors
@@ -398,5 +393,4 @@ let subtract_vectors
           <:
           t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
   lhs
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
@@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification
   in
   let signing_key:t_Slice u8 = tmp0 in
   let verification_key:t_Slice u8 = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Slice u8 & t_Slice u8)
 
 let sign___inner

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
@@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification
   in
   let signing_key:t_Slice u8 = tmp0 in
   let verification_key:t_Slice u8 = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Slice u8 & t_Slice u8)
 
 let sign___inner

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst
@@ -43,7 +43,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) (signing_key verification
   in
   let signing_key:t_Slice u8 = tmp0 in
   let verification_key:t_Slice u8 = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Slice u8 & t_Slice u8)
 
 let sign___inner

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst
@@ -35,7 +35,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 2560) = tmp0 in
   let verification_key:t_Array u8 (sz 1312) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
 
 let sign

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst
@@ -35,7 +35,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 4032) = tmp0 in
   let verification_key:t_Array u8 (sz 1952) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))
 
 let sign

diff --git a/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst b/.../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst
@@ -35,7 +35,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 4896) = tmp0 in
   let verification_key:t_Array u8 (sz 2592) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592))
 
 let sign

diff --git a/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst b/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst
@@ -34,7 +34,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 2560) = tmp0 in
   let verification_key:t_Array u8 (sz 1312) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
 
 let sign

diff --git a/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst b/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst
@@ -34,7 +34,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 4032) = tmp0 in
   let verification_key:t_Array u8 (sz 1952) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))
 
 let sign

diff --git a/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst b/...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst
@@ -34,7 +34,7 @@ let generate_key_pair
   in
   let signing_key:t_Array u8 (sz 4896) = tmp0 in
   let verification_key:t_Array u8 (sz 2592) = tmp1 in
-  let hax_temp_output:Prims.unit = () in
+  let _:Prims.unit = () in
   signing_key, verification_key <: (t_Array u8 (sz 4896) & t_Array u8 (sz 2592))
 
 let sign

diff --git a/...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst b/...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst
@@ -8,9 +8,7 @@ let generate_key_pair
       (signing_key: t_Array u8 (sz 2560))
       (verification_key: t_Array u8 (sz 1312))
      =
-  let (signing_key, verification_key), hax_temp_output:((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)
-    ) &
-    Prims.unit) =
+  let signing_key, verification_key:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) =
     if Libcrux_platform.Platform.simd256_support ()
     then
       let tmp0, tmp1:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) =
@@ -21,9 +19,7 @@ let generate_key_pair
       let signing_key:t_Array u8 (sz 2560) = tmp0 in
       let verification_key:t_Array u8 (sz 1312) = tmp1 in
       let _:Prims.unit = () in
-      (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), ()
-      <:
-      ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit)
+      signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
     else
       if Libcrux_platform.Platform.simd128_support ()
       then
@@ -35,9 +31,7 @@ let generate_key_pair
         let signing_key:t_Array u8 (sz 2560) = tmp0 in
         let verification_key:t_Array u8 (sz 1312) = tmp1 in
         let _:Prims.unit = () in
-        (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), ()
-        <:
-        ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit)
+        signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
       else
         let tmp0, tmp1:(t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) =
           Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.generate_key_pair randomness
@@ -47,9 +41,7 @@ let generate_key_pair
         let signing_key:t_Array u8 (sz 2560) = tmp0 in
         let verification_key:t_Array u8 (sz 1312) = tmp1 in
         let _:Prims.unit = () in
-        (signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))), ()
-        <:
-        ((t_Array u8 (sz 2560) & t_Array u8 (sz 1312)) & Prims.unit)
+        signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
   in
   signing_key, verification_key <: (t_Array u8 (sz 2560) & t_Array u8 (sz 1312))
 

diff --git a/...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst b/...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst
@@ -8,9 +8,7 @@ let generate_key_pair
       (signing_key: t_Array u8 (sz 4032))
       (verification_key: t_Array u8 (sz 1952))
      =
-  let (signing_key, verification_key), hax_temp_output:((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)
-    ) &
-    Prims.unit) =
+  let signing_key, verification_key:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) =
     if Libcrux_platform.Platform.simd256_support ()
     then
       let tmp0, tmp1:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) =
@@ -21,9 +19,7 @@ let generate_key_pair
       let signing_key:t_Array u8 (sz 4032) = tmp0 in
       let verification_key:t_Array u8 (sz 1952) = tmp1 in
       let _:Prims.unit = () in
-      (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), ()
-      <:
-      ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit)
+      signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))
     else
       if Libcrux_platform.Platform.simd128_support ()
       then
@@ -35,9 +31,7 @@ let generate_key_pair
         let signing_key:t_Array u8 (sz 4032) = tmp0 in
         let verification_key:t_Array u8 (sz 1952) = tmp1 in
         let _:Prims.unit = () in
-        (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), ()
-        <:
-        ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit)
+        signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))
       else
         let tmp0, tmp1:(t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) =
           Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.generate_key_pair randomness
@@ -47,9 +41,7 @@ let generate_key_pair
         let signing_key:t_Array u8 (sz 4032) = tmp0 in
         let verification_key:t_Array u8 (sz 1952) = tmp1 in
         let _:Prims.unit = () in
-        (signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))), ()
-        <:
-        ((t_Array u8 (sz 4032) & t_Array u8 (sz 1952)) & Prims.unit)
+        signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))
   in
   signing_key, verification_key <: (t_Array u8 (sz 4032) & t_Array u8 (sz 1952))