~/bend-docscommunity

proofs/crypto/secp256k1/paff.bend checks

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

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

12 imports
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/point.bend as P
import ../../lib/logic.bend as Lg
import ./fieldops.bend as FO
import ./fieldpow.bend as FP
import ./fwrap.bend as FW
import ./point.bend as PT
import ./sel.bend as PM
import ./lits.bend as LT

Definitions

def av source · line 18 · raw

@+one:Nat -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SAffine

def ared source · line 22 · raw

@+one:Nat -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> Bool

def red3 source · line 26 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+z:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point{x, y, z}) == True{} : Bool} -> {Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x), Bool.and(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, z))) == True{} : Bool}

def rx source · line 29 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+z:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point{x, y, z}) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool}

def ry source · line 32 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+z:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point{x, y, z}) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool}

def rz source · line 35 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+z:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point{x, y, z}) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, z) == True{} : Bool}

def aff_v source · line 39 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, a) == True{} : Bool} -> {av(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.to_affine(a)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.to_affine(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, a)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SAffine}

(X / Z, Y / Z)

def aff_r source · line 51 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, a) == True{} : Bool} -> {ared(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.to_affine(a)) == True{} : Bool}

def is_inf_v source · line 60 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.is_inf(a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.is_inf(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, a)) : Bool}

def gx_l source · line 67 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.gx) == True{} : Bool}

def gy_l source · line 70 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.gy) == True{} : Bool}

def lt_p_red source · line 73 · raw

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

def g_r source · line 77 · raw

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

def g_v source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.g) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.g(one) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}