Removed one TODO in NTT.

cryspen · Oct 27, 2023 · 9287a20 · 9287a20
1 parent 8aa11d2
commit 9287a20
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 4 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst
@@ -87,6 +87,28 @@ let decompress_q (#v_COEFFICIENT_BITS: usize) (fe: i32) : i32 =
   in
   let decompressed:u32 = (decompressed <<! 1l <: u32) +! (1ul <<! v_COEFFICIENT_BITS <: u32) in
   let decompressed:u32 = decompressed >>! (v_COEFFICIENT_BITS +! sz 1 <: usize) in
+  let _:Prims.unit =
+    if true
+    then
+      let _:Prims.unit =
+        if
+          ~.(decompressed <.
+            (Core.Result.impl__unwrap (Core.Convert.f_try_from Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+
+                  <:
+                  Core.Result.t_Result u32 Core.Num.Error.t_TryFromIntError)
+              <:
+              u32)
+            <:
+            bool)
+        then
+          Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: decompressed < u32::try_from(FIELD_MODULUS).unwrap()"
+
+              <:
+              Rust_primitives.Hax.t_Never)
+      in
+      ()
+  in
   cast decompressed <: i32
 
 let decompress

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Ntt.fst
@@ -682,7 +682,7 @@ let ntt_vector_u
       (#v_VECTOR_U_COMPRESSION_FACTOR: usize)
       (re: Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement)
     : Libcrux.Kem.Kyber.Arithmetic.t_KyberPolynomialRingElement =
-  let initial_coefficient_bound:i32 = 3329l in
+  let initial_coefficient_bound:i32 = 3328l in
   let _:Prims.unit =
     if true
     then

diff --git a/src/kem/kyber/compress.rs b/src/kem/kyber/compress.rs
@@ -34,6 +34,8 @@ pub(super) fn decompress_q<const COEFFICIENT_BITS: usize>(
     decompressed = (decompressed << 1) + (1 << COEFFICIENT_BITS);
     decompressed >>= COEFFICIENT_BITS + 1;
 
+    debug_assert!(decompressed < u32::try_from(FIELD_MODULUS).unwrap());
+
     decompressed as KyberFieldElement
 }
 pub fn decompress<const COEFFICIENT_BITS: usize>(

diff --git a/src/kem/kyber/ntt.rs b/src/kem/kyber/ntt.rs
@@ -88,9 +88,7 @@ pub(in crate::kem::kyber) fn ntt_binomially_sampled_ring_element(
 pub(in crate::kem::kyber) fn ntt_vector_u<const VECTOR_U_COMPRESSION_FACTOR: usize>(
     mut re: KyberPolynomialRingElement,
 ) -> KyberPolynomialRingElement {
-    // TODO: This could be tighter, but we have to analyze other functions
-    // first before we can say for sure here.
-    let initial_coefficient_bound = 3329;
+    let initial_coefficient_bound = 3328;
     debug_assert!(re
         .coefficients
         .into_iter()