proofs/crypto/secp256k1/bounds.bend checks

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

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

10 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/logic.bend as Lg
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

Definitions

def lt_one source · line 16 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0n, one) == True{} : Bool}

def pos_pos source · line 20 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @k:Nat -> {Nat.is_lt(0n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(k, one)) == True{} : Bool}

def pos_shift source · line 29 · raw

@n:Nat -> @+y:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(n, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.mul(n, 16n), y) : Nat}

2^(16 n) y

def pos16 source · line 39 · raw

@+y:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(16n, y) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, y) : Nat}

2^256 y

def mod256_lt source · line 43 · raw

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

s mod 256 < 2^8, and the low 16 bits of s below 2^16

def lo16_lt source · line 47 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Nat -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.lo16(s), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool}

def carry_limbs source · line 53 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @n:Nat -> @j:Nat -> @xs:List<&2, Nat> -> @+u:Nat -> @+hj:{Nat.is_le(j, n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, j, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(j, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(n, xs, u))) == True{} : Bool}

the first j <= n limbs of a carry pass: exactly j limbs below 2^16

def limbs_lt source · line 73 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @k:Nat -> @ys:List<&2, Nat> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, k, ys) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(ys), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(k, one)) == True{} : Bool}

k limbs below 2^16 have a value below 2^(16 k)

def limbs_take source · line 87 · raw

@+one:Nat -> @n:Nat -> @j:Nat -> @+xs:List<&2, Nat> -> @+hj:{Nat.is_le(j, n) == True{} : Bool} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(n, xs)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, j, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(j, xs)) == True{} : Bool}

the first j limbs of a list whose first n >= j limbs are fine