 Timestamp:
 Jul 20, 2012, 4:29:29 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2218 r2223 3 3 include "RTLabs/CostSpec.ma". 4 4 include "common/StructuredTraces.ma". 5 include "common/Executions.ma". 5 6 6 7 discriminator status_class. … … 253 254 (* Before attempting to construct a structured trace, let's show that we can 254 255 form flat traces with evidence that they were constructed from an execution. 256 As with the structured traces, we only consider good traces (i.e., ones 257 which don't go wrong). 255 258 256 259 For now we don't consider I/O. *) … … 265 268 coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ 266 269  ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s 267  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s 268  ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s. 269 270 coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝ 271  nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H) 272  nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr'). 273 274 lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'. 275 not_wrong o i ge s (ft_step o i ge s tr s' H tr') → 276 not_wrong o i ge s' tr'. 277 #o #i #ge #s #tr #s' #H #tr' #NW inversion NW 278 [ #H105 #H106 #H107 #H108 #H109 destruct 279  #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct // 280 ] qed. 270  ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s. 281 271 282 272 let corec make_flat_trace ge s 283 273 (NF:RTLabs_is_final s = None ?) 284 (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 274 (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) 275 (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : 285 276 flat_trace io_out io_in ge s ≝ 286 277 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in 287 278 match e return λx. e = x → ? with 288 279 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) 289  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?? )290  e_wrong m ⇒ λE. ft_wrong … s m ??280  e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???) 281  e_wrong m ⇒ λE. ⊥ 291 282  e_interact o f ⇒ λE. ⊥ 292 283 ] (refl ? e). 293 [ 1, 2: whd in E:(??%?); >exec_inf_aux_unfold in E;284 [ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E; 294 285 cases (eval_statement ge s) 295 286 [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct … … 298 289 lapply (refl ? (RTLabs_is_final s1)) 299 290 cases (RTLabs_is_final s1) in ⊢ (???% → %); 300 [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct 301  #i #_ whd in ⊢ (??%? → ?); #E destruct /2/@refl302  #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct291 [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct % 292  #i #_ whd in ⊢ (??%? → ?); #E destruct @refl 293  #i #E whd in ⊢ (??%? → ?); #E2 destruct 303 294 ] 304 295  *: #m whd in ⊢ (??%? → ?); #E destruct … … 306 297  whd in E:(??%?); >exec_inf_aux_unfold in E; 307 298 cases (eval_statement ge s) 308 [ # O#K whd in ⊢ (??%? → ?); #E destruct299 [ #o #K whd in ⊢ (??%? → ?); #E destruct 309 300  * #tr #s1 whd in ⊢ (??%? → ?); 310 cases (is_final ?????) 311 [ whd in ⊢ (??%? → ?); #E destruct @refl 312  #i whd in ⊢ (??%? → ?); #E destruct 313 ] 314  #m whd in ⊢ (??%? → ?); #E destruct 301 lapply (refl ? (RTLabs_is_final s1)) 302 change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?_⇒?])? → ?); 303 cases (RTLabs_is_final s1) in ⊢ (???% → %); 304 [ #F #E whd in E:(??%?); destruct 305  #r #F #E whd in E:(??%?); destruct >F % #E destruct 306 ] 307  #m #E whd in E:(??%?); destruct 315 308 ] 316 309  whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; … … 331 324  #m whd in ⊢ (??%? → ?); #E destruct 332 325 ] 326  whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E; 327 cases (eval_statement ge s) 328 [ #O #K whd in ⊢ (??%? → ?); #E destruct 329  * #tr #s1 whd in ⊢ (??%? → ?); 330 cases (is_final ?????) 331 [ whd in ⊢ (??%? → ?); #E 332 change with (eval_statement ge s1) in E:(??(??????(?????%))?); 333 destruct 334 inversion NW 335 [ #a #b #c #E1 #_ destruct 336  #trx #sx #ex #H1 #E2 #E3 destruct @H1 337  #o #k #K #E1 destruct 338 ] 339  #i whd in ⊢ (??%? → ?); #E destruct 340 ] 341  #m whd in ⊢ (??%? → ?); #E destruct 342 ] 333 343  whd in E:(??%?); >exec_inf_aux_unfold in E; 334 344 cases (eval_statement ge s) … … 343 353  #m #E whd in E:(??%?); destruct 344 354 ] 345  @NF 346  whd in E:(??%?); >exec_inf_aux_unfold in E; 347 cases (eval_statement ge s) 348 [ #O #K whd in ⊢ (??%? → ?); #E destruct 349  * #tr1 #s1 whd in ⊢ (??%? → ?); 350 cases (is_final ?????) 351 [ whd in ⊢ (??%? → ?); #E destruct 352  #i whd in ⊢ (??%? → ?); #E destruct 353 ] 354  #m whd in ⊢ (??%? → ?); #E destruct @refl 355 ] 356  whd in E:(??%?); >E in H; #H 357 inversion H 358 [ #a #b #c #E destruct 359  #a #b #c #d #E1 destruct 360  #m #E1 destruct 361 ] 362 ] qed. 363 364 let corec make_whole_flat_trace p s 365 (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) 366 (I:make_initial_state ??? p = OK ? s) : 355  whd in E:(??%?); >E in NW; #X inversion X 356 #A #B #C #D #E destruct 357  whd in E:(??%?); >E in H; #H inversion H 358 #A #B #C try #D try #E destruct 359 ] qed. 360 361 definition make_whole_flat_trace : ∀p,s. 362 exec_no_io … (exec_inf … RTLabs_fullexec p) → 363 not_wrong … (exec_inf … RTLabs_fullexec p) → 364 make_initial_state ??? p = OK ? s → 367 365 flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ 366 λp,s,H,NW,I. 368 367 let ge ≝ make_global … p in 369 368 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in 370 369 match e return λx. e = x → ? with 371 370 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? 372  e_step _ _ e' ⇒ λE. make_flat_trace ge s ?? 371  e_step _ _ e' ⇒ λE. make_flat_trace ge s ??? 373 372  e_wrong m ⇒ λE. ⊥ 374 373  e_interact o f ⇒ λE. ⊥ … … 382 381 ] 383 382  @(initial_state_is_not_final … I) 383  whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?); 384 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????) 385 [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H 386 [ #a #b #c #E1 destruct 387  #tr1 #s1 #e1 #H1 #E1 #E2 E2 I destruct (E1) 388 @H1 389  #o #k #K #E1 destruct 390 ] 391  #i whd in ⊢ (??%? → ??% → ?); #E destruct 392 ] 384 393  whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); 385 394 >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) … … 602 611 ] qed. 603 612 604 lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.605 ∀T:will_return ge d s t.606 not_wrong io_out io_in ge s t →607 will_return_end … T = ❬s', t'❭ →608 not_wrong io_out io_in ge s' t'.609 #ge #d #s #t #s' #t' #T elim T610 [ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH611 [ inversion NW612 [ #H1 #H2 #H3 #H4 #H5 destruct613  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //614 ]615  @E616 ]617  #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH618 [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]619  @E620 ]621  #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH622 [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]623  @E624 ]625  #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct626 inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]627 ] qed.628 613 629 614 … … 1203 1188 ] (refl ? (RTLabs_classify start)) 1204 1189 1205  ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥1206 1207 1190 ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME 1208 1191 ] TERMINATES_IN_TIME. … … 1298 1281 @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME) 1299 1282 // 1300  inversion TERMINATES1301 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES TERMINATES destruct1302  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 TERMINATES TERMINATES destruct1303  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 TERMINATES TERMINATES destruct1304  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 TERMINATES TERMINATES destruct1305 ]1306 1283 ] qed. 1307 1284 … … 1622 1599 ro_soundly_labelled: soundly_labelled_state s; 1623 1600 ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t)); 1624 ro_not_undefined: not_wrong … t;1625 1601 ro_not_final: RTLabs_is_final s = None ? 1626 1602 }. … … 1734 1710  cl_return ⇒ λCL. ⊥ 1735 1711 ] (refl ??) 1736  ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥1737 1712 ] mtc0 1738 1713 ] trace TRACE_OK … … 1744 1719  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK)  // ] 1745 1720  5,6,9,10,11: /3/ 1746  cases TRACE_OK #H1 #H2 #H3 #H4 #H51721  cases TRACE_OK #H1 #H2 #H3 #H4 1747 1722 % [ @(well_cost_labelled_state_step … EV) // 1748 1723  @(soundly_labelled_state_step … EV) // 1749 1724  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/ 1750  @(still_not_wrong … EV) //1751 1725  @(not_return_to_not_final … EV) >CL % #E destruct 1752 1726 ] … … 1762 1736 @(will_return_prepend … TERMINATES … TM1) 1763 1737 cases (terminates … tlr) // 1764  @(will_return_not_wrong … TERMINATES)1765 [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK)1766  cases (terminates … tlr) //1767 ]1768 1738  (* By stack preservation we cannot be in the final state *) 1769 1739 inversion (stack_ok … tlr) … … 1788 1758  /2/ 1789 1759  %{tr} %{EV} % 1790  cases TRACE_OK #H1 #H2 #H3 #H4 #H51760  cases TRACE_OK #H1 #H2 #H3 #H4 1791 1761 % [ @(well_cost_labelled_state_step … EV) /2/ 1792 1762  @(soundly_labelled_state_step … EV) /2/ 1793 1763  @(not_to_not … NO_TERMINATION) * #depth * #TM % 1794 1764 @(will_return_lower … TM) // 1795  @(still_not_wrong … EV) /2/1796 1765  @(not_return_to_not_final … EV) >CL % #E destruct 1797 1766 ] … … 1806 1775  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 TRACE_OK' destruct 1807 1776 @wr_base // 1808  #H99 #H100 #H101 #H102 #H103 TRACE_OK' destruct1809 inversion (ro_not_undefined … TRACE_OK)1810 [ #H137 #H138 #H139 #H140 #H141 destruct1811  #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct1812 inversion H1481813 [ #H153 #H154 #H155 #H156 #H157 destruct1814  #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct1815 ]1816 ]1817 1777 ] 1818 1778 ] … … 1822 1782  // 1823 1783 ] 1824  cases TRACE_OK #H1 #H2 #H3 #H4 #H51784  cases TRACE_OK #H1 #H2 #H3 #H4 1825 1785 % [ @(well_cost_labelled_state_step … EV) // 1826 1786  @(soundly_labelled_state_step … EV) // 1827 1787  @(not_to_not … (ro_no_termination … TRACE_OK)) 1828 1788 * #depth * #TERM %{depth} % @wr_step /2/ 1829  @(still_not_wrong … (ro_not_undefined … TRACE_OK))1830 1789  @(not_return_to_not_final … EV) >CL % #E destruct 1831 1790 ] 1832  inversion (ro_not_undefined … TRACE_OK)1833 [ #H169 #H170 #H171 #H172 #H173 destruct1834  #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct1835 ]1836 1791 ] qed. 1837 1792 … … 1916 1871 : ∀trace: flat_trace io_out io_in ge s. 1917 1872 ∀INITIAL: make_initial_state p = OK state s. 1918 ∀NOT_WRONG: not_wrong ??? s trace.1919 1873 ∀STATE_COSTLABELLED: well_cost_labelled_state s. 1920 1874 ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s. … … 1922 1876 match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. 1923 1877 make_initial_state p = OK ? s → 1924 not_wrong ??? s trace →1925 1878 well_cost_labelled_state s → 1926 1879 soundly_labelled_state s → … … 1929 1882 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. 1930 1883 make_initial_state p = OK state s → 1931 not_wrong ??? s trace →1932 1884 well_cost_labelled_state s → 1933 1885 soundly_labelled_state s → 1934 1886 trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with 1935 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL, NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.1887 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. 1936 1888 let IS_CALL ≝ initial_state_is_call … INITIAL in 1937 1889 let s' ≝ mk_RTLabs_state ge s stk mtc in … … 1949 1901 ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?) 1950 1902 ] 1951  ft_stop st FINAL ⇒ λmtc,INITIAL,NOT_WRONG. ⊥ 1952  ft_wrong start m NF EV ⇒ λmtc,INITIAL,NOT_WRONG. ⊥ 1903  ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥ 1953 1904 ] mtc0 ]. 1954 1905 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct … … 1964 1915  @(soundly_labelled_state_step … EV) // 1965 1916  @(not_to_not … NO_TERMINATION) * #d * #TM % /2/ 1966  @(still_not_wrong … NOT_WRONG)1967 1917  @(not_return_to_not_final … EV) >IS_CALL % #E destruct 1968 1918 ] 1969  inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct1970 1919 ] qed. 1971 1920 … … 2162 2111 coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝ 2163 2112  eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F) 2164  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) 2165  eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX). 2113  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). 2166 2114 2167 2115 (* XXX move to semantics *) … … 2184 2132 [ ft_stop s F ⇒ λEX. ? 2185 2133  ft_step s tr' s2' EX' tr2' ⇒ λEX. ? 2186  ft_wrong s m NF EX' ⇒ λEX. ?2187 2134 ] EX0 2188  ft_wrong s m NF EX ⇒ λtr2. ?2189 2135 ]. 2190 2136 [ inversion tr2 in tr1 F; … … 2192 2138  #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct 2193 2139 cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct 2194  #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/2195 2140 ] 2196 2141  @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct … … 2203 2148 E EX' #EX' 2204 2149 @eft_step @flat_traces_are_determined_by_starting_point 2205  @⊥ >EX in EX'; #E destruct2206  inversion tr2 in NF EX;2207 [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/2208  #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct2209  #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.2210 #E destruct2211 @eft_wrong2212 ]2213 2150 ] qed. 2214 2151
Note: See TracChangeset
for help on using the changeset viewer.