proofs/crypto/secp256k1/laws.bend open laws/TODOs

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws.bend as Laws

4 imports

import Base
import ../../../src/crypto/secp256k1.bend as K
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
import ../../../spec/crypto/secp256k1/schnorr.bend as SS

Laws

law PublicKey.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @c:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.public_key(sk, c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.public_key(one, sk, c) : Maybe<&2, List<&2, U32>>}

the SEC 1 public key (33 bytes compressed, 65 uncompressed) of [d] G

law GenerateKeypair.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 29 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+seed:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.generate_keypair(seed) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.keypair_of(seed, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.public_key(one, seed, True{})) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.Keypair>}

a key pair from a 32-byte seed: the seed and its compressed public key

law EthAddress.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 36 · raw

@+pk:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.eth_address(pk) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.eth_address(pk) : Maybe<&2, List<&2, U32>>}

the Ethereum address of an uncompressed public key