diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti
index b5a8cb0e..380fec1b 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Avx2.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
result == Spec.Utils.v_PRF v_LEN input)
val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K)
- : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+ : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+ (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+ (ensures
+ fun result ->
+ let result:t_Array (t_Array u8 v_LEN) v_K = result in
+ result == Spec.Utils.v_PRFxN v_K v_LEN input)
/// The state.
/// It\'s only used for SHAKE128.
@@ -63,7 +68,10 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd256Hash v_K =
(fun (v_LEN: usize) (input: t_Slice u8) (out: t_Array u8 v_LEN) ->
v v_LEN < pow2 32 ==> out == Spec.Utils.v_PRF v_LEN input);
f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
- f_PRFxN_pre = (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> true);
+ f_PRFxN_pre
+ =
+ (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) ->
+ v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
f_PRFxN_post
=
(fun
@@ -71,7 +79,8 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd256Hash v_K =
(input: t_Array (t_Array u8 (sz 33)) v_K)
(out: t_Array (t_Array u8 v_LEN) v_K)
->
- true);
+ (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+ out == Spec.Utils.v_PRFxN v_K v_LEN input);
f_PRFxN
=
(fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> v_PRFxN v_K v_LEN input);
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti
index 5294a8dc..94eb62c9 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Neon.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
result == Spec.Utils.v_PRF v_LEN input)
val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K)
- : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+ : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+ (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+ (ensures
+ fun result ->
+ let result:t_Array (t_Array u8 v_LEN) v_K = result in
+ result == Spec.Utils.v_PRFxN v_K v_LEN input)
/// The state.
/// It\'s only used for SHAKE128.
@@ -63,7 +68,10 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd128Hash v_K =
(fun (v_LEN: usize) (input: t_Slice u8) (out: t_Array u8 v_LEN) ->
v v_LEN < pow2 32 ==> out == Spec.Utils.v_PRF v_LEN input);
f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
- f_PRFxN_pre = (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> true);
+ f_PRFxN_pre
+ =
+ (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) ->
+ v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
f_PRFxN_post
=
(fun
@@ -71,7 +79,8 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash t_Simd128Hash v_K =
(input: t_Array (t_Array u8 (sz 33)) v_K)
(out: t_Array (t_Array u8 v_LEN) v_K)
->
- true);
+ (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+ out == Spec.Utils.v_PRFxN v_K v_LEN input);
f_PRFxN
=
(fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> v_PRFxN v_K v_LEN input);
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti
index 89c8300f..e0222ac2 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.Portable.fsti
@@ -28,7 +28,12 @@ val v_PRF (v_LEN: usize) (input: t_Slice u8)
result == Spec.Utils.v_PRF v_LEN input)
val v_PRFxN (v_K v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K)
- : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K) Prims.l_True (fun _ -> Prims.l_True)
+ : Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
+ (requires v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4))
+ (ensures
+ fun result ->
+ let result:t_Array (t_Array u8 v_LEN) v_K = result in
+ result == Spec.Utils.v_PRFxN v_K v_LEN input)
/// The state.
/// It\'s only used for SHAKE128.
@@ -63,7 +68,10 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash (t_PortableHash v_K
(fun (v_LEN: usize) (input: t_Slice u8) (out: t_Array u8 v_LEN) ->
v v_LEN < pow2 32 ==> out == Spec.Utils.v_PRF v_LEN input);
f_PRF = (fun (v_LEN: usize) (input: t_Slice u8) -> v_PRF v_LEN input);
- f_PRFxN_pre = (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> true);
+ f_PRFxN_pre
+ =
+ (fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) ->
+ v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4));
f_PRFxN_post
=
(fun
@@ -71,7 +79,8 @@ let impl (v_K: usize) : Libcrux_ml_kem.Hash_functions.t_Hash (t_PortableHash v_K
(input: t_Array (t_Array u8 (sz 33)) v_K)
(out: t_Array (t_Array u8 v_LEN) v_K)
->
- true);
+ (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+ out == Spec.Utils.v_PRFxN v_K v_LEN input);
f_PRFxN
=
(fun (v_LEN: usize) (input: t_Array (t_Array u8 (sz 33)) v_K) -> v_PRFxN v_K v_LEN input);
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti
index 076ee08e..f734de67 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti
@@ -25,9 +25,17 @@ class t_Hash (v_Self: Type0) (v_K: usize) = {
-> pred: Type0{pred ==> v v_LEN < pow2 32 ==> result == Spec.Utils.v_PRF v_LEN input};
f_PRF:v_LEN: usize -> x0: t_Slice u8
-> Prims.Pure (t_Array u8 v_LEN) (f_PRF_pre v_LEN x0) (fun result -> f_PRF_post v_LEN x0 result);
- f_PRFxN_pre:v_LEN: usize -> input: t_Array (t_Array u8 (sz 33)) v_K -> pred: Type0{true ==> pred};
- f_PRFxN_post:v_LEN: usize -> t_Array (t_Array u8 (sz 33)) v_K -> t_Array (t_Array u8 v_LEN) v_K
- -> Type0;
+ f_PRFxN_pre:v_LEN: usize -> input: t_Array (t_Array u8 (sz 33)) v_K
+ -> pred: Type0{v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4) ==> pred};
+ f_PRFxN_post:
+ v_LEN: usize ->
+ input: t_Array (t_Array u8 (sz 33)) v_K ->
+ result: t_Array (t_Array u8 v_LEN) v_K
+ -> pred:
+ Type0
+ { pred ==>
+ (v v_LEN < pow2 32 /\ (v v_K == 2 \/ v v_K == 3 \/ v v_K == 4)) ==>
+ result == Spec.Utils.v_PRFxN v_K v_LEN input };
f_PRFxN:v_LEN: usize -> x0: t_Array (t_Array u8 (sz 33)) v_K
-> Prims.Pure (t_Array (t_Array u8 v_LEN) v_K)
(f_PRFxN_pre v_LEN x0)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
index 4821be2e..fbdbe501 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fst
@@ -12,6 +12,8 @@ let _ =
let open Libcrux_ml_kem.Vector.Traits in
()
+#push-options "--max_fuel 10 --z3rlimit 1000 --ext context_pruning --z3refresh --split_queries always"
+
let sample_ring_element_cbd
(v_K v_ETA2_RANDOMNESS_SIZE v_ETA2: usize)
(#v_Vector #v_Hasher: Type0)
@@ -35,13 +37,22 @@ let sample_ring_element_cbd
in
let prf_inputs:t_Array (t_Array u8 (sz 33)) v_K = Rust_primitives.Hax.repeat prf_input v_K in
let v__domain_separator_init:u8 = domain_separator in
+ let v__prf_inputs_init:t_Array (t_Array u8 (sz 33)) v_K = prf_inputs in
let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) =
Rust_primitives.Hax.Folds.fold_range (sz 0)
v_K
(fun temp_0_ i ->
let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in
let i:usize = i in
- v domain_separator == v v__domain_separator_init + v i)
+ v domain_separator == v v__domain_separator_init + v i /\
+ (v i < v v_K ==>
+ (forall (j: nat).
+ (j >= v i /\ j < v v_K) ==> prf_inputs.[ sz j ] == v__prf_inputs_init.[ sz j ])) /\
+ (forall (j: nat).
+ j < v i ==>
+ v (Seq.index (Seq.index prf_inputs j) 32) == v v__domain_separator_init + j /\
+ Seq.slice (Seq.index prf_inputs j) 0 32 ==
+ Seq.slice (Seq.index v__prf_inputs_init j) 0 32))
(domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K))
(fun temp_0_ i ->
let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in
@@ -60,6 +71,28 @@ let sample_ring_element_cbd
let domain_separator:u8 = domain_separator +! 1uy in
domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K))
in
+ let _:Prims.unit =
+ let lemma_aux (i: nat{i < v v_K})
+ : Lemma
+ (prf_inputs.[ sz i ] ==
+ (Seq.append (Seq.slice prf_input 0 32)
+ (Seq.create 1
+ (mk_int #u8_inttype (v (v__domain_separator_init +! (mk_int #u8_inttype i))))))) =
+ Lib.Sequence.eq_intro #u8
+ #33
+ prf_inputs.[ sz i ]
+ (Seq.append (Seq.slice prf_input 0 32)
+ (Seq.create 1 (mk_int #u8_inttype (v v__domain_separator_init + i))))
+ in
+ Classical.forall_intro lemma_aux;
+ Lib.Sequence.eq_intro #(t_Array u8 (sz 33))
+ #(v v_K)
+ prf_inputs
+ (createi v_K
+ (Spec.MLKEM.sample_vector_cbd2_prf_input #v_K
+ (Seq.slice prf_input 0 32)
+ (sz (v v__domain_separator_init))))
+ in
let (prf_outputs: t_Array (t_Array u8 v_ETA2_RANDOMNESS_SIZE) v_K):t_Array
(t_Array u8 v_ETA2_RANDOMNESS_SIZE) v_K =
Libcrux_ml_kem.Hash_functions.f_PRFxN #v_Hasher
@@ -71,37 +104,45 @@ let sample_ring_element_cbd
let error_1_:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K =
Rust_primitives.Hax.Folds.fold_range (sz 0)
v_K
- (fun error_1_ temp_1_ ->
+ (fun error_1_ i ->
let error_1_:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K =
error_1_
in
- let _:usize = temp_1_ in
- true)
+ let i:usize = i in
+ forall (j: nat).
+ j < v i ==>
+ Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector error_1_.[ sz j ] ==
+ Spec.MLKEM.sample_poly_cbd v_ETA2 prf_outputs.[ sz j ])
error_1_
(fun error_1_ i ->
let error_1_:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K =
error_1_
in
let i:usize = i in
- Rust_primitives.Hax.Monomorphized_update_at.update_at_usize error_1_
- i
- (Libcrux_ml_kem.Sampling.sample_from_binomial_distribution v_ETA2
- #v_Vector
- (prf_outputs.[ i ] <: t_Slice u8)
- <:
- Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
- <:
- t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K)
- in
- let result:(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8) =
- error_1_, domain_separator
- <:
- (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
+ let error_1_:t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K =
+ Rust_primitives.Hax.Monomorphized_update_at.update_at_usize error_1_
+ i
+ (Libcrux_ml_kem.Sampling.sample_from_binomial_distribution v_ETA2
+ #v_Vector
+ (prf_outputs.[ i ] <: t_Slice u8)
+ <:
+ Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
+ in
+ error_1_)
in
- let _:Prims.unit = admit () (* Panic freedom *) in
- result
+ let _:Prims.unit =
+ Lib.Sequence.eq_intro #(Spec.MLKEM.polynomial)
+ #(v v_K)
+ (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector error_1_)
+ (Spec.MLKEM.sample_vector_cbd2 #v_K
+ (Seq.slice prf_input 0 32)
+ (sz (v v__domain_separator_init)))
+ in
+ error_1_, domain_separator
+ <:
+ (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
-#push-options "--admit_smt_queries true"
+#pop-options
let sample_vector_cbd_then_ntt
(v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
@@ -124,7 +165,9 @@ let sample_vector_cbd_then_ntt
(fun temp_0_ i ->
let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in
let i:usize = i in
- v domain_separator == v v__domain_separator_init + v i)
+ v domain_separator == v v__domain_separator_init + v i /\
+ (forall (j: nat). j < v i ==> v (Seq.index prf_input j) == v v__domain_separator_init + j)
+ )
(domain_separator, prf_inputs <: (u8 & t_Array (t_Array u8 (sz 33)) v_K))
(fun temp_0_ i ->
let domain_separator, prf_inputs:(u8 & t_Array (t_Array u8 (sz 33)) v_K) = temp_0_ in
@@ -185,13 +228,13 @@ let sample_vector_cbd_then_ntt
in
re_as_ntt)
in
- let hax_temp_output:u8 = domain_separator in
+ let result:u8 = domain_separator in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ let hax_temp_output:u8 = result in
re_as_ntt, hax_temp_output
<:
(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
-#pop-options
-
let sample_vector_cbd_then_ntt_out
(v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize)
(#v_Vector #v_Hasher: Type0)
@@ -577,7 +620,11 @@ let decrypt_unpacked
secret_key.Libcrux_ml_kem.Ind_cpa.Unpacked.f_secret_as_ntt
u_as_ntt
in
- Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message
+ let result:t_Array u8 (sz 32) =
+ Libcrux_ml_kem.Serialize.compress_then_serialize_message #v_Vector message
+ in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ result
let decrypt
(v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
@@ -717,7 +764,9 @@ let encrypt_unpacked
<:
t_Slice u8)
in
- ciphertext
+ let result:t_Array u8 v_CIPHERTEXT_SIZE = ciphertext in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ result
#pop-options
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
index 34b5b8ad..65384862 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti
@@ -23,8 +23,17 @@ val sample_ring_element_cbd
: Prims.Pure (t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K & u8)
(requires
Spec.MLKEM.is_rank v_K /\ v_ETA2_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA2_RANDOMNESS_SIZE v_K /\
- v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ range (v domain_separator + v v_K) u8_inttype)
- (fun _ -> Prims.l_True)
+ v_ETA2 == Spec.MLKEM.v_ETA2 v_K /\ v domain_separator < 2 * v v_K /\
+ range (v domain_separator + v v_K) u8_inttype)
+ (ensures
+ fun temp_0_ ->
+ let err1, ds:(t_Array (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector) v_K &
+ u8) =
+ temp_0_
+ in
+ v ds == v domain_separator + v v_K /\
+ Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector err1 ==
+ Spec.MLKEM.sample_vector_cbd2 #v_K (Seq.slice prf_input 0 32) (sz (v domain_separator)))
/// Sample a vector of ring elements from a centered binomial distribution and
/// convert them into their NTT representations.
@@ -233,7 +242,13 @@ val decrypt_unpacked
v_U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR v_K /\
v_V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR v_K /\
v_VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE v_K)
- (fun _ -> Prims.l_True)
+ (ensures
+ fun result ->
+ let result:t_Array u8 (sz 32) = result in
+ result ==
+ Spec.MLKEM.ind_cpa_decrypt_unpacked v_K
+ ciphertext
+ (Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector secret_key.f_secret_as_ntt))
val decrypt
(v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR:
@@ -310,7 +325,15 @@ val encrypt_unpacked
v_BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE v_K /\
v_CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE v_K /\
length randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE)
- (fun _ -> Prims.l_True)
+ (ensures
+ fun result ->
+ let result:t_Array u8 v_CIPHERTEXT_SIZE = result in
+ result ==
+ 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))
val encrypt
(v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE:
@@ -396,6 +419,14 @@ val generate_keypair_unpacked
Libcrux_ml_kem.Ind_cpa.Unpacked.t_IndCpaPublicKeyUnpacked v_K v_Vector) =
temp_0_
in
+ let ((t_as_ntt, seed_for_A), 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.f_t_as_ntt) ==
+ t_as_ntt) /\ (public_key.f_seed_for_A == seed_for_A) /\
+ ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #v_K #v_Vector private_key.f_secret_as_ntt) ==
+ secret_as_ntt)) /\
(forall (i: nat).
i < v v_K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index private_key_future
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fsti
index d8352118..8c7edaca 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Invert_ntt.fsti
@@ -17,12 +17,12 @@ val inv_ntt_layer_int_vec_step_reduce
: Prims.Pure (v_Vector & v_Vector)
(requires
Spec.Utils.is_i16b 1664 zeta_r /\
- (forall i.
+ (forall (i: nat).
i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array b) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i))) /\
- (forall i.
+ (forall (i: nat).
i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) +
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti
index 487f928c..750573e7 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti
@@ -18,12 +18,12 @@ val ntt_layer_int_vec_step
(requires
Spec.Utils.is_i16b 1664 zeta_r /\
(let t = Libcrux_ml_kem.Vector.Traits.montgomery_multiply_fe b zeta_r in
- (forall i.
+ (forall (i: nat).
i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\
- (forall i.
+ (forall (i: nat).
i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) +
@@ -131,15 +131,15 @@ val ntt_at_layer_4_plus
let ntt_layer_7_pre (#v_Vector: Type0)
{| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
(re_0 re_1: v_Vector) =
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_1) i) * v (-1600s))) /\
(let t = Libcrux_ml_kem.Vector.Traits.f_multiply_by_constant re_1 (-1600s) in
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) +
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))
@@ -150,7 +150,7 @@ val ntt_at_layer_7_
(re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
: Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
(requires
- forall i.
+ forall (i: nat).
i < 8 ==>
ntt_layer_7_pre (re.f_coefficients.[ sz i ]) (re.f_coefficients.[ sz i +! sz 8 ]))
(fun _ -> Prims.l_True)
@@ -161,7 +161,7 @@ val ntt_binomially_sampled_ring_element
(re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
: Prims.Pure (Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
(requires
- forall i.
+ forall (i: nat).
i < 8 ==>
ntt_layer_7_pre (re.f_coefficients.[ sz i ]) (re.f_coefficients.[ sz i +! sz 8 ]))
(fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fst
index 0ed1d6eb..de03f397 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fst
@@ -316,14 +316,18 @@ let sample_from_binomial_distribution
(randomness: t_Slice u8)
=
let _:Prims.unit = assert ((v (cast v_ETA <: u32) == 2) \/ (v (cast v_ETA <: u32) == 3)) in
- match cast (v_ETA <: usize) <: u32 with
- | 2ul -> sample_from_binomial_distribution_2_ #v_Vector randomness
- | 3ul -> sample_from_binomial_distribution_3_ #v_Vector randomness
- | _ ->
- Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code"
+ let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector =
+ match cast (v_ETA <: usize) <: u32 with
+ | 2ul -> sample_from_binomial_distribution_2_ #v_Vector randomness
+ | 3ul -> sample_from_binomial_distribution_3_ #v_Vector randomness
+ | _ ->
+ Rust_primitives.Hax.never_to_any (Core.Panicking.panic "internal error: entered unreachable code"
- <:
- Rust_primitives.Hax.t_Never)
+ <:
+ Rust_primitives.Hax.t_Never)
+ in
+ let _:Prims.unit = admit () (* Panic freedom *) in
+ result
#push-options "--admit_smt_queries true"
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti
index 8d7df649..2c2418aa 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti
@@ -117,7 +117,15 @@ val sample_from_binomial_distribution
(requires
(v_ETA =. sz 2 || v_ETA =. sz 3) &&
(Core.Slice.impl__len #u8 randomness <: usize) =. (v_ETA *! sz 64 <: usize))
- (fun _ -> Prims.l_True)
+ (ensures
+ fun result ->
+ let result:Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector = result in
+ (forall (i: nat).
+ i < 8 ==>
+ Libcrux_ml_kem.Ntt.ntt_layer_7_pre (result.f_coefficients.[ sz i ])
+ (result.f_coefficients.[ sz i +! sz 8 ])) /\
+ Libcrux_ml_kem.Polynomial.to_spec_poly_t #v_Vector result ==
+ Spec.MLKEM.sample_poly_cbd v_ETA randomness)
val sample_from_xof
(v_K: usize)
diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst
index 07c9216a..83119822 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst
+++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.MLKEM.fst
@@ -168,8 +168,19 @@ let sample_poly_cbd1 #r seed domain_sep =
let sample_vector_cbd1 (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) : vector r =
createi r (fun i -> sample_poly_cbd1 #r seed (domain_sep +! i))
+// let sample_vector_cbd2 (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) : vector r =
+// createi r (fun i -> sample_poly_cbd2 #r seed (domain_sep +! i))
+
+let sample_vector_cbd2_prf_input (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) (i:usize{i <. r}) : t_Array u8 (sz 33) =
+ Seq.append seed (Seq.create 1 (mk_int #u8_inttype (v domain_sep + v i)))
+
+let sample_vector_cbd2_prf_output (#r:rank) (prf_output:t_Array (t_Array u8 (v_ETA2_RANDOMNESS_SIZE r)) r) (i:usize{i <. r}) : polynomial =
+ sample_poly_cbd (v_ETA2 r) prf_output.[i]
+
let sample_vector_cbd2 (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) : vector r =
- createi r (fun i -> sample_poly_cbd2 #r seed (domain_sep +! i))
+ let prf_input = createi r (sample_vector_cbd2_prf_input #r seed domain_sep) in
+ let prf_output = v_PRFxN r (v_ETA2_RANDOMNESS_SIZE r) prf_input in
+ createi r (sample_vector_cbd2_prf_output #r prf_output)
let sample_vector_cbd_then_ntt (#r:rank) (seed:t_Array u8 (sz 32)) (domain_sep:usize{v domain_sep < 2 * v r}) : vector r =
vector_ntt (sample_vector_cbd1 #r seed domain_sep)
@@ -213,6 +224,17 @@ let decode_then_decompress_v (#r:rank): t_Array u8 (v_C2_SIZE r) -> polynomial
(** IND-CPA Functions *)
+val ind_cpa_generate_keypair_unpacked (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) :
+ ((((vector r) & (t_Array u8 (sz 32))) & (vector r)) & bool)
+let ind_cpa_generate_keypair_unpacked r randomness =
+ let hashed = v_G randomness in
+ let (seed_for_A, seed_for_secret_and_error) = split hashed (sz 32) in
+ let (matrix_A_as_ntt, sufficient_randomness) = sample_matrix_A_ntt #r seed_for_A in
+ let secret_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error (sz 0) in
+ let error_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error r in
+ let t_as_ntt = compute_As_plus_e_ntt #r matrix_A_as_ntt secret_as_ntt error_as_ntt in
+ (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness)
+
/// This function implements most of Algorithm 12 of the
/// NIST FIPS 203 specification; this is the MLKEM CPA-PKE key generation algorithm.
///
@@ -223,16 +245,30 @@ let decode_then_decompress_v (#r:rank): t_Array u8 (v_C2_SIZE r) -> polynomial
val ind_cpa_generate_keypair (r:rank) (randomness:t_Array u8 v_CPA_KEY_GENERATION_SEED_SIZE) :
(t_MLKEMCPAKeyPair r & bool)
let ind_cpa_generate_keypair r randomness =
- let hashed = v_G randomness in
- let (seed_for_A, seed_for_secret_and_error) = split hashed (sz 32) in
- let (matrix_A_as_ntt, sufficient_randomness) = sample_matrix_A_ntt #r seed_for_A in
- let secret_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error (sz 0) in
- let error_as_ntt = sample_vector_cbd_then_ntt #r seed_for_secret_and_error r in
- let t_as_ntt = compute_As_plus_e_ntt #r matrix_A_as_ntt secret_as_ntt error_as_ntt in
+ let (((t_as_ntt,seed_for_A), secret_as_ntt), sufficient_randomness) =
+ ind_cpa_generate_keypair_unpacked r randomness in
let public_key_serialized = Seq.append (vector_encode_12 #r t_as_ntt) seed_for_A in
let secret_key_serialized = vector_encode_12 #r secret_as_ntt in
((secret_key_serialized,public_key_serialized), sufficient_randomness)
+val ind_cpa_encrypt_unpacked (r:rank)
+ (message: t_Array u8 v_SHARED_SECRET_SIZE)
+ (randomness:t_Array u8 v_SHARED_SECRET_SIZE)
+ (t_as_ntt:vector r)
+ (matrix_A_as_ntt:matrix r) :
+ t_MLKEMCiphertext r
+
+let ind_cpa_encrypt_unpacked r message randomness t_as_ntt matrix_A_as_ntt =
+ let r_as_ntt = sample_vector_cbd_then_ntt #r randomness (sz 0) in
+ let error_1 = sample_vector_cbd2 #r randomness r in
+ let error_2 = sample_poly_cbd2 #r randomness (r +! r) in
+ let u = vector_add (vector_inv_ntt (matrix_vector_mul_ntt (matrix_transpose matrix_A_as_ntt) r_as_ntt)) error_1 in
+ let mu = decode_then_decompress_message message in
+ let v = poly_add (poly_add (vector_dot_product_ntt t_as_ntt r_as_ntt) error_2) mu in
+ let c1 = compress_then_encode_u #r u in
+ let c2 = compress_then_encode_v #r v in
+ concat c1 c2
+
/// This function implements Algorithm 13 of the
/// NIST FIPS 203 specification; this is the MLKEM CPA-PKE encryption algorithm.
@@ -246,15 +282,19 @@ let ind_cpa_encrypt r public_key message randomness =
let (t_as_ntt_bytes, seed_for_A) = split public_key (v_T_AS_NTT_ENCODED_SIZE r) in
let t_as_ntt = vector_decode_12 #r t_as_ntt_bytes in
let matrix_A_as_ntt, sufficient_randomness = sample_matrix_A_ntt #r seed_for_A in
- let r_as_ntt = sample_vector_cbd_then_ntt #r randomness (sz 0) in
- let error_1 = sample_vector_cbd2 #r randomness r in
- let error_2 = sample_poly_cbd2 #r randomness (r +! r) in
- let u = vector_add (vector_inv_ntt (matrix_vector_mul_ntt (matrix_transpose matrix_A_as_ntt) r_as_ntt)) error_1 in
- let mu = decode_then_decompress_message message in
- let v = poly_add (poly_add (vector_dot_product_ntt t_as_ntt r_as_ntt) error_2) mu in
- let c1 = compress_then_encode_u #r u in
- let c2 = compress_then_encode_v #r v in
- (concat c1 c2, sufficient_randomness)
+ let c = ind_cpa_encrypt_unpacked r message randomness t_as_ntt matrix_A_as_ntt in
+ (c, sufficient_randomness)
+
+val ind_cpa_decrypt_unpacked (r:rank)
+ (ciphertext: t_MLKEMCiphertext r) (secret_as_ntt:vector r):
+ t_MLKEMSharedSecret
+
+let ind_cpa_decrypt_unpacked r ciphertext secret_as_ntt =
+ let (c1,c2) = split ciphertext (v_C1_SIZE r) in
+ let u = decode_then_decompress_u #r c1 in
+ let v = decode_then_decompress_v #r c2 in
+ let w = poly_sub v (poly_inv_ntt (vector_dot_product_ntt secret_as_ntt (vector_ntt u))) in
+ compress_then_encode_message w
/// This function implements Algorithm 14 of the
/// NIST FIPS 203 specification; this is the MLKEM CPA-PKE decryption algorithm.
@@ -265,12 +305,8 @@ val ind_cpa_decrypt (r:rank) (secret_key: t_MLKEMCPAPrivateKey r)
[@ "opaque_to_smt"]
let ind_cpa_decrypt r secret_key ciphertext =
- let (c1,c2) = split ciphertext (v_C1_SIZE r) in
- let u = decode_then_decompress_u #r c1 in
- let v = decode_then_decompress_v #r c2 in
let secret_as_ntt = vector_decode_12 #r secret_key in
- let w = poly_sub v (poly_inv_ntt (vector_dot_product_ntt secret_as_ntt (vector_ntt u))) in
- compress_then_encode_message w
+ ind_cpa_decrypt_unpacked r ciphertext secret_as_ntt
(** IND-CCA Functions *)
diff --git a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
index 1c6ed14b..5c77472f 100644
--- a/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
+++ b/libcrux-ml-kem/proofs/fstar/spec/Spec.Utils.fst
@@ -126,6 +126,9 @@ val v_PRF (v_LEN: usize{v v_LEN < pow2 32}) (input: t_Slice u8) : t_Array u8 v_L
let v_PRF v_LEN input = map_slice Lib.RawIntTypes.u8_to_UInt8 (
shake256 (Seq.length input) (map_slice Lib.IntTypes.secret input) (v v_LEN))
+assume val v_PRFxN (r:usize{v r == 2 \/ v r == 3 \/ v r == 4}) (v_LEN: usize{v v_LEN < pow2 32})
+ (input: t_Array (t_Array u8 (sz 33)) r) : t_Array (t_Array u8 v_LEN) r
+
let v_J (input: t_Slice u8) : t_Array u8 (sz 32) = v_PRF (sz 32) input
val v_XOF (v_LEN: usize{v v_LEN < pow2 32}) (input: t_Slice u8) : t_Array u8 v_LEN
diff --git a/libcrux-ml-kem/src/hash_functions.rs b/libcrux-ml-kem/src/hash_functions.rs
index 6627b3d7..aa91579d 100644
--- a/libcrux-ml-kem/src/hash_functions.rs
+++ b/libcrux-ml-kem/src/hash_functions.rs
@@ -48,7 +48,12 @@ pub(crate) trait Hash {
fn PRF(input: &[u8]) -> [u8; LEN];
/// PRFxN aka N SHAKE256
- #[requires(true)]
+ #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ #[ensures(|result|
+ // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784
+ fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==>
+ $result == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K];
/// Create a SHAKE128 state and absorb the input.
@@ -113,6 +118,10 @@ pub(crate) mod portable {
digest
}
+ #[hax_lib::requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ #[hax_lib::ensures(|result|
+ fstar!("$result == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
debug_assert!(K == 2 || K == 3 || K == 4);
@@ -190,6 +199,12 @@ pub(crate) mod portable {
PRF::(input)
}
+ #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ // Output name has be `out` https://github.com/hacspec/hax/issues/832
+ #[ensures(|out|
+ fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==>
+ $out == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
PRFxN::(input)
@@ -261,6 +276,10 @@ pub(crate) mod avx2 {
digest
}
+ #[hax_lib::requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ #[hax_lib::ensures(|result|
+ fstar!("$result == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
debug_assert!(K == 2 || K == 3 || K == 4);
@@ -437,6 +456,12 @@ pub(crate) mod avx2 {
PRF::(input)
}
+ #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ // Output name has be `out` https://github.com/hacspec/hax/issues/832
+ #[ensures(|out|
+ fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==>
+ $out == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
PRFxN::(input)
@@ -506,6 +531,10 @@ pub(crate) mod neon {
digest
}
+ #[hax_lib::requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ #[hax_lib::ensures(|result|
+ fstar!("$result == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
debug_assert!(K == 2 || K == 3 || K == 4);
@@ -712,6 +741,13 @@ pub(crate) mod neon {
PRF::(input)
}
+ #[requires(fstar!("v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)"))]
+ // Output name has be `out` https://github.com/hacspec/hax/issues/832
+ #[ensures(|out|
+ // We need to repeat the pre-condition here because of https://github.com/hacspec/hax/issues/784
+ fstar!("(v $LEN < pow2 32 /\\ (v $K == 2 \\/ v $K == 3 \\/ v $K == 4)) ==>
+ $out == Spec.Utils.v_PRFxN $K $LEN $input"))
+ ]
#[inline(always)]
fn PRFxN(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
PRFxN::(input)
diff --git a/libcrux-ml-kem/src/ind_cpa.rs b/libcrux-ml-kem/src/ind_cpa.rs
index 81aa3e1e..5b8d7d6a 100644
--- a/libcrux-ml-kem/src/ind_cpa.rs
+++ b/libcrux-ml-kem/src/ind_cpa.rs
@@ -154,11 +154,17 @@ pub(crate) fn serialize_secret_key::ZERO());
let mut prf_inputs = [prf_input; K];
let _domain_separator_init = domain_separator;
+ let _prf_inputs_init = prf_inputs;
for i in 0..K {
- hax_lib::loop_invariant!(|i: usize| { fstar!("v $domain_separator == v $_domain_separator_init + v $i") });
+ hax_lib::loop_invariant!(|i: usize| { fstar!("v $domain_separator == v $_domain_separator_init + v $i /\\
+ (v $i < v $K ==> (forall (j:nat). (j >= v $i /\\ j < v $K) ==>
+ ${prf_inputs}.[ sz j ] == ${_prf_inputs_init}.[ sz j ])) /\\
+ (forall (j:nat). j < v $i ==> v (Seq.index (Seq.index $prf_inputs j) 32) == v $_domain_separator_init + j /\\
+ Seq.slice (Seq.index $prf_inputs j) 0 32 == Seq.slice (Seq.index $_prf_inputs_init j) 0 32)") });
prf_inputs[i][32] = domain_separator;
domain_separator += 1;
}
+ hax_lib::fstar!("let lemma_aux (i:nat{ i < v $K }) : Lemma (${prf_inputs}.[sz i] == (Seq.append (Seq.slice $prf_input 0 32)
+ (Seq.create 1 (mk_int #u8_inttype (v ($_domain_separator_init +! (mk_int #u8_inttype i))))))) =
+ Lib.Sequence.eq_intro #u8 #33 ${prf_inputs}.[sz i] (Seq.append (Seq.slice $prf_input 0 32)
+ (Seq.create 1 (mk_int #u8_inttype (v $_domain_separator_init + i)))) in
+
+ Classical.forall_intro lemma_aux;
+ Lib.Sequence.eq_intro #(t_Array u8 (sz 33)) #(v $K) $prf_inputs
+ (createi $K (Spec.MLKEM.sample_vector_cbd2_prf_input #$K (Seq.slice $prf_input 0 32) (sz (v $_domain_separator_init))))");
let prf_outputs: [[u8; ETA2_RANDOMNESS_SIZE]; K] = Hasher::PRFxN(&prf_inputs);
for i in 0..K {
+ hax_lib::loop_invariant!(|i: usize| { fstar!("forall (j:nat). j < v $i ==>
+ Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector ${error_1}.[ sz j ] ==
+ Spec.MLKEM.sample_poly_cbd $ETA2 ${prf_outputs}.[ sz j ]") });
error_1[i] = sample_from_binomial_distribution::(&prf_outputs[i]);
}
+ hax_lib::fstar!("Lib.Sequence.eq_intro #(Spec.MLKEM.polynomial) #(v $K)
+ (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector $error_1)
+ (Spec.MLKEM.sample_vector_cbd2 #$K (Seq.slice $prf_input 0 32) (sz (v $_domain_separator_init)))");
(error_1, domain_separator)
}
/// Sample a vector of ring elements from a centered binomial distribution and
/// convert them into their NTT representations.
#[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$ETA_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
$ETA == Spec.MLKEM.v_ETA1 $K /\\
@@ -212,7 +237,8 @@ fn sample_vector_cbd_then_ntt<
let mut prf_inputs = [prf_input; K];
let _domain_separator_init = domain_separator;
for i in 0..K {
- hax_lib::loop_invariant!(|i: usize| { fstar!("v $domain_separator == v $_domain_separator_init + v $i") });
+ hax_lib::loop_invariant!(|i: usize| { fstar!("v $domain_separator == v $_domain_separator_init + v $i /\\
+ (forall (j:nat). j < v i ==> v (Seq.index prf_input j) == v v__domain_separator_init + j)") });
prf_inputs[i][32] = domain_separator;
domain_separator += 1;
}
@@ -299,7 +325,10 @@ fn sample_vector_cbd_then_ntt_out<
$ETA1_RANDOMNESS_SIZE == Spec.MLKEM.v_ETA1_RANDOMNESS_SIZE $K /\\
$ETA1 == Spec.MLKEM.v_ETA1 $K /\\
length $key_generation_seed == Spec.MLKEM.v_CPA_KEY_GENERATION_SEED_SIZE"))]
-#[hax_lib::ensures(|_| fstar!("
+#[hax_lib::ensures(|_| fstar!("let (((t_as_ntt,seed_for_A), secret_as_ntt), valid) = Spec.MLKEM.ind_cpa_generate_keypair_unpacked $K $key_generation_seed in
+ (valid ==> ((Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$: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_vector_t #$K #$:Vector ${private_key}.f_secret_as_ntt) == secret_as_ntt)) /\\
(forall (i:nat). i < v $K ==>
Libcrux_ml_kem.Serialize.coefficients_field_modulus_range (Seq.index ${private_key}_future.f_secret_as_ntt i)) /\\
(forall (i:nat). i < v $K ==>
@@ -476,6 +505,7 @@ fn compress_then_serialize_u<
/// The NIST FIPS 203 standard can be found at
/// .
#[allow(non_snake_case)]
+#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::fstar::options("--z3rlimit 200")]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$ETA1 == Spec.MLKEM.v_ETA1 $K /\\
@@ -489,6 +519,11 @@ fn compress_then_serialize_u<
$BLOCK_LEN == Spec.MLKEM.v_C1_BLOCK_SIZE $K /\\
$CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
length $randomness == Spec.MLKEM.v_SHARED_SECRET_SIZE"))]
+#[hax_lib::ensures(|result|
+ fstar!("$result == Spec.MLKEM.ind_cpa_encrypt_unpacked $K $message $randomness
+ (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${public_key}.f_t_as_ntt)
+ (Libcrux_ml_kem.Polynomial.to_spec_matrix_t #$K #$:Vector ${public_key}.f_A)")
+)]
pub(crate) fn encrypt_unpacked<
const K: usize,
const CIPHERTEXT_SIZE: usize,
@@ -721,11 +756,16 @@ fn deserialize_secret_key(
/// The NIST FIPS 203 standard can be found at
/// .
#[allow(non_snake_case)]
+#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::requires(fstar!("Spec.MLKEM.is_rank $K /\\
$CIPHERTEXT_SIZE == Spec.MLKEM.v_CPA_CIPHERTEXT_SIZE $K /\\
$U_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_U_COMPRESSION_FACTOR $K /\\
$V_COMPRESSION_FACTOR == Spec.MLKEM.v_VECTOR_V_COMPRESSION_FACTOR $K /\\
$VECTOR_U_ENCODED_SIZE == Spec.MLKEM.v_C1_SIZE $K"))]
+#[hax_lib::ensures(|result|
+ fstar!("$result == Spec.MLKEM.ind_cpa_decrypt_unpacked $K $ciphertext
+ (Libcrux_ml_kem.Polynomial.to_spec_vector_t #$K #$:Vector ${secret_key}.f_secret_as_ntt)")
+)]
pub(crate) fn decrypt_unpacked<
const K: usize,
const CIPHERTEXT_SIZE: usize,
diff --git a/libcrux-ml-kem/src/invert_ntt.rs b/libcrux-ml-kem/src/invert_ntt.rs
index 49fa7fea..530f0a84 100644
--- a/libcrux-ml-kem/src/invert_ntt.rs
+++ b/libcrux-ml-kem/src/invert_ntt.rs
@@ -137,11 +137,11 @@ pub(crate) fn invert_ntt_at_layer_3(
#[inline(always)]
#[hax_lib::requires(fstar!("Spec.Utils.is_i16b 1664 $zeta_r /\\
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $b) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i))) /\\
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i) +
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $b) i))) /\\
diff --git a/libcrux-ml-kem/src/ntt.rs b/libcrux-ml-kem/src/ntt.rs
index b3aa4087..604a9847 100644
--- a/libcrux-ml-kem/src/ntt.rs
+++ b/libcrux-ml-kem/src/ntt.rs
@@ -155,11 +155,11 @@ pub(crate) fn ntt_at_layer_3(
#[inline(always)]
#[hax_lib::requires(fstar!("Spec.Utils.is_i16b 1664 $zeta_r /\\
(let t = ${montgomery_multiply_fe::} $b $zeta_r in
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\\
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i) +
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))"))]
@@ -224,19 +224,19 @@ pub(crate) fn ntt_at_layer_4_plus(
let ntt_layer_7_pre (#v_Vector: Type0)
{| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
(re_0 re_1: v_Vector) =
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_1) i) * v (-1600s))) /\\
(let t = Libcrux_ml_kem.Vector.Traits.f_multiply_by_constant re_1 (-1600s) in
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) -
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))) /\\
- (forall i. i < 16 ==>
+ (forall (i:nat). i < 16 ==>
Spec.Utils.is_intb (pow2 15 - 1)
(v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re_0) i) +
v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array t) i))))")]
-#[hax_lib::requires(fstar!("forall i. i < 8 ==> ntt_layer_7_pre (${re}.f_coefficients.[ sz i ])
+#[hax_lib::requires(fstar!("forall (i:nat). i < 8 ==> ntt_layer_7_pre (${re}.f_coefficients.[ sz i ])
(${re}.f_coefficients.[ sz i +! sz 8 ])"))]
pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement) {
let step = VECTORS_IN_RING_ELEMENT / 2;
@@ -257,7 +257,7 @@ pub(crate) fn ntt_at_layer_7(re: &mut PolynomialRingElement<
#[inline(always)]
#[hax_lib::fstar::options("--z3rlimit 200")]
-#[hax_lib::requires(fstar!("forall i. i < 8 ==> ntt_layer_7_pre (${re}.f_coefficients.[ sz i ])
+#[hax_lib::requires(fstar!("forall (i:nat). i < 8 ==> ntt_layer_7_pre (${re}.f_coefficients.[ sz i ])
(${re}.f_coefficients.[ sz i +! sz 8 ])"))]
pub(crate) fn ntt_binomially_sampled_ring_element(
re: &mut PolynomialRingElement,
diff --git a/libcrux-ml-kem/src/sampling.rs b/libcrux-ml-kem/src/sampling.rs
index 094334c5..1a140d1a 100644
--- a/libcrux-ml-kem/src/sampling.rs
+++ b/libcrux-ml-kem/src/sampling.rs
@@ -252,7 +252,12 @@ fn sample_from_binomial_distribution_3(
}
#[inline(always)]
+#[hax_lib::fstar::verification_status(panic_free)]
#[hax_lib::requires((ETA == 2 || ETA == 3) && randomness.len() == ETA * 64)]
+#[hax_lib::ensures(|result| fstar!("(forall (i:nat). i < 8 ==> Libcrux_ml_kem.Ntt.ntt_layer_7_pre
+ (${result}.f_coefficients.[ sz i ]) (${result}.f_coefficients.[ sz i +! sz 8 ])) /\\
+ Libcrux_ml_kem.Polynomial.to_spec_poly_t #$:Vector $result ==
+ Spec.MLKEM.sample_poly_cbd $ETA $randomness"))]
pub(super) fn sample_from_binomial_distribution(
randomness: &[u8],
) -> PolynomialRingElement {