Changeset 321 for C-semantics

Timestamp:

Nov 26, 2010, 7:00:11 PM (9 years ago)

Author:

campbell

Message:

Soundness for reactive executions.

File:

• C-semantics/CexecIO.ma (modified) (3 diffs)

C-semantics/CexecIO.ma

@@ -1427 +1427 @@
 
 (* NB: "reacting" includes hitting a cost label. *)
-ncoinductive execution_reacts : traceinf → execution → Prop ≝
-| reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') e. 
-
-ninductive execution_goes_wrong: trace → execution → Prop ≝
-| go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr e.
+ncoinductive execution_reacts : traceinf → state → execution → Prop ≝
+| reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' s' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') s e. 
+
+ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝
+| go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr s e s'.
 
 ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
@@ -1440 +1440 @@
     execution_diverges tr e → 
     execution_matches_behavior e (Diverges tr)
-| emb_reacts: ∀e,tr.
-    execution_reacts tr e →
+| emb_reacts: ∀s,e,tr.
+    execution_reacts tr s e →
     execution_matches_behavior e (Reacts tr)
-| emb_wrong: ∀e,tr.
-    execution_goes_wrong tr e →
+| emb_wrong: ∀e,s,s',tr.
+    execution_goes_wrong tr s e s' →
     execution_matches_behavior e (Goes_wrong tr).
 
@@ -1507 +1507 @@
 ##] nqed. 
 
+nlet corec reacts_sound ge tr s e
+  (REACTS:execution_reacts tr s e)
+  (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) :
+  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
+ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacts tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr'');
+##[ ninversion REACTS;
+    #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
+    @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
+##| *; #s'; *; #e'; *; #tr'; *; #tr'';
+    *; *; *; #REACTS' ESTEPS REACTED APPTR;
+(*    nrewrite > APPTR;*)
+    napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
+    @;
+    ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
+    ##[ ##2: napply STEPS;
+    ##| ##skip
+    ##| napply REACTED
+    ##| napply reacts_sound;
+      ##[ ##2: napply REACTS';
+      ##| ##skip
+      ##| napply EXEC'
+      ##]
+    ##]
+nqed.
+
+(* is/needs completeness...
+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';
+*)
+
 (*
 ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.