Changeset 2134


Ignore:
Timestamp:
Jun 28, 2012, 12:37:38 PM (5 years ago)
Author:
campbell
Message:

Split out behavioural equivalence spec for labelling.

Location:
src/Clight
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2118 r2134  
    11
    2 include "Clight/label.ma".
    3 include "Clight/Cexec.ma".
     2include "Clight/labelSpecification.ma".
    43include "Clight/CexecInd.ma".
    54
     
    3635qed.
    3736
    38 (* Formalise the notion of a trace with extra cost labels added.  Note that
    39    we don't require the left trace to be cost free.  *)
    40 inductive trace_with_extra_labels : trace → trace → Prop ≝
    41 | twel_0 : trace_with_extra_labels E0 E0
    42 | twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
    43 | twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
     37(* Lemmas about trace_with_extra_labels *)
    4438
    4539lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
     
    5347#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
    5448qed. 
     49
    5550
    5651theorem label_expr_ok : ∀ge,ge',en,m.
     
    10911086 
    10921087
    1093 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
    1094 | steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
    1095 | steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
    1096 | steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
    1097 
    1098 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
    1099 | swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
    1100     steps tr2 e2 (e_stop … tr2' r s2) →
    1101     trace_with_extra_labels tr1 tr2 →
    1102     sim_with_labels (e_stop … tr1 r s1) e2
    1103 | swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
    1104     steps tr2 e2 e2' →
    1105     trace_with_extra_labels tr1 tr2 →
    1106     sim_with_labels e1 e2' →
    1107     sim_with_labels (e_step … tr1 s1 e1) e2.
    1108 
    1109 coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝
    1110 | nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)
    1111 | nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).
    11121088
    11131089lemma not_wrong_init : ∀p.
     
    12271203
    12281204
    1229 theorem labelling_sim : ∀p.
    1230   let e1 ≝ exec_inf … clight_fullexec p in
    1231   let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
    1232   not_wrong_no_io e1 →
    1233   sim_with_labels e1 e2.
     1205theorem labelling_sim : labelled_exec_is_equiv.
     1206whd (* let's remind ourselves of the spec *)
    12341207#p
    12351208#NW
     
    12391212#s2 * #I2
    12401213
    1241 whd in match (exec_inf ??? p) in NW ⊢ %;
    1242 letin ge1 ≝ (make_global ??? p) in NW ⊢ %;
    1243 change with (make_initial_state p) in match (make_initial_state ??? p);
     1214whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
     1215letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
     1216change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
    12441217>I1
    12451218
Note: See TracChangeset for help on using the changeset viewer.