source: src/Clight/labelSpecification.ma @ 2177

Last change on this file since 2177 was 2145, checked in by campbell, 8 years ago

Cost labelling doesn't affect interaction.

File size: 2.1 KB
Line 
1include "Clight/Cexec.ma".
2include "Clight/label.ma".
3
4(* Formalise the notion of a trace with extra cost labels added.  Note that
5   we don't require the left trace to be cost free (we possibly should...).  *)
6inductive trace_with_extra_labels : trace → trace → Prop ≝
7| twel_0 : trace_with_extra_labels E0 E0
8| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
9| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
10
11(* A finite trace is produced by some prefix of an execution. *)
12
13inductive 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
18(* One execution is simulated by another, but possibly using more steps and
19   introducing some cost labels. *)
20
21coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
22| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
23    steps tr2 e2 (e_stop … tr2' r s2) →
24    trace_with_extra_labels tr1 tr2 →
25    sim_with_labels (e_stop … tr1 r s1) e2
26| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
27    steps tr2 e2 e2' →
28    trace_with_extra_labels tr1 tr2 →
29    sim_with_labels e1 e2' →
30    sim_with_labels (e_step … tr1 s1 e1) e2
31| swl_interact : ∀o,k1,k2.
32    (∀i. sim_with_labels (k1 i) (k2 i)) →
33    sim_with_labels (e_interact … o k1) (e_interact … o k2).
34
35(* We do not consider wrong executions or I/O. *)
36
37coinductive 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
42(* Desired result *)
43
44definition labelled_exec_is_equiv : Prop ≝
45∀p:clight_program.
46  let e1 ≝ exec_inf … clight_fullexec p in
47  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
48  not_wrong e1 →
49  sim_with_labels e1 e2.
Note: See TracBrowser for help on using the repository browser.