archive.bend
bend-kit-archive@0.5.0.2 · 373 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.5.0.0/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, Bytes.Bytes>) -> 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{b}:
265 Done{b}
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 do IO<Result<&1, &1, U32 & String, Bytes.Bytes>>:
270 r : Result<&1, &1, U32 & String, Bytes.Bytes> <- Zlib.libz.inflate.raw(size, b)
271 return inflated(r)
272
273def decode(stored: Bool, +size: U32, raw: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, Bytes.Bytes>):
274 match stored:
275 case True{}:
276 IO.pure(Result<&1, &1, U32 & String, Bytes.Bytes>, Done{raw})
277 case False{}:
278 inflate.of(size, raw)
279
280def check.crc.of(ok: Bool, b: Bytes.Bytes) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
281 match ok:
282 case True{}:
283 Done{b}
284 case False{}:
285 Fail{(22, "entry CRC-32 does not match")}
286
287def check.crc(r: Bytes.Bytes & U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
288 (b, +c) = r
289 check.crc.of(U32.is_eq(c, crc), b)
290
291def check.len.of(ok: Bool, b: Bytes.Bytes, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
292 match ok:
293 case False{}:
294 Fail{(22, "entry size differs from the central directory")}
295 case True{}:
296 check.crc(crc.bytes(b), crc)
297
298def check.len(r: Bytes.Bytes & U32, +size: U32, +crc: U32) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
299 (b, +n) = r
300 check.len.of(U32.is_eq(n, size), b, crc)
301
302def check(+size: U32, +crc: U32, r: Result<&1, &1, U32 & String, Bytes.Bytes>) -> Result<&1, &1, U32 & String, Bytes.Bytes>:
303 match r:
304 case Fail{e}:
305 Fail{e}
306 case Done{b}:
307 check.len(Bytes.length(b), size, crc)
308
309def 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>>:
310 match r:
311 case Fail{e}:
312 Fail{e}
313 case Done{b}:
314 Done{((left - size : U32), Con{Entry{nm, b, method, crc}, acc})}
315
316def 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>>):
317 (input, raw) = r
318 do IO<Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>>:
319 out : Result<&1, &1, U32 & String, Bytes.Bytes> <- decode(U32.is_eq(method, 0), size, raw)
320 return (input, one.put(check(size, crc, out), nm, method, crc, left, size, acc))
321
322def 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>>):
323 (input, nm) = r
324 one.data(Bytes.slice(input, data, packed), nm, method, crc, size, left, acc)
325
326# left: the output still allowed under the caller's max.
327def 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>>):
328 match over:
329 case True{}:
330 IO.pure(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>, (input, Fail{(27, "archive output is larger than max")}))
331 case False{}:
332 Header{+name, +nlen, +method, +crc, +packed, +size, +data} = hd
333 one.name(Bytes.slice(input, name, nlen), method, crc, packed, size, data, left, acc)
334
335def one(+hd: Header, input: Bytes.Bytes, +left: U32, acc: List<&1, Entry>) -> IO(Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>>):
336 Header{name, nlen, method, crc, packed, +size, data} = hd
337 one.cap(U32.is_lt(left, size), input, hd, left, acc)
338
339def run.fin(res: Result<&1, &1, U32 & String, U32 & List<&1, Entry>>) -> Result<&1, &1, U32 & String, List<&1, Entry>>:
340 match res:
341 case Fail{e}:
342 Fail{e}
343 case Done{(left, acc)}:
344 Done{List.reverse(&1, Entry, acc)}
345
346def 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>>):
347 match xs:
348 case Nil{}:
349 (input, res) = st
350 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, run.fin(res))
351 case Con{hd, t}:
352 (input, res) = st
353 match res:
354 case Fail{e}:
355 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
356 case Done{(+left, acc)}:
357 do IO<Result<&1, &1, U32 & String, List<&1, Entry>>>:
358 next : Bytes.Bytes & Result<&1, &1, U32 & String, U32 & List<&1, Entry>> <- one(hd, input, left, acc)
359 run(t, next)
360
361def read.of(r: Bytes.Bytes & Result<&1, &1, U32 & String, List<&2, Header>>, +max: U32) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
362 (input, res) = r
363 match res:
364 case Fail{e}:
365 IO.pure(Result<&1, &1, U32 & String, List<&1, Entry>>, Fail{e})
366 case Done{xs}:
367 run(xs, (input, Done{(max, Nil{})}))
368
369# Every entry of a ZIP archive, in central directory order, or the first problem found.
370# Stored (0) and DEFLATE (8) entries only; no ZIP64, encryption, or multi-disk archives.
371# 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.
372def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
373 read.of(headers(input), max)