HeapCleanup.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
2namespace ZlibF.Spec.Public.Proofs
3open C Zlib.GzFs Zlib.Gzlib
4
5def messageState : GzState := { (default : GzState) with mode := GZ_READ, path := .ref (.blk 0) 0, msg := .ref (.blk 1) 0, want := 8, err := Z_OK }
6def messageHeap : Heap := { Heap.empty with
7  bytes := ⟨#[some #[0], some #[0]]⟩,
8  gzstates := ⟨#[none, none, some messageState]⟩,
9  nextBlk := 3,
10  static := Zlib.Crc32.initStatics (Zlib.Inftrees.initStatics (Zlib.Trees.trees_statics Heap.empty.static)) }
11
12theorem messageHeap_valid : GzValid messageHeap 2 messageState := by
13  unfold GzValid
14  refine ⟨rfl, Or.inl rfl, ?_, ?_, rfl, ?_, ?_, ?_, by decide, by decide, ?_, ?_⟩
15  · intro b hb
16    change 3 ≤ b at hb
17    have hbytes : (#[some #[0], some #[0]] : Array (Option (Array UInt8)))[b]? = none :=
18      Array.getElem?_eq_none (by simp; omega)
19    have hstates : (#[none, none, some messageState] : Array (Option GzState))[b]? = none :=
20      Array.getElem?_eq_none (by simp; omega)
21    simp [Heap.live, messageHeap, Heap.empty, Tbl.get, Tbl.empty, hbytes, hstates] <;> decide
22  · intro b
23    by_cases h0 : b = 0
24    · subst b; decide
25    by_cases h1 : b = 1
26    · subst b; decide
27    by_cases h2 : b = 2
28    · subst b; decide
29    have hb : 3 ≤ b := by omega
30    have hbytes : (#[some #[0], some #[0]] : Array (Option (Array UInt8)))[b]? = none :=
31      Array.getElem?_eq_none (by simp; omega)
32    have hstates : (#[none, none, some messageState] : Array (Option GzState))[b]? = none :=
33      Array.getElem?_eq_none (by simp; omega)
34    simp [Zlib.Gzlib.Spec.cnt, messageHeap, Heap.empty, Tbl.get, Tbl.empty, hbytes, hstates] <;> decide
35  · refine ⟨[], ?_, 0, #[0], rfl, rfl, rfl, by decide⟩
36    exact ⟨Or.inr ⟨.blk 0, 0, #[0], rfl, rfl, by decide, rfl⟩, by simp, by decide⟩
37  · right
38    refine ⟨[], ?_, 1, #[0], rfl, rfl, rfl, by decide⟩
39    exact ⟨Or.inr ⟨.blk 1, 0, #[0], rfl, rfl, by decide, rfl⟩, by simp, by decide⟩
40  · intro he; cases he
41  · intro he; exact (he rfl).elim
42  · intro he; exact (he rfl).elim
43
44
45def clearedMessageHeap : Heap :=
46  putGz { messageHeap with bytes := upd messageHeap.bytes 1 none } 2
47    { messageState with eof := 0, past := 0, err := Z_OK, msg := .null }
48
49theorem clear_message_witness : C.run (gzclearerr (some (.in_gzstate_x 2))) messageHeap = .ok ((), clearedMessageHeap) := by
50  rfl
51
52
53/-- The source allocator's free operation removes only bytes. It does not resize or clear
54the read-only table. This covers the byte-block effect shared by reset and message cleanup. -/
55theorem free_writable_matches_dropWindow (h : Heap) (p : BPtr) (valid : WindowAllocation h p) :
56    C.run (freeB p) h = .ok ((), dropWindow h p) := by
57  rcases valid with rfl | ⟨b, bytes, rfl, hb, hr⟩
58  · rfl
59  · simp [C.run, freeB, dropWindow, hb, hr]
60
61/-- Freeze the former mistaken update solely to retain the counterexample. -/
62def legacyDropWindow (h : Heap) : BPtr → Heap
63  | .ref (.blk b) 0 => { h with bytes := upd h.bytes b none, ro := upd h.ro b false }
64  | _ => h
65
66/-- The corrected contract agrees with the actual function on a valid public-domain heap. -/
67theorem clear_message_matches_contract :
68    C.run (gzclearerr (some (.in_gzstate_x 2))) messageHeap =
69      .ok ((), putGz (dropWindow messageHeap messageState.msg) 2
70        { messageState with eof := 0, past := 0, err := Z_OK, msg := .null }) := by
71  rfl
72
73/-- The legacy whole-heap equality fails although all public-domain preconditions hold. -/
74theorem clear_message_rejects_legacy_update :
75    C.run (gzclearerr (some (.in_gzstate_x 2))) messageHeap ≠
76      .ok ((), putGz (legacyDropWindow messageHeap messageState.msg) 2
77        { messageState with eof := 0, past := 0, err := Z_OK, msg := .null }) := by
78  intro he
79  rw [clear_message_witness] at he
80  have hh := congrArg (fun p : Unit × Heap => p.2) (Except.ok.inj he)
81  have sizes := congrArg (fun h : Heap => h.ro.arr.size) hh
82  change 0 = 2 at sizes
83  omega
84
85end ZlibF.Spec.Public.Proofs