1 import Base 2 import ../../../../spec/lib/common.bend as C 3 import ../../../../spec/math/w64.bend as SW 4 import ../../../../spec/math/random/pcg.bend as SP 5 import ../../../../src/math/u64.bend as WU 6 import ../../../../src/math/w64.bend as X 7 import ../../../../src/math/random/pcg.bend as P 8 import ../../../lib/lemmas/spec/numeric.bend as S 9 import ../../../lib/lemmas/proofs/nat_algebra.bend as NA 10 import ../../../lib/u32alg.bend as A 11 import ../../typed/width.bend as WW 12 import ../../typed/w64add.bend as WA 13 import ../../typed/w64m128.bend as M128 14 import ../../typed/w64mul.bend as W64M 15 import ../../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 26 def 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 37 def 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 45 def 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 58 def 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 62 def 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) 84 def 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) 124 def 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 133 def 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) 151 def 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 176 def 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) 180 def 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) 193 def 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))))