Inflate.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Api.Header
2
3/-!
4# API model: the inflate stream
5
6A heap-free model of one `z_stream` used for `inflate`. The model state remembers the whole
7history (all input consumed and all output delivered since the last reset), so that what a call
8may do is stated against the format specification (`Layer.Decodes`), independent of how the
9caller cuts the input and the output room. Every function is a *relation* between the state
10before, the inputs of the call, and the results: zlib does not promise how much input a call
11consumes, only the properties below. `docs/design/api-model.md` explains the choices.
12-/
13
14namespace ZlibF.Spec.Api
15
16open ZlibF.Spec
17
18/-- The mode of an inflate stream as far as the caller can see it. `needDict` is after
19`Z_NEED_DICT`, `done` after `Z_STREAM_END`, `bad` after `Z_DATA_ERROR`, `mem` after `Z_MEM_ERROR`, `syncing` after a failed `inflateSync` (`inflate` then
20returns `Z_STREAM_ERROR` until the pattern is found or the stream is reset). -/
21inductive IPhase where
22  | running | needDict | done | bad | mem | syncing
23  deriving DecidableEq, Repr
24
25/-- The model of an initialised inflate stream.
26
27* `seen`, `out`: all input consumed and all output delivered since init or reset
28  (`total_in`, `total_out` are their lengths, plus what `Reset`/`Sync` keep: see `totalIn`).
29* `dict`: the preset dictionary given to `inflateSetDictionary`.
30* `adler`: the field `strm->adler`.
31* `precise`: the data-level promises apply. It is cleared by operations after which `zlib.h`
32  promises less (priming bits, `inflateSync`, switching the checksum off).
33* `validate`: the checksum is checked (`inflateValidate`).
34* `pre`: bits inserted by `inflatePrime`, read before `seen`.
35* `syncHave`: how much of the pattern `00 00 FF FF` `inflateSync` has matched.
36* `hdrReq`, `hdr`: `inflateGetHeader`'s request and the record that `inflate` filled. -/
37structure InflState where
38  wrap : Wrap
39  wbits : Nat
40  phase : IPhase
41  seen : List UInt8
42  out : List UInt8
43  dict : Option (List UInt8)
44  totalIn : Nat
45  totalOut : Nat
46  adler : UInt32
47  precise : Bool
48  validate : Bool
49  pre : List Bool
50  syncHave : Nat
51  hdrReq : Option HdrReq
52  hdr : Option GzHdrOut
53
54/-- The state after a successful `inflateInit2` or `inflateReset2` with these parameters
55(`inflateResetKeep`: `adler` is `wrap & 1`, the totals are 0). -/
56def InflState.fresh (w : Wrap) (b : Nat) : InflState where
57  wrap := w
58  wbits := b
59  phase := .running
60  seen := []
61  out := []
62  dict := none
63  totalIn := 0
64  totalOut := 0
65  adler := if w = .zlib ∨ w = .auto then 1 else 0
66  precise := true
67  validate := true
68  pre := []
69  syncHave := 0
70  hdrReq := none
71  hdr := none
72
73/-- The data-level promises apply to this state. -/
74def InflState.Exact (st : InflState) : Prop := st.precise = true ∧ st.validate = true
75
76/-- The dictionary the decoder uses: the one supplied, else none. -/
77def InflState.dictEff (st : InflState) : List UInt8 := st.dict.getD []
78
79/-- Dictionaries still available to a legal continuation. A supplied dictionary is fixed.
80A raw stream with no dictionary uses the empty dictionary. A wrapped stream that has not
81received one may still request a preset dictionary: ignorance of that dictionary is not
82evidence that the input is corrupt. Gzip ignores this argument in the format relation. -/
83def InflState.PermitsDictionary (st : InflState) (dictionary : List UInt8) : Prop :=
84  match st.dict with
85  | some known => dictionary = known
86  | none => st.wrap ≠ .raw ∨ dictionary = []
87
88/-- The checksum that `strm->adler` holds for the output `out` of `seen`
89(`A-adler-field`): Adler-32 for zlib, CRC-32 for gzip, nothing promised for raw. For `auto` the
90first two bytes decide. -/
91def checkValue (w : Wrap) (seen out : List UInt8) : Option UInt32 :=
92  match w with
93  | .raw => none
94  | .zlib => some (adler32 out)
95  | .gzip => some (crc32 out)
96  | .auto => if seen.take 2 = [31, 139] then some (crc32 out) else some (adler32 out)
97
98/-- `Consistent x out`: the bytes `x` begin a stream (or are one) that a decoder with this
99configuration accepts, and `out` is a prefix of what that stream decodes to. -/
100def Layer.Consistent (w : Wrap) (wbits : Nat) (dict x out : List UInt8) : Prop :=
101  (x.length < hdrLag w ∧ out = []) ∨
102    ∃ (t o : List UInt8) (n : Nat), x.length ≤ n ∧
103      Layer.Decodes w wbits dict ((x ++ t).take n) o ∧ out <+: o
104
105/-- Output determined by consumed bytes. For every complete stream compatible with the bytes
106already read, the output is a prefix of its decoding. Compatibility includes a stream that ends
107within the consumed bytes, so unread trailing data cannot select a different decoding. This is
108a universal condition: one favourable future continuation is not enough. It does not constrain
109which input the caller may supply, or assume a decoder implementation obeys this condition. -/
110def Layer.Determined (w : Wrap) (wbits : Nat) (dict x out : List UInt8) : Prop :=
111  ∀ (stream decoded : List UInt8), (x <+: stream ∨ stream <+: x) →
112    Layer.Decodes w wbits dict stream decoded → out <+: decoded
113
114/-- Compatibility with a checked bit prefix, including a complete stream ending inside it. -/
115def Layer.BitCompatible (pfx : List Bool) (stream : List UInt8) : Prop :=
116  pfx <+: bytesToBits stream ∨ bytesToBits stream <+: pfx
117
118/-- Some checked prefix of the pulled bytes justifies the output. It has a valid completion,
119and every compatible completion with a still-permitted dictionary has that output prefix.
120The remaining pulled bits can contain an error that has not been checked yet. -/
121def Layer.OutputEvidence (w : Wrap) (wbits : Nat) (allowed : List UInt8 → Prop)
122    (input output : List UInt8) : Prop :=
123  ∃ pfx : List Bool, pfx <+: bytesToBits input ∧
124    (∃ dictionary stream decoded, allowed dictionary ∧ Layer.BitCompatible pfx stream ∧
125      Layer.Decodes w wbits dictionary stream decoded) ∧
126    (∀ dictionary stream decoded, allowed dictionary → Layer.BitCompatible pfx stream →
127      Layer.Decodes w wbits dictionary stream decoded → output <+: decoded)
128
129/-- Nonvacuous causal evidence from checked bits. Pulled lookahead need not have a complete
130valid continuation. A wrapped stream's unknown dictionary is not assumed to be empty. -/
131def InflState.Consistent (st : InflState) (input output : List UInt8) : Prop :=
132  Layer.OutputEvidence st.wrap st.wbits st.PermitsDictionary input output
133
134/-- The bytes already read determine the output for every dictionary still permitted by the
135state. A dictionary not yet supplied cannot be chosen to justify speculative output. -/
136def InflState.Determined (st : InflState) (input output : List UInt8) : Prop :=
137  ∀ dictionary, st.PermitsDictionary dictionary →
138    Layer.Determined st.wrap st.wbits dictionary input output
139
140/-- What one call of `inflate` is given: the input bytes (`avail_in` of them), the room
141`avail_out`, the flush value, and `badBuf` when `next_out` is null or `next_in` is null with
142`avail_in ≠ 0` (the model has no null buffers). -/
143structure InflCall where
144  inp : List UInt8
145  availOut : Nat
146  flush : Flush
147  badBuf : Bool
148
149/-- What one call of `inflate` returns: the number of input bytes consumed, the bytes written, the
150return code. -/
151structure InflOut where
152  consumed : Nat
153  produced : List UInt8
154  rc : Int
155
156/-- The call made progress: it consumed input or produced output. -/
157def InflOut.Progress (o : InflOut) : Prop := 0 < o.consumed ∨ o.produced ≠ []
158
159/-- The record that `inflateGetHeader` asked for, after the bytes `seen'` were read: filled with the
160header if it is complete in `seen'`, else unchanged. -/
161def InflHdrClause (st : InflState) (seen' : List UInt8) (st' : InflState) : Prop :=
162  ∀ req, st.hdrReq = some req → (∃ h, st'.hdr = some h ∧ HeaderRead req seen' h) ∨
163    (¬ ∃ h, HeaderRead req seen' h) ∧ st'.hdr = st.hdr
164
165/-- `inflate(strm, flush)` on a running stream, the outcomes other than `Z_MEM_ERROR`
166(`A-inflate-progress`, `A-inflate-err-data`, `zlib.h` `inflate`). The clauses:
167
1681. *Frame.* It consumes a prefix of the input and writes at most `avail_out` bytes; the history
169   and the totals grow by exactly that; everything else keeps its value, except `adler` and `hdr`.
1702. *Return codes.* `Z_OK` needs progress and no `Z_FINISH`; `Z_BUF_ERROR` is no progress, or
171   `Z_FINISH` that did not finish; the other codes change the mode.
1723. *Soundness* (needs `Exact`). A checked bit prefix justifies the output (`Layer.OutputEvidence`),
173   which is determined by the pulled bytes (`Layer.Determined`), so it must
174   be a prefix of the decoding of every compatible complete stream. `Z_STREAM_END` only for a complete
175   stream with all its output written; `Z_DATA_ERROR` only if the input consumed is not viable
176   (or the window is smaller than 32 KiB: `FullWindow`).
1774. *Stopping.* With input left over, the call stopped because the output is full, or the stream
178   ended or failed, or the flush value asked for a block boundary.
1795. *Liveness* (needs `Exact`, flush `Z_NO_FLUSH`, `Z_SYNC_FLUSH` or `Z_FINISH`, a full window).
180   The call ends the stream if the stream ends within the input and the output fits; it
181   reports a data error that shows at least `detectLag` bytes before the end of the input if
182   there is room left; it returns `Z_NEED_DICT` when the header asks for a dictionary. (In every
183   case `InflRunMem` is the other allowed outcome of such a call.)
1846. *Checksum field.* After the call `adler` is the checksum of the output so far
185   (`checkValue`), once there is output or the stream ended. -/
186def InflRunOk (st : InflState) (c : InflCall) (o : InflOut) (st' : InflState) : Prop :=
187  let all := st.seen ++ c.inp
188  let seen' := st.seen ++ c.inp.take o.consumed
189  let out' := st.out ++ o.produced
190  -- 1. frame
191  o.consumed ≤ c.inp.length ∧ o.produced.length ≤ c.availOut ∧
192  st'.seen = seen' ∧ st'.out = out' ∧
193  st'.totalIn = st.totalIn + o.consumed ∧ st'.totalOut = st.totalOut + o.produced.length ∧
194  st'.wrap = st.wrap ∧ st'.wbits = st.wbits ∧ st'.dict = st.dict ∧ st'.precise = st.precise ∧
195  st'.validate = st.validate ∧ st'.pre = st.pre ∧ st'.syncHave = st.syncHave ∧
196  st'.hdrReq = st.hdrReq ∧
197  -- 2. return codes
198  (o.rc = Z.ok ∨ o.rc = Z.streamEnd ∨ o.rc = Z.needDict ∨ o.rc = Z.dataError ∨
199    o.rc = Z.bufError) ∧
200  (o.rc = Z.ok → o.Progress ∧ c.flush ≠ .finish ∧ st'.phase = .running) ∧
201  (o.rc = Z.bufError → (¬ o.Progress ∨ c.flush = .finish) ∧ st'.phase = .running) ∧
202  (o.rc = Z.streamEnd → st'.phase = .done) ∧
203  (o.rc = Z.dataError → st'.phase = .bad) ∧
204  (o.rc = Z.needDict → st'.phase = .needDict ∧ o.produced = [] ∧ st.dict = none ∧
205    seen'.length = 6 ∧ HdrNeedsDict st.wrap st.wbits seen') ∧
206  -- 3. soundness
207  (st.Exact → (o.rc = Z.ok ∨ o.rc = Z.bufError) →
208    st.Consistent seen' out') ∧
209  (st.Exact → o.rc = Z.streamEnd → Layer.Decodes st.wrap st.wbits st.dictEff seen' out') ∧
210  (st.Exact → o.rc = Z.dataError → FullWindow st.wrap st.wbits all →
211    ∀ dictionary, st.PermitsDictionary dictionary →
212      ¬ Layer.Viable st.wrap st.wbits dictionary seen') ∧
213  -- 4. stopping
214  (o.consumed < c.inp.length →
215    o.produced.length = c.availOut ∨ o.rc = Z.streamEnd ∨ o.rc = Z.dataError ∨
216    o.rc = Z.needDict ∨ c.flush = .block ∨ c.flush = .trees) ∧
217  -- 5. liveness
218  (st.Exact → (c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish) →
219    FullWindow st.wrap st.wbits all →
220    (st.dict = none → ¬ HdrNeedsDict st.wrap st.wbits all) →
221    (∃ (n : Nat) (o' : List UInt8), st.seen.length ≤ n ∧ n ≤ all.length ∧
222        Layer.Decodes st.wrap st.wbits st.dictEff (all.take n) o' ∧ st.out <+: o' ∧
223        o'.length ≤ st.out.length + c.availOut) →
224    o.rc = Z.streamEnd) ∧
225  (st.Exact → (c.flush = .noFlush ∨ c.flush = .syncFlush ∨ c.flush = .finish) →
226    (st.dict = none → ¬ HdrNeedsDict st.wrap st.wbits all) →
227    Layer.Detectable st.wrap st.wbits st.dictEff all → o.produced.length < c.availOut →
228    o.rc = Z.dataError) ∧
229  (st.dict = none → st.seen.length < 6 → 6 ≤ all.length → HdrNeedsDict st.wrap st.wbits all →
230    o.rc = Z.needDict ∧ o.consumed = 6 - st.seen.length) ∧
231  -- 6. checksum field
232  (st.Exact → (checkValue st.wrap seen' out').isSome → (out' ≠ [] ∨ o.rc = Z.streamEnd) →
233    some st'.adler = checkValue st.wrap seen' out') ∧
234  -- Consistency with one possible future does not permit guessing output from unread input.
235  (st.Exact → (o.rc = Z.ok ∨ o.rc = Z.bufError) →
236    st.Determined seen' out') ∧
237  -- header record
238  InflHdrClause st seen' st'
239
240/-- `inflate(strm, flush)` on a running stream, the outcome `Z_MEM_ERROR` (`inflate.c`, `inf_leave`:
241`updatewindow` fails to allocate the window, `mode = MEM`, and the function returns *before* it
242updates `total_in`, `total_out` and `adler`). The call has read input and written output
243(`consumed`, `produced`, as `avail_in` and `avail_out` show; `produced` is not empty, since the window
244is allocated only when output was written), but the totals and `adler` keep their old values.
245The stream is in the state `mem`: every later `inflate` returns `Z_MEM_ERROR`, and only `inflateEnd`,
246`inflateReset` and `inflateReset2` are meaningful. The data written is correct (a prefix of the
247decoding). Checked against the real library with a window allocation that fails. -/
248def InflRunMem (st : InflState) (c : InflCall) (o : InflOut) (st' : InflState) : Prop :=
249  let seen' := st.seen ++ c.inp.take o.consumed
250  let out' := st.out ++ o.produced
251  o.rc = Z.memError ∧ o.consumed ≤ c.inp.length ∧ o.produced.length ≤ c.availOut ∧ o.produced ≠ [] ∧
252  st'.phase = .mem ∧ st'.seen = seen' ∧ st'.out = out' ∧
253  st'.totalIn = st.totalIn ∧ st'.totalOut = st.totalOut ∧ st'.adler = st.adler ∧
254  st'.wrap = st.wrap ∧ st'.wbits = st.wbits ∧ st'.dict = st.dict ∧ st'.precise = st.precise ∧
255  st'.validate = st.validate ∧ st'.pre = st.pre ∧ st'.syncHave = st.syncHave ∧
256  st'.hdrReq = st.hdrReq ∧
257  (st.Exact → st.Consistent seen' out') ∧
258  (st.Exact → st.Determined seen' out') ∧
259  InflHdrClause st seen' st'
260
261/-- `inflate(strm, flush)` on a running stream: one of the two outcomes above. -/
262def InflRun (st : InflState) (c : InflCall) (o : InflOut) (st' : InflState) : Prop :=
263  InflRunOk st c o st' ∨ InflRunMem st c o st'
264
265/-- The real raw decoder emits A and fills one output byte before checking the pending bad
266distance. It consumes three bytes and returns OK; a later call returns DATA_ERROR. -/
267def Goal.inflate_deferred_distance : Prop :=
268  ∃ after, InflRunOk (InflState.fresh .raw 15)
269    ⟨[115, 4, 66, 0], 1, .noFlush, false⟩ ⟨3, [65], Z.ok⟩ after
270
271/-- `inflate(strm, flush)` for any stream state (`zlib.h`; `inflate.c` start of `inflate` and the
272modes `DONE`, `BAD`, `MEM`, `DICT`):
273a bad buffer is `Z_STREAM_ERROR`; a finished stream keeps returning `Z_STREAM_END`, a failed one
274`Z_DATA_ERROR`, one out of memory `Z_MEM_ERROR`, one waiting for a dictionary `Z_NEED_DICT`,
275one in the sync search `Z_STREAM_ERROR`, all without consuming or producing anything. -/
276def InflStep (st : InflState) (c : InflCall) (o : InflOut) (st' : InflState) : Prop :=
277  (c.badBuf = true → o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st) ∧
278  (c.badBuf = false →
279    match st.phase with
280    | .running => InflRun st c o st'
281    | .done => o.rc = Z.streamEnd ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st
282    | .bad => o.rc = Z.dataError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st
283    | .mem => o.rc = Z.memError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st
284    | .needDict => o.rc = Z.needDict ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st
285    | .syncing => o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st)
286
287/-! ## The other inflate functions
288
289Each is a relation `rc`, `st'` for the state before `st`; a call that fails leaves the state
290unchanged unless said otherwise. -/
291
292/-- `inflateInit2_` / `inflateInit_` (`windowBits` 15): the result code and the new stream.
293`versionOK` says that the version string and the structure size are the library's. `Z_MEM_ERROR`
294is the failure of an allocation; then there is no stream. -/
295def InflInit (wb : Int) (versionOK : Bool) (rc : Int) (r : Option InflState) : Prop :=
296  if versionOK = false then rc = Z.versionError ∧ r = none
297  else match inflWbits wb with
298    | none => rc = Z.streamError ∧ r = none
299    | some (w, b) => (rc = Z.ok ∧ r = some (InflState.fresh w b)) ∨ (rc = Z.memError ∧ r = none)
300
301/-- `inflateReset2(strm, windowBits)`: forgets all data (history, dictionary, header request);
302`total_in`, `total_out` are 0. A bad `windowBits` is `Z_STREAM_ERROR` and changes nothing.
303`inflateReset` is `windowBits` of the stream (`InflReset`). -/
304def InflReset2 (st : InflState) (wb : Int) (rc : Int) (st' : InflState) : Prop :=
305  match inflWbits wb with
306  | none => rc = Z.streamError ∧ st' = st
307  | some (w, b) => rc = Z.ok ∧ st' = InflState.fresh w b
308
309/-- `inflateReset(strm)`: as `InflReset2` with the configuration the stream was last given. -/
310def InflReset (st : InflState) (rc : Int) (st' : InflState) : Prop :=
311  rc = Z.ok ∧ st' = InflState.fresh st.wrap st.wbits
312
313/-- `inflateEnd(strm)`: succeeds and ends the stream (the model has no further state). -/
314def InflEnd (_st : InflState) (rc : Int) : Prop := rc = Z.ok
315
316/-- `inflatePrime(strm, bits, value)`: `bits = 0` does nothing; `bits < 0` clears the bit buffer;
317`bits > 16`, or more than 32 bits in the buffer, is `Z_STREAM_ERROR`. Otherwise the `bits` low
318bits of `value` are put in front of the pending input, and the data-level promises stop
319(`precise := false`). The bits in the buffer are known exactly only while no input has been
320consumed; afterwards `Z_STREAM_ERROR` is allowed when the buffer may be full
321(`zlib.h`: "inflatePrime"). -/
322def InflPrime (st : InflState) (bits value : Int) (rc : Int) (st' : InflState) : Prop :=
323  if bits = 0 then rc = Z.ok ∧ st' = st
324  else if bits < 0 then rc = Z.ok ∧ st' = { st with pre := [] }
325  else if bits > 16 then rc = Z.streamError ∧ st' = st
326  else if st.seen = [] ∧ st.pre.length + bits.toNat > 32 then rc = Z.streamError ∧ st' = st
327  else (rc = Z.ok ∧
328      st' = { st with pre := st.pre ++ (List.range bits.toNat).map (fun i => (value % (2 ^ bits.toNat : Int)).toNat.testBit i),
329                      precise := false }) ∨
330    (st.seen ≠ [] ∧ rc = Z.streamError ∧ st' = st)
331
332/-- `inflateSetDictionary(strm, dict, len)`. A stream with a zlib header accepts it only after
333`Z_NEED_DICT`, and checks its Adler-32 against the `DICTID` read from the header
334(`Z_DATA_ERROR` if different). A raw stream accepts it before any input is consumed; zlib also
335accepts it later (it then amends the window), which this model leaves out (`seen = []`). -/
336def InflSetDict (st : InflState) (d : List UInt8) (rc : Int) (st' : InflState) : Prop :=
337  match st.wrap with
338  | .raw => st.seen = [] ∧ ((rc = Z.ok ∧ st' = { st with dict := some d }) ∨
339      (rc = Z.memError ∧ st' = { st with phase := .mem }))
340  | _ =>
341    if st.phase = .needDict then
342      if st.seen.drop 2 = be32 (adler32 d).toNat then
343        (rc = Z.ok ∧ st' = { st with dict := some d, phase := .running }) ∨
344        (rc = Z.memError ∧ st' = { st with phase := .mem })
345      else rc = Z.dataError ∧ st' = st
346    else rc = Z.streamError ∧ st' = st
347
348/-- The window size in bytes, when the configuration fixes it (`wbits ≠ 0`). -/
349def InflState.winSize (st : InflState) : Nat := 2 ^ st.wbits
350
351/-- `inflateGetDictionary(strm, buf, &len)`: `Z_OK`. While the stream is running with a fixed window
352size, the dictionary returned is a suffix of the dictionary and the output so far, at most the window.
353(It is exactly the last `min(window, history)` bytes unless the last call was `Z_FINISH` and ended
354inside the trailer, when the window is not updated; the model does not track that.) -/
355def InflGetDict (st : InflState) (buf : List UInt8) (rc : Int) : Prop :=
356  rc = Z.ok ∧ (st.phase = .running → st.wbits ≠ 0 →
357    buf <:+ (st.dictEff ++ st.out) ∧ buf.length ≤ st.winSize)
358
359/-- One byte of `syncsearch` (`inflate.c`): `got` bytes of the pattern `00 00 FF FF` are matched. -/
360def syncStep (got : Nat) (b : UInt8) : Nat :=
361  if b = (if got < 2 then 0 else 255) then got + 1 else if b ≠ 0 then 0 else 4 - got
362
363/-- `syncsearch(&have, buf, len)`: the new `have` and the number of bytes looked at. -/
364def syncSearch : Nat → List UInt8 → Nat × Nat
365  | got, [] => (got, 0)
366  | got, b :: r =>
367    if got < 4 then
368      let p := syncSearch (syncStep got b) r
369      (p.1, p.2 + 1)
370    else (got, 0)
371
372/-- `inflateSync(strm)` on the input `inp` (`avail_in` bytes; the bit buffer is assumed to hold
373less than a byte): `Z_BUF_ERROR` if there is no input. Otherwise the input is searched with
374`syncSearch`, starting from the partial match of an earlier failed call. If the pattern is
375found, `Z_OK`, the input up to and including it is consumed, the stream is reset as by
376`inflateReset` but the totals are kept, and the data-level promises stop. If not, `Z_DATA_ERROR`,
377all the input is consumed and the stream is in the sync search (`syncing`). -/
378def InflSync (st : InflState) (inp : List UInt8) (consumed : Nat) (rc : Int) (st' : InflState) :
379    Prop :=
380  if inp = [] then rc = Z.bufError ∧ consumed = 0 ∧ st' = st
381  else
382    let r := syncSearch (if st.phase = .syncing then st.syncHave else 0) inp
383    consumed = r.2 ∧
384    (if r.1 = 4 then
385      rc = Z.ok ∧ st' = { InflState.fresh st.wrap st.wbits with
386                totalIn := st.totalIn + consumed, totalOut := st.totalOut, precise := false,
387                adler := st.adler }
388    else
389      rc = Z.dataError ∧
390        st' = { st with phase := .syncing, syncHave := r.1, totalIn := st.totalIn + consumed })
391
392/-- `inflateSyncPoint(strm)`: 0 or 1, never an error for a valid stream. The model promises that
393a stream that has consumed nothing, has ended or has failed is not at a sync point. -/
394def InflSyncPoint (st : InflState) (r : Int) : Prop :=
395  (r = 0 ∨ r = 1) ∧ ((st.seen = [] ∨ st.phase ≠ .running) → r = 0)
396
397/-- `inflateCopy(dest, source)`: `dest` becomes an independent copy of the same model state
398(`C6`); `Z_MEM_ERROR` leaves `dest` without a state. -/
399def InflCopy (st : InflState) (rc : Int) (dest : Option InflState) : Prop :=
400  (rc = Z.ok ∧ dest = some st) ∨ (rc = Z.memError ∧ dest = none)
401
402/-- `inflateGetHeader(strm, head)`: only for a gzip or automatic stream (`Z_STREAM_ERROR`
403otherwise). It must be called before the first `inflate`; the model requires `seen = []`.
404`head->done` is 0 until `inflate` completes the header. -/
405def InflGetHeader (st : InflState) (req : HdrReq) (rc : Int) (st' : InflState) : Prop :=
406  if st.wrap = .raw ∨ st.wrap = .zlib then rc = Z.streamError ∧ st' = st
407  else st.seen = [] ∧ rc = Z.ok ∧ st' = { st with hdrReq := some req, hdr := none }
408
409/-- `inflateUndermine(strm, subvert)`: in the default build (without
410`INFLATE_ALLOW_INVALID_DISTANCE_TOOFAR_ARRR`) it returns `Z_DATA_ERROR` and changes nothing. -/
411def InflUndermine (st : InflState) (_subvert : Int) (rc : Int) (st' : InflState) : Prop :=
412  rc = Z.dataError ∧ st' = st
413
414/-- `inflateValidate(strm, check)`: switches checking of the trailer on or off; the data-level
415promises hold only while it is on and was on from the start. -/
416def InflValidate (st : InflState) (check : Int) (rc : Int) (st' : InflState) : Prop :=
417  rc = Z.ok ∧ st' = { st with validate := decide (check ≠ 0) , precise := st.precise && st.validate }
418
419/-- `inflateMark(strm)`: upper 16 bits and lower 16 bits as in `zlib.h`. Note that `-65536` is
420both the answer for an inconsistent stream and "upper -1, lower 0" (outside a block). The model
421promises only that a stream that has consumed nothing is outside a block. -/
422def InflMark (st : InflState) (v : Int) : Prop :=
423  (st.seen = [] → st.pre = [] → v = -65536)
424
425/-! ## `inflateBack`: callbacks as a function parameter -/
426
427/-- The callbacks of `inflateBack`: the buffer returned by the `k`-th call of `in` (`[]` means "no
428input": `inflateBack` then returns `Z_BUF_ERROR`), and whether the `k`-th call of `out` fails. -/
429structure BackCallbacks where
430  input : Nat → List UInt8
431  outFails : Nat → Bool
432
433/-- What `inflateBack` did: the buffers passed to `out` in order, the return code, the unused
434part of the last input buffer, and whether `strm->next_in` is `Z_NULL` (set when `in` returned
435nothing). -/
436structure BackResult where
437  chunks : List (List UInt8)
438  rc : Int
439  unused : List UInt8
440  nextInNull : Bool
441
442/-- `inflateBack(strm, in, in_desc, out, out_desc)` for a stream initialised with `windowBits`
443`wb` (8 to 15), with the first input `first` (`strm->next_in`, `avail_in`) and the callbacks
444`cb` (`zlib.h`). The stream read is a raw deflate stream. The consumed input is `first` followed by
445whole buffers of `cb.input 0, cb.input 1, ...` minus `unused` at the end.
446
447* `Z_OK` is never returned (the return code is one of the three below).
448* `Z_STREAM_END`: the consumed input is exactly one raw deflate stream; the buffers given to `out`
449  concatenate to its decoding; each buffer has at most `2^wb` bytes.
450* `Z_DATA_ERROR`: the consumed input is not viable (or the window is smaller than 32 KiB, where
451  a valid stream with a far distance may be refused).
452* `Z_BUF_ERROR`: `in` returned nothing (and `next_in` is null), or `out` failed.
453
454In all cases the buffers passed to `out` (the last one may be the one that failed) concatenate to
455a prefix of what the input consumed so far decodes to (soundness). -/
456def InflBack (wb : Nat) (first : List UInt8) (cb : BackCallbacks) (r : BackResult) : Prop :=
457  8 ≤ wb ∧ wb ≤ 15 ∧
458  (r.rc = Z.streamEnd ∨ r.rc = Z.dataError ∨ r.rc = Z.bufError) ∧
459  (∀ ch, ch ∈ r.chunks → ch.length ≤ 2 ^ wb) ∧
460  ∃ (k : Nat) (consumed : List UInt8),
461    consumed ++ r.unused = first ++ ((List.range k).map cb.input).flatten ∧
462    r.unused.length ≤ (if k = 0 then first else cb.input (k - 1)).length ∧
463    (r.rc = Z.streamEnd → Deflate.Decodes [] consumed r.chunks.flatten) ∧
464    (r.rc = Z.dataError → wb = 15 → ¬ Layer.Viable .raw wb [] consumed) ∧
465    (r.rc = Z.bufError →
466      (r.nextInNull = true ∧ cb.input k = []) ∨ (r.nextInNull = false ∧ ∃ i, cb.outFails i = true)) ∧
467    ∃ m, m ≤ consumed.length ∧ Layer.Consistent .raw wb [] (consumed.take m) r.chunks.flatten
468
469end ZlibF.Spec.Api