Changeset 2608 for src/common/GenMem.ma


Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (8 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/GenMem.ma

    r2332 r2608  
    4949  λA,x,v,f.
    5050    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
    51    
     51
    5252lemma update_block_s:
    5353  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    5454  update_block … x v f x = v.
    55 #A * * #ix #v #f whd in ⊢ (??%?);
     55#A * #ix #v #f whd in ⊢ (??%?);
    5656>eq_block_b_b //
    5757qed.
     
    119119qed.
    120120
    121 let rec alloc (m:mem) (lo:Z) (hi:Z) (r:region) on m : mem × Σb:block. block_region b = r
    122   let b ≝ mk_block r (nextblock … m) in
     121let rec alloc (m:mem) (lo:Z) (hi:Z) (*(r:region)*) on m : mem × block (*Σb:block. block_region b = r *)
     122  let b ≝ mk_block (nextblock … m) in
    123123  〈mk_mem
    124124    (update_block … b
     
    128128    (succ_nextblock_pos … m),
    129129    b〉.
    130 % qed.
     130(* % qed. *)
    131131
    132132(* Freeing a block.  Return the updated memory state where the given
Note: See TracChangeset for help on using the changeset viewer.