proofs/crypto/secp256k1/bitsrel.bend checks

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

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

11 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 ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW
import ./limbs.bend as LV
import ./bytes.bend as BY

Definitions

def sb source · line 19 · raw

@i:Nat -> @+off:Nat -> @+k:Nat -> List<&2, Nat>

bits off + i - 1 down to off of K

def app_nat source · line 24 · raw

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

def div2 source · line 31 · raw

@x:Nat -> {Nat.div(x, 2n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.half(x) : Nat}

def sb_one source · line 42 · raw

@j:Nat -> @+x:Nat -> {sb(j, 1n, x) == sb(j, 0n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.half(x)) : List<&2, Nat>}

offset 1 is offset 0 of the half

def sb_last source · line 50 · raw

@j:Nat -> @+x:Nat -> {sb(1n+j, 0n, x) == List.append(&2, Nat, sb(j, 1n, x), [0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bit(0n, x)]) : List<&2, Nat>}

the last bit comes off the end

def bits_of_sb source · line 57 · raw

@j:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits_of(j, x) == sb(j, 0n, x) : List<&2, Nat>}

def sb_split source · line 70 · raw

@a:Nat -> @+b:Nat -> @+k:Nat -> {sb(Nat.add(a, b), 0n, k) == List.append(&2, Nat, sb(a, b, k), sb(b, 0n, k)) : List<&2, Nat>}

sb(a + b, 0) = sb(a, b) ++ sb(b, 0)

def sb_hi source · line 80 · raw

@i:Nat -> @+x:Nat -> @+r:Nat -> @+f16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(16n, x) == True{} : Bool} -> {sb(i, 16n, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, r))) == sb(i, 0n, r) : List<&2, Nat>}

above 16: the bits of the rest

def bit_lo source · line 92 · raw

@+j:Nat -> @+d:Nat -> @+x:Nat -> @+r:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bit(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(j, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(j, 1n+d), r)))) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bit(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(j, x)) : Nat}

below 16: the bits of the limb (j + 1 + d = 16)

def sh_idx source · line 97 · raw

@+j:Nat -> @+d:Nat -> @+r:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(1n+j, d), r) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(j, 1n+d), r) : Nat}

def sb_lo source · line 101 · raw

@i:Nat -> @+d:Nat -> @+x:Nat -> @+r:Nat -> {sb(i, 0n, Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(i, d), r))) == sb(i, 0n, x) : List<&2, Nat>}

def bits_sb source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @n:Nat -> @xs:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bits(xs) == sb(Nat.mul(n, 16n), 0n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs)) : List<&2, Nat>}

the bits of n limbs below 2^16