proofs/crypto/secp256k1/lits.bend checks

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

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

6 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../lib/logic.bend as Lg
import ./consts.bend as K
import ./ineq.bend as I

Definitions

def shk source · line 13 · raw

@+k:Nat -> @+one:Nat -> @+v:Nat -> @+hv:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one) == v : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(1n+k, one) == Nat.add(v, v) : Nat}

def sh10 source · line 19 · raw

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

def lt16 source · line 24 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+w:Nat -> @+hw:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(10n, one) == w : Nat} -> @+hx:{Nat.is_lt(x, Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))), Nat.add(Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w)))), Nat.add(Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))), Nat.add(Nat.add(Nat.add(w, w), Nat.add(w, w)), Nat.add(Nat.add(w, w), Nat.add(w, w))))))) == True{} : Bool} -> {Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool}

a literal below 2^16 is a limb (2^16 is written 64 w with w = 2^10, as doublings: literals past about 2^12 cannot be compared with unary terms)

def ok16 source · line 28 · raw

@+w:Nat -> @n:Nat -> @xs:List<&2, Nat> -> Bool

def lits16_w source · line 35 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+w:Nat -> @+hw:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(10n, one) == w : Nat} -> @n:Nat -> @xs:List<&2, Nat> -> @+h:{ok16(w, n, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool}

def lits16 source · line 49 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @n:Nat -> @xs:List<&2, Nat> -> @+h:{ok16(1024n, n, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool}