proofs/math/random/pcg/step.bend

bend-collections-laws-math@1.0.0.0 · 211 lines · 12 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/spec/math/random/pcg.bend as SP
5import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/random/pcg.bend as P
8import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
9import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
16
17# One PCG step (src/math/random/pcg.bend step_with) is the 128-bit LCG
18# s * mul + inc mod 2^128 of spec/math/random/pcg.bend, for every state,
19# multiplier and increment: the limb algebra of Go's (*PCG).next (a 64x64
20# product, the cross products mod 2^64, and a carried 128-bit sum), closed by
21# arithmetic mod 2^64 and 2^128 on the values (C.low), never forming a
22# closed power of two.
23
24# ---- arithmetic mod 2^k ----
25
26def low_l(+k: Nat, +a: Nat, +b: Nat) -> {C.low(k, Nat.add(C.low(k, a), b)) == C.low(k, Nat.add(a, b)) : Nat}:
27  +la = C.low(k, a)
28  +h = C.high(k, a)
29  +e1 = Equal.trans(Nat, Nat.add(a, b), Nat.add(Nat.add(la, C.shift(k, h)), b), Nat.add(Nat.add(la, b), C.shift(k, h)),
30    Equal.cong(Nat, Nat, z => Nat.add(z, b), a, Nat.add(la, C.shift(k, h)), WW.low_high(k, a)),
31    A.add_rot(la, C.shift(k, h), b))
32  Equal.sym(Nat, C.low(k, Nat.add(a, b)), C.low(k, Nat.add(la, b)),
33    Equal.trans(Nat, C.low(k, Nat.add(a, b)), C.low(k, Nat.add(Nat.add(la, b), C.shift(k, h))), C.low(k, Nat.add(la, b)),
34      Equal.cong(Nat, Nat, z => C.low(k, z), Nat.add(a, b), Nat.add(Nat.add(la, b), C.shift(k, h)), e1),
35      WW.low_add_shift(k, Nat.add(la, b), h)))
36
37def low_r(+k: Nat, +a: Nat, +b: Nat) -> {C.low(k, Nat.add(a, C.low(k, b))) == C.low(k, Nat.add(a, b)) : Nat}:
38  Equal.trans(Nat, C.low(k, Nat.add(a, C.low(k, b))), C.low(k, Nat.add(C.low(k, b), a)), C.low(k, Nat.add(a, b)),
39    Equal.cong(Nat, Nat, z => C.low(k, z), Nat.add(a, C.low(k, b)), Nat.add(C.low(k, b), a), NA.add_comm(a, C.low(k, b))),
40    Equal.trans(Nat, C.low(k, Nat.add(C.low(k, b), a)), C.low(k, Nat.add(b, a)), C.low(k, Nat.add(a, b)),
41      low_l(k, b, a),
42      Equal.cong(Nat, Nat, z => C.low(k, z), Nat.add(b, a), Nat.add(a, b), NA.add_comm(b, a))))
43
44# congruence mod 2^k is kept by sums
45def low_add(+k: Nat, +x: Nat, +x2: Nat, +y: Nat, +y2: Nat, +hx: {C.low(k, x) == C.low(k, x2) : Nat}, +hy: {C.low(k, y) == C.low(k, y2) : Nat}) -> {C.low(k, Nat.add(x, y)) == C.low(k, Nat.add(x2, y2)) : Nat}:
46  +e1 = Equal.trans(Nat, C.low(k, Nat.add(x, y)), C.low(k, Nat.add(C.low(k, x), y)), C.low(k, Nat.add(C.low(k, x2), y)),
47    Equal.sym(Nat, C.low(k, Nat.add(C.low(k, x), y)), C.low(k, Nat.add(x, y)), low_l(k, x, y)),
48    Equal.cong(Nat, Nat, z => C.low(k, Nat.add(z, y)), C.low(k, x), C.low(k, x2), hx))
49  +e2 = Equal.trans(Nat, C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, y)), C.low(k, Nat.add(x2, C.low(k, y))),
50    low_l(k, x2, y),
51    Equal.sym(Nat, C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, y)), low_r(k, x2, y)))
52  +e3 = Equal.trans(Nat, C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, C.low(k, y2))), C.low(k, Nat.add(x2, y2)),
53    Equal.cong(Nat, Nat, z => C.low(k, Nat.add(x2, z)), C.low(k, y), C.low(k, y2), hy),
54    low_r(k, x2, y2))
55  Equal.trans(Nat, C.low(k, Nat.add(x, y)), C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, y2)), e1,
56    Equal.trans(Nat, C.low(k, Nat.add(C.low(k, x2), y)), C.low(k, Nat.add(x2, C.low(k, y))), C.low(k, Nat.add(x2, y2)), e2, e3))
57
58def low_low(+k: Nat, +x: Nat) -> {C.low(k, C.low(k, x)) == C.low(k, x) : Nat}:
59  WW.low_fit(k, C.low(k, x), WW.low_fits(k, x))
60
61# mod 2^128, a + 2^64 b depends on b mod 2^64 = lb only
62def low_hi(+k: Nat, +a: Nat, +b: Nat, +lb: Nat, +hlb: {lb == C.low(k, b) : Nat}) -> {C.low(Nat.add(k, k), Nat.add(a, C.shift(k, b))) == C.low(Nat.add(k, k), Nat.add(a, C.shift(k, lb))) : Nat}:
63  +hb = C.high(k, b)
64  +shb = C.shift(k, hb)
65  +e0 = Equal.trans(Nat, b, Nat.add(C.low(k, b), shb), Nat.add(lb, shb), WW.low_high(k, b), Equal.cong(Nat, Nat, z => Nat.add(z, shb), C.low(k, b), lb, Equal.sym(Nat, lb, C.low(k, b), hlb)))
66  +e1 = Equal.trans(Nat, C.shift(k, b), C.shift(k, Nat.add(lb, shb)), Nat.add(C.shift(k, lb), C.shift(k, shb)),
67    Equal.cong(Nat, Nat, z => C.shift(k, z), b, Nat.add(lb, shb), e0),
68    WW.shift_add(k, lb, shb))
69  +e2 = Equal.sym(Nat, C.shift(Nat.add(k, k), hb), C.shift(k, shb), WW.shift_comp(k, k, hb))
70  +sl = C.shift(k, lb)
71  +sh2 = C.shift(Nat.add(k, k), hb)
72  +e3 = Equal.trans(Nat, Nat.add(a, C.shift(k, b)), Nat.add(a, Nat.add(sl, sh2)), Nat.add(Nat.add(a, sl), sh2),
73    Equal.cong(Nat, Nat, z => Nat.add(a, z), C.shift(k, b), Nat.add(sl, sh2),
74      Equal.trans(Nat, C.shift(k, b), Nat.add(sl, C.shift(k, shb)), Nat.add(sl, sh2), e1,
75        Equal.cong(Nat, Nat, z => Nat.add(sl, z), C.shift(k, shb), sh2, e2))),
76    Equal.sym(Nat, Nat.add(Nat.add(a, sl), sh2), Nat.add(a, Nat.add(sl, sh2)), NA.add_assoc(a, sl, sh2)))
77  Equal.trans(Nat, C.low(Nat.add(k, k), Nat.add(a, C.shift(k, b))), C.low(Nat.add(k, k), Nat.add(Nat.add(a, sl), sh2)), C.low(Nat.add(k, k), Nat.add(a, sl)),
78    Equal.cong(Nat, Nat, z => C.low(Nat.add(k, k), z), Nat.add(a, C.shift(k, b)), Nat.add(Nat.add(a, sl), sh2), e3),
79    WW.low_add_shift(Nat.add(k, k), Nat.add(a, sl), hb))
80
81# ---- rearrangements ----
82
83# (((a + c) + d) + (e + g)) + (b + f) == (a + b) + (((c + (e + d)) + f) + g)
84def perm7(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: Nat, +f: Nat, +g: Nat) -> {Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)) == Nat.add(Nat.add(a, b), Nat.add(Nat.add(Nat.add(c, Nat.add(e, d)), f), g)) : Nat}:
85  +R2 = Nat.add(e, Nat.add(f, g))
86  +T = Nat.add(Nat.add(e, g), Nat.add(b, f))
87  +CAN = Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, R2))))
88  +eT1 = Equal.trans(Nat, T, Nat.add(e, Nat.add(g, Nat.add(b, f))), Nat.add(e, Nat.add(b, Nat.add(g, f))),
89    NA.add_assoc(e, g, Nat.add(b, f)),
90    Equal.cong(Nat, Nat, z => Nat.add(e, z), Nat.add(g, Nat.add(b, f)), Nat.add(b, Nat.add(g, f)), NA.add_swap(g, b, f)))
91  +eT2 = Equal.trans(Nat, Nat.add(e, Nat.add(b, Nat.add(g, f))), Nat.add(e, Nat.add(b, Nat.add(f, g))), Nat.add(b, R2),
92    Equal.cong(Nat, Nat, z => Nat.add(e, Nat.add(b, z)), Nat.add(g, f), Nat.add(f, g), NA.add_comm(g, f)),
93    NA.add_swap(e, b, Nat.add(f, g)))
94  +eT = Equal.trans(Nat, T, Nat.add(e, Nat.add(b, Nat.add(g, f))), Nat.add(b, R2), eT1, eT2)
95  +eU = Equal.trans(Nat, Nat.add(Nat.add(c, d), Nat.add(b, R2)), Nat.add(c, Nat.add(d, Nat.add(b, R2))), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
96    NA.add_assoc(c, d, Nat.add(b, R2)),
97    Equal.trans(Nat, Nat.add(c, Nat.add(d, Nat.add(b, R2))), Nat.add(c, Nat.add(b, Nat.add(d, R2))), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
98      Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(d, Nat.add(b, R2)), Nat.add(b, Nat.add(d, R2)), NA.add_swap(d, b, R2)),
99      NA.add_swap(c, b, Nat.add(d, R2))))
100  +eL1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(Nat.add(a, c), d), T), Nat.add(Nat.add(a, Nat.add(c, d)), T),
101    NA.add_assoc(Nat.add(Nat.add(a, c), d), Nat.add(e, g), Nat.add(b, f)),
102    Equal.cong(Nat, Nat, z => Nat.add(z, T), Nat.add(Nat.add(a, c), d), Nat.add(a, Nat.add(c, d)), NA.add_assoc(a, c, d)))
103  +eL2 = Equal.trans(Nat, Nat.add(Nat.add(a, Nat.add(c, d)), T), Nat.add(a, Nat.add(Nat.add(c, d), T)), CAN,
104    NA.add_assoc(a, Nat.add(c, d), T),
105    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(Nat.add(c, d), T), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
106      Equal.trans(Nat, Nat.add(Nat.add(c, d), T), Nat.add(Nat.add(c, d), Nat.add(b, R2)), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
107        Equal.cong(Nat, Nat, z => Nat.add(Nat.add(c, d), z), T, Nat.add(b, R2), eT), eU)))
108  +eL = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(a, Nat.add(c, d)), T), CAN, eL1, eL2)
109  +Rr = Nat.add(Nat.add(Nat.add(c, Nat.add(e, d)), f), g)
110  +eR1 = Equal.trans(Nat, Rr, Nat.add(Nat.add(c, Nat.add(e, d)), Nat.add(f, g)), Nat.add(c, Nat.add(Nat.add(e, d), Nat.add(f, g))),
111    NA.add_assoc(Nat.add(c, Nat.add(e, d)), f, g),
112    NA.add_assoc(c, Nat.add(e, d), Nat.add(f, g)))
113  +eR2 = Equal.trans(Nat, Nat.add(Nat.add(e, d), Nat.add(f, g)), Nat.add(e, Nat.add(d, Nat.add(f, g))), Nat.add(d, R2),
114    NA.add_assoc(e, d, Nat.add(f, g)),
115    NA.add_swap(e, d, Nat.add(f, g)))
116  +eR = Equal.trans(Nat, Nat.add(Nat.add(a, b), Rr), Nat.add(a, Nat.add(b, Rr)), CAN,
117    NA.add_assoc(a, b, Rr),
118    Equal.cong(Nat, Nat, z => Nat.add(a, Nat.add(b, z)), Rr, Nat.add(c, Nat.add(d, R2)),
119      Equal.trans(Nat, Rr, Nat.add(c, Nat.add(Nat.add(e, d), Nat.add(f, g))), Nat.add(c, Nat.add(d, R2)), eR1,
120        Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(Nat.add(e, d), Nat.add(f, g)), Nat.add(d, R2), eR2))))
121  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), CAN, Nat.add(Nat.add(a, b), Rr), eL, Equal.sym(Nat, Nat.add(Nat.add(a, b), Rr), CAN, eR))
122
123# (L + x) + (y + z) == L + ((y + x) + z)
124def swap3(+L: Nat, +x: Nat, +y: Nat, +z: Nat) -> {Nat.add(Nat.add(L, x), Nat.add(y, z)) == Nat.add(L, Nat.add(Nat.add(y, x), z)) : Nat}:
125  Equal.trans(Nat, Nat.add(Nat.add(L, x), Nat.add(y, z)), Nat.add(L, Nat.add(x, Nat.add(y, z))), Nat.add(L, Nat.add(Nat.add(y, x), z)),
126    NA.add_assoc(L, x, Nat.add(y, z)),
127    Equal.cong(Nat, Nat, t => Nat.add(L, t), Nat.add(x, Nat.add(y, z)), Nat.add(Nat.add(y, x), z),
128      Equal.trans(Nat, Nat.add(x, Nat.add(y, z)), Nat.add(Nat.add(x, y), z), Nat.add(Nat.add(y, x), z),
129        Equal.sym(Nat, Nat.add(Nat.add(x, y), z), Nat.add(x, Nat.add(y, z)), NA.add_assoc(x, y, z)),
130        Equal.cong(Nat, Nat, t => Nat.add(t, z), Nat.add(x, y), Nat.add(y, x), NA.add_comm(x, y)))))
131
132# 2^64 ((((h + (p2 + p1)) + i) + c) + 2^64 p3), distributed
133def shx(+k: Nat, +h: Nat, +p2: Nat, +p1: Nat, +i: Nat, +c: Nat, +p3: Nat) -> {C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(h, Nat.add(p2, p1)), i), c), C.shift(k, p3))) == Nat.add(Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)), C.shift(k, C.shift(k, p3))) : Nat}:
134  +w1 = Nat.add(Nat.add(h, Nat.add(p2, p1)), i)
135  +ew1 = Equal.trans(Nat, C.shift(k, w1), Nat.add(C.shift(k, Nat.add(h, Nat.add(p2, p1))), C.shift(k, i)), Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)),
136    WW.shift_add(k, Nat.add(h, Nat.add(p2, p1)), i),
137    Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, i)), C.shift(k, Nat.add(h, Nat.add(p2, p1))), Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))),
138      Equal.trans(Nat, C.shift(k, Nat.add(h, Nat.add(p2, p1))), Nat.add(C.shift(k, h), C.shift(k, Nat.add(p2, p1))), Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))),
139        WW.shift_add(k, h, Nat.add(p2, p1)),
140        Equal.cong(Nat, Nat, z => Nat.add(C.shift(k, h), z), C.shift(k, Nat.add(p2, p1)), Nat.add(C.shift(k, p2), C.shift(k, p1)), WW.shift_add(k, p2, p1)))))
141  Equal.trans(Nat, C.shift(k, Nat.add(Nat.add(w1, c), C.shift(k, p3))), Nat.add(C.shift(k, Nat.add(w1, c)), C.shift(k, C.shift(k, p3))), Nat.add(Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)), C.shift(k, C.shift(k, p3))),
142    WW.shift_add(k, Nat.add(w1, c), C.shift(k, p3)),
143    Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, C.shift(k, p3))), C.shift(k, Nat.add(w1, c)), Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)),
144      Equal.trans(Nat, C.shift(k, Nat.add(w1, c)), Nat.add(C.shift(k, w1), C.shift(k, c)), Nat.add(Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), C.shift(k, c)),
145        WW.shift_add(k, w1, c),
146        Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(k, c)), C.shift(k, w1), Nat.add(Nat.add(C.shift(k, h), Nat.add(C.shift(k, p2), C.shift(k, p1))), C.shift(k, i)), ew1))))
147
148# ---- the step on values ----
149
150# s * M + I == L + 2^64 Z for Z = ((((h + (P2 + P1)) + i) + c) + 2^64 P3)
151def expand(+k: Nat, +vlo: Nat, +vhi: Nat, +vml: Nat, +vmh: Nat, +vil: Nat, +vih: Nat, +vl: Nat, +vh: Nat, +L: Nat, +c: Nat, +h1: {Nat.add(vl, C.shift(k, vh)) == Nat.mul(vlo, vml) : Nat}, +h3: {Nat.add(vl, vil) == Nat.add(L, C.shift(k, c)) : Nat}) -> {Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(vil, C.shift(k, vih))) == Nat.add(L, C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(Nat.mul(vhi, vml), Nat.mul(vlo, vmh))), vih), c), C.shift(k, Nat.mul(vhi, vmh))))) : Nat}:
152  +P1 = Nat.mul(vlo, vmh)
153  +P2 = Nat.mul(vhi, vml)
154  +P3 = Nat.mul(vhi, vmh)
155  +a = vl
156  +b = vil
157  +cc = C.shift(k, vh)
158  +d = C.shift(k, P1)
159  +e = C.shift(k, P2)
160  +f = C.shift(k, vih)
161  +g = C.shift(k, C.shift(k, P3))
162  +W0 = Nat.add(Nat.add(cc, Nat.add(e, d)), f)
163  +s1 = Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(b, f)), Nat.add(Nat.add(Nat.add(Nat.mul(vlo, vml), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(Nat.add(Nat.add(a, cc), d), Nat.add(e, g)), Nat.add(b, f)),
164    Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(b, f)), Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(Nat.add(Nat.mul(vlo, vml), d), Nat.add(e, g)), WW.expand_k(k, vlo, vhi, vml, vmh)),
165    Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.add(z, d), Nat.add(e, g)), Nat.add(b, f)), Nat.mul(vlo, vml), Nat.add(a, cc), Equal.sym(Nat, Nat.add(a, cc), Nat.mul(vlo, vml), h1)))
166  +s2 = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, cc), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(a, b), Nat.add(W0, g)), Nat.add(Nat.add(L, C.shift(k, c)), Nat.add(W0, g)),
167    perm7(a, b, cc, d, e, f, g),
168    Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(W0, g)), Nat.add(a, b), Nat.add(L, C.shift(k, c)), h3))
169  +s3 = Equal.trans(Nat, Nat.add(Nat.add(L, C.shift(k, c)), Nat.add(W0, g)), Nat.add(L, Nat.add(Nat.add(W0, C.shift(k, c)), g)), Nat.add(L, C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(P2, P1)), vih), c), C.shift(k, P3)))),
170    swap3(L, C.shift(k, c), W0, g),
171    Equal.cong(Nat, Nat, z => Nat.add(L, z), Nat.add(Nat.add(W0, C.shift(k, c)), g), C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(P2, P1)), vih), c), C.shift(k, P3))),
172      Equal.sym(Nat, C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(P2, P1)), vih), c), C.shift(k, P3))), Nat.add(Nat.add(W0, C.shift(k, c)), g), shx(k, vh, P2, P1, vih, c, P3))))
173  Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(b, f)), Nat.add(Nat.add(Nat.add(Nat.add(a, cc), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(L, C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(P2, P1)), vih), c), C.shift(k, P3)))), s1,
174    Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, cc), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(L, C.shift(k, c)), Nat.add(W0, g)), Nat.add(L, C.shift(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(P2, P1)), vih), c), C.shift(k, P3)))), s2, s3))
175
176def eqm_of(+k: Nat, +v: Nat, +x: Nat, +e: {v == C.low(k, x) : Nat}) -> {C.low(k, v) == C.low(k, x) : Nat}:
177  Equal.trans(Nat, C.low(k, v), C.low(k, C.low(k, x)), C.low(k, x), Equal.cong(Nat, Nat, z => C.low(k, z), v, C.low(k, x), e), low_low(k, x))
178
179# the new high word is Z mod 2^64 (t, vH, u: the sums of the implementation)
180def high_word(+k: Nat, +vh: Nat, +p2: Nat, +p1: Nat, +p3: Nat, +vih: Nat, +c: Nat, +t: Nat, +vH: Nat, +u: Nat, +vH2: Nat, +hT: {C.low(k, t) == C.low(k, Nat.add(p2, p1)) : Nat}, +hH: {C.low(k, vH) == C.low(k, Nat.add(vh, t)) : Nat}, +hU: {C.low(k, u) == C.low(k, Nat.add(vH, vih)) : Nat}, +hV: {vH2 == C.low(k, Nat.add(u, c)) : Nat}) -> {C.low(k, Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(p2, p1)), vih), c), C.shift(k, p3))) == vH2 : Nat}:
181  +S = Nat.add(p2, p1)
182  +V = Nat.add(vh, S)
183  +W1 = Nat.add(V, vih)
184  +eH = Equal.trans(Nat, C.low(k, vH), C.low(k, Nat.add(vh, t)), C.low(k, V), hH, low_add(k, vh, vh, t, S, {==}, hT))
185  +eU = Equal.trans(Nat, C.low(k, u), C.low(k, Nat.add(vH, vih)), C.low(k, W1), hU, low_add(k, vH, V, vih, vih, eH, {==}))
186  +eZ = Equal.trans(Nat, C.low(k, Nat.add(Nat.add(W1, c), C.shift(k, p3))), C.low(k, Nat.add(W1, c)), C.low(k, Nat.add(u, c)),
187    WW.low_add_shift(k, Nat.add(W1, c), p3),
188    Equal.sym(Nat, C.low(k, Nat.add(u, c)), C.low(k, Nat.add(W1, c)), low_add(k, u, W1, c, c, eU, {==})))
189  Equal.trans(Nat, C.low(k, Nat.add(Nat.add(W1, c), C.shift(k, p3))), C.low(k, Nat.add(u, c)), vH2, eZ, Equal.sym(Nat, vH2, C.low(k, Nat.add(u, c)), hV))
190
191# THEOREM on values: the limb results are the LCG step mod 2^128 (the state
192# s, multiplier mul and increment inc given by their limbs)
193def step_value(+k: Nat, +vlo: Nat, +vhi: Nat, +vml: Nat, +vmh: Nat, +vil: Nat, +vih: Nat, +vl: Nat, +vh: Nat, +t: Nat, +vH: Nat, +u: Nat, +L: Nat, +c: Nat, +vH2: Nat, +s: Nat, +mul: Nat, +inc: Nat, +hs: {s == Nat.add(vlo, C.shift(k, vhi)) : Nat}, +hm: {mul == Nat.add(vml, C.shift(k, vmh)) : Nat}, +hi: {inc == Nat.add(vil, C.shift(k, vih)) : Nat}, +h1: {Nat.add(vl, C.shift(k, vh)) == Nat.mul(vlo, vml) : Nat}, +hT: {C.low(k, t) == C.low(k, Nat.add(Nat.mul(vhi, vml), Nat.mul(vlo, vmh))) : Nat}, +hH: {C.low(k, vH) == C.low(k, Nat.add(vh, t)) : Nat}, +hU: {C.low(k, u) == C.low(k, Nat.add(vH, vih)) : Nat}, +hV: {vH2 == C.low(k, Nat.add(u, c)) : Nat}, +h3: {Nat.add(vl, vil) == Nat.add(L, C.shift(k, c)) : Nat}, +hL: {C.fits(k, L) == True{} : Bool}, +hH2: {C.fits(k, vH2) == True{} : Bool}) -> {Nat.add(L, C.shift(k, vH2)) == C.low(Nat.add(k, k), Nat.add(Nat.mul(s, mul), inc)) : Nat}:
194  +p1 = Nat.mul(vlo, vmh)
195  +p2 = Nat.mul(vhi, vml)
196  +p3 = Nat.mul(vhi, vmh)
197  +Z = Nat.add(Nat.add(Nat.add(Nat.add(vh, Nat.add(p2, p1)), vih), c), C.shift(k, p3))
198  +SX = Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), Nat.add(vil, C.shift(k, vih)))
199  +SMI = Nat.add(Nat.mul(s, mul), inc)
200  +LS = Nat.add(L, C.shift(k, vH2))
201  +eS = Equal.trans(Nat, SMI, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), mul), inc), SX,
202    Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, mul), inc), s, Nat.add(vlo, C.shift(k, vhi)), hs),
203    Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), mul), inc), Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), inc), SX,
204      Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), z), inc), mul, Nat.add(vml, C.shift(k, vmh)), hm),
205      Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.add(vlo, C.shift(k, vhi)), Nat.add(vml, C.shift(k, vmh))), z), inc, Nat.add(vil, C.shift(k, vih)), hi)))
206  +eZ = Equal.trans(Nat, SMI, SX, Nat.add(L, C.shift(k, Z)), eS, expand(k, vlo, vhi, vml, vmh, vil, vih, vl, vh, L, c, h1, h3))
207  +hw = high_word(k, vh, p2, p1, p3, vih, c, t, vH, u, vH2, hT, hH, hU, hV)
208  +e1 = Equal.trans(Nat, C.low(Nat.add(k, k), SMI), C.low(Nat.add(k, k), Nat.add(L, C.shift(k, Z))), C.low(Nat.add(k, k), LS),
209    Equal.cong(Nat, Nat, z => C.low(Nat.add(k, k), z), SMI, Nat.add(L, C.shift(k, Z)), eZ),
210    low_hi(k, L, Z, vH2, Equal.sym(Nat, C.low(k, Z), vH2, hw)))
211  Equal.sym(Nat, C.low(Nat.add(k, k), SMI), LS, Equal.trans(Nat, C.low(Nat.add(k, k), SMI), C.low(Nat.add(k, k), LS), LS, e1, WW.low_fit(Nat.add(k, k), LS, WW.limbs_fit(k, k, L, vH2, hL, hH2))))