~/bend-docscommunity

proofs/crypto/secp256k1/pmul.bend checks

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

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

13 imports
import Base
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../spec/crypto/secp256k1/curve.bend as CV
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../../src/crypto/secp256k1/point.bend as P
import ../../lib/logic.bend as Lg
import ./limbs.bend as LV
import ./fieldops.bend as FO
import ./bitsv.bend as BV
import ./bitsrel.bend as BR
import ./point.bend as PT
import ./sel.bend as SL

Definitions

def go_sb source · line 22 · raw

@i:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bits_go(i, k) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsrel.sb(i, 0n, k) : List<&2, Nat>}

def bits_is source · line 29 · raw

@+i:Nat -> @k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bits(i, k) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bits_go(i, k) : List<&2, Nat>}

def lbits source · line 37 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ks:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, ks) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(ks) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bits(256n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, ks)) : List<&2, Nat>}

the bits of a scalar's limbs are the specification's bits of its value

def pinf_r source · line 46 · raw

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

def pinf_v source · line 49 · raw

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

def step_r source · line 57 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @b:Nat -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, d) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.step(b, pp, d)) == True{} : Bool}

def step_v source · line 68 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @b:Nat -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+d:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, d) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.step(b, pp, d)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.step(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pp), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, d)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}

def mul_go_r source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @bs:List<&2, Nat> -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul_go(bs, pp, r)) == True{} : Bool}

def mul_go_v source · line 88 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @bs:List<&2, Nat> -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+r:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hbs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(bs) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, r) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul_go(bs, pp, r)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.lmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), bs, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pp), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, r)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}

def lbits01 source · line 105 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ks:List<&2, Nat> -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, ks) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(ks)) == True{} : Bool}

the bits of a scalar are bits

def mul_r source · line 109 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ks:List<&2, Nat> -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, ks) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(ks, pp)) == True{} : Bool}

def mul_v source · line 112 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+ks:List<&2, Nat> -> @+pp:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+hk:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, ks) == True{} : Bool} -> @+hp:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pred(one, pp) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.mul(ks, pp)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, ks), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, pp)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}