def low_hi

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:61

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

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))