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/random/pcg.bend as P
7	import ../../../lib/lemmas/spec/numeric.bend as S
8	import ../../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../../lib/word.bend as WD
10	import ../../../lib/u32div.bend as UD
11	import ../../../lib/logic.bend as L
12	import ../../typed/width.bend as WW
13	import ../../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	
19	def v(+x: U32) -> Nat:
20	  U32.to_nat(x)
21	
22	# the low bit and the rest of bv(b) + 2 u
23	def 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	
30	def 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
42	def 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
52	def 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	
64	def 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	
71	def 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
79	def 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
100	def 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)))