~/bend-docscommunity

proofs/crypto/secp256k1/penc.bend checks

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

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

17 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/bytes.bend as B
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 ./fieldpow.bend as FP
import ./fwrap.bend as FW
import ./bytes.bend as BY
import ./point.bend as PT
import ./sel.bend as PM
import ./paff.bend as PA
import ../../math/natural/arith.bend as NR

Definitions

def mpv source · line 24 · raw

@+one:Nat -> @m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point> -> Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>

def mpred source · line 29 · raw

@+one:Nat -> @m:Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point> -> Bool

def enc_c_v source · line 36 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.enc_c(a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.enc_c(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : List<&2, U32>}

def enc_u_v source · line 45 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Affine -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.ared(one, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.enc_u(a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.enc_u(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.av(one, a)) : List<&2, U32>}

def encode_compressed_v source · line 56 · 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.encode_compressed(q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.encode_compressed(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q)) : List<&2, U32>}

def encode_uncompressed_v source · line 60 · 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.encode_uncompressed(q) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.encode_uncompressed(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.pv(one, q)) : List<&2, U32>}

def seven_lt source · line 66 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(7n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == True{} : Bool}

def rhs_r source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.rhs(x)) == True{} : Bool}

def rhs_v source · line 74 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.rhs(x)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.rhs(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)) : Nat}

def on_curve_v source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.on_curve(x, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.on_curve(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y)) : Bool}

def one_v source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.one) == 1n : Nat}

def one_r source · line 96 · raw

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

def dif_v source · line 99 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @ok:Bool -> {mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decompress_if(x, y, ok)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decompress_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), ok) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def dif_r source · line 107 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> @ok:Bool -> {mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decompress_if(x, y, ok)) == True{} : Bool}

def mod2_lt source · line 114 · raw

@+v:Nat -> {Nat.is_lt(Nat.mod(v, 2n), 2n) == True{} : Bool}

def pick_v source · line 118 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @q:Nat -> @par:Nat -> @+y:List<&2, Nat> -> @+hq:{Nat.is_lt(q, 2n) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.select(Nat.sub(Nat.add(q, par), Nat.mul(Nat.mul(q, par), 2n)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.neg(y), y)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pick_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), Nat.is_eq(q, par)) : Nat}

y or p - y by the parities q and par (both 0 or 1)

def pick_r source · line 137 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @q:Nat -> @par:Nat -> @+y:List<&2, Nat> -> @+hq:{Nat.is_lt(q, 2n) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.select(Nat.sub(Nat.add(q, par), Nat.mul(Nat.mul(q, par), 2n)), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.neg(y), y)) == True{} : Bool}

def lift_v source · line 156 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+y:List<&2, Nat> -> @+par:Nat -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.lift_y(y, par)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pick_parity(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), par) : Nat}

def lift_r source · line 161 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+y:List<&2, Nat> -> @+par:Nat -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.lift_y(y, par)) == True{} : Bool}

def dy source · line 166 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+r:List<&2, Nat> -> @+y:List<&2, Nat> -> @+par:Nat -> @+hr:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, r) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, y) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> {mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decompress_if(x, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.lift_y(y, par), 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.mul(y, y), r))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decompress_if(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.pick_parity(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), par), Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.mmul(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, y)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, r))) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def decompress_v source · line 173 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+par:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> {mpv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decompress(x, par)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.decompress(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), par) : Maybe<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint>}

def decompress_r source · line 185 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+par:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool} -> @+hp:{Nat.is_lt(par, 2n) == True{} : Bool} -> {mpred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.decompress(x, par)) == True{} : Bool}