Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove double return workarounds. #750

Merged
merged 3 commits into from
Jan 15, 2025
+306 −921
Merged

Remove double return workarounds. #750

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8619341
Remove double return workarounds.
maximebuyse Jan 15, 2025
508e6fc
Merge branch 'main' into remove-double-return-workarounds
franziskuskiefer Jan 15, 2025
8374870
Re-generate F* without double return workaround.
maximebuyse Jan 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 0 additions & 4 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) &
Expand Down Expand Up @@ -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) &
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 0 additions & 2 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Commitment.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ let serialize
<:
t_Slice u8)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
serialized

let serialize_vector
Expand Down Expand Up @@ -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
3 changes: 0 additions & 3 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Error.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -168,5 +166,4 @@ let serialize
<:
t_Slice u8)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
serialized
4 changes: 2 additions & 2 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Gamma1.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
6 changes: 1 addition & 5 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ]
Expand All @@ -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

Expand Down Expand Up @@ -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
1 change: 0 additions & 1 deletion libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signing_key.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
3 changes: 0 additions & 3 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T0.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -156,5 +154,4 @@ let serialize
<:
t_Slice u8)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
serialized
2 changes: 0 additions & 2 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.T1.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -107,5 +106,4 @@ let serialize
<:
t_Slice u8)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
serialized
2 changes: 0 additions & 2 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Verification_key.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -140,5 +139,4 @@ let generate_serialized
in
verification_key_serialized)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
verification_key_serialized
6 changes: 0 additions & 6 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Matrix.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -366,7 +362,6 @@ let compute_w_approx
in
t1)
in
let hax_temp_output:Prims.unit = () <: Prims.unit in
t1

let subtract_vectors
Expand Down Expand Up @@ -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
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_65_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_87_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_65_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion .../proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_87_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_65_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion ...ofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_87_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
16 changes: 4 additions & 12 deletions ...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) =
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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))

Expand Down
16 changes: 4 additions & 12 deletions ...-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_65_.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) =
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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))

Expand Down
Loading
Loading