Changeset 3063 for src/common


Ignore:
Timestamp:
Apr 2, 2013, 12:16:41 PM (7 years ago)
Author:
campbell
Message:

Remove measure function from FEMeasurable because we're not using it and
it would need to be generalised for clight to cminor. Sketch out rest
of clight to cminor meas_sim record.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r3032 r3063  
    5656  (* Measure on source states; only needed for showing preservation of
    5757     non-termination.  Should not be necessary for showing that the measurable
    58      traces are preserved. *)
     58     traces are preserved.
     59     
     60     Commented out because we're not using it for now.
    5961  ms_measure1 : ∀g1. state … ms_C1 g1 → nat;
     62  *)
    6063
    6164  sim_normal :
     
    6972    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'.
    7073      tr = tr' ∧
    71       ms_rel g1 g2 INV s2 s2'
    72       (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
     74      ms_rel g1 g2 INV s2 s2' (*
     75      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))*)
    7376    );
    7477  (* Naughty code without a cost label will end up being rejected, but we don't
     
    201204      ms_rel MS g g' INV sr sr'.
    202205
    203 * #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
     206* #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
    204207#g #g' #INV #s1 #s1' #REL
    205208#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     
    237240      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
    238241      #n' #AFTER1'
    239       cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
     242      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2
    240243      cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ]
    241244      #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R''
     
    456459       measurable trace, so the end is no longer in the relation. ☹ *)
    457460   
    458 * #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
     461* #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
    459462#g #g' #INV #s1 #s1' #depth #callstack #REL
    460463#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     
    507510      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
    508511      #n' #AFTER1'
    509       cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *)
     512      cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2
    510513      cases (IH m ? depth current_stack … R2 … EXEC2 ??)
    511514      [ 2: //
Note: See TracChangeset for help on using the changeset viewer.