Changeset 2940
 Timestamp:
 Mar 22, 2013, 7:16:17 PM (5 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2898 r2940 165 165 definition state_rel ≝ λprog : ertl_program.λf_lbls. 166 166 λf_regs : (block → label → list register). 167 λbl ,st1,st2.∃f,fn.167 λbl.λ_:label.λst1,st2.∃f,fn. 168 168 fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 169 169 let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in … … 236 236 whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind 237 237 normalize nodelta #H @('bind_inversion H) H #st1_no_pc' #EQst1_no_pc' 238 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ) 238 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 239 whd in match (succ_pc ???); normalize nodelta 240 whd in match (set_no_pc ???); normalize nodelta 241 whd in ⊢ (%→?); #EQ destruct(EQ) 239 242 whd in match sigma_state_pc in EQst1_no_pc'; normalize nodelta in EQst1_no_pc'; 240 243 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch) … … 838 841 >EQcall in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); normalize nodelta 839 842 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); 840 >EQfetch' in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); % 843 >EQfetch' in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); normalize nodelta 844 845 [cut (block_of_call 846 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 847 (globals 848 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) 849 (ev_genv 850 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) 851 (inr ident … 〈c_ptr1,c_ptr2〉) 852 (set_regs ERTL_state 853 〈add RegisterTag beval (\fst (regs ERTLptr_semantics st2)) r 854 (\snd (beval_pair_of_pc 855 (pc_of_point ERTLptr_semantics 856 (pc_block (pc ERTLptr_semantics st2)) mid1))), 857 \snd (regs ERTLptr_semantics st2)〉 858 st_no_pc_pre_call) = 859 block_of_call (mk_prog_params ERTL_semantics prog stack_size) 860 (globals (mk_prog_params ERTL_semantics prog stack_size)) 861 (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) 862 (inr ident … 〈c_ptr1,c_ptr2〉) 863 (sigma_state_pc prog f_lbls f_regs st2)) 864 [ 865 866 generalize in match (block_of_call ?????); 867 868 % 841 869 *: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 842 870 @if_elim change with (pc_block(pc … st2)) in match (pc_block ?); 
src/ERTLptr/ERTLptrToLTLProof.ma
r2938 r2940 530 530 qed. 531 531 532 axiom to_be_cleared_sb_respects_equal_valuations: 533 ∀live,coloured,l1,l2. 534 live l1 = live l2 → 535 to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2. 536 537 axiom to_be_cleared_fb_respects_equal_valuations: 538 ∀live,l1,l2. 539 live l1 = live l2 → 540 to_be_cleared_fb live l1 = to_be_cleared_fb live l2. 541 532 542 lemma make_ERTLptr_To_LTL_good_state_relation : 533 543 ∀fix_comp,colour,prog. … … 601 611 normalize nodelta #EQ cases(state_pc_eq … EQ) * 602 612 #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn} 603 <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 … 604 (point_of_pc ERTLptr_semantics (pc … st2))) 613 <(insensitive_to_be_cleared_sb prog … st2) 605 614 [2,4: @dead_registers_in_dead @acc_is_dead ] 606 assumption 615 whd >point_of_pc_of_point 616 [ cut 617 (analyse_liveness fix_comp … fn ltrue = 618 analyse_liveness fix_comp … fn 619 (point_of_pc ERTLptr_semantics (pc … st1))) 620 [ cases daemon (*CSC: Genuine proof obligation! *) 621  #Hext ] 622  cut 623 (analyse_liveness fix_comp … fn lfalse = 624 analyse_liveness fix_comp … fn 625 (point_of_pc ERTLptr_semantics (pc … st1))) 626 [ cases daemon (*CSC: Genuine proof obligation! *) 627  #Hext ]] 628 >(to_be_cleared_sb_respects_equal_valuations … 629 (colour … fn …) … Hext) <EQst1st2 630 >(to_be_cleared_fb_respects_equal_valuations … Hext) % 607 631 ] 608 632 *: % 
src/joint/StatusSimulationHelper.ma
r2939 r2940 150 150 (st_no_pc ? st2) 151 151 = return st2_pre_mid_no_pc ∧ 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) ∧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) ∧ 154 154 joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 155 155 ((\snd (\fst blp)) mid) = cl_jump ∧ … … 187 187 repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 188 188 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 189 st_no_pc_rel (pc_block (pc … st1 ))190 (point_of_pc P_in … (pc … st1 ))189 st_no_pc_rel (pc_block (pc … st1')) 190 (point_of_pc P_in … (pc … st1')) 191 191 (st_no_pc … st1') st2_fin_no_pc 192 192 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) … … 272 272 *) 273 273 274 (* 274 275 (*CSC: Isn't this already proved somewhere else??? *) 275 276 lemma point_of_pc_pc_of_point: … … 279 280 (pc_block (pc P_in st)) l) = l. 280 281 #P * // 281 qed. 282 qed.*) 282 283 283 284 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 298 299 ∀a,ltrue,lfalse. 299 300 st_rel st1 st2 → 300 301 fetch_statement P_in …302 (globalenv_noinit ? prog) (pc … st1) =303 return 〈f, fn, sequential … cond lfalse〉 →304 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)305 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' → 306 307 as_costed (joint_abstract_status prog_pars_in) st1' → 307 308 ∃ st2'. st_rel st1' st2' ∧ … … 349 350 [1,3: @(st_rel_def … goodR … f fn ?) 350 351 [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption 351 2,5: >point_of_pc_pc_of_pointassumption352 2,5: assumption 352 353 3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption 353 354 ] … … 408 409 ∀stmt,nxt. 409 410 st_rel st1 st2 → 410 411 fetch_statement P_in …412 (globalenv_noinit ? prog) (pc … st1) =413 return 〈f, fn, sequential ?? seq nxt〉 →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〉 → 414 415 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 415 416 st1 = return st1' → 416 417 ∃st2'. st_rel st1' st2' ∧ 417 418 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
Note: See TracChangeset
for help on using the changeset viewer.