public-deflate-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.«deflate.c.life.end»
3
4open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Proofs ZlibF.Spec.Public
5
6namespace ZlibF.Spec.Public.DeflateEndProof
7
8/-- `int deflateEnd(z_streamp strm)`
9The exact public result, state, frame and ownership contract. -/
10theorem deflate_end_public : Goal.deflateEnd := by
11  intro h r i z s hG hf
12  obtain ⟨w,p,q,b,hB,after,hr,he,hz,hd,hw,hb,hp,hq,hdrest,hbrest,hwrest,hro,hgh,hist,hnext,hnalloc,hstream,hgz,hu,hfresh,hown⟩ := deflateEnd_safe hG hf
13  refine ⟨after, hr, hz, ?_, ?_, hnalloc, hnext⟩
14  · have ho := hown (fun b => h.live b) (fun _ => Iff.rfl)
15    intro x
16    have hxi : DOwned s i x ↔ DeflateOwned i s x := by
17      rw [DOwned_iff hB]
18      simp [DeflateOwned, hB.win, hB.prev, hB.head, hB.pbuf, eq_comm]
19    simpa [LiveChange, hxi] using ho x
20  · have hs : h.static = after.static := by
21      rw [he, endHeap_eq hB]
22      cases r <;> simp [ZStreamRef.put] <;> split <;> rfl
23    have ha : h.allocOk = after.allocOk := by
24      rw [he, endHeap_eq hB]
25      cases r <;> simp [ZStreamRef.put] <;> split <;> rfl
26    have hg : h.garbage = after.garbage := by
27      rw [he, endHeap_eq hB]
28      cases r <;> simp [ZStreamRef.put] <;> split <;> rfl
29    refine ⟨hs,ha,hg,by omega,by omega,?_⟩
30    intro x hx hnot
31    have hi : x ≠ i := fun e => hnot (Or.inr (Or.inl e))
32    have hw' : x ≠ w := fun e => hnot (Or.inr (Or.inr (Or.inl (by simpa [hB.win] using e.symm))))
33    have hp' : x ≠ p := fun e => hnot (Or.inr (Or.inr (Or.inr (Or.inl (by simpa [hB.prev] using e.symm)))))
34    have hq' : x ≠ q := fun e => hnot (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl (by simpa [hB.head] using e.symm))))))
35    have hb' : x ≠ b := fun e => hnot (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (by simpa [hB.pbuf] using e.symm))))))
36    refine ⟨hbrest x hw' hb', hwrest x hp' hq', ?_, by rw [hgh], hdrest x hi, by rw [hist], ?_, by rw [hro]⟩
37    · apply hstream x
38      intro j h e
39      apply hnot
40      exact Or.inl (by simpa [StreamRoot, h] using e)
41    · apply hgz x
42      intro j h e
43      apply hnot
44      exact Or.inl (by simpa [StreamRoot, h] using e)
45
46#print axioms deflate_end_public
47
48end ZlibF.Spec.Public.DeflateEndProof