1	# The edge cases of 64-bit arithmetic, as vectors: wrapping at 2^64, the two
2	# 32-bit halves, shifts across the halves, a multiply that overflows, and the
3	# text forms. 0xDEADBEEF = 3735928559, 0xCAFEBABE = 3405691582.
4	import Base
5	import ./word64.bend as W
6	
7	law add_wraps:
8	  {W.W64.add(W.W64.max(), W.W64.one()) == W.W64.zero() : W.W64}
9	
10	law sub_wraps:
11	  {W.W64.sub(W.W64.zero(), W.W64.one()) == W.W64.max() : W.W64}
12	
13	law hi_of_parts:
14	  {W.W64.hi(W.W64.from_parts(3735928559, 3405691582)) == 3735928559 : U32}
15	
16	law lo_of_parts:
17	  {W.W64.lo(W.W64.from_parts(3735928559, 3405691582)) == 3405691582 : U32}
18	
19	law shl_crosses_halves:
20	  {W.W64.shl(W.W64.one(), 32n) == W.W64.from_parts(1, 0) : W.W64}
21	
22	law shr_crosses_halves:
23	  {W.W64.shr(W.W64.from_parts(1, 0), 1n) == W.W64.from_parts(0, 2147483648) : W.W64}
24	
25	# (2^32 - 1)^2 = 2^64 - 2^33 + 1
26	law mul_of_max_halves:
27	  {W.W64.mul(W.W64.from_u32(4294967295), W.W64.from_u32(4294967295)) == W.W64.from_parts(4294967294, 1) : W.W64}
28	
29	law show_max:
30	  {W.W64.show(W.W64.max()) == "18446744073709551615" : String}
31	
32	law show_hex_parts:
33	  {W.W64.show_hex(W.W64.from_parts(3735928559, 3405691582)) == "deadbeefcafebabe" : String}
34	
35	law show_hex_zero:
36	  {W.W64.show_hex(W.W64.zero()) == "0000000000000000" : String}
37	
38	# For every 32-bit a: from_u32 then lo gives a back.
39	law lo_from_u32:
40	  for a: U32
41	  {W.W64.lo(W.W64.from_u32(a)) == a : U32}
42	
43	# For every pair of halves: splitting the joined word gives them back.
44	law hi_from_parts:
45	  for h: U32
46	  for l: U32
47	  {W.W64.hi(W.W64.from_parts(h, l)) == h : U32}
48	
49	law lo_from_parts:
50	  for h: U32
51	  for l: U32
52	  {W.W64.lo(W.W64.from_parts(h, l)) == l : U32}
53	
54	# Interface law: a word is its two halves joined (for every word). Other
55	# packages' proofs use this instead of looking inside W64.
56	law parts_of:
57	  for v: W.W64
58	  {W.W64.from_parts(W.W64.hi(v), W.W64.lo(v)) == v : W.W64}