Changeset 3096 for src/RTL

Timestamp:

Apr 5, 2013, 6:04:14 PM (8 years ago)

Author:

tranquil

Message:

preliminary work on closing correctness.ma

Location:

src/RTL

Files:

• RTLToERTLAxiom.ma (modified) (1 diff)
• RTL_overflow_to_unique.ma (modified) (1 diff)
• RTL_separate_to_overflow.ma (modified) (3 diffs)

src/RTL/RTLToERTLAxiom.ma

@@ -5 +5 @@
 include "common/StatusSimulation.ma".
 
-axiom RTLabsToRTL_ok :
+axiom RTLToERTL_ok :
 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
 ∀p_in : rtl_program.
 let p_out ≝ rtl_to_ertl p_in in
+  ∀init_in.make_initial_state
+    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
+∃init_out.
+  make_initial_state
+   (mk_prog_params ERTL_semantics p_out stacksizes) =
+    OK ? init_out ∧
 ∃[1] R.
-  status_simulation
+  status_simulation_with_init
     (joint_status RTL_semantics_unique p_in stacksizes)
     (joint_status ERTL_semantics p_out stacksizes)
-    R ∧
-  ∀init_in.make_initial_state
-    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
-  ∃init_out.
-    make_initial_state
-     (mk_prog_params ERTL_semantics p_out stacksizes) =
-      OK ? init_out ∧
-   R init_in init_out.
+    R init_in init_out.

src/RTL/RTL_overflow_to_unique.ma

@@ -6 +6 @@
 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
 ∀p_in : rtl_program.
+∀init_in.make_initial_state
+  (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
+∃init_out.
+  make_initial_state
+   (mk_prog_params RTL_semantics_unique p_in stacksizes) =
+    OK ? init_out ∧
 ∃[1] R.
-  status_simulation
+  status_simulation_with_init
     (joint_status RTL_semantics_separate_overflow p_in stacksizes)
     (joint_status RTL_semantics_unique p_in stacksizes)
-    R ∧
-  ∀init_in.make_initial_state
-    (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
-  ∃init_out.
-    make_initial_state
-     (mk_prog_params RTL_semantics_unique p_in stacksizes) =
-      OK ? init_out ∧
-   R init_in init_out.
+    R init_in init_out.

src/RTL/RTL_separate_to_overflow.ma

@@ -2 +2 @@
 include "joint/Traces.ma".
 include "common/stacksize.ma".
+include "common/StatusSimulation.ma".
+
+definition extract_call_ud_from_ft ≝
+  λS : abstract_status.λs1,s2.λft :flat_trace S s1 s2.
+  extract_call_ud_from_observables … (ft_observables … ft).
+
+definition good_stack_usage_ft :
+  ∀p, stacksizes.
+  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
+  flat_trace … st1 st2 → Prop ≝
+  λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λft.
+  ∀m : ℕ.m < 2^16 →
+  let info ≝ mk_stacksize_info (stack_usage … st1) m in
+  let info' ≝ update_stacksize_info stacksizes info
+    (extract_call_ud_from_ft … ft) in
+  maximum info' < 2^16.
 
 definition good_stack_usage_tlr :
@@ -41 +57 @@
   maximum info' < 2^16.
 
+axiom RTL_separate_to_overflow_produce_ft_and_tlr :
+∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
+∀p_in : rtl_program.
+let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
+let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
+∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate.
+∀ft1 : flat_trace S1 st1 st1'.
+∀tlr1 : trace_label_return S1 st1' st1''.
+good_stack_usage_ft … ft1 →
+good_stack_usage_tlr … fn tlr1 →
+∃ft2 : flat_trace S2 st1 st1'.
+∃tlr2 : trace_label_return S2 st1' st1''.
+ft_observables … ft1 = ft_observables … ft2 ∧
+tlr_rel … tlr1 tlr2.
+
+(*
 axiom RTL_separate_to_overflow_produce_tlr :
 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
@@ -73 +105 @@
 good_stack_usage_tal … curr_id tal →
 trace_any_label S2 fl s1 s2.
-
-
-
-
+*)