Changeset 2953 for src/common
- Timestamp:
- Mar 26, 2013, 3:34:30 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/FEMeasurable.ma
r2727 r2953 60 60 (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1)) 61 61 ); 62 sim_call _return:62 sim_call : 63 63 ∀g1,g2. 64 64 ∀INV:ms_inv g1 g2. 65 65 ∀s1,s1'. 66 66 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 → 68 97 ¬ pcs_labelled ms_C1 g1 s1 → 69 98 (* NB: calls and returns don't emit timing cost labels; otherwise we would … … 196 225 qed. 197 226 227 228 (* TODO repair proof 198 229 199 230 lemma prefix_preserved : … … 634 665 #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % 635 666 ] qed. 667 *)
Note: See TracChangeset
for help on using the changeset viewer.