source: src/Cminor/toRTLabsCorrectness.ma @ 2511

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

Conjecture main Cminor/RTLabs simulation results.
Add a few notes about measurable traces.

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