~/bend-docscommunity

proofs/crypto/secp256k1/prec.bend checks

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

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

28 imports
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../spec/crypto/secp256k1/ecdsa.bend as ES
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/ecdsa.bend as E
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ./consts.bend as K
import ./ineq.bend as I
import ./fieldops.bend as FO
import ./scalarops.bend as SO
import ./scalarpow.bend as SP
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./sel.bend as SL
import ./paff.bend as PA
import ./penc.bend as PE
import ./pver.bend as PV
import ./rconst.bend as RC
import ./blist.bend as BL
import ./pscal.bend as SQ
import ./ptwo.bend as TW

Definitions

def pl1 source · line 36 · raw

@+sig:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, sig) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.prefix(32n, sig)) == True{} : Bool}

def pl2 source · line 40 · raw

@+sig:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, sig) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.prefix(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.suffix(32n, sig))) == True{} : Bool}

def rq_b source · line 47 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hq:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, q) == True{} : Bool} -> @b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_q(q, b) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_q_if(one, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q), b) : Maybe<&2, List<&2, U32>>}

def rq_v source · line 54 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+q:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hq:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, q) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_q(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.is_inf(q)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_q(one, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q)) : Maybe<&2, List<&2, U32>>}

def rr source · line 58 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> @m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point> -> @+hm:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpred(one, m) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_r(z, r, s, m) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_r(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, m)) : Maybe<&2, List<&2, U32>>}

def rxg source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> @+id:Nat -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+xv:Nat -> @+hxv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x) == Nat.mod(xv, 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) : Nat} -> @c:Bool -> @+hc:{Nat.is_lt(xv, 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) == c : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_x(z, r, s, id, x, c) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_x_if(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), id, xv, c) : Maybe<&2, List<&2, U32>>}

def r_lt_n source · line 90 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)) == True{} : Bool}

r < n < p

def r_lt_pp source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) == True{} : Bool}

def to_p source · line 96 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_lt(x, 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) == True{} : Bool} -> {Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == True{} : Bool}

def rp_red source · line 99 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, r) == True{} : Bool}

def cn_red source · line 102 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.cn_fe) == True{} : Bool}

def cp_red source · line 106 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.cp_fe) == True{} : Bool}

def x1_r source · line 111 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.rn_fe(r)) == True{} : Bool}

x1 = (r - c_n + c_p) mod p = (r + n) mod p

def x1_v source · line 114 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.rn_fe(r)) == Nat.mod(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one)), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) : Nat}

def lt4 source · line 124 · raw

@c:Nat -> {Nat.is_lt(4n+c, 4n) == False{} : Bool}

def not4 source · line 131 · raw

@+c:Nat -> @+h:{Nat.is_lt(4n+c, 4n) == True{} : Bool} -> Empty

def rfl_b source · line 134 · raw

@+b:Bool -> {b == b : Bool}

def zmul source · line 137 · raw

@+x:Nat -> {Nat.mul(0n, x) == 0n : Nat}

def rc0 source · line 140 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, 0n, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 0n, True{}) : Maybe<&2, List<&2, U32>>}

def rc1 source · line 150 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, 1n, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 1n, True{}) : Maybe<&2, List<&2, U32>>}

def rc2 source · line 160 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, 2n, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 2n, True{}) : Maybe<&2, List<&2, U32>>}

def rc3 source · line 173 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, 3n, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), 3n, True{}) : Maybe<&2, List<&2, U32>>}

def rid source · line 186 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 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} -> @id:Nat -> @+hid:{Nat.is_lt(id, 4n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, id, True{}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), id, True{}) : Maybe<&2, List<&2, U32>>}

def rok source · line 199 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, Nat> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), z) == True{} : Bool} -> @+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} -> @+id:Nat -> @a:Bool -> @b:Bool -> @c:Bool -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r)) == a : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s)) == b : Bool} -> @+hc:{Nat.is_lt(id, 4n) == c : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_ok(z, r, s, id, Bool.and(Bool.and(a, b), c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), id, Bool.and(Bool.and(a, b), c)) : Maybe<&2, List<&2, U32>>}

def rsig source · line 210 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> @+sig:List<&2, U32> -> @+hsig:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, sig) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_sig(h, sig) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_len(one, h, sig, True{}) : Maybe<&2, List<&2, U32>>}

def rlen source · line 232 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+sig:List<&2, U32> -> @a:Bool -> @b:Bool -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == a : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(65n, sig) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.recover_len(h, sig, Bool.and(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.recover_len(one, h, sig, Bool.and(a, b)) : Maybe<&2, List<&2, U32>>}

def recover_v source · line 242 · raw

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

the key recovered from a 32-byte hash and a 65-byte r || s || id