bytes.bend

lawful-bytes@0.1.1.0 · 219 lines · 35 definitions

1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.1.0/defs.bend as D
4
5# lawful-bytes operations. This is the reference version: a byte at a time,
6# simple to prove. Faster versions (a word at a time) replace these bodies
7# under the same laws. Loops here read one byte ahead and discard it at the
8# end; reads past len stay inside the block (Base wraps indexes), and the
9# value read never reaches a result.
10
11# An empty Bytes with room for 4 * 2^d bytes.
12def empty(+d: Nat) -> D.Bytes:
13  D.Bytes{0, Array.new(U32, d, 0)}
14
15def at.fin(+len: U32, +i: U32, r: Array<U32> & U32) -> D.Bytes & U32:
16  (buf, +w) = r
17  (D.Bytes{len, buf}, W.byte(w, U32.to_nat((i .&. 3 : U32))))
18
19# Byte i (for i < len).
20def at(b: D.Bytes, +i: U32) -> D.Bytes & U32:
21  D.Bytes{+len, buf} = b
22  at.fin(len, i, Array.get(U32, buf, (i >> 2n : U32)))
23
24def set.fin(+len: U32, +i: U32, +v: U32, r: Array<U32> & U32) -> D.Bytes:
25  (buf, +w) = r
26  D.Bytes{len, Array.set(U32, buf, (i >> 2n : U32), W.put_byte(w, U32.to_nat((i .&. 3 : U32)), v))}
27
28# Byte i set to v (for i < len and v < 256).
29def set(b: D.Bytes, +i: U32, +v: U32) -> D.Bytes:
30  D.Bytes{+len, buf} = b
31  set.fin(len, i, v, Array.get(U32, buf, (i >> 2n : U32)))
32
33def push.fin(+len: U32, +v: U32, r: Array<U32> & U32) -> D.Bytes:
34  (buf, +w) = r
35  D.Bytes{(len + 1 : U32), Array.set(U32, buf, (len >> 2n : U32), W.put_byte(w, U32.to_nat((len .&. 3 : U32)), v))}
36
37# v added at the end (for len < cap and v < 256).
38def push(b: D.Bytes, +v: U32) -> D.Bytes:
39  D.Bytes{+len, buf} = b
40  push.fin(len, v, Array.get(U32, buf, (len >> 2n : U32)))
41
42# n more bytes of src, from s; r holds src's byte s.
43def append.go(n: Nat, dst: D.Bytes, r: D.Bytes & U32, +s: U32) -> D.Bytes & D.Bytes:
44  match n:
45    case 0n:
46      (src, x) = r
47      (dst, src)
48    case 1n+k:
49      (src, +x) = r
50      append.go(k, push(dst, x), at(src, (s + 1 : U32)), (s + 1 : U32))
51
52# dst with bytes s .. s+n-1 of src added at the end; src handed back.
53def append(dst: D.Bytes, src: D.Bytes, +s: U32, +n: U32) -> D.Bytes & D.Bytes:
54  append.go(U32.to_nat(n), dst, at(src, s), s)
55
56# Word i onwards copied into dst; r holds word i of the old block.
57def grow.go(n: Nat, r: Array<U32> & U32, dst: Array<U32>, +i: U32) -> Array<U32>:
58  match n:
59    case 0n:
60      (src, w) = r
61      dst
62    case 1n+k:
63      (src, +w) = r
64      grow.go(k, Array.get(U32, src, (i + 1 : U32)), Array.set(U32, dst, i, w), (i + 1 : U32))
65
66def grow.fin(+len: U32, +e: Nat, r: Array<U32> & U32) -> D.Bytes:
67  (buf, +n) = r
68  D.Bytes{len, grow.go(U32.to_nat(n), Array.get(U32, buf, 0), Array.new(U32, e, 0), 0)}
69
70# The same bytes in a block of 2^e words (for e at least the current depth).
71def grow(b: D.Bytes, +e: Nat) -> D.Bytes:
72  D.Bytes{+len, buf} = b
73  grow.fin(len, e, Array.size(U32, buf))
74
75# hit says byte j is c; r holds byte j + 1; n counts positions left from j.
76def find.go(n: Nat, hit: Bool, r: D.Bytes & U32, +j: U32, +to: U32, +c: U32) -> D.Bytes & U32:
77  match n hit:
78    case 0n _:
79      (b, x) = r
80      (b, to)
81    case 1n+k True{}:
82      (b, x) = r
83      (b, j)
84    case 1n+k False{}:
85      (b, +x) = r
86      find.go(k, U32.is_eq(x, c), at(b, (j + 2 : U32)), (j + 1 : U32), to, c)
87
88def find.start(n: Nat, r: D.Bytes & U32, +from: U32, +to: U32, +c: U32) -> D.Bytes & U32:
89  (b, +x) = r
90  find.go(n, U32.is_eq(x, c), at(b, (from + 1 : U32)), from, to, c)
91
92# The first index j with from <= j < to where byte j is c; to if none.
93def find(b: D.Bytes, +from: U32, +to: U32, +c: U32) -> D.Bytes & U32:
94  find.start(Nat.sub(U32.to_nat(to), U32.to_nat(from)), at(b, from), from, to, c)
95
96def find2.go(n: Nat, hit: Bool, r: D.Bytes & U32, +j: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32:
97  match n hit:
98    case 0n _:
99      (b, x) = r
100      (b, to)
101    case 1n+k True{}:
102      (b, x) = r
103      (b, j)
104    case 1n+k False{}:
105      (b, +x) = r
106      find2.go(k, U32.is_eq(x, c1) || U32.is_eq(x, c2), at(b, (j + 2 : U32)), (j + 1 : U32), to, c1, c2)
107
108def find2.start(n: Nat, r: D.Bytes & U32, +from: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32:
109  (b, +x) = r
110  find2.go(n, U32.is_eq(x, c1) || U32.is_eq(x, c2), at(b, (from + 1 : U32)), from, to, c1, c2)
111
112# The first index j with from <= j < to where byte j is c1 or c2; to if none.
113def find2(b: D.Bytes, +from: U32, +to: U32, +c1: U32, +c2: U32) -> D.Bytes & U32:
114  find2.start(Nat.sub(U32.to_nat(to), U32.to_nat(from)), at(b, from), from, to, c1, c2)
115
116# ra, rb hold byte i of a and byte j of b; acc says all bytes so far matched.
117def same.go(n: Nat, ra: D.Bytes & U32, rb: D.Bytes & U32, +i: U32, +j: U32, acc: Bool) -> D.Bytes & (D.Bytes & Bool):
118  match n:
119    case 0n:
120      (a, x) = ra
121      (b, y) = rb
122      (a, (b, acc))
123    case 1n+k:
124      (a, +x) = ra
125      (b, +y) = rb
126      same.go(k, at(a, (i + 1 : U32)), at(b, (j + 1 : U32)), (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(x, y))
127
128# Bytes i .. i+n-1 of a equal bytes j .. j+n-1 of b; both handed back.
129def same(a: D.Bytes, +i: U32, b: D.Bytes, +j: U32, +n: U32) -> D.Bytes & (D.Bytes & Bool):
130  same.go(U32.to_nat(n), at(a, i), at(b, j), i, j, True{})
131
132# The number of bytes in use.
133def len(b: D.Bytes) -> D.Bytes & U32:
134  D.Bytes{+n, buf} = b
135  (D.Bytes{n, buf}, n)
136
137def capacity.fin(+n: U32, r: Array<U32> & U32) -> D.Bytes & U32:
138  (buf, +w) = r
139  (D.Bytes{n, buf}, (w << 2n : U32))
140
141# How many bytes fit (4 per word).
142def capacity(b: D.Bytes) -> D.Bytes & U32:
143  D.Bytes{+n, buf} = b
144  capacity.fin(n, Array.size(U32, buf))
145
146# Only the first n bytes kept (for n <= len).
147def truncate(b: D.Bytes, +n: U32) -> D.Bytes:
148  D.Bytes{len, buf} = b
149  D.Bytes{n, buf}
150
151# Bytes j + k onwards moved to j; r holds byte j + k.
152def shift.go(n: Nat, r: D.Bytes & U32, +j: U32, +k: U32) -> D.Bytes:
153  match n:
154    case 0n:
155      (b, x) = r
156      b
157    case 1n+m:
158      (b, +x) = r
159      shift.go(m, at(set(b, j, x), ((j + 1 : U32) + k : U32)), (j + 1 : U32), k)
160
161# The first k bytes dropped, the rest moved to the start (for k <= len).
162def shift(b: D.Bytes, +k: U32) -> D.Bytes:
163  D.Bytes{+n, buf} = b
164  truncate(shift.go(Nat.sub(U32.to_nat(n), U32.to_nat(k)), at(D.Bytes{n, buf}, k), 0, k), (n - k : U32))
165
166def of_list.go(xs: List<&2, U32>, b: D.Bytes) -> D.Bytes:
167  match xs:
168    case Nil{}:
169      b
170    case Con{x, t}:
171      of_list.go(t, push(b, x))
172
173# A Bytes in a block of 2^d words holding the bytes of xs (Base's file
174# reads give such lists).
175def of_list(+d: Nat, xs: List<&2, U32>) -> D.Bytes:
176  of_list.go(xs, empty(d))
177
178# n more bytes put in front of acc, from byte j down; r holds byte j. A tail
179# call, so the loop runs in constant stack.
180def to_list.go(n: Nat, r: D.Bytes & U32, +j: U32, acc: List<&2, U32>) -> D.Bytes & List<&2, U32>:
181  match n:
182    case 0n:
183      (b, x) = r
184      (b, acc)
185    case 1n+m:
186      (b, +x) = r
187      to_list.go(m, at(b, (j - 1 : U32)), (j - 1 : U32), Con{x, acc})
188
189# Bytes s .. s+n-1 as a list (Base's file writes take such lists), built from
190# the last byte back.
191def to_list(b: D.Bytes, +s: U32, +n: U32) -> D.Bytes & List<&2, U32>:
192  to_list.go(U32.to_nat(n), at(b, ((s + n : U32) - 1 : U32)), ((s + n : U32) - 1 : U32), Nil{})
193
194def at2.fin2(+x: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32):
195  (b, +y) = r
196  (b, (x, y))
197
198def at2.fin(+j: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32):
199  (b, +x) = r
200  at2.fin2(x, at(b, j))
201
202# Bytes i and j.
203def at2(b: D.Bytes, +i: U32, +j: U32) -> D.Bytes & (U32 & U32):
204  at2.fin(j, at(b, i))
205
206# r holds bytes i and j; acc says all bytes so far matched.
207def same1.go(n: Nat, r: D.Bytes & (U32 & U32), +i: U32, +j: U32, acc: Bool) -> D.Bytes & Bool:
208  match n:
209    case 0n:
210      (b, q) = r
211      (b, acc)
212    case 1n+m:
213      (b, q) = r
214      (x, y) = q
215      same1.go(m, at2(b, (i + 1 : U32), (j + 1 : U32)), (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(x, y))
216
217# Bytes i .. i+n-1 equal bytes j .. j+n-1 of the same buffer.
218def same1(b: D.Bytes, +i: U32, +j: U32, +n: U32) -> D.Bytes & Bool:
219  same1.go(U32.to_nat(n), at2(b, i, j), i, j, True{})