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