Ignore:
Timestamp:
Apr 25, 2013, 6:03:24 PM (6 years ago)
Author:
campbell
Message:

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2822 r3178  
    759759#Halloc destruct (Halloc) /2/
    760760qed.
     761
     762lemma 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 *)
     767whd in match (alloc ???(*?*)); whd in match (valid_block ??);
     768#Halloc destruct (Halloc) /2/
     769qed.
     770
    761771
    762772(* All data in a valid block is unchanged after an alloc. *)
     
    14671477] qed.   
    14681478
     1479(* And show the compatibility of the new injection. *)
     1480
     1481lemma 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
     1491whd
     1492#b @eq_block_elim
     1493[ #E destruct %1 @(mi_freeblock … MI) /2/
     1494| #_ %2 %
     1495] qed.
     1496
     1497
    14691498(* -------------------------------------- *)
    14701499(* Lemmas pertaining to [free] *)
Note: See TracChangeset for help on using the changeset viewer.