gzclose.c.lean

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

1import ZlibF.Proof.«gzlib.c.seek»
2import ZlibF.Zlib.«gzclose.c»
3
4/-!
5# gzclose.c: `gzclose`
6
7`gzclose` dispatches on the mode of the handle: a reader goes to `gzclose_r` (`gzread.c`), every other handle to
8`gzclose_w` (`gzwrite.c`). What `gzclose_r` and `gzclose_w` do (free the stream, the buffers, the path and the message,
9close the descriptor, return the error) is stated and proved with those files; this module proves the dispatch and the
10null-handle case, which need only the invariant of the handle.
11-/
12
13namespace Zlib.Gzclose.Proofs
14open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
15
16/-- `gzclose(NULL)` is `Z_STREAM_ERROR`, nothing else happens. -/
17theorem gzclose_null (fs : Fs) (h : Heap) :
18    Zlib.Gzclose.gzclose none fs h = .ok ((Z_STREAM_ERROR, fs), h) := rfl
19
20/-- **gzclose, dispatch.** On a handle that satisfies the invariant, `gzclose` is `gzclose_r` for a reader and `gzclose_w`
21for a writer (the state is read once, nothing else is done before the call). -/
22theorem gzclose_dispatch {h : Heap} {gs : Nat} {s : GzState} (hG : GzGood h gs s) (fs : Fs) :
23    Zlib.Gzclose.gzclose (hnd gs) fs h =
24      if s.mode = GZ_READ then Zlib.Gzread.gzclose_r (hnd gs) fs h else Zlib.Gzwrite.gzclose_w (hnd gs) fs h := by
25  have hs := hG.hs
26  unfold Zlib.Gzclose.gzclose
27  by_cases hm : s.mode = GZ_READ
28  · ggsimp [hs, hm]
29  · ggsimp [hs, hm]
30
31end Zlib.Gzclose.Proofs