Changeset 125


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

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

Location:
C-semantics
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r24 r125  
    104104  | Mfloat64 : memory_chunk.       (*r 64-bit double-precision float *)
    105105
     106(* Memory spaces *)
     107
     108ninductive memory_space : Type ≝
     109  | Any : memory_space
     110  | Data : memory_space
     111  | IData : memory_space
     112  | XData : memory_space
     113  | Code : memory_space.
     114
    106115(* * Initialization data for global variables. *)
    107116
     
    130139  prog_funct: list (ident × F);
    131140  prog_main: ident;
    132   prog_vars: list (ident × (list init_data) × V)
     141  prog_vars: list (ident × (list init_data) × memory_space × V)
    133142}.
    134143
     
    137146
    138147ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
    139   map ?? (λx: ident × (list init_data) × V. fst ?? (fst ?? x)) (prog_vars ?? p).
     148  map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? x)) (prog_vars ?? p).
    140149(*
    141150(** * Generic transformations over programs *)
  • C-semantics/CexecIO.ma

    r124 r125  
    223223    p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
    224224    s' ← match ty' with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];:
    225     if is_class_compat (blockclass m b) (ptr_spc_cls s')
    226     then OK ? (Vptr (ptr_spc_cls s') b ofs)
     225    if is_pointer_compat (block_space m b) s'
     226    then OK ? (Vptr s' b ofs)
    227227    else Error ?)
    228228  (* XXX: maybe should allow some Tint? *)
     
    239239          nwhd in e:(??%?); ndestruct; //;
    240240      ##| #Hty' Hty;
    241           nwhd in match (is_class_compat ??) in ⊢ %;
    242           ncases (class_compat_dec (blockclass m c1) (ptr_spc_cls s')); #Hcompat;
     241          nwhd in match (is_pointer_compat ??) in ⊢ %;
     242          ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
    243243          nwhd; /2/;
    244244      ##]
     
    247247
    248248ndefinition load_value_of_type' ≝
    249 λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒
    250   load_value_of_type ty m pcl loc ofs ] ].
     249λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
     250  load_value_of_type ty m psp loc ofs ] ].
    251251
    252252(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    305305  ]
    306306]
    307 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:ptr_class × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     307and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    308308  match e' with
    309309  [ Evar id ⇒
    310310      match (get … id en) with
    311       [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈Universal (* XXX *),l〉,zero〉) (* global *)
    312       | Some bl ⇒ match bl with [ mk_pair bcl loc ⇒ Some ? (OK ? 〈〈blk_ptr_cls bcl,loc〉,zero〉) ] (* local *)
     311      [ None ⇒ Some ? (〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈sp,l〉,zero〉) (* global *)
     312      | Some loc ⇒ Some ? (OK ? 〈〈Any,loc〉,zero〉) (* local *)
    313313      ]
    314314  | Ederef a ⇒ Some ? (
    315315      v ← exec_expr ge en m a;:
    316316      match v with
    317       [ Vptr pcl l ofs ⇒ OK ? 〈〈pcl,l〉,ofs〉
     317      [ Vptr sp l ofs ⇒ OK ? 〈〈sp,l〉,ofs〉
    318318      | _ ⇒ Error ?
    319319      ])
     
    331331  | _ ⇒ Some ? (Error ?)
    332332  ]
    333 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:ptr_class × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
     333and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝
    334334match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    335335nwhd;
    336 ##[ //
    337 ##| //
     336##[ ##1,2: //
    338337##| ##3,4:
    339     napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #pcl loc ofs H;
     338    napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs H;
    340339    napply opt_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
    341 ##| napply sig_bind2_OK; #x; ncases x; #pcl loc ofs H;
     340##| napply sig_bind2_OK; #x; ncases x; #sp loc ofs H;
    342341    nwhd; napply eval_Eaddrof; //;
    343342##| napply sig_bind_OK; #v1 Hv1;
     
    374373    ##]
    375374##| //
    376 ##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #pcl l ofs H;
     375##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs H;
    377376    napply opt_OK; #v ev; napply (eval_Elvalue … H ev);
    378377##| //
    379378##| //
    380 ##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
    381 ##| napply eval_Evar_local; nrewrite < c6; /2/
    382 ##| napply sig_bind_OK; #v; ncases v; //; #pcl l ofs Hv; nwhd;
     379##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
     380##| napply (eval_Evar_local … c3);
     381##| napply sig_bind_OK; #v; ncases v; //; #sp l ofs Hv; nwhd;
    383382    napply eval_Ederef; //
    384383##| ##19,20,21,22,23,24,25,26,27,28,29,30,31,32: //
    385 ##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
     384##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    386385    napply bind_OK; #delta Hdelta;
    387386    napply (eval_Efield_struct … H c5 Hdelta);
    388 ##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
     387##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    389388    napply (eval_Efield_union … H c5);
    390389##| //
     
    414413| cons h vars ⇒
    415414  match h with [ mk_pair id ty ⇒
    416     match alloc m 0 (sizeof ty) UnspecifiedB with [ mk_pair m1 b1 ⇒
    417       match exec_alloc_variables (set … id 〈UnspecifiedB,b1〉 en) m1 vars with
     415    match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
     416      match exec_alloc_variables (set … id b1 en) m1 vars with
    418417      [ sig_intro r p ⇒ r ]
    419 ]]]. nwhd; //;
    420 nelim (exec_alloc_variables (set ident ? ? c3 〈UnspecifiedB,c7〉 en) c6 c1);
    421 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
     418]]]. nwhd;
     419##[ //;
     420##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
     421    #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    422422napply (alloc_variables_cons … IH); /2/;
    423423nqed.
     
    431431      [ nil ⇒ Some ? (Error ?)
    432432      | cons v1 vl ⇒ Some ? (
    433           〈bcl,b〉 ← opt_to_res ? (get … id e);:
    434           m1 ← opt_to_res ? (store_value_of_type ty m (blk_ptr_cls bcl) b zero v1);:
     433          b ← opt_to_res ? (get … id e);:
     434          m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);:
    435435          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
    436436      ]
    437437  ] ].
    438438nwhd; //;
    439 napply opt_bind_OK; #x; ncases x; #bcl b eb;
     439napply opt_bind_OK; #b eb;
    440440napply opt_bind_OK; #m1 em1;
    441441napply reinject; #m2 em2 Hm2;
     
    474474ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    475475#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    476 ndefinition ms_eq_dec : ∀s1,s2:mem_space. (s1 = s2) + (s1 ≠ s2).
     476ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
    477477#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    478478
     
    823823  let m0 ≝ init_mem Genv ?? p in
    824824  Some ? (
    825     ! b ← find_symbol ? ? ge (prog_main ?? p);:
     825    ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);:
     826    ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);:
    826827    ! f ← find_funct_ptr ? ? ge b;:
    827828    ret ? (Callstate f (nil ?) Kstop m0)).
    828829nwhd;
    829 napply opt_bindIO_OK; #b eb;
     830napply opt_bindIO2_OK; #sp b esb;
     831napply opt_bindIO_OK; #u ecode;
    830832napply opt_bindIO_OK; #f ef;
    831 nwhd; napply (initial_state_intro … eb ef);
     833ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4: ndestruct (ecode); ##]
     834nwhd; napply (initial_state_intro … esb ef);
    832835nqed.
    833836
  • C-semantics/Csem.ma

    r124 r125  
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_int: ∀pcl,b,ofs,sz,sg.
    51       is_true (Vptr pcl b ofs) (Tint sz sg)
     50  | is_true_pointer_int: ∀psp,b,ofs,sz,sg.
     51      is_true (Vptr psp b ofs) (Tint sz sg)
    5252  | is_true_int_pointer: ∀n,s,t.
    5353      n ≠ zero →
    5454      is_true (Vint n) (Tpointer s t)
    55   | is_true_pointer_pointer: ∀pcl,b,ofs,s,t.
    56       is_true (Vptr pcl b ofs) (Tpointer s t)
     55  | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
     56      is_true (Vptr psp b ofs) (Tpointer s t)
    5757  | is_true_float: ∀f,sz.
    5858      f ≠ Fzero →
     
    313313      [ Vint n1 ⇒ match v2 with
    314314         [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    315          | Vptr pcl b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
     315         | Vptr psp b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
    316316         | _ ⇒ None ?
    317317         ]
     
    400400  ].
    401401
    402 (* XXX should go somewhere else? *)
    403 ndefinition ptr_cls_spc : ptr_class → mem_space ≝
    404 λp.match p with
    405 [ Universal ⇒ Generic
    406 | Data ⇒ Data
    407 | IData ⇒ IData
    408 | XData ⇒ XData
    409 | Code ⇒ Code
    410 ].
    411 ndefinition ptr_spc_cls : mem_space → ptr_class ≝
    412 λp.match p with
    413 [ Generic ⇒ Universal
    414 | Data ⇒ Data
    415 | IData ⇒ IData
    416 | XData ⇒ XData
    417 | Code ⇒ Code
    418 ].
    419 
    420 ndefinition blk_ptr_cls : block_class → ptr_class ≝
    421 λb.match b with
    422 [ UnspecifiedB ⇒ Universal
    423 | DataB ⇒ Data
    424 | IDataB ⇒ IData
    425 | XDataB ⇒ XData
    426 | CodeB ⇒ Code
    427 ].
    428 
    429402ninductive type_pointable : type → Prop ≝
    430403| type_ptr_int : type_pointable (Tint I32 Unsigned)
     
    433406| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
    434407
    435 ninductive type_space : type → mem_space → Prop ≝
    436 | type_spc_int : type_space (Tint I32 Unsigned) Generic
     408ninductive type_space : type → memory_space → Prop ≝
     409| type_spc_int : type_space (Tint I32 Unsigned) Any
    437410| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
    438411| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     
    452425      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    453426           (Vfloat (cast_float_float sz2 f))
    454   | cast_pp: ∀m,pcl,psp,ty,ty',b,ofs.
     427  | cast_pp: ∀m,psp,psp',ty,ty',b,ofs.
    455428      type_pointable ty →
    456       type_space ty' psp
    457       class_compat (blockclass m b) (ptr_spc_cls psp)
    458       cast m (Vptr pcl b ofs) ty ty' (Vptr (ptr_spc_cls psp) b ofs)
     429      type_space ty' psp'
     430      pointer_compat (block_space m b) psp'
     431      cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs)
    459432  | cast_pp_z: ∀m,ty,ty'.
    460433      type_pointable ty → (* Don't care which space it is for the source type *)
     
    478451  block. *)
    479452
    480 ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable -> location *)
     453ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    481454
    482455ndefinition empty_env: env ≝ (empty …).
     
    488461  reference, the pointer [Vptr b ofs] is returned. *)
    489462
    490 nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝
     463nlet rec load_value_of_type (ty: type) (m: mem) (psp:memory_space) (b: block) (ofs: int) : option val ≝
    491464  match access_mode ty with
    492   [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs)
    493   | By_reference ⇒ Some ? (Vptr pcl b ofs)
     465  [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
     466  | By_reference ⇒ Some ? (Vptr psp b ofs)
    494467  | By_nothing ⇒ None ?
    495468  ].
     
    500473  This is allowed only if [ty] indicates an access by value. *)
    501474
    502 nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝
     475nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:memory_space) (loc: block) (ofs: int) (v: val) : option mem ≝
    503476  match access_mode ty_dest with
    504   [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v
     477  [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
    505478  | By_reference ⇒ None ?
    506479  | By_nothing ⇒ None ?
     
    522495  | alloc_variables_cons:
    523496      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    524       alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)
    525       alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 →
     497      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
     498      alloc_variables (set … id b1 e) m1 vars e2 m2 →
    526499      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    527500
     
    538511      bind_parameters e m (nil ?) (nil ?) m
    539512  | bind_parameters_cons:
    540       ∀e,m,id,ty,params,v1,vl,bcls,b,m1,m2.
    541       get ??? id e = Some ? 〈bcls,b〉
    542       store_value_of_type ty m (blk_ptr_cls bcls) b zero v1 = Some ? m1 →
     513      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
     514      get ??? id e = Some ? b
     515      store_value_of_type ty m Any b zero v1 = Some ? m1 →
    543516      bind_parameters e m1 params vl m2 →
    544517      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
    545518
     519(* XXX: this doesn't look right - we're assigning arbitrary memory spaces to
     520   parameters? *)
     521
    546522(* * Return the list of blocks in the codomain of [e]. *)
    547523
    548524ndefinition blocks_of_env : env → list block ≝ λe.
    549   map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).
     525  map ?? (λx. snd ?? x) (elements ??? e).
    550526
    551527(* * Selection of the appropriate case of a [switch], given the value [n]
     
    588564  | eval_Econst_float:   ∀f,ty.
    589565      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    590   | eval_Elvalue: ∀a,ty,pcl,loc,ofs,v.
    591       eval_lvalue ge e m (Expr a ty) pcl loc ofs ->
    592       load_value_of_type ty m pcl loc ofs = Some ? v ->
     566  | eval_Elvalue: ∀a,ty,psp,loc,ofs,v.
     567      eval_lvalue ge e m (Expr a ty) psp loc ofs ->
     568      load_value_of_type ty m psp loc ofs = Some ? v ->
    593569      eval_expr ge e m (Expr a ty) v
    594   | eval_Eaddrof: ∀a,ty,pcl,loc,ofs.
    595       eval_lvalue ge e m a pcl loc ofs ->
    596       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr pcl loc ofs)
     570  | eval_Eaddrof: ∀a,ty,psp,loc,ofs.
     571      eval_lvalue ge e m a psp loc ofs ->
     572      eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs)
    597573  | eval_Esizeof: ∀ty',ty.
    598574      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
     
    645621  that contains the value of the expression [a]. *)
    646622
    647 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → ptr_class → block -> int -> Prop ≝
    648   | eval_Evar_local:   ∀id,bcl,l,ty.
    649       (* XXX notation? e!id*) get ??? id e = Some ? 〈bcl,l〉 ->
    650       eval_lvalue ge e m (Expr (Evar id) ty) (blk_ptr_cls bcl) l zero
    651   | eval_Evar_global: ∀id,l,ty.
     623with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block -> int -> Prop ≝
     624  | eval_Evar_local:   ∀id,l,ty.
     625      (* XXX notation? e!id*) get ??? id e = Some ? l →
     626      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero
     627  | eval_Evar_global: ∀id,sp,l,ty.
    652628      (* XXX e!id *) get ??? id e = None ? ->
    653       find_symbol ?? ge id = Some ? l ->
    654       eval_lvalue ge e m (Expr (Evar id) ty) Universal l zero (* XXX *)
    655   | eval_Ederef: ∀a,ty,pcl,l,ofs.
    656       eval_expr ge e m a (Vptr pcl l ofs) ->
    657       eval_lvalue ge e m (Expr (Ederef a) ty) pcl l ofs
    658  | eval_Efield_struct:   ∀a,i,ty,pcl,l,ofs,id,fList,delta.
    659       eval_lvalue ge e m a pcl l ofs ->
     629      find_symbol ?? ge id = Some ? 〈sp,l〉 ->
     630      eval_lvalue ge e m (Expr (Evar id) ty) sp l zero
     631  | eval_Ederef: ∀a,ty,psp,l,ofs.
     632      eval_expr ge e m a (Vptr psp l ofs) ->
     633      eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs
     634 | eval_Efield_struct:   ∀a,i,ty,psp,l,ofs,id,fList,delta.
     635      eval_lvalue ge e m a psp l ofs ->
    660636      typeof a = Tstruct id fList ->
    661637      field_offset i fList = OK ? delta ->
    662       eval_lvalue ge e m (Expr (Efield a i) ty) pcl l (add ofs (repr delta))
    663  | eval_Efield_union:   ∀a,i,ty,pcl,l,ofs,id,fList.
    664       eval_lvalue ge e m a pcl l ofs ->
     638      eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta))
     639 | eval_Efield_union:   ∀a,i,ty,psp,l,ofs,id,fList.
     640      eval_lvalue ge e m a psp l ofs ->
    665641      typeof a = Tunion id fList ->
    666       eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs.
     642      eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs.
    667643
    668644(*
     
    702678  | Kswitch: cont -> cont
    703679       (**r catches [break] statements arising out of [switch] *)
    704   | Kcall: option (ptr_class × block × int × type) ->   (**r where to store result *)
     680  | Kcall: option (memory_space × block × int × type) ->   (**r where to store result *)
    705681           function ->                      (**r calling function *)
    706682           env ->                           (**r local env of calling function *)
     
    800776ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    801777
    802   | step_assign:   ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'.
    803       eval_lvalue ge e m a1 pcl loc ofs ->
     778  | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'.
     779      eval_lvalue ge e m a1 psp loc ofs ->
    804780      eval_expr ge e m a2 v2 ->
    805       store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' ->
     781      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' ->
    806782      step ge (State f (Sassign a1 a2) k e m)
    807783           E0 (State f Sskip k e m')
     
    815791           E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    816792
    817   | step_call_some:   ∀f,lhs,a,al,k,e,m,pcl,loc,ofs,vf,vargs,fd.
    818       eval_lvalue ge e m lhs pcl loc ofs ->
     793  | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd.
     794      eval_lvalue ge e m lhs psp loc ofs ->
    819795      eval_expr ge e m a vf ->
    820796      eval_exprlist ge e m al vargs ->
     
    822798      type_of_fundef fd = typeof a ->
    823799      step ge (State f (Scall (Some ? lhs) a al) k e m)
    824            E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m)
     800           E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
    825801
    826802  | step_seq:  ∀f,s1,s2,k,e,m.
     
    961937           E0 (State f Sskip k e m)
    962938
    963   | step_returnstate_1: ∀v,f,e,k,m,m',pcl,loc,ofs,ty.
    964       store_value_of_type ty m pcl loc ofs v = Some ? m' ->
    965       step ge (Returnstate v (Kcall (Some ? 〈〈〈pcl,loc〉, ofs〉, ty〉) f e k) m)
     939  | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
     940      store_value_of_type ty m psp loc ofs v = Some ? m' ->
     941      step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
    966942           E0 (State f Sskip k e m').
    967943(*
     
    12811257      let ge := globalenv Genv ?? p in
    12821258      let m0 := init_mem Genv ?? p in
    1283       find_symbol ?? ge (prog_main ?? p) = Some ? b ->
     1259      find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 ->
    12841260      find_funct_ptr ?? ge b = Some ? f ->
    12851261      initial_state p (Callstate f (nil ?) Kstop m0).
  • C-semantics/Csyntax.ma

    r124 r125  
    4646  | F32: floatsize
    4747  | F64: floatsize.
    48 
    49 (* Pointers can point to particular memory spaces. *)
    50 ninductive mem_space : Type ≝
    51   | Generic : mem_space
    52   | Data : mem_space
    53   | IData : mem_space
    54   | XData : mem_space
    55   | Code : mem_space.
    5648
    5749(* * The syntax of type expressions.  Some points to note:
     
    9486  | Tint: intsize → signedness → type   (**r integer types *)
    9587  | Tfloat: floatsize → type            (**r floating-point types *)
    96   | Tpointer: mem_space → type → type   (**r pointer types ([*ty]) *)
    97   | Tarray: mem_space → type → Z → type (**r array types ([ty[len]]) *)
     88  | Tpointer: memory_space → type → type   (**r pointer types ([*ty]) *)
     89  | Tarray: memory_space → type → Z → type (**r array types ([ty[len]]) *)
    9890  | Tfunction: typelist → type → type   (**r function types *)
    9991  | Tstruct: ident → fieldlist → type   (**r struct types *)
  • C-semantics/Globalenvs.ma

    r124 r125  
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type. genv_t F → ident → option block;
     68  find_symbol: ∀F: Type. genv_t F → ident → option (memory_space × block)(*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
    7171(* * ** Properties of the operations. *)
    72 (*
     72
    7373  find_funct_inv:
    7474    ∀F: Type. ∀ge: t F. ∀v: val. ∀f: F.
     
    142142(* * Commutation properties between program transformations
    143143  and operations over global environments. *)
    144 *)*)
     144*)
    145145  find_funct_ptr_transf:
    146146    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     
    171171    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
    172172    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf
    173 (*
     173
    174174(* * Commutation properties between partial program transformations
    175175  and operations over global environments. *)
     
    310310].
    311311
     312(* Functions are given negative block numbers *)
     313
    312314(* XXX: temporary definition
    313315   NB: only global functions, no global variables *)
     
    315317  functions: block → option F;
    316318  nextfunction: Z;
    317   symbols: ident → option block
     319  symbols: ident → option (memory_space × block)
    318320}.
     321(*
     322(** The rest of this library is a straightforward implementation of
     323  the module signature above. *)
     324
     325Module Genv: GENV.
     326
     327Section GENV.
     328
     329Variable F: Type.                    (* The type of functions *)
     330Variable V: Type.                    (* The type of information over variables *)
     331
     332Record genv : Type := mkgenv {
     333  functions: ZMap.t (option F);     (* mapping function ptr → function *)
     334  nextfunction: Z;
     335  symbols: PTree.t block                (* mapping symbol → block *)
     336}.
     337
     338Definition t := genv.
     339*)
     340
     341ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝
     342λF,name_fun,g.
     343  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'))
     345            (Zpred b)
     346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
     347
     348ndefinition add_symbol : ∀F:Type. ident → memory_space → block → genv F → genv F ≝
     349λF,name,bsp,b,g.
     350  mk_genv F (functions ? g)
     351            (nextfunction ? g)
     352            ((*PTree.set*) λi. match ident_eq name i with [ inl _ ⇒ Some ? 〈bsp,b〉 | inr _ ⇒ symbols ? g i ]).
     353(*
     354Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
     355  ZMap.get b g.(functions).
     356
     357Definition find_funct (g: genv) (v: val) : option F :=
     358  match v with
     359  | Vptr b ofs =>
     360      if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
     361  | _ =>
     362      None
     363  end.
     364
     365Definition find_symbol ? (g: genv) (symb: ident) : option block :=
     366  PTree.get symb g.(symbols).
     367
     368Lemma find_funct_inv:
     369  forall (ge: t) (v: val) (f: F),
     370  find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
     371Proof.
     372  intros until f. unfold find_funct. destruct v; try (intros; discriminate).
     373  generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
     374  exists b. congruence.
     375  discriminate.
     376Qed.
     377
     378Lemma find_funct_find_funct_ptr:
     379  forall (ge: t) (b: block),
     380  find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
     381Proof.
     382  intros. simpl.
     383  generalize (Int.eq_spec Int.zero Int.zero).
     384  case (Int.eq Int.zero Int.zero); intros.
     385  auto. tauto.
     386Qed.
     387*)
     388(* Construct environment and initial memory store *)
     389ndefinition empty_mem ≝ empty. (* XXX*)
     390ndefinition empty : ∀F. genv F ≝
     391  λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
     392(*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
     393
     394ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝
     395λF,init,fns.
     396  foldr ?? (add_funct F) init fns.
     397
     398ndefinition add_globals : ∀F,V:Type.
     399       genv F × mem → list (ident × (list init_data) × memory_space × V) →
     400       genv F × mem ≝
     401λF,V,init,vars.
     402  foldr ??
     403    (λid_init: ident × (list init_data) × memory_space × V. λg_st: genv F × mem.
     404      match id_init with [ mk_pair id_init1 info ⇒
     405      match id_init1 with [ mk_pair id_init2 bsp ⇒
     406      match id_init2 with [ mk_pair id init ⇒
     407      match g_st with [ mk_pair g st ⇒
     408        match alloc_init_data st init bsp with [ mk_pair st' b ⇒
     409          〈add_symbol ? id bsp b g, st'〉
     410        ] ] ] ] ])
     411    init vars.
     412
     413ndefinition globalenv_initmem : ∀F,V:Type. program F V → genv F × mem ≝
     414λF,V,p.
     415  add_globals F V
     416    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     417    (prog_vars ?? p).
     418
     419ndefinition globalenv_ : ∀F,V:Type. program F V → genv F ≝
     420λF,V,p.
     421  \fst (globalenv_initmem F V p).
     422ndefinition init_mem_ : ∀F,V:Type. program F V → mem ≝
     423λF,V,p.
     424  \snd (globalenv_initmem F V p).
    319425
    320426ndefinition Genv : GENV ≝ mk_GENV
    321427  genv  (* genv_t *)
    322   (λF,V,p. foldr ??
    323     (λf,ge. match f with [ mk_pair id def ⇒
    324             let b ≝ nextfunction ? ge in
    325             mk_genv ? (λb'. if eqZb b b' then Some ? def else (functions ? ge b'))
    326                       (Zsucc b)
    327                       (λi. match ident_eq id i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? ge i)])
    328             ])
    329    (mk_genv ? (λ_.None ?) 0 (λ_.None ?)) (prog_funct ?? p))  (* globalenv *)
    330   (λF,V,p. empty)  (* init_mem *)
     428  globalenv_
     429  init_mem_
    331430  (λF,ge. functions ? ge) (* find_funct_ptr *)
    332431  (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    333432  (λF,ge. symbols ? ge) (* find_symbol *)
     433(*  ?
    334434  ?
    335435  ?
    336436  ?
    337437  ?
    338   ?
    339   ?
     438  ?*)
    340439.
     440(*
    341441##[ #A B C transf p b f; nelim p; #fns main vars;
    342442    nelim fns;
    343     ##[ nnormalize; #H; ndestruct;
     443    ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct;
    344444    ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);
    345445        nrewrite > (?:nextfunction ?? = length ? t);
     
    443543##] nqed.
    444544         
    445 (*
    446 (** The rest of this library is a straightforward implementation of
    447   the module signature above. *)
    448 
    449 Module Genv: GENV.
    450 
    451 Section GENV.
    452 
    453 Variable F: Type.                    (* The type of functions *)
    454 Variable V: Type.                    (* The type of information over variables *)
    455 
    456 Record genv : Type := mkgenv {
    457   functions: ZMap.t (option F);     (* mapping function ptr → function *)
    458   nextfunction: Z;
    459   symbols: PTree.t block                (* mapping symbol → block *)
    460 }.
    461 
    462 Definition t := genv.
    463 
    464 Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=
    465   let b := g.(nextfunction) in
    466   mkgenv (ZMap.set b (Some ? (snd name_fun)) g.(functions))
    467          (Zpred b)
    468          (PTree.set (fst name_fun) b g.(symbols)).
    469 
    470 Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
    471   mkgenv g.(functions)
    472          g.(nextfunction)
    473          (PTree.set name b g.(symbols)).
    474 
    475 Definition find_funct_ptr ? (g: genv) (b: block) : option F :=
    476   ZMap.get b g.(functions).
    477 
    478 Definition find_funct (g: genv) (v: val) : option F :=
    479   match v with
    480   | Vptr b ofs =>
    481       if Int.eq ofs Int.zero then find_funct_ptr ? g b else None
    482   | _ =>
    483       None
    484   end.
    485 
    486 Definition find_symbol ? (g: genv) (symb: ident) : option block :=
    487   PTree.get symb g.(symbols).
    488 
    489 Lemma find_funct_inv:
    490   forall (ge: t) (v: val) (f: F),
    491   find_funct ge v = Some ? f → ∃b. v = Vptr b Int.zero.
    492 Proof.
    493   intros until f. unfold find_funct. destruct v; try (intros; discriminate).
    494   generalize (Int.eq_spec i Int.zero). case (Int.eq i Int.zero); intros.
    495   exists b. congruence.
    496   discriminate.
    497 Qed.
    498 
    499 Lemma find_funct_find_funct_ptr:
    500   forall (ge: t) (b: block),
    501   find_funct ge (Vptr b Int.zero) = find_funct_ptr ? ge b.
    502 Proof.
    503   intros. simpl.
    504   generalize (Int.eq_spec Int.zero Int.zero).
    505   case (Int.eq Int.zero Int.zero); intros.
    506   auto. tauto.
    507 Qed.
    508 
    509 (* Construct environment and initial memory store *)
    510 
    511 Definition empty : genv :=
    512   mkgenv (ZMap.init None) (-1) (PTree.empty block).
    513 
    514 Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
    515   List.fold_right add_funct init fns.
    516 
    517 Definition add_globals
    518        (init: genv * mem) (vars: list (ident * list init_data * V))
    519        : genv * mem :=
    520   List.fold_right
    521     (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>
    522        match id_init, g_st with
    523        | ((id, init), info), (g, st) =>
    524            let (st', b) := Mem.alloc_init_data st init in
    525            (add_symbol id b g, st')
    526        end)
    527     init vars.
    528 
    529 Definition globalenv_initmem (p: program F V) : (genv * mem) :=
    530   add_globals
    531     (add_functs empty p.(prog_funct), Mem.empty)
    532     p.(prog_vars).
    533 
    534 Definition globalenv (p: program F V) : genv :=
    535   fst (globalenv_initmem p).
    536 Definition init_mem  (p: program F V) : mem :=
    537   snd (globalenv_initmem p).
    538545
    539546Lemma functions_globalenv:
  • C-semantics/IOMonad.ma

    r25 r125  
    118118nqed.
    119119
     120nlemma opt_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO I O C.
     121  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
     122  P_io I O ? P (bindIO2 I O A B C e f).
     123#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
     124nqed.
     125
    120126nlemma bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
    121127  (∀v:A. P_io I O ? P (f v)) →
  • C-semantics/Mem.ma

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

    r124 r125  
    3636*)
    3737
    38 ninductive ptr_class : Type ≝
    39 | Universal : ptr_class
    40 | Data : ptr_class
    41 | IData : ptr_class
    42 | XData : ptr_class
    43 (* pdata?  I'd rather not... *)
    44 | Code : ptr_class.
    45 
    46 ninductive ptr_class_compat : ptr_class → ptr_class → Prop ≝
    47 | ptr_class_same : ∀pcl. ptr_class_compat pcl pcl
    48 | ptr_univ_l : ∀pcl. ptr_class_compat Universal pcl
    49 | ptr_univ_r : ∀pcl. ptr_class_compat pcl Universal.
    50 
    51 nlemma ptr_class_compat_sym : ∀p,p'. ptr_class_compat p p' → ptr_class_compat p' p.
    52 #p p' H; ninversion H; //; nqed.
    53 
    5438(* TODO: should comparison and subtraction of pointers of different sorts
    5539         be supported? *)
     
    5943  | Vint: int -> val
    6044  | Vfloat: float -> val
    61   | Vptr: ptr_class → block -> int -> val.
     45  | Vptr: memory_space → block -> int -> val.
    6246
    6347ndefinition Vzero: val ≝ Vint zero.
  • C-semantics/test/io.c.ma

    r20 r125  
    2929   ret ? 〈t,s〉).
    3030
     31ninductive result (T:Type) : T → Prop ≝
     32| witness : ∀t:T. result T t.
     33
    3134(* The trick to being able to normalize the term is to avoid looking at the
    3235   continuations! *)
    3336nremark exec_OK:
    34     match match ts with [ Interact f args k ⇒ k (EVint (repr 6))
    35                  | Value v ⇒ Wrong ?
    36                  | Wrong ⇒ Wrong ? ] with
    37     [ Interact _ _ _ ⇒ False
    38     | Value v ⇒ v = v
     37    match match ts with [ Interact call k ⇒ k (EVint (repr 6))
     38                 | Value v ⇒ Wrong ???
     39                 | Wrong ⇒ Wrong ??? ] with
     40    [ Interact _ _ ⇒ False
     41    | Value v ⇒ result ? v
    3942    | Wrong ⇒ False
    4043    ].
Note: See TracChangeset for help on using the changeset viewer.