~/bend-docscommunity

proofs/crypto/secp256k1/reducek.bend source

proofs/crypto/secp256k1/reducek.bend on the hub · documented module

# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reducek.src; edit the .srcimport Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/secp256k1/field.bend as FSimport ../../../src/crypto/secp256k1/limbs.bend as Limport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Lgimport ../../lib/lemmas/proofs/nat_algebra.bend as NAimport ./limbs.bend as LVimport ./fprot.bend as FRimport ./ineq.bend as Iimport ./reduce.bend as R# L.reduce(c, k, x) = x mod m for x below 2^512: k = 3 folds when# (1 + c) c + c <= 2^256 (the field, c = 2^32 + 977), k = 4 when# (1 + c) c <= 4 2^256 and 6 c <= 2^256 (the scalars, c < 2^129); in both# cases 2 c < 2^256. The hypotheses on c are stated with the specification's# value (FS.value(one, c), which the checker keeps symbolic), so that a# constant c can be substituted.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}:  R.round_lo(one, h1, xs)# t + t c = (1 + c) tdef addmul(+t: Nat, +cv: Nat) -> {Nat.add(t, Nat.mul(t, cv)) == Nat.mul(1n+cv, t) : Nat}:  %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}  {==}# ---- three folds ----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}:  +t = C.shift(256n, one)  +cv = LV.ev(c)  +x0 = L.carry(32n, xs, 0n)  +x1 = L.carry(32n, L.fold(c, x0), 0n)  +x2 = L.carry(32n, L.fold(c, x1), 0n)  +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)  +h1b = R.round_lt1(one, h1, c, x0, t, x0_lo(one, h1, xs), h0)  +h1c = I.lt_subst_r(LV.ev(x1), Nat.add(t, Nat.mul(t, cv)), Nat.mul(1n+cv, t), addmul(t, cv), h1b)  +h2b = R.round_lt1(one, h1, c, x1, 1n+cv, R.round_lo(one, h1, L.fold(c, x0)), h1c)  +h3 = R.fold_lt2(one, h1, c, x2, Nat.mul(1n+cv, cv), hb, R.round_lo(one, h1, L.fold(c, x1)), h2b)  %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}  h3def 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}:  +x0 = L.carry(32n, xs, 0n)  +x1 = L.carry(32n, L.fold(c, x0), 0n)  +x2 = L.carry(32n, L.fold(c, x1), 0n)  %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}  %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}  %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}  %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}  {==}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}:  %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}  %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}  %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}  %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}  %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}  {==}# ---- four folds ----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}:  +t = C.shift(256n, one)  +cv = LV.ev(c)  +x0 = L.carry(32n, xs, 0n)  +x1 = L.carry(32n, L.fold(c, x0), 0n)  +x2 = L.carry(32n, L.fold(c, x1), 0n)  +x3 = L.carry(32n, L.fold(c, x2), 0n)  +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)  +h1b = R.round_lt1(one, h1, c, x0, t, x0_lo(one, h1, xs), h0)  +h1c = I.lt_subst_r(LV.ev(x1), Nat.add(t, Nat.mul(t, cv)), Nat.mul(1n+cv, t), addmul(t, cv), h1b)  +h2b = R.round_lt1(one, h1, c, x1, 1n+cv, R.round_lo(one, h1, L.fold(c, x0)), h1c)  +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))  +h3b = R.round_lt1(one, h1, c, x2, 5n, R.round_lo(one, h1, L.fold(c, x1)), h2c)  +h4 = R.fold_lt2(one, h1, c, x3, Nat.mul(5n, cv), hb2, R.round_lo(one, h1, L.fold(c, x2)), h3b)  %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}  h4# ---- the reductions ----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}:  +et = R.take_small(one, h1, r, hr)  +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)  %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}  %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}  {==}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}:  +et = R.take_small(one, h1, r, hr)  +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)  R.canon_limbs(one, h1, c, L.take(16n, r), hlo, hv, hcc)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}:  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)))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}:  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)))# x mod m for x < 2^512, m = 2^256 - c, (1 + c) c + c <= 2^256, 2 c < 2^256def 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}:  %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}  +r = L.rounds(3n, c, L.carry(32n, xs, 0n))  %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}  %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}  {==}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}:  %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}  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))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}:  %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}  %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}  %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}  {==}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}:  %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}  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))# ---- with the hypotheses on c in the specification's terms ----def hv_ev(+one: Nat, +h1: {one == 1n : Nat}, +c: List<&2, Nat>) -> {FS.value(one, c) == LV.ev(c) : Nat}:  LV.ev_value(one, h1, c)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}:  +e = hv_ev(one, h1, c)  +hm2 = Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), e, hm)  +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)  +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)  reduce3_v(one, h1, mp, c, hm2, hcc2, hb2, xs, hx)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}:  +e = hv_ev(one, h1, c)  +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)  +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)  reduce3_l(one, h1, c, hcc2, hb2, xs, hx)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}:  +e = hv_ev(one, h1, c)  +hm2 = Lg.subst(Nat, z => {Nat.add(1n+mp, z) == C.shift(256n, one) : Nat}, FS.value(one, c), LV.ev(c), e, hm)  +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)  +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)  +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)  reduce4_v(one, h1, mp, c, hm2, hcc2, hb12, hb22, xs, hx)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}:  +e = hv_ev(one, h1, c)  +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)  +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)  +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)  reduce4_l(one, h1, c, hcc2, hb12, hb22, xs, hx)