Changeset 2891
 Timestamp:
 Mar 16, 2013, 10:42:43 AM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2883 r2891 160 160 161 161 include "joint/StatusSimulationHelper.ma". 162 include alias "basics/lists/listb.ma". 162 163 163 164 lemma make_ERTL_To_ERTLptr_good_state_relation : … … 209 210 change with (pc_block (pc … st2)) in match (pc_block ?); 210 211 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn % 212  #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state; 213 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind 214 normalize nodelta #H @('bind_inversion H) H #st1_no_pc' #EQst1_no_pc' 215 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ) 216 whd in match sigma_state_pc in EQst1_no_pc'; normalize nodelta in EQst1_no_pc'; 217 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) 218 #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc' 219 #t_fn #EQt_fn whd % [2: %{(refl …)} ] lapply(err_eq_from_io ????? EQst1_no_pc') 220 EQst1_no_pc' #EQst1_no_pc' 221 cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc') 222 [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ) 223 %{(mk_state_pc ? st2_no_pc' 224 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt) 225 (last_pop … st2))} % 226 [ whd in ⊢ (??%?); >EQst2_no_pc' % 227  whd whd in match sigma_state_pc; normalize nodelta >EQfn % 228 ] 229  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta 230 inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ 231 cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) 232 (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = 233 return 〈f,fn,stmt1〉) 234 [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 235 cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) 236 #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *] 237 normalize nodelta #EQ destruct(EQ) * #labels * #registers 238 ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); 239 #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters 240 cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) 241 (get_used_registers_from_seq … (functs ERTL) stmt) ?) 242 [3: #a #_ cases(¬a∈registers) // 1: #H assumption] #H @⊥ 243 cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) 244 #reg ** #H1 #H2 @H1 H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters 245 #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption 246 ] 211 247 ] 212 248 qed. 
src/ERTL/ERTLtoERTLptrUtils.ma
r2845 r2891 413 413 (be_op2 b op). 414 414 #prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta 415 cases bv 415 cases daemon 416 qed. (*TODO*) 417 (*cases bv 416 418 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 417 normalize nodelta [ @res_preserve_error1] whd in match sigma_beval;419 normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval; 418 420 normalize nodelta 419 421 cases bv1 … … 499 501 ] 500 502 ] 501 qed. 503 qed.*) 502 504 503 505 lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct. … … 1049 1051 sigma_stored_pc prog f_lbls pc〉) 1050 1052 (pop_ra ERTL_semantics) 1051 (pop_ra ERTLptr_semantics). 1053 (pop_ra ERTLptr_semantics). 1054 cases daemon (*TODO*) qed. 1055 (* 1052 1056 #prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta 1053 1057 @mfr_bind1 … … 1088 1092  #pc @mfr_return_eq1 % 1089 1093 ] 1090 qed. 1094 qed.*) 1091 1095 1092 1096 lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc. 
src/joint/StatusSimulationHelper.ma
r2886 r2891 45 45 ] 46 46 qed. 47 48 49 definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).50 joint_classify_step p stmt = cl_other →51 (∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝52 λp,stmt,CL_OTHER,COST.53 (match stmt return λx.x = stmt → ? with54 [ COST_LABEL c ⇒ λprf.⊥55  CALL id args dest ⇒ λprf.⊥56  COND r lab ⇒ λprf.⊥57  step_seq seq ⇒ λprf.«seq,?»58 ])(refl …).59 @hide_prf60 [ lapply(COST c) * #H @H >prf %61 2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)62  >prf %63 ]64 qed.65 66 check ensure_step_block67 47 68 48 record good_state_relation (P_in : sem_graph_params) … … 141 121 ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes) 142 122 (globals (mk_prog_params P_out trans_prog stack_sizes))). 143 blp = (ensure_step_block ?? l) ∧ True 144 (* 145 TUTTO IL RESTO PARLA DI R 146 147 ∀mid,mid1. 148 stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid 149 = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→ 150 ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 151 ((\snd (\fst blp)) mid) = cl_other. 152 ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 153 (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?. 154 ∃st2_fin_no_pc. 155 let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in 156 let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes) 157 ((\snd (\fst blp)) mid) CL_OTHER ?)] in 123 blp = (ensure_step_block ?? l) ∧ 124 ∃st2_fin_no_pc. 158 125 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 159 (pre@ middle @ (\snd blp))(st_no_pc … st2)= return st2_fin_no_pc ∧126 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 160 127 let st2_fin ≝ 161 128 mk_state_pc ? st2_fin_no_pc 162 129 (pc_of_point P_out (pc_block(pc … st2)) nxt) 163 130 (last_pop … st2) in 164 R st1' st2_fin *)) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)131 R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq) 165 132 ) (init ? fn) 166 133 }. 167 (*@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)168 qed.*)169 134 170 135 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 270 235 if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) 271 236 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 272 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 273 cases daemon qed. 274 275 (* 237 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 276 238 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1' 277 239 #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval 278 240 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 279 241 #init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) 280 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta *** 281 #blp #blm #bls * @if_elim 242 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim 282 243 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 283 244 whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) … … 287 248 ] 288 249 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl 289 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC 290 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); 291 #_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 292 #_ 250 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC 293 251 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit 294 252 (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) 295 [4: @EQmid *:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????) 296 #seq_mid cases daemon (*TODO*) 297 qed. 298 299 cases(blm mid1) in 300 #stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC; destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ) 301 302 303 * #EQst2_pre_mid_no_pc 304 * #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin 253 #l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem 305 254 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} 306 %{Hfin} 307 lapply(taaf_to_taa ??? 308 (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn 309 seq_pre_l EQst2_pre_mid_no_pc) ?) 310 [ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta 311 whd in match (as_label ??); whd in match fetch_statement; normalize nodelta 312 >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc; 313 normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind 314 normalize nodelta >COST * #H @H %] 315 #taa1 316 letin st2_mid_pc ≝ (mk_state_pc ? st2_mid 317 (pc_of_point P_out (pc_block (pc … st2)) mid2) 318 (last_pop … st2)) 319 <(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l; 320 #seq_post_l 321 lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes) 322 st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn 323 (seq_post_l) EQst2_fin_no_pc) 324 * #taaf2 * #taaf2_prf1 #taaf2_prf2 325 %{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)} 326 [ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_ 327 % whd in match (as_costed ??); whd in match (as_label ??); 328 whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta 329 >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta 330 >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls 331 [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1 332 >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_ 333 >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta 334 * #H @H % 335  @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement; 336 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid 337 >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance; 338 normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1) 339 normalize nodelta 340 [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 341  #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 342  #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ) 343  #jseq #EQjseq #_ #_ % 344 ] 345  @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn 346 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption 347  @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 348 ] 349 qed. 350 *) 255 %{Rsem} 256 %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 257 SBiC EQst2_fin_no_pc)} 258 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 259 qed.
Note: See TracChangeset
for help on using the changeset viewer.