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
2	import Base
3	import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes
4	import bend-kit-zlib@0.5.0.0/zlib.bend as Zlib
5	import 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.
8	type 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.
13	type 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).
17	def supported(+method: U32) -> Bool:
18	  Bool.or(U32.is_eq(method, 0), U32.is_eq(method, 8))
19	
20	def crc.bytes(b: Bytes.Bytes) -> Bytes.Bytes & U32:
21	  Hash.crc32(b)
22	
23	def crc.value(r: Bytes.Bytes & U32) -> U32:
24	  (b, crc) = r
25	  crc
26	
27	def 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.
31	def 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	
40	def 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	
44	def 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.
52	def u16(+xs: List<&2, U32>, +o: U32) -> U32:
53	  (at(xs, o) .|. (at(xs, (o + 1 : U32)) << 8n) : U32)
54	
55	def 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.
59	def 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).
63	def 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.
67	def same.at3(r: Array<U32> & U32, +u: U32) -> Array<U32> & Bool:
68	  (a, +v) = r
69	  (a, U32.is_eq(u, v))
70	
71	def same.at2(r: Array<U32> & U32, +y: U32) -> Array<U32> & Bool:
72	  (a, +u) = r
73	  same.at3(Bytes.peek(a, y), u)
74	
75	def 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.
88	def 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	
92	def 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.
96	def 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	
109	def 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	
116	def 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	
123	def 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	
130	def 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	
134	def 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.
143	def 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	
152	def 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	
161	def 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.
169	def 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	
183	def 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	
191	def 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	
195	def 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.
203	def 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	
216	def 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	
222	def 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	
230	def 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	
234	def 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	
242	def 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	
250	def 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.
255	def 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	
259	def 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.
268	def 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	
273	def 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	
280	def 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	
287	def 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	
291	def 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	
298	def 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	
302	def 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	
309	def 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	
316	def 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	
322	def 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.
327	def 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	
335	def 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	
339	def 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	
346	def 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	
361	def 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.
372	def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
373	  read.of(headers(input), max)