Changeset 2592
 Timestamp:
 Jan 29, 2013, 11:20:53 AM (6 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptr.ma
r2570 r2592 16 16 include "ERTLptr/ERTLptr.ma". 17 17 include "joint/TranslateUtils.ma". 18 18 19 19 definition translate_step_seq : 20 20 ∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝ 
src/ERTLptr/ERTLtoERTLptrOK.ma
r2590 r2592 46 46 ERTLptr_semantics (pc_block pc) ertl_ptr_point. 47 47 48 49 48 definition sigma_stored_pc ≝ 50 49 λprog,sigma,pc. match sigma_pc_opt prog sigma pc with 51 [None ⇒ null_pc  Some x ⇒ x].50 [None ⇒ null_pc (pc_offset … pc)  Some x ⇒ x]. 52 51 53 52 … … 1088 1087 1089 1088 definition dummy_state_pc : state_pc ERTL_semantics ≝ 1090 mk_state_pc ? dummy_state null_pc null_pc.1089 mk_state_pc ? dummy_state (null_pc one) (null_pc one). 1091 1090 1092 1091 check fetch_internal_function … … 1684 1683 qed. 1685 1684 1685 lemma sp_ok : ∀prog : ertl_program. ∀sigma : sigma_map (ertl_to_ertlptr prog). 1686 ∀stack_size. 1687 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 1688 preserving1 … res_preserve1 … 1689 (λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn)) 1690 (λx.x) 1691 (sp ERTL_semantics) 1692 (sp ERTLptr_semantics). 1693 cases daemon 1694 qed. 1695 1696 lemma set_sp_ok : ∀prog : ertl_program. 1697 let trans_prog ≝ ertl_to_ertlptr prog in 1698 ∀sigma : sigma_map trans_prog. 1699 ∀stack_size. 1700 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 1701 ∀ptr,st. 1702 set_sp ? ptr (sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) = 1703 sigma_state trans_prog sigma (set_sp ? ptr st) (joint_if_locals ERTL ? fn). 1704 cases daemon 1705 qed. 1706 1686 1707 lemma eval_seq_no_pc_no_call_ok : 1687 1708 ∀prog : ertl_program. … … 1692 1713 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1693 1714 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1694 (eval_seq_no_pc (mk_prog_params ERTL_semantics prog stack_size)1715 (eval_seq_no_pc ERTL_semantics 1695 1716 (globals (mk_prog_params ERTL_semantics prog stack_size)) 1696 1717 (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq) 1697 (eval_seq_no_pc (mk_prog_params ERTLptr_semantics trans_prog stack_size)1718 (eval_seq_no_pc ERTLptr_semantics 1698 1719 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size)) 1699 1720 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (translate_step_seq … seq)). … … 1706 1727 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1707 1728  change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok 1708  #regs #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ]1729  #regs @mfr_return_eq1 % 1709 1730 ] 1710 1731  #r #st @mfr_bind1 … … 1716 1737 [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1717 1738  @ps_reg_store_ok 1718  #regs #x whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ]1739  #regs @mfr_return_eq1 % 1719 1740 ] 1720 1741 ] … … 1742 1763 in ⊢ (???????(?????%?)?); 1743 1764 @ps_reg_store_ok 1744  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1745 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1765  #regs @mfr_return_eq1 % 1746 1766 ] 1747 1767  #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl' … … 1754 1774 in ⊢ (???????(?????%?)?); 1755 1775 @ps_reg_store_ok 1756  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1757 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1776  #regs @mfr_return_eq1 % 1758 1777 ] 1759 1778 ] … … 1776 1795 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1777 1796  @ps_reg_store_ok 1778  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1779 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1797  #regs @mfr_return_eq1 % 1780 1798 ] 1781 1799  #st1 whd in match accb_store; normalize nodelta @mfr_bind1 … … 1783 1801  whd in match sigma_state; normalize nodelta 1784 1802 @ps_reg_store_ok 1785  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1786 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1787 ] 1803  #regs @mfr_return_eq1 % ] 1788 1804 ] 1789 1805 ] … … 1799 1815 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1800 1816  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1801  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1802 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1817  #regs @mfr_return_eq1 % 1803 1818 ] 1804 1819 ] … … 1818 1833 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1819 1834  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1820  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1821 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1835  #regs @mfr_return_eq1 % 1822 1836 ] 1823  #st1 #st2 whd in match set_carry; whd in match sigma_state; normalize nodelta 1824 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1837  #st1 @mfr_return_eq1 % 1825 1838 ] 1826 1839 ] 1827 1840 ] 1828 1841 ] 1829  #st whd in match set_carry; whd in match sigma_state; normalize nodelta 1830 #st1 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1831  #st #st1 whd in match set_carry; whd in match sigma_state; normalize nodelta 1832 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1842  #st @mfr_return_eq1 % 1843  #st @mfr_return_eq1 % 1833 1844  #r1 #dpl #dph #st @mfr_bind1 1834 1845 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) … … 1846 1857 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1847 1858  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1848  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1849 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1859  #regs @mfr_return_eq1 % 1850 1860 ] 1851 1861 ] … … 1868 1878 [ @(sigma_mem (ertl_to_ertlptr prog) sigma) 1869 1879  @opt_to_res_preserve1 @bestorev_ok 1870  #m #st1 whd in ⊢ (??%% → ?); whd in match set_m; whd in match sigma_state; 1871 normalize nodelta #EQ destruct % [2: % [%] %] 1880  #m @mfr_return_eq1 % 1872 1881 ] 1873 1882 ] … … 1875 1884 ] 1876 1885 ] 1877  #ext #st cases daemon 1886  #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f) 1887 normalize nodelta 1888 [ @res_preserve_error1 1889  #n cases ext normalize nodelta 1890 [1,2: @mfr_bind1 1891 [1,4: @(λx.x) 1892 2,5: @sp_ok 1893 3,6: #ptr @mfr_return_eq1 >set_sp_ok % 1894 ] 1895  #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1 1896 [2: whd in match sigma_state; normalize nodelta 1897 change with (sigma_beval ? sigma (BVByte ?)) in ⊢ (???????(??%?)?); 1898 @ps_reg_store_ok 1899  1900  #regs @mfr_return_eq1 % 1901 ] 1902 ] 1903 ] 1878 1904 ] 1879 1905 qed. 1906 1907 lemma fetch_statement_commute : 1908 ∀prog : ertl_program. 1909 let trans_prog ≝ (ertl_to_ertlptr prog) in 1910 ∀sigma : sigma_map trans_prog. 1911 ∀stack_sizes,id,fn,stmt,pc. 1912 fetch_statement ERTL_semantics 1913 (globals (mk_prog_params ERTL_semantics prog stack_sizes)) 1914 (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 1915 pc = return 〈id,fn,stmt〉 → 1916 match stmt with 1917 [ sequential seq nxt ⇒ 1918 match seq with 1919 [ CALL ids args dest ⇒ 1920 match ids with 1921 [ inl i ⇒ 1922 fetch_statement ERTLptr_semantics 1923 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1924 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1925 pc = 1926 return 〈id, 1927 translate_internal … fn, 1928 sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉 1929  inr p ⇒ ?(* 1930 ∃reg,lbl. 1931 fetch_statement ERTLptr_semantics 1932 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1933 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1934 pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉 1935 ∧ ∃ nxt'. 1936 ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1937 id nxt; 1938 fetch_statement ERTLptr_semantics 1939 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1940 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1941 pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉 1942 ∧ ∃ nxt''. 1943 ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1944 id nxt'; 1945 fetch_statement ERTLptr_semantics 1946 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1947 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1948 pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉 1949 ∧ ∃ nxt'''. 1950 ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1951 id nxt''; 1952 fetch_statement ERTLptr_semantics 1953 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1954 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1955 pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉 1956 ∧ ∃ nxt''''. 1957 ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1958 id nxt'''; 1959 fetch_statement ERTLptr_semantics 1960 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1961 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1962 pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉 1963 ∧ sigma (translate_internal … fn) nxt''' = return point_of_pc ERTL_semantics pc *) 1964 ] 1965  COND r lbl ⇒ 1966 fetch_statement ERTLptr_semantics 1967 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1968 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1969 pc = 1970 return 〈id, 1971 translate_internal … fn, 1972 sequential ?? (COND ERTLptr ? r lbl) nxt〉 1973  step_seq s ⇒ 1974 fetch_statement ERTLptr_semantics 1975 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1976 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1977 pc = 1978 return 〈id, 1979 translate_internal … fn, 1980 sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉 1981 ] 1982  final fin ⇒ 1983 fetch_statement ERTLptr_semantics 1984 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1985 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 1986 pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉 1987  FCOND abs _ _ _ ⇒ Ⓧabs 1988 ]. 1989 cases daemon 1990 qed. 1991 1992 lemma eval_seq_no_call_ok : 1993 ∀prog. 1994 let trans_prog ≝ ertl_to_ertlptr prog in 1995 ∀sigma : sigma_map trans_prog.∀stack_sizes. 1996 (*? →*) 1997 ∀st,st',f,fn,stmt,nxt. 1998 fetch_statement ERTL_semantics 1999 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2000 (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 2001 (pc … (sigma_state_pc ? sigma st)) = 2002 return 〈f, fn, sequential … (step_seq ERTL … stmt) nxt〉 → 2003 eval_state ERTL_semantics 2004 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2005 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2006 (sigma_state_pc ? sigma st) = 2007 return st' → 2008 ∃st''. st' = sigma_state_pc ? sigma st'' ∧ 2009 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2010 st 2011 st''. 2012 bool_to_Prop (taaf_non_empty … taf). 2013 #prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state; 2014 normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 2015 whd in match eval_statement_no_pc; normalize nodelta 2016 #H @('bind_inversion H) H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) EQ 2017 #EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf 2018 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim 2019 [ #EQbl 2020  #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_] 2021 ] 2022 [1,2: whd in match dummy_state_pc; whd in match null_pc; 2023 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function; 2024 normalize nodelta lapply(fetch_function_no_zero ??????) 2025 [2,9: @( «mk_block Code OZ,refl region Code») 2026 1,8: % 3,10: @prog 7,14: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2027 * #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #fn1_spec normalize nodelta 2028 whd in match fetch_statement; normalize nodelta >fn1_spec 2029 >m_return_bind #H @('bind_inversion H) H #stmt1 #EQ 2030 lapply(opt_eq_from_res ???? EQ) EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct 2031 lapply EQeval EQeval whd in match sigma_state_pc in ⊢ (% → ?); 2032 normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec 2033 normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval) 2034 #st_no_pc' * #EQeval' #EQst_no_pc' 2035 whd in match set_no_pc; normalize nodelta 2036 % [ % [@st_no_pc'@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1)) 2037 nxt) @(last_pop ? st1)]] 2038 % [ whd in match sigma_state_pc; normalize nodelta 2039 @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta 2040 @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta 2041 >EQst_no_pc' %] 2042 %{(taaf_step … (taa_base …) …)} 2043 [3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta 2044 whd in match sigma_state_pc; normalize nodelta 2045 @if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta 2046 #EQf1 2047 [ whd in match as_classifier; normalize nodelta whd in match (as_classify ??); 2048 >EQf1 normalize nodelta % 2049  whd in match (as_execute ???); whd in match eval_state; normalize nodelta 2050 >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta 2051 >EQeval' >m_return_bind % 2052 ] 2053 qed. 2054 2055 lemma pc_of_label_eq : 2056 ∀globals,ge,bl,i_fn,lbl. 2057 fetch_internal_function ? ge bl = return i_fn → 2058 pc_of_label ERTL_semantics globals ge bl lbl = 2059 OK ? (pc_of_point ERTL_semantics bl lbl). 2060 #globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label; 2061 normalize nodelta >EQf % 2062 qed. 2063 2064 lemma eval_goto_ok : 2065 ∀prog : ertl_program. 2066 let trans_prog ≝ ertl_to_ertlptr prog in 2067 ∀stack_sizes. 2068 ∀sigma : sigma_map trans_prog. 2069 ∀st,st',f,fn,nxt. 2070 fetch_statement ERTL_semantics … 2071 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2072 return 〈f, fn, final … (GOTO ERTL … nxt)〉 → 2073 eval_state ERTL_semantics 2074 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2075 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2076 (sigma_state_pc ? sigma st) = 2077 return st' → 2078 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2079 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2080 st 2081 st''. 2082 bool_to_Prop (taaf_non_empty … taf). 2083 #prog #stack_sizes #sigma #st #st' #f #fn #nxt 2084 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2085 @if_elim 2086 [ #EQbl whd in match dummy_state_pc; whd in match null_pc; 2087 whd in match fetch_statement; whd in match fetch_internal_function; 2088 normalize nodelta lapply(fetch_function_no_zero ??????) 2089 [2: @( «mk_block Code OZ,refl region Code») 2090  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2091 #Hbl inversion(fetch_internal_function ???) 2092 [2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; 2093 whd in match fetch_statement; whd in match fetch_internal_function; 2094 normalize nodelta lapply(fetch_function_no_zero ??????) 2095 [2: @( «mk_block Code OZ,refl region Code») 2096  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2097 * #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #fn1_spec normalize nodelta 2098 #EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec 2099 >m_return_bind #H @('bind_inversion H) H #stmt' #_ whd in ⊢ (??%% → ?); 2100 #EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2101 @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state; 2102 normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 2103 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 2104 whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) H 2105 #H @('bind_inversion H) H #pc' whd in match set_no_pc; normalize nodelta 2106 >(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1 2107 destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf) 2108 normalize nodelta #EQf' % 2109 [ % [ @st 2110  @(mk_program_counter 2111 (pc_block (pc ERTLptr_semantics st)) 2112 (offset_of_point ERTL_semantics nxt)) 2113  @(last_pop … st) 2114 ] 2115 ] % 2116 [ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *] 2117 >fn1_spec normalize nodelta #_ % ] 2118 %{(taaf_step … (taa_base …) …)} 2119 [ whd in match as_classifier; normalize nodelta whd in match (as_classify ??); 2120 >EQf' normalize nodelta % 2121  whd in match (as_execute ???); whd in match eval_state; normalize nodelta 2122 >EQf' >m_return_bind whd in match eval_statement_no_pc; 2123 whd in match eval_statement_advance; normalize nodelta >m_return_bind 2124 whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta 2125 lapply(fetch_internal_function_transf ??????? fn1_spec) 2126 [ #vars @translate_internal ] #EQ >EQ >m_return_bind % 2127  % 2128 ] 2129 qed. 2130 2131 axiom partial_inj_sigma : ∀ prog : ertlptr_program. 2132 ∀sigma :sigma_map prog. 2133 ∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2. 2134 2135 lemma pop_ra_ok : 2136 ∀prog : ertl_program. 2137 let trans_prog ≝ ertl_to_ertlptr prog in 2138 ∀sigma : sigma_map trans_prog. 2139 ∀stack_size. 2140 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 2141 preserving1 … res_preserve1 … 2142 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 2143 (λx.let 〈st,pc〉 ≝ x in 2144 〈sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn), 2145 sigma_stored_pc ? sigma pc〉) 2146 (pop_ra ERTL_semantics) 2147 (pop_ra ERTLptr_semantics). 2148 #prog #sigma #stack_size #fn #st whd in match pop_ra; normalize nodelta @mfr_bind1 2149 [  @pop_ok ] * #bv #st1 @mfr_bind1 [  @pop_ok] * #bv1 #st2 @mfr_bind1 2150 [ @(sigma_stored_pc ? sigma)  whd in match pc_of_bevals; normalize nodelta 2151 cases bv [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p] 2152 whd in match sigma_beval; normalize nodelta try @res_preserve_error1 2153 inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1] 2154 #sigma_pc #sigma_pc_spec normalize nodelta cases bv1 2155 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 2156 normalize nodelta try @res_preserve_error1 2157 inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1] 2158 #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1] 2159 @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *] 2160 #_ #H >H @eq_program_counter_elim [2: #_ *] 2161 #EQspc * @eq_program_counter_elim 2162 [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta 2163 >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec 2164 whd in match sigma_pc_opt; normalize nodelta @if_elim 2165 [ #H2 #EQ lapply(sym_eq ??? EQ) EQ @if_elim [#_ whd in ⊢ (??%% → ?); #EQ destruct %] 2166 #H3 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 2167 cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; * 2168  #H2 @if_elim 2169 [ #H3 #H @('bind_inversion H) H #x1 #_ #H @('bind_inversion H) H #lbl1 #_ 2170 cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?); 2171 #EQ destruct >H3 in H2; * 2172  #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim 2173 [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) EQ #x #x_spec 2174 lapply(res_eq_from_opt ??? x_spec) x_spec #x_spec #H @('bind_inversion H) * #lbl 2175 #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1 2176 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2 2177 #H @('bind_inversion H) H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) x1_spec #x1_spec 2178 #H @('bind_inversion H) H * #lbl2 #lbl2_spec 2179 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct 2180 <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct 2181 lapply(partial_inj_sigma (ertl_to_ertlptr prog) sigma ???? EQsig) 2182 [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta 2183 whd in match (point_of_offset ??); whd in match (point_of_offset ??); 2184 #EQ destruct cases pc1 #bl #p % 2185 ] 2186 ] 2187  #pc @mfr_return_eq1 % 2188 ] 2189 qed. 2190 2191 lemma pc_block_eq : ∀prog : ertl_program. 2192 let trans_prog ≝ ertl_to_ertlptr prog in 2193 ∀sigma : sigma_map trans_prog. 2194 ∀pc,id,fn. 2195 fetch_internal_function (joint_closed_internal_function ERTLptr 2196 (prog_var_names (joint_function ERTLptr) ℕ trans_prog)) 2197 (globalenv_noinit (joint_function ERTLptr) trans_prog) (pc_block … pc) = return 〈id,fn〉→ 2198 sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? → 2199 pc_block … pc = pc_block … (sigma_stored_pc trans_prog sigma pc). 2200 #prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc; 2201 normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %] 2202 #_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind % 2203 qed. 2204 2205 2206 2207 lemma eval_return_ok : 2208 ∀prog : ertl_program. 2209 let trans_prog ≝ ertl_to_ertlptr prog in 2210 ∀stack_sizes. 2211 ∀sigma : sigma_map trans_prog. 2212 ∀st,st',f,fn. 2213 fetch_statement ERTL_semantics … 2214 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2215 return 〈f, fn, final … (RETURN ERTL … )〉 → 2216 eval_state ERTL_semantics 2217 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2218 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2219 (sigma_state_pc ? sigma st) = 2220 return st' → 2221 joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) 2222 st = Some ? cl_return ∧ 2223 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2224 ∃st2_after_ret. 2225 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2226 st2_after_ret 2227 st''. 2228 (if taaf_non_empty … taf then 2229 ¬as_costed (ERTLptr_status trans_prog stack_sizes) 2230 st2_after_ret 2231 else True) ∧ 2232 eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st = 2233 return st2_after_ret ∧ 2234 ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret. 2235 #prog #stack_size #sigma #st #st' #f #fn 2236 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2237 @if_elim 2238 [ #EQbl whd in match dummy_state_pc; whd in match null_pc; 2239 whd in match fetch_statement; whd in match fetch_internal_function; 2240 normalize nodelta lapply(fetch_function_no_zero ??????) 2241 [2: @( «mk_block Code OZ,refl region Code») 2242  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2243 #Hbl inversion(fetch_internal_function ???) 2244 [2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; 2245 whd in match fetch_statement; whd in match fetch_internal_function; 2246 normalize nodelta lapply(fetch_function_no_zero ??????) 2247 [2: @( «mk_block Code OZ,refl region Code») 2248  %  @prog 7: #EQ >EQ *:] whd in ⊢ (??%% → ?); #EQ destruct] 2249 * #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #fn1_spec normalize nodelta 2250 #EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec 2251 >m_return_bind #H @('bind_inversion H) H #stmt' #_ whd in ⊢ (??%% → ?); 2252 #EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta 2253 @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta 2254 whd in match eval_state; normalize nodelta >EQf >m_return_bind 2255 whd in match eval_statement_no_pc; whd in match eval_statement_advance; 2256 normalize nodelta >m_return_bind 2257 #H lapply (err_eq_from_io ????? H) H #H @('bind_inversion H) H 2258 * #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta 2259 >m_bind_bind #H @('bind_inversion H) H ** #f1 #fn2 * normalize nodelta 2260 [ * [ #c_id #args #dest  #r #lbl  #seq ] #nxt  #fin  * ] 2261 #EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct] 2262 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 2263 lapply (fetch_statement_commute prog sigma stack_size … EQf) 2264 normalize nodelta #EQf' 2265 % [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %] 2266 cases(pop_ra_ok ? sigma stack_size ??? EQpop) * #st3 #pc3 * #st3_spec 2267 normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc; 2268 normalize nodelta whd in match (point_of_succ ???); 2269 % [ % [ @st3  @(pc_of_point ERTL_semantics (pc_block … pc3) nxt)  @pc3] ] 2270 % [ @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc; 2271 normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta 2272 [ #_ #H @('bind_inversion H) H #x whd in match null_pc; normalize nodelta 2273 >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct 2274  #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim 2275 [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) H 2276 #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct] 2277 lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc; 2278 normalize nodelta whd in match sigma_pc_opt; normalize nodelta 2279 >bl3_spec normalize nodelta assumption 2280  #bl3_spec #H @('bind_inversion H) H * #fn4 #id4 2281 #H lapply(res_eq_from_opt ??? H) H #fn4_spec 2282 #H @('bind_inversion H) H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ 2283 destruct #fn3_spec #H @('bind_inversion H) H #stmt1 #_ 2284 whd in ⊢ (??%% → ?); #EQ destruct 2285 >(fetch_internal_function_transf … fn3_spec) in fn4_spec; 2286 whd in ⊢ (??%% → ?); #EQ destruct 2287 ] 2288 ] 2289 whd in match sigma_state_pc; normalize nodelta @if_elim 2290 [ >(pc_block_eq prog sigma ????) in bl3_spec; 2291 [2: >lbl4_spec % #ABS destruct 2292 3: >(fetch_internal_function_transf … fn3_spec) % *:] 2293 #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; * 2294  #_ inversion(fetch_internal_function ???) [#x #_ normalize nodelta % cases daemon (*serve lemma sul fetch della call *) 2295 xxxxxxxxxxxxxxx 2296  2297 whd in match sigma_state_pc; normalize nodelta @if_elim 2298 2299 qed. 2300 2301 lemma eval_tailcall_ok : 2302 ∀prog. 2303 let trans_prog ≝ ertl_to_ertlptr prog in 2304 ∀stack_sizes. 2305 ∀sigma : sigma_map trans_prog. 2306 ∀st,st',f,fn,fl,called,args. 2307 fetch_statement ERTL_semantics … 2308 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2309 return 〈f, fn, final … (TAILCALL ERTL … fl called args)〉 → 2310 eval_state ERTL_semantics 2311 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2312 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2313 (sigma_state_pc ? sigma st) = 2314 return st' → 2315 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2316 ∃is_tailcall, is_tailcall'. 2317 joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» = 2318 joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧ 2319 eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) 2320 st = return st''. 2321 cases daemon 2322 qed. 2323 2324 lemma eval_cond_ok : 2325 ∀prog. 2326 let trans_prog ≝ ertl_to_ertlptr prog in 2327 ∀stack_sizes. 2328 ∀sigma : sigma_map trans_prog. 2329 ∀st,st',f,fn,a,ltrue,lfalse. 2330 fetch_statement ERTL_semantics … 2331 (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) = 2332 return 〈f, fn, sequential … (COND ERTL … a ltrue) lfalse〉 → 2333 eval_state ERTL_semantics 2334 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2335 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2336 (sigma_state_pc ? sigma st) = 2337 return st' → 2338 as_costed (ERTL_status prog stack_sizes) 2339 st' → 2340 ∃ st''. st' = sigma_state_pc ? sigma st'' ∧ 2341 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2342 st st''. 2343 bool_to_Prop (taaf_non_empty … taf). 2344 cases daemon 2345 qed. 2346 1880 2347 1881 2348 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ … … 1883 2350 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 1884 2351 1885 lemma linearise_ok: 2352 lemma 2353 find_funct_ptr_none: 2354 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). 2355 ∀b: block. 2356 find_funct_ptr ? (globalenv … iV p) b = None ? → 2357 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?. 2358 #A #B #V #i #p #transf #b 2359 whd in match find_funct_ptr; normalize nodelta 2360 cases b b * normalize nodelta [#x #_ %] * normalize nodelta 2361 [1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta 2362 whd in match globalenv_allocmem; normalize nodelta 2363 cases daemon (*forse e' falso *) 2364 qed. 2365 2366 lemma as_label_ok : ∀ prog : ertl_program. 2367 let trans_prog ≝ ertl_to_ertlptr prog in 2368 ∀ sigma : sigma_map trans_prog. 2369 ∀stack_sizes. 2370 ∀ st. 2371 as_label (ERTLptr_status trans_prog stack_sizes) st = as_label 2372 (ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st). 2373 #prog #sigma #stack_size * #st #pc #lp 2374 whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%); 2375 whd in match (as_label_of_pc ??) in ⊢ (??%%); 2376 2377 2378 (* 2379 2380 whd in match fetch_statement; normalize nodelta 2381 whd in match sigma_state_pc; normalize nodelta @if_elim 2382 [ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind 2383 lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc)  lapply EQbl 2384 @eqZb_elim #H * @H @(ertl_to_ertlptr prog) 7: #EQ >EQ *:] normalize nodelta 2385 whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc; 2386 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function; 2387 normalize nodelta >m_bind_bind 2388 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code») 2389  %  @prog 7: #EQ >EQ *:] % 2390  inversion ( fetch_internal_function 2391 (joint_closed_internal_function ERTL 2392 (prog_var_names (joint_function ERTL) ℕ prog)) 2393 (globalenv_noinit (joint_function ERTL) prog) (pc_block pc)) 2394 [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec) 2395 [ @(λvars,fn.translate_internal … fn) ] #EQ >EQ >m_return_bind normalize nodelta 2396 whd in match (as_label_of_pc ??); 2397 whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind 2398 cases daemon (*serve specifica su sigma TODO*) 2399  #err #EQ lapply(jmeq_to_eq ??? EQ) EQ #fetch_err #_ normalize nodelta 2400 whd in match dummy_state_pc; 2401 whd in match (as_label_of_pc ??); whd in match null_pc; 2402 whd in match fetch_statement; normalize nodelta 2403 whd in match fetch_internal_function in ⊢ (???%); 2404 normalize nodelta 2405 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code») 2406  %  @prog 7: #EQ >EQ in ⊢ (???%); *:] normalize nodelta EQ 2407 lapply fetch_err fetch_err whd in match fetch_internal_function; normalize nodelta 2408 inversion(fetch_function ???) 2409 [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct] 2410 #EQ destruct lapply(jmeq_to_eq ??? fn_spec) fn_spec #fn_spec 2411 lapply(fetch_function_transf ????????? fn_spec) [ #v @transf_fundef [2:@translate_internal ]] 2412 #EQ >EQ >m_return_bind % 2413  #err1 #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct 2414 normalize nodelta lapply EQfetch EQfetch whd in match fetch_function; 2415 normalize nodelta check joint_function 2416 lapply(symbol_for_block_transf ? ? ? ? prog (λvars.?) (pc_block pc)) 2417 [@transf_fundef [2: @translate_internal] 4: #EQ >EQ in ⊢ (? → %); *:] 2418 cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %] 2419 #id >m_return_bind inversion(find_funct_ptr ???) 2420 [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct] 2421 #EQf whd in ⊢ (??%? → ?); #EQ destruct 2422 lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*) 2423 [#vars @transf_fundef [2: @translate_internal]] 2424 #EQ >EQ % 2425 ] 2426 ] 2427 ]*) 2428 cases daemon 2429 qed. 2430 2431 2432 lemma ertl_to_ertlptr_ok: 1886 2433 ∀prog. 1887 2434 let trans_prog ≝ ertl_to_ertlptr prog in … … 1894 2441 whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta 1895 2442 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 1896 whd in match eval_state; normalize nodelta @('bind_inversion) ** #id #fn #stmt 1897 #H lapply (err_eq_from_io ????? H) H #EQfetch @('bind_inversion) #st #EQst 1898 #EQst1' whd in match ERTLptrStatusSimulation; normalize nodelta 1899 #EQsim whd in match joint_abstract_status in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 1900 normalize nodelta whd in match joint_classify; normalize nodelta >EQfetch 1901 >m_return_bind cases stmt in EQst EQst1'; stmt normalize nodelta 1902 [ * [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  (*FCOND absurd*) cases daemon] 1903 [3: whd in match joint_classify_step; normalize nodelta whd in match eval_statement_no_pc; 1904 normalize nodelta #H1 whd in match eval_statement_advance; normalize nodelta 1905 whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta 1906 #EQtobdest >EQsim in H1; #H1 cases(eval_seq_no_pc_no_call_ok ????????? H1) 1907 [2: cases daemon (*TODO*)] #st' * #st_spec' #st_sim % 1908 [% [ @st' @(pc … st1')  @(last_pop … st1')]] 1909 check taa_base 1910 %{(taaf_step ???? (taa_base … st2) ? ?)} 1911 [(*dalla commutazione del fetch TODO*) cases daemon 1912  whd in match (as_execute ???); whd in match eval_state; normalize nodelta 1913 cases daemon (*dalla commutazione del fetch + st_spec' TODO *) 1914 ] normalize nodelta % [% // cases daemon (*facile TODO *)] whd in match label_rel; 1915 normalize nodelta (*specifica di sigma TODO *) cases daemon 1916  1917 1918 1919 1920 >EQsim in EQfetch; whd in match sigma_state_pc in ⊢ (%→ ?); 1921 whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) H 1922 * #id1 #fn1 whd in match fetch_internal_function; normalize nodelta 1923 #H @('bind_inversion H) H * #id2 #fn2 @if_elim #block_st2_spec 1924 [whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1925 lapply(fetch_function_no_zero ??????) 1926 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1927 whd in ⊢ (???% → ?); #ABS destruct] 1928 inversion(fetch_function 1929 (fundef 1930 (joint_closed_internal_function ERTLptr 1931 (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog)))) 1932 (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog)) 1933 (pc_block (pc ERTLptr_semantics st2))) 1934 [2: #err #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1935 lapply(fetch_function_no_zero ??????) 1936 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1937 whd in ⊢ (???% → ?); #ABS destruct] * #id3 #fn3 #EQ lapply(jmeq_to_eq ??? EQ) EQ 1938 #EQffst2 >m_return_bind cases fn3 in EQffst2; fn3 [2: #ext #_ normalize nodelta 1939 whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1940 lapply(fetch_function_no_zero ??????) 1941 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1942 whd in ⊢ (???% → ?); #ABS destruct] #fn3 #fn3_spec normalize nodelta 1943 #fn2_spec >(fetch_function_transf ??????????) in fn3_spec; [2: @fn2_spec*:] 1944 cases fn2 in fn2_spec; fn2 #fn2 #fn2_spec whd in match transf_fundef; 1945 normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct whd in ⊢ (??%% → ?); #EQ destruct 1946 #H @('bind_inversion H) H #stmt1 #H lapply(opt_eq_from_res ???? H) H #stmt1_spec 1947 whd in ⊢ (??%% → ?); #EQ destruct cases stmt in stmt1_spec EQst1' EQst; stmt 1948 [* [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  (*FCOND absurd*) cases daemon] 1949 #stmt_spec whd in match eval_statement_advance; normalize nodelta whd in match eval_call; 1950 normalize nodelta #EQst1' whd in match eval_statement_no_pc; normalize nodelta 1951 [3: #H cases(eval_seq_no_pc_no_call_ok ????????? H) [2: whd in match fetch_internal_function; 1952 normalize nodelta whd in match sigma_state_pc; normalize nodelta @if_elim 1953 [ #H1 >H1 in block_st2_spec; *] #_ whd in match fetch_internal_function; normalize nodelta 1954 >(fetch_function_transf ??????????) [2: @fn2_spec *: ] whd in match transf_fundef; 1955 normalize nodelta >fn2_spec >m_return_bind %] #st3 * #st3_spec #sem_rel 1956 % [ % [ @st3  @(pc … st1')  @(last_pop … st2)]] % [%2 [2: %11:4: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); normalize nodelta 1957 1958 %{(taaf_step … (taa_base …) …) I} 1959 1960 1961 [1,2,4: whd in ⊢ (??%% → ?); #EQ destruct 1962 3: whd in EQst1' : (??%%); whd in match set_no_pc in EQst1'; normalize nodelta in EQst1'; 1963 whd in match sigma_state_pc in EQst1'; normalize nodelta in EQst1'; 1964 >block_st2_spec in EQst1'; @if_elim [ #H >H in block_st2_spec; *] #_ 1965 whd in match fetch_internal_function; normalize nodelta >(fetch_function_transf ??????????) [2: @fn2_spec*:] 1966 >m_return_bind whd in match transf_fundef; normalize nodelta whd in match next; 1967 normalize nodelta whd in match set_pc; normalize nodelta #EQ destruct #H 1968 1969 1970 1971 1972 whd ;in match in EQst1'; 1973 destruct #EQst 1974 #EQst normalize nodelta 1975 [ whd in match joint_classify_step; normalize nodelta 1976 1977 1978 1979 lapply(fetch_function_no_zero ??????) [2: @(«mk_block Code OZ,refl region Code») 1980 2: %  %7: #EQ >EQ *: try assumption 1981 1982 normalize in ⊢ (%→ ?); 1983 normalize in as_ex; 1984 1985 1986 2443 change with 2444 (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) 2445 #EQeval @('bind_inversion EQeval) 2446 ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) H #EQfetch 2447 #_ whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct 2448 cases stmt in EQfetch; stmt 2449 [ * [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  *] 2450 normalize nodelta #EQfetch 2451 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2452 [ (*CALL*) 2453 cases daemon (*TODO*) 2454  whd in match joint_classify; normalize nodelta 2455 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2456 normalize nodelta 2457 #n_cost 2458 cases (eval_cond_ok … EQfetch EQeval n_cost) 2459 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} 2460 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok % 2461  whd in match joint_classify; normalize nodelta 2462 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2463 normalize nodelta 2464 cases (eval_seq_no_call_ok ????????? EQfetch EQeval) 2465 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta 2466 % [% //] whd >as_label_ok [2:assumption] % 2467  (*FIN*) 2468 cases fin_step in EQfetch; 2469 [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta 2470 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2471 cases (eval_goto_ok … EQfetch EQeval) 2472 #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta 2473 % [% //] whd >as_label_ok [2:assumption] % 2474  (*RETURN*) #EQfetch 2475 whd in match joint_classify; normalize nodelta 2476 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2477 cases (eval_return_ok … EQfetch EQeval) #is_ret 2478 * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf 2479 % [2: % [2: % [2: %{(taa_base …)} %{taf}] *: ] *:] 2480 % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption] 2481 % assumption 2482  (*TAILCALL*) #fl #called #args #EQfetch 2483 cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall 2484 * #is_tailcall' * #eq_call #EQeval' >is_tailcall normalize nodelta 2485 #prf %{«?, is_tailcall'»} %{eq_call} 2486 % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} % ]  ]  ] 2487 whd >as_label_ok % 2488 ] 2489 ] 2490 qed. 2491 2492 2493 
src/joint/semantics.ma
r2590 r2592 77 77 mk_program_counter «mk_block Code (1), refl …» one. 78 78 79 definition null_pc : program_counter ≝80 mk_program_counter «mk_block Code OZ, refl …» one.79 definition null_pc : Pos → program_counter ≝ λpos. 80 mk_program_counter «mk_block Code OZ, refl …» pos. 81 81 82 82 definition set_m: ∀p. bemem → state p → state p ≝
Note: See TracChangeset
for help on using the changeset viewer.