inflate.c.lean

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

1import ZlibF.Runtime.Alloc
2import ZlibF.Runtime.Tables
3import ZlibF.Zlib.«adler32.c»
4import ZlibF.Zlib.«inftrees.c»
5import ZlibF.Zlib.«zutil.c»
6import ZlibF.Zlib.«crc32.c»
7import ZlibF.Zlib.«inffast.c»
8
9/-!
10# inflate.c — faithful translation
11
12Source: `inflate.c` of the verified source (`zlib/` plus `patches/*.patch`; there is no `ub.patch` yet), default x86_64
13Linux build: `GUNZIP` defined, `Z_SOLO`, `PKZIP_BUG_WORKAROUND`, `INFLATE_STRICT`,
14`INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR`, `ZLIB_DEBUG` undefined (so `Tracev` is nothing and `dmax` is written but
15never read). Types as in `docs/design/translation.md`. The notes are `docs/proof/inflate.md`.
16
17## How the control flow is translated
18
19* `inflate()` keeps its registers (`next put have left hold bits in out`) and its other locals (`copy from here last len
20  ret`) in the record `IL`. A mode of the `switch` is one `def` (`inflate_HEAD`, ...) of the monad `X`, which is the
21  state monad on `IL` over the runtime monad `M` with an exception: `X α = ExceptT Ex (StateT IL M) α`.
22  * a mode that ends with `break` just returns;
23  * `goto inf_leave` is `throw Ex.leave` (the registers at that moment are kept: the state is not rolled back);
24  * `return v` is `throw (Ex.ret v)`;
25  * a fall-through is a tail call of the next mode (`TYPE` calls `TYPEDO` without writing the mode field);
26  * the macros are `def`s of `X` (`PULLBYTE`, `NEEDBITS`, `BITS`, ...), so a `goto` inside a macro is a `throw`.
27* Loops are the runtime's `cwhile` (through `xwhileBrk`, which carries the registers and the exit reason in the loop
28  state). `break` out of a `while` or `for (;;)` is the Boolean the body returns.
29* The next mode is read from the heap field `state->mode` on every trip of `for (;;)`, as in C.
30
31## Decisions (see the report with this file)
32
33* A pointer to a scalar field (`&state->next`, `&state->lenbits`, `&state->have`, `uInt *dictLength`) is passed as the
34  value in and returned as the value out.
35* `unsigned char hbuf[4]` and `unsigned char buf[4]` are byte blocks made at the declaration (`allocLocalB`, which never
36  fails; it uses the runtime's `allocBytes`) and freed before every return.
37* The local variables of `inflate()` that the C leaves uninitialised (`copy len from here last`) start as `0`, `NULL`,
38  `{0,0,0}`: an arbitrary value, as the guide allows; `from` starts null so that a use before assignment faults.
39* Only the default allocator is modelled (`zcalloc`/`zcfree` stored in the stream); another `zalloc`/`zfree` that the
40  code would call is `ub "custom allocator not modelled"`.
41* The cast of `strm->state` to `struct inflate_state *` faults if the state is a `deflate_state` (the C reads through
42  the wrong type, which is formally undefined).
43* `inflateCopy` compares `state->lencode` with `state->codes` with `>=` and `<=`, as the source does (no `ub.patch`).
44  Pointers into two different arrays are not comparable, so the comparison faults when `lencode` points to the static
45  `lenfix` (a stream stopped inside a fixed block): this is the real undefined behaviour of the source.
46* Error messages are string literals: `strm->msg` points to a fresh read-only block (`Zlib.Zutil.strLit`).
47-/
48
49namespace Zlib.Inflate
50open C
51open Zlib.Crc32 (crc32)
52open Zlib.Inffast (inflate_fast)
53open Zlib.Inftrees (inflate_table inflate_fixed)
54open Zlib.Adler32 (adler32)
55
56/-! ## Arithmetic with the checks of the C -/
57
58/-- `x << n` for `unsigned x`: faults if `n >= 32` (the count is out of range). -/
59def shl32 (x n : UInt32) : M UInt32 := if n < 32 then pure (x <<< n) else ub "shift count out of range"
60/-- `x >> n` for `unsigned x`. -/
61def shr32 (x n : UInt32) : M UInt32 := if n < 32 then pure (x >>> n) else ub "shift count out of range"
62/-- `x << n` for `unsigned long x`: faults if `n >= 64`. -/
63def shl64 (x : UInt64) (n : UInt32) : M UInt64 := if n < 64 then pure (x <<< n.toUInt64) else ub "shift count out of range"
64/-- `x >> n` for `unsigned long x`. -/
65def shr64 (x : UInt64) (n : UInt32) : M UInt64 := if n < 64 then pure (x >>> n.toUInt64) else ub "shift count out of range"
66/-- An `int` result: faults on signed overflow. -/
67def chkI32 (v : Int) : M Int32 :=
68  if -2147483648 ≤ v ∧ v < 2147483648 then pure (Int32.ofInt v) else ub "signed integer overflow"
69/-- A `long` result: faults on signed overflow. -/
70def chkI64 (v : Int) : M Int64 :=
71  if -9223372036854775808 ≤ v ∧ v < 9223372036854775808 then pure (Int64.ofInt v) else ub "signed integer overflow"
72/-- `(int)u` for `unsigned u` (modulo 2^32). -/
73def u2i (x : UInt32) : Int32 := Int32.ofInt (x.toNat : Int)
74/-- `(unsigned)i` for `int i`. -/
75def i2u (x : Int32) : UInt32 := x.toUInt32
76/-- `(unsigned long)i` for `int i` (sign extension, then modulo 2^64). -/
77def i2ul (x : Int32) : UInt64 := x.toInt64.toUInt64
78
79/-! ## The default allocator through the stream (`ZALLOC`, `ZFREE`) -/
80
81/-- `ZALLOC(strm, items, size)` for a byte block: calls `strm->zalloc`. Only `zcalloc` is modelled. -/
82def ZALLOCB (strm : ZStreamPtr) (items size : UInt32) : M BPtr := do
83  let z ← ldZStream strm
84  match z.zalloc with
85  | .fn "zcalloc" => Zlib.Zutil.zcalloc z.«opaque» items size
86  | _ => ub "custom allocator not modelled"
87
88/-- `ZALLOC(strm, 1, sizeof(struct inflate_state))`: uninitialised record (arbitrary integers, null pointers). -/
89def ZALLOCS (strm : ZStreamPtr) : M InflateStatePtr := do
90  let z ← ldZStream strm
91  match z.zalloc with
92  | .fn "zcalloc" => allocInflateState
93  | _ => ub "custom allocator not modelled"
94
95/-- `ZFREE(strm, addr)` for a byte block. -/
96def ZFREEB (strm : ZStreamPtr) (p : BPtr) : M Unit := do
97  let z ← ldZStream strm
98  match z.zfree with
99  | .fn "zcfree" => Zlib.Zutil.zcfree z.«opaque» p
100  | _ => ub "custom allocator not modelled"
101
102/-- `ZFREE(strm, state)` for an inflate state. -/
103def ZFREES (strm : ZStreamPtr) (st : InflateStatePtr) : M Unit := do
104  let z ← ldZStream strm
105  match z.zfree with
106  | .fn "zcfree" => freeInflateState st
107  | _ => ub "custom allocator not modelled"
108
109/-- A local array (`unsigned char hbuf[4]`): a writable block made at the declaration, with arbitrary content. It takes
110no allocation call of the failure oracle (a local cannot fail to exist); it uses the runtime's block allocator. -/
111def allocLocalB (n : Nat) : M BPtr := fun h =>
112  allocBytes (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val)) h
113
114/-- `strm->msg = (z_const char *)"..."`. -/
115def setMsg (strm : ZStreamPtr) (s : String) : M Unit := do
116  let p ← Zlib.Zutil.strLit s
117  let z ← ldZStream strm
118  stZStream strm { z with msg := p }
119
120/-! ## Access to the state and the stream -/
121
122/-- Read a field of `*st`. -/
123def rdS {α : Type} (st : InflateStatePtr) (f : InflateState → α) : M α := do return f (← ldInflateState st)
124/-- Update fields of `*st`. -/
125def wrS (st : InflateStatePtr) (f : InflateState → InflateState) : M Unit := do
126  let s ← ldInflateState st
127  stInflateState st (f s)
128/-- Read a field of `*strm`. -/
129def rdZ {α : Type} (strm : ZStreamPtr) (f : ZStream → α) : M α := do return f (← ldZStream strm)
130/-- Update fields of `*strm`. -/
131def wrZ (strm : ZStreamPtr) (f : ZStream → ZStream) : M Unit := do
132  let z ← ldZStream strm
133  stZStream strm (f z)
134
135/-- `state->lens` (a pointer to element 0 of the array field). -/
136def lensP (st : InflateStatePtr) : WPtr := match st with | some (.tab i) => .ref (.istate_lens i) 0 | none => .null
137/-- `state->work`. -/
138def workP (st : InflateStatePtr) : WPtr := match st with | some (.tab i) => .ref (.istate_work i) 0 | none => .null
139/-- `state->codes`. -/
140def codesP (st : InflateStatePtr) : CodePtr := match st with | some (.tab i) => .ref (.istate_codes i) 0 | none => .null
141
142/-- `static const unsigned short order[19]` -/
143def order : Array UInt16 := #[16, 17, 18, 0, 8, 7, 9, 6, 10, 5, 11, 4, 12, 3, 13, 2, 14, 1, 15]
144/-- `order[i]`: faults outside the array. -/
145def orderAt (i : UInt32) : M UInt16 :=
146  match order[i.toNat]? with
147  | some v => pure v
148  | none => ub "order index outside its array"
149
150/-! ## `inflateStateCheck` .. `inflatePrime` -/
151
152/-- `local int inflateStateCheck(z_streamp strm)` -/
153def inflateStateCheck (strm : ZStreamPtr) : M Int32 := do
154  -- if (strm == Z_NULL || strm->zalloc == (alloc_func)0 || strm->zfree == (free_func)0) return 1;
155  if strm == none then return 1
156  let z ← ldZStream strm
157  if z.zalloc == .null || z.zfree == .null then return 1
158  -- state = (struct inflate_state FAR *)strm->state;
159  let state ← castInflateState z.state
160  -- if (state == Z_NULL || state->strm != strm || state->mode < HEAD || state->mode > SYNC) return 1;
161  if state == none then return 1
162  let s ← ldInflateState state
163  if s.strm != strm || s.mode < HEAD || s.mode > SYNC then return 1
164  return 0
165
166/-- `int ZEXPORT inflateResetKeep(z_streamp strm)` -/
167def inflateResetKeep (strm : ZStreamPtr) : M Int32 := do
168  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
169  let z ← ldZStream strm
170  let state ← castInflateState z.state
171  -- strm->total_in = strm->total_out = state->total = 0;
172  wrS state fun s => { s with total := 0 }
173  -- strm->msg = Z_NULL; strm->data_type = 0;
174  wrZ strm fun z => { z with total_out := 0, total_in := 0, msg := .null, data_type := 0 }
175  -- if (state->wrap) strm->adler = state->wrap & 1;
176  let s ← ldInflateState state
177  if s.wrap != 0 then wrZ strm fun z => { z with adler := i2ul (s.wrap &&& 1) }
178  -- state->mode = HEAD; last = 0; havedict = 0; flags = -1; dmax = 32768U; head = Z_NULL; hold = 0; bits = 0;
179  -- state->lencode = state->distcode = state->next = state->codes;
180  -- state->sane = 1; state->back = -1;
181  wrS state fun s => { s with
182    mode := HEAD, last := 0, havedict := 0, flags := -1, dmax := 32768, head := none,
183    hold := 0, bits := 0, next := codesP state, distcode := codesP state, lencode := codesP state, sane := 1, back := -1 }
184  return Z_OK
185
186/-- `int ZEXPORT inflateReset(z_streamp strm)` -/
187def inflateReset (strm : ZStreamPtr) : M Int32 := do
188  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
189  let z ← ldZStream strm
190  let state ← castInflateState z.state
191  let s ← ldInflateState state
192  -- if (state->wbits != state->reqbits) { if (state->window != Z_NULL) { ZFREE; window = Z_NULL; } wbits = reqbits; }
193  if s.wbits != s.reqbits then
194    if s.window != .null then
195      ZFREEB strm s.window
196      wrS state fun s => { s with window := .null }
197    wrS state fun s => { s with wbits := s.reqbits }
198  -- state->wrap = state->reqwrap; wsize = 0; whave = 0; wnext = 0;
199  wrS state fun s => { s with wrap := s.reqwrap, wsize := 0, whave := 0, wnext := 0 }
200  return (← inflateResetKeep strm)
201
202/-- `int ZEXPORT inflateReset2(z_streamp strm, int windowBits)` -/
203def inflateReset2 (strm : ZStreamPtr) (windowBits : Int32) : M Int32 := do
204  -- if (inflateStateCheck(strm)) return Z_STREAM_ERROR;
205  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
206  let z ← ldZStream strm
207  let state ← castInflateState z.state
208  let mut windowBits := windowBits
209  let mut wrap : Int32 := 0
210  -- if (windowBits < 0) { if (windowBits < -15) return Z_STREAM_ERROR; wrap = 0; windowBits = -windowBits; }
211  if windowBits < 0 then
212    if windowBits < -15 then return Z_STREAM_ERROR
213    wrap := 0
214    windowBits ← chkI32 (-(windowBits.toInt))
215  else
216    -- wrap = (windowBits >> 4) + 5;
217    wrap ← chkI32 ((windowBits >>> 4).toInt + 5)
218    -- if (windowBits < 48) windowBits &= 15;
219    if windowBits < 48 then windowBits := windowBits &&& 15
220  -- if (windowBits && (windowBits < 8 || windowBits > 15)) return Z_STREAM_ERROR;
221  if windowBits != 0 && (windowBits < 8 || windowBits > 15) then return Z_STREAM_ERROR
222  -- if (state->window != Z_NULL && state->wbits != (unsigned)windowBits) { ZFREE; window = Z_NULL; }
223  let s ← ldInflateState state
224  if s.window != .null && s.wbits != i2u windowBits then
225    ZFREEB strm s.window
226    wrS state fun s => { s with window := .null }
227  -- state->reqwrap = state->wrap = wrap; state->reqbits = state->wbits = (unsigned)windowBits;
228  wrS state fun s => { s with wrap := wrap, reqwrap := wrap, wbits := i2u windowBits, reqbits := i2u windowBits }
229  return (← inflateReset strm)
230
231/-- `int ZEXPORT inflateInit2_(z_streamp strm, int windowBits, const char *version, int stream_size)`
232(`version` is a pointer to a NUL-terminated string; `sizeof(z_stream)` is 112) -/
233def inflateInit2_ (strm : ZStreamPtr) (windowBits : Int32) (version : BPtr) (stream_size : Int32) : M Int32 := do
234  -- if (version == Z_NULL || version[0] != ZLIB_VERSION[0] || stream_size != (int)(sizeof(z_stream))) return Z_VERSION_ERROR;
235  if version == .null then return Z_VERSION_ERROR
236  if (← index8 version 0) != 49 then return Z_VERSION_ERROR
237  if stream_size != 112 then return Z_VERSION_ERROR
238  -- if (strm == Z_NULL) return Z_STREAM_ERROR;
239  if strm == none then return Z_STREAM_ERROR
240  -- strm->msg = Z_NULL;
241  wrZ strm fun z => { z with msg := .null }
242  -- if (strm->zalloc == (alloc_func)0) { strm->zalloc = zcalloc; strm->opaque = (voidpf)0; }
243  if (← rdZ strm (·.zalloc)) == .null then
244    wrZ strm fun z => { z with zalloc := .fn "zcalloc", «opaque» := .null }
245  -- if (strm->zfree == (free_func)0) strm->zfree = zcfree;
246  if (← rdZ strm (·.zfree)) == .null then
247    wrZ strm fun z => { z with zfree := .fn "zcfree" }
248  -- state = (struct inflate_state FAR *)ZALLOC(strm, 1, sizeof(struct inflate_state));
249  let state ← ZALLOCS strm
250  -- if (state == Z_NULL) return Z_MEM_ERROR;
251  if state == none then return Z_MEM_ERROR
252  -- zmemzero(state, sizeof(struct inflate_state));
253  stInflateState state (InflateState.zeroed)
254  -- strm->state = (struct internal_state FAR *)state;
255  wrZ strm fun z => { z with state := StateRef.ofInflateState state }
256  -- state->strm = strm; state->window = Z_NULL; state->mode = HEAD;
257  wrS state fun s => { s with strm := strm, window := .null, mode := HEAD }
258  -- ret = inflateReset2(strm, windowBits);
259  let ret ← inflateReset2 strm windowBits
260  -- if (ret != Z_OK) { ZFREE(strm, state); strm->state = Z_NULL; }
261  if ret != Z_OK then
262    ZFREES strm state
263    wrZ strm fun z => { z with state := none }
264  return ret
265
266/-- `int ZEXPORT inflateInit_(z_streamp strm, const char *version, int stream_size)` -/
267def inflateInit_ (strm : ZStreamPtr) (version : BPtr) (stream_size : Int32) : M Int32 :=
268  inflateInit2_ strm DEF_WBITS version stream_size
269
270/-- `int ZEXPORT inflatePrime(z_streamp strm, int bits, int value)` -/
271def inflatePrime (strm : ZStreamPtr) (bits : Int32) (value : Int32) : M Int32 := do
272  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
273  -- if (bits == 0) return Z_OK;
274  if bits == 0 then return Z_OK
275  let z ← ldZStream strm
276  let state ← castInflateState z.state
277  -- if (bits < 0) { state->hold = 0; state->bits = 0; return Z_OK; }
278  if bits < 0 then
279    wrS state fun s => { s with hold := 0, bits := 0 }
280    return Z_OK
281  -- if (bits > 16 || state->bits + (uInt)bits > 32) return Z_STREAM_ERROR;
282  let s ← ldInflateState state
283  if bits > 16 || s.bits + i2u bits > 32 then return Z_STREAM_ERROR
284  -- value &= (1L << bits) - 1;   (`long` arithmetic; bits is in 1..16)
285  let m : Int64 := ((1 : Int64) <<< bits.toInt64) - 1
286  let value : Int32 := (value.toInt64 &&& m).toInt32
287  -- state->hold += (unsigned long)value << state->bits;
288  let sh ← shl64 (i2ul value) s.bits
289  -- state->bits += (uInt)bits;
290  wrS state fun s => { s with hold := s.hold + sh, bits := s.bits + i2u bits }
291  return Z_OK
292
293/-- `local int updatewindow(z_streamp strm, const Bytef *end, unsigned copy)` -/
294def updatewindow (strm : ZStreamPtr) (end_ : BPtr) (copy : UInt32) : M Int32 := do
295  let z ← ldZStream strm
296  let state ← castInflateState z.state
297  let s ← ldInflateState state
298  -- if (state->window == Z_NULL) { state->window = ZALLOC(strm, 1U << state->wbits, sizeof(unsigned char)); if (...== Z_NULL) return 1; }
299  if s.window == .null then
300    let w ← ZALLOCB strm (← shl32 1 s.wbits) 1
301    wrS state fun s => { s with window := w }
302    if w == .null then return 1
303  -- if (state->wsize == 0) { state->wsize = 1U << state->wbits; state->wnext = 0; state->whave = 0; }
304  let s ← ldInflateState state
305  if s.wsize == 0 then
306    let ws ← shl32 1 s.wbits
307    wrS state fun s => { s with wsize := ws, wnext := 0, whave := 0 }
308  let s ← ldInflateState state
309  if copy >= s.wsize then
310    -- zmemcpy(state->window, end - state->wsize, state->wsize); wnext = 0; whave = wsize;
311    memcpyB s.window (← end_.add (-(s.wsize.toNat : Int))) s.wsize.toNat
312    wrS state fun s => { s with wnext := 0, whave := s.wsize }
313  else
314    -- dist = state->wsize - state->wnext; if (dist > copy) dist = copy;
315    let mut dist := s.wsize - s.wnext
316    if dist > copy then dist := copy
317    -- zmemcpy(state->window + state->wnext, end - copy, dist);
318    memcpyB (← s.window.add (s.wnext.toNat : Int)) (← end_.add (-(copy.toNat : Int))) dist.toNat
319    -- copy -= dist;
320    let copy := copy - dist
321    if copy != 0 then
322      -- zmemcpy(state->window, end - copy, copy); state->wnext = copy; state->whave = state->wsize;
323      memcpyB s.window (← end_.add (-(copy.toNat : Int))) copy.toNat
324      wrS state fun s => { s with wnext := copy, whave := s.wsize }
325    else
326      -- state->wnext += dist; if (state->wnext == state->wsize) state->wnext = 0; if (state->whave < state->wsize) state->whave += dist;
327      let mut wnext := s.wnext + dist
328      if wnext == s.wsize then wnext := 0
329      let mut whave := s.whave
330      if whave < s.wsize then whave := whave + dist
331      wrS state fun s => { s with wnext := wnext, whave := whave }
332  return 0
333
334/-! ## The registers of `inflate()` and the monad of its modes -/
335
336/-- How a mode leaves other than by `break`: `goto inf_leave`, or `return v`. -/
337inductive Ex where
338  | leave
339  | ret (v : Int32)
340
341/-- The locals of `inflate()` (and of `inflateBack()`): `next put have left hold bits in out copy from here last len
342ret`. `have` and `in` are keywords, so `have_` and `in_`; `out` is `out_` for symmetry. -/
343structure IL where
344  next : BPtr
345  put : BPtr
346  have_ : UInt32
347  left : UInt32
348  hold : UInt64
349  bits : UInt32
350  in_ : UInt32
351  out_ : UInt32
352  copy : UInt32
353  from_ : BPtr
354  here : Code
355  last : Code
356  len : UInt32
357  ret : Int32
358
359/-- The registers before the first assignment (the C leaves these uninitialised; see the file comment). -/
360def IL.init : IL where
361  next := .null
362  put := .null
363  have_ := 0
364  left := 0
365  hold := 0
366  bits := 0
367  in_ := 0
368  out_ := 0
369  copy := 0
370  from_ := .null
371  here := default
372  last := default
373  len := 0
374  ret := 0
375
376/-- The monad of a mode: the registers, `goto inf_leave` / `return` as an exception, and the heap. -/
377abbrev X := ExceptT Ex (StateT IL M)
378
379/-- Why a loop of `X` ended. -/
380inductive Stop where
381  | go
382  | brk
383  | ex (e : Ex)
384
385/-- `while (cond) body` where `body` returns `true` for `break`. Built on the runtime's `cwhile`; the registers and the
386reason for stopping are the loop-carried state, so a `goto` or `return` inside leaves with the registers it had. -/
387def xwhileBrk (cond : X Bool) (body : X Bool) : X Unit :=
388  ExceptT.mk (fun l0 => do
389    let r ← cwhile (σ := IL × Stop)
390      (fun (l, s) => match s with
391        | .go => do
392          let (r, l') ← StateT.run (ExceptT.run cond) l
393          pure (match r with
394            | .ok b => (b, (l', Stop.go))
395            | .error e => (false, (l', Stop.ex e)))
396        | s => pure (false, (l, s)))
397      (fun (l, _) => do
398        let (r, l') ← StateT.run (ExceptT.run body) l
399        pure (match r with
400          | .ok b => (l', if b then Stop.brk else Stop.go)
401          | .error e => (l', Stop.ex e)))
402      (l0, Stop.go)
403    let (l, s) := r
404    pure (match s with
405      | .ex e => (Except.error e, l)
406      | _ => (Except.ok (), l)))
407
408/-- `while (cond) body` -/
409def xwhile (cond : X Bool) (body : X Unit) : X Unit := xwhileBrk cond (do body; pure false)
410
411/-- `do body while (cond)` -/
412def xdoWhile (body : X Unit) (cond : X Bool) : X Unit := do
413  body
414  xwhile cond body
415
416/-- `for (;;) body` where `body` returns `true` for `break`. -/
417def xloopBrk (body : X Bool) : X Unit := xwhileBrk (pure true) body
418
419/-- The information `inflate()` and its macros share. -/
420structure Ctx where
421  strm : ZStreamPtr
422  st : InflateStatePtr
423  hbuf : BPtr
424  flush : Int32
425
426/-! ## The macros of `inflate.c`, each one a `def` -/
427
428/-- `LOAD()` -/
429def LOAD (strm : ZStreamPtr) (st : InflateStatePtr) : X Unit := do
430  let z ← ldZStream strm
431  let s ← ldInflateState st
432  modify fun l => { l with
433    put := z.next_out, left := z.avail_out, next := z.next_in, have_ := z.avail_in,
434    hold := s.hold, bits := s.bits }
435
436/-- `RESTORE()` -/
437def RESTORE (strm : ZStreamPtr) (st : InflateStatePtr) : X Unit := do
438  let l ← get
439  wrZ strm fun z => { z with next_out := l.put, avail_out := l.left, next_in := l.next, avail_in := l.have_ }
440  wrS st fun s => { s with hold := l.hold, bits := l.bits }
441
442/-- `INITBITS()` -/
443def INITBITS : X Unit := modify fun l => { l with hold := 0, bits := 0 }
444
445/-- `PULLBYTE()`: `goto inf_leave` if there is no input. -/
446def PULLBYTE : X Unit := do
447  let l ← get
448  if l.have_ == 0 then throw Ex.leave
449  -- have--;
450  set { l with have_ := l.have_ - 1 }
451  -- hold += (unsigned long)(*next++) << bits; bits += 8;
452  let b ← load8 l.next
453  let nx ← l.next.add 1
454  let sh ← shl64 b.toUInt64 l.bits
455  set { l with have_ := l.have_ - 1, next := nx, hold := l.hold + sh, bits := l.bits + 8 }
456
457/-- `NEEDBITS(n)`: `while (bits < (unsigned)(n)) PULLBYTE();` -/
458def NEEDBITS (n : UInt32) : X Unit :=
459  xwhile (do return (← get).bits < n) PULLBYTE
460
461/-- `BITS(n)`: `((unsigned)hold & ((1U << (n)) - 1))` -/
462def BITS (n : UInt32) : X UInt32 := do
463  let l ← get
464  let m ← shl32 1 n
465  return l.hold.toUInt32 &&& (m - 1)
466
467/-- `DROPBITS(n)`: `hold >>= (n); bits -= (unsigned)(n);` -/
468def DROPBITS (n : UInt32) : X Unit := do
469  let l ← get
470  let h ← shr64 l.hold n
471  set { l with hold := h, bits := l.bits - n }
472
473/-- `BYTEBITS()`: `hold >>= bits & 7; bits -= bits & 7;` -/
474def BYTEBITS : X Unit := do
475  let l ← get
476  let h ← shr64 l.hold (l.bits &&& 7)
477  set { l with hold := h, bits := l.bits - (l.bits &&& 7) }
478
479/-- `ZSWAP32(q)` -/
480def ZSWAP32 (q : UInt64) : UInt64 :=
481  ((q >>> 24) &&& (0xff : UInt64)) + ((q >>> 8) &&& (0xff00 : UInt64)) + ((q &&& (0xff00 : UInt64)) <<< 8) + ((q &&& (0xff : UInt64)) <<< 24)
482
483/-- `UPDATE_CHECK(check, buf, len)`: `(state->flags ? crc32(check, buf, len) : adler32(check, buf, len))` -/
484def UPDATE_CHECK (st : InflateStatePtr) (check : UInt64) (buf : BPtr) (len : UInt32) : M UInt64 := do
485  if (← rdS st (·.flags)) != 0 then crc32 check buf len else adler32 check buf len
486
487/-- `CRC2(state->check, hold)` -/
488def CRC2 (c : Ctx) : X Unit := do
489  let l ← get
490  -- hbuf[0] = (unsigned char)(word); hbuf[1] = (unsigned char)((word) >> 8);
491  store8 c.hbuf l.hold.toUInt8
492  store8 (← c.hbuf.add 1) (l.hold >>> 8).toUInt8
493  -- check = crc32(check, hbuf, 2);
494  let ck ← rdS c.st (·.check)
495  let v ← crc32 ck c.hbuf 2
496  wrS c.st fun s => { s with check := v }
497
498/-- `CRC4(state->check, hold)` -/
499def CRC4 (c : Ctx) : X Unit := do
500  let l ← get
501  store8 c.hbuf l.hold.toUInt8
502  store8 (← c.hbuf.add 1) (l.hold >>> 8).toUInt8
503  store8 (← c.hbuf.add 2) (l.hold >>> 16).toUInt8
504  store8 (← c.hbuf.add 3) (l.hold >>> 24).toUInt8
505  let ck ← rdS c.st (·.check)
506  let v ← crc32 ck c.hbuf 4
507  wrS c.st fun s => { s with check := v }
508
509/-- `(state->flags & 0x0200) && (state->wrap & 4)` -/
510def hcrcOn (st : InflateStatePtr) : M Bool := do
511  let s ← ldInflateState st
512  return (s.flags &&& 0x0200) != 0 && (s.wrap &&& 4) != 0
513
514/-- `state->mode = m;` -/
515def setMode (st : InflateStatePtr) (m : UInt32) : M Unit := wrS st fun s => { s with mode := m }
516
517/-- `strm->msg = "..."; state->mode = BAD;` -/
518def badMode (c : Ctx) (msg : String) : M Unit := do
519  setMsg c.strm msg
520  setMode c.st BAD
521
522/-! ## The modes of `inflate()`, from the last to the first (a fall-through is a tail call) -/
523
524/-- `case DONE:` -/
525def inflate_DONE (_c : Ctx) : X Unit := do
526  -- ret = Z_STREAM_END; goto inf_leave;
527  modify fun l => { l with ret := Z_STREAM_END }
528  throw Ex.leave
529
530/-- `case LENGTH:` -/
531def inflate_LENGTH (c : Ctx) : X Unit := do
532  -- if (state->wrap && state->flags) {
533  let s ← ldInflateState c.st
534  if s.wrap != 0 && s.flags != 0 then
535    NEEDBITS 32
536    -- if ((state->wrap & 4) && hold != (state->total & 0xffffffff)) { ...BAD; break; }
537    let s ← ldInflateState c.st
538    let l ← get
539    if (s.wrap &&& 4) != 0 && l.hold != (s.total &&& 0xffffffff) then
540      badMode c "incorrect length check"
541      return
542    INITBITS
543  -- state->mode = DONE; /* fallthrough */
544  setMode c.st DONE
545  inflate_DONE c
546
547/-- `case CHECK:` -/
548def inflate_CHECK (c : Ctx) : X Unit := do
549  let s ← ldInflateState c.st
550  -- if (state->wrap) {
551  if s.wrap != 0 then
552    NEEDBITS 32
553    -- out -= left;
554    modify fun l => { l with out_ := l.out_ - l.left }
555    let l ← get
556    -- strm->total_out += out; state->total += out;
557    wrZ c.strm fun z => { z with total_out := z.total_out + l.out_.toUInt64 }
558    wrS c.st fun s => { s with total := s.total + l.out_.toUInt64 }
559    -- if ((state->wrap & 4) && out) strm->adler = state->check = UPDATE_CHECK(state->check, put - out, out);
560    let s ← ldInflateState c.st
561    if (s.wrap &&& 4) != 0 && l.out_ != 0 then
562      let p ← l.put.add (-(l.out_.toNat : Int))
563      let v ← UPDATE_CHECK c.st s.check p l.out_
564      wrS c.st fun s => { s with check := v }
565      wrZ c.strm fun z => { z with adler := v }
566    -- out = left;
567    modify fun l => { l with out_ := l.left }
568    -- if ((state->wrap & 4) && ((state->flags ? hold : ZSWAP32(hold)) != state->check)) { ...BAD; break; }
569    let s ← ldInflateState c.st
570    let l ← get
571    if (s.wrap &&& 4) != 0 && (if s.flags != 0 then l.hold else ZSWAP32 l.hold) != s.check then
572      badMode c "incorrect data check"
573      return
574    INITBITS
575  -- state->mode = LENGTH; /* fallthrough */
576  setMode c.st LENGTH
577  inflate_LENGTH c
578
579/-- `case LIT:` -/
580def inflate_LIT (c : Ctx) : X Unit := do
581  let l ← get
582  -- if (left == 0) goto inf_leave;
583  if l.left == 0 then throw Ex.leave
584  -- *put++ = (unsigned char)(state->length);
585  let s ← ldInflateState c.st
586  store8 l.put s.length.toUInt8
587  let p ← l.put.add 1
588  -- left--; state->mode = LEN;
589  set { l with put := p, left := l.left - 1 }
590  setMode c.st LEN
591
592/-- `case MATCH:` -/
593def inflate_MATCH (c : Ctx) : X Unit := do
594  let l ← get
595  -- if (left == 0) goto inf_leave;
596  if l.left == 0 then throw Ex.leave
597  -- copy = out - left;
598  let mut copy := l.out_ - l.left
599  let mut from_ : BPtr := l.from_
600  let s ← ldInflateState c.st
601  -- if (state->offset > copy) { /* copy from window */
602  if s.offset > copy then
603    -- copy = state->offset - copy;
604    copy := s.offset - copy
605    -- if (copy > state->whave) { if (state->sane) { ...BAD; break; } }
606    if copy > s.whave then
607      if s.sane != 0 then
608        badMode c "invalid distance too far back"
609        return
610    -- if (copy > state->wnext) { copy -= state->wnext; from = state->window + (state->wsize - copy); }
611    if copy > s.wnext then
612      copy := copy - s.wnext
613      from_ ← s.window.add ((s.wsize - copy).toNat : Int)
614    else
615      -- else from = state->window + (state->wnext - copy);
616      from_ ← s.window.add ((s.wnext - copy).toNat : Int)
617    -- if (copy > state->length) copy = state->length;
618    if copy > s.length then copy := s.length
619  else
620    -- from = put - state->offset; copy = state->length;
621    from_ ← l.put.add (-(s.offset.toNat : Int))
622    copy := s.length
623  -- if (copy > left) copy = left;
624  if copy > l.left then copy := l.left
625  -- left -= copy; state->length -= copy;
626  set { l with left := l.left - copy, copy := copy, from_ := from_ }
627  wrS c.st fun s => { s with length := s.length - copy }
628  -- do { *put++ = *from++; } while (--copy);
629  xdoWhile
630    (do
631      let l ← get
632      let b ← load8 l.from_
633      store8 l.put b
634      let p ← l.put.add 1
635      let f ← l.from_.add 1
636      set { l with put := p, from_ := f })
637    (do
638      let l ← get
639      let n := l.copy - 1
640      set { l with copy := n }
641      return n != 0)
642  -- if (state->length == 0) state->mode = LEN;
643  if (← rdS c.st (·.length)) == 0 then setMode c.st LEN
644
645/-- The bit-extraction part shared in spirit by `LENEXT` and `DISTEXT`: `if (state->extra) { NEEDBITS(state->extra); ...}`.
646`case DISTEXT:` -/
647def inflate_DISTEXT (c : Ctx) : X Unit := do
648  let s ← ldInflateState c.st
649  -- if (state->extra) {
650  if s.extra != 0 then
651    NEEDBITS s.extra
652    -- state->offset += BITS(state->extra);
653    let b ← BITS s.extra
654    wrS c.st fun s => { s with offset := s.offset + b }
655    -- DROPBITS(state->extra);
656    DROPBITS s.extra
657    -- state->back += state->extra;   (`int += unsigned`: computed in unsigned, converted back)
658    wrS c.st fun s => { s with back := u2i (i2u s.back + s.extra) }
659  -- state->mode = MATCH; /* fallthrough */
660  setMode c.st MATCH
661  inflate_MATCH c
662
663/-- The two-level table lookup `for (;;) { here = TABLE[BITS(bitsOfTable)]; if ((unsigned)(here.bits) <= bits) break; PULLBYTE(); }`.
664`dist` selects `distcode`/`distbits`, else `lencode`/`lenbits`. -/
665def lookup1 (c : Ctx) (dist : Bool) : X Unit :=
666  xloopBrk (do
667    let s ← ldInflateState c.st
668    let tab := if dist then s.distcode else s.lencode
669    let nb := if dist then s.distbits else s.lenbits
670    let b ← BITS nb
671    let here ← Ptr.index tab (b.toNat : Int)
672    modify fun l => { l with here := here }
673    if here.bits.toUInt32 <= (← get).bits then return true
674    PULLBYTE
675    return false)
676
677/-- `for (;;) { here = TABLE[last.val + (BITS(last.bits + last.op) >> last.bits)]; if ((unsigned)(last.bits + here.bits) <= bits) break; PULLBYTE(); }` -/
678def lookup2 (c : Ctx) (dist : Bool) : X Unit :=
679  xloopBrk (do
680    let s ← ldInflateState c.st
681    let tab := if dist then s.distcode else s.lencode
682    let last := (← get).last
683    let b ← BITS (last.bits.toUInt32 + last.op.toUInt32)
684    let sh ← shr32 b last.bits.toUInt32
685    let here ← Ptr.index tab ((last.val.toUInt32 + sh).toNat : Int)
686    modify fun l => { l with here := here }
687    if (last.bits.toUInt32 + here.bits.toUInt32) <= (← get).bits then return true
688    PULLBYTE
689    return false)
690
691/-- `case DIST:` -/
692def inflate_DIST (c : Ctx) : X Unit := do
693  lookup1 c true
694  let here := (← get).here
695  -- if ((here.op & 0xf0) == 0) {
696  if (here.op &&& 0xf0) == 0 then
697    modify fun l => { l with last := here }
698    lookup2 c true
699    let last := (← get).last
700    DROPBITS last.bits.toUInt32
701    let s ← ldInflateState c.st
702    let bk ← chkI32 (s.back.toInt + last.bits.toNat)
703    wrS c.st fun s => { s with back := bk }
704  -- DROPBITS(here.bits); state->back += here.bits;
705  let here := (← get).here
706  DROPBITS here.bits.toUInt32
707  let s ← ldInflateState c.st
708  let bk ← chkI32 (s.back.toInt + here.bits.toNat)
709  wrS c.st fun s => { s with back := bk }
710  -- if (here.op & 64) { ...BAD; break; }
711  if (here.op &&& 64) != 0 then
712    badMode c "invalid distance code"
713    return
714  -- state->offset = (unsigned)here.val; state->extra = (unsigned)(here.op) & 15; state->mode = DISTEXT;
715  wrS c.st fun s => { s with offset := here.val.toUInt32, extra := here.op.toUInt32 &&& 15 }
716  setMode c.st DISTEXT
717  inflate_DISTEXT c
718
719/-- `case LENEXT:` -/
720def inflate_LENEXT (c : Ctx) : X Unit := do
721  let s ← ldInflateState c.st
722  if s.extra != 0 then
723    NEEDBITS s.extra
724    -- state->length += BITS(state->extra);
725    let b ← BITS s.extra
726    wrS c.st fun s => { s with length := s.length + b }
727    DROPBITS s.extra
728    wrS c.st fun s => { s with back := u2i (i2u s.back + s.extra) }
729  -- state->was = state->length; state->mode = DIST; /* fallthrough */
730  wrS c.st fun s => { s with was := s.length, mode := DIST }
731  inflate_DIST c
732
733/-- `case LEN:` -/
734def inflate_LEN (c : Ctx) : X Unit := do
735  let l ← get
736  -- if (have >= 6 && left >= 258 && bits < 8) { RESTORE(); inflate_fast(strm, out); LOAD(); ...; break; }
737  if l.have_ >= 6 && l.left >= 258 && l.bits < 8 then
738    RESTORE c.strm c.st
739    inflate_fast c.strm l.out_
740    LOAD c.strm c.st
741    -- if (state->mode == TYPE) state->back = -1;
742    if (← rdS c.st (·.mode)) == TYPE then wrS c.st fun s => { s with back := -1 }
743    return
744  -- state->back = 0;
745  wrS c.st fun s => { s with back := 0 }
746  lookup1 c false
747  let here := (← get).here
748  -- if (here.op && (here.op & 0xf0) == 0) {
749  if here.op != 0 && (here.op &&& 0xf0) == 0 then
750    modify fun l => { l with last := here }
751    lookup2 c false
752    let last := (← get).last
753    DROPBITS last.bits.toUInt32
754    let s ← ldInflateState c.st
755    let bk ← chkI32 (s.back.toInt + last.bits.toNat)
756    wrS c.st fun s => { s with back := bk }
757  -- DROPBITS(here.bits); state->back += here.bits; state->length = (unsigned)here.val;
758  let here := (← get).here
759  DROPBITS here.bits.toUInt32
760  let s ← ldInflateState c.st
761  let bk ← chkI32 (s.back.toInt + here.bits.toNat)
762  wrS c.st fun s => { s with back := bk, length := here.val.toUInt32 }
763  -- if ((int)(here.op) == 0) { state->mode = LIT; break; }
764  if here.op.toNat == 0 then
765    setMode c.st LIT
766    return
767  -- if (here.op & 32) { state->back = -1; state->mode = TYPE; break; }
768  if (here.op &&& 32) != 0 then
769    wrS c.st fun s => { s with back := -1, mode := TYPE }
770    return
771  -- if (here.op & 64) { ...BAD; break; }
772  if (here.op &&& 64) != 0 then
773    badMode c "invalid literal/length code"
774    return
775  -- state->extra = (unsigned)(here.op) & 15; state->mode = LENEXT; /* fallthrough */
776  wrS c.st fun s => { s with extra := here.op.toUInt32 &&& 15, mode := LENEXT }
777  inflate_LENEXT c
778
779/-- `case LEN_:` -/
780def inflate_LEN_ (c : Ctx) : X Unit := do
781  setMode c.st LEN
782  inflate_LEN c
783
784/-- `case CODELENS:` -/
785def inflate_CODELENS (c : Ctx) : X Unit := do
786  -- while (state->have < state->nlen + state->ndist) {
787  xwhileBrk
788    (do let s ← ldInflateState c.st; return s.have < s.nlen + s.ndist)
789    (do
790      lookup1 c false
791      let here := (← get).here
792      -- if (here.val < 16) { DROPBITS(here.bits); state->lens[state->have++] = here.val; }
793      if here.val < 16 then
794        DROPBITS here.bits.toUInt32
795        let s ← ldInflateState c.st
796        Ptr.store (← (lensP c.st).add (s.have.toNat : Int)) here.val
797        wrS c.st fun s => { s with «have» := s.«have» + 1 }
798        return false
799      else
800        if here.val == 16 then
801          NEEDBITS (here.bits.toUInt32 + 2)
802          DROPBITS here.bits.toUInt32
803          -- if (state->have == 0) { "invalid bit length repeat"; BAD; break; }
804          let s ← ldInflateState c.st
805          if s.«have» == 0 then
806            badMode c "invalid bit length repeat"
807            return true
808          -- len = state->lens[state->have - 1]; copy = 3 + BITS(2); DROPBITS(2);
809          let v ← Ptr.index (lensP c.st) ((s.«have» - 1).toNat : Int)
810          let b ← BITS 2
811          modify fun l => { l with len := v.toUInt32, copy := 3 + b }
812          DROPBITS 2
813        else if here.val == 17 then
814          NEEDBITS (here.bits.toUInt32 + 3)
815          DROPBITS here.bits.toUInt32
816          let b ← BITS 3
817          modify fun l => { l with len := 0, copy := 3 + b }
818          DROPBITS 3
819        else
820          NEEDBITS (here.bits.toUInt32 + 7)
821          DROPBITS here.bits.toUInt32
822          let b ← BITS 7
823          modify fun l => { l with len := 0, copy := 11 + b }
824          DROPBITS 7
825        -- if (state->have + copy > state->nlen + state->ndist) { "invalid bit length repeat"; BAD; break; }
826        let s ← ldInflateState c.st
827        if s.«have» + (← get).copy > s.nlen + s.ndist then
828          badMode c "invalid bit length repeat"
829          return true
830        -- while (copy--) state->lens[state->have++] = (unsigned short)len;
831        xwhile
832          (do
833            let l ← get
834            set { l with copy := l.copy - 1 }
835            return l.copy != 0)
836          (do
837            let s ← ldInflateState c.st
838            Ptr.store (← (lensP c.st).add (s.«have».toNat : Int)) (← get).len.toUInt16
839            wrS c.st fun s => { s with «have» := s.«have» + 1 })
840        return false)
841  -- if (state->mode == BAD) break;
842  if (← rdS c.st (·.mode)) == BAD then return
843  -- if (state->lens[256] == 0) { "invalid code -- missing end-of-block"; BAD; break; }
844  if (← Ptr.index (lensP c.st) 256) == (0 : UInt16) then
845    badMode c "invalid code -- missing end-of-block"
846    return
847  -- state->next = state->codes; state->lencode = (const code FAR *)(state->next); state->lenbits = 9;
848  wrS c.st fun s => { s with next := codesP c.st, lencode := codesP c.st, lenbits := 9 }
849  -- ret = inflate_table(LENS, state->lens, state->nlen, &(state->next), &(state->lenbits), state->work);
850  let s ← ldInflateState c.st
851  let (r, nx, lb) ← inflate_table LENS (lensP c.st) s.nlen s.next s.lenbits (workP c.st)
852  wrS c.st fun s => { s with next := nx, lenbits := lb }
853  modify fun l => { l with ret := r }
854  -- if (ret) { "invalid literal/lengths set"; BAD; break; }
855  if r != 0 then
856    badMode c "invalid literal/lengths set"
857    return
858  -- state->distcode = (const code FAR *)(state->next); state->distbits = 6;
859  wrS c.st fun s => { s with distcode := s.next, distbits := 6 }
860  -- ret = inflate_table(DISTS, state->lens + state->nlen, state->ndist, &(state->next), &(state->distbits), state->work);
861  let s ← ldInflateState c.st
862  let (r, nx, db) ← inflate_table DISTS (← (lensP c.st).add (s.nlen.toNat : Int)) s.ndist s.next s.distbits (workP c.st)
863  wrS c.st fun s => { s with next := nx, distbits := db }
864  modify fun l => { l with ret := r }
865  if r != 0 then
866    badMode c "invalid distances set"
867    return
868  -- state->mode = LEN_; if (flush == Z_TREES) goto inf_leave; /* fallthrough */
869  setMode c.st LEN_
870  if c.flush == Z_TREES then throw Ex.leave
871  inflate_LEN_ c
872
873/-- `case LENLENS:` -/
874def inflate_LENLENS (c : Ctx) : X Unit := do
875  -- while (state->have < state->ncode) { NEEDBITS(3); state->lens[order[state->have++]] = (unsigned short)BITS(3); DROPBITS(3); }
876  xwhile
877    (do let s ← ldInflateState c.st; return s.«have» < s.ncode)
878    (do
879      NEEDBITS 3
880      let s ← ldInflateState c.st
881      wrS c.st fun s => { s with «have» := s.«have» + 1 }
882      let o ← orderAt s.«have»
883      let b ← BITS 3
884      Ptr.store (← (lensP c.st).add (o.toNat : Int)) b.toUInt16
885      DROPBITS 3)
886  -- while (state->have < 19) state->lens[order[state->have++]] = 0;
887  xwhile
888    (do let s ← ldInflateState c.st; return s.«have» < 19)
889    (do
890      let s ← ldInflateState c.st
891      wrS c.st fun s => { s with «have» := s.«have» + 1 }
892      let o ← orderAt s.«have»
893      Ptr.store (← (lensP c.st).add (o.toNat : Int)) (0 : UInt16))
894  -- state->next = state->codes; state->lencode = state->distcode = (const code FAR *)(state->next); state->lenbits = 7;
895  wrS c.st fun s => { s with next := codesP c.st, distcode := codesP c.st, lencode := codesP c.st, lenbits := 7 }
896  -- ret = inflate_table(CODES, state->lens, 19, &(state->next), &(state->lenbits), state->work);
897  let s ← ldInflateState c.st
898  let (r, nx, lb) ← inflate_table CODES (lensP c.st) 19 s.next s.lenbits (workP c.st)
899  wrS c.st fun s => { s with next := nx, lenbits := lb }
900  modify fun l => { l with ret := r }
901  -- if (ret) { "invalid code lengths set"; BAD; break; }
902  if r != 0 then
903    badMode c "invalid code lengths set"
904    return
905  -- state->have = 0; state->mode = CODELENS; /* fallthrough */
906  wrS c.st fun s => { s with «have» := 0, mode := CODELENS }
907  inflate_CODELENS c
908
909/-- `case TABLE:` -/
910def inflate_TABLE (c : Ctx) : X Unit := do
911  NEEDBITS 14
912  -- state->nlen = BITS(5) + 257; DROPBITS(5);
913  let b ← BITS 5
914  wrS c.st fun s => { s with nlen := b + 257 }
915  DROPBITS 5
916  -- state->ndist = BITS(5) + 1; DROPBITS(5);
917  let b ← BITS 5
918  wrS c.st fun s => { s with ndist := b + 1 }
919  DROPBITS 5
920  -- state->ncode = BITS(4) + 4; DROPBITS(4);
921  let b ← BITS 4
922  wrS c.st fun s => { s with ncode := b + 4 }
923  DROPBITS 4
924  -- if (state->nlen > 286 || state->ndist > 30) { "too many length or distance symbols"; BAD; break; }
925  let s ← ldInflateState c.st
926  if s.nlen > 286 || s.ndist > 30 then
927    badMode c "too many length or distance symbols"
928    return
929  -- state->have = 0; state->mode = LENLENS; /* fallthrough */
930  wrS c.st fun s => { s with «have» := 0, mode := LENLENS }
931  inflate_LENLENS c
932
933/-- `case COPY:` -/
934def inflate_COPY (c : Ctx) : X Unit := do
935  -- copy = state->length;
936  let s ← ldInflateState c.st
937  let mut copy := s.length
938  -- if (copy) {
939  if copy != 0 then
940    let l ← get
941    if copy > l.have_ then copy := l.have_
942    if copy > l.left then copy := l.left
943    -- if (copy == 0) goto inf_leave;
944    if copy == 0 then
945      set { l with copy := copy }
946      throw Ex.leave
947    -- zmemcpy(put, next, copy);
948    memcpyB l.put l.next copy.toNat
949    -- have -= copy; next += copy; left -= copy; put += copy; state->length -= copy;
950    let nx ← l.next.add (copy.toNat : Int)
951    let pt ← l.put.add (copy.toNat : Int)
952    set { l with copy := copy, have_ := l.have_ - copy, next := nx, left := l.left - copy, put := pt }
953    wrS c.st fun s => { s with length := s.length - copy }
954    return
955  modify fun l => { l with copy := copy }
956  -- state->mode = TYPE; break;
957  setMode c.st TYPE
958
959/-- `case COPY_:` -/
960def inflate_COPY_ (c : Ctx) : X Unit := do
961  setMode c.st COPY
962  inflate_COPY c
963
964/-- `case STORED:` -/
965def inflate_STORED (c : Ctx) : X Unit := do
966  BYTEBITS
967  NEEDBITS 32
968  let l ← get
969  -- if ((hold & 0xffff) != ((hold >> 16) ^ 0xffff)) { "invalid stored block lengths"; BAD; break; }
970  if (l.hold &&& (0xffff : UInt64)) != ((l.hold >>> 16) ^^^ (0xffff : UInt64)) then
971    badMode c "invalid stored block lengths"
972    return
973  -- state->length = (unsigned)hold & 0xffff;
974  wrS c.st fun s => { s with length := l.hold.toUInt32 &&& 0xffff }
975  INITBITS
976  -- state->mode = COPY_; if (flush == Z_TREES) goto inf_leave; /* fallthrough */
977  setMode c.st COPY_
978  if c.flush == Z_TREES then throw Ex.leave
979  inflate_COPY_ c
980
981/-- `case TYPEDO:` -/
982def inflate_TYPEDO (c : Ctx) : X Unit := do
983  -- if (state->last) { BYTEBITS(); state->mode = CHECK; break; }
984  if (← rdS c.st (·.last)) != 0 then
985    BYTEBITS
986    setMode c.st CHECK
987    return
988  NEEDBITS 3
989  -- state->last = BITS(1); DROPBITS(1);
990  let b ← BITS 1
991  wrS c.st fun s => { s with last := u2i b }
992  DROPBITS 1
993  -- switch (BITS(2)) {
994  match (← BITS 2) with
995  | 0 => setMode c.st STORED
996  | 1 =>
997    inflate_fixed c.st
998    setMode c.st LEN_
999    -- if (flush == Z_TREES) { DROPBITS(2); goto inf_leave; }
1000    if c.flush == Z_TREES then
1001      DROPBITS 2
1002      throw Ex.leave
1003  | 2 => setMode c.st TABLE
1004  | _ => badMode c "invalid block type"
1005  -- DROPBITS(2); break;
1006  DROPBITS 2
1007
1008/-- `case TYPE:` -/
1009def inflate_TYPE (c : Ctx) : X Unit := do
1010  -- if (flush == Z_BLOCK || flush == Z_TREES) goto inf_leave; /* fallthrough, the mode is not written */
1011  if c.flush == Z_BLOCK || c.flush == Z_TREES then throw Ex.leave
1012  inflate_TYPEDO c
1013
1014/-- `case DICT:` -/
1015def inflate_DICT (c : Ctx) : X Unit := do
1016  -- if (state->havedict == 0) { RESTORE(); strm->total_in += in - strm->avail_in; return Z_NEED_DICT; }
1017  if (← rdS c.st (·.havedict)) == 0 then
1018    RESTORE c.strm c.st
1019    let l ← get
1020    wrZ c.strm fun z => { z with total_in := z.total_in + (l.in_ - z.avail_in).toUInt64 }
1021    throw (Ex.ret Z_NEED_DICT)
1022  -- strm->adler = state->check = adler32(0L, Z_NULL, 0);
1023  let v ← adler32 0 .null 0
1024  wrS c.st fun s => { s with check := v }
1025  wrZ c.strm fun z => { z with adler := v }
1026  -- state->mode = TYPE; /* fallthrough */
1027  setMode c.st TYPE
1028  inflate_TYPE c
1029
1030/-- `case DICTID:` -/
1031def inflate_DICTID (c : Ctx) : X Unit := do
1032  NEEDBITS 32
1033  -- strm->adler = state->check = ZSWAP32(hold);
1034  let v := ZSWAP32 (← get).hold
1035  wrS c.st fun s => { s with check := v }
1036  wrZ c.strm fun z => { z with adler := v }
1037  INITBITS
1038  setMode c.st DICT
1039  inflate_DICT c
1040
1041/-- `case HCRC:` -/
1042def inflate_HCRC (c : Ctx) : X Unit := do
1043  -- if (state->flags & 0x0200) {
1044  if ((← rdS c.st (·.flags)) &&& 0x0200) != 0 then
1045    NEEDBITS 16
1046    let s ← ldInflateState c.st
1047    -- if ((state->wrap & 4) && hold != (state->check & 0xffff)) { "header crc mismatch"; BAD; break; }
1048    if (s.wrap &&& 4) != 0 && (← get).hold != (s.check &&& 0xffff) then
1049      badMode c "header crc mismatch"
1050      return
1051    INITBITS
1052  -- if (state->head != Z_NULL) { state->head->hcrc = (int)((state->flags >> 9) & 1); state->head->done = 1; }
1053  let s ← ldInflateState c.st
1054  if s.head != none then
1055    let g ← ldGzHeader s.head
1056    stGzHeader s.head { g with hcrc := (s.flags >>> 9) &&& 1, done := 1 }
1057  -- strm->adler = state->check = crc32(0L, Z_NULL, 0);
1058  let v ← crc32 0 .null 0
1059  wrS c.st fun s => { s with check := v }
1060  wrZ c.strm fun z => { z with adler := v }
1061  -- state->mode = TYPE; break;
1062  setMode c.st TYPE
1063
1064/-- `case COMMENT:` -/
1065def inflate_COMMENT (c : Ctx) : X Unit := do
1066  -- if (state->flags & 0x1000) {
1067  if ((← rdS c.st (·.flags)) &&& 0x1000) != 0 then
1068    -- if (have == 0) goto inf_leave; copy = 0;
1069    if (← get).have_ == 0 then throw Ex.leave
1070    modify fun l => { l with copy := 0 }
1071    -- do { len = (unsigned)(next[copy++]); if (head && head->comment && length < comm_max) head->comment[length++] = (Bytef)len; } while (len && copy < have);
1072    xdoWhile
1073      (do
1074        let l ← get
1075        let b ← index8 l.next l.copy.toNat
1076        set { l with len := b.toUInt32, copy := l.copy + 1 }
1077        let s ← ldInflateState c.st
1078        if s.head != none then
1079          let g ← ldGzHeader s.head
1080          if g.comment != .null && s.length < g.comm_max then
1081            store8 (← g.comment.add (s.length.toNat : Int)) b
1082            wrS c.st fun s => { s with length := s.length + 1 })
1083      (do let l ← get; return l.len != 0 && l.copy < l.have_)
1084    -- if ((state->flags & 0x0200) && (state->wrap & 4)) state->check = crc32(state->check, next, copy);
1085    if ← hcrcOn c.st then
1086      let l ← get
1087      let v ← crc32 (← rdS c.st (·.check)) l.next l.copy
1088      wrS c.st fun s => { s with check := v }
1089    -- have -= copy; next += copy; if (len) goto inf_leave;
1090    let l ← get
1091    let nx ← l.next.add (l.copy.toNat : Int)
1092    set { l with have_ := l.have_ - l.copy, next := nx }
1093    if l.len != 0 then throw Ex.leave
1094  else
1095    -- else if (state->head != Z_NULL) state->head->comment = Z_NULL;
1096    let s ← ldInflateState c.st
1097    if s.head != none then
1098      let g ← ldGzHeader s.head
1099      stGzHeader s.head { g with comment := .null }
1100  -- state->mode = HCRC; /* fallthrough */
1101  setMode c.st HCRC
1102  inflate_HCRC c
1103
1104/-- `case NAME:` -/
1105def inflate_NAME (c : Ctx) : X Unit := do
1106  if ((← rdS c.st (·.flags)) &&& 0x0800) != 0 then
1107    if (← get).have_ == 0 then throw Ex.leave
1108    modify fun l => { l with copy := 0 }
1109    xdoWhile
1110      (do
1111        let l ← get
1112        let b ← index8 l.next l.copy.toNat
1113        set { l with len := b.toUInt32, copy := l.copy + 1 }
1114        let s ← ldInflateState c.st
1115        if s.head != none then
1116          let g ← ldGzHeader s.head
1117          if g.name != .null && s.length < g.name_max then
1118            store8 (← g.name.add (s.length.toNat : Int)) b
1119            wrS c.st fun s => { s with length := s.length + 1 })
1120      (do let l ← get; return l.len != 0 && l.copy < l.have_)
1121    if ← hcrcOn c.st then
1122      let l ← get
1123      let v ← crc32 (← rdS c.st (·.check)) l.next l.copy
1124      wrS c.st fun s => { s with check := v }
1125    let l ← get
1126    let nx ← l.next.add (l.copy.toNat : Int)
1127    set { l with have_ := l.have_ - l.copy, next := nx }
1128    if l.len != 0 then throw Ex.leave
1129  else
1130    -- else if (state->head != Z_NULL) state->head->name = Z_NULL;
1131    let s ← ldInflateState c.st
1132    if s.head != none then
1133      let g ← ldGzHeader s.head
1134      stGzHeader s.head { g with name := .null }
1135  -- state->length = 0; state->mode = COMMENT; /* fallthrough */
1136  wrS c.st fun s => { s with length := 0, mode := COMMENT }
1137  inflate_COMMENT c
1138
1139/-- `case EXTRA:` -/
1140def inflate_EXTRA (c : Ctx) : X Unit := do
1141  -- if (state->flags & 0x0400) {
1142  if ((← rdS c.st (·.flags)) &&& 0x0400) != 0 then
1143    -- copy = state->length; if (copy > have) copy = have;
1144    let s ← ldInflateState c.st
1145    let l ← get
1146    let copy := if s.length > l.have_ then l.have_ else s.length
1147    set { l with copy := copy }
1148    -- if (copy) {
1149    if copy != 0 then
1150      -- if (state->head != Z_NULL && state->head->extra != Z_NULL && (len = state->head->extra_len - state->length) < state->head->extra_max) {
1151      if s.head != none then
1152        let g ← ldGzHeader s.head
1153        if g.extra != .null then
1154          let len := g.extra_len - s.length
1155          modify fun l => { l with len := len }
1156          if len < g.extra_max then
1157            -- zmemcpy(state->head->extra + len, next, len + copy > extra_max ? extra_max - len : copy);
1158            let n := if len + copy > g.extra_max then g.extra_max - len else copy
1159            memcpyB (← g.extra.add (len.toNat : Int)) (← get).next n.toNat
1160      -- if ((state->flags & 0x0200) && (state->wrap & 4)) state->check = crc32(state->check, next, copy);
1161      if ← hcrcOn c.st then
1162        let v ← crc32 (← rdS c.st (·.check)) (← get).next copy
1163        wrS c.st fun s => { s with check := v }
1164      -- have -= copy; next += copy; state->length -= copy;
1165      let l ← get
1166      let nx ← l.next.add (copy.toNat : Int)
1167      set { l with have_ := l.have_ - copy, next := nx }
1168      wrS c.st fun s => { s with length := s.length - copy }
1169    -- if (state->length) goto inf_leave;
1170    if (← rdS c.st (·.length)) != 0 then throw Ex.leave
1171  -- state->length = 0; state->mode = NAME; /* fallthrough */
1172  wrS c.st fun s => { s with length := 0, mode := NAME }
1173  inflate_NAME c
1174
1175/-- `case EXLEN:` -/
1176def inflate_EXLEN (c : Ctx) : X Unit := do
1177  let s ← ldInflateState c.st
1178  -- if (state->flags & 0x0400) {
1179  if (s.flags &&& 0x0400) != 0 then
1180    NEEDBITS 16
1181    let l ← get
1182    -- state->length = (unsigned)(hold);
1183    wrS c.st fun s => { s with length := l.hold.toUInt32 }
1184    -- if (state->head != Z_NULL) state->head->extra_len = (unsigned)hold;
1185    let s ← ldInflateState c.st
1186    if s.head != none then
1187      let g ← ldGzHeader s.head
1188      stGzHeader s.head { g with extra_len := l.hold.toUInt32 }
1189    -- if ((state->flags & 0x0200) && (state->wrap & 4)) CRC2(state->check, hold);
1190    if ← hcrcOn c.st then CRC2 c
1191    INITBITS
1192  else
1193    -- else if (state->head != Z_NULL) state->head->extra = Z_NULL;
1194    if s.head != none then
1195      let g ← ldGzHeader s.head
1196      stGzHeader s.head { g with extra := .null }
1197  -- state->mode = EXTRA; /* fallthrough */
1198  setMode c.st EXTRA
1199  inflate_EXTRA c
1200
1201/-- `case OS:` -/
1202def inflate_OS (c : Ctx) : X Unit := do
1203  NEEDBITS 16
1204  let l ← get
1205  let s ← ldInflateState c.st
1206  -- if (state->head != Z_NULL) { state->head->xflags = (int)(hold & 0xff); state->head->os = (int)(hold >> 8); }
1207  if s.head != none then
1208    let g ← ldGzHeader s.head
1209    stGzHeader s.head { g with xflags := (l.hold &&& 0xff).toUInt32.toInt32, os := (l.hold >>> 8).toUInt32.toInt32 }
1210  if ← hcrcOn c.st then CRC2 c
1211  INITBITS
1212  setMode c.st EXLEN
1213  inflate_EXLEN c
1214
1215/-- `case TIME:` -/
1216def inflate_TIME (c : Ctx) : X Unit := do
1217  NEEDBITS 32
1218  let l ← get
1219  let s ← ldInflateState c.st
1220  -- if (state->head != Z_NULL) state->head->time = hold;
1221  if s.head != none then
1222    let g ← ldGzHeader s.head
1223    stGzHeader s.head { g with time := l.hold }
1224  -- if ((state->flags & 0x0200) && (state->wrap & 4)) CRC4(state->check, hold);
1225  if ← hcrcOn c.st then CRC4 c
1226  INITBITS
1227  setMode c.st OS
1228  inflate_OS c
1229
1230/-- `case FLAGS:` -/
1231def inflate_FLAGS (c : Ctx) : X Unit := do
1232  NEEDBITS 16
1233  let l ← get
1234  -- state->flags = (int)(hold);   (implementation-defined conversion: modulo 2^32)
1235  wrS c.st fun s => { s with flags := l.hold.toUInt32.toInt32 }
1236  let s ← ldInflateState c.st
1237  -- if ((state->flags & 0xff) != Z_DEFLATED) { "unknown compression method"; BAD; break; }
1238  if (s.flags &&& 0xff) != Z_DEFLATED then
1239    badMode c "unknown compression method"
1240    return
1241  -- if (state->flags & 0xe000) { "unknown header flags set"; BAD; break; }
1242  if (s.flags &&& 0xe000) != 0 then
1243    badMode c "unknown header flags set"
1244    return
1245  -- if (state->head != Z_NULL) state->head->text = (int)((hold >> 8) & 1);
1246  if s.head != none then
1247    let g ← ldGzHeader s.head
1248    stGzHeader s.head { g with text := ((l.hold >>> 8) &&& 1).toUInt32.toInt32 }
1249  -- if ((state->flags & 0x0200) && (state->wrap & 4)) CRC2(state->check, hold);
1250  if ← hcrcOn c.st then CRC2 c
1251  INITBITS
1252  setMode c.st TIME
1253  inflate_TIME c
1254
1255/-- `case HEAD:` -/
1256def inflate_HEAD (c : Ctx) : X Unit := do
1257  -- if (state->wrap == 0) { state->mode = TYPEDO; break; }
1258  if (← rdS c.st (·.wrap)) == 0 then
1259    setMode c.st TYPEDO
1260    return
1261  NEEDBITS 16
1262  let l ← get
1263  let s ← ldInflateState c.st
1264  -- if ((state->wrap & 2) && hold == 0x8b1f) {  /* gzip header */
1265  if (s.wrap &&& 2) != 0 && l.hold == 0x8b1f then
1266    -- if (state->wbits == 0) state->wbits = 15;
1267    if s.wbits == 0 then wrS c.st fun s => { s with wbits := 15 }
1268    -- state->check = crc32(0L, Z_NULL, 0); CRC2(state->check, hold); INITBITS(); state->mode = FLAGS; break;
1269    let v ← crc32 0 .null 0
1270    wrS c.st fun s => { s with check := v }
1271    CRC2 c
1272    INITBITS
1273    setMode c.st FLAGS
1274    return
1275  -- if (state->head != Z_NULL) state->head->done = -1;
1276  if s.head != none then
1277    let g ← ldGzHeader s.head
1278    stGzHeader s.head { g with done := -1 }
1279  -- if (!(state->wrap & 1) || ((BITS(8) << 8) + (hold >> 8)) % 31) { "incorrect header check"; BAD; break; }
1280  let b8 ← BITS 8
1281  if (s.wrap &&& 1) == 0 || ((b8 <<< 8).toUInt64 + (l.hold >>> 8)) % 31 != 0 then
1282    badMode c "incorrect header check"
1283    return
1284  -- if (BITS(4) != Z_DEFLATED) { "unknown compression method"; BAD; break; }
1285  if (← BITS 4) != i2u Z_DEFLATED then
1286    badMode c "unknown compression method"
1287    return
1288  DROPBITS 4
1289  -- len = BITS(4) + 8;
1290  let len := (← BITS 4) + 8
1291  modify fun l => { l with len := len }
1292  -- if (len > 15 || (state->wbits != 0 && len > state->wbits)) { "invalid window size"; BAD; break; }
1293  let s ← ldInflateState c.st
1294  if len > 15 || (s.wbits != 0 && len > s.wbits) then
1295    badMode c "invalid window size"
1296    return
1297  -- if (state->wbits == 0) state->wbits = len;
1298  if s.wbits == 0 then wrS c.st fun s => { s with wbits := len }
1299  -- state->dmax = 1U << len; state->flags = 0;
1300  let dm ← shl32 1 len
1301  wrS c.st fun s => { s with dmax := dm, flags := 0 }
1302  -- strm->adler = state->check = adler32(0L, Z_NULL, 0);
1303  let v ← adler32 0 .null 0
1304  wrS c.st fun s => { s with check := v }
1305  wrZ c.strm fun z => { z with adler := v }
1306  -- state->mode = hold & 0x200 ? DICTID : TYPE; INITBITS(); break;
1307  let l ← get
1308  setMode c.st (if (l.hold &&& 0x200) != 0 then DICTID else TYPE)
1309  INITBITS
1310
1311/-- The `switch (state->mode)`: the mode is read from the heap on every trip. `MEM` returns `Z_MEM_ERROR`; `SYNC` and
1312every other value return `Z_STREAM_ERROR`. -/
1313def inflate_dispatch (c : Ctx) : X Unit := do
1314  let m ← rdS c.st (·.mode)
1315  if m == HEAD then inflate_HEAD c
1316  else if m == FLAGS then inflate_FLAGS c
1317  else if m == TIME then inflate_TIME c
1318  else if m == OS then inflate_OS c
1319  else if m == EXLEN then inflate_EXLEN c
1320  else if m == EXTRA then inflate_EXTRA c
1321  else if m == NAME then inflate_NAME c
1322  else if m == COMMENT then inflate_COMMENT c
1323  else if m == HCRC then inflate_HCRC c
1324  else if m == DICTID then inflate_DICTID c
1325  else if m == DICT then inflate_DICT c
1326  else if m == TYPE then inflate_TYPE c
1327  else if m == TYPEDO then inflate_TYPEDO c
1328  else if m == STORED then inflate_STORED c
1329  else if m == COPY_ then inflate_COPY_ c
1330  else if m == COPY then inflate_COPY c
1331  else if m == TABLE then inflate_TABLE c
1332  else if m == LENLENS then inflate_LENLENS c
1333  else if m == CODELENS then inflate_CODELENS c
1334  else if m == LEN_ then inflate_LEN_ c
1335  else if m == LEN then inflate_LEN c
1336  else if m == LENEXT then inflate_LENEXT c
1337  else if m == DIST then inflate_DIST c
1338  else if m == DISTEXT then inflate_DISTEXT c
1339  else if m == MATCH then inflate_MATCH c
1340  else if m == LIT then inflate_LIT c
1341  else if m == CHECK then inflate_CHECK c
1342  else if m == LENGTH then inflate_LENGTH c
1343  else if m == DONE then inflate_DONE c
1344  else if m == BAD then
1345    -- case BAD: ret = Z_DATA_ERROR; goto inf_leave;
1346    modify fun l => { l with ret := Z_DATA_ERROR }
1347    throw Ex.leave
1348  else if m == MEM then throw (Ex.ret Z_MEM_ERROR)
1349  else throw (Ex.ret Z_STREAM_ERROR)
1350
1351/-- Everything of `inflate()` from `LOAD()` to the end of `for (;;) switch`. -/
1352def inflate_run (c : Ctx) : X Unit := do
1353  -- if (state->mode == TYPE) state->mode = TYPEDO;      /* skip check */
1354  if (← rdS c.st (·.mode)) == TYPE then setMode c.st TYPEDO
1355  LOAD c.strm c.st
1356  -- in = have; out = left; ret = Z_OK;
1357  modify fun l => { l with in_ := l.have_, out_ := l.left, ret := Z_OK }
1358  -- for (;;) switch (state->mode) { ... }
1359  xwhile (pure true) (inflate_dispatch c)
1360
1361/-- `inf_leave:` and what follows it (`RESTORE()` .. `return ret`), with the registers `l` at the `goto`. -/
1362def inflate_leave (c : Ctx) (l : IL) : M Int32 := do
1363  -- RESTORE();
1364  wrZ c.strm fun z => { z with next_out := l.put, avail_out := l.left, next_in := l.next, avail_in := l.have_ }
1365  wrS c.st fun s => { s with hold := l.hold, bits := l.bits }
1366  let z ← ldZStream c.strm
1367  let s ← ldInflateState c.st
1368  -- if (state->wsize || (out != strm->avail_out && state->mode < BAD && (state->mode < CHECK || flush != Z_FINISH)))
1369  --     if (updatewindow(strm, strm->next_out, out - strm->avail_out)) { state->mode = MEM; return Z_MEM_ERROR; }
1370  if s.wsize != 0 || (l.out_ != z.avail_out && s.mode < BAD && (s.mode < CHECK || c.flush != Z_FINISH)) then
1371    if (← updatewindow c.strm z.next_out (l.out_ - z.avail_out)) != 0 then
1372      setMode c.st MEM
1373      return Z_MEM_ERROR
1374  -- in -= strm->avail_in; out -= strm->avail_out;
1375  let in_ := l.in_ - z.avail_in
1376  let out_ := l.out_ - z.avail_out
1377  -- strm->total_in += in; strm->total_out += out; state->total += out;
1378  wrZ c.strm fun z => { z with total_in := z.total_in + in_.toUInt64, total_out := z.total_out + out_.toUInt64 }
1379  wrS c.st fun s => { s with total := s.total + out_.toUInt64 }
1380  -- if ((state->wrap & 4) && out) strm->adler = state->check = UPDATE_CHECK(state->check, strm->next_out - out, out);
1381  let s ← ldInflateState c.st
1382  if (s.wrap &&& 4) != 0 && out_ != 0 then
1383    let p ← z.next_out.add (-(out_.toNat : Int))
1384    let v ← UPDATE_CHECK c.st s.check p out_
1385    wrS c.st fun s => { s with check := v }
1386    wrZ c.strm fun z => { z with adler := v }
1387  -- strm->data_type = (int)state->bits + (state->last ? 64 : 0) + (state->mode == TYPE ? 128 : 0) +
1388  --                   (state->mode == LEN_ || state->mode == COPY_ ? 256 : 0);
1389  let s ← ldInflateState c.st
1390  let dt ← chkI32 ((u2i s.bits).toInt + (if s.last != 0 then 64 else 0) + (if s.mode == TYPE then 128 else 0) +
1391    (if s.mode == LEN_ || s.mode == COPY_ then 256 else 0))
1392  wrZ c.strm fun z => { z with data_type := dt }
1393  -- if (((in == 0 && out == 0) || flush == Z_FINISH) && ret == Z_OK) ret = Z_BUF_ERROR;
1394  let mut ret := l.ret
1395  if ((in_ == 0 && out_ == 0) || c.flush == Z_FINISH) && ret == Z_OK then ret := Z_BUF_ERROR
1396  return ret
1397
1398/-- `int ZEXPORT inflate(z_streamp strm, int flush)` -/
1399def inflate (strm : ZStreamPtr) (flush : Int32) : M Int32 := do
1400  -- unsigned char hbuf[4];
1401  let hbuf ← allocLocalB 4
1402  let r ← (do
1403    -- if (inflateStateCheck(strm) || strm->next_out == Z_NULL || (strm->next_in == Z_NULL && strm->avail_in != 0)) return Z_STREAM_ERROR;
1404    if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1405    let z ← ldZStream strm
1406    if z.next_out == .null || (z.next_in == .null && z.avail_in != 0) then return Z_STREAM_ERROR
1407    -- state = (struct inflate_state FAR *)strm->state;
1408    let st ← castInflateState z.state
1409    let c : Ctx := { strm, st, hbuf, flush }
1410    let (r, l) ← StateT.run (ExceptT.run (inflate_run c)) IL.init
1411    match r with
1412    | .error (.ret v) => return v
1413    | _ => inflate_leave c l)
1414  freeB hbuf
1415  return r
1416
1417/-- `int ZEXPORT inflateEnd(z_streamp strm)` -/
1418def inflateEnd (strm : ZStreamPtr) : M Int32 := do
1419  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1420  let z ← ldZStream strm
1421  let st ← castInflateState z.state
1422  -- if (state->window != Z_NULL) ZFREE(strm, state->window);
1423  let s ← ldInflateState st
1424  if s.window != .null then ZFREEB strm s.window
1425  -- ZFREE(strm, strm->state); strm->state = Z_NULL;
1426  ZFREES strm st
1427  wrZ strm fun z => { z with state := none }
1428  return Z_OK
1429
1430/-- `int ZEXPORT inflateGetDictionary(z_streamp strm, Bytef *dictionary, uInt *dictLength)`.
1431`dictLength` is the value of `*dictLength` (`none` for `NULL`); the second result is `*dictLength` afterwards. -/
1432def inflateGetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : Option UInt32) :
1433    M (Int32 × Option UInt32) := do
1434  if (← inflateStateCheck strm) != 0 then return (Z_STREAM_ERROR, dictLength)
1435  let z ← ldZStream strm
1436  let st ← castInflateState z.state
1437  let s ← ldInflateState st
1438  -- if (state->whave && dictionary != Z_NULL) {
1439  if s.whave != 0 && dictionary != .null then
1440    -- zmemcpy(dictionary, state->window + state->wnext, state->whave - state->wnext);
1441    memcpyB dictionary (← s.window.add (s.wnext.toNat : Int)) (s.whave - s.wnext).toNat
1442    -- zmemcpy(dictionary + state->whave - state->wnext, state->window, state->wnext);
1443    let d1 ← dictionary.add (s.whave.toNat : Int)
1444    let d2 ← d1.add (-(s.wnext.toNat : Int))
1445    memcpyB d2 s.window s.wnext.toNat
1446  -- if (dictLength != Z_NULL) *dictLength = state->whave;
1447  match dictLength with
1448  | some _ => return (Z_OK, some s.whave)
1449  | none => return (Z_OK, none)
1450
1451/-- `int ZEXPORT inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)` -/
1452def inflateSetDictionary (strm : ZStreamPtr) (dictionary : BPtr) (dictLength : UInt32) : M Int32 := do
1453  -- if (inflateStateCheck(strm) || dictionary == Z_NULL) return Z_STREAM_ERROR;
1454  if (← inflateStateCheck strm) != 0 || dictionary == .null then return Z_STREAM_ERROR
1455  let z ← ldZStream strm
1456  let st ← castInflateState z.state
1457  let s ← ldInflateState st
1458  -- if (state->wrap != 0 && state->mode != DICT) return Z_STREAM_ERROR;
1459  if s.wrap != 0 && s.mode != DICT then return Z_STREAM_ERROR
1460  -- if (state->mode == DICT) { dictid = adler32(0L, Z_NULL, 0); dictid = adler32(dictid, dictionary, dictLength); if (dictid != state->check) return Z_DATA_ERROR; }
1461  if s.mode == DICT then
1462    let dictid ← adler32 0 .null 0
1463    let dictid ← adler32 dictid dictionary dictLength
1464    if dictid != s.check then return Z_DATA_ERROR
1465  -- ret = updatewindow(strm, dictionary + dictLength, dictLength);
1466  let ret ← updatewindow strm (← dictionary.add (dictLength.toNat : Int)) dictLength
1467  -- if (ret) { state->mode = MEM; return Z_MEM_ERROR; }
1468  if ret != 0 then
1469    setMode st MEM
1470    return Z_MEM_ERROR
1471  -- state->havedict = 1;
1472  wrS st fun s => { s with havedict := 1 }
1473  return Z_OK
1474
1475/-- `int ZEXPORT inflateGetHeader(z_streamp strm, gz_headerp head)` -/
1476def inflateGetHeader (strm : ZStreamPtr) (head : GzHeaderPtr) : M Int32 := do
1477  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1478  let z ← ldZStream strm
1479  let st ← castInflateState z.state
1480  -- if ((state->wrap & 2) == 0) return Z_STREAM_ERROR;
1481  if ((← rdS st (·.wrap)) &&& 2) == 0 then return Z_STREAM_ERROR
1482  -- state->head = head; head->done = 0;
1483  wrS st fun s => { s with head := head }
1484  let g ← ldGzHeader head
1485  stGzHeader head { g with done := 0 }
1486  return Z_OK
1487
1488/-- `local unsigned syncsearch(unsigned FAR *have, const unsigned char FAR *buf, unsigned len)`.
1489`have` is the value of `*have`; the result is (return value, `*have` afterwards). -/
1490def syncsearch (have_ : UInt32) (buf : BPtr) (len : UInt32) : M (UInt32 × UInt32) := do
1491  -- got = *have; next = 0;
1492  let (next, got) ← cwhile (σ := UInt32 × UInt32)
1493    -- while (next < len && got < 4) {
1494    (fun (next, got) => pure (next < len && got < 4, (next, got)))
1495    (fun (next, got) => do
1496      let b ← index8 buf next.toNat
1497      -- if ((int)(buf[next]) == (got < 2 ? 0 : 0xff)) got++; else if (buf[next]) got = 0; else got = 4 - got;
1498      let got := if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
1499      -- next++;
1500      pure (next + 1, got))
1501    (0, have_)
1502  -- *have = got; return next;
1503  return (next, got)
1504
1505/-- `int ZEXPORT inflateSync(z_streamp strm)` -/
1506def inflateSync (strm : ZStreamPtr) : M Int32 := do
1507  -- unsigned char buf[4];
1508  let buf ← allocLocalB 4
1509  let r ← (do
1510    if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1511    let z ← ldZStream strm
1512    let st ← castInflateState z.state
1513    let s ← ldInflateState st
1514    -- if (strm->avail_in == 0 && state->bits < 8) return Z_BUF_ERROR;
1515    if z.avail_in == 0 && s.bits < 8 then return Z_BUF_ERROR
1516    -- if (state->mode != SYNC) {
1517    if s.mode != SYNC then
1518      -- state->mode = SYNC; state->hold >>= state->bits & 7; state->bits -= state->bits & 7;
1519      let h ← shr64 s.hold (s.bits &&& 7)
1520      wrS st fun s => { s with mode := SYNC, hold := h, bits := s.bits - (s.bits &&& 7) }
1521      -- len = 0; while (state->bits >= 8) { buf[len++] = (unsigned char)(state->hold); state->hold >>= 8; state->bits -= 8; }
1522      let len ← cwhile (σ := UInt32)
1523        (fun len => do return ((← rdS st (·.bits)) >= 8, len))
1524        (fun len => do
1525          let s ← ldInflateState st
1526          store8 (← buf.add (len.toNat : Int)) s.hold.toUInt8
1527          wrS st fun s => { s with hold := s.hold >>> 8, bits := s.bits - 8 }
1528          pure (len + 1))
1529        0
1530      -- state->have = 0; syncsearch(&(state->have), buf, len);
1531      wrS st fun s => { s with «have» := 0 }
1532      let (_, hv) ← syncsearch 0 buf len
1533      wrS st fun s => { s with «have» := hv }
1534    -- len = syncsearch(&(state->have), strm->next_in, strm->avail_in);
1535    let z ← ldZStream strm
1536    let (len, hv) ← syncsearch (← rdS st (·.«have»)) z.next_in z.avail_in
1537    wrS st fun s => { s with «have» := hv }
1538    -- strm->avail_in -= len; strm->next_in += len; strm->total_in += len;
1539    let ni ← z.next_in.add (len.toNat : Int)
1540    wrZ strm fun z => { z with avail_in := z.avail_in - len, next_in := ni, total_in := z.total_in + len.toUInt64 }
1541    -- if (state->have != 4) return Z_DATA_ERROR;
1542    if (← rdS st (·.«have»)) != 4 then return Z_DATA_ERROR
1543    -- flags = state->flags; in = strm->total_in; out = strm->total_out;
1544    let flags ← rdS st (·.flags)
1545    let z ← ldZStream strm
1546    let in_ := z.total_in
1547    let out_ := z.total_out
1548    -- inflateReset(strm);
1549    let _ ← inflateReset strm
1550    -- strm->total_in = in; strm->total_out = out; state->flags = flags;
1551    wrZ strm fun z => { z with total_in := in_, total_out := out_ }
1552    wrS st fun s => { s with flags := flags }
1553    -- if (flags == -1) state->wrap = 0; else state->wrap &= ~4;
1554    if flags == -1 then wrS st fun s => { s with wrap := 0 }
1555    else wrS st fun s => { s with wrap := s.wrap &&& ~~~4 }
1556    -- if (state->wbits == 0) {
1557    let s ← ldInflateState st
1558    if s.wbits == 0 then
1559      if s.window != .null then
1560        ZFREEB strm s.window
1561        wrS st fun s => { s with window := .null }
1562      wrS st fun s => { s with wbits := 15 }
1563    -- state->mode = TYPE; return Z_OK;
1564    setMode st TYPE
1565    return Z_OK)
1566  freeB buf
1567  return r
1568
1569/-- `int ZEXPORT inflateSyncPoint(z_streamp strm)` -/
1570def inflateSyncPoint (strm : ZStreamPtr) : M Int32 := do
1571  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1572  let z ← ldZStream strm
1573  let st ← castInflateState z.state
1574  let s ← ldInflateState st
1575  -- return state->mode == STORED && state->bits == 0;
1576  return if s.mode == STORED && s.bits == 0 then 1 else 0
1577
1578/-- `int ZEXPORT inflateCopy(z_streamp dest, z_streamp source)` -/
1579def inflateCopy (dest source : ZStreamPtr) : M Int32 := do
1580  -- if (dest == Z_NULL) return Z_STREAM_ERROR;
1581  if dest == none then return Z_STREAM_ERROR
1582  -- if (inflateStateCheck(source)) { dest->state = Z_NULL; return Z_STREAM_ERROR; }
1583  if (← inflateStateCheck source) != 0 then
1584    wrZ dest fun z => { z with state := none }
1585    return Z_STREAM_ERROR
1586  let zs ← ldZStream source
1587  let state ← castInflateState zs.state
1588  -- copy = ZALLOC(source, 1, sizeof(struct inflate_state));
1589  let copy ← ZALLOCS source
1590  -- if (copy == Z_NULL) { dest->state = Z_NULL; return Z_MEM_ERROR; }
1591  if copy == none then
1592    wrZ dest fun z => { z with state := none }
1593    return Z_MEM_ERROR
1594  -- zmemzero(copy, sizeof(struct inflate_state));
1595  stInflateState copy (InflateState.zeroed)
1596  -- window = Z_NULL;
1597  let mut window : BPtr := .null
1598  let s ← ldInflateState state
1599  -- if (state->window != Z_NULL) {
1600  if s.window != .null then
1601    window ← ZALLOCB source (← shl32 1 s.wbits) 1
1602    -- if (window == Z_NULL) { ZFREE(source, copy); dest->state = Z_NULL; return Z_MEM_ERROR; }
1603    if window == .null then
1604      ZFREES source copy
1605      wrZ dest fun z => { z with state := none }
1606      return Z_MEM_ERROR
1607  -- zmemcpy(dest, source, sizeof(z_stream));   (a whole-struct copy; the same object is overlapping)
1608  copyZStream dest source
1609  -- zmemcpy(copy, state, sizeof(struct inflate_state));
1610  copyInflateState copy state
1611  -- copy->strm = dest;
1612  wrS copy fun s => { s with strm := dest }
1613  -- if (state->lencode >= state->codes && state->lencode <= state->codes + ENOUGH - 1) {
1614  let s ← ldInflateState state
1615  let hi ← (← (codesP state).add 1444).add (-1)
1616  if (← Ptr.le (codesP state) s.lencode) && (← Ptr.le s.lencode hi) then
1617    -- copy->lencode = copy->codes + (state->lencode - state->codes);
1618    let d1 ← Ptr.diff s.lencode (codesP state)
1619    let lc ← (codesP copy).add d1.toInt
1620    -- copy->distcode = copy->codes + (state->distcode - state->codes);
1621    let d2 ← Ptr.diff s.distcode (codesP state)
1622    let dc ← (codesP copy).add d2.toInt
1623    wrS copy fun s => { s with lencode := lc, distcode := dc }
1624  -- copy->next = copy->codes + (state->next - state->codes);
1625  let d3 ← Ptr.diff s.next (codesP state)
1626  let nx ← (codesP copy).add d3.toInt
1627  wrS copy fun s => { s with next := nx }
1628  -- if (window != Z_NULL) zmemcpy(window, state->window, state->whave);
1629  if window != .null then memcpyB window s.window s.whave.toNat
1630  -- copy->window = window; dest->state = (struct internal_state FAR *)copy;
1631  wrS copy fun s => { s with window := window }
1632  wrZ dest fun z => { z with state := StateRef.ofInflateState copy }
1633  return Z_OK
1634
1635/-- `int ZEXPORT inflateUndermine(z_streamp strm, int subvert)` (`INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR` undefined) -/
1636def inflateUndermine (strm : ZStreamPtr) (_subvert : Int32) : M Int32 := do
1637  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1638  let z ← ldZStream strm
1639  let st ← castInflateState z.state
1640  -- (void)subvert; state->sane = 1; return Z_DATA_ERROR;
1641  wrS st fun s => { s with sane := 1 }
1642  return Z_DATA_ERROR
1643
1644/-- `int ZEXPORT inflateValidate(z_streamp strm, int check)` -/
1645def inflateValidate (strm : ZStreamPtr) (check : Int32) : M Int32 := do
1646  if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
1647  let z ← ldZStream strm
1648  let st ← castInflateState z.state
1649  let s ← ldInflateState st
1650  -- if (check && state->wrap) state->wrap |= 4; else state->wrap &= ~4;
1651  let wrap := if check != 0 && s.wrap != 0 then s.wrap ||| 4 else s.wrap &&& ~~~4
1652  -- if (check && state->reqwrap) state->reqwrap |= 4; else state->reqwrap &= ~4;
1653  let reqwrap := if check != 0 && s.reqwrap != 0 then s.reqwrap ||| 4 else s.reqwrap &&& ~~~4
1654  wrS st fun s => { s with wrap := wrap, reqwrap := reqwrap }
1655  return Z_OK
1656
1657/-- `long ZEXPORT inflateMark(z_streamp strm)` -/
1658def inflateMark (strm : ZStreamPtr) : M Int64 := do
1659  -- if (inflateStateCheck(strm)) return -(1L << 16);
1660  if (← inflateStateCheck strm) != 0 then return -((1 : Int64) <<< 16)
1661  let z ← ldZStream strm
1662  let st ← castInflateState z.state
1663  let s ← ldInflateState st
1664  -- (long)(((unsigned long)((long)state->back)) << 16)
1665  let hi : Int64 := ((s.back.toInt64.toUInt64) <<< 16).toInt64
1666  -- state->mode == COPY ? state->length : (state->mode == MATCH ? state->was - state->length : 0)   (type unsigned)
1667  let lo : UInt32 := if s.mode == COPY then s.length else if s.mode == MATCH then s.was - s.length else 0
1668  chkI64 (hi.toInt + lo.toNat)
1669
1670/-- `unsigned long ZEXPORT inflateCodesUsed(z_streamp strm)` -/
1671def inflateCodesUsed (strm : ZStreamPtr) : M UInt64 := do
1672  -- if (inflateStateCheck(strm)) return (unsigned long)-1;
1673  if (← inflateStateCheck strm) != 0 then return 0xffffffffffffffff
1674  let z ← ldZStream strm
1675  let st ← castInflateState z.state
1676  let s ← ldInflateState st
1677  -- return (unsigned long)(state->next - state->codes);
1678  let d ← Ptr.diff s.next (codesP st)
1679  return d.toUInt64
1680
1681end Zlib.Inflate