Changeset 2597 for src/Cminor/toRTLabsCorrectness.ma

Timestamp:

Jan 31, 2013, 12:07:02 PM (7 years ago)

Author:

campbell

Message:

Some work in progress on measurable subtrace preservation.

File:

• src/Cminor/toRTLabsCorrectness.ma (modified) (2 diffs)

src/Cminor/toRTLabsCorrectness.ma

@@ -2 +2 @@
 include "Cminor/abstract.ma".
 include "RTLabs/abstract.ma".
+include "Cminor/toRTLabs.ma".
 
 record cminor_rtlabs_inv : Type[0] ≝ {
@@ -68 +69 @@
     cminor_rtlabs_rel INV s2 s2'
   ).
+
+(* Note that we start from the "no initialisation" version of the Cminor
+   semantics.  I plan to prove the initialisation generation separately. *)
+
+axiom cminor_noinit_rtlabs_init : ∀cm_program,ra_program,s,s'.
+  cminor_noinit_to_rtlabs cm_program = ra_program →
+  make_initial_state ?? Cminor_noinit_fullexec cm_program = OK ? s →
+  make_initial_state ?? RTLabs_fullexec ra_program = OK ? s' →
+  ∃INV. cminor_rtlabs_rel INV s s'.
+