deflate.c.init.cleanup.lean

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

1import ZlibF.Proof.«deflate.c.life.end»
2
3/-! # deflate.c: cleanup of a partially allocated initializer state -/
4
5namespace Zlib.Deflate.Proofs.DefaultInit
6open C Zlib.Deflate Zlib.Deflate.Spec
7set_option autoImplicit false
8
9def FreeableB (h : Heap) (p : BPtr) : Prop :=
10  p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false
11
12def FreeableW (h : Heap) (p : WPtr) : Prop :=
13  p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.words b = some a
14
15theorem freeableB_after {h : Heap} {p q : BPtr} (hq : FreeableB h q)
16    (hp : FreeableB h p) (hsep : p = .null ∨ q = .null ∨ p ≠ q) : FreeableB (freeBytes h p) q := by
17  rcases hq with rfl | ⟨qb, qa, rfl, hqa, hqr⟩
18  · exact Or.inl rfl
19  · rcases hp with rfl | ⟨pb, pa, rfl, hpa, hpr⟩
20    · exact Or.inr ⟨qb, qa, rfl, hqa, hqr⟩
21    · have hn : qb ≠ pb := by
22        rcases hsep with impossible | impossible | hn
23        · cases impossible
24        · cases impossible
25        · intro he
26          subst qb
27          exact hn rfl
28      exact Or.inr ⟨qb, qa, rfl, by simpa [freeBytes, upd_ne _ _ _ _ hn] using hqa, hqr⟩
29
30theorem freeableW_after {h : Heap} {p q : WPtr} (hq : FreeableW h q)
31    (hp : FreeableW h p) (hsep : p = .null ∨ q = .null ∨ p ≠ q) : FreeableW (freeWords h p) q := by
32  rcases hq with rfl | ⟨qb, qa, rfl, hqa⟩
33  · exact Or.inl rfl
34  · rcases hp with rfl | ⟨pb, pa, rfl, hpa⟩
35    · exact Or.inr ⟨qb, qa, rfl, hqa⟩
36    · have hn : qb ≠ pb := by
37        rcases hsep with impossible | impossible | hn
38        · cases impossible
39        · cases impossible
40        · intro he
41          subst qb
42          exact hn rfl
43      exact Or.inr ⟨qb, qa, rfl, by simpa [freeWords, upd_ne _ _ _ _ hn] using hqa⟩
44
45theorem freeB_continue {α : Type} {h : Heap} {r : ZStreamRef} {z : ZStream} {p : BPtr}
46    (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree") (hp : FreeableB h p) (k : M α) :
47    (if p != .null then do ZFREE_bytes (some r) p; k else k) h = k (freeBytes h p) := by
48  by_cases hn : p = .null
49  · subst p
50    rfl
51  · have hr := zfreeB_run hz hf hp
52    simp [hn, bind_app, hr]
53
54theorem freeW_continue {α : Type} {h : Heap} {r : ZStreamRef} {z : ZStream} {p : WPtr}
55    (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree") (hp : FreeableW h p) (k : M α) :
56    (if p != .null then do ZFREE_words (some r) p; k else k) h = k (freeWords h p) := by
57  by_cases hn : p = .null
58  · subst p
59    rfl
60  · have hr := zfreeW_run hz hf hp
61    simp [hn, bind_app, hr]
62
63/-- `int deflateEnd(z_streamp strm)`.
64The actual cleanup also executes on partially allocated init buffers. The
65source accepts NULL buffers; no DGood or complete-buffer premise is needed.
66Distinct non-NULL buffers of each element type are freed once. -/
67theorem end_partial_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
68    (hl : DLive h r ds z d) (hf : z.zfree = .fn "zcfree")
69    (hb : FreeableB h d.pending_buf) (hw : FreeableB h d.window)
70    (hq : FreeableW h d.head) (hp : FreeableW h d.prev)
71    (hwb : d.pending_buf = .null ∨ d.window = .null ∨ d.pending_buf ≠ d.window)
72    (hpq : d.head = .null ∨ d.prev = .null ∨ d.head ≠ d.prev) :
73    deflateEnd (some r) h =
74      .ok ((if d.status == BUSY_STATE then Z_DATA_ERROR else Z_OK), endHeap h r ds z d) := by
75  have hq1 : FreeableW (freeBytes h d.pending_buf) d.head := by
76    simpa only [FreeableW, freeBytes_words] using hq
77  have hp1 : FreeableW (freeBytes h d.pending_buf) d.prev := by
78    simpa only [FreeableW, freeBytes_words] using hp
79  have hp2 := freeableW_after hp1 hq1 hpq
80  have hw1 := freeableB_after hw hb hwb
81  have hw3 : FreeableB (freeWords (freeWords (freeBytes h d.pending_buf) d.head) d.prev) d.window := by
82    simpa only [FreeableB, freeWords_bytes, freeWords_ro] using hw1
83  unfold deflateEnd
84  simp only [bind_app, stateCheck_live hl, bne_self_eq_false, Bool.false_eq_true, ite_false,
85    zrd_eq, hl.hz, hl.zst, castD, rdD_eq, hl.hs]
86  rw [freeB_continue hl.hz hf hb]
87  simp only [bind_app, rdD_eq, freeBytes_dstates, hl.hs]
88  rw [freeW_continue (by simpa using hl.hz) hf hq1]
89  simp only [bind_app, rdD_eq, freeWords_dstates, freeBytes_dstates, hl.hs]
90  rw [freeW_continue (by simpa using hl.hz) hf hp2]
91  simp only [bind_app, rdD_eq, freeWords_dstates, freeBytes_dstates, hl.hs]
92  rw [freeB_continue (by simpa using hl.hz) hf hw3]
93  rw [bind_app, zfree_default_run (by simpa using hl.hz) hf]
94  simp only []
95  rw [bind_app, freeDeflateState_free_ok (d := d) (by simpa using hl.hs)]
96  simp only [zwr_eq, ZStreamRef.get_dstates, ZStreamRef.get_freeBytes, ZStreamRef.get_freeWords,
97    hl.hz, bind_app, pure_app, ZStreamRef.put_with_dstates, endHeap, freeBytes_dstates, freeWords_dstates]
98
99end Zlib.Deflate.Proofs.DefaultInit