proofs/crypto/secp256k1/listops.bend checks

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

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

14 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 ./bounds.bend as B
import ./reduce.bend as R

Definitions

def is_eq_add0 source · line 22 · raw

@a:Nat -> @+b:Nat -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}

def and_true source · line 29 · raw

@+b:Bool -> {Bool.and(True{}, b) == b : Bool}

def and_assoc source · line 32 · raw

@a:Bool -> @+b:Bool -> @+c:Bool -> {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}

def sh_eq0 source · line 40 · raw

@+y:Nat -> {Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, y), 0n) == Nat.is_eq(y, 0n) : Bool}

2^16 y == 0 exactly when y == 0

def and_true_r source · line 45 · raw

@b:Bool -> {Bool.and(b, True{}) == b : Bool}

def nonzero_v source · line 53 · raw

@xs:List<&2, Nat> -> @+acc:Nat -> {Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.nonzero(xs, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 0n)) : Bool}

def is_zero_v source · line 65 · raw

@+xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.is_zero(xs) == Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 0n) : Bool}

def parity_v source · line 70 · raw

@+xs:List<&2, Nat> -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.hd0(xs), 2n) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 2n) : Nat}

def iff_bool source · line 79 · raw

@p:Bool -> @q:Bool -> @f:(@_:{p == True{} : Bool} -> {q == True{} : Bool}) -> @g:(@_:{q == True{} : Bool} -> {p == True{} : Bool}) -> {p == q : Bool}

def w_succ source · line 92 · raw

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

def digit_form source · line 96 · raw

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

x + 2^16 a = a W + x with W = 1 + wp

def lt_w source · line 102 · raw

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

def uniq_lo source · line 106 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+e:{Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, a)) == Nat.add(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, b)) : Nat} -> {x == y : Nat}

def uniq_hi source · line 113 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+e:{Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, a)) == Nat.add(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, b)) : Nat} -> {a == b : Nat}

def eq_digit_f source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+h:{Nat.is_eq(Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, a)), Nat.add(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, b))) == True{} : Bool} -> {Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool}

def eq_digit_g source · line 126 · raw

@+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) == True{} : Bool} -> {Nat.is_eq(Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, a)), Nat.add(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, b))) == True{} : Bool}

def eq_digit source · line 133 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_lt(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, one)) == True{} : Bool} -> {Nat.is_eq(Nat.add(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, a)), Nat.add(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(16n, b))) == Bool.and(Nat.is_eq(x, y), Nat.is_eq(a, b)) : Bool}

def absdiff source · line 139 · raw

@x:Nat -> @y:Nat -> {Nat.is_eq(Nat.add(Nat.sub(x, y), Nat.sub(y, x)), 0n) == Nat.is_eq(x, y) : Bool}

(x - y) + (y - x) == 0 exactly when x == y

def diff_v source · line 150 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @n:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, Nat> -> @+acc:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, xs) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, n, ys) == True{} : Bool} -> {Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.diff(xs, ys, acc), 0n) == Bool.and(Nat.is_eq(acc, 0n), Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(ys))) : Bool}

def eq_v source · line 174 · raw

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

def hz source · line 179 · raw

@+lo:Nat -> @hi:Nat -> @+t:Nat -> @+hl:{Nat.is_lt(lo, t) == True{} : Bool} -> {Nat.is_eq(hi, 0n) == Nat.is_lt(Nat.add(lo, Nat.mul(hi, t)), t) : Bool}

def ltm_v source · line 187 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mp:Nat -> @+c:List<&2, Nat> -> @+hm:{Nat.add(1n+mp, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat} -> @+x:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.ltm(c, x) == Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), 1n+mp) : Bool}

def ltm_vv source · line 198 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mp:Nat -> @+c:List<&2, Nat> -> @+hm:{Nat.add(1n+mp, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat} -> @+x:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.ltm(c, x) == Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(x), 1n+mp) : Bool}

def small_ev source · line 203 · raw

@+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev([k]) == k : Nat}

def small_v source · line 208 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> @+hk:{Nat.is_lt(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([k])) == k : Nat}

def small_l source · line 215 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+k:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16([k])) == True{} : Bool}