~/bend-docscommunity

proofs/crypto/secp256k1/pschn.bend timeout

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

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/pschn.src; edit the .src

28 imports
import Base
import ../../../spec/crypto/sha.bend as FIPS
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/schnorr.bend as SS
import ../../../src/crypto/sha/sha256.bend as SHA
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/scalar.bend as S
import ../../../src/crypto/secp256k1/bytes.bend as B
import ../../../src/crypto/secp256k1/point.bend as P
import ../../../src/crypto/secp256k1/schnorr.bend as SC
import ../../lib/logic.bend as Lg
import ../sha/laws.bend as SHL
import ../sha/correctness.bend as SHC
import ./limbs.bend as LV
import ./ineq.bend as I
import ./scalarops.bend as SO
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./sel.bend as SL
import ./pmul.bend as PM
import ./paff.bend as PA
import ./penc.bend as PE
import ./blist.bend as BL
import ./pscal.bend as SQ
import ./ptwo.bend as TW

Definitions

def fips_len source · line 37 · raw

@+bytes:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha.sha256_bytes(bytes)) == 32n : Nat}

def tbv source · line 40 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.to_be(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : List<&2, U32>}

def xor_v source · line 45 · raw

@xs:List<&2, U32> -> @ys:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.xor_bytes(xs, ys) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.xor_bytes(xs, ys) : List<&2, U32>}

def tagged_v source · line 54 · raw

@+tag:List<&2, U32> -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tagged(tag, x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tagged(tag, x) : List<&2, U32>}

def tagged_len source · line 60 · raw

@+tag:List<&2, U32> -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tagged(tag, x)) == True{} : Bool}

def th_v source · line 66 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:List<&2, U32> -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tagged(tag, x)))) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tagged(tag, x)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)) : Nat}

int(hash) mod n

def th_r source · line 70 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+tag:List<&2, U32> -> @+x:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tagged(tag, x)))) == True{} : Bool}

def ev_q source · line 76 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @q:Nat -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(x), x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.even_b(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), q, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : Nat}

def ev_qr source · line 87 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @q:Nat -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> @+hq:{Nat.is_lt(q, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(x), x)) == True{} : Bool}

def even_v source · line 98 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+y:List<&2, Nat> -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.is_odd(y), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(x), x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.even(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : Nat}

def even_r source · line 102 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+y:List<&2, Nat> -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.is_odd(y), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(x), x)) == True{} : Bool}

def va source · line 108 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, r) == True{} : Bool} -> @+inf:Bool -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_aff(r, inf, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.check_r(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), inf, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : Bool}

def vr source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, r) == True{} : Bool} -> @+rr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hrr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, rr) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_r(r, rr) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.check_r(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.is_inf(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, rr)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.to_affine(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, rr))) : Bool}

def vrs source · line 121 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, r) == True{} : Bool} -> @+s:List<&2, Nat> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), s) == True{} : Bool} -> @+e:List<&2, Nat> -> @+he:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), e) == True{} : Bool} -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_r(r, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(s, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.g), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(e), pp))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.verify_rs(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, e), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pp)) : Bool}

def tc source · line 131 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tag_challenge == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tag_challenge : List<&2, U32>}

def ta source · line 134 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tag_aux == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tag_aux : List<&2, U32>}

def tn source · line 137 · raw

{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.tag_nonce == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.tag_nonce : List<&2, U32>}

def red_n source · line 140 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @+h:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool}

def vok source · line 143 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hlr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, r) == True{} : Bool} -> @+s:List<&2, Nat> -> @+hls:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, s) == True{} : Bool} -> @+e:List<&2, Nat> -> @+he:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), e) == True{} : Bool} -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> @a:Bool -> @b:Bool -> @+ha:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == a : Bool} -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_ok(r, s, e, pp, Bool.and(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.verify_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, e), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pp), Bool.and(a, b)) : Bool}

def vp source · line 152 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pk:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> @+hsig:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, sig) == True{} : Bool} -> @mp:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point> -> @+hmp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, mp) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_p(pk, m, sig, mp) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.verify_p(one, pk, m, sig, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, mp)) : Bool}

def lxb source · line 174 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @b:Bool -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.lift_if(x, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.lift_if(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), b) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def lxr source · line 181 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @b:Bool -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.lift_if(x, b)) == True{} : Bool}

def lx source · line 188 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.lift_x(x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.lift_x(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def lx_r source · line 192 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.lift_x(x)) == True{} : Bool}

def vlen source · line 196 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pk:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> @a:Bool -> @b:Bool -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, pk) == a : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(64n, sig) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.verify_len(pk, m, sig, Bool.and(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.verify_len(one, pk, m, sig, Bool.and(a, b)) : Bool}

def verify_v source · line 209 · raw

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

BIP-340 verification

def sok source · line 216 · raw

@+sig:List<&2, U32> -> @b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_ok(sig, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_if(sig, b) : Maybe<&2, List<&2, U32>>}

def sfin source · line 223 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+sig:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_fin(pb, m, sig) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_fin(one, pb, m, sig) : Maybe<&2, List<&2, U32>>}

def ax_l source · line 227 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine{x, y}) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool}

def sk_v source · line 230 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:List<&2, Nat> -> @+hk0:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k0) == True{} : Bool} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_k(d, pb, m, k0, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_r(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), pb, m, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k0), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : Maybe<&2, List<&2, U32>>}

def snz source · line 249 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:List<&2, Nat> -> @+hk0:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k0) == True{} : Bool} -> @z:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_nz(d, pb, m, k0, Bool.not(z)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_kz(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), pb, m, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k0), z) : Maybe<&2, List<&2, U32>>}

def sk2 source · line 261 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+pb:List<&2, U32> -> @+m:List<&2, U32> -> @+k0:List<&2, Nat> -> @+hk0:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k0) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_nz(d, pb, m, k0, Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_zero(k0))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_k(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), pb, m, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k0)) : Maybe<&2, List<&2, U32>>}

def spk source · line 265 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d0:List<&2, Nat> -> @+hd0:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d0) == True{} : Bool} -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_p(d0, m, aux, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_p(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d0), m, aux, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : Maybe<&2, List<&2, U32>>}

def s3 source · line 288 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, sk) == True{} : Bool} -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @c:Bool -> @+hc:{Bool.and(Bool.not(Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0n)), Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one))) == c : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_d(m, aux, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.secret_if(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk), c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_ok(one, sk, m, aux, c) : Maybe<&2, List<&2, U32>>}

def s2 source · line 305 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, sk) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_d(m, aux, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.secret_if(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk), Bool.and(b, Bool.and(Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_zero(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk))), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.lt_n(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk)))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_ok(one, sk, m, aux, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0n)), Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one))))) : Maybe<&2, List<&2, U32>>}

def s1 source · line 316 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+m:List<&2, U32> -> @+aux:List<&2, U32> -> @a:Bool -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, aux) == a : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.sign_len(sk, m, aux, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.sign_ok(one, sk, m, aux, Bool.and(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.secret_ok(one, sk))) : Maybe<&2, List<&2, U32>>}

def sign_v source · line 325 · raw

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

BIP-340 signing

def paff source · line 331 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.pubkey_aff(a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.pub_of(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : List<&2, U32>}

def pk3 source · line 336 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, sk) == True{} : Bool} -> @c:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.pubkey_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.secret_if(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk), c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.pubkey_ok(one, sk, c) : Maybe<&2, List<&2, U32>>}

def pk2 source · line 351 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, sk) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.pubkey_d(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.secret_if(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk), Bool.and(b, Bool.and(Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_zero(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk))), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.lt_n(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk)))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.pubkey_ok(one, sk, Bool.and(b, Bool.and(Bool.not(Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0n)), Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one))))) : Maybe<&2, List<&2, U32>>}

def pubkey_v source · line 363 · 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>>}

the x-only public key of a secret key