Schema.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

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