Gz.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.Deflate
2
3/-!
4# API model: the gz file API as state machines over an abstract file
5
6`gzopen` .. `gzclose` (`gzlib.c`, `gzread.c`, `gzwrite.c`, `gzclose.c`). The file system and the
7file are abstract: a file is its content, a `List UInt8`; the operating system is not modelled
8(an input/output failure is an allowed outcome of the operations that touch the file, after which
9the data-level promises stop: `failed`).
10
11*Reading.* What a reader sees is a function of the content of the file only: `GzDecoded raw D S`
12says that reading the file to its end returns exactly the bytes `D` and then the status `S`
13(`Z_OK`, or the error that `gzerror` reports). The handle keeps the position in `D`.
14
15*Writing.* The handle keeps all the uncompressed bytes written and the compressed bytes the
16library has handed to the file so far; `GzDecoded` of the final content gives back what was written.
17-/
18
19namespace ZlibF.Spec.Api
20
21open ZlibF.Spec
22
23/-- The pinned source selects gzip at the start only after four consistent header bytes.
24An invalid method, invalid flags, or a shorter initial file is read transparently. -/
25def GzLooksGzip (raw : List UInt8) : Prop :=
26  raw.length ≥ 4 ∧ raw[0]! = 31 ∧ raw[1]! = 139 ∧ raw[2]! = 8 ∧ raw[3]!.toNat < 32
27
28/-- Reading the whole file `raw` (`gzread` until the end; `gonly`: opened with `G`, so
29transparent reading is off):
30
31* a file that does not look like gzip is returned unchanged with status `Z_OK` (`gzdirect` is 1);
32* otherwise the file is a sequence of complete gzip members, followed by `rest`. The data is the
33  concatenation of the members' data. If `rest` is empty, the status is `Z_OK`. Trailing garbage
34  after at least one member is ignored (`Z_OK`, `zlib.h` `gzread`); otherwise the status is the
35  error (`Z_BUF_ERROR` for a truncated member, `Z_DATA_ERROR` for a corrupt one) and the data
36  also holds what was decoded of `rest` before it (`Layer.Consistent`);
37* `gonly` and an empty file: no data and `Z_BUF_ERROR`. -/
38def GzDecoded (gonly : Bool) (raw D : List UInt8) (S : Int) : Prop :=
39  (gonly = false ∧ ¬ GzLooksGzip raw ∧ D = raw ∧ S = Z.ok) ∨
40  (gonly = true ∧ raw = [] ∧ D = [] ∧ S = Z.bufError) ∨
41  ((GzLooksGzip raw ∨ (gonly = true ∧ raw ≠ [])) ∧
42    ∃ (ms : List (List UInt8 × List UInt8)) (rest : List UInt8),
43      (∀ p, p ∈ ms → Gzip.Decodes p.1 p.2) ∧ raw = (ms.map Prod.fst).flatten ++ rest ∧
44      (¬ ∃ m o t, rest = m ++ t ∧ Gzip.Decodes m o) ∧
45      ((rest = [] ∧ ms ≠ [] ∧ D = (ms.map Prod.snd).flatten ∧ S = Z.ok) ∨
46       (rest ≠ [] ∧ ms ≠ [] ∧ D = (ms.map Prod.snd).flatten ∧ S = Z.ok) ∨
47       (rest ≠ [] ∧ (S = Z.bufError ∨ S = Z.dataError) ∧
48         ∃ q, D = (ms.map Prod.snd).flatten ++ q ∧ Layer.Consistent .gzip 15 [] rest q)))
49
50/-- The mode of the mode string. A handle opened with `a` has mode `write` (as in `gz_open`, which
51seeks to the end and then writes). -/
52inductive GzMode where
53  | read | write | append
54  deriving DecidableEq, Repr
55
56/-- `gz_open`'s reading of the mode string: the mode (`r`, `w`, `a`; the last wins), the level (a
57digit), the strategy (`f`, `h`, `R`, `F`), and the direct flag (`T` is 1, `G` is -1). `none` for
58`+`, for no `r`/`w`/`a`, for `T` with `r`, for `G` with `w`/`a` (a `NULL` result). -/
59def gzMode? (m : List Char) : Option (GzMode × Int × Nat × Int) :=
60  let step (acc : Option GzMode × Int × Nat × Int × Bool) (c : Char) :=
61    let (mo, lv, st, di, bad) := acc
62    if '0' ≤ c ∧ c ≤ '9' then (mo, (c.toNat - '0'.toNat : Nat), st, di, bad)
63    else if c = 'r' then (some .read, lv, st, di, bad)
64    else if c = 'w' then (some .write, lv, st, di, bad)
65    else if c = 'a' then (some .append, lv, st, di, bad)
66    else if c = '+' then (mo, lv, st, di, true)
67    else if c = 'f' then (mo, lv, 1, di, bad)
68    else if c = 'h' then (mo, lv, 2, di, bad)
69    else if c = 'R' then (mo, lv, 3, di, bad)
70    else if c = 'F' then (mo, lv, 4, di, bad)
71    else if c = 'G' then (mo, lv, st, -1, bad)
72    else if c = 'T' then (mo, lv, st, 1, bad)
73    else acc
74  match m.foldl step (none, -1, 0, 0, false) with
75  | (some mo, lv, st, di, false) =>
76    if mo = .read ∧ di = 1 then none
77    else if mo ≠ .read ∧ di = -1 then none
78    else some (mo, lv, st, di)
79  | _ => none
80
81/-- The state of an open gz file. Fields of the reader: `raw` (the content), `dec`, `dstat` (what
82`GzDecoded` gives for it), `rpos` (index in `dec` of the next byte, it may be past the end after
83a forward `gzseek`), `pushed` (bytes put back by `gzungetc`, delivered first), `past` (a read came up
84short). Fields of the writer: `written` (all bytes written, with the zeros of forward seeks), `out`
85(the compressed bytes handed to the file so far), `base` (the content that was there before an
86append). Both: `err` (the code `gzerror` reports), `want` (buffer size of `gzbuffer`), `sized`
87(buffers exist), `failed` (an input/output error happened). -/
88structure GzHandle where
89  mode : GzMode
90  level : Int
91  strategy : Nat
92  direct : Int
93  raw : List UInt8
94  dec : List UInt8
95  dstat : Int
96  rpos : Nat
97  pushed : List UInt8
98  past : Bool
99  err : Int
100  written : List UInt8
101  out : List UInt8
102  base : List UInt8
103  want : Nat
104  sized : Bool
105  failed : Bool
106  deriving DecidableEq
107
108/-- The size of the buffer unless `gzbuffer` changes it (`GZBUFSIZE`). -/
109def gzBufDefault : Nat := 8192
110
111/-- `gzopen(path, mode)` / `gzdopen(fd, mode)`: `existing` is the content of the file (`none`: it does
112not exist, or the descriptor is invalid). The result is `NULL` for a bad mode, a missing file when
113reading, or an input/output or allocation failure (not distinguished: any of them may happen);
114otherwise a handle. Writing starts with an empty file; appending keeps the content (`base`). -/
115def GzOpen (mode : List Char) (existing : Option (List UInt8)) (r : Option GzHandle) : Prop :=
116  match gzMode? mode with
117  | none => r = none
118  | some (mo, lv, st, di) =>
119    r = none ∨
120    (∃ raw D S, (mo = .read → existing = some raw ∧ GzDecoded (decide (di = -1)) raw D S) ∧
121      r = some
122        { mode := (if mo = .append then .write else mo), level := lv, strategy := st, direct := di,
123          raw := if mo = .read then raw else [], dec := if mo = .read then D else [],
124          dstat := if mo = .read then S else Z.ok, rpos := 0, pushed := [], past := false,
125          err := Z.ok, written := [], out := [],
126          base := if mo = .append then existing.getD [] else [],
127          want := gzBufDefault, sized := false, failed := false })
128
129/-- `gzbuffer(file, size)`: allowed only before buffers exist. Doubling must fit in unsigned;
130sizes below eight become eight. -/
131def GzBuffer (h : GzHandle) (size : Nat) (ret : Int) (h' : GzHandle) : Prop :=
132  if h.sized = true ∨ 2 ^ 31 ≤ size then ret = -1 ∧ h' = h
133  else ret = 0 ∧ h' = { h with want := max size 8 }
134
135/-- `gzdirect(file)`: for a reader, 1 if the content is read as it is, 0 if it is decoded
136(`GzDecoded`); the call looks at the file (`sized`). For a writer, 1 only if opened with `T`. A file
137opened with `G` is never direct; an empty file and files shorter than four bytes are transparent otherwise. -/
138def GzDirect (h : GzHandle) (ret : Int) (h' : GzHandle) : Prop :=
139  match h.mode with
140  | .read =>
141    ((ret = 1 ∧ h.dec = h.raw ∧ ¬ GzLooksGzip h.raw ∧ h.direct ≠ -1) ∨
142      (ret = 0 ∧ (GzLooksGzip h.raw ∨ h.direct = -1))) ∧ h' = { h with sized := true }
143  | _ => ret = (if h.direct = 1 then 1 else 0) ∧ h' = h
144
145/-- The bytes a reader can still deliver, pushed-back bytes first. -/
146def GzHandle.avail (h : GzHandle) : List UInt8 := h.pushed ++ h.dec.drop h.rpos
147
148/-- `gztell` for a reader (`gztell64`: `x.pos + (past ? 0 : skip)`): the uncompressed position, negative
149after a push back at the start. After the end was hit (`past`) a pending skip of a forward `gzseek`
150is **not** counted: the position stays at the end of the data (quirk of `gzlib.c`, see `GzSeek`). -/
151def GzHandle.tell (h : GzHandle) : Int :=
152  (if h.past = true then ((min h.rpos h.dec.length : Nat) : Int) else (h.rpos : Int)) - h.pushed.length
153
154/-- The reader is in the mode that copies the file as it is (`how == COPY`): the first read or
155`gzdirect` looked at the file (`sized`), it is not empty and does not look like gzip. -/
156def GzHandle.CopyMode (h : GzHandle) : Prop :=
157  h.sized = true ∧ h.raw ≠ [] ∧ ¬ GzLooksGzip h.raw ∧ h.direct ≠ -1
158
159/-- `gzread(file, buf, len)`: returns `bytes.length`, or `-1`. The bytes are the next bytes of
160`pushed ++ dec.drop rpos`; a request longer than `2^31 - 1` is `-1` with `Z_STREAM_ERROR`; a
161serious error from earlier is `-1` (data read before the error is delivered first). A read that
162comes up short sets `past`, and reveals the status `dstat` of the file (`gzerror`); the status may
163also be revealed earlier. `-1` is returned only if no byte was read and the error is serious.
164`Z_BUF_ERROR` (a truncated file) does not stop reading. -/
165def GzReadFn (h : GzHandle) (len : Nat) (bytes : List UInt8) (ret : Int) (h' : GzHandle) : Prop :=
166  (h.mode ≠ .read → ret = -1 ∧ bytes = [] ∧ h' = h) ∧
167  (h.mode = .read → if len > 2 ^ 31 - 1 then
168    ret = -1 ∧ bytes = [] ∧
169      h' = { h with err := if h.err = Z.ok ∨ h.err = Z.bufError then Z.streamError else h.err }
170  else if (h.err ≠ Z.ok ∧ h.err ≠ Z.bufError) ∧ h.pushed = [] ∧ h.dec.drop h.rpos = [] then
171    ret = -1 ∧ bytes = [] ∧ h' = h
172  else
173    bytes = h.avail.take len ∧
174    h'.pushed = h.pushed.drop bytes.length ∧
175    h'.rpos = h.rpos + (bytes.length - min bytes.length h.pushed.length) ∧
176    h'.dec = h.dec ∧ h'.raw = h.raw ∧ h'.mode = h.mode ∧
177    (0 < len → h'.sized = true) ∧ (len = 0 → h'.sized = h.sized) ∧
178    (bytes.length < len → h'.past = true ∧ h'.err = h.dstat) ∧
179    (bytes.length = len → h'.past = h.past ∧ (h'.err = h.err ∨ h'.err = h.dstat)) ∧
180    (ret = if bytes = [] ∧ len > 0 ∧ h'.err ≠ Z.ok ∧ h'.err ≠ Z.bufError then -1
181           else (bytes.length : Int)))
182
183/-- `gzfread(buf, size, nitems, file)`: the number of whole items read; a partial item that was
184read is lost (`zlib.h`). -/
185def GzFread (h : GzHandle) (size nitems : Nat) (bytes : List UInt8) (items : Nat) (h' : GzHandle) :
186    Prop :=
187  (h.mode ≠ .read ∨ size = 0 → items = 0 ∧ bytes = [] ∧ h' = h) ∧
188  (h.mode = .read → size ≠ 0 → ∃ ret, GzReadFn h (size * nitems) bytes ret h' ∧ items = bytes.length / size)
189
190/-- `gzgetc(file)`: a byte (0 to 255) or `-1` at the end or on error. -/
191def GzGetc (h : GzHandle) (ret : Int) (h' : GzHandle) : Prop :=
192  ∃ bytes r, GzReadFn h 1 bytes r h' ∧ (ret = match bytes with | [b] => (b.toNat : Int) | _ => -1)
193
194/-- `gzungetc(c, file)`: pushes the byte back and returns it; `-1` for `c < 0` or if there is no
195room. At least one byte can be pushed back when the pushed-back list is empty. -/
196def GzUngetc (h : GzHandle) (c : Int) (ret : Int) (h' : GzHandle) : Prop :=
197  (h.mode ≠ .read → ret = -1 ∧ h' = h) ∧
198  (h.mode = .read → c < 0 → ret = -1 ∧ h' = h) ∧
199  (h.mode = .read → 0 ≤ c → (ret = c ∧ h'.pushed = (c.toNat.toUInt8) :: h.pushed ∧ h'.past = false ∧
200      h'.rpos = h.rpos ∧ h'.dec = h.dec ∧ h'.sized = true) ∨
201    (h.pushed ≠ [] ∧ ret = -1))
202
203/-- `gzgets(file, buf, len)`: `none` for `NULL`. The line is read up to and including the first
204newline, or `len - 1` bytes, or the end. `NULL` if `len < 1`, or nothing was read with `len > 1`. -/
205def GzGets (h : GzHandle) (len : Int) (line : Option (List UInt8)) (h' : GzHandle) : Prop :=
206  (h.mode ≠ .read ∨ len < 1 → line = none ∧ h' = h) ∧
207  (h.mode = .read → 1 ≤ len →
208    ∃ bytes, line = (if bytes = [] ∧ len > 1 then none else some bytes) ∧
209      bytes <+: h.avail ∧ bytes.length ≤ len.toNat - 1 ∧
210      (∀ b, b ∈ bytes.dropLast → b ≠ 10) ∧
211      (bytes.getLast? = some 10 ∨ bytes.length = len.toNat - 1 ∨ bytes = h.avail) ∧
212      h'.pushed = h.pushed.drop bytes.length ∧
213      h'.rpos = h.rpos + (bytes.length - min bytes.length h.pushed.length) ∧ h'.dec = h.dec)
214
215/-- `gzeof(file)`: true iff a read came up short (the read position is at the end and a read
216tried to go past it); false for a writer. -/
217def GzEof (h : GzHandle) (ret : Int) : Prop :=
218  ret = (if h.mode = .read ∧ h.past = true then 1 else 0)
219
220/-- `gzerror(file, &errnum)`: the code. It is `Z_OK` for a handle on which nothing failed. -/
221def GzError (h : GzHandle) (code : Int) : Prop := code = h.err
222
223/-- `gzclearerr(file)`: no error, no end-of-file indicator. -/
224def GzClearerr (h : GzHandle) (h' : GzHandle) : Prop :=
225  h' = { h with err := Z.ok, past := false }
226
227/-- `gzrewind(file)`: reader without a serious error: back to position 0 (`0`), else `-1`. -/
228def GzRewind (h : GzHandle) (ret : Int) (h' : GzHandle) : Prop :=
229  (h.mode = .read ∧ (h.err = Z.ok ∨ h.err = Z.bufError) ∧
230    ((ret = 0 ∧ h' = { h with rpos := 0, pushed := [], past := false, err := Z.ok }) ∨
231     (ret = -1 ∧ h' = h))) ∨
232  ((h.mode ≠ .read ∨ (h.err ≠ Z.ok ∧ h.err ≠ Z.bufError)) ∧ ret = -1 ∧ h' = h)
233
234/-- `gzseek(file, offset, whence)`: `whence` 0 (`SEEK_SET`) or 1 (`SEEK_CUR`; relative to `gztell`);
235anything else, a serious error, or a position before the start is `-1`. The new position is
236returned, **but `gztell` need not agree with it**. A reader may seek anywhere forward (the skipping is
237done by the next read); a writer only forward (zeros fill the gap).
238
239For a reader (`gzseek64`):
240* in the copying mode (`CopyMode`) the file is repositioned: nothing pushed back, `past` and the
241  error are cleared, and `gztell` is the position;
242* a backward seek rewinds the file and then skips: the same (nothing pushed back, `past` and the
243  error cleared);
244* a forward seek of `d` bytes in the decoding mode first consumes pushed-back bytes, and skips
245  the rest later (`rpos` is the virtual position). It does **not** clear `past`: if a read has
246  come up short before, `gzeof` stays 1 and `gztell` still reports the end of the data, not the new
247  position (`gztell64` ignores the skip while `past` is set). `gzseek` returned the new
248  position anyway. This was seen on the real library (a quirk, not undefined behaviour). -/
249def GzSeek (h : GzHandle) (off whence : Int) (ret : Int) (h' : GzHandle) : Prop :=
250  let cur : Int := if h.mode = .read then h.tell else (h.written.length : Int)
251  let target : Int := (if whence = 0 then 0 else cur) + off
252  let d : Nat := (target - cur).toNat
253  let bad := (h.err ≠ Z.ok ∧ h.err ≠ Z.bufError) ∨ (whence ≠ 0 ∧ whence ≠ 1) ∨
254    target < 0 ∨ (h.mode = .write ∧ target < cur)
255  (bad → ret = -1 ∧ h' = h) ∧
256  (¬ bad →
257    (ret = -1 ∧ h.mode = .read) ∨
258    (ret = target ∧
259      (h.mode = .write → h'.written = h.written ++ List.replicate d 0) ∧
260      (h.mode = .read → h'.dec = h.dec ∧ h'.sized = h.sized ∧
261        ((h.CopyMode ∨ target < cur) →
262          h'.pushed = [] ∧ h'.past = false ∧ h'.err = Z.ok ∧ h'.rpos = target.toNat) ∧
263        (¬ h.CopyMode → cur ≤ target →
264          h'.past = h.past ∧ h'.err = h.err ∧ h'.pushed = h.pushed.drop d ∧
265          h'.rpos = h.rpos + (d - min d h.pushed.length)))))
266
267/-- `gztell(file)`: the uncompressed position: bytes read (reader) or written, zeros of seeks
268included (writer); the append handle counts the bytes written. -/
269def GzTell (h : GzHandle) (ret : Int) : Prop :=
270  ret = (if h.mode = .read then h.tell else (h.written.length : Int))
271
272/-- `gzoffset(file)`: the position in the compressed file (`lseek` of the descriptor, less the
273input not yet used by a reader), or `-1` if it is unknown. It is not bounded by the size of the
274content: the descriptor of `gzdopen` may start at a position other than 0, and in the copying mode
275a seek beyond the end moves the descriptor beyond the end (seen on the real library: 100 for a file
276of 5 bytes). -/
277def GzOffset (_h : GzHandle) (ret : Int) : Prop :=
278  ret = -1 ∨ 0 ≤ ret
279
280/-! ## Writing -/
281
282/-- The compressed bytes of a writer are a growing prefix of one gzip member (or, for a
283transparent writer, the data itself). -/
284def GzHandle.OutGrows (h h' : GzHandle) : Prop :=
285  h.out <+: h'.out ∧ h'.base = h.base ∧ h'.mode = h.mode ∧ h'.direct = h.direct
286
287/-- Writing `s` succeeded or failed. On success `written` grows by `s`; on a failure of the file
288the handle is marked `failed`, `err` is `Z_ERRNO` and nothing is promised about the data. -/
289def GzWriteBytes (h : GzHandle) (s : List UInt8) (ok : Bool) (h' : GzHandle) : Prop :=
290  h.OutGrows h' ∧ h'.sized = true ∧ h'.level = h.level ∧ h'.strategy = h.strategy ∧
291  (if ok then h'.written = h.written ++ s ∧ h'.err = Z.ok ∧ h'.failed = h.failed
292   else h'.failed = true ∧ h'.err = Z.errno)
293
294/-- `gzwrite(file, buf, len)`: returns `len` (or 0 if `len = 0`); 0 for a reader, after a serious
295error, for `len > 2^31 - 1`, or if the file failed. -/
296def GzWrite (h : GzHandle) (s : List UInt8) (ret : Int) (h' : GzHandle) : Prop :=
297  ((h.mode = .read ∨ h.err ≠ Z.ok) → ret = 0 ∧ h' = h) ∧
298  (¬ (h.mode = .read ∨ h.err ≠ Z.ok) →
299    (s.length > 2 ^ 31 - 1 → ret = 0 ∧ h'.err = Z.dataError ∧ h'.written = h.written) ∧
300    (s.length ≤ 2 ^ 31 - 1 →
301      ((ret = s.length ∧ GzWriteBytes h s true h') ∨ (ret = 0 ∧ GzWriteBytes h s false h'))))
302
303/-- `gzputc(file, c)`: returns `c` mod 256, or `-1`. -/
304def GzPutc (h : GzHandle) (c : Int) (ret : Int) (h' : GzHandle) : Prop :=
305  ((h.mode = .read ∨ h.err ≠ Z.ok) → ret = -1 ∧ h' = h) ∧
306  (¬ (h.mode = .read ∨ h.err ≠ Z.ok) →
307    ((ret = c % 256 ∧ GzWriteBytes h [(c % 256).toNat.toUInt8] true h') ∨
308     (ret = -1 ∧ GzWriteBytes h [(c % 256).toNat.toUInt8] false h')))
309
310/-- `gzputs(file, s)`: `s` has no zero byte. Returns the length of `s`, or `-1`. -/
311def GzPuts (h : GzHandle) (s : List UInt8) (ret : Int) (h' : GzHandle) : Prop :=
312  ((h.mode = .read ∨ h.err ≠ Z.ok) → ret = -1 ∧ h' = h) ∧
313  (¬ (h.mode = .read ∨ h.err ≠ Z.ok) →
314    ((ret = s.length ∧ GzWriteBytes h s true h') ∨ (ret = -1 ∧ GzWriteBytes h s false h')))
315
316/-- `gzprintf(file, format, ...)`: `s` is the formatted output. It is written only if it is not
317empty and shorter than the buffer (`want`); otherwise 0 is returned and nothing is written. -/
318def GzPrintf (h : GzHandle) (s : List UInt8) (ret : Int) (h' : GzHandle) : Prop :=
319  if h.mode = .read ∨ h.err ≠ Z.ok then ret = Z.streamError ∧ h' = h
320  else if s = [] ∨ s.length ≥ h.want then ret = 0 ∧ h.written = h'.written
321  else (ret = s.length ∧ GzWriteBytes h s true h') ∨
322    (ret = Z.errno ∧ GzWriteBytes h s false h')
323
324/-- `gzfwrite(buf, size, nitems, file)`: writes `size * nitems` bytes; returns the number of
325items written. -/
326def GzFwrite (h : GzHandle) (size : Nat) (s : List UInt8) (items : Nat) (h' : GzHandle) : Prop :=
327  (size = 0 → items = 0 ∧ h' = h) ∧
328  (size ≠ 0 → s.length % size = 0 ∧ ∃ ret, GzWrite h s ret h' ∧ items = ret.toNat / size)
329
330/-- `gzsetparams(file, level, strategy)`: for a writer, `Z_OK` (the new level and strategy are
331used from then on; the data written is unaffected) or an error code; `Z_STREAM_ERROR` for a
332reader. -/
333def GzSetParams (h : GzHandle) (_level _strategy : Int) (rc : Int) (h' : GzHandle) : Prop :=
334  if h.mode = .read ∨ h.err ≠ Z.ok then rc = Z.streamError ∧ h' = h
335  else
336    (rc = Z.ok ∧ h'.written = h.written ∧ h.OutGrows h') ∨
337    (rc = Z.streamError ∧ h' = h) ∨
338    (rc = Z.errno ∧ h'.failed = true ∧ h'.err = Z.errno)
339
340/-- `gzflush(file, flush)`: `flush` is one of `Z_NO_FLUSH` .. `Z_FINISH` (0 to 4), else
341`Z_STREAM_ERROR`. After `Z_FINISH` the member is ended and later writes are lost, so the model marks the handle `failed` (no data promise remains). After `Z_OK` with `Z_SYNC_FLUSH` or `Z_FULL_FLUSH` all the data written is in the
342file, on a byte boundary: the bytes handed to the file so far plus `closer` are a gzip member of
343exactly what was written (`F-deflate-flush`). -/
344def GzFlush (h : GzHandle) (flush : Int) (rc : Int) (h' : GzHandle) : Prop :=
345  if h.mode ≠ .write ∨ h.err ≠ Z.ok then rc = Z.streamError ∧ h' = h
346  else if flush < 0 ∨ flush > 4 then rc = Z.streamError ∧ h' = h
347  else
348    (rc = Z.ok ∧ h.OutGrows h' ∧ h'.written = h.written ∧ h'.failed = h.failed ∧ h'.sized = true ∧
349      ((flush = 2 ∨ flush = 3) → h.failed = false → h.direct ≠ 1 →
350        Gzip.Decodes (h'.out ++ closer .gzip h.written) h.written) ∧
351      (flush = 4 → h'.failed = true)) ∨
352    (rc = Z.errno ∧ h.OutGrows h' ∧ h'.failed = true ∧ h'.err = Z.errno)
353
354/-- `gzclose(file)` / `gzclose_r` / `gzclose_w`: the handle ends. Result: `Z_OK`; or for a reader
355`Z_BUF_ERROR` if the file was truncated and read to its end; or `Z_ERRNO` for a writer or reader
356whose file failed. The content of the file after closing a writer: for a gzip writer that did
357not fail, `base` followed by one gzip member that decodes to exactly what was written (an
358empty file for nothing written is a member of no data), so that `GzDecoded` gives it back
359(`C7`); for a transparent writer, `base` followed by the data. `final` is that content. -/
360def GzClose (h : GzHandle) (rc : Int) (final : List UInt8) : Prop :=
361  (rc = Z.ok ∨ rc = Z.bufError ∨ rc = Z.errno) ∧
362  (h.mode = .read → rc = Z.bufError ∨ rc = Z.ok ∨ rc = Z.errno) ∧
363  (h.mode ≠ .read → h.failed = false → rc = Z.errno ∨ rc = Z.ok) ∧
364  (h.mode ≠ .read → h.failed = false → rc = Z.ok →
365    (h.direct = 1 → final = h.base ++ h.written) ∧
366    (h.direct ≠ 1 → ∃ m, final = h.base ++ m ∧ h.out <+: m ∧ Gzip.Decodes m h.written))
367
368end ZlibF.Spec.Api