Skip to content

Commit

Permalink
Updated F* extraction
Browse files Browse the repository at this point in the history
  • Loading branch information
jschneider-bensch committed Jan 7, 2025
1 parent 019b839 commit da62157
Show file tree
Hide file tree
Showing 50 changed files with 7,498 additions and 234 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module Libcrux_ml_dsa.Constants.Ml_dsa_44_
#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
open Core
open FStar.Mul

let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 6

let v_BITS_PER_ERROR_COEFFICIENT: usize = sz 3

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 18

let v_COLUMNS_IN_A: usize = sz 4

let v_COMMITMENT_HASH_SIZE: usize = sz 32

let v_ETA: Libcrux_ml_dsa.Constants.t_Eta =
Libcrux_ml_dsa.Constants.Eta_Two <: Libcrux_ml_dsa.Constants.t_Eta

let v_GAMMA1_EXPONENT: usize = sz 17

let v_MAX_ONES_IN_HINT: usize = sz 80

let v_ONES_IN_VERIFIER_CHALLENGE: usize = sz 39

let v_ROWS_IN_A: usize = sz 4

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 88l
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module Libcrux_ml_dsa.Constants.Ml_dsa_65_
#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
open Core
open FStar.Mul

let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 4

let v_BITS_PER_ERROR_COEFFICIENT: usize = sz 4

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 20

let v_COLUMNS_IN_A: usize = sz 5

let v_COMMITMENT_HASH_SIZE: usize = sz 48

let v_ETA: Libcrux_ml_dsa.Constants.t_Eta =
Libcrux_ml_dsa.Constants.Eta_Four <: Libcrux_ml_dsa.Constants.t_Eta

let v_GAMMA1_EXPONENT: usize = sz 19

let v_MAX_ONES_IN_HINT: usize = sz 55

let v_ONES_IN_VERIFIER_CHALLENGE: usize = sz 49

let v_ROWS_IN_A: usize = sz 6

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 32l
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
module Libcrux_ml_dsa.Constants.Ml_dsa_87_
#set-options "--fuel 0 --ifuel 1 --z3rlimit 100"
open Core
open FStar.Mul

let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 4

let v_BITS_PER_ERROR_COEFFICIENT: usize = sz 3

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 20

let v_COLUMNS_IN_A: usize = sz 7

let v_COMMITMENT_HASH_SIZE: usize = sz 64

let v_ETA: Libcrux_ml_dsa.Constants.t_Eta =
Libcrux_ml_dsa.Constants.Eta_Two <: Libcrux_ml_dsa.Constants.t_Eta

let v_GAMMA1_EXPONENT: usize = sz 19

let v_MAX_ONES_IN_HINT: usize = sz 75

let v_ONES_IN_VERIFIER_CHALLENGE: usize = sz 60

let v_ROWS_IN_A: usize = sz 8

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 32l
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,10 @@ val init_absorb_x4':
let init_absorb_x4 = init_absorb_x4'

assume
val shake128': v_OUTPUT_LENGTH: usize -> input: t_Slice u8 -> out: t_Array u8 v_OUTPUT_LENGTH
-> Prims.Pure (t_Array u8 v_OUTPUT_LENGTH) Prims.l_True (fun _ -> Prims.l_True)
val shake128': input: t_Slice u8 -> out: t_Slice u8
-> Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

let shake128 (v_OUTPUT_LENGTH: usize) = shake128' v_OUTPUT_LENGTH
let shake128 = shake128'

assume
val shake256': v_OUTPUT_LENGTH: usize -> input: t_Slice u8 -> out: t_Array u8 v_OUTPUT_LENGTH
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,7 @@ val init_absorb_final_shake256 (input: t_Slice u8)
val init_absorb_x4 (input0 input1 input2 input3: t_Slice u8)
: Prims.Pure t_Shake256X4 Prims.l_True (fun _ -> Prims.l_True)

val shake128 (v_OUTPUT_LENGTH: usize) (input: t_Slice u8) (out: t_Array u8 v_OUTPUT_LENGTH)
: Prims.Pure (t_Array u8 v_OUTPUT_LENGTH) Prims.l_True (fun _ -> Prims.l_True)
val shake128 (input out: t_Slice u8) : Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val shake256 (v_OUTPUT_LENGTH: usize) (input: t_Slice u8) (out: t_Array u8 v_OUTPUT_LENGTH)
: Prims.Pure (t_Array u8 v_OUTPUT_LENGTH) Prims.l_True (fun _ -> Prims.l_True)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,17 +4,10 @@ open Core
open FStar.Mul

class t_Xof (v_Self: Type0) = {
f_shake128_pre:v_OUTPUT_LENGTH: usize -> t_Slice u8 -> t_Array u8 v_OUTPUT_LENGTH -> Type0;
f_shake128_post:
v_OUTPUT_LENGTH: usize ->
t_Slice u8 ->
t_Array u8 v_OUTPUT_LENGTH ->
t_Array u8 v_OUTPUT_LENGTH
-> Type0;
f_shake128:v_OUTPUT_LENGTH: usize -> x0: t_Slice u8 -> x1: t_Array u8 v_OUTPUT_LENGTH
-> Prims.Pure (t_Array u8 v_OUTPUT_LENGTH)
(f_shake128_pre v_OUTPUT_LENGTH x0 x1)
(fun result -> f_shake128_post v_OUTPUT_LENGTH x0 x1 result)
f_shake128_pre:t_Slice u8 -> t_Slice u8 -> Type0;
f_shake128_post:t_Slice u8 -> t_Slice u8 -> t_Slice u8 -> Type0;
f_shake128:x0: t_Slice u8 -> x1: t_Slice u8
-> Prims.Pure (t_Slice u8) (f_shake128_pre x0 x1) (fun result -> f_shake128_post x0 x1 result)
}

/// When sampling matrix A we always want to do 4 absorb/squeeze calls in
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,22 @@ let sign_pre_hashed_shake128
(message context: t_Slice u8)
(randomness: t_Array u8 (sz 32))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
randomness
let pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
Libcrux_ml_dsa.Types.t_SigningError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
pre_hash_buffer
randomness
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out

let verify
(verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
Expand All @@ -70,11 +78,18 @@ let verify_pre_hashed_shake128
(message context: t_Slice u8)
(signature: Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.verify_pre_hashed_shake128 (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 pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Avx2.Ml_dsa_44_.verify_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl_2__as_ref
(sz 1312)
verification_key
<:
t_Array u8 (sz 1312))
message
context
pre_hash_buffer
(Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,22 @@ let sign_pre_hashed_shake128
(message context: t_Slice u8)
(randomness: t_Array u8 (sz 32))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
randomness
let pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
Libcrux_ml_dsa.Types.t_SigningError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
pre_hash_buffer
randomness
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out

let verify
(verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
Expand All @@ -70,11 +78,18 @@ let verify_pre_hashed_shake128
(message context: t_Slice u8)
(signature: Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.verify_pre_hashed_shake128 (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 pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Neon.Ml_dsa_44_.verify_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl_2__as_ref
(sz 1312)
verification_key
<:
t_Array u8 (sz 1312))
message
context
pre_hash_buffer
(Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,22 @@ let sign_pre_hashed_shake128
(message context: t_Slice u8)
(randomness: t_Array u8 (sz 32))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
randomness
let pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
Libcrux_ml_dsa.Types.t_SigningError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
pre_hash_buffer
randomness
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out

let verify
(verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
Expand All @@ -70,11 +78,18 @@ let verify_pre_hashed_shake128
(message context: t_Slice u8)
(signature: Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
=
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.verify_pre_hashed_shake128 (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 pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
Libcrux_ml_dsa.Ml_dsa_generic.Instantiations.Portable.Ml_dsa_44_.verify_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl_2__as_ref
(sz 1312)
verification_key
<:
t_Array u8 (sz 1312))
message
context
pre_hash_buffer
(Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,22 @@ let sign_pre_hashed_shake128
(message context: t_Slice u8)
(randomness: t_Array u8 (sz 32))
=
Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
randomness
let pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result (Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
Libcrux_ml_dsa.Types.t_SigningError) =
Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.sign_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl__as_ref
(sz 2560)
signing_key
<:
t_Array u8 (sz 2560))
message
context
pre_hash_buffer
randomness
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out

let verify
(verification_key: Libcrux_ml_dsa.Types.t_MLDSAVerificationKey (sz 1312))
Expand All @@ -70,11 +78,18 @@ let verify_pre_hashed_shake128
(message context: t_Slice u8)
(signature: Libcrux_ml_dsa.Types.t_MLDSASignature (sz 2420))
=
Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.verify_pre_hashed_shake128 (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 pre_hash_buffer:t_Array u8 (sz 256) = Rust_primitives.Hax.repeat 0uy (sz 256) in
let tmp0, out:(t_Array u8 (sz 256) &
Core.Result.t_Result Prims.unit Libcrux_ml_dsa.Types.t_VerificationError) =
Libcrux_ml_dsa.Ml_dsa_generic.Multiplexing.Ml_dsa_44_.verify_pre_hashed_shake128 (Libcrux_ml_dsa.Types.impl_2__as_ref
(sz 1312)
verification_key
<:
t_Array u8 (sz 1312))
message
context
pre_hash_buffer
(Libcrux_ml_dsa.Types.impl_4__as_ref (sz 2420) signature <: t_Array u8 (sz 2420))
in
let pre_hash_buffer:t_Array u8 (sz 256) = tmp0 in
out
Loading

0 comments on commit da62157

Please sign in to comment.