diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst
index 0aff4b996..b30651d80 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fst
@@ -9,7 +9,18 @@ let _ =
   let open Libcrux_ml_kem.Vector.Traits in
   ()
 
-#push-options "--admit_smt_queries true"
+let to_unsigned_field_modulus
+      (#v_Vector: Type0)
+      (#[FStar.Tactics.Typeclasses.tcresolve ()]
+          i1:
+          Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
+      (a: v_Vector)
+     =
+  let result:v_Vector = Libcrux_ml_kem.Vector.Traits.to_unsigned_representative #v_Vector a in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
+
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
 
 let compress_then_serialize_10_
       (v_OUT_LEN: usize)
@@ -19,23 +30,37 @@ let compress_then_serialize_10_
           Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
      =
+  let _:Prims.unit = assert_norm (pow2 10 == 1024) in
   let serialized:t_Array u8 v_OUT_LEN = Rust_primitives.Hax.repeat 0uy v_OUT_LEN in
   let serialized:t_Array u8 v_OUT_LEN =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
       Libcrux_ml_kem.Polynomial.v_VECTORS_IN_RING_ELEMENT
-      (fun serialized temp_1_ ->
+      (fun serialized i ->
           let serialized:t_Array u8 v_OUT_LEN = serialized in
-          let _:usize = temp_1_ in
-          true)
+          let i:usize = i in
+          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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       serialized
       (fun serialized i ->
           let serialized:t_Array u8 v_OUT_LEN = serialized in
           let i:usize = i in
+          let _:Prims.unit = assert (20 * v i + 20 <= 320) in
           let coefficient:v_Vector =
             Libcrux_ml_kem.Vector.Traits.f_compress #v_Vector
               #FStar.Tactics.Typeclasses.solve
               10l
-              (Libcrux_ml_kem.Vector.Traits.to_unsigned_representative #v_Vector
+              (to_unsigned_field_modulus #v_Vector
                   (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: v_Vector)
                 <:
                 v_Vector)
@@ -68,7 +93,9 @@ let compress_then_serialize_10_
           in
           serialized)
   in
-  serialized
+  let result:t_Array u8 v_OUT_LEN = serialized in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 #pop-options
 
@@ -135,7 +162,7 @@ let compress_then_serialize_11_
 
 #pop-options
 
-#push-options "--admit_smt_queries true"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
 
 let compress_then_serialize_4_
       (#v_Vector: Type0)
@@ -145,6 +172,7 @@ let compress_then_serialize_4_
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (serialized: t_Slice u8)
      =
+  let _:Prims.unit = assert_norm (pow2 4 == 16) in
   let v__serialized_len:usize = Core.Slice.impl__len #u8 serialized in
   let serialized:t_Slice u8 =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
@@ -152,16 +180,29 @@ let compress_then_serialize_4_
       (fun serialized i ->
           let serialized:t_Slice u8 = serialized in
           let i:usize = i in
-          (Core.Slice.impl__len #u8 serialized <: usize) =. v__serialized_len <: bool)
+          v i >= 0 /\ v i <= 16 /\ Seq.length serialized == v v__serialized_len /\
+          (v i < 16 ==>
+            (forall (j: nat).
+                j < 16 ==>
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       serialized
       (fun serialized i ->
           let serialized:t_Slice u8 = serialized in
           let i:usize = i in
+          let _:Prims.unit = assert (8 * v i + 8 <= 128) in
           let coefficient:v_Vector =
             Libcrux_ml_kem.Vector.Traits.f_compress #v_Vector
               #FStar.Tactics.Typeclasses.solve
               4l
-              (Libcrux_ml_kem.Vector.Traits.to_unsigned_representative #v_Vector
+              (to_unsigned_field_modulus #v_Vector
                   (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: v_Vector)
                 <:
                 v_Vector)
@@ -194,7 +235,9 @@ let compress_then_serialize_4_
           in
           serialized)
   in
-  let hax_temp_output:Prims.unit = () <: Prims.unit in
+  let result:Prims.unit = () <: Prims.unit in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  let hax_temp_output:Prims.unit = result in
   serialized
 
 #pop-options
@@ -263,8 +306,6 @@ let compress_then_serialize_5_
 
 #pop-options
 
-#push-options "--admit_smt_queries true"
-
 let compress_then_serialize_message
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -276,16 +317,28 @@ let compress_then_serialize_message
   let serialized:t_Array u8 (sz 32) =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
       (sz 16)
-      (fun serialized temp_1_ ->
+      (fun serialized i ->
           let serialized:t_Array u8 (sz 32) = serialized in
-          let _:usize = temp_1_ in
-          true)
+          let i:usize = i in
+          v i < 16 ==>
+          (forall (j: nat).
+              j < 16 ==>
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                    j) >=
+              -
+              (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                    j) <
+              v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS))
       serialized
       (fun serialized i ->
           let serialized:t_Array u8 (sz 32) = serialized in
           let i:usize = i in
+          let _:Prims.unit = assert (2 * v i + 2 <= 32) in
           let coefficient:v_Vector =
-            Libcrux_ml_kem.Vector.Traits.to_unsigned_representative #v_Vector
+            to_unsigned_field_modulus #v_Vector
               (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: v_Vector)
           in
           let coefficient_compressed:v_Vector =
@@ -321,9 +374,11 @@ let compress_then_serialize_message
           in
           serialized)
   in
-  serialized
+  let result:t_Array u8 (sz 32) = serialized in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
-#pop-options
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
 
 let compress_then_serialize_ring_element_u
       (v_COMPRESSION_FACTOR v_OUT_LEN: usize)
@@ -335,7 +390,8 @@ let compress_then_serialize_ring_element_u
      =
   let _:Prims.unit =
     assert ((v (cast v_COMPRESSION_FACTOR <: u32) == 10) \/
-        (v (cast v_COMPRESSION_FACTOR <: u32) == 11))
+        (v (cast v_COMPRESSION_FACTOR <: u32) == 11));
+    Rust_primitives.Integers.mk_int_equiv_lemma #usize_inttype (v v_COMPRESSION_FACTOR)
   in
   match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with
   | 10ul -> compress_then_serialize_10_ v_OUT_LEN #v_Vector re
@@ -346,6 +402,10 @@ let compress_then_serialize_ring_element_u
         <:
         Rust_primitives.Hax.t_Never)
 
+#pop-options
+
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
+
 let compress_then_serialize_ring_element_v
       (v_COMPRESSION_FACTOR v_OUT_LEN: usize)
       (#v_Vector: Type0)
@@ -357,7 +417,8 @@ let compress_then_serialize_ring_element_v
      =
   let _:Prims.unit =
     assert ((v (cast v_COMPRESSION_FACTOR <: u32) == 4) \/
-        (v (cast v_COMPRESSION_FACTOR <: u32) == 5))
+        (v (cast v_COMPRESSION_FACTOR <: u32) == 5));
+    Rust_primitives.Integers.mk_int_equiv_lemma #usize_inttype (v v_COMPRESSION_FACTOR)
   in
   let out, hax_temp_output:(t_Slice u8 & Prims.unit) =
     match cast (v_COMPRESSION_FACTOR <: usize) <: u32 with
@@ -374,6 +435,8 @@ let compress_then_serialize_ring_element_v
   in
   out
 
+#pop-options
+
 let deserialize_then_decompress_10_
       (#v_Vector: Type0)
       (#[FStar.Tactics.Typeclasses.tcresolve ()]
@@ -821,7 +884,7 @@ let deserialize_to_uncompressed_ring_element
   in
   re
 
-#push-options "--admit_smt_queries true"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 500"
 
 let serialize_uncompressed_ring_element
       (#v_Vector: Type0)
@@ -830,20 +893,34 @@ let serialize_uncompressed_ring_element
           Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector)
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
      =
+  let _:Prims.unit = assert_norm (pow2 12 == 4096) in
   let serialized:t_Array u8 (sz 384) = Rust_primitives.Hax.repeat 0uy (sz 384) in
   let serialized:t_Array u8 (sz 384) =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
       Libcrux_ml_kem.Polynomial.v_VECTORS_IN_RING_ELEMENT
-      (fun serialized temp_1_ ->
+      (fun serialized i ->
           let serialized:t_Array u8 (sz 384) = serialized in
-          let _:usize = temp_1_ in
-          true)
+          let i:usize = i in
+          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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       serialized
       (fun serialized i ->
           let serialized:t_Array u8 (sz 384) = serialized in
           let i:usize = i in
+          let _:Prims.unit = assert (24 * v i + 24 <= 384) in
           let coefficient:v_Vector =
-            Libcrux_ml_kem.Vector.Traits.to_unsigned_representative #v_Vector
+            to_unsigned_field_modulus #v_Vector
               (re.Libcrux_ml_kem.Polynomial.f_coefficients.[ i ] <: v_Vector)
           in
           let bytes:t_Array u8 (sz 24) =
@@ -874,6 +951,8 @@ let serialize_uncompressed_ring_element
           in
           serialized)
   in
-  serialized
+  let result:t_Array u8 (sz 384) = serialized in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
 
 #pop-options
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
index c5c20e382..df1a37b01 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Serialize.fsti
@@ -9,19 +9,57 @@ let _ =
   let open Libcrux_ml_kem.Vector.Traits in
   ()
 
+val to_unsigned_field_modulus
+      (#v_Vector: Type0)
+      {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
+      (a: v_Vector)
+    : Prims.Pure v_Vector
+      (requires
+        forall (i: nat).
+          i < 16 ==>
+          v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) >=
+          -
+          (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+          v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array a) i) <
+          v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)
+      (ensures
+        fun result ->
+          let result:v_Vector = result in
+          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 Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)
+
 val compress_then_serialize_10_
       (v_OUT_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-    : Prims.Pure (t_Array u8 v_OUT_LEN) (requires v_OUT_LEN =. sz 320) (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array u8 v_OUT_LEN)
+      (requires
+        v 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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
+      (fun _ -> Prims.l_True)
 
 val compress_then_serialize_11_
       (v_OUT_LEN: usize)
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-    : Prims.Pure (t_Array u8 v_OUT_LEN) (requires v_OUT_LEN =. sz 352) (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)
 
 val compress_then_serialize_4_
       (#v_Vector: Type0)
@@ -29,7 +67,21 @@ val compress_then_serialize_4_
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
       (serialized: t_Slice u8)
     : Prims.Pure (t_Slice u8)
-      (requires (Core.Slice.impl__len #u8 serialized <: usize) =. sz 128)
+      (requires
+        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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       (fun _ -> Prims.l_True)
 
 val compress_then_serialize_5_
@@ -45,7 +97,22 @@ val compress_then_serialize_message
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-    : Prims.Pure (t_Array u8 (sz 32)) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array u8 (sz 32))
+      (requires
+        forall (i: nat).
+          i < 16 ==>
+          (forall (j: nat).
+              j < 16 ==>
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                    j) >=
+              -
+              (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                    j) <
+              v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS))
+      (fun _ -> Prims.l_True)
 
 val compress_then_serialize_ring_element_u
       (v_COMPRESSION_FACTOR v_OUT_LEN: usize)
@@ -54,8 +121,21 @@ val compress_then_serialize_ring_element_u
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
     : Prims.Pure (t_Array u8 v_OUT_LEN)
       (requires
-        (v_COMPRESSION_FACTOR =. sz 10 || v_COMPRESSION_FACTOR =. sz 11) &&
-        v_OUT_LEN =. (sz 32 *! v_COMPRESSION_FACTOR <: usize))
+        (v v_COMPRESSION_FACTOR == 10 \/ v v_COMPRESSION_FACTOR == 11) /\
+        v v_OUT_LEN == 32 * v 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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       (fun _ -> Prims.l_True)
 
 val compress_then_serialize_ring_element_v
@@ -66,9 +146,21 @@ val compress_then_serialize_ring_element_v
       (out: t_Slice u8)
     : Prims.Pure (t_Slice u8)
       (requires
-        (v_COMPRESSION_FACTOR =. sz 4 || v_COMPRESSION_FACTOR =. sz 5) &&
-        v_OUT_LEN =. (sz 32 *! v_COMPRESSION_FACTOR <: usize) &&
-        (Core.Slice.impl__len #u8 out <: usize) =. v_OUT_LEN)
+        (v v_COMPRESSION_FACTOR == 4 \/ v v_COMPRESSION_FACTOR == 5) /\
+        v v_OUT_LEN == 32 * v v_COMPRESSION_FACTOR /\ Seq.length out == v 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
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) >=
+                -
+                (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+                v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                            .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                      j) <
+                v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)))
       (ensures
         fun out_future ->
           let out_future:t_Slice u8 = out_future in
@@ -176,4 +268,19 @@ val serialize_uncompressed_ring_element
       (#v_Vector: Type0)
       {| i1: Libcrux_ml_kem.Vector.Traits.t_Operations v_Vector |}
       (re: Libcrux_ml_kem.Polynomial.t_PolynomialRingElement v_Vector)
-    : Prims.Pure (t_Array u8 (sz 384)) Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure (t_Array u8 (sz 384))
+      (requires
+        forall (i: nat).
+          i < 16 ==>
+          (forall (j: nat).
+              j < 16 ==>
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                    j) >=
+              -
+              (v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) /\
+              v (Seq.index (Libcrux_ml_kem.Vector.Traits.f_to_i16_array re
+                          .Libcrux_ml_kem.Polynomial.f_coefficients.[ sz i ])
+                    j) <
+              v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS))
+      (fun _ -> Prims.l_True)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
index 2aa6f7ab9..14a8a6489 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Avx2.fsti
@@ -177,11 +177,21 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
         }
         <:
         t_SIMD256Vector);
-    f_compress_1_pre = (fun (vector: t_SIMD256Vector) -> true);
-    f_compress_1_post = (fun (vector: t_SIMD256Vector) (out: t_SIMD256Vector) -> true);
+    f_compress_1_pre
+    =
+    (fun (vector: t_SIMD256Vector) ->
+        forall (i: nat).
+          i < 16 ==>
+          v (Seq.index (impl.f_repr vector) i) >= 0 /\
+          v (Seq.index (impl.f_repr vector) i) < v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS);
+    f_compress_1_post
+    =
+    (fun (vector: t_SIMD256Vector) (out: t_SIMD256Vector) ->
+        forall (i: nat). i < 16 ==> bounded (Seq.index (impl.f_repr out) i) 1);
     f_compress_1_
     =
     (fun (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         {
           f_elements
           =
@@ -192,14 +202,23 @@ let impl_3: Libcrux_ml_kem.Vector.Traits.t_Operations t_SIMD256Vector =
     f_compress_pre
     =
     (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) ->
-        v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-        v_COEFFICIENT_BITS =. 11l);
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v 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 Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS));
     f_compress_post
     =
-    (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) (out: t_SIMD256Vector) -> true);
+    (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) (out: t_SIMD256Vector) ->
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v v_COEFFICIENT_BITS == 11) ==>
+        (forall (i: nat). i < 16 ==> bounded (Seq.index (impl.f_repr out) i) (v v_COEFFICIENT_BITS))
+    );
     f_compress
     =
     (fun (v_COEFFICIENT_BITS: i32) (vector: t_SIMD256Vector) ->
+        let _:Prims.unit = admit () in
         {
           f_elements
           =
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fst
index 4a470d7d1..d8c5b91a8 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fst
@@ -22,78 +22,146 @@ let compress_message_coefficient (fe: u16) =
   let shifted_positive_in_range:i16 = shifted_to_positive -! 832s in
   cast ((shifted_positive_in_range >>! 15l <: i16) &. 1s <: i16) <: u8
 
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 2000"
+
 let compress
       (v_COEFFICIENT_BITS: i32)
-      (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+      (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
      =
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
+  let _:Prims.unit =
+    assert (v (cast (v_COEFFICIENT_BITS) <: u8) == v v_COEFFICIENT_BITS);
+    assert (v (cast (v_COEFFICIENT_BITS) <: u32) == v v_COEFFICIENT_BITS)
+  in
+  let _:Prims.unit =
+    assert (forall (i: nat).
+          i < 16 ==>
+          (cast (a.f_elements.[ sz i ]) <: u16) <.
+          (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) <: u16))
+  in
+  let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
       Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR
-      (fun v temp_1_ ->
-          let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = v in
-          let _:usize = temp_1_ in
-          true)
-      v
-      (fun v i ->
-          let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = v in
+      (fun a i ->
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = a in
+          let i:usize = i in
+          (v i < 16 ==>
+            (forall (j: nat).
+                (j >= v i /\ j < 16) ==>
+                v (cast (a.f_elements.[ sz j ]) <: u16) <
+                v (cast (Libcrux_ml_kem.Vector.Traits.v_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 (v_COEFFICIENT_BITS) <: u32))))
+      a
+      (fun a i ->
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = a in
           let i:usize = i in
-          {
-            v with
-            Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-            =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-                .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-              i
-              (compress_ciphertext_coefficient (cast (v_COEFFICIENT_BITS <: i32) <: u8)
-                  (cast (v.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ] <: i16)
-                    <:
-                    u16)
-                <:
-                i16)
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
+            {
+              a with
+              Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize a
+                  .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+                i
+                (compress_ciphertext_coefficient (cast (v_COEFFICIENT_BITS <: i32) <: u8)
+                    (cast (a.Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ] <: i16)
+                      <:
+                      u16)
+                  <:
+                  i16)
+            }
             <:
-            t_Array i16 (sz 16)
-          }
-          <:
-          Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+            Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+          in
+          let _:Prims.unit =
+            assert (v (a.f_elements.[ i ] <: i16) >= 0 /\
+                v (a.f_elements.[ i ] <: i16) < pow2 (v (cast (v_COEFFICIENT_BITS) <: u32)))
+          in
+          a)
   in
-  v
+  let _:Prims.unit =
+    assert (forall (i: nat).
+          i < 16 ==>
+          v (a.f_elements.[ sz i ] <: i16) >= 0 /\
+          v (a.f_elements.[ sz i ] <: i16) < pow2 (v v_COEFFICIENT_BITS))
+  in
+  a
 
-let compress_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
-  let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
+#pop-options
+
+#push-options "--fuel 0 --ifuel 0 --z3rlimit 2000"
+
+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)
+
+let compress_1_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) =
+  let _:Prims.unit =
+    assert (forall (i: nat).
+          i < 16 ==>
+          (cast (a.f_elements.[ sz i ]) <: u16) <.
+          (cast (Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS) <: u16))
+  in
+  let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
     Rust_primitives.Hax.Folds.fold_range (sz 0)
       Libcrux_ml_kem.Vector.Traits.v_FIELD_ELEMENTS_IN_VECTOR
-      (fun v temp_1_ ->
-          let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = v in
-          let _:usize = temp_1_ in
-          true)
-      v
-      (fun v i ->
-          let v:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = v in
+      (fun a i ->
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = a in
+          let i:usize = i in
+          (v i < 16 ==>
+            (forall (j: nat).
+                (j >= v i /\ j < 16) ==>
+                v (cast (a.f_elements.[ sz j ]) <: u16) <
+                v (cast (Libcrux_ml_kem.Vector.Traits.v_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))
+      a
+      (fun a i ->
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = a in
           let i:usize = i in
-          {
-            v with
-            Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-            =
-            Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v
-                .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
-              i
-              (cast (compress_message_coefficient (cast (v
-                              .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ]
-                            <:
-                            i16)
-                        <:
-                        u16)
-                    <:
-                    u8)
-                <:
-                i16)
+          let _:Prims.unit =
+            compress_message_coefficient_range_helper (cast (a.f_elements.[ i ]) <: u16)
+          in
+          let a:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
+            {
+              a with
+              Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+              =
+              Rust_primitives.Hax.Monomorphized_update_at.update_at_usize a
+                  .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements
+                i
+                (cast (compress_message_coefficient (cast (a
+                                .Libcrux_ml_kem.Vector.Portable.Vector_type.f_elements.[ i ]
+                              <:
+                              i16)
+                          <:
+                          u16)
+                      <:
+                      u8)
+                  <:
+                  i16)
+            }
             <:
-            t_Array i16 (sz 16)
-          }
-          <:
-          Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+            Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
+          in
+          let _:Prims.unit =
+            assert (v (a.f_elements.[ i ] <: i16) >= 0 /\ v (a.f_elements.[ i ] <: i16) < 2)
+          in
+          a)
   in
-  v
+  let _:Prims.unit =
+    assert (forall (i: nat).
+          i < 16 ==> v (a.f_elements.[ sz i ] <: i16) >= 0 /\ v (a.f_elements.[ sz i ] <: i16) < 2)
+  in
+  a
+
+#pop-options
 
 let decompress_ciphertext_coefficient
       (v_COEFFICIENT_BITS: i32)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fsti
index 8a078f1b0..57e5a0a1d 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.Compress.fsti
@@ -47,15 +47,36 @@ val compress_message_coefficient (fe: u16)
 
 val compress
       (v_COEFFICIENT_BITS: i32)
-      (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+      (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+      (requires
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v 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 Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS))
+      (ensures
+        fun result ->
+          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
+          forall (i: nat).
+            i < 16 ==>
+            v (result.f_elements.[ sz i ] <: i16) >= 0 /\
+            v (result.f_elements.[ sz i ] <: i16) < pow2 (v v_COEFFICIENT_BITS))
 
-val compress_1_ (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+val compress_1_ (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
     : Prims.Pure Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector
-      Prims.l_True
-      (fun _ -> Prims.l_True)
+      (requires
+        forall (i: nat).
+          i < 16 ==>
+          v (Seq.index a.f_elements i) >= 0 /\
+          v (Seq.index a.f_elements i) < v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS)
+      (ensures
+        fun result ->
+          let result:Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector = result in
+          forall (i: nat).
+            i < 16 ==>
+            v (result.f_elements.[ sz i ] <: i16) >= 0 /\ v (result.f_elements.[ sz i ] <: i16) < 2)
 
 val decompress_ciphertext_coefficient
       (v_COEFFICIENT_BITS: i32)
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst
new file mode 100644
index 000000000..dbd72c7e0
--- /dev/null
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fst
@@ -0,0 +1,15 @@
+module Libcrux_ml_kem.Vector.Portable
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let _ =
+  (* This module has implicit dependencies, here we make them explicit. *)
+  (* The implicit dependencies arise from typeclasses instances. *)
+  let open Libcrux_ml_kem.Vector.Portable.Vector_type in
+  let open Libcrux_ml_kem.Vector.Traits in
+  ()
+
+#push-options "--z3rlimit 300"
+
+#pop-options
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
index 461660a87..8f46599b2 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Portable.fsti
@@ -206,41 +206,52 @@ Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector =
         Libcrux_ml_kem.Vector.Portable.Arithmetic.montgomery_multiply_by_constant v r);
     f_compress_1_pre
     =
-    (fun (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) -> true);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        forall (i: nat).
+          i < 16 ==>
+          v (Seq.index (impl.f_repr a) i) >= 0 /\
+          v (Seq.index (impl.f_repr a) i) < v Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS);
     f_compress_1_post
     =
     (fun
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
-        true);
+        forall (i: nat). i < 16 ==> bounded (Seq.index (impl.f_repr out) i) 1);
     f_compress_1_
     =
-    (fun (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
-        Libcrux_ml_kem.Vector.Portable.Compress.compress_1_ v);
+    (fun (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector) ->
+        Libcrux_ml_kem.Vector.Portable.Compress.compress_1_ a);
     f_compress_pre
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
-        v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-        v_COEFFICIENT_BITS =. 11l);
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v 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 Libcrux_ml_kem.Vector.Traits.v_FIELD_MODULUS));
     f_compress_post
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         (out: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
-        true);
+        (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+          v v_COEFFICIENT_BITS == 11) ==>
+        (forall (i: nat). i < 16 ==> bounded (Seq.index (impl.f_repr out) i) (v v_COEFFICIENT_BITS))
+    );
     f_compress
     =
     (fun
         (v_COEFFICIENT_BITS: i32)
-        (v: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
+        (a: Libcrux_ml_kem.Vector.Portable.Vector_type.t_PortableVector)
         ->
-        Libcrux_ml_kem.Vector.Portable.Compress.compress v_COEFFICIENT_BITS v);
+        Libcrux_ml_kem.Vector.Portable.Compress.compress v_COEFFICIENT_BITS a);
     f_decompress_ciphertext_coefficient_pre
     =
     (fun
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst
index be631a15d..05c102c6a 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fst
@@ -45,4 +45,6 @@ let to_unsigned_representative
   let fm:v_T =
     f_bitwise_and_with_constant #v_T #FStar.Tactics.Typeclasses.solve t v_FIELD_MODULUS
   in
-  f_add #v_T #FStar.Tactics.Typeclasses.solve a fm
+  let result:v_T = f_add #v_T #FStar.Tactics.Typeclasses.solve a fm in
+  let _:Prims.unit = admit () (* Panic freedom *) in
+  result
diff --git a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
index 1df7c1846..44ad4dd11 100644
--- a/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
+++ b/libcrux-ml-kem/proofs/fstar/extraction/Libcrux_ml_kem.Vector.Traits.fsti
@@ -101,17 +101,32 @@ class t_Operations (v_Self: Type0) = {
     -> Prims.Pure v_Self
         (f_montgomery_multiply_by_constant_pre x0 x1)
         (fun result -> f_montgomery_multiply_by_constant_post x0 x1 result);
-  f_compress_1_pre:v: v_Self -> pred: Type0{true ==> pred};
-  f_compress_1_post:v_Self -> v_Self -> Type0;
+  f_compress_1_pre:a: v_Self
+    -> pred:
+      Type0
+        { (forall (i: nat).
+              i < 16 ==> v (Seq.index (f_repr a) i) >= 0 /\ v (Seq.index (f_repr a) i) < 3329) ==>
+          pred };
+  f_compress_1_post:a: v_Self -> result: v_Self
+    -> pred: Type0{pred ==> (forall (i: nat). i < 16 ==> bounded (Seq.index (f_repr result) i) 1)};
   f_compress_1_:x0: v_Self
     -> Prims.Pure v_Self (f_compress_1_pre x0) (fun result -> f_compress_1_post x0 result);
-  f_compress_pre:v_COEFFICIENT_BITS: i32 -> v: v_Self
+  f_compress_pre:v_COEFFICIENT_BITS: i32 -> a: v_Self
     -> pred:
       Type0
-        { v_COEFFICIENT_BITS =. 4l || v_COEFFICIENT_BITS =. 5l || v_COEFFICIENT_BITS =. 10l ||
-          v_COEFFICIENT_BITS =. 11l ==>
+        { (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+            v v_COEFFICIENT_BITS == 11) /\
+          (forall (i: nat).
+              i < 16 ==> v (Seq.index (f_repr a) i) >= 0 /\ v (Seq.index (f_repr a) i) < 3329) ==>
           pred };
-  f_compress_post:v_COEFFICIENT_BITS: i32 -> v_Self -> v_Self -> Type0;
+  f_compress_post:v_COEFFICIENT_BITS: i32 -> a: v_Self -> result: v_Self
+    -> pred:
+      Type0
+        { pred ==>
+          (v v_COEFFICIENT_BITS == 4 \/ v v_COEFFICIENT_BITS == 5 \/ v v_COEFFICIENT_BITS == 10 \/
+            v v_COEFFICIENT_BITS == 11) ==>
+          (forall (i: nat). i < 16 ==> bounded (Seq.index (f_repr result) i) (v v_COEFFICIENT_BITS))
+        };
   f_compress:v_COEFFICIENT_BITS: i32 -> x0: v_Self
     -> Prims.Pure v_Self
         (f_compress_pre v_COEFFICIENT_BITS x0)
@@ -333,4 +348,12 @@ val to_standard_domain (#v_T: Type0) {| i1: t_Operations v_T |} (v: v_T)
     : Prims.Pure v_T Prims.l_True (fun _ -> Prims.l_True)
 
 val to_unsigned_representative (#v_T: Type0) {| i1: t_Operations v_T |} (a: v_T)
-    : Prims.Pure v_T Prims.l_True (fun _ -> Prims.l_True)
+    : Prims.Pure v_T
+      Prims.l_True
+      (ensures
+        fun result ->
+          let result:v_T = result in
+          f_to_i16_array result ==
+          Spec.Utils.map2 ( +. )
+            (f_to_i16_array a)
+            (Spec.Utils.map_array (fun x -> (x >>! 15l) &. v_FIELD_MODULUS) (f_to_i16_array a)))