Changeset 2953 for src/common

Timestamp:

Mar 26, 2013, 3:34:30 PM (7 years ago)

Author:

campbell

Message:

Fix silly label handling bug I realised was there during my talk...

File:

• src/common/FEMeasurable.ma (modified) (3 diffs)

src/common/FEMeasurable.ma

@@ -60 +60 @@
       (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
     );
-  sim_call_return :
+  sim_call :
     ∀g1,g2.
     ∀INV:ms_inv g1 g2.
     ∀s1,s1'.
     ms_rel g1 g2 INV s1 s1' →
-    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
+    pcs_classify ms_C1 g1 s1 = cl_call →
+    ¬ pcs_labelled ms_C1 g1 s1 →
+    (* NB: calls and returns don't emit timing cost labels; otherwise we would
+       have to worry about whether the cost labels seen at the final return of
+       the measured trace might appear in the target in subsequent steps that
+       are *after* the new measurable subtrace.  Also note that extra steps are
+       introduced in the front-end: to perform variable saves on entry and to
+       write back the result *after* exit.  The latter do not get included in
+       the measurable subtrace because it stops at the return, and they are the
+       caller's responsibility. *)
+    ∀s2,tr.
+      if pcs_labelled ms_C1 g1 s2 then
+        (∃si,tri1,tri2. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tri1,si〉 ∧
+          bool_to_Prop (pcs_labelled ms_C1 g1 si) ∧
+          step … (pcs_exec ms_C1) g1 si = Value … 〈tri1,s2〉 ∧
+          tr = tri1 ⧺ tri2)
+      else
+        (step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉)
+      →
+    ∃m.
+      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
+      tr = tr' ∧
+      ms_rel g1 g2 INV s2 s2'
+    );
+  sim_return :
+    ∀g1,g2.
+    ∀INV:ms_inv g1 g2.
+    ∀s1,s1'.
+    ms_rel g1 g2 INV s1 s1' →
+    pcs_classify ms_C1 g1 s1 = cl_return →
     ¬ pcs_labelled ms_C1 g1 s1 →
     (* NB: calls and returns don't emit timing cost labels; otherwise we would
@@ -196 +225 @@
 qed.
 
+
+(* TODO repair proof
 
 lemma prefix_preserved :
@@ -634 +665 @@
   #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % 
 ] qed.
+*)