checkpoint_zip.bend
stelliferous@0.0.3.0 · 171 lines · 0 definitions
1# A ZIP archive read through the official File effects. The end record locates
2# the central directory, which names every entry with its size and the offset of
3# its local header; the entry's bytes follow that header. Only stored entries
4# are read, the form torch.save writes.
5import Base
6import stelliferous@0.0.3.0/storage_bytes.bend as Bytes
7
8# An entry: its name as bytes, the offset of its local header, its length and
9# its compression method, 0 for stored.
10type Record is Data:
11 Record{name: List<&2,U32>,header: U32,length: U32,method: U32}
12
13type Listing is Data:
14 Records{records: List<&2,Record>}
15 Unreadable{detail: String}
16
17type Fetched is Type:
18 Fetched{file: File,bytes: Maybe<&2,List<&2,U32>>}
19
20def Read() -> Type:
21 File & Result<&1,&1,U32 & String,List<&2,U32>>
22
23def Sized() -> Type:
24 File & Result<&1,&1,U32 & String,U32>
25
26# Signatures, least significant byte first.
27def central_signature() -> U32:
28 33639248
29
30def local_signature() -> U32:
31 67324752
32
33def end_signature() -> List<&2,U32>:
34 [80,75,5,6]
35
36# A central directory entry is 46 bytes, then its name, extra field and comment.
37def records(fuel: Nat,valid: Bool,+bytes: List<&2,U32>,found: List<&2,Record>) -> Listing:
38 match fuel valid:
39 case 0n valid: Records{List.reverse(&2,Record,found)}
40 case 1n+rest False{}: Unreadable{"has a damaged central directory"}
41 case 1n+rest True{}:
42 +name_length = Bytes.u16_at(bytes,28n)
43 +skipped = U32.to_nat((46 + name_length + Bytes.u16_at(bytes,30n) + Bytes.u16_at(bytes,32n) : U32))
44 +next = List.drop(&2,U32,bytes,skipped)
45 records(rest,U32.is_eq(Bytes.u32_at(next,0n),central_signature()),next,
46 Record{List.take(&2,U32,List.drop(&2,U32,bytes,46n),U32.to_nat(name_length)),Bytes.u32_at(bytes,42n),Bytes.u32_at(bytes,24n),Bytes.u16_at(bytes,10n)} <> found)
47
48def directory_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+count: U32) -> Listing:
49 match result:
50 case Fail{error}: Unreadable{"cannot be read"}
51 case Done{+bytes}: records(U32.to_nat(count),U32.is_eq(Bytes.u32_at(bytes,0n),central_signature()),bytes,[])
52
53def directory_fetched(read: Read(),+count: U32) -> File & Listing:
54 (file,result) = read
55 (file,directory_read(result,count))
56
57def ending(wide: Bool,file: File,+count: U32,+size: U32,+offset: U32) -> IO(File & Listing):
58 match wide:
59 case True{}: IO.pure(File & Listing,(file,Unreadable{"is a ZIP64 archive"}))
60 case False{}:
61 do IO<File & Listing>:
62 read : Read() <- File.read_at(file,offset,size)
63 IO.pure(File & Listing,directory_fetched(read,count))
64
65# The end record: entry count at byte 10, directory size at 12 and offset at 16.
66# A count or an offset of all ones means ZIP64, which a 32-bit file never needs.
67def end_found(found: Maybe<&2,U32>,+tail: List<&2,U32>,file: File) -> IO(File & Listing):
68 match found:
69 case None{}: IO.pure(File & Listing,(file,Unreadable{"is not a ZIP archive"}))
70 case Some{+start}:
71 +count = Bytes.u16_at(tail,U32.to_nat((start + 10 : U32)))
72 +size = Bytes.u32_at(tail,U32.to_nat((start + 12 : U32)))
73 +offset = Bytes.u32_at(tail,U32.to_nat((start + 16 : U32)))
74 ending(U32.is_eq(count,65535) || U32.is_eq(offset,4294967295),file,count,size,offset)
75
76def tail_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,file: File) -> IO(File & Listing):
77 match result:
78 case Fail{error}: IO.pure(File & Listing,(file,Unreadable{"cannot be read"}))
79 case Done{+tail}: end_found(Bytes.last_start(tail,end_signature(),0,None{}),tail,file)
80
81def tail_fetched(read: Read()) -> IO(File & Listing):
82 (file,result) = read
83 tail_read(result,file)
84
85# The end record is 22 bytes plus a comment of at most 65535.
86def measured(result: Result<&1,&1,U32 & String,U32>,file: File) -> IO(File & Listing):
87 match result:
88 case Fail{error}: IO.pure(File & Listing,(file,Unreadable{"cannot be measured"}))
89 case Done{+size}:
90 +tail = U32.min(size,65557)
91 do IO<File & Listing>:
92 read : Read() <- File.read_at(file,(size - tail : U32),tail)
93 tail_fetched(read)
94
95def sized(sized: Sized()) -> IO(File & Listing):
96 (file,result) = sized
97 measured(result,file)
98
99# The entries of an open file, in directory order.
100def directory(file: File) -> IO(File & Listing):
101 do IO<File & Listing>:
102 size : Sized() <- File.size(file)
103 sized(size)
104
105def find(records: List<&2,Record>,+name: List<&2,U32>) -> Maybe<&2,Record>:
106 match records:
107 case Nil{}: None{}
108 case Con{Record{+entry,+header,+length,+method},rest}:
109 Bool.pick(Maybe<&2,Record>,Bytes.same(entry,name),Some{Record{entry,header,length,method}},find(rest,name))
110
111def first_matching(records: List<&2,Record>,+suffix: List<&2,U32>) -> Maybe<&2,Record>:
112 match records:
113 case Nil{}: None{}
114 case Con{Record{+entry,+header,+length,+method},rest}:
115 Bool.pick(Maybe<&2,Record>,Bytes.ends(entry,suffix),Some{Record{entry,header,length,method}},first_matching(rest,suffix))
116
117# The local header is 30 bytes, then the name and the extra field; the data follows.
118def located(valid: Bool,+bytes: List<&2,U32>,+header: U32) -> Maybe<&2,U32>:
119 match valid:
120 case False{}: None{}
121 case True{}: Some{(header + 30 + Bytes.u16_at(bytes,26n) + Bytes.u16_at(bytes,28n) : U32)}
122
123def header_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+header: U32) -> Maybe<&2,U32>:
124 match result:
125 case Fail{error}: None{}
126 case Done{+bytes}: located(U32.is_eq(Bytes.u32_at(bytes,0n),local_signature()),bytes,header)
127
128def header_fetched(read: Read(),+header: U32) -> File & Maybe<&2,U32>:
129 (file,result) = read
130 (file,header_read(result,header))
131
132# The offset of the first byte of a stored entry. A compressed entry has none.
133def stored_offset(stored: Bool,file: File,+header: U32) -> IO(File & Maybe<&2,U32>):
134 match stored:
135 case True{}:
136 do IO<File & Maybe<&2,U32>>:
137 read : Read() <- File.read_at(file,header,30)
138 IO.pure(File & Maybe<&2,U32>,header_fetched(read,header))
139 case False{}: IO.pure(File & Maybe<&2,U32>,(file,None{}))
140
141def data_offset(file: File,+record: Record) -> IO(File & Maybe<&2,U32>):
142 Record{name,+header,length,+method} = record
143 stored_offset(U32.is_eq(method,0),file,header)
144
145def entry_read(result: Result<&1,&1,U32 & String,List<&2,U32>>,+length: U32) -> Maybe<&2,List<&2,U32>>:
146 match result:
147 case Fail{error}: None{}
148 case Done{+bytes}: Bool.pick(Maybe<&2,List<&2,U32>>,Nat.is_eq(List.length(&2,U32,bytes),U32.to_nat(length)),Some{bytes},None{})
149
150def entry_fetched(read: Read(),+length: U32) -> Fetched:
151 (file,result) = read
152 Fetched{file,entry_read(result,length)}
153
154def entry_at(offset: Maybe<&2,U32>,file: File,+length: U32) -> IO(Fetched):
155 match offset:
156 case None{}: IO.pure(Fetched,Fetched{file,None{}})
157 case Some{offset}:
158 do IO<Fetched>:
159 read : Read() <- File.read_at(file,offset,length)
160 IO.pure(Fetched,entry_fetched(read,length))
161
162def entry_located(located: File & Maybe<&2,U32>,+length: U32) -> IO(Fetched):
163 (file,offset) = located
164 entry_at(offset,file,length)
165
166# Every byte of a stored entry in one read, for small entries.
167def entry(file: File,+record: Record) -> IO(Fetched):
168 Record{name,header,+length,method} = record
169 do IO<Fetched>:
170 located : File & Maybe<&2,U32> <- data_offset(file,Record{name,header,length,method})
171 entry_located(located,length)