From 61129bcdbdff56970ffef3031e928a3cc1833b7c Mon Sep 17 00:00:00 2001 From: mamonet Date: Fri, 20 Dec 2024 06:57:36 +0000 Subject: [PATCH] Make polynomial.rs panic-free --- .../extraction/Libcrux_ml_kem.Polynomial.fst | 239 +++++++++++----- .../extraction/Libcrux_ml_kem.Polynomial.fsti | 186 ++++++++++-- .../extraction/Libcrux_ml_kem.Vector.Avx2.fst | 20 +- .../Libcrux_ml_kem.Vector.Portable.fst | 19 +- .../Libcrux_ml_kem.Vector.Traits.fsti | 17 +- libcrux-ml-kem/src/polynomial.rs | 268 ++++++++++++++++-- libcrux-ml-kem/src/vector/avx2.rs | 12 +- libcrux-ml-kem/src/vector/portable.rs | 12 +- libcrux-ml-kem/src/vector/traits.rs | 10 +- 9 files changed, 648 insertions(+), 135 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst index 4cad63238..50ec8d159 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fst @@ -14,6 +14,30 @@ let zeta (i: usize) = let _:Prims.unit = admit () (* Panic freedom *) in result +[@@ "opaque_to_smt"] + +let add_vector + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + (lhs rhs: v_Vector) + = + let _:Prims.unit = reveal_opaque (`%add_vector_pre) (add_vector_pre #v_Vector) in + let _:Prims.unit = reveal_opaque (`%add_vector_post) (add_vector_post #v_Vector) in + Libcrux_ml_kem.Vector.Traits.f_add #v_Vector #FStar.Tactics.Typeclasses.solve lhs rhs + +let sub_vector + (#v_Vector: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] + i1: + Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) + (lhs rhs: v_Vector) + = + let _:Prims.unit = reveal_opaque (`%sub_vector_pre) (sub_vector_pre #v_Vector) in + let _:Prims.unit = reveal_opaque (`%sub_vector_post) (sub_vector_post #v_Vector) in + Libcrux_ml_kem.Vector.Traits.f_sub #v_Vector #FStar.Tactics.Typeclasses.solve lhs rhs + [@@ FStar.Tactics.Typeclasses.tcinstance] assume val impl': @@ -46,7 +70,39 @@ let impl_1 Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) = impl_1' #v_Vector #i1 #i2 -#push-options "--admit_smt_queries true" +#push-options "--max_fuel 3 --z3rlimit 200 --ext context_pruning --z3refresh" + +let add_error_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (error: t_Array v_Vector (sz 16)) + (coefficient_normal_form: v_Vector) : Lemma + (requires (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ])) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form)) + (ensures (forall (i:nat). i < 16 ==> add_vector_pre coefficient_normal_form error.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector coefficient_normal_form error.[ sz i ])))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%add_vector_pre) (add_vector_pre #v_Vector); + reveal_opaque (`%add_vector_post) (add_vector_post #v_Vector); + reveal_opaque (`%add_vector) (add_vector #v_Vector); + assert_norm (pow2 15 == 32768); + assert (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ])); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb 28296 + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ]) j)))); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ]) j)))) + +#pop-options let add_error_reduce (#v_Vector: Type0) @@ -72,6 +128,7 @@ let add_error_reduce (myself.f_coefficients.[ j ] <: v_Vector) 1441s in + let _:Prims.unit = add_error_reduce_helper error.f_coefficients coefficient_normal_form in let myself:t_PolynomialRingElement v_Vector = { myself with @@ -81,8 +138,7 @@ let add_error_reduce j (Libcrux_ml_kem.Vector.Traits.f_barrett_reduce #v_Vector #FStar.Tactics.Typeclasses.solve - (Libcrux_ml_kem.Vector.Traits.f_add #v_Vector - #FStar.Tactics.Typeclasses.solve + (add_vector #v_Vector coefficient_normal_form (error.f_coefficients.[ j ] <: v_Vector) <: @@ -98,8 +154,6 @@ let add_error_reduce let hax_temp_output:Prims.unit = () <: Prims.unit in myself -#pop-options - let impl_2__add_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -110,7 +164,21 @@ let impl_2__add_error_reduce let self:t_PolynomialRingElement v_Vector = add_error_reduce #v_Vector self error in self -#push-options "--admit_smt_queries true" +let add_message_error_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result coefficient_normal_form: v_Vector) : Lemma + (requires (Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form))) + (ensures (add_vector_pre coefficient_normal_form result /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector coefficient_normal_form result)))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%add_vector_pre) (add_vector_pre #v_Vector); + reveal_opaque (`%add_vector_post) (add_vector_post #v_Vector); + assert_norm (pow2 15 == 32768) let add_message_error_reduce (#v_Vector: Type0) @@ -137,17 +205,12 @@ let add_message_error_reduce 1441s in let tmp:v_Vector = - Libcrux_ml_kem.Vector.Traits.f_add #v_Vector - #FStar.Tactics.Typeclasses.solve + add_vector #v_Vector (myself.f_coefficients.[ i ] <: v_Vector) (message.f_coefficients.[ i ] <: v_Vector) in - let tmp:v_Vector = - Libcrux_ml_kem.Vector.Traits.f_add #v_Vector - #FStar.Tactics.Typeclasses.solve - coefficient_normal_form - tmp - in + let _:Prims.unit = add_message_error_reduce_helper tmp coefficient_normal_form in + let tmp:v_Vector = add_vector #v_Vector coefficient_normal_form tmp in let result:t_PolynomialRingElement v_Vector = { result with @@ -168,8 +231,6 @@ let add_message_error_reduce in result -#pop-options - let impl_2__add_message_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -178,8 +239,6 @@ let impl_2__add_message_error_reduce (self message result: t_PolynomialRingElement v_Vector) = add_message_error_reduce #v_Vector self message result -#push-options "--admit_smt_queries true" - let add_standard_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -202,6 +261,7 @@ let add_standard_error_reduce Libcrux_ml_kem.Vector.Traits.to_standard_domain #v_Vector (myself.f_coefficients.[ j ] <: v_Vector) in + let _:Prims.unit = add_error_reduce_helper error.f_coefficients coefficient_normal_form in let myself:t_PolynomialRingElement v_Vector = { myself with @@ -211,8 +271,7 @@ let add_standard_error_reduce j (Libcrux_ml_kem.Vector.Traits.f_barrett_reduce #v_Vector #FStar.Tactics.Typeclasses.solve - (Libcrux_ml_kem.Vector.Traits.f_add #v_Vector - #FStar.Tactics.Typeclasses.solve + (add_vector #v_Vector coefficient_normal_form (error.f_coefficients.[ j ] <: v_Vector) <: @@ -228,8 +287,6 @@ let add_standard_error_reduce let hax_temp_output:Prims.unit = () <: Prims.unit in myself -#pop-options - let impl_2__add_standard_error_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -240,8 +297,6 @@ let impl_2__add_standard_error_reduce let self:t_PolynomialRingElement v_Vector = add_standard_error_reduce #v_Vector self error in self -#push-options "--admit_smt_queries true" - let poly_barrett_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -252,36 +307,39 @@ let poly_barrett_reduce let myself:t_PolynomialRingElement v_Vector = Rust_primitives.Hax.Folds.fold_range (sz 0) v_VECTORS_IN_RING_ELEMENT - (fun myself temp_1_ -> + (fun myself i -> let myself:t_PolynomialRingElement v_Vector = myself in - let _:usize = temp_1_ in - true) + let i:usize = i in + v i < v v_VECTORS_IN_RING_ELEMENT ==> + (forall (j: nat). + (j >= v i /\ j < v v_VECTORS_IN_RING_ELEMENT) ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.f_coefficients.[ sz j ]))) myself (fun myself i -> let myself:t_PolynomialRingElement v_Vector = myself in let i:usize = i in - { - myself with - f_coefficients - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize myself.f_coefficients - i - (Libcrux_ml_kem.Vector.Traits.f_barrett_reduce #v_Vector - #FStar.Tactics.Typeclasses.solve - (myself.f_coefficients.[ i ] <: v_Vector) - <: - v_Vector) + let myself:t_PolynomialRingElement v_Vector = + { + myself with + f_coefficients + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize myself.f_coefficients + i + (Libcrux_ml_kem.Vector.Traits.f_barrett_reduce #v_Vector + #FStar.Tactics.Typeclasses.solve + (myself.f_coefficients.[ i ] <: v_Vector) + <: + v_Vector) + } <: - t_Array v_Vector (sz 16) - } - <: - t_PolynomialRingElement v_Vector) + t_PolynomialRingElement v_Vector + in + myself) in let hax_temp_output:Prims.unit = () <: Prims.unit in myself -#pop-options - let impl_2__poly_barrett_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -292,7 +350,38 @@ let impl_2__poly_barrett_reduce let self:t_PolynomialRingElement v_Vector = poly_barrett_reduce #v_Vector self in self -#push-options "--admit_smt_queries true" +#push-options "--z3rlimit 200 --ext context_pruning" + +let subtract_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (myself: t_Array v_Vector (sz 16)) + (coefficient_normal_form: v_Vector) : Lemma + (requires (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ])) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form)) + (ensures (forall (i:nat). i < 16 ==> sub_vector_pre myself.[ sz i ] coefficient_normal_form /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (sub_vector myself.[ sz i ] coefficient_normal_form)))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%sub_vector_pre) (sub_vector_pre #v_Vector); + reveal_opaque (`%sub_vector_post) (sub_vector_post #v_Vector); + assert_norm (pow2 15 == 32768); + assert (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ])); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb 28296 + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ]) j) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j)))); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ]) j) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j)))) + +#pop-options let subtract_reduce (#v_Vector: Type0) @@ -318,6 +407,7 @@ let subtract_reduce (b.f_coefficients.[ i ] <: v_Vector) 1441s in + let _:Prims.unit = subtract_reduce_helper myself.f_coefficients coefficient_normal_form in let b:t_PolynomialRingElement v_Vector = { b with @@ -327,8 +417,7 @@ let subtract_reduce i (Libcrux_ml_kem.Vector.Traits.f_barrett_reduce #v_Vector #FStar.Tactics.Typeclasses.solve - (Libcrux_ml_kem.Vector.Traits.f_sub #v_Vector - #FStar.Tactics.Typeclasses.solve + (sub_vector #v_Vector (myself.f_coefficients.[ i ] <: v_Vector) coefficient_normal_form <: @@ -343,8 +432,6 @@ let subtract_reduce in b -#pop-options - let impl_2__subtract_reduce (#v_Vector: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] @@ -446,7 +533,7 @@ let impl_2__from_i16_array (a: t_Slice i16) = from_i16_array #v_Vector a -#push-options "--admit_smt_queries true" +#push-options "--z3rlimit 200 --ext context_pruning" let ntt_multiply (#v_Vector: Type0) @@ -501,8 +588,6 @@ let impl_2__ntt_multiply (self rhs: t_PolynomialRingElement v_Vector) = ntt_multiply #v_Vector self rhs -#push-options "--admit_smt_queries true" - let add_to_ring_element (#v_Vector: Type0) (v_K: usize) @@ -511,40 +596,48 @@ let add_to_ring_element Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector) (myself rhs: t_PolynomialRingElement v_Vector) = + let v__myself:t_Array v_Vector (sz 16) = myself.f_coefficients in let myself:t_PolynomialRingElement v_Vector = Rust_primitives.Hax.Folds.fold_range (sz 0) (Core.Slice.impl__len #v_Vector (myself.f_coefficients <: t_Slice v_Vector) <: usize) - (fun myself temp_1_ -> + (fun myself i -> let myself:t_PolynomialRingElement v_Vector = myself in - let _:usize = temp_1_ in - true) + let i:usize = i in + (v i < v (Core.Slice.impl__len myself.f_coefficients) ==> + (forall (j: nat). + (j >= v i /\ j < v (Core.Slice.impl__len myself.f_coefficients)) ==> + myself.f_coefficients.[ sz j ] == v__myself.[ sz j ] /\ + add_vector_pre myself.f_coefficients.[ sz j ] rhs.f_coefficients.[ sz j ])) /\ + (forall (j: nat). + j < v i ==> + add_vector_post myself.f_coefficients.[ sz j ] + v__myself.[ sz j ] + rhs.f_coefficients.[ sz j ])) myself (fun myself i -> let myself:t_PolynomialRingElement v_Vector = myself in let i:usize = i in - { - myself with - f_coefficients - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize myself.f_coefficients - i - (Libcrux_ml_kem.Vector.Traits.f_add #v_Vector - #FStar.Tactics.Typeclasses.solve - (myself.f_coefficients.[ i ] <: v_Vector) - (rhs.f_coefficients.[ i ] <: v_Vector) - <: - v_Vector) + let myself:t_PolynomialRingElement v_Vector = + { + myself with + f_coefficients + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize myself.f_coefficients + i + (add_vector #v_Vector + (myself.f_coefficients.[ i ] <: v_Vector) + (rhs.f_coefficients.[ i ] <: v_Vector) + <: + v_Vector) + } <: - t_Array v_Vector (sz 16) - } - <: - t_PolynomialRingElement v_Vector) + t_PolynomialRingElement v_Vector + in + myself) in let hax_temp_output:Prims.unit = () <: Prims.unit in myself -#pop-options - let impl_2__add_to_ring_element (#v_Vector: Type0) (v_K: usize) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti index 7f60ace38..7e2c0bef6 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti @@ -58,6 +58,62 @@ let to_spec_matrix_t (#r:Spec.MLKEM.rank) (#v_Vector: Type0) (m:t_Array (t_Array (t_PolynomialRingElement v_Vector) r) r) : Spec.MLKEM.matrix r = createi r (fun i -> to_spec_vector_t #r #v_Vector (m.[i])) +[@@ "opaque_to_smt"] +let add_vector_pre (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) = + forall i. i < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i)) + +[@@ "opaque_to_smt"] +let add_vector_post (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result lhs rhs: v_Vector) = + forall i. i < 16 ==> + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) i) == + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i)) + +val add_vector + (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) + : Prims.Pure v_Vector + (requires add_vector_pre lhs rhs) + (ensures + fun result -> + let result:v_Vector = result in + add_vector_post result lhs rhs) + +[@@ "opaque_to_smt"] +let sub_vector_pre (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) = + forall i. i < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i)) + +[@@ "opaque_to_smt"] +let sub_vector_post (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result lhs rhs: v_Vector) = + forall i. i < 16 ==> + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) i) == + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i)) + +val sub_vector + (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) + : Prims.Pure v_Vector + (requires sub_vector_pre lhs rhs) + (ensures + fun result -> + let result:v_Vector = result in + sub_vector_post result lhs rhs) + let v_VECTORS_IN_RING_ELEMENT: usize = Libcrux_ml_kem.Constants.v_COEFFICIENTS_IN_RING_ELEMENT /! Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR @@ -80,61 +136,126 @@ val add_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself error: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__add_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self error: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val add_message_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself message result: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + (forall (i: nat). + i < 16 ==> + add_vector_pre myself.f_coefficients.[ sz i ] message.f_coefficients.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (add_vector myself.f_coefficients.[ sz i + ] + message.f_coefficients.[ sz i ])))) + (fun _ -> Prims.l_True) val impl_2__add_message_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self message result: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + (forall (i: nat). + i < 16 ==> + add_vector_pre self.f_coefficients.[ sz i ] message.f_coefficients.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array (add_vector self.f_coefficients.[ sz i ] + message.f_coefficients.[ sz i ])))) + (fun _ -> Prims.l_True) val add_standard_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself error: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__add_standard_error_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self error: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val poly_barrett_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v v_VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__poly_barrett_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v v_VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val subtract_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself b: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__subtract_reduce (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self b: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__ZERO: #v_Vector: Type0 -> @@ -168,7 +289,7 @@ val impl_2__from_i16_array /// Given two `KyberPolynomialRingElement`s in their NTT representations, /// compute their product. Given two polynomials in the NTT domain `f^` and `ĵ`, -/// the `iᵗʰ` coefficient of the product `k̂` is determined by the calculation: +/// the `iᵗʰ` coefficient of the product `k\u{302}` is determined by the calculation: /// ```plaintext /// ĥ[2·i] + ĥ[2·i + 1]X = (f^[2·i] + f^[2·i + 1]X)·(ĝ[2·i] + ĝ[2·i + 1]X) mod (X² - ζ^(2·BitRev₇(i) + 1)) /// ``` @@ -182,7 +303,7 @@ val impl_2__from_i16_array /// end for /// return ĥ /// ``` -/// We say "almost" because the coefficients of the ring element output by +/// We say \"almost\" because the coefficients of the ring element output by /// this function are in the Montgomery domain. /// The NIST FIPS 203 standard can be found at /// . @@ -190,13 +311,29 @@ val ntt_multiply (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself rhs: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v v_VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.f_coefficients.[ sz i ]) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) val impl_2__ntt_multiply (#v_Vector: Type0) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self rhs: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v v_VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ]) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs.f_coefficients.[ sz i ])) + (fun _ -> Prims.l_True) /// Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise /// sum of their constituent coefficients. @@ -205,7 +342,19 @@ val add_to_ring_element (v_K: usize) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (myself rhs: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v (Core.Slice.impl__len myself.f_coefficients) ==> + add_vector_pre myself.f_coefficients.[ sz i ] rhs.f_coefficients.[ sz i ]) + (ensures + fun myself_future -> + let myself_future:t_PolynomialRingElement v_Vector = myself_future in + forall (i: nat). + i < v (Core.Slice.impl__len myself.f_coefficients) ==> + add_vector_post myself_future.f_coefficients.[ sz i ] + myself.f_coefficients.[ sz i ] + rhs.f_coefficients.[ sz i ]) /// Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise /// sum of their constituent coefficients. @@ -214,4 +363,9 @@ val impl_2__add_to_ring_element (v_K: usize) {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} (self rhs: t_PolynomialRingElement v_Vector) - : Prims.Pure (t_PolynomialRingElement v_Vector) Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure (t_PolynomialRingElement v_Vector) + (requires + forall (i: nat). + i < v (Core.Slice.impl__len self.f_coefficients) ==> + add_vector_pre self.f_coefficients.[ sz i ] rhs.f_coefficients.[ sz i ]) + (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst index b0b8981ad..f03973365 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fst @@ -348,11 +348,14 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = f_cond_subtract_3329_ = (fun (vector: t_SIMD256Vector) -> cond_subtract_3329_ vector); f_barrett_reduce_pre = - (fun (vector: t_SIMD256Vector) -> Spec.Utils.is_i16b_array 28296 (impl.f_repr vector)); + (fun (vector: t_SIMD256Vector) -> Spec.Utils.is_i16b_array_opaque 28296 (impl.f_repr vector)); f_barrett_reduce_post = (fun (vector: t_SIMD256Vector) (out: t_SIMD256Vector) -> true); f_barrett_reduce = (fun (vector: t_SIMD256Vector) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in { f_elements = Libcrux_ml_kem.Vector.Avx2.Arithmetic.barrett_reduce vector.f_elements } <: t_SIMD256Vector); @@ -361,10 +364,14 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = (fun (vector: t_SIMD256Vector) (constant: i16) -> Spec.Utils.is_i16b 1664 constant); f_montgomery_multiply_by_constant_post = - (fun (vector: t_SIMD256Vector) (constant: i16) (out: t_SIMD256Vector) -> true); + (fun (vector: t_SIMD256Vector) (constant: i16) (out: t_SIMD256Vector) -> + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr out)); f_montgomery_multiply_by_constant = (fun (vector: t_SIMD256Vector) (constant: i16) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in { f_elements = @@ -526,8 +533,8 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = -> Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr lhs) /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr rhs)); + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr lhs) /\ + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr rhs)); f_ntt_multiply_post = (fun @@ -539,7 +546,7 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = (zeta3: i16) (out: t_SIMD256Vector) -> - Spec.Utils.is_i16b_array 3328 (impl.f_repr out)); + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr out)); f_ntt_multiply = (fun @@ -550,6 +557,9 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector = (zeta2: i16) (zeta3: i16) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in ntt_multiply lhs rhs zeta0 zeta1 zeta2 zeta3); f_serialize_1_pre = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst index 7c018d9cf..f0122de73 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst @@ -242,7 +242,7 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = f_barrett_reduce_pre = (fun (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> - Spec.Utils.is_i16b_array 28296 (impl.f_repr v)); + Spec.Utils.is_i16b_array_opaque 28296 (impl.f_repr v)); f_barrett_reduce_post = (fun @@ -253,6 +253,9 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = f_barrett_reduce = (fun (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in Libcrux_ml_kem.Vector.Portable.Arithmetic.barrett_reduce v); f_montgomery_multiply_by_constant_pre = @@ -265,10 +268,13 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = (r: i16) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> - true); + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr out)); f_montgomery_multiply_by_constant = (fun (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) (r: i16) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in Libcrux_ml_kem.Vector.Portable.Arithmetic.montgomery_multiply_by_constant v r); f_compress_1_pre = @@ -505,8 +511,8 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = -> Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr lhs) /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr rhs)); + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr lhs) /\ + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr rhs)); f_ntt_multiply_post = (fun @@ -518,7 +524,7 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = (zeta3: i16) (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> - Spec.Utils.is_i16b_array 3328 (impl.f_repr out)); + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr out)); f_ntt_multiply = (fun @@ -529,6 +535,9 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = (zeta2: i16) (zeta3: i16) -> + let _:Prims.unit = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque + in Libcrux_ml_kem.Vector.Portable.Ntt.ntt_multiply lhs rhs zeta0 zeta1 zeta2 zeta3); f_serialize_1_pre = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti index 21e6d6a50..d594f5cfb 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti @@ -126,13 +126,14 @@ class t_Operations (v_Self: Type0) = { (f_cond_subtract_3329_pre x0) (fun result -> f_cond_subtract_3329_post x0 result); f_barrett_reduce_pre:vector: v_Self - -> pred: Type0{Spec.Utils.is_i16b_array 28296 (f_repr vector) ==> pred}; + -> pred: Type0{Spec.Utils.is_i16b_array_opaque 28296 (f_repr vector) ==> pred}; f_barrett_reduce_post:v_Self -> v_Self -> Type0; f_barrett_reduce:x0: v_Self -> Prims.Pure v_Self (f_barrett_reduce_pre x0) (fun result -> f_barrett_reduce_post x0 result); f_montgomery_multiply_by_constant_pre:v: v_Self -> c: i16 -> pred: Type0{Spec.Utils.is_i16b 1664 c ==> pred}; - f_montgomery_multiply_by_constant_post:v_Self -> i16 -> v_Self -> Type0; + f_montgomery_multiply_by_constant_post:v: v_Self -> c: i16 -> result: v_Self + -> pred: Type0{pred ==> Spec.Utils.is_i16b_array_opaque 3328 (f_repr result)}; f_montgomery_multiply_by_constant:x0: v_Self -> x1: i16 -> Prims.Pure v_Self (f_montgomery_multiply_by_constant_pre x0 x1) @@ -275,7 +276,8 @@ class t_Operations (v_Self: Type0) = { Type0 { Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (f_repr lhs) /\ Spec.Utils.is_i16b_array 3328 (f_repr rhs) ==> + Spec.Utils.is_i16b_array_opaque 3328 (f_repr lhs) /\ + Spec.Utils.is_i16b_array_opaque 3328 (f_repr rhs) ==> pred }; f_ntt_multiply_post: lhs: v_Self -> @@ -285,7 +287,7 @@ class t_Operations (v_Self: Type0) = { zeta2: i16 -> zeta3: i16 -> out: v_Self - -> pred: Type0{pred ==> Spec.Utils.is_i16b_array 3328 (f_repr out)}; + -> pred: Type0{pred ==> Spec.Utils.is_i16b_array_opaque 3328 (f_repr out)}; f_ntt_multiply:x0: v_Self -> x1: v_Self -> x2: i16 -> x3: i16 -> x4: i16 -> x5: i16 -> Prims.Pure v_Self (f_ntt_multiply_pre x0 x1 x2 x3 x4 x5) @@ -426,7 +428,12 @@ val montgomery_multiply_fe (#v_T: Type0) {| i1: t_Operations v_T |} (v: v_T) (fe : Prims.Pure v_T (requires Spec.Utils.is_i16b 1664 fer) (fun _ -> Prims.l_True) val to_standard_domain (#v_T: Type0) {| i1: t_Operations v_T |} (v: v_T) - : Prims.Pure v_T Prims.l_True (fun _ -> Prims.l_True) + : Prims.Pure v_T + Prims.l_True + (ensures + fun result -> + let result:v_T = result in + Spec.Utils.is_i16b_array_opaque 3328 (i1._super_8706949974463268012.f_repr result)) val to_unsigned_representative (#v_T: Type0) {| i1: t_Operations v_T |} (a: v_T) : Prims.Pure v_T diff --git a/libcrux-ml-kem/src/polynomial.rs b/libcrux-ml-kem/src/polynomial.rs index 75cfd1e49..4c6fcc45b 100644 --- a/libcrux-ml-kem/src/polynomial.rs +++ b/libcrux-ml-kem/src/polynomial.rs @@ -15,6 +15,102 @@ pub(crate) const ZETAS_TIMES_MONTGOMERY_R: [i16; 128] = { ] }; +#[inline(always)] +#[hax_lib::fstar::before(interface, +r#"[@@ "opaque_to_smt"] +let add_vector_post (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result lhs rhs: v_Vector) = + forall i. i < 16 ==> + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) i) == + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i))"# +)] +#[hax_lib::fstar::before(interface, +r#"[@@ "opaque_to_smt"] +let add_vector_pre (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) = + forall i. i < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i))"# +)] +#[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)] +#[hax_lib::requires(fstar!(r#"add_vector_pre $lhs $rhs"#))] +#[hax_lib::ensures(|result| fstar!(r#"add_vector_post $result $lhs $rhs"#))] +fn add_vector( + lhs: Vector, + rhs: &Vector, +) -> Vector { + hax_lib::fstar!(r#"reveal_opaque (`%add_vector_pre) (add_vector_pre #$:Vector)"#); + hax_lib::fstar!(r#"reveal_opaque (`%add_vector_post) (add_vector_post #$:Vector)"#); + Vector::add(lhs, rhs) +} + +#[inline(always)] +#[hax_lib::fstar::before(interface, +r#"[@@ "opaque_to_smt"] +let sub_vector_post (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result lhs rhs: v_Vector) = + forall i. i < 16 ==> + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) i) == + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i))"# +)] +#[hax_lib::fstar::before(interface, +r#"[@@ "opaque_to_smt"] +let sub_vector_pre (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (lhs rhs: v_Vector) = + forall i. i < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array lhs) i) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array rhs) i))"# +)] +#[hax_lib::requires(fstar!(r#"sub_vector_pre $lhs $rhs"#))] +#[hax_lib::ensures(|result| fstar!(r#"sub_vector_post $result $lhs $rhs"#))] +fn sub_vector( + lhs: Vector, + rhs: &Vector, +) -> Vector { + hax_lib::fstar!(r#"reveal_opaque (`%sub_vector_pre) (sub_vector_pre #$:Vector)"#); + hax_lib::fstar!(r#"reveal_opaque (`%sub_vector_post) (sub_vector_post #$:Vector)"#); + Vector::sub(lhs, rhs) +} + +// #[inline(always)] +// #[hax_lib::fstar::before(interface, +// r#"[@@ "opaque_to_smt"] +// let montgomery_multiply_by_constant_vector_post (#v_Vector: Type0) +// {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} +// (result: v_Vector) = +// Spec.Utils.is_i16b_array 3328 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result)"# +// )] +// #[hax_lib::ensures(|result| fstar!(r#"sub_vector_post $result"#))] +// fn montgomery_multiply_by_constant_vector( +// vec: Vector, +// c: i16, +// ) -> Vector { +// hax_lib::fstar!(r#"reveal_opaque (`%montgomery_multiply_by_constant_vector_post) +// (montgomery_multiply_by_constant_vector_post #$:Vector)"#); +// Vector::montgomery_multiply_by_constant(vec, c) +// } + +// #[hax_lib::fstar::before(interface, +// r#"[@@ "opaque_to_smt"] +// let barrett_reduce_vector_pre (#v_Vector: Type0) +// {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} +// (vec: v_Vector) = +// Spec.Utils.is_i16b_array 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array vec)"# +// )] +// #[hax_lib::requires(fstar!(r#"barrett_reduce_vector_pre $vec"#))] +// fn barrett_reduce_vector( +// vec: Vector, +// ) -> Vector { +// hax_lib::fstar!(r#"reveal_opaque (`%barrett_reduce_vector_pre) (barrett_reduce_vector_pre #$:Vector)"#); +// Vector::barrett_reduce(vec) +// } + // A function to retrieve zetas so that we can add a post-condition #[inline(always)] #[hax_lib::fstar::verification_status(panic_free)] @@ -87,42 +183,95 @@ fn from_i16_array(a: &[i16]) -> PolynomialRingElement + add_vector_pre ${myself}.f_coefficients.[ sz i ] ${rhs}.f_coefficients.[ sz i ]"#))] +#[hax_lib::ensures(|result| fstar!(r#"forall (i:nat). i < v (Core.Slice.impl__len ${myself}.f_coefficients) ==> + add_vector_post ${myself}_future.f_coefficients.[ sz i ] ${myself}.f_coefficients.[ sz i ] ${rhs}.f_coefficients.[ sz i ]"#))] fn add_to_ring_element( myself: &mut PolynomialRingElement, rhs: &PolynomialRingElement, ) { + let _myself = myself.coefficients; // The semicolon and parentheses at the end of loop are a workaround // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..myself.coefficients.len() { - myself.coefficients[i] = Vector::add(myself.coefficients[i], &rhs.coefficients[i]); + hax_lib::loop_invariant!(|i: usize| { fstar!( + r#"(v $i < v (Core.Slice.impl__len myself.f_coefficients) ==> + (forall (j:nat). (j >= v $i /\ j < v (Core.Slice.impl__len myself.f_coefficients)) ==> + myself.f_coefficients.[ sz j ] == ${_myself}.[ sz j ] /\ + add_vector_pre myself.f_coefficients.[ sz j ] ${rhs}.f_coefficients.[ sz j ])) /\ + (forall (j:nat). j < v $i ==> + add_vector_post myself.f_coefficients.[ sz j ] ${_myself}.[ sz j ] ${rhs}.f_coefficients.[ sz j ])"#) + }); + myself.coefficients[i] = add_vector(myself.coefficients[i], &rhs.coefficients[i]); } () } #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::requires(fstar!(r#"forall (i:nat). i < v $VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${myself}.f_coefficients.[ sz i ])"#))] fn poly_barrett_reduce(myself: &mut PolynomialRingElement) { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting // The semicolon and parentheses at the end of loop are a workaround // for the following bug https://github.com/hacspec/hax/issues/720 for i in 0..VECTORS_IN_RING_ELEMENT { + hax_lib::loop_invariant!(|i: usize| { fstar!( + r#"v $i < v $VECTORS_IN_RING_ELEMENT ==> + (forall (j:nat). (j >= v $i /\ j < v $VECTORS_IN_RING_ELEMENT) ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.f_coefficients.[ sz j ]))"#) + }); myself.coefficients[i] = Vector::barrett_reduce(myself.coefficients[i]); } () } #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::fstar::before(r#"#push-options "--z3rlimit 200 --ext context_pruning" + +let subtract_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (myself: t_Array v_Vector (sz 16)) + (coefficient_normal_form: v_Vector) : Lemma + (requires (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ])) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form)) + (ensures (forall (i:nat). i < 16 ==> sub_vector_pre myself.[ sz i ] coefficient_normal_form /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (sub_vector myself.[ sz i ] coefficient_normal_form)))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%sub_vector_pre) (sub_vector_pre #v_Vector); + reveal_opaque (`%sub_vector_post) (sub_vector_post #v_Vector); + assert_norm (pow2 15 == 32768); + assert (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ])); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb 28296 + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ]) j) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j)))); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array myself.[ sz i ]) j) - + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j)))) + +#pop-options"#)] +#[hax_lib::requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${myself}.f_coefficients.[ sz i ])"#))] fn subtract_reduce( myself: &PolynomialRingElement, mut b: PolynomialRingElement, ) -> PolynomialRingElement { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting for i in 0..VECTORS_IN_RING_ELEMENT { let coefficient_normal_form = - Vector::montgomery_multiply_by_constant(b.coefficients[i], 1441); - b.coefficients[i] = Vector::barrett_reduce(Vector::sub( + Vector::montgomery_multiply_by_constant(b.coefficients[i], 1441); + hax_lib::fstar!( + r#"subtract_reduce_helper ${myself}.f_coefficients $coefficient_normal_form"#); + b.coefficients[i] = Vector::barrett_reduce(sub_vector( myself.coefficients[i], &coefficient_normal_form, )); @@ -131,13 +280,30 @@ fn subtract_reduce( } #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::fstar::before(r#"let add_message_error_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (result coefficient_normal_form: v_Vector) : Lemma + (requires (Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array result) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form))) + (ensures (add_vector_pre coefficient_normal_form result /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector coefficient_normal_form result)))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%add_vector_pre) (add_vector_pre #v_Vector); + reveal_opaque (`%add_vector_post) (add_vector_post #v_Vector); + assert_norm (pow2 15 == 32768)"#)] +#[hax_lib::requires(fstar!(r#"(forall (i:nat). i < 16 ==> + add_vector_pre ${myself}.f_coefficients.[ sz i ] ${message}.f_coefficients.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque (28296 - 3328) (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector ${myself}.f_coefficients.[ sz i ] ${message}.f_coefficients.[ sz i ])))"#))] fn add_message_error_reduce( myself: &PolynomialRingElement, message: &PolynomialRingElement, mut result: PolynomialRingElement, ) -> PolynomialRingElement { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting for i in 0..VECTORS_IN_RING_ELEMENT { let coefficient_normal_form = Vector::montgomery_multiply_by_constant(result.coefficients[i], 1441); @@ -158,39 +324,76 @@ fn add_message_error_reduce( // )); // ``` - let tmp = Vector::add(myself.coefficients[i], &message.coefficients[i]); - let tmp = Vector::add(coefficient_normal_form, &tmp); + let tmp = add_vector(myself.coefficients[i], &message.coefficients[i]); + hax_lib::fstar!( + r#"add_message_error_reduce_helper $tmp $coefficient_normal_form"#); + let tmp = add_vector(coefficient_normal_form, &tmp); result.coefficients[i] = Vector::barrett_reduce(tmp); } result } #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::fstar::before(r#"#push-options "--max_fuel 3 --z3rlimit 200 --ext context_pruning --z3refresh" + +let add_error_reduce_helper (#v_Vector: Type0) + {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |} + (error: t_Array v_Vector (sz 16)) + (coefficient_normal_form: v_Vector) : Lemma + (requires (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ])) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form)) + (ensures (forall (i:nat). i < 16 ==> add_vector_pre coefficient_normal_form error.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque 28296 (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector coefficient_normal_form error.[ sz i ])))) + = + reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque; + reveal_opaque (`%add_vector_pre) (add_vector_pre #v_Vector); + reveal_opaque (`%add_vector_post) (add_vector_post #v_Vector); + reveal_opaque (`%add_vector) (add_vector #v_Vector); + assert_norm (pow2 15 == 32768); + assert (forall (i:nat). i < 16 ==> + Spec.Utils.is_i16b_array (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ])); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb 28296 + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ]) j)))); + assert (forall (i:nat). i < 16 ==> (forall j. j < 16 ==> + Spec.Utils.is_intb (pow2 15 - 1) + (v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array coefficient_normal_form) j) + + v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array error.[ sz i ]) j)))) + +#pop-options"#)] +#[hax_lib::requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${error}.f_coefficients.[ sz i ])"#))] fn add_error_reduce( myself: &mut PolynomialRingElement, error: &PolynomialRingElement, ) { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting // The semicolon and parentheses at the end of loop are a workaround // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { let coefficient_normal_form = Vector::montgomery_multiply_by_constant(myself.coefficients[j], 1441); + hax_lib::fstar!( + r#"add_error_reduce_helper ${error}.f_coefficients $coefficient_normal_form"#); myself.coefficients[j] = - Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); + Vector::barrett_reduce(add_vector(coefficient_normal_form, &error.coefficients[j])); } () } #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${error}.f_coefficients.[ sz i ])"#))] fn add_standard_error_reduce( myself: &mut PolynomialRingElement, error: &PolynomialRingElement, ) { - // Using `hax_lib::fstar::verification_status(lax)` works but produces an error while extracting // The semicolon and parentheses at the end of loop are a workaround // for the following bug https://github.com/hacspec/hax/issues/720 for j in 0..VECTORS_IN_RING_ELEMENT { @@ -198,8 +401,10 @@ fn add_standard_error_reduce( // calling to_montgomery_domain() on them should return a mod q. let coefficient_normal_form = to_standard_domain::(myself.coefficients[j]); + hax_lib::fstar!( + r#"add_error_reduce_helper ${error}.f_coefficients $coefficient_normal_form"#); myself.coefficients[j] = - Vector::barrett_reduce(Vector::add(coefficient_normal_form, &error.coefficients[j])); + Vector::barrett_reduce(add_vector(coefficient_normal_form, &error.coefficients[j])); } () } @@ -243,7 +448,12 @@ fn add_standard_error_reduce( // result.coefficients[i].abs() <= FIELD_MODULUS // ))))] #[inline(always)] -#[hax_lib::fstar::verification_status(lax)] +#[hax_lib::fstar::options("--z3rlimit 200 --ext context_pruning")] +#[hax_lib::requires(fstar!(r#"forall (i:nat). i < v $VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${myself}.f_coefficients.[ sz i ]) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${rhs}.f_coefficients.[ sz i ])"#))] fn ntt_multiply( myself: &PolynomialRingElement, rhs: &PolynomialRingElement, @@ -284,36 +494,56 @@ impl PolynomialRingElement { /// Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise /// sum of their constituent coefficients. #[inline(always)] + #[hax_lib::requires(fstar!(r#"forall (i:nat). i < v (Core.Slice.impl__len self.f_coefficients) ==> + add_vector_pre self.f_coefficients.[ sz i ] ${rhs}.f_coefficients.[ sz i ]"#))] pub(crate) fn add_to_ring_element(&mut self, rhs: &Self) { add_to_ring_element::(self, rhs); } #[inline(always)] + #[requires(fstar!(r#"forall (i:nat). i < v $VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 28296 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ])"#))] pub(crate) fn poly_barrett_reduce(&mut self) { poly_barrett_reduce(self); } #[inline(always)] + #[requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ])"#))] pub(crate) fn subtract_reduce(&self, b: Self) -> Self { subtract_reduce(self, b) } #[inline(always)] + #[requires(fstar!(r#"(forall (i:nat). i < 16 ==> + add_vector_pre self.f_coefficients.[ sz i ] ${message}.f_coefficients.[ sz i ] /\ + Spec.Utils.is_i16b_array_opaque (28296 - 3328) (Libcrux_ml_kem.Vector.Traits.f_to_i16_array + (add_vector self.f_coefficients.[ sz i ] ${message}.f_coefficients.[ sz i ])))"#))] pub(crate) fn add_message_error_reduce(&self, message: &Self, result: Self) -> Self { add_message_error_reduce(self, message, result) } #[inline(always)] + #[requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${error}.f_coefficients.[ sz i ])"#))] pub(crate) fn add_error_reduce(&mut self, error: &Self) { add_error_reduce(self, error); } #[inline(always)] + #[requires(fstar!(r#"forall (i:nat). i < 16 ==> Spec.Utils.is_i16b_array_opaque (28296 - 3328) + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${error}.f_coefficients.[ sz i ])"#))] pub(crate) fn add_standard_error_reduce(&mut self, error: &Self) { add_standard_error_reduce(self, error); } #[inline(always)] + #[requires(fstar!(r#"forall (i:nat). i < v $VECTORS_IN_RING_ELEMENT ==> + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array self.f_coefficients.[ sz i ]) /\ + Spec.Utils.is_i16b_array_opaque 3328 + (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${rhs}.f_coefficients.[ sz i ])"#))] pub(crate) fn ntt_multiply(&self, rhs: &Self) -> Self { ntt_multiply(self, rhs) } diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs index 730fe0e6c..be3d944c0 100644 --- a/libcrux-ml-kem/src/vector/avx2.rs +++ b/libcrux-ml-kem/src/vector/avx2.rs @@ -341,17 +341,20 @@ impl Operations for SIMD256Vector { cond_subtract_3329(vector) } - #[requires(fstar!(r#"Spec.Utils.is_i16b_array 28296 (impl.f_repr ${vector})"#))] + #[requires(fstar!(r#"Spec.Utils.is_i16b_array_opaque 28296 (impl.f_repr ${vector})"#))] #[inline(always)] fn barrett_reduce(vector: Self) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); Self { elements: arithmetic::barrett_reduce(vector.elements), } } #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 $constant"#))] + #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr $out)"#))] #[inline(always)] fn montgomery_multiply_by_constant(vector: Self, constant: i16) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); Self { elements: arithmetic::montgomery_multiply_by_constant(vector.elements, constant), } @@ -448,9 +451,9 @@ impl Operations for SIMD256Vector { #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr ${lhs}) /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr ${rhs})"#))] - #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr ${lhs}) /\ + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr ${rhs})"#))] + #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr $out)"#))] #[inline(always)] fn ntt_multiply( lhs: &Self, @@ -460,6 +463,7 @@ impl Operations for SIMD256Vector { zeta2: i16, zeta3: i16, ) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); ntt_multiply(lhs, rhs, zeta0, zeta1, zeta2, zeta3) } diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs index 58ccdf1e0..eae8fb0e5 100644 --- a/libcrux-ml-kem/src/vector/portable.rs +++ b/libcrux-ml-kem/src/vector/portable.rs @@ -169,13 +169,16 @@ impl Operations for PortableVector { cond_subtract_3329(v) } - #[requires(fstar!(r#"Spec.Utils.is_i16b_array 28296 (impl.f_repr ${v})"#))] + #[requires(fstar!(r#"Spec.Utils.is_i16b_array_opaque 28296 (impl.f_repr ${v})"#))] fn barrett_reduce(v: Self) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); barrett_reduce(v) } #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 $r"#))] + #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr $out)"#))] fn montgomery_multiply_by_constant(v: Self, r: i16) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); montgomery_multiply_by_constant(v, r) } @@ -257,9 +260,9 @@ impl Operations for PortableVector { #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr ${lhs}) /\ - Spec.Utils.is_i16b_array 3328 (impl.f_repr ${rhs})"#))] - #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (impl.f_repr $out)"#))] + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr ${lhs}) /\ + Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr ${rhs})"#))] + #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (impl.f_repr $out)"#))] fn ntt_multiply( lhs: &Self, rhs: &Self, @@ -268,6 +271,7 @@ impl Operations for PortableVector { zeta2: i16, zeta3: i16, ) -> Self { + hax_lib::fstar!(r#"reveal_opaque (`%Spec.Utils.is_i16b_array_opaque) Spec.Utils.is_i16b_array_opaque"#); ntt_multiply(lhs, rhs, zeta0, zeta1, zeta2, zeta3) } diff --git a/libcrux-ml-kem/src/vector/traits.rs b/libcrux-ml-kem/src/vector/traits.rs index 2263b02d3..efc2e42d3 100644 --- a/libcrux-ml-kem/src/vector/traits.rs +++ b/libcrux-ml-kem/src/vector/traits.rs @@ -66,10 +66,11 @@ pub trait Operations: Copy + Clone + Repr { #[ensures(|result| fstar!(r#"f_repr $result == Spec.Utils.map_array (fun x -> if x >=. 3329s then x -! 3329s else x) (f_repr $v)"#))] fn cond_subtract_3329(v: Self) -> Self; - #[requires(fstar!(r#"Spec.Utils.is_i16b_array 28296 (f_repr $vector)"#))] + #[requires(fstar!(r#"Spec.Utils.is_i16b_array_opaque 28296 (f_repr $vector)"#))] fn barrett_reduce(vector: Self) -> Self; #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 c"#))] + #[ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (f_repr $result)"#))] fn montgomery_multiply_by_constant(v: Self, c: i16) -> Self; // Compression @@ -128,9 +129,9 @@ pub trait Operations: Copy + Clone + Repr { #[requires(fstar!(r#"Spec.Utils.is_i16b 1664 zeta0 /\ Spec.Utils.is_i16b 1664 zeta1 /\ Spec.Utils.is_i16b 1664 zeta2 /\ Spec.Utils.is_i16b 1664 zeta3 /\ - Spec.Utils.is_i16b_array 3328 (f_repr ${lhs}) /\ - Spec.Utils.is_i16b_array 3328 (f_repr ${rhs}) "#))] - #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array 3328 (f_repr $out)"#))] + Spec.Utils.is_i16b_array_opaque 3328 (f_repr ${lhs}) /\ + Spec.Utils.is_i16b_array_opaque 3328 (f_repr ${rhs}) "#))] + #[ensures(|out| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (f_repr $out)"#))] fn ntt_multiply(lhs: &Self, rhs: &Self, zeta0: i16, zeta1: i16, zeta2: i16, zeta3: i16) -> Self; @@ -228,6 +229,7 @@ pub fn montgomery_multiply_fe(v: T, fer: i16) -> T { } #[inline(always)] +#[hax_lib::ensures(|result| fstar!(r#"Spec.Utils.is_i16b_array_opaque 3328 (i1._super_8706949974463268012.f_repr $result)"#))] pub fn to_standard_domain(v: T) -> T { T::montgomery_multiply_by_constant(v, MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS as i16) }