Changeset 2223 for src

Timestamp:

Jul 20, 2012, 4:29:29 PM (9 years ago)

Author:

campbell

Message:

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

File:

• src/RTLabs/Traces.ma (modified) (27 diffs)

src/RTLabs/Traces.ma

@@ -3 +3 @@
 include "RTLabs/CostSpec.ma".
 include "common/StructuredTraces.ma".
+include "common/Executions.ma".
 
 discriminator status_class.
@@ -253 +254 @@
 (* Before attempting to construct a structured trace, let's show that we can
    form flat traces with evidence that they were constructed from an execution.
+   As with the structured traces, we only consider good traces (i.e., ones
+   which don't go wrong).
    
    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] ≝
 | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
-| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
-| ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
-
-coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
-| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
-| 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').
-
-lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
-  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
-  not_wrong o i ge s' tr'.
-#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
-[ #H105 #H106 #H107 #H108 #H109 destruct
-| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
-] qed.
+| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s.
 
 let corec make_flat_trace ge s
   (NF:RTLabs_is_final s = None ?)
-  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
+  (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s)))
+  (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
   flat_trace io_out io_in ge s ≝
 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
 match e return λx. e = x → ? with
 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
-| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??)
-| e_wrong m ⇒ λE. ft_wrong … s m ??
+| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???)
+| e_wrong m ⇒ λE. ⊥
 | e_interact o f ⇒ λE. ⊥
 ] (refl ? e).
-[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
+[ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E;
   cases (eval_statement ge s)
   [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
@@ -298 +289 @@
     lapply (refl ? (RTLabs_is_final s1))
     cases (RTLabs_is_final s1) in ⊢ (???% → %);
-    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
-    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
-    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
+    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
+    | #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
+    | #i #E whd in ⊢ (??%? → ?); #E2 destruct
     ]
   | *: #m whd in ⊢ (??%? → ?); #E destruct
@@ -306 +297 @@
 | whd in E:(??%?); >exec_inf_aux_unfold in E;
   cases (eval_statement ge s)
-  [ #O #K whd in ⊢ (??%? → ?); #E destruct
+  [ #o #K whd in ⊢ (??%? → ?); #E destruct
   | * #tr #s1 whd in ⊢ (??%? → ?);
-    cases (is_final ?????)
-    [ whd in ⊢ (??%? → ?); #E destruct @refl
-    | #i whd in ⊢ (??%? → ?); #E destruct
-    ]
-  | #m whd in ⊢ (??%? → ?); #E destruct
+    lapply (refl ? (RTLabs_is_final s1))
+    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
+    cases (RTLabs_is_final s1) in ⊢ (???% → %);
+    [ #F #E whd in E:(??%?); destruct
+    | #r #F #E whd in E:(??%?); destruct >F % #E destruct
+    ]
+  | #m #E whd in E:(??%?); destruct
   ]
 | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
@@ -331 +324 @@
   | #m whd in ⊢ (??%? → ?); #E destruct
   ]
+| whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E;
+  cases (eval_statement ge s)
+  [ #O #K whd in ⊢ (??%? → ?); #E destruct
+  | * #tr #s1 whd in ⊢ (??%? → ?);
+    cases (is_final ?????)
+    [ whd in ⊢ (??%? → ?); #E
+      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
+      destruct
+      inversion NW
+      [ #a #b #c #E1 #_ destruct
+      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
+      | #o #k #K #E1 destruct
+      ]
+    | #i whd in ⊢ (??%? → ?); #E destruct
+    ]
+  | #m whd in ⊢ (??%? → ?); #E destruct
+  ]
 | whd in E:(??%?); >exec_inf_aux_unfold in E;
   cases (eval_statement ge s)
@@ -343 +353 @@
   | #m #E whd in E:(??%?); destruct
   ]
-| @NF
-| whd in E:(??%?); >exec_inf_aux_unfold in E;
-  cases (eval_statement ge s)
-  [ #O #K whd in ⊢ (??%? → ?); #E destruct
-  | * #tr1 #s1 whd in ⊢ (??%? → ?);
-    cases (is_final ?????)
-    [ whd in ⊢ (??%? → ?); #E destruct
-    | #i whd in ⊢ (??%? → ?); #E destruct
-    ]
-  | #m whd in ⊢ (??%? → ?); #E destruct @refl
-  ]
-| whd in E:(??%?); >E in H; #H
-  inversion H
-  [ #a #b #c #E destruct
-  | #a #b #c #d #E1 destruct
-  | #m #E1 destruct
-  ]
-] qed.
-
-let corec make_whole_flat_trace p s
-  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
-  (I:make_initial_state ??? p = OK ? s) :
+| whd in E:(??%?); >E in NW; #X inversion X
+  #A #B #C #D #E destruct
+| whd in E:(??%?); >E in H; #H inversion H
+  #A #B #C try #D try #E destruct
+] qed.
+
+definition make_whole_flat_trace : ∀p,s.
+  exec_no_io … (exec_inf … RTLabs_fullexec p) →
+  not_wrong … (exec_inf … RTLabs_fullexec p) →
+  make_initial_state ??? p = OK ? s →
   flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
+λp,s,H,NW,I.
 let ge ≝ make_global … p in
 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
 match e return λx. e = x → ? with
 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
-| e_step _ _ e' ⇒ λE. make_flat_trace ge s ??
+| e_step _ _ e' ⇒ λE. make_flat_trace ge s ???
 | e_wrong m ⇒ λE. ⊥
 | e_interact o f ⇒ λE. ⊥
@@ -382 +381 @@
   ]
 | @(initial_state_is_not_final … I)
+| whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?);
+  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????)
+  [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H
+    [ #a #b #c #E1 destruct
+    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
+      @H1
+    | #o #k #K #E1 destruct
+    ]
+  | #i whd in ⊢ (??%? → ??% → ?); #E destruct
+  ]
 | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
   >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
@@ -602 +611 @@
 ] qed.
 
-lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
-  ∀T:will_return ge d s t.
-  not_wrong io_out io_in ge s t →
-  will_return_end … T = ❬s', t'❭ →
-  not_wrong io_out io_in ge s' t'.
-#ge #d #s #t #s' #t' #T elim T
-[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
-  [ inversion NW
-    [ #H1 #H2 #H3 #H4 #H5 destruct
-    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
-    ]
-  | @E
-  ]
-| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
-  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
-  | @E
-  ]
-| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
-  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
-  | @E
-  ]
-| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
-  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
-] qed.
 
 
@@ -1203 +1188 @@
     ] (refl ? (RTLabs_classify start))
     
-  | ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥
-  
   ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
 ] TERMINATES_IN_TIME.
@@ -1298 +1281 @@
   @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
   //
-| inversion TERMINATES
-  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
-  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
-  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
-  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
-  ]
 ] qed.
 
@@ -1622 +1599 @@
   ro_soundly_labelled: soundly_labelled_state s;
   ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
-  ro_not_undefined: not_wrong … t;
   ro_not_final: RTLabs_is_final s = None ?
 }.
@@ -1734 +1710 @@
         | cl_return ⇒ λCL. ⊥
         ] (refl ??)
-    | ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
     ] mtc0
   ] trace TRACE_OK
@@ -1744 +1719 @@
 | @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
 | 5,6,9,10,11: /3/
-| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
+| cases TRACE_OK #H1 #H2 #H3 #H4
   % [ @(well_cost_labelled_state_step … EV) //
     | @(soundly_labelled_state_step … EV) //
     | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
-    | @(still_not_wrong … EV) //
     | @(not_return_to_not_final … EV) >CL % #E destruct
     ]
@@ -1762 +1736 @@
       @(will_return_prepend … TERMINATES … TM1)
       cases (terminates … tlr) //
-    | @(will_return_not_wrong … TERMINATES)
-      [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK)
-      | cases (terminates … tlr) //
-      ]
     | (* By stack preservation we cannot be in the final state *)
       inversion (stack_ok … tlr)
@@ -1788 +1758 @@
 | /2/
 | %{tr} %{EV} %
-| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
+| cases TRACE_OK #H1 #H2 #H3 #H4
   % [ @(well_cost_labelled_state_step … EV) /2/
     | @(soundly_labelled_state_step … EV) /2/
     | @(not_to_not … NO_TERMINATION) * #depth * #TM %
       @(will_return_lower … TM) //
-    | @(still_not_wrong … EV) /2/
     | @(not_return_to_not_final … EV) >CL % #E destruct
     ]
@@ -1806 +1775 @@
     | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
       @wr_base //
-    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
-      inversion (ro_not_undefined … TRACE_OK)
-      [ #H137 #H138 #H139 #H140 #H141 destruct
-      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
-        inversion H148
-        [ #H153 #H154 #H155 #H156 #H157 destruct
-        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
-        ]
-      ]
     ]
     ]
@@ -1822 +1782 @@
   | //
   ]
-| cases TRACE_OK #H1 #H2 #H3 #H4 #H5
+| cases TRACE_OK #H1 #H2 #H3 #H4
   % [ @(well_cost_labelled_state_step … EV) //
     | @(soundly_labelled_state_step … EV) //
     | @(not_to_not … (ro_no_termination … TRACE_OK))
       * #depth * #TERM %{depth} % @wr_step /2/
-    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
     | @(not_return_to_not_final … EV) >CL % #E destruct
     ]
-| inversion (ro_not_undefined … TRACE_OK)
-  [ #H169 #H170 #H171 #H172 #H173 destruct
-  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
-  ]
 ] qed.
 
@@ -1916 +1871 @@
   : ∀trace: flat_trace io_out io_in ge s.
     ∀INITIAL: make_initial_state p = OK state s.
-    ∀NOT_WRONG: not_wrong ??? s trace.
     ∀STATE_COSTLABELLED: well_cost_labelled_state s.
     ∀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.
                    make_initial_state p = OK ? s →
-                   not_wrong ??? s trace →
                    well_cost_labelled_state s →
                    soundly_labelled_state s →
@@ -1929 +1882 @@
 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
                              make_initial_state p = OK state s →
-                             not_wrong ??? s trace →
                              well_cost_labelled_state s →
                              soundly_labelled_state s →
                              trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
-[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
+[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
     let IS_CALL ≝ initial_state_is_call … INITIAL in
     let s' ≝ mk_RTLabs_state ge s stk mtc in
@@ -1949 +1901 @@
             ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
     ]
-| ft_stop st FINAL ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
-| ft_wrong start m NF EV ⇒ λmtc,INITIAL,NOT_WRONG. ⊥
+| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
 ] mtc0 ].
 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
@@ -1964 +1915 @@
     | @(soundly_labelled_state_step … EV) //
     | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
-    | @(still_not_wrong … NOT_WRONG)
     | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
     ]
-| inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
 ] qed.
 
@@ -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 ≝
 | eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
-| 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)
-| eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX).
+| 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).
 
 (* XXX move to semantics *)
@@ -2184 +2132 @@
     [ ft_stop s F ⇒ λEX. ?
     | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
-    | ft_wrong s m NF EX' ⇒ λEX. ?
     ] EX0
-| ft_wrong s m NF EX ⇒ λtr2. ?
 ].
 [ inversion tr2 in tr1 F;
@@ -2192 +2138 @@
   | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
     cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
-  | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/
   ]
 | @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
@@ -2203 +2148 @@
   -E -EX' #EX'
     @eft_step @flat_traces_are_determined_by_starting_point
-| @⊥ >EX in EX'; #E destruct
-| inversion tr2 in NF EX;
-  [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/
-  | #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct
-  | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.
-    #E destruct
-    @eft_wrong
-  ]
 ] qed.