source: src/Cminor/toRTLabsCorrectness.ma @ 2844

Last change on this file since 2844 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.
File size: 3.1 KB
Line 
1
2include "Cminor/Cminor_abstract.ma".
3include "RTLabs/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.