~/bend-docscommunity

proofs/crypto/secp256k1/ppub.bend checks

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

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

14 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/bytes.bend as B
import ../../../src/crypto/secp256k1/point.bend as P
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ./bytes.bend as BY
import ./point.bend as PT
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

Definitions

def pk_v source · line 22 · raw

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

def pubpt_v source · line 30 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, d) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.public_point(d)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.g(one)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}

[d] G

def pubpt_r source · line 35 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, d) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.public_point(d)) == True{} : Bool}

def pub_ok source · line 38 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @c:Bool -> @+d:List<&2, Nat> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, d) == True{} : Bool} -> @b:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.public_key_d(c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.secret_if(d, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.public_d(one, c, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), b) : Maybe<&2, List<&2, U32>>}

def pub_len source · line 47 · raw

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

def public_key_v source · line 59 · raw

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

the SEC 1 public key of a secret key