Changeset 1736

Timestamp:

Feb 24, 2012, 1:19:10 PM (9 years ago)

Author:

campbell

Message:

Show that the bound on the number of instructions until a cost label is
preserved by function calls in RTLabs structured traces.

File:

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

src/RTLabs/Traces.ma

@@ -43 +43 @@
         [ Callstate fd args dst stk m ⇒
           λ_. match s' with
-          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
-          | Finalstate r ⇒ True
+          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
+          | Finalstate r ⇒ stk = [ ]
           | _ ⇒ False
           ]
@@ -569 +569 @@
 | sp_finished : ∀s1,f,f',fs,m.
     next f = next f' →
+    frame_rel f f' →
     stack_of_state (f::fs) s1 →
     stack_preserved ends_with_ret s1 (State f' fs m)
-| sp_stop : ∀e,s1,r.
-    stack_preserved e s1 (Finalstate r)
+| sp_stop : ∀s1,r.
+    stack_of_state [ ] s1 →
+    stack_preserved ends_with_ret s1 (Finalstate r)
+| sp_top : ∀fd,args,dst,m,r.
+    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
 .
 
@@ -591 +595 @@
 
 lemma stack_preserved_final : ∀e,r,s.
-  stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'.
-#e #r #s #H inversion H
+  ¬stack_preserved e (Finalstate r) s.
+#e #r #s % #H inversion H
 [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
   inversion SOS #a #b #c #d #e #f try #g try #h destruct
-| #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct
+| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
   inversion SOS #a #b #c #d #e #f try #g try #h destruct
-| #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl
+| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
+  inversion SOS #a #b #c #d #e #f try #g try #h destruct
+| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
 ] qed.
 
@@ -609 +615 @@
   [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
     @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
-  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
+  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
     @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
-  | #s1'' #r #E1 #E2 #E3 #E4 destruct //
+  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
+  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
+    inversion S2
+    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
+    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
+    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
+    ]
   ]
 | #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
 | #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
-  cases (stack_preserved_final … H) #r #E destruct //
+  cases (stack_preserved_final … H) #r #E destruct
+| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
+  @(absurd … F) //
 ] qed.
 
@@ -628 +642 @@
 | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
 | #res #dst *
-  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct // | *: normalize #a try #b destruct ] ]
+  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
+    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
   | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
     whd in EV:(??%?); destruct @(sp_finished ? f) //
+    cases f //
   ]
 | #r #s2 #tr #E normalize in E; destruct 
@@ -660 +676 @@
 inversion SP
 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
-| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
+| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
   inversion (eval_perserves … EV)
   [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
@@ -674 +690 @@
   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
   ]
-| #e #s1 #r #E1 #E2 #E3 #_ destruct //
+| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
+  inversion (eval_perserves … EV)
+  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
+  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
+  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
+    inversion S1
+    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
+    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
+    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
+    ]
+  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
+  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
+  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
+  ]
+| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
 ] qed. 
   
@@ -686 +716 @@
 inversion S23
 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
-| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
+| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
   inversion (eval_perserves … EV)
   [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
@@ -692 +722 @@
   | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
     inversion S
-    [ #fy #fsy #my #E1 #E2 #E3 destruct @N
+    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
     | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
     | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
@@ -700 +730 @@
   | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
   ]
-| #e #s1 #r #E1 #E2 #E3 #E4 destruct //
+| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
+  inversion (eval_perserves … EV)
+  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
+  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
+  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
+    inversion S1
+    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
+    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
+    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
+    ]
+  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
+  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
+  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
+  ]
+| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
 ] qed.
 
@@ -1244 +1288 @@
 ] qed.
 
+lemma bound_after_call : ∀ge,s,s',n.
+  state_bound_on_steps_to_cost s (S n) →
+  ∀CL:RTLabs_classify s = cl_call.
+  as_after_return (RTLabs_status ge) «s, CL» s' →
+  RTLabs_cost s' = false →
+  state_bound_on_steps_to_cost s' n.
+#ge #s #s' #n #H inversion H
+[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
+  #fn * #args * #dst * #stk * #m' #E destruct
+| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
+  whd in S; #CL cases s'
+  [ #f' #fs' #m' * #N #F #CS
+    %1 whd
+    inversion S
+    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
+      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
+    | #l #n #B #E1 #E2 #_ destruct <N <F @B
+    ]
+  | #fd' #args' #dst' #fs' #m' *
+  | #rv #dst' #fs' #m' *
+  | #r #E normalize in E; destruct
+  ]
+| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
+] qed.
+
 lemma bound_after_step : ∀ge,s,tr,s',n.
   state_bound_on_steps_to_cost s (S n) →
@@ -1291 +1360 @@
   | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
     %1 whd in FS ⊢ %;
-    inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct | 4: #H276 #H277 #H278 #H279 #H280 #H281 #H282 destruct ]
-    #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
+    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
+    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
     inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
     inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
@@ -1414 +1483 @@
   cases (terminates … tlr) //
 | (* FIXME: post-call not-wrong *)
-| (* FIXME: bound on steps after call *)
+| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
+  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
 | @(well_cost_labelled_state_step … EV) //
 | @(well_cost_labelled_call … EV) //