~/bend-docscommunity

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

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

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 Sign.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> -> @+h:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.sign_compact(sk, h) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign(one, sk, h) : Maybe<&2, List<&2, U32>>}

ECDSA signing: RFC 6979 nonce, low s, recovery id; r || s || v