deflate.c.init.storage.lean

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

1import ZlibF.Proof.«deflate.c.init.default»
2import ZlibF.Proof.«deflate.c.init.cleanup»
3
4/-! # deflate.c: exact default allocation storage and failure alternatives -/
5
6namespace Zlib.Deflate.Proofs.DefaultInit
7open C Zlib.Deflate Zlib.Deflate.Spec
8set_option autoImplicit false
9
10structure StableFields (h g : Heap) : Prop where
11  streams : g.streams = h.streams
12  gzheaders : g.gzheaders = h.gzheaders
13  dstates : g.dstates = h.dstates
14  istates : g.istates = h.istates
15  gzstates : g.gzstates = h.gzstates
16  static : g.static = h.static
17  allocOk : g.allocOk = h.allocOk
18  garbage : g.garbage = h.garbage
19
20theorem StableFields.trans {h g j : Heap} (a : StableFields h g) (b : StableFields g j) :
21    StableFields h j :=
22  ⟨b.streams.trans a.streams, b.gzheaders.trans a.gzheaders, b.dstates.trans a.dstates,
23    b.istates.trans a.istates, b.gzstates.trans a.gzstates, b.static.trans a.static,
24    b.allocOk.trans a.allocOk, b.garbage.trans a.garbage⟩
25
26theorem byteResult_stable (h : Heap) (n : Nat) : StableFields h (byteResult h n) := by
27  unfold byteResult
28  split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
29
30theorem wordResult_stable (h : Heap) (n : Nat) : StableFields h (wordResult h n) := by
31  unfold wordResult
32  split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
33
34theorem buffers_stable (h : Heap) : StableFields h (buffersHeap h) :=
35  (((byteResult_stable h 65536).trans (wordResult_stable (windowHeap h) 32768)).trans
36    (wordResult_stable (prevHeap h) 32768)).trans (byteResult_stable (headHeap h) 65536)
37
38theorem freeBytes_stable (h : Heap) (p : BPtr) : StableFields h (freeBytes h p) := by
39  unfold freeBytes
40  split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
41
42theorem freeWords_stable (h : Heap) (p : WPtr) : StableFields h (freeWords h p) := by
43  unfold freeWords
44  split <;> exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
45
46@[simp] theorem freeBytes_nalloc (h : Heap) (p : BPtr) : (freeBytes h p).nalloc = h.nalloc := by
47  unfold freeBytes
48  split <;> rfl
49
50@[simp] theorem freeWords_nalloc (h : Heap) (p : WPtr) : (freeWords h p).nalloc = h.nalloc := by
51  unfold freeWords
52  split <;> rfl
53
54theorem buffers_fresh {h : Heap} (hf : Fresh h) : Fresh (buffersHeap h) :=
55  fresh_byteResult (fresh_wordResult (fresh_wordResult (fresh_byteResult hf 65536) 32768) 32768) 65536
56
57theorem buffers_uniq {h : Heap} (hu : Uniq h) (hf : Fresh h) : Uniq (buffersHeap h) :=
58  uniq_byteResult
59    (uniq_wordResult
60      (uniq_wordResult (uniq_byteResult hu hf 65536) (fresh_byteResult hf 65536) 32768)
61      (fresh_wordResult (fresh_byteResult hf 65536) 32768) 32768)
62    (fresh_wordResult (fresh_wordResult (fresh_byteResult hf 65536) 32768) 32768) 65536
63
64theorem buffers_next (h : Heap) : h.nextBlk ≤ (buffersHeap h).nextBlk := by
65  have a := byteResult_next h 65536
66  have b := wordResult_next (windowHeap h) 32768
67  have c := wordResult_next (prevHeap h) 32768
68  have d := byteResult_next (headHeap h) 65536
69  dsimp only [buffersHeap, headHeap, prevHeap, windowHeap] at *
70  omega
71
72theorem buffers_old (h : Heap) (x : Nat) (hx : x < h.nextBlk) : SlotSame h (buffersHeap h) x := by
73  have a := byteResult_next h 65536
74  have b := wordResult_next (windowHeap h) 32768
75  have c := wordResult_next (prevHeap h) 32768
76  exact ((byteResult_old h 65536 x hx).trans
77    (wordResult_old (windowHeap h) 32768 x (by dsimp only [windowHeap] at *; omega))).trans
78    ((wordResult_old (prevHeap h) 32768 x (by dsimp only [prevHeap, windowHeap] at *; omega)).trans
79      (byteResult_old (headHeap h) 65536 x (by dsimp only [headHeap, prevHeap, windowHeap] at *; omega)))
80
81@[simp] theorem buffers_nalloc (h : Heap) : (buffersHeap h).nalloc = h.nalloc + 4 := by
82  simp [buffersHeap, headHeap, prevHeap, windowHeap, Nat.add_assoc]
83
84@[simp] theorem buffers_dstates (h : Heap) : (buffersHeap h).dstates = h.dstates := by
85  simp [buffersHeap, headHeap, prevHeap, windowHeap]
86
87@[simp] theorem get_buffersHeap (h : Heap) (r : ZStreamRef) : r.get (buffersHeap h) = r.get h := by
88  simp [buffersHeap, headHeap, prevHeap, windowHeap]
89
90theorem buffers_live (h : Heap) (x : Nat) :
91    (buffersHeap h).live x ↔ h.live x ∨ (bufferPointers h).1 = .ref (.blk x) 0 ∨
92      (bufferPointers h).2.1 = .ref (.blk x) 0 ∨
93      (bufferPointers h).2.2.1 = .ref (.blk x) 0 ∨
94      (bufferPointers h).2.2.2 = .ref (.blk x) 0 := by
95  simp only [buffersHeap, byteResult_live, headHeap, wordResult_live, prevHeap,
96    windowHeap, bufferPointers, or_assoc]
97
98def byteGarbage (h : Heap) (j : Nat) : Array UInt8 :=
99  Array.ofFn (n := 65536) fun i => Junk.of (h.garbage (h.nalloc + j) i.val)
100def wordGarbage (h : Heap) (j : Nat) : Array UInt16 :=
101  Array.ofFn (n := 32768) fun i => Junk.of (h.garbage (h.nalloc + j) i.val)
102
103def successfulBuffers (h : Heap) : Heap :=
104  { h with
105    bytes := upd (upd h.bytes h.nextBlk (some (byteGarbage h 0))) (h.nextBlk + 3) (some (byteGarbage h 3)),
106    words := upd (upd h.words (h.nextBlk + 1) (some (wordGarbage h 1)))
107      (h.nextBlk + 2) (some (wordGarbage h 2)),
108    ro := upd (upd h.ro h.nextBlk false) (h.nextBlk + 3) false,
109    nextBlk := h.nextBlk + 4, nalloc := h.nalloc + 4 }
110
111/-- Exact storage when all four requests succeed; all arrays keep the
112allocator's arbitrary integer contents. -/
113theorem buffers_success (h : Heap) (ha : ∀ j, j < 4 → h.allocOk (h.nalloc + j) = true) :
114    buffersHeap h = successfulBuffers h ∧
115    bufferPointers h = (.ref (.blk h.nextBlk) 0, .ref (.blk (h.nextBlk + 1)) 0,
116      .ref (.blk (h.nextBlk + 2)) 0, .ref (.blk (h.nextBlk + 3)) 0) := by
117  have hw := ha 0 (by decide)
118  have hp := ha 1 (by decide)
119  have hq := ha 2 (by decide)
120  have hb := ha 3 (by decide)
121  simp only [Nat.add_zero] at hw
122  constructor
123  · simp [buffersHeap, headHeap, prevHeap, windowHeap, successfulBuffers,
124      byteResult, wordResult, byteHeap, wordHeap, Zlib.Zutil.Proofs.allocHeap,
125      byteGarbage, wordGarbage, hw, hp, hq, hb, Nat.add_assoc]
126  · simp [bufferPointers, headHeap, prevHeap, windowHeap,
127      byteResult, wordResult, bytePtr, wordPtr, byteHeap, wordHeap,
128      Zlib.Zutil.Proofs.allocHeap, hw, hp, hq, hb, Nat.add_assoc]
129
130/-- Every returned buffer is NULL or the live allocation of its request.
131The two byte buffers and two word buffers cannot alias when non-NULL. -/
132theorem buffers_freeable (h : Heap) :
133    FreeableB (buffersHeap h) (bufferPointers h).1 ∧
134    FreeableW (buffersHeap h) (bufferPointers h).2.1 ∧
135    FreeableW (buffersHeap h) (bufferPointers h).2.2.1 ∧
136    FreeableB (buffersHeap h) (bufferPointers h).2.2.2 ∧
137    ((bufferPointers h).2.2.2 = .null ∨ (bufferPointers h).1 = .null ∨
138      (bufferPointers h).2.2.2 ≠ (bufferPointers h).1) ∧
139    ((bufferPointers h).2.2.1 = .null ∨ (bufferPointers h).2.1 = .null ∨
140      (bufferPointers h).2.2.1 ≠ (bufferPointers h).2.1) := by
141  by_cases hw : h.allocOk h.nalloc = true <;>
142    by_cases hp : h.allocOk (h.nalloc + 1) = true <;>
143    by_cases hq : h.allocOk (h.nalloc + 2) = true <;>
144    by_cases hb : h.allocOk (h.nalloc + 3) = true
145  all_goals simp [FreeableB, FreeableW, bufferPointers, buffersHeap, headHeap, prevHeap, windowHeap,
146    byteResult, wordResult, bytePtr, wordPtr, byteHeap, wordHeap, failedHeap,
147    Zlib.Zutil.Proofs.allocHeap, hw, hp, hq, hb, Nat.add_assoc]
148
149/-- The failure test sees the exact four allocator outcomes. -/
150theorem buffers_failed_iff (h : Heap) :
151    ((bufferPointers h).1 == .null || (bufferPointers h).2.1 == .null ||
152      (bufferPointers h).2.2.1 == .null || (bufferPointers h).2.2.2 == .null) = false ↔
153      h.allocOk h.nalloc = true ∧ h.allocOk (h.nalloc + 1) = true ∧
154        h.allocOk (h.nalloc + 2) = true ∧ h.allocOk (h.nalloc + 3) = true := by
155  by_cases hw : h.allocOk h.nalloc = true <;>
156    by_cases hp : h.allocOk (h.nalloc + 1) = true <;>
157    by_cases hq : h.allocOk (h.nalloc + 2) = true <;>
158    by_cases hb : h.allocOk (h.nalloc + 3) = true
159  all_goals simp [bufferPointers, buffersHeap, headHeap, prevHeap, windowHeap,
160    byteResult, wordResult, bytePtr, wordPtr, byteHeap, wordHeap, failedHeap,
161    Zlib.Zutil.Proofs.allocHeap, hw, hp, hq, hb, Nat.add_assoc]
162
163theorem freeBytes_congr (h g : Heap) (p : BPtr) (he : h.bytes = g.bytes) :
164    (freeBytes h p).bytes = (freeBytes g p).bytes := by
165  unfold freeBytes
166  split <;> simp_all
167
168theorem freeWords_congr (h g : Heap) (p : WPtr) (he : h.words = g.words) :
169    (freeWords h p).words = (freeWords g p).words := by
170  unfold freeWords
171  split <;> simp_all
172
173theorem freeBytes_congr_at (h g : Heap) (p : BPtr) (x : Nat) (he : h.bytes x = g.bytes x) :
174    (freeBytes h p).bytes x = (freeBytes g p).bytes x := by
175  unfold freeBytes
176  split <;> simp_all [upd_apply]
177
178theorem freeWords_congr_at (h g : Heap) (p : WPtr) (x : Nat) (he : h.words x = g.words x) :
179    (freeWords h p).words x = (freeWords g p).words x := by
180  unfold freeWords
181  split <;> simp_all [upd_apply]
182
183/-- Cleanup restores each byte-object lookup. It does not shrink a grown
184table or rewind the allocation counters and permission metadata. -/
185theorem byte_pop_at {h : Heap} (hf : Fresh h) (n x : Nat) :
186    (freeBytes (byteResult h n) (bytePtr h)).bytes x = h.bytes x := by
187  obtain ⟨hb, _, _, _, _, _, _⟩ := Heap.not_live.mp (hf _ (Nat.le_refl _))
188  by_cases ho : h.allocOk h.nalloc = true <;> by_cases hx : x = h.nextBlk
189  all_goals simp [byteResult, bytePtr, byteHeap, Zlib.Zutil.Proofs.allocHeap,
190    failedHeap, ho, freeBytes, upd_apply, hx, hb]
191
192theorem word_pop_at {h : Heap} (hf : Fresh h) (n x : Nat) :
193    (freeWords (wordResult h n) (wordPtr h)).words x = h.words x := by
194  obtain ⟨_, hw, _, _, _, _, _⟩ := Heap.not_live.mp (hf _ (Nat.le_refl _))
195  by_cases ho : h.allocOk h.nalloc = true <;> by_cases hx : x = h.nextBlk
196  all_goals simp [wordResult, wordPtr, wordHeap, failedHeap, ho, freeWords, upd_apply, hx, hw]
197
198def rollbackBuffers (h g : Heap) : Heap :=
199  freeBytes (freeWords (freeWords (freeBytes g (bufferPointers h).2.2.2)
200    (bufferPointers h).2.2.1) (bufferPointers h).2.1) (bufferPointers h).1
201
202theorem rollback_stable (h g : Heap) : StableFields g (rollbackBuffers h g) := by
203  unfold rollbackBuffers
204  exact (((freeBytes_stable g _).trans (freeWords_stable _ _)).trans
205    (freeWords_stable _ _)).trans (freeBytes_stable _ _)
206
207@[simp] theorem rollback_nalloc (h g : Heap) : (rollbackBuffers h g).nalloc = g.nalloc := by
208  simp [rollbackBuffers]
209
210@[simp] theorem rollback_next (h g : Heap) : (rollbackBuffers h g).nextBlk = g.nextBlk := by
211  simp [rollbackBuffers]
212
213@[simp] theorem get_rollback (h g : Heap) (r : ZStreamRef) : r.get (rollbackBuffers h g) = r.get g := by
214  simp [rollbackBuffers]
215
216theorem slot_freeBytePtr_old (h g : Heap) (x : Nat) (hx : x < h.nextBlk) :
217    SlotSame g (freeBytes g (bytePtr h)) x := by
218  unfold bytePtr
219  split
220  · simp [SlotSame, freeBytes, upd_ne _ _ _ _ (show x ≠ h.nextBlk by omega)]
221  · exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
222
223theorem slot_freeWordPtr_old (h g : Heap) (x : Nat) (hx : x < h.nextBlk) :
224    SlotSame g (freeWords g (wordPtr h)) x := by
225  unfold wordPtr
226  split
227  · simp [SlotSame, freeWords, upd_ne _ _ _ _ (show x ≠ h.nextBlk by omega)]
228  · exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
229
230theorem rollback_old (h g : Heap) (x : Nat) (hx : x < h.nextBlk) : SlotSame g (rollbackBuffers h g) x := by
231  have a := byteResult_next h 65536
232  have b := wordResult_next (windowHeap h) 32768
233  have c := wordResult_next (prevHeap h) 32768
234  have i1 := slot_freeBytePtr_old (headHeap h) g x (by
235    dsimp only [headHeap, prevHeap, windowHeap] at *; omega)
236  have i2 := slot_freeWordPtr_old (prevHeap h) (freeBytes g (bytePtr (headHeap h))) x (by
237    dsimp only [headHeap, prevHeap, windowHeap] at *; omega)
238  have i3 := slot_freeWordPtr_old (windowHeap h)
239    (freeWords (freeBytes g (bytePtr (headHeap h))) (wordPtr (prevHeap h))) x (by
240      dsimp only [windowHeap] at *; omega)
241  exact ((i1.trans i2).trans i3).trans (slot_freeBytePtr_old h _ x hx)
242
243/-- Reverse-order cleanup restores every byte/word object lookup for all
244sixteen buffer-success patterns. Table capacities may remain enlarged. -/
245theorem rollback_arrays_at {h g : Heap} (hf : Fresh h) (x : Nat)
246    (hb : g.bytes x = (buffersHeap h).bytes x) (hw : g.words x = (buffersHeap h).words x) :
247    (rollbackBuffers h g).bytes x = h.bytes x ∧ (rollbackBuffers h g).words x = h.words x := by
248  have fW := fresh_byteResult hf 65536
249  have fP := fresh_wordResult fW 32768
250  have fH := fresh_wordResult fP 32768
251  have popB := byte_pop_at fH 65536 x
252  have popH := word_pop_at fP 32768 x
253  have popP := word_pop_at fW 32768 x
254  have popW := byte_pop_at hf 65536 x
255  have b1 : (freeBytes g (bytePtr (headHeap h))).bytes x = (headHeap h).bytes x := by
256    rw [freeBytes_congr_at g (buffersHeap h) _ x hb]
257    exact popB
258  have w1 : (freeBytes g (bytePtr (headHeap h))).words x = (headHeap h).words x := by
259    simpa [buffersHeap] using hw
260  have w2 : (freeWords (freeBytes g (bytePtr (headHeap h))) (wordPtr (prevHeap h))).words x =
261      (prevHeap h).words x := by
262    rw [freeWords_congr_at _ (headHeap h) _ x w1]
263    exact popH
264  have w3 : (freeWords (freeWords (freeBytes g (bytePtr (headHeap h))) (wordPtr (prevHeap h)))
265      (wordPtr (windowHeap h))).words x = (windowHeap h).words x := by
266    rw [freeWords_congr_at _ (prevHeap h) _ x w2]
267    exact popP
268  constructor
269  · unfold rollbackBuffers bufferPointers
270    simp only [freeWords_bytes] at b1 ⊢
271    have eq : (freeWords (freeWords (freeBytes g (bytePtr (headHeap h))) (wordPtr (prevHeap h)))
272        (wordPtr (windowHeap h))).bytes x = (windowHeap h).bytes x := by
273      simpa [headHeap, prevHeap] using b1
274    rw [freeBytes_congr_at _ (windowHeap h) _ x eq]
275    exact popW
276  · unfold rollbackBuffers bufferPointers
277    simpa [windowHeap] using w3
278
279end Zlib.Deflate.Proofs.DefaultInit