Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Adapt to new hax ordering. #759

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Adapt to new hax ordering. #759

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
396 changes: 198 additions & 198 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fst
View file
Open in desktop

Large diffs are not rendered by default.

38 changes: 19 additions & 19 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Arithmetic.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,12 @@ let _ =
let open Libcrux_ml_dsa.Simd.Traits in
()

val decompose_vector
val shift_left_then_reduce
(#v_SIMDUnit: Type0)
(v_SHIFT_BY: i32)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(dimension: usize)
(gamma2: i32)
(t low high: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
: Prims.Pure
(t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

Expand All @@ -31,15 +28,26 @@ val power2round_vector
Prims.l_True
(fun _ -> Prims.l_True)

val shift_left_then_reduce
val decompose_vector
(#v_SIMDUnit: Type0)
(v_SHIFT_BY: i32)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
(dimension: usize)
(gamma2: i32)
(t low high: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
: Prims.Pure
(t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit) &
t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
Prims.l_True
(fun _ -> Prims.l_True)

val make_hint
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(low high: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
(gamma2: i32)
(hint: t_Slice (t_Array i32 (sz 256)))
: Prims.Pure (t_Slice (t_Array i32 (sz 256)) & usize) Prims.l_True (fun _ -> Prims.l_True)

val use_hint
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
Expand All @@ -56,11 +64,3 @@ val vector_infinity_norm_exceeds
(vector: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
(bound: i32)
: Prims.Pure bool Prims.l_True (fun _ -> Prims.l_True)

val make_hint
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(low high: t_Slice (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit))
(gamma2: i32)
(hint: t_Slice (t_Array i32 (sz 256)))
: Prims.Pure (t_Slice (t_Array i32 (sz 256)) & usize) Prims.l_True (fun _ -> Prims.l_True)
18 changes: 9 additions & 9 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.Ml_dsa_44_.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,25 +3,25 @@ module Libcrux_ml_dsa.Constants.Ml_dsa_44_
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_ROWS_IN_A: usize = sz 4

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_BITS_PER_ERROR_COEFFICIENT: usize = sz 3

let v_GAMMA1_EXPONENT: usize = sz 17

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 88l

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 18

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_COMMITMENT_HASH_SIZE: usize = sz 32

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 88l
let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 6
18 changes: 9 additions & 9 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.Ml_dsa_65_.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,25 +3,25 @@ module Libcrux_ml_dsa.Constants.Ml_dsa_65_
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_ROWS_IN_A: usize = sz 6

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_BITS_PER_ERROR_COEFFICIENT: usize = sz 4

let v_GAMMA1_EXPONENT: usize = sz 19

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 32l

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 20

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_COMMITMENT_HASH_SIZE: usize = sz 48

let v_GAMMA2: i32 = (Libcrux_ml_dsa.Constants.v_FIELD_MODULUS -! 1l <: i32) /! 32l
let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 4
18 changes: 9 additions & 9 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.Ml_dsa_87_.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,25 +3,25 @@ module Libcrux_ml_dsa.Constants.Ml_dsa_87_
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_ROWS_IN_A: usize = sz 8

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_BITS_PER_ERROR_COEFFICIENT: usize = sz 3

let v_GAMMA1_EXPONENT: usize = sz 19

let v_BITS_PER_GAMMA1_COEFFICIENT: usize = sz 20

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

let v_BITS_PER_COMMITMENT_COEFFICIENT: usize = sz 4

let v_COMMITMENT_HASH_SIZE: usize = sz 64
58 changes: 29 additions & 29 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,18 @@ let t_Eta_cast_to_repr (x: t_Eta) =
| Eta_Two -> discriminant_Eta_Two
| Eta_Four -> discriminant_Eta_Four

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl': Core.Clone.t_Clone t_Eta

let impl = impl'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_1': Core.Marker.t_Copy t_Eta

let impl_1 = impl_1'

let beta (ones_in_verifier_challenge: usize) (eta: t_Eta) =
let (eta_val: usize):usize =
match eta <: t_Eta with
Expand All @@ -16,30 +28,17 @@ let beta (ones_in_verifier_challenge: usize) (eta: t_Eta) =
in
cast (ones_in_verifier_challenge *! eta_val <: usize) <: i32

let commitment_ring_element_size (bits_per_commitment_coefficient: usize) =
(bits_per_commitment_coefficient *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

let commitment_vector_size (bits_per_commitment_coefficient rows_in_a: usize) =
(commitment_ring_element_size bits_per_commitment_coefficient <: usize) *! rows_in_a

let error_ring_element_size (bits_per_error_coefficient: usize) =
(bits_per_error_coefficient *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

let gamma1_ring_element_size (bits_per_gamma1_coefficient: usize) =
(bits_per_gamma1_coefficient *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

let signature_size
(rows_in_a columns_in_a max_ones_in_hint commitment_hash_size bits_per_gamma1_coefficient:
usize)
=
((commitment_hash_size +!
(columns_in_a *! (gamma1_ring_element_size bits_per_gamma1_coefficient <: usize) <: usize)
<:
usize) +!
max_ones_in_hint
<:
usize) +!
rows_in_a
let commitment_ring_element_size (bits_per_commitment_coefficient: usize) =
(bits_per_commitment_coefficient *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

let commitment_vector_size (bits_per_commitment_coefficient rows_in_a: usize) =
(commitment_ring_element_size bits_per_commitment_coefficient <: usize) *! rows_in_a

let signing_key_size (rows_in_a columns_in_a error_ring_element_size: usize) =
(((v_SEED_FOR_A_SIZE +! v_SEED_FOR_SIGNING_SIZE <: usize) +! v_BYTES_FOR_VERIFICATION_KEY_HASH
Expand All @@ -60,14 +59,15 @@ let verification_key_size (rows_in_a: usize) =
<:
usize)

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl': Core.Clone.t_Clone t_Eta

let impl = impl'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl_1': Core.Marker.t_Copy t_Eta

let impl_1 = impl_1'
let signature_size
(rows_in_a columns_in_a max_ones_in_hint commitment_hash_size bits_per_gamma1_coefficient:
usize)
=
((commitment_hash_size +!
(columns_in_a *! (gamma1_ring_element_size bits_per_gamma1_coefficient <: usize) <: usize)
<:
usize) +!
max_ones_in_hint
<:
usize) +!
rows_in_a
86 changes: 43 additions & 43 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Constants.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,88 +3,88 @@ module Libcrux_ml_dsa.Constants
open Core
open FStar.Mul

let discriminant_Eta_Four: isize = isz 4

/// Eta values
type t_Eta =
| Eta_Two : t_Eta
| Eta_Four : t_Eta
let v_FIELD_MODULUS: i32 = 8380417l

let discriminant_Eta_Two: isize = isz 2
let v_COEFFICIENTS_IN_RING_ELEMENT: usize = sz 256

val t_Eta_cast_to_repr (x: t_Eta) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True)
let v_FIELD_MODULUS_MINUS_ONE_BIT_LENGTH: usize = sz 23

let v_BITS_IN_LOWER_PART_OF_T: usize = sz 13

let v_BYTES_FOR_VERIFICATION_KEY_HASH: usize = sz 64

let v_COEFFICIENTS_IN_RING_ELEMENT: usize = sz 256
let v_RING_ELEMENT_OF_T0S_SIZE: usize =
(v_BITS_IN_LOWER_PART_OF_T *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

/// The length of `context` is serialized to a single `u8`.
let v_CONTEXT_MAX_LEN: usize = sz 255
let v_BITS_IN_UPPER_PART_OF_T: usize =
v_FIELD_MODULUS_MINUS_ONE_BIT_LENGTH -! v_BITS_IN_LOWER_PART_OF_T

let v_FIELD_MODULUS: i32 = 8380417l
let v_RING_ELEMENT_OF_T1S_SIZE: usize =
(v_BITS_IN_UPPER_PART_OF_T *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8

let v_FIELD_MODULUS_MINUS_ONE_BIT_LENGTH: usize = sz 23
let v_SEED_FOR_A_SIZE: usize = sz 32

let v_BITS_IN_UPPER_PART_OF_T: usize =
v_FIELD_MODULUS_MINUS_ONE_BIT_LENGTH -! v_BITS_IN_LOWER_PART_OF_T
let v_SEED_FOR_ERROR_VECTORS_SIZE: usize = sz 64

let v_GAMMA2_V261_888_: i32 = 261888l
let v_BYTES_FOR_VERIFICATION_KEY_HASH: usize = sz 64

let v_GAMMA2_V95_232_: i32 = 95232l
let v_SEED_FOR_SIGNING_SIZE: usize = sz 32

/// Number of bytes of entropy required for key generation.
let v_KEY_GENERATION_RANDOMNESS_SIZE: usize = sz 32

let v_MASK_SEED_SIZE: usize = sz 64
/// Number of bytes of entropy required for signing.
let v_SIGNING_RANDOMNESS_SIZE: usize = sz 32

let v_MESSAGE_REPRESENTATIVE_SIZE: usize = sz 64

let v_MASK_SEED_SIZE: usize = sz 64

let v_REJECTION_SAMPLE_BOUND_SIGN: usize = sz 814

let v_RING_ELEMENT_OF_T0S_SIZE: usize =
(v_BITS_IN_LOWER_PART_OF_T *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8
/// The length of `context` is serialized to a single `u8`.
let v_CONTEXT_MAX_LEN: usize = sz 255

let v_RING_ELEMENT_OF_T1S_SIZE: usize =
(v_BITS_IN_UPPER_PART_OF_T *! v_COEFFICIENTS_IN_RING_ELEMENT <: usize) /! sz 8
/// Eta values
type t_Eta =
| Eta_Two : t_Eta
| Eta_Four : t_Eta

let v_SEED_FOR_A_SIZE: usize = sz 32
let discriminant_Eta_Two: isize = isz 2

let v_SEED_FOR_ERROR_VECTORS_SIZE: usize = sz 64
let discriminant_Eta_Four: isize = isz 4

let v_SEED_FOR_SIGNING_SIZE: usize = sz 32
val t_Eta_cast_to_repr (x: t_Eta) : Prims.Pure isize Prims.l_True (fun _ -> Prims.l_True)

/// Number of bytes of entropy required for signing.
let v_SIGNING_RANDOMNESS_SIZE: usize = sz 32
[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl:Core.Clone.t_Clone t_Eta

val beta (ones_in_verifier_challenge: usize) (eta: t_Eta)
: Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)
[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_1:Core.Marker.t_Copy t_Eta

val commitment_ring_element_size (bits_per_commitment_coefficient: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
let v_GAMMA2_V261_888_: i32 = 261888l

val commitment_vector_size (bits_per_commitment_coefficient rows_in_a: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
let v_GAMMA2_V95_232_: i32 = 95232l

val beta (ones_in_verifier_challenge: usize) (eta: t_Eta)
: Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

val error_ring_element_size (bits_per_error_coefficient: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

val gamma1_ring_element_size (bits_per_gamma1_coefficient: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

val signature_size
(rows_in_a columns_in_a max_ones_in_hint commitment_hash_size bits_per_gamma1_coefficient:
usize)
val commitment_ring_element_size (bits_per_commitment_coefficient: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

val commitment_vector_size (bits_per_commitment_coefficient rows_in_a: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

val signing_key_size (rows_in_a columns_in_a error_ring_element_size: usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

val verification_key_size (rows_in_a: usize) : Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl:Core.Clone.t_Clone t_Eta

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl_1:Core.Marker.t_Copy t_Eta
val signature_size
(rows_in_a columns_in_a max_ones_in_hint commitment_hash_size bits_per_gamma1_coefficient:
usize)
: Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
Loading
Loading