bytes.bend
lawful-bytes@0.1.0.0 · 221 lines · 0 definitions
1import Base
2import lawful-words@0.1.0.0/defs.bend as W
3import lawful-bytes@0.1.0.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
178def to_list.cons(+x: U32, r: D.Bytes & List<&2, U32>) -> D.Bytes & List<&2, U32>:
179 (b, t) = r
180 (b, Con{x, t})
181
182# r holds byte s.
183def to_list.go(n: Nat, r: D.Bytes & U32, +s: U32) -> D.Bytes & List<&2, U32>:
184 match n:
185 case 0n:
186 (b, x) = r
187 (b, Nil{})
188 case 1n+m:
189 (b, +x) = r
190 to_list.cons(x, to_list.go(m, at(b, (s + 1 : U32)), (s + 1 : U32)))
191
192# Bytes s .. s+n-1 as a list (Base's file writes take such lists).
193def to_list(b: D.Bytes, +s: U32, +n: U32) -> D.Bytes & List<&2, U32>:
194 to_list.go(U32.to_nat(n), at(b, s), s)
195
196def at2.fin2(+x: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32):
197 (b, +y) = r
198 (b, (x, y))
199
200def at2.fin(+j: U32, r: D.Bytes & U32) -> D.Bytes & (U32 & U32):
201 (b, +x) = r
202 at2.fin2(x, at(b, j))
203
204# Bytes i and j.
205def at2(b: D.Bytes, +i: U32, +j: U32) -> D.Bytes & (U32 & U32):
206 at2.fin(j, at(b, i))
207
208# r holds bytes i and j; acc says all bytes so far matched.
209def same1.go(n: Nat, r: D.Bytes & (U32 & U32), +i: U32, +j: U32, acc: Bool) -> D.Bytes & Bool:
210 match n:
211 case 0n:
212 (b, q) = r
213 (b, acc)
214 case 1n+m:
215 (b, q) = r
216 (x, y) = q
217 same1.go(m, at2(b, (i + 1 : U32), (j + 1 : U32)), (i + 1 : U32), (j + 1 : U32), acc && U32.is_eq(x, y))
218
219# Bytes i .. i+n-1 equal bytes j .. j+n-1 of the same buffer.
220def same1(b: D.Bytes, +i: U32, +j: U32, +n: U32) -> D.Bytes & Bool:
221 same1.go(U32.to_nat(n), at2(b, i, j), i, j, True{})