1	# bend-osdev-u32: the arithmetic of Base's words as Nat arithmetic.
2	#
3	# This package has no word type of its own: its laws (LAWS.bend) are about
4	# Base's Word(n) and U32 operations, stated through their values
5	# (Word.to_nat, U32.to_nat): comparison is the order of the values, and
6	# addition, subtraction, increment and the shifts are the Nat operations on
7	# the values when nothing wraps, and the wrapping ones otherwise. Other
8	# packages' proofs use these laws instead of each proving them again.
9	#
10	# The defs below are the Nat functions the laws are stated with. None of
11	# them names a power of two as a closed number: 2^n is U32Nat.dbl(n, 1n),
12	# and 2^32 itself is never written out (see README.md, "Stating the
13	# bounds").
14	import Base
15	
16	# x times 2^n: x doubled n times
17	def U32Nat.dbl(n: Nat, x: Nat) -> Nat:
18	  match n:
19	    case 0n:
20	      x
21	    case 1n+p:
22	      Nat.double(U32Nat.dbl(p, x))
23	
24	# 1 for True, 0 for False
25	def U32Nat.bit(b: Bool) -> Nat:
26	  match b:
27	    case True{}:
28	      1n
29	    case False{}:
30	      0n
31	
32	# n / 2, rounded down
33	def U32Nat.half(n: Nat) -> Nat:
34	  match n:
35	    case 0n:
36	      0n
37	    case 1n+p:
38	      match p:
39	        case 0n:
40	          0n
41	        case 1n+q:
42	          1n+U32Nat.half(q)
43	
44	# x mod 2: 1 for an odd x, 0 for an even one
45	def U32Nat.odd(n: Nat) -> Nat:
46	  match n:
47	    case 0n:
48	      0n
49	    case 1n+p:
50	      match p:
51	        case 0n:
52	          1n
53	        case 1n+q:
54	          U32Nat.odd(q)
55	
56	# the low k bits of x (x mod 2^k), and the rest (x / 2^k, rounded down):
57	# x = low(k, x) + 2^k high(k, x)
58	def U32Nat.low(k: Nat, +x: Nat) -> Nat:
59	  match k:
60	    case 0n:
61	      0n
62	    case 1n+j:
63	      Nat.add(U32Nat.odd(x), Nat.double(U32Nat.low(j, U32Nat.half(x))))
64	
65	def U32Nat.high(k: Nat, x: Nat) -> Nat:
66	  match k:
67	    case 0n:
68	      x
69	    case 1n+j:
70	      U32Nat.high(j, U32Nat.half(x))
71	
72	# the word of width n whose low k bits are set (2^k - 1, for k <= n): the
73	# mask that U32.and(x, m) takes x's low k bits with
74	def U32Word.mask(n: Nat, k: Nat) -> Word(n):
75	  match n:
76	    case 0n:
77	      WNil{}
78	    case 1n+p:
79	      match k:
80	        case 0n:
81	          Word.zero(1n+p)
82	        case 1n+j:
83	          WCon{True{}, U32Word.mask(p, j)}