~/bend-docscommunity

proofs/crypto/secp256k1/reduce.bend checks

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

GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reduce.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/arith.bend as AR
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

Definitions

def split256 source · line 27 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(16n, xs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) : Nat}

x = lo + hi 2^256 for lo, hi the first 16 limbs and the rest

def fold_v source · line 33 · raw

@+c:List<&2, Nat> -> @+xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(16n, xs)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c))) : Nat}

def fold_eq source · line 39 · 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} -> @+xs:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(16n, xs)), 1n+mp)) : Nat}

x = fold(x) + hi m

def fold_mod source · line 66 · 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} -> @+xs:List<&2, Nat> -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs)), 1n+mp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def mul_lt_cancel source · line 75 · raw

@+t:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(Nat.mul(a, t), Nat.mul(b, t)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

T a < T b gives a < b

def hi_lt source · line 84 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs:List<&2, Nat> -> @+hh:Nat -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(hh, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(16n, xs)), hh) == True{} : Bool}

the high part of x < 2^256 H is below H

def fold_lt1 source · line 93 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+xs:List<&2, Nat> -> @+hh:Nat -> @+hlo:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)) == True{} : Bool} -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(hh, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), Nat.mul(hh, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)))) == True{} : Bool}

a fold of x < 2^256 H (low 16 limbs fine) is below 2^256 + H c

def cancel_t source · line 101 · raw

@+t:Nat -> @+lo:Nat -> @+h:Nat -> @+d:Nat -> @+hx:{Nat.is_lt(Nat.add(lo, Nat.mul(1n+h, t)), Nat.add(t, d)) == True{} : Bool} -> {Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d) == True{} : Bool}

lo + h t < d when lo + (1 + h) t < t + d

def fold_lt2_h source · line 107 · raw

@+t:Nat -> @+lo:Nat -> @+cv:Nat -> @+d:Nat -> @+f:Nat -> @+hd:{Nat.is_le(Nat.add(d, cv), t) == True{} : Bool} -> @h:Nat -> @+hs:{Nat.is_lt(Nat.add(lo, Nat.mul(h, t)), d) == True{} : Bool} -> @+ef:{f == Nat.add(lo, Nat.mul(1n+h, cv)) : Nat} -> {Nat.is_lt(f, t) == True{} : Bool}

(the hi >= 1 case) lo + h t < d with d + c <= t: h = 0, and then lo + c < t

def fold_lt2_z source · line 122 · raw

@+t:Nat -> @+lo:Nat -> @+cv:Nat -> @+f:Nat -> @+ll:{Nat.is_lt(lo, t) == True{} : Bool} -> @+ef:{f == Nat.add(lo, Nat.mul(0n, cv)) : Nat} -> {Nat.is_lt(f, t) == True{} : Bool}

the hi = 0 case: the fold is lo

def fold_lt2_hi source · line 128 · raw

@+t:Nat -> @+lo:Nat -> @+cv:Nat -> @+d:Nat -> @+f:Nat -> @+x:Nat -> @+hd:{Nat.is_le(Nat.add(d, cv), t) == True{} : Bool} -> @+ll:{Nat.is_lt(lo, t) == True{} : Bool} -> @+hx:{Nat.is_lt(x, Nat.add(t, d)) == True{} : Bool} -> @hi:Nat -> @+ex:{x == Nat.add(lo, Nat.mul(hi, t)) : Nat} -> @+ef:{f == Nat.add(lo, Nat.mul(hi, cv)) : Nat} -> {Nat.is_lt(f, t) == True{} : Bool}

def fold_lt2 source · line 136 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+xs:List<&2, Nat> -> @+d:Nat -> @+hd:{Nat.is_le(Nat.add(d, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hlo:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)) == True{} : Bool} -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), d)) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

a fold of x < 2^256 + D (low 16 limbs fine), with D + c <= 2^256, is below 2^256

def pick_one source · line 144 · raw

@+x:Nat -> @+y:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.pick1(1n, x, y) == x : Nat}

def pick_zero source · line 150 · raw

@+x:Nat -> @+y:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.pick1(0n, x, y) == y : Nat}

def sel_one source · line 157 · raw

@+one:Nat -> @n:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.select(1n, xs, ys) == xs : List<&2, Nat>}

select(1, xs, ys) == xs and select(0, xs, ys) == ys for lists of n limbs

def sel_zero source · line 173 · raw

@+one:Nat -> @n:Nat -> @xs:List<&2, Nat> -> @ys:List<&2, 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} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.select(0n, xs, ys) == ys : List<&2, Nat>}

def canon0_val source · line 194 · raw

@+mp:Nat -> @+v:Nat -> @+cv:Nat -> @+lo:Nat -> @+t:Nat -> @+ht:{Nat.add(1n+mp, cv) == t : Nat} -> @+ll:{Nat.is_lt(lo, t) == True{} : Bool} -> @+eu:{Nat.add(v, cv) == lo : Nat} -> {v == Nat.mod(v, 1n+mp) : Nat}

v + cv = lo < t = m + cv: v < m, and v mod m = v

def canon1_val source · line 201 · raw

@+mp:Nat -> @+v:Nat -> @+cv:Nat -> @+lo:Nat -> @+t:Nat -> @+ht:{Nat.add(1n+mp, cv) == t : Nat} -> @+hv:{Nat.is_lt(v, t) == True{} : Bool} -> @+hcc:{Nat.is_lt(Nat.add(cv, cv), t) == True{} : Bool} -> @+eu:{Nat.add(v, cv) == Nat.add(lo, t) : Nat} -> {lo == Nat.mod(v, 1n+mp) : Nat}

v + cv = lo + t with t = m + cv, v < t, cv + cv < t: v mod m = lo

def u_val source · line 221 · raw

@+c:List<&2, Nat> -> @+t:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.add(t, c), 0n)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)) : Nat}

def u_hi source · line 227 · raw

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

the carried sum t + c is below 2 2^256, so its part above 2^256 is 0 or 1

def canon_u source · line 236 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mp:Nat -> @+c:List<&2, Nat> -> @+t:List<&2, Nat> -> @+ht16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, t) == True{} : Bool} -> @+hv:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+htc:{Nat.add(1n+mp, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat} -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @b:Nat -> @+eb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.drop(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.add(t, c), 0n))) == b : Nat} -> @+hb:{Nat.is_lt(b, 2n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.select(b, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.add(t, c), 0n)), t)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 1n+mp) : Nat}

def canon_v source · line 258 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+mp:Nat -> @+c:List<&2, Nat> -> @+t:List<&2, Nat> -> @+ht16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, t) == True{} : Bool} -> @+hv:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+htc:{Nat.add(1n+mp, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one) : Nat} -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 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.canon(c, t)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 1n+mp) : Nat}

def canon_lb source · line 262 · raw

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

def canon_limbs source · line 275 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+t:List<&2, Nat> -> @+ht16:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, t) == True{} : Bool} -> @+hv:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(t), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.canon(c, t)) == True{} : Bool}

def round_v source · line 281 · raw

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

def round_mod source · line 284 · 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} -> @+xs:List<&2, Nat> -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs), 0n)), 1n+mp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def round_lo source · line 289 · raw

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

def round_lt1 source · line 293 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+xs:List<&2, Nat> -> @+hh:Nat -> @+hlo:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)) == True{} : Bool} -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(hh, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.fold(c, xs), 0n)), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), Nat.mul(hh, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)))) == True{} : Bool}

below 2^256 H after a round, from below 2^256 H' before (H = 1 + H' c)

def take_small_h source · line 297 · raw

@+xs:List<&2, Nat> -> @hi:Nat -> @+tt:Nat -> @+h0:{Nat.is_lt(hi, 1n) == True{} : Bool} -> @+es:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)), Nat.mul(hi, tt)) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, xs)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs) : Nat}

def take_small source · line 308 · raw

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

x below 2^256 (16 limbs fine): the first 16 limbs are all of it