[2312] | 1 | include "Clight/Cexec.ma". |
---|
[2468] | 2 | include "Clight/MemProperties.ma". |
---|
[2385] | 3 | include "Clight/frontend_misc.ma". |
---|
[2312] | 4 | |
---|
| 5 | (* This file contains some definitions and lemmas related to memory injections. |
---|
| 6 | Could be useful for the Clight → Cminor. Needs revision: the definitions are |
---|
| 7 | too lax and allow inconsistent embeddings (more precisely, these embeddings do |
---|
| 8 | not allow to prove that the semantics for pointer less-than comparisons is |
---|
| 9 | conserved). *) |
---|
| 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 | |
---|
[2468] | 32 | (* --------------------------------------------------------------------------- *) |
---|
| 33 | (* Some shorthands for conversion functions from BitVectorZ. *) |
---|
| 34 | (* --------------------------------------------------------------------------- *) |
---|
| 35 | |
---|
| 36 | definition Zoub ≝ Z_of_unsigned_bitvector. |
---|
| 37 | definition boZ ≝ bitvector_of_Z. |
---|
| 38 | |
---|
| 39 | (* Offsets are just bitvectors packed inside some useless and annoying constructor. *) |
---|
| 40 | definition Zoo ≝ λx. Zoub ? (offv x). |
---|
| 41 | definition boo ≝ λx. mk_offset (boZ ? x). |
---|
| 42 | |
---|
[2312] | 43 | (* --------------------------------------------------------------------------- *) |
---|
| 44 | (* In the definition of injections below, we maintain a list of blocks that are |
---|
| 45 | writeable. We need some lemmas to reason on the fact that a block cannot be |
---|
| 46 | both writeable and not writeable, etc. *) |
---|
| 47 | (* --------------------------------------------------------------------------- *) |
---|
| 48 | |
---|
| 49 | (* When equality on A is decidable, [mem A elt l] is too. *) |
---|
| 50 | lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l). |
---|
| 51 | #A #dec #elt #l elim l |
---|
| 52 | [ 1: normalize %2 /2/ |
---|
| 53 | | 2: #hd #tl #Hind |
---|
| 54 | elim (dec elt hd) |
---|
| 55 | [ 1: #Heq >Heq %1 /2/ |
---|
| 56 | | 2: #Hneq cases Hind |
---|
| 57 | [ 1: #Hmem %1 /2/ |
---|
| 58 | | 2: #Hnmem %2 normalize |
---|
| 59 | % #H cases H |
---|
| 60 | [ 1: lapply Hneq * #Hl #Eq @(Hl Eq) |
---|
| 61 | | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ] |
---|
| 62 | ] ] ] |
---|
| 63 | qed. |
---|
| 64 | |
---|
| 65 | lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b. |
---|
| 66 | #a #b @(eq_block_elim … a b) /2/ qed. |
---|
| 67 | |
---|
| 68 | lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2. |
---|
| 69 | #l #elt1 #elt2 elim l |
---|
| 70 | [ 1: normalize #Habsurd @(False_ind … Habsurd) |
---|
| 71 | | 2: #hd #tl #Hind normalize #Hl #Hr |
---|
| 72 | cases Hl |
---|
| 73 | [ 1: #Heq >Heq |
---|
| 74 | @(eq_block_elim … hd elt2) |
---|
| 75 | [ 1: #Heq >Heq /2 by not_to_not/ |
---|
| 76 | | 2: #x @x ] |
---|
| 77 | | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl) |
---|
| 78 | [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2 |
---|
| 79 | | 2: #Hmem2 @Hind // |
---|
| 80 | ] |
---|
| 81 | ] |
---|
| 82 | ] qed. |
---|
| 83 | |
---|
| 84 | lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false. |
---|
| 85 | #b1 #b2 * #Hb |
---|
| 86 | @(eq_block_elim … b1 b2) |
---|
| 87 | [ 1: #Habsurd @(False_ind … (Hb Habsurd)) |
---|
| 88 | | 2: // ] qed. |
---|
| 89 | |
---|
| 90 | (* --------------------------------------------------------------------------- *) |
---|
[2332] | 91 | (* Lemmas related to freeing memory and pointer validity. *) |
---|
| 92 | (* --------------------------------------------------------------------------- *) |
---|
| 93 | (* |
---|
| 94 | lemma nextblock_free_ok : ∀m,b. nextblock m = nextblock (free m b). |
---|
| 95 | * #contents #next #posnext * #rg #id |
---|
| 96 | normalize @refl |
---|
| 97 | qed. |
---|
| 98 | |
---|
| 99 | lemma low_bound_free_ok : ∀m,b,ptr. |
---|
| 100 | b ≠ (pblock ptr) → |
---|
| 101 | Zleb (low_bound (free m b) (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = |
---|
| 102 | Zleb (low_bound m (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))). |
---|
| 103 | * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize |
---|
| 104 | cases prg cases brg normalize nodelta try // |
---|
| 105 | @(eqZb_elim pid bid) |
---|
| 106 | [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??))) |
---|
| 107 | | 2,4: #_ #_ @refl |
---|
| 108 | ] qed. |
---|
| 109 | |
---|
| 110 | lemma high_bound_free_ok : ∀m,b,ptr. |
---|
| 111 | b ≠ (pblock ptr) → |
---|
| 112 | Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound (free m b) (pblock ptr)) = |
---|
| 113 | Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound m (pblock ptr)). |
---|
| 114 | * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize |
---|
| 115 | cases prg cases brg normalize nodelta try // |
---|
| 116 | @(eqZb_elim pid bid) |
---|
| 117 | [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??))) |
---|
| 118 | | 2,4: #_ #_ @refl |
---|
| 119 | ] qed. |
---|
| 120 | |
---|
| 121 | lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr. |
---|
| 122 | valid_pointer m ptr = true → |
---|
| 123 | pblock ptr ≠ b → |
---|
| 124 | valid_pointer (free m b) ptr = true. |
---|
| 125 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
| 126 | normalize |
---|
| 127 | @(eqZb_elim pbid bid) |
---|
| 128 | [ 1: #Heqid >Heqid cases pbr cases br normalize |
---|
| 129 | [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ] |
---|
| 130 | cases (Zltb bid next) normalize nodelta |
---|
| 131 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
| 132 | // |
---|
| 133 | | 2: #Hneqid cases pbr cases br normalize try // ] |
---|
| 134 | qed. |
---|
| 135 | |
---|
| 136 | lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr. |
---|
| 137 | valid_pointer m ptr = true → |
---|
| 138 | ¬ mem ? (pblock ptr) blocks → |
---|
| 139 | valid_pointer (free_list m blocks) ptr = true. |
---|
| 140 | #blocks |
---|
| 141 | elim blocks |
---|
| 142 | [ 1: #m #ptr normalize #H #_ @H |
---|
| 143 | | 2: #b #tl #Hind #m #ptr #Hvalid |
---|
| 144 | whd in match (mem block (pblock ptr) ?); |
---|
| 145 | >free_list_cons * #Hguard |
---|
| 146 | @valid_pointer_free_ok |
---|
| 147 | [ 2: % #Heq @Hguard %1 @Heq ] |
---|
| 148 | @Hind |
---|
| 149 | [ 1: @Hvalid |
---|
| 150 | | 2: % #Hmem @Hguard %2 @Hmem ] |
---|
| 151 | ] qed. *) |
---|
| 152 | |
---|
[2448] | 153 | |
---|
[2332] | 154 | lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr. |
---|
| 155 | valid_pointer m ptr = true → |
---|
| 156 | pblock ptr ≠ b → |
---|
| 157 | valid_pointer (free m b) ptr = true. |
---|
| 158 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
| 159 | normalize |
---|
| 160 | @(eqZb_elim pbid bid) |
---|
| 161 | [ 1: #Heqid >Heqid cases pbr cases br normalize |
---|
| 162 | [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ] |
---|
| 163 | cases (Zltb bid next) normalize nodelta |
---|
| 164 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
| 165 | // |
---|
| 166 | | 2: #Hneqid cases pbr cases br normalize try // ] |
---|
| 167 | qed. |
---|
| 168 | |
---|
| 169 | lemma free_list_cons : ∀m,b,tl. free_list m (b :: tl) = (free (free_list m tl) b). |
---|
| 170 | #m #b #tl whd in match (free_list ??) in ⊢ (??%%); |
---|
| 171 | whd in match (free ??); @refl qed. |
---|
| 172 | |
---|
| 173 | lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr. |
---|
| 174 | valid_pointer (free m b) ptr = true → |
---|
| 175 | pblock ptr ≠ b → (* This hypothesis is necessary to handle the cse of "valid" pointers to empty *) |
---|
| 176 | valid_pointer m ptr = true. |
---|
| 177 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
| 178 | @(eqZb_elim pbid bid) |
---|
| 179 | [ 1: #Heqid >Heqid |
---|
| 180 | cases pbr cases br normalize |
---|
| 181 | [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ] |
---|
| 182 | cases (Zltb bid next) normalize nodelta |
---|
| 183 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
| 184 | // |
---|
| 185 | | 2: #Hneqid cases pbr cases br normalize try // |
---|
| 186 | >(eqZb_false … Hneqid) normalize nodelta try // |
---|
| 187 | qed. |
---|
| 188 | |
---|
| 189 | lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr. |
---|
| 190 | valid_pointer (free_list m blocks) ptr = true → |
---|
| 191 | ¬ mem ? (pblock ptr) blocks → |
---|
| 192 | valid_pointer m ptr = true. |
---|
| 193 | #blocks |
---|
| 194 | elim blocks |
---|
| 195 | [ 1: #m #ptr normalize #H #_ @H |
---|
| 196 | | 2: #b #tl #Hind #m #ptr #Hvalid |
---|
| 197 | whd in match (mem block (pblock ptr) ?); |
---|
| 198 | >free_list_cons in Hvalid; #Hvalid * #Hguard |
---|
| 199 | lapply (valid_pointer_free_ok … Hvalid) #H |
---|
| 200 | @Hind |
---|
| 201 | [ 2: % #Heq @Hguard %2 @Heq |
---|
| 202 | | 1: @H % #Heq @Hguard %1 @Heq ] |
---|
| 203 | ] qed. |
---|
| 204 | |
---|
| 205 | (* An alternative version without the gard on the equality of blocks. *) |
---|
| 206 | lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr. |
---|
| 207 | valid_pointer (free m b) ptr = true → |
---|
| 208 | (pblock ptr) = b ∨ (pblock ptr ≠ b ∧ valid_pointer m ptr = true). |
---|
| 209 | * #br #bid * #contents #next #posnext * * #pbr #pbid #poff |
---|
| 210 | @(eq_block_elim … (mk_block br bid) (mk_block pbr pbid)) |
---|
| 211 | [ 1: #Heq #_ %1 @(sym_eq … Heq) |
---|
| 212 | | 2: cases pbr cases br normalize nodelta |
---|
| 213 | [ 1,4: @(eqZb_elim pbid bid) |
---|
| 214 | [ 1,3: #Heq >Heq * #H @(False_ind … (H (refl ??))) |
---|
| 215 | | 2,4: #Hneq #_ normalize >(eqZb_false … Hneq) normalize nodelta |
---|
| 216 | #H %2 @conj try assumption |
---|
| 217 | % #Habsurd destruct (Habsurd) elim Hneq #Hneq @Hneq try @refl |
---|
| 218 | ] |
---|
| 219 | | *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ] |
---|
| 220 | ] qed. |
---|
| 221 | |
---|
| 222 | (* Well in fact a valid pointer can be valid even after a free. Ah. *) |
---|
| 223 | (* |
---|
| 224 | lemma pointer_in_free_list_not_valid : ∀blocks,m,ptr. |
---|
| 225 | mem ? (pblock ptr) blocks → |
---|
| 226 | valid_pointer (free_list m blocks) ptr = false. |
---|
| 227 | *) |
---|
| 228 | (* |
---|
| 229 | #blocks elim blocks |
---|
| 230 | [ 1: #m #ptr normalize #Habsurd @(False_ind … Habsurd) |
---|
| 231 | | 2: #b #tl #Hind #m #ptr |
---|
| 232 | whd in match (mem block (pblock ptr) ?); |
---|
| 233 | >free_list_cons |
---|
| 234 | * |
---|
| 235 | [ 1: #Hptr_match whd in match (free ??); |
---|
| 236 | whd in match (update_block ????); |
---|
| 237 | whd in match (valid_pointer ??); |
---|
| 238 | whd in match (low_bound ??); |
---|
| 239 | whd in match (high_bound ??); |
---|
| 240 | >Hptr_match >eq_block_identity normalize nodelta |
---|
| 241 | whd in match (low ?); |
---|
| 242 | cut (Zleb OZ (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) = true) |
---|
| 243 | [ 1: elim (offv (poff ptr)) // |
---|
| 244 | #n' #hd #tl cases hd normalize |
---|
| 245 | [ 1: #_ try @refl |
---|
| 246 | | 2: #H @H ] ] |
---|
| 247 | #H >H |
---|
| 248 | cut (Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) OZ = false) |
---|
| 249 | [ 1: elim (offv (poff ptr)) normalize |
---|
| 250 | #n' #hd #tl cases hd normalize |
---|
| 251 | [ 1: normalize #_ try @refl |
---|
| 252 | | 2: #H @H ] ] |
---|
| 253 | valid_pointer (free_list m blocks) ptr = false. |
---|
| 254 | *) |
---|
| 255 | |
---|
| 256 | |
---|
| 257 | (* --------------------------------------------------------------------------- *) |
---|
[2312] | 258 | (* Memory injections *) |
---|
| 259 | (* --------------------------------------------------------------------------- *) |
---|
| 260 | |
---|
| 261 | (* An embedding is a function from blocks to (blocks × offset). *) |
---|
| 262 | definition embedding ≝ block → option (block × offset). |
---|
| 263 | |
---|
| 264 | definition offset_plus : offset → offset → offset ≝ |
---|
| 265 | λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)). |
---|
| 266 | |
---|
| 267 | lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o. |
---|
| 268 | * #o |
---|
| 269 | whd in match (offset_plus ??); |
---|
| 270 | >addition_n_0 @refl |
---|
| 271 | qed. |
---|
| 272 | |
---|
| 273 | (* Translates a pointer through an embedding. *) |
---|
| 274 | definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝ |
---|
| 275 | λp,E. |
---|
| 276 | match p with |
---|
| 277 | [ mk_pointer pblock poff ⇒ |
---|
| 278 | match E pblock with |
---|
| 279 | [ None ⇒ None ? |
---|
| 280 | | Some loc ⇒ |
---|
| 281 | let 〈dest_block,dest_off〉 ≝ loc in |
---|
| 282 | let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in |
---|
| 283 | Some ? ptr |
---|
| 284 | ] |
---|
| 285 | ]. |
---|
| 286 | |
---|
| 287 | (* We parameterise the "equivalence" relation on values with an embedding. *) |
---|
| 288 | (* Front-end values. *) |
---|
| 289 | inductive value_eq (E : embedding) : val → val → Prop ≝ |
---|
[2468] | 290 | | undef_eq : |
---|
| 291 | value_eq E Vundef Vundef |
---|
[2312] | 292 | | vint_eq : ∀sz,i. |
---|
| 293 | value_eq E (Vint sz i) (Vint sz i) |
---|
| 294 | | vnull_eq : |
---|
| 295 | value_eq E Vnull Vnull |
---|
| 296 | | vptr_eq : ∀p1,p2. |
---|
| 297 | pointer_translation p1 E = Some ? p2 → |
---|
| 298 | value_eq E (Vptr p1) (Vptr p2). |
---|
| 299 | |
---|
| 300 | (* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. |
---|
| 301 | * the values are equivalent. *) |
---|
| 302 | definition load_sim ≝ |
---|
| 303 | λ(E : embedding).λ(m1 : mem).λ(m2 : mem). |
---|
| 304 | ∀b1,off1,b2,off2,ty,v1. |
---|
| 305 | 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 *) |
---|
| 306 | E b1 = Some ? 〈b2,off2〉 → |
---|
| 307 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
| 308 | (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). |
---|
| 309 | |
---|
| 310 | definition load_sim_ptr ≝ |
---|
| 311 | λ(E : embedding).λ(m1 : mem).λ(m2 : mem). |
---|
| 312 | ∀b1,off1,b2,off2,ty,v1. |
---|
| 313 | 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 *) |
---|
| 314 | pointer_translation (mk_pointer b1 off1) E = Some ? (mk_pointer b2 off2) → |
---|
| 315 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
| 316 | (∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2). |
---|
[2468] | 317 | |
---|
| 318 | (* Adapted from Compcert's Memory *) |
---|
| 319 | definition non_aliasing : embedding → mem → Prop ≝ |
---|
| 320 | λE,m. |
---|
| 321 | ∀b1,b2,b1',b2',delta1,delta2. |
---|
| 322 | b1 ≠ b2 → |
---|
| 323 | E b1 = Some ? 〈b1',delta1〉 → |
---|
| 324 | E b2 = Some ? 〈b2',delta2〉 → |
---|
| 325 | (b1' ≠ b2') ∨ |
---|
| 326 | high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ |
---|
| 327 | high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1). |
---|
| 328 | |
---|
[2312] | 329 | (* Definition of a memory injection *) |
---|
[2468] | 330 | record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Prop ≝ |
---|
[2312] | 331 | { (* Load simulation *) |
---|
| 332 | mi_inj : load_sim_ptr E m1 m2; |
---|
| 333 | (* Invalid blocks are not mapped *) |
---|
| 334 | mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; |
---|
| 335 | (* Valid pointers are mapped to valid pointers*) |
---|
| 336 | mi_valid_pointers : ∀p,p'. |
---|
| 337 | valid_pointer m1 p = true → |
---|
| 338 | pointer_translation p E = Some ? p' → |
---|
| 339 | valid_pointer m2 p' = true; |
---|
| 340 | (* Blocks in the codomain are valid *) |
---|
| 341 | (* mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; *) |
---|
| 342 | (* Regions are preserved *) |
---|
| 343 | mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; |
---|
[2468] | 344 | (* sub-blocks do not overlap (non-aliasing property) *) |
---|
| 345 | mi_nonalias : non_aliasing E m1 |
---|
[2312] | 346 | }. |
---|
| 347 | |
---|
| 348 | (* ---------------------------------------------------------------------------- *) |
---|
| 349 | (* End of the definitions on memory injections. Now, on to proving some lemmas. *) |
---|
| 350 | |
---|
| 351 | (* A particular inversion. *) |
---|
| 352 | lemma value_eq_ptr_inversion : |
---|
| 353 | ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2. |
---|
| 354 | #E #p1 #v #Heq inversion Heq |
---|
[2468] | 355 | [ 1: #Habsurd destruct (Habsurd) |
---|
[2312] | 356 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
[2468] | 357 | | 3: #Habsurd destruct (Habsurd) |
---|
| 358 | | 4: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct |
---|
[2312] | 359 | %{p2} @conj try @refl try assumption |
---|
| 360 | ] qed. |
---|
| 361 | |
---|
| 362 | (* A cleaner version of inversion for [value_eq] *) |
---|
| 363 | lemma value_eq_inversion : |
---|
| 364 | ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → |
---|
[2468] | 365 | (P Vundef Vundef) → |
---|
[2312] | 366 | (∀sz,i. P (Vint sz i) (Vint sz i)) → |
---|
| 367 | (P Vnull Vnull) → |
---|
| 368 | (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) → |
---|
| 369 | P v1 v2. |
---|
[2468] | 370 | #E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 |
---|
[2312] | 371 | inversion Heq |
---|
[2468] | 372 | [ 1: #Hv1 #Hv2 #_ destruct @H1 |
---|
[2312] | 373 | | 2: #sz #i #Hv1 #Hv2 #_ destruct @H2 |
---|
[2468] | 374 | | 3: #Hv1 #Hv2 #_ destruct @H3 |
---|
| 375 | | 4: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H4 // ] qed. |
---|
| 376 | |
---|
[2312] | 377 | (* If we succeed to load something by value from a 〈b,off〉 location, |
---|
| 378 | [b] is a valid block. *) |
---|
| 379 | lemma load_by_value_success_valid_block_aux : |
---|
| 380 | ∀ty,m,b,off,v. |
---|
| 381 | access_mode ty = By_value (typ_of_type ty) → |
---|
| 382 | load_value_of_type ty m b off = Some ? v → |
---|
| 383 | Zltb (block_id b) (nextblock m) = true. |
---|
| 384 | #ty #m * #brg #bid #off #v |
---|
| 385 | cases ty |
---|
[2468] | 386 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 387 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2312] | 388 | whd in match (load_value_of_type ????); |
---|
[2468] | 389 | [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] |
---|
[2312] | 390 | #Hmode |
---|
[2468] | 391 | [ 1,2,5: [ 1: elim sz ] |
---|
[2312] | 392 | normalize in match (typesize ?); |
---|
| 393 | whd in match (loadn ???); |
---|
| 394 | whd in match (beloadv ??); |
---|
| 395 | cases (Zltb bid (nextblock m)) normalize nodelta |
---|
| 396 | try // #Habsurd destruct (Habsurd) |
---|
| 397 | | *: normalize in Hmode; destruct (Hmode) |
---|
| 398 | ] qed. |
---|
| 399 | |
---|
| 400 | (* If we succeed in loading some data from a location, then this loc is a valid pointer. *) |
---|
| 401 | lemma load_by_value_success_valid_ptr_aux : |
---|
| 402 | ∀ty,m,b,off,v. |
---|
| 403 | access_mode ty = By_value (typ_of_type ty) → |
---|
| 404 | load_value_of_type ty m b off = Some ? v → |
---|
| 405 | Zltb (block_id b) (nextblock m) = true ∧ |
---|
| 406 | Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ |
---|
| 407 | Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. |
---|
| 408 | #ty #m * #brg #bid #off #v |
---|
| 409 | cases ty |
---|
[2468] | 410 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 411 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2312] | 412 | whd in match (load_value_of_type ????); |
---|
[2468] | 413 | [ 1,6,7: #_ #Habsurd destruct (Habsurd) ] |
---|
[2312] | 414 | #Hmode |
---|
[2468] | 415 | [ 1,2,5: [ 1: elim sz ] |
---|
[2312] | 416 | normalize in match (typesize ?); |
---|
| 417 | whd in match (loadn ???); |
---|
| 418 | whd in match (beloadv ??); |
---|
| 419 | cases (Zltb bid (nextblock m)) normalize nodelta |
---|
| 420 | cases (Zleb (low (blocks m (mk_block brg bid))) |
---|
| 421 | (Z_of_unsigned_bitvector offset_size (offv off))) |
---|
| 422 | cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brg bid)))) |
---|
| 423 | normalize nodelta |
---|
| 424 | #Heq destruct (Heq) |
---|
| 425 | try /3 by conj, refl/ |
---|
| 426 | | *: normalize in Hmode; destruct (Hmode) |
---|
| 427 | ] qed. |
---|
| 428 | |
---|
| 429 | lemma load_by_value_success_valid_block : |
---|
| 430 | ∀ty,m,b,off,v. |
---|
| 431 | access_mode ty = By_value (typ_of_type ty) → |
---|
| 432 | load_value_of_type ty m b off = Some ? v → |
---|
| 433 | valid_block m b. |
---|
| 434 | #ty #m #b #off #v #Haccess_mode #Hload |
---|
[2468] | 435 | @Zltb_true_to_Zlt |
---|
[2312] | 436 | elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) * // |
---|
| 437 | qed. |
---|
| 438 | |
---|
| 439 | lemma load_by_value_success_valid_pointer : |
---|
| 440 | ∀ty,m,b,off,v. |
---|
| 441 | access_mode ty = By_value (typ_of_type ty) → |
---|
| 442 | load_value_of_type ty m b off = Some ? v → |
---|
| 443 | valid_pointer m (mk_pointer b off). |
---|
| 444 | #ty #m #b #off #v #Haccess_mode #Hload normalize |
---|
| 445 | elim (load_by_value_success_valid_ptr_aux ty m b off v Haccess_mode Hload) |
---|
[2438] | 446 | * #H1 #H2 #H3 >H1 >H2 normalize nodelta >H3 @I |
---|
| 447 | qed. |
---|
[2312] | 448 | |
---|
[2468] | 449 | (* Making explicit the contents of memory_inj for load_value_of_type. |
---|
| 450 | * Equivalent to Lemma 59 of Leroy & Blazy *) |
---|
[2312] | 451 | lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty. |
---|
| 452 | memory_inj E m1 m2 → |
---|
| 453 | value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) → |
---|
| 454 | load_value_of_type ty m1 b1 off1 = Some ? v1 → |
---|
| 455 | ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2. |
---|
| 456 | #E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq |
---|
| 457 | lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct |
---|
| 458 | lapply (refl ? (access_mode ty)) |
---|
| 459 | cases ty |
---|
[2468] | 460 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 461 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2312] | 462 | normalize in ⊢ ((???%) → ?); #Hmode #Hyp |
---|
[2468] | 463 | [ 1,6,7: normalize in Hyp; destruct (Hyp) |
---|
| 464 | | 4,5: normalize in Hyp ⊢ %; destruct (Hyp) /3 by ex_intro, conj, vptr_eq/ ] |
---|
[2312] | 465 | lapply (load_by_value_success_valid_pointer … Hmode … Hyp) #Hvalid_pointer |
---|
| 466 | lapply (mi_inj … Hinj b1 off1 b2 off2 … Hvalid_pointer Hembed Hyp) #H @H |
---|
[2468] | 467 | qed. |
---|
[2312] | 468 | |
---|
| 469 | (* -------------------------------------- *) |
---|
| 470 | (* Lemmas pertaining to memory allocation *) |
---|
| 471 | |
---|
| 472 | (* A valid block stays valid after an alloc. *) |
---|
| 473 | lemma alloc_valid_block_conservation : |
---|
| 474 | ∀m,m',z1,z2,r,new_block. |
---|
| 475 | alloc m z1 z2 r = 〈m', new_block〉 → |
---|
| 476 | ∀b. valid_block m b → valid_block m' b. |
---|
| 477 | #m #m' #z1 #z2 #r * #b' #Hregion_eq |
---|
| 478 | elim m #contents #nextblock #Hcorrect whd in match (alloc ????); |
---|
| 479 | #Halloc destruct (Halloc) |
---|
| 480 | #b whd in match (valid_block ??) in ⊢ (% → %); /2/ |
---|
| 481 | qed. |
---|
| 482 | |
---|
| 483 | (* Allocating a new zone produces a valid block. *) |
---|
| 484 | lemma alloc_valid_new_block : |
---|
| 485 | ∀m,m',z1,z2,r,new_block. |
---|
| 486 | alloc m z1 z2 r = 〈m', new_block〉 → |
---|
| 487 | valid_block m' new_block. |
---|
| 488 | * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq |
---|
| 489 | whd in match (alloc ????); whd in match (valid_block ??); |
---|
| 490 | #Halloc destruct (Halloc) /2/ |
---|
| 491 | qed. |
---|
| 492 | |
---|
| 493 | (* All data in a valid block is unchanged after an alloc. *) |
---|
| 494 | lemma alloc_beloadv_conservation : |
---|
| 495 | ∀m,m',block,offset,z1,z2,r,new_block. |
---|
| 496 | valid_block m block → |
---|
| 497 | alloc m z1 z2 r = 〈m', new_block〉 → |
---|
| 498 | beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset). |
---|
| 499 | * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc |
---|
| 500 | whd in Halloc:(??%?); destruct (Halloc) |
---|
| 501 | whd in match (beloadv ??) in ⊢ (??%%); |
---|
[2468] | 502 | lapply (Zlt_to_Zltb_true … Hvalid) #Hlt |
---|
[2312] | 503 | >Hlt >(zlt_succ … Hlt) |
---|
| 504 | normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??); |
---|
| 505 | cut (eqZb (block_id block) next = false) |
---|
[2468] | 506 | [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq |
---|
[2312] | 507 | >Hneq cases (eq_region ??) normalize nodelta @refl |
---|
| 508 | qed. |
---|
| 509 | |
---|
| 510 | (* Lift [alloc_beloadv_conservation] to loadn *) |
---|
| 511 | lemma alloc_loadn_conservation : |
---|
| 512 | ∀m,m',z1,z2,r,new_block. |
---|
| 513 | alloc m z1 z2 r = 〈m', new_block〉 → |
---|
| 514 | ∀n. ∀block,offset. |
---|
| 515 | valid_block m block → |
---|
| 516 | loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n. |
---|
| 517 | #m #m' #z1 #z2 #r #new_block #Halloc #n |
---|
| 518 | elim n try // |
---|
| 519 | #n' #Hind #block #offset #Hvalid_block |
---|
| 520 | whd in ⊢ (??%%); |
---|
| 521 | >(alloc_beloadv_conservation … Hvalid_block Halloc) |
---|
| 522 | cases (beloadv m' (mk_pointer block offset)) // |
---|
| 523 | #bev normalize nodelta |
---|
| 524 | whd in match (shift_pointer ???); >Hind try // |
---|
| 525 | qed. |
---|
| 526 | |
---|
| 527 | (* Memory allocation preserves [memory_inj] *) |
---|
| 528 | lemma alloc_memory_inj : |
---|
[2468] | 529 | ∀E:embedding. |
---|
| 530 | ∀m1,m2,m2',z1,z2,r,new_block. |
---|
| 531 | ∀H:memory_inj E m1 m2. |
---|
[2312] | 532 | alloc m2 z1 z2 r = 〈m2', new_block〉 → |
---|
| 533 | memory_inj E m1 m2'. |
---|
| 534 | #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc |
---|
| 535 | % |
---|
| 536 | [ 1: |
---|
| 537 | whd |
---|
| 538 | #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload |
---|
| 539 | elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload) |
---|
| 540 | #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try // |
---|
| 541 | lapply (refl ? (access_mode ty)) |
---|
| 542 | cases ty in Hload_eq; |
---|
[2468] | 543 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 544 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
[2312] | 545 | #Hload normalize in ⊢ ((???%) → ?); #Haccess |
---|
[2468] | 546 | [ 1,6,7: normalize in Hload; destruct (Hload) |
---|
| 547 | | 2,3,8: whd in match (load_value_of_type ????); |
---|
[2312] | 548 | whd in match (load_value_of_type ????); |
---|
| 549 | lapply (load_by_value_success_valid_block … Haccess Hload) |
---|
| 550 | #Hvalid_block |
---|
| 551 | whd in match (load_value_of_type ????) in Hload; |
---|
| 552 | <(alloc_loadn_conservation … Halloc … Hvalid_block) |
---|
| 553 | @Hload |
---|
[2468] | 554 | | 4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] |
---|
[2312] | 555 | | 2: @(mi_freeblock … Hmemory_inj) |
---|
| 556 | | 3: #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) |
---|
| 557 | elim m2 in Halloc; #contentmap #nextblock #Hnextblock |
---|
| 558 | elim p' * #br' #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc) |
---|
| 559 | whd in match (valid_pointer ??) in ⊢ (% → %); |
---|
| 560 | @Zltb_elim_Type0 |
---|
| 561 | [ 2: normalize #_ #Habsurd destruct (Habsurd) ] |
---|
| 562 | #Hbid' cut (Zltb bid' (Zsucc nextblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ] |
---|
| 563 | #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %); |
---|
| 564 | whd in match (high_bound ??) in ⊢ (% → %); |
---|
| 565 | whd in match (update_block ?????); |
---|
| 566 | whd in match (eq_block ??); |
---|
| 567 | cut (eqZb bid' nextblock = false) [ 1: @eqZb_false /2 by not_to_not/ ] |
---|
| 568 | #Hbid_neq >Hbid_neq |
---|
| 569 | cases (eq_region br' r) normalize #H @H |
---|
| 570 | | 4: @(mi_region … Hmemory_inj) |
---|
[2468] | 571 | | 5: @(mi_nonalias … Hmemory_inj) |
---|
| 572 | qed. |
---|
[2312] | 573 | |
---|
[2468] | 574 | (* ---------------------------------------------------------- *) |
---|
| 575 | (* Lemma 40 of the paper of Leroy & Blazy on the memory model |
---|
| 576 | * and related lemmas *) |
---|
[2312] | 577 | |
---|
| 578 | lemma bestorev_beloadv_conservation : |
---|
| 579 | ∀mA,mB,wb,wo,v. |
---|
| 580 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
| 581 | ∀rb,ro. eq_block wb rb = false → |
---|
| 582 | beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro). |
---|
| 583 | #mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq |
---|
| 584 | whd in ⊢ (??%%); |
---|
| 585 | elim mB in Hstore; #contentsB #nextblockB #HnextblockB |
---|
| 586 | normalize in ⊢ (% → ?); |
---|
| 587 | cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta |
---|
| 588 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
| 589 | cases (if Zleb (low (blocks mA wb)) (Z_of_unsigned_bitvector 16 (offv wo)) |
---|
| 590 | then Zltb (Z_of_unsigned_bitvector 16 (offv wo)) (high (blocks mA wb)) |
---|
| 591 | else false) normalize nodelta |
---|
| 592 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
| 593 | #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid |
---|
| 594 | cases rr cases wr normalize try // |
---|
| 595 | @(eqZb_elim … rid wid) |
---|
| 596 | [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ] |
---|
| 597 | try // |
---|
| 598 | qed. |
---|
| 599 | |
---|
| 600 | (* lift [bestorev_beloadv_conservation to [loadn] *) |
---|
| 601 | lemma bestorev_loadn_conservation : |
---|
| 602 | ∀mA,mB,n,wb,wo,v. |
---|
| 603 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
| 604 | ∀rb,ro. eq_block wb rb = false → |
---|
| 605 | loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n. |
---|
| 606 | #mA #mB #n |
---|
| 607 | elim n |
---|
| 608 | [ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl |
---|
| 609 | | 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq |
---|
| 610 | whd in ⊢ (??%%); |
---|
| 611 | >(bestorev_beloadv_conservation … Hstore … Hneq) |
---|
| 612 | >(Hind … Hstore … Hneq) @refl |
---|
| 613 | ] qed. |
---|
| 614 | |
---|
| 615 | (* lift [bestorev_loadn_conservation] to [load_value_of_type] *) |
---|
| 616 | lemma bestorev_load_value_of_type_conservation : |
---|
| 617 | ∀mA,mB,wb,wo,v. |
---|
| 618 | bestorev mA (mk_pointer wb wo) v = Some ? mB → |
---|
| 619 | ∀rb,ro. eq_block wb rb = false → |
---|
| 620 | ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. |
---|
| 621 | #mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty |
---|
| 622 | cases ty |
---|
[2468] | 623 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 624 | | #structname #fieldspec | #unionname #fieldspec | #id ] |
---|
| 625 | // |
---|
| 626 | [ 1: elim sz ] |
---|
[2312] | 627 | whd in ⊢ (??%%); |
---|
| 628 | >(bestorev_loadn_conservation … Hstore … Hneq) @refl |
---|
| 629 | qed. |
---|
| 630 | |
---|
[2468] | 631 | (* lift [bestorev_load_value_of_type_conservation] to storen *) |
---|
| 632 | lemma storen_load_value_of_type_conservation : |
---|
| 633 | ∀l,mA,mB,wb,wo. |
---|
| 634 | storen mA (mk_pointer wb wo) l = Some ? mB → |
---|
| 635 | ∀rb,ro. eq_block wb rb = false → |
---|
| 636 | ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro. |
---|
| 637 | #l elim l |
---|
| 638 | [ 1: #mA #mB #wb #wo normalize #Heq destruct // |
---|
| 639 | | 2: #hd #tl #Hind #mA #mB #wb #wo #Hstoren |
---|
| 640 | cases (some_inversion ????? Hstoren) #mA' * #Hbestorev #Hstoren' |
---|
| 641 | whd in match (shift_pointer ???) in Hstoren':(??%?); #rb #ro #Hneq_block #ty |
---|
| 642 | lapply (Hind ???? Hstoren' … ro … Hneq_block ty) #Heq1 |
---|
| 643 | lapply (bestorev_load_value_of_type_conservation … Hbestorev … ro … Hneq_block ty) #Heq2 |
---|
| 644 | // |
---|
| 645 | ] qed. |
---|
| 646 | |
---|
| 647 | definition typesize' ≝ λty. typesize (typ_of_type ty). |
---|
| 648 | |
---|
| 649 | lemma storen_load_value_of_type_conservation_in_block_high : |
---|
| 650 | ∀E,mA,mB,mC,wo,l. |
---|
| 651 | memory_inj E mA mB → |
---|
| 652 | ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → |
---|
| 653 | ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → |
---|
| 654 | high_bound mA b1 + Zoo delta < Zoo wo → |
---|
| 655 | ∀ty,off. |
---|
| 656 | Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → |
---|
| 657 | low_bound … mA b1 ≤ Zoo off → |
---|
| 658 | Zoo off < high_bound … mA b1 → |
---|
| 659 | load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = |
---|
| 660 | load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). |
---|
| 661 | #E #mA #mB #mC #wo #data #Hinj #blo #Hstoren #b1 #delta #Hembed #Hhigh #ty |
---|
| 662 | (* need some stuff asserting that if a ptr is valid at the start of a write it's valid at the end. *) |
---|
| 663 | cases data in Hstoren; |
---|
| 664 | [ 1: normalize in ⊢ (% → ?); #Heq destruct // |
---|
| 665 | | 2: #xd #data ] |
---|
| 666 | #Hstoren |
---|
| 667 | cases ty |
---|
| 668 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 669 | | #structname #fieldspec | #unionname #fieldspec | #id ]#off #Hofflt #Hlow_load #Hhigh_load try @refl |
---|
| 670 | whd in match (load_value_of_type ????) in ⊢ (??%%); |
---|
| 671 | [ 1: lapply (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hbefore #Hafter |
---|
| 672 | lapply Hofflt -Hofflt lapply Hlow_load -Hlow_load lapply Hhigh_load -Hhigh_load |
---|
| 673 | lapply off -off whd in match typesize'; normalize nodelta |
---|
| 674 | generalize in match (typesize ?); #n elim n try // |
---|
| 675 | #n' #Hind #o #Hhigh_load #Hlow_load #Hlt |
---|
| 676 | whd in match (loadn ???) in ⊢ (??%%); |
---|
| 677 | whd in match (beloadv ??) in ⊢ (??%%); |
---|
| 678 | cases (valid_pointer_to_Prop … Hbefore) * #HltB_store #HlowB_store #HhighB_store |
---|
| 679 | cases (valid_pointer_to_Prop … Hafter) * #HltC_store #HlowC_store #HhighC_store |
---|
| 680 | >(Zlt_to_Zltb_true … HltB_store) >(Zlt_to_Zltb_true … HltC_store) normalize nodelta |
---|
| 681 | cut (Zleb (low (blocks mB blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) |
---|
| 682 | [ 1: (* Notice that: |
---|
| 683 | low mA b1 ≤ o < high mA b1 |
---|
| 684 | hence, since E b1 = 〈blo, delta〉 with delta >= 0 |
---|
| 685 | low mB blo ≤ (low mA b1 + delta) ≤ o+delta < (high mA b1 + delta) ≤ high mB blo *) |
---|
| 686 | @cthulhu ] |
---|
| 687 | #HA >HA >andb_lsimpl_true -HA |
---|
| 688 | cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mB blo)) = true) |
---|
| 689 | [ 1: (* Same argument as above *) @cthulhu ] |
---|
| 690 | #HA >HA normalize nodelta -HA |
---|
| 691 | cut (Zleb (low (blocks mC blo)) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = true) |
---|
| 692 | [ 1: (* Notice that storen does not modify the bounds of a block. Related lemma present in [MemProperties]. |
---|
| 693 | This cut follows from this lemma (which needs some info on the size of the data written, which we |
---|
| 694 | have but must make explicit) and from the first cut. *) |
---|
| 695 | @cthulhu ] |
---|
| 696 | #HA >HA >andb_lsimpl_true -HA |
---|
| 697 | cut (Zltb (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) (high (blocks mC blo)) = true) |
---|
| 698 | [ 1: (* Same argument as above *) @cthulhu ] |
---|
| 699 | #HA >HA normalize nodelta -HA |
---|
| 700 | normalize in match (bitvector_of_nat ??); whd in match (shift_pointer ???); |
---|
| 701 | whd in match (shift_offset ???); >commutative_addition_n >associative_addition_n |
---|
| 702 | lapply (Hind (mk_offset (addition_n offset_size (sign_ext 2 ? [[false; true]]) (offv o))) ???) |
---|
| 703 | [ 1: (* Provable from Hlt *) @cthulhu |
---|
| 704 | | 2: (* Provable from Hlow_load, need to make a "succ" commute from bitvector to Z *) @cthulhu |
---|
| 705 | | 3: (* Provable from Hlt, again *) @cthulhu ] |
---|
| 706 | cases (loadn mB (mk_pointer blo |
---|
| 707 | (mk_offset (addition_n ? (addition_n ? |
---|
| 708 | (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') |
---|
| 709 | normalize nodelta |
---|
| 710 | cases (loadn mC (mk_pointer blo |
---|
| 711 | (mk_offset (addition_n ? (addition_n ? |
---|
| 712 | (sign_ext 2 offset_size [[false; true]]) (offv o)) (offv delta)))) n') |
---|
| 713 | normalize nodelta try // |
---|
| 714 | [ 1,2: #l #Habsurd destruct ] |
---|
| 715 | #l1 #l2 #Heq |
---|
| 716 | cut (contents (blocks mB blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta))) = |
---|
| 717 | contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) |
---|
| 718 | [ 1: (* Follows from Hhigh, indirectly *) @cthulhu ] |
---|
| 719 | #Hcontents_eq >Hcontents_eq whd in match (be_to_fe_value ??) in ⊢ (??%%); |
---|
| 720 | cases (contents (blocks mC blo) (Z_of_unsigned_bitvector ? (addition_n ? (offv o) (offv delta)))) |
---|
| 721 | normalize nodelta try // |
---|
| 722 | (* Ok this is going to be more painful than what I thought. *) |
---|
| 723 | @cthulhu |
---|
| 724 | | *: @cthulhu |
---|
| 725 | ] qed. |
---|
| 726 | |
---|
| 727 | lemma storen_load_value_of_type_conservation_in_block_low : |
---|
| 728 | ∀E,mA,mB,mC,wo,l. |
---|
| 729 | memory_inj E mA mB → |
---|
| 730 | ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → |
---|
| 731 | ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → |
---|
| 732 | Zoo wo < low_bound mA b1 + Zoo delta → |
---|
| 733 | ∀ty,off. |
---|
| 734 | Zoo off + Z_of_nat (typesize' ty) < high_bound mA b1 → |
---|
| 735 | low_bound … mA b1 ≤ Zoo off → |
---|
| 736 | Zoo off < high_bound … mA b1 → |
---|
| 737 | load_value_of_type ty mB blo (mk_offset (addition_n ? (offv off) (offv delta))) = |
---|
| 738 | load_value_of_type ty mC blo (mk_offset (addition_n ? (offv off) (offv delta))). |
---|
| 739 | @cthulhu |
---|
| 740 | qed. |
---|
| 741 | |
---|
| 742 | (* Writing in the "extended" part of a memory preserves the underlying injection. *) |
---|
| 743 | lemma bestorev_memory_inj_to_load_sim : |
---|
[2312] | 744 | ∀E,mA,mB,mC. |
---|
[2468] | 745 | ∀Hext:memory_inj E mA mB. |
---|
| 746 | ∀block2. ∀i : offset. ∀ty : type. |
---|
| 747 | (∀block1,delta. |
---|
| 748 | E block1 = Some ? 〈block2, delta〉 → |
---|
| 749 | (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → |
---|
| 750 | ∀v.store_value_of_type ty mB block2 i v = Some ? mC → |
---|
[2312] | 751 | load_sim_ptr E mA mC. |
---|
[2468] | 752 | #E #mA #mB #mC #Hinj #block2 #i #storety |
---|
| 753 | cases storety |
---|
| 754 | [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain |
---|
| 755 | | #structname #fieldspec | #unionname #fieldspec | #id ]#Hout #storeval #Hstore whd |
---|
| 756 | #b1 #off1 #b2 #off2 #ty #readval #Hvalid #Hptr_trans #Hload_value |
---|
| 757 | whd in Hstore:(??%?); |
---|
| 758 | [ 1,5,6,7,8: destruct ] |
---|
| 759 | [ 1: |
---|
| 760 | lapply (mi_inj … Hinj … Hvalid … Hptr_trans … Hload_value) |
---|
| 761 | lapply Hload_value -Hload_value |
---|
| 762 | cases ty |
---|
| 763 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
| 764 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
| 765 | #Hload_value |
---|
| 766 | (* Prove that the contents of mB where v1 was were untouched. *) |
---|
| 767 | * #readval' * #Hload_value2 #Hvalue_eq %{readval'} @conj try assumption |
---|
| 768 | cases (some_inversion ????? Hptr_trans) * #b2' #delta' * #Hembed -Hptr_trans normalize nodelta |
---|
| 769 | #Heq destruct (Heq) |
---|
| 770 | @(eq_block_elim … b2 block2) |
---|
| 771 | [ 2,4,6,8: #Hblocks_neq <Hload_value2 @sym_eq @(storen_load_value_of_type_conservation … Hstore) |
---|
| 772 | @not_eq_block @sym_neq @Hblocks_neq |
---|
| 773 | | 1,3,5,7: #Heq destruct (Heq) lapply (Hout … Hembed) * |
---|
| 774 | [ 1,3,5,7: #Hhigh <Hload_value2 -Hload_value2 @sym_eq |
---|
| 775 | lapply (load_by_value_success_valid_ptr_aux … Hload_value) // |
---|
| 776 | * * #Hlt #Hlowb_off1 #Hhighb_off1 |
---|
| 777 | lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1 |
---|
| 778 | lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1 |
---|
| 779 | @(storen_load_value_of_type_conservation_in_block_high … Hinj … Hstore … Hembed) |
---|
| 780 | try // |
---|
| 781 | (* remaining stuff provable from Hload_value *) |
---|
| 782 | @cthulhu |
---|
| 783 | | 2,4,6,8: #Hlow <Hload_value2 -Hload_value2 @sym_eq |
---|
| 784 | lapply (load_by_value_success_valid_ptr_aux … Hload_value) // |
---|
| 785 | * * #Hlt #Hlowb_off1 #Hhighb_off1 |
---|
| 786 | lapply (Zleb_true_to_Zle … Hlowb_off1) #Hlow_off1 -Hlowb_off1 |
---|
| 787 | lapply (Zltb_true_to_Zlt … Hhighb_off1) #Hhigh_off1 -Hhighb_off1 |
---|
| 788 | @(storen_load_value_of_type_conservation_in_block_low … Hinj … Hstore … Hembed) |
---|
| 789 | try // |
---|
| 790 | [ 1,3,5,7: (* deductible from Hlow + (sizeof ?) > 0 *) @cthulhu |
---|
| 791 | | 2,4,6,8: (* deductible from Hload_value *) @cthulhu ] |
---|
| 792 | ] |
---|
| 793 | ] |
---|
| 794 | | *: (* exactly the same proof as above *) @cthulhu ] |
---|
[2312] | 795 | qed. |
---|
| 796 | |
---|
[2468] | 797 | (* Lift the above result to memory_inj |
---|
| 798 | * This is Lemma 40 of Leroy & Blazy *) |
---|
| 799 | lemma bestorev_memory_inj_to_memory_inj : |
---|
[2312] | 800 | ∀E,mA,mB,mC. |
---|
[2468] | 801 | ∀Hext:memory_inj E mA mB. |
---|
| 802 | ∀block2. ∀i : offset. ∀ty : type. |
---|
| 803 | (∀block1,delta. |
---|
| 804 | E block1 = Some ? 〈block2, delta〉 → |
---|
| 805 | (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → |
---|
| 806 | ∀v.store_value_of_type ty mB block2 i v = Some ? mC → |
---|
[2312] | 807 | memory_inj E mA mC. |
---|
[2468] | 808 | #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % |
---|
| 809 | lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // |
---|
| 810 | cases Hinj #Hsim' #Hnot_valid #Hvalid #Hregion #Hnonalias try assumption |
---|
| 811 | #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid |
---|
| 812 | cases ty in Hstore; |
---|
| 813 | [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain' |
---|
| 814 | | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ] |
---|
| 815 | whd in ⊢ ((??%?) → ?); |
---|
| 816 | [ 1,4,5,6,7: #Habsurd destruct ] |
---|
| 817 | cases (fe_to_be_values ??) |
---|
| 818 | [ 1,3,5,7: whd in ⊢ ((??%?) → ?); #Heq <Hvalid -Hvalid destruct @refl |
---|
| 819 | | *: #hd #tl #Hstoren cases (storen_to_valid_pointer … Hstoren) * * #Hbounds #Hnext #_ #_ |
---|
| 820 | @valid_pointer_of_Prop cases (valid_pointer_to_Prop … Hvalid) * #Hnext' #Hlow #Hhigh |
---|
| 821 | @conj try @conj try assumption >Hnext try // |
---|
| 822 | cases (Hbounds (pblock p')) #HA #HB |
---|
| 823 | whd in match (low_bound ??); whd in match (high_bound ??); |
---|
| 824 | >HA >HB try assumption |
---|
| 825 | ] qed. |
---|
[2312] | 826 | |
---|
[2468] | 827 | (* ---------------------------------------------------------- *) |
---|
| 828 | (* Lemma 41 of the paper of Leroy & Blazy on the memory model |
---|
| 829 | * and related lemmas *) |
---|
| 830 | |
---|
| 831 | (* The back-end might contain something similar to this lemma. *) |
---|
| 832 | lemma be_to_fe_value_ptr : |
---|
| 833 | ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). |
---|
| 834 | #b * #o whd in ⊢ (??%%); normalize cases b #br #bid normalize nodelta |
---|
| 835 | cases br normalize nodelta >eqZb_z_z normalize nodelta |
---|
| 836 | cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq |
---|
| 837 | <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl |
---|
| 838 | * // |
---|
[2312] | 839 | qed. |
---|
| 840 | |
---|
[2468] | 841 | lemma value_eq_to_be_and_back_again : |
---|
| 842 | ∀E,ty,v1,v2. |
---|
| 843 | value_eq E v1 v2 → |
---|
| 844 | ast_typ_consistent_with_value ty v1 → |
---|
| 845 | ast_typ_consistent_with_value ty v2 → |
---|
| 846 | 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)). |
---|
| 847 | #E #ty #v1 #v2 #Hvalue_eq |
---|
| 848 | @(value_eq_inversion … Hvalue_eq) try // |
---|
| 849 | [ 1: cases ty // |
---|
| 850 | | 2: #sz #i cases ty |
---|
| 851 | [ 2: @False_ind |
---|
| 852 | | 1: #sz' #sg #H whd in ⊢ (% → ?); #Heq |
---|
| 853 | lapply (fe_to_be_to_fe_value … H) #H >H // ] |
---|
| 854 | | 3: #p1 #p2 #Hembed cases ty |
---|
| 855 | [ 1: #sz #sg @False_ind |
---|
| 856 | | 2: #_ #_ |
---|
| 857 | cases p1 in Hembed; #b1 #o1 |
---|
| 858 | cases p2 #b2 #o2 whd in ⊢ ((??%%) → ?); #H |
---|
| 859 | cases (some_inversion ????? H) * #b3 #o3 * #Hembed |
---|
| 860 | normalize nodelta #Heq >be_to_fe_value_ptr >be_to_fe_value_ptr |
---|
| 861 | destruct %4 whd in match (pointer_translation ??); |
---|
| 862 | >Hembed normalize nodelta @refl |
---|
| 863 | ] |
---|
| 864 | ] qed. |
---|
[2312] | 865 | |
---|
[2468] | 866 | lemma storen_parallel_memory_exists : |
---|
| 867 | ∀E,m1,m2,m1',b1,i,b2,delta,ty,v1,v2. |
---|
| 868 | memory_inj E m1 m2 → |
---|
| 869 | value_eq E v1 v2 → |
---|
| 870 | storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → |
---|
| 871 | E b1 = Some ? 〈b2, delta〉 → |
---|
| 872 | ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2'. |
---|
| 873 | @cthulhu qed. |
---|
| 874 | (* |
---|
| 875 | #E #m1 #m2 #m1' #b1 #i #b2 #delta #ty #v1 #v2 #Hinj #Hvalue_eq |
---|
| 876 | @(value_eq_inversion … Hvalue_eq) |
---|
| 877 | [ 1: #v #Hstoren *) |
---|
| 878 | |
---|
| 879 | |
---|
| 880 | lemma storen_parallel_aux : |
---|
| 881 | ∀E,m1,m2. |
---|
| 882 | ∀Hinj:memory_inj E m1 m2. |
---|
| 883 | ∀v1,v2. value_eq E v1 v2 → |
---|
| 884 | ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → |
---|
| 885 | ∀ty,i,m1'. |
---|
| 886 | ast_typ_consistent_with_value ty v1 → |
---|
| 887 | ast_typ_consistent_with_value ty v2 → |
---|
| 888 | storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1' → |
---|
| 889 | ∃m2'. storen m2 (mk_pointer b2 (offset_plus i delta)) (fe_to_be_values ty v2) = Some ? m2' ∧ |
---|
| 890 | memory_inj E m1' m2'. |
---|
| 891 | #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hok1 #Hok2 |
---|
| 892 | #Hstoren lapply (storen_to_valid_pointer_fe_to_be … Hstoren) |
---|
| 893 | * * * #Hblocks_eq1 #Hnextblock1 #Hvalid_m1 #Hvalid_m1' |
---|
| 894 | lapply (mi_valid_pointers … Hinj … (mk_pointer b1 i) (mk_pointer b2 (offset_plus i delta)) Hvalid_m1 ?) |
---|
| 895 | [ 1: whd in ⊢ (??%%); >Hembed @refl ] |
---|
| 896 | #Hvalid_m2 |
---|
| 897 | cases (valid_pointer_to_Prop … Hvalid_m2) * #Hnextblock2 #Hlow2 #Hhigh2 |
---|
| 898 | @cthulhu |
---|
[2312] | 899 | qed. |
---|
[2332] | 900 | |
---|
[2468] | 901 | lemma foo : |
---|
| 902 | ∀E,m1,m2. |
---|
| 903 | ∀Hinj:memory_inj E m1 m2. |
---|
| 904 | ∀v1,v2. value_eq E v1 v2 → |
---|
| 905 | ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → |
---|
| 906 | ∀ty,i,m1'. store_value_of_type ty m1 b1 i v1 = Some ? m1' → |
---|
| 907 | ∃m2'. store_value_of_type ty m2 b2 (offset_plus i delta) v2 = Some ? m2' ∧ |
---|
| 908 | memory_inj E m1' m2'. |
---|
| 909 | #E #m1 #m2 #Hinj #v1 #v2 #Hvalue_eq #b1 #b2 #delta #Hembed #ty #i #m1' #Hstore |
---|
| 910 | @cthulhu qed. |
---|
| 911 | |
---|
| 912 | (* ------------------------------------------------------------------------- *) |
---|
| 913 | (* Commutation results of standard unary and binary operations with value_eq. *) |
---|
| 914 | |
---|
[2332] | 915 | lemma unary_operation_value_eq : |
---|
| 916 | ∀E,op,v1,v2,ty. |
---|
| 917 | value_eq E v1 v2 → |
---|
| 918 | ∀r1. |
---|
| 919 | sem_unary_operation op v1 ty = Some ? r1 → |
---|
| 920 | ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2. |
---|
| 921 | #E #op #v1 #v2 #ty #Hvalue_eq #r1 |
---|
| 922 | inversion Hvalue_eq |
---|
[2468] | 923 | [ 1: #v #Hv1 #Hv2 destruct |
---|
[2332] | 924 | cases op normalize |
---|
[2468] | 925 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 926 | normalize #Habsurd destruct (Habsurd) |
---|
[2468] | 927 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 928 | normalize #Habsurd destruct (Habsurd) |
---|
| 929 | | 2: #Habsurd destruct (Habsurd) ] |
---|
| 930 | | 2: #vsz #i #Hv1 #Hv2 #_ |
---|
| 931 | cases op |
---|
[2468] | 932 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 933 | whd in ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???); |
---|
| 934 | [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct |
---|
| 935 | %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))} |
---|
| 936 | cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj |
---|
| 937 | // |
---|
| 938 | | *: #Habsurd destruct (Habsurd) ] |
---|
| 939 | | 2: whd in match (sem_unary_operation ???); |
---|
| 940 | #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj // |
---|
| 941 | | 3: whd in match (sem_unary_operation ???); |
---|
[2468] | 942 | cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 943 | normalize nodelta |
---|
| 944 | whd in ⊢ ((??%?) → ?); |
---|
| 945 | [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct |
---|
| 946 | %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj // |
---|
| 947 | | *: #Habsurd destruct (Habsurd) ] ] |
---|
[2468] | 948 | | 3: #Hv1 #Hv2 #_ destruct whd in match (sem_unary_operation ???); |
---|
[2332] | 949 | cases op normalize nodelta |
---|
[2468] | 950 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 951 | whd in match (sem_notbool ??); |
---|
| 952 | #Heq1 destruct /3 by ex_intro, vint_eq, conj/ |
---|
| 953 | | 2: normalize #Habsurd destruct (Habsurd) |
---|
[2468] | 954 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 955 | whd in match (sem_neg ??); |
---|
| 956 | #Heq1 destruct ] |
---|
[2468] | 957 | | 4: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_ whd in match (sem_unary_operation ???); |
---|
[2332] | 958 | cases op normalize nodelta |
---|
[2468] | 959 | [ 1: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 960 | whd in match (sem_notbool ??); |
---|
| 961 | #Heq1 destruct /3 by ex_intro, vint_eq, conj/ |
---|
| 962 | | 2: normalize #Habsurd destruct (Habsurd) |
---|
[2468] | 963 | | 3: cases ty [ | #sz #sg | #ty | #ty #n | #tl #ty | #id #fl | #id #fl | #ty ] |
---|
[2332] | 964 | whd in match (sem_neg ??); |
---|
| 965 | #Heq1 destruct ] |
---|
| 966 | ] |
---|
| 967 | qed. |
---|
| 968 | |
---|
| 969 | (* value_eq lifts to addition *) |
---|
| 970 | lemma add_value_eq : |
---|
| 971 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
| 972 | value_eq E v1 v2 → |
---|
| 973 | value_eq E v1' v2' → |
---|
| 974 | (* memory_inj E m1 m2 → This injection seems useless TODO *) |
---|
| 975 | ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→ |
---|
| 976 | ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
| 977 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 978 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 979 | [ 1: | 2: #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 980 | [ 1: whd in match (sem_add ????); normalize nodelta |
---|
| 981 | cases (classify_add ty1 ty2) normalize nodelta |
---|
[2468] | 982 | [ 1: #sz #sg | 2: #n #ty #sz #sg | 3: #n #sz #sg #ty | 4: #ty1' #ty2' ] |
---|
[2332] | 983 | #Habsurd destruct (Habsurd) |
---|
| 984 | | 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
[2468] | 985 | cases (classify_add ty1 ty2) normalize nodelta |
---|
| 986 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 987 | [ 2,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 988 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 989 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
| 990 | [ 1,2,4,5,7: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 991 | [ 1: @intsize_eq_elim_elim |
---|
| 992 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 993 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 994 | #Heq destruct (Heq) |
---|
| 995 | /3 by ex_intro, conj, vint_eq/ ] |
---|
| 996 | | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct |
---|
| 997 | /3 by ex_intro, conj, vint_eq/ |
---|
| 998 | | 3: #Heq destruct (Heq) |
---|
| 999 | normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed |
---|
| 1000 | %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl |
---|
| 1001 | @vptr_eq whd in match (pointer_translation ??); |
---|
| 1002 | cases (E b1') in Hembed; |
---|
| 1003 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1004 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
| 1005 | whd in match (shift_pointer_n ????); |
---|
| 1006 | cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset = |
---|
| 1007 | (shift_offset_n (bitsize_of_intsize sz) (mk_offset (addition_n ? (offv o1') (offv offset))) (sizeof ty) i)) |
---|
| 1008 | [ 1: whd in match (offset_plus ??); |
---|
| 1009 | whd in match (shift_offset_n ????) in ⊢ (??%%); |
---|
| 1010 | >commutative_addition_n >associative_addition_n |
---|
| 1011 | <(commutative_addition_n … (offv offset) (offv o1')) @refl ] |
---|
| 1012 | #Heq >Heq @refl ] |
---|
| 1013 | ] |
---|
[2468] | 1014 | (* | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
| 1015 | cases (classify_add ty1 ty2) normalize nodelta |
---|
| 1016 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1017 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
| 1018 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
| 1019 | [ 1: | 2: #sz' #i'| 3: | 4: #p1' #p2' #Hembed' ] |
---|
| 1020 | [ 1,3,4,5,7: #Habsurd destruct (Habsurd) ] |
---|
| 1021 | #Heq >Heq %{r1} @conj // |
---|
| 1022 | /3 by ex_intro, conj, vfloat_eq/ *) |
---|
[2332] | 1023 | | 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
[2468] | 1024 | cases (classify_add ty1 ty2) normalize nodelta |
---|
| 1025 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1026 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1027 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1028 | [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ] |
---|
[2332] | 1029 | [ 1,3,4,5: #Habsurd destruct (Habsurd) ] |
---|
[2468] | 1030 | @eq_bv_elim |
---|
[2332] | 1031 | [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ |
---|
| 1032 | | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
[2468] | 1033 | | 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta |
---|
[2332] | 1034 | cases (classify_add ty1 ty2) normalize nodelta |
---|
[2468] | 1035 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1036 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1037 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1038 | [ 1: | 2: #sz' #i' | 3: | 4: #p1' #p2' #Hembed' ] |
---|
[2332] | 1039 | [ 1,3,4,5: #Habsurd destruct (Habsurd) ] |
---|
| 1040 | #Heq destruct (Heq) |
---|
| 1041 | %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl |
---|
| 1042 | @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; |
---|
| 1043 | elim p1 in Hembed; #b1 #o1 normalize nodelta |
---|
| 1044 | cases (E b1) |
---|
| 1045 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1046 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
| 1047 | whd in match (shift_pointer_n ????); |
---|
| 1048 | whd in match (shift_offset_n ????) in ⊢ (??%%); |
---|
| 1049 | whd in match (offset_plus ??); |
---|
| 1050 | whd in match (offset_plus ??); |
---|
| 1051 | >commutative_addition_n >(associative_addition_n … offset_size ?) |
---|
| 1052 | >(commutative_addition_n ? (offv offset) ?) @refl |
---|
| 1053 | ] |
---|
| 1054 | ] qed. |
---|
| 1055 | |
---|
| 1056 | lemma subtraction_delta : ∀x,y,delta. |
---|
| 1057 | subtraction offset_size |
---|
| 1058 | (addition_n offset_size x delta) |
---|
| 1059 | (addition_n offset_size y delta) = |
---|
| 1060 | subtraction offset_size x y. |
---|
| 1061 | #x #y #delta whd in match subtraction; normalize nodelta |
---|
| 1062 | (* Remove all the equal parts on each side of the equation. *) |
---|
| 1063 | <associative_addition_n |
---|
| 1064 | >two_complement_negation_plus |
---|
| 1065 | <(commutative_addition_n … (two_complement_negation ? delta)) |
---|
| 1066 | >(associative_addition_n ? delta) >bitvector_opp_addition_n |
---|
| 1067 | >(commutative_addition_n ? (zero ?)) >neutral_addition_n |
---|
| 1068 | @refl |
---|
| 1069 | qed. |
---|
| 1070 | |
---|
| 1071 | (* Offset subtraction is invariant by translation *) |
---|
| 1072 | lemma sub_offset_translation : |
---|
| 1073 | ∀n,x,y,delta. sub_offset n x y = sub_offset n (offset_plus x delta) (offset_plus y delta). |
---|
| 1074 | #n #x #y #delta |
---|
| 1075 | whd in match (sub_offset ???) in ⊢ (??%%); |
---|
| 1076 | elim x #x' elim y #y' elim delta #delta' |
---|
| 1077 | whd in match (offset_plus ??); |
---|
| 1078 | whd in match (offset_plus ??); |
---|
| 1079 | >subtraction_delta @refl |
---|
| 1080 | qed. |
---|
| 1081 | |
---|
| 1082 | (* value_eq lifts to subtraction *) |
---|
| 1083 | lemma sub_value_eq : |
---|
| 1084 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
| 1085 | value_eq E v1 v2 → |
---|
| 1086 | value_eq E v1' v2' → |
---|
| 1087 | ∀r1. (sem_sub v1 ty1 v1' ty2=Some val r1→ |
---|
| 1088 | ∃r2:val.sem_sub v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
| 1089 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1090 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1091 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1092 | [ 1: whd in match (sem_sub ????); normalize nodelta |
---|
| 1093 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
[2468] | 1094 | [ #sz #sg | #n #ty #sz #sg | #n #sz #sg #ty |#ty1' #ty2' ] |
---|
[2332] | 1095 | #Habsurd destruct (Habsurd) |
---|
| 1096 | | 2: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta |
---|
| 1097 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
[2468] | 1098 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1099 | [ 2,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1100 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1101 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
| 1102 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1103 | @intsize_eq_elim_elim |
---|
| 1104 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1105 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1106 | #Heq destruct (Heq) |
---|
| 1107 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1108 | ] |
---|
[2468] | 1109 | (*| 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta |
---|
| 1110 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
| 1111 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1112 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1113 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1114 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
[2332] | 1115 | [ 1,2,4,5: #Habsurd destruct (Habsurd) ] |
---|
| 1116 | #Heq destruct (Heq) |
---|
[2468] | 1117 | /3 by ex_intro, conj, vfloat_eq/ *) |
---|
| 1118 | | 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta |
---|
[2332] | 1119 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
[2468] | 1120 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1121 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1122 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1123 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
| 1124 | [ 1,2,4,5,7,8: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1125 | [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ |
---|
| 1126 | | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 1127 | | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] |
---|
[2468] | 1128 | | 4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta |
---|
[2332] | 1129 | cases (classify_sub ty1 ty2) normalize nodelta |
---|
[2468] | 1130 | [ 1: #tsz #tsg | 2: #tn #ty #tsz #tsg | 3: #tn #tsz #tsg #ty | 4: #ty1' #ty2' ] |
---|
| 1131 | [ 1,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1132 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1133 | [ 1,5: | 2,6: #sz' #i' | 3,7: | 4,8: #p1' #p2' #Hembed' ] |
---|
| 1134 | [ 1,2,4,5,6,7: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1135 | #Heq destruct (Heq) |
---|
| 1136 | [ 1: %{(Vptr (neg_shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl |
---|
| 1137 | @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; |
---|
| 1138 | elim p1 in Hembed; #b1 #o1 normalize nodelta |
---|
| 1139 | cases (E b1) |
---|
| 1140 | [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1141 | | 2: * #block #offset normalize nodelta #Heq destruct (Heq) |
---|
| 1142 | whd in match (offset_plus ??) in ⊢ (??%%); |
---|
| 1143 | whd in match (neg_shift_pointer_n ????) in ⊢ (??%%); |
---|
| 1144 | whd in match (neg_shift_offset_n ????) in ⊢ (??%%); |
---|
| 1145 | whd in match (subtraction) in ⊢ (??%%); normalize nodelta |
---|
| 1146 | generalize in match (short_multiplication ???); #mult |
---|
| 1147 | /3 by associative_addition_n, commutative_addition_n, refl/ |
---|
| 1148 | ] |
---|
| 1149 | | 2: lapply Heq @eq_block_elim |
---|
| 1150 | [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) |
---|
| 1151 | | 1: #Hpblock1_eq normalize nodelta |
---|
| 1152 | elim p1 in Hpblock1_eq Hembed Hembed'; #b1 #off1 |
---|
| 1153 | elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) |
---|
| 1154 | whd in ⊢ ((??%?) → (??%?) → ?); |
---|
| 1155 | cases (E b1') normalize nodelta |
---|
| 1156 | [ 1: #Habsurd destruct (Habsurd) ] |
---|
| 1157 | * #dest_block #dest_off normalize nodelta |
---|
| 1158 | #Heq_ptr1 #Heq_ptr2 destruct >eq_block_b_b normalize nodelta |
---|
| 1159 | cases (eqb (sizeof tsg) O) normalize nodelta |
---|
| 1160 | [ 1: #Habsurd destruct (Habsurd) |
---|
| 1161 | | 2: >(sub_offset_translation 32 off1 off1' dest_off) |
---|
| 1162 | cases (division_u 31 |
---|
| 1163 | (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off)) |
---|
| 1164 | (repr (sizeof tsg))) |
---|
| 1165 | [ 1: normalize nodelta #Habsurd destruct (Habsurd) |
---|
| 1166 | | 2: #r1' normalize nodelta #Heq2 destruct (Heq2) |
---|
| 1167 | /3 by ex_intro, conj, vint_eq/ ] |
---|
| 1168 | ] ] ] |
---|
| 1169 | ] qed. |
---|
| 1170 | |
---|
| 1171 | |
---|
| 1172 | lemma mul_value_eq : |
---|
| 1173 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
| 1174 | value_eq E v1 v2 → |
---|
| 1175 | value_eq E v1' v2' → |
---|
| 1176 | ∀r1. (sem_mul v1 ty1 v1' ty2=Some val r1→ |
---|
| 1177 | ∃r2:val.sem_mul v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
| 1178 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1179 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1180 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1181 | [ 1: whd in match (sem_mul ????); normalize nodelta |
---|
| 1182 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1183 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1184 | #Habsurd destruct (Habsurd) |
---|
| 1185 | | 2: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
| 1186 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1187 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1188 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1189 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1190 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
| 1191 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1192 | @intsize_eq_elim_elim |
---|
| 1193 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1194 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1195 | #Heq destruct (Heq) |
---|
| 1196 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1197 | ] |
---|
| 1198 | | 3: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
| 1199 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1200 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1201 | [ 1,2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1202 | | 4: whd in match (sem_mul ????); whd in match (sem_mul ????); normalize nodelta |
---|
| 1203 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1204 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1205 | #Habsurd destruct (Habsurd) |
---|
[2468] | 1206 | ] qed. |
---|
[2332] | 1207 | |
---|
| 1208 | lemma div_value_eq : |
---|
| 1209 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
| 1210 | value_eq E v1 v2 → |
---|
| 1211 | value_eq E v1' v2' → |
---|
| 1212 | ∀r1. (sem_div v1 ty1 v1' ty2=Some val r1→ |
---|
| 1213 | ∃r2:val.sem_div v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
| 1214 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1215 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1216 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1217 | [ 1: whd in match (sem_div ????); normalize nodelta |
---|
| 1218 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1219 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1220 | #Habsurd destruct (Habsurd) |
---|
| 1221 | | 2: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
| 1222 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1223 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1224 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1225 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1226 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
| 1227 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1228 | elim sg normalize nodelta |
---|
| 1229 | @intsize_eq_elim_elim |
---|
| 1230 | [ 1,3: #_ #Habsurd destruct (Habsurd) |
---|
| 1231 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
| 1232 | @(match (division_s (bitsize_of_intsize sz') i i') with |
---|
| 1233 | [ None ⇒ ? |
---|
| 1234 | | Some bv' ⇒ ? ]) |
---|
| 1235 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
| 1236 | | 2: normalize #Heq destruct (Heq) |
---|
| 1237 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1238 | | 3,4: elim sz' in i' i; #i' #i |
---|
| 1239 | normalize in match (pred_size_intsize ?); |
---|
| 1240 | generalize in match division_u; #division_u normalize |
---|
| 1241 | @(match (division_u ???) with |
---|
| 1242 | [ None ⇒ ? |
---|
| 1243 | | Some bv ⇒ ?]) normalize nodelta |
---|
| 1244 | #H destruct (H) |
---|
| 1245 | /3 by ex_intro, conj, vint_eq/ ] |
---|
| 1246 | ] |
---|
| 1247 | | 3: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
| 1248 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1249 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1250 | [ 1,2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1251 | | 4: whd in match (sem_div ????); whd in match (sem_div ????); normalize nodelta |
---|
| 1252 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1253 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1254 | #Habsurd destruct (Habsurd) |
---|
[2468] | 1255 | ] qed. |
---|
[2332] | 1256 | |
---|
| 1257 | lemma mod_value_eq : |
---|
| 1258 | ∀E,v1,v2,v1',v2',ty1,ty2. |
---|
| 1259 | value_eq E v1 v2 → |
---|
| 1260 | value_eq E v1' v2' → |
---|
| 1261 | ∀r1. (sem_mod v1 ty1 v1' ty2=Some val r1→ |
---|
| 1262 | ∃r2:val.sem_mod v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2). |
---|
| 1263 | #E #v1 #v2 #v1' #v2' #ty1 #ty2 #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1264 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1265 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1266 | [ 1: whd in match (sem_mod ????); normalize nodelta |
---|
| 1267 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1268 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1269 | #Habsurd destruct (Habsurd) |
---|
| 1270 | | 2: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta |
---|
| 1271 | cases (classify_aop ty1 ty2) normalize nodelta |
---|
[2468] | 1272 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1273 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1274 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1275 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
| 1276 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1277 | elim sg normalize nodelta |
---|
| 1278 | @intsize_eq_elim_elim |
---|
| 1279 | [ 1,3: #_ #Habsurd destruct (Habsurd) |
---|
| 1280 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
| 1281 | @(match (modulus_s (bitsize_of_intsize sz') i i') with |
---|
| 1282 | [ None ⇒ ? |
---|
| 1283 | | Some bv' ⇒ ? ]) |
---|
| 1284 | [ 1: normalize #Habsurd destruct (Habsurd) |
---|
| 1285 | | 2: normalize #Heq destruct (Heq) |
---|
| 1286 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1287 | | 3,4: elim sz' in i' i; #i' #i |
---|
| 1288 | generalize in match modulus_u; #modulus_u normalize |
---|
| 1289 | @(match (modulus_u ???) with |
---|
| 1290 | [ None ⇒ ? |
---|
| 1291 | | Some bv ⇒ ?]) normalize nodelta |
---|
| 1292 | #H destruct (H) |
---|
| 1293 | /3 by ex_intro, conj, vint_eq/ ] |
---|
[2468] | 1294 | ] |
---|
| 1295 | | *: whd in match (sem_mod ????); whd in match (sem_mod ????); normalize nodelta |
---|
| 1296 | cases (classify_aop ty1 ty2) normalize nodelta #foo #bar #Habsurd destruct (Habsurd) |
---|
[2332] | 1297 | ] qed. |
---|
| 1298 | |
---|
| 1299 | (* boolean ops *) |
---|
| 1300 | lemma and_value_eq : |
---|
| 1301 | ∀E,v1,v2,v1',v2'. |
---|
| 1302 | value_eq E v1 v2 → |
---|
| 1303 | value_eq E v1' v2' → |
---|
| 1304 | ∀r1. (sem_and v1 v1'=Some val r1→ |
---|
| 1305 | ∃r2:val.sem_and v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
| 1306 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1307 | @(value_eq_inversion E … Hvalue_eq1) |
---|
| 1308 | [ 2: #sz #i |
---|
| 1309 | @(value_eq_inversion E … Hvalue_eq2) |
---|
| 1310 | [ 2: #sz' #i' whd in match (sem_and ??); |
---|
| 1311 | @intsize_eq_elim_elim |
---|
| 1312 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1313 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1314 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
| 1315 | ] ] |
---|
| 1316 | normalize in match (sem_and ??); #arg1 destruct |
---|
| 1317 | normalize in match (sem_and ??); #arg2 destruct |
---|
| 1318 | normalize in match (sem_and ??); #arg3 destruct |
---|
| 1319 | normalize in match (sem_and ??); #arg4 destruct |
---|
| 1320 | qed. |
---|
| 1321 | |
---|
| 1322 | lemma or_value_eq : |
---|
| 1323 | ∀E,v1,v2,v1',v2'. |
---|
| 1324 | value_eq E v1 v2 → |
---|
| 1325 | value_eq E v1' v2' → |
---|
| 1326 | ∀r1. (sem_or v1 v1'=Some val r1→ |
---|
| 1327 | ∃r2:val.sem_or v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
| 1328 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1329 | @(value_eq_inversion E … Hvalue_eq1) |
---|
| 1330 | [ 2: #sz #i |
---|
| 1331 | @(value_eq_inversion E … Hvalue_eq2) |
---|
| 1332 | [ 2: #sz' #i' whd in match (sem_or ??); |
---|
| 1333 | @intsize_eq_elim_elim |
---|
| 1334 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1335 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1336 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
| 1337 | ] ] |
---|
| 1338 | normalize in match (sem_or ??); #arg1 destruct |
---|
| 1339 | normalize in match (sem_or ??); #arg2 destruct |
---|
| 1340 | normalize in match (sem_or ??); #arg3 destruct |
---|
| 1341 | normalize in match (sem_or ??); #arg4 destruct |
---|
| 1342 | qed. |
---|
| 1343 | |
---|
| 1344 | lemma xor_value_eq : |
---|
| 1345 | ∀E,v1,v2,v1',v2'. |
---|
| 1346 | value_eq E v1 v2 → |
---|
| 1347 | value_eq E v1' v2' → |
---|
| 1348 | ∀r1. (sem_xor v1 v1'=Some val r1→ |
---|
| 1349 | ∃r2:val.sem_xor v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
| 1350 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1351 | @(value_eq_inversion E … Hvalue_eq1) |
---|
| 1352 | [ 2: #sz #i |
---|
| 1353 | @(value_eq_inversion E … Hvalue_eq2) |
---|
| 1354 | [ 2: #sz' #i' whd in match (sem_xor ??); |
---|
| 1355 | @intsize_eq_elim_elim |
---|
| 1356 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1357 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1358 | #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ ] |
---|
| 1359 | ] ] |
---|
| 1360 | normalize in match (sem_xor ??); #arg1 destruct |
---|
| 1361 | normalize in match (sem_xor ??); #arg2 destruct |
---|
| 1362 | normalize in match (sem_xor ??); #arg3 destruct |
---|
| 1363 | normalize in match (sem_xor ??); #arg4 destruct |
---|
| 1364 | qed. |
---|
| 1365 | |
---|
| 1366 | lemma shl_value_eq : |
---|
| 1367 | ∀E,v1,v2,v1',v2'. |
---|
| 1368 | value_eq E v1 v2 → |
---|
| 1369 | value_eq E v1' v2' → |
---|
| 1370 | ∀r1. (sem_shl v1 v1'=Some val r1→ |
---|
| 1371 | ∃r2:val.sem_shl v2 v2'=Some val r2∧value_eq E r1 r2). |
---|
| 1372 | #E #v1 #v2 #v1' #v2' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1373 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1374 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1375 | [ 2: |
---|
| 1376 | @(value_eq_inversion E … Hvalue_eq2) |
---|
[2468] | 1377 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
[2332] | 1378 | [ 2: whd in match (sem_shl ??); |
---|
| 1379 | cases (lt_u ???) normalize nodelta |
---|
| 1380 | [ 1: #Heq destruct (Heq) /3 by ex_intro,conj,vint_eq/ |
---|
| 1381 | | 2: #Habsurd destruct (Habsurd) |
---|
| 1382 | ] |
---|
| 1383 | | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] |
---|
| 1384 | | *: whd in match (sem_shl ??); #Habsurd destruct (Habsurd) ] |
---|
| 1385 | qed. |
---|
| 1386 | |
---|
| 1387 | lemma shr_value_eq : |
---|
| 1388 | ∀E,v1,v2,v1',v2',ty,ty'. |
---|
| 1389 | value_eq E v1 v2 → |
---|
| 1390 | value_eq E v1' v2' → |
---|
| 1391 | ∀r1. (sem_shr v1 ty v1' ty'=Some val r1→ |
---|
| 1392 | ∃r2:val.sem_shr v2 ty v2' ty'=Some val r2∧value_eq E r1 r2). |
---|
| 1393 | #E #v1 #v2 #v1' #v2' #ty #ty' #Hvalue_eq1 #Hvalue_eq2 #r1 |
---|
| 1394 | @(value_eq_inversion E … Hvalue_eq1) |
---|
[2468] | 1395 | [ | #sz #i | 3: | 4: #p1 #p2 #Hembed ] |
---|
[2332] | 1396 | whd in match (sem_shr ????); whd in match (sem_shr ????); |
---|
| 1397 | [ 1: cases (classify_aop ty ty') normalize nodelta |
---|
[2468] | 1398 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
[2332] | 1399 | #Habsurd destruct (Habsurd) |
---|
| 1400 | | 2: cases (classify_aop ty ty') normalize nodelta |
---|
[2468] | 1401 | [ 1: #sz #sg | 2: #ty1' #ty2' ] |
---|
| 1402 | [ 2: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1403 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
[2468] | 1404 | [ | #sz' #i' | | #p1' #p2' #Hembed' ] |
---|
| 1405 | [ 1,3,4: #Habsurd destruct (Habsurd) ] |
---|
[2332] | 1406 | elim sg normalize nodelta |
---|
| 1407 | cases (lt_u ???) normalize nodelta #Heq destruct (Heq) |
---|
| 1408 | /3 by ex_intro, conj, refl, vint_eq/ |
---|
[2468] | 1409 | | *: cases (classify_aop ty ty') normalize nodelta |
---|
| 1410 | #foo #bar |
---|
[2332] | 1411 | #Habsurd destruct (Habsurd) |
---|
[2468] | 1412 | ] qed. |
---|
[2332] | 1413 | |
---|
| 1414 | lemma eq_offset_translation : ∀delta,x,y. cmp_offset Ceq (offset_plus x delta) (offset_plus y delta) = cmp_offset Ceq x y. |
---|
| 1415 | * #delta * #x * #y |
---|
| 1416 | whd in match (offset_plus ??); |
---|
| 1417 | whd in match (offset_plus ??); |
---|
| 1418 | whd in match cmp_offset; normalize nodelta |
---|
| 1419 | whd in match eq_offset; normalize nodelta |
---|
| 1420 | @(eq_bv_elim … x y) |
---|
| 1421 | [ 1: #Heq >Heq >eq_bv_true @refl |
---|
| 1422 | | 2: #Hneq lapply (injective_inv_addition_n … x y delta Hneq) |
---|
| 1423 | @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta)) |
---|
| 1424 | [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ] |
---|
| 1425 | ] qed. |
---|
| 1426 | |
---|
| 1427 | lemma neq_offset_translation : ∀delta,x,y. cmp_offset Cne (offset_plus x delta) (offset_plus y delta) = cmp_offset Cne x y. |
---|
| 1428 | * #delta * #x * #y |
---|
| 1429 | whd in match (offset_plus ??); |
---|
| 1430 | whd in match (offset_plus ??); |
---|
| 1431 | whd in match cmp_offset; normalize nodelta |
---|
| 1432 | whd in match eq_offset; normalize nodelta |
---|
| 1433 | @(eq_bv_elim … x y) |
---|
| 1434 | [ 1: #Heq >Heq >eq_bv_true @refl |
---|
| 1435 | | 2: #Hneq lapply (injective_inv_addition_n … x y delta Hneq) |
---|
| 1436 | @(eq_bv_elim … (addition_n offset_size x delta) (addition_n offset_size y delta)) |
---|
| 1437 | [ 1: #H * #H' @(False_ind … (H' H)) | 2: #_ #_ @refl ] |
---|
| 1438 | ] qed. |
---|
| 1439 | |
---|
| 1440 | |
---|
| 1441 | (* /!\ Here is the source of all sadness (op = lt) /!\ *) |
---|
| 1442 | axiom cmp_offset_translation : ∀op,delta,x,y. |
---|
| 1443 | cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). |
---|
| 1444 | |
---|
[2438] | 1445 | (* 5 Nov. 2012 : the rest of the stuff doesn't checks anymore. Not a big deal, it was here |
---|
| 1446 | * for historical purposes, and for potential inspiration for Clight to Cminor. I leave the |
---|
| 1447 | * code commented for future reference. |
---|
| 1448 | *) |
---|
| 1449 | |
---|
| 1450 | (* |
---|
[2332] | 1451 | lemma cmp_value_eq : |
---|
| 1452 | ∀E,v1,v2,v1',v2',ty,ty',m1,m2. |
---|
| 1453 | value_eq E v1 v2 → |
---|
| 1454 | value_eq E v1' v2' → |
---|
| 1455 | memory_inj E m1 m2 → |
---|
| 1456 | ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→ |
---|
| 1457 | ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). |
---|
| 1458 | #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 |
---|
| 1459 | elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj |
---|
| 1460 | whd in match (sem_cmp ??????) in ⊢ ((??%?) → %); |
---|
| 1461 | cases (classify_cmp ty ty') normalize nodelta |
---|
| 1462 | [ 1: #tsz #tsg |
---|
| 1463 | @(value_eq_inversion E … Hvalue_eq1) normalize nodelta |
---|
| 1464 | [ 1: #v #Habsurd destruct (Habsurd) |
---|
| 1465 | | 3: #f #Habsurd destruct (Habsurd) |
---|
| 1466 | | 4: #Habsurd destruct (Habsurd) |
---|
| 1467 | | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
| 1468 | #sz #i |
---|
| 1469 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
| 1470 | [ 1: #v #Habsurd destruct (Habsurd) |
---|
| 1471 | | 3: #f #Habsurd destruct (Habsurd) |
---|
| 1472 | | 4: #Habsurd destruct (Habsurd) |
---|
| 1473 | | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
| 1474 | #sz' #i' cases tsg normalize nodelta |
---|
| 1475 | @intsize_eq_elim_elim |
---|
| 1476 | [ 1,3: #Hneq #Habsurd destruct (Habsurd) |
---|
| 1477 | | 2,4: #Heq destruct (Heq) normalize nodelta |
---|
[2438] | 1478 | #Heq destruct (Heq) |
---|
[2332] | 1479 | [ 1: cases (cmp_int ????) whd in match (of_bool ?); |
---|
| 1480 | | 2: cases (cmpu_int ????) whd in match (of_bool ?); ] |
---|
| 1481 | /3 by ex_intro, conj, vint_eq/ ] |
---|
| 1482 | | 3: #fsz |
---|
| 1483 | @(value_eq_inversion E … Hvalue_eq1) normalize nodelta |
---|
| 1484 | [ 1: #v #Habsurd destruct (Habsurd) |
---|
| 1485 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
| 1486 | | 4: #Habsurd destruct (Habsurd) |
---|
| 1487 | | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
| 1488 | #f |
---|
| 1489 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
| 1490 | [ 1: #v #Habsurd destruct (Habsurd) |
---|
| 1491 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
| 1492 | | 4: #Habsurd destruct (Habsurd) |
---|
| 1493 | | 5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] |
---|
| 1494 | #f' |
---|
| 1495 | #Heq destruct (Heq) cases (Fcmp op f f') |
---|
| 1496 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1497 | | 4: #ty1 #ty2 #Habsurd destruct (Habsurd) |
---|
[2438] | 1498 | | 2: #optn #typ |
---|
[2332] | 1499 | @(value_eq_inversion E … Hvalue_eq1) normalize nodelta |
---|
| 1500 | [ 1: #v #Habsurd destruct (Habsurd) |
---|
| 1501 | | 2: #sz #i #Habsurd destruct (Habsurd) |
---|
| 1502 | | 3: #f #Habsurd destruct (Habsurd) |
---|
| 1503 | | 5: #p1 #p2 #Hembed ] |
---|
| 1504 | @(value_eq_inversion E … Hvalue_eq2) normalize nodelta |
---|
| 1505 | [ 1,6: #v #Habsurd destruct (Habsurd) |
---|
| 1506 | | 2,7: #sz #i #Habsurd destruct (Habsurd) |
---|
| 1507 | | 3,8: #f #Habsurd destruct (Habsurd) |
---|
| 1508 | | 5,10: #p1' #p2' #Hembed' ] |
---|
| 1509 | [ 2,3: cases op whd in match (sem_cmp_mismatch ?); |
---|
| 1510 | #Heq destruct (Heq) |
---|
| 1511 | [ 1,3: %{Vfalse} @conj try @refl @vint_eq |
---|
| 1512 | | 2,4: %{Vtrue} @conj try @refl @vint_eq ] |
---|
| 1513 | | 4: cases op whd in match (sem_cmp_match ?); |
---|
| 1514 | #Heq destruct (Heq) |
---|
| 1515 | [ 2,4: %{Vfalse} @conj try @refl @vint_eq |
---|
| 1516 | | 1,3: %{Vtrue} @conj try @refl @vint_eq ] ] |
---|
| 1517 | lapply (mi_valid_pointers … Hinj p1' p2') |
---|
| 1518 | lapply (mi_valid_pointers … Hinj p1 p2) |
---|
| 1519 | cases (valid_pointer (mk_mem ???) p1') |
---|
| 1520 | [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
| 1521 | cases (valid_pointer (mk_mem ???) p1) |
---|
| 1522 | [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
| 1523 | #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 |
---|
| 1524 | >Hvalid1 >Hvalid2 normalize nodelta -H1 -H2 |
---|
| 1525 | elim p1 in Hembed; #b1 #o1 |
---|
| 1526 | elim p1' in Hembed'; #b1' #o1' |
---|
| 1527 | whd in match (pointer_translation ??); |
---|
| 1528 | whd in match (pointer_translation ??); |
---|
| 1529 | @(eq_block_elim … b1 b1') |
---|
| 1530 | [ 1: #Heq destruct (Heq) |
---|
| 1531 | cases (E b1') normalize nodelta |
---|
| 1532 | [ 1: #Habsurd destruct (Habsurd) ] |
---|
| 1533 | * #eb1' #eo1' normalize nodelta |
---|
| 1534 | #Heq1 #Heq2 #Heq3 destruct |
---|
| 1535 | >eq_block_b_b normalize nodelta |
---|
| 1536 | <cmp_offset_translation |
---|
| 1537 | cases (cmp_offset ???) normalize nodelta |
---|
| 1538 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1539 | | 2: #Hneq lapply (mi_disjoint … Hinj b1 b1') |
---|
| 1540 | cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 1541 | * #eb1 #eo1 |
---|
| 1542 | cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] |
---|
| 1543 | * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct |
---|
| 1544 | lapply (H ???? Hneq (refl ??) (refl ??)) |
---|
| 1545 | #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta |
---|
| 1546 | elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) |
---|
| 1547 | /3 by ex_intro, conj, vint_eq/ |
---|
| 1548 | ] |
---|
[2438] | 1549 | ] qed. *) |
---|
[2332] | 1550 | |
---|
[2438] | 1551 | (* |
---|
[2332] | 1552 | lemma binary_operation_value_eq : |
---|
| 1553 | ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2. |
---|
| 1554 | value_eq E v1 v2 → |
---|
| 1555 | value_eq E v1' v2' → |
---|
| 1556 | memory_inj E m1 m2 → |
---|
| 1557 | ∀r1. |
---|
| 1558 | sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 → |
---|
| 1559 | ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2. |
---|
| 1560 | #E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1 |
---|
| 1561 | cases op |
---|
| 1562 | whd in match (sem_binary_operation ??????); |
---|
| 1563 | whd in match (sem_binary_operation ??????); |
---|
| 1564 | [ 1: @add_value_eq try assumption |
---|
| 1565 | | 2: @sub_value_eq try assumption |
---|
| 1566 | | 3: @mul_value_eq try assumption |
---|
| 1567 | | 4: @div_value_eq try assumption |
---|
| 1568 | | 5: @mod_value_eq try assumption |
---|
| 1569 | | 6: @and_value_eq try assumption |
---|
| 1570 | | 7: @or_value_eq try assumption |
---|
| 1571 | | 8: @xor_value_eq try assumption |
---|
| 1572 | | 9: @shl_value_eq try assumption |
---|
| 1573 | | 10: @shr_value_eq try assumption |
---|
| 1574 | | *: @cmp_value_eq try assumption |
---|
[2438] | 1575 | ] qed. *) |
---|
[2332] | 1576 | |
---|
[2438] | 1577 | (* |
---|
[2332] | 1578 | lemma cast_value_eq : |
---|
| 1579 | ∀E,m1,m2,v1,v2. (* memory_inj E m1 m2 → *) value_eq E v1 v2 → |
---|
| 1580 | ∀ty,cast_ty,res. exec_cast m1 v1 ty cast_ty = OK ? res → |
---|
| 1581 | ∃res'. exec_cast m2 v2 ty cast_ty = OK ? res' ∧ value_eq E res res'. |
---|
| 1582 | #E #m1 #m2 #v1 #v2 (* #Hmemory_inj *) #Hvalue_eq #ty #cast_ty #res |
---|
| 1583 | @(value_eq_inversion … Hvalue_eq) |
---|
| 1584 | [ 1: #v normalize #Habsurd destruct (Habsurd) |
---|
| 1585 | | 2: #vsz #vi whd in match (exec_cast ????); |
---|
| 1586 | cases ty |
---|
| 1587 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] |
---|
| 1588 | normalize nodelta |
---|
| 1589 | [ 1,3,7,8,9: #Habsurd destruct (Habsurd) |
---|
| 1590 | | 2: @intsize_eq_elim_elim |
---|
| 1591 | [ 1: #Hneq #Habsurd destruct (Habsurd) |
---|
| 1592 | | 2: #Heq destruct (Heq) normalize nodelta |
---|
| 1593 | cases cast_ty |
---|
| 1594 | [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn |
---|
| 1595 | | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ] |
---|
| 1596 | normalize nodelta |
---|
| 1597 | [ 1,7,8,9: #Habsurd destruct (Habsurd) |
---|
| 1598 | | 2: #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ |
---|
| 1599 | | 3: #Heq destruct (Heq) /3 by ex_intro, conj, vfloat_eq/ |
---|
| 1600 | | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta |
---|
| 1601 | @eq_bv_elim |
---|
| 1602 | [ 1,3,5: #Heq destruct (Heq) >eq_intsize_identity normalize nodelta |
---|
| 1603 | whd in match (m_bind ?????); |
---|
| 1604 | #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ |
---|
| 1605 | | 2,4,6: #Hneq >eq_intsize_identity normalize nodelta |
---|
| 1606 | whd in match (m_bind ?????); |
---|
| 1607 | #Habsurd destruct (Habsurd) ] ] |
---|
| 1608 | ] |
---|
| 1609 | | 4,5,6: whd in match (try_cast_null ?????); normalize nodelta |
---|
| 1610 | @eq_bv_elim |
---|
| 1611 | [ 1,3,5: #Heq destruct (Heq) normalize nodelta |
---|
| 1612 | whd in match (m_bind ?????); #Habsurd destruct (Habsurd) |
---|
| 1613 | | 2,4,6: #Hneq normalize nodelta |
---|
| 1614 | whd in match (m_bind ?????); #Habsurd destruct (Habsurd) ] |
---|
| 1615 | ] |
---|
| 1616 | | 3: #f whd in match (exec_cast ????); |
---|
| 1617 | cases ty |
---|
| 1618 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n |
---|
| 1619 | | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] |
---|
| 1620 | normalize nodelta |
---|
| 1621 | [ 1,2,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] |
---|
| 1622 | cases cast_ty |
---|
| 1623 | [ 1: | 2: #csz #csg | 3: #cfl | 4: #cptrty | 5: #carrayty #cn |
---|
| 1624 | | 6: #ctl #cretty | 7: #cid #cfl | 8: #cid #cfl | 9: #ccomptrty ] |
---|
| 1625 | normalize nodelta |
---|
| 1626 | [ 1,4,5,6,7,8,9: #Habsurd destruct (Habsurd) ] |
---|
| 1627 | #Heq destruct (Heq) |
---|
| 1628 | [ 1: /3 by ex_intro, conj, vint_eq/ |
---|
| 1629 | | 2: /3 by ex_intro, conj, vfloat_eq/ ] |
---|
| 1630 | | 4: whd in match (exec_cast ????); |
---|
| 1631 | cases ty |
---|
| 1632 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n |
---|
| 1633 | | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] |
---|
| 1634 | normalize |
---|
| 1635 | [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] |
---|
| 1636 | cases cast_ty normalize nodelta |
---|
| 1637 | [ 1,10,19: #Habsurd destruct (Habsurd) |
---|
| 1638 | | 2,11,20: #csz #csg #Habsurd destruct (Habsurd) |
---|
| 1639 | | 3,12,21: #cfl #Habsurd destruct (Habsurd) |
---|
| 1640 | | 4,13,22: #cptrty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ |
---|
| 1641 | | 5,14,23: #carrayty #cn #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ |
---|
| 1642 | | 6,15,24: #ctl #cretty #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ |
---|
| 1643 | | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd) |
---|
| 1644 | | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd) |
---|
| 1645 | | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] |
---|
| 1646 | | 5: #p1 #p2 #Hembed whd in match (exec_cast ????); |
---|
| 1647 | cases ty |
---|
| 1648 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ptrty | 5: #arrayty #n |
---|
| 1649 | | 6: #tl #retty | 7: #id #fl | 8: #id #fl | 9: #comptrty ] |
---|
| 1650 | normalize |
---|
| 1651 | [ 1,2,3,7,8,9: #Habsurd destruct (Habsurd) ] |
---|
| 1652 | cases cast_ty normalize nodelta |
---|
| 1653 | [ 1,10,19: #Habsurd destruct (Habsurd) |
---|
| 1654 | | 2,11,20: #csz #csg #Habsurd destruct (Habsurd) |
---|
| 1655 | | 3,12,21: #cfl #Habsurd destruct (Habsurd) |
---|
| 1656 | | 4,13,22: #cptrty #Heq destruct (Heq) %{(Vptr p2)} @conj try @refl @vptr_eq assumption |
---|
| 1657 | | 5,14,23: #carrayty #cn #Heq destruct (Heq) |
---|
| 1658 | %{(Vptr p2)} @conj try @refl @vptr_eq assumption |
---|
| 1659 | | 6,15,24: #ctl #cretty #Heq destruct (Heq) |
---|
| 1660 | %{(Vptr p2)} @conj try @refl @vptr_eq assumption |
---|
| 1661 | | 7,16,25: #cid #cfl #Habsurd destruct (Habsurd) |
---|
| 1662 | | 8,17,26: #cid #cfl #Habsurd destruct (Habsurd) |
---|
| 1663 | | 9,18,27: #ccomptrty #Habsurd destruct (Habsurd) ] |
---|
| 1664 | qed. |
---|
| 1665 | |
---|
| 1666 | lemma bool_of_val_value_eq : |
---|
| 1667 | ∀E,v1,v2. value_eq E v1 v2 → |
---|
| 1668 | ∀ty,b.exec_bool_of_val v1 ty = OK ? b → exec_bool_of_val v2 ty = OK ? b. |
---|
| 1669 | #E #v1 #v2 #Hvalue_eq #ty #b |
---|
| 1670 | @(value_eq_inversion … Hvalue_eq) // |
---|
| 1671 | [ 1: #v #H normalize in H; destruct (H) |
---|
| 1672 | | 2: #p1 #p2 #Hembed #H @H ] qed. |
---|
| 1673 | |
---|
[2438] | 1674 | *) |
---|
[2332] | 1675 | (* |
---|
| 1676 | lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext. |
---|
| 1677 | ∀E:embedding. |
---|
| 1678 | ∀Hext:memory_ext E m1 m2. |
---|
| 1679 | switch_removal_globals E ? fundef_switch_removal ge ge' → |
---|
| 1680 | disjoint_extension en1 m1 en2 m2 ext E Hext → |
---|
| 1681 | ext_fresh_for_genv ext ge → |
---|
| 1682 | (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧ |
---|
| 1683 | (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)). |
---|
| 1684 | #ge #ge' #en1 #m1 #en2 #m2 #ext #E #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv |
---|
| 1685 | @expr_lvalue_ind_combined |
---|
| 1686 | [ 1: #csz #cty #i #a1 |
---|
| 1687 | whd in match (exec_expr ????); elim cty |
---|
| 1688 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
| 1689 | normalize nodelta |
---|
| 1690 | [ 2: cases (eq_intsize csz sz) normalize nodelta |
---|
| 1691 | [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/ |
---|
| 1692 | | 2: #Habsurd destruct (Habsurd) ] |
---|
| 1693 | | 4,5,6: #_ #H destruct (H) |
---|
| 1694 | | *: #H destruct (H) ] |
---|
| 1695 | | 2: #ty #fl #a1 |
---|
| 1696 | whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/ |
---|
| 1697 | | 3: * |
---|
| 1698 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 1699 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 1700 | #ty whd in ⊢ (% → ?); #Hind try @I |
---|
| 1701 | whd in match (Plvalue ???); |
---|
| 1702 | [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1 |
---|
| 1703 | cases (exec_lvalue' ge en1 m1 ? ty) in Hind; |
---|
| 1704 | [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) |
---|
| 1705 | | 1,3,5: #b1 #H elim (H b1 (refl ??)) #b2 * |
---|
| 1706 | elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2 |
---|
| 1707 | #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq |
---|
| 1708 | whd in match (load_value_of_type' ???); |
---|
| 1709 | whd in match (load_value_of_type' ???); |
---|
| 1710 | lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq) |
---|
| 1711 | cases (load_value_of_type ty m1 bl1 o1) |
---|
| 1712 | [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd) |
---|
| 1713 | | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq) |
---|
| 1714 | elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload |
---|
| 1715 | normalize /4 by ex_intro, conj/ |
---|
| 1716 | ] ] ] |
---|
| 1717 | | 4: #v #ty whd * * #b1 #o1 #tr1 |
---|
| 1718 | whd in match (exec_lvalue' ?????); |
---|
| 1719 | whd in match (exec_lvalue' ?????); |
---|
| 1720 | lapply (Hdisjoint v) |
---|
| 1721 | lapply (Hext_fresh_for_genv v) |
---|
| 1722 | cases (mem_assoc_env v ext) #Hglobal |
---|
| 1723 | [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1 |
---|
| 1724 | >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?); |
---|
| 1725 | >(Hglobal (refl ??)) normalize |
---|
| 1726 | #Habsurd destruct (Habsurd) |
---|
| 1727 | | 2: normalize nodelta |
---|
| 1728 | cases (lookup ?? en1 v) normalize nodelta |
---|
| 1729 | [ 1: #Hlookup2 >Hlookup2 normalize nodelta |
---|
| 1730 | lapply (rg_find_symbol … Hrelated v) |
---|
| 1731 | cases (find_symbol ???) normalize |
---|
| 1732 | [ 1: #_ #Habsurd destruct (Habsurd) |
---|
| 1733 | | 2: #block cases (lookup ?? (symbols clight_fundef ge') v) |
---|
| 1734 | [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse) |
---|
| 1735 | | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq) |
---|
| 1736 | %{〈block',mk_offset (zero offset_size),[]〉} @conj try @refl |
---|
| 1737 | normalize /2/ |
---|
| 1738 | ] ] |
---|
| 1739 | | 2: #block |
---|
| 1740 | cases (lookup ?? en2 v) normalize nodelta |
---|
| 1741 | [ 1: #Hfalse @(False_ind … Hfalse) |
---|
| 1742 | | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq) |
---|
| 1743 | %{〈b, zero_offset, E0〉} @conj try @refl |
---|
| 1744 | normalize /2/ |
---|
| 1745 | ] ] ] |
---|
| 1746 | | 5: #e #ty whd in ⊢ (% → %); |
---|
| 1747 | whd in match (exec_lvalue' ?????); |
---|
| 1748 | whd in match (exec_lvalue' ?????); |
---|
| 1749 | cases (exec_expr ge en1 m1 e) |
---|
| 1750 | [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' * #Heq >Heq normalize nodelta |
---|
| 1751 | * elim v1 normalize nodelta |
---|
| 1752 | [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd) |
---|
| 1753 | | 2: #sz #i #_ #_ #a1 #Habsurd destruct (Habsurd) |
---|
| 1754 | | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd) |
---|
| 1755 | | 4: #_ #_ #a1 #Habsurd destruct (Habsurd) |
---|
| 1756 | | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq |
---|
| 1757 | >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2 |
---|
| 1758 | #Hvalue_eq normalize |
---|
| 1759 | cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
| 1760 | * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace) |
---|
| 1761 | * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize |
---|
| 1762 | %{〈b2,mk_offset (addition_n ? (offv o1') (offv o2')),tr1''〉} @conj try @refl |
---|
| 1763 | normalize @conj // ] |
---|
| 1764 | | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ] |
---|
| 1765 | | 6: #ty #e #ty' |
---|
| 1766 | #Hsim @(exec_lvalue_expr_elim … Hsim) |
---|
| 1767 | cases ty |
---|
| 1768 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
| 1769 | * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/ |
---|
| 1770 | #tr #H @conj try @refl try assumption |
---|
| 1771 | | 7: #ty #op #e |
---|
| 1772 | #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq |
---|
| 1773 | lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq) |
---|
| 1774 | cases (sem_unary_operation op v1 (typeof e)) normalize nodelta |
---|
| 1775 | [ 1: #_ @I |
---|
| 1776 | | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq |
---|
| 1777 | normalize /2/ ] |
---|
| 1778 | | 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 |
---|
| 1779 | @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq |
---|
| 1780 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 1781 | [ 2: #error // ] |
---|
| 1782 | * #val #trace normalize in ⊢ (% → ?); #Hsim2 |
---|
| 1783 | elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2 |
---|
| 1784 | whd in match (m_bind ?????); whd in match (m_bind ?????); |
---|
| 1785 | lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext)) |
---|
| 1786 | cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1) |
---|
| 1787 | [ 1: #_ // ] |
---|
| 1788 | #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq #Hvalue_eq_opval |
---|
| 1789 | >Hopval_eq normalize destruct /2 by conj/ |
---|
| 1790 | | 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) |
---|
| 1791 | #v1 #v2 #trace #Hvalue_eq lapply (cast_value_eq E m1 m2 … Hvalue_eq (typeof e) cast_ty) |
---|
| 1792 | cases (exec_cast m1 v1 (typeof e) cast_ty) |
---|
| 1793 | [ 2: #error #_ normalize @I |
---|
| 1794 | | 1: #res #H lapply (H res (refl ??)) whd in match (m_bind ?????); |
---|
| 1795 | * #res' * #Hexec_cast >Hexec_cast #Hvalue_eq normalize nodelta |
---|
| 1796 | @conj // ] |
---|
| 1797 | | 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 |
---|
| 1798 | @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq |
---|
| 1799 | lapply (bool_of_val_value_eq E v1 v2 Hvalue_eq (typeof e1)) |
---|
| 1800 | cases (exec_bool_of_val ? (typeof e1)) #b |
---|
| 1801 | [ 2: #_ normalize @I ] |
---|
| 1802 | #H lapply (H ? (refl ??)) #Hexec >Hexec normalize |
---|
| 1803 | cases b normalize nodelta |
---|
| 1804 | [ 1: (* true branch *) |
---|
| 1805 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 1806 | [ 2: #error normalize #_ @I |
---|
| 1807 | | 1: * #e2v #e2tr normalize #H elim (H ? (refl ??)) |
---|
| 1808 | * #e2v' #e2tr' * #Hexec2 >Hexec2 * #Hvalue_eq2 #Htrace_eq2 normalize |
---|
| 1809 | destruct @conj try // ] |
---|
| 1810 | | 2: (* false branch *) |
---|
| 1811 | cases (exec_expr ge en1 m1 e3) in Hsim3; |
---|
| 1812 | [ 2: #error normalize #_ @I |
---|
| 1813 | | 1: * #e3v #e3tr normalize #H elim (H ? (refl ??)) |
---|
| 1814 | * #e3v' #e3tr' * #Hexec3 >Hexec3 * #Hvalue_eq3 #Htrace_eq3 normalize |
---|
| 1815 | destruct @conj // ] ] |
---|
| 1816 | | 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 |
---|
| 1817 | @(exec_expr_expr_elim … Hsim1) #v1 #v1' #trace #Hvalue_eq |
---|
| 1818 | lapply (bool_of_val_value_eq E v1 v1' Hvalue_eq (typeof e1)) |
---|
| 1819 | cases (exec_bool_of_val v1 (typeof e1)) |
---|
| 1820 | [ 2,4: #error #_ normalize @I ] |
---|
| 1821 | #b cases b #H lapply (H ? (refl ??)) #Heq >Heq |
---|
| 1822 | whd in match (m_bind ?????); |
---|
| 1823 | whd in match (m_bind ?????); |
---|
| 1824 | [ 2,3: normalize @conj try @refl try @vint_eq ] |
---|
| 1825 | cases (exec_expr ge en1 m1 e2) in Hsim2; |
---|
| 1826 | [ 2,4: #error #_ normalize @I ] |
---|
| 1827 | * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta elim (H2 ? (refl ??)) |
---|
| 1828 | * #v2' #tr2' * #Heq2 * #Hvalue_eq2 #Htrace2 >Heq2 normalize nodelta |
---|
| 1829 | lapply (bool_of_val_value_eq E v2 v2' Hvalue_eq2 (typeof e2)) |
---|
| 1830 | cases (exec_bool_of_val v2 (typeof e2)) |
---|
| 1831 | [ 2,4: #error #_ normalize @I ] |
---|
| 1832 | #b2 #H3 lapply (H3 ? (refl ??)) #Heq3 >Heq3 normalize nodelta |
---|
| 1833 | destruct @conj try @conj // |
---|
| 1834 | cases b2 whd in match (of_bool ?); @vint_eq |
---|
| 1835 | | 13: #ty #ty' cases ty |
---|
| 1836 | [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n |
---|
| 1837 | | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ] |
---|
| 1838 | whd in match (exec_expr ????); whd |
---|
| 1839 | * #v #trace #Heq destruct %{〈Vint sz (repr sz (sizeof ty')), E0〉} |
---|
| 1840 | @conj try @refl @conj // |
---|
| 1841 | | 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr normalize nodelta |
---|
| 1842 | whd in match (exec_lvalue' ?????); |
---|
| 1843 | whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty); |
---|
| 1844 | whd in match (typeof ?); |
---|
| 1845 | cases aggregty in Hsim; |
---|
| 1846 | [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n' |
---|
| 1847 | | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ] |
---|
| 1848 | normalize nodelta #Hsim |
---|
| 1849 | [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ] |
---|
| 1850 | whd in match (m_bind ?????); |
---|
| 1851 | whd in match (m_bind ?????); |
---|
| 1852 | whd in match (exec_lvalue ge en1 m1 (Expr ed ?)); |
---|
| 1853 | cases (exec_lvalue' ge en1 m1 ed ?) in Hsim; |
---|
| 1854 | [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] |
---|
| 1855 | * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H elim (H ? (refl ??)) |
---|
| 1856 | * * #b1' #o1' #tr1' * #Hexec normalize nodelta * #Hvalue_eq #Htrace_eq |
---|
| 1857 | whd in match (exec_lvalue ????); >Hexec normalize nodelta |
---|
| 1858 | [ 2: #Heq destruct (Heq) %{〈 b1',o1',tr1'〉} @conj // |
---|
| 1859 | normalize @conj // ] |
---|
| 1860 | cases (field_offset i fl') |
---|
| 1861 | [ 2: #error normalize #Habsurd destruct (Habsurd) ] |
---|
| 1862 | #offset whd in match (m_bind ?????); #Heq destruct (Heq) |
---|
| 1863 | whd in match (m_bind ?????); |
---|
| 1864 | %{〈b1',shift_offset (bitsize_of_intsize I32) o1' (repr I32 offset),tr1'〉} @conj |
---|
| 1865 | destruct // normalize nodelta @conj try @refl @vptr_eq |
---|
| 1866 | -H lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hptr_eq |
---|
| 1867 | whd in match (pointer_translation ??); |
---|
| 1868 | whd in match (pointer_translation ??); |
---|
| 1869 | cases (E b) |
---|
| 1870 | [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] |
---|
| 1871 | * #b' #o' normalize nodelta #Heq destruct (Heq) destruct (Hptr_eq) |
---|
| 1872 | cut (offset_plus (mk_offset (addition_n offset_size |
---|
| 1873 | (offv o1) |
---|
| 1874 | (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 offset)))) o' |
---|
| 1875 | = (shift_offset (bitsize_of_intsize I32) (offset_plus o1 o') (repr I32 offset))) |
---|
| 1876 | [ whd in match (shift_offset ???) in ⊢ (???%); |
---|
| 1877 | whd in match (offset_plus ??) in ⊢ (??%%); |
---|
| 1878 | /3 by associative_addition_n, commutative_addition_n, refl/ ] |
---|
| 1879 | #Heq >Heq @refl |
---|
| 1880 | | 15: #ty #l #e #Hsim |
---|
| 1881 | @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq normalize nodelta @conj // |
---|
| 1882 | | 16: * |
---|
| 1883 | [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1 |
---|
| 1884 | | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ] |
---|
| 1885 | #ty normalize in ⊢ (% → ?); |
---|
| 1886 | [ 3,4,13: @False_ind |
---|
| 1887 | | *: #_ normalize #a1 #Habsurd destruct (Habsurd) ] |
---|
| 1888 | ] qed. *) |
---|