~/bend-docscommunity

proofs/crypto/secp256k1/consts.bend checks

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

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

12 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/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW
import ./semiring.bend as SR
import ./limbs.bend as LV
import ./ineq.bend as I
import ./bounds.bend as B

Definitions

def T source · line 20 · raw

@+one:Nat -> Nat

def shift_twice source · line 25 · raw

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

def shift_more source · line 29 · raw

@d:Nat -> @+k:Nat -> @+x:Nat -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(d, k), x)) == True{} : Bool}

2^k x <= 2^(d + k) x

def shift_le_k source · line 36 · raw

@+j:Nat -> @+k:Nat -> @+x:Nat -> @+d:Nat -> @+hd:{Nat.add(d, j) == k : Nat} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(j, x), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x)) == True{} : Bool}

def shift_mul2 source · line 40 · raw

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

2^a 2^b = 2^(a + b)

def shift_pos source · line 47 · raw

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

0 < 2^k

def small_le source · line 52 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+a:Nat -> @+h:{Nat.is_le(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, 1n)) == True{} : Bool} -> {Nat.is_le(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool}

a small closed number below 2^k

def cp_eq source · line 58 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(32n, one), 977n) : Nat}

def cp_le source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(33n, one)) == True{} : Bool}

def shift_lt_succ source · line 75 · raw

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

2^j < 2^(1 + j), and 2^j < 2^k for j < k (k = d + 1 + j)

def shift_lt_k source · line 79 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+j:Nat -> @+k:Nat -> @+d:Nat -> @+hd:{Nat.add(d, 1n+j) == k : Nat} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(j, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool}

def cp_cc source · line 83 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

the fold bounds for p: 2 c < 2^256 and (1 + c) c + c <= 2^256

def cp_succ_le source · line 89 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(34n, one)) == True{} : Bool}

def cp_hb source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

def pp source · line 101 · raw

@+one:Nat -> Nat

p = 1 + pp, m + c = 2^256

def cp1_le source · line 104 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

def pp_sum source · line 110 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 1n), pp(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

(c + 1) + pp = 2^256

def hm_p source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(1n+pp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

def prime_eq source · line 123 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.prime(one) == 1n+pp(one) : Nat}

def digits_split source · line 130 · raw

@+one:Nat -> @n:Nat -> @ds:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, ds) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(n, ds)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(n, ds)))) : Nat}

def digits_lt source · line 153 · 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/spec/crypto/secp256k1/field.digits(one, ys), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(k, one)) == True{} : Bool}

def cn8 source · line 157 · raw

List<&2, Nat>

def cn8_limbs source · line 160 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 8n, cn8) == True{} : Bool}

def cn_split source · line 164 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.digits(one, cn8), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(8n, one)) : Nat}

def cn_lt source · line 171 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(129n, one)) == True{} : Bool}

def cn_cc source · line 178 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

the fold bounds for n: 2 c < 2^256, (1 + c) c <= 4 2^256, 5 c + c <= 2^256

def four_t source · line 184 · raw

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

def cn_hb1 source · line 191 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool}

def six source · line 197 · raw

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

def eight source · line 200 · raw

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

def cn_hb2 source · line 211 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

def np source · line 220 · raw

@+one:Nat -> Nat

n = 1 + np, n + c = 2^256

def cn1_le source · line 223 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 1n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

def np_sum source · line 227 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one), 1n), np(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

def hm_n source · line 230 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(1n+np(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat}

def order_eq source · line 240 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.order(one) == 1n+np(one) : Nat}