Changeset 3046


Ignore:
Timestamp:
Mar 30, 2013, 1:11:01 AM (4 years ago)
Author:
campbell
Message:

Main part of combined switch removal and labelling proof.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SwitchAndLabel.ma

    r3044 r3046  
    8989] qed.
    9090
     91lemma interactive_switch_step : ∀ge,ge'.
     92  switch_removal_globals ? fundef_switch_removal ge ge' →
     93  ∀s1,s1',o,k.
     94  exec_step ge s1 = Interact … o k →
     95  switch_state_sim ge s1 s1' →
     96  ∃k'.
     97      exec_step ge' s1' = Interact … o k' ∧
     98  ∀i. ∃tr,s2.
     99    k i = Value … 〈tr,s2〉 ∧
     100    ∃s2'.
     101      k' i = Value … 〈tr,s2'〉 ∧
     102      switch_state_sim ge s2 s2'.
     103#ge #ge' #RG #s1 #s1' #o #k #EX
     104cases (exec_step_interaction … EX)
     105#vf * #fn * #argtys * #retty * #vargs * #k' * #m #E
     106destruct
     107#S inversion S
     108[1,3,4: #H1 #H2 #H3 #H4 destruct
     109  #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     110  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 destruct
     111]
     112#s_vf #s_fd #s_args #s_k #s_k_ext #s_m #s_m_ext #s_writeable #s_me #s_H
     113#E1 #E2 #E3 destruct
     114whd in EX:(??%?);
     115@(bindIO_res_interact ?????????? EX) -EX
     116#vs #CHECK #EX whd in EX:(??%?); destruct
     117% [2: %
     118[ whd in ⊢ (??%?);
     119  >CHECK in ⊢ (??%?);
     120  whd in ⊢ (??%?);
     121  @refl
     122| #i
     123  % [2: % [2: %
     124  [ @refl
     125  | % [2: %
     126    [ @refl
     127    | @(sws_returnstate … s_me) // ]
     128    | skip ] ] | skip ]
     129  ] ]| skip
     130] qed.
     131
     132lemma Value_eq_l : ∀tr,s,tr',s'.
     133  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
     134  tr = tr'.
     135#tr #s #tr' #s' #E destruct %
     136qed.
     137
     138lemma Value_eq_r : ∀tr,s,tr',s'.
     139  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
     140  s = s'.
     141#tr #s #tr' #s' #E destruct %
     142qed.
    91143
    92144let corec build_exec
     
    121173  cases (switch_removal_correction … SRG … S1 EX1)
    122174  #n1 #A1
    123   cases (after_n_result … A1) #tr1' * #s2' * * #E destruct (E) #S1' #A1'
     175  cases (after_n_result … A1) #tr1' * #s2' * * #E @(match E with [refl ⇒ ?]) #S1' #A1'
    124176  cases (steps_with_labels … RG … S2 A1')
    125177  #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S'
     
    130182    @(build_exec … SRG RG … S1' S') >E1' in NW1; //
    131183  | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
    132     >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct
     184    >(exec_e_step_not_final ?? clight_fullexec … E1) #E' destruct
    133185  ]
    134186| #E1
    135187  cases (extract_interact ?? clight_fullexec … E1)
    136188  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
    137   cases (interactive_step_with_labels … RG … EX1 S)
    138   #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
     189  cases (interactive_switch_step … SRG … EX1 S1) #k2' * #EX2 #H2
     190  cases (interactive_step_with_labels … RG … EX2 S2)
     191  #k3' * #EX3 #H3 @(match sym_eq … EX3 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
    139192  @swl_interact
    140   #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
     193  #i cases (H3 i) #tr2 * #s2' * #K2 * #tr3 * #s3' * * #K3 #TR2 #S2'
     194  cases (H2 i) #tr1 * #s1' * #K1 * #s2x' * @(match sym_eq … K2 with [refl ⇒ ?]) #Ex
     195  @(match (Value_eq_r … Ex) with [refl ⇒ ?]) #S1'
    141196  lapply (NWk i)
    142   @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
    143   @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
    144   cases (is_final s2')
    145   [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
    146     inversion NW'
    147     [ #H1 #H2 #H3 #H4 #H5 destruct
    148     | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
    149     | #H14 #H15 #H16 #H17 #H18 destruct
     197  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????);
     198  @(match sym_eq … (switch_final_related … S1') with [refl ⇒ ?]) @(match sym_eq … (final_related … S2') with [refl ⇒ ?])
     199  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge3 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%);
     200  @(match sym_eq … K3 with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
     201  cases (is_final s3')
     202  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …))
     203    [ destruct //
     204    | @build_exec //
     205      inversion NW'
     206      [ #H1 #H2 #H3 #H4 #H5 destruct
     207      | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
     208      | #H14 #H15 #H16 #H17 #H18 destruct
     209      ]
    150210    ]
    151   | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
     211  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) destruct //
    152212  ]
    153213] qed.
  • src/Clight/switchRemoval.ma

    r3044 r3046  
    20002000 ∀ssc_writeable.
    20012001 ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable.
    2002  (match ssc_fd with
     2002 switch_cont_sim (match ssc_fd with
    20032003  [ CL_Internal ssc_f ⇒
    2004     switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
    2005   | _ ⇒ True ])
     2004    (\snd (function_switch_removal ssc_f))
     2005  | _ ⇒ [ ] ]) ssc_k ssc_k_ext
    20062006    switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
    20072007                        (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
     
    29212921       [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl
    29222922            %2{sss_writeable … sss_mem_hyp}
    2923             cases called_fundef
    2924             [ 2: #id #tl #ty @I
    2925             | 1: #called_function whd
    2926                  cut (sss_func_tr = \fst (function_switch_removal sss_func))
    2927                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2928                  cut (sss_new_vars = \snd (function_switch_removal sss_func))
    2929                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2930                  @(swc_call … sss_k_hyp) try assumption
    2931                  <sss_func_hyp @refl ]
     2923            cut (sss_func_tr = \fst (function_switch_removal sss_func))
     2924            [ 1: <sss_func_hyp @refl ] #H >H -H
     2925            cut (sss_new_vars = \snd (function_switch_removal sss_func))
     2926            [ 1: <sss_func_hyp @refl ] #H >H -H
     2927            @(swc_call … sss_k_hyp) try assumption
     2928            <sss_func_hyp @refl
    29322929       | 2: #ret_expr #Hexec_ret_expr
    29332930            cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret
     
    29382935            [ 1: <sss_func_hyp @refl ] #H >H -H
    29392936            @(sws_callstate … sss_writeable … sss_mem_hyp)
    2940             cases called_fundef
    2941             [ 2: #id #tl #ty @I
    2942             | 1: #called_function whd
    2943                  cut (sss_func_tr = \fst (function_switch_removal sss_func))
    2944                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2945                  cut (sss_new_vars = \snd (function_switch_removal sss_func))
    2946                  [ 1: <sss_func_hyp @refl ] #H >H -H
    2947                  @(swc_call … sss_k_hyp) try assumption
    2948                  <sss_func_hyp @refl ] ]
     2937            cut (sss_func_tr = \fst (function_switch_removal sss_func))
     2938            [ 1: <sss_func_hyp @refl ] #H >H -H
     2939            cut (sss_new_vars = \snd (function_switch_removal sss_func))
     2940            [ 1: <sss_func_hyp @refl ] #H >H -H
     2941            @(swc_call … sss_k_hyp) try assumption
     2942            <sss_func_hyp @refl ]
    29492943  | 4: (* Sequence statement *)
    29502944       #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)
Note: See TracChangeset for help on using the changeset viewer.