Changeset 2202 for src/Clight/labelSpecification.ma

Timestamp:

Jul 17, 2012, 6:57:39 PM (8 years ago)

Author:

campbell

Message:

Start defining equivalent executions.

File:

• src/Clight/labelSpecification.ma (modified) (5 diffs)

src/Clight/labelSpecification.ma

@@ -1 +1 @@
 include "Clight/Cexec.ma".
 include "Clight/label.ma".
+include "common/Executions.ma".
 
 (* Formalise the notion of a trace with extra cost labels added.  Note that
@@ -9 +10 @@
 | twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
 
-(* A finite trace is produced by some prefix of an execution. *)
-
-inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
-| steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
-| steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
-| steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
-
 (* One execution is simulated by another, but possibly using more steps and
    introducing some cost labels. *)
@@ -21 +15 @@
 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
 | swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
-    steps tr2 e2 (e_stop … tr2' r s2) →
+    steps state tr2 e2 (e_stop … tr2' r s2) →
     trace_with_extra_labels tr1 tr2 →
     sim_with_labels (e_stop … tr1 r s1) e2
 | swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
-    steps tr2 e2 e2' →
+    steps state tr2 e2 e2' →
     trace_with_extra_labels tr1 tr2 →
     sim_with_labels e1 e2' →
@@ -33 +27 @@
     sim_with_labels (e_interact … o k1) (e_interact … o k2).
 
-(* We do not consider wrong executions. *)
-
-coinductive not_wrong : execution state io_out io_in → Prop ≝
-| nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
-| nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
-| nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
-
 (* Desired result *)
 
@@ -46 +33 @@
   let e1 ≝ exec_inf … clight_fullexec p in
   let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
-  not_wrong e1 →
+  not_wrong state e1 →
   sim_with_labels e1 e2.