~/bend-docscommunity

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

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

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 SchnorrPubkey.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> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.schnorr_pubkey(sk) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.pubkey(one, sk) : Maybe<&2, List<&2, U32>>}

BIP-340 x-only public keys, signing and verification

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

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+msg:List<&2, U32> -> @+aux:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.schnorr_sign(sk, msg, aux) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign(one, sk, msg, aux) : Maybe<&2, List<&2, U32>>}

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

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