1	import Base
2	import ./defs.bend as D
3	import ./bytes.bend as B
4	import ./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	
15	law 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	
21	law view_bytes:
22	  for b: D.Bytes
23	  {D.all_bytes(D.view(b)) == True{} : Bool}
24	
25	law 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	
35	law empty_view:
36	  for d: Nat
37	  {D.view(B.empty(d)) == Nil{} : List<&2, U32>}
38	
39	law 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.
45	law 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	
54	law 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	
67	law 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).
76	law 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.
83	law 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).
96	law 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	
103	law 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).
118	law 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.
127	law 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).
142	law 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	
154	law 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	
164	law 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	
172	law 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	
181	law 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.
190	law 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	
203	law 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).
214	law 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	
225	law len_view:
226	  for b: D.Bytes
227	  {U32.to_nat(Pair.snd(D.Bytes, U32, B.len(b))) == D.size(b) : Nat}
228	
229	law len_pair:
230	  for b: D.Bytes
231	  {B.len(b) == (b, Pair.snd(D.Bytes, U32, B.len(b))) : D.Bytes & U32}
232	
233	law 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	
239	law capacity_pair:
240	  for b: D.Bytes
241	  {B.capacity(b) == (b, Pair.snd(D.Bytes, U32, B.capacity(b))) : D.Bytes & U32}
242	
243	law 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	
249	law 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).
259	law 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	
267	law 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	
279	law 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	
287	law 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	
294	law 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	
303	law 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	
313	law 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	
324	law 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	
335	law 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.
345	law 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.
356	law 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	
366	law 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	
376	law 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	
387	law 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.
399	law 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.
406	law 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.
417	law 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	
429	law 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).
445	law 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	
452	law 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.
462	law 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	
475	law 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	
485	law 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}