1 | include "Clight/Cexec.ma". |
---|
2 | include "Clight/MemProperties.ma". |
---|
3 | include "Clight/frontend_misc.ma". |
---|
4 | |
---|
5 | (* This file contains some definitions and lemmas related to memory injections. |
---|
6 | * The whole development is quite similar to the one described in the article by |
---|
7 | * Leroy & Blazy in J.A.R., except that in Cerco, we describe data down to the byte |
---|
8 | * level (similar to the memory model of CompCert v2 but not to the aforementioned |
---|
9 | * paper). |
---|
10 | * *) |
---|
11 | |
---|
12 | (* --------------------------------------------------------------------------- *) |
---|
13 | (* Aux lemmas that are likely to be found elsewhere. *) |
---|
14 | (* --------------------------------------------------------------------------- *) |
---|
15 | |
---|
16 | lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true. |
---|
17 | #a #b #HA |
---|
18 | lapply (Zltb_true_to_Zlt … HA) #HA_prop |
---|
19 | @Zlt_to_Zltb_true /2/ |
---|
20 | qed. |
---|
21 | |
---|
22 | lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true. |
---|
23 | #a @Zlt_to_Zltb_true /2/ qed. |
---|
24 | (* |
---|
25 | definition le_offset : offset → offset → bool. |
---|
26 | λx,y. Zleb (offv x) (offv y). |
---|
27 | *) |
---|
28 | lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed. |
---|
29 | |
---|
30 | lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed. |
---|
31 | |
---|
32 | lemma eqZb_symmetric : ∀x,y:Z. eqZb x y = eqZb y x. |
---|
33 | #x #y @(eqZb_elim … x y) |
---|
34 | [ * >eqZb_z_z @refl |
---|
35 | | #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ] |
---|
36 | qed. |
---|
37 | |
---|
38 | (* TODO: move in frontend_misc. This axiom states that for small bitvectors, bitvector addition |
---|
39 | * commutes with conversion to Z, i.e. there is no overflow. *) |
---|
40 | axiom Z_addition_bv_commute : |
---|
41 | ∀n. ∀v1,v2:BitVector n. |
---|
42 | (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2) < Z_two_power_nat n → |
---|
43 | Z_of_unsigned_bitvector ? (addition_n ? v1 v2) = |
---|
44 | (Z_of_unsigned_bitvector ? v1) + (Z_of_unsigned_bitvector ? v2). |
---|
45 | |
---|
46 | (* TODO: move in frontend_misc *) |
---|
47 | lemma Zlt_to_Zneq : ∀x,y:Z. x < y → x ≠ y. |
---|
48 | #x #y /3 by absurd, nmk/ |
---|
49 | qed. |
---|
50 | |
---|
51 | lemma Zlt_translate : ∀x,y,delta:Z. x < y → x + delta < y + delta. |
---|
52 | #x #y #delta /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle/ |
---|
53 | qed. |
---|
54 | |
---|
55 | lemma Zlt_weaken : ∀x,y,delta:Z. delta ≥ 0 → x < y → x < y + delta. |
---|
56 | #x #y #delta cases delta try // #p |
---|
57 | [ 2: #Habsurd @(False_ind … Habsurd) ] |
---|
58 | /3 by Zlt_to_Zle_to_Zlt, Zplus_le_pos/ |
---|
59 | qed. |
---|
60 | |
---|
61 | lemma Zlt_sum_weaken : ∀a,a',b,c:Z. a+b < c → a' < a → a'+b < c. |
---|
62 | #a #a' #b #c /3 by transitive_Zlt, Zlt_translate/ qed. |
---|
63 | |
---|
64 | |
---|
65 | (* TODO: move to Z.ma *) |
---|
66 | lemma monotonic_Zlt_Zsucc : monotonic Z Zlt Zsucc. |
---|
67 | #x #y cases x cases y /2/ |
---|
68 | [ #n /3 by Zle_to_Zlt_to_Zlt, monotonic_Zle_Zplus_r/ ] |
---|
69 | #n #m @(pos_cases … n) @(pos_cases … m) // |
---|
70 | [ #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/ |
---|
71 | | #m #n /3 by I, Zle_to_Zlt, monotonic_Zle_Zplus_r/ |
---|
72 | | /2 by Zlt_translate/ |
---|
73 | | /3 by Zle_to_Zlt, monotonic_Zle_Zplus_r/ |
---|
74 | | #n' /3 by Zle_to_Zlt_to_Zlt, lt_to_Zlt_neg_neg, Zlt_to_Zle/ |
---|
75 | | #n' #m' /3 by lt_plus_to_lt_r, lt_to_Zlt_neg_neg/ ] |
---|
76 | qed. |
---|
77 | |
---|
78 | lemma monotonic_Zlt_Zpred : monotonic Z Zlt Zpred. |
---|
79 | #x #y cases x cases y /2/ |
---|
80 | [ #n /3 by Zle_to_Zlt, monotonic_Zle_Zpred/ |
---|
81 | | #m #n @(pos_cases … n) @(pos_cases … m) |
---|
82 | [ /3 by monotonic_Zlt_Zsucc/ |
---|
83 | | /3 by refl, true_to_andb_true, Zltb_true_to_Zlt/ |
---|
84 | | #n' cases n' normalize |
---|
85 | [ #H inversion H [ #H' destruct | #m' #_ #_ #Habsurd @(absurd … Habsurd (not_eq_one_succ m')) ] |
---|
86 | | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/ |
---|
87 | | #p /3 by le_to_lt_to_lt, le_S_contradiction_1/ ] |
---|
88 | | #m' #n' /3 by lt_plus_to_lt_r, lt_to_Zlt_pos_pos/ ] |
---|
89 | | #m #n /3 by Zplus_le_pos, Zle_to_Zlt/ |
---|
90 | ] qed. |
---|
91 | |
---|
92 | lemma monotonic_Zlt_Zplus_l: ∀n.monotonic Z Zlt (λm.m + n). |
---|
93 | #n cases n // #n' #a #b #H |
---|
94 | [ @(pos_elim … n') |
---|
95 | [ >sym_Zplus >(sym_Zplus b) <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) @monotonic_Zlt_Zsucc @H |
---|
96 | | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) // |
---|
97 | >(Zplus_Zsucc …) >(Zplus_Zsucc …) // |
---|
98 | cases a in H; cases b /2/ |
---|
99 | #p #H /3 by Zlt_to_Zle_to_Zlt, monotonic_Zle_Zsucc, monotonic_Zlt_Zsucc/ |
---|
100 | ] |
---|
101 | | @(pos_elim … n') |
---|
102 | [ >sym_Zplus >(sym_Zplus b) <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/; |
---|
103 | | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) // |
---|
104 | /3 by Zle_to_Zlt_to_Zlt, monotonic_Zlt_Zpred/ |
---|
105 | ] |
---|
106 | ] qed. |
---|
107 | |
---|
108 | |
---|
109 | lemma Zlt_to_Zle' : ∀x,y:Z. x < y → x ≤ y. |
---|
110 | #x #y /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ |
---|
111 | qed. |
---|
112 | |
---|
113 | |
---|
114 | |
---|
115 | (* --------------------------------------------------------------------------- *) |
---|
116 | (* Some shorthands for conversion functions from BitVectorZ. *) |
---|
117 | (* --------------------------------------------------------------------------- *) |
---|
118 | |
---|
119 | (* Offsets are just bitvectors packed inside some annoying constructor. *) |
---|
120 | definition Zoo ≝ λx. Z_of_unsigned_bitvector ? (offv x). |
---|
121 | definition boo ≝ λx. mk_offset (bitvector_of_Z ? x). |
---|
122 | |
---|
123 | (* --------------------------------------------------------------------------- *) |
---|
124 | (* In the definition of injections below, we maintain a list of blocks that are |
---|
125 | writeable. We need some lemmas to reason on the fact that a block cannot be |
---|
126 | both writeable and not writeable, etc. *) |
---|
127 | (* --------------------------------------------------------------------------- *) |
---|
128 | |
---|
129 | (* When equality on A is decidable, [mem A elt l] is too. *) |
---|
130 | lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l). |
---|
131 | #A #dec #elt #l elim l |
---|
132 | [ 1: normalize %2 /2/ |
---|
133 | | 2: #hd #tl #Hind |
---|
134 | elim (dec elt hd) |
---|
135 | [ 1: #Heq >Heq %1 /2/ |
---|
136 | | 2: #Hneq cases Hind |
---|
137 | [ 1: #Hmem %1 /2/ |
---|
138 | | 2: #Hnmem %2 normalize |
---|
139 | % #H cases H |
---|
140 | [ 1: lapply Hneq * #Hl #Eq @(Hl Eq) |
---|
141 | | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ] |
---|
142 | ] ] ] |
---|
143 | qed. |
---|
144 | |
---|
145 | |
---|
146 | lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b. |
---|
147 | * #a * #b |
---|
148 | cases (decidable_eq_Z … a b) |
---|
149 | [ * %1 @refl |
---|
150 | | #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed. |
---|
151 | |
---|
152 | lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b). |
---|
153 | * #a * #b |
---|
154 | cases (decidable_eq_Z_Type … a b) |
---|
155 | [ * %1 @refl |
---|
156 | | #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed. |
---|
157 | |
---|
158 | lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2. |
---|
159 | #l #elt1 #elt2 elim l |
---|
160 | [ 1: normalize #Habsurd @(False_ind … Habsurd) |
---|
161 | | 2: #hd #tl #Hind normalize #Hl #Hr |
---|
162 | cases Hl |
---|
163 | [ 1: #Heq >Heq |
---|
164 | @(eq_block_elim … hd elt2) |
---|
165 | [ 1: #Heq >Heq /2 by not_to_not/ |
---|
166 | | 2: #x @x ] |
---|
167 | | 2: #Hmem1 cases (mem_dec ? block_eq_dec ? tl) |
---|
168 | [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2 |
---|
169 | | 2: #Hmem2 @Hind // |
---|
170 | ] |
---|
171 | ] |
---|
172 | ] qed. |
---|
173 | |
---|
174 | lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false. |
---|
175 | #b1 #b2 * #Hb |
---|
176 | @(eq_block_elim … b1 b2) |
---|
177 | [ 1: #Habsurd @(False_ind … (Hb Habsurd)) |
---|
178 | | 2: // ] qed. |
---|
179 | |
---|
180 | (* --------------------------------------------------------------------------- *) |
---|
181 | (* Lemmas related to freeing memory and pointer validity. *) |
---|
182 | (* --------------------------------------------------------------------------- *) |
---|
183 | |
---|
184 | lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr. |
---|
185 | valid_pointer m ptr = true → |
---|
186 | pblock ptr ≠ b → |
---|
187 | valid_pointer (free m b) ptr = true. |
---|
188 | * (* #br *) #bid * #contents #next #posnext * * (* #pbr *) #pbid #poff |
---|
189 | normalize |
---|
190 | @(eqZb_elim pbid bid) |
---|
191 | [ 1: #Heqid >Heqid (* cases pbr cases br normalize *) |
---|
192 | cases (Zltb bid next) normalize nodelta |
---|
193 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
194 | #_ #H @False_ind @(absurd … (refl ??) H) |
---|
195 | | 2: #Hneqid (* cases pbr cases br normalize *) try // ] |
---|
196 | qed. |
---|
197 | |
---|
198 | lemma free_list_cons : ∀m,b,tl. free_list m (b :: tl) = (free (free_list m tl) b). |
---|
199 | #m #b #tl whd in match (free_list ??) in ⊢ (??%%); |
---|
200 | whd in match (free ??); @refl qed. |
---|
201 | |
---|
202 | (* |
---|
203 | lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr. |
---|
204 | valid_pointer (free m b) ptr = true → |
---|
205 | pblock ptr ≠ b → (* This hypothesis is necessary to handle the cse of "valid" pointers to empty *) |
---|
206 | valid_pointer m ptr = true. |
---|
207 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
208 | @(eqZb_elim pbid bid) |
---|
209 | [ 1: #Heqid >Heqid |
---|
210 | cases pbr cases br normalize |
---|
211 | [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ] |
---|
212 | cases (Zltb bid next) normalize nodelta |
---|
213 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
214 | // |
---|
215 | | 2: #Hneqid cases pbr cases br normalize try // |
---|
216 | >(eqZb_false … Hneqid) normalize nodelta try // |
---|
217 | qed. |
---|
218 | |
---|
219 | lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr. |
---|
220 | valid_pointer (free_list m blocks) ptr = true → |
---|
221 | ¬ mem ? (pblock ptr) blocks → |
---|
222 | valid_pointer m ptr = true. |
---|
223 | #blocks |
---|
224 | elim blocks |
---|
225 | [ 1: #m #ptr normalize #H #_ @H |
---|
226 | | 2: #b #tl #Hind #m #ptr #Hvalid |
---|
227 | whd in match (mem block (pblock ptr) ?); |
---|
228 | >free_list_cons in Hvalid; #Hvalid * #Hguard |
---|
229 | lapply (valid_pointer_free_ok … Hvalid) #H |
---|
230 | @Hind |
---|
231 | [ 2: % #Heq @Hguard %2 @Heq |
---|
232 | | 1: @H % #Heq @Hguard %1 @Heq ] |
---|
233 | ] qed. *) |
---|
234 | |
---|
235 | (* An alternative version without the gard on the equality of blocks. *) |
---|
236 | (* |
---|
237 | lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr. |
---|
238 | valid_pointer (free m b) ptr = true → |
---|
239 | (pblock ptr) = b ∨ (pblock ptr ≠ b ∧ valid_pointer m ptr = true). |
---|
240 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
241 | @(eq_block_elim … (mk_block br bid) (mk_block pbr pbid)) |
---|
242 | [ 1: #Heq #_ %1 @(sym_eq … Heq) |
---|
243 | | 2: cases pbr cases br normalize nodelta |
---|
244 | [ 1,4: @(eqZb_elim pbid bid) |
---|
245 | [ 1,3: #Heq >Heq * #H @(False_ind … (H (refl ??))) |
---|
246 | | 2,4: #Hneq #_ normalize >(eqZb_false … Hneq) normalize nodelta |
---|
247 | #H %2 @conj try assumption |
---|
248 | % #Habsurd destruct (Habsurd) elim Hneq #Hneq @Hneq try @refl |
---|
249 | ] |
---|
250 | | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ] |
---|
251 | ] qed. *) |
---|
252 | |
---|
253 | (* Well in fact a valid pointer can be valid even after a free. Ah. *) |
---|
254 | (* |
---|
255 | lemma pointer_in_free_list_not_valid : ∀blocks,m,ptr. |
---|
256 | mem ? (pblock ptr) blocks → |
---|
257 | valid_pointer (free_list m blocks) ptr = false. |
---|
258 | *) |
---|
259 | (* |
---|
260 | #blocks elim blocks |
---|
261 | [ 1: #m #ptr normalize #Habsurd @(False_ind … Habsurd) |
---|
262 | | 2: #b #tl #Hind #m #ptr |
---|
263 | whd in match (mem block (pblock ptr) ?); |
---|
264 | >free_list_cons |
---|
265 | * |
---|
266 | [ 1: #Hptr_match whd in match (free ??); |
---|
267 | whd in match (update_block ????); |
---|
268 | whd in match (valid_pointer ??); |
---|
269 | whd in match (low_bound ??); |
---|
270 | whd in match (high_bound ??); |
---|
271 | >Hptr_match >eq_block_identity normalize nodelta |
---|
272 | whd in match (low ?); |
---|
273 | cut (Zleb OZ (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = true) |
---|
274 | [ 1: elim (offv (poff ptr)) // |
---|
275 | #n' #hd #tl cases hd normalize |
---|
276 | [ 1: #_ try @refl |
---|
277 | | 2: #H @H ] ] |
---|
278 | #H >H |
---|
279 | cut (Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) OZ = false) |
---|
280 | [ 1: elim (offv (poff ptr)) normalize |
---|
281 | #n' #hd #tl cases hd normalize |
---|
282 | [ 1: normalize #_ try @refl |
---|
283 | | 2: #H @H ] ] |
---|
284 | valid_pointer (free_list m blocks) ptr = false. |
---|
285 | *) |
---|
286 | |
---|
287 | |
---|
288 | (* --------------------------------------------------------------------------- *) |
---|
289 | (* Memory injections *) |
---|
290 | (* --------------------------------------------------------------------------- *) |
---|
291 | |
---|
292 | (* An embedding is a function from block ids to (blocks × offset). *) |
---|
293 | definition embedding ≝ block → option (block × offset). |
---|
294 | |
---|
295 | definition offset_plus : offset → offset → offset ≝ |
---|
296 | λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)). |
---|
297 | |
---|
298 | lemma offset_plus_0 : ∀o. offset_plus (mk_offset (zero ?)) o = o. |
---|
299 | * #o |
---|
300 | whd in match (offset_plus ??); |
---|
301 | >commutative_addition_n |
---|
302 | >addition_n_0 @refl |
---|
303 | qed. |
---|
304 | |
---|
305 | (* Translates a pointer through an embedding. *) |
---|
306 | definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝ |
---|
307 | λp,E. |
---|
308 | match p with |
---|
309 | [ mk_pointer pblock poff ⇒ |
---|
310 | match E pblock with |
---|
311 | [ None ⇒ None ? |
---|
312 | | Some loc ⇒ |
---|
313 | let 〈dest_block,dest_off〉 ≝ loc in |
---|
314 | let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in |
---|
315 | Some ? ptr |
---|
316 | ] |
---|
317 | ]. |
---|
318 | |
---|
319 | (* Definition of embedding compatibility. *) |
---|
320 | definition embedding_compatible : embedding → embedding → Prop ≝ |
---|
321 | λE,E'. |
---|
322 | ∀b:block. E b = None ? ∨ |
---|
323 | E b = E' b. |
---|
324 | |
---|
325 | (* We parameterise the "equivalence" relation on values with an embedding. *) |
---|
326 | (* Front-end values. *) |
---|
327 | inductive value_eq (E : embedding) : val → val → Prop ≝ |
---|
328 | | undef_eq : |
---|
329 | value_eq E Vundef Vundef |
---|
330 | | vint_eq : ∀sz,i. |
---|
331 | value_eq E (Vint sz i) (Vint sz i) |
---|
332 | | vnull_eq : |
---|
333 | value_eq E Vnull Vnull |
---|
334 | | vptr_eq : ∀p1,p2. |
---|
335 | pointer_translation p1 E = Some ? p2 → |
---|
336 | value_eq E (Vptr p1) (Vptr p2). |
---|
337 | |
---|
338 | (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. |
---|
339 | * the values are equivalent. *) |
---|
340 | definition load_sim ≝ |
---|
341 | λ(E : embedding).λ(m1 : mem).λ(m2 : mem). |
---|
342 | ∀b1,off1,b2,off2,ty,v1. |
---|
343 | valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *) |
---|
344 | E b1 = Some ? 〈b2,off2〉 → |
---|
345 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
346 | (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). |
---|
347 | |
---|
348 | definition load_sim_ptr ≝ |
---|
349 | λ(E : embedding).λ(m1 : mem).λ(m2 : mem). |
---|
350 | ∀b1,off1,b2,off2,ty,v1. |
---|
351 | valid_pointer m1 (mk_pointer b1 off1) = true → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading by-ref *) |
---|
352 | pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) → |
---|
353 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
354 | (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2). |
---|
355 | |
---|
356 | definition block_is_empty : mem → block → Prop ≝ |
---|
357 | λm,b. |
---|
358 | high_bound m b ≤ low_bound m b. |
---|
359 | |
---|
360 | (* Definition of a 16 bit bitvector-implementable Z *) |
---|
361 | definition z_implementable_bv : Z → Prop ≝ |
---|
362 | λz:Z. |
---|
363 | 0 ≤ z ∧ z < Z_two_power_nat 16. |
---|
364 | |
---|
365 | (* Characterizing implementable blocks *) |
---|
366 | definition block_implementable_bv ≝ |
---|
367 | λm:mem.λb:block. |
---|
368 | z_implementable_bv (low_bound m b) ∧ |
---|
369 | z_implementable_bv (high_bound m b). (* FIXME this is slightly restrictive. We could allow the high bound to be 2^16.*) |
---|
370 | |
---|
371 | (* Characterizing blocks compatible with an embedding. This condition ensures |
---|
372 | * that we do not stray out of memory. *) |
---|
373 | (* |
---|
374 | definition block_ok_with_embedding ≝ λE:embedding.λb,m. |
---|
375 | ∀b',delta. |
---|
376 | E b = Some ? 〈b', delta〉 → |
---|
377 | (high_bound m b) + (Zoo delta) < Z_two_power_nat 16. *) |
---|
378 | |
---|
379 | (* We have to prove that the blocks we allocate are compatible with a given embedding. |
---|
380 | This amounts to proving that the embedding cannot shift the new block outside the 2^16 bound. |
---|
381 | Notice that the following def. only constraints block mapped through the embedding. |
---|
382 | *) |
---|
383 | definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝ |
---|
384 | λE.λb.λm,m'. |
---|
385 | match E b with |
---|
386 | [ None ⇒ True |
---|
387 | | Some loc ⇒ |
---|
388 | let 〈b', delta〉 ≝ loc in |
---|
389 | block_implementable_bv m b ∧ |
---|
390 | block_implementable_bv m' b' ∧ |
---|
391 | (high_bound m b) + (Zoo delta) < Z_two_power_nat 16 |
---|
392 | ]. |
---|
393 | |
---|
394 | (* Adapted from Compcert's Memory *) |
---|
395 | definition non_aliasing : embedding → mem → Prop ≝ |
---|
396 | λE,m. |
---|
397 | ∀b1,b2,b1',b2',delta1,delta2. |
---|
398 | b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *) |
---|
399 | E b1 = Some ? 〈b1',delta1〉 → |
---|
400 | E b2 = Some ? 〈b2',delta2〉 → |
---|
401 | (if eq_block b1' b2' then |
---|
402 | (* block_is_empty m b1' ∨ *) |
---|
403 | high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ |
---|
404 | high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨ |
---|
405 | block_is_empty m b1 ∨ |
---|
406 | block_is_empty m b2 |
---|
407 | else |
---|
408 | True). |
---|
409 | |
---|
410 | |
---|
411 | (* Adapted from Compcert's "Memory" *) |
---|
412 | |
---|
413 | (* Definition of a memory injection *) |
---|
414 | record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝ |
---|
415 | { (* Load simulation *) |
---|
416 | mi_inj : load_sim_ptr E m1 m2; |
---|
417 | (* Invalid blocks are not mapped *) |
---|
418 | mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; |
---|
419 | (* Valid pointers are mapped to valid pointers *) |
---|
420 | mi_valid_pointers : ∀p,p'. |
---|
421 | valid_pointer m1 p = true → |
---|
422 | pointer_translation p E = Some ? p' → |
---|
423 | valid_pointer m2 p' = true; |
---|
424 | (* Blocks in the codomain are valid *) |
---|
425 | mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; |
---|
426 | (* Regions are preserved *) |
---|
427 | mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; |
---|
428 | (* sub-blocks do not overlap (non-aliasing property) *) |
---|
429 | mi_nonalias : non_aliasing E m1; |
---|
430 | (* mapped blocks are bitvector-implementable *) |
---|
431 | (* mi_implementable : |
---|
432 | ∀b,b',o'. |
---|
433 | E b = Some ? 〈b',o'〉 → |
---|
434 | block_implementable_bv m1 b ∧ |
---|
435 | block_implementable_bv m2 b'; *) |
---|
436 | (* The offset produced by the embedding shifts data within the 2^16 bound ... |
---|
437 | * We need this to rule out the following case: consider a huge block taking up |
---|
438 | * all the space [0; 2^16[. We can come up with an embedding that keeps the same block |
---|
439 | * but which shifts the data by some value, effectively rotating all the data around the |
---|
440 | * 2^16 offset limit. Valid pointers stay valid, the block is implementable ... But we |
---|
441 | * obviously can't prove that the semantics of pointer comparisons is preserved. *) |
---|
442 | mi_nowrap : |
---|
443 | ∀b. block_in_bounds_if_mapped E b m1 m2 |
---|
444 | }. |
---|
445 | |
---|
446 | (* ---------------------------------------------------------------------------- *) |
---|
447 | (* Setting up an empty injection *) |
---|
448 | (* ---------------------------------------------------------------------------- *) |
---|
449 | |
---|
450 | definition empty_injection : memory_inj (λx. None ?) empty empty. |
---|
451 | % |
---|
452 | [ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload |
---|
453 | normalize in Hptr_trans; destruct |
---|
454 | | #b #H @refl |
---|
455 | | * #b #o #p' #_ normalize #Habsurd destruct |
---|
456 | | #b #b' #off #Habsurd destruct |
---|
457 | | #b #b' #o' #Habsurd destruct |
---|
458 | | whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct |
---|
459 | | #b whd @I |
---|
460 | ] qed. |
---|
461 | |
---|
462 | (* ---------------------------------------------------------------------------- *) |
---|
463 | (* End of the definitions on memory injections. Now, on to proving some lemmas. *) |
---|
464 | (* ---------------------------------------------------------------------------- *) |
---|
465 | |
---|
466 | |
---|
467 | |
---|
468 | (**** Lemmas on value_eq. *) |
---|
469 | |
---|
470 | (* particulars inversions. *) |
---|
471 | lemma value_eq_ptr_inversion : |
---|
472 | ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2. |
---|
473 | #E #p1 #v #Heq inversion Heq |
---|
474 | [ 1: #Habsurd destruct (Habsurd) |
---|
475 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
476 | | 3: #Habsurd destruct (Habsurd) |
---|
477 | | 4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct |
---|
478 | %{p2} @conj try @refl try assumption |
---|
479 | ] qed. |
---|
480 | |
---|
481 | lemma value_eq_int_inversion : |
---|
482 | ∀E,sz,i,v. value_eq E (Vint sz i) v → v = (Vint sz i). |
---|
483 | #E #sz #i #v #Heq inversion Heq |
---|
484 | [ 1: #Habsurd destruct (Habsurd) |
---|
485 | | 2: #sz #i #Heq #Heq' #_ @refl |
---|
486 | | 3: #Habsurd destruct (Habsurd) |
---|
487 | | 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ] |
---|
488 | qed. |
---|
489 | |
---|
490 | lemma value_eq_int_inversion' : |
---|
491 | ∀E,sz,i,v. value_eq E v (Vint sz i) → v = (Vint sz i). |
---|
492 | #E #sz #i #v #Heq inversion Heq |
---|
493 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
494 | | 2: #sz #i #Heq #Heq' #_ @refl |
---|
495 | | 3: #_ #Habsurd destruct (Habsurd) |
---|
496 | | 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ] |
---|
497 | qed. |
---|
498 | |
---|
499 | lemma value_eq_null_inversion : |
---|
500 | ∀E,v. value_eq E Vnull v → v = Vnull. |
---|
501 | #E #v #Heq inversion Heq // |
---|
502 | #p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd) |
---|
503 | #Habsurd' destruct |
---|
504 | qed. |
---|
505 | |
---|
506 | lemma value_eq_null_inversion' : |
---|
507 | ∀E,v. value_eq E v Vnull → v = Vnull. |
---|
508 | #E #v #Heq inversion Heq // |
---|
509 | #p1 #p2 #Htranslate #_ #Habsurd lapply (jmeq_to_eq ??? Habsurd) |
---|
510 | #Habsurd' destruct |
---|
511 | qed. |
---|
512 | |
---|
513 | (* A cleaner version of inversion for [value_eq] *) |
---|
514 | lemma value_eq_inversion : |
---|
515 | ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → |
---|
516 | (P Vundef Vundef) → |
---|
517 | (∀sz,i. P (Vint sz i) (Vint sz i)) → |
---|
518 | (P Vnull Vnull) → |
---|
519 | (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) → |
---|
520 | P v1 v2. |
---|
521 | #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 |
---|
522 | inversion Heq |
---|
523 | [ 1: #Hv1 #Hv2 #_ destruct @H1 |
---|
524 | | 2: #sz #i #Hv1 #Hv2 #_ destruct @H2 |
---|
525 | | 3: #Hv1 #Hv2 #_ destruct @H3 |
---|
526 | | 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed. |
---|
527 | |
---|
528 | (* Avoids the use of cut in toCminorCorrectness *) |
---|
529 | lemma value_eq_triangle_diagram : |
---|
530 | ∀E,v1,v2,v3. |
---|
531 | value_eq E v1 v2 → v2 = v3 → value_eq E v1 v3. |
---|
532 | #H1 #H2 #H3 #H4 #H5 #H6 destruct // |
---|
533 | qed. |
---|
534 | |
---|
535 | (* embedding compatibility preserves value equivalence *) |
---|
536 | (* This is lemma 65 of Leroy&Blazy. *) |
---|
537 | lemma embedding_compatibility_value_eq : |
---|
538 | ∀E,E'. embedding_compatible E E' → ∀v1,v2. value_eq E v1 v2 → value_eq E' v1 v2. |
---|
539 | #E #E' #Hcompat #v1 #v2 #Hvalue_eq |
---|
540 | @(value_eq_inversion … Hvalue_eq) try // |
---|
541 | #p1 #p2 whd in match (pointer_translation ??); cases p1 #b1 #o1 normalize nodelta |
---|
542 | cases (Hcompat b1) |
---|
543 | [ #Hnone >Hnone normalize nodelta #Habsurd destruct |
---|
544 | | #Heq >Heq #Hres %4 @Hres ] |
---|
545 | qed. |
---|
546 | |
---|
547 | |
---|
548 | |
---|
549 | |
---|
550 | (**** Lemmas on pointer validity wrt loads. *) |
---|
551 | |
---|
552 | (* If we succeed to load something by value from a 〈b,off〉 location, |
---|
553 | [b] is a valid block. *) |
---|
554 | (* |
---|
555 | lemma load_by_value_success_valid_block_aux : |
---|
556 | ∀ty,m,b,off,v. |
---|
557 | access_mode ty = By_value (typ_of_type ty) → |
---|
558 | load_value_of_type ty m b off = Some ? v → |
---|
559 | Zltb (block_id b) (nextblock m) = true. |
---|
560 | #ty #m * #brg #bid #off #v |
---|
561 | cases ty |
---|
562 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
563 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
564 | whd in match (load_value_of_type ????); |
---|
565 | [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] |
---|
566 | #Hmode |
---|
567 | [ 1,2,5: [ 1: elim sz ] |
---|
568 | normalize in match (typesize ?); |
---|
569 | whd in match (loadn ???); |
---|
570 | whd in match (beloadv ??); |
---|
571 | cases (Zltb bid (nextblock m)) normalize nodelta |
---|
572 | try // #Habsurd destruct (Habsurd) |
---|
573 | | *: normalize in Hmode; destruct (Hmode) |
---|
574 | ] qed. *) |
---|
575 | |
---|
576 | (* If we succeed in loading some data from a location, then this loc is a valid pointer. *) |
---|
577 | lemma load_by_value_success_valid_ptr_aux : |
---|
578 | ∀ty,m,b,off,v. |
---|
579 | access_mode ty = By_value (typ_of_type ty) → |
---|
580 | load_value_of_type ty m b off = Some ? v → |
---|
581 | Zltb (block_id b) (nextblock m) = true ∧ |
---|
582 | Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ |
---|
583 | Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. |
---|
584 | #ty #m * (* #brg *) #bid #off #v |
---|
585 | cases ty |
---|
586 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
587 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
588 | whd in match (load_value_of_type ????); |
---|
589 | [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] |
---|
590 | #Hmode |
---|
591 | [ 1,2,5: [ 1: elim sz ] |
---|
592 | normalize in match (typesize ?); |
---|
593 | whd in match (loadn ???); |
---|
594 | whd in match (beloadv ??); |
---|
595 | cases (Zltb bid (nextblock m)) normalize nodelta |
---|
596 | cases (Zleb (low (blocks m (mk_block (*brg*) bid))) |
---|
597 | (Z_of_unsigned_bitvector offset_size (offv off))) |
---|
598 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block (*brg*) bid)))) |
---|
599 | normalize nodelta |
---|
600 | #Heq destruct (Heq) |
---|
601 | try /3 by conj, refl/ |
---|
602 | | *: normalize in Hmode; destruct (Hmode) |
---|
603 | ] qed. |
---|
604 | |
---|
605 | lemma load_by_value_success_valid_block : |
---|
606 | ∀ty,m,b,off,v. |
---|
607 | access_mode ty = By_value (typ_of_type ty) → |
---|
608 | load_value_of_type ty m b off = Some ? v → |
---|
609 | valid_block m b. |
---|
610 | #ty #m #b #off #v #Haccess_mode #Hload |
---|
611 | @Zltb_true_to_Zlt |
---|
612 | elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * // |
---|
613 | qed. |
---|
614 | |
---|
615 | lemma load_by_value_success_valid_pointer : |
---|
616 | ∀ty,m,b,off,v. |
---|
617 | access_mode ty = By_value (typ_of_type ty) → |
---|
618 | load_value_of_type ty m b off = Some ? v → |
---|
619 | valid_pointer m (mk_pointer b off) = true. |
---|
620 | #ty #m #b #off #v #Haccess_mode #Hload normalize |
---|
621 | elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) |
---|
622 | * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @refl |
---|
623 | qed. |
---|
624 | |
---|
625 | |
---|
626 | |
---|
627 | (**** Lemmas related to memory injections. *) |
---|
628 | |
---|
629 | (* Making explicit the contents of memory_inj for load_value_of_type. |
---|
630 | * Equivalent to Lemma 59 of Leroy & Blazy *) |
---|
631 | lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty. |
---|
632 | memory_inj E m1 m2 → |
---|
633 | value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) → |
---|
634 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
635 | ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2. |
---|
636 | #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq |
---|
637 | lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct |
---|
638 | lapply (refl ? (access_mode ty)) |
---|
639 | cases ty |
---|
640 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
641 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
642 | normalize in ⊢ ((???%) → ?); #Hmode #Hyp |
---|
643 | [ 1,6,7: normalize in Hyp; destruct (Hyp) |
---|
644 | | 4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ] |
---|
645 | lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer |
---|
646 | lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H |
---|
647 | qed. |
---|
648 | |
---|
649 | |
---|
650 | (* Lemmas pertaining to memory allocation *) |
---|
651 | |
---|
652 | (* |
---|
653 | lemma alloc_valid_block_not_eq : |
---|
654 | ∀m,m',z1,z2,(*r,*)new_block. |
---|
655 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
656 | ∀b. valid_block m b → b ≠ new_block. |
---|
657 | * #c #n #Hn #m' #z1 #z2 #new |
---|
658 | whd in ⊢ ((??%?) → ?); #Heq destruct |
---|
659 | #b whd in ⊢ (% → ?); cases b #bid |
---|
660 | #Hlt % #Heq destruct (Heq) |
---|
661 | @(absurd … Hlt (irreflexive_Zlt n)) |
---|
662 | qed. |
---|
663 | *) |
---|
664 | (* A valid block stays valid after an alloc. *) |
---|
665 | lemma alloc_valid_block_conservation : |
---|
666 | ∀m,m',z1,z2,(*r,*)new_block. |
---|
667 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
668 | ∀b. valid_block m b → valid_block m' b. |
---|
669 | #m #m' #z1 #z2 (* #r*) * #b' (* #Hregion_eq *) |
---|
670 | elim m #contents #nextblock #Hcorrect whd in match (alloc ???(*?*)); |
---|
671 | #Halloc destruct (Halloc) |
---|
672 | #b whd in match (valid_block ??) in ⊢ (% → %); /2/ |
---|
673 | qed. |
---|
674 | |
---|
675 | lemma Zle_split : |
---|
676 | ∀a,b:Z. a ≤ b → a ≠ b → a < b. |
---|
677 | #a #b elim a elim b try /2/ |
---|
678 | #p1 #p2 #Hle #Hneq whd |
---|
679 | @not_eq_to_le_to_lt |
---|
680 | try // % #Heq destruct cases Hneq #H @H @refl |
---|
681 | qed. |
---|
682 | |
---|
683 | (* A valid block /after/ an alloc was valid before if it is different |
---|
684 | * from the newly allocated one. *) |
---|
685 | lemma alloc_valid_block_conservation2 : |
---|
686 | ∀m,m',z1,z2,new_block. |
---|
687 | alloc m z1 z2 =〈m',new_block〉 → |
---|
688 | ∀b. b ≠ new_block → |
---|
689 | valid_block m' b → |
---|
690 | valid_block m b. |
---|
691 | #m #m' #z1 #z2 #new_block |
---|
692 | cases m #cont #next #Hnext |
---|
693 | whd in ⊢ ((??%%) → ?); |
---|
694 | #Heq destruct (Heq) #b #Hneq #Hvalid |
---|
695 | whd in Hvalid ⊢ %; |
---|
696 | cases b in Hneq Hvalid; #bid * #H #Hlt |
---|
697 | cut (bid ≠ next) |
---|
698 | [ % #Heq destruct @H @refl ] |
---|
699 | #Hneq |
---|
700 | @(Zle_split … Hneq) |
---|
701 | /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ |
---|
702 | qed. |
---|
703 | |
---|
704 | lemma alloc_bounds_conservation : |
---|
705 | ∀m,m',z1,z2,new_block. |
---|
706 | alloc m z1 z2 =〈m',new_block〉 → |
---|
707 | ∀b. b ≠ new_block → |
---|
708 | low_bound m' b = low_bound m b ∧ |
---|
709 | high_bound m' b = high_bound m b. |
---|
710 | #m #m' #z1 #z2 #new #Halloc #b |
---|
711 | #Hneq cases m in Halloc; #c #n #Hn |
---|
712 | whd in ⊢ ((??%?) → ?); #Heq destruct |
---|
713 | @conj |
---|
714 | [ >unfold_low_bound whd in match (update_block ?????); |
---|
715 | >(neq_block_eq_block_false … Hneq) @refl |
---|
716 | | >unfold_high_bound whd in match (update_block ?????); |
---|
717 | >(neq_block_eq_block_false … Hneq) @refl |
---|
718 | ] qed. |
---|
719 | |
---|
720 | (* A valid pointer stays valid after an alloc *) |
---|
721 | |
---|
722 | lemma alloc_valid_pointer_conservation : |
---|
723 | ∀m,m',z1,z2,(*r,*)new_block. |
---|
724 | alloc m z1 z2 (*r*) = 〈m',new_block〉 → |
---|
725 | ∀p. (pblock p) ≠ new_block → |
---|
726 | valid_pointer m' p = true → |
---|
727 | valid_pointer m p = true. |
---|
728 | #m #m' #z1 #z2 (*#r*) #new_block |
---|
729 | cases m #cont #next #Hnext |
---|
730 | whd in ⊢ ((??%%) → ?); |
---|
731 | #Heq destruct (Heq) * #b #o #Hneq #Hvalid |
---|
732 | @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) |
---|
733 | -Hvalid |
---|
734 | * * #Hblock_id |
---|
735 | >unfold_low_bound >unfold_high_bound |
---|
736 | >unfold_low_bound >unfold_high_bound |
---|
737 | whd in match (update_block ?????); |
---|
738 | whd in match (update_block ?????); |
---|
739 | cut (b ≠ (mk_block (*r*) next)) |
---|
740 | [ @(eq_block_elim … b (mk_block (*r*) next)) #H destruct try // |
---|
741 | @False_ind |
---|
742 | @(absurd … (refl ??) Hneq) ] #Hneqb |
---|
743 | >(not_eq_block … Hneqb) normalize nodelta |
---|
744 | #HA #HB % [ % ] try assumption |
---|
745 | cases b in Hneqb Hneq Hblock_id; (* #r'*) #id * #Hnext_not_id #Hneq |
---|
746 | #Hlt cut (id ≤ next) |
---|
747 | [ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ] |
---|
748 | #Hle @Zle_split try @Hle % #Heq destruct |
---|
749 | @(absurd … (refl ??) Hneq) |
---|
750 | qed. |
---|
751 | |
---|
752 | (* Allocating a new zone produces a valid block. *) |
---|
753 | lemma alloc_valid_new_block : |
---|
754 | ∀m,m',z1,z2(*,r*),new_block. |
---|
755 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
756 | valid_block m' new_block. |
---|
757 | * #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *) |
---|
758 | whd in match (alloc ???(*?*)); whd in match (valid_block ??); |
---|
759 | #Halloc destruct (Halloc) /2/ |
---|
760 | qed. |
---|
761 | |
---|
762 | (* All data in a valid block is unchanged after an alloc. *) |
---|
763 | lemma alloc_beloadv_conservation : |
---|
764 | ∀m,m',block,offset,z1,z2,(*r,*)new_block. |
---|
765 | valid_block m block → |
---|
766 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
767 | beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset). |
---|
768 | * #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc |
---|
769 | whd in Halloc:(??%?); destruct (Halloc) |
---|
770 | whd in match (beloadv ??) in ⊢ (??%%); |
---|
771 | lapply (Zlt_to_Zltb_true … Hvalid) #Hlt |
---|
772 | >Hlt >(zlt_succ … Hlt) |
---|
773 | normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??); |
---|
774 | cut (eqZb (block_id block) next = false) |
---|
775 | [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq |
---|
776 | >Hneq @refl |
---|
777 | qed. |
---|
778 | |
---|
779 | (* Lift [alloc_beloadv_conservation] to loadn *) |
---|
780 | lemma alloc_loadn_conservation : |
---|
781 | ∀m,m',z1,z2,(*r,*)new_block. |
---|
782 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
783 | ∀n. ∀block,offset. |
---|
784 | valid_block m block → |
---|
785 | loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n. |
---|
786 | #m #m' #z1 #z2 (*#r*) #new_block #Halloc #n |
---|
787 | elim n try // |
---|
788 | #n' #Hind #block #offset #Hvalid_block |
---|
789 | whd in ⊢ (??%%); |
---|
790 | >(alloc_beloadv_conservation … Hvalid_block Halloc) |
---|
791 | cases (beloadv m' (mk_pointer block offset)) // |
---|
792 | #bev normalize nodelta |
---|
793 | whd in match (shift_pointer ???); >Hind try // |
---|
794 | qed. |
---|
795 | |
---|
796 | lemma alloc_load_value_of_type_conservation : |
---|
797 | ∀m,m',z1,z2(*,r*),new_block. |
---|
798 | alloc m z1 z2 (*r*) = 〈m', new_block〉 → |
---|
799 | ∀block,offset. |
---|
800 | valid_block m block → |
---|
801 | ∀ty. load_value_of_type ty m block offset = |
---|
802 | load_value_of_type ty m' block offset. |
---|
803 | #m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid |
---|
804 | #ty cases ty |
---|
805 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
806 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
807 | try // |
---|
808 | whd in match (load_value_of_type ????) in ⊢ (??%%); |
---|
809 | >(alloc_loadn_conservation … Halloc … Hvalid) @refl |
---|
810 | qed. |
---|
811 | |
---|
812 | (* Memory allocation in m2 preserves [memory_inj]. |
---|
813 | * This is lemma 66 from Leroy&Blazy. *) |
---|
814 | lemma alloc_memory_inj_m2 : |
---|
815 | ∀E:embedding. |
---|
816 | ∀m1,m2,m2',z1,z2(*,r*),new_block. |
---|
817 | ∀H:memory_inj E m1 m2. |
---|
818 | alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 → |
---|
819 | block_implementable_bv m2' new_block → |
---|
820 | memory_inj E m1 m2'. |
---|
821 | #E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl |
---|
822 | % |
---|
823 | [ whd |
---|
824 | #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload |
---|
825 | elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload) |
---|
826 | #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try // |
---|
827 | lapply (refl ? (access_mode ty)) |
---|
828 | cases ty in Hload_eq; |
---|
829 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
830 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
831 | #Hload normalize in ⊢ ((???%) → ?); #Haccess |
---|
832 | [ 1,6,7: normalize in Hload; destruct (Hload) |
---|
833 | | 2,3,8: |
---|
834 | lapply (load_by_value_success_valid_block … Haccess Hload) |
---|
835 | #Hvalid_block |
---|
836 | <(alloc_load_value_of_type_conservation … Halloc … Hvalid_block) |
---|
837 | assumption |
---|
838 | | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] |
---|
839 | | @(mi_freeblock … Hmemory_inj) |
---|
840 | | #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) |
---|
841 | elim m2 in Halloc; #contentmap #nextblock #Hnextblock |
---|
842 | elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc) |
---|
843 | whd in match (valid_pointer ??) in ⊢ (% → %); |
---|
844 | @Zltb_elim_Type0 |
---|
845 | [ 2: normalize #_ #Habsurd destruct (Habsurd) ] |
---|
846 | #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ] |
---|
847 | #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %); |
---|
848 | whd in match (high_bound ??) in ⊢ (% → %); |
---|
849 | whd in match (update_block ?????); |
---|
850 | whd in match (eq_block ??); |
---|
851 | cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ] |
---|
852 | #Hbid_neq >Hbid_neq #H @H |
---|
853 | (* cases (eq_region br' r) normalize #H @H*) |
---|
854 | | #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H |
---|
855 | @(alloc_valid_block_conservation … Halloc … H) |
---|
856 | | @(mi_region … Hmemory_inj) |
---|
857 | | @(mi_nonalias … Hmemory_inj) |
---|
858 | | #b lapply (mi_nowrap … Hmemory_inj b) |
---|
859 | whd in ⊢ (% → %); |
---|
860 | lapply (mi_nodangling … Hmemory_inj b) |
---|
861 | cases (E b) normalize nodelta try // |
---|
862 | * #B #OFF normalize nodelta #Hguard |
---|
863 | * * #H1 #H2 #Hinbounds @conj try @conj try assumption |
---|
864 | @(eq_block_elim … (mk_block new_block) B) |
---|
865 | [ #H <H assumption |
---|
866 | | #H cases m2 in Halloc H2; #contents #nextblock #notnull |
---|
867 | whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) * |
---|
868 | >unfold_low_bound >unfold_high_bound #HA #HB |
---|
869 | @conj |
---|
870 | >unfold_low_bound >unfold_high_bound |
---|
871 | whd in match (update_block ?????); |
---|
872 | >(not_eq_block … (sym_neq ??? H)) normalize nodelta |
---|
873 | try assumption ] |
---|
874 | ] qed. |
---|
875 | |
---|
876 | (* Allocating in m1 such that the resulting block has no image in m2 preserves |
---|
877 | the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as |
---|
878 | in Blazy & Leroy. Notice that we must consider blocks with different regions but |
---|
879 | same id as equal. *) |
---|
880 | lemma alloc_memory_inj_m1 : |
---|
881 | ∀E:embedding. |
---|
882 | ∀m1,m2,m1',z1,z2,(*r,*)new_block. |
---|
883 | ∀H:memory_inj E m1 m2. |
---|
884 | alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 → |
---|
885 | memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧ |
---|
886 | embedding_compatible E (λx. if eq_block new_block x then None ? else E x). |
---|
887 | #E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc |
---|
888 | cut (E new_block = None ?) |
---|
889 | [ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?); |
---|
890 | #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] |
---|
891 | #Hempty |
---|
892 | cut (embedding_compatible E |
---|
893 | (λx. |
---|
894 | if eq_block new_block x |
---|
895 | then None (block×offset) |
---|
896 | else E x)) |
---|
897 | [ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ] |
---|
898 | #Hembedding_compatible @conj try assumption |
---|
899 | % |
---|
900 | [ whd #b1 #off1 #b2 #off2 #ty #v1 |
---|
901 | @(eq_block_elim … b1 new_block) |
---|
902 | [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta |
---|
903 | #Habsurd destruct ] |
---|
904 | #Hneq #Hvalid |
---|
905 | whd in ⊢ ((??%?) → ?); |
---|
906 | @(eq_block_elim … new_block b1) |
---|
907 | normalize nodelta |
---|
908 | [ #Heq #Habsurd destruct (Habsurd) ] |
---|
909 | #Hneq_id |
---|
910 | #Hembed #Hload |
---|
911 | lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) (sym_neq ??? Hneq_id) Hvalid) |
---|
912 | #Hvalid' |
---|
913 | cut (valid_block m1 b1) |
---|
914 | [ cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block #_ #_ @Hvalid_block ] |
---|
915 | #Hvalid_block |
---|
916 | lapply (alloc_load_value_of_type_conservation … Halloc … off1 … Hvalid_block ty) |
---|
917 | #Heq <Heq in Hload; #Hload |
---|
918 | lapply (mi_inj … Hinj … Hvalid' … Hembed … Hload) * #v2 * #Hload2 #Hveq2 |
---|
919 | %{v2} @conj try assumption |
---|
920 | @(embedding_compatibility_value_eq … Hveq2) assumption |
---|
921 | | #b #Hnot_valid @(eq_block_elim … new_block b) |
---|
922 | normalize nodelta |
---|
923 | [ #Heq @refl |
---|
924 | | #Hneq @(mi_freeblock … Hinj) % #Hvalid cases Hnot_valid #H @H |
---|
925 | @(alloc_valid_block_conservation … Halloc) assumption ] |
---|
926 | | #p #p' lapply (mi_valid_pointers … Hinj p p') |
---|
927 | cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1' |
---|
928 | whd in ⊢ ((??%%) → ?); |
---|
929 | @(eq_block_elim … new_block b) normalize nodelta |
---|
930 | [ #Heq #Habsurd destruct ] |
---|
931 | #Hneq #Hembed |
---|
932 | lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b o) (sym_neq ??? Hneq) Hvalid1') |
---|
933 | #Hvalid1 |
---|
934 | @(Hvalidptr Hvalid1 Hembed) |
---|
935 | | #b #b' #o' @(eq_block_elim … new_block b) |
---|
936 | [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
937 | normalize nodelta #Henq |
---|
938 | @(mi_nodangling … Hinj) |
---|
939 | | #b #b' #o' @(eq_block_elim … new_block b) |
---|
940 | [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
941 | #Hneq @(mi_region … Hinj) |
---|
942 | | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq |
---|
943 | @(eq_block_elim … new_block b1) |
---|
944 | normalize nodelta |
---|
945 | [ #Heq #Habsurd destruct (Habsurd) ] |
---|
946 | #Hneq1 #Hembed1 |
---|
947 | @(eq_block_elim … new_block b2) |
---|
948 | normalize nodelta |
---|
949 | [ #Heq #Habsurd destruct (Habsurd) ] |
---|
950 | #Hneq2 #Hembed2 |
---|
951 | @(eq_block_elim … b1' b2') normalize nodelta try // |
---|
952 | #Heq |
---|
953 | lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq |
---|
954 | >eq_block_b_b normalize nodelta |
---|
955 | cases m1 in Halloc; #contents #next #Hnext |
---|
956 | >unfold_high_bound >unfold_low_bound |
---|
957 | >unfold_high_bound >unfold_low_bound |
---|
958 | >unfold_high_bound >unfold_low_bound |
---|
959 | >unfold_high_bound >unfold_low_bound |
---|
960 | whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq) |
---|
961 | lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1)) |
---|
962 | lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2)) |
---|
963 | #Heq_block_2 |
---|
964 | #Heq_block_1 |
---|
965 | * [ * [ * | ] | ] |
---|
966 | whd in match (update_block ?????); |
---|
967 | >Heq_block_1 normalize nodelta |
---|
968 | whd in match (update_block ?????); |
---|
969 | >Heq_block_2 normalize nodelta |
---|
970 | #H |
---|
971 | try /4 by or_introl, or_intror, conj/ |
---|
972 | [ %1 %2 whd whd in H; |
---|
973 | >unfold_high_bound |
---|
974 | whd in match (update_block ?????); |
---|
975 | >unfold_low_bound |
---|
976 | whd in match (update_block ?????); |
---|
977 | >Heq_block_1 normalize nodelta @H |
---|
978 | | %2 whd whd in H; |
---|
979 | >unfold_high_bound |
---|
980 | whd in match (update_block ?????); |
---|
981 | >unfold_low_bound |
---|
982 | whd in match (update_block ?????); |
---|
983 | >Heq_block_1 >Heq_block_2 @H |
---|
984 | ] |
---|
985 | | #b whd @(eq_block_elim … new_block b) normalize nodelta try // |
---|
986 | #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?); |
---|
987 | cases (E b) normalize nodelta try // |
---|
988 | * #bb #oo normalize nodelta |
---|
989 | * * * #HA #HB * #HC #HD #HE @conj try @conj |
---|
990 | try @conj |
---|
991 | lapply HE -HE |
---|
992 | lapply HD -HD |
---|
993 | lapply HC -HC |
---|
994 | lapply HB -HB |
---|
995 | lapply HA -HA |
---|
996 | >unfold_low_bound >unfold_low_bound [ >unfold_low_bound ] |
---|
997 | >unfold_high_bound >unfold_high_bound [ 2,5: >unfold_high_bound ] |
---|
998 | cases m1 in Halloc; #cont #next #Hnext |
---|
999 | whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try // |
---|
1000 | whd in match (update_block ?????); |
---|
1001 | cut (eq_block b (mk_block next) = false) |
---|
1002 | [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq) |
---|
1003 | | 2,4,6: #Heq_block >Heq_block // ] |
---|
1004 | ] qed. |
---|
1005 | |
---|
1006 | (* loading by-value from a freshly allocated block yields either an undef value or |
---|
1007 | * None. *) |
---|
1008 | lemma load_by_value_after_alloc_undef : |
---|
1009 | ∀m,m',z1,z2,b. |
---|
1010 | alloc m z1 z2 = 〈m', b〉 → |
---|
1011 | ∀ty. access_mode ty = By_value (typ_of_type ty) → |
---|
1012 | ∀off. load_value_of_type ty m' b off = Some ? Vundef ∨ |
---|
1013 | load_value_of_type ty m' b off = None ?. |
---|
1014 | #m #m' #z1 #z2 (* * #br #bid *) #b |
---|
1015 | cases m #contents #nextblock #Hnext |
---|
1016 | whd in ⊢ ((??%?) → ?); |
---|
1017 | #Heq destruct (Heq) |
---|
1018 | #ty cases ty |
---|
1019 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1020 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1021 | whd in ⊢ ((??%?) → ?); |
---|
1022 | #Heq destruct (Heq) |
---|
1023 | #off |
---|
1024 | whd in match (load_value_of_type ????); |
---|
1025 | (* We can't generalize over the typesize, sadly. We thus perform three identical inductions. |
---|
1026 | * Another solution would be to provide an ad-hoc lemma, but the goal is too ugly for that. *) |
---|
1027 | [ lapply off -off |
---|
1028 | generalize in match (typesize ?); #tsz |
---|
1029 | | lapply off -off |
---|
1030 | generalize in match (typesize ?); #tsz |
---|
1031 | | lapply off -off |
---|
1032 | generalize in match (typesize ?); #tsz |
---|
1033 | ] |
---|
1034 | elim tsz |
---|
1035 | [ 1,3,5: #off whd in match (loadn ???); normalize nodelta %1 @refl |
---|
1036 | | *: #tsz' #Hind #off |
---|
1037 | whd in match (loadn ???); |
---|
1038 | whd in match (beloadv ??); |
---|
1039 | cases (Zltb ??) normalize nodelta try /1 by or_intror/ |
---|
1040 | cases (Zleb ??) normalize nodelta try /1 by or_intror/ |
---|
1041 | >andb_lsimpl_true |
---|
1042 | cases (Zltb ??); normalize nodelta try /1 by or_intror/ |
---|
1043 | whd in match (update_block ?????); |
---|
1044 | >eq_block_b_b normalize nodelta |
---|
1045 | cases (Hind (shift_offset 2 off (bitvector_of_nat 2 1))) |
---|
1046 | cases (loadn ???) normalize nodelta try // |
---|
1047 | #bevals #Heq %1 whd in match (be_to_fe_value ??); |
---|
1048 | try @refl ] |
---|
1049 | qed. |
---|
1050 | |
---|
1051 | |
---|
1052 | (* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order |
---|
1053 | * to prove the equivalent of lemma 68 of L&B, we need to provide an additional |
---|
1054 | * property of the target memory: the /target/ portion of memory we are going to map a block |
---|
1055 | * to must only contains BVundef (whereas in CompCert, the fact that the source block |
---|
1056 | * contains BVundefs is enough to proceed). |
---|
1057 | * |
---|
1058 | * The following definition expresses the fact that a portion of memory [z1; z2] contains only |
---|
1059 | * BVundefs. |
---|
1060 | * Note that the bounds are /inclusive/. We do not check for their validity. *) |
---|
1061 | definition undef_memory_zone : mem → block → Z → Z → Prop ≝ |
---|
1062 | λm,b,z1,z2. |
---|
1063 | ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef. |
---|
1064 | |
---|
1065 | (* Explictly stating the properties of alloc. *) |
---|
1066 | lemma alloc_properties : |
---|
1067 | ∀m,m',z1,z2(*,r*),b. |
---|
1068 | alloc m z1 z2 (* r *) = 〈m',b〉 → |
---|
1069 | low_bound m' b = z1 ∧ |
---|
1070 | high_bound m' b = z2 ∧ |
---|
1071 | undef_memory_zone m' b z1 z2. |
---|
1072 | #m #m' #z1 #z2 * (* #br *) #bid |
---|
1073 | cases m #contents #next #Hnext |
---|
1074 | whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) |
---|
1075 | >unfold_low_bound >unfold_high_bound |
---|
1076 | @conj try @conj |
---|
1077 | /2 by refl, pair_destruct_2/ |
---|
1078 | whd |
---|
1079 | #i #H1 #H2 whd in match (update_block ?????); |
---|
1080 | >eq_block_b_b normalize nodelta @refl |
---|
1081 | qed. |
---|
1082 | |
---|
1083 | |
---|
1084 | (* Embed a fresh block inside an unmapped portion of the target block. |
---|
1085 | * This is the equivalent of lemma 68 of Leroy&Blazy. |
---|
1086 | * Compared to L&B, an additional "undef_memory_zone" proof object must be provided. |
---|
1087 | * We also constrain the memory bounds of the new block to be bitvector-implementable, |
---|
1088 | * otherwise we can't prove that addition commutes with conversions between Z and |
---|
1089 | * bitvectors. |
---|
1090 | *) |
---|
1091 | lemma alloc_memory_inj_m1_to_m2 : |
---|
1092 | ∀E:embedding. |
---|
1093 | ∀m1,m2,m1':mem. |
---|
1094 | ∀z1,z2:Z. |
---|
1095 | ∀target,new_block. |
---|
1096 | ∀delta:offset. |
---|
1097 | valid_block m2 target → |
---|
1098 | block_implementable_bv m1' new_block → |
---|
1099 | block_implementable_bv m2 target → |
---|
1100 | block_region new_block = block_region target → |
---|
1101 | (high_bound m1' new_block) + (Zoo delta) < Z_two_power_nat 16 → |
---|
1102 | alloc m1 z1 z2 = 〈m1', new_block〉 → |
---|
1103 | low_bound m2 target ≤ z1 + Zoo delta → |
---|
1104 | z2 + Zoo delta ≤ high_bound m2 target → |
---|
1105 | undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) → |
---|
1106 | (∀b,delta'. b ≠ new_block → |
---|
1107 | E b = Some ? 〈target, delta'〉 → |
---|
1108 | high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ |
---|
1109 | z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → |
---|
1110 | memory_inj E m1 m2 → |
---|
1111 | memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2. |
---|
1112 | #E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #target (* * * #newr *) #new_block (* * *) #delta |
---|
1113 | #Hvalid #Himpl1 #Himpl2 #Hregion #Hno_overflow #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj |
---|
1114 | cut (E new_block = (None ?)) |
---|
1115 | [ @(mi_freeblock ??? Hinj new_block) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj |
---|
1116 | whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] |
---|
1117 | #Hnew_not_mapped |
---|
1118 | cut (embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x)) |
---|
1119 | [ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 assumption ] |
---|
1120 | #Hembedding_compatible |
---|
1121 | % |
---|
1122 | [ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload |
---|
1123 | @(eq_block_elim … new_block b1) |
---|
1124 | [ 2: (* we do not load from the newly allocated block *) |
---|
1125 | #Hneq |
---|
1126 | (* prove that we can equivalently load from the memory before alloc *) |
---|
1127 | cases (some_inversion ????? Hembed) * #target' #delta' |
---|
1128 | >(neq_block_eq_block_false … Hneq) normalize nodelta |
---|
1129 | * #Hembed #Heq destruct (Heq) |
---|
1130 | cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh |
---|
1131 | lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block') |
---|
1132 | #Hvalid_block |
---|
1133 | lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty) |
---|
1134 | #Heq_load <Heq_load in Hload; #Hload |
---|
1135 | lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid') |
---|
1136 | #Hvalid_ptr |
---|
1137 | lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload) |
---|
1138 | [ whd in ⊢ (??%?); >Hembed @refl ] |
---|
1139 | (* conclude *) |
---|
1140 | * #v2 * #Hload2 #Hvalue_eq %{v2} @conj |
---|
1141 | [ @Hload2 |
---|
1142 | | @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ] |
---|
1143 | | 1: (* we allegedly performed a load from a block with the same id as |
---|
1144 | * the newly allocated block (which by def. of alloc contains only BVundefs) *) |
---|
1145 | #Heq destruct (Heq) |
---|
1146 | whd in Hembed:(??%?); >eq_block_b_b in Hembed; normalize nodelta |
---|
1147 | #Heq_ptr |
---|
1148 | (* cull out all boring cases *) |
---|
1149 | lapply Hload -Hload cases ty |
---|
1150 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1151 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1152 | [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) |
---|
1153 | | 4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq) |
---|
1154 | %{(Vptr (mk_pointer b2 (offset_plus off1 delta)))} |
---|
1155 | @conj |
---|
1156 | [ 1,3: @refl |
---|
1157 | | *: %4 whd in ⊢ (??%?); >eq_block_b_b @refl ] ] |
---|
1158 | (* Now: load-by-value cases. Outcome is either None or Undef. *) |
---|
1159 | lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 Halloc) |
---|
1160 | #Hload_eq |
---|
1161 | [ lapply (Hload_eq (Tint sz sg) (refl ??) off1) |
---|
1162 | | lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1) |
---|
1163 | | lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ] |
---|
1164 | * |
---|
1165 | (* None case: absurd *) |
---|
1166 | [ 2,4,6: #Hload >Hload #Habsurd destruct (Habsurd) ] |
---|
1167 | #Hload >Hload #Heq destruct (Heq) %{Vundef} |
---|
1168 | @conj try // destruct (Heq_ptr) |
---|
1169 | (* prove the validity of this pointer in order tu unfold load *) |
---|
1170 | cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true) |
---|
1171 | [ 1,3,5: @valid_pointer_of_Prop @conj try @conj |
---|
1172 | [ 1,4,7: assumption |
---|
1173 | | 2,5,8: >unfold_low_bound |
---|
1174 | lapply (alloc_properties … Halloc) * * |
---|
1175 | >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef |
---|
1176 | lapply (valid_pointer_to_Prop … Hvalid') * * |
---|
1177 | #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh' |
---|
1178 | #Hle_low #Hlt_high destruct |
---|
1179 | cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta) |
---|
1180 | [ 1,3,5: >Z_addition_bv_commute try @refl |
---|
1181 | @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l |
---|
1182 | @Hlt_high |
---|
1183 | ] |
---|
1184 | #Hsum_split |
---|
1185 | cut (low (blocks m1' b1) + Zoo delta ≤ Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta))) |
---|
1186 | [ 1,3,5: >Hsum_split @monotonic_Zle_Zplus_l assumption ] |
---|
1187 | @(transitive_Zle … Hlow) |
---|
1188 | | 3,6,9: >unfold_high_bound |
---|
1189 | lapply (alloc_properties … Halloc) * * |
---|
1190 | >unfold_low_bound >unfold_high_bound #Hlow' #Hhigh' #Hundef |
---|
1191 | lapply (valid_pointer_to_Prop … Hvalid') * * |
---|
1192 | #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow' >Hhigh' |
---|
1193 | #Hle_low #Hlt_high destruct |
---|
1194 | cut (Z_of_unsigned_bitvector ? (offv (offset_plus off1 delta)) = Zoo off1 + Zoo delta) |
---|
1195 | [ 1,3,5: >Z_addition_bv_commute try @refl |
---|
1196 | @(transitive_Zlt ???? Hno_overflow) @monotonic_Zlt_Zplus_l |
---|
1197 | @Hlt_high |
---|
1198 | ] |
---|
1199 | #Hsum_split |
---|
1200 | cut (Z_of_unsigned_bitvector offset_size (offv (offset_plus off1 delta)) < high (blocks m1' b1) + Zoo delta) |
---|
1201 | [ 1,3,5: >Hsum_split @monotonic_Zlt_Zplus_l assumption ] |
---|
1202 | #Hlt_aux @(Zlt_to_Zle_to_Zlt … Hlt_aux Hhigh) |
---|
1203 | ] |
---|
1204 | ] |
---|
1205 | -Hno_interference |
---|
1206 | #Hvalid_ptr2 |
---|
1207 | (* reformulate the goals in an induction friendly way *) |
---|
1208 | [ cut (∃bvals. loadn m2 |
---|
1209 | (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta)))) |
---|
1210 | (typesize (typ_of_type (Tint sz sg))) = Some ? bvals ∧ |
---|
1211 | (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef))) |
---|
1212 | [ 2: * #bvals * #Hloadn * #Heq destruct (Heq) |
---|
1213 | whd in match (load_value_of_type ????); |
---|
1214 | >Hloadn normalize nodelta try @refl |
---|
1215 | cases bvals in Heq; try // |
---|
1216 | #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?); |
---|
1217 | #Heq destruct (Heq) try @refl ] |
---|
1218 | | cut (∃bvals. loadn m2 |
---|
1219 | (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta)))) |
---|
1220 | (typesize (typ_of_type (Tpointer ptr_ty))) = Some ? bvals ∧ |
---|
1221 | (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef))) |
---|
1222 | [ 2: * #bvals * #Hloadn * #Heq destruct (Heq) |
---|
1223 | whd in match (load_value_of_type ????); |
---|
1224 | >Hloadn normalize nodelta try @refl |
---|
1225 | cases bvals in Heq; try // |
---|
1226 | #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?); |
---|
1227 | #Heq destruct (Heq) try @refl ] |
---|
1228 | | cut (∃bvals. loadn m2 |
---|
1229 | (mk_pointer b2 (mk_offset (addition_n ? (offv off1) (offv delta)))) |
---|
1230 | (typesize (typ_of_type (Tcomp_ptr id))) = Some ? bvals ∧ |
---|
1231 | (bvals = [ ] ∨ (option_hd … bvals = Some ? BVundef))) |
---|
1232 | [ 2: * #bvals * #Hloadn * #Heq destruct (Heq) |
---|
1233 | whd in match (load_value_of_type ????); |
---|
1234 | >Hloadn normalize nodelta try @refl |
---|
1235 | cases bvals in Heq; try // |
---|
1236 | #hd #tl normalize nodelta whd in ⊢ ((??%?) → ?); |
---|
1237 | #Heq destruct (Heq) try @refl ] |
---|
1238 | ] |
---|
1239 | cases (valid_pointer_to_Prop … Hvalid') -Hvalid' * #HA #HB #HC |
---|
1240 | cases (valid_pointer_to_Prop … Hvalid_ptr2) -Hvalid_ptr2 * #HD |
---|
1241 | whd in match (offset_plus ??); #HE #HF |
---|
1242 | cases Himpl1 cases Himpl2 -Himpl1 -Himpl2 |
---|
1243 | >unfold_low_bound >unfold_low_bound >unfold_high_bound >unfold_high_bound |
---|
1244 | * #HG #HH * #HI #HJ * #HK #HL * #HM #HN |
---|
1245 | lapply (alloc_properties … Halloc) * * #HO #HP #Hsrc_undef destruct (HO HP) |
---|
1246 | cases (some_inversion ????? Hload) |
---|
1247 | #bevals * |
---|
1248 | #Hloadn #_ lapply Hloadn -Hloadn |
---|
1249 | whd in match (typesize ?); |
---|
1250 | [ generalize in match (S (pred_size_intsize sz)); |
---|
1251 | | generalize in match (S (S O)); |
---|
1252 | | generalize in match (S (S O)); ] |
---|
1253 | #typesize |
---|
1254 | lapply HE lapply HF lapply HB lapply HC |
---|
1255 | -HE -HF -HB -HC |
---|
1256 | lapply bevals |
---|
1257 | lapply off1 |
---|
1258 | elim typesize |
---|
1259 | [ 1,3,5: |
---|
1260 | #off #bevals #HC #HB #HF #HE #_ %{[ ]} @conj try @refl |
---|
1261 | %1 @refl |
---|
1262 | | *: |
---|
1263 | #n #Hind #off #bevals #HC #HB #HF #HE #Hloadn |
---|
1264 | cases (some_inversion ????? Hloadn) -Hloadn |
---|
1265 | #bval1 * #Hbeloadv_eq #Hloadn |
---|
1266 | cases (some_inversion ????? Hloadn) -Hloadn |
---|
1267 | whd in match (shift_pointer ???); |
---|
1268 | whd in match (shift_offset ???); |
---|
1269 | #bevals1 * #Hloadn #Hbevals' |
---|
1270 | whd in match (loadn ???); |
---|
1271 | whd in match (beloadv ??); |
---|
1272 | >(Zlt_to_Zltb_true … HD) normalize nodelta |
---|
1273 | >(Zle_to_Zleb_true … HE) |
---|
1274 | >(Zlt_to_Zltb_true … HF) normalize nodelta |
---|
1275 | lapply (Hundef_zone (Z_of_unsigned_bitvector ? (addition_n offset_size (offv off) (offv delta))) ??) |
---|
1276 | [ 1,4,7: >Z_addition_bv_commute |
---|
1277 | [ 2,4,6: @(transitive_Zlt … Hno_overflow) |
---|
1278 | @(monotonic_Zlt_Zplus_l) assumption |
---|
1279 | | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ] |
---|
1280 | | 2,5,8: >Z_addition_bv_commute |
---|
1281 | [ 2,4,6: @(transitive_Zlt … Hno_overflow) |
---|
1282 | @(monotonic_Zlt_Zplus_l) assumption |
---|
1283 | | 1,3,5: @(monotonic_Zle_Zplus_l) /3 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle/ ] |
---|
1284 | ] |
---|
1285 | #Hcontents_undef |
---|
1286 | cases n in Hind Hloadn; |
---|
1287 | [ 1,3,5: #_ normalize in match (loadn ???); normalize nodelta #Heq destruct |
---|
1288 | >Hcontents_undef %{[BVundef]} @conj try @refl %2 @refl ] |
---|
1289 | #n' #Hind #Hloadn |
---|
1290 | lapply Hloadn #Hloadn' |
---|
1291 | cases (some_inversion ????? Hloadn') -Hloadn' |
---|
1292 | #bval * whd in match (beloadv ??); |
---|
1293 | >(Zlt_to_Zltb_true … HA) normalize nodelta #Hbeloadv |
---|
1294 | cases (if_opt_inversion ???? Hbeloadv) -Hbeloadv #Hbounds |
---|
1295 | cases (andb_inversion … Hbounds) -Hbounds #Hle1 #Hlt1 #Hcontents1 #_ |
---|
1296 | lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ????) |
---|
1297 | (* lapply (Hind (mk_offset (addition_n ? (offv off) (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) bevals1 ???? Hloadn) *) |
---|
1298 | [ 1,6,11: |
---|
1299 | @(transitive_Zle ??? HE) |
---|
1300 | <associative_addition_n |
---|
1301 | >(commutative_addition_n ? (sign_ext ???) (offv delta)) |
---|
1302 | >associative_addition_n |
---|
1303 | >(Z_addition_bv_commute ?? (sign_ext ???)) |
---|
1304 | [ 2,4,6: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???)); |
---|
1305 | >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O |
---|
1306 | @(Zle_to_Zlt_to_Zlt … HJ) @Zlt_to_Zle @HF |
---|
1307 | | 1,3,5: normalize in match (Z_of_unsigned_bitvector ? (sign_ext ???)); |
---|
1308 | >(sym_Zplus ? (pos one)) <Zsucc_Zplus_pos_O @Zsucc_le |
---|
1309 | ] |
---|
1310 | | 2,7,12: |
---|
1311 | @(Zlt_to_Zle_to_Zlt ??? ? Hhigh) |
---|
1312 | >Z_addition_bv_commute |
---|
1313 | [ 2,4,6: @(transitive_Zlt … Hno_overflow) |
---|
1314 | @(monotonic_Zlt_Zplus_l) @(Zltb_true_to_Zlt … Hlt1) |
---|
1315 | | 1,3,5: @monotonic_Zlt_Zplus_l @(Zltb_true_to_Zlt … Hlt1) ] |
---|
1316 | | 3,8,13: |
---|
1317 | @(Zleb_true_to_Zle … Hle1) |
---|
1318 | | 4,9,14: |
---|
1319 | @(Zltb_true_to_Zlt … Hlt1) |
---|
1320 | ] |
---|
1321 | -Hind #Hind lapply (Hind Hloadn) |
---|
1322 | * #bevals2 * #Hloadn2 #Hbe_to_fe |
---|
1323 | whd in match (shift_pointer ???); |
---|
1324 | whd in match (shift_offset ???); |
---|
1325 | cases Hbe_to_fe |
---|
1326 | [ 1,3,5: #Heq destruct (Heq) |
---|
1327 | %{(contents (blocks m2 b2) |
---|
1328 | (Z_of_unsigned_bitvector offset_size |
---|
1329 | (addition_n offset_size (offv off) (offv delta))) |
---|
1330 | ::[ ])} |
---|
1331 | <associative_addition_n |
---|
1332 | >(commutative_addition_n ? (offv delta)) |
---|
1333 | >associative_addition_n |
---|
1334 | >Hloadn2 normalize nodelta @conj try @refl %2 |
---|
1335 | >Hcontents_undef @refl |
---|
1336 | | *: #Hhd_empty |
---|
1337 | %{(contents (blocks m2 b2) |
---|
1338 | (Z_of_unsigned_bitvector offset_size |
---|
1339 | (addition_n offset_size (offv off) (offv delta))) |
---|
1340 | :: bevals2)} |
---|
1341 | <associative_addition_n |
---|
1342 | >(commutative_addition_n ? (offv delta)) |
---|
1343 | >associative_addition_n |
---|
1344 | >Hloadn2 normalize nodelta @conj try @refl %2 |
---|
1345 | >Hcontents_undef @refl |
---|
1346 | ] |
---|
1347 | ] |
---|
1348 | ] |
---|
1349 | | #b lapply (alloc_valid_new_block … Halloc) @(eq_block_elim … new_block b) |
---|
1350 | [ #Heq destruct #Ha #Hb @False_ind @(absurd … Ha Hb) |
---|
1351 | | #Hneq #Hvalid_new #Hnot_valid normalize nodelta |
---|
1352 | cut (¬valid_block m1 b) |
---|
1353 | [ cases m1 in Halloc; #cont #next #Hnext |
---|
1354 | whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) |
---|
1355 | % #H cases Hnot_valid #H' @H' |
---|
1356 | whd whd in H; /2 by transitive_Zlt/ ] |
---|
1357 | @ (mi_freeblock … Hinj) ] |
---|
1358 | | * #blo #off #p' #Hvalid1 |
---|
1359 | @(eq_block_elim … new_block blo) |
---|
1360 | [ #Heq whd in match (pointer_translation ??); |
---|
1361 | destruct (Heq) >eq_block_b_b normalize nodelta |
---|
1362 | lapply (alloc_properties … Halloc) * * |
---|
1363 | #Hlow_eq #Hhigh_eq #Hundef destruct |
---|
1364 | cases (valid_pointer_to_Prop … Hvalid1) * |
---|
1365 | #Hvalid_block1 #Hlow1 #Hhigh1 |
---|
1366 | #Heq destruct (Heq) @valid_pointer_of_Prop |
---|
1367 | @conj try @conj |
---|
1368 | [ @Hvalid |
---|
1369 | | @(transitive_Zle … Hlow) |
---|
1370 | >Z_addition_bv_commute |
---|
1371 | [ @monotonic_Zle_Zplus_l assumption |
---|
1372 | | @(transitive_Zlt … Hno_overflow) |
---|
1373 | @monotonic_Zlt_Zplus_l assumption |
---|
1374 | ] |
---|
1375 | | @(Zlt_to_Zle_to_Zlt … Hhigh) |
---|
1376 | >Z_addition_bv_commute |
---|
1377 | [ @monotonic_Zlt_Zplus_l assumption |
---|
1378 | | @(transitive_Zlt … Hno_overflow) |
---|
1379 | @monotonic_Zlt_Zplus_l assumption |
---|
1380 | ] |
---|
1381 | ] |
---|
1382 | | #Hblocks_neq whd in match (pointer_translation ??); |
---|
1383 | >(neq_block_eq_block_false … Hblocks_neq) normalize nodelta |
---|
1384 | #Htranslate |
---|
1385 | lapply (mi_valid_pointers ??? Hinj (mk_pointer blo off) p' ?) |
---|
1386 | [ @(alloc_valid_pointer_conservation … Halloc … Hvalid1) @sym_neq assumption ] |
---|
1387 | #H @H |
---|
1388 | assumption |
---|
1389 | ] |
---|
1390 | | #b #b' #o' |
---|
1391 | @(eq_block_elim … new_block b) |
---|
1392 | [ #Heq destruct (Heq) normalize nodelta |
---|
1393 | #Heq destruct (Heq) @Hvalid |
---|
1394 | | #Hneq normalize nodelta |
---|
1395 | #Hembed |
---|
1396 | @(mi_nodangling ??? Hinj … Hembed) |
---|
1397 | ] |
---|
1398 | | #b #b' #o' |
---|
1399 | @(eq_block_elim … new_block b) |
---|
1400 | [ #Heq normalize nodelta #Heq' destruct (Heq Heq') |
---|
1401 | @Hregion |
---|
1402 | | #Hneq normalize nodelta #Hembed |
---|
1403 | @(mi_region … Hinj … Hembed) |
---|
1404 | ] |
---|
1405 | | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq |
---|
1406 | cases (alloc_properties … Halloc) * #Hlow1 #Hhigh1 #Hundef |
---|
1407 | @(eq_block_elim … new_block b1) |
---|
1408 | normalize nodelta |
---|
1409 | [ #Heq #Heq' destruct |
---|
1410 | >(neq_block_eq_block_false … Hneq) normalize nodelta |
---|
1411 | #Hembed |
---|
1412 | (* lapply (alloc_bounds_conservation … Halloc) … *) |
---|
1413 | @(eq_block_elim … b1' b2') normalize nodelta |
---|
1414 | [ #Heq destruct (Heq) |
---|
1415 | lapply (Hno_interference b2 ? (sym_neq ??? Hneq) Hembed) * |
---|
1416 | cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq)) #HA #HB |
---|
1417 | [ #H %1 %1 %2 |
---|
1418 | >HB @H |
---|
1419 | | #H %1 %1 %1 >HA @H ] |
---|
1420 | | #Hneq @I ] |
---|
1421 | | #Hneq' #Hembed |
---|
1422 | @(eq_block_elim … new_block b2) normalize nodelta |
---|
1423 | [ #Heq #Heq' destruct |
---|
1424 | @(eq_block_elim … b1' b2') normalize nodelta |
---|
1425 | [ #Heq destruct (Heq) |
---|
1426 | lapply (Hno_interference b1 ? Hneq Hembed) * |
---|
1427 | cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq')) #HA #HB |
---|
1428 | [ #H %1 %1 %1 |
---|
1429 | >HB @H |
---|
1430 | | #H %1 %1 %2 >HA @H ] |
---|
1431 | | #Hneq @I ] |
---|
1432 | | #Hneq'' #Hembed' |
---|
1433 | @(eq_block_elim … b1' b2') normalize nodelta |
---|
1434 | [ #Heq'' destruct (Heq'') |
---|
1435 | lapply (mi_nonalias … Hinj … Hneq … Hembed Hembed') |
---|
1436 | >eq_block_b_b normalize nodelta |
---|
1437 | cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq'')) |
---|
1438 | #HA #HB |
---|
1439 | cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq')) |
---|
1440 | #HC #HD |
---|
1441 | * [ * [ * | ] | ] |
---|
1442 | [ #Hle %1 %1 %1 >HD >HA @Hle |
---|
1443 | | #Hle %1 %1 %2 >HB >HC @Hle |
---|
1444 | | #Hempty %1 %2 whd in Hempty ⊢ %; >HD >HC |
---|
1445 | @Hempty |
---|
1446 | | #Hempty %2 whd in Hempty ⊢ %; >HB >HA @Hempty |
---|
1447 | ] |
---|
1448 | | #_ @I |
---|
1449 | ] |
---|
1450 | ] |
---|
1451 | ] |
---|
1452 | | #b whd |
---|
1453 | @(eq_block_elim … new_block b) |
---|
1454 | normalize nodelta |
---|
1455 | #Hneq destruct (Hneq) |
---|
1456 | [ @conj try @conj try assumption |
---|
1457 | | lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?); |
---|
1458 | cases (alloc_bounds_conservation … Halloc … (sym_neq ??? Hneq)) |
---|
1459 | #HA #HB |
---|
1460 | cases (E b) normalize nodelta try // |
---|
1461 | * #blo #off normalize nodelta * * #HA' #HB' #HC' |
---|
1462 | @conj try @conj whd in HA'; whd in HB'; |
---|
1463 | whd in match (block_implementable_bv ??); |
---|
1464 | [ 1,2: >HA >HB assumption |
---|
1465 | | *: >HB assumption ] |
---|
1466 | ] |
---|
1467 | ] qed. |
---|
1468 | |
---|
1469 | (* -------------------------------------- *) |
---|
1470 | (* Lemmas pertaining to [free] *) |
---|
1471 | |
---|
1472 | (* Lemma 46 by Leroy&Blazy *) |
---|
1473 | lemma free_load_sim_ptr_m1 : |
---|
1474 | ∀E:embedding. |
---|
1475 | ∀m1,m2,m1'. |
---|
1476 | load_sim_ptr E m1 m2 → |
---|
1477 | ∀b. free m1 b = m1' → |
---|
1478 | load_sim_ptr E m1' m2. |
---|
1479 | #E #m1 #m2 #m1' #Hinj #b #Hfree |
---|
1480 | whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans |
---|
1481 | cases ty |
---|
1482 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1483 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1484 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) |
---|
1485 | normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl |
---|
1486 | %4 @Htrans ] |
---|
1487 | #Hload <Hfree in Hload; #Hload lapply (load_value_of_type_free_load_value_of_type … Hload) |
---|
1488 | #Hload' @(Hinj … Hload') // |
---|
1489 | <Hfree in Hvalid; @valid_free_to_valid |
---|
1490 | qed. |
---|
1491 | |
---|
1492 | (* lemma 47 of L&B *) |
---|
1493 | |
---|
1494 | lemma free_loadn_sim_ptr_m2 : |
---|
1495 | ∀sz,m,b,b',o,res. |
---|
1496 | b ≠ b' → |
---|
1497 | loadn m (mk_pointer b' o) sz = Some ? res → |
---|
1498 | loadn (free m b) (mk_pointer b' o) sz = Some ? res. |
---|
1499 | #sz |
---|
1500 | elim sz |
---|
1501 | [ normalize // |
---|
1502 | | #sz' #Hind #m #b #b' #o #res #Hneq whd in ⊢ ((??%?) → (??%?)); |
---|
1503 | #H cases (some_inversion ????? H) -H #beres * |
---|
1504 | #Hbeloadv #Hloadn |
---|
1505 | lapply (beloadv_free_beloadv2 m b ??? Hbeloadv) |
---|
1506 | [ @sym_neq @Hneq ] |
---|
1507 | #Hbeloadv' >Hbeloadv' normalize nodelta |
---|
1508 | cases (some_inversion ????? Hloadn) -Hloadn #bevals * #Hloadn |
---|
1509 | #Heq destruct (Heq) |
---|
1510 | >(Hind … Hneq Hloadn) normalize nodelta @refl |
---|
1511 | ] qed. |
---|
1512 | |
---|
1513 | lemma free_load_sim_ptr_m2 : |
---|
1514 | ∀E:embedding. |
---|
1515 | ∀m1,m2,m2'. |
---|
1516 | load_sim_ptr E m1 m2 → |
---|
1517 | ∀b. free m2 b = m2' → |
---|
1518 | (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → |
---|
1519 | load_sim_ptr E m1 m2'. |
---|
1520 | #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped |
---|
1521 | whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Htrans |
---|
1522 | cases ty |
---|
1523 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1524 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1525 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) |
---|
1526 | normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl |
---|
1527 | %4 @Htrans ] |
---|
1528 | lapply Htrans -Htrans lapply Hsim -Hsim lapply Hfree -Hfree |
---|
1529 | cases m2 #contents2 #next2 #Hnext2 |
---|
1530 | whd in ⊢ ((??%?) → ?); #Hm2' destruct |
---|
1531 | #Hsim #Htrans |
---|
1532 | cases (some_inversion ????? Htrans) * #b2' #off2' * #Hembed normalize nodelta |
---|
1533 | #Heq destruct (Heq) #Hload |
---|
1534 | lapply (Hsim … Hvalid … Htrans … Hload) |
---|
1535 | * #v2' * #Hload_before_free #Hvalue_eq |
---|
1536 | @(eq_block_elim … b2 b) |
---|
1537 | [ 1,3,5: #Heq destruct |
---|
1538 | lapply (Hunmapped b1 off2' Hembed) * |
---|
1539 | [ 1,3,5: #Hnot_valid lapply (valid_pointer_to_Prop … Hvalid) |
---|
1540 | -Hvalid whd in match (valid_block ??) in Hnot_valid; |
---|
1541 | * * #Hvalid #_ #_ @False_ind |
---|
1542 | cases Hnot_valid #H @H @Hvalid |
---|
1543 | | *: whd in ⊢ (% → ?); #Hempty |
---|
1544 | lapply (valid_pointer_to_Prop … Hvalid) |
---|
1545 | -Hvalid * * #_ #Hlow #Hhigh |
---|
1546 | cut ((low_bound m1 b1 < high_bound m1 b1)) |
---|
1547 | [ 1,3,5: /2 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle_to_Zlt/ ] |
---|
1548 | #Hnonempty @False_ind -Hlow -Hhigh |
---|
1549 | lapply (Zlt_to_Zle_to_Zlt … Hnonempty Hempty) |
---|
1550 | #H cases (irreflexive_Zlt (low_bound m1 b1)) #H' @H' @H ] |
---|
1551 | | *: #Hneq %{v2'} @conj try assumption |
---|
1552 | whd in match (load_value_of_type ????) in Hload_before_free:(??%?) ⊢ (??%?); |
---|
1553 | cases (some_inversion ????? Hload_before_free) -Hload_before_free |
---|
1554 | #bevals * #Hloadn #Heq |
---|
1555 | >(free_loadn_sim_ptr_m2 … Hloadn) normalize nodelta |
---|
1556 | try assumption @sym_neq @Hneq |
---|
1557 | ] qed. |
---|
1558 | |
---|
1559 | lemma free_block_is_empty : |
---|
1560 | ∀m,m',b,b'. |
---|
1561 | block_region b = block_region b' → |
---|
1562 | block_is_empty m b → |
---|
1563 | free m b' = m' → |
---|
1564 | block_is_empty m' b. |
---|
1565 | * #contents #nextblock #Hpos |
---|
1566 | #m' #b #b' #Hregions_eq |
---|
1567 | #HA #HB normalize in HB; <HB whd |
---|
1568 | normalize >Hregions_eq cases (block_region b') normalize nodelta |
---|
1569 | @(eqZb_elim … (block_id b) (block_id b')) |
---|
1570 | [ 1,3: #Heq normalize nodelta // |
---|
1571 | | 2,4: #Hneq normalize nodelta @HA ] |
---|
1572 | qed. |
---|
1573 | |
---|
1574 | lemma high_bound_freed_block : |
---|
1575 | ∀m,b. high_bound (free m b) b = OZ. |
---|
1576 | #m #b normalize |
---|
1577 | cases (block_region b) normalize |
---|
1578 | >eqZb_z_z normalize @refl |
---|
1579 | qed. |
---|
1580 | |
---|
1581 | lemma low_bound_freed_block : |
---|
1582 | ∀m,b. low_bound (free m b) b = (pos one). |
---|
1583 | #m #b normalize |
---|
1584 | cases (block_region b) normalize |
---|
1585 | >eqZb_z_z normalize @refl |
---|
1586 | qed. |
---|
1587 | |
---|
1588 | (* Lemma 49 in Leroy&Blazy *) |
---|
1589 | lemma free_non_aliasing_m1 : |
---|
1590 | ∀E:embedding. |
---|
1591 | ∀m1,m2,m1'. |
---|
1592 | memory_inj E m1 m2 → |
---|
1593 | ∀b. free m1 b = m1' → |
---|
1594 | non_aliasing E m1'. |
---|
1595 | (* The proof proceeds by a first case analysis to see wether b lives in the |
---|
1596 | same world as the non-aliasing blocks (if not : trivial), in this case |
---|
1597 | we proceed to a second case analysis on the non-aliasing hypothesis in |
---|
1598 | memory_inj. *) |
---|
1599 | #E #m1 #m2 #m1' #Hinj #b #Hfree |
---|
1600 | whd |
---|
1601 | #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq |
---|
1602 | #Hembed1 #Hembed2 |
---|
1603 | @(eq_block_elim … b1' b2') normalize nodelta |
---|
1604 | [ 2: try // ] |
---|
1605 | #Hblocks_eq |
---|
1606 | lapply Hembed2 -Hembed2 |
---|
1607 | lapply Hembed1 -Hembed1 |
---|
1608 | lapply Hblocks_eq -Hblocks_eq |
---|
1609 | (*cases b1' #r1' #bid1' |
---|
1610 | cases b2' #r2' #bid2' *) |
---|
1611 | #Heq destruct (Heq) |
---|
1612 | generalize in match b2'; |
---|
1613 | #target #Hembed1 #Hembed2 |
---|
1614 | lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2) |
---|
1615 | >eq_block_b_b normalize nodelta |
---|
1616 | normalize nodelta <Hfree |
---|
1617 | @(eq_block_elim … b1 b) |
---|
1618 | [ #Heq destruct (Heq) #Hcase |
---|
1619 | %1 %2 whd |
---|
1620 | >high_bound_freed_block >low_bound_freed_block |
---|
1621 | // |
---|
1622 | | #Hneq1 @(eq_block_elim … b2 b) |
---|
1623 | [ #Heq destruct (Heq) #Hcase |
---|
1624 | %2 whd |
---|
1625 | >high_bound_freed_block >low_bound_freed_block |
---|
1626 | // ] ] |
---|
1627 | #Hneq2 |
---|
1628 | >unfold_high_bound >unfold_high_bound >unfold_high_bound >unfold_high_bound |
---|
1629 | >unfold_low_bound >unfold_low_bound >unfold_low_bound >unfold_low_bound |
---|
1630 | <(high_free_eq … Hneq1) <(high_free_eq … Hneq2) |
---|
1631 | <(low_free_eq … Hneq1) <(low_free_eq … Hneq2) |
---|
1632 | * |
---|
1633 | [ 2: #H %2 whd >unfold_high_bound >unfold_low_bound |
---|
1634 | <(low_free_eq … Hneq2) <(high_free_eq … Hneq2) @H ] |
---|
1635 | * |
---|
1636 | [ 2: #H %1%2 whd >unfold_high_bound >unfold_low_bound |
---|
1637 | <(low_free_eq … Hneq1) <(high_free_eq … Hneq1) @H ] |
---|
1638 | * #H |
---|
1639 | [ %1 %1 %1 @H |
---|
1640 | | %1 %1 %2 @H ] |
---|
1641 | qed. |
---|
1642 | |
---|
1643 | (* Extending lemma 46 and 49 to memory injections *) |
---|
1644 | lemma free_memory_inj_m1 : |
---|
1645 | ∀E:embedding. |
---|
1646 | ∀m1,m2,m1'. |
---|
1647 | memory_inj E m1 m2 → |
---|
1648 | ∀b. free m1 b = m1' → |
---|
1649 | memory_inj E m1' m2. |
---|
1650 | #E #m1 #m2 #m1' #Hinj #b #Hfree |
---|
1651 | cases Hinj |
---|
1652 | #Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable |
---|
1653 | % try assumption |
---|
1654 | [ @(free_load_sim_ptr_m1 … Hload_sim … Hfree) |
---|
1655 | | #bb #Hnot_valid lapply (Hfreeblock bb) #HA @HA % #HB |
---|
1656 | cases Hnot_valid #HC @HC <Hfree @HB |
---|
1657 | | #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation) |
---|
1658 | <Hfree in Hvalid_m1'; @valid_free_to_valid |
---|
1659 | | @(free_non_aliasing_m1 … Hinj … Hfree) |
---|
1660 | | #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?); |
---|
1661 | cases (E bb) normalize nodelta try // |
---|
1662 | * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj |
---|
1663 | try // |
---|
1664 | @(eq_block_elim … b bb) |
---|
1665 | [ 2,4: |
---|
1666 | #Hneq destruct (Hfree) |
---|
1667 | whd in match (free ??); |
---|
1668 | whd >unfold_low_bound >unfold_high_bound |
---|
1669 | whd in match (update_block ?????); >(not_eq_block … (sym_neq ??? Hneq)) |
---|
1670 | try @conj normalize nodelta cases HA try // |
---|
1671 | | 1,3: |
---|
1672 | #H destruct whd in match (free ??); |
---|
1673 | whd [ >unfold_low_bound ] >unfold_high_bound |
---|
1674 | whd in match (update_block ?????); >eq_block_b_b |
---|
1675 | normalize nodelta try @conj try // % try // |
---|
1676 | ] |
---|
1677 | ] qed. |
---|
1678 | |
---|
1679 | (* Lifting lemma 47 to memory injs - note that we require a much stronger condition |
---|
1680 | * on the freed block : no block of m1 can map to it. Not even an invalid block or |
---|
1681 | * an empty one. |
---|
1682 | * XXX this lemma is not given in Leroy&Blazy, and unless future developments requires |
---|
1683 | * it I will comment it out. XXX *) |
---|
1684 | lemma free_memory_inj_m2 : |
---|
1685 | ∀E:embedding. |
---|
1686 | ∀m1,m2,m2'. |
---|
1687 | memory_inj E m1 m2 → |
---|
1688 | ∀b. free m2 b = m2' → |
---|
1689 | (∀b1,delta. E b1 = Some ? 〈b, delta〉 → |
---|
1690 | (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → |
---|
1691 | memory_inj E m1 m2'. |
---|
1692 | #E #m1 #m2 #m2' #Hinj #b #Hfree #b_not_mapped |
---|
1693 | % cases Hinj try // |
---|
1694 | #Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl |
---|
1695 | [ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed |
---|
1696 | @(b_not_mapped … b1 delta Hembed) |
---|
1697 | | @Hfreeblock |
---|
1698 | | * #bp #op #p' #Hp_valid #Hptr_trans |
---|
1699 | @(eq_block_elim … (pblock p') b) |
---|
1700 | [ #Heq lapply (Hvalid … Hp_valid Hptr_trans) #Hp_valid' destruct (Heq) |
---|
1701 | cases (some_inversion ????? Hptr_trans) |
---|
1702 | * #bp' #op' * #Hembed normalize nodelta #Heq destruct (Heq) |
---|
1703 | cases (b_not_mapped … Hembed) |
---|
1704 | [ #Hnot_valid lapply (Hfreeblock … Hnot_valid) >Hembed #Habsurd destruct (Habsurd) |
---|
1705 | | #Hempty @False_ind lapply (valid_pointer_to_Prop … Hp_valid) * * #_ |
---|
1706 | whd in Hempty; #Hle #Hlt |
---|
1707 | lapply (Zlt_to_Zle_to_Zlt … Hlt Hempty) #Hlt2 |
---|
1708 | lapply (Zlt_to_Zle_to_Zlt … Hlt2 Hle) #Hlt3 |
---|
1709 | @(absurd … Hlt3 (irreflexive_Zlt ?)) ] |
---|
1710 | | #Hneq lapply (Hvalid … Hp_valid Hptr_trans) <Hfree #HA |
---|
1711 | @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … HA) -HA * * |
---|
1712 | #HA #HB #HC @conj try @conj try assumption |
---|
1713 | [ >unfold_low_bound <(low_free_eq m2 ?? Hneq) @HB |
---|
1714 | | >unfold_high_bound <(high_free_eq m2 ?? Hneq) @HC ] |
---|
1715 | ] |
---|
1716 | | #bb #b' #o' #Hembed |
---|
1717 | lapply (Hnodangling … Hembed) <Hfree // |
---|
1718 | | @Hregion |
---|
1719 | | #bb lapply (Himpl bb) |
---|
1720 | whd in ⊢ (% → %); cases (E bb) normalize nodelta try // |
---|
1721 | * #BLO #OFF normalize nodelta * * destruct (Hfree) |
---|
1722 | #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption |
---|
1723 | cases Hbb try // #Hlow_bb #Hhigh_bb |
---|
1724 | [ >unfold_low_bound |
---|
1725 | | *: >unfold_high_bound ] |
---|
1726 | whd in match (update_block ?????); |
---|
1727 | @(eq_block_elim … BLO b) |
---|
1728 | #H [ 1,3,5: destruct (H) normalize nodelta try // |
---|
1729 | @conj try // |
---|
1730 | | *: normalize nodelta cases HBLO try // ] |
---|
1731 | ] qed. |
---|
1732 | |
---|
1733 | |
---|
1734 | (* Lemma 64 of L&B on [freelist] *) |
---|
1735 | lemma freelist_memory_inj_m1_m2 : |
---|
1736 | ∀E:embedding. |
---|
1737 | ∀m1,m2,m1',m2'. |
---|
1738 | memory_inj E m1 m2 → |
---|
1739 | ∀blocklist,b2. |
---|
1740 | (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → |
---|
1741 | free m2 b2 = m2' → |
---|
1742 | free_list m1 blocklist = m1' → |
---|
1743 | memory_inj E m1' m2'. |
---|
1744 | #E #m1 #m2 #m1' #m2' #Hinj #blocklist #b2 #Hnot_mapped #Hfree2 #Hfree_list |
---|
1745 | cut (memory_inj E m1' m2) |
---|
1746 | [ <Hfree_list -Hfree_list |
---|
1747 | -Hnot_mapped |
---|
1748 | lapply Hinj -Hinj |
---|
1749 | lapply m1 -m1 |
---|
1750 | elim blocklist |
---|
1751 | [ #m1 #Hinj @Hinj |
---|
1752 | | #hd #tl #Hind #m1 #Hinj |
---|
1753 | @(free_memory_inj_m1 ? (free_list m1 tl) ? (free (free_list m1 tl) hd) ? hd) |
---|
1754 | try @refl @(Hind … Hinj) |
---|
1755 | ] |
---|
1756 | ] |
---|
1757 | #Hinj' |
---|
1758 | @(free_memory_inj_m2 … Hinj' … Hfree2) |
---|
1759 | #b1 #delta #Hembed %2 |
---|
1760 | lapply (Hnot_mapped … Hembed) |
---|
1761 | lapply Hfree_list -Hfree_list |
---|
1762 | generalize in match m1'; |
---|
1763 | generalize in match m1; |
---|
1764 | elim blocklist |
---|
1765 | [ #m1 #m1' whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @False_ind |
---|
1766 | | #hd #tl #Hind #m1 #m1' #Hfree_list * |
---|
1767 | [ #Heq destruct whd |
---|
1768 | whd in match (free_list ??); |
---|
1769 | >unfold_high_bound >unfold_low_bound |
---|
1770 | whd in match (update_block ?????); >eq_block_b_b |
---|
1771 | normalize nodelta @I |
---|
1772 | | >free_list_cons in Hfree_list; #Hfree_list #H |
---|
1773 | <Hfree_list whd cases m1 #contents2 #n2 #Hn2 |
---|
1774 | >unfold_high_bound >unfold_low_bound |
---|
1775 | whd in match (update_block ?????); |
---|
1776 | @(eq_block_elim … b1 hd) |
---|
1777 | [ #Heq normalize nodelta @I |
---|
1778 | | #Hneq normalize nodelta @(Hind … (mk_mem contents2 n2 Hn2) … (refl ??) … H) |
---|
1779 | ] |
---|
1780 | ] |
---|
1781 | ] qed. |
---|
1782 | |
---|
1783 | (* ---------------------------------------------------------- *) |
---|
1784 | (* Lemma 40 of the paper of Leroy & Blazy on the memory model |
---|
1785 | * and store-related lemmas *) |
---|
1786 | |
---|
1787 | lemma bestorev_beloadv_conservation : |
---|
1788 | ∀mA,mB,wb,wo,v. |
---|
1789 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
1790 | ∀rb,ro. eq_block wb rb = false → |
---|
1791 | beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro). |
---|
1792 | #mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq |
---|
1793 | whd in ⊢ (??%%); |
---|
1794 | elim mB in Hstore; #contentsB #nextblockB #HnextblockB |
---|
1795 | normalize in ⊢ (% → ?); |
---|
1796 | cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta |
---|
1797 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
1798 | cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo)) |
---|
1799 | then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) |
---|
1800 | else false) normalize nodelta |
---|
1801 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
1802 | #Heq destruct (Heq) |
---|
1803 | cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try // |
---|
1804 | cut (eqZb (block_id rb) (block_id wb) = false) |
---|
1805 | [ >eqZb_symmetric @Hblock_neq ] |
---|
1806 | #Heqzb >Heqzb normalize nodelta @refl |
---|
1807 | qed. |
---|
1808 | |
---|
1809 | (* lift [bestorev_beloadv_conservation to [loadn] *) |
---|
1810 | lemma bestorev_loadn_conservation : |
---|
1811 | ∀mA,mB,n,wb,wo,v. |
---|
1812 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
1813 | ∀rb,ro. eq_block wb rb = false → |
---|
1814 | loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n. |
---|
1815 | #mA #mB #n |
---|
1816 | elim n |
---|
1817 | [ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl |
---|
1818 | | 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq |
---|
1819 | whd in ⊢ (??%%); |
---|
1820 | >(bestorev_beloadv_conservation … Hstore … Hneq) |
---|
1821 | >(Hind … Hstore … Hneq) @refl |
---|
1822 | ] qed. |
---|
1823 | |
---|
1824 | (* lift [bestorev_loadn_conservation] to [load_value_of_type] *) |
---|
1825 | lemma bestorev_load_value_of_type_conservation : |
---|
1826 | ∀mA,mB,wb,wo,v. |
---|
1827 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
1828 | ∀rb,ro. eq_block wb rb = false → |
---|
1829 | ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. |
---|
1830 | #mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty |
---|
1831 | cases ty |
---|
1832 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1833 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1834 | // |
---|
1835 | [ 1: elim sz ] |
---|
1836 | whd in ⊢ (??%%); |
---|
1837 | >(bestorev_loadn_conservation … Hstore … Hneq) @refl |
---|
1838 | qed. |
---|
1839 | |
---|
1840 | (* lift [bestorev_load_value_of_type_conservation] to storen *) |
---|
1841 | lemma storen_load_value_of_type_conservation : |
---|
1842 | ∀l,mA,mB,wb,wo. |
---|
1843 | storen mA (mk_pointer wb wo) l = Some ? mB → |
---|
1844 | ∀rb,ro. eq_block wb rb = false → |
---|
1845 | ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. |
---|
1846 | #l elim l |
---|
1847 | [ 1: #mA #mB #wb #wo normalize #Heq destruct // |
---|
1848 | | 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren |
---|
1849 | cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren' |
---|
1850 | whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty |
---|
1851 | lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1 |
---|
1852 | lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2 |
---|
1853 | // |
---|
1854 | ] qed. |
---|
1855 | |
---|
1856 | lemma store_value_of_type_load_value_of_type_conservation : |
---|
1857 | ∀ty,mA,mB,wb,wo,v. |
---|
1858 | store_value_of_type ty mA wb wo v = Some ? mB → |
---|
1859 | ∀rb,ro. eq_block wb rb = false → |
---|
1860 | ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. |
---|
1861 | #ty #mA #mB #wb #wo #v #Hstore #rb #ro #Heq_block |
---|
1862 | cases ty in Hstore; |
---|
1863 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1864 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
1865 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); #Heq destruct ] |
---|
1866 | whd in ⊢ ((??%?) → ?); #Hstoren |
---|
1867 | @(storen_load_value_of_type_conservation … Hstoren … Heq_block) |
---|
1868 | qed. |
---|
1869 | |
---|
1870 | definition typesize' ≝ λty. typesize (typ_of_type ty). |
---|
1871 | |
---|
1872 | lemma storen_load_value_of_type_conservation_in_block_high : |
---|
1873 | ∀E,mA,mB,mC,wo,l. |
---|
1874 | memory_inj E mA mB → |
---|
1875 | ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → |
---|
1876 | ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → |
---|
1877 | high_bound mA b1 + Zoo delta < Zoo wo → |
---|
1878 | ∀ty,off. |
---|
1879 | Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → |
---|
1880 | low_bound … mA b1 ≤ Zoo off → |
---|
1881 | Zoo off < high_bound … mA b1 → |
---|
1882 | load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = |
---|
1883 | load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). |
---|
1884 | #E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty |
---|
1885 | (* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *) |
---|
1886 | cases data in Hstoren; |
---|
1887 | [ 1: normalize in ⊢ (% → ?); #Heq destruct // |
---|
1888 | | 2: #xd #data ] |
---|
1889 | #Hstoren |
---|
1890 | cases ty |
---|
1891 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1892 | | #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl |
---|
1893 | whd in match (load_value_of_type ????) in ⊢ (??%%); |
---|
1894 | [ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter |
---|
1895 | lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load |
---|
1896 | lapply off -off whd in match typesize'; normalize nodelta |
---|
1897 | generalize in match (typesize ?); #n elim n try // |
---|
1898 | #n' #Hind #o #Hhigh_load #Hlow_load #Hlt |
---|
1899 | whd in match (loadn ???) in ⊢ (??%%); |
---|
1900 | whd in match (beloadv ??) in ⊢ (??%%); |
---|
1901 | cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store |
---|
1902 | cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store |
---|
1903 | >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta |
---|
1904 | cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) |
---|
1905 | [ 1: (* Notice that: |
---|
1906 | low mA b1 ≤ o < high mA b1 |
---|
1907 | hence, since E b1 = 〈blo, delta〉 with delta >= 0 |
---|
1908 | low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *) |
---|
1909 | @cthulhu ] |
---|
1910 | #HA >HA >andb_lsimpl_true -HA |
---|
1911 | cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true) |
---|
1912 | [ 1: (* Same argument as above *) @cthulhu ] |
---|
1913 | #HA >HA normalize nodelta -HA |
---|
1914 | cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) |
---|
1915 | [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties]. |
---|
1916 | This cut follows from this lemma (which needs some info on the size of the data written, which we |
---|
1917 | have but must make explicit) and from the first cut. *) |
---|
1918 | @cthulhu ] |
---|
1919 | #HA >HA >andb_lsimpl_true -HA |
---|
1920 | cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true) |
---|
1921 | [ 1: (* Same argument as above *) @cthulhu ] |
---|
1922 | #HA >HA normalize nodelta -HA |
---|
1923 | normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???); |
---|
1924 | whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n |
---|
1925 | lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???) |
---|
1926 | [ 1: (* Provable from Hlt *) @cthulhu |
---|
1927 | | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu |
---|
1928 | | 3: (* Provable from Hlt, again *) @cthulhu ] |
---|
1929 | cases (loadn mB (mk_pointer blo |
---|
1930 | (mk_offset (addition_n ? (addition_n ? |
---|
1931 | (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') |
---|
1932 | normalize nodelta |
---|
1933 | cases (loadn mC (mk_pointer blo |
---|
1934 | (mk_offset (addition_n ? (addition_n ? |
---|
1935 | (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') |
---|
1936 | normalize nodelta try // |
---|
1937 | [ 1,2: #l #Habsurd destruct ] |
---|
1938 | #l1 #l2 #Heq |
---|
1939 | cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = |
---|
1940 | contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) |
---|
1941 | [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ] |
---|
1942 | #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%); |
---|
1943 | cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) |
---|
1944 | normalize nodelta try // |
---|
1945 | (* Ok this is going to be more painful than what I thought. *) |
---|
1946 | @cthulhu |
---|
1947 | | *: @cthulhu |
---|
1948 | ] qed. |
---|
1949 | |
---|
1950 | lemma storen_load_value_of_type_conservation_in_block_low : |
---|
1951 | ∀E,mA,mB,mC,wo,l. |
---|
1952 | memory_inj E mA mB → |
---|
1953 | ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → |
---|
1954 | ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → |
---|
1955 | Zoo wo < low_bound mA b1 + Zoo delta → |
---|
1956 | ∀ty,off. |
---|
1957 | Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → |
---|
1958 | low_bound … mA b1 ≤ Zoo off → |
---|
1959 | Zoo off < high_bound … mA b1 → |
---|
1960 | load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = |
---|
1961 | load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). |
---|
1962 | @cthulhu |
---|
1963 | qed. |
---|
1964 | |
---|
1965 | (* Writing in the "extended" part of a memory preserves the underlying injection. *) |
---|
1966 | lemma bestorev_memory_inj_to_load_sim : |
---|
1967 | ∀E,mA,mB,mC. |
---|
1968 | ∀Hext:memory_inj E mA mB. |
---|
1969 | ∀block2. ∀i : offset. ∀ty : type. |
---|
1970 | (∀block1,delta. |
---|
1971 | E block1 = Some ? 〈block2, delta〉 → |
---|
1972 | (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → |
---|
1973 | ∀v.store_value_of_type ty mB block2 i v = Some ? mC → |
---|
1974 | load_sim_ptr E mA mC. |
---|
1975 | #E #mA #mB #mC #Hinj #block2 #i #storety |
---|
1976 | cases storety |
---|
1977 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
1978 | | #structname #fieldspec | #unionname #fieldspec | #id ] #Hout #storeval #Hstore whd |
---|
1979 | #b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value |
---|
1980 | whd in Hstore:(??%?); |
---|
1981 | [ 1,5,6,7,8: destruct ] |
---|
1982 | [ 1: |
---|
1983 | lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value) |
---|
1984 | lapply Hload_value -Hload_value |
---|
1985 | cases ty |
---|
1986 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
1987 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
1988 | #Hload_value |
---|
1989 | (* Prove that the contents of mB where v1 was were untouched. *) |
---|
1990 | * #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption |
---|
1991 | cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta |
---|
1992 | #Heq destruct (Heq) |
---|
1993 | @(eq_block_elim … b2 block2) |
---|
1994 | [ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore) |
---|
1995 | @not_eq_block @sym_neq @Hblocks_neq |
---|
1996 | | 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) * |
---|
1997 | [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq |
---|
1998 | lapply (load_by_value_success_valid_ptr_aux … Hload_value) // |
---|
1999 | * * #Hlt #Hlowb_off1 #Hhighb_off1 |
---|
2000 | lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1 |
---|
2001 | lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1 |
---|
2002 | @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed) |
---|
2003 | try // |
---|
2004 | (* remaining stuff provable from Hload_value *) |
---|
2005 | @cthulhu |
---|
2006 | | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq |
---|
2007 | lapply (load_by_value_success_valid_ptr_aux … Hload_value) // |
---|
2008 | * * #Hlt #Hlowb_off1 #Hhighb_off1 |
---|
2009 | lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1 |
---|
2010 | lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1 |
---|
2011 | @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed) |
---|
2012 | try // |
---|
2013 | [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu |
---|
2014 | | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ] |
---|
2015 | ] |
---|
2016 | ] |
---|
2017 | | *: (* exactly the same proof as above *) @cthulhu ] |
---|
2018 | qed. |
---|
2019 | |
---|
2020 | (* Lift the above result to memory_inj |
---|
2021 | * This is Lemma 40 of Leroy & Blazy *) |
---|
2022 | lemma bestorev_memory_inj_to_memory_inj : |
---|
2023 | ∀E,mA,mB,mC. |
---|
2024 | ∀Hext:memory_inj E mA mB. |
---|
2025 | ∀block2. ∀i : offset. ∀ty : type. |
---|
2026 | (∀block1,delta. |
---|
2027 | E block1 = Some ? 〈block2, delta〉 → |
---|
2028 | (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → |
---|
2029 | ∀v.store_value_of_type ty mB block2 i v = Some ? mC → |
---|
2030 | memory_inj E mA mC. |
---|
2031 | #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % |
---|
2032 | lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // |
---|
2033 | cases Hinj #Hsim' #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption |
---|
2034 | [ |
---|
2035 | #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid |
---|
2036 | cases ty in Hstore; |
---|
2037 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
2038 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
2039 | whd in ⊢ ((??%?) → ?); |
---|
2040 | [ 1,4,5,6,7: #Habsurd destruct ] |
---|
2041 | cases (fe_to_be_values ??) |
---|
2042 | [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl |
---|
2043 | | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_ |
---|
2044 | @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh |
---|
2045 | @conj try @conj try assumption >Hnext try // |
---|
2046 | cases (Hbounds (pblock p')) #HA #HB |
---|
2047 | whd in match (low_bound ??); whd in match (high_bound ??); |
---|
2048 | >HA >HB try assumption |
---|
2049 | ] |
---|
2050 | | lapply (mem_bounds_after_store_value_of_type … Hstore) |
---|
2051 | * #Hnext_eq #Hb |
---|
2052 | #b #b' #o' cases (Hb b') #Hlow_eq #Hhigh_eq #Hembed |
---|
2053 | lapply (mi_nodangling … Hinj … Hembed) |
---|
2054 | whd in match (valid_block ??) in ⊢ (% → %); |
---|
2055 | >(Hnext_eq) try // |
---|
2056 | | #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %); |
---|
2057 | cases (E b) try // |
---|
2058 | * #BLO #OFF normalize nodelta * * |
---|
2059 | #Hb #HBLO #Hbound try @conj try @conj try assumption |
---|
2060 | lapply (mem_bounds_after_store_value_of_type … Hstore) * |
---|
2061 | #_ #Hbounds |
---|
2062 | cases (Hbounds BLO) #Hlow #Hhigh whd % |
---|
2063 | [ >unfold_low_bound | >unfold_high_bound ] |
---|
2064 | >Hlow >Hhigh cases HBLO try // |
---|
2065 | ] qed. |
---|
2066 | |
---|
2067 | |
---|
2068 | (* ---------------------------------------------------------- *) |
---|
2069 | (* Lemma 41 of the paper of Leroy & Blazy on the memory model |
---|
2070 | * and related lemmas *) |
---|
2071 | |
---|
2072 | (* The back-end might contain something similar to this lemma. *) |
---|
2073 | lemma be_to_fe_value_ptr : |
---|
2074 | ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). |
---|
2075 | #b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta |
---|
2076 | (*cases br normalize nodelta *) >eqZb_z_z normalize nodelta |
---|
2077 | cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq |
---|
2078 | <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl |
---|
2079 | * // |
---|
2080 | qed. |
---|
2081 | |
---|
2082 | lemma fe_to_be_values_length : |
---|
2083 | ∀E,v1,v2,ty. |
---|
2084 | value_eq E v1 v2 → |fe_to_be_values ty v1| = |fe_to_be_values ty v2|. |
---|
2085 | #E #v1 #v2 #ty #Hvalue_eq |
---|
2086 | @(value_eq_inversion … Hvalue_eq) // |
---|
2087 | qed. |
---|
2088 | |
---|
2089 | lemma value_eq_to_be_and_back_again : |
---|
2090 | ∀E,ty,v1,v2. |
---|
2091 | value_eq E v1 v2 → |
---|
2092 | ast_typ_consistent_with_value ty v1 → |
---|
2093 | value_eq E (be_to_fe_value ty (fe_to_be_values ty v1 )) (be_to_fe_value ty (fe_to_be_values ty v2)). |
---|
2094 | #E #ty #v1 #v2 #Hvalue_eq |
---|
2095 | @(value_eq_inversion … Hvalue_eq) try // |
---|
2096 | [ 1: cases ty // |
---|
2097 | | 2: #sz #i cases ty |
---|
2098 | [ 2: @False_ind |
---|
2099 | | 1: #sz' #sg #H lapply H whd in ⊢ (% → ?); #Heq |
---|
2100 | lapply (fe_to_be_to_fe_value_int … H) #H >H // ] |
---|
2101 | | 3: #p1 #p2 #Hembed cases ty |
---|
2102 | [ 1: #sz #sg @False_ind |
---|
2103 | | 2: #_ |
---|
2104 | cases p1 in Hembed; #b1 #o1 |
---|
2105 | cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H |
---|
2106 | cases (some_inversion ????? H) * #b3 #o3 * #Hembed |
---|
2107 | normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr |
---|
2108 | destruct %4 whd in match (pointer_translation ??); |
---|
2109 | >Hembed normalize nodelta @refl |
---|
2110 | ] |
---|
2111 | ] qed. |
---|
2112 | |
---|
2113 | (* ------------------------------------------------------------ *) |
---|
2114 | (* Lemma ?? of the paper of Leroy & Blazy on the memory model ? *) |
---|
2115 | |
---|
2116 | lemma storen_parallel_memory_exists : |
---|
2117 | ∀E,m1,m2. |
---|
2118 | memory_inj E m1 m2 → |
---|
2119 | ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → |
---|
2120 | ∀v1,v2. value_eq E v1 v2 → |
---|
2121 | ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ |
---|
2122 | ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'. |
---|
2123 | (* ∧ loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2).*) |
---|
2124 | #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty |
---|
2125 | lapply (mi_valid_pointers … Hinj) |
---|
2126 | generalize in match m2; |
---|
2127 | generalize in match m1; |
---|
2128 | generalize in match i; |
---|
2129 | lapply (fe_to_be_values_length … ty Hvalue_eq) |
---|
2130 | generalize in match (fe_to_be_values ty v2); |
---|
2131 | generalize in match (fe_to_be_values ty v1); |
---|
2132 | #l1 elim l1 |
---|
2133 | [ 1: #l2 #Hl2 |
---|
2134 | cut (l2 = []) |
---|
2135 | [ cases l2 in Hl2; // #hd' #tl' normalize #Habsurd destruct ] |
---|
2136 | #Hl2_empty >Hl2_empty #o #m1 #m2 #_ normalize /2 by ex_intro/ |
---|
2137 | | 2: #hd1 #tl1 #Hind #l2 #Hlength |
---|
2138 | cut (∃hd2,tl2.l2 = hd2::tl2 ∧ |tl1| = |tl2|) |
---|
2139 | [ cases l2 in Hlength; |
---|
2140 | [ normalize #Habsurd destruct |
---|
2141 | | #hd2 #tl2 normalize #H %{hd2} %{tl2} @conj try @refl destruct (H) assumption ] ] |
---|
2142 | * #hd2 * #tl2 * #Heq2 destruct (Heq2) #Hlen_tl |
---|
2143 | #o #m1 #m2 #Hvalid_embed #Hstoren |
---|
2144 | cases (some_inversion ????? Hstoren) #m1_tmp * #Hbestorev #Hstoren_tl |
---|
2145 | lapply (Hvalid_embed (mk_pointer b1 o) (mk_pointer b2 (offset_plus o delta)) ??) |
---|
2146 | [ 1: whd in match (pointer_translation ??); |
---|
2147 | >Hembed normalize nodelta @refl |
---|
2148 | | 2: @(bestorev_to_valid_pointer … Hbestorev) ] |
---|
2149 | #Hvalid_ptr_m2 |
---|
2150 | whd in match (storen ???); |
---|
2151 | lapply (valid_pointer_to_bestorev_ok m2 (mk_pointer b2 (offset_plus o delta)) hd2 Hvalid_ptr_m2) |
---|
2152 | * #m2_tmp #Hbestorev2 >Hbestorev2 normalize nodelta |
---|
2153 | whd in match (shift_pointer ???) in Hstoren_tl ⊢ %; |
---|
2154 | whd in match (shift_offset ???) in Hstoren_tl ⊢ %; |
---|
2155 | (* normalize in match (sign_ext ???) in Hstoren_tl ⊢ %;*) |
---|
2156 | cut (mk_offset (addition_n ? (offv (offset_plus o delta)) (sign_ext 2 offset_size (bitvector_of_nat 2 1))) = |
---|
2157 | offset_plus (offset_plus o (mk_offset (sign_ext 2 offset_size (bitvector_of_nat 2 1)))) delta) |
---|
2158 | [ cases o #o' normalize nodelta whd in match (offset_plus ??) in ⊢ (??%%); |
---|
2159 | whd in match (offset_plus ??) in ⊢ (???(?%)); |
---|
2160 | /2 by associative_addition_n, commutative_addition_n, refl/ ] |
---|
2161 | #Heq_cleanup >Heq_cleanup >Heq_cleanup in Hind; #Hind @(Hind … Hstoren_tl) |
---|
2162 | try assumption |
---|
2163 | #p #p' #Hvalid_in_m1_tmp #Hp_embed @valid_pointer_of_Prop |
---|
2164 | lapply (mem_bounds_invariant_after_bestorev … Hbestorev) * * * * |
---|
2165 | #Hnextblock_eq #Hbounds_eq #Hoffset_in_bounds #Hcontents_at_eq #Hcontents_else_eq |
---|
2166 | lapply (mem_bounds_invariant_after_bestorev … Hbestorev2) * * * * |
---|
2167 | #Hnextblock_eq2 #Hbounds_eq2 #Hoffset_in_bounds2 #Hcontents_at_eq2 #Hcontents_else_eq2 |
---|
2168 | cut (valid_pointer m1 p = true) |
---|
2169 | [ @valid_pointer_of_Prop |
---|
2170 | cases (valid_pointer_to_Prop … Hvalid_in_m1_tmp) |
---|
2171 | >Hnextblock_eq cases (Hbounds_eq (pblock p)) #Hlow' #Hhigh' |
---|
2172 | whd in match (low_bound ??); whd in match (high_bound ??); |
---|
2173 | >Hlow' >Hhigh' * /3 by conj/ ] |
---|
2174 | #Hvalid_in_m1 |
---|
2175 | lapply (Hvalid_embed p p' Hvalid_in_m1 Hp_embed) #Hvalid_in_m2 |
---|
2176 | cases (valid_pointer_to_Prop … Hvalid_in_m2) * #Hnextblock2' #Hlow2' #Hhigh2' |
---|
2177 | @conj try @conj |
---|
2178 | >Hnextblock_eq2 try assumption |
---|
2179 | cases (Hbounds_eq2 … (pblock p')) #Hlow2'' #Hhigh2'' |
---|
2180 | whd in match (low_bound ??); |
---|
2181 | whd in match (high_bound ??); |
---|
2182 | >Hlow2'' >Hhigh2'' assumption |
---|
2183 | ] qed. |
---|
2184 | |
---|
2185 | lemma storen_parallel_memory_exists_and_preserves_loads : |
---|
2186 | ∀E,m1,m2. |
---|
2187 | memory_inj E m1 m2 → |
---|
2188 | ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → |
---|
2189 | ∀v1,v2. value_eq E v1 v2 → |
---|
2190 | ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ |
---|
2191 | ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ |
---|
2192 | loadn m2' (mk_pointer b2 (offset_plus i delta)) (|fe_to_be_values ty v2|) = Some ? (fe_to_be_values ty v2). |
---|
2193 | #E #m1 #m2 #Hinj #b1 #b2 #delta #Hembed #v1 #v2 #Hvalue_eq #i #m1' #ty #Hstoren |
---|
2194 | cases (storen_parallel_memory_exists … Hinj … Hembed … Hvalue_eq i m1' ty Hstoren) |
---|
2195 | #m2' #Hstoren' %{m2'} @conj try assumption |
---|
2196 | @(storen_loadn_ok … Hstoren') |
---|
2197 | // |
---|
2198 | qed. |
---|
2199 | |
---|
2200 | (* If E ⊢ m1 ↦ m2 |
---|
2201 | *and* if E b1 = 〈b2,delta〉, |
---|
2202 | *and* if we write /A PROPER VALUE/ at 〈b1,i〉 successfuly, |
---|
2203 | *then* we can write /something value_eq-compatible/ in m2 at 〈b2,i+delta〉 successfuly yielding m2' |
---|
2204 | *and* preserve the injection : E ⊢ m1' ↦ m2' |
---|
2205 | N.B.: this result cannot be given at the back-end level : we could overwrite a pointer |
---|
2206 | and break the value_eq correspondence between the memories. *) |
---|
2207 | axiom storen_parallel_aux : |
---|
2208 | ∀E,m1,m2. |
---|
2209 | ∀Hinj:memory_inj E m1 m2. |
---|
2210 | ∀v1,v2. value_eq E v1 v2 → |
---|
2211 | ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → |
---|
2212 | ∀ty,i,m1'. |
---|
2213 | ast_typ_consistent_with_value ty v1 → |
---|
2214 | storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → |
---|
2215 | ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ |
---|
2216 | memory_inj E m1' m2'. |
---|
2217 | (* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to |
---|
2218 | * explain why, and how we might still be able to prove it given enough time. |
---|
2219 | I'll be refering to a paper by Leroy & Blazy in the J.A.R. |
---|
2220 | In CompCert, when storing some data of size S in some location 〈block, offset〉, |
---|
2221 | what happens is that |
---|
2222 | 1) the memory is extended with a map from 〈block,offset〉 to the actual data |
---|
2223 | 2) the memory inteval from 〈block,offset+1〉 to 〈block,offset+S-1〉 is invalidated, |
---|
2224 | meaning that every load in this interval will fail. |
---|
2225 | This behaviour is documented at page 9 in the aforementioned paper. |
---|
2226 | The memory model of Cerco is in a sense much more realistic. When storing a front-end |
---|
2227 | value fv, the story is the following : |
---|
2228 | 1) the value fv is marshalled into a list of back-end values (byte-sized) which correspond |
---|
2229 | to the actual size of the data in-memory. 2) This list is then stored as-is at the |
---|
2230 | location 〈block, offset〉. |
---|
2231 | |
---|
2232 | Now on to the lemma we want to prove. The difficult part is to prove [load_sim E m1' m2'], |
---|
2233 | i.e. we want to prove that ∀c1,off1,c2,off2,delta. s.t. E c1 = 〈c2, off2〉 |
---|
2234 | load_value_of_type m1' c1 off1 = ⌊vA⌋ → |
---|
2235 | load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋ ∧ |
---|
2236 | value_eq E vA vB, |
---|
2237 | where m1' and m2' are the result of storing some values v1 and v2 in resp. m1 and m2 |
---|
2238 | at some resp. locations 〈b1,i〉 and (pointer_translation E b1 i) (cf statement). |
---|
2239 | |
---|
2240 | In CompCert, the proof of this statement goes by case analysis on 〈c1,off1〉. |
---|
2241 | Case 1: 〈b1,i〉 = 〈c1,off1〉 → we read the freshly stored data. |
---|
2242 | Case 2: b1 = c1 but [i; i+|v1|] and [c1, c1+|vA|] describe /disjoint/ areas of the |
---|
2243 | same block. In this case, we can use the lemma store_value_load_disjoint |
---|
2244 | on the hypothesis (load_value_of_type m1' c1 off1 = ⌊vA⌋) |
---|
2245 | yielding (load_value_of_type m1' c1 off1 = load_value_of_type m1 c1 off1) |
---|
2246 | allowing us to use the load_sim hypothesis on (m1, m2) to obtain |
---|
2247 | (load_value_of_type m2 c2 (off1+off2) = ⌊vB⌋) |
---|
2248 | which we can lift back to |
---|
2249 | (load_value_of_type m2' c2 (off1+off2) = ⌊vB⌋) |
---|
2250 | using the disjointness hypothesis contained in the original memory injection [Hinj]. |
---|
2251 | case 4: b1 ≠ c1, nothing difficult |
---|
2252 | case 3: the intervals [i; i+|v1|] and [c1, c1+|vA|] /overalap/ ! |
---|
2253 | in CompCert, the prof follows simply from the fact that the load |
---|
2254 | (load_value_of_type m1' c1 off1) will fail because of invalidated memory, |
---|
2255 | yielding a contradiction. We have no such possibility in Cerco. |
---|
2256 | |
---|
2257 | I see a possible, convoluted way out of this problem. In the case of an overlap, we |
---|
2258 | need to proceed to an inversion on load_value_of_type m1' c1 off1 = ⌊vA⌋ and to |
---|
2259 | actually look at the data beeing written. If we succeeded in proceeding to this load, |
---|
2260 | this means that the back-end values stored are "consistent". |
---|
2261 | Besides, we need to proceed to a case analysis on what we stored beforehand. |
---|
2262 | A) If we stored an integer |
---|
2263 | . of size 8: this means that the overlap actually includes all of the freshly stored |
---|
2264 | area. This area contains one [BVByte]. If we succeeded in performing an overlapping load, |
---|
2265 | we either overlapped from the beginning, from the end or from both ends of the stored |
---|
2266 | area. In all cases, since this area contains a BVByte, all other offsets MUST contain |
---|
2267 | BVBytes, otherwise we would have a contradiction ... (cumbersome to show but possible) |
---|
2268 | Hence, we can splice the load in 2 or 3 sub-loads : |
---|
2269 | . re-use the Case 2 above (disjoint areas) for the parts of the load that are before |
---|
2270 | and after the stored area |
---|
2271 | . re-use the Case 1 above for the stored area |
---|
2272 | and show the whole successful load |
---|
2273 | . of size 16,32: we have more freedom but only a finite number of overlap possibilities |
---|
2274 | in each case. We can enumerate them and proceed along the same lines as in the 8 bit |
---|
2275 | case. |
---|
2276 | B) If we stored a pointer (of size 2 bytes, necessarily) |
---|
2277 | . the bytes of a pointer are stored in order and (/!\ important /!\) are /numbered/. |
---|
2278 | This means that any successful overlapping load has managed to read a pointer in |
---|
2279 | the wrong order, which yields a contradiction. |
---|
2280 | C) If we stored a Vnull, roughly the same reasoning as in the pointer case |
---|
2281 | D) If we stored a Vundef ... This gets hairy. We must reason on the way fe_to_be_values |
---|
2282 | and be_to_fe_value works. What we want is to show that the load |
---|
2283 | [load_value_of_a type m1' c1 off1] yields a Vundef. This can happen in several ways. |
---|
2284 | . If we try to load something of integer type, we will have a Vundef because |
---|
2285 | we can show that some of the back-end values are BVundef (cf [build_integer]) |
---|
2286 | . If we try to load a pointer, it will also fail for the same reason. |
---|
2287 | I'll admit that I'm not too sure about the last case. Also, my reasoning on pointers might |
---|
2288 | fail if we have "longer that 2 bytes" pointers. |
---|
2289 | |
---|
2290 | This was a high-level and sketchy proof, and in the interests of time I decide to axiomatize |
---|
2291 | it. |
---|
2292 | *) |
---|
2293 | |
---|
2294 | (* This is lemma 60 from Leroy&Blazy *) |
---|
2295 | lemma store_value_of_type_parallel : |
---|
2296 | ∀E,m1,m2. |
---|
2297 | ∀Hinj:memory_inj E m1 m2. |
---|
2298 | ∀v1,v2. value_eq E v1 v2 → |
---|
2299 | ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → |
---|
2300 | ∀ty,i,m1'. |
---|
2301 | type_consistent_with_value ty v1 → |
---|
2302 | store_value_of_type ty m1 b1 i v1 = Some ? m1' → |
---|
2303 | ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧ |
---|
2304 | memory_inj E m1' m2'. |
---|
2305 | #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' |
---|
2306 | cases ty |
---|
2307 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
2308 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
2309 | #Hconsistent whd in ⊢ ((??%?) → ?); |
---|
2310 | [ 1,4,5,6,7: #Habsurd destruct ] |
---|
2311 | whd in match (store_value_of_type ?????); |
---|
2312 | @(storen_parallel_aux … Hinj … Hembed … Hconsistent) // |
---|
2313 | qed. |
---|
2314 | |
---|
2315 | lemma store_value_of_type_load_sim : |
---|
2316 | ∀E,m1,m2,m1'. |
---|
2317 | ∀Hinj:memory_inj E m1 m2. |
---|
2318 | ∀ty,b,i,v. |
---|
2319 | E b = None ? → |
---|
2320 | store_value_of_type ty m1 b i v = Some ? m1' → |
---|
2321 | load_sim_ptr E m1' m2. |
---|
2322 | #E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore |
---|
2323 | cases Hinj #Hsim #Hfreeblock #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl |
---|
2324 | cases ty in Hstore; |
---|
2325 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
2326 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
2327 | [ 1,4,5,6,7: #Heq normalize in Heq; destruct ] |
---|
2328 | #Hstore whd |
---|
2329 | #b1 #off1 #b2 #off2 #ty' #v1 #Hvalid #Hembed' #Hload |
---|
2330 | lapply (store_value_of_type_load_value_of_type_conservation … Hstore b1 off1 ? ty') |
---|
2331 | [ 1,3,5: @(eq_block_elim … b b1) try // #Heq >Heq in Hembed; |
---|
2332 | #Hembed whd in Hembed':(??%?); >Hembed in Hembed'; #H normalize in H; |
---|
2333 | destruct ] |
---|
2334 | #Heq <Heq in Hload; #Hload |
---|
2335 | (* Three times the same proof, but computing the indices for the subcases is a PITA *) |
---|
2336 | [ 1: |
---|
2337 | cases ty' in Hload; |
---|
2338 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
2339 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
2340 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); |
---|
2341 | #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} |
---|
2342 | @conj try @refl %4 assumption ] |
---|
2343 | #Hload @(Hsim … Hembed' … Hload) |
---|
2344 | @(load_by_value_success_valid_pointer … Hload) // |
---|
2345 | | 2: |
---|
2346 | cases ty' in Hload; |
---|
2347 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
2348 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
2349 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); |
---|
2350 | #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} |
---|
2351 | @conj try @refl %4 assumption ] |
---|
2352 | #Hload @(Hsim … Hembed' … Hload) |
---|
2353 | @(load_by_value_success_valid_pointer … Hload) // |
---|
2354 | | 3: |
---|
2355 | cases ty' in Hload; |
---|
2356 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
2357 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
2358 | [ 1,4,5,6,7: whd in ⊢ ((??%?) → ?); whd in match (load_value_of_type ????); |
---|
2359 | #Heq destruct (Heq) %{(Vptr (mk_pointer b2 off2))} |
---|
2360 | @conj try @refl %4 assumption ] |
---|
2361 | #Hload @(Hsim … Hembed' … Hload) |
---|
2362 | @(load_by_value_success_valid_pointer … Hload) // |
---|
2363 | ] qed. |
---|
2364 | |
---|
2365 | lemma store_value_of_type_memory_inj : |
---|
2366 | ∀E,m1,m2,m1'. |
---|
2367 | ∀Hinj:memory_inj E m1 m2. |
---|
2368 | ∀ty,b,i,v. |
---|
2369 | E b = None ? → |
---|
2370 | store_value_of_type ty m1 b i v = Some ? m1' → |
---|
2371 | memory_inj E m1' m2. |
---|
2372 | #E #m1 #m2 #m1' #Hinj #ty #b #i #v1 #Hnot_mapped #Hstore |
---|
2373 | % |
---|
2374 | [ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore) |
---|
2375 | | *: lapply (mem_bounds_after_store_value_of_type … Hstore) |
---|
2376 | * #H1 #H2 |
---|
2377 | [ #b * #Hnot_valid @(mi_freeblock ??? Hinj) |
---|
2378 | % #H @Hnot_valid whd in H:% ⊢ %; >H1 @H |
---|
2379 | | #p #p' #Hvalid @(mi_valid_pointers ??? Hinj) |
---|
2380 | @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) |
---|
2381 | >H1 cases (H2 (pblock p)) #HA #HB |
---|
2382 | >unfold_high_bound >unfold_low_bound |
---|
2383 | >unfold_high_bound >unfold_low_bound |
---|
2384 | >HA >HB // |
---|
2385 | | @(mi_nodangling … Hinj) |
---|
2386 | | @(mi_region … Hinj) |
---|
2387 | | whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq #Hembed1 #Hembed2 |
---|
2388 | whd in match (block_is_empty ??); |
---|
2389 | whd in match (block_is_empty m1' b2); |
---|
2390 | >unfold_high_bound >unfold_low_bound |
---|
2391 | >unfold_high_bound >unfold_low_bound |
---|
2392 | cases (H2 b1) #HA #HB |
---|
2393 | cases (H2 b2) #HC #HD |
---|
2394 | >HA >HB >HC >HD |
---|
2395 | @(mi_nonalias ??? Hinj) assumption |
---|
2396 | | #bb whd |
---|
2397 | lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?); |
---|
2398 | cases (E bb) normalize nodelta try // * #bb' #off |
---|
2399 | normalize nodelta |
---|
2400 | whd in match (block_implementable_bv ??); |
---|
2401 | whd in match (block_implementable_bv m2 bb'); |
---|
2402 | whd in match (block_implementable_bv m1' bb); |
---|
2403 | >unfold_high_bound >unfold_low_bound |
---|
2404 | >unfold_high_bound >unfold_low_bound |
---|
2405 | >unfold_high_bound |
---|
2406 | cases (H2 bb) #HA #HB |
---|
2407 | >HA >HB // |
---|
2408 | ] |
---|
2409 | ] qed. |
---|
2410 | |
---|
2411 | (* ------------------------------------------------------------------------- *) |
---|
2412 | (* Commutation results of standard unary and binary operations with value_eq. *) |
---|
2413 | |
---|
2414 | lemma unary_operation_value_eq : |
---|
2415 | ∀E,op,v1,v2,ty. |
---|
2416 | value_eq E v1 v2 → |
---|
2417 | ∀r1. |
---|
2418 | sem_unary_operation op v1 ty = Some ? r1 → |
---|
2419 | ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2. |
---|
2420 | #E #op #v1 #v2 #ty #Hvalue_eq #r1 |
---|
2421 | inversion Hvalue_eq |
---|
2422 | [ 1: #v #Hv1 #Hv2 destruct |
---|
2423 | cases op normalize |
---|
2424 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2425 | normalize #Habsurd destruct (Habsurd) |
---|
2426 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2427 | normalize #Habsurd destruct (Habsurd) |
---|
2428 | | 2: #Habsurd destruct (Habsurd) ] |
---|
2429 | | 2: #vsz #i #Hv1 #Hv2 #_ |
---|
2430 | cases op |
---|
2431 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2432 | whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???); |
---|
2433 | [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct |
---|
2434 | %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))} |
---|
2435 | cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj |
---|
2436 | // |
---|
2437 | | *: #Habsurd destruct (Habsurd) ] |
---|
2438 | | 2: whd in match (sem_unary_operation ???); |
---|
2439 | #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj // |
---|
2440 | | 3: whd in match (sem_unary_operation ???); |
---|
2441 | cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2442 | normalize nodelta |
---|
2443 | whd in ⊢ ((??%?) → ?); |
---|
2444 | [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct |
---|
2445 | %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj // |
---|
2446 | | *: #Habsurd destruct (Habsurd) ] ] |
---|
2447 | | 3: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); |
---|
2448 | cases op normalize nodelta |
---|
2449 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2450 | whd in match (sem_notbool ??); |
---|
2451 | #Heq1 destruct /3 by ex_intro, vint_eq, conj/ |
---|
2452 | | 2: normalize #Habsurd destruct (Habsurd) |
---|
2453 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2454 | whd in match (sem_neg ??); |
---|
2455 | #Heq1 destruct ] |
---|
2456 | | 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???); |
---|
2457 | cases op normalize nodelta |
---|
2458 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2459 | whd in match (sem_notbool ??); |
---|
2460 | #Heq1 destruct /3 by ex_intro, vint_eq, conj/ |
---|
2461 | | 2: normalize #Habsurd destruct (Habsurd) |
---|
2462 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
2463 | whd in match (sem_neg ??); |
---|
2464 | #Heq1 destruct ] |
---|
2465 | ] |
---|
2466 | qed. |
---|
2467 | |
---|
2468 | (* value_eq lifts to addition *) |
---|
2469 | lemma add_value_eq : |
---|
2470 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
2471 | value_eq E v1 v2 → |
---|
2472 | value_eq E v1' v2' → |
---|
2473 | (* memory_inj E m1 m2 → This injection seems useless TODO *) |
---|
2474 | ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→ |
---|
2475 | ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
2476 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2477 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2478 | [ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2479 | [ 1: whd in match (sem_add ????); normalize nodelta |
---|
2480 | cases (classify_add ty1 ty2) normalize nodelta |
---|
2481 | [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ] |
---|
2482 | #Habsurd destruct (Habsurd) |
---|
2483 | | 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
2484 | cases (classify_add ty1 ty2) normalize nodelta |
---|
2485 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2486 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
2487 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2488 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
2489 | [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ] |
---|
2490 | [ 1: @intsize_eq_elim_elim |
---|
2491 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2492 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2493 | #Heq destruct (Heq) |
---|
2494 | /3 by ex_intro, conj, vint_eq/ ] |
---|
2495 | | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct |
---|
2496 | /3 by ex_intro, conj, vint_eq/ |
---|
2497 | | 3: #Heq destruct (Heq) |
---|
2498 | normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed |
---|
2499 | @(ex_intro … (conj … (refl …) ?)) |
---|
2500 | @vptr_eq whd in match (pointer_translation ??); |
---|
2501 | cases (E b1') in Hembed; |
---|
2502 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2503 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
2504 | whd in match (shift_pointer_n ????); |
---|
2505 | cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) tsg i) offset = |
---|
2506 | (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) tsg i)) |
---|
2507 | [ 1: whd in match (offset_plus ??); |
---|
2508 | whd in match (shift_offset_n ????) in ⊢ (??%%); |
---|
2509 | >commutative_addition_n >associative_addition_n |
---|
2510 | <(commutative_addition_n … (offv offset) (offv o1')) @refl ] |
---|
2511 | #Heq >Heq @refl ] |
---|
2512 | ] |
---|
2513 | (* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
2514 | cases (classify_add ty1 ty2) normalize nodelta |
---|
2515 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2516 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2517 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2518 | [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ] |
---|
2519 | [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ] |
---|
2520 | #Heq >Heq %{r1} @conj // |
---|
2521 | /3 by ex_intro, conj, vfloat_eq/ *) |
---|
2522 | | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
2523 | cases (classify_add ty1 ty2) normalize nodelta |
---|
2524 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2525 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2526 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2527 | [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ] |
---|
2528 | [ 1,3,4,5: #Habsurd destruct (Habsurd) ] |
---|
2529 | @eq_bv_elim |
---|
2530 | [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ |
---|
2531 | | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
2532 | | 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
2533 | cases (classify_add ty1 ty2) normalize nodelta |
---|
2534 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2535 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2536 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2537 | [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ] |
---|
2538 | [ 1,3,4,5: #Habsurd destruct (Habsurd) ] |
---|
2539 | #Heq destruct (Heq) |
---|
2540 | @(ex_intro … (conj … (refl …) ?)) |
---|
2541 | @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; |
---|
2542 | elim p1 in Hembed; #b1 #o1 normalize nodelta |
---|
2543 | cases (E b1) |
---|
2544 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2545 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
2546 | whd in match (shift_pointer_n ????); |
---|
2547 | whd in match (shift_offset_n ????) in ⊢ (??%%); |
---|
2548 | whd in match (offset_plus ??); |
---|
2549 | whd in match (offset_plus ??); |
---|
2550 | >commutative_addition_n >(associative_addition_n … offset_size ?) |
---|
2551 | >(commutative_addition_n ? (offv offset) ?) @refl |
---|
2552 | ] |
---|
2553 | ] qed. |
---|
2554 | |
---|
2555 | lemma subtraction_delta : ∀x,y,delta. |
---|
2556 | subtraction offset_size |
---|
2557 | (addition_n offset_size x delta) |
---|
2558 | (addition_n offset_size y delta) = |
---|
2559 | subtraction offset_size x y. |
---|
2560 | #x #y #delta whd in match subtraction; normalize nodelta |
---|
2561 | (* Remove all the equal parts on each side of the equation. *) |
---|
2562 | <associative_addition_n |
---|
2563 | >two_complement_negation_plus |
---|
2564 | <(commutative_addition_n … (two_complement_negation ? delta)) |
---|
2565 | >(associative_addition_n ? delta) >bitvector_opp_addition_n |
---|
2566 | >(commutative_addition_n ? (zero ?)) >neutral_addition_n |
---|
2567 | @refl |
---|
2568 | qed. |
---|
2569 | |
---|
2570 | (* Offset subtraction is invariant by translation *) |
---|
2571 | lemma sub_offset_translation : |
---|
2572 | ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta). |
---|
2573 | #n #x #y #delta |
---|
2574 | whd in match (sub_offset ???) in ⊢ (??%%); |
---|
2575 | elim x #x' elim y #y' elim delta #delta' |
---|
2576 | whd in match (offset_plus ??); |
---|
2577 | whd in match (offset_plus ??); |
---|
2578 | >subtraction_delta @refl |
---|
2579 | qed. |
---|
2580 | |
---|
2581 | (* value_eq lifts to subtraction *) |
---|
2582 | lemma sub_value_eq : |
---|
2583 | ∀E,v1,v2,v1',v2',ty1,ty2,target. |
---|
2584 | value_eq E v1 v2 → |
---|
2585 | value_eq E v1' v2' → |
---|
2586 | ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→ |
---|
2587 | ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2). |
---|
2588 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2589 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2590 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2591 | [ 1: whd in match (sem_sub ?????); normalize nodelta |
---|
2592 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
2593 | [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ] |
---|
2594 | #Habsurd destruct (Habsurd) |
---|
2595 | | 2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta |
---|
2596 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
2597 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2598 | [ 2,3,4: #Habsurd destruct (Habsurd) ] |
---|
2599 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2600 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2601 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2602 | @intsize_eq_elim_elim |
---|
2603 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2604 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2605 | #Heq destruct (Heq) |
---|
2606 | /3 by ex_intro, conj, vint_eq/ |
---|
2607 | ] |
---|
2608 | (*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta |
---|
2609 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
2610 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2611 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
2612 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2613 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2614 | [ 1,2,4,5: #Habsurd destruct (Habsurd) ] |
---|
2615 | #Heq destruct (Heq) |
---|
2616 | /3 by ex_intro, conj, vfloat_eq/ *) |
---|
2617 | | 3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta |
---|
2618 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
2619 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2620 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
2621 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2622 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
2623 | [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ] |
---|
2624 | [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ |
---|
2625 | | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
2626 | | 2: cases target |
---|
2627 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
2628 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
2629 | normalize nodelta |
---|
2630 | #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] |
---|
2631 | | 4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta |
---|
2632 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
2633 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
2634 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
2635 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2636 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
2637 | [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ] |
---|
2638 | #Heq destruct (Heq) |
---|
2639 | [ 1: @(ex_intro … (conj … (refl …) ?)) |
---|
2640 | @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; |
---|
2641 | elim p1 in Hembed; #b1 #o1 normalize nodelta |
---|
2642 | cases (E b1) |
---|
2643 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
2644 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
2645 | whd in match (offset_plus ??) in ⊢ (??%%); |
---|
2646 | whd in match (neg_shift_pointer_n ?????) in ⊢ (??%%); |
---|
2647 | whd in match (neg_shift_offset_n ?????) in ⊢ (??%%); |
---|
2648 | whd in match (subtraction) in ⊢ (??%%); normalize nodelta |
---|
2649 | generalize in match (short_multiplication ???); #mult |
---|
2650 | /3 by associative_addition_n, commutative_addition_n, refl/ |
---|
2651 | ] |
---|
2652 | | 2: lapply Heq @eq_block_elim |
---|
2653 | [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) |
---|
2654 | | 1: #Hpblock1_eq normalize nodelta |
---|
2655 | elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1 |
---|
2656 | elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) |
---|
2657 | whd in ⊢ ((??%?) → (??%?) → ?); |
---|
2658 | cases (E b1') normalize nodelta |
---|
2659 | [ 1: #Habsurd destruct (Habsurd) ] |
---|
2660 | * #dest_block #dest_off normalize nodelta |
---|
2661 | #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta |
---|
2662 | cases (eqb (sizeof tsg) O) normalize nodelta |
---|
2663 | [ 1: #Habsurd destruct (Habsurd) |
---|
2664 | | 2: cases target |
---|
2665 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
2666 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
2667 | normalize nodelta |
---|
2668 | #Heq destruct (Heq) |
---|
2669 | <(sub_offset_translation 32 off1 off1' dest_off) |
---|
2670 | cases (division_u ? |
---|
2671 | (sub_offset ? off1 off1') |
---|
2672 | (repr (sizeof tsg))) in Heq; |
---|
2673 | [ 1: normalize nodelta #Habsurd destruct (Habsurd) |
---|
2674 | | 2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2) |
---|
2675 | /3 by ex_intro, conj, vint_eq/ ] |
---|
2676 | ] ] ] |
---|
2677 | ] qed. |
---|
2678 | |
---|
2679 | lemma mul_value_eq : |
---|
2680 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
2681 | value_eq E v1 v2 → |
---|
2682 | value_eq E v1' v2' → |
---|
2683 | ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→ |
---|
2684 | ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
2685 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2686 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2687 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2688 | [ 1: whd in match (sem_mul ????); normalize nodelta |
---|
2689 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2690 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2691 | #Habsurd destruct (Habsurd) |
---|
2692 | | 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
2693 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2694 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2695 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
2696 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2697 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2698 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2699 | @intsize_eq_elim_elim |
---|
2700 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2701 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2702 | #Heq destruct (Heq) |
---|
2703 | /3 by ex_intro, conj, vint_eq/ |
---|
2704 | ] |
---|
2705 | | 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
2706 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2707 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2708 | [ 1,2: #Habsurd destruct (Habsurd) ] |
---|
2709 | | 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
2710 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2711 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2712 | #Habsurd destruct (Habsurd) |
---|
2713 | ] qed. |
---|
2714 | |
---|
2715 | lemma div_value_eq : |
---|
2716 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
2717 | value_eq E v1 v2 → |
---|
2718 | value_eq E v1' v2' → |
---|
2719 | ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→ |
---|
2720 | ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
2721 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2722 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2723 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2724 | [ 1: whd in match (sem_div ????); normalize nodelta |
---|
2725 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2726 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2727 | #Habsurd destruct (Habsurd) |
---|
2728 | | 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
2729 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2730 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2731 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
2732 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2733 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2734 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2735 | elim sg normalize nodelta |
---|
2736 | @intsize_eq_elim_elim |
---|
2737 | [ 1,3: #_ #Habsurd destruct (Habsurd) |
---|
2738 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
2739 | @(match (division_s (bitsize_of_intsize sz') i i') with |
---|
2740 | [ None ⇒ ? |
---|
2741 | | Some bv' ⇒ ? ]) |
---|
2742 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
2743 | | 2: normalize #Heq destruct (Heq) |
---|
2744 | /3 by ex_intro, conj, vint_eq/ |
---|
2745 | | 3,4: elim sz' in i' i; #i' #i |
---|
2746 | normalize in match (pred_size_intsize ?); |
---|
2747 | generalize in match division_u; #division_u normalize |
---|
2748 | @(match (division_u ???) with |
---|
2749 | [ None ⇒ ? |
---|
2750 | | Some bv ⇒ ?]) normalize nodelta |
---|
2751 | #H destruct (H) |
---|
2752 | /3 by ex_intro, conj, vint_eq/ ] |
---|
2753 | ] |
---|
2754 | | 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
2755 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2756 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2757 | [ 1,2: #Habsurd destruct (Habsurd) ] |
---|
2758 | | 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
2759 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2760 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2761 | #Habsurd destruct (Habsurd) |
---|
2762 | ] qed. |
---|
2763 | |
---|
2764 | lemma mod_value_eq : |
---|
2765 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
2766 | value_eq E v1 v2 → |
---|
2767 | value_eq E v1' v2' → |
---|
2768 | ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→ |
---|
2769 | ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
2770 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2771 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2772 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2773 | [ 1: whd in match (sem_mod ????); normalize nodelta |
---|
2774 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2775 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2776 | #Habsurd destruct (Habsurd) |
---|
2777 | | 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta |
---|
2778 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
2779 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2780 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
2781 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2782 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2783 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2784 | elim sg normalize nodelta |
---|
2785 | @intsize_eq_elim_elim |
---|
2786 | [ 1,3: #_ #Habsurd destruct (Habsurd) |
---|
2787 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
2788 | @(match (modulus_s (bitsize_of_intsize sz') i i') with |
---|
2789 | [ None ⇒ ? |
---|
2790 | | Some bv' ⇒ ? ]) |
---|
2791 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
2792 | | 2: normalize #Heq destruct (Heq) |
---|
2793 | /3 by ex_intro, conj, vint_eq/ |
---|
2794 | | 3,4: elim sz' in i' i; #i' #i |
---|
2795 | generalize in match modulus_u; #modulus_u normalize |
---|
2796 | @(match (modulus_u ???) with |
---|
2797 | [ None ⇒ ? |
---|
2798 | | Some bv ⇒ ?]) normalize nodelta |
---|
2799 | #H destruct (H) |
---|
2800 | /3 by ex_intro, conj, vint_eq/ ] |
---|
2801 | ] |
---|
2802 | | *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta |
---|
2803 | cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd) |
---|
2804 | ] qed. |
---|
2805 | |
---|
2806 | (* boolean ops *) |
---|
2807 | lemma and_value_eq : |
---|
2808 | ∀E,v1,v2,v1',v2'. |
---|
2809 | value_eq E v1 v2 → |
---|
2810 | value_eq E v1' v2' → |
---|
2811 | ∀r1. (sem_and v1 v1'=Some val r1→ |
---|
2812 | ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
2813 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2814 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2815 | [ 2: #sz #i |
---|
2816 | @(value_eq_inversion E … Hvalue_eq2) |
---|
2817 | [ 2: #sz' #i' whd in match (sem_and ??); |
---|
2818 | @intsize_eq_elim_elim |
---|
2819 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2820 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2821 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
2822 | ] ] |
---|
2823 | normalize in match (sem_and ??); #arg1 destruct |
---|
2824 | normalize in match (sem_and ??); #arg2 destruct |
---|
2825 | normalize in match (sem_and ??); #arg3 destruct |
---|
2826 | normalize in match (sem_and ??); #arg4 destruct |
---|
2827 | qed. |
---|
2828 | |
---|
2829 | lemma or_value_eq : |
---|
2830 | ∀E,v1,v2,v1',v2'. |
---|
2831 | value_eq E v1 v2 → |
---|
2832 | value_eq E v1' v2' → |
---|
2833 | ∀r1. (sem_or v1 v1'=Some val r1→ |
---|
2834 | ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
2835 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2836 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2837 | [ 2: #sz #i |
---|
2838 | @(value_eq_inversion E … Hvalue_eq2) |
---|
2839 | [ 2: #sz' #i' whd in match (sem_or ??); |
---|
2840 | @intsize_eq_elim_elim |
---|
2841 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2842 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2843 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
2844 | ] ] |
---|
2845 | normalize in match (sem_or ??); #arg1 destruct |
---|
2846 | normalize in match (sem_or ??); #arg2 destruct |
---|
2847 | normalize in match (sem_or ??); #arg3 destruct |
---|
2848 | normalize in match (sem_or ??); #arg4 destruct |
---|
2849 | qed. |
---|
2850 | |
---|
2851 | lemma xor_value_eq : |
---|
2852 | ∀E,v1,v2,v1',v2'. |
---|
2853 | value_eq E v1 v2 → |
---|
2854 | value_eq E v1' v2' → |
---|
2855 | ∀r1. (sem_xor v1 v1'=Some val r1→ |
---|
2856 | ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
2857 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2858 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2859 | [ 2: #sz #i |
---|
2860 | @(value_eq_inversion E … Hvalue_eq2) |
---|
2861 | [ 2: #sz' #i' whd in match (sem_xor ??); |
---|
2862 | @intsize_eq_elim_elim |
---|
2863 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
2864 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
2865 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
2866 | ] ] |
---|
2867 | normalize in match (sem_xor ??); #arg1 destruct |
---|
2868 | normalize in match (sem_xor ??); #arg2 destruct |
---|
2869 | normalize in match (sem_xor ??); #arg3 destruct |
---|
2870 | normalize in match (sem_xor ??); #arg4 destruct |
---|
2871 | qed. |
---|
2872 | |
---|
2873 | lemma shl_value_eq : |
---|
2874 | ∀E,v1,v2,v1',v2'. |
---|
2875 | value_eq E v1 v2 → |
---|
2876 | value_eq E v1' v2' → |
---|
2877 | ∀r1. (sem_shl v1 v1'=Some val r1→ |
---|
2878 | ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
2879 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2880 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2881 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2882 | [ 2: |
---|
2883 | @(value_eq_inversion E … Hvalue_eq2) |
---|
2884 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2885 | [ 2: whd in match (sem_shl ??); |
---|
2886 | cases (lt_u ???) normalize nodelta |
---|
2887 | [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ |
---|
2888 | | 2: #Habsurd destruct (Habsurd) |
---|
2889 | ] |
---|
2890 | | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] |
---|
2891 | | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] |
---|
2892 | qed. |
---|
2893 | |
---|
2894 | lemma shr_value_eq : |
---|
2895 | ∀E,v1,v2,v1',v2',ty,ty'. |
---|
2896 | value_eq E v1 v2 → |
---|
2897 | value_eq E v1' v2' → |
---|
2898 | ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→ |
---|
2899 | ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2). |
---|
2900 | #E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
2901 | @(value_eq_inversion E … Hvalue_eq1) |
---|
2902 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
2903 | whd in match (sem_shr ????); whd in match (sem_shr ????); |
---|
2904 | [ 1: cases (classify_aop ty ty') normalize nodelta |
---|
2905 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2906 | #Habsurd destruct (Habsurd) |
---|
2907 | | 2: cases (classify_aop ty ty') normalize nodelta |
---|
2908 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
2909 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
2910 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2911 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
2912 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
2913 | elim sg normalize nodelta |
---|
2914 | cases (lt_u ???) normalize nodelta #Heq destruct (Heq) |
---|
2915 | /3 by ex_intro, conj, refl, vint_eq/ |
---|
2916 | | *: cases (classify_aop ty ty') normalize nodelta |
---|
2917 | #foo #bar |
---|
2918 | #Habsurd destruct (Habsurd) |
---|
2919 | ] qed. |
---|
2920 | |
---|
2921 | lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y. |
---|
2922 | * #delta * #x * #y |
---|
2923 | whd in match (offset_plus ??); |
---|
2924 | whd in match (offset_plus ??); |
---|
2925 | whd in match cmp_offset; normalize nodelta |
---|
2926 | whd in match eq_offset; normalize nodelta |
---|
2927 | @(eq_bv_elim … x y) |
---|
2928 | [ 1: #Heq >Heq >eq_bv_true @refl |
---|
2929 | | 2: #Hneq lapply (injective_inv_addition_n … x y delta Hneq) |
---|
2930 | @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta)) |
---|
2931 | [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ] |
---|
2932 | ] qed. |
---|
2933 | |
---|
2934 | lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y. |
---|
2935 | * #delta * #x * #y |
---|
2936 | whd in match (offset_plus ??); |
---|
2937 | whd in match (offset_plus ??); |
---|
2938 | whd in match cmp_offset; normalize nodelta |
---|
2939 | whd in match eq_offset; normalize nodelta |
---|
2940 | @(eq_bv_elim … x y) |
---|
2941 | [ 1: #Heq >Heq >eq_bv_true @refl |
---|
2942 | | 2: #Hneq lapply (injective_inv_addition_n … x y delta Hneq) |
---|
2943 | @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta)) |
---|
2944 | [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ] |
---|
2945 | ] qed. |
---|
2946 | |
---|
2947 | (* Note that x and y are bounded below and above, similarly for the shifted offsets. |
---|
2948 | This is enough to prove that there is no "wrap-around-the-end" problem, |
---|
2949 | /provided we know that the block bounds are implementable by 2^16 bitvectors/. |
---|
2950 | We axiomatize it for now. *) |
---|
2951 | axiom cmp_offset_translation : |
---|
2952 | ∀op,delta,x,y. |
---|
2953 | (Zoo x) + (Zoo delta) < Z_two_power_nat 16 → |
---|
2954 | (Zoo y) + (Zoo delta) < Z_two_power_nat 16 → |
---|
2955 | cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). |
---|
2956 | |
---|
2957 | lemma valid_pointer_of_implementable_block_is_implementable : |
---|
2958 | ∀m,b. |
---|
2959 | block_implementable_bv m b → |
---|
2960 | ∀o. valid_pointer m (mk_pointer b o) = true → |
---|
2961 | Zoo o < Z_two_power_nat 16. |
---|
2962 | #m #b whd in ⊢ (% → ?); * #Hlow #Hhigh |
---|
2963 | * #o #Hvalid cases (valid_pointer_to_Prop … Hvalid) * #_ |
---|
2964 | #Hlow' #Hhigh' |
---|
2965 | cases Hlow -Hlow #Hlow0 #Hlow16 |
---|
2966 | cases Hhigh -Hhigh #Hhigh0 #Hhigh16 |
---|
2967 | whd in match (Zoo ?); |
---|
2968 | @(transitive_Zlt … Hhigh' Hhigh16) |
---|
2969 | qed. |
---|
2970 | |
---|
2971 | lemma cmp_value_eq : |
---|
2972 | ∀E,v1,v2,v1',v2',ty,ty',m1,m2. |
---|
2973 | value_eq E v1 v2 → |
---|
2974 | value_eq E v1' v2' → |
---|
2975 | memory_inj E m1 m2 → |
---|
2976 | ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1 → |
---|
2977 | ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). |
---|
2978 | #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 |
---|
2979 | elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj |
---|
2980 | whd in match (sem_cmp ??????) in ⊢ ((??%?) → %); |
---|
2981 | cases (classify_cmp ty ty') normalize nodelta |
---|
2982 | [ 1: #tsz #tsg |
---|
2983 | @(value_eq_inversion E … Hvalue_eq1) normalize nodelta |
---|
2984 | [ 1: #Habsurd destruct (Habsurd) |
---|
2985 | | 3: #Habsurd destruct (Habsurd) |
---|
2986 | | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
2987 | #sz #i |
---|
2988 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
2989 | [ 1: #Habsurd destruct (Habsurd) |
---|
2990 | | 3: #Habsurd destruct (Habsurd) |
---|
2991 | | 4: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
2992 | #sz' #i' cases tsg normalize nodelta |
---|
2993 | @intsize_eq_elim_elim |
---|
2994 | [ 1,3: #Hneq #Habsurd destruct (Habsurd) |
---|
2995 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
2996 | #Heq destruct (Heq) |
---|
2997 | [ 1: cases (cmp_int ????) whd in match (of_bool ?); |
---|
2998 | | 2: cases (cmpu_int ????) whd in match (of_bool ?); ] |
---|
2999 | /3 by ex_intro, conj, vint_eq/ ] |
---|
3000 | | 3: #ty1 #ty2 #Habsurd destruct (Habsurd) |
---|
3001 | | 2: lapply Hinj -Hinj |
---|
3002 | generalize in match (mk_mem contmap1 ??); #m1 |
---|
3003 | generalize in match (mk_mem contmap2 ??); #m2 |
---|
3004 | #Hinj #optn #typ |
---|
3005 | @(value_eq_inversion E … Hvalue_eq1) normalize nodelta |
---|
3006 | [ 1: #Habsurd destruct (Habsurd) |
---|
3007 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
3008 | | 4: #p1 #p2 #Hembed ] |
---|
3009 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
3010 | [ 1,5: #Habsurd destruct (Habsurd) |
---|
3011 | | 2,6: #sz #i #Habsurd destruct (Habsurd) |
---|
3012 | | 4,8: #q1 #q2 #Hembed' ] |
---|
3013 | [ 2,3: cases op whd in match (sem_cmp_mismatch ?); |
---|
3014 | #Heq destruct (Heq) |
---|
3015 | [ 1,3: %{Vfalse} @conj try @refl @vint_eq |
---|
3016 | | 2,4: %{Vtrue} @conj try @refl @vint_eq ] |
---|
3017 | | 4: cases op whd in match (sem_cmp_match ?); |
---|
3018 | #Heq destruct (Heq) |
---|
3019 | [ 2,4: %{Vfalse} @conj try @refl @vint_eq |
---|
3020 | | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ] |
---|
3021 | #Hvalid |
---|
3022 | lapply (if_opt_inversion ???? Hvalid) -Hvalid * #Hconj |
---|
3023 | lapply (andb_inversion … Hconj) -Hconj * #Hvalid #Hvalid' |
---|
3024 | lapply (mi_valid_pointers … Hinj q1 q2 Hvalid' Hembed') #Hvalid2' >Hvalid2' |
---|
3025 | lapply (mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) #Hvalid2 >Hvalid2 |
---|
3026 | normalize nodelta |
---|
3027 | (* >(mi_valid_pointers … Hinj p1' p2' Hvalid' Hembed') |
---|
3028 | >(mi_valid_pointers … Hinj p1 p2 Hvalid Hembed) normalize nodelta *) |
---|
3029 | elim p1 in Hvalid Hembed; #bp1 #op1 |
---|
3030 | elim q1 in Hvalid' Hembed'; #bq1 #oq1 |
---|
3031 | #Hvalid' #Htmp #Hvalid lapply Htmp -Htmp |
---|
3032 | whd in match (pointer_translation ??); |
---|
3033 | whd in match (pointer_translation ??); |
---|
3034 | @(eq_block_elim … bp1 bq1) |
---|
3035 | [ 1: #Heq destruct (Heq) normalize nodelta |
---|
3036 | lapply (mi_nowrap … Hinj bq1) |
---|
3037 | whd in ⊢ (% → ?); |
---|
3038 | cases (E bq1) normalize nodelta |
---|
3039 | [ #_ #Habsurd destruct ] |
---|
3040 | * #BLO #OFF normalize nodelta * * |
---|
3041 | #Hbq1_implementable #HBLO_implementable #Hno_wrap |
---|
3042 | #Heq1 #Heq2 #Heq3 destruct |
---|
3043 | >eq_block_b_b normalize nodelta |
---|
3044 | lapply (cmp_offset_translation op OFF op1 oq1 ??) |
---|
3045 | [ @(Zlt_sum_weaken … Hno_wrap) |
---|
3046 | cases (valid_pointer_to_Prop … Hvalid') * #_ #_ try // |
---|
3047 | | @(Zlt_sum_weaken … Hno_wrap) |
---|
3048 | cases (valid_pointer_to_Prop … Hvalid) * #_ #_ try // ] |
---|
3049 | #Heq <Heq |
---|
3050 | cases (cmp_offset op op1 oq1) |
---|
3051 | normalize nodelta |
---|
3052 | try /3 by ex_intro, conj, refl, vint_eq/ |
---|
3053 | | 2: #Hneq lapply (mi_nonalias … Hinj bp1 bq1) |
---|
3054 | normalize nodelta |
---|
3055 | lapply (mi_nowrap … Hinj bp1) whd in ⊢ (% → ?); |
---|
3056 | lapply (mi_nowrap … Hinj bq1) whd in ⊢ (% → ?); |
---|
3057 | lapply (mi_region … Hinj bq1) |
---|
3058 | lapply (mi_region … Hinj bp1) |
---|
3059 | cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
3060 | * #BLOq #DELTAq normalize nodelta |
---|
3061 | cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ] |
---|
3062 | * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct |
---|
3063 | lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) -Hregion1 -Hregion2 |
---|
3064 | #Hregion2 #Hregion1 |
---|
3065 | cases op |
---|
3066 | whd in ⊢ ((??%?) → ?); #H' destruct (H') |
---|
3067 | whd in match (sem_cmp_mismatch ?); |
---|
3068 | lapply (H ???? Hneq (refl ??) (refl ??)) -H |
---|
3069 | cases (block_decidable_eq BLOp BLOq) normalize nodelta |
---|
3070 | #H |
---|
3071 | [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2 |
---|
3072 | | 4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ] |
---|
3073 | destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %; |
---|
3074 | #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1 |
---|
3075 | * * #Himplp1 #_ #Hnowrap_p1 #Hvalid2 #Hvalid2' |
---|
3076 | lapply (valid_pointer_to_Prop … Hvalid) |
---|
3077 | lapply (valid_pointer_to_Prop … Hvalid') |
---|
3078 | * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp |
---|
3079 | >eq_block_b_b normalize nodelta |
---|
3080 | * |
---|
3081 | [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind |
---|
3082 | cases (valid_pointer_to_Prop … Hvalid') * #_ #Hle #Hlt |
---|
3083 | lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt' |
---|
3084 | lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl |
---|
3085 | @(absurd … Hlt_refl (irreflexive_Zlt ?)) ] |
---|
3086 | * |
---|
3087 | [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind |
---|
3088 | cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt |
---|
3089 | lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt' |
---|
3090 | lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl |
---|
3091 | @(absurd … Hlt_refl (irreflexive_Zlt ?)) ] |
---|
3092 | * |
---|
3093 | #Hdisjoint |
---|
3094 | whd in match (cmp_offset); normalize nodelta |
---|
3095 | whd in match (eq_offset); normalize nodelta |
---|
3096 | whd in match (offset_plus ??); |
---|
3097 | whd in match (offset_plus ??); |
---|
3098 | lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2) |
---|
3099 | lapply (valid_pointer_of_implementable_block_is_implementable … Himpltarget … Hvalid2') |
---|
3100 | #Himpl1 #Himpl2 |
---|
3101 | [ 1,3: |
---|
3102 | (* We show the non-equality of the rhs by exhibiting disjointness of blocks. This is made |
---|
3103 | * painful by invariants on non-overflowing offsets. We exhibit [a]+[b] < [c]+[d], then |
---|
3104 | * cut [a+b]<[c+d] (using a subcut for needed consistency hypotheses) and conclude easily |
---|
3105 | * [a+b] ≠ [c+d]. *) |
---|
3106 | cut ((Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp)) |
---|
3107 | < (Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq))) |
---|
3108 | [ 1,3: |
---|
3109 | @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bp1 + Zoo DELTAp) ?) |
---|
3110 | [ 1,3: @Zlt_translate assumption |
---|
3111 | | 2,4: @(transitive_Zle ? (low_bound m1 bq1+Zoo DELTAq) ?) try assumption |
---|
3112 | @monotonic_Zle_Zplus_l try assumption ] |
---|
3113 | ] |
---|
3114 | #Hlt_stepA |
---|
3115 | cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp)) |
---|
3116 | < Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq))) |
---|
3117 | [ 1,3: |
---|
3118 | >Z_addition_bv_commute |
---|
3119 | [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ] |
---|
3120 | >Z_addition_bv_commute |
---|
3121 | [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ] |
---|
3122 | try assumption ] -Hlt_stepA |
---|
3123 | | 2,4: |
---|
3124 | cut ((Z_of_unsigned_bitvector ? (offv oq1)) + (Z_of_unsigned_bitvector ? (offv DELTAq)) |
---|
3125 | < (Z_of_unsigned_bitvector ? (offv op1)) + (Z_of_unsigned_bitvector ? (offv DELTAp))) |
---|
3126 | [ 1,3: |
---|
3127 | @(Zlt_to_Zle_to_Zlt ? (high_bound m1 bq1 + Zoo DELTAq) ?) |
---|
3128 | [ 1,3: @Zlt_translate assumption |
---|
3129 | | 2,4: @(transitive_Zle ? (low_bound m1 bp1+Zoo DELTAp) ?) try assumption |
---|
3130 | @monotonic_Zle_Zplus_l try assumption ] |
---|
3131 | ] |
---|
3132 | #Hlt_stepA |
---|
3133 | cut (Z_of_unsigned_bitvector ? (addition_n offset_size (offv oq1) (offv DELTAq)) |
---|
3134 | < Z_of_unsigned_bitvector ? (addition_n offset_size (offv op1) (offv DELTAp))) |
---|
3135 | [ 1,3: |
---|
3136 | >Z_addition_bv_commute |
---|
3137 | [ 2,4: @(transitive_Zlt … Hnowrap_q1) @Zlt_translate try assumption ] |
---|
3138 | >Z_addition_bv_commute |
---|
3139 | [ 2,4: @(transitive_Zlt … Hnowrap_p1) @Zlt_translate try assumption ] |
---|
3140 | try assumption ] -Hlt_stepA |
---|
3141 | ] |
---|
3142 | generalize in match (addition_n ? (offv op1) ?); #lhs |
---|
3143 | generalize in match (addition_n ? (offv oq1) ?); #rhs |
---|
3144 | #Hlt_stepB lapply (Zlt_to_Zneq … Hlt_stepB) |
---|
3145 | @(eq_bv_elim … lhs rhs) |
---|
3146 | [ 1,3,5,7: #Heq destruct * #H @(False_ind … (H (refl ??))) |
---|
3147 | | 2,4,6,8: #Hneq #_ /3 by ex_intro, conj, vint_eq/ ] |
---|
3148 | ] |
---|
3149 | ] qed. |
---|
3150 | |
---|