Changeset 3007 for src/common


Ignore:
Timestamp:
Mar 28, 2013, 2:59:43 PM (7 years ago)
Author:
campbell
Message:

Sketch out how Cminor to RTLabs correctness would fit into the
front-end measurable traces proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2990 r3007  
    2222   Note: as we're interested in measurable subtraces, we don't have to worry
    2323   about the execution "going wrong."
     24   
     25   For call and return states we only allow the addition of extra steps *after*
     26   the corresponding call or return state (i.e., the simulation must always
     27   start with it).  This is true in the front-end: Callstate and Returnstate
     28   are the second half of calls and returns, the first is the instruction for
     29   the call or return which is translated as a "normal" step, where any extra
     30   instructions for before the action are added.
    2431    *)
    2532
     
    2936  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
    3037  ms_inv : ? → ? → Type[0];
    31   ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    3238  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
    3339  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2;
     
    192198      ms_rel MS g g' INV sr sr'.
    193199
    194 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
     200* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
    195201#g #g' #INV #s1 #s1' #REL
    196202#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     
    447453       measurable trace, so the end is no longer in the relation. ☹ *)
    448454   
    449 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
     455* #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init
    450456#g #g' #INV #s1 #s1' #depth #callstack #REL
    451457#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
Note: See TracChangeset for help on using the changeset viewer.