public-inflate-end.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.Lifecycle
2import ZlibF.Proof.«inflate.c.end»
3
4open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.InflateEndProof
7
8theorem end_frame {h : Heap} {r : ZStreamRef} {i : Nat} {z : ZStream} {s : InflateState}
9    (hz : r.get h = some z) (hw : s.window = .null ∨ ∃ b a, s.window = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false) :
10    Frame h (r.put (endHeap h i s) {z with state := none}) (fun b => StreamRoot r b ∨ InflateOwned i s b) := by
11  rcases hw with hnull | ⟨w,a,hwin,ha,hro⟩
12  · cases r with
13    | tab j =>
14      have hjz : h.streams j = some z := hz
15      simp only [Frame, endHeap, freeIst, freeWin, hnull, ZStreamRef.put, hjz, true_and]
16      refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
17      intro b hl hb
18      have hi : b ≠ i := fun e => hb (Or.inr (Or.inl e))
19      have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
20      simp [upd_ne, hi, hj]
21    | in_gzstate_strm j =>
22      cases hg : h.gzstates j with
23      | none => simp [ZStreamRef.get, hg] at hz
24      | some g =>
25        simp only [Frame, endHeap, freeIst, freeWin, hnull, ZStreamRef.put, hg, true_and]
26        refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
27        intro b hl hb
28        have hi : b ≠ i := fun e => hb (Or.inr (Or.inl e))
29        have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
30        simp [upd_ne, hi, hj]
31  · cases r with
32    | tab j =>
33      have hjz : h.streams j = some z := hz
34      simp only [Frame, endHeap, freeIst, freeWin, hwin, ZStreamRef.put, hjz, true_and]
35      refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
36      intro b hl hb
37      have hi : b ≠ i := fun e => hb (Or.inr (Or.inl e))
38      have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
39      have hw : b ≠ w := fun e => hb (Or.inr (Or.inr (by simpa [hwin] using e.symm)))
40      simp [upd_ne, hi, hj, hw]
41    | in_gzstate_strm j =>
42      cases hg : h.gzstates j with
43      | none => simp [ZStreamRef.get, hg] at hz
44      | some g =>
45        simp only [Frame, endHeap, freeIst, freeWin, hwin, ZStreamRef.put, hg, true_and]
46        refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
47        intro b hl hb
48        have hi : b ≠ i := fun e => hb (Or.inr (Or.inl e))
49        have hj : b ≠ j := fun e => hb (Or.inl (by simpa [StreamRoot] using e))
50        have hw : b ≠ w := fun e => hb (Or.inr (Or.inr (by simpa [hwin] using e.symm)))
51        simp [upd_ne, hi, hj, hw]
52
53/-- `int inflateEnd(z_streamp strm)`
54The exact public result, state, frame and ownership contract. -/
55theorem inflate_end_public : Goal.inflateEnd := by
56  intro h r i z s hG hf
57  obtain ⟨after, hr, he, hu, hfr, hz, hown, hc⟩ := inflateEnd_safe hG hf
58  refine ⟨after, hr, hz, ?_, ?_, ?_, ?_⟩
59  · have ho := hown (fun b => h.live b) (fun _ => Iff.rfl)
60    intro b
61    simpa [LiveChange, InflateOwned, OwnedBy, WinBlk, and_comm] using ho b
62  · rw [he]
63    exact end_frame hG.live.hz (windowBlock hG.inv.win)
64  · rw [he]
65    rcases windowBlock hG.inv.win with hnull | ⟨w,a,hwin,ha,hro⟩
66    · cases r <;> simp [endHeap, freeIst, freeWin, ZStreamRef.put, hnull] <;> split <;> rfl
67    · cases r <;> simp [endHeap, freeIst, freeWin, ZStreamRef.put, hwin] <;> split <;> rfl
68  · rw [he]
69    rcases windowBlock hG.inv.win with hnull | ⟨w,a,hwin,ha,hro⟩
70    · cases r <;> simp [endHeap, freeIst, freeWin, ZStreamRef.put, hnull] <;> split <;> rfl
71    · cases r <;> simp [endHeap, freeIst, freeWin, ZStreamRef.put, hwin] <;> split <;> rfl
72
73#print axioms inflate_end_public
74
75end ZlibF.Spec.Public.InflateEndProof