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