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