Skip to content

Commit

Permalink
Merge pull request #774 from cryspen/adapt-to-new-hax-naming
Browse files Browse the repository at this point in the history 
Adapt to new hax naming.
  • Loading branch information
@franziskuskiefer
franziskuskiefer authored Jan 30, 2025
2 parents 7755d48 + 4602719 commit 184f22d
Show file tree
Hide file tree
Showing 23 changed files with 287 additions and 390 deletions.
130 changes: 75 additions & 55 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cca.Unpacked.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,9 @@ val unpack_public_key
v_T_AS_NTT_ENCODED_SIZE == Spec.MLKEM.v_T_AS_NTT_ENCODED_SIZE v_K)
(ensures
fun unpacked_public_key_future ->
let unpacked_public_key_future:t_MlKemPublicKeyUnpacked v_K v_Vector =
unpacked_public_key_future
in
let unpacked_public_key_future:t_MlKemPublicKeyUnpacked v_K v_Vector =
unpacked_public_key_future
in
Expand All @@ -70,13 +73,16 @@ val unpack_public_key
(valid ==>
Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
unpacked_public_key_future.f_ind_cpa_public_key.f_A ==
unpacked_public_key_future.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
matrix_A) /\
Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
unpacked_public_key_future.f_ind_cpa_public_key.f_t_as_ntt ==
deserialized_pk /\ unpacked_public_key_future.f_ind_cpa_public_key.f_seed_for_A == seed /\
unpacked_public_key_future.f_public_key_hash == public_key_hash)
unpacked_public_key_future.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
deserialized_pk /\
unpacked_public_key_future.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A ==
seed /\ unpacked_public_key_future.f_public_key_hash == public_key_hash)

/// Get the serialized public key.
val impl_3__serialized_mut
Expand All @@ -88,26 +94,28 @@ val impl_3__serialized_mut
(serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
(requires
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self
.f_ind_cpa_public_key
.f_t_as_ntt
i)))
(let self___ = self in
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))))
(ensures
fun serialized_future ->
let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE =
serialized_future
in
let self___ = self in
serialized_future.f_value ==
Seq.append (Spec.MLKEM.vector_encode_12 #v_K
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
self.f_ind_cpa_public_key.f_t_as_ntt))
self.f_ind_cpa_public_key.f_seed_for_A)
self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)

/// Get the serialized public key.
val impl_3__serialized
Expand All @@ -118,24 +126,26 @@ val impl_3__serialized
(self: t_MlKemPublicKeyUnpacked v_K v_Vector)
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
(requires
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self
.f_ind_cpa_public_key
.f_t_as_ntt
i)))
(let self___ = self in
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))))
(ensures
fun res ->
let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in
res.f_value ==
let self___ = self in
res.Libcrux_ml_kem.Types.f_value ==
Seq.append (Spec.MLKEM.vector_encode_12 #v_K
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
self.f_ind_cpa_public_key.f_t_as_ntt))
self.f_ind_cpa_public_key.f_seed_for_A)
self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
self___.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)

[@@ FStar.Tactics.Typeclasses.tcinstance]
val impl
Expand Down Expand Up @@ -187,26 +197,30 @@ val impl_4__serialized_public_key_mut
(serialized: Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
(requires
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key
.f_ind_cpa_public_key
.f_t_as_ntt
i)))
(let self___ = self in
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
.f_public_key
.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))))
(ensures
fun serialized_future ->
let serialized_future:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE =
serialized_future
in
let self___ = self in
serialized_future.f_value ==
Seq.append (Spec.MLKEM.vector_encode_12 #v_K
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)
self___.f_public_key.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
self___.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)

/// Get the serialized public key.
val impl_4__serialized_public_key
Expand All @@ -217,24 +231,28 @@ val impl_4__serialized_public_key
(self: t_MlKemKeyPairUnpacked v_K v_Vector)
: Prims.Pure (Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE)
(requires
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self.f_public_key
.f_ind_cpa_public_key
.f_t_as_ntt
i)))
(let self___ = self in
Spec.MLKEM.is_rank v_K /\
v_RANKED_BYTES_PER_RING_ELEMENT == Spec.MLKEM.v_RANKED_BYTES_PER_RING_ELEMENT v_K /\
v_PUBLIC_KEY_SIZE == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index self___
.f_public_key
.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))))
(ensures
fun res ->
let res:Libcrux_ml_kem.Types.t_MlKemPublicKey v_PUBLIC_KEY_SIZE = res in
let self___ = self in
res.f_value ==
Seq.append (Spec.MLKEM.vector_encode_12 #v_K
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
self.f_public_key.f_ind_cpa_public_key.f_t_as_ntt))
self.f_public_key.f_ind_cpa_public_key.f_seed_for_A)
self___.f_public_key.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt))
self___.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A)

/// Get the serialized private key.
val impl_4__serialized_private_key_mut
Expand Down Expand Up @@ -383,10 +401,10 @@ val encapsulate
public_key.f_public_key_hash
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
public_key.f_ind_cpa_public_key.f_t_as_ntt)
public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
public_key.f_ind_cpa_public_key.f_A)
public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A)
randomness
in
ciphertext_result.f_value == ciphertext /\ shared_secret_array == shared_secret)
Expand Down Expand Up @@ -418,13 +436,15 @@ val decapsulate
Spec.MLKEM.ind_cca_unpack_decapsulate v_K
key_pair.f_public_key.f_public_key_hash
key_pair.f_private_key.f_implicit_rejection_value
ciphertext.f_value
ciphertext.Libcrux_ml_kem.Types.f_value
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
key_pair.f_private_key.f_ind_cpa_private_key.f_secret_as_ntt)
key_pair.f_private_key.f_ind_cpa_private_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt)
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
key_pair.f_public_key.f_ind_cpa_public_key.f_t_as_ntt)
key_pair.f_public_key.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
key_pair.f_public_key.f_ind_cpa_public_key.f_A))
key_pair.f_public_key.f_ind_cpa_public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A))
20 changes: 13 additions & 7 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -636,21 +636,27 @@ let generate_keypair_unpacked
Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed
in
assert (valid ==>
((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt) ==
t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A == matrix_A_as_ntt
) /\
((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) ==
((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt) ==
t_as_ntt) /\ (public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_seed_for_A == seed_for_A) /\
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
matrix_A_as_ntt) /\
((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
private_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt) ==
secret_as_ntt));
assert ((forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index private_key
.f_secret_as_ntt
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt
i)) /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
.f_t_as_ntt
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i)))
in
private_key, public_key
Expand Down
38 changes: 29 additions & 9 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -213,11 +213,17 @@ val generate_keypair_unpacked
Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) =
temp_0_
in
let public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K
v_Vector =
public_key_future
in
let (((t_as_ntt, seed_for_A), matrix_A_as_ntt), secret_as_ntt), valid =
Spec.MLKEM.ind_cpa_generate_keypair_unpacked v_K key_generation_seed
in
(valid ==>
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key_future.f_t_as_ntt ==
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
t_as_ntt) /\ (public_key_future.f_seed_for_A == seed_for_A) /\
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key_future.f_A ==
matrix_A_as_ntt) /\
Expand All @@ -233,7 +239,7 @@ val generate_keypair_unpacked
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key_future
.f_t_as_ntt
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i)))

/// Serialize the secret key from the unpacked key pair generation.
Expand Down Expand Up @@ -354,8 +360,12 @@ val encrypt_unpacked
Spec.MLKEM.ind_cpa_encrypt_unpacked v_K
message
randomness
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector public_key.f_t_as_ntt)
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector public_key.f_A))
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt)
(Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
public_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A))

val build_unpacked_public_key_mut
(v_K v_T_AS_NTT_ENCODED_SIZE: usize)
Expand All @@ -370,6 +380,10 @@ val build_unpacked_public_key_mut
length public_key == Spec.MLKEM.v_CPA_PUBLIC_KEY_SIZE v_K)
(ensures
fun unpacked_public_key_future ->
let unpacked_public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked
v_K v_Vector =
unpacked_public_key_future
in
let unpacked_public_key_future:Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked
v_K v_Vector =
unpacked_public_key_future
Expand All @@ -379,9 +393,11 @@ val build_unpacked_public_key_mut
let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #v_K seed_for_A in
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
unpacked_public_key_future.f_t_as_ntt ==
unpacked_public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
t_as_ntt /\ valid ==>
Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector unpacked_public_key_future.f_A ==
Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
unpacked_public_key_future.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
Spec.MLKEM.matrix_transpose matrix_A_as_ntt))

val build_unpacked_public_key
Expand All @@ -402,9 +418,13 @@ val build_unpacked_public_key
let t_as_ntt_bytes, seed_for_A = split public_key v_T_AS_NTT_ENCODED_SIZE in
let t_as_ntt = Spec.MLKEM.vector_decode_12 #v_K t_as_ntt_bytes in
let matrix_A_as_ntt, valid = Spec.MLKEM.sample_matrix_A_ntt #v_K seed_for_A in
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector result.f_t_as_ntt == t_as_ntt /\
valid ==>
Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K #v_Vector result.f_A ==
(Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K
#v_Vector
result.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt ==
t_as_ntt /\ valid ==>
Libcrux_ml_kem.Polynomial.to_spec_matrix_t #v_K
#v_Vector
result.Libcrux_ml_kem.Ind_cpa.Unpacked.f_A ==
Spec.MLKEM.matrix_transpose matrix_A_as_ntt))

val encrypt
Expand Down
18 changes: 10 additions & 8 deletions libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Mlkem1024.Avx2.Unpacked.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ val serialized_public_key
forall (i: nat).
i < 4 ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index public_key
.f_ind_cpa_public_key
.f_t_as_ntt
.Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))
(fun _ -> Prims.l_True)

Expand Down Expand Up @@ -68,9 +68,10 @@ val key_pair_serialized_public_key_mut
(requires
forall (i: nat).
i < 4 ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
.f_ind_cpa_public_key
.f_t_as_ntt
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
.Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
.Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))
(fun _ -> Prims.l_True)

Expand All @@ -83,9 +84,10 @@ val key_pair_serialized_public_key
(requires
forall (i: nat).
i < 4 ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair.f_public_key
.f_ind_cpa_public_key
.f_t_as_ntt
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index key_pair
.Libcrux_ml_kem.Ind_cca.Unpacked.f_public_key
.Libcrux_ml_kem.Ind_cca.Unpacked.f_ind_cpa_public_key
.Libcrux_ml_kem.Ind_cpa.Unpacked.f_t_as_ntt
i))
(fun _ -> Prims.l_True)

Expand Down
Loading

0 comments on commit 184f22d

Please sign in to comment.