CompressRoundtrip.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
6private theorem compressParams_wrap {level : Int} {p : DeflParams}
7    (h : compressParams level = some p) : p.wrap = .zlib := by
8  simp [compressParams, deflInit?] at h
9  split at h <;> rcases h with ⟨_, he⟩ <;> cases he <;> rfl
10
11private theorem compress_decodes {level : Int} {src dst : List UInt8} {cap : Nat}
12    (h : Compress2 true level src cap Z.ok dst) :
13    Zlib.Decodes [] dst src ∧ ¬ HdrNeedsDict .zlib 15 dst := by
14  cases hp : compressParams level with
15  | none => simp [Compress2, hp, Z.ok, Z.streamError] at h
16  | some p =>
17    simp only [Compress2, Bool.true_eq_false, ↓reduceIte, hp] at h
18    rcases h with ⟨he, _⟩ | ⟨_, hv, _, _⟩ | ⟨he, _, _, _⟩
19    · cases he
20    · have hw := compressParams_wrap hp
21      simp only [DeflState.Valid, DeflState.fresh, hw, DeflState.dictEff, Option.getD_none] at hv
22      refine ⟨hv.1, ?_⟩
23      rintro ⟨_, cmf, flg, rest, he, _, hflag, _⟩
24      obtain ⟨cmf', flg', rest', he', hnot⟩ := hv.2.2
25      rw [he] at he'
26      simp only [List.cons.injEq] at he'
27      obtain ⟨rfl, rfl, _⟩ := he'
28      exact (hnot.mp hflag) rfl
29    · cases he
30
31/-- The abstract compression and decompression relations round-trip without allocation failure. -/
32theorem compress_roundtrip : Goal.compress_roundtrip := by
33  intro level src cap cap2 dst src2 used rc2 hc hcap hu
34  obtain ⟨hdecode, hnodict⟩ := compress_decodes hc
35  simp only [Uncompress2, Bool.true_eq_false, ↓reduceIte] at hu
36  obtain ⟨hused, _, _, hok, _, _, _, hlive⟩ := hu
37  have hl := hlive dst.length src (Nat.le_refl _) (by simpa using hdecode)
38  have hrc : rc2 = Z.ok ∨ rc2 = Z.memError := (hl.2 (by simpa using hnodict)).1 hcap
39  constructor
40  · intro hr
41    have hdec2 := hok hr
42    have he : dst.take used ++ dst.drop used = dst := List.take_append_drop used dst
43    have hdecode' : Zlib.Decodes [] (dst.take used ++ dst.drop used) src := by simpa [he] using hdecode
44    obtain ⟨hdrop, hout⟩ := Zlib.ext hdec2 hdecode'
45    constructor
46    · exact hout
47    · have hd := congrArg List.length hdrop
48      simp only [List.length_drop, List.length_nil] at hd
49      omega
50  · intro hne
51    exact hrc.resolve_left hne
52
53#print axioms compress_roundtrip
54end ZlibF.Spec.Api.Proofs