~/bend-docscommunity

proofs/crypto/secp256k1/sel.bend checks

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

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

12 imports
import Base
import ../../../spec/lib/common.bend as C
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/point.bend as P
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./fieldops.bend as FO
import ./bitsv.bend as BV
import ./bitsrel.bend as BR
import ./point.bend as PT

Definitions

def bit01 source · line 16 · raw

@n:Nat -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bit(n), 2n) == True{} : Bool}

Selection (b ? p : q, b in {0, 1}) and small facts for the point proofs.

def sb01 source · line 25 · raw

@i:Nat -> @+off:Nat -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.all01(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsrel.sb(i, off, k)) == True{} : Bool}

def sel0 source · line 32 · raw

@+one:Nat -> @n:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, ys) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.select(0n, xs, ys) == ys : List<&2, Nat>}

def sel1 source · line 56 · raw

@+one:Nat -> @n:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, Nat> -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, ys) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.select(1n, xs, ys) == xs : List<&2, Nat>}

def l16 source · line 81 · raw

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

def rx source · line 84 · 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/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool}

def ry source · line 87 · 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/spec/crypto/secp256k1/field.limbs16(one, 16n, y) == True{} : Bool}

def rz source · line 90 · 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/spec/crypto/secp256k1/field.limbs16(one, 16n, z) == True{} : Bool}

def psel0 source · line 94 · raw

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

b = 0 picks the second point, b = 1 the first

def psel1 source · line 102 · raw

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

def one_lt source · line 110 · raw

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

def lt2 source · line 113 · raw

@c:Nat -> {Nat.is_lt(2n+c, 2n) == False{} : Bool}

def not01 source · line 120 · raw

@+c:Nat -> @+h:{Nat.is_lt(2n+c, 2n) == True{} : Bool} -> Empty

def red_of source · line 123 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+hl:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool} -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.red(one, x) == True{} : Bool}

def sl16 source · line 126 · raw

@+one:Nat -> @+x:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.reduced(one, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one), x) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, x) == True{} : Bool}