Changeset 3178 for src/Clight/memoryInjections.ma
 Timestamp:
 Apr 25, 2013, 6:03:24 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2822 r3178 759 759 #Halloc destruct (Halloc) /2/ 760 760 qed. 761 762 lemma new_block_invalid_before_alloc : 763 ∀m,m',z1,z2,new_block. 764 alloc m z1 z2 = 〈m', new_block〉 → 765 ¬valid_block m new_block. 766 * #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *) 767 whd in match (alloc ???(*?*)); whd in match (valid_block ??); 768 #Halloc destruct (Halloc) /2/ 769 qed. 770 761 771 762 772 (* All data in a valid block is unchanged after an alloc. *) … … 1467 1477 ] qed. 1468 1478 1479 (* And show the compatibility of the new injection. *) 1480 1481 lemma alloc_memory_inj_m1_to_m2_compat : 1482 ∀E:embedding. 1483 ∀m1,m2,m1':mem. 1484 ∀z1,z2:Z. 1485 ∀target,new_block. 1486 ∀delta:offset. 1487 alloc m1 z1 z2 = 〈m1', new_block〉 → 1488 memory_inj E m1 m2 → 1489 embedding_compatible E (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x). 1490 #E #m1 #m2 #m1' #z1 #z2 #target #new_block #delta #ALLOC #MI 1491 whd 1492 #b @eq_block_elim 1493 [ #E destruct %1 @(mi_freeblock … MI) /2/ 1494  #_ %2 % 1495 ] qed. 1496 1497 1469 1498 (*  *) 1470 1499 (* Lemmas pertaining to [free] *)
Note: See TracChangeset
for help on using the changeset viewer.