source: src/Cminor/toRTLabsCorrectness.ma @ 2597

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

Some work in progress on measurable subtrace preservation.

File size: 3.1 KB
Line 
1
2include "Cminor/abstract.ma".
3include "RTLabs/abstract.ma".
4include "Cminor/toRTLabs.ma".
5
6record cminor_rtlabs_inv : Type[0] ≝ {
7  ge_cm : cm_genv;
8  ge_ra : RTLabs_genv
9}.
10axiom cminor_rtlabs_rel : cminor_rtlabs_inv → Cminor_state → RTLabs_state → Prop.
11
12(* Conjectured simulation results
13
14   We split these based on the start state:
15   
16   1. ‘normal’ states take some [S n] normal steps and simulates them by [m]
17      normal steps in RTLabs ([m] can be zero if the Cminor program executed an
18      St_skip);
19   2. call and return steps are simulated by a call/return step plus [m] normal
20      steps (to copy stack allocated parameters / results); and
21   3. lone cost label steps are simulates by a lone cost label step
22
23   Note that we'll need something more to show that non-termination is
24   preserved (because it isn't obvious that we don't squash a loop to zero
25   instructions).  Options are a traditional measure, or using the soundness of
26   the cost labelling.
27
28   These should allow us to maintain enough structure to identify the RTLabs
29   subtrace corresponding to a measurable Clight/Cminor subtrace.
30 *)
31
32definition cminor_normal : Cminor_state → bool ≝
33λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
34
35definition rtlabs_normal : RTLabs_state → bool ≝
36λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
37
38axiom cminor_rtlabs_normal :
39  ∀INV:cminor_rtlabs_inv.
40  ∀s1,s1',s2,tr.
41  cminor_rtlabs_rel INV s1 s1' →
42  cminor_normal s1 →
43  ¬ Cminor_labelled s1 →
44  ∃n. after_n_steps (S n) … Cminor_exec (ge_cm INV) s1 (λs.cminor_normal s ∧ ¬ Cminor_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
45  ∃m. after_n_steps m … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
46    tr = tr' ∧
47    cminor_rtlabs_rel INV s2 s2'
48  ).
49
50axiom cminor_rtlabs_call_return :
51  ∀INV:cminor_rtlabs_inv.
52  ∀s1,s1',s2,tr.
53  cminor_rtlabs_rel INV s1 s1' →
54  match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] →
55  after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
56  ∃m. after_n_steps (S m) … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'.
57    tr = tr' ∧
58    cminor_rtlabs_rel INV s2 s2'
59  ).
60
61axiom cminor_rtlabs_cost :
62  ∀INV:cminor_rtlabs_inv.
63  ∀s1,s1',s2,tr.
64  cminor_rtlabs_rel INV s1 s1' →
65  Cminor_labelled s1 →
66  after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
67  after_n_steps 1 … RTLabs_exec (ge_ra INV) s1' (λs.true) (λtr',s2'.
68    tr = tr' ∧
69    cminor_rtlabs_rel INV s2 s2'
70  ).
71
72(* Note that we start from the "no initialisation" version of the Cminor
73   semantics.  I plan to prove the initialisation generation separately. *)
74
75axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'.
76  cminor_noinit_to_rtlabs cm_program = ra_program →
77  make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s →
78  make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' →
79  ∃INV. cminor_rtlabs_rel INV s s'.
80
Note: See TracBrowser for help on using the repository browser.