inftrees.c.final-layout.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inftrees.c.step»
2
3/-! Retain the actual last iteration's layout fields. The ordinary loop
4postcondition intentionally keeps only the facts needed for safety; these
5partial-correctness lemmas preserve the additional fields on that same run. -/
6
7namespace Zlib.Inftrees.Proofs
8open C Zlib.Inftrees
9set_option autoImplicit false
10
11private theorem bind_return {α β : Type} {m : M α} {f : α → M β}
12    {h after : Heap} {value : β} (run : (m >>= f) h = .ok (value, after)) :
13    ∃ a middle, m h = .ok (a, middle) ∧ f a middle = .ok (value, after) := by
14  cases first : m h with
15  | error fault => simp only [bind_app, first] at run; contradiction
16  | ok pair => exact ⟨pair.1, pair.2, rfl, by simpa only [bind_app, first] using run⟩
17
18private theorem while_projection {σ α : Type} (project : σ → α) (test : σ → Bool)
19    (body : σ → M σ)
20    (preserves : ∀ s h result after, body s h = .ok (result, after) → project result = project s)
21    {s result : σ} {h after : Heap}
22    (run : cwhile (fun s => pure (test s, s)) body s h = .ok (result, after)) :
23    project result = project s := by
24  have go : ∀ n s h, cwhile.go (fun s => pure (test s, s)) body n s h =
25      .ok (result, after) → project result = project s := by
26    intro n
27    induction n with
28    | zero => intro s h run; cases run
29    | succ n ih =>
30      intro s h run
31      simp only [cwhile.go, bind_app, pure_app] at run
32      split at run
33      · obtain ⟨next, middle, first, rest⟩ := bind_return run
34        exact (ih next middle rest).trans (preserves s h next middle first)
35      · cases run; rfl
36  exact go fuel s h run
37
38private theorem doWhile_projection {σ α : Type} (project : σ → α) (test : σ → Bool)
39    (body : σ → M σ)
40    (preserves : ∀ s h result after, body s h = .ok (result, after) → project result = project s)
41    {s result : σ} {h after : Heap}
42    (run : cdoWhile body (fun s => pure (test s, s)) s h = .ok (result, after)) :
43    project result = project s := by
44  have go : ∀ n s h, cdoWhile.go body (fun s => pure (test s, s)) n s h =
45      .ok (result, after) → project result = project s := by
46    intro n
47    induction n with
48    | zero => intro s h run; cases run
49    | succ n ih =>
50      intro s h run
51      change (body s >>= fun next => do
52        let (again, next) ← (pure (test next, next) : M (Bool × σ))
53        if again then cdoWhile.go body (fun s => pure (test s, s)) n next else pure next) h = _ at run
54      obtain ⟨next, middle, first, rest⟩ := bind_return run
55      simp only [bind_app, pure_app] at rest
56      split at rest
57      · exact (ih next middle rest).trans (preserves s h next middle first)
58      · cases rest
59        exact preserves s h result after first
60  exact go fuel s h run
61
62private def retained (s : TS) : TS :=
63  { s with low := 0, min := 0, fill := 0, incr := 0, here := default, left := 0 }
64
65private def layout (s : TS) : UInt32 × UInt32 × UInt32 × UInt32 × CodePtr :=
66  (s.len, s.curr, s.drop, s.used, s.next)
67
68private theorem jp1_last_layout {c : Ctx} {s result : TS} {h after : Heap}
69    (max : s.len = c.max) (inside : s.len.toNat < s.count.size)
70    (last : s.count[s.len.toNat] = 1)
71    (run : jp1 c s h = .ok (result, after)) : layout result = layout s := by
72  unfold jp1 at run
73  simp only [geta_eq inside, bind_app, pure_app, last] at run
74  try dsimp only at run
75  rw [seta_eq inside] at run
76  simp only [bind_app, pure_app, UInt16.sub_self, beq_self_eq_true, ite_true] at run
77  simp only [max, beq_self_eq_true, ite_true, pure_app] at run
78  cases run
79  simp only [layout, max]
80
81private theorem jp1_last_huff {c : Ctx} {s result : TS} {h after : Heap}
82    (max : s.len = c.max) (inside : s.len.toNat < s.count.size)
83    (last : s.count[s.len.toNat] = 1)
84    (run : jp1 c s h = .ok (result, after)) : result.huff = s.huff := by
85  unfold jp1 at run
86  simp only [geta_eq inside, bind_app, pure_app, last] at run
87  rw [seta_eq inside] at run
88  simp only [bind_app, pure_app, UInt16.sub_self, beq_self_eq_true, ite_true] at run
89  simp only [max, beq_self_eq_true, ite_true, pure_app] at run
90  cases run
91  rfl
92
93private theorem hereTop_jp0_cut {c : Ctx} {s result : TS} {h after : Heap}
94    (run : hereTop c s h = .ok (result, after)) :
95    ∃ here middle, jp0 c { s with here := here } middle = .ok (result, after) := by
96  unfold hereTop at run
97  obtain ⟨w, h1, _, run⟩ := bind_return run
98  split at run
99  · obtain ⟨w2, h2, _, run⟩ := bind_return run
100    exact ⟨_, h2, run⟩
101  · obtain ⟨w2, h2, _, run⟩ := bind_return run
102    split at run
103    · obtain ⟨w3, h3, _, run⟩ := bind_return run
104      obtain ⟨extra, h4, _, run⟩ := bind_return run
105      obtain ⟨w4, h5, _, run⟩ := bind_return run
106      obtain ⟨base, h6, _, run⟩ := bind_return run
107      exact ⟨_, h6, run⟩
108    · exact ⟨_, h2, run⟩
109
110private theorem jp0_single_huff {c : Ctx} {s result : TS} {h after : Heap}
111    (len : s.len = 1) (max : s.len = c.max) (huff : s.huff = 0)
112    (inside : s.len.toNat < s.count.size) (last : s.count[s.len.toNat] = 1)
113    (run : jp0 c s h = .ok (result, after)) : result.huff = 1 := by
114  unfold jp0 at run
115  obtain ⟨incr, h1, _, run⟩ := bind_return run
116  obtain ⟨fill, h2, _, run⟩ := bind_return run
117  obtain ⟨filled, h3, fillRun, run⟩ := bind_return run
118  have frame := doWhile_projection retained (fun s : TS => s.fill != 0) _
119    (by
120      intro before h value after run
121      obtain ⟨hd, middle, _, run⟩ := bind_return run
122      obtain ⟨ignored, middle', _, run⟩ := bind_return run
123      cases run
124      rfl) fillRun
125  have lenFill : filled.len = s.len := by simpa only [retained] using congrArg TS.len frame
126  have countFill : filled.count = s.count := by simpa only [retained] using congrArg TS.count frame
127  have huffFill : filled.huff = 0 := by
128    have equality : filled.huff = s.huff := by simpa only [retained] using congrArg TS.huff frame
129    exact equality.trans huff
130  obtain ⟨incr2, h4, incrRun, run⟩ := bind_return run
131  rw [lenFill, len] at incrRun
132  change Except.ok ((1 : UInt32), h3) = Except.ok (incr2, h4) at incrRun
133  cases incrRun
134  obtain ⟨incremented, h5, incrementRun, run⟩ := bind_return run
135  have stopped : cwhile (fun s : TS => pure (s.huff &&& s.incr != 0, s))
136      (fun s => pure { s with incr := s.incr >>> 1 }) { filled with incr := 1 } h3 =
137      .ok ({ filled with incr := 1 }, h3) := by
138    unfold cwhile
139    change cwhile.go _ _ (18446744073709551615 + 1) _ _ = _
140    rw [cwhile.go]
141    simp [huffFill]
142  rw [stopped] at incrementRun
143  cases incrementRun
144  dsimp only at run
145  have branch : ((1 : UInt32) != 0) = true := rfl
146  rw [ite_eq_left branch] at run
147  have value : (filled.huff &&& ((1 : UInt32) - 1)) + 1 = 1 := by rw [huffFill]; rfl
148  rw [value] at run
149  exact jp1_last_huff (s := { filled with incr := 1, huff := 1 })
150    (by exact lenFill.trans max) (by simpa only [lenFill, countFill] using inside)
151    (by simpa only [lenFill, countFill] using last) run
152
153/-- The accepted incomplete singleton leaves huff at one, so the final
154invalid entry is actually written rather than merely allowed by the post. -/
155theorem hereTop_single_huff {c : Ctx} {s result : TS} {h after : Heap}
156    (len : s.len = 1) (max : s.len = c.max) (huff : s.huff = 0)
157    (inside : s.len.toNat < s.count.size) (last : s.count[s.len.toNat] = 1)
158    (run : hereTop c s h = .ok (result, after)) : result.huff = 1 := by
159  obtain ⟨here, middle, cut⟩ := hereTop_jp0_cut run
160  exact jp0_single_huff (s := { s with here := here }) len max huff inside last cut
161
162/-- A final symbol's fill and bit-increment loops preserve its allocation
163layout. The final count decrement stops before any new subtable is opened. -/
164private theorem jp0_last_layout {c : Ctx} {s result : TS} {h after : Heap}
165    (max : s.len = c.max) (inside : s.len.toNat < s.count.size)
166    (last : s.count[s.len.toNat] = 1)
167    (run : jp0 c s h = .ok (result, after)) : layout result = layout s := by
168  unfold jp0 at run
169  obtain ⟨incr, h1, _, run⟩ := bind_return run
170  obtain ⟨fill, h2, _, run⟩ := bind_return run
171  obtain ⟨filled, h3, fillRun, run⟩ := bind_return run
172  have fillFrame := doWhile_projection retained (fun s : TS => s.fill != 0) _
173    (by
174      intro before h value after run
175      obtain ⟨hd, middle, _, run⟩ := bind_return run
176      obtain ⟨unit, middle', _, run⟩ := bind_return run
177      cases run
178      rfl) fillRun
179  have len : filled.len = s.len := by simpa only [retained] using congrArg TS.len fillFrame
180  have count : filled.count = s.count := by simpa only [retained] using congrArg TS.count fillFrame
181  have fields : layout filled = layout s := by simpa only [retained, layout] using congrArg layout fillFrame
182  obtain ⟨incr2, h4, _, run⟩ := bind_return run
183  obtain ⟨incremented, h5, incrementRun, run⟩ := bind_return run
184  have incrementFrame := while_projection retained (fun s : TS => s.huff &&& s.incr != 0) _
185    (by intro before h value after run; cases run; rfl) incrementRun
186  have len' : incremented.len = filled.len := by
187    simpa only [retained] using congrArg TS.len incrementFrame
188  have count' : incremented.count = filled.count := by
189    simpa only [retained] using congrArg TS.count incrementFrame
190  have fields' : layout incremented = layout filled := by
191    simpa only [retained, layout] using congrArg layout incrementFrame
192  have len2 := len'.trans len
193  have count2 := count'.trans count
194  have fields2 := fields'.trans fields
195  have final : ∀ huff, jp1 c { incremented with huff := huff } h5 = .ok (result, after) →
196      layout result = layout s := by
197    intro huff run
198    exact (jp1_last_layout (s := { incremented with huff := huff }) (by exact len2.trans max)
199      (by simpa only [len2, count2] using inside)
200      (by simpa only [len2, count2] using last) run).trans fields2
201  dsimp only at run
202  split at run
203  all_goals exact final _ run
204
205/-- The actual last iteration retains len, curr, drop, used and next.
206This complements, rather than assumes or changes, hereTop_wp. -/
207theorem hereTop_last_layout {c : Ctx} {s result : TS} {h after : Heap}
208    (max : s.len = c.max) (inside : s.len.toNat < s.count.size)
209    (last : s.count[s.len.toNat] = 1)
210    (run : hereTop c s h = .ok (result, after)) :
211    result.len = s.len ∧ result.curr = s.curr ∧ result.drop = s.drop ∧
212      result.used = s.used ∧ result.next = s.next := by
213  have fields : layout result = layout s := by
214    have final : ∀ here middle, jp0 c { s with here := here } middle = .ok (result, after) →
215        layout result = layout s := by
216      intro here middle run
217      exact jp0_last_layout (s := { s with here := here }) max inside last run
218    unfold hereTop at run
219    obtain ⟨w, h1, _, run⟩ := bind_return run
220    split at run
221    · obtain ⟨w2, h2, _, run⟩ := bind_return run
222      exact final _ _ run
223    · obtain ⟨w2, h2, _, run⟩ := bind_return run
224      split at run
225      · obtain ⟨w3, h3, _, run⟩ := bind_return run
226        obtain ⟨extra, h4, _, run⟩ := bind_return run
227        obtain ⟨w4, h5, _, run⟩ := bind_return run
228        obtain ⟨base, h6, _, run⟩ := bind_return run
229        exact final _ _ run
230      · exact final _ _ run
231  exact ⟨congrArg Prod.fst fields, congrArg (fun p => p.2.1) fields,
232    congrArg (fun p => p.2.2.1) fields, congrArg (fun p => p.2.2.2.1) fields,
233    congrArg (fun p => p.2.2.2.2) fields⟩
234
235/-- The final iteration has exactly one remaining code of its length. -/
236theorem MI_final_entry {e : Env} {i : Nat} {s : TS} {ca : Array Code}
237    (inv : MI e i s ca) (final : i + 1 = e.m) :
238    s.len = e.c.max ∧ ∃ inside : s.len.toNat < s.count.size,
239      s.count[s.len.toNat]'inside = 1 := by
240  have hi : i < Tc e.f e.n 15 := inv.1
241  have len : s.len.toNat = lenAt e.f e.n i := inv.2.2.2.1
242  have count := inv.2.2.2.2.2.2.1
243  have interval := lenAt_bounds (f := e.f) (n := e.n) hi
244  have maxLen : e.l i = e.mx := by
245    change lenAt e.f e.n i = lenAt e.f e.n (Tc e.f e.n 15 - 1)
246    congr 1
247    change i + 1 = Tc e.f e.n 15 at final
248    omega
249  have max : s.len = e.c.max := by
250    apply UInt32.toNat_inj.mp
251    rw [e.h_max]
252    exact len.trans maxLen
253  have inside : s.len.toNat < s.count.size := by rw [count.1, len]; omega
254  have counted := count.2 (lenAt e.f e.n i) interval.1 interval.2
255  have block := (lenAt_eq_iff (f := e.f) (n := e.n) interval.1 interval.2 hi).mp rfl
256  have top := Tc_mono (f := e.f) (n := e.n) interval.2
257  have last : s.count[s.len.toNat] = 1 := by
258    apply UInt16.toNat_inj.mp
259    rw [← len] at counted
260    rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem inside,
261      Option.getD_some] at counted
262    change i + 1 = Tc e.f e.n 15 at final
263    unfold rem at counted
264    conv at counted => rhs; rw [len]
265    change (s.count[s.len.toNat]).toNat = 1
266    omega
267  exact ⟨max, inside, last⟩
268
269/-- Retain the final descriptor from the actual final iteration. The last
270symbol and count hypotheses are derived from MI, not supplied by a caller. -/
271theorem hereTop_final_descriptor {e : Env} {i : Nat} {s result : TS} {ca : Array Code}
272    {after : Heap} (inv : MI e i s ca) (cells : Ex e i s ca)
273    (final : i + 1 = e.m) (run : hereTop e.c s (e.hc ca) = .ok (result, after)) :
274    DescB e i result ∧ result.drop.toNat = (e.D i).drop ∧ result.len.toNat = e.l i := by
275  have len : s.len.toNat = lenAt e.f e.n i := inv.2.2.2.1
276  obtain ⟨max, inside, last⟩ := MI_final_entry inv final
277  obtain ⟨len', curr, drop, used, next⟩ := hereTop_last_layout max inside last run
278  refine ⟨?_, ?_, by rw [len']; exact len⟩
279  · obtain ⟨⟨k, pointer, base⟩, width, extent⟩ := cells.1.1
280    exact ⟨⟨k, by rw [next]; exact pointer, base⟩,
281      by rw [curr]; exact width, by rw [used]; exact extent⟩
282  · rw [drop]
283    exact cells.1.2.1
284
285/-- The final singleton iteration's nonzero huff fact comes from its actual
286bit-increment execution. -/
287theorem hereTop_final_single_huff {e : Env} {i : Nat} {s result : TS} {ca : Array Code}
288    {after : Heap} (inv : MI e i s ca) (final : i + 1 = e.m)
289    (single : e.m = 1) (one : e.mx = 1)
290    (run : hereTop e.c s (e.hc ca) = .ok (result, after)) : result.huff = 1 := by
291  have zero : i = 0 := by omega
292  obtain ⟨max, inside, last⟩ := MI_final_entry inv final
293  have maxOne : e.c.max = 1 := by
294    apply UInt32.toNat_inj.mp
295    rw [e.h_max]
296    exact one
297  have len : s.len = 1 := max.trans maxOne
298  have huff : s.huff = 0 := by
299    apply UInt32.toNat_inj.mp
300    have value := inv.2.2.2.2.1
301    rw [zero, show e.v 0 = 0 from val_zero e.h_pos, rev_zero] at value
302    exact value
303  exact hereTop_single_huff len max huff inside last run
304
305end Zlib.Inftrees.Proofs