law GenerateKeypair.correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/laws.bend:28

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES

28# a key pair from a 32-byte seed: the seed and its compressed public key
29law GenerateKeypair.correct:
30  for +one: Nat
31  for +h1: {one == 1n : Nat}
32  for +seed: List<&2, U32>
33  {K.generate_keypair(seed) == K.keypair_of(seed, ES.public_key(one, seed, True{})) : Maybe<&2, K.Keypair>}