~/bend-docscommunity

proofs/crypto/secp256k1/psign.bend timeout

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

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

26 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/logic.bend as Lg
import ../../../spec/crypto/hmac.bend as HMS
import ../mac/hmac.bend as MH
import ./limbs.bend as LV
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 ./pmul.bend as PM
import ./paff.bend as PA
import ./penc.bend as PE
import ./pver.bend as PV
import ./blist.bend as BL
import ./pscal.bend as SQ

Definitions

def sigb source · line 34 · raw

@sig:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Signature -> List<&2, U32>

def msig source · line 38 · raw

@m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Signature> -> Maybe<&2, List<&2, U32>>

def matt source · line 43 · raw

@a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Attempt -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt

def dr source · line 48 · raw

@g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Drbg -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Drbg

def tbv source · line 54 · 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 id_v source · line 59 · raw

@lb:Bool -> @hb:Bool -> @q:Nat -> @+hq:{Nat.is_lt(q, 2n) == True{} : Bool} -> {Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(Bool.not(lb)), 2n), Nat.sub(Nat.add(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(hb)), Nat.mul(Nat.mul(q, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(hb)), 2n))) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ge2(lb), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.flip(hb, q)) : Nat}

def sel_v source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @hb:Bool -> @+s0:List<&2, Nat> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), s0) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.to_be(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(hb), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(s0), s0)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.low(hb, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s0))) : List<&2, U32>}

def bad_v source · line 91 · raw

@bad:Bool -> @+sig:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Signature -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.finish_if(bad, sig)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.finish_if(bad, sigb(sig)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

def s0_r source · line 98 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k) == True{} : Bool} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv(k), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add(z, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(x), d)))) == True{} : Bool}

def s0_v source · line 102 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k) == True{} : Bool} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.inv(k), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.add(z, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(x), d)))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.mmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.minv(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.madd(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.mmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d)))) : Nat}

def fin_g source · line 113 · 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} -> @+s0:List<&2, Nat> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), s0) == True{} : Bool} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+rv:Nat -> @+hrv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r) == rv : Nat} -> @+sv:Nat -> @+hsv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s0) == sv : Nat} -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.finish_if(Bool.or(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_zero(r), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_zero(s0)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Signature{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.to_be(r), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.to_be(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.select(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_high(s0)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.neg(s0), s0)), U32.from_nat(Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.lt_n(x))), 2n), Nat.sub(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.parity(y), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_high(s0))), Nat.mul(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.parity(y), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.b2n(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.is_high(s0))), 2n))))})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.finish_if(Bool.or(Nat.is_eq(rv, 0n), Nat.is_eq(sv, 0n)), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(32n, rv), List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.i2osp(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.low(Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), Nat.double(sv)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), sv)), [U32.from_nat(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.ge2(Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.flip(Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), Nat.double(sv)), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), 2n))))]))) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

the end of signing on scalars r, s0 of values rv, sv

def fin_v source · line 133 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k) == True{} : Bool} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+y:List<&2, Nat> -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.finish(z, d, k, x, y)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.finish(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SAffine{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y)}) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

def aff_fin source · line 139 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), k) == True{} : Bool} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.attempt_aff(z, d, k, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.finish(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

def aok source · line 144 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, k) == True{} : Bool} -> @b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k)) == b : Bool} -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.attempt_ok(z, d, k, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.attempt_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, k), b) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

def att_v source · line 156 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+v:List<&2, U32> -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, v) == True{} : Bool} -> {matt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.attempt(z, d, v)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.attempt(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), v) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Attempt}

def hm source · line 164 · raw

@k:List<&2, U32> -> @+m:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.hmac(k, m) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hmac(k, m) : List<&2, U32>}

def hlen source · line 171 · raw

@k:List<&2, U32> -> @+m:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.hmac(k, m)) == True{} : Bool}

def sl source · line 182 · raw

@fuel:Nat -> @+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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @+k:List<&2, U32> -> @+v:List<&2, U32> -> @att:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Attempt -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_loop(fuel, z, d, k, v, att)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_loop(fuel, one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), k, v, matt(att)) : Maybe<&2, List<&2, U32>>}

def step_v source · line 203 · raw

@+k:List<&2, U32> -> @+v:List<&2, U32> -> @+tag:U32 -> @+seed:List<&2, U32> -> {dr(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.drbg_step(k, v, tag, seed)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.update(k, v, tag, seed) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Drbg}

def second_v source · line 209 · raw

@d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Drbg -> @+seed:List<&2, U32> -> {dr(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.drbg_second(d, seed)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.update2(dr(d), seed) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Drbg}

def init_v source · line 214 · raw

@+seed:List<&2, U32> -> {dr(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.drbg_init(seed)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.drbg_init(seed) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.Drbg}

def drbg_sign source · line 219 · 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} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> @g:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.Drbg -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_drbg(z, d, g)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_drbg(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), dr(g)) : Maybe<&2, List<&2, U32>>}

def sd source · line 229 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), d) == True{} : Bool} -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_d(h, Some{d})) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_d(one, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), True{}) : Maybe<&2, List<&2, U32>>}

def sk3 source · line 238 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> @+d:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, d) == True{} : Bool} -> @c:Bool -> @+hc:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d)) == c : Bool} -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_d(h, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.secret_if(d, c))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_d(one, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), c) : Maybe<&2, List<&2, U32>>}

def sk2 source · line 245 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == True{} : Bool} -> @b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, sk) == b : Bool} -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_d(h, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.secret_if(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk), Bool.and(b, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.scalar_ok(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.of_be(sk)))))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_d(one, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), Bool.and(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk)))) : Maybe<&2, List<&2, U32>>}

def sh source · line 255 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+sk:List<&2, U32> -> @+h:List<&2, U32> -> @a:Bool -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.has_len(32n, h) == a : Bool} -> {msig(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.sign_h(sk, h, a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.sign_d(one, h, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk), Bool.and(a, Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.length_is(32n, sk), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.scalar_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.os2ip(sk))))) : Maybe<&2, List<&2, U32>>}

def sign_v source · line 264 · raw

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

the signature of a 32-byte hash under a 32-byte secret key