Changeset 251 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Nov 22, 2010, 2:40:26 PM (9 years ago)
Author:
campbell
Message:

Separate out soundness of exec_expr from definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r250 r251  
    414414#A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed.
    415415
    416 nlemma exec_expr_sound_0: ∀ge:genv. ∀en:env. ∀m:mem.
    417 (∀e,ty. P_res ? (λx.eval_lvalue ge en m (Expr e ty) (\fst (\fst (\fst x))) (\snd (\fst (\fst x))) (\snd (\fst x)) (\snd x)) (exec_lvalue' ge en m e ty)) →
    418 ∀e:expr. P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e).
    419 #ge en m lvalue_sound e; ncases e; #e' ty; ncases e';
    420 ##[ ##1,2: #c; nwhd; //;
    421 ##| ##3,4: #z; nwhd in ⊢ (???%);
     416(* We define a special induction principle tailored to the recursive definition
     417   above. *)
     418
     419ndefinition is_not_lvalue: expr_descr → Prop ≝
     420λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
     421
     422ndefinition Plvalue ≝ λP:(expr → Prop).λe,ty.
     423match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
     424
     425nlet rec expr_lvalue_ind
     426  (P:expr → Prop)
     427  (Q:expr_descr → type → Prop)
     428  (ci:∀ty,i.P (Expr (Econst_int i) ty))
     429  (cf:∀ty,f.P (Expr (Econst_float f) ty))
     430  (lv:∀e,ty. Q e ty → Plvalue P e ty)
     431  (vr:∀v,ty.Q (Evar v) ty)
     432  (dr:∀e,ty.P e → Q (Ederef e) ty)
     433  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
     434  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
     435  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
     436  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
     437  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
     438  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
     439  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
     440  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
     441  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
     442  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
     443  (xx:∀e,ty. is_not_lvalue e → Q e ty)
     444  (e:expr) on e : P e ≝
     445match e with
     446[ Expr e' ty ⇒
     447  match e' with
     448  [ Econst_int i ⇒ ci ty i
     449  | Econst_float f ⇒ cf ty f
     450  | Evar v ⇒ lv (Evar v) ty (vr v ty)
     451  | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
     452  | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
     453  | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     454  | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     455  | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     456  | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
     457  | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     458  | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
     459  | Esizeof ty' ⇒ sz ty ty'
     460  | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
     461  | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     462  ]
     463]
     464and lvalue_expr_ind
     465  (P:expr → Prop)
     466  (Q:expr_descr → type → Prop)
     467  (ci:∀ty,i.P (Expr (Econst_int i) ty))
     468  (cf:∀ty,f.P (Expr (Econst_float f) ty))
     469  (lv:∀e,ty. Q e ty → Plvalue P e ty)
     470  (vr:∀v,ty.Q (Evar v) ty)
     471  (dr:∀e,ty.P e → Q (Ederef e) ty)
     472  (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
     473  (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
     474  (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
     475  (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
     476  (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
     477  (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
     478  (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
     479  (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
     480  (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
     481  (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
     482  (xx:∀e,ty. is_not_lvalue e → Q e ty)
     483  (e:expr_descr) (ty:type) on e : Q e ty ≝
     484  match e return λe0. Q e0 ty with
     485  [ Evar v ⇒ vr v ty
     486  | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
     487  | 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'') ]
     488  | _ ⇒ xx ? ty ?
     489  ]. nwhd; napply I; nqed.
     490
     491
     492ntheorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
     493(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
     494#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);
     495##[ ##1,2: #ty c; nwhd; //;
     496(* expressions that are lvalues *)
     497##| #e' ty; ncases e'; //; ##[ #i He' ##| #e He' ##| #e i He' ##] nwhd in He' ⊢ %;
    422498    napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    423     napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … ev);
    424     napply (P_res_to_P … (lvalue_sound ??) H);
    425 ##| #e''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    426     nwhd; napply eval_Eaddrof; ncases e'' in H ⊢ %; #e0 ty0 H; napply (P_res_to_P … (lvalue_sound ??) H);
    427 ##| #op e1; napply bind2_OK; #v1 tr Hv1;
     499    napply opt_bind_OK;  #vl evl; nwhd in evl:(??%?); napply (eval_Elvalue … evl);
     500    nrewrite > H in He'; #He'; napply He';
     501##| #v ty;
     502    nwhd in ⊢ (???%);
     503    nlapply (refl ? (get ident PTree block v en));
     504    ncases (get ident PTree block v en) in ⊢ (???% → %);
     505    ##[ #eget; napply opt_bind_OK; #sploc; ncases sploc; #sp loc efind;
     506        nwhd; napply (eval_Evar_global … eget efind);
     507    ##| #loc eget; napply (eval_Evar_local … eget);
     508    ##]
     509##| #ty e He; nwhd in ⊢ (???%);
     510    napply bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
     511    napply eval_Ederef; nrewrite > Hv in He; #He; napply He;
     512##| #ty e'' ty'' He''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
     513    nwhd; napply eval_Eaddrof; nrewrite > H in He''; #He''; napply He'';
     514##| #ty op e1 He1; napply bind2_OK; #v1 tr Hv1;
    428515    napply opt_bind_OK; #v ev;
    429516    napply (eval_Eunop … ev);
    430 ##| napply sig_bind2_OK; #v1 tr1 Hv1;
    431     napply sig_bind2_OK; #v2 tr2 Hv2;
    432     napply opt_bind_OK; #v ev;
    433     napply (eval_Ebinop … Hv1 Hv2 ev);
    434 ##| napply sig_bind2_OK; #v tr Hv;
     517    nrewrite > Hv1 in He1; #He1; napply He1;
     518##| #ty op e1 e2 He1 He2;
     519    napply bind2_OK; #v1 tr1 ev1; nrewrite > ev1 in He1; #He1;
     520    napply bind2_OK; #v2 tr2 ev2; nrewrite > ev2 in He2; #He2;
     521    napply opt_bind_OK; #v ev; nwhd in He1 He2; nwhd;
     522    napply (eval_Ebinop … He1 He2 ev);
     523##| #ty ty' e' He';
     524    napply bind2_OK; #v tr Hv; nrewrite > Hv in He'; #He';
    435525    napply bind_OK; #v' ev';
    436     napply (eval_Ecast … Hv ?);
     526    napply (eval_Ecast … He' ?);
    437527    /2/;
    438 ##| napply sig_bind2_OK; #vb tr1 Hvb;
     528##| #ty e1 e2 e3 He1 He2 He3;
     529    napply bind2_OK; #vb tr1 Hvb; nrewrite > Hvb in He1; #He1;
    439530    napply bind_OK; #b;
    440531    ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    441     napply sig_bind2_OK; #v tr Hv;
    442     ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
    443     ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
    444     ##]
    445 ##| napply sig_bind2_OK; #v1 tr1 Hv1;
     532    napply bind2_OK; #v tr Hv;
     533    ##[ nrewrite > Hv in He2; #He2; nwhd in He2 Hv:(??%?) ⊢%;
     534        napply (eval_Econdition_true … He1 ? He2);  napply (bool_of ??? Hb);
     535    ##| nrewrite > Hv in He3; #He3; nwhd in He3 Hv:(??%?) ⊢%;
     536        napply (eval_Econdition_false … He1 ? He3);  napply (bool_of ??? Hb);
     537    ##]
     538##| #ty e1 e2 He1 He2;
     539    napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    446540    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    447     ##[ napply sig_bind2_OK; #v2 tr2 Hv2;
     541    ##[ napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    448542        napply bind_OK; #b2 eb2;
    449         napply (eval_Eandbool_2 … Hv1 … Hv2);
     543        napply (eval_Eandbool_2 … He1 … He2);
    450544        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    451     ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
    452     ##]
    453 ##| napply sig_bind2_OK; #v1 tr1 Hv1;
     545    ##| napply (eval_Eandbool_1 … He1); napply (bool_of … Hb1);
     546    ##]
     547##| #ty e1 e2 He1 He2;
     548    napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    454549    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    455     ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
    456     ##| napply sig_bind2_OK; #v2 tr2 Hv2;
     550    ##[ napply (eval_Eorbool_1 … He1); napply (bool_of … Hb1);
     551    ##| napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    457552        napply bind_OK; #b2 eb2;
    458         napply (eval_Eorbool_2 … Hv1 … Hv2);
     553        napply (eval_Eorbool_2 … He1 … He2);
    459554        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    460555    ##]
    461 ##| //
    462 ##| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H;
    463     napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev);
    464 ##| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H);
    465 ##| //
    466 ##| //
    467 ##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
    468 ##| napply (eval_Evar_local … c3);
    469 ##| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
    470     napply eval_Ederef; //
    471 ##| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: //
    472 ##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    473     napply bind_OK; #delta Hdelta;
    474     napply (eval_Efield_struct … H c5 Hdelta);
    475 ##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
    476     napply (eval_Efield_union … H c5);
    477 ##| //
    478 ##| //
     556##| #ty ty'; nwhd; //
     557##| #ty e' ty' i; ncases ty'; //;
     558    ##[ #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
     559        napply bind_OK; #delta Hdelta; nrewrite > H in He'; #He';
     560        napply (eval_Efield_struct …  He' (refl ??) Hdelta);
     561    ##| #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
     562        nrewrite > H in He'; #He';
     563        napply (eval_Efield_union … He' (refl ??));
     564    ##]
     565##| #ty l e' He'; napply bind2_OK; #v tr1 H; nrewrite > H in He'; #He';
     566    napply (eval_Ecost … He');
     567(* exec_lvalue fails on non-lvalues. *)
     568##| #e' ty; ncases e';
     569    ##[ ##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 ##]
     570    napply I;
    479571##] nqed.
    480 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
    481 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
     572
     573nlemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
     574eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
     575eval_lvalue ge en m e sp loc off tr.
     576#ge en m e sp loc off tr ty H; ninversion H;
     577##[ ##1,2,5: #a b H; napply False_ind; ndestruct (H);
     578##| #a b c d e f g H1 i H2; nrewrite < H2 in H1; #H1; napply False_ind;
     579    napply (eval_lvalue_inv_ind … H1);
     580    ##[ #a b c d bad; ndestruct (bad);
     581    ##| #a b c d e f bad; ndestruct (bad);
     582    ##| #a b c d e f g bad; ndestruct (bad);
     583    ##| #a b c d e f g  h i j k l m n bad; napply False_ind; ndestruct (bad);
     584    ##| #a b c d e f g h i j k l bad; ndestruct (bad);
     585    ##]
     586##| #e' ty' sp' loc' ofs' tr' H e1 e2 e3; ndestruct (e1 e2 e3); napply H;
     587##| #a b c d e f g h i bad; ndestruct (bad);
     588##| #a b c d e f g h i j k l k l bad; ndestruct (bad);
     589##| #a b c d e f g h i j k l m bad; ndestruct (bad);
     590##| #a b c d e f g h i j k l m bad; ndestruct (bad);
     591##| #a b c d e f g h bad; ndestruct (bad);
     592##| #a b c d e f g h i j k l m n bad; ndestruct (bad);
     593##| #a b c d e f g h bad; ndestruct (bad);
     594##| #a b c d e f g h i j k l m n bad;  ndestruct (bad);
     595##| #a b c d e f g h i bad; ndestruct (bad);
     596##| #a b c d e f g bad; ndestruct (bad);
     597##] nqed.
     598
     599nlemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
     600exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
     601exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
     602#ge en m e sp loc off tr ty H; nwhd in ⊢ (??%?);
     603nrewrite > H; //;
     604nqed.
     605
     606ntheorem exec_lvalue_sound: ∀ge,en,m,e.
     607P_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).
     608#ge en m e; nlapply (refl ? (exec_lvalue ge en m e));
     609ncases (exec_lvalue ge en m e) in ⊢ (???% → %);
     610##[ #x; ncases x; #y; ncases y; #z; ncases z; #sp loc off tr H; nwhd;
     611    napply (addrof_eval_lvalue … Tvoid);
     612    nlapply (addrof_exec_lvalue … Tvoid H); #H';
     613    nlapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
     614    nrewrite > H'; #H''; napply H'';
     615##| #_; nwhd; napply I;
     616##] nqed.
     617
     618(* Plain equality versions of the above *)
     619
     620ndefinition exec_expr_sound' ≝ λge,en,m,e,v.
     621  λH:exec_expr ge en m e = OK ? v.
     622  P_res_to_P ???? (exec_expr_sound ge en m e) H.
     623
     624ndefinition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
     625  λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
     626  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
    482627
    483628(* TODO: Can we do this sensibly with a map combinator? *)
    484 nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) ≝
     629nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
    485630match l with
    486 [ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
    487 | cons e1 es ⇒ Some ? (
     631[ nil ⇒ OK ? 〈nil val, E0〉
     632| cons e1 es ⇒
    488633  do 〈v,tr1〉 ← exec_expr ge e m e1;
    489634  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
    490   OK ? 〈cons val v vs, tr1⧺tr2〉)
    491 ]. nwhd; //;
    492 napply sig_bind2_OK; #v tr1 Hv;
    493 napply sig_bind2_OK; #vs tr2 Hvs;
    494 nwhd; napply eval_Econs; //;
    495 nqed.
     635  OK ? 〈cons val v vs, tr1⧺tr2〉
     636].
     637
     638nlemma 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).
     639#ge e m l; nelim l;
     640 nwhd; //;
     641 #e1 es; #IH;
     642napply bind2_OK; #v tr1 Hv;
     643napply bind2_OK; #vs tr2 Hvs;
     644nwhd; napply eval_Econs;
     645##[ napply (P_res_to_P … (exec_expr_sound ge e m e1) Hv);
     646##| napply (P_res_to_P … IH Hvs);
     647##] nqed.
    496648
    497649(* Don't really want to use subset rather than sigma here, but can't be bothered
     
    789941      ]
    790942    | Some a ⇒ Some ? (
    791         ! u ← is_not_void (fn_return f);
     943        ! u ← err_to_io_sig … (is_not_void (fn_return f));
    792944        ! 〈v,tr〉 ← exec_expr ge e m a;
    793945        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
     
    809961  [ Internal f ⇒ Some ? (
    810962    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
    811       ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
     963      ! m2 ← err_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs);
    812964      ret ? 〈E0, State f (fn_body f) k e m2〉
    813965    ])
    814966  | External f argtys retty ⇒ Some ? (
    815       ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
     967      ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
    816968      ! evres ← do_io f evargs;
    817       ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));
     969      ! vres ← err_to_io_sig … (check_eventval evres (proj_sig_res (signature_of_type argtys retty)));
    818970      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
    819971  ]
     
    839991##[ nrewrite > c7; napply step_skip_call; //; napply c8;
    840992##| napply step_skip_or_continue_while; @; //;
    841 ##| napply sig_bindIO2_OK; #v tr Hv;
     993##| napply res_bindIO2_OK; #v tr Hv;
    842994    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    843995    nlapply (refl ? bexpr);
     
    845997    ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    846998        nwhd in ⊢ (?????%);
    847         ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     999        ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    8481000          ##[ @; // ##| napply (bool_of … Hb); ##]
    849         ##| napply (step_skip_or_continue_dowhile_false … Hv);
     1001        ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    8501002          ##[ @; // ##| napply (bool_of … Hb); ##]
    8511003        ##]
     
    8551007##| napply step_skip_break_switch; @; //;
    8561008##| nrewrite > c11; napply step_skip_call; //; napply c12;
    857 ##| napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
    858     napply sig_bindIO2_OK; #v2 tr2 Hv2;
     1009##| napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
     1010    napply res_bindIO2_OK; #v2 tr2 Hv2;
    8591011    napply opt_bindIO_OK; #m' em';
    860     nwhd; napply (step_assign … Hlval Hv2 em');
    861 ##| napply sig_bindIO2_OK; #vf tr1 Hvf;
    862     napply sig_bindIO2_OK; #vargs tr2 Hvargs;
     1012    nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em');
     1013##| napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
     1014    napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs;
    8631015    napply opt_bindIO_OK; #fd efd;
    8641016    napply bindIO_OK; #ety;
     
    8661018    ##[ napply (step_call_none … Hvf Hvargs efd ety);
    8671019    ##| #lhs';
    868         napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
    869         nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
    870     ##]
    871 ##| napply sig_bindIO2_OK; #v tr Hv;
     1020        napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
     1021        nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety);
     1022    ##]
     1023##| napply res_bindIO2_OK; #v tr Hv;
    8721024    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
    8731025    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    8741026    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    875     ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
    876     ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
    877     ##]
    878 ##| napply sig_bindIO2_OK; #v tr Hv;
     1027    ##[ napply (step_ifthenelse_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
     1028    ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb)
     1029    ##]
     1030##| napply res_bindIO2_OK; #v tr Hv;
    8791031    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
    8801032    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    8811033    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    882     ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
    883     ##| napply (step_while_false … Hv); napply (bool_of … Hb);
     1034    ##[ napply (step_while_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
     1035    ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    8841036    ##]
    8851037##| nrewrite > c11;
    886     napply sig_bindIO2_OK; #v tr Hv;
     1038    napply res_bindIO2_OK; #v tr Hv;
    8871039    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    8881040    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    8891041    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    890     ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
    891     ##| napply (step_for_false … Hv); napply (bool_of … Hb);
     1042    ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
     1043    ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    8921044    ##]
    8931045##| napply step_for_start; //;
    8941046##| napply step_skip_break_switch; @2; //;
    8951047##| napply step_skip_or_continue_while; @2; //;
    896 ##| napply sig_bindIO2_OK; #v tr Hv;
     1048##| napply res_bindIO2_OK; #v tr Hv;
    8971049    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
    8981050    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    8991051    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    900     ##[ napply (step_skip_or_continue_dowhile_true … Hv);
     1052    ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    9011053      ##[ @2; // ##| napply (bool_of … Hb); ##]
    902     ##| napply (step_skip_or_continue_dowhile_false … Hv);
     1054    ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    9031055      ##[ @2; // ##| napply (bool_of … Hb); ##]
    9041056    ##]
     
    9061058##| napply step_return_0; napply c9;
    9071059##| napply sig_bindIO_OK; #u Hnotvoid;
    908     napply sig_bindIO2_OK; #v tr Hv;
    909     nwhd; napply (step_return_1 … Hnotvoid Hv);
    910 ##| napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv;
    911     napply step_switch; //;
     1060    napply res_bindIO2_OK; #v tr Hv;
     1061    nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
     1062##| napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
     1063    napply step_switch; napply (exec_expr_sound' … Hv);
    9121064##| napply step_goto; nrewrite < c12; napply c9;
    9131065##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
Note: See TracChangeset for help on using the changeset viewer.