diff --git a/patches/blst_header.patch b/patches/blst_header.patch new file mode 100644 index 00000000..a4152d6b --- /dev/null +++ b/patches/blst_header.patch @@ -0,0 +1,41 @@ +diff --git a/bindings/blst.h b/bindings/blst.h +index 3a333b1..cbd3642 100644 +--- a/bindings/blst.h ++++ b/bindings/blst.h +@@ -168,10 +168,10 @@ bool blst_p1_is_equal(const blst_p1 *a, const blst_p1 *b); + bool blst_p1_is_inf(const blst_p1 *a); + const blst_p1 *blst_p1_generator(); + +-bool blst_p1_affine_on_curve(const blst_p1_affine *p); +-bool blst_p1_affine_in_g1(const blst_p1_affine *p); ++limb_t blst_p1_affine_on_curve(const blst_p1_affine *p); ++limb_t blst_p1_affine_in_g1(const blst_p1_affine *p); + bool blst_p1_affine_is_equal(const blst_p1_affine *a, const blst_p1_affine *b); +-bool blst_p1_affine_is_inf(const blst_p1_affine *a); ++limb_t blst_p1_affine_is_inf(const blst_p1_affine *a); + const blst_p1_affine *blst_p1_affine_generator(); + + typedef struct { blst_fp2 x, y, z; } blst_p2; +@@ -194,10 +194,10 @@ bool blst_p2_is_equal(const blst_p2 *a, const blst_p2 *b); + bool blst_p2_is_inf(const blst_p2 *a); + const blst_p2 *blst_p2_generator(); + +-bool blst_p2_affine_on_curve(const blst_p2_affine *p); +-bool blst_p2_affine_in_g2(const blst_p2_affine *p); ++limb_t blst_p2_affine_on_curve(const blst_p2_affine *p); ++limb_t blst_p2_affine_in_g2(const blst_p2_affine *p); + bool blst_p2_affine_is_equal(const blst_p2_affine *a, const blst_p2_affine *b); +-bool blst_p2_affine_is_inf(const blst_p2_affine *a); ++limb_t blst_p2_affine_is_inf(const blst_p2_affine *a); + const blst_p2_affine *blst_p2_affine_generator(); + + /* +@@ -351,7 +351,7 @@ BLST_ERROR blst_core_verify_pk_in_g1(const blst_p1_affine *pk, + size_t aug_len DEFNULL); + BLST_ERROR blst_core_verify_pk_in_g2(const blst_p2_affine *pk, + const blst_p1_affine *signature, +- bool hash_or_encode, ++ int hash_or_encode, + const byte *msg, size_t msg_len, + const byte *DST DEFNULL, + size_t DST_len DEFNULL, diff --git a/proof/aggregate_in_g2.saw b/proof/aggregate_in_g2.saw index ede3d539..e1cbe680 100644 --- a/proof/aggregate_in_g2.saw +++ b/proof/aggregate_in_g2.saw @@ -5,7 +5,7 @@ // NOTE: we only consider inputs that either have the infinity-bit set or compressed-bit set -// aggregate_in_g2_error_precond describes the circumstances under which aggregate_in_g2 returns an error (assuming either the compressed bit is set of the infinity bit is set) +// aggregate_in_g2_error_precond describes the circumstances under which aggregate_in_g2 returns an error (assuming either the compressed bit is set or the infinity bit is set) let {{ aggregate_in_g2_error_precond : [96][8] -> Bool aggregate_in_g2_error_precond zwire = @@ -95,7 +95,8 @@ let overrides = foldr concat [vec_overrides,curve_operations_e2_ovs] [POINTonE2_ // Assumptions -uncompress_not_point_O <- admit_cryptol {{ \x -> (is_point_O E' (uncompress_E2_OK x)) == if uncompress_E2_x_fp x != Fp_2.field_zero then False else apply is_point_O E' (uncompress_E2_OK x) }}; +// uncompressing a valid point that does not have the infinity bit set does not return point_O: +uncompress_not_point_O <- admit_cryptol {{ \x -> (is_point_O E' (uncompress_E2_OK x)) == if (uncompress_E2_imp x != nothing) then False else apply is_point_O E' (uncompress_E2_OK x) }}; uncompress_on_curve <- admit_cryptol {{ \x -> (is_point_affine E' (uncompress_E2_OK x)) == True }}; diff --git a/proof/api-extra-for-release-2.saw b/proof/api-extra-for-release-2.saw index 1359d9a0..f8e0bc1b 100644 --- a/proof/api-extra-for-release-2.saw +++ b/proof/api-extra-for-release-2.saw @@ -1,6 +1,6 @@ /* -Copyright (c) 2020 Galois, Inc. -SPDX-License-Identifier: Apache-2.0 OR MIT + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT */ blst_p1_affine_in_g1_ov <- verify_unint "blst_p1_affine_in_g1" diff --git a/proof/bls_operations.c b/proof/bls_operations.c new file mode 100644 index 00000000..86c70deb --- /dev/null +++ b/proof/bls_operations.c @@ -0,0 +1,138 @@ +#include "blst.h" +#include // for NULL + +// TODO: Move + +// Two variants: +// _A: min signature size +// _B: min pk size + +// Explicitly note that demo_DST_A is 43 bytes to avoid the null terminator +// (needed for SAW to treat the allocation as 32 bytes) +byte demo_DST_A[43] = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_"; +byte demo_DST_B[43] = "BLS_SIG_BLS12381G2_XMD:SHA-256_SSWU_RO_NUL_"; + +// KeyGen maps directly to blst_keygen + +// SkToPk +void demo_SkToPk_A(unsigned char out[96], const blst_scalar *SK) { + blst_p2 pk; + blst_sk_to_pk_in_g2(&pk, SK); + blst_p2_compress(out, &pk); + } + +void demo_SkToPk_B(unsigned char out[48], const blst_scalar *SK) { + blst_p1 pk; + blst_sk_to_pk_in_g1(&pk, SK); + blst_p1_compress(out, &pk); +}; + +// KeyValidate + +limb_t demo_KeyValidate_A(const unsigned char in[96]) { + blst_p2_affine pk; + BLST_ERROR r; + r = blst_p2_uncompress(&pk, in); + /* + return r == BLST_SUCCESS && + blst_p2_affine_on_curve(&pk) && + !blst_p2_affine_is_inf(&pk) && + blst_p2_affine_in_g2(&pk); + */ + if (r != BLST_SUCCESS) return 0; + if (! blst_p2_affine_on_curve(&pk)) return 0; + if (blst_p2_affine_is_inf(&pk)) return 0; + if (! blst_p2_affine_in_g2(&pk)) return 0; + return 1; +}; + +limb_t demo_KeyValidate_B(const unsigned char in[48]) { + blst_p1_affine pk; + BLST_ERROR r; + r = blst_p1_uncompress(&pk, in); + if (r != BLST_SUCCESS) return 0; + if (! blst_p1_affine_on_curve(&pk)) return 0; + if (blst_p1_affine_is_inf(&pk)) return 0; + if (! blst_p1_affine_in_g1(&pk)) return 0; + return 1; +}; + + +// BasicSign + +void demo_BasicSign_A(byte out[48], const blst_scalar *SK, + const byte *message, size_t message_len) { + // TODO: Figure out how to use globals in SAW? + //const byte local_DST_A[] = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_AUG_"; + blst_p1 Q1, Q2; + // TODO: Double check, but I think aug is supposed to be a public key? That + // will determine the size it should be. + // TODO: Is DST_len supposted to include the null terminator? It's 44 with + // the null terminator, and 43 without. + blst_hash_to_g1(&Q1, message, message_len, demo_DST_A, 43, NULL, 0); // no "aug" string + // blst_p1_mult(&Q, &Q, SK, 256); // or 255? + blst_sign_pk_in_g2(&Q2, &Q1, SK); + blst_p1_compress(out, &Q2); +}; + +void demo_BasicSign_B(byte out[96], const blst_scalar *SK, + const byte *message, size_t message_len) { + blst_p2 Q1, Q2; + blst_hash_to_g2(&Q1, message, message_len, demo_DST_B, 43, NULL, 0); // no "aug" string + blst_sign_pk_in_g1(&Q2, &Q1, SK); + blst_p2_compress(out, &Q2); +}; + +// BasicVerify + +limb_t demo_BasicVerify_A(const byte sig[48], const byte pk[96], const byte *message, size_t message_len) { + blst_p1_affine R; + blst_p1 Q; + blst_p2_affine PK; + // uncompress and check the sig + if (blst_p1_uncompress(&R, sig) != BLST_SUCCESS) return 0; + if (! blst_p1_affine_on_curve(&R)) return 0; + if (blst_p1_affine_is_inf(&R)) return 0; + if (! blst_p1_affine_in_g1(&R)) return 0; + + if (!demo_KeyValidate_A(pk)) return 0; + + // TODO: Use KeyValidate below instead to better match the spec? + // uncompress and check the pub key + if (blst_p2_uncompress(&PK, pk) != BLST_SUCCESS) return 0; + /* + if (! blst_p2_affine_on_curve(&PK)) return 0; + if (blst_p2_affine_is_inf(&PK)) return 0; + if (! blst_p2_affine_in_g2(&PK)) return 0; + */ + + if (blst_core_verify_pk_in_g2(&PK, &R, 1, message, message_len, demo_DST_A, 43, NULL, 0) != BLST_SUCCESS) + return 0; + return 1; +}; + +bool demo_BasicVerify_B(const byte sig[96], const byte pk[48], const byte *message, size_t message_len) { + blst_p2_affine R; + blst_p2 Q; + blst_p1_affine PK; + // uncompress and check the sig + if (blst_p2_uncompress(&R, sig) != BLST_SUCCESS) return 0; + if (! blst_p2_affine_on_curve(&R)) return 0; + if (blst_p2_affine_is_inf(&R)) return 0; + if (! blst_p2_affine_in_g2(&R)) return 0; + + // TODO: Maybe remove the above checks if the override handles error cases. + // Can't remove pubkey checks? (Same goes for A variant) + + // uncompress and check the pub key + if (blst_p1_uncompress(&PK, pk) != BLST_SUCCESS) return 0; + if (! blst_p1_affine_on_curve(&PK)) return 0; + if (blst_p1_affine_is_inf(&PK)) return 0; + if (! blst_p1_affine_in_g1(&PK)) return 0; + + + // TODO: fix DST string + if (blst_core_verify_pk_in_g1(&PK, &R, 1, message, message_len, demo_DST_A, 43, NULL, 0) != BLST_SUCCESS) + return 0; + return 1; +}; diff --git a/proof/bls_operations.saw b/proof/bls_operations.saw new file mode 100644 index 00000000..525e882b --- /dev/null +++ b/proof/bls_operations.saw @@ -0,0 +1,1099 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +import "../spec/BLSMinimalSignatureSize.cry"; + +let do_prove = true; + +let {{ + drop_join_reverse: {n_bits, n_bytes} (fin n_bytes, n_bits <= 8*n_bytes) => [n_bytes][8] -> [n_bits] + drop_join_reverse bytes = drop`{back=n_bits} (join (reverse bytes)) + + same_point_affine_E' = same_point_affine E' + same_point_affine_E = same_point_affine E + + is_bad_O_form_E: POINTonE1_t -> Bool + is_bad_O_form_E P = ((is_point_O E (fp_abs P.0, fp_abs P.1)) /\ + (fp_abs (P.2) != Fp.field_zero)) \/ + ((~(is_point_O E (fp_abs P.0, fp_abs P.1))) /\ + fp_abs (P.2) == Fp.field_zero) + + is_bad_O_form_E': POINTonE2_t -> Bool + is_bad_O_form_E' P = ((is_point_O E' (fp2_abs P.0, fp2_abs P.1)) /\ + (fp2_abs (P.2) != Fp_2.field_zero)) \/ + ((~(is_point_O E' (fp2_abs P.0, fp2_abs P.1))) /\ + fp2_abs (P.2) == Fp_2.field_zero) + + pubkey_to_point_is_affine: [96][8] -> Bool + pubkey_to_point_is_affine pk = + maybe_cases (pubkey_to_point (join pk)) + False + (\y -> is_point_affine E' y) + + signature_to_point_is_affine: [48][8] -> Bool + signature_to_point_is_affine sig = + maybe_cases (signature_to_point (join sig)) + False + (\y -> is_point_affine E y) +}}; + +same_point_affine_E_thm <- prove_cryptol + {{ \P1 P2 -> same_point_affine E P1 P2 == same_point_affine_E P1 P2 }} []; + +let demo_SkToPk_A_spec = do { + let n_bytes = 32; + let bits = 255; + out_ptr <- llvm_alloc (llvm_array 96 (llvm_int 8)); + scalar_ptr <- crucible_alloc_readonly_aligned 8 (llvm_array n_bytes (llvm_int 8)); + scalar <- crucible_fresh_var "scalar" (llvm_array n_bytes (llvm_int 8)); + crucible_points_to scalar_ptr (crucible_term scalar); + // extra precondition from POINTonE2_mult_w5 + crucible_precond {{ e2_order BP' > scalar_value`{bits,n_bytes} scalar + shift }}; + llvm_precond {{ scalar != zero }}; + llvm_execute_func [out_ptr, scalar_ptr]; + // TODO: is this `join . reverse` (and `reverse . split`) necessary? Seems + // like an endianness conversion? + // TODO: I *think* you only need the endianness reversal going in, but it + // isn't necessary on the way out because the key is supposed to be big + // endian. Double check though. + //llvm_points_to out_ptr (llvm_term {{ reverse (split`{each=8} (sk_to_pk (drop_join_reverse scalar))) }}); + llvm_points_to out_ptr (llvm_term {{ (split`{each=8} (sk_to_pk (drop_join_reverse scalar))) }}); +}; + +let or_core = parse_core "or"; +let not_core = parse_core "not"; +let and_core = parse_core "and"; + +affine_inv_affine_rep_e2_thm <- custom_prove_cryptol + {{ \P -> POINTonE2_affine_invariant (POINTonE2_affine_rep P) == True }} + do { + unfolding [ "POINTonE2_affine_rep" , "POINTonE2_affine_invariant" ]; + rw_with fp2_rep_thms; + print_goal; + w4_unint_z3 []; + }; + +affine_E'_inv_thm <- test_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> + (and_core (same_point_affine E' (affinify E' (POINTonE2_abs P1)) P2) + (and_core (POINTonE2_invariant P1) + (and_core (not_core (is_bad_O_form_E' P1)) + (is_point_projective E' (POINTonE2_abs P1))))) == + (same_point_affine E' (affinify E' (POINTonE2_abs P1)) P2 /\ + ~(is_bad_O_form_E' P1) /\ + is_point_affine E' P2) }}); + +// NOTE: Too slow to quickcheck +e2_scalar_mult_on_curve_thm <- admit_cryptol + {{ \sk P -> is_point_affine E' (e2_scalar_mult sk P) == + if is_point_affine E' P + then True + else apply is_point_affine E' (e2_scalar_mult sk P) }}; + +BP'_is_point_affine_thm <- prove_cryptol + {{ is_point_affine E' BP' == True }} []; + +let boolEq_core = parse_core "boolEq"; + +and_true_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b1 b2 -> boolEq_core (and_core b1 b2) (b1 /\ (b2 /\ True)) == True }}) []; + +e2_scalar_mult_not_bad_O_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \P sk -> (same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) BP')) == + ((apply same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) BP')) && + ~(is_bad_O_form_E' P)) }}); + +same_point_affine_E'_thm <- prove_cryptol + {{ \P1 P2 -> same_point_affine E' P1 P2 == same_point_affine_E' P1 P2 }} []; + + +// Can't use normal conditional formulation because "sk" is a fresh var that +// exists only on the right hand side of the substitution, so the override +// never applies +test_thm_correct <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P sk -> (same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) BP')) == + ((apply same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) BP')) && + POINTonE2_invariant P && + ~(is_bad_O_form_E' P) && + is_point_projective E' (POINTonE2_abs P)) }}) + do { + rw_with_1 e2_scalar_mult_not_bad_O_thm; + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps [ affine_E'_inv_thm + , affine_inv_affine_rep_e2_thm + , e2_scalar_mult_on_curve_thm + , BP'_is_point_affine_thm ] empty_ss); + simplify basic_ss; + simplify (addsimp same_point_affine_E'_thm empty_ss); + print_goal; + w4_unint_z3 (concat [ "e2_scalar_mult" + , "is_bad_O_form_E'" + , "scalar_value" + , "same_point_affine_E'" ] + e2_unints); + }; + +mult_scalar_mult_thm <- admit_cryptol + {{ \b P -> mult E' b P == e2_scalar_mult (toInt b) P }}; + +fold_scalar_value_thm <- prove_cryptol + {{ \x -> toInt`{255} (drop_join_reverse`{255, 32} x) == scalar_value`{255, 32} x }} []; + +split_join_thms <- for [48, 96] + (\x -> prove_cryptol (rewrite (cryptol_ss()) + {{ \v -> split`{x, 8, Bool} (join`{x, 8, Bool} v) == v }}) []); + +let vecEq = parse_core "vecEq 96 (Vec 8 Bool) (bvEq 8)"; + +is_equal_thms <- for + [ {{ \ x y -> E.base_field.is_equal (x,y) == (x==y) }} + , {{ \ x y -> E'.base_field.is_equal (x,y) == (x==y) }} + ] (\ t -> prove_cryptol t []); + +serialize_e2_eq_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> (vecEq (serialize_E2 P1) (serialize_E2 P2)) == + if same_point_affine E' P1 P2 + then True + else apply vecEq (serialize_E2 P1) (serialize_E2 P2) }}) + ["serialize_E2"]; + +point_e2_eq <- parse_core "pairEq (Vec 2 Integer) (Vec 2 Integer) (vecEq 2 Integer intEq) (vecEq 2 Integer intEq)"; + +eq_to_same_point_affine_E'_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> (point_e2_eq P1 P2) == same_point_affine E' P1 P2 }}) []; + + // TODO: This feels provable +affinify_affine_thm <- test_cryptol + {{ \P -> serialize_E2 (fp2_abs P.0, fp2_abs P.1) == + if (fp2_abs P.2) == Fp_2.field_unit + then serialize_E2 (affinify E' (POINTonE2_abs P)) + else apply serialize_E2 (fp2_abs P.0, fp2_abs P.1) }}; + +include "horrible_core_terms.saw"; + +if_elim_thms <- for at_96_cores + (\x -> prove_cryptol (rewrite (cryptol_ss()) + {{ \b1 b2 b3 (x1 : [96][8]) (x2 : [96][8]) -> + (if (and_core (and_core b1 b2) b3) + then x (if b2 then x1 else x2) + else (x x1)) == (x x1) }}) []); + +O_O_unit_implies_bad_O_form_E' <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> (is_bad_O_form_E' P) == + if (is_point_O E' (fp2_abs P.0, fp2_abs P.1)) /\ + (fp2_abs (P.2) == Fp_2.field_unit) + then True + else apply is_bad_O_form_E' P }}) []; + +demo_SkToPk_A_ov <- custom_verify "demo_SkToPk_A" + [blst_sk_to_pk_in_g2_ov, blst_p2_compress_projective_ov, blst_p2_compress_affine_ov] + demo_SkToPk_A_spec + do { + unfolding [ "sk_to_pk" + , "module parameter point_to_pubkey" + , "module parameter other_curve" + , "module parameter P" + , "other_curve" + , "P" + , "point_to_pubkey" ]; + simplify (cryptol_ss()); + simplify (addsimp eq_to_same_point_affine_E'_thm empty_ss); + simplify (addsimps [test_thm_correct] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 O_O_unit_implies_bad_O_form_E'; + // BEGIN final goal proof + simplify (addsimps (concat split_join_thms + [mult_scalar_mult_thm, + affinify_affine_thm, + fold_scalar_value_thm, + serialize_e2_eq_thm]) + empty_ss); + simplify (addsimps split_join_thms empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps if_elim_thms empty_ss); + simplify (addsimps [unrip_thm_96, serialize_e2_eq_thm] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["apply"]; + simplify remove_higher_order_function_simpset; + simplify (addsimp same_point_affine_E'_thm empty_ss); + print_goal; + w4_unint_z3 (concat [ "e2_order" + , "scalar_value" + , "POINTonE2_abs" + , "serialize_E2" + , "fp2_abs" + , "e2_scalar_mult" + , "same_point_affine_E'" + , "POINTonE2_invariant" ] + e2_unints); + }; + +let demo_KeyValidate_A_spec = do { + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE2_Uncompress_in" compressed_E2_rep_type; + crucible_precond {{ uncompress_E2_imp inp != nothing }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ ~((inp@0)@1) }}; + //llvm_precond {{ is_point_affine E' ((pubkey_to_point (join inp)).1) }}; + llvm_precond {{ pubkey_to_point_is_affine inp }}; + llvm_execute_func [ in_ptr ]; + llvm_return (llvm_term {{ bool_to_limb (KeyValidate (join inp)) }}); +}; + +uncompress_E2_OK_on_curve <- admit_cryptol + {{ \x -> is_point_affine E' (uncompress_E2_OK x) == + if uncompress_E2_imp x != nothing + then True + else is_point_affine E' (uncompress_E2_OK x) }}; + +is_point_O_E'_affine_rev_thm <- prove_cryptol + {{ \x y -> (Fp_2.is_equal (x, Fp_2.field_zero) /\ + Fp_2.is_equal (y, Fp_2.field_zero)) == + is_point_O E' (x, y) }} []; + +just_thm <- prove_cryptol (rewrite (cryptol_ss()) {{ \(x : AffinePoint t_Fp_2) -> just x == (True, x) }}) []; + +// We assume that pubkey_subgroup_check is equivalent to is_in_g2_impl for +// points on the curve. This assumption is proved in Bowe "Faster Subgroup +// Checks for BLS12-381". +is_in_g2_impl_thm <- admit_cryptol + (rewrite (cryptol_ss()) + {{ \P -> pubkey_subgroup_check P == + if is_point_affine_E' P + then is_in_g2_impl P + else apply pubkey_subgroup_check P }}); + +hoist_POINTonE2_affine_invariant <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> POINTonE2_affine_invariant (if c then p1 else p2) == + if c then POINTonE2_affine_invariant p1 else POINTonE2_affine_invariant p2 }}) + ["POINTonE2_affine_invariant"]; + +// TODO: Is this proved somewhere? +deserialize_E2_uncompress_E2_OK_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \x -> deserialize_E2 x == + if uncompress_E2_imp x != nothing + then (True, uncompress_E2_OK x) + else apply deserialize_E2 x }}); + +fold_normalize_affine_fp2_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> (Fp_2.normalize P.0, Fp_2.normalize P.1) == + normalize_affine_point Fp_2 P }}) []; + +hoist_normalize_affine_fp2_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b P1 P2 -> normalize_affine_point Fp_2 (if b then P1 else P2) == + if b + then normalize_affine_point Fp_2 P1 + else normalize_affine_point Fp_2 P2 }}) []; + +hoist_pair_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b (x : t_Fp_2) (y : t_Fp_2) -> (x, if b then y else x) == + if b then (x, y) else (x, x) }}) []; + +normalize_point_O_E'_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ normalize_affine_point Fp_2 (point_O E') == point_O E' }}) []; + +unfold_Fp_2_normalize_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \(x : t_Fp_2) -> (Fp_2.normalize x == + [Fp.normalize x0, Fp.normalize x1] where + [x0, x1] = x) }}) []; + +include "print_readably.saw"; + +normalize_uncompress_E2_OK_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \x -> normalize_affine_point Fp_2 (uncompress_E2_OK x) == + uncompress_E2_OK x }}) + do { + unfolding ["uncompress_E2_OK", "uncompress_E2_x_fp", "uncompress_E2_y"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps [hoist_normalize_affine_fp2_thm] empty_ss); + unfolding ["normalize_affine_point"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps fp2_laws empty_ss); + simplify (addsimps [normalize_sqrt_fp2_thm] empty_ss); + simplify (addsimps [unfold_Fp_2_normalize_thm] empty_ss); + simplify (addsimps fp_laws empty_ss); + print_goal; + print_readably; + w4_unint_z3 fp2_unints; + }; + +demo_KeyValidate_A_ov <- custom_verify "demo_KeyValidate_A" + [ blst_p2_uncompress_OK_ov + , POINTonE2_affine_on_curve_ov + , vec_is_zero_2fp2_ov + , blst_p2_affine_in_g2_ov ] + demo_KeyValidate_A_spec + do { + unfolding [ "KeyValidate" + , "maybe_cases" + , "module parameter pubkey_to_point" + , "module parameter other_curve" + , "bool_to_limb" + , "POINTonE2_affine_rep" + , "pubkey_to_point_is_affine" + , "POINTonE2_affine_abs" + , "other_curve" + , "pubkey_to_point" + , "reexport_pubkey_subgroup_check" + , "module parameter pubkey_subgroup_check"]; + simplify (addsimp is_point_affine_E'_thm empty_ss); + simplify (addsimps [ uncompress_E2_OK_on_curve] empty_ss); + simplify basic_ss; + simplify (addsimp is_point_O_E'_affine_rev_thm empty_ss); + simplify (cryptol_ss()); + simplify (addsimps core_rewrites empty_ss); + simplify (addsimp fp2_abs_ite_thm empty_ss); + simplify fp2_simpset; + simplify (addsimp is_in_g2_impl_thm empty_ss); + simplify basic_ss; + simplify (addsimp is_point_O_E'_thm empty_ss); + simplify (basic_ss); + simplify (addsimps [ hoist_POINTonE2_affine_rep + , affine_inv_affine_rep_e2_thm + , hoist_POINTonE2_affine_invariant ] empty_ss); + simplify (basic_ss); + simplify (cryptol_ss()); + simplify (addsimps core_rewrites empty_ss); + simplify (addsimps split_join_thms empty_ss); + simplify (addsimps [ deserialize_E2_uncompress_E2_OK_thm ] empty_ss); + simplify remove_higher_order_function_simpset; + goal_num_ite 4 + (do { + simplify (addsimp just_thm empty_ss); + simplify (basic_ss); + simplify (cryptol_ss()); + simplify (addsimps [ fold_normalize_affine_fp2_thm + , hoist_pair_thm + , normalize_point_O_E'_thm + , normalize_uncompress_E2_OK_thm + , hoist_normalize_affine_fp2_thm ] empty_ss); + simplify (basic_ss); + simplify (cryptol_ss()); + (print_goal); + w4_unint_z3 [ "is_in_g2_impl" + , "uncompress_E2_OK" + , "is_point_affine_E'" + , "pubkey_subgroup_check" + , "is_point_O_E'" + , "is_point_affine_E'" + , "deserialize_E2" + , "POINTonE2_affine_invariant" + , "fp2_rep" + , "uncompress_E2_imp"]; + }) + (do { + (print_goal); + w4_unint_z3 [ "is_in_g2_impl" + , "uncompress_E2_OK" + , "is_point_affine_E'" + , "pubkey_subgroup_check" + , "is_point_O_E'" + , "is_point_affine_E'" + , "deserialize_E2" + , "uncompress_E2_imp"]; + }); + }; + +let demo_BasicSign_A_spec = do { + //let DST = {{ "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_" }}; + global_alloc_init "demo_DST_A" {{ DST }}; + let msg_len = 32; + out_ptr <- llvm_alloc (llvm_array 48 (llvm_int 8)); + // SK must be aligned + SK_ptr <- llvm_alloc_readonly_aligned 8 pow256_type; + SK <- llvm_fresh_var "SK" pow256_type; + llvm_points_to SK_ptr (llvm_term SK); + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + // TODO: This precond was the only way I could think of to be able to talk + // about the relationship between SK and the result of blst_hash_to_g1. Is + // there maybe a theorem that would work better? + llvm_precond {{ e1_order (affinify E (hash_to_curve_opt_impl (msg,DST))) > + scalar_value`{255,32} SK + shift }}; + // TODO: Do I need this precond VV ? + llvm_precond {{ SK != zero }}; + llvm_execute_func [ out_ptr + , SK_ptr + , msg_ptr + , llvm_term {{ `msg_len : [64] }} ]; + // TODO: Endianness? (Both for return, and for args to CoreSign) + llvm_points_to + out_ptr + (llvm_term {{ split`{each=8} (CoreSign ((drop_join_reverse`{255, 32} SK), msg)) }}); +}; + +// TODO: Under what conditions is this true? Should probably be done over IETF +// spec version rather than _impl version. Also, see note on +// hash_to_g2.saw:118 to see why this is with is_point_affine rather than +// is_point_projective (it might not be easy to transform goal to +// is_point_projective) +hash_to_g1_on_curve_thm <- admit_cryptol + {{ \x -> is_point_affine E (affinify E (hash_to_curve_opt_impl x)) == True }}; + +affine_inv_thm <- test_cryptol + {{ \P1 P2 -> + (and_core (same_point_affine E (affinify E (POINTonE1_abs P1)) P2) + (and_core (POINTonE1_invariant P1) + (and_core (not_core (is_bad_O_form_E P1)) + (is_point_projective E (POINTonE1_abs P1))))) == + (same_point_affine E (affinify E (POINTonE1_abs P1)) P2 /\ + ~(is_bad_O_form_E P1) /\ + is_point_affine E P2) }}; + +affine_inv_affine_rep_e1_thm <- custom_prove_cryptol + {{ \P -> POINTonE1_affine_invariant (POINTonE1_affine_rep P) == True }} + do { + unfolding [ "POINTonE1_affine_rep" , "POINTonE1_affine_invariant" ]; + rw_with fp_rep_thms; + print_goal; + w4_unint_z3 []; + }; + +// NOTE: Too slow to quickcheck +e1_scalar_mult_on_curve_thm <- admit_cryptol + {{ \sk P -> is_point_affine E (e1_scalar_mult sk P) == + if is_point_affine E P + then True + else apply is_point_affine E (e1_scalar_mult sk P) }}; + +e1_scalar_mult_not_bad_O_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \P sk (x:([32][8],[43][8])) -> + (same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) + (affinify E (hash_to_curve_opt_impl x)))) == + ((apply same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) + (affinify E (hash_to_curve_opt_impl x)))) && + ~(is_bad_O_form_E P)) }}); + +let remove_ho_rules = concat + [ point_add_fp2_thm, point_dadd_fp2_thm, point_double_fp2_thm, point_neg_fp2_thm + , point_add_affine_fp2_thm, point_dadd_affine_fp2_thm + , add_E'_thm, add'_E'_thm, neg_E'_thm + , affinify_E'_thm, projectify_E'_thm + , is_point_affine_E'_thm, is_point_projective_E'_thm + , is_point_O_E'_thm ] + [ point_add_fp_thm, point_dadd_fp_thm, point_double_fp_thm, point_neg_fp_thm + , point_add_affine_fp_thm, point_dadd_affine_fp_thm + , add_E_thm, add'_E_thm, affinify_E_thm, projectify_E_thm + , is_point_affine_E_thm, is_point_projective_E_thm, is_point_O_E_thm, point_O_E_thm + ]; + + +test_thm_correct' <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P sk (x:([32][8],[43][8])) -> + (same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) + (affinify E (hash_to_curve_opt_impl x)))) == + ((apply same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) + (affinify E (hash_to_curve_opt_impl x)))) && + POINTonE1_invariant P && + ~(is_bad_O_form_E P) && + is_point_projective E (POINTonE1_abs P)) }}) + do { + rw_with_1 e1_scalar_mult_not_bad_O_thm; + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with POINTonE1_base_thms; + simplify (addsimps [ affine_inv_thm + , e1_scalar_mult_on_curve_thm + , hash_to_g1_on_curve_thm + , affine_inv_affine_rep_e1_thm ] + empty_ss); + simplify basic_ss; + rw_with remove_ho_rules; + rw_with_1 same_point_affine_E_thm; + rw_with_1 and_true_thm; + print_goal; + w4_unint_z3 (concat [ "same_point_affine_E" + , "hash_to_curve_opt_impl" + , "scalar_value" + , "is_bad_O_form_E" ] + ec_mult_unints); + }; + +hash_to_curve_e1_opt_thm <- admit_cryptol + {{ \x -> HE1::hash_to_curve x == HE1::hash_to_curve_opt x }}; + +hash_to_curve_arg_expand_thm <- prove_cryptol + {{ \(x:([32][8],[43][8])) -> + hash_to_curve_opt_impl x == + apply hash_to_curve_opt_impl (([]:[0][8])#x.0, x.1) }} ["hash_to_curve_opt_impl"]; + +// TODO: why is this needed here (see prove_hash_to_g1_ov in hash_to_g1.saw)? +hash_to_curve_e1_impl_thm <- custom_prove_cryptol + {{ \(x:([32][8],[43][8])) -> HE1::hash_to_curve x == affinify E (hash_to_curve_opt_impl x) }} + do { + simplify (addsimp hash_to_curve_arg_expand_thm empty_ss); + unfolding ["apply"]; + simplify (addsimp hash_to_curve_E1_opt_impl_equiv_ov empty_ss); + simplify (addsimp hash_to_curve_e1_opt_thm empty_ss); + simplify basic_ss; + (print_goal); + w4_unint_z3 ["HashToCurveE1::hash_to_curve_opt"]; + }; + +mult_e1_scalar_mult_thm <- admit_cryptol + {{ \b P -> mult E b P == e1_scalar_mult (toInt b) P }}; + +let vecEq48 = parse_core "vecEq 48 (Vec 8 Bool) (bvEq 8)"; + +serialize_e1_eq_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> (vecEq48 (serialize_E1 P1) (serialize_E1 P2)) == + if same_point_affine E P1 P2 + then True + else apply vecEq48 (serialize_E1 P1) (serialize_E1 P2) }}) + ["serialize_E1"]; + +hoist_if_vecEq48_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b v1 v2 v3 -> (vecEq48 (if b then v1 else v2) v3) == + (if b then (vecEq48 v1 v3) else (vecEq48 v2 v3)) }}) []; + +point_e1_eq <- parse_core "pairEq Integer Integer intEq intEq"; + +eq_to_same_point_affine_E_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> (point_e1_eq P1 P2) == same_point_affine E P1 P2 }}) []; + +// The proof of eliminate_normalized_args_affinify_E_thm is a bit intricate: +div_0_fp_lemma_1 <- prove_cryptol {{ \x -> Fp.div(x, Fp.field_zero) == Fp.field_zero }} []; + +div_0_fp_lemma_2 <- custom_prove_cryptol + {{ \x y -> Fp.div(x,y) == if is_zero Fp y then apply Fp.div(x, Fp.field_zero) else apply Fp.div(x,y)}} + do { unfolding ["is_zero", "apply"]; rw_with_1 fp_is_equal_elim_thm; w4_unint_z3 ["Fp"]; }; + +div_0_fp_lemma <- custom_prove_cryptol + {{ \x y -> Fp.div(x,y) == if is_zero Fp y then Fp.field_zero else apply Fp.div(x,y)}} + do { rw_with_1 div_0_fp_lemma_2; + unfolding ["apply"]; + rw_with_1 div_0_fp_lemma_1; + w4_unint_z3 ["Fp"]; }; + +hoist_fp_mul_arg_thms <- for + [ {{ \ c x y z -> Fp.mul (if c then x else y, z) == if c then Fp.mul(x,z) else Fp.mul(y,z) }} + , {{ \ c x y z -> Fp.mul (x, if c then y else z) == if c then Fp.mul(x,y) else Fp.mul(x,z) }} + ] (\ t -> prove_cryptol (rewrite (cryptol_ss()) t) ["Fp"]); + +affinify_E_needs_no_special_case_thm <- custom_prove_cryptol + {{ \ p -> (affinify E p == (Fp.mul(lambda2, x), Fp.mul(lambda3, y)) + where + (x,y,z) = p + lambda = Fp.div (Fp.field_unit, z) + lambda2 = Fp.sq lambda + lambda3 = Fp.mul(lambda, lambda2)) }} + do { unfolding ["affinify", "E", "is_point_O", "same_point_affine", "point_O"]; + rw_with_1 div_0_fp_lemma; + unfolding ["apply"]; + simplify (addsimps hoist_fp_mul_arg_thms (addsimps fp_alg_thms fp_simpset)); + w4_unint_z3 fp_unints; }; + + +eliminate_normalized_args_affinify_E_thm <- custom_prove_cryptol + {{ \ p -> affinify E (normalize_point Fp p) == affinify E p }} + do { + rw_with_1 affinify_E_needs_no_special_case_thm; + unfolding ["E", "normalize_point"]; + simplify fp_simpset; + print_goal; + w4_unint_z3 fp_unints; + }; + +affinify_concrete_z_unit_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> affinify E (POINTonE1_abs P) == + if (POINTonE1_invariant P) /\ ((fp_abs P.2) == Fp.field_unit) + then affinify E (fp_abs P.0, fp_abs P.1, Fp.field_unit) + else apply affinify E (POINTonE1_abs P) }}) + do { + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps remove_ho_rules empty_ss); + print_goal; + w4_unint_z3 (concat ["fp_abs", "Fp"] ec_mult_unints); + }; + +Fp_div_unit_unit_thm <- prove_cryptol + {{ Fp.div (Fp.field_unit, Fp.field_unit) == Fp.field_unit }} []; + +Fp_normalize_abs_thm <- custom_prove_cryptol + {{ \x -> Fp.normalize (fp_abs x) == fp_abs x }} + do { + simplify (addsimps [fp_abs_normalize_thm, fp_abstract_invariant_thm] empty_ss); + (print_goal); + w4_unint_z3 []; + }; + +affinify_z_1_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> affinify E (POINTonE1_abs P) == + if (POINTonE1_invariant P) /\ ((fp_abs P.2) == Fp.field_unit) + then (fp_abs P.0, fp_abs P.1) + else apply affinify E (POINTonE1_abs P) }}) + do { + simplify (addsimp affinify_concrete_z_unit_thm empty_ss); + simplify (addsimps [affinify_E_needs_no_special_case_thm] empty_ss); + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimp Fp_div_unit_unit_thm empty_ss); + simplify (addsimps fp_laws empty_ss); + unfolding ["POINTonE1_invariant"]; + simplify (addsimp Fp_normalize_abs_thm empty_ss); + simplify (addsimps remove_ho_rules empty_ss); + (print_goal); + w4_unint_z3 (concat ["Fp", "fp_invariant", "fp_abs"] ec_mult_unints); + }; + +serialize_e1_affine_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> serialize_E1 (fp_abs P.0, fp_abs P.1) == + if (POINTonE1_invariant P) /\ (fp_abs (P.2) == Fp.field_unit) + then serialize_E1 (affinify E (POINTonE1_abs P)) + else apply serialize_E1 (fp_abs P.0, fp_abs P.1) }}) + do { + simplify (addsimps [affinify_z_1_thm] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps remove_ho_rules empty_ss); + print_goal; + w4_unint_z3 ["fp_abs", "serialize_E1", "affinify_E", "POINTonE1_abs"]; + }; + +O_O_unit_implies_bad_O_form_E <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> (is_bad_O_form_E P) == + if (is_point_O E (fp_abs P.0, fp_abs P.1)) /\ + (fp_abs (P.2) == Fp.field_unit) + then True + else apply is_bad_O_form_E P }}) []; + +// TODO: Solution is going to be some kind of "zero is not one" theorem, since +// we have to leave Fp uninterpreted (or that ~is_bad_O_form_E -> P.2 != 1) +demo_BasicSign_A_ov <- custom_verify "demo_BasicSign_A" + [ hash_to_g1_impl_ov + // [ hash_to_g1_ov + , POINTonE1_mult_w5_sk_ov + , blst_p1_compress_affine_ov + , blst_p1_compress_projective_ov ] + demo_BasicSign_A_spec + do { + simplify (addsimp eq_to_same_point_affine_E_thm (cryptol_ss())); + rw_with POINTonE1_base_thms; + simplify (addsimps POINTonE1_thms (cryptol_ss())); + simplify (addsimp eliminate_normalized_args_affinify_E_thm empty_ss); + simplify basic_ss; + simplify (addsimps [test_thm_correct'] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 O_O_unit_implies_bad_O_form_E; + unfolding ["apply", "BLSMinimalSignatureSize::DST", "is_bad_O_form_E"]; + simplify basic_ss; + simplify (cryptol_ss()); + // BEGIN final goal proof + unfolding [ "CoreSign" + , "module parameter point_to_signature" + , "module parameter main_curve" + , "main_curve" + , "module parameter hash_to_point" + , "hash_to_point" + , "point_to_signature" + , "BLSMinimalSignatureSize::DST" ]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps (concat split_join_thms + [ hash_to_curve_e1_impl_thm + , fold_scalar_value_thm + // [ fold_scalar_value_thm + , serialize_e1_eq_thm + , mult_e1_scalar_mult_thm ]) + empty_ss); + simplify basic_ss; + simplify (addsimps [hoist_unrip_48_thm] empty_ss); + simplify (addsimps [hoist_if_vecEq48_thm] empty_ss); + simplify (addsimps [serialize_e1_affine_thm] empty_ss); + simplify (addsimps [serialize_e1_eq_thm] empty_ss); + simplify (addsimps [hoist_if_vecEq48_thm] empty_ss); + simplify (addsimps [serialize_e1_eq_thm] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps remove_ho_rules empty_ss); + simplify (addsimps [same_point_affine_E_thm] empty_ss); + (print_goal); + w4_unint_z3 (concat [ "e1_order" + , "e1_scalar_mult" + , "fp_abs" + , "Fp" + , "is_point_projective_E" + , "hash_to_curve_opt_impl" + , "scalar_value" + , "same_point_affine_E" + , "hash_to_curve_opt_impl" ] + ec_mult_unints); + }; + +let compressed_E1_rep_type = llvm_array 48 (llvm_int 8); + +let demo_BasicVerify_A_spec = do { + global_alloc_init "demo_DST_A" {{ DST }}; + (sig, sig_ptr) <- ptr_to_fresh_readonly "sig" compressed_E1_rep_type; + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" compressed_E2_rep_type; + let message_len = 32; + (message, message_ptr) <- + ptr_to_fresh_readonly "message" (llvm_array message_len (llvm_int 8)); + crucible_precond {{ uncompress_E1_imp sig != nothing }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ ~((sig@0)@1) }}; + crucible_precond {{ uncompress_E2_imp pk != nothing }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ ~((pk@0)@1) }}; + llvm_precond {{ pubkey_to_point_is_affine pk }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ uncompress_E1_x_fp sig != Fp.field_zero }}; + // TODO: Explain (the library disagrees with spec on treating point_O as on + // the curve?) + let uncompressed_sig = {{ uncompress_E1_OK sig }}; + llvm_precond {{ ~(((uncompressed_sig.0) == Fp.field_zero) /\ + ((uncompressed_sig.1) == Fp.field_zero)) }}; + llvm_precond {{ signature_to_point_is_affine sig }}; + // preconditions + llvm_execute_func [ sig_ptr + , pk_ptr + , message_ptr + , llvm_term {{ `message_len : [64] }} ]; + // TODO: Postcond + llvm_return (llvm_term + {{ bool_to_limb (CoreVerify (join pk) message (join sig)) }}); +}; + +is_point_O_E_affine_rev_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \x y -> (((fp_abs x) == Fp.field_zero) /\ ((fp_abs y) == Fp.field_zero)) == + is_point_O E (POINTonE1_affine_abs (x, y)) }}) []; + +hoist_POINTonE1_affine_invariant <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> POINTonE1_affine_invariant (if c then p1 else p2) == + if c then POINTonE1_affine_invariant p1 else POINTonE1_affine_invariant p2 }}) + ["POINTonE1_affine_invariant"]; + +let BasicVerify_A_unints = (concat [ + "HE1::hash_to_curve" +, "KeyValidate" +, "POINTonE1_affine_abs" +, "POINTonE1_affine_invariant" +, "POINTonE1_affine_rep" +, "POINTonE2_affine_abs" +, "POINTonE2_affine_invariant" +, "POINTonE2_affine_rep" +//, "point_O_E" +//, "Fp" +//, "fp_abs" +, "bls_ate_pairing" +, "deserialize_E2" +, "fp_invariant" +, "fp_rep" +, "is_in_g1_impl" +, "is_in_g2_impl" +, "is_point_affine_E" +, "is_point_affine_E'" +, "is_square_fp" +, "nothing" +, "pubkey_subgroup_check" +, "pubkey_to_point_is_affine" +, "sign_F_p" +, "signature_subgroup_check" +, "signature_to_point_is_affine" +, "sqrt_fp" +, "uncompress_E1" +, "uncompress_E1_OK" +, "uncompress_E1_imp" +, "uncompress_E1_x" +, "uncompress_E1_x_fp" +, "uncompress_E1_y2" +, "uncompress_E2_OK" +, "uncompress_E2_imp" +] []); //(concat ec_mult_unints e2_unints)); + +zero_lt_one_thm <- prove_core abc + "EqTrue (boolEq (intLe (natToInt 0) (natToInt 1)) True)"; + +fold_POINTonE1_affine_invariant <- prove_cryptol + {{ \P -> (fp_invariant (P.0) /\ fp_invariant (P.1)) == + POINTonE1_affine_invariant P }} []; + +fold_POINTonE2_affine_invariant <- prove_cryptol + {{ \P -> (fp2_invariant (P.0) /\ fp2_invariant (P.1)) == + POINTonE2_affine_invariant P }} []; + +// TODO: Is this proved somewhere? +uncompress_E1_uncompress_E1_OK_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \x -> uncompress_E1 x == + if uncompress_E1_imp x != nothing + then (True, uncompress_E1_OK x) + else apply uncompress_E1 x }}); + +// We assume that signature_subgroup_check is equivalent to is_in_g1_impl for +// points on the curve. This assumption is proved in Bowe "Faster Subgroup +// Checks for BLS12-381". +is_in_g1_impl_thm <- admit_cryptol + (rewrite (cryptol_ss()) + {{ \P -> signature_subgroup_check P == + if is_point_affine_E P + then is_in_g1_impl P + else apply signature_subgroup_check P }}); + +fold_normalize_affine_fp_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> (Fp.normalize P.0, Fp.normalize P.1) == + normalize_affine_point Fp P }}) []; + +POINTonE1_affine_abs_rep_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> POINTonE1_affine_abs (POINTonE1_affine_rep P) == + normalize_affine_point Fp P }}) + do { + unfolding [ "POINTonE1_affine_abs" + , "POINTonE1_affine_rep" + , "normalize_affine_point"]; + rw_with fp_rep_thms; + print_goal; + w4_unint_z3 []; + }; + +hoist_normalize_affine_fp_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b P1 P2 -> normalize_affine_point Fp (if b then P1 else P2) == + if b + then normalize_affine_point Fp P1 + else normalize_affine_point Fp P2 }}) []; + +normalize_uncompress_E1_OK_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \x -> normalize_affine_point Fp (uncompress_E1_OK x) == + uncompress_E1_OK x }}) + do { + unfolding ["uncompress_E1_OK", "uncompress_E1_x_fp", "uncompress_E1_y"]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 hoist_normalize_affine_fp_thm; + unfolding ["normalize_affine_point"]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with fp_laws; + rw_with [normalize_sqrt_fp_thm]; + print_goal; + w4_unint_z3 fp_unints; + }; + +let fp_rep_at0 = parse_core "\\ (x:(Vec 2 (Vec 6 (Vec 64 Bool)))) -> at 2 (Vec 6 (Vec 64 Bool)) x 0"; + +squash_at_0_thm <- prove_cryptol + {{ \(x : Fp_rep_t) (y : Fp_rep_t) -> (fp_rep_at0 [x, y]) == x }} []; + +uncompress_E1_OK_on_curve <- admit_cryptol + {{ \x -> is_point_affine E (uncompress_E1_OK x) == + if uncompress_E1_imp x != nothing + then True + else apply is_point_affine E (uncompress_E1_OK x) }}; + +// TODO: Do not use +//denorm <- admit_cryptol {{ \x -> Fp.normalize x == x }}; + +is_point_O_E_affine_no_abs_rev_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \x y -> ((peq x Fp.field_zero) /\ (peq y Fp.field_zero)) == + is_point_O E (x, y) }}) []; + +fold_POINTonE2_affine_abs_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> ((fp2_abs P.0), (fp2_abs P.1)) == POINTonE2_affine_abs P }}) []; + +hoist_POINTonE2_affine_abs_thm <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> POINTonE2_affine_abs (if c then p1 else p2) == + if c then POINTonE2_affine_abs p1 else POINTonE2_affine_abs p2 }}) + ["POINTonE2_affine_abs"]; + +hoist_is_point_O_E'_thm <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> is_point_O E' (if c then p1 else p2) == + if c then is_point_O E' p1 else is_point_O E' p2 }}) []; + +// TODO: Prove +POINTonE2_affine_abs_rep_thm <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> POINTonE2_affine_abs (POINTonE2_affine_rep P) == + normalize_affine_point Fp_2 P }}) + do { + unfolding [ "POINTonE2_affine_abs" + , "POINTonE2_affine_rep" + , "normalize_affine_point" ]; + rw_with fp2_rep_thms; + w4_unint_z3 fp2_unints; + }; + +// TODO: Prove +// TODO: Try new is_point_O assumption based on CoreVerify precondition instead +is_point_O_KeyValidate_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \pk -> is_point_O E' (uncompress_E2_OK pk) == + if KeyValidate (join pk) + then False + else apply is_point_O E' (uncompress_E2_OK pk) }}); + +let {{ + core_verify_pk_in_g2 pk sig msg dst = Fp_12.is_equal(c1, c2) where + c1 = bls_ate_pairing (HE1::hash_to_curve (msg, dst)) pk + c2 = bls_ate_pairing sig BP' +}}; + +core_verify_pk_in_g2_impl_thm <- admit_cryptol {{ \pk sig msg dst -> core_verify_pk_in_g2_impl pk sig msg dst [] == core_verify_pk_in_g2 pk sig msg dst }}; + +blst_core_verify_pk_in_g2_ov <- verify_blst_core_verify_pk_in_g2_null_aug 32 43 0; + +// TODO: goal 6 fails +demo_BasicVerify_A_ov <- custom_verify "demo_BasicVerify_A" + [ POINTonE1_Uncompress_OK_ov // blst_p1_uncompress_OK_ov + , POINTonE1_affine_on_curve_ov + , vec_is_zero_2fp_ov + , blst_p1_affine_in_g1_ov + , blst_p2_uncompress_OK_ov + , POINTonE2_affine_on_curve_ov + , vec_is_zero_2fp2_ov + , blst_p2_affine_in_g2_ov + , demo_KeyValidate_A_ov + , blst_core_verify_pk_in_g2_ov ] + demo_BasicVerify_A_spec + do { + (goal_num_ite 7 + (do { + // Postcondition proof + unfolding [ "CoreVerify" + , "module parameter signature_to_point" + , "module parameter signature_subgroup_check" + , "signature_to_point_is_affine" + , "maybe_cases" + //, "POINTonE1_affine_rep" + , "signature_to_point" + //, "POINTonE1_affine_abs" + //, "POINTonE2_affine_abs" + , "module parameter pubkey_to_point" + , "pubkey_to_point" + , "blst_core_verify_pk_in_g2_error_precond"]; + rw_with_1 core_verify_pk_in_g2_impl_thm; + unfolding [ "core_verify_pk_in_g2" + , "module parameter pairing" + , "pairing" + , "module parameter hash_to_point" + , "hash_to_point" + , "module parameter P" + , "P" ]; + rw_with split_join_thms; + rw_with [ uncompress_E1_uncompress_E1_OK_thm + , POINTonE1_affine_abs_rep_thm + , is_in_g1_impl_thm]; + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify fp_simpset; + simplify (addsimps core_rewrites empty_ss); + //rw_with_1 squash_at_0_thm; + rw_with [ fold_normalize_affine_fp_thm + , intLe_sym_thm + , normalize_uncompress_E1_OK_thm ]; + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["POINTonE1_affine_rep"]; + rw_with fp_rep_thms; + rw_with [ normalize_uncompress_E1_OK_thm + , intLe_sym_thm + , zero_lt_one_thm + , is_point_O_E_affine_no_abs_rev_thm + , uncompress_E1_OK_on_curve ]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 is_point_O_E_affine_no_abs_rev_thm; + rw_with [ fold_normalize_affine_fp_thm + , deserialize_E2_uncompress_E2_OK_thm + , normalize_uncompress_E1_OK_thm ]; + // TODO: core_verify rewrite rule goes here + rw_with [ POINTonE2_affine_abs_rep_thm + , hoist_normalize_affine_fp2_thm + , normalize_uncompress_E2_OK_thm ]; + rw_with remove_ho_rules; + print_goal; + w4_unint_z3 BasicVerify_A_unints; + }) + (do { + // Precondition proof(s) + unfolding [ "POINTonE1_affine_abs" + , "uncompress_E1_imp" + , "POINTonE2_affine_abs" + /* + , "KeyValidate" + , "module parameter pubkey_to_point" + , "pubkey_to_point" + , "module parameter pubkey_subgroup_check" + , "module parameter other_curve" + , "other_curve" + , "maybe_cases" + */ + , "blst_core_verify_pk_in_g2_error_precond" + ]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify basic_ss; + rw_with [ hoist_POINTonE1_affine_rep + , hoist_POINTonE1_affine_invariant + , hoist_POINTonE2_affine_rep + , hoist_POINTonE2_affine_invariant + , affine_inv_affine_rep_e2_thm + , zero_lt_one_thm + , intLe_sym_thm + , affine_inv_affine_rep_e1_thm ]; + rw_with structural_rewrites; + simplify basic_ss; + rw_with [ fold_POINTonE1_affine_invariant + , fold_POINTonE2_affine_invariant + , hoist_POINTonE1_affine_invariant + , hoist_POINTonE2_affine_invariant + , affine_inv_affine_rep_e2_thm + , fold_POINTonE2_affine_abs_thm + , hoist_POINTonE2_affine_abs_thm + , hoist_is_point_O_E'_thm + , POINTonE2_affine_abs_rep_thm + , is_point_O_KeyValidate_thm + , normalize_uncompress_E2_OK_thm + , affine_inv_affine_rep_e1_thm ]; + //rw_with_1 is_point_O_affine_rev_thm; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with remove_ho_rules; + // END Precondition proofs + print_goal; + w4_unint_z3 BasicVerify_A_unints; + })); + }; diff --git a/proof/blst_error.saw b/proof/blst_error.saw index 7cf7ecb3..0d159bbe 100644 --- a/proof/blst_error.saw +++ b/proof/blst_error.saw @@ -3,4 +3,5 @@ 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_VERIFY_FAIL = 5; let BLST_PK_IS_INFINITY = 6; diff --git a/proof/clear_cofactor_p2.saw b/proof/clear_cofactor_p2.saw index 9c046fad..4a09ebb8 100644 --- a/proof/clear_cofactor_p2.saw +++ b/proof/clear_cofactor_p2.saw @@ -26,6 +26,7 @@ times_minus_z_rev_thm <- custom_prove_cryptol w4_unint_z3 ["affinify_E'", "E'", "POINTonE2_abs", "e2_scalar_mult"]; }; +// Prove times_minus_z is equivalent to e2_scalar_mult times_minus_z_thm <- custom_prove_cryptol {{ \P -> affinify E' (times_minus_z P) == e2_scalar_mult HE2Aux::pos_c1 (affinify E' P) }} do { @@ -84,16 +85,16 @@ e2_scalar_mult_inv_thm <- admit_cryptol // Prove clear_cofactor_bls12381_g2 (RFC spec) is equivalent to // clear_cofactor_E2_impl (spec based on C clear_cofactor_E2 function). + clear_cofactor_E2_equiv_thm <- custom_prove_cryptol {{ \P -> HE2Aux::clear_cofactor_bls12381_g2 (affinify E' P) == if AffinePoint_Fp_2_invariant (affinify E' P) then affinify E' (clear_cofactor_E2_impl P) else apply HE2Aux::clear_cofactor_bls12381_g2 (affinify E' P) }} - do { - unfolding ["clear_cofactor_bls12381_g2", "clear_cofactor_E2_impl"]; + do { + unfolding ["HE2Aux::clear_cofactor_bls12381_g2", "clear_cofactor_E2_impl"]; // Affinify goal - simplify (addsimps (concat [psi_psi_double_equiv_thm, times_minus_z_thm, psi_equiv_thm'] e2_curve_op_thms) (cryptol_ss())); - + simplify (addsimps (concat [psi_psi_double_equiv_thm, times_minus_z_thm, psi_equiv_thm'] e2_curve_op_thms) (cryptol_ss())); // Selectively remove polymorphic curve parameters from goal simplify (addsimps [affinify_E'_thm, e2_scalar_mult_thm] empty_ss); // Algebraic goal manipulation @@ -121,6 +122,7 @@ let POINTonE2_add_n_dbl_spec n = do { llvm_points_to out_ptr (llvm_term out'); }; + POINTonE2_add_n_dbl_ovs <- for [2, 3, 9, 32, 16] (\x -> custom_verify "POINTonE2_add_n_dbl" [POINTonE2_double_alias_1_2_ov, POINTonE2_dadd_null_alias_1_2_ov] @@ -138,7 +140,6 @@ normalize_add_n_dbl_thms <- for [2,3,9,32,16] do { goal_eval_unint fp_unints; simplify fp_simpset; w4_unint_z3 fp_unints; }); - // Prove POINTonE2_times_minus_z matches the times_minus_z spec let POINTonE2_times_minus_z_spec = do { @@ -150,6 +151,7 @@ let POINTonE2_times_minus_z_spec = do { llvm_postcond {{ POINTonE2_invariant out }}; llvm_points_to out_ptr (llvm_term out); }; + POINTonE2_times_minus_z_ov <- custom_verify "POINTonE2_times_minus_z" (concat [POINTonE2_double_ov] POINTonE2_add_n_dbl_ovs) POINTonE2_times_minus_z_spec @@ -182,6 +184,7 @@ let POINTonE2_cneg_nonzero_spec = do { llvm_execute_func [p_ptr, llvm_term cbit]; llvm_points_to p_ptr (llvm_term {{ POINTonE2_rep (point_neg Fp_2 (POINTonE2_abs p)) }} ); }; + POINTonE2_cneg_nonzero_ov <- custom_verify "POINTonE2_cneg" (concat vec_fp2_overrides fp2_overrides) POINTonE2_cneg_nonzero_spec @@ -204,8 +207,8 @@ clear_cofactor_ov <- custom_verify "clear_cofactor" POINTonE2_dadd_null_alias_1_2_ov] clear_cofactor_impl_spec do { - rw_with POINTonE2_thms; - unfolding ["clear_cofactor_E2_impl", + rw_with POINTonE2_thms; + unfolding ["clear_cofactor_E2_impl", "POINTonE2_abs", "POINTonE2_rep", "POINTonE2_invariant"]; diff --git a/proof/compress-p1.saw b/proof/compress-p1.saw index 88eb3847..69aa9f7c 100644 --- a/proof/compress-p1.saw +++ b/proof/compress-p1.saw @@ -61,6 +61,24 @@ let POINTonE1_from_Jacobian_spec = do { crucible_points_to_untyped out_ptr (crucible_term out); }; +let POINTonE1_from_Jacobian_alias_spec = do { + (inp, inp_ptr) <- ptr_to_fresh "in" POINTonE1_type; + + crucible_precond {{ POINTonE1_invariant inp }}; + crucible_precond {{ is_point_projective E (POINTonE1_abs inp) }}; // on the curve + crucible_precond {{ ~(Fp.is_equal ((fp_abs (inp.2)), Fp.field_zero)) }}; + + crucible_execute_func [inp_ptr, inp_ptr]; + + let out = {{ POINTonE1_affine_rep (affinify E (POINTonE1_abs inp)) }}; + crucible_postcond {{ POINTonE1_affine_invariant out }}; + + // Use points_to_untyped because out_ptr is a POINTonE1 that the caller + // immediately casts to a POINTonE1_affine. Therefore, we can treat out_ptr + // as a POINTonE1_affine and ignore Z. + crucible_points_to_untyped inp_ptr (crucible_term out); +}; + // commute mul once -- use with caution! mul_commutes_fp_thm <- prove_cryptol {{ \x y -> Fp.mul (x, y) == apply Fp.mul (y,x) }} []; reciprocal_div_fp_thm <- admit_cryptol {{ \x -> inverse_fp x == Fp.div (Fp.field_unit, x) }}; @@ -75,6 +93,16 @@ POINTonE1_from_Jacobian_ov <- custom_verify "POINTonE1_from_Jacobian" w4_unint_z3 fp_unints; }; +POINTonE1_from_Jacobian_alias_ov <- custom_verify "POINTonE1_from_Jacobian" + (concat [reciprocal_fp_ov] (concat vec_select_asm_ovs fp_overrides)) + POINTonE1_from_Jacobian_alias_spec + do { + (simplify (addsimps [mul_commutes_fp_thm, reciprocal_div_fp_thm] empty_ss)); + unfolding ["POINTonE1_affine_invariant", "POINTonE1_affine_rep", "apply"]; + apply_fp_rewrites; + w4_unint_z3 fp_unints; + }; + // POINTonE1_Compress_BE compresses X and returns the sign of Y. It supports // both affine points (indicated by Z == 1) and projective points (Z != 1). let POINTonE1_Compress_BE_spec is_point_affine = do { diff --git a/proof/compress-p2.saw b/proof/compress-p2.saw index 5918c44e..2b60fc19 100644 --- a/proof/compress-p2.saw +++ b/proof/compress-p2.saw @@ -43,6 +43,24 @@ let POINTonE2_from_Jacobian_spec = do { crucible_points_to_untyped out_ptr (crucible_term out); }; +let POINTonE2_from_Jacobian_alias_spec = do { + (out, out_ptr) <- ptr_to_fresh "out" POINTonE2_type; + + crucible_precond {{ POINTonE2_invariant out }}; + crucible_precond {{ is_point_projective E' (POINTonE2_abs out) }}; // on the curve + crucible_precond {{ ~(Fp_2.is_equal ((fp2_abs (out.2)), Fp_2.field_zero)) }}; + + crucible_execute_func [out_ptr, out_ptr]; + + let new_out = {{ POINTonE2_affine_rep (affinify E' (POINTonE2_abs out)) }}; + crucible_postcond {{ POINTonE2_affine_invariant new_out }}; + + // Use points_to_untyped because out_ptr is a POINTonE2 that the caller + // immediately casts to a POINTonE2_affine. Therefore, we can treat out_ptr + // as a POINTonE2_affine and ignore Z. + crucible_points_to_untyped out_ptr (crucible_term new_out); +}; + // commute mul once -- use with caution! mul_commutes_fp2_thm <- prove_cryptol {{ \x y -> Fp_2.mul (x, y) == apply Fp_2.mul (y,x) }} []; reciprocal_div_fp2_thm <- admit_cryptol {{ \x -> inverse_fp2 x == Fp_2.div (Fp_2.field_unit, x) }}; @@ -57,6 +75,16 @@ POINTonE2_from_Jacobian_ov <- custom_verify "POINTonE2_from_Jacobian" w4_unint_z3 fp2_unints; }; +POINTonE2_from_Jacobian_alias_ov <- custom_verify "POINTonE2_from_Jacobian" + (concat [reciprocal_fp2_ov] (concat vec_select_asm_ovs fp2_overrides)) + POINTonE2_from_Jacobian_alias_spec + do { + rw_with [mul_commutes_fp2_thm, reciprocal_div_fp2_thm]; + unfolding ["POINTonE2_affine_invariant", "POINTonE2_affine_rep", "apply"]; + simplify (addsimp fp2_unrip_thm fp2_simpset); + w4_unint_z3 fp2_unints; + }; + // POINTonE2_Compress_BE compresses X and returns the sign of Y. It supports // both affine points (indicated by Z == 1) and projective points (Z != 1). let POINTonE2_Compress_BE_spec is_point_affine = do { @@ -119,19 +147,21 @@ POINTonE2_Compress_BE_projective_ov <- custom_verify "POINTonE2_Compress_BE" unfolding [ "POINTonE2_affine_abs" , "POINTonE2_affine_rep" , "POINTonE2_invariant" ]; - (apply_fp_rewrites); + apply_fp_rewrites; simplify (addsimps [ one_mont_px_abs_thm , one_mont_px_invariant_thm , seq_ite_2_thm , unrip_thm_2 ] (addsimps POINTonE2_thms fp2_simpset)); + simplify remove_higher_order_function_simpset; w4_unint_z3 [ "POINTonE2_abs" , "POINTonE2_invariant" - , "Fp_2" , "fp2_abs" , "I2OSP48" , "fp2_invariant" - , "POINTonE2_affine_invariant"]; + , "POINTonE2_affine_invariant" + , "affinify_E'" + , "is_point_projective_E'"]; }; // Prove POINTonE2_Compress_BE matches the spec for affine points @@ -146,7 +176,6 @@ POINTonE2_Compress_BE_affine_ov <- custom_verify "POINTonE2_Compress_BE" simplify (addsimp one_mont_px_abs_thm fp2_simpset); w4_unint_z3 [ "POINTonE2_abs" , "POINTonE2_invariant" - , "Fp_2" , "fp2_abs" , "I2OSP48"]; }; diff --git a/proof/core_verify_pk_in_g1.saw b/proof/core_verify_pk_in_g1.saw new file mode 100644 index 00000000..6ab05452 --- /dev/null +++ b/proof/core_verify_pk_in_g1.saw @@ -0,0 +1,288 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +// Specifications + +// We assume that we use the uniform encoding to the curve, i.e. +// `hash_or_encode` is true. Moreover, we assume that the input points satisfy +// the invariants POINTonE1_affine_invariant (pk) and +// POINTonE2_affine_invariant (sig) and that the signature is a point on the +// curve; ensuring those is the responsibility of the caller. Note that, +// assuming the signature has been deserialized using `blst_p1_uncompress`, +// then there's no need to check whether it's on the curve because that is a +// guarantee of a successful call to `blst_p1_uncompress`. Also note that the +// public key must be a point on the curve and in the right subgroup (this is +// not checked at all by the C code; presumably, public keys should be validated +// separately before use). + +// NOTE: calling the function with a null pk is not safe + +let {{ + blst_core_verify_pk_in_g1_error_precond : POINTonE1_affine_t -> POINTonE2_affine_t -> Bool + blst_core_verify_pk_in_g1_error_precond pk sig = + is_point_O E (POINTonE1_affine_abs pk) \/ ( ~(is_point_O E' (POINTonE2_affine_abs sig)) /\ ~is_in_g2_impl (POINTonE2_affine_abs sig) ) +}}; + +// case in which no argument is null and the error condition is false +let blst_core_verify_pk_in_g1_non_null_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE1_affine"); + (sig, signature_ptr) <- ptr_to_fresh_readonly "signature" (llvm_struct "struct.POINTonE2_affine"); + llvm_precond {{ POINTonE1_affine_invariant pk /\ POINTonE2_affine_invariant sig /\ is_point_affine E' (POINTonE2_affine_abs sig) /\ ~blst_core_verify_pk_in_g1_error_precond pk sig}}; + hash_or_encode <- llvm_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + llvm_execute_func [pk_ptr, signature_ptr, llvm_term hash_or_encode, msg_ptr, llvm_term {{ `msg_len : [64] }}, dst_ptr, llvm_term {{ `dst_len : [64] }}, aug_ptr, llvm_term {{ `aug_len : [64] }}]; + llvm_return (llvm_term {{ if core_verify_pk_in_g1_impl (POINTonE1_affine_abs pk) (POINTonE2_affine_abs sig) msg dst aug then (`BLST_SUCCESS:[32]) else `BLST_VERIFY_FAIL }}); +}; + +// error case +let blst_core_verify_pk_in_g1_error_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE1_affine"); + (sig, signature_ptr) <- ptr_to_fresh_readonly "signature" (llvm_struct "struct.POINTonE2_affine"); + llvm_precond {{ POINTonE1_affine_invariant pk /\ POINTonE2_affine_invariant sig /\ is_point_affine E' (POINTonE2_affine_abs sig) /\ blst_core_verify_pk_in_g1_error_precond pk sig }}; + hash_or_encode <- llvm_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + llvm_execute_func [pk_ptr, signature_ptr, llvm_term hash_or_encode, msg_ptr, llvm_term {{ `msg_len : [64] }}, dst_ptr, llvm_term {{ `dst_len : [64] }}, aug_ptr, llvm_term {{ `aug_len : [64] }}]; + ret <- llvm_fresh_var "blst_core_verify_pk_in_g1_ret" (llvm_int 32); + llvm_return (llvm_term ret); + llvm_postcond {{ ret != `BLST_SUCCESS }}; +}; + +// sig is null +let blst_core_verify_pk_in_g1_null_sig_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE1_affine"); + let signature_ptr = llvm_null; + llvm_precond {{ POINTonE1_affine_invariant pk }}; + hash_or_encode <- llvm_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + llvm_execute_func [pk_ptr, signature_ptr, llvm_term hash_or_encode, msg_ptr, llvm_term {{ `msg_len : [64] }}, dst_ptr, llvm_term {{ `dst_len : [64] }}, aug_ptr, llvm_term {{ `aug_len : [64] }}]; + llvm_return (llvm_term {{ if is_point_O E (POINTonE1_affine_abs pk) then `BLST_PK_IS_INFINITY else if core_verify_pk_in_g1_impl (POINTonE1_affine_abs pk) (point_O E') msg dst aug then (`BLST_SUCCESS:[32]) else `BLST_VERIFY_FAIL }}); +}; + +let overrides = concat mul_fp12_ovs // fp12.saw +[ POINTonE2_from_Jacobian_alias_ov // compress-p2.saw +, POINTonE1_from_Jacobian_ov // compress-p2.saw +, POINTonE2_from_Jacobian_ov // compress-p2.saw +, miller_loop_n_1_ov // pairing.saw +, conjugate_fp12_ov // fp12.saw +, final_exp_alias_ov +, vec_copy_2fp_ov +, vec_copy_POINTonE1_affine_ov +, vec_copy_POINTonE2_affine_ov +, vec_copy_fp12_ov +, vec_select_2Fp_ov +, vec_is_zero_10fp_ov +, vec_is_zero_2fp2_ov +, vec_is_zero_2fp_is_equal_ov +, vec_is_equal_fp2_ov // TODO: needed? +, POINTonE2_in_g2_ov // subgroup_check_g2.saw +]; + +// Assumptions + +let normalize_hash_to_curve_impl msg_len dst_len aug_len = do { + l1 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> normalize_point Fp_2 (hash_to_curve_E2_opt_impl (aug#msg, DST)) == hash_to_curve_E2_opt_impl (aug#msg, DST) }}; + l2 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> Fp_2.normalize (hash_to_curve_E2_opt_impl (aug#msg, DST)).2 == (hash_to_curve_E2_opt_impl (aug#msg, DST)).2 }}; + return [l1,l2]; +}; + +normalize_final_exp_thms <- for [ + {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(0:[2])@(0:[2])) == (final_exponentiation_impl x)@(0:[2])@(0:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(0:[2])@(1:[2])) == (final_exponentiation_impl x)@(0:[2])@(0:[2])@(1:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(1:[2])@(0:[2])) == (final_exponentiation_impl x)@(0:[2])@(1:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(1:[2])@(1:[2])) == (final_exponentiation_impl x)@(0:[2])@(1:[2])@(1:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(2:[2])@(0:[2])) == (final_exponentiation_impl x)@(0:[2])@(2:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(0:[2])@(2:[2])@(1:[2])) == (final_exponentiation_impl x)@(0:[2])@(2:[2])@(1:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(0:[2])@(0:[2])) == (final_exponentiation_impl x)@(1:[2])@(0:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(0:[2])@(1:[2])) == (final_exponentiation_impl x)@(1:[2])@(0:[2])@(1:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(1:[2])@(0:[2])) == (final_exponentiation_impl x)@(1:[2])@(1:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(1:[2])@(1:[2])) == (final_exponentiation_impl x)@(1:[2])@(1:[2])@(1:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(2:[2])@(0:[2])) == (final_exponentiation_impl x)@(1:[2])@(2:[2])@(0:[2]) }} + , {{ \x -> Fp.normalize ((final_exponentiation_impl x)@(1:[2])@(2:[2])@(1:[2])) == (final_exponentiation_impl x)@(1:[2])@(2:[2])@(1:[2]) }} +] (\e -> admit_cryptol (rewrite (cryptol_ss ()) e)); + +miller_loop_zero_thm <- admit_cryptol {{ \x -> fp12_conjugate (miller_loop_opt_checked BP x) == if (is_point_O E' x) then Fp_12.field_unit else apply miller_loop_opt_checked BP x }}; + +// TODO: not sure this is true if pk or sig are invalid. +// core_verify_pk_in_g1_impl_thm <- admit_cryptol {{ \pk sig msg dst aug -> core_verify_pk_in_g1_impl pk sig msg dst aug == core_verify_pk_in_g1 pk sig msg dst aug }}; + +// Proofs + +let remove_ho_rules = concat + [ point_add_fp2_thm, point_dadd_fp2_thm, point_double_fp2_thm, point_neg_fp2_thm + , point_add_affine_fp2_thm, point_dadd_affine_fp2_thm + , add_E'_thm, add'_E'_thm, neg_E'_thm + , affinify_E'_thm, projectify_E'_thm + , is_point_affine_E'_thm, is_point_projective_E'_thm + , is_point_O_E'_thm ] + [ point_add_fp_thm, point_dadd_fp_thm, point_double_fp_thm, point_neg_fp_thm + , point_add_affine_fp_thm, point_dadd_affine_fp_thm + , add_E_thm, add'_E_thm, affinify_E_thm, projectify_E_thm + , is_point_affine_E_thm, is_point_projective_E_thm, is_point_O_E_thm, point_O_E_thm + ]; + +restitching_rules <- for [ + {{ \(x:[6][64]) -> ([x1,x2,x3,x4,x5,x6] == x where [x1,x2,x3,x4,x5,x6] = x) }} +, {{ \(x:[2][6][64]) -> ([x1,x2] == x where [x1,x2] = x) }} +, {{ \(a:[2]Integer) -> ([x,y] == a where [x,y] = a) }} +, {{ \(a:[2][6][64]) -> ([x,y] == a where [x,y] = a) }} +, {{ + \(x:t_Fp_2) -> ( + [[a1, a2, a3, a4, a5, a6], [b1, b2, b3, b4, b5, b6]] == fp2_rep x where + [a,b] = fp2_rep x + [a1, a2, a3, a4, a5, a6] = a + [b1, b2, b3, b4, b5, b6] = b + ) + }} +] (\ eq -> custom_prove_cryptol (rewrite (cryptol_ss ()) eq) w4); + +fp2_unit_rep <- eval_term {{ fp2_rep Fp_2.field_unit }}; + +// creating the following rewrite rules takes a little work +let select_term = rewrite (add_cryptol_defs ["ecEq"] (cryptol_ss ())) {{ \(x:POINTonE2_affine_t) -> select x.0 fp2_unit_rep (~((if ((Fp_2.is_equal (fp2_abs x.0, Fp_2.field_zero)) /\ (Fp_2.is_equal (fp2_abs x.1, Fp_2.field_zero))) then (1:[64]) else zero) == zero)) }}; + +affinify_projectify_is_id <- admit_cryptol (rewrite (cryptol_ss ()) {{ \x -> affinify E' (POINTonE2_abs (x.0,x.1,select_term x)) == if POINTonE2_affine_invariant x then (POINTonE2_affine_abs x) else apply affinify E' (POINTonE2_abs (x.0,x.1,select_term x)) }}); + +core_verify_pk_in_g1_POINTonE2_from_Jacobian_sig_preconds <- do { + on_curve <- admit_cryptol (rewrite (cryptol_ss ()) {{ \sig -> is_point_projective E' (POINTonE2_abs (sig.0,sig.1,select_term sig)) == if (is_point_affine E' (POINTonE2_affine_abs sig)) then True else apply is_point_projective E' (POINTonE2_abs (sig.0,sig.1,select_term sig)) }}); + not_zero <- admit_cryptol (rewrite (cryptol_ss ()) {{ \sig-> Fp_2.is_equal (fp2_abs (select_term sig), Fp_2.field_zero) == (is_point_O E' (POINTonE2_affine_abs sig)) }}); + return [on_curve,not_zero]; +}; + +let core_verify_pk_in_g1_POINTonE2_from_Jacobian_hash_preconds msg_len dst_len aug_len = do { + on_curve <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> is_point_projective E' (hash_to_curve_E2_opt_impl (aug#msg, DST)) == True }}); + not_zero <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> Fp_2.is_equal ((hash_to_curve_E2_opt_impl (aug#msg, DST)).2, Fp_2.field_zero) == False }}); // NOTE: this is unsound, but it's morally okay as it's deemed it will never happen + return [on_curve,not_zero]; +}; + +let core_verify_pk_in_g1_unints = ["BP","is_in_g2_impl","hash_to_curve_E2_opt_impl","miller_loop_opt_checked","final_exponentiation_impl","fp12_conjugate","affinify_E","affinify_E'", "projectify_E'", "projectify_E","is_point_projective_E","is_point_projective_E'","is_point_affine_E","is_point_affine_E'","Fp_12"]; // the stuff we want to leave unfolded + +let rewrite_fp2_unit = run (custom_prove_cryptol (rewrite (cryptol_ss ()) {{ fp2_abs fp2_unit_rep == Fp_2.field_unit }}) w4); +let BP_rep = run ( eval_term {{ POINTonE1_affine_rep BP }}); +let BP_rewrite = run (custom_prove_cryptol (rewrite (cryptol_ss ()) {{ POINTonE1_affine_abs BP_rep == BP }}) w4); + +// below we rewrite Fp_12.is_equal in terms of lower-level operations; we do that because we don't want to unfold the whole Fp_12 record. +let rewrite_is_equal = run (custom_prove_cryptol {{ + \x -> Fp_12.is_equal (x,Fp_12.field_unit) == + (Fp_2.is_equal(x12, Fp_2.field_unit) /\ all (\a -> Fp.is_equal (a, Fp.field_zero)) y + where [x0,x1] = x; [x00,x01,x02] = x0; [x10,x11,x12] = x1; y = take`{front=10} (join (join x))) + }} w4); + +let fp12_unit_rep = run( eval_term {{ fp12_rep Fp_12.field_unit }}); +let rewrite_fp12_unit = run (custom_prove_cryptol (rewrite (cryptol_ss ()) {{ fp12_abs fp12_unit_rep == Fp_12.field_unit }}) w4); + +// Case in which no argument is null and we reach the final check + +// Technicalities: +// * Need to establish the preconditions of POINTonE2_from_Jacobian +// * Need some normalization assumptions +// * The C code transforms the signature to Jacobian coordinates (using macro FROM_AFFINE) and back to affine coordinates (using POINTonE2_from_Jacobian); we need to prove that this is the identity transformation. This is made harder than it seems by `ite` terms appearing in the middle of things, and the fact that hoist_ifs does not eliminate them all (TODO: create an issues for this) +// * The implementation of the final test for equality needs to be shown equivalent to equality in Fp_12; since we leave Fp_12 uninterpreted to avoid unfolding `Fp_12.mul`, we rewrite the Fp_12.is_equal in terms of `is_equal` in lower fields + +let side_conditions_script msg_len dst_len aug_len = do { + rw_with (concat POINTonE1_thms POINTonE2_thms); + unfolding ["POINTonE2_rep"]; + simplify fp12_simpset; + simplify fp2_simpset; + simplify fp_simpset; + // get rid of normalize terms produced by the rewrites: + let normalize_hash_to_curve_impl_thms = run (normalize_hash_to_curve_impl msg_len dst_len aug_len); + rw_with (concat normalize_hash_to_curve_impl_thms [normalize_miller_loop_opt_checked_thm]); + // take care of the round-trip that sig takes from affine represetation to jacobian and back to affine: + rw_with [affinify_projectify_is_id]; + // establish the preconditions of POINTonE2_from_Jacobian: + let core_verify_pk_in_g1_POINTonE2_from_Jacobian_hash_preconds_thms = run (core_verify_pk_in_g1_POINTonE2_from_Jacobian_hash_preconds msg_len dst_len aug_len); + rw_with (concat core_verify_pk_in_g1_POINTonE2_from_Jacobian_hash_preconds_thms core_verify_pk_in_g1_POINTonE2_from_Jacobian_sig_preconds); + unfolding ["apply"]; + rw_with remove_ho_rules; + goal_eval_unint (concat core_verify_pk_in_g1_unints ["fp_rep","fp_abs","fp_invariant"]); + simplify fp_simpset; + w4_unint_z3 (concat core_verify_pk_in_g1_unints ["fp_rep","fp_abs"]); +}; + +let post_condition_script msg_len dst_len aug_len = do { + // get rid of `abs rep` terms + rw_with (concat POINTonE1_thms POINTonE2_thms); + unfolding ["POINTonE2_rep"]; + simplify fp12_simpset; + simplify fp2_simpset; + simplify fp_simpset; + // get rid of normalize terms produced by the rewrites: + let normalize_hash_to_curve_impl_thms = run (normalize_hash_to_curve_impl msg_len dst_len aug_len); + rw_with (concat normalize_hash_to_curve_impl_thms [normalize_miller_loop_opt_checked_thm]); + // take care of the round-trip that sig takes from affine representation to Jacobian and back to affine: + rw_with [affinify_projectify_is_id]; + // rewrite abstracted constants (we're leaving fp_rep and fp_abs uninterpreted, so we need to rewrite the concrete constants): + simplify (addsimps [BP_rewrite,rewrite_fp12_unit,rewrite_fp2_unit] empty_ss); + // we rewrite the spec term: + unfolding ["core_verify_pk_in_g1_impl"]; + rw_with [miller_loop_zero_thm]; + unfolding ["apply"]; + rw_with [rewrite_is_equal]; + rw_with remove_ho_rules; + goal_eval_unint (concat core_verify_pk_in_g1_unints ["fp_rep","fp_abs","POINTonE2_invariant","POINTonE2_affine_invariant","POINTonE1_affine_invariant","fp2_invariant","fp_invariant"]); + rw_with restitching_rules; + simplify fp_simpset; // get rid of remaining `abs rep` terms + rw_with normalize_final_exp_thms; // get rid of `normalize` terms introduced by fp_simpset + w4_unint_z3 (concat core_verify_pk_in_g1_unints ["fp_rep","fp_abs","POINTonE2_invariant","POINTonE2_affine_invariant","POINTonE1_affine_invariant","fp2_invariant","fp_invariant"]); +}; + +let verify_blst_core_verify_pk_in_g1_non_null msg_len dst_len aug_len = do { + let Hash_to_G2_ov = run (prove_Hash_to_G2_impl msg_len dst_len aug_len); + custom_verify_path_sat + "blst_core_verify_pk_in_g1" + (concat overrides [Hash_to_G2_ov]) + (blst_core_verify_pk_in_g1_non_null_spec msg_len dst_len aug_len) + (goal_num_ite 17 + (post_condition_script msg_len dst_len aug_len) + (side_conditions_script msg_len dst_len aug_len)); +}; + +let verify_blst_core_verify_pk_in_g1_error msg_len dst_len aug_len = do { + let Hash_to_G2_ov = run (prove_Hash_to_G2_impl msg_len dst_len aug_len); + custom_verify_path_sat + "blst_core_verify_pk_in_g1" + (concat overrides [Hash_to_G2_ov]) + (blst_core_verify_pk_in_g1_error_spec msg_len dst_len aug_len) + do { + unfolding ["blst_core_verify_pk_in_g1_error_precond"]; + // hoist_ifs_in_goal; + simplify (addsimps (concat POINTonE1_thms POINTonE2_thms) empty_ss); + unfolding ["POINTonE2_rep"]; + simplify fp12_simpset; + simplify fp2_simpset; + simplify fp_simpset; + simplify (addsimps remove_ho_rules empty_ss); + (w4_unint_z3 (concat ["fp_rep","fp_abs","fp12_rep","POINTonE2_invariant","POINTonE1_invariant","fp_invariant","fp2_invariant"] core_verify_pk_in_g1_unints)); + }; +}; + +let verify_blst_core_verify_pk_in_g1_null_sig msg_len dst_len aug_len = do { + // a null sig is treated as a zero sig + let Hash_to_G2_ov = run (prove_Hash_to_G2_impl msg_len dst_len aug_len); + custom_verify + "blst_core_verify_pk_in_g1" + (concat overrides [Hash_to_G2_ov]) + (blst_core_verify_pk_in_g1_null_sig_spec msg_len dst_len aug_len) + (goal_num_ite 11 + (post_condition_script msg_len dst_len aug_len) + (side_conditions_script msg_len dst_len aug_len)); +}; + +let msg_len = 32; +let dst_len = 8; +let aug_len = 8; + +verify_blst_core_verify_pk_in_g1_non_null msg_len dst_len aug_len; +verify_blst_core_verify_pk_in_g1_error msg_len dst_len aug_len; +verify_blst_core_verify_pk_in_g1_null_sig msg_len dst_len aug_len; diff --git a/proof/core_verify_pk_in_g2.saw b/proof/core_verify_pk_in_g2.saw new file mode 100644 index 00000000..8503b00a --- /dev/null +++ b/proof/core_verify_pk_in_g2.saw @@ -0,0 +1,217 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + + +// Specifications + +let {{ + blst_core_verify_pk_in_g2_error_precond : POINTonE2_affine_t -> POINTonE1_affine_t -> Bool + blst_core_verify_pk_in_g2_error_precond pk sig = + is_point_O E' (POINTonE2_affine_abs pk) \/ ( ~(is_point_O E (POINTonE1_affine_abs sig)) /\ ~is_in_g1_impl (POINTonE1_affine_abs sig) ) +}}; + +// case in which no argument is null and the error condition is false +let blst_core_verify_pk_in_g2_non_null_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE2_affine"); + (sig, signature_ptr) <- ptr_to_fresh_readonly "signature" (llvm_struct "struct.POINTonE1_affine"); + llvm_precond {{ POINTonE2_affine_invariant pk /\ POINTonE1_affine_invariant sig /\ is_point_affine E (POINTonE1_affine_abs sig) /\ ~blst_core_verify_pk_in_g2_error_precond pk sig }}; + hash_or_encode <- crucible_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + crucible_execute_func [pk_ptr, signature_ptr, crucible_term hash_or_encode, msg_ptr, crucible_term {{ `msg_len : [64] }}, dst_ptr, crucible_term {{ `dst_len : [64] }}, aug_ptr, crucible_term {{ `aug_len : [64] }}]; + crucible_return (crucible_term {{ if core_verify_pk_in_g2_impl (POINTonE2_affine_abs pk) (POINTonE1_affine_abs sig) msg dst aug then (`BLST_SUCCESS:[32]) else `BLST_VERIFY_FAIL }}); +}; + +// same but with NULL aug +let blst_core_verify_pk_in_g2_null_aug_spec msg_len dst_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE2_affine"); + (sig, signature_ptr) <- ptr_to_fresh_readonly "signature" (llvm_struct "struct.POINTonE1_affine"); + llvm_precond {{ POINTonE2_affine_invariant pk /\ POINTonE1_affine_invariant sig /\ is_point_affine E (POINTonE1_affine_abs sig) /\ ~blst_core_verify_pk_in_g2_error_precond pk sig }}; + hash_or_encode <- crucible_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + let aug_ptr = llvm_null; + crucible_execute_func [pk_ptr, signature_ptr, crucible_term hash_or_encode, msg_ptr, crucible_term {{ `msg_len : [64] }}, dst_ptr, crucible_term {{ `dst_len : [64] }}, aug_ptr, crucible_term {{ zero : [64] }}]; + crucible_return (crucible_term {{ if core_verify_pk_in_g2_impl (POINTonE2_affine_abs pk) (POINTonE1_affine_abs sig) msg dst [] then (`BLST_SUCCESS:[32]) else `BLST_VERIFY_FAIL }}); +}; + +// error case +let blst_core_verify_pk_in_g2_error_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE2_affine"); + (sig, signature_ptr) <- ptr_to_fresh_readonly "signature" (llvm_struct "struct.POINTonE1_affine"); + llvm_precond {{ POINTonE2_affine_invariant pk /\ POINTonE1_affine_invariant sig /\ is_point_affine E (POINTonE1_affine_abs sig) /\ blst_core_verify_pk_in_g2_error_precond pk sig }}; + hash_or_encode <- crucible_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + crucible_execute_func [pk_ptr, signature_ptr, crucible_term hash_or_encode, msg_ptr, crucible_term {{ `msg_len : [64] }}, dst_ptr, crucible_term {{ `dst_len : [64] }}, aug_ptr, crucible_term {{ `aug_len : [64] }}]; + ret <- llvm_fresh_var "blst_core_verify_pk_in_g2_ret" (llvm_int 32); + llvm_return (llvm_term ret); + llvm_postcond {{ ret != `BLST_SUCCESS }}; +}; + +// sig is null +let blst_core_verify_pk_in_g2_null_sig_spec msg_len dst_len aug_len = do { + (pk, pk_ptr) <- ptr_to_fresh_readonly "pk" (llvm_struct "struct.POINTonE2_affine"); + let signature_ptr = llvm_null; + llvm_precond {{ POINTonE2_affine_invariant pk }}; + hash_or_encode <- crucible_fresh_var "hash_or_encode" (llvm_int 32); + llvm_precond {{ hash_or_encode != zero }}; + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + (dst, dst_ptr) <- ptr_to_fresh_readonly "dst" (llvm_array dst_len (llvm_int 8)); + (aug, aug_ptr) <- ptr_to_fresh_readonly "aug" (llvm_array aug_len (llvm_int 8)); + crucible_execute_func [pk_ptr, signature_ptr, crucible_term hash_or_encode, msg_ptr, crucible_term {{ `msg_len : [64] }}, dst_ptr, crucible_term {{ `dst_len : [64] }}, aug_ptr, crucible_term {{ `aug_len : [64] }}]; + crucible_return (crucible_term {{ if is_point_O E' (POINTonE2_affine_abs pk) then `BLST_PK_IS_INFINITY else if core_verify_pk_in_g2_impl (POINTonE2_affine_abs pk) (POINTonE1_affine_abs zero) msg dst aug then (`BLST_SUCCESS:[32]) else `BLST_VERIFY_FAIL }}); +}; + +// overrides: + +let core_verify_pk_in_g2_overrides = concat mul_fp12_ovs // fp12.saw +[ POINTonE1_from_Jacobian_alias_ov // compress-p1.saw +, POINTonE2_from_Jacobian_ov // compress-p2.saw +, POINTonE1_from_Jacobian_ov // compress-p1.saw +, miller_loop_n_1_ov // pairing.saw +, conjugate_fp12_ov // fp12.saw +, final_exp_alias_ov +, vec_copy_2fp_ov +, vec_copy_POINTonE2_affine_ov +, vec_copy_POINTonE1_affine_ov +, vec_copy_fp12_ov +, vec_select_Fp_ov +, vec_is_zero_10fp_ov +, vec_is_zero_2fp2_ov +, vec_is_zero_2fp_is_equal_ov +, vec_is_equal_fp2_ov +, POINTonE1_in_G1_ov // subgroup_check_g1.saw +]; + +// Assumptions + +let normalize_hash_to_curve_impl_thms msg_len dst_len aug_len = do { + if (eval_bool {{ `aug_len == zero }}) + then do { + l1 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) -> normalize_point Fp (hash_to_curve_opt_impl (msg, DST)) == hash_to_curve_opt_impl (msg, DST) }}; + l2 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) -> Fp.normalize (hash_to_curve_opt_impl (msg, DST)).2 == (hash_to_curve_opt_impl (msg, DST)).2 }}; + return [l1,l2]; + } + else do { + l1 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> normalize_point Fp (hash_to_curve_opt_impl (aug#msg, DST)) == hash_to_curve_opt_impl (aug#msg, DST) }}; + l2 <- simp_then_admit {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> Fp.normalize (hash_to_curve_opt_impl (aug#msg, DST)).2 == (hash_to_curve_opt_impl (aug#msg, DST)).2 }}; + return [l1,l2]; + }; +}; + +miller_loop_zero_thm <- admit_cryptol {{ \x -> fp12_conjugate (miller_loop_opt_checked x BP') == if (is_point_O E x) then Fp_12.field_unit else apply miller_loop_opt_checked x BP' }}; + +// TODO: not sure this is true if pk or sig are invalid. +// core_verify_pk_in_g2_impl_thm <- admit_cryptol {{ \pk sig msg dst aug -> core_verify_pk_in_g2_impl pk sig msg dst aug == core_verify_pk_in_g2 pk sig msg dst aug }}; + +// Proofs + +fp_unit_rep <- eval_term {{ fp_rep Fp.field_unit }}; + +let select_term = rewrite (add_cryptol_defs ["ecEq"] (cryptol_ss ())) {{ \(x:POINTonE1_affine_t) -> select x.0 fp_unit_rep (~(bool_to_limb (Fp.is_equal (fp_abs x.0, Fp.field_zero) /\ Fp.is_equal (fp_abs x.1, Fp.field_zero)) == zero)) }}; + +affinify_projectify_is_id <- admit_cryptol (rewrite (cryptol_ss ()) {{ \x -> affinify E (POINTonE1_abs (x.0,x.1,select_term x)) == if POINTonE1_affine_invariant x then (POINTonE1_affine_abs x) else apply affinify E (POINTonE1_abs (x.0,x.1,select_term x)) }}); + +core_verify_pk_in_g2_POINTonE1_from_Jacobian_sig_preconds <- do { + on_curve <- admit_cryptol (rewrite (cryptol_ss ()) {{ \sig -> is_point_projective E (POINTonE1_abs (sig.0,sig.1,select_term sig)) == if (is_point_affine E (POINTonE1_affine_abs sig)) then True else apply is_point_projective E (POINTonE1_abs (sig.0,sig.1,select_term sig)) }}); + not_zero <- admit_cryptol (rewrite (cryptol_ss ()) {{ \sig-> Fp.is_equal (fp_abs (select_term sig), Fp.field_zero) == (is_point_O E (POINTonE1_affine_abs sig)) }}); + return [on_curve,not_zero]; +}; + +let core_verify_pk_in_g2_POINTonE1_from_Jacobian_hash_preconds msg_len dst_len aug_len = do { + if (eval_bool {{ `aug_len == zero }}) + then do { + on_curve <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) -> is_point_projective E (hash_to_curve_opt_impl (msg, DST)) == True }}); + not_zero <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) -> Fp.is_equal ((hash_to_curve_opt_impl (msg, DST)).2, Fp.field_zero) == False }}); // NOTE: this is unsound, but it's morally okay as it's deemed it will never happen + return [on_curve,not_zero]; + } + else do { + on_curve <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> is_point_projective E (hash_to_curve_opt_impl (aug#msg, DST)) == True }}); + not_zero <- admit_cryptol (rewrite (cryptol_ss ()) {{ \(msg:[msg_len][8]) (DST:[dst_len][8]) (aug:[aug_len][8]) -> Fp.is_equal ((hash_to_curve_opt_impl (aug#msg, DST)).2, Fp.field_zero) == False }}); // NOTE: this is unsound, but it's morally okay as it's deemed it will never happen + return [on_curve,not_zero]; + }; +}; + +let core_verify_pk_in_g2_unints = ["BP'","is_in_g1_impl","hash_to_curve_opt_impl","miller_loop_opt_checked","final_exponentiation_impl","fp12_conjugate","affinify_E","affinify_E'", "projectify_E'", "projectify_E","is_point_projective_E","is_point_projective_E'","is_point_affine_E","is_point_affine_E'","Fp_12"]; // the stuff we want to leave unfolded + +rewrite_unit <- custom_prove_cryptol (rewrite (cryptol_ss ()) {{ fp_abs fp_unit_rep == Fp.field_unit }}) w4; +let BP'_rep = run (eval_term {{ POINTonE2_affine_rep BP' }}); +let BP'_rewrite = run (custom_prove_cryptol (rewrite (cryptol_ss ()) {{ POINTonE2_affine_abs BP'_rep == BP' }}) w4); + +let side_conditions_script msg_len dst_len aug_len = do { + rw_with (concat POINTonE1_thms POINTonE2_thms); + unfolding ["POINTonE1_rep"]; + simplify fp12_simpset; + simplify fp2_simpset; + simplify fp_simpset; + // get rid of normalize terms produced by the rewrites: + let normalize_hash_to_curve_impl_rewrites = run ( normalize_hash_to_curve_impl_thms msg_len dst_len aug_len ); + rw_with (concat normalize_hash_to_curve_impl_rewrites [normalize_miller_loop_opt_checked_thm]); + // take care of the round-trip that sig takes from affine represetation to jacobian and back to affine: + rw_with [affinify_projectify_is_id]; + // establish the preconditions of POINTonE2_from_Jacobian: + let core_verify_pk_in_g2_POINTonE1_from_Jacobian_hash_preconds_thms = run (core_verify_pk_in_g2_POINTonE1_from_Jacobian_hash_preconds msg_len dst_len aug_len); + rw_with (concat core_verify_pk_in_g2_POINTonE1_from_Jacobian_hash_preconds_thms core_verify_pk_in_g2_POINTonE1_from_Jacobian_sig_preconds); + unfolding ["apply"]; + rw_with remove_ho_rules; + goal_eval_unint (concat core_verify_pk_in_g2_unints ["fp_rep","fp_abs","fp_invariant"]); + simplify fp_simpset; + // Not sure why the following is needed.. + let r1 = run (custom_prove_cryptol {{fp_invariant fp_unit_rep == True}} w4); + let r2 = run (custom_prove_cryptol (rewrite (cryptol_ss ()) {{fp_invariant [zero,zero,zero,zero,zero,zero] == True}}) w4); + rw_with [r1,r2]; + w4_unint_z3 (concat core_verify_pk_in_g2_unints ["fp_rep","fp_abs"]); +}; + +let post_condition_script msg_len dst_len aug_len = do { + // get rid of `abs rep` terms + rw_with (concat POINTonE1_thms POINTonE2_thms); + unfolding ["POINTonE1_rep"]; + simplify fp12_simpset; + simplify fp2_simpset; + simplify fp_simpset; + // get rid of normalize terms produced by the rewrites: + let normalize_hash_to_curve_impl_rewrites = run ( normalize_hash_to_curve_impl_thms msg_len dst_len aug_len ); + rw_with (concat normalize_hash_to_curve_impl_rewrites [normalize_miller_loop_opt_checked_thm]); + // take care of the round-trip that sig takes from affine represetation to jacobian and back to affine: + rw_with [affinify_projectify_is_id]; + // rewrite abstracted constants (we're leaving fp_rep and fp_abs uninterpreted, so we need to rewrite the concrete constants): + simplify (addsimps [BP'_rewrite,rewrite_fp12_unit,rewrite_fp2_unit,rewrite_unit] empty_ss); + // we rewrite the spec term: + unfolding ["core_verify_pk_in_g2_impl"]; + rw_with [miller_loop_zero_thm]; + unfolding ["apply"]; + rw_with [rewrite_is_equal]; + rw_with remove_ho_rules; + goal_eval_unint (concat core_verify_pk_in_g2_unints ["fp_rep","fp_abs","POINTonE2_invariant","POINTonE1_invariant","POINTonE2_affine_invariant","POINTonE1_affine_invariant","fp_invariant"]); + rw_with restitching_rules; // TODO: do we need other rules here? + simplify fp_simpset; // get rid of remaining `abs rep` terms + rw_with normalize_final_exp_thms; // get rid of `normalize` terms introduced by fp_simpset + w4_unint_z3 (concat core_verify_pk_in_g2_unints ["fp_rep","fp_abs","POINTonE1_invariant","POINTonE2_invariant","POINTonE2_affine_invariant","POINTonE1_affine_invariant","fp2_invariant","fp_invariant"]); +}; + +let verify_blst_core_verify_pk_in_g2 spec msg_len dst_len aug_len = do { + let Hash_to_G1_ov = run (admit "Hash_to_G1" (Hash_to_G1_impl_spec msg_len DST_len aug_len)); + custom_verify_path_sat + "blst_core_verify_pk_in_g2" + (concat core_verify_pk_in_g2_overrides [Hash_to_G1_ov]) + (spec msg_len dst_len aug_len) + (goal_num_ite 17 + (post_condition_script msg_len dst_len aug_len) + (side_conditions_script msg_len dst_len aug_len)); +}; + +let verify_blst_core_verify_pk_in_g2_non_null = verify_blst_core_verify_pk_in_g2 blst_core_verify_pk_in_g2_non_null_spec; + +let verify_blst_core_verify_pk_in_g2_null_aug = verify_blst_core_verify_pk_in_g2 (\x y z -> blst_core_verify_pk_in_g2_null_aug_spec x y); + +verify_blst_core_verify_pk_in_g2_non_null 32 43 8; +verify_blst_core_verify_pk_in_g2_null_aug 32 43 0; diff --git a/proof/cryptol_imports.saw b/proof/cryptol_imports.saw index 2b9a128c..b1289613 100644 --- a/proof/cryptol_imports.saw +++ b/proof/cryptol_imports.saw @@ -47,3 +47,6 @@ import "../spec/implementation/Fp12.cry"; import "../spec/Pairing.cry"; import "../spec/implementation/PairingImpl.cry"; import "../spec/implementation/FinalExp.cry"; + +import "../spec/implementation/CoreVerifyPKInG1.cry"; +import "../spec/implementation/CoreVerifyPKInG2.cry"; diff --git a/proof/curve_operations.saw b/proof/curve_operations.saw index e984c8d9..bfe745ed 100644 --- a/proof/curve_operations.saw +++ b/proof/curve_operations.saw @@ -29,7 +29,6 @@ more_rewrites <- for let structural_rewrites = concat more_rewrites core_rewrites; - //////////////////////////////////////////////////////////////// // // Operations on E1, over Fp diff --git a/proof/deserialize-p2.saw b/proof/deserialize-p2.saw index f0decc5d..3cb687b7 100644 --- a/proof/deserialize-p2.saw +++ b/proof/deserialize-p2.saw @@ -26,7 +26,7 @@ let blst_p2_uncompress_OK_spec = do { }; // The proof is a compostional verification, in 3 stages: first proofs about POINTonE2_Uncompress_BE, -// themn proofs about POINTonE2_Uncompress, and finally the proof of blst_p2_uncompress. +// then proofs about POINTonE2_Uncompress, and finally the proof of blst_p2_uncompress. // POINTonE2_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. diff --git a/proof/ec_mult.saw b/proof/ec_mult.saw index 9863297f..d4e38fc0 100644 --- a/proof/ec_mult.saw +++ b/proof/ec_mult.saw @@ -276,6 +276,7 @@ let ec_mult_unints = , "precomputed_table" , "add_E", "add'_E", "affinify_E", "projectify_E" ]; +let e1_unints = ec_mult_unints; //////////////// diff --git a/proof/final_exp.saw b/proof/final_exp.saw index 4d47b3b7..efaeaa4f 100644 --- a/proof/final_exp.saw +++ b/proof/final_exp.saw @@ -276,6 +276,14 @@ let final_exp_spec = do { llvm_points_to ret_ptr (llvm_term {{ fp12_rep (final_exponentiation_impl (fp12_abs f)) }}); }; +let final_exp_alias_spec = do { + (f, f_ptr) <- ptr_to_fresh "f" vec384fp12_type; + llvm_precond {{ fp12_invariant f }}; + llvm_execute_func [f_ptr, f_ptr]; + llvm_points_to f_ptr (llvm_term {{ fp12_rep (final_exponentiation_impl (fp12_abs f)) }}); +}; + + vec_copy_fp12_ov <- verify "vec_copy" [] (vec_copy_spec 576 vec384fp12_type); @@ -301,3 +309,25 @@ final_exp_ov <- custom_verify "final_exp" basic_ss); w4_unint_z3 (concat ["raise_to_z_div_by_2", "C_expt"] fp12_unints); }; + +final_exp_alias_ov <- really_custom_verify "final_exp" + (concat [vec_copy_fp12_ov, raise_to_z_div_by_2_ov] fp12_overrides) + final_exp_alias_spec + do { + unfolding ["final_exponentiation_impl", "raise_to_z_div_by_2"]; + simplify fp12_simpset; + simplify (addsimps [ mul_inverse_div_fp12_ov + , to_final_exp_frobenius_map_thm ] + empty_ss); + simplify (addsimps [ cyclotomic_sqr_fp12_C_expt_thm + , double_C_expt_thm + , fp12_conjugate_C_expt_thm + , mul_C_expt_thm + , mul_commutes_fp12_thm + , mul_C_expt_base_thm + , final_exp_frobenius_map_is_cyclotomic_thm + , expt_final_exp_frobenius_map_is_cyclotomic_thm + , frobenius_map_fp12_C_expt_thm ] + basic_ss); + w4_unint_z3 (concat ["raise_to_z_div_by_2", "C_expt"] fp12_unints); + }; diff --git a/proof/fp_overrides.saw b/proof/fp_overrides.saw index 7c3f27eb..00ffc9b7 100644 --- a/proof/fp_overrides.saw +++ b/proof/fp_overrides.saw @@ -292,7 +292,6 @@ fp_alg_thms <- for , {{ Fp.neg Fp.field_zero == Fp.field_zero }} // -0 = 0 ] (\ t -> prove_cryptol t []); - //////////////////////////////////////////////////////////////// // // Overrides for the fp_operations diff --git a/proof/functional_proofs.saw b/proof/functional_proofs.saw index 948d1044..102ad6bb 100644 --- a/proof/functional_proofs.saw +++ b/proof/functional_proofs.saw @@ -32,6 +32,7 @@ include "ec_mult.saw"; include "subgroup_check_g1.saw"; include "sgn0.saw"; include "hash_to_g1.saw"; + include "compress-p1.saw"; include "deserialize-p1.saw"; include "aggregate_in_g1.saw"; @@ -54,3 +55,9 @@ include "384x384_ops.saw"; include "fp12.saw"; include "pairing.saw"; include "final_exp.saw"; + +include "core_verify_pk_in_g1.saw"; +include "core_verify_pk_in_g2.saw"; + +include "bls_operations.saw"; +include "min_key.saw"; diff --git a/proof/hash_to_field.saw b/proof/hash_to_field.saw index 0d3e62ea..149dca75 100644 --- a/proof/hash_to_field.saw +++ b/proof/hash_to_field.saw @@ -144,9 +144,7 @@ let verify_hash_to_field_for aug_len msg_len DST_len nelems = do { let len_in_bytes = eval_size {| L*nelems |}; block_data_order_ovs <- make_block_data_order_ovs [aug_len, msg_len, eval_size {| (33+DST_len+1+9)+63 |}]; // last size is b_i_blocks from hash_to_field.c expand_message_ov <- custom_verify "expand_message_xmd" (concat bcopy_ovs (concat block_data_order_ovs [blst_sha256_emit_ov, blst_sha256_hcopy_ov])) (expand_message_spec len_in_bytes aug_len msg_len DST_len) abc; // z3 takes forever, but abc does better - // expand_message_ov <- admit "expand_message_xmd" (expand_message_spec len_in_bytes aug_len msg_len DST_len); let overrides = [expand_message_ov, limbs_from_be_bytes_ov, redc_mont_384_ov, mul_mont_384_ov]; - // r <- admit "hash_to_field" (hash_to_field_fp_spec nelems aug_len msg_len DST_len); r <- custom_verify "hash_to_field" overrides (hash_to_field_fp_spec nelems aug_len msg_len DST_len) (do { // assume_unsat;}); @@ -174,9 +172,7 @@ let verify_hash_to_field_fp2_for aug_len msg_len DST_len nelems = do { let len_in_bytes = eval_size {| L*2*nelems |}; block_data_order_ovs <- make_block_data_order_ovs [aug_len, msg_len, eval_size {| (33+DST_len+1+9)+63 |}]; // last size is b_i_blocks from hash_to_field.c expand_message_ov <- custom_verify "expand_message_xmd" (concat bcopy_ovs (concat block_data_order_ovs [blst_sha256_emit_ov, blst_sha256_hcopy_ov])) (expand_message_spec len_in_bytes aug_len msg_len DST_len) abc; // z3 takes forever, but abc does better - // expand_message_ov <- admit "expand_message_xmd" (expand_message_spec len_in_bytes aug_len msg_len DST_len); let overrides = [expand_message_ov, limbs_from_be_bytes_ov, redc_mont_384_ov, mul_mont_384_ov]; - // r <- admit "hash_to_field" (hash_to_field_fp2_spec nelems aug_len msg_len DST_len); r <- custom_verify "hash_to_field" overrides (hash_to_field_fp2_spec nelems aug_len msg_len DST_len) do { // assume_unsat;}); diff --git a/proof/hash_to_g1.saw b/proof/hash_to_g1.saw index ca0b3f92..0a7bbe3f 100644 --- a/proof/hash_to_g1.saw +++ b/proof/hash_to_g1.saw @@ -545,8 +545,6 @@ let prove_hash_to_curve_E1_opt_impl_equiv_thm msg_len DST_len = custom_prove_cry w4_unint_z3 (concat fp_unints ["HE1::iso_map","HE1::map_to_curve_simple_swu","HE1::clear_cofactor","HashToCurveE1::hash_to_field"]); }; -// The final overrides: - let prove_Hash_to_G1_impl_ov msg_len DST_len aug_len = do { hash_to_field_fp_ov <- verify_hash_to_field_for aug_len msg_len DST_len 2; // we need two fp elements custom_verify @@ -579,8 +577,6 @@ let prove_hash_to_g1_impl_ov msg_len DST_len aug_len = do { (w4_unint_z3 ["hash_to_curve_opt_impl"]); }; -// TODO below - let prove_hash_to_g1_ov msg_len DST_len aug_len = do { Hash_to_G1_ov <- prove_Hash_to_G1_impl_ov msg_len DST_len aug_len; custom_verify //test @@ -610,7 +606,7 @@ let DST_len= 43; // "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_" in the chosen prove_hash_to_g1_impl_ov msg_len DST_len aug_len; prove_hash_to_g1_ov msg_len DST_len aug_len; -prove_hash_to_g1_impl_ov msg_len DST_len 0; +hash_to_g1_impl_ov <- prove_hash_to_g1_impl_ov msg_len DST_len 0; prove_hash_to_g1_ov msg_len DST_len 0; // another value of msg_len: @@ -620,3 +616,9 @@ prove_hash_to_g1_impl_ov msg_len DST_len aug_len; prove_hash_to_g1_ov msg_len DST_len aug_len; prove_hash_to_g1_impl_ov msg_len DST_len 0; prove_hash_to_g1_ov msg_len DST_len 0; + +// Used in bls_operations.saw: +// TODO: does not seem to work if called in bls_operations.saw +hash_to_curve_E1_opt_impl_equiv_ov <- (prove_hash_to_curve_E1_opt_impl_equiv_thm 32 43); +hash_to_g1_ov <- prove_hash_to_g1_ov 32 43 0; + diff --git a/proof/hash_to_g2.saw b/proof/hash_to_g2.saw index 217d6d17..7205b987 100644 --- a/proof/hash_to_g2.saw +++ b/proof/hash_to_g2.saw @@ -386,7 +386,7 @@ prove_blst_hash_to_g2_abstract_postcond msg_len DST_len aug_len ; prove_blst_hash_to_g2_impl msg_len DST_len aug_len ; // and with aug_len=0 for the basic scheme: prove_blst_hash_to_g2_abstract_postcond msg_len DST_len 0 ; -prove_blst_hash_to_g2_impl msg_len DST_len 0 ; +hash_to_g2_impl_ov <- prove_blst_hash_to_g2_impl msg_len DST_len 0 ; // another value of msg_len: let msg_len = 69; diff --git a/proof/horrible_core_terms.saw b/proof/horrible_core_terms.saw new file mode 100644 index 00000000..efd11f4f --- /dev/null +++ b/proof/horrible_core_terms.saw @@ -0,0 +1,497 @@ +let at_48_cores = + [ parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 0" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 1" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 2" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 3" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 4" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 5" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 6" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 7" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 8" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 9" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 10" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 11" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 12" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 13" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 14" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 15" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 16" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 17" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 18" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 19" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 20" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 21" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 22" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 23" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 24" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 25" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 26" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 27" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 28" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 29" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 30" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 31" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 32" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 33" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 34" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 35" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 36" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 37" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 38" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 39" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 40" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 41" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 42" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 43" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 44" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 45" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 46" + , parse_core "\\(v:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) v 47" ]; + +let at_48_0 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 0"; +let at_48_1 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 1"; +let at_48_2 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 2"; +let at_48_3 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 3"; +let at_48_4 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 4"; +let at_48_5 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 5"; +let at_48_6 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 6"; +let at_48_7 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 7"; +let at_48_8 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 8"; +let at_48_9 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 9"; +let at_48_10 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 10"; +let at_48_11 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 11"; +let at_48_12 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 12"; +let at_48_13 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 13"; +let at_48_14 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 14"; +let at_48_15 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 15"; +let at_48_16 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 16"; +let at_48_17 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 17"; +let at_48_18 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 18"; +let at_48_19 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 19"; +let at_48_20 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 20"; +let at_48_21 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 21"; +let at_48_22 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 22"; +let at_48_23 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 23"; +let at_48_24 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 24"; +let at_48_25 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 25"; +let at_48_26 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 26"; +let at_48_27 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 27"; +let at_48_28 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 28"; +let at_48_29 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 29"; +let at_48_30 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 30"; +let at_48_31 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 31"; +let at_48_32 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 32"; +let at_48_33 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 33"; +let at_48_34 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 34"; +let at_48_35 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 35"; +let at_48_36 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 36"; +let at_48_37 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 37"; +let at_48_38 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 38"; +let at_48_39 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 39"; +let at_48_40 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 40"; +let at_48_41 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 41"; +let at_48_42 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 42"; +let at_48_43 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 43"; +let at_48_44 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 44"; +let at_48_45 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 45"; +let at_48_46 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 46"; +let at_48_47 = parse_core "\\(x:Vec 48 (Vec 8 Bool)) -> at 48 (Vec 8 Bool) x 47"; + +unrip_thm_48 <- prove_cryptol (rewrite (cryptol_ss()) + {{ \(v : [48][8]) -> + [ at_48_0 v + , at_48_1 v + , at_48_2 v + , at_48_3 v + , at_48_4 v + , at_48_5 v + , at_48_6 v + , at_48_7 v + , at_48_8 v + , at_48_9 v + , at_48_10 v + , at_48_11 v + , at_48_12 v + , at_48_13 v + , at_48_14 v + , at_48_15 v + , at_48_16 v + , at_48_17 v + , at_48_18 v + , at_48_19 v + , at_48_20 v + , at_48_21 v + , at_48_22 v + , at_48_23 v + , at_48_24 v + , at_48_25 v + , at_48_26 v + , at_48_27 v + , at_48_28 v + , at_48_29 v + , at_48_30 v + , at_48_31 v + , at_48_32 v + , at_48_33 v + , at_48_34 v + , at_48_35 v + , at_48_36 v + , at_48_37 v + , at_48_38 v + , at_48_39 v + , at_48_40 v + , at_48_41 v + , at_48_42 v + , at_48_43 v + , at_48_44 v + , at_48_45 v + , at_48_46 v + , at_48_47 v + ] == v }}) []; + +let at_96_cores = + [ parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 0" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 1" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 2" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 3" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 4" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 5" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 6" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 7" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 8" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 9" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 10" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 11" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 12" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 13" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 14" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 15" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 16" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 17" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 18" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 19" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 20" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 21" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 22" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 23" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 24" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 25" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 26" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 27" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 28" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 29" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 30" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 31" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 32" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 33" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 34" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 35" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 36" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 37" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 38" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 39" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 40" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 41" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 42" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 43" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 44" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 45" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 46" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 47" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 48" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 49" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 50" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 51" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 52" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 53" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 54" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 55" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 56" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 57" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 58" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 59" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 60" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 61" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 62" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 63" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 64" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 65" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 66" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 67" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 68" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 69" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 70" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 71" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 72" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 73" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 74" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 75" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 76" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 77" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 78" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 79" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 80" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 81" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 82" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 83" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 84" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 85" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 86" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 87" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 88" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 89" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 90" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 91" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 92" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 93" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 94" + , parse_core "\\(v:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) v 95" ]; + +let at_96_0 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 0"; +let at_96_1 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 1"; +let at_96_2 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 2"; +let at_96_3 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 3"; +let at_96_4 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 4"; +let at_96_5 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 5"; +let at_96_6 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 6"; +let at_96_7 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 7"; +let at_96_8 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 8"; +let at_96_9 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 9"; +let at_96_10 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 10"; +let at_96_11 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 11"; +let at_96_12 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 12"; +let at_96_13 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 13"; +let at_96_14 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 14"; +let at_96_15 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 15"; +let at_96_16 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 16"; +let at_96_17 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 17"; +let at_96_18 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 18"; +let at_96_19 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 19"; +let at_96_20 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 20"; +let at_96_21 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 21"; +let at_96_22 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 22"; +let at_96_23 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 23"; +let at_96_24 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 24"; +let at_96_25 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 25"; +let at_96_26 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 26"; +let at_96_27 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 27"; +let at_96_28 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 28"; +let at_96_29 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 29"; +let at_96_30 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 30"; +let at_96_31 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 31"; +let at_96_32 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 32"; +let at_96_33 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 33"; +let at_96_34 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 34"; +let at_96_35 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 35"; +let at_96_36 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 36"; +let at_96_37 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 37"; +let at_96_38 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 38"; +let at_96_39 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 39"; +let at_96_40 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 40"; +let at_96_41 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 41"; +let at_96_42 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 42"; +let at_96_43 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 43"; +let at_96_44 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 44"; +let at_96_45 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 45"; +let at_96_46 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 46"; +let at_96_47 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 47"; +let at_96_48 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 48"; +let at_96_49 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 49"; +let at_96_50 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 50"; +let at_96_51 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 51"; +let at_96_52 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 52"; +let at_96_53 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 53"; +let at_96_54 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 54"; +let at_96_55 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 55"; +let at_96_56 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 56"; +let at_96_57 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 57"; +let at_96_58 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 58"; +let at_96_59 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 59"; +let at_96_60 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 60"; +let at_96_61 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 61"; +let at_96_62 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 62"; +let at_96_63 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 63"; +let at_96_64 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 64"; +let at_96_65 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 65"; +let at_96_66 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 66"; +let at_96_67 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 67"; +let at_96_68 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 68"; +let at_96_69 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 69"; +let at_96_70 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 70"; +let at_96_71 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 71"; +let at_96_72 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 72"; +let at_96_73 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 73"; +let at_96_74 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 74"; +let at_96_75 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 75"; +let at_96_76 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 76"; +let at_96_77 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 77"; +let at_96_78 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 78"; +let at_96_79 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 79"; +let at_96_80 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 80"; +let at_96_81 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 81"; +let at_96_82 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 82"; +let at_96_83 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 83"; +let at_96_84 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 84"; +let at_96_85 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 85"; +let at_96_86 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 86"; +let at_96_87 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 87"; +let at_96_88 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 88"; +let at_96_89 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 89"; +let at_96_90 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 90"; +let at_96_91 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 91"; +let at_96_92 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 92"; +let at_96_93 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 93"; +let at_96_94 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 94"; +let at_96_95 = parse_core "\\(x:Vec 96 (Vec 8 Bool)) -> at 96 (Vec 8 Bool) x 95"; + +unrip_thm_96 <- prove_cryptol (rewrite (cryptol_ss()) + {{ \(v : [96][8]) -> + [ at_96_0 v + , at_96_1 v + , at_96_2 v + , at_96_3 v + , at_96_4 v + , at_96_5 v + , at_96_6 v + , at_96_7 v + , at_96_8 v + , at_96_9 v + , at_96_10 v + , at_96_11 v + , at_96_12 v + , at_96_13 v + , at_96_14 v + , at_96_15 v + , at_96_16 v + , at_96_17 v + , at_96_18 v + , at_96_19 v + , at_96_20 v + , at_96_21 v + , at_96_22 v + , at_96_23 v + , at_96_24 v + , at_96_25 v + , at_96_26 v + , at_96_27 v + , at_96_28 v + , at_96_29 v + , at_96_30 v + , at_96_31 v + , at_96_32 v + , at_96_33 v + , at_96_34 v + , at_96_35 v + , at_96_36 v + , at_96_37 v + , at_96_38 v + , at_96_39 v + , at_96_40 v + , at_96_41 v + , at_96_42 v + , at_96_43 v + , at_96_44 v + , at_96_45 v + , at_96_46 v + , at_96_47 v + , at_96_48 v + , at_96_49 v + , at_96_50 v + , at_96_51 v + , at_96_52 v + , at_96_53 v + , at_96_54 v + , at_96_55 v + , at_96_56 v + , at_96_57 v + , at_96_58 v + , at_96_59 v + , at_96_60 v + , at_96_61 v + , at_96_62 v + , at_96_63 v + , at_96_64 v + , at_96_65 v + , at_96_66 v + , at_96_67 v + , at_96_68 v + , at_96_69 v + , at_96_70 v + , at_96_71 v + , at_96_72 v + , at_96_73 v + , at_96_74 v + , at_96_75 v + , at_96_76 v + , at_96_77 v + , at_96_78 v + , at_96_79 v + , at_96_80 v + , at_96_81 v + , at_96_82 v + , at_96_83 v + , at_96_84 v + , at_96_85 v + , at_96_86 v + , at_96_87 v + , at_96_88 v + , at_96_89 v + , at_96_90 v + , at_96_91 v + , at_96_92 v + , at_96_93 v + , at_96_94 v + , at_96_95 v + ] == v }}) []; + +hoist_unrip_48_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b (x1 : [48][8]) (x2 : [48][8]) -> + [ if b then at_48_0 x1 else at_48_0 x2 + , if b then at_48_1 x1 else at_48_1 x2 + , if b then at_48_2 x1 else at_48_2 x2 + , if b then at_48_3 x1 else at_48_3 x2 + , if b then at_48_4 x1 else at_48_4 x2 + , if b then at_48_5 x1 else at_48_5 x2 + , if b then at_48_6 x1 else at_48_6 x2 + , if b then at_48_7 x1 else at_48_7 x2 + , if b then at_48_8 x1 else at_48_8 x2 + , if b then at_48_9 x1 else at_48_9 x2 + , if b then at_48_10 x1 else at_48_10 x2 + , if b then at_48_11 x1 else at_48_11 x2 + , if b then at_48_12 x1 else at_48_12 x2 + , if b then at_48_13 x1 else at_48_13 x2 + , if b then at_48_14 x1 else at_48_14 x2 + , if b then at_48_15 x1 else at_48_15 x2 + , if b then at_48_16 x1 else at_48_16 x2 + , if b then at_48_17 x1 else at_48_17 x2 + , if b then at_48_18 x1 else at_48_18 x2 + , if b then at_48_19 x1 else at_48_19 x2 + , if b then at_48_20 x1 else at_48_20 x2 + , if b then at_48_21 x1 else at_48_21 x2 + , if b then at_48_22 x1 else at_48_22 x2 + , if b then at_48_23 x1 else at_48_23 x2 + , if b then at_48_24 x1 else at_48_24 x2 + , if b then at_48_25 x1 else at_48_25 x2 + , if b then at_48_26 x1 else at_48_26 x2 + , if b then at_48_27 x1 else at_48_27 x2 + , if b then at_48_28 x1 else at_48_28 x2 + , if b then at_48_29 x1 else at_48_29 x2 + , if b then at_48_30 x1 else at_48_30 x2 + , if b then at_48_31 x1 else at_48_31 x2 + , if b then at_48_32 x1 else at_48_32 x2 + , if b then at_48_33 x1 else at_48_33 x2 + , if b then at_48_34 x1 else at_48_34 x2 + , if b then at_48_35 x1 else at_48_35 x2 + , if b then at_48_36 x1 else at_48_36 x2 + , if b then at_48_37 x1 else at_48_37 x2 + , if b then at_48_38 x1 else at_48_38 x2 + , if b then at_48_39 x1 else at_48_39 x2 + , if b then at_48_40 x1 else at_48_40 x2 + , if b then at_48_41 x1 else at_48_41 x2 + , if b then at_48_42 x1 else at_48_42 x2 + , if b then at_48_43 x1 else at_48_43 x2 + , if b then at_48_44 x1 else at_48_44 x2 + , if b then at_48_45 x1 else at_48_45 x2 + , if b then at_48_46 x1 else at_48_46 x2 + , if b then at_48_47 x1 else at_48_47 x2 + ] == (if b then x1 else x2) }}) []; diff --git a/proof/min_key.saw b/proof/min_key.saw new file mode 100644 index 00000000..e671a8fe --- /dev/null +++ b/proof/min_key.saw @@ -0,0 +1,391 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +// TODO: Rename this file + +BMPKS <- cryptol_load "../spec/BLSMinimalPublicKeySize.cry"; + +/* +let do_prove = true; +include "proof-helpers.saw"; +*/ + +let {{ + pubkey_to_point_is_affine_min_key: [48][8] -> Bool + pubkey_to_point_is_affine_min_key pk = + // TODO: I had to manually unfold pubkey_to_point here. Could that cause + // problems in the proof?? + maybe_cases (uncompress_E1 pk) + False + (\y -> is_point_affine E y) +}}; + +let demo_SkToPk_B_spec = do { + let n_bytes = 32; + let bits = 255; + out_ptr <- llvm_alloc (llvm_array 48 (llvm_int 8)); + scalar_ptr <- crucible_alloc_readonly_aligned 8 (llvm_array n_bytes (llvm_int 8)); + scalar <- crucible_fresh_var "scalar" (llvm_array n_bytes (llvm_int 8)); + crucible_points_to scalar_ptr (crucible_term scalar); + // extra precondition from POINTonE2_mult_w5 + crucible_precond {{ e1_order BP > scalar_value`{bits,n_bytes} scalar + shift }}; + llvm_precond {{ scalar != zero }}; + llvm_execute_func [out_ptr, scalar_ptr]; + llvm_points_to out_ptr (llvm_term {{ (split`{each=8} (BMPKS::sk_to_pk (drop_join_reverse scalar))) }}); +}; + +affine_E_inv_thm <- test_cryptol (rewrite (cryptol_ss()) + {{ \P1 P2 -> + (and_core (same_point_affine E (affinify E (POINTonE1_abs P1)) P2) + (and_core (POINTonE1_invariant P1) + (and_core (not_core (is_bad_O_form_E P1)) + (is_point_projective E (POINTonE1_abs P1))))) == + (same_point_affine E (affinify E (POINTonE1_abs P1)) P2 /\ + ~(is_bad_O_form_E P1) /\ + // TODO: Might need that P1/P2 are not point_O (see + // hash_to_g2.saw:118). Can hash to curve even return point_O? + is_point_affine E P2) }}); + +BP_is_point_affine_thm <- prove_cryptol + {{ is_point_affine E BP == True }} []; + +e1_scalar_mult_not_bad_O_min_pk_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \P sk -> (same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) BP)) == + ((apply same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) BP)) && + ~(is_bad_O_form_E P)) }}); + +test_thm_correct_min_pk <- custom_prove_cryptol (rewrite (cryptol_ss()) + {{ \P sk -> (same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) BP)) == + ((apply same_point_affine + E + (affinify E (POINTonE1_abs P)) + (e1_scalar_mult (scalar_value`{255,32} sk) BP)) && + POINTonE1_invariant P && + ~(is_bad_O_form_E P) && + is_point_projective E (POINTonE1_abs P)) }}) + do { + rw_with_1 e1_scalar_mult_not_bad_O_min_pk_thm; + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps [ affine_E_inv_thm + , affine_inv_affine_rep_e1_thm + , e1_scalar_mult_on_curve_thm + , BP_is_point_affine_thm ] empty_ss); + simplify basic_ss; + simplify (addsimp same_point_affine_E_thm empty_ss); + print_goal; + w4_unint_z3 (concat [ "e1_scalar_mult" + , "is_bad_O_form_E" + , "scalar_value" + , "same_point_affine_E" ] + e1_unints); + }; + +mult_scalar_mult_E_thm <- admit_cryptol + {{ \b P -> mult E b P == e1_scalar_mult (toInt b) P }}; + + // TODO: This feels provable +affinify_affine_E1_thm <- test_cryptol + {{ \P -> serialize_E1 (fp_abs P.0, fp_abs P.1) == + if (fp_abs P.2) == Fp.field_unit + then serialize_E1 (affinify E (POINTonE1_abs P)) + else apply serialize_E1 (fp_abs P.0, fp_abs P.1) }}; + +if_elim_48_thms <- for at_48_cores + (\x -> prove_cryptol (rewrite (cryptol_ss()) + {{ \b1 b2 b3 (x1 : [48][8]) (x2 : [48][8]) -> + (if (and_core (and_core b1 b2) b3) + then x (if b2 then x1 else x2) + else (x x1)) == (x x1) }}) []); + + +demo_SkToPk_B_ov <- custom_verify "demo_SkToPk_B" + [blst_sk_to_pk_in_g1_ov, blst_p1_compress_projective_ov, blst_p1_compress_affine_ov] + demo_SkToPk_B_spec + do { + unfolding [ "BMPKS::sk_to_pk" + , "BLSMinimalPublicKeySize::module parameter point_to_pubkey" + , "BLSMinimalPublicKeySize::module parameter other_curve" + , "BLSMinimalPublicKeySize::module parameter P" + , "BLSMinimalPublicKeySize::other_curve" + , "BLSMinimalPublicKeySize::P" + , "BLSMinimalPublicKeySize::point_to_pubkey" ]; + simplify (cryptol_ss()); + simplify (addsimp eq_to_same_point_affine_E_thm empty_ss); + simplify (addsimps [test_thm_correct_min_pk] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["apply"]; + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 O_O_unit_implies_bad_O_form_E; + unfolding ["apply"]; + // END precond proof + simplify (addsimps (concat split_join_thms + [mult_scalar_mult_E_thm, + affinify_affine_E1_thm, + fold_scalar_value_thm, + serialize_e1_eq_thm]) + empty_ss); + simplify (addsimps split_join_thms empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + simplify (addsimps if_elim_48_thms empty_ss); + simplify (addsimps [unrip_thm_48, serialize_e1_eq_thm] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + unfolding ["apply"]; + rw_with remove_ho_rules; + simplify (addsimp same_point_affine_E_thm empty_ss); + print_goal; + w4_unint_z3 (concat [ "e1_order" + , "is_point_projective_E" + , "is_bad_O_form_E" + , "scalar_value" + , "POINTonE2_abs" + , "serialize_E1" + , "fp_abs" + , "e1_scalar_mult" + , "same_point_affine_E" + , "POINTonE1_invariant" ] + e1_unints); + }; + +let demo_KeyValidate_B_spec = do { + (inp, in_ptr) <- ptr_to_fresh_readonly "POINTonE1_Uncompress_in" compressed_E1_rep_type; + crucible_precond {{ uncompress_E1_imp inp != nothing }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ ~((inp@0)@1) }}; + llvm_precond {{ pubkey_to_point_is_affine_min_key inp }}; + // TODO: Maybe drop this precond vv + crucible_precond {{ uncompress_E1_x_fp inp != Fp.field_zero }}; + // TODO: Explain (the library disagrees with spec on treating point_O as on + // the curve?) + let uncompressed_inp = {{ uncompress_E1_OK inp }}; + llvm_precond {{ ~(((uncompressed_inp.0) == Fp.field_zero) /\ + ((uncompressed_inp.1) == Fp.field_zero)) }}; + llvm_execute_func [ in_ptr ]; + // TODO: Postcond + llvm_return (llvm_term {{ bool_to_limb (BMPKS::KeyValidate (join inp)) }}); +}; + +// TODO: Is this proved somewhere? +uncompress_E1_uncompress_E1_OK_thm <- admit_cryptol (rewrite (cryptol_ss()) + {{ \x -> uncompress_E1 x == + if uncompress_E1_imp x != nothing + then (True, uncompress_E1_OK x) + else apply uncompress_E1 x }}); + +just_e1_thm <- prove_cryptol (rewrite (cryptol_ss()) {{ \(x : AffinePoint t_Fp) -> just x == (True, x) }}) []; + +fold_normalize_affine_fp_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \P -> (Fp.normalize P.0, Fp.normalize P.1) == + normalize_affine_point Fp P }}) []; + +hoist_pair_fp_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \b (x : t_Fp) (y : t_Fp) -> (x, if b then y else x) == + if b then (x, y) else (x, x) }}) []; + +normalize_point_O_E_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ normalize_affine_point Fp (point_O E) == point_O E }}) []; + +is_in_g1_impl_min_key_thm <- admit_cryptol + (rewrite (cryptol_ss()) + {{ \P -> BMPKS::reexport_pubkey_subgroup_check P == + if is_point_affine_E P + then is_in_g1_impl P + else apply BMPKS::reexport_pubkey_subgroup_check P }}); + +hoist_POINTonE1_affine_invariant <- prove_cryptol + (rewrite (cryptol_ss()) + {{ \c p1 p2 -> POINTonE1_affine_invariant (if c then p1 else p2) == + if c then POINTonE1_affine_invariant p1 else POINTonE1_affine_invariant p2 }}) + ["POINTonE1_affine_invariant"]; + +inteq_core <- parse_core "intEq"; + +fold_is_point_O_E_thm <- prove_cryptol (rewrite (cryptol_ss()) + {{ \x y -> ((inteq_core x Fp.field_zero) /\ (inteq_core y Fp.field_zero)) == + is_point_O E (x, y) }}) []; + +demo_KeyValidate_B_ov <- custom_verify "demo_KeyValidate_B" + [ POINTonE1_Uncompress_OK_ov //blst_p1_uncompress_OK_ov + , POINTonE1_affine_on_curve_ov + , vec_is_zero_2fp_ov + , blst_p1_affine_in_g1_ov ] + demo_KeyValidate_B_spec + do { + unfolding [ "BMPKS::KeyValidate" + , "maybe_cases" + , "BLSMinimalPublicKeySize::module parameter pubkey_to_point" + , "BLSMinimalPublicKeySize::module parameter other_curve" + , "bool_to_limb" + , "POINTonE1_affine_rep" + , "pubkey_to_point_is_affine_min_key" + , "POINTonE1_affine_abs" + , "BLSMinimalPublicKeySize::other_curve" + , "BLSMinimalPublicKeySize::pubkey_to_point" ]; + simplify (addsimp is_point_affine_E_thm empty_ss); + simplify (addsimps [ uncompress_E1_OK_on_curve] empty_ss); + simplify basic_ss; + simplify (addsimp is_point_O_E_affine_rev_thm empty_ss); + simplify (cryptol_ss()); + simplify (addsimps core_rewrites empty_ss); + simplify (addsimp fp_abs_ite_thm empty_ss); + simplify fp_simpset; + simplify (addsimp is_in_g1_impl_min_key_thm empty_ss); + simplify basic_ss; + simplify (addsimp is_point_O_E_thm empty_ss); + simplify (basic_ss); + simplify (addsimps [ hoist_POINTonE1_affine_rep + , affine_inv_affine_rep_e1_thm + , hoist_POINTonE1_affine_invariant ] empty_ss); + simplify (basic_ss); + simplify (cryptol_ss()); + simplify (addsimps core_rewrites empty_ss); + simplify (addsimps split_join_thms empty_ss); + simplify (addsimps [ uncompress_E1_uncompress_E1_OK_thm ] empty_ss); + goal_num_ite 4 + (do { + simplify (addsimp just_e1_thm empty_ss); + simplify (basic_ss); + simplify (cryptol_ss()); + simplify (addsimps [ fold_normalize_affine_fp_thm + , hoist_pair_fp_thm + , fold_is_point_O_E_thm + , normalize_point_O_E_thm + , normalize_uncompress_E1_OK_thm + , zero_lt_one_thm + , hoist_normalize_affine_fp_thm ] empty_ss); + unfolding [ "POINTonE1_affine_invariant" + , "apply" + , "uncompress_E1_imp" ]; + rw_with fp_rep_thms; + simplify (basic_ss); + simplify (cryptol_ss()); + rw_with remove_ho_rules; + (print_goal); + w4_unint_z3 (concat [ "is_in_g1_impl" + , "uncompress_E1_OK" + , "is_point_affine_E" + , "BMPKS::reexport_pubkey_subgroup_check" + , "is_point_O_E" + , "is_point_affine_E" + , "uncompress_E1" + , "POINTonE1_affine_invariant" + , "fp_rep" + , "uncompress_E1_imp"] + BasicVerify_A_unints); + }) + (do { + simplify remove_higher_order_function_simpset; + unfolding [ "POINTonE1_affine_invariant" + , "uncompress_E1_imp" ]; + rw_with fp_rep_thms; + (print_goal); + w4_unint_z3 [ "is_in_g1_impl" + , "Fp" + , "uncompress_E1_OK" + , "is_point_affine_E" + , "BMPKS::reexport_pubkey_subgroup_check" + , "is_point_O_E" + , "is_point_affine_E" + , "uncompress_E1" + , "uncompress_E1_imp"]; + }); + }; + +let demo_BasicSign_B_spec = do { + //let DST = {{ "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_" }}; + global_alloc_init "demo_DST_B" {{ DST }}; + let msg_len = 32; + out_ptr <- llvm_alloc (llvm_array 96 (llvm_int 8)); + // SK must be aligned + SK_ptr <- llvm_alloc_readonly_aligned 8 pow256_type; + SK <- llvm_fresh_var "SK" pow256_type; + llvm_points_to SK_ptr (llvm_term SK); + (msg, msg_ptr) <- ptr_to_fresh_readonly "msg" (llvm_array msg_len (llvm_int 8)); + // TODO: This precond was the only way I could think of to be able to talk + // about the relationship between SK and the result of blst_hash_to_g2. Is + // there maybe a theorem that would work better? + llvm_precond {{ e2_order (affinify E' (hash_to_curve_E2_opt_impl (msg,DST))) > + scalar_value`{255,32} SK + shift }}; + // TODO: Do I need this precond VV ? + llvm_precond {{ SK != zero }}; + llvm_execute_func [ out_ptr + , SK_ptr + , msg_ptr + , llvm_term {{ `msg_len : [64] }} ]; + // TODO: Endianness? (Both for return, and for args to CoreSign) + // TODO: Postcond + /* + llvm_points_to + out_ptr + (llvm_term + {{ split`{each=8} (BMPKS::CoreSign (drop_join_reverse`{255, 32} SK, + msg)) }}); + */ +}; + +// TODO: Prove +test_thm_correct'_min_pk <- admit_cryptol (rewrite (cryptol_ss()) + {{ \P sk (x:([32][8],[43][8])) -> + (same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) + (affinify E' (hash_to_curve_E2_opt_impl x)))) == + ((apply same_point_affine + E' + (affinify E' (POINTonE2_abs P)) + (e2_scalar_mult (scalar_value`{255,32} sk) + (affinify E' (hash_to_curve_E2_opt_impl x)))) && + POINTonE2_invariant P && + ~(is_bad_O_form_E' P) && + is_point_projective E' (POINTonE2_abs P)) }}); + +demo_BasicSign_B_ov <- really_custom_verify "demo_BasicSign_B" + [ hash_to_g2_impl_ov + , POINTonE2_mult_w5_sk_ov + , blst_p2_compress_affine_ov + , blst_p2_compress_projective_ov ] + demo_BasicSign_B_spec + do { + simplify (addsimp eq_to_same_point_affine_E'_thm (cryptol_ss())); + rw_with POINTonE2_base_thms; + simplify (addsimps POINTonE2_thms (cryptol_ss())); + simplify (addsimp eliminate_normalized_args_affinify_thm empty_ss); + simplify basic_ss; + simplify (addsimps [test_thm_correct'_min_pk] empty_ss); + simplify basic_ss; + simplify (cryptol_ss()); + rw_with_1 O_O_unit_implies_bad_O_form_E'; + unfolding ["apply", "BLSMinimalPublicKeySize::DST", "is_bad_O_form_E'"]; + simplify basic_ss; + simplify (cryptol_ss()); + // BEGIN final goal proof + simplify (addsimps remove_ho_rules empty_ss); + simplify (addsimps [same_point_affine_E'_thm] empty_ss); + (print_goal); + w4_unint_z3 (concat [ "e2_order" + , "e2_scalar_mult" + , "fp2_abs" + , "Fp_2" + , "is_point_projective_E'" + , "hash_to_curve_E2_opt_impl" + , "scalar_value" + , "same_point_affine_E'" ] + ec_mult_unints ); + }; diff --git a/proof/misc_rules.saw b/proof/misc_rules.saw new file mode 100644 index 00000000..68a3ca25 --- /dev/null +++ b/proof/misc_rules.saw @@ -0,0 +1,70 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +let remove_ho_rules = concat + [ point_add_fp2_thm, point_dadd_fp2_thm, point_double_fp2_thm, point_neg_fp2_thm + , point_add_affine_fp2_thm, point_dadd_affine_fp2_thm + , add_E'_thm, add'_E'_thm, neg_E'_thm + , affinify_E'_thm, projectify_E'_thm + , is_point_affine_E'_thm, is_point_projective_E'_thm + , is_point_O_E'_thm ] + [ point_add_fp_thm, point_dadd_fp_thm, point_double_fp_thm, point_neg_fp_thm + , point_add_affine_fp_thm, point_dadd_affine_fp_thm + , add_E_thm, add'_E_thm, affinify_E_thm, projectify_E_thm + , is_point_affine_E_thm, is_point_projective_E_thm, is_point_O_E_thm, point_O_E_thm + ]; + +// a bunch of rules to move ite terms up +hoist_ifs_rules_ <- for [ + {{ \(x1:[64]) x2 x3 x4 x5 x6 y1 y2 y3 y4 y5 y6 c -> [if c then x1 else y1, if c then x2 else y2, if c then x3 else y3, if c then x4 else y4, if c then x5 else y5, if c then x6 else y6] == if c then [x1,x2,x3,x4,x5,x6] else [y1,y2,y3,y4,y5,y6] }} +, {{ \(x1:[64]) x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 c -> [[if c then x1 else y1, if c then x2 else y2, if c then x3 else y3, if c then x4 else y4, if c then x5 else y5, if c then x6 else y6],[if c then x7 else y7, if c then x8 else y8, if c then x9 else y9, if c then x10 else y10, if c then x11 else y11, if c then x12 else y12]] == if c then [[x1,x2,x3,x4,x5,x6],[x7,x8,x9,x10,x11,x12]] else [[y1,y2,y3,y4,y5,y6],[y7,y8,y9,y10,y11,y12]] }} +, {{ \(x1:Integer) x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 c -> [if c then x1 else y1, if c then x2 else y2, if c then x3 else y3, if c then x4 else y4, if c then x5 else y5, if c then x6 else y6,if c then x7 else y7, if c then x8 else y8, if c then x9 else y9, if c then x10 else y10, if c then x11 else y11, if c then x12 else y12] == if c then [x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12] else [y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] }} +, {{ \c (x:[6][64]) y a -> [if c then x else y, a] == if c then [x,a] else [y,a] }} +, {{ \c (x:[6][64]) y a -> [a, if c then x else y] == if c then [a,x] else [a,y] }} +, {{ + \(x:t_Fp_2) y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 c -> ( + [[z1, z2, z3, z4, z5, z6], [z7, z8, z9, z10, z11, z12]] == (if c then [[y1, y2, y3, y4, y5, y6], [y7, y8, y9, y10, y11, y12]] else (fp2_rep x)) where + [a,b] = fp2_rep x + [a1, a2, a3, a4, a5, a6] = a + [b1, b2, b3, b4, b5, b6] = b + z = (if c then [y1, y2, y3, y4, y5, y6, y7, y8, y9, y10, y11, y12] else [a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6]) + [z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12] = z + ) + }} +, {{ \c (x:[12][64]) y -> ([[a1,a2,a3,a4,a5,a6],[a7,a8,a9,a10,a11,a12]] == if c then [[x1,x2,x3,x4,x5,x6],[x7,x8,x9,x10,x11,x12]] else [[y1,y2,y3,y4,y5,y6],[y7,y8,y9,y10,y11,y12]] where [a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12] = (if c then x else y); [x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12] = x; [y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12] = y) }} +, {{ \c (x:[2][6][64]) y (a:[2][6][64]) (b:[2][6][64]) -> (a,b,if c then x else y) == if c then (a,b,x) else (a,b,y) }} +, {{ \c (x:[6][64]) y (a:[6][64]) (b:[6][64]) -> (a,b,if c then x else y) == if c then (a,b,x) else (a,b,y) }} +, {{ \c x y -> POINTonE2_abs (if c then x else y) == if c then POINTonE2_abs x else POINTonE2_abs y }} +, {{ \c x y -> POINTonE1_abs (if c then x else y) == if c then POINTonE1_abs x else POINTonE1_abs y }} +, {{ \c x y -> is_point_projective E' (if c then x else y) == if c then is_point_projective E' x else is_point_projective E' y }} +, {{ \c x y -> is_point_projective E (if c then x else y) == if c then is_point_projective E x else is_point_projective E y }} +, {{ \c x y -> affinify E' (if c then x else y) == if c then affinify E' x else affinify E' y }} +, {{ \c x y -> affinify E (if c then x else y) == if c then affinify E x else affinify E y }} +] (\ eq -> custom_prove_cryptol (rewrite (cryptol_ss ()) eq) + do { + simplify (addsimps remove_ho_rules empty_ss); + w4_unint_z3 ["POINTonE1_abs","POINTonE2_abs","affinify_E'","affinify_E"]; + }); +// ] (\ eq -> custom_prove_cryptol eq w4); + +let hoist_ifs_rules = concat hoist_ifs_rules_ [fp2_abs_ite_thm, fp2_invariant_ite_thm, fp2_rep_ite_thm, fp_abs_ite_thm, fp_invariant_ite_thm, fp_rep_ite_thm]; + +restitching_rules <- for [ + {{ \(x:[6][64]) -> ([x1,x2,x3,x4,x5,x6] == x where [x1,x2,x3,x4,x5,x6] = x) }} +, {{ \(x:[2][6][64]) -> ([x1,x2] == x where [x1,x2] = x) }} +, {{ \(a:[2]Integer) -> ([x,y] == a where [x,y] = a) }} +, {{ \(a:[2][6][64]) -> ([x,y] == a where [x,y] = a) }} +, {{ \(a:[6][64]) -> ([a1,a2,a3,a4,a5,a6] == a where [a1,a2,a3,a4,a5,a6] = a) }} +, {{ + \(x:t_Fp_2) -> ( + [[a1, a2, a3, a4, a5, a6], [b1, b2, b3, b4, b5, b6]] == fp2_rep x where + [a,b] = fp2_rep x + [a1, a2, a3, a4, a5, a6] = a + [b1, b2, b3, b4, b5, b6] = b + ) + }} +] (\ eq -> custom_prove_cryptol (rewrite (cryptol_ss ()) eq) w4); + +let misc_rules = concat hoist_ifs_rules restitching_rules; diff --git a/proof/pairing.saw b/proof/pairing.saw index 4a64628c..768a68d3 100644 --- a/proof/pairing.saw +++ b/proof/pairing.saw @@ -167,7 +167,7 @@ let add_n_dbl_n_spec n k = do { let miller_loop_n_1_spec = do { ret_ptr <- crucible_alloc vec384fp12_type; - (Q, Q_ptr) <- ptr_to_fresh "Q" POINTonE2_affine_type; // array in general + (Q, Q_ptr) <- ptr_to_fresh_readonly "Q" POINTonE2_affine_type; // array in general (P, P_ptr) <- ptr_to_fresh_readonly "P" POINTonE1_affine_type; // array in general crucible_precond {{ POINTonE2_affine_invariant Q }}; crucible_precond {{ POINTonE1_affine_invariant P }}; diff --git a/proof/print_readably.saw b/proof/print_readably.saw index 67bb99ed..2a036d4d 100644 --- a/proof/print_readably.saw +++ b/proof/print_readably.saw @@ -16,6 +16,7 @@ let {{ fp12_unit = Fp_12.field_unit fp12_is_equal = Fp_12.is_equal fp12_neg = Fp_12.neg + fp12_normalize = Fp_12.normalize fp2_mul = Fp_2.mul fp2_sq = Fp_2.sq fp2_add = Fp_2.add @@ -24,6 +25,7 @@ let {{ fp2_unit = Fp_2.field_unit fp2_is_equal = Fp_2.is_equal fp2_neg = Fp_2.neg + fp2_normalize = Fp_2.normalize fp_mul = Fp.mul fp_sq = Fp.sq fp_add = Fp.add @@ -33,7 +35,6 @@ let {{ fp_is_equal = Fp.is_equal fp_neg = Fp.neg fp_normalize = Fp.normalize - fp2_normalize = Fp_2.normalize }}; readability_rewrites <- for [ @@ -63,6 +64,7 @@ readability_rewrites <- for [ , {{ \x y -> Fp_12.is_equal (x,y) == fp12_is_equal (x,y) }} , {{ \p -> Fp.normalize p == fp_normalize p }} , {{ \p -> Fp_2.normalize p == fp2_normalize p }} +, {{ \p -> Fp_12.normalize p == fp12_normalize p }} ] (\e -> custom_prove_cryptol (rewrite (cryptol_ss ()) e) (w4_unint_z3 ["Fp","Fp_2","Fp_12"])); let print_readably = do { // NOTE this modifies the goal diff --git a/proof/proof-helpers.saw b/proof/proof-helpers.saw index 38629828..e639e35c 100644 --- a/proof/proof-helpers.saw +++ b/proof/proof-helpers.saw @@ -38,22 +38,27 @@ let prover = w4_unint_z3; // ... for code proofs -let verify_unint func overrides unints spec = +let verify_unint func overrides unints spec = if do_prove - then crucible_llvm_verify m func overrides false spec (prover unints) + then crucible_llvm_verify m func overrides false spec (prover unints) else crucible_llvm_unsafe_assume_spec m func spec; let verify func overrides spec = - verify_unint func overrides [] spec; + verify_unint func overrides [] spec; let test func overrides spec = if do_prove then crucible_llvm_verify m func overrides false spec (quickcheck 100) else crucible_llvm_unsafe_assume_spec m func spec; -let custom_verify func overrides spec custom_tactic = +let custom_verify func overrides spec custom_tactic = if do_prove - then crucible_llvm_verify m func overrides false spec custom_tactic + then crucible_llvm_verify m func overrides false spec custom_tactic + else crucible_llvm_unsafe_assume_spec m func spec; + +let custom_verify_path_sat func overrides spec custom_tactic = + if do_prove + then crucible_llvm_verify m func overrides true spec custom_tactic else crucible_llvm_unsafe_assume_spec m func spec; let admit func spec = @@ -91,9 +96,9 @@ let really_verify func overrides spec = really_verify_unint func overrides [] spec; let really_test func overrides spec = - crucible_llvm_verify m func overrides false spec (quickcheck 100); + crucible_llvm_verify m func overrides false spec (quickcheck 100); -let really_custom_verify func overrides spec custom_tactic = +let really_custom_verify func overrides spec custom_tactic = crucible_llvm_verify m func overrides false spec custom_tactic; let show_admit func overrides spec = @@ -166,3 +171,11 @@ let print_clean_goal = do { print_goal; }; +// used to force a goal to fail quickly (to see the error message...): +let rewrite_to_false = do { + let implies = parse_core "implies"; + let rewrite_implies_to_false = run ( admit_cryptol (rewrite (cryptol_ss ()) {{ \x y -> (implies x y) == False}}) ); + simplify (addsimp rewrite_implies_to_false empty_ss); +}; + +let big_simpset = []; // to collect rules as we go diff --git a/proof/subgroup_check_g1.saw b/proof/subgroup_check_g1.saw index e3399408..56151ad5 100644 --- a/proof/subgroup_check_g1.saw +++ b/proof/subgroup_check_g1.saw @@ -3,8 +3,6 @@ * SPDX-License-Identifier: Apache-2.0 OR MIT */ -import "../spec/implementation/Types.cry"; // bool_to_limb - let point_op_overrides = concat vec_overrides [ POINTonE1_add_ov, POINTonE1_add_alias_1_2_ov // <= prob not needed , POINTonE1_dadd_null_ov, POINTonE1_dadd_null_alias_1_2_ov diff --git a/proof/subgroup_check_g2.saw b/proof/subgroup_check_g2.saw index 9b06bcdf..5412dbe1 100644 --- a/proof/subgroup_check_g2.saw +++ b/proof/subgroup_check_g2.saw @@ -95,6 +95,7 @@ let POINTonE2_in_g2_spec = do { (p, p_ptr) <- ptr_to_fresh_readonly "p" POINTonE2_affine_type; crucible_precond {{ POINTonE2_affine_invariant p }}; crucible_precond {{ is_point_affine E' (POINTonE2_affine_abs p) }}; // on the curve + crucible_precond {{ ~ (is_point_O E' (POINTonE2_affine_abs p)) }}; // and not at infinity crucible_execute_func [p_ptr]; crucible_return (crucible_term {{ bool_to_limb (is_in_g2_impl (POINTonE2_affine_abs p)) }}); }; @@ -175,9 +176,7 @@ POINTonE2_in_g2_ov <- custom_verify "POINTonE2_in_G2" simplify (addsimps [fp2_abs_POINTonE2_rep_2_thm, is_point_O_thm] basic_ss); // replace the zero test by conditional is_point_O simplify (addsimps (foldr concat [is_point_projective_thms,POINTonE2_thms,hoist_if_thms] [is_point_projective_psi_thm,is_point_projective_POINTonE2_times_minus_z,point_affine_is_point_proj_thm,one_abs_thm', normalize_psi_imp_thm]) basic_ss); // get rid of conditional is_point_O simplify (addsimps (foldr concat [e2_curve_op_thms, POINTonE2_thms, hoist_if_thms] [psi_equiv_thm',affinify_POINTonE2_times_minus_z_thm,one_abs_thm',affinify_projectify_thm,normalize_psi_imp_thm]) basic_ss); // get rid of the implementation curve ops in the term representing the C computation - // stuff from aggregate_in_g2 branch: - // simplify (addsimps (foldr concat [is_point_projective_thms,POINTonE2_thms,hoist_if_thms] [is_point_projective_psi_thm,is_point_projective_POINTonE2_times_minus_z,point_affine_is_point_proj_thm,one_abs_thm']) basic_ss); // get rid of conditional is_point_O - // simplify (addsimps (foldr concat [e2_curve_op_thms, POINTonE2_thms, hoist_if_thms] [psi_equiv_thm',affinify_POINTonE2_times_minus_z_thm,one_abs_thm',affinify_projectify_thm]) basic_ss); // get rid of the implementation curve ops in the term representing the C computation + //w4_unint_z3 (concat e2_unints ["e2_scalar_mult","psi"]); simplify remove_higher_order_function_simpset; w4_unint_z3 (concat e2_unints ["e2_scalar_mult","e2_scalar_mult","psi","psi_imp","POINTonE2_times_minus_z","fp2_invariant"]); }) diff --git a/proof/vect.saw b/proof/vect.saw index 419c23b5..35d1ffdb 100644 --- a/proof/vect.saw +++ b/proof/vect.saw @@ -140,19 +140,35 @@ let vec_is_zero_2fp_spec = do { (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array 2 vec384_type); crucible_precond {{ fp_invariant (a@0) /\ fp_invariant (a@1) }}; crucible_execute_func [a_ptr, crucible_term {{ (96:Size_t) }}]; // Non-portable - crucible_return (crucible_term {{ if fp_abs (a@0) == Fp.field_zero /\ fp_abs (a@1) == Fp.field_zero then 1 else (0:Limb) }}); + crucible_return (crucible_term {{ if fp_abs a0 == Fp.field_zero /\ fp_abs a1 == Fp.field_zero then 1 else (0:Limb) where [a0,a1]=a }}); + }; + +// TODO: let's settle on whether we use is_equal or not... +let vec_is_zero_2fp_is_equal_spec = do { + (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array 2 vec384_type); + crucible_precond {{ fp_invariant (a@0) /\ fp_invariant (a@1) }}; + crucible_execute_func [a_ptr, crucible_term {{ (96:Size_t) }}]; // Non-portable + crucible_return (crucible_term {{ bool_to_limb (Fp.is_equal(fp_abs a0, Fp.field_zero) /\ Fp.is_equal(fp_abs a1, Fp.field_zero)) where [a0,a1]=a }}); }; let vec_is_zero_2fp2_spec = do { (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array 2 vec384x_type); crucible_precond {{ fp2_invariant (a@0) /\ fp2_invariant (a@1) }}; crucible_execute_func [a_ptr, crucible_term {{ (192:Size_t) }}]; // Non-portable - crucible_return (crucible_term {{ if ((Fp_2.is_equal (fp2_abs (a@0), Fp_2.field_zero)) /\ (Fp_2.is_equal (fp2_abs (a@1), Fp_2.field_zero))) then 1 else (0:Limb) }}); - }; // TODO: is this specification okay? + crucible_return (crucible_term {{ (if ((Fp_2.is_equal (fp2_abs a0, Fp_2.field_zero)) /\ (Fp_2.is_equal (fp2_abs a1, Fp_2.field_zero))) then 1 else (0:Limb)) where [a0,a1] = a }}); + }; + +let vec_is_zero_10fp_spec = do { + (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array 10 vec384_type); + crucible_execute_func [a_ptr, crucible_term {{ (480:Size_t) }}]; // Non-portable + crucible_return (crucible_term {{ bool_to_limb (all (\x -> Fp.is_equal (fp_abs x, Fp.field_zero)) a) }}); + }; // TODO: prove vec_is_zero_2fp_ov <- test "vec_is_zero" [] vec_is_zero_2fp_spec; +vec_is_zero_2fp_is_equal_ov <- test "vec_is_zero" [] vec_is_zero_2fp_is_equal_spec; vec_is_zero_2fp2_ov <- test "vec_is_zero" [] vec_is_zero_2fp2_spec; +vec_is_zero_10fp_ov <- test "vec_is_zero" [] vec_is_zero_10fp_spec; // ... continuing with vec_is_equal @@ -187,12 +203,21 @@ let vec_is_equal_fp2_spec = do { (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384x_type; crucible_precond {{ fp2_invariant a /\ fp2_invariant b }}; crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (96:Size_t) }}]; // Non-portable - crucible_return (crucible_term {{ if fp2_abs a == fp2_abs b then 1 else (0:Limb) }}); + crucible_return (crucible_term {{ bool_to_limb (Fp_2.is_equal (fp2_abs a, fp2_abs b)) }}); }; +// let vec_is_equal_fp2_spec_ = do { + // (a, a_ptr) <- ptr_to_fresh_readonly "a" vec384x_type; + // (b, b_ptr) <- ptr_to_fresh_readonly "b" vec384x_type; + // crucible_precond {{ fp2_invariant a /\ fp2_invariant b }}; // TODO: remove + // crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (96:Size_t) }}]; // Non-portable + // crucible_return (crucible_term {{ if a == b then 1 else (0:Limb) }}); + // }; + //TODO: prove vec_is_equal_fp_ov <- test "vec_is_equal" [] vec_is_equal_fp_spec; vec_is_equal_fp2_ov <- test "vec_is_equal" [] vec_is_equal_fp2_spec; +// vec_is_equal_fp2_ov_ <- test "vec_is_equal" [] vec_is_equal_fp2_spec_; let vec_is_equal_2fp_spec = do { (a, a_ptr) <- ptr_to_fresh_readonly "a" (llvm_array 2 vec384_type); @@ -200,8 +225,8 @@ let vec_is_equal_2fp_spec = do { crucible_precond {{ fp_invariant (a@0) /\ fp_invariant (a@1) /\ fp_invariant (b@0) /\ fp_invariant (b@1) }}; crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (96:Size_t) }}]; // Non-portable - crucible_return (crucible_term {{ if fp_abs (a@0) == fp_abs (b@0) /\ fp_abs (a@1) == fp_abs (b@1) - then 1 else (0:Limb) }}); + crucible_return (crucible_term {{ if fp_abs a0 == fp_abs b0 /\ fp_abs a1 == fp_abs b1 + then 1 else (0:Limb) where [a0,a1]=a; [b0,b1]=b}}); }; let vec_is_equal_2fp2_spec = do { @@ -210,8 +235,8 @@ let vec_is_equal_2fp2_spec = do { crucible_precond {{ fp2_invariant (a@0) /\ fp2_invariant (a@1) /\ fp2_invariant (b@0) /\ fp2_invariant (b@1) }}; crucible_execute_func [a_ptr, b_ptr, crucible_term {{ (192:Size_t) }}]; // Non-portable - crucible_return (crucible_term {{ if Fp_2.is_equal(fp2_abs (a@0), fp2_abs (b@0)) /\ Fp_2.is_equal(fp2_abs (a@1), fp2_abs (b@1)) - then 1 else (0:Limb) }}); // TODO: is this specification okay? + crucible_return (crucible_term {{ if Fp_2.is_equal(fp2_abs a0, fp2_abs b0) /\ Fp_2.is_equal(fp2_abs a1, fp2_abs b1) + then 1 else (0:Limb) where [a0,a1]=a; [b0,b1]=b }}); // TODO: is this specification okay? }; // TODO: prove diff --git a/scripts/build_llvm.sh b/scripts/build_llvm.sh index 1f638fa0..2934fa3b 100755 --- a/scripts/build_llvm.sh +++ b/scripts/build_llvm.sh @@ -20,6 +20,14 @@ build () { export LLVM_COMPILER=clang sed -i'' 's/^CFLAGS=/# CFLAGS=/' build.sh ./build.sh + + + if [ "$2" = blst ]; then + cp ../../proof/bls_operations.c . + cp bindings/*.h . + wllvm -c bls_operations.c + ar rcs libblst.a bls_operations.o + fi extract-bc --bitcode libblst.a ) } diff --git a/spec/BLSGeneric.cry b/spec/BLSGeneric.cry index b6fc8300..5ca0e212 100644 --- a/spec/BLSGeneric.cry +++ b/spec/BLSGeneric.cry @@ -9,7 +9,7 @@ // definitions, and later defines ciphersuites that instantiate those parameters. // // This module defines the specification in terms of the parameters, using a Cryptol -// parameterized module. The instantiations are done in separate Cyytpol files, +// parameterized module. The instantiations are done in separate Crytpol files, // as required by the language. module BLSGeneric where @@ -43,7 +43,8 @@ parameter // H, a hash function, is always HKDF, so not listed here // hash_to_point - type DST_len: # + // TODO: why is this not working? + // type DST_len: # hash_to_point: {msg_len} (Hashable msg_len) => [msg_len][8] -> EC::AffinePoint t_F @@ -64,7 +65,12 @@ parameter pubkey_subgroup_check: EC::AffinePoint t_F' -> Bool signature_subgroup_check: EC::AffinePoint t_F -> Bool -type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + DST_len)) +//type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + DST_len)) +type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + 43)) + +// TODO: Better name. Maybe param should be _pubkey_subgroup_check and this +// should be pubkey_subgroup_check +reexport_pubkey_subgroup_check = pubkey_subgroup_check // 2.3 KeyGen @@ -74,7 +80,9 @@ type constraint Hashable msg_len = (msg_len <= 255, 61 >= width (69 + msg_len + // 2.4 SkToPk -sk_to_pk: [256] -> [pubkey_len] +// TODO: This was 256, but the BLST sk_to_pk spec drops the first bit, so I +// made it 255 to match. Why do the parameter lengths differ? +sk_to_pk: [255] -> [pubkey_len] sk_to_pk sk = point_to_pubkey (EC::mult other_curve sk P) @@ -87,12 +95,15 @@ KeyValidate pk = ret where ret = maybe_cases xP False // xP is None, step 2 (\y -> (~ (EC::is_point_O other_curve y)) // Step 3 - /\ pubkey_subgroup_check y) // Step 4 + /\ reexport_pubkey_subgroup_check y) // Step 4 // 2.6 CoreSign -CoreSign: {msg_len} (Hashable msg_len) => [256] -> [msg_len][8] -> [signature_len] -CoreSign sk message = signature where +/* CoreSign: {msg_len} (Hashable msg_len) => [256] -> [msg_len][8] -> [signature_len] */ +/* CoreSign sk message = signature where */ +// TODO: Same note about dropped first bit... +CoreSign: {msg_len} (Hashable msg_len) => ([255], [msg_len][8]) -> [signature_len] +CoreSign (sk, message) = signature where Q = hash_to_point message R = EC::mult main_curve sk Q signature = point_to_signature R @@ -123,4 +134,4 @@ CoreVerify PK message signature = C2 = pairing (R, P)))) // line 8 // TODO? -CoreAggregateVerify: {n, msg_len} (fin n, Hashable msg_len) => [n][pubkey_len] -> [signature_len] -> [n][msg_len] -> Bool +/* CoreAggregateVerify: {n, msg_len} (fin n, Hashable msg_len) => [n][pubkey_len] -> [signature_len] -> [n][msg_len] -> Bool */ diff --git a/spec/BLSMinimalPublicKeySize.cry b/spec/BLSMinimalPublicKeySize.cry new file mode 100644 index 00000000..494e055e --- /dev/null +++ b/spec/BLSMinimalPublicKeySize.cry @@ -0,0 +1,72 @@ +/* + * Copyright (c) 2020 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +module BLSMinimalPublicKeySize = BLSGeneric where + +// Suite BLS_SIG_BLS12381G2_XMD:SHA-256_SSWU_RO_NUL_, as defined in +// draft-irtf-cfrg-bls-signature-04, Secton 4.2.1 and Appendix A + +import Parameters +import HashToCurveE2 +import Pairing (bls_ate_pairing) +import Serialization +import ShortWeierstrassCurve as EC + +// a pairing-friendly elliptic curve +type t_F = t_Fp_2 // representation type for field of the primary curve (signature) +type t_F' = t_Fp // representation type for field of the secondary curve (pubkey) +type t_G = t_Fp_12 // representation type for field of the pairing result + +type pubkey_len = 48*8 +type signature_len = 96*8 + +main_curve = E' +other_curve = E + +// hash_to_point BLS12381G2_XMD:SHA-256_SSWU_RO_ +// type DST_len = 43 + +DST: [43][8] +DST = "BLS_SIG_BLS12381G2_XMD:SHA-256_SSWU_RO_NUL_" + +hash_to_point hx = hash_to_curve (DST, hx) + +// other primitives "determined by the above parameters" + +P: EC::AffinePoint t_F' // base point +P = BP + +// pairing: (EC::AffinePoint t_F, EC::AffinePoint t_F') -> t_G +pairing (p,q) = bls_ate_pairing q p // Section 2.2 + +// point_to_pubkey: EC::AffinePoint t_F' -> [pubkey_len] +// point_to_pubkey = point_to_octets_E2 // Section 2.2 BUT +// draft-irtf-cfrg-pairing-friendly-curves-07 does not mention +// a function of this name. So: +point_to_pubkey S = join (serialize_E1 S) + +// point_to_signature: EC::AffinePoint t_F -> [signature_len] +//point_to_signature = point_to_octets_E1 // Section 2.2 +point_to_signature S = join (serialize_E2 S) + +// pubkey_to_point: [pubkey_len] -> Maybe (EC::AffinePoint t_F') // can fail +pubkey_to_point S = uncompress_E1 (split S) + +// signature_to_point: [signature_len] -> Maybe (EC::AffinePoint t_F) // can fail + +// signature_to_point: [signature_len] -> Maybe (EC::AffinePoint t_F) // can fail +// signature_to_point = octets_to_point_E1 +signature_to_point S = deserialize_E2 (split S) + +// Here are the unoptimized versions of the subgroup check + +// pubkey_subgroup_check: EC::AffinePoint t_F' -> Bool +pubkey_subgroup_check S = + EC::is_point_O E (EC::mult E r S) + +// signature_subgroup_check: EC::AffinePoint t_F -> Bool +// ... more efficient versions are allowed. +signature_subgroup_check S = + EC::is_point_O E' (EC::mult E' r S) diff --git a/spec/BLSMinimalSignatureSize.cry b/spec/BLSMinimalSignatureSize.cry index a16411f1..6c33fc74 100644 --- a/spec/BLSMinimalSignatureSize.cry +++ b/spec/BLSMinimalSignatureSize.cry @@ -26,12 +26,14 @@ main_curve = E other_curve = E' // hash_to_point BLS12381G1_XMD:SHA-256_SSWU_RO_ -type DST_len = 43 +// type DST_len = 43 -DST: [DST_len][8] +// TODO: Make this match whatever DST string we use (what about null +// terminator?) +DST: [43][8] DST = "BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_" -hash_to_point hx = hash_to_curve (DST, hx) +hash_to_point hx = hash_to_curve (hx, DST) // other primitives "determined by the above parameters" @@ -52,12 +54,15 @@ point_to_pubkey S = join (serialize_E2 S) point_to_signature S = join (serialize_E1 S) // pubkey_to_point: [pubkey_len] -> Maybe (EC::AffinePoint t_F') // can fail -//pubkey_to_point = octets_to_point_E2 // Section 2.2 +// pubkey_len = 768 +// deserialize_E2: [96][8] -> Maybe (EC::AffinePoint t_Fp_2) pubkey_to_point S = deserialize_E2 (split S) // signature_to_point: [signature_len] -> Maybe (EC::AffinePoint t_F) // can fail // signature_to_point = octets_to_point_E1 -signature_to_point S = deserialize_E1 (split S) +// TODO: Was deserialize_E1, but types didn't line up with the expected +// signature length +signature_to_point S = uncompress_E1 (split S) // Here are the unoptimized versions of the subgroup check diff --git a/spec/CoreVerifyPKInG2.cry b/spec/CoreVerifyPKInG2.cry new file mode 100644 index 00000000..086e379c --- /dev/null +++ b/spec/CoreVerifyPKInG2.cry @@ -0,0 +1,10 @@ +// TODO: Belongs in implementation directory +module CoreVerifyPKInG2 where + +import Parameters +import HashToCurveE1 +import Pairing + +core_verify_pk_in_g2 pk sig msg dst = Fp_12.is_equal(c1, c2) where + c1 = bls_ate_pairing (hash_to_curve (msg, dst)) pk + c2 = bls_ate_pairing sig BP' diff --git a/spec/implementation/CoreVerifyPKInG1.cry b/spec/implementation/CoreVerifyPKInG1.cry new file mode 100644 index 00000000..66a620c2 --- /dev/null +++ b/spec/implementation/CoreVerifyPKInG1.cry @@ -0,0 +1,38 @@ +/* + * Copyright (c) 2021 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +module implementation::CoreVerifyPKInG1 where + +import Parameters (Fp_12, t_Fp, t_Fp_2, BP, E') +import ShortWeierstrassCurve (AffinePoint, affinify) +import implementation::PairingImpl (miller_loop_opt) +import implementation::HashToG2 (hash_to_curve_E2_opt_impl) +import implementation::FinalExp (final_exponentiation_impl) +import implementation::PairingImpl (miller_loop_opt_checked) +import ExpandMessage +import Frobenius (fp12_conjugate) +import HashToCurveE2 + +core_verify_pk_in_g1_impl : {msg_len,dst_len,aug_len} + (fin msg_len, fin dst_len, fin aug_len + , Expandable (msg_len+aug_len) dst_len + , dst_len <= 255) => + AffinePoint t_Fp -> AffinePoint t_Fp_2 -> [msg_len][8] -> [dst_len][8] -> [aug_len][8] -> Bool + +core_verify_pk_in_g1_impl pk sig msg dst aug = Fp_12.is_equal(gt, Fp_12.field_unit) where + Q = affinify E' (hash_to_curve_E2_opt_impl (aug#msg, dst)) + gtPQ = miller_loop_opt_checked pk Q + gtSig = fp12_conjugate (miller_loop_opt_checked BP sig) + gt = final_exponentiation_impl (Fp_12.mul (gtSig, gtPQ)) + +/* core_verify_pk_in_g1 : {msg_len,dst_len,aug_len} */ + /* (fin msg_len, fin dst_len, fin aug_len */ + /* , Expandable (msg_len+aug_len) dst_len */ + /* , dst_len <= 255) => */ + /* AffinePoint t_Fp -> AffinePoint t_Fp_2 -> [msg_len][8] -> [dst_len][8] -> [aug_len][8] -> Bool */ + +/* core_verify_pk_in_g1 pk sig msg dst aug = Fp_12.is_equal(c1, c2) where */ + /* c1 = bls_ate_pairing pk (hash_to_curve (aug#msg, dst)) */ + /* c2 = bls_ate_pairing BP sig */ diff --git a/spec/implementation/CoreVerifyPKInG2.cry b/spec/implementation/CoreVerifyPKInG2.cry new file mode 100644 index 00000000..5c7773c7 --- /dev/null +++ b/spec/implementation/CoreVerifyPKInG2.cry @@ -0,0 +1,28 @@ +/* + * Copyright (c) 2021 Galois, Inc. + * SPDX-License-Identifier: Apache-2.0 OR MIT +*/ + +module implementation::CoreVerifyPKInG2 where + +import Parameters (Fp_12, t_Fp, t_Fp_2, BP', E) +import ShortWeierstrassCurve (AffinePoint, affinify) +import implementation::PairingImpl (miller_loop_opt) +import implementation::HashToG1 (hash_to_curve_opt_impl) +import implementation::FinalExp (final_exponentiation_impl) +import implementation::PairingImpl (miller_loop_opt_checked) +import ExpandMessage +import Frobenius (fp12_conjugate) +import HashToCurveE1 + +core_verify_pk_in_g2_impl : {msg_len,dst_len,aug_len} + (fin msg_len, fin dst_len, fin aug_len + , Expandable (msg_len+aug_len) dst_len + , dst_len <= 255) => + AffinePoint t_Fp_2 -> AffinePoint t_Fp -> [msg_len][8] -> [dst_len][8] -> [aug_len][8] -> Bool + +core_verify_pk_in_g2_impl pk sig msg dst aug = Fp_12.is_equal(gt, Fp_12.field_unit) where + Q = affinify E (hash_to_curve_opt_impl (aug#msg, dst)) + gtPQ = miller_loop_opt_checked Q pk + gtSig = fp12_conjugate (miller_loop_opt_checked sig BP') + gt = final_exponentiation_impl (Fp_12.mul (gtSig, gtPQ)) diff --git a/spec/implementation/PairingImpl.cry b/spec/implementation/PairingImpl.cry index 0f65bb10..5666740d 100644 --- a/spec/implementation/PairingImpl.cry +++ b/spec/implementation/PairingImpl.cry @@ -37,9 +37,10 @@ derivation; see below. Again the key is that we can introduce factors that get wiped out (mapped to 1) in the final exponentiation. - (5) A final trick used in the C code is to avoid negating Q, computing with Q itself and then - conjugating the final result. This is OK, because in - Fp_12, conjugation is inversion, and the bilinearity if pairing shows + (5) A final trick used in the C code is to avoid negating Q, computing with + Q itself and then conjugating the final result. This is OK, because for + points in Fp_12 that are in the cyclotomic subgroup, conjugation is + inversion, and the bilinearity of pairing shows [-Q,P] = [Q,P]^{-1} @@ -62,7 +63,7 @@ import implementation::CurveOperation (point_double, point_add_affine, normalize // Step (1) // Note: the layout of Fp_12 over Fp_2 is -// [[a,c,e],[b,d,f]] represents a*w^5 + b*w^4 + c*w^3 + d*w^2 + e*w + f +// [[a,c,e],[b,d,f]] represents a*w^5 + b*w^4 + c*w^3 + d*w^2 + e*w + f /** * Take a point on E/F_p to a point on E'/F_p^12 @@ -211,7 +212,7 @@ line_double_opt (xT,yT,zT) (xP, yP) = ret where yP' = P::Fp_to_Fp_2 yP l0 = Fp_2.sub (mul_by_3 Fp_2 (cubed xT), mul_by_2 Fp_2 (Fp_2.sq yT)) // 3xT^3 - 2yT^2 l1 = Fp_2.neg (mul_by_3 Fp_2 (Fp_2.mul (Fp_2.sq xT, Fp_2.mul (Fp_2.sq zT, xP')))) // -3 xP xT^2 zT^2 - l2 = Fp_2.mul (mul_by_2 Fp_2 (Fp_2.mul (yT, cubed zT)), yP') // 2 yP yT zT^3 + l2 = Fp_2.mul (mul_by_2 Fp_2 (Fp_2.mul (yT, cubed zT)), yP') // 2 yP yT zT^3 ret = fp6_to_fp12_xy00z0 [ mul_by_2 Fp_2 l2 // factor of w^3 , mul_by_2 Fp_2 l1 // factor of w^2 @@ -224,7 +225,7 @@ line_double_opt (xT,yT,zT) (xP, yP) = ret where /* Putting all that together, with the conjugation trick of step 5, gives this function, which we will use as a high-level specification for the C code. */ - + // TODO? This function could take the projective add and double functions as parameters, // since it does not matter what they are so long a they get projectively correct answers.