From 7ddbda4b824b04fd06e6ab9973218a12e1834d6d Mon Sep 17 00:00:00 2001 From: xvzcf Date: Thu, 26 Oct 2023 17:06:20 -0400 Subject: [PATCH 1/5] Rearranged some code to speed things up and get bounds on compress_q and decompress_q. --- .../Libcrux.Kem.Kyber.Arithmetic.fst | 2 - .../extraction/Libcrux.Kem.Kyber.Compress.fst | 33 ++- .../extraction/Libcrux.Kem.Kyber.Ind_cpa.fst | 53 +--- .../extraction/Libcrux.Kem.Kyber.Ntt.fst | 269 +++++++++++++++--- proofs/fstar/extraction/Libcrux.Kem.Kyber.fst | 19 +- src/kem/kyber/arithmetic.rs | 8 - src/kem/kyber/compress.rs | 9 +- src/kem/kyber/ind_cpa.rs | 21 +- src/kem/kyber/ntt.rs | 104 ++++--- 9 files changed, 347 insertions(+), 171 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst index 5c1b9139d..dade74105 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst @@ -155,8 +155,6 @@ let montgomery_reduce (value: i32) : i32 = in reduced -let to_montgomery_domain (value: i32) : i32 = montgomery_reduce (1353l *! value <: i32) - type t_KyberPolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) } let impl__KyberPolynomialRingElement__ZERO: t_KyberPolynomialRingElement = diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst index 501b543f5..fcb5d19e6 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst @@ -7,15 +7,27 @@ let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 = if true then let _:Prims.unit = - if ~.(v_COEFFICIENT_BITS <=. Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT <: bool) + if ~.(v_COEFFICIENT_BITS <=. sz 11 <: bool) then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= BITS_PER_COEFFICIENT" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= 11" <: Rust_primitives.Hax.t_Never) in () in + let _:Prims.unit = + if true + then + let _:Prims.unit = + if ~.(fe <. 3329us <: bool) + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: fe < 3329" + <: + Rust_primitives.Hax.t_Never) + in + () + in let compressed:u32 = (cast fe <: u32) < - Rust_primitives.Hax.update_at u - i - ((Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (u.[ i ] - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +! - (error_1_.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) + Libcrux.Kem.Kyber.Ntt.compute_vector_u v_A_transpose r_as_ntt error_1_ in let message_as_ring_element:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Libcrux.Kem.Kyber.Serialize.deserialize_then_decompress_message message in let v:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - ((Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (Libcrux.Kem.Kyber.Ntt.multiply_row_by_column_montgomery - tt_as_ntt - r_as_ntt - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +! - error_2_ - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +! - message_as_ring_element + Libcrux.Kem.Kyber.Ntt.compute_ring_element_v tt_as_ntt r_as_ntt error_2_ message_as_ring_element in let c1:t_Array u8 v_C1_LEN = compress_then_encode_u u in let c2:t_Array u8 v_C2_LEN = @@ -729,7 +697,7 @@ let decrypt let u_as_ntt:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.update_at u_as_ntt i - (Libcrux.Kem.Kyber.Ntt.ntt_representation u + (Libcrux.Kem.Kyber.Ntt.ntt_vector_u u <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) in @@ -764,13 +732,6 @@ let decrypt t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) in let message:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - v -! - (Libcrux.Kem.Kyber.Ntt.invert_ntt_montgomery (Libcrux.Kem.Kyber.Ntt.multiply_row_by_column_montgomery - secret_as_ntt - u_as_ntt - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + Libcrux.Kem.Kyber.Ntt.compute_message v secret_as_ntt u_as_ntt in Libcrux.Kem.Kyber.Serialize.compress_then_serialize_message message \ No newline at end of file diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst index 7e54384e1..7b53acd0b 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst @@ -21,10 +21,10 @@ let v_ZETAS_MONTGOMERY_DOMAIN: t_Array i32 (sz 128) = FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 128); Rust_primitives.Hax.array_of_list list -let ntt_with_debug_asserts +let ntt_binomially_sampled_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - (coefficient_bound: i32) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + let coefficient_bound:i32 = 3l in let _:Prims.unit = if true then @@ -584,7 +584,9 @@ let ntt_with_debug_asserts in re -let ntt_representation (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +let ntt_vector_u + (#v_VECTOR_U_COMPRESSION_FACTOR: usize) + (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = let zeta_i:usize = sz 0 in let re, zeta_i:(Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement & usize) = @@ -1238,21 +1240,6 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin in re, zeta_i) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - { - re with - Libcrux.Kem.Kyber.Arithmetic.f_coefficients - = - Core.Array.impl_23__map re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients - (fun coefficient -> - Libcrux.Kem.Kyber.Arithmetic.barrett_reduce (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce - (coefficient *! 1441l <: i32) - <: - i32) - <: - i32) - } - in re let ntt_multiply_binomials (a0, a1: (i32 & i32)) (b0, b1: (i32 & i32)) (zeta: i32) : (i32 & i32) = @@ -1380,9 +1367,10 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing in out -let multiply_row_by_column_montgomery +let compute_message (#v_K: usize) - (row_vector column_vector: + (v: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + (secret_as_ntt u_as_ntt: t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -1390,12 +1378,12 @@ let multiply_row_by_column_montgomery in let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip - (Core.Slice.impl__iter (Rust_primitives.unsize row_vector + (Core.Slice.impl__iter (Rust_primitives.unsize secret_as_ntt <: t_Slice Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) <: Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - (Core.Slice.impl__iter (Rust_primitives.unsize column_vector + (Core.Slice.impl__iter (Rust_primitives.unsize u_as_ntt <: t_Slice Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) <: @@ -1409,9 +1397,9 @@ let multiply_row_by_column_montgomery (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) result - (fun result (row_element, column_element) -> + (fun result (secret_element, u_element) -> result +! - (ntt_multiply row_element column_element + (ntt_multiply secret_element u_element <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) <: @@ -1426,12 +1414,148 @@ let multiply_row_by_column_montgomery Libcrux.Kem.Kyber.Arithmetic.barrett_reduce } in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + invert_ntt_montgomery result + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end + = + Core.Slice.impl__len (Rust_primitives.unsize result + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + t_Slice i32) + <: + usize + }) + <: + Core.Ops.Range.t_Range usize) + result + (fun result i -> + let coefficient_normal_form:i32 = + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((result + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] + <: + i32) *! + 1441l + <: + i32) + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + result with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at result.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + i + (Libcrux.Kem.Kyber.Arithmetic.barrett_reduce ((v + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] + <: + i32) -! + coefficient_normal_form + <: + i32) + <: + i32) + } + in + result) + in result -let multiply_matrix_by_column_montgomery +let compute_ring_element_v (#v_K: usize) - (matrix: t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K) - (vector: t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) + (tt_as_ntt r_as_ntt: t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) + (error_2_ message: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_zip + (Core.Slice.impl__iter (Rust_primitives.unsize tt_as_ntt + <: + t_Slice Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + <: + Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + (Core.Slice.impl__iter (Rust_primitives.unsize r_as_ntt + <: + t_Slice Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + <: + Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + <: + Core.Iter.Adapters.Zip.t_Zip + (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) + <: + Core.Iter.Adapters.Zip.t_Zip + (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) + result + (fun result (tt_element, r_element) -> + result +! + (ntt_multiply tt_element r_element + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + invert_ntt_montgomery result + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end + = + Core.Slice.impl__len (Rust_primitives.unsize result + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + t_Slice i32) + <: + usize + }) + <: + Core.Ops.Range.t_Range usize) + result + (fun result i -> + let coefficient_normal_form:i32 = + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((result + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] + <: + i32) *! + 1441l + <: + i32) + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + result with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at result.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + i + (Libcrux.Kem.Kyber.Arithmetic.barrett_reduce ((coefficient_normal_form +! + (error_2_.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] <: i32) + <: + i32) +! + (message.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] <: i32) + <: + i32) + <: + i32) + } + in + result) + in + result + +let compute_vector_u + (#v_K: usize) + (a_as_ntt: + t_Array (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) v_K) + (r_as_ntt error_1_: t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) : t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__KyberPolynomialRingElement__ZERO @@ -1439,7 +1563,7 @@ let multiply_matrix_by_column_montgomery in let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate - (Core.Slice.impl__iter (Rust_primitives.unsize matrix + (Core.Slice.impl__iter (Rust_primitives.unsize a_as_ntt <: t_Slice (t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K)) <: @@ -1471,10 +1595,10 @@ let multiply_matrix_by_column_montgomery Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) result - (fun result (j, matrix_element) -> + (fun result (j, a_element) -> let product:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - ntt_multiply matrix_element - (vector.[ j ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + ntt_multiply a_element + (r_as_ntt.[ j ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) in let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.update_at result @@ -1489,20 +1613,68 @@ let multiply_matrix_by_column_montgomery let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.update_at result i - ({ - (result.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) with - Libcrux.Kem.Kyber.Arithmetic.f_coefficients - = - Core.Array.impl_23__map (result.[ i ] - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - .Libcrux.Kem.Kyber.Arithmetic.f_coefficients - Libcrux.Kem.Kyber.Arithmetic.barrett_reduce - <: - t_Array i32 (sz 256) - }) + (invert_ntt_montgomery (result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) in - result) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end + = + Core.Slice.impl__len (Rust_primitives.unsize (result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + t_Slice i32) + <: + usize + }) + <: + Core.Ops.Range.t_Range usize) + result + (fun result j -> + let coefficient_normal_form:i32 = + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (((result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] + <: + i32) *! + 1441l + <: + i32) + in + let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = + Rust_primitives.Hax.update_at result + i + ({ + (result.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at (result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + (Libcrux.Kem.Kyber.Arithmetic.barrett_reduce (coefficient_normal_form +! + ((error_1_.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] + <: + i32) + <: + i32) + <: + i32) + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement + }) + in + result)) in result @@ -1608,10 +1780,13 @@ let compute_As_plus_e result (fun result j -> let coefficient_normal_form:i32 = - Libcrux.Kem.Kyber.Arithmetic.to_montgomery_domain ((result.[ i ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (((result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] + i32) *! + 1353l <: i32) in diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst index cd26d4d1b..99fb81fca 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst @@ -323,16 +323,9 @@ let generate_keypair (randomness: t_Array u8 (sz 64)) : Core.Result.t_Result (t_KyberKeyPair v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE) t_BadRejectionSamplingRandomnessError = - let ind_cpa_keypair_randomness:t_Slice u8 = - randomness.[ { - Core.Ops.Range.f_start = sz 0; - Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE - } ] - in - let implicit_rejection_value:t_Slice u8 = - randomness.[ { - Core.Ops.Range.f_start = Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE - } ] + let ind_cpa_keypair_randomness, implicit_rejection_value:(t_Slice u8 & t_Slice u8) = + Core.Slice.impl__split_at (Rust_primitives.unsize randomness <: t_Slice u8) + Libcrux.Kem.Kyber.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE in let (ind_cpa_private_key, public_key), sampling_a_error:((Libcrux.Kem.Kyber.Ind_cpa.t_PrivateKey v_CPA_PRIVATE_KEY_SIZE & @@ -408,9 +401,9 @@ let encapsulate randomness pseudorandomness in - if Core.Option.impl__is_some sampling_a_error - then Core.Result.Result_Err (Core.Option.impl__unwrap sampling_a_error) - else + match sampling_a_error with + | Core.Option.Option_Some e -> Core.Result.Result_Err e + | Core.Option.Option_None -> Core.Result.Result_Ok (ciphertext, Core.Result.impl__unwrap (Core.Convert.f_try_into shared_secret diff --git a/src/kem/kyber/arithmetic.rs b/src/kem/kyber/arithmetic.rs index 67766650e..a554c4f22 100644 --- a/src/kem/kyber/arithmetic.rs +++ b/src/kem/kyber/arithmetic.rs @@ -42,14 +42,6 @@ pub(crate) fn montgomery_reduce(value: KyberFieldElement) -> KyberFieldElement { reduced } -// Given a |value|, return |value|*R mod q. Notice that montgomery_reduce -// returns a value aR^{-1} mod q, and so montgomery_reduce(|value| * R^2) -// returns |value| * R^2 & R^{-1} mod q = |value| * R mod q. -pub(crate) fn to_montgomery_domain(value: KyberFieldElement) -> KyberFieldElement { - // R^2 mod q = (2^16)^2 mod 3329 = 1353 - montgomery_reduce(1353 * value) -} - #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct KyberPolynomialRingElement { pub(crate) coefficients: [KyberFieldElement; COEFFICIENTS_IN_RING_ELEMENT], diff --git a/src/kem/kyber/compress.rs b/src/kem/kyber/compress.rs index 21c205790..e0e6434ba 100644 --- a/src/kem/kyber/compress.rs +++ b/src/kem/kyber/compress.rs @@ -1,11 +1,12 @@ use super::{ arithmetic::{KyberFieldElement, KyberPolynomialRingElement}, - constants::{BITS_PER_COEFFICIENT, FIELD_MODULUS}, + constants::FIELD_MODULUS, conversions::to_unsigned_representative, }; pub(super) fn compress_q(fe: u16) -> KyberFieldElement { - debug_assert!(COEFFICIENT_BITS <= BITS_PER_COEFFICIENT); + debug_assert!(COEFFICIENT_BITS <= 11); + debug_assert!(fe < 3329); let mut compressed = (fe as u32) << (COEFFICIENT_BITS + 1); compressed += FIELD_MODULUS as u32; @@ -13,6 +14,7 @@ pub(super) fn compress_q(fe: u16) -> KyberFieldEl (compressed & ((1u32 << COEFFICIENT_BITS) - 1)) as KyberFieldElement } + pub fn compress( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { @@ -25,7 +27,8 @@ pub fn compress( pub(super) fn decompress_q( fe: KyberFieldElement, ) -> KyberFieldElement { - debug_assert!(COEFFICIENT_BITS <= BITS_PER_COEFFICIENT); + debug_assert!(COEFFICIENT_BITS <= 11); + debug_assert!(0 <= fe && fe < (1 << 11)); let mut decompressed = (fe as u32) * (FIELD_MODULUS as u32); decompressed = (decompressed << 1) + (1 << COEFFICIENT_BITS); diff --git a/src/kem/kyber/ind_cpa.rs b/src/kem/kyber/ind_cpa.rs index 5da4f9fa3..b1a84a57d 100644 --- a/src/kem/kyber/ind_cpa.rs +++ b/src/kem/kyber/ind_cpa.rs @@ -84,7 +84,7 @@ fn cbd( let prf_output: [u8; ETA_RANDOMNESS_SIZE] = PRF(&prf_input); let r = sample_from_binomial_distribution::(&prf_output); - re_as_ntt[i] = ntt_with_debug_asserts(r, ETA as i32); + re_as_ntt[i] = ntt_binomially_sampled_ring_element(r); } (re_as_ntt, domain_separator) } @@ -148,7 +148,7 @@ pub(crate) fn generate_keypair< let secret = sample_from_binomial_distribution::(&prf_output); - secret_as_ntt[i] = ntt_with_debug_asserts(secret, ETA1 as i32); + secret_as_ntt[i] = ntt_binomially_sampled_ring_element(secret); } // for i from 0 to k−1 do @@ -163,7 +163,7 @@ pub(crate) fn generate_keypair< let prf_output: [u8; ETA1_RANDOMNESS_SIZE] = PRF(&prf_input); let error = sample_from_binomial_distribution::(&prf_output); - error_as_ntt[i] = ntt_with_debug_asserts(error, ETA1 as i32); + error_as_ntt[i] = ntt_binomially_sampled_ring_element(error); } // tˆ := Aˆ ◦ sˆ + eˆ @@ -271,16 +271,11 @@ pub(crate) fn encrypt< let error_2 = sample_from_binomial_distribution::(&prf_output); // u := NTT^{-1}(AˆT ◦ rˆ) + e_1 - let mut u = multiply_matrix_by_column_montgomery(&A_transpose, &r_as_ntt); - for i in 0..K { - u[i] = invert_ntt_montgomery(u[i]) + error_1[i]; - } + let u = compute_vector_u(&A_transpose, &r_as_ntt, &error_1); // v := NTT^{−1}(tˆT ◦ rˆ) + e_2 + Decompress_q(Decode_1(m),1) let message_as_ring_element = deserialize_then_decompress_message(message); - let v = invert_ntt_montgomery(multiply_row_by_column_montgomery(&t_as_ntt, &r_as_ntt)) - + error_2 - + message_as_ring_element; + let v = compute_ring_element_v(&t_as_ntt, &r_as_ntt, &error_2, &message_as_ring_element); // c_1 := Encode_{du}(Compress_q(u,d_u)) let c1 = compress_then_encode_u::(u); @@ -317,7 +312,7 @@ pub(crate) fn decrypt< let u = decompress::(deserialize_little_endian::< VECTOR_U_COMPRESSION_FACTOR, >(u_bytes)); - u_as_ntt[i] = ntt_representation(u); + u_as_ntt[i] = ntt_vector_u::(u); } // v := Decompress_q(Decode_{d_v}(c + d_u·k·n / 8), d_v) @@ -331,8 +326,6 @@ pub(crate) fn decrypt< } // m := Encode_1(Compress_q(v − NTT^{−1}(sˆT ◦ NTT(u)) , 1)) - let message = - v - invert_ntt_montgomery(multiply_row_by_column_montgomery(&secret_as_ntt, &u_as_ntt)); - + let message = compute_message(&v, &secret_as_ntt, &u_as_ntt); compress_then_serialize_message(message) } diff --git a/src/kem/kyber/ntt.rs b/src/kem/kyber/ntt.rs index 6cfc00cbc..c40f35424 100644 --- a/src/kem/kyber/ntt.rs +++ b/src/kem/kyber/ntt.rs @@ -1,7 +1,6 @@ use super::{ arithmetic::{ - barrett_reduce, montgomery_reduce, to_montgomery_domain, KyberFieldElement, - KyberPolynomialRingElement, + barrett_reduce, montgomery_reduce, KyberFieldElement, KyberPolynomialRingElement, }, constants::{COEFFICIENTS_IN_RING_ELEMENT, FIELD_MODULUS}, }; @@ -21,10 +20,10 @@ const ZETAS_MONTGOMERY_DOMAIN: [KyberFieldElement; 128] = [ // invocations to this function, upon which this function will be renamed back to // ntt_representation(). #[inline(always)] -pub(in crate::kem::kyber) fn ntt_with_debug_asserts( +pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( mut re: KyberPolynomialRingElement, - coefficient_bound: i32, ) -> KyberPolynomialRingElement { + let coefficient_bound = 3; debug_assert!(re .coefficients .into_iter() @@ -84,12 +83,12 @@ pub(in crate::kem::kyber) fn ntt_with_debug_asserts( } #[inline(always)] -pub(in crate::kem::kyber) fn ntt_representation( +pub(in crate::kem::kyber) fn ntt_vector_u( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { let mut zeta_i = 0; - macro_rules! layers { + macro_rules! ntt_at_layer { ($layer:literal) => { for offset in (0..(COEFFICIENTS_IN_RING_ELEMENT - $layer)).step_by(2 * $layer) { zeta_i += 1; @@ -103,13 +102,13 @@ pub(in crate::kem::kyber) fn ntt_representation( }; } - layers!(128); - layers!(64); - layers!(32); - layers!(16); - layers!(8); - layers!(4); - layers!(2); + ntt_at_layer!(128); + ntt_at_layer!(64); + ntt_at_layer!(32); + ntt_at_layer!(16); + ntt_at_layer!(8); + ntt_at_layer!(4); + ntt_at_layer!(2); re.coefficients = re.coefficients.map(barrett_reduce); @@ -117,9 +116,7 @@ pub(in crate::kem::kyber) fn ntt_representation( } #[inline(always)] -pub(in crate::kem::kyber) fn invert_ntt_montgomery( - mut re: KyberPolynomialRingElement, -) -> KyberPolynomialRingElement { +fn invert_ntt_montgomery(mut re: KyberPolynomialRingElement) -> KyberPolynomialRingElement { let mut zeta_i = COEFFICIENTS_IN_RING_ELEMENT / 2; macro_rules! layers { @@ -149,10 +146,6 @@ pub(in crate::kem::kyber) fn invert_ntt_montgomery( layers!(64); layers!(128); - re.coefficients = re - .coefficients - .map(|coefficient| barrett_reduce(montgomery_reduce(coefficient * 1441))); - re } @@ -207,36 +200,79 @@ fn ntt_multiply( out } +// v := NTT^{−1}(tˆT ◦ rˆ) + e_2 + Decompress_q(Decode_1(m),1) #[inline(always)] -pub(in crate::kem::kyber) fn multiply_row_by_column_montgomery( - row_vector: &[KyberPolynomialRingElement; K], - column_vector: &[KyberPolynomialRingElement; K], +pub(in crate::kem::kyber) fn compute_message( + v: &KyberPolynomialRingElement, + secret_as_ntt: &[KyberPolynomialRingElement; K], + u_as_ntt: &[KyberPolynomialRingElement; K], ) -> KyberPolynomialRingElement { let mut result = KyberPolynomialRingElement::ZERO; - for (row_element, column_element) in row_vector.iter().zip(column_vector.iter()) { - result = result + ntt_multiply(row_element, column_element); + for (secret_element, u_element) in secret_as_ntt.iter().zip(u_as_ntt.iter()) { + result = result + ntt_multiply(secret_element, u_element); } - + // TODO: Without this, there's a failure in Kyber-1024. We need to see if + // this round of barrett reductions can be removed. result.coefficients = result.coefficients.map(barrett_reduce); + result = invert_ntt_montgomery(result); + + for i in 0..result.coefficients.len() { + let coefficient_normal_form = montgomery_reduce(result.coefficients[i] * 1441); + result.coefficients[i] = barrett_reduce(v.coefficients[i] - coefficient_normal_form); + } + + result +} + +// v := NTT^{−1}(tˆT ◦ rˆ) + e_2 + Decompress_q(Decode_1(m),1) +#[inline(always)] +pub(in crate::kem::kyber) fn compute_ring_element_v( + t_as_ntt: &[KyberPolynomialRingElement; K], + r_as_ntt: &[KyberPolynomialRingElement; K], + error_2: &KyberPolynomialRingElement, + message: &KyberPolynomialRingElement, +) -> KyberPolynomialRingElement { + let mut result = KyberPolynomialRingElement::ZERO; + + for (t_element, r_element) in t_as_ntt.iter().zip(r_as_ntt.iter()) { + result = result + ntt_multiply(t_element, r_element); + } + result = invert_ntt_montgomery(result); + + for i in 0..result.coefficients.len() { + let coefficient_normal_form = montgomery_reduce(result.coefficients[i] * 1441); + result.coefficients[i] = barrett_reduce( + coefficient_normal_form + error_2.coefficients[i] + message.coefficients[i], + ); + } + result } +// u := NTT^{-1}(AˆT ◦ rˆ) + e_1 #[inline(always)] -pub(in crate::kem::kyber) fn multiply_matrix_by_column_montgomery( - matrix: &[[KyberPolynomialRingElement; K]; K], - vector: &[KyberPolynomialRingElement; K], +pub(in crate::kem::kyber) fn compute_vector_u( + a_as_ntt: &[[KyberPolynomialRingElement; K]; K], + r_as_ntt: &[KyberPolynomialRingElement; K], + error_1: &[KyberPolynomialRingElement; K], ) -> [KyberPolynomialRingElement; K] { let mut result = [KyberPolynomialRingElement::ZERO; K]; - for (i, row) in matrix.iter().enumerate() { - for (j, matrix_element) in row.iter().enumerate() { - let product = ntt_multiply(matrix_element, &vector[j]); + for (i, row) in a_as_ntt.iter().enumerate() { + for (j, a_element) in row.iter().enumerate() { + let product = ntt_multiply(a_element, &r_as_ntt[j]); result[i] = result[i] + product; } + result[i] = invert_ntt_montgomery(result[i]); + + for j in 0..result[i].coefficients.len() { + let coefficient_normal_form = montgomery_reduce(result[i].coefficients[j] * 1441); - result[i].coefficients = result[i].coefficients.map(barrett_reduce); + result[i].coefficients[j] = + barrett_reduce(coefficient_normal_form + error_1[i].coefficients[j]); + } } result @@ -269,7 +305,7 @@ pub(in crate::kem::kyber) fn compute_As_plus_e( for j in 0..result[i].coefficients.len() { // The coefficients are of the form aR^{-1} mod q, which means // calling to_montgomery_domain() on them should return a mod q. - let coefficient_normal_form = to_montgomery_domain(result[i].coefficients[j]); + let coefficient_normal_form = montgomery_reduce(result[i].coefficients[j] * 1353); result[i].coefficients[j] = barrett_reduce(coefficient_normal_form + error_as_ntt[i].coefficients[j]) From c0123314d6829dc9e6c30434c6bbeeb3140c20f4 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Thu, 26 Oct 2023 22:55:35 -0400 Subject: [PATCH 2/5] Slightly refine the precondition for decompress. --- proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst | 10 ++++++---- src/kem/kyber/compress.rs | 4 ++-- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst index fcb5d19e6..af919c9b7 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst @@ -20,9 +20,11 @@ let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 = if true then let _:Prims.unit = - if ~.(fe <. 3329us <: bool) + if + ~.((Core.Convert.f_from fe <: i32) <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: bool) then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: fe < 3329" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: i32::from(fe) < FIELD_MODULUS" + <: Rust_primitives.Hax.t_Never) in @@ -71,9 +73,9 @@ let decompress_q (#v_COEFFICIENT_BITS: usize) (fe: i32) : i32 = if true then let _:Prims.unit = - if ~.((0l <=. fe <: bool) && (fe <. (1l <(fe: u16) -> KyberFieldElement { debug_assert!(COEFFICIENT_BITS <= 11); - debug_assert!(fe < 3329); + debug_assert!(i32::from(fe) < FIELD_MODULUS); let mut compressed = (fe as u32) << (COEFFICIENT_BITS + 1); compressed += FIELD_MODULUS as u32; @@ -28,7 +28,7 @@ pub(super) fn decompress_q( fe: KyberFieldElement, ) -> KyberFieldElement { debug_assert!(COEFFICIENT_BITS <= 11); - debug_assert!(0 <= fe && fe < (1 << 11)); + debug_assert!(0 <= fe && fe < (1 << COEFFICIENT_BITS)); let mut decompressed = (fe as u32) * (FIELD_MODULUS as u32); decompressed = (decompressed << 1) + (1 << COEFFICIENT_BITS); From 7aabdecb11d2712d35f673322a0d32c181c58dec Mon Sep 17 00:00:00 2001 From: xvzcf Date: Fri, 27 Oct 2023 10:10:32 -0400 Subject: [PATCH 3/5] Deduplicated ntt_at_layer macro. --- .../extraction/Libcrux.Kem.Kyber.Ntt.fst | 434 ++++++++++++++---- src/kem/kyber/ntt.rs | 95 ++-- 2 files changed, 378 insertions(+), 151 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst index 7b53acd0b..57b3538cc 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst @@ -24,7 +24,7 @@ let v_ZETAS_MONTGOMERY_DOMAIN: t_Array i32 (sz 128) = let ntt_binomially_sampled_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - let coefficient_bound:i32 = 3l in + let initial_coefficient_bound:i32 = 3l in let _:Prims.unit = if true then @@ -34,12 +34,12 @@ let ntt_binomially_sampled_ring_element <: Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> - (Core.Num.impl__i32__abs coefficient <: i32) <=. coefficient_bound <: bool) + (Core.Num.impl__i32__abs coefficient <: i32) <=. initial_coefficient_bound <: bool) in let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n coefficient.abs() <= coefficient_bound)" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n coefficient.abs() <= initial_coefficient_bound)" <: Rust_primitives.Hax.t_Never) @@ -47,7 +47,6 @@ let ntt_binomially_sampled_ring_element () in let zeta_i:usize = sz 0 in - let layer_number:i32 = 0l in let re, zeta_i:(Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement & usize) = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_step_by ({ @@ -86,7 +85,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -97,11 +95,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! - (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) - <: - i32) + (initial_coefficient_bound +! + (3l *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) <: i32) <: @@ -110,22 +105,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound + (3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 64 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -152,7 +148,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 64 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -162,7 +158,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -173,8 +168,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 6l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -186,22 +181,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 6) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 32 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -228,7 +224,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 32 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -238,7 +234,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -249,8 +244,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 5l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -262,22 +257,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 5) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 16 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -304,7 +300,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 16 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -314,7 +310,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -325,8 +320,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 4l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -338,22 +333,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 4) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 8 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -380,7 +376,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 8 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -390,7 +386,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -401,8 +396,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 3l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -414,22 +409,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 3) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 4 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -456,7 +452,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 4 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -466,7 +462,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -477,8 +472,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 2l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -490,22 +485,23 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 2) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) in () in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 2 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -532,7 +528,7 @@ let ntt_binomially_sampled_ring_element in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 2 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -542,7 +538,6 @@ let ntt_binomially_sampled_ring_element in re, zeta_i) in - let layer_number:i32 = layer_number +! 1l in let _:Prims.unit = if true then @@ -553,8 +548,8 @@ let ntt_binomially_sampled_ring_element Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (Core.Num.impl__i32__abs coefficient <: i32) <. - (coefficient_bound +! - ((layer_number *! 3l <: i32) *! + (initial_coefficient_bound +! + (((8l -! 1l <: i32) *! 3l <: i32) *! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) <: i32) @@ -566,7 +561,7 @@ let ntt_binomially_sampled_ring_element let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2))\\n })" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 1) * 3 * (FIELD_MODULUS / 2))\\n })" <: Rust_primitives.Hax.t_Never) @@ -588,16 +583,39 @@ let ntt_vector_u (#v_VECTOR_U_COMPRESSION_FACTOR: usize) (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + let initial_coefficient_bound:i32 = 3329l in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <=. initial_coefficient_bound <: bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n coefficient.abs() <= initial_coefficient_bound)" + + <: + Rust_primitives.Hax.t_Never) + in + () + in let zeta_i:usize = sz 0 in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 128 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -624,7 +642,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 128 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -634,15 +652,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 7l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 7) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 64 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -669,7 +718,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 64 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -679,15 +728,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 6l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 6) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 32 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -714,7 +794,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 32 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -724,15 +804,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 5l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 5) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 16 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -759,7 +870,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 16 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -769,15 +880,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 4l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 4) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 8 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -804,7 +946,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 8 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -814,15 +956,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 3l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 3) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 4 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -849,7 +1022,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 4 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -859,15 +1032,46 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 2l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 2) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in + let layer_jump:usize = sz 1 < let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! sz 2 <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -894,7 +1098,7 @@ let ntt_vector_u in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = Rust_primitives.Hax.update_at re - (j +! sz 2 <: usize) + (j +! layer_jump <: usize) ((re.[ j ] <: i32) -! t <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -904,6 +1108,36 @@ let ntt_vector_u in re, zeta_i) in + let _:Prims.unit = + if true + then + let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = + Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + <: + Core.Array.Iter.t_IntoIter i32 (sz 256)) + (fun coefficient -> + (Core.Num.impl__i32__abs coefficient <: i32) <. + (initial_coefficient_bound +! + (((8l -! 1l <: i32) *! 3l <: i32) *! + (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS /! 2l <: i32) + <: + i32) + <: + i32) + <: + bool) + in + let _:Prims.unit = + if ~.out + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: re.coefficients.into_iter().all(|coefficient|\\n {\\n coefficient.abs() <\\n initial_coefficient_bound +\\n ((8 - 1) * 3 * (FIELD_MODULUS / 2))\\n })" + + <: + Rust_primitives.Hax.t_Never) + in + () + in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = { re with diff --git a/src/kem/kyber/ntt.rs b/src/kem/kyber/ntt.rs index c40f35424..ce7bbc688 100644 --- a/src/kem/kyber/ntt.rs +++ b/src/kem/kyber/ntt.rs @@ -16,6 +16,26 @@ const ZETAS_MONTGOMERY_DOMAIN: [KyberFieldElement; 128] = [ -1530, -1278, 794, -1510, -854, -870, 478, -108, -308, 996, 991, 958, -1460, 1522, 1628, ]; +macro_rules! ntt_at_layer { + ($layer:literal, $zeta_i:ident, $re:ident, $initial_coefficient_bound:ident) => { + let layer_jump = 1 << $layer; + for offset in (0..(COEFFICIENTS_IN_RING_ELEMENT - layer_jump)).step_by(2 * layer_jump) { + $zeta_i += 1; + + for j in offset..offset + layer_jump { + let t = montgomery_reduce($re[j + layer_jump] * ZETAS_MONTGOMERY_DOMAIN[$zeta_i]); + $re[j + layer_jump] = $re[j] - t; + $re[j] = $re[j] + t; + } + } + + debug_assert!($re.coefficients.into_iter().all(|coefficient| { + coefficient.abs() + < $initial_coefficient_bound + ((8 - $layer) * 3 * (FIELD_MODULUS / 2)) + })); + }; +} + // Over time, all invocations of ntt_representation() will be replaced by // invocations to this function, upon which this function will be renamed back to // ntt_representation(). @@ -23,14 +43,13 @@ const ZETAS_MONTGOMERY_DOMAIN: [KyberFieldElement; 128] = [ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { - let coefficient_bound = 3; + let initial_coefficient_bound = 3; debug_assert!(re .coefficients .into_iter() - .all(|coefficient| coefficient.abs() <= coefficient_bound)); + .all(|coefficient| coefficient.abs() <= initial_coefficient_bound)); let mut zeta_i = 0; - let mut layer_number = 0; // This function is only being used in key-generation for the moment, and we // can skip the first round of montgomery reductions for the ring elements @@ -46,36 +65,16 @@ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( re[j] = re[j] + t; } } - layer_number += 1; debug_assert!(re.coefficients.into_iter().all(|coefficient| { - coefficient.abs() < coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2)) + coefficient.abs() < initial_coefficient_bound + (3 * (FIELD_MODULUS / 2)) })); - macro_rules! ntt_at_layer { - ($layer:literal) => { - for offset in (0..(COEFFICIENTS_IN_RING_ELEMENT - $layer)).step_by(2 * $layer) { - zeta_i += 1; - - for j in offset..offset + $layer { - let t = montgomery_reduce(re[j + $layer] * ZETAS_MONTGOMERY_DOMAIN[zeta_i]); - re[j + $layer] = re[j] - t; - re[j] = re[j] + t; - } - } - - layer_number += 1; - debug_assert!(re.coefficients.into_iter().all(|coefficient| { - coefficient.abs() < coefficient_bound + (layer_number * 3 * (FIELD_MODULUS / 2)) - })); - }; - } - - ntt_at_layer!(64); - ntt_at_layer!(32); - ntt_at_layer!(16); - ntt_at_layer!(8); - ntt_at_layer!(4); - ntt_at_layer!(2); + ntt_at_layer!(6, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(5, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(4, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(3, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(2, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(1, zeta_i, re, initial_coefficient_bound); re.coefficients = re.coefficients.map(barrett_reduce); @@ -86,29 +85,23 @@ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( pub(in crate::kem::kyber) fn ntt_vector_u( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { - let mut zeta_i = 0; - - macro_rules! ntt_at_layer { - ($layer:literal) => { - for offset in (0..(COEFFICIENTS_IN_RING_ELEMENT - $layer)).step_by(2 * $layer) { - zeta_i += 1; + // TODO: This could be tighter, but we have to analyze other functions + // first before we can say for sure here. + let initial_coefficient_bound = 3329; + debug_assert!(re + .coefficients + .into_iter() + .all(|coefficient| coefficient.abs() <= initial_coefficient_bound)); - for j in offset..offset + $layer { - let t = montgomery_reduce(re[j + $layer] * ZETAS_MONTGOMERY_DOMAIN[zeta_i]); - re[j + $layer] = re[j] - t; - re[j] = re[j] + t; - } - } - }; - } + let mut zeta_i = 0; - ntt_at_layer!(128); - ntt_at_layer!(64); - ntt_at_layer!(32); - ntt_at_layer!(16); - ntt_at_layer!(8); - ntt_at_layer!(4); - ntt_at_layer!(2); + ntt_at_layer!(7, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(6, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(5, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(4, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(3, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(2, zeta_i, re, initial_coefficient_bound); + ntt_at_layer!(1, zeta_i, re, initial_coefficient_bound); re.coefficients = re.coefficients.map(barrett_reduce); From 8aa11d20221453b4b7dc92b69519f0752c95eca3 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Fri, 27 Oct 2023 10:53:25 -0400 Subject: [PATCH 4/5] Removed all traits on KyberPolynomialRingElement for F-star proofs. --- hax-driver.py | 2 +- .../Libcrux.Kem.Kyber.Arithmetic.fst | 101 +-- .../extraction/Libcrux.Kem.Kyber.Ntt.fst | 706 +++++++++++++----- .../extraction/Libcrux.Kem.Kyber.Sampling.fst | 42 +- src/kem/kyber/arithmetic.rs | 58 +- src/kem/kyber/ntt.rs | 53 +- src/kem/kyber/sampling.rs | 8 +- 7 files changed, 639 insertions(+), 331 deletions(-) diff --git a/hax-driver.py b/hax-driver.py index 241d81311..1b30e17f7 100755 --- a/hax-driver.py +++ b/hax-driver.py @@ -103,7 +103,7 @@ def shell(command, expect=0, cwd=None): "hax", "into", "-i", - "-** +libcrux::kem::kyber::** -libcrux::kem::kyber::arithmetic::mutable_operations::** -libcrux::hacl::sha3::** -libcrux::digest::**", + "-** +libcrux::kem::kyber::** -libcrux::hacl::sha3::** -libcrux::digest::**", "fstar", ], cwd=".", diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst index dade74105..d5a304d6c 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst @@ -160,80 +160,29 @@ type t_KyberPolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) } let impl__KyberPolynomialRingElement__ZERO: t_KyberPolynomialRingElement = { f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) } -let impl_1: Core.Ops.Index.t_Index t_KyberPolynomialRingElement usize = - { - f_Output = i32; - f_index - = - fun (self: t_KyberPolynomialRingElement) (index: usize) -> self.f_coefficients.[ index ] - } - -let impl_2: Core.Iter.Traits.Collect.t_IntoIterator t_KyberPolynomialRingElement = - { - f_Item = i32; - f_IntoIter = Core.Array.Iter.t_IntoIter i32 (sz 256); - f_into_iter - = - fun (self: t_KyberPolynomialRingElement) -> - Core.Iter.Traits.Collect.f_into_iter self.f_coefficients - } - -let impl_3: Core.Ops.Arith.t_Add t_KyberPolynomialRingElement t_KyberPolynomialRingElement = - { - f_Output = t_KyberPolynomialRingElement; - f_add - = - fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) -> - let result:t_KyberPolynomialRingElement = impl__KyberPolynomialRingElement__ZERO in - let result:t_KyberPolynomialRingElement = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ - Core.Ops.Range.f_start = sz 0; - Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT - }) - <: - Core.Ops.Range.t_Range usize) - result - (fun result i -> - { - result with - f_coefficients - = - Rust_primitives.Hax.update_at result.f_coefficients - i - ((self.f_coefficients.[ i ] <: i32) +! (other.f_coefficients.[ i ] <: i32) <: i32) - <: - t_KyberPolynomialRingElement - }) - in - result - } - -let impl_4: Core.Ops.Arith.t_Sub t_KyberPolynomialRingElement t_KyberPolynomialRingElement = - { - f_Output = t_KyberPolynomialRingElement; - f_sub - = - fun (self: t_KyberPolynomialRingElement) (other: t_KyberPolynomialRingElement) -> - let result:t_KyberPolynomialRingElement = impl__KyberPolynomialRingElement__ZERO in - let result:t_KyberPolynomialRingElement = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ - Core.Ops.Range.f_start = sz 0; - Core.Ops.Range.f_end = Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT - }) +let add_to_ring_element (lhs rhs: t_KyberPolynomialRingElement) : t_KyberPolynomialRingElement = + let lhs:t_KyberPolynomialRingElement = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ + Core.Ops.Range.f_start = sz 0; + Core.Ops.Range.f_end + = + Core.Slice.impl__len (Rust_primitives.unsize lhs.f_coefficients <: t_Slice i32) + <: + usize + }) + <: + Core.Ops.Range.t_Range usize) + lhs + (fun lhs i -> + { + lhs with + f_coefficients + = + Rust_primitives.Hax.update_at lhs.f_coefficients + i + ((lhs.f_coefficients.[ i ] <: i32) +! (rhs.f_coefficients.[ i ] <: i32) <: i32) <: - Core.Ops.Range.t_Range usize) - result - (fun result i -> - { - result with - f_coefficients - = - Rust_primitives.Hax.update_at result.f_coefficients - i - ((self.f_coefficients.[ i ] <: i32) -! (other.f_coefficients.[ i ] <: i32) <: i32) - <: - t_KyberPolynomialRingElement - }) - in - result - } \ No newline at end of file + t_KyberPolynomialRingElement + }) + in + lhs \ No newline at end of file diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst index 57b3538cc..d5263563c 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst @@ -72,14 +72,29 @@ let ntt_binomially_sampled_ring_element Core.Ops.Range.t_Range usize) re (fun re j -> - let t:i32 = (re.[ j +! sz 128 <: usize ] <: i32) *! (-1600l) in + let t:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 128 <: usize ] <: i32) *! + (-1600l) + in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 128 <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 128 <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -139,7 +154,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -147,12 +164,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -215,7 +244,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -223,12 +254,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -291,7 +334,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -299,12 +344,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -367,7 +424,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -375,12 +434,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -443,7 +514,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -451,12 +524,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -519,7 +604,9 @@ let ntt_binomially_sampled_ring_element re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -527,12 +614,24 @@ let ntt_binomially_sampled_ring_element i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -633,7 +732,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -641,12 +742,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -709,7 +822,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -717,12 +832,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -785,7 +912,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -793,12 +922,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -861,7 +1002,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -869,12 +1012,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -937,7 +1092,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -945,12 +1102,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -1013,7 +1182,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -1021,12 +1192,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -1089,7 +1272,9 @@ let ntt_vector_u re (fun re j -> let t:i32 = - Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re.[ j +! layer_jump <: usize ] + Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce ((re + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! layer_jump <: usize + ] <: i32) *! (v_ZETAS_MONTGOMERY_DOMAIN.[ zeta_i ] <: i32) @@ -1097,12 +1282,24 @@ let ntt_vector_u i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! layer_jump <: usize) - ((re.[ j ] <: i32) -! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! layer_jump <: usize) + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) -! t <: i32) + } in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re j ((re.[ j ] <: i32) +! t <: i32) + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! t <: i32) + } in re) in @@ -1179,20 +1376,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 2 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 2 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 2 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 2 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 2 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 2 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1225,20 +1440,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 4 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 4 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 4 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 4 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 4 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 4 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1271,20 +1504,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 8 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 8 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 8 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 8 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 8 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 8 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1317,20 +1568,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 16 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 16 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 16 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 16 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 16 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 16 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1363,20 +1632,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 32 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 32 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 32 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 32 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 32 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 32 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1409,20 +1696,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 64 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 64 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 64 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 64 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 64 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 64 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1455,20 +1760,38 @@ let invert_ntt_montgomery (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRin Core.Ops.Range.t_Range usize) re (fun re j -> - let a_minus_b:i32 = (re.[ j +! sz 128 <: usize ] <: i32) -! (re.[ j ] <: i32) in - let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - j - ((re.[ j ] <: i32) +! (re.[ j +! sz 128 <: usize ] <: i32) <: i32) + let a_minus_b:i32 = + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 128 <: usize ] <: i32) -! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) in let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at re - (j +! sz 128 <: usize) - (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + j + ((re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j ] <: i32) +! + (re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ j +! sz 128 <: usize ] <: i32) - <: - i32) + <: + i32) + } + in + let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + { + re with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at re.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (j +! sz 128 <: usize) + (Libcrux.Kem.Kyber.Arithmetic.montgomery_reduce (a_minus_b *! zeta_i_value + <: + i32) + <: + i32) + } in re) in @@ -1490,6 +1813,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing then let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter left + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients <: Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> (coefficient >=. 0l <: bool) && (coefficient <. 4096l <: bool)) @@ -1497,7 +1821,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: left.into_iter().all(|coefficient| coefficient >= 0 && coefficient < 4096)" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: left.coefficients.into_iter().all(|coefficient|\\n coefficient >= 0 && coefficient < 4096)" <: Rust_primitives.Hax.t_Never) @@ -1509,6 +1833,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing then let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter right + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients <: Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> @@ -1521,7 +1846,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: right.into_iter().all(|coefficient|\\n coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: right.coefficients.into_iter().all(|coefficient|\\n coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)" <: Rust_primitives.Hax.t_Never) @@ -1545,20 +1870,41 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing out (fun out i -> let product:(i32 & i32) = - ntt_multiply_binomials ((left.[ i ] <: i32), (left.[ i +! sz 1 <: usize ] <: i32)) - ((right.[ i ] <: i32), (right.[ i +! sz 1 <: usize ] <: i32)) + ntt_multiply_binomials ((left.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] <: i32), + (left.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 1 <: usize ] <: i32)) + ((right.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i ] <: i32), + (right.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 1 <: usize ] <: i32)) (v_ZETAS_MONTGOMERY_DOMAIN.[ sz 64 +! (i /! sz 4 <: usize) <: usize ] <: i32) in let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out i product._1 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + i + product._1 + } in let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out (i +! sz 1 <: usize) product._2 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (i +! sz 1 <: usize) + product._2 + } in let product:(i32 & i32) = - ntt_multiply_binomials ((left.[ i +! sz 2 <: usize ] <: i32), - (left.[ i +! sz 3 <: usize ] <: i32)) - ((right.[ i +! sz 2 <: usize ] <: i32), (right.[ i +! sz 3 <: usize ] <: i32)) + ntt_multiply_binomials ((left.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 2 + <: + usize ] + <: + i32), + (left.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 3 <: usize ] <: i32)) + ((right.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 2 <: usize ] <: i32), + (right.Libcrux.Kem.Kyber.Arithmetic.f_coefficients.[ i +! sz 3 <: usize ] <: i32)) (Core.Ops.Arith.Neg.neg (v_ZETAS_MONTGOMERY_DOMAIN.[ sz 64 +! (i /! sz 4 <: usize) <: usize ] @@ -1568,10 +1914,24 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing i32) in let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out (i +! sz 2 <: usize) product._1 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (i +! sz 2 <: usize) + product._1 + } in let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out (i +! sz 3 <: usize) product._2 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + (i +! sz 3 <: usize) + product._2 + } in out) in @@ -1580,6 +1940,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing then let _, out:(Core.Array.Iter.t_IntoIter i32 (sz 256) & bool) = Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter out + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients <: Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> @@ -1592,7 +1953,7 @@ let ntt_multiply (left right: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRing let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: out.into_iter().all(|coefficient|\\n coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: out.coefficients.into_iter().all(|coefficient|\\n coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)" <: Rust_primitives.Hax.t_Never) @@ -1632,12 +1993,13 @@ let compute_message (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) result (fun result (secret_element, u_element) -> - result +! - (ntt_multiply secret_element u_element - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + let product:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + ntt_multiply secret_element u_element + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Libcrux.Kem.Kyber.Arithmetic.add_to_ring_element result product + in + result) in let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = { @@ -1728,12 +2090,13 @@ let compute_ring_element_v (Core.Slice.Iter.t_Iter Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)) result (fun result (tt_element, r_element) -> - result +! - (ntt_multiply tt_element r_element - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - <: - Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + let product:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + ntt_multiply tt_element r_element + in + let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = + Libcrux.Kem.Kyber.Arithmetic.add_to_ring_element result product + in + result) in let result:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = invert_ntt_montgomery result @@ -1837,8 +2200,10 @@ let compute_vector_u let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.update_at result i - ((result.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +! - product + (Libcrux.Kem.Kyber.Arithmetic.add_to_ring_element (result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + product <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) in @@ -1964,8 +2329,10 @@ let compute_As_plus_e let result:t_Array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Rust_primitives.Hax.update_at result i - ((result.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) +! - product + (Libcrux.Kem.Kyber.Arithmetic.add_to_ring_element (result.[ i ] + <: + Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + product <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) in @@ -1978,6 +2345,7 @@ let compute_As_plus_e Core.Iter.Traits.Iterator.f_all (Core.Iter.Traits.Collect.f_into_iter (result.[ i ] <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients <: Core.Array.Iter.t_IntoIter i32 (sz 256)) (fun coefficient -> @@ -1989,7 +2357,7 @@ let compute_As_plus_e let _:Prims.unit = if ~.out then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: result[i].into_iter().all(|coefficient|\\n coefficient.abs() < (K as i32) * FIELD_MODULUS)" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: result[i].coefficients.into_iter().all(|coefficient|\\n coefficient.abs() < (K as i32) * FIELD_MODULUS)" <: Rust_primitives.Hax.t_Never) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst index 531d987aa..5b8736622 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst @@ -33,7 +33,14 @@ let sample_from_uniform_distribution (#v_SEED_SIZE: usize) (randomness: t_Array sampled_coefficients <. Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT then let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out sampled_coefficients d1 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + sampled_coefficients + d1 + } in out, sampled_coefficients +! sz 1 else out, sampled_coefficients @@ -45,7 +52,14 @@ let sample_from_uniform_distribution (#v_SEED_SIZE: usize) (randomness: t_Array sampled_coefficients <. Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT then let out:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at out sampled_coefficients d2 + { + out with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at out.Libcrux.Kem.Kyber.Arithmetic.f_coefficients + sampled_coefficients + d2 + } in let sampled_coefficients:usize = sampled_coefficients +! sz 1 in out, sampled_coefficients @@ -131,9 +145,15 @@ let sample_from_binomial_distribution_2_ (randomness: t_Slice u8) in let offset:usize = cast (outcome_set >>! 2l) <: usize in let sampled:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at sampled - ((sz 8 *! chunk_number <: usize) +! offset <: usize) - (outcome_1_ -! outcome_2_ <: i32) + { + sampled with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at sampled + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + ((sz 8 *! chunk_number <: usize) +! offset <: usize) + (outcome_1_ -! outcome_2_ <: i32) + } in sampled)) in @@ -202,9 +222,15 @@ let sample_from_binomial_distribution_3_ (randomness: t_Slice u8) in let offset:usize = cast (outcome_set /! 6l) <: usize in let sampled:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - Rust_primitives.Hax.update_at sampled - ((sz 4 *! chunk_number <: usize) +! offset <: usize) - (outcome_1_ -! outcome_2_ <: i32) + { + sampled with + Libcrux.Kem.Kyber.Arithmetic.f_coefficients + = + Rust_primitives.Hax.update_at sampled + .Libcrux.Kem.Kyber.Arithmetic.f_coefficients + ((sz 4 *! chunk_number <: usize) +! offset <: usize) + (outcome_1_ -! outcome_2_ <: i32) + } in sampled)) in diff --git a/src/kem/kyber/arithmetic.rs b/src/kem/kyber/arithmetic.rs index a554c4f22..fb23995a4 100644 --- a/src/kem/kyber/arithmetic.rs +++ b/src/kem/kyber/arithmetic.rs @@ -1,5 +1,3 @@ -use std::ops::{self, Index, IndexMut}; - use super::constants::{COEFFICIENTS_IN_RING_ELEMENT, FIELD_MODULUS}; pub(crate) type KyberFieldElement = i32; @@ -53,55 +51,13 @@ impl KyberPolynomialRingElement { }; } -// Adding this to a module to ignore it for extraction. -mod mutable_operations { - use super::*; - - impl IndexMut for KyberPolynomialRingElement { - fn index_mut(&mut self, index: usize) -> &mut Self::Output { - &mut self.coefficients[index] - } - } -} - -impl Index for KyberPolynomialRingElement { - type Output = KyberFieldElement; - - fn index(&self, index: usize) -> &Self::Output { - &self.coefficients[index] - } -} - -impl IntoIterator for KyberPolynomialRingElement { - type Item = KyberFieldElement; - - type IntoIter = std::array::IntoIter; - - fn into_iter(self) -> Self::IntoIter { - self.coefficients.into_iter() +pub(crate) fn add_to_ring_element( + mut lhs: KyberPolynomialRingElement, + rhs: &KyberPolynomialRingElement, +) -> KyberPolynomialRingElement { + for i in 0..lhs.coefficients.len() { + lhs.coefficients[i] += rhs.coefficients[i]; } -} -impl ops::Add for KyberPolynomialRingElement { - type Output = Self; - - fn add(self, other: Self) -> Self { - let mut result = KyberPolynomialRingElement::ZERO; - for i in 0..COEFFICIENTS_IN_RING_ELEMENT { - result.coefficients[i] = self.coefficients[i] + other.coefficients[i]; - } - result - } -} - -impl ops::Sub for KyberPolynomialRingElement { - type Output = Self; - - fn sub(self, other: Self) -> Self { - let mut result = KyberPolynomialRingElement::ZERO; - for i in 0..COEFFICIENTS_IN_RING_ELEMENT { - result.coefficients[i] = self.coefficients[i] - other.coefficients[i]; - } - result - } + lhs } diff --git a/src/kem/kyber/ntt.rs b/src/kem/kyber/ntt.rs index ce7bbc688..8e25bc49c 100644 --- a/src/kem/kyber/ntt.rs +++ b/src/kem/kyber/ntt.rs @@ -1,6 +1,7 @@ use super::{ arithmetic::{ - barrett_reduce, montgomery_reduce, KyberFieldElement, KyberPolynomialRingElement, + add_to_ring_element, barrett_reduce, montgomery_reduce, KyberFieldElement, + KyberPolynomialRingElement, }, constants::{COEFFICIENTS_IN_RING_ELEMENT, FIELD_MODULUS}, }; @@ -23,9 +24,11 @@ macro_rules! ntt_at_layer { $zeta_i += 1; for j in offset..offset + layer_jump { - let t = montgomery_reduce($re[j + layer_jump] * ZETAS_MONTGOMERY_DOMAIN[$zeta_i]); - $re[j + layer_jump] = $re[j] - t; - $re[j] = $re[j] + t; + let t = montgomery_reduce( + $re.coefficients[j + layer_jump] * ZETAS_MONTGOMERY_DOMAIN[$zeta_i], + ); + $re.coefficients[j + layer_jump] = $re.coefficients[j] - t; + $re.coefficients[j] = $re.coefficients[j] + t; } } @@ -59,10 +62,10 @@ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( for j in offset..offset + 128 { // Multiply by the appropriate zeta in the normal domain. - let t = re[j + 128] * -1600; + let t = re.coefficients[j + 128] * -1600; - re[j + 128] = re[j] - t; - re[j] = re[j] + t; + re.coefficients[j + 128] = re.coefficients[j] - t; + re.coefficients[j] = re.coefficients[j] + t; } } debug_assert!(re.coefficients.into_iter().all(|coefficient| { @@ -120,12 +123,12 @@ fn invert_ntt_montgomery(mut re: KyberPolynomialRingElement) -> KyberPolynomialR let end = offset + $layer; for j in offset..end { - let a_minus_b = re[j + $layer] - re[j]; + let a_minus_b = re.coefficients[j + $layer] - re.coefficients[j]; // Instead of dividing by 2 here, we just divide by // 2^7 in one go in the end. - re[j] = re[j] + re[j + $layer]; - re[j + $layer] = montgomery_reduce(a_minus_b * zeta_i_value); + re.coefficients[j] = re.coefficients[j] + re.coefficients[j + $layer]; + re.coefficients[j + $layer] = montgomery_reduce(a_minus_b * zeta_i_value); } } }; @@ -160,9 +163,11 @@ fn ntt_multiply( right: &KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { debug_assert!(left + .coefficients .into_iter() .all(|coefficient| coefficient >= 0 && coefficient < 4096)); debug_assert!(right + .coefficients .into_iter() .all(|coefficient| coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)); @@ -170,23 +175,24 @@ fn ntt_multiply( for i in (0..COEFFICIENTS_IN_RING_ELEMENT).step_by(4) { let product = ntt_multiply_binomials( - (left[i], left[i + 1]), - (right[i], right[i + 1]), + (left.coefficients[i], left.coefficients[i + 1]), + (right.coefficients[i], right.coefficients[i + 1]), ZETAS_MONTGOMERY_DOMAIN[64 + (i / 4)], ); - out[i] = product.0; - out[i + 1] = product.1; + out.coefficients[i] = product.0; + out.coefficients[i + 1] = product.1; let product = ntt_multiply_binomials( - (left[i + 2], left[i + 3]), - (right[i + 2], right[i + 3]), + (left.coefficients[i + 2], left.coefficients[i + 3]), + (right.coefficients[i + 2], right.coefficients[i + 3]), -ZETAS_MONTGOMERY_DOMAIN[64 + (i / 4)], ); - out[i + 2] = product.0; - out[i + 3] = product.1; + out.coefficients[i + 2] = product.0; + out.coefficients[i + 3] = product.1; } debug_assert!(out + .coefficients .into_iter() .all(|coefficient| coefficient > -FIELD_MODULUS && coefficient < FIELD_MODULUS)); @@ -203,7 +209,8 @@ pub(in crate::kem::kyber) fn compute_message( let mut result = KyberPolynomialRingElement::ZERO; for (secret_element, u_element) in secret_as_ntt.iter().zip(u_as_ntt.iter()) { - result = result + ntt_multiply(secret_element, u_element); + let product = ntt_multiply(secret_element, u_element); + result = add_to_ring_element(result, &product); } // TODO: Without this, there's a failure in Kyber-1024. We need to see if // this round of barrett reductions can be removed. @@ -230,7 +237,8 @@ pub(in crate::kem::kyber) fn compute_ring_element_v( let mut result = KyberPolynomialRingElement::ZERO; for (t_element, r_element) in t_as_ntt.iter().zip(r_as_ntt.iter()) { - result = result + ntt_multiply(t_element, r_element); + let product = ntt_multiply(t_element, r_element); + result = add_to_ring_element(result, &product); } result = invert_ntt_montgomery(result); @@ -256,7 +264,7 @@ pub(in crate::kem::kyber) fn compute_vector_u( for (i, row) in a_as_ntt.iter().enumerate() { for (j, a_element) in row.iter().enumerate() { let product = ntt_multiply(a_element, &r_as_ntt[j]); - result[i] = result[i] + product; + result[i] = add_to_ring_element(result[i], &product); } result[i] = invert_ntt_montgomery(result[i]); @@ -288,10 +296,11 @@ pub(in crate::kem::kyber) fn compute_As_plus_e( for (i, row) in matrix_A.iter().enumerate() { for (j, matrix_element) in row.iter().enumerate() { let product = ntt_multiply(matrix_element, &s_as_ntt[j]); - result[i] = result[i] + product; + result[i] = add_to_ring_element(result[i], &product); } debug_assert!(result[i] + .coefficients .into_iter() .all(|coefficient| coefficient.abs() < (K as i32) * FIELD_MODULUS)); diff --git a/src/kem/kyber/sampling.rs b/src/kem/kyber/sampling.rs index 9a64a39b6..b211ae7be 100644 --- a/src/kem/kyber/sampling.rs +++ b/src/kem/kyber/sampling.rs @@ -22,11 +22,11 @@ pub fn sample_from_uniform_distribution( let d2 = (b3 << 4) | (b2 >> 4); if d1 < FIELD_MODULUS && sampled_coefficients < COEFFICIENTS_IN_RING_ELEMENT { - out[sampled_coefficients] = d1; + out.coefficients[sampled_coefficients] = d1; sampled_coefficients += 1 } if d2 < FIELD_MODULUS && sampled_coefficients < COEFFICIENTS_IN_RING_ELEMENT { - out[sampled_coefficients] = d2; + out.coefficients[sampled_coefficients] = d2; sampled_coefficients += 1; } if sampled_coefficients == COEFFICIENTS_IN_RING_ELEMENT { @@ -94,7 +94,7 @@ fn sample_from_binomial_distribution_2(randomness: &[u8]) -> KyberPolynomialRing let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 2)) & 0x3) as KyberFieldElement; let offset = (outcome_set >> 2) as usize; - sampled[8 * chunk_number + offset] = outcome_1 - outcome_2; + sampled.coefficients[8 * chunk_number + offset] = outcome_1 - outcome_2; } } @@ -123,7 +123,7 @@ fn sample_from_binomial_distribution_3(randomness: &[u8]) -> KyberPolynomialRing let outcome_2 = ((coin_toss_outcomes >> (outcome_set + 3)) & 0x7) as KyberFieldElement; let offset = (outcome_set / 6) as usize; - sampled[4 * chunk_number + offset] = outcome_1 - outcome_2; + sampled.coefficients[4 * chunk_number + offset] = outcome_1 - outcome_2; } } From 9287a200909052204968f34cf9fc2a0d1ad8d935 Mon Sep 17 00:00:00 2001 From: xvzcf Date: Fri, 27 Oct 2023 13:42:05 -0400 Subject: [PATCH 5/5] Removed one TODO in NTT. --- .../extraction/Libcrux.Kem.Kyber.Compress.fst | 22 +++++++++++++++++++ .../extraction/Libcrux.Kem.Kyber.Ntt.fst | 2 +- src/kem/kyber/compress.rs | 2 ++ src/kem/kyber/ntt.rs | 4 +--- 4 files changed, 26 insertions(+), 4 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst index af919c9b7..53496600d 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst @@ -87,6 +87,28 @@ let decompress_q (#v_COEFFICIENT_BITS: usize) (fe: i32) : i32 = in let decompressed:u32 = (decompressed <>! (v_COEFFICIENT_BITS +! sz 1 <: usize) in + let _:Prims.unit = + if true + then + let _:Prims.unit = + if + ~.(decompressed <. + (Core.Result.impl__unwrap (Core.Convert.f_try_from Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS + + <: + Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError) + <: + u32) + <: + bool) + then + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: decompressed < u32::try_from(FIELD_MODULUS).unwrap()" + + <: + Rust_primitives.Hax.t_Never) + in + () + in cast decompressed <: i32 let decompress diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst index d5263563c..8bc09cb4c 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst @@ -682,7 +682,7 @@ let ntt_vector_u (#v_VECTOR_U_COMPRESSION_FACTOR: usize) (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = - let initial_coefficient_bound:i32 = 3329l in + let initial_coefficient_bound:i32 = 3328l in let _:Prims.unit = if true then diff --git a/src/kem/kyber/compress.rs b/src/kem/kyber/compress.rs index 34944eb66..a234d48f6 100644 --- a/src/kem/kyber/compress.rs +++ b/src/kem/kyber/compress.rs @@ -34,6 +34,8 @@ pub(super) fn decompress_q( decompressed = (decompressed << 1) + (1 << COEFFICIENT_BITS); decompressed >>= COEFFICIENT_BITS + 1; + debug_assert!(decompressed < u32::try_from(FIELD_MODULUS).unwrap()); + decompressed as KyberFieldElement } pub fn decompress( diff --git a/src/kem/kyber/ntt.rs b/src/kem/kyber/ntt.rs index 8e25bc49c..340db5479 100644 --- a/src/kem/kyber/ntt.rs +++ b/src/kem/kyber/ntt.rs @@ -88,9 +88,7 @@ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element( pub(in crate::kem::kyber) fn ntt_vector_u( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { - // TODO: This could be tighter, but we have to analyze other functions - // first before we can say for sure here. - let initial_coefficient_bound = 3329; + let initial_coefficient_bound = 3328; debug_assert!(re .coefficients .into_iter()