From e15494b46b84962a20b7af8af83a75fe14a37f99 Mon Sep 17 00:00:00 2001 From: msaaltink Date: Wed, 6 Jan 2021 20:00:17 -0500 Subject: [PATCH] Serialization ms (#32) Add proof of `blst_p1_uncompress` --- proof/blst_error.saw | 6 + proof/curve_operations.saw | 18 - proof/deserialize-p1.saw | 481 ++++++++++++++++++++++++++ proof/exp.saw | 71 +++- proof/functional_proofs.saw | 3 +- proof/proof-helpers.saw | 32 ++ proof/vect.saw | 22 +- scripts/build_llvm.sh | 2 +- spec/Serialization.cry | 50 ++- spec/implementation/serialization.cry | 78 +++++ tests/SerializationTests.cry | 2 +- 11 files changed, 713 insertions(+), 52 deletions(-) create mode 100644 proof/blst_error.saw create mode 100644 proof/deserialize-p1.saw create mode 100644 spec/implementation/serialization.cry diff --git a/proof/blst_error.saw b/proof/blst_error.saw new file mode 100644 index 00000000..7cf7ecb3 --- /dev/null +++ b/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; diff --git a/proof/curve_operations.saw b/proof/curve_operations.saw index 85e0b0b4..26b2c37d 100644 --- a/proof/curve_operations.saw +++ b/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; diff --git a/proof/deserialize-p1.saw b/proof/deserialize-p1.saw new file mode 100644 index 00000000..9ab7884f --- /dev/null +++ b/proof/deserialize-p1.saw @@ -0,0 +1,481 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +include "blst_error.saw"; + +import "../spec/Serialization.cry"; +EC <- cryptol_load "../spec/ShortWeierstrassCurve.cry"; +import "../Parameters.cry"; +import "../spec/implementation/Types.cry"; +import "../spec/Maybe.cry"; +import "../spec/implementation/CurveOperation.cry"; +import "../spec/implementation/serialization.cry"; + +/////////////////////////////////////////////////////////////////////////////// +// Specifications +/////////////////////////////////////////////////////////////////////////////// + +// The main specification here is for blst_p1_uncompress + +let blst_p1_uncompress_OK_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + crucible_precond {{ uncompress_E1_imp inp != nothing }}; + crucible_execute_func [out_ptr, in_ptr]; + + ret <- crucible_fresh_var "ret" (llvm_int 32); + crucible_return (crucible_term ret); + crucible_points_to out_ptr (crucible_term {{ + POINTonE1_affine_rep (if (inp@0)@1 // infinity bit // was uncompress_E1_imp inp == just (point_O E) + then point_O E + else uncompress_E1_OK inp) }}); + // the return still might be BLST_POINT_NOT_IN_GROUP rather than BLST_SUCCESS +}; + +// The proof is a compostional verification, in 3 stages: first proofs about POINTonE1_Uncompress_BE, +// then proofs about POINTonE1_Uncompress, and finally the proof of blst_p1_uncompress. + +// POINTonE1_Uncompress_BE has two different error conditions, which we deal with by having +// three different specifications and overrides, one for each error and one for success. + +// ... the success case +let POINTonE1_Uncompress_BE_OK_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + // crucible_precond {{ fp_invariant (uncompress_E1_x inp) }}; + crucible_precond {{ uncompress_E1_x inp < `p }}; + crucible_precond {{ is_square_fp (uncompress_E1_y2 inp) }}; + crucible_execute_func [out_ptr, in_ptr]; + crucible_points_to out_ptr (crucible_term {{ + (fp_rep (uncompress_E1_x_fp inp), fp_rep (sqrt_fp (uncompress_E1_y2 inp))) }}) ; + // This return value is copied from sgn0_pty_mont_384_spec + crucible_return (crucible_term {{ if sign_F_p (sqrt_fp (uncompress_E1_y2 inp)) then zext 0b10 else (zero:[64]) }}); +}; + +// ... first error case, when the given X coordinate is too large +let POINTonE1_Uncompress_BE_BAD0_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + crucible_precond {{ uncompress_E1_x inp >= `p }}; + crucible_execute_func [out_ptr, in_ptr]; + crucible_return (crucible_term {{ (0:Limb) - `BLST_BAD_ENCODING }} ); +}; + +// ... second error case, when the X coordinate does not belong to a point on the curve +let POINTonE1_Uncompress_BE_BAD1_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + crucible_precond {{ uncompress_E1_x inp < `p }}; + crucible_precond {{ ~ (is_square_fp (uncompress_E1_y2 inp)) }}; + crucible_execute_func [out_ptr, in_ptr]; + crucible_return (crucible_term {{ (0:Limb) - `BLST_POINT_NOT_ON_CURVE }} ); +}; + +// Uncompress + +let POINTonE1_Uncompress_OK_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + + crucible_precond {{ (inp@0)@0 }}; // only dealing with compressed points + crucible_precond {{ ~ (inp@0)@1 }}; // not point-at-infinity + crucible_precond {{ uncompress_E1_x inp < `p }}; // given X is not too big + crucible_precond {{ is_square_fp (uncompress_E1_y2 inp) }}; // and is on the curve + crucible_execute_func [out_ptr, in_ptr]; + crucible_points_to out_ptr (crucible_term {{ POINTonE1_affine_rep (uncompress_E1_OK inp) }}); + crucible_return (crucible_term {{ if uncompress_E1_x_fp inp == Fp.field_zero + then `BLST_POINT_NOT_IN_GROUP + else `BLST_SUCCESS: [32] }}); + }; + +let POINTonE1_Uncompress_inf_OK_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + + crucible_precond {{ (inp@0)@0 }}; // only dealing with compressed points + crucible_precond {{ (inp@0)@1 }}; // point-at-infinity + crucible_precond {{ ~(inp@0)@2 }}; // sign bit clear + crucible_precond {{ uncompress_E1_x inp == zero }}; + + crucible_execute_func [out_ptr, in_ptr]; + + crucible_points_to out_ptr (crucible_term {{ POINTonE1_affine_rep (EC::point_O E) }}); + crucible_return (crucible_term {{ `BLST_SUCCESS: [32] }}); +}; + +let POINTonE1_Uncompress_inf_BAD_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + + crucible_precond {{ (inp@0)@0 }}; // only dealing with compressed points + crucible_precond {{ (inp@0)@1 }}; // point-at-infinity + crucible_precond {{ (inp@0)@2 \/ uncompress_E1_x inp != zero }}; + + crucible_execute_func [out_ptr, in_ptr]; + + crucible_return (crucible_term {{ `BLST_BAD_ENCODING: [32] }}); +}; + +// We do not care about specific error codes, so... +let POINTonE1_Uncompress_BAD_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + crucible_precond {{ ~ (inp@0)@1 }}; // not point-at-infinity + crucible_precond {{ ~ (inp@0)@0 + \/ uncompress_E1_x inp >= `p + \/ ~ is_square_fp (uncompress_E1_y2 inp) }}; // and is on the curve + crucible_execute_func [out_ptr, in_ptr]; + ret <- crucible_fresh_var "ret_POINTonE1_Uncompress" (llvm_int 32); + crucible_return (crucible_term {{ ret }}); + crucible_postcond {{ ret != `BLST_SUCCESS }}; + }; + +let POINTonE1_Uncompress_BAD1_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" (llvm_array 48 (llvm_int 8)); + crucible_precond {{ ~ (inp@0)@0 }}; // not compressed + crucible_execute_func [out_ptr, in_ptr]; + ret <- crucible_fresh_var "ret_POINTonE1_Uncompress" (llvm_int 32); + crucible_return (crucible_term {{ ret }}); + crucible_postcond {{ ret == `BLST_BAD_ENCODING }}; + }; + +// ... Deserialize (out of scope; the BLS ciphersuites use compression) +// but some analysis is included here in case we want to include these functions later. + +let POINTonE1_Deserialize_BE_BAD0_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Deserialize_in" (llvm_array 96 (llvm_int 8)); + // crucible_precond {{ deserialize_E1_x inp >= `p \/ deserialize_E1_y inp < `p }}; // given X or Y is too big + crucible_precond {{ deserialize_E1_x inp >= `p }}; // given X is too big + crucible_execute_func [out_ptr, in_ptr]; + crucible_return (crucible_term {{ `BLST_BAD_ENCODING: [32] }}); + }; + +let POINTonE1_Deserialize_BE_BAD0a_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Deserialize_in" (llvm_array 96 (llvm_int 8)); + // crucible_precond {{ deserialize_E1_x inp >= `p \/ deserialize_E1_y inp < `p }}; // given X or Y is too big + crucible_precond {{ deserialize_E1_y inp >= `p }}; // given Y is too big + crucible_execute_func [out_ptr, in_ptr]; + crucible_return (crucible_term {{ `BLST_BAD_ENCODING: [32] }}); + }; + +let POINTonE1_Deserialize_BE_BAD1_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Deserialize_in" (llvm_array 96 (llvm_int 8)); + crucible_precond {{ deserialize_E1_x inp < `p }}; // given X is not too big + crucible_precond {{ deserialize_E1_y inp < `p }}; // given Y is not too big + crucible_precond {{ ~ (is_point_affine E (deserialize_E1_x_fp inp, deserialize_E1_y_fp inp)) }}; // not on curve + crucible_execute_func [out_ptr, in_ptr]; + crucible_return (crucible_term {{ `BLST_POINT_NOT_ON_CURVE: [32] }}); + }; + +let POINTonE1_Deserialize_BE_OK_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Deserialize_in" (llvm_array 96 (llvm_int 8)); + crucible_precond {{ deserialize_E1_x inp < `p }}; // given X is not too big + crucible_precond {{ deserialize_E1_y inp < `p }}; // given Y is not too big + crucible_precond {{ is_point_affine E (deserialize_E1_x_fp inp, deserialize_E1_y_fp inp) }}; // on the curve + crucible_execute_func [out_ptr, in_ptr]; + crucible_points_to out_ptr (crucible_term {{ + (fp_rep (deserialize_E1_x_fp inp), fp_rep (deserialize_E1_y_fp inp)) }} ); + }; + +let POINTonE1_Deserialize_BE_OK_spec' = do { // For proof debugging + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Deserialize_in" (llvm_array 96 (llvm_int 8)); + crucible_precond {{ deserialize_E1_x inp < `p }}; // given X is not too big + crucible_precond {{ deserialize_E1_y inp < `p }}; // given Y is not too big + crucible_precond {{ is_point_affine E (deserialize_E1_x_fp inp, deserialize_E1_y_fp inp) }}; // on the curve + crucible_execute_func [out_ptr, in_ptr]; + w <- crucible_fresh_var "w" (llvm_struct "struct.POINTonE1_affine"); + crucible_points_to out_ptr (crucible_term w); + crucible_postcond {{ w.1 == fp_rep (deserialize_E1_y_fp inp) }}; + // {{ w.0 == fp_rep (deserialize_E1_x_fp inp) }} ? + }; + +// just to try: +let blst_p1_deserialize_inf_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE1_affine"); + inp <- crucible_fresh_var "p1_deserialize_in" (llvm_array 96 (llvm_int 8)); + in_ptr <- crucible_alloc_readonly (llvm_array 96 (llvm_int 8)); + crucible_points_to_untyped in_ptr (crucible_term inp); + crucible_precond {{ inp@0 && 0x80 == zero }}; // not compressed + crucible_precond {{ inp@0 && 0x40 != zero }}; // point at infinity + + crucible_execute_func [out_ptr, in_ptr]; + + new_out <- crucible_fresh_var "new_out" (llvm_struct "struct.POINTonE1_affine"); + ret <- crucible_fresh_var "ret" (llvm_int 32); + crucible_conditional_points_to {{ ret == `BLST_SUCCESS }} out_ptr (crucible_term new_out); + crucible_postcond {{ inp@0 && 0x40 != zero /\ ([inp@0 && 0x3F]#(tail inp)) == zero ==> ret == `BLST_SUCCESS /\ new_out.0 == vec384_rep (from_Fp (EC::point_O E).0) /\ new_out.1 == vec384_rep (from_Fp (EC::point_O E).1) }}; // TODO spec says 0x1F and not 0x3F + crucible_return (crucible_term ret); +}; + +// ... other overrides used in the proofs: + +// Not necessary, but useful when developing a proof, to keep the SAW +// formulas more readable. This override also appears in keygen.saw: TODO refactor +let limbs_from_be_bytes_spec48 = do { + ret_p <-crucible_alloc (llvm_array 6 limb_type); + (inx, in_ptr) <- ptr_to_fresh_readonly "limbs_from_be_bytes_in" + (llvm_array 48 (llvm_int 8)); // "in" is a keyword + crucible_execute_func [ret_p, in_ptr, crucible_term {{ 48:[64] }}]; + crucible_points_to ret_p (crucible_term {{ vec384_rep (join inx) }}); + }; + +let blst_p2_deserialize_spec = do { + out_ptr <- crucible_alloc (llvm_struct "struct.POINTonE2_affine"); + (_, in_ptr) <- ptr_to_fresh_readonly "in" (llvm_array 192 (llvm_int 8)); + crucible_execute_func [out_ptr, in_ptr]; + new_out <- crucible_fresh_var "new_out" (llvm_struct "struct.POINTonE2_affine"); + ret <- crucible_fresh_var "ret" (llvm_int 32); + crucible_conditional_points_to {{ ret == zero }} out_ptr (crucible_term new_out); + crucible_return (crucible_term ret); +}; + +let {{ + add_rep a = if vec384_abs a < `p then a else vec384_rep ((vec384_abs a) - `p) + }}; + +let add_fp_noabs_spec = do { + ret_ptr <- crucible_alloc vec384_type; + (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384_type; + (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384_type; + crucible_precond {{ b == zero }}; // make sure this override is applied only where we want it. + + crucible_execute_func [ret_ptr, a_ptr, b_ptr]; + crucible_points_to ret_ptr (crucible_term {{ add_rep a }}); + // {{ if vec384_abs a < `p then a else vec384_rep ((vec384_abs a) - `p) }}) ; +}; + +let sgn0_pty_mont_384_spec = do { + (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384_type; + (b, b_ptr) <- ptr_to_fresh_readonly "p" vec384_type; + crucible_precond {{ b == vec384_rep `p }}; + crucible_execute_func [a_ptr, b_ptr, crucible_term {{0x89f3fffcfffcfffd}}]; + return_value <- crucible_fresh_var "return_value" limb_type; + // TODO: Not sure what the return value should be. From what follows in the C code, it seems that the sign bit is the second bit of the return value. + crucible_return (crucible_term {{ (if (sign_F_p (fp_abs a)) then (zext 0b10) else zero):[64] }}); +}; + +//////////////////////////////////////////////////////////////////////////////// +// Proofs +//////////////////////////////////////////////////////////////////////////////// + +// Starting with proofs that the as-implemented algorithm matches the reference specification +// as-implemented has an additional check + +// We have a conditional property +// {{ \x -> fp_invariant x ==> Fp.mul (fp_abs x, montgomery_factor_p) == to_Fp (vec384_abs x) }} +// expressed as this conditional rewrite rule: +mul_to_fp_thm <- prove_cryptol + {{ \x -> Fp.mul (fp_abs x, montgomery_factor_p) == + if fp_invariant x + then to_Fp (vec384_abs x) + else apply Fp.mul (fp_abs x, montgomery_factor_p) }} + [] ; + +// "uncompress_OK" is the correct value in the non-infinity case + +prove_cryptol + {{ \ s -> (s@0)@1 // infinity bit is set, or + \/ maybe_cases (uncompress_E1_imp s) + True // the input is rejected + (\ p -> p == (uncompress_E1_OK s) ) }} // or accepted, giving the OK values + (concat ["sqrt_fp", "sign_F_p", "is_square_fp"] fp_unints); + +// The implementation must reject at least everything rejected by the spec +// (implied by the theorem that follows) +custom_prove_cryptol + {{ \s -> uncompress_E1 s == nothing ==> uncompress_E1_imp s == nothing }} + do { unfolding ["uncompress_E1", "uncompress_E1_imp", "uncompress_E1_x" + , "uncompress_E1_x_fp", "uncompress_E1_y2"]; + simplify (addsimp mul_to_fp_thm fp_simpset); + simplify (addsimps fp_alg_thms empty_ss); // resolve mul(sq x, x) vs mul (x, sq x) + unfolding ["fp_invariant"]; + w4_unint_z3 (concat ["sqrt_fp", "sign_F_p", "is_square_fp"] fp_unints); + }; + +// The implementation may reject more strings, but otherwise agrees with the spec: +custom_prove_cryptol + {{ \s -> maybe_cases (uncompress_E1_imp s) + True // may reject more + (\ P -> maybe_cases (uncompress_E1 s) + False // may not reject less + (\ Q -> P == Q)) }} ; // spec and impl deliver the same result + do { unfolding ["uncompress_E1", "uncompress_E1_imp", "uncompress_E1_x" + , "uncompress_E1_x_fp", "uncompress_E1_y2"]; + simplify (addsimp mul_to_fp_thm fp_simpset); + simplify (addsimps fp_alg_thms empty_ss); // resolve mul(sq x, x) vs mul (x, sq x) + unfolding ["fp_invariant"]; + w4_unint_z3 (concat ["sqrt_fp", "sign_F_p", "is_square_fp"] fp_unints); + }; + +// Now the code proofs + +add_fp_noabs_ov <- admit "add_fp" add_fp_noabs_spec; + +sgn0_pty_mont_384_ov <- admit "sgn0x_pty_mont_384" sgn0_pty_mont_384_spec; + +limbs_from_be_bytes_48_ov <- verify "limbs_from_be_bytes" [] limbs_from_be_bytes_spec48; + +blst_p1_deserialize_inf_ov <- verify "blst_p1_deserialize" [] blst_p1_deserialize_inf_spec; + +add_rep_invariant_thm <- prove_cryptol + {{ \ x -> fp_invariant x == (x == add_rep x) }} + []; + +let overrides_for_POINTonE1_Uncompress_BE = + foldr concat [sqrt_fp_ovs, fp_overrides] + [sgn0_pty_mont_384_ov, add_fp_noabs_ov, limbs_from_be_bytes_48_ov, vec_is_equal_48_vec_ov]; + +POINTonE1_Uncompress_BE_BAD0_ov <- custom_verify "POINTonE1_Uncompress_BE" + overrides_for_POINTonE1_Uncompress_BE + POINTonE1_Uncompress_BE_BAD0_spec + do { apply_fp_rewrites; + unfolding ["fp_invariant", "vec384_abs", "vec_abs"]; // evaluate this for BLS12_381_RR + w4_unint_z3 fp_unints;}; + + +// Cryptol can evaluate:fp_rep (montgomery_factor_p) +// [0xf4df1f341c341746, 0x0a76e6a609d104f1, 0x8de5476c4c95b6d5, +// 0x67eb88a9939d83c0, 0x9a793e85b519952d, 0x11988fe592cae3aa] + +fp_abs_RR_thm <- prove_cryptol + (rewrite (cryptol_ss ()) + {{ fp_abs [ 0xf4df1f341c341746, 0x0a76e6a609d104f1, 0x8de5476c4c95b6d5 + , 0x67eb88a9939d83c0, 0x9a793e85b519952d, 0x11988fe592cae3aa] + == montgomery_factor_p }}) + [] ; + +fp_inv_RR_thm <- prove_cryptol + (rewrite (cryptol_ss ()) + {{ fp_invariant [ 0xf4df1f341c341746, 0x0a76e6a609d104f1, 0x8de5476c4c95b6d5 + , 0x67eb88a9939d83c0, 0x9a793e85b519952d, 0x11988fe592cae3aa] + == True }}) + [] ; + +// Cryptol also can produce the value of `B_E1`: +//implementation::Field> fp_rep (to_Fp 4) +//[0xaa270000000cfff3, 0x53cc0032fc34000a, 0x478fe97a6b0a807f, +// 0xb1d37ebee6ba24d7, 0x8ec9733bbf78ab2f, 0x09d645513d83de7e] + +fp_abs_B_E1_thm <- prove_cryptol + (rewrite (cryptol_ss ()) + {{ fp_abs [ 0xaa270000000cfff3, 0x53cc0032fc34000a, 0x478fe97a6b0a807f + , 0xb1d37ebee6ba24d7, 0x8ec9733bbf78ab2f, 0x09d645513d83de7e] + == to_Fp 0x4 }}) []; + +fp_invariant_B_E1_thm <- prove_cryptol + (rewrite (cryptol_ss ()) + {{ fp_invariant [ 0xaa270000000cfff3, 0x53cc0032fc34000a, 0x478fe97a6b0a807f + , 0xb1d37ebee6ba24d7, 0x8ec9733bbf78ab2f, 0x09d645513d83de7e] + == True }}) []; + +POINTonE1_Uncompress_BE_BAD1_ov <- custom_verify "POINTonE1_Uncompress_BE" + overrides_for_POINTonE1_Uncompress_BE + POINTonE1_Uncompress_BE_BAD1_spec + do { apply_fp_rewrites; + simplify (addsimps [fp_abs_RR_thm, fp_inv_RR_thm, fp_abs_B_E1_thm, fp_invariant_B_E1_thm] empty_ss); + simplify (addsimp add_rep_invariant_thm empty_ss); // only after applying fp_inv_RR_thm! + w4_unint_z3 fp_unints;}; + +// The OK case, proper compressed input +POINTonE1_Uncompress_BE_OK_ov <- custom_verify "POINTonE1_Uncompress_BE" + overrides_for_POINTonE1_Uncompress_BE + POINTonE1_Uncompress_BE_OK_spec + do { apply_fp_rewrites; + simplify (addsimps [fp_abs_RR_thm, fp_inv_RR_thm, fp_abs_B_E1_thm, fp_invariant_B_E1_thm] empty_ss); + simplify (addsimp add_rep_invariant_thm empty_ss); // only after applying fp_inv_RR_thm! + w4_unint_z3 fp_unints;}; + +let POINTonE1_Uncompress_BE_overrides = + [POINTonE1_Uncompress_BE_OK_ov, POINTonE1_Uncompress_BE_BAD0_ov, POINTonE1_Uncompress_BE_BAD1_ov]; + +// Uncompress + +POINTonE1_Uncompress_inf_BAD_ov <- verify_unint "POINTonE1_Uncompress" [] fp_unints + POINTonE1_Uncompress_inf_BAD_spec; + +POINTonE1_Uncompress_inf_OK_ov <- verify "POINTonE1_Uncompress" [] POINTonE1_Uncompress_inf_OK_spec ; + +POINTonE1_Uncompress_OK_ov <- custom_verify + "POINTonE1_Uncompress" + (foldr concat [fp_overrides, vec_overrides] POINTonE1_Uncompress_BE_overrides) + POINTonE1_Uncompress_OK_spec + do {apply_fp_rewrites; + w4_unint_z3 (concat ["sign_F_p", "uncompress_E1_y2", "uncompress_E1_x_fp" + , "is_square_fp", "uncompress_E1_x"] + fp_unints);}; + +POINTonE1_Uncompress_BAD_ov <- custom_verify + "POINTonE1_Uncompress" + (foldr concat [fp_overrides, vec_overrides] POINTonE1_Uncompress_BE_overrides) + POINTonE1_Uncompress_BAD_spec + do {apply_fp_rewrites; + w4_unint_z3 (concat ["sign_F_p", "uncompress_E1_y2", "uncompress_E1_x_fp" + , "is_square_fp", "uncompress_E1_x"] + fp_unints);}; + +POINTonE1_Uncompress_BAD1_ov <- custom_verify + "POINTonE1_Uncompress" + (foldr concat [fp_overrides, vec_overrides] POINTonE1_Uncompress_BE_overrides) + POINTonE1_Uncompress_BAD1_spec + do {apply_fp_rewrites; + w4_unint_z3 (concat ["sign_F_p", "uncompress_E1_y2", "uncompress_E1_x_fp" + , "sqrt_fp", "is_square_fp", "uncompress_E1_x"] + fp_unints);}; + + +// Main result: blst_p1_uncompress + +point_O_rep <- prove_cryptol + {{ POINTonE1_affine_rep (point_O E) == zero }} + []; + +hoist_POINTonE1_affine_rep <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> POINTonE1_affine_rep (if c then p1 else p2) == + if c then POINTonE1_affine_rep p1 else POINTonE1_affine_rep p2 }}) + ["POINTonE1_affine_rep"]; + +blst_p1_uncompress_OK_ov <- custom_verify "blst_p1_uncompress" + [ POINTonE1_Uncompress_OK_ov //, POINTonE1_Uncompress_BAD_ov, POINTonE1_Uncompress_BAD1_ov + , POINTonE1_Uncompress_inf_OK_ov] // , POINTonE1_Uncompress_inf_BAD_ov] + blst_p1_uncompress_OK_spec + do { + unfolding ["uncompress_E1_imp", "uncompress_E1_x"]; + simplify fp_simpset; + simplify (addsimps [point_O_rep, hoist_POINTonE1_affine_rep] empty_ss); + w4_unint_z3 (concat ["sign_F_p", "sqrt_fp", "is_square_fp"] fp_unints); + }; + +// Deserialize + +POINTonE1_Deserialize_BE_BAD0_ov <- custom_verify + "POINTonE1_Deserialize_BE" + (foldr concat [fp_overrides, vec_overrides] + [POINTonE1_affine_on_curve_ov, add_fp_noabs_ov, limbs_from_be_bytes_48_ov, vec_is_equal_48_vec_ov]) + POINTonE1_Deserialize_BE_BAD0_spec + do {apply_fp_rewrites; + simplify (addsimps [fp_abs_RR_thm, fp_inv_RR_thm] empty_ss); + simplify (addsimp add_rep_invariant_thm empty_ss); + unfolding ["POINTonE1_affine_invariant"]; + apply_fp_rewrites; + (w4_unint_z3 fp_unints);}; + +POINTonE1_Deserialize_BE_BAD0a_ov <- custom_verify + "POINTonE1_Deserialize_BE" + (foldr concat [fp_overrides, vec_overrides] + [POINTonE1_affine_on_curve_ov, add_fp_noabs_ov, limbs_from_be_bytes_48_ov, vec_is_equal_48_vec_ov]) + POINTonE1_Deserialize_BE_BAD0a_spec + do {apply_fp_rewrites; + simplify (addsimps [fp_abs_RR_thm, fp_inv_RR_thm] empty_ss); + simplify (addsimp add_rep_invariant_thm empty_ss); + unfolding ["POINTonE1_affine_invariant"]; + apply_fp_rewrites; + (w4_unint_z3 fp_unints);}; diff --git a/proof/exp.saw b/proof/exp.saw index 0b31bef0..06b5ead5 100644 --- a/proof/exp.saw +++ b/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,7 +138,8 @@ 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; @@ -141,7 +147,8 @@ let reciprocal_fp_spec = do { 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,25 +161,18 @@ 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; @@ -180,6 +180,7 @@ let recip_sqrt_fp_spec = do { 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]; diff --git a/proof/functional_proofs.saw b/proof/functional_proofs.saw index 5840c850..f8631a9b 100644 --- a/proof/functional_proofs.saw +++ b/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"; \ No newline at end of file +include "curve_operations_e2.saw"; +include "deserialize-p1.saw"; diff --git a/proof/proof-helpers.saw b/proof/proof-helpers.saw index de01b757..c86fcccf 100644 --- a/proof/proof-helpers.saw +++ b/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; + }; + + diff --git a/proof/vect.saw b/proof/vect.saw index ce4873d7..1d807ea3 100644 --- a/proof/vect.saw +++ b/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: diff --git a/scripts/build_llvm.sh b/scripts/build_llvm.sh index c4ef664c..762cbe35 100755 --- a/scripts/build_llvm.sh +++ b/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 diff --git a/spec/Serialization.cry b/spec/Serialization.cry index 9efa1d47..12483885 100755 --- a/spec/Serialization.cry +++ b/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 diff --git a/spec/implementation/serialization.cry b/spec/implementation/serialization.cry new file mode 100644 index 00000000..e214a801 --- /dev/null +++ b/spec/implementation/serialization.cry @@ -0,0 +1,78 @@ +module implementation::serialization where + +import Parameters (p, E, E', t_Fp, to_Fp, t_Fp_2, Fp, Fp_2) +import ShortWeierstrassCurve as EC +import rfc8017 +import Maybe +import FieldExtras (F_expt) +import BLSFieldExtras +import Serialization +import implementation::Types +import implementation::Field + +// deserialization of compressed representations + +uncompress_E1_x: [48][8] -> [384] +uncompress_E1_x s_string = x where + s_string' = [(s_string@0) && 0x1F] # tail s_string + // Step 6 + x = join s_string' // OS2IP(s_string') + +uncompress_E1_x_fp: [48][8] -> t_Fp +uncompress_E1_x_fp s_string = + Fp.mul (fp_abs (vec384_rep (uncompress_E1_x s_string)), montgomery_factor_p) + +uncompress_E1_y2: [48][8] -> t_Fp +uncompress_E1_y2 s_string = y2 where + // x = to_Fp (uncompress_E1_x s_string) + x = Fp.mul ( fp_abs (vec384_rep (uncompress_E1_x s_string)) + , montgomery_factor_p) // we will prove this = to_Fp ... + y2 = Fp.add (Fp.mul (Fp.sq x, x), 4) + +uncompress_E1_y: [48][8] -> t_Fp +uncompress_E1_y s_string = sqrt_fp (uncompress_E1_y2 s_string) + +uncompress_E1_imp: [48][8] -> Maybe (EC::AffinePoint t_Fp) +uncompress_E1_imp 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 + s_string' = [(s_string@0) && 0x1F] # tail s_string + x = uncompress_E1_x_fp s_string + y2 = uncompress_E1_y2 s_string + y = sqrt_fp y2 + Y_bit = sign_F_p y + ret = if C_bit == False then nothing // Error, from Step 2 + | I_bit then (if ~S_bit /\ s_string' == zero then just (EC::point_O E) else nothing) + | uncompress_E1_x s_string >= `p then nothing // extra check in the C code + | ~ (is_square_fp y2) then nothing // from Step 7 + | S_bit == Y_bit then just (x,y) + else just (x, Fp.neg y) + + +uncompress_E1_OK: [48][8] -> EC::AffinePoint t_Fp +uncompress_E1_OK s_string = if S_bit == Y_bit then (x,y) else (x, Fp.neg y) where + x = uncompress_E1_x_fp s_string + y = uncompress_E1_y s_string + S_bit = (s_string@0)@2 + Y_bit = sign_F_p y + +// deserialization of uncompressed representations + +deserialize_E1_x: [96][8] -> [384] +deserialize_E1_x s_string = x where + s_string' = take`{48} ([(s_string@0) && 0x1F] # tail s_string) + x = join s_string' + +deserialize_E1_x_fp: [96][8] -> t_Fp +deserialize_E1_x_fp s_string = + Fp.mul (fp_abs (vec384_rep (deserialize_E1_x s_string)), montgomery_factor_p) + +deserialize_E1_y: [96][8] -> [384] +deserialize_E1_y s_string = join (drop`{48} s_string) + +deserialize_E1_y_fp: [96][8] -> t_Fp +deserialize_E1_y_fp s_string = + Fp.mul (fp_abs (vec384_rep (deserialize_E1_y s_string)), montgomery_factor_p) diff --git a/tests/SerializationTests.cry b/tests/SerializationTests.cry index cd405f26..02db8de1 100755 --- a/tests/SerializationTests.cry +++ b/tests/SerializationTests.cry @@ -9,7 +9,7 @@ import ShortWeierstrassCurve as EC import Maybe property ser_des_E1 (m:[16]) = - deserialize_E1 (serialize_E1 Q) == just Q where Q = EC::mult E m BP + deserialize_E1 ((serialize_E1 Q) # zero) == just Q where Q = EC::mult E m BP property ser_des_E2 (m:[16]) = deserialize_E2 (serialize_E2 Q) == just Q where Q = EC::mult E' m BP'