Ignore:
Timestamp:
Jul 17, 2012, 6:57:39 PM (8 years ago)
Author:
campbell
Message:

Start defining equivalent executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSpecification.ma

    r2201 r2202  
    11include "Clight/Cexec.ma".
    22include "Clight/label.ma".
     3include "common/Executions.ma".
    34
    45(* Formalise the notion of a trace with extra cost labels added.  Note that
     
    910| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
    1011
    11 (* A finite trace is produced by some prefix of an execution. *)
    12 
    13 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
    14 | steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
    15 | steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
    16 | steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
    17 
    1812(* One execution is simulated by another, but possibly using more steps and
    1913   introducing some cost labels. *)
     
    2115coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
    2216| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
    23     steps tr2 e2 (e_stop … tr2' r s2) →
     17    steps state tr2 e2 (e_stop … tr2' r s2) →
    2418    trace_with_extra_labels tr1 tr2 →
    2519    sim_with_labels (e_stop … tr1 r s1) e2
    2620| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
    27     steps tr2 e2 e2' →
     21    steps state tr2 e2 e2' →
    2822    trace_with_extra_labels tr1 tr2 →
    2923    sim_with_labels e1 e2' →
     
    3327    sim_with_labels (e_interact … o k1) (e_interact … o k2).
    3428
    35 (* We do not consider wrong executions. *)
    36 
    37 coinductive not_wrong : execution state io_out io_in → Prop ≝
    38 | nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
    39 | nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
    40 | nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
    41 
    4229(* Desired result *)
    4330
     
    4633  let e1 ≝ exec_inf … clight_fullexec p in
    4734  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
    48   not_wrong e1 →
     35  not_wrong state e1 →
    4936  sim_with_labels e1 e2.
Note: See TracChangeset for help on using the changeset viewer.