Add conditions for generic compress and serialize functions

cryspen · Sep 17, 2024 · fa71b36 · fa71b36
1 parent a94aed7
commit fa71b36
Show file tree

Hide file tree

Showing 5 changed files with 188 additions and 52 deletions.
diff --git a/libcrux-ml-kem/src/serialize.rs b/libcrux-ml-kem/src/serialize.rs
@@ -2,17 +2,39 @@ use crate::{
     constants::{COEFFICIENTS_IN_RING_ELEMENT, BYTES_PER_RING_ELEMENT, SHARED_SECRET_SIZE},
     helper::cloop,
     polynomial::{PolynomialRingElement, VECTORS_IN_RING_ELEMENT},
-    vector::{decompress_1, to_unsigned_representative, Operations},
+    vector::{decompress_1, to_unsigned_representative, Operations, FIELD_MODULUS},
 };
 
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
+#[hax_lib::requires(fstar!("forall (i:nat). i < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $a) i) < v $FIELD_MODULUS"))]
+#[hax_lib::ensures(|result| fstar!("forall (i:nat). i < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $result) i) >= 0 /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array $result) i) < v $FIELD_MODULUS"))]
+pub(super) fn to_unsigned_field_modulus<Vector: Operations>(
+    a: Vector,
+) -> Vector {
+    to_unsigned_representative::<Vector>(a)
+}
+
+#[inline(always)]
+#[hax_lib::fstar::verification_status(panic_free)]
+#[hax_lib::requires(fstar!("forall (i:nat). i < 16 ==>
+    (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS)"))]
 pub(super) fn compress_then_serialize_message<Vector: Operations>(
     re: PolynomialRingElement<Vector>,
 ) -> [u8; SHARED_SECRET_SIZE] {
     let mut serialized = [0u8; SHARED_SECRET_SIZE];
     for i in 0..16 {
-        let coefficient = to_unsigned_representative::<Vector>(re.coefficients[i]);
+        hax_lib::loop_invariant!(|i: usize| { fstar!("v $i < 16 ==> (forall (j:nat). j < 16 ==>
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) >= -(v $FIELD_MODULUS) /\\
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) < v $FIELD_MODULUS)") });
+        hax_lib::fstar!("assert (2 * v $i + 2 <= 32)");
+        let coefficient = to_unsigned_field_modulus(re.coefficients[i]);
         let coefficient_compressed = Vector::compress_1(coefficient);
 
         let bytes = Vector::serialize_1(coefficient_compressed);
@@ -34,13 +56,23 @@ pub(super) fn deserialize_then_decompress_message<Vector: Operations>(
 }
 
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
+#[hax_lib::fstar::verification_status(panic_free)]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
+#[hax_lib::requires(fstar!("forall (i:nat). i < 16 ==>
+    (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS)"))]
 pub(super) fn serialize_uncompressed_ring_element<Vector: Operations>(
     re: &PolynomialRingElement<Vector>,
 ) -> [u8; BYTES_PER_RING_ELEMENT] {
+    hax_lib::fstar!("assert_norm (pow2 12 == 4096)");
     let mut serialized = [0u8; BYTES_PER_RING_ELEMENT];
     for i in 0..VECTORS_IN_RING_ELEMENT {
-        let coefficient = to_unsigned_representative::<Vector>(re.coefficients[i]);
+        hax_lib::loop_invariant!(|i: usize| { fstar!("v $i >= 0 /\\ v $i <= 16 /\\ (v $i < 16 ==> (forall (j:nat). j < 16 ==>
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) >= -(v $FIELD_MODULUS) /\\
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) < v $FIELD_MODULUS))") });
+        hax_lib::fstar!("assert (24 * v $i + 24 <= 384)");
+        let coefficient = to_unsigned_field_modulus(re.coefficients[i]);
 
         let bytes = Vector::serialize_12(coefficient);
         serialized[24 * i..24 * i + 24].copy_from_slice(&bytes);
@@ -117,17 +149,24 @@ pub(super) fn deserialize_ring_elements_reduced<
 }
 
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
-#[hax_lib::requires(
-    OUT_LEN == 320
-)]
+#[hax_lib::fstar::verification_status(panic_free)]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
+#[hax_lib::requires(fstar!("v $OUT_LEN == 320 /\\ (forall (i:nat). i < 16 ==>
+    (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS))"))]
 fn compress_then_serialize_10<const OUT_LEN: usize, Vector: Operations>(
     re: &PolynomialRingElement<Vector>,
 ) -> [u8; OUT_LEN] {
+    hax_lib::fstar!("assert_norm (pow2 10 == 1024)");
     let mut serialized = [0u8; OUT_LEN];
     for i in 0..VECTORS_IN_RING_ELEMENT {
+        hax_lib::loop_invariant!(|i: usize| { fstar!("v $i >= 0 /\\ v $i <= 16 /\\ (v $i < 16 ==> (forall (j:nat). j < 16 ==>
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) >= -(v $FIELD_MODULUS) /\\
+            v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) < v $FIELD_MODULUS))") });
+        hax_lib::fstar!("assert (20 * v $i + 20 <= 320)");
         let coefficient =
-            Vector::compress::<10>(to_unsigned_representative::<Vector>(re.coefficients[i]));
+            Vector::compress::<10>(to_unsigned_field_modulus(re.coefficients[i]));
 
         let bytes = Vector::serialize_10(coefficient);
         serialized[20 * i..20 * i + 20].copy_from_slice(&bytes);
@@ -137,9 +176,6 @@ fn compress_then_serialize_10<const OUT_LEN: usize, Vector: Operations>(
 
 #[inline(always)]
 #[hax_lib::fstar::verification_status(lax)]
-#[hax_lib::requires(
-    OUT_LEN == 352
-)]
 fn compress_then_serialize_11<const OUT_LEN: usize, Vector: Operations>(
     re: &PolynomialRingElement<Vector>,
 ) -> [u8; OUT_LEN] {
@@ -155,10 +191,11 @@ fn compress_then_serialize_11<const OUT_LEN: usize, Vector: Operations>(
 }
 
 #[inline(always)]
-#[hax_lib::requires(
-    (COMPRESSION_FACTOR == 10 || COMPRESSION_FACTOR == 11) &&
-    OUT_LEN == 32 * COMPRESSION_FACTOR
-)]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
+#[hax_lib::requires(fstar!("(v $COMPRESSION_FACTOR == 10 \\/ v $COMPRESSION_FACTOR == 11) /\\ v $OUT_LEN == 32 * v $COMPRESSION_FACTOR /\\
+    (forall (i:nat). i < 16 ==> (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS))"))]
 pub(super) fn compress_then_serialize_ring_element_u<
     const COMPRESSION_FACTOR: usize,
     const OUT_LEN: usize,
@@ -168,7 +205,8 @@ pub(super) fn compress_then_serialize_ring_element_u<
 ) -> [u8; OUT_LEN] {
     hax_lib::fstar!("assert (
         (v (cast $COMPRESSION_FACTOR <: u32) == 10) \\/
-        (v (cast $COMPRESSION_FACTOR <: u32) == 11))");
+        (v (cast $COMPRESSION_FACTOR <: u32) == 11));
+        Rust_primitives.Integers.mk_int_equiv_lemma #usize_inttype (v $COMPRESSION_FACTOR)");
     match COMPRESSION_FACTOR as u32 {
         10 => compress_then_serialize_10(re),
         11 => compress_then_serialize_11(re),
@@ -177,21 +215,29 @@ pub(super) fn compress_then_serialize_ring_element_u<
 }
 
 #[inline(always)]
-#[hax_lib::fstar::verification_status(lax)]
-#[hax_lib::requires(
-    serialized.len() == 128
-)]
+#[hax_lib::fstar::verification_status(panic_free)]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
+#[hax_lib::requires(fstar!("Seq.length $serialized == 128 /\\ (forall (i:nat). i < 16 ==>
+    (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS))"))]
 fn compress_then_serialize_4<Vector: Operations>(
     re: PolynomialRingElement<Vector>,
     serialized: &mut [u8],
 ) {
+    hax_lib::fstar!("assert_norm (pow2 4 == 16)");
     let _serialized_len = serialized.len();
     // The semicolon and parentheses at the end of loop are a workaround
     // for the following bug https://github.com/hacspec/hax/issues/720
     for i in 0..VECTORS_IN_RING_ELEMENT {
-        hax_lib::loop_invariant!(|i: usize| serialized.len() == _serialized_len);
+        // NOTE: Using `$serialized` in loop_invariant doesn't work here
+        hax_lib::loop_invariant!(|i: usize| { fstar!("v $i >= 0 /\\ v $i <= 16 /\\
+            Seq.length serialized == v $_serialized_len /\\ (v $i < 16 ==> (forall (j:nat). j < 16 ==>
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) >= -(v $FIELD_MODULUS) /\\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[i]) j) < v $FIELD_MODULUS))") });
+        hax_lib::fstar!("assert (8 * v $i + 8 <= 128)");
         let coefficient =
-            Vector::compress::<4>(to_unsigned_representative::<Vector>(re.coefficients[i]));
+            Vector::compress::<4>(to_unsigned_field_modulus(re.coefficients[i]));
 
         let bytes = Vector::serialize_4(coefficient);
         serialized[8 * i..8 * i + 8].copy_from_slice(&bytes);
@@ -223,11 +269,11 @@ fn compress_then_serialize_5<Vector: Operations>(
 }
 
 #[inline(always)]
-#[hax_lib::requires(
-    (COMPRESSION_FACTOR == 4 || COMPRESSION_FACTOR == 5) &&
-    OUT_LEN == 32 * COMPRESSION_FACTOR &&
-    out.len() == OUT_LEN
-)]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 500")]
+#[hax_lib::requires(fstar!("(v $COMPRESSION_FACTOR == 4 \\/ v $COMPRESSION_FACTOR == 5) /\\ v $OUT_LEN == 32 * v $COMPRESSION_FACTOR /\\
+    Seq.length $out == v $OUT_LEN /\\ (forall (i:nat). i < 16 ==> (forall (j:nat). j < 16 ==>
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) >= -(v $FIELD_MODULUS) /\\
+    v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array ${re.coefficients}.[sz i]) j) < v $FIELD_MODULUS))"))]
 #[hax_lib::ensures(|_|
     fstar!("${out_future.len()} == ${out.len()}")
 )]
@@ -241,7 +287,8 @@ pub(super) fn compress_then_serialize_ring_element_v<
 ) {
     hax_lib::fstar!("assert (
         (v (cast $COMPRESSION_FACTOR <: u32) == 4) \\/
-        (v (cast $COMPRESSION_FACTOR <: u32) == 5))");
+        (v (cast $COMPRESSION_FACTOR <: u32) == 5));
+        Rust_primitives.Integers.mk_int_equiv_lemma #usize_inttype (v $COMPRESSION_FACTOR)");
     match COMPRESSION_FACTOR as u32 {
         4 => compress_then_serialize_4(re, out),
         5 => compress_then_serialize_5(re, out),

diff --git a/libcrux-ml-kem/src/vector/avx2.rs b/libcrux-ml-kem/src/vector/avx2.rs
@@ -7,6 +7,8 @@ mod ntt;
 mod sampling;
 mod serialize;
 
+use crate::vector::FIELD_MODULUS;
+
 #[derive(Clone, Copy)]
 #[hax_lib::fstar::before(interface,"noeq")]
 #[hax_lib::fstar::after(interface,"let repr (x:t_SIMD256Vector) : t_Array i16 (sz 16) = Libcrux_intrinsics.Avx2_extract.vec256_as_i16x16 x.f_elements")]
@@ -127,15 +129,29 @@ impl Operations for SIMD256Vector {
         }
     }
 
+    #[requires(fstar!("forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\\
+        v (Seq.index (impl.f_repr $vector) i) < v $FIELD_MODULUS"))]
+    #[ensures(|out| fstar!("forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) 1"))]
     fn compress_1(vector: Self) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: compress::compress_message_coefficient(vector.elements),
         }
     }
 
-    #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||
-        COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)]
+    #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+            v $COEFFICIENT_BITS == 5 \\/
+            v $COEFFICIENT_BITS == 10 \\/
+            v $COEFFICIENT_BITS == 11) /\\
+        (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $vector) i) >= 0 /\\
+            v (Seq.index (impl.f_repr $vector) i) < v $FIELD_MODULUS)"))]
+    #[ensures(|out| fstar!("(v $COEFFICIENT_BITS == 4 \\/
+            v $COEFFICIENT_BITS == 5 \\/
+            v $COEFFICIENT_BITS == 10 \\/
+            v $COEFFICIENT_BITS == 11) ==>
+                (forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) (v $COEFFICIENT_BITS))"))]
     fn compress<const COEFFICIENT_BITS: i32>(vector: Self) -> Self {
+        hax_lib::fstar!("admit()");
         Self {
             elements: compress::compress_ciphertext_coefficient::<COEFFICIENT_BITS>(
                 vector.elements,

diff --git a/libcrux-ml-kem/src/vector/portable.rs b/libcrux-ml-kem/src/vector/portable.rs
@@ -15,6 +15,8 @@ use vector_type::*;
 
 pub(crate) use vector_type::PortableVector;
 
+use crate::vector::FIELD_MODULUS;
+
 #[cfg(hax)]
 impl crate::vector::traits::Repr for PortableVector {
     fn repr(x: Self) -> [i16; 16] {
@@ -83,14 +85,26 @@ impl Operations for PortableVector {
         montgomery_multiply_by_constant(v, r)
     }
 
-    fn compress_1(v: Self) -> Self {
-        compress_1(v)
-    }
-
-    #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||
-               COEFFICIENT_BITS == 10 || COEFFICIENT_BITS == 11)]
-    fn compress<const COEFFICIENT_BITS: i32>(v: Self) -> Self {
-        compress::<COEFFICIENT_BITS>(v)
+    #[requires(fstar!("forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\
+        v (Seq.index (impl.f_repr $a) i) < v $FIELD_MODULUS"))]
+    #[ensures(|out| fstar!("forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) 1"))]
+    fn compress_1(a: Self) -> Self {
+        compress_1(a)
+    }
+
+    #[requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+            v $COEFFICIENT_BITS == 5 \\/
+            v $COEFFICIENT_BITS == 10 \\/
+            v $COEFFICIENT_BITS == 11) /\\
+        (forall (i:nat). i < 16 ==> v (Seq.index (impl.f_repr $a) i) >= 0 /\\
+            v (Seq.index (impl.f_repr $a) i) < v $FIELD_MODULUS)"))]
+    #[ensures(|out| fstar!("(v $COEFFICIENT_BITS == 4 \\/
+            v $COEFFICIENT_BITS == 5 \\/
+            v $COEFFICIENT_BITS == 10 \\/
+            v $COEFFICIENT_BITS == 11) ==>
+                (forall (i:nat). i < 16 ==> bounded (Seq.index (impl.f_repr $out) i) (v $COEFFICIENT_BITS))"))]
+    fn compress<const COEFFICIENT_BITS: i32>(a: Self) -> Self {
+        compress::<COEFFICIENT_BITS>(a)
     }
 
     #[requires(COEFFICIENT_BITS == 4 || COEFFICIENT_BITS == 5 ||

diff --git a/libcrux-ml-kem/src/vector/portable/compress.rs b/libcrux-ml-kem/src/vector/portable/compress.rs
@@ -84,21 +84,66 @@ pub(crate) fn compress_ciphertext_coefficient(coefficient_bits: u8, fe: u16) ->
 }
 
 #[inline(always)]
-pub(crate) fn compress_1(mut v: PortableVector) -> PortableVector {
+#[cfg_attr(hax, hax_lib::fstar::before("
+let compress_message_coefficient_range_helper (fe: u16) : Lemma
+  (requires fe <. (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) <: u16))
+  (ensures v (cast (compress_message_coefficient fe) <: i16) >= 0 /\\
+    v (cast (compress_message_coefficient fe) <: i16) < 2) =
+  assert (v (cast (compress_message_coefficient fe) <: i16) >= 0 /\\
+    v (cast (compress_message_coefficient fe) <: i16) < 2)
+"))]
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 2000")]
+#[hax_lib::requires(fstar!("forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\\
+    v (Seq.index ${a}.f_elements i) < v $FIELD_MODULUS"))]
+#[hax_lib::ensures(|result| fstar!("forall (i:nat). i < 16 ==> v (${result}.f_elements.[ sz i ] <: i16) >= 0 /\\
+    v (${result}.f_elements.[ sz i ] <: i16) < 2"))]
+pub(crate) fn compress_1(mut a: PortableVector) -> PortableVector {
+    hax_lib::fstar!("assert (forall (i:nat). i < 16 ==> (cast (${a}.f_elements.[ sz i ]) <: u16) <.
+        (cast ($FIELD_MODULUS) <: u16))");
     for i in 0..FIELD_ELEMENTS_IN_VECTOR {
-        v.elements[i] = compress_message_coefficient(v.elements[i] as u16) as i16;
+        hax_lib::loop_invariant!(|i: usize| { fstar!("(v $i < 16 ==> (forall (j:nat). (j >= v $i /\\ j < 16) ==>
+            v (cast (${a}.f_elements.[ sz j ]) <: u16) < v (cast ($FIELD_MODULUS) <: u16))) /\\
+            (forall (j:nat). j < v $i ==> v (${a}.f_elements.[ sz j ] <: i16) >= 0 /\\
+                v (${a}.f_elements.[ sz j ] <: i16) < 2)") });
+        hax_lib::fstar!("compress_message_coefficient_range_helper (cast (${a}.f_elements.[ $i ]) <: u16)");
+        a.elements[i] = compress_message_coefficient(a.elements[i] as u16) as i16;
+        hax_lib::fstar!("assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\\
+            v (${a}.f_elements.[ $i ] <: i16) < 2)");
     }
 
-    v
+    hax_lib::fstar!("assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\\
+        v (${a}.f_elements.[ sz i ] <: i16) < 2)");
+    a
 }
 
 #[inline(always)]
-pub(crate) fn compress<const COEFFICIENT_BITS: i32>(mut v: PortableVector) -> PortableVector {
+#[hax_lib::fstar::options("--fuel 0 --ifuel 0 --z3rlimit 2000")]
+#[hax_lib::requires(fstar!("(v $COEFFICIENT_BITS == 4 \\/
+        v $COEFFICIENT_BITS == 5 \\/
+        v $COEFFICIENT_BITS == 10 \\/
+        v $COEFFICIENT_BITS == 11) /\\
+    (forall (i:nat). i < 16 ==> v (Seq.index ${a}.f_elements i) >= 0 /\\
+        v (Seq.index ${a}.f_elements i) < v $FIELD_MODULUS)"))]
+#[hax_lib::ensures(|result| fstar!("forall (i:nat). i < 16 ==> v (${result}.f_elements.[ sz i ] <: i16) >= 0 /\\
+    v (${result}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))"))]
+pub(crate) fn compress<const COEFFICIENT_BITS: i32>(mut a: PortableVector) -> PortableVector {
+    hax_lib::fstar!("assert (v (cast ($COEFFICIENT_BITS) <: u8) == v $COEFFICIENT_BITS);
+        assert (v (cast ($COEFFICIENT_BITS) <: u32) == v $COEFFICIENT_BITS)");
+    hax_lib::fstar!("assert (forall (i:nat). i < 16 ==> (cast (${a}.f_elements.[ sz i ]) <: u16) <.
+        (cast ($FIELD_MODULUS) <: u16))");
     for i in 0..FIELD_ELEMENTS_IN_VECTOR {
-        v.elements[i] =
-            compress_ciphertext_coefficient(COEFFICIENT_BITS as u8, v.elements[i] as u16) as i16;
+        hax_lib::loop_invariant!(|i: usize| { fstar!("(v $i < 16 ==> (forall (j:nat). (j >= v $i /\\ j < 16) ==>
+            v (cast (${a}.f_elements.[ sz j ]) <: u16) < v (cast ($FIELD_MODULUS) <: u16))) /\\
+            (forall (j:nat). j < v $i ==> v (${a}.f_elements.[ sz j ] <: i16) >= 0 /\\
+                v (${a}.f_elements.[ sz j ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))") });
+        a.elements[i] =
+            compress_ciphertext_coefficient(COEFFICIENT_BITS as u8, a.elements[i] as u16) as i16;
+        hax_lib::fstar!("assert (v (${a}.f_elements.[ $i ] <: i16) >= 0 /\\
+            v (${a}.f_elements.[ $i ] <: i16) < pow2 (v (cast ($COEFFICIENT_BITS) <: u32)))");
     }
-    v
+    hax_lib::fstar!("assert (forall (i:nat). i < 16 ==> v (${a}.f_elements.[ sz i ] <: i16) >= 0 /\\
+        v (${a}.f_elements.[ sz i ] <: i16) < pow2 (v $COEFFICIENT_BITS))");
+    a
 }
 
 #[inline(always)]