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

Main part of combined switch removal and labelling proof.

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.