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