~/bend-docscommunity

proofs/crypto/secp256k1/pver.bend checks

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

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

21 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/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 ./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 ./pdec.bend as PD
import ./blist.bend as BL
import ./pscal.bend as SQ

Definitions

def aff_x_v source · line 27 · raw

@+one:Nat -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.aff_x(a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.aff_x(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : Nat}

def aff_x_l source · line 32 · raw

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

def vfin source · line 38 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+rr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hrr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, rr) == True{} : Bool} -> @+r:List<&2, Nat> -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), r) == True{} : Bool} -> {Bool.and(Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.is_inf(rr)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.reduce(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.aff_x(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.to_affine(rr))), r)) == Bool.and(Bool.not(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.is_inf(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, rr))), Nat.is_eq(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.aff_x(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.to_affine(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, rr))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r))) : Bool}

R not the point at infinity and x(R) mod n = r

def vrs source · line 48 · 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} -> @+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.verify_rs(q, z, r, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.verify_rs(one, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s)) : Bool}

def ok_red source · line 76 · raw

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

a valid scalar (1 <= x < n) is reduced

def vok source · line 79 · 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} -> @+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} -> @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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.verify_ok(q, z, r, s, Bool.and(Bool.and(a, b), c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.verify_ok(one, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, z), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, s), Bool.and(Bool.and(a, b), c)) : Bool}

def vq source · line 90 · 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(64n, sig) == True{} : Bool} -> @strict: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.verify_q(h, sig, strict, m) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.verify_q(one, h, sig, strict, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.mpv(one, m)) : Bool}

def vlen source · line 115 · raw

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

def verify_v source · line 126 · raw

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

verify (strict = False) and verify_strict (strict = True)