Changeset 2223 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Jul 20, 2012, 4:29:29 PM (7 years ago)
Author:
campbell
Message:

Simplify RTLabs structure traces proofs by getting rid of wrong
executions earlier.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2218 r2223  
    33include "RTLabs/CostSpec.ma".
    44include "common/StructuredTraces.ma".
     5include "common/Executions.ma".
    56
    67discriminator status_class.
     
    253254(* Before attempting to construct a structured trace, let's show that we can
    254255   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).
    255258   
    256259   For now we don't consider I/O. *)
     
    265268coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
    266269| 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.
    281271
    282272let corec make_flat_trace ge s
    283273  (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))) :
    285276  flat_trace io_out io_in ge s ≝
    286277let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
    287278match e return λx. e = x → ? with
    288279[ 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.
    291282| e_interact o f ⇒ λE. ⊥
    292283] (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;
    294285  cases (eval_statement ge s)
    295286  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
     
    298289    lapply (refl ? (RTLabs_is_final s1))
    299290    cases (RTLabs_is_final s1) in ⊢ (???% → %);
    300     [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
    301     | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
    302     | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
     291    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
     292    | #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
     293    | #i #E whd in ⊢ (??%? → ?); #E2 destruct
    303294    ]
    304295  | *: #m whd in ⊢ (??%? → ?); #E destruct
     
    306297| whd in E:(??%?); >exec_inf_aux_unfold in E;
    307298  cases (eval_statement ge s)
    308   [ #O #K whd in ⊢ (??%? → ?); #E destruct
     299  [ #o #K whd in ⊢ (??%? → ?); #E destruct
    309300  | * #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
    315308  ]
    316309| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
     
    331324  | #m whd in ⊢ (??%? → ?); #E destruct
    332325  ]
     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  ]
    333343| whd in E:(??%?); >exec_inf_aux_unfold in E;
    334344  cases (eval_statement ge s)
     
    343353  | #m #E whd in E:(??%?); destruct
    344354  ]
    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
     361definition 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 →
    367365  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
     366λp,s,H,NW,I.
    368367let ge ≝ make_global … p in
    369368let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
    370369match e return λx. e = x → ? with
    371370[ 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 ???
    373372| e_wrong m ⇒ λE. ⊥
    374373| e_interact o f ⇒ λE. ⊥
     
    382381  ]
    383382| @(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  ]
    384393| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
    385394  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
     
    602611] qed.
    603612
    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 T
    610 [ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
    611   [ inversion NW
    612     [ #H1 #H2 #H3 #H4 #H5 destruct
    613     | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
    614     ]
    615   | @E
    616   ]
    617 | #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
    618   [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
    619   | @E
    620   ]
    621 | #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
    622   [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
    623   | @E
    624   ]
    625 | #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
    626   inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
    627 ] qed.
    628613
    629614
     
    12031188    ] (refl ? (RTLabs_classify start))
    12041189   
    1205   | ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥
    1206  
    12071190  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
    12081191] TERMINATES_IN_TIME.
     
    12981281  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
    12991282  //
    1300 | inversion TERMINATES
    1301   [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
    1302   | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
    1303   | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
    1304   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
    1305   ]
    13061283] qed.
    13071284
     
    16221599  ro_soundly_labelled: soundly_labelled_state s;
    16231600  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
    1624   ro_not_undefined: not_wrong … t;
    16251601  ro_not_final: RTLabs_is_final s = None ?
    16261602}.
     
    17341710        | cl_return ⇒ λCL. ⊥
    17351711        ] (refl ??)
    1736     | ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
    17371712    ] mtc0
    17381713  ] trace TRACE_OK
     
    17441719| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    17451720| 5,6,9,10,11: /3/
    1746 | cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1721| cases TRACE_OK #H1 #H2 #H3 #H4
    17471722  % [ @(well_cost_labelled_state_step … EV) //
    17481723    | @(soundly_labelled_state_step … EV) //
    17491724    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
    1750     | @(still_not_wrong … EV) //
    17511725    | @(not_return_to_not_final … EV) >CL % #E destruct
    17521726    ]
     
    17621736      @(will_return_prepend … TERMINATES … TM1)
    17631737      cases (terminates … tlr) //
    1764     | @(will_return_not_wrong … TERMINATES)
    1765       [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK)
    1766       | cases (terminates … tlr) //
    1767       ]
    17681738    | (* By stack preservation we cannot be in the final state *)
    17691739      inversion (stack_ok … tlr)
     
    17881758| /2/
    17891759| %{tr} %{EV} %
    1790 | cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1760| cases TRACE_OK #H1 #H2 #H3 #H4
    17911761  % [ @(well_cost_labelled_state_step … EV) /2/
    17921762    | @(soundly_labelled_state_step … EV) /2/
    17931763    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
    17941764      @(will_return_lower … TM) //
    1795     | @(still_not_wrong … EV) /2/
    17961765    | @(not_return_to_not_final … EV) >CL % #E destruct
    17971766    ]
     
    18061775    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
    18071776      @wr_base //
    1808     | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
    1809       inversion (ro_not_undefined … TRACE_OK)
    1810       [ #H137 #H138 #H139 #H140 #H141 destruct
    1811       | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
    1812         inversion H148
    1813         [ #H153 #H154 #H155 #H156 #H157 destruct
    1814         | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
    1815         ]
    1816       ]
    18171777    ]
    18181778    ]
     
    18221782  | //
    18231783  ]
    1824 | cases TRACE_OK #H1 #H2 #H3 #H4 #H5
     1784| cases TRACE_OK #H1 #H2 #H3 #H4
    18251785  % [ @(well_cost_labelled_state_step … EV) //
    18261786    | @(soundly_labelled_state_step … EV) //
    18271787    | @(not_to_not … (ro_no_termination … TRACE_OK))
    18281788      * #depth * #TERM %{depth} % @wr_step /2/
    1829     | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
    18301789    | @(not_return_to_not_final … EV) >CL % #E destruct
    18311790    ]
    1832 | inversion (ro_not_undefined … TRACE_OK)
    1833   [ #H169 #H170 #H171 #H172 #H173 destruct
    1834   | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
    1835   ]
    18361791] qed.
    18371792
     
    19161871  : ∀trace: flat_trace io_out io_in ge s.
    19171872    ∀INITIAL: make_initial_state p = OK state s.
    1918     ∀NOT_WRONG: not_wrong ??? s trace.
    19191873    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
    19201874    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
     
    19221876match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
    19231877                   make_initial_state p = OK ? s →
    1924                    not_wrong ??? s trace →
    19251878                   well_cost_labelled_state s →
    19261879                   soundly_labelled_state s →
     
    19291882match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
    19301883                             make_initial_state p = OK state s →
    1931                              not_wrong ??? s trace →
    19321884                             well_cost_labelled_state s →
    19331885                             soundly_labelled_state s →
    19341886                             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.
    19361888    let IS_CALL ≝ initial_state_is_call … INITIAL in
    19371889    let s' ≝ mk_RTLabs_state ge s stk mtc in
     
    19491901            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
    19501902    ]
    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. ⊥
    19531904] mtc0 ].
    19541905[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
     
    19641915    | @(soundly_labelled_state_step … EV) //
    19651916    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
    1966     | @(still_not_wrong … NOT_WRONG)
    19671917    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
    19681918    ]
    1969 | inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
    19701919] qed.
    19711920
     
    21622111coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
    21632112| 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).
    21662114
    21672115(* XXX move to semantics *)
     
    21842132    [ ft_stop s F ⇒ λEX. ?
    21852133    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
    2186     | ft_wrong s m NF EX' ⇒ λEX. ?
    21872134    ] EX0
    2188 | ft_wrong s m NF EX ⇒ λtr2. ?
    21892135].
    21902136[ inversion tr2 in tr1 F;
     
    21922138  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
    21932139    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
    2194   | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/
    21952140  ]
    21962141| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
     
    22032148  -E -EX' #EX'
    22042149    @eft_step @flat_traces_are_determined_by_starting_point
    2205 | @⊥ >EX in EX'; #E destruct
    2206 | 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 destruct
    2209   | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.
    2210     #E destruct
    2211     @eft_wrong
    2212   ]
    22132150] qed.
    22142151
Note: See TracChangeset for help on using the changeset viewer.