Changeset 2953 for src/common


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2727 r2953  
    6060      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
    6161    );
    62   sim_call_return :
     62  sim_call :
    6363    ∀g1,g2.
    6464    ∀INV:ms_inv g1 g2.
    6565    ∀s1,s1'.
    6666    ms_rel g1 g2 INV s1 s1' →
    67     match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
     67    pcs_classify ms_C1 g1 s1 = cl_call →
     68    ¬ pcs_labelled ms_C1 g1 s1 →
     69    (* NB: calls and returns don't emit timing cost labels; otherwise we would
     70       have to worry about whether the cost labels seen at the final return of
     71       the measured trace might appear in the target in subsequent steps that
     72       are *after* the new measurable subtrace.  Also note that extra steps are
     73       introduced in the front-end: to perform variable saves on entry and to
     74       write back the result *after* exit.  The latter do not get included in
     75       the measurable subtrace because it stops at the return, and they are the
     76       caller's responsibility. *)
     77    ∀s2,tr.
     78      if pcs_labelled ms_C1 g1 s2 then
     79        (∃si,tri1,tri2. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tri1,si〉 ∧
     80          bool_to_Prop (pcs_labelled ms_C1 g1 si) ∧
     81          step … (pcs_exec ms_C1) g1 si = Value … 〈tri1,s2〉 ∧
     82          tr = tri1 ⧺ tri2)
     83      else
     84        (step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉)
     85      →
     86    ∃m.
     87      after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
     88      tr = tr' ∧
     89      ms_rel g1 g2 INV s2 s2'
     90    );
     91  sim_return :
     92    ∀g1,g2.
     93    ∀INV:ms_inv g1 g2.
     94    ∀s1,s1'.
     95    ms_rel g1 g2 INV s1 s1' →
     96    pcs_classify ms_C1 g1 s1 = cl_return →
    6897    ¬ pcs_labelled ms_C1 g1 s1 →
    6998    (* NB: calls and returns don't emit timing cost labels; otherwise we would
     
    196225qed.
    197226
     227
     228(* TODO repair proof
    198229
    199230lemma prefix_preserved :
     
    634665  #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' %
    635666] qed.
     667*)
Note: See TracChangeset for help on using the changeset viewer.