source: src/Clight/labelSpecification.ma @ 3367

Last change on this file since 3367 was 2319, checked in by campbell, 7 years ago

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File size: 1.5 KB
Line 
1include "Clight/Cexec.ma".
2include "Clight/label.ma".
3include "common/Executions.ma".
4
5(* Formalise the notion of a trace with extra cost labels added.  Note that
6   we don't require the left trace to be cost free (we possibly should...).  *)
7inductive trace_with_extra_labels : trace → trace → Prop ≝
8| twel_0 : trace_with_extra_labels E0 E0
9| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
10| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
11
12(* One execution is simulated by another, but possibly using more steps and
13   introducing some cost labels. *)
14
15coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
16| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
17    steps state tr2 e2 (e_stop … tr2' r s2) →
18    trace_with_extra_labels tr1 tr2 →
19    sim_with_labels (e_stop … tr1 r s1) e2
20| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
21    steps state tr2 e2 e2' →
22    trace_with_extra_labels tr1 tr2 →
23    sim_with_labels e1 e2' →
24    sim_with_labels (e_step … tr1 s1 e1) e2
25| swl_interact : ∀o,k1,k2.
26    (∀i. sim_with_labels (k1 i) (k2 i)) →
27    sim_with_labels (e_interact … o k1) (e_interact … o k2).
28
29(* Desired result *)
30
31definition labelled_exec_is_equiv : Prop ≝
32∀p:clight_program.
33  let e1 ≝ exec_inf … clight_fullexec p in
34  let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label p)) in
35  not_wrong state e1 →
36  sim_with_labels e1 e2.
Note: See TracBrowser for help on using the repository browser.