Changeset 239

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:

• CexecIO.ma (modified) (3 diffs)
• CexecIOcomplete.ma (modified) (7 diffs)

C-semantics/CexecIO.ma

@@ -865 +865 @@
 nqed.
 
-ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
+ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
 #st; nelim st;
 ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
@@ -931 +931 @@
 (* A (possibly non-terminating) execution. *)
 ncoinductive execution : Type ≝
-| e_stop : trace → state → execution
+| e_stop : trace → int → execution
 | e_step : trace → state → execution → execution
 | e_wrong : execution
@@ -941 +941 @@
 | Value v ⇒ match v with [ mk_pair t s' ⇒ 
     match is_final_state s' with
-    [ inl _ ⇒ e_stop t s'
+    [ inl r ⇒ e_stop t (sig_eject … r)
     | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
 | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
 ].
 
+
 ndefinition exec_inf : program → execution ≝
 λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
 
+(*
+FIXME: unfolding cofixpoints appears to be rather tricky.
+
+nremark execution_cases: ∀e.
+ e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
+ | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
+#e; ncases e; //; nqed.
+
+nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
+match s with
+[ Wrong ⇒ e_wrong
+| Value v ⇒ match v with [ mk_pair t s' ⇒ 
+    match is_final_state s' with
+    [ inl r ⇒ e_stop t (sig_eject … r)
+    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
+| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
+].
+#ge s; nrewrite > (execution_cases (exec_inf_aux …));
+ncases s; //; napply refl;
+
+
+nlemma exec_inf_aux_wrong: ∀ge,s. exec_inf_aux ge s = e_wrong → s = Wrong ….
+#ge s; ncases s;
+##[ #o k EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
+    ndestruct;
+##| #v; ncases v; #tr s'; #EXEC; nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC; nnormalize in EXEC;
+    ncases (is_final_state s');
+    ndestruct;
+*)
+
+(* Finite number of steps without interaction. *)
+ninductive execution_steps : trace → execution → execution → Prop ≝
+| steps_none : ∀e. execution_steps E0 e e
+| steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
+
+(* Finite number of steps allowing interaction. *)
+ninductive execution_isteps : trace → execution → execution → Prop ≝
+| isteps_none : ∀e. execution_isteps E0 e e
+| isteps_step : ∀e,e',tr,tr',s. execution_isteps tr e e' → execution_isteps (tr⧺tr') (e_step tr s e) e'
+| isteps_interact : ∀k,o,i,e',tr. execution_isteps tr (k i) e' → execution_isteps tr (e_interact o k) e'.
+
+ninductive execution_terminates : trace → int → execution → Prop ≝
+| terminates : ∀tr,tr',r,e. execution_isteps tr e (e_stop tr' r) → execution_terminates (tr⧺tr') r e.
+
+ncoinductive execution_diverging : execution → Prop ≝
+| diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
+
+(* Makes a finite number of interactions (including cost labels) before diverging. *)
+ninductive execution_diverges : trace → execution → Prop ≝
+| diverges_diverging: ∀tr,e,e'.
+    execution_isteps tr e e' →
+    execution_diverging e' →
+    execution_diverges tr e.
+
+(* NB: "reacting" includes hitting a cost label. *)
+ncoinductive execution_reacts : traceinf → execution → Prop ≝
+| reacting: ∀tr,tr',e,e'. execution_reacts tr' e' → execution_isteps tr e e' → tr ≠ E0 → execution_reacts (tr⧻tr') e. 
+
+ninductive execution_goes_wrong: trace → execution → Prop ≝
+| go_wrong: ∀tr,e. execution_isteps tr e e_wrong → execution_goes_wrong tr e.
+
+ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
+| emb_terminates: ∀e,tr,r.
+    execution_terminates tr r e →
+    execution_matches_behavior e (Terminates tr r)
+| emb_diverges: ∀e,tr.
+    execution_diverges tr e → 
+    execution_matches_behavior e (Diverges tr)
+| emb_reacts: ∀e,tr.
+    execution_reacts tr e →
+    execution_matches_behavior e (Reacts tr)
+| emb_wrong: ∀e,tr.
+    execution_goes_wrong tr e →
+    execution_matches_behavior e (Goes_wrong tr).
+
+(*
+nlemma silent_sound: ∀ge,s,e.
+  execution_diverging e →
+  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
+  forever_silent (mk_transrel ?? step) … ge s.
+#ge s e H; ncases H; #s1 e1 H' EXEC;
+napply (forever_silent_intro (mk_transrel ?? step) … ge s s1);
+##[ nrewrite > (execution_cases (exec_inf_aux …)) in EXEC; #EXEC;
+    nnormalize in EXEC;
+ nnormalize in match exec_inf_aux in EXEC:(??%?);
+
+ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
+*)

C-semantics/CexecIOcomplete.ma

@@ -4 +4 @@
 ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
-ndefinition yieldsIO : ∀A,P. IO eventval io_out (Σx:A. P x) → A → Prop ≝
-λA,P,e,v. match e with [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
-(*
-ndefinition yields : ∀A.∀P:A → Prop. res (sigma A P) → A → Prop ≝
-λA,P,e,v. err_eject A P e = OK ? v.
-*)
+
+(* This tells us that some execution of e results in v.
+   (There may be many possible executions due to I/O, but we're trying to prove
+   that one particular one exists corresponding to a derivation in the inductive
+   semantics.) *)
+nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out (Σx:A. P x)) (v:A) on e : Prop ≝
+match e with
+[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
+| Interact _ k ⇒ ∃r.yieldsIO A P (k r) v
+| _ ⇒ False].
+
 nlemma is_pointer_compat_true: ∀m,b,sp.
   pointer_compat (block_space m b) sp →
@@ -27 +32 @@
 interpretation "yields" 'yields e e' = (yields ?? e e').
 interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
-(*
-(*notation < "vbox( ident v ← e;: break e' )" with precedence 40 for @{'bindnat ${e} (\lambda ${ident v} : ${ty}. ${e'})}.*)
-notation < "vbox( e ;: break e' )" with precedence 40 for @{'binde ${e} ${e'}}.
-notation < "vbox( ident v ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v}. ${e'})}.
-notation < "vbox( ident v : ty ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v} : ${ty}. ${e'})}.
-interpretation "error monad bind" 'binde e f = (bind ? ? e f).
-(*interpretation "error monad bind" 'bindnat e f = (bind nat nat e f).*)
-
-nlemma foo: ∀e:res nat. ∀f: nat → res nat. (x ← e;: f x) = OK ? 5.
-*)
-(*interpretation "error monad bind" 'bind e f = (bind ? ? e f).*)
 
 ntheorem is_det: ∀p,s,s'.
@@ -53 +47 @@
 ##] nqed.
 
-ndefinition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A.
-match a with [ Value v ⇒ v' = v | _ ⇒ False ].
+nlet rec yieldsIObare (A:Type) (a:IO eventval io_out A) (v':A) on a : Prop ≝
+match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
 
 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
 yieldsIObare A a v' →
 yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
-#A P a; ncases a;
-##[ #a b c d; *;
+#A P a; nelim a;
+##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
 ##| #v v' p H; napply H;
 ##| #a b; *;
@@ -113 +107 @@
 ##| *;
 ##] nqed.
-(*
-nlemma lvalue_complete_cond: ∀ge,env,m.
-(∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) →
-(∀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〉)).
-#ge env m IH;
-#e sp l off tr H; napply (eval_lvalue_ind … H);
-##[ #id l ty H1; nwhd in ⊢ (???%?);
-    nrewrite > H1;
-    napply refl;
-##| #id sp l ty H1 H2; nwhd in ⊢ (???%?); 
-    nrewrite > H1; nwhd nodelta in ⊢ (???%?); napply remove_res_sig;
-    nrewrite > H2;
-*)
 
 (* Use to narrow down the choice of expression to just the lvalues. *)
@@ -184 +165 @@
 ##] nqed. 
 
-nlemma expr_complete: ∀ge,env,m.
+nlemma expr_lvalue_complete: ∀ge,env,m.
 (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧
 (∀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〉)).
@@ -255 +236 @@
  
  (* FIXME: next two cases produce type checking failures at nqed. *) 
-##|napply daemon; (* #id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
+##| napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
 ##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1);
     nrewrite > e2; napply refl;*)
@@ -272 +253 @@
 ##] nqed.
 
-
+ntheorem expr_complete:  ∀ge,env,m.
+ ∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉).
+#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
+
+ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
+  eval_exprlist ge env m es vs tr → yields ?? (exec_exprlist ge env m es) (〈vs,tr〉).
+#ge env m es vs tr H; nelim H;
+##[ napply refl;
+##| #e et v vt tr trt H1 H2 H3; napply remove_res_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
+    napply refl;
+##] nqed. 
+
+ntheorem lvalue_complete: ∀ge,env,m.
+ ∀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〉).
+#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
+
+nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
+match l with
+[ Tnil ⇒ True
+| Tcons h t ⇒ P h ∧ P_typelist P t
+].
+
+nlet rec type_ind2l
+  (P:type → Prop) (Q:typelist → Prop)
+  (vo:P Tvoid)
+  (it:∀i,s. P (Tint i s))
+  (fl:∀f. P (Tfloat f))
+  (pt:∀s,t. P t → P (Tpointer s t))
+  (ar:∀s,t,n. P t → P (Tarray s t n))
+  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
+  (st:∀i,fl. P (Tstruct i fl))
+  (un:∀i,fl. P (Tunion i fl))
+  (cp:∀i. P (Tcomp_ptr i))
+  (nl:Q Tnil)
+  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
+ (t:type) on t : P t ≝
+  match t return λt'.P t' with
+  [ Tvoid ⇒ vo
+  | Tint i s ⇒ it i s
+  | Tfloat s ⇒ fl s
+  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
+  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
+  | 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')
+  | Tstruct i fs ⇒ st i fs
+  | Tunion i fs ⇒ un i fs
+  | Tcomp_ptr i ⇒ cp i
+  ]
+and typelist_ind2l
+  (P:type → Prop) (Q:typelist → Prop)
+  (vo:P Tvoid)
+  (it:∀i,s. P (Tint i s))
+  (fl:∀f. P (Tfloat f))
+  (pt:∀s,t. P t → P (Tpointer s t))
+  (ar:∀s,t,n. P t → P (Tarray s t n))
+  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
+  (st:∀i,fl. P (Tstruct i fl))
+  (un:∀i,fl. P (Tunion i fl))
+  (cp:∀i. P (Tcomp_ptr i))
+  (nl:Q Tnil)
+  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
+  (ts:typelist) on ts : Q ts ≝
+  match ts return λts'.Q ts' with
+  [ Tnil ⇒ nl
+  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
+                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
+  ].
+
+naxiom assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
+(*nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
+#t; napply (type_ind2l ? (λtl. ∃p.assert_typelist_eq tl tl = OK ? p) … t);
+##[ @ (refl ??); // ##| #sz si; ncases sz; ncases si; @ (refl ??); //;
+##| #sz; ncases sz; @ ?; //;
+##| #sp ty IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH; @ ?; //;
+##| #sp ty n IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH;
+    nwhd in ⊢ (??(λ_.??%?)); ncases (decidable_eq_Z_Type n n);
+    ##[ ##1,3,5,7,9,11: #H; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
+    ##| ##*: #H; napply False_ind; /2/;
+    ##]
+##| #tys ty IH1 IH2; @ ?;
+    ##[ ##2: nwhd in ⊢ (??%?); nelim IH1; #p1 e1;
+    nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim IH2;
+    *)
+
+nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
+#f; ncases f; #ty; #_; #_; #_; ncases ty;
+##[ #H; napply False_ind; /2/;
+##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
+    #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
+nqed. 
+
+nlemma alloc_vars_complete: ∀env,m,l,env',m'.
+  alloc_variables env m l env' m' →
+  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
+#env m l env' m' H; nelim H;
+##[ #env'' m''; @ ?; nwhd; //;
+##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
+    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
+    ndestruct (H1);
+    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
+##] nqed.
+
+nlemma bind_params_complete: ∀e,m,params,vs,m2.
+  bind_parameters e m params vs m2 →
+  yields ?? (exec_bind_parameters e m params vs) m2.
+#e m params vs m2 H; nelim H;
+##[ //;
+##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
+    napply remove_res_sig;
+    nrewrite > H1; nwhd in ⊢ (??%?);
+    nrewrite > H2; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
+    napply refl;
+##] nqed.
+
+nlemma eventval_match_complete: ∀ev,ty,v.
+  eventval_match ev ty v → yields ?? (check_eventval ev ty) v.
+#ev ty v H; nelim H; //; nqed.
+
+nlemma eventval_match_complete': ∀ev,ty,v.
+  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
+#ev ty v H; nelim H; //; nqed.
+
+nlemma eventval_list_match_complete: ∀vs,tys,evs.
+  eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
+#vs tys evs H; nelim H;
+##[ //
+##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
+    nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
+    napply refl;
+##] nqed.    
+
+
+ntheorem step_complete: ∀ge,s,tr,s'.
+  step ge s tr s' → yieldsIO ?? (exec_step ge s) 〈tr,s'〉.
+#ge s tr s' H; nelim H;
+##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; napply remove_io_sig;
+    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
+    nrewrite > H3; napply refl;
+##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (exprlist_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
+    nrewrite > H3; nwhd in ⊢ (??%?);
+    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
+    napply refl;
+##| #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;
+    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (exprlist_complete … H3)); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
+    nrewrite > H4; nwhd in ⊢ (??%?);
+    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
+    nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    napply refl;
+##| #f s1 s2 k env m; napply refl
+##| ##5,6,7: #f s k env m; napply refl
+##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f e s k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f e s k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
+##| ##13,14: #f e s k env m; napply refl
+##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl
+##| #f e s k env m; napply refl; 
+##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (???%?); ncases (is_Sskip s1);
+    ##[ #H; napply False_ind; /2/;
+    ##| #H; napply remove_io_sig; napply refl ##]
+##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl;
+##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
+    napply refl;
+##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
+##| ##22,23: #f e s1 s2 k env m; napply refl;
+##| napply daemon (* FIXME: rewrite causes failure at nqed  #f k env m H; nwhd in ⊢ (???%?); nrewrite > H; napply refl;*)
+##| #f e k env m v tr H1 H2; napply remove_io_sig;
+    nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
+    napply refl;
+##| #f k env m; ncases k;
+    ##[ #H1 H2; napply daemon (* FIXME nwhd in ⊢ (???%?); nrewrite > H2; napply refl; *)
+    ##| #s' k'; nwhd in ⊢ (% → ?); *;
+    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
+    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
+    ##| #k'; nwhd in ⊢ (% → ?); *;
+    ##| #r f' env' k' H1 H2; napply daemon (* FIXME typing error at nqed nwhd in ⊢ (???%?); nrewrite > H2; napply refl *)
+    ##]
+##| #f e s k env m i tr H1; napply remove_io_sig;
+    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    napply refl
+##| #f s k env m; napply daemon (* FIXME *; #es; nrewrite > es; napply refl;*)
+##| #f k env m; napply refl
+##| #f l s k env m; napply refl
+##| #f l k env m s k' H1; napply daemon(* FIXME nwhd in ⊢ (???%?); nrewrite > H1; napply refl; *)
+##| #f args k m1 env m2 m3 H1 H2; napply remove_io_sig;
+    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
+    napply refl;
+##| #id tys rty args k m rv tr H; napply remove_io_sig;
+    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
+    #H1 H2;
+    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
+    nwhd; @ erv; nwhd in ⊢ (??%?);
+    nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
+##| #v f env k m; nwhd in ⊢ (???%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
+##| #v f env k m1 m2 sp loc ofs ty H; napply remove_io_sig;
+    nrewrite > H; napply refl
+##| #f l s k env m; napply refl
+##] nqed.
+