Changeset 3096 for src/RTL/RTL_separate_to_overflow.ma

Timestamp:

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

Author:

tranquil

Message:

preliminary work on closing correctness.ma

File:

• src/RTL/RTL_separate_to_overflow.ma (modified) (3 diffs)

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.
-
-
-
-
+*)