From a9714a49b61929b267e95bbf799c0c0a8ac8a5b1 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Wed, 18 Dec 2024 12:13:53 +0100 Subject: [PATCH] Update hax extraction --- .../Libcrux_ml_dsa.Encoding.Signature.fst | 2 +- .../Libcrux_ml_dsa.Encoding.Signature.fsti | 2 +- .../Libcrux_ml_dsa.Hash_functions.Neon.fsti | 4 +- ...ibcrux_ml_dsa.Hash_functions.Portable.fsti | 10 +- ...Libcrux_ml_dsa.Hash_functions.Simd256.fsti | 10 +- .../Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst | 12 +- .../extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst | 12 +- .../extraction/Libcrux_ml_dsa.Ml_dsa_65_.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_87_.Avx2.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_87_.Neon.fst | 12 +- .../Libcrux_ml_dsa.Ml_dsa_87_.Portable.fst | 12 +- .../extraction/Libcrux_ml_dsa.Ml_dsa_87_.fst | 12 +- ...neric.Instantiations.Avx2.Avx2_feature.fst | 12 +- ...eric.Instantiations.Avx2.Avx2_feature.fsti | 2 + ...dsa.Ml_dsa_generic.Instantiations.Neon.fst | 12 +- ...sa.Ml_dsa_generic.Instantiations.Neon.fsti | 2 + ...Ml_dsa_generic.Instantiations.Portable.fst | 7 + ...l_dsa_generic.Instantiations.Portable.fsti | 2 + .../Libcrux_ml_dsa.Ml_dsa_generic.fst | 812 ++++---- .../Libcrux_ml_dsa.Ml_dsa_generic.fsti | 179 +- .../extraction/Libcrux_ml_dsa.Polynomial.fst | 42 +- .../extraction/Libcrux_ml_dsa.Polynomial.fsti | 24 +- .../extraction/Libcrux_ml_dsa.Sample.fst | 735 +++---- .../extraction/Libcrux_ml_dsa.Sample.fsti | 45 +- .../extraction/Libcrux_ml_dsa.Samplex4.fst | 1681 +++++++++-------- .../extraction/Libcrux_ml_dsa.Samplex4.fsti | 67 +- .../Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst | 12 + .../Libcrux_ml_dsa.Simd.Avx2.Vector_type.fsti | 6 + ...bcrux_ml_dsa.Simd.Portable.Vector_type.fst | 12 + ...crux_ml_dsa.Simd.Portable.Vector_type.fsti | 6 + .../fstar/extraction/Libcrux_ml_dsa.Types.fst | 36 +- .../extraction/Libcrux_ml_dsa.Types.fsti | 21 +- .../extraction/Libcrux_platform.X86.fsti | 6 + 38 files changed, 2063 insertions(+), 1830 deletions(-) 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 index 096a14a68..c351af8bb 100644 --- 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 @@ -14,7 +14,7 @@ let impl__deserialize (v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_MAX_ONES_IN_HINT v_SIGNATURE_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (serialized: t_Array u8 v_SIGNATURE_SIZE) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti index 0ef8c6563..53b1e72ed 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Encoding.Signature.fsti @@ -25,7 +25,7 @@ val impl__deserialize (#v_SIMDUnit: Type0) (v_COMMITMENT_HASH_SIZE v_COLUMNS_IN_A v_ROWS_IN_A v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_MAX_ONES_IN_HINT v_SIGNATURE_SIZE: usize) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (serialized: t_Array u8 v_SIGNATURE_SIZE) : Prims.Pure (Core.Result.t_Result diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti index a7762dfe1..d27a20455 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Neon.fsti @@ -3,10 +3,10 @@ module Libcrux_ml_dsa.Hash_functions.Neon open Core open FStar.Mul -val t_Shake128x4:Type0 +val t_Shake128x4:eqtype /// Neon SHAKE 256 x4 state -val t_Shake256x4:Type0 +val t_Shake256x4:eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti index b2a04571e..0b7e313f7 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Portable.fsti @@ -4,20 +4,20 @@ open Core open FStar.Mul /// Portable SHAKE 128 state -val t_Shake128:Type0 +val t_Shake128:eqtype /// Portable SHAKE 128 x4 state. /// We\'re using a portable implementation so this is actually sequential. -val t_Shake128X4:Type0 +val t_Shake128X4:eqtype /// Portable SHAKE 256 state -val t_Shake256:Type0 +val t_Shake256:eqtype /// Portable SHAKE 256 x4 state. /// We\'re using a portable implementation so this is actually sequential. -val t_Shake256X4:Type0 +val t_Shake256X4:eqtype -val t_Shake256Xof:Type0 +val t_Shake256Xof:eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128X4 diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti index c40649c70..109c7ccf9 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Hash_functions.Simd256.fsti @@ -6,13 +6,13 @@ open FStar.Mul /// AVX2 SHAKE 128 state /// This only implements the XofX4 API. For the single Xof, the portable /// version is used. -val t_Shake128x4:Type0 - -/// AVX2 SHAKE 256 x4 state. -val t_Shake256x4:Type0 +val t_Shake128x4:eqtype /// AVX2 SHAKE 256 state -val t_Shake256:Type0 +val t_Shake256:eqtype + +/// AVX2 SHAKE 256 x4 state. +val t_Shake256x4:eqtype [@@ FStar.Tactics.Typeclasses.tcinstance] val impl:Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 t_Shake128x4 diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst index 57daef3c6..c923aaf46 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Avx2.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify_pre_hashed_shake128 (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst index 881529d16..cbfcb41f1 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Neon.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify_pre_hashed_shake128 (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst index 47feb8acb..5ecf58ac3 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.Portable.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) - (sz 2420) (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) + (sz 2420) (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify_pre_hashed_shake128 (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst index de9e24809..fd9368339 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_44_.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign_pre_hashed_shake128 (sz 4) (sz 4) (sz 2) (sz 96) (sz 17) 95232l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) (sz 576) (sz 2560) (sz 2420) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 2560) signing_key <: t_Array u8 (sz 2560)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 2560) signing_key <: t_Array u8 (sz 2560)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify_pre_hashed_shake128 (sz 4) (sz 4) (sz 2420) (sz 1312) (sz 17) (sz 576) 95232l 78l (sz 192) (sz 768) (sz 32) (sz 39) (sz 80) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1312) verification_key <: t_Array u8 (sz 1312)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 2420) signature <: t_Array u8 (sz 2420)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1312) verification_key <: t_Array u8 (sz 1312)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst index 93a4a47d2..fb56ab400 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Avx2.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify_pre_hashed_shake128 (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst index 52cd13c55..06692d1d7 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Neon.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify_pre_hashed_shake128 (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst index 272c8f309..d696b883f 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.Portable.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) - (sz 3309) (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) + (sz 3309) (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify_pre_hashed_shake128 (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.fst index 47f6598f5..9029cf9f8 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_65_.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign_pre_hashed_shake128 (sz 6) (sz 5) (sz 4) (sz 128) (sz 19) 261888l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) (sz 640) (sz 4032) (sz 3309) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4032) signing_key <: t_Array u8 (sz 4032)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4032) signing_key <: t_Array u8 (sz 4032)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1952)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify_pre_hashed_shake128 (sz 6) (sz 5) (sz 3309) (sz 1952) (sz 19) (sz 640) 261888l 196l (sz 128) (sz 768) (sz 48) (sz 49) (sz 55) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 1952) verification_key <: t_Array u8 (sz 1952)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 3309) signature <: t_Array u8 (sz 3309)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 1952) verification_key <: t_Array u8 (sz 1952)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 3309) signature <: t_Array u8 (sz 3309)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Avx2.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Avx2.fst index a5cb7cc82..bed872537 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Avx2.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Avx2.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.sign_pre_hashed_shake128 (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 2592)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.verify_pre_hashed_shake128 (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Neon.fst index bec5c242e..f4bc8340a 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Neon.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Neon.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.sign_pre_hashed_shake128 (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 2592)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.verify_pre_hashed_shake128 (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Portable.fst index a5b4a3a2a..6f6364908 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.Portable.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.sign_pre_hashed_shake128 (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) - (sz 4627) (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) + (sz 4627) (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 2592)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.verify_pre_hashed_shake128 (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.fst index b7bfad8f1..a72c5865b 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_87_.fst @@ -29,7 +29,7 @@ let sign = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let sign_pre_hashed_shake128 @@ -39,7 +39,7 @@ let sign_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.sign_pre_hashed_shake128 (sz 8) (sz 7) (sz 2) (sz 96) (sz 19) 261888l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) (sz 640) (sz 4896) (sz 4627) - (Libcrux_ml_dsa.Types.impl__as_raw (sz 4896) signing_key <: t_Array u8 (sz 4896)) message + (Libcrux_ml_dsa.Types.impl__as_ref (sz 4896) signing_key <: t_Array u8 (sz 4896)) message context randomness let verify @@ -49,8 +49,8 @@ let verify = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) let verify_pre_hashed_shake128 (verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 2592)) @@ -59,5 +59,5 @@ let verify_pre_hashed_shake128 = Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.verify_pre_hashed_shake128 (sz 8) (sz 7) (sz 4627) (sz 2592) (sz 19) (sz 640) 261888l 120l (sz 128) (sz 1024) (sz 64) (sz 60) (sz 75) - (Libcrux_ml_dsa.Types.impl_2__as_raw (sz 2592) verification_key <: t_Array u8 (sz 2592)) message - context (Libcrux_ml_dsa.Types.impl_4__as_raw (sz 4627) signature <: t_Array u8 (sz 4627)) + (Libcrux_ml_dsa.Types.impl_2__as_ref (sz 2592) verification_key <: t_Array u8 (sz 2592)) message + context (Libcrux_ml_dsa.Types.impl_4__as_ref (sz 4627) signature <: t_Array u8 (sz 4627)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst index 3ae7a4680..c1553434f 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst @@ -11,6 +11,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Hash_functions.Simd256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Avx2 in let open Libcrux_ml_dsa.Simd.Avx2 in let open Libcrux_ml_dsa.Simd.Traits in () @@ -21,7 +23,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.generate_key_pair #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit - #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Avx2.t_AVX2Sampler #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA @@ -37,7 +39,7 @@ let sign (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit - #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Avx2.t_AVX2Sampler #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA @@ -56,7 +58,7 @@ let sign_pre_hashed_shake128 (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit - #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 + #Libcrux_ml_dsa.Samplex4.Avx2.t_AVX2Sampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof @@ -77,7 +79,7 @@ let verify (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit - #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Avx2.t_AVX2Sampler #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 @@ -95,7 +97,7 @@ let verify_pre_hashed_shake128 (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify_pre_hashed #Libcrux_ml_dsa.Simd.Avx2.Vector_type.t_AVX2SIMDUnit - #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 + #Libcrux_ml_dsa.Samplex4.Avx2.t_AVX2Sampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti index d24fb5ad1..aaa4d5643 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti @@ -11,6 +11,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Hash_functions.Simd256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Avx2 in let open Libcrux_ml_dsa.Simd.Avx2 in let open Libcrux_ml_dsa.Simd.Traits in () diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fst index bc44352c6..c81b51ec3 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fst @@ -11,6 +11,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Neon in let open Libcrux_ml_dsa.Simd.Portable in let open Libcrux_ml_dsa.Simd.Traits in () @@ -21,7 +23,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.generate_key_pair #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit - #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Neon.t_NeonSampler #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA @@ -37,7 +39,7 @@ let sign (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit - #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Neon.t_NeonSampler #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA @@ -56,7 +58,7 @@ let sign_pre_hashed_shake128 (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign_pre_hashed #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit - #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 + #Libcrux_ml_dsa.Samplex4.Neon.t_NeonSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof @@ -77,7 +79,7 @@ let verify (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit - #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 + #Libcrux_ml_dsa.Samplex4.Neon.t_NeonSampler #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 @@ -95,7 +97,7 @@ let verify_pre_hashed_shake128 (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify_pre_hashed #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit - #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 + #Libcrux_ml_dsa.Samplex4.Neon.t_NeonSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Neon.t_Shake128x4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fsti index 93c40dc34..45fac8db0 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.fsti @@ -11,6 +11,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Neon in let open Libcrux_ml_dsa.Simd.Portable in let open Libcrux_ml_dsa.Simd.Traits in () diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fst index 581a147b8..fba006d14 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fst @@ -10,6 +10,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Portable in let open Libcrux_ml_dsa.Simd.Portable in let open Libcrux_ml_dsa.Simd.Traits in () @@ -20,6 +22,7 @@ let generate_key_pair (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.generate_key_pair #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit + #Libcrux_ml_dsa.Samplex4.Portable.t_PortableSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof @@ -36,6 +39,7 @@ let sign (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit + #Libcrux_ml_dsa.Samplex4.Portable.t_PortableSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof @@ -55,6 +59,7 @@ let sign_pre_hashed_shake128 (randomness: t_Array u8 (sz 32)) = Libcrux_ml_dsa.Ml_dsa_generic.sign_pre_hashed #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit + #Libcrux_ml_dsa.Samplex4.Portable.t_PortableSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 @@ -76,6 +81,7 @@ let verify (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit + #Libcrux_ml_dsa.Samplex4.Portable.t_PortableSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256Xof v_ROWS_IN_A v_COLUMNS_IN_A @@ -94,6 +100,7 @@ let verify_pre_hashed_shake128 (signature: t_Array u8 v_SIGNATURE_SIZE) = Libcrux_ml_dsa.Ml_dsa_generic.verify_pre_hashed #Libcrux_ml_dsa.Simd.Portable.Vector_type.t_PortableSIMDUnit + #Libcrux_ml_dsa.Samplex4.Portable.t_PortableSampler #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake256 diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fsti index 1e4399d64..9bd1f00f2 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.fsti @@ -10,6 +10,8 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in + let open Libcrux_ml_dsa.Samplex4.Portable in let open Libcrux_ml_dsa.Simd.Portable in let open Libcrux_ml_dsa.Simd.Traits in () 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 index 0bf89311c..1fec04ec9 100644 --- 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 @@ -9,6 +9,7 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in let open Libcrux_ml_dsa.Simd.Traits in () @@ -109,26 +110,311 @@ let derive_message_representative let _:Prims.unit = () in message_representative +let verify_internal + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: + usize) + (v_GAMMA2 v_BETA: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: + usize) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i5: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i6: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i7: + Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i8: + Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i9: + Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) + (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) + (message: t_Slice u8) + (domain_separation_context: + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) + (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) + = + let seed_for_A, t1:(t_Array u8 (sz 32) & + t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_ROWS_IN_A) = + Libcrux_ml_dsa.Encoding.Verification_key.deserialize #v_SIMDUnit + v_ROWS_IN_A + v_VERIFICATION_KEY_SIZE + verification_key_serialized + in + match + Libcrux_ml_dsa.Encoding.Signature.impl__deserialize #v_SIMDUnit + v_COMMITMENT_HASH_SIZE + v_COLUMNS_IN_A + v_ROWS_IN_A + v_GAMMA1_EXPONENT + v_GAMMA1_RING_ELEMENT_SIZE + v_MAX_ONES_IN_HINT + v_SIGNATURE_SIZE + signature_serialized + with + | Core.Result.Result_Ok s -> + let signature:Libcrux_ml_dsa.Encoding.Signature.t_Signature v_SIMDUnit + v_COMMITMENT_HASH_SIZE + v_COLUMNS_IN_A + v_ROWS_IN_A = + s + in + if + Libcrux_ml_dsa.Arithmetic.vector_infinity_norm_exceeds #v_SIMDUnit + v_COLUMNS_IN_A + signature.Libcrux_ml_dsa.Encoding.Signature.f_signer_response + ((2l < + Core.Result.Result_Err e + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + +let verify + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: + usize) + (v_GAMMA2 v_BETA: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: + usize) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i5: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i6: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i7: + Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i8: + Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i9: + Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) + (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) + (message context: t_Slice u8) + (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) + = + match + Libcrux_ml_dsa.Pre_hash.impl_1__new context + (Core.Option.Option_None <: Core.Option.t_Option (t_Array u8 (sz 11))) + with + | Core.Result.Result_Ok dsc -> + let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in + verify_internal #v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof v_ROWS_IN_A + v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT + v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA v_COMMITMENT_RING_ELEMENT_SIZE + v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE + v_MAX_ONES_IN_HINT verification_key_serialized message + (Core.Option.Option_Some domain_separation_context + <: + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) signature_serialized + | Core.Result.Result_Err _ -> + Core.Result.Result_Err + (Libcrux_ml_dsa.Types.VerificationError_VerificationContextTooLongError + <: + Libcrux_ml_dsa.Types.t_VerificationError) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + +let verify_pre_hashed + (#v_SIMDUnit #v_Sampler #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_PH: Type0) + (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: + usize) + (v_GAMMA2 v_BETA: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: + usize) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i7: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i8: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i9: + Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i10: + Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i11: + Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i12: + Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i13: + Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN) + (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) + (message context: t_Slice u8) + (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) + = + let pre_hashed_message:t_Array u8 v_PH_DIGEST_LEN = + Libcrux_ml_dsa.Pre_hash.f_hash #v_PH + #v_PH_DIGEST_LEN + #FStar.Tactics.Typeclasses.solve + #v_Shake128 + message + in + match + Libcrux_ml_dsa.Pre_hash.impl_1__new context + (Core.Option.Option_Some + (Libcrux_ml_dsa.Pre_hash.f_oid #v_PH #v_PH_DIGEST_LEN #FStar.Tactics.Typeclasses.solve () + <: + t_Array u8 (sz 11)) + <: + Core.Option.t_Option (t_Array u8 (sz 11))) + with + | Core.Result.Result_Ok dsc -> + let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in + verify_internal #v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof v_ROWS_IN_A + v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT + v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 v_BETA v_COMMITMENT_RING_ELEMENT_SIZE + v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE + v_MAX_ONES_IN_HINT verification_key_serialized (pre_hashed_message <: t_Slice u8) + (Core.Option.Option_Some domain_separation_context + <: + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) signature_serialized + | Core.Result.Result_Err _ -> + Core.Result.Result_Err + (Libcrux_ml_dsa.Types.VerificationError_VerificationContextTooLongError + <: + Libcrux_ml_dsa.Types.t_VerificationError) + <: + Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + let sign_internal - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) (v_GAMMA2: i32) (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i5: + i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: + i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: + i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i8: + i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i9: + i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) (message: t_Slice u8) @@ -154,7 +440,9 @@ let sign_internal let v_A_as_ntt:t_Array (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) v_ROWS_IN_A = - Libcrux_ml_dsa.Samplex4.matrix_A #v_SIMDUnit + Libcrux_ml_dsa.Samplex4.f_matrix_A #v_Sampler + #FStar.Tactics.Typeclasses.solve + #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A (Libcrux_ml_dsa.Utils.into_padded_array (sz 34) (seed_for_A <: t_Slice u8) @@ -480,354 +768,67 @@ let sign_internal ({ Libcrux_ml_dsa.Encoding.Signature.f_commitment_hash = commitment_hash; Libcrux_ml_dsa.Encoding.Signature.f_signer_response = signer_response; - Libcrux_ml_dsa.Encoding.Signature.f_hint = hint - } - <: - Libcrux_ml_dsa.Encoding.Signature.t_Signature v_SIMDUnit - v_COMMITMENT_HASH_SIZE - v_COLUMNS_IN_A - v_ROWS_IN_A) - in - Core.Result.Result_Ok (Libcrux_ml_dsa.Types.impl_4__new v_SIGNATURE_SIZE signature) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError - | Core.Option.Option_None -> - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError - <: - Libcrux_ml_dsa.Types.t_SigningError) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError) - | Core.Option.Option_None -> - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError - <: - Libcrux_ml_dsa.Types.t_SigningError) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError) - | Core.Option.Option_None -> - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError <: Libcrux_ml_dsa.Types.t_SigningError - ) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError - -let sign - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) - (v_GAMMA2: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: - usize) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i5: - Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: - Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: - Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i8: - Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i9: - Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) - (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) - (message context: t_Slice u8) - (randomness: t_Array u8 (sz 32)) - = - match - Libcrux_ml_dsa.Pre_hash.impl_1__new context - (Core.Option.Option_None <: Core.Option.t_Option (t_Array u8 (sz 11))) - with - | Core.Result.Result_Ok dsc -> - let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in - sign_internal #v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 v_ROWS_IN_A - v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 - v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE - v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE - v_SIGNATURE_SIZE signing_key message - (Core.Option.Option_Some domain_separation_context - <: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) randomness - | Core.Result.Result_Err _ -> - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError - -let sign_pre_hashed - (#v_SIMDUnit #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 #v_PH: Type0) - (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: - usize) - (v_GAMMA2: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: - usize) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: - Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i8: - Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i9: - Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i10: - Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i11: - Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i12: - Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i13: - Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN) - (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) - (message context: t_Slice u8) - (randomness: t_Array u8 (sz 32)) - = - if (Core.Slice.impl__len #u8 context <: usize) >. Libcrux_ml_dsa.Constants.v_CONTEXT_MAX_LEN - then - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError - else - let pre_hashed_message:t_Array u8 v_PH_DIGEST_LEN = - Libcrux_ml_dsa.Pre_hash.f_hash #v_PH - #v_PH_DIGEST_LEN - #FStar.Tactics.Typeclasses.solve - #v_Shake128 - message - in - match - Libcrux_ml_dsa.Pre_hash.impl_1__new context - (Core.Option.Option_Some - (Libcrux_ml_dsa.Pre_hash.f_oid #v_PH #v_PH_DIGEST_LEN #FStar.Tactics.Typeclasses.solve () - <: - t_Array u8 (sz 11)) - <: - Core.Option.t_Option (t_Array u8 (sz 11))) - with - | Core.Result.Result_Ok dsc -> - let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in - sign_internal #v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 v_ROWS_IN_A - v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 - v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE - v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE - v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE signing_key (pre_hashed_message <: t_Slice u8) - (Core.Option.Option_Some domain_separation_context - <: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) randomness - | Core.Result.Result_Err _ -> - Core.Result.Result_Err - (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) - <: - Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError - -let verify_internal - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: - usize) - (v_GAMMA2 v_BETA: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: - usize) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i4: - Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i5: - Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: - Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) - (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: - Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) - (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) - (message: t_Slice u8) - (domain_separation_context: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) - (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) - = - let seed_for_A, t1:(t_Array u8 (sz 32) & - t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_ROWS_IN_A) = - Libcrux_ml_dsa.Encoding.Verification_key.deserialize #v_SIMDUnit - v_ROWS_IN_A - v_VERIFICATION_KEY_SIZE - verification_key_serialized - in - match - Libcrux_ml_dsa.Encoding.Signature.impl__deserialize #v_SIMDUnit - v_COMMITMENT_HASH_SIZE - v_COLUMNS_IN_A - v_ROWS_IN_A - v_GAMMA1_EXPONENT - v_GAMMA1_RING_ELEMENT_SIZE - v_MAX_ONES_IN_HINT - v_SIGNATURE_SIZE - signature_serialized - with - | Core.Result.Result_Ok s -> - let signature:Libcrux_ml_dsa.Encoding.Signature.t_Signature v_SIMDUnit - v_COMMITMENT_HASH_SIZE - v_COLUMNS_IN_A - v_ROWS_IN_A = - s - in - if - Libcrux_ml_dsa.Arithmetic.vector_infinity_norm_exceeds #v_SIMDUnit - v_COLUMNS_IN_A - signature.Libcrux_ml_dsa.Encoding.Signature.f_signer_response - ((2l < + Core.Result.Result_Err + (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError + <: + Libcrux_ml_dsa.Types.t_SigningError) <: - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - in - let w_approx:t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - v_ROWS_IN_A = - Libcrux_ml_dsa.Matrix.compute_w_approx #v_SIMDUnit - v_ROWS_IN_A - v_COLUMNS_IN_A - v_A_as_ntt - signature.Libcrux_ml_dsa.Encoding.Signature.f_signer_response - verifier_challenge_as_ntt - t1 - in - let commitment_hash:t_Array u8 v_COMMITMENT_HASH_SIZE = - Rust_primitives.Hax.repeat 0uy v_COMMITMENT_HASH_SIZE - in - let commitment:t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - v_ROWS_IN_A = - Libcrux_ml_dsa.Arithmetic.use_hint #v_SIMDUnit - v_ROWS_IN_A - v_GAMMA2 - signature.Libcrux_ml_dsa.Encoding.Signature.f_hint - w_approx - in - let commitment_serialized:t_Array u8 v_COMMITMENT_VECTOR_SIZE = - Libcrux_ml_dsa.Encoding.Commitment.serialize_vector #v_SIMDUnit - v_ROWS_IN_A - v_COMMITMENT_RING_ELEMENT_SIZE - v_COMMITMENT_VECTOR_SIZE - commitment - in - let shake:v_Shake256Xof = - Libcrux_ml_dsa.Hash_functions.Shake256.f_init #v_Shake256Xof - #FStar.Tactics.Typeclasses.solve - () - in - let shake:v_Shake256Xof = - Libcrux_ml_dsa.Hash_functions.Shake256.f_absorb #v_Shake256Xof - #FStar.Tactics.Typeclasses.solve - shake - (message_representative <: t_Slice u8) - in - let shake:v_Shake256Xof = - Libcrux_ml_dsa.Hash_functions.Shake256.f_absorb_final #v_Shake256Xof - #FStar.Tactics.Typeclasses.solve - shake - (commitment_serialized <: t_Slice u8) - in - let tmp0, tmp1:(v_Shake256Xof & t_Array u8 v_COMMITMENT_HASH_SIZE) = - Libcrux_ml_dsa.Hash_functions.Shake256.f_squeeze #v_Shake256Xof - #FStar.Tactics.Typeclasses.solve - shake - commitment_hash - in - let shake:v_Shake256Xof = tmp0 in - let commitment_hash:t_Array u8 v_COMMITMENT_HASH_SIZE = tmp1 in - let _:Prims.unit = () in - let _:Prims.unit = () in - if signature.Libcrux_ml_dsa.Encoding.Signature.f_commitment_hash =. commitment_hash - then - Core.Result.Result_Ok (() <: Prims.unit) - <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError - else + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError) + | Core.Option.Option_None -> Core.Result.Result_Err - (Libcrux_ml_dsa.Types.VerificationError_CommitmentHashesDontMatchError + (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError <: - Libcrux_ml_dsa.Types.t_VerificationError) + Libcrux_ml_dsa.Types.t_SigningError) <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError - | Core.Result.Result_Err e -> - Core.Result.Result_Err e + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError) + | Core.Option.Option_None -> + Core.Result.Result_Err + (Libcrux_ml_dsa.Types.SigningError_RejectionSamplingError <: Libcrux_ml_dsa.Types.t_SigningError + ) <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError -let verify - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: - usize) - (v_GAMMA2 v_BETA: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: +let sign + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) + (v_GAMMA2: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i4: + i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i5: + i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: + i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: + i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) - (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i11: + Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) + (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) (message context: t_Slice u8) - (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) + (randomness: t_Array u8 (sz 32)) = match Libcrux_ml_dsa.Pre_hash.impl_1__new context @@ -835,102 +836,115 @@ let verify with | Core.Result.Result_Ok dsc -> let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in - verify_internal #v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof v_ROWS_IN_A v_COLUMNS_IN_A - v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 - v_BETA v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE - v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT verification_key_serialized message + sign_internal #v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 + v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 + v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE + v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE + v_SIGNATURE_SIZE signing_key message (Core.Option.Option_Some domain_separation_context <: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) signature_serialized + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) randomness | Core.Result.Result_Err _ -> Core.Result.Result_Err - (Libcrux_ml_dsa.Types.VerificationError_VerificationContextTooLongError - <: - Libcrux_ml_dsa.Types.t_VerificationError) + (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError -let verify_pre_hashed - (#v_SIMDUnit #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_PH: Type0) - (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: +let sign_pre_hashed + (#v_SIMDUnit #v_Sampler #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 #v_PH: + Type0) + (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) - (v_GAMMA2 v_BETA: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: + (v_GAMMA2: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: + i8: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i9: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: + i10: Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i8: + i11: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i9: + i12: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i10: + i13: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i11: + i14: + Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i15: Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN) - (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) + (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) (message context: t_Slice u8) - (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) + (randomness: t_Array u8 (sz 32)) = - let pre_hashed_message:t_Array u8 v_PH_DIGEST_LEN = - Libcrux_ml_dsa.Pre_hash.f_hash #v_PH - #v_PH_DIGEST_LEN - #FStar.Tactics.Typeclasses.solve - #v_Shake128 - message - in - match - Libcrux_ml_dsa.Pre_hash.impl_1__new context - (Core.Option.Option_Some - (Libcrux_ml_dsa.Pre_hash.f_oid #v_PH #v_PH_DIGEST_LEN #FStar.Tactics.Typeclasses.solve () - <: - t_Array u8 (sz 11)) - <: - Core.Option.t_Option (t_Array u8 (sz 11))) - with - | Core.Result.Result_Ok dsc -> - let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in - verify_internal #v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof v_ROWS_IN_A v_COLUMNS_IN_A - v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE v_GAMMA2 - v_BETA v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE - v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT verification_key_serialized - (pre_hashed_message <: t_Slice u8) - (Core.Option.Option_Some domain_separation_context - <: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) signature_serialized - | Core.Result.Result_Err _ -> + if (Core.Slice.impl__len #u8 context <: usize) >. Libcrux_ml_dsa.Constants.v_CONTEXT_MAX_LEN + then Core.Result.Result_Err - (Libcrux_ml_dsa.Types.VerificationError_VerificationContextTooLongError - <: - Libcrux_ml_dsa.Types.t_VerificationError) + (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) <: - Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError + else + let pre_hashed_message:t_Array u8 v_PH_DIGEST_LEN = + Libcrux_ml_dsa.Pre_hash.f_hash #v_PH + #v_PH_DIGEST_LEN + #FStar.Tactics.Typeclasses.solve + #v_Shake128 + message + in + match + Libcrux_ml_dsa.Pre_hash.impl_1__new context + (Core.Option.Option_Some + (Libcrux_ml_dsa.Pre_hash.f_oid #v_PH #v_PH_DIGEST_LEN #FStar.Tactics.Typeclasses.solve () + <: + t_Array u8 (sz 11)) + <: + Core.Option.t_Option (t_Array u8 (sz 11))) + with + | Core.Result.Result_Ok dsc -> + let domain_separation_context:Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext = dsc in + sign_internal #v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 + v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT v_GAMMA2 + v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE + v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE + v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE signing_key (pre_hashed_message <: t_Slice u8) + (Core.Option.Option_Some domain_separation_context + <: + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) randomness + | Core.Result.Result_Err _ -> + Core.Result.Result_Err + (Libcrux_ml_dsa.Types.SigningError_ContextTooLongError <: Libcrux_ml_dsa.Types.t_SigningError) + <: + Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError let generate_key_pair - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE: usize) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i5: + i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i6: + i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i7: + i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i8: + i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i9: + i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4) (randomness: t_Array u8 (sz 32)) = @@ -977,7 +991,9 @@ let generate_key_pair let a_as_ntt:t_Array (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) v_ROWS_IN_A = - Libcrux_ml_dsa.Samplex4.matrix_A #v_SIMDUnit + Libcrux_ml_dsa.Samplex4.f_matrix_A #v_Sampler + #FStar.Tactics.Typeclasses.solve + #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A (Libcrux_ml_dsa.Utils.into_padded_array (sz 34) seed_for_a <: t_Array u8 (sz 34)) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fsti index b333cdc66..a1ac213b3 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.fsti @@ -9,6 +9,7 @@ let _ = let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Pre_hash in + let open Libcrux_ml_dsa.Samplex4 in let open Libcrux_ml_dsa.Simd.Traits in () @@ -39,82 +40,21 @@ val derive_message_representative (message_representative: t_Array u8 (sz 64)) : Prims.Pure (t_Array u8 (sz 64)) Prims.l_True (fun _ -> Prims.l_True) -/// The internal signing API. -/// If no `domain_separation_context` is supplied, it is assumed that -/// `message` already contains the domain separation. -val sign_internal - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) - (v_GAMMA2: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: - usize) - {| i5: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i6: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i8: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} - {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} - (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) - (message: t_Slice u8) - (domain_separation_context: - Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) - (randomness: t_Array u8 (sz 32)) - : Prims.Pure - (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) - -val sign - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) - (v_GAMMA2: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: - usize) - {| i5: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i6: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i8: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} - {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} - (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) - (message context: t_Slice u8) - (randomness: t_Array u8 (sz 32)) - : Prims.Pure - (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) - -val sign_pre_hashed - (#v_SIMDUnit #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 #v_PH: Type0) - (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: - usize) - (v_GAMMA2: i32) - (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: - usize) - {| i7: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128 |} - {| i9: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} - {| i12: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} - {| i13: Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN |} - (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) - (message context: t_Slice u8) - (randomness: t_Array u8 (sz 32)) - : Prims.Pure - (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) - Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) - /// The internal verification API. /// If no `domain_separation_context` is supplied, it is assumed that /// `message` already contains the domain separation. val verify_internal - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: usize) (v_GAMMA2 v_BETA: i32) (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: usize) - {| i4: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i5: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i6: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i5: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i6: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i7: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i8: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) (message: t_Slice u8) (domain_separation_context: @@ -125,16 +65,17 @@ val verify_internal (fun _ -> Prims.l_True) val verify - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: usize) (v_GAMMA2 v_BETA: i32) (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: usize) - {| i4: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i5: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i6: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i5: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i6: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i7: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i8: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) (message context: t_Slice u8) (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) @@ -143,18 +84,19 @@ val verify (fun _ -> Prims.l_True) val verify_pre_hashed - (#v_SIMDUnit #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_PH: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_PH: Type0) (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_SIGNATURE_SIZE v_VERIFICATION_KEY_SIZE v_GAMMA1_EXPONENT v_GAMMA1_RING_ELEMENT_SIZE: usize) (v_GAMMA2 v_BETA: i32) (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT: usize) - {| i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128 |} - {| i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} - {| i11: Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN |} + {| i7: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i8: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128 |} + {| i10: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i12: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i13: Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN |} (verification_key_serialized: t_Array u8 v_VERIFICATION_KEY_SIZE) (message context: t_Slice u8) (signature_serialized: t_Array u8 v_SIGNATURE_SIZE) @@ -162,16 +104,83 @@ val verify_pre_hashed Prims.l_True (fun _ -> Prims.l_True) +/// The internal signing API. +/// If no `domain_separation_context` is supplied, it is assumed that +/// `message` already contains the domain separation. +val sign_internal + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) + (v_GAMMA2: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: + usize) + {| i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} + (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) + (message: t_Slice u8) + (domain_separation_context: + Core.Option.t_Option Libcrux_ml_dsa.Pre_hash.t_DomainSeparationContext) + (randomness: t_Array u8 (sz 32)) + : Prims.Pure + (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) + +val sign + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: usize) + (v_GAMMA2: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: + usize) + {| i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} + (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) + (message context: t_Slice u8) + (randomness: t_Array u8 (sz 32)) + : Prims.Pure + (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) + +val sign_pre_hashed + (#v_SIMDUnit #v_Sampler #v_Shake128 #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4 #v_PH: + Type0) + (v_PH_DIGEST_LEN v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_GAMMA1_EXPONENT: + usize) + (v_GAMMA2: i32) + (v_COMMITMENT_RING_ELEMENT_SIZE v_COMMITMENT_VECTOR_SIZE v_COMMITMENT_HASH_SIZE v_ONES_IN_VERIFIER_CHALLENGE v_MAX_ONES_IN_HINT v_GAMMA1_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_SIGNATURE_SIZE: + usize) + {| i8: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i9: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i10: Libcrux_ml_dsa.Hash_functions.Shake128.t_Xof v_Shake128 |} + {| i11: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i12: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i13: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i14: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} + {| i15: Libcrux_ml_dsa.Pre_hash.t_PreHash v_PH v_PH_DIGEST_LEN |} + (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) + (message context: t_Slice u8) + (randomness: t_Array u8 (sz 32)) + : Prims.Pure + (Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature v_SIGNATURE_SIZE) + Libcrux_ml_dsa.Types.t_SigningError) Prims.l_True (fun _ -> Prims.l_True) + /// Generate a key pair. val generate_key_pair - (#v_SIMDUnit #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) + (#v_SIMDUnit #v_Sampler #v_Shake128X4 #v_Shake256 #v_Shake256Xof #v_Shake256X4: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE: usize) - {| i5: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - {| i6: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} - {| i7: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} - {| i8: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} - {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} + {| i6: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i7: Libcrux_ml_dsa.Samplex4.t_X4Sampler v_Sampler |} + {| i8: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128X4 |} + {| i9: Libcrux_ml_dsa.Hash_functions.Shake256.t_DsaXof v_Shake256 |} + {| i10: Libcrux_ml_dsa.Hash_functions.Shake256.t_Xof v_Shake256Xof |} + {| i11: Libcrux_ml_dsa.Hash_functions.Shake256.t_XofX4 v_Shake256X4 |} (randomness: t_Array u8 (sz 32)) : Prims.Pure (t_Array u8 v_SIGNING_KEY_SIZE & t_Array u8 v_VERIFICATION_KEY_SIZE) Prims.l_True diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst index 1cfb3ccb5..99e46c0e2 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fst @@ -9,6 +9,38 @@ let _ = let open Libcrux_ml_dsa.Simd.Traits in () +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': + #v_SIMDUnit: Type0 -> + {| i1: Core.Clone.t_Clone v_SIMDUnit |} -> + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + -> Core.Clone.t_Clone (t_PolynomialRingElement v_SIMDUnit) + +let impl_1 + (#v_SIMDUnit: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + = impl_1' #v_SIMDUnit #i1 #i2 + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': + #v_SIMDUnit: Type0 -> + {| i1: Core.Marker.t_Copy v_SIMDUnit |} -> + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + -> Core.Marker.t_Copy (t_PolynomialRingElement v_SIMDUnit) + +let impl_2 + (#v_SIMDUnit: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + = impl_2' #v_SIMDUnit #i1 #i2 + let impl__ZERO (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -32,7 +64,7 @@ let impl__ZERO let impl__from_i32_array (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (array: t_Slice i32) = @@ -92,7 +124,7 @@ let impl__from_i32_array let impl__add (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (self rhs: t_PolynomialRingElement v_SIMDUnit) = @@ -131,7 +163,7 @@ let impl__add let impl__infinity_norm_exceeds (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (self: t_PolynomialRingElement v_SIMDUnit) (bound: i32) @@ -161,7 +193,7 @@ let impl__infinity_norm_exceeds let impl__subtract (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (self rhs: t_PolynomialRingElement v_SIMDUnit) = @@ -200,7 +232,7 @@ let impl__subtract let impl__to_i32_array (#v_SIMDUnit: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] - i2: + i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) (self: t_PolynomialRingElement v_SIMDUnit) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fsti index 6f7a5837e..b9648e9ab 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Polynomial.fsti @@ -13,6 +13,20 @@ type t_PolynomialRingElement (v_SIMDUnit: Type0) {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} = { f_simd_units:t_Array v_SIMDUnit (sz 32) } +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1 + (#v_SIMDUnit: Type0) + {| i1: Core.Clone.t_Clone v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + : Core.Clone.t_Clone (t_PolynomialRingElement v_SIMDUnit) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2 + (#v_SIMDUnit: Type0) + {| i1: Core.Marker.t_Copy v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + : Core.Marker.t_Copy (t_PolynomialRingElement v_SIMDUnit) + val impl__ZERO: #v_SIMDUnit: Type0 -> {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} -> @@ -21,31 +35,31 @@ val impl__ZERO: val impl__from_i32_array (#v_SIMDUnit: Type0) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (array: t_Slice i32) : Prims.Pure (t_PolynomialRingElement v_SIMDUnit) Prims.l_True (fun _ -> Prims.l_True) val impl__add (#v_SIMDUnit: Type0) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (self rhs: t_PolynomialRingElement v_SIMDUnit) : Prims.Pure (t_PolynomialRingElement v_SIMDUnit) Prims.l_True (fun _ -> Prims.l_True) val impl__infinity_norm_exceeds (#v_SIMDUnit: Type0) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (self: t_PolynomialRingElement v_SIMDUnit) (bound: i32) : Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True) val impl__subtract (#v_SIMDUnit: Type0) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (self rhs: t_PolynomialRingElement v_SIMDUnit) : Prims.Pure (t_PolynomialRingElement v_SIMDUnit) Prims.l_True (fun _ -> Prims.l_True) val impl__to_i32_array (#v_SIMDUnit: Type0) - {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} (self: t_PolynomialRingElement v_SIMDUnit) : Prims.Pure (t_Array i32 (sz 256)) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst index 288d73ebd..a209fd286 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fst @@ -6,12 +6,14 @@ open FStar.Mul let _ = (* This module has implicit dependencies, here we make them explicit. *) (* The implicit dependencies arise from typeclasses instances. *) - let open Libcrux_ml_dsa.Hash_functions.Portable in let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Simd.Traits in () +let generate_domain_separator (row, column: (u8 & u8)) = + (cast (column <: u8) <: u16) |. ((cast (row <: u8) <: u16) <>! 8l <: u16) <: u8) - in - let seed1:t_Array u8 (sz 34) = seed0 in - let seed1:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed1 - (sz 32) - (cast (domain_separator1 <: u16) <: u8) - in - let seed1:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed1 - (sz 33) - (cast (domain_separator1 >>! 8l <: u16) <: u8) - in - let seed2:t_Array u8 (sz 34) = seed0 in - let seed2:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed2 - (sz 32) - (cast (domain_seperator2 <: u16) <: u8) - in - let seed2:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed2 - (sz 33) - (cast (domain_seperator2 >>! 8l <: u16) <: u8) - in - let seed3:t_Array u8 (sz 34) = seed0 in - let seed3:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed3 - (sz 32) - (cast (domain_separator3 <: u16) <: u8) - in - let seed3:t_Array u8 (sz 34) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed3 - (sz 33) - (cast (domain_separator3 >>! 8l <: u16) <: u8) - in - let state:Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 = - Libcrux_ml_dsa.Hash_functions.Shake128.f_init_absorb #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 - #FStar.Tactics.Typeclasses.solve - (seed0 <: t_Slice u8) - (seed1 <: t_Slice u8) - (seed2 <: t_Slice u8) - (seed3 <: t_Slice u8) - in - let randomness0:t_Array u8 (sz 840) = Rust_primitives.Hax.repeat 0uy (sz 840) in - let randomness1:t_Array u8 (sz 840) = Rust_primitives.Hax.repeat 0uy (sz 840) in - let randomness2:t_Array u8 (sz 840) = Rust_primitives.Hax.repeat 0uy (sz 840) in - let randomness3:t_Array u8 (sz 840) = Rust_primitives.Hax.repeat 0uy (sz 840) in - let tmp0, tmp1, tmp2, tmp3, tmp4:(Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 & - t_Array u8 (sz 840) & - t_Array u8 (sz 840) & - t_Array u8 (sz 840) & - t_Array u8 (sz 840)) = - Libcrux_ml_dsa.Hash_functions.Shake128.f_squeeze_first_five_blocks #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 - #FStar.Tactics.Typeclasses.solve - state - randomness0 - randomness1 - randomness2 - randomness3 - in - let state:Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 = tmp0 in - let randomness0:t_Array u8 (sz 840) = tmp1 in - let randomness1:t_Array u8 (sz 840) = tmp2 in - let randomness2:t_Array u8 (sz 840) = tmp3 in - let randomness3:t_Array u8 (sz 840) = tmp4 in - let _:Prims.unit = () in - let coefficients0:t_Array i32 (sz 263) = Rust_primitives.Hax.repeat 0l (sz 263) in - let coefficients1:t_Array i32 (sz 263) = Rust_primitives.Hax.repeat 0l (sz 263) in - let coefficients2:t_Array i32 (sz 263) = Rust_primitives.Hax.repeat 0l (sz 263) in - let coefficients3:t_Array i32 (sz 263) = Rust_primitives.Hax.repeat 0l (sz 263) in - let sampled0:usize = sz 0 in - let sampled1:usize = sz 0 in - let sampled2:usize = sz 0 in - let sampled3:usize = sz 0 in - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomness0 <: t_Slice u8) - sampled0 - coefficients0 - in - let sampled0:usize = tmp0 in - let coefficients0:t_Array i32 (sz 263) = tmp1 in - let done0:bool = out in - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomness1 <: t_Slice u8) - sampled1 - coefficients1 - in - let sampled1:usize = tmp0 in - let coefficients1:t_Array i32 (sz 263) = tmp1 in - let done1:bool = out in - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomness2 <: t_Slice u8) - sampled2 - coefficients2 - in - let sampled2:usize = tmp0 in - let coefficients2:t_Array i32 (sz 263) = tmp1 in - let done2:bool = out in - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomness3 <: t_Slice u8) - sampled3 - coefficients3 - in - let sampled3:usize = tmp0 in - let coefficients3:t_Array i32 (sz 263) = tmp1 in - let done3:bool = out in - let - coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state:(t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4) = - Rust_primitives.f_while_loop (fun temp_0_ -> - let - coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state:(t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4) = - temp_0_ - in - (~.done0 <: bool) || (~.done1 <: bool) || (~.done2 <: bool) || (~.done3 <: bool)) - (coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state - <: - (t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4)) - (fun temp_0_ -> - let - coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state:(t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4) = - temp_0_ - in - let tmp0, out:(Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 & - (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168))) - = - Libcrux_ml_dsa.Hash_functions.Shake128.f_squeeze_next_block #Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 - #FStar.Tactics.Typeclasses.solve - state - in - let state:Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4 = tmp0 in - let randomnesses:(t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & - t_Array u8 (sz 168)) = - out - in - let coefficients0, done0, sampled0:(t_Array i32 (sz 263) & bool & usize) = - if ~.done0 - then - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomnesses._1 <: t_Slice u8) - sampled0 - coefficients0 - in - let sampled0:usize = tmp0 in - let coefficients0:t_Array i32 (sz 263) = tmp1 in - let done0:bool = out in - coefficients0, done0, sampled0 <: (t_Array i32 (sz 263) & bool & usize) - else coefficients0, done0, sampled0 <: (t_Array i32 (sz 263) & bool & usize) - in - let coefficients1, done1, sampled1:(t_Array i32 (sz 263) & bool & usize) = - if ~.done1 - then - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomnesses._2 <: t_Slice u8) - sampled1 - coefficients1 - in - let sampled1:usize = tmp0 in - let coefficients1:t_Array i32 (sz 263) = tmp1 in - let done1:bool = out in - coefficients1, done1, sampled1 <: (t_Array i32 (sz 263) & bool & usize) - else coefficients1, done1, sampled1 <: (t_Array i32 (sz 263) & bool & usize) - in - let coefficients2, done2, sampled2:(t_Array i32 (sz 263) & bool & usize) = - if ~.done2 - then - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomnesses._3 <: t_Slice u8) - sampled2 - coefficients2 - in - let sampled2:usize = tmp0 in - let coefficients2:t_Array i32 (sz 263) = tmp1 in - let done2:bool = out in - coefficients2, done2, sampled2 <: (t_Array i32 (sz 263) & bool & usize) - else coefficients2, done2, sampled2 <: (t_Array i32 (sz 263) & bool & usize) - in - if ~.done3 - then - let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = - rejection_sample_less_than_field_modulus #v_SIMDUnit - (randomnesses._4 <: t_Slice u8) - sampled3 - coefficients3 - in - let sampled3:usize = tmp0 in - let coefficients3:t_Array i32 (sz 263) = tmp1 in - let done3:bool = out in - coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state - <: - (t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4) - else - coefficients0, - coefficients1, - coefficients2, - coefficients3, - done0, - done1, - done2, - done3, - sampled0, - sampled1, - sampled2, - sampled3, - state - <: - (t_Array i32 (sz 263) & t_Array i32 (sz 263) & t_Array i32 (sz 263) & - t_Array i32 (sz 263) & - bool & - bool & - bool & - bool & - usize & - usize & - usize & - usize & - Libcrux_ml_dsa.Hash_functions.Portable.t_Shake128X4)) - in - Libcrux_ml_dsa.Polynomial.impl__from_i32_array #v_SIMDUnit (coefficients0 <: t_Slice i32), - Libcrux_ml_dsa.Polynomial.impl__from_i32_array #v_SIMDUnit (coefficients1 <: t_Slice i32), - Libcrux_ml_dsa.Polynomial.impl__from_i32_array #v_SIMDUnit (coefficients2 <: t_Slice i32), - Libcrux_ml_dsa.Polynomial.impl__from_i32_array #v_SIMDUnit (coefficients3 <: t_Slice i32) - <: - (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - let sample_mask_ring_element (#v_SIMDUnit #v_Shake256: Type0) (v_GAMMA1_EXPONENT: usize) @@ -1317,3 +961,376 @@ let sample_mask_vector domain_separator, hax_temp_output <: (u16 & t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_DIMENSION) + +let sample_up_to_four_ring_elements + (#v_SIMDUnit #v_Shake128: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A: usize) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i2: + Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i3: + Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128) + (seed0: t_Array u8 (sz 34)) + (matrix: + t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A) + (rand_stack: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840))) + (tmp_stack: t_Slice (t_Array i32 (sz 263))) + (indices: t_Array (u8 & u8) (sz 4)) + (elements_requested: usize) + = + let _:Prims.unit = + if true + then + let _:Prims.unit = Hax_lib.v_assert (elements_requested <=. sz 4 <: bool) in + () + in + let domain_separator0:u16 = generate_domain_separator (indices.[ sz 0 ] <: (u8 & u8)) in + let domain_separator1:u16 = generate_domain_separator (indices.[ sz 1 ] <: (u8 & u8)) in + let domain_separator2:u16 = generate_domain_separator (indices.[ sz 2 ] <: (u8 & u8)) in + let domain_separator3:u16 = generate_domain_separator (indices.[ sz 3 ] <: (u8 & u8)) in + let seed0:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed0 + (sz 32) + (cast (domain_separator0 <: u16) <: u8) + in + let seed0:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed0 + (sz 33) + (cast (domain_separator0 >>! 8l <: u16) <: u8) + in + let seed1:t_Array u8 (sz 34) = seed0 in + let seed1:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed1 + (sz 32) + (cast (domain_separator1 <: u16) <: u8) + in + let seed1:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed1 + (sz 33) + (cast (domain_separator1 >>! 8l <: u16) <: u8) + in + let seed2:t_Array u8 (sz 34) = seed0 in + let seed2:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed2 + (sz 32) + (cast (domain_separator2 <: u16) <: u8) + in + let seed2:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed2 + (sz 33) + (cast (domain_separator2 >>! 8l <: u16) <: u8) + in + let seed3:t_Array u8 (sz 34) = seed0 in + let seed3:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed3 + (sz 32) + (cast (domain_separator3 <: u16) <: u8) + in + let seed3:t_Array u8 (sz 34) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize seed3 + (sz 33) + (cast (domain_separator3 >>! 8l <: u16) <: u8) + in + let state:v_Shake128 = + Libcrux_ml_dsa.Hash_functions.Shake128.f_init_absorb #v_Shake128 + #FStar.Tactics.Typeclasses.solve + (seed0 <: t_Slice u8) + (seed1 <: t_Slice u8) + (seed2 <: t_Slice u8) + (seed3 <: t_Slice u8) + in + let tmp0, tmp1, tmp2, tmp3, tmp4:(v_Shake128 & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + Libcrux_ml_dsa.Hash_functions.Shake128.f_squeeze_first_five_blocks #v_Shake128 + #FStar.Tactics.Typeclasses.solve + state + rand_stack._1 + rand_stack._2 + rand_stack._3 + rand_stack._4 + in + let state:v_Shake128 = tmp0 in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _1 = tmp1 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _2 = tmp2 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _3 = tmp3 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _4 = tmp4 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let _:Prims.unit = () in + let sampled0:usize = sz 0 in + let sampled1:usize = sz 0 in + let sampled2:usize = sz 0 in + let sampled3:usize = sz 0 in + let tmp0, out:(t_Array u8 (sz 840) & t_Array u8 (sz 840)) = rand_stack._1 in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _1 = tmp0 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (out <: t_Slice u8) + sampled0 + (tmp_stack.[ sz 0 ] <: t_Array i32 (sz 263)) + in + let sampled0:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 0) tmp1 + in + let done0:bool = out in + let tmp0, out:(t_Array u8 (sz 840) & t_Array u8 (sz 840)) = rand_stack._2 in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _2 = tmp0 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (out <: t_Slice u8) + sampled1 + (tmp_stack.[ sz 1 ] <: t_Array i32 (sz 263)) + in + let sampled1:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 1) tmp1 + in + let done1:bool = out in + let tmp0, out:(t_Array u8 (sz 840) & t_Array u8 (sz 840)) = rand_stack._3 in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _3 = tmp0 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (out <: t_Slice u8) + sampled2 + (tmp_stack.[ sz 2 ] <: t_Array i32 (sz 263)) + in + let sampled2:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 2) tmp1 + in + let done2:bool = out in + let tmp0, out:(t_Array u8 (sz 840) & t_Array u8 (sz 840)) = rand_stack._4 in + let rand_stack:(t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & + t_Array u8 (sz 840)) = + { rand_stack with _4 = tmp0 } + <: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) + in + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (out <: t_Slice u8) + sampled3 + (tmp_stack.[ sz 3 ] <: t_Array i32 (sz 263)) + in + let sampled3:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 3) tmp1 + in + let done3:bool = out in + let done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack:(bool & + bool & + bool & + bool & + usize & + usize & + usize & + usize & + v_Shake128 & + t_Slice (t_Array i32 (sz 263))) = + Rust_primitives.f_while_loop (fun temp_0_ -> + let done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack:(bool & + bool & + bool & + bool & + usize & + usize & + usize & + usize & + v_Shake128 & + t_Slice (t_Array i32 (sz 263))) = + temp_0_ + in + (~.done0 <: bool) || (~.done1 <: bool) || (~.done2 <: bool) || (~.done3 <: bool)) + (done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack + <: + (bool & bool & bool & bool & usize & usize & usize & usize & v_Shake128 & + t_Slice (t_Array i32 (sz 263)))) + (fun temp_0_ -> + let done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack:(bool & + bool & + bool & + bool & + usize & + usize & + usize & + usize & + v_Shake128 & + t_Slice (t_Array i32 (sz 263))) = + temp_0_ + in + let tmp0, out:(v_Shake128 & + (t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168))) + = + Libcrux_ml_dsa.Hash_functions.Shake128.f_squeeze_next_block #v_Shake128 + #FStar.Tactics.Typeclasses.solve + state + in + let state:v_Shake128 = tmp0 in + let randomnesses:(t_Array u8 (sz 168) & t_Array u8 (sz 168) & t_Array u8 (sz 168) & + t_Array u8 (sz 168)) = + out + in + let done0, sampled0, tmp_stack:(bool & usize & t_Slice (t_Array i32 (sz 263))) = + if ~.done0 + then + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (randomnesses._1 <: t_Slice u8) + sampled0 + (tmp_stack.[ sz 0 ] <: t_Array i32 (sz 263)) + in + let sampled0:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 0) tmp1 + in + let done0:bool = out in + done0, sampled0, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + else done0, sampled0, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + in + let done1, sampled1, tmp_stack:(bool & usize & t_Slice (t_Array i32 (sz 263))) = + if ~.done1 + then + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (randomnesses._2 <: t_Slice u8) + sampled1 + (tmp_stack.[ sz 1 ] <: t_Array i32 (sz 263)) + in + let sampled1:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 1) tmp1 + in + let done1:bool = out in + done1, sampled1, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + else done1, sampled1, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + in + let done2, sampled2, tmp_stack:(bool & usize & t_Slice (t_Array i32 (sz 263))) = + if ~.done2 + then + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (randomnesses._3 <: t_Slice u8) + sampled2 + (tmp_stack.[ sz 2 ] <: t_Array i32 (sz 263)) + in + let sampled2:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 2) tmp1 + in + let done2:bool = out in + done2, sampled2, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + else done2, sampled2, tmp_stack <: (bool & usize & t_Slice (t_Array i32 (sz 263))) + in + if ~.done3 + then + let tmp0, tmp1, out:(usize & t_Array i32 (sz 263) & bool) = + rejection_sample_less_than_field_modulus #v_SIMDUnit + (randomnesses._4 <: t_Slice u8) + sampled3 + (tmp_stack.[ sz 3 ] <: t_Array i32 (sz 263)) + in + let sampled3:usize = tmp0 in + let tmp_stack:t_Slice (t_Array i32 (sz 263)) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize tmp_stack (sz 3) tmp1 + in + let done3:bool = out in + done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack + <: + (bool & bool & bool & bool & usize & usize & usize & usize & v_Shake128 & + t_Slice (t_Array i32 (sz 263))) + else + done0, done1, done2, done3, sampled0, sampled1, sampled2, sampled3, state, tmp_stack + <: + (bool & bool & bool & bool & usize & usize & usize & usize & v_Shake128 & + t_Slice (t_Array i32 (sz 263)))) + in + let matrix, hax_temp_output:(t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A & + Prims.unit) = + Rust_primitives.Hax.Folds.fold_range (sz 0) + elements_requested + (fun matrix temp_1_ -> + let matrix:t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A = + matrix + in + let _:usize = temp_1_ in + true) + matrix + (fun matrix k -> + let matrix:t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A = + matrix + in + let k:usize = k in + let i, j:(u8 & u8) = indices.[ k ] in + let matrix:t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize matrix + (cast (i <: u8) <: usize) + (Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (matrix.[ cast (i <: u8) + <: + usize ] + <: + t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) + v_COLUMNS_IN_A) + (cast (j <: u8) <: usize) + (Libcrux_ml_dsa.Polynomial.impl__from_i32_array #v_SIMDUnit + (tmp_stack.[ k ] <: t_Slice i32) + <: + Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) + <: + t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) + v_COLUMNS_IN_A) + in + matrix) + in + matrix, rand_stack, tmp_stack + <: + (t_Array (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A & + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) & + t_Slice (t_Array i32 (sz 263))) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fsti index 9cab11744..142041aa2 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Sample.fsti @@ -6,12 +6,13 @@ open FStar.Mul let _ = (* This module has implicit dependencies, here we make them explicit. *) (* The implicit dependencies arise from typeclasses instances. *) - let open Libcrux_ml_dsa.Hash_functions.Portable in let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Simd.Traits in () +val generate_domain_separator: (u8 & u8) -> Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True) + val update_seed (seed: t_Array u8 (sz 66)) (domain_separator: u16) : Prims.Pure (u16 & t_Array u8 (sz 66)) Prims.l_True (fun _ -> Prims.l_True) @@ -80,19 +81,6 @@ val sample_four_error_ring_elements Prims.l_True (fun _ -> Prims.l_True) -val sample_four_ring_elements - (#v_SIMDUnit: Type0) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - (seed0: t_Array u8 (sz 34)) - (domain_separator0 domain_separator1 domain_seperator2 domain_separator3: u16) - : Prims.Pure - (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit & - Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - Prims.l_True - (fun _ -> Prims.l_True) - val sample_mask_ring_element (#v_SIMDUnit #v_Shake256: Type0) (v_GAMMA1_EXPONENT: usize) @@ -116,3 +104,32 @@ val sample_mask_vector (u16 & t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_DIMENSION) Prims.l_True (fun _ -> Prims.l_True) + +/// Sample and write out up to four ring elements. +/// If i <= `elements_requested`, a field element with domain separated +/// seed according to the provided index is generated in +/// `tmp_stack[i]`. After successful rejection sampling in +/// `tmp_stack[i]`, the ring element is written to `matrix` at the +/// provided index in `indices[i]`. +/// `rand_stack` is a working buffer that holds initial Shake output. +val sample_up_to_four_ring_elements + (#v_SIMDUnit #v_Shake128: Type0) + (v_ROWS_IN_A v_COLUMNS_IN_A: usize) + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i3: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128 |} + (seed0: t_Array u8 (sz 34)) + (matrix: + t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A) + (rand_stack: + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840))) + (tmp_stack: t_Slice (t_Array i32 (sz 263))) + (indices: t_Array (u8 & u8) (sz 4)) + (elements_requested: usize) + : Prims.Pure + (t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A & + (t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840) & t_Array u8 (sz 840)) & + t_Slice (t_Array i32 (sz 263))) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst index 06a86b638..105849569 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fst @@ -6,47 +6,20 @@ open FStar.Mul let _ = (* This module has implicit dependencies, here we make them explicit. *) (* The implicit dependencies arise from typeclasses instances. *) + let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Simd.Traits in () -let generate_domain_separator (row column: u8) = - (cast (column <: u8) <: u16) |. ((cast (row <: u8) <: u16) < matrix_A_4_by_4_ #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A seed - | 6uy, 5uy -> matrix_A_6_by_5_ #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A seed - | 8uy, 7uy -> matrix_A_8_by_7_ #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A seed + | 4uy, 4uy -> matrix_A_4_by_4_ #v_SIMDUnit #v_Shake128 v_ROWS_IN_A v_COLUMNS_IN_A seed + | 6uy, 5uy -> matrix_A_6_by_5_ #v_SIMDUnit #v_Shake128 v_ROWS_IN_A v_COLUMNS_IN_A seed + | 8uy, 7uy -> matrix_A_8_by_7_ #v_SIMDUnit #v_Shake128 v_ROWS_IN_A v_COLUMNS_IN_A seed | _ -> Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code" diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fsti index e1b9a56dc..13aa21421 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Samplex4.fsti @@ -6,31 +6,49 @@ open FStar.Mul let _ = (* This module has implicit dependencies, here we make them explicit. *) (* The implicit dependencies arise from typeclasses instances. *) + let open Libcrux_ml_dsa.Hash_functions.Shake128 in let open Libcrux_ml_dsa.Hash_functions.Shake256 in let open Libcrux_ml_dsa.Simd.Traits in () -val generate_domain_separator (row column: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True) - -val update_matrix - (#v_SIMDUnit: Type0) - (v_ROWS_IN_A v_COLUMNS_IN_A: usize) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} - (m: - t_Array +/// The x4 sampling implementation that is selected during multiplexing. +class t_X4Sampler (v_Self: Type0) = { + f_matrix_A_pre: + #v_SIMDUnit: Type0 -> + v_ROWS_IN_A: usize -> + v_COLUMNS_IN_A: usize -> + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} -> + t_Array u8 (sz 34) + -> Type0; + f_matrix_A_post: + #v_SIMDUnit: Type0 -> + v_ROWS_IN_A: usize -> + v_COLUMNS_IN_A: usize -> + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} -> + t_Array u8 (sz 34) -> + t_Array + (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) + v_ROWS_IN_A + -> Type0; + f_matrix_A: + #v_SIMDUnit: Type0 -> + v_ROWS_IN_A: usize -> + v_COLUMNS_IN_A: usize -> + {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} -> + x0: t_Array u8 (sz 34) + -> Prims.Pure + (t_Array (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) v_ROWS_IN_A) - (i j: usize) - (v: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) - : Prims.Pure - (t_Array - (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) - v_ROWS_IN_A) Prims.l_True (fun _ -> Prims.l_True) + (f_matrix_A_pre #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A #i1 x0) + (fun result -> f_matrix_A_post #v_SIMDUnit v_ROWS_IN_A v_COLUMNS_IN_A #i1 x0 result) +} val matrix_A_4_by_4_ - (#v_SIMDUnit: Type0) + (#v_SIMDUnit #v_Shake128: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A: usize) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i3: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128 |} (seed: t_Array u8 (sz 34)) : Prims.Pure (t_Array @@ -38,9 +56,10 @@ val matrix_A_4_by_4_ v_ROWS_IN_A) Prims.l_True (fun _ -> Prims.l_True) val matrix_A_6_by_5_ - (#v_SIMDUnit: Type0) + (#v_SIMDUnit #v_Shake128: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A: usize) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i3: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128 |} (seed: t_Array u8 (sz 34)) : Prims.Pure (t_Array @@ -48,19 +67,21 @@ val matrix_A_6_by_5_ v_ROWS_IN_A) Prims.l_True (fun _ -> Prims.l_True) val matrix_A_8_by_7_ - (#v_SIMDUnit: Type0) + (#v_SIMDUnit #v_Shake128: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A: usize) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i3: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128 |} (seed: t_Array u8 (sz 34)) : Prims.Pure (t_Array (t_Array (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) v_COLUMNS_IN_A) v_ROWS_IN_A) Prims.l_True (fun _ -> Prims.l_True) -val matrix_A - (#v_SIMDUnit: Type0) +val matrix_A_generic + (#v_SIMDUnit #v_Shake128: Type0) (v_ROWS_IN_A v_COLUMNS_IN_A: usize) - {| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i2: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |} + {| i3: Libcrux_ml_dsa.Hash_functions.Shake128.t_XofX4 v_Shake128 |} (seed: t_Array u8 (sz 34)) : Prims.Pure (t_Array diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst index 8dc299c31..5d2d5a9a6 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fst @@ -23,6 +23,18 @@ let from_coefficient_array (coefficient_array: t_Slice i32) = #FStar.Tactics.Typeclasses.solve (Libcrux_intrinsics.Avx2_extract.mm256_loadu_si256_i32 coefficient_array <: u8) +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Clone.t_Clone t_AVX2SIMDUnit + +let impl_1 = impl_1' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_2': Core.Marker.t_Copy t_AVX2SIMDUnit + +let impl_2 = impl_2' + let to_coefficient_array (x: t_AVX2SIMDUnit) = let coefficient_array:t_Array i32 (sz 8) = Rust_primitives.Hax.repeat 0l (sz 8) in let coefficient_array:t_Array i32 (sz 8) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fsti index e14bacddd..e5d296f3a 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Avx2.Vector_type.fsti @@ -13,5 +13,11 @@ val v_ZERO: Prims.unit -> Prims.Pure t_AVX2SIMDUnit Prims.l_True (fun _ -> Prims val from_coefficient_array (coefficient_array: t_Slice i32) : Prims.Pure t_AVX2SIMDUnit Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Clone.t_Clone t_AVX2SIMDUnit + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_2:Core.Marker.t_Copy t_AVX2SIMDUnit + val to_coefficient_array (x: t_AVX2SIMDUnit) : Prims.Pure (t_Array i32 (sz 8)) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst index 338234407..cf5cb8df2 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fst @@ -25,5 +25,17 @@ let from_coefficient_array (array: t_Slice i32) = let to_coefficient_array (x: t_PortableSIMDUnit) = x.f_coefficients +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl': Core.Clone.t_Clone t_PortableSIMDUnit + +let impl = impl' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': Core.Marker.t_Copy t_PortableSIMDUnit + +let impl_1 = impl_1' + let v_ZERO (_: Prims.unit) = { f_coefficients = Rust_primitives.Hax.repeat 0l (sz 8) } <: t_PortableSIMDUnit diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fsti index 0b3010e59..f30200b21 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Simd.Portable.Vector_type.fsti @@ -11,4 +11,10 @@ val from_coefficient_array (array: t_Slice i32) val to_coefficient_array (x: t_PortableSIMDUnit) : Prims.Pure (t_Array i32 (sz 8)) Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_PortableSIMDUnit + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_PortableSIMDUnit + val v_ZERO: Prims.unit -> Prims.Pure t_PortableSIMDUnit Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst index 0a457fc6e..eee5c0b42 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fst @@ -9,17 +9,17 @@ let impl_2__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE let impl_4__len (v_SIZE: usize) (_: Prims.unit) = v_SIZE -let impl_4__as_raw (v_SIZE: usize) (self: t_MLDSASignature v_SIZE) = self.f_value +let impl_4__as_ref (v_SIZE: usize) (self: t_MLDSASignature v_SIZE) = self.f_value let impl_4__new (v_SIZE: usize) (value: t_Array u8 v_SIZE) = { f_value = value } <: t_MLDSASignature v_SIZE -let impl__as_raw (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) = self.f_value +let impl__as_ref (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) = self.f_value let impl__new (v_SIZE: usize) (value: t_Array u8 v_SIZE) = { f_value = value } <: t_MLDSASigningKey v_SIZE -let impl_2__as_raw (v_SIZE: usize) (self: t_MLDSAVerificationKey v_SIZE) = self.f_value +let impl_2__as_ref (v_SIZE: usize) (self: t_MLDSAVerificationKey v_SIZE) = self.f_value let impl_2__new (v_SIZE: usize) (value: t_Array u8 v_SIZE) = { f_value = value } <: t_MLDSAVerificationKey v_SIZE @@ -36,6 +36,36 @@ let t_VerificationError_cast_to_repr (x: t_VerificationError) = | VerificationError_CommitmentHashesDontMatchError -> isz 3 | VerificationError_VerificationContextTooLongError -> isz 6 +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_1': v_SIZE: usize -> Core.Clone.t_Clone (t_MLDSASigningKey v_SIZE) + +let impl_1 (v_SIZE: usize) = impl_1' v_SIZE + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_3': v_SIZE: usize -> Core.Clone.t_Clone (t_MLDSAVerificationKey v_SIZE) + +let impl_3 (v_SIZE: usize) = impl_3' v_SIZE + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_5': v_SIZE: usize -> Core.Clone.t_Clone (t_MLDSASignature v_SIZE) + +let impl_5 (v_SIZE: usize) = impl_5' v_SIZE + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_6': Core.Fmt.t_Debug t_VerificationError + +let impl_6 = impl_6' + +[@@ FStar.Tactics.Typeclasses.tcinstance] +assume +val impl_7': Core.Fmt.t_Debug t_SigningError + +let impl_7 = impl_7' + let impl__as_slice (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) = self.f_value <: t_Slice u8 let impl_2__as_slice (v_SIZE: usize) (self: t_MLDSAVerificationKey v_SIZE) = diff --git a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fsti b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fsti index 0a03514df..ee4a22f89 100644 --- a/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fsti +++ b/libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Types.fsti @@ -18,7 +18,7 @@ val impl_4__len: v_SIZE: usize -> Prims.unit type t_MLDSASignature (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } /// A reference to the raw byte array. -val impl_4__as_raw (v_SIZE: usize) (self: t_MLDSASignature v_SIZE) +val impl_4__as_ref (v_SIZE: usize) (self: t_MLDSASignature v_SIZE) : Prims.Pure (t_Array u8 v_SIZE) Prims.l_True (fun _ -> Prims.l_True) /// Build @@ -29,7 +29,7 @@ val impl_4__new (v_SIZE: usize) (value: t_Array u8 v_SIZE) type t_MLDSASigningKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } /// A reference to the raw byte array. -val impl__as_raw (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) +val impl__as_ref (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) : Prims.Pure (t_Array u8 v_SIZE) Prims.l_True (fun _ -> Prims.l_True) /// Build @@ -40,7 +40,7 @@ val impl__new (v_SIZE: usize) (value: t_Array u8 v_SIZE) type t_MLDSAVerificationKey (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } /// A reference to the raw byte array. -val impl_2__as_raw (v_SIZE: usize) (self: t_MLDSAVerificationKey v_SIZE) +val impl_2__as_ref (v_SIZE: usize) (self: t_MLDSAVerificationKey v_SIZE) : Prims.Pure (t_Array u8 v_SIZE) Prims.l_True (fun _ -> Prims.l_True) /// Build @@ -69,6 +69,21 @@ type t_VerificationError = val t_VerificationError_cast_to_repr (x: t_VerificationError) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1 (v_SIZE: usize) : Core.Clone.t_Clone (t_MLDSASigningKey v_SIZE) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_3 (v_SIZE: usize) : Core.Clone.t_Clone (t_MLDSAVerificationKey v_SIZE) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_5 (v_SIZE: usize) : Core.Clone.t_Clone (t_MLDSASignature v_SIZE) + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_6:Core.Fmt.t_Debug t_VerificationError + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_7:Core.Fmt.t_Debug t_SigningError + /// A reference to the raw byte slice. val impl__as_slice (v_SIZE: usize) (self: t_MLDSASigningKey v_SIZE) : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True) diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti index 968a5585c..0c9c90e71 100644 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti +++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.X86.fsti @@ -38,6 +38,12 @@ type t_Feature = val t_Feature_cast_to_repr (x: t_Feature) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True) +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl:Core.Clone.t_Clone t_Feature + +[@@ FStar.Tactics.Typeclasses.tcinstance] +val impl_1:Core.Marker.t_Copy t_Feature + /// Initialize CPU detection. val init: Prims.unit -> Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)