GzOpen.lean

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

1import ZlibF.Spec.Public.GzControl
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6def parsedMode (bytes : List UInt8) : Option (Api.GzMode × Int × Nat × Int) :=
7  Api.gzMode? (bytes.map fun b => Char.ofNat b.toNat)
8
9def openFlags (bytes : List UInt8) (mode : Api.GzMode) : Int32 :=
10  (if 101 ∈ bytes then O_CLOEXEC else 0) ||| (if 78 ∈ bytes then O_NONBLOCK else 0) |||
11  (if mode = .read then 0 else O_WRONLY ||| O_CREAT |||
12    (if 120 ∈ bytes then O_EXCL else 0) ||| (if mode = .append then O_APPEND else O_TRUNC))
13
14/-- OS operations remain the fixed external-world semantics, rather than an assumed zlib callee. -/
15def OpenWorld (h : Heap) (before after : Fs) (path modeBytes : List UInt8)
16    (mode : Api.GzMode) (existing : Option Int32) (fd : Int32) (start : Int64) : Prop :=
17  ∃ opened,
18    (match existing with
19     | none => Zlib.GzFs.fsOpen path.toArray (openFlags modeBytes mode) before h = .ok ((fd, opened), h)
20     | some oldFd => fd = oldFd ∧ opened = before) ∧
21    (if fd = -1 then after = opened
22     else if mode = .append then
23       ∃ ignored, Zlib.GzFs.fsLseek fd 0 SEEK_END opened h = .ok ((ignored, after), h)
24     else if mode = .read then
25       ∃ position, Zlib.GzFs.fsLseek fd 0 SEEK_CUR opened h = .ok ((position, after), h) ∧
26         start = (if position = -1 then 0 else position)
27     else after = opened)
28
29def OpenState (h : Heap) (i : Nat) (s : GzState) (mode : Api.GzMode)
30    (level : Int) (strategy : Nat) (direct : Int) (fd : Int32) (path : List UInt8) : Prop :=
31  GzValid h i s ∧
32  s.mode = (if mode = .read then GZ_READ else GZ_WRITE) ∧ s.fd = fd ∧
33  CString h s.path path ∧ s.level.toInt = level ∧ s.strategy.toInt = strategy ∧
34  s.direct.toInt = (if mode = .read ∧ direct = 0 then 1 else direct) ∧
35  s.size = 0 ∧ s.want = 8192 ∧ s.err = Z_OK ∧ s.msg = .null ∧
36  s.x.have = 0 ∧ s.x.pos = 0 ∧ s.past = 0 ∧ s.again = 0 ∧ s.skip = 0 ∧ s.strm.avail_in = 0 ∧
37  (mode = .read → s.eof = 0 ∧ s.how = LOOK ∧ s.junk = -1)
38
39def OpenContract (program : BPtr → BPtr → G GzFilePtr) : Prop :=
40  (∀ h fs path mode, path = .null ∨ mode = .null → program path mode fs h = .ok ((none, fs), h)) ∧
41  (∀ h fs path mode name flags,
42    Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
43    CString h path name → CString h mode flags →
44    ∃ result fs' after, program path mode fs h = .ok ((result, fs'), after) ∧
45      Frame h after (fun _ => False) ∧
46      (match result with
47       | none => LiveChange h after (fun _ => False) (fun _ => False) ∧
48           (parsedMode flags = none ∨ AllocationFailed h after ∨
49             ∃ mode level strategy direct start,
50               parsedMode flags = some (mode, level, strategy, direct) ∧
51               OpenWorld h fs fs' name flags mode none (-1) start)
52       | some (.in_gzstate_x i) => ∃ s mode level strategy direct,
53           parsedMode flags = some (mode, level, strategy, direct) ∧
54           OpenState after i s mode level strategy direct s.fd name ∧
55           OpenWorld h fs fs' name flags mode none s.fd s.start ∧ s.fd ≠ -1 ∧
56           LiveChange h after (GzOwned after i s) (fun _ => False)))
57
58/-- `gzFile gzopen(const char *path, const char *mode)`.
59Parse the complete mode string, open/truncate/append as requested, transfer descriptor ownership,
60initialize the handle, and release every allocation on a null result. -/
61def Goal.gzopen : Prop := OpenContract Zlib.Gzlib.gzopen
62
63/-- `gzFile gzopen64(const char *path, const char *mode)`.
64The LP64 entry uses the same open flags and position range as `gzopen`. -/
65def Goal.gzopen64 : Prop := OpenContract Zlib.Gzlib.gzopen64
66
67/-- `gzFile gzdopen(int fd, const char *mode)`.
68Negative descriptors are rejected. No open syscall occurs, and failure retains the caller's
69descriptor. A successful handle takes ownership; its path is the formatted descriptor name. -/
70def Goal.gzdopen : Prop :=
71  (∀ h fs fd mode, fd.toInt < 0 → Zlib.Gzlib.gzdopen fd mode fs h = .ok ((none, fs), h)) ∧
72  (∀ h fs fd mode flags,
73    Fresh h → Zlib.Gzlib.Spec.Uniq h → LibraryGlobals h → FileSystem fs →
74    0 ≤ fd.toInt → (mode ≠ .null → CString h mode flags) →
75    ∃ result fs' after, Zlib.Gzlib.gzdopen fd mode fs h = .ok ((result, fs'), after) ∧
76      Frame h after (fun _ => False) ∧
77      (match result with
78       | none => fs'.fds = fs.fds ∧ LiveChange h after (fun _ => False) (fun _ => False) ∧
79           (mode = .null ∨ parsedMode flags = none ∨ AllocationFailed h after)
80       | some (.in_gzstate_x i) => ∃ s mode level strategy direct,
81           parsedMode flags = some (mode, level, strategy, direct) ∧
82           OpenState after i s mode level strategy direct fd
83             (String.toUTF8 ("<fd:" ++ toString fd.toInt ++ ">")).toList ∧
84           OpenWorld h fs fs' [] flags mode (some fd) fd s.start ∧
85           LiveChange h after (GzOwned after i s) (fun _ => False)))
86
87end ZlibF.Spec.Public