archive/archive.bend
bend-kit-archive@0.2.0.1 · 381 lines · 0 definitions
1# ZIP archives read over Bytes: stored and DEFLATE entries, checked against their CRC-32 and sizes. Source: https://github.com/paymog/bend-kit/tree/main/archive
2import Base
3import bend-kit-archive@0.2.0.1/bytes/bytes.bend as Bytes
4import bend-kit-bytes@0.3.0.0/bytes.bend as HubBytes
5import bend-kit-zlib@0.2.0.1/zlib.bend as Zlib
6import bend-kit-hash@0.1.0.0/hash.bend as Hash
7
8# One member: its name and contents as raw bytes, its method (0 stored, 8 DEFLATE), and its CRC-32.
9type Entry is Type:
10 Entry{name: Bytes.Bytes, data: Bytes.Bytes, method: U32, crc: U32}
11
12# A checked central directory entry. name and data are byte offsets into the input;
13# packed is the stored or compressed length, size the length after decoding.
14type Header is Data:
15 Header{name: U32, name_len: U32, method: U32, crc: U32, packed: U32, size: U32, data: U32}
16
17# The methods read: 0 (stored) and 8 (DEFLATE).
18def supported(+method: U32) -> Bool:
19 Bool.or(U32.is_eq(method, 0), U32.is_eq(method, 8))
20
21# Hash uses the published Bytes type; transfer the array without copying.
22def crc.local(r: HubBytes.Bytes & U32) -> Bytes.Bytes & U32:
23 (HubBytes.Bytes{len, buf}, crc) = r
24 (Bytes.Bytes{len, buf}, crc)
25
26def crc.bytes(b: Bytes.Bytes) -> Bytes.Bytes & U32:
27 Bytes.Bytes{len, buf} = b
28 crc.local(Hash.crc32(HubBytes.Bytes{len, buf}))
29
30def crc.value(r: Bytes.Bytes & U32) -> U32:
31 (b, crc) = r
32 crc
33
34def crc32(b: Bytes.Bytes) -> U32:
35 crc.value(crc.bytes(b))
36
37# n bytes from i as a list. Callers keep i + n within the buffer.
38def grab.go(k: Nat, r: Array<U32> & U32, +j: U32, acc: List<&2, U32>) -> Array<U32> & List<&2, U32>:
39 match k:
40 case 0n:
41 (a, v) = r
42 (a, acc)
43 case 1n+p:
44 (a, +v) = r
45 grab.go(p, Bytes.peek(a, (j - 1 : U32)), (j - 1 : U32), Con{v, acc})
46
47def grab(a: Array<U32>, +i: U32, +n: U32) -> Array<U32> & List<&2, U32>:
48 +j = (i + n - 1 : U32)
49 grab.go(U32.to_nat(n), Bytes.peek(a, j), j, Nil{})
50
51def at(xs: List<&2, U32>, +i: U32) -> U32:
52 match xs:
53 case Nil{}:
54 0
55 case Con{h, t}:
56 Bool.pick(U32, U32.is_zero(i), h, at(t, (i - 1 : U32)))
57
58# Little-endian fields of a grabbed record.
59def u16(+xs: List<&2, U32>, +o: U32) -> U32:
60 (at(xs, o) .|. (at(xs, (o + 1 : U32)) << 8n) : U32)
61
62def u32(+xs: List<&2, U32>, +o: U32) -> U32:
63 (u16(xs, o) .|. (u16(xs, (o + 2 : U32)) << 16n) : U32)
64
65# The first failed check's message, outermost first.
66def why(+ok: Bool, +msg: String, +rest: Maybe<&2, String>) -> Maybe<&2, String>:
67 Bool.pick(Maybe<&2, String>, ok, rest, Some{msg})
68
69# General purpose flags: encrypted (bit 0), strong encryption (bit 6), masked headers (bit 13).
70def encrypted(+flags: U32) -> Bool:
71 Bool.not(U32.is_zero((flags .&. 8257 : U32)))
72
73# Do n bytes at x and at y match? r holds the previous byte's answer.
74def same.at3(r: Array<U32> & U32, +u: U32) -> Array<U32> & Bool:
75 (a, +v) = r
76 (a, U32.is_eq(u, v))
77
78def same.at2(r: Array<U32> & U32, +y: U32) -> Array<U32> & Bool:
79 (a, +u) = r
80 same.at3(Bytes.peek(a, y), u)
81
82def same.go(n: Nat, r: Array<U32> & Bool, +x: U32, +y: U32) -> Array<U32> & Bool:
83 match n:
84 case 0n:
85 r
86 case 1n+q:
87 (a, ok) = r
88 match ok:
89 case False{}:
90 (a, False{})
91 case True{}:
92 same.go(q, same.at2(Bytes.peek(a, x), y), (x + 1 : U32), (y + 1 : U32))
93
94# End of central directory (APPNOTE 4.3.16): the last signature whose comment length reaches the end exactly.
95def eocd.of(r: Array<U32> & List<&2, U32>, +len: U32, +p: U32) -> Array<U32> & Bool:
96 (a, +x) = r
97 (a, Bool.and(U32.is_eq(u32(x, 0), 101010256), U32.is_eq(u16(x, 20), (len - p - 22 : U32))))
98
99def eocd.win(a: Array<U32>, +len: U32, +p: U32) -> Array<U32> & Bool:
100 eocd.of(grab(a, p, 22), len, p)
101
102# f counts the positions left below p; a comment is at most 65535 bytes.
103def eocd.go(f: Nat, r: Array<U32> & Bool, +len: U32, +p: U32) -> Array<U32> & Maybe<&2, U32>:
104 match f:
105 case 0n:
106 (a, hit) = r
107 (a, Bool.pick(Maybe<&2, U32>, hit, Some{p}, None{}))
108 case 1n+q:
109 (a, hit) = r
110 match hit:
111 case True{}:
112 (a, Some{p})
113 case False{}:
114 eocd.go(q, eocd.win(a, len, (p - 1 : U32)), len, (p - 1 : U32))
115
116def cd.fin.end(ok: Bool, acc: List<&2, Header>) -> Result<&1, &1, U32 & String, List<&2, Header>>:
117 match ok:
118 case True{}:
119 Done{List.reverse(&2, Header, acc)}
120 case False{}:
121 Fail{(22, "central directory size does not match its entries")}
122
123def cd.fin(res: Result<&1, &1, U32 & String, U32 & List<&2, Header>>, +end: U32) -> Result<&1, &1, U32 & String, List<&2, Header>>:
124 match res:
125 case Fail{e}:
126 Fail{e}
127 case Done{(+p, acc)}:
128 cd.fin.end(U32.is_eq(p, end), acc)
129
130def lh.push(ok: Bool, a: Array<U32>, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
131 match ok:
132 case False{}:
133 (a, Fail{(22, "local header name differs from the central directory")})
134 case True{}:
135 (a, Done{(next, Con{hd, acc})})
136
137def lh.same(r: Array<U32> & Bool, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
138 (a, ok) = r
139 lh.push(ok, a, hd, next, acc)
140
141def lh.name(err: Maybe<&2, String>, a: Array<U32>, +lname: U32, +hd: Header, +next: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
142 match err:
143 case Some{m}:
144 (a, Fail{(22, m)})
145 case None{}:
146 Header{+name, +nlen, method, crc, packed, size, data} = hd
147 lh.same(same.go(U32.to_nat(nlen), (a, True{}), name, lname), hd, next, acc)
148
149# Local file header (APPNOTE 4.3.7): it must agree with the central directory, and its data must end before the directory.
150def lh.err(+l: List<&2, U32>, +method: U32, +nlen: U32, +packed: U32, +cdoff: U32, +lname: U32, +extra: U32) -> Maybe<&2, String>:
151 +data = (lname + extra : U32)
152 why(U32.is_eq(u32(l, 0), 67324752), "bad local header signature",
153 why(Bool.not(encrypted(u16(l, 6))), "encrypted entries are unsupported",
154 why(U32.is_eq(u16(l, 8), method), "local header method differs from the central directory",
155 why(U32.is_eq(u16(l, 26), nlen), "local header name differs from the central directory",
156 why(Bytes.fits(cdoff, lname, extra), "local header runs past the central directory",
157 why(Bytes.fits(cdoff, data, packed), "entry data runs past the central directory", None{}))))))
158
159def lh.head(r: Array<U32> & List<&2, U32>, +h: List<&2, U32>, +p: U32, +next: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
160 (a, +l) = r
161 +nlen = u16(h, 28)
162 +method = u16(h, 10)
163 +packed = u32(h, 20)
164 +lname = (u32(h, 42) + 30 : U32)
165 +extra = (u16(l, 26) + u16(l, 28) : U32)
166 lh.name(lh.err(l, method, nlen, packed, cdoff, lname, extra), a, lname, Header{(p + 46 : U32), nlen, method, u32(h, 16), packed, u32(h, 24), (lname + extra : U32)}, next, acc)
167
168def lh.at(ok: Bool, a: Array<U32>, +h: List<&2, U32>, +p: U32, +next: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
169 match ok:
170 case False{}:
171 (a, Fail{(22, "local header is out of bounds")})
172 case True{}:
173 lh.head(grab(a, u32(h, 42), 30), h, p, next, cdoff, acc)
174
175# Central directory file header (APPNOTE 4.3.12) at p, with the directory ending at end.
176def cd.err(+h: List<&2, U32>, +p: U32, +end: U32) -> Maybe<&2, String>:
177 +method = u16(h, 10)
178 +packed = u32(h, 20)
179 +size = u32(h, 24)
180 +rest = (u16(h, 28) + u16(h, 30) + u16(h, 32) : U32)
181 +zip64 = Bool.or(Bool.or(U32.is_eq(packed, 4294967295), U32.is_eq(size, 4294967295)), U32.is_eq(u32(h, 42), 4294967295))
182 why(U32.is_eq(u32(h, 0), 33639248), "bad central directory header signature",
183 why(Bool.not(encrypted(u16(h, 8))), "encrypted entries are unsupported",
184 why(supported(method), "unsupported compression method " ++ U32.show(method),
185 why(Bool.not(zip64), "ZIP64 is unsupported",
186 why(U32.is_eq(u16(h, 34), 0), "multi-disk ZIP is unsupported",
187 why(Bytes.fits(end, (p + 46 : U32), rest), "central directory header runs past the directory",
188 why(Bool.or(U32.is_eq(method, 8), U32.is_eq(packed, size)), "stored entry sizes differ", None{})))))))
189
190def cd.head.of(err: Maybe<&2, String>, a: Array<U32>, +h: List<&2, U32>, +p: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
191 match err:
192 case Some{m}:
193 (a, Fail{(22, m)})
194 case None{}:
195 +next = (p + 46 + u16(h, 28) + u16(h, 30) + u16(h, 32) : U32)
196 lh.at(Bytes.fits(cdoff, u32(h, 42), 30), a, h, p, next, cdoff, acc)
197
198def cd.head(r: Array<U32> & List<&2, U32>, +p: U32, +end: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
199 (a, +h) = r
200 cd.head.of(cd.err(h, p, end), a, h, p, cdoff, acc)
201
202def cd.entry(ok: Bool, a: Array<U32>, +p: U32, +end: U32, +cdoff: U32, acc: List<&2, Header>) -> Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>:
203 match ok:
204 case False{}:
205 (a, Fail{(22, "central directory is truncated")})
206 case True{}:
207 cd.head(grab(a, p, 46), p, end, cdoff, acc)
208
209# k entries left; r holds the next header's offset and the headers so far, reversed.
210def cd.go(k: Nat, r: Array<U32> & Result<&1, &1, U32 & String, U32 & List<&2, Header>>, +end: U32, +cdoff: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
211 match k:
212 case 0n:
213 (a, res) = r
214 (a, cd.fin(res, end))
215 case 1n+q:
216 (a, res) = r
217 match res:
218 case Fail{e}:
219 (a, Fail{e})
220 case Done{(+p, acc)}:
221 cd.go(q, cd.entry(Bytes.fits(end, p, 46), a, p, end, cdoff, acc), end, cdoff)
222
223def eocd.err(+x: List<&2, U32>, +e: U32) -> Maybe<&2, String>:
224 +zip64 = Bool.or(Bool.or(U32.is_eq(u16(x, 10), 65535), U32.is_eq(u32(x, 12), 4294967295)), U32.is_eq(u32(x, 16), 4294967295))
225 why(Bool.and(Bool.and(U32.is_eq(u16(x, 4), 0), U32.is_eq(u16(x, 6), 0)), U32.is_eq(u16(x, 8), u16(x, 10))), "multi-disk ZIP is unsupported",
226 why(Bool.not(zip64), "ZIP64 is unsupported",
227 why(Bytes.fits(e, u32(x, 16), u32(x, 12)), "central directory is out of bounds", None{})))
228
229def eocd.checked(err: Maybe<&2, String>, a: Array<U32>, +x: List<&2, U32>) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
230 match err:
231 case Some{m}:
232 (a, Fail{(22, m)})
233 case None{}:
234 +off = u32(x, 16)
235 cd.go(U32.to_nat(u16(x, 10)), (a, Done{(off, Nil{})}), (off + u32(x, 12) : U32), off)
236
237def eocd.parse(r: Array<U32> & List<&2, U32>, +e: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
238 (a, +x) = r
239 eocd.checked(eocd.err(x, e), a, x)
240
241def eocd.found(r: Array<U32> & Maybe<&2, U32>) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
242 (a, m) = r
243 match m:
244 case None{}:
245 (a, Fail{(22, "no end of central directory record")})
246 case Some{+e}:
247 eocd.parse(grab(a, e, 22), e)
248
249def headers.at(short: Bool, a: Array<U32>, +len: U32) -> Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>:
250 match short:
251 case True{}:
252 (a, Fail{(22, "input is shorter than an end of central directory record")})
253 case False{}:
254 +p = (len - 22 : U32)
255 eocd.found(eocd.go(U32.to_nat(U32.min(p, 65535)), eocd.win(a, len, p), len, p))
256
257def headers.fin(+len: U32, r: Array<U32> & Result<&1, &1, U32 & String, List<&2, Header>>) -> Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>:
258 (a, res) = r
259 (Bytes.Bytes{len, a}, res)
260
261# The input back, and its central directory with every bound, local header, and method checked. Pure: no data is decoded.
262def headers(input: Bytes.Bytes) -> Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>:
263 Bytes.Bytes{+len, buf} = input
264 headers.fin(len, headers.at(U32.is_lt(len, 22), buf, len))
265
266def inflated(r: Result<&1, &1, U32 & String, U32 & Array<U32>>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
267 match r:
268 case Fail{e}:
269 (+code, msg) = e
270 Fail{Bool.pick(U32 & String, U32.is_eq(code, 27), (22, "entry size differs from the central directory"), (code, "DEFLATE entry: " ++ msg))}
271 case Done{(+n, w)}:
272 Done{Bytes.Bytes{n, w}}
273
274# Output past size is refused inside libz, so a bomb never grows beyond its declared size.
275def inflate.of(+size: U32, b: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Bytes.Bytes>):
276 Bytes.Bytes{+n, buf} = b
277 do IO<Result<&1, &1, U32 & String, Bytes.Bytes>>:
278 r : Result<&1, &1, U32 & String, U32 & Array<U32>> <- Zlib.inflate.raw.words(size, n, buf)
279 return inflated(r)
280
281def decode(stored: Bool, +size: U32, raw: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Bytes.Bytes>):
282 match stored:
283 case True{}:
284 IO.pure(Result<&1, &1, U32 & String, Bytes.Bytes>, Done{raw})
285 case False{}:
286 inflate.of(size, raw)
287
288def check.crc.of(ok: Bool, b: Bytes.Bytes) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
289 match ok:
290 case True{}:
291 Done{b}
292 case False{}:
293 Fail{(22, "entry CRC-32 does not match")}
294
295def check.crc(r: Bytes.Bytes & U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
296 (b, +c) = r
297 check.crc.of(U32.is_eq(c, crc), b)
298
299def check.len.of(ok: Bool, b: Bytes.Bytes, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
300 match ok:
301 case False{}:
302 Fail{(22, "entry size differs from the central directory")}
303 case True{}:
304 check.crc(crc.bytes(b), crc)
305
306def check.len(r: Bytes.Bytes & U32, +size: U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
307 (b, +n) = r
308 check.len.of(U32.is_eq(n, size), b, crc)
309
310def check(+size: U32, +crc: U32, r: Result<&1, &1, U32 & String, Bytes.Bytes>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
311 match r:
312 case Fail{e}:
313 Fail{e}
314 case Done{b}:
315 check.len(Bytes.length(b), size, crc)
316
317def one.put(r: Result<&1, &1, U32 & String, Bytes.Bytes>, nm: Bytes.Bytes, +method: U32, +crc: U32, +left: U32, +size: U32, acc: List<&1, Entry>) -> Result<&1, &1, U32 & String, U32 & List<&1, Entry>>:
318 match r:
319 case Fail{e}:
320 Fail{e}
321 case Done{b}:
322 Done{((left - size : U32), Con{Entry{nm, b, method, crc}, acc})}
323
324def one.data(r: Bytes.Bytes & Bytes.Bytes, nm: Bytes.Bytes, +method: U32, +crc: U32, +size: U32, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
325 (input, raw) = r
326 do IO<Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>>:
327 out : Result<&1, &1, U32 & String, Bytes.Bytes> <- decode(U32.is_eq(method, 0), size, raw)
328 return (input, one.put(check(size, crc, out), nm, method, crc, left, size, acc))
329
330def one.name(r: Bytes.Bytes & Bytes.Bytes, +method: U32, +crc: U32, +packed: U32, +size: U32, +data: U32, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
331 (input, nm) = r
332 one.data(Bytes.slice(input, data, packed), nm, method, crc, size, left, acc)
333
334# left: the output still allowed under the caller's max.
335def one.cap(over: Bool, input: Bytes.Bytes, +hd: Header, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
336 match over:
337 case True{}:
338 IO.pure(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>, (input, Fail{(27, "archive output is larger than max")}))
339 case False{}:
340 Header{+name, +nlen, +method, +crc, +packed, +size, +data} = hd
341 one.name(Bytes.slice(input, name, nlen), method, crc, packed, size, data, left, acc)
342
343def one(+hd: Header, input: Bytes.Bytes, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
344 Header{name, nlen, method, crc, packed, +size, data} = hd
345 one.cap(U32.is_lt(left, size), input, hd, left, acc)
346
347def run.fin(res: Result<&1, &1, U32 & String, U32 & List<&1, Entry>>) -> Result<&1, &1, U32 & String, List<&1, Entry>>:
348 match res:
349 case Fail{e}:
350 Fail{e}
351 case Done{(left, acc)}:
352 Done{List.reverse(&1, Entry, acc)}
353
354def run(xs: List<&2, Header>, st: Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
355 match xs:
356 case Nil{}:
357 (input, res) = st
358 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, run.fin(res))
359 case Con{hd, t}:
360 (input, res) = st
361 match res:
362 case Fail{e}:
363 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
364 case Done{(+left, acc)}:
365 do IO<Result<&1, &1, U32 & String, List<&1, Entry>>>:
366 next : Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>> <- one(hd, input, left, acc)
367 run(t, next)
368
369def read.of(r: Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>, +max: U32) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
370 (input, res) = r
371 match res:
372 case Fail{e}:
373 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
374 case Done{xs}:
375 run(xs, (input, Done{(max, Nil{})}))
376
377# Every entry of a ZIP archive, in central directory order, or the first problem found.
378# Stored (0) and DEFLATE (8) entries only; no ZIP64, encryption, or multi-disk archives.
379# Output past max bytes in total fails with 27 (EFBIG). Malformed ZIP fails with 22 (EINVAL); libz load and allocation errors keep their host codes.
380def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
381 read.of(headers(input), max)