proofs/crypto/secp256k1/bitsv.bend checks

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

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

13 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/nat.bend as N
import ../../lib/logic.bend as Lg
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
import ./limbs.bend as LV
import ./ineq.bend as I
import ./reduce.bend as R

Definitions

def hv source · line 20 · raw

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

def hv_app source · line 25 · raw

@+one:Nat -> @xs:List<&2, Nat> -> @+e:Nat -> @+ys:List<&2, Nat> -> {hv(List.append(&2, Nat, xs, ys), one, e) == hv(ys, one, hv(xs, one, e)) : Nat}

def all01 source · line 32 · raw

@bs:List<&2, Nat> -> Bool

def all01_app source · line 37 · raw

@xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> @+hx:{all01(xs) == True{} : Bool} -> @+hy:{all01(ys) == True{} : Bool} -> {all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}

def mod2_lt source · line 44 · raw

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

def bits_of01 source · line 47 · raw

@k:Nat -> @+x:Nat -> {all01(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits_of(k, x)) == True{} : Bool}

def bits01 source · line 54 · raw

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

def two_x source · line 64 · raw

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

d < 2 s gives d / 2 < s

def half_lt source · line 69 · raw

@+d:Nat -> @+s:Nat -> @+h:{Nat.is_lt(d, Nat.double(s)) == True{} : Bool} -> {Nat.is_lt(Nat.div(d, 2n), s) == True{} : Bool}

def bits_of_v source · line 76 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @k:Nat -> @+d:Nat -> @+e:Nat -> @+hd:{Nat.is_lt(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool} -> {hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits_of(k, d), one, e) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, e), Nat.mul(one, d)) : Nat}

the k bits of d < 2^k spell d

def bits_v source · line 112 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @n:Nat -> @xs:List<&2, Nat> -> @+e:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool} -> {hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(xs), one, e) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(n, e), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, xs)) : Nat}

the bits of n limbs below 2^16 spell their value

def cbit source · line 136 · raw

@b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {Nat.add(Nat.sub(1n, b), b) == 1n : Nat}

def cbit_one source · line 146 · raw

@+one:Nat -> @+b:Nat -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)) == one : Nat}

(1 - b) one + b one = one

def arr source · line 152 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+e:Nat -> {Nat.add(Nat.add(Nat.add(a, b), Nat.add(c, d)), e) == Nat.add(Nat.add(Nat.add(a, c), e), Nat.add(b, d)) : Nat}

hv(e1, flipped bits) + hv(e2, bits) + one = 2^length (e1 + e2 + one)

def cb source · line 165 · raw

@+one:Nat -> @bs:List<&2, Nat> -> @+e1:Nat -> @+e2:Nat -> @+hb:{all01(bs) == True{} : Bool} -> {Nat.add(Nat.add(hv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(bs), one, e1), hv(bs, one, e2)), one) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(List.length(&2, Nat, bs), Nat.add(Nat.add(e1, e2), one)) : Nat}

def sub1_lt source · line 209 · raw

@b:Nat -> {Nat.is_lt(Nat.sub(1n, b), 2n) == True{} : Bool}

def cbits01 source · line 217 · raw

@bs:List<&2, Nat> -> {all01(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.cbits(bs)) == True{} : Bool}