f* update

cryspen · Mar 18, 2024 · 49c50ae · 49c50ae
1 parent 441677b
commit 49c50ae
Show file tree

Hide file tree

Showing 7 changed files with 352 additions and 190 deletions.
diff --git a/proofs/fstar/extraction-edited.patch b/proofs/fstar/extraction-edited.patch
diff --git a/proofs/fstar/extraction-secret-independent.patch b/proofs/fstar/extraction-secret-independent.patch
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Arithmetic.fst
@@ -39,13 +39,10 @@ let to_standard_domain (mfe: i32) =
   montgomery_reduce (mfe *! v_MONTGOMERY_R_SQUARED_MOD_FIELD_MODULUS <: i32)
 
 let to_unsigned_representative (fe: i32) =
-  let result:u16 =
-    cast (fe +! (Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS &. (fe >>! 31l <: i32) <: i32) <: i32)
-    <:
-    u16
-  in
   let _:Prims.unit = () <: Prims.unit in
-  result
+  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) =
   let _:Prims.unit = () <: Prims.unit in

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Sampling.fst
@@ -375,5 +375,4 @@ let sample_from_xof (v_K: usize) (seeds: t_Array (t_Array u8 (sz 34)) v_K) =
             Libcrux.Digest.Incremental_x4.t_Shake128StateX4))
   in
   let _:Prims.unit = Libcrux.Kem.Kyber.Hash_functions.free_state xof_state in
-  let _:Prims.unit = () <: Prims.unit in
   out
diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fst
@@ -666,6 +666,83 @@ let compress_then_serialize_ring_element_v
         <:
         Rust_primitives.Hax.t_Never)
 
+let deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8) =
+  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+    Rust_primitives.Hax.repeat Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO v_K
+  in
+  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+    Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+              (Core.Slice.impl__chunks_exact public_key
+                  Libcrux.Kem.Kyber.Constants.v_BYTES_PER_RING_ELEMENT
+                <:
+                Core.Slice.Iter.t_ChunksExact u8)
+            <:
+            Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+        <:
+        Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+      deserialized_pk
+      (fun deserialized_pk temp_1_ ->
+          let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+            deserialized_pk
+          in
+          let i, ring_element:(usize & t_Slice u8) = temp_1_ in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            Libcrux.Kem.Kyber.Arithmetic.impl__PolynomialRingElement__ZERO
+          in
+          let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+            Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Traits.Iterator.f_enumerate
+                      (Core.Slice.impl__chunks_exact ring_element (sz 3)
+                        <:
+                        Core.Slice.Iter.t_ChunksExact u8)
+                    <:
+                    Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+                <:
+                Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_ChunksExact u8))
+              re
+              (fun re temp_1_ ->
+                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement = re in
+                  let i, bytes:(usize & t_Slice u8) = temp_1_ in
+                  let byte1:i32 = cast (bytes.[ sz 0 ] <: u8) <: i32 in
+                  let byte2:i32 = cast (bytes.[ sz 1 ] <: u8) <: i32 in
+                  let byte3:i32 = cast (bytes.[ sz 2 ] <: u8) <: i32 in
+                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+                    {
+                      re with
+                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                      =
+                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                        (sz 2 *! i <: usize)
+                        ((((byte2 &. 15l <: i32) <<! 8l <: i32) |. (byte1 &. 255l <: i32) <: i32) %!
+                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+                          <:
+                          i32)
+                    }
+                    <:
+                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+                  in
+                  let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =
+                    {
+                      re with
+                      Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                      =
+                      Rust_primitives.Hax.Monomorphized_update_at.update_at_usize re
+                          .Libcrux.Kem.Kyber.Arithmetic.f_coefficients
+                        ((sz 2 *! i <: usize) +! sz 1 <: usize)
+                        (((byte3 <<! 4l <: i32) |. ((byte2 >>! 4l <: i32) &. 15l <: i32) <: i32) %!
+                          Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
+                          <:
+                          i32)
+                    }
+                    <:
+                    Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
+                  in
+                  re)
+          in
+          Rust_primitives.Hax.Monomorphized_update_at.update_at_usize deserialized_pk i re)
+  in
+  deserialized_pk
+
 let deserialize_then_decompress_10_ (serialized: t_Slice u8) =
   let _:Prims.unit = () <: Prims.unit in
   let re:Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement =

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti b/proofs/fstar/extraction/Libcrux.Kem.Kyber.Serialize.fsti
@@ -71,6 +71,11 @@ val compress_then_serialize_ring_element_v
       (re: Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement)
     : Prims.Pure (t_Array u8 v_OUT_LEN) Prims.l_True (fun _ -> Prims.l_True)
 
+val deserialize_ring_elementes_reduced (v_PUBLIC_KEY_SIZE v_K: usize) (public_key: t_Slice u8)
+    : Prims.Pure (t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K)
+      Prims.l_True
+      (fun _ -> Prims.l_True)
+
 val deserialize_then_decompress_10_ (serialized: t_Slice u8)
     : Prims.Pure Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement
       Prims.l_True

diff --git a/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst b/proofs/fstar/extraction/Libcrux.Kem.Kyber.fst
@@ -264,8 +264,9 @@ let validate_public_key
       (v_K v_RANKED_BYTES_PER_RING_ELEMENT v_PUBLIC_KEY_SIZE: usize)
       (public_key: t_Array u8 v_PUBLIC_KEY_SIZE)
      =
-  let pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
-    Libcrux.Kem.Kyber.Ind_cpa.deserialize_public_key v_K
+  let deserialized_pk:t_Array Libcrux.Kem.Kyber.Arithmetic.t_PolynomialRingElement v_K =
+    Libcrux.Kem.Kyber.Serialize.deserialize_ring_elementes_reduced v_PUBLIC_KEY_SIZE
+      v_K
       (public_key.[ { Core.Ops.Range.f_end = v_RANKED_BYTES_PER_RING_ELEMENT }
           <:
           Core.Ops.Range.t_RangeTo usize ]
@@ -276,7 +277,7 @@ let validate_public_key
     Libcrux.Kem.Kyber.Ind_cpa.serialize_public_key v_K
       v_RANKED_BYTES_PER_RING_ELEMENT
       v_PUBLIC_KEY_SIZE
-      pk
+      deserialized_pk
       (public_key.[ { Core.Ops.Range.f_start = v_RANKED_BYTES_PER_RING_ELEMENT }
           <:
           Core.Ops.Range.t_RangeFrom usize ]