deflate.c.init.frame.lean

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

1import ZlibF.Proof.«deflate.c.init.success»
2
3/-! # deflate.c: old-object frame for default initialization -/
4
5namespace Zlib.Deflate.Proofs.DefaultInit
6open C Zlib.Deflate Zlib.Deflate.Spec ZlibF.Spec.Public
7set_option autoImplicit false
8
9theorem slot_put_except (h : Heap) (r : ZStreamRef) (z : ZStream) (x : Nat)
10    (hn : ¬ StreamRoot r x) : SlotSame h (r.put h z) x := by
11  cases r with
12  | tab i =>
13    have hi : x ≠ i := hn
14    simp only [ZStreamRef.put]
15    split <;> simp [SlotSame, upd_ne _ _ _ _ hi]
16  | in_gzstate_strm i =>
17    have hi : x ≠ i := hn
18    simp only [ZStreamRef.put]
19    split <;> simp [SlotSame, upd_ne _ _ _ _ hi]
20
21theorem slot_setD_except (h : Heap) (ds : Nat) (d : DeflateState) (x : Nat) (hn : x ≠ ds) :
22    SlotSame h (setD h ds d) x := by simp [SlotSame, setD, upd_ne _ _ _ _ hn]
23
24theorem slot_setW_except (h : Heap) (q : Nat) (a : Array UInt16) (x : Nat) (hn : x ≠ q) :
25    SlotSame h (setW h q a) x := by simp [SlotSame, setW, upd_ne _ _ _ _ hn]
26
27theorem slot_stateHeap_old (h : Heap) (d : DeflateState) (x : Nat) (hx : x < h.nextBlk) :
28    SlotSame h (stateHeap h d) x := by
29  simp [SlotSame, stateHeap, upd_ne _ _ _ _ (show x ≠ h.nextBlk by omega)]
30
31theorem slot_successfulBuffers_old (h : Heap) (x : Nat) (hx : x < h.nextBlk) :
32    SlotSame h (successfulBuffers h) x := by
33  have h0 : x ≠ h.nextBlk := by omega
34  have h1 : x ≠ h.nextBlk + 1 := by omega
35  have h2 : x ≠ h.nextBlk + 2 := by omega
36  have h3 : x ≠ h.nextBlk + 3 := by omega
37  simp [SlotSame, successfulBuffers, upd_ne _ _ _ _ h0, upd_ne _ _ _ _ h1,
38    upd_ne _ _ _ _ h2, upd_ne _ _ _ _ h3]
39
40theorem frame_of_old {h g : Heap} (r : ZStreamRef) (hf : Fresh h)
41    (hs : h.static = g.static) (ha : h.allocOk = g.allocOk) (hg : h.garbage = g.garbage)
42    (hn : h.nextBlk ≤ g.nextBlk) (hc : h.nalloc ≤ g.nalloc)
43    (hold : ∀ x, x < h.nextBlk → ¬ StreamRoot r x → SlotSame h g x) : Frame h g (StreamRoot r) := by
44  exact ⟨hs, ha, hg, hn, hc, fun x hl hx => hold x (hf.lt hl) hx⟩
45
46theorem SlotSame.live {h g : Heap} {x : Nat} (hs : SlotSame h g x) : g.live x ↔ h.live x := by
47  rcases hs with ⟨a, b, c, d, e, f, k, _⟩
48  simp only [Heap.live, a, b, c, d, e, f, k]
49
50theorem frame_trans {h g j : Heap} (r : ZStreamRef)
51    (a : Frame h g (StreamRoot r)) (b : Frame g j (StreamRoot r)) : Frame h j (StreamRoot r) := by
52  rcases a with ⟨as_, aa, ag, an, ac, ao⟩
53  rcases b with ⟨bs, ba, bg, bn, bc, bo⟩
54  refine ⟨as_.trans bs, aa.trans ba, ag.trans bg, Nat.le_trans an bn, Nat.le_trans ac bc, ?_⟩
55  intro x hl hn
56  have first : SlotSame h g x := ao x hl hn
57  exact first.trans (bo x (first.live.mpr hl) hn)
58
59theorem frame_put {h : Heap} (r : ZStreamRef) (z : ZStream) (hf : Fresh h) :
60    Frame h (r.put h z) (StreamRoot r) := by
61  refine frame_of_old r hf (by simp) (by simp) (by simp) (by simp) (by simp) ?_
62  exact fun x _ hn => slot_put_except h r z x hn
63
64def resultStream (h : Heap) (r : ZStreamRef) (z : ZStream) (level : Int32) : ZStream :=
65  let ph := publishedHeap h r z
66  rkZ (stateStream z h.nextBlk)
67    (readyState r level ph.nextBlk (ph.nextBlk + 1) (ph.nextBlk + 2) (ph.nextBlk + 3))
68
69def successHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (level : Int32)
70    (a1 a2 a3 : Array CtData) (qa : Array UInt16) : Heap :=
71  let ph := publishedHeap h r z
72  let rh := readyHeap ph h.nextBlk r level
73  let dr := resetState h.nextBlk r level ph.nextBlk (ph.nextBlk + 1) (ph.nextBlk + 2) (ph.nextBlk + 3) a1 a2 a3
74  setD (setW (setD (r.put rh (resultStream h r z level)) h.nextBlk dr)
75    (ph.nextBlk + 2) (clearHead qa 32768)) h.nextBlk (lmD dr)
76
77/-- Every old object outside the caller stream is retained, even though
78tree initialization and hash clearing write the newly allocated blocks. -/
79theorem success_frame {h : Heap} (r : ZStreamRef) (z : ZStream) (level : Int32)
80    (a1 a2 a3 : Array CtData) (qa : Array UInt16) (hf : Fresh h) :
81    Frame h (successHeap h r z level a1 a2 a3 qa) (StreamRoot r) := by
82  have next : (successHeap h r z level a1 a2 a3 qa).nextBlk = h.nextBlk + 5 := by
83    simp only [successHeap, setD_nextBlk, setW, readyHeap, successfulBuffers,
84      publishedHeap, stateHeap, ZStreamRef.put_nextBlk, Nat.add_assoc]
85  have count : (successHeap h r z level a1 a2 a3 qa).nalloc = h.nalloc + 5 := by
86    simp only [successHeap, setD_nalloc, setW, readyHeap, successfulBuffers,
87      publishedHeap, stateHeap, ZStreamRef.put_nalloc, Nat.add_assoc]
88  refine frame_of_old (g := successHeap h r z level a1 a2 a3 qa) r hf ?_ ?_ ?_ ?_ ?_ ?_
89  all_goals try { simp [successHeap, readyHeap, successfulBuffers, publishedHeap, stateHeap, setW] }
90  all_goals try omega
91  intro x hx hn
92  let ph := publishedHeap h r z
93  let rd := readyState r level ph.nextBlk (ph.nextBlk + 1) (ph.nextBlk + 2) (ph.nextBlk + 3)
94  let dr := resetState h.nextBlk r level ph.nextBlk (ph.nextBlk + 1)
95    (ph.nextBlk + 2) (ph.nextBlk + 3) a1 a2 a3
96  have hp : h.nextBlk < ph.nextBlk := by simp [ph, publishedHeap, stateHeap]
97  have hds : x ≠ h.nextBlk := by omega
98  have hq : x ≠ ph.nextBlk + 2 := by omega
99  have a : SlotSame h ph x :=
100    (slot_put_except h r (stateStream z h.nextBlk) x hn).trans
101      (slot_stateHeap_old _ (baseState r) x (by simpa using hx))
102  have b := a.trans (slot_successfulBuffers_old ph x (by omega))
103  have c := b.trans (slot_setD_except _ h.nextBlk rd x hds)
104  have e := c.trans (slot_put_except _ r (resultStream h r z level) x hn)
105  have f := e.trans (slot_setD_except _ h.nextBlk dr x hds)
106  have g := f.trans (slot_setW_except _ (ph.nextBlk + 2) (clearHead qa 32768) x hq)
107  exact g.trans (slot_setD_except _ h.nextBlk (lmD dr) x hds)
108
109/-- Before reset, exactly the state and four successful requests are new. -/
110theorem ready_live {h : Heap} {r : ZStreamRef} {z : ZStream}
111    (hz : r.get h = some z) (level : Int32)
112    (ha : ∀ j, j < 4 → (publishedHeap h r z).allocOk ((publishedHeap h r z).nalloc + j) = true)
113    (x : Nat) :
114    (readyHeap (publishedHeap h r z) h.nextBlk r level).live x ↔
115      h.live x ∨ h.nextBlk ≤ x ∧ x < h.nextBlk + 5 := by
116  let ph := publishedHeap h r z
117  have he := (buffers_success ph ha).1
118  have hp := (buffers_success ph ha).2
119  have hs : (successfulBuffers ph).dstates h.nextBlk = some (baseState r) := by
120    simp [successfulBuffers, ph, publishedHeap, stateHeap]
121  have preserved := (shape_setD hs
122    (readyState r level ph.nextBlk (ph.nextBlk + 1) (ph.nextBlk + 2) (ph.nextBlk + 3))).live x
123  change (setD (successfulBuffers ph) h.nextBlk _).live x ↔ _
124  rw [preserved, ← he, buffers_live, hp]
125  have before : ph.live x ↔ h.live x ∨ x = h.nextBlk := by
126    dsimp only [ph, publishedHeap]
127    rw [stateHeap_live, (shape_put hz (stateStream z h.nextBlk)).live]
128    simp
129  rw [before]
130  simp only [ph, publishedHeap, stateHeap, ZStreamRef.put_nextBlk]
131  by_cases hl : h.live x <;> simp [hl, eq_comm] <;> omega
132
133end Zlib.Deflate.Proofs.DefaultInit