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

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

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 Verify.correct openits proof in laws_crypto.bend does not pass the checker (fails)source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pk:List<&2, U32> -> @+h:List<&2, U32> -> @+sig:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.verify(pk, h, sig) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.verify(one, pk, h, sig, False{}) : Bool}

ECDSA verification (SEC 1 4.1.4), high s accepted

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

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pk:List<&2, U32> -> @+h:List<&2, U32> -> @+sig:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.verify_strict(pk, h, sig) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.verify(one, pk, h, sig, True{}) : Bool}

the same with high s rejected