Deflate.lean

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

1import ZlibF.Spec.Api.Inflate
2
3/-!
4# API model: the deflate stream
5
6A heap-free model of one `z_stream` used for `deflate`, in the same style as `Inflate.lean`:
7the state remembers the whole input accepted and the whole output delivered, and a call is a
8relation between the state before, the inputs, and the results. What the compressor chooses
9(block boundaries, match lengths, how much input a call takes before the output is full) is not
10specified; what `zlib.h` promises is.
11-/
12
13namespace ZlibF.Spec.Api
14
15open ZlibF.Spec
16
17/-- The model of an initialised deflate stream.
18
19* `input`, `produced`: all input accepted and all output delivered since init or reset.
20* `dict`: the preset dictionary; `hdr`: the header given to `deflateSetHeader`.
21* `pend`, `bits`: bytes and bits the library holds and has not delivered (`deflatePending`).
22* `last`: the flush value of the previous call (`last_flush`; -2 after init, -1 after a call
23  that filled the output).
24* `finishing`: `Z_FINISH` was accepted. `done`: the whole stream, trailer included, was delivered.
25* `started`: a call got past the argument checks (the header is being written).
26* `clean`: nothing since init changed the stream except input and `Z_FINISH`, so that
27  `deflateBound` applies. `precise`: the data-level promises apply (cleared by priming bits, by
28  setting a dictionary or a header at a time that `zlib.h` does not allow).
29* `fullAt`: lengths of `produced` and `input` at the last completed `Z_FULL_FLUSH`. -/
30structure DeflState where
31  params : DeflParams
32  dict : Option (List UInt8)
33  hdr : Option GzHead
34  input : List UInt8
35  produced : List UInt8
36  totalIn : Nat
37  totalOut : Nat
38  adler : UInt32
39  pend : Nat
40  bits : Nat
41  last : Int
42  finishing : Bool
43  done : Bool
44  started : Bool
45  clean : Bool
46  precise : Bool
47  fullAt : Option (Nat × Nat)
48
49/-- The state after `deflateInit2` / `deflateReset` (`deflateResetKeep`: `adler` is the CRC-32 or
50Adler-32 of nothing, `last_flush = -2`, no header, no dictionary). -/
51def DeflState.fresh (p : DeflParams) : DeflState where
52  params := p
53  dict := none
54  hdr := none
55  input := []
56  produced := []
57  totalIn := 0
58  totalOut := 0
59  adler := if p.wrap = .gzip then 0 else 1
60  pend := 0
61  bits := 0
62  last := -2
63  finishing := false
64  done := false
65  started := false
66  clean := true
67  precise := true
68  fullAt := none
69
70/-- The dictionary as the format specification takes it (none: empty). -/
71def DeflState.dictEff (st : DeflState) : List UInt8 := st.dict.getD []
72
73/-- The header record that is written: the one set, else the default. -/
74def DeflState.header (st : DeflState) : GzHead := st.hdr.getD GzHead.default
75
76/-- `deflateBound(strm, n)` (`deflate.c`), without the overflow clamp (the argument is below
77`2^60`): wrapper length, then one of three bounds. -/
78def DeflState.bound (st : DeflState) (n : Nat) : Nat :=
79  let p := st.params
80  let fixedlen := n + n / 8 + n / 256 + n / 512 + 4
81  let storelen := n + n / 32 + n / 128 + n / 2048 + 7
82  let h := st.header
83  let wraplen :=
84    match p.wrap with
85    | .raw => 0
86    | .zlib => 6 + (if st.dictEff ≠ [] then 4 else 0)
87    | .gzip =>
88      18 + (if st.hdr.isNone then 0 else
89        (match h.extra with | some e => 2 + e.length | none => 0) +
90        (match h.name with | some s => s.length + 1 | none => 0) +
91        (match h.comment with | some s => s.length + 1 | none => 0) +
92        (if h.hcrc then 2 else 0))
93  if p.wbits ≠ 15 ∨ p.memLevel + 7 ≠ 15 then
94    (if p.wbits ≤ p.memLevel + 7 ∧ p.level ≠ 0 then fixedlen else storelen) + wraplen
95  else n + n / 4096 + n / 16384 + n / 2 ^ 25 + 13 - 6 + wraplen
96
97/-- The compression function class of a level (`configuration_table`): 0 stored, 1 fast
98(levels 1 to 3), 2 lazy (levels 4 to 9). -/
99def funcOf (level : Nat) : Nat := if level = 0 then 0 else if level ≤ 3 then 1 else 2
100
101/-- `F-deflate-valid` for the configuration of a stream: `produced` is a complete stream of the
102stream's layer for `input` (with the stream's dictionary and header; the zlib header announces
103the stream's window and has `FDICT` set exactly when the dictionary is not empty). -/
104def DeflState.Valid (st : DeflState) (produced input : List UInt8) : Prop :=
105  match st.params.wrap with
106  | .raw => Deflate.Decodes (st.dictEff.drop (st.dictEff.length - 2 ^ st.params.wbits)) produced input
107  | .zlib => Zlib.Decodes st.dictEff produced input ∧
108      produced.head?.map (·.toNat / 16 + 8) = some st.params.wbits ∧
109      ∃ cmf flg r, produced = cmf :: flg :: r ∧ (flg.toNat / 32 % 2 = 1 ↔ st.dictEff ≠ [])
110  | .gzip => Gzip.DecodesWith (st.header.bytes st.params) produced input
111
112/-- The stream that follows the output of a complete sync or full flush, closing the stream
113without more data: an empty final fixed block (`03 00`) and the trailer of the layer. -/
114def closer (w : DWrap) (input : List UInt8) : List UInt8 :=
115  [3, 0] ++ (match w with
116    | .raw => []
117    | .zlib => be32 (adler32 input).toNat
118    | .gzip => le32 (crc32 input).toNat ++ le32 (input.length % 2 ^ 32))
119
120/-- `F-deflate-flush`: after a completed `Z_SYNC_FLUSH` or `Z_FULL_FLUSH`, the output so far
121followed by `closer` is a valid stream of all input so far; in other words the output ends on a
122byte boundary with an empty stored block, and a decoder that gets exactly this output can recover
123all the input. -/
124def DeflState.FlushedAt (st : DeflState) (produced input : List UInt8) : Prop :=
125  st.Valid (produced ++ closer st.params.wrap input) input
126
127/-- What one call of `deflate` is given. `badBuf`: `next_out` is null or `next_in` is null with
128`avail_in ≠ 0`. -/
129structure DeflCall where
130  inp : List UInt8
131  availOut : Nat
132  flush : Flush
133  badBuf : Bool
134
135/-- What one call of `deflate` returns. -/
136structure DeflOut where
137  consumed : Nat
138  produced : List UInt8
139  rc : Int
140
141/-- The checksum that `strm->adler` holds once input has been accepted: Adler-32 for zlib,
142CRC-32 for gzip. -/
143def DeflState.check (st : DeflState) (input : List UInt8) : Option UInt32 :=
144  match st.params.wrap with
145  | .raw => none | .zlib => some (adler32 input) | .gzip => some (crc32 input)
146
147/-- The part of the effect of `deflate` and `deflateParams` that is just bookkeeping: input
148accepted, output delivered, totals, and the fields that do not change (`fullAt` is not among
149them: a completed full flush sets it). -/
150def DeflFrame (st : DeflState) (c : DeflCall) (o : DeflOut) (st' : DeflState) : Prop :=
151  o.consumed ≤ c.inp.length ∧ o.produced.length ≤ c.availOut ∧
152  st'.input = st.input ++ c.inp.take o.consumed ∧ st'.produced = st.produced ++ o.produced ∧
153  st'.totalIn = st.totalIn + o.consumed ∧ st'.totalOut = st.totalOut + o.produced.length ∧
154  st'.dict = st.dict ∧ st'.hdr = st.hdr
155
156/-- `deflate(strm, flush)` once it got past the argument checks, with room, on a stream
157(`zlib.h` `deflate`, `A-deflate-flush`, `F-deflate-valid`, `F-deflate-flush`, `A-deflate-bound`):
158
1591. *Frame*: `DeflFrame`; the parameters do not change; once `started` is set, a call cannot
160   clear it, including a refused call. The checksum field is the checksum of the input accepted
161   so far once the call returned `Z_OK` or `Z_STREAM_END`.
1622. *Refused calls*: a repeated flush without new input is `Z_BUF_ERROR` and nothing else happens;
163   after `Z_FINISH`, new input is refused and nothing is consumed.
1643. *Return codes*: input is left over only if the output is full; `Z_FINISH` with `Z_OK` means the
165   output is full; `Z_STREAM_END` only for `Z_FINISH` with all input consumed and the whole
166   stream delivered, and it is a valid stream of the input (`Valid`), no longer than `bound`
167   (if `clean`); for raw deflate, what follows a completed full flush is a valid stream by itself
168   (the full flush forgets the history); a complete sync or full flush (`Z_OK` with room left) consumed all input and
169   leaves nothing pending, on a byte boundary (`FlushedAt`); every complete flush consumed
170   all input.
1714. *Liveness*: `Z_FINISH` with enough room for the bound ends the stream.
172
173The promises about the content need `precise`. -/
174def DeflRun (st : DeflState) (c : DeflCall) (o : DeflOut) (st' : DeflState) : Prop :=
175  let input' := st.input ++ c.inp.take o.consumed
176  let produced' := st.produced ++ o.produced
177  -- 1. frame
178  DeflFrame st c o st' ∧ st'.params = st.params ∧ st'.precise = st.precise ∧
179  (o.rc = Z.ok ∨ o.rc = Z.streamEnd → st'.started = true ∧
180    ∀ v, st.check input' = some v → st'.adler = v) ∧
181  (o.rc = Z.ok ∨ o.rc = Z.streamEnd ∨ o.rc = Z.bufError) ∧
182  -- 2. refused calls
183  ((st.pend = 0 ∧ c.inp = [] ∧ c.flush ≠ .finish ∧ Flush.rank c.flush.code ≤ Flush.rank st.last) →
184    o.rc = Z.bufError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = { st with last := c.flush.code }) ∧
185  (st.finishing = true → c.inp ≠ [] → o.consumed = 0 ∧
186    (o.rc = Z.bufError ∨ (o.rc = Z.ok ∧ o.produced.length = c.availOut))) ∧
187  -- 3. return codes
188  (o.rc = Z.ok → o.consumed < c.inp.length → o.produced.length = c.availOut) ∧
189  (o.rc = Z.ok → c.flush = .finish → o.produced.length = c.availOut) ∧
190  (o.rc = Z.streamEnd → c.flush = .finish ∧ o.consumed = c.inp.length ∧ st'.done = true ∧
191    st'.finishing = true ∧ st'.pend = 0 ∧ st'.bits = 0 ∧
192    (st.precise = true → st.Valid produced' input') ∧
193    (st.precise = true → st.params.wrap = .raw → st.dict = none → ∀ pl il,
194      st.fullAt = some (pl, il) → Deflate.Decodes [] (produced'.drop pl) (input'.drop il)) ∧
195    (st.clean = true → produced'.length ≤ st.bound input'.length)) ∧
196  (o.rc = Z.ok → o.produced.length < c.availOut →
197    (c.flush = .partialFlush ∨ c.flush = .syncFlush ∨ c.flush = .fullFlush ∨ c.flush = .block) →
198    o.consumed = c.inp.length ∧ st'.pend = 0 ∧ st'.clean = false) ∧
199  (o.rc = Z.ok → o.produced.length < c.availOut →
200    (c.flush = .syncFlush ∨ c.flush = .fullFlush) →
201    st'.bits = 0 ∧ (st.precise = true → st.FlushedAt produced' input')) ∧
202  (o.rc = Z.ok → o.produced.length < c.availOut → c.flush = .fullFlush →
203    st'.fullAt = some (produced'.length, input'.length)) ∧
204  (¬ (o.rc = Z.ok ∧ o.produced.length < c.availOut ∧ c.flush = .fullFlush) →
205    st'.fullAt = st.fullAt) ∧
206  -- the end of the stream
207  (st'.done = true ↔ (st.done = true ∨ o.rc = Z.streamEnd)) ∧
208  (c.flush ≠ .finish → st'.finishing = st.finishing) ∧
209  (o.rc = Z.bufError → o.consumed = 0 ∧ st'.finishing = st.finishing) ∧
210  (st.done = true → o.consumed = 0 ∧ o.produced = []) ∧
211  (st.done = true → c.inp = [] → c.flush = .finish → o.rc = Z.streamEnd) ∧
212  -- the bound applies only to a stream that was fed input and `Z_FINISH` only
213  (st'.clean = true → st.clean = true) ∧
214  (c.flush ≠ .noFlush → c.flush ≠ .finish → o.rc ≠ Z.bufError → st'.clean = false) ∧
215  (c.flush = .noFlush → st'.clean = st.clean) ∧
216  -- A refusal does not erase the history of the already-written wrapper.
217  (st.started = true → st'.started = true) ∧
218  -- 4. liveness
219  (c.flush = .finish → st.clean = true → st.precise = true → st.finishing = false → st.done = false →
220    st.bound (st.input.length + c.inp.length) ≤ st.produced.length + c.availOut →
221    o.rc = Z.streamEnd)
222
223/-- `deflate(strm, flush)` (`deflate.c`, start of `deflate`): `Z_TREES` is not a deflate flush
224value, a bad buffer, or a flush other than `Z_FINISH` after `Z_FINISH`, is `Z_STREAM_ERROR`;
225no room (`avail_out = 0`) is `Z_BUF_ERROR`; all without changing the state. -/
226def DeflStep (st : DeflState) (c : DeflCall) (o : DeflOut) (st' : DeflState) : Prop :=
227  (c.flush = .trees →
228    o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st) ∧
229  (c.flush ≠ .trees →
230    (c.badBuf = true ∨ (st.finishing = true ∧ c.flush ≠ .finish)) →
231      o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st) ∧
232  (c.flush ≠ .trees → c.badBuf = false → ¬ (st.finishing = true ∧ c.flush ≠ .finish) →
233    c.availOut = 0 → o.rc = Z.bufError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st) ∧
234  (c.flush ≠ .trees → c.badBuf = false → ¬ (st.finishing = true ∧ c.flush ≠ .finish) →
235    c.availOut ≠ 0 → DeflRun st c o st')
236
237/-! ## The other deflate functions -/
238
239/-- `deflateInit2_` / `deflateInit_`: the result and the new stream. `Z_MEM_ERROR` is an
240allocation failure (then there is no stream and nothing stays allocated). -/
241def DeflInit (level method wbits memLevel strategy : Int) (versionOK : Bool) (rc : Int)
242    (r : Option DeflState) : Prop :=
243  if versionOK = false then rc = Z.versionError ∧ r = none
244  else match deflInit? level method wbits memLevel strategy with
245    | none => rc = Z.streamError ∧ r = none
246    | some p => (rc = Z.ok ∧ r = some (DeflState.fresh p)) ∨ (rc = Z.memError ∧ r = none)
247
248/-- `deflateReset(strm)`: forgets all data, the dictionary and the header, keeps the parameters
249(`Z_OK`). The parameters are those last set by `deflateParams`. -/
250def DeflReset (st : DeflState) (rc : Int) (st' : DeflState) : Prop :=
251  rc = Z.ok ∧ st' = DeflState.fresh st.params
252
253/-- `deflateEnd(strm)`: `Z_DATA_ERROR` only if the stream is freed while it is busy, that is
254after a call that started it and before `Z_FINISH`; `Z_OK` if it never started or finished. -/
255def DeflEnd (st : DeflState) (rc : Int) : Prop :=
256  (rc = Z.ok ∨ rc = Z.dataError) ∧ ((st.started = false ∨ st.finishing = true) → rc = Z.ok)
257
258/-- `deflateParams(strm, level, strategy)` with the input and the output room that the stream
259has at the time of the call. If the strategy or the compression function changes after the
260stream started, zlib first completes the current block (`deflate(strm, Z_BLOCK)`), into the
261output room and from the input that is there. It then returns `Z_OK` with the new parameters
262(all input accepted), or `Z_BUF_ERROR` with the old ones. An invalid level or strategy is
263`Z_STREAM_ERROR`. The model: if no flush is needed, nothing is consumed or produced. -/
264def DeflParamsFn (st : DeflState) (level strategy : Int) (c : DeflCall) (o : DeflOut)
265    (st' : DeflState) : Prop :=
266  let level' : Int := if level = -1 then 6 else level
267  if level' < 0 ∨ level' > 9 ∨ strategy < 0 ∨ strategy > 4 then
268    o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st
269  else
270    let p' := { st.params with level := level'.toNat, strategy := strategy.toNat }
271    if (strategy.toNat ≠ st.params.strategy ∨ funcOf level'.toNat ≠ funcOf st.params.level) ∧
272        st.last ≠ -2 then
273      (st.finishing = true ∧ o.rc = Z.streamError ∧ o.consumed = 0 ∧ o.produced = [] ∧ st' = st) ∨
274      (st.finishing = false ∧ DeflFrame st c o st' ∧ st'.fullAt = st.fullAt ∧ st'.clean = false ∧
275        ((o.rc = Z.ok ∧ o.consumed = c.inp.length ∧ st'.params = p') ∨
276         (o.rc = Z.bufError ∧ st'.params = st.params)))
277    else
278      o.rc = Z.ok ∧ o.consumed = 0 ∧ o.produced = [] ∧
279        st' = { st with params := p', clean := false }
280
281/-- `deflateTune(strm, ...)`: `Z_OK`; only the choice of matches changes (not modelled), and
282`deflateBound` no longer applies. -/
283def DeflTune (st : DeflState) (rc : Int) (st' : DeflState) : Prop :=
284  rc = Z.ok ∧ st' = { st with clean := false }
285
286/-- `deflateBound(strm, n)`: the value `DeflState.bound`, an upper bound on the size of the
287complete output for `n` bytes of input (`DeflRun`, clause 3). -/
288def DeflBound (st : DeflState) (n r : Nat) : Prop := r = st.bound n
289
290/-- `deflateSetDictionary(strm, dict, len)`. Not for gzip (`Z_STREAM_ERROR`); for zlib only
291before the first `deflate`, and then the adler field becomes the Adler-32 of the dictionary (the
292`DICTID`) and the dictionary becomes the preset dictionary. For raw deflate it is allowed
293when no accepted input is still unflushed; the model gives the data-level promises only when
294no input has been accepted. -/
295def DeflSetDict (st : DeflState) (d : List UInt8) (rc : Int) (st' : DeflState) : Prop :=
296  match st.params.wrap with
297  | .gzip => rc = Z.streamError ∧ st' = st
298  | .zlib =>
299    if st.started = true then rc = Z.streamError ∧ st' = st
300    else rc = Z.ok ∧ st' = { st with dict := some d, adler := adler32 d }
301  | .raw =>
302    if st.input = [] then rc = Z.ok ∧ st' = { st with dict := some d }
303    else (rc = Z.streamError ∧ st' = st) ∨
304      (rc = Z.ok ∧ st' = { st with dict := some d, precise := false, clean := false })
305
306/-- `deflateGetDictionary(strm, buf, &len)`: `Z_OK`; the dictionary returned is a suffix of the
307history (the preset dictionary and the input since the last full flush), at most the window, and
308at least the window less 262 bytes (the part that the compressor may already have dropped), or
309all of it if shorter. -/
310def DeflGetDict (st : DeflState) (buf : List UInt8) (rc : Int) : Prop :=
311  let hist := st.dictEff ++ st.input.drop ((st.fullAt.map (·.2)).getD 0)
312  let w := 2 ^ st.params.wbits
313  rc = Z.ok ∧ buf <:+ hist ∧ buf.length ≤ w ∧ min hist.length (w - 262) ≤ buf.length
314
315/-- `deflateCopy(dest, source)`: an independent copy of the same model state; `Z_MEM_ERROR` leaves
316`dest` without a state. -/
317def DeflCopy (st : DeflState) (rc : Int) (dest : Option DeflState) : Prop :=
318  (rc = Z.ok ∧ dest = some st) ∨ (rc = Z.memError ∧ dest = none)
319
320/-- `deflatePending(strm, &pending, &bits)`: the bytes and the bits not delivered yet. -/
321def DeflPending (st : DeflState) (pending bits : Nat) (rc : Int) : Prop :=
322  rc = Z.ok ∧ pending = st.pend ∧ bits = st.bits
323
324/-- `deflatePrime(strm, bits, value)`: `Z_BUF_ERROR` if `bits` is not in 0 to 16 or the pending
325buffer has no room; otherwise `Z_OK` and the low `bits` bits of `value` are inserted in the
326output (not modelled: the stream no longer follows the format specification). -/
327def DeflPrime (st : DeflState) (bits _value : Int) (rc : Int) (st' : DeflState) : Prop :=
328  if bits < 0 ∨ bits > 16 then rc = Z.bufError ∧ st' = st
329  else (rc = Z.bufError ∧ st' = st) ∨
330    (rc = Z.ok ∧ st' = { st with precise := false, clean := false })
331
332/-- `deflateSetHeader(strm, head)`: only for a gzip stream (`Z_STREAM_ERROR` otherwise). It must
333come before the first `deflate`; later it is accepted but the data-level promises stop. A header
334record that `zlib.h` does not allow (a name or comment with a zero byte, an extra field of 65536
335bytes or more, which `deflate` writes truncated) is accepted but the promises stop too. -/
336def DeflSetHeader (st : DeflState) (h : GzHead) (rc : Int) (st' : DeflState) : Prop :=
337  if st.params.wrap ≠ .gzip then rc = Z.streamError ∧ st' = st
338  else rc = Z.ok ∧
339    ((st.started = true ∨ ¬ h.Valid) →
340      st' = { st with hdr := some h, precise := false, clean := false }) ∧
341    (¬ (st.started = true ∨ ¬ h.Valid) → st' = { st with hdr := some h })
342
343end ZlibF.Spec.Api