Revert changes outside of extraction-edited

cryspen · Jan 9, 2024 · 7658d96 · 7658d96
1 parent 518a11f
commit 7658d96
Show file tree

Hide file tree

Showing 25 changed files with 887 additions and 112 deletions.
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
@@ -3,11 +3,49 @@ module Libcrux.Kem.Kyber.Arithmetic
 open Core
 open FStar.Mul
 
-let get_n_least_significant_bits (n: u8) (value: u32) =
+unfold
+let t_FieldElement = i32
+
+unfold
+let t_FieldElementTimesMontgomeryR = i32
+
+unfold
+let t_MontgomeryFieldElement = i32
+
+let v_BARRETT_MULTIPLIER: i64 = 20159L
+
+let v_BARRETT_SHIFT: i64 = 26L
+
+let v_BARRETT_R: i64 = 1L <<! v_BARRETT_SHIFT
+
+let v_INVERSE_OF_MODULUS_MOD_R: u32 = 62209ul
+
+let v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS: i32 = 1353l
+
+let v_MONTGOMERY_SHIFT: u8 = 16uy
+
+let v_MONTGOMERY_R: i32 = 1l <<! v_MONTGOMERY_SHIFT
+
+let get_n_least_significant_bits (n: u8) (value: u32)
+    : Prims.Pure u32
+      (requires n =. 4uy || n =. 5uy || n =. 10uy || n =. 11uy || n =. v_MONTGOMERY_SHIFT)
+      (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 barrett_reduce (value: i32) =
+let barrett_reduce (value: i32)
+    : Prims.Pure i32
+      (requires
+        (Core.Convert.f_from value <: i64) >. (Core.Ops.Arith.Neg.neg v_BARRETT_R <: i64) &&
+        (Core.Convert.f_from value <: i64) <. v_BARRETT_R)
+      (ensures
+        fun result ->
+          let result:i32 = result in
+          result >. (Core.Ops.Arith.Neg.neg Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) &&
+          result <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS) =
   let _:Prims.unit = () <: Prims.unit in
   let t:i64 =
     ((Core.Convert.f_from value <: i64) *! v_BARRETT_MULTIPLIER <: i64) +!
@@ -18,7 +56,25 @@ let barrett_reduce (value: i32) =
   let _:Prims.unit = () <: Prims.unit in
   result
 
-let montgomery_reduce (value: i32) =
+let montgomery_reduce (value: i32)
+    : Prims.Pure i32
+      (requires
+        value >=.
+        ((Core.Ops.Arith.Neg.neg Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) *!
+          v_MONTGOMERY_R
+          <:
+          i32) &&
+        value <=. (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS *! v_MONTGOMERY_R <: i32))
+      (ensures
+        fun result ->
+          let result:i32 = result in
+          result >=.
+          ((Core.Ops.Arith.Neg.neg (3l *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: i32
+            ) /!
+            2l
+            <:
+            i32) &&
+          result <=. ((3l *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) /! 2l <: i32)) =
   let _:i32 = v_MONTGOMERY_R in
   let _:Prims.unit = () <: Prims.unit in
   let t:u32 =
@@ -33,18 +89,73 @@ 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) = montgomery_reduce (fe *! fer <: i32)
+let montgomery_multiply_sfe_by_fer (fe fer: i32) : i32 = montgomery_reduce (fe *! fer <: i32)
 
-let to_standard_domain (mfe: i32) =
+let to_standard_domain (mfe: i32) : i32 =
   montgomery_reduce (mfe *! v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS <: i32)
 
-let to_unsigned_representative (fe: i32) =
+let to_unsigned_representative (fe: i32)
+    : Prims.Pure u16
+      (requires
+        fe >=. (Core.Ops.Arith.Neg.neg Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) &&
+        fe <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS)
+      (ensures
+        fun result ->
+          let result:u16 = result in
+          result >=. 0us &&
+          result <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16)) =
   let _:Prims.unit = () <: Prims.unit in
   cast (fe +! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS &. (fe >>! 31l <: i32) <: i32) <: i32)
   <:
   u16
 
-let add_to_ring_element (v_K: usize) (lhs rhs: t_PolynomialRingElement) =
+type t_PolynomialRingElement = { f_coefficients:t_Array i32 (sz 256) }
+
+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_PolynomialRingElement)
+    : Prims.Pure t_PolynomialRingElement
+      (requires
+        Hax_lib.v_forall (fun i ->
+              let i:usize = i in
+              Hax_lib.implies (i <. Libcrux.Kem.Kyber.Constants.v_COEFFICIENTS_IN_RING_ELEMENT
+                  <:
+                  bool)
+                (((Core.Num.impl__i32__abs (lhs.f_coefficients.[ i ] <: i32) <: i32) <=.
+                    (((cast (v_K <: usize) <: i32) -! 1l <: i32) *!
+                      Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+                      <:
+                      i32)
+                    <:
+                    bool) &&
+                  ((Core.Num.impl__i32__abs (rhs.f_coefficients.[ i ] <: i32) <: i32) <=.
+                    Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+                    <:
+                    bool))
+              <:
+              bool))
+      (ensures
+        fun result ->
+          let result:t_PolynomialRingElement = result in
+          Hax_lib.v_forall (fun i ->
+                let i:usize = i in
+                Hax_lib.implies (i <.
+                    (Core.Slice.impl__len (Rust_primitives.unsize result.f_coefficients
+                          <:
+                          t_Slice i32)
+                      <:
+                      usize)
+                    <:
+                    bool)
+                  ((Core.Num.impl__i32__abs (result.f_coefficients.[ i ] <: i32) <: i32) <=.
+                    ((cast (v_K <: usize) <: i32) *! Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+                      <:
+                      i32)
+                    <:
+                    bool)
+                <:
+                bool)) =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
   let lhs:t_PolynomialRingElement =

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fst
@@ -3,14 +3,33 @@ module Libcrux.Kem.Kyber.Compress
 open Core
 open FStar.Mul
 
-let compress_message_coefficient (fe: u16) =
+let compress_message_coefficient (fe: u16)
+    : Prims.Pure u8
+      (requires fe <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
+      (ensures
+        fun result ->
+          let result:u8 = result in
+          Hax_lib.implies ((833us <=. fe <: bool) && (fe <=. 2596us <: bool))
+            (result =. 1uy <: bool) &&
+          Hax_lib.implies (~.((833us <=. fe <: bool) && (fe <=. 2596us <: bool)) <: bool)
+            (result =. 0uy <: bool)) =
   let (shifted: i16):i16 = 1664s -! (cast (fe <: u16) <: i16) in
   let mask:i16 = shifted >>! 15l in
   let shifted_to_positive:i16 = mask ^. shifted in
   let shifted_positive_in_range:i16 = shifted_to_positive -! 832s in
   cast ((shifted_positive_in_range >>! 15l <: i16) &. 1s <: i16) <: u8
 
-let compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16) =
+let compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
+    : Prims.Pure i32
+      (requires
+        (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
+          result >=. 0l &&
+          result <. (Core.Num.impl__i32__pow 2l (cast (coefficient_bits <: u8) <: u32) <: i32)) =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
   let compressed:u32 = (cast (fe <: u16) <: u32) <<! (coefficient_bits +! 1uy <: u8) in
@@ -25,7 +44,17 @@ let compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16) =
   <:
   i32
 
-let decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32) =
+let decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32)
+    : Prims.Pure i32
+      (requires
+        (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 ->
+          let result:i32 = result in
+          result <. Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS) =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
   let decompressed:u32 =
@@ -35,6 +64,7 @@ let decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32) =
   let decompressed:u32 = decompressed >>! (coefficient_bits +! 1uy <: u8) in
   cast (decompressed <: u32) <: i32
 
-let decompress_message_coefficient (fe: 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)
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fsti b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Compress.fsti
@@ -3,6 +3,18 @@ module Libcrux.Kem.Kyber.Compress
 open Core
 open FStar.Mul
 
+val compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
+    : Prims.Pure i32
+      (requires
+        (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
+          result >=. 0l &&
+          result <. (Core.Num.impl__i32__pow 2l (cast (coefficient_bits <: u8) <: u32) <: i32))
+
 val compress_message_coefficient (fe: u16)
     : Prims.Pure u8
       (requires fe <. (cast (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS <: i32) <: u16))
@@ -18,18 +30,6 @@ val compress_message_coefficient (fe: u16)
                 let _:Prims.unit = temp_0_ in
                 result =. 0uy <: bool))
 
-val compress_ciphertext_coefficient (coefficient_bits: u8) (fe: u16)
-    : Prims.Pure i32
-      (requires
-        (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
-          result >=. 0l &&
-          result <. (Core.Num.impl__i32__pow 2l (cast (coefficient_bits <: u8) <: u32) <: i32))
-
 val decompress_ciphertext_coefficient (coefficient_bits: u8) (fe: i32)
     : Prims.Pure i32
       (requires

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constant_time_ops.fst
@@ -3,15 +3,29 @@ module Libcrux.Kem.Kyber.Constant_time_ops
 open Core
 open FStar.Mul
 
-let is_non_zero (value: u8) =
+let is_non_zero (value: u8)
+    : Prims.Pure u8
+      Prims.l_True
+      (ensures
+        fun result ->
+          let result:u8 = result in
+          Hax_lib.implies (value =. 0uy <: bool) (result =. 0uy <: bool) &&
+          Hax_lib.implies (value <>. 0uy <: bool) (result =. 1uy <: bool)) =
   let value:u16 = cast (value <: u8) <: u16 in
   let result:u16 =
     ((value |. (Core.Num.impl__u16__wrapping_add (~.value <: u16) 1us <: u16) <: u16) >>! 8l <: u16) &.
     1us
   in
   cast (result <: u16) <: u8
 
-let compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8) =
+let compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_Slice u8)
+    : Prims.Pure u8
+      Prims.l_True
+      (ensures
+        fun result ->
+          let result:u8 = result in
+          Hax_lib.implies (lhs =. rhs <: bool) (result =. 0uy <: bool) &&
+          Hax_lib.implies (lhs <>. rhs <: bool) (result =. 1uy <: bool)) =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
   let (r: u8):u8 = 0uy in
@@ -32,7 +46,14 @@ let compare_ciphertexts_in_constant_time (v_CIPHERTEXT_SIZE: usize) (lhs rhs: t_
   in
   is_non_zero r
 
-let select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8) =
+let select_shared_secret_in_constant_time (lhs rhs: t_Slice u8) (selector: u8)
+    : Prims.Pure (t_Array u8 (sz 32))
+      Prims.l_True
+      (ensures
+        fun result ->
+          let result:t_Array u8 (sz 32) = result in
+          Hax_lib.implies (selector =. 0uy <: bool) (result =. lhs <: bool) &&
+          Hax_lib.implies (selector <>. 0uy <: bool) (result =. rhs <: bool)) =
   let _:Prims.unit = () <: Prims.unit in
   let _:Prims.unit = () <: Prims.unit in
   let mask:u8 = Core.Num.impl__u8__wrapping_sub (is_non_zero selector <: u8) 1uy in

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fst
@@ -0,0 +1,23 @@
+module Libcrux.Kem.Kyber.Constants
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let v_BITS_PER_COEFFICIENT: usize = sz 12
+
+let v_COEFFICIENTS_IN_RING_ELEMENT: usize = sz 256
+
+let v_BITS_PER_RING_ELEMENT: usize = v_COEFFICIENTS_IN_RING_ELEMENT *! sz 12
+
+let v_BYTES_PER_RING_ELEMENT: usize = v_BITS_PER_RING_ELEMENT /! sz 8
+
+let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = sz 32
+
+let v_FIELD_MODULUS: i32 = 3329l
+
+let v_H_DIGEST_SIZE: usize =
+  Libcrux.Digest.digest_size (Libcrux.Digest.Algorithm_Sha3_256_ <: Libcrux.Digest.t_Algorithm)
+
+let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5
+
+let v_SHARED_SECRET_SIZE: usize = sz 32
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fsti b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Constants.fsti
@@ -15,8 +15,7 @@ let v_CPA_PKE_KEY_GENERATION_SEED_SIZE: usize = sz 32
 
 let v_FIELD_MODULUS: i32 = 3329l
 
-let v_H_DIGEST_SIZE: usize =
-  Libcrux.Digest.digest_size (Libcrux.Digest.Algorithm_Sha3_256_ <: Libcrux.Digest.t_Algorithm)
+let v_H_DIGEST_SIZE: usize = sz 32
 
 let v_REJECTION_SAMPLING_SEED_SIZE: usize = sz 168 *! sz 5