~/bend-docscommunity

proofs/crypto/secp256k1/ptwo.bend checks

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

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

8 imports
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/point.bend as P
import ./point.bend as PT
import ./sel.bend as SL
import ./pmul.bend as PM
import ./paff.bend as PA

Definitions

def two_r source · line 14 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+u1:List<&2, Nat> -> @+hu1:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), u1) == True{} : Bool} -> @+u2:List<&2, Nat> -> @+hu2:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), u2) == True{} : Bool} -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hpr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pr) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(u1, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.g), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(u2, pr))) == True{} : Bool}

[u1] G + [u2] R

def two_v source · line 17 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+u1:List<&2, Nat> -> @+hu1:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), u1) == True{} : Bool} -> @+u2:List<&2, Nat> -> @+hu2:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), u2) == True{} : Bool} -> @+pr:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hpr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pr) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(u1, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.g), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(u2, pr))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.padd(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, u1), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.g(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, u2), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pr))) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}