Changeset 2953


Ignore:
Timestamp:
Mar 26, 2013, 3:34:30 PM (4 years ago)
Author:
campbell
Message:

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

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2877 r2953  
    15221522
    15231523(* params and statement aren't real parameters, they're just there for giving the invariant. *)
    1524 definition alloc_params :
     1524definition alloc_params_main :
    15251525 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
    15261526   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
     
    15441544@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
    15451545qed.
     1546
     1547(* For a soundly-labelled program there will be a cost label at the start of the
     1548   function.  We should keep it there to keep it soundly-labelled. *)
     1549
     1550definition alloc_params :
     1551 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
     1552   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝
     1553λvars,lbls,statement,uv,ul,rettyp,params,su.
     1554  match su return λsu. trans_inv vars lbls statement uv ul rettyp su → ? with
     1555  [ mk_Prod tl s0 ⇒
     1556    match s0 return λs. trans_inv vars lbls statement uv ul rettyp 〈tl, s〉 → ? with
     1557    [ St_cost cl s' ⇒ λinv.
     1558      ! tls ← alloc_params_main vars lbls statement uv ul rettyp params «〈tl,s'〉,?»;
     1559      return «〈\fst tls,St_cost cl (\snd tls)〉, ?»
     1560    | _ ⇒ λ_. alloc_params_main vars lbls statement uv ul rettyp params su
     1561    ]
     1562  ] (pi2 ?? su).
     1563[ cases tl in inv ⊢ %;
     1564  #tg #lg * * * * * #SV #SP #LT #TP * #_ #RO * #_ #LW whd
     1565  % [ % [ % [ % [ @SP | @LT ]| @TP ]| @RO ]| @LW ]
     1566| cases tls * * #tg #lb #s * * * * #SI #LT #TP #RO #LW whd
     1567  % [ % [ % [ % [ % [ // | @SI ] | @LT ]| @TP ]| % // ]| % // ]
     1568] qed.
     1569
    15461570
    15471571definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
  • 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.