~/jendhub

proofs/math/random/pcg/xor.bend

bend-collections-laws-math@1.0.0.0 · 105 lines · 9 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/random/pcg.bend as P
7import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
8import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
11import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
14
15# Exclusive or on words against SP.xor_bits on their values: bit by bit on
16# a Word(n), then split at a limb boundary, then the two-limb U64 of
17# src/math/random/pcg.bend's xor64.
18
19def v(+x: U32) -> Nat:
20  U32.to_nat(x)
21
22# the low bit and the rest of bv(b) + 2 u
23def bit_bvd(+b: Bool, +u: Nat) -> {C.bit(Nat.add(S.bit_value(b), Nat.double(u))) == S.bit_value(b) : Nat}:
24  match b:
25    case True{}:
26      WW.bit_dbl(1n, u)
27    case False{}:
28      WW.bit_dbl(0n, u)
29
30def xbit(+a: Bool, +b: Bool) -> {S.bit_value(Bool.xor(a, b)) == SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))) : Nat}:
31  match a b:
32    case True{} True{}:
33      {==}
34    case True{} False{}:
35      {==}
36    case False{} True{}:
37      {==}
38    case False{} False{}:
39      {==}
40
41# one step of xor_bits on two values written bit + 2 rest
42def step_eq(+p: Nat, +ba: Bool, +ua: Nat, +bb: Bool, +ub: Nat) -> {SP.xor_bits(1n+p, Nat.add(S.bit_value(ba), Nat.double(ua)), Nat.add(S.bit_value(bb), Nat.double(ub))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}:
43  +A = Nat.add(S.bit_value(ba), Nat.double(ua))
44  +B = Nat.add(S.bit_value(bb), Nat.double(ub))
45  %Equal.sym(Nat, C.bit(A), S.bit_value(ba), bit_bvd(ba, ua)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(_, C.bit(B)))), Nat.double(SP.xor_bits(p, C.half(A), C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
46  %Equal.sym(Nat, C.bit(B), S.bit_value(bb), bit_bvd(bb, ub)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), _))), Nat.double(SP.xor_bits(p, C.half(A), C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
47  %Equal.sym(Nat, C.half(A), ua, SH.half_bv(ba, ua)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, _, C.half(B)))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
48  %Equal.sym(Nat, C.half(B), ub, SH.half_bv(bb, ub)) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, _))) == Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(ba), S.bit_value(bb)))), Nat.double(SP.xor_bits(p, ua, ub))) : Nat}
49  {==}
50
51# the value of a word xor is xor_bits of the values
52def xor_word(+n: Nat, +x: Word(n), +y: Word(n)) -> {WD.uw(n, Word.xor(n, x, y)) == SP.xor_bits(n, WD.uw(n, x), WD.uw(n, y)) : Nat}:
53  match n x y:
54    case 0n WNil{} WNil{}:
55      {==}
56    case 1n+p WCon{+a, +xt} WCon{+b, +yt}:
57      +M = Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))), Nat.double(SP.xor_bits(p, WD.uw(p, xt), WD.uw(p, yt))))
58      +e1 = Equal.trans(Nat, Nat.add(S.bit_value(Bool.xor(a, b)), Nat.double(WD.uw(p, Word.xor(p, xt, yt)))), Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))), Nat.double(WD.uw(p, Word.xor(p, xt, yt)))), M,
59        Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(WD.uw(p, Word.xor(p, xt, yt)))), S.bit_value(Bool.xor(a, b)), SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))), xbit(a, b)),
60        Equal.cong(Nat, Nat, z => Nat.add(SP.b2n(Bool.not(Nat.is_eq(S.bit_value(a), S.bit_value(b)))), Nat.double(z)), WD.uw(p, Word.xor(p, xt, yt)), SP.xor_bits(p, WD.uw(p, xt), WD.uw(p, yt)), xor_word(p, xt, yt)))
61      Equal.trans(Nat, Nat.add(S.bit_value(Bool.xor(a, b)), Nat.double(WD.uw(p, Word.xor(p, xt, yt)))), M, SP.xor_bits(1n+p, Nat.add(S.bit_value(a), Nat.double(WD.uw(p, xt))), Nat.add(S.bit_value(b), Nat.double(WD.uw(p, yt)))),
62        e1, Equal.sym(Nat, SP.xor_bits(1n+p, Nat.add(S.bit_value(a), Nat.double(WD.uw(p, xt))), Nat.add(S.bit_value(b), Nat.double(WD.uw(p, yt)))), M, step_eq(p, a, WD.uw(p, xt), b, WD.uw(p, yt))))
63
64def xor32(+x: U32, +y: U32) -> {v(U32.xor(x, y)) == SP.xor_bits(32n, v(x), v(y)) : Nat}:
65  match x y:
66    case U32{+wx} U32{+wy}:
67      %Equal.sym(Nat, v(U32{wx}), WD.uw(32n, wx), UD.vw(wx)) : {v(U32{Word.xor(32n, wx, wy)}) == SP.xor_bits(32n, _, v(U32{wy})) : Nat}
68      %Equal.sym(Nat, v(U32{wy}), WD.uw(32n, wy), UD.vw(wy)) : {v(U32{Word.xor(32n, wx, wy)}) == SP.xor_bits(32n, WD.uw(32n, wx), _) : Nat}
69      Equal.trans(Nat, v(U32{Word.xor(32n, wx, wy)}), WD.uw(32n, Word.xor(32n, wx, wy)), SP.xor_bits(32n, WD.uw(32n, wx), WD.uw(32n, wy)), UD.vw(Word.xor(32n, wx, wy)), xor_word(32n, wx, wy))
70
71def fits0(+a: Nat, +h: {C.fits(0n, a) == True{} : Bool}) -> {a == 0n : Nat}:
72  match a:
73    case 0n:
74      {==}
75    case 1n+q:
76      Empty.absurd({1n+q == 0n : Nat}, L.false_true(h))
77
78# xor_bits splits at bit k when the low parts fit k bits
79def xsplit(+k: Nat, +j: Nat, +al: Nat, +ah: Nat, +bl: Nat, +bh: Nat, +ha: {C.fits(k, al) == True{} : Bool}, +hb: {C.fits(k, bl) == True{} : Bool}) -> {SP.xor_bits(Nat.add(k, j), Nat.add(al, C.shift(k, ah)), Nat.add(bl, C.shift(k, bh))) == Nat.add(SP.xor_bits(k, al, bl), C.shift(k, SP.xor_bits(j, ah, bh))) : Nat}:
80  match k:
81    case 0n:
82      %Equal.sym(Nat, al, 0n, fits0(al, ha)) : {SP.xor_bits(j, Nat.add(_, ah), Nat.add(bl, bh)) == SP.xor_bits(j, ah, bh) : Nat}
83      %Equal.sym(Nat, bl, 0n, fits0(bl, hb)) : {SP.xor_bits(j, Nat.add(0n, ah), Nat.add(_, bh)) == SP.xor_bits(j, ah, bh) : Nat}
84      {==}
85    case 1n+p:
86      +A = Nat.add(al, Nat.double(C.shift(p, ah)))
87      +B = Nat.add(bl, Nat.double(C.shift(p, bh)))
88      +X = SP.xor_bits(j, ah, bh)
89      +Y = SP.xor_bits(p, C.half(al), C.half(bl))
90      +bx = SP.b2n(Bool.not(Nat.is_eq(C.bit(al), C.bit(bl))))
91      %Equal.sym(Nat, C.bit(A), C.bit(al), WW.bit_dbl(al, C.shift(p, ah))) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(_, C.bit(B)))), Nat.double(SP.xor_bits(Nat.add(p, j), C.half(A), C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
92      %Equal.sym(Nat, C.bit(B), C.bit(bl), WW.bit_dbl(bl, C.shift(p, bh))) : {Nat.add(SP.b2n(Bool.not(Nat.is_eq(C.bit(al), _))), Nat.double(SP.xor_bits(Nat.add(p, j), C.half(A), C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
93      %Equal.sym(Nat, C.half(A), Nat.add(C.half(al), C.shift(p, ah)), WW.half_dbl(al, C.shift(p, ah))) : {Nat.add(bx, Nat.double(SP.xor_bits(Nat.add(p, j), _, C.half(B)))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
94      %Equal.sym(Nat, C.half(B), Nat.add(C.half(bl), C.shift(p, bh)), WW.half_dbl(bl, C.shift(p, bh))) : {Nat.add(bx, Nat.double(SP.xor_bits(Nat.add(p, j), Nat.add(C.half(al), C.shift(p, ah)), _))) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
95      %Equal.sym(Nat, SP.xor_bits(Nat.add(p, j), Nat.add(C.half(al), C.shift(p, ah)), Nat.add(C.half(bl), C.shift(p, bh))), Nat.add(Y, C.shift(p, X)), xsplit(p, j, C.half(al), ah, C.half(bl), bh, ha, hb)) : {Nat.add(bx, Nat.double(_)) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
96      %Equal.sym(Nat, Nat.double(Nat.add(Y, C.shift(p, X))), Nat.add(Nat.double(Y), Nat.double(C.shift(p, X))), NA.double_add(Y, C.shift(p, X))) : {Nat.add(bx, _) == Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))) : Nat}
97      Equal.sym(Nat, Nat.add(Nat.add(bx, Nat.double(Y)), Nat.double(C.shift(p, X))), Nat.add(bx, Nat.add(Nat.double(Y), Nat.double(C.shift(p, X)))), NA.add_assoc(bx, Nat.double(Y), Nat.double(C.shift(p, X))))
98
99# THEOREM: the value of xor64 is xor_bits(64) of the values
100def xor64_value(+a: WU.U64, +b: WU.U64) -> {SW.value(P.xor64(a, b)) == SP.xor_bits(64n, SW.value(a), SW.value(b)) : Nat}:
101  match a b:
102    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
103      %Equal.sym(Nat, v(U32.xor(al, bl)), SP.xor_bits(32n, v(al), v(bl)), xor32(al, bl)) : {Nat.add(_, C.shift(32n, v(U32.xor(ah, bh)))) == SP.xor_bits(64n, Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))) : Nat}
104      %Equal.sym(Nat, v(U32.xor(ah, bh)), SP.xor_bits(32n, v(ah), v(bh)), xor32(ah, bh)) : {Nat.add(SP.xor_bits(32n, v(al), v(bl)), C.shift(32n, _)) == SP.xor_bits(64n, Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))) : Nat}
105      Equal.sym(Nat, SP.xor_bits(Nat.add(32n, 32n), Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(SP.xor_bits(32n, v(al), v(bl)), C.shift(32n, SP.xor_bits(32n, v(ah), v(bh)))), xsplit(32n, 32n, v(al), v(ah), v(bl), v(bh), SH.vb(al), SH.vb(bl)))