proofs/math/random/pcg/impl.bend

bend-collections-laws-math@1.0.0.0 · 68 lines · 8 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
17import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as ST
18import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SR
19
20# The implementation's words of one PCG step against ST.main.
21
22def eqm_of(+v: Nat, +x: Nat, +e: {v == C.low(64n, x) : Nat}) -> {C.low(64n, v) == C.low(64n, x) : Nat}:
23  ST.eqm_of(64n, v, x, e)
24
25# ---- the implementation's words ----
26
27def v(+x: U32) -> Nat:
28  U32.to_nat(x)
29
30def carry_value(+c: Bool) -> {SW.value(WU.U64{X.b32(c), 0}) == S.bit_value(c) : Nat}:
31  Equal.trans(Nat, SW.value(WU.U64{X.b32(c), 0}), v(X.b32(c)), S.bit_value(c), SH.val0(X.b32(c)), W64M.b32_v(c))
32
33# the cross products mod 2^64
34def fT(+hi: WU.U64, +lo: WU.U64, +ml: WU.U64, +mh: WU.U64) -> {C.low(64n, SW.value(X.add(X.mul(hi, ml), X.mul(lo, mh)))) == C.low(64n, Nat.add(Nat.mul(SW.value(hi), SW.value(ml)), Nat.mul(SW.value(lo), SW.value(mh)))) : Nat}:
35  +m1 = X.mul(hi, ml)
36  +m2 = X.mul(lo, mh)
37  Equal.trans(Nat, C.low(64n, SW.value(X.add(m1, m2))), C.low(64n, Nat.add(SW.value(m1), SW.value(m2))), C.low(64n, Nat.add(Nat.mul(SW.value(hi), SW.value(ml)), Nat.mul(SW.value(lo), SW.value(mh)))),
38    eqm_of(SW.value(X.add(m1, m2)), Nat.add(SW.value(m1), SW.value(m2)), WA.add_value(m1, m2)),
39    ST.low_add(64n, SW.value(m1), Nat.mul(SW.value(hi), SW.value(ml)), SW.value(m2), Nat.mul(SW.value(lo), SW.value(mh)), eqm_of(SW.value(m1), Nat.mul(SW.value(hi), SW.value(ml)), WA.mul_value(hi, ml)), eqm_of(SW.value(m2), Nat.mul(SW.value(lo), SW.value(mh)), WA.mul_value(lo, mh))))
40
41# a sum mod 2^64
42def fS(+a: WU.U64, +b: WU.U64) -> {C.low(64n, SW.value(X.add(a, b))) == C.low(64n, Nat.add(SW.value(a), SW.value(b))) : Nat}:
43  eqm_of(SW.value(X.add(a, b)), Nat.add(SW.value(a), SW.value(b)), WA.add_value(a, b))
44
45# adding the carry
46def fV(+a: WU.U64, +cb: Bool) -> {SW.value(X.add(a, WU.U64{X.b32(cb), 0})) == C.low(64n, Nat.add(SW.value(a), S.bit_value(cb))) : Nat}:
47  Equal.trans(Nat, SW.value(X.add(a, WU.U64{X.b32(cb), 0})), C.low(64n, Nat.add(SW.value(a), SW.value(WU.U64{X.b32(cb), 0}))), C.low(64n, Nat.add(SW.value(a), S.bit_value(cb))),
48    WA.add_value(a, WU.U64{X.b32(cb), 0}),
49    Equal.cong(Nat, Nat, z => C.low(64n, Nat.add(SW.value(a), z)), SW.value(WU.U64{X.b32(cb), 0}), S.bit_value(cb), carry_value(cb)))
50
51# one step for any product pair (l, h) with l + 2^64 h == lo * ml (the pair
52# is abstract here, so the checker never unfolds the 128-bit product)
53def step_pair(+mh: WU.U64, +ml: WU.U64, +ih: WU.U64, +il: WU.U64, +hi: WU.U64, +lo: WU.U64, pr: WU.U64 & WU.U64, +h1: {Nat.add(SW.value(X.pfst(pr)), C.shift(64n, SW.value(X.psnd(pr)))) == Nat.mul(SW.value(lo), SW.value(ml)) : Nat}) -> {SR.value128(P.step_mul(mh, ml, ih, il, hi, lo, pr)) == C.low(Nat.add(64n, 64n), Nat.add(Nat.mul(SR.value128(P.P{hi, lo}), SR.value128(P.P{mh, ml})), SR.value128(P.P{ih, il}))) : Nat}:
54  match pr:
55    case Tuple{+l, +h}:
56      +T = X.add(X.mul(hi, ml), X.mul(lo, mh))
57      +H = X.add(h, T)
58      +H1 = X.add(H, ih)
59      +cb = X.add_over(l, il)
60      +H2 = X.add(H1, WU.U64{X.b32(cb), 0})
61      +L = X.add(l, il)
62      ST.step_value(64n, SW.value(lo), SW.value(hi), SW.value(ml), SW.value(mh), SW.value(il), SW.value(ih), SW.value(l), SW.value(h), SW.value(T), SW.value(H), SW.value(H1), SW.value(L), S.bit_value(cb), SW.value(H2), SR.value128(P.P{hi, lo}), SR.value128(P.P{mh, ml}), SR.value128(P.P{ih, il}), {==}, {==}, {==},
63        h1, fT(hi, lo, ml, mh), fS(h, T), fS(H, ih), fV(H1, cb), M128.add_split(l, il), M128.fit64(L), M128.fit64(H2))
64
65def m128(+a: WU.U64, +b: WU.U64) -> {Nat.add(SW.value(X.pfst(X.mul128(a, b))), C.shift(64n, SW.value(X.psnd(X.mul128(a, b))))) == Nat.mul(SW.value(a), SW.value(b)) : Nat}:
66  match a b:
67    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
68      M128.m128_value(al, ah, bl, bh)