LAWS.bend
lawful-bytes@0.1.0.0 · 490 lines · 0 definitions
1import Base
2import lawful-bytes@0.1.0.0/defs.bend as D
3import lawful-bytes@0.1.0.0/bytes.bend as B
4import lawful-bytes@0.1.0.0/fast.bend as FA
5
6# lawful-bytes: bytes packed four to a word in an Array<U32> block. Every law
7# describes an operation by what it does to the list of bytes a Bytes holds
8# (D.view). Hypotheses D.ok(b, d) say b is well formed with a block of 2^d
9# words; every operation keeps it so.
10
11# ==========================================================================
12# What a Bytes holds
13# ==========================================================================
14
15law view_size:
16 for b: D.Bytes
17 for d: Nat
18 for h: {D.ok(b, d) == True{} : Bool}
19 {List.length(&2, U32, D.view(b)) == D.size(b) : Nat}
20
21law view_bytes:
22 for b: D.Bytes
23 {D.all_bytes(D.view(b)) == True{} : Bool}
24
25law cap_ok:
26 for b: D.Bytes
27 for d: Nat
28 for h: {D.ok(b, d) == True{} : Bool}
29 {D.cap(b) == Nat.mul(4n, Nat.pow(2n, d)) : Nat}
30
31# ==========================================================================
32# Making
33# ==========================================================================
34
35law empty_view:
36 for d: Nat
37 {D.view(B.empty(d)) == Nil{} : List<&2, U32>}
38
39law empty_ok:
40 for d: Nat
41 for hd: {Nat.is_le(d, 29n) == True{} : Bool}
42 {D.ok(B.empty(d), d) == True{} : Bool}
43
44# grow keeps the bytes in a larger block.
45law grow_view:
46 for b: D.Bytes
47 for d: Nat
48 for e: Nat
49 for h: {D.ok(b, d) == True{} : Bool}
50 for he: {Nat.is_le(d, e) == True{} : Bool}
51 for he29: {Nat.is_le(e, 29n) == True{} : Bool}
52 {D.view(B.grow(b, e)) == D.view(b) : List<&2, U32>}
53
54law grow_ok:
55 for b: D.Bytes
56 for d: Nat
57 for e: Nat
58 for h: {D.ok(b, d) == True{} : Bool}
59 for he: {Nat.is_le(d, e) == True{} : Bool}
60 for he29: {Nat.is_le(e, 29n) == True{} : Bool}
61 {D.ok(B.grow(b, e), e) == True{} : Bool}
62
63# ==========================================================================
64# Reading
65# ==========================================================================
66
67law at_view:
68 for b: D.Bytes
69 for d: Nat
70 for i: U32
71 for h: {D.ok(b, d) == True{} : Bool}
72 for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
73 {Some{Pair.snd(D.Bytes, U32, B.at(b, i))} == List.get(&2, U32, D.view(b), U32.to_nat(i)) : Maybe<&2, U32>}
74
75# The result as a literal pair: the same Bytes and the value (for rewriting).
76law at_pair:
77 for b: D.Bytes
78 for i: U32
79 {B.at(b, i) == (b, Pair.snd(D.Bytes, U32, B.at(b, i))) : D.Bytes & U32}
80
81# find answers the first index in from .. to-1 holding c, or to. c must be a
82# byte value: a word-at-a-time search compares 8 bits per byte.
83law find_view:
84 for b: D.Bytes
85 for d: Nat
86 for from: U32
87 for to: U32
88 for c: U32
89 for h: {D.ok(b, d) == True{} : Bool}
90 for hft: {U32.is_le(from, to) == True{} : Bool}
91 for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
92 for hc: {U32.is_lt(c, 256) == True{} : Bool}
93 {U32.to_nat(Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) == D.first(D.view(b), U32.to_nat(from), U32.to_nat(to), c) : Nat}
94
95# The result as a literal pair: the same Bytes and the value (for rewriting).
96law find_pair:
97 for b: D.Bytes
98 for from: U32
99 for to: U32
100 for c: U32
101 {B.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, B.find(b, from, to, c))) : D.Bytes & U32}
102
103law find2_view:
104 for b: D.Bytes
105 for d: Nat
106 for from: U32
107 for to: U32
108 for c1: U32
109 for c2: U32
110 for h: {D.ok(b, d) == True{} : Bool}
111 for hft: {U32.is_le(from, to) == True{} : Bool}
112 for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
113 for hc1: {U32.is_lt(c1, 256) == True{} : Bool}
114 for hc2: {U32.is_lt(c2, 256) == True{} : Bool}
115 {U32.to_nat(Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) == D.first2(D.view(b), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
116
117# The result as a literal pair: the same Bytes and the value (for rewriting).
118law find2_pair:
119 for b: D.Bytes
120 for from: U32
121 for to: U32
122 for c1: U32
123 for c2: U32
124 {B.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, B.find2(b, from, to, c1, c2))) : D.Bytes & U32}
125
126# same compares two ranges of equal length, n bytes each.
127law same_view:
128 for a: D.Bytes
129 for b: D.Bytes
130 for d: Nat
131 for e: Nat
132 for i: U32
133 for j: U32
134 for n: U32
135 for ha: {D.ok(a, d) == True{} : Bool}
136 for hb: {D.ok(b, e) == True{} : Bool}
137 for hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(a)) == True{} : Bool}
138 for hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}
139 {Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))) == D.list_eq(D.slice(D.view(a), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}
140
141# same hands both buffers back (as a literal tuple, for rewriting).
142law same_pair:
143 for a: D.Bytes
144 for b: D.Bytes
145 for i: U32
146 for j: U32
147 for n: U32
148 {B.same(a, i, b, j, n) == (a, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}
149
150# ==========================================================================
151# Writing
152# ==========================================================================
153
154law set_view:
155 for b: D.Bytes
156 for d: Nat
157 for i: U32
158 for v: U32
159 for h: {D.ok(b, d) == True{} : Bool}
160 for hi: {Nat.is_lt(U32.to_nat(i), D.size(b)) == True{} : Bool}
161 for hv: {U32.is_lt(v, 256) == True{} : Bool}
162 {D.view(B.set(b, i, v)) == List.set(&2, U32, D.view(b), U32.to_nat(i), v) : List<&2, U32>}
163
164law set_ok:
165 for b: D.Bytes
166 for d: Nat
167 for i: U32
168 for v: U32
169 for h: {D.ok(b, d) == True{} : Bool}
170 {D.ok(B.set(b, i, v), d) == True{} : Bool}
171
172law push_view:
173 for b: D.Bytes
174 for d: Nat
175 for v: U32
176 for h: {D.ok(b, d) == True{} : Bool}
177 for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
178 for hv: {U32.is_lt(v, 256) == True{} : Bool}
179 {D.view(B.push(b, v)) == List.append(&2, U32, D.view(b), [v]) : List<&2, U32>}
180
181law push_ok:
182 for b: D.Bytes
183 for d: Nat
184 for v: U32
185 for h: {D.ok(b, d) == True{} : Bool}
186 for hc: {Nat.is_lt(D.size(b), D.cap(b)) == True{} : Bool}
187 {D.ok(B.push(b, v), d) == True{} : Bool}
188
189# append adds n bytes of src, from s, at the end of dst.
190law append_view:
191 for dst: D.Bytes
192 for src: D.Bytes
193 for d: Nat
194 for e: Nat
195 for s: U32
196 for n: U32
197 for hd: {D.ok(dst, d) == True{} : Bool}
198 for he: {D.ok(src, e) == True{} : Bool}
199 for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}
200 for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
201 {D.view(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
202
203law append_ok:
204 for dst: D.Bytes
205 for src: D.Bytes
206 for d: Nat
207 for s: U32
208 for n: U32
209 for hd: {D.ok(dst, d) == True{} : Bool}
210 for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
211 {D.ok(Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), d) == True{} : Bool}
212
213# append hands src back (as a literal pair, for rewriting).
214law append_pair:
215 for dst: D.Bytes
216 for src: D.Bytes
217 for s: U32
218 for n: U32
219 {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}
220
221# ==========================================================================
222# Length, capacity, trimming
223# ==========================================================================
224
225law len_view:
226 for b: D.Bytes
227 {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(b))) == D.size(b) : Nat}
228
229law len_pair:
230 for b: D.Bytes
231 {B.len(b) == (b, Pair.snd(D.Bytes, U32, B.len(b))) : D.Bytes & U32}
232
233law capacity_view:
234 for b: D.Bytes
235 for d: Nat
236 for h: {D.ok(b, d) == True{} : Bool}
237 {U32.to_nat(Pair.snd(D.Bytes, U32, B.capacity(b))) == D.cap(b) : Nat}
238
239law capacity_pair:
240 for b: D.Bytes
241 {B.capacity(b) == (b, Pair.snd(D.Bytes, U32, B.capacity(b))) : D.Bytes & U32}
242
243law truncate_view:
244 for b: D.Bytes
245 for n: U32
246 for h: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}
247 {D.view(B.truncate(b, n)) == List.take(&2, U32, D.view(b), U32.to_nat(n)) : List<&2, U32>}
248
249law truncate_ok:
250 for b: D.Bytes
251 for d: Nat
252 for n: U32
253 for h: {D.ok(b, d) == True{} : Bool}
254 for hn: {Nat.is_le(U32.to_nat(n), D.size(b)) == True{} : Bool}
255 {D.ok(B.truncate(b, n), d) == True{} : Bool}
256
257# shift drops the first k bytes and moves the rest to the start (for reusing a
258# buffer when reading a stream in pieces).
259law shift_view:
260 for b: D.Bytes
261 for d: Nat
262 for k: U32
263 for h: {D.ok(b, d) == True{} : Bool}
264 for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
265 {D.view(B.shift(b, k)) == List.drop(&2, U32, D.view(b), U32.to_nat(k)) : List<&2, U32>}
266
267law shift_ok:
268 for b: D.Bytes
269 for d: Nat
270 for k: U32
271 for h: {D.ok(b, d) == True{} : Bool}
272 for hk: {Nat.is_le(U32.to_nat(k), D.size(b)) == True{} : Bool}
273 {D.ok(B.shift(b, k), d) == True{} : Bool}
274
275# ==========================================================================
276# Lists (Base's file reads and writes use List<U32>)
277# ==========================================================================
278
279law of_list_view:
280 for d: Nat
281 for xs: List<&2, U32>
282 for hd: {Nat.is_le(d, 29n) == True{} : Bool}
283 for hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
284 for hb: {D.all_bytes(xs) == True{} : Bool}
285 {D.view(B.of_list(d, xs)) == xs : List<&2, U32>}
286
287law of_list_ok:
288 for d: Nat
289 for xs: List<&2, U32>
290 for hd: {Nat.is_le(d, 29n) == True{} : Bool}
291 for hn: {Nat.is_le(List.length(&2, U32, xs), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
292 {D.ok(B.of_list(d, xs), d) == True{} : Bool}
293
294law to_list_view:
295 for b: D.Bytes
296 for d: Nat
297 for s: U32
298 for n: U32
299 for h: {D.ok(b, d) == True{} : Bool}
300 for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(b)) == True{} : Bool}
301 {Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n)) == D.slice(D.view(b), U32.to_nat(s), U32.to_nat(n)) : List<&2, U32>}
302
303law to_list_pair:
304 for b: D.Bytes
305 for s: U32
306 for n: U32
307 {B.to_list(b, s, n) == (b, Pair.snd(D.Bytes, List<&2, U32>, B.to_list(b, s, n))) : D.Bytes & List<&2, U32>}
308
309# ==========================================================================
310# Comparing two ranges of one buffer
311# ==========================================================================
312
313law same1_view:
314 for b: D.Bytes
315 for d: Nat
316 for i: U32
317 for j: U32
318 for n: U32
319 for h: {D.ok(b, d) == True{} : Bool}
320 for hi: {Nat.is_le(Nat.add(U32.to_nat(i), U32.to_nat(n)), D.size(b)) == True{} : Bool}
321 for hj: {Nat.is_le(Nat.add(U32.to_nat(j), U32.to_nat(n)), D.size(b)) == True{} : Bool}
322 {Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n)) == D.list_eq(D.slice(D.view(b), U32.to_nat(i), U32.to_nat(n)), D.slice(D.view(b), U32.to_nat(j), U32.to_nat(n))) : Bool}
323
324law same1_pair:
325 for b: D.Bytes
326 for i: U32
327 for j: U32
328 for n: U32
329 {B.same1(b, i, j, n) == (b, Pair.snd(D.Bytes, Bool, B.same1(b, i, j, n))) : D.Bytes & Bool}
330
331# ==========================================================================
332# Facts about the search and comparison definitions (for proofs of parsers)
333# ==========================================================================
334
335law first_range:
336 for xs: List<&2, U32>
337 for from: Nat
338 for to: Nat
339 for c: U32
340 for hft: {Nat.is_le(from, to) == True{} : Bool}
341 for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
342 {(Nat.is_le(from, D.first(xs, from, to, c)) && Nat.is_le(D.first(xs, from, to, c), to)) == True{} : Bool}
343
344# Below to, the answer holds c.
345law first_hit:
346 for xs: List<&2, U32>
347 for from: Nat
348 for to: Nat
349 for c: U32
350 for hft: {Nat.is_le(from, to) == True{} : Bool}
351 for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
352 for hlt: {Nat.is_lt(D.first(xs, from, to, c), to) == True{} : Bool}
353 {D.has(xs, D.first(xs, from, to, c), c) == True{} : Bool}
354
355# No index from from up to the answer holds c.
356law first_miss:
357 for xs: List<&2, U32>
358 for from: Nat
359 for to: Nat
360 for c: U32
361 for k: Nat
362 for hk1: {Nat.is_le(from, k) == True{} : Bool}
363 for hk2: {Nat.is_lt(k, D.first(xs, from, to, c)) == True{} : Bool}
364 {D.has(xs, k, c) == False{} : Bool}
365
366law first2_range:
367 for xs: List<&2, U32>
368 for from: Nat
369 for to: Nat
370 for c1: U32
371 for c2: U32
372 for hft: {Nat.is_le(from, to) == True{} : Bool}
373 for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
374 {(Nat.is_le(from, D.first2(xs, from, to, c1, c2)) && Nat.is_le(D.first2(xs, from, to, c1, c2), to)) == True{} : Bool}
375
376law first2_hit:
377 for xs: List<&2, U32>
378 for from: Nat
379 for to: Nat
380 for c1: U32
381 for c2: U32
382 for hft: {Nat.is_le(from, to) == True{} : Bool}
383 for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
384 for hlt: {Nat.is_lt(D.first2(xs, from, to, c1, c2), to) == True{} : Bool}
385 {D.has2(xs, D.first2(xs, from, to, c1, c2), c1, c2) == True{} : Bool}
386
387law first2_miss:
388 for xs: List<&2, U32>
389 for from: Nat
390 for to: Nat
391 for c1: U32
392 for c2: U32
393 for k: Nat
394 for hk1: {Nat.is_le(from, k) == True{} : Bool}
395 for hk2: {Nat.is_lt(k, D.first2(xs, from, to, c1, c2)) == True{} : Bool}
396 {D.has2(xs, k, c1, c2) == False{} : Bool}
397
398# A passed list_eq test gives equal lists.
399law list_eq_true:
400 for xs: List<&2, U32>
401 for ys: List<&2, U32>
402 for h: {D.list_eq(xs, ys) == True{} : Bool}
403 {xs == ys : List<&2, U32>}
404
405# Equal lists pass list_eq.
406law list_eq_refl:
407 for xs: List<&2, U32>
408 {D.list_eq(xs, xs) == True{} : Bool}
409
410# ==========================================================================
411# Fast versions (fast.bend: a word at a time)
412# ==========================================================================
413
414# The word-at-a-time find gives exactly the reference result (the same Bytes
415# and the same index). c must be a byte value: the search compares 8 bits per
416# byte.
417law fast_find:
418 for b: D.Bytes
419 for d: Nat
420 for from: U32
421 for to: U32
422 for c: U32
423 for h: {D.ok(b, d) == True{} : Bool}
424 for hft: {U32.is_le(from, to) == True{} : Bool}
425 for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
426 for hc: {U32.is_lt(c, 256) == True{} : Bool}
427 {FA.find(b, from, to, c) == B.find(b, from, to, c) : D.Bytes & U32}
428
429law fast_find2:
430 for b: D.Bytes
431 for d: Nat
432 for from: U32
433 for to: U32
434 for c1: U32
435 for c2: U32
436 for h: {D.ok(b, d) == True{} : Bool}
437 for hft: {U32.is_le(from, to) == True{} : Bool}
438 for ht: {Nat.is_le(U32.to_nat(to), D.size(b)) == True{} : Bool}
439 for hc1: {U32.is_lt(c1, 256) == True{} : Bool}
440 for hc2: {U32.is_lt(c2, 256) == True{} : Bool}
441 {FA.find2(b, from, to, c1, c2) == B.find2(b, from, to, c1, c2) : D.Bytes & U32}
442
443# The fast searches hand back the same Bytes, for any arguments (as find_pair
444# and find2_pair say of the reference).
445law fast_find_pair:
446 for b: D.Bytes
447 for from: U32
448 for to: U32
449 for c: U32
450 {FA.find(b, from, to, c) == (b, Pair.snd(D.Bytes, U32, FA.find(b, from, to, c))) : D.Bytes & U32}
451
452law fast_find2_pair:
453 for b: D.Bytes
454 for from: U32
455 for to: U32
456 for c1: U32
457 for c2: U32
458 {FA.find2(b, from, to, c1, c2) == (b, Pair.snd(D.Bytes, U32, FA.find2(b, from, to, c1, c2))) : D.Bytes & U32}
459
460# The word-at-a-time append writes whole words, so up to 3 bytes past the new
461# length differ from the reference's: its laws are append's, on the view.
462law fast_append_view:
463 for dst: D.Bytes
464 for src: D.Bytes
465 for d: Nat
466 for e: Nat
467 for s: U32
468 for n: U32
469 for hd: {D.ok(dst, d) == True{} : Bool}
470 for he: {D.ok(src, e) == True{} : Bool}
471 for hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(src)) == True{} : Bool}
472 for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
473 {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n))) == List.append(&2, U32, D.view(dst), D.slice(D.view(src), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}
474
475law fast_append_ok:
476 for dst: D.Bytes
477 for src: D.Bytes
478 for d: Nat
479 for s: U32
480 for n: U32
481 for hd: {D.ok(dst, d) == True{} : Bool}
482 for hc: {Nat.is_le(Nat.add(D.size(dst), U32.to_nat(n)), D.cap(dst)) == True{} : Bool}
483 {D.ok(Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), d) == True{} : Bool}
484
485law fast_append_pair:
486 for dst: D.Bytes
487 for src: D.Bytes
488 for s: U32
489 for n: U32
490 {FA.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, FA.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}