1 | include "Clight/Cexec.ma". |
---|
2 | include "Clight/label.ma". |
---|
3 | include "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...). *) |
---|
7 | inductive 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 | |
---|
15 | coinductive 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 | |
---|
31 | definition 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. |
---|