More kyber code refactoring

proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst

@@ -4,7 +4,13 @@ open Core
 open FStar.Mul
 
 unfold
-let t_KyberFieldElement = i32
+let t_FieldElementTimesMontgomeryR = i32
+
+unfold
+let t_MontgomeryFieldElement = i32
+
+unfold
+let t_StandardFieldElement = i32
 
 let v_BARRETT_MULTIPLIER: i64 = 20159L
 
@@ -80,6 +86,10 @@ let montgomery_reduce (value: i32)
   let value_high:i32 = value >>! v_MONTGOMERY_SHIFT in
   value_high -! c
 
+let montgomery_multiply_sfe_by_fer (fe fer: i32) : i32 = montgomery_reduce (fe *! fer <: i32)
+
+let to_standard_domain (mfe: i32) : i32 = montgomery_reduce (mfe *! 1353l <: i32)
+
 let to_unsigned_representative (fe: i32)
     : Prims.Pure u16
       (requires
@@ -95,16 +105,15 @@ let to_unsigned_representative (fe: i32)
   <:
   u16
 
-type t_KyberPolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) }
+type t_PolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) }
 
-let impl__KyberPolynomialRingElement__ZERO: t_KyberPolynomialRingElement =
-  { f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) } <: t_KyberPolynomialRingElement
+let impl__PolynomialRingElement__ZERO: t_PolynomialRingElement =
+  { f_coefficients = Rust_primitives.Hax.repeat 0l (sz 256) } <: t_PolynomialRingElement
 
-let add_to_ring_element (v_K: usize) (lhs rhs: t_KyberPolynomialRingElement)
-    : t_KyberPolynomialRingElement =
+let add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) : t_PolynomialRingElement =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
-  let lhs:t_KyberPolynomialRingElement =
+  let lhs:t_PolynomialRingElement =
     Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter ({
               Core.Ops.Range.f_start = sz 0;
               Core.Ops.Range.f_end
@@ -119,7 +128,7 @@ let add_to_ring_element (v_K: usize) (lhs rhs: t_KyberPolynomialRingElement)
         Core.Ops.Range.t_Range usize)
       lhs
       (fun lhs i ->
-          let lhs:t_KyberPolynomialRingElement = lhs in
+          let lhs:t_PolynomialRingElement = lhs in
           let i:usize = i in
           {
             lhs with
@@ -132,7 +141,7 @@ let add_to_ring_element (v_K: usize) (lhs rhs: t_KyberPolynomialRingElement)
             t_Array i32 (sz 256)
           }
           <:
-          t_KyberPolynomialRingElement)
+          t_PolynomialRingElement)
   in
   let _:Prims.unit = () <: Prims.unit in
   lhs

proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst

@@ -3,21 +3,31 @@ module Libcrux.Kem.Kyber.Compress
 open Core
 open FStar.Mul
 
+let compress_message_coefficient (fe: u16)
+    : Prims.Pure u8
+      (requires fe <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
+      (fun _ -> Prims.l_True) =
+  let (shifted: i16):i16 = 1664s -! (cast (fe <: u16) <: i16) in
+  let shifted_to_positive:i16 = (shifted >>! 15l <: i16) ^. shifted in
+  let shifted_positive_in_range:i16 = shifted_to_positive -! 832s in
+  cast ((shifted_positive_in_range >>! 15l <: i16) &. 1s <: i16) <: u8
+
 let get_n_least_significant_bits (n: u8) (value: u32)
     : Prims.Pure u32
-      (requires n >. 0uy && n <=. 11uy)
+      (requires n =. 4uy || n =. 5uy || n =. 10uy || n =. 11uy)
       (ensures
         fun result ->
           let result:u32 = result in
           result <. (Core.Num.impl__u32__pow 2ul (Core.Convert.f_into n <: u32) <: u32)) =
   let _:Prims.unit = () <: Prims.unit in
   value &. ((1ul <<! n <: u32) -! 1ul <: u32)
 
-let compress_q (coefficient_bits: u8) (fe: u16)
+let compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
     : Prims.Pure i32
       (requires
-        coefficient_bits >. 0uy && coefficient_bits <=. 11uy &&
-        fe <=. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
+        (coefficient_bits =. 4uy || coefficient_bits =. 5uy || coefficient_bits =. 10uy ||
+        coefficient_bits =. 11uy) &&
+        fe <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
       (ensures
         fun result ->
           let result:i32 = result in
@@ -34,10 +44,12 @@ let compress_q (coefficient_bits: u8) (fe: u16)
   in
   cast (get_n_least_significant_bits coefficient_bits compressed <: u32) <: i32
 
-let decompress_q (coefficient_bits: u8) (fe: i32)
+let decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32)
     : Prims.Pure i32
       (requires
-        coefficient_bits >. 0uy && coefficient_bits <=. 11uy && fe >=. 0l &&
+        (coefficient_bits =. 4uy || coefficient_bits =. 5uy || coefficient_bits =. 10uy ||
+        coefficient_bits =. 11uy) &&
+        fe >=. 0l &&
         fe <. (Core.Num.impl__i32__pow 2l (cast (coefficient_bits <: u8) <: u32) <: i32))
       (ensures
         fun result ->
@@ -51,3 +63,8 @@ let decompress_q (coefficient_bits: u8) (fe: i32)
   let decompressed:u32 = (decompressed <<! 1l <: u32) +! (1ul <<! coefficient_bits <: u32) in
   let decompressed:u32 = decompressed >>! (coefficient_bits +! 1uy <: u8) in
   cast (decompressed <: u32) <: i32
+
+let decompress_message_coefficient (fe: i32)
+    : Prims.Pure i32 (requires fe =. 0l || fe =. 1l) (fun _ -> Prims.l_True) =
+  (Core.Ops.Arith.Neg.neg fe <: i32) &.
+  ((Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS +! 1l <: i32) /! 2l <: i32)