Ignore:
Timestamp:
Feb 15, 2013, 11:27:58 AM (8 years ago)
Author:
campbell
Message:

Tweak exec_steps output; show that simulations extend to measurable
subtrace prefixes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2668 r2669  
    66λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
    77
     8lemma normal_state_inv : ∀C,g,s.
     9  normal_state C g s →
     10  pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump.
     11#C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ *
     12qed.
     13
    814(* A record giving the languages and simulation results necessary to show that
    9    measurability is preserved. *)
     15   measurability is preserved.
     16   
     17   Note: as we're interested in measurable subtraces, we don't have to worry
     18   about the execution "going wrong."
     19    *)
    1020
    1121record meas_sim : Type[2] ≝ {
     
    1828  ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
    1929  ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2);
     30
     31  (* These hold in (at least) the languages of interest for measurable subtraces *)
     32  ms_labelled_normal_1 : ∀g1,s1. bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C1 g1 s1);
     33  ms_labelled_normal_2 : ∀g2,s2. bool_to_Prop (pcs_labelled ms_C2 g2 s2) ↔ bool_to_Prop (normal_state ms_C2 g2 s2);
     34  ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall;
     35
    2036  sim_normal :
    2137    ∀g1,g2.
    2238    ∀INV:ms_inv g1 g2.
    23     ∀s1,s1',s2,tr.
     39    ∀s1,s1'.
    2440    ms_rel g1 g2 INV s1 s1' →
    2541    normal_state ms_C1 g1 s1 →
    2642    ¬ pcs_labelled ms_C1 g1 s1 →
    27     ∃n. 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〉) →
     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〉) ∧
    2844    ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
    2945      tr = tr' ∧
     
    3349    ∀g1,g2.
    3450    ∀INV:ms_inv g1 g2.
    35     ∀s1,s1',s2,tr.
     51    ∀s1,s1'.
    3652    ms_rel g1 g2 INV s1 s1' →
    3753    match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] →
    3854    ¬ pcs_labelled ms_C1 g1 s1 →
    39     after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →
     55    ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧
    4056    ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'.
    4157      tr = tr' ∧
     
    131147] qed.
    132148
    133 lemma stack_labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     149lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
    134150  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
    135   pcs_labelled C g s1 →
     151  normal_state C g s1 →
    136152  stack_after (pcs_to_cs C g stack) current trace = current.
    137153#C #g #s1 #trace #s2 #stack #current #EXEC
    138154cases (exec_steps_S … EXEC)
    139155#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
    140 #CS
    141 whd in ⊢ (??%?); whd in match (cs_classify ??); >CS
     156#N
     157whd in ⊢ (??%?); generalize in match (cs_stack ??);
     158whd in match (cs_classify ??);
     159cases (normal_state_inv … N)
     160#CL >CL #f %
     161qed.
     162
     163lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     164  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
     165  normal_state C g s1 →
     166  max_stack (pcs_to_cs C g stack) current trace = current.
     167#C #g #s1 #trace #s2 #stack #current #EXEC
     168cases (exec_steps_S … EXEC)
     169#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
     170#N
     171whd in ⊢ (??%?); generalize in match (cs_stack ??);
     172whd in match (cs_classify ??);
     173cases (normal_state_inv … N)
     174#CL >CL #f %
     175qed.
     176
     177lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf.
     178  exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
     179  ¬pcs_labelled C g s1 →
     180  pcs_labelled C g sf →
     181  ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) →
     182  ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P →
     183  ∃p,trace1,s2,trace2.
     184    exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
     185    P (gather_trace … trace1) s2 ∧
     186    exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧
     187    m = n + p.
     188#C #g #m elim m -m
     189[ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct
     190  #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS
     191| #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H *
     192  [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ]
     193  | #n #P #AFTER
     194    cases (exec_steps_S … EXEC1)
     195    #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2
     196    cases (after_1_of_n_steps … AFTER)
     197    #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2
     198    >STEP in STEP'; #E destruct
     199    cases (IH … EXEC2 … AFTER2)
     200    [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E
     201      %{p} % [2: %{s2} %{trace2} % [ % [ %
     202       [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ]
     203      | @P2 ]| @EXEC2 ]| >E % ] | skip ]
     204    | @H assumption
     205    | assumption
     206    | assumption
     207    ]
     208  ]
     209] qed.
     210
     211lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf.
     212  exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 →
     213  ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P →
     214  ∃trace1,s2,trace2.
     215    exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧
     216    P (gather_trace … trace1) s2 ∧
     217    exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉.
     218#C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1
     219cases (exec_steps_S … EXEC1)
     220#NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2
     221%{[〈s1,tr〉]} %{s2} %{tl} % [ %
     222 [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize
     223 cases (inv s2) // * ]| // ]
     224qed.
     225
     226(* XXX do I need to do the max_stack reasoning here?  perhaps just by preserving
     227   observables? *)
    142228
    143229
     
    153239  ∀m,prefix,sf.
    154240  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
     241  pcs_labelled (ms_C1 MS) g sf →
    155242  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
    156243
     
    160247 
    161248    ms_rel MS g g' INV sf sf'.
    162 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #sim_normal #sim_call_return #sim_cost #sim_init
     249* #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
    163250#g #g' #INV #max #s1 #s1' #REL
    164251#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     
    166253@(nat_elim1 m0)
    167254*
    168 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #exec whd in exec:(??%?); destruct
     255[ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf
    169256  #max_ok %{0} %{[]} %{s1'}
    170257  % [ % // | // ]
    171 | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #exec #max_ok
     258| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK
    172259  cases (true_or_false_Prop … (pcs_labelled … s1))
    173260  [ #CS
    174     cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
     261    cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
    175262    lapply (sim_cost … s2 ? REL CS ?)
    176263    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
     
    178265    cases (after_n_exec_steps … AFTER')
    179266    #prefix' * #s2' * #EXEC1' * #Etrace #R2
    180     cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?)
    181     [ 2: // | 3: @(transitive_le … max_ok) >E1 <max_stack_append
    182 
    183      @le_maxr
     267    cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1
     268    cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1'
     269    cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     270    [ 2: // | 3: @(transitive_le … MAX_OK) >E1 <max_stack_append
     271      >(stack_normal_step … EXEC1 N1)
     272      >(stack_normal_step … EXEC1' N1')
     273      @max_r //
     274    ]
    184275    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
    185276    %{(1+m'')} %{(prefix'@prefix'')} %{sf''}
    186     % [ % [ @(exec_steps_join … EXEC1') @EXEC'' | cases daemon ] | @R2
    187   |
    188     %{trace1 }
    189 
    190   cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC'
    191   cases (true_or_false_Prop … (pcs_labelled … s1))
    192   [ #CS lapply (sim_cost … s' tr' REL CS ?)
    193     [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ]
    194     #AFTER %{1}
    195     [ 3: whd in match (after_n_steps ????? s1 ??);
    196       >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
    197 lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?);
    198 [
    199 | #CL
     277    % [ % [ @(exec_steps_join … EXEC1') @EXEC''
     278      | <max_stack_append @to_max
     279        [ >(max_stack_normal_step … EXEC1' N1')
     280          lapply MAX_OK >E1 <max_stack_append
     281          >(max_stack_normal_step … EXEC1 N1)
     282          #H /2 by le_maxl/
     283        | @MAX'' ] ]
     284      | @R''
     285      ]
     286 
     287  | #NCS
     288    cases (true_or_false_Prop (normal_state C1 g s1))
     289    [ #NORMAL
     290      (* XXX should set things up so that notb_Prop isn't needed *)
     291      cases (sim_normal … REL NORMAL (notb_Prop … NCS))
     292      #n * #s2x * #tr * #AFTER * #n' #AFTER'
     293      cases (exec_split … EXEC (notb_Prop … NCS) CSf … AFTER)
     294      [ 2: #s #H cases (andb_Prop_true … H) // ]
     295      #p * #trace1 * #s2 * #trace2 * * * #EXEC1 #E2 #EXEC2 #Esplit destruct
     296      cases (after_n_exec_steps … AFTER') #prefix' * #s2' * #EXEC1' * #Etrace #R2
     297      cases (IH p ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     298      [ 2: /2/ | 3: cases daemon ] (* XXX *)
     299      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     300      %{(n'+m'')} %{(prefix'@prefix'')} %{sf''}
     301      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
     302        | <max_stack_append @to_max
     303          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
     304            lapply MAX_OK >E1 <max_stack_append
     305            >(max_stack_normal_step … EXEC1 N1)
     306            #H /2 by le_maxl/*)
     307          | @MAX'' ] ]
     308        | @R''
     309        ]
     310    | #CALLRET
     311      cases (sim_call_return … REL … (notb_Prop … NCS))
     312      [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET;
     313        lapply (no_tailcalls … s1)
     314        cases (pcs_classify … s1) in CALLRET ⊢ %;
     315        normalize * #H #H' try % try cases (H I)
     316        cases H' /2/ ]
     317      #s2 * #tr2 * #AFTER1 * #m' #AFTER1'
     318      cases (exec_split1 … EXEC … AFTER1)
     319      #trace1 * #s2x * #trace2 * * #EXEC1 #E2 #EXEC2 destruct
     320      cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2
     321      cases (IH ?? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?)
     322      [ 2: /2/ | 3: cases daemon ] (* XXX *)
     323      #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     324      %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''}
     325      % [ % [ @(exec_steps_join … EXEC1') @EXEC''
     326        | <max_stack_append @to_max
     327          [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1')
     328            lapply MAX_OK >E1 <max_stack_append
     329            >(max_stack_normal_step … EXEC1 N1)
     330            #H /2 by le_maxl/*)
     331          | @MAX'' ] ]
     332        | @R''
     333        ]
     334    ]
     335  ]
     336qed.
     337       
     338     
    200339
    201340theorem measured_subtrace_preserved :
Note: See TracChangeset for help on using the changeset viewer.