~/bend-docscommunity

proofs/crypto/secp256k1/negate.bend checks

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

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/negate.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 e255 source · line 22 · raw

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

def bb_sq source · line 26 · raw

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

def bb_pos source · line 32 · raw

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

def pred_succ source · line 37 · raw

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

(B - 1) + 1 = B

def digit_max source · line 42 · raw

@+b:Nat -> @+h:{Nat.is_le(1n, b) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(b, 1n), Nat.mul(Nat.sub(b, 1n), b)), 1n) == Nat.mul(b, b) : Nat}

(B - 1) + (B - 1) B + 1 = B B

def hi_byte_lt source · line 55 · 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(Nat.div(x, 256n), 256n) == True{} : Bool}

x < 2^16: x div 256 < 256

def combine source · line 66 · raw

@+l:Nat -> @+h:Nat -> @+h2:Nat -> @+l2:Nat -> @+b:Nat -> {Nat.add(Nat.add(l, Nat.mul(h, b)), Nat.add(Nat.mul(h2, b), l2)) == Nat.add(Nat.add(l2, l), Nat.mul(Nat.add(h2, h), b)) : Nat}

(l + h B) + (h' B + l') = (l' + l) + (h' + h) B

def comp1_v source · line 85 · raw

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

comp1(x) + x + 1 = 2^16 for x < 2^16

def comp1_o source · line 100 · raw

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

def comp_v source · line 105 · 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} -> {Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.comp(xs)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs)), one) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.pos(n, one) : Nat}

comp(x) + x + 1 = 2^(16 n) for n limbs below 2^16

def bc_limbs source · line 136 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+b:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.norm16(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.add(b, c))) == True{} : Bool}

b + c as 16 limbs, when b + c < 2^256

def bc_v source · line 139 · raw

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

def neg_t source · line 148 · raw

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

neg_raw(c, b) + b + c = 2^256

def neg_v source · line 162 · 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} -> @+b:List<&2, Nat> -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(b), 1n+mp) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.neg_raw(c, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(b)) == 1n+mp : Nat}

neg_raw(c, b) + b = m, for b < m = 2^256 - c

def neg_vv source · line 170 · 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} -> @+b:List<&2, Nat> -> @+hb:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(b), 1n+mp) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.neg_raw(c, b)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(b)) == 1n+mp : Nat}

def sub_mod source · line 174 · raw

@+mp:Nat -> @+a:Nat -> @+b:Nat -> @+nb:Nat -> @+hlt:{Nat.is_lt(b, 1n+mp) == True{} : Bool} -> @+hn:{Nat.add(nb, b) == 1n+mp : Nat} -> {Nat.mod(Nat.add(a, nb), 1n+mp) == Nat.mod(Nat.sub(Nat.add(a, 1n+mp), Nat.mod(b, 1n+mp)), 1n+mp) : Nat}

a + (m - b) = (a + m) - b, for b < m