Changeset 2556
- Timestamp:
- Dec 14, 2012, 2:54:06 PM (8 years ago)
- Location:
- src/joint
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Traces.ma
r2553 r2556 5 5 { globals: list ident 6 6 ; sparams:> sem_params 7 ; exit: program_counter8 7 ; ev_genv: genv sparams globals 9 8 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) … … 47 46 ≝ 48 47 λpars. 49 (* Invariant: a -1 block is unused in common/Globalenvs *)50 let b ≝ mk_block Code (-1) in51 let ptr ≝ mk_program_counter «b, refl …» one in52 48 let p ≝ prog pars in 53 49 mk_evaluation_params 54 50 (prog_var_names … p) 55 51 (prog_spars pars) 56 ptr57 52 (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars)) 58 53 (* (prog_io pars) *). … … 76 71 let m ≝ alloc_mem … p in 77 72 let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in 78 let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in79 let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in80 73 let spp : xpointer ≝ 81 74 «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)), … … 84 77 let main ≝ prog_main … p in 85 78 let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in 86 (* use exit sem_globalsas ra and call_dest_for_main as dest *)87 let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals)in88 ! st0 ''← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;89 let st _pc0 ≝ mk_state_pc ? st0'' dummy_pcin90 ! bl ← block_of_call … ge (inl … main) st _pc0;79 (* use exit_pc as ra and call_dest_for_main as dest *) 80 let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in 81 ! st0_no_pc ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ; 82 let st0'' ≝ set_no_pc … st0_no_pc st0' in 83 ! bl ← block_of_call … ge (inl … main) st0''; 91 84 ! 〈i, fn〉 ← fetch_function … ge bl ; 92 85 match fn with 93 86 [ Internal ifn ⇒ 94 ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st _pc0;87 ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ; 95 88 let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in 96 return mk_state_pc … st' pc' 89 return mk_state_pc … st' pc' exit_pc 97 90 | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 98 91 ]. … … 231 224 match \snd x with 232 225 [ sequential s next ⇒ 226 last_pop … s2 = pc … s1 ∧ 233 227 pc … s2 = succ_pc p (pc … s1) next 234 228 | _ ⇒ False (* never happens *) … … 374 368 ]) 375 369 (* as_after_return ≝ *) (joint_after_ret p) 376 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) (exit p)s ≠ None ?)370 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) exit_pc s ≠ None ?) 377 371 (* as_call_ident ≝ *) (joint_call_ident p) 378 372 (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). -
src/joint/lineariseProof.ma
r2555 r2556 627 627 #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. 628 628 629 lemma sigma_pc_irr : 630 ∀p,p',graph_prog,sigma,pc1,pc2,prf1,prf2. 631 pc1 = pc2 → 632 sigma_pc p p' graph_prog sigma pc1 prf1 = 633 sigma_pc p p' graph_prog sigma pc2 prf2. 634 #p #p' #graph_prog #sigma #pc1 #pc2 #prf1 #prf2 635 #EQ destruct(EQ) % qed. 636 629 637 definition well_formed_state_pc : 630 638 ∀p,p',graph_prog,sigma. … … 632 640 state_pc (make_sem_graph_params p p') → Prop ≝ 633 641 λp,p',prog,sigma,gsss,st. 634 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st. 642 well_formed_pc p p' prog sigma (last_pop … st) ∧ 643 well_formed_pc p p' prog sigma (pc … st) ∧ 644 well_formed_state … gsss st. 635 645 636 646 definition sigma_state_pc : … … 646 656 ≝ 647 657 λp,p',graph_prog,sigma,gsss,s,prf. 648 let pc' ≝ sigma_pc … (proj1 … prf) in 658 let last_pop' ≝ sigma_pc … (proj1 … (proj1 … prf)) in 659 let pc' ≝ sigma_pc … (proj2 … (proj1 … prf)) in 649 660 let st' ≝ sigma_state … (proj2 … prf) in 650 mk_state_pc ? st' pc' .661 mk_state_pc ? st' pc' last_pop'. 651 662 (* 652 663 definition sigma_function_name : … … 660 671 ∀M : MonadProps.∀X,Y,f,l. 661 672 All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. 662 cases daemon qed. 673 #M #X #Y #f #l elim l -l 674 [ * %{[ ]} % 675 | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ' 676 %{(y :: ys)} 677 change with (! y ← ? ; ? = ?) 678 >EQ >m_return_bind 679 change with (! acc ← m_list_map ????? ; ? = ?) >EQ' 680 @m_return_bind 681 qed. 663 682 664 683 definition helper_def_store__commute : … … 717 736 (λr.pair_reg_move_ ? ? (p' ?) r mv) 718 737 (λr.pair_reg_move_ ? ? (p' ?) r mv) 719 ; allocate_locals_ commute :738 ; allocate_locals__commute : 720 739 ∀loc, r1, prf1. ∃ prf2. 721 740 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = … … 724 743 ∀dest,fl. 725 744 preserving … res_preserve … 726 (λst : state_pc ?.λprf. 727 mk_state_pc … 728 (sigma_state … gsss st (proj2 ?? prf)) 729 (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf))) 745 (sigma_state_pc … gsss) 730 746 (sigma_state … gsss) 731 747 (save_frame ?? (p' ?) fl dest) … … 776 792 preserving … res_preserve … 777 793 (sigma_state … gsss) 778 (λst : state_pc ?.λprf. 779 mk_state_pc … 780 (sigma_state … gsss st (proj2 ?? prf)) 781 (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf))) 794 (sigma_state_pc … gsss) 782 795 (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 783 796 curr_id curr_fn) … … 785 798 curr_id (\fst (linearise_int_fun … curr_fn))) 786 799 }. 800 801 lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r. 802 well_formed_state p p' graph_prog sigma gss st → 803 well_formed_regs … gss r → 804 well_formed_state … gss (set_regs … r st). 805 #p #p' #graph_prog #sigma #gss #st #r 806 *** #H1 #H2 #_ #H4 #H3 807 %{H4} %{H3} %{H2} @H1 808 qed. 809 810 lemma allocate_locals_def : 811 ∀p,F,p',loc,locs,st. 812 allocate_locals p F p' (loc::locs) st = 813 (let st' ≝ allocate_locals p F p' locs st in 814 set_regs … (allocate_locals_ p F p' loc (regs … st')) st'). 815 #p #F #p' #loc #locs #st % qed. 816 817 lemma allocate_locals_commute : 818 ∀p,p',graph_prog,sigma. 819 ∀gss : good_state_sigma p p' graph_prog sigma. 820 ∀locs, st1, prf1. ∃ prf2. 821 allocate_locals ? ? (p' ?) locs (sigma_state … gss st1 prf1) = 822 sigma_state … gss (allocate_locals ? ? (p' ?) locs st1) prf2. 823 #p #p' #gp #sigma #gss #locs elim locs -locs 824 [ #st1 #prf1 %{prf1} % ] 825 #loc #tl #IH #st1 #prf1 826 letin st2 ≝ (sigma_state … st1 prf1) 827 cases (IH st1 prf1) 828 letin st1' ≝ (allocate_locals ??? tl st1) 829 letin st2' ≝ (allocate_locals ??? tl st2) 830 #prf' #EQ' 831 cases (allocate_locals__commute … gss loc (regs … st1') ?) 832 [2: @hide_prf cases prf' ** // ] 833 #prf'' #EQ'' 834 % [ @hide_prf @wf_set_regs assumption ] 835 change with (set_regs ? (allocate_locals_ ??? loc (regs ? st1')) st1') 836 in match (allocate_locals ??? (loc::tl) st1); 837 change with (set_regs ? (allocate_locals_ ??? loc (regs ? st2')) st2') 838 in match (allocate_locals ??? (loc::tl) st2); 839 >EQ' >EQ'' % 840 qed. 787 841 788 842 lemma store_commute : … … 1557 1611 (* call_rel ≝ *) (λs1,s2. 1558 1612 ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1. 1559 pc ? s2 = sigma_pc … (pc ? s1) (proj 1 … prf))1613 pc ? s2 = sigma_pc … (pc ? s1) (proj2 … (proj1 … prf))) 1560 1614 (* sim_final ≝ *) ?. 1561 1615 #st1 #st2 * #prf #EQ2 … … 1563 1617 >EQ2 1564 1618 whd in ⊢ (%→%); 1565 whd in match (exit ?);1566 letin exit_pc ≝ (mk_program_counter «mk_block Code (-1), refl …» one)1567 1619 #H lapply (opt_to_opt_safe … H) 1568 1620 @opt_safe_elim -H #res #_ whd in match is_final; normalize nodelta … … 1570 1622 #H @('bind_inversion H) -H 1571 1623 ** #id #int_f #stmt 1572 #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj 1 … prf) stmt_spec)1624 #stmt_spec cases (fetch_statement_sigma_commute ???????? good (proj2 … (proj1 … prf)) stmt_spec) 1573 1625 cases stmt in stmt_spec; -stmt normalize nodelta 1574 1626 [1,3: [ #a #b #_| #a #b #c #d #e] #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] … … 1598 1650 [ #st #prf @mfr_bind [3: @pop_frame_commute |*:] 1599 1651 #st' #prf' @eq_program_counter_elim 1600 [ #EQ_pc >(sigma_pc_exit … EQ_pc) normalize nodelta 1652 [ #EQ_pc normalize nodelta 1653 change with (sigma_pc ??????) in match (pc ??); 1654 >(sigma_pc_exit … EQ_pc) normalize nodelta 1601 1655 @mfr_bind [3: @read_result_commute |*:] 1602 1656 #lbv #prf_lbv @opt_safe_elim #lbv' #EQ_lbv' … … 1641 1695 qed. 1642 1696 1697 lemma as_label_sigma_commute : 1698 ∀p,p',graph_prog,stack_sizes,sigma,gss.good_sigma p graph_prog sigma → 1699 ∀st,prf. 1700 as_label (lin_abstract_status p p' (linearise … graph_prog) stack_sizes) 1701 (sigma_state_pc p p' graph_prog sigma gss st prf) = 1702 as_label (graph_abstract_status p p' graph_prog stack_sizes) st. 1703 #p #p' #graph_prog #stack_sizes #sigma #gss #good * #st #pc #popped 1704 ** #prf1 #prf2 #prf3 1705 change with (as_label_of_pc ?? = as_label_of_pc ??) 1706 change with (sigma_pc ??????) in match (as_pc_of ??); 1707 change with pc in match (as_pc_of ??); 1708 whd in match sigma_pc; normalize nodelta 1709 @opt_safe_elim #pc' 1710 whd in match sigma_pc_opt; normalize nodelta 1711 @eqZb_elim #Hbl normalize nodelta 1712 [ whd in ⊢ (??%%→??%%); #EQ destruct(EQ) 1713 whd in match fetch_statement; normalize nodelta 1714 >(fetch_internal_function_no_minus_one … graph_prog … Hbl) 1715 >(fetch_internal_function_no_minus_one … (linearise … graph_prog) … Hbl) % 1716 | #H @('bind_inversion H) * #i #f -H 1717 inversion (fetch_internal_function … (pc_block pc)) 1718 [2: #e #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 1719 * #i' #f' #EQfetch whd in ⊢ (??%%→?); #EQ destruct(EQ) 1720 #H @('bind_inversion H) #n #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) 1721 whd in ⊢ (??%%); 1722 whd in match fetch_statement; normalize nodelta >EQfetch 1723 >(fetch_internal_function_transf … graph_prog 1724 (λvars,fn.\fst (linearise_int_fun … fn)) … EQfetch) 1725 >m_return_bind >m_return_bind 1726 cases (good f) * #_ #all_labels_in #spec 1727 cases (spec … EQsigma) #s ** cases s -s 1728 [ * [#s|#a#lbl]#nxt|#s|*] normalize nodelta #EQstmt_at #_ 1729 [ * #EQstmt_at' #_ | * [ * #EQstmt_at' #_ | #EQstmt_at' ] | #EQstmt_at' ] 1730 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1731 >EQstmt_at >EQstmt_at' normalize nodelta % 1732 qed. 1733 1643 1734 lemma set_istack_sigma_commute : 1644 1735 ∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3. … … 1841 1932 λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉. 1842 1933 1843 lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r.1844 well_formed_state p p' graph_prog sigma gss st →1845 well_formed_regs … gss r →1846 well_formed_state … gss (set_regs … r st).1847 #p #p' #graph_prog #sigma #gss #st #r1848 *** #H1 #H2 #_ #H4 #H31849 %{H4} %{H3} %{H2} @H11850 qed.1851 1852 1934 lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is. 1853 1935 well_formed_state p p' graph_prog sigma gss st → … … 1907 1989 [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return 1908 1990 | (* MOVE *) #mv_sig #st #prf' 1909 @(mfr_bind … (sigma_regs … gss)) 1910 [ @pair_reg_move_commute 1911 | #r #prf @mfr_return @wf_set_regs assumption 1912 ] 1991 @mfr_bind [3: @pair_reg_move_commute |*:] 1992 #r #prf @mfr_return @wf_set_regs assumption 1913 1993 | (* POP *) 1914 1994 #a #st #prf … … 1922 2002 | (* PUSH *) 1923 2003 #a #st #prf 1924 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1925 [ @acca_arg_retrieve_commute 1926 | #bv #prf_bv 1927 @(mfr_bind … (sigma_is p p' graph_prog sigma)) 1928 [ @is_push_sigma_commute 1929 | #is #prf_is @mfr_return @wf_set_is assumption 1930 ] 1931 ] 2004 @mfr_bind [3: @acca_arg_retrieve_commute |*:] 2005 #bv #prf_bv 2006 @mfr_bind [3: @is_push_sigma_commute |*:] 2007 #is #prf_is @mfr_return @wf_set_is assumption 1932 2008 | (*C_ADDRESS*) 1933 2009 #sy … … 1954 2030 | (*C_OPACCS*) 1955 2031 #op #a #b #arg1 #arg2 #st #prf 1956 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1957 [ @acca_arg_retrieve_commute ] 2032 @mfr_bind [3: @acca_arg_retrieve_commute |*: ] 1958 2033 #bv1 #bv1_prf 1959 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1960 [ @accb_arg_retrieve_commute ] 2034 @mfr_bind [3: @accb_arg_retrieve_commute |*: ] 1961 2035 #bv2 #bv2_prf 1962 @(mfr_bind … (combine_strong … 1963 (sigma_beval p p' graph_prog sigma) 1964 (sigma_beval p p' graph_prog sigma))) 1965 [ @beopaccs_sigma_commute ] 2036 @mfr_bind [3: @beopaccs_sigma_commute |*: ] 1966 2037 * #res1 #res2 * #res1_prf #res2_prf 1967 2038 @(mfr_bind … (sigma_state … gss)) … … 1974 2045 | (*C_OP1*) 1975 2046 #op #a #arg #st #prf 1976 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1977 [ @acca_retrieve_commute ] 2047 @mfr_bind [3: @acca_retrieve_commute |*: ] 1978 2048 #bv #bv_prf 1979 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1980 [ @beop1_sigma_commute ] 2049 @mfr_bind [3: @beop1_sigma_commute |*: ] 1981 2050 #res #res_prf 1982 2051 @mfr_bind [3: @acca_store__commute |*: ] … … 1984 2053 | (*C_OP2*) 1985 2054 #op #a #arg1 #arg2 #st #prf 1986 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1987 [ @acca_arg_retrieve_commute ] 2055 @mfr_bind [3: @acca_arg_retrieve_commute |*: ] 1988 2056 #bv1 #bv1_prf 1989 @(mfr_bind … (sigma_beval p p' graph_prog sigma)) 1990 [ @snd_arg_retrieve_commute ] 2057 @mfr_bind [3: @snd_arg_retrieve_commute |*: ] 1991 2058 #bv2 #bv2_prf 1992 @mfr_bind 1993 [3: @beop2_sigma_commute |*: ] 2059 @mfr_bind [3: @beop2_sigma_commute |*: ] 1994 2060 * #res1 #carry' #res1_prf 1995 2061 @(mfr_bind … (sigma_state … gss)) … … 2044 2110 qed. 2045 2111 2046 lemma eval_seq_no_call_ no_goto_ok :2112 lemma eval_seq_no_call_ok : 2047 2113 ∀p,p',graph_prog. 2048 2114 let lin_prog ≝ linearise p graph_prog in 2049 2115 ∀stack_sizes. 2050 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 2116 ∀sigma.good_sigma p graph_prog sigma → 2117 ∀gss : good_state_sigma p p' graph_prog sigma. 2051 2118 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → 2052 2119 ∀prf : well_formed_state_pc … gss st. 2053 fetch_statement (make_sem_lin_params p p') … 2054 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) = 2055 return 〈f, \fst (linearise_int_fun … fn), 2056 sequential … (step_seq (mk_lin_params p) … stmt) it〉 → 2057 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 2058 f fn stmt st = return st' → 2059 let st_pc' ≝ mk_state_pc ? st' 2060 (succ_pc (make_sem_graph_params p p') … 2061 (pc … st) nxt) in 2062 ∀prf'. 2063 succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it = 2064 sigma_pc p p' graph_prog sigma 2065 (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' → 2066 ∃prf''. 2120 fetch_statement (make_sem_graph_params p p') … 2121 (globalenv_noinit ? graph_prog) (pc … st) = 2122 return 〈f, fn, sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 → 2123 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2124 return st' → 2125 ∃prf'. 2067 2126 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 2068 2127 (sigma_state_pc … gss st prf) 2069 (sigma_state_pc … gss st _pc' prf'').2128 (sigma_state_pc … gss st' prf'). 2070 2129 bool_to_Prop (taaf_non_empty … taf). 2071 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 2072 #prf #EQfetch' #EQeval #prf' #EQsucc_pc 2073 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)] 2074 #prf'' #EQeval' 2075 % [ @hide_prf % assumption ] 2076 %{(taaf_step … (taa_base …) …)} [3: % ] 2077 [ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 2130 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 2131 #prf #EQfetch 2132 whd in match eval_state; normalize nodelta >EQfetch 2133 >m_return_bind whd in match eval_statement_no_pc; 2134 whd in match eval_statement_advance; normalize nodelta 2135 @'bind_inversion #st_no_pc' #EQeval 2136 >no_call_advance [2: assumption] 2137 whd in ⊢ (??%%→?); #EQ destruct(EQ) 2138 cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) 2139 normalize nodelta #_ * #EQfetch' * 2140 #prf_nxt #nxt_spec 2141 lapply (err_eq_from_io ????? EQeval) -EQeval #EQeval 2142 cases (eval_seq_no_pc_sigma_commute … gss … (proj2 … prf) … EQeval) 2143 #st_no_pc_prf 2144 #EQeval' 2145 %{(hide_prf …)} [ %{st_no_pc_prf} %{prf_nxt} cases st in prf; -st #st #pc #popped ** // ] 2146 cases nxt_spec -nxt_spec 2147 [ #nxt_spec %{(taaf_step … (taa_base …) …) I} 2148 | * #nxt_spec #pc_of_label_spec %{(taaf_step … (taa_step … (taa_base …))…) I} 2149 ] 2150 [1,6: 2151 whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 2078 2152 whd in match joint_classify_step; normalize nodelta 2079 2153 >no_call_other try % assumption 2080 | whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind 2154 |2,5: 2155 whd whd in match eval_state; normalize nodelta 2156 change with (sigma_pc ??????) in match (pc ??); 2157 try >EQfetch' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2081 2158 whd in match eval_statement_no_pc; normalize nodelta 2082 >EQeval' >m_return_bind2159 try >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2083 2160 whd in match eval_statement_advance; normalize nodelta 2084 >no_call_advance [2: assumption ] 2085 whd in match (next ???); 2086 >EQsucc_pc % 2087 ] 2088 qed. 2089 2090 lemma eval_seq_no_call_goto_ok : 2091 ∀p,p',graph_prog. 2092 let lin_prog ≝ linearise p graph_prog in 2093 ∀stack_sizes. 2094 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 2095 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → 2096 ∀prf : well_formed_state_pc … gss st. 2097 fetch_statement (make_sem_lin_params p p') … 2098 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) = 2099 return 〈f, \fst (linearise_int_fun … fn), 2100 sequential … (step_seq (mk_lin_params p) … stmt) it〉 → 2101 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 2102 f fn stmt st = return st' → 2103 let st_pc' ≝ mk_state_pc ? st' 2104 (succ_pc (make_sem_graph_params p p') … 2105 (pc … st) nxt) in 2106 ∀prf'. 2107 fetch_statement (make_sem_lin_params p p') … 2108 (globalenv_noinit … lin_prog) 2109 (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = 2110 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → 2111 pc_of_label (make_sem_lin_params p p') ? 2112 (globalenv_noinit ? (linearise p … graph_prog)) 2113 (pc_block (pc … st)) 2114 nxt = return sigma_pc p p' graph_prog sigma 2115 (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' → 2116 ∃prf''. 2117 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 2118 (sigma_state_pc … gss st prf) 2119 (sigma_state_pc … gss st_pc' prf''). 2120 bool_to_Prop (taaf_non_empty … taf). 2121 #p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call 2122 #prf #EQfetch' #EQeval #prf' #EQsucc_pc #EQ_pc_of_label 2123 cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)] 2124 #prf'' #EQeval' 2125 % [ @hide_prf % assumption ] 2126 %{(taaf_step … (taa_step … (taa_base …)) …)} [7: % ] 2127 [4: whd whd in ⊢ (??%?); >EQfetch' normalize nodelta 2128 whd in match joint_classify_step; normalize nodelta 2129 >no_call_other try % assumption 2130 |3: whd whd in match eval_state; normalize nodelta >EQfetch' in ⊢ (??%?); 2131 >m_return_bind in ⊢ (??%?); 2132 whd in match eval_statement_no_pc; normalize nodelta 2133 >EQeval' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2161 >no_call_advance try assumption 2162 whd in match (next ???) in ⊢ (??%?); 2163 [ >nxt_spec % 2164 | % 2165 ] 2166 |3: 2167 whd whd in ⊢ (??%?); >nxt_spec normalize nodelta % 2168 |4: 2169 whd whd in match eval_state; normalize nodelta 2170 >nxt_spec >m_return_bind >m_return_bind 2134 2171 whd in match eval_statement_advance; normalize nodelta 2135 >no_call_advance in ⊢ (??%?); [2: assumption ] 2136 whd in match (next ???) in ⊢ (??%?); 2137 >EQsucc_pc in ⊢ (??%?); % 2138 |1: whd whd in ⊢ (??%?); >EQsucc_pc % 2139 |5: %* #H @H -H whd in ⊢ (??%?); >EQsucc_pc % 2140 |2: whd whd in match eval_state; normalize nodelta 2141 >EQsucc_pc >m_return_bind >m_return_bind whd in match eval_statement_advance; 2142 normalize nodelta whd in match goto; normalize nodelta 2172 whd in match goto; normalize nodelta 2143 2173 whd in match (pc_block ?); >pc_block_sigma_commute 2144 >EQ_pc_of_label % 2145 |*: 2174 >pc_of_label_spec % 2175 |7: %* #H @H -H 2176 whd in ⊢ (??%?); >nxt_spec % 2177 |8: 2146 2178 ] 2147 2179 qed. … … 2170 2202 #bv2 #bv2_prf 2171 2203 @(mfr_bind … (λptr.λ_:True.ptr)) 2172 [ lapply bv2_prf lapply bv2 lapply bv1_prf lapply bv1 2173 @bv_pc_other 2174 [ #pc1 #p #bv1_prf #bv2 #bv2_prf @res_preserve_error ] 2175 #bv1 #bv1_no_pc #bv1_prf 2176 @bv_pc_other 2177 [ cases bv1 in bv1_prf; 2178 [||#a #b #c| #a | #a | #a #b | #a #b ] #bv1_prf 2179 #pc2 #p #bv2_prf @res_preserve_error ] 2180 #bv2 #bv2_no_pc #bv2_prf 2181 >sigma_bv_no_pc try assumption 2182 >sigma_bv_no_pc try assumption 2183 whd #ptr #EQ %{I EQ} 2184 ] #ptr * 2185 @if_elim #_ [ @mfr_return | @res_preserve_error ] % 2204 [ change with (pointer_of_address 〈?,?〉) in 2205 match (pointer_of_bevals ?); 2206 change with (pointer_of_address 〈?,?〉) in 2207 match (pointer_of_bevals [sigma_beval ??????;?]); 2208 @sigma_ptr_commute % assumption 2209 ] #ptr * 2210 @if_elim #_ [ @mfr_return | @res_preserve_error ] % 2186 2211 ] 2187 2212 |4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ … … 2190 2215 qed. 2191 2216 2192 2217 lemma fetch_function_no_minus_one : 2218 ∀F,V,i,p,bl. 2219 block_id (pi1 … bl) = -1 → 2220 fetch_function … (globalenv (λvars.fundef (F vars)) V i p) 2221 bl = Error … [MSG BadFunction]. 2222 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct 2223 whd in match fetch_function; normalize nodelta 2224 >globalenv_no_minus_one 2225 cases (symbol_for_block ???) normalize // 2226 qed. 2227 2193 2228 lemma eval_call_ok : 2194 2229 ∀p,p',graph_prog. … … 2203 2238 return 〈f, fn, 2204 2239 sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 → 2205 eval_s eq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes))2206 (CALL … called args dest) nxt st =return st' →2240 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2241 return st' → 2207 2242 (* let st_pc' ≝ mk_state_pc ? st' 2208 2243 (succ_pc (make_sem_graph_params p p') … … … 2228 2263 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn 2229 2264 #called #args #dest #nxt #prf #fetch_spec 2230 cases(fetch_statement_sigma_commute … good (proj 1 … prf) … fetch_spec) #_2265 cases(fetch_statement_sigma_commute … good (proj2 … (proj1 … prf)) … fetch_spec) #_ 2231 2266 normalize nodelta * #lin_fetch_spec #_ 2267 whd in match eval_state in ⊢ (%→?); normalize nodelta >fetch_spec 2268 >m_return_bind >m_return_bind whd in match eval_statement_advance; 2232 2269 whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta 2233 2270 @('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) -H #bl_spec … … 2236 2273 [2:#H @('bind_inversion H) -H #st' #H #_ @('bind_inversion H) -H #vals #_ 2237 2274 @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 2238 #H % 2275 #H lapply (err_eq_from_io ????? H) -H 2276 #H @('bind_inversion H) -H #st_no_pc #save_frame_spec 2277 >m_bind_bind 2278 #H @('bind_inversion H) -H #stack_size #H lapply (opt_eq_from_res ???? H) -H 2279 whd in match (stack_sizes ?); 2280 #stack_size_spec 2281 >m_bind_bind 2282 #H @('bind_inversion H) -H #st_no_pc' #set_call_spec 2283 >m_return_bind whd in ⊢ (??%%→?); 2284 whd in match set_no_pc; normalize nodelta #EQ destruct(EQ) 2285 % 2239 2286 [ @hide_prf 2240 2287 whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind … … 2242 2289 whd in match joint_classify_seq; normalize nodelta 2243 2290 >bl_spec >m_return_bind >int_f_spec normalize nodelta % 2244 | % 2291 | cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2292 bl_spec) 2293 * #lin_bl_spec 2294 generalize in match (fetch_function_transf … graph_prog … 2295 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) 2296 … int_f_spec : fetch_function … (globalenv_noinit … (linearise … graph_prog)) bl = ?) in ⊢ ?; 2297 #lin_int_f_spec 2298 % 2245 2299 [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec 2246 2300 >m_return_bind normalize nodelta whd in match joint_classify_step; 2247 2301 whd in match joint_classify_seq; normalize nodelta 2248 cases bl in bl_spec int_f_spec; #reg #reg_prf -bl #reg_spec #int_f_spec 2249 cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2250 reg_spec) 2251 * #EQ >EQ -EQ >m_return_bind 2252 lapply(fetch_function_transf ????? 2253 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????) 2254 [ 2255 | @(Internal ? fn) 2256 | @id 2257 | assumption assumption 2258 | 2259 | 2260 | % 2261 [@(prog_vars … graph_prog) 2262 |@(prog_funct … graph_prog) 2263 |@(prog_main … graph_prog) 2264 ] 2265 ] 2266 [>int_f_spec % | | |] #EQ >EQ normalize nodelta % 2267 | % 2268 [2: % 2269 [ change with ((λx.joint_call_ident (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 2270 (mk_Sig ? ? ? x)) ? = (λx.joint_call_ident ? (mk_Sig ? ? ? x)) ?) 2271 whd in match joint_call_ident in ⊢ (??(%?)?); normalize nodelta in ⊢ (??(%?)?); 2272 whd in match (pc ?); >lin_fetch_spec in ⊢ (??(%?)?); normalize nodelta in ⊢ (??%?); 2273 whd in match joint_call_ident in ⊢ (???(%?)); normalize nodelta in ⊢ (???(%?)); 2274 >fetch_spec in ⊢ (???(%?)); normalize nodelta >bl_spec in ⊢ (???%); 2275 >m_return_bind in ⊢ (???%); 2276 | whd in match eval_state; normalize nodelta 2277 >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2278 whd in match eval_statement_no_pc; normalize nodelta 2279 whd in match eval_seq_no_pc; normalize nodelta 2280 >m_return_bind in ⊢ (??%?); 2281 whd in match eval_statement_advance; whd in match eval_seq_advance; 2282 whd in match eval_seq_call; normalize nodelta 2302 >lin_bl_spec >m_return_bind 2303 >lin_int_f_spec % 2304 | cases (save_frame_commute … gss … save_frame_spec) in ⊢ ?; 2305 [2: @hide_prf cases st in prf; // ] 2306 #st_no_pc_wf #lin_save_frame_spec 2307 cases (setup_call_commute … gss … st_no_pc_wf … set_call_spec) in ⊢ ?; 2308 #st_no_pc_wf' #lin_set_call_spec 2309 cases (allocate_locals_commute … gss … (joint_if_locals … fn) … st_no_pc_wf') 2310 #st_no_pc_wf'' #lin_allocate_locals_spec 2311 cut 2312 (∃prf.sigma_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') bl (joint_if_entry ?? fn)) prf = 2313 pc_of_point (make_sem_lin_params p p') bl 0) 2314 [ cases (good fn) * #entry_in #_ #_ 2315 % [ @hide_prf % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc ] 2316 whd in match sigma_pc_opt; normalize nodelta 2317 >eqZb_false whd in match (pc_block ?); 2318 [2,4: % #EQbl 2319 >(fetch_function_no_minus_one … graph_prog … EQbl) in int_f_spec; 2320 whd in ⊢ (???%→?); #ABS destruct(ABS) ] 2321 normalize nodelta whd in match fetch_internal_function; 2322 normalize nodelta >int_f_spec >m_return_bind >point_of_pc_of_point 2323 >entry_in whd in ⊢ (??%%→?); #EQ destruct(EQ) % 2324 ] * #entry_prf #entry_spec 2325 % [ @hide_prf %{st_no_pc_wf''} %{entry_prf} @(proj1 … (proj1 … prf)) ] 2326 % [ whd in match joint_call_ident; normalize nodelta 2327 >lin_fetch_spec in ⊢ (??match % with [ _ ⇒ ? | _ ⇒ ?]?); 2328 >fetch_spec in ⊢ (???match % with [ _ ⇒ ? | _ ⇒ ?]); 2329 normalize nodelta 2330 >lin_bl_spec >bl_spec >m_return_bind >m_return_bind 2331 whd in match fetch_internal_function; normalize nodelta 2332 >lin_int_f_spec >int_f_spec % 2333 | whd in match eval_state; normalize nodelta 2334 >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2335 whd in match eval_statement_no_pc; normalize nodelta 2336 whd in match eval_seq_no_pc; normalize nodelta 2337 >m_return_bind in ⊢ (??%?); 2338 whd in match eval_statement_advance; whd in match eval_seq_advance; 2339 whd in match eval_seq_call; normalize nodelta 2340 >lin_bl_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2341 >lin_int_f_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2342 normalize nodelta 2343 >lin_save_frame_spec >m_return_bind 2344 >m_bind_bind whd in match (stack_sizes ?); 2345 >stack_size_spec >m_return_bind 2346 >lin_set_call_spec >m_return_bind 2347 >lin_allocate_locals_spec 2348 <entry_spec % 2283 2349 ] 2284 cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2285 bl_spec) * #EQ >EQ in ⊢ (??%?); >m_return_bind in ⊢ (??%?); -EQ 2286 [ whd in match fetch_internal_function; normalize nodelta >int_f_spec in ⊢ (???%); 2287 >m_return_bind in ⊢ (???%); normalize nodelta ] 2288 lapply(fetch_function_transf ????? 2289 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????) 2290 [ 2291 | 2,12: @(Internal ? fn) 2292 | 3,13: @id 2293 | 4,14: assumption assumption 2294 | 5,15: 2295 | 6,16: 2296 |7,17: % 2297 [1,4: @(prog_vars … graph_prog) 2298 |2,5: @(prog_funct … graph_prog) 2299 |3,6: @(prog_main … graph_prog) 2300 ] 2301 ] 2302 [1,5: >int_f_spec % |*:] #EQ >EQ in ⊢ (??%?); -EQ 2303 >m_return_bind in ⊢ (??%?); normalize nodelta [ %] 2304 ] 2305 ] 2306 ] 2307 [2: @hide_prf] 2308 lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) 2309 #st' #st_spec' #H @('bind_inversion H) -H #st'' #st_spec'' 2310 whd in ⊢ (??%% → ?); #EQ destruct(EQ) [ % ] 2311 [2,3: elim(save_frame_commute p p' graph_prog sigma gss … prf … st_spec') 2312 #wf_st' #sigma_st_spec' [2: >sigma_st_spec' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);] 2313 lapply st_spec'' -st_spec'' whd in match eval_internal_call; normalize nodelta 2314 #H @('bind_inversion H) -H #dim_s #dim_s_spec #H 2315 [ >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);] 2316 elim(bind_inversion ????? H) -H #st''' * #st_spec''' 2317 elim(setup_call_commute p p' graph_prog sigma gss … wf_st' … st_spec''') 2318 #wf_st''' #sigma_st_spec''' whd in ⊢ (??%% → ?); 2319 whd in match allocate_locals; whd in match set_regs; normalize nodelta 2320 #EQ destruct(EQ) 2321 ] 2322 [ >sigma_st_spec''' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2323 whd in match sigma_state_pc; normalize nodelta 2324 change with (return mk_state_pc (make_sem_lin_params p p') ? ? = ?) 2325 cut(∀A,semp,pc,pc',st,st'.∀ f : ? → A.pc = pc' ∧ st = st' → 2326 f(mk_state_pc semp st pc) = f(mk_state_pc semp st' pc')) 2327 [#A #H1 #H2 #H3 #H4 #H5 #f * #H8 #H9 //] 2328 #APP @APP % 2329 ] 2330 [1,4: [whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc | whd in match well_formed_pc;] 2331 whd in match sigma_pc_opt; normalize nodelta @if_elim 2332 [1,3: @eqZb_elim [2,4: #_ *] #EQbl cases bl in EQbl int_f_spec; * 2333 #reg #pos #reg_prf normalize in ⊢ (% → ?); 2334 #EQbl whd in match fetch_function; normalize nodelta 2335 >EQbl cases(symbol_for_block ???) 2336 [1,3: whd in ⊢ (??%% → ?); #ABS destruct(ABS)] 2337 #id1 >m_return_bind inversion(find_funct_ptr ???) 2338 [1,3:#_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)] 2339 #z lapply(globalenv_no_minus_one ??? graph_prog) [1,3: @(λn.[Init_space n])] 2340 #EQ 2341 change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?) → ?) 2342 change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?)) in EQ; 2343 cases reg in ⊢ (% → ?); 2344 [1,3: whd in match find_funct_ptr; normalize nodelta #ABS destruct(ABS) 2345 |2,4: >EQ #ABS destruct(ABS) 2346 ] 2347 |2,4: #_ whd in match fetch_internal_function; normalize nodelta 2348 whd in match (pc_block ?); >int_f_spec >m_return_bind 2349 >point_of_pc_of_point lapply(good fn) ** #EQ #_ #_ >EQ -EQ 2350 >m_return_bind [2:%] whd in ⊢ (??%? → ?); #EQ destruct(EQ) 2351 % 2352 ] 2353 | whd in match sigma_state; normalize nodelta 2354 cut(∀A,semp,fr,fr',is,is',c,c',r,r',m,m'.∀ f : ? → A. 2355 fr = fr' ∧ is = is' ∧ c = c' ∧ r = r' ∧ m = m'→ 2356 f(mk_state semp fr is c r m) = f(mk_state semp fr' is' c' r' m')) 2357 [#A #semp #fr #fr' #is #is' #c #c' #r #r' #m #m' #f **** //] 2358 #APP @APP % [% [% [% [%]]]] // [whd in match sigma_is; normalize nodelta % |3: 2359 whd in match sigma_mem; normalize nodelta %] 2360 | % [2: @(proj2 … wf_st')] % [ % [ @(proj1 … (proj1 … (proj1 … wf_st'))) | 2361 @(proj2 … (proj1 … (proj1 … wf_st')))] ] 2362 ] 2363 [ change with (? = (λx.sigma_regs ? ? ? ? ? (foldr ? ? ? ? x) ?)?) 2364 [ cut((joint_if_locals (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 2365 (globals (lin_prog_params p p' (linearise p graph_prog) stack_sizes)) 2366 (\fst (linearise_int_fun p 2367 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))) = (joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2368 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn)) 2369 [%] #EQ >EQ 2370 elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2371 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) in ⊢ (??%(?%)); 2372 | @hide_prf elim x 2373 ] 2374 | @hide_prf elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2375 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) 2376 ] 2377 [3,5: whd in match (foldr ? ? ???); @(proj2 … (proj1 … wf_st')) 2378 |4,6: #locs_t #tl_list #wf_regs_tail whd in match (foldr ? ? ???); 2379 elim(allocate_locals_commute p p' graph_prog sigma gss locs_t 2380 ? wf_regs_tail) #wf_regs_locs_t #_ assumption 2381 |*: normalize nodelta 2382 [ whd in match (foldr ? ? ???) in ⊢ (??%%); % 2383 | #locs_t #tl_list #EQtl whd in match (foldr ?????) in ⊢ (??%%); 2384 >EQtl 2385 lapply(allocate_locals_commute p p' graph_prog sigma gss locs_t 2386 (foldr (localsT ?) (regsT ?) (allocate_locals_ ???) (regs ? st') tl_list) ?) 2387 [2: * #x #H >H % |] 2388 ] 2389 ] 2350 ] 2351 ] 2390 2352 qed. 2391 2353 2392 2354 lemma eval_goto_ok : 2393 lemma eval_tailcall_ok 2394 : 2395 lemma eval_cond_cond_ok : 2396 lemma eval_cond_fcond_ok : 2355 ∀p,p',graph_prog. 2356 let lin_prog ≝ linearise p graph_prog in 2357 ∀stack_sizes. 2358 ∀sigma.good_sigma p graph_prog sigma → 2359 ∀gss : good_state_sigma p p' graph_prog sigma. 2360 ∀st,st',f,fn,nxt. 2361 ∀prf : well_formed_state_pc … gss st. 2362 fetch_statement (make_sem_graph_params p p') … 2363 (globalenv_noinit ? graph_prog) (pc … st) = 2364 return 〈f, fn, final … (GOTO (mk_graph_params p) … nxt)〉 → 2365 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2366 return st' → 2367 ∃prf'. 2368 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 2369 (sigma_state_pc … gss st prf) 2370 (sigma_state_pc … gss st' prf'). 2371 bool_to_Prop (taaf_non_empty … taf). 2372 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn 2373 #nxt #prf #EQfetch 2374 whd in match eval_state; normalize nodelta >EQfetch 2375 >m_return_bind >m_return_bind 2376 whd in match eval_statement_advance; normalize nodelta 2377 whd in match goto; normalize nodelta 2378 #H lapply (err_eq_from_io ????? H) -H 2379 #H @('bind_inversion H) #pc' 2380 @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn 2381 #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); 2382 #EQ destruct(EQ) 2383 >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); 2384 #EQ1 #EQ2 destruct 2385 cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) 2386 normalize nodelta ** #prf' #EQpc_of_label' * 2387 #EQfetch' 2388 -H 2389 % 2390 [ @hide_prf cases st in prf prf'; -st #st #pc #popped ** #H1 #H2 #H3 2391 #H4 %{H3} %{H1 H4} ] 2392 %{(taaf_step … (taa_base …) …) I} 2393 [ whd whd in ⊢ (??%?); >EQfetch' % 2394 | whd whd in match eval_state; normalize nodelta 2395 >EQfetch' >m_return_bind >m_return_bind 2396 whd in match eval_statement_advance; whd in match goto; 2397 normalize nodelta >pc_block_sigma_commute >EQpc_of_label' 2398 >m_return_bind % 2399 ] 2400 qed. 2401 2402 lemma eval_cond_ok : 2403 ∀p,p',graph_prog. 2404 let lin_prog ≝ linearise p graph_prog in 2405 ∀stack_sizes. 2406 ∀sigma.good_sigma p graph_prog sigma → 2407 ∀gss : good_state_sigma p p' graph_prog sigma. 2408 ∀st,st',f,fn,a,ltrue,lfalse. 2409 ∀prf : well_formed_state_pc … gss st. 2410 fetch_statement (make_sem_graph_params p p') … 2411 (globalenv_noinit ? graph_prog) (pc … st) = 2412 return 〈f, fn, sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 → 2413 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2414 return st' → 2415 as_costed (joint_abstract_status (graph_prog_params p p' graph_prog stack_sizes)) 2416 st' → 2417 ∃prf'. 2418 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 2419 (sigma_state_pc … gss st prf) 2420 (sigma_state_pc … gss st' prf'). 2421 bool_to_Prop (taaf_non_empty … taf). 2422 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn 2423 #a #ltrue #lfalse #prf #EQfetch 2424 whd in match eval_state; normalize nodelta >EQfetch 2425 >m_return_bind >m_return_bind 2426 whd in match eval_statement_advance; normalize nodelta 2427 #H @('bind_inversion (err_eq_from_io ????? H)) 2428 @bv_pc_other [ #pc' #p #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 2429 #bv #bv_no_pc #EQretrieve 2430 cut 2431 (∃prf'.acca_retrieve ?? (p' ?) (sigma_state_pc p p' graph_prog sigma gss st prf) a = 2432 return sigma_beval p p' graph_prog sigma bv prf') 2433 [ @acca_retrieve_commute assumption ] 2434 * #bv_prf >(sigma_bv_no_pc … bv_no_pc) #EQretrieve' 2435 -H #H @('bind_inversion H) * 2436 #EQbool normalize nodelta -H 2437 [ whd in match goto; normalize nodelta 2438 #H @('bind_inversion H) -H #pc' 2439 @('bind_inversion EQfetch) * #curr_i #curr_fn #EQfetchfn 2440 #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%%→?); 2441 #EQ destruct(EQ) 2442 >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→??%%→?); 2443 #EQ1 #EQ2 destruct 2444 | whd in ⊢ (??%%→?); 2445 #EQ destruct(EQ) 2446 ] 2447 #ncost 2448 cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) 2449 normalize nodelta ** #prf' #EQpc_of_label' ** #prf'' ** 2450 #EQfetch' #nxt_spec 2451 % [1,3,5,7: @hide_prf 2452 cases st in prf prf' prf''; 2453 -st #st #pc #popped ** #H1 #H2 #H3 #H4 #H5 2454 %{H3} %{H1} assumption ] 2455 %{(taaf_step_jump … (taa_base …) …) I} 2456 [1,4,7,10: whd 2457 >(as_label_sigma_commute … good) assumption 2458 |2,5,8,11: whd whd in ⊢ (??%?); 2459 >EQfetch' % 2460 |*: whd whd in match eval_state; normalize nodelta >EQfetch' 2461 >m_return_bind >m_return_bind 2462 whd in match eval_statement_advance; normalize nodelta >EQretrieve' 2463 >m_return_bind >EQbool >m_return_bind normalize nodelta 2464 [1,2: whd in match goto; normalize nodelta 2465 >pc_block_sigma_commute >EQpc_of_label' % 2466 |3: whd in match next; normalize nodelta >nxt_spec % 2467 |4: whd in match goto; normalize nodelta 2468 >pc_block_sigma_commute >nxt_spec % 2469 ] 2470 ] 2471 qed. 2472 2397 2473 lemma eval_return_ok : 2474 ∀p,p',graph_prog. 2475 let lin_prog ≝ linearise p graph_prog in 2476 ∀stack_sizes. 2477 ∀sigma.∀good : good_sigma p graph_prog sigma. 2478 ∀gss : good_state_sigma p p' graph_prog sigma. 2479 ∀st,st',f,fn. 2480 ∀prf : well_formed_state_pc … gss st. 2481 fetch_statement (make_sem_graph_params p p') … 2482 (globalenv_noinit ? graph_prog) (pc … st) = 2483 return 〈f, fn, final … (RETURN (mk_graph_params p) … )〉 → 2484 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2485 return st' → 2486 joint_classify (lin_prog_params … (linearise … graph_prog) stack_sizes) 2487 (sigma_state_pc … st prf) = Some ? cl_return ∧ 2488 ∃prf'. 2489 ∃st2_after_ret. 2490 ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes) 2491 st2_after_ret 2492 (sigma_state_pc … gss st' prf'). 2493 (if taaf_non_empty … taf then 2494 ¬as_costed (joint_abstract_status (lin_prog_params p p' (linearise … graph_prog) stack_sizes)) 2495 st2_after_ret 2496 else True) ∧ 2497 eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) 2498 (sigma_state_pc … st prf) = 2499 return st2_after_ret ∧ 2500 ret_rel … (linearise_status_rel … gss good) st' st2_after_ret. 2501 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st' #f #fn 2502 #prf #EQfetch 2503 whd in match eval_state; normalize nodelta >EQfetch 2504 >m_return_bind >m_return_bind 2505 whd in match eval_statement_advance; normalize nodelta 2506 #H lapply (err_eq_from_io ????? H) -H 2507 #H @('bind_inversion H) -H #st1' #EQpop 2508 cut (∃prf'. 2509 (pop_frame … (ev_genv (lin_prog_params ? p' (linearise ? graph_prog) stack_sizes)) 2510 f (\fst (pi1 ?? (linearise_int_fun ?? fn))) (sigma_state … gss st (proj2 … prf))) 2511 = return sigma_state_pc … gss st1' prf') 2512 [ @pop_frame_commute assumption ] 2513 * #prf' #EQpop' >m_bind_bind 2514 #H @('bind_inversion H) ** #call_i #call_fn 2515 * [ * [ #s | #a #lbl ] #nxt | #s | * ] normalize nodelta 2516 #EQfetch_ret -H 2517 whd in ⊢ (??%%→?); #EQ destruct(EQ) whd in match (next ???); >graph_succ_pc 2518 cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf)) … EQfetch) 2519 #_ normalize nodelta #EQfetch' 2520 cases (fetch_statement_sigma_commute … good … (proj2 … (proj1 … prf')) … EQfetch_ret) 2521 normalize nodelta 2522 #all_labels_in 2523 * #EQfetch_ret' * #prf'' * [2: * ] #nxt_spec [2:| #EQpc_of_label'] 2524 % [1,3: whd in match joint_classify; normalize nodelta 2525 >EQfetch' >m_return_bind % ] 2526 % [1,3: @hide_prf cases prf' * #_ #H1 #H2 %{H2} %{H1 prf''} ] 2527 [ % [2: %{(taaf_base …)} |] 2528 % [ %{I} ] 2529 [ >EQfetch' >m_return_bind >m_return_bind normalize nodelta 2530 whd in match eval_return; normalize nodelta 2531 >EQpop' >m_return_bind 2532 whd in match next_of_pc; normalize nodelta 2533 >EQfetch_ret' >m_return_bind whd in match next; normalize nodelta 2534 >nxt_spec % 2535 | * #s1_pre #s1_call 2536 cases (joint_classify_call … s1_call) 2537 * #calling_i #calling * #call_spec * #arg * #dest * #nxt * #bl 2538 * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called 2539 * #s2_pre #s2_call 2540 whd in ⊢ (%→?); >EQfetch_call * #EQ #_ 2541 * #s1_pre_prf #EQpc_s2_pre 2542 whd >EQpc_s2_pre 2543 <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] 2544 >EQfetch_ret' % [ % | >nxt_spec % ] 2545 ] 2546 | % [2: %{(taaf_step … (taa_base …) …)} |*:] 2547 [3: % [ % normalize nodelta ] 2548 [2: >EQfetch' in ⊢ (??%?); 2549 >m_return_bind in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2550 normalize nodelta 2551 whd in match eval_return; normalize nodelta 2552 >EQpop' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2553 whd in match next_of_pc; normalize nodelta 2554 >EQfetch_ret' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2555 whd in match next; normalize nodelta % 2556 |1: normalize nodelta %* #H @H -H 2557 whd in ⊢ (??%?); >nxt_spec % 2558 |3: * #s1_pre #s1_call 2559 cases (joint_classify_call … s1_call) 2560 * #calling_i #calling * #call_spec * #arg * #dest * #nxt' * #bl 2561 * #called_i * #called ** #EQfetch_call #EQbl #EQfetch_called 2562 * #s2_pre #s2_call 2563 whd in ⊢ (%→?); >EQfetch_call * #EQ #_ 2564 * #s1_pre_prf #EQpc_s2_pre 2565 whd >EQpc_s2_pre 2566 <(sigma_pc_irr … EQ) [2: @hide_prf @(proj2 … (proj1 … prf')) ] 2567 >EQfetch_ret' %% 2568 ] 2569 |1: whd whd in ⊢ (??%?); >nxt_spec % 2570 |2: whd whd in match eval_state; normalize nodelta 2571 >nxt_spec >m_return_bind >m_return_bind 2572 whd in match eval_statement_advance; whd in match goto; normalize nodelta 2573 whd in match (pc_block ?); >pc_block_sigma_commute 2574 >EQpc_of_label' >m_return_bind % whd in match (set_pc ???); % 2575 |*: 2576 ] 2577 ] 2578 qed. 2579 2580 (* TODO *) 2581 axiom eval_tailcall_ok : 2582 ∀p,p',graph_prog. 2583 let lin_prog ≝ linearise p graph_prog in 2584 ∀stack_sizes. 2585 ∀sigma.good_sigma p graph_prog sigma → 2586 ∀gss : good_state_sigma p p' graph_prog sigma. 2587 ∀st,st',f,fn,fl,called,args. 2588 ∀prf : well_formed_state_pc … gss st. 2589 fetch_statement (make_sem_graph_params p p') … 2590 (globalenv_noinit ? graph_prog) (pc … st) = 2591 return 〈f, fn, final … (TAILCALL (mk_graph_params p) … fl called args)〉 → 2592 eval_state … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) st = 2593 return st' → 2594 let st2_pre_call ≝ sigma_state_pc … gss st prf in 2595 ∃is_tailcall, is_tailcall'. 2596 ∃prf'. 2597 let st2_after_call ≝ sigma_state_pc … gss st' prf' in 2598 joint_tailcall_ident (lin_prog_params … (linearise … graph_prog) stack_sizes) «st2_pre_call, is_tailcall'» = 2599 joint_tailcall_ident (graph_prog_params … graph_prog stack_sizes) «st, is_tailcall» ∧ 2600 eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) 2601 st2_pre_call = return st2_after_call. 2398 2602 2399 2603 … … 2432 2636 change with 2433 2637 (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) 2434 whd in match eval_state in ⊢ (%→?); normalize nodelta 2435 @'bind_inversion 2436 ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt 2437 cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_ 2438 @'bind_inversion 2439 #st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance 2440 * #wf_prf #st2_EQ 2441 2442 cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt) 2443 cases stmt in EQfetch_stmt ex ex_advance; -stmt 2638 #EQeval 2639 @('bind_inversion EQeval) 2640 ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch 2641 #_ * #prf #EQst2 2642 cases stmt in EQfetch; -stmt 2444 2643 [ @cond_call_other 2445 2644 [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ] 2446 2645 normalize nodelta 2447 #EQfetch _stmt2448 whd in match eval_statement_no_pc in ⊢ (%→?); normalize nodelta 2449 #ex 2450 [| whd in match eval_statement_advance in ⊢ (%→?);2451 whd in match eval_seq_advance in ⊢ (%→?);2646 #EQfetch 2647 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 2648 [ (* COND *) 2649 whd in match joint_classify; normalize nodelta; 2650 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 2452 2651 normalize nodelta 2453 | whd in match eval_statement_advance in ⊢ (%→?); 2652 #ncost 2653 cases (eval_cond_ok … good … prf EQfetch EQeval ncost) 2654 #prf' * #taf #taf_ne 2655 destruct(EQst2) 2656 % [2: %{taf} |*:] 2657 >taf_ne normalize nodelta 2658 % [ %{I} %{prf'} % ] 2659 whd >(as_label_sigma_commute … good) % 2660 | (* CALL *) 2661 cases (eval_call_ok … good … prf EQfetch EQeval) 2662 #is_call * #is_call' * 2663 #prf' * #eq_call #EQeval' 2664 destruct(EQst2) 2665 >is_call in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta 2666 #ignore %{«?, is_call'»} 2667 % [ %{eq_call} %{prf} % ] 2668 % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] 2669 whd >(as_label_sigma_commute … good) % 2670 | (* SEQ *) 2671 whd in match joint_classify; normalize nodelta; 2672 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 2454 2673 normalize nodelta 2455 >(no_call_advance (mk_prog_params (make_sem_graph_params p p') 2456 graph_prog stack_sizes)) in ⊢ (%→?); try assumption 2457 ] 2458 #ex_advance 2459 #all_labels_in 2460 letin lin_prog ≝ (linearise … graph_prog) 2461 lapply (refl … (eval_state … (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2)) 2462 whd in match eval_state in ⊢ (???%→?); 2463 >st2_EQ in ⊢ (???%→?); normalize nodelta 2464 [ (* COND *) 2465 | (* CALL *) 2466 | (* SEQ *) 2467 #ex' 2468 * #lin_fetch_stmt #next_spec 2469 whd in match (as_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2470 >EQfetch_stmt in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2471 normalize nodelta 2472 whd in match joint_classify_step; 2473 normalize nodelta 2474 >no_call_other in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2475 try assumption 2476 normalize nodelta 2477 >lin_fetch_stmt in ex' : (???%) ⊢ ?; >m_return_bind in ⊢ (???%→?); 2478 whd in match eval_statement_no_pc in ⊢ (???%→?); 2479 normalize nodelta 2480 cases (eval_seq_no_pc_sigma_commute … gss … ex) in ⊢ ?; 2481 [2: @hide_prf @(proj2 … wf_prf) ] 2482 #st1_no_pc_wf #EQ >EQ in ⊢ (???%→?); -EQ 2483 >m_return_bind in ⊢ (???%→?); 2484 whd in match eval_statement_advance in ⊢ (%→?); 2485 normalize nodelta 2486 >(no_call_advance (mk_prog_params (make_sem_lin_params p p') 2487 lin_prog stack_sizes)) in ⊢ (%→?); try assumption 2488 whd in match (next ???) in ⊢ (%→?); 2489 change with (sigma_pc ????? (hide_prf ??)) in match (pc ??) in ⊢ (%→?); 2490 #ex' 2491 cases next_spec 2492 #succ_pc_nxt_wf * 2493 [ #succ_pc_commute >succ_pc_commute in ex' ⊢ ?; 2494 #ex' 2495 % [2: %{(taaf_step … (taa_base …) …)} [2: @ex' ] |*:] 2496 whd 2497 [ whd in ⊢ (??%?); 2498 >lin_fetch_stmt normalize nodelta 2499 whd in match joint_classify_step; normalize nodelta 2500 @no_call_other assumption 2501 | normalize nodelta 2502 cut (? : Prop) 2503 [3: #H % [ % [ % | @H ]] |*:] 2504 [ (* TODO lemma : sem_rel → label_rel *) 2505 cases daemon 2506 | whd in ex_advance : (??%%); destruct(ex_advance) 2507 % [ % assumption | % ] 2508 ] 2509 ] 2510 | #fetch_GOTO 2511 cases (all_labels_in) #wf_next #_ 2512 cases (pc_of_label_sigma_commute … p' … good … EQfetchfn ?) 2513 [2: @nxt |3: cases daemon ] 2514 #wf_next' #EQ 2515 % [2: %{(taaf_step … (taa_step … (taa_base …) …) …)} 2516 [3: @ex' 2517 |2: whd 2518 whd in match eval_state; normalize nodelta 2519 >fetch_GOTO in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2520 >m_return_bind in ⊢ (??%?); 2521 whd in match eval_statement_advance; normalize nodelta 2522 whd in match goto; normalize nodelta 2523 whd in match (pc_block ?); 2524 >sigma_pblock_eq_lemma >EQ in ⊢ (??%?); % 2525 |7: normalize nodelta 2526 cut (? : Prop) 2527 [3: #H % [ % [ % | @H ]] |*:] 2528 [ (* TODO lemma : sem_rel → label_rel *) 2529 cases daemon 2530 | whd in ex_advance : (??%%); destruct(ex_advance) 2531 % [ % assumption | % ] 2532 ] 2533 |5: % * #H @H -H whd in ⊢ (??%?); >fetch_GOTO % 2534 |4: whd whd in ⊢ (??%?); 2535 >lin_fetch_stmt normalize nodelta 2536 whd in match joint_classify_step; normalize nodelta 2537 @no_call_other assumption 2538 |1: whd whd in ⊢ (??%?); 2539 >fetch_GOTO normalize nodelta % 2540 |*: 2541 ] 2542 |*: 2543 ] 2544 ] 2545 | (* FIN *) 2546 ] 2547 2548 #stmt_spec 2549 2550 2551 cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?; 2552 #wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?); 2553 2554 whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2555 >EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2556 normalize nodelta 2557 2558 normalize nodelta 2559 [ whd in match joint_classify_step; @cond_call_other 2560 [ (* COND *) #a #lbltrue #nxt 2561 #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta 2562 #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other 2563 [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 2564 #bv #bv_no_pc #EQretrieve 2565 cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve) 2566 #ignore >(sigma_bv_no_pc … bv_no_pc) 2567 change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?) 2568 #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); 2569 #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv 2570 >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta 2571 [ whd in match goto; normalize nodelta 2572 >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?); 2573 #EQ destruct(EQ) #ex_advance #ex_advance' 2574 % [2: %{(tal_base_not_return …)} [3: @ex_advance' 2575 | (* CALL *) #f #args #dest #nxt 2576 | (* other *) #stmt #no_call #nxt 2577 ] normalize nodelta 2578 [ #ex 2579 #ex_advance #ex_advance' 2580 | whd in ⊢ (??%%→?); #EQ destruct(EQ) 2581 #H @('bind_inversion H) -H #called_block 2582 #H lapply (err_eq_from_io ????? H) -H #EQcalled_block 2583 #H @('bind_inversion H) -H * #called * #called_fn 2584 #H lapply (err_eq_from_io ????? H) -H #EQcalled 2674 whd in match joint_classify_step; normalize nodelta 2675 >no_call_other [2: assumption ] normalize nodelta 2676 cases (eval_seq_no_call_ok … good … prf EQfetch EQeval) [2: assumption ] 2677 #prf' * #taf #taf_ne 2678 destruct(EQst2) 2679 % [2: %{taf} |*:] 2680 >taf_ne normalize nodelta % [ %{I} ] 2681 [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] 2682 | (* FIN *) cases s in EQfetch; 2683 [ (* GOTO *) #lbl #EQfetch 2684 whd in match joint_classify; normalize nodelta; 2685 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 2585 2686 normalize nodelta 2586 [ #H lapply (err_eq_from_io ????? H) -H ] 2587 #H @('bind_inversion H) -H 2588 | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ] 2589 #ex_advance #ex_advance' 2590 whd in match joint_classify_seq; normalize nodelta 2591 >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 2592 2593 cut (∀p,p',graph_prog,sigma,gss,st,f,bl. 2594 ∀prf : well_formed_state p p' graph_prog sigma gss st. 2595 block_of_call (make_sem_graph_params p p') ? 2596 (globalenv_noinit ? graph_prog) st f = return bl → 2597 block_of_call (make_sem_lin_params p p') ? 2598 (globalenv_noinit ? (linearise … graph_prog)) 2599 (sigma_state … st prf) f = return bl) 2600 [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute 2601 whd in match eval_seq_advance; normalize nodelta 2602 >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?); 2603 >m_return_bind in ⊢ (???%→?); 2604 >(fetch_function_transf … EQcalled : 2605 fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?); 2606 >m_return_bind in ⊢ (???%→?); 2607 whd in match (transf_fundef); normalize nodelta 2608 2609 2610 #block_of_call_sigma_commute 2611 @match_int_fun #called_descr #EQcalled_descr 2612 [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ] 2613 #ex_advance 2614 cut 2615 (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ. 2616 ∀trans : ∀vars.A vars → B vars. 2617 let prog_out : program (λvars.fundef (B vars)) ℕ ≝ 2618 transform_program ??? prog (λvars.transf_fundef … (trans vars)) in 2619 ∀i.is_function … (globalenv_noinit … prog) i → 2620 is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ] 2621 #f_propagate 2622 letin sigma_function ≝ (λA,B,prog,trans. 2623 λf : Σi.is_function ? (globalenv_noinit ? prog) i. 2624 «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *) 2625 cut (∀p,p',graph_prog. 2626 let lin_prog ≝ linearise ? graph_prog in 2627 ∀sigma.∀gss : good_state_sigma … graph_prog sigma. 2628 ∀f,st,fn. 2629 ∀prf : well_formed_state … gss st. 2630 function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog) 2631 st f = return fn → 2632 function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) 2633 (sigma_state … gss st prf) f = return sigma_function … fn) 2634 [1,3: (* TODO lemma *) cases daemon ] 2635 #function_of_call_sigma_commute 2636 whd in match joint_classify_step; whd in match joint_classify_seq; 2637 normalize nodelta #next_spec 2638 >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?); 2639 >m_return_bind in ⊢ (%→?); 2640 @match_int_fun 2641 [2,3: #EQdescr' lapply EQdescr' 2642 >description_of_function_transf in EQdescr'; 2643 2644 2645 whd in match sigma_beval; normalize nodelta 2646 cases bv 2647 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ] 2648 whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?); 2649 [7: #ignore #_ 2650 #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve 2651 whd in match (bool_of_beval ?) in ⊢ (% → ?); 2652 3: >no_call_advance [2: @no_call] 2653 2654 2655 2656 generalize in match wf_pc in ⊢ ?; 2657 whd in ⊢ (%→?); 2658 inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ] 2659 #lin_pc 2660 whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta 2661 >EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?); 2662 #H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt * 2663 #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_ 2664 elim (good_local … EQsigma) -good_local 2665 #stmt' * 2666 change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?) 2667 >EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) 2668 #H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta 2669 >(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ] 2670 change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?); 2671 letin lin_fun ≝ (\fst (linearise_int_fun p globals graph_fun)) 2672 change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?); 2673 * 2674 #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec 2675 destruct(EQst2) 2676 whd in match eval_state in ⊢ (???%→?); normalize nodelta 2677 (* resolve classifier *) 2678 [ * 2679 [ #stmt #nxt 2680 whd in match eval_statement in ⊢ (?→%→?); normalize nodelta 2681 #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec 2682 whd in match (graph_to_lin_statement ???) in ⊢ (%→?); 2683 whd in match eval_statement in ⊢ (%→?); normalize nodelta 2684 elim (IO_bind_inversion ??????? EQeval) #st1_no_pc * 2685 #EQeval_no_pc #EQeval_pc 2686 >(eval_seq_no_pc_sigma_commute … EQeval_no_pc) 2687 [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ] 2688 >m_return_bind 2689 cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec; 2690 [14: #f #args #dest 2691 | #c 2692 | #lbl 2693 | #move_sig 2694 | #a 2695 | #a 2696 | #sy #sy_prf #dpl #dph 2697 | #op #a #b #arg1 #arg2 2698 | #op #a #arg 2699 | #op #a #arg1 #arg2 2700 || 2701 | #a #dpl #dph 2702 | #dpl #dph #a 2703 | #s_ext 2704 ] 2705 [ (* CALL *) 2706 |(*:*) 2707 normalize nodelta 2708 #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec 2709 whd in match eval_seq_pc; normalize nodelta 2710 #ex1 2711 cases next_spec 2712 [ #EQnext_sigma 2713 %[2: %{(taaf_step … (taa_base …) ex1 ?)} 2714 [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|] 2715 normalize nodelta 2716 cut (? : Prop) [3: #R' % [ %{I R'} ] |*:] 2717 [ cases daemon (* TODO lemma joint_label_sigma_commute *) 2718 | % 2719 [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon 2720 | whd in match eval_seq_pc in EQeval_pc; 2721 whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?); 2722 destruct (EQeval_pc) 2723 whd in ⊢ (??%%); 2724 change with (sigma_pc ??????) in match 2725 (pc ? (sigma_state_pc ???????)); 2726 whd in match (succ_pc ????) in ⊢ (??%%); 2727 whd in match (point_of_succ ???) in ⊢ (??%%); 2728 >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma) 2729 whd in match sigma_pc in ⊢ (???%); 2730 whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta 2731 @opt_safe_elim #pc' 2732 >EQfunc_of_block >m_return_bind 2733 whd in match point_of_pc; normalize nodelta 2734 >point_of_offset_of_point 2735 >EQnext_sigma whd in ⊢ (??%?→?); 2736 whd in match pc_of_point; normalize nodelta 2737 #EQ destruct(EQ) 2738 >sigma_pblock_eq_lemma % 2739 ] 2740 ] 2741 | -next_spec #next_spec 2742 % 2743 2744 2745 whd in ⊢ (?→???%→?); 2746 generalize in ⊢ (??%? → ???(????%) → ?); |*: skip] | #a #lbltrue #next 2747 ] #next change with label in next; 2748 | * 2749 [ #lbl 2750 | 2751 | #fl #f #args 2687 cases (eval_goto_ok … good … prf EQfetch EQeval) 2688 #prf' * #taf #taf_ne 2689 destruct(EQst2) 2690 % [2: %{taf} |*:] 2691 >taf_ne normalize nodelta % [ %{I} ] 2692 [ %{prf'} % | whd >(as_label_sigma_commute … good) % ] 2693 | (* RETURN *) #EQfetch 2694 whd in match joint_classify; normalize nodelta; 2695 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); 2696 normalize nodelta 2697 cases (eval_return_ok … good … prf EQfetch EQeval) 2698 #is_ret' * 2699 #prf' * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf 2700 destruct(EQst2) 2701 % [2: % [2: % [2: %{(taa_base …)} %{taf} ]] |*:] 2702 % [2: whd >(as_label_sigma_commute … good) % ] 2703 %{ret_prf} 2704 % [2: %{prf'} % ] 2705 %{EQeval'} 2706 %{taf_prf is_ret'} 2707 | (* TAILCALL *) #fl #called #args #EQfetch 2708 cases (eval_tailcall_ok … good … prf EQfetch EQeval) 2709 #is_tailcall * #is_tailcall' * 2710 #prf' * #eq_call #EQeval' 2711 destruct(EQst2) 2712 >is_tailcall in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta 2713 #ignore %{«?, is_tailcall'»} 2714 %{eq_call} 2715 % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} %{prf'} % ]] |*:] 2716 whd >(as_label_sigma_commute … good) % 2752 2717 ] 2753 2718 ] 2754 whd in match eval_statement in ⊢ (?→%→?); normalize nodelta 2755 #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec 2756 normalize nodelta 2757 whd in match (graph_to_lin_statement ???) in ⊢ (%→?); 2758 whd in match eval_statement in ⊢ (%→?); normalize nodelta 2759 [ >m_return_bind in ⊢ (%→?); 2760 >m_return_bind in EQeval; 2761 2762 2763 2764 (* common for all non-call seq *) 2765 >m_return_bind in ⊢ (%→?); 2766 whd in ⊢ (??%%→?); #EQ destruct(EQ) 2767 >m_return_bind in ⊢ (%→?); 2768 2769 2770 #ex1 2771 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) 2772 2773 whd in match (point_of_pc ???); 2774 whd in match (point_of_succ ???); 2775 whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim 2776 #pc' #H 2777 elim (bind_opt_inversion ????? H) #fn * #EQbl 2778 -H #H 2779 elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?); 2780 #EQ destruct(EQ) 2781 whd in match (succ_pc ????); 2782 whd in match (point_of_succ ???); 2783 change with (point_of_offset ???) in match (point_of_pc ???); 2784 >point_of_offset_of_point 2785 whd in match sigma_pc; normalize nodelta @opt_safe_elim 2786 #pc' whd in match sigma_pc_opt; normalize nodelta 2787 2788 2789 2790 whd in match (succ_pc ????); 2791 2792 change with next in match (offset_of_point ???) in ⊢ (???%); 2793 whd in fetch_statement_spec : (??()%); 2794 cases cl in classified_st1_cl; -cl #classified_st1_cl whd 2795 [4: 2796 >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog) 2797 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ] 2798 #sigma_entry_is_zero #sigma_spec 2799 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1))) 2800 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ] 2801 -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec 2802 cases (opt_Exists_elim … sigma_spec) in ⊢ ?; 2803 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved 2804 #related_lin_stm_graph_stm 2805 2806 inversion (stmt_implicit_label ???) 2807 [ whd in match (opt_All ???); #stmt_implicit_spec #_ 2808 letin st2_opt' ≝ (eval_state … 2809 (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) 2810 (sigma_state_pc … wf_st1)) 2811 cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') 2812 [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' 2813 normalize nodelta in st2_spec'; -st2_opt' 2814 %{st2'} %{(taaf_step … (taa_base …) …)} 2815 [ cases daemon (* TODO, together with the previous one? *) 2816 | @st2_spec' ] 2817 %[%] [%] 2818 [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec'; 2819 >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec'; 2820 >m_return_bind 2821 (* Case analysis over the possible statements *) 2822 inversion graph_stmt in stmt_implicit_spec; normalize nodelta 2823 [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] 2824 XXXXXXXXXX siamo qua, caso GOTO e RETURN 2825 | cases daemon (* TODO, after the definition of label_rel, trivial *) ] 2826 ] 2827 | .... 2828 qed. 2829 2830 2831 2832 2833 2834 [ * 2835 [ * 2836 [ letin C_COMMENT ≝ 0 in ⊢ ?; #c 2837 | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl 2838 | letin C_MOVE ≝ 0 in ⊢ ?; #move_sig 2839 | letin C_POP ≝ 0 in ⊢ ?; #a 2840 | letin C_PUSH ≝ 0 in ⊢ ?; #a 2841 | letin C_ADDRESS ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph 2842 | letin C_OPACCS ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2 2843 | letin C_OP1 ≝ 0 in ⊢ ?; #op #a #arg 2844 | letin C_OP2 ≝ 0 in ⊢ ?; #op #a #arg1 #arg2 2845 | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?; 2846 | letin C_SET_CARRY ≝ 0 in ⊢ ?; 2847 | letin C_LOAD ≝ 0 in ⊢ ?; #a #dpl #dph 2848 | letin C_STORE ≝ 0 in ⊢ ?; #dpl #dph #a 2849 | letin C_CALL ≝ 0 in ⊢ ?; #f #args #dest 2850 | letin C_EXT ≝ 0 in ⊢ ?; #s_ext 2851 ] 2852 | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue 2853 ] #next change with label in next; 2854 | * 2855 [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl 2856 | letin C_RETURN ≝ 0 in ⊢ ?; 2857 | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args 2858 ] 2859 ] 2719 qed. -
src/joint/semantics.ma
r2551 r2556 68 68 { st_no_pc :> state semp 69 69 ; pc : program_counter 70 (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *) 71 ; last_pop : program_counter 70 72 }. 73 74 (* special program counter that is guaranteed to not correspond to anything *) 75 definition exit_pc : program_counter ≝ 76 mk_program_counter «mk_block Code (-1), refl …» one. 71 77 72 78 definition set_m: ∀p. bemem → state p → state p ≝ … … 87 93 88 94 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ 89 λp,pc,st. mk_state_pc … (st_no_pc … st) pc .95 λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st). 90 96 91 97 definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝ 92 λp,s,st. mk_state_pc … s (pc … st). 98 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st). 99 100 definition set_last_pop: ∀p. ? → state_pc p → state_pc p ≝ 101 λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s. 93 102 94 103 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ … … 356 365 λp,globals,ge,l,st. 357 366 ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ; 358 return mk_state_pc … st newpc.367 return set_pc … newpc st. 359 368 360 369 (* … … 366 375 λp,l,st. 367 376 let newpc ≝ succ_pc … (pc … st) l in 368 mk_state_pc … st newpc.377 set_pc … newpc st. 369 378 370 379 axiom NoSuccessor : String. … … 374 383 ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ; 375 384 match stmt with 376 [ sequential _ nxt ⇒ return nxt 385 [ sequential s nxt ⇒ 386 match s with 387 [ step_seq _ => return nxt 388 | COND _ _ => Error … [MSG NoSuccessor] 389 ] 377 390 | _ ⇒ Error … [MSG NoSuccessor] 378 391 ]. … … 493 506 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ; 494 507 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ; 495 return allocate_locals … p (joint_if_locals … fn) st .508 return allocate_locals … p (joint_if_locals … fn) st'. 496 509 497 510 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ]. … … 507 520 ! st'' ← eval_internal_call p globals ge i ifd args st' ; 508 521 let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in 509 return mk_state_pc … st'' pc 522 return mk_state_pc … st'' pc (last_pop … st) 510 523 | External efd ⇒ 511 524 ! st' ← eval_external_call … efd args dest st ; 512 return mk_state_pc … st' (succ_pc p (pc … st) nxt) 525 return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st) 513 526 ]. 514 527 … … 544 557 ! st' ← pop_frame … ge curr_id curr_fn st ; 545 558 ! nxt ← next_of_pc … ge (pc … st') ; 546 return next … nxt st' (* now address pushed on stack are calling ones! *). 559 return 560 set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *). 547 561 548 562 definition eval_tailcall ≝ … … 556 570 ! st' ← eval_internal_call p globals ge i ifd args st ; 557 571 let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in 558 return mk_state_pc … st' pc 572 return mk_state_pc … st' pc (last_pop … st) 559 573 | External efd ⇒ 560 574 let curr_dest ≝ joint_if_result ?? curr_fn in … … 604 618 ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???; 605 619 ! st' ← eval_statement_no_pc … ge id fn s st : IO ???; 606 let st'' ≝ mk_state_pc … st' (pc … st)in620 let st'' ≝ set_no_pc … st' st in 607 621 eval_statement_advance … ge id fn s st''. 608 622
Note: See TracChangeset
for help on using the changeset viewer.