GzRoundtrip.lean

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

1import ZlibF.Spec.Api.Examples
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec
5
6/-- Every complete gzip member has the header recognized by the gzip reader model. -/
7theorem gzip_looks_gzip {stream output : List UInt8} (hd : Gzip.Decodes stream output) :
8    GzLooksGzip stream := by
9  obtain ⟨flg, mt, xfl, os, ex, nm, cm, s, hflg, _, _, _, _, hz, _⟩ := hd
10  rw [hz, ZlibF.Spec.Proofs.header_eq]
11  simp [GzLooksGzip, hflg]
12
13/-- A successfully closed abstract gzip writer yields a file decoded to its input by the
14abstract reader. This does not establish refinement of the translated file operations. -/
15theorem gz_roundtrip : Goal.gz_roundtrip := by
16  intro h rc final hmode hbase hfailed hdirect hclose hrc
17  have hw : h.mode ≠ .read := by rw [hmode]; decide
18  obtain ⟨m, hm, _, hdecode⟩ := ((hclose.2.2.2 hw hfailed hrc).2 hdirect)
19  rw [hbase] at hm
20  simp only [List.nil_append] at hm
21  rw [hm]
22  refine Or.inr (Or.inr ⟨Or.inl (gzip_looks_gzip hdecode), [(m, h.written)], [], ?_, ?_, ?_, ?_⟩)
23  · simpa using hdecode
24  · simp
25  · rintro ⟨m', o, t, he, hd⟩
26    have hm' : m' = [] := (List.append_eq_nil_iff.mp he.symm).1
27    subst m'
28    exact gzip_empty o hd
29  · exact Or.inl ⟨rfl, by simp, by simp, rfl⟩
30
31#print axioms gzip_looks_gzip
32#print axioms gz_roundtrip
33end ZlibF.Spec.Api.Proofs