~/bend-docscommunity

proofs/crypto/secp256k1/point.bend checks

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

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

7 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

Definitions

def pr source · line 15 · raw

@+one:Nat -> Nat

def red source · line 18 · raw

@+one:Nat -> @+x:List<&2, Nat> -> Bool

def vals source · line 21 · raw

@+one:Nat -> @rs:List<&2, List<&2, Nat>> -> List<&2, Nat>

def allred source · line 26 · raw

@+one:Nat -> @rs:List<&2, List<&2, Nat>> -> Bool

def cop source · line 31 · raw

@op:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SOp

def cprog source · line 37 · raw

@ops:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SOp>

def zero_r source · line 44 · raw

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

def zero_v source · line 47 · raw

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

def nth_r source · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @i:Nat -> @rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.nth(i, rs)) == True{} : Bool}

def nth_v source · line 61 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @i:Nat -> @rs:List<&2, List<&2, Nat>> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.nth(i, rs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.nth(i, vals(one, rs)) : Nat}

def exec_r source · line 72 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @op:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {red(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.exec(op, rs)) == True{} : Bool}

def exec_v source · line 81 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @op:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.exec(op, rs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.exec(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), cop(op), vals(one, rs)) : Nat}

def vals_app source · line 99 · raw

@+one:Nat -> @rs:List<&2, List<&2, Nat>> -> @+x:List<&2, Nat> -> {vals(one, List.append(&2, List<&2, Nat>, rs, [x])) == List.append(&2, Nat, vals(one, rs), [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x)]) : List<&2, Nat>}

def allred_app source · line 106 · raw

@+one:Nat -> @rs:List<&2, List<&2, Nat>> -> @+x:List<&2, Nat> -> @+h:{allred(one, rs) == True{} : Bool} -> @+hx:{red(one, x) == True{} : Bool} -> {allred(one, List.append(&2, List<&2, Nat>, rs, [x])) == True{} : Bool}

def run_go_r source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {allred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run_go(prog, rs)) == True{} : Bool}

def run_go_v source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {vals(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run_go(prog, rs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.run_go(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}

def run_is source · line 133 · raw

@prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> @rs:List<&2, List<&2, Nat>> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run(prog, rs) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run_go(prog, rs) : List<&2, List<&2, Nat>>}

run looks at its first register first

def srun_is source · line 142 · raw

@+p:Nat -> @prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SOp> -> @rs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.run(p, prog, rs) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.run_go(p, prog, rs) : List<&2, Nat>}

def run_r source · line 151 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {allred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run(prog, rs)) == True{} : Bool}

def run_v source · line 155 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+prog:List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Op> -> @+rs:List<&2, List<&2, Nat>> -> @+h:{allred(one, rs) == True{} : Bool} -> {vals(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.run(prog, rs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.run(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), cprog(prog), vals(one, rs)) : List<&2, Nat>}

def pv source · line 162 · raw

@+one:Nat -> @p:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint

def pred source · line 166 · raw

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

def b3_r source · line 170 · raw

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

def b3_v source · line 173 · raw

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

def add_prog_eq source · line 176 · raw

{cprog(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.add_prog) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.add_prog : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SOp>}

def dbl_prog_eq source · line 179 · raw

{cprog(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.dbl_prog) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.dbl_prog : List<&2, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SOp>}

def regs7 source · line 182 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x1:List<&2, Nat> -> @+y1:List<&2, Nat> -> @+z1:List<&2, Nat> -> @+x2:List<&2, Nat> -> @+y2:List<&2, Nat> -> @+z2:List<&2, Nat> -> @+h:{Bool.and(red(one, x1), Bool.and(red(one, y1), red(one, z1))) == True{} : Bool} -> @+g:{Bool.and(red(one, x2), Bool.and(red(one, y2), red(one, z2))) == True{} : Bool} -> {allred(one, [x1, y1, z1, x2, y2, z2, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.b3]) == True{} : Bool}

def vals7 source · line 192 · raw

@+one:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+c:List<&2, Nat> -> @+d:List<&2, Nat> -> @+e:List<&2, Nat> -> @+f:List<&2, Nat> -> @+g:List<&2, Nat> -> {vals(one, [a, b, c, d, e, f, g]) == [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, b), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, e), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, f), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, g)] : List<&2, Nat>}

def padd_v source · line 195 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @a:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @b:0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point -> @+ha:{pred(one, a) == True{} : Bool} -> @+hb:{pred(one, b) == True{} : Bool} -> {pv(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.add(a, b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.padd(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one), pv(one, a), pv(one, b)) : 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.SPoint}

def regs4 source · line 216 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:List<&2, Nat> -> @+y:List<&2, Nat> -> @+z:List<&2, Nat> -> @+h:{Bool.and(red(one, x), Bool.and(red(one, y), red(one, z))) == True{} : Bool} -> {allred(one, [x, y, z, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.b3]) == True{} : Bool}

def vals4 source · line 223 · raw

@+one:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+c:List<&2, Nat> -> @+d:List<&2, Nat> -> {vals(one, [a, b, c, d]) == [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, b), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, d)] : List<&2, Nat>}

def pdbl_v source · line 226 · raw

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

def pr3 source · line 248 · raw

@+one:Nat -> @+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+c:List<&2, Nat> -> @+ha:{red(one, a) == True{} : Bool} -> @+hb:{red(one, b) == True{} : Bool} -> @+hc:{red(one, c) == True{} : Bool} -> {pred(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.Point{a, b, c}) == True{} : Bool}

the results are reduced

def padd_r source · line 251 · raw

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

def pdbl_r source · line 258 · raw

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