gzlib.c.open.lean

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

1import ZlibF.Proof.«public-gz-offset»
2import ZlibF.Spec.Public.GzOpen
3
4/-!
5# gzlib.c: open refusal and initial allocation failure
6
7These execution lemmas cover the front of the actual open functions. They do not
8prove successful mode parsing, handle construction or the complete public targets.
9Null arguments are checked before allocation by `gz_open`. `gzdopen` first rejects
10negative descriptors and then allocates its temporary path.
11-/
12
13namespace Zlib.Gzlib.Proofs
14open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib.Spec ZlibF.Spec.Public.OffsetProof
15
16/-- `gzFile gz_open(const void *path, int fd, const char *mode)` rejects NULL first. -/
17theorem gz_open_null (h : Heap) (fs : Fs) (path : BPtr) (fd : Int32) (mode : BPtr)
18    (hn : path = .null ∨ mode = .null) :
19    gz_open path fd mode fs h = .ok ((none, fs), h) := by
20  unfold gz_open
21  offsetsimp [hn]
22
23/-- `gzFile gzopen(const char *path, const char *mode)` rejects either NULL argument. -/
24theorem gzopen_null (h : Heap) (fs : Fs) (path mode : BPtr)
25    (hn : path = .null ∨ mode = .null) :
26    gzopen path mode fs h = .ok ((none, fs), h) := gz_open_null h fs path (-1) mode hn
27
28/-- `gzFile gzopen64(const char *path, const char *mode)` rejects either NULL argument. -/
29theorem gzopen64_null (h : Heap) (fs : Fs) (path mode : BPtr)
30    (hn : path = .null ∨ mode = .null) :
31    gzopen64 path mode fs h = .ok ((none, fs), h) := gz_open_null h fs path (-1) mode hn
32
33/-- `gzFile gz_open(const void *path, int fd, const char *mode)` returns NULL when
34its first allocation fails. No path or mode byte is read; no descriptor is opened. -/
35theorem gz_open_alloc_failure (h : Heap) (fs : Fs) (path : BPtr) (fd : Int32) (mode : BPtr)
36    (hp : path ≠ .null) (hm : mode ≠ .null) (hf : h.allocOk h.nalloc = false) :
37    gz_open path fd mode fs h = .ok ((none, fs), { h with nalloc := h.nalloc + 1 }) := by
38  unfold gz_open
39  offsetsimp [hp, hm, allocGzState, hf]
40
41/-- `gzFile gzopen(const char *path, const char *mode)` has exact first-allocation failure effects. -/
42theorem gzopen_alloc_failure (h : Heap) (fs : Fs) (path mode : BPtr)
43    (hp : path ≠ .null) (hm : mode ≠ .null) (hf : h.allocOk h.nalloc = false) :
44    gzopen path mode fs h = .ok ((none, fs), { h with nalloc := h.nalloc + 1 }) :=
45  gz_open_alloc_failure h fs path (-1) mode hp hm hf
46
47/-- `gzFile gzopen64(const char *path, const char *mode)` has the same allocation failure effects. -/
48theorem gzopen64_alloc_failure (h : Heap) (fs : Fs) (path mode : BPtr)
49    (hp : path ≠ .null) (hm : mode ≠ .null) (hf : h.allocOk h.nalloc = false) :
50    gzopen64 path mode fs h = .ok ((none, fs), { h with nalloc := h.nalloc + 1 }) :=
51  gz_open_alloc_failure h fs path (-1) mode hp hm hf
52
53/-- `gzFile gzdopen(int fd, const char *mode)` rejects negative descriptors before allocation. -/
54theorem gzdopen_negative (h : Heap) (fs : Fs) (fd : Int32) (mode : BPtr) (hf : fd < 0) :
55    gzdopen fd mode fs h = .ok ((none, fs), h) := by
56  unfold gzdopen
57  offsetsimp [hf]
58
59/-- `gzFile gzdopen(int fd, const char *mode)` retains the descriptor when its temporary
60path allocation fails. The allocation counter advances once and no other heap field changes. -/
61theorem gzdopen_alloc_failure (h : Heap) (fs : Fs) (fd : Int32) (mode : BPtr)
62    (hn : ¬ fd < 0) (hf : h.allocOk h.nalloc = false) :
63    gzdopen fd mode fs h = .ok ((none, fs), { h with nalloc := h.nalloc + 1 }) := by
64  unfold gzdopen
65  offsetsimp [hn, allocB, hf]
66
67#print axioms gz_open_alloc_failure
68#print axioms gzdopen_alloc_failure
69end Zlib.Gzlib.Proofs