1	import Base
2	import ../../../src/crypto/secp256k1.bend as K
3	import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
4	import ./laws.bend as Laws
5	import ./ppub.bend as PP
6	import ./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	
14	def Laws.PublicKey.correct(one, h1, sk, c):
15	  PP.public_key_v(one, h1, sk, c)
16	
17	def 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	
20	def Laws.GenerateKeypair.correct(one, h1, seed):
21	  gk(one, h1, seed)
22	
23	def Laws.EthAddress.correct(pk):
24	  PE.eth_address_v(pk)