From 2befd455eb287b83a56cb69a1fb940c979b0f385 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Sun, 28 Apr 2024 20:33:37 +0200 Subject: [PATCH] update F* and drop sha3 changes --- .../extraction/Libcrux_ml_kem.Arithmetic.fsti | 57 +++++++++++ .../extraction/Libcrux_ml_kem.Compress.fsti | 15 +++ .../Libcrux_ml_kem.Constant_time_ops.fsti | 5 + .../extraction/Libcrux_ml_kem.Constants.fsti | 6 ++ .../Libcrux_ml_kem.Hash_functions.fsti | 2 + .../extraction/Libcrux_ml_kem.Ind_cpa.fsti | 96 +++++++++++++++++++ .../extraction/Libcrux_ml_kem.Kyber1024.fsti | 5 + .../extraction/Libcrux_ml_kem.Kyber512.fsti | 5 + .../extraction/Libcrux_ml_kem.Kyber768.fsti | 5 + .../extraction/Libcrux_ml_kem.Matrix.fsti | 7 ++ .../fstar/extraction/Libcrux_ml_kem.Ntt.fsti | 12 +++ .../extraction/Libcrux_ml_kem.Polynomial.fsti | 25 +++++ .../extraction/Libcrux_ml_kem.Sampling.fsti | 71 ++++++++++++++ .../extraction/Libcrux_ml_kem.Serialize.fst | 8 +- .../extraction/Libcrux_ml_kem.Serialize.fsti | 5 + .../Libcrux_ml_kem.Simd.Portable.fst | 8 +- .../Libcrux_ml_kem.Simd.Portable.fsti | 14 ++- .../Libcrux_ml_kem.Simd.Simd_trait.fsti | 52 +++++----- .../extraction/Libcrux_ml_kem.Types.fsti | 2 + .../fstar/extraction/Libcrux_ml_kem.fsti | 5 + sys/hacl/c/src/Hacl_Hash_SHA3_Scalar.c | 23 +++-- 21 files changed, 384 insertions(+), 44 deletions(-) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Arithmetic.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Arithmetic.fsti index 0a56d6dc0..299350482 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Arithmetic.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Arithmetic.fsti @@ -3,15 +3,24 @@ module Libcrux_ml_kem.Arithmetic open Core open FStar.Mul +/// Values having this type hold a representative 'x' of the Kyber field. +/// We use 'fe' as a shorthand for this type. unfold let t_FieldElement = i32 +/// If 'x' denotes a value of type `fe`, values having this type hold a +/// representative y ≡ x·MONTGOMERY_R (mod FIELD_MODULUS). +/// We use 'fer' as a shorthand for this type. unfold let t_FieldElementTimesMontgomeryR = i32 +/// If 'x' denotes a value of type `fe`, values having this type hold a +/// representative y ≡ x·MONTGOMERY_R^(-1) (mod FIELD_MODULUS). +/// We use 'mfe' as a shorthand for this type unfold let t_MontgomeryFieldElement = i32 +/// This is calculated as ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋ let v_BARRETT_MULTIPLIER: i64 = 20159L let v_BARRETT_SHIFT: i64 = 26L @@ -20,6 +29,7 @@ let v_BARRETT_R: i64 = 1L <=. 0us && result <. (cast (Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i32) <: u16)) +/// Signed Barrett Reduction +/// Given an input `value`, `barrett_reduce` outputs a representative `result` +/// such that: +/// - result ≡ value (mod FIELD_MODULUS) +/// - the absolute value of `result` is bound as follows: +/// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1) +/// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`. val barrett_reduce (value: i32) : Prims.Pure i32 (requires @@ -56,6 +77,13 @@ val barrett_reduce (value: i32) result >. (Core.Ops.Arith.Neg.neg Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i32) && result <. Libcrux_ml_kem.Constants.v_FIELD_MODULUS) +/// Signed Montgomery Reduction +/// Given an input `value`, `montgomery_reduce` outputs a representative `o` +/// such that: +/// - o ≡ value · MONTGOMERY_R^(-1) (mod FIELD_MODULUS) +/// - the absolute value of `o` is bound as follows: +/// `|result| ≤ (|value| / MONTGOMERY_R) + (FIELD_MODULUS / 2) +/// In particular, if `|value| ≤ FIELD_MODULUS * MONTGOMERY_R`, then `|o| < (3 · FIELD_MODULUS) / 2`. val montgomery_reduce (value: i32) : Prims.Pure i32 (requires @@ -74,10 +102,39 @@ val montgomery_reduce (value: i32) i32) && result <=. ((3l *! Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i32) /! 2l <: i32)) +/// If x is some field element of the Kyber field and `mfe` is congruent to +/// x · MONTGOMERY_R^{-1}, this procedure outputs a value that is congruent to +/// `x`, as follows: +/// mfe · MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS ≡ x · MONTGOMERY_R^{-1} * (MONTGOMERY_R)^2 (mod FIELD_MODULUS) +/// => mfe · MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS ≡ x · MONTGOMERY_R (mod FIELD_MODULUS) +/// `montgomery_reduce` takes the value `x · MONTGOMERY_R` and outputs a representative +/// `x · MONTGOMERY_R * MONTGOMERY_R^{-1} ≡ x (mod FIELD_MODULUS)` val v__to_standard_domain (mfe: i32) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) +/// If `fe` is some field element 'x' of the Kyber field and `fer` is congruent to +/// `y · MONTGOMERY_R`, this procedure outputs a value that is congruent to +/// `x · y`, as follows: +/// `fe · fer ≡ x · y · MONTGOMERY_R (mod FIELD_MODULUS)` +/// `montgomery_reduce` takes the value `x · y · MONTGOMERY_R` and outputs a representative +/// `x · y · MONTGOMERY_R * MONTGOMERY_R^{-1} ≡ x · y (mod FIELD_MODULUS)`. val montgomery_multiply_fe_by_fer (fe fer: i32) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True) +/// Compute the product of two Kyber binomials with respect to the +/// modulus `X² - zeta`. +/// This function almost implements Algorithm 11 of the +/// NIST FIPS 203 standard, which is reproduced below: +/// ```plaintext +/// Input: a₀, a₁, b₀, b₁ ∈ ℤq. +/// Input: γ ∈ ℤq. +/// Output: c₀, c₁ ∈ ℤq. +/// c₀ ← a₀·b₀ + a₁·b₁·γ +/// c₁ ← a₀·b₁ + a₁·b₀ +/// return c₀, c₁ +/// ``` +/// We say "almost" because the coefficients output by this function are in +/// the Montgomery domain (unlike in the specification). +/// The NIST FIPS 203 standard can be found at +/// . val ntt_multiply_binomials: (i32 & i32) -> (i32 & i32) -> zeta: i32 -> Prims.Pure (i32 & i32) Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Compress.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Compress.fsti index 30e422274..ce823adbb 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Compress.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Compress.fsti @@ -15,6 +15,21 @@ val compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16) result >=. 0l && result <. (Core.Num.impl__i32__pow 2l (cast (coefficient_bits <: u8) <: u32) <: i32)) +/// The `compress_*` functions implement the `Compress` function specified in the NIST FIPS +/// 203 standard (Page 18, Expression 4.5), which is defined as: +/// ```plaintext +/// Compress_d: ℤq -> ℤ_{2ᵈ} +/// Compress_d(x) = ⌈(2ᵈ/q)·x⌋ +/// ``` +/// Since `⌈x⌋ = ⌊x + 1/2⌋` we have: +/// ```plaintext +/// Compress_d(x) = ⌊(2ᵈ/q)·x + 1/2⌋ +/// = ⌊(2^{d+1}·x + q) / 2q⌋ +/// ``` +/// For further information about the function implementations, consult the +/// `implementation_notes.pdf` document in this directory. +/// The NIST FIPS 203 standard can be found at +/// . val compress_message_coefficient (fe: u16) : Prims.Pure u8 (requires fe <. (cast (Libcrux_ml_kem.Constants.v_FIELD_MODULUS <: i32) <: u16)) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti index 42159b9af..fa256358d 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constant_time_ops.fsti @@ -3,6 +3,7 @@ module Libcrux_ml_kem.Constant_time_ops open Core open FStar.Mul +/// Return 1 if `value` is not zero and 0 otherwise. val is_non_zero (value: u8) : Prims.Pure u8 Prims.l_True @@ -18,6 +19,8 @@ val is_non_zero (value: u8) let _:Prims.unit = temp_0_ in result =. 1uy <: bool)) +/// Return 1 if the bytes of `lhs` and `rhs` do not exactly +/// match and 0 otherwise. val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8) : Prims.Pure u8 Prims.l_True @@ -33,6 +36,8 @@ val compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_ let _:Prims.unit = temp_0_ in result =. 1uy <: bool)) +/// If `selector` is not zero, return the bytes in `rhs`; return the bytes in +/// `lhs` otherwise. val select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8) : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti index 50e4d2724..1595f5594 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Constants.fsti @@ -3,18 +3,24 @@ module Libcrux_ml_kem.Constants open Core open FStar.Mul +/// Each field element needs floor(log_2(FIELD_MODULUS)) + 1 = 12 bits to represent let v_BITS_PER_COEFFICIENT: usize = sz 12 +/// Coefficients per ring element let v_COEFFICIENTS_IN_RING_ELEMENT: usize = sz 256 +/// Bits required per (uncompressed) ring element let v_BITS_PER_RING_ELEMENT: usize = v_COEFFICIENTS_IN_RING_ELEMENT *! sz 12 +/// Bytes required per (uncompressed) ring element let v_BYTES_PER_RING_ELEMENT: usize = v_BITS_PER_RING_ELEMENT /! sz 8 let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = sz 32 +/// Field modulus: 3329 let v_FIELD_MODULUS: i32 = 3329l let v_H_DIGEST_SIZE: usize = sz 32 +/// PKE message size let v_SHARED_SECRET_SIZE: usize = sz 32 diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti index 31037f7e4..78f3192cc 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Hash_functions.fsti @@ -7,6 +7,8 @@ let v_BLOCK_SIZE: usize = sz 168 let v_THREE_BLOCKS: usize = v_BLOCK_SIZE *! sz 3 +/// Free the memory of the state. +/// **NOTE:** That this needs to be done manually for now. val free_state (xof_state: Libcrux_sha3.X4.t_Shake128StateX4) : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti index b55c2e79a..a7803e891 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ind_cpa.fsti @@ -3,9 +3,11 @@ module Libcrux_ml_kem.Ind_cpa open Core open FStar.Mul +/// Pad the `slice` with `0`s at the end. val into_padded_array (v_LEN: usize) (slice: t_Slice u8) : Prims.Pure (t_Array u8 v_LEN) Prims.l_True (fun _ -> Prims.l_True) +/// Sample a vector of ring elements from a centered binomial distribution. val sample_ring_element_cbd (v_K v_ETA2_RANDOMNESS_SIZE v_ETA2: usize) (prf_input: t_Array u8 (sz 33)) @@ -15,6 +17,8 @@ val sample_ring_element_cbd Prims.l_True (fun _ -> Prims.l_True) +/// Sample a vector of ring elements from a centered binomial distribution and +/// convert them into their NTT representations. val sample_vector_cbd_then_ntt (v_K v_ETA v_ETA_RANDOMNESS_SIZE: usize) (prf_input: t_Array u8 (sz 33)) @@ -23,11 +27,14 @@ val sample_vector_cbd_then_ntt Prims.l_True (fun _ -> Prims.l_True) +/// Call [`compress_then_serialize_ring_element_u`] on each ring element. val compress_then_serialize_u (v_K v_OUT_LEN v_COMPRESSION_FACTOR v_BLOCK_LEN: usize) (input: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True) +/// Call [`deserialize_then_decompress_ring_element_u`] on each ring element +/// in the `ciphertext`. val deserialize_then_decompress_u (v_K v_CIPHERTEXT_SIZE v_U_COMPRESSION_FACTOR: usize) (ciphertext: t_Array u8 v_CIPHERTEXT_SIZE) @@ -35,6 +42,41 @@ val deserialize_then_decompress_u Prims.l_True (fun _ -> Prims.l_True) +/// This function implements Algorithm 13 of the +/// NIST FIPS 203 specification; this is the Kyber CPA-PKE encryption algorithm. +/// Algorithm 13 is reproduced below: +/// ```plaintext +/// Input: encryption key ekₚₖₑ ∈ 𝔹^{384k+32}. +/// Input: message m ∈ 𝔹^{32}. +/// Input: encryption randomness r ∈ 𝔹^{32}. +/// Output: ciphertext c ∈ 𝔹^{32(dᵤk + dᵥ)}. +/// N ← 0 +/// t̂ ← ByteDecode₁₂(ekₚₖₑ[0:384k]) +/// ρ ← ekₚₖₑ[384k: 384k + 32] +/// for (i ← 0; i < k; i++) +/// for(j ← 0; j < k; j++) +/// Â[i,j] ← SampleNTT(XOF(ρ, i, j)) +/// end for +/// end for +/// for(i ← 0; i < k; i++) +/// r[i] ← SamplePolyCBD_{η₁}(PRF_{η₁}(r,N)) +/// N ← N + 1 +/// end for +/// for(i ← 0; i < k; i++) +/// e₁[i] ← SamplePolyCBD_{η₂}(PRF_{η₂}(r,N)) +/// N ← N + 1 +/// end for +/// e₂ ← SamplePolyCBD_{η₂}(PRF_{η₂}(r,N)) +/// r̂ ← NTT(r) +/// u ← NTT-¹(Âᵀ ◦ r̂) + e₁ +/// μ ← Decompress₁(ByteDecode₁(m))) +/// v ← NTT-¹(t̂ᵀ ◦ rˆ) + e₂ + μ +/// c₁ ← ByteEncode_{dᵤ}(Compress_{dᵤ}(u)) +/// c₂ ← ByteEncode_{dᵥ}(Compress_{dᵥ}(v)) +/// return c ← (c₁ ‖ c₂) +/// ``` +/// The NIST FIPS 203 standard can be found at +/// . val encrypt (v_K v_CIPHERTEXT_SIZE v_T_AS_NTT_ENCODED_SIZE v_C1_LEN v_C2_LEN v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR v_BLOCK_LEN v_ETA1 v_ETA1_RANDOMNESS_SIZE v_ETA2 v_ETA2_RANDOMNESS_SIZE: usize) @@ -43,11 +85,30 @@ val encrypt (randomness: t_Slice u8) : Prims.Pure (t_Array u8 v_CIPHERTEXT_SIZE) Prims.l_True (fun _ -> Prims.l_True) +/// Call [`deserialize_to_uncompressed_ring_element`] for each ring element. val deserialize_secret_key (v_K: usize) (secret_key: t_Slice u8) : Prims.Pure (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) Prims.l_True (fun _ -> Prims.l_True) +/// This function implements Algorithm 14 of the +/// NIST FIPS 203 specification; this is the Kyber CPA-PKE decryption algorithm. +/// Algorithm 14 is reproduced below: +/// ```plaintext +/// Input: decryption key dkₚₖₑ ∈ 𝔹^{384k}. +/// Input: ciphertext c ∈ 𝔹^{32(dᵤk + dᵥ)}. +/// Output: message m ∈ 𝔹^{32}. +/// c₁ ← c[0 : 32dᵤk] +/// c₂ ← c[32dᵤk : 32(dᵤk + dᵥ)] +/// u ← Decompress_{dᵤ}(ByteDecode_{dᵤ}(c₁)) +/// v ← Decompress_{dᵥ}(ByteDecode_{dᵥ}(c₂)) +/// ŝ ← ByteDecode₁₂(dkₚₖₑ) +/// w ← v - NTT-¹(ŝᵀ ◦ NTT(u)) +/// m ← ByteEncode₁(Compress₁(w)) +/// return m +/// ``` +/// The NIST FIPS 203 standard can be found at +/// . val decrypt (v_K v_CIPHERTEXT_SIZE v_VECTOR_U_ENCODED_SIZE v_U_COMPRESSION_FACTOR v_V_COMPRESSION_FACTOR: usize) @@ -55,17 +116,52 @@ val decrypt (ciphertext: t_Array u8 v_CIPHERTEXT_SIZE) : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True) +/// Call [`serialize_uncompressed_ring_element`] for each ring element. val serialize_secret_key (v_K v_OUT_LEN: usize) (key: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True) +/// Concatenate `t` and `ρ` into the public key. val serialize_public_key (v_K v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize) (tt_as_ntt: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) (seed_for_a: t_Slice u8) : Prims.Pure (t_Array u8 v_PUBLIC_KEY_SIZE) Prims.l_True (fun _ -> Prims.l_True) +/// This function implements most of Algorithm 12 of the +/// NIST FIPS 203 specification; this is the Kyber CPA-PKE key generation algorithm. +/// We say "most of" since Algorithm 12 samples the required randomness within +/// the function itself, whereas this implementation expects it to be provided +/// through the `key_generation_seed` parameter. +/// Algorithm 12 is reproduced below: +/// ```plaintext +/// Output: encryption key ekₚₖₑ ∈ 𝔹^{384k+32}. +/// Output: decryption key dkₚₖₑ ∈ 𝔹^{384k}. +/// d ←$ B +/// (ρ,σ) ← G(d) +/// N ← 0 +/// for (i ← 0; i < k; i++) +/// for(j ← 0; j < k; j++) +/// Â[i,j] ← SampleNTT(XOF(ρ, i, j)) +/// end for +/// end for +/// for(i ← 0; i < k; i++) +/// s[i] ← SamplePolyCBD_{η₁}(PRF_{η₁}(σ,N)) +/// N ← N + 1 +/// end for +/// for(i ← 0; i < k; i++) +/// e[i] ← SamplePolyCBD_{η₂}(PRF_{η₂}(σ,N)) +/// N ← N + 1 +/// end for +/// ŝ ← NTT(s) +/// ê ← NTT(e) +/// t̂ ← Â◦ŝ + ê +/// ekₚₖₑ ← ByteEncode₁₂(t̂) ‖ ρ +/// dkₚₖₑ ← ByteEncode₁₂(ŝ) +/// ``` +/// The NIST FIPS 203 standard can be found at +/// . val generate_keypair (v_K v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE v_RANKED_BYTES_PER_RING_ELEMENT v_ETA1 v_ETA1_RANDOMNESS_SIZE: usize) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fsti index f3188bd69..77aa0174e 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber1024.fsti @@ -71,11 +71,13 @@ let t_MlKem1024PrivateKey = Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 3168) unfold let t_MlKem1024PublicKey = Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568) +/// Decapsulate ML-KEM 1024 val decapsulate (secret_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 3168)) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext (sz 1568)) : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True) +/// Encapsulate ML-KEM 1024 val encapsulate (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568)) (randomness: t_Array u8 (sz 32)) @@ -83,11 +85,14 @@ val encapsulate Prims.l_True (fun _ -> Prims.l_True) +/// Generate ML-KEM 1024 Key Pair val generate_key_pair (randomness: t_Array u8 (sz 64)) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 3168) (sz 1568)) Prims.l_True (fun _ -> Prims.l_True) +/// Validate a public key. +/// Returns `Some(public_key)` if valid, and `None` otherwise. val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568)) : Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1568))) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fsti index 97e233b2c..7c5f8b643 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber512.fsti @@ -71,11 +71,13 @@ let t_MlKem512PrivateKey = Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 1632) unfold let t_MlKem512PublicKey = Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800) +/// Decapsulate ML-KEM 512 val decapsulate (secret_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 1632)) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext (sz 768)) : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True) +/// Encapsulate ML-KEM 512 val encapsulate (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) (randomness: t_Array u8 (sz 32)) @@ -83,11 +85,14 @@ val encapsulate Prims.l_True (fun _ -> Prims.l_True) +/// Generate ML-KEM 512 Key Pair val generate_key_pair (randomness: t_Array u8 (sz 64)) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 1632) (sz 800)) Prims.l_True (fun _ -> Prims.l_True) +/// Validate a public key. +/// Returns `Some(public_key)` if valid, and `None` otherwise. val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800)) : Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 800))) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fsti index 92379b967..d98be2284 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Kyber768.fsti @@ -71,11 +71,13 @@ let t_MlKem768PrivateKey = Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 2400) unfold let t_MlKem768PublicKey = Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184) +/// Decapsulate ML-KEM 768 val decapsulate (secret_key: Libcrux_ml_kem.Types.t_MlKemPrivateKey (sz 2400)) (ciphertext: Libcrux_ml_kem.Types.t_MlKemCiphertext (sz 1088)) : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True) +/// Encapsulate ML-KEM 768 val encapsulate (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184)) (randomness: t_Array u8 (sz 32)) @@ -83,11 +85,14 @@ val encapsulate Prims.l_True (fun _ -> Prims.l_True) +/// Generate ML-KEM 768 Key Pair val generate_key_pair (randomness: t_Array u8 (sz 64)) : Prims.Pure (Libcrux_ml_kem.Types.t_MlKemKeyPair (sz 2400) (sz 1184)) Prims.l_True (fun _ -> Prims.l_True) +/// Validate a public key. +/// Returns `Some(public_key)` if valid, and `None` otherwise. val validate_public_key (public_key: Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184)) : Prims.Pure (Core.Option.t_Option (Libcrux_ml_kem.Types.t_MlKemPublicKey (sz 1184))) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fsti index 5f4d78550..8cdf8f256 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Matrix.fsti @@ -3,6 +3,7 @@ module Libcrux_ml_kem.Matrix open Core open FStar.Mul +/// Compute  ◦ ŝ + ê val compute_As_plus_e (v_K: usize) (matrix_A: t_Array (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) v_K) @@ -11,6 +12,7 @@ val compute_As_plus_e Prims.l_True (fun _ -> Prims.l_True) +/// Compute InverseNTT(tᵀ ◦ r̂) + e₂ + message val compute_ring_element_v (v_K: usize) (tt_as_ntt r_as_ntt: t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) @@ -19,6 +21,7 @@ val compute_ring_element_v Prims.l_True (fun _ -> Prims.l_True) +/// Compute u := InvertNTT(Aᵀ ◦ r̂) + e₁ val compute_vector_u (v_K: usize) (a_as_ntt: t_Array (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) v_K) @@ -27,6 +30,10 @@ val compute_vector_u Prims.l_True (fun _ -> Prims.l_True) +/// The following functions compute various expressions involving +/// vectors and matrices. The computation of these expressions has been +/// abstracted away into these functions in order to save on loop iterations. +/// Compute v − InverseNTT(sᵀ ◦ NTT(u)) val compute_message (v_K: usize) (v: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti index 44b56ea6b..eb88ad0e3 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Ntt.fsti @@ -3,16 +3,28 @@ module Libcrux_ml_kem.Ntt open Core open FStar.Mul +/// Use the Gentleman-Sande butterfly to invert, in-place, the NTT representation +/// of a `KyberPolynomialRingElement`. The coefficients of the output +/// ring element are in the Montgomery domain. val invert_ntt_montgomery (v_K: usize) (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement) : Prims.Pure Libcrux_ml_kem.Polynomial.t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) +/// Use the Cooley–Tukey butterfly to compute an in-place NTT representation +/// of a `KyberPolynomialRingElement`. +/// This function operates only on those which were produced by binomial +/// sampling, and thus those which have small coefficients. The small +/// coefficients let us skip the first round of Montgomery reductions. val ntt_binomially_sampled_ring_element (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement) : Prims.Pure Libcrux_ml_kem.Polynomial.t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) +/// Use the Cooley–Tukey butterfly to compute an in-place NTT representation +/// of a `KyberPolynomialRingElement`. +/// This function operates on the ring element that partly constitutes +/// the ciphertext. val ntt_vector_u (v_VECTOR_U_COMPRESSION_FACTOR: usize) (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti index 73f7e276a..4b420b39b 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Polynomial.fsti @@ -42,6 +42,8 @@ val add_message_error_reduce (err message result: t_PolynomialRingElement) val add_standard_error_reduce (err result: t_PolynomialRingElement) : Prims.Pure t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) +/// Given two polynomial ring elements `lhs` and `rhs`, compute the pointwise +/// sum of their constituent coefficients. val add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) : Prims.Pure t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) @@ -62,6 +64,9 @@ val invert_ntt_at_layer_2_ (zeta_i: usize) (re: t_PolynomialRingElement) (v__lay val invert_ntt_at_layer_3_plus (zeta_i: usize) (re: t_PolynomialRingElement) (layer: usize) : Prims.Pure (usize & t_PolynomialRingElement) Prims.l_True (fun _ -> Prims.l_True) +/// Represents an intermediate polynomial splitting step in the NTT. All +/// resulting coefficients are in the normal domain since the zetas have been +/// multiplied by MONTGOMERY_R. val ntt_at_layer_1_ (zeta_i: usize) (re: t_PolynomialRingElement) @@ -93,6 +98,26 @@ val ntt_at_layer_3_plus (layer v__initial_coefficient_bound: usize) : Prims.Pure (usize & t_PolynomialRingElement) Prims.l_True (fun _ -> Prims.l_True) +/// Given two `KyberPolynomialRingElement`s in their NTT representations, +/// compute their product. Given two polynomials in the NTT domain `f^` and `ĵ`, +/// the `iᵗʰ` coefficient of the product `k̂` is determined by the calculation: +/// ```plaintext +/// ĥ[2·i] + ĥ[2·i + 1]X = (f^[2·i] + f^[2·i + 1]X)·(ĝ[2·i] + ĝ[2·i + 1]X) mod (X² - ζ^(2·BitRev₇(i) + 1)) +/// ``` +/// This function almost implements Algorithm 10 of the +/// NIST FIPS 203 standard, which is reproduced below: +/// ```plaintext +/// Input: Two arrays fˆ ∈ ℤ₂₅₆ and ĝ ∈ ℤ₂₅₆. +/// Output: An array ĥ ∈ ℤq. +/// for(i ← 0; i < 128; i++) +/// (ĥ[2i], ĥ[2i+1]) ← BaseCaseMultiply(fˆ[2i], fˆ[2i+1], ĝ[2i], ĝ[2i+1], ζ^(2·BitRev₇(i) + 1)) +/// end for +/// return ĥ +/// ``` +/// We say "almost" because the coefficients of the ring element output by +/// this function are in the Montgomery domain. +/// The NIST FIPS 203 standard can be found at +/// . val ntt_multiply (lhs rhs: t_PolynomialRingElement) : Prims.Pure t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti index 6ddcb90a1..8cc26bf3b 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Sampling.fsti @@ -3,6 +3,39 @@ module Libcrux_ml_kem.Sampling open Core open FStar.Mul +/// If `bytes` contains a set of uniformly random bytes, this function +/// uniformly samples a ring element `â` that is treated as being the NTT representation +/// of the corresponding polynomial `a`. +/// Since rejection sampling is used, it is possible the supplied bytes are +/// not enough to sample the element, in which case an `Err` is returned and the +/// caller must try again with a fresh set of bytes. +/// This function partially implements Algorithm 6 of the NIST FIPS 203 standard, +/// We say "partially" because this implementation only accepts a finite set of +/// bytes as input and returns an error if the set is not enough; Algorithm 6 of +/// the FIPS 203 standard on the other hand samples from an infinite stream of bytes +/// until the ring element is filled. Algorithm 6 is reproduced below: +/// ```plaintext +/// Input: byte stream B ∈ 𝔹*. +/// Output: array â ∈ ℤ₂₅₆. +/// i ← 0 +/// j ← 0 +/// while j < 256 do +/// d₁ ← B[i] + 256·(B[i+1] mod 16) +/// d₂ ← ⌊B[i+1]/16⌋ + 16·B[i+2] +/// if d₁ < q then +/// â[j] ← d₁ +/// j ← j + 1 +/// end if +/// if d₂ < q and j < 256 then +/// â[j] ← d₂ +/// j ← j + 1 +/// end if +/// i ← i + 3 +/// end while +/// return â +/// ``` +/// The NIST FIPS 203 standard can be found at +/// . val sample_from_uniform_distribution_next (v_K v_N: usize) (randomness: t_Array (t_Array u8 v_N) v_K) @@ -12,6 +45,44 @@ val sample_from_uniform_distribution_next Prims.l_True (fun _ -> Prims.l_True) +/// Given a series of uniformly random bytes in `randomness`, for some number `eta`, +/// the `sample_from_binomial_distribution_{eta}` functions sample +/// a ring element from a binomial distribution centered at 0 that uses two sets +/// of `eta` coin flips. If, for example, +/// `eta = ETA`, each ring coefficient is a value `v` such +/// such that `v ∈ {-ETA, -ETA + 1, ..., 0, ..., ETA + 1, ETA}` and: +/// ```plaintext +/// - If v < 0, Pr[v] = Pr[-v] +/// - If v >= 0, Pr[v] = BINOMIAL_COEFFICIENT(2 * ETA; ETA - v) / 2 ^ (2 * ETA) +/// ``` +/// The values `v < 0` are mapped to the appropriate `KyberFieldElement`. +/// The expected value is: +/// ```plaintext +/// E[X] = (-ETA)Pr[-ETA] + (-(ETA - 1))Pr[-(ETA - 1)] + ... + (ETA - 1)Pr[ETA - 1] + (ETA)Pr[ETA] +/// = 0 since Pr[-v] = Pr[v] when v < 0. +/// ``` +/// And the variance is: +/// ```plaintext +/// Var(X) = E[(X - E[X])^2] +/// = E[X^2] +/// = sum_(v=-ETA to ETA)v^2 * (BINOMIAL_COEFFICIENT(2 * ETA; ETA - v) / 2^(2 * ETA)) +/// = ETA / 2 +/// ``` +/// This function implements Algorithm 7 of the NIST FIPS 203 standard, which is +/// reproduced below: +/// ```plaintext +/// Input: byte array B ∈ 𝔹^{64η}. +/// Output: array f ∈ ℤ₂₅₆. +/// b ← BytesToBits(B) +/// for (i ← 0; i < 256; i++) +/// x ← ∑(j=0 to η - 1) b[2iη + j] +/// y ← ∑(j=0 to η - 1) b[2iη + η + j] +/// f[i] ← x−y mod q +/// end for +/// return f +/// ``` +/// The NIST FIPS 203 standard can be found at +/// . val sample_from_binomial_distribution_2_ (randomness: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Polynomial.t_PolynomialRingElement (requires (Core.Slice.impl__len randomness <: usize) =. (sz 2 *! sz 64 <: usize)) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst index 7a59b3111..9da5f3c3e 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst @@ -22,7 +22,7 @@ let compress_then_serialize_10_ let serialized:t_Array u8 v_OUT_LEN = serialized in let i:usize = i in let coefficient:Libcrux_ml_kem.Simd.Portable.t_PortableVector = - Libcrux_ml_kem.Simd.Simd_trait.f_compress 10uy + Libcrux_ml_kem.Simd.Simd_trait.f_compress 10l (Libcrux_ml_kem.Simd.Simd_trait.f_to_unsigned_representative (re .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: @@ -106,7 +106,7 @@ let compress_then_serialize_11_ let serialized:t_Array u8 v_OUT_LEN = serialized in let i:usize = i in let coefficient:Libcrux_ml_kem.Simd.Portable.t_PortableVector = - Libcrux_ml_kem.Simd.Simd_trait.f_compress 11uy + Libcrux_ml_kem.Simd.Simd_trait.f_compress 11l (Libcrux_ml_kem.Simd.Simd_trait.f_to_unsigned_representative (re .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: @@ -195,7 +195,7 @@ let compress_then_serialize_4_ let serialized:t_Array u8 v_OUT_LEN = serialized in let i:usize = i in let coefficient:Libcrux_ml_kem.Simd.Portable.t_PortableVector = - Libcrux_ml_kem.Simd.Simd_trait.f_compress 4uy + Libcrux_ml_kem.Simd.Simd_trait.f_compress 4l (Libcrux_ml_kem.Simd.Simd_trait.f_to_unsigned_representative (re .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: @@ -247,7 +247,7 @@ let compress_then_serialize_5_ let serialized:t_Array u8 v_OUT_LEN = serialized in let i:usize = i in let coefficients:Libcrux_ml_kem.Simd.Portable.t_PortableVector = - Libcrux_ml_kem.Simd.Simd_trait.f_compress 5uy + Libcrux_ml_kem.Simd.Simd_trait.f_compress 5l (Libcrux_ml_kem.Simd.Simd_trait.f_to_unsigned_representative (re .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti index b22181e35..2df84a28f 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti @@ -75,11 +75,16 @@ val deserialize_then_decompress_ring_element_v Prims.l_True (fun _ -> Prims.l_True) +/// Only use with public values. +/// This MUST NOT be used with secret inputs, like its caller `deserialize_ring_elements_reduced`. val deserialize_to_reduced_ring_element (serialized: t_Slice u8) : Prims.Pure Libcrux_ml_kem.Polynomial.t_PolynomialRingElement Prims.l_True (fun _ -> Prims.l_True) +/// This function deserializes ring elements and reduces the result by the field +/// modulus. +/// This function MUST NOT be used on secret inputs. val deserialize_ring_elements_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) : Prims.Pure (t_Array Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_K) Prims.l_True diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fst index 135c5996e..b3f774843 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fst +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fst @@ -122,7 +122,7 @@ let bitwise_and_with_constant (v: t_PortableVector) (c: i32) = in v -let compress (coefficient_bits: u8) (v: t_PortableVector) = +let compress (v_COEFFICIENT_BITS: i32) (v: t_PortableVector) = let v:t_PortableVector = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({ Core.Ops.Range.f_start = sz 0; @@ -142,7 +142,11 @@ let compress (coefficient_bits: u8) (v: t_PortableVector) = = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v.f_elements i - (Libcrux_ml_kem.Compress.compress_ciphertext_coefficient coefficient_bits + (Libcrux_ml_kem.Compress.compress_ciphertext_coefficient (cast (v_COEFFICIENT_BITS + <: + i32) + <: + u8) (cast (v.f_elements.[ i ] <: i32) <: u16) <: i32) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fsti index ba8e40612..4c966919d 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Portable.fsti @@ -19,7 +19,7 @@ val barrett_reduce (v: t_PortableVector) val bitwise_and_with_constant (v: t_PortableVector) (c: i32) : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True) -val compress (coefficient_bits: u8) (v: t_PortableVector) +val compress (v_COEFFICIENT_BITS: i32) (v: t_PortableVector) : Prims.Pure t_PortableVector Prims.l_True (fun _ -> Prims.l_True) val compress_1_ (v: t_PortableVector) @@ -101,7 +101,9 @@ val ntt_multiply (lhs rhs: t_PortableVector) (zeta0 zeta1: i32) [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: Libcrux_ml_kem.Simd.Simd_trait.t_Operations t_PortableVector = { - f_ZERO = v_ZERO (); + f_ZERO_pre = (fun (_: Prims.unit) -> true); + f_ZERO_post = (fun (_: Prims.unit) (out: t_PortableVector) -> true); + f_ZERO = (fun (_: Prims.unit) -> v_ZERO ()); f_to_i32_array_pre = (fun (v: t_PortableVector) -> true); f_to_i32_array_post = (fun (v: t_PortableVector) (out: t_Array i32 (sz 8)) -> true); f_to_i32_array = (fun (v: t_PortableVector) -> to_i32_array v); @@ -155,11 +157,13 @@ let impl: Libcrux_ml_kem.Simd.Simd_trait.t_Operations t_PortableVector = f_compress_1_pre = (fun (v: t_PortableVector) -> true); f_compress_1_post = (fun (v: t_PortableVector) (out: t_PortableVector) -> true); f_compress_1_ = (fun (v: t_PortableVector) -> compress_1_ v); - f_compress_pre = (fun (coefficient_bits: u8) (v: t_PortableVector) -> true); + f_compress_pre = (fun (v_COEFFICIENT_BITS: i32) (v: t_PortableVector) -> true); f_compress_post = - (fun (coefficient_bits: u8) (v: t_PortableVector) (out: t_PortableVector) -> true); - f_compress = (fun (coefficient_bits: u8) (v: t_PortableVector) -> compress coefficient_bits v); + (fun (v_COEFFICIENT_BITS: i32) (v: t_PortableVector) (out: t_PortableVector) -> true); + f_compress + = + (fun (v_COEFFICIENT_BITS: i32) (v: t_PortableVector) -> compress v_COEFFICIENT_BITS v); f_ntt_layer_1_step_pre = (fun (a: t_PortableVector) (zeta1: i32) (zeta2: i32) -> true); f_ntt_layer_1_step_post = diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Simd_trait.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Simd_trait.fsti index cbf4da7f9..19816e5a7 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Simd_trait.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Simd.Simd_trait.fsti @@ -25,7 +25,7 @@ class t_GenericOperations (v_Self: Type) = { f_decompress_1_pre:v_Self -> bool; f_decompress_1_post:v_Self -> v_Self -> bool; f_decompress_1_:x0: v_Self - -> Prims.Pure v_Self (f_decompress_1__pre x0) (fun result -> f_decompress_1__post x0 result); + -> Prims.Pure v_Self (f_decompress_1_pre x0) (fun result -> f_decompress_1_post x0 result); f_decompress_pre:v_COEFFICIENT_BITS: i32 -> v_Self -> bool; f_decompress_post:v_COEFFICIENT_BITS: i32 -> v_Self -> v_Self -> bool; f_decompress:v_COEFFICIENT_BITS: i32 -> x0: v_Self @@ -88,8 +88,8 @@ class t_Operations (v_Self: Type) = { f_cond_subtract_3329_post:v_Self -> v_Self -> bool; f_cond_subtract_3329_:x0: v_Self -> Prims.Pure v_Self - (f_cond_subtract_3329__pre x0) - (fun result -> f_cond_subtract_3329__post x0 result); + (f_cond_subtract_3329_pre x0) + (fun result -> f_cond_subtract_3329_post x0 result); f_barrett_reduce_pre:v_Self -> bool; f_barrett_reduce_post:v_Self -> v_Self -> bool; f_barrett_reduce:x0: v_Self @@ -103,11 +103,13 @@ class t_Operations (v_Self: Type) = { f_compress_1_pre:v_Self -> bool; f_compress_1_post:v_Self -> v_Self -> bool; f_compress_1_:x0: v_Self - -> Prims.Pure v_Self (f_compress_1__pre x0) (fun result -> f_compress_1__post x0 result); - f_compress_pre:u8 -> v_Self -> bool; - f_compress_post:u8 -> v_Self -> v_Self -> bool; - f_compress:x0: u8 -> x1: v_Self - -> Prims.Pure v_Self (f_compress_pre x0 x1) (fun result -> f_compress_post x0 x1 result); + -> Prims.Pure v_Self (f_compress_1_pre x0) (fun result -> f_compress_1_post x0 result); + f_compress_pre:v_COEFFICIENT_BITS: i32 -> v_Self -> bool; + f_compress_post:v_COEFFICIENT_BITS: i32 -> v_Self -> v_Self -> bool; + f_compress:v_COEFFICIENT_BITS: i32 -> x0: v_Self + -> Prims.Pure v_Self + (f_compress_pre v_COEFFICIENT_BITS x0) + (fun result -> f_compress_post v_COEFFICIENT_BITS x0 result); f_ntt_layer_1_step_pre:v_Self -> i32 -> i32 -> bool; f_ntt_layer_1_step_post:v_Self -> i32 -> i32 -> v_Self -> bool; f_ntt_layer_1_step:x0: v_Self -> x1: i32 -> x2: i32 @@ -141,61 +143,61 @@ class t_Operations (v_Self: Type) = { f_serialize_1_pre:v_Self -> bool; f_serialize_1_post:v_Self -> u8 -> bool; f_serialize_1_:x0: v_Self - -> Prims.Pure u8 (f_serialize_1__pre x0) (fun result -> f_serialize_1__post x0 result); + -> Prims.Pure u8 (f_serialize_1_pre x0) (fun result -> f_serialize_1_post x0 result); f_deserialize_1_pre:u8 -> bool; f_deserialize_1_post:u8 -> v_Self -> bool; f_deserialize_1_:x0: u8 - -> Prims.Pure v_Self (f_deserialize_1__pre x0) (fun result -> f_deserialize_1__post x0 result); + -> Prims.Pure v_Self (f_deserialize_1_pre x0) (fun result -> f_deserialize_1_post x0 result); f_serialize_4_pre:v_Self -> bool; f_serialize_4_post:v_Self -> t_Array u8 (sz 4) -> bool; f_serialize_4_:x0: v_Self -> Prims.Pure (t_Array u8 (sz 4)) - (f_serialize_4__pre x0) - (fun result -> f_serialize_4__post x0 result); + (f_serialize_4_pre x0) + (fun result -> f_serialize_4_post x0 result); f_deserialize_4_pre:t_Slice u8 -> bool; f_deserialize_4_post:t_Slice u8 -> v_Self -> bool; f_deserialize_4_:x0: t_Slice u8 - -> Prims.Pure v_Self (f_deserialize_4__pre x0) (fun result -> f_deserialize_4__post x0 result); + -> Prims.Pure v_Self (f_deserialize_4_pre x0) (fun result -> f_deserialize_4_post x0 result); f_serialize_5_pre:v_Self -> bool; f_serialize_5_post:v_Self -> t_Array u8 (sz 5) -> bool; f_serialize_5_:x0: v_Self -> Prims.Pure (t_Array u8 (sz 5)) - (f_serialize_5__pre x0) - (fun result -> f_serialize_5__post x0 result); + (f_serialize_5_pre x0) + (fun result -> f_serialize_5_post x0 result); f_deserialize_5_pre:t_Slice u8 -> bool; f_deserialize_5_post:t_Slice u8 -> v_Self -> bool; f_deserialize_5_:x0: t_Slice u8 - -> Prims.Pure v_Self (f_deserialize_5__pre x0) (fun result -> f_deserialize_5__post x0 result); + -> Prims.Pure v_Self (f_deserialize_5_pre x0) (fun result -> f_deserialize_5_post x0 result); f_serialize_10_pre:v_Self -> bool; f_serialize_10_post:v_Self -> t_Array u8 (sz 10) -> bool; f_serialize_10_:x0: v_Self -> Prims.Pure (t_Array u8 (sz 10)) - (f_serialize_10__pre x0) - (fun result -> f_serialize_10__post x0 result); + (f_serialize_10_pre x0) + (fun result -> f_serialize_10_post x0 result); f_deserialize_10_pre:t_Slice u8 -> bool; f_deserialize_10_post:t_Slice u8 -> v_Self -> bool; f_deserialize_10_:x0: t_Slice u8 - -> Prims.Pure v_Self (f_deserialize_10__pre x0) (fun result -> f_deserialize_10__post x0 result); + -> Prims.Pure v_Self (f_deserialize_10_pre x0) (fun result -> f_deserialize_10_post x0 result); f_serialize_11_pre:v_Self -> bool; f_serialize_11_post:v_Self -> t_Array u8 (sz 11) -> bool; f_serialize_11_:x0: v_Self -> Prims.Pure (t_Array u8 (sz 11)) - (f_serialize_11__pre x0) - (fun result -> f_serialize_11__post x0 result); + (f_serialize_11_pre x0) + (fun result -> f_serialize_11_post x0 result); f_deserialize_11_pre:t_Slice u8 -> bool; f_deserialize_11_post:t_Slice u8 -> v_Self -> bool; f_deserialize_11_:x0: t_Slice u8 - -> Prims.Pure v_Self (f_deserialize_11__pre x0) (fun result -> f_deserialize_11__post x0 result); + -> Prims.Pure v_Self (f_deserialize_11_pre x0) (fun result -> f_deserialize_11_post x0 result); f_serialize_12_pre:v_Self -> bool; f_serialize_12_post:v_Self -> t_Array u8 (sz 12) -> bool; f_serialize_12_:x0: v_Self -> Prims.Pure (t_Array u8 (sz 12)) - (f_serialize_12__pre x0) - (fun result -> f_serialize_12__post x0 result); + (f_serialize_12_pre x0) + (fun result -> f_serialize_12_post x0 result); f_deserialize_12_pre:t_Slice u8 -> bool; f_deserialize_12_post:t_Slice u8 -> v_Self -> bool; f_deserialize_12_:x0: t_Slice u8 - -> Prims.Pure v_Self (f_deserialize_12__pre x0) (fun result -> f_deserialize_12__post x0 result) + -> Prims.Pure v_Self (f_deserialize_12_pre x0) (fun result -> f_deserialize_12_post x0 result) } [@@ FStar.Tactics.Typeclasses.tcinstance] diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti index edd1dadc6..2de0ab7bb 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Types.fsti @@ -219,6 +219,7 @@ let impl_17 (v_SIZE: usize) : Core.Convert.t_TryFrom (t_MlKemPublicKey v_SIZE) ( Core.Result.t_Result (t_MlKemPublicKey v_SIZE) Core.Array.t_TryFromSliceError } +/// An ML-KEM key pair type t_MlKemKeyPair (v_PRIVATE_KEY_SIZE: usize) (v_PUBLIC_KEY_SIZE: usize) = { f_sk:t_MlKemPrivateKey v_PRIVATE_KEY_SIZE; f_pk:t_MlKemPublicKey v_PUBLIC_KEY_SIZE @@ -232,6 +233,7 @@ val impl__from Prims.l_True (fun _ -> Prims.l_True) +/// Creates a new [`MlKemKeyPair`]. val impl__new (v_PRIVATE_KEY_SIZE v_PUBLIC_KEY_SIZE: usize) (sk: t_Array u8 v_PRIVATE_KEY_SIZE) diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.fsti index e7fd2e46c..0b1520067 100644 --- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.fsti +++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.fsti @@ -6,10 +6,15 @@ open FStar.Mul unfold let t_MlKemSharedSecret = t_Array u8 (sz 32) +/// Seed size for encapsulation +let v_ENCAPS_SEED_SIZE: usize = Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE + +/// Seed size for key generation let v_KEY_GENERATION_SEED_SIZE: usize = Libcrux_ml_kem.Constants.v_CPA_PKE_KEY_GENERATION_SEED_SIZE +! Libcrux_ml_kem.Constants.v_SHARED_SECRET_SIZE +/// Serialize the secret key. val serialize_kem_secret_key (v_SERIALIZED_KEY_LEN: usize) (private_key public_key implicit_rejection_value: t_Slice u8) diff --git a/sys/hacl/c/src/Hacl_Hash_SHA3_Scalar.c b/sys/hacl/c/src/Hacl_Hash_SHA3_Scalar.c index 24f05386b..6d6806a37 100644 --- a/sys/hacl/c/src/Hacl_Hash_SHA3_Scalar.c +++ b/sys/hacl/c/src/Hacl_Hash_SHA3_Scalar.c @@ -1158,12 +1158,14 @@ void Hacl_Hash_SHA3_Scalar_sha3_224(uint8_t *output, uint8_t *input, uint32_t in uint64_t c = Hacl_Impl_SHA3_Vec_keccak_rndc[i0]; s[0U] = s[0U] ^ c; } - uint8_t hbuf[200U] = { 0U }; for (uint32_t i0 = 0U; i0 < 28U / rateInBytes; i0++) { - for (uint32_t i = 0U; i < 25U; i++) + uint8_t hbuf[256U] = { 0U }; + uint64_t ws[32U] = { 0U }; + memcpy(ws, s, 25U * sizeof (uint64_t)); + for (uint32_t i = 0U; i < 32U; i++) { - store64_le(hbuf + i * 8U, s[i]); + store64_le(hbuf + i * 8U, ws[i]); } memcpy(output + i0 * rateInBytes, hbuf, rateInBytes * sizeof (uint8_t)); for (uint32_t i1 = 0U; i1 < 24U; i1++) @@ -1211,9 +1213,12 @@ void Hacl_Hash_SHA3_Scalar_sha3_224(uint8_t *output, uint8_t *input, uint32_t in } } uint32_t remOut = 28U % rateInBytes; - for (uint32_t i = 0U; i < 25U; i++) + uint8_t hbuf[256U] = { 0U }; + uint64_t ws[32U] = { 0U }; + memcpy(ws, s, 25U * sizeof (uint64_t)); + for (uint32_t i = 0U; i < 32U; i++) { - store64_le(hbuf + i * 8U, s[i]); + store64_le(hbuf + i * 8U, ws[i]); } memcpy(output + 28U - remOut, hbuf, remOut * sizeof (uint8_t)); } @@ -2732,12 +2737,14 @@ Hacl_Hash_SHA3_Scalar_shake128_squeeze_nblocks( uint32_t outputByteLen ) { - uint8_t hbuf[200U] = { 0U }; for (uint32_t i0 = 0U; i0 < outputByteLen / 168U; i0++) { - for (uint32_t i = 0U; i < 25U; i++) + uint8_t hbuf[256U] = { 0U }; + uint64_t ws[32U] = { 0U }; + memcpy(ws, state, 25U * sizeof (uint64_t)); + for (uint32_t i = 0U; i < 32U; i++) { - store64_le(hbuf + i * 8U, state[i]); + store64_le(hbuf + i * 8U, ws[i]); } memcpy(output + i0 * 168U, hbuf, 168U * sizeof (uint8_t)); for (uint32_t i1 = 0U; i1 < 24U; i1++)