1	import Base
2	import ./LAWS.bend as L
3	import ./proof_nat.bend as N
4	import ./proof_u32.bend as U
5	import ./proof_bytes.bend as Y
6	import ./proof_zb.bend as Z
7	
8	# Proofs of the laws of LAWS.bend: `def L.name` proves `law name`. Each
9	# forwards to the proof file that restates the law with every variable
10	# reusable: proof_nat.bend (Nat), proof_word.bend (Word(n), used by the
11	# others), proof_u32.bend (U32), proof_bytes.bend (bytes in a word),
12	# proof_zb.bend (the zero-byte test).
13	
14	# Numbers
15	# =======
16	
17	def L.to_nat_lt(a):
18	  U.to_nat_lt_p(a)
19	
20	def L.to_nat_from_nat(n):
21	  U.to_nat_from_nat_p(n)
22	
23	def L.wrap_small(n, h):
24	  U.wrap_small_p(n, h)
25	
26	def L.to_nat_inc(a):
27	  U.to_nat_inc_p(a)
28	
29	def L.to_nat_add(a, b):
30	  U.to_nat_add_p(a, b)
31	
32	def L.to_nat_sub(a, b):
33	  U.to_nat_sub_p(a, b)
34	
35	def L.to_nat_mul(a, b):
36	  U.to_nat_mul_p(a, b)
37	
38	def L.to_nat_add_fits(a, b, h):
39	  U.to_nat_add_fits_p(a, b, h)
40	
41	def L.to_nat_mul_fits(a, b, h):
42	  U.to_nat_mul_fits_p(a, b, h)
43	
44	def L.to_nat_shl(a):
45	  U.to_nat_shl_p(a)
46	
47	def L.to_nat_shln(a, k):
48	  U.to_nat_shln_p(a, k)
49	
50	def L.to_nat_shln_fits(a, k, h):
51	  U.to_nat_shln_fits_p(a, k, h)
52	
53	def L.to_nat_not(a):
54	  U.to_nat_not_p(a)
55	
56	def L.to_nat_inj(a, b, h):
57	  U.to_nat_inj(a, b, h)
58	
59	def L.from_nat_to_nat(a):
60	  U.from_nat_to_nat(a)
61	
62	# Comparisons
63	# ===========
64	
65	def L.cmp_to_nat(a, b):
66	  U.cmp_to_nat(a, b)
67	
68	def L.is_eq_to_nat(a, b):
69	  U.is_eq_to_nat(a, b)
70	
71	def L.is_lt_to_nat(a, b):
72	  U.is_lt_to_nat(a, b)
73	
74	def L.is_le_to_nat(a, b):
75	  U.is_le_to_nat(a, b)
76	
77	def L.is_gt_to_nat(a, b):
78	  U.is_gt_to_nat(a, b)
79	
80	def L.is_ge_to_nat(a, b):
81	  U.is_ge_to_nat(a, b)
82	
83	def L.is_ne_to_nat(a, b):
84	  U.is_ne_to_nat(a, b)
85	
86	def L.is_zero_to_nat(a):
87	  U.is_zero_to_nat(a)
88	
89	def L.is_zero_xor(a, b):
90	  U.is_zero_xor(a, b)
91	
92	def L.is_eq_true(a, b, h):
93	  U.is_eq_true(a, b, h)
94	
95	# Arithmetic modulo 2^32
96	# ======================
97	
98	def L.from_nat_add(x, y):
99	  U.from_nat_add(x, y)
100	
101	def L.from_nat_mul(x, y):
102	  U.from_nat_mul(x, y)
103	
104	# Arithmetic when the result fits
105	# ===============================
106	
107	def L.to_nat_inc_lt(a, b, h):
108	  U.to_nat_inc_lt(a, b, h)
109	
110	def L.to_nat_sub_le(a, b, h):
111	  U.to_nat_sub_le(a, b, h)
112	
113	# Division, remainder, minimum, maximum
114	# =====================================
115	
116	def L.to_nat_div(a, b):
117	  U.to_nat_div(a, b)
118	
119	def L.to_nat_mod(a, b):
120	  U.to_nat_mod(a, b)
121	
122	def L.to_nat_min(a, b):
123	  U.to_nat_min(a, b)
124	
125	def L.to_nat_max(a, b):
126	  U.to_nat_max(a, b)
127	
128	# Shifts
129	# ======
130	
131	def L.to_nat_shr(a):
132	  U.to_nat_shr(a)
133	
134	def L.to_nat_shrn(a, k):
135	  U.to_nat_shrn(a, k)
136	
137	def L.to_nat_shln_mod(a, k):
138	  U.to_nat_shln_mod(a, k)
139	
140	def L.to_nat_shrn_lt(a, k):
141	  U.to_nat_shrn_lt(a, k)
142	
143	# Indexes
144	# =======
145	
146	def L.to_nat_split(a, m, k, h):
147	  U.to_nat_split(a, m, k, h)
148	
149	def L.shrn_lt_words(i, w, k, h):
150	  U.shrn_lt_words(i, w, k, h)
151	
152	# Bitwise operations as numbers
153	# =============================
154	
155	def L.to_nat_and_mask(a, m, k, h):
156	  U.to_nat_and_mask(a, m, k, h)
157	
158	def L.to_nat_or_split(a, b, k, ha, hb):
159	  U.to_nat_or_split(a, b, k, ha, hb)
160	
161	def L.to_nat_xor_split(a, b, k, ha, hb):
162	  U.to_nat_xor_split(a, b, k, ha, hb)
163	
164	# Bitwise operations bit by bit
165	# =============================
166	
167	def L.bit_and(a, b, k):
168	  U.bit_and(a, b, k)
169	
170	def L.bit_or(a, b, k):
171	  U.bit_or(a, b, k)
172	
173	def L.bit_xor(a, b, k):
174	  U.bit_xor(a, b, k)
175	
176	def L.bit_not(a, k):
177	  U.bit_not(a, k)
178	
179	def L.bit_ext(a, b, h):
180	  U.bit_ext(a, b, h)
181	
182	# Bytes in a word
183	# ===============
184	
185	def L.to_nat_byte(w, j):
186	  Y.to_nat_byte(w, j)
187	
188	def L.byte_put_same(w, j, b, hj, hb):
189	  Y.byte_put_same(w, j, b, hj, hb)
190	
191	def L.byte_put_other(w, i, j, b, hb, hij):
192	  Y.byte_put_other(w, i, j, b, hb, hij)
193	
194	def L.to_nat_pack4(b0, b1, b2, b3, h0, h1, h2, h3):
195	  Y.to_nat_pack4(b0, b1, b2, b3, h0, h1, h2, h3)
196	
197	def L.byte_pack4(b0, b1, b2, b3, j, h0, h1, h2, h3, hj):
198	  Y.byte_pack4(b0, b1, b2, b3, j, h0, h1, h2, h3, hj)
199	
200	def L.pack4_bytes(w):
201	  Y.pack4_bytes(w)
202	
203	def L.byte_ext(a, b, h0, h1, h2, h3):
204	  Y.byte_ext(a, b, h0, h1, h2, h3)
205	
206	def L.byte_and(a, b, j):
207	  Y.byte_and(a, b, j)
208	
209	def L.byte_or(a, b, j):
210	  Y.byte_or(a, b, j)
211	
212	def L.byte_xor(a, b, j):
213	  Y.byte_xor(a, b, j)
214	
215	def L.byte_not(a, j, hj):
216	  Y.byte_not(a, j, hj)
217	
218	def L.byte_shrn(w, s, j):
219	  Y.byte_shrn(w, s, j)
220	
221	def L.byte_shln_high(w, s, j, hs, hj):
222	  Y.byte_shln_high(w, s, j, hs, hj)
223	
224	def L.byte_shln_low(w, s, j, hj):
225	  Y.byte_shln_low(w, s, j, hj)
226	
227	def L.byte_merge_lo(lo, hi, r, j, h):
228	  Y.byte_merge_lo(lo, hi, r, j, h)
229	
230	def L.byte_merge_hi(lo, hi, r, j, hr, hj, h):
231	  Y.byte_merge_hi(lo, hi, r, j, hr, hj, h)
232	
233	def L.zb_zero(v):
234	  Z.zb_zero(v)
235	
236	def L.byte_lt(w, j):
237	  Y.byte_lt(w, j)
238	
239	# Facts about Nat
240	# ===============
241	
242	def L.nat_mod_lt(a, b, h):
243	  N.mod_lt(a, b, h)
244	
245	def L.nat_mod_small(a, b, h):
246	  N.mod_small(a, b, h)
247	
248	def L.nat_div_small(a, b, h):
249	  N.div_small(a, b, h)
250	
251	def L.nat_div_mod(a, b):
252	  N.div_mod(a, b)
253	
254	def L.nat_pow_add(b, j, k):
255	  N.pow_add(b, j, k)
256	
257	def L.nat_div_div(a, x, y):
258	  N.div_div(a, x, y)
259	
260	def L.nat_add_comm(a, b):
261	  N.add_comm(a, b)
262	
263	def L.nat_add_assoc(a, b, c):
264	  N.add_assoc(a, b, c)
265	
266	def L.nat_mul_comm(a, b):
267	  N.mul_comm(a, b)
268	
269	def L.nat_mul_assoc(a, b, c):
270	  N.mul_assoc(a, b, c)
271	
272	def L.nat_mul_add(a, b, c):
273	  N.mul_add(a, b, c)
274	
275	def L.nat_lt_le_trans(a, b, c, h1, h2):
276	  N.lt_le_trans(a, b, c, h1, h2)
277	
278	def L.nat_le_trans(a, b, c, h1, h2):
279	  N.le_trans(a, b, c, h1, h2)
280	
281	def L.nat_div_lt(a, b, c, hb, h):
282	  N.div_lt(a, b, c, hb, h)
283	
284	def L.nat_div_mul_add(q, b, r, h):
285	  N.div_mul_add(q, b, r, h)
286	
287	def L.nat_mod_mul_add(q, b, r, h):
288	  N.mod_mul_add(q, b, r, h)
289	
290	def L.nat_mul_mod(a, b):
291	  N.mul_mod(a, b)
292	
293	def L.nat_mod_mod_pow(a, k, m, h):
294	  N.mod_mod_pow(a, k, m, h)