GzClose.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.GzWrite
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6def DescriptorPresent (fs : Fs) (fd : Int32) : Prop :=
7  0 ≤ fd.toInt ∧ ∃ file, fs.fds[fd.toInt.toNat]? = some (some file)
8
9def CloseEffects (h after : Heap) (fs fs' : Fs) (i : Nat) (s : GzState) : Prop :=
10  after.gzstates i = none ∧ Frame h after (GzOwned h i s) ∧
11  LiveChange h after (fun _ => False) (GzOwned h i s) ∧
12  FileSystem fs' ∧ fs'.names = fs.names ∧ fs'.fsizeLimit = fs.fsizeLimit ∧
13  fs'.fds.size = fs.fds.size ∧ fs'.nodes.size = fs.nodes.size ∧
14  (∀ j, j ≠ s.fd.toInt.toNat → fs'.fds[j]? = fs.fds[j]?) ∧
15  (DescriptorPresent fs s.fd → fs'.fds[s.fd.toInt.toNat]? = some none) ∧
16  (¬ DescriptorPresent fs s.fd → fs'.fds = fs.fds) ∧
17  (∀ file j, fs.fds[s.fd.toInt.toNat]? = some (some file) → j ≠ file.node →
18    fs'.nodes[j]? = fs.nodes[j]?) ∧
19  (s.mode = GZ_READ → fs'.nodes = fs.nodes)
20
21def CloseContract (program : GzFilePtr → G Int32) (mode : Option Int32) : Prop :=
22  (∀ h fs, program none fs h = .ok ((Z_STREAM_ERROR, fs), h)) ∧
23  (∀ h fs i s, GzReachable h fs i → GzValid h i s →
24    ∃ rc fs' after, program (some (.in_gzstate_x i)) fs h = .ok ((rc, fs'), after) ∧
25      (if ∃ expected, mode = some expected ∧ expected ≠ s.mode then
26        rc = Z_STREAM_ERROR ∧ after = h ∧ fs' = fs
27       else CloseEffects h after fs fs' i s ∧
28        (¬ DescriptorPresent fs s.fd → rc = Z_ERRNO) ∧
29        (DescriptorPresent fs s.fd → s.mode = GZ_READ → rc = if s.err = Z_BUF_ERROR then Z_BUF_ERROR else Z_OK) ∧
30        (NoAllocationFailure h → WriterReady s → WriteRoom fs s 0 → rc = Z_OK)))
31
32/-- `int gzclose_r(gzFile file)`.
33Reject a writer without closing it. A reader releases every owned allocation and closes its
34descriptor, reporting a truncated-member buffer error unless close itself fails. -/
35def Goal.gzclose_r : Prop := CloseContract Zlib.Gzread.gzclose_r (some GZ_READ)
36
37/-- `int gzclose_w(gzFile file)`.
38Reject a reader without closing it. Complete pending zeros and the final member, then release
39all storage and close the descriptor, including every error path. -/
40def Goal.gzclose_w : Prop := CloseContract Zlib.Gzwrite.gzclose_w (some GZ_WRITE)
41
42/-- `int gzclose(gzFile file)`.
43Dispatch by the actual mode and apply the corresponding complete close contract. -/
44def Goal.gzclose : Prop := CloseContract Zlib.Gzclose.gzclose none
45
46end ZlibF.Spec.Public