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