Changeset 2863 for src/joint/StatusSimulationHelper.ma

Timestamp:

Mar 13, 2013, 2:22:29 PM (7 years ago)

Author:

piccolo

Message:

Added new invariant to good_if
Generalized version of cond case for the correctness proof of each translate step

File:

• src/joint/StatusSimulationHelper.ma (modified) (3 diffs)

src/joint/StatusSimulationHelper.ma

@@ -46 +46 @@
 qed. 
 
+check joint_classify
+check as_label
+
+record good_state_relation (P_in : sem_graph_params) 
+   (P_out : sem_graph_params) (prog : joint_program P_in)
+   (stack_sizes : ident → option ℕ)
+   (init : ∀globals.joint_closed_internal_function P_in globals
+         →bound_b_graph_translate_data P_in P_out globals) 
+   (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) → 
+        joint_abstract_status (mk_prog_params P_out 
+                                (b_graph_transform_program P_in P_out init prog) 
+                                stack_sizes) 
+        → Prop) : Prop ≝ 
+{ pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → pc … st1 = pc … st2
+; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
+                ∀st2 : joint_abstract_status ?. 
+                ∀f,fn,stmt. 
+                  fetch_statement ? (prog_var_names … prog)
+                  (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 → 
+                  R st1 st2 → as_label ? st1 = as_label ? st2
+; cond_commutation :
+    let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
+    ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
+    ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
+    ∀f,fn,a,ltrue,lfalse. 
+    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 
+    st1 = return st1' →
+    let cond ≝ (COND P_in ? a ltrue) in
+    fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 
+    return 〈f, fn,  sequential … cond lfalse〉 → 
+    R st1 st2 → 
+    ∀t_fn.
+    fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
+    return 〈f,t_fn〉 → 
+    bind_new_P' ??
+     (λregs1.λdata.bind_new_P' ?? 
+     (λregs2.λblp.
+        ∀mid,nxt1.
+          stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
+          = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→ 
+         ∃st2_pre_mid_no_pc. 
+            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) 
+                                   (st_no_pc ? st2) 
+            = return st2_pre_mid_no_pc ∧
+            let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid)
+                                            (last_pop … st2) in
+            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 
+                                ((\snd (\fst blp)) mid)  = cl_jump ∧
+            cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 
+                               (sequential P_out ? ((\snd (\fst blp)) mid) nxt1) = None ? ∧
+            (\snd blp) = [ ] ∧
+            ∃st2_mid .
+                eval_state P_out (prog_var_names … trans_prog) 
+                (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid =
+                return st2_mid ∧ R st1' st2_mid
+   )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
+  ) (init ? fn)
+}.
+
 
 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
@@ -51 +110 @@
 ∀stack_sizes.
 ∀ f_lbls,f_regs.∀f_bl_r.∀init.
-∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 
+∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
 let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
+∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
+good_state_relation P_in P_out prog stack_sizes init R → 
 ∀st1,st1' : joint_abstract_status prog_pars_in.
 ∀st2 : joint_abstract_status prog_pars_out.
-∀f,fn,a,ltrue,lfalse.
-∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
+∀f.
+∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
+∀a,ltrue,lfalse.
 R st1 st2 → 
-let step ≝ (COND P_in ? a ltrue) in
-bind_new_P' ??
- (λregs1.λdata.∀lbl.bind_new_P' ?? 
-  (λregs2.λblp.
-   (∀mid1.∃st2'.
-     repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2) 
-     = return (st_no_pc … st2') ∧
-     pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
-     last_pop … st2' = last_pop … st2)
-   ) (f_step ??? data lbl step)   
-  ) (init ? fn) → 
+    let cond ≝ (COND P_in ? a ltrue) in
  fetch_statement P_in …
-  (globalenv_noinit ? prog) (pc … st1) =
-    return 〈f, fn,  sequential … step lfalse〉 → 
+  (globalenv_noinit ? prog) (pc … st1) = 
+    return 〈f, fn,  sequential … cond lfalse〉 → 
  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 
             st1 = return st1' → 
@@ -80 +132 @@
 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
 bool_to_Prop (taaf_non_empty … taf).
-#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2 
-#f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta 
->EQfetch >m_return_bind
-whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
-whd in match eval_statement_advance; normalize nodelta
-#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
-#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
-lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 
-[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
-| whd in match next; normalize nodelta
-] 
-whd in ⊢ (??%% → ?); #EQ destruct(EQ) #n_cost
+#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2 
+#f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed 
 cases(b_graph_transform_program_fetch_statement … good … EQfetch)
-#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); #Hinit (*cases (f_bl_r ?) normalize nodelta
-[2,4: #r #tl] whd in ⊢ (%→?); #EQ >EQ -init_data 
->if_merge_right in ⊢ (% → ?); [2,4: %] *) 
+#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
+#EQt_fn1 whd in ⊢ (% → ?); #Hinit 
 * #labs * #regs 
-(*[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *]*) 
 ** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls * 
-whd in ⊢ (% → ?); #EQbl
-whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 
-#seq_pre_l
-letin trans_prog  ≝ (b_graph_transform_program P_in P_out init prog)
-letin prog_pars_out ≝ (mk_prog_params P_out trans_prog stack_sizes)
-cases(? : ∃st2'.
-           repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2) 
-           = return (st_no_pc … st2') ∧
-           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
-           last_pop … st2' = last_pop … st2)
-   [2,4: assumption ]
-#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
->(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
->(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
-whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ 
->EQ in EQmid ⊢ %; -nxt1 #EQmid
+whd in ⊢ (% → ?); @if_elim
+[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 
+  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 
+  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc; 
+  normalize nodelta whd in match (point_of_offset ??); <ABS 
+  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
+]
+#_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 
+* #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 
+* #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
+cases(bind_new_bind_new_instantiates … EQbl 
+            (bind_new_bind_new_instantiates … Hinit
+               (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1))
+            … EQmid)    
+#st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) *
+#st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
+%{st2_mid} %{Hst2_mid} 
+>(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l
 lapply(taaf_to_taa ??? 
-           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1 
-                                       seq_pre_l res_st2_pre_mid) ?)
-[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta 
-      whd in match (as_label ??); whd in match (as_pc_of ??); 
-      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
-      >m_return_bind whd in match point_of_pc; normalize nodelta 
-      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta 
-      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
-#taa_pre_mid whd in ⊢ (% → ?);
-cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
-                     return st2_cond )
-[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
-#st2_mid #EQst2_mid 
-cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump) 
-[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
-* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
-letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
-cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
-%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
-[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption] 
-     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
-|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
+           (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
+                                       seq_pre_l EQst_pre_mid_no_pc) ?)
+[ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??);
+  whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind
+  whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta
+  >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST *
+  #H @H %
+] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
+[ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*)
+| whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta
+  >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta
+  assumption
+| assumption
 ]
-qed.*)
+qed.
+