LAWS.bend

lawful-bytes@0.1.1.0 · 490 lines · 51 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-bytes@0.1.1.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}