Changeset 124 for C-semantics/Mem.ma


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

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Mem.ma

    r24 r124  
    8383  plus a mapping from byte offsets to contents.  *)
    8484
     85ninductive block_class : Type ≝
     86| UnspecifiedB : block_class
     87| DataB : block_class
     88| IDataB : block_class
     89| XDataB : block_class
     90| CodeB : block_class.
     91
    8592(* XXX: mkblock *)
    8693nrecord block_contents : Type[0] ≝ {
    8794  low: Z;
    8895  high: Z;
    89   contents: contentmap
     96  contents: contentmap;
     97  class: block_class
    9098}.
    9199
     
    184192nqed.
    185193
    186 ndefinition empty_block : Z → Z → block_contents ≝
    187   λlo,hi.mk_block_contents lo hi (λy. Undef).
     194ndefinition empty_block : Z → Z → block_class → block_contents ≝
     195  λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.
    188196
    189197ndefinition empty: mem ≝
    190   mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
     198  mk_mem (λx.empty_block OZ OZ UnspecifiedB) (pos one) one_pos.
    191199
    192200ndefinition nullptr: block ≝ OZ.
     
    204212nqed.
    205213
    206 ndefinition alloc : mem → Z → Z → mem × block ≝
    207   λm,lo,hi.〈mk_mem
     214ndefinition alloc : mem → Z → Z → block_class → mem × block ≝
     215  λm,lo,hi,bty.〈mk_mem
    208216              (update … (nextblock m)
    209                  (empty_block lo hi)
     217                 (empty_block lo hi bty)
    210218                 (blocks m))
    211219              (Zsucc (nextblock m))
     
    221229ndefinition free ≝
    222230  λm,b.mk_mem (update … b
    223                 (empty_block OZ OZ)
     231                (empty_block OZ OZ UnspecifiedB)
    224232                (blocks m))
    225233        (nextblock m)
     
    241249ndefinition high_bound : mem → block → Z ≝
    242250  λm,b.high (blocks m b).
     251ndefinition blockclass: mem → block → block_class ≝
     252  λm,b.class (blocks m b).
    243253
    244254(* A block address is valid if it was previously allocated. It remains valid
     
    550560nqed.
    551561
    552 
    553 (* [valid_access m chunk b ofs] holds if a memory access (load or store)
     562ninductive 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
     570nlemma class_compat_dec : ∀b,p. class_compat b p + ¬class_compat b p.
     571#b p; ncases b;
     572##[ ##1: @1; //;
     573##| ##*: ncases p; /2/; @2; @; #H; ninversion H; #e1 e2; ndestruct; #e3; ndestruct;
     574##] nqed.
     575
     576ndefinition 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)
    554580    of the given chunk is possible in [m] at address [b, ofs].
    555581    This means:
     
    557583- The range of bytes accessed is within the bounds of [b].
    558584- The offset [ofs] is aligned.
     585- The pointer classs [pcl] is compatible with the class of [b].
    559586*)
    560587
    561 ninductive valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z)
     588ninductive valid_access (m: mem) (chunk: memory_chunk) (pcl: ptr_class) (b: block) (ofs: Z)
    562589            : Prop ≝
    563590  | valid_access_intro:
     
    566593      ofs + size_chunk chunk ≤ high_bound m b →
    567594      (align_chunk chunk ∣ ofs) →
    568       valid_access m chunk b ofs.
     595      class_compat (blockclass m b) pcl →
     596      valid_access m chunk pcl b ofs.
    569597
    570598(* The following function checks whether accessing the given memory chunk
     
    573601(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
    574602nlet rec in_bounds
    575   (m:mem) (chunk:memory_chunk) (b:block) (ofs:Z) on b : 
    576     Sum (valid_access m chunk b ofs) (Not (valid_access m chunk b ofs)) ≝ ?.
     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)) ≝ ?.
    577605napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
    578606##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo;
    579607    ##[ napply (Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)); #Hhi;
    580608        ##[ nelim (dec_dividesZ (align_chunk chunk) ofs); #Hal;
    581           ##[ @1; @; // ##]
     609          ##[ ncases (class_compat_dec (blockclass m b) pcl); #Hcl;
     610            ##[ @1; @; // ##]
     611          ##]
    582612        ##]
    583613    ##]
    584614##]
    585 @2; napply nmk; *; #Hval; #Hlo'; #Hhi'; #Hal'; napply (absurd ???); //;
     615@2; napply nmk; *; #Hval; #Hlo'; #Hhi'; #Hal'; #Hcl'; napply (absurd ???); //;
    586616nqed.
    587617
    588618nlemma in_bounds_true:
    589   ∀m,chunk,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
    590   valid_access m chunk b ofs ->
    591   (match in_bounds m chunk b ofs with
     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
    592622   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
    593 #m;#chunk;#b;#ofs;#A;#a1;#a2;#H;
    594 ncases (in_bounds m chunk b ofs);nnormalize;#H1;
     623#m chunk pcl b ofs A a1 a2 H;
     624ncases (in_bounds m chunk pcl b ofs);nnormalize;#H1;
    595625##[//
    596626##|nelim (?:False);napply (absurd ? H H1)]
     
    600630  given offset falls within the bounds of the corresponding block. *)
    601631
    602 ndefinition valid_pointer : mem → block → Z → bool ≝
    603 λm,b,ofs. Zltb b (nextblock m) ∧
     632ndefinition valid_pointer : mem → ptr_class → block → Z → bool ≝
     633λm,pcl,b,ofs. Zltb b (nextblock m) ∧
    604634  Zleb (low_bound m b) ofs ∧
    605   Zltb ofs (high_bound m b).
    606 (* XXX: use lebZ etc.
    607  ≝ λm,b,ofs.b < nextblock m ∧
    608   low_bound m b ≤ ofs ∧
    609  
    610   ofs < high_bound m b. *)
     635  Zltb ofs (high_bound m b) ∧
     636  is_class_compat (blockclass m b) pcl.
    611637
    612638(* [load chunk m b ofs] perform a read in memory state [m], at address
     
    614640  or the memory access is out of bounds. *)
    615641
    616 ndefinition load : memory_chunk → mem → block → Z → option val ≝
    617 λchunk,m,b,ofs.
    618   match in_bounds m chunk b ofs with
     642ndefinition 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
    619645  [ inl _ ⇒ Some ? (load_result chunk
    620646           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
     
    622648
    623649nlemma load_inv:
    624   ∀chunk,m,b,ofs,v.
    625   load chunk m b ofs = Some ? v →
    626   valid_access m chunk b ofs ∧
     650  ∀chunk,m,pcl,b,ofs,v.
     651  load chunk m pcl b ofs = Some ? v →
     652  valid_access m chunk pcl b ofs ∧
    627653  v = load_result chunk
    628654           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
    629 #chunk;#m;#b;#ofs;#v;nwhd in ⊢ (??%? → ?);
    630 ncases (in_bounds m chunk b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;
     655#chunk m pcl b ofs v; nwhd in ⊢ (??%? → ?);
     656ncases (in_bounds m chunk pcl b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;
    631657##[ @;//; ndestruct; //;
    632658##| ndestruct
     
    639665nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    640666  match addr with
    641   [ Vptr b ofs ⇒ load chunk m b (signed ofs)
     667  [ Vptr pcl b ofs ⇒ load chunk m pcl b (signed ofs)
    642668  | _ ⇒ None ? ].
    643669
     
    651677    (update ? b
    652678        (mk_block_contents (low c) (high c)
    653                  (setN (pred_size_chunk chunk) ofs v (contents c)))
     679                 (setN (pred_size_chunk chunk) ofs v (contents c)) (class c))
    654680        (blocks m))
    655681    (nextblock m)
     
    661687  or the memory access is out of bounds. *)
    662688
    663 ndefinition store : memory_chunk → mem → block → Z → val → option mem ≝
    664 λchunk,m,b,ofs,v.
    665   match in_bounds m chunk b ofs with
     689ndefinition 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
    666692  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
    667693  | inr _ ⇒ None ? ].
    668694
    669695nlemma store_inv:
    670   ∀chunk,m,b,ofs,v,m'.
    671   store chunk m b ofs v = Some ? m' →
    672   valid_access m chunk b ofs ∧
     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 ∧
    673699  m' = unchecked_store chunk m b ofs v.
    674 #chunk;#m;#b;#ofs;#v;#m';nwhd in ⊢ (??%? → ?);
     700#chunk m pcl b ofs v m'; nwhd in ⊢ (??%? → ?);
    675701(*9*)
    676 ncases (in_bounds m chunk b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
     702ncases (in_bounds m chunk pcl b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
    677703##[@; ##[//|ndestruct;//]
    678704##|ndestruct]
     
    685711λchunk,m,addr,v.
    686712  match addr with
    687   [ Vptr b ofs ⇒ store chunk m b (signed ofs) v
     713  [ Vptr pcl b ofs ⇒ store chunk m pcl b (signed ofs) v
    688714  | _ ⇒ None ? ].
    689715
     
    752778nqed.
    753779
    754 ndefinition block_init_data : list init_data → block_contents ≝
    755   λi_data.mk_block_contents
    756     OZ (size_init_data_list i_data) (contents_init_data OZ i_data).
    757 
    758 ndefinition alloc_init_data : mem → list init_data → mem × block ≝
    759   λm,i_data.
     780ndefinition block_init_data : list init_data → block_class → block_contents ≝
     781  λi_data,bcl.mk_block_contents
     782    OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.
     783
     784ndefinition alloc_init_data : mem → list init_data → block_class → mem × block ≝
     785  λm,i_data,bcl.
    760786  〈mk_mem (update ? (nextblock m)
    761                  (block_init_data i_data)
     787                 (block_init_data i_data bcl)
    762788                 (blocks m))
    763789         (Zsucc (nextblock m))
     
    766792
    767793nremark block_init_data_empty:
    768   block_init_data [] = empty_block OZ OZ.
     794  ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl.
    769795//;
    770796nqed.
     
    781807
    782808nlemma valid_access_valid_block:
    783   ∀m,chunk,b,ofs. valid_access m chunk b ofs → valid_block m b.
    784 #m;#chunk;#b;#ofs;#H;
     809  ∀m,chunk,pcl,b,ofs. valid_access m chunk pcl b ofs → valid_block m b.
     810#m;#chunk;#pcl;#b;#ofs;#H;
    785811nelim H;//;
    786812nqed.
    787813
    788814nlemma valid_access_aligned:
    789   ∀m,chunk,b,ofs.
    790   valid_access m chunk b ofs → (align_chunk chunk ∣ ofs).
    791 #m;#chunk;#b;#ofs;#H;
     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;
    792818nelim H;//;
    793819nqed.
    794820
    795821nlemma valid_access_compat:
    796   ∀m,chunk1,chunk2,b,ofs.
     822  ∀m,chunk1,chunk2,pcl,b,ofs.
    797823  size_chunk chunk1 = size_chunk chunk2 →
    798   valid_access m chunk1 b ofs →
    799   valid_access m chunk2 b ofs.
    800 #m;#chunk;#chunk2;#b;#ofs;#H1;#H2;
    801 nelim H2;#H3;#H4;#H5;#H6;
     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;
     827nelim H2;#H3;#H4;#H5;#H6;#H7;
    802828nrewrite > H1 in H5;#H5;
    803829@;//;
     
    810836
    811837ntheorem valid_access_load:
    812   ∀m,chunk,b,ofs.
    813   valid_access m chunk b ofs →
    814   ∃v. load chunk m b ofs = Some ? v.
    815 #m;#chunk;#b;#ofs;#H;@;
     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;@;
    816842##[##2:nwhd in ⊢ (??%?);napply in_bounds_true;//;
    817843##|##skip]
     
    819845
    820846ntheorem load_valid_access:
    821   ∀m,chunk,b,ofs,v.
    822   load chunk m b ofs = Some ? v →
    823   valid_access m chunk b ofs.
    824 #m;#chunk;#b;#ofs;#v;#H;
     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;
    825851ncases (load_inv … H);//;
    826852nqed.
     
    831857
    832858nlemma valid_access_store:
    833   ∀m1,chunk,b,ofs,v.
    834   valid_access m1 chunk b ofs →
    835   ∃m2. store chunk m1 b ofs v = Some ? m2.
    836 #m1;#chunk;#b;#ofs;#v;#H;
     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;
    837863@;
    838864##[##2:napply in_bounds_true;//
     
    843869
    844870nlemma low_bound_store:
    845   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     871  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    846872  ∀b'.low_bound m2 b' = low_bound m1 b'.
    847 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     873#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    848874#b';ncases (store_inv … STORE);
    849875#H1;#H2;nrewrite > H2;
     
    854880
    855881nlemma nextblock_store :
    856   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     882  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    857883  nextblock m2 = nextblock m1.
    858 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     884#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    859885ncases (store_inv … STORE);
    860886#Hvalid;#Heq;
     
    863889
    864890nlemma high_bound_store:
    865   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     891  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    866892  ∀b'. high_bound m2 b' = high_bound m1 b'.
    867 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     893#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    868894#b';ncases (store_inv … STORE);
    869895#Hvalid;#H;
     
    874900nqed.
    875901
     902nlemma 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;
     906#b';ncases (store_inv … STORE);
     907#Hvalid;#H;
     908nrewrite > H;
     909nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
     910nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
     911ncases (eqZb b' b);nnormalize;//;
     912nqed.
     913
    876914nlemma store_valid_block_1:
    877   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     915  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    878916  ∀b'. valid_block m1 b' → valid_block m2 b'.
    879 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     917#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    880918#b';nwhd in ⊢ (% → %);#Hv;
    881919nrewrite > (nextblock_store … STORE);//;
     
    883921
    884922nlemma store_valid_block_2:
    885   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     923  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    886924  ∀b'. valid_block m2 b' → valid_block m1 b'.
    887 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     925#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    888926#b';nwhd in ⊢ (%→%);
    889927nrewrite > (nextblock_store … STORE);//;
     
    893931
    894932nlemma store_valid_access_1:
    895   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    896   ∀chunk',b',ofs'.
    897   valid_access m1 chunk' b' ofs' → valid_access m2 chunk' b' ofs'.
    898 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
    899 #chunk';#b';#ofs';
     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';
    900938* Hv;
    901 #Hvb;#Hl;#Hr;#Halign;
     939#Hvb;#Hl;#Hr;#Halign;#Hptr;
    902940@;//;
    903941##[napply (store_valid_block_1 … STORE);//
    904942##|nrewrite > (low_bound_store … STORE …);//
    905 ##|nrewrite > (high_bound_store … STORE …);//]
     943##|nrewrite > (high_bound_store … STORE …);//
     944##|nrewrite > (block_class_store … STORE …);//]
    906945nqed.
    907946
    908947nlemma store_valid_access_2:
    909   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    910   ∀chunk',b',ofs'.
    911   valid_access m2 chunk' b' ofs' → valid_access m1 chunk' b' ofs'.
    912 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
    913 #chunk';#b';#ofs';
     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';
    914953* Hv;
    915 #Hvb;#Hl;#Hr;#Halign;
     954#Hvb;#Hl;#Hr;#Halign;#Hcompat;
    916955@;//;
    917956##[napply (store_valid_block_2 … STORE);//
    918957##|nrewrite < (low_bound_store … STORE …);//
    919 ##|nrewrite < (high_bound_store … STORE …);//]
     958##|nrewrite < (high_bound_store … STORE …);//
     959##|nrewrite < (block_class_store … STORE …);//]
    920960nqed.
    921961
    922962nlemma store_valid_access_3:
    923   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    924   valid_access m1 chunk b ofs.
    925 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     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;
    926966ncases (store_inv … STORE);//;
    927967nqed.
     
    930970             store_valid_access_3: mem.*)
    931971
     972nlemma 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.
     978nlapply (load_valid_access … LOAD); #Hvalid;
     979ncut (valid_access m chunk pcl' b ofs);
     980##[ @;nelim Hvalid; //;
     981##| #Hvalid';
     982    nrewrite < LOAD; nwhd in ⊢ (??%%);
     983    nrewrite > (in_bounds_true … (option val) ?? Hvalid);
     984    nrewrite > (in_bounds_true … (option val) ?? Hvalid');
     985    //
     986##] nqed.
     987
    932988ntheorem load_store_similar:
    933   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     989  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    934990  ∀chunk'.
    935991  size_chunk chunk' = size_chunk chunk →
    936   load chunk' m2 b ofs = Some ? (load_result chunk' v).
    937 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     992  load chunk' m2 pcl b ofs = Some ? (load_result chunk' v).
     993#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    938994#chunk';#Hsize;ncases (store_inv … STORE);
    939995#Hv;#Heq;
    940996nwhd in ⊢ (??%?);
    941 nrewrite > (in_bounds_true m2 chunk' b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
     997nrewrite > (in_bounds_true m2 chunk' pcl b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))
    942998               (None ?) ?);
    943999##[nrewrite > Heq;
     
    9491005      nrewrite > (size_chunk_pred …) in Hsize;#Hsize;
    9501006      napply injective_Z_of_nat;napply (injective_Zplus_r 1);//;##]
    951 ##|napply (store_valid_access_1 ?????? STORE);
    952    ncases Hv;#H1;#H2;#H3;#H4;@;//;
     1007##|napply (store_valid_access_1 STORE);
     1008   ncases Hv;#H1;#H2;#H3;#H4;#H5;@;//;
    9531009   nrewrite > (align_chunk_compat … Hsize);//]
    9541010nqed.
    9551011
    9561012ntheorem load_store_same:
    957   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    958   load chunk m2 b ofs = Some ? (load_result chunk v).
    959 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     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;
    9601016napply load_store_similar;//;
    9611017nqed.
    9621018       
    9631019ntheorem load_store_other:
    964   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    965   ∀chunk',b',ofs'.
     1020  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
     1021  ∀chunk',pcl',b',ofs'.
    9661022  b' ≠ b
    9671023  ∨ ofs' + size_chunk chunk' ≤  ofs
    9681024  ∨ ofs + size_chunk chunk ≤ ofs' →
    969   load chunk' m2 b' ofs' = load chunk' m1 b' ofs'.
    970 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
    971 #chunk';#b';#ofs';#H;
     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;
    9721028ncases (store_inv … STORE);
    9731029#Hvalid;#Heq;nwhd in ⊢ (??%%);
    974 ncases (in_bounds m1 chunk' b' ofs');
    975 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' b' ofs' ? (Some ? ?) ??);
     1030ncases (in_bounds m1 chunk' pcl' b' ofs');
     1031##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' pcl' b' ofs' ? (Some ? ?) ??);
    9761032   ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f;
    9771033      nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
     
    9891045      ##|#Hneq;@ ##]
    9901046   ##|napply (store_valid_access_1 … STORE);//##]
    991 ##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' b' ofs');
     1047##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' pcl' b' ofs');
    9921048   #H1;ncases H1;
    9931049   ##[#H2;#H3;nlapply (store_valid_access_2 … STORE … H2);#Hfalse;
     
    9991055
    10001056ntheorem load_store_overlap:
    1001   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    1002   ∀chunk',ofs',v'. load chunk' m2 b ofs' = Some ? v' →
     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' →
    10031059  ofs' ≠ ofs →
    10041060  ofs < ofs' + size_chunk chunk' →
    10051061  ofs' < ofs + size_chunk chunk →
    10061062  v' = Vundef.
    1007 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     1063#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    10081064#chunk';#ofs';#v';#H;
    10091065#H1;#H2;#H3;
     
    10211077
    10221078ntheorem load_store_overlap':
    1023   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     1079  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    10241080  ∀chunk',ofs'.
    1025   valid_access m1 chunk' b ofs' →
     1081  valid_access m1 chunk' pcl b ofs' →
    10261082  ofs' ≠ ofs →
    10271083  ofs < ofs' + size_chunk chunk' →
    10281084  ofs' < ofs + size_chunk chunk →
    1029   load chunk' m2 b ofs' = Some ? Vundef.
    1030 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     1085  load chunk' m2 pcl b ofs' = Some ? Vundef.
     1086#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    10311087#chunk';#ofs';#Hvalid;#H;#H1;#H2;
    1032 ncut (∃v'.load chunk' m2 b ofs' = Some ? v')
     1088ncut (∃v'.load chunk' m2 pcl b ofs' = Some ? v')
    10331089##[napply valid_access_load;
    10341090   napply (store_valid_access_1 … STORE);//
     
    10391095
    10401096ntheorem load_store_mismatch:
    1041   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     1097  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    10421098  ∀chunk',v'.
    1043   load chunk' m2 b ofs = Some ? v' →
     1099  load chunk' m2 pcl b ofs = Some ? v' →
    10441100  size_chunk chunk' ≠ size_chunk chunk →
    10451101  v' = Vundef.
    1046 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     1102#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    10471103#chunk';#v';#H;#H1;
    10481104ncases (store_inv … STORE);
     
    10601116
    10611117ntheorem load_store_mismatch':
    1062   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
     1118  ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 →
    10631119  ∀chunk'.
    1064   valid_access m1 chunk' b ofs →
     1120  valid_access m1 chunk' pcl b ofs →
    10651121  size_chunk chunk' ≠ size_chunk chunk →
    1066   load chunk' m2 b ofs = Some ? Vundef.
    1067 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
     1122  load chunk' m2 pcl b ofs = Some ? Vundef.
     1123#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
    10681124#chunk';#Hvalid;#Hsize;
    1069 ncut (∃v'.load chunk' m2 b ofs = Some ? v')
     1125ncut (∃v'.load chunk' m2 pcl b ofs = Some ? v')
    10701126##[napply (valid_access_load …);
    1071    napply (store_valid_access_1 … STORE);//
     1127   napply
     1128    (store_valid_access_1 … STORE);//
    10721129##|*;#x;#Hx;nrewrite > Hx;napply eq_f;
    10731130   napply (load_store_mismatch … STORE … Hsize);//;##]
     
    11211178
    11221179ntheorem load_store_characterization:
    1123   ∀chunk,m1,b,ofs,v,m2.store chunk m1 b ofs v = Some ? m2 →
    1124   ∀chunk',b',ofs'.
    1125   valid_access m1 chunk' b' ofs' ->
    1126   load chunk' m2 b' ofs' =
     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' =
    11271184    match load_store_classification chunk b ofs chunk' b' ofs' with
    1128     [ lsc_similar _ _ _ => Some ? (load_result chunk' v)
    1129     | lsc_other _ => load chunk' m1 b' ofs'
    1130     | lsc_overlap _ _ _ _ => Some ? Vundef
    1131     | lsc_mismatch _ _ _ => Some ? Vundef ].
    1132 #chunk;#m1;#b;#ofs;#v;#m2;#STORE;
    1133 #chunk';#b';#ofs';#Hvalid;
    1134 ncut (∃v'. load chunk' m2 b' ofs' = Some ? v')
     1185    [ lsc_similar _ _ _ Some ? (load_result chunk' v)
     1186    | lsc_other _ ⇒ load chunk' m1 pcl' b' ofs'
     1187    | lsc_overlap _ _ _ _ Some ? Vundef
     1188    | lsc_mismatch _ _ _ Some ? Vundef ].
     1189#chunk;#m1;#pcl b ofs;#v;#m2;#STORE;
     1190#chunk';#pcl';#b';#ofs';#Hvalid;
     1191ncut (∃v'. load chunk' m2 pcl' b' ofs' = Some ? v')
    11351192##[napply valid_access_load;
    11361193   napply (store_valid_access_1 … STORE … Hvalid);
    11371194##|*;#x;#Hx;
    11381195   ncases (load_store_classification chunk b ofs chunk' b' ofs')
    1139    ##[#H1;#H2;#H3;nrewrite > H1;napply load_store_similar;//;
     1196   ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2;
     1197      napply (load_compat_pointer … pcl);
     1198      ##[ nrewrite > (block_class_store … STORE b);
     1199          ncases Hvalid; //;
     1200      ##| napply (load_store_similar … STORE);//;
     1201      ##]
    11401202   ##|#H1;napply (load_store_other … STORE);
    11411203      ncases H1
     
    11441206         ##|#H2;@;@2;//]
    11451207      ##|#H2;@2;//]
    1146    ##|#H1;#H2;#H3;#H4;nrewrite < H1 in Hx;
    1147       #Hx;nrewrite > Hx;
    1148       napply eq_f;napply (load_store_overlap … STORE … Hx);/2/;
    1149    ##|#H1;#H2;#H3;nrewrite < H1 in Hx;
    1150       nrewrite < H2;#Hx;nrewrite > Hx;napply eq_f;
    1151       napply (load_store_mismatch … STORE … Hx);/2/]
     1208   ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … pcl … Hx);
     1209     ##[ nrewrite > (block_class_store … STORE b');
     1210         nrewrite > H1; nelim (store_valid_access_3 … STORE); //
     1211     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
     1212         nrewrite < H1 in Hx;#Hx;nrewrite > Hx;
     1213      napply eq_f;napply (load_store_overlap … STORE … Hx');/2/;
     1214     ##]
     1215   ##|#H1;#H2;#H3;
     1216       nlapply (load_compat_pointer … pcl … Hx);
     1217       ##[ nrewrite > (block_class_store … STORE b');
     1218           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
     1219       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
     1220           nrewrite > Hx;napply eq_f;
     1221           napply (load_store_mismatch … STORE … Hx');/2/
     1222       ##]
     1223   ##]
     1224           
    11521225##]
    11531226nqed.
     
    11831256
    11841257nlemma nextblock_alloc:
    1185   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1258  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    11861259  nextblock m2 = Zsucc (nextblock m1).
    1187 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1260#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    11881261nwhd in ALLOC:(??%%); ndestruct; //;
    11891262nqed.
    11901263
    11911264nlemma alloc_result:
    1192   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1265  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    11931266  b = nextblock m1.
    1194 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1267#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    11951268nwhd in ALLOC:(??%%); ndestruct; //;
    11961269nqed.
     
    11981271
    11991272nlemma valid_block_alloc:
    1200   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1273  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12011274  ∀b'. valid_block m1 b' → valid_block m2 b'.
    1202 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1275#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12031276#b'; nrewrite > (unfold_valid_block m1 b');
    12041277nrewrite > (unfold_valid_block m2 b');
     
    12081281
    12091282nlemma fresh_block_alloc:
    1210   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1283  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12111284  ¬(valid_block m1 b).
    1212 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1285#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12131286nrewrite > (unfold_valid_block m1 b);
    12141287nrewrite > (alloc_result … ALLOC);
     
    12171290
    12181291nlemma valid_new_block:
    1219   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1292  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12201293  valid_block m2 b.
    1221 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1294#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12221295nrewrite > (unfold_valid_block m2 b);
    12231296nrewrite > (alloc_result … ALLOC);
     
    12311304
    12321305nlemma valid_block_alloc_inv:
    1233   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1306  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12341307  ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'.
    1235 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1308#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12361309#b';
    12371310nrewrite > (unfold_valid_block m2 b');
     
    12431316
    12441317nlemma low_bound_alloc:
    1245   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1318  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12461319  ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'.
    1247 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1320#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12481321nwhd in ALLOC:(??%%); ndestruct; #b';
    12491322nrewrite > (unfold_update block_contents ????);
     
    12521325
    12531326nlemma low_bound_alloc_same:
    1254   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1327  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12551328  low_bound m2 b = lo.
    1256 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1329#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12571330nrewrite > (low_bound_alloc … ALLOC b);
    12581331nrewrite > (eqZb_z_z …);
     
    12611334
    12621335nlemma low_bound_alloc_other:
    1263   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1336  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12641337  ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'.
    1265 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1338#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12661339#b'; nrewrite > (low_bound_alloc … ALLOC b');
    12671340napply eqZb_elim; #Hb;
     
    12721345
    12731346nlemma high_bound_alloc:
    1274   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1347  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12751348  ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'.
    1276 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1349#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12771350nwhd in ALLOC:(??%%); ndestruct; #b';
    12781351nrewrite > (unfold_update block_contents ????);
     
    12811354
    12821355nlemma high_bound_alloc_same:
    1283   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1356  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12841357  high_bound m2 b = hi.
    1285 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1358#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12861359nrewrite > (high_bound_alloc … ALLOC b);
    12871360nrewrite > (eqZb_z_z …);
     
    12901363
    12911364nlemma high_bound_alloc_other:
    1292   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
     1365  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
    12931366  ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'.
    1294 #m1;#lo;#hi;#m2;#b;#ALLOC;
     1367#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
    12951368#b'; nrewrite > (high_bound_alloc … ALLOC b');
    12961369napply eqZb_elim; #Hb;
     
    13001373##] nqed.
    13011374
     1375nlemma class_alloc:
     1376  ∀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'.
     1378#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1379nwhd in ALLOC:(??%%); ndestruct; #b';
     1380ncases (eqZb b' (nextblock m1)); //;
     1381nqed.
     1382
     1383nlemma class_alloc_same:
     1384  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
     1385  blockclass m2 b = bcl.
     1386#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1387nwhd in ALLOC:(??%%); ndestruct;
     1388nrewrite > (eqZb_z_z ?); //;
     1389nqed.
     1390
     1391nlemma class_alloc_other:
     1392  ∀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'.
     1394#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1395#b'; nrewrite > (class_alloc … ALLOC b');
     1396napply eqZb_elim; #Hb;
     1397##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
     1398    napply (fresh_block_alloc … ALLOC)
     1399##| //
     1400##] nqed.
     1401
    13021402nlemma valid_access_alloc_other:
    1303   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1304   ∀chunk,b',ofs.
    1305   valid_access m1 chunk b' ofs →
    1306   valid_access m2 chunk b' ofs.
    1307 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1308 #chunk;#b';#ofs;#H;
    1309 ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;
     1403  ∀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.
     1407#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1408#chunk;#pcl;#b';#ofs;#H;
     1409ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;#Hcompat;
    13101410@;
    13111411##[ napply (valid_block_alloc … ALLOC); //
     
    13131413##| nrewrite > (high_bound_alloc_other … ALLOC b' Hvalid); //
    13141414##| //
     1415##| nrewrite > (class_alloc_other … ALLOC b' Hvalid); //;
    13151416##] nqed.
    13161417
    13171418nlemma valid_access_alloc_same:
    1318   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1319   ∀chunk,ofs.
     1419  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
     1420  ∀chunk,pcl,ofs.
    13201421  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1321   valid_access m2 chunk b ofs.
    1322 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1323 #chunk;#ofs; #Hlo; #Hhi; #Halign;
     1422  class_compat bcl pcl →
     1423  valid_access m2 chunk pcl b ofs.
     1424#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1425#chunk;#pcl;#ofs; #Hlo; #Hhi; #Halign; #Hcompat;
    13241426@;
    13251427##[ napply (valid_new_block … ALLOC)
     
    13271429##| nrewrite > (high_bound_alloc_same … ALLOC); //
    13281430##| //
     1431##| nrewrite > (class_alloc_same … ALLOC); //
    13291432##] nqed.
    13301433
     
    13341437
    13351438nlemma valid_access_alloc_inv:
    1336   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1337   ∀chunk,b',ofs.
    1338   valid_access m2 chunk b' ofs →
    1339   valid_access m1 chunk b' ofs ∨
    1340   (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs))).
    1341 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1342 #chunk;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;
     1439  ∀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)).
     1444#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1445#chunk;#pcl;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;#Hct;
    13431446nelim (valid_block_alloc_inv … ALLOC ? Hblk);#H;
    13441447##[ nrewrite < H in ALLOC ⊢ %; #ALLOC';
    13451448    nrewrite > (low_bound_alloc_same … ALLOC') in Hlo; #Hlo';
    13461449    nrewrite > (high_bound_alloc_same … ALLOC') in Hhi; #Hhi';
    1347     @2; /4/
     1450    nrewrite > (class_alloc_same … ALLOC') in Hct; #Hct;
     1451    @2; /4/;
    13481452##| @1;@;//;
    13491453  ##[ nrewrite > (low_bound_alloc_other … ALLOC ??) in Hlo; //
    13501454  ##| nrewrite > (high_bound_alloc_other … ALLOC ??) in Hhi; //
     1455  ##| nrewrite > (class_alloc_other … ALLOC ??) in Hct; //
    13511456  ##]
    13521457##] nqed.
    13531458
    13541459ntheorem load_alloc_unchanged:
    1355   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1356   ∀chunk,b',ofs.
     1460  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
     1461  ∀chunk,pcl,b',ofs.
    13571462  valid_block m1 b' →
    1358   load chunk m2 b' ofs = load chunk m1 b' ofs.
    1359 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1360 #chunk;#b';#ofs;#H;nwhd in ⊢ (??%%);
    1361 ncases (in_bounds m2 chunk b' ofs); #H';
    1362 ##[ nelim (valid_access_alloc_inv … ALLOC ??? H');
     1463  load chunk m2 pcl b' ofs = load chunk m1 pcl b' ofs.
     1464#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1465#chunk;#pcl;#b';#ofs;#H;nwhd in ⊢ (??%%);
     1466ncases (in_bounds m2 chunk pcl b' ofs); #H';
     1467##[ nelim (valid_access_alloc_inv … ALLOC ???? H');
    13631468  ##[ #H''; (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
    13641469  nrewrite > (in_bounds_true ???? ??? H''); *) nrewrite > (in_bounds_true … ? (option val) ?? H'');
    13651470      nwhd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *)
    1366        nwhd in ALLOC:(??%%); ndestruct;
    1367       nrewrite > (update_o block_contents ?????);
    1368       ##[ // ##| napply sym_neq; napply (valid_not_valid_diff … H); napply (fresh_block_alloc … );//; ##]
     1471      ncut (b' ≠ b);
     1472      ##[ napply (valid_not_valid_diff … H); napply (fresh_block_alloc … ALLOC);
     1473      ##| nwhd in ALLOC:(??%%); ndestruct;
     1474          nrewrite > (update_o block_contents ?????); /2/;
     1475      ##]
    13691476  ##| *;*;#A;#B;#C; nrewrite < A in ALLOC ⊢ %; #ALLOC;
    13701477      napply False_ind; napply (absurd ? H); napply (fresh_block_alloc … ALLOC)
    13711478  ##]
    1372 ##| ncases (in_bounds m1 chunk b' ofs); #H''; nwhd in ⊢ (??%%); //;
     1479##| ncases (in_bounds m1 chunk pcl b' ofs); #H''; nwhd in ⊢ (??%%); //;
    13731480    napply False_ind; napply (absurd ? ? H'); napply (valid_access_alloc_other … ALLOC); //
    13741481##] nqed.
    13751482 
    13761483ntheorem load_alloc_other:
    1377   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1378   ∀chunk,b',ofs,v.
    1379   load chunk m1 b' ofs = Some ? v →
    1380   load chunk m2 b' ofs = Some ? v.
    1381 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1382 #chunk;#b';#ofs;#v;#H;
    1383 nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); /3/;
     1484  ∀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.
     1488#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1489#chunk;#pcl;#b';#ofs;#v;#H;
     1490nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); ncases (load_valid_access … H); //;
    13841491nqed.
    13851492
    13861493ntheorem load_alloc_same:
    1387   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1388   ∀chunk,ofs,v.
    1389   load chunk m2 b ofs = Some ? v →
     1494  ∀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 →
    13901497  v = Vundef.
    1391 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1392 #chunk;#ofs;#v;#H;
     1498#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1499#chunk;#pcl;#ofs;#v;#H;
    13931500nelim (load_inv … H); #H0; #H1; nrewrite > H1;
    13941501 nwhd in ALLOC:(??%%); (* XXX ndestruct; ??? *) napply (pairdisc_elim … ALLOC);
    13951502 nwhd in ⊢ (??%% → ?);#e0;nrewrite < e0 in ⊢ (%→?);
    13961503 nwhd in ⊢ (??%% → ?);#e1;
    1397 nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi) ?);
     1504nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi bcl) ?);
    13981505nnormalize; ncases chunk; //;
    13991506nqed.
    14001507
    14011508ntheorem load_alloc_same':
    1402   ∀m1,lo,hi,m2,b.alloc m1 lo hi = 〈m2,b〉 →
    1403   ∀chunk,ofs.
     1509  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
     1510  ∀chunk,pcl,ofs.
    14041511  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
    1405   load chunk m2 b ofs = Some ? Vundef.
    1406 #m1;#lo;#hi;#m2;#b;#ALLOC;
    1407 #chunk;#ofs;#Hlo;#Hhi;#Hal;
    1408 ncut (∃v. load chunk m2 b ofs = Some ? v);
    1409 ##[ napply valid_access_load; @; /2/;
    1410   ##[ nrewrite > (low_bound_alloc_same … ALLOC); //
     1512  class_compat bcl pcl →
     1513  load chunk m2 pcl b ofs = Some ? Vundef.
     1514#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
     1515#chunk;#pcl;#ofs;#Hlo;#Hhi;#Hal;#Hct;
     1516ncut (∃v. load chunk m2 pcl b ofs = Some ? v);
     1517##[ napply valid_access_load; @; //;
     1518  ##[ napply (valid_new_block … ALLOC);
     1519  ##| nrewrite > (low_bound_alloc_same … ALLOC); //
    14111520  ##| nrewrite > (high_bound_alloc_same … ALLOC); //
     1521  ##| nrewrite > (class_alloc_same … ALLOC); //
    14121522  ##]
    14131523##| *; #v;#LOAD; nrewrite > LOAD; napply eq_f;
     
    14701580nqed.
    14711581
     1582nlemma class_free:
     1583  ∀m,bf,b. b ≠ bf → blockclass (free m bf) b = blockclass m b.
     1584#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
     1585nrewrite > (update_o block_contents …); //; napply sym_neq; //;
     1586nqed.
     1587
    14721588nlemma valid_access_free_1:
    1473   ∀m,bf,chunk,b,ofs.
    1474   valid_access m chunk b ofs → b ≠ bf →
    1475   valid_access (free m bf) chunk b ofs.
    1476 #m;#bf;#chunk;#b;#ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hneq;
     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;
    14771593@; //;
    14781594##[ napply valid_block_free_1; //
    14791595##| nrewrite > (low_bound_free … Hneq); //
    14801596##| nrewrite > (high_bound_free … Hneq); //
     1597##| nrewrite > (class_free … Hneq); //
    14811598##] nqed.
    14821599
    14831600nlemma valid_access_free_2:
    1484   ∀m,bf,chunk,ofs. ¬(valid_access (free m bf) chunk bf ofs).
    1485 #m;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;
     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;
    14861603nwhd in Hlo:(?%?);nwhd in Hlo:(?(?(?%?))?); nrewrite > (update_s block_contents …) in Hlo;
    14871604nwhd in Hhi:(??%);nwhd in Hhi:(??(?(?%?))); nrewrite > (update_s block_contents …) in Hhi;
     
    14941611
    14951612nlemma valid_access_free_inv:
    1496   ∀m,bf,chunk,b,ofs.
    1497   valid_access (free m bf) chunk b ofs →
    1498   valid_access m chunk b ofs ∧ b ≠ bf.
    1499 #m;#bf;#chunk;#b;#ofs; nelim (decidable_eq_Z_Type b bf);
     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);
    15001617##[ #e; nrewrite > e;
    15011618    #H; napply False_ind; napply (absurd ? H (valid_access_free_2 …));
    15021619##| #ne; *; nrewrite > (low_bound_free … ne);
    15031620    nrewrite > (high_bound_free … ne);
    1504     #Hval; #Hlo; #Hhi; #Hal;
    1505     @; ##[ @; //; napply (valid_block_free_2 … Hval); ##| /2/ ##]
     1621    nrewrite > (class_free … ne);
     1622    #Hval; #Hlo; #Hhi; #Hal; #Hct;
     1623    @; ##[ @; /2/; ##| /2/ ##]
    15061624##] nqed.
    15071625
    15081626ntheorem load_free:
    1509   ∀m,bf,chunk,b,ofs.
     1627  ∀m,bf,chunk,pcl,b,ofs.
    15101628  b ≠ bf →
    1511   load chunk (free m bf) b ofs = load chunk m b ofs.
    1512 #m;#bf;#chunk;#b;#ofs;#ne; nwhd in ⊢ (??%%);
    1513 nelim (in_bounds m chunk b ofs);
    1514 ##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ???? (option val) ???);
     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 ⊢ (??%%);
     1631nelim (in_bounds m chunk pcl b ofs);
     1632##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ????? (option val) ???);
    15151633  ##[ nwhd in ⊢ (??(??(??(???(?(?%?)))))?); nrewrite > (update_o block_contents …); //;
    15161634      napply sym_neq; //
    15171635  ##| napply valid_access_free_1; //; napply ne;
    15181636  ##]
    1519 ##| nelim (in_bounds (free m bf) chunk b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
     1637##| nelim (in_bounds (free m bf) chunk pcl b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
    15201638    #H;#H'; napply False_ind; napply (absurd ? ? H');
    15211639    nelim (valid_access_free_inv …H); //;
     
    15451663
    15461664nlemma valid_access_free_list:
    1547   ∀chunk,b,ofs,m,bl.
    1548   valid_access m chunk b ofs → ¬in_list ? b bl →
    1549   valid_access (free_list m bl) chunk b ofs.
    1550 #chunk; #b; #ofs; #m; #bl; nelim bl;
    1551 ##[ nwhd in ⊢ (?→?→(?%???)); //
     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;
     1669##[ nwhd in ⊢ (?→?→(?%????)); //
    15521670##| #h;#t;#IH;#H;#notin; nrewrite > (unfold_free_list m h t); napply valid_access_free_1;
    15531671    ##[ napply IH; //; napply (not_to_not ??? notin); #Ht; napply (in_list_cons … Ht)
     
    15561674
    15571675nlemma valid_access_free_list_inv:
    1558   ∀chunk,b,ofs,m,bl.
    1559   valid_access (free_list m bl) chunk b ofs →
    1560   ¬in_list ? b bl ∧ valid_access m chunk b ofs.
    1561 #chunk; #b; #ofs; #m; #bl; nelim bl;
    1562 ##[ nwhd in ⊢ ((?%???)→?); #H; @; //
     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;
     1680##[ nwhd in ⊢ ((?%????)→?); #H; @; //
    15631681##| #h;#t;#IH; nrewrite > (unfold_free_list m h t); #H;
    15641682    nelim (valid_access_free_inv … H); #H';#ne;
     
    15711689
    15721690nlemma valid_pointer_valid_access:
    1573   ∀m,b,ofs.
    1574   valid_pointer m b ofs = true ↔ valid_access m Mint8unsigned b ofs.
    1575 #m;#b;#ofs;nwhd in ⊢ (?(??%?)?); @;
     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 ⊢ (?(??%?)?); @;
    15761694##[ #H;
    15771695    nlapply (andb_true_l … H); #H';
    1578     nlapply (andb_true_l … H'); #H1;
    1579     nlapply (andb_true_r … H'); #H2;
    1580     nlapply (andb_true_r … H); #H3;
     1696    nlapply (andb_true_l … H'); #H'';
     1697    nlapply (andb_true_l … H''); #H1;
     1698    nlapply (andb_true_r … H''); #H2;
     1699    nlapply (andb_true_r … H'); #H3;
     1700    nlapply (andb_true_r … H); #H4;
    15811701    @;
    15821702    ##[ nrewrite > (unfold_valid_block m b); napply (Zltb_true_to_Zlt … H1)
     
    15841704    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    15851705    ##| ncases ofs; /2/;
     1706    ##| nwhd in H4:(??%?); nelim (class_compat_dec (blockclass m b) pcl) in H4;
     1707        ##[ //; ##| #Hn e; nwhd in e:(??%%); ndestruct ##]
    15861708    ##]
    1587 ##| *; #Hval;#Hlo;#Hhi;#Hal;
     1709##| *; #Hval;#Hlo;#Hhi;#Hal;#Hct;
    15881710    nrewrite > (Zlt_to_Zltb_true … Hval);
    15891711    nrewrite > (Zle_to_Zleb_true … Hlo);
    15901712    nwhd in Hhi:(?(??%)?); nrewrite > (Zlt_to_Zltb_true … ?);
    1591     //; (* arith *) napply daemon
    1592 ##] nqed.
     1713    ##[ nwhd in ⊢ (??%?); nelim (class_compat_dec (blockclass m b) pcl);
     1714      ##[ //;
     1715      ##| #Hct'; napply False_ind; napply (absurd … Hct Hct');
     1716      ##]
     1717    ##| (* arith *) napply daemon
     1718    ##]
     1719##]
     1720 nqed.
    15931721
    15941722ntheorem valid_pointer_alloc:
    1595   ∀m1,m2: mem. ∀lo,hi: Z. ∀b,b': block. ∀ofs: Z.
    1596   alloc m1 lo hi = 〈m2, b'〉 →
    1597   valid_pointer m1 b ofs = true →
    1598   valid_pointer m2 b ofs = true.
    1599 #m1;#m2;#lo;#hi;#b;#b';#ofs;#ALLOC;#VALID;
    1600 nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
    1601 napply (proj2 ?? (valid_pointer_valid_access ???));
     1723  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,pcl. ∀b,b': block. ∀ofs: Z.
     1724  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;
     1728nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
     1729napply (proj2 ?? (valid_pointer_valid_access ????));
    16021730napply (valid_access_alloc_other … ALLOC … Hval);
    16031731nqed.
    16041732
    16051733ntheorem valid_pointer_store:
    1606   ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
    1607   store chunk m1 b' ofs' v = Some ? m2 →
    1608   valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true.
    1609 #chunk;#m1;#m2;#b;#b';#ofs;#ofs';#v;#STORE;#VALID;
    1610 nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
    1611 napply (proj2 ?? (valid_pointer_valid_access ???));
     1734  ∀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;
     1739nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
     1740napply (proj2 ?? (valid_pointer_valid_access ????));
    16121741napply (store_valid_access_1 … STORE … Hval);
    16131742nqed.
    16141743
    16151744(* * * Generic injections between memory states. *)
    1616 
     1745(*
    16171746(* Section GENERIC_INJECT. *)
    16181747
     
    16561785
    16571786(*Hint Resolve valid_access_inj: mem.*)
    1658 
     1787*)
    16591788(* FIXME: can't use ndestruct below *)
    16601789nlemma grumpydestruct : ∀A,v. None A = Some A v → False.
    16611790#A;#v;#H;ndestruct;
    16621791nqed.
    1663 
     1792(*
    16641793nlemma store_unmapped_inj: ∀val_inj.
    1665   ∀mi,m1,m2,b,ofs,v,chunk,m1'.
     1794  ∀mi,m1,m2,pcl,b,ofs,v,chunk,m1'.
    16661795  mem_inj val_inj mi m1 m2 →
    16671796  mi b = None ? →
    1668   store chunk m1 b ofs v = Some ? m1' →
     1797  store chunk m1 pcl b ofs v = Some ? m1' →
    16691798  mem_inj val_inj mi m1' m2.
    16701799#val_inj;
    1671 #mi;#m1;#m2;#b;#ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
     1800#mi;#m1;#m2;#pcl b ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
    16721801nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
    16731802ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
     
    16781807
    16791808nlemma store_outside_inj: ∀val_inj.
    1680   ∀mi,m1,m2,chunk,b,ofs,v,m2'.
     1809  ∀mi,m1,m2,chunk,pcl,b,ofs,v,m2'.
    16811810  mem_inj val_inj mi m1 m2 →
    16821811  (∀b',delta.
     
    16841813    high_bound m1 b' + delta ≤ ofs
    16851814    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
    1686   store chunk m2 b ofs v = Some ? m2' →
     1815  store chunk m2 pcl b ofs v = Some ? m2' →
    16871816  mem_inj val_inj mi m1 m2'.
    16881817#val_inj;
    1689 #mi;#m1;#m2;#chunk;#b;#ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
     1818#mi;#m1;#m2;#chunk;#pcl b ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
    16901819nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
    16911820nlapply (Hinj … Hmi0 Hload);*;#v2;*;#LOAD2;#VINJ;
     
    17121841  (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2)
    17131842      (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)).
    1714 
     1843*)
    17151844(* FIXME *)
    17161845nlemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2.
     
    17201849#A;#B;#x1;#y1;#x2;#y2;#H;ndestruct;/2/;
    17211850nqed.
    1722 
     1851(*
    17231852nlemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
    17241853  ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'.
     
    20602189  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
    20612190  extends m1 m2 →
    2062   load chunk m1 b ofs = Some ? v →
    2063   load chunk m2 b ofs = Some ? v.
    2064 #chunk;#m1;#m2;#b;#ofs;#v;
     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;
    20652194*;#Hnext;#Hinj;#LOAD;
    20662195nlapply (Hinj … LOAD); ##[ nnormalize; // ##| ##2,3: ##]
     
    20722201  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
    20732202  extends m1 m2 →
    2074   store chunk m1 b ofs v = Some ? m1' →
    2075   ∃m2'. store chunk m2 b ofs v = Some ? m2' ∧ 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'.
    20762205#chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1;
    20772206nlapply (store_mapped_inj … Hinj ?? STORE1 ?);
     
    20952224  extends m1 m2 →
    20962225  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
    2097   store chunk m2 b ofs v = Some ? m2' →
     2226  store chunk m2 pcl b ofs v = Some ? m2' →
    20982227  extends m1 m2'.
    20992228#chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @;
     
    21092238ntheorem valid_pointer_extends:
    21102239  ∀m1,m2,b,ofs.
    2111   extends m1 m2 → valid_pointer m1 b ofs = true →
    2112   valid_pointer m2 b ofs = true.
     2240  extends m1 m2 → valid_pointer m1 pcl b ofs = true →
     2241  valid_pointer m2 pcl b ofs = true.
    21132242#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
    21142243nrewrite < (Zplus_z_OZ ofs);
     
    21402269nlemma load_lessdef:
    21412270  ∀m1,m2,chunk,b,ofs,v1.
    2142   lessdef m1 m2 → load chunk m1 b ofs = Some ? v1 →
    2143   ∃v2. load chunk m2 b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
     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.
    21442273#m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0;
    21452274nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ##| ##2,3:##skip ##]
     
    21652294  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
    21662295  lessdef m1 m2 → Val_lessdef v1 v2 →
    2167   store chunk m1 b ofs v1 = Some ? m1' →
    2168   ∃m2'. store chunk m2 b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
     2296  store chunk m1 pcl b ofs v1 = Some ? m1' →
     2297  ∃m2'. store chunk m2 pcl b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
    21692298#m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1';
    21702299*;#Hnext;#Hinj;#Hvless;#STORE0;
     
    22572386nlemma valid_pointer_lessdef:
    22582387  ∀m1,m2,b,ofs.
    2259   lessdef m1 m2 → valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true.
     2388  lessdef m1 m2 → valid_pointer m1 pcl b ofs = true → valid_pointer m2 pcl b ofs = true.
    22602389#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
    22612390nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //;
     
    23942523  mem_inject f m1 m2 →
    23952524  valid_pointer m1 b (signed ofs) = true →
    2396   val_inject f (Vptr b ofs) (Vptr b' ofs') →
     2525  val_inject f (Vptr pcl b ofs) (Vptr b' ofs') →
    23972526  valid_pointer m2 b' (signed ofs') = true.
    23982527#f;#m1;#m2;#b;#ofs;#b';#ofs';
     
    34333562##]
    34343563nqed.
    3435 
     3564*)
    34363565(* ** Relation between signed and unsigned loads and stores *)
    34373566
     
    34423571
    34433572nremark in_bounds_equiv:
    3444   ∀chunk1,chunk2,m,b,ofs.∀A:Type.∀a1,a2: A.
     3573  ∀chunk1,chunk2,m,pcl,b,ofs.∀A:Type.∀a1,a2: A.
    34453574  size_chunk chunk1 = size_chunk chunk2 →
    3446   (match in_bounds m chunk1 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
    3447   (match in_bounds m chunk2 b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
    3448 #chunk1;#chunk2;#m;#b;#ofs;#A;#a1;#a2;#Hsize;
    3449 nelim (in_bounds m chunk1 b ofs);
     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;
     3578nelim (in_bounds m chunk1 pcl b ofs);
    34503579##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //;
    34513580    napply valid_access_compat; //;
    3452 ##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 b ofs); //;
     3581##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 pcl b ofs); //;
    34533582    #H'; napply False_ind; napply (absurd ?? H);
    34543583    napply valid_access_compat; //;
     
    34593588  storev Mint8signed m a v = storev Mint8unsigned m a v.
    34603589#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
    3461 #b;#ofs; nwhd in ⊢ (??%%);
     3590#pcl b ofs; nwhd in ⊢ (??%%);
    34623591nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //;
    34633592nqed.
     
    34673596  storev Mint16signed m a v = storev Mint16unsigned m a v.
    34683597#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
    3469 #b;#ofs; nwhd in ⊢ (??%%);
     3598#pcl b ofs; nwhd in ⊢ (??%%);
    34703599nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //;
    34713600nqed.
     
    34803609  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
    34813610#m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //;
    3482 #b;#ofs; nwhd in ⊢ (??%(????%));
     3611#pcl b ofs; nwhd in ⊢ (??%(????%));
    34833612nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //;
    3484 nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;
     3613nelim (in_bounds m Mint8unsigned pcl b (signed ofs)); /2/;
    34853614#H; nwhd in ⊢ (??%%);
    34863615nelim (getN 0 (signed ofs) (contents (blocks m b)));
Note: See TracChangeset for help on using the changeset viewer.