trees.c.lean

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

1import ZlibF.Runtime.Alloc
2import ZlibF.Runtime.Tables
3
4/-!
5# trees.c — faithful translation (draft)
6
7Source: `zlib/trees.c` and `zlib/trees.h`, default build (LP64; `ZLIB_DEBUG`, `GEN_TREES_H`, `LIT_MEM`,
8`NO_INIT_GLOBAL_POINTERS`, `FORCE_STATIC`, `FORCE_STORED` undefined; `STDC` defined, so the tables come from
9`trees.h`). Translated statement by statement. Macros are expanded in source order: `put_byte`, `put_short`,
10`send_bits`, `send_code`, `pqremove`, `smaller`, `d_code`.
11
12Conventions of this file:
13
14* `deflate_state *s` is `DeflateStatePtr`. A scalar field is read with `rd s` (a load of the whole record) and
15  written with `md s` (a load, a record update and a store). An array field decays to a pointer: `pLtree s`
16  (`s->dyn_ltree`), `pDtree`, `pBltree`, `pHeap`, `pDepth`, `pBlCount`.
17* `int` is `Int32` with checked arithmetic (`iadd`, `isub`, `shl1`, ...): an overflow is `Fault.ub`.
18  `unsigned`, `ush`, `uch`, `ulg` wrap.
19* `Assert` and `Trace*` are compiled out (no `ZLIB_DEBUG`); `tr_static_init` is an empty function.
20* The static tables of `trees.h` and `trees.c` are `*_tab` constants below, installed in the heap by
21  `install_trees` (they are `Statics` fields; a store through them is a fault).
22* `ct_data`: `Freq`/`Code` is `fc`, `Dad`/`Len` is `dl`.
23* Local `ush next_code[MAX_BITS+1]` of `gen_codes` is a Lean `Array UInt16`; its element 0 is never read
24  (`len == 0` is skipped) and an index outside it is a fault.
25-/
26
27namespace Zlib.Trees
28open C
29
30/-! ## Constants -/
31
32def MAX_BL_BITS : Int32 := 7
33def END_BLOCK : Int32 := 256
34def REP_3_6 : Int32 := 16
35def REPZ_3_10 : Int32 := 17
36def REPZ_11_138 : Int32 := 18
37
38/-- `extra_lbits[LENGTH_CODES]` (trees.c). -/
39def extra_lbits_tab : Array Int32 := #[0,0,0,0,0,0,0,0,1,1,1,1,2,2,2,2,3,3,3,3,4,4,4,4,5,5,5,5,0]
40/-- `extra_dbits[D_CODES]` (trees.c). -/
41def extra_dbits_tab : Array Int32 := #[0,0,0,0,1,1,2,2,3,3,4,4,5,5,6,6,7,7,8,8,9,9,10,10,11,11,12,12,13,13]
42/-- `extra_blbits[BL_CODES]` (trees.c). -/
43def extra_blbits_tab : Array Int32 := #[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,2,3,7]
44/-- `local const uch bl_order[BL_CODES]` (trees.c). -/
45def bl_order : Array UInt8 := #[16,17,18,0,8,7,9,6,10,5,11,4,12,3,13,2,14,1,15]
46
47/-! ## Tables of `trees.h` (verbatim) -/
48
49/-- `static_ltree`: `trees.h`, verbatim (288 entries; `fc` = `Code`, `dl` = `Len`). -/
50def static_ltree_tab : Array CtData := #[
51  ⟨12, 8⟩, ⟨140, 8⟩, ⟨76, 8⟩, ⟨204, 8⟩, ⟨44, 8⟩, ⟨172, 8⟩,
52  ⟨108, 8⟩, ⟨236, 8⟩, ⟨28, 8⟩, ⟨156, 8⟩, ⟨92, 8⟩, ⟨220, 8⟩,
53  ⟨60, 8⟩, ⟨188, 8⟩, ⟨124, 8⟩, ⟨252, 8⟩, ⟨2, 8⟩, ⟨130, 8⟩,
54  ⟨66, 8⟩, ⟨194, 8⟩, ⟨34, 8⟩, ⟨162, 8⟩, ⟨98, 8⟩, ⟨226, 8⟩,
55  ⟨18, 8⟩, ⟨146, 8⟩, ⟨82, 8⟩, ⟨210, 8⟩, ⟨50, 8⟩, ⟨178, 8⟩,
56  ⟨114, 8⟩, ⟨242, 8⟩, ⟨10, 8⟩, ⟨138, 8⟩, ⟨74, 8⟩, ⟨202, 8⟩,
57  ⟨42, 8⟩, ⟨170, 8⟩, ⟨106, 8⟩, ⟨234, 8⟩, ⟨26, 8⟩, ⟨154, 8⟩,
58  ⟨90, 8⟩, ⟨218, 8⟩, ⟨58, 8⟩, ⟨186, 8⟩, ⟨122, 8⟩, ⟨250, 8⟩,
59  ⟨6, 8⟩, ⟨134, 8⟩, ⟨70, 8⟩, ⟨198, 8⟩, ⟨38, 8⟩, ⟨166, 8⟩,
60  ⟨102, 8⟩, ⟨230, 8⟩, ⟨22, 8⟩, ⟨150, 8⟩, ⟨86, 8⟩, ⟨214, 8⟩,
61  ⟨54, 8⟩, ⟨182, 8⟩, ⟨118, 8⟩, ⟨246, 8⟩, ⟨14, 8⟩, ⟨142, 8⟩,
62  ⟨78, 8⟩, ⟨206, 8⟩, ⟨46, 8⟩, ⟨174, 8⟩, ⟨110, 8⟩, ⟨238, 8⟩,
63  ⟨30, 8⟩, ⟨158, 8⟩, ⟨94, 8⟩, ⟨222, 8⟩, ⟨62, 8⟩, ⟨190, 8⟩,
64  ⟨126, 8⟩, ⟨254, 8⟩, ⟨1, 8⟩, ⟨129, 8⟩, ⟨65, 8⟩, ⟨193, 8⟩,
65  ⟨33, 8⟩, ⟨161, 8⟩, ⟨97, 8⟩, ⟨225, 8⟩, ⟨17, 8⟩, ⟨145, 8⟩,
66  ⟨81, 8⟩, ⟨209, 8⟩, ⟨49, 8⟩, ⟨177, 8⟩, ⟨113, 8⟩, ⟨241, 8⟩,
67  ⟨9, 8⟩, ⟨137, 8⟩, ⟨73, 8⟩, ⟨201, 8⟩, ⟨41, 8⟩, ⟨169, 8⟩,
68  ⟨105, 8⟩, ⟨233, 8⟩, ⟨25, 8⟩, ⟨153, 8⟩, ⟨89, 8⟩, ⟨217, 8⟩,
69  ⟨57, 8⟩, ⟨185, 8⟩, ⟨121, 8⟩, ⟨249, 8⟩, ⟨5, 8⟩, ⟨133, 8⟩,
70  ⟨69, 8⟩, ⟨197, 8⟩, ⟨37, 8⟩, ⟨165, 8⟩, ⟨101, 8⟩, ⟨229, 8⟩,
71  ⟨21, 8⟩, ⟨149, 8⟩, ⟨85, 8⟩, ⟨213, 8⟩, ⟨53, 8⟩, ⟨181, 8⟩,
72  ⟨117, 8⟩, ⟨245, 8⟩, ⟨13, 8⟩, ⟨141, 8⟩, ⟨77, 8⟩, ⟨205, 8⟩,
73  ⟨45, 8⟩, ⟨173, 8⟩, ⟨109, 8⟩, ⟨237, 8⟩, ⟨29, 8⟩, ⟨157, 8⟩,
74  ⟨93, 8⟩, ⟨221, 8⟩, ⟨61, 8⟩, ⟨189, 8⟩, ⟨125, 8⟩, ⟨253, 8⟩,
75  ⟨19, 9⟩, ⟨275, 9⟩, ⟨147, 9⟩, ⟨403, 9⟩, ⟨83, 9⟩, ⟨339, 9⟩,
76  ⟨211, 9⟩, ⟨467, 9⟩, ⟨51, 9⟩, ⟨307, 9⟩, ⟨179, 9⟩, ⟨435, 9⟩,
77  ⟨115, 9⟩, ⟨371, 9⟩, ⟨243, 9⟩, ⟨499, 9⟩, ⟨11, 9⟩, ⟨267, 9⟩,
78  ⟨139, 9⟩, ⟨395, 9⟩, ⟨75, 9⟩, ⟨331, 9⟩, ⟨203, 9⟩, ⟨459, 9⟩,
79  ⟨43, 9⟩, ⟨299, 9⟩, ⟨171, 9⟩, ⟨427, 9⟩, ⟨107, 9⟩, ⟨363, 9⟩,
80  ⟨235, 9⟩, ⟨491, 9⟩, ⟨27, 9⟩, ⟨283, 9⟩, ⟨155, 9⟩, ⟨411, 9⟩,
81  ⟨91, 9⟩, ⟨347, 9⟩, ⟨219, 9⟩, ⟨475, 9⟩, ⟨59, 9⟩, ⟨315, 9⟩,
82  ⟨187, 9⟩, ⟨443, 9⟩, ⟨123, 9⟩, ⟨379, 9⟩, ⟨251, 9⟩, ⟨507, 9⟩,
83  ⟨7, 9⟩, ⟨263, 9⟩, ⟨135, 9⟩, ⟨391, 9⟩, ⟨71, 9⟩, ⟨327, 9⟩,
84  ⟨199, 9⟩, ⟨455, 9⟩, ⟨39, 9⟩, ⟨295, 9⟩, ⟨167, 9⟩, ⟨423, 9⟩,
85  ⟨103, 9⟩, ⟨359, 9⟩, ⟨231, 9⟩, ⟨487, 9⟩, ⟨23, 9⟩, ⟨279, 9⟩,
86  ⟨151, 9⟩, ⟨407, 9⟩, ⟨87, 9⟩, ⟨343, 9⟩, ⟨215, 9⟩, ⟨471, 9⟩,
87  ⟨55, 9⟩, ⟨311, 9⟩, ⟨183, 9⟩, ⟨439, 9⟩, ⟨119, 9⟩, ⟨375, 9⟩,
88  ⟨247, 9⟩, ⟨503, 9⟩, ⟨15, 9⟩, ⟨271, 9⟩, ⟨143, 9⟩, ⟨399, 9⟩,
89  ⟨79, 9⟩, ⟨335, 9⟩, ⟨207, 9⟩, ⟨463, 9⟩, ⟨47, 9⟩, ⟨303, 9⟩,
90  ⟨175, 9⟩, ⟨431, 9⟩, ⟨111, 9⟩, ⟨367, 9⟩, ⟨239, 9⟩, ⟨495, 9⟩,
91  ⟨31, 9⟩, ⟨287, 9⟩, ⟨159, 9⟩, ⟨415, 9⟩, ⟨95, 9⟩, ⟨351, 9⟩,
92  ⟨223, 9⟩, ⟨479, 9⟩, ⟨63, 9⟩, ⟨319, 9⟩, ⟨191, 9⟩, ⟨447, 9⟩,
93  ⟨127, 9⟩, ⟨383, 9⟩, ⟨255, 9⟩, ⟨511, 9⟩, ⟨0, 7⟩, ⟨64, 7⟩,
94  ⟨32, 7⟩, ⟨96, 7⟩, ⟨16, 7⟩, ⟨80, 7⟩, ⟨48, 7⟩, ⟨112, 7⟩,
95  ⟨8, 7⟩, ⟨72, 7⟩, ⟨40, 7⟩, ⟨104, 7⟩, ⟨24, 7⟩, ⟨88, 7⟩,
96  ⟨56, 7⟩, ⟨120, 7⟩, ⟨4, 7⟩, ⟨68, 7⟩, ⟨36, 7⟩, ⟨100, 7⟩,
97  ⟨20, 7⟩, ⟨84, 7⟩, ⟨52, 7⟩, ⟨116, 7⟩, ⟨3, 8⟩, ⟨131, 8⟩,
98  ⟨67, 8⟩, ⟨195, 8⟩, ⟨35, 8⟩, ⟨163, 8⟩, ⟨99, 8⟩, ⟨227, 8⟩
99]
100
101/-- `static_dtree`: `trees.h`, verbatim (30 entries; `fc` = `Code`, `dl` = `Len`). -/
102def static_dtree_tab : Array CtData := #[
103  ⟨0, 5⟩, ⟨16, 5⟩, ⟨8, 5⟩, ⟨24, 5⟩, ⟨4, 5⟩, ⟨20, 5⟩,
104  ⟨12, 5⟩, ⟨28, 5⟩, ⟨2, 5⟩, ⟨18, 5⟩, ⟨10, 5⟩, ⟨26, 5⟩,
105  ⟨6, 5⟩, ⟨22, 5⟩, ⟨14, 5⟩, ⟨30, 5⟩, ⟨1, 5⟩, ⟨17, 5⟩,
106  ⟨9, 5⟩, ⟨25, 5⟩, ⟨5, 5⟩, ⟨21, 5⟩, ⟨13, 5⟩, ⟨29, 5⟩,
107  ⟨3, 5⟩, ⟨19, 5⟩, ⟨11, 5⟩, ⟨27, 5⟩, ⟨7, 5⟩, ⟨23, 5⟩
108]
109
110/-- `_dist_code`: `trees.h`, verbatim (512 entries). -/
111def dist_code_tab : Array UInt8 := #[
112  0, 1, 2, 3, 4, 4, 5, 5, 6, 6, 6, 6, 7, 7, 7, 7, 8, 8, 8, 8,
113  8, 8, 8, 8, 9, 9, 9, 9, 9, 9, 9, 9, 10, 10, 10, 10, 10, 10, 10, 10,
114  10, 10, 10, 10, 10, 10, 10, 10, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11,
115  11, 11, 11, 11, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12,
116  12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 13, 13, 13, 13,
117  13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13,
118  13, 13, 13, 13, 13, 13, 13, 13, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14,
119  14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14,
120  14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14,
121  14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 15, 15, 15, 15, 15, 15, 15, 15,
122  15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15,
123  15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15,
124  15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 0, 0, 16, 17,
125  18, 18, 19, 19, 20, 20, 20, 20, 21, 21, 21, 21, 22, 22, 22, 22, 22, 22, 22, 22,
126  23, 23, 23, 23, 23, 23, 23, 23, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
127  24, 24, 24, 24, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25,
128  26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26,
129  26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 27, 27, 27, 27, 27, 27, 27, 27,
130  27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27,
131  27, 27, 27, 27, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28,
132  28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28,
133  28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28, 28,
134  28, 28, 28, 28, 28, 28, 28, 28, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29,
135  29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29,
136  29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29,
137  29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29, 29
138]
139
140/-- `_length_code`: `trees.h`, verbatim (256 entries). -/
141def length_code_tab : Array UInt8 := #[
142  0, 1, 2, 3, 4, 5, 6, 7, 8, 8, 9, 9, 10, 10, 11, 11, 12, 12, 12, 12,
143  13, 13, 13, 13, 14, 14, 14, 14, 15, 15, 15, 15, 16, 16, 16, 16, 16, 16, 16, 16,
144  17, 17, 17, 17, 17, 17, 17, 17, 18, 18, 18, 18, 18, 18, 18, 18, 19, 19, 19, 19,
145  19, 19, 19, 19, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20,
146  21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 21, 22, 22, 22, 22,
147  22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 23, 23, 23, 23, 23, 23, 23, 23,
148  23, 23, 23, 23, 23, 23, 23, 23, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
149  24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
150  25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25,
151  25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 25, 26, 26, 26, 26, 26, 26, 26, 26,
152  26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26, 26,
153  26, 26, 26, 26, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27,
154  27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 27, 28
155]
156
157/-- `base_length`: `trees.h`, verbatim (29 entries). -/
158def base_length_tab : Array Int32 := #[
159  0, 1, 2, 3, 4, 5, 6, 7, 8, 10, 12, 14, 16, 20, 24, 28, 32, 40, 48, 56,
160  64, 80, 96, 112, 128, 160, 192, 224, 0
161]
162
163/-- `base_dist`: `trees.h`, verbatim (30 entries). -/
164def base_dist_tab : Array Int32 := #[
165  0, 1, 2, 3, 4, 6, 8, 12, 16, 24, 32, 48, 64, 96, 128, 192, 256, 384, 512, 768,
166  1024, 1536, 2048, 3072, 4096, 6144, 8192, 12288, 16384, 24576
167]
168
169/-- The static tables and descriptors of `trees.c`, installed in the `Statics` of a heap:
170`static_l_desc = {static_ltree, extra_lbits, LITERALS+1, L_CODES, MAX_BITS}`,
171`static_d_desc = {static_dtree, extra_dbits, 0, D_CODES, MAX_BITS}`,
172`static_bl_desc = {NULL, extra_blbits, 0, BL_CODES, MAX_BL_BITS}`. -/
173def trees_statics (st : Statics) : Statics :=
174  { st with
175    dist_code := dist_code_tab
176    length_code := length_code_tab
177    base_dist := base_dist_tab
178    base_length := base_length_tab
179    static_dtree := static_dtree_tab
180    static_ltree := static_ltree_tab
181    extra_lbits := extra_lbits_tab
182    extra_dbits := extra_dbits_tab
183    extra_blbits := extra_blbits_tab
184    static_l_desc := { static_tree := .ref .st_static_ltree 0, extra_bits := .ref .st_extra_lbits 0,
185                       extra_base := LITERALS + 1, elems := L_CODES, max_length := MAX_BITS }
186    static_d_desc := { static_tree := .ref .st_static_dtree 0, extra_bits := .ref .st_extra_dbits 0,
187                       extra_base := 0, elems := D_CODES, max_length := MAX_BITS }
188    static_bl_desc := { static_tree := .null, extra_bits := .ref .st_extra_blbits 0,
189                        extra_base := 0, elems := BL_CODES, max_length := MAX_BL_BITS } }
190
191/-- The heap with the static data of `trees.c` and `trees.h` in place. -/
192def install_trees (h : Heap) : Heap := { h with static := trees_statics h.static }
193
194/-! ## Helpers (not C functions): checked `int` arithmetic, record and array access -/
195
196/-- A checked `int` result. -/
197def ck (x : Int) : M Int32 :=
198  if -2147483648 ≤ x ∧ x ≤ 2147483647 then pure (Int32.ofInt x) else ub "signed integer overflow"
199def iadd (a b : Int32) : M Int32 := ck (a.toInt + b.toInt)
200def isub (a b : Int32) : M Int32 := ck (a.toInt - b.toInt)
201/-- `x << 1` for an `int`: undefined for a negative `x` or if the result does not fit. -/
202def shl1 (x : Int32) : M Int32 := if x.toInt < 0 then ub "left shift of a negative value" else ck (x.toInt * 2)
203/-- `ush` to `int`. -/
204def u16i (x : UInt16) : Int32 := Int32.ofInt x.toNat
205/-- `uch` to `int`. -/
206def u8i (x : UInt8) : Int32 := Int32.ofInt x.toNat
207/-- `int` to `unsigned` (modulo 2^32). -/
208def i2u (x : Int32) : UInt32 := UInt32.ofNat (x.toInt % 4294967296).toNat
209/-- `unsigned` to `int` (modulo 2^32, as gcc). -/
210def u2i (x : UInt32) : Int32 := Int32.ofInt (if x.toNat ≥ 2147483648 then (x.toNat : Int) - 4294967296 else x.toNat)
211/-- `int` to `unsigned long` (sign extension, modulo 2^64). -/
212def i2ul (x : Int32) : UInt64 := UInt64.ofNat (x.toInt % 18446744073709551616).toNat
213/-- `(ush)x` for an `int`. -/
214def i2us (x : Int32) : UInt16 := UInt16.ofNat (x.toInt % 65536).toNat
215
216/-- `for (init; cond; step) body` over the locals `σ`; `continue` is the end of `body`. -/
217def cfor {σ : Type} (cond : σ → M Bool) (step : σ → M σ) (body : σ → M σ) (s : σ) : M σ :=
218  cwhile (fun s => do pure (← cond s, s)) (fun s => do step (← body s)) s
219
220/-- `s` is a live deflate state; its block number. -/
221def sid (s : DeflateStatePtr) : M Nat := do
222  let _ ← ldDeflateState s
223  match s with
224  | some (.tab i) => pure i
225  | none => ub "null dereference (deflate_state)"
226
227/-- `s->f` for a scalar field: the whole record. -/
228def rd (s : DeflateStatePtr) : M DeflateState := ldDeflateState s
229/-- `s->f = v`, as a load, a record update and a store. -/
230def md (s : DeflateStatePtr) (f : DeflateState → DeflateState) : M Unit := do
231  stDeflateState s (f (← ldDeflateState s))
232
233/-- `s->dyn_ltree` -/
234def pLtree (s : DeflateStatePtr) : M CtDataPtr := do pure (.ref (.dstate_dyn_ltree (← sid s)) 0)
235/-- `s->dyn_dtree` -/
236def pDtree (s : DeflateStatePtr) : M CtDataPtr := do pure (.ref (.dstate_dyn_dtree (← sid s)) 0)
237/-- `s->bl_tree` -/
238def pBltree (s : DeflateStatePtr) : M CtDataPtr := do pure (.ref (.dstate_bl_tree (← sid s)) 0)
239/-- `s->heap` -/
240def pHeap (s : DeflateStatePtr) : M IPtr := do pure (.ref (.dstate_heap (← sid s)) 0)
241/-- `s->depth` -/
242def pDepth (s : DeflateStatePtr) : M BPtr := do pure (.ref (.dstate_depth (← sid s)) 0)
243/-- `s->bl_count` -/
244def pBlCount (s : DeflateStatePtr) : M WPtr := do pure (.ref (.dstate_bl_count (← sid s)) 0)
245/-- `&s->l_desc`, `&s->d_desc`, `&s->bl_desc` -/
246def pLdesc (s : DeflateStatePtr) : M TreeDescPtr := do pure (some (.in_dstate_l_desc (← sid s)))
247def pDdesc (s : DeflateStatePtr) : M TreeDescPtr := do pure (some (.in_dstate_d_desc (← sid s)))
248def pBldesc (s : DeflateStatePtr) : M TreeDescPtr := do pure (some (.in_dstate_bl_desc (← sid s)))
249
250/-- `p[i] = v` -/
251def setAt {R T : Type} [Space Heap R T] (p : Ptr R) (i : Int) (v : T) : M Unit := do
252  Ptr.store (← Ptr.add p i) v
253/-- `s->heap[i]` -/
254def heapAt (s : DeflateStatePtr) (i : Int32) : M Int32 := do Ptr.index (← pHeap s) i.toInt
255/-- `s->heap[i] = v` -/
256def heapSet (s : DeflateStatePtr) (i : Int32) (v : Int32) : M Unit := do setAt (← pHeap s) i.toInt v
257
258/-- `tree[i].Freq` / `.Code` -/
259def getFc (tree : CtDataPtr) (i : Int) : M UInt16 := do pure (← Ptr.index tree i).fc
260/-- `tree[i].Dad` / `.Len` -/
261def getDl (tree : CtDataPtr) (i : Int) : M UInt16 := do pure (← Ptr.index tree i).dl
262/-- `tree[i].Freq = v` -/
263def setFc (tree : CtDataPtr) (i : Int) (v : UInt16) : M Unit := do
264  let p ← Ptr.add tree i
265  let e ← Ptr.load p
266  Ptr.store p { e with fc := v }
267/-- `tree[i].Len = v` -/
268def setDl (tree : CtDataPtr) (i : Int) (v : UInt16) : M Unit := do
269  let p ← Ptr.add tree i
270  let e ← Ptr.load p
271  Ptr.store p { e with dl := v }
272
273/-- `bl_order[i]` (a static array; an index outside it is undefined). -/
274def blOrder (i : Int) : M UInt8 :=
275  if 0 ≤ i ∧ i < 19 then pure bl_order[i.toNat]! else ub "bl_order index outside its array"
276
277/-! ## Macros of `deflate.h` and `trees.c` -/
278
279/-- `put_byte(s, c)`: `{s->pending_buf[s->pending++] = (Bytef)(c);}` -/
280def put_byte (s : DeflateStatePtr) (c : UInt8) : M Unit := do
281  let d ← rd s
282  let p ← Ptr.add d.pending_buf (d.pending.toNat : Int)
283  store8 p c
284  md s fun d => { d with pending := d.pending + 1 }
285
286/-- `put_short(s, w)`: `{ put_byte(s, (uch)((w) & 0xff)); put_byte(s, (uch)((ush)(w) >> 8)); }` -/
287def put_short (s : DeflateStatePtr) (w : UInt16) : M Unit := do
288  put_byte s (w &&& 0xff).toUInt8
289  put_byte s (w >>> 8).toUInt8
290
291/-- `(ush)val << s->bi_valid` (an `int` shift: the count must be in `0..31` and the result must fit). -/
292def shlUs (val : Int32) (c : Int32) : M Nat :=
293  if c.toInt < 0 ∨ 31 < c.toInt then ub "invalid shift count"
294  else if (i2us val).toNat * 2 ^ c.toInt.toNat ≥ 2147483648 then ub "signed overflow in left shift"
295  else pure ((i2us val).toNat * 2 ^ c.toInt.toNat)
296
297/-- `(ush)val >> c` -/
298def shrUs (val : Int32) (c : Int32) : M UInt16 :=
299  if c.toInt < 0 ∨ 31 < c.toInt then ub "invalid shift count"
300  else pure (UInt16.ofNat ((i2us val).toNat >>> c.toInt.toNat))
301
302/-- `send_bits(s, value, length)` (the macro of `trees.c`, `Buf_size` = 16). -/
303def send_bits (s : DeflateStatePtr) (value : Int32) (length : Int32) : M Unit := do
304  -- int len = length;
305  let len := length
306  let d ← rd s
307  if d.bi_valid > (← isub Buf_size len) then
308    -- int val = (int)value;
309    let val := value
310    -- s->bi_buf |= (ush)val << s->bi_valid;
311    let sh ← shlUs val d.bi_valid
312    md s fun d => { d with bi_buf := UInt16.ofNat (d.bi_buf.toNat ||| sh) }
313    -- put_short(s, s->bi_buf);
314    put_short s (← rd s).bi_buf
315    -- s->bi_buf = (ush)val >> (Buf_size - s->bi_valid);
316    let c ← isub Buf_size (← rd s).bi_valid
317    let r ← shrUs val c
318    md s fun d => { d with bi_buf := r }
319    -- s->bi_valid += len - Buf_size;
320    let t ← isub len Buf_size
321    let nv ← iadd (← rd s).bi_valid t
322    md s fun d => { d with bi_valid := nv }
323  else
324    -- s->bi_buf |= (ush)(value) << s->bi_valid;
325    let sh ← shlUs value d.bi_valid
326    md s fun d => { d with bi_buf := UInt16.ofNat (d.bi_buf.toNat ||| sh) }
327    -- s->bi_valid += len;
328    let nv ← iadd (← rd s).bi_valid len
329    md s fun d => { d with bi_valid := nv }
330
331/-- `send_code(s, c, tree)`: `send_bits(s, tree[c].Code, tree[c].Len)`. -/
332def send_code (s : DeflateStatePtr) (c : Int) (tree : CtDataPtr) : M Unit := do
333  let len := u16i (← getDl tree c)
334  let code := u16i (← getFc tree c)
335  send_bits s code len
336
337/-- `d_code(dist)`: `((dist) < 256 ? _dist_code[dist] : _dist_code[256+((dist)>>7)])`, `dist` unsigned. -/
338def d_code (dist : UInt32) : M UInt8 :=
339  if dist < 256 then Ptr.index (.ref .st_dist_code 0 : BPtr) (dist.toNat : Int)
340  else Ptr.index (.ref .st_dist_code 0 : BPtr) (((256 : UInt32) + (dist >>> 7)).toNat : Int)
341
342/-- `smaller(tree, n, m, depth)` -/
343def smaller (tree : CtDataPtr) (n m : Int32) (depth : BPtr) : M Bool := do
344  let fn ← getFc tree n.toInt
345  let fm ← getFc tree m.toInt
346  if fn < fm then return true
347  if fn == fm then
348    let dn ← Ptr.index depth n.toInt
349    let dm ← Ptr.index depth m.toInt
350    return decide (dn ≤ dm)
351  return false
352
353/-! ## Functions -/
354
355/-- `local unsigned bi_reverse(unsigned code, int len)` -/
356def bi_reverse (code : UInt32) (len : Int32) : M UInt32 := do
357  -- unsigned res = 0;
358  -- do { res |= code & 1; code >>= 1, res <<= 1; } while (--len > 0);
359  let (_, res, _) ← cdoWhile (σ := UInt32 × UInt32 × Int32)
360    (fun (code, res, len) => do
361      let res := res ||| (code &&& 1)
362      pure (code >>> 1, res <<< 1, len))
363    (fun (code, res, len) => do
364      let len ← isub len 1
365      pure (decide (len.toInt > 0), (code, res, len)))
366    (code, 0, len)
367  return res >>> 1
368
369/-- `local void bi_flush(deflate_state *s)` -/
370def bi_flush (s : DeflateStatePtr) : M Unit := do
371  let d ← rd s
372  if d.bi_valid == 16 then
373    put_short s (← rd s).bi_buf
374    md s fun d => { d with bi_buf := 0 }
375    md s fun d => { d with bi_valid := 0 }
376  else if d.bi_valid ≥ 8 then
377    put_byte s (← rd s).bi_buf.toUInt8
378    md s fun d => { d with bi_buf := d.bi_buf >>> 8 }
379    let nv ← isub (← rd s).bi_valid 8
380    md s fun d => { d with bi_valid := nv }
381
382/-- `local void bi_windup(deflate_state *s)` -/
383def bi_windup (s : DeflateStatePtr) : M Unit := do
384  let d ← rd s
385  if d.bi_valid > 8 then
386    put_short s (← rd s).bi_buf
387  else if d.bi_valid > 0 then
388    put_byte s (← rd s).bi_buf.toUInt8
389  -- s->bi_used = ((s->bi_valid - 1) & 7) + 1;
390  let t ← isub (← rd s).bi_valid 1
391  let u ← iadd (t &&& 7) 1
392  md s fun d => { d with bi_used := u }
393  md s fun d => { d with bi_buf := 0 }
394  md s fun d => { d with bi_valid := 0 }
395
396/-- `local void gen_codes(ct_data *tree, int max_code, ushf *bl_count)` -/
397def gen_codes (tree : CtDataPtr) (max_code : Int32) (bl_count : WPtr) : M Unit := do
398  -- ush next_code[MAX_BITS+1]; unsigned code = 0;
399  let next_code0 : Array UInt16 := Array.replicate 16 0
400  -- for (bits = 1; bits <= MAX_BITS; bits++) { code = (code + bl_count[bits - 1]) << 1; next_code[bits] = (ush)code; }
401  let (_, _, next_code) ← cfor (σ := Int32 × UInt32 × Array UInt16)
402    (fun (bits, _, _) => pure (decide (bits.toInt ≤ MAX_BITS.toInt)))
403    (fun (bits, code, nc) => do pure (← iadd bits 1, code, nc))
404    (fun (bits, code, nc) => do
405      let b ← Ptr.index bl_count (← isub bits 1).toInt
406      let code := (code + b.toUInt32) <<< 1
407      if bits.toInt < 0 ∨ nc.size ≤ bits.toInt.toNat then ub "next_code index outside its array"
408      pure (bits, code, nc.set! bits.toInt.toNat code.toUInt16))
409    (1, 0, next_code0)
410  -- for (n = 0; n <= max_code; n++) { int len = tree[n].Len; if (len == 0) continue;
411  --   tree[n].Code = (ush)bi_reverse(next_code[len]++, len); }
412  let _ ← cfor (σ := Int32 × Array UInt16)
413    (fun (n, _) => pure (decide (n.toInt ≤ max_code.toInt)))
414    (fun (n, nc) => do pure (← iadd n 1, nc))
415    (fun (n, nc) => do
416      let len := u16i (← getDl tree n.toInt)
417      if len == 0 then return (n, nc)
418      let li := len.toInt.toNat
419      if nc.size ≤ li then ub "next_code index outside its array"
420      let old := nc[li]!
421      let nc := nc.set! li (old + 1)
422      let r ← bi_reverse old.toUInt32 len
423      setFc tree n.toInt r.toUInt16
424      pure (n, nc))
425    (0, next_code)
426
427/-- `local void tr_static_init(void)`: the body is inside `#if defined(GEN_TREES_H) || !defined(STDC)`, which is
428false in the default build, so the function is empty. -/
429def tr_static_init : M Unit := pure ()
430
431/-- `local void init_block(deflate_state *s)` -/
432def init_block (s : DeflateStatePtr) : M Unit := do
433  -- for (n = 0; n < L_CODES; n++) s->dyn_ltree[n].Freq = 0;
434  let _ ← cfor (σ := Int32) (fun n => pure (decide (n.toInt < L_CODES.toInt))) (fun n => iadd n 1)
435    (fun n => do setFc (← pLtree s) n.toInt 0; pure n) 0
436  let _ ← cfor (σ := Int32) (fun n => pure (decide (n.toInt < D_CODES.toInt))) (fun n => iadd n 1)
437    (fun n => do setFc (← pDtree s) n.toInt 0; pure n) 0
438  let _ ← cfor (σ := Int32) (fun n => pure (decide (n.toInt < BL_CODES.toInt))) (fun n => iadd n 1)
439    (fun n => do setFc (← pBltree s) n.toInt 0; pure n) 0
440  -- s->dyn_ltree[END_BLOCK].Freq = 1;
441  setFc (← pLtree s) END_BLOCK.toInt 1
442  -- s->opt_len = s->static_len = 0L;
443  md s fun d => { d with static_len := 0 }
444  md s fun d => { d with opt_len := 0 }
445  -- s->sym_next = s->matches = 0;
446  md s fun d => { d with «matches» := 0 }
447  md s fun d => { d with sym_next := 0 }
448
449/-- `void ZLIB_INTERNAL _tr_init(deflate_state *s)` -/
450def «_tr_init» (s : DeflateStatePtr) : M Unit := do
451  tr_static_init
452  let id ← sid s
453  md s fun d => { d with l_desc := { d.l_desc with dyn_tree := .ref (.dstate_dyn_ltree id) 0 } }
454  md s fun d => { d with l_desc := { d.l_desc with stat_desc := some .st_static_l_desc } }
455  md s fun d => { d with d_desc := { d.d_desc with dyn_tree := .ref (.dstate_dyn_dtree id) 0 } }
456  md s fun d => { d with d_desc := { d.d_desc with stat_desc := some .st_static_d_desc } }
457  md s fun d => { d with bl_desc := { d.bl_desc with dyn_tree := .ref (.dstate_bl_tree id) 0 } }
458  md s fun d => { d with bl_desc := { d.bl_desc with stat_desc := some .st_static_bl_desc } }
459  md s fun d => { d with bi_buf := 0 }
460  md s fun d => { d with bi_valid := 0 }
461  md s fun d => { d with bi_used := 0 }
462  -- Initialize the first block of the first file:
463  init_block s
464
465/-- `local void pqdownheap(deflate_state *s, ct_data *tree, int k)` -/
466def pqdownheap (s : DeflateStatePtr) (tree : CtDataPtr) (k : Int32) : M Unit := do
467  -- int v = s->heap[k]; int j = k << 1;
468  let v ← heapAt s k
469  let j ← shl1 k
470  -- while (j <= s->heap_len) { ... }   (the flag is the `break`)
471  let (k, _, _) ← cwhile (σ := Int32 × Int32 × Bool)
472    (fun (k, j, brk) => do
473      if brk then return (false, (k, j, brk))
474      pure (decide (j.toInt ≤ (← rd s).heap_len.toInt), (k, j, brk)))
475    (fun (k, j, _) => do
476      let mut jj := j
477      -- if (j < s->heap_len && smaller(tree, s->heap[j + 1], s->heap[j], s->depth)) j++;
478      if jj.toInt < (← rd s).heap_len.toInt then
479        let a ← heapAt s (← iadd jj 1)
480        let b ← heapAt s jj
481        if ← smaller tree a b (← pDepth s) then jj ← iadd jj 1
482      -- if (smaller(tree, v, s->heap[j], s->depth)) break;
483      let hj ← heapAt s jj
484      if ← smaller tree v hj (← pDepth s) then return (k, jj, true)
485      -- s->heap[k] = s->heap[j];  k = j;
486      heapSet s k hj
487      -- j <<= 1;
488      let j2 ← shl1 jj
489      return (jj, j2, false))
490    (k, j, false)
491  -- s->heap[k] = v;
492  heapSet s k v
493
494/-- `pqremove(s, tree, top)`: `{ top = s->heap[SMALLEST]; s->heap[SMALLEST] = s->heap[s->heap_len--];
495pqdownheap(s, tree, SMALLEST); }`; returns `top`. -/
496def pqremove (s : DeflateStatePtr) (tree : CtDataPtr) : M Int32 := do
497  let top ← heapAt s 1
498  -- s->heap[SMALLEST] = s->heap[s->heap_len--];
499  let hl := (← rd s).heap_len
500  let v ← heapAt s hl
501  let hl' ← isub hl 1
502  md s fun d => { d with heap_len := hl' }
503  heapSet s 1 v
504  pqdownheap s tree 1
505  return top
506
507/-- `local void gen_bitlen(deflate_state *s, tree_desc *desc)` -/
508def gen_bitlen (s : DeflateStatePtr) (desc : TreeDescPtr) : M Unit := do
509  let dd ← ldTreeDesc desc
510  let tree := dd.dyn_tree
511  let max_code := dd.max_code
512  let sd ← ldStaticTreeDesc dd.stat_desc
513  let stree := sd.static_tree
514  let extra := sd.extra_bits
515  let base := sd.extra_base
516  let max_length := sd.max_length
517  -- for (bits = 0; bits <= MAX_BITS; bits++) s->bl_count[bits] = 0;
518  let _ ← cfor (σ := Int32) (fun b => pure (decide (b.toInt ≤ MAX_BITS.toInt))) (fun b => iadd b 1)
519    (fun b => do setAt (← pBlCount s) b.toInt 0; pure b) 0
520  -- tree[s->heap[s->heap_max]].Len = 0;
521  setDl tree (← heapAt s (← rd s).heap_max).toInt 0
522  -- for (h = s->heap_max + 1; h < HEAP_SIZE; h++) { ... }     state (h, overflow)
523  let h0 ← iadd (← rd s).heap_max 1
524  let (h, overflow) ← cfor (σ := Int32 × Int32)
525    (fun (h, _) => pure (decide (h.toInt < HEAP_SIZE.toInt)))
526    (fun (h, o) => do pure (← iadd h 1, o))
527    (fun (h, overflow) => do
528      let n ← heapAt s h
529      -- bits = tree[tree[n].Dad].Len + 1;
530      let mut bits ← iadd (u16i (← getDl tree (u16i (← getDl tree n.toInt)).toInt)) 1
531      let mut overflow := overflow
532      -- if (bits > max_length) bits = max_length, overflow++;
533      if bits.toInt > max_length.toInt then
534        bits := max_length
535        overflow ← iadd overflow 1
536      -- tree[n].Len = (ush)bits;
537      setDl tree n.toInt (i2us bits)
538      -- if (n > max_code) continue;
539      if n.toInt > max_code.toInt then return (h, overflow)
540      -- s->bl_count[bits]++;
541      let bc ← pBlCount s
542      setAt bc bits.toInt ((← Ptr.index bc bits.toInt) + 1)
543      -- xbits = 0; if (n >= base) xbits = extra[n - base];
544      let mut xbits : Int32 := 0
545      if n.toInt ≥ base.toInt then xbits ← Ptr.index extra (← isub n base).toInt
546      -- f = tree[n].Freq;
547      let f ← getFc tree n.toInt
548      -- s->opt_len += (ulg)f * (unsigned)(bits + xbits);
549      let t ← iadd bits xbits
550      md s fun d => { d with opt_len := d.opt_len + f.toUInt64 * (i2u t).toUInt64 }
551      -- if (stree) s->static_len += (ulg)f * (unsigned)(stree[n].Len + xbits);
552      if stree != .null then
553        let t2 ← iadd (u16i (← getDl stree n.toInt)) xbits
554        md s fun d => { d with static_len := d.static_len + f.toUInt64 * (i2u t2).toUInt64 }
555      return (h, overflow))
556    (h0, 0)
557  -- if (overflow == 0) return;
558  if overflow == 0 then return
559  -- do { bits = max_length-1; while (bl_count[bits]==0) bits--; ... overflow -= 2; } while (overflow > 0);
560  let _ ← cdoWhile (σ := Int32)
561    (fun overflow => do
562      let bits ← isub max_length 1
563      let bc ← pBlCount s
564      let bits ← cwhile (σ := Int32)
565        (fun b => do pure (decide ((← Ptr.index bc b.toInt) == 0), b))
566        (fun b => isub b 1) bits
567      setAt bc bits.toInt ((← Ptr.index bc bits.toInt) - 1)
568      let b1 ← iadd bits 1
569      setAt bc b1.toInt ((← Ptr.index bc b1.toInt) + 2)
570      setAt bc max_length.toInt ((← Ptr.index bc max_length.toInt) - 1)
571      isub overflow 2)
572    (fun overflow => pure (decide (overflow.toInt > 0), overflow))
573    overflow
574  -- for (bits = max_length; bits != 0; bits--) { n = s->bl_count[bits]; while (n != 0) { ... } }
575  let _ ← cfor (σ := Int32 × Int32)
576    (fun (bits, _) => pure (bits != 0))
577    (fun (bits, h) => do pure (← isub bits 1, h))
578    (fun (bits, h) => do
579      let n0 := u16i (← Ptr.index (← pBlCount s) bits.toInt)
580      let (_, h) ← cwhile (σ := Int32 × Int32)
581        (fun (n, h) => pure (n != 0, (n, h)))
582        (fun (n, h) => do
583          -- m = s->heap[--h];
584          let h ← isub h 1
585          let m ← heapAt s h
586          -- if (m > max_code) continue;
587          if m.toInt > max_code.toInt then return (n, h)
588          -- if ((unsigned) tree[m].Len != (unsigned) bits) {...}
589          let lm ← getDl tree m.toInt
590          if lm.toUInt32 != i2u bits then
591            -- s->opt_len += ((ulg)bits - tree[m].Len) * tree[m].Freq;
592            let fm ← getFc tree m.toInt
593            md s fun d => { d with opt_len := d.opt_len + (i2ul bits - lm.toUInt64) * fm.toUInt64 }
594            setDl tree m.toInt (i2us bits)
595          -- n--;
596          pure (← isub n 1, h))
597        (n0, h)
598      pure (bits, h))
599    (max_length, h)
600
601/-- `local void build_tree(deflate_state *s, tree_desc *desc)` -/
602def build_tree (s : DeflateStatePtr) (desc : TreeDescPtr) : M Unit := do
603  let dd ← ldTreeDesc desc
604  let tree := dd.dyn_tree
605  let sd ← ldStaticTreeDesc dd.stat_desc
606  let stree := sd.static_tree
607  let elems := sd.elems
608  -- int max_code = -1;
609  -- s->heap_len = 0, s->heap_max = HEAP_SIZE;
610  md s fun d => { d with heap_len := 0 }
611  md s fun d => { d with heap_max := HEAP_SIZE }
612  -- for (n = 0; n < elems; n++) { if (tree[n].Freq != 0) {...} else tree[n].Len = 0; }
613  let max_code ← cfor (σ := Int32 × Int32)
614    (fun (n, _) => pure (decide (n.toInt < elems.toInt)))
615    (fun (n, mc) => do pure (← iadd n 1, mc))
616    (fun (n, mc) => do
617      if (← getFc tree n.toInt) != 0 then
618        -- s->heap[++(s->heap_len)] = max_code = n;
619        let hl ← iadd (← rd s).heap_len 1
620        md s fun d => { d with heap_len := hl }
621        heapSet s hl n
622        -- s->depth[n] = 0;
623        setAt (← pDepth s) n.toInt 0
624        pure (n, n)
625      else
626        setDl tree n.toInt 0
627        pure (n, mc))
628    (0, -1)
629  let mut max_code := max_code.2
630  -- while (s->heap_len < 2) { ... }
631  let mc ← cwhile (σ := Int32)
632    (fun mc => do pure (decide ((← rd s).heap_len.toInt < 2), mc))
633    (fun mc => do
634      -- node = s->heap[++(s->heap_len)] = (max_code < 2 ? ++max_code : 0);
635      let mut mc := mc
636      let mut val : Int32 := 0
637      if mc.toInt < 2 then
638        mc ← iadd mc 1
639        val := mc
640      let hl ← iadd (← rd s).heap_len 1
641      md s fun d => { d with heap_len := hl }
642      heapSet s hl val
643      let node := val
644      -- tree[node].Freq = 1; s->depth[node] = 0;
645      setFc tree node.toInt 1
646      setAt (← pDepth s) node.toInt 0
647      -- s->opt_len--; if (stree) s->static_len -= stree[node].Len;
648      md s fun d => { d with opt_len := d.opt_len - 1 }
649      if stree != .null then
650        let l ← getDl stree node.toInt
651        md s fun d => { d with static_len := d.static_len - l.toUInt64 }
652      pure mc)
653    max_code
654  max_code := mc
655  -- desc->max_code = max_code;
656  stTreeDesc desc { (← ldTreeDesc desc) with max_code := max_code }
657  -- for (n = s->heap_len/2; n >= 1; n--) pqdownheap(s, tree, n);
658  let _ ← cfor (σ := Int32) (fun n => pure (decide (n.toInt ≥ 1))) (fun n => isub n 1)
659    (fun n => do pqdownheap s tree n; pure n) ((← rd s).heap_len / 2)
660  -- node = elems;
661  -- do { ... } while (s->heap_len >= 2);
662  let _ ← cdoWhile (σ := Int32)
663    (fun node => do
664      -- pqremove(s, tree, n);  m = s->heap[SMALLEST];
665      let n ← pqremove s tree
666      let m ← heapAt s 1
667      -- s->heap[--(s->heap_max)] = n;  s->heap[--(s->heap_max)] = m;
668      let hm ← isub (← rd s).heap_max 1
669      md s fun d => { d with heap_max := hm }
670      heapSet s hm n
671      let hm ← isub (← rd s).heap_max 1
672      md s fun d => { d with heap_max := hm }
673      heapSet s hm m
674      -- tree[node].Freq = tree[n].Freq + tree[m].Freq;
675      let fn ← getFc tree n.toInt
676      let fm ← getFc tree m.toInt
677      setFc tree node.toInt (fn + fm)
678      -- s->depth[node] = (uch)((s->depth[n] >= s->depth[m] ? s->depth[n] : s->depth[m]) + 1);
679      let dp ← pDepth s
680      let dn ← Ptr.index dp n.toInt
681      let dm ← Ptr.index dp m.toInt
682      let mx ← if dn ≥ dm then Ptr.index dp n.toInt else Ptr.index dp m.toInt
683      setAt dp node.toInt (mx + 1)
684      -- tree[n].Dad = tree[m].Dad = (ush)node;
685      setDl tree m.toInt (i2us node)
686      setDl tree n.toInt (i2us node)
687      -- s->heap[SMALLEST] = node++;
688      heapSet s 1 node
689      let node' ← iadd node 1
690      pqdownheap s tree 1
691      pure node')
692    (fun node => do pure (decide ((← rd s).heap_len.toInt ≥ 2), node))
693    elems
694  -- s->heap[--(s->heap_max)] = s->heap[SMALLEST];
695  let top ← heapAt s 1
696  let hm ← isub (← rd s).heap_max 1
697  md s fun d => { d with heap_max := hm }
698  heapSet s hm top
699  -- gen_bitlen(s, (tree_desc *)desc);
700  gen_bitlen s desc
701  -- gen_codes ((ct_data *)tree, max_code, s->bl_count);
702  gen_codes tree max_code (← pBlCount s)
703
704/-- `local void scan_tree(deflate_state *s, ct_data *tree, int max_code)` -/
705def scan_tree (s : DeflateStatePtr) (tree : CtDataPtr) (max_code : Int32) : M Unit := do
706  -- locals: n, prevlen, curlen, nextlen, count, max_count, min_count
707  let nextlen0 := u16i (← getDl tree 0)
708  let (mx0, mn0) : Int32 × Int32 := if nextlen0 == 0 then (138, 3) else (7, 4)
709  -- tree[max_code + 1].Len = (ush)0xffff;
710  setDl tree (← iadd max_code 1).toInt 0xffff
711  let _ ← cfor (σ := Int32 × Int32 × Int32 × Int32 × Int32 × Int32 × Int32)
712    (fun (n, _) => pure (decide (n.toInt ≤ max_code.toInt)))
713    (fun (n, r) => do pure (← iadd n 1, r))
714    (fun (n, prevlen, nextlen, count, max_count, min_count, _) => do
715      -- curlen = nextlen; nextlen = tree[n + 1].Len;
716      let curlen := nextlen
717      let nextlen := u16i (← getDl tree (← iadd n 1).toInt)
718      -- if (++count < max_count && curlen == nextlen) continue;
719      let count ← iadd count 1
720      if count.toInt < max_count.toInt ∧ curlen == nextlen then
721        return (n, prevlen, nextlen, count, max_count, min_count, 0)
722      let blt ← pBltree s
723      if count.toInt < min_count.toInt then
724        -- s->bl_tree[curlen].Freq += (ush)count;
725        setFc blt curlen.toInt ((← getFc blt curlen.toInt) + i2us count)
726      else if curlen != 0 then
727        -- if (curlen != prevlen) s->bl_tree[curlen].Freq++;
728        if curlen != prevlen then setFc blt curlen.toInt ((← getFc blt curlen.toInt) + 1)
729        setFc blt REP_3_6.toInt ((← getFc blt REP_3_6.toInt) + 1)
730      else if count.toInt ≤ 10 then
731        setFc blt REPZ_3_10.toInt ((← getFc blt REPZ_3_10.toInt) + 1)
732      else
733        setFc blt REPZ_11_138.toInt ((← getFc blt REPZ_11_138.toInt) + 1)
734      -- count = 0; prevlen = curlen;
735      let count : Int32 := 0
736      let prevlen := curlen
737      let (max_count, min_count) : Int32 × Int32 :=
738        if nextlen == 0 then (138, 3) else if curlen == nextlen then (6, 3) else (7, 4)
739      return (n, prevlen, nextlen, count, max_count, min_count, 0))
740    (0, -1, nextlen0, 0, mx0, mn0, 0)
741
742/-- `local void send_tree(deflate_state *s, ct_data *tree, int max_code)` -/
743def send_tree (s : DeflateStatePtr) (tree : CtDataPtr) (max_code : Int32) : M Unit := do
744  let nextlen0 := u16i (← getDl tree 0)
745  -- /* tree[max_code + 1].Len = -1; */  /* guard already set */
746  let (mx0, mn0) : Int32 × Int32 := if nextlen0 == 0 then (138, 3) else (7, 4)
747  let _ ← cfor (σ := Int32 × Int32 × Int32 × Int32 × Int32 × Int32 × Int32)
748    (fun (n, _) => pure (decide (n.toInt ≤ max_code.toInt)))
749    (fun (n, r) => do pure (← iadd n 1, r))
750    (fun (n, prevlen, nextlen, count, max_count, min_count, _) => do
751      let curlen := nextlen
752      let nextlen := u16i (← getDl tree (← iadd n 1).toInt)
753      let mut count ← iadd count 1
754      if count.toInt < max_count.toInt ∧ curlen == nextlen then
755        return (n, prevlen, nextlen, count, max_count, min_count, 0)
756      if count.toInt < min_count.toInt then
757        -- do { send_code(s, curlen, s->bl_tree); } while (--count != 0);
758        count ← cdoWhile (σ := Int32)
759          (fun c => do send_code s curlen.toInt (← pBltree s); pure c)
760          (fun c => do let c ← isub c 1; pure (c != 0, c))
761          count
762      else if curlen != 0 then
763        if curlen != prevlen then
764          send_code s curlen.toInt (← pBltree s)
765          count ← isub count 1
766        send_code s REP_3_6.toInt (← pBltree s)
767        send_bits s (← isub count 3) 2
768      else if count.toInt ≤ 10 then
769        send_code s REPZ_3_10.toInt (← pBltree s)
770        send_bits s (← isub count 3) 3
771      else
772        send_code s REPZ_11_138.toInt (← pBltree s)
773        send_bits s (← isub count 11) 7
774      -- count = 0; prevlen = curlen;
775      count := 0
776      let prevlen := curlen
777      let (max_count, min_count) : Int32 × Int32 :=
778        if nextlen == 0 then (138, 3) else if curlen == nextlen then (6, 3) else (7, 4)
779      return (n, prevlen, nextlen, count, max_count, min_count, 0))
780    (0, -1, nextlen0, 0, mx0, mn0, 0)
781
782/-- `local int build_bl_tree(deflate_state *s)` -/
783def build_bl_tree (s : DeflateStatePtr) : M Int32 := do
784  -- scan_tree(s, (ct_data *)s->dyn_ltree, s->l_desc.max_code);
785  scan_tree s (← pLtree s) (← rd s).l_desc.max_code
786  scan_tree s (← pDtree s) (← rd s).d_desc.max_code
787  -- build_tree(s, (tree_desc *)(&(s->bl_desc)));
788  build_tree s (← pBldesc s)
789  -- for (max_blindex = BL_CODES-1; max_blindex >= 3; max_blindex--) { if (...Len != 0) break; }
790  let (mb, _) ← cwhile (σ := Int32 × Bool)
791    (fun (mb, brk) => pure (!brk && decide (mb.toInt ≥ 3), (mb, brk)))
792    (fun (mb, _) => do
793      if (← getDl (← pBltree s) (u8i (← blOrder mb.toInt)).toInt) != 0 then return (mb, true)
794      pure (← isub mb 1, false))
795    (BL_CODES - 1, false)
796  -- s->opt_len += 3*((ulg)max_blindex + 1) + 5 + 5 + 4;
797  md s fun d => { d with opt_len := d.opt_len + (3 * (i2ul mb + 1) + 5 + 5 + 4) }
798  return mb
799
800/-- `local void send_all_trees(deflate_state *s, int lcodes, int dcodes, int blcodes)` -/
801def send_all_trees (s : DeflateStatePtr) (lcodes dcodes blcodes : Int32) : M Unit := do
802  send_bits s (← isub lcodes 257) 5
803  send_bits s (← isub dcodes 1) 5
804  send_bits s (← isub blcodes 4) 4
805  -- for (rank = 0; rank < blcodes; rank++) send_bits(s, s->bl_tree[bl_order[rank]].Len, 3);
806  let _ ← cfor (σ := Int32) (fun r => pure (decide (r.toInt < blcodes.toInt))) (fun r => iadd r 1)
807    (fun r => do
808      let l ← getDl (← pBltree s) (u8i (← blOrder r.toInt)).toInt
809      send_bits s (u16i l) 3
810      pure r) 0
811  send_tree s (← pLtree s) (← isub lcodes 1)
812  send_tree s (← pDtree s) (← isub dcodes 1)
813
814/-- `void ZLIB_INTERNAL _tr_stored_block(deflate_state *s, charf *buf, ulg stored_len, int last)` -/
815def «_tr_stored_block» (s : DeflateStatePtr) (buf : BPtr) (stored_len : UInt64) (last : Int32) : M Unit := do
816  -- send_bits(s, (STORED_BLOCK<<1) + last, 3);
817  send_bits s (← iadd (STORED_BLOCK <<< 1) last) 3
818  bi_windup s
819  put_short s stored_len.toUInt16
820  put_short s (~~~stored_len).toUInt16
821  -- if (stored_len) zmemcpy(s->pending_buf + s->pending, (Bytef *)buf, stored_len);
822  if stored_len != 0 then
823    let d ← rd s
824    let dst ← Ptr.add d.pending_buf (d.pending.toNat : Int)
825    memcpyB dst buf stored_len.toNat
826  md s fun d => { d with pending := d.pending + stored_len }
827
828/-- `void ZLIB_INTERNAL _tr_flush_bits(deflate_state *s)` -/
829def «_tr_flush_bits» (s : DeflateStatePtr) : M Unit := bi_flush s
830
831/-- `void ZLIB_INTERNAL _tr_align(deflate_state *s)` -/
832def «_tr_align» (s : DeflateStatePtr) : M Unit := do
833  send_bits s (STATIC_TREES <<< 1) 3
834  send_code s END_BLOCK.toInt (.ref .st_static_ltree 0)
835  bi_flush s
836
837/-- `local void compress_block(deflate_state *s, const ct_data *ltree, const ct_data *dtree)` -/
838def compress_block (s : DeflateStatePtr) (ltree dtree : CtDataPtr) : M Unit := do
839  let lcp : BPtr := .ref .st_length_code 0
840  -- if (s->sym_next != 0) do { ... } while (sx < s->sym_next);
841  if (← rd s).sym_next != 0 then
842    let _ ← cdoWhile (σ := UInt32)
843      (fun sx => do
844        -- dist = s->sym_buf[sx++] & 0xff;
845        let sb := (← rd s).sym_buf
846        let b0 ← Ptr.index sb sx.toNat
847        let sx := sx + 1
848        let dist : UInt32 := b0.toUInt32 &&& 0xff
849        -- dist += (unsigned)(s->sym_buf[sx++] & 0xff) << 8;
850        let b1 ← Ptr.index sb sx.toNat
851        let sx := sx + 1
852        let dist := dist + ((b1.toUInt32 &&& 0xff) <<< 8)
853        -- lc = s->sym_buf[sx++];
854        let b2 ← Ptr.index sb sx.toNat
855        let sx := sx + 1
856        let lc := u8i b2
857        if dist == 0 then
858          send_code s lc.toInt ltree
859        else
860          -- code = _length_code[lc];
861          let code := (← Ptr.index lcp lc.toInt).toUInt32
862          -- send_code(s, code + LITERALS + 1, ltree);
863          send_code s (code + (i2u LITERALS) + 1).toNat ltree
864          -- extra = extra_lbits[code];
865          let extra ← Ptr.index (.ref .st_extra_lbits 0 : IPtr) code.toNat
866          let mut lc := lc
867          if extra != 0 then
868            lc ← isub lc (← Ptr.index (.ref .st_base_length 0 : IPtr) code.toNat)
869            send_bits s lc extra
870          -- dist--; code = d_code(dist);
871          let dist := dist - 1
872          let code := (← d_code dist).toUInt32
873          send_code s code.toNat dtree
874          let extra ← Ptr.index (.ref .st_extra_dbits 0 : IPtr) code.toNat
875          if extra != 0 then
876            let dist := dist - (i2u (← Ptr.index (.ref .st_base_dist 0 : IPtr) code.toNat))
877            send_bits s (u2i dist) extra
878        pure sx)
879      (fun sx => do pure (decide (sx < (← rd s).sym_next), sx))
880      0
881  -- send_code(s, END_BLOCK, ltree);
882  send_code s END_BLOCK.toInt ltree
883
884/-- `local int detect_data_type(deflate_state *s)` -/
885def detect_data_type (s : DeflateStatePtr) : M Int32 := do
886  -- unsigned long block_mask = 0xf3ffc07fUL;
887  -- for (n = 0; n <= 31; n++, block_mask >>= 1) if ((block_mask & 1) && ...Freq != 0) return Z_BINARY;
888  let (_, _, r) ← cwhile (σ := Int32 × UInt64 × Option Int32)
889    (fun (n, bm, r) => pure (r.isNone && decide (n.toInt ≤ 31), (n, bm, r)))
890    (fun (n, bm, _) => do
891      if (bm &&& 1) != 0 ∧ (← getFc (← pLtree s) n.toInt) != 0 then return (n, bm, some Z_BINARY)
892      pure (← iadd n 1, bm >>> 1, none))
893    (0, 0xf3ffc07f, none)
894  if let some v := r then return v
895  -- if (dyn_ltree[9].Freq != 0 || dyn_ltree[10].Freq != 0 || dyn_ltree[13].Freq != 0) return Z_TEXT;
896  if (← getFc (← pLtree s) 9) != 0 ∨ (← getFc (← pLtree s) 10) != 0 ∨ (← getFc (← pLtree s) 13) != 0 then
897    return Z_TEXT
898  -- for (n = 32; n < LITERALS; n++) if (s->dyn_ltree[n].Freq != 0) return Z_TEXT;
899  let (_, r) ← cwhile (σ := Int32 × Option Int32)
900    (fun (n, r) => pure (r.isNone && decide (n.toInt < LITERALS.toInt), (n, r)))
901    (fun (n, _) => do
902      if (← getFc (← pLtree s) n.toInt) != 0 then return (n, some Z_TEXT)
903      pure (← iadd n 1, none))
904    (32, none)
905  if let some v := r then return v
906  return Z_BINARY
907
908/-- `void ZLIB_INTERNAL _tr_flush_block(deflate_state *s, charf *buf, ulg stored_len, int last)` -/
909def «_tr_flush_block» (s : DeflateStatePtr) (buf : BPtr) (stored_len : UInt64) (last : Int32) : M Unit := do
910  -- int max_blindex = 0;
911  let mut max_blindex : Int32 := 0
912  let mut opt_lenb : UInt64 := 0
913  let mut static_lenb : UInt64 := 0
914  if (← rd s).level.toInt > 0 then
915    -- if (s->strm->data_type == Z_UNKNOWN) s->strm->data_type = detect_data_type(s);
916    let strm := (← rd s).strm
917    if (← ldZStream strm).data_type == Z_UNKNOWN then
918      let t ← detect_data_type s
919      stZStream strm { (← ldZStream strm) with data_type := t }
920    build_tree s (← pLdesc s)
921    build_tree s (← pDdesc s)
922    max_blindex ← build_bl_tree s
923    -- opt_lenb = (s->opt_len + 3 + 7) >> 3; static_lenb = (s->static_len + 3 + 7) >> 3;
924    opt_lenb := ((← rd s).opt_len + 3 + 7) >>> 3
925    static_lenb := ((← rd s).static_len + 3 + 7) >>> 3
926    -- if (static_lenb <= opt_lenb || s->strategy == Z_FIXED) opt_lenb = static_lenb;
927    if static_lenb ≤ opt_lenb ∨ (← rd s).strategy == Z_FIXED then opt_lenb := static_lenb
928  else
929    -- opt_lenb = static_lenb = stored_len + 5;
930    opt_lenb := stored_len + 5
931    static_lenb := stored_len + 5
932  if stored_len + 4 ≤ opt_lenb ∧ buf != .null then
933    «_tr_stored_block» s buf stored_len last
934  else if static_lenb == opt_lenb then
935    send_bits s (← iadd (STATIC_TREES <<< 1) last) 3
936    compress_block s (.ref .st_static_ltree 0) (.ref .st_static_dtree 0)
937  else
938    send_bits s (← iadd (DYN_TREES <<< 1) last) 3
939    send_all_trees s (← iadd (← rd s).l_desc.max_code 1) (← iadd (← rd s).d_desc.max_code 1)
940      (← iadd max_blindex 1)
941    compress_block s (← pLtree s) (← pDtree s)
942  init_block s
943  -- if (last) bi_windup(s);
944  if last != 0 then bi_windup s
945
946/-- `int ZLIB_INTERNAL _tr_tally(deflate_state *s, unsigned dist, unsigned lc)` -/
947def «_tr_tally» (s : DeflateStatePtr) (dist lc : UInt32) : M Int32 := do
948  -- s->sym_buf[s->sym_next++] = (uch)dist;  (uch)(dist >> 8);  (uch)lc;
949  let put (v : UInt8) : M Unit := do
950    let d ← rd s
951    setAt d.sym_buf d.sym_next.toNat v
952    md s fun d => { d with sym_next := d.sym_next + 1 }
953  put dist.toUInt8
954  put (dist >>> 8).toUInt8
955  put lc.toUInt8
956  if dist == 0 then
957    -- s->dyn_ltree[lc].Freq++;
958    let lt ← pLtree s
959    setFc lt lc.toNat ((← getFc lt lc.toNat) + 1)
960  else
961    md s fun d => { d with «matches» := d.«matches» + 1 }
962    let dist := dist - 1
963    -- s->dyn_ltree[_length_code[lc] + LITERALS + 1].Freq++;
964    let lcode ← Ptr.index (.ref .st_length_code 0 : BPtr) lc.toNat
965    let idx := (u8i lcode).toInt + LITERALS.toInt + 1
966    let lt ← pLtree s
967    setFc lt idx ((← getFc lt idx) + 1)
968    -- s->dyn_dtree[d_code(dist)].Freq++;
969    let dc ← d_code dist
970    let dt ← pDtree s
971    setFc dt dc.toNat ((← getFc dt dc.toNat) + 1)
972  -- return (s->sym_next == s->sym_end);
973  let d ← rd s
974  return (if d.sym_next == d.sym_end then 1 else 0)
975
976end Zlib.Trees