| 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. |
|---|
