1 # GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reducek.src; edit the .src 2 import Base 3 import ../../../spec/lib/common.bend as C 4 import ../../../spec/crypto/secp256k1/field.bend as FS 5 import ../../../src/crypto/secp256k1/limbs.bend as L 6 import ../../lib/nat.bend as N 7 import ../../lib/logic.bend as Lg 8 import ../../lib/lemmas/proofs/nat_algebra.bend as NA 9 import ./limbs.bend as LV 10 import ./fprot.bend as FR 11 import ./ineq.bend as I 12 import ./reduce.bend as R 13 14 # L.reduce(c, k, x) = x mod m for x below 2^512: k = 3 folds when 15 # (1 + c) c + c <= 2^256 (the field, c = 2^32 + 977), k = 4 when 16 # (1 + c) c <= 4 2^256 and 6 c <= 2^256 (the scalars, c < 2^129); in both 17 # cases 2 c < 2^256. The hypotheses on c are stated with the specification's 18 # value (FS.value(one, c), which the checker keeps symbolic), so that a 19 # constant c can be substituted. 20 21 def x0_lo(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.take(16n, L.carry(32n, xs, 0n))) == True{} : Bool}: 22 R.round_lo(one, h1, xs) 23 24 # t + t c = (1 + c) t 25 def addmul(+t: Nat, +cv: Nat) -> {Nat.add(t, Nat.mul(t, cv)) == Nat.mul(1n+cv, t) : Nat}: 26 %Equal.sym(Nat, Nat.mul(t, cv), Nat.mul(cv, t), NA.mul_comm(t, cv)) : {Nat.add(t, _) == Nat.mul(1n+cv, t) : Nat} 27 {==} 28 29 # ---- three folds ---- 30 31 def red3_x3(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>, +hb: {Nat.is_le(Nat.add(Nat.mul(1n+LV.ev(c), LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.rounds(3n, c, L.carry(32n, xs, 0n))), C.shift(256n, one)) == True{} : Bool}: 32 +t = C.shift(256n, one) 33 +cv = LV.ev(c) 34 +x0 = L.carry(32n, xs, 0n) 35 +x1 = L.carry(32n, L.fold(c, x0), 0n) 36 +x2 = L.carry(32n, L.fold(c, x1), 0n) 37 +h0 = I.lt_subst_l(LV.ev(xs), LV.ev(x0), Nat.mul(t, t), Equal.sym(Nat, LV.ev(x0), LV.ev(xs), LV.carry_v(32n, xs, 0n)), hx) 38 +h1b = R.round_lt1(one, h1, c, x0, t, x0_lo(one, h1, xs), h0) 39 +h1c = I.lt_subst_r(LV.ev(x1), Nat.add(t, Nat.mul(t, cv)), Nat.mul(1n+cv, t), addmul(t, cv), h1b) 40 +h2b = R.round_lt1(one, h1, c, x1, 1n+cv, R.round_lo(one, h1, L.fold(c, x0)), h1c) 41 +h3 = R.fold_lt2(one, h1, c, x2, Nat.mul(1n+cv, cv), hb, R.round_lo(one, h1, L.fold(c, x1)), h2b) 42 %Equal.sym(Nat, LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), LV.ev(L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n))), R.round_v(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n))) : {Nat.is_lt(_, C.shift(256n, one)) == True{} : Bool} 43 h3 44 45 def red3_mod(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +xs: List<&2, Nat>) -> {Nat.mod(LV.ev(L.rounds(3n, c, L.carry(32n, xs, 0n))), 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 46 +x0 = L.carry(32n, xs, 0n) 47 +x1 = L.carry(32n, L.fold(c, x0), 0n) 48 +x2 = L.carry(32n, L.fold(c, x1), 0n) 49 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 50 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 51 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, xs, 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, xs, 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 52 %Equal.sym(Nat, LV.ev(L.carry(32n, xs, 0n)), Nat.add(0n, LV.ev(xs)), LV.carry_v(32n, xs, 0n)) : {Nat.mod(_, 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 53 {==} 54 55 def red4_mod(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +xs: List<&2, Nat>) -> {Nat.mod(LV.ev(L.rounds(4n, c, L.carry(32n, xs, 0n))), 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 56 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 57 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 58 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 59 %Equal.sym(Nat, Nat.mod(LV.ev(L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 1n+mp), Nat.mod(LV.ev(L.carry(32n, xs, 0n)), 1n+mp), R.round_mod(one, h1, mp, c, hm, L.carry(32n, xs, 0n))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 60 %Equal.sym(Nat, LV.ev(L.carry(32n, xs, 0n)), Nat.add(0n, LV.ev(xs)), LV.carry_v(32n, xs, 0n)) : {Nat.mod(_, 1n+mp) == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 61 {==} 62 63 # ---- four folds ---- 64 65 def red4_x4(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>, +hb1: {Nat.is_le(Nat.mul(1n+LV.ev(c), LV.ev(c)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, +hb2: {Nat.is_le(Nat.add(Nat.mul(5n, LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {Nat.is_lt(LV.ev(L.rounds(4n, c, L.carry(32n, xs, 0n))), C.shift(256n, one)) == True{} : Bool}: 66 +t = C.shift(256n, one) 67 +cv = LV.ev(c) 68 +x0 = L.carry(32n, xs, 0n) 69 +x1 = L.carry(32n, L.fold(c, x0), 0n) 70 +x2 = L.carry(32n, L.fold(c, x1), 0n) 71 +x3 = L.carry(32n, L.fold(c, x2), 0n) 72 +h0 = I.lt_subst_l(LV.ev(xs), LV.ev(x0), Nat.mul(t, t), Equal.sym(Nat, LV.ev(x0), LV.ev(xs), LV.carry_v(32n, xs, 0n)), hx) 73 +h1b = R.round_lt1(one, h1, c, x0, t, x0_lo(one, h1, xs), h0) 74 +h1c = I.lt_subst_r(LV.ev(x1), Nat.add(t, Nat.mul(t, cv)), Nat.mul(1n+cv, t), addmul(t, cv), h1b) 75 +h2b = R.round_lt1(one, h1, c, x1, 1n+cv, R.round_lo(one, h1, L.fold(c, x0)), h1c) 76 +h2c = N.lt_le_trans(LV.ev(x2), Nat.add(t, Nat.mul(1n+cv, cv)), Nat.add(t, Nat.mul(4n, t)), h2b, N.le_add_left(Nat.mul(1n+cv, cv), Nat.mul(4n, t), t, hb1)) 77 +h3b = R.round_lt1(one, h1, c, x2, 5n, R.round_lo(one, h1, L.fold(c, x1)), h2c) 78 +h4 = R.fold_lt2(one, h1, c, x3, Nat.mul(5n, cv), hb2, R.round_lo(one, h1, L.fold(c, x2)), h3b) 79 %Equal.sym(Nat, LV.ev(L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n)), 0n)), LV.ev(L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n))), R.round_v(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n))) : {Nat.is_lt(_, C.shift(256n, one)) == True{} : Bool} 80 h4 81 82 # ---- the reductions ---- 83 84 def red_fin_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +r: List<&2, Nat>, +hlo: {FS.limbs16(one, 16n, L.take(16n, r)) == True{} : Bool}, +hr: {Nat.is_lt(LV.ev(r), C.shift(256n, one)) == True{} : Bool}) -> {LV.ev(L.canon(c, L.take(16n, r))) == Nat.mod(LV.ev(r), 1n+mp) : Nat}: 85 +et = R.take_small(one, h1, r, hr) 86 +hv = I.lt_subst_l(LV.ev(r), LV.ev(L.take(16n, r)), C.shift(256n, one), Equal.sym(Nat, LV.ev(L.take(16n, r)), LV.ev(r), et), hr) 87 %Equal.sym(Nat, LV.ev(L.canon(c, L.take(16n, r))), Nat.mod(LV.ev(L.take(16n, r)), 1n+mp), R.canon_v(one, h1, mp, c, L.take(16n, r), hlo, hv, hm, hcc)) : {_ == Nat.mod(LV.ev(r), 1n+mp) : Nat} 88 %Equal.sym(Nat, LV.ev(L.take(16n, r)), LV.ev(r), et) : {Nat.mod(_, 1n+mp) == Nat.mod(LV.ev(r), 1n+mp) : Nat} 89 {==} 90 91 def red_fin_l(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +r: List<&2, Nat>, +hlo: {FS.limbs16(one, 16n, L.take(16n, r)) == True{} : Bool}, +hr: {Nat.is_lt(LV.ev(r), C.shift(256n, one)) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.canon(c, L.take(16n, r))) == True{} : Bool}: 92 +et = R.take_small(one, h1, r, hr) 93 +hv = I.lt_subst_l(LV.ev(r), LV.ev(L.take(16n, r)), C.shift(256n, one), Equal.sym(Nat, LV.ev(L.take(16n, r)), LV.ev(r), et), hr) 94 R.canon_limbs(one, h1, c, L.take(16n, r), hlo, hv, hcc) 95 96 def r3_lo(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.take(16n, L.rounds(3n, c, L.carry(32n, xs, 0n)))) == True{} : Bool}: 97 R.round_lo(one, h1, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n))) 98 99 def r4_lo(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +xs: List<&2, Nat>) -> {FS.limbs16(one, 16n, L.take(16n, L.rounds(4n, c, L.carry(32n, xs, 0n)))) == True{} : Bool}: 100 R.round_lo(one, h1, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, L.fold(c, L.carry(32n, xs, 0n)), 0n)), 0n)), 0n))) 101 102 # x mod m for x < 2^512, m = 2^256 - c, (1 + c) c + c <= 2^256, 2 c < 2^256 103 def reduce3_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_le(Nat.add(Nat.mul(1n+LV.ev(c), LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(L.reduce(c, 3n, xs)) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 104 %Equal.sym(List<&2, Nat>, L.reduce(c, 3n, xs), L.reduce_go(c, 3n, xs), FR.lred(c, 3n, xs)) : {LV.ev(_) == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 105 +r = L.rounds(3n, c, L.carry(32n, xs, 0n)) 106 %Equal.sym(Nat, LV.ev(L.canon(c, L.take(16n, L.rounds(3n, c, L.carry(32n, xs, 0n))))), Nat.mod(LV.ev(L.rounds(3n, c, L.carry(32n, xs, 0n))), 1n+mp), red_fin_v(one, h1, mp, c, hm, hcc, L.rounds(3n, c, L.carry(32n, xs, 0n)), r3_lo(one, h1, c, xs), red3_x3(one, h1, c, xs, hb, hx))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 107 %Equal.sym(Nat, Nat.mod(LV.ev(L.rounds(3n, c, L.carry(32n, xs, 0n))), 1n+mp), Nat.mod(LV.ev(xs), 1n+mp), red3_mod(one, h1, mp, c, hm, xs)) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 108 {==} 109 110 def reduce3_l(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_le(Nat.add(Nat.mul(1n+LV.ev(c), LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.reduce(c, 3n, xs)) == True{} : Bool}: 111 %Equal.sym(List<&2, Nat>, L.reduce(c, 3n, xs), L.reduce_go(c, 3n, xs), FR.lred(c, 3n, xs)) : {FS.limbs16(one, 16n, _) == True{} : Bool} 112 red_fin_l(one, h1, c, hcc, L.rounds(3n, c, L.carry(32n, xs, 0n)), r3_lo(one, h1, c, xs), red3_x3(one, h1, c, xs, hb, hx)) 113 114 def reduce4_v(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, LV.ev(c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hb1: {Nat.is_le(Nat.mul(1n+LV.ev(c), LV.ev(c)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, +hb2: {Nat.is_le(Nat.add(Nat.mul(5n, LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(L.reduce(c, 4n, xs)) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 115 %Equal.sym(List<&2, Nat>, L.reduce(c, 4n, xs), L.reduce_go(c, 4n, xs), FR.lred(c, 4n, xs)) : {LV.ev(_) == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 116 %Equal.sym(Nat, LV.ev(L.canon(c, L.take(16n, L.rounds(4n, c, L.carry(32n, xs, 0n))))), Nat.mod(LV.ev(L.rounds(4n, c, L.carry(32n, xs, 0n))), 1n+mp), red_fin_v(one, h1, mp, c, hm, hcc, L.rounds(4n, c, L.carry(32n, xs, 0n)), r4_lo(one, h1, c, xs), red4_x4(one, h1, c, xs, hb1, hb2, hx))) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 117 %Equal.sym(Nat, Nat.mod(LV.ev(L.rounds(4n, c, L.carry(32n, xs, 0n))), 1n+mp), Nat.mod(LV.ev(xs), 1n+mp), red4_mod(one, h1, mp, c, hm, xs)) : {_ == Nat.mod(LV.ev(xs), 1n+mp) : Nat} 118 {==} 119 120 def reduce4_l(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +hcc: {Nat.is_lt(Nat.add(LV.ev(c), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +hb1: {Nat.is_le(Nat.mul(1n+LV.ev(c), LV.ev(c)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, +hb2: {Nat.is_le(Nat.add(Nat.mul(5n, LV.ev(c)), LV.ev(c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.reduce(c, 4n, xs)) == True{} : Bool}: 121 %Equal.sym(List<&2, Nat>, L.reduce(c, 4n, xs), L.reduce_go(c, 4n, xs), FR.lred(c, 4n, xs)) : {FS.limbs16(one, 16n, _) == True{} : Bool} 122 red_fin_l(one, h1, c, hcc, L.rounds(4n, c, L.carry(32n, xs, 0n)), r4_lo(one, h1, c, xs), red4_x4(one, h1, c, xs, hb1, hb2, hx)) 123 124 # ---- with the hypotheses on c in the specification's terms ---- 125 126 def hv_ev(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>) -> {FS.value(one, c) == LV.ev(c) : Nat}: 127 LV.ev_value(one, h1, c) 128 129 def reduce3_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(FS.value(one, c), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_le(Nat.add(Nat.mul(1n+FS.value(one, c), FS.value(one, c)), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(L.reduce(c, 3n, xs)) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 130 +e = hv_ev(one, h1, c) 131 +hm2 = Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), e, hm) 132 +hcc2 = Lg.subst(Nat, z => {Nat.is_lt(Nat.add(z, z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hcc) 133 +hb2 = Lg.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(1n+z, z), z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb) 134 reduce3_v(one, h1, mp, c, hm2, hcc2, hb2, xs, hx) 135 136 def reduce3_lv(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +hcc: {Nat.is_lt(Nat.add(FS.value(one, c), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +hb: {Nat.is_le(Nat.add(Nat.mul(1n+FS.value(one, c), FS.value(one, c)), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.reduce(c, 3n, xs)) == True{} : Bool}: 137 +e = hv_ev(one, h1, c) 138 +hcc2 = Lg.subst(Nat, z => {Nat.is_lt(Nat.add(z, z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hcc) 139 +hb2 = Lg.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(1n+z, z), z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb) 140 reduce3_l(one, h1, c, hcc2, hb2, xs, hx) 141 142 def reduce4_vv(+one: Nat, +h1: {one == 1n : Nat}, +mp: Nat, +c: List<&2, Nat>, +hm: {Nat.add(1n+mp, FS.value(one, c)) == C.shift(256n, one) : Nat}, +hcc: {Nat.is_lt(Nat.add(FS.value(one, c), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +hb1: {Nat.is_le(Nat.mul(1n+FS.value(one, c), FS.value(one, c)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, +hb2: {Nat.is_le(Nat.add(Nat.mul(5n, FS.value(one, c)), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {LV.ev(L.reduce(c, 4n, xs)) == Nat.mod(LV.ev(xs), 1n+mp) : Nat}: 143 +e = hv_ev(one, h1, c) 144 +hm2 = Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), e, hm) 145 +hcc2 = Lg.subst(Nat, z => {Nat.is_lt(Nat.add(z, z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hcc) 146 +hb12 = Lg.subst(Nat, z => {Nat.is_le(Nat.mul(1n+z, z), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb1) 147 +hb22 = Lg.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(5n, z), z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb2) 148 reduce4_v(one, h1, mp, c, hm2, hcc2, hb12, hb22, xs, hx) 149 150 def reduce4_lv(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>, +hcc: {Nat.is_lt(Nat.add(FS.value(one, c), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +hb1: {Nat.is_le(Nat.mul(1n+FS.value(one, c), FS.value(one, c)), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, +hb2: {Nat.is_le(Nat.add(Nat.mul(5n, FS.value(one, c)), FS.value(one, c)), C.shift(256n, one)) == True{} : Bool}, +xs: List<&2, Nat>, +hx: {Nat.is_lt(LV.ev(xs), Nat.mul(C.shift(256n, one), C.shift(256n, one))) == True{} : Bool}) -> {FS.limbs16(one, 16n, L.reduce(c, 4n, xs)) == True{} : Bool}: 151 +e = hv_ev(one, h1, c) 152 +hcc2 = Lg.subst(Nat, z => {Nat.is_lt(Nat.add(z, z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hcc) 153 +hb12 = Lg.subst(Nat, z => {Nat.is_le(Nat.mul(1n+z, z), Nat.mul(4n, C.shift(256n, one))) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb1) 154 +hb22 = Lg.subst(Nat, z => {Nat.is_le(Nat.add(Nat.mul(5n, z), z), C.shift(256n, one)) == True{} : Bool}, FS.value(one, c), LV.ev(c), e, hb2) 155 reduce4_l(one, h1, c, hcc2, hb12, hb22, xs, hx)