Changeset 2134 for src/Clight/labelSimulation.ma

Timestamp:

Jun 28, 2012, 12:37:38 PM (8 years ago)

Author:

campbell

Message:

Split out behavioural equivalence spec for labelling.

File:

• src/Clight/labelSimulation.ma (modified) (6 diffs)

src/Clight/labelSimulation.ma

@@ -1 +1 @@
 
-include "Clight/label.ma".
-include "Clight/Cexec.ma".
+include "Clight/labelSpecification.ma".
 include "Clight/CexecInd.ma".
 
@@ -36 +35 @@
 qed.
 
-(* Formalise the notion of a trace with extra cost labels added.  Note that
-   we don't require the left trace to be cost free.  *)
-inductive trace_with_extra_labels : trace → trace → Prop ≝
-| twel_0 : trace_with_extra_labels E0 E0
-| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
-| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
+(* Lemmas about trace_with_extra_labels *)
 
 lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
@@ -53 +47 @@
 #tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
 qed.  
+
 
 theorem label_expr_ok : ∀ge,ge',en,m.
@@ -1091 +1086 @@
   
 
-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'.
-
-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) →
-    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' →
-    trace_with_extra_labels tr1 tr2 →
-    sim_with_labels e1 e2' →
-    sim_with_labels (e_step … tr1 s1 e1) e2.
-
-coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
-| nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
-| nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
 
 lemma not_wrong_init : ∀p.
@@ -1227 +1203 @@
 
 
-theorem labelling_sim : ∀p.
-  let e1 ≝ exec_inf … clight_fullexec p in
-  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
-  not_wrong_no_io e1 →
-  sim_with_labels e1 e2.
+theorem labelling_sim : labelled_exec_is_equiv.
+whd (* let's remind ourselves of the spec *)
 #p
 #NW
@@ -1239 +1212 @@
 #s2 * #I2
 
-whd in match (exec_inf ??? p) in NW ⊢ %;
-letin ge1 ≝ (make_global ??? p) in NW ⊢ %;
-change with (make_initial_state p) in match (make_initial_state ??? p);
+whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
+letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
+change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
 >I1