REFERENCE / ZLIB × LEAN
Schema.lean
Source snapshot ·
1b5824d6534d0536 · Source at the matching commit ↗Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.
1import ZlibF.Runtime.Space
2
3/-!
4# Runtime schema (GENERATED, do not edit)
5
6Generated by `scripts/gen_schema.py` from the C headers of the verified source (zlib commit `757f0527154291bcf6bfbd6396ecde6bedd2db95`).
7Default build: x86_64 Linux, LP64. The decisions are explained in `docs/runtime-schema.md`.
8
9Contents: the constants of the headers, the reference types (where an array or a struct lives), the record of
10every struct with all its fields in declaration order, the static tables, and the heap with one table per kind
11of object. Nothing here is a computation on the heap; the primitives are in the other files of `Runtime/`.
12-/
13
14namespace C
15
16/-! ## Constants of the headers (object-like macros that evaluate to an integer or a string) -/
17
18def BL_CODES : Int32 := 19
19def BUSY_STATE : Int32 := 113
20def Buf_size : Int32 := 16
21def COMMENT_STATE : Int32 := 91
22def DEF_MEM_LEVEL : Int32 := 8
23def DEF_WBITS : Int32 := 15
24def DYN_TREES : Int32 := 2
25def D_CODES : Int32 := 30
26def ENOUGH : Int32 := 1444
27def ENOUGH_DISTS : Int32 := 592
28def ENOUGH_LENS : Int32 := 852
29def EXTRA_STATE : Int32 := 69
30def FINISH_STATE : Int32 := 666
31def GZBUFSIZE : Int32 := 8192
32def GZIP : Int32 := 2
33def GZIP_STATE : Int32 := 57
34def GZ_APPEND : Int32 := 1
35/-- The macro `COPY` of the headers (`COPY = 1`). The name `COPY` itself is the enumerator of `inflate.h` below. -/
36def GZ_COPY : Int32 := 1
37def GZ_NONE : Int32 := 0
38def GZ_READ : Int32 := 7247
39def GZ_WRITE : Int32 := 31153
40def HCRC_STATE : Int32 := 103
41def HEAP_SIZE : Int32 := 573
42def INIT_STATE : Int32 := 42
43def LENGTH_CODES : Int32 := 29
44def LITERALS : Int32 := 256
45def LIT_BUFS : Int32 := 4
46def LOOK : Int32 := 0
47def L_CODES : Int32 := 286
48def MAX_BITS : Int32 := 15
49def MAX_MATCH : Int32 := 258
50def MAX_MEM_LEVEL : Int32 := 9
51def MAX_WBITS : Int32 := 15
52def MIN_LOOKAHEAD : Int32 := 262
53def MIN_MATCH : Int32 := 3
54def NAME_STATE : Int32 := 73
55def OS_CODE : Int32 := 3
56def PRESET_DICT : Int32 := 32
57def STATIC_TREES : Int32 := 1
58def STORED_BLOCK : Int32 := 0
59def WIN_INIT : Int32 := 258
60def ZLIB_VERNUM : Int32 := 4897
61def ZLIB_VER_MAJOR : Int32 := 1
62def ZLIB_VER_MINOR : Int32 := 3
63def ZLIB_VER_REVISION : Int32 := 2
64def ZLIB_VER_SUBREVISION : Int32 := 1
65def Z_ASCII : Int32 := 1
66def Z_BEST_COMPRESSION : Int32 := 9
67def Z_BEST_SPEED : Int32 := 1
68def Z_BINARY : Int32 := 0
69def Z_BLOCK : Int32 := 5
70def Z_BUF_ERROR : Int32 := (-5 : Int32)
71def Z_DATA_ERROR : Int32 := (-3 : Int32)
72def Z_DEFAULT_COMPRESSION : Int32 := (-1 : Int32)
73def Z_DEFAULT_STRATEGY : Int32 := 0
74def Z_DEFLATED : Int32 := 8
75def Z_ERRNO : Int32 := (-1 : Int32)
76def Z_FILTERED : Int32 := 1
77def Z_FINISH : Int32 := 4
78def Z_FIXED : Int32 := 4
79def Z_FULL_FLUSH : Int32 := 3
80def Z_HUFFMAN_ONLY : Int32 := 2
81def Z_MEM_ERROR : Int32 := (-4 : Int32)
82def Z_NEED_DICT : Int32 := 2
83def Z_NO_COMPRESSION : Int32 := 0
84def Z_NO_FLUSH : Int32 := 0
85def Z_NULL : Int32 := 0
86def Z_OK : Int32 := 0
87def Z_PARTIAL_FLUSH : Int32 := 1
88def Z_RLE : Int32 := 3
89def Z_STREAM_END : Int32 := 1
90def Z_STREAM_ERROR : Int32 := (-2 : Int32)
91def Z_SYNC_FLUSH : Int32 := 2
92def Z_TEXT : Int32 := 1
93def Z_TREES : Int32 := 6
94def Z_UNKNOWN : Int32 := 2
95def Z_VERSION_ERROR : Int32 := (-6 : Int32)
96def _LARGEFILE_SOURCE : Int32 := 1
97def ZLIB_VERSION : String := "1.3.2.1-motley"
98
99/-! ## Enumerators
100
101In C an enumeration constant has type `int`. The object of enum type (`inflate_state.mode`, the `type` argument of
102`inflate_table`) is stored as `unsigned int` by gcc, so the plain name `X` is a `UInt32`: it is right for a comparison
103with such an object (the `int` constant is converted to `unsigned int`). Where the constant meets an `int`
104(`x < HEAD` with `int x`, `-CODES`, arithmetic), use `X_i`, which is the `Int32` constant. -/
105
106def CODES : UInt32 := 0
107def LENS : UInt32 := 1
108def DISTS : UInt32 := 2
109/-- The enumeration constant `CODES` with its C type `int`. -/
110def CODES_i : Int32 := 0
111/-- The enumeration constant `LENS` with its C type `int`. -/
112def LENS_i : Int32 := 1
113/-- The enumeration constant `DISTS` with its C type `int`. -/
114def DISTS_i : Int32 := 2
115def HEAD : UInt32 := 16180
116def FLAGS : UInt32 := 16181
117def TIME : UInt32 := 16182
118def OS : UInt32 := 16183
119def EXLEN : UInt32 := 16184
120def EXTRA : UInt32 := 16185
121def NAME : UInt32 := 16186
122def COMMENT : UInt32 := 16187
123def HCRC : UInt32 := 16188
124def DICTID : UInt32 := 16189
125def DICT : UInt32 := 16190
126def TYPE : UInt32 := 16191
127def TYPEDO : UInt32 := 16192
128def STORED : UInt32 := 16193
129def COPY_ : UInt32 := 16194
130def COPY : UInt32 := 16195
131def TABLE : UInt32 := 16196
132def LENLENS : UInt32 := 16197
133def CODELENS : UInt32 := 16198
134def LEN_ : UInt32 := 16199
135def LEN : UInt32 := 16200
136def LENEXT : UInt32 := 16201
137def DIST : UInt32 := 16202
138def DISTEXT : UInt32 := 16203
139def MATCH : UInt32 := 16204
140def LIT : UInt32 := 16205
141def CHECK : UInt32 := 16206
142def LENGTH : UInt32 := 16207
143def DONE : UInt32 := 16208
144def BAD : UInt32 := 16209
145def MEM : UInt32 := 16210
146def SYNC : UInt32 := 16211
147/-- The enumeration constant `HEAD` with its C type `int`. -/
148def HEAD_i : Int32 := 16180
149/-- The enumeration constant `FLAGS` with its C type `int`. -/
150def FLAGS_i : Int32 := 16181
151/-- The enumeration constant `TIME` with its C type `int`. -/
152def TIME_i : Int32 := 16182
153/-- The enumeration constant `OS` with its C type `int`. -/
154def OS_i : Int32 := 16183
155/-- The enumeration constant `EXLEN` with its C type `int`. -/
156def EXLEN_i : Int32 := 16184
157/-- The enumeration constant `EXTRA` with its C type `int`. -/
158def EXTRA_i : Int32 := 16185
159/-- The enumeration constant `NAME` with its C type `int`. -/
160def NAME_i : Int32 := 16186
161/-- The enumeration constant `COMMENT` with its C type `int`. -/
162def COMMENT_i : Int32 := 16187
163/-- The enumeration constant `HCRC` with its C type `int`. -/
164def HCRC_i : Int32 := 16188
165/-- The enumeration constant `DICTID` with its C type `int`. -/
166def DICTID_i : Int32 := 16189
167/-- The enumeration constant `DICT` with its C type `int`. -/
168def DICT_i : Int32 := 16190
169/-- The enumeration constant `TYPE` with its C type `int`. -/
170def TYPE_i : Int32 := 16191
171/-- The enumeration constant `TYPEDO` with its C type `int`. -/
172def TYPEDO_i : Int32 := 16192
173/-- The enumeration constant `STORED` with its C type `int`. -/
174def STORED_i : Int32 := 16193
175/-- The enumeration constant `COPY_` with its C type `int`. -/
176def COPY__i : Int32 := 16194
177/-- The enumeration constant `COPY` with its C type `int`. -/
178def COPY_i : Int32 := 16195
179/-- The enumeration constant `TABLE` with its C type `int`. -/
180def TABLE_i : Int32 := 16196
181/-- The enumeration constant `LENLENS` with its C type `int`. -/
182def LENLENS_i : Int32 := 16197
183/-- The enumeration constant `CODELENS` with its C type `int`. -/
184def CODELENS_i : Int32 := 16198
185/-- The enumeration constant `LEN_` with its C type `int`. -/
186def LEN__i : Int32 := 16199
187/-- The enumeration constant `LEN` with its C type `int`. -/
188def LEN_i : Int32 := 16200
189/-- The enumeration constant `LENEXT` with its C type `int`. -/
190def LENEXT_i : Int32 := 16201
191/-- The enumeration constant `DIST` with its C type `int`. -/
192def DIST_i : Int32 := 16202
193/-- The enumeration constant `DISTEXT` with its C type `int`. -/
194def DISTEXT_i : Int32 := 16203
195/-- The enumeration constant `MATCH` with its C type `int`. -/
196def MATCH_i : Int32 := 16204
197/-- The enumeration constant `LIT` with its C type `int`. -/
198def LIT_i : Int32 := 16205
199/-- The enumeration constant `CHECK` with its C type `int`. -/
200def CHECK_i : Int32 := 16206
201/-- The enumeration constant `LENGTH` with its C type `int`. -/
202def LENGTH_i : Int32 := 16207
203/-- The enumeration constant `DONE` with its C type `int`. -/
204def DONE_i : Int32 := 16208
205/-- The enumeration constant `BAD` with its C type `int`. -/
206def BAD_i : Int32 := 16209
207/-- The enumeration constant `MEM` with its C type `int`. -/
208def MEM_i : Int32 := 16210
209/-- The enumeration constant `SYNC` with its C type `int`. -/
210def SYNC_i : Int32 := 16211
211
212/-! ## String literals
213
214A string literal of C is a static array of bytes: read-only, alive for the whole run, never freed, and the same
215object every time the literal is evaluated. `strTable` lists every string literal of the library sources (the
216`*.c` and `*.h` files of the top directory of the verified source, comments excluded, adjacent literals joined,
217plus the empty string), sorted. The literal number `i` is the array `strTable[i]` followed by a NUL byte, and
218`BRef.str i` is where it lives. It is not a block of the heap: it is not in any table, not in `Heap.live`, not
219touched by `nextBlk`, and the same in every heap. `strLitRef` (in `Libc.lean`) is the pointer to a literal. -/
220
221/-- The string literals of the library sources, sorted (177 of them). Bytes are ASCII. -/
222def strTable : Array String := #[
223 "",
224 "\n ",
225 "\n#else /* W == 4 */\n\nlocal const z_crc_t FAR crc_braid_table[][256] = {\n",
226 "\n#else /* W == 4 */\n\nlocal const z_word_t FAR crc_big_table[] = {\n ",
227 "\n#endif\n",
228 "\n#if N == %d\n",
229 "\n#if W == 8\n\nlocal const z_crc_t FAR crc_braid_table[][256] = {\n",
230 "\n#ifdef W\n\n#if W == 8\n\nlocal const z_word_t FAR crc_big_table[] = {\n ",
231 "\nbit length overflow\n",
232 "\nbl code %2d ",
233 "\nbl counts: ",
234 "\nbl tree: sent %lu",
235 "\ncd %3d ",
236 "\ncomprlen %lu(%lu) ",
237 "\ndist data: dyn %lu, stat %lu",
238 "\ndist tree: sent %lu",
239 "\ndyn trees: dyn %lu, stat %lu",
240 "\ngen_codes: max_code %d ",
241 "\nlit data: dyn %lu, stat %lu",
242 "\nlit tree: sent %lu",
243 "\nlocal const z_crc_t FAR x2n_table[] = {\n ",
244 "\nn %3d %c l %2d c %4x (%x) ",
245 "\nnode %d(%d), sons %d(%d) %d(%d)",
246 "\nopt %lu(%lu) stat %lu(%lu) stored %lu lit %u ",
247 "\nstatic const code distfix[%u] = {",
248 "\n};",
249 "\n};\n\n",
250 " ",
251 " It is part of the implementation of this library and is",
252 " subject to change. Applications should only use zlib.h.",
253 " {",
254 " '%c' ",
255 " (last)",
256 " * Generated automatically by makefixed().",
257 " */",
258 " 3_6?",
259 " deflate 1.3.2.1 Copyright 1995-2026 Jean-loup Gailly and Mark Adler ",
260 " inflate 1.3.2.1 Copyright 1995-2026 Mark Adler ",
261 " l %2d v %4x ",
262 " start %u, match %d, length %d\n",
263 "%1u%s",
264 "%2u%s",
265 "%5u%s",
266 "%c",
267 "%s",
268 "%s\n",
269 "%s%s%s",
270 "%s0x%016llx%s",
271 "%s0x%08lx%s",
272 "(%02x %02x)",
273 "+r",
274 ",\n",
275 ", ",
276 "/* WARNING: this file should *not* be used by applications.",
277 "/* crc32.h -- tables for rapid CRC calculation\n * Generated automatically by crc32.c\n */\n\nlocal const z_crc_t FAR crc_table[] = {\n ",
278 "/* header created automatically with -DGEN_TREES_H */\n\n",
279 "/* inffixed.h -- table for decoding fixed codes",
280 "1.3.2.1-motley",
281 ": ",
282 "<fd:%d>",
283 "C",
284 "Can't open trees.h",
285 "Code too clever",
286 "[FLUSH]",
287 "\\[%d,%d]",
288 "_tr_tally: bad match",
289 "already enough lookahead",
290 "bad compressed size",
291 "bad d_code",
292 "buffer error",
293 "code %d bits %d->%d\n",
294 "compressed data error",
295 "const uch ZLIB_INTERNAL _dist_code[DIST_CODE_LEN] = {\n",
296 "const uch ZLIB_INTERNAL _length_code[MAX_MATCH-MIN_MATCH+1]= {\n",
297 "crc32.h",
298 "crc32b %w0, %w0, %w1",
299 "crc32x %w0, %w0, %x1",
300 "ctx=stm",
301 "data error",
302 "file error",
303 "header crc mismatch",
304 "hidden",
305 "incompatible version",
306 "inconsistent bit counts",
307 "incorrect data check",
308 "incorrect header check",
309 "incorrect length check",
310 "inflate.c too far\n",
311 "inflate: distance %u\n",
312 "inflate: end of block\n",
313 "inflate: length %u\n",
314 "inflate: literal '%c'\n",
315 "inflate: literal 0x%02x\n",
316 "inflate: code lengths ok\n",
317 "inflate: codes ok\n",
318 "inflate: stored end\n",
319 "inflate: stored length %u\n",
320 "inflate: table sizes ok\n",
321 "inflate: dynamic codes block%s\n",
322 "inflate: fixed codes block%s\n",
323 "inflate: stored block%s\n",
324 "inflate: check matches trailer\n",
325 "inflate: dictionary set\n",
326 "inflate: length matches trailer\n",
327 "inflate: zlib header ok\n",
328 "inflate: allocated\n",
329 "inflate: end\n",
330 "inflate: reset\n",
331 "insufficient memory",
332 "internal error: deflate stream corrupt",
333 "internal error: inflate stream corrupt",
334 "invalid bit length repeat",
335 "invalid block type",
336 "invalid code -- missing end-of-block",
337 "invalid code lengths set",
338 "invalid distance code",
339 "invalid distance too far back",
340 "invalid distances set",
341 "invalid length",
342 "invalid literal/length code",
343 "invalid literal/lengths set",
344 "invalid match",
345 "invalid stored block lengths",
346 "invalid window size",
347 "local const ct_data static_dtree[D_CODES] = {\n",
348 "local const ct_data static_ltree[L_CODES+2] = {\n",
349 "local const int base_dist[D_CODES] = {\n",
350 "local const int base_length[LENGTH_CODES] = {\n",
351 "lost buf",
352 "match[2]?",
353 "mbc=60",
354 "memory",
355 "more < 2",
356 "mrs=512",
357 "need dictionary",
358 "need lookahead",
359 "no flush?",
360 "no future",
361 "not enough codes",
362 "not enough room for search",
363 "out of memory",
364 "out of room to push characters",
365 "pendingBuf overflow",
366 "r",
367 "request does not fit in a size_t",
368 "request does not fit in an int",
369 "requested length does not fit in int",
370 "rfm=fix",
371 "scan[2]?",
372 "stalled write on gzprintf",
373 "state corrupt",
374 "static const code lenfix[%u] = {",
375 "stdio error (consult errno)",
376 "stream end",
377 "stream error",
378 "string length does not fit in int",
379 "too many codes",
380 "too many length or distance symbols",
381 "tr_static_init: 256 + dist != 512",
382 "tr_static_init: dist != 256",
383 "tr_static_init: length != 256",
384 "trees.h",
385 "unexpected end of file",
386 "unknown compression method",
387 "unknown header flags set",
388 "unknown win32 error (%ld)",
389 "w",
390 "wild scan",
391 "zcfree: ptr not found",
392 "{%u,%u,%d}",
393 "{{%2u},{%2u}}%s",
394 "{{%3u},{%3u}}%s",
395 "}%s",
396 "};\n",
397 "};\n\n#endif\n",
398 "};\n\n#endif\n\n#endif\n",
399 "};\n\nlocal const z_word_t FAR crc_braid_big_table[][256] = {\n"
400]
401
402/-- The bytes of a string literal in memory: its text and the terminating NUL. -/
403def strBytes (s : String) : Array UInt8 := s.toUTF8.data.push 0
404
405/-! ## Where an array or a struct lives (reference types) -/
406
407/-- Where an array of `Int32` lives. -/
408inductive IRef where
409 /-- the array `heap` inside the DeflateState with this block number -/
410 | dstate_heap (id : Nat)
411 /-- the static table `base_dist` (read-only) -/
412 | st_base_dist
413 /-- the static table `base_length` (read-only) -/
414 | st_base_length
415 /-- the static table `extra_lbits` (read-only) -/
416 | st_extra_lbits
417 /-- the static table `extra_dbits` (read-only) -/
418 | st_extra_dbits
419 /-- the static table `extra_blbits` (read-only) -/
420 | st_extra_blbits
421 deriving DecidableEq, Inhabited
422
423/-- A pointer into an array of `Int32`: null, or an array and an index. -/
424abbrev IPtr := Ptr IRef
425
426/-- Where an array of `UInt16` lives. -/
427inductive WRef where
428 /-- a block of 16-bit words of the heap (table `words`) -/
429 | blk (b : Nat)
430 /-- the array `bl_count` inside the DeflateState with this block number -/
431 | dstate_bl_count (id : Nat)
432 /-- the array `lens` inside the InflateState with this block number -/
433 | istate_lens (id : Nat)
434 /-- the array `work` inside the InflateState with this block number -/
435 | istate_work (id : Nat)
436 deriving DecidableEq, Inhabited
437
438/-- A pointer into an array of `UInt16`: null, or an array and an index. -/
439abbrev WPtr := Ptr WRef
440
441/-- Where an array of `UInt32` lives. -/
442inductive URef where
443 /-- the static table `crc_table` (read-only) -/
444 | st_crc_table
445 /-- the static table `x2n_table` (read-only) -/
446 | st_x2n_table
447 deriving DecidableEq, Inhabited
448
449/-- A pointer into an array of `UInt32`: null, or an array and an index. -/
450abbrev UPtr := Ptr URef
451
452/-- Where an array of `UInt8` lives. -/
453inductive BRef where
454 /-- a byte block of the heap (table `bytes`) -/
455 | blk (b : Nat)
456 /-- the string literal number `i` of `strTable` (read-only, never freed, not a block of the heap) -/
457 | str (i : Nat)
458 /-- the array `depth` inside the DeflateState with this block number -/
459 | dstate_depth (id : Nat)
460 /-- the static table `dist_code` (read-only) -/
461 | st_dist_code
462 /-- the static table `length_code` (read-only) -/
463 | st_length_code
464 deriving DecidableEq, Inhabited
465
466/-- A pointer into an array of `UInt8`: null, or an array and an index. -/
467abbrev BPtr := Ptr BRef
468
469/-- Identities whose byte-array origin has symbolic low address bits. Raw blocks retain their aligned origin. -/
470inductive ByteBaseRef where
471 /-- the string literal number `i` of `strTable` (read-only, never freed, not a block of the heap) -/
472 | str (i : Nat)
473 /-- the array `depth` inside the DeflateState with this block number -/
474 | dstate_depth (id : Nat)
475 /-- the static table `dist_code` (read-only) -/
476 | st_dist_code
477 /-- the static table `length_code` (read-only) -/
478 | st_length_code
479 deriving DecidableEq, Inhabited
480
481/-- Where an array of `Code` lives. -/
482inductive CodeRef where
483 /-- the array `codes` inside the InflateState with this block number -/
484 | istate_codes (id : Nat)
485 /-- the static table `lenfix` (read-only) -/
486 | st_lenfix
487 /-- the static table `distfix` (read-only) -/
488 | st_distfix
489 deriving DecidableEq, Inhabited
490
491/-- A pointer into an array of `Code`: null, or an array and an index. -/
492abbrev CodePtr := Ptr CodeRef
493
494/-- Where an array of `CtData` lives. -/
495inductive CtDataRef where
496 /-- the array `dyn_ltree` inside the DeflateState with this block number -/
497 | dstate_dyn_ltree (id : Nat)
498 /-- the array `dyn_dtree` inside the DeflateState with this block number -/
499 | dstate_dyn_dtree (id : Nat)
500 /-- the array `bl_tree` inside the DeflateState with this block number -/
501 | dstate_bl_tree (id : Nat)
502 /-- the static table `static_dtree` (read-only) -/
503 | st_static_dtree
504 /-- the static table `static_ltree` (read-only) -/
505 | st_static_ltree
506 deriving DecidableEq, Inhabited
507
508/-- A pointer into an array of `CtData`: null, or an array and an index. -/
509abbrev CtDataPtr := Ptr CtDataRef
510
511/-- Where a `z_stream` lives. -/
512inductive ZStreamRef where
513 /-- entry `id` of the table `streams` -/
514 | tab (id : Nat)
515 /-- the field `strm` of the GzState with this block number -/
516 | in_gzstate_strm (id : Nat)
517 deriving DecidableEq, Inhabited
518
519abbrev ZStreamPtr := Option ZStreamRef
520
521/-- Where a `gz_header` lives. -/
522inductive GzHeaderRef where
523 /-- entry `id` of the table `gzheaders` -/
524 | tab (id : Nat)
525 deriving DecidableEq, Inhabited
526
527abbrev GzHeaderPtr := Option GzHeaderRef
528
529/-- Where a `deflate_state` lives. -/
530inductive DeflateStateRef where
531 /-- entry `id` of the table `dstates` -/
532 | tab (id : Nat)
533 deriving DecidableEq, Inhabited
534
535abbrev DeflateStatePtr := Option DeflateStateRef
536
537/-- Where a `inflate_state` lives. -/
538inductive InflateStateRef where
539 /-- entry `id` of the table `istates` -/
540 | tab (id : Nat)
541 deriving DecidableEq, Inhabited
542
543abbrev InflateStatePtr := Option InflateStateRef
544
545/-- Where a `gz_state` lives. -/
546inductive GzStateRef where
547 /-- entry `id` of the table `gzstates` -/
548 | tab (id : Nat)
549 deriving DecidableEq, Inhabited
550
551abbrev GzStatePtr := Option GzStateRef
552
553/-- Where a `gzFile_s` lives. -/
554inductive GzFileRef where
555 /-- the field `x` of the GzState with this block number -/
556 | in_gzstate_x (id : Nat)
557 deriving DecidableEq, Inhabited
558
559abbrev GzFilePtr := Option GzFileRef
560
561/-- Where a `tree_desc` lives. -/
562inductive TreeDescRef where
563 /-- the field `l_desc` of the DeflateState with this block number -/
564 | in_dstate_l_desc (id : Nat)
565 /-- the field `d_desc` of the DeflateState with this block number -/
566 | in_dstate_d_desc (id : Nat)
567 /-- the field `bl_desc` of the DeflateState with this block number -/
568 | in_dstate_bl_desc (id : Nat)
569 deriving DecidableEq, Inhabited
570
571abbrev TreeDescPtr := Option TreeDescRef
572
573/-- Where a `static_tree_desc` lives. -/
574inductive StaticTreeDescRef where
575 /-- the static instance `static_l_desc` (read-only) -/
576 | st_static_l_desc
577 /-- the static instance `static_d_desc` (read-only) -/
578 | st_static_d_desc
579 /-- the static instance `static_bl_desc` (read-only) -/
580 | st_static_bl_desc
581 deriving DecidableEq, Inhabited
582
583abbrev StaticTreeDescPtr := Option StaticTreeDescRef
584
585/-- `struct internal_state *`: a deflate state or an inflate state. -/
586inductive StateRef where
587 | deflate (id : Nat)
588 | inflate (id : Nat)
589 deriving DecidableEq, Inhabited
590
591/-! ## Records (all fields, in declaration order) -/
592
593/-- `struct z_stream`. -/
594structure ZStream where
595 /-- `Bytef *` -/
596 next_in : BPtr
597 /-- `uInt` -/
598 avail_in : UInt32
599 /-- `uLong` -/
600 total_in : UInt64
601 /-- `Bytef *` -/
602 next_out : BPtr
603 /-- `uInt` -/
604 avail_out : UInt32
605 /-- `uLong` -/
606 total_out : UInt64
607 /-- `char *` -/
608 msg : BPtr
609 /-- `struct internal_state *` -/
610 state : Option StateRef
611 /-- `alloc_func` -/
612 zalloc : FnPtr
613 /-- `free_func` -/
614 zfree : FnPtr
615 /-- `voidpf` -/
616 «opaque» : BPtr
617 /-- `int` -/
618 data_type : Int32
619 /-- `uLong` -/
620 adler : UInt64
621 /-- `uLong` -/
622 reserved : UInt64
623 deriving Inhabited
624
625/-- `struct gz_header`. -/
626structure GzHeader where
627 /-- `int` -/
628 text : Int32
629 /-- `uLong` -/
630 time : UInt64
631 /-- `int` -/
632 xflags : Int32
633 /-- `int` -/
634 os : Int32
635 /-- `Bytef *` -/
636 extra : BPtr
637 /-- `uInt` -/
638 extra_len : UInt32
639 /-- `uInt` -/
640 extra_max : UInt32
641 /-- `Bytef *` -/
642 name : BPtr
643 /-- `uInt` -/
644 name_max : UInt32
645 /-- `Bytef *` -/
646 comment : BPtr
647 /-- `uInt` -/
648 comm_max : UInt32
649 /-- `int` -/
650 hcrc : Int32
651 /-- `int` -/
652 done : Int32
653 deriving Inhabited
654
655/-- `struct ct_data`. -/
656structure CtData where
657 /-- `union { ush freq; ush code }` -/
658 fc : UInt16
659 /-- `union { ush dad; ush len }` -/
660 dl : UInt16
661 deriving Inhabited
662
663/-- `struct tree_desc`. -/
664structure TreeDesc where
665 /-- `ct_data *` -/
666 dyn_tree : CtDataPtr
667 /-- `int` -/
668 max_code : Int32
669 /-- `const static_tree_desc *` -/
670 stat_desc : Option StaticTreeDescRef
671 deriving Inhabited
672
673/-- `struct deflate_state`. -/
674structure DeflateState where
675 /-- `z_streamp` -/
676 strm : Option ZStreamRef
677 /-- `int` -/
678 status : Int32
679 /-- `Bytef *` -/
680 pending_buf : BPtr
681 /-- `ulg` -/
682 pending_buf_size : UInt64
683 /-- `Bytef *` -/
684 pending_out : BPtr
685 /-- `ulg` -/
686 pending : UInt64
687 /-- `int` -/
688 wrap : Int32
689 /-- `gz_headerp` -/
690 gzhead : Option GzHeaderRef
691 /-- `ulg` -/
692 gzindex : UInt64
693 /-- `Byte` -/
694 method : UInt8
695 /-- `int` -/
696 last_flush : Int32
697 /-- `uInt` -/
698 w_size : UInt32
699 /-- `uInt` -/
700 w_bits : UInt32
701 /-- `uInt` -/
702 w_mask : UInt32
703 /-- `Bytef *` -/
704 window : BPtr
705 /-- `ulg` -/
706 window_size : UInt64
707 /-- `Posf *` -/
708 prev : WPtr
709 /-- `Posf *` -/
710 head : WPtr
711 /-- `uInt` -/
712 ins_h : UInt32
713 /-- `uInt` -/
714 hash_size : UInt32
715 /-- `uInt` -/
716 hash_bits : UInt32
717 /-- `uInt` -/
718 hash_mask : UInt32
719 /-- `uInt` -/
720 hash_shift : UInt32
721 /-- `long` -/
722 block_start : Int64
723 /-- `uInt` -/
724 match_length : UInt32
725 /-- `IPos` -/
726 prev_match : UInt32
727 /-- `int` -/
728 match_available : Int32
729 /-- `uInt` -/
730 strstart : UInt32
731 /-- `uInt` -/
732 match_start : UInt32
733 /-- `uInt` -/
734 lookahead : UInt32
735 /-- `uInt` -/
736 prev_length : UInt32
737 /-- `uInt` -/
738 max_chain_length : UInt32
739 /-- `uInt` -/
740 max_lazy_match : UInt32
741 /-- `int` -/
742 level : Int32
743 /-- `int` -/
744 strategy : Int32
745 /-- `uInt` -/
746 good_match : UInt32
747 /-- `int` -/
748 nice_match : Int32
749 /-- `struct ct_data_s[573]` -/
750 dyn_ltree : Array CtData
751 /-- `struct ct_data_s[61]` -/
752 dyn_dtree : Array CtData
753 /-- `struct ct_data_s[39]` -/
754 bl_tree : Array CtData
755 /-- `struct tree_desc_s` -/
756 l_desc : TreeDesc
757 /-- `struct tree_desc_s` -/
758 d_desc : TreeDesc
759 /-- `struct tree_desc_s` -/
760 bl_desc : TreeDesc
761 /-- `ush[16]` -/
762 bl_count : Array UInt16
763 /-- `int[573]` -/
764 heap : Array Int32
765 /-- `int` -/
766 heap_len : Int32
767 /-- `int` -/
768 heap_max : Int32
769 /-- `uch[573]` -/
770 depth : Array UInt8
771 /-- `uchf *` -/
772 sym_buf : BPtr
773 /-- `uInt` -/
774 lit_bufsize : UInt32
775 /-- `uInt` -/
776 sym_next : UInt32
777 /-- `uInt` -/
778 sym_end : UInt32
779 /-- `ulg` -/
780 opt_len : UInt64
781 /-- `ulg` -/
782 static_len : UInt64
783 /-- `uInt` -/
784 «matches» : UInt32
785 /-- `uInt` -/
786 insert : UInt32
787 /-- `ush` -/
788 bi_buf : UInt16
789 /-- `int` -/
790 bi_valid : Int32
791 /-- `int` -/
792 bi_used : Int32
793 /-- `ulg` -/
794 high_water : UInt64
795 /-- `int` -/
796 slid : Int32
797 deriving Inhabited
798
799/-- `struct code`. -/
800structure Code where
801 /-- `unsigned char` -/
802 op : UInt8
803 /-- `unsigned char` -/
804 bits : UInt8
805 /-- `unsigned short` -/
806 val : UInt16
807 deriving Inhabited
808
809/-- `struct inflate_state`. -/
810structure InflateState where
811 /-- `z_streamp` -/
812 strm : Option ZStreamRef
813 /-- `inflate_mode` -/
814 mode : UInt32
815 /-- `int` -/
816 last : Int32
817 /-- `int` -/
818 wrap : Int32
819 /-- `int` -/
820 reqwrap : Int32
821 /-- `int` -/
822 havedict : Int32
823 /-- `int` -/
824 flags : Int32
825 /-- `unsigned int` -/
826 dmax : UInt32
827 /-- `unsigned long` -/
828 check : UInt64
829 /-- `unsigned long` -/
830 total : UInt64
831 /-- `gz_headerp` -/
832 head : Option GzHeaderRef
833 /-- `unsigned int` -/
834 reqbits : UInt32
835 /-- `unsigned int` -/
836 wbits : UInt32
837 /-- `unsigned int` -/
838 wsize : UInt32
839 /-- `unsigned int` -/
840 whave : UInt32
841 /-- `unsigned int` -/
842 wnext : UInt32
843 /-- `unsigned char *` -/
844 window : BPtr
845 /-- `unsigned long` -/
846 hold : UInt64
847 /-- `unsigned int` -/
848 bits : UInt32
849 /-- `unsigned int` -/
850 length : UInt32
851 /-- `unsigned int` -/
852 offset : UInt32
853 /-- `unsigned int` -/
854 extra : UInt32
855 /-- `const code *` -/
856 lencode : CodePtr
857 /-- `const code *` -/
858 distcode : CodePtr
859 /-- `unsigned int` -/
860 lenbits : UInt32
861 /-- `unsigned int` -/
862 distbits : UInt32
863 /-- `unsigned int` -/
864 ncode : UInt32
865 /-- `unsigned int` -/
866 nlen : UInt32
867 /-- `unsigned int` -/
868 ndist : UInt32
869 /-- `unsigned int` -/
870 «have» : UInt32
871 /-- `code *` -/
872 next : CodePtr
873 /-- `unsigned short[320]` -/
874 lens : Array UInt16
875 /-- `unsigned short[288]` -/
876 work : Array UInt16
877 /-- `code[1444]` -/
878 codes : Array Code
879 /-- `int` -/
880 sane : Int32
881 /-- `int` -/
882 back : Int32
883 /-- `unsigned int` -/
884 was : UInt32
885 deriving Inhabited
886
887/-- `struct gzFile_s`. -/
888structure GzFile where
889 /-- `unsigned int` -/
890 «have» : UInt32
891 /-- `unsigned char *` -/
892 next : BPtr
893 /-- `off64_t` -/
894 pos : Int64
895 deriving Inhabited
896
897/-- `struct gz_state`. -/
898structure GzState where
899 /-- `struct gzFile_s` -/
900 x : GzFile
901 /-- `int` -/
902 mode : Int32
903 /-- `int` -/
904 fd : Int32
905 /-- `char *` -/
906 path : BPtr
907 /-- `unsigned int` -/
908 size : UInt32
909 /-- `unsigned int` -/
910 want : UInt32
911 /-- `unsigned char *` -/
912 «in» : BPtr
913 /-- `unsigned char *` -/
914 out : BPtr
915 /-- `int` -/
916 direct : Int32
917 /-- `int` -/
918 junk : Int32
919 /-- `int` -/
920 how : Int32
921 /-- `int` -/
922 again : Int32
923 /-- `off64_t` -/
924 start : Int64
925 /-- `int` -/
926 eof : Int32
927 /-- `int` -/
928 past : Int32
929 /-- `int` -/
930 level : Int32
931 /-- `int` -/
932 strategy : Int32
933 /-- `int` -/
934 reset : Int32
935 /-- `off64_t` -/
936 «skip» : Int64
937 /-- `int` -/
938 err : Int32
939 /-- `char *` -/
940 msg : BPtr
941 /-- `z_stream` -/
942 strm : ZStream
943 deriving Inhabited
944
945/-- `struct static_tree_desc`. -/
946structure StaticTreeDesc where
947 /-- `const ct_data *` -/
948 static_tree : CtDataPtr
949 /-- `const intf *` -/
950 extra_bits : IPtr
951 /-- `int` -/
952 extra_base : Int32
953 /-- `int` -/
954 elems : Int32
955 /-- `int` -/
956 max_length : Int32
957 deriving Inhabited
958
959/-! ## Static objects -/
960
961/-- The static tables and instances. Read-only: no primitive stores into them. Their contents are
962fixed by the translation of the file that defines them (see `docs/runtime-schema.md`). -/
963structure Statics where
964 /-- `_dist_code`, 512 elements, from header -/
965 dist_code : Array UInt8 := #[]
966 /-- `_length_code`, 256 elements, from header -/
967 length_code : Array UInt8 := #[]
968 /-- `base_dist`, 30 elements, from header -/
969 base_dist : Array Int32 := #[]
970 /-- `base_length`, 29 elements, from header -/
971 base_length : Array Int32 := #[]
972 /-- `crc_table`, 256 elements, from header -/
973 crc_table : Array UInt32 := #[]
974 /-- `static_dtree`, 30 elements, from header -/
975 static_dtree : Array CtData := #[]
976 /-- `static_ltree`, 288 elements, from header -/
977 static_ltree : Array CtData := #[]
978 /-- `x2n_table`, 32 elements, from header -/
979 x2n_table : Array UInt32 := #[]
980 /-- `lenfix`, 512 elements, from inffixed.h (included by inftrees.c; copy verbatim) -/
981 lenfix : Array Code := #[]
982 /-- `distfix`, 32 elements, from inffixed.h (included by inftrees.c; copy verbatim) -/
983 distfix : Array Code := #[]
984 /-- `extra_lbits`, 29 elements, from trees.c -/
985 extra_lbits : Array Int32 := #[]
986 /-- `extra_dbits`, 30 elements, from trees.c -/
987 extra_dbits : Array Int32 := #[]
988 /-- `extra_blbits`, 19 elements, from trees.c -/
989 extra_blbits : Array Int32 := #[]
990 /-- the instance `static_l_desc` of `struct static_tree_desc`, from trees.c -/
991 static_l_desc : StaticTreeDesc := default
992 /-- the instance `static_d_desc` of `struct static_tree_desc`, from trees.c -/
993 static_d_desc : StaticTreeDesc := default
994 /-- the instance `static_bl_desc` of `struct static_tree_desc`, from trees.c -/
995 static_bl_desc : StaticTreeDesc := default
996 deriving Inhabited
997
998/-! ## The heap -/
999
1000/-- The heap: one table per kind of object. A table maps a block number to the object, or to `none` when the
1001block is free or was never allocated. Block numbers are never reused. -/
1002structure Heap where
1003 /-- byte blocks (`unsigned char` arrays: buffers, windows, strings) -/
1004 bytes : Tbl (Option (Array UInt8))
1005 /-- blocks of 16-bit words (`head`, `prev`) -/
1006 words : Tbl (Option (Array UInt16))
1007 /-- the byte blocks that are read-only (string literals, `const` buffers) -/
1008 ro : Tbl Bool
1009 /-- the table of `struct z_stream` -/
1010 streams : Tbl (Option ZStream)
1011 /-- the table of `struct gz_header` -/
1012 gzheaders : Tbl (Option GzHeader)
1013 /-- the table of `struct deflate_state` -/
1014 dstates : Tbl (Option DeflateState)
1015 /-- the table of `struct inflate_state` -/
1016 istates : Tbl (Option InflateState)
1017 /-- the table of `struct gz_state` -/
1018 gzstates : Tbl (Option GzState)
1019 /-- the static tables -/
1020 static : Statics
1021 /-- the next unused block number -/
1022 nextBlk : Nat
1023 /-- the number of allocation calls so far -/
1024 nalloc : Nat
1025 /-- the failure oracle: allocation call number `n` succeeds iff `allocOk n` -/
1026 allocOk : Nat → Bool
1027 /-- the content of fresh memory: position `i` of the memory returned by allocation call number `n` -/
1028 garbage : Nat → Nat → UInt64
1029 /-- low three origin-address bits for static and embedded byte arrays; read-only metadata -/
1030 byteBase : ByteBaseRef → Fin 8
1031
1032/-- The heap with nothing allocated. -/
1033def Heap.empty : Heap where
1034 bytes := Tbl.empty
1035 words := Tbl.empty
1036 ro := Tbl.empty
1037 streams := Tbl.empty
1038 gzheaders := Tbl.empty
1039 dstates := Tbl.empty
1040 istates := Tbl.empty
1041 gzstates := Tbl.empty
1042 static := default
1043 nextBlk := 0
1044 nalloc := 0
1045 allocOk := fun _ => true
1046 garbage := fun _ _ => 0
1047 byteBase := fun _ => 0
1048
1049instance : Inhabited Heap := ⟨Heap.empty⟩
1050
1051/-- The block number `b` is in use: some table holds an object under it. -/
1052def Heap.live (h : Heap) (b : Nat) : Prop :=
1053 h.bytes b ≠ none ∨ h.words b ≠ none ∨ h.streams b ≠ none ∨ h.gzheaders b ≠ none ∨ h.dstates b ≠ none ∨ h.istates b ≠ none ∨ h.gzstates b ≠ none
1054
1055/-- Every block number from `nextBlk` on is unused. -/
1056def Fresh (h : Heap) : Prop := ∀ b, h.nextBlk ≤ b → ¬ h.live b
1057
1058/-- The heap with nothing allocated is `Fresh`. -/
1059theorem Heap.empty_fresh : Fresh Heap.empty := by
1060 intro b _ hl
1061 simp [Heap.live, Heap.empty] at hl
1062
1063/-- The decidable form of `Heap.live`: some table holds an object under the block number `b`. Every allocation
1064primitive tests it for the number it is about to use and faults if it is set, so an allocation never overwrites a
1065live object. -/
1066def Heap.slotUsed (h : Heap) (b : Nat) : Bool :=
1067 (h.bytes b).isSome || (h.words b).isSome || (h.streams b).isSome || (h.gzheaders b).isSome || (h.dstates b).isSome || (h.istates b).isSome || (h.gzstates b).isSome
1068
1069theorem Heap.slotUsed_eq_false {h : Heap} {b : Nat} : h.slotUsed b = false ↔ ¬ h.live b := by
1070 simp [Heap.slotUsed, Heap.live, and_assoc]
1071
1072/-- In a `Fresh` heap the number the next allocation takes is unused. -/
1073theorem Fresh.slotUsed_next {h : Heap} (hF : Fresh h) : h.slotUsed h.nextBlk = false :=
1074 Heap.slotUsed_eq_false.2 (hF h.nextBlk (Nat.le_refl _))
1075
1076/-- Discharges the hypothesis `h.slotUsed h.nextBlk = false` of the allocation rules (`allocB_some`, ...) from a
1077hypothesis of the context: itself, or `Fresh h`. -/
1078macro "fresh_slot" : tactic => `(tactic| first | assumption | exact Fresh.slotUsed_next ‹_›)
1079
1080/-- The live blocks are exactly those of `S`: the ownership statement, and with it the absence of leaks. -/
1081def Heap.Owns (h : Heap) (S : Nat → Prop) : Prop := ∀ b, h.live b ↔ S b
1082
1083theorem Heap.not_live {h : Heap} {b : Nat} :
1084 ¬ h.live b ↔ (h.bytes b = none ∧ h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧ h.istates b = none ∧ h.gzstates b = none) := by
1085 simp [Heap.live]
1086
1087/-- A heap whose tables agree with those of a `Fresh` heap from its own `nextBlk` on, and whose `nextBlk` is not
1088smaller, is `Fresh` too. -/
1089theorem Fresh.mono {h h' : Heap} (hF : Fresh h) (hnb : h.nextBlk ≤ h'.nextBlk)
1090 (ht : ∀ x, h'.nextBlk ≤ x → (h'.bytes x = h.bytes x ∧ h'.words x = h.words x ∧ h'.streams x = h.streams x ∧ h'.gzheaders x = h.gzheaders x ∧ h'.dstates x = h.dstates x ∧ h'.istates x = h.istates x ∧ h'.gzstates x = h.gzstates x)) : Fresh h' := by
1091 intro x hx hl
1092 obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := ht x hx
1093 apply hF x (Nat.le_trans hnb hx)
1094 unfold Heap.live at hl ⊢
1095 rw [e0, e1, e2, e3, e4, e5, e6] at hl
1096 exact hl
1097
1098/-- A live block number is below `nextBlk`. -/
1099theorem Fresh.lt {h : Heap} (hF : Fresh h) {b : Nat} (hl : h.live b) : b < h.nextBlk := by
1100 rcases Nat.lt_or_ge b h.nextBlk with hb | hb
1101 · exact hb
1102 · exact absurd hl (hF b hb)
1103
1104theorem Fresh.bytes {h : Heap} (hF : Fresh h) {b : Nat} (hb : h.nextBlk ≤ b) : h.bytes b = none := by
1105 cases hn : h.bytes b with
1106 | none => rfl
1107 | some a => exact absurd (Or.inl (by rw [hn]; simp)) (hF b hb)
1108
1109/-! ## Fresh memory of every record (`ZALLOC` does not initialise)
1110
1111Integers are arbitrary (the values `g i`). Pointers are NULL: this is a documented gap, not C: a pointer read from
1112uninitialised memory is indeterminate in C, and here it is a valid null (see `docs/trusted-base.md`, item 2).
1113`K.zeroed` is the same record with every integer 0: the content after `memset(p, 0, sizeof *p)`, where NULL
1114is the right value of every pointer. -/
1115
1116/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1117def ZStream.garbage (g : Nat → UInt64) : ZStream where
1118 next_in := default
1119 avail_in := Junk.of (g 0)
1120 total_in := Junk.of (g 1)
1121 next_out := default
1122 avail_out := Junk.of (g 2)
1123 total_out := Junk.of (g 3)
1124 msg := default
1125 state := default
1126 zalloc := default
1127 zfree := default
1128 «opaque» := default
1129 data_type := Junk.of (g 4)
1130 adler := Junk.of (g 5)
1131 reserved := Junk.of (g 6)
1132
1133/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1134def ZStream.zeroed : ZStream := ZStream.garbage (fun _ => 0)
1135
1136/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1137def GzHeader.garbage (g : Nat → UInt64) : GzHeader where
1138 text := Junk.of (g 0)
1139 time := Junk.of (g 1)
1140 xflags := Junk.of (g 2)
1141 os := Junk.of (g 3)
1142 extra := default
1143 extra_len := Junk.of (g 4)
1144 extra_max := Junk.of (g 5)
1145 name := default
1146 name_max := Junk.of (g 6)
1147 comment := default
1148 comm_max := Junk.of (g 7)
1149 hcrc := Junk.of (g 8)
1150 done := Junk.of (g 9)
1151
1152/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1153def GzHeader.zeroed : GzHeader := GzHeader.garbage (fun _ => 0)
1154
1155/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1156def CtData.garbage (g : Nat → UInt64) : CtData where
1157 fc := Junk.of (g 0)
1158 dl := Junk.of (g 1)
1159
1160/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1161def CtData.zeroed : CtData := CtData.garbage (fun _ => 0)
1162
1163/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1164def TreeDesc.garbage (g : Nat → UInt64) : TreeDesc where
1165 dyn_tree := default
1166 max_code := Junk.of (g 0)
1167 stat_desc := default
1168
1169/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1170def TreeDesc.zeroed : TreeDesc := TreeDesc.garbage (fun _ => 0)
1171
1172/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1173def DeflateState.garbage (g : Nat → UInt64) : DeflateState where
1174 strm := default
1175 status := Junk.of (g 0)
1176 pending_buf := default
1177 pending_buf_size := Junk.of (g 1)
1178 pending_out := default
1179 pending := Junk.of (g 2)
1180 wrap := Junk.of (g 3)
1181 gzhead := default
1182 gzindex := Junk.of (g 4)
1183 method := Junk.of (g 5)
1184 last_flush := Junk.of (g 6)
1185 w_size := Junk.of (g 7)
1186 w_bits := Junk.of (g 8)
1187 w_mask := Junk.of (g 9)
1188 window := default
1189 window_size := Junk.of (g 10)
1190 prev := default
1191 head := default
1192 ins_h := Junk.of (g 11)
1193 hash_size := Junk.of (g 12)
1194 hash_bits := Junk.of (g 13)
1195 hash_mask := Junk.of (g 14)
1196 hash_shift := Junk.of (g 15)
1197 block_start := Junk.of (g 16)
1198 match_length := Junk.of (g 17)
1199 prev_match := Junk.of (g 18)
1200 match_available := Junk.of (g 19)
1201 strstart := Junk.of (g 20)
1202 match_start := Junk.of (g 21)
1203 lookahead := Junk.of (g 22)
1204 prev_length := Junk.of (g 23)
1205 max_chain_length := Junk.of (g 24)
1206 max_lazy_match := Junk.of (g 25)
1207 level := Junk.of (g 26)
1208 strategy := Junk.of (g 27)
1209 good_match := Junk.of (g 28)
1210 nice_match := Junk.of (g 29)
1211 dyn_ltree := Array.ofFn (n := 573) fun i => CtData.garbage (fun j => g (30 + 2 * i.val + j))
1212 dyn_dtree := Array.ofFn (n := 61) fun i => CtData.garbage (fun j => g (1176 + 2 * i.val + j))
1213 bl_tree := Array.ofFn (n := 39) fun i => CtData.garbage (fun j => g (1298 + 2 * i.val + j))
1214 l_desc := TreeDesc.garbage (fun i => g (1376 + i))
1215 d_desc := TreeDesc.garbage (fun i => g (1377 + i))
1216 bl_desc := TreeDesc.garbage (fun i => g (1378 + i))
1217 bl_count := Array.ofFn (n := 16) fun i => Junk.of (g (1379 + i.val))
1218 heap := Array.ofFn (n := 573) fun i => Junk.of (g (1395 + i.val))
1219 heap_len := Junk.of (g 1968)
1220 heap_max := Junk.of (g 1969)
1221 depth := Array.ofFn (n := 573) fun i => Junk.of (g (1970 + i.val))
1222 sym_buf := default
1223 lit_bufsize := Junk.of (g 2543)
1224 sym_next := Junk.of (g 2544)
1225 sym_end := Junk.of (g 2545)
1226 opt_len := Junk.of (g 2546)
1227 static_len := Junk.of (g 2547)
1228 «matches» := Junk.of (g 2548)
1229 insert := Junk.of (g 2549)
1230 bi_buf := Junk.of (g 2550)
1231 bi_valid := Junk.of (g 2551)
1232 bi_used := Junk.of (g 2552)
1233 high_water := Junk.of (g 2553)
1234 slid := Junk.of (g 2554)
1235
1236/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1237def DeflateState.zeroed : DeflateState := DeflateState.garbage (fun _ => 0)
1238
1239/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1240def Code.garbage (g : Nat → UInt64) : Code where
1241 op := Junk.of (g 0)
1242 bits := Junk.of (g 1)
1243 val := Junk.of (g 2)
1244
1245/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1246def Code.zeroed : Code := Code.garbage (fun _ => 0)
1247
1248/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1249def InflateState.garbage (g : Nat → UInt64) : InflateState where
1250 strm := default
1251 mode := Junk.of (g 0)
1252 last := Junk.of (g 1)
1253 wrap := Junk.of (g 2)
1254 reqwrap := Junk.of (g 3)
1255 havedict := Junk.of (g 4)
1256 flags := Junk.of (g 5)
1257 dmax := Junk.of (g 6)
1258 check := Junk.of (g 7)
1259 total := Junk.of (g 8)
1260 head := default
1261 reqbits := Junk.of (g 9)
1262 wbits := Junk.of (g 10)
1263 wsize := Junk.of (g 11)
1264 whave := Junk.of (g 12)
1265 wnext := Junk.of (g 13)
1266 window := default
1267 hold := Junk.of (g 14)
1268 bits := Junk.of (g 15)
1269 length := Junk.of (g 16)
1270 offset := Junk.of (g 17)
1271 extra := Junk.of (g 18)
1272 lencode := default
1273 distcode := default
1274 lenbits := Junk.of (g 19)
1275 distbits := Junk.of (g 20)
1276 ncode := Junk.of (g 21)
1277 nlen := Junk.of (g 22)
1278 ndist := Junk.of (g 23)
1279 «have» := Junk.of (g 24)
1280 next := default
1281 lens := Array.ofFn (n := 320) fun i => Junk.of (g (25 + i.val))
1282 work := Array.ofFn (n := 288) fun i => Junk.of (g (345 + i.val))
1283 codes := Array.ofFn (n := 1444) fun i => Code.garbage (fun j => g (633 + 3 * i.val + j))
1284 sane := Junk.of (g 4965)
1285 back := Junk.of (g 4966)
1286 was := Junk.of (g 4967)
1287
1288/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1289def InflateState.zeroed : InflateState := InflateState.garbage (fun _ => 0)
1290
1291/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1292def GzFile.garbage (g : Nat → UInt64) : GzFile where
1293 «have» := Junk.of (g 0)
1294 next := default
1295 pos := Junk.of (g 1)
1296
1297/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1298def GzFile.zeroed : GzFile := GzFile.garbage (fun _ => 0)
1299
1300/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1301def GzState.garbage (g : Nat → UInt64) : GzState where
1302 x := GzFile.garbage (fun i => g (0 + i))
1303 mode := Junk.of (g 2)
1304 fd := Junk.of (g 3)
1305 path := default
1306 size := Junk.of (g 4)
1307 want := Junk.of (g 5)
1308 «in» := default
1309 out := default
1310 direct := Junk.of (g 6)
1311 junk := Junk.of (g 7)
1312 how := Junk.of (g 8)
1313 again := Junk.of (g 9)
1314 start := Junk.of (g 10)
1315 eof := Junk.of (g 11)
1316 past := Junk.of (g 12)
1317 level := Junk.of (g 13)
1318 strategy := Junk.of (g 14)
1319 reset := Junk.of (g 15)
1320 «skip» := Junk.of (g 16)
1321 err := Junk.of (g 17)
1322 msg := default
1323 strm := ZStream.garbage (fun i => g (18 + i))
1324
1325/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1326def GzState.zeroed : GzState := GzState.garbage (fun _ => 0)
1327
1328/-- A record whose integer fields are the arbitrary values `g 0`, `g 1`, ...; pointers are null. -/
1329def StaticTreeDesc.garbage (g : Nat → UInt64) : StaticTreeDesc where
1330 static_tree := default
1331 extra_bits := default
1332 extra_base := Junk.of (g 0)
1333 elems := Junk.of (g 1)
1334 max_length := Junk.of (g 2)
1335
1336/-- The record after `memset(p, 0, sizeof *p)` (`zmemzero`): every integer 0, every pointer NULL. -/
1337def StaticTreeDesc.zeroed : StaticTreeDesc := StaticTreeDesc.garbage (fun _ => 0)
1338
1339/-! ## Well-formed records
1340
1341The array fields of a record are `Array`s of any length. The C declares the length. `K.WellFormed v` says that every
1342array field of `v` (and of the records nested in it) has exactly the declared length, so that `Ptr.load` of an
1343index inside the array is a read inside the C object. Nothing in the runtime checks it: `K.garbage` and `K.zeroed`
1344are well-formed, `Heap.RecordsWellFormed` says that every record of the heap is, and the lemmas
1345`Heap.RecordsWellFormed.set_*` and `clear_*` show that storing a well-formed record or freeing one keeps it. A
1346theorem about a record must state this as a hypothesis. -/
1347
1348/-- Every entry of the table `t` satisfies `P`. -/
1349def TableWF {K : Type} (P : K → Prop) (t : Tbl (Option K)) : Prop := ∀ i v, t i = some v → P v
1350
1351theorem TableWF.set {K : Type} {P : K → Prop} {t : Tbl (Option K)} (ht : TableWF P t) (i : Nat) {v : K} (hv : P v) :
1352 TableWF P (upd t i (some v)) := by
1353 intro j w hw
1354 by_cases hj : j = i
1355 · subst hj; simp at hw; subst hw; exact hv
1356 · rw [upd_ne _ _ _ _ hj] at hw; exact ht j w hw
1357
1358theorem TableWF.clear {K : Type} {P : K → Prop} {t : Tbl (Option K)} (ht : TableWF P t) (i : Nat) :
1359 TableWF P (upd t i none) := by
1360 intro j w hw
1361 by_cases hj : j = i
1362 · subst hj; simp at hw
1363 · rw [upd_ne _ _ _ _ hj] at hw; exact ht j w hw
1364
1365/-- The array fields of a `z_stream` have the lengths of the C declaration. -/
1366def ZStream.WellFormed (v : ZStream) : Prop := True
1367
1368theorem ZStream.garbage_wf (g : Nat → UInt64) : (ZStream.garbage g).WellFormed := by
1369 simp [ZStream.garbage, ZStream.WellFormed]
1370
1371theorem ZStream.zeroed_wf : ZStream.zeroed.WellFormed := ZStream.garbage_wf _
1372
1373/-- The array fields of a `gz_header` have the lengths of the C declaration. -/
1374def GzHeader.WellFormed (v : GzHeader) : Prop := True
1375
1376theorem GzHeader.garbage_wf (g : Nat → UInt64) : (GzHeader.garbage g).WellFormed := by
1377 simp [GzHeader.garbage, GzHeader.WellFormed]
1378
1379theorem GzHeader.zeroed_wf : GzHeader.zeroed.WellFormed := GzHeader.garbage_wf _
1380
1381/-- The array fields of a `ct_data` have the lengths of the C declaration. -/
1382def CtData.WellFormed (v : CtData) : Prop := True
1383
1384theorem CtData.garbage_wf (g : Nat → UInt64) : (CtData.garbage g).WellFormed := by
1385 simp [CtData.garbage, CtData.WellFormed]
1386
1387theorem CtData.zeroed_wf : CtData.zeroed.WellFormed := CtData.garbage_wf _
1388
1389/-- The array fields of a `tree_desc` have the lengths of the C declaration. -/
1390def TreeDesc.WellFormed (v : TreeDesc) : Prop := True
1391
1392theorem TreeDesc.garbage_wf (g : Nat → UInt64) : (TreeDesc.garbage g).WellFormed := by
1393 simp [TreeDesc.garbage, TreeDesc.WellFormed]
1394
1395theorem TreeDesc.zeroed_wf : TreeDesc.zeroed.WellFormed := TreeDesc.garbage_wf _
1396
1397/-- The array fields of a `deflate_state` have the lengths of the C declaration. -/
1398def DeflateState.WellFormed (v : DeflateState) : Prop := v.dyn_ltree.size = 573 ∧ v.dyn_dtree.size = 61 ∧ v.bl_tree.size = 39 ∧ v.bl_count.size = 16 ∧ v.heap.size = 573 ∧ v.depth.size = 573
1399
1400theorem DeflateState.garbage_wf (g : Nat → UInt64) : (DeflateState.garbage g).WellFormed := by
1401 simp [DeflateState.garbage, DeflateState.WellFormed]
1402
1403theorem DeflateState.zeroed_wf : DeflateState.zeroed.WellFormed := DeflateState.garbage_wf _
1404
1405/-- The array fields of a `code` have the lengths of the C declaration. -/
1406def Code.WellFormed (v : Code) : Prop := True
1407
1408theorem Code.garbage_wf (g : Nat → UInt64) : (Code.garbage g).WellFormed := by
1409 simp [Code.garbage, Code.WellFormed]
1410
1411theorem Code.zeroed_wf : Code.zeroed.WellFormed := Code.garbage_wf _
1412
1413/-- The array fields of a `inflate_state` have the lengths of the C declaration. -/
1414def InflateState.WellFormed (v : InflateState) : Prop := v.lens.size = 320 ∧ v.work.size = 288 ∧ v.codes.size = 1444
1415
1416theorem InflateState.garbage_wf (g : Nat → UInt64) : (InflateState.garbage g).WellFormed := by
1417 simp [InflateState.garbage, InflateState.WellFormed]
1418
1419theorem InflateState.zeroed_wf : InflateState.zeroed.WellFormed := InflateState.garbage_wf _
1420
1421/-- The array fields of a `gzFile_s` have the lengths of the C declaration. -/
1422def GzFile.WellFormed (v : GzFile) : Prop := True
1423
1424theorem GzFile.garbage_wf (g : Nat → UInt64) : (GzFile.garbage g).WellFormed := by
1425 simp [GzFile.garbage, GzFile.WellFormed]
1426
1427theorem GzFile.zeroed_wf : GzFile.zeroed.WellFormed := GzFile.garbage_wf _
1428
1429/-- The array fields of a `gz_state` have the lengths of the C declaration. -/
1430def GzState.WellFormed (v : GzState) : Prop := True
1431
1432theorem GzState.garbage_wf (g : Nat → UInt64) : (GzState.garbage g).WellFormed := by
1433 simp [GzState.garbage, GzState.WellFormed]
1434
1435theorem GzState.zeroed_wf : GzState.zeroed.WellFormed := GzState.garbage_wf _
1436
1437/-- The array fields of a `static_tree_desc` have the lengths of the C declaration. -/
1438def StaticTreeDesc.WellFormed (v : StaticTreeDesc) : Prop := True
1439
1440theorem StaticTreeDesc.garbage_wf (g : Nat → UInt64) : (StaticTreeDesc.garbage g).WellFormed := by
1441 simp [StaticTreeDesc.garbage, StaticTreeDesc.WellFormed]
1442
1443theorem StaticTreeDesc.zeroed_wf : StaticTreeDesc.zeroed.WellFormed := StaticTreeDesc.garbage_wf _
1444
1445/-- Every record in a table of the heap is well-formed. -/
1446def Heap.RecordsWellFormed (h : Heap) : Prop :=
1447 TableWF ZStream.WellFormed h.streams ∧ TableWF GzHeader.WellFormed h.gzheaders ∧ TableWF DeflateState.WellFormed h.dstates ∧ TableWF InflateState.WellFormed h.istates ∧ TableWF GzState.WellFormed h.gzstates
1448
1449theorem Heap.empty_recordsWellFormed : Heap.empty.RecordsWellFormed := by
1450 refine ⟨fun _ _ hv => by simp [Heap.empty] at hv, fun _ _ hv => by simp [Heap.empty] at hv, fun _ _ hv => by simp [Heap.empty] at hv, fun _ _ hv => by simp [Heap.empty] at hv, fun _ _ hv => by simp [Heap.empty] at hv⟩
1451
1452theorem Heap.RecordsWellFormed.set_streams {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) {v : ZStream}
1453 (hv : v.WellFormed) : ({ h with streams := upd h.streams i (some v) } : Heap).RecordsWellFormed := by
1454 unfold Heap.RecordsWellFormed at hw ⊢
1455 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1456 exact ⟨(t0.set i hv), (t1), (t2), (t3), (t4)⟩
1457
1458theorem Heap.RecordsWellFormed.clear_streams {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) :
1459 ({ h with streams := upd h.streams i none } : Heap).RecordsWellFormed := by
1460 unfold Heap.RecordsWellFormed at hw ⊢
1461 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1462 exact ⟨(t0.clear i), (t1), (t2), (t3), (t4)⟩
1463
1464theorem Heap.RecordsWellFormed.set_gzheaders {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) {v : GzHeader}
1465 (hv : v.WellFormed) : ({ h with gzheaders := upd h.gzheaders i (some v) } : Heap).RecordsWellFormed := by
1466 unfold Heap.RecordsWellFormed at hw ⊢
1467 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1468 exact ⟨(t0), (t1.set i hv), (t2), (t3), (t4)⟩
1469
1470theorem Heap.RecordsWellFormed.clear_gzheaders {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) :
1471 ({ h with gzheaders := upd h.gzheaders i none } : Heap).RecordsWellFormed := by
1472 unfold Heap.RecordsWellFormed at hw ⊢
1473 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1474 exact ⟨(t0), (t1.clear i), (t2), (t3), (t4)⟩
1475
1476theorem Heap.RecordsWellFormed.set_dstates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) {v : DeflateState}
1477 (hv : v.WellFormed) : ({ h with dstates := upd h.dstates i (some v) } : Heap).RecordsWellFormed := by
1478 unfold Heap.RecordsWellFormed at hw ⊢
1479 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1480 exact ⟨(t0), (t1), (t2.set i hv), (t3), (t4)⟩
1481
1482theorem Heap.RecordsWellFormed.clear_dstates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) :
1483 ({ h with dstates := upd h.dstates i none } : Heap).RecordsWellFormed := by
1484 unfold Heap.RecordsWellFormed at hw ⊢
1485 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1486 exact ⟨(t0), (t1), (t2.clear i), (t3), (t4)⟩
1487
1488theorem Heap.RecordsWellFormed.set_istates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) {v : InflateState}
1489 (hv : v.WellFormed) : ({ h with istates := upd h.istates i (some v) } : Heap).RecordsWellFormed := by
1490 unfold Heap.RecordsWellFormed at hw ⊢
1491 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1492 exact ⟨(t0), (t1), (t2), (t3.set i hv), (t4)⟩
1493
1494theorem Heap.RecordsWellFormed.clear_istates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) :
1495 ({ h with istates := upd h.istates i none } : Heap).RecordsWellFormed := by
1496 unfold Heap.RecordsWellFormed at hw ⊢
1497 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1498 exact ⟨(t0), (t1), (t2), (t3.clear i), (t4)⟩
1499
1500theorem Heap.RecordsWellFormed.set_gzstates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) {v : GzState}
1501 (hv : v.WellFormed) : ({ h with gzstates := upd h.gzstates i (some v) } : Heap).RecordsWellFormed := by
1502 unfold Heap.RecordsWellFormed at hw ⊢
1503 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1504 exact ⟨(t0), (t1), (t2), (t3), (t4.set i hv)⟩
1505
1506theorem Heap.RecordsWellFormed.clear_gzstates {h : Heap} (hw : h.RecordsWellFormed) (i : Nat) :
1507 ({ h with gzstates := upd h.gzstates i none } : Heap).RecordsWellFormed := by
1508 unfold Heap.RecordsWellFormed at hw ⊢
1509 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1510 exact ⟨(t0), (t1), (t2), (t3), (t4.clear i)⟩
1511
1512/-- The static tables have the lengths of the C declaration. Their content is a separate obligation of the
1513translation that fixes them (see `docs/runtime-schema.md`). -/
1514def Statics.WellFormed (v : Statics) : Prop := v.dist_code.size = 512 ∧ v.length_code.size = 256 ∧ v.base_dist.size = 30 ∧ v.base_length.size = 29 ∧ v.crc_table.size = 256 ∧ v.static_dtree.size = 30 ∧ v.static_ltree.size = 288 ∧ v.x2n_table.size = 32 ∧ v.lenfix.size = 512 ∧ v.distfix.size = 32 ∧ v.extra_lbits.size = 29 ∧ v.extra_dbits.size = 30 ∧ v.extra_blbits.size = 19
1515
1516/-- The records and the static tables of the heap are well-formed. -/
1517def Heap.WellFormed (h : Heap) : Prop := h.RecordsWellFormed ∧ h.static.WellFormed
1518
1519/-! ## Reading and writing arrays and structs through a reference -/
1520
1521instance : Space Heap IRef Int32 where
1522 get h r := match r with
1523 | .dstate_heap id => (h.dstates id).map (·.heap)
1524 | .st_base_dist => some h.static.base_dist
1525 | .st_base_length => some h.static.base_length
1526 | .st_extra_lbits => some h.static.extra_lbits
1527 | .st_extra_dbits => some h.static.extra_dbits
1528 | .st_extra_blbits => some h.static.extra_blbits
1529 put h r a := match r with
1530 | .dstate_heap id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with heap := a }) } | none => h)
1531 | .st_base_dist => h
1532 | .st_base_length => h
1533 | .st_extra_lbits => h
1534 | .st_extra_dbits => h
1535 | .st_extra_blbits => h
1536 ro _ r := match r with
1537 | .dstate_heap _ => false
1538 | .st_base_dist => true
1539 | .st_base_length => true
1540 | .st_extra_lbits => true
1541 | .st_extra_dbits => true
1542 | .st_extra_blbits => true
1543 modify h r f := match r with
1544 | .dstate_heap id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.heap; let s := { s with heap := #[] }; { s with heap := f l })) }
1545 | .st_base_dist => h
1546 | .st_base_length => h
1547 | .st_extra_lbits => h
1548 | .st_extra_dbits => h
1549 | .st_extra_blbits => h
1550 modify_eq := by
1551 intro h r a f hg
1552 cases r with
1553 | dstate_heap id =>
1554 dsimp only at hg ⊢
1555 cases hs : h.dstates id with
1556 | none => simp [hs] at hg
1557 | some s =>
1558 have ha : s.heap = a := by simpa [hs] using hg
1559 subst ha
1560 have hm := Tbl.modify_opt h.dstates id (fun s => { s with heap := f s.heap }) s hs
1561 simp only [hs]
1562 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1563 | st_base_dist =>
1564 dsimp only at hg ⊢
1565 try rfl
1566 | st_base_length =>
1567 dsimp only at hg ⊢
1568 try rfl
1569 | st_extra_lbits =>
1570 dsimp only at hg ⊢
1571 try rfl
1572 | st_extra_dbits =>
1573 dsimp only at hg ⊢
1574 try rfl
1575 | st_extra_blbits =>
1576 dsimp only at hg ⊢
1577 try rfl
1578
1579theorem IRef.get_dstate_heap {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1580 Space.get h (IRef.dstate_heap id) = some s.heap := by simp [Space.get, e]
1581theorem IRef.put_dstate_heap {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array Int32) :
1582 Space.put h (IRef.dstate_heap id) a = { h with dstates := upd h.dstates id (some { s with heap := a }) } := by
1583 simp [Space.put, e]
1584/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1585well-formed. -/
1586theorem IRef.put_dstate_heap_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1587 {a : Array Int32} (ha : a.size = s.heap.size) : (Space.put h (IRef.dstate_heap id) a).RecordsWellFormed := by
1588 rw [IRef.put_dstate_heap e a]
1589 have hs : s.WellFormed := by
1590 unfold Heap.RecordsWellFormed at hw
1591 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1592 exact t2 id s e
1593 apply Heap.RecordsWellFormed.set_dstates hw
1594 simpa [DeflateState.WellFormed, ha] using hs
1595@[simp] theorem IRef.ro_dstate_heap (h : Heap) (id : Nat) : Space.ro h (IRef.dstate_heap id) = false := rfl
1596@[simp] theorem IRef.get_st_base_dist (h : Heap) : Space.get h IRef.st_base_dist = some h.static.base_dist := rfl
1597@[simp] theorem IRef.ro_st_base_dist (h : Heap) : Space.ro h IRef.st_base_dist = true := rfl
1598@[simp] theorem IRef.get_st_base_length (h : Heap) : Space.get h IRef.st_base_length = some h.static.base_length := rfl
1599@[simp] theorem IRef.ro_st_base_length (h : Heap) : Space.ro h IRef.st_base_length = true := rfl
1600@[simp] theorem IRef.get_st_extra_lbits (h : Heap) : Space.get h IRef.st_extra_lbits = some h.static.extra_lbits := rfl
1601@[simp] theorem IRef.ro_st_extra_lbits (h : Heap) : Space.ro h IRef.st_extra_lbits = true := rfl
1602@[simp] theorem IRef.get_st_extra_dbits (h : Heap) : Space.get h IRef.st_extra_dbits = some h.static.extra_dbits := rfl
1603@[simp] theorem IRef.ro_st_extra_dbits (h : Heap) : Space.ro h IRef.st_extra_dbits = true := rfl
1604@[simp] theorem IRef.get_st_extra_blbits (h : Heap) : Space.get h IRef.st_extra_blbits = some h.static.extra_blbits := rfl
1605@[simp] theorem IRef.ro_st_extra_blbits (h : Heap) : Space.ro h IRef.st_extra_blbits = true := rfl
1606instance : Space Heap WRef UInt16 where
1607 get h r := match r with
1608 | .blk b => h.words b
1609 | .dstate_bl_count id => (h.dstates id).map (·.bl_count)
1610 | .istate_lens id => (h.istates id).map (·.lens)
1611 | .istate_work id => (h.istates id).map (·.work)
1612 put h r a := match r with
1613 | .blk b => { h with words := upd h.words b (some a) }
1614 | .dstate_bl_count id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with bl_count := a }) } | none => h)
1615 | .istate_lens id => (match h.istates id with | some s => { h with istates := upd h.istates id (some { s with lens := a }) } | none => h)
1616 | .istate_work id => (match h.istates id with | some s => { h with istates := upd h.istates id (some { s with work := a }) } | none => h)
1617 ro _ r := match r with
1618 | .blk _ => false
1619 | .dstate_bl_count _ => false
1620 | .istate_lens _ => false
1621 | .istate_work _ => false
1622 modify h r f := match r with
1623 | .blk b => { h with words := h.words.modify b (Option.map f) }
1624 | .dstate_bl_count id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.bl_count; let s := { s with bl_count := #[] }; { s with bl_count := f l })) }
1625 | .istate_lens id => { h with istates := h.istates.modify id (Option.map (fun s => let l := s.lens; let s := { s with lens := #[] }; { s with lens := f l })) }
1626 | .istate_work id => { h with istates := h.istates.modify id (Option.map (fun s => let l := s.work; let s := { s with work := #[] }; { s with work := f l })) }
1627 modify_eq := by
1628 intro h r a f hg
1629 cases r with
1630 | blk b =>
1631 dsimp only at hg ⊢
1632 rw [Tbl.modify_opt _ _ _ _ hg]
1633 | dstate_bl_count id =>
1634 dsimp only at hg ⊢
1635 cases hs : h.dstates id with
1636 | none => simp [hs] at hg
1637 | some s =>
1638 have ha : s.bl_count = a := by simpa [hs] using hg
1639 subst ha
1640 have hm := Tbl.modify_opt h.dstates id (fun s => { s with bl_count := f s.bl_count }) s hs
1641 simp only [hs]
1642 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1643 | istate_lens id =>
1644 dsimp only at hg ⊢
1645 cases hs : h.istates id with
1646 | none => simp [hs] at hg
1647 | some s =>
1648 have ha : s.lens = a := by simpa [hs] using hg
1649 subst ha
1650 have hm := Tbl.modify_opt h.istates id (fun s => { s with lens := f s.lens }) s hs
1651 simp only [hs]
1652 exact congrArg (fun t => ({ h with istates := t } : Heap)) hm
1653 | istate_work id =>
1654 dsimp only at hg ⊢
1655 cases hs : h.istates id with
1656 | none => simp [hs] at hg
1657 | some s =>
1658 have ha : s.work = a := by simpa [hs] using hg
1659 subst ha
1660 have hm := Tbl.modify_opt h.istates id (fun s => { s with work := f s.work }) s hs
1661 simp only [hs]
1662 exact congrArg (fun t => ({ h with istates := t } : Heap)) hm
1663
1664theorem WRef.get_dstate_bl_count {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1665 Space.get h (WRef.dstate_bl_count id) = some s.bl_count := by simp [Space.get, e]
1666theorem WRef.put_dstate_bl_count {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array UInt16) :
1667 Space.put h (WRef.dstate_bl_count id) a = { h with dstates := upd h.dstates id (some { s with bl_count := a }) } := by
1668 simp [Space.put, e]
1669/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1670well-formed. -/
1671theorem WRef.put_dstate_bl_count_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1672 {a : Array UInt16} (ha : a.size = s.bl_count.size) : (Space.put h (WRef.dstate_bl_count id) a).RecordsWellFormed := by
1673 rw [WRef.put_dstate_bl_count e a]
1674 have hs : s.WellFormed := by
1675 unfold Heap.RecordsWellFormed at hw
1676 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1677 exact t2 id s e
1678 apply Heap.RecordsWellFormed.set_dstates hw
1679 simpa [DeflateState.WellFormed, ha] using hs
1680@[simp] theorem WRef.ro_dstate_bl_count (h : Heap) (id : Nat) : Space.ro h (WRef.dstate_bl_count id) = false := rfl
1681theorem WRef.get_istate_lens {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) :
1682 Space.get h (WRef.istate_lens id) = some s.lens := by simp [Space.get, e]
1683theorem WRef.put_istate_lens {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) (a : Array UInt16) :
1684 Space.put h (WRef.istate_lens id) a = { h with istates := upd h.istates id (some { s with lens := a }) } := by
1685 simp [Space.put, e]
1686/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1687well-formed. -/
1688theorem WRef.put_istate_lens_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : InflateState} (e : h.istates id = some s)
1689 {a : Array UInt16} (ha : a.size = s.lens.size) : (Space.put h (WRef.istate_lens id) a).RecordsWellFormed := by
1690 rw [WRef.put_istate_lens e a]
1691 have hs : s.WellFormed := by
1692 unfold Heap.RecordsWellFormed at hw
1693 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1694 exact t3 id s e
1695 apply Heap.RecordsWellFormed.set_istates hw
1696 simpa [InflateState.WellFormed, ha] using hs
1697@[simp] theorem WRef.ro_istate_lens (h : Heap) (id : Nat) : Space.ro h (WRef.istate_lens id) = false := rfl
1698theorem WRef.get_istate_work {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) :
1699 Space.get h (WRef.istate_work id) = some s.work := by simp [Space.get, e]
1700theorem WRef.put_istate_work {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) (a : Array UInt16) :
1701 Space.put h (WRef.istate_work id) a = { h with istates := upd h.istates id (some { s with work := a }) } := by
1702 simp [Space.put, e]
1703/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1704well-formed. -/
1705theorem WRef.put_istate_work_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : InflateState} (e : h.istates id = some s)
1706 {a : Array UInt16} (ha : a.size = s.work.size) : (Space.put h (WRef.istate_work id) a).RecordsWellFormed := by
1707 rw [WRef.put_istate_work e a]
1708 have hs : s.WellFormed := by
1709 unfold Heap.RecordsWellFormed at hw
1710 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1711 exact t3 id s e
1712 apply Heap.RecordsWellFormed.set_istates hw
1713 simpa [InflateState.WellFormed, ha] using hs
1714@[simp] theorem WRef.ro_istate_work (h : Heap) (id : Nat) : Space.ro h (WRef.istate_work id) = false := rfl
1715@[simp] theorem WRef.get_blk (h : Heap) (b : Nat) : Space.get h (WRef.blk b) = h.words b := rfl
1716@[simp] theorem WRef.put_blk (h : Heap) (b : Nat) (a : Array UInt16) :
1717 Space.put h (WRef.blk b) a = { h with words := upd h.words b (some a) } := rfl
1718@[simp] theorem WRef.ro_blk (h : Heap) (b : Nat) : Space.ro h (WRef.blk b) = false := rfl
1719
1720instance : Space Heap URef UInt32 where
1721 get h r := match r with
1722 | .st_crc_table => some h.static.crc_table
1723 | .st_x2n_table => some h.static.x2n_table
1724 put h r _ := match r with
1725 | .st_crc_table => h
1726 | .st_x2n_table => h
1727 ro _ r := match r with
1728 | .st_crc_table => true
1729 | .st_x2n_table => true
1730 modify h r _ := match r with
1731 | .st_crc_table => h
1732 | .st_x2n_table => h
1733 modify_eq := by
1734 intro h r a f hg
1735 cases r with
1736 | st_crc_table =>
1737 dsimp only at hg ⊢
1738 try rfl
1739 | st_x2n_table =>
1740 dsimp only at hg ⊢
1741 try rfl
1742
1743@[simp] theorem URef.get_st_crc_table (h : Heap) : Space.get h URef.st_crc_table = some h.static.crc_table := rfl
1744@[simp] theorem URef.ro_st_crc_table (h : Heap) : Space.ro h URef.st_crc_table = true := rfl
1745@[simp] theorem URef.get_st_x2n_table (h : Heap) : Space.get h URef.st_x2n_table = some h.static.x2n_table := rfl
1746@[simp] theorem URef.ro_st_x2n_table (h : Heap) : Space.ro h URef.st_x2n_table = true := rfl
1747instance : Space Heap BRef UInt8 where
1748 get h r := match r with
1749 | .blk b => h.bytes b
1750 | .str i => (strTable[i]?).map strBytes
1751 | .dstate_depth id => (h.dstates id).map (·.depth)
1752 | .st_dist_code => some h.static.dist_code
1753 | .st_length_code => some h.static.length_code
1754 put h r a := match r with
1755 | .blk b => { h with bytes := upd h.bytes b (some a) }
1756 | .str _ => h
1757 | .dstate_depth id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with depth := a }) } | none => h)
1758 | .st_dist_code => h
1759 | .st_length_code => h
1760 ro h r := match r with
1761 | .blk b => h.ro b
1762 | .str _ => true
1763 | .dstate_depth _ => false
1764 | .st_dist_code => true
1765 | .st_length_code => true
1766 modify h r f := match r with
1767 | .blk b => { h with bytes := h.bytes.modify b (Option.map f) }
1768 | .str _ => h
1769 | .dstate_depth id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.depth; let s := { s with depth := #[] }; { s with depth := f l })) }
1770 | .st_dist_code => h
1771 | .st_length_code => h
1772 modify_eq := by
1773 intro h r a f hg
1774 cases r with
1775 | blk b =>
1776 dsimp only at hg ⊢
1777 rw [Tbl.modify_opt _ _ _ _ hg]
1778 | str i =>
1779 dsimp only at hg ⊢
1780 try rfl
1781 | dstate_depth id =>
1782 dsimp only at hg ⊢
1783 cases hs : h.dstates id with
1784 | none => simp [hs] at hg
1785 | some s =>
1786 have ha : s.depth = a := by simpa [hs] using hg
1787 subst ha
1788 have hm := Tbl.modify_opt h.dstates id (fun s => { s with depth := f s.depth }) s hs
1789 simp only [hs]
1790 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1791 | st_dist_code =>
1792 dsimp only at hg ⊢
1793 try rfl
1794 | st_length_code =>
1795 dsimp only at hg ⊢
1796 try rfl
1797
1798theorem BRef.get_dstate_depth {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1799 Space.get h (BRef.dstate_depth id) = some s.depth := by simp [Space.get, e]
1800theorem BRef.put_dstate_depth {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array UInt8) :
1801 Space.put h (BRef.dstate_depth id) a = { h with dstates := upd h.dstates id (some { s with depth := a }) } := by
1802 simp [Space.put, e]
1803/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1804well-formed. -/
1805theorem BRef.put_dstate_depth_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1806 {a : Array UInt8} (ha : a.size = s.depth.size) : (Space.put h (BRef.dstate_depth id) a).RecordsWellFormed := by
1807 rw [BRef.put_dstate_depth e a]
1808 have hs : s.WellFormed := by
1809 unfold Heap.RecordsWellFormed at hw
1810 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1811 exact t2 id s e
1812 apply Heap.RecordsWellFormed.set_dstates hw
1813 simpa [DeflateState.WellFormed, ha] using hs
1814@[simp] theorem BRef.ro_dstate_depth (h : Heap) (id : Nat) : Space.ro h (BRef.dstate_depth id) = false := rfl
1815@[simp] theorem BRef.get_st_dist_code (h : Heap) : Space.get h BRef.st_dist_code = some h.static.dist_code := rfl
1816@[simp] theorem BRef.ro_st_dist_code (h : Heap) : Space.ro h BRef.st_dist_code = true := rfl
1817@[simp] theorem BRef.get_st_length_code (h : Heap) : Space.get h BRef.st_length_code = some h.static.length_code := rfl
1818@[simp] theorem BRef.ro_st_length_code (h : Heap) : Space.ro h BRef.st_length_code = true := rfl
1819@[simp] theorem BRef.get_blk (h : Heap) (b : Nat) : Space.get h (BRef.blk b) = h.bytes b := rfl
1820@[simp] theorem BRef.put_blk (h : Heap) (b : Nat) (a : Array UInt8) :
1821 Space.put h (BRef.blk b) a = { h with bytes := upd h.bytes b (some a) } := rfl
1822@[simp] theorem BRef.ro_blk (h : Heap) (b : Nat) : Space.ro h (BRef.blk b) = h.ro b := rfl
1823@[simp] theorem BRef.get_str (h : Heap) (i : Nat) : Space.get h (BRef.str i) = (strTable[i]?).map strBytes := by simp [Space.get]
1824@[simp] theorem BRef.put_str (h : Heap) (i : Nat) (a : Array UInt8) : Space.put h (BRef.str i) a = h := by simp [Space.put]
1825@[simp] theorem BRef.ro_str (h : Heap) (i : Nat) : Space.ro h (BRef.str i) = true := by simp [Space.ro]
1826
1827instance : Space Heap CodeRef Code where
1828 get h r := match r with
1829 | .istate_codes id => (h.istates id).map (·.codes)
1830 | .st_lenfix => some h.static.lenfix
1831 | .st_distfix => some h.static.distfix
1832 put h r a := match r with
1833 | .istate_codes id => (match h.istates id with | some s => { h with istates := upd h.istates id (some { s with codes := a }) } | none => h)
1834 | .st_lenfix => h
1835 | .st_distfix => h
1836 ro _ r := match r with
1837 | .istate_codes _ => false
1838 | .st_lenfix => true
1839 | .st_distfix => true
1840 modify h r f := match r with
1841 | .istate_codes id => { h with istates := h.istates.modify id (Option.map (fun s => let l := s.codes; let s := { s with codes := #[] }; { s with codes := f l })) }
1842 | .st_lenfix => h
1843 | .st_distfix => h
1844 modify_eq := by
1845 intro h r a f hg
1846 cases r with
1847 | istate_codes id =>
1848 dsimp only at hg ⊢
1849 cases hs : h.istates id with
1850 | none => simp [hs] at hg
1851 | some s =>
1852 have ha : s.codes = a := by simpa [hs] using hg
1853 subst ha
1854 have hm := Tbl.modify_opt h.istates id (fun s => { s with codes := f s.codes }) s hs
1855 simp only [hs]
1856 exact congrArg (fun t => ({ h with istates := t } : Heap)) hm
1857 | st_lenfix =>
1858 dsimp only at hg ⊢
1859 try rfl
1860 | st_distfix =>
1861 dsimp only at hg ⊢
1862 try rfl
1863
1864theorem CodeRef.get_istate_codes {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) :
1865 Space.get h (CodeRef.istate_codes id) = some s.codes := by simp [Space.get, e]
1866theorem CodeRef.put_istate_codes {h : Heap} {id : Nat} {s : InflateState} (e : h.istates id = some s) (a : Array Code) :
1867 Space.put h (CodeRef.istate_codes id) a = { h with istates := upd h.istates id (some { s with codes := a }) } := by
1868 simp [Space.put, e]
1869/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1870well-formed. -/
1871theorem CodeRef.put_istate_codes_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : InflateState} (e : h.istates id = some s)
1872 {a : Array Code} (ha : a.size = s.codes.size) : (Space.put h (CodeRef.istate_codes id) a).RecordsWellFormed := by
1873 rw [CodeRef.put_istate_codes e a]
1874 have hs : s.WellFormed := by
1875 unfold Heap.RecordsWellFormed at hw
1876 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1877 exact t3 id s e
1878 apply Heap.RecordsWellFormed.set_istates hw
1879 simpa [InflateState.WellFormed, ha] using hs
1880@[simp] theorem CodeRef.ro_istate_codes (h : Heap) (id : Nat) : Space.ro h (CodeRef.istate_codes id) = false := rfl
1881@[simp] theorem CodeRef.get_st_lenfix (h : Heap) : Space.get h CodeRef.st_lenfix = some h.static.lenfix := rfl
1882@[simp] theorem CodeRef.ro_st_lenfix (h : Heap) : Space.ro h CodeRef.st_lenfix = true := rfl
1883@[simp] theorem CodeRef.get_st_distfix (h : Heap) : Space.get h CodeRef.st_distfix = some h.static.distfix := rfl
1884@[simp] theorem CodeRef.ro_st_distfix (h : Heap) : Space.ro h CodeRef.st_distfix = true := rfl
1885instance : Space Heap CtDataRef CtData where
1886 get h r := match r with
1887 | .dstate_dyn_ltree id => (h.dstates id).map (·.dyn_ltree)
1888 | .dstate_dyn_dtree id => (h.dstates id).map (·.dyn_dtree)
1889 | .dstate_bl_tree id => (h.dstates id).map (·.bl_tree)
1890 | .st_static_dtree => some h.static.static_dtree
1891 | .st_static_ltree => some h.static.static_ltree
1892 put h r a := match r with
1893 | .dstate_dyn_ltree id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with dyn_ltree := a }) } | none => h)
1894 | .dstate_dyn_dtree id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with dyn_dtree := a }) } | none => h)
1895 | .dstate_bl_tree id => (match h.dstates id with | some s => { h with dstates := upd h.dstates id (some { s with bl_tree := a }) } | none => h)
1896 | .st_static_dtree => h
1897 | .st_static_ltree => h
1898 ro _ r := match r with
1899 | .dstate_dyn_ltree _ => false
1900 | .dstate_dyn_dtree _ => false
1901 | .dstate_bl_tree _ => false
1902 | .st_static_dtree => true
1903 | .st_static_ltree => true
1904 modify h r f := match r with
1905 | .dstate_dyn_ltree id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.dyn_ltree; let s := { s with dyn_ltree := #[] }; { s with dyn_ltree := f l })) }
1906 | .dstate_dyn_dtree id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.dyn_dtree; let s := { s with dyn_dtree := #[] }; { s with dyn_dtree := f l })) }
1907 | .dstate_bl_tree id => { h with dstates := h.dstates.modify id (Option.map (fun s => let l := s.bl_tree; let s := { s with bl_tree := #[] }; { s with bl_tree := f l })) }
1908 | .st_static_dtree => h
1909 | .st_static_ltree => h
1910 modify_eq := by
1911 intro h r a f hg
1912 cases r with
1913 | dstate_dyn_ltree id =>
1914 dsimp only at hg ⊢
1915 cases hs : h.dstates id with
1916 | none => simp [hs] at hg
1917 | some s =>
1918 have ha : s.dyn_ltree = a := by simpa [hs] using hg
1919 subst ha
1920 have hm := Tbl.modify_opt h.dstates id (fun s => { s with dyn_ltree := f s.dyn_ltree }) s hs
1921 simp only [hs]
1922 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1923 | dstate_dyn_dtree id =>
1924 dsimp only at hg ⊢
1925 cases hs : h.dstates id with
1926 | none => simp [hs] at hg
1927 | some s =>
1928 have ha : s.dyn_dtree = a := by simpa [hs] using hg
1929 subst ha
1930 have hm := Tbl.modify_opt h.dstates id (fun s => { s with dyn_dtree := f s.dyn_dtree }) s hs
1931 simp only [hs]
1932 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1933 | dstate_bl_tree id =>
1934 dsimp only at hg ⊢
1935 cases hs : h.dstates id with
1936 | none => simp [hs] at hg
1937 | some s =>
1938 have ha : s.bl_tree = a := by simpa [hs] using hg
1939 subst ha
1940 have hm := Tbl.modify_opt h.dstates id (fun s => { s with bl_tree := f s.bl_tree }) s hs
1941 simp only [hs]
1942 exact congrArg (fun t => ({ h with dstates := t } : Heap)) hm
1943 | st_static_dtree =>
1944 dsimp only at hg ⊢
1945 try rfl
1946 | st_static_ltree =>
1947 dsimp only at hg ⊢
1948 try rfl
1949
1950theorem CtDataRef.get_dstate_dyn_ltree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1951 Space.get h (CtDataRef.dstate_dyn_ltree id) = some s.dyn_ltree := by simp [Space.get, e]
1952theorem CtDataRef.put_dstate_dyn_ltree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array CtData) :
1953 Space.put h (CtDataRef.dstate_dyn_ltree id) a = { h with dstates := upd h.dstates id (some { s with dyn_ltree := a }) } := by
1954 simp [Space.put, e]
1955/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1956well-formed. -/
1957theorem CtDataRef.put_dstate_dyn_ltree_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1958 {a : Array CtData} (ha : a.size = s.dyn_ltree.size) : (Space.put h (CtDataRef.dstate_dyn_ltree id) a).RecordsWellFormed := by
1959 rw [CtDataRef.put_dstate_dyn_ltree e a]
1960 have hs : s.WellFormed := by
1961 unfold Heap.RecordsWellFormed at hw
1962 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1963 exact t2 id s e
1964 apply Heap.RecordsWellFormed.set_dstates hw
1965 simpa [DeflateState.WellFormed, ha] using hs
1966@[simp] theorem CtDataRef.ro_dstate_dyn_ltree (h : Heap) (id : Nat) : Space.ro h (CtDataRef.dstate_dyn_ltree id) = false := rfl
1967theorem CtDataRef.get_dstate_dyn_dtree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1968 Space.get h (CtDataRef.dstate_dyn_dtree id) = some s.dyn_dtree := by simp [Space.get, e]
1969theorem CtDataRef.put_dstate_dyn_dtree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array CtData) :
1970 Space.put h (CtDataRef.dstate_dyn_dtree id) a = { h with dstates := upd h.dstates id (some { s with dyn_dtree := a }) } := by
1971 simp [Space.put, e]
1972/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1973well-formed. -/
1974theorem CtDataRef.put_dstate_dyn_dtree_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1975 {a : Array CtData} (ha : a.size = s.dyn_dtree.size) : (Space.put h (CtDataRef.dstate_dyn_dtree id) a).RecordsWellFormed := by
1976 rw [CtDataRef.put_dstate_dyn_dtree e a]
1977 have hs : s.WellFormed := by
1978 unfold Heap.RecordsWellFormed at hw
1979 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1980 exact t2 id s e
1981 apply Heap.RecordsWellFormed.set_dstates hw
1982 simpa [DeflateState.WellFormed, ha] using hs
1983@[simp] theorem CtDataRef.ro_dstate_dyn_dtree (h : Heap) (id : Nat) : Space.ro h (CtDataRef.dstate_dyn_dtree id) = false := rfl
1984theorem CtDataRef.get_dstate_bl_tree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) :
1985 Space.get h (CtDataRef.dstate_bl_tree id) = some s.bl_tree := by simp [Space.get, e]
1986theorem CtDataRef.put_dstate_bl_tree {h : Heap} {id : Nat} {s : DeflateState} (e : h.dstates id = some s) (a : Array CtData) :
1987 Space.put h (CtDataRef.dstate_bl_tree id) a = { h with dstates := upd h.dstates id (some { s with bl_tree := a }) } := by
1988 simp [Space.put, e]
1989/-- Storing into an array field of a well-formed record, with an array of the same length, keeps every record
1990well-formed. -/
1991theorem CtDataRef.put_dstate_bl_tree_wf {h : Heap} (hw : h.RecordsWellFormed) {id : Nat} {s : DeflateState} (e : h.dstates id = some s)
1992 {a : Array CtData} (ha : a.size = s.bl_tree.size) : (Space.put h (CtDataRef.dstate_bl_tree id) a).RecordsWellFormed := by
1993 rw [CtDataRef.put_dstate_bl_tree e a]
1994 have hs : s.WellFormed := by
1995 unfold Heap.RecordsWellFormed at hw
1996 obtain ⟨t0, t1, t2, t3, t4⟩ := hw
1997 exact t2 id s e
1998 apply Heap.RecordsWellFormed.set_dstates hw
1999 simpa [DeflateState.WellFormed, ha] using hs
2000@[simp] theorem CtDataRef.ro_dstate_bl_tree (h : Heap) (id : Nat) : Space.ro h (CtDataRef.dstate_bl_tree id) = false := rfl
2001@[simp] theorem CtDataRef.get_st_static_dtree (h : Heap) : Space.get h CtDataRef.st_static_dtree = some h.static.static_dtree := rfl
2002@[simp] theorem CtDataRef.ro_st_static_dtree (h : Heap) : Space.ro h CtDataRef.st_static_dtree = true := rfl
2003@[simp] theorem CtDataRef.get_st_static_ltree (h : Heap) : Space.get h CtDataRef.st_static_ltree = some h.static.static_ltree := rfl
2004@[simp] theorem CtDataRef.ro_st_static_ltree (h : Heap) : Space.ro h CtDataRef.st_static_ltree = true := rfl
2005/-- The record a reference denotes, if it is live. -/
2006def ZStreamRef.get (h : Heap) : ZStreamRef → Option ZStream
2007 | .tab i => h.streams i
2008 | .in_gzstate_strm i => (h.gzstates i).map (·.strm)
2009
2010/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2011brought back). -/
2012def ZStreamRef.put (h : Heap) : ZStreamRef → ZStream → Heap
2013 | .tab i, v => (match h.streams i with
2014 | some _ => { h with streams := upd h.streams i (some v) }
2015 | none => h)
2016 | .in_gzstate_strm i, v => (match h.gzstates i with
2017 | some s => { h with gzstates := upd h.gzstates i (some { s with strm := v }) }
2018 | none => h)
2019
2020theorem ZStreamRef.put_tab {h : Heap} {i : Nat} {v : ZStream} (e : h.streams i = some v) (v' : ZStream) :
2021 (ZStreamRef.tab i).put h v' = { h with streams := upd h.streams i (some v') } := by simp [ZStreamRef.put, e]
2022
2023/-- Is the record read-only (a static instance)? -/
2024def ZStreamRef.isRo : ZStreamRef → Bool
2025 | .tab _ => false
2026 | .in_gzstate_strm _ => false
2027
2028/-- The record a reference denotes, if it is live. -/
2029def GzHeaderRef.get (h : Heap) : GzHeaderRef → Option GzHeader
2030 | .tab i => h.gzheaders i
2031
2032/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2033brought back). -/
2034def GzHeaderRef.put (h : Heap) : GzHeaderRef → GzHeader → Heap
2035 | .tab i, v => (match h.gzheaders i with
2036 | some _ => { h with gzheaders := upd h.gzheaders i (some v) }
2037 | none => h)
2038
2039theorem GzHeaderRef.put_tab {h : Heap} {i : Nat} {v : GzHeader} (e : h.gzheaders i = some v) (v' : GzHeader) :
2040 (GzHeaderRef.tab i).put h v' = { h with gzheaders := upd h.gzheaders i (some v') } := by simp [GzHeaderRef.put, e]
2041
2042/-- Is the record read-only (a static instance)? -/
2043def GzHeaderRef.isRo : GzHeaderRef → Bool
2044 | .tab _ => false
2045
2046/-- The record a reference denotes, if it is live. -/
2047def DeflateStateRef.get (h : Heap) : DeflateStateRef → Option DeflateState
2048 | .tab i => h.dstates i
2049
2050/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2051brought back). -/
2052def DeflateStateRef.put (h : Heap) : DeflateStateRef → DeflateState → Heap
2053 | .tab i, v => (match h.dstates i with
2054 | some _ => { h with dstates := upd h.dstates i (some v) }
2055 | none => h)
2056
2057theorem DeflateStateRef.put_tab {h : Heap} {i : Nat} {v : DeflateState} (e : h.dstates i = some v) (v' : DeflateState) :
2058 (DeflateStateRef.tab i).put h v' = { h with dstates := upd h.dstates i (some v') } := by simp [DeflateStateRef.put, e]
2059
2060/-- Is the record read-only (a static instance)? -/
2061def DeflateStateRef.isRo : DeflateStateRef → Bool
2062 | .tab _ => false
2063
2064/-- The record a reference denotes, if it is live. -/
2065def InflateStateRef.get (h : Heap) : InflateStateRef → Option InflateState
2066 | .tab i => h.istates i
2067
2068/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2069brought back). -/
2070def InflateStateRef.put (h : Heap) : InflateStateRef → InflateState → Heap
2071 | .tab i, v => (match h.istates i with
2072 | some _ => { h with istates := upd h.istates i (some v) }
2073 | none => h)
2074
2075theorem InflateStateRef.put_tab {h : Heap} {i : Nat} {v : InflateState} (e : h.istates i = some v) (v' : InflateState) :
2076 (InflateStateRef.tab i).put h v' = { h with istates := upd h.istates i (some v') } := by simp [InflateStateRef.put, e]
2077
2078/-- Is the record read-only (a static instance)? -/
2079def InflateStateRef.isRo : InflateStateRef → Bool
2080 | .tab _ => false
2081
2082/-- The record a reference denotes, if it is live. -/
2083def GzStateRef.get (h : Heap) : GzStateRef → Option GzState
2084 | .tab i => h.gzstates i
2085
2086/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2087brought back). -/
2088def GzStateRef.put (h : Heap) : GzStateRef → GzState → Heap
2089 | .tab i, v => (match h.gzstates i with
2090 | some _ => { h with gzstates := upd h.gzstates i (some v) }
2091 | none => h)
2092
2093theorem GzStateRef.put_tab {h : Heap} {i : Nat} {v : GzState} (e : h.gzstates i = some v) (v' : GzState) :
2094 (GzStateRef.tab i).put h v' = { h with gzstates := upd h.gzstates i (some v') } := by simp [GzStateRef.put, e]
2095
2096/-- Is the record read-only (a static instance)? -/
2097def GzStateRef.isRo : GzStateRef → Bool
2098 | .tab _ => false
2099
2100/-- The record a reference denotes, if it is live. -/
2101def GzFileRef.get (h : Heap) : GzFileRef → Option GzFile
2102 | .in_gzstate_x i => (h.gzstates i).map (·.x)
2103
2104/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2105brought back). -/
2106def GzFileRef.put (h : Heap) : GzFileRef → GzFile → Heap
2107 | .in_gzstate_x i, v => (match h.gzstates i with
2108 | some s => { h with gzstates := upd h.gzstates i (some { s with x := v }) }
2109 | none => h)
2110
2111/-- Is the record read-only (a static instance)? -/
2112def GzFileRef.isRo : GzFileRef → Bool
2113 | .in_gzstate_x _ => false
2114
2115/-- The record a reference denotes, if it is live. -/
2116def TreeDescRef.get (h : Heap) : TreeDescRef → Option TreeDesc
2117 | .in_dstate_l_desc i => (h.dstates i).map (·.l_desc)
2118 | .in_dstate_d_desc i => (h.dstates i).map (·.d_desc)
2119 | .in_dstate_bl_desc i => (h.dstates i).map (·.bl_desc)
2120
2121/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2122brought back). -/
2123def TreeDescRef.put (h : Heap) : TreeDescRef → TreeDesc → Heap
2124 | .in_dstate_l_desc i, v => (match h.dstates i with
2125 | some s => { h with dstates := upd h.dstates i (some { s with l_desc := v }) }
2126 | none => h)
2127 | .in_dstate_d_desc i, v => (match h.dstates i with
2128 | some s => { h with dstates := upd h.dstates i (some { s with d_desc := v }) }
2129 | none => h)
2130 | .in_dstate_bl_desc i, v => (match h.dstates i with
2131 | some s => { h with dstates := upd h.dstates i (some { s with bl_desc := v }) }
2132 | none => h)
2133
2134/-- Is the record read-only (a static instance)? -/
2135def TreeDescRef.isRo : TreeDescRef → Bool
2136 | .in_dstate_l_desc _ => false
2137 | .in_dstate_d_desc _ => false
2138 | .in_dstate_bl_desc _ => false
2139
2140/-- The record a reference denotes, if it is live. -/
2141def StaticTreeDescRef.get (h : Heap) : StaticTreeDescRef → Option StaticTreeDesc
2142 | .st_static_l_desc => some h.static.static_l_desc
2143 | .st_static_d_desc => some h.static.static_d_desc
2144 | .st_static_bl_desc => some h.static.static_bl_desc
2145
2146/-- The heap after replacing the record a reference denotes (unchanged if it is not live: a freed record is not
2147brought back). -/
2148def StaticTreeDescRef.put (h : Heap) : StaticTreeDescRef → StaticTreeDesc → Heap
2149 | .st_static_l_desc, _ => h
2150 | .st_static_d_desc, _ => h
2151 | .st_static_bl_desc, _ => h
2152
2153/-- Is the record read-only (a static instance)? -/
2154def StaticTreeDescRef.isRo : StaticTreeDescRef → Bool
2155 | .st_static_l_desc => true
2156 | .st_static_d_desc => true
2157 | .st_static_bl_desc => true
2158
2159/-! ## Constants and tables the generator could not turn into a definition -/
2160
2161/-
2162Macros of the headers that are not emitted as a constant: 32 names, by reason.
2163 empty: a feature flag:
2164 DEFLATE_H FAR GUNZIP HAVE_MEMCPY HAVE_VSNPRINTF STDC
2165 STDC99 ZCONF_H ZEXPORT ZEXPORTVA ZLIB_H ZLIB_INTERNAL
2166 ZUTIL_H Z_HAVE_UNISTD_H Z_LARGE64 Z_LFS64 z_const
2167 not an integer constant expression:
2168 Code Dad Freq Len ZEXTERN Z_U4
2169 Z_U8 local max_insert_length z_off64_t z_off_t zlib_version
2170 zmemcmp zmemcpy
2171 uses sizeof, which the evaluator does not know:
2172 GZ_OFF_MAX
2173
2174Names that are also an enumerator: `COPY` is emitted as `GZ_COPY`.
2175`GZ_OFF_MAX` (gzguts.h) is `((((z_off64_t)1 << (sizeof(z_off64_t) * CHAR_BIT - 2)) - 1) * 2 + 1)`, that is
21769223372036854775807 here; it is defined with that value in the translation of gzguts.h.
2177-/
2178
2179end C