Changeset 3046

Timestamp:

Mar 30, 2013, 1:11:01 AM (8 years ago)

Author:

campbell

Message:

Main part of combined switch removal and labelling proof.

Location:

src/Clight

Files:

• SwitchAndLabel.ma (modified) (3 diffs)
• switchRemoval.ma (modified) (3 diffs)

src/Clight/SwitchAndLabel.ma

@@ -89 +89 @@
 ] qed.
 
+lemma interactive_switch_step : ∀ge,ge'.
+  switch_removal_globals ? fundef_switch_removal ge ge' →
+  ∀s1,s1',o,k.
+  exec_step ge s1 = Interact … o k →
+  switch_state_sim ge s1 s1' →
+  ∃k'.
+      exec_step ge' s1' = Interact … o k' ∧
+  ∀i. ∃tr,s2.
+    k i = Value … 〈tr,s2〉 ∧
+    ∃s2'.
+      k' i = Value … 〈tr,s2'〉 ∧
+      switch_state_sim ge s2 s2'.
+#ge #ge' #RG #s1 #s1' #o #k #EX
+cases (exec_step_interaction … EX)
+#vf * #fn * #argtys * #retty * #vargs * #k' * #m #E
+destruct
+#S inversion S
+[1,3,4: #H1 #H2 #H3 #H4 destruct
+  #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
+  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 destruct
+]
+#s_vf #s_fd #s_args #s_k #s_k_ext #s_m #s_m_ext #s_writeable #s_me #s_H
+#E1 #E2 #E3 destruct
+whd in EX:(??%?);
+@(bindIO_res_interact ?????????? EX) -EX
+#vs #CHECK #EX whd in EX:(??%?); destruct
+% [2: %
+[ whd in ⊢ (??%?);
+  >CHECK in ⊢ (??%?);
+  whd in ⊢ (??%?);
+  @refl
+| #i
+  % [2: % [2: %
+  [ @refl
+  | % [2: %
+    [ @refl
+    | @(sws_returnstate … s_me) // ]
+    | skip ] ] | skip ]
+  ] ]| skip
+] qed.
+
+lemma Value_eq_l : ∀tr,s,tr',s'.
+  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
+  tr = tr'.
+#tr #s #tr' #s' #E destruct %
+qed.
+
+lemma Value_eq_r : ∀tr,s,tr',s'.
+  Value io_out io_in (trace×state) 〈tr,s〉 = Value io_out io_in (trace×state) 〈tr',s'〉 →
+  s = s'.
+#tr #s #tr' #s' #E destruct %
+qed.
 
 let corec build_exec
@@ -121 +173 @@
   cases (switch_removal_correction … SRG … S1 EX1)
   #n1 #A1
-  cases (after_n_result … A1) #tr1' * #s2' * * #E destruct (E) #S1' #A1'
+  cases (after_n_result … A1) #tr1' * #s2' * * #E @(match E with [refl ⇒ ?]) #S1' #A1'
   cases (steps_with_labels … RG … S2 A1')
   #n #AF cases (after_inv clight_fullexec ????? AF) #tr' * #s' * * #TWL #S'
@@ -130 +182 @@
     @(build_exec … SRG RG … S1' S') >E1' in NW1; //
   | #r <(final_related … S') <(switch_final_related … S1') change with (is_final … clight_fullexec ge1 s1') in ⊢ (??%? → ?);
-    >(exec_e_step_not_final ?? clight_fullexec … E1) #E destruct
+    >(exec_e_step_not_final ?? clight_fullexec … E1) #E' destruct
   ]
 | #E1 
   cases (extract_interact ?? clight_fullexec … E1)
   #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
-  cases (interactive_step_with_labels … RG … EX1 S)
-  #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 ⊢ (??%);
+  cases (interactive_switch_step … SRG … EX1 S1) #k2' * #EX2 #H2
+  cases (interactive_step_with_labels … RG … EX2 S2)
+  #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 ⊢ (??%);
   @swl_interact
-  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
+  #i cases (H3 i) #tr2 * #s2' * #K2 * #tr3 * #s3' * * #K3 #TR2 #S2'
+  cases (H2 i) #tr1 * #s1' * #K1 * #s2x' * @(match sym_eq … K2 with [refl ⇒ ?]) #Ex
+  @(match (Value_eq_r … Ex) with [refl ⇒ ?]) #S1'
   lapply (NWk i)
-  @(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 ⇒ ?])
-  @(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 ?????);
-  cases (is_final s2')
-  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
-    inversion NW'
-    [ #H1 #H2 #H3 #H4 #H5 destruct
-    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
-    | #H14 #H15 #H16 #H17 #H18 destruct
+  @(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 … (switch_final_related … S1') with [refl ⇒ ?]) @(match sym_eq … (final_related … S2') with [refl ⇒ ?])
+  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge3 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%);
+  @(match sym_eq … K3 with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
+  cases (is_final s3')
+  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …))
+    [ destruct //
+    | @build_exec //
+      inversion NW'
+      [ #H1 #H2 #H3 #H4 #H5 destruct
+      | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
+      | #H14 #H15 #H16 #H17 #H18 destruct
+      ]
     ]
-  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
+  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) destruct //
   ]
 ] qed.

src/Clight/switchRemoval.ma

@@ -2000 +2000 @@
  ∀ssc_writeable.
  ∀ssc_mem_hyp : sr_memext ssc_m ssc_m_ext ssc_writeable.
- (match ssc_fd with
+ switch_cont_sim (match ssc_fd with
   [ CL_Internal ssc_f ⇒
-    switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
-  | _ ⇒ True ]) →
+    (\snd (function_switch_removal ssc_f))
+  | _ ⇒ [ ] ]) ssc_k ssc_k_ext →
     switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
                         (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
@@ -2921 +2921 @@
        [ 1: whd in ⊢ ((??%%) → (??%%)); #Heq whd destruct (Heq) @conj try @refl
             %2{sss_writeable … sss_mem_hyp}
-            cases called_fundef
-            [ 2: #id #tl #ty @I
-            | 1: #called_function whd
-                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
-                 [ 1: <sss_func_hyp @refl ] #H >H -H
-                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
-                 [ 1: <sss_func_hyp @refl ] #H >H -H
-                 @(swc_call … sss_k_hyp) try assumption
-                 <sss_func_hyp @refl ]
+            cut (sss_func_tr = \fst (function_switch_removal sss_func))
+            [ 1: <sss_func_hyp @refl ] #H >H -H
+            cut (sss_new_vars = \snd (function_switch_removal sss_func))
+            [ 1: <sss_func_hyp @refl ] #H >H -H
+            @(swc_call … sss_k_hyp) try assumption
+            <sss_func_hyp @refl
        | 2: #ret_expr #Hexec_ret_expr
             cases (bindIO_inversion ??????? Hexec_ret_expr) #xret * #Heq_ret
@@ -2938 +2935 @@
             [ 1: <sss_func_hyp @refl ] #H >H -H
             @(sws_callstate … sss_writeable … sss_mem_hyp)
-            cases called_fundef
-            [ 2: #id #tl #ty @I
-            | 1: #called_function whd
-                 cut (sss_func_tr = \fst (function_switch_removal sss_func))
-                 [ 1: <sss_func_hyp @refl ] #H >H -H
-                 cut (sss_new_vars = \snd (function_switch_removal sss_func))
-                 [ 1: <sss_func_hyp @refl ] #H >H -H
-                 @(swc_call … sss_k_hyp) try assumption
-                 <sss_func_hyp @refl ] ]
+            cut (sss_func_tr = \fst (function_switch_removal sss_func))
+            [ 1: <sss_func_hyp @refl ] #H >H -H
+            cut (sss_new_vars = \snd (function_switch_removal sss_func))
+            [ 1: <sss_func_hyp @refl ] #H >H -H
+            @(swc_call … sss_k_hyp) try assumption
+            <sss_func_hyp @refl ]
   | 4: (* Sequence statement *)
        #Hexec %{0} whd in sss_result_hyp:(??%?); whd whd in Hexec:(??%?) ⊢ (??%?); destruct (Hexec)