smaller change

cryspen · Oct 10, 2023 · b8e7179 · b8e7179
1 parent 638c2d9
commit b8e7179
Show file tree

Hide file tree

Showing 14 changed files with 65 additions and 92 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -3,17 +3,15 @@ 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 =
     if true
     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,16 +82,15 @@ 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
     then
       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
@@ -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
@@ -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<PUBLIC_KEY_SIZE>,
@@ -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<SECRET_KEY_SIZE>,

diff --git 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<const COEFFICIENT_BITS: u32>(
+pub fn compress<const COEFFICIENT_BITS: usize>(
     mut re: KyberPolynomialRingElement,
 ) -> KyberPolynomialRingElement {
     re.coefficients = re
@@ -23,8 +23,8 @@ pub fn decompress(
     re
 }
 
-fn compress_q<const COEFFICIENT_BITS: u32>(fe: u16) -> KyberFieldElement {
-    debug_assert!(COEFFICIENT_BITS as usize <= BITS_PER_COEFFICIENT);
+fn compress_q<const COEFFICIENT_BITS: usize>(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
@@ -184,7 +184,7 @@ pub fn serialize_secret_key<const SERIALIZED_KEY_LEN: usize>(
 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<CIPHERTEXT_SIZE>,
@@ -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::<VECTOR_U_COMPRESSION_FACTOR>(u_bytes);
@@ -318,7 +318,7 @@ pub(crate) fn decrypt<
         deserialize_little_endian::<VECTOR_V_COMPRESSION_FACTOR>(
             &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
@@ -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::<VECTOR_U_COMPRESSION_FACTOR_1024>();
 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::<RANK_1024, C1_BLOCK_SIZE_1024>();
 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::<VECTOR_V_COMPRESSION_FACTOR_1024>()
-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
@@ -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::<VECTOR_U_COMPRESSION_FACTOR_512>()
 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::<RANK_512, C1_BLOCK_SIZE_512>()
 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::<VECTOR_V_COMPRESSION_FACTOR_512>()
-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;