Changeset 365 for C-semantics/CexecIOcomplete.ma

Timestamp:

Dec 2, 2010, 4:40:54 PM (10 years ago)

Author:

campbell

Message:

Soundness (really completeness) of Wrong executions.

File:

• C-semantics/CexecIOcomplete.ma (modified) (1 diff)

C-semantics/CexecIOcomplete.ma

@@ -485 +485 @@
 ##] nqed.
   
+nlemma wrong_sound: ∀ge,tr,s,s',e.
+  execution_goes_wrong tr s e s' →
+  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
+  star (mk_transrel … step) ge s tr s' ∧
+  nostep (mk_transrel … step) ge s' ∧
+  (¬∃r. final_state s' r).
+#ge tr0 s0 s0' e0 WRONG; ncases WRONG;
+#tr s s' e ESTEPS EXEC;
+ncases (several_steps … ESTEPS EXEC);
+#STAR EXEC'; @;
+##[ @; ##[ napply STAR;
+       ##| #badtr bads; @; #badSTEP;
+           nlapply (step_complete … badSTEP);
+           nlapply (exec_e_step … EXEC');
+           ncases (exec_step ge s');
+           ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?);
+               ndestruct
+           ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …);
+               nwhd in ⊢ (??%? → ?); ncases (is_final_state stx);
+               #FINAL E; nwhd in E:(??%?); ndestruct
+           ##| #E H; nwhd in H; napply H
+           ##]
+       ##]
+##| @; #FINAL;
+    nrewrite > (exec_inf_aux_unfold …) in EXEC'; 
+    nwhd in ⊢ (??%? → ?);
+    ncases (is_final_state s'); #FINAL';
+    ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct;
+    ##| napply False_ind; napply (absurd … FINAL FINAL');
+    ##]
+##] nqed.