proofs/crypto/secp256k1/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 24 lines · 1 definition

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1.bend as K
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws.bend as Laws
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ppub.bend as PP
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend as PE
7
8# Gate for src/crypto/secp256k1.bend, keys and addresses:
9# `bend proofs/crypto/secp256k1/proof.bend`. The other clauses of laws.bend
10# are proved in the roots proof_sign.bend, proof_verify.bend,
11# proof_recover.bend and proof_schnorr.bend (each checks alone; together
12# they check every clause).
13
14def Laws.PublicKey.correct(one, h1, sk, c):
15  PP.public_key_v(one, h1, sk, c)
16
17def gk(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>) -> {K.generate_keypair(seed) == K.keypair_of(seed, ES.public_key(one, seed, True{})) : Maybe<&2, K.Keypair>}:
18  Equal.cong(Maybe<&2, List<&2, U32>>, Maybe<&2, K.Keypair>, m => K.keypair_of(seed, m), K.public_key(seed, True{}), ES.public_key(one, seed, True{}), PP.public_key_v(one, h1, seed, True{}))
19
20def Laws.GenerateKeypair.correct(one, h1, seed):
21  gk(one, h1, seed)
22
23def Laws.EthAddress.correct(pk):
24  PE.eth_address_v(pk)