Changeset 2678 for src/common


Ignore:
Timestamp:
Feb 19, 2013, 12:23:52 PM (7 years ago)
Author:
campbell
Message:

Switch to single source step simulations for front-end measurable subtraces
results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2670 r2678  
    3434  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
    3535
     36  (* Measure on source states; only needed for showing preservation of
     37     non-termination.  Should not be necessary for showing that the measurable
     38     traces are preserved. *)
     39  ms_measure1 : ∀g1. state … ms_C1 g1 → nat;
     40
    3641  sim_normal :
    3742    ∀g1,g2.
     
    4146    normal_state ms_C1 g1 s1 →
    4247    ¬ pcs_labelled ms_C1 g1 s1 →
    43     ∃n,s2,tr. after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
     48    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    4449    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
    4550      tr = tr' ∧
    46       ms_rel g1 g2 INV s2 s2'
     51      ms_rel g1 g2 INV s2 s2' ∧
     52      (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))
    4753    );
    4854  sim_call_return :
     
    5359    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
    5460    ¬ pcs_labelled ms_C1 g1 s1 →
    55     ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
     61    ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 →
    5662    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
    5763      tr = tr' ∧
     
    6470    ms_rel g1 g2 INV s1 s1' →
    6571    pcs_labelled ms_C1 g1 s1 →
    66     after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉)
     72    step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉
    6773    after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'.
    6874      tr = tr' ∧
     
    179185 
    180186    ms_rel MS g g' INV sf sf'.
    181 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #labelled_normal1 #labelled_normal2 #no_tailcalls #sim_normal #sim_call_return #sim_cost #sim_init
     187* #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init
    182188#g #g' #INV #max #s1 #s1' #REL
    183189#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
    184190generalize in match 0; (* current stack level *)
    185 @(nat_elim1 m0)
    186 *
    187 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
     191elim m0
     192[ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
    188193  #max_ok %{0} %{[]} %{s1'}
    189194  % [ % // | // ]
    190195| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK
     196  cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2
    191197  cases (true_or_false_Prop … (pcs_labelled … s1))
    192198  [ #CS
    193     cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
    194     lapply (sim_cost … s2 ? REL CS ?)
    195     [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
    196     #AFTER'
    197     cases (after_n_exec_steps … AFTER')
     199    lapply (sim_cost … REL CS STEP1)
     200    #AFTER1'
     201    cases (after_n_exec_steps … AFTER1')
    198202    #prefix' * #s2' * #EXEC1' * #Etrace #R2
    199203    cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1
    200204    cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1'
    201     cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    202     [ 2: // | 3: @(transitive_le … MAX_OK) >E1 <max_stack_append
     205    cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     206    [ 2: @(transitive_le … MAX_OK) >E1 cases daemon (* <max_stack_append
    203207      >(stack_normal_step … EXEC1 N1)
    204208      >(stack_normal_step … EXEC1' N1')
    205       @max_r //
     209      @max_r //*)
    206210    ]
    207211    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     
    210214      | <max_stack_append @to_max
    211215        [ >(max_stack_normal_step … EXEC1' N1')
    212           lapply MAX_OK >E1 <max_stack_append
     216          lapply MAX_OK >E1 cases daemon (* <max_stack_append
    213217          >(max_stack_normal_step … EXEC1 N1)
    214           #H /2 by le_maxl/
     218          #H /2 by le_maxl/*)
    215219        | @MAX'' ] ]
    216220      | @R''
     
    221225    [ #NORMAL
    222226      (* XXX should set things up so that notb_Prop isn't needed *)
    223       cases (sim_normal … REL NORMAL (notb_Prop … NCS))
    224       #n * #s2x * #tr * #AFTER * #n' #AFTER'
    225       cases (exec_split … EXEC (notb_Prop … NCS) CSf … AFTER)
    226       [ 2: #s #H cases (andb_Prop_true … H) // ]
    227       #p * #trace1 * #s2 * #trace2 * * * #EXEC1 #E2 #EXEC2 #Esplit destruct
    228       cases (after_n_exec_steps … AFTER') #prefix' * #s2' * #EXEC1' * #Etrace #R2
    229       cases (IH p ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    230       [ 2: /2/ | 3: cases daemon ] (* XXX *)
     227      cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1)
     228      #n' #AFTER1'
     229      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * * #Etrace #R2 #_ (* measure *)
     230      cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     231      [ 2: cases daemon ] (* XXX *)
    231232      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
    232233      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
     
    241242        ]
    242243    | #CALLRET
    243       cases (sim_call_return … REL … (notb_Prop … NCS))
     244      cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1)
    244245      [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;
    245246        lapply (no_tailcalls … s1)
     
    247248        normalize * #H #H' try % try cases (H I)
    248249        cases H' /2/ ]
    249       #s2 * #tr2 * #AFTER1 * #m' #AFTER1'
    250       cases (exec_split1 … EXEC … AFTER1)
    251       #trace1 * #s2x * #trace2 * * #EXEC1 #E2 #EXEC2 destruct
     250      #m' #AFTER1'
    252251      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2
    253       cases (IH ?? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
    254       [ 2: /2/ | 3: cases daemon ] (* XXX *)
     252      cases (IH (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     253      [ 2: cases daemon ] (* XXX *)
    255254      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
    256255      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
Note: See TracChangeset for help on using the changeset viewer.