Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (8 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

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

    r485 r487  
    11include "Cexec.ma".
    22
    3 include "Plogic/connectives.ma".
    4 
    5 nlemma exec_bool_of_val_sound: ∀v,ty,r.
     3(*include "Plogic/connectives.ma".*)
     4
     5lemma exec_bool_of_val_sound: ∀v,ty,r.
    66 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    7 #v ty r;
    8 ncases v; ##[ ##| #i ##| #f ##| #r1 ##| #r b of ##]
    9 ncases ty; ##[ ##2,11,20,29,38: #sz sg ##| ##3,12,21,30,39: #sz ##| ##4,13,22,31,40: #r ty ##| ##5,14,23,32,41: #r ty n ##| ##6,15,24,33,42: #args rty ##| ##7,8,16,17,25,26,34,35,43,44: #id fs ##| ##9,18,27,36,45: #r id ##]
    10 #H; nwhd in H:(??%?); ndestruct;
    11 ##[ nlapply (eq_spec i zero); nelim (eq i zero);
    12   ##[ #e; nrewrite > e; napply bool_of_val_false; //;
    13   ##| #ne; napply bool_of_val_true; /2/;
    14   ##]
    15 ##| nelim (eq_dec f Fzero);
    16   ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
    17   ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
    18   ##]
    19 ##| napply bool_of_val_false; //
    20 ##| napply bool_of_val_true; //
    21 ##] nqed.
    22 
    23 nlemma bool_val_distinct: Vtrue ≠ Vfalse.
    24 @; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
    25 nqed.
    26 
    27 nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
     7#v #ty #r
     8cases v; [ | #i | #f | #r1 | #r #b #of ]
     9cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
     10#H whd in H:(??%?); destruct;
     11[ lapply (eq_spec i zero); elim (eq i zero);
     12  [ #e >e @bool_of_val_false //;
     13  | #ne @bool_of_val_true /2/;
     14  ]
     15| elim (eq_dec f Fzero);
     16  [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
     17  | #ne >(Feq_zero_false …) //; @bool_of_val_true /2/;
     18  ]
     19| @bool_of_val_false //
     20| @bool_of_val_true //
     21] qed.
     22
     23lemma bool_val_distinct: Vtrue ≠ Vfalse.
     24% #H whd in H:(??%%); destruct; @(absurd ? e0 one_not_zero)
     25qed.
     26
     27lemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
    2828  if b then is_true v ty else is_false v ty.
    29 #v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
    30 napply False_ind; napply (absurd ? ev ?);
    31 ##[ ##2: napply sym_neq ##] napply bool_val_distinct;
    32 nqed.
    33 
    34 nlemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
    35 #m i ty ty' v';
    36 nwhd in ⊢ (??%? → ?);
    37 nlapply (eq_spec i zero); ncases (eq i zero);
    38 ##[ #e; nrewrite > e;
    39     ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
    40     nwhd in ⊢ (??%? → ?); #H; ndestruct;
    41     ncases ty' in H ⊢ %; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #r id ##]
    42     nwhd in ⊢ (??%? → ?); #H; ndestruct (H); napply cast_ip_z; //;
    43 ##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
    44 ##]
    45 nqed.
    46 
    47 ndefinition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
    48 #m v ty ty' v';
    49 ncases v;
    50 ##[ #H; nwhd in H:(??%?); ndestruct;
    51 ##| #i; ncases ty;
    52   ##[ #H; nwhd in H:(??%?); ndestruct;
    53   ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct;
    54   ##| ##7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct;
    55   ##| #sz1 si1; ncases ty';
    56     ##[ #H; nwhd in H:(??%?); ndestruct;
    57     ##| ##3: #a; #H; nwhd in H:(??%?); ndestruct; //
    58     ##| ##2,7,8,9: #a b; #H; nwhd in H:(??%?); ndestruct; //
    59     ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    60                  ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
    61                  ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
    62         nwhd in ⊢ (??%? → ?);
    63         nlapply (try_cast_null_sound m i (Tint sz1 si1) t v');
    64         ncases (try_cast_null m i (Tint sz1 si1) t);
    65         ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
    66         ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    67         ##]
    68     ##]
    69   ##| ##*: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    70            ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
    71            ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
    72         nwhd in ⊢ (??%? → ?);
    73         nlapply (try_cast_null_sound m i t ty' v');
    74         ncases (try_cast_null m i t ty');
    75         ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
    76         ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    77         ##]
    78   ##]
    79 ##| #f; ncases ty;  ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
    80                     ##[ ncases ty'; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    81                         nwhd in e:(??%?); ndestruct; //;
    82                     ##| ##*: #e; nwhd in e:(??%?); ndestruct
    83                     ##]
    84 ##| #r; ncases ty; ##[ ##3: #x; ##| ##2,4,6,7,8,9: #x y; ##| ##5: #x y z; ##]
    85     nwhd in ⊢ (??%? → ?); #H; ndestruct; ncases (eq_region_dec r ?) in H;
    86     nwhd in ⊢ (? → ??%? → ?); #H1 H2; ndestruct;
    87     ncases ty' in H2; nnormalize; ntry #a; ntry #b; ntry #c; ntry #d; ndestruct;
    88     napply cast_pp_z; //;
    89 ##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
    90     nelim (bind_inversion ????? e); #s; *; #es e';
    91     nelim (bind_inversion ????? e'); #u; *; #eu e'';
    92     nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    93     ncut (type_region ty s);
    94     ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    95         nwhd in e:(??%?); ndestruct; //;
    96     ##| #Hty;
    97         ncut (type_region ty' s');
    98         ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3: #a e; ##| ##2,4,6,7,8,9: #a b e; ##| #a b c e; ##]
    99             nwhd in e:(??%?); ndestruct; //;
    100         ##| #Hty';
    101             ncut (s = sp). nelim (eq_region_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
    102             #e; nrewrite < e;
    103             nwhd in match (is_pointer_compat ??) in e''';
    104             ncases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat e''';
    105             nwhd in e''':(??%?); ndestruct (e'''); /2/
    106         ##]
    107     ##]
    108 ##] nqed.
    109 
    110 nlet rec expr_lvalue_ind
     29#v #ty #b cases b; #H inversion H; #v' #ty' #H' #ev #et #ev //;
     30@False_ind @(absurd ? ev ?)
     31[ 2: @sym_neq ] @bool_val_distinct
     32qed.
     33
     34lemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
     35#m #i #ty #ty' #v'
     36whd in ⊢ (??%? → ?);
     37lapply (eq_spec i zero); cases (eq i zero);
     38[ #e >e
     39    cases ty; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     40    whd in ⊢ (??%? → ?); #H destruct;
     41    cases ty' in H ⊢ %; [ | #sz #sg | #fs | #sp #ty | #sp #ty #n | #args #rty | #id #fs | #id #fs | #r #id ]
     42    whd in ⊢ (??%? → ?); #H destruct (H); @cast_ip_z //;
     43| #_ whd in ⊢ (??%? → ?); #H destruct
     44]
     45qed.
     46
     47definition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
     48#m #v #ty #ty' #v'
     49cases v;
     50[ #H whd in H:(??%?); destruct;
     51| #i cases ty;
     52  [ #H whd in H:(??%?); destruct;
     53  | 3: #a #H whd in H:(??%?); destruct;
     54  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
     55  | #sz1 #si1 cases ty';
     56    [ #H whd in H:(??%?); destruct;
     57    | 3: #a #H whd in H:(??%?); destruct; //
     58    | 2,7,8,9: #a #b #H whd in H:(??%?); destruct; //
     59    | 4,5,6: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
     60                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
     61                 | #args #rty letin t ≝ (Tfunction args rty) ]
     62        whd in ⊢ (??%? → ?);
     63        lapply (try_cast_null_sound m i (Tint sz1 si1) t v');
     64        cases (try_cast_null m i (Tint sz1 si1) t);
     65        [ 1,3,5: #v'' #H' #e @H' @e
     66        | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     67        ]
     68    ]
     69  | *: [ #sp #ty'' letin t ≝ (Tpointer sp ty'')
     70           | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
     71           | #args #rty letin t ≝ (Tfunction args rty) ]
     72        whd in ⊢ (??%? → ?);
     73        lapply (try_cast_null_sound m i t ty' v');
     74        cases (try_cast_null m i t ty');
     75        [ 1,3,5: #v'' #H' #e @H' @e
     76        | *: #_ whd in ⊢ (??%? → ?); #H destruct (H);
     77        ]
     78  ]
     79| #f cases ty;  [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
     80                    [ cases ty'; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     81                        whd in e:(??%?); destruct; //;
     82                    | *: #e whd in e:(??%?); destruct
     83                    ]
     84| #r cases ty; [ 3: #x | 2,4,6,7,8,9: #x #y | 5: #x #y #z ]
     85    whd in ⊢ (??%? → ?); #H destruct; cases (eq_region_dec r ?) in H;
     86    whd in ⊢ (? → ??%? → ?); #H1 #H2 destruct;
     87    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
     88    @cast_pp_z //;
     89| #sp #b #of whd in ⊢ (??%? → ?); #e
     90    elim (bind_inversion ????? e); #s *; #es #e'
     91    elim (bind_inversion ????? e'); #u *; #eu #e''
     92    elim (bind_inversion ????? e''); #s' *; #es' #e'''
     93    cut (type_region ty s);
     94    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     95        whd in e:(??%?); destruct; //;
     96    | #Hty
     97        cut (type_region ty' s');
     98        [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
     99            whd in e:(??%?); destruct; //;
     100        | #Hty'
     101            cut (s = sp). elim (eq_region_dec sp s) in eu; //; normalize; #_ #e destruct.
     102            #e <e
     103            whd in match (is_pointer_compat ??) in e''';
     104            cases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat #e'''
     105            whd in e''':(??%?); destruct (e'''); /2/
     106        ]
     107    ]
     108] qed.
     109
     110let rec expr_lvalue_ind
    111111  (P:expr → Prop)
    112112  (Q:expr_descr → type → Prop)
     
    172172  | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
    173173  | _ ⇒ xx ? ty ?
    174   ]. nwhd; napply I; nqed.
    175 
    176 
    177 ntheorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
     174  ]. whd; @I qed.
     175
     176
     177theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
    178178(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    179 #ge en m e; napply (expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e);
    180 ##[ ##1,2: #ty c; nwhd; //;
     179#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
     180(* XXX // fails [ 1,2: #ty #c whd //  *)
     181[ #ty #c whd %
     182| #ty #c whd %2
    181183(* expressions that are lvalues *)
    182 ##| #e' ty; ncases e'; //; ##[ #i He' ##| #e He' ##| #e i He' ##] nwhd in He' ⊢ %;
    183     napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    184     napply opt_bind_OK;  #vl evl; nwhd in evl:(??%?); napply (eval_Elvalue … evl);
    185     nrewrite > H in He'; #He'; napply He';
    186 ##| #v ty;
    187     nwhd in ⊢ (???%);
    188     nlapply (refl ? (get ident PTree block v en));
    189     ncases (get ident PTree block v en) in ⊢ (???% → %);
    190     ##[ #eget; napply opt_bind_OK; #sploc; ncases sploc; #sp loc efind;
    191         nwhd; napply (eval_Evar_global … eget efind);
    192     ##| #loc eget; napply (eval_Evar_local … eget);
    193     ##]
    194 ##| #ty e He; nwhd in ⊢ (???%);
    195     napply bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
    196     napply eval_Ederef; nrewrite > Hv in He; #He; napply He;
    197 ##| #ty e'' ty'' He''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    198     nwhd; napply eval_Eaddrof; nrewrite > H in He''; #He''; napply He'';
    199 ##| #ty op e1 He1; napply bind2_OK; #v1 tr Hv1;
    200     napply opt_bind_OK; #v ev;
    201     napply (eval_Eunop … ev);
    202     nrewrite > Hv1 in He1; #He1; napply He1;
    203 ##| #ty op e1 e2 He1 He2;
    204     napply bind2_OK; #v1 tr1 ev1; nrewrite > ev1 in He1; #He1;
    205     napply bind2_OK; #v2 tr2 ev2; nrewrite > ev2 in He2; #He2;
    206     napply opt_bind_OK; #v ev; nwhd in He1 He2; nwhd;
    207     napply (eval_Ebinop … He1 He2 ev);
    208 ##| #ty ty' e' He';
    209     napply bind2_OK; #v tr Hv; nrewrite > Hv in He'; #He';
    210     napply bind_OK; #v' ev';
    211     napply (eval_Ecast … He' ?);
    212     /2/;
    213 ##| #ty e1 e2 e3 He1 He2 He3;
    214     napply bind2_OK; #vb tr1 Hvb; nrewrite > Hvb in He1; #He1;
    215     napply bind_OK; #b;
    216     ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    217     napply bind2_OK; #v tr Hv;
    218     ##[ nrewrite > Hv in He2; #He2; nwhd in He2 Hv:(??%?) ⊢%;
    219         napply (eval_Econdition_true … He1 ? He2);  napply (bool_of ??? Hb);
    220     ##| nrewrite > Hv in He3; #He3; nwhd in He3 Hv:(??%?) ⊢%;
    221         napply (eval_Econdition_false … He1 ? He3);  napply (bool_of ??? Hb);
    222     ##]
    223 ##| #ty e1 e2 He1 He2;
    224     napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    225     napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    226     ##[ napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    227         napply bind_OK; #b2 eb2;
    228         napply (eval_Eandbool_2 … He1 … He2);
    229         ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    230     ##| napply (eval_Eandbool_1 … He1); napply (bool_of … Hb1);
    231     ##]
    232 ##| #ty e1 e2 He1 He2;
    233     napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    234     napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    235     ##[ napply (eval_Eorbool_1 … He1); napply (bool_of … Hb1);
    236     ##| napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    237         napply bind_OK; #b2 eb2;
    238         napply (eval_Eorbool_2 … He1 … He2);
    239         ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    240     ##]
    241 ##| #ty ty'; nwhd; //
    242 ##| #ty e' ty' i; ncases ty'; //;
    243     ##[ #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
    244         napply bind_OK; #delta Hdelta; nrewrite > H in He'; #He';
    245         napply (eval_Efield_struct …  He' (refl ??) Hdelta);
    246     ##| #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
    247         nrewrite > H in He'; #He';
    248         napply (eval_Efield_union … He' (refl ??));
    249     ##]
    250 ##| #ty l e' He'; napply bind2_OK; #v tr1 H; nrewrite > H in He'; #He';
    251     napply (eval_Ecost … He');
     184| #e' #ty cases e'; //; [ #i #He' | #e #He' | #e #i #He' ] whd in He' ⊢ %;
     185    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
     186    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
     187    >H in He' #He' @He'
     188| #v #ty
     189    whd in ⊢ (???%);
     190    lapply (refl ? (get ident PTree block v en));
     191    cases (get ident PTree block v en) in ⊢ (???% → %);
     192    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
     193        whd; @(eval_Evar_global … eget efind)
     194    | #loc #eget @(eval_Evar_local … eget)
     195    ]
     196| #ty #e #He whd in ⊢ (???%);
     197    @bind2_OK #v cases v; //; #sp #l #ofs #tr #Hv whd;
     198    @eval_Ederef >Hv in He #He @He
     199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
     200    whd; @eval_Eaddrof >H in He'' #He'' @He''
     201| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
     202    @opt_bind_OK #v #ev
     203    @(eval_Eunop … ev)
     204    >Hv1 in He1 #He1 @He1
     205| #ty #op #e1 #e2 #He1 #He2
     206    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
     207    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
     208    @opt_bind_OK #v #ev whd in He1 He2; whd;
     209    @(eval_Ebinop … He1 He2 ev)
     210| #ty #ty' #e' #He'
     211    @bind2_OK #v #tr #Hv >Hv in He' #He'
     212    @bind_OK #v' #ev'
     213    @(eval_Ecast … He' ?)
     214    (* XXX /2/; *)
     215    @(exec_cast_sound … ev')
     216| #ty #e1 #e2 #e3 #He1 #He2 #He3
     217    @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
     218    @bind_OK #b
     219    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     220    @bind2_OK #v #tr #Hv
     221    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
     222        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
     223    | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
     224        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
     225    ]
     226| #ty #e1 #e2 #He1 #He2
     227    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     228    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
     229    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     230        @bind_OK #b2 #eb2
     231        @(eval_Eandbool_2 … He1 … He2)
     232        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     233    | @(eval_Eandbool_1 … He1) @(bool_of … Hb1)
     234    ]
     235| #ty #e1 #e2 #He1 #He2
     236    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     237    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
     238    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
     239    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     240        @bind_OK #b2 #eb2
     241        @(eval_Eorbool_2 … He1 … He2)
     242        [ @(bool_of … Hb1) | @(exec_bool_of_val_sound … eb2) ]
     243    ]
     244| #ty #ty' whd; (* XXX //*) @eval_Esizeof
     245| #ty #e' #ty' #i cases ty'; //;
     246    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     247        @bind_OK #delta #Hdelta >H in He' #He'
     248        @(eval_Efield_struct …  He' (refl ??) Hdelta)
     249    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     250        >H in He' #He'
     251        @(eval_Efield_union … He' (refl ??))
     252    ]
     253| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
     254    @(eval_Ecost … He')
    252255(* exec_lvalue fails on non-lvalues. *)
    253 ##| #e' ty; ncases e';
    254     ##[ ##1,2,5,12: #a H ##| ##3,4: #a; * ##| ##13,14: #a b; * ##| ##6,8,10,11: #a b H ##| ##7,9: #a b c H ##]
    255     napply I;
    256 ##] nqed.
    257 
    258 nlemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
     256| #e' #ty cases e';
     257    [ 1,2,5,12: #a #H | 3,4: #a * | 13,14: #a #b * | 6,8,10,11: #a #b #H | 7,9: #a #b #c #H ]
     258    @I
     259] qed.
     260
     261lemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    259262eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
    260263eval_lvalue ge en m e sp loc off tr.
    261 #ge en m e sp loc off tr ty H; ninversion H;
    262 ##[ ##1,2,5: #a b H; napply False_ind; ndestruct (H);
    263 ##| #a b c d e f g H1 i H2; nrewrite < H2 in H1; #H1; napply False_ind;
    264     napply (eval_lvalue_inv_ind … H1);
    265     ##[ #a b c d bad; ndestruct (bad);
    266     ##| #a b c d e f bad; ndestruct (bad);
    267     ##| #a b c d e f g bad; ndestruct (bad);
    268     ##| #a b c d e f g  h i j k l m n bad; napply False_ind; ndestruct (bad);
    269     ##| #a b c d e f g h i j k l bad; ndestruct (bad);
    270     ##]
    271 ##| #e' ty' sp' loc' ofs' tr' H e1 e2 e3; ndestruct (e1 e2 e3); napply H;
    272 ##| #a b c d e f g h i bad; ndestruct (bad);
    273 ##| #a b c d e f g h i j k l k l bad; ndestruct (bad);
    274 ##| #a b c d e f g h i j k l m bad; ndestruct (bad);
    275 ##| #a b c d e f g h i j k l m bad; ndestruct (bad);
    276 ##| #a b c d e f g h bad; ndestruct (bad);
    277 ##| #a b c d e f g h i j k l m n bad; ndestruct (bad);
    278 ##| #a b c d e f g h bad; ndestruct (bad);
    279 ##| #a b c d e f g h i j k l m n bad;  ndestruct (bad);
    280 ##| #a b c d e f g h i bad; ndestruct (bad);
    281 ##| #a b c d e f g bad; ndestruct (bad);
    282 ##] nqed.
    283 
    284 nlemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
     264#ge #en #m #e #sp #loc #off #tr #ty #H inversion H;
     265[ 1,2,5: #a #b #H @False_ind destruct (H);
     266| #a #b #c #d #e #f #g #H1 #i #H2 <H2 in H1 #H1 @False_ind
     267    @(eval_lvalue_inv_ind … H1)
     268    [ #a #b #c #d #bad destruct (bad);
     269    | #a #b #c #d #e #f #bad destruct (bad);
     270    | #a #b #c #d #e #f #g #bad destruct (bad);
     271    | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad @False_ind destruct (bad);
     272    | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     273    ]
     274| #e' #ty' #sp' #loc' #ofs' #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
     275| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     276| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
     277| #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
     278| #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
     279| #a #b #c #d #e #f #g #h #bad destruct (bad);
     280| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
     281| #a #b #c #d #e #f #g #h #bad destruct (bad);
     282| #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
     283| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
     284| #a #b #c #d #e #f #g #bad destruct (bad);
     285] qed.
     286
     287lemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    285288exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
    286289exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
    287 #ge en m e sp loc off tr ty H; nwhd in ⊢ (??%?);
    288 nrewrite > H; //;
    289 nqed.
    290 
    291 ntheorem exec_lvalue_sound: ∀ge,en,m,e.
     290#ge #en #m #e #sp #loc #off #tr #ty #H whd in ⊢ (??%?);
     291>H //;
     292qed.
     293
     294theorem exec_lvalue_sound: ∀ge,en,m,e.
    292295P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
    293 #ge en m e; nlapply (refl ? (exec_lvalue ge en m e));
    294 ncases (exec_lvalue ge en m e) in ⊢ (???% → %);
    295 ##[ #x; ncases x; #y; ncases y; #z; ncases z; #sp loc off tr H; nwhd;
    296     napply (addrof_eval_lvalue … Tvoid);
    297     nlapply (addrof_exec_lvalue … Tvoid H); #H';
    298     nlapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
    299     nrewrite > H'; #H''; napply H'';
    300 ##| #_; nwhd; napply I;
    301 ##] nqed.
     296#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
     297cases (exec_lvalue ge en m e) in ⊢ (???% → %);
     298[ #x cases x; #y cases y; #z cases z; #sp #loc #off #tr #H whd;
     299    @(addrof_eval_lvalue … Tvoid)
     300    lapply (addrof_exec_lvalue … Tvoid H); #H'
     301    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
     302    >H' #H'' @H''
     303| #_ whd; @I
     304] qed.
    302305
    303306(* Plain equality versions of the above *)
    304307
    305 ndefinition exec_expr_sound' ≝ λge,en,m,e,v.
     308definition exec_expr_sound' ≝ λge,en,m,e,v.
    306309  λH:exec_expr ge en m e = OK ? v.
    307310  P_res_to_P ???? (exec_expr_sound ge en m e) H.
    308311
    309 ndefinition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
     312definition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
    310313  λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
    311314  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
    312315
    313 nlemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
    314 #ge e m l; nelim l;
    315  nwhd; //;
    316  #e1 es; #IH;
    317 napply bind2_OK; #v tr1 Hv;
    318 napply bind2_OK; #vs tr2 Hvs;
    319 nwhd; napply eval_Econs;
    320 ##[ napply (P_res_to_P … (exec_expr_sound ge e m e1) Hv);
    321 ##| napply (P_res_to_P … IH Hvs);
    322 ##] nqed.
    323 
    324 ntheorem exec_step_sound: ∀ge,st.
     316lemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
     317#ge #e #m #l elim l;
     318 whd; (* XXX //; *)
     319[ %
     320| #e1 #es #IH
     321  @bind2_OK #v #tr1 #Hv
     322  @bind2_OK #vs #tr2 #Hvs
     323  whd; @eval_Econs
     324  [ @(P_res_to_P … (exec_expr_sound ge e m e1) Hv)
     325  | @(P_res_to_P … IH Hvs)
     326  ]
     327] qed.
     328
     329lemma exec_alloc_variables_sound : ∀l,en,m,en',m'.
     330  exec_alloc_variables en m l = 〈en',m'〉 →
     331  alloc_variables en m l en' m'.
     332#l elim l
     333[ #en #m #en' #m' #EXEC whd in EXEC:(??%?); destruct %
     334| * #id #ty #t #IH #en #m #en' #m'
     335  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
     336  whd in EXEC:(??%?) ALLOC:(???%)
     337 @(alloc_variables_cons … ALLOC)
     338 @IH @EXEC
     339qed.
     340
     341lemma exec_bind_parameters_sound : ∀ps,vs,en,m.
     342  P_res ? (λm'. bind_parameters en m ps vs m') (exec_bind_parameters en m ps vs).
     343#ps elim ps
     344[ * //
     345| * #id #ty #ps' #IH *
     346    [ //
     347    | #v #vs #en #m
     348      @opt_bind_OK #b #GET
     349      @opt_bind_OK #m' #STORE
     350      lapply (refl ? (exec_bind_parameters en m' ps' vs))
     351      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #_ %]
     352      #m'' #BIND
     353      @(bind_parameters_cons … GET STORE)
     354      lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
     355    ]
     356] qed.
     357
     358lemma check_eventval_list_sound : ∀vs,tys.
     359  P_res ? (λevs. eventval_list_match evs tys vs) (check_eventval_list vs tys).
     360#vs0 elim vs0
     361[ * //
     362| #v #vs #IH *
     363  [ //
     364  | #ty #tys whd in ⊢ (???%)
     365    cases ty cases v // #v'
     366    @bind_OK #evs #CHECK
     367    @(evl_match_cons ??????? (P_res_to_P … CHECK)) //
     368  ]
     369] qed.
     370
     371theorem exec_step_sound: ∀ge,st.
    325372  P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
    326 #ge st; ncases st;
    327 ##[ #f s k e m; ncases s;
    328   ##[ ncases k;
    329     ##[ nwhd in ⊢ (?????%);
    330         nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
    331         //; #H; nwhd;
    332         napply step_skip_call; //;
    333     ##| #s' k'; nwhd; //;
    334     ##| #ex s' k'; napply step_skip_or_continue_while; @; //;
    335     ##| #ex s' k';
    336         napply res_bindIO2_OK; #v tr Hv;
    337         nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    338         nlapply (refl ? bexpr);
    339         ncases bexpr in ⊢ (???% → %);
    340         ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    341             nwhd in ⊢ (?????%);
    342             ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    343               ##[ @; // ##| napply (bool_of … Hb); ##]
    344             ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    345               ##[ @; // ##| napply (bool_of … Hb); ##]
    346             ##]
    347         ##| #_; //;
    348         ##]
    349     ##| #ex s1 s2 k'; napply step_skip_or_continue_for2; @; //;
    350     ##| #ex s1 s2 k'; napply step_skip_for3;
    351     ##| #k'; napply step_skip_break_switch; @; //;
    352     ##| #r f' e' k'; nwhd in ⊢ (?????%);
    353         nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
    354         //; #H; nwhd;
    355         napply step_skip_call; //;
    356     ##]
    357   ##| #ex1 ex2;
    358     napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
    359     napply res_bindIO2_OK; #v2 tr2 Hv2;
    360     napply opt_bindIO_OK; #m' em';
    361     nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em');
    362   ##| #lex fex args;
    363     napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
    364     napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs;
    365     napply opt_bindIO_OK; #fd efd;
    366     napply bindIO_OK; #ety;
    367     ncases lex; nwhd;
    368     ##[ napply (step_call_none … Hvf Hvargs efd ety);
    369     ##| #lhs';
    370         napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
    371         nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety);
    372     ##]
    373   ##| #s1 s2; nwhd; //;
    374   ##| #ex s1 s2;
    375     napply res_bindIO2_OK; #v tr Hv;
    376     nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    377     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    378     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    379     ##[ napply (step_ifthenelse_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    380     ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb)
    381     ##]
    382   ##| #ex s';
    383     napply res_bindIO2_OK; #v tr Hv;
    384     nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    385     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    386     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    387     ##[ napply (step_while_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    388     ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    389     ##]
    390   ##| #ex s'; nwhd; //;
    391   ##| #s1 ex s2 s3; nwhd in ⊢ (?????%); nelim (is_Sskip s1); #Hs1; nwhd in ⊢ (?????%);
    392     ##[ nrewrite > Hs1;
    393       napply res_bindIO2_OK; #v tr Hv;
    394       nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    395       nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    396       #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    397       ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    398       ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    399       ##]
    400     ##| napply step_for_start; //;
    401     ##]
    402   ##| nwhd in ⊢ (?????%); ncases k; //;
    403     ##[ #s' k'; nwhd; //;
    404     ##| #ex s' k'; nwhd; //;
    405     ##| #ex s' k'; nwhd; //;
    406     ##| #ex s1 s2 k'; nwhd; //;
    407     ##| #k'; napply step_skip_break_switch; @2; //;
    408     ##]
    409   ##| nwhd in ⊢ (?????%); ncases k; //;
    410     ##[ #s' k'; nwhd; //;
    411     ##| #ex s' k'; nwhd; napply step_skip_or_continue_while; @2; //;
    412     ##| #ex s' k'; nwhd;
    413       napply res_bindIO2_OK; #v tr Hv;
    414       nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    415       nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    416       #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    417       ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    418         ##[ @2; // ##| napply (bool_of … Hb); ##]
    419       ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    420         ##[ @2; // ##| napply (bool_of … Hb); ##]
    421       ##]
    422     ##| #ex s1 s2 k'; nwhd; napply step_skip_or_continue_for2; @2; //
    423     ##| #k'; nwhd; //;
    424     ##]
    425   ##| #r; nwhd in ⊢ (?????%); ncases r;
    426     ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H;
    427         napply step_return_0; napply H;
    428     ##| #ex; ncases (type_eq_dec (fn_return f) Tvoid); //; nwhd in ⊢ (% → ?????%); #Hnotvoid;
    429         napply res_bindIO2_OK; #v tr Hv;
    430         nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
    431     ##]
    432   ##| #ex ls; napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
    433     napply step_switch; napply (exec_expr_sound' … Hv);
    434   ##| #l s'; nwhd; //;
    435   ##| #l; nwhd in ⊢ (?????%); nlapply (refl ? (find_label l (fn_body f) (call_cont k)));
    436       ncases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
    437       #sk; ncases sk; #s' k' H;
    438       napply (step_goto … H);
    439   ##| #l s'; nwhd; //;
    440   ##]
    441 ##| #f0 vargs k m; nwhd in ⊢ (?????%); ncases f0;
    442   ##[ #fn;
    443     napply extract_subset_pair_io; #e m1 ealloc Halloc;
    444     napply sig_bindIO_OK; #m2 Hbind;
    445     nwhd; napply (step_internal_function … Halloc Hbind);
    446   ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
    447     napply bindIO_OK; #eres; nwhd;
    448     napply step_external_function; @; ##[ napply Hevs; ##| napply mk_val_correct; ##]
    449   ##] 
    450 ##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
    451     #r f e k; nwhd in ⊢ (?????%); ncases r;
    452   ##[ nwhd; //;
    453   ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
    454     napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
    455   ##]
    456 ##]
    457 nqed.
    458 
    459 nlemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
    460 #p; ncases p; #fns main vars;
    461 nwhd in ⊢ (???%);
    462 napply bind_OK; #ge Ege;
    463 napply bind_OK; #m Em;
    464 napply opt_bind_OK; #x; ncases x; #sp b esb;
    465 napply opt_bind_OK; #u ecode;
    466 napply opt_bind_OK; #f ef;
    467 ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    468 nwhd; @; //; napply (initial_state_intro … Ege Em esb ef);
    469 nqed.
    470 
    471 ntheorem exec_steps_sound: ∀ge,n,st.
     373#ge #st cases st;
     374[ #f #s #k #e #m cases s;
     375  [ cases k;
     376    [ whd in ⊢ (?????%);
     377        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
     378        //; #H whd;
     379        @step_skip_call //;
     380    | #s' #k' whd; (* XXX //; *) @step_skip_seq
     381    | #ex #s' #k' @step_skip_or_continue_while % //;
     382    | #ex #s' #k'
     383        @res_bindIO2_OK #v #tr #Hv
     384        letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     385        lapply (refl ? bexpr);
     386        cases bexpr in ⊢ (???% → %);
     387        [ #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     388            whd in ⊢ (?????%);
     389            [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
     390              [ % // | @(bool_of … Hb) ]
     391            | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
     392              [ % // | @(bool_of … Hb) ]
     393            ]
     394        | #_ //;
     395        ]
     396    | #ex #s1 #s2 #k' @step_skip_or_continue_for2 % //;
     397    | #ex #s1 #s2 #k' @step_skip_for3
     398    | #k' @step_skip_break_switch % //;
     399    | #r #f' #e' #k' whd in ⊢ (?????%);
     400        lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %);
     401        //; #H whd;
     402        @step_skip_call //;
     403    ]
     404  | #ex1 #ex2
     405    @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr1 #Hlval
     406    @res_bindIO2_OK #v2 #tr2 #Hv2
     407    @opt_bindIO_OK #m' #em'
     408    whd; @(step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em')
     409  | #lex #fex #args
     410    @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf
     411    @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs
     412    @opt_bindIO_OK #fd #efd
     413    @bindIO_OK #ety
     414    cases lex; whd;
     415    [ @(step_call_none … Hvf Hvargs efd ety)
     416    | #lhs'
     417        @res_bindIO2_OK #x cases x; #y cases y; #pcl #loc #ofs #tr3 #Hlocofs
     418        whd; @(step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety)
     419    ]
     420  | #s1 #s2 whd; (* XXX //; *) @step_seq
     421  | #ex #s1 #s2
     422    @res_bindIO2_OK #v #tr #Hv
     423    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     424    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
     425    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     426    [ @(step_ifthenelse_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     427    | @(step_ifthenelse_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     428    ]
     429  | #ex #s'
     430    @res_bindIO2_OK #v #tr #Hv
     431    letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     432    lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
     433    #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     434    [ @(step_while_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     435    | @(step_while_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     436    ]
     437  | #ex #s' whd; (* XXX //; *) @step_dowhile
     438  | #s1 #ex #s2 #s3 whd in ⊢ (?????%); elim (is_Sskip s1); #Hs1 whd in ⊢ (?????%);
     439    [ >Hs1
     440      @res_bindIO2_OK #v #tr #Hv
     441      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     442      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
     443      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     444      [ @(step_for_true … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     445      | @(step_for_false … (exec_expr_sound' … Hv)) @(bool_of … Hb)
     446      ]
     447    | @step_for_start //;
     448    ]
     449  | whd in ⊢ (?????%); cases k; //;
     450    [ #s' #k' whd (* XXX // *) @step_break_seq
     451    | #ex #s' #k' whd (* //; *) @step_break_while
     452    | #ex #s' #k' whd (* //; *) @step_break_dowhile
     453    | #ex #s1 #s2 #k' whd (* //; *) @step_break_for2
     454    | #k' @step_skip_break_switch %2  //
     455    ]
     456  | whd in ⊢ (?????%); cases k; //;
     457    [ #s' #k' whd; (* XXX //;*) @step_continue_seq
     458    | #ex #s' #k' whd; @step_skip_or_continue_while %2 ; //;
     459    | #ex #s' #k' whd;
     460      @res_bindIO2_OK #v #tr #Hv
     461      letin bexpr ≝ (exec_bool_of_val v (typeof ex));
     462      lapply (refl ? bexpr); cases bexpr in ⊢ (???% → %); //;
     463      #b cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
     464      [ @(step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv))
     465        [ %2 ; // | @(bool_of … Hb) ]
     466      | @(step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv))
     467        [ %2 ; // | @(bool_of … Hb) ]
     468      ]
     469    | #ex #s1 #s2 #k' whd; @step_skip_or_continue_for2 %2 ; //
     470    | #k' whd; (* XXX //;*) @step_continue_switch
     471    ]
     472  | #r whd in ⊢ (?????%); cases r;
     473    [ whd; lapply (refl ? (fn_return f)); cases (fn_return f) in ⊢ (???% → %); //; #H
     474        @step_return_0 @H
     475    | #ex cases (type_eq_dec (fn_return f) Tvoid); //; whd in ⊢ (% → ?????%); #Hnotvoid
     476        @res_bindIO2_OK #v #tr #Hv
     477        whd; @(step_return_1 … Hnotvoid (exec_expr_sound' … Hv))
     478    ]
     479  | #ex #ls @res_bindIO2_OK #v cases v; //; #n #tr #Hv
     480    @step_switch @(exec_expr_sound' … Hv)
     481  | #l #s' whd; @step_label (* XXX //; *)
     482  | #l whd in ⊢ (?????%); lapply (refl ? (find_label l (fn_body f) (call_cont k)));
     483      cases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
     484      #sk cases sk; #s' #k' #H
     485      @(step_goto … H)
     486  | #l #s' whd; (* XXX //; *) @step_cost
     487  ]
     488| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
     489  [ #fn whd in ⊢ (?????%)
     490    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
     491    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
     492    #en' #m' #ALLOC whd in ⊢ (?????%)
     493    @res_bindIO_OK #m2 #BIND
     494    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
     495    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
     496  | #id #argtys #rty @res_bindIO_OK #evs #Hevs
     497    @bindIO_OK #eres whd;
     498    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
     499                              | @mk_val_correct ]
     500  ] 
     501| #v #k' #m' whd in ⊢ (?????%); cases k'; //;
     502    #r #f #e #k whd in ⊢ (?????%); cases r;
     503  [ whd; @step_returnstate_0
     504  | #x cases x; #y cases y; #z cases z; #pcl #b #ofs #ty
     505    @opt_bindIO_OK #m' #em' @step_returnstate_1 whd in em':(??%?); //;
     506  ]
     507]
     508qed.
     509
     510lemma make_initial_state_sound : ∀p. P_res ? (λgs.globalenv Genv ?? p = OK ? (\fst gs) ∧ initial_state p (\snd gs)) (make_initial_state p).
     511#p cases p; #fns #main #vars
     512whd in ⊢ (???%);
     513@bind_OK #ge #Ege
     514@bind_OK #m #Em
     515@opt_bind_OK #x cases x; #sp #b #esb
     516@opt_bind_OK #u #ecode
     517@opt_bind_OK #f #ef
     518cases sp in esb ecode; #esb #ecode whd in ecode:(??%%); [ 1,2,3,4,5: destruct (ecode); ]
     519whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
     520qed.
     521
     522theorem exec_steps_sound: ∀ge,n,st.
    472523 P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
    473524 (exec_steps n ge st).
    474 #ge n; nelim n;
    475 ##[ #st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; nwhd; //;
    476 ##| #n' IH st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H;
    477   ##[ nwhd; //;
    478   ##| napply (P_bindIO2_OK ????????? (exec_step_sound …)); #t s'; ncases s';
    479       ##[ #f s k e m; ##| #fd args k m; ##| #r k m; ##]
    480       nwhd in ⊢ (? → ?????(??????%?));
    481       ncases m; #mc mn mp; #Hstep;
    482       nwhd in ⊢ (?????(??????%?));
    483       napply (P_bindIO2_OK ????????? (IH …)); #t' s'' Hsteps;
    484       nwhd; napply (star_step ????????? Hsteps); ##[ ##2,5,8: napply Hstep; ##| ##3,6,9: // ##]
    485   ##]
    486 nqed.
     525#ge #n elim n;
     526[ #st whd in ⊢ (?????%); elim (is_final_state st); #H whd; %
     527| #n' #IH #st whd in ⊢ (?????%); elim (is_final_state st); #H
     528  [ whd; %
     529  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
     530      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ]
     531      whd in ⊢ (? → ?????(??????%?));
     532      cases m; #mc #mn #mp #Hstep
     533      whd in ⊢ (?????(??????%?));
     534      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
     535      whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
     536  ]
     537qed.
Note: See TracChangeset for help on using the changeset viewer.