~/jendhub

proofs/crypto/secp256k1/reducek.bend

bend-collections-laws-crypto@1.0.0.0 · 155 lines · 19 definitions

1# GENERATED by tools/generators/rw.py from ../../../tools/generators/secp256k1_hand/reducek.src; edit the .src
2import Base
3import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fprot.bend as FR
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/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
21def 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
25def 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
31def 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
45def 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
55def 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
65def 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
84def 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
91def 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
96def 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
99def 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
103def 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
110def 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
114def 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
120def 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
126def 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
129def 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
136def 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
142def 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
150def 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)