Update f-star extraction.

cryspen · Sep 28, 2023 · 0e26ba2 · 0e26ba2
1 parent af6705a
commit 0e26ba2
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 23 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Compress.fst
@@ -13,7 +13,13 @@ let compress
       =
       Core.Array.map_under_impl_23 re
           .Libcrux.Kem.Kyber768.Arithmetic.KyberPolynomialRingElement.f_coefficients
-        (fun coefficient -> compress_q coefficient bits_per_compressed_coefficient <: i32)
+        (fun coefficient ->
+            compress_q (Libcrux.Kem.Kyber768.Conversions.to_unsigned_representative coefficient
+                <:
+                u16)
+              bits_per_compressed_coefficient
+            <:
+            i32)
     }
   in
   re
@@ -34,25 +40,22 @@ let decompress
   in
   re
 
-let compress_q (fe: i32) (to_bit_size: usize) : i32 =
+let compress_q (fe: u16) (to_bit_size: usize) : i32 =
   let _:Prims.unit =
     if true
     then
       let _:Prims.unit =
         if ~.(to_bit_size <=. Libcrux.Kem.Kyber768.Parameters.v_BITS_PER_COEFFICIENT <: bool)
         then
-          Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"
+          Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= BITS_PER_COEFFICIENT"
 
               <:
               Rust_primitives.Hax.t_Never)
       in
       ()
   in
   let two_pow_bit_size:u32 = 1ul >>. to_bit_size in
-  let fe_unsigned:i32 =
-    fe +. ((fe <<. 15l <: i32) &. Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS <: i32)
-  in
-  let compressed:u32 = cast fe_unsigned *. (two_pow_bit_size >>. 1l <: u32) in
+  let compressed:u32 = cast fe *. (two_pow_bit_size >>. 1l <: u32) in
   let compressed:Prims.unit = compressed +. cast Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS in
   let compressed:Prims.unit =
     compressed /. cast (Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS >>. 1l <: i32)
@@ -66,7 +69,7 @@ let decompress_q (fe: i32) (to_bit_size: usize) : i32 =
       let _:Prims.unit =
         if ~.(to_bit_size <=. Libcrux.Kem.Kyber768.Parameters.v_BITS_PER_COEFFICIENT <: bool)
         then
-          Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= parameters::BITS_PER_COEFFICIENT"
+          Rust_primitives.Hax.never_to_any (Core.Panicking.panic "assertion failed: to_bit_size <= BITS_PER_COEFFICIENT"
 
               <:
               Rust_primitives.Hax.t_Never)

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Conversions.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Conversions.fst
@@ -107,4 +107,7 @@ let impl (#len: usize) : t_UpdatingArray (t_UpdatableArray v_LEN) =
         }
       in
       self
-  }
+  }
+
+let to_unsigned_representative (fe: i32) : u16 =
+  cast (fe +. ((fe <<. 15l <: i32) &. Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS <: i32))
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Serialize.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber768.Serialize.fst
@@ -353,34 +353,28 @@ let serialize_little_endian_12_ (re: Libcrux.Kem.Kyber768.Arithmetic.t_KyberPoly
         _)
       serialized
       (fun serialized (i, chunks) ->
-          let coefficient1:i32 = chunks.[ 0sz ] in
-          let coefficient1:Prims.unit =
-            coefficient1 +.
-            ((coefficient1 <<. 15l <: i32) &. Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS <: i32
-            )
+          let coefficient1:u16 =
+            Libcrux.Kem.Kyber768.Conversions.to_unsigned_representative (chunks.[ 0sz ] <: i32)
           in
-          let coefficient2:i32 = chunks.[ 1sz ] in
-          let coefficient2:Prims.unit =
-            coefficient2 +.
-            ((coefficient2 <<. 15l <: i32) &. Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS <: i32
-            )
+          let coefficient2:u16 =
+            Libcrux.Kem.Kyber768.Conversions.to_unsigned_representative (chunks.[ 1sz ] <: i32)
           in
           let serialized:array u8 384sz =
             Rust_primitives.Hax.update_at serialized
               (3sz *. i <: usize)
-              (cast (coefficient1 &. 255l <: i32))
+              (cast (coefficient1 &. 255us <: u16))
           in
           let serialized:array u8 384sz =
             Rust_primitives.Hax.update_at serialized
               ((3sz *. i <: usize) +. 1sz <: usize)
-              (cast ((coefficient1 <<. 8l <: i32) |. ((coefficient2 &. 15l <: i32) >>. 4l <: i32)
+              (cast ((coefficient1 <<. 8l <: u16) |. ((coefficient2 &. 15us <: u16) >>. 4l <: u16)
                     <:
-                    i32))
+                    u16))
           in
           let serialized:array u8 384sz =
             Rust_primitives.Hax.update_at serialized
               ((3sz *. i <: usize) +. 2sz <: usize)
-              (cast ((coefficient2 <<. 4l <: i32) &. 255l <: i32))
+              (cast ((coefficient2 <<. 4l <: u16) &. 255us <: u16))
           in
           serialized)
   in
-Original file line number
+Diff line change
@@ Expand Up @@
             }
           in
           self
-      }
+      }
+    let to_unsigned_representative (fe: i32) : u16 =
+      cast (fe +. ((fe <<. 15l <: i32) &. Libcrux.Kem.Kyber768.Parameters.v_FIELD_MODULUS <: i32))