DictionaryRoundtrip.lean

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

1import ZlibF.Proof.Api.GzipRoundtrip
2
3namespace ZlibF.Spec.Api.Proofs
4open ZlibF.Spec
5
6private theorem be32_inj (a b : UInt32) (h : be32 a.toNat = be32 b.toNat) : a = b := by
7  apply UInt32.toNat_inj.mp
8  simp only [be32, List.cons.injEq, and_true] at h
9  obtain ⟨h1, h2, h3, h4⟩ := h
10  have h1 := congrArg UInt8.toNat h1
11  have h2 := congrArg UInt8.toNat h2
12  have h3 := congrArg UInt8.toNat h3
13  have h4 := congrArg UInt8.toNat h4
14  simp only [UInt8.toNat_ofNat', Nat.mod_mod, Nat.toUInt8] at h1 h2 h3 h4
15  have ha : a.toNat < 2 ^ 32 := a.toFin.isLt
16  have hb : b.toNat < 2 ^ 32 := b.toFin.isLt
17  omega
18
19/-- A completed zlib trace with a nonempty dictionary announces and decodes that dictionary. -/
20theorem dict_trace_format {p : DeflParams} {d x : List UInt8} {sd : DeflState}
21    (hc : DeflCfg p) (hw : p.wrap = .zlib) (ht : DeflTrace x (DeflState.fresh p) sd)
22    (hd : sd.done = true) (hp : sd.precise = true) (hi : sd.input = x)
23    (hdy : sd.dict = some d) (hn : d ≠ []) :
24    Layer.Decodes .zlib 15 d sd.produced x ∧
25      ∀ d', adler32 d' ≠ adler32 d → ¬ Zlib.Decodes d' sd.produced x := by
26  have heff : sd.dictEff = d := by simp [DeflState.dictEff, hdy]
27  have hz : Layer.Decodes .zlib 15 d sd.produced x := by
28    simpa [heff] using zlib_trace_decodes hc hw ht hd hp hi (Or.inl rfl)
29  refine ⟨hz, ?_⟩
30  intro d' hne hz'
31  have hparam : sd.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
32  have hv := deflate_valid p x sd hc ht hd hp
33  have hv' : Zlib.Decodes d sd.produced x ∧
34      sd.produced.head?.map (·.toNat / 16 + 8) = some p.wbits ∧
35      ∃ cmf flg r, sd.produced = cmf :: flg :: r ∧ (flg.toNat / 32 % 2 = 1 ↔ d ≠ []) := by
36    simpa [DeflState.Valid, hparam, hw, hi, heff] using hv
37  obtain ⟨cmf, flg, rest, hs, hflag⟩ := hv'.2.2
38  have hset : flg.toNat / 32 % 2 = 1 := hflag.mpr hn
39  obtain ⟨cmf1, flg1, pre1, body1, hs1, _, _, hdict1⟩ := hv'.1
40  obtain ⟨cmf2, flg2, pre2, body2, hs2, _, _, hdict2⟩ := hz'
41  have he1 := hs1
42  rw [hs] at he1
43  simp only [List.cons.injEq] at he1
44  obtain ⟨rfl, rfl, _⟩ := he1
45  have he2 := hs2
46  rw [hs] at he2
47  simp only [List.cons.injEq] at he2
48  obtain ⟨rfl, rfl, _⟩ := he2
49  have hpre1 := (hdict1 hset).1
50  have hpre2 := (hdict2 hset).1
51  rw [hpre1] at hs1
52  rw [hpre2] at hs2
53  rw [hs1] at hs2
54  simp only [List.cons.injEq] at hs2
55  have hid := List.append_inj_left hs2.2.2 (by simp [ZlibF.Spec.be32_length])
56  exact hne (be32_inj _ _ hid.symm)
57
58private def NeedInvariant (s : InflState) : Prop :=
59  s.wrap = .zlib ∧ (s.phase = .needDict → s.seen.length = 6)
60
61private theorem need_dict_step {s s' : InflState} {d : List UInt8} {rc : Int}
62    (hd : InflSetDict s d rc s') (hinv : NeedInvariant s) : NeedInvariant s' := by
63  obtain ⟨hw, hneed⟩ := hinv
64  simp only [InflSetDict, hw] at hd
65  split at hd
66  · split at hd
67    · rcases hd with ⟨_, rfl⟩ | ⟨_, rfl⟩ <;> simp [NeedInvariant]
68    · rcases hd with ⟨_, rfl⟩
69      exact ⟨hw, hneed⟩
70  · rcases hd with ⟨_, rfl⟩
71    exact ⟨hw, hneed⟩
72
73private theorem need_inflate_step {s s' : InflState} {c : InflCall} {o : InflOut}
74    (hr : InflStep s c o s') (hinv : NeedInvariant s) : NeedInvariant s' := by
75  obtain ⟨hw, hneed⟩ := hinv
76  by_cases hb : c.badBuf = true
77  · rw [(hr.1 hb).2.2.2]
78    exact ⟨hw, hneed⟩
79  have hbuf : c.badBuf = false := by cases he : c.badBuf <;> simp_all
80  have hrun := hr.2 hbuf
81  cases hp : s.phase with
82  | done | bad | mem | needDict | syncing =>
83    simp only [hp] at hrun
84    rw [hrun.2.2.2]
85    exact ⟨hw, hneed⟩
86  | running =>
87    simp only [hp] at hrun
88    rcases hrun with hrun | hrun
89    · rcases hrun with ⟨_, _, hseen, _, _, _, hwrap, _, _, _, _, _, _, _, hrc, hok,
90        hbuferr, hend, hbad, hneed', _, _, _, _, _, _, _, _, _, _⟩
91      refine ⟨hwrap.trans hw, fun hphase => ?_⟩
92      rcases hrc with hrc | hrc | hrc | hrc | hrc
93      · have he := (hok hrc).2.2
94        rw [he] at hphase; cases hphase
95      · have he := hend hrc
96        rw [he] at hphase; cases hphase
97      · rw [hseen]
98        exact (hneed' hrc).2.2.2.1
99      · have he := hbad hrc
100        rw [he] at hphase; cases hphase
101      · have he := (hbuferr hrc).2
102        rw [he] at hphase; cases hphase
103    · rcases hrun with ⟨_, _, _, _, hphase', _, _, _, _, _, hwrap, _, _, _, _, _, _, _, _, _, _⟩
104      refine ⟨hwrap.trans hw, fun he => ?_⟩
105      rw [hphase'] at he; cases he
106
107/-- A zlib trace can wait for a dictionary only after reading six bytes. -/
108theorem need_dict_seen_length {z d : List UInt8} {s : InflState}
109    (ht : InflTrace z d (InflState.fresh .zlib 15) s) (hn : s.phase = .needDict) :
110    s.seen.length = 6 := by
111  have keep : ∀ {a b : InflState}, InflTrace z d a b → NeedInvariant a → NeedInvariant b := by
112    intro a b trace
113    induction trace with
114    | nil => exact id
115    | step _ hm _ ih => intro h; exact ih (need_inflate_step hm.1 h)
116    | dict hm _ ih => intro h; exact ih (need_dict_step hm h)
117  have initial : NeedInvariant (InflState.fresh .zlib 15) := by simp [NeedInvariant, InflState.fresh]
118  exact (keep ht initial).2 hn
119
120/-- The full dictionary round trip in the abstract API and format models. -/
121theorem dict_roundtrip : Goal.dict_roundtrip := by
122  intro p d x sd hc hw ht hd hp hi hdict hnonempty
123  obtain ⟨hdecode, hwrong⟩ := dict_trace_format hc hw ht hd hp hi hdict hnonempty
124  refine ⟨hdecode, hwrong, ?_⟩
125  intro st d' rc st' htrace hneed hset hneq
126  have htrace' : InflTrace sd.produced d (InflStart .zlib 15 d) st := by
127    simpa [InflStart] using htrace
128  obtain ⟨hwrap, _, _, _, _, _, _, hprefix, _, _⟩ :=
129    inflate_trace_fields hdecode (Or.inl rfl) htrace'
130  have hlen := need_dict_seen_length htrace hneed
131  have hseen : st.seen = sd.produced.take 6 := by
132    have he := List.prefix_iff_eq_take.mp hprefix
133    simpa [hlen] using he
134  have hparam : sd.params = p := by simpa [DeflState.fresh] using deflate_trace_params ht
135  have heff : sd.dictEff = d := by simp [DeflState.dictEff, hdict]
136  have hv := deflate_valid p x sd hc ht hd hp
137  have hv' : Zlib.Decodes d sd.produced x ∧
138      sd.produced.head?.map (·.toNat / 16 + 8) = some p.wbits ∧
139      ∃ cmf flg r, sd.produced = cmf :: flg :: r ∧ (flg.toNat / 32 % 2 = 1 ↔ d ≠ []) := by
140    simpa [DeflState.Valid, hparam, hw, hi, heff] using hv
141  obtain ⟨cmf, flg, rest, hs, hflag⟩ := hv'.2.2
142  have hflag' : flg.toNat / 32 % 2 = 1 := hflag.mpr hnonempty
143  obtain ⟨cmf', flg', pre, body, hs', _, _, hwith⟩ := hv'.1
144  have hheads := hs'
145  rw [hs] at hheads
146  simp only [List.cons.injEq] at hheads
147  obtain ⟨rfl, rfl, _⟩ := hheads
148  have hpref := (hwith hflag').1
149  rw [hpref] at hs'
150  have hfirst : st.seen.drop 2 = be32 (adler32 d).toNat := by
151    rw [hseen, hs']
152    simp [be32]
153  have hbad : st.seen.drop 2 ≠ be32 (adler32 d').toNat := by
154    rw [hfirst]
155    intro he
156    exact hneq (be32_inj _ _ he.symm)
157  simp [InflSetDict, hwrap, hneed, hbad] at hset
158  exact hset.1
159
160#print axioms dict_roundtrip
161#print axioms need_dict_seen_length
162#print axioms dict_trace_format
163end ZlibF.Spec.Api.Proofs