Changeset 1595 for src/RTLabs

Timestamp:

Dec 7, 2011, 4:24:42 PM (9 years ago)

Author:

campbell

Message:

We don't need an explicit termination count when building traces.

File:

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

src/RTLabs/Traces.ma

@@ -204 +204 @@
 *)
 
-(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
-   [s] we reach the return state for the current function.  [depth] performs
-   the call/return counting necessary for handling deeper function calls.
-   It should be zero at the top level. *)
-inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
-| nir_step : ∀n,s,tr,s',depth,EX,trace.
+(* [will_return ge depth s trace] says that after a finite number of steps of
+   [trace] from [s] we reach the return state for the current function.  [depth]
+   performs the call/return counting necessary for handling deeper function
+   calls.  It should be zero at the top level. *)
+inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
+| wr_step : ∀s,tr,s',depth,EX,trace.
     RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
-    nth_is_return ge n depth s' trace →
-    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
-| nir_call : ∀n,s,tr,s',depth,EX,trace.
+    will_return ge depth s' trace →
+    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
+| wr_call : ∀s,tr,s',depth,EX,trace.
     RTLabs_classify s = cl_call →
-    nth_is_return ge n (S depth) s' trace →
-    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
-| nir_ret : ∀n,s,tr,s',depth,EX,trace.
+    will_return ge (S depth) s' trace →
+    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
+| wr_ret : ∀s,tr,s',depth,EX,trace.
     RTLabs_classify s = cl_return →
-    nth_is_return ge n depth s' trace →
-    nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
+    will_return ge depth s' trace →
+    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
     (* Note that we require the ability to make a step after the return (this
        corresponds to somewhere that will be guaranteed to be a label at the
        end of the compilation chain). *)
-| nir_base : ∀s,tr,s',EX,trace.
+| wr_base : ∀s,tr,s',EX,trace.
     RTLabs_classify s = cl_return →
-    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
+    will_return ge O s (ft_step ?? ge s tr s' EX trace)
 .
 
 discriminator nat.
+
+lemma will_return_call : ∀ge,depth,s,trace.
+  will_return ge depth s trace →
+  will_return ge (pred depth) s trace.
+#ge #depth #s #trace #H elim H
+[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
+| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
+  cases d in H1 H2 ⊢ %; //
+| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
+  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
+| #s1 #tr #s2 #EX #trc #CL %4 //
+] qed. 
+
+(*
+(* If we'll return then we must return from calls. *)
+lemma will_return_call : ∀ge,depth,s,trace.
+  will_return ge (S depth) s trace →
+  will_return ge depth s trace.
+#ge #depth #s #trace #H elim H in ⊢ ?;
+[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
+| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
+| #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/
+| #H215 #H216 #H217 #H218 #H219 #H220 #H221
+  inversion H221
+  [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct
+  | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct
+  | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct
+  | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct
+] qed. check will_return_call.
+| #H130 #H131 #H132 #H133 #H134 #H135
+  inversion H
+  [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct
+    cases H196 #E destruct
+  
+
+let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace)
+  on H : will_return ge depth s trace ≝
+match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with
+[ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ?
+| wr_call s tr s' d EX trace CL H' ⇒ λE. ?
+| wr_ret s tr s' d EX trace CL H' ⇒ λE. ?
+| wr_base s tr s' EX trace CL ⇒ λE. ?
+] (refl ? (S depth)).
+[ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H')
+  @(will_return_call … H'')
+| *: cases daemon ] qed.
+| %2 /2/
+| destruct cases d in H' ⊢ %;
+  [ #H' @wr_base //
+  | #d' #H' %3 /2/
+  ]
+| destruct
+] qed.
+
+(* If we'll return then we must return from calls. *)
+lemma will_return_call : ∀ge,depth,s,trace.
+  will_return ge (S depth) s trace →
+  will_return ge depth s trace.
+#ge #depth #s #trace #H lapply (refl ? (S depth))
+generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %);
+[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/
+| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3
+  
+discriminator nat.
+
+
 
 (* Find time until a nested call completes. *)
@@ -294 +360 @@
 | #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
 | #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
+] qed.
+*)
+
+lemma will_return_notfn : ∀ge,s,tr,s',EX,trace.
+  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
+  will_return ge O s (ft_step ?? ge s tr s' EX trace) →
+  will_return ge O s' trace.
+#ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM
+[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
+| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
+| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct
+| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
+| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
+| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
+| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct
+| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
 ] qed.
 
@@ -407 +489 @@
 ] qed.
 
+lemma rtlabs_call_inv : ∀s.
+  RTLabs_classify s = cl_call →
+  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
+* [ #f #fs #m whd in ⊢ (??%? → ?);
+    cases (lookup_present … (next f) (next_ok f)) normalize
+    try #A try #B try #C try #D try #E try #F try #G destruct
+  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
+  | normalize #H411 #H412 #H413 #H414 #H415 destruct
+  ] qed.
+
+lemma well_cost_labelled_call : ∀ge,s,tr,s'.
+  eval_statement ge s = Value ??? 〈tr,s'〉 →
+  well_cost_labelled_state s →
+  RTLabs_classify s = cl_call →
+  RTLabs_cost s' = true.
+#ge #s #tr #s' #EV #WCL #CL
+cases (rtlabs_call_inv s CL)
+#fd * #args * #dst * #stk * #m #E >E in EV WCL;
+whd in ⊢ (??%? → % → ?);
+cases fd
+[ #fn whd in ⊢ (??%? → % → ?);
+  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
+  #m' #b whd in ⊢ (??%? → ?); #E' destruct
+  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
+  @WCL2
+| #fn whd in ⊢ (??%? → % → ?);
+  @bindIO_value #evargs #Eargs
+  @bindIO_value #evres #Eres
+  normalize in Eres; destruct
+] qed.
 
 (* Don't need to know that labels break loops because we have termination. *)
@@ -412 +524 @@
 record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
   new_state : state;
-  termination_count : nat;
   remainder : flat_trace io_out io_in ge new_state;
   cost_labelled : well_cost_labelled_state new_state;
@@ -424 +535 @@
     (* We handle returns specially *)
     match ends with
-    [ doesnt_end_with_ret ⇒ nth_is_return ge (termination_count ?? trace_res) O (new_state ?? trace_res) (remainder ?? trace_res)
+    [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res)
     | ends_with_ret ⇒ True
     ]
@@ -436 +547 @@
     (mk_trace_result ge (T2 (ends … r))
       (new_state … r)
-      (termination_count … r)
       (remainder … r)
       (cost_labelled … r)
@@ -449 +559 @@
   mk_trace_result ge T2
     (new_state … r)
-    (termination_count … r)
     (remainder … r)
     (cost_labelled … r)
@@ -455 +564 @@
 .
 
-let rec make_label_return n ge s
+let rec make_label_return ge s
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
   (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
-  (TERMINATES: nth_is_return ge n O s trace)
+  (TERMINATES: will_return ge O s trace)
   : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝
 
-  let r ≝ make_label_label n ge s trace ???? in
+  let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
   match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with
   [ ends_with_ret ⇒ λtll,term.
       replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
   | doesnt_end_with_ret ⇒ λtll,term.
-      let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
-                 (remainder … r) ??? term in
+      let r' ≝ make_label_return ge (new_state … r)
+                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in
         replace_trace … r'
           (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
   ] (new_trace … r) (terminates … r)
 
-and make_label_label n ge s
+and make_label_label ge s
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
   (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
-  (TERMINATES: nth_is_return ge n O s trace)
+  (TERMINATES: will_return ge O s trace)
   : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
-let r ≝ make_any_label n ge s trace ??? in
+let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
   replace_sub_trace ??? r
     (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
 
-and make_any_label n ge s
+and make_any_label ge s
   (trace: flat_trace io_out io_in ge s)
   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
   (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
-  (TERMINATES: nth_is_return ge n O s trace)
+  (TERMINATES: will_return ge O s trace)
   : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
-match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
+match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
 | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
@@ -498 +607 @@
         match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
         [ true ⇒ λCS.
-            mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
+            mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
         | false ⇒ λCS.
-            let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
+            let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in
                 replace_sub_trace ??? r
                   (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
         ] (refl ??)
     | cl_jump ⇒ λCL.
-        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
-    | cl_call ⇒ λCL. ?
+        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
+    | cl_call ⇒ λCL.
+        let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in
+        let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
+        replace_sub_trace ??? r'
+          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
     | cl_return ⇒ λCL.
-        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
+        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
     ] (refl ? (RTLabs_classify start))
 | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
 ] STATE_COSTLABELLED TERMINATES.
 
-[ //
-| //
-| @(trace_label_label_label … tll)
-| //
-| //
-| //
-| //
-| //
-| //
-| //
+[ @(trace_label_label_label … tll)
 |
 | %{tr} @EV
@@ -531 +635 @@
 | @(well_cost_labelled_jump … EV) //
 | @(well_cost_labelled_state_step  … EV) //
-| @(nth_is_return_notfn … TERMINATES) %2 @CL
+| @(will_return_notfn … TERMINATES) %2 @CL
+| (* oh dear *)
+| %{tr} @EV
+| @(cost_labelled … r)
 |
-| %{tr} @EV
+|
+| 
+
+ @(well_cost_labelled_state_step  … EV) //
 | % whd in ⊢ (% → ?); >CL #E destruct
 | @CS
-| @(well_cost_labelled_state_step  … EV) //
 | @(nth_is_return_notfn … TERMINATES) %1 @CL
 | % whd in ⊢ (% → ?); >CS #E destruct