From b8e7179405a0fbd503cc07226c2ff3227eb230e2 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Tue, 10 Oct 2023 10:59:45 +0200 Subject: [PATCH] smaller change --- .../extraction/Libcrux.Kem.Kyber.Compress.fst | 12 ++++-------- .../extraction/Libcrux.Kem.Kyber.Ind_cpa.fst | 17 +++++++---------- .../extraction/Libcrux.Kem.Kyber.Kyber1024.fst | 10 ++++------ .../extraction/Libcrux.Kem.Kyber.Kyber512.fst | 10 ++++------ .../extraction/Libcrux.Kem.Kyber.Kyber768.fst | 10 ++++------ .../extraction/Libcrux.Kem.Kyber.Serialize.fst | 17 +++++++---------- proofs/fstar/extraction/Libcrux.Kem.Kyber.fst | 8 ++------ src/kem/kyber.rs | 8 ++++---- src/kem/kyber/compress.rs | 6 +++--- src/kem/kyber/ind_cpa.rs | 14 +++++++------- src/kem/kyber/kyber1024.rs | 9 ++++----- src/kem/kyber/kyber512.rs | 9 ++++----- src/kem/kyber/kyber768.rs | 9 ++++----- src/kem/kyber/serialize.rs | 18 +++++++----------- 14 files changed, 65 insertions(+), 92 deletions(-) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst index ce194229d..7d9e0a7e4 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst @@ -3,7 +3,7 @@ module Libcrux.Kem.Kyber.Compress open Core let compress - (#v_COEFFICIENT_BITS: u32) + (#v_COEFFICIENT_BITS: usize) (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = let re:Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = @@ -35,18 +35,14 @@ let decompress in re -let compress_q (#v_COEFFICIENT_BITS: u32) (fe: u16) : i32 = +let compress_q (#v_COEFFICIENT_BITS: usize) (fe: u16) : i32 = let _:Prims.unit = if true then let _:Prims.unit = - if - ~.((cast v_COEFFICIENT_BITS <: usize) <=. - Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT - <: - bool) + if ~.(v_COEFFICIENT_BITS <=. Libcrux.Kem.Kyber.Constants.v_BITS_PER_COEFFICIENT <: bool) then - Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS as usize <= BITS_PER_COEFFICIENT" + Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: COEFFICIENT_BITS <= BITS_PER_COEFFICIENT" <: Rust_primitives.Hax.t_Never) diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst index 200ab3227..95b6b1abb 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ind_cpa.fst @@ -469,9 +469,7 @@ let serialize_secret_key Libcrux.Kem.Kyber.Conversions.t_UpdatableArray v_SERIALIZED_KEY_LEN) let compress_then_encode_u - (#v_K #v_OUT_LEN: usize) - (#v_COMPRESSION_FACTOR: u32) - (#v_BLOCK_LEN: usize) + (#v_K #v_OUT_LEN #v_COMPRESSION_FACTOR #v_BLOCK_LEN: usize) (input: array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K) : array u8 v_OUT_LEN = let out:array u8 v_OUT_LEN = Rust_primitives.Hax.repeat 0uy v_OUT_LEN in @@ -516,9 +514,8 @@ let compress_then_encode_u out let encrypt - (#v_K #v_CIPHERTEXT_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_LEN #v_C2_LEN: usize) - (#v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR: u32) - (#v_BLOCK_LEN: usize) + (#v_K #v_CIPHERTEXT_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_LEN #v_C2_LEN #v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR #v_BLOCK_LEN: + usize) (public_key: slice u8) (message: array u8 (sz 32)) (randomness: slice u8) @@ -672,8 +669,8 @@ let encrypt Core.Convert.f_into ciphertext, sampling_A_error let decrypt - (#v_K #v_CIPHERTEXT_SIZE #v_VECTOR_U_ENCODED_SIZE: usize) - (#v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR: u32) + (#v_K #v_CIPHERTEXT_SIZE #v_VECTOR_U_ENCODED_SIZE #v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR: + usize) (secret_key: slice u8) (ciphertext: Libcrux.Kem.Kyber.t_KyberCiphertext v_CIPHERTEXT_SIZE) : array u8 (sz 32) = @@ -691,7 +688,7 @@ let decrypt <: slice u8) ((Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_U_COMPRESSION_FACTOR <: usize) + v_VECTOR_U_COMPRESSION_FACTOR <: usize) /! sz 8 @@ -727,7 +724,7 @@ let decrypt slice u8) <: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) - (cast v_VECTOR_V_COMPRESSION_FACTOR <: usize) + v_VECTOR_V_COMPRESSION_FACTOR in let secret_as_ntt:array Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement v_K = Core.Iter.Traits.Iterator.Iterator.fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst index 7fff01223..3ab01eee6 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber1024.fst @@ -14,22 +14,20 @@ let v_T_AS_NTT_ENCODED_SIZE_1024_: usize = usize) /! sz 8 -let v_VECTOR_U_COMPRESSION_FACTOR_1024_: u32 = 11ul +let v_VECTOR_U_COMPRESSION_FACTOR_1024_: usize = sz 11 let v_C1_BLOCK_SIZE_1024_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_U_COMPRESSION_FACTOR_1024_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_U_COMPRESSION_FACTOR_1024_ <: usize) /! sz 8 let v_C1_SIZE_1024_: usize = v_C1_BLOCK_SIZE_1024_ *! v_RANK_1024_ -let v_VECTOR_V_COMPRESSION_FACTOR_1024_: u32 = 5ul +let v_VECTOR_V_COMPRESSION_FACTOR_1024_: usize = sz 5 let v_C2_SIZE_1024_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_V_COMPRESSION_FACTOR_1024_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_V_COMPRESSION_FACTOR_1024_ <: usize) /! sz 8 diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst index 1394f63a9..dae0e7871 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber512.fst @@ -14,22 +14,20 @@ let v_T_AS_NTT_ENCODED_SIZE_512_: usize = usize) /! sz 8 -let v_VECTOR_U_COMPRESSION_FACTOR_512_: u32 = 10ul +let v_VECTOR_U_COMPRESSION_FACTOR_512_: usize = sz 10 let v_C1_BLOCK_SIZE_512_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_U_COMPRESSION_FACTOR_512_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_U_COMPRESSION_FACTOR_512_ <: usize) /! sz 8 let v_C1_SIZE_512_: usize = v_C1_BLOCK_SIZE_512_ *! v_RANK_512_ -let v_VECTOR_V_COMPRESSION_FACTOR_512_: u32 = 4ul +let v_VECTOR_V_COMPRESSION_FACTOR_512_: usize = sz 4 let v_C2_SIZE_512_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_V_COMPRESSION_FACTOR_512_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_V_COMPRESSION_FACTOR_512_ <: usize) /! sz 8 diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst index 9c7995837..73ad919f3 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Kyber768.fst @@ -14,22 +14,20 @@ let v_T_AS_NTT_ENCODED_SIZE_768_: usize = usize) /! sz 8 -let v_VECTOR_U_COMPRESSION_FACTOR_768_: u32 = 10ul +let v_VECTOR_U_COMPRESSION_FACTOR_768_: usize = sz 10 let v_C1_BLOCK_SIZE_768_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_U_COMPRESSION_FACTOR_768_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_U_COMPRESSION_FACTOR_768_ <: usize) /! sz 8 let v_C1_SIZE_768_: usize = v_C1_BLOCK_SIZE_768_ *! v_RANK_768_ -let v_VECTOR_V_COMPRESSION_FACTOR_768_: u32 = 4ul +let v_VECTOR_V_COMPRESSION_FACTOR_768_: usize = sz 4 let v_C2_SIZE_768_: usize = - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_VECTOR_V_COMPRESSION_FACTOR_768_ <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_VECTOR_V_COMPRESSION_FACTOR_768_ <: usize) /! sz 8 diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst index b7b1dc1bc..b8498c01e 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst @@ -3,8 +3,7 @@ module Libcrux.Kem.Kyber.Serialize open Core let serialize_little_endian - (#v_COMPRESSION_FACTOR: u32) - (#v_OUT_LEN: usize) + (#v_COMPRESSION_FACTOR #v_OUT_LEN: usize) (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement) : array u8 v_OUT_LEN = let _:Prims.unit = @@ -12,8 +11,7 @@ let serialize_little_endian then let _:Prims.unit = if - ~.(((Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_COMPRESSION_FACTOR <: usize) + ~.(((Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_COMPRESSION_FACTOR <: usize) /! sz 8 @@ -32,7 +30,7 @@ let serialize_little_endian (Rust_primitives.unsize (let list = [ Core.Fmt.Rt.impl_1__new_display ((Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_COMPRESSION_FACTOR <: usize) + v_COMPRESSION_FACTOR <: usize) /! sz 8 @@ -54,7 +52,7 @@ let serialize_little_endian in () in - match v_COMPRESSION_FACTOR with + match cast v_COMPRESSION_FACTOR <: u32 with | 1ul -> serialize_little_endian_1_ re | 4ul -> serialize_little_endian_4_ re | 5ul -> serialize_little_endian_5_ re @@ -84,7 +82,7 @@ let serialize_little_endian <: Rust_primitives.Hax.t_Never) -let deserialize_little_endian (#v_COMPRESSION_FACTOR: u32) (serialized: slice u8) +let deserialize_little_endian (#v_COMPRESSION_FACTOR: usize) (serialized: slice u8) : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement = let _:Prims.unit = if true @@ -92,8 +90,7 @@ let deserialize_little_endian (#v_COMPRESSION_FACTOR: u32) (serialized: slice u8 let _:Prims.unit = match Core.Slice.impl__len serialized, - (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! - (cast v_COMPRESSION_FACTOR <: usize) + (Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT *! v_COMPRESSION_FACTOR <: usize) /! sz 8 @@ -111,7 +108,7 @@ let deserialize_little_endian (#v_COMPRESSION_FACTOR: u32) (serialized: slice u8 in () in - match v_COMPRESSION_FACTOR with + match cast v_COMPRESSION_FACTOR <: u32 with | 1ul -> deserialize_little_endian_1_ serialized | 4ul -> deserialize_little_endian_4_ serialized | 5ul -> deserialize_little_endian_5_ serialized diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst index c3f704e10..5b1c746e0 100644 --- a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst +++ b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst @@ -447,10 +447,8 @@ let generate_keypair Core.Result.Result_Ok (Libcrux.Kem.Kyber.Types.impl__from private_key public_key) let encapsulate - (#v_K #v_SHARED_SECRET_SIZE #v_CIPHERTEXT_SIZE #v_PUBLIC_KEY_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_SIZE #v_C2_SIZE: + (#v_K #v_SHARED_SECRET_SIZE #v_CIPHERTEXT_SIZE #v_PUBLIC_KEY_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_SIZE #v_C2_SIZE #v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR #v_VECTOR_U_BLOCK_LEN: usize) - (#v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR: u32) - (#v_VECTOR_U_BLOCK_LEN: usize) (public_key: t_KyberPublicKey v_PUBLIC_KEY_SIZE) (randomness: array u8 v_SHARED_SECRET_SIZE) : Core.Result.t_Result @@ -533,10 +531,8 @@ let encapsulate else Core.Result.Result_Ok (ciphertext, shared_secret) let decapsulate - (#v_K #v_SECRET_KEY_SIZE #v_CPA_SECRET_KEY_SIZE #v_PUBLIC_KEY_SIZE #v_CIPHERTEXT_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_SIZE #v_C2_SIZE: + (#v_K #v_SECRET_KEY_SIZE #v_CPA_SECRET_KEY_SIZE #v_PUBLIC_KEY_SIZE #v_CIPHERTEXT_SIZE #v_T_AS_NTT_ENCODED_SIZE #v_C1_SIZE #v_C2_SIZE #v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR #v_C1_BLOCK_SIZE: usize) - (#v_VECTOR_U_COMPRESSION_FACTOR #v_VECTOR_V_COMPRESSION_FACTOR: u32) - (#v_C1_BLOCK_SIZE: usize) (secret_key: t_KyberPrivateKey v_SECRET_KEY_SIZE) (ciphertext: t_KyberCiphertext v_CIPHERTEXT_SIZE) : array u8 (sz 32) = diff --git a/src/kem/kyber.rs b/src/kem/kyber.rs index cb326f165..e3b8fab93 100644 --- a/src/kem/kyber.rs +++ b/src/kem/kyber.rs @@ -94,8 +94,8 @@ pub(super) fn encapsulate< const T_AS_NTT_ENCODED_SIZE: usize, const C1_SIZE: usize, const C2_SIZE: usize, - const VECTOR_U_COMPRESSION_FACTOR: u32, - const VECTOR_V_COMPRESSION_FACTOR: u32, + const VECTOR_U_COMPRESSION_FACTOR: usize, + const VECTOR_V_COMPRESSION_FACTOR: usize, const VECTOR_U_BLOCK_LEN: usize, >( public_key: &KyberPublicKey, @@ -148,8 +148,8 @@ pub(super) fn decapsulate< const T_AS_NTT_ENCODED_SIZE: usize, const C1_SIZE: usize, const C2_SIZE: usize, - const VECTOR_U_COMPRESSION_FACTOR: u32, - const VECTOR_V_COMPRESSION_FACTOR: u32, + const VECTOR_U_COMPRESSION_FACTOR: usize, + const VECTOR_V_COMPRESSION_FACTOR: usize, const C1_BLOCK_SIZE: usize, >( secret_key: &KyberPrivateKey, diff --git a/src/kem/kyber/compress.rs b/src/kem/kyber/compress.rs index 4b9e5bdb1..d151affd6 100644 --- a/src/kem/kyber/compress.rs +++ b/src/kem/kyber/compress.rs @@ -4,7 +4,7 @@ use super::{ conversions::to_unsigned_representative, }; -pub fn compress( +pub fn compress( mut re: KyberPolynomialRingElement, ) -> KyberPolynomialRingElement { re.coefficients = re @@ -23,8 +23,8 @@ pub fn decompress( re } -fn compress_q(fe: u16) -> KyberFieldElement { - debug_assert!(COEFFICIENT_BITS as usize <= BITS_PER_COEFFICIENT); +fn compress_q(fe: u16) -> KyberFieldElement { + debug_assert!(COEFFICIENT_BITS <= BITS_PER_COEFFICIENT); let two_pow_bit_size = 1u32 << COEFFICIENT_BITS; diff --git a/src/kem/kyber/ind_cpa.rs b/src/kem/kyber/ind_cpa.rs index 3be002332..784b03394 100644 --- a/src/kem/kyber/ind_cpa.rs +++ b/src/kem/kyber/ind_cpa.rs @@ -184,7 +184,7 @@ pub fn serialize_secret_key( fn compress_then_encode_u< const K: usize, const OUT_LEN: usize, - const COMPRESSION_FACTOR: u32, + const COMPRESSION_FACTOR: usize, const BLOCK_LEN: usize, >( input: [KyberPolynomialRingElement; K], @@ -208,8 +208,8 @@ pub(crate) fn encrypt< const T_AS_NTT_ENCODED_SIZE: usize, const C1_LEN: usize, const C2_LEN: usize, - const VECTOR_U_COMPRESSION_FACTOR: u32, - const VECTOR_V_COMPRESSION_FACTOR: u32, + const VECTOR_U_COMPRESSION_FACTOR: usize, + const VECTOR_V_COMPRESSION_FACTOR: usize, const BLOCK_LEN: usize, >( public_key: &[u8], @@ -295,8 +295,8 @@ pub(crate) fn decrypt< const K: usize, const CIPHERTEXT_SIZE: usize, const VECTOR_U_ENCODED_SIZE: usize, - const VECTOR_U_COMPRESSION_FACTOR: u32, - const VECTOR_V_COMPRESSION_FACTOR: u32, + const VECTOR_U_COMPRESSION_FACTOR: usize, + const VECTOR_V_COMPRESSION_FACTOR: usize, >( secret_key: &[u8], ciphertext: &super::KyberCiphertext, @@ -306,7 +306,7 @@ pub(crate) fn decrypt< // u := Decompress_q(Decode_{d_u}(c), d_u) for (i, u_bytes) in ciphertext[..VECTOR_U_ENCODED_SIZE] - .chunks_exact((COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR as usize) / 8) + .chunks_exact((COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR) / 8) .enumerate() { let u = deserialize_little_endian::(u_bytes); @@ -318,7 +318,7 @@ pub(crate) fn decrypt< deserialize_little_endian::( &ciphertext[VECTOR_U_ENCODED_SIZE..], ), - VECTOR_V_COMPRESSION_FACTOR as usize, + VECTOR_V_COMPRESSION_FACTOR, ); // sˆ := Decode_12(sk) diff --git a/src/kem/kyber/kyber1024.rs b/src/kem/kyber/kyber1024.rs index 058790ada..b64ce3f18 100644 --- a/src/kem/kyber/kyber1024.rs +++ b/src/kem/kyber/kyber1024.rs @@ -5,19 +5,18 @@ const RANK_1024: usize = 4; const RANKED_BYTES_PER_RING_ELEMENT_1024: usize = RANK_1024 * BITS_PER_RING_ELEMENT / 8; const T_AS_NTT_ENCODED_SIZE_1024: usize = (RANK_1024 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; -const VECTOR_U_COMPRESSION_FACTOR_1024: u32 = 11; +const VECTOR_U_COMPRESSION_FACTOR_1024: usize = 11; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::(); const C1_BLOCK_SIZE_1024: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_1024 as usize) / 8; + (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_1024) / 8; // [hax]: hacspec/hacspec-v2#27 stealing error // serialized_len::(); const C1_SIZE_1024: usize = C1_BLOCK_SIZE_1024 * RANK_1024; -const VECTOR_V_COMPRESSION_FACTOR_1024: u32 = 5; +const VECTOR_V_COMPRESSION_FACTOR_1024: usize = 5; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::() -const C2_SIZE_1024: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_1024 as usize) / 8; +const C2_SIZE_1024: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_1024) / 8; const CPA_PKE_SECRET_KEY_SIZE_1024: usize = (RANK_1024 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; const CPA_PKE_PUBLIC_KEY_SIZE_1024: usize = T_AS_NTT_ENCODED_SIZE_1024 + 32; diff --git a/src/kem/kyber/kyber512.rs b/src/kem/kyber/kyber512.rs index 3e915087e..6b8ba060b 100644 --- a/src/kem/kyber/kyber512.rs +++ b/src/kem/kyber/kyber512.rs @@ -5,19 +5,18 @@ const RANK_512: usize = 2; const RANKED_BYTES_PER_RING_ELEMENT_512: usize = RANK_512 * BITS_PER_RING_ELEMENT / 8; const T_AS_NTT_ENCODED_SIZE_512: usize = (RANK_512 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; -const VECTOR_U_COMPRESSION_FACTOR_512: u32 = 10; +const VECTOR_U_COMPRESSION_FACTOR_512: usize = 10; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::() const C1_BLOCK_SIZE_512: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_512 as usize) / 8; + (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_512) / 8; // [hax]: hacspec/hacspec-v2#27 stealing error // serialized_len::() const C1_SIZE_512: usize = C1_BLOCK_SIZE_512 * RANK_512; -const VECTOR_V_COMPRESSION_FACTOR_512: u32 = 4; +const VECTOR_V_COMPRESSION_FACTOR_512: usize = 4; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::() -const C2_SIZE_512: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_512 as usize) / 8; +const C2_SIZE_512: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_512) / 8; const CPA_PKE_SECRET_KEY_SIZE_512: usize = (RANK_512 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; const CPA_PKE_PUBLIC_KEY_SIZE_512: usize = T_AS_NTT_ENCODED_SIZE_512 + 32; diff --git a/src/kem/kyber/kyber768.rs b/src/kem/kyber/kyber768.rs index fa8b5e42a..19f0a252e 100644 --- a/src/kem/kyber/kyber768.rs +++ b/src/kem/kyber/kyber768.rs @@ -5,19 +5,18 @@ const RANK_768: usize = 3; const RANKED_BYTES_PER_RING_ELEMENT_768: usize = RANK_768 * BITS_PER_RING_ELEMENT / 8; const T_AS_NTT_ENCODED_SIZE_768: usize = (RANK_768 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; -const VECTOR_U_COMPRESSION_FACTOR_768: u32 = 10; +const VECTOR_U_COMPRESSION_FACTOR_768: usize = 10; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::() const C1_BLOCK_SIZE_768: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_768 as usize) / 8; + (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_U_COMPRESSION_FACTOR_768) / 8; // [hax]: hacspec/hacspec-v2#27 stealing error // serialized_len::(); const C1_SIZE_768: usize = C1_BLOCK_SIZE_768 * RANK_768; -const VECTOR_V_COMPRESSION_FACTOR_768: u32 = 4; +const VECTOR_V_COMPRESSION_FACTOR_768: usize = 4; // [hax]: hacspec/hacspec-v2#27 stealing error // block_len::() -const C2_SIZE_768: usize = - (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_768 as usize) / 8; +const C2_SIZE_768: usize = (COEFFICIENTS_IN_RING_ELEMENT * VECTOR_V_COMPRESSION_FACTOR_768) / 8; const CPA_PKE_SECRET_KEY_SIZE_768: usize = (RANK_768 * COEFFICIENTS_IN_RING_ELEMENT * BITS_PER_COEFFICIENT) / 8; const CPA_PKE_PUBLIC_KEY_SIZE_768: usize = T_AS_NTT_ENCODED_SIZE_768 + 32; diff --git a/src/kem/kyber/serialize.rs b/src/kem/kyber/serialize.rs index f526ad6ac..4eaf243f6 100644 --- a/src/kem/kyber/serialize.rs +++ b/src/kem/kyber/serialize.rs @@ -1,7 +1,3 @@ -//! (De)serialization -//! -//! [hax] due to limitations of `usize`, the compression factor is a `u32` for now. -//! https://github.com/hacspec/hacspec-v2/pull/274 use super::{ arithmetic::{KyberFieldElement, KyberPolynomialRingElement}, constants::{BYTES_PER_RING_ELEMENT, COEFFICIENTS_IN_RING_ELEMENT}, @@ -45,17 +41,17 @@ use super::{ /// is called, and `compress_q` also performs this conversion. #[inline(always)] -pub(super) fn serialize_little_endian( +pub(super) fn serialize_little_endian( re: KyberPolynomialRingElement, ) -> [u8; OUT_LEN] { debug_assert!( - (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR as usize) / 8 == OUT_LEN, + (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR) / 8 == OUT_LEN, "{} != {}", - (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR as usize) / 8, + (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR) / 8, OUT_LEN ); - match COMPRESSION_FACTOR { + match COMPRESSION_FACTOR as u32 { 1 => serialize_little_endian_1(re), // VECTOR_V_COMPRESSION_FACTOR_768 & VECTOR_V_COMPRESSION_FACTOR_512 4 => serialize_little_endian_4(re), @@ -71,15 +67,15 @@ pub(super) fn serialize_little_endian( +pub(super) fn deserialize_little_endian( serialized: &[u8], ) -> KyberPolynomialRingElement { debug_assert_eq!( serialized.len(), - (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR as usize) / 8 + (COEFFICIENTS_IN_RING_ELEMENT * COMPRESSION_FACTOR) / 8 ); - match COMPRESSION_FACTOR { + match COMPRESSION_FACTOR as u32 { 1 => deserialize_little_endian_1(serialized), // VECTOR_V_COMPRESSION_FACTOR_768 & VECTOR_V_COMPRESSION_FACTOR_512 4 => deserialize_little_endian_4(serialized),