Ignore:
Timestamp:
Feb 11, 2011, 4:45:28 PM (9 years ago)
Author:
campbell
Message:

First pass at moving regions to block type.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Mem.ma

    r487 r496  
    4040    λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ].
    4141   
    42 (* Implicit Arguments update [A].*)
    43 
    4442lemma update_s:
    4543  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A.
     
    6159//; qed.
    6260
     61definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝
     62  λA,x,v,f.
     63    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
     64   
     65lemma update_block_s:
     66  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
     67  update_block … x v f x = v.
     68#A * * #ix #v #f whd in ⊢ (??%?);
     69>(eqZb_z_z …) //;
     70qed.
     71
     72lemma update_block_o:
     73  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block.
     74  x ≠ y → update_block … x v f y = f y.
     75#A #x #v #f #y #H whd in ⊢ (??%?);
     76@eq_block_elim //;
     77#H2 cases H;#H3 elim (H3 ?);//;
     78qed.
     79
     80(* FIXME: workaround for lack of nunfold *)
     81lemma unfold_update_block : ∀A,x,v,f,y.
     82  update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ].
     83//; qed.
     84
    6385
    6486(* * Structure of memory states *)
     
    87109  low: Z;
    88110  high: Z;
    89   contents: contentmap;
    90   space: region
     111  contents: contentmap
    91112}.
    92113
    93 (* A memory state is a mapping from block addresses (represented by [Z]
    94   integers) to blocks.  We also maintain the address of the next
     114(* A memory state is a mapping from block addresses (represented by memory
     115  regions and integers) to blocks.  We also maintain the address of the next
    95116  unallocated block, and a proof that this address is positive. *)
    96117
    97118record mem : Type[0] ≝ {
    98   blocks: Z -> block_contents;
    99   nextblock: block;
     119  blocks: block -> block_contents;
     120  nextblock: Z;
    100121  nextblock_pos: OZ < nextblock
    101122}.
     
    195216qed.
    196217
    197 definition empty_block : Z → Z → region → block_contents ≝
    198   λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.
     218definition empty_block : Z → Z → block_contents ≝
     219  λlo,hi.mk_block_contents lo hi (λy. Undef).
    199220
    200221definition empty: mem ≝
    201   mk_mem (λx.empty_block OZ OZ Any) (pos one) one_pos.
    202 
    203 definition nullptr: block ≝ OZ.
     222  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
     223
     224definition nullptr: block ≝ 〈Any,OZ〉.
    204225
    205226(* Allocation of a fresh block with the given bounds.  Return an updated
     
    216237
    217238definition alloc : mem → Z → Z → region → mem × block ≝
    218   λm,lo,hi,bty.〈mk_mem
    219               (update … (nextblock m)
    220                  (empty_block lo hi bty)
     239  λm,lo,hi,r.〈mk_mem
     240              (update_block … 〈r,nextblock m〉
     241                 (empty_block lo hi)
    221242                 (blocks m))
    222243              (Zsucc (nextblock m))
    223244              (succ_nextblock_pos m),
    224             nextblock m〉.
     245            〈r,nextblock m〉〉.
    225246
    226247(* Freeing a block.  Return the updated memory state where the given
     
    231252
    232253definition free ≝
    233   λm,b.mk_mem (update … b
    234                 (empty_block OZ OZ Any)
     254  λm,b.mk_mem (update_block … b
     255                (empty_block OZ OZ)
    235256                (blocks m))
    236257        (nextblock m)
     
    252273definition high_bound : mem → block → Z ≝
    253274  λm,b.high (blocks m b).
    254 definition block_space: mem → block → region ≝
    255   λm,b.space (blocks m b).
     275definition block_region: mem → block → region ≝
     276  λm,b.\fst b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
    256277
    257278(* A block address is valid if it was previously allocated. It remains valid
    258279  even after being freed. *)
    259280
     281(* TODO: should this check for region? *)
    260282definition valid_block : mem → block → Prop ≝
    261   λm,b.b < nextblock m.
     283  λm,b.\snd b < nextblock m.
    262284
    263285(* FIXME: hacks to get around lack of nunfold *)
     
    266288lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b).
    267289//; qed.
    268 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (b < nextblock m).
     290lemma unfold_valid_block : ∀m,b. (valid_block m b) = (\snd b < nextblock m).
    269291//; qed.
    270292
     
    564586qed.
    565587*)
    566 (* pointer_compat block_space pointer_space *)
     588(* pointer_compat block_region pointer_region *)
    567589
    568590inductive pointer_compat : region → region → Prop ≝
    569 same_compat : ∀s. pointer_compat s s
    570 | pxdata_compat : pointer_compat PData XData
     591      same_compat : ∀s. pointer_compat s s
     592|      pxdata_compat : pointer_compat PData XData
    571593| unspecified_compat : ∀p. pointer_compat Any p
    572 | universal_compat : ∀b. pointer_compat b Any.
     594|   universal_compat : ∀b. pointer_compat b Any.
    573595
    574596lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
     
    581603λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    582604
    583 (* [valid_access m chunk psp b ofs] holds if a memory access (load or store)
     605(* [valid_access m chunk r b ofs] holds if a memory access (load or store)
    584606    of the given chunk is possible in [m] at address [b, ofs].
    585607    This means:
     
    587609- The range of bytes accessed is within the bounds of [b].
    588610- The offset [ofs] is aligned.
    589 - The pointer classs [psp] is compatible with the class of [b].
     611- The pointer representation (i.e., region) [r] is compatible with the class of [b].
    590612*)
    591613
    592 inductive valid_access (m: mem) (chunk: memory_chunk) (psp: region) (b: block) (ofs: Z)
     614inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z)
    593615            : Prop ≝
    594616  | valid_access_intro:
     
    597619      ofs + size_chunk chunk ≤ high_bound m b →
    598620      (align_chunk chunk ∣ ofs) →
    599       pointer_compat (block_space m b) psp
    600       valid_access m chunk psp b ofs.
     621      pointer_compat (block_region m b) r
     622      valid_access m chunk r b ofs.
    601623
    602624(* The following function checks whether accessing the given memory chunk
     
    605627(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    606628let rec in_bounds
    607   (m:mem) (chunk:memory_chunk) (psp:region) (b:block) (ofs:Z) on b : 
    608     Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?.
    609 @(Zltb_elim_Type0 b (nextblock m)) #Hnext
    610 [ @(Zleb_elim_Type0 (low_bound m b) ofs) #Hlo
    611     [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)) #Hhi
     629  (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : 
     630    Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?.
     631cases b #br #bi
     632@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
     633[ @(Zleb_elim_Type0 (low_bound m 〈br,bi〉) ofs) #Hlo
     634    [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m 〈br,bi〉)) #Hhi
    612635        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    613           [ cases (pointer_compat_dec (block_space m b) psp); #Hcl
    614             [ %1 % // ]
     636          [ cases (pointer_compat_dec (block_region m 〈br,bi〉) r); #Hcl
     637            [ %1 % // @Hnext ]
    615638          ]
    616639        ]
    617640    ]
    618641]
    619 %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) //;
     642%2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval | 3: @Hnext ]
    620643qed.
    621644
    622645lemma in_bounds_true:
    623   ∀m,chunk,psp,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
    624   valid_access m chunk psp b ofs ->
    625   (match in_bounds m chunk psp b ofs with
     646  ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
     647  valid_access m chunk r b ofs ->
     648  (match in_bounds m chunk r b ofs with
    626649   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
    627 #m #chunk #psp #b #ofs #A #a1 #a2 #H
    628 cases (in_bounds m chunk psp b ofs);normalize;#H1
     650#m #chunk #r #b #ofs #A #a1 #a2 #H
     651cases (in_bounds m chunk r b ofs);normalize;#H1
    629652[//
    630653|elim (?:False); @(absurd ? H H1)]
    631654qed.
    632655
    633 (* [valid_pointer] holds if the given block address is valid and the
     656(* [valid_pointer] holds if the given block address is valid (and can be
     657  represented in a pointer with the region [r]) and the
    634658  given offset falls within the bounds of the corresponding block. *)
    635659
    636660definition valid_pointer : mem → region → block → Z → bool ≝
    637 λm,psp,b,ofs. Zltb b (nextblock m) ∧
     661λm,r,b,ofs. Zltb (\snd b) (nextblock m) ∧
    638662  Zleb (low_bound m b) ofs ∧
    639663  Zltb ofs (high_bound m b) ∧
    640   is_pointer_compat (block_space m b) psp.
    641 
    642 (* [load chunk m b ofs] perform a read in memory state [m], at address
     664  is_pointer_compat (block_region m b) r.
     665
     666(* [load chunk m r b ofs] perform a read in memory state [m], at address
    643667  [b] and offset [ofs].  [None] is returned if the address is invalid
    644   or the memory access is out of bounds. *)
     668  or the memory access is out of bounds or the address cannot be represented
     669  by a pointer with region [r]. *)
    645670
    646671definition load : memory_chunk → mem → region → block → Z → option val ≝
    647 λchunk,m,psp,b,ofs.
    648   match in_bounds m chunk psp b ofs with
     672λchunk,m,r,b,ofs.
     673  match in_bounds m chunk r b ofs with
    649674  [ inl _ ⇒ Some ? (load_result chunk
    650675           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
     
    652677
    653678lemma load_inv:
    654   ∀chunk,m,psp,b,ofs,v.
    655   load chunk m psp b ofs = Some ? v →
    656   valid_access m chunk psp b ofs ∧
     679  ∀chunk,m,r,b,ofs,v.
     680  load chunk m r b ofs = Some ? v →
     681  valid_access m chunk r b ofs ∧
    657682  v = load_result chunk
    658683           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
    659 #chunk #m #psp #b #ofs #v whd in ⊢ (??%? → ?);
    660 cases (in_bounds m chunk psp b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H
     684#chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?);
     685cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H
    661686[ % //; destruct; //;
    662687| destruct
     
    669694let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    670695  match addr with
    671   [ Vptr psp b ofs ⇒ load chunk m psp b (signed ofs)
     696  [ Vptr r b ofs ⇒ load chunk m r b (signed ofs)
    672697  | _ ⇒ None ? ].
    673698
     
    679704  let c ≝ (blocks m b) in
    680705  mk_mem
    681     (update ? b
     706    (update_block ? b
    682707        (mk_block_contents (low c) (high c)
    683                  (setN (pred_size_chunk chunk) ofs v (contents c)) (space c))
     708                 (setN (pred_size_chunk chunk) ofs v (contents c)))
    684709        (blocks m))
    685710    (nextblock m)
    686711    (nextblock_pos m).
    687712
    688 (* [store chunk m b ofs v] perform a write in memory state [m].
     713(* [store chunk m r b ofs v] perform a write in memory state [m].
    689714  Value [v] is stored at address [b] and offset [ofs].
    690715  Return the updated memory store, or [None] if the address is invalid
    691   or the memory access is out of bounds. *)
     716  or the memory access is out of bounds or the address cannot be represented
     717  by a pointer with region [r]. *)
    692718
    693719definition store : memory_chunk → mem → region → block → Z → val → option mem ≝
    694 λchunk,m,psp,b,ofs,v.
    695   match in_bounds m chunk psp b ofs with
     720λchunk,m,r,b,ofs,v.
     721  match in_bounds m chunk r b ofs with
    696722  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
    697723  | inr _ ⇒ None ? ].
    698724
    699725lemma store_inv:
    700   ∀chunk,m,psp,b,ofs,v,m'.
    701   store chunk m psp b ofs v = Some ? m' →
    702   valid_access m chunk psp b ofs ∧
     726  ∀chunk,m,r,b,ofs,v,m'.
     727  store chunk m r b ofs v = Some ? m' →
     728  valid_access m chunk r b ofs ∧
    703729  m' = unchecked_store chunk m b ofs v.
    704 #chunk #m #psp #b #ofs #v #m' whd in ⊢ (??%? → ?);
     730#chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?);
    705731(*9*)
    706 cases (in_bounds m chunk psp b ofs);#Hv whd in ⊢(??%? → ?);#Heq
     732cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq
    707733[% [//|destruct;//]
    708734|destruct]
     
    715741λchunk,m,addr,v.
    716742  match addr with
    717   [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v
     743  [ Vptr r b ofs ⇒ store chunk m r b (signed ofs) v
    718744  | _ ⇒ None ? ].
    719745
     
    729755
    730756lemma valid_access_valid_block:
    731   ∀m,chunk,psp,b,ofs. valid_access m chunk psp b ofs → valid_block m b.
    732 #m #chunk #psp #b #ofs #H
     757  ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b.
     758#m #chunk #r #b #ofs #H
    733759elim H;//;
    734760qed.
    735761
    736762lemma valid_access_aligned:
    737   ∀m,chunk,psp,b,ofs.
    738   valid_access m chunk psp b ofs → (align_chunk chunk ∣ ofs).
    739 #m #chunk #psp #b #ofs #H
     763  ∀m,chunk,r,b,ofs.
     764  valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs).
     765#m #chunk #r #b #ofs #H
    740766elim H;//;
    741767qed.
    742768
    743769lemma valid_access_compat:
    744   ∀m,chunk1,chunk2,psp,b,ofs.
     770  ∀m,chunk1,chunk2,r,b,ofs.
    745771  size_chunk chunk1 = size_chunk chunk2 →
    746   valid_access m chunk1 psp b ofs →
    747   valid_access m chunk2 psp b ofs.
    748 #m #chunk #chunk2 #psp #b #ofs #H1 #H2
     772  valid_access m chunk1 r b ofs →
     773  valid_access m chunk2 r b ofs.
     774#m #chunk #chunk2 #r #b #ofs #H1 #H2
    749775elim H2;#H3 #H4 #H5 #H6 #H7
    750776>H1 in H5 #H5
     
    758784
    759785theorem valid_access_load:
    760   ∀m,chunk,psp,b,ofs.
    761   valid_access m chunk psp b ofs →
    762   ∃v. load chunk m psp b ofs = Some ? v.
    763 #m #chunk #psp #b #ofs #H %
     786  ∀m,chunk,r,b,ofs.
     787  valid_access m chunk r b ofs →
     788  ∃v. load chunk m r b ofs = Some ? v.
     789#m #chunk #r #b #ofs #H %
    764790[2:whd in ⊢ (??%?);@in_bounds_true //;
    765791|skip]
     
    767793
    768794theorem load_valid_access:
    769   ∀m,chunk,psp,b,ofs,v.
    770   load chunk m psp b ofs = Some ? v →
    771   valid_access m chunk psp b ofs.
    772 #m #chunk #psp #b #ofs #v #H
     795  ∀m,chunk,r,b,ofs,v.
     796  load chunk m r b ofs = Some ? v →
     797  valid_access m chunk r b ofs.
     798#m #chunk #r #b #ofs #v #H
    773799cases (load_inv … H);//;
    774800qed.
     
    779805
    780806lemma valid_access_store:
    781   ∀m1,chunk,psp,b,ofs,v.
    782   valid_access m1 chunk psp b ofs →
    783   ∃m2. store chunk m1 psp b ofs v = Some ? m2.
    784 #m1 #chunk #psp #b #ofs #v #H
     807  ∀m1,chunk,r,b,ofs,v.
     808  valid_access m1 chunk r b ofs →
     809  ∃m2. store chunk m1 r b ofs v = Some ? m2.
     810#m1 #chunk #r #b #ofs #v #H
    785811%
    786812[2:@in_bounds_true //
     
    791817
    792818lemma low_bound_store:
    793   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     819  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    794820  ∀b'.low_bound m2 b' = low_bound m1 b'.
    795 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     821#chunk #m1 #r #b #ofs #v #m2 #STORE
    796822#b' cases (store_inv … STORE)
    797823#H1 #H2 >H2
    798824whd in ⊢ (??(?%?)?) whd in ⊢ (??%?)
    799 whd in ⊢ (??(?%)?) lapply (eqZb_to_Prop b' b)
    800 cases (eqZb b' b) normalize //
     825whd in ⊢ (??(?%)?) @eq_block_elim #E
     826normalize //
    801827qed.
    802828
    803829lemma nextblock_store :
    804   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     830  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    805831  nextblock m2 = nextblock m1.
    806 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     832#chunk #m1 #r #b #ofs #v #m2 #STORE
    807833cases (store_inv … STORE);
    808834#Hvalid #Heq
     
    811837
    812838lemma high_bound_store:
    813   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     839  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    814840  ∀b'. high_bound m2 b' = high_bound m1 b'.
    815 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     841#chunk #m1 #r #b #ofs #v #m2 #STORE
    816842#b' cases (store_inv … STORE);
    817843#Hvalid #H
    818844>H
    819845whd in ⊢ (??(?%?)?);whd in ⊢ (??%?);
    820 whd in ⊢ (??(?%)?);lapply (eqZb_to_Prop b' b);
    821 cases (eqZb b' b);normalize;//;
     846whd in ⊢ (??(?%)?); @eq_block_elim #E
     847normalize;//;
    822848qed.
    823849
    824850lemma region_store:
    825   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    826   ∀b'. block_space m2 b' = block_space m1 b'.
    827 #chunk #m1 #psp #b #ofs #v #m2 #STORE
    828 #b' cases (store_inv … STORE);
    829 #Hvalid #H
    830 >H
    831 whd in ⊢ (??(?%?)?);whd in ⊢ (??%?);
    832 whd in ⊢ (??(?%)?);lapply (eqZb_to_Prop b' b);
    833 cases (eqZb b' b);normalize;//;
     851  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     852  ∀b'. block_region m2 b' = block_region m1 b'.
     853#chunk #m1 #r #b #ofs #v #m2 #STORE
     854* #r #b' //
    834855qed.
    835856
    836857lemma store_valid_block_1:
    837   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     858  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    838859  ∀b'. valid_block m1 b' → valid_block m2 b'.
    839 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     860#chunk #m1 #r #b #ofs #v #m2 #STORE
    840861#b' whd in ⊢ (% → %);#Hv
    841862>(nextblock_store … STORE) //;
     
    843864
    844865lemma store_valid_block_2:
    845   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     866  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    846867  ∀b'. valid_block m2 b' → valid_block m1 b'.
    847 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     868#chunk #m1 #r #b #ofs #v #m2 #STORE
    848869#b' whd in ⊢ (%→%);
    849870>(nextblock_store … STORE) //;
     
    853874
    854875lemma store_valid_access_1:
    855   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    856   ∀chunk',psp',b',ofs'.
    857   valid_access m1 chunk' psp' b' ofs' → valid_access m2 chunk' psp' b' ofs'.
    858 #chunk #m1 #psp #b #ofs #v #m2 #STORE
    859 #chunk' #psp' #b' #ofs'
     876  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     877  ∀chunk',r',b',ofs'.
     878  valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'.
     879#chunk #m1 #r #b #ofs #v #m2 #STORE
     880#chunk' #r' #b' #ofs'
    860881* Hv;
    861882#Hvb #Hl #Hr #Halign #Hptr
     
    868889
    869890lemma store_valid_access_2:
    870   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    871   ∀chunk',psp',b',ofs'.
    872   valid_access m2 chunk' psp' b' ofs' → valid_access m1 chunk' psp' b' ofs'.
    873 #chunk #m1 #psp #b #ofs #v #m2 #STORE
    874 #chunk' #psp' #b' #ofs'
     891  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     892  ∀chunk',r',b',ofs'.
     893  valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'.
     894#chunk #m1 #r #b #ofs #v #m2 #STORE
     895#chunk' #r' #b' #ofs'
    875896* Hv;
    876897#Hvb #Hl #Hr #Halign #Hcompat
     
    883904
    884905lemma store_valid_access_3:
    885   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    886   valid_access m1 chunk psp b ofs.
    887 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     906  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     907  valid_access m1 chunk r b ofs.
     908#chunk #m1 #r #b #ofs #v #m2 #STORE
    888909cases (store_inv … STORE);//;
    889910qed.
     
    893914
    894915lemma load_compat_pointer:
    895   ∀chunk,m,psp,psp',b,ofs,v.
    896   pointer_compat (block_space m b) psp' →
    897   load chunk m psp b ofs = Some ? v →
    898   load chunk m psp' b ofs = Some ? v.
    899 #chunk #m #psp #psp' #b #ofs #v #Hcompat #LOAD
     916  ∀chunk,m,r,r',b,ofs,v.
     917  pointer_compat (block_region m b) r' →
     918  load chunk m r b ofs = Some ? v →
     919  load chunk m r' b ofs = Some ? v.
     920#chunk #m #r #r' #b #ofs #v #Hcompat #LOAD
    900921lapply (load_valid_access … LOAD); #Hvalid
    901 cut (valid_access m chunk psp' b ofs);
     922cut (valid_access m chunk r' b ofs);
    902923[ % elim Hvalid; //;
    903924| #Hvalid'
     
    910931(* Nonessential properties that may require arithmetic
    911932theorem load_store_similar:
    912   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     933  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    913934  ∀chunk'.
    914935  size_chunk chunk' = size_chunk chunk →
    915   load chunk' m2 psp b ofs = Some ? (load_result chunk' v).
    916 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     936  load chunk' m2 r b ofs = Some ? (load_result chunk' v).
     937#chunk #m1 #r #b #ofs #v #m2 #STORE
    917938#chunk' #Hsize cases (store_inv … STORE);
    918939#Hv #Heq
    919940whd in ⊢ (??%?);
    920 nrewrite > (in_bounds_true m2 chunk' psp b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
     941nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
    921942               (None ?) ?);
    922943[>Heq
     
    934955
    935956theorem load_store_same:
    936   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    937   load chunk m2 psp b ofs = Some ? (load_result chunk v).
    938 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     957  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     958  load chunk m2 r b ofs = Some ? (load_result chunk v).
     959#chunk #m1 #r #b #ofs #v #m2 #STORE
    939960@load_store_similar //;
    940961qed.
    941962       
    942963theorem load_store_other:
    943   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    944   ∀chunk',psp',b',ofs'.
     964  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     965  ∀chunk',r',b',ofs'.
    945966  b' ≠ b
    946967  ∨ ofs' + size_chunk chunk' ≤  ofs
    947968  ∨ ofs + size_chunk chunk ≤ ofs' →
    948   load chunk' m2 psp' b' ofs' = load chunk' m1 psp' b' ofs'.
    949 #chunk #m1 #psp #b #ofs #v #m2 #STORE
    950 #chunk' #psp' #b' #ofs' #H
     969  load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'.
     970#chunk #m1 #r #b #ofs #v #m2 #STORE
     971#chunk' #r' #b' #ofs' #H
    951972cases (store_inv … STORE);
    952973#Hvalid #Heq whd in ⊢ (??%%);
    953 cases (in_bounds m1 chunk' psp' b' ofs');
    954 [#Hvalid1 >(in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??)
     974cases (in_bounds m1 chunk' r' b' ofs');
     975[#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??)
    955976   [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk'))
    956977      >Heq whd in ⊢ (??(???(? (? % ?)))?);
     
    968989      |#Hneq @ ]
    969990   |@(store_valid_access_1 … STORE) //]
    970 |whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' psp' b' ofs');
     991|whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs');
    971992   #H1 cases H1;
    972993   [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse
     
    978999
    9791000theorem load_store_overlap:
    980   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    981   ∀chunk',ofs',v'. load chunk' m2 psp b ofs' = Some ? v' →
     1001  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     1002  ∀chunk',ofs',v'. load chunk' m2 r b ofs' = Some ? v' →
    9821003  ofs' ≠ ofs →
    9831004  ofs < ofs' + size_chunk chunk' →
    9841005  ofs' < ofs + size_chunk chunk →
    9851006  v' = Vundef.
    986 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     1007#chunk #m1 #r #b #ofs #v #m2 #STORE
    9871008#chunk' #ofs' #v' #H
    9881009#H1 #H2 #H3
     
    10001021
    10011022theorem load_store_overlap':
    1002   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1023  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    10031024  ∀chunk',ofs'.
    1004   valid_access m1 chunk' psp b ofs' →
     1025  valid_access m1 chunk' r b ofs' →
    10051026  ofs' ≠ ofs →
    10061027  ofs < ofs' + size_chunk chunk' →
    10071028  ofs' < ofs + size_chunk chunk →
    1008   load chunk' m2 psp b ofs' = Some ? Vundef.
    1009 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     1029  load chunk' m2 r b ofs' = Some ? Vundef.
     1030#chunk #m1 #r #b #ofs #v #m2 #STORE
    10101031#chunk' #ofs' #Hvalid #H #H1 #H2
    1011 cut (∃v'.load chunk' m2 psp b ofs' = Some ? v')
     1032cut (∃v'.load chunk' m2 r b ofs' = Some ? v')
    10121033[@valid_access_load
    10131034   @(store_valid_access_1 … STORE) //
     
    10181039
    10191040theorem load_store_mismatch:
    1020   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1041  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    10211042  ∀chunk',v'.
    1022   load chunk' m2 psp b ofs = Some ? v' →
     1043  load chunk' m2 r b ofs = Some ? v' →
    10231044  size_chunk chunk' ≠ size_chunk chunk →
    10241045  v' = Vundef.
    1025 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     1046#chunk #m1 #r #b #ofs #v #m2 #STORE
    10261047#chunk' #v' #H #H1
    10271048cases (store_inv … STORE);
     
    10391060
    10401061theorem load_store_mismatch':
    1041   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1062  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
    10421063  ∀chunk'.
    1043   valid_access m1 chunk' psp b ofs →
     1064  valid_access m1 chunk' r b ofs →
    10441065  size_chunk chunk' ≠ size_chunk chunk →
    1045   load chunk' m2 psp b ofs = Some ? Vundef.
    1046 #chunk #m1 #psp #b #ofs #v #m2 #STORE
     1066  load chunk' m2 r b ofs = Some ? Vundef.
     1067#chunk #m1 #r #b #ofs #v #m2 #STORE
    10471068#chunk' #Hvalid #Hsize
    1048 cut (∃v'.load chunk' m2 psp b ofs = Some ? v')
     1069cut (∃v'.load chunk' m2 r b ofs = Some ? v')
    10491070[@(valid_access_load …)
    10501071   napply
     
    11011122
    11021123theorem load_store_characterization:
    1103   ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    1104   ∀chunk',psp',b',ofs'.
    1105   valid_access m1 chunk' psp' b' ofs' →
    1106   load chunk' m2 psp' b' ofs' =
     1124  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
     1125  ∀chunk',r',b',ofs'.
     1126  valid_access m1 chunk' r' b' ofs' →
     1127  load chunk' m2 r' b' ofs' =
    11071128    match load_store_classification chunk b ofs chunk' b' ofs' with
    11081129    [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v)
    1109     | lsc_other _ ⇒ load chunk' m1 psp' b' ofs'
     1130    | lsc_other _ ⇒ load chunk' m1 r' b' ofs'
    11101131    | lsc_overlap _ _ _ _ ⇒ Some ? Vundef
    11111132    | lsc_mismatch _ _ _ ⇒ Some ? Vundef ].
    1112 #chunk #m1 #psp #b #ofs #v #m2 #STORE
    1113 #chunk' #psp' #b' #ofs' #Hvalid
    1114 cut (∃v'. load chunk' m2 psp' b' ofs' = Some ? v')
     1133#chunk #m1 #r #b #ofs #v #m2 #STORE
     1134#chunk' #r' #b' #ofs' #Hvalid
     1135cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v')
    11151136[@valid_access_load
    11161137   @(store_valid_access_1 … STORE … Hvalid)
     
    11181139   cases (load_store_classification chunk b ofs chunk' b' ofs')
    11191140   [#H1 #H2 #H3 whd in ⊢ (???%);<H1 <H2
    1120       @(load_compat_pointer … psp)
     1141      @(load_compat_pointer … r)
    11211142      [ >(region_store … STORE b)
    11221143          cases Hvalid; //;
     
    11291150         |#H2 % %{2} //]
    11301151      |#H2 %{2} //]
    1131    |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … psp … Hx);
     1152   |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx);
    11321153     [ >(region_store … STORE b')
    11331154         >H1 elim (store_valid_access_3 … STORE); //
     
    11371158     ]
    11381159   |#H1 #H2 #H3
    1139        lapply (load_compat_pointer … psp … Hx);
     1160       lapply (load_compat_pointer … r … Hx);
    11401161       [ >(region_store … STORE b')
    11411162           >H1 elim (store_valid_access_3 … STORE); //
     
    12981319lemma class_alloc:
    12991320  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1300   ∀b'.block_space m2 b' = if eqZb b' b then bcl else block_space m1 b'.
     1321  ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'.
    13011322#m1 #lo #hi #bcl #m2 #b #ALLOC
    13021323whd in ALLOC:(??%%); destruct; #b'
     
    13061327lemma class_alloc_same:
    13071328  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1308   block_space m2 b = bcl.
     1329  block_region m2 b = bcl.
    13091330#m1 #lo #hi #bcl #m2 #b #ALLOC
    13101331whd in ALLOC:(??%%); destruct;
     
    13141335lemma class_alloc_other:
    13151336  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1316   ∀b'. valid_block m1 b' → block_space m2 b' = block_space m1 b'.
     1337  ∀b'. valid_block m1 b' → block_region m2 b' = block_region m1 b'.
    13171338#m1 #lo #hi #bcl #m2 #b #ALLOC
    13181339#b' >(class_alloc … ALLOC b')
     
    13251346lemma valid_access_alloc_other:
    13261347  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1327   ∀chunk,psp,b',ofs.
    1328   valid_access m1 chunk psp b' ofs →
    1329   valid_access m2 chunk psp b' ofs.
     1348  ∀chunk,r,b',ofs.
     1349  valid_access m1 chunk r b' ofs →
     1350  valid_access m2 chunk r b' ofs.
    13301351#m1 #lo #hi #bcl #m2 #b #ALLOC
    1331 #chunk #psp #b' #ofs #H
     1352#chunk #r #b' #ofs #H
    13321353cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat
    13331354%
     
    13411362lemma valid_access_alloc_same:
    13421363  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1343   ∀chunk,psp,ofs.
     1364  ∀chunk,r,ofs.
    13441365  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1345   pointer_compat bcl psp
    1346   valid_access m2 chunk psp b ofs.
     1366  pointer_compat bcl r
     1367  valid_access m2 chunk r b ofs.
    13471368#m1 #lo #hi #bcl #m2 #b #ALLOC
    1348 #chunk #psp #ofs #Hlo #Hhi #Halign #Hcompat
     1369#chunk #r #ofs #Hlo #Hhi #Halign #Hcompat
    13491370%
    13501371[ napply (valid_new_block … ALLOC)
     
    13611382lemma valid_access_alloc_inv:
    13621383  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1363   ∀chunk,psp,b',ofs.
    1364   valid_access m2 chunk psp b' ofs →
    1365   valid_access m1 chunk psp b' ofs ∨
    1366   (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl psp)).
     1384  ∀chunk,r,b',ofs.
     1385  valid_access m2 chunk r b' ofs →
     1386  valid_access m1 chunk r b' ofs ∨
     1387  (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl r)).
    13671388#m1 #lo #hi #bcl #m2 #b #ALLOC
    1368 #chunk #psp #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct
     1389#chunk #r #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct
    13691390elim (valid_block_alloc_inv … ALLOC ? Hblk);#H
    13701391[ <H in ALLOC ⊢ % #ALLOC'
     
    13821403theorem load_alloc_unchanged:
    13831404  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
    1384   ∀chunk,psp,b',ofs.
     1405  ∀chunk,r,b',ofs.
    13851406  valid_block m1 b' →
    1386   load chunk m2 psp b' ofs = load chunk m1 psp b' ofs.
     1407  load chunk m2 r b' ofs = load chunk m1 r b' ofs.
    13871408#m1 #lo #hi #bcl #m2 #b #ALLOC
    1388 #chunk #psp #b' #ofs #H whd in ⊢ (??%%);
    1389 cases (in_bounds m2 chunk psp b' ofs); #H'
     1409#chunk #r #b' #ofs #H whd in ⊢ (??%%);
     1410cases (in_bounds m2 chunk r b' ofs); #H'
    13901411[ elim (valid_access_alloc_inv … ALLOC ???? H');
    13911412  [ #H'' (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
     
    14001421      @False_ind @(absurd ? H) napply (fresh_block_alloc … ALLOC)
    14011422  ]
    1402 | cases (in_bounds m1 chunk psp b' ofs); #H'' whd in ⊢ (??%%); //;
     1423| cases (in_bounds m1 chunk r b' ofs); #H'' whd in ⊢ (??%%); //;
    14031424    @False_ind @(absurd ? ? H') @(valid_access_alloc_other … ALLOC) //
    14041425] qed.
     
    14061427theorem load_alloc_other:
    14071428  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1408   ∀chunk,psp,b',ofs,v.
    1409   load chunk m1 psp b' ofs = Some ? v →
    1410   load chunk m2 psp b' ofs = Some ? v.
     1429  ∀chunk,r,b',ofs,v.
     1430  load chunk m1 r b' ofs = Some ? v →
     1431  load chunk m2 r b' ofs = Some ? v.
    14111432#m1 #lo #hi #bcl #m2 #b #ALLOC
    1412 #chunk #psp #b' #ofs #v #H
     1433#chunk #r #b' #ofs #v #H
    14131434<H @(load_alloc_unchanged … ALLOC ???) cases (load_valid_access … H); //;
    14141435qed.
     
    14161437theorem load_alloc_same:
    14171438  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1418   ∀chunk,psp,ofs,v.
    1419   load chunk m2 psp b ofs = Some ? v →
     1439  ∀chunk,r,ofs,v.
     1440  load chunk m2 r b ofs = Some ? v →
    14201441  v = Vundef.
    14211442#m1 #lo #hi #bcl #m2 #b #ALLOC
    1422 #chunk #psp #ofs #v #H
     1443#chunk #r #ofs #v #H
    14231444elim (load_inv … H); #H0 #H1 >H1
    14241445 whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC)
     
    14311452theorem load_alloc_same':
    14321453  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1433   ∀chunk,psp,ofs.
     1454  ∀chunk,r,ofs.
    14341455  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1435   pointer_compat bcl psp
    1436   load chunk m2 psp b ofs = Some ? Vundef.
     1456  pointer_compat bcl r
     1457  load chunk m2 r b ofs = Some ? Vundef.
    14371458#m1 #lo #hi #bcl #m2 #b #ALLOC
    1438 #chunk #psp #ofs #Hlo #Hhi #Hal #Hct
    1439 cut (∃v. load chunk m2 psp b ofs = Some ? v);
     1459#chunk #r #ofs #Hlo #Hhi #Hal #Hct
     1460cut (∃v. load chunk m2 r b ofs = Some ? v);
    14401461[ @valid_access_load % //;
    14411462  [ @(valid_new_block … ALLOC)
     
    15041525
    15051526lemma class_free:
    1506   ∀m,bf,b. b ≠ bf → block_space (free m bf) b = block_space m b.
     1527  ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b.
    15071528#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
    15081529>(update_o block_contents …) //; @sym_neq //;
     
    15101531
    15111532lemma valid_access_free_1:
    1512   ∀m,bf,chunk,psp,b,ofs.
    1513   valid_access m chunk psp b ofs → b ≠ bf →
    1514   valid_access (free m bf) chunk psp b ofs.
    1515 #m #bf #chunk #psp #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq
     1533  ∀m,bf,chunk,r,b,ofs.
     1534  valid_access m chunk r b ofs → b ≠ bf →
     1535  valid_access (free m bf) chunk r b ofs.
     1536#m #bf #chunk #r #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq
    15161537% //;
    15171538[ @valid_block_free_1 //
     
    15221543
    15231544lemma valid_access_free_2:
    1524   ∀m,psp,bf,chunk,ofs. ¬(valid_access (free m bf) chunk psp bf ofs).
    1525 #m #psp #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct
     1545  ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs).
     1546#m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct
    15261547whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo
    15271548whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi
     
    15341555
    15351556lemma valid_access_free_inv:
    1536   ∀m,bf,chunk,psp,b,ofs.
    1537   valid_access (free m bf) chunk psp b ofs →
    1538   valid_access m chunk psp b ofs ∧ b ≠ bf.
    1539 #m #bf #chunk #psp #b #ofs elim (decidable_eq_Z_Type b bf);
     1557  ∀m,bf,chunk,r,b,ofs.
     1558  valid_access (free m bf) chunk r b ofs →
     1559  valid_access m chunk r b ofs ∧ b ≠ bf.
     1560#m #bf #chunk #r #b #ofs elim (decidable_eq_Z_Type b bf);
    15401561[ #e >e
    15411562    #H @False_ind @(absurd ? H (valid_access_free_2 …))
     
    15481569
    15491570theorem load_free:
    1550   ∀m,bf,chunk,psp,b,ofs.
     1571  ∀m,bf,chunk,r,b,ofs.
    15511572  b ≠ bf →
    1552   load chunk (free m bf) psp b ofs = load chunk m psp b ofs.
    1553 #m #bf #chunk #psp #b #ofs #ne whd in ⊢ (??%%);
    1554 elim (in_bounds m chunk psp b ofs);
     1573  load chunk (free m bf) r b ofs = load chunk m r b ofs.
     1574#m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%);
     1575elim (in_bounds m chunk r b ofs);
    15551576[ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???)
    15561577  [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //;
     
    15581579  | @valid_access_free_1 //; @ne
    15591580  ]
    1560 | elim (in_bounds (free m bf) chunk psp b ofs); (* XXX just // used to work *) [ 2: normalize; //; ]
     1581| elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ]
    15611582    #H #H' @False_ind @(absurd ? ? H')
    15621583    elim (valid_access_free_inv …H); //;
     
    15861607
    15871608lemma valid_access_free_list:
    1588   ∀chunk,psp,b,ofs,m,bl.
    1589   valid_access m chunk psp b ofs → ¬in_list ? b bl →
    1590   valid_access (free_list m bl) chunk psp b ofs.
    1591 #chunk #psp #b #ofs #m #bl elim bl;
     1609  ∀chunk,r,b,ofs,m,bl.
     1610  valid_access m chunk r b ofs → ¬in_list ? b bl →
     1611  valid_access (free_list m bl) chunk r b ofs.
     1612#chunk #r #b #ofs #m #bl elim bl;
    15921613[ whd in ⊢ (?→?→(?%????)); //
    15931614| #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1
     
    15971618
    15981619lemma valid_access_free_list_inv:
    1599   ∀chunk,psp,b,ofs,m,bl.
    1600   valid_access (free_list m bl) chunk psp b ofs →
    1601   ¬in_list ? b bl ∧ valid_access m chunk psp b ofs.
    1602 #chunk #psp #b #ofs #m #bl elim bl;
     1620  ∀chunk,r,b,ofs,m,bl.
     1621  valid_access (free_list m bl) chunk r b ofs →
     1622  ¬in_list ? b bl ∧ valid_access m chunk r b ofs.
     1623#chunk #r #b #ofs #m #bl elim bl;
    16031624[ whd in ⊢ ((?%????)→?); #H % //
    16041625| #h #t #IH >(unfold_free_list m h t) #H
     
    16121633
    16131634lemma valid_pointer_valid_access:
    1614   ∀m,psp,b,ofs.
    1615   valid_pointer m psp b ofs = true ↔ valid_access m Mint8unsigned psp b ofs.
    1616 #m #psp #b #ofs whd in ⊢ (?(??%?)?); %
     1635  ∀m,r,b,ofs.
     1636  valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs.
     1637#m #r #b #ofs whd in ⊢ (?(??%?)?); %
    16171638[ #H
    16181639    lapply (andb_true_l … H); #H'
     
    16271648    | whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    16281649    | cases ofs; /2/;
    1629     | whd in H4:(??%?); elim (pointer_compat_dec (block_space m b) psp) in H4;
     1650    | whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4;
    16301651        [ //; | #Hn #e whd in e:(??%%); destruct ]
    16311652    ]
     
    16341655    >(Zle_to_Zleb_true … Hlo)
    16351656    whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?)
    1636     [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_space m b) psp);
     1657    [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r);
    16371658      [ //;
    16381659      | #Hct' @False_ind @(absurd … Hct Hct')
     
    16441665
    16451666theorem valid_pointer_alloc:
    1646   ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,psp. ∀b,b': block. ∀ofs: Z.
     1667  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z.
    16471668  alloc m1 lo hi bcl = 〈m2, b'〉 →
    1648   valid_pointer m1 psp b ofs = true →
    1649   valid_pointer m2 psp b ofs = true.
    1650 #m1 #m2 #lo #hi #bcl #psp #b #b' #ofs #ALLOC #VALID
     1669  valid_pointer m1 r b ofs = true →
     1670  valid_pointer m2 r b ofs = true.
     1671#m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID
    16511672lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
    16521673@(proj2 ?? (valid_pointer_valid_access ????))
     
    16561677theorem valid_pointer_store:
    16571678  ∀chunk: memory_chunk. ∀m1,m2: mem.
    1658   ∀psp,psp': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
    1659   store chunk m1 psp' b' ofs' v = Some ? m2 →
    1660   valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
    1661 #chunk #m1 #m2 #psp #psp' #b #b' #ofs #ofs' #v #STORE #VALID
     1679  ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
     1680  store chunk m1 r' b' ofs' v = Some ? m2 →
     1681  valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
     1682#chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID
    16621683lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
    16631684@(proj2 ?? (valid_pointer_valid_access ????))
     
    17151736(*
    17161737lemma store_unmapped_inj: ∀val_inj.
    1717   ∀mi,m1,m2,psp,b,ofs,v,chunk,m1'.
     1738  ∀mi,m1,m2,r,b,ofs,v,chunk,m1'.
    17181739  mem_inj val_inj mi m1 m2 →
    17191740  mi b = None ? →
    1720   store chunk m1 psp b ofs v = Some ? m1' →
     1741  store chunk m1 r b ofs v = Some ? m1' →
    17211742  mem_inj val_inj mi m1' m2.
    17221743#val_inj
    1723 #mi #m1 #m2 #psp #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore
     1744#mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore
    17241745whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
    17251746cut (load chunk0 m1 b1 ofs0 = Some ? v1);
     
    17301751
    17311752lemma store_outside_inj: ∀val_inj.
    1732   ∀mi,m1,m2,chunk,psp,b,ofs,v,m2'.
     1753  ∀mi,m1,m2,chunk,r,b,ofs,v,m2'.
    17331754  mem_inj val_inj mi m1 m2 →
    17341755  (∀b',delta.
     
    17361757    high_bound m1 b' + delta ≤ ofs
    17371758    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
    1738   store chunk m2 psp b ofs v = Some ? m2' →
     1759  store chunk m2 r b ofs v = Some ? m2' →
    17391760  mem_inj val_inj mi m1 m2'.
    17401761#val_inj
    1741 #mi #m1 #m2 #chunk #psp #b #ofs #v #m2' #Hinj #Hbounds #Hstore
     1762#mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore
    17421763whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
    17431764lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ
     
    21122133  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
    21132134  extends m1 m2 →
    2114   load chunk m1 psp b ofs = Some ? v →
    2115   load chunk m2 psp b ofs = Some ? v.
    2116 #chunk #m1 #m2 #psp #b #ofs #v
     2135  load chunk m1 r b ofs = Some ? v →
     2136  load chunk m2 r b ofs = Some ? v.
     2137#chunk #m1 #m2 #r #b #ofs #v
    21172138*;#Hnext #Hinj #LOAD
    21182139lapply (Hinj … LOAD); [ normalize; // | 2,3: ]
     
    21242145  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
    21252146  extends m1 m2 →
    2126   store chunk m1 psp b ofs v = Some ? m1' →
    2127   ∃m2'. store chunk m2 psp b ofs v = Some ? m2' ∧ extends m1' m2'.
     2147  store chunk m1 r b ofs v = Some ? m1' →
     2148  ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'.
    21282149#chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1
    21292150lapply (store_mapped_inj … Hinj ?? STORE1 ?);
     
    21472168  extends m1 m2 →
    21482169  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
    2149   store chunk m2 psp b ofs v = Some ? m2' →
     2170  store chunk m2 r b ofs v = Some ? m2' →
    21502171  extends m1 m2'.
    21512172#chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE %
     
    21612182theorem valid_pointer_extends:
    21622183  ∀m1,m2,b,ofs.
    2163   extends m1 m2 → valid_pointer m1 psp b ofs = true →
    2164   valid_pointer m2 psp b ofs = true.
     2184  extends m1 m2 → valid_pointer m1 r b ofs = true →
     2185  valid_pointer m2 r b ofs = true.
    21652186#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
    21662187<(Zplus_z_OZ ofs)
     
    21922213lemma load_lessdef:
    21932214  ∀m1,m2,chunk,b,ofs,v1.
    2194   lessdef m1 m2 → load chunk m1 psp b ofs = Some ? v1 →
    2195   ∃v2. load chunk m2 psp b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
     2215  lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 →
     2216  ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
    21962217#m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0
    21972218lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); // | 2,3:##skip ]
     
    22172238  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
    22182239  lessdef m1 m2 → Val_lessdef v1 v2 →
    2219   store chunk m1 psp b ofs v1 = Some ? m1' →
    2220   ∃m2'. store chunk m2 psp b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
     2240  store chunk m1 r b ofs v1 = Some ? m1' →
     2241  ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
    22212242#m1 #m2 #chunk #b #ofs #v1 #v2 #m1'
    22222243*;#Hnext #Hinj #Hvless #STORE0
     
    23092330lemma valid_pointer_lessdef:
    23102331  ∀m1,m2,b,ofs.
    2311   lessdef m1 m2 → valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
     2332  lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
    23122333#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
    23132334<(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //;
     
    24462467  mem_inject f m1 m2 →
    24472468  valid_pointer m1 b (signed ofs) = true →
    2448   val_inject f (Vptr psp b ofs) (Vptr b' ofs') →
     2469  val_inject f (Vptr r b ofs) (Vptr b' ofs') →
    24492470  valid_pointer m2 b' (signed ofs') = true.
    24502471#f #m1 #m2 #b #ofs #b' #ofs'
     
    34943515
    34953516lemma in_bounds_equiv:
    3496   ∀chunk1,chunk2,m,psp,b,ofs.∀A:Type[0].∀a1,a2: A.
     3517  ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A.
    34973518  size_chunk chunk1 = size_chunk chunk2 →
    3498   (match in_bounds m chunk1 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
    3499   (match in_bounds m chunk2 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
    3500 #chunk1 #chunk2 #m #psp #b #ofs #A #a1 #a2 #Hsize
    3501 elim (in_bounds m chunk1 psp b ofs);
     3519  (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
     3520  (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
     3521#chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize
     3522elim (in_bounds m chunk1 r b ofs);
    35023523[ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //;
    35033524    @valid_access_compat //;
    3504 | #H whd in ⊢ (??%?); elim (in_bounds m chunk2 psp b ofs); //;
     3525| #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //;
    35053526    #H' @False_ind @(absurd ?? H)
    35063527    @valid_access_compat //;
     
    35113532  storev Mint8signed m a v = storev Mint8unsigned m a v.
    35123533#m #a #v whd in ⊢ (??%%); elim a; //;
    3513 #psp #b #ofs whd in ⊢ (??%%);
     3534#r #b #ofs whd in ⊢ (??%%);
    35143535>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //;
    35153536qed.
     
    35193540  storev Mint16signed m a v = storev Mint16unsigned m a v.
    35203541#m #a #v whd in ⊢ (??%%); elim a; //;
    3521 #psp #b #ofs whd in ⊢ (??%%);
     3542#r #b #ofs whd in ⊢ (??%%);
    35223543>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //;
    35233544qed.
     
    35333554  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
    35343555#m #a whd in ⊢ (??%(????(%))); elim a; //;
    3535 #psp #b #ofs whd in ⊢ (??%(????%));
     3556#r #b #ofs whd in ⊢ (??%(????%));
    35363557>(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //;
    3537 elim (in_bounds m Mint8unsigned psp b (signed ofs)); /2/;
     3558elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/;
    35383559#H whd in ⊢ (??%%);
    35393560elim (getN 0 (signed ofs) (contents (blocks m b)));
Note: See TracChangeset for help on using the changeset viewer.