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.4.0.1/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, 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.
268	def 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	
274	def 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	
281	def 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	
288	def 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	
292	def 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	
299	def 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	
303	def 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	
310	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>>:
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	
317	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>>):
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	
323	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>>):
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.
328	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>>):
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	
336	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>>):
337	  Header{name, nlen, method, crc, packed, +size, data} = hd
338	  one.cap(U32.is_lt(left, size), input, hd, left, acc)
339	
340	def 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	
347	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>>):
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	
362	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>>):
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.
373	def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
374	  read.of(headers(input), max)