deflate.c.init.memory.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.base»
2
3/-! # deflate.c: allocation bookkeeping for the default initializer
4
5These are exact heap effects of the existing allocator. No runtime or
6allocation semantics is changed. Integer buffer contents remain arbitrary.
7-/
8
9namespace Zlib.Deflate.Proofs.DefaultInit
10open C Zlib.Deflate Zlib.Deflate.Spec
11set_option autoImplicit false
12
13def stateHeap (h : Heap) (d : DeflateState) : Heap :=
14  { h with
15    dstates := upd h.dstates h.nextBlk (some d),
16    nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }
17
18def wordHeap (h : Heap) (n : Nat) : Heap :=
19  { h with
20    words := upd h.words h.nextBlk
21      (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
22    nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }
23
24def byteHeap (h : Heap) (n : Nat) : Heap := Zlib.Zutil.Proofs.allocHeap h n
25
26def failedHeap (h : Heap) : Heap := { h with nalloc := h.nalloc + 1 }
27
28def bytePtr (h : Heap) : BPtr := if h.allocOk h.nalloc then .ref (.blk h.nextBlk) 0 else .null
29def wordPtr (h : Heap) : WPtr := if h.allocOk h.nalloc then .ref (.blk h.nextBlk) 0 else .null
30def byteResult (h : Heap) (n : Nat) : Heap := if h.allocOk h.nalloc then byteHeap h n else failedHeap h
31def wordResult (h : Heap) (n : Nat) : Heap := if h.allocOk h.nalloc then wordHeap h n else failedHeap h
32
33@[simp] theorem get_stateHeap (h : Heap) (d : DeflateState) (r : ZStreamRef) :
34    r.get (stateHeap h d) = r.get h := by cases r <;> rfl
35
36@[simp] theorem stateHeap_dstates_same (h : Heap) (d : DeflateState) :
37    (stateHeap h d).dstates h.nextBlk = some d := by simp [stateHeap]
38
39@[simp] theorem stateHeap_dstates (h : Heap) (d : DeflateState) :
40    (stateHeap h d).dstates = upd h.dstates h.nextBlk (some d) := rfl
41
42@[simp] theorem put_stateHeap (h : Heap) (d : DeflateState) (r : ZStreamRef) (z : ZStream) :
43    r.put (stateHeap h d) z = stateHeap (r.put h z) d := by
44  cases r with
45  | tab i => simp only [stateHeap, ZStreamRef.put]; cases h.streams i <;> rfl
46  | in_gzstate_strm i => simp only [stateHeap, ZStreamRef.put]; cases h.gzstates i <;> rfl
47
48@[simp] theorem stateHeap_setD (h : Heap) (d e : DeflateState) :
49    setD (stateHeap h d) h.nextBlk e = stateHeap h e := by
50  simp [stateHeap, setD, upd_upd]
51
52@[simp] theorem stateHeap_put_setD (h : Heap) (r : ZStreamRef) (z : ZStream)
53    (d e : DeflateState) :
54    setD (stateHeap (r.put h z) d) h.nextBlk e = stateHeap (r.put h z) e := by
55  have hn : (r.put h z).nextBlk = h.nextBlk := by
56    cases r <;> simp only [ZStreamRef.put] <;> split <;> rfl
57  rw [← hn]
58  exact stateHeap_setD _ _ _
59
60theorem fresh_stateHeap {h : Heap} (hf : Fresh h) (d : DeflateState) : Fresh (stateHeap h d) := by
61  intro x hx hl
62  have hn : x ≠ h.nextBlk := by change h.nextBlk + 1 ≤ x at hx; omega
63  apply hf x (by change h.nextBlk + 1 ≤ x at hx; omega)
64  simpa only [Heap.live, stateHeap, upd_ne _ _ _ _ hn] using hl
65
66theorem fresh_wordHeap {h : Heap} (hf : Fresh h) (n : Nat) : Fresh (wordHeap h n) := by
67  intro x hx hl
68  have hn : x ≠ h.nextBlk := by change h.nextBlk + 1 ≤ x at hx; omega
69  apply hf x (by change h.nextBlk + 1 ≤ x at hx; omega)
70  simpa only [Heap.live, wordHeap, upd_ne _ _ _ _ hn] using hl
71
72theorem fresh_byteHeap {h : Heap} (hf : Fresh h) (n : Nat) : Fresh (byteHeap h n) :=
73  (Zlib.Zutil.Proofs.allocHeap_frame h n).2.1 hf
74
75theorem fresh_byteResult {h : Heap} (hf : Fresh h) (n : Nat) : Fresh (byteResult h n) := by
76  unfold byteResult
77  split
78  · exact fresh_byteHeap hf n
79  · exact hf
80
81theorem fresh_wordResult {h : Heap} (hf : Fresh h) (n : Nat) : Fresh (wordResult h n) := by
82  unfold wordResult
83  split
84  · exact fresh_wordHeap hf n
85  · exact hf
86
87theorem fresh_setD_below {h : Heap} (hf : Fresh h) (ds : Nat) (hd : ds < h.nextBlk)
88    (d : DeflateState) : Fresh (setD h ds d) := by
89  intro x hx hl
90  have hn : x ≠ ds := by change h.nextBlk ≤ x at hx; omega
91  apply hf x hx
92  simpa only [Heap.live, setD, upd_ne _ _ _ _ hn] using hl
93
94theorem uniq_stateHeap {h : Heap} (hu : Uniq h) (hf : Fresh h) (d : DeflateState) :
95    Uniq (stateHeap h d) := by
96  intro x
97  by_cases hn : x = h.nextBlk
98  · subst x
99    obtain ⟨hb, hw, hs, hg, hd, hi, hz⟩ := Heap.not_live.mp (hf _ (Nat.le_refl _))
100    simp [stateHeap, hb, hw, hs, hg, hi, hz]
101  · simpa only [Uniq, stateHeap, upd_ne _ _ _ _ hn] using hu x
102
103theorem uniq_wordHeap {h : Heap} (hu : Uniq h) (hf : Fresh h) (n : Nat) :
104    Uniq (wordHeap h n) := by
105  intro x
106  by_cases hn : x = h.nextBlk
107  · subst x
108    obtain ⟨hb, hw, hs, hg, hd, hi, hz⟩ := Heap.not_live.mp (hf _ (Nat.le_refl _))
109    simp [wordHeap, hb, hs, hg, hd, hi, hz]
110  · simpa only [Uniq, wordHeap, upd_ne _ _ _ _ hn] using hu x
111
112theorem uniq_byteHeap {h : Heap} (hu : Uniq h) (hf : Fresh h) (n : Nat) :
113    Uniq (byteHeap h n) := by
114  intro x
115  by_cases hn : x = h.nextBlk
116  · subst x
117    obtain ⟨hb, hw, hs, hg, hd, hi, hz⟩ := Heap.not_live.mp (hf _ (Nat.le_refl _))
118    simp [byteHeap, Zlib.Zutil.Proofs.allocHeap, hw, hs, hg, hd, hi, hz]
119  · simpa only [Uniq, byteHeap, Zlib.Zutil.Proofs.allocHeap, upd_ne _ _ _ _ hn] using hu x
120
121theorem byte_alloc_run {h : Heap} (hf : Fresh h) (n : Nat) :
122    allocB n h = .ok (bytePtr h, byteResult h n) := by
123  by_cases ho : h.allocOk h.nalloc = true
124  · rw [allocB_some n ho]
125    simp [bytePtr, byteResult, byteHeap, Zlib.Zutil.Proofs.allocHeap, ho]
126  · rw [allocB_none n ho]
127    simp [bytePtr, byteResult, failedHeap, ho]
128
129theorem word_alloc_run {h : Heap} (hf : Fresh h) (n : Nat) :
130    allocW n h = .ok (wordPtr h, wordResult h n) := by
131  by_cases ho : h.allocOk h.nalloc = true
132  · rw [allocW_some n ho]
133    simp [wordPtr, wordResult, wordHeap, ho]
134  · rw [allocW_none n ho]
135    simp [wordPtr, wordResult, failedHeap, ho]
136
137@[simp] theorem byteResult_nalloc (h : Heap) (n : Nat) : (byteResult h n).nalloc = h.nalloc + 1 := by
138  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
139  split <;> rfl
140@[simp] theorem wordResult_nalloc (h : Heap) (n : Nat) : (wordResult h n).nalloc = h.nalloc + 1 := by
141  unfold wordResult wordHeap failedHeap
142  split <;> rfl
143@[simp] theorem byteResult_dstates (h : Heap) (n : Nat) : (byteResult h n).dstates = h.dstates := by
144  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
145  split <;> rfl
146@[simp] theorem wordResult_dstates (h : Heap) (n : Nat) : (wordResult h n).dstates = h.dstates := by
147  unfold wordResult wordHeap failedHeap
148  split <;> rfl
149@[simp] theorem byteResult_words (h : Heap) (n : Nat) : (byteResult h n).words = h.words := by
150  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
151  split <;> rfl
152@[simp] theorem wordResult_bytes (h : Heap) (n : Nat) : (wordResult h n).bytes = h.bytes := by
153  unfold wordResult wordHeap failedHeap
154  split <;> rfl
155@[simp] theorem wordResult_ro (h : Heap) (n : Nat) : (wordResult h n).ro = h.ro := by
156  unfold wordResult wordHeap failedHeap
157  split <;> rfl
158@[simp] theorem byteResult_allocOk (h : Heap) (n : Nat) : (byteResult h n).allocOk = h.allocOk := by
159  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
160  split <;> rfl
161@[simp] theorem wordResult_allocOk (h : Heap) (n : Nat) : (wordResult h n).allocOk = h.allocOk := by
162  unfold wordResult wordHeap failedHeap
163  split <;> rfl
164@[simp] theorem get_byteResult (h : Heap) (n : Nat) (r : ZStreamRef) :
165    r.get (byteResult h n) = r.get h := by
166  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
167  split <;> cases r <;> rfl
168@[simp] theorem get_wordResult (h : Heap) (n : Nat) (r : ZStreamRef) :
169    r.get (wordResult h n) = r.get h := by
170  unfold wordResult wordHeap failedHeap
171  split <;> cases r <;> rfl
172
173@[simp] theorem byteResult_setD (h : Heap) (ds : Nat) (d : DeflateState) (n : Nat) :
174    byteResult (setD h ds d) n = setD (byteResult h n) ds d := by
175  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap setD
176  split <;> rfl
177@[simp] theorem wordResult_setD (h : Heap) (ds : Nat) (d : DeflateState) (n : Nat) :
178    wordResult (setD h ds d) n = setD (wordResult h n) ds d := by
179  unfold wordResult wordHeap failedHeap setD
180  split <;> rfl
181@[simp] theorem bytePtr_setD (h : Heap) (ds : Nat) (d : DeflateState) :
182    bytePtr (setD h ds d) = bytePtr h := rfl
183@[simp] theorem wordPtr_setD (h : Heap) (ds : Nat) (d : DeflateState) :
184    wordPtr (setD h ds d) = wordPtr h := rfl
185
186theorem byteResult_next (h : Heap) (n : Nat) : h.nextBlk ≤ (byteResult h n).nextBlk := by
187  unfold byteResult byteHeap Zlib.Zutil.Proofs.allocHeap failedHeap
188  split <;> simp
189theorem wordResult_next (h : Heap) (n : Nat) : h.nextBlk ≤ (wordResult h n).nextBlk := by
190  unfold wordResult wordHeap failedHeap
191  split <;> simp
192
193theorem uniq_byteResult {h : Heap} (hu : Uniq h) (hf : Fresh h) (n : Nat) : Uniq (byteResult h n) := by
194  unfold byteResult
195  split
196  · exact uniq_byteHeap hu hf n
197  · exact hu
198
199theorem uniq_wordResult {h : Heap} (hu : Uniq h) (hf : Fresh h) (n : Nat) : Uniq (wordResult h n) := by
200  unfold wordResult
201  split
202  · exact uniq_wordHeap hu hf n
203  · exact hu
204
205theorem byteResult_live (h : Heap) (n x : Nat) :
206    (byteResult h n).live x ↔ h.live x ∨ bytePtr h = .ref (.blk x) 0 := by
207  unfold byteResult bytePtr
208  split
209  · by_cases hx : x = h.nextBlk
210    · subst x
211      simp [Heap.live, byteHeap, Zlib.Zutil.Proofs.allocHeap]
212    · simp [Heap.live, byteHeap, Zlib.Zutil.Proofs.allocHeap, upd_ne _ _ _ _ hx,
213        show h.nextBlk ≠ x from Ne.symm hx]
214  · simp [failedHeap, Heap.live]
215
216theorem wordResult_live (h : Heap) (n x : Nat) :
217    (wordResult h n).live x ↔ h.live x ∨ wordPtr h = .ref (.blk x) 0 := by
218  unfold wordResult wordPtr
219  split
220  · by_cases hx : x = h.nextBlk
221    · subst x
222      simp [Heap.live, wordHeap]
223    · simp [Heap.live, wordHeap, upd_ne _ _ _ _ hx, show h.nextBlk ≠ x from Ne.symm hx]
224  · simp [failedHeap, Heap.live]
225
226theorem stateHeap_live (h : Heap) (d : DeflateState) (x : Nat) :
227    (stateHeap h d).live x ↔ h.live x ∨ x = h.nextBlk := by
228  by_cases hx : x = h.nextBlk
229  · subst x
230    simp [stateHeap, Heap.live]
231  · simp [stateHeap, Heap.live, upd_ne _ _ _ _ hx, hx]
232
233/-- Equality of every represented object and its byte-write permission at
234one allocation identity. Allocation metadata is treated separately. -/
235def SlotSame (h g : Heap) (x : Nat) : Prop :=
236  g.bytes x = h.bytes x ∧ g.words x = h.words x ∧ g.streams x = h.streams x ∧
237    g.gzheaders x = h.gzheaders x ∧ g.dstates x = h.dstates x ∧
238    g.istates x = h.istates x ∧ g.gzstates x = h.gzstates x ∧ g.ro x = h.ro x
239
240theorem SlotSame.trans {h g j : Heap} {x : Nat} (a : SlotSame h g x) (b : SlotSame g j x) :
241    SlotSame h j x := by
242  rcases a with ⟨a1, a2, a3, a4, a5, a6, a7, a8⟩
243  rcases b with ⟨b1, b2, b3, b4, b5, b6, b7, b8⟩
244  exact ⟨b1.trans a1, b2.trans a2, b3.trans a3, b4.trans a4, b5.trans a5,
245    b6.trans a6, b7.trans a7, b8.trans a8⟩
246
247theorem byteResult_old (h : Heap) (n x : Nat) (hx : x < h.nextBlk) : SlotSame h (byteResult h n) x := by
248  unfold byteResult
249  split
250  · have hn : x ≠ h.nextBlk := by omega
251    simp [SlotSame, byteHeap, Zlib.Zutil.Proofs.allocHeap, upd_ne _ _ _ _ hn]
252  · exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
253
254theorem wordResult_old (h : Heap) (n x : Nat) (hx : x < h.nextBlk) : SlotSame h (wordResult h n) x := by
255  unfold wordResult
256  split
257  · have hn : x ≠ h.nextBlk := by omega
258    simp [SlotSame, wordHeap, upd_ne _ _ _ _ hn]
259  · exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
260
261end Zlib.Deflate.Proofs.DefaultInit