Changeset 239


Ignore:
Timestamp:
Nov 12, 2010, 7:16:52 PM (9 years ago)
Author:
campbell
Message:

More work on soundness and completeness of executable Clight semantics.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r225 r239  
    865865nqed.
    866866
    867 ndefinition is_final_state : ∀st:state. (r. final_state st r) + (¬∃r. final_state st r).
     867ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
    868868#st; nelim st;
    869869##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
     
    931931(* A (possibly non-terminating) execution. *)
    932932ncoinductive execution : Type ≝
    933 | e_stop : trace → state → execution
     933| e_stop : trace → int → execution
    934934| e_step : trace → state → execution → execution
    935935| e_wrong : execution
     
    941941| Value v ⇒ match v with [ mk_pair t s' ⇒
    942942    match is_final_state s' with
    943     [ inl _ ⇒ e_stop t s'
     943    [ inl r ⇒ e_stop t (sig_eject … r)
    944944    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    945945| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    946946].
    947947
     948
    948949ndefinition exec_inf : program → execution ≝
    949950λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
    950951
     952(*
     953FIXME: unfolding cofixpoints appears to be rather tricky.
     954
     955nremark execution_cases: ∀e.
     956 e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
     957 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
     958#e; ncases e; //; nqed.
     959
     960nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
     961match s with
     962[ Wrong ⇒ e_wrong
     963| Value v ⇒ match v with [ mk_pair t s' ⇒
     964    match is_final_state s' with
     965    [ inl r ⇒ e_stop t (sig_eject … r)
     966    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
     967| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
     968].
     969#ge s; nrewrite > (execution_cases (exec_inf_aux …));
     970ncases s; //; napply refl;
     971
     972
     973nlemma exec_inf_aux_wrong: ∀ge,s. exec_inf_aux ge s = e_wrong → s = Wrong ….
     974#ge s; ncases s;
     975##[ #o k EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
     976    ndestruct;
     977##| #v; ncases v; #tr s'; #EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
     978    ncases (is_final_state s');
     979    ndestruct;
     980*)
     981
     982(* Finite number of steps without interaction. *)
     983ninductive execution_steps : trace → execution → execution → Prop ≝
     984| steps_none : ∀e. execution_steps E0 e e
     985| steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
     986
     987(* Finite number of steps allowing interaction. *)
     988ninductive execution_isteps : trace → execution → execution → Prop ≝
     989| isteps_none : ∀e. execution_isteps E0 e e
     990| isteps_step : ∀e,e',tr,tr',s. execution_isteps tr e e' → execution_isteps (tr⧺tr') (e_step tr s e) e'
     991| isteps_interact : ∀k,o,i,e',tr. execution_isteps tr (k i) e' → execution_isteps tr (e_interact o k) e'.
     992
     993ninductive execution_terminates : trace → int → execution → Prop ≝
     994| terminates : ∀tr,tr',r,e. execution_isteps tr e (e_stop tr' r) → execution_terminates (tr⧺tr') r e.
     995
     996ncoinductive execution_diverging : execution → Prop ≝
     997| diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
     998
     999(* Makes a finite number of interactions (including cost labels) before diverging. *)
     1000ninductive execution_diverges : trace → execution → Prop ≝
     1001| diverges_diverging: ∀tr,e,e'.
     1002    execution_isteps tr e e' →
     1003    execution_diverging e' →
     1004    execution_diverges tr e.
     1005
     1006(* NB: "reacting" includes hitting a cost label. *)
     1007ncoinductive execution_reacts : traceinf → execution → Prop ≝
     1008| reacting: ∀tr,tr',e,e'. execution_reacts tr' e' → execution_isteps tr e e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
     1009
     1010ninductive execution_goes_wrong: trace → execution → Prop ≝
     1011| go_wrong: ∀tr,e. execution_isteps tr e e_wrong → execution_goes_wrong tr e.
     1012
     1013ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
     1014| emb_terminates: ∀e,tr,r.
     1015    execution_terminates tr r e →
     1016    execution_matches_behavior e (Terminates tr r)
     1017| emb_diverges: ∀e,tr.
     1018    execution_diverges tr e →
     1019    execution_matches_behavior e (Diverges tr)
     1020| emb_reacts: ∀e,tr.
     1021    execution_reacts tr e →
     1022    execution_matches_behavior e (Reacts tr)
     1023| emb_wrong: ∀e,tr.
     1024    execution_goes_wrong tr e →
     1025    execution_matches_behavior e (Goes_wrong tr).
     1026
     1027(*
     1028nlemma silent_sound: ∀ge,s,e.
     1029  execution_diverging e →
     1030  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
     1031  forever_silent (mk_transrel ?? step) … ge s.
     1032#ge s e H; ncases H; #s1 e1 H' EXEC;
     1033napply (forever_silent_intro (mk_transrel ?? step) … ge s s1);
     1034##[ nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC;
     1035    nnormalize in EXEC;
     1036 nnormalize in match exec_inf_aux in EXEC:(??%?);
     1037
     1038ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
     1039*)
  • C-semantics/CexecIOcomplete.ma

    r226 r239  
    44ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
    55λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
    6 ndefinition yieldsIO : ∀A,P. IO eventval io_out (Σx:A. P x) → A → Prop ≝
    7 λA,P,e,v. match e with [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
    8 (*
    9 ndefinition yields : ∀A.∀P:A → Prop. res (sigma A P) → A → Prop ≝
    10 λA,P,e,v. err_eject A P e = OK ? v.
    11 *)
     6
     7(* This tells us that some execution of e results in v.
     8   (There may be many possible executions due to I/O, but we're trying to prove
     9   that one particular one exists corresponding to a derivation in the inductive
     10   semantics.) *)
     11nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out (Σx:A. P x)) (v:A) on e : Prop ≝
     12match e with
     13[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
     14| Interact _ k ⇒ ∃r.yieldsIO A P (k r) v
     15| _ ⇒ False].
     16
    1217nlemma is_pointer_compat_true: ∀m,b,sp.
    1318  pointer_compat (block_space m b) sp →
     
    2732interpretation "yields" 'yields e e' = (yields ?? e e').
    2833interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
    29 (*
    30 (*notation < "vbox( ident v ← e;: break e' )" with precedence 40 for @{'bindnat ${e} (\lambda ${ident v} : ${ty}. ${e'})}.*)
    31 notation < "vbox( e ;: break e' )" with precedence 40 for @{'binde ${e} ${e'}}.
    32 notation < "vbox( ident v ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v}. ${e'})}.
    33 notation < "vbox( ident v : ty ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v} : ${ty}. ${e'})}.
    34 interpretation "error monad bind" 'binde e f = (bind ? ? e f).
    35 (*interpretation "error monad bind" 'bindnat e f = (bind nat nat e f).*)
    36 
    37 nlemma foo: ∀e:res nat. ∀f: nat → res nat. (x ← e;: f x) = OK ? 5.
    38 *)
    39 (*interpretation "error monad bind" 'bind e f = (bind ? ? e f).*)
    4034
    4135ntheorem is_det: ∀p,s,s'.
     
    5347##] nqed.
    5448
    55 ndefinition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A.
    56 match a with [ Value v ⇒ v' = v | _ ⇒ False ].
     49nlet rec yieldsIObare (A:Type) (a:IO eventval io_out A) (v':A) on a : Prop ≝
     50match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
    5751
    5852nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    5953yieldsIObare A a v' →
    6054yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
    61 #A P a; ncases a;
    62 ##[ #a b c d; *;
     55#A P a; nelim a;
     56##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
    6357##| #v v' p H; napply H;
    6458##| #a b; *;
     
    113107##| *;
    114108##] nqed.
    115 (*
    116 nlemma lvalue_complete_cond: ∀ge,env,m.
    117 (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) →
    118 (∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
    119 #ge env m IH;
    120 #e sp l off tr H; napply (eval_lvalue_ind … H);
    121 ##[ #id l ty H1; nwhd in ⊢ (???%?);
    122     nrewrite > H1;
    123     napply refl;
    124 ##| #id sp l ty H1 H2; nwhd in ⊢ (???%?);
    125     nrewrite > H1; nwhd nodelta in ⊢ (???%?); napply remove_res_sig;
    126     nrewrite > H2;
    127 *)
    128109
    129110(* Use to narrow down the choice of expression to just the lvalues. *)
     
    184165##] nqed.
    185166
    186 nlemma expr_complete: ∀ge,env,m.
     167nlemma expr_lvalue_complete: ∀ge,env,m.
    187168(∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧
    188169(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
     
    255236 
    256237 (* FIXME: next two cases produce type checking failures at nqed. *)
    257 ##|napply daemon; (* #id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
     238##| napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
    258239##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1);
    259240    nrewrite > e2; napply refl;*)
     
    272253##] nqed.
    273254
    274 
     255ntheorem expr_complete:  ∀ge,env,m.
     256 ∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉).
     257#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
     258
     259ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
     260  eval_exprlist ge env m es vs tr → yields ?? (exec_exprlist ge env m es) (〈vs,tr〉).
     261#ge env m es vs tr H; nelim H;
     262##[ napply refl;
     263##| #e et v vt tr trt H1 H2 H3; napply remove_res_sig;
     264    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     265    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     266    napply refl;
     267##] nqed.
     268
     269ntheorem lvalue_complete: ∀ge,env,m.
     270 ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
     271#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
     272
     273nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
     274match l with
     275[ Tnil ⇒ True
     276| Tcons h t ⇒ P h ∧ P_typelist P t
     277].
     278
     279nlet rec type_ind2l
     280  (P:type → Prop) (Q:typelist → Prop)
     281  (vo:P Tvoid)
     282  (it:∀i,s. P (Tint i s))
     283  (fl:∀f. P (Tfloat f))
     284  (pt:∀s,t. P t → P (Tpointer s t))
     285  (ar:∀s,t,n. P t → P (Tarray s t n))
     286  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
     287  (st:∀i,fl. P (Tstruct i fl))
     288  (un:∀i,fl. P (Tunion i fl))
     289  (cp:∀i. P (Tcomp_ptr i))
     290  (nl:Q Tnil)
     291  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     292 (t:type) on t : P t ≝
     293  match t return λt'.P t' with
     294  [ Tvoid ⇒ vo
     295  | Tint i s ⇒ it i s
     296  | Tfloat s ⇒ fl s
     297  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     298  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     299  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
     300  | Tstruct i fs ⇒ st i fs
     301  | Tunion i fs ⇒ un i fs
     302  | Tcomp_ptr i ⇒ cp i
     303  ]
     304and typelist_ind2l
     305  (P:type → Prop) (Q:typelist → Prop)
     306  (vo:P Tvoid)
     307  (it:∀i,s. P (Tint i s))
     308  (fl:∀f. P (Tfloat f))
     309  (pt:∀s,t. P t → P (Tpointer s t))
     310  (ar:∀s,t,n. P t → P (Tarray s t n))
     311  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
     312  (st:∀i,fl. P (Tstruct i fl))
     313  (un:∀i,fl. P (Tunion i fl))
     314  (cp:∀i. P (Tcomp_ptr i))
     315  (nl:Q Tnil)
     316  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
     317  (ts:typelist) on ts : Q ts ≝
     318  match ts return λts'.Q ts' with
     319  [ Tnil ⇒ nl
     320  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
     321                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
     322  ].
     323
     324naxiom assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
     325(*nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
     326#t; napply (type_ind2l ? (λtl. ∃p.assert_typelist_eq tl tl = OK ? p) … t);
     327##[ @ (refl ??); // ##| #sz si; ncases sz; ncases si; @ (refl ??); //;
     328##| #sz; ncases sz; @ ?; //;
     329##| #sp ty IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH; @ ?; //;
     330##| #sp ty n IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH;
     331    nwhd in ⊢ (??(λ_.??%?)); ncases (decidable_eq_Z_Type n n);
     332    ##[ ##1,3,5,7,9,11: #H; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
     333    ##| ##*: #H; napply False_ind; /2/;
     334    ##]
     335##| #tys ty IH1 IH2; @ ?;
     336    ##[ ##2: nwhd in ⊢ (??%?); nelim IH1; #p1 e1;
     337    nrewrite > e1; nwhd in ⊢ (??%?);
     338    nelim IH2;
     339    *)
     340
     341nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
     342#f; ncases f; #ty; #_; #_; #_; ncases ty;
     343##[ #H; napply False_ind; /2/;
     344##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
     345    #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
     346nqed.
     347
     348nlemma alloc_vars_complete: ∀env,m,l,env',m'.
     349  alloc_variables env m l env' m' →
     350  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
     351#env m l env' m' H; nelim H;
     352##[ #env'' m''; @ ?; nwhd; //;
     353##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
     354    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
     355    ndestruct (H1);
     356    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
     357##] nqed.
     358
     359nlemma bind_params_complete: ∀e,m,params,vs,m2.
     360  bind_parameters e m params vs m2 →
     361  yields ?? (exec_bind_parameters e m params vs) m2.
     362#e m params vs m2 H; nelim H;
     363##[ //;
     364##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
     365    napply remove_res_sig;
     366    nrewrite > H1; nwhd in ⊢ (??%?);
     367    nrewrite > H2; nwhd in ⊢ (??%?);
     368    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
     369    napply refl;
     370##] nqed.
     371
     372nlemma eventval_match_complete: ∀ev,ty,v.
     373  eventval_match ev ty v → yields ?? (check_eventval ev ty) v.
     374#ev ty v H; nelim H; //; nqed.
     375
     376nlemma eventval_match_complete': ∀ev,ty,v.
     377  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
     378#ev ty v H; nelim H; //; nqed.
     379
     380nlemma eventval_list_match_complete: ∀vs,tys,evs.
     381  eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
     382#vs tys evs H; nelim H;
     383##[ //
     384##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
     385    nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     386    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     387    napply refl;
     388##] nqed.   
     389
     390
     391ntheorem step_complete: ∀ge,s,tr,s'.
     392  step ge s tr s' → yieldsIO ?? (exec_step ge s) 〈tr,s'〉.
     393#ge s tr s' H; nelim H;
     394##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; napply remove_io_sig;
     395    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     396    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     397    nrewrite > H3; napply refl;
     398##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; napply remove_io_sig;
     399    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     400    nelim (yields_eq ???? (exprlist_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     401    nrewrite > H3; nwhd in ⊢ (??%?);
     402    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
     403    napply refl;
     404##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; napply remove_io_sig;
     405    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     406    nelim (yields_eq ???? (exprlist_complete … H3)); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     407    nrewrite > H4; nwhd in ⊢ (??%?);
     408    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
     409    nwhd in ⊢ (??%?);
     410    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     411    napply refl;
     412##| #f s1 s2 k env m; napply refl
     413##| ##5,6,7: #f s k env m; napply refl
     414##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
     415    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     416    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     417    napply refl
     418##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
     419    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     420    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
     421    napply refl
     422##| #f e s k env m v tr H1 H2; napply remove_io_sig;
     423    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     424    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
     425    napply refl
     426##| #f e s k env m v tr H1 H2; napply remove_io_sig;
     427    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     428    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     429    napply refl
     430##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
     431##| ##13,14: #f e s k env m; napply refl
     432##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
     433    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     434    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
     435    napply refl
     436##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
     437    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     438    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     439    napply refl
     440##| #f e s k env m; napply refl;
     441##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (???%?); ncases (is_Sskip s1);
     442    ##[ #H; napply False_ind; /2/;
     443    ##| #H; napply remove_io_sig; napply refl ##]
     444##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
     445    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     446    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
     447    napply refl;
     448##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
     449    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     450    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     451    napply refl;
     452##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
     453##| ##22,23: #f e s1 s2 k env m; napply refl;
     454##| napply daemon (* FIXME: rewrite causes failure at nqed  #f k env m H; nwhd in ⊢ (???%?); nrewrite > H; napply refl;*)
     455##| #f e k env m v tr H1 H2; napply remove_io_sig;
     456    nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
     457    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     458    napply refl;
     459##| #f k env m; ncases k;
     460    ##[ #H1 H2; napply daemon (* FIXME nwhd in ⊢ (???%?); nrewrite > H2; napply refl; *)
     461    ##| #s' k'; nwhd in ⊢ (% → ?); *;
     462    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
     463    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
     464    ##| #k'; nwhd in ⊢ (% → ?); *;
     465    ##| #r f' env' k' H1 H2; napply daemon (* FIXME typing error at nqed nwhd in ⊢ (???%?); nrewrite > H2; napply refl *)
     466    ##]
     467##| #f e s k env m i tr H1; napply remove_io_sig;
     468    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     469    napply refl
     470##| #f s k env m; napply daemon (* FIXME *; #es; nrewrite > es; napply refl;*)
     471##| #f k env m; napply refl
     472##| #f l s k env m; napply refl
     473##| #f l k env m s k' H1; napply daemon(* FIXME nwhd in ⊢ (???%?); nrewrite > H1; napply refl; *)
     474##| #f args k m1 env m2 m3 H1 H2; napply remove_io_sig;
     475    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     476    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
     477    napply refl;
     478##| #id tys rty args k m rv tr H; napply remove_io_sig;
     479    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
     480    #H1 H2;
     481    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     482    nwhd; @ erv; nwhd in ⊢ (??%?);
     483    nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
     484##| #v f env k m; nwhd in ⊢ (???%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
     485##| #v f env k m1 m2 sp loc ofs ty H; napply remove_io_sig;
     486    nrewrite > H; napply refl
     487##| #f l s k env m; napply refl
     488##] nqed.
     489 
Note: See TracChangeset for help on using the changeset viewer.