Merge branch 'main' into franziskus/ml-kem-cli

proofs/fstar/extraction/Libcrux.Digest.Incremental_x4.fsti

@@ -3,20 +3,28 @@ module Libcrux.Digest.Incremental_x4
 open Core
 open FStar.Mul
 
+/// Incremental state
 val t_Shake128StateX4:Type
 
+/// Absorb up to 4 blocks.
+/// The `input` must be of length 1 to 4.
+/// A blocks MUST all be the same length.
+/// Each slice MUST be a multiple of the block length 168.
 val impl__Shake128StateX4__absorb_final
       (v_N: usize)
       (self: t_Shake128StateX4)
       (input: t_Array (t_Slice u8) v_N)
     : Prims.Pure t_Shake128StateX4 Prims.l_True (fun _ -> Prims.l_True)
 
+/// This is only used internally to work around Eurydice bugs.
 val impl__Shake128StateX4__free_memory (self: t_Shake128StateX4)
     : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)
 
+/// Create a new Shake128 x4 state.
 val impl__Shake128StateX4__new: Prims.unit
   -> Prims.Pure t_Shake128StateX4 Prims.l_True (fun _ -> Prims.l_True)
 
+/// Squeeze `M` blocks of length `N`
 val impl__Shake128StateX4__squeeze_blocks (v_N v_M: usize) (self: t_Shake128StateX4)
     : Prims.Pure (t_Shake128StateX4 & t_Array (t_Array u8 v_N) v_M)
       Prims.l_True

proofs/fstar/extraction/Libcrux.Digest.fsti

@@ -9,5 +9,7 @@ val sha3_256_ (payload: t_Slice u8)
 val sha3_512_ (payload: t_Slice u8)
     : Prims.Pure (t_Array u8 (sz 64)) Prims.l_True (fun _ -> Prims.l_True)
 
+/// SHAKE 256
+/// The caller must define the size of the output in the return type.
 val shake256 (v_LEN: usize) (data: t_Slice u8)
     : Prims.Pure (t_Array u8 v_LEN) Prims.l_True (fun _ -> Prims.l_True)

proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fsti

@@ -3,15 +3,24 @@ module Libcrux.Kem.Kyber.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 <<! v_BARRETT_SHIFT
 
 let v_INVERSE_OF_MODULUS_MOD_MONTGOMERY_R: u32 = 62209ul
 
+/// This is calculated as (MONTGOMERY_R)^2 mod FIELD_MODULUS
 let v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS: i32 = 1353l
 
 let v_MONTGOMERY_SHIFT: u8 = 16uy
@@ -34,6 +44,13 @@ val get_n_least_significant_bits (n: u8) (value: u32)
           let result:u32 = result in
           result <. (Core.Num.impl__u32__pow 2ul (Core.Convert.f_into n <: u32) <: u32))
 
+/// 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
@@ -45,6 +62,13 @@ val barrett_reduce (value: i32)
           result >. (Core.Ops.Arith.Neg.neg Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) &&
           result <. Libcrux.Kem.Kyber.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
@@ -65,11 +89,28 @@ val montgomery_reduce (value: i32)
             i32) &&
           result <=. ((3l *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) /! 2l <: i32))
 
+/// 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)
 
+/// 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 to_standard_domain (mfe: i32) : Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)
 
+/// Given a field element `fe` such that -FIELD_MODULUS ≤ fe < FIELD_MODULUS,
+/// output `o` such that:
+/// - `o` is congruent to `fe`
+/// - 0 ≤ `o` FIELD_MODULUS
 val to_unsigned_representative (fe: i32)
     : Prims.Pure u16
       (requires
@@ -86,6 +127,8 @@ type t_PolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) }
 let impl__PolynomialRingElement__ZERO: t_PolynomialRingElement =
   { f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) } <: t_PolynomialRingElement
 
+/// 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
       (requires

proofs/fstar/extraction/Libcrux.Kem.Kyber.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
+/// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 val compress_message_coefficient (fe: u16)
     : Prims.Pure u8
       (requires fe <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
@@ -42,5 +57,20 @@ val decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32)
           let result:i32 = result in
           result <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS)
 
+/// The `decompress_*` functions implement the `Decompress` function specified in the NIST FIPS
+/// 203 standard (Page 18, Expression 4.6), which is defined as:
+/// ```plaintext
+/// Decompress_d: ℤ_{2ᵈ} -> ℤq
+/// Decompress_d(y) = ⌈(q/2ᵈ)·y⌋
+/// ```
+/// Since `⌈x⌋ = ⌊x + 1/2⌋` we have:
+/// ```plaintext
+/// Decompress_d(y) = ⌊(q/2ᵈ)·y + 1/2⌋
+///                 = ⌊(2·y·q + 2ᵈ) / 2^{d+1})⌋
+/// ```
+/// 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
+/// <https://csrc.nist.gov/pubs/fips/203/ipd>.
 val decompress_message_coefficient (fe: i32)
     : Prims.Pure i32 (requires fe =. 0l || fe =. 1l) (fun _ -> Prims.l_True)

proofs/fstar/extraction/Libcrux.Kem.Kyber.Constant_time_ops.fsti

@@ -3,6 +3,7 @@ module Libcrux.Kem.Kyber.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

proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fsti

@@ -3,18 +3,24 @@ module Libcrux.Kem.Kyber.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

proofs/fstar/extraction/Libcrux.Kem.Kyber.Hash_functions.fsti

@@ -19,6 +19,8 @@ val absorb (v_K: usize) (input: t_Array (t_Array u8 (sz 34)) v_K)
       Prims.l_True
       (fun _ -> Prims.l_True)
 
+/// Free the memory of the state.
+/// **NOTE:** That this needs to be done manually for now.
 val free_state (xof_state: Libcrux.Digest.Incremental_x4.t_Shake128StateX4)
     : Prims.Pure Prims.unit Prims.l_True (fun _ -> Prims.l_True)