-
Notifications
You must be signed in to change notification settings - Fork 15
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #642 from cryspen/jonas/ml-dsa-target-feature
ML-DSA: AVX2 target feature
- Loading branch information
Showing
69 changed files
with
4,016 additions
and
1,468 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
97 changes: 97 additions & 0 deletions
97
...roofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fst
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,97 @@ | ||
| module Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature | ||
| #set-options "--fuel 0 --ifuel 1 --z3rlimit 100" | ||
| open Core | ||
| 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.Hash_functions.Simd256 in | ||
| let open Libcrux_ml_dsa.Pre_hash in | ||
| let open Libcrux_ml_dsa.Simd.Avx2 in | ||
| let open Libcrux_ml_dsa.Simd.Traits in | ||
| () | ||
|
|
||
| let generate_key_pair | ||
| (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE: | ||
| usize) | ||
| (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.Hash_functions.Simd256.t_Shake256 | ||
| #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 v_ROWS_IN_A v_COLUMNS_IN_A v_ETA | ||
| v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE randomness | ||
|
|
||
| let sign | ||
| (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) | ||
| (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (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.Hash_functions.Simd256.t_Shake256 | ||
| #Libcrux_ml_dsa.Hash_functions.Simd256.t_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 context | ||
| randomness | ||
|
|
||
| let sign_pre_hashed_shake128 | ||
| (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) | ||
| (signing_key: t_Array u8 v_SIGNING_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (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.Simd256.t_Shake128x4 | ||
| #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 | ||
| #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256x4 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH | ||
| (sz 256) 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 context randomness | ||
|
|
||
| let verify | ||
| (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) | ||
| (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (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.Hash_functions.Simd256.t_Shake256 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 message context signature | ||
|
|
||
| let verify_pre_hashed_shake128 | ||
| (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) | ||
| (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (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.Simd256.t_Shake128x4 | ||
| #Libcrux_ml_dsa.Hash_functions.Simd256.t_Shake256 #Libcrux_ml_dsa.Pre_hash.t_SHAKE128_PH | ||
| (sz 256) 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 message context signature |
78 changes: 78 additions & 0 deletions
78
...oofs/fstar/extraction/Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature.fsti
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,78 @@ | ||
| module Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Avx2_feature | ||
| #set-options "--fuel 0 --ifuel 1 --z3rlimit 100" | ||
| open Core | ||
| 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.Hash_functions.Simd256 in | ||
| let open Libcrux_ml_dsa.Pre_hash in | ||
| let open Libcrux_ml_dsa.Simd.Avx2 in | ||
| let open Libcrux_ml_dsa.Simd.Traits in | ||
| () | ||
|
|
||
| /// Generate key pair. | ||
| val generate_key_pair | ||
| (v_ROWS_IN_A v_COLUMNS_IN_A v_ETA v_ERROR_RING_ELEMENT_SIZE v_SIGNING_KEY_SIZE v_VERIFICATION_KEY_SIZE: | ||
| usize) | ||
| (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 | ||
| (fun _ -> Prims.l_True) | ||
|
|
||
| /// Sign. | ||
| val sign | ||
| (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) | ||
| (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) | ||
|
|
||
| /// Sign (pre-hashed). | ||
| val sign_pre_hashed_shake128 | ||
| (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) | ||
| (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) | ||
|
|
||
| /// Verify. | ||
| val verify | ||
| (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) | ||
| (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (signature: t_Array u8 v_SIGNATURE_SIZE) | ||
| : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) | ||
| Prims.l_True | ||
| (fun _ -> Prims.l_True) | ||
|
|
||
| /// Verify (pre-hashed with SHAKE-128). | ||
| val verify_pre_hashed_shake128 | ||
| (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) | ||
| (verification_key: t_Array u8 v_VERIFICATION_KEY_SIZE) | ||
| (message context: t_Slice u8) | ||
| (signature: t_Array u8 v_SIGNATURE_SIZE) | ||
| : Prims.Pure (Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) | ||
| Prims.l_True | ||
| (fun _ -> Prims.l_True) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.