[2851] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "joint/semanticsUtils.ma". |
---|
| 16 | include "joint/Traces.ma". |
---|
| 17 | include "common/StatusSimulation.ma". |
---|
| 18 | include "joint/semantics_blocks.ma". |
---|
| 19 | |
---|
| 20 | lemma set_no_pc_eta: |
---|
| 21 | ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1. |
---|
| 22 | #P * // |
---|
| 23 | qed. |
---|
| 24 | |
---|
| 25 | lemma pc_of_label_eq : |
---|
| 26 | ∀p,p'.let pars ≝ mk_sem_graph_params p p' in |
---|
| 27 | ∀globals,ge,bl,i_fn,lbl. |
---|
| 28 | fetch_internal_function ? ge bl = return i_fn → |
---|
| 29 | pc_of_label pars globals ge bl lbl = |
---|
| 30 | OK ? (pc_of_point pars bl lbl). |
---|
| 31 | #p #p' #globals #ge #bl #i_fn #lbl #EQf |
---|
| 32 | whd in match pc_of_label; |
---|
| 33 | normalize nodelta >EQf >m_return_bind % |
---|
| 34 | qed. |
---|
| 35 | |
---|
| 36 | |
---|
[2855] | 37 | lemma bind_new_bind_new_instantiates : |
---|
| 38 | ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P. |
---|
| 39 | bind_new_instantiates B X x m l → bind_new_P' ?? P m → |
---|
| 40 | P l x. |
---|
| 41 | #B #X #m elim m normalize nodelta |
---|
| 42 | [#x #y * normalize // #B #l' #P * |
---|
| 43 | | #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H) |
---|
| 44 | @Hr |
---|
| 45 | ] |
---|
[2883] | 46 | qed. |
---|
[2851] | 47 | |
---|
[2898] | 48 | definition joint_state_relation ≝ |
---|
[2939] | 49 | λP_in,P_out.(Σb:block.block_region b=Code) → label → state P_in → state P_out → Prop. |
---|
[2898] | 50 | |
---|
| 51 | definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. |
---|
| 52 | |
---|
| 53 | definition sigma_map ≝ block → label → option label. |
---|
| 54 | definition lbl_funct ≝ block → label → (list label). |
---|
| 55 | definition regs_funct ≝ block → label → (list register). |
---|
| 56 | |
---|
| 57 | definition get_sigma : ∀p : sem_graph_params. |
---|
| 58 | joint_program p → lbl_funct → sigma_map ≝ |
---|
| 59 | λp,prog,f_lbls.λbl,searched. |
---|
| 60 | let globals ≝ prog_var_names … prog in |
---|
| 61 | let ge ≝ globalenv_noinit … prog in |
---|
| 62 | ! bl ← code_block_of_block bl ; |
---|
| 63 | ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl); |
---|
| 64 | !〈res,s〉 ← find ?? (joint_if_code ?? fn) |
---|
| 65 | (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with |
---|
| 66 | [None ⇒ eq_identifier … searched lbl |
---|
| 67 | |Some x ⇒ eq_identifier … searched (\snd x) |
---|
| 68 | ]); |
---|
| 69 | return res. |
---|
| 70 | |
---|
| 71 | definition sigma_pc_opt : ∀p_in,p_out : sem_graph_params. |
---|
| 72 | joint_program p_in → lbl_funct → |
---|
| 73 | program_counter → option program_counter ≝ |
---|
| 74 | λp_in,p_out,prog,f_lbls,pc. |
---|
| 75 | let sigma ≝ get_sigma p_in prog f_lbls in |
---|
| 76 | let ertl_ptr_point ≝ point_of_pc p_out pc in |
---|
| 77 | if eqZb (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *) |
---|
| 78 | return pc |
---|
| 79 | else |
---|
| 80 | ! point ← sigma (pc_block pc) ertl_ptr_point; |
---|
| 81 | return pc_of_point p_in (pc_block pc) point. |
---|
| 82 | |
---|
| 83 | definition sigma_stored_pc ≝ |
---|
| 84 | λp_in,p_out,prog,f_lbls,pc. match sigma_pc_opt p_in p_out prog f_lbls pc with |
---|
| 85 | [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x]. |
---|
| 86 | |
---|
[2863] | 87 | record good_state_relation (P_in : sem_graph_params) |
---|
| 88 | (P_out : sem_graph_params) (prog : joint_program P_in) |
---|
| 89 | (stack_sizes : ident → option ℕ) |
---|
| 90 | (init : ∀globals.joint_closed_internal_function P_in globals |
---|
[2898] | 91 | →bound_b_graph_translate_data P_in P_out globals) |
---|
| 92 | (f_bl_r : block → list register) (f_lbls : lbl_funct) (f_regs : regs_funct) |
---|
| 93 | (good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs) |
---|
| 94 | (st_no_pc_rel : joint_state_relation P_in P_out) |
---|
| 95 | (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝ |
---|
| 96 | { fetch_ok_sigma_state_ok : |
---|
| 97 | ∀st1,st2,f,fn. st_rel st1 st2 → |
---|
| 98 | fetch_internal_function ? (globalenv_noinit … prog) |
---|
| 99 | (pc_block (pc … st1)) = return 〈f,fn〉 → |
---|
[2939] | 100 | st_no_pc_rel (pc_block(pc … st1)) |
---|
| 101 | (point_of_pc P_in (pc … st1)) |
---|
| 102 | (st_no_pc … st1) (st_no_pc … st2) |
---|
[2898] | 103 | ; fetch_ok_pc_ok : |
---|
| 104 | ∀st1,st2,f,fn.st_rel st1 st2 → |
---|
| 105 | fetch_internal_function ? (globalenv_noinit … prog) |
---|
| 106 | (pc_block (pc … st1)) = return 〈f,fn〉 → |
---|
| 107 | pc … st1 = pc … st2 |
---|
| 108 | ; fetch_ok_sigma_last_pop_ok : |
---|
| 109 | ∀st1,st2,f,fn.st_rel st1 st2 → |
---|
| 110 | fetch_internal_function ? (globalenv_noinit … prog) |
---|
| 111 | (pc_block (pc … st1)) = return 〈f,fn〉 → |
---|
| 112 | (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) |
---|
| 113 | ; st_rel_def : |
---|
| 114 | ∀st1,st2,pc,lp1,lp2,f,fn. |
---|
| 115 | fetch_internal_function ? (globalenv_noinit … prog) |
---|
[2939] | 116 | (pc_block pc) = return 〈f,fn〉 → |
---|
| 117 | st_no_pc_rel (pc_block pc) (point_of_pc P_in pc) st1 st2 → |
---|
[2898] | 118 | lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 → |
---|
| 119 | st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) |
---|
[2939] | 120 | ; as_label_ok : |
---|
| 121 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
[2898] | 122 | ∀st1,st2,f,fn,stmt. |
---|
| 123 | fetch_statement ? (prog_var_names … prog) |
---|
| 124 | (globalenv_noinit … prog) (pc … st1) = return〈f,fn,stmt〉 → |
---|
| 125 | st_rel st1 st2 → |
---|
| 126 | as_label (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 = |
---|
| 127 | as_label (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) st2 |
---|
[2863] | 128 | ; cond_commutation : |
---|
| 129 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
| 130 | ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
| 131 | ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
[2883] | 132 | ∀f,fn,a,ltrue,lfalse. |
---|
[2863] | 133 | let cond ≝ (COND P_in ? a ltrue) in |
---|
| 134 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
[2883] | 135 | return 〈f, fn, sequential … cond lfalse〉 → |
---|
| 136 | eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) |
---|
| 137 | st1 = return st1' → |
---|
[2898] | 138 | st_rel st1 st2 → |
---|
[2863] | 139 | ∀t_fn. |
---|
| 140 | fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) = |
---|
| 141 | return 〈f,t_fn〉 → |
---|
| 142 | bind_new_P' ?? |
---|
| 143 | (λregs1.λdata.bind_new_P' ?? |
---|
[2883] | 144 | (λregs2.λblp.(\snd blp) = [ ] ∧ |
---|
| 145 | ∀mid. |
---|
[2863] | 146 | stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid |
---|
[2883] | 147 | = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ |
---|
[2863] | 148 | ∃st2_pre_mid_no_pc. |
---|
| 149 | repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) |
---|
| 150 | (st_no_pc ? st2) |
---|
| 151 | = return st2_pre_mid_no_pc ∧ |
---|
[2940] | 152 | st_no_pc_rel (pc_block(pc … st1')) |
---|
| 153 | (point_of_pc P_in … (pc … st1')) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧ |
---|
[2863] | 154 | joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) |
---|
| 155 | ((\snd (\fst blp)) mid) = cl_jump ∧ |
---|
| 156 | cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) |
---|
[2883] | 157 | (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧ |
---|
[2898] | 158 | let st2_pre_mid ≝ mk_state_pc P_out st2_pre_mid_no_pc |
---|
| 159 | (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in |
---|
| 160 | let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in |
---|
| 161 | eval_statement_advance P_out (prog_var_names … trans_prog) |
---|
| 162 | (ev_genv … (mk_prog_params P_out trans_prog stack_sizes)) f t_fn |
---|
| 163 | (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2' |
---|
[2863] | 164 | ) (f_step … data (point_of_pc P_in (pc … st1)) cond) |
---|
[2898] | 165 | ) (init ? fn) |
---|
[2883] | 166 | ; seq_commutation : |
---|
| 167 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
| 168 | ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . |
---|
| 169 | ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). |
---|
| 170 | ∀f,fn,stmt,nxt. |
---|
| 171 | let seq ≝ (step_seq P_in ? stmt) in |
---|
| 172 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
| 173 | return 〈f, fn, sequential … seq nxt〉 → |
---|
| 174 | eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) |
---|
| 175 | st1 = return st1' → |
---|
[2898] | 176 | st_rel st1 st2 → |
---|
[2883] | 177 | ∀t_fn. |
---|
| 178 | fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) = |
---|
| 179 | return 〈f,t_fn〉 → |
---|
| 180 | bind_new_P' ?? |
---|
| 181 | (λregs1.λdata.bind_new_P' ?? |
---|
[2898] | 182 | (λregs2.λblp. |
---|
[2886] | 183 | ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes) |
---|
| 184 | (globals (mk_prog_params P_out trans_prog stack_sizes))). |
---|
[2891] | 185 | blp = (ensure_step_block ?? l) ∧ |
---|
| 186 | ∃st2_fin_no_pc. |
---|
[2883] | 187 | repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f |
---|
[2891] | 188 | l (st_no_pc … st2)= return st2_fin_no_pc ∧ |
---|
[2940] | 189 | st_no_pc_rel (pc_block (pc … st1')) |
---|
| 190 | (point_of_pc P_in … (pc … st1')) |
---|
[2939] | 191 | (st_no_pc … st1') st2_fin_no_pc |
---|
[2898] | 192 | ) (f_step … data (point_of_pc P_in (pc … st1)) seq) |
---|
| 193 | ) (init ? fn) |
---|
[2863] | 194 | }. |
---|
| 195 | |
---|
[2898] | 196 | lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params. |
---|
| 197 | ∀prog : joint_program P_in. |
---|
| 198 | ∀stack_sizes. |
---|
| 199 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 200 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
| 201 | ∀st_no_pc_rel,st_rel. |
---|
| 202 | ∀f,fn,stmt,st1,st2. |
---|
| 203 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 204 | st_no_pc_rel st_rel → |
---|
| 205 | st_rel st1 st2 → |
---|
| 206 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
| 207 | return 〈f,fn,stmt〉 → |
---|
[2939] | 208 | st_no_pc_rel (pc_block (pc … st1)) (point_of_pc P_in … (pc … st1)) (st_no_pc … st1) (st_no_pc … st2). |
---|
[2898] | 209 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel |
---|
| 210 | #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch |
---|
| 211 | cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt |
---|
| 212 | @(fetch_ok_sigma_state_ok … goodR … EQfn) assumption |
---|
| 213 | qed. |
---|
| 214 | |
---|
| 215 | lemma fetch_stmt_ok_sigma_pc_ok : ∀ P_in , P_out: sem_graph_params. |
---|
| 216 | ∀prog : joint_program P_in. |
---|
| 217 | ∀stack_sizes. |
---|
| 218 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 219 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
| 220 | ∀st_no_pc_rel,st_rel. |
---|
| 221 | ∀f,fn,stmt,st1,st2. |
---|
| 222 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 223 | st_no_pc_rel st_rel → |
---|
| 224 | st_rel st1 st2 → |
---|
| 225 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
| 226 | return 〈f,fn,stmt〉 → |
---|
| 227 | pc … st1 = pc … st2. |
---|
| 228 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel |
---|
| 229 | #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch |
---|
| 230 | cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt |
---|
| 231 | @(fetch_ok_pc_ok … goodR … EQfn) assumption |
---|
| 232 | qed. |
---|
| 233 | |
---|
| 234 | lemma fetch_stmt_ok_sigma_last_pop_ok : ∀ P_in , P_out: sem_graph_params. |
---|
| 235 | ∀prog : joint_program P_in. |
---|
| 236 | ∀stack_sizes. |
---|
| 237 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 238 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
| 239 | ∀st_no_pc_rel,st_rel. |
---|
| 240 | ∀f,fn,stmt,st1,st2. |
---|
| 241 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 242 | st_no_pc_rel st_rel → |
---|
| 243 | st_rel st1 st2 → |
---|
| 244 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
| 245 | return 〈f,fn,stmt〉 → |
---|
| 246 | (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2). |
---|
| 247 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel |
---|
| 248 | #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch |
---|
| 249 | cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt |
---|
| 250 | @(fetch_ok_sigma_last_pop_ok … goodR … EQfn) assumption |
---|
| 251 | qed. |
---|
| 252 | |
---|
| 253 | (* |
---|
| 254 | lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params. |
---|
| 255 | ∀prog : joint_program P_in. |
---|
| 256 | ∀stack_sizes. |
---|
| 257 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 258 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
| 259 | ∀st_no_pc_rel,st_rel. |
---|
| 260 | ∀f,fn,stmt,st1,st2. |
---|
| 261 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 262 | st_no_pc_rel st_rel → |
---|
| 263 | st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) → |
---|
| 264 | (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) → |
---|
| 265 | fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = |
---|
| 266 | return 〈f,fn,stmt〉 → st_rel st1 st2. |
---|
| 267 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel |
---|
| 268 | #st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ) |
---|
| 269 | #EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt |
---|
| 270 | @(st_rel_def … goodR … EQfn) assumption |
---|
| 271 | qed. |
---|
| 272 | *) |
---|
| 273 | |
---|
[2940] | 274 | (* |
---|
[2939] | 275 | (*CSC: Isn't this already proved somewhere else??? *) |
---|
| 276 | lemma point_of_pc_pc_of_point: |
---|
| 277 | ∀P_in: sem_graph_params.∀l,st. |
---|
| 278 | point_of_pc P_in |
---|
| 279 | (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in)) |
---|
| 280 | (pc_block (pc P_in st)) l) = l. |
---|
| 281 | #P * // |
---|
[2940] | 282 | qed.*) |
---|
[2939] | 283 | |
---|
[2855] | 284 | lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. |
---|
[2851] | 285 | ∀prog : joint_program P_in. |
---|
| 286 | ∀stack_sizes. |
---|
| 287 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
[2863] | 288 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
[2898] | 289 | ∀st_no_pc_rel,st_rel. |
---|
[2851] | 290 | let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in |
---|
| 291 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
| 292 | let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in |
---|
[2898] | 293 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 294 | st_no_pc_rel st_rel → |
---|
[2851] | 295 | ∀st1,st1' : joint_abstract_status prog_pars_in. |
---|
| 296 | ∀st2 : joint_abstract_status prog_pars_out. |
---|
[2863] | 297 | ∀f. |
---|
| 298 | ∀fn : joint_closed_internal_function P_in (prog_var_names … prog). |
---|
| 299 | ∀a,ltrue,lfalse. |
---|
[2898] | 300 | st_rel st1 st2 → |
---|
[2940] | 301 | let cond ≝ (COND P_in ? a ltrue) in |
---|
| 302 | fetch_statement P_in … |
---|
| 303 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 304 | return 〈f, fn, sequential … cond lfalse〉 → |
---|
| 305 | eval_state P_in (prog_var_names … ℕ prog) |
---|
| 306 | (ev_genv … prog_pars_in) st1 = return st1' → |
---|
[2851] | 307 | as_costed (joint_abstract_status prog_pars_in) st1' → |
---|
[2898] | 308 | ∃ st2'. st_rel st1' st2' ∧ |
---|
[2851] | 309 | ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. |
---|
| 310 | bool_to_Prop (taaf_non_empty … taf). |
---|
[2898] | 311 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel |
---|
| 312 | #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval |
---|
| 313 | @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 314 | whd in match eval_statement_no_pc; normalize nodelta >m_return_bind |
---|
| 315 | #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv #EQbv |
---|
| 316 | #H @('bind_inversion H) -H * #EQbool normalize nodelta whd in ⊢ (??%% → ?); |
---|
| 317 | cases(fetch_statement_inv … EQfetch) #EQfn #_ |
---|
| 318 | [ >(pc_of_label_eq … EQfn) |
---|
| 319 | normalize nodelta whd in match set_pc; normalize nodelta whd in ⊢ (??%? → ?); |
---|
| 320 | | whd in match next; whd in match set_pc; whd in match set_no_pc; normalize nodelta |
---|
| 321 | ] |
---|
| 322 | #EQ destruct(EQ) #n_costed |
---|
[2851] | 323 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
[2898] | 324 | #init_data * #t_fn1 ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) |
---|
[2863] | 325 | #EQt_fn1 whd in ⊢ (% → ?); #Hinit |
---|
[2898] | 326 | * #labs * #regs ** #EQlabs #EQf_regs normalize nodelta *** #blp #blm #bls * |
---|
[2863] | 327 | whd in ⊢ (% → ?); @if_elim |
---|
[2898] | 328 | [1,3: @eq_identifier_elim [2,4: #_ *] whd in match point_of_pc; normalize nodelta |
---|
[2863] | 329 | whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) |
---|
[2898] | 330 | * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; |
---|
[2863] | 331 | normalize nodelta whd in match (point_of_offset ??); <ABS |
---|
| 332 | cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) |
---|
| 333 | ] |
---|
[2898] | 334 | #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * |
---|
| 335 | #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 |
---|
[2863] | 336 | * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) |
---|
[2883] | 337 | cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit |
---|
| 338 | (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1))) |
---|
| 339 | #EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
[2898] | 340 | cases(APP … EQmid) -APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta |
---|
| 341 | #EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid |
---|
| 342 | [ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue) |
---|
| 343 | (last_pop … st2))} |
---|
| 344 | | %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) lfalse) |
---|
| 345 | (last_pop … st2))} |
---|
| 346 | ] |
---|
| 347 | letin st1' ≝ (mk_state_pc P_in ???) |
---|
| 348 | letin st2' ≝ (mk_state_pc P_out ???) |
---|
| 349 | cut(st_rel st1' st2') |
---|
| 350 | [1,3: @(st_rel_def … goodR … f fn ?) |
---|
| 351 | [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption |
---|
[2940] | 352 | |2,5: assumption |
---|
[2898] | 353 | |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption |
---|
| 354 | ] |
---|
| 355 | ] |
---|
| 356 | #H_fin |
---|
| 357 | % |
---|
| 358 | [1,3: assumption] |
---|
| 359 | >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l |
---|
[2851] | 360 | lapply(taaf_to_taa ??? |
---|
[2863] | 361 | (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1 |
---|
| 362 | seq_pre_l EQst_pre_mid_no_pc) ?) |
---|
[2898] | 363 | [1,3: @if_elim #_ // % whd in ⊢ (% → ?); whd in match (as_label ??); |
---|
| 364 | whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind |
---|
| 365 | whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta |
---|
| 366 | >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >COST * |
---|
| 367 | #H @H % |
---|
| 368 | ] |
---|
| 369 | #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I} |
---|
| 370 | [1,4: whd <(as_label_ok ??????????? goodR st1' st2' f fn ?? H_fin) [1,4: assumption] |
---|
| 371 | cases daemon (*TODO: general lemma!*) |
---|
| 372 | |2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta |
---|
| 373 | >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta |
---|
| 374 | assumption |
---|
| 375 | |*: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta |
---|
| 376 | >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind |
---|
| 377 | cases(blm mid1) in CL_JUMP COST Hst2_mid; |
---|
| 378 | [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 379 | |2,4,6,8: [1,3: #c_id #args #dest |*: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 380 | ] |
---|
| 381 | #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta |
---|
| 382 | >m_return_bind assumption |
---|
[2851] | 383 | ] |
---|
[2863] | 384 | qed. |
---|
| 385 | |
---|
[2883] | 386 | (* |
---|
| 387 | let rec taa_to_taaf S st1 st2 (taa : trace_any_any S st1 st2) on taa : |
---|
| 388 | trace_any_any_free S st1 st2 ≝ |
---|
| 389 | (match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with |
---|
| 390 | [taa_base st1' ⇒ λprf.? |
---|
| 391 | |taa_step st1' st2' st3' H I J tl ⇒ λprf.? |
---|
| 392 | ]) (refl … st1) (refl … st2) (refl_jmeq ? taa). |
---|
| 393 | *) |
---|
| 394 | |
---|
[2898] | 395 | lemma general_eval_seq_no_call_ok :∀ P_in , P_out: sem_graph_params. |
---|
[2883] | 396 | ∀prog : joint_program P_in. |
---|
| 397 | ∀stack_sizes. |
---|
| 398 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 399 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
[2898] | 400 | ∀st_no_pc_rel,st_rel. |
---|
[2883] | 401 | let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in |
---|
| 402 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
| 403 | let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in |
---|
[2898] | 404 | good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good |
---|
| 405 | st_no_pc_rel st_rel → |
---|
[2883] | 406 | ∀st1,st1' : joint_abstract_status prog_pars_in. |
---|
| 407 | ∀st2 : joint_abstract_status prog_pars_out. |
---|
[2898] | 408 | ∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog). |
---|
[2883] | 409 | ∀stmt,nxt. |
---|
[2898] | 410 | st_rel st1 st2 → |
---|
[2940] | 411 | let seq ≝ (step_seq P_in ? stmt) in |
---|
| 412 | fetch_statement P_in … |
---|
| 413 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 414 | return 〈f, fn, sequential ?? seq nxt〉 → |
---|
[2883] | 415 | eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) |
---|
[2940] | 416 | st1 = return st1' → |
---|
[2898] | 417 | ∃st2'. st_rel st1' st2' ∧ |
---|
[2883] | 418 | ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. |
---|
| 419 | if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) |
---|
| 420 | (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ |
---|
[2891] | 421 | ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). |
---|
[2898] | 422 | #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel #st_rel |
---|
| 423 | #goodR #st1 #st1' #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval |
---|
| 424 | @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 425 | #H @('bind_inversion H) -H #st1_no_pc #H lapply(err_eq_from_io ????? H) -H |
---|
| 426 | #EQst1_no_pc whd in ⊢ (??%% → ?); whd in match next; whd in match set_pc; |
---|
| 427 | whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) |
---|
[2883] | 428 | cases(b_graph_transform_program_fetch_statement … good … EQfetch) |
---|
[2898] | 429 | #init_data * #t_fn ** >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) |
---|
[2891] | 430 | #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim |
---|
[2883] | 431 | [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta |
---|
| 432 | whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) |
---|
[2898] | 433 | * #_ >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) whd in match point_of_pc; |
---|
[2883] | 434 | normalize nodelta whd in match (point_of_offset ??); <ABS |
---|
| 435 | cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1) |
---|
| 436 | ] |
---|
[2898] | 437 | #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl |
---|
| 438 | >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC |
---|
[2883] | 439 | cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit |
---|
| 440 | (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) |
---|
[2891] | 441 | #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem |
---|
[2883] | 442 | %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} |
---|
[2898] | 443 | cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) |
---|
| 444 | #EQfn #_ |
---|
| 445 | % |
---|
| 446 | [ @(st_rel_def ??????????? goodR … f fn) |
---|
| 447 | [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption |
---|
| 448 | | <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption |
---|
| 449 | | @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption |
---|
| 450 | ] |
---|
| 451 | ] |
---|
[2891] | 452 | %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn |
---|
| 453 | SBiC EQst2_fin_no_pc)} |
---|
| 454 | @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch % |
---|
[2883] | 455 | qed. |
---|
[2898] | 456 | |
---|
| 457 | (* |
---|
| 458 | lemma eval_cost_ok : |
---|
| 459 | ∀ P_in , P_out: sem_graph_params. |
---|
| 460 | ∀prog : joint_program P_in. |
---|
| 461 | ∀stack_sizes. |
---|
| 462 | ∀ f_lbls,f_regs.∀f_bl_r.∀init. |
---|
| 463 | ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs. |
---|
| 464 | let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in |
---|
| 465 | let trans_prog ≝ b_graph_transform_program P_in P_out init prog in |
---|
| 466 | let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in |
---|
| 467 | ∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop. |
---|
| 468 | ∀st1,st1' : joint_abstract_status prog_pars_in. |
---|
| 469 | ∀st2 : joint_abstract_status prog_pars_out. |
---|
| 470 | ∀f. |
---|
| 471 | ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt. |
---|
| 472 | R st1 st2 → |
---|
| 473 | let cost ≝ COST_LABEL P_in ? c in |
---|
| 474 | fetch_statement P_in … |
---|
| 475 | (globalenv_noinit ? prog) (pc … st1) = |
---|
| 476 | return 〈f, fn, sequential ?? cost nxt〉 → |
---|
| 477 | eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) |
---|
| 478 | st1 = return st1' → |
---|
| 479 | ∃ st2'. R st1' st2' ∧ |
---|
| 480 | ∃taf : trace_any_any_free |
---|
| 481 | (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) |
---|
| 482 | st2 st2'. |
---|
| 483 | bool_to_Prop (taaf_non_empty … taf). |
---|
| 484 | #P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #good #R #st1 #st1' |
---|
| 485 | #st2 #f #fn #c #nxt #Rst1st2 normalize nodelta #EQfetch whd in match eval_state; |
---|
| 486 | whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind |
---|
| 487 | normalize nodelta >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
| 488 | *) |
---|