LAWS_bits.bend

bend-osdev-word64@0.1.1.0 · 49 lines · 8 definitions

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.
3import Base
4import bend-osdev-u32@0.1.0.0/u32.bend as U
5import bend-osdev-word64@0.1.1.0/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.
10law 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
15law 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
20law 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
25law 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
30law 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
35law 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
41law 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.
47law 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}