1	# bend-osdev-word64's laws of the bitwise operations and of the one-bit
2	# shift, for every input. Proved in PROOF_bits.bend.
3	import Base
4	import bend-osdev-u32@0.1.0.0/u32.bend as U
5	import ./word64.bend as W
6	
7	# The bits: and, or and xor commute; and + or is the sum of the values, and
8	# so is xor + 2 and; with no bit in common (and is 0), or is the sum; not is
9	# the subtraction from 2^64 - 1.
10	law and_comm:
11	  for +a: W.W64
12	  for +b: W.W64
13	  {W.W64.and(a, b) == W.W64.and(b, a) : W.W64}
14	
15	law or_comm:
16	  for +a: W.W64
17	  for +b: W.W64
18	  {W.W64.or(a, b) == W.W64.or(b, a) : W.W64}
19	
20	law xor_comm:
21	  for +a: W.W64
22	  for +b: W.W64
23	  {W.W64.xor(a, b) == W.W64.xor(b, a) : W.W64}
24	
25	law and_or:
26	  for +a: W.W64
27	  for +b: W.W64
28	  {Nat.add(W.W64.to_nat(W.W64.and(a, b)), W.W64.to_nat(W.W64.or(a, b))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
29	
30	law xor_and:
31	  for +a: W.W64
32	  for +b: W.W64
33	  {Nat.add(W.W64.to_nat(W.W64.xor(a, b)), Nat.double(W.W64.to_nat(W.W64.and(a, b)))) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
34	
35	law or_disjoint:
36	  for +a: W.W64
37	  for +b: W.W64
38	  for h: {W.W64.and(a, b) == W.W64.zero() : W.W64}
39	  {W.W64.to_nat(W.W64.or(a, b)) == Nat.add(W.W64.to_nat(a), W.W64.to_nat(b)) : Nat}
40	
41	law not_sub:
42	  for +a: W.W64
43	  {W.W64.not(a) == W.W64.sub(W.W64.max(), a) : W.W64}
44	
45	# A shift left by one bit: twice the value, less 2^64 for the top bit (bit
46	# 31 of the high half) going out.
47	law shl_one_wrap:
48	  for +a: W.W64
49	  {Nat.add(W.W64.to_nat(W.W64.shl(a, 1n)), U.U32Nat.dbl(64n, U32.to_nat(U32.shrn(W.W64.hi(a), 31n)))) == Nat.double(W.W64.to_nat(a)) : Nat}