Changeset 1880 for src/RTLabs


Ignore:
Timestamp:
Apr 6, 2012, 4:57:22 PM (8 years ago)
Author:
campbell
Message:

Show that RTLabs flat traces are determined by their starting state, and
that structured traces can be flattened, so must describe the same
execution as a flat trace from the same starting point.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1877 r1880  
    3131].
    3232
    33 definition RTLabs_status : genv → abstract_status ≝
     33definition RTLabs_status : genv → final_abstract_status ≝
    3434λge.
    35   mk_abstract_status
     35mk_final_abstract_status
     36  (mk_abstract_status
    3637    state
    3738    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
     
    5051        | _ ⇒ λH.⊥
    5152        ] 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:(??%?);
    5656  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    5757  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
    5860] qed.
    5961
     
    7981| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
    8082| 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.
    8284
    8385coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
     
    9496
    9597let corec make_flat_trace ge s
     98  (NF:RTLabs_is_final s = None ?)
    9699  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
    97100  flat_trace io_out io_in ge s ≝
     
    99102match e return λx. e = x → ? with
    100103[ 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 ??
    103106| e_interact o f ⇒ λE. ⊥
    104107] (refl ? e).
     
    145148| whd in E:(??%?); >exec_inf_aux_unfold in E;
    146149  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)
    147163  [ #O #K whd in ⊢ (??%? → ?); #E destruct
    148164  | * #tr1 #s1 whd in ⊢ (??%? → ?);
     
    169185match e return λx. e = x → ? with
    170186[ 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 ??
    172188| e_wrong m ⇒ λE. ⊥
    173189| e_interact o f ⇒ λE. ⊥
     
    175191[ whd in E:(??%?); >exec_inf_aux_unfold in E;
    176192  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 ⊢ (??%? → ?); #E destruct
    181   | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
    182   ]
     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)
    183199| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
    184200  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
     
    10141030    ] (refl ? (RTLabs_classify start))
    10151031   
    1016   | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
     1032  | ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
    10171033 
    10181034  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
     
    11761192[ St_skip l ⇒ [l]
    11771193| St_cost _ l ⇒ [l]
    1178 | St_const _ _ l ⇒ [l]
     1194| St_const _ _ _ l ⇒ [l]
    11791195| St_op1 _ _ _ _ _ l ⇒ [l]
    11801196| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
     
    12201236[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    12211237| #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} % // % //
    12231239| #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} % // % //
    12241240| #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} % // % //
     
    13121328[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
    13131329| #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 @refl
     1330| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    13151331| #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
    13161332| #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
     
    16081624        | cl_return ⇒ λCL. ⊥
    16091625        ] (refl ??)
    1610     | ft_wrong start m EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
     1626    | ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
    16111627    ] TRACE_OK
    16121628] LABEL_LIMIT.
     
    16771693      inversion (ro_not_undefined … TRACE_OK)
    16781694      [ #H137 #H138 #H139 #H140 #H141 destruct
    1679       | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct
     1695      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
    16801696        inversion H148
    16811697        [ #H153 #H154 #H155 #H156 #H157 destruct
     
    17461762] qed.
    17471763
    1748 let rec whole_structured_trace_exists ge s
     1764lemma 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
     1784lemma 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
     1793qed.
     1794
     1795let rec whole_structured_trace_exists ge p s
    17491796  (trace: flat_trace io_out io_in ge s)
    17501797  (ORACLE: termination_oracle)
    17511798  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    17521799  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1753   : ∀IS_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.
    17551802    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
    17561803    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
    17571804    trace_whole_program_exists (RTLabs_status ge) s ≝
    1758 match trace return λs,trace. RTLabs_classify s = cl_call
    1759                              not_wrong s trace →
     1805match trace return λs,trace. make_initial_state p = OK ? s
     1806                             not_wrong ??? s trace →
    17601807                             well_cost_labelled_state s →
    17611808                             soundly_labelled_state s →
    17621809                             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
    17641812    match ORACLE ge O next trace' with
    17651813    [ or_introl TERMINATES ⇒
     
    17671815        [ witness TERMINATES ⇒
    17681816          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) ?
    17701818        ]
    17711819    | or_intror NO_TERMINATION ⇒
     
    17741822            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
    17751823    ]
    1776 | ft_stop st FINAL ⇒ λIS_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. ⊥
    17781826].
    1779 [ cases (rtlabs_call_inv … IS_CALL) #fn * #args * #dst * #stk * #m #E destruct
     1827[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
    17801828  cases FINAL #E @E @refl
    17811829| %{tr} @EV
     1830| @(after_the_initial_call_is_the_final_state … INITIAL EV)
     1831  @(stack_ok … tlr)
    17821832| @(well_cost_labelled_state_step … EV) //
    17831833| @(well_cost_labelled_call … EV) //
     
    18191869[ whd
    18201870*)
     1871
     1872(* as_execute might be in Prop, but because the semantics is deterministic
     1873   we can retrieve the event trace anyway. *)
     1874let 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'〉 ≝
     1877match 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 non-empty finite section of a flat_trace *)
     1886inductive 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
     1890let rec append_partial_flat_trace o i ge s1 s2 s3
     1891  (tr1:partial_flat_trace o i ge s1 s2)
     1892on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
     1893match 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
     1898let rec partial_to_flat_trace o i ge s1 s2
     1899  (tr:partial_flat_trace o i ge s1 s2)
     1900on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
     1901match 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. *)
     1907let rec flatten_trace_label_return ge s s'
     1908  (tr:trace_label_return (RTLabs_status ge) s s')
     1909on tr :
     1910  partial_flat_trace io_out io_in ge s s' ≝
     1911match 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]
     1918and flatten_trace_label_label ge ends s s'
     1919  (tr:trace_label_label (RTLabs_status ge) ends s s')
     1920on tr :
     1921  partial_flat_trace io_out io_in ge s s' ≝
     1922match tr with
     1923[ tll_base e s1 s2 tal _ ⇒ flatten_trace_any_label ge e s1 s2 tal
     1924]
     1925and flatten_trace_any_label ge ends s s'
     1926  (tr:trace_any_label (RTLabs_status ge) ends s s')
     1927on tr :
     1928  partial_flat_trace io_out io_in ge s s' ≝
     1929match 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 non-empty trace to
     1955   satisfy the guardedness condition in the cofixpoint. *)
     1956let 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''〉)
     1959on tr :
     1960  partial_flat_trace io_out io_in ge s s'' ≝
     1961match 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
     1977let 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''〉)
     1980on tr :
     1981  partial_flat_trace io_out io_in ge s s'' ≝
     1982match 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 non-empty. *)
     1989let 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 ≝
     1992match 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. *)
     2008and 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 ≝
     2012match 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
     2018coinductive 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 *)
     2024lemma 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
     2034let corec flat_traces_are_determined_by_starting_point ge s tr1
     2035: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
     2036match 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
     2071let 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
     2076qed.
     2077
     2078let rec flatten_trace_whole_program ge s
     2079  (tr:trace_whole_program (RTLabs_status ge) s)
     2080on tr : flat_trace io_out io_in ge s ≝
     2081match 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
     2092let 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
     2097qed.
  • src/RTLabs/semantics.ma

    r1878 r1880  
    326326] qed.
    327327
     328
     329lemma initial_state_is_not_final : ∀p,s.
     330  make_initial_state p = OK ? s →
     331  RTLabs_is_final s = None ?.
     332#p #s whd in ⊢ (??%? → ?);
     333@bind_ok #m #Em
     334@bind_ok #b #Eb
     335@bind_ok #f #Ef
     336#E destruct
     337@refl
     338qed.
Note: See TracChangeset for help on using the changeset viewer.