revert dcdaf1a

cryspen · Feb 1, 2024 · 8747049 · 8747049
1 parent 38aea7d
commit 8747049
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 37 deletions.
diff --git a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Arithmetic.fsti
@@ -57,11 +57,6 @@ let int_to_spec_fe (m:int) : Spec.Kyber.field_element =
       m_v + v Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
     else m_v
 
-let wf_fe_to_spec_fe (m: wfFieldElement): Spec.Kyber.field_element =
-  if v m < 0 
-  then v m + v Libcrux.Kem.Kyber.Constants.v_FIELD_MODULUS
-  else v m
-
 let to_spec_fe (m:i32) : Spec.Kyber.field_element = 
     int_to_spec_fe (v m)
 
@@ -193,12 +188,6 @@ let to_spec_poly (m:t_PolynomialRingElement) : (Spec.Kyber.polynomial) =
     assert (forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS);
     p
 
-let wf_poly_to_spec_poly (re: wfPolynomialRingElement): Spec.Kyber.polynomial 
-    = let p = Spec.Kyber.map' (fun x -> wf_fe_to_spec_fe x <: nat) re.f_coefficients in
-      introduce forall i. Seq.index p i < v Spec.Kyber.v_FIELD_MODULUS
-      with assert (Seq.index p i == Seq.index p (v (sz i)));
-      p
-
 let to_spec_poly_b #b (m:t_PolynomialRingElement_b b) : (Spec.Kyber.polynomial) =
     to_spec_poly (derefine_poly_b m)
 

diff --git a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fst b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fst
@@ -1322,21 +1322,6 @@ let deserialize_to_uncompressed_ring_element (serialized: t_Slice u8) =
   in
   re
 #pop-options
-
-module A = Libcrux.Kem.Kyber.Arithmetic
-
-let bitwise_equality #len #d (p1 p2: (p: t_Array nat len {forall i. Seq.index p i < pow2 d}))
-  : Lemma 
-    (requires forall i. bit_vec_of_nat_array p1 d i == bit_vec_of_nat_array p2 d i)
-    (ensures p1 == p2)
-  = admit ()
-
-let eq_rw #len (re_poly: t_Array nat len)
-  : Lemma (
-
-        bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12)
-    )
-  = admit ()
 
 #push-options "--z3rlimit 100"
 let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement) =
@@ -1378,13 +1363,5 @@ let serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPoly
           in
           serialized)
   in
-  // admitP (bitwise_equality serialized (Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re)));
-  // admitP (serialized == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re));
-  let re_poly = A.wf_poly_to_spec_poly re in
-  assert (
-       bit_vec_to_int_t_array 8 (bit_vec_of_nat_array re_poly 12)
-    == Spec.Kyber.byte_encode 12 re_poly
-  );
-  admit ();
   serialized
 #pop-options
diff --git a/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti b/proofs/fstar/extraction-edited/Libcrux.Kem.Kyber.Serialize.fsti
@@ -188,9 +188,7 @@ val deserialize_to_uncompressed_ring_element (serialized: t_Slice u8)
       (requires (length serialized == Spec.Kyber.v_BYTES_PER_RING_ELEMENT))
       (ensures fun _ -> True)
 
-module A = Libcrux.Kem.Kyber.Arithmetic
-
 val serialize_uncompressed_ring_element (re: Libcrux.Kem.Kyber.Arithmetic.wfPolynomialRingElement)
     : Pure (t_Array u8 (sz 384))
       (requires True)
-      (ensures (fun res -> res == Spec.Kyber.byte_encode 12 (A.wf_poly_to_spec_poly re)))
+      (ensures (fun res -> True))