~/bend-docscommunity

proofs/crypto/secp256k1/rconst.bend checks

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

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

17 imports
import Base
import ./limbs.bend as LV
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/ecdsa.bend as E
import ../../lib/nat.bend as N
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 ./ineq.bend as I
import ./bounds.bend as B2
import ./consts.bend as K
import ./lits.bend as LT
import ./fieldops.bend as FO
import ./fieldpow.bend as FP
import ./scalarpow.bend as SP

Definitions

def cn_fe_v source · line 26 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.cn_fe) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one) : Nat}

def cp_fe_v source · line 30 · raw

@+one:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.cp_fe) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one) : Nat}

def cn_fe_l source · line 34 · raw

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

def cp_fe_l source · line 37 · raw

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

def cn_ge source · line 42 · raw

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

def cp_lt_cn source · line 48 · raw

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

def p_ge source · line 52 · raw

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

2^255 <= p

def cn_lt_p source · line 59 · raw

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

def cp_lt_p source · line 62 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one)) == True{} : Bool}

def pn_sum source · line 66 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.add(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.pp(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cp(one)) == Nat.add(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.np(one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.cn(one)) : Nat}

p + c_p = n + c_n (= 2^256)

def le_cancel_l source · line 71 · raw

@+c:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(Nat.add(c, x), Nat.add(c, y)) == True{} : Bool} -> {Nat.is_le(x, y) == True{} : Bool}

def sc source · line 74 · raw

@+b:Nat -> @+c:Nat -> {1n+Nat.add(b, c) == Nat.add(c, 1n+b) : Nat}

def lt_of_sum source · line 82 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+e:{Nat.add(a, c) == Nat.add(b, d) : Nat} -> @+h:{Nat.is_lt(c, d) == True{} : Bool} -> {Nat.is_lt(b, a) == True{} : Bool}

a + c = b + d and c < d give b < a

def m1 source · line 91 · raw

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

def mod_small source · line 95 · raw

@+pp:Nat -> @+x:Nat -> @+h:{Nat.is_lt(x, 1n+pp) == True{} : Bool} -> {Nat.mod(x, 1n+pp) == x : Nat}

x mod P = x for x < P

def mod_p1 source · line 99 · raw

@+pp:Nat -> @+e:Nat -> @+h:{Nat.is_lt(e, 1n+pp) == True{} : Bool} -> {Nat.mod(Nat.add(1n+pp, e), 1n+pp) == e : Nat}

(P + e) mod P = e for e < P

def rn_sum_c source · line 103 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+cn:Nat -> @+cp:Nat -> @+hs:{Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat} -> @+sa:{Nat.add(cn, Nat.sub(Nat.add(r, 1n+pp), cn)) == Nat.add(r, 1n+pp) : Nat} -> {Nat.add(cn, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp)) == Nat.add(cn, Nat.add(r, nn)) : Nat}

def rn_sum source · line 115 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+cn:Nat -> @+cp:Nat -> @+hs:{Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat} -> @+hl:{Nat.is_le(cn, Nat.add(r, 1n+pp)) == True{} : Bool} -> {Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp) == Nat.add(r, nn) : Nat}

with P + c_p = N + c_n and c_n <= r + P: (r + P - c_n) + c_p = r + N

def rn_val source · line 121 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+cn:Nat -> @+cp:Nat -> @+hs:{Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat} -> @+hcn:{Nat.is_lt(cn, 1n+pp) == True{} : Bool} -> {Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), Nat.mod(cn, 1n+pp)), 1n+pp), cp), 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}

((r + P - (c_n mod P)) mod P + c_p) mod P = (r + N) mod P

def rc_true source · line 128 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+h:{Nat.is_lt(Nat.add(r, nn), 1n+pp) == True{} : Bool} -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == True{} : Bool}

def rc_false source · line 133 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+hr:{Nat.is_lt(r, nn) == True{} : Bool} -> @+hn:{Nat.is_lt(nn, 1n+pp) == True{} : Bool} -> @+h:{Nat.is_lt(Nat.add(r, nn), 1n+pp) == False{} : Bool} -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == False{} : Bool}

def rn_cond source · line 146 · raw

@+r:Nat -> @+nn:Nat -> @+pp:Nat -> @+hr:{Nat.is_lt(r, nn) == True{} : Bool} -> @+hn:{Nat.is_lt(nn, 1n+pp) == True{} : Bool} -> @c:Bool -> @+hc:{Nat.is_lt(Nat.add(r, nn), 1n+pp) == c : Bool} -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == c : Bool}

for r < N < P: (r + N) mod P >= N exactly when r + N < P

def n_lt_p source · line 154 · raw

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

n < p