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 ../bytes/bytes.bend as Bytes
4	import bend-kit-bytes@0.3.2.0/bytes.bend as HubBytes
5	import bend-kit-zlib@0.3.0.0/zlib.bend as Zlib
6	import bend-kit-hash@0.2.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.
9	type 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.
14	type 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).
18	def 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.
22	def crc.local(r: HubBytes.Bytes & U32) -> Bytes.Bytes & U32:
23	  (HubBytes.Bytes{len, buf}, crc) = r
24	  (Bytes.Bytes{len, buf}, crc)
25	
26	def crc.bytes(b: Bytes.Bytes) -> Bytes.Bytes & U32:
27	  Bytes.Bytes{len, buf} = b
28	  crc.local(Hash.crc32(HubBytes.Bytes{len, buf}))
29	
30	def crc.value(r: Bytes.Bytes & U32) -> U32:
31	  (b, crc) = r
32	  crc
33	
34	def 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.
38	def 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	
47	def 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	
51	def 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.
59	def u16(+xs: List<&2, U32>, +o: U32) -> U32:
60	  (at(xs, o) .|. (at(xs, (o + 1 : U32)) << 8n) : U32)
61	
62	def 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.
66	def 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).
70	def 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.
74	def same.at3(r: Array<U32> & U32, +u: U32) -> Array<U32> & Bool:
75	  (a, +v) = r
76	  (a, U32.is_eq(u, v))
77	
78	def same.at2(r: Array<U32> & U32, +y: U32) -> Array<U32> & Bool:
79	  (a, +u) = r
80	  same.at3(Bytes.peek(a, y), u)
81	
82	def 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.
95	def 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	
99	def 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.
103	def 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	
116	def 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	
123	def 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	
130	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>>:
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	
137	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>>:
138	  (a, ok) = r
139	  lh.push(ok, a, hd, next, acc)
140	
141	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>>:
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.
150	def 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	
159	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>>:
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	
168	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>>:
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.
176	def 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	
190	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>>:
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	
198	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>>:
199	  (a, +h) = r
200	  cd.head.of(cd.err(h, p, end), a, h, p, cdoff, acc)
201	
202	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>>:
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.
210	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>>:
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	
223	def 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	
229	def 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	
237	def 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	
241	def 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	
249	def 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	
257	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>>:
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.
262	def 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	
266	def 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.
275	def 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	
281	def 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	
288	def 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	
295	def 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	
299	def 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	
306	def 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	
310	def 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	
317	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>>:
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	
324	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>>):
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	
330	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>>):
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.
335	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>>):
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	
343	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>>):
344	  Header{name, nlen, method, crc, packed, +size, data} = hd
345	  one.cap(U32.is_lt(left, size), input, hd, left, acc)
346	
347	def 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	
354	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>>):
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	
369	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>>):
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.
380	def read(max: U32, input: Bytes.Bytes) -> IO(Result<&1, &1, U32 & String, List<&1, Entry>>):
381	  read.of(headers(input), max)