Changeset 496


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

First pass at moving regions to block type.

Location:
Deliverables/D3.1/C-semantics
Files:
7 edited

Legend:

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

    r487 r496  
    170170         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
    171171         | _ ⇒ Error ? ];
    172     if is_pointer_compat (block_space m b) s'
     172    if is_pointer_compat (block_region m b) s'
    173173    then OK ? (Vptr s' b ofs)
    174174    else Error ?
     
    184184
    185185definition load_value_of_type' ≝
    186 λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair psp loc ⇒
    187   load_value_of_type ty m psp loc ofs ] ].
     186λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair r loc ⇒
     187  load_value_of_type ty m r loc ofs ] ].
    188188
    189189(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    258258  [ Evar id ⇒
    259259      match (get … id en) with
    260       [ None ⇒ do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉 (* global *)
     260      [ None ⇒ do 〈r,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈r,〈r,l〉〉,zero〉,E0〉 (* global *)
    261261      | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
    262262      ]
     
    654654  do ge ← globalenv Genv ?? p;
    655655  do m0 ← init_mem Genv ?? p;
    656   do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    657   do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? it | inr _ ⇒ None ? ]);
     656  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    658657  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    659658  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r487 r496  
    4040
    4141lemma is_pointer_compat_true: ∀m,b,sp.
    42   pointer_compat (block_space m b) sp →
    43   is_pointer_compat (block_space m b) sp = true.
     42  pointer_compat (block_region m b) sp →
     43  is_pointer_compat (block_region m b) sp = true.
    4444#m #b #sp #H whd in ⊢ (??%?);
    45 elim (pointer_compat_dec (block_space m b) sp);
     45elim (pointer_compat_dec (block_region m b) sp);
    4646[ //
    4747| #H' @False_ind @(absurd … H H')
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r487 r496  
    102102            #e <e
    103103            whd in match (is_pointer_compat ??) in e''';
    104             cases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat #e'''
     104            cases (pointer_compat_dec (block_region m b) s') in e'''; #Hcompat #e'''
    105105            whd in e''':(??%?); destruct (e'''); /2/
    106106        ]
     
    514514@bind_OK #m #Em
    515515@opt_bind_OK #x cases x; #sp #b #esb
    516 @opt_bind_OK #u #ecode
    517516@opt_bind_OK #f #ef
    518 cases sp in esb ecode; #esb #ecode whd in ecode:(??%%); [ 1,2,3,4,5: destruct (ecode); ]
    519517whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
    520518qed.
  • Deliverables/D3.1/C-semantics/Csem.ma

    r487 r496  
    169169      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    170170        [ Vptr pcl2 b2 ofs2 ⇒
    171           if eqZb b1 b2 then
     171          if eq_block b1 b2 then
    172172            if eq (repr (sizeof ty)) zero then None ?
    173173            else Some ? (Vint (divu (sub ofs1 ofs2) (repr (sizeof ty))))
     
    326326          if valid_pointer m r1 b1 (signed ofs1)
    327327          ∧ valid_pointer m r2 b2 (signed ofs2) then
    328             if eqZb b1 b2
     328            if eq_block b1 b2
    329329            then Some ? (of_bool (cmp c ofs1 ofs2))
    330330            else sem_cmp_mismatch c
     
    432432      type_region ty r →
    433433      type_region ty' r' →
    434       pointer_compat (block_space m b) r' →
     434      pointer_compat (block_region m b) r' →
    435435      cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs)
    436436  | cast_ip_z: ∀m,sz,sg,ty',r.
     
    567567  | eval_Econst_float:   ∀f,ty.
    568568      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
    569   | eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr.
    570       eval_lvalue ge e m (Expr a ty) psp loc ofs tr →
    571       load_value_of_type ty m psp loc ofs = Some ? v →
     569  | eval_Elvalue: ∀a,ty,r,loc,ofs,v,tr.
     570      eval_lvalue ge e m (Expr a ty) r loc ofs tr →
     571      load_value_of_type ty m r loc ofs = Some ? v →
    572572      eval_expr ge e m (Expr a ty) v tr
    573   | eval_Eaddrof: ∀a,ty,psp,loc,ofs,tr.
    574       eval_lvalue ge e m a psp loc ofs tr →
    575       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) tr
     573  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
     574      eval_lvalue ge e m a r loc ofs tr →
     575      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr r loc ofs) tr
    576576  | eval_Esizeof: ∀ty',ty.
    577577      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    623623      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)
    624624
    625 (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
     625(* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]
    626626  in l-value position.  The result is the memory location [b, ofs]
    627   that contains the value of the expression [a]. *)
     627  that contains the value of the expression [a].  The memory location should
     628  be representable in a pointer of region r. *)
    628629
    629630with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
     
    631632      (* XXX notation? e!id*) get ??? id e = Some ? l →
    632633      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    633   | eval_Evar_global: ∀id,sp,l,ty.
     634  | eval_Evar_global: ∀id,r,l,ty.
    634635      (* XXX e!id *) get ??? id e = None ? →
    635       find_symbol ?? ge id = Some ? 〈sp,l〉 →
    636       eval_lvalue ge e m (Expr (Evar id) ty) sp l zero E0
    637   | eval_Ederef: ∀a,ty,psp,l,ofs,tr.
    638       eval_expr ge e m a (Vptr psp l ofs) tr →
    639       eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs tr
    640  | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta,tr.
    641       eval_lvalue ge e m a psp l ofs tr →
     636      find_symbol ?? ge id = Some ? 〈r,l〉 →
     637      eval_lvalue ge e m (Expr (Evar id) ty) r 〈r,l〉 zero E0
     638  | eval_Ederef: ∀a,ty,r,l,ofs,tr.
     639      eval_expr ge e m a (Vptr r l ofs) tr →
     640      eval_lvalue ge e m (Expr (Ederef a) ty) r l ofs tr
     641 | eval_Efield_struct:   ∀a,i,ty,r,l,ofs,id,fList,delta,tr.
     642      eval_lvalue ge e m a r l ofs tr →
    642643      typeof a = Tstruct id fList →
    643644      field_offset i fList = OK ? delta →
    644       eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) tr
    645  | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList,tr.
    646       eval_lvalue ge e m a psp l ofs tr →
     645      eval_lvalue ge e m (Expr (Efield a i) ty) r l (add ofs (repr delta)) tr
     646 | eval_Efield_union:   ∀a,i,ty,r,l,ofs,id,fList,tr.
     647      eval_lvalue ge e m a r l ofs tr →
    647648      typeof a = Tunion id fList →
    648       eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr.
     649      eval_lvalue ge e m (Expr (Efield a i) ty) r l ofs tr.
    649650
    650651let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
     
    14791480      globalenv Genv ?? p = OK ? ge →
    14801481      init_mem Genv ?? p = OK ? m0 →
    1481       find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉
     1482      find_symbol ?? ge (prog_main ?? p) = Some ? b
    14821483      find_funct_ptr ?? ge b = Some ? f →
    14831484      initial_state p (Callstate f (nil ?) Kstop m0).
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r487 r496  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type[0]. genv_t F → ident → option (region × block)(*;
     68  find_symbol: ∀F: Type[0]. genv_t F → ident → option block (*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
     
    317317  functions: block → option F;
    318318  nextfunction: Z;
    319   symbols: ident → option (region × block)
     319  symbols: ident → option block
    320320}.
    321321(*
     
    342342λF,name_fun,g.
    343343  let b ≝ nextfunction ? g in
    344   mk_genv F ((*ZMap.set*) λb'. if eqZb b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
     344  mk_genv F ((*ZMap.set*) λb'. if eq_block 〈Code,b〉 b' then (Some ? (\snd name_fun)) else (functions ? g b'))
    345345            (Zpred b)
    346346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
    347347
    348 definition add_symbol : ∀F:Type[0]. ident → region → block → genv F → genv F ≝
    349 λF,name,bsp,b,g.
     348definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝
     349λF,name,b,g.
    350350  mk_genv F (functions ? g)
    351351            (nextfunction ? g)
    352             ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]).
     352            ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? b | inr _ ⇒ symbols ? g i ]).
    353353(*
    354354Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
     
    398398(* init *)
    399399
    400 definition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
    401 λF,ge,m,r,b,p,id.
     400definition store_init_data : ∀F.genv F → mem → block → Z → init_data → option mem ≝
     401λF,ge,m,b,p,id.
     402  (* store checks that the address came from something capable of representing
     403     addresses of the memory region in question - here there are no real
     404     pointers, so use the real region. *)
     405  let r ≝ \fst b in
    402406  match id with
    403407  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     
    409413      match (*find_symbol ge symb*) symbols ? ge symb with
    410414      [ None ⇒ None ?
    411       | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' (snd ?? b') ofs)
     415      | Some b' ⇒ store (Mpointer r') m r b p (Vptr r' b' ofs)
    412416      ]
    413417  | Init_space n ⇒ Some ? m
     
    427431
    428432let rec store_init_data_list (F:Type[0]) (ge:genv F)
    429                               (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data)
     433                              (m: mem) (b: block) (p: Z) (idl: list init_data)
    430434                              on idl : option mem ≝
    431435  match idl with
    432436  [ nil ⇒ Some ? m
    433437  | cons id idl' ⇒
    434       match store_init_data F ge m r b p id with
     438      match store_init_data F ge m b p id with
    435439      [ None ⇒ None ?
    436       | Some m' ⇒ store_init_data_list F ge m' r b (p + size_init_data id) idl'
     440      | Some m' ⇒ store_init_data_list F ge m' b (p + size_init_data id) idl'
    437441      ]
    438442  ].
     
    463467
    464468definition alloc_init_data : mem → list init_data → region → mem × block ≝
    465   λm,i_data,bcl.
    466   〈mk_mem (update ? (nextblock m)
    467                  (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef) bcl)
     469  λm,i_data,r.
     470  〈mk_mem (update_block ? 〈r, nextblock m〉
     471                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    468472                 (blocks m))
    469473         (Zsucc (nextblock m))
    470474         (succ_nextblock_pos m),
    471    (nextblock m)〉.
     475   〈r, nextblock m〉〉.
    472476
    473477(* init *)
     
    484488        do 〈g,st〉 ← g_st;
    485489        match alloc_init_data st init r with [ pair st' b ⇒
    486           let g' ≝ add_symbol ? id r b g in
    487           do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init);
     490          let g' ≝ add_symbol ? id b g in
     491          do st'' ← opt_to_res ? (store_init_data_list F g' st' b OZ init);
    488492            OK ? 〈g', st''〉
    489493        ] ] ] ])
  • Deliverables/D3.1/C-semantics/Mem.ma

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

    r487 r496  
    2424include "basics/logic.ma".
    2525
    26 definition block ≝ Z.
    27 (*definition eq_block ≝ zeq.*)
     26definition block ≝ region × Z.
     27
     28definition eq_block ≝
     29λb1,b2.
     30match b1 with [ pair r1 i1 ⇒
     31match b2 with [ pair r2 i2 ⇒
     32  eq_region r1 r2 ∧ eqZb i1 i2
     33] ].
     34
     35lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
     36  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
     37  P (eq_block b1 b2).
     38#P * #r1 #i1 * #r2 #i2 #H1 #H2
     39whd in ⊢ (?%) @eq_region_elim #H3
     40[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
     41| @H2 % #E destruct elim H3 /2/
     42] qed.
    2843
    2944(* * A value is either:
     
    201216    [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
    202217    | Vptr pty2 b2 ofs2 ⇒
    203         if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
     218        if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    204219    | _ ⇒ Vundef ]
    205220  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     
    372387  | Vptr r1 b1 ofs1 ⇒ match v2 with
    373388    [ Vptr r2 b2 ofs2 ⇒
    374         if eqZb b1 b2
     389        if eq_block b1 b2
    375390        then of_bool (cmp c ofs1 ofs2)
    376391        else cmp_mismatch c
     
    391406  | Vptr r1 b1 ofs1 ⇒ match v2 with
    392407    [ Vptr r2 b2 ofs2 ⇒
    393         if eqZb b1 b2
     408        if eq_block b1 b2
    394409        then of_bool (cmpu c ofs1 ofs2)
    395410        else cmp_mismatch c
Note: See TracChangeset for help on using the changeset viewer.