~/bend-docscommunity

proofs/crypto/secp256k1/reducek.bend checks

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

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

11 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 ./limbs.bend as LV
import ./fprot.bend as FR
import ./ineq.bend as I
import ./reduce.bend as R

Definitions

def x0_lo source · line 21 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+xs: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, xs, 0n))) == True{} : Bool}

def addmul source · line 25 · raw

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

t + t c = (1 + c) t

def red3_x3 source · line 31 · raw

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

def red3_mod source · line 45 · 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.rounds(3n, c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, xs, 0n))), 1n+mp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def red4_mod source · line 55 · 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.rounds(4n, c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, xs, 0n))), 1n+mp) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def red4_x4 source · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+xs:List<&2, Nat> -> @+hb1:{Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> @+hb2:{Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.rounds(4n, c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.carry(32n, xs, 0n))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool}

def red_fin_v source · line 84 · 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} -> @+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} -> @+r:List<&2, Nat> -> @+hlo:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, r)) == True{} : Bool} -> @+hr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.canon(c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, r))) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(r), 1n+mp) : Nat}

def red_fin_l source · line 91 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, 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} -> @+r:List<&2, Nat> -> @+hlo:{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, r)) == True{} : Bool} -> @+hr:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(r), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.canon(c, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.take(16n, r))) == True{} : Bool}

def r3_lo source · line 96 · raw

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

def r4_lo source · line 99 · raw

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

def reduce3_v source · line 103 · 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} -> @+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} -> @+hb:{Nat.is_le(Nat.add(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 3n, xs)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

x mod m for x < 2^512, m = 2^256 - c, (1 + c) c + c <= 2^256, 2 c < 2^256

def reduce3_l source · line 110 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, 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} -> @+hb:{Nat.is_le(Nat.add(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 3n, xs)) == True{} : Bool}

def reduce4_v source · line 114 · 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} -> @+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} -> @+hb1:{Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> @+hb2:{Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 4n, xs)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def reduce4_l source · line 120 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, 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} -> @+hb1:{Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> @+hb2:{Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 4n, xs)) == True{} : Bool}

def hv_ev source · line 126 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(c) : Nat}

def reduce3_vv source · line 129 · 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} -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hb:{Nat.is_le(Nat.add(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 3n, xs)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def reduce3_lv source · line 136 · raw

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

def reduce4_vv source · line 142 · 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} -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hb1:{Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> @+hb2:{Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 4n, xs)) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), 1n+mp) : Nat}

def reduce4_lv source · line 150 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+c:List<&2, Nat> -> @+hcc:{Nat.is_lt(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+hb1:{Nat.is_le(Nat.mul(1n+0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), Nat.mul(4n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> @+hb2:{Nat.is_le(Nat.add(Nat.mul(5n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.value(one, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one)) == True{} : Bool} -> @+xs:List<&2, Nat> -> @+hx:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.ev(xs), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(256n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.limbs16(one, 16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.reduce(c, 4n, xs)) == True{} : Bool}