Changeset 124


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

Initial work on Clight semantics with 8051 memory spaces.

Location:
C-semantics
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r25 r124  
    55include "IOMonad.ma".
    66
    7 (* Some experimental definitions for an executable semantics. *)
    8 
    9 ndefinition bool_of_val_1 : val → type → res val ≝
    10   λv,ty. match v with
    11   [ Vint i ⇒ match ty with
    12     [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero))
    13     | Tpointer _ ⇒ OK ? (of_bool (¬eq i zero))
    14     | _ ⇒ Error ?
    15     ]
    16   | Vfloat f ⇒ match ty with
    17     [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero))
    18     | _ ⇒ Error ?
    19     ]
    20   | Vptr _ _ ⇒ match ty with
    21     [ Tint _ _ ⇒ OK ? Vtrue
    22     | Tpointer _ ⇒ OK ? Vtrue
    23     | _ ⇒ Error ?
    24     ]
    25   | _ ⇒ Error ?
    26   ].
    27 
    28 (* There's a lot more repetition than I'd like here, in large part because
    29    there's no way to introduce different numbers of hypotheses when doing the
    30    case distinctions. *)
    31 
    32 nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r.
    33 #v ty r; @;
    34 ##[
    35   nelim v; ##[ #H; nnormalize in H; ndestruct; ##| ##2,3: #x; ##| ##4: #x y; ##]
    36   ncases ty;
    37   ##[ ##1,10,19: #H; nnormalize in H; ndestruct;
    38   ##| #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    39     ##[ nrewrite > H; nrewrite > (eq_true …); #H';
    40         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    41         #H''; nrewrite > H''; /2/;
    42     ##| nrewrite > (eq_false …); //; #H';
    43         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    44         #H''; nrewrite > H''; /3/;
    45     ##]
    46   ##|##3,9,13,18,21,27: #x H; nnormalize in H; ndestruct;
    47   ##| #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
    48     ##[ nrewrite > H; nrewrite > (eq_true …); #H';
    49         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    50         #H''; nrewrite > H''; /2/;
    51     ##| nrewrite > (eq_false …); //; #H';
    52         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    53         #H''; nrewrite > H''; /3/;
    54     ##]
    55   ##| ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct;
    56   ##| #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H;
    57     ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H';
    58         ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    59         #H''; nrewrite > H''; /2/;
    60     ##| nrewrite > (Feq_zero_false …); //; #H';
    61         ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
    62         #H''; nrewrite > H''; /3/;
    63     ##]
    64   ##| #i s H; nwhd in H:(??%?);
    65       ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
    66       #H'; nrewrite > H'; /2/;
    67   ##| #t H; nwhd in H:(??%?);
    68       ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
    69       #H'; nrewrite > H'; /2/;
    70   ##]
    71 ##| #H; nelim H; #v t H'; nelim H';
    72   ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    73   ##| ##2,4: //
    74   ##| #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    75   ##| #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    76   ##| #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    77   ##| #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
    78   ##| #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    79   ##]
    80 ##] nqed.
    81 
    827include "Plogic/russell_support.ma".
    83 
    84 (* Nicer - we still have to deal with all of the cases, but only need to
    85    introduce the result value, so there's a single case for getting rid of
    86    all the Error goals. *)
    87 
    88 ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool | ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝
    89   λv,ty. match v in val with
    90   [ Vint i ⇒ match ty with
    91     [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    92     | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
    93     | _ ⇒ Some ? (Error ?)
    94     ]
    95   | Vfloat f ⇒ match ty with
    96     [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
    97     | _ ⇒ Some ? (Error ?)
    98     ]
    99   | Vptr _ _ ⇒ match ty with
    100     [ Tint _ _ ⇒ Some ? (OK ? true)
    101     | Tpointer _ ⇒ Some ? (OK ? true)
    102     | _ ⇒ Some ? (Error ?)
    103     ]
    104   | _ ⇒ Some ? (Error ?)
    105   ]. nwhd;
    106 ##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero);
    107   ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/;
    108   ##| ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue);  ##[ ##2,4: ndestruct; // ##] /3/;
    109   ##]
    110 ##| ##13: #r; nelim (eq_dec c0 Fzero);
    111   ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/;
    112   ##| #ne; nrewrite > (Feq_zero_false …); //; #H;
    113       nrewrite > (?:of_bool r=Vtrue);  ##[ ##2: ndestruct; // ##] /3/;
    114   ##]
    115 ##| ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/
    116 ##| ##*: #a b; ndestruct;
    117 ##] nqed.
    118 
    119 (* Same as before, except we have to write eject in because the type for the
    120    equality is left implied, so the coercion isn't used. *)
    121 
    122 nlemma bool_of_val_2_complete : ∀v,ty,r.
    123   bool_of_val v ty r →
    124   ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b.
    125 #v ty r H; nelim H; #v t H'; nelim H';
    126   ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    127   ##| #b i i0 s; @ true; @; //
    128   ##| #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
    129   ##| #b i t0; @ true; @; //
    130   ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
    131   ##| #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    132   ##| #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
    133   ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
    134   ##]
    135 nqed.
    136 
    137 
    138 (* Nicer again (after the extra definitions).  Just use sigma type rather than
    139    the subset, but take into account the error monad.  The error cases all
    140    become trivial and we don't have to muck around to get the result. *)
    1418
    1429ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
     
    17542  [ Vint i ⇒ match ty with
    17643    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
    177     | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
     44    | Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero))
    17845    | _ ⇒ Some ? (Error ?)
    17946    ]
     
    18249    | _ ⇒ Some ? (Error ?)
    18350    ]
    184   | Vptr _ _ ⇒ match ty with
     51  | Vptr _ _ _ ⇒ match ty with
    18552    [ Tint _ _ ⇒ Some ? (OK ? true)
    186     | Tpointer _ ⇒ Some ? (OK ? true)
     53    | Tpointer _ _ ⇒ Some ? (OK ? true)
    18754    | _ ⇒ Some ? (Error ?)
    18855    ]
     
    21077#v ty r H; nelim H; #v t H'; nelim H';
    21178  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    212   ##| #b i i0 s; @ true; @; //
    213   ##| #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
    214   ##| #b i t0; @ true; @; //
     79  ##| #p b i i0 s; @ true; @; //
     80  ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     81  ##| #p b i p0 t0; @ true; @; //
    21582  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
    21683  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    217   ##| #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
     84  ##| #p t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
    21885  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
    21986  ##]
     
    23299
    233100nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
    234   (∀v:A. err_eq A P e v → ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
     101  (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
    235102  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
    236 #A B P P' e f; nelim e; //;
    237 #v0; nelim v0; #v Hv IH; napply IH; //; nqed.
     103#A B P P' e f; nelim e;
     104##[ #v0; nelim v0; #v Hv IH; napply IH;
     105##| #_; napply I;
     106##] nqed.
    238107
    239108nlemma bind2_OK: ∀A,B,C,P,e,f.
     
    286155##] nqed.
    287156
    288 nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
    289 match ty with
    290 [ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
    291 | Tpointer _ ⇒ Some ? (OK ? something)
    292 | Tarray _ _ ⇒ Some ? (OK ? something)
    293 | Tfunction _ _ ⇒ Some ? (OK ? something)
    294 | _ ⇒ Some ? (Error ?)
    295 ]. nwhd; //; nqed.
    296157(*
    297158nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
     
    299160*)
    300161
    301 nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
     162nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) : res (Σv':val. cast m (Vint i) ty ty' v') ≝
     163match eq i zero with
     164[ true ⇒
     165  match ty with
     166  [ Tpointer _ _ ⇒
     167    match ty' with
     168    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     169    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     170    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     171    | _ ⇒ Some ? (Error ?)
     172    ]
     173  | Tarray _ _ _ ⇒
     174    match ty' with
     175    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     176    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     177    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     178    | _ ⇒ Some ? (Error ?)
     179    ]
     180  | Tfunction _ _ ⇒
     181    match ty' with
     182    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     183    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     184    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     185    | _ ⇒ Some ? (Error ?)
     186    ]
     187  | _ ⇒ Some ? (Error ?)
     188  ]
     189| false ⇒ Some ? (Error ?)
     190]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
     191   napply cast_pp_z; //; nqed.
     192
     193nlet rec exec_cast (m:mem) (v:val) (ty:type) (ty':type) : res (Σv':val. cast m v ty ty' v') ≝
    302194match v with
    303195[ Vint i ⇒
     
    307199    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
    308200    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
    309     (* no change in data repr *)
    310     | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
    311     ]
    312   | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
     201    | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     202    | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     203    | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     204    | _ ⇒ Some ? (Error ?)
     205    ]
     206  | Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     207  | Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     208  | Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for non-null values? *)
     209  | _ ⇒ Some ? (Error ?)
    313210  ]
    314211| Vfloat f ⇒
     
    322219  | _ ⇒ Some ? (Error ?)
    323220  ]
    324 | Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
     221| Vptr p b ofs ⇒
     222  Some ? (
     223    p ← match ty with [ Tpointer _ _ ⇒ OK ? something | Tarray _ _ _ ⇒ OK ? something | Tfunction _ _ ⇒ OK ? something | _ ⇒ Error ? ];:
     224    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)
     227    else Error ?)
     228  (* XXX: maybe should allow some Tint? *)
    325229| _ ⇒ Some ? (Error ?)
    326 ]. ndestruct; /2/;
    327 ##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
    328 ##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
    329 ##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
    330     napply cast_nn_p; //
     230]. nwhd; //;
     231##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
     232##| napply bind_OK; #u1 tyok;
     233    napply bind_OK; #s' es';
     234    ncut (type_pointable ty);
     235    ##[ ncases ty in tyok ⊢ %; //;
     236      ##[ #e; ##| ##3,6: #a e; ##| ##2,4,5: #a b e; ##] nwhd in e:(??%?); ndestruct;
     237    ##| ncut (type_space ty' s');
     238      ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
     239          nwhd in e:(??%?); ndestruct; //;
     240      ##| #Hty' Hty;
     241          nwhd in match (is_class_compat ??) in ⊢ %;
     242          ncases (class_compat_dec (blockclass m c1) (ptr_spc_cls s')); #Hcompat;
     243          nwhd; /2/;
     244      ##]
     245    ##]
    331246##] nqed.
     247
     248ndefinition 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 ] ].
    332251
    333252(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    342261  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
    343262  | Evar _ ⇒ Some ? (
    344       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    345       opt_to_res ? (load_value_of_type ty m loc ofs))
     263      l ← exec_lvalue' ge en m e' ty;:
     264      opt_to_res ? (load_value_of_type' ty m l))
    346265  | Ederef _ ⇒ Some ? (
    347       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    348       opt_to_res ? (load_value_of_type ty m loc ofs))
     266      l ← exec_lvalue' ge en m e' ty;:
     267      opt_to_res ? (load_value_of_type' ty m l))
    349268  | Efield _ _ ⇒ Some ? (
    350       〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
    351       opt_to_res ? (load_value_of_type ty m loc ofs))
     269      l ← exec_lvalue' ge en m e' ty;:
     270      opt_to_res ? (load_value_of_type' ty m l))
    352271  | Eaddrof a ⇒ Some ? (
    353       〈loc, ofs〉 ← exec_lvalue ge en m a;:
    354       OK ? (Vptr loc ofs))
     272      〈pl, ofs〉 ← exec_lvalue ge en m a;:
     273      OK ? (match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ]))
    355274  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
    356275  | Eunop op a ⇒ Some ? (
     
    383302  | Ecast ty' a ⇒ Some ? (
    384303      v ← exec_expr ge en m a;:
    385       exec_cast v (typeof a) ty')
     304      exec_cast m v (typeof a) ty')
    386305  ]
    387306]
    388 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝
     307and 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)) ≝
    389308  match e' with
    390309  [ Evar id ⇒
    391310      match (get … id en) with
    392       [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
    393       | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
     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 *)
    394313      ]
    395314  | Ederef a ⇒ Some ? (
    396315      v ← exec_expr ge en m a;:
    397316      match v with
    398       [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
     317      [ Vptr pcl l ofs ⇒ OK ? 〈〈pcl,l〉,ofs〉
    399318      | _ ⇒ Error ?
    400319      ])
     
    402321      match (typeof a) with
    403322      [ Tstruct id fList ⇒ Some ? (
    404           〈l,ofs〉 ← exec_lvalue ge en m a;:
     323          〈pl,ofs〉 ← exec_lvalue ge en m a;:
    405324          delta ← field_offset i fList;:
    406           OK ? 〈l,add ofs (repr delta)〉)
     325          OK ? 〈pl,add ofs (repr delta)〉)
    407326      | Tunion id fList ⇒ Some ? (
    408           〈l,ofs〉 ← exec_lvalue ge en m a;:
    409           OK ? 〈l,ofs〉)
     327          〈pl,ofs〉 ← exec_lvalue ge en m a;:
     328          OK ? 〈pl,ofs〉)
    410329      | _ ⇒ Some ? (Error ?)
    411330      ]
    412331  | _ ⇒ Some ? (Error ?)
    413332  ]
    414 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝
     333and 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)) ≝
    415334match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    416 nwhd; //;
    417 ##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    418     napply opt_OK;  #v ev; /2/;
    419 ##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
    420     napply opt_OK;  #v ev; /2/;
    421 ##| napply sig_bind2_OK; #loc ofs H;
     335nwhd;
     336##[ //
     337##| //
     338##| ##3,4:
     339    napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #pcl loc ofs H;
     340    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;
    422342    nwhd; napply eval_Eaddrof; //;
    423 ##| napply sig_bind_OK; #v1 ev1 Hv1;
     343##| napply sig_bind_OK; #v1 Hv1;
    424344    napply opt_OK; #v ev;
    425345    napply (eval_Eunop … Hv1 ev);
    426 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    427     napply sig_bind_OK; #v2 ev2 Hv2;
     346##| napply sig_bind_OK; #v1 Hv1;
     347    napply sig_bind_OK; #v2 Hv2;
    428348    napply opt_OK; #v ev;
    429349    napply (eval_Ebinop … Hv1 Hv2 ev);
    430 ##| napply sig_bind_OK; #v ev Hv;
    431     napply sig_bind_OK; #v' ev' Hv';
     350##| napply sig_bind_OK; #v Hv;
     351    napply sig_bind_OK; #v' Hv';
    432352    napply (eval_Ecast … Hv Hv');
    433 ##| napply sig_bind_OK; #vb evb Hvb;
     353##| napply sig_bind_OK; #vb Hvb;
    434354    napply sig_bind_OK; #b;
    435     ncases b; #eb Hb; napply reinject; #v ev Hv;
     355    ncases b; #Hb; napply reinject; #v ev Hv;
    436356    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    437357    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    438358    ##]
    439 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    440     napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
    441     ##[ napply sig_bind_OK; #v2 ev2 Hv2;
    442         napply sig_bind_OK; #b2 eb2 Hb2;
     359##| napply sig_bind_OK; #v1 Hv1;
     360    napply sig_bind_OK; #b1; ncases b1; #Hb1;
     361    ##[ napply sig_bind_OK; #v2 Hv2;
     362        napply sig_bind_OK; #b2 Hb2;
    443363        napply (eval_Eandbool_2 … Hv1 … Hv2);
    444364        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    445365    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    446366    ##]
    447 ##| napply sig_bind_OK; #v1 ev1 Hv1;
    448     napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
     367##| napply sig_bind_OK; #v1 Hv1;
     368    napply sig_bind_OK; #b1; ncases b1; #Hb1;
    449369    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    450     ##| napply sig_bind_OK; #v2 ev2 Hv2;
    451         napply sig_bind_OK; #b2 eb2 Hb2;
     370    ##| napply sig_bind_OK; #v2 Hv2;
     371        napply sig_bind_OK; #b2 Hb2;
    452372        napply (eval_Eorbool_2 … Hv1 … Hv2);
    453373        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
    454374    ##]
    455 ##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
    456     napply opt_OK; #v ev; /2/;
     375##| //
     376##| napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #pcl l ofs H;
     377    napply opt_OK; #v ev; napply (eval_Elvalue … H ev);
     378##| //
     379##| //
    457380##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
    458 ##| napply eval_Evar_local; /2/
    459 ##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
     381##| napply eval_Evar_local; nrewrite < c6; /2/
     382##| napply sig_bind_OK; #v; ncases v; //; #pcl l ofs Hv; nwhd;
    460383    napply eval_Ederef; //
    461 ##| napply sig_bind2_OK; #l ofs H;
     384##| ##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;
    462386    napply bind_OK; #delta Hdelta;
    463387    napply (eval_Efield_struct … H c5 Hdelta);
    464 ##| napply sig_bind2_OK; #l ofs H;
     388##| napply sig_bind2_OK; #x; ncases x; #pcl l ofs H;
    465389    napply (eval_Efield_union … H c5);
     390##| //
    466391##] nqed.
    467392
     
    475400  OK ? (cons val v vs))
    476401]. nwhd; //;
    477 napply sig_bind_OK; #v ev Hv;
    478 napply sig_bind_OK; #vs evs Hvs;
     402napply sig_bind_OK; #v Hv;
     403napply sig_bind_OK; #vs Hvs;
    479404nnormalize; /2/;
    480405nqed.
     
    489414| cons h vars ⇒
    490415  match h with [ mk_pair id ty ⇒
    491     match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
    492       match exec_alloc_variables (set … id b1 en) m1 vars with
     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
    493418      [ sig_intro r p ⇒ r ]
    494419]]]. nwhd; //;
    495 nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
     420nelim (exec_alloc_variables (set ident ? ? c3 〈UnspecifiedB,c7〉 en) c6 c1);
    496421#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
    497422napply (alloc_variables_cons … IH); /2/;
     
    506431      [ nil ⇒ Some ? (Error ?)
    507432      | cons v1 vl ⇒ Some ? (
    508           b ← opt_to_res ? (get … id e);:
    509           m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
     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);:
    510435          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
    511436      ]
    512437  ] ].
    513438nwhd; //;
    514 napply opt_bind_OK; #b eb;
     439napply opt_bind_OK; #x; ncases x; #bcl b eb;
    515440napply opt_bind_OK; #m1 em1;
    516441napply reinject; #m2 em2 Hm2;
     
    549474ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
    550475#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
     476ndefinition ms_eq_dec : ∀s1,s2:mem_space. (s1 = s2) + (s1 ≠ s2).
     477#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
    551478
    552479nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
     
    555482| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    556483| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    557 | Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
    558 | Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
    559     match assert_type_eq t t' with [ OK _ ⇒
    560       match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     484| Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒
     485    match ms_eq_dec s s' with [ inl _ ⇒
     486      match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     487| Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
     488    match ms_eq_dec s s' with [ inl _ ⇒
     489      match assert_type_eq t t' with [ OK _ ⇒
     490        match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
    561491| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
    562492    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
     
    652582  ]
    653583]. nwhd; //;
    654 napply sig_bind_OK; #ev eev Hev;
    655 napply sig_bind_OK; #evt eevt Hevt;
     584napply sig_bind_OK; #ev Hev;
     585napply sig_bind_OK; #evt Hevt;
    656586nnormalize; /2/;
    657587nqed.
    658588
    659589(* execution *)
     590
     591ndefinition store_value_of_type' ≝
     592λty,m,l,v.
     593match l with [ mk_pair pl ofs ⇒
     594  match pl with [ mk_pair pcl loc ⇒
     595    store_value_of_type ty m pcl loc ofs v ] ].
    660596
    661597nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     
    664600  match s with
    665601  [ Sassign a1 a2 ⇒ Some ? (
    666     ! 〈loc, ofs〉 ← exec_lvalue ge e m a1;:
     602    ! l ← exec_lvalue ge e m a1;:
    667603    ! v2 ← exec_expr ge e m a2;:
    668     ! m' ← store_value_of_type (typeof a1) m loc ofs v2;:
     604    ! m' ← store_value_of_type' (typeof a1) m l v2;:
    669605    ret ? 〈E0, State f Sskip k e m'〉)
    670606  | Scall lhs a al ⇒ Some ? (
     
    802738      ]
    803739    | Some r' ⇒
    804       match r' with [ mk_pair locofs ty ⇒
    805         match locofs with [ mk_pair loc ofs ⇒ Some ? (
    806           ! m' ← store_value_of_type ty m loc ofs res;:
     740      match r' with [ mk_pair l ty ⇒
     741        Some ? (
     742          ! m' ← store_value_of_type' ty m l res;:
    807743          ret ? 〈E0, (State f Sskip k' e m')〉)
    808         ]
    809744      ]
    810745    ]
     
    824759##| napply step_skip_break_switch; @; //;
    825760##| nrewrite > c11; napply step_skip_call; //; napply c12;
    826 ##| napply sig_bindIO2_OK; #loc ofs Hlval;
     761##| napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlval;
    827762    napply sig_bindIO_OK; #v2 Hv2;
    828763    napply opt_bindIO_OK; #m' em';
     
    835770    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    836771    ##| #lhs';
    837         napply sig_bindIO_OK; #locofs; ncases locofs; #loc ofs Hlocofs;
     772        napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlocofs;
    838773        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    839774    ##]
     
    879814    napply sig_bindIO_OK; #res Hres;
    880815    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
    881 ##| napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //;
     816##| ncases c11; #x; ncases x; #pcl b ofs;
     817    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
    882818##]
    883819nqed.
     
    905841    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    906842    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    907     ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
     843    ##| #pcl b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
    908844    ##]
    909845  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
  • C-semantics/Csem.ma

    r13 r124  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint zero) (Tint sz sg)
    41   | is_false_pointer: ∀t.
    42       is_false (Vint zero) (Tpointer t)
     41  | is_false_pointer: ∀s,t.
     42      is_false (Vint zero) (Tpointer s t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
     
    4848      n ≠ zero →
    4949      is_true (Vint n) (Tint sz sg)
    50   | is_true_pointer_int: ∀b,ofs,sz,sg.
    51       is_true (Vptr b ofs) (Tint sz sg)
    52   | is_true_int_pointer: ∀n,t.
     50  | is_true_pointer_int: ∀pcl,b,ofs,sz,sg.
     51      is_true (Vptr pcl b ofs) (Tint sz sg)
     52  | is_true_int_pointer: ∀n,s,t.
    5353      n ≠ zero →
    54       is_true (Vint n) (Tpointer t)
    55   | is_true_pointer_pointer: ∀b,ofs,t.
    56       is_true (Vptr b ofs) (Tpointer t)
     54      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)
    5757  | is_true_float: ∀f,sz.
    5858      f ≠ Fzero →
     
    101101      match v with
    102102      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    103       | Vptr _ _ ⇒ Some ? Vfalse
     103      | Vptr _ _ _ ⇒ Some ? Vfalse
    104104      | _ ⇒ None ?
    105105      ]
    106   | Tpointer _
     106  | Tpointer _ _
    107107      match v with
    108108      [ Vint n ⇒ Some ? (of_bool (eq n zero))
    109       | Vptr _ _ ⇒ Some ? Vfalse
     109      | Vptr _ _ _ ⇒ Some ? Vfalse
    110110      | _ ⇒ None ?
    111111      ]
     
    134134  | add_case_pi ty ⇒                    (**r pointer plus integer *)
    135135      match v1 with
    136       [ Vptr b1 ofs1 ⇒ match v2 with
    137         [ Vint n2 ⇒ Some ? (Vptr b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
     136      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     137        [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2)))
    138138        | _ ⇒ None ? ]
    139139      | _ ⇒ None ? ]
     
    141141      match v1 with
    142142      [ Vint n1 ⇒ match v2 with
    143         [ Vptr b2 ofs2 ⇒ Some ? (Vptr b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
     143        [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1)))
    144144        | _ ⇒ None ? ]
    145145      | _ ⇒ None ? ]
     
    163163  | sub_case_pi ty ⇒             (**r pointer minus integer *)
    164164      match v1 with
    165       [ Vptr b1 ofs1 ⇒ match v2 with
    166         [ Vint n2 ⇒ Some ? (Vptr b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
     165      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     166        [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))
    167167        | _ ⇒ None ? ]
    168168      | _ ⇒ None ? ]
    169169  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
    170170      match v1 with
    171       [ Vptr b1 ofs1 ⇒ match v2 with
    172         [ Vptr b2 ofs2 ⇒
     171      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
     172        [ Vptr pcl2 b2 ofs2 ⇒
    173173          if eqZb b1 b2 then
    174174            if eq (repr (sizeof ty)) zero then None ?
     
    179179  | sub_default ⇒ None ?
    180180  ].
    181  
     181
    182182nlet rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
    183183 match classify_mul t1 t2 with
     
    313313      [ Vint n1 ⇒ match v2 with
    314314         [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
    315          | Vptr b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
     315         | Vptr pcl b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?
    316316         | _ ⇒ None ?
    317317         ]
    318       | Vptr b1 ofs1 ⇒
     318      | Vptr pcl1 b1 ofs1 ⇒
    319319        match v2 with
    320         [ Vptr b2 ofs2 ⇒
    321           if valid_pointer m b1 (signed ofs1)
    322           ∧ valid_pointer m b2 (signed ofs2) then
     320        [ Vptr pcl2 b2 ofs2 ⇒
     321          if valid_pointer m pcl1 b1 (signed ofs1)
     322          ∧ valid_pointer m pcl2 b2 (signed ofs2) then
    323323            if eqZb b1 b2
    324324            then Some ? (of_bool (cmp c ofs1 ofs2))
     
    400400  ].
    401401
    402 ninductive neutral_for_cast: type → Prop ≝
    403   | nfc_int: ∀sg.
    404       neutral_for_cast (Tint I32 sg)
    405   | nfc_ptr: ∀ty.
    406       neutral_for_cast (Tpointer ty)
    407   | nfc_array: ∀ty,sz.
    408       neutral_for_cast (Tarray ty sz)
    409   | nfc_fun: ∀targs,tres.
    410       neutral_for_cast (Tfunction targs tres).
    411 
    412 ninductive cast : val → type → type → val → Prop ≝
    413   | cast_ii:   ∀i,sz2,sz1,si1,si2.            (**r int to int  *)
    414       cast (Vint i) (Tint sz1 si1) (Tint sz2 si2)
     402(* XXX should go somewhere else? *)
     403ndefinition 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].
     411ndefinition 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
     420ndefinition 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
     429ninductive type_pointable : type → Prop ≝
     430| type_ptr_int : type_pointable (Tint I32 Unsigned)
     431| type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t)
     432| type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n)
     433| type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty).
     434
     435ninductive type_space : type → mem_space → Prop ≝
     436| type_spc_int : type_space (Tint I32 Unsigned) Generic
     437| type_spc_pointer : ∀s,t. type_space (Tpointer s t) s
     438| type_spc_array : ∀s,t,n. type_space (Tarray s t n) s
     439| type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code.
     440
     441ninductive cast : mem → val → type → type → val → Prop ≝
     442  | cast_ii:   ∀m,i,sz2,sz1,si1,si2.            (**r int to int  *)
     443      cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2)
    415444           (Vint (cast_int_int sz2 si2 i))
    416   | cast_fi:   ∀f,sz1,sz2,si2.                (**r float to int *)
    417       cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
     445  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
     446      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
    418447           (Vint (cast_int_int sz2 si2 (cast_float_int si2 f)))
    419   | cast_if:   ∀i,sz1,sz2,si1.                (**r int to float  *)
    420       cast (Vint i) (Tint sz1 si1) (Tfloat sz2)
     448  | cast_if:   ∀m,i,sz1,sz2,si1.                (**r int to float  *)
     449      cast m (Vint i) (Tint sz1 si1) (Tfloat sz2)
    421450          (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
    422   | cast_ff:   ∀f,sz1,sz2.                    (**r float to float *)
    423       cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)
     451  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
     452      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    424453           (Vfloat (cast_float_float sz2 f))
    425   | cast_nn_p: ∀b,ofs,t1,t2. (**r no change in data representation *)
     454  | cast_pp: ∀m,pcl,psp,ty,ty',b,ofs.
     455      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)
     459  | cast_pp_z: ∀m,ty,ty'.
     460      type_pointable ty → (* Don't care which space it is for the source type *)
     461      type_pointable ty' →
     462      cast m (Vint zero) ty ty' (Vint zero).
     463(* XXX: other integers?
     464  | cast_nn_i: ∀m,n,t1,t2.     (**r no change in data representation *)
    426465      neutral_for_cast t1 → neutral_for_cast t2 →
    427       cast (Vptr b ofs) t1 t2 (Vptr b ofs)
    428   | cast_nn_i: ∀n,t1,t2.     (**r no change in data representation *)
    429       neutral_for_cast t1 → neutral_for_cast t2 →
    430       cast (Vint n) t1 t2 (Vint n).
    431 
     466      cast m (Vint n) t1 t2 (Vint n).
     467*)
    432468(* * * Operational semantics *)
    433469
     
    442478  block. *)
    443479
    444 ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
     480ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable -> location *)
    445481
    446482ndefinition empty_env: env ≝ (empty …).
     
    452488  reference, the pointer [Vptr b ofs] is returned. *)
    453489
    454 nlet rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
     490nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝
    455491  match access_mode ty with
    456   [ By_value chunk ⇒ loadv chunk m (Vptr b ofs)
    457   | By_reference ⇒ Some ? (Vptr b ofs)
     492  [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs)
     493  | By_reference ⇒ Some ? (Vptr pcl b ofs)
    458494  | By_nothing ⇒ None ?
    459495  ].
     
    464500  This is allowed only if [ty] indicates an access by value. *)
    465501
    466 nlet rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
     502nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝
    467503  match access_mode ty_dest with
    468   [ By_value chunk ⇒ storev chunk m (Vptr loc ofs) v
     504  [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v
    469505  | By_reference ⇒ None ?
    470506  | By_nothing ⇒ None ?
     
    486522  | alloc_variables_cons:
    487523      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    488       alloc m 0 (sizeof ty) = 〈m1, b1〉 →
    489       alloc_variables (set … id b1 e) m1 vars e2 m2 →
     524      alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)
     525      alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 →
    490526      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    491527
     
    502538      bind_parameters e m (nil ?) (nil ?) m
    503539  | bind_parameters_cons:
    504       ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    505       get ??? id e = Some ? b
    506       store_value_of_type ty m b zero v1 = Some ? m1 →
     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 →
    507543      bind_parameters e m1 params vl m2 →
    508544      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
     
    511547
    512548ndefinition blocks_of_env : env → list block ≝ λe.
    513   map ?? (snd ident block) (elements ??? e).
     549  map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).
    514550
    515551(* * Selection of the appropriate case of a [switch], given the value [n]
     
    552588  | eval_Econst_float:   ∀f,ty.
    553589      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f)
    554   | eval_Elvalue: ∀a,ty,loc,ofs,v.
    555       eval_lvalue ge e m (Expr a ty) loc ofs ->
    556       load_value_of_type ty m loc ofs = Some ? v ->
     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 ->
    557593      eval_expr ge e m (Expr a ty) v
    558   | eval_Eaddrof: ∀a,ty,loc,ofs.
    559       eval_lvalue ge e m a loc ofs ->
    560       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr loc ofs)
     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)
    561597  | eval_Esizeof: ∀ty',ty.
    562598      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty')))
     
    602638  | eval_Ecast:   ∀a,ty,ty',v1,v.
    603639      eval_expr ge e m a v1 ->
    604       cast v1 (typeof a) ty v ->
     640      cast m v1 (typeof a) ty v ->
    605641      eval_expr ge e m (Expr (Ecast ty a) ty') v
    606642
     
    609645  that contains the value of the expression [a]. *)
    610646
    611 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝
    612   | eval_Evar_local:   ∀id,l,ty.
    613       (* XXX notation? e!id*) get ??? id e = Some ? l ->
    614       eval_lvalue ge e m (Expr (Evar id) ty) l zero
     647with 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
    615651  | eval_Evar_global: ∀id,l,ty.
    616652      (* XXX e!id *) get ??? id e = None ? ->
    617653      find_symbol ?? ge id = Some ? l ->
    618       eval_lvalue ge e m (Expr (Evar id) ty) l zero
    619   | eval_Ederef: ∀a,ty,l,ofs.
    620       eval_expr ge e m a (Vptr l ofs) ->
    621       eval_lvalue ge e m (Expr (Ederef a) ty) l ofs
    622  | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta.
    623       eval_lvalue ge e m a l ofs ->
     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 ->
    624660      typeof a = Tstruct id fList ->
    625661      field_offset i fList = OK ? delta ->
    626       eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta))
    627  | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList.
    628       eval_lvalue ge e m a l ofs ->
     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 ->
    629665      typeof a = Tunion id fList ->
    630       eval_lvalue ge e m (Expr (Efield a i) ty) l ofs.
     666      eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs.
    631667
    632668(*
     
    666702  | Kswitch: cont -> cont
    667703       (**r catches [break] statements arising out of [switch] *)
    668   | Kcall: option (block × int × type) ->   (**r where to store result *)
     704  | Kcall: option (ptr_class × block × int × type) ->   (**r where to store result *)
    669705           function ->                      (**r calling function *)
    670706           env ->                           (**r local env of calling function *)
     
    764800ninductive step (ge:genv) : state -> trace -> state -> Prop :=
    765801
    766   | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m'.
    767       eval_lvalue ge e m a1 loc ofs ->
     802  | step_assign:   ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'.
     803      eval_lvalue ge e m a1 pcl loc ofs ->
    768804      eval_expr ge e m a2 v2 ->
    769       store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' ->
     805      store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' ->
    770806      step ge (State f (Sassign a1 a2) k e m)
    771807           E0 (State f Sskip k e m')
     
    779815           E0 (Callstate fd vargs (Kcall (None ?) f e k) m)
    780816
    781   | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd.
    782       eval_lvalue ge e m lhs loc ofs ->
     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 ->
    783819      eval_expr ge e m a vf ->
    784820      eval_exprlist ge e m al vargs ->
     
    786822      type_of_fundef fd = typeof a ->
    787823      step ge (State f (Scall (Some ? lhs) a al) k e m)
    788            E0 (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     824           E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m)
    789825
    790826  | step_seq:  ∀f,s1,s2,k,e,m.
     
    925961           E0 (State f Sskip k e m)
    926962
    927   | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
    928       store_value_of_type ty m loc ofs v = Some ? m' ->
    929       step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
     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)
    930966           E0 (State f Sskip k e m').
    931967(*
  • C-semantics/Csyntax.ma

    r24 r124  
    4646  | F32: floatsize
    4747  | F64: floatsize.
     48
     49(* Pointers can point to particular memory spaces. *)
     50ninductive mem_space : Type ≝
     51  | Generic : mem_space
     52  | Data : mem_space
     53  | IData : mem_space
     54  | XData : mem_space
     55  | Code : mem_space.
    4856
    4957(* * The syntax of type expressions.  Some points to note:
     
    8694  | Tint: intsize → signedness → type   (**r integer types *)
    8795  | Tfloat: floatsize → type            (**r floating-point types *)
    88   | Tpointer: type → type               (**r pointer types ([*ty]) *)
    89   | Tarray: type → Z → type            (**r array types ([ty[len]]) *)
     96  | Tpointer: mem_space → type → type   (**r pointer types ([*ty]) *)
     97  | Tarray: mem_space → type → Z → type (**r array types ([ty[len]]) *)
    9098  | Tfunction: typelist → type → type   (**r function types *)
    9199  | Tstruct: ident → fieldlist → type   (**r struct types *)
     
    107115  (it:∀i,s. P (Tint i s))
    108116  (fl:∀f. P (Tfloat f))
    109   (pt:∀t. P t → P (Tpointer t))
    110   (ar:∀t,n. P t → P (Tarray t n))
     117  (pt:∀s,t. P t → P (Tpointer s t))
     118  (ar:∀s,t,n. P t → P (Tarray s t n))
    111119  (fn:∀tl,t. P t → P (Tfunction tl t))
    112120  (st:∀i,fl. P (Tstruct i fl))
     
    118126  | Tint i s ⇒ it i s
    119127  | Tfloat s ⇒ fl s
    120   | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
    121   | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
     128  | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
     129  | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
    122130  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
    123131  | Tstruct i fs ⇒ st i fs
     
    357365  | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    358366  | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    359   | Tpointer _ ⇒ 4
    360   | Tarray t' n ⇒ alignof t'
     367  | Tpointer _ _ ⇒ 4
     368  | Tarray _ t' n ⇒ alignof t'
    361369  | Tfunction _ _ ⇒ 1
    362370  | Tstruct _ fld ⇒ alignof_fields fld
     
    382390  (it:∀i,s. P (Tint i s))
    383391  (fl:∀f. P (Tfloat f))
    384   (pt:∀t. P t → P (Tpointer t))
    385   (ar:∀t,n. P t → P (Tarray t n))
     392  (pt:∀s,t. P t → P (Tpointer s t))
     393  (ar:∀s,t,n. P t → P (Tarray s t n))
    386394  (fn:∀tl,t. P t → P (Tfunction tl t))
    387395  (st:∀i,fl. Q fl → P (Tstruct i fl))
     
    395403  | Tint i s ⇒ it i s
    396404  | Tfloat s ⇒ fl s
    397   | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    398   | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     405  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     406  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    399407  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    400408  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
     
    407415  (it:∀i,s. P (Tint i s))
    408416  (fl:∀f. P (Tfloat f))
    409   (pt:∀t. P t → P (Tpointer t))
    410   (ar:∀t,n. P t → P (Tarray t n))
     417  (pt:∀s,t. P t → P (Tpointer s t))
     418  (ar:∀s,t,n. P t → P (Tarray s t n))
    411419  (fn:∀tl,t. P t → P (Tfunction tl t))
    412420  (st:∀i,fl. Q fl → P (Tstruct i fl))
     
    442450  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    443451  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    444   | Tpointer _ ⇒ 4
    445   | Tarray t' n ⇒ sizeof t' * Zmax 1 n
     452  | Tpointer _ _ ⇒ 4
     453  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
    446454  | Tfunction _ _ ⇒ 1
    447455  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
     
    631639                            | F64 ⇒ By_value Mfloat64 ]
    632640  | Tvoid ⇒ By_nothing
    633   | Tpointer _ ⇒ By_value Mint32
    634   | Tarray _ _ ⇒ By_reference
     641  | Tpointer _ _ ⇒ By_value Mint32
     642  | Tarray _ _ _ ⇒ By_reference
    635643  | Tfunction _ _ ⇒ By_reference
    636644  | Tstruct _ fList ⇒ By_nothing
     
    672680    match ty2 with
    673681    [ Tint _ _ ⇒ add_case_ii
    674     | Tpointer ty ⇒ add_case_ip ty
    675     | Tarray ty _ ⇒ add_case_ip ty
     682    | Tpointer _ ty ⇒ add_case_ip ty
     683    | Tarray _ ty _ ⇒ add_case_ip ty
    676684    | _ ⇒ add_default ]
    677685  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
    678   | Tpointer ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
    679   | Tarray ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
     686  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
     687  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
    680688  | _ ⇒ add_default
    681689  ].
     
    704712  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
    705713  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
    706   | Tpointer ty ⇒
     714  | Tpointer _ ty ⇒
    707715    match ty2 with
    708716    [ Tint _ _ ⇒ sub_case_pi ty
    709     | Tpointer _ ⇒ sub_case_pp ty
    710     | Tarray _ _ ⇒ sub_case_pp ty
     717    | Tpointer _ _ ⇒ sub_case_pp ty
     718    | Tarray _ _ _ ⇒ sub_case_pp ty
    711719    | _ ⇒ sub_default ]
    712   | Tarray ty _ ⇒
     720  | Tarray _ ty _ ⇒
    713721    match ty2 with
    714722    [ Tint _ _ ⇒ sub_case_pi ty
    715     | Tpointer _ ⇒ sub_case_pp ty
    716     | Tarray _ _ ⇒ sub_case_pp ty
     723    | Tpointer _ _ ⇒ sub_case_pp ty
     724    | Tarray _ _ _ ⇒ sub_case_pp ty
    717725    | _ ⇒ sub_default ]
    718726  | _ ⇒ sub_default
     
    831839    | _ ⇒ cmp_default ]
    832840  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
    833   | Tpointer _
     841  | Tpointer _ _
    834842    match ty2 with
    835843    [ Tint _ _ ⇒ cmp_case_ipip
    836     | Tpointer _ ⇒ cmp_case_ipip
    837     | Tarray _ _ ⇒ cmp_case_ipip
     844    | Tpointer _ _ ⇒ cmp_case_ipip
     845    | Tarray _ _ _ ⇒ cmp_case_ipip
    838846    | _ ⇒ cmp_default ]
    839   | Tarray _ _
     847  | Tarray _ _ _
    840848    match ty2 with
    841849    [ Tint _ _ ⇒ cmp_case_ipip
    842     | Tpointer _ ⇒ cmp_case_ipip
    843     | Tarray _ _ ⇒ cmp_case_ipip
     850    | Tpointer _ _ ⇒ cmp_case_ipip
     851    | Tarray _ _ _ ⇒ cmp_case_ipip
    844852    | _ ⇒ cmp_default ]
    845853  | _ ⇒ cmp_default
     
    869877  match ty with
    870878  [ Tfunction args res ⇒ fun_case_f args res
    871   | Tpointer ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
    872                                   | _ ⇒ fun_default
    873                                   ]
     879  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
     880                                    | _ ⇒ fun_default
     881                                    ]
    874882  | _ ⇒ fun_default
    875883  ].
  • C-semantics/Globalenvs.ma

    r24 r124  
    330330  (λF,V,p. empty)  (* init_mem *)
    331331  (λF,ge. functions ? ge) (* find_funct_ptr *)
    332   (λF,ge,v. match v with [ Vptr b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     332  (λF,ge,v. match v with [ Vptr _ b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    333333  (λF,ge. symbols ? ge) (* find_symbol *)
    334334  ?
     
    359359    ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    360360    ##| ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    361     ##| #b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
     361    ##| #pcl b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
    362362        nwhd in ⊢ (??%? → ??%?);
    363363        ##[ nelim p; #fns main vars; nelim fns;
     
    420420  ##[ nnormalize; #H; ndestruct;
    421421  ##| ##2,3: #x; nnormalize; #H; ndestruct;
    422   ##| #b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
     422  ##| #pcl b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
    423423    ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
    424424      nelim fns;
  • C-semantics/Mem.ma

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

    r14 r124  
    3636*)
    3737
     38ninductive 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
     46ninductive 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
     51nlemma ptr_class_compat_sym : ∀p,p'. ptr_class_compat p p' → ptr_class_compat p' p.
     52#p p' H; ninversion H; //; nqed.
     53
     54(* TODO: should comparison and subtraction of pointers of different sorts
     55         be supported? *)
     56
    3857ninductive val: Type[0] ≝
    3958  | Vundef: val
    4059  | Vint: int -> val
    4160  | Vfloat: float -> val
    42   | Vptr: block -> int -> val.
     61  | Vptr: ptr_class → block -> int -> val.
    4362
    4463ndefinition Vzero: val ≝ Vint zero.
     
    6382  | Vint _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
    6483  | Vfloat _ ⇒ match t with [ Tfloat ⇒ True | _ ⇒ False ]
    65   | Vptr _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
     84  | Vptr _ _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
    6685  | _ ⇒ False
    6786  ].
     
    81100  match v with
    82101  [ Vint n ⇒ n ≠ zero
    83   | Vptr b ofs ⇒ True
     102  | Vptr _ b ofs ⇒ True
    84103  | _ ⇒ False
    85104  ].
     
    97116      bool_of_val (Vint zero) false
    98117  | bool_of_val_ptr:
    99       ∀b,ofs. bool_of_val (Vptr b ofs) true.
     118      ∀pty,b,ofs. bool_of_val (Vptr pty b ofs) true.
    100119
    101120ndefinition neg : val → val ≝ λv.
     
    152171  match v with
    153172  [ Vint n ⇒ of_bool (int_eq n zero)
    154   | Vptr b ofs ⇒ Vfalse
     173  | Vptr _ b ofs ⇒ Vfalse
    155174  | _ ⇒ Vundef
    156175  ].
     
    178197  [ Vint n1 ⇒ match v2 with
    179198    [ Vint n2 ⇒ Vint (add n1 n2)
    180     | Vptr b2 ofs2 ⇒ Vptr b2 (add ofs2 n1)
    181     | _ ⇒ Vundef ]
    182   | Vptr b1 ofs1 ⇒ match v2 with
    183     [ Vint n2 ⇒ Vptr b1 (add ofs1 n2)
     199    | Vptr pty b2 ofs2 ⇒ Vptr pty b2 (add ofs2 n1)
     200    | _ ⇒ Vundef ]
     201  | Vptr pty b1 ofs1 ⇒ match v2 with
     202    [ Vint n2 ⇒ Vptr pty b1 (add ofs1 n2)
    184203    | _ ⇒ Vundef ]
    185204  | _ ⇒ Vundef ].
     
    190209    [ Vint n2 ⇒ Vint (sub n1 n2)
    191210    | _ ⇒ Vundef ]
    192   | Vptr b1 ofs1 ⇒ match v2 with
    193     [ Vint n2 ⇒ Vptr b1 (sub ofs1 n2)
    194     | Vptr b2 ofs2 ⇒
     211  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     212    [ Vint n2 ⇒ Vptr pty1 b1 (sub ofs1 n2)
     213    | Vptr pty2 b2 ofs2 ⇒
    195214        if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    196215    | _ ⇒ Vundef ]
     
    352371  [ Vint n1 ⇒ match v2 with
    353372    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    354     | Vptr b2 ofs2 ⇒
     373    | Vptr pty2 b2 ofs2 ⇒
    355374        if eq n1 zero then cmp_mismatch c else Vundef
    356375    | _ ⇒ Vundef ]
    357   | Vptr b1 ofs1 ⇒ match v2 with
    358     [ Vptr b2 ofs2 ⇒
     376  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     377    [ Vptr pty2 b2 ofs2 ⇒
    359378        if eqZb b1 b2
    360379        then of_bool (cmp c ofs1 ofs2)
     
    369388  [ Vint n1 ⇒ match v2 with
    370389    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    371     | Vptr b2 ofs2 ⇒
     390    | Vptr pty2 b2 ofs2 ⇒
    372391        if eq n1 zero then cmp_mismatch c else Vundef
    373392    | _ ⇒ Vundef ]
    374   | Vptr b1 ofs1 ⇒ match v2 with
    375     [ Vptr b2 ofs2 ⇒
     393  | Vptr pty1 b1 ofs1 ⇒ match v2 with
     394    [ Vptr pty2 b2 ofs2 ⇒
    376395        if eqZb b1 b2
    377396        then of_bool (cmpu c ofs1 ofs2)
     
    409428    | _ ⇒ Vundef
    410429    ]
    411   | Vptr b ofs ⇒
     430  | Vptr pty b ofs ⇒
    412431    match chunk with
    413     [ Mint32 ⇒ Vptr b ofs
     432    [ Mint32 ⇒ Vptr pty b ofs
    414433    | _ ⇒ Vundef
    415434    ]
  • C-semantics/test/io2.c.ma

    r20 r124  
    3636interpretation "hide memory" 'mem = (mk_mem ???).
    3737
     38ninductive result (T:Type) : T → Prop ≝
     39| witness : ∀t:T. result T t.
     40
    3841(* The trick to being able to normalize the term is to avoid looking at the
    3942   continuations! *)
    4043nremark foo:
    41     match match s with [ Interact f args k ⇒ k (EVint (repr 10))
    42                  | Value v ⇒ Wrong ?
    43                  | Wrong ⇒ Wrong ? ] with
    44     [ Interact _ _ _ ⇒ False
    45     | Value v ⇒ v = v
     44    match match s with [ Interact call k ⇒ k (EVint (repr 10))
     45                 | Value v ⇒ Wrong ???
     46                 | Wrong ⇒ Wrong ??? ] with
     47    [ Interact _ _ ⇒ False
     48    | Value v ⇒ result ? v
    4649    | Wrong ⇒ False
    4750    ].
Note: See TracChangeset for help on using the changeset viewer.