1	# The order of Nat and of Base's words: transitivity, reflexivity and
2	# antisymmetry, for Nat.is_lt and Nat.is_le (and x <= x + w), Word.cmp of
3	# every width n, and U32.cmp, U32.is_lt and U32.is_le. Other bend-osdev packages' proofs use
4	# these laws instead of each proving them again.
5	import Base
6	
7	# Nat
8	
9	law nat_le_trans:
10	  for +x: Nat
11	  for +y: Nat
12	  for +z: Nat
13	  for h1: {Nat.is_le(x, y) == True{} : Bool}
14	  for h2: {Nat.is_le(y, z) == True{} : Bool}
15	  {Nat.is_le(x, z) == True{} : Bool}
16	
17	law nat_lt_trans:
18	  for +x: Nat
19	  for +y: Nat
20	  for +z: Nat
21	  for h1: {Nat.is_lt(x, y) == True{} : Bool}
22	  for h2: {Nat.is_lt(y, z) == True{} : Bool}
23	  {Nat.is_lt(x, z) == True{} : Bool}
24	
25	law nat_lt_le_trans:
26	  for +x: Nat
27	  for +y: Nat
28	  for +z: Nat
29	  for h1: {Nat.is_lt(x, y) == True{} : Bool}
30	  for h2: {Nat.is_le(y, z) == True{} : Bool}
31	  {Nat.is_lt(x, z) == True{} : Bool}
32	
33	law nat_le_lt_trans:
34	  for +x: Nat
35	  for +y: Nat
36	  for +z: Nat
37	  for h1: {Nat.is_le(x, y) == True{} : Bool}
38	  for h2: {Nat.is_lt(y, z) == True{} : Bool}
39	  {Nat.is_lt(x, z) == True{} : Bool}
40	
41	law nat_le_add_r:
42	  for +x: Nat
43	  for +w: Nat
44	  {Nat.is_le(x, Nat.add(x, w)) == True{} : Bool}
45	
46	# Words of any width n
47	
48	law word_cmp_refl:
49	  for +n: Nat
50	  for +a: Word(n)
51	  {Word.cmp(n, a, a) == EQ{} : Cmp}
52	
53	law word_cmp_eq:
54	  for +n: Nat
55	  for +a: Word(n)
56	  for +b: Word(n)
57	  for e: {Word.cmp(n, a, b) == EQ{} : Cmp}
58	  {a == b : Word(n)}
59	
60	law word_cmp_lt_trans:
61	  for +n: Nat
62	  for +a: Word(n)
63	  for +b: Word(n)
64	  for +c: Word(n)
65	  for h1: {Word.cmp(n, a, b) == LT{} : Cmp}
66	  for h2: {Word.cmp(n, b, c) == LT{} : Cmp}
67	  {Word.cmp(n, a, c) == LT{} : Cmp}
68	
69	# U32
70	
71	law u32_cmp_refl:
72	  for +a: U32
73	  {U32.cmp(a, a) == EQ{} : Cmp}
74	
75	law u32_cmp_eq:
76	  for +a: U32
77	  for +b: U32
78	  for e: {U32.cmp(a, b) == EQ{} : Cmp}
79	  {a == b : U32}
80	
81	law u32_cmp_lt_trans:
82	  for +a: U32
83	  for +b: U32
84	  for +c: U32
85	  for h1: {U32.cmp(a, b) == LT{} : Cmp}
86	  for h2: {U32.cmp(b, c) == LT{} : Cmp}
87	  {U32.cmp(a, c) == LT{} : Cmp}
88	
89	law u32_le_refl:
90	  for +a: U32
91	  {U32.is_le(a, a) == True{} : Bool}
92	
93	law u32_lt_irrefl:
94	  for +a: U32
95	  for e: {U32.is_lt(a, a) == True{} : Bool}
96	  Empty
97	
98	law u32_lt_le:
99	  for +a: U32
100	  for +b: U32
101	  for e: {U32.is_lt(a, b) == True{} : Bool}
102	  {U32.is_le(a, b) == True{} : Bool}
103	
104	law u32_lt_trans:
105	  for +a: U32
106	  for +b: U32
107	  for +c: U32
108	  for h1: {U32.is_lt(a, b) == True{} : Bool}
109	  for h2: {U32.is_lt(b, c) == True{} : Bool}
110	  {U32.is_lt(a, c) == True{} : Bool}
111	
112	law u32_le_trans:
113	  for +a: U32
114	  for +b: U32
115	  for +c: U32
116	  for h1: {U32.is_le(a, b) == True{} : Bool}
117	  for h2: {U32.is_le(b, c) == True{} : Bool}
118	  {U32.is_le(a, c) == True{} : Bool}
119	
120	law u32_lt_le_trans:
121	  for +a: U32
122	  for +b: U32
123	  for +c: U32
124	  for h1: {U32.is_lt(a, b) == True{} : Bool}
125	  for h2: {U32.is_le(b, c) == True{} : Bool}
126	  {U32.is_lt(a, c) == True{} : Bool}
127	
128	law u32_le_lt_trans:
129	  for +a: U32
130	  for +b: U32
131	  for +c: U32
132	  for h1: {U32.is_le(a, b) == True{} : Bool}
133	  for h2: {U32.is_lt(b, c) == True{} : Bool}
134	  {U32.is_lt(a, c) == True{} : Bool}
135	
136	law u32_le_antisym:
137	  for +a: U32
138	  for +b: U32
139	  for h1: {U32.is_le(a, b) == True{} : Bool}
140	  for h2: {U32.is_le(b, a) == True{} : Bool}
141	  {a == b : U32}
142	
143	law u32_not_lt:
144	  for +a: U32
145	  for +b: U32
146	  for e: {U32.is_lt(a, b) == False{} : Bool}
147	  {U32.is_le(b, a) == True{} : Bool}
148	
149	law u32_not_le:
150	  for +a: U32
151	  for +b: U32
152	  for e: {U32.is_le(a, b) == False{} : Bool}
153	  {U32.is_lt(b, a) == True{} : Bool}
154	
155	law u32_lt_not_le:
156	  for +a: U32
157	  for +b: U32
158	  for e: {U32.is_lt(a, b) == True{} : Bool}
159	  {U32.is_le(b, a) == False{} : Bool}
160	
161	law u32_le_not_lt:
162	  for +a: U32
163	  for +b: U32
164	  for e: {U32.is_le(a, b) == True{} : Bool}
165	  {U32.is_lt(b, a) == False{} : Bool}