proofs/crypto/secp256k1/limbs.bend checks

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

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

8 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR

Definitions

def ev source · line 18 · raw

@xs:List<&2, Nat> -> Nat

def pos source · line 24 · raw

@n:Nat -> @+y:Nat -> Nat

y at limb position n: y 2^(16 n)

def b8 source · line 31 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one) == 256n : Nat}

256 as a shift of one (the checker expands 2^8 in 256 steps, well within its depth)

def m256 source · line 35 · raw

@+y:Nat -> {Nat.mul(y, 256n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, y) : Nat}

def mul_one_l source · line 39 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {Nat.mul(one, x) == x : Nat}

def ev_value source · line 43 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, xs) == ev(xs) : Nat}

def add_v source · line 54 · raw

@xs:List<&2, Nat> -> @ys:List<&2, Nat> -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.add(xs, ys)) == Nat.add(ev(xs), ev(ys)) : Nat}

def scal_v source · line 76 · raw

@+a:Nat -> @ys:List<&2, Nat> -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.scal(a, ys)) == Nat.mul(ev(ys), a) : Nat}

def conv_v source · line 92 · raw

@xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.conv(xs, ys)) == Nat.mul(ev(xs), ev(ys)) : Nat}

def pos_add source · line 110 · raw

@n:Nat -> @+x:Nat -> @+y:Nat -> {pos(n, Nat.add(x, y)) == Nat.add(pos(n, x), pos(n, y)) : Nat}

def pos_zero source · line 119 · raw

@n:Nat -> {pos(n, 0n) == 0n : Nat}

def pos_mul source · line 128 · raw

@n:Nat -> @+x:Nat -> @+y:Nat -> {pos(n, Nat.mul(x, y)) == Nat.mul(pos(n, x), y) : Nat}

def take_drop_v source · line 138 · raw

@n:Nat -> @xs:List<&2, Nat> -> {ev(xs) == Nat.add(ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(n, xs)), pos(n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(n, xs)))) : Nat}

ev(xs) = ev(take n xs) + 2^(16 n) ev(drop n xs)

def hd_tl_v source · line 159 · raw

@xs:List<&2, Nat> -> {ev(xs) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.hd0(xs), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.tl(xs)))) : Nat}

def lohi source · line 168 · raw

@+s:Nat -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.lo16(s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.hi16(s))) == s : Nat}

def horner_v source · line 183 · raw

@xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.horner(xs) == ev(xs) : Nat}

def carry_v source · line 196 · raw

@n:Nat -> @xs:List<&2, Nat> -> @+u:Nat -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(n, xs, u)) == Nat.add(u, ev(xs)) : Nat}

a carry pass keeps the value: the carry in plus the limbs