Changeset 2669 for src


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

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

Location:
src/common
Files:
3 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 :
  • src/common/Measurable.ma

    r2668 r2669  
    2222 *)
    2323
    24 definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝
    25 λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
     24definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
     25λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    2626
    2727definition measure_stack_aux ≝
    28 λC. (λx. λtrs:trace × (cs_state … C).
     28λC. (λx. λstr:cs_state … C × trace.
    2929    let 〈current,max_stack〉 ≝ x in
    30     let 〈tr,s〉 ≝ trs in
     30    let 〈s,tr〉 ≝ str in
    3131    let new ≝
    3232      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
     
    3737    〈new, max max_stack new〉).
    3838
    39 definition measure_stack : ∀C. nat → execution_prefix (cs_state … C) → nat × nat ≝
     39definition measure_stack : ∀C. nat → list (cs_state … C × trace) → nat × nat ≝
    4040λC,current.
    4141  foldl … (measure_stack_aux C) 〈current,0〉.
    4242
    43 definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝
     43definition stack_after : ∀C. nat → list (cs_state … C × trace) → nat ≝
    4444λC,current,x. \fst (measure_stack C current x).
    4545
    46 definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → nat ≝
     46definition max_stack : ∀C. nat → list (cs_state … C × trace) → nat ≝
    4747λC,current,x. \snd (measure_stack C current x).
    4848
     
    5757
    5858lemma max_stack_step : ∀C,a,m,a',m',tr,s.
    59   measure_stack_aux C 〈a,m〉 〈tr,s〉 = 〈a',m'〉 →
     59  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
    6060  m' = max m a'.
    6161#C #a #m #a' #m' #tr #s
     
    6565qed.
    6666
    67 lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',trs.
    68   measure_stack_aux C 〈a,m1〉 trs = 〈a1',m1'〉 →
    69   measure_stack_aux C 〈a,m2〉 trs = 〈a2',m2'〉 →
     67lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
     68  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
     69  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
    7070  a1' = a2'.
    71 #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #tr #s
     71#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
    7272whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
    7373generalize in match (cs_stack C s); cases (cs_classify C s) #f
     
    224224
    225225let rec will_return_aux C (depth:nat)
    226                         (trace:execution_prefix (cs_state … C)) on trace : bool ≝
     226                        (trace:list (cs_state … C × trace)) on trace : bool ≝
    227227match trace with
    228228[ nil ⇒ false
    229229| cons h tl ⇒
    230   let 〈tr,s〉 ≝ h in
     230  let 〈s,tr〉 ≝ h in
    231231  match cs_classify C s with
    232232  [ cl_call ⇒ will_return_aux C (S depth) tl
    233233  | cl_return ⇒
    234234      match depth with
    235        (* We need to see the state after the return to build the structured
    236           trace. *)
    237       [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
     235       (* The state after the return will appear in the structured trace, but
     236          not here because it is the second part of the pair returned by
     237          exec_steps. *)
     238      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
    238239      | S d ⇒ will_return_aux C d tl
    239240      ]
     
    241242  ]
    242243].
    243 definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
     244definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
    244245
    245246(* Like classified_system, but we don't fix the global environment so that we
  • src/common/SmallstepExec.ma

    r2668 r2669  
    383383(* For now I'm doing this without I/O, to keep things simple.  In the place I
    384384   intend to use it (the definition of measurable subtraces, and proofs using
    385    that) I should allow I/O for the prefix. *)
    386 
    387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝
     385   that) I should allow I/O for the prefix.
     386   
     387   If the execution has the form
     388   
     389     s1 -tr1→ s2 -tr2→ … sn -trn→ s'
     390   
     391   then the function returns
     392   
     393     〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉
     394   *)
     395
     396let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝
    388397match n with
    389398[ O ⇒ return 〈[ ], s〉
     
    395404    [ Value trs ⇒
    396405        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
    397         return 〈trs::tl, s'〉
     406        return 〈〈s, \fst trs〉::tl, s'〉
    398407    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
    399408    | Wrong m ⇒ Error … m
     
    408417  is_final … fx g s = None ? ∧
    409418  ∃tr',s',tl.
    410     trace = 〈tr',s'〉::tl ∧
     419    trace = 〈s,tr'〉::tl ∧
    411420    step … fx g s = Value … 〈tr',s'〉 ∧
    412421    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
     
    454463qed.
    455464
    456 let rec gather_trace S (l:list (trace × S)) on l : trace ≝
     465let rec gather_trace S (l:list (S × trace)) on l : trace ≝
    457466match l with
    458467[ nil ⇒ E0
    459 | cons h t ⇒ (\fst h)⧺(gather_trace S t)
     468| cons h t ⇒ (\snd h)⧺(gather_trace S t)
    460469].
    461470
     
    474483lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
    475484  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
    476   all … (λts. inv (\snd ts)) trace →
     485  all ? (λstr. inv (\fst str)) (tail … trace) →
     486  inv s' →
    477487  P (gather_trace ? trace) s' →
    478488  after_n_steps n O I fx g s inv P.
    479489#n elim n
    480490[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
    481   #ALL #p whd @p
     491  #ALL #FI #p whd @p
    482492| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
    483493  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
    484494  destruct
    485   #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl))
    486   [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl
    487   #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
     495  #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
     496  [ cases m in STEPS;
     497    [ whd in ⊢ (??%? → ?); #E destruct /2/
     498    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
     499      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/
     500    ]
     501  ] * #i1 #itl
     502  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??))
    488503  [ @p
     504  | @FALL
    489505  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
    490506  ]
     
    497513#n #O #I #fx #g #s #trace #s' #P #EXEC #p
    498514@(exec_steps_after_n … EXEC) //
    499 elim trace /2/
     515cases trace // #x #trace'
     516elim trace' /2/
    500517qed.
    501518
     
    510527  cases (IH … AFTER')
    511528  #tl * #s' * #STEPS #p
    512   %{(〈tr1,s1〉::tl)} %{s'} %
     529  %{(〈s,tr1〉::tl)} %{s'} %
    513530  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
    514531] qed.
     
    526543  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
    527544  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
    528   %{(〈tr',s'〉::trace1)} %{trace2} %{s1}
     545  %{(〈s,tr'〉::trace1)} %{trace2} %{s1}
    529546  %
    530547  [ %
     
    549566] qed.
    550567
    551 (* Show that it corresponds to split_trace … (exec_inf …) *)
     568lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
     569  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
     570  s = s1.
     571#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
     572lapply (exec_steps_length … EXEC) #E normalize in E; destruct
     573cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
     574%
     575qed.
     576
     577(* Show that it corresponds to split_trace … (exec_inf …).
     578   We need to adjust the form of trace. *)
     579
     580let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝
     581match l with
     582[ nil ⇒ [〈tr,s'〉]
     583| cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s')
     584].
     585
     586definition switch_trace ≝
     587λS,l,s'. match l with
     588[ nil ⇒ nil ?
     589| cons h t ⇒ switch_trace_aux S (\snd h) t s'
     590].
    552591
    553592lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
    554593  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
    555594  match is_final … s' with
    556   [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉
    557   | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉
     595  [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉
     596  | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉
    558597  ].
    559598#O #I #fx #g #n elim n
     
    570609    >exec_inf_aux_unfold normalize nodelta
    571610    cases (is_final … s')
    572     [ %
     611    [ whd %
    573612    | #r %2 %{tr''} %
    574613    ]
    575   | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps
     614  | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps
    576615    lapply (IH … Esteps) cases (is_final … s')
    577     [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
    578       >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
     616    [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps)
     617      >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     618      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta %
    579619    | normalize nodelta #r *
    580620      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
    581       | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     621      | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps)
     622        >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
    582623        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
    583624      ]
Note: See TracChangeset for help on using the changeset viewer.