Changeset 2863
 Timestamp:
 Mar 13, 2013, 2:22:29 PM (6 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2855 r2863 184 184 include "joint/semantics_blocks.ma". 185 185 include "ASM/Util.ma". 186 include "joint/StatusSimulationHelper.ma".187 186 188 187 lemma eval_cond_ok : … … 210 209 bool_to_Prop (taaf_non_empty … taf). 211 210 #fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a 212 #ltrue #lfalse #Rst1st2 #EQfetch #EQeval 213 @(general_eval_cond_ok … good … Rst1st2 … EQfetch EQeval) 214 whd #lbl whd #mid1 normalize nodelta 215 letin LTL_prog_params ≝ (mk_prog_params LTL_semantics ??) 216 217 218 whd in match eval_state; normalize nodelta 211 #ltrue #lfalse #Rst1st2 #EQfetch 212 whd in match eval_state; normalize nodelta 219 213 >EQfetch >m_return_bind 220 214 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 
src/joint/Joint.ma
r2843 r2863 520 520 521 521 include alias "basics/logic.ma". 522 522 check stmt_at 523 523 record good_if 524 524 (p : params) (globals : list ident) (def : joint_internal_function p globals) … … 539 539 ; regs_are_in_univers : 540 540 regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def) 541 ; entry_is_cost : 542 ∃nxt,c. 543 stmt_at p globals (joint_if_code … def) (joint_if_entry … def) = 544 Some ? (sequential p ? (COST_LABEL ?? c) nxt) 541 545 }. 542 546 
src/joint/StatusSimulationHelper.ma
r2855 r2863 46 46 qed. 47 47 48 check joint_classify 49 check as_label 50 51 record good_state_relation (P_in : sem_graph_params) 52 (P_out : sem_graph_params) (prog : joint_program P_in) 53 (stack_sizes : ident → option ℕ) 54 (init : ∀globals.joint_closed_internal_function P_in globals 55 →bound_b_graph_translate_data P_in P_out globals) 56 (R : joint_abstract_status (mk_prog_params P_in prog stack_sizes) → 57 joint_abstract_status (mk_prog_params P_out 58 (b_graph_transform_program P_in P_out init prog) 59 stack_sizes) 60 → Prop) : Prop ≝ 61 { pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → pc … st1 = pc … st2 62 ; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes). 63 ∀st2 : joint_abstract_status ?. 64 ∀f,fn,stmt. 65 fetch_statement ? (prog_var_names … prog) 66 (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 → 67 R st1 st2 → as_label ? st1 = as_label ? st2 68 ; cond_commutation : 69 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 70 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 71 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 72 ∀f,fn,a,ltrue,lfalse. 73 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 74 st1 = return st1' → 75 let cond ≝ (COND P_in ? a ltrue) in 76 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 77 return 〈f, fn, sequential … cond lfalse〉 → 78 R st1 st2 → 79 ∀t_fn. 80 fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) = 81 return 〈f,t_fn〉 → 82 bind_new_P' ?? 83 (λregs1.λdata.bind_new_P' ?? 84 (λregs2.λblp. 85 ∀mid,nxt1. 86 stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid 87 = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→ 88 ∃st2_pre_mid_no_pc. 89 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) 90 (st_no_pc ? st2) 91 = return st2_pre_mid_no_pc ∧ 92 let st2_pre_mid ≝ mk_state_pc ? st2_pre_mid_no_pc (pc_of_point P_out (pc_block (pc … st2)) mid) 93 (last_pop … st2) in 94 joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 95 ((\snd (\fst blp)) mid) = cl_jump ∧ 96 cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 97 (sequential P_out ? ((\snd (\fst blp)) mid) nxt1) = None ? ∧ 98 (\snd blp) = [ ] ∧ 99 ∃st2_mid . 100 eval_state P_out (prog_var_names … trans_prog) 101 (ev_genv (mk_prog_params P_out trans_prog stack_sizes)) st2_pre_mid = 102 return st2_mid ∧ R st1' st2_mid 103 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 104 ) (init ? fn) 105 }. 106 48 107 49 108 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 51 110 ∀stack_sizes. 52 111 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 53 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 112 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. 54 113 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 55 114 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 56 115 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 116 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 117 good_state_relation P_in P_out prog stack_sizes init R → 57 118 ∀st1,st1' : joint_abstract_status prog_pars_in. 58 119 ∀st2 : joint_abstract_status prog_pars_out. 59 ∀f,fn,a,ltrue,lfalse. 60 ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. 120 ∀f. 121 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog). 122 ∀a,ltrue,lfalse. 61 123 R st1 st2 → 62 let step ≝ (COND P_in ? a ltrue) in 63 bind_new_P' ?? 64 (λregs1.λdata.∀lbl.bind_new_P' ?? 65 (λregs2.λblp. 66 (∀mid1.∃st2'. 67 repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2) 68 = return (st_no_pc … st2') ∧ 69 pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧ 70 last_pop … st2' = last_pop … st2) 71 ) (f_step ??? data lbl step) 72 ) (init ? fn) → 124 let cond ≝ (COND P_in ? a ltrue) in 73 125 fetch_statement P_in … 74 (globalenv_noinit ? prog) (pc … st1) = 75 return 〈f, fn, sequential … steplfalse〉 →126 (globalenv_noinit ? prog) (pc … st1) = 127 return 〈f, fn, sequential … cond lfalse〉 → 76 128 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 77 129 st1 = return st1' → … … 80 132 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 81 133 bool_to_Prop (taaf_non_empty … taf). 82 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2 83 #f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta 84 >EQfetch >m_return_bind 85 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 86 whd in match eval_statement_advance; normalize nodelta 87 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H 88 #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) H * #EQbool normalize nodelta 89 lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 90 [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind 91  whd in match next; normalize nodelta 92 ] 93 whd in ⊢ (??%% → ?); #EQ destruct(EQ) #n_cost 134 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' #st2 135 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed 94 136 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 95 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); #Hinit (*cases (f_bl_r ?) normalize nodelta 96 [2,4: #r #tl] whd in ⊢ (%→?); #EQ >EQ init_data 97 >if_merge_right in ⊢ (% → ?); [2,4: %] *) 137 #init_data * #t_fn1 ** >(pc_eq_sigma_commute … goodR … Rst1st2) 138 #EQt_fn1 whd in ⊢ (% → ?); #Hinit 98 139 * #labs * #regs 99 (*[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *]*)100 140 ** #EQlabs #EQf_regs normalize nodelta * ** #blp #blm #bls * 101 whd in ⊢ (% → ?); #EQbl 102 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 103 #seq_pre_l 104 letin trans_prog ≝ (b_graph_transform_program P_in P_out init prog) 105 letin prog_pars_out ≝ (mk_prog_params P_out trans_prog stack_sizes) 106 cases(? : ∃st2'. 107 repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2) 108 = return (st_no_pc … st2') ∧ 109 pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧ 110 last_pop … st2' = last_pop … st2) 111 [2,4: assumption ] 112 #st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid 113 >(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1 114 >(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l 115 whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ 116 >EQ in EQmid ⊢ %; nxt1 #EQmid 141 whd in ⊢ (% → ?); @if_elim 142 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 143 whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 144 * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc; 145 normalize nodelta whd in match (point_of_offset ??); <ABS 146 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) 147 ] 148 #_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 149 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 150 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 151 cases(bind_new_bind_new_instantiates … EQbl 152 (bind_new_bind_new_instantiates … Hinit 153 (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1)) 154 … EQmid) 155 #st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) * 156 #st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 157 %{st2_mid} %{Hst2_mid} 158 >(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l 117 159 lapply(taaf_to_taa ??? 118 (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1 119 seq_pre_l res_st2_pre_mid) ?) 120 [1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta 121 whd in match (as_label ??); whd in match (as_pc_of ??); 122 whd in match fetch_statement; normalize nodelta * #H @H H >EQt_fn1 123 >m_return_bind whd in match point_of_pc; normalize nodelta 124 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta 125 cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ] 126 #taa_pre_mid whd in ⊢ (% → ?); 127 cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid = 128 return st2_cond ) 129 [2,4: cases daemon (*THE EXTENSIONAL PROOF *)] 130 #st2_mid #EQst2_mid 131 cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump) 132 [1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?); 133 * #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 l2 >EQ2 in seq_pre_l EQmid; mid2 #seq_pre_l #EQmid 134 letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)) 135 cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid 136 %{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I} 137 [1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption] 138 cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *) 139 *: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption 160 (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1 161 seq_pre_l EQst_pre_mid_no_pc) ?) 162 [ @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??); 163 whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind 164 whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta 165 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST * 166 #H @H % 167 ] #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I} 168 [ whd <(as_label_ok … goodR … Hst2_mid) [assumption] cases daemon (*TODO: general lemma!*) 169  whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta 170 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta 171 assumption 172  assumption 140 173 ] 141 qed.*) 174 qed. 175
Note: See TracChangeset
for help on using the changeset viewer.