gzread.c.close.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.GzClose
3
4/-!
5# gzread.c: closing a reader before lazy buffer allocation
6
7This internal execution theorem covers `size = 0`, with the existing `GzGood`
8representation invariant. It includes a pending error message and descriptor failure.
9It does not prove the complete public close target or establish `GzGood` from public
10histories. Initialized readers still require the decoder and buffer cleanup proof.
11-/
12
13namespace Zlib.Gzread.Proofs
14open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib Zlib.Gzlib.Spec Zlib.Gzlib.Proofs
15open ZlibF.Spec.Public.OffsetProof
16
17/-- The exact heap after freeing the message, path and handle of an unbuffered reader. -/
18def closedHeap (h : Heap) (i : Nat) (s : GzState) : Heap :=
19  let freed := freeStr (freeStr h s.msg) s.path
20  { freed with gzstates := upd h.gzstates i none }
21
22private theorem freeStr_gzstates (h : Heap) (p : BPtr) :
23    (freeStr h p).gzstates = h.gzstates := by
24  cases p with
25  | null => rfl
26  | ref r off => cases r <;> rfl
27
28/-- `close(fd)` returns its fixed external result without changing the heap. -/
29def closeResult (fd : Int32) (fs : Fs) : Int32 × Fs :=
30  if fd < 0 || fd.toInt ≥ fs.fds.size then (-1, { fs with errno := EBADF })
31  else match fs.fds[fd.toInt.toNat]! with
32    | none => (-1, { fs with errno := EBADF })
33    | some _ => (0, { fs with fds := fs.fds.set! fd.toInt.toNat none })
34
35theorem fsClose_run (fd : Int32) (fs : Fs) (h : Heap) :
36    fsClose fd fs h = .ok (closeResult fd fs, h) := by
37  unfold fsClose closeResult
38  split
39  · rfl
40  · split <;> simp_all [pure_app]
41
42/-- `int gzclose_r(gzFile file)` rejects NULL without heap or file effects. -/
43theorem gzclose_r_null (fs : Fs) (h : Heap) :
44    Zlib.Gzread.gzclose_r none fs h = .ok ((Z_STREAM_ERROR, fs), h) := rfl
45
46/-- `int gzclose_r(gzFile file)` rejects every non-reader mode before any effect. -/
47theorem gzclose_r_wrong_mode {h : Heap} {i : Nat} {s : GzState}
48    (hs : h.gzstates i = some s) (hm : s.mode ≠ GZ_READ) (fs : Fs) :
49    Zlib.Gzread.gzclose_r (hnd i) fs h = .ok ((Z_STREAM_ERROR, fs), h) := by
50  unfold Zlib.Gzread.gzclose_r
51  offsetsimp [hs, hm]
52
53/-- `int gzclose_r(gzFile file)` closes an unbuffered reader completely.
54This internal domain requires `GzGood` and `size = 0`; it is narrower than the public
55API. No callee specification is assumed. The initialized-reader path remains open. -/
56theorem gzclose_r_unbuffered {h : Heap} {i : Nat} {s : GzState}
57    (hg : GzGood h i s) (hm : s.mode = GZ_READ) (hz : s.size = 0) (fs : Fs) :
58    Zlib.Gzread.gzclose_r (hnd i) fs h =
59      .ok (((if (closeResult s.fd fs).1 ≠ 0 then Z_ERRNO
60        else if s.err = Z_BUF_ERROR then Z_BUF_ERROR else Z_OK),
61        (closeResult s.fd fs).2), closedHeap h i s) := by
62  have he := gz_error_null_run hg Z_OK
63  have hg' := Zlib.Gzlib.Proofs.GzGood.afterErr hg Z_OK
64  obtain ⟨pb, hp, a, ha, hro, _⟩ := hg'.path
65  have hf := freeB_run hp ha hro
66  have hm' : (s.mode != GZ_READ) = false := by simp [hm]
67  have hz' : (s.size != 0) = false := by simp [hz]
68  unfold Zlib.Gzread.gzclose_r
69  simp only [hnd_isNone, Bool.false_eq_true, ↓reduceIte, castState_hnd]
70  simp only [liftM, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, G_bind_app, G_lift_app,
71    ldS_run hg.hs, hm', hz', Bool.false_eq_true, ↓reduceIte, he, ldS_run hg'.hs, hf]
72  simp [liftM, monadLift, MonadLift.monadLift, MonadLiftT.monadLift, G_bind_app, G_lift_app,
73    G_pure_app, fsClose_run, freeGzState, freeStr_setS, freeStr_gzstates, closedHeap, upd_upd, errNull]
74  simp [setS, upd_upd, freeStr_gzstates]
75
76/-- `int gzclose_r(gzFile file)` preserves unrelated allocations and does not allocate
77on the unbuffered close path. The stated footprint includes the handle, path and message. -/
78theorem gzclose_r_unbuffered_frame (h : Heap) (i : Nat) (s : GzState) :
79    ZlibF.Spec.Public.Frame h (closedHeap h i s)
80      (fun b => b = i ∨ ptrBlk s.path = some b ∨ ptrBlk s.msg = some b) ∧
81    (closedHeap h i s).nalloc = h.nalloc ∧ (closedHeap h i s).nextBlk = h.nextBlk := by
82  cases hp : s.path with
83  | null =>
84    cases hm : s.msg with
85    | null => simp [ZlibF.Spec.Public.Frame, closedHeap, hp, hm, freeStr, ptrBlk, upd_apply] <;> intro b _ <;> intros <;> simp_all
86    | ref r off => cases r <;>
87        simp [ZlibF.Spec.Public.Frame, closedHeap, hp, hm, freeStr, ptrBlk, upd_apply, eq_comm] <;> intro b _ <;> intros <;> simp_all
88  | ref r off =>
89    cases r <;> cases hm : s.msg with
90    | null => simp [ZlibF.Spec.Public.Frame, closedHeap, hp, hm, freeStr, ptrBlk, upd_apply, eq_comm] <;> intro b _ <;> intros <;> simp_all
91    | ref r' off' => cases r' <;>
92        simp [ZlibF.Spec.Public.Frame, closedHeap, hp, hm, freeStr, ptrBlk, upd_apply, eq_comm] <;> intro b _ <;> intros <;> simp_all
93
94#print axioms gzclose_r_unbuffered
95end Zlib.Gzread.Proofs