1 | (* *********************************************************************) |
---|
2 | (* *) |
---|
3 | (* The Compcert verified compiler *) |
---|
4 | (* *) |
---|
5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
6 | (* Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt *) |
---|
7 | (* *) |
---|
8 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
9 | (* Automatique. All rights reserved. This file is distributed *) |
---|
10 | (* under the terms of the GNU General Public License as published by *) |
---|
11 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
12 | (* (at your option) any later version. This file is also distributed *) |
---|
13 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
14 | (* *) |
---|
15 | (* *********************************************************************) |
---|
16 | |
---|
17 | (* * This file develops the memory model that is used in the dynamic |
---|
18 | semantics of all the languages used in the compiler. |
---|
19 | It defines a type [mem] of memory states, the following 4 basic |
---|
20 | operations over memory states, and their properties: |
---|
21 | - [load]: read a memory chunk at a given address; |
---|
22 | - [store]: store a memory chunk at a given address; |
---|
23 | - [alloc]: allocate a fresh memory block; |
---|
24 | - [free]: invalidate a memory block. |
---|
25 | *) |
---|
26 | |
---|
27 | include "arithmetics/nat.ma". |
---|
28 | (*include "binary/Z.ma".*) |
---|
29 | (*include "datatypes/sums.ma".*) |
---|
30 | (*include "datatypes/list.ma".*) |
---|
31 | (*include "Plogic/equality.ma".*) |
---|
32 | |
---|
33 | (*include "Coqlib.ma".*) |
---|
34 | include "Values.ma". |
---|
35 | (*include "AST.ma".*) |
---|
36 | include "extralib.ma". |
---|
37 | |
---|
38 | definition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝ |
---|
39 | λA,x,v,f. |
---|
40 | λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ]. |
---|
41 | |
---|
42 | lemma update_s: |
---|
43 | ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. |
---|
44 | update … x v f x = v. |
---|
45 | #A #x #v #f whd in ⊢ (??%?); |
---|
46 | >(eqZb_z_z …) //; |
---|
47 | qed. |
---|
48 | |
---|
49 | lemma update_o: |
---|
50 | ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. ∀y: Z. |
---|
51 | x ≠ y → update … x v f y = f y. |
---|
52 | #A #x #v #f #y #H whd in ⊢ (??%?); |
---|
53 | @eqZb_elim //; |
---|
54 | #H2 cases H;#H3 elim (H3 ?);//; |
---|
55 | qed. |
---|
56 | |
---|
57 | (* FIXME: workaround for lack of nunfold *) |
---|
58 | lemma unfold_update : ∀A,x,v,f,y. update A x v f y = match eqZb y x with [ true ⇒ v | false ⇒ f y ]. |
---|
59 | //; qed. |
---|
60 | |
---|
61 | definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝ |
---|
62 | λA,x,v,f. |
---|
63 | λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ]. |
---|
64 | |
---|
65 | lemma update_block_s: |
---|
66 | ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. |
---|
67 | update_block … x v f x = v. |
---|
68 | #A * * #ix #v #f whd in ⊢ (??%?); |
---|
69 | >(eqZb_z_z …) //; |
---|
70 | qed. |
---|
71 | |
---|
72 | lemma update_block_o: |
---|
73 | ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block. |
---|
74 | x ≠ y → update_block … x v f y = f y. |
---|
75 | #A #x #v #f #y #H whd in ⊢ (??%?); |
---|
76 | @eq_block_elim //; |
---|
77 | #H2 cases H;#H3 elim (H3 ?);//; |
---|
78 | qed. |
---|
79 | |
---|
80 | (* FIXME: workaround for lack of nunfold *) |
---|
81 | lemma unfold_update_block : ∀A,x,v,f,y. |
---|
82 | update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ]. |
---|
83 | //; qed. |
---|
84 | |
---|
85 | |
---|
86 | (* * Structure of memory states *) |
---|
87 | |
---|
88 | (* A memory state is organized in several disjoint blocks. Each block |
---|
89 | has a low and a high bound that defines its size. Each block map |
---|
90 | byte offsets to the contents of this byte. *) |
---|
91 | |
---|
92 | (* The possible contents of a byte-sized memory cell. To give intuitions, |
---|
93 | a 4-byte value [v] stored at offset [d] will be represented by |
---|
94 | the content [Datum(4, v)] at offset [d] and [Cont] at offsets [d+1], |
---|
95 | [d+2] and [d+3]. The [Cont] contents enable detecting future writes |
---|
96 | that would partially overlap the 4-byte value. *) |
---|
97 | |
---|
98 | inductive content : Type[0] ≝ |
---|
99 | | Undef: content (*r undefined contents *) |
---|
100 | | Datum: nat → val → content (*r first byte of a value *) |
---|
101 | | Cont: content. (*r continuation bytes for a multi-byte value *) |
---|
102 | |
---|
103 | definition contentmap : Type[0] ≝ Z → content. |
---|
104 | |
---|
105 | (* A memory block comprises the dimensions of the block (low and high bounds) |
---|
106 | plus a mapping from byte offsets to contents. *) |
---|
107 | |
---|
108 | record block_contents : Type[0] ≝ { |
---|
109 | low: Z; |
---|
110 | high: Z; |
---|
111 | contents: contentmap |
---|
112 | }. |
---|
113 | |
---|
114 | (* A memory state is a mapping from block addresses (represented by memory |
---|
115 | regions and integers) to blocks. We also maintain the address of the next |
---|
116 | unallocated block, and a proof that this address is positive. *) |
---|
117 | |
---|
118 | record mem : Type[0] ≝ { |
---|
119 | blocks: block -> block_contents; |
---|
120 | nextblock: Z; |
---|
121 | nextblock_pos: OZ < nextblock |
---|
122 | }. |
---|
123 | |
---|
124 | (* * Operations on memory stores *) |
---|
125 | |
---|
126 | (* Memory reads and writes are performed by quantities called memory chunks, |
---|
127 | encoding the type, size and signedness of the chunk being addressed. |
---|
128 | The following functions extract the size information from a chunk. *) |
---|
129 | |
---|
130 | definition size_pointer : region → Z ≝ |
---|
131 | λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ]. |
---|
132 | |
---|
133 | definition size_chunk : memory_chunk → Z ≝ |
---|
134 | λchunk.match chunk with |
---|
135 | [ Mint8signed => 1 |
---|
136 | | Mint8unsigned => 1 |
---|
137 | | Mint16signed => 2 |
---|
138 | | Mint16unsigned => 2 |
---|
139 | | Mint32 => 4 |
---|
140 | | Mfloat32 => 4 |
---|
141 | | Mfloat64 => 8 |
---|
142 | | Mpointer r ⇒ size_pointer r |
---|
143 | ]. |
---|
144 | |
---|
145 | definition pred_size_pointer : region → nat ≝ |
---|
146 | λsp. match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ]. |
---|
147 | |
---|
148 | definition pred_size_chunk : memory_chunk → nat ≝ |
---|
149 | λchunk.match chunk with |
---|
150 | [ Mint8signed => 0 |
---|
151 | | Mint8unsigned => 0 |
---|
152 | | Mint16signed => 1 |
---|
153 | | Mint16unsigned => 1 |
---|
154 | | Mint32 => 3 |
---|
155 | | Mfloat32 => 3 |
---|
156 | | Mfloat64 => 7 |
---|
157 | | Mpointer r ⇒ pred_size_pointer r |
---|
158 | ]. |
---|
159 | |
---|
160 | alias symbol "plus" (instance 2) = "integer plus". |
---|
161 | lemma size_chunk_pred: |
---|
162 | ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk. |
---|
163 | #chunk cases chunk;//; #r cases r; @refl |
---|
164 | qed. |
---|
165 | |
---|
166 | lemma size_chunk_pos: |
---|
167 | ∀chunk. 0 < size_chunk chunk. |
---|
168 | #chunk >(size_chunk_pred ?) cases (pred_size_chunk chunk); |
---|
169 | normalize;//; |
---|
170 | qed. |
---|
171 | |
---|
172 | (* Memory reads and writes must respect alignment constraints: |
---|
173 | the byte offset of the location being addressed should be an exact |
---|
174 | multiple of the natural alignment for the chunk being addressed. |
---|
175 | This natural alignment is defined by the following |
---|
176 | [align_chunk] function. Some target architectures |
---|
177 | (e.g. the PowerPC) have no alignment constraints, which we could |
---|
178 | reflect by taking [align_chunk chunk = 1]. However, other architectures |
---|
179 | have stronger alignment requirements. The following definition is |
---|
180 | appropriate for PowerPC and ARM. *) |
---|
181 | |
---|
182 | definition align_chunk : memory_chunk → Z ≝ |
---|
183 | λchunk.match chunk return λ_.Z with |
---|
184 | [ Mint8signed ⇒ 1 |
---|
185 | | Mint8unsigned ⇒ 1 |
---|
186 | | Mint16signed ⇒ 1 |
---|
187 | | Mint16unsigned ⇒ 1 |
---|
188 | | _ ⇒ 1 ]. |
---|
189 | |
---|
190 | lemma align_chunk_pos: |
---|
191 | ∀chunk. OZ < align_chunk chunk. |
---|
192 | #chunk cases chunk;normalize;//; |
---|
193 | qed. |
---|
194 | |
---|
195 | lemma align_size_chunk_divides: |
---|
196 | ∀chunk. (align_chunk chunk ∣ size_chunk chunk). |
---|
197 | #chunk cases chunk;[8:#r cases r ]normalize;/3/; |
---|
198 | qed. |
---|
199 | |
---|
200 | lemma align_chunk_compat: |
---|
201 | ∀chunk1,chunk2. |
---|
202 | size_chunk chunk1 = size_chunk chunk2 → |
---|
203 | align_chunk chunk1 = align_chunk chunk2. |
---|
204 | #chunk1 #chunk2 |
---|
205 | cases chunk1; try ( #r1 #cases #r1 ) |
---|
206 | cases chunk2; try ( #r2 #cases #r2 ) |
---|
207 | normalize;//; |
---|
208 | qed. |
---|
209 | |
---|
210 | (* The initial store. *) |
---|
211 | |
---|
212 | definition oneZ ≝ pos one. |
---|
213 | |
---|
214 | lemma one_pos: OZ < oneZ. |
---|
215 | //; |
---|
216 | qed. |
---|
217 | |
---|
218 | definition empty_block : Z → Z → block_contents ≝ |
---|
219 | λlo,hi.mk_block_contents lo hi (λy. Undef). |
---|
220 | |
---|
221 | definition empty: mem ≝ |
---|
222 | mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. |
---|
223 | |
---|
224 | definition nullptr: block ≝ 〈Any,OZ〉. |
---|
225 | |
---|
226 | (* Allocation of a fresh block with the given bounds. Return an updated |
---|
227 | memory state and the address of the fresh block, which initially contains |
---|
228 | undefined cells. Note that allocation never fails: we model an |
---|
229 | infinite memory. *) |
---|
230 | |
---|
231 | lemma succ_nextblock_pos: |
---|
232 | ∀m. OZ < Zsucc (nextblock m). (* XXX *) |
---|
233 | #m lapply (nextblock_pos m);normalize; |
---|
234 | cases (nextblock m);//; |
---|
235 | #n cases n;//; |
---|
236 | qed. |
---|
237 | |
---|
238 | definition alloc : mem → Z → Z → region → mem × block ≝ |
---|
239 | λm,lo,hi,r.〈mk_mem |
---|
240 | (update_block … 〈r,nextblock m〉 |
---|
241 | (empty_block lo hi) |
---|
242 | (blocks m)) |
---|
243 | (Zsucc (nextblock m)) |
---|
244 | (succ_nextblock_pos m), |
---|
245 | 〈r,nextblock m〉〉. |
---|
246 | |
---|
247 | (* Freeing a block. Return the updated memory state where the given |
---|
248 | block address has been invalidated: future reads and writes to this |
---|
249 | address will fail. Note that we make no attempt to return the block |
---|
250 | to an allocation pool: the given block address will never be allocated |
---|
251 | later. *) |
---|
252 | |
---|
253 | definition free ≝ |
---|
254 | λm,b.mk_mem (update_block … b |
---|
255 | (empty_block OZ OZ) |
---|
256 | (blocks m)) |
---|
257 | (nextblock m) |
---|
258 | (nextblock_pos m). |
---|
259 | |
---|
260 | (* Freeing of a list of blocks. *) |
---|
261 | |
---|
262 | definition free_list ≝ |
---|
263 | λm,l.foldr ?? (λb,m.free m b) m l. |
---|
264 | (* XXX hack for lack of reduction with restricted unfolding *) |
---|
265 | lemma unfold_free_list : ∀m,h,t. free_list m (h::t) = free (free_list m t) h. |
---|
266 | normalize; //; qed. |
---|
267 | |
---|
268 | (* Return the low and high bounds for the given block address. |
---|
269 | Those bounds are 0 for freed or not yet allocated address. *) |
---|
270 | |
---|
271 | definition low_bound : mem → block → Z ≝ |
---|
272 | λm,b.low (blocks m b). |
---|
273 | definition high_bound : mem → block → Z ≝ |
---|
274 | λm,b.high (blocks m b). |
---|
275 | definition block_region: mem → block → region ≝ |
---|
276 | λm,b.\fst b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) |
---|
277 | |
---|
278 | (* A block address is valid if it was previously allocated. It remains valid |
---|
279 | even after being freed. *) |
---|
280 | |
---|
281 | (* TODO: should this check for region? *) |
---|
282 | definition valid_block : mem → block → Prop ≝ |
---|
283 | λm,b.\snd b < nextblock m. |
---|
284 | |
---|
285 | (* FIXME: hacks to get around lack of nunfold *) |
---|
286 | lemma unfold_low_bound : ∀m,b. low_bound m b = low (blocks m b). |
---|
287 | //; qed. |
---|
288 | lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b). |
---|
289 | //; qed. |
---|
290 | lemma unfold_valid_block : ∀m,b. (valid_block m b) = (\snd b < nextblock m). |
---|
291 | //; qed. |
---|
292 | |
---|
293 | (* Reading and writing [N] adjacent locations in a [contentmap]. |
---|
294 | |
---|
295 | We define two functions and prove some of their properties: |
---|
296 | - [getN n ofs m] returns the datum at offset [ofs] in block contents [m] |
---|
297 | after checking that the contents of offsets [ofs+1] to [ofs+n+1] |
---|
298 | are [Cont]. |
---|
299 | - [setN n ofs v m] updates the block contents [m], storing the content [v] |
---|
300 | at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1]. |
---|
301 | *) |
---|
302 | |
---|
303 | let rec check_cont (n: nat) (p: Z) (m: contentmap) on n : bool ≝ |
---|
304 | match n return λ_.bool with |
---|
305 | [ O ⇒ true |
---|
306 | | S n1 ⇒ |
---|
307 | match m p with |
---|
308 | [ Cont ⇒ check_cont n1 (Zplus p 1) m (* FIXME: cannot disambiguate + properly *) |
---|
309 | | _ ⇒ false ] ]. |
---|
310 | |
---|
311 | (* XXX : was +, not ∨ logical or |
---|
312 | is used when eqb is expected, coq idiom, is it necessary?? *) |
---|
313 | definition eq_nat: ∀p,q: nat. p=q ∨ p≠q. |
---|
314 | @decidable_eq_nat (* // not working, why *) |
---|
315 | qed. |
---|
316 | |
---|
317 | definition getN : nat → Z → contentmap → val ≝ |
---|
318 | λn,p,m.match m p with |
---|
319 | [ Datum n' v ⇒ |
---|
320 | match andb (eqb n n') (check_cont n (p + oneZ) m) with |
---|
321 | [ true ⇒ v |
---|
322 | | false ⇒ Vundef ] |
---|
323 | | _ ⇒ |
---|
324 | Vundef ]. |
---|
325 | |
---|
326 | let rec set_cont (n: nat) (p: Z) (m: contentmap) on n : contentmap ≝ |
---|
327 | match n with |
---|
328 | [ O ⇒ m |
---|
329 | | S n1 ⇒ update ? p Cont (set_cont n1 (p + oneZ) m) ]. |
---|
330 | |
---|
331 | definition setN : nat → Z → val → contentmap → contentmap ≝ |
---|
332 | λn,p,v,m.update ? p (Datum n v) (set_cont n (p + oneZ) m). |
---|
333 | |
---|
334 | (* Nonessential properties that may require arithmetic |
---|
335 | (* XXX: the daemons *) |
---|
336 | axiom daemon : ∀A:Prop.A. |
---|
337 | |
---|
338 | lemma check_cont_spec: |
---|
339 | ∀n,m,p. |
---|
340 | match (check_cont n p m) with |
---|
341 | [ true ⇒ ∀q.p ≤ q → q < p + n → m q = Cont |
---|
342 | | false ⇒ ∃q. p ≤ q ∧ q < (p + n) ∧ m q ≠ Cont ]. |
---|
343 | #n elim n; |
---|
344 | [#m #p #q #Hl #Hr |
---|
345 | (* derive contradiction from Hl, Hr; needs: |
---|
346 | - p + O = p |
---|
347 | - p ≤ q → q < p → False *) |
---|
348 | napply daemon |
---|
349 | |#n1 #IH #m #p |
---|
350 | (* whd : doesn't work either *) |
---|
351 | cut (check_cont (S n1) p m = match m p with [ Undef ⇒ false | Datum _ _ ⇒ false | Cont ⇒ check_cont n1 (Zplus p oneZ) m ]) |
---|
352 | [@ |
---|
353 | |#Heq >Heq lapply (refl ? (m p)); |
---|
354 | cases (m p) in ⊢ (???% → %); |
---|
355 | [#Heq1 % |
---|
356 | [napply p |
---|
357 | |% [napply daemon |
---|
358 | |@nmk #Hfalse >Hfalse in Heq1 #Heq1 |
---|
359 | destruct ] |
---|
360 | ] |
---|
361 | |#n2 #v #Heq1 % |
---|
362 | [napply p |
---|
363 | | % [ (* refl≤ and p < p + S n1 *)napply daemon |
---|
364 | |@nmk #Hfalse >Hfalse in Heq1 #Heq1 |
---|
365 | destruct ] |
---|
366 | ] |
---|
367 | |#Heq1 lapply (IH m (p + 1)); |
---|
368 | lapply (refl ? (check_cont n1 (p + 1) m)); |
---|
369 | (* napply daemon *) |
---|
370 | cases (check_cont n1 (p + 1) m) in ⊢ (???% → %); |
---|
371 | whd in ⊢ (? → % → %); |
---|
372 | [#H #H1 #q #Hl #Hr |
---|
373 | cut (p = q ∨ p + 1 ≤ q) |
---|
374 | [(* Hl *) napply daemon |
---|
375 | |*; |
---|
376 | [// |
---|
377 | |#Hl2 @H1 //;(*Hr*)napply daemon ] ] |
---|
378 | |#H #H1 cases H1;#x *;*;#Hl #Hr #Hx |
---|
379 | %{ x} @ |
---|
380 | [@ |
---|
381 | [(*Hl*) napply daemon |
---|
382 | |(*Hr*) napply daemon ] |
---|
383 | |//]]]] |
---|
384 | qed. |
---|
385 | |
---|
386 | lemma check_cont_true: |
---|
387 | ∀n:nat.∀m,p. |
---|
388 | (∀q. p ≤ q → q < p + n → m q = Cont) → |
---|
389 | check_cont n p m = true. |
---|
390 | #n #m #p #H lapply (check_cont_spec n m p); |
---|
391 | cases (check_cont n p m);//; |
---|
392 | whd in ⊢ (%→?);*; |
---|
393 | #q *;*;#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //; |
---|
394 | qed. |
---|
395 | |
---|
396 | lemma check_cont_false: |
---|
397 | ∀n:nat.∀m,p,q. |
---|
398 | p ≤ q → q < p + n → m q ≠ Cont → |
---|
399 | check_cont n p m = false. |
---|
400 | #n #m #p #q lapply (check_cont_spec n m p); |
---|
401 | cases (check_cont n p m);//; |
---|
402 | whd in ⊢ (%→?);#H |
---|
403 | #Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //; |
---|
404 | qed. |
---|
405 | |
---|
406 | lemma set_cont_inside: |
---|
407 | ∀n:nat.∀p:Z.∀m.∀q:Z. |
---|
408 | p ≤ q → q < p + n → |
---|
409 | (set_cont n p m) q = Cont. |
---|
410 | #n elim n; |
---|
411 | [#p #m #q #Hl #Hr (* by Hl, Hr → False *)napply daemon |
---|
412 | |#n1 #IH #p #m #q #Hl #Hr |
---|
413 | cut (p = q ∨ p+1 ≤ q) |
---|
414 | [napply daemon |
---|
415 | |*; |
---|
416 | [#Heq >Heq @update_s |
---|
417 | |#Hl2 whd in ⊢ (??%?);nrewrite > (? : eqZb q p = false) |
---|
418 | [whd in ⊢ (??%?);napply IH |
---|
419 | [napply Hl2 |
---|
420 | |(* Hr *) napply daemon ] |
---|
421 | |(*Hl2*)napply daemon ] |
---|
422 | ] |
---|
423 | ] |
---|
424 | ] |
---|
425 | qed. |
---|
426 | |
---|
427 | lemma set_cont_outside: |
---|
428 | ∀n:nat.∀p:Z.∀m.∀q:Z. |
---|
429 | q < p ∨ p + n ≤ q → |
---|
430 | (set_cont n p m) q = m q. |
---|
431 | #n elim n |
---|
432 | [#p #m #q #_ @ |
---|
433 | |#n1 #IH #p #m #q |
---|
434 | #H whd in ⊢ (??%?);>(? : eqZb q p = false) |
---|
435 | [whd in ⊢ (??%?);@IH cases H; |
---|
436 | [#Hl % napply daemon |
---|
437 | |#Hr %{2} napply daemon] |
---|
438 | |(*H*)napply daemon ] |
---|
439 | ] |
---|
440 | qed. |
---|
441 | |
---|
442 | lemma getN_setN_same: |
---|
443 | ∀n,p,v,m. |
---|
444 | getN n p (setN n p v m) = v. |
---|
445 | #n #p #v #m nchange in ⊢ (??(???%)?) with (update ????); |
---|
446 | whd in ⊢ (??%?); |
---|
447 | >(update_s content p ??) whd in ⊢ (??%?); |
---|
448 | >(eqb_n_n n) |
---|
449 | nrewrite > (check_cont_true ????) |
---|
450 | [@ |
---|
451 | |#q #Hl #Hr >(update_o content …) |
---|
452 | [/2/; |
---|
453 | |(*Hl*)napply daemon ] |
---|
454 | ] |
---|
455 | qed. |
---|
456 | |
---|
457 | lemma getN_setN_other: |
---|
458 | ∀n1,n2:nat.∀p1,p2:Z.∀v,m. |
---|
459 | p1 + n1 < p2 ∨ p2 + n2 < p1 → |
---|
460 | getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m. |
---|
461 | #n1 #n2 #p1 #p2 #v #m #H |
---|
462 | ngeneralize in match (check_cont_spec n2 m (p2 + oneZ)); |
---|
463 | lapply (refl ? (check_cont n2 (p2+oneZ) m)); |
---|
464 | cases (check_cont n2 (p2+oneZ) m) in ⊢ (???% → %); |
---|
465 | #H1 whd in ⊢ (% →?); whd in ⊢ (?→(???%)); >H1 |
---|
466 | [#H2 |
---|
467 | nchange in ⊢ (??(???%)?) with (update ????); |
---|
468 | whd in ⊢(??%%);>(check_cont_true …) |
---|
469 | [ >(check_cont_true … H2) |
---|
470 | >(update_o content ?????) |
---|
471 | [ >(set_cont_outside ?????) //; (* arith *) napply daemon |
---|
472 | | (* arith *) napply daemon |
---|
473 | ] |
---|
474 | | #q #Hl #Hh >(update_o content ?????) |
---|
475 | [ >(set_cont_outside ?????) /2/; (* arith *) napply daemon |
---|
476 | | (* arith *) napply daemon |
---|
477 | ] |
---|
478 | ] |
---|
479 | | *; #q *;#A #B |
---|
480 | nchange in ⊢ (??(???%)?) with (update ????); |
---|
481 | whd in ⊢(??%%); |
---|
482 | >(check_cont_false n2 (update ? p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q …) |
---|
483 | [ >(update_o content ?????) |
---|
484 | [ >(set_cont_outside ?????) //; (* arith *) napply daemon |
---|
485 | | napply daemon |
---|
486 | ] |
---|
487 | | >(update_o content ?????) |
---|
488 | [ >(set_cont_outside ?????) //; (* arith *) napply daemon |
---|
489 | | napply daemon |
---|
490 | ] |
---|
491 | | napply daemon |
---|
492 | | napply daemon |
---|
493 | ] |
---|
494 | ] qed. |
---|
495 | |
---|
496 | lemma getN_setN_overlap: |
---|
497 | ∀n1,n2,p1,p2,v,m. |
---|
498 | p1 ≠ p2 → |
---|
499 | p2 ≤ p1 + Z_of_nat n1 → p1 ≤ p2 + Z_of_nat n2 → |
---|
500 | getN n2 p2 (setN n1 p1 v m) = Vundef. |
---|
501 | #n1 #n2 #p1 #p2 #v #m |
---|
502 | #H #H1 #H2 |
---|
503 | nchange in ⊢ (??(???%)?) with (update ????); |
---|
504 | whd in ⊢(??%?);>(update_o content ?????) |
---|
505 | [lapply (Z_compare_to_Prop p2 p1); |
---|
506 | lapply (refl ? (Z_compare p2 p1)); |
---|
507 | cases (Z_compare p2 p1) in ⊢ (???% → %);#H3 |
---|
508 | [nchange in ⊢ (% → ?) with (p2 < p1);#H4 |
---|
509 | (* [p1] belongs to [[p2, p2 + n2 - 1]], |
---|
510 | therefore [check_cont n2 (p2 + 1) ...] is false. *) |
---|
511 | >(check_cont_false …) |
---|
512 | [cases (set_cont n1 (p1+oneZ) m p2) |
---|
513 | [1,3:@ |
---|
514 | |#n3 #v1 whd in ⊢ (??%?); |
---|
515 | cases (eqb n2 n3);@ ] |
---|
516 | |>(update_s content …) @nmk |
---|
517 | #Hfalse destruct |
---|
518 | |(*H2*) napply daemon |
---|
519 | |(*H4*) napply daemon |
---|
520 | |##skip ] |
---|
521 | |whd in ⊢ (% → ?);#H4 elim H;#H5 elim (H5 ?);//; |
---|
522 | |nchange in ⊢ (% → ?) with (p1 < p2);#H4 |
---|
523 | (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]], |
---|
524 | therefore [ |
---|
525 | set_cont n1 (p1 + 1) m p2] is [Cont]. *) |
---|
526 | >(set_cont_inside …) |
---|
527 | [@ |
---|
528 | |(*H1*)napply daemon |
---|
529 | |(*H4*)napply daemon] |
---|
530 | ] |
---|
531 | |//] |
---|
532 | qed. |
---|
533 | |
---|
534 | lemma getN_setN_mismatch: |
---|
535 | ∀n1,n2,p,v,m. |
---|
536 | n1 ≠ n2 → |
---|
537 | getN n2 p (setN n1 p v m) = Vundef. |
---|
538 | #n1 #n2 #p #v #m #H |
---|
539 | nchange in ⊢ (??(???%)?) with (update ????); |
---|
540 | whd in ⊢(??%?);>(update_s content …) |
---|
541 | whd in ⊢(??%?);>(not_eq_to_eqb_false … (sym_neq … H)) //; |
---|
542 | qed. |
---|
543 | |
---|
544 | lemma getN_setN_characterization: |
---|
545 | ∀m,v,n1,p1,n2,p2. |
---|
546 | getN n2 p2 (setN n1 p1 v m) = v |
---|
547 | ∨ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m |
---|
548 | ∨ getN n2 p2 (setN n1 p1 v m) = Vundef. |
---|
549 | #m #v #n1 #p1 #n2 #p2 |
---|
550 | lapply (eqZb_to_Prop p1 p2); cases (eqZb p1 p2); #Hp |
---|
551 | [>Hp |
---|
552 | @(eqb_elim n1 n2) #Hn |
---|
553 | [>Hn % % //; |
---|
554 | |%{2} /2/] |
---|
555 | |lapply (Z_compare_to_Prop (p1 + n1) p2); |
---|
556 | cases (Z_compare (p1 + n1) p2);#Hcmp |
---|
557 | [% %{2} @getN_setN_other /2/ |
---|
558 | |lapply (Z_compare_to_Prop (p2 + n2) p1); |
---|
559 | cases (Z_compare (p2 + n2) p1);#Hcmp2 |
---|
560 | [% %{2} @getN_setN_other /2/ |
---|
561 | |%{2} @getN_setN_overlap |
---|
562 | [// |
---|
563 | |*:(* arith *) napply daemon] |
---|
564 | |%{2} @getN_setN_overlap |
---|
565 | [// |
---|
566 | |*:(* arith *) napply daemon] |
---|
567 | ] |
---|
568 | |lapply (Z_compare_to_Prop (p2 + n2) p1); |
---|
569 | cases (Z_compare (p2 + n2) p1);#Hcmp2 |
---|
570 | [% %{2} @getN_setN_other /2/ |
---|
571 | |%{2} @getN_setN_overlap |
---|
572 | [// |
---|
573 | |*:(* arith *) napply daemon] |
---|
574 | |%{2} @getN_setN_overlap |
---|
575 | [// |
---|
576 | |*:(* arith *) napply daemon] |
---|
577 | ] |
---|
578 | ] |
---|
579 | ] |
---|
580 | qed. |
---|
581 | |
---|
582 | lemma getN_init: |
---|
583 | ∀n,p. |
---|
584 | getN n p (λ_.Undef) = Vundef. |
---|
585 | #n #p //; |
---|
586 | qed. |
---|
587 | *) |
---|
588 | (* pointer_compat block_region pointer_region *) |
---|
589 | |
---|
590 | inductive pointer_compat : region → region → Prop ≝ |
---|
591 | | same_compat : ∀s. pointer_compat s s |
---|
592 | | pxdata_compat : pointer_compat PData XData |
---|
593 | | universal_compat : ∀b. pointer_compat b Any. |
---|
594 | |
---|
595 | lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. |
---|
596 | #b #p cases b |
---|
597 | cases p /2/ %2 % #H inversion H #e1 #e2 destruct #e3 destruct |
---|
598 | qed. |
---|
599 | |
---|
600 | definition is_pointer_compat : region → region → bool ≝ |
---|
601 | λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ]. |
---|
602 | |
---|
603 | (* [valid_access m chunk r b ofs] holds if a memory access (load or store) |
---|
604 | of the given chunk is possible in [m] at address [b, ofs]. |
---|
605 | This means: |
---|
606 | - The block [b] is valid. |
---|
607 | - The range of bytes accessed is within the bounds of [b]. |
---|
608 | - The offset [ofs] is aligned. |
---|
609 | - The pointer representation (i.e., region) [r] is compatible with the class of [b]. |
---|
610 | *) |
---|
611 | |
---|
612 | inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z) |
---|
613 | : Prop ≝ |
---|
614 | | valid_access_intro: |
---|
615 | valid_block m b → |
---|
616 | low_bound m b ≤ ofs → |
---|
617 | ofs + size_chunk chunk ≤ high_bound m b → |
---|
618 | (align_chunk chunk ∣ ofs) → |
---|
619 | pointer_compat (block_region m b) r → |
---|
620 | valid_access m chunk r b ofs. |
---|
621 | |
---|
622 | (* The following function checks whether accessing the given memory chunk |
---|
623 | at the given offset in the given block respects the bounds of the block. *) |
---|
624 | |
---|
625 | (* XXX: Using + and ¬ instead of Sum and Not causes trouble *) |
---|
626 | let rec in_bounds |
---|
627 | (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : |
---|
628 | Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?. |
---|
629 | cases b #br #bi |
---|
630 | @(Zltb_elim_Type0 bi (nextblock m)) #Hnext |
---|
631 | [ @(Zleb_elim_Type0 (low_bound m 〈br,bi〉) ofs) #Hlo |
---|
632 | [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m 〈br,bi〉)) #Hhi |
---|
633 | [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal |
---|
634 | [ cases (pointer_compat_dec (block_region m 〈br,bi〉) r); #Hcl |
---|
635 | [ %1 % // @Hnext ] |
---|
636 | ] |
---|
637 | ] |
---|
638 | ] |
---|
639 | ] |
---|
640 | %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ] |
---|
641 | qed. |
---|
642 | |
---|
643 | lemma in_bounds_true: |
---|
644 | ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A. |
---|
645 | valid_access m chunk r b ofs -> |
---|
646 | (match in_bounds m chunk r b ofs with |
---|
647 | [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1. |
---|
648 | #m #chunk #r #b #ofs #A #a1 #a2 #H |
---|
649 | cases (in_bounds m chunk r b ofs);normalize;#H1 |
---|
650 | [// |
---|
651 | |elim (?:False); @(absurd ? H H1)] |
---|
652 | qed. |
---|
653 | |
---|
654 | (* [valid_pointer] holds if the given block address is valid (and can be |
---|
655 | represented in a pointer with the region [r]) and the |
---|
656 | given offset falls within the bounds of the corresponding block. *) |
---|
657 | |
---|
658 | definition valid_pointer : mem → region → block → Z → bool ≝ |
---|
659 | λm,r,b,ofs. Zltb (\snd b) (nextblock m) ∧ |
---|
660 | Zleb (low_bound m b) ofs ∧ |
---|
661 | Zltb ofs (high_bound m b) ∧ |
---|
662 | is_pointer_compat (block_region m b) r. |
---|
663 | |
---|
664 | (* [load chunk m r b ofs] perform a read in memory state [m], at address |
---|
665 | [b] and offset [ofs]. [None] is returned if the address is invalid |
---|
666 | or the memory access is out of bounds or the address cannot be represented |
---|
667 | by a pointer with region [r]. *) |
---|
668 | |
---|
669 | definition load : memory_chunk → mem → region → block → Z → option val ≝ |
---|
670 | λchunk,m,r,b,ofs. |
---|
671 | match in_bounds m chunk r b ofs with |
---|
672 | [ inl _ ⇒ Some ? (load_result chunk |
---|
673 | (getN (pred_size_chunk chunk) ofs (contents (blocks m b)))) |
---|
674 | | inr _ ⇒ None ? ]. |
---|
675 | |
---|
676 | lemma load_inv: |
---|
677 | ∀chunk,m,r,b,ofs,v. |
---|
678 | load chunk m r b ofs = Some ? v → |
---|
679 | valid_access m chunk r b ofs ∧ |
---|
680 | v = load_result chunk |
---|
681 | (getN (pred_size_chunk chunk) ofs (contents (blocks m b))). |
---|
682 | #chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?); |
---|
683 | cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H |
---|
684 | [ % //; destruct; //; |
---|
685 | | destruct |
---|
686 | ] |
---|
687 | qed. |
---|
688 | |
---|
689 | (* [loadv chunk m addr] is similar, but the address and offset are given |
---|
690 | as a single value [addr], which must be a pointer value. *) |
---|
691 | |
---|
692 | let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝ |
---|
693 | match addr with |
---|
694 | [ Vptr r b ofs ⇒ load chunk m r b (signed ofs) |
---|
695 | | _ ⇒ None ? ]. |
---|
696 | |
---|
697 | (* The memory state [m] after a store of value [v] at offset [ofs] |
---|
698 | in block [b]. *) |
---|
699 | |
---|
700 | definition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝ |
---|
701 | λchunk,m,b,ofs,v. |
---|
702 | let c ≝ (blocks m b) in |
---|
703 | mk_mem |
---|
704 | (update_block ? b |
---|
705 | (mk_block_contents (low c) (high c) |
---|
706 | (setN (pred_size_chunk chunk) ofs v (contents c))) |
---|
707 | (blocks m)) |
---|
708 | (nextblock m) |
---|
709 | (nextblock_pos m). |
---|
710 | |
---|
711 | (* [store chunk m r b ofs v] perform a write in memory state [m]. |
---|
712 | Value [v] is stored at address [b] and offset [ofs]. |
---|
713 | Return the updated memory store, or [None] if the address is invalid |
---|
714 | or the memory access is out of bounds or the address cannot be represented |
---|
715 | by a pointer with region [r]. *) |
---|
716 | |
---|
717 | definition store : memory_chunk → mem → region → block → Z → val → option mem ≝ |
---|
718 | λchunk,m,r,b,ofs,v. |
---|
719 | match in_bounds m chunk r b ofs with |
---|
720 | [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v) |
---|
721 | | inr _ ⇒ None ? ]. |
---|
722 | |
---|
723 | lemma store_inv: |
---|
724 | ∀chunk,m,r,b,ofs,v,m'. |
---|
725 | store chunk m r b ofs v = Some ? m' → |
---|
726 | valid_access m chunk r b ofs ∧ |
---|
727 | m' = unchecked_store chunk m b ofs v. |
---|
728 | #chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?); |
---|
729 | (*9*) |
---|
730 | cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq |
---|
731 | [% [//|destruct;//] |
---|
732 | |destruct] |
---|
733 | qed. |
---|
734 | |
---|
735 | (* [storev chunk m addr v] is similar, but the address and offset are given |
---|
736 | as a single value [addr], which must be a pointer value. *) |
---|
737 | |
---|
738 | definition storev : memory_chunk → mem → val → val → option mem ≝ |
---|
739 | λchunk,m,addr,v. |
---|
740 | match addr with |
---|
741 | [ Vptr r b ofs ⇒ store chunk m r b (signed ofs) v |
---|
742 | | _ ⇒ None ? ]. |
---|
743 | |
---|
744 | (* * Properties of the memory operations *) |
---|
745 | |
---|
746 | (* ** Properties related to block validity *) |
---|
747 | |
---|
748 | lemma valid_not_valid_diff: |
---|
749 | ∀m,b,b'. valid_block m b → ¬(valid_block m b') → b ≠ b'. |
---|
750 | #m #b #b' #H #H' @nmk #e >e in H #H |
---|
751 | @(absurd ? H H') |
---|
752 | qed. |
---|
753 | |
---|
754 | lemma valid_access_valid_block: |
---|
755 | ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b. |
---|
756 | #m #chunk #r #b #ofs #H |
---|
757 | elim H;//; |
---|
758 | qed. |
---|
759 | |
---|
760 | lemma valid_access_aligned: |
---|
761 | ∀m,chunk,r,b,ofs. |
---|
762 | valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs). |
---|
763 | #m #chunk #r #b #ofs #H |
---|
764 | elim H;//; |
---|
765 | qed. |
---|
766 | |
---|
767 | lemma valid_access_compat: |
---|
768 | ∀m,chunk1,chunk2,r,b,ofs. |
---|
769 | size_chunk chunk1 = size_chunk chunk2 → |
---|
770 | valid_access m chunk1 r b ofs → |
---|
771 | valid_access m chunk2 r b ofs. |
---|
772 | #m #chunk #chunk2 #r #b #ofs #H1 #H2 |
---|
773 | elim H2;#H3 #H4 #H5 #H6 #H7 |
---|
774 | >H1 in H5 #H5 |
---|
775 | % //; |
---|
776 | <(align_chunk_compat … H1) //; |
---|
777 | qed. |
---|
778 | |
---|
779 | (* Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.*) |
---|
780 | |
---|
781 | (* ** Properties related to [load] *) |
---|
782 | |
---|
783 | theorem valid_access_load: |
---|
784 | ∀m,chunk,r,b,ofs. |
---|
785 | valid_access m chunk r b ofs → |
---|
786 | ∃v. load chunk m r b ofs = Some ? v. |
---|
787 | #m #chunk #r #b #ofs #H % |
---|
788 | [2:whd in ⊢ (??%?);@in_bounds_true //; |
---|
789 | |skip] |
---|
790 | qed. |
---|
791 | |
---|
792 | theorem load_valid_access: |
---|
793 | ∀m,chunk,r,b,ofs,v. |
---|
794 | load chunk m r b ofs = Some ? v → |
---|
795 | valid_access m chunk r b ofs. |
---|
796 | #m #chunk #r #b #ofs #v #H |
---|
797 | cases (load_inv … H);//; |
---|
798 | qed. |
---|
799 | |
---|
800 | (* Hint Resolve load_valid_access valid_access_load.*) |
---|
801 | |
---|
802 | (* ** Properties related to [store] *) |
---|
803 | |
---|
804 | lemma valid_access_store: |
---|
805 | ∀m1,chunk,r,b,ofs,v. |
---|
806 | valid_access m1 chunk r b ofs → |
---|
807 | ∃m2. store chunk m1 r b ofs v = Some ? m2. |
---|
808 | #m1 #chunk #r #b #ofs #v #H |
---|
809 | % |
---|
810 | [2:@in_bounds_true // |
---|
811 | |skip] |
---|
812 | qed. |
---|
813 | |
---|
814 | (* section STORE *) |
---|
815 | |
---|
816 | lemma low_bound_store: |
---|
817 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
818 | ∀b'.low_bound m2 b' = low_bound m1 b'. |
---|
819 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
820 | #b' cases (store_inv … STORE) |
---|
821 | #H1 #H2 >H2 |
---|
822 | whd in ⊢ (??(?%?)?) whd in ⊢ (??%?) |
---|
823 | whd in ⊢ (??(?%)?) @eq_block_elim #E |
---|
824 | normalize // |
---|
825 | qed. |
---|
826 | |
---|
827 | lemma nextblock_store : |
---|
828 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
829 | nextblock m2 = nextblock m1. |
---|
830 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
831 | cases (store_inv … STORE); |
---|
832 | #Hvalid #Heq |
---|
833 | >Heq % |
---|
834 | qed. |
---|
835 | |
---|
836 | lemma high_bound_store: |
---|
837 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
838 | ∀b'. high_bound m2 b' = high_bound m1 b'. |
---|
839 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
840 | #b' cases (store_inv … STORE); |
---|
841 | #Hvalid #H |
---|
842 | >H |
---|
843 | whd in ⊢ (??(?%?)?);whd in ⊢ (??%?); |
---|
844 | whd in ⊢ (??(?%)?); @eq_block_elim #E |
---|
845 | normalize;//; |
---|
846 | qed. |
---|
847 | |
---|
848 | lemma region_store: |
---|
849 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
850 | ∀b'. block_region m2 b' = block_region m1 b'. |
---|
851 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
852 | * #r #b' // |
---|
853 | qed. |
---|
854 | |
---|
855 | lemma store_valid_block_1: |
---|
856 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
857 | ∀b'. valid_block m1 b' → valid_block m2 b'. |
---|
858 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
859 | #b' whd in ⊢ (% → %);#Hv |
---|
860 | >(nextblock_store … STORE) //; |
---|
861 | qed. |
---|
862 | |
---|
863 | lemma store_valid_block_2: |
---|
864 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
865 | ∀b'. valid_block m2 b' → valid_block m1 b'. |
---|
866 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
867 | #b' whd in ⊢ (%→%); |
---|
868 | >(nextblock_store … STORE) //; |
---|
869 | qed. |
---|
870 | |
---|
871 | (*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*) |
---|
872 | |
---|
873 | lemma store_valid_access_1: |
---|
874 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
875 | ∀chunk',r',b',ofs'. |
---|
876 | valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'. |
---|
877 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
878 | #chunk' #r' #b' #ofs' |
---|
879 | * Hv; |
---|
880 | #Hvb #Hl #Hr #Halign #Hptr |
---|
881 | % //; |
---|
882 | [@(store_valid_block_1 … STORE) // |
---|
883 | |>(low_bound_store … STORE …) // |
---|
884 | |>(high_bound_store … STORE …) // |
---|
885 | |>(region_store … STORE …) //] |
---|
886 | qed. |
---|
887 | |
---|
888 | lemma store_valid_access_2: |
---|
889 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
890 | ∀chunk',r',b',ofs'. |
---|
891 | valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'. |
---|
892 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
893 | #chunk' #r' #b' #ofs' |
---|
894 | * Hv; |
---|
895 | #Hvb #Hl #Hr #Halign #Hcompat |
---|
896 | % //; |
---|
897 | [@(store_valid_block_2 … STORE) // |
---|
898 | |<(low_bound_store … STORE …) // |
---|
899 | |<(high_bound_store … STORE …) // |
---|
900 | |<(region_store … STORE …) //] |
---|
901 | qed. |
---|
902 | |
---|
903 | lemma store_valid_access_3: |
---|
904 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
905 | valid_access m1 chunk r b ofs. |
---|
906 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
907 | cases (store_inv … STORE);//; |
---|
908 | qed. |
---|
909 | |
---|
910 | (*Hint Resolve store_valid_access_1 store_valid_access_2 |
---|
911 | store_valid_access_3: mem.*) |
---|
912 | |
---|
913 | lemma load_compat_pointer: |
---|
914 | ∀chunk,m,r,r',b,ofs,v. |
---|
915 | pointer_compat (block_region m b) r' → |
---|
916 | load chunk m r b ofs = Some ? v → |
---|
917 | load chunk m r' b ofs = Some ? v. |
---|
918 | #chunk #m #r #r' #b #ofs #v #Hcompat #LOAD |
---|
919 | lapply (load_valid_access … LOAD); #Hvalid |
---|
920 | cut (valid_access m chunk r' b ofs); |
---|
921 | [ % elim Hvalid; //; |
---|
922 | | #Hvalid' |
---|
923 | <LOAD whd in ⊢ (??%%); |
---|
924 | >(in_bounds_true … (option val) ?? Hvalid) |
---|
925 | >(in_bounds_true … (option val) ?? Hvalid') |
---|
926 | // |
---|
927 | ] qed. |
---|
928 | |
---|
929 | (* Nonessential properties that may require arithmetic |
---|
930 | theorem load_store_similar: |
---|
931 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
932 | ∀chunk'. |
---|
933 | size_chunk chunk' = size_chunk chunk → |
---|
934 | load chunk' m2 r b ofs = Some ? (load_result chunk' v). |
---|
935 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
936 | #chunk' #Hsize cases (store_inv … STORE); |
---|
937 | #Hv #Heq |
---|
938 | whd in ⊢ (??%?); |
---|
939 | nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) |
---|
940 | (None ?) ?); |
---|
941 | [>Heq |
---|
942 | whd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?); |
---|
943 | >(update_s ? b ? (blocks m1)) (* XXX too many metas for my taste *) |
---|
944 | >(? : pred_size_chunk chunk = pred_size_chunk chunk') |
---|
945 | [//; |
---|
946 | |>(size_chunk_pred …) in Hsize #Hsize |
---|
947 | >(size_chunk_pred …) in Hsize #Hsize |
---|
948 | @injective_Z_of_nat @(injective_Zplus_r 1) //;] |
---|
949 | |@(store_valid_access_1 … STORE) |
---|
950 | cases Hv;#H1 #H2 #H3 #H4 #H5 % //; |
---|
951 | >(align_chunk_compat … Hsize) //] |
---|
952 | qed. |
---|
953 | |
---|
954 | theorem load_store_same: |
---|
955 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
956 | load chunk m2 r b ofs = Some ? (load_result chunk v). |
---|
957 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
958 | @load_store_similar //; |
---|
959 | qed. |
---|
960 | |
---|
961 | theorem load_store_other: |
---|
962 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
963 | ∀chunk',r',b',ofs'. |
---|
964 | b' ≠ b |
---|
965 | ∨ ofs' + size_chunk chunk' ≤ ofs |
---|
966 | ∨ ofs + size_chunk chunk ≤ ofs' → |
---|
967 | load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'. |
---|
968 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
969 | #chunk' #r' #b' #ofs' #H |
---|
970 | cases (store_inv … STORE); |
---|
971 | #Hvalid #Heq whd in ⊢ (??%%); |
---|
972 | cases (in_bounds m1 chunk' r' b' ofs'); |
---|
973 | [#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??) |
---|
974 | [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk')) |
---|
975 | >Heq whd in ⊢ (??(???(? (? % ?)))?); |
---|
976 | whd in ⊢ (??(???(? %))?); |
---|
977 | lapply (eqZb_to_Prop b' b);cases (eqZb b' b); |
---|
978 | whd in ⊢ (% → ?); |
---|
979 | [#Heq1 >Heq1 whd in ⊢ (??(??? (? %))?); |
---|
980 | >(size_chunk_pred …) in H |
---|
981 | >(size_chunk_pred …) #H |
---|
982 | @(getN_setN_other …) cases H |
---|
983 | [* |
---|
984 | [#Hfalse elim Hfalse;#H1 elim (H1 Heq1) |
---|
985 | |#H1 %{2} (*H1*)napply daemon ] |
---|
986 | |#H1 % (*H1*)napply daemon ] |
---|
987 | |#Hneq @ ] |
---|
988 | |@(store_valid_access_1 … STORE) //] |
---|
989 | |whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs'); |
---|
990 | #H1 cases H1; |
---|
991 | [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse |
---|
992 | cases H3;#H4 elim (H4 Hfalse) |
---|
993 | |#H2 #H3 @] |
---|
994 | ] |
---|
995 | qed. |
---|
996 | |
---|
997 | |
---|
998 | theorem load_store_overlap: |
---|
999 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
1000 | ∀chunk',ofs',v'. load chunk' m2 r b ofs' = Some ? v' → |
---|
1001 | ofs' ≠ ofs → |
---|
1002 | ofs < ofs' + size_chunk chunk' → |
---|
1003 | ofs' < ofs + size_chunk chunk → |
---|
1004 | v' = Vundef. |
---|
1005 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
1006 | #chunk' #ofs' #v' #H |
---|
1007 | #H1 #H2 #H3 |
---|
1008 | cases (store_inv … STORE); |
---|
1009 | cases (load_inv … H); |
---|
1010 | #Hvalid #Heq #Hvalid1 #Heq1 >Heq >Heq1 |
---|
1011 | nchange in ⊢ (??(??(???(?(?%?))))?) with (mk_mem ???); |
---|
1012 | >(update_s block_contents …) |
---|
1013 | >(getN_setN_overlap …) |
---|
1014 | [cases chunk';// |
---|
1015 | |>(size_chunk_pred …) in H2 (*arith*) napply daemon |
---|
1016 | |>(size_chunk_pred …) in H3 (*arith*) napply daemon |
---|
1017 | |@sym_neq //] |
---|
1018 | qed. |
---|
1019 | |
---|
1020 | theorem load_store_overlap': |
---|
1021 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
1022 | ∀chunk',ofs'. |
---|
1023 | valid_access m1 chunk' r b ofs' → |
---|
1024 | ofs' ≠ ofs → |
---|
1025 | ofs < ofs' + size_chunk chunk' → |
---|
1026 | ofs' < ofs + size_chunk chunk → |
---|
1027 | load chunk' m2 r b ofs' = Some ? Vundef. |
---|
1028 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
1029 | #chunk' #ofs' #Hvalid #H #H1 #H2 |
---|
1030 | cut (∃v'.load chunk' m2 r b ofs' = Some ? v') |
---|
1031 | [@valid_access_load |
---|
1032 | @(store_valid_access_1 … STORE) // |
---|
1033 | |#H3 cases H3; |
---|
1034 | #x #Hx >Hx @(eq_f … (Some val)) |
---|
1035 | @(load_store_overlap … STORE … Hx) //;] |
---|
1036 | qed. |
---|
1037 | |
---|
1038 | theorem load_store_mismatch: |
---|
1039 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
1040 | ∀chunk',v'. |
---|
1041 | load chunk' m2 r b ofs = Some ? v' → |
---|
1042 | size_chunk chunk' ≠ size_chunk chunk → |
---|
1043 | v' = Vundef. |
---|
1044 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
1045 | #chunk' #v' #H #H1 |
---|
1046 | cases (store_inv … STORE); |
---|
1047 | cases (load_inv … H); |
---|
1048 | #Hvalid #H2 #Hvalid1 #H3 |
---|
1049 | >H2 |
---|
1050 | nchange in H3:(???%) with (mk_mem ???); |
---|
1051 | >H3 >(update_s block_contents …) |
---|
1052 | >(getN_setN_mismatch …) |
---|
1053 | [cases chunk';//; |
---|
1054 | |>(size_chunk_pred …) in H1 >(size_chunk_pred …) |
---|
1055 | #H1 @nmk #Hfalse elim H1;#H4 @H4 |
---|
1056 | @(eq_f ?? (λx.1 + x) ???) //] |
---|
1057 | qed. |
---|
1058 | |
---|
1059 | theorem load_store_mismatch': |
---|
1060 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
1061 | ∀chunk'. |
---|
1062 | valid_access m1 chunk' r b ofs → |
---|
1063 | size_chunk chunk' ≠ size_chunk chunk → |
---|
1064 | load chunk' m2 r b ofs = Some ? Vundef. |
---|
1065 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
1066 | #chunk' #Hvalid #Hsize |
---|
1067 | cut (∃v'.load chunk' m2 r b ofs = Some ? v') |
---|
1068 | [@(valid_access_load …) |
---|
1069 | napply |
---|
1070 | (store_valid_access_1 … STORE);// |
---|
1071 | |*;#x #Hx >Hx @(eq_f … (Some val)) |
---|
1072 | @(load_store_mismatch … STORE … Hsize) //;] |
---|
1073 | qed. |
---|
1074 | |
---|
1075 | inductive load_store_cases |
---|
1076 | (chunk1: memory_chunk) (b1: block) (ofs1: Z) |
---|
1077 | (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type[0] ≝ |
---|
1078 | | lsc_similar: |
---|
1079 | b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 = size_chunk chunk2 → |
---|
1080 | load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 |
---|
1081 | | lsc_other: |
---|
1082 | b1 ≠ b2 ∨ ofs2 + size_chunk chunk2 ≤ ofs1 ∨ ofs1 + size_chunk chunk1 ≤ ofs2 → |
---|
1083 | load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 |
---|
1084 | | lsc_overlap: |
---|
1085 | b1 = b2 -> ofs1 ≠ ofs2 -> ofs1 < ofs2 + size_chunk chunk2 → ofs2 < ofs1 + size_chunk chunk1 -> |
---|
1086 | load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2 |
---|
1087 | | lsc_mismatch: |
---|
1088 | b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 ≠ size_chunk chunk2 -> |
---|
1089 | load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. |
---|
1090 | |
---|
1091 | definition load_store_classification: |
---|
1092 | ∀chunk1,b1,ofs1,chunk2,b2,ofs2. |
---|
1093 | load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2. |
---|
1094 | #chunk1 #b1 #ofs1 #chunk2 #b2 #ofs2 |
---|
1095 | cases (decidable_eq_Z_Type b1 b2);#H |
---|
1096 | [cases (decidable_eq_Z_Type ofs1 ofs2);#H1 |
---|
1097 | [cases (decidable_eq_Z_Type (size_chunk chunk1) (size_chunk chunk2));#H2 |
---|
1098 | [@lsc_similar //; |
---|
1099 | |@lsc_mismatch //;] |
---|
1100 | |lapply (Z_compare_to_Prop (ofs2 + size_chunk chunk2) ofs1); |
---|
1101 | cases (Z_compare (ofs2+size_chunk chunk2) ofs1); |
---|
1102 | [nchange with (Zlt ? ? → ?);#H2 |
---|
1103 | @lsc_other % %{2} (*trivial Zlt_to_Zle BUT the statement is strange*) |
---|
1104 | napply daemon |
---|
1105 | |nchange with (? = ? → ?);#H2 |
---|
1106 | @lsc_other % %{2} (*trivial eq_to_Zle not defined *) napply daemon |
---|
1107 | |nchange with (Zlt ? ? → ?);#H2 |
---|
1108 | lapply (Z_compare_to_Prop (ofs1 + size_chunk chunk1) ofs2); |
---|
1109 | cases (Z_compare (ofs1 + size_chunk chunk1) ofs2); |
---|
1110 | [nchange with (Zlt ? ? → ?);#H3 |
---|
1111 | @lsc_other %{2} (*trivial as previously*) napply daemon |
---|
1112 | |nchange with (? = ? → ?);#H3 |
---|
1113 | @lsc_other %{2} (*trivial as previously*) napply daemon |
---|
1114 | |nchange with (Zlt ? ? → ?);#H3 |
---|
1115 | @lsc_overlap //;] |
---|
1116 | ] |
---|
1117 | ] |
---|
1118 | |@lsc_other % % (* XXX // doesn't spot this! *) napply H ] |
---|
1119 | qed. |
---|
1120 | |
---|
1121 | theorem load_store_characterization: |
---|
1122 | ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → |
---|
1123 | ∀chunk',r',b',ofs'. |
---|
1124 | valid_access m1 chunk' r' b' ofs' → |
---|
1125 | load chunk' m2 r' b' ofs' = |
---|
1126 | match load_store_classification chunk b ofs chunk' b' ofs' with |
---|
1127 | [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v) |
---|
1128 | | lsc_other _ ⇒ load chunk' m1 r' b' ofs' |
---|
1129 | | lsc_overlap _ _ _ _ ⇒ Some ? Vundef |
---|
1130 | | lsc_mismatch _ _ _ ⇒ Some ? Vundef ]. |
---|
1131 | #chunk #m1 #r #b #ofs #v #m2 #STORE |
---|
1132 | #chunk' #r' #b' #ofs' #Hvalid |
---|
1133 | cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v') |
---|
1134 | [@valid_access_load |
---|
1135 | @(store_valid_access_1 … STORE … Hvalid) |
---|
1136 | |*;#x #Hx |
---|
1137 | cases (load_store_classification chunk b ofs chunk' b' ofs') |
---|
1138 | [#H1 #H2 #H3 whd in ⊢ (???%);<H1 <H2 |
---|
1139 | @(load_compat_pointer … r) |
---|
1140 | [ >(region_store … STORE b) |
---|
1141 | cases Hvalid; //; |
---|
1142 | | @(load_store_similar … STORE) //; |
---|
1143 | ] |
---|
1144 | |#H1 @(load_store_other … STORE) |
---|
1145 | cases H1 |
---|
1146 | [* |
---|
1147 | [#H2 % % @sym_neq // |
---|
1148 | |#H2 % %{2} //] |
---|
1149 | |#H2 %{2} //] |
---|
1150 | |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx); |
---|
1151 | [ >(region_store … STORE b') |
---|
1152 | >H1 elim (store_valid_access_3 … STORE); // |
---|
1153 | | <H1 in ⊢ (% → ?) #Hx' |
---|
1154 | <H1 in Hx #Hx >Hx |
---|
1155 | @(eq_f … (Some val)) @(load_store_overlap … STORE … Hx') /2/; |
---|
1156 | ] |
---|
1157 | |#H1 #H2 #H3 |
---|
1158 | lapply (load_compat_pointer … r … Hx); |
---|
1159 | [ >(region_store … STORE b') |
---|
1160 | >H1 elim (store_valid_access_3 … STORE); // |
---|
1161 | | <H1 in Hx ⊢ % <H2 #Hx #Hx' |
---|
1162 | >Hx @(eq_f … (Some val)) |
---|
1163 | @(load_store_mismatch … STORE … Hx') /2/ |
---|
1164 | ] |
---|
1165 | ] |
---|
1166 | |
---|
1167 | ] |
---|
1168 | qed. |
---|
1169 | |
---|
1170 | (*lemma d : ∀a,b,c,d:nat.∀e:〈a,b〉 = 〈c,d〉. ∀P:(∀a,b,c,d,e.Prop). |
---|
1171 | P a b c d e → P a b a b (refl ??). |
---|
1172 | #a #b #c #d #e #P #H1 destruct;*) |
---|
1173 | |
---|
1174 | (* |
---|
1175 | Section ALLOC. |
---|
1176 | |
---|
1177 | Variable m1: mem. |
---|
1178 | Variables lo hi: Z. |
---|
1179 | Variable m2: mem. |
---|
1180 | Variable b: block. |
---|
1181 | Hypothesis ALLOC: alloc m1 lo hi = (m2, b). |
---|
1182 | *) |
---|
1183 | |
---|
1184 | definition pairdisc ≝ |
---|
1185 | λA,B.λx,y:Prod A B. |
---|
1186 | match x with |
---|
1187 | [(pair t0 t1) ⇒ |
---|
1188 | match y with |
---|
1189 | [(pair u0 u1) ⇒ |
---|
1190 | ∀P: Type[1]. |
---|
1191 | (∀e0: (eq A (R0 ? t0) u0). |
---|
1192 | ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. |
---|
1193 | |
---|
1194 | lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. |
---|
1195 | #A #B #x #y #e >e cases y; |
---|
1196 | #a #b normalize;#P #PH @PH % |
---|
1197 | qed. |
---|
1198 | |
---|
1199 | lemma nextblock_alloc: |
---|
1200 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1201 | nextblock m2 = Zsucc (nextblock m1). |
---|
1202 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1203 | whd in ALLOC:(??%%); destruct; //; |
---|
1204 | qed. |
---|
1205 | |
---|
1206 | lemma alloc_result: |
---|
1207 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1208 | b = nextblock m1. |
---|
1209 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1210 | whd in ALLOC:(??%%); destruct; //; |
---|
1211 | qed. |
---|
1212 | |
---|
1213 | |
---|
1214 | lemma valid_block_alloc: |
---|
1215 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1216 | ∀b'. valid_block m1 b' → valid_block m2 b'. |
---|
1217 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1218 | #b' >(unfold_valid_block m1 b') |
---|
1219 | >(unfold_valid_block m2 b') |
---|
1220 | >(nextblock_alloc … ALLOC) |
---|
1221 | (* arith *) @daemon |
---|
1222 | qed. |
---|
1223 | |
---|
1224 | lemma fresh_block_alloc: |
---|
1225 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1226 | ¬(valid_block m1 b). |
---|
1227 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1228 | >(unfold_valid_block m1 b) |
---|
1229 | >(alloc_result … ALLOC) |
---|
1230 | (* arith *) @daemon |
---|
1231 | qed. |
---|
1232 | |
---|
1233 | lemma valid_new_block: |
---|
1234 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1235 | valid_block m2 b. |
---|
1236 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1237 | >(unfold_valid_block m2 b) |
---|
1238 | >(alloc_result … ALLOC) |
---|
1239 | >(nextblock_alloc … ALLOC) |
---|
1240 | (* arith *) @daemon |
---|
1241 | qed. |
---|
1242 | |
---|
1243 | (* |
---|
1244 | Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. |
---|
1245 | *) |
---|
1246 | |
---|
1247 | lemma valid_block_alloc_inv: |
---|
1248 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1249 | ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'. |
---|
1250 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1251 | #b' |
---|
1252 | >(unfold_valid_block m2 b') |
---|
1253 | >(unfold_valid_block m1 b') |
---|
1254 | >(nextblock_alloc … ALLOC) #H |
---|
1255 | >(alloc_result … ALLOC) |
---|
1256 | (* arith *) @daemon |
---|
1257 | qed. |
---|
1258 | |
---|
1259 | lemma low_bound_alloc: |
---|
1260 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1261 | ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'. |
---|
1262 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1263 | whd in ALLOC:(??%%); destruct; #b' |
---|
1264 | >(unfold_update block_contents ????) |
---|
1265 | cases (eqZb b' (nextblock m1)); //; |
---|
1266 | qed. |
---|
1267 | |
---|
1268 | lemma low_bound_alloc_same: |
---|
1269 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1270 | low_bound m2 b = lo. |
---|
1271 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1272 | >(low_bound_alloc … ALLOC b) |
---|
1273 | >(eqZb_z_z …) |
---|
1274 | //; |
---|
1275 | qed. |
---|
1276 | |
---|
1277 | lemma low_bound_alloc_other: |
---|
1278 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1279 | ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'. |
---|
1280 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1281 | #b' >(low_bound_alloc … ALLOC b') |
---|
1282 | @eqZb_elim #Hb |
---|
1283 | [ >Hb #bad @False_ind @(absurd ? bad) |
---|
1284 | napply (fresh_block_alloc … ALLOC) |
---|
1285 | | // |
---|
1286 | ] qed. |
---|
1287 | |
---|
1288 | lemma high_bound_alloc: |
---|
1289 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1290 | ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'. |
---|
1291 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1292 | whd in ALLOC:(??%%); destruct; #b' |
---|
1293 | >(unfold_update block_contents ????) |
---|
1294 | cases (eqZb b' (nextblock m1)); //; |
---|
1295 | qed. |
---|
1296 | |
---|
1297 | lemma high_bound_alloc_same: |
---|
1298 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1299 | high_bound m2 b = hi. |
---|
1300 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1301 | >(high_bound_alloc … ALLOC b) |
---|
1302 | >(eqZb_z_z …) |
---|
1303 | //; |
---|
1304 | qed. |
---|
1305 | |
---|
1306 | lemma high_bound_alloc_other: |
---|
1307 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1308 | ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'. |
---|
1309 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1310 | #b' >(high_bound_alloc … ALLOC b') |
---|
1311 | @eqZb_elim #Hb |
---|
1312 | [ >Hb #bad @False_ind @(absurd ? bad) |
---|
1313 | napply (fresh_block_alloc … ALLOC) |
---|
1314 | | // |
---|
1315 | ] qed. |
---|
1316 | |
---|
1317 | lemma class_alloc: |
---|
1318 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1319 | ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'. |
---|
1320 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1321 | whd in ALLOC:(??%%); destruct; #b' |
---|
1322 | cases (eqZb b' (nextblock m1)); //; |
---|
1323 | qed. |
---|
1324 | |
---|
1325 | lemma class_alloc_same: |
---|
1326 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1327 | block_region m2 b = bcl. |
---|
1328 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1329 | whd in ALLOC:(??%%); destruct; |
---|
1330 | >(eqZb_z_z ?) //; |
---|
1331 | qed. |
---|
1332 | |
---|
1333 | lemma class_alloc_other: |
---|
1334 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1335 | ∀b'. valid_block m1 b' → block_region m2 b' = block_region m1 b'. |
---|
1336 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1337 | #b' >(class_alloc … ALLOC b') |
---|
1338 | @eqZb_elim #Hb |
---|
1339 | [ >Hb #bad @False_ind @(absurd ? bad) |
---|
1340 | napply (fresh_block_alloc … ALLOC) |
---|
1341 | | // |
---|
1342 | ] qed. |
---|
1343 | |
---|
1344 | lemma valid_access_alloc_other: |
---|
1345 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1346 | ∀chunk,r,b',ofs. |
---|
1347 | valid_access m1 chunk r b' ofs → |
---|
1348 | valid_access m2 chunk r b' ofs. |
---|
1349 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1350 | #chunk #r #b' #ofs #H |
---|
1351 | cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat |
---|
1352 | % |
---|
1353 | [ @(valid_block_alloc … ALLOC) // |
---|
1354 | | >(low_bound_alloc_other … ALLOC b' Hvalid) // |
---|
1355 | | >(high_bound_alloc_other … ALLOC b' Hvalid) // |
---|
1356 | | // |
---|
1357 | | >(class_alloc_other … ALLOC b' Hvalid) //; |
---|
1358 | ] qed. |
---|
1359 | |
---|
1360 | lemma valid_access_alloc_same: |
---|
1361 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1362 | ∀chunk,r,ofs. |
---|
1363 | lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → |
---|
1364 | pointer_compat bcl r → |
---|
1365 | valid_access m2 chunk r b ofs. |
---|
1366 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1367 | #chunk #r #ofs #Hlo #Hhi #Halign #Hcompat |
---|
1368 | % |
---|
1369 | [ napply (valid_new_block … ALLOC) |
---|
1370 | | >(low_bound_alloc_same … ALLOC) // |
---|
1371 | | >(high_bound_alloc_same … ALLOC) // |
---|
1372 | | // |
---|
1373 | | >(class_alloc_same … ALLOC) // |
---|
1374 | ] qed. |
---|
1375 | |
---|
1376 | (* |
---|
1377 | Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. |
---|
1378 | *) |
---|
1379 | |
---|
1380 | lemma valid_access_alloc_inv: |
---|
1381 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1382 | ∀chunk,r,b',ofs. |
---|
1383 | valid_access m2 chunk r b' ofs → |
---|
1384 | valid_access m1 chunk r b' ofs ∨ |
---|
1385 | (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl r)). |
---|
1386 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1387 | #chunk #r #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct |
---|
1388 | elim (valid_block_alloc_inv … ALLOC ? Hblk);#H |
---|
1389 | [ <H in ALLOC ⊢ % #ALLOC' |
---|
1390 | >(low_bound_alloc_same … ALLOC') in Hlo #Hlo' |
---|
1391 | >(high_bound_alloc_same … ALLOC') in Hhi #Hhi' |
---|
1392 | >(class_alloc_same … ALLOC') in Hct #Hct |
---|
1393 | %{2} /4/; |
---|
1394 | | %{1} % //; |
---|
1395 | [ >(low_bound_alloc_other … ALLOC ??) in Hlo // |
---|
1396 | | >(high_bound_alloc_other … ALLOC ??) in Hhi // |
---|
1397 | | >(class_alloc_other … ALLOC ??) in Hct // |
---|
1398 | ] |
---|
1399 | ] qed. |
---|
1400 | |
---|
1401 | theorem load_alloc_unchanged: |
---|
1402 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 → |
---|
1403 | ∀chunk,r,b',ofs. |
---|
1404 | valid_block m1 b' → |
---|
1405 | load chunk m2 r b' ofs = load chunk m1 r b' ofs. |
---|
1406 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1407 | #chunk #r #b' #ofs #H whd in ⊢ (??%%); |
---|
1408 | cases (in_bounds m2 chunk r b' ofs); #H' |
---|
1409 | [ elim (valid_access_alloc_inv … ALLOC ???? H'); |
---|
1410 | [ #H'' (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error |
---|
1411 | >(in_bounds_true ???? ??? H'') *) >(in_bounds_true … ? (option val) ?? H'') |
---|
1412 | whd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *) |
---|
1413 | cut (b' ≠ b); |
---|
1414 | [ @(valid_not_valid_diff … H) @(fresh_block_alloc … ALLOC) |
---|
1415 | | whd in ALLOC:(??%%); destruct; |
---|
1416 | >(update_o block_contents ?????) /2/; |
---|
1417 | ] |
---|
1418 | | *;*;#A #B #C <A in ALLOC ⊢ % #ALLOC |
---|
1419 | @False_ind @(absurd ? H) napply (fresh_block_alloc … ALLOC) |
---|
1420 | ] |
---|
1421 | | cases (in_bounds m1 chunk r b' ofs); #H'' whd in ⊢ (??%%); //; |
---|
1422 | @False_ind @(absurd ? ? H') @(valid_access_alloc_other … ALLOC) // |
---|
1423 | ] qed. |
---|
1424 | |
---|
1425 | theorem load_alloc_other: |
---|
1426 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1427 | ∀chunk,r,b',ofs,v. |
---|
1428 | load chunk m1 r b' ofs = Some ? v → |
---|
1429 | load chunk m2 r b' ofs = Some ? v. |
---|
1430 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1431 | #chunk #r #b' #ofs #v #H |
---|
1432 | <H @(load_alloc_unchanged … ALLOC ???) cases (load_valid_access … H); //; |
---|
1433 | qed. |
---|
1434 | |
---|
1435 | theorem load_alloc_same: |
---|
1436 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1437 | ∀chunk,r,ofs,v. |
---|
1438 | load chunk m2 r b ofs = Some ? v → |
---|
1439 | v = Vundef. |
---|
1440 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1441 | #chunk #r #ofs #v #H |
---|
1442 | elim (load_inv … H); #H0 #H1 >H1 |
---|
1443 | whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC) |
---|
1444 | whd in ⊢ (??%% → ?);#e0 <e0 in ⊢ (%→?) |
---|
1445 | whd in ⊢ (??%% → ?);#e1 |
---|
1446 | <e1 <e0 >(update_s ? ? (empty_block lo hi bcl) ?) |
---|
1447 | normalize; cases chunk; //; |
---|
1448 | qed. |
---|
1449 | |
---|
1450 | theorem load_alloc_same': |
---|
1451 | ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → |
---|
1452 | ∀chunk,r,ofs. |
---|
1453 | lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → |
---|
1454 | pointer_compat bcl r → |
---|
1455 | load chunk m2 r b ofs = Some ? Vundef. |
---|
1456 | #m1 #lo #hi #bcl #m2 #b #ALLOC |
---|
1457 | #chunk #r #ofs #Hlo #Hhi #Hal #Hct |
---|
1458 | cut (∃v. load chunk m2 r b ofs = Some ? v); |
---|
1459 | [ @valid_access_load % //; |
---|
1460 | [ @(valid_new_block … ALLOC) |
---|
1461 | | >(low_bound_alloc_same … ALLOC) // |
---|
1462 | | >(high_bound_alloc_same … ALLOC) // |
---|
1463 | | >(class_alloc_same … ALLOC) // |
---|
1464 | ] |
---|
1465 | | *; #v #LOAD >LOAD @(eq_f … (Some val)) |
---|
1466 | @(load_alloc_same … ALLOC … LOAD) |
---|
1467 | ] qed. |
---|
1468 | |
---|
1469 | (* |
---|
1470 | End ALLOC. |
---|
1471 | |
---|
1472 | Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem. |
---|
1473 | Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. |
---|
1474 | Hint Resolve load_alloc_unchanged: mem. |
---|
1475 | |
---|
1476 | *) |
---|
1477 | |
---|
1478 | (* ** Properties related to [free]. *) |
---|
1479 | (* |
---|
1480 | Section FREE. |
---|
1481 | |
---|
1482 | Variable m: mem. |
---|
1483 | Variable bf: block. |
---|
1484 | *) |
---|
1485 | |
---|
1486 | lemma valid_block_free_1: |
---|
1487 | ∀m,bf,b. valid_block m b → valid_block (free m bf) b. |
---|
1488 | normalize;//; |
---|
1489 | qed. |
---|
1490 | |
---|
1491 | lemma valid_block_free_2: |
---|
1492 | ∀m,bf,b. valid_block (free m bf) b → valid_block m b. |
---|
1493 | normalize;//; |
---|
1494 | qed. |
---|
1495 | |
---|
1496 | (* |
---|
1497 | Hint Resolve valid_block_free_1 valid_block_free_2: mem. |
---|
1498 | *) |
---|
1499 | |
---|
1500 | lemma low_bound_free: |
---|
1501 | ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b. |
---|
1502 | #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); |
---|
1503 | >(update_o block_contents …) //; @sym_neq //; |
---|
1504 | qed. |
---|
1505 | |
---|
1506 | lemma high_bound_free: |
---|
1507 | ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b. |
---|
1508 | #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); |
---|
1509 | >(update_o block_contents …) //; @sym_neq //; |
---|
1510 | qed. |
---|
1511 | |
---|
1512 | lemma low_bound_free_same: |
---|
1513 | ∀m,b. low_bound (free m b) b = 0. |
---|
1514 | #m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); |
---|
1515 | >(update_s block_contents …) //; |
---|
1516 | qed. |
---|
1517 | |
---|
1518 | lemma high_bound_free_same: |
---|
1519 | ∀m,b. high_bound (free m b) b = 0. |
---|
1520 | #m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); |
---|
1521 | >(update_s block_contents …) //; |
---|
1522 | qed. |
---|
1523 | |
---|
1524 | lemma class_free: |
---|
1525 | ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b. |
---|
1526 | #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); |
---|
1527 | >(update_o block_contents …) //; @sym_neq //; |
---|
1528 | qed. |
---|
1529 | |
---|
1530 | lemma valid_access_free_1: |
---|
1531 | ∀m,bf,chunk,r,b,ofs. |
---|
1532 | valid_access m chunk r b ofs → b ≠ bf → |
---|
1533 | valid_access (free m bf) chunk r b ofs. |
---|
1534 | #m #bf #chunk #r #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq |
---|
1535 | % //; |
---|
1536 | [ @valid_block_free_1 // |
---|
1537 | | >(low_bound_free … Hneq) // |
---|
1538 | | >(high_bound_free … Hneq) // |
---|
1539 | | >(class_free … Hneq) // |
---|
1540 | ] qed. |
---|
1541 | |
---|
1542 | lemma valid_access_free_2: |
---|
1543 | ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs). |
---|
1544 | #m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct |
---|
1545 | whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo |
---|
1546 | whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi |
---|
1547 | whd in ⊢ ((??%)→(?%?)→?); (* arith *) @daemon |
---|
1548 | qed. |
---|
1549 | |
---|
1550 | (* |
---|
1551 | Hint Resolve valid_access_free_1 valid_access_free_2: mem. |
---|
1552 | *) |
---|
1553 | |
---|
1554 | lemma valid_access_free_inv: |
---|
1555 | ∀m,bf,chunk,r,b,ofs. |
---|
1556 | valid_access (free m bf) chunk r b ofs → |
---|
1557 | valid_access m chunk r b ofs ∧ b ≠ bf. |
---|
1558 | #m #bf #chunk #r #b #ofs elim (decidable_eq_Z_Type b bf); |
---|
1559 | [ #e >e |
---|
1560 | #H @False_ind @(absurd ? H (valid_access_free_2 …)) |
---|
1561 | | #ne *; >(low_bound_free … ne) |
---|
1562 | >(high_bound_free … ne) |
---|
1563 | >(class_free … ne) |
---|
1564 | #Hval #Hlo #Hhi #Hal #Hct |
---|
1565 | % [ % /2/; | /2/ ] |
---|
1566 | ] qed. |
---|
1567 | |
---|
1568 | theorem load_free: |
---|
1569 | ∀m,bf,chunk,r,b,ofs. |
---|
1570 | b ≠ bf → |
---|
1571 | load chunk (free m bf) r b ofs = load chunk m r b ofs. |
---|
1572 | #m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%); |
---|
1573 | elim (in_bounds m chunk r b ofs); |
---|
1574 | [ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???) |
---|
1575 | [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //; |
---|
1576 | @sym_neq // |
---|
1577 | | @valid_access_free_1 //; @ne |
---|
1578 | ] |
---|
1579 | | elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ] |
---|
1580 | #H #H' @False_ind @(absurd ? ? H') |
---|
1581 | elim (valid_access_free_inv …H); //; |
---|
1582 | ] qed. |
---|
1583 | |
---|
1584 | (* |
---|
1585 | End FREE. |
---|
1586 | *) |
---|
1587 | |
---|
1588 | (* ** Properties related to [free_list] *) |
---|
1589 | |
---|
1590 | lemma valid_block_free_list_1: |
---|
1591 | ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b. |
---|
1592 | #bl elim bl; |
---|
1593 | [ #m #b #H whd in ⊢ (?%?); // |
---|
1594 | | #h #t #IH #m #b #H >(unfold_free_list m h t) |
---|
1595 | @valid_block_free_1 @IH // |
---|
1596 | ] qed. |
---|
1597 | |
---|
1598 | lemma valid_block_free_list_2: |
---|
1599 | ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b. |
---|
1600 | #bl elim bl; |
---|
1601 | [ #m #b #H whd in H:(?%?); // |
---|
1602 | | #h #t #IH #m #b >(unfold_free_list m h t) #H |
---|
1603 | @IH @valid_block_free_2 // |
---|
1604 | ] qed. |
---|
1605 | |
---|
1606 | lemma valid_access_free_list: |
---|
1607 | ∀chunk,r,b,ofs,m,bl. |
---|
1608 | valid_access m chunk r b ofs → ¬in_list ? b bl → |
---|
1609 | valid_access (free_list m bl) chunk r b ofs. |
---|
1610 | #chunk #r #b #ofs #m #bl elim bl; |
---|
1611 | [ whd in ⊢ (?→?→(?%????)); // |
---|
1612 | | #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1 |
---|
1613 | [ @IH //; @(not_to_not ??? notin) #Ht napply (in_list_cons … Ht) |
---|
1614 | | @nmk #e @(absurd ?? notin) >e // ] |
---|
1615 | ] qed. |
---|
1616 | |
---|
1617 | lemma valid_access_free_list_inv: |
---|
1618 | ∀chunk,r,b,ofs,m,bl. |
---|
1619 | valid_access (free_list m bl) chunk r b ofs → |
---|
1620 | ¬in_list ? b bl ∧ valid_access m chunk r b ofs. |
---|
1621 | #chunk #r #b #ofs #m #bl elim bl; |
---|
1622 | [ whd in ⊢ ((?%????)→?); #H % // |
---|
1623 | | #h #t #IH >(unfold_free_list m h t) #H |
---|
1624 | elim (valid_access_free_inv … H); #H' #ne |
---|
1625 | elim (IH H'); #notin #H'' % //; |
---|
1626 | @(not_to_not ??? notin) #Ht |
---|
1627 | (* WTF? this is specialised to nat! @(in_list_tail t b h) *) napply daemon |
---|
1628 | ] qed. |
---|
1629 | |
---|
1630 | (* ** Properties related to pointer validity *) |
---|
1631 | |
---|
1632 | lemma valid_pointer_valid_access: |
---|
1633 | ∀m,r,b,ofs. |
---|
1634 | valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs. |
---|
1635 | #m #r #b #ofs whd in ⊢ (?(??%?)?); % |
---|
1636 | [ #H |
---|
1637 | lapply (andb_true_l … H); #H' |
---|
1638 | lapply (andb_true_l … H'); #H'' |
---|
1639 | lapply (andb_true_l … H''); #H1 |
---|
1640 | lapply (andb_true_r … H''); #H2 |
---|
1641 | lapply (andb_true_r … H'); #H3 |
---|
1642 | lapply (andb_true_r … H); #H4 |
---|
1643 | % |
---|
1644 | [ >(unfold_valid_block m b) napply (Zltb_true_to_Zlt … H1) |
---|
1645 | | napply (Zleb_true_to_Zle … H2) |
---|
1646 | | whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon |
---|
1647 | | cases ofs; /2/; |
---|
1648 | | whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4; |
---|
1649 | [ //; | #Hn #e whd in e:(??%%); destruct ] |
---|
1650 | ] |
---|
1651 | | *; #Hval #Hlo #Hhi #Hal #Hct |
---|
1652 | >(Zlt_to_Zltb_true … Hval) |
---|
1653 | >(Zle_to_Zleb_true … Hlo) |
---|
1654 | whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?) |
---|
1655 | [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r); |
---|
1656 | [ //; |
---|
1657 | | #Hct' @False_ind @(absurd … Hct Hct') |
---|
1658 | ] |
---|
1659 | | (* arith *) napply daemon |
---|
1660 | ] |
---|
1661 | ] |
---|
1662 | qed. |
---|
1663 | |
---|
1664 | theorem valid_pointer_alloc: |
---|
1665 | ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z. |
---|
1666 | alloc m1 lo hi bcl = 〈m2, b'〉 → |
---|
1667 | valid_pointer m1 r b ofs = true → |
---|
1668 | valid_pointer m2 r b ofs = true. |
---|
1669 | #m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID |
---|
1670 | lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval |
---|
1671 | @(proj2 ?? (valid_pointer_valid_access ????)) |
---|
1672 | @(valid_access_alloc_other … ALLOC … Hval) |
---|
1673 | qed. |
---|
1674 | |
---|
1675 | theorem valid_pointer_store: |
---|
1676 | ∀chunk: memory_chunk. ∀m1,m2: mem. |
---|
1677 | ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val. |
---|
1678 | store chunk m1 r' b' ofs' v = Some ? m2 → |
---|
1679 | valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. |
---|
1680 | #chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID |
---|
1681 | lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval |
---|
1682 | @(proj2 ?? (valid_pointer_valid_access ????)) |
---|
1683 | @(store_valid_access_1 … STORE … Hval) |
---|
1684 | qed. |
---|
1685 | |
---|
1686 | (* * * Generic injections between memory states. *) |
---|
1687 | (* |
---|
1688 | (* Section GENERIC_INJECT. *) |
---|
1689 | |
---|
1690 | definition meminj : Type[0] ≝ block → option (block × Z). |
---|
1691 | (* |
---|
1692 | Variable val_inj: meminj -> val -> val -> Prop. |
---|
1693 | |
---|
1694 | Hypothesis val_inj_undef: |
---|
1695 | ∀mi. val_inj mi Vundef Vundef. |
---|
1696 | *) |
---|
1697 | |
---|
1698 | definition mem_inj ≝ λval_inj.λmi: meminj. λm1,m2: mem. |
---|
1699 | ∀chunk, b1, ofs, v1, b2, delta. |
---|
1700 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1701 | load chunk m1 b1 ofs = Some ? v1 → |
---|
1702 | ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2. |
---|
1703 | |
---|
1704 | (* FIXME: another nunfold hack*) |
---|
1705 | lemma unfold_mem_inj : ∀val_inj.∀mi: meminj. ∀m1,m2: mem. |
---|
1706 | (mem_inj val_inj mi m1 m2) = |
---|
1707 | (∀chunk, b1, ofs, v1, b2, delta. |
---|
1708 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1709 | load chunk m1 b1 ofs = Some ? v1 → |
---|
1710 | ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2). |
---|
1711 | //; qed. |
---|
1712 | |
---|
1713 | lemma valid_access_inj: ∀val_inj. |
---|
1714 | ∀mi,m1,m2,chunk,b1,ofs,b2,delta. |
---|
1715 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1716 | mem_inj val_inj mi m1 m2 → |
---|
1717 | valid_access m1 chunk b1 ofs → |
---|
1718 | valid_access m2 chunk b2 (ofs + delta). |
---|
1719 | #val_inj |
---|
1720 | #mi #m1 #m2 #chunk #b1 #ofs #b2 #delta #H #Hinj #Hval |
---|
1721 | cut (∃v1. load chunk m1 b1 ofs = Some ? v1); |
---|
1722 | [ /2/; |
---|
1723 | | *;#v1 #LOAD1 |
---|
1724 | elim (Hinj … H LOAD1);#v2 *;#LOAD2 #VCP |
---|
1725 | /2/ |
---|
1726 | ] qed. |
---|
1727 | |
---|
1728 | (*Hint Resolve valid_access_inj: mem.*) |
---|
1729 | *) |
---|
1730 | (* FIXME: can't use destruct below *) |
---|
1731 | lemma grumpydestruct : ∀A,v. None A = Some A v → False. |
---|
1732 | #A #v #H destruct; |
---|
1733 | qed. |
---|
1734 | (* |
---|
1735 | lemma store_unmapped_inj: ∀val_inj. |
---|
1736 | ∀mi,m1,m2,r,b,ofs,v,chunk,m1'. |
---|
1737 | mem_inj val_inj mi m1 m2 → |
---|
1738 | mi b = None ? → |
---|
1739 | store chunk m1 r b ofs v = Some ? m1' → |
---|
1740 | mem_inj val_inj mi m1' m2. |
---|
1741 | #val_inj |
---|
1742 | #mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore |
---|
1743 | whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload |
---|
1744 | cut (load chunk0 m1 b1 ofs0 = Some ? v1); |
---|
1745 | [ <Hload @sym_eq @(load_store_other … Hstore) |
---|
1746 | %{1} %{1} @nmk #eq >eq in Hmi0 >Hmi #H destruct; |
---|
1747 | | #Hload' @(Hinj … Hmi0 Hload') |
---|
1748 | ] qed. |
---|
1749 | |
---|
1750 | lemma store_outside_inj: ∀val_inj. |
---|
1751 | ∀mi,m1,m2,chunk,r,b,ofs,v,m2'. |
---|
1752 | mem_inj val_inj mi m1 m2 → |
---|
1753 | (∀b',delta. |
---|
1754 | mi b' = Some ? 〈b, delta〉 → |
---|
1755 | high_bound m1 b' + delta ≤ ofs |
---|
1756 | ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) → |
---|
1757 | store chunk m2 r b ofs v = Some ? m2' → |
---|
1758 | mem_inj val_inj mi m1 m2'. |
---|
1759 | #val_inj |
---|
1760 | #mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore |
---|
1761 | whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload |
---|
1762 | lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ |
---|
1763 | %{ v2} % //; |
---|
1764 | <LOAD2 @(load_store_other … Hstore) |
---|
1765 | elim (decidable_eq_Z b2 b); |
---|
1766 | [ #Heq >Heq in Hmi0 LOAD2 #Hmi0 #LOAD2 |
---|
1767 | lapply (Hbounds … Hmi0); #Hb |
---|
1768 | cut (valid_access m1 chunk0 b1 ofs0); /2/; |
---|
1769 | #Hv elim Hv; #Hv1 #Hlo1 #Hhi1 #Hal1 |
---|
1770 | elim Hb; #Hb [ %{1} %{2} (* arith *) napply daemon | %{2} (* arith *) napply daemon ] |
---|
1771 | | #ineq %{1} %{1} @ineq |
---|
1772 | ] qed. |
---|
1773 | |
---|
1774 | (* XXX: use Or rather than ∨ to bring resource usage under control. *) |
---|
1775 | definition meminj_no_overlap ≝ λmi: meminj. λm: mem. |
---|
1776 | ∀b1,b1',delta1,b2,b2',delta2. |
---|
1777 | b1 ≠ b2 → |
---|
1778 | mi b1 = Some ? 〈b1', delta1〉 → |
---|
1779 | mi b2 = Some ? 〈b2', delta2〉 → |
---|
1780 | Or (Or (Or (b1' ≠ b2') |
---|
1781 | (low_bound m b1 ≥ high_bound m b1)) |
---|
1782 | (low_bound m b2 ≥ high_bound m b2)) |
---|
1783 | (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2) |
---|
1784 | (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)). |
---|
1785 | *) |
---|
1786 | (* FIXME *) |
---|
1787 | lemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2. |
---|
1788 | #A #x1 #x2 #H destruct;//; |
---|
1789 | qed. |
---|
1790 | lemma grumpydestruct2 : ∀A,B,x1,y1,x2,y2. Some (A×B) 〈x1,y1〉 = Some (A×B) 〈x2,y2〉 → x1 = x2 ∧ y1 = y2. |
---|
1791 | #A #B #x1 #y1 #x2 #y2 #H destruct;/2/; |
---|
1792 | qed. |
---|
1793 | (* |
---|
1794 | lemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef. |
---|
1795 | ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'. |
---|
1796 | mem_inj val_inj mi m1 m2 → |
---|
1797 | meminj_no_overlap mi m1 → |
---|
1798 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1799 | store chunk m1 b1 ofs v1 = Some ? m1' → |
---|
1800 | (∀chunk'. size_chunk chunk' = size_chunk chunk → |
---|
1801 | val_inj mi (load_result chunk' v1) (load_result chunk' v2)) → |
---|
1802 | ∃m2'. |
---|
1803 | store chunk m2 b2 (ofs + delta) v2 = Some ? m2' ∧ mem_inj val_inj mi m1' m2'. |
---|
1804 | #val_inj #val_inj_undef |
---|
1805 | #mi #m1 #m2 #b1 #ofs #b2 #delta #v1 #v2 #chunk #m1' |
---|
1806 | #Hinj #Hnoover #Hb1 #STORE #Hvalinj |
---|
1807 | cut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2'); |
---|
1808 | [ @valid_access_store @(valid_access_inj ? mi ??????? Hb1 Hinj ?) (* XXX why do I have to give mi here? *) /2/ |
---|
1809 | | *;#m2' #STORE2 |
---|
1810 | %{ m2'} % //; |
---|
1811 | whd; #chunk' #b1' #ofs' #v #b2' #delta' #CP #LOAD1 |
---|
1812 | cut (valid_access m1 chunk' b1' ofs'); |
---|
1813 | [ @(store_valid_access_2 … STORE) @(load_valid_access … LOAD1) |
---|
1814 | | #Hval |
---|
1815 | lapply (load_store_characterization … STORE … Hval); |
---|
1816 | elim (load_store_classification chunk b1 ofs chunk' b1' ofs'); |
---|
1817 | [ #e #e0 #e1 #H (* similar *) |
---|
1818 | >e in Hb1 #Hb1 |
---|
1819 | >CP in Hb1 #Hb1 (* XXX destruct expands proof state too much;*) |
---|
1820 | elim (grumpydestruct2 ?????? Hb1); |
---|
1821 | #e2 #e3 <e0 >e2 >e3 |
---|
1822 | %{ (load_result chunk' v2)} % |
---|
1823 | [ @(load_store_similar … STORE2) // |
---|
1824 | | >LOAD1 in H #H whd in H:(??%%); destruct; |
---|
1825 | @Hvalinj //; |
---|
1826 | ] |
---|
1827 | | #Hdis #H (* disjoint *) |
---|
1828 | >LOAD1 in H #H |
---|
1829 | lapply (Hinj … CP ?); [ @sym_eq @H | *: ] |
---|
1830 | *;#v2' *;#LOAD2 #VCP |
---|
1831 | %{ v2'} % //; |
---|
1832 | <LOAD2 @(load_store_other … STORE2) |
---|
1833 | elim (decidable_eq_Z b1 b1'); #eb1 |
---|
1834 | [ <eb1 in CP #CP >CP in Hb1 #eb2d |
---|
1835 | elim (grumpydestruct2 ?????? eb2d); #eb2 #ed |
---|
1836 | elim Hdis; [ #Hdis elim Hdis; |
---|
1837 | [ #eb1' @False_ind @(absurd ? eb1 eb1') |
---|
1838 | | #Hdis %{1} %{2} (* arith *) napply daemon |
---|
1839 | ] | #Hdis %{2} (* arith *) napply daemon ] |
---|
1840 | | cut (valid_access m1 chunk b1 ofs); /2/; #Hval' |
---|
1841 | lapply (Hnoover … eb1 Hb1 CP); |
---|
1842 | #Ha elim Ha; #Ha |
---|
1843 | [ elim Ha; #Ha |
---|
1844 | [ elim Ha; #Ha |
---|
1845 | [ %{1} %{1} /2/ |
---|
1846 | | elim Hval'; lapply (size_chunk_pos chunk); (* arith *) napply daemon ] |
---|
1847 | | elim Hval; lapply (size_chunk_pos chunk'); (* arith *) napply daemon ] |
---|
1848 | | elim Hval'; elim Hval; (* arith *) napply daemon ] |
---|
1849 | ] |
---|
1850 | | #eb1 #Hofs1 #Hofs2 #Hofs3 #H (* overlapping *) |
---|
1851 | <eb1 in CP #CP >CP in Hb1 #eb2d |
---|
1852 | elim (grumpydestruct2 ?????? eb2d); #eb2 #ed |
---|
1853 | cut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2'); |
---|
1854 | [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 // |
---|
1855 | | *;#v2' #LOAD2' |
---|
1856 | cut (v2' = Vundef); [ @(load_store_overlap … STORE2 … LOAD2') (* arith *) napply daemon | ] |
---|
1857 | #ev2' %{ v2'} % //; |
---|
1858 | >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H) |
---|
1859 | >ev2' |
---|
1860 | @val_inj_undef ] |
---|
1861 | | #eb1 #Hofs <Hofs in Hval LOAD1 ⊢ % #Hval #LOAD1 #Hsize #H (* overlapping *) |
---|
1862 | |
---|
1863 | <eb1 in CP #CP >CP in Hb1 #eb2d |
---|
1864 | elim (grumpydestruct2 ?????? eb2d); #eb2 #ed |
---|
1865 | cut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2'); |
---|
1866 | [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 // |
---|
1867 | | *;#v2' #LOAD2' |
---|
1868 | cut (v2' = Vundef); [ @(load_store_mismatch … STORE2 … LOAD2' ?) @sym_neq // | ] |
---|
1869 | #ev2' %{ v2'} % //; |
---|
1870 | >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H) |
---|
1871 | >ev2' |
---|
1872 | @val_inj_undef ] |
---|
1873 | ] |
---|
1874 | ] |
---|
1875 | ] qed. |
---|
1876 | |
---|
1877 | definition inj_offset_aligned ≝ λdelta: Z. λsize: Z. |
---|
1878 | ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta). |
---|
1879 | |
---|
1880 | lemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef. |
---|
1881 | ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta. |
---|
1882 | mem_inj val_inj mi m1 m2 → |
---|
1883 | alloc m1 lo1 hi1 = 〈m1', b1〉 → |
---|
1884 | alloc m2 lo2 hi2 = 〈m2', b2〉 → |
---|
1885 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1886 | lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 → |
---|
1887 | inj_offset_aligned delta (hi1 - lo1) → |
---|
1888 | mem_inj val_inj mi m1' m2'. |
---|
1889 | #val_inj #val_inj_undef |
---|
1890 | #mi #m1 #m2 #lo1 #hi1 #m1' #b1 #lo2 #hi2 #m2' #b2 #delta |
---|
1891 | #Hinj #ALLOC1 #ALLOC2 #Hbinj #Hlo #Hhi #Hal |
---|
1892 | whd; #chunk #b1' #ofs #v #b2' #delta' #Hbinj' #LOAD |
---|
1893 | lapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/; |
---|
1894 | *; |
---|
1895 | [ #A |
---|
1896 | cut (load chunk m1 b1' ofs = Some ? v); |
---|
1897 | [ <LOAD @sym_eq @(load_alloc_unchanged … ALLOC1) /2/; ] |
---|
1898 | #LOAD0 lapply (Hinj … Hbinj' LOAD0); *;#v2 *;#LOAD2 #VINJ |
---|
1899 | %{ v2} % |
---|
1900 | [ <LOAD2 @(load_alloc_unchanged … ALLOC2) |
---|
1901 | @valid_access_valid_block [ 3: @load_valid_access ] |
---|
1902 | // |
---|
1903 | | // |
---|
1904 | ] |
---|
1905 | | *;*;#A #B #C |
---|
1906 | >A in Hbinj' LOAD #Hbinj' #LOAD |
---|
1907 | >Hbinj in Hbinj' #Hbinj' elim (grumpydestruct2 ?????? Hbinj'); |
---|
1908 | #eb2 #edelta <eb2 <edelta |
---|
1909 | cut (v = Vundef); [ @(load_alloc_same … ALLOC1 … LOAD) ] |
---|
1910 | #ev >ev |
---|
1911 | cut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2); |
---|
1912 | [ @valid_access_load |
---|
1913 | @(valid_access_alloc_same … ALLOC2) |
---|
1914 | [ 1,2: (*arith*) @daemon |
---|
1915 | | (* arith using Hal *) napply daemon |
---|
1916 | ] ] |
---|
1917 | *;#v2 #LOAD2 |
---|
1918 | cut (v2 = Vundef); [ napply (load_alloc_same … ALLOC2 … LOAD2) ] |
---|
1919 | #ev2 >ev2 |
---|
1920 | %{ Vundef} % //; |
---|
1921 | ] qed. |
---|
1922 | |
---|
1923 | lemma alloc_right_inj: ∀val_inj. |
---|
1924 | ∀mi,m1,m2,lo,hi,b2,m2'. |
---|
1925 | mem_inj val_inj mi m1 m2 → |
---|
1926 | alloc m2 lo hi = 〈m2', b2〉 → |
---|
1927 | mem_inj val_inj mi m1 m2'. |
---|
1928 | #val_inj |
---|
1929 | #mi #m1 #m2 #lo #hi #b2 #m2' |
---|
1930 | #Hinj #ALLOC |
---|
1931 | whd; #chunk #b1 #ofs #v1 #b2' #delta #Hbinj #LOAD |
---|
1932 | lapply (Hinj … Hbinj LOAD); *; #v2 *;#LOAD2 #VINJ |
---|
1933 | %{ v2} % //; |
---|
1934 | cut (valid_block m2 b2'); |
---|
1935 | [ @(valid_access_valid_block ? chunk ? (ofs + delta)) /2/ ] |
---|
1936 | #Hval |
---|
1937 | <LOAD2 @(load_alloc_unchanged … ALLOC … Hval) |
---|
1938 | qed. |
---|
1939 | |
---|
1940 | (* |
---|
1941 | Hypothesis val_inj_undef_any: |
---|
1942 | ∀mi,v. val_inj mi Vundef v. |
---|
1943 | *) |
---|
1944 | |
---|
1945 | lemma alloc_left_unmapped_inj: ∀val_inj. |
---|
1946 | ∀mi,m1,m2,lo,hi,b1,m1'. |
---|
1947 | mem_inj val_inj mi m1 m2 → |
---|
1948 | alloc m1 lo hi = 〈m1', b1〉 → |
---|
1949 | mi b1 = None ? → |
---|
1950 | mem_inj val_inj mi m1' m2. |
---|
1951 | #val_inj |
---|
1952 | #mi #m1 #m2 #lo #hi #b1 #m1' |
---|
1953 | #Hinj #ALLOC #Hbinj |
---|
1954 | whd; #chunk #b1' #ofs #v1 #b2' #delta #Hbinj' #LOAD |
---|
1955 | lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/; |
---|
1956 | *; |
---|
1957 | [ #A |
---|
1958 | @(Hinj … Hbinj' ) |
---|
1959 | <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/; |
---|
1960 | | *;*;#A #B #C |
---|
1961 | >A in Hbinj' LOAD #Hbinj' #LOAD |
---|
1962 | >Hbinj in Hbinj' #bad destruct; |
---|
1963 | ] qed. |
---|
1964 | |
---|
1965 | lemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v. |
---|
1966 | ∀mi,m1,m2,lo,hi,b1,m1',b2,delta. |
---|
1967 | mem_inj val_inj mi m1 m2 → |
---|
1968 | alloc m1 lo hi = 〈m1', b1〉 → |
---|
1969 | mi b1 = Some ? 〈b2, delta〉 → |
---|
1970 | valid_block m2 b2 → |
---|
1971 | low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 → |
---|
1972 | inj_offset_aligned delta (hi - lo) → |
---|
1973 | mem_inj val_inj mi m1' m2. |
---|
1974 | #val_inj #val_inj_undef_any |
---|
1975 | #mi #m1 #m2 #lo #hi #b1 #m1' #b2 #delta |
---|
1976 | #Hinj #ALLOC #Hbinj #Hval #Hlo #Hhi #Hal |
---|
1977 | whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD |
---|
1978 | lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/; |
---|
1979 | *; |
---|
1980 | [ #A |
---|
1981 | @(Hinj … Hbinj') |
---|
1982 | <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/; |
---|
1983 | | *;*;#A #B *;#C #D |
---|
1984 | >A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj' |
---|
1985 | #Hbinj' (* XXX destruct normalizes too much here *) elim (grumpydestruct2 ?????? Hbinj'); #eb2 #edelta |
---|
1986 | <eb2 <edelta |
---|
1987 | cut (v1 = Vundef); [ napply (load_alloc_same … ALLOC … LOAD) ] |
---|
1988 | #ev1 >ev1 |
---|
1989 | cut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2); |
---|
1990 | [ @valid_access_load % //; |
---|
1991 | [ (* arith *) napply daemon |
---|
1992 | | (* arith *) napply daemon |
---|
1993 | | (* arith *) napply daemon |
---|
1994 | ] |
---|
1995 | ] |
---|
1996 | *;#v2 #LOAD2 %{ v2} % //; |
---|
1997 | ] qed. |
---|
1998 | |
---|
1999 | lemma free_parallel_inj: ∀val_inj. |
---|
2000 | ∀mi,m1,m2,b1,b2,delta. |
---|
2001 | mem_inj val_inj mi m1 m2 → |
---|
2002 | mi b1 = Some ? 〈b2, delta〉 → |
---|
2003 | (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) → |
---|
2004 | mem_inj val_inj mi (free m1 b1) (free m2 b2). |
---|
2005 | #val_inj |
---|
2006 | #mi #m1 #m2 #b1 #b2 #delta #Hinj #Hb1inj #Hbinj |
---|
2007 | whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD |
---|
2008 | lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B |
---|
2009 | cut (load chunk m1 b1' ofs = Some ? v1); |
---|
2010 | [ <LOAD @sym_eq @load_free @B ] #LOAD' |
---|
2011 | elim (Hinj … Hbinj' LOAD'); #v2 *;#LOAD2 #INJ |
---|
2012 | %{ v2} % |
---|
2013 | [ <LOAD2 @load_free |
---|
2014 | @nmk #e @(absurd ?? B) |
---|
2015 | >e in Hbinj' #Hbinj' @(Hbinj ?? Hbinj') |
---|
2016 | | // |
---|
2017 | ] qed. |
---|
2018 | |
---|
2019 | lemma free_left_inj: ∀val_inj. |
---|
2020 | ∀mi,m1,m2,b1. |
---|
2021 | mem_inj val_inj mi m1 m2 → |
---|
2022 | mem_inj val_inj mi (free m1 b1) m2. |
---|
2023 | #val_inj #mi #m1 #m2 #b1 #Hinj |
---|
2024 | whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD |
---|
2025 | lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B |
---|
2026 | @(Hinj … Hbinj') |
---|
2027 | <LOAD @sym_eq @load_free @B |
---|
2028 | qed. |
---|
2029 | |
---|
2030 | lemma free_list_left_inj: ∀val_inj. |
---|
2031 | ∀mi,bl,m1,m2. |
---|
2032 | mem_inj val_inj mi m1 m2 → |
---|
2033 | mem_inj val_inj mi (free_list m1 bl) m2. |
---|
2034 | #val_inj #mi #bl elim bl; |
---|
2035 | [ whd in ⊢ (?→?→?→???%?); // |
---|
2036 | | #h #t #IH #m1 #m2 #H >(unfold_free_list m1 h t) |
---|
2037 | @free_left_inj @IH // |
---|
2038 | ] qed. |
---|
2039 | |
---|
2040 | lemma free_right_inj: ∀val_inj. |
---|
2041 | ∀mi,m1,m2,b2. |
---|
2042 | mem_inj val_inj mi m1 m2 → |
---|
2043 | (∀b1,delta,chunk,ofs. |
---|
2044 | mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) → |
---|
2045 | mem_inj val_inj mi m1 (free m2 b2). |
---|
2046 | #val_inj #mi #m1 #m2 #b2 #Hinj #Hinval |
---|
2047 | whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD |
---|
2048 | cut (b2' ≠ b2); |
---|
2049 | [ @nmk #e >e in Hbinj' #Hbinj' |
---|
2050 | @(absurd ?? (Hinval … Hbinj')) @(load_valid_access … LOAD) ] |
---|
2051 | #ne lapply (Hinj … Hbinj' LOAD); *;#v2 *;#LOAD2 #INJ |
---|
2052 | %{ v2} % //; |
---|
2053 | <LOAD2 @load_free @ne |
---|
2054 | qed. |
---|
2055 | |
---|
2056 | lemma valid_pointer_inj: ∀val_inj. |
---|
2057 | ∀mi,m1,m2,b1,ofs,b2,delta. |
---|
2058 | mi b1 = Some ? 〈b2, delta〉 → |
---|
2059 | mem_inj val_inj mi m1 m2 → |
---|
2060 | valid_pointer m1 b1 ofs = true → |
---|
2061 | valid_pointer m2 b2 (ofs + delta) = true. |
---|
2062 | #val_inj #mi #m1 #m2 #b1 #ofs #b2 #delta #Hbinj #Hinj #VALID |
---|
2063 | lapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval |
---|
2064 | @(proj2 ?? (valid_pointer_valid_access ???)) |
---|
2065 | @(valid_access_inj … Hval) //; |
---|
2066 | qed. |
---|
2067 | |
---|
2068 | (* |
---|
2069 | End GENERIC_INJECT. |
---|
2070 | *) |
---|
2071 | (* ** Store extensions *) |
---|
2072 | |
---|
2073 | (* A store [m2] extends a store [m1] if [m2] can be obtained from [m1] |
---|
2074 | by increasing the sizes of the memory blocks of [m1] (decreasing |
---|
2075 | the low bounds, increasing the high bounds), while still keeping the |
---|
2076 | same contents for block offsets that are valid in [m1]. *) |
---|
2077 | |
---|
2078 | definition inject_id : meminj ≝ λb. Some ? 〈b, OZ〉. |
---|
2079 | |
---|
2080 | definition val_inj_id ≝ λmi: meminj. λv1,v2: val. v1 = v2. |
---|
2081 | |
---|
2082 | definition extends ≝ λm1,m2: mem. |
---|
2083 | nextblock m1 = nextblock m2 ∧ mem_inj val_inj_id inject_id m1 m2. |
---|
2084 | |
---|
2085 | theorem extends_refl: |
---|
2086 | ∀m: mem. extends m m. |
---|
2087 | #m % //; |
---|
2088 | whd; #chunk #b1 #ofs #v1 #b2 #delta normalize in ⊢ (%→?);#H |
---|
2089 | (* XXX: destruct makes the goal unreadable *) elim (grumpydestruct2 ?????? H); #eb1 #edelta #LOAD |
---|
2090 | %{ v1} % |
---|
2091 | [ <edelta >(Zplus_z_OZ ofs) //; |
---|
2092 | | // |
---|
2093 | ] qed. |
---|
2094 | |
---|
2095 | theorem alloc_extends: |
---|
2096 | ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block. |
---|
2097 | extends m1 m2 → |
---|
2098 | lo2 ≤ lo1 → hi1 ≤ hi2 → |
---|
2099 | alloc m1 lo1 hi1 = 〈m1', b1〉 → |
---|
2100 | alloc m2 lo2 hi2 = 〈m2', b2〉 → |
---|
2101 | b1 = b2 ∧ extends m1' m2'. |
---|
2102 | #m1 #m2 #m1' #m2' #lo1 #hi1 #lo2 #hi2 #b1 #b2 |
---|
2103 | *;#Hnext #Hinj #Hlo #Hhi #ALLOC1 #ALLOC2 |
---|
2104 | cut (b1 = b2); |
---|
2105 | [ @(transitive_eq … (nextblock m1)) [ @(alloc_result … ALLOC1) |
---|
2106 | | @sym_eq >Hnext napply (alloc_result … ALLOC2) ] ] |
---|
2107 | #eb <eb in ALLOC2 ⊢ % #ALLOC2 % //; % |
---|
2108 | [ >(nextblock_alloc … ALLOC1) |
---|
2109 | >(nextblock_alloc … ALLOC2) |
---|
2110 | //; |
---|
2111 | | @(alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????) |
---|
2112 | [ 1,4: normalize; //; |
---|
2113 | | 3,5,6: // |
---|
2114 | | 7: whd; #chunk #Hsize (* divides 0 *) napply daemon |
---|
2115 | ] |
---|
2116 | ] qed. |
---|
2117 | |
---|
2118 | theorem free_extends: |
---|
2119 | ∀m1,m2: mem. ∀b: block. |
---|
2120 | extends m1 m2 → |
---|
2121 | extends (free m1 b) (free m2 b). |
---|
2122 | #m1 #m2 #b *;#Hnext #Hinj % |
---|
2123 | [ normalize; //; |
---|
2124 | | @(free_parallel_inj … Hinj) |
---|
2125 | [ 2: //; |
---|
2126 | | 3: normalize; #b' #delta #ee destruct; // |
---|
2127 | ] |
---|
2128 | ] qed. |
---|
2129 | |
---|
2130 | theorem load_extends: |
---|
2131 | ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val. |
---|
2132 | extends m1 m2 → |
---|
2133 | load chunk m1 r b ofs = Some ? v → |
---|
2134 | load chunk m2 r b ofs = Some ? v. |
---|
2135 | #chunk #m1 #m2 #r #b #ofs #v |
---|
2136 | *;#Hnext #Hinj #LOAD |
---|
2137 | lapply (Hinj … LOAD); [ normalize; // | 2,3: ] |
---|
2138 | *;#v2 *; >(Zplus_z_OZ ofs) #LOAD2 #EQ whd in EQ; |
---|
2139 | //; |
---|
2140 | qed. |
---|
2141 | |
---|
2142 | theorem store_within_extends: |
---|
2143 | ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val. |
---|
2144 | extends m1 m2 → |
---|
2145 | store chunk m1 r b ofs v = Some ? m1' → |
---|
2146 | ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'. |
---|
2147 | #chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1 |
---|
2148 | lapply (store_mapped_inj … Hinj ?? STORE1 ?); |
---|
2149 | [ 1,2,7: normalize; // |
---|
2150 | | (* TODO: unfolding, etc ought to tidy this up *) |
---|
2151 | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb #Hinj1 #Hinj2 |
---|
2152 | normalize in Hinj1 Hinj2; %{1} %{1} %{1} destruct; // |
---|
2153 | | 4,5,6: ##skip |
---|
2154 | ] |
---|
2155 | *;#m2' *;#STORE #MINJ |
---|
2156 | %{ m2'} % >(Zplus_z_OZ ofs) in STORE #STORE //; |
---|
2157 | % |
---|
2158 | [ >(nextblock_store … STORE1) |
---|
2159 | >(nextblock_store … STORE) |
---|
2160 | // |
---|
2161 | | // |
---|
2162 | ] qed. |
---|
2163 | |
---|
2164 | theorem store_outside_extends: |
---|
2165 | ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val. |
---|
2166 | extends m1 m2 → |
---|
2167 | ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs → |
---|
2168 | store chunk m2 r b ofs v = Some ? m2' → |
---|
2169 | extends m1 m2'. |
---|
2170 | #chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE % |
---|
2171 | [ >(nextblock_store … STORE) // |
---|
2172 | | @(store_outside_inj … STORE) //; |
---|
2173 | #b' #delta #einj normalize in einj; destruct; |
---|
2174 | elim Houtside; |
---|
2175 | [ #lo %{ 2} >(Zplus_z_OZ ?) /2/ |
---|
2176 | | #hi %{ 1} >(Zplus_z_OZ ?) /2/ |
---|
2177 | ] |
---|
2178 | ] qed. |
---|
2179 | |
---|
2180 | theorem valid_pointer_extends: |
---|
2181 | ∀m1,m2,b,ofs. |
---|
2182 | extends m1 m2 → valid_pointer m1 r b ofs = true → |
---|
2183 | valid_pointer m2 r b ofs = true. |
---|
2184 | #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID |
---|
2185 | <(Zplus_z_OZ ofs) |
---|
2186 | @(valid_pointer_inj … Hinj VALID) //; |
---|
2187 | qed. |
---|
2188 | |
---|
2189 | |
---|
2190 | (* * The ``less defined than'' relation over memory states *) |
---|
2191 | |
---|
2192 | (* A memory state [m1] is less defined than [m2] if, for all addresses, |
---|
2193 | the value [v1] read in [m1] at this address is less defined than |
---|
2194 | the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *) |
---|
2195 | |
---|
2196 | definition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val. |
---|
2197 | Val_lessdef v1 v2. |
---|
2198 | |
---|
2199 | definition lessdef ≝ λm1,m2: mem. |
---|
2200 | nextblock m1 = nextblock m2 ∧ |
---|
2201 | mem_inj val_inj_lessdef inject_id m1 m2. |
---|
2202 | |
---|
2203 | lemma lessdef_refl: |
---|
2204 | ∀m. lessdef m m. |
---|
2205 | #m % //; |
---|
2206 | whd; #chunk #b1 #ofs #v1 #b2 #delta #H #LOAD |
---|
2207 | whd in H:(??%?); elim (grumpydestruct2 ?????? H); #eb1 #edelta |
---|
2208 | %{ v1} % //; |
---|
2209 | qed. |
---|
2210 | |
---|
2211 | lemma load_lessdef: |
---|
2212 | ∀m1,m2,chunk,b,ofs,v1. |
---|
2213 | lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 → |
---|
2214 | ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2. |
---|
2215 | #m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0 |
---|
2216 | lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); // | 2,3:##skip ] |
---|
2217 | *;#v2 *;#LOAD #INJ %{ v2} % //; |
---|
2218 | qed. |
---|
2219 | |
---|
2220 | lemma loadv_lessdef: |
---|
2221 | ∀m1,m2,chunk,addr1,addr2,v1. |
---|
2222 | lessdef m1 m2 → Val_lessdef addr1 addr2 → |
---|
2223 | loadv chunk m1 addr1 = Some ? v1 → |
---|
2224 | ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2. |
---|
2225 | #m1 #m2 #chunk #addr1 #addr2 #v1 #H #H0 #LOAD |
---|
2226 | inversion H0; |
---|
2227 | [ #v #e1 #e2 >e1 in LOAD cases v; |
---|
2228 | [ whd in ⊢ ((??%?)→?); #H' destruct; |
---|
2229 | | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct; |
---|
2230 | | #b' #off @load_lessdef // |
---|
2231 | ] |
---|
2232 | | #v #e >e in LOAD #LOAD whd in LOAD:(??%?); destruct; |
---|
2233 | ] qed. |
---|
2234 | |
---|
2235 | lemma store_lessdef: |
---|
2236 | ∀m1,m2,chunk,b,ofs,v1,v2,m1'. |
---|
2237 | lessdef m1 m2 → Val_lessdef v1 v2 → |
---|
2238 | store chunk m1 r b ofs v1 = Some ? m1' → |
---|
2239 | ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'. |
---|
2240 | #m1 #m2 #chunk #b #ofs #v1 #v2 #m1' |
---|
2241 | *;#Hnext #Hinj #Hvless #STORE0 |
---|
2242 | lapply (store_mapped_inj … Hinj … STORE0 ?); |
---|
2243 | [ #chunk' #Hsize whd;@load_result_lessdef napply Hvless |
---|
2244 | | whd in ⊢ (??%?); // |
---|
2245 | | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neq |
---|
2246 | whd in ⊢ ((??%?)→(??%?)→?); #e1 #e2 destruct; |
---|
2247 | % % % // |
---|
2248 | | 7: #mi whd; //; |
---|
2249 | | 8: *;#m2' *;#STORE #MINJ |
---|
2250 | %{ m2'} % /2/; |
---|
2251 | % |
---|
2252 | >(nextblock_store … STORE0) |
---|
2253 | >(nextblock_store … STORE) |
---|
2254 | //; |
---|
2255 | ] qed. |
---|
2256 | |
---|
2257 | lemma storev_lessdef: |
---|
2258 | ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'. |
---|
2259 | lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 → |
---|
2260 | storev chunk m1 addr1 v1 = Some ? m1' → |
---|
2261 | ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'. |
---|
2262 | #m1 #m2 #chunk #addr1 #v1 #addr2 #v2 #m1' |
---|
2263 | #Hmless #Haless #Hvless #STORE |
---|
2264 | inversion Haless; |
---|
2265 | [ #v #e1 #e2 >e1 in STORE cases v; |
---|
2266 | [ whd in ⊢ ((??%?)→?); #H' @False_ind destruct; |
---|
2267 | | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct; |
---|
2268 | | #b' #off @store_lessdef // |
---|
2269 | ] |
---|
2270 | | #v #e >e in STORE #STORE whd in STORE:(??%?); destruct |
---|
2271 | ] qed. |
---|
2272 | |
---|
2273 | lemma alloc_lessdef: |
---|
2274 | ∀m1,m2,lo,hi,b1,m1',b2,m2'. |
---|
2275 | lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 → |
---|
2276 | b1 = b2 ∧ lessdef m1' m2'. |
---|
2277 | #m1 #m2 #lo #hi #b1 #m1' #b2 #m2' |
---|
2278 | *;#Hnext #Hinj #ALLOC1 #ALLOC2 |
---|
2279 | cut (b1 = b2); |
---|
2280 | [ >(alloc_result … ALLOC1) >(alloc_result … ALLOC2) // |
---|
2281 | ] |
---|
2282 | #e <e in ALLOC2 ⊢ % #ALLOC2 % //; |
---|
2283 | % |
---|
2284 | [ >(nextblock_alloc … ALLOC1) |
---|
2285 | >(nextblock_alloc … ALLOC2) |
---|
2286 | // |
---|
2287 | | @(alloc_parallel_inj … Hinj ALLOC1 ALLOC2) |
---|
2288 | [ // |
---|
2289 | | 3: whd in ⊢ (??%?); // |
---|
2290 | | 4,5: //; |
---|
2291 | | 6: whd; #chunk #_ cases chunk;//; |
---|
2292 | ] qed. |
---|
2293 | |
---|
2294 | lemma free_lessdef: |
---|
2295 | ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b). |
---|
2296 | #m1 #m2 #b *;#Hnext #Hinj % |
---|
2297 | [ whd in ⊢ (??%%); // |
---|
2298 | | @(free_parallel_inj … Hinj) //; |
---|
2299 | #b' #delta #H whd in H:(??%?); elim (grumpydestruct2 ?????? H); // |
---|
2300 | ] qed. |
---|
2301 | |
---|
2302 | lemma free_left_lessdef: |
---|
2303 | ∀m1,m2,b. |
---|
2304 | lessdef m1 m2 → lessdef (free m1 b) m2. |
---|
2305 | #m1 #m2 #b *;#Hnext #Hinj % |
---|
2306 | <Hnext //; |
---|
2307 | @free_left_inj //; |
---|
2308 | qed. |
---|
2309 | |
---|
2310 | lemma free_right_lessdef: |
---|
2311 | ∀m1,m2,b. |
---|
2312 | lessdef m1 m2 → low_bound m1 b ≥ high_bound m1 b → |
---|
2313 | lessdef m1 (free m2 b). |
---|
2314 | #m1 #m2 #b *;#Hnext #Hinj #Hbounds |
---|
2315 | % >Hnext //; |
---|
2316 | @free_right_inj //; |
---|
2317 | #b1 #delta #chunk #ofs #H whd in H:(??%?); destruct; |
---|
2318 | @nmk *; #H1 #H2 #H3 #H4 |
---|
2319 | (* arith H2 and H3 contradict Hbounds. *) @daemon |
---|
2320 | qed. |
---|
2321 | |
---|
2322 | lemma valid_block_lessdef: |
---|
2323 | ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b. |
---|
2324 | #m1 #m2 #b *;#Hnext #Hinj |
---|
2325 | >(unfold_valid_block …) >(unfold_valid_block m2 b) |
---|
2326 | //; qed. |
---|
2327 | |
---|
2328 | lemma valid_pointer_lessdef: |
---|
2329 | ∀m1,m2,b,ofs. |
---|
2330 | lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. |
---|
2331 | #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID |
---|
2332 | <(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //; |
---|
2333 | qed. |
---|
2334 | |
---|
2335 | |
---|
2336 | (* ** Memory injections *) |
---|
2337 | |
---|
2338 | (* A memory injection [f] is a function from addresses to either [None] |
---|
2339 | or [Some] of an address and an offset. It defines a correspondence |
---|
2340 | between the blocks of two memory states [m1] and [m2]: |
---|
2341 | - if [f b = None], the block [b] of [m1] has no equivalent in [m2]; |
---|
2342 | - if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to |
---|
2343 | a sub-block at offset [ofs] of the block [b'] in [m2]. |
---|
2344 | *) |
---|
2345 | |
---|
2346 | (* A memory injection defines a relation between values that is the |
---|
2347 | identity relation, except for pointer values which are shifted |
---|
2348 | as prescribed by the memory injection. *) |
---|
2349 | |
---|
2350 | inductive val_inject (mi: meminj): val → val → Prop := |
---|
2351 | | val_inject_int: |
---|
2352 | ∀i. val_inject mi (Vint i) (Vint i) |
---|
2353 | | val_inject_float: |
---|
2354 | ∀f. val_inject mi (Vfloat f) (Vfloat f) |
---|
2355 | | val_inject_ptr: |
---|
2356 | ∀b1,ofs1,b2,ofs2,x. |
---|
2357 | mi b1 = Some ? 〈b2, x〉 → |
---|
2358 | ofs2 = add ofs1 (repr x) → |
---|
2359 | val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) |
---|
2360 | | val_inject_undef: ∀v. |
---|
2361 | val_inject mi Vundef v. |
---|
2362 | (* |
---|
2363 | Hint Resolve val_inject_int val_inject_float val_inject_ptr |
---|
2364 | val_inject_undef. |
---|
2365 | *) |
---|
2366 | inductive val_list_inject (mi: meminj): list val → list val→ Prop:= |
---|
2367 | | val_nil_inject : |
---|
2368 | val_list_inject mi (nil ?) (nil ?) |
---|
2369 | | val_cons_inject : ∀v,v',vl,vl'. |
---|
2370 | val_inject mi v v' → val_list_inject mi vl vl'→ |
---|
2371 | val_list_inject mi (v :: vl) (v' :: vl'). |
---|
2372 | (* |
---|
2373 | Hint Resolve val_nil_inject val_cons_inject. |
---|
2374 | *) |
---|
2375 | (* A memory state [m1] injects into another memory state [m2] via the |
---|
2376 | memory injection [f] if the following conditions hold: |
---|
2377 | - loads in [m1] must have matching loads in [m2] in the sense |
---|
2378 | of the [mem_inj] predicate; |
---|
2379 | - unallocated blocks in [m1] must be mapped to [None] by [f]; |
---|
2380 | - if [f b = Some〈b', delta〉], [b'] must be valid in [m2]; |
---|
2381 | - distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2]; |
---|
2382 | - the sizes of [m2]'s blocks are representable with signed machine integers; |
---|
2383 | - the offsets [delta] are representable with signed machine integers. |
---|
2384 | *) |
---|
2385 | |
---|
2386 | record mem_inject (f: meminj) (m1,m2: mem) : Prop ≝ |
---|
2387 | { |
---|
2388 | mi_inj: |
---|
2389 | mem_inj val_inject f m1 m2; |
---|
2390 | mi_freeblocks: |
---|
2391 | ∀b. ¬(valid_block m1 b) → f b = None ?; |
---|
2392 | mi_mappedblocks: |
---|
2393 | ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b'; |
---|
2394 | mi_no_overlap: |
---|
2395 | meminj_no_overlap f m1; |
---|
2396 | mi_range_1: |
---|
2397 | ∀b,b',delta. |
---|
2398 | f b = Some ? 〈b', delta〉 → |
---|
2399 | min_signed ≤ delta ∧ delta ≤ max_signed; |
---|
2400 | mi_range_2: |
---|
2401 | ∀b,b',delta. |
---|
2402 | f b = Some ? 〈b', delta〉 → |
---|
2403 | delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed) |
---|
2404 | }. |
---|
2405 | |
---|
2406 | |
---|
2407 | (* The following lemmas establish the absence of machine integer overflow |
---|
2408 | during address computations. *) |
---|
2409 | |
---|
2410 | lemma address_inject: |
---|
2411 | ∀f,m1,m2,chunk,b1,ofs1,b2,delta. |
---|
2412 | mem_inject f m1 m2 → |
---|
2413 | valid_access m1 chunk b1 (signed ofs1) → |
---|
2414 | f b1 = Some ? 〈b2, delta〉 → |
---|
2415 | signed (add ofs1 (repr delta)) = signed ofs1 + delta. |
---|
2416 | #f #m1 #m2 #chunk #b1 #ofs1 #b2 #delta |
---|
2417 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2418 | #Hvalid #Hb1inj |
---|
2419 | elim (mi_range_2 ??? Hb1inj); |
---|
2420 | [ (* delta = 0 *) |
---|
2421 | #edelta >edelta |
---|
2422 | >(?:repr O = zero) [ 2: // ] |
---|
2423 | >(add_zero ?) |
---|
2424 | >(Zplus_z_OZ …) |
---|
2425 | //; |
---|
2426 | | (* delta ≠ 0 *) |
---|
2427 | #Hrange >(add_signed ??) |
---|
2428 | >(signed_repr delta ?) |
---|
2429 | [ >(signed_repr ??) |
---|
2430 | [ // |
---|
2431 | | cut (valid_access m2 chunk b2 (signed ofs1 + delta)); |
---|
2432 | [ @(valid_access_inj … Hvalid) //; |
---|
2433 | | *; #_ #Hlo #Hhi #_ (* arith *) napply daemon |
---|
2434 | ] |
---|
2435 | ] |
---|
2436 | | /2/ |
---|
2437 | ] |
---|
2438 | ] qed. |
---|
2439 | |
---|
2440 | lemma valid_pointer_inject_no_overflow: |
---|
2441 | ∀f,m1,m2,b,ofs,b',x. |
---|
2442 | mem_inject f m1 m2 → |
---|
2443 | valid_pointer m1 b (signed ofs) = true → |
---|
2444 | f b = Some ? 〈b', x〉 → |
---|
2445 | min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed. |
---|
2446 | #f #m1 #m2 #b #ofs #b' #x |
---|
2447 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2448 | #Hvalid #Hb1inj |
---|
2449 | lapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid' |
---|
2450 | cut (valid_access m2 Mint8unsigned b' (signed ofs + x)); |
---|
2451 | [ @(valid_access_inj … Hvalid') // ] |
---|
2452 | *; >(?:size_chunk Mint8unsigned = 1) [ 2: // ] #_ #Hlo #Hhi #_ |
---|
2453 | >(signed_repr ??) [ 2: /2/; ] |
---|
2454 | lapply (mi_range_2 … Hb1inj); *; |
---|
2455 | [ #ex >ex >(Zplus_z_OZ ?) @signed_range |
---|
2456 | | (* arith *) napply daemon |
---|
2457 | ] qed. |
---|
2458 | |
---|
2459 | (* XXX: should use destruct, but reduces large definitions *) |
---|
2460 | lemma vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'. |
---|
2461 | #b #b' #i #i' #e destruct; /2/; qed. |
---|
2462 | |
---|
2463 | lemma valid_pointer_inject: |
---|
2464 | ∀f,m1,m2,b,ofs,b',ofs'. |
---|
2465 | mem_inject f m1 m2 → |
---|
2466 | valid_pointer m1 b (signed ofs) = true → |
---|
2467 | val_inject f (Vptr r b ofs) (Vptr b' ofs') → |
---|
2468 | valid_pointer m2 b' (signed ofs') = true. |
---|
2469 | #f #m1 #m2 #b #ofs #b' #ofs' |
---|
2470 | #Hinj #Hvalid #Hvinj inversion Hvinj; |
---|
2471 | [ 1,2,4: #x #H destruct; ] |
---|
2472 | #b0 #i #b0' #i' #delta #Hb #Hi' #eptr #eptr' |
---|
2473 | <(proj1 … (vptr_eq ???? eptr)) in Hb <(proj1 … (vptr_eq ???? eptr')) |
---|
2474 | <(proj2 … (vptr_eq ???? eptr)) in Hi' <(proj2 … (vptr_eq ???? eptr')) |
---|
2475 | #Hofs #Hbinj |
---|
2476 | >Hofs |
---|
2477 | lapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV |
---|
2478 | elim Hinj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2479 | >(add_signed ??) >(signed_repr ??) //; |
---|
2480 | >(signed_repr ??) /2/; |
---|
2481 | @(valid_pointer_inj … mi_inj Hvalid) //; |
---|
2482 | qed. |
---|
2483 | |
---|
2484 | lemma different_pointers_inject: |
---|
2485 | ∀f,m,m',b1,ofs1,b2,ofs2,b1',delta1,b2',delta2. |
---|
2486 | mem_inject f m m' → |
---|
2487 | b1 ≠ b2 → |
---|
2488 | valid_pointer m b1 (signed ofs1) = true → |
---|
2489 | valid_pointer m b2 (signed ofs2) = true → |
---|
2490 | f b1 = Some ? 〈b1', delta1〉 → |
---|
2491 | f b2 = Some ? 〈b2', delta2〉 → |
---|
2492 | b1' ≠ b2' ∨ |
---|
2493 | signed (add ofs1 (repr delta1)) ≠ |
---|
2494 | signed (add ofs2 (repr delta2)). |
---|
2495 | #f #m #m' #b1 #ofs1 #b2 #ofs2 #b1' #delta1 #b2' #delta2 |
---|
2496 | #Hinj #neb #Hval1 #Hval2 #Hf1 #Hf2 |
---|
2497 | lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1' |
---|
2498 | lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2' |
---|
2499 | >(address_inject … Hinj Hval1' Hf1) |
---|
2500 | >(address_inject … Hinj Hval2' Hf2) |
---|
2501 | elim Hval1'; #Hbval #Hlo #Hhi #Hal whd in Hhi:(?(??%)?); |
---|
2502 | elim Hval2'; #Hbval2 #Hlo2 #Hhi2 #Hal2 whd in Hhi2:(?(??%)?); |
---|
2503 | lapply (mi_no_overlap ??? Hinj … Hf1 Hf2 …); //; |
---|
2504 | *; [ |
---|
2505 | *; [ |
---|
2506 | *; [ /2/; |
---|
2507 | | (* arith contradiction *) napply daemon ] |
---|
2508 | | (* arith contradiction *) napply daemon ] |
---|
2509 | | *; [ #H %{2} (* arith *) napply daemon |
---|
2510 | | #H %{2} (* arith *) napply daemon ] ] |
---|
2511 | qed. |
---|
2512 | |
---|
2513 | (* Relation between injections and loads. *) |
---|
2514 | |
---|
2515 | lemma load_inject: |
---|
2516 | ∀f,m1,m2,chunk,b1,ofs,b2,delta,v1. |
---|
2517 | mem_inject f m1 m2 → |
---|
2518 | load chunk m1 b1 ofs = Some ? v1 → |
---|
2519 | f b1 = Some ? 〈b2, delta〉 → |
---|
2520 | ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inject f v1 v2. |
---|
2521 | #f #m1 #m2 #chunk #b1 #ofs #b2 #delta #v1 |
---|
2522 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2523 | #LOAD #Hbinj |
---|
2524 | @mi_inj //; |
---|
2525 | qed. |
---|
2526 | |
---|
2527 | lemma loadv_inject: |
---|
2528 | ∀f,m1,m2,chunk,a1,a2,v1. |
---|
2529 | mem_inject f m1 m2 → |
---|
2530 | loadv chunk m1 a1 = Some ? v1 → |
---|
2531 | val_inject f a1 a2 → |
---|
2532 | ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_inject f v1 v2. |
---|
2533 | #f #m1 #m2 #chunk #a1 #a2 #v1 |
---|
2534 | #Hinj #LOADV #Hvinj inversion Hvinj; |
---|
2535 | [ 1,2,4: #x #ex #ex' @False_ind destruct; ] |
---|
2536 | #b #ofs #b' #ofs' #delta #Hbinj #Hofs #ea1 #ea2 |
---|
2537 | >ea1 in LOADV #LOADV |
---|
2538 | lapply (load_inject … Hinj LOADV … Hbinj); *; #v2 *; #LOAD #INJ |
---|
2539 | %{ v2} % //; >Hofs |
---|
2540 | <(?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD |
---|
2541 | [ #H @H (* XXX: used to work with /2/ *) |
---|
2542 | | @(address_inject … chunk … Hinj ? Hbinj) @(load_valid_access …) |
---|
2543 | [ 2: @LOADV ] |
---|
2544 | ] qed. |
---|
2545 | |
---|
2546 | (* Relation between injections and stores. *) |
---|
2547 | |
---|
2548 | inductive val_content_inject (f: meminj): memory_chunk → val → val → Prop ≝ |
---|
2549 | | val_content_inject_base: |
---|
2550 | ∀chunk,v1,v2. |
---|
2551 | val_inject f v1 v2 → |
---|
2552 | val_content_inject f chunk v1 v2 |
---|
2553 | | val_content_inject_8: |
---|
2554 | ∀chunk,n1,n2. |
---|
2555 | chunk = Mint8unsigned ∨ chunk = Mint8signed → |
---|
2556 | zero_ext 8 n1 = zero_ext 8 n2 → |
---|
2557 | val_content_inject f chunk (Vint n1) (Vint n2) |
---|
2558 | | val_content_inject_16: |
---|
2559 | ∀chunk,n1,n2. |
---|
2560 | chunk = Mint16unsigned ∨ chunk = Mint16signed → |
---|
2561 | zero_ext 16 n1 = zero_ext 16 n2 → |
---|
2562 | val_content_inject f chunk (Vint n1) (Vint n2) |
---|
2563 | | val_content_inject_32: |
---|
2564 | ∀f1,f2. |
---|
2565 | singleoffloat f1 = singleoffloat f2 → |
---|
2566 | val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2). |
---|
2567 | |
---|
2568 | (*Hint Resolve val_content_inject_base.*) |
---|
2569 | |
---|
2570 | lemma load_result_inject: |
---|
2571 | ∀f,chunk,v1,v2,chunk'. |
---|
2572 | val_content_inject f chunk v1 v2 → |
---|
2573 | size_chunk chunk = size_chunk chunk' → |
---|
2574 | val_inject f (load_result chunk' v1) (load_result chunk' v2). |
---|
2575 | #f #chunk #v1 #v2 #chunk' |
---|
2576 | #Hvci inversion Hvci; |
---|
2577 | [ #chunk'' #v1' #v2' #Hvinj #_ #_ #_ #Hsize inversion Hvinj; |
---|
2578 | [ cases chunk'; #i #_ #_ [ 1,2,3,4,5: @ | 6,7: @4 ] |
---|
2579 | | cases chunk'; #f #_ #_ [ 1,2,3,4,5: @4 | 6,7: @2 ] |
---|
2580 | | cases chunk'; #b1 #ofs1 #b2 #ofs2 #delta #Hmap #Hofs #_ #_ [ 5: %{3} // | *: @4 ] |
---|
2581 | | cases chunk'; #v #_ #_ %{4} |
---|
2582 | ] |
---|
2583 | (* FIXME: the next two cases are very similar *) |
---|
2584 | | #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_ |
---|
2585 | elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; |
---|
2586 | [ 2,4: whd in ⊢ (??%%); >Hz @ |
---|
2587 | | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz) |
---|
2588 | % [ 1,3: @I | 2,4: @leb_true_to_le % ] |
---|
2589 | ] |
---|
2590 | | #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_ |
---|
2591 | elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; |
---|
2592 | [ 2,4: whd in ⊢ (??%%); >Hz @ |
---|
2593 | | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz) |
---|
2594 | % [ 1,3: @I | 2,4: @leb_true_to_le % ] |
---|
2595 | ] |
---|
2596 | |
---|
2597 | | #f #f' #float #echunk >echunk #_ #_ |
---|
2598 | elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct; |
---|
2599 | [ %{4} | >float @2 ] |
---|
2600 | ] qed. |
---|
2601 | |
---|
2602 | lemma store_mapped_inject_1 : |
---|
2603 | ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2. |
---|
2604 | mem_inject f m1 m2 → |
---|
2605 | store chunk m1 b1 ofs v1 = Some ? n1 → |
---|
2606 | f b1 = Some ? 〈b2, delta〉 → |
---|
2607 | val_content_inject f chunk v1 v2 → |
---|
2608 | ∃n2. |
---|
2609 | store chunk m2 b2 (ofs + delta) v2 = Some ? n2 |
---|
2610 | ∧ mem_inject f n1 n2. |
---|
2611 | #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2 |
---|
2612 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2613 | #STORE1 #INJb1 #Hvcinj |
---|
2614 | lapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //; |
---|
2615 | [ #chunk' #Hchunksize @(load_result_inject … chunk …) //; |
---|
2616 | | ##skip ] |
---|
2617 | *;#n2 *;#STORE #MINJ |
---|
2618 | %{ n2} % //; % |
---|
2619 | [ (* inj *) // |
---|
2620 | | (* freeblocks *) #b #notvalid @mi_freeblocks |
---|
2621 | @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE1) |
---|
2622 | | (* mappedblocks *) #b #b' #delta' #INJb' @(store_valid_block_1 … STORE) |
---|
2623 | /2/; |
---|
2624 | | (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb' |
---|
2625 | #fb1' #fb2' |
---|
2626 | >(low_bound_store … STORE1 ?) >(low_bound_store … STORE1 ?) |
---|
2627 | >(high_bound_store … STORE1 ?) >(high_bound_store … STORE1 ?) |
---|
2628 | @mi_no_overlap //; |
---|
2629 | | (* range *) /2/; |
---|
2630 | | (* range 2 *) #b #b' #delta' #INJb |
---|
2631 | >(low_bound_store … STORE ?) |
---|
2632 | >(high_bound_store … STORE ?) |
---|
2633 | @mi_range_2 //; |
---|
2634 | ] qed. |
---|
2635 | |
---|
2636 | lemma store_mapped_inject: |
---|
2637 | ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2. |
---|
2638 | mem_inject f m1 m2 → |
---|
2639 | store chunk m1 b1 ofs v1 = Some ? n1 → |
---|
2640 | f b1 = Some ? 〈b2, delta〉 → |
---|
2641 | val_inject f v1 v2 → |
---|
2642 | ∃n2. |
---|
2643 | store chunk m2 b2 (ofs + delta) v2 = Some ? n2 |
---|
2644 | ∧ mem_inject f n1 n2. |
---|
2645 | #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 #b2 #delta #v2 |
---|
2646 | #MINJ #STORE #INJb1 #Hvalinj @(store_mapped_inject_1 … STORE) //; |
---|
2647 | @val_content_inject_base //; |
---|
2648 | qed. |
---|
2649 | |
---|
2650 | lemma store_unmapped_inject: |
---|
2651 | ∀f,chunk,m1,b1,ofs,v1,n1,m2. |
---|
2652 | mem_inject f m1 m2 → |
---|
2653 | store chunk m1 b1 ofs v1 = Some ? n1 → |
---|
2654 | f b1 = None ? → |
---|
2655 | mem_inject f n1 m2. |
---|
2656 | #f #chunk #m1 #b1 #ofs #v1 #n1 #m2 |
---|
2657 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2658 | #STORE #INJb1 % |
---|
2659 | [ (* inj *) @(store_unmapped_inj … STORE) // |
---|
2660 | | (* freeblocks *) #b #notvalid @mi_freeblocks |
---|
2661 | @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE) |
---|
2662 | | (* mappedblocks *) #b #b' #delta #INJb @mi_mappedblock //; |
---|
2663 | | (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb' |
---|
2664 | #fb1' #fb2' |
---|
2665 | >(low_bound_store … STORE ?) >(low_bound_store … STORE ?) |
---|
2666 | >(high_bound_store … STORE ?) >(high_bound_store … STORE ?) |
---|
2667 | @mi_no_overlap //; |
---|
2668 | | (* range *) /2/ |
---|
2669 | | /2/ |
---|
2670 | ] qed. |
---|
2671 | |
---|
2672 | lemma storev_mapped_inject_1: |
---|
2673 | ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. |
---|
2674 | mem_inject f m1 m2 → |
---|
2675 | storev chunk m1 a1 v1 = Some ? n1 → |
---|
2676 | val_inject f a1 a2 → |
---|
2677 | val_content_inject f chunk v1 v2 → |
---|
2678 | ∃n2. |
---|
2679 | storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2. |
---|
2680 | #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 |
---|
2681 | #MINJ #STORE #Hvinj #Hvcinj |
---|
2682 | inversion Hvinj; |
---|
2683 | [ 1,2,4:#x #ex1 #ex2 >ex1 in STORE whd in ⊢ ((??%?)→?); #H |
---|
2684 | @False_ind destruct; ] |
---|
2685 | #b #ofs #b' #ofs' #delta #INJb #Hofs #ea1 #ea2 |
---|
2686 | >Hofs >ea1 in STORE #STORE |
---|
2687 | lapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj); |
---|
2688 | <(?:signed (add ofs (repr delta)) = signed ofs + delta) //; |
---|
2689 | @(address_inject … chunk … MINJ ? INJb) |
---|
2690 | @(store_valid_access_3 … STORE) |
---|
2691 | qed. |
---|
2692 | |
---|
2693 | lemma storev_mapped_inject: |
---|
2694 | ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. |
---|
2695 | mem_inject f m1 m2 → |
---|
2696 | storev chunk m1 a1 v1 = Some ? n1 → |
---|
2697 | val_inject f a1 a2 → |
---|
2698 | val_inject f v1 v2 → |
---|
2699 | ∃n2. |
---|
2700 | storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2. |
---|
2701 | #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 #MINJ #STOREV #Hvinj #Hvinj' |
---|
2702 | @(storev_mapped_inject_1 … STOREV) /2/; |
---|
2703 | qed. |
---|
2704 | |
---|
2705 | (* Relation between injections and [free] *) |
---|
2706 | |
---|
2707 | lemma meminj_no_overlap_free: |
---|
2708 | ∀mi,m,b. |
---|
2709 | meminj_no_overlap mi m → |
---|
2710 | meminj_no_overlap mi (free m b). |
---|
2711 | #mi #m #b #H whd;#b1 #b1' #delta1 #b2 #b2' #delta2 #Hne #mi1 #mi2 |
---|
2712 | cut (low_bound (free m b) b ≥ high_bound (free m b) b); |
---|
2713 | [ >(low_bound_free_same …) >(high_bound_free_same …) // ] |
---|
2714 | #Hbounds |
---|
2715 | cases (decidable_eq_Z b1 b);#e1 [ >e1 in Hne mi1 ⊢ % #Hne #mi1 ] |
---|
2716 | cases (decidable_eq_Z b2 b);#e2 [ 1,3: >e2 in Hne mi2 ⊢ % #Hne #mi2 ] |
---|
2717 | [ @False_ind elim Hne; /2/ |
---|
2718 | | % %{2} //; |
---|
2719 | | % % %{2} // |
---|
2720 | | >(low_bound_free …) //; >(low_bound_free …) //; |
---|
2721 | >(high_bound_free …) //; >(high_bound_free …) //; |
---|
2722 | /2/; |
---|
2723 | ] qed. |
---|
2724 | |
---|
2725 | lemma meminj_no_overlap_free_list: |
---|
2726 | ∀mi,m,bl. |
---|
2727 | meminj_no_overlap mi m → |
---|
2728 | meminj_no_overlap mi (free_list m bl). |
---|
2729 | #mi #m #bl elim bl; |
---|
2730 | [ #H whd in ⊢ (??%); // |
---|
2731 | | #h #t #IH #H @meminj_no_overlap_free @IH // |
---|
2732 | ] qed. |
---|
2733 | |
---|
2734 | lemma free_inject: |
---|
2735 | ∀f,m1,m2,l,b. |
---|
2736 | (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) → |
---|
2737 | mem_inject f m1 m2 → |
---|
2738 | mem_inject f (free_list m1 l) (free m2 b). |
---|
2739 | #f #m1 #m2 #l #b #mappedin |
---|
2740 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2741 | % |
---|
2742 | [ (* inj *) |
---|
2743 | @free_right_inj [ @free_list_left_inj //; ] |
---|
2744 | #b1 #delta #chunk #ofs #INJb1 @nmk #Hvalid |
---|
2745 | elim (valid_access_free_list_inv … Hvalid); #b1ni #Haccess |
---|
2746 | @(absurd ? (mappedin ?? INJb1) b1ni) |
---|
2747 | | (* freeblocks *) |
---|
2748 | #b' #notvalid @mi_freeblocks @(not_to_not ??? notvalid) |
---|
2749 | #H @valid_block_free_list_1 // |
---|
2750 | | (* mappedblocks *) |
---|
2751 | #b1 #b1' #delta #INJb1 @valid_block_free_1 /2/ |
---|
2752 | | (* overlap *) |
---|
2753 | @meminj_no_overlap_free_list // |
---|
2754 | | (* range *) |
---|
2755 | /2/ |
---|
2756 | | #b1 #b2 #delta #INJb1 cases (decidable_eq_Z b2 b); #eb |
---|
2757 | [ >eb |
---|
2758 | >(low_bound_free_same ??) >(high_bound_free_same ??) |
---|
2759 | %{2} (* arith *) napply daemon |
---|
2760 | | >(low_bound_free …) //; >(high_bound_free …) /2/; |
---|
2761 | ] |
---|
2762 | ] qed. |
---|
2763 | |
---|
2764 | (* Monotonicity properties of memory injections. *) |
---|
2765 | |
---|
2766 | definition inject_incr : meminj → meminj → Prop ≝ λf1,f2. |
---|
2767 | ∀b. f1 b = f2 b ∨ f1 b = None ?. |
---|
2768 | |
---|
2769 | lemma inject_incr_refl : |
---|
2770 | ∀f. inject_incr f f . |
---|
2771 | #f whd;#b % //; qed. |
---|
2772 | |
---|
2773 | lemma inject_incr_trans : |
---|
2774 | ∀f1,f2,f3. |
---|
2775 | inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 . |
---|
2776 | #f1 #f2 #f3 whd in ⊢ (%→%→%);#H1 #H2 #b |
---|
2777 | elim (H1 b); elim (H2 b); /2/; qed. |
---|
2778 | |
---|
2779 | lemma val_inject_incr: |
---|
2780 | ∀f1,f2,v,v'. |
---|
2781 | inject_incr f1 f2 → |
---|
2782 | val_inject f1 v v' → |
---|
2783 | val_inject f2 v v'. |
---|
2784 | #f1 #f2 #v #v' #Hincr #Hvinj |
---|
2785 | inversion Hvinj; |
---|
2786 | [ 1,2,4: #x #_ #_ //; |
---|
2787 | |#b #ofs #b' #ofs' #delta #INJb #Hofs #_ #_ |
---|
2788 | elim (Hincr b); #H |
---|
2789 | [ @(val_inject_ptr ??????? Hofs) /2/; |
---|
2790 | | @False_ind >INJb in H #H destruct; |
---|
2791 | ] qed. |
---|
2792 | |
---|
2793 | lemma val_list_inject_incr: |
---|
2794 | ∀f1,f2,vl,vl'. |
---|
2795 | inject_incr f1 f2 → val_list_inject f1 vl vl' → |
---|
2796 | val_list_inject f2 vl vl'. |
---|
2797 | #f1 #f2 #vl elim vl; |
---|
2798 | [ #vl' #Hincr #H inversion H; //; #v #v' #l #l0 #_ #_ #_ #H destruct; |
---|
2799 | | #h #t #IH #vl' #Hincr #H1 inversion H1; |
---|
2800 | [ #H destruct |
---|
2801 | | #h' #h'' #t' #t'' #Hinj1 #Hintt #_ #e1 #e2 destruct; |
---|
2802 | %{2} /2/; @IH //; @Hincr |
---|
2803 | ] |
---|
2804 | ] qed. |
---|
2805 | |
---|
2806 | (* |
---|
2807 | Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr. |
---|
2808 | *) |
---|
2809 | |
---|
2810 | (* Properties of injections and allocations. *) |
---|
2811 | |
---|
2812 | definition extend_inject ≝ |
---|
2813 | λb: block. λx: option (block × Z). λf: meminj. |
---|
2814 | λb': block. if eqZb b' b then x else f b'. |
---|
2815 | |
---|
2816 | lemma extend_inject_incr: |
---|
2817 | ∀f,b,x. |
---|
2818 | f b = None ? → |
---|
2819 | inject_incr f (extend_inject b x f). |
---|
2820 | #f #b #x #INJb whd;#b' whd in ⊢ (?(???%)?); |
---|
2821 | @(eqZb_elim b' b) #eb /2/; |
---|
2822 | qed. |
---|
2823 | |
---|
2824 | lemma alloc_right_inject: |
---|
2825 | ∀f,m1,m2,lo,hi,m2',b. |
---|
2826 | mem_inject f m1 m2 → |
---|
2827 | alloc m2 lo hi = 〈m2', b〉 → |
---|
2828 | mem_inject f m1 m2'. |
---|
2829 | #f #m1 #m2 #lo #hi #m2' #b |
---|
2830 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2831 | #ALLOC % |
---|
2832 | [ @(alloc_right_inj … ALLOC) //; |
---|
2833 | | /2/; |
---|
2834 | | #b1 #b2 #delta #INJb1 @(valid_block_alloc … ALLOC) /2/; |
---|
2835 | | //; |
---|
2836 | | /2/; |
---|
2837 | |#b1 #b2 #delta #INJb1 >(?:low_bound m2' b2 = low_bound m2 b2) |
---|
2838 | [ >(?:high_bound m2' b2 = high_bound m2 b2) /2/; |
---|
2839 | @high_bound_alloc_other /2/; |
---|
2840 | | @low_bound_alloc_other /2/ |
---|
2841 | ] |
---|
2842 | ] qed. |
---|
2843 | |
---|
2844 | lemma alloc_unmapped_inject: |
---|
2845 | ∀f,m1,m2,lo,hi,m1',b. |
---|
2846 | mem_inject f m1 m2 → |
---|
2847 | alloc m1 lo hi = 〈m1', b〉 → |
---|
2848 | mem_inject (extend_inject b (None ?) f) m1' m2 ∧ |
---|
2849 | inject_incr f (extend_inject b (None ?) f). |
---|
2850 | #f #m1 #m2 #lo #hi #m1' #b |
---|
2851 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2852 | #ALLOC |
---|
2853 | cut (inject_incr f (extend_inject b (None ?) f)); |
---|
2854 | [ @extend_inject_incr @mi_freeblocks /2/; ] |
---|
2855 | #Hinject_incr % //; % |
---|
2856 | [ (* inj *) |
---|
2857 | @(alloc_left_unmapped_inj … ALLOC) |
---|
2858 | [ 2: whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ] |
---|
2859 | whd; #chunk #b1 #ofs #v1 #b2 #delta |
---|
2860 | whd in ⊢ ((??%?)→?→?); @eqZb_elim #e whd in ⊢ ((??%?)→?→?); |
---|
2861 | #Hextend #LOAD |
---|
2862 | [ destruct; |
---|
2863 | | lapply (mi_inj … Hextend LOAD); *; #v2 *; #LOAD2 #VINJ |
---|
2864 | %{ v2} % //; |
---|
2865 | @val_inject_incr //; |
---|
2866 | ] |
---|
2867 | | (* freeblocks *) |
---|
2868 | #b' #Hinvalid whd in ⊢ (??%?); @(eqZb_elim b' b) //; |
---|
2869 | #neb @mi_freeblocks @(not_to_not ??? Hinvalid) |
---|
2870 | @valid_block_alloc //; |
---|
2871 | | (* mappedblocks *) |
---|
2872 | #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb |
---|
2873 | [ #H destruct; |
---|
2874 | | #H @(mi_mappedblock … H) |
---|
2875 | ] |
---|
2876 | | (* overlap *) |
---|
2877 | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?); |
---|
2878 | >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?) |
---|
2879 | >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) |
---|
2880 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2881 | [ destruct |
---|
2882 | | lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2 |
---|
2883 | [ destruct |
---|
2884 | | @mi_no_overlap /2/; |
---|
2885 | ] |
---|
2886 | ] |
---|
2887 | | (* range *) |
---|
2888 | #b1 #b2 #delta whd in ⊢ (??%?→?); |
---|
2889 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2890 | [ destruct |
---|
2891 | | @(mi_range_1 … INJb1) |
---|
2892 | ] |
---|
2893 | | #b1 #b2 #delta whd in ⊢ (??%?→?); |
---|
2894 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2895 | [ destruct |
---|
2896 | | @(mi_range_2 … INJb1) |
---|
2897 | ] |
---|
2898 | ] qed. |
---|
2899 | |
---|
2900 | lemma alloc_mapped_inject: |
---|
2901 | ∀f,m1,m2,lo,hi,m1',b,b',ofs. |
---|
2902 | mem_inject f m1 m2 → |
---|
2903 | alloc m1 lo hi = 〈m1', b〉 → |
---|
2904 | valid_block m2 b' → |
---|
2905 | min_signed ≤ ofs ∧ ofs ≤ max_signed → |
---|
2906 | min_signed ≤ low_bound m2 b' → |
---|
2907 | high_bound m2 b' ≤ max_signed → |
---|
2908 | low_bound m2 b' ≤ lo + ofs → |
---|
2909 | hi + ofs ≤ high_bound m2 b' → |
---|
2910 | inj_offset_aligned ofs (hi-lo) → |
---|
2911 | (∀b0,ofs0. |
---|
2912 | f b0 = Some ? 〈b', ofs0〉 → |
---|
2913 | high_bound m1 b0 + ofs0 ≤ lo + ofs ∨ |
---|
2914 | hi + ofs ≤ low_bound m1 b0 + ofs0) → |
---|
2915 | mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧ |
---|
2916 | inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f). |
---|
2917 | #f #m1 #m2 #lo #hi #m1' #b #b' #ofs |
---|
2918 | *;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
2919 | #ALLOC #validb' #rangeofs #rangelo #rangehi #boundlo #boundhi #injaligned #boundmapped |
---|
2920 | cut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f)); |
---|
2921 | [ @extend_inject_incr @mi_freeblocks /2/; ] |
---|
2922 | #Hincr % //; % |
---|
2923 | [ (* inj *) |
---|
2924 | @(alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi) /2/; |
---|
2925 | [ 2:whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ] |
---|
2926 | whd; #chunk #b1 #ofs' #v1 #b2 #delta #Hextend #LOAD |
---|
2927 | whd in Hextend:(??%?); >(eqZb_false b1 b ?) in Hextend |
---|
2928 | [ #Hextend lapply (mi_inj … Hextend LOAD); |
---|
2929 | *; #v2 *; #LOAD2 #VINJ |
---|
2930 | %{ v2} % //; |
---|
2931 | @val_inject_incr //; |
---|
2932 | | @(valid_not_valid_diff m1) /2/; |
---|
2933 | @(valid_access_valid_block … chunk … ofs') /2/; |
---|
2934 | ] |
---|
2935 | | (* freeblocks *) |
---|
2936 | #b' #Hinvalid whd in ⊢ (??%?); >(eqZb_false b' b ?) |
---|
2937 | [ @mi_freeblocks @(not_to_not ??? Hinvalid) |
---|
2938 | @valid_block_alloc //; |
---|
2939 | | @sym_neq @(valid_not_valid_diff m1') //; |
---|
2940 | @(valid_new_block … ALLOC) |
---|
2941 | ] |
---|
2942 | | (* mappedblocks *) |
---|
2943 | #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb #einj |
---|
2944 | [ destruct; //; |
---|
2945 | | @(mi_mappedblock … einj) |
---|
2946 | ] |
---|
2947 | | (* overlap *) |
---|
2948 | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?); |
---|
2949 | >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?) |
---|
2950 | >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?) |
---|
2951 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2952 | [ elim (grumpydestruct2 ?????? INJb1); #eb1' #eofs1 ] |
---|
2953 | lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2 |
---|
2954 | [ elim (grumpydestruct2 ?????? INJb2); #eb2' #eofs2 ] |
---|
2955 | [ @False_ind >e in neb1 >e2 /2/; |
---|
2956 | | elim (decidable_eq_Z b1' b2'); #e' |
---|
2957 | [ <e' in INJb2 ⊢ % <eb1' <eofs1 #INJb2 lapply (boundmapped … INJb2); |
---|
2958 | *; #H %{2} [ %{2 | @1 ] napply H} |
---|
2959 | | %{1} %{1} %{1} napply e' |
---|
2960 | ] |
---|
2961 | | elim (decidable_eq_Z b1' b2'); #e' |
---|
2962 | [ <e' in INJb2 ⊢ % #INJb2 elim (grumpydestruct2 ?????? INJb2); #eb' #eofs <eb' in INJb1 <eofs #INJb1 lapply (boundmapped … INJb1); |
---|
2963 | *; #H %{2} [ %{1} /2/ | %{2} @H ] |
---|
2964 | | %{1} %{1} %{1} napply e' |
---|
2965 | ] |
---|
2966 | | @mi_no_overlap /2/; |
---|
2967 | ] |
---|
2968 | | (* range *) |
---|
2969 | #b1 #b2 #delta whd in ⊢ (??%?→?); |
---|
2970 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2971 | [ destruct; /2/; |
---|
2972 | | @(mi_range_1 … INJb1) |
---|
2973 | ] |
---|
2974 | | #b1 #b2 #delta whd in ⊢ (??%?→?); |
---|
2975 | lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1 |
---|
2976 | [ destruct; %{2} % /2/; |
---|
2977 | | @(mi_range_2 … INJb1) |
---|
2978 | ] |
---|
2979 | ] qed. |
---|
2980 | |
---|
2981 | lemma alloc_parallel_inject: |
---|
2982 | ∀f,m1,m2,lo,hi,m1',m2',b1,b2. |
---|
2983 | mem_inject f m1 m2 → |
---|
2984 | alloc m1 lo hi = 〈m1', b1〉 → |
---|
2985 | alloc m2 lo hi = 〈m2', b2〉 → |
---|
2986 | min_signed ≤ lo → hi ≤ max_signed → |
---|
2987 | mem_inject (extend_inject b1 (Some ? 〈b2, OZ〉) f) m1' m2' ∧ |
---|
2988 | inject_incr f (extend_inject b1 (Some ? 〈b2, OZ〉) f). |
---|
2989 | #f #m1 #m2 #lo #hi #m1' #m2' #b1 #b2 |
---|
2990 | #Hminj #ALLOC1 #ALLOC2 #Hlo #Hhi |
---|
2991 | @(alloc_mapped_inject … ALLOC1) /2/; |
---|
2992 | [ @(alloc_right_inject … Hminj ALLOC2) |
---|
2993 | | >(low_bound_alloc_same … ALLOC2) // |
---|
2994 | | >(high_bound_alloc_same … ALLOC2) // |
---|
2995 | | >(low_bound_alloc_same … ALLOC2) // |
---|
2996 | | >(high_bound_alloc_same … ALLOC2) // |
---|
2997 | | whd; (* arith *) napply daemon |
---|
2998 | | #b #ofs #INJb0 @False_ind |
---|
2999 | elim Hminj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2 |
---|
3000 | lapply (mi_mappedblock … INJb0); |
---|
3001 | #H @(absurd ? H ?) /2/; |
---|
3002 | ] qed. |
---|
3003 | |
---|
3004 | definition meminj_init ≝ λm: mem. |
---|
3005 | λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?. |
---|
3006 | |
---|
3007 | definition mem_inject_neutral ≝ λm: mem. |
---|
3008 | ∀f,chunk,b,ofs,v. |
---|
3009 | load chunk m b ofs = Some ? v → val_inject f v v. |
---|
3010 | |
---|
3011 | lemma init_inject: |
---|
3012 | ∀m. |
---|
3013 | mem_inject_neutral m → |
---|
3014 | mem_inject (meminj_init m) m m. |
---|
3015 | #m #neutral % |
---|
3016 | [ (* inj *) |
---|
3017 | whd; #chunk #b1 #ofs #v1 #b2 #delta whd in ⊢ (??%?→?→?); |
---|
3018 | @Zltb_elim_Type0 #ltb1 [ |
---|
3019 | #H elim (grumpydestruct2 ?????? H); #eb1 #edelta |
---|
3020 | <eb1 <edelta #LOAD %{v1} % //; |
---|
3021 | @neutral //; |
---|
3022 | | #H whd in H:(??%?); destruct; |
---|
3023 | ] |
---|
3024 | | (* free blocks *) |
---|
3025 | #b >(unfold_valid_block …) whd in ⊢ (?→??%?); #notvalid |
---|
3026 | @Zltb_elim_Type0 #ltb1 |
---|
3027 | [ @False_ind napply (absurd ? ltb1 notvalid) |
---|
3028 | | // |
---|
3029 | ] |
---|
3030 | | (* mapped blocks *) |
---|
3031 | #b #b' #delta whd in ⊢ (??%?→?); >(unfold_valid_block …) |
---|
3032 | @Zltb_elim_Type0 #ltb |
---|
3033 | #H whd in H:(??%?); destruct; // |
---|
3034 | | (* overlap *) |
---|
3035 | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢(??%?→??%?→?); |
---|
3036 | @Zltb_elim_Type0 #ltb1 |
---|
3037 | [ #H whd in H:(??%?); destruct; |
---|
3038 | @Zltb_elim_Type0 #ltb2 |
---|
3039 | #H2 whd in H2:(??%?); destruct; % % % /2/; |
---|
3040 | | #H whd in H:(??%?); destruct; |
---|
3041 | ] |
---|
3042 | | (* range *) |
---|
3043 | #b #b' #delta whd in ⊢ (??%?→?); |
---|
3044 | @Zltb_elim_Type0 #ltb |
---|
3045 | [ #H elim (grumpydestruct2 ?????? H); #eb #edelta <edelta |
---|
3046 | (* FIXME: should be in integers.ma *) napply daemon |
---|
3047 | | #H whd in H:(??%?); destruct; |
---|
3048 | ] |
---|
3049 | | (* range *) |
---|
3050 | #b #b' #delta whd in ⊢ (??%?→?); |
---|
3051 | @Zltb_elim_Type0 #ltb |
---|
3052 | [ #H elim (grumpydestruct2 ?????? H); #eb #edelta <edelta |
---|
3053 | (* FIXME: should be in integers.ma *) napply daemon |
---|
3054 | | #H whd in H:(??%?); destruct; |
---|
3055 | ] |
---|
3056 | ] qed. |
---|
3057 | |
---|
3058 | lemma getN_setN_inject: |
---|
3059 | ∀f,m,v,n1,p1,n2,p2. |
---|
3060 | val_inject f (getN n2 p2 m) (getN n2 p2 m) → |
---|
3061 | val_inject f v v → |
---|
3062 | val_inject f (getN n2 p2 (setN n1 p1 v m)) |
---|
3063 | (getN n2 p2 (setN n1 p1 v m)). |
---|
3064 | #f #m #v #n1 #p1 #n2 #p2 #injget #injv |
---|
3065 | cases (getN_setN_characterization m v n1 p1 n2 p2);[ * ] #A |
---|
3066 | >A //; |
---|
3067 | qed. |
---|
3068 | |
---|
3069 | lemma getN_contents_init_data_inject: |
---|
3070 | ∀f,n,ofs,id,pos. |
---|
3071 | val_inject f (getN n ofs (contents_init_data pos id)) |
---|
3072 | (getN n ofs (contents_init_data pos id)). |
---|
3073 | #f #n #ofs #id elim id; |
---|
3074 | [ #pos >(getN_init …) // |
---|
3075 | | #h #t #IH #pos cases h; |
---|
3076 | [ 1,2,3,4,5: #x @getN_setN_inject // |
---|
3077 | | 6,8: #x @IH | #x #y napply IH ] (* XXX // doesn't work? *) |
---|
3078 | qed. |
---|
3079 | |
---|
3080 | lemma alloc_init_data_neutral: |
---|
3081 | ∀m,id,m',b. |
---|
3082 | mem_inject_neutral m → |
---|
3083 | alloc_init_data m id = 〈m', b〉 → |
---|
3084 | mem_inject_neutral m'. |
---|
3085 | #m #id #m' #b #Hneutral #INIT whd in INIT:(??%?); (* XXX: destruct makes a bit of a mess *) |
---|
3086 | @(pairdisc_elim … INIT) |
---|
3087 | whd in ⊢ (??%% → ?);#B <B in ⊢ (??%% → ?) |
---|
3088 | whd in ⊢ (??%% → ?);#A |
---|
3089 | whd; #f #chunk #b' #ofs #v #LOAD |
---|
3090 | lapply (load_inv … LOAD); *; #C #D |
---|
3091 | <B in D >A |
---|
3092 | >(unfold_update block_contents …) @eqZb_elim |
---|
3093 | [ #eb' #D whd in D:(???(??(???%))); >D |
---|
3094 | @(load_result_inject … chunk) //; % |
---|
3095 | @getN_contents_init_data_inject |
---|
3096 | | #neb' #D @(Hneutral ? chunk b' ofs ??) whd in ⊢ (??%?); |
---|
3097 | >(in_bounds_true m chunk b' ofs (option ?) …) |
---|
3098 | [ <D // |
---|
3099 | | elim C; #Cval #Clo #Chi #Cal % |
---|
3100 | [ >(unfold_valid_block …) |
---|
3101 | >(unfold_valid_block …) in Cval <B |
---|
3102 | (* arith using neb' *) napply daemon |
---|
3103 | | >(?:low_bound m b' = low_bound m' b') //; |
---|
3104 | whd in ⊢ (??%%); <B >A |
---|
3105 | >(update_o block_contents …) //; @sym_neq //; |
---|
3106 | | >(?:high_bound m b' = high_bound m' b') //; |
---|
3107 | whd in ⊢ (??%%); <B >A |
---|
3108 | >(update_o block_contents …) //; @sym_neq //; |
---|
3109 | | //; |
---|
3110 | ] |
---|
3111 | ] qed. |
---|
3112 | |
---|
3113 | |
---|
3114 | (* ** Memory shifting *) |
---|
3115 | |
---|
3116 | (* A special case of memory injection where blocks are not coalesced: |
---|
3117 | each source block injects in a distinct target block. *) |
---|
3118 | |
---|
3119 | definition memshift ≝ block → option Z. |
---|
3120 | |
---|
3121 | definition meminj_of_shift : memshift → meminj ≝ λmi: memshift. |
---|
3122 | λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ]. |
---|
3123 | |
---|
3124 | definition val_shift ≝ λmi: memshift. λv1,v2: val. |
---|
3125 | val_inject (meminj_of_shift mi) v1 v2. |
---|
3126 | |
---|
3127 | record mem_shift (f: memshift) (m1,m2: mem) : Prop := |
---|
3128 | { |
---|
3129 | ms_inj: |
---|
3130 | mem_inj val_inject (meminj_of_shift f) m1 m2; |
---|
3131 | ms_samedomain: |
---|
3132 | nextblock m1 = nextblock m2; |
---|
3133 | ms_domain: |
---|
3134 | ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ]; |
---|
3135 | ms_range_1: |
---|
3136 | ∀b,delta. |
---|
3137 | f b = Some ? delta → |
---|
3138 | min_signed ≤ delta ∧ delta ≤ max_signed; |
---|
3139 | ms_range_2: |
---|
3140 | ∀b,delta. |
---|
3141 | f b = Some ? delta → |
---|
3142 | min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed |
---|
3143 | }. |
---|
3144 | |
---|
3145 | (* * The following lemmas establish the absence of machine integer overflow |
---|
3146 | during address computations. *) |
---|
3147 | |
---|
3148 | lemma address_shift: |
---|
3149 | ∀f,m1,m2,chunk,b,ofs1,delta. |
---|
3150 | mem_shift f m1 m2 → |
---|
3151 | valid_access m1 chunk b (signed ofs1) → |
---|
3152 | f b = Some ? delta → |
---|
3153 | signed (add ofs1 (repr delta)) = signed ofs1 + delta. |
---|
3154 | #f #m1 #m2 #chunk #b #ofs1 #delta |
---|
3155 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 #Hvalid_access #INJb |
---|
3156 | elim (ms_range_2 … INJb); #Hlo #Hhi |
---|
3157 | >(add_signed …) |
---|
3158 | >(signed_repr …) >(signed_repr …) /2/; |
---|
3159 | cut (valid_access m2 chunk b (signed ofs1 + delta)); |
---|
3160 | [ @(valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access) |
---|
3161 | whd in ⊢ (??%?); >INJb // ] |
---|
3162 | *; (* arith *) @daemon |
---|
3163 | qed. |
---|
3164 | |
---|
3165 | lemma valid_pointer_shift_no_overflow: |
---|
3166 | ∀f,m1,m2,b,ofs,x. |
---|
3167 | mem_shift f m1 m2 → |
---|
3168 | valid_pointer m1 b (signed ofs) = true → |
---|
3169 | f b = Some ? x → |
---|
3170 | min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed. |
---|
3171 | #f #m1 #m2 #b #ofs #x |
---|
3172 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3173 | #VALID #INJb |
---|
3174 | lapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access |
---|
3175 | cut (valid_access m2 Mint8unsigned b (signed ofs + x)); |
---|
3176 | [ @(valid_access_inj … ms_inj Hvalid_access) |
---|
3177 | whd in ⊢ (??%?); >INJb // ] |
---|
3178 | *;#Hvalid_block #Hlo #Hhi #Hal whd in Hhi:(?(??%)?); |
---|
3179 | >(signed_repr …) /2/; |
---|
3180 | lapply (ms_range_2 … INJb);*;#A #B |
---|
3181 | (* arith *) @daemon |
---|
3182 | qed. |
---|
3183 | |
---|
3184 | (* FIXME to get around destruct problems *) |
---|
3185 | lemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'. |
---|
3186 | #b #b' #ofs #ofs' #H destruct;//; |
---|
3187 | qed. |
---|
3188 | lemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'. |
---|
3189 | #b #b' #ofs #ofs' #H destruct;//; |
---|
3190 | qed. |
---|
3191 | |
---|
3192 | lemma valid_pointer_shift: |
---|
3193 | ∀f,m1,m2,b,ofs,b',ofs'. |
---|
3194 | mem_shift f m1 m2 → |
---|
3195 | valid_pointer m1 b (signed ofs) = true → |
---|
3196 | val_shift f (Vptr b ofs) (Vptr b' ofs') → |
---|
3197 | valid_pointer m2 b' (signed ofs') = true. |
---|
3198 | #f #m1 #m2 #b #ofs #b' #ofs' #Hmem_shift #VALID #Hval_shift |
---|
3199 | whd in Hval_shift; inversion Hval_shift; |
---|
3200 | [ 1,2,4: #a #H destruct; ] |
---|
3201 | #b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #eb1 #eb2 |
---|
3202 | <(vptr_eq_1 … eb1) in INJb1 <(vptr_eq_1 … eb2) #INJb' |
---|
3203 | <(vptr_eq_2 … eb1) in Hofs <(vptr_eq_2 … eb2) #Hofs >Hofs |
---|
3204 | cut (f b = Some ? delta); |
---|
3205 | [ whd in INJb':(??%?); cases (f b) in INJb' ⊢ %; |
---|
3206 | [ #H @(False_ind … (grumpydestruct … H)) | #delta' #H elim (grumpydestruct2 ?????? H); // ] |
---|
3207 | ] #INJb |
---|
3208 | lapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV |
---|
3209 | elim Hmem_shift;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3210 | >(add_signed …) >(signed_repr …) //; |
---|
3211 | >(signed_repr …) /2/; |
---|
3212 | @(valid_pointer_inj … VALID) /2/; |
---|
3213 | qed. |
---|
3214 | |
---|
3215 | (* Relation between shifts and loads. *) |
---|
3216 | |
---|
3217 | lemma load_shift: |
---|
3218 | ∀f,m1,m2,chunk,b,ofs,delta,v1. |
---|
3219 | mem_shift f m1 m2 → |
---|
3220 | load chunk m1 b ofs = Some ? v1 → |
---|
3221 | f b = Some ? delta → |
---|
3222 | ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2. |
---|
3223 | #f #m1 #m2 #chunk #b #ofs #delta #v1 |
---|
3224 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3225 | #LOAD #INJb |
---|
3226 | whd in ⊢ (??(λ_.??%)); @(ms_inj … LOAD) |
---|
3227 | whd in ⊢ (??%?); >INJb //; |
---|
3228 | qed. |
---|
3229 | |
---|
3230 | lemma loadv_shift: |
---|
3231 | ∀f,m1,m2,chunk,a1,a2,v1. |
---|
3232 | mem_shift f m1 m2 → |
---|
3233 | loadv chunk m1 a1 = Some ? v1 → |
---|
3234 | val_shift f a1 a2 → |
---|
3235 | ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2. |
---|
3236 | #f #m1 #m2 #chunk #a1 #a2 #v1 #Hmem_shift #LOADV #Hval_shift |
---|
3237 | inversion Hval_shift; |
---|
3238 | [ 1,2,4: #x #H >H in LOADV #H' whd in H':(??%?);@False_ind destruct; ] |
---|
3239 | #b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #ea1 #ea2 >ea1 in LOADV #LOADV |
---|
3240 | lapply INJb1; whd in ⊢ (??%? → ?); |
---|
3241 | lapply (refl ? (f b1)); cases (f b1) in ⊢ (???% → %); |
---|
3242 | [ #_ whd in ⊢ (??%? → ?); #H @False_ind @(False_ind … (grumpydestruct … H)) |
---|
3243 | | #delta' #DELTA whd in ⊢ (??%? → ?); #H elim (grumpydestruct2 ?????? H); |
---|
3244 | #eb #edelta |
---|
3245 | ] lapply (load_shift … Hmem_shift LOADV DELTA); *; #v2 *;#LOAD #INJ |
---|
3246 | %{ v2} % //; >Hofs >eb in LOAD >edelta |
---|
3247 | <(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta) |
---|
3248 | [#H' @H' (* XXX // doesn't work *) |
---|
3249 | | <edelta @(address_shift … chunk … Hmem_shift … DELTA) |
---|
3250 | @(load_valid_access … LOADV) |
---|
3251 | ] |
---|
3252 | qed. |
---|
3253 | |
---|
3254 | (* Relation between shifts and stores. *) |
---|
3255 | |
---|
3256 | lemma store_within_shift: |
---|
3257 | ∀f,chunk,m1,b,ofs,v1,n1,m2,delta,v2. |
---|
3258 | mem_shift f m1 m2 → |
---|
3259 | store chunk m1 b ofs v1 = Some ? n1 → |
---|
3260 | f b = Some ? delta → |
---|
3261 | val_shift f v1 v2 → |
---|
3262 | ∃n2. |
---|
3263 | store chunk m2 b (ofs + delta) v2 = Some ? n2 |
---|
3264 | ∧ mem_shift f n1 n2. |
---|
3265 | #f #chunk #m1 #b #ofs #v1 #n1 #m2 #delta #v2 |
---|
3266 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3267 | #STORE1 #INJb #Hval_shift |
---|
3268 | lapply (store_mapped_inj … ms_inj ?? STORE1 ?); |
---|
3269 | [ #chunk' #echunk @(load_result_inject … chunk) /2/; |
---|
3270 | | whd in ⊢ (??%?); >INJb (* XXX: // has stopped working *) napply refl |
---|
3271 | | whd; #b1 #b1' #delta1 #b2 #b2' #delta2 |
---|
3272 | whd in ⊢ (? → ??%? → ??%? → ?); |
---|
3273 | elim (f b1); elim (f b2); |
---|
3274 | [#_ #e1 whd in e1:(??%?);destruct; |
---|
3275 | |#z #_ #e1 whd in e1:(??%?);destruct; |
---|
3276 | |#z #_ #_ #e2 whd in e2:(??%?);destruct; |
---|
3277 | |#delta1' #delta2' #neb #e1 #e2 |
---|
3278 | whd in e1:(??%?) e2:(??%?); |
---|
3279 | destruct; |
---|
3280 | %{1} %{1} %{1} //; |
---|
3281 | ] |
---|
3282 | | 7: //; |
---|
3283 | | 4,5,6: ##skip |
---|
3284 | ] |
---|
3285 | *;#n2 *;#STORE #MINJ |
---|
3286 | %{ n2} % //; % |
---|
3287 | [ (* inj *) // |
---|
3288 | | (* samedomain *) |
---|
3289 | >(nextblock_store … STORE1) |
---|
3290 | >(nextblock_store … STORE) |
---|
3291 | //; |
---|
3292 | | (* domain *) |
---|
3293 | >(nextblock_store … STORE1) |
---|
3294 | // |
---|
3295 | | (* range *) |
---|
3296 | /2/ |
---|
3297 | | #b1 #delta1 #INJb1 |
---|
3298 | >(low_bound_store … STORE b1) |
---|
3299 | >(high_bound_store … STORE b1) |
---|
3300 | @ms_range_2 //; |
---|
3301 | ] qed. |
---|
3302 | |
---|
3303 | lemma store_outside_shift: |
---|
3304 | ∀f,chunk,m1,b,ofs,m2,v,m2',delta. |
---|
3305 | mem_shift f m1 m2 → |
---|
3306 | f b = Some ? delta → |
---|
3307 | high_bound m1 b + delta ≤ ofs |
---|
3308 | ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta → |
---|
3309 | store chunk m2 b ofs v = Some ? m2' → |
---|
3310 | mem_shift f m1 m2'. |
---|
3311 | #f #chunk #m1 #b #ofs #m2 #v #m2' #delta |
---|
3312 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3313 | #INJb #Hbounds #STORE % |
---|
3314 | [ (* inj *) |
---|
3315 | @(store_outside_inj … STORE) //; |
---|
3316 | #b' #d' whd in ⊢ (??%? → ?); lapply (refl ? (f b')); elim (f b') in ⊢ (???% → %); |
---|
3317 | [ #_ #e whd in e:(??%?); destruct; |
---|
3318 | | #d'' #ef #e elim (grumpydestruct2 ?????? e); #eb #ed |
---|
3319 | >eb in ef ⊢ % >ed >INJb #ed' |
---|
3320 | <(grumpydestruct1 ??? ed') // |
---|
3321 | ] |
---|
3322 | | (* samedomain *) >(nextblock_store … STORE) // |
---|
3323 | | (* domain *) // |
---|
3324 | | (* range *) /2/ |
---|
3325 | | #b1 #delta1 #INJb1 |
---|
3326 | >(low_bound_store … STORE b1) |
---|
3327 | >(high_bound_store … STORE b1) |
---|
3328 | @ms_range_2 //; |
---|
3329 | ] qed. |
---|
3330 | |
---|
3331 | lemma storev_shift: |
---|
3332 | ∀f,chunk,m1,a1,v1,n1,m2,a2,v2. |
---|
3333 | mem_shift f m1 m2 → |
---|
3334 | storev chunk m1 a1 v1 = Some ? n1 → |
---|
3335 | val_shift f a1 a2 → |
---|
3336 | val_shift f v1 v2 → |
---|
3337 | ∃n2. |
---|
3338 | storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2. |
---|
3339 | #f #chunk #m1 #a1 #v1 #n1 #m2 #a2 #v2 |
---|
3340 | #Hmem_shift #STOREV #Hval_shift_a #Hval_shift_v |
---|
3341 | inversion Hval_shift_a; |
---|
3342 | [ 1,2,4: #x #H >H in STOREV #H' whd in H':(??%?); @False_ind destruct; ] |
---|
3343 | #b1 #ofs1 #b2 #ofs2 #delta |
---|
3344 | whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %); |
---|
3345 | [#_ #e whd in e:(??%?); destruct; ] |
---|
3346 | #x #INJb1 #e elim (grumpydestruct2 ?????? e); #eb #ex |
---|
3347 | >ex in INJb1 #INJb1 |
---|
3348 | #OFS #ea1 #ea2 >ea1 in STOREV #STOREV |
---|
3349 | lapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v); |
---|
3350 | *; #n2 *; #A #B |
---|
3351 | %{ n2} % //; |
---|
3352 | >OFS >eb in A |
---|
3353 | <(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta) |
---|
3354 | [ #H @H (* XXX /2/ *) |
---|
3355 | | @(address_shift … chunk … Hmem_shift ? INJb1) |
---|
3356 | @(store_valid_access_3 … STOREV) |
---|
3357 | ] |
---|
3358 | qed. |
---|
3359 | |
---|
3360 | (* Relation between shifts and [free]. *) |
---|
3361 | |
---|
3362 | lemma free_shift: |
---|
3363 | ∀f,m1,m2,b. |
---|
3364 | mem_shift f m1 m2 → |
---|
3365 | mem_shift f (free m1 b) (free m2 b). |
---|
3366 | #f #m1 #m2 #b |
---|
3367 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 % |
---|
3368 | [ (* inj *) |
---|
3369 | @free_right_inj [ @free_left_inj // |
---|
3370 | | #b1 #delta #chunk #ofs whd in ⊢ (??%? → ?); |
---|
3371 | lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %); |
---|
3372 | [ #_ #e whd in e:(??%?); destruct; |
---|
3373 | | #delta' #INJb1 #e whd in e:(??%?); destruct; |
---|
3374 | napply valid_access_free_2 |
---|
3375 | ] |
---|
3376 | ] |
---|
3377 | | (* samedomain *) whd in ⊢ (??%%); // |
---|
3378 | | (* domain *) >(?:nextblock (free m1 b) = nextblock m1) // |
---|
3379 | | (* range *) /2/ |
---|
3380 | | #b' #delta #INJb' cases (decidable_eq_Z b' b); #eb |
---|
3381 | [ >eb |
---|
3382 | >(low_bound_free_same ??) >(high_bound_free_same ??) |
---|
3383 | (* arith *) napply daemon |
---|
3384 | | >(low_bound_free …) //; >(high_bound_free …) /2/; |
---|
3385 | ] |
---|
3386 | ] qed. |
---|
3387 | |
---|
3388 | (* Relation between shifts and allocation. *) |
---|
3389 | |
---|
3390 | definition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift. |
---|
3391 | ∀b. f1 b = f2 b ∨ f1 b = None ?. |
---|
3392 | |
---|
3393 | lemma shift_incr_inject_incr: |
---|
3394 | ∀f1,f2. |
---|
3395 | shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2). |
---|
3396 | #f1 #f2 #Hshift whd in ⊢ (?%%); whd; #b |
---|
3397 | elim (Hshift b); #INJ >INJ /2/; |
---|
3398 | qed. |
---|
3399 | |
---|
3400 | lemma val_shift_incr: |
---|
3401 | ∀f1,f2,v1,v2. |
---|
3402 | shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2. |
---|
3403 | #f1 #f2 #v1 #v2 #Hshift_incr whd in ⊢ (% → %); |
---|
3404 | @val_inject_incr |
---|
3405 | @shift_incr_inject_incr //; |
---|
3406 | qed. |
---|
3407 | |
---|
3408 | (* * |
---|
3409 | Remark mem_inj_incr: |
---|
3410 | ∀f1,f2,m1,m2. |
---|
3411 | inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2. |
---|
3412 | Proof. |
---|
3413 | intros; red; intros. |
---|
3414 | destruct (H b1). rewrite <- H3 in H1. |
---|
3415 | exploit H0; eauto. intros [v2 [A B]]. |
---|
3416 | exists v2; split. auto. apply val_inject_incr with f1; auto. |
---|
3417 | congruence. |
---|
3418 | ***) |
---|
3419 | |
---|
3420 | lemma alloc_shift: |
---|
3421 | ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2. |
---|
3422 | mem_shift f m1 m2 → |
---|
3423 | alloc m1 lo1 hi1 = 〈m1', b〉 → |
---|
3424 | lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 → |
---|
3425 | min_signed ≤ delta ∧ delta ≤ max_signed → |
---|
3426 | min_signed ≤ lo2 → hi2 ≤ max_signed → |
---|
3427 | inj_offset_aligned delta (hi1-lo1) → |
---|
3428 | ∃f'. ∃m2'. |
---|
3429 | alloc m2 lo2 hi2 = 〈m2', b〉 |
---|
3430 | ∧ mem_shift f' m1' m2' |
---|
3431 | ∧ shift_incr f f' |
---|
3432 | ∧ f' b = Some ? delta. |
---|
3433 | #f #m1 #m2 #lo1 #hi1 #m1' #b #delta #lo2 #hi2 |
---|
3434 | *;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2 |
---|
3435 | #ALLOC #Hlo_delta #Hhi_delta #Hdelta_range #Hlo_range #Hhi_range #Hinj_aligned |
---|
3436 | lapply (refl ? (alloc m2 lo2 hi2)); elim (alloc m2 lo2 hi2) in ⊢ (???% → %); |
---|
3437 | #m2' #b' #ALLOC2 |
---|
3438 | cut (b' = b); |
---|
3439 | [ >(alloc_result … ALLOC) >(alloc_result … ALLOC2) // ] |
---|
3440 | #eb >eb |
---|
3441 | cut (f b = None ?); |
---|
3442 | [ lapply (ms_domain b); >(alloc_result … ALLOC) |
---|
3443 | elim (f (nextblock m1)); //; |
---|
3444 | #z (* arith *) napply daemon |
---|
3445 | ] |
---|
3446 | #FB |
---|
3447 | letin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b'); |
---|
3448 | cut (shift_incr f f'); |
---|
3449 | [ whd; #b0 whd in ⊢ (?(???%)?); |
---|
3450 | @eqZb_elim /2/; ] |
---|
3451 | #Hshift_incr |
---|
3452 | cut (f' b = Some ? delta); |
---|
3453 | [ whd in ⊢ (??%?); >(eqZb_z_z …) // ] #efb' |
---|
3454 | %{ f'} %{ m2'} % //; % //; % //; % |
---|
3455 | [ (* inj *) |
---|
3456 | cut (mem_inj val_inject (meminj_of_shift f') m1 m2); |
---|
3457 | [ whd; #chunk #b1 #ofs #v1 #b2 #delta2 #MINJf' #LOAD |
---|
3458 | cut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉); |
---|
3459 | [ <MINJf' whd in ⊢ (???(?%?)); whd in ⊢ (??%%); |
---|
3460 | @eqZb_elim //; #eb |
---|
3461 | >eb |
---|
3462 | cut (valid_block m1 b); |
---|
3463 | [ @valid_access_valid_block |
---|
3464 | [ 3: @load_valid_access // ] |
---|
3465 | ] |
---|
3466 | cut (¬valid_block m1 b); [ /2/ ] |
---|
3467 | #H #H' @False_ind napply (absurd ? H' H) |
---|
3468 | ] #MINJf |
---|
3469 | lapply (ms_inj … MINJf LOAD); *; #v2 *; #A #B |
---|
3470 | %{ v2} % //; |
---|
3471 | @(val_inject_incr … B) |
---|
3472 | @shift_incr_inject_incr // |
---|
3473 | ] #Hmem_inj |
---|
3474 | @(alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?) /2/; |
---|
3475 | whd in ⊢ (??%?); >efb' /2/; |
---|
3476 | | (* samedomain *) |
---|
3477 | >(nextblock_alloc … ALLOC) |
---|
3478 | >(nextblock_alloc … ALLOC2) |
---|
3479 | //; |
---|
3480 | | (* domain *) |
---|
3481 | #b0 (* FIXME: unfold *) >(refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0) |
---|
3482 | >(nextblock_alloc … ALLOC) |
---|
3483 | >(alloc_result … ALLOC) |
---|
3484 | @eqZb_elim #eb0 |
---|
3485 | [ >eb0 (* arith *) napply daemon |
---|
3486 | | lapply (ms_domain b0); elim (f b0); |
---|
3487 | (* arith *) napply daemon |
---|
3488 | ] |
---|
3489 | | (* range *) |
---|
3490 | #b0 #delta0 whd in ⊢ (??%? → ?); |
---|
3491 | @eqZb_elim |
---|
3492 | [ #_ #e <(grumpydestruct1 ??? e) // |
---|
3493 | | #neb #e @(ms_range_1 … b0) @e |
---|
3494 | ] |
---|
3495 | | #b0 #delta0 whd in ⊢ (??%? → ?); |
---|
3496 | >(low_bound_alloc … ALLOC2 ?) |
---|
3497 | >(high_bound_alloc … ALLOC2 ?) |
---|
3498 | @eqZb_elim #eb0 >eb |
---|
3499 | [ >eb0 #ed <(grumpydestruct1 ??? ed) |
---|
3500 | >(eqZb_z_z ?) /3/; |
---|
3501 | | #edelta0 >(eqZb_false … eb0) |
---|
3502 | @ms_range_2 whd in edelta0:(??%?); //; |
---|
3503 | ] |
---|
3504 | ] |
---|
3505 | qed. |
---|
3506 | *)*) |
---|
3507 | (* ** Relation between signed and unsigned loads and stores *) |
---|
3508 | |
---|
3509 | (* Target processors do not distinguish between signed and unsigned |
---|
3510 | stores of 8- and 16-bit quantities. We show these are equivalent. *) |
---|
3511 | |
---|
3512 | (* Signed 8- and 16-bit stores can be performed like unsigned stores. *) |
---|
3513 | |
---|
3514 | lemma in_bounds_equiv: |
---|
3515 | ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A. |
---|
3516 | size_chunk chunk1 = size_chunk chunk2 → |
---|
3517 | (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) = |
---|
3518 | (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]). |
---|
3519 | #chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize |
---|
3520 | elim (in_bounds m chunk1 r b ofs); |
---|
3521 | [ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //; |
---|
3522 | @valid_access_compat //; |
---|
3523 | | #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //; |
---|
3524 | #H' @False_ind @(absurd ?? H) |
---|
3525 | @valid_access_compat //; |
---|
3526 | ] qed. |
---|
3527 | |
---|
3528 | lemma storev_8_signed_unsigned: |
---|
3529 | ∀m,a,v. |
---|
3530 | storev Mint8signed m a v = storev Mint8unsigned m a v. |
---|
3531 | #m #a #v whd in ⊢ (??%%); elim a; //; |
---|
3532 | #r #b #ofs whd in ⊢ (??%%); |
---|
3533 | >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //; |
---|
3534 | qed. |
---|
3535 | |
---|
3536 | lemma storev_16_signed_unsigned: |
---|
3537 | ∀m,a,v. |
---|
3538 | storev Mint16signed m a v = storev Mint16unsigned m a v. |
---|
3539 | #m #a #v whd in ⊢ (??%%); elim a; //; |
---|
3540 | #r #b #ofs whd in ⊢ (??%%); |
---|
3541 | >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //; |
---|
3542 | qed. |
---|
3543 | |
---|
3544 | (* Likewise, some target processors (e.g. the PowerPC) do not have |
---|
3545 | a ``load 8-bit signed integer'' instruction. |
---|
3546 | We show that it can be synthesized as a ``load 8-bit unsigned integer'' |
---|
3547 | followed by a sign extension. *) |
---|
3548 | |
---|
3549 | (* Nonessential properties that may require arithmetic |
---|
3550 | lemma loadv_8_signed_unsigned: |
---|
3551 | ∀m,a. |
---|
3552 | loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a). |
---|
3553 | #m #a whd in ⊢ (??%(????(%))); elim a; //; |
---|
3554 | #r #b #ofs whd in ⊢ (??%(????%)); |
---|
3555 | >(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //; |
---|
3556 | elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/; |
---|
3557 | #H whd in ⊢ (??%%); |
---|
3558 | elim (getN 0 (signed ofs) (contents (blocks m b))); |
---|
3559 | [ 1,3: //; |
---|
3560 | | #i whd in ⊢ (??(??%)(??%)); |
---|
3561 | >(sign_ext_zero_ext ?? i) [ @refl (* XXX: // ? *) |
---|
3562 | | (* arith *) @daemon |
---|
3563 | ] |
---|
3564 | | #sp cases sp; //; |
---|
3565 | ] |
---|
3566 | qed. |
---|
3567 | *) |
---|