Changeset 2843
 Timestamp:
 Mar 11, 2013, 1:02:02 PM (4 years ago)
 Location:
 src
 Files:

 7 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTLToERTLptr.ma
r2820 r2843 100 100  * #called #args #dest whd in match translate_step; normalize nodelta whd 101 101 [ #l' %{I} %{I} %{I} % 102  #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 % 102  #r #l' whd %{I} % 103 [2: whd %{I} whd in match step_forall_registers; normalize nodelta 104 whd in match step_registers; whd in match get_used_registers_from_step; 105 normalize nodelta normalize cases(\fst called) [#r1  #b1] 106 normalize nodelta cases(\snd called) [1,3: #r2 *: #b2 ] 107 normalize nodelta /2 by All_mp, I/ % // [1,3,4: %2 % %] 108 % [%2 %2 % %] % 109  % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 % 110 ] 103 111 ] 104 112  #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 % … … 111 119 qed. 112 120 121 113 122 definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝ 114 123 b_graph_transform_program ERTL ERTLptr translate_data. 
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 
src/ERTL/ERTLtoERTLptrUtils.ma
r2801 r2843 29 29 30 30 definition sigma_map ≝ block → label → option label. 31 definition lbl_funct ≝ block → label → option(list label).32 definition regs_funct ≝ block → label → option(list register).31 definition lbl_funct ≝ block → label → (list label). 32 definition regs_funct ≝ block → label → (list register). 33 33 34 34 (*TO BE MOVED*) … … 49 49 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl); 50 50 !〈res,s〉 ← find ?? (joint_if_code … fn) 51 (λlbl.λ_. match f_lbls bl lbl with 52 [None ⇒ false 53 Some lbls ⇒ 54 match split_on_last … lbls with 55 [None ⇒ eq_identifier … searched lbl 56 Some x ⇒ eq_identifier … searched (\snd x) 57 ] 51 (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with 52 [None ⇒ eq_identifier … searched lbl 53 Some x ⇒ eq_identifier … searched (\snd x) 58 54 ]); 59 55 return res. … … 682 678 ∀globals : list ident.∀fn,f_regs,r. 683 679 (∀lbl. code_has_label p globals (joint_if_code … fn) lbl → 684 opt_All … (λl.¬(bool_to_Prop (r ∈ l))) (f_regs lbl)) →680 ¬(bool_to_Prop (r ∈ (f_regs lbl)))) → 685 681 ¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))). 686 682 #p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta … … 689 685 lapply(H lbl ?) 690 686 [whd in match code_has_label; whd in match code_has_point; normalize nodelta 691 whd in match (stmt_at ????); >EQstmt @I] cases(f_regs lbl) 692 [ #_ @notb_Prop % assumption] 693 #l whd in ⊢ (% → ?); normalize nodelta * #H1 @notb_elim @if_elim [2: #_ @I] #ABS 687 whd in match (stmt_at ????); >EQstmt @I] 688 * #H1 @notb_elim @if_elim [2: #_ @I] #ABS 694 689 lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS'' 695 [ @H1 @Exists_memb lapply ABS'' elim l[ *] #hd #tl #IH whd in ⊢ (% → %);690 [ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %); 696 691 * [ #EQ >EQ % %] #H %2 @IH @H 697 692  @IH @list_as_set_mem assumption … … 699 694 qed. 700 695 696 lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a. 697 #A #l1 elim l1 [#l2 #a *] #hd #tl #IH * 698 [#a normalize * [#H % assumption  #H %2 >append_nil assumption]] 699 #hd1 #tl1 #a normalize * [#H % assumption  #H %2 @IH assumption] 700 qed. 701 702 lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a. 703 #A #l1 #l2 lapply l1 l1 elim l2 [#l1 #a *] #hd #tl #IH * 704 [#a normalize * [#H %1 assumption #H %2 assumption]] 705 #hd1 #tl1 #a normalize * 706 [ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 // 707  #H %2 >append_cons @IH assumption] 708 qed. 709 710 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A. 711 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2. 712 #A #P #l1 elim l1 713 [ #l2 change with l2 in ⊢ (???% → ?); #H % //] 714 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?); 715 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % // 716 qed. 717 718 include alias "common/PositiveMap.ma". 719 720 lemma added_register_pm : ∀A,B. ∀m : positive_map A. 721 ∀f : Pos → list B.∀b. 722 let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in 723 All B (λx.x≠b) added → 724 (∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)). 725 #A #B #m #f #b normalize nodelta @pm_fold_ind 726 [ #_ #i normalize * #H @⊥ @H % 727  #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p) 728 [1,3: #EQ destruct(EQ) #_ cases(append_All … H3) // 729 *: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2 730 cases(append_All … H3) // 731 ] 732 ] 733 qed. 734 735 lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 736 decidable (In A l a). 737 #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC) 738 [ #H % %2 assumption  * #H cases (DEC hd) 739 [ #H1 %1 %1 assumption  * #H1 %2 % * [ #H2 @H1 assumption  #H2 @H assumption]] 740 qed. 741 742 lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l. 743 #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption] 744 % #H1 @H % >H1 % 745 qed. 746 747 lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a. 748 #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % * 749 [ #H3 @H1 >H3 %  cases(IH a H2) #H3 #H4 @H3 assumption] 750 qed. 751 752 lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A. 753 ∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) → 754 let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in 755 ∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b. 756 #tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta 757 #H #H1 758 cases(decidable_In ? (foldi A (list B) tag 759 (λl.λ_.λacc.(f l)@acc) 760 (an_id_map tag A m) []) b (DEC b)) [//] 761 #H3 @⊥ lapply(In_all ??? H3) H3 #H3 762 lapply(added_register_pm ?? m ?? H3 i ?) 763 [cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct] 764 lapply H1 elim (f ?) [*] #hd #tl #IH * [#EQ * >EQ * #H4 #_ @H4 %] 765 #H4 * #_ @IH assumption 766 qed. 767 768 lemma in_added_registers : ∀p : graph_params. 769 ∀globals : list ident.∀fn,f_regs,r. 770 ∀lbl.code_has_label p globals (joint_if_code … fn) lbl → 771 In ? (f_regs lbl) r → 772 In ? (added_registers p globals fn f_regs) r. 773 #p #globals #fn #f_regs #r #lbl whd in match code_has_label; 774 whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); 775 inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_ 776 #H @(added_register_aux … EQstmt H) 777 * #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % %  * #H1 %2 % #EQ destruct @H1 %] 778 qed. 779 701 780 702 781 include alias "basics/lists/listb.ma". 703 782 704 check eval_seq_no_pc 705 706 xxxxxxxxxxxxxxxxxxxxxxxx 783 (* 784 definition get_internal_function_from_ident : 785 ∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals). 786 ident → option (joint_closed_internal_function p globals) ≝ 787 λp,globals,ge,id. 788 ! bl ← (find_symbol (joint_function p globals) ge id); 789 ! bl' ← (code_block_of_block bl); 790 ! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl'); 791 return fn. 792 793 lemma get_internal_function_from_ident_ok : 794 ∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals). 795 ∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 → 796 get_internal_function_from_ident p globals ge f= return fn. 797 #p #globals #ge #bl #f #fn #EQf 798 @('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function; 799 normalize nodelta #H lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) H 800 #f2 #EQf2 #H @('bind_inversion H) H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?); 801 #EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta 802 >(symbol_of_block_rev … EQf2) >m_return_bind 803 cut(code_block_of_block bl = return bl) 804 [ whd in match code_block_of_block; normalize nodelta @match_reg_elim 805 [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl 806 >m_return_bind >EQf % 807 qed. 808 *) 707 809 708 810 lemma eval_seq_no_pc_no_call_ok : … … 712 814 ∀stack_size. 713 815 ∀bl.∀id. 714 ∀seq. 715 (∀fn : joint_closed_internal_function ERTL (prog_var_names … prog). 716 ∀l. code_has_label … (joint_if_code … fn) l → 717 opt_All … 718 (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs))) 719 (get_used_registers_from_seq … (functs … ERTL) seq))) 720 (f_regs bl l)) → 816 ∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq. 817 (∀l. code_has_label … (joint_if_code … fn) l → 818 (All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l)))) 819 (get_used_registers_from_seq … (functs … ERTL) seq))) → 721 820 preserving1 ?? res_preserve1 ???? 722 821 (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) … … 729 828 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) 730 829 id (seq_embed … seq)). 731 #prog #f_lbls #f_regs #stack_size #bl #f # seq #fresh_regs830 #prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs 732 831 cases seq in fresh_regs; 733 832 [ #c #_ #st @mfr_return1 … … 738 837 * [#r1  #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs 739 838 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 740 cases(f_regs bl lbl) [ #_ @I] #labswhd in ⊢ (% → %); * #H #_ @Prop_notb @H839 whd in ⊢ (% → %); * #H #_ @Prop_notb @H 741 840   #regs @mfr_return_eq1 % 742 841 ] … … 744 843 [2: @pop_ok  745 844  * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1 746 [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl 747 lapply(fresh_regs lbl Hlbl) 748 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H  749  #regs @mfr_return_eq1 % 845 [2: @ps_reg_store_ok 846 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 847 whd in ⊢ (% → %); * #H #_ @Prop_notb @H 750 848 ] 751 849 ] … … 769 867 change with (sigma_beval prog f_lbls (BVptr …)) 770 868 in ⊢ (???????(?????%?)?); 771 @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 772 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H  869 @ps_reg_store_ok 870 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 871 whd in ⊢ (% → %); * #H #_ @Prop_notb @H  773 872  #regs @mfr_return_eq1 % 774 873 ] … … 781 880 in ⊢ (???????(?????%?)?); 782 881 @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 783 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ whd in ⊢ (% → ?); * #H 784 #_ @Prop_notb @H 882 whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H  785 883  #regs @mfr_return_eq1 % 786 884 ] … … 798 896  whd in match acca_store; normalize nodelta @mfr_bind1 799 897 [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl 800 lapply(fresh_regs lbl Hlbl) 801 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H  898 lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H  802 899  #regs @mfr_return_eq1 % 803 900 ] … … 805 902 [2: whd in match sigma_state; normalize nodelta 806 903 @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl 807 lapply(fresh_regs lbl Hlbl) 808 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ * #H #_ 809 @Prop_notb @H  904 lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H  810 905  #regs @mfr_return_eq1 % 811 906 ] … … 823 918 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 824 919 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 825 cases(f_regs bl lbl) [ #_ @I] #labswhd in ⊢ (% → %); * #H #_ @Prop_notb @H 920 whd in ⊢ (% → %); * #H #_ @Prop_notb @H  826 921  #regs @mfr_return_eq1 % 827 922 ] … … 837 932 [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl))) 838 933  whd in match acca_store; normalize nodelta @mfr_bind1 839 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 934 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 840 935 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 841 cases(f_regs bl lbl) [ #_ @I] #labswhd in ⊢ (% → %); * #H #_ @Prop_notb @H 936 whd in ⊢ (% → %); * #H #_ @Prop_notb @H  842 937  #regs @mfr_return_eq1 % 843 938 ] … … 860 955  #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 861 956 [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 862 863 cases(f_regs bl lbl) [ #_ @I] #labswhd in ⊢ (% → %); * #H #_ @Prop_notb @H 957 @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 958 whd in ⊢ (% → %); * #H #_ @Prop_notb @H  864 959  #regs @mfr_return_eq1 % 865 960 ] … … 898 993 change with (sigma_beval prog f_lbls (BVByte ?)) 899 994 in ⊢ (???????(??%?)?); 900 @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl) 901 cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H 902  995 @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl 996 lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H  903 997  #regs @mfr_return_eq1 % 904 998 ] 905 ] 999 ] 906 1000 ] 907 1001 ] 1002 #regs @mfr_return_eq1 % 908 1003 qed. 909 1004 … … 921 1016 #H @('bind_inversion H) H * #lbl2' #stmt2 #H2 922 1017 whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1) 923 lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta [*] 924 * 1018 lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta 925 1019 [ normalize nodelta @eq_identifier_elim #EQ1 * 926 1020 @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % … … 1189 1283 qed. 1190 1284 1191 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.1192 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.1193 #A #P #l1 elim l11194 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]1195 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);1196 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //1197 qed.1198 1199 1285 include alias "common/Identifiers.ma". 1200 1286 … … 1204 1290 ∀f_bl_r. 1205 1291 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 1206 translate_dataprog f_bl_r f_lbls f_regs →1292 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 1207 1293 ∀id,fn,bl,pt,stmt. 1208 1294 fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 → 1209 1295 stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 1210 f_lbls bl pt = return [ ] → get_sigma prog f_lbls bl pt = return pt.1296 f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt. 1211 1297 #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels 1212 1298 cases(b_graph_transform_program_fetch_internal_function … good … EQfn) 1213 1299 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) 1214 1300 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_ 1215 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) H * #lbls * #regs ** >EQlabels1216 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta 1217 [3: * 2: * [#lbl  *] #EQstmt * #bl * whd in ⊢ (% → ?); cases regs in EQregs; 1218 [2,4: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (%→?);1219 * #pref * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)1220 whd in ⊢ (% → ?); #EQt_stmt1301 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) H cases stmt in EQstmt; 1302 [3: * 1303 2: * [#lbl  *] #EQstmt normalize nodelta * #bl * whd in ⊢ (% → ?); 1304 inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta 1305 #EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?); 1306 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt 1221 1307  * [#c  * [#c_id#c_ptr] #args #dest  #r #lbl  #seq ] #nxt #EQstmt 1222 1308 whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?); 1223 cases regs in EQregs;normalize nodelta1224 [2,4,5,8,10: [1,2,4,5: #x #y] #_ *6: #r * [2: #x #y] ]1225 #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);1309 inversion(f_regs ??) normalize nodelta 1310 [2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] *6: #r * [2: #x #y] ] 1311 [1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?); 1226 1312 * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?); 1227 1313 [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * 1228 1314 #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 1229 1315 whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) 1230 whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); 1231 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%); 1232 destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ) 1233 whd in ⊢ (% → ?); * #_ #EQ destruct(EQ) 1234 ] whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind 1316 whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0; 1317 #e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%); 1318 destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt 1319 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 1320 * #_ #EQ destruct(EQ) ] 1321 whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind 1235 1322 >EQfn >m_return_bind inversion(find ????) 1236 1323 [1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels 1237 1324 normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * *: * #H #_ @H %]] 1238 1325 * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) 1239 inversion(f_lbls ??) [1,3,5,7,9,11: #_ *] #l @(list_elim_left … l …) 1240 normalize nodelta [1,3,5,7,9,11: #_ @eq_identifier_elim 1241 [1,3,5,7,9,11: #EQ destruct(EQ) #_ % *: #_ *]] 1242 #last #pre #_ #EQlbl >split_on_last_append normalize nodelta @eq_identifier_elim 1326 inversion(f_lbls ??) 1327 [1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %] 1328 #lb #l @(list_elim_left … l …) normalize nodelta 1329 [1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim 1330 [1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ *: #_ *] 1331 lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H 1332 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 1333 whd in match code_has_point; normalize nodelta >EQstmt @I ] 1334 #last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last) 1335 normalize nodelta @eq_identifier_elim 1243 1336 [2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥ 1244 lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); #H lapply(append_All … H) H1337 lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) H 1245 1338 * #_ whd in ⊢ (% → ?); *** #H #_ #_ @H H @(code_is_in_universe … (pi2 ?? fn)) 1246 1339 whd in match code_has_label; whd in match code_has_point; normalize nodelta … … 1261 1354 qed. 1262 1355 1356 1263 1357 lemma get_sigma_last : 1264 1358 ∀prog : ertl_program. … … 1266 1360 ∀f_bl_r. 1267 1361 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 1268 translate_dataprog f_bl_r f_lbls f_regs →1362 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 1269 1363 ∀id,fn,bl,pt,stmt,pre,last. 1270 1364 fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 → 1271 1365 stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 1272 f_lbls bl pt = return (pre@[last])→ get_sigma prog f_lbls bl last = return pt.1366 f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt. 1273 1367 #prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last 1274 1368 #EQfn #EQstmt #EQlabels 1275 1369 cases(b_graph_transform_program_fetch_internal_function … good … EQfn) 1276 1370 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) 1277 [2 ,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs1278 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) H * #lbls * #regs ** >EQlabels1279 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregscases stmt in EQstmt; normalize nodelta1371 [2: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs 1372 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) H normalize nodelta 1373 cases stmt in EQstmt; normalize nodelta 1280 1374 [3: * 1281 1375 2: * [#lbl  *] #EQstmt whd in ⊢ (%→ ?); * #bl * 1282 1376 *: * [#c  * [ #c_id  #c_ptr] #args #dest  #r #lbl  #seq ] #nxt #EQstmt 1283 1377 >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl * 1284 ] whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta 1285 [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y] #_ *10: #r #tl] #EQregs 1378 ] 1379 whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta 1380 [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *10: #r #tl #_] #EQregs 1286 1381 [ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs] 1287 1382 #EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid ***: * #l1 * #mid1 * #mid2 * #l2 ***] 1288 1383 #EQmid1 whd in ⊢ (% → ?); 1289 [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) 1384 [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) 1290 1385 [3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ) ] 1291 whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ @(append_absurd ??? e0)]1386 whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)] 1292 1387 * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_ 1293 1388 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); … … 1304 1399 >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 1305 1400 inversion(find ????) 1306 [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) > EQlabels1401 [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0 1307 1402 normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H 1308 whd in EQmid1 : (??%%); destruct(EQmid1) @(last_append_eq ????? e1)]1403 >(last_append_eq ????? EQlabels) % ] 1309 1404 * #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) 1310 inversion(f_lbls ??) [ #_ normalize nodelta *] #labels 1311 @(list_elim_left … labels …) labels normalize nodelta 1312 [ #EQl @eq_identifier_elim [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl 1313 lapply(fresh_labs pt) >EQlabels <e0 whd in ⊢ (% → ?); 1314 #H lapply(append_All … H) H * #_ whd in ⊢ (% → ?); *** #H #_ #_ #_ @⊥ @H 1315 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 1405 inversion(f_lbls ??) 1406 [ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) 1407 lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥ 1408 lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #H #_ #_ @H H 1409 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 1316 1410 whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); 1317 1411 >(find_lookup ?????? EQfind) @I 1318  #last1 #pre1 #_ #EQl >split_on_last_append normalize nodelta @eq_identifier_elim 1319 [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl #_ lapply pp_labs 1320 whd in match partial_partition; normalize nodelta * #_ #H lapply(H lbl pt) 1321 >EQl <e0 in EQlabels; #EQlabels >EQlabels whd in ⊢ (% → ?); H #H 1322 >(H last1 ? ?) [%] >(memb_append_l2 ? last1 ? [last1] ?) /2 by / 1323 ] 1324 qed. 1412 ] 1413 #lb #labels #_ @(list_elim_left … (labels) …) labels normalize nodelta 1414 [2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ] 1415 normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_ 1416 lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) 1417 lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H 1418 lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl 1419 #H [ >(H last1 ? ?)  >(H lb ? ?) ] [1,4: % 1420 6: whd in match (memb ???); @if_elim [#_ @I] 1421 #H lapply(Prop_notb ? H) * H #H @⊥ @H cases lb #x normalize 1422 @if_elim [#_ %] #H lapply(Prop_notb ? H) * H #H @H >(eqb_n_n x) % 1423 5: >(memb_append_l2 ? lb ? [lb] ?) /2 by / 1424 *: >(memb_append_l2 ? last1 ? [last1] ?) /2 by / 1425 @Exists_memb %2 elim pre [ % %  #hd #tl #IH %2 @IH] 1426 ] 1427 qed. 1428 1325 1429 1326 1430 lemma fetch_call_commute : … … 1330 1434 ∀f_bl_r. 1331 1435 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 1332 translate_dataprog f_bl_r f_lbls f_regs →1436 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 1333 1437 ∀id,fn,c_id,c_args,c_dest,nxt,pc. 1334 1438 fetch_statement ERTL_semantics … … 1343 1447 cases(b_graph_transform_program_fetch_internal_function … good … EQfn) 1344 1448 #init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?) 1345 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs 1346 #_ #fresh_labs #_ #_ #_ #H cases(H … EQstmt) H #labels * #registers 1347 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %] 1348 whd in match translate_step; 1349 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?); 1350 cases registers in EQregisters; registers normalize nodelta 1351 [2,3: [ #x #y] #_ *4: #r #tl] #EQregisters 1352 [ whd in ⊢ (% → ?); cases tl in EQregisters; tl [2: #x #y #_ *] normalize nodelta 1353 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); * 1354 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?); 1355 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?); 1449 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_ 1450 #_ #_ #_ #_ #_ #H cases(H … EQstmt) H #bl whd in ⊢ (% → ?); * 1451 >if_merge_right [2,4: %] whd in match translate_step; 1452 normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta 1453 [2,3:[ #x #y #_] #_ * 4: #r #tl #_ ] #EQregs 1454 [  cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ) 1455 whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?); 1456 [2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?); 1356 1457 * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 1357 1458 whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 * … … 1372 1473 [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption 1373 1474 #EQ destruct(EQ)] #_ normalize nodelta 1374 [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ labels)1475 [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ) 1375 1476 *: change with (pc_block pc) in match (pc_block ?); 1376 >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)1477 >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0) 1377 1478 ] >m_return_bind normalize nodelta >pc_of_point_of_pc % 1378 1479 *: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind … … 1387 1488 ∀ f_lbls,f_regs.∀f_bl_r. 1388 1489 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics 1389 translate_dataprog f_bl_r f_lbls f_regs →1490 (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 1390 1491 ∀pc,lb. 1391 1492 next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog) … … 1603 1704 ] 1604 1705 qed. 1706 1707 
src/common/ExtraIdentifiers.ma
r2801 r2843 241 241 qed. 242 242 243 243 lemma map_opt_none : ∀A,B.∀m : positive_map A. 244 map_opt A B (λx.None ?) m = pm_leaf B. 245 #A #B #m elim m [%] #opt_a #l #r #EQ1 #EQ2 cases opt_a [2: #a] normalize 246 >EQ1 >EQ2 % 247 qed. 248 249 lemma set_minus_add :∀tag,A,B.∀a:identifier_map tag A.∀b:identifier_map tag B. 250 ∀i,v.i∈b→ (add tag A a i v)∖b = a ∖ b. 251 #tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) [ #_ *] 252 #v1 #EQv1 #_ @eq_f lapply EQv1 EQv1 lapply v1 v1 lapply v v lapply b b 253 lapply i i elim a 254 [ #i elim i [ * [2: #opt_v #l #r] #v1 #v2 normalize #EQb destruct(EQb) %] 255 #i1 #IH * [2,4: #opt_v #l #r] #v1 #v2 normalize [3,4: #ABS destruct(ABS)] 256 cases opt_v [2,4: #v'] normalize nodelta #EQb >(IH … EQb) >map_opt_none % 257  #opt_v #l #r #IHl #IHr #i * [#v1 #v2 normalize #EQ destruct] #opt_v1 #l1 #r1 258 #c1 #c2 normalize cases i [2,3: #x] normalize [3: #EQ destruct] normalize nodelta 259 [ %] #EQc2 cases opt_v [2,4: #c3] normalize cases opt_v1 [2,4,6,8: #c4] normalize 260 [1,3,4,5,7: >(IHr … EQc2) inversion(merge A B A ? l l1) // 261 [2: #opt_v4 #l4 #r4 #_ #_] #EQ <EQ >(IHl … EQc2) // 262 *: >(IHl … EQc2) // 263 ] 264 qed. 265 
src/joint/Joint.ma
r2824 r2843 190 190 match step with 191 191 [ COST_LABEL c ⇒ [ ] 192  CALL id args dest ⇒ (f_call_args … functs args) @ (f_call_dest … functs dest) 192  CALL id args dest ⇒ 193 let r_id ≝ match id with 194 [ inl _ ⇒ [ ] 195  inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @ 196 ((dph_args … functs) (\snd ptr)) 197 ] in 198 r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest) 193 199  COND r lbl ⇒ acc_a_regs … functs r 194 200  step_seq s ⇒ get_used_registers_from_seq … functs s 
src/joint/TranslateUtils.ma
r2823 r2843 606 606 definition added_registers : 607 607 ∀p : graph_params.∀g. 608 joint_internal_function p g → (label → option (list register)) → list register ≝608 joint_internal_function p g → (label → list register) → list register ≝ 609 609 λp,g,def,f_regs. 610 let f ≝ λlbl : label.λ_.λacc. 611 match f_regs lbl with [ None ⇒ acc  Some regs ⇒ regs@acc ] in 610 let f ≝ λlbl : label.λ_.λacc.(f_regs lbl)@acc in 612 611 foldi … f (joint_if_code p g def) [ ]. 613 612 … … 615 614 ∀p,g,def,f_regs. 616 615 ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s → 617 opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).616 (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs)) (f_regs l)). 618 617 619 618 (*(* translation without register allocation (more or less an alias) *) 
src/joint/semanticsUtils.ma
r2816 r2843 633 633  % [2: % [2: % [% %]]  skip] @(multi_fetch_ok … H3 … EQstmt_at) ] 634 634 qed. 635 636 lemma b_graph_transform_program_fetch_statement_plus : 637 ∀src,dst:sem_graph_params. 638 ∀data : ∀globals.joint_closed_internal_function src globals → 639 bound_b_graph_translate_data src dst globals. 640 ∀prog_in : joint_program src. 641 ∀init_regs : block → list register. 642 ∀f_lbls : block → label → list label. 643 ∀f_regs : block → label → list register. 644 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs → 645 let prog_out ≝ b_graph_transform_program … data prog_in in 646 let src_genv ≝ globalenv_noinit ? prog_in in 647 let dst_genv ≝ globalenv_noinit ? prog_out in 648 ∀pc,id,def_in,s. 649 fetch_statement … src_genv pc = return 〈id, def_in, s〉 → 650 ∃init_data,def_out. 651 let bl ≝ pc_block pc in 652 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧ 653 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧ 654 let l ≝ point_of_pc dst pc in 655 ∃lbls,regs. 656 f_lbls bl l = lbls ∧ 657 f_regs bl l = regs ∧ 658 joint_if_entry … def_out = joint_if_entry … def_in ∧ 659 partial_partition … (f_lbls bl) ∧ 660 partial_partition … (f_regs bl) ∧ 661 (∀l.All … 662 (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧ 663 fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧ 664 (∀l.All … 665 (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧ 666 fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧ 667 match s with 668 [ sequential s' nxt ⇒ 669 let block ≝ 670 if eq_identifier … (joint_if_entry … def_in) l then 671 append_seq_list … (f_step … init_data l s') (added_prologue … init_data) 672 else 673 f_step … init_data l s' in 674 l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out 675  final s' ⇒ 676 l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out 677  FCOND abs _ _ _ ⇒ Ⓧabs 678 ]. 679 #src #dst #data #prog_in 680 #init_regs #f_lbls #f_regs #props 681 #pc #id #def_in #s 682 #H @('bind_inversion H) * #id' #def_in' H 683 #EQfif 684 #H @('bind_inversion H) H #s 685 #H lapply (opt_eq_from_res ???? H) H 686 #EQstmt_at whd in ⊢ (??%%→?); #EQ destruct 687 cases (b_graph_transform_program_fetch_internal_function … props … EQfif) 688 #a * #b ** #H1 #H2 #H3 %{a} %{b} % 689 [ %{H1 H2} 690  % 691 [2: 692 % 693 [2: % 694 [% 695 [% 696 [% 697 [% 698 [% 699 [% 700 % 701  @(entry_eq … H3) 702 ] 703  @(partition_lbls … H3) 704 ] 705  @(partition_regs … H3) 706 ] 707  @(freshness_lbls … H3) 708 ] 709  @(freshness_regs … H3) 710 ] 711  @(multi_fetch_ok … H3 … EQstmt_at) 712 ] 713  714 ] 715  716 ] 717 ] 718 qed.
Note: See TracChangeset
for help on using the changeset viewer.