Changeset 2843 for src/ERTL/ERTLtoERTLptrOK.ma
 Timestamp:
 Mar 11, 2013, 1:02:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLtoERTLptrOK.ma
r2801 r2843 122 122 ∀f_bl_r. 123 123 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 124 translate_dataprog f_bl_r f_lbls f_regs →124 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 125 125 ∀st,fn,id,stmt. 126 126 fetch_statement ERTL_semantics (prog_var_names … prog) … … 167 167 ∀f_bl_r. 168 168 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 169 translate_dataprog f_bl_r f_lbls f_regs →169 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 170 170 ∀st2 : state_pc ERTLptr_semantics. 171 171 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in … … 197 197 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply EQfetch 198 198 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch' 199 lapply(fetch_statement_inv … EQfetch') * #EQfn #EQstmt 200 cases(b_graph_transform_program_fetch_internal_function … good … EQfn) 199 cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') 201 200 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta 202 [2: #r #tl *] #EQ destruct(EQ) * #_ #_ #_ #_ #_ #_ #_ #fresh_regs #_ #_ #stmt_at_spec 203 cases(stmt_at_spec … EQstmt) #labs * #regs ** #EQlabs #EQregs normalize nodelta 204 >if_merge_right in ⊢ (% → ?); [2: %] whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?); 205 cases regs in EQregs; regs [2: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ) 206 #eval_spec 201 [2: #r #tl *] #EQ destruct(EQ) * #labs * #regs ******* #EQlabs #EQregs #_ #_ #_ #_ 202 #fresh_regs * #bl * >if_merge_right in ⊢ (% → ?); [2: %] 203 whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs 204 #EQ destruct(EQ) #eval_spec 207 205 lapply(err_eq_from_io ????? EQnopc) EQnopc >(fetch_stmt_ok_sigma_state_ok … EQfetch) 208 206 #EQnopc 209 cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ????????? EQnopc) 210 [2: @(t_fn1) 211  #stnopc'' * #EQstnopc'' #EQsem % 207 cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQnopc) 208 [ #stnopc'' * #EQstnopc'' #EQsem % 212 209 [ % [@stnopc''  @(succ_pc ERTL_semantics (pc … st2) nxt)  @(last_pop … st2)]] 213 210 % … … 221 218 normalize nodelta * #H @H whd in ⊢ (??%?); >EQfetch % 222 219  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta 223 inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cases(stmt_at_spec … EQstmt1) 224 #labels * #registers ** #_ #EQregisters #_ labels >EQregisters whd 225 check excluded_middle_list 220 inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ 221 cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) 222 (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) = 223 return 〈f,fn,stmt1〉) 224 [ lapply(fetch_statement_inv … EQfetch') * #EQfn #_ whd in ⊢ (??%?); 225 >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1 226 cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1) 227 #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *] 228 normalize nodelta #EQ destruct(EQ) * #labels * #registers 229 ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); 230 #EQregisters #_ #_ #_ #_ #_ #_ >EQregisters 226 231 cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) 227 (get_used_registers_from_seq … (functs ERTL) stmt) ?) 228 [3: #a #_ cases(¬a∈registers) // 1: #H assumption] #H @⊥ 232 (get_used_registers_from_seq … (functs ERTL) stmt) ?) 233 [3: #a #_ cases(¬a∈registers) // 1: #H assumption] #H @⊥ 234 lapply(fetch_statement_inv … EQfetch') * #_ normalize nodelta #EQstmt 229 235 cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt)) 230 #reg ** #H1 #H2 @H1 H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters236 #reg ** #H1 #H2 @H1 H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters 231 237 whd in ⊢ (% → ?); #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption 232 238 ] … … 239 245 ∀f_bl_r. 240 246 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 241 translate_dataprog f_bl_r f_lbls f_regs →247 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 242 248 ∀st2. 243 249 let st1 ≝ (sigma_state_pc prog f_lbls f_regs st2) in … … 456 462 ∀f_bl_r. 457 463 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 458 translate_dataprog f_bl_r f_lbls f_regs.464 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 459 465 ∀st2,st1',f,fn,a,ltrue,lfalse. 460 466 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in … … 561 567 ∀f_bl_r. 562 568 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 563 translate_dataprog f_bl_r f_lbls f_regs.569 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 564 570 ∀st2,st1',f,fn,c,nxt. 565 571 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in … … 609 615 ∀f_bl_r. 610 616 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 611 translate_dataprog f_bl_r f_lbls f_regs.617 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 612 618 ∀st2,st1',f,fn,called,args,dest,nxt. 613 619 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in … … 628 634 (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2_pre_call 629 635 =return st2'. 630 #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id  #c_ptr]636 #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id  * #c_ptr1 #c_ptr2 ] 631 637 #args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch 632 638 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind … … 652 658 lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?); 653 659 #EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt 654 cases(b_graph_transform_program_fetch_ internal_function … good … EQfn)660 cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch') 655 661 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) 656 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_ 657 #_ #_ #_ #_ #_ #H cases(H … EQstmt) H #labels * #registers 658 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %] 659 whd in match translate_step; normalize nodelta * #bl * 660 cases registers in EQregisters; registers normalize nodelta 661 [2,3: [ #x #y] #_ *4: #r #tl] #EQregisters 662 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers 663 ******* #EQlabels #EQregisters #_ #_ #_ #_ #fresh_regs 664 normalize nodelta >if_merge_right [2,4: %] whd in match translate_step; 665 normalize nodelta * #bl * cases registers in EQregisters; registers 666 normalize nodelta [2,3: [ #x #y] #_ *4: #r #tl] #EQregisters 662 667 [ whd in ⊢ (% → ?); cases tl in EQregisters; tl [2: #x #y #_ *] normalize nodelta 663 668 #EQregisters  whd in ⊢ (% → ?);] #EQ destruct(EQ) … … 673 678 [1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %] 674 679 cases(ertl_save_frame_ok prog f_lbls f_regs ? 675 (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st2)))) 676 ? st1''' ?) 680 (added_registers ERTL (prog_var_names … prog) fn1 (f_regs c_bl')) ? st1''' ?) 677 681 [2: @PTR 678 682 3,7: [ %{(mk_state_pc ? (st_no_pc … st2) … … 704 708 whd in match set_no_pc; normalize nodelta] 705 709 #EQst_no_pc_after_call #EQ destruct(EQ) 706 [ %{(mk_state_pc ? st_no_pc_pre_call 710 [ letin pairpc ≝ (beval_pair_of_pc 711 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)) 712 %{(mk_state_pc ? (set_regs ERTL_state 713 (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) 714 st_no_pc_pre_call) 707 715 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) 708 716 (last_pop … st2))} … … 732 740 ] 733 741 4: %{(taa_base …)} 734  lapply(produce_trace_any_any_free (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 742  %{(taaf_to_taa ??? 743 (produce_trace_any_any_free 744 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 735 745 st2 ????? 736 (mk_state_pc ? st_no_pc_pre_call 737 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) 738 (last_pop … st2)) EQcalling' m_fetch_pre ?) 739 [2: #taaf inversion(taaf) 740 [ #s #EQ #EQ1 @⊥ destruct(EQ EQ1) cases s in EQ1 EQst_no_pc_pre_call; 741 * #fms #is #bb #regs #m #y #z #EQ #H @('bind_inversion H) H #a1 742 #H @('bind_inversion H) H #is1 whd in ⊢ (??%% → ?); cases is in EQ; 743 [2: #bv1 3: #bv1 #bv2] #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) 744 whd in ⊢ (??%% → ??%% → ?); #EQ1 destruct(EQ1) normalize nodelta 745 whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) destruct(EQ) 746 3: #s1 #s2 #s3 #taa #H1 #H2 #H3 #EQ #EQ1 @⊥ destruct(EQ EQ1) 747 lapply H3 H3 whd in ⊢ (% → ?); whd in match (as_label ??); 748 whd in match fetch_statement; normalize nodelta 749 whd in match (as_pc_of ??); >EQcalling' >m_return_bind 750 whd in match point_of_pc; normalize nodelta; >point_of_offset_of_point 751 >EQcall normalize nodelta whd in match cost_label_of_stmt; 752 normalize nodelta * #H @H % 753 ] 754 #s1 #s2 #s3 #taa #H1 #H2 #EQst2 #EQs3 #_ <EQst2 in taa; <EQs3 in H1; #H1 #taa 755 %{(taa_append_taa … taa (taa_step … H1 … (taa_base …)))} 756 xxxxxxxxxxxxxxxxxxxx 757 3,7: whd in match sigma_pc_opt; normalize nodelta @if_elim 758 [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; 759 [1,3: #EQ destruct(EQ) *: assumption]] 760 #_ [ 761 762 763 whd in ⊢ (% → ?); 764 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?); 765 * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 766 whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 * 767 #EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 768 whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh 769 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 770 * #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2 771 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 772 ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) 773 whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?); 774 * #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 775 776 777 778 779 780 781 782 783 784 785 786 [ letin pairpc ≝ (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)) 787 letin st2_pre ≝ (mk_state_pc ? 788 (mk_state ? (st_frms … st2) (both_is (\fst pairpc) (\snd pairpc)) 789 (carry … st2) (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) 790 (m … st2)) 791 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) 792 (last_pop … st2)) 793 %{st2_pre} 794  %{st2} 795 ] % 796 [1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 797 >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind % ] 746 (mk_state_pc ? 747 (set_regs ERTL_state 748 (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉) 749 st_no_pc_pre_call) 750 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) 751 (last_pop … st2)) 752 EQcalling' m_fetch_pre ?) ?)} 753 [ @if_elim [2: #_ @I] #_ % whd in ⊢ (% → ?); whd in match (as_label ??); 754 whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta 755 >EQcalling' >m_return_bind whd in match point_of_pc; normalize nodelta 756 >point_of_offset_of_point >EQcall >m_return_bind normalize nodelta 757 whd in match cost_label_of_stmt; normalize nodelta * #H @H % 758  whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?); 759 whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ? _ ⇒ ?]?); 760 normalize nodelta whd in match (eval_ext_seq ????????); 761 whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; 762 normalize nodelta @('bind_inversion EQfn) * #f2 * #fn2 763 whd in match fetch_function; normalize nodelta #H 764 lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) H #f3 #EQf3 765 #H @('bind_inversion H) H #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2 766 destruct(EQ1 EQ2) 767 >(find_symbol_transf … 768 (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) 769 >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq 770 normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta 771 whd in ⊢ (??%?); 772 whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ? _ ⇒ ?]?); 773 normalize nodelta whd in match (eval_ext_seq ????????); 774 whd in match acca_arg_retrieve; normalize nodelta 775 change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); 776 whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta 777 >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta 778 @('bind_inversion EQst_no_pc_pre_call) #new_st whd in match push in ⊢ (%→ ?); 779 normalize nodelta #H @('bind_inversion H) H #is1 #EQis1 whd in ⊢ (??%% → ?); 780 #EQ destruct(EQ) #H @('bind_inversion H) H #is2 #EQis2 whd in match set_istack; 781 normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match push; 782 normalize nodelta >EQis1 >m_return_bind whd in match set_istack; normalize nodelta 783 whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ? _ ⇒ ?]?); 784 normalize nodelta whd in match (eval_ext_seq ????????); 785 whd in match (get_pc_from_label ?????); whd in match block_of_funct_id; 786 normalize nodelta 787 >(find_symbol_transf … 788 (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) 789 >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq 790 normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta 791 whd in ⊢ (??%?); 792 whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ? _ ⇒ ?]?); 793 normalize nodelta whd in match (eval_ext_seq ????????); 794 whd in match acca_arg_retrieve; normalize nodelta 795 change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); 796 whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta 797 >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta 798 whd in match push; normalize nodelta >EQis2 >m_return_bind normalize nodelta 799 whd in ⊢ (??%?); @eq_f whd in match set_istack; normalize nodelta 800 whd in match reg_store; normalize nodelta >add_idempotent % 801  cut(∀st,st',kind.ertlptr_save_frame kind it st = return st' → 802 ∃hd,tl.st_frms … st' = return (cons ? hd tl) ∧ 803 \snd hd = pc_block (pc … st)) 804 [ #st * #frms #is #b #regs #m * whd in match ertlptr_save_frame; 805 normalize nodelta [ >m_return_bind  #H @('bind_inversion H) H #st'' #EQst''] 806 #H @('bind_inversion H) H #frames #H lapply(opt_eq_from_res ???? H) H 807 #EQframes whd in ⊢ (??%% → ?); whd in match set_frms; whd in match set_regs; 808 normalize nodelta #EQ destruct(EQ) %{(〈\fst (regs ERTLptr_semantics ?),pc_block (pc … st)〉)} 809 [2,4: %{frames} % [1,3: %] 1,3:] %] 810 ] #save_frame_non_empty cases(save_frame_non_empty … EQst_no_pc_after_call) 811 * #fst_hd #snd_hd * #rest * #EQrest #EQhd 812 ] 813 cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?) 814 [2,4: whd in match fetch_internal_function; normalize nodelta >EQfn1 %] 815 #init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_ 816 [ %{(mk_state_pc ? st_no_pc_after_call 817 (pc_of_point 818 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 819 c_bl' (joint_if_entry … t_fn1)) 820 (last_pop … st2))} 821  822 %{(mk_state_pc ? (set_frms ERTL_state (〈(add ?? (fst_hd) r (\snd pairpc)),snd_hd〉 823 :: rest) 824 st_no_pc_after_call) 825 (pc_of_point 826 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 827 c_bl' (joint_if_entry … t_fn1)) 828 (last_pop … st2))} 829 ] 798 830 % 799 [1,3: % 800 [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?); 801 normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 802 >m_return_bind in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 803 [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?);] 804 >EQcall in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); normalize nodelta 805 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); 806 >EQfetch' in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); % 807 *: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 808 @if_elim change with (pc_block(pc … st2)) in match (pc_block ?); 809 [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_ 810 >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption] 811 whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_ 812 [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels) 813  >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) 814 ] 815 >m_return_bind >pc_of_point_of_pc % 816 ] 817 4: %{(taa_base …)} 818 2: letin st2'' ≝ (mk_state_pc ? 819 (mk_state ? (st_frms … st2) (empty_is) (carry … st2) 820 (〈add ?? (\fst (regs … st2)) r (\fst pairpc),\snd(regs … st2)〉) 821 (m … st2)) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid) 822 (last_pop … st2)) 823 letin st2''' ≝ (mk_state_pc ? (set_istack ? (one_is (\fst pairpc)) st2'') 824 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid3) 825 (last_pop … st2)) 826 letin st2''''≝ (mk_state_pc ? (mk_state ? (st_frms … st2) (istack … st2''') 827 (carry … st2) 828 (〈add ?? (\fst (regs … st2''')) r (\snd pairpc),\snd (regs … st2)〉) (m … st2''')) 829 (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid4) (last_pop … st2)) 830 %{(taa_step ? st2 st2'' st2_pre ??? 831 (taa_step ? st2'' st2''' st2_pre ??? 832 (taa_step ? st2''' st2'''' st2_pre ??? 833 (taa_step ? st2'''' st2_pre st2_pre ??? (taa_base …)))))} 834 [3,6,7,10: % whd in ⊢ (% → ?); * #H @H whd in ⊢ (??%?); 835 whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind 836 [ >point_of_pc_of_point >EQhigh 837  >point_of_pc_of_point >EQcall 838  >point_of_pc_of_point >EQpush2 839  >point_of_pc_of_point >EQpush1 ] % 840 1,2,4,5,8,9,11,12: whd 841 [1,3,6,8: whd in match eval_state; normalize nodelta 842 *: whd in ⊢ (??%?); 831 [1,3: whd in match sigma_state_pc; normalize nodelta 832 whd in match pc_of_point in ⊢ (???%); normalize nodelta 833 whd in match fetch_internal_function; normalize nodelta >EQfn1 834 >m_return_bind normalize nodelta @eq_f3 835 [1,3,6: % 2,5: >EQentry %] 836 whd in match sigma_state; normalize nodelta 837 cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2. 838 a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → 839 mk_state ERTL_semantics a1 b1 c1 d1 e1 = 840 mk_state ERTL_semantics a2 b2 c2 d2 e2) 841 [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 842 #H15 //] #APP @APP try % 843 whd in match set_frms; normalize nodelta >EQrest 844 whd in match sigma_frames; normalize nodelta >m_return_bind 845 >m_return_bind whd in match sigma_frames_opt; whd in match m_list_map; 846 normalize nodelta whd in match (foldr ?????) in ⊢ (???%); 847 normalize nodelta >EQhd >EQfn >m_return_bind normalize nodelta 848 whd in match (foldr ?????); normalize nodelta 849 >EQfn >m_return_bind normalize nodelta 850 change with (sigma_frames_opt prog f_lbls f_regs ?) 851 in match (foldr ?????); 852 change with (sigma_frames_opt prog f_lbls f_regs ?) 853 in match (foldr ?????); 854 cases(sigma_frames_opt ????) [%] #t_rest >m_return_bind >m_return_bind 855 @eq_f @eq_f2 [2: %] @eq_f2 [2: %] 856 change with (pc_block (pc … st2)) in match (pc_block ?); 857 change with (pc_block (pc … st2)) in match (pc_block ?); 858 whd in match sigma_register_env; normalize nodelta 859 >map_add >set_minus_add [%] @list_as_set_mem @in_added_registers 860 [@(point_of_pc ERTL_semantics (pc ERTLptr_semantics st2)) 861  whd in match code_has_label; whd in match code_has_point; normalize nodelta 862 >EQstmt %  >EQregisters % % ] 863 *: whd in match fetch_statement; normalize nodelta; >EQcalling' >m_return_bind 864 [2: >point_of_pc_of_point ] >EQcall >m_return_bind normalize nodelta 865 >m_return_bind 866 [2: >EQc_bl' >m_return_bind 867  whd in match block_of_call; normalize nodelta 868 @('bind_inversion EQst_no_pc_pre_call) #st3 #H @('bind_inversion H) H 869 #is3 inversion(istack … st2) [2: #bv 3: #bv1 #bv2] #EQis3 870 whd in match is_push; normalize nodelta whd in ⊢ (??%% → ??%% → ?); 871 #EQ1 #EQ2 destruct(EQ1 EQ2) #H @('bind_inversion H) H #is3 872 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 873 whd in match set_regs; whd in match dpl_arg_retrieve; normalize nodelta 874 change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); 875 @('bind_inversion EQc_bl') #c_bl'' whd in match dpl_arg_retrieve; normalize nodelta 876 change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????); 877 #H @('bind_inversion H) H #bv_ptr1 whd in match ps_arg_retrieve; 878 normalize nodelta cases (c_ptr1) in EQstmt; [#r_ptr1  #b_ptr1] #EQstmt 879 normalize nodelta 880 [ whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta 881 #H lapply(opt_eq_from_res ???? H) H #EQbv_ptr1 882  whd in ⊢ (??%% → ?); #EQ destruct(EQ) 883 ] 884 whd in match dph_arg_retrieve; normalize nodelta 885 change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); 886 whd in match ps_arg_retrieve; normalize nodelta cases c_ptr2 in EQstmt; 887 [1,3: #r_ptr2 *: #b_ptr2] #EQstmt normalize nodelta 888 [1,2: whd in match ps_reg_retrieve; whd in match reg_retrieve; 889 normalize nodelta #H @('bind_inversion H) H 890 #bv_ptr2 #H lapply(opt_eq_from_res ???? H) H #EQbv_ptr2 891 *: >m_return_bind 892 ] #H @('bind_inversion H) H #ptr #EQptr @if_elim #ptr_ok whd in ⊢ (??%% → ?); 893 #EQ destruct(EQ) #H lapply(opt_eq_from_res ???? H) H #EQptr_code 894 [2,4: >m_return_bind 895 *: >lookup_add_miss 896 [1,3: >EQbv_ptr1 >m_return_bind 897 *: % #ABS destruct(ABS) 898 lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) 899 >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS 900 lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; 901 whd in match get_used_registers_from_step; normalize nodelta 902 whd in ⊢ (???% → ?); * // 903 ] 904 ] 905 change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????); 906 whd in match ps_arg_retrieve; normalize nodelta 907 [2,4: >m_return_bind 908 *: whd in match ps_reg_retrieve; whd in match reg_retrieve; 909 normalize nodelta >lookup_add_miss 910 [1,3: >EQbv_ptr2 >m_return_bind 911 *: % #ABS destruct(ABS) 912 lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2))) 913 >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS 914 lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers; 915 whd in match get_used_registers_from_step; normalize nodelta 916 whd in ⊢ (???% → ?); * // #_ * // 917 ] 918 ] 919 >EQptr >m_return_bind @if_elim [2,4,6,8: >ptr_ok *] #_ >m_return_bind 920 >EQptr_code >m_return_bind 843 921 ] 844 whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind 845 [1,5: >point_of_pc_of_point >EQpush1 >m_return_bind [2: %] 846 2,6: >point_of_pc_of_point >EQpush2 >m_return_bind [2: %] 847 3,7: >point_of_pc_of_point >EQhigh >m_return_bind [2: %] 848 *: >EQlow >m_return_bind [2: %] 922 @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQfn2 normalize nodelta 923 whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn2 >m_return_bind normalize nodelta 924 [ change with (ertlptr_save_frame ? it ?) in match (save_frame ??????); 925 cut(st2 = mk_state_pc ? st2 (pc … st2) (last_pop … st2)) 926 [ cases st2 #H1 #H2 #H3 %] #EQ <EQ EQ >EQst_no_pc_after_call 927 >m_return_bind 928 *: change with (ertlptr_save_frame PTR it ?) in match (save_frame ??????); 929 @('bind_inversion EQst_no_pc_after_call) #st4 whd in ⊢ (??%% → ?); 930 #EQ destruct(EQ) #H @('bind_inversion H) H #frms4 #H 931 lapply(opt_eq_from_res ???? H) H #EQfrms4 whd in ⊢ (??%% → ?); 932 #EQ destruct(EQ) whd in match ertlptr_save_frame; normalize nodelta 933 >m_return_bind whd in EQrest : (???%); destruct(EQrest) >EQfrms4 934 >m_return_bind 849 935 ] 850 whd in match eval_statement_no_pc; whd in match eval_seq_no_pc; normalize nodelta 851 whd in match (eval_ext_seq ?????????); whd in match (get_pc_from_label ?????); 852 whd in match block_of_funct_id; normalize nodelta 853 [1,2: whd in match acca_arg_retrieve; normalize nodelta 854 change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????); 855 whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta 856 >lookup_add_hit >m_return_bind [% >add_idempotent %] 857 *: @('bind_inversion EQfn) * #f2 * #fn2 whd in match fetch_function; 858 normalize nodelta #H lapply(opt_eq_from_res ???? H) H 859 #H @('bind_inversion H) H #f3 #EQf3 #H @('bind_inversion H) H 860 #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 861 >(find_symbol_transf … 862 (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f) 863 >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq 864 normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta 865 whd in match ps_reg_store_status; normalize nodelta >m_return_bind [%] 866 whd in match eval_statement_advance; normalize nodelta whd in match set_no_pc; 867 normalize nodelta whd in match next; whd in match set_pc; normalize nodelta 868 @eq_f @eq_f3 [2,3: %] whd in match set_regs; normalize nodelta 869 cut(istack … st2 = empty_is) 870 [ @('bind_inversion EQst1'') #new_st whd in match push_ra; normalize nodelta 871 #H @('bind_inversion H) H #new_st' whd in match push; normalize nodelta 872 #H @('bind_inversion H) H #new_is whd in match sigma_state; normalize nodelta 873 cases(istack ? st2) [ #_ #_ #_ #_ % 3: #bv1 #bv2 whd in ⊢ (??%% → ?); #EQ destruct] 874 #bv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_istack; normalize nodelta 875 whd in ⊢ (??%% → ?); #EQ destruct #H @('bind_inversion H) H #new_is2 whd in ⊢ (??%% → ?); 876 #EQ destruct(EQ) ] #EQ >EQ % 877 ] 878 ] 936 change with (stack_size ?) in match (stack_sizes ????); >EQs_size 937 >m_return_bind % 879 938 ] 880 cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?) 881 [2,4: whd in match fetch_internal_function; normalize nodelta lapply(err_eq_from_io ????? EQfn1) 882 EQfn1 #EQfn1 >EQfn1 %] 883 #init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_ 884 [2: %{(mk_state_pc ? (set_frms ERTL_state (〈\fst (regs … st2_pre),pc_block(pc … st2)〉 :: (st_frms … st2)) 885 (set_regs ERTL_state (〈empty_map …,\snd (regs … st2)〉) st2_pre)) 886 (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 887 c_bl' (joint_if_entry … t_fn1)) 888 (last_pop … st2))} 889  @('bind_inversion EQst1'') #new_st 890 cut(pc … st2 = sigma_stored_pc prog f_lbls (pc … st2)) 891 [ whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 892 @if_elim [ @eqZb_elim [2: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; [2: //] #EQ destruct] 893 #_ >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) >m_return_bind >pc_of_point_of_pc %] 894 #EQ >EQ #EQnew_st cases(push_ra_ok … EQnew_st) 895 [2: lapply EQ whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???) [2: #x #_ % #EQ destruct] 896 normalize nodelta #ABS >fetch_internal_function_no_zero in EQfn; [2: >ABS %] #EQ destruct] 897 #t_new_st * #EQt_new_st #new_st_t_new_st whd in ⊢ (???% → ?); #EQ destruct(EQ) 898 %{(mk_state_pc ? (set_frms ERTL_state (〈(\fst (regs … t_new_st)), pc_block (pc … st2)〉 :: (st_frms … st2)) 899 (set_regs ERTL_state (〈empty_map …,\snd(regs … st2)〉) t_new_st)) 900 (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 901 c_bl' (joint_if_entry … t_fn1)) 902 (last_pop … st2))} 903 ] % 904 [1,3: whd in match sigma_state_pc; normalize nodelta whd in match fetch_internal_function; 905 normalize nodelta lapply(err_eq_from_io ????? EQfn1) EQfn1 #EQfn1 >EQfn1 >m_return_bind 906 normalize nodelta @eq_f3 try % [2,4: >EQentry %] whd in match sigma_state; normalize nodelta 907 whd in match set_frms; whd in match set_regs; normalize nodelta 908 [ @('bind_inversion EQst1'') #new_st #H @('bind_inversion H) H #new_st1 909 #H @('bind_inversion H) H #new_is whd in match is_push; normalize nodelta 910 whd in match sigma_state; normalize nodelta cases (istack … st2) normalize nodelta 911 [3: #bv1 #bv2 whd in ⊢ (???% → ?); #EQ destruct(EQ) 2: #bv] whd in ⊢ (??%% → ?); 912 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct 913 whd in ⊢ (???% → ?); #EQ destruct(EQ) 914 ] 915 cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 → 916 mk_state ERTL_semantics a1 b1 c1 d1 e1 = 917 mk_state ERTL_semantics a2 b2 c2 d2 e2) 918 [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 //] 919 #APP @APP 920 [ whd in match sigma_frames in ⊢ (???%); normalize nodelta whd in match sigma_frames_opt; 921 whd in match m_list_map; normalize nodelta whd in match (foldr ?????); 922 normalize nodelta >EQfn >m_return_bind normalize nodelta 923 check coerced_step_list_in_code 924 whd in match sigma_frames; whd in match sigma_frames_opt; whd in match m_list_map; 925 normalize nodelta cases(foldr ? (Option ?) ???) [% 926 // 927 whd in ⊢ 928 xxxxxxxxxxxxxxxxxxxxxxxx 929 930 change with c_bl' in match (pc_block ?) in ⊢ (???%); >EQfn1 931 change with (ge … (ev_genv (mk_prog_params ERTL_semantics prog stack_size))) 932 in match (globalenv_noinit ? prog); >EQfn1 933 change with 934 935 #EQnew_st whd in ⊢ (???% → ?); #EQ destruct(EQ) cases(push_ra_ok ???????? EQnew_st) 936 937 xxxxxxxxxxx 938 lapply EQfn whd in match fetch_internal_function; whd in match fetch_function; 939 normalize nodelta 940 check find_symbol 941 letin (*〈addrl,addrh〉*) x ≝ beval_pair_of_pc ? % 942 943 944 945 %{(mk_state_pc ? 946 (mk_state ? (st_frms … st2) 947 (both_is (\snd (beval_pair_of_pc (pc … st2))) 948 (\fst (beval_pair_of_pc (pc … st2)))) 949 (carry … st2) (regs … st2) (m … st2)) 950 (pc … st2) 951 (last_pop … st2))} 952 953 954 955 956 957 958 959 960 939 qed. 940 961 941 962 942 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ … … 965 945 966 946 lemma ertl_to_ertlptr_ok: 967 ∀prog. 947 ∀prog.∀stack_sizes. 968 948 let trans_prog ≝ ertl_to_ertlptr prog in 969 ∀ f_lbls,f_regs,stack_sizes.970 ∀f_bl_r.971 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics972 translate_data prog f_bl_r f_lbls f_regs →973 949 ex_Type1 … (λR. 974 950 status_simulation 975 951 (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). 976 #prog #f_lbls #f_regs #stack_size #f_bl_r #good % 952 #prog #stack_size 953 cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 954 (λglobals,fn.«translate_data globals fn,(refl …)») prog) 955 #fregs * #f_lbls * #f_bl_r #good % 977 956 [@ERTLptrStatusSimulation assumption] 978 957 whd in match status_simulation; normalize nodelta … … 987 966 [ * [ #cost  #called_id #args #dest #reg #lbl  #seq] #nxt  #fin_step  *] 988 967 #EQfetch 989 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]);990 [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind 991 968 change with (joint_classify ??) in 969 ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]); 970 [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta 992 971 cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne 993 972 %{st2'} %{taf} >tafne normalize nodelta % [ % [@I  assumption]] 994 973 whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *) 995  (*CALL*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind974  (*CALL*) whd in match joint_classify; normalize nodelta >EQfetch 996 975 normalize nodelta #is_call_st1 997 976 cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1' … … 1001 980 %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption] 1002 981 whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*) 1003  (*COND*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind982  (*COND*) whd in match joint_classify; normalize nodelta >EQfetch 1004 983 normalize nodelta #n_costed 1005 984 cases(eval_cond_ok … good … EQfetch EQeval) [2: @n_costed] 1006 985 #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@Iassumption]] 1007 986 whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (*TODO*) 1008  (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind987  (*seq*) whd in match joint_classify; normalize nodelta >EQfetch 1009 988 normalize nodelta 1010 989 cases (eval_seq_no_call_ok … good … EQfetch EQeval) … … 1014 993  cases fin_step in EQfetch; 1015 994 [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta 1016 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]);normalize nodelta995 >EQfetch normalize nodelta 1017 996 cases (eval_goto_ok … good … EQfetch EQeval) 1018 997 #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta … … 1021 1000  (*RETURN*) #EQfetch 1022 1001 whd in match joint_classify; normalize nodelta 1023 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]);normalize nodelta1002 >EQfetch normalize nodelta 1024 1003 cases (eval_return_ok … good … EQfetch EQeval) #is_ret 1025 1004 * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
Note: See TracChangeset
for help on using the changeset viewer.