Changeset 125 for C-semantics/Mem.ma


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (9 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r124 r125  
    3333include "Coqlib.ma".
    3434include "Values.ma".
     35include "AST.ma".
    3536include "extralib.ma".
    3637
     
    8384  plus a mapping from byte offsets to contents.  *)
    8485
    85 ninductive block_class : Type ≝
    86 | UnspecifiedB : block_class
    87 | DataB : block_class
    88 | IDataB : block_class
    89 | XDataB : block_class
    90 | CodeB : block_class.
    91 
    9286(* XXX: mkblock *)
    9387nrecord block_contents : Type[0] ≝ {
     
    9589  high: Z;
    9690  contents: contentmap;
    97   class: block_class
     91  space: memory_space
    9892}.
    9993
     
    192186nqed.
    193187
    194 ndefinition empty_block : Z → Z → block_class → block_contents ≝
     188ndefinition empty_block : Z → Z → memory_space → block_contents ≝
    195189  λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.
    196190
    197191ndefinition empty: mem ≝
    198   mk_mem (λx.empty_block OZ OZ UnspecifiedB) (pos one) one_pos.
     192  mk_mem (λx.empty_block OZ OZ Any) (pos one) one_pos.
    199193
    200194ndefinition nullptr: block ≝ OZ.
     
    212206nqed.
    213207
    214 ndefinition alloc : mem → Z → Z → block_class → mem × block ≝
     208ndefinition alloc : mem → Z → Z → memory_space → mem × block ≝
    215209  λm,lo,hi,bty.〈mk_mem
    216210              (update … (nextblock m)
     
    229223ndefinition free ≝
    230224  λm,b.mk_mem (update … b
    231                 (empty_block OZ OZ UnspecifiedB)
     225                (empty_block OZ OZ Any)
    232226                (blocks m))
    233227        (nextblock m)
     
    249243ndefinition high_bound : mem → block → Z ≝
    250244  λm,b.high (blocks m b).
    251 ndefinition blockclass: mem → block → block_class
    252   λm,b.class (blocks m b).
     245ndefinition block_space: mem → block → memory_space
     246  λm,b.space (blocks m b).
    253247
    254248(* A block address is valid if it was previously allocated. It remains valid
     
    560554nqed.
    561555
    562 ninductive class_compat : block_class → ptr_class → Prop ≝
    563 |  data_compat : class_compat  DataB  Data
    564 | idata_compat : class_compat IDataB IData
    565 | xdata_compat : class_compat XDataB XData
    566 |  code_compat : class_compat  CodeB  Code
    567 | unspecified_compat : ∀p. class_compat UnspecifiedB p
    568 | universal_compat : ∀b. class_compat b Universal.
    569 
    570 nlemma class_compat_dec : ∀b,p. class_compat b p + ¬class_compat b p.
     556(* pointer_compat block_space pointer_space *)
     557
     558ninductive pointer_compat : memory_space → memory_space → Prop ≝
     559|  data_compat : pointer_compat  Data  Data
     560| idata_compat : pointer_compat IData IData
     561| xdata_compat : pointer_compat XData XData
     562|  code_compat : pointer_compat  Code  Code
     563| unspecified_compat : ∀p. pointer_compat Any p
     564| universal_compat : ∀b. pointer_compat b Any.
     565
     566nlemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
    571567#b p; ncases b;
    572568##[ ##1: @1; //;
     
    574570##] nqed.
    575571
    576 ndefinition is_class_compat : block_class → ptr_class → bool ≝
    577 λb,p. match class_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    578 
    579 (* [valid_access m chunk pcl b ofs] holds if a memory access (load or store)
     572ndefinition is_pointer_compat : memory_space → memory_space → bool ≝
     573λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
     574
     575(* [valid_access m chunk psp b ofs] holds if a memory access (load or store)
    580576    of the given chunk is possible in [m] at address [b, ofs].
    581577    This means:
     
    583579- The range of bytes accessed is within the bounds of [b].
    584580- The offset [ofs] is aligned.
    585 - The pointer classs [pcl] is compatible with the class of [b].
     581- The pointer classs [psp] is compatible with the class of [b].
    586582*)
    587583
    588 ninductive valid_access (m: mem) (chunk: memory_chunk) (pcl: ptr_class) (b: block) (ofs: Z)
     584ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: memory_space) (b: block) (ofs: Z)
    589585            : Prop ≝
    590586  | valid_access_intro:
     
    593589      ofs + size_chunk chunk ≤ high_bound m b →
    594590      (align_chunk chunk ∣ ofs) →
    595       class_compat (blockclass m b) pcl
    596       valid_access m chunk pcl b ofs.
     591      pointer_compat (block_space m b) psp
     592      valid_access m chunk psp b ofs.
    597593
    598594(* The following function checks whether accessing the given memory chunk
     
    601597(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    602598nlet rec in_bounds
    603   (m:mem) (chunk:memory_chunk) (pcl:ptr_class) (b:block) (ofs:Z) on b : 
    604     Sum (valid_access m chunk pcl b ofs) (Not (valid_access m chunk pcl b ofs)) ≝ ?.
     599  (m:mem) (chunk:memory_chunk) (psp:memory_space) (b:block) (ofs:Z) on b : 
     600    Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?.
    605601napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
    606602##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo;
    607603    ##[ napply (Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)); #Hhi;
    608604        ##[ nelim (dec_dividesZ (align_chunk chunk) ofs); #Hal;
    609           ##[ ncases (class_compat_dec (blockclass m b) pcl); #Hcl;
     605          ##[ ncases (pointer_compat_dec (block_space m b) psp); #Hcl;
    610606            ##[ @1; @; // ##]
    611607          ##]
     
    617613
    618614nlemma in_bounds_true:
    619   ∀m,chunk,pcl,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
    620   valid_access m chunk pcl b ofs ->
    621   (match in_bounds m chunk pcl b ofs with
     615  ∀m,chunk,psp,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
     616  valid_access m chunk psp b ofs ->
     617  (match in_bounds m chunk psp b ofs with
    622618   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
    623 #m chunk pcl b ofs A a1 a2 H;
    624 ncases (in_bounds m chunk pcl b ofs);nnormalize;#H1;
     619#m chunk psp b ofs A a1 a2 H;
     620ncases (in_bounds m chunk psp b ofs);nnormalize;#H1;
    625621##[//
    626622##|nelim (?:False);napply (absurd ? H H1)]
     
    630626  given offset falls within the bounds of the corresponding block. *)
    631627
    632 ndefinition valid_pointer : mem → ptr_class → block → Z → bool ≝
    633 λm,pcl,b,ofs. Zltb b (nextblock m) ∧
     628ndefinition valid_pointer : mem → memory_space → block → Z → bool ≝
     629λm,psp,b,ofs. Zltb b (nextblock m) ∧
    634630  Zleb (low_bound m b) ofs ∧
    635631  Zltb ofs (high_bound m b) ∧
    636   is_class_compat (blockclass m b) pcl.
     632  is_pointer_compat (block_space m b) psp.
    637633
    638634(* [load chunk m b ofs] perform a read in memory state [m], at address
     
    640636  or the memory access is out of bounds. *)
    641637
    642 ndefinition load : memory_chunk → mem → ptr_class → block → Z → option val ≝
    643 λchunk,m,pcl,b,ofs.
    644   match in_bounds m chunk pcl b ofs with
     638ndefinition load : memory_chunk → mem → memory_space → block → Z → option val ≝
     639λchunk,m,psp,b,ofs.
     640  match in_bounds m chunk psp b ofs with
    645641  [ inl _ ⇒ Some ? (load_result chunk
    646642           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
     
    648644
    649645nlemma load_inv:
    650   ∀chunk,m,pcl,b,ofs,v.
    651   load chunk m pcl b ofs = Some ? v →
    652   valid_access m chunk pcl b ofs ∧
     646  ∀chunk,m,psp,b,ofs,v.
     647  load chunk m psp b ofs = Some ? v →
     648  valid_access m chunk psp b ofs ∧
    653649  v = load_result chunk
    654650           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
    655 #chunk m pcl b ofs v; nwhd in ⊢ (??%? → ?);
    656 ncases (in_bounds m chunk pcl b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;
     651#chunk m psp b ofs v; nwhd in ⊢ (??%? → ?);
     652ncases (in_bounds m chunk psp b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;
    657653##[ @;//; ndestruct; //;
    658654##| ndestruct
     
    665661nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    666662  match addr with
    667   [ Vptr pcl b ofs ⇒ load chunk m pcl b (signed ofs)
     663  [ Vptr psp b ofs ⇒ load chunk m psp b (signed ofs)
    668664  | _ ⇒ None ? ].
    669665
     
    677673    (update ? b
    678674        (mk_block_contents (low c) (high c)
    679                  (setN (pred_size_chunk chunk) ofs v (contents c)) (class c))
     675                 (setN (pred_size_chunk chunk) ofs v (contents c)) (space c))
    680676        (blocks m))
    681677    (nextblock m)
     
    687683  or the memory access is out of bounds. *)
    688684
    689 ndefinition store : memory_chunk → mem → ptr_class → block → Z → val → option mem ≝
    690 λchunk,m,pcl,b,ofs,v.
    691   match in_bounds m chunk pcl b ofs with
     685ndefinition store : memory_chunk → mem → memory_space → block → Z → val → option mem ≝
     686λchunk,m,psp,b,ofs,v.
     687  match in_bounds m chunk psp b ofs with
    692688  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
    693689  | inr _ ⇒ None ? ].
    694690
    695691nlemma store_inv:
    696   ∀chunk,m,pcl,b,ofs,v,m'.
    697   store chunk m pcl b ofs v = Some ? m' →
    698   valid_access m chunk pcl b ofs ∧
     692  ∀chunk,m,psp,b,ofs,v,m'.
     693  store chunk m psp b ofs v = Some ? m' →
     694  valid_access m chunk psp b ofs ∧
    699695  m' = unchecked_store chunk m b ofs v.
    700 #chunk m pcl b ofs v m'; nwhd in ⊢ (??%? → ?);
     696#chunk m psp b ofs v m'; nwhd in ⊢ (??%? → ?);
    701697(*9*)
    702 ncases (in_bounds m chunk pcl b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
     698ncases (in_bounds m chunk psp b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
    703699##[@; ##[//|ndestruct;//]
    704700##|ndestruct]
     
    711707λchunk,m,addr,v.
    712708  match addr with
    713   [ Vptr pcl b ofs ⇒ store chunk m pcl b (signed ofs) v
     709  [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v
    714710  | _ ⇒ None ? ].
    715711
     
    778774nqed.
    779775
    780 ndefinition block_init_data : list init_data → block_class → block_contents ≝
     776ndefinition block_init_data : list init_data → memory_space → block_contents ≝
    781777  λi_data,bcl.mk_block_contents
    782778    OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
    783779
    784 ndefinition alloc_init_data : mem → list init_data → block_class → mem × block ≝
     780ndefinition alloc_init_data : mem → list init_data → memory_space → mem × block ≝
    785781  λm,i_data,bcl.
    786782  〈mk_mem (update ? (nextblock m)
     
    807803
    808804nlemma valid_access_valid_block:
    809   ∀m,chunk,pcl,b,ofs. valid_access m chunk pcl b ofs → valid_block m b.
    810 #m;#chunk;#pcl;#b;#ofs;#H;
     805  ∀m,chunk,psp,b,ofs. valid_access m chunk psp b ofs → valid_block m b.
     806#m;#chunk;#psp;#b;#ofs;#H;
    811807nelim H;//;
    812808nqed.
    813809
    814810nlemma valid_access_aligned:
    815   ∀m,chunk,pcl,b,ofs.
    816   valid_access m chunk pcl b ofs → (align_chunk chunk ∣ ofs).
    817 #m;#chunk;#pcl;#b;#ofs;#H;
     811  ∀m,chunk,psp,b,ofs.
     812  valid_access m chunk psp b ofs → (align_chunk chunk ∣ ofs).
     813#m;#chunk;#psp;#b;#ofs;#H;
    818814nelim H;//;
    819815nqed.
    820816
    821817nlemma valid_access_compat:
    822   ∀m,chunk1,chunk2,pcl,b,ofs.
     818  ∀m,chunk1,chunk2,psp,b,ofs.
    823819  size_chunk chunk1 = size_chunk chunk2 →
    824   valid_access m chunk1 pcl b ofs →
    825   valid_access m chunk2 pcl b ofs.
    826 #m;#chunk;#chunk2;#pcl;#b;#ofs;#H1;#H2;
     820  valid_access m chunk1 psp b ofs →
     821  valid_access m chunk2 psp b ofs.
     822#m;#chunk;#chunk2;#psp;#b;#ofs;#H1;#H2;
    827823nelim H2;#H3;#H4;#H5;#H6;#H7;
    828824nrewrite > H1 in H5;#H5;
     
    836832
    837833ntheorem valid_access_load:
    838   ∀m,chunk,pcl,b,ofs.
    839   valid_access m chunk pcl b ofs →
    840   ∃v. load chunk m pcl b ofs = Some ? v.
    841 #m;#chunk;#pcl;#b;#ofs;#H;@;
     834  ∀m,chunk,psp,b,ofs.
     835  valid_access m chunk psp b ofs →
     836  ∃v. load chunk m psp b ofs = Some ? v.
     837#m;#chunk;#psp;#b;#ofs;#H;@;
    842838##[##2:nwhd in ⊢ (??%?);napply in_bounds_true;//;
    843839##|##skip]
     
    845841
    846842ntheorem load_valid_access:
    847   ∀m,chunk,pcl,b,ofs,v.
    848   load chunk m pcl b ofs = Some ? v →
    849   valid_access m chunk pcl b ofs.
    850 #m;#chunk;#pcl;#b;#ofs;#v;#H;
     843  ∀m,chunk,psp,b,ofs,v.
     844  load chunk m psp b ofs = Some ? v →
     845  valid_access m chunk psp b ofs.
     846#m;#chunk;#psp;#b;#ofs;#v;#H;
    851847ncases (load_inv … H);//;
    852848nqed.
     
    857853
    858854nlemma valid_access_store:
    859   ∀m1,chunk,pcl,b,ofs,v.
    860   valid_access m1 chunk pcl b ofs →
    861   ∃m2. store chunk m1 pcl b ofs v = Some ? m2.
    862 #m1;#chunk;#pcl;#b;#ofs;#v;#H;
     855  ∀m1,chunk,psp,b,ofs,v.
     856  valid_access m1 chunk psp b ofs →
     857  ∃m2. store chunk m1 psp b ofs v = Some ? m2.
     858#m1;#chunk;#psp;#b;#ofs;#v;#H;
    863859@;
    864860##[##2:napply in_bounds_true;//
     
    869865
    870866nlemma low_bound_store:
    871   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     867  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    872868  ∀b'.low_bound m2 b' = low_bound m1 b'.
    873 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     869#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    874870#b';ncases (store_inv … STORE);
    875871#H1;#H2;nrewrite > H2;
     
    880876
    881877nlemma nextblock_store :
    882   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     878  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    883879  nextblock m2 = nextblock m1.
    884 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     880#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    885881ncases (store_inv … STORE);
    886882#Hvalid;#Heq;
     
    889885
    890886nlemma high_bound_store:
    891   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     887  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    892888  ∀b'. high_bound m2 b' = high_bound m1 b'.
    893 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     889#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    894890#b';ncases (store_inv … STORE);
    895891#Hvalid;#H;
     
    900896nqed.
    901897
    902 nlemma block_class_store:
    903   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    904   ∀b'. blockclass m2 b' = blockclass m1 b'.
    905 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     898nlemma memory_space_store:
     899  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     900  ∀b'. block_space m2 b' = block_space m1 b'.
     901#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    906902#b';ncases (store_inv … STORE);
    907903#Hvalid;#H;
     
    913909
    914910nlemma store_valid_block_1:
    915   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     911  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    916912  ∀b'. valid_block m1 b' → valid_block m2 b'.
    917 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     913#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    918914#b';nwhd in ⊢ (% → %);#Hv;
    919915nrewrite > (nextblock_store … STORE);//;
     
    921917
    922918nlemma store_valid_block_2:
    923   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     919  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    924920  ∀b'. valid_block m2 b' → valid_block m1 b'.
    925 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     921#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    926922#b';nwhd in ⊢ (%→%);
    927923nrewrite > (nextblock_store … STORE);//;
     
    931927
    932928nlemma store_valid_access_1:
    933   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    934   ∀chunk',pcl',b',ofs'.
    935   valid_access m1 chunk' pcl' b' ofs' → valid_access m2 chunk' pcl' b' ofs'.
    936 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    937 #chunk';#pcl';#b';#ofs';
     929  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     930  ∀chunk',psp',b',ofs'.
     931  valid_access m1 chunk' psp' b' ofs' → valid_access m2 chunk' psp' b' ofs'.
     932#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
     933#chunk';#psp';#b';#ofs';
    938934* Hv;
    939935#Hvb;#Hl;#Hr;#Halign;#Hptr;
     
    942938##|nrewrite > (low_bound_store … STORE …);//
    943939##|nrewrite > (high_bound_store … STORE …);//
    944 ##|nrewrite > (block_class_store … STORE …);//]
     940##|nrewrite > (memory_space_store … STORE …);//]
    945941nqed.
    946942
    947943nlemma store_valid_access_2:
    948   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    949   ∀chunk',pcl',b',ofs'.
    950   valid_access m2 chunk' pcl' b' ofs' → valid_access m1 chunk' pcl' b' ofs'.
    951 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    952 #chunk';#pcl';#b';#ofs';
     944  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     945  ∀chunk',psp',b',ofs'.
     946  valid_access m2 chunk' psp' b' ofs' → valid_access m1 chunk' psp' b' ofs'.
     947#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
     948#chunk';#psp';#b';#ofs';
    953949* Hv;
    954950#Hvb;#Hl;#Hr;#Halign;#Hcompat;
     
    957953##|nrewrite < (low_bound_store … STORE …);//
    958954##|nrewrite < (high_bound_store … STORE …);//
    959 ##|nrewrite < (block_class_store … STORE …);//]
     955##|nrewrite < (memory_space_store … STORE …);//]
    960956nqed.
    961957
    962958nlemma store_valid_access_3:
    963   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    964   valid_access m1 chunk pcl b ofs.
    965 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     959  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     960  valid_access m1 chunk psp b ofs.
     961#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    966962ncases (store_inv … STORE);//;
    967963nqed.
     
    971967
    972968nlemma load_compat_pointer:
    973   ∀chunk,m,pcl,pcl',b,ofs,v.
    974   class_compat (blockclass m b) pcl' →
    975   load chunk m pcl b ofs = Some ? v →
    976   load chunk m pcl' b ofs = Some ? v.
    977 #chunk m pcl pcl' b ofs v Hcompat LOAD.
     969  ∀chunk,m,psp,psp',b,ofs,v.
     970  pointer_compat (block_space m b) psp' →
     971  load chunk m psp b ofs = Some ? v →
     972  load chunk m psp' b ofs = Some ? v.
     973#chunk m psp psp' b ofs v Hcompat LOAD.
    978974nlapply (load_valid_access … LOAD); #Hvalid;
    979 ncut (valid_access m chunk pcl' b ofs);
     975ncut (valid_access m chunk psp' b ofs);
    980976##[ @;nelim Hvalid; //;
    981977##| #Hvalid';
     
    987983
    988984ntheorem load_store_similar:
    989   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     985  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    990986  ∀chunk'.
    991987  size_chunk chunk' = size_chunk chunk →
    992   load chunk' m2 pcl b ofs = Some ? (load_result chunk' v).
    993 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     988  load chunk' m2 psp b ofs = Some ? (load_result chunk' v).
     989#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    994990#chunk';#Hsize;ncases (store_inv … STORE);
    995991#Hv;#Heq;
    996992nwhd in ⊢ (??%?);
    997 nrewrite > (in_bounds_true m2 chunk' pcl b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
     993nrewrite > (in_bounds_true m2 chunk' psp b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
    998994               (None ?) ?);
    999995##[nrewrite > Heq;
     
    10111007
    10121008ntheorem load_store_same:
    1013   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    1014   load chunk m2 pcl b ofs = Some ? (load_result chunk v).
    1015 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1009  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1010  load chunk m2 psp b ofs = Some ? (load_result chunk v).
     1011#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    10161012napply load_store_similar;//;
    10171013nqed.
    10181014       
    10191015ntheorem load_store_other:
    1020   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    1021   ∀chunk',pcl',b',ofs'.
     1016  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1017  ∀chunk',psp',b',ofs'.
    10221018  b' ≠ b
    10231019  ∨ ofs' + size_chunk chunk' ≤  ofs
    10241020  ∨ ofs + size_chunk chunk ≤ ofs' →
    1025   load chunk' m2 pcl' b' ofs' = load chunk' m1 pcl' b' ofs'.
    1026 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    1027 #chunk';#pcl';#b';#ofs';#H;
     1021  load chunk' m2 psp' b' ofs' = load chunk' m1 psp' b' ofs'.
     1022#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
     1023#chunk';#psp';#b';#ofs';#H;
    10281024ncases (store_inv … STORE);
    10291025#Hvalid;#Heq;nwhd in ⊢ (??%%);
    1030 ncases (in_bounds m1 chunk' pcl' b' ofs');
    1031 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' pcl' b' ofs' ? (Some ? ?) ??);
     1026ncases (in_bounds m1 chunk' psp' b' ofs');
     1027##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??);
    10321028   ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f;
    10331029      nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
     
    10451041      ##|#Hneq;@ ##]
    10461042   ##|napply (store_valid_access_1 … STORE);//##]
    1047 ##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' pcl' b' ofs');
     1043##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' psp' b' ofs');
    10481044   #H1;ncases H1;
    10491045   ##[#H2;#H3;nlapply (store_valid_access_2 … STORE … H2);#Hfalse;
     
    10551051
    10561052ntheorem load_store_overlap:
    1057   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    1058   ∀chunk',ofs',v'. load chunk' m2 pcl b ofs' = Some ? v' →
     1053  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1054  ∀chunk',ofs',v'. load chunk' m2 psp b ofs' = Some ? v' →
    10591055  ofs' ≠ ofs →
    10601056  ofs < ofs' + size_chunk chunk' →
    10611057  ofs' < ofs + size_chunk chunk →
    10621058  v' = Vundef.
    1063 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1059#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    10641060#chunk';#ofs';#v';#H;
    10651061#H1;#H2;#H3;
     
    10771073
    10781074ntheorem load_store_overlap':
    1079   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     1075  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    10801076  ∀chunk',ofs'.
    1081   valid_access m1 chunk' pcl b ofs' →
     1077  valid_access m1 chunk' psp b ofs' →
    10821078  ofs' ≠ ofs →
    10831079  ofs < ofs' + size_chunk chunk' →
    10841080  ofs' < ofs + size_chunk chunk →
    1085   load chunk' m2 pcl b ofs' = Some ? Vundef.
    1086 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1081  load chunk' m2 psp b ofs' = Some ? Vundef.
     1082#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    10871083#chunk';#ofs';#Hvalid;#H;#H1;#H2;
    1088 ncut (∃v'.load chunk' m2 pcl b ofs' = Some ? v')
     1084ncut (∃v'.load chunk' m2 psp b ofs' = Some ? v')
    10891085##[napply valid_access_load;
    10901086   napply (store_valid_access_1 … STORE);//
     
    10951091
    10961092ntheorem load_store_mismatch:
    1097   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     1093  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    10981094  ∀chunk',v'.
    1099   load chunk' m2 pcl b ofs = Some ? v' →
     1095  load chunk' m2 psp b ofs = Some ? v' →
    11001096  size_chunk chunk' ≠ size_chunk chunk →
    11011097  v' = Vundef.
    1102 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1098#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    11031099#chunk';#v';#H;#H1;
    11041100ncases (store_inv … STORE);
     
    11161112
    11171113ntheorem load_store_mismatch':
    1118   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     1114  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
    11191115  ∀chunk'.
    1120   valid_access m1 chunk' pcl b ofs →
     1116  valid_access m1 chunk' psp b ofs →
    11211117  size_chunk chunk' ≠ size_chunk chunk →
    1122   load chunk' m2 pcl b ofs = Some ? Vundef.
    1123 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1118  load chunk' m2 psp b ofs = Some ? Vundef.
     1119#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
    11241120#chunk';#Hvalid;#Hsize;
    1125 ncut (∃v'.load chunk' m2 pcl b ofs = Some ? v')
     1121ncut (∃v'.load chunk' m2 psp b ofs = Some ? v')
    11261122##[napply (valid_access_load …);
    11271123   napply
     
    11781174
    11791175ntheorem load_store_characterization:
    1180   ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    1181   ∀chunk',pcl',b',ofs'.
    1182   valid_access m1 chunk' pcl' b' ofs' →
    1183   load chunk' m2 pcl' b' ofs' =
     1176  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
     1177  ∀chunk',psp',b',ofs'.
     1178  valid_access m1 chunk' psp' b' ofs' →
     1179  load chunk' m2 psp' b' ofs' =
    11841180    match load_store_classification chunk b ofs chunk' b' ofs' with
    11851181    [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v)
    1186     | lsc_other _ ⇒ load chunk' m1 pcl' b' ofs'
     1182    | lsc_other _ ⇒ load chunk' m1 psp' b' ofs'
    11871183    | lsc_overlap _ _ _ _ ⇒ Some ? Vundef
    11881184    | lsc_mismatch _ _ _ ⇒ Some ? Vundef ].
    1189 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    1190 #chunk';#pcl';#b';#ofs';#Hvalid;
    1191 ncut (∃v'. load chunk' m2 pcl' b' ofs' = Some ? v')
     1185#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
     1186#chunk';#psp';#b';#ofs';#Hvalid;
     1187ncut (∃v'. load chunk' m2 psp' b' ofs' = Some ? v')
    11921188##[napply valid_access_load;
    11931189   napply (store_valid_access_1 … STORE … Hvalid);
     
    11951191   ncases (load_store_classification chunk b ofs chunk' b' ofs')
    11961192   ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2;
    1197       napply (load_compat_pointer … pcl);
    1198       ##[ nrewrite > (block_class_store … STORE b);
     1193      napply (load_compat_pointer … psp);
     1194      ##[ nrewrite > (memory_space_store … STORE b);
    11991195          ncases Hvalid; //;
    12001196      ##| napply (load_store_similar … STORE);//;
     
    12061202         ##|#H2;@;@2;//]
    12071203      ##|#H2;@2;//]
    1208    ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … pcl … Hx);
    1209      ##[ nrewrite > (block_class_store … STORE b');
     1204   ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … psp … Hx);
     1205     ##[ nrewrite > (memory_space_store … STORE b');
    12101206         nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12111207     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
     
    12141210     ##]
    12151211   ##|#H1;#H2;#H3;
    1216        nlapply (load_compat_pointer … pcl … Hx);
    1217        ##[ nrewrite > (block_class_store … STORE b');
     1212       nlapply (load_compat_pointer … psp … Hx);
     1213       ##[ nrewrite > (memory_space_store … STORE b');
    12181214           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
    12191215       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
     
    13751371nlemma class_alloc:
    13761372  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1377   ∀b'.blockclass m2 b' = if eqZb b' b then bcl else blockclass m1 b'.
     1373  ∀b'.block_space m2 b' = if eqZb b' b then bcl else block_space m1 b'.
    13781374#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    13791375nwhd in ALLOC:(??%%); ndestruct; #b';
     
    13831379nlemma class_alloc_same:
    13841380  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1385   blockclass m2 b = bcl.
     1381  block_space m2 b = bcl.
    13861382#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    13871383nwhd in ALLOC:(??%%); ndestruct;
     
    13911387nlemma class_alloc_other:
    13921388  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1393   ∀b'. valid_block m1 b' → blockclass m2 b' = blockclass m1 b'.
     1389  ∀b'. valid_block m1 b' → block_space m2 b' = block_space m1 b'.
    13941390#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    13951391#b'; nrewrite > (class_alloc … ALLOC b');
     
    14021398nlemma valid_access_alloc_other:
    14031399  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1404   ∀chunk,pcl,b',ofs.
    1405   valid_access m1 chunk pcl b' ofs →
    1406   valid_access m2 chunk pcl b' ofs.
     1400  ∀chunk,psp,b',ofs.
     1401  valid_access m1 chunk psp b' ofs →
     1402  valid_access m2 chunk psp b' ofs.
    14071403#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1408 #chunk;#pcl;#b';#ofs;#H;
     1404#chunk;#psp;#b';#ofs;#H;
    14091405ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;#Hcompat;
    14101406@;
     
    14181414nlemma valid_access_alloc_same:
    14191415  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1420   ∀chunk,pcl,ofs.
     1416  ∀chunk,psp,ofs.
    14211417  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1422   class_compat bcl pcl
    1423   valid_access m2 chunk pcl b ofs.
     1418  pointer_compat bcl psp
     1419  valid_access m2 chunk psp b ofs.
    14241420#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1425 #chunk;#pcl;#ofs; #Hlo; #Hhi; #Halign; #Hcompat;
     1421#chunk;#psp;#ofs; #Hlo; #Hhi; #Halign; #Hcompat;
    14261422@;
    14271423##[ napply (valid_new_block … ALLOC)
     
    14381434nlemma valid_access_alloc_inv:
    14391435  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1440   ∀chunk,pcl,b',ofs.
    1441   valid_access m2 chunk pcl b' ofs →
    1442   valid_access m1 chunk pcl b' ofs ∨
    1443   (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ class_compat bcl pcl)).
     1436  ∀chunk,psp,b',ofs.
     1437  valid_access m2 chunk psp b' ofs →
     1438  valid_access m1 chunk psp b' ofs ∨
     1439  (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl psp)).
    14441440#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1445 #chunk;#pcl;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;#Hct;
     1441#chunk;#psp;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;#Hct;
    14461442nelim (valid_block_alloc_inv … ALLOC ? Hblk);#H;
    14471443##[ nrewrite < H in ALLOC ⊢ %; #ALLOC';
     
    14591455ntheorem load_alloc_unchanged:
    14601456  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
    1461   ∀chunk,pcl,b',ofs.
     1457  ∀chunk,psp,b',ofs.
    14621458  valid_block m1 b' →
    1463   load chunk m2 pcl b' ofs = load chunk m1 pcl b' ofs.
     1459  load chunk m2 psp b' ofs = load chunk m1 psp b' ofs.
    14641460#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1465 #chunk;#pcl;#b';#ofs;#H;nwhd in ⊢ (??%%);
    1466 ncases (in_bounds m2 chunk pcl b' ofs); #H';
     1461#chunk;#psp;#b';#ofs;#H;nwhd in ⊢ (??%%);
     1462ncases (in_bounds m2 chunk psp b' ofs); #H';
    14671463##[ nelim (valid_access_alloc_inv … ALLOC ???? H');
    14681464  ##[ #H''; (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
     
    14771473      napply False_ind; napply (absurd ? H); napply (fresh_block_alloc … ALLOC)
    14781474  ##]
    1479 ##| ncases (in_bounds m1 chunk pcl b' ofs); #H''; nwhd in ⊢ (??%%); //;
     1475##| ncases (in_bounds m1 chunk psp b' ofs); #H''; nwhd in ⊢ (??%%); //;
    14801476    napply False_ind; napply (absurd ? ? H'); napply (valid_access_alloc_other … ALLOC); //
    14811477##] nqed.
     
    14831479ntheorem load_alloc_other:
    14841480  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1485   ∀chunk,pcl,b',ofs,v.
    1486   load chunk m1 pcl b' ofs = Some ? v →
    1487   load chunk m2 pcl b' ofs = Some ? v.
     1481  ∀chunk,psp,b',ofs,v.
     1482  load chunk m1 psp b' ofs = Some ? v →
     1483  load chunk m2 psp b' ofs = Some ? v.
    14881484#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1489 #chunk;#pcl;#b';#ofs;#v;#H;
     1485#chunk;#psp;#b';#ofs;#v;#H;
    14901486nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); ncases (load_valid_access … H); //;
    14911487nqed.
     
    14931489ntheorem load_alloc_same:
    14941490  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1495   ∀chunk,pcl,ofs,v.
    1496   load chunk m2 pcl b ofs = Some ? v →
     1491  ∀chunk,psp,ofs,v.
     1492  load chunk m2 psp b ofs = Some ? v →
    14971493  v = Vundef.
    14981494#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1499 #chunk;#pcl;#ofs;#v;#H;
     1495#chunk;#psp;#ofs;#v;#H;
    15001496nelim (load_inv … H); #H0; #H1; nrewrite > H1;
    15011497 nwhd in ALLOC:(??%%); (* XXX ndestruct; ??? *) napply (pairdisc_elim … ALLOC);
     
    15081504ntheorem load_alloc_same':
    15091505  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    1510   ∀chunk,pcl,ofs.
     1506  ∀chunk,psp,ofs.
    15111507  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1512   class_compat bcl pcl
    1513   load chunk m2 pcl b ofs = Some ? Vundef.
     1508  pointer_compat bcl psp
     1509  load chunk m2 psp b ofs = Some ? Vundef.
    15141510#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    1515 #chunk;#pcl;#ofs;#Hlo;#Hhi;#Hal;#Hct;
    1516 ncut (∃v. load chunk m2 pcl b ofs = Some ? v);
     1511#chunk;#psp;#ofs;#Hlo;#Hhi;#Hal;#Hct;
     1512ncut (∃v. load chunk m2 psp b ofs = Some ? v);
    15171513##[ napply valid_access_load; @; //;
    15181514  ##[ napply (valid_new_block … ALLOC);
     
    15811577
    15821578nlemma class_free:
    1583   ∀m,bf,b. b ≠ bf → blockclass (free m bf) b = blockclass m b.
     1579  ∀m,bf,b. b ≠ bf → block_space (free m bf) b = block_space m b.
    15841580#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
    15851581nrewrite > (update_o block_contents …); //; napply sym_neq; //;
     
    15871583
    15881584nlemma valid_access_free_1:
    1589   ∀m,bf,chunk,pcl,b,ofs.
    1590   valid_access m chunk pcl b ofs → b ≠ bf →
    1591   valid_access (free m bf) chunk pcl b ofs.
    1592 #m;#bf;#chunk;#pcl b ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hcompat;#Hneq;
     1585  ∀m,bf,chunk,psp,b,ofs.
     1586  valid_access m chunk psp b ofs → b ≠ bf →
     1587  valid_access (free m bf) chunk psp b ofs.
     1588#m;#bf;#chunk;#psp b ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hcompat;#Hneq;
    15931589@; //;
    15941590##[ napply valid_block_free_1; //
     
    15991595
    16001596nlemma valid_access_free_2:
    1601   ∀m,pcl,bf,chunk,ofs. ¬(valid_access (free m bf) chunk pcl bf ofs).
    1602 #m;#pcl;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;#Hct;
     1597  ∀m,psp,bf,chunk,ofs. ¬(valid_access (free m bf) chunk psp bf ofs).
     1598#m;#psp;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;#Hct;
    16031599nwhd in Hlo:(?%?);nwhd in Hlo:(?(?(?%?))?); nrewrite > (update_s block_contents …) in Hlo;
    16041600nwhd in Hhi:(??%);nwhd in Hhi:(??(?(?%?))); nrewrite > (update_s block_contents …) in Hhi;
     
    16111607
    16121608nlemma valid_access_free_inv:
    1613   ∀m,bf,chunk,pcl,b,ofs.
    1614   valid_access (free m bf) chunk pcl b ofs →
    1615   valid_access m chunk pcl b ofs ∧ b ≠ bf.
    1616 #m;#bf;#chunk;#pcl b ofs; nelim (decidable_eq_Z_Type b bf);
     1609  ∀m,bf,chunk,psp,b,ofs.
     1610  valid_access (free m bf) chunk psp b ofs →
     1611  valid_access m chunk psp b ofs ∧ b ≠ bf.
     1612#m;#bf;#chunk;#psp b ofs; nelim (decidable_eq_Z_Type b bf);
    16171613##[ #e; nrewrite > e;
    16181614    #H; napply False_ind; napply (absurd ? H (valid_access_free_2 …));
     
    16251621
    16261622ntheorem load_free:
    1627   ∀m,bf,chunk,pcl,b,ofs.
     1623  ∀m,bf,chunk,psp,b,ofs.
    16281624  b ≠ bf →
    1629   load chunk (free m bf) pcl b ofs = load chunk m pcl b ofs.
    1630 #m;#bf;#chunk;#pcl b ofs;#ne; nwhd in ⊢ (??%%);
    1631 nelim (in_bounds m chunk pcl b ofs);
     1625  load chunk (free m bf) psp b ofs = load chunk m psp b ofs.
     1626#m;#bf;#chunk;#psp b ofs;#ne; nwhd in ⊢ (??%%);
     1627nelim (in_bounds m chunk psp b ofs);
    16321628##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ????? (option val) ???);
    16331629  ##[ nwhd in ⊢ (??(??(??(???(?(?%?)))))?); nrewrite > (update_o block_contents …); //;
     
    16351631  ##| napply valid_access_free_1; //; napply ne;
    16361632  ##]
    1637 ##| nelim (in_bounds (free m bf) chunk pcl b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
     1633##| nelim (in_bounds (free m bf) chunk psp b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
    16381634    #H;#H'; napply False_ind; napply (absurd ? ? H');
    16391635    nelim (valid_access_free_inv …H); //;
     
    16631659
    16641660nlemma valid_access_free_list:
    1665   ∀chunk,pcl,b,ofs,m,bl.
    1666   valid_access m chunk pcl b ofs → ¬in_list ? b bl →
    1667   valid_access (free_list m bl) chunk pcl b ofs.
    1668 #chunk; #pcl b ofs; #m; #bl; nelim bl;
     1661  ∀chunk,psp,b,ofs,m,bl.
     1662  valid_access m chunk psp b ofs → ¬in_list ? b bl →
     1663  valid_access (free_list m bl) chunk psp b ofs.
     1664#chunk; #psp b ofs; #m; #bl; nelim bl;
    16691665##[ nwhd in ⊢ (?→?→(?%????)); //
    16701666##| #h;#t;#IH;#H;#notin; nrewrite > (unfold_free_list m h t); napply valid_access_free_1;
     
    16741670
    16751671nlemma valid_access_free_list_inv:
    1676   ∀chunk,pcl,b,ofs,m,bl.
    1677   valid_access (free_list m bl) chunk pcl b ofs →
    1678   ¬in_list ? b bl ∧ valid_access m chunk pcl b ofs.
    1679 #chunk; #pcl b ofs; #m; #bl; nelim bl;
     1672  ∀chunk,psp,b,ofs,m,bl.
     1673  valid_access (free_list m bl) chunk psp b ofs →
     1674  ¬in_list ? b bl ∧ valid_access m chunk psp b ofs.
     1675#chunk; #psp b ofs; #m; #bl; nelim bl;
    16801676##[ nwhd in ⊢ ((?%????)→?); #H; @; //
    16811677##| #h;#t;#IH; nrewrite > (unfold_free_list m h t); #H;
     
    16891685
    16901686nlemma valid_pointer_valid_access:
    1691   ∀m,pcl,b,ofs.
    1692   valid_pointer m pcl b ofs = true ↔ valid_access m Mint8unsigned pcl b ofs.
    1693 #m;#pcl b ofs;nwhd in ⊢ (?(??%?)?); @;
     1687  ∀m,psp,b,ofs.
     1688  valid_pointer m psp b ofs = true ↔ valid_access m Mint8unsigned psp b ofs.
     1689#m;#psp b ofs;nwhd in ⊢ (?(??%?)?); @;
    16941690##[ #H;
    16951691    nlapply (andb_true_l … H); #H';
     
    17041700    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    17051701    ##| ncases ofs; /2/;
    1706     ##| nwhd in H4:(??%?); nelim (class_compat_dec (blockclass m b) pcl) in H4;
     1702    ##| nwhd in H4:(??%?); nelim (pointer_compat_dec (block_space m b) psp) in H4;
    17071703        ##[ //; ##| #Hn e; nwhd in e:(??%%); ndestruct ##]
    17081704    ##]
     
    17111707    nrewrite > (Zle_to_Zleb_true … Hlo);
    17121708    nwhd in Hhi:(?(??%)?); nrewrite > (Zlt_to_Zltb_true … ?);
    1713     ##[ nwhd in ⊢ (??%?); nelim (class_compat_dec (blockclass m b) pcl);
     1709    ##[ nwhd in ⊢ (??%?); nelim (pointer_compat_dec (block_space m b) psp);
    17141710      ##[ //;
    17151711      ##| #Hct'; napply False_ind; napply (absurd … Hct Hct');
     
    17211717
    17221718ntheorem valid_pointer_alloc:
    1723   ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,pcl. ∀b,b': block. ∀ofs: Z.
     1719  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,psp. ∀b,b': block. ∀ofs: Z.
    17241720  alloc m1 lo hi bcl = 〈m2, b'〉 →
    1725   valid_pointer m1 pcl b ofs = true →
    1726   valid_pointer m2 pcl b ofs = true.
    1727 #m1;#m2;#lo;#hi;#bcl pcl;#b;#b';#ofs;#ALLOC;#VALID;
     1721  valid_pointer m1 psp b ofs = true →
     1722  valid_pointer m2 psp b ofs = true.
     1723#m1;#m2;#lo;#hi;#bcl psp;#b;#b';#ofs;#ALLOC;#VALID;
    17281724nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
    17291725napply (proj2 ?? (valid_pointer_valid_access ????));
     
    17331729ntheorem valid_pointer_store:
    17341730  ∀chunk: memory_chunk. ∀m1,m2: mem.
    1735   ∀pcl,pcl': ptr_class. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
    1736   store chunk m1 pcl' b' ofs' v = Some ? m2 →
    1737   valid_pointer m1 pcl b ofs = true → valid_pointer m2 pcl b ofs = true.
    1738 #chunk;#m1;#m2;#pcl pcl';#b;#b';#ofs;#ofs';#v;#STORE;#VALID;
     1731  ∀psp,psp': memory_space. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
     1732  store chunk m1 psp' b' ofs' v = Some ? m2 →
     1733  valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
     1734#chunk;#m1;#m2;#psp psp';#b;#b';#ofs;#ofs';#v;#STORE;#VALID;
    17391735nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
    17401736napply (proj2 ?? (valid_pointer_valid_access ????));
     
    17921788(*
    17931789nlemma store_unmapped_inj: ∀val_inj.
    1794   ∀mi,m1,m2,pcl,b,ofs,v,chunk,m1'.
     1790  ∀mi,m1,m2,psp,b,ofs,v,chunk,m1'.
    17951791  mem_inj val_inj mi m1 m2 →
    17961792  mi b = None ? →
    1797   store chunk m1 pcl b ofs v = Some ? m1' →
     1793  store chunk m1 psp b ofs v = Some ? m1' →
    17981794  mem_inj val_inj mi m1' m2.
    17991795#val_inj;
    1800 #mi;#m1;#m2;#pcl b ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
     1796#mi;#m1;#m2;#psp b ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
    18011797nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
    18021798ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
     
    18071803
    18081804nlemma store_outside_inj: ∀val_inj.
    1809   ∀mi,m1,m2,chunk,pcl,b,ofs,v,m2'.
     1805  ∀mi,m1,m2,chunk,psp,b,ofs,v,m2'.
    18101806  mem_inj val_inj mi m1 m2 →
    18111807  (∀b',delta.
     
    18131809    high_bound m1 b' + delta ≤ ofs
    18141810    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
    1815   store chunk m2 pcl b ofs v = Some ? m2' →
     1811  store chunk m2 psp b ofs v = Some ? m2' →
    18161812  mem_inj val_inj mi m1 m2'.
    18171813#val_inj;
    1818 #mi;#m1;#m2;#chunk;#pcl b ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
     1814#mi;#m1;#m2;#chunk;#psp b ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
    18191815nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
    18201816nlapply (Hinj … Hmi0 Hload);*;#v2;*;#LOAD2;#VINJ;
     
    21892185  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
    21902186  extends m1 m2 →
    2191   load chunk m1 pcl b ofs = Some ? v →
    2192   load chunk m2 pcl b ofs = Some ? v.
    2193 #chunk;#m1;#m2;#pcl b ofs;#v;
     2187  load chunk m1 psp b ofs = Some ? v →
     2188  load chunk m2 psp b ofs = Some ? v.
     2189#chunk;#m1;#m2;#psp b ofs;#v;
    21942190*;#Hnext;#Hinj;#LOAD;
    21952191nlapply (Hinj … LOAD); ##[ nnormalize; // ##| ##2,3: ##]
     
    22012197  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
    22022198  extends m1 m2 →
    2203   store chunk m1 pcl b ofs v = Some ? m1' →
    2204   ∃m2'. store chunk m2 pcl b ofs v = Some ? m2' ∧ extends m1' m2'.
     2199  store chunk m1 psp b ofs v = Some ? m1' →
     2200  ∃m2'. store chunk m2 psp b ofs v = Some ? m2' ∧ extends m1' m2'.
    22052201#chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1;
    22062202nlapply (store_mapped_inj … Hinj ?? STORE1 ?);
     
    22242220  extends m1 m2 →
    22252221  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
    2226   store chunk m2 pcl b ofs v = Some ? m2' →
     2222  store chunk m2 psp b ofs v = Some ? m2' →
    22272223  extends m1 m2'.
    22282224#chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @;
     
    22382234ntheorem valid_pointer_extends:
    22392235  ∀m1,m2,b,ofs.
    2240   extends m1 m2 → valid_pointer m1 pcl b ofs = true →
    2241   valid_pointer m2 pcl b ofs = true.
     2236  extends m1 m2 → valid_pointer m1 psp b ofs = true →
     2237  valid_pointer m2 psp b ofs = true.
    22422238#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
    22432239nrewrite < (Zplus_z_OZ ofs);
     
    22692265nlemma load_lessdef:
    22702266  ∀m1,m2,chunk,b,ofs,v1.
    2271   lessdef m1 m2 → load chunk m1 pcl b ofs = Some ? v1 →
    2272   ∃v2. load chunk m2 pcl b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
     2267  lessdef m1 m2 → load chunk m1 psp b ofs = Some ? v1 →
     2268  ∃v2. load chunk m2 psp b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
    22732269#m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0;
    22742270nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ##| ##2,3:##skip ##]
     
    22942290  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
    22952291  lessdef m1 m2 → Val_lessdef v1 v2 →
    2296   store chunk m1 pcl b ofs v1 = Some ? m1' →
    2297   ∃m2'. store chunk m2 pcl b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
     2292  store chunk m1 psp b ofs v1 = Some ? m1' →
     2293  ∃m2'. store chunk m2 psp b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
    22982294#m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1';
    22992295*;#Hnext;#Hinj;#Hvless;#STORE0;
     
    23862382nlemma valid_pointer_lessdef:
    23872383  ∀m1,m2,b,ofs.
    2388   lessdef m1 m2 → valid_pointer m1 pcl b ofs = true → valid_pointer m2 pcl b ofs = true.
     2384  lessdef m1 m2 → valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
    23892385#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
    23902386nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //;
     
    25232519  mem_inject f m1 m2 →
    25242520  valid_pointer m1 b (signed ofs) = true →
    2525   val_inject f (Vptr pcl b ofs) (Vptr b' ofs') →
     2521  val_inject f (Vptr psp b ofs) (Vptr b' ofs') →
    25262522  valid_pointer m2 b' (signed ofs') = true.
    25272523#f;#m1;#m2;#b;#ofs;#b';#ofs';
     
    35713567
    35723568nremark in_bounds_equiv:
    3573   ∀chunk1,chunk2,m,pcl,b,ofs.∀A:Type.∀a1,a2: A.
     3569  ∀chunk1,chunk2,m,psp,b,ofs.∀A:Type.∀a1,a2: A.
    35743570  size_chunk chunk1 = size_chunk chunk2 →
    3575   (match in_bounds m chunk1 pcl b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
    3576   (match in_bounds m chunk2 pcl b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
    3577 #chunk1;#chunk2;#m;#pcl b ofs;#A;#a1;#a2;#Hsize;
    3578 nelim (in_bounds m chunk1 pcl b ofs);
     3571  (match in_bounds m chunk1 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
     3572  (match in_bounds m chunk2 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
     3573#chunk1;#chunk2;#m;#psp b ofs;#A;#a1;#a2;#Hsize;
     3574nelim (in_bounds m chunk1 psp b ofs);
    35793575##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //;
    35803576    napply valid_access_compat; //;
    3581 ##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 pcl b ofs); //;
     3577##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 psp b ofs); //;
    35823578    #H'; napply False_ind; napply (absurd ?? H);
    35833579    napply valid_access_compat; //;
     
    35883584  storev Mint8signed m a v = storev Mint8unsigned m a v.
    35893585#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
    3590 #pcl b ofs; nwhd in ⊢ (??%%);
     3586#psp b ofs; nwhd in ⊢ (??%%);
    35913587nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //;
    35923588nqed.
     
    35963592  storev Mint16signed m a v = storev Mint16unsigned m a v.
    35973593#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
    3598 #pcl b ofs; nwhd in ⊢ (??%%);
     3594#psp b ofs; nwhd in ⊢ (??%%);
    35993595nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //;
    36003596nqed.
     
    36093605  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
    36103606#m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //;
    3611 #pcl b ofs; nwhd in ⊢ (??%(????%));
     3607#psp b ofs; nwhd in ⊢ (??%(????%));
    36123608nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //;
    3613 nelim (in_bounds m Mint8unsigned pcl b (signed ofs)); /2/;
     3609nelim (in_bounds m Mint8unsigned psp b (signed ofs)); /2/;
    36143610#H; nwhd in ⊢ (??%%);
    36153611nelim (getN 0 (signed ofs) (contents (blocks m b)));
Note: See TracChangeset for help on using the changeset viewer.