Changeset 3063


Ignore:
Timestamp:
Apr 2, 2013, 12:16:41 PM (4 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.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCastsMeasurable.ma

    r3053 r3063  
    5151  ?
    5252  ?
    53   (λ_,_. 0)
    5453  ?
    5554  ?
     
    8988  whd in match (is_final … s1'); >(step_not_final … ST')
    9089  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    91   whd % [ % [ % | assumption ] | #E destruct ]
     90  whd % [ % | assumption ]
    9291| (* sim_call_nolabel *)
    9392  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2
  • src/Clight/toCminorMeasurable.ma

    r3055 r3063  
    4444  ?
    4545  ?
    46   (λ_,_.0) (*FIXME measure_Clight*)
    4746  ?
    4847  ?
     
    8887  #m #AF %{m} @(after_n_covariant … AF)
    8988  #tr' #s' * * #TR #R #M % /2/
    90   (* HWM <--- *)
    9189| (* sim_call_nolabel *)
     90  cases daemon (*
    9291  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST #NCS2
    9392  cases (cast_correction … RG … S1 ST)
     
    9594  whd in match (is_final … s1'); >(step_not_final … ST')
    9695  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    97   whd % [ % | assumption ]
     96  whd % [ % | assumption ]*)
    9897| (* sim_call_label *)
     98  cases daemon (*
    9999  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #ST1 #CS2 #ST2
    100100  cases (cast_correction … RG … S1 ST1)
     
    108108  whd whd in match (is_final … s2'); >(step_not_final … ST2')
    109109  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
    110   whd % [ % | assumption ]
     110  whd % [ % | assumption ]*)
    111111| (* sim_return *)
     112  cases daemon (*
    112113  #ge #ge' #RG #s1 #s1' #S1 #CL1 #NCS1 #s2 #tr #ST
    113114  cases (cast_correction … RG … S1 ST)
     
    116117  whd in match (is_final … s1'); >(step_not_final … ST')
    117118  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    118   whd % [ >(return_E0 … ST) // assumption | assumption ]
     119  whd % [ >(return_E0 … ST) // assumption | assumption ]*)
    119120| (* sim_cost *)
     121  cases daemon (*
    120122  #ge #ge' #RG #s1 #s1' #s2 #tr #S1 #CS1 #ST
    121123  cases (cast_correction … RG … S1 ST)
     
    123125  whd in match (is_final … s1'); >(step_not_final … ST')
    124126  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    125   whd % [ % | assumption ]
     127  whd % [ % | assumption ]*)
    126128| (* sim_init *)
    127129  #p1 #p2 #s #COMPILE #INIT
    128   cases (initial_state_casts … INIT)
    129   #s' * * >COMPILE #INIT' #RG #S
    130   %{s'} % [ @INIT' | %{RG} assumption ]
     130  cases (init_clight_cminor … INIT COMPILE)
     131  #INV * #s' * #INIT' #S
     132  %{s'} % [ @INIT' | %{INV} assumption ]
    131133] qed.
  • src/Cminor/toRTLabsCorrectness.ma

    r3007 r3063  
    138138  ? (* labelled_normal_2 *)
    139139  ? (* notailcalls *)
    140   (λ_.cminor_measure)
    141140  ? (* sim_normal *)
    142141  ? (* sim_call_nolabel *)
  • 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.