Changeset 1880 for src/RTLabs/Traces.ma
 Timestamp:
 Apr 6, 2012, 4:57:22 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1877 r1880 31 31 ]. 32 32 33 definition RTLabs_status : genv → abstract_status ≝33 definition RTLabs_status : genv → final_abstract_status ≝ 34 34 λge. 35 mk_abstract_status 35 mk_final_abstract_status 36 (mk_abstract_status 36 37 state 37 38 (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) … … 50 51  _ ⇒ λH.⊥ 51 52 ] p 52 ]). 53 [ normalize in H; destruct 54  normalize in H; destruct 55  whd in H:(??%?); 53 ])) 54 (λs. RTLabs_is_final s ≠ None ?). 55 [ whd in H:(??%?); 56 56 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; 57 57 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 58  normalize in H; destruct 59  normalize in H; destruct 58 60 ] qed. 59 61 … … 79 81  ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s 80 82  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s 81  ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.83  ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s. 82 84 83 85 coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝ … … 94 96 95 97 let corec make_flat_trace ge s 98 (NF:RTLabs_is_final s = None ?) 96 99 (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 97 100 flat_trace io_out io_in ge s ≝ … … 99 102 match e return λx. e = x → ? with 100 103 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) 101  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ? )102  e_wrong m ⇒ λE. ft_wrong … s m ? 104  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??) 105  e_wrong m ⇒ λE. ft_wrong … s m ?? 103 106  e_interact o f ⇒ λE. ⊥ 104 107 ] (refl ? e). … … 145 148  whd in E:(??%?); >exec_inf_aux_unfold in E; 146 149 cases (eval_statement ge s) 150 [ #o #K whd in ⊢ (??%? → ?); #E destruct 151  * #tr #s1 whd in ⊢ (??%? → ?); 152 lapply (refl ? (RTLabs_is_final s1)) 153 change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?_⇒?])? → ?); 154 cases (RTLabs_is_final s1) in ⊢ (???% → %); 155 [ #F #E whd in E:(??%?); destruct @F 156  #r #F #E whd in E:(??%?); destruct 157 ] 158  #m #E whd in E:(??%?); destruct 159 ] 160  @NF 161  whd in E:(??%?); >exec_inf_aux_unfold in E; 162 cases (eval_statement ge s) 147 163 [ #O #K whd in ⊢ (??%? → ?); #E destruct 148 164  * #tr1 #s1 whd in ⊢ (??%? → ?); … … 169 185 match e return λx. e = x → ? with 170 186 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? 171  e_step _ _ e' ⇒ λE. make_flat_trace ge s ? 187  e_step _ _ e' ⇒ λE. make_flat_trace ge s ?? 172 188  e_wrong m ⇒ λE. ⊥ 173 189  e_interact o f ⇒ λE. ⊥ … … 175 191 [ whd in E:(??%?); >exec_inf_aux_unfold in E; 176 192 whd in ⊢ (??%? → ?); 177 >(?:is_final ????? = RTLabs_is_final s) //178 lapply (refl ? (RTLabs_is_final s))179 cases (RTLabs_is_final s) in ⊢ (???% → %);180 [ #_ whd in ⊢ (??%? → ?); #Edestruct181  #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct182 ] 193 change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?_⇒?])? → ?); 194 cases (RTLabs_is_final s) 195 [ #E whd in E:(??%?); destruct 196  #r #E % #E' destruct 197 ] 198  @(initial_state_is_not_final … I) 183 199  whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); 184 200 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) … … 1014 1030 ] (refl ? (RTLabs_classify start)) 1015 1031 1016  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥1032  ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 1017 1033 1018 1034 ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME … … 1176 1192 [ St_skip l ⇒ [l] 1177 1193  St_cost _ l ⇒ [l] 1178  St_const _ _ l ⇒ [l]1194  St_const _ _ _ l ⇒ [l] 1179 1195  St_op1 _ _ _ _ _ l ⇒ [l] 1180 1196  St_op2 _ _ _ _ _ _ _ l ⇒ [l] … … 1220 1236 [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1221 1237  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1222  # r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //1238  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1223 1239  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1224 1240  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // … … 1312 1328 [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1313 1329  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1314  # r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl1330  #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1315 1331  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1316 1332  #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl … … 1608 1624  cl_return ⇒ λCL. ⊥ 1609 1625 ] (refl ??) 1610  ft_wrong start m EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥1626  ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ 1611 1627 ] TRACE_OK 1612 1628 ] LABEL_LIMIT. … … 1677 1693 inversion (ro_not_undefined … TRACE_OK) 1678 1694 [ #H137 #H138 #H139 #H140 #H141 destruct 1679  #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct1695  #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct 1680 1696 inversion H148 1681 1697 [ #H153 #H154 #H155 #H156 #H157 destruct … … 1746 1762 ] qed. 1747 1763 1748 let rec whole_structured_trace_exists ge s 1764 lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'. 1765 make_initial_state p = OK ? s1 → 1766 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 1767 stack_preserved ends_with_ret s2 s' → 1768 RTLabs_is_final s' ≠ None ?. 1769 #ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?); 1770 @bind_ok #m #_ 1771 @bind_ok #b #_ 1772 @bind_ok #f #_ 1773 #E destruct 1774 #EV #SP inversion (eval_perserves … EV) 1775 [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct 1776 inversion SP 1777 [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct 1778  *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct 1779 inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct 1780 ] 1781  *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct 1782 ] qed. 1783 1784 lemma initial_state_is_call : ∀p,s. 1785 make_initial_state p = OK ? s → 1786 RTLabs_classify s = cl_call. 1787 #p #s whd in ⊢ (??%? → ?); 1788 @bind_ok #m #_ 1789 @bind_ok #b #_ 1790 @bind_ok #f #_ 1791 #E destruct 1792 @refl 1793 qed. 1794 1795 let rec whole_structured_trace_exists ge p s 1749 1796 (trace: flat_trace io_out io_in ge s) 1750 1797 (ORACLE: termination_oracle) 1751 1798 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1752 1799 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1753 : ∀I S_CALL: RTLabs_classify s = cl_call.1754 ∀NOT_WRONG: not_wrong …s trace.1800 : ∀INITIAL: make_initial_state p = OK ? s. 1801 ∀NOT_WRONG: not_wrong ??? s trace. 1755 1802 ∀STATE_COSTLABELLED: well_cost_labelled_state s. 1756 1803 ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s. 1757 1804 trace_whole_program_exists (RTLabs_status ge) s ≝ 1758 match trace return λs,trace. RTLabs_classify s = cl_call→1759 not_wrong …s trace →1805 match trace return λs,trace. make_initial_state p = OK ? s → 1806 not_wrong ??? s trace → 1760 1807 well_cost_labelled_state s → 1761 1808 soundly_labelled_state s → 1762 1809 trace_whole_program_exists (RTLabs_status ge) s with 1763 [ ft_step s tr next EV trace' ⇒ λIS_CALL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. 1810 [ ft_step s tr next EV trace' ⇒ λINITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. 1811 let IS_CALL ≝ initial_state_is_call … INITIAL in 1764 1812 match ORACLE ge O next trace' with 1765 1813 [ or_introl TERMINATES ⇒ … … 1767 1815 [ witness TERMINATES ⇒ 1768 1816 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in 1769 twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) 1817 twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) ? 1770 1818 ] 1771 1819  or_intror NO_TERMINATION ⇒ … … 1774 1822 ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?) 1775 1823 ] 1776  ft_stop st FINAL ⇒ λI S_CALL,NOT_WRONG. ⊥1777  ft_wrong start m EV ⇒ λIS_CALL,NOT_WRONG. ⊥1824  ft_stop st FINAL ⇒ λINITIAL,NOT_WRONG. ⊥ 1825  ft_wrong start m NF EV ⇒ λINITIAL,NOT_WRONG. ⊥ 1778 1826 ]. 1779 [ cases (rtlabs_call_inv … IS_CALL) #fn * #args * #dst * #stk * #m #E destruct1827 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct 1780 1828 cases FINAL #E @E @refl 1781 1829  %{tr} @EV 1830  @(after_the_initial_call_is_the_final_state … INITIAL EV) 1831 @(stack_ok … tlr) 1782 1832  @(well_cost_labelled_state_step … EV) // 1783 1833  @(well_cost_labelled_call … EV) // … … 1819 1869 [ whd 1820 1870 *) 1871 1872 (* as_execute might be in Prop, but because the semantics is deterministic 1873 we can retrieve the event trace anyway. *) 1874 let rec deprop_as_execute ge s s' 1875 (X:as_execute (RTLabs_status ge) s s') 1876 : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝ 1877 match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ? with 1878 [ Value ts ⇒ λY. «fst … ts, ?» 1879  _ ⇒ λY. ⊥ 1880 ] X. 1881 [ 1,3: cases Y #x #E destruct 1882  cases Y #trP #E destruct @refl 1883 ] qed. 1884 1885 (* A nonempty finite section of a flat_trace *) 1886 inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝ 1887  pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s' 1888  pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''. 1889 1890 let rec append_partial_flat_trace o i ge s1 s2 s3 1891 (tr1:partial_flat_trace o i ge s1 s2) 1892 on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝ 1893 match tr1 with 1894 [ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX 1895  pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2) 1896 ]. 1897 1898 let rec partial_to_flat_trace o i ge s1 s2 1899 (tr:partial_flat_trace o i ge s1 s2) 1900 on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝ 1901 match tr with 1902 [ pft_base s tr s' EX ⇒ ft_step … EX 1903  pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'') 1904 ]. 1905 1906 (* Extract a flat trace from a structured one. *) 1907 let rec flatten_trace_label_return ge s s' 1908 (tr:trace_label_return (RTLabs_status ge) s s') 1909 on tr : 1910 partial_flat_trace io_out io_in ge s s' ≝ 1911 match tr with 1912 [ tlr_base s1 s2 tll ⇒ flatten_trace_label_label ge ends_with_ret s1 s2 tll 1913  tlr_step s1 s2 s3 tll tlr ⇒ 1914 append_partial_flat_trace … 1915 (flatten_trace_label_label ge doesnt_end_with_ret s1 s2 tll) 1916 (flatten_trace_label_return ge s2 s3 tlr) 1917 ] 1918 and flatten_trace_label_label ge ends s s' 1919 (tr:trace_label_label (RTLabs_status ge) ends s s') 1920 on tr : 1921 partial_flat_trace io_out io_in ge s s' ≝ 1922 match tr with 1923 [ tll_base e s1 s2 tal _ ⇒ flatten_trace_any_label ge e s1 s2 tal 1924 ] 1925 and flatten_trace_any_label ge ends s s' 1926 (tr:trace_any_label (RTLabs_status ge) ends s s') 1927 on tr : 1928 partial_flat_trace io_out io_in ge s s' ≝ 1929 match tr with 1930 [ tal_base_not_return s1 s2 EX CL CS ⇒ 1931 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1932 pft_base … EX' ] 1933  tal_base_return s1 s2 EX CL ⇒ 1934 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1935 pft_base … EX' ] 1936  tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒ 1937 let suffix' ≝ flatten_trace_label_return ge ?? tlr in 1938 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1939 pft_step … EX' suffix' ] 1940  tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒ 1941 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1942 pft_step … EX' 1943 (append_partial_flat_trace … 1944 (flatten_trace_label_return ge ?? tlr) 1945 (flatten_trace_any_label ge ??? tal)) 1946 ] 1947  tal_step_default ends s1 s2 s3 EX tal CL CS ⇒ 1948 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1949 pft_step … EX' (flatten_trace_any_label ge ??? tal) 1950 ] 1951 ]. 1952 1953 1954 (* We take an extra step so that we can always return a nonempty trace to 1955 satisfy the guardedness condition in the cofixpoint. *) 1956 let rec flatten_trace_any_call ge s s' s'' et 1957 (tr:trace_any_call (RTLabs_status ge) s s') 1958 (EX'':eval_statement ge s' = Value … 〈et,s''〉) 1959 on tr : 1960 partial_flat_trace io_out io_in ge s s'' ≝ 1961 match tr return λs,s'.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with 1962 [ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX'' 1963  tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''. 1964 match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒ 1965 pft_step … EX' 1966 (append_partial_flat_trace … 1967 (flatten_trace_label_return ge ?? tlr) 1968 (flatten_trace_any_call ge … tac EX'')) 1969 ] 1970  tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''. 1971 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 1972 pft_step … EX' 1973 (flatten_trace_any_call ge … tal EX'') 1974 ] 1975 ] EX''. 1976 1977 let rec flatten_trace_label_call ge s s' s'' et 1978 (tr:trace_label_call (RTLabs_status ge) s s') 1979 (EX'':eval_statement ge s' = Value … 〈et,s''〉) 1980 on tr : 1981 partial_flat_trace io_out io_in ge s s'' ≝ 1982 match tr with 1983 [ tlc_base s1 s2 tac CS ⇒ flatten_trace_any_call … tac 1984 ] EX''. 1985 1986 (* Now reconstruct the flat_trace of a diverging execution. Note that we need 1987 to take care to satisfy the guardedness condition by witnessing the fact that 1988 the partial traces are nonempty. *) 1989 let corec flatten_trace_label_diverges ge s 1990 (tr:trace_label_diverges (RTLabs_status ge) s) 1991 : flat_trace io_out io_in ge s ≝ 1992 match tr with 1993 [ tld_step sx sy tll tld ⇒ 1994 match flatten_trace_label_label ge … tll with 1995 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld) 1996  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 1997 ] tld 1998  tld_base s1 s2 s3 tlc EX CL tld ⇒ 1999 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2000 match flatten_trace_label_call … tlc EX' with 2001 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld) 2002  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 2003 ] tld 2004 ] 2005 ] 2006 (* Helper to keep adding the partial trace without violating the guardedness 2007 condition. *) 2008 and add_partial_flat_trace ge s s' 2009 (ptr:partial_flat_trace io_out io_in ge s s') 2010 (tr:trace_label_diverges (RTLabs_status ge) s') 2011 : flat_trace io_out io_in ge s ≝ 2012 match ptr with 2013 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flatten_trace_label_diverges ge s' tr) 2014  pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr) 2015 ] tr 2016 . 2017 2018 coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝ 2019  eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F) 2020  eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2) 2021  eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX). 2022 2023 (* XXX move to semantics *) 2024 lemma final_cannot_move : ∀ge,s. 2025 RTLabs_is_final s ≠ None ? → 2026 ∃err. eval_statement ge s = Wrong ??? err. 2027 #ge * 2028 [ #f #fs #m * #F cases (F ?) @refl 2029  #a #b #c #d #e * #F cases (F ?) @refl 2030  #a #b #c #d * #F cases (F ?) @refl 2031  #r #F % [2: @refl  skip ] 2032 ] qed. 2033 2034 let corec flat_traces_are_determined_by_starting_point ge s tr1 2035 : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝ 2036 match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with 2037 [ ft_stop s F ⇒ λtr2. ? 2038  ft_step s1 tr s2 EX0 tr1' ⇒ λtr2. 2039 match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with 2040 [ ft_stop s F ⇒ λEX. ? 2041  ft_step s tr' s2' EX' tr2' ⇒ λEX. ? 2042  ft_wrong s m NF EX' ⇒ λEX. ? 2043 ] EX0 2044  ft_wrong s m NF EX ⇒ λtr2. ? 2045 ]. 2046 [ inversion tr2 in tr1 F; 2047 [ #s #F #_ #_ #tr1 #F' @eft_stop 2048  #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct 2049 cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct 2050  #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/ 2051 ] 2052  @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct 2053  EX0 2054 cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *) 2055 @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX') 2056 E EX' tr2' #tr2' #EX' 2057 cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *) 2058 @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX') 2059 E EX' #EX' 2060 @eft_step @flat_traces_are_determined_by_starting_point 2061  @⊥ >EX in EX'; #E destruct 2062  inversion tr2 in NF EX; 2063 [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/ 2064  #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct 2065  #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl. 2066 #E destruct 2067 @eft_wrong 2068 ] 2069 ] qed. 2070 2071 let corec diverging_traces_have_unique_flat_trace ge s 2072 (str:trace_label_diverges (RTLabs_status ge) s) 2073 (tr:flat_trace io_out io_in ge s) 2074 : equal_flat_traces … (flatten_trace_label_diverges … str) tr ≝ ?. 2075 @flat_traces_are_determined_by_starting_point 2076 qed. 2077 2078 let rec flatten_trace_whole_program ge s 2079 (tr:trace_whole_program (RTLabs_status ge) s) 2080 on tr : flat_trace io_out io_in ge s ≝ 2081 match tr with 2082 [ twp_terminating s1 s2 sf CL EX tlr F ⇒ 2083 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2084 ft_step … EX' (partial_to_flat_trace … (flatten_trace_label_return … tlr) (ft_stop … sf F)) 2085 ] 2086  twp_diverges s1 s2 CL EX tld ⇒ 2087 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2088 ft_step … EX' (flatten_trace_label_diverges … tld) 2089 ] 2090 ]. 2091 2092 let corec whole_traces_have_unique_flat_trace ge s 2093 (str:trace_whole_program (RTLabs_status ge) s) 2094 (tr:flat_trace io_out io_in ge s) 2095 : equal_flat_traces … (flatten_trace_whole_program … str) tr ≝ ?. 2096 @flat_traces_are_determined_by_starting_point 2097 qed.
Note: See TracChangeset
for help on using the changeset viewer.