Serialization ms (#32)

Add proof of `blst_p1_uncompress`

proof/blst_error.saw

@@ -0,0 +1,6 @@
+let BLST_SUCCESS = 0;
+let BLST_BAD_ENCODING = 1;
+let BLST_POINT_NOT_ON_CURVE = 2;
+let BLST_POINT_NOT_IN_GROUP = 3;
+let BLST_AGGR_TYPE_MISMATCH = 4;
+let BLST_PK_IS_INFINITY = 6;

proof/curve_operations.saw

@@ -7,24 +7,6 @@ import "../spec/ShortWeierstrassCurve.cry";
 import "../spec/implementation/Types.cry";
 import "../spec/implementation/CurveOperation.cry";
 
-// useful things for proof development, to tidy up the goal formula before printing it.
-
-propositional_rewrites <- for
-  [ "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (ite Bool a True b) (or a b))"
-  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (ite Bool a b False) (and a b))"
-  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (not (and a b)) (or (not a) (not b)))"
-  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (not (or a b)) (and (not a) (not b)))"
-   ] (prove_core abc);
-
-let prop_simpset = add_prelude_eqs
-  [ "ite_true", "ite_false", "ite_eq"
-  , "not_True", "not_False", "not_not"
-  , "and_True1", "and_True2", "and_False1", "and_False2", "and_idem"
-  , "or_True1", "or_True2", "or_False1", "or_False2", "or_idem"]
-  (addsimps propositional_rewrites empty_ss);
-
-let cleanup_simpset = add_cryptol_defs ["ecEq", "PEqInteger"] prop_simpset;
-
 let print_goal_readably_fp = do {
     unfolding ["Fp", "prime_field_bv", "prime_field_integer", "prime_field"];
     simplify cleanup_simpset;

proof/exp.saw

@@ -95,6 +95,11 @@ me_6 <- admit_cryptol {{ \n -> fp_exp Fp.field_unit n == Fp.field_unit }};
 
 fp_exp_simps <- addsimps (concat [me_1, me_2, me_3, me_4, me_5, me_6] fp_alg_thms) fp_simpset;
 
+// We will assume (and should prove in Coq)
+//  (fp_exp_fact)   {{ fp_exp x e == F_expt`{n} x `e }}
+// provided 1 <= e < 2^^n
+
+
 // Assumed overrides
 
 let {{
@@ -133,15 +138,17 @@ let ovs_for_reciprocal =
 // This computes x^(p-2).  Since for nonzero x we have x^(p-1) = 1, this gives the inverse.
 // And as we have conveneintly defined Fp.div(1,0) = 0, recip will always give Fp.div(1,x)
 
-recip_fp_algebra_thm <- admit_cryptol {{ \x -> Fp.div (Fp.field_unit, x) == fp_exp x (`p-2) }};
+// an instance of (fp_exp_fact):
+recip_fp_algebra_thm <- admit_cryptol {{ \x -> inverse_fp x == fp_exp x (`p-2) }};
 
 let reciprocal_fp_spec = do {
     out_ptr <- crucible_alloc vec384_type;
     (inp, inp_ptr) <- ptr_to_fresh_readonly "inp" vec384_type;
     crucible_precond {{ fp_invariant inp }};
     crucible_execute_func [out_ptr, inp_ptr];
     // crucible_points_to out_ptr (crucible_term {{ fp_rep (fp_exp (fp_abs inp) (`p-2)) }});
-    crucible_points_to out_ptr (crucible_term {{ fp_rep (Fp.div (Fp.field_unit, fp_abs inp)) }});
+    // crucible_points_to out_ptr (crucible_term {{ fp_rep (Fp.div (Fp.field_unit, fp_abs inp)) }});
+    crucible_points_to out_ptr (crucible_term {{ fp_rep (inverse_fp (fp_abs inp)) }});
     };
 
 reciprocal_fp_ov <- custom_verify "reciprocal_fp"
@@ -154,32 +161,26 @@ reciprocal_fp_ov <- custom_verify "reciprocal_fp"
                       w4_unint_z3 (concat ["fp_exp"] fp_unints);
                       };
 
-
-// this function also computes `inverse_fp`
-
-/* TODO: fails if x is not in Fp.  Will be OK if t_Fp is `Z p` 
-reciprocal_fp_is_inverse_thm <- custom_prove_cryptol
-  {{ \x -> inverse_fp x == Fp.div (Fp.field_unit, x) }}
-  do { goal_eval_unint (concat ["fp_exp"] fp_unints);
-       simplify fp_exp_simps;
-       //unfolding ["Fp", "prime_field_bv", "prime_field_integer", "prime_field"];
-       //simplify cleanup_simpset;
-       //print_goal;
-       w4_unint_z3 (concat ["fp_exp"] fp_unints);
-       };
-*/
-
 // ... recip_sqrt_fp
 
+// ... an algebraic fact:
 recip_sqrt_fp_algebra_thm <- admit_cryptol {{ \x -> Fp.div (Fp.field_unit, sqrt_fp x) == fp_exp x ((`p-3)/4) }};
 
+// Another instance of (fp_exp_fact)
+sqrt_fp_alg_thm <- admit_cryptol {{ \x -> sqrt_fp x == fp_exp x ((`p+1)/4) }} ;
+
+// ... and an algebraic fact about is_square_fp
+is_square_fp_thm <- admit_cryptol
+  {{ \x -> is_square_fp x == (x == Fp.sq (sqrt_fp x)) }} ;
+
 let recip_sqrt_fp_spec = do {
     out_ptr <- crucible_alloc vec384_type;
     (inp, inp_ptr) <- ptr_to_fresh_readonly "inp" vec384_type;
     crucible_precond {{ fp_invariant inp }};
     crucible_execute_func [out_ptr, inp_ptr];
     // crucible_points_to out_ptr (crucible_term {{ fp_rep (fp_exp (fp_abs inp) ((`p-3)/4)) }});
     crucible_points_to out_ptr (crucible_term {{fp_rep (Fp.div (Fp.field_unit, sqrt_fp (fp_abs inp))) }});
+    crucible_return (crucible_term {{ if is_square_fp (fp_abs inp) then 1:Limb else 0 }});
     };
 
 recip_sqrt_fp_ov <- custom_verify "recip_sqrt_fp"
@@ -188,6 +189,42 @@ recip_sqrt_fp_ov <- custom_verify "recip_sqrt_fp"
                     do {
                       simplify (addsimp recip_sqrt_fp_algebra_thm empty_ss);
                       unfolding ["sqr_n_mul"];
+                      simplify (addsimps [is_square_fp_thm, sqrt_fp_alg_thm] empty_ss);
                       simplify fp_exp_simps;
                       w4_unint_z3 (concat ["fp_exp"] fp_unints);
                       };
+
+// ... sqrt_fp
+
+let sqrt_fp_spec = do {
+    out_ptr <- crucible_alloc vec384_type;
+    (inp, inp_ptr) <- ptr_to_fresh_readonly "inp" vec384_type;
+    crucible_precond {{ fp_invariant inp }};
+    crucible_execute_func [out_ptr, inp_ptr];
+    // crucible_points_to out_ptr (crucible_term {{ fp_rep (fp_exp (fp_abs inp) ((`p+1)/4)) }});
+    crucible_points_to out_ptr (crucible_term {{ fp_rep (sqrt_fp (fp_abs inp)) }});
+    crucible_return (crucible_term {{ if is_square_fp (fp_abs inp) then 1:Limb else 0 }});
+};
+
+let sqrt_fp_alias_spec = do {
+    (out, out_ptr) <- ptr_to_fresh "out" vec384_type;
+    crucible_precond {{ fp_invariant out }};
+    crucible_execute_func [out_ptr, out_ptr];
+    crucible_points_to out_ptr (crucible_term {{ fp_rep (sqrt_fp (fp_abs out)) }});
+    crucible_return (crucible_term {{ if is_square_fp (fp_abs out) then 1:Limb else 0 }});
+};
+
+let verify_sqrt_fp spec = custom_verify "sqrt_fp"
+              ovs_for_reciprocal
+              spec
+              do {
+                 simplify (addsimps [is_square_fp_thm, sqrt_fp_alg_thm] empty_ss);
+                 unfolding ["sqr_n_mul"];
+                 simplify fp_exp_simps;
+                 w4_unint_z3 (concat ["fp_exp"] fp_unints);
+                 };
+
+sqrt_fp_ov <- verify_sqrt_fp sqrt_fp_spec;
+sqrt_fp_alias_ov <- verify_sqrt_fp  sqrt_fp_alias_spec;
+
+let sqrt_fp_ovs = [sqrt_fp_ov, sqrt_fp_alias_ov];

proof/functional_proofs.saw

@@ -19,4 +19,5 @@ include "exp.saw";
 include "curve_operations.saw";
 include "ec_mult.saw";
 include "map_to_g1.saw";
-include "curve_operations_e2.saw";
+include "curve_operations_e2.saw";
+include "deserialize-p1.saw";

proof/proof-helpers.saw

@@ -110,3 +110,35 @@ let really_prove_cryptol thm unints =
 let really_custom_prove_cryptol thm script =
   prove_print script thm;
 
+
+////////////////////////////////////////////////////////////////
+//
+// Other helpers for proofs
+//
+
+// useful things for proof development, to tidy up the goal formula before printing it.
+
+propositional_rewrites <- for
+  [ "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (ite Bool a True b) (or a b))"
+  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (ite Bool a b False) (and a b))"
+  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (not (and a b)) (or (not a) (not b)))"
+  , "(a:Bool) -> (b:Bool) -> EqTrue (eq Bool (not (or a b)) (and (not a) (not b)))"
+   ] (prove_core abc);
+
+let prop_simpset = add_prelude_eqs
+  [ "ite_true", "ite_false", "ite_eq"
+  , "not_True", "not_False", "not_not"
+  , "and_True1", "and_True2", "and_False1", "and_False2", "and_idem"
+  , "or_True1", "or_True2", "or_False1", "or_False2", "or_idem"]
+  (addsimps propositional_rewrites empty_ss);
+
+let cleanup_simpset = add_cryptol_defs ["ecEq", "PEqInteger"] prop_simpset;
+
+let print_clean_goal = do {
+  unfolding ["/\\", "\\/", "==>"];
+  simplify (cryptol_ss());
+  simplify cleanup_simpset;
+  print_goal;
+  };
+
+

proof/vect.saw

@@ -150,6 +150,24 @@ vec_is_zero_2fp2_ov <- test "vec_is_zero" []  vec_is_zero_2fp2_spec;
 
 // ... continuing with vec_is_equal
 
+let vec_is_equal_48_spec = do {
+  (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384_type;
+  (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384_type;
+  crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (48:Size_t) }}]; // Non-portable
+  crucible_return (crucible_term {{ if a == b then 1 else (0:Limb) }});
+  };
+
+vec_is_equal_48_ov <- verify "vec_is_equal" []  vec_is_equal_48_spec;
+
+let vec_is_equal_48_vec_spec = do {
+  (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384_type;
+  (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384_type;
+  crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (48:Size_t) }}]; // Non-portable
+  crucible_return (crucible_term {{ if (vec384_abs a) == (vec384_abs b) then 1 else (0:Limb) }});
+  };
+
+vec_is_equal_48_vec_ov <- verify "vec_is_equal" []  vec_is_equal_48_spec;
+
 let vec_is_equal_fp_spec = do {
   (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384_type;
   (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384_type;
@@ -205,12 +223,14 @@ let vec_copy_spec bytes  ty = do {
 
 vec_copy_fp_ov <- verify "vec_copy" [] (vec_copy_spec 48 vec384_type);
 vec_copy_POINTonE1_ov <- verify "vec_copy" [] (vec_copy_spec 144 POINTonE1_type);
+vec_copy_POINTonE1_affine_ov <- verify "vec_copy" [] (vec_copy_spec 96 POINTonE1_affine_type);
 
 // all overrides
 
 let vec_overrides = concat [ vec_is_zero_fp_ov, vec_is_zero_2fp_ov
                            , vec_is_equal_fp_ov, vec_is_equal_2fp_ov
-                           , vec_copy_fp_ov, vec_copy_POINTonE1_ov] vec_select_overrides;
+                           , vec_copy_fp_ov, vec_copy_POINTonE1_ov
+                           , vec_copy_POINTonE1_affine_ov] vec_select_overrides;
 
 // for E2:
 

scripts/build_llvm.sh

@@ -11,7 +11,7 @@ do
   patch -f -p1 -t < "$p" # -f to prevent patch from automatically enabling option -R when it things it should
 done
 
-export CFLAGS='-g -fPIC -Wall -Wextra -Werror'
+export CFLAGS='-g -fPIC -Wall -Wextra -Werror -D__ADX__'
 export CC=wllvm
 export LLVM_COMPILER=clang
 ./build.sh

spec/Serialization.cry

@@ -13,6 +13,7 @@ import ShortWeierstrassCurve as EC
 import rfc8017
 import Maybe
 import FieldExtras (F_expt)
+import BLSFieldExtras
 
 //// Serialization (with compression)
 
@@ -58,13 +59,7 @@ serialize_E2 P = x_string_E2 P || ([m_byte]# zero) where
 
 // TODO: These definitions are copied from hash-to-curve, but there they are in a parameter definiton
 // and are not in scope for importation here.
-
-is_square_F_p: t_Fp -> Bit
-is_square_F_p x =  y == 0 \/ y == 1 where
-    y = F_expt`{n=width p} Fp x `((p-1)/2)
-
-sqrt_F_p: t_Fp -> t_Fp
-sqrt_F_p x = F_expt`{n=width p} Fp x `((p+1)/4) // the "= 3 (mod 4)" variant
+// TODO: Those also appear in BLSFieldExtras.cry
 
 type q = p*p
 
@@ -101,29 +96,58 @@ sqrt_F_p_2 x = z where
 
 // end TODO section
 
-deserialize_E1: [48][8] -> Maybe (EC::AffinePoint t_Fp)
+// TODO: we need [96][8] because if the infinity bit is set, we must check all 96 bytes (except first 3 bits) are zero. We could also have a separate uncompress function.
+// the C code can take a 96 bytes array whose last 48 are unintialized
+// we deviate from the RFC: the RFC says "if the string has length...", but in the C code there's no concept of length of the string
+
+deserialize_E1: [96][8] -> Maybe (EC::AffinePoint t_Fp)
 deserialize_E1 s_string = ret where
     // Step 1.
-    m_byte = (s_string@0) && 0xE0
+    m_byte = (s_string@0) && 0xE0 // three highest bits
     C_bit = m_byte @ 0
     I_bit = m_byte @ 1
     S_bit = m_byte @ 2
     // Step 2 deferred (we check that C_bit is 1 later)
     // Step 3
-    s_string' = [(s_string@0) && 0x1F] # tail s_string
+    s_string' = take`{front=48} ([(s_string@0) && 0x1F] # tail s_string) // the last 48 bytes may be uninitialized for a compressed point. TODO should we assume they're zero? doesn't seem to make sense (extra work for the caller)
     // Step 6
     x = OS2IP(s_string')
     //Step 7 (on curve E)
     y2 = Fp.add (Fp.mul (x, Fp.sq x), 4)
-    y = sqrt_F_p y2
+    y = sqrt_fp y2
     Y_bit = sign_F_p y
     // Steps 2, 4, 8
-    ret = if C_bit == False then nothing // Error, from Step 2
+    ret = if C_bit == False then nothing // Error, from Step 2; TODO what if I_bit is set? We could still return inf
            | I_bit then (if s_string' == zero then just (EC::point_O E) else nothing) // Step 4
-           | ~ (is_square_F_p y2) then nothing // from Step 7
+           | ~ (is_square_fp y2) then nothing // from Step 7
            | S_bit == Y_bit then just (x,y)
           else just (x, Fp.neg y)
 
+// draft-irtf-cfrg-bls-signature-04 specifies that the compressed representation is used for BLST
+uncompress_E1: [48][8] -> Maybe (EC::AffinePoint t_Fp)
+uncompress_E1 s_string = ret where
+    // Step 1.
+    m_byte = (s_string@0) && 0xE0 // three highest bits
+    C_bit = m_byte @ 0
+    I_bit = m_byte @ 1
+    S_bit = m_byte @ 2
+    // Step 2 deferred (we check that C_bit is 1 later)
+    // Step 3
+    s_string' = [(s_string@0) && 0x1F] # tail s_string
+    // Step 6
+    x = OS2IP(s_string')
+    // TODO here the C implementation checks that x is smaller than the modulus
+    //Step 7 (on curve E)
+    y2 = Fp.add (Fp.mul (x, Fp.sq x), 4)
+    y = sqrt_fp y2
+    Y_bit = sign_F_p y
+    // Steps 2, 4, 8
+    ret = if (m_byte == 0x20 ) || (m_byte == 0x60) || (m_byte == 0xE0) then nothing
+           | C_bit == False then nothing // Error, from Step 2
+           | I_bit then (if s_string' == zero then just (EC::point_O E) else nothing) // Step 4
+           | ~ (is_square_fp y2) then nothing // from Step 7
+           | S_bit == Y_bit then just (x,y)
+          else just (x, Fp.neg y)
 
 deserialize_E2: [96][8] -> Maybe (EC::AffinePoint t_Fp_2)
 deserialize_E2 s_string = ret where