[1537] | 1 | |
---|
| 2 | include "RTLabs/semantics.ma". |
---|
| 3 | include "common/StructuredTraces.ma". |
---|
| 4 | |
---|
[1552] | 5 | discriminator status_class. |
---|
[1537] | 6 | |
---|
[1565] | 7 | (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps |
---|
| 8 | will be added later (LTL → LIN). *) |
---|
[1552] | 9 | |
---|
[1563] | 10 | definition RTLabs_classify : state → status_class ≝ |
---|
| 11 | λs. match s with |
---|
[1565] | 12 | [ State f _ _ ⇒ |
---|
| 13 | match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with |
---|
| 14 | [ St_cond _ _ _ ⇒ cl_jump |
---|
| 15 | | St_jumptable _ _ ⇒ cl_jump |
---|
| 16 | | _ ⇒ cl_other |
---|
| 17 | ] |
---|
[1563] | 18 | | Callstate _ _ _ _ _ ⇒ cl_call |
---|
| 19 | | Returnstate _ _ _ _ ⇒ cl_return |
---|
| 20 | ]. |
---|
[1552] | 21 | |
---|
[1583] | 22 | definition RTLabs_cost : state → bool ≝ |
---|
| 23 | λs. match s with |
---|
| 24 | [ State f fs m ⇒ |
---|
| 25 | match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with |
---|
| 26 | [ St_cost c l ⇒ true |
---|
| 27 | | _ ⇒ false |
---|
| 28 | ] |
---|
| 29 | | _ ⇒ false |
---|
| 30 | ]. |
---|
[1552] | 31 | |
---|
[1537] | 32 | definition RTLabs_status : genv → abstract_status ≝ |
---|
| 33 | λge. |
---|
| 34 | mk_abstract_status |
---|
| 35 | state |
---|
| 36 | (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) |
---|
[1563] | 37 | (λs,c. RTLabs_classify s = c) |
---|
[1583] | 38 | (λs. RTLabs_cost s = true) |
---|
[1537] | 39 | (λs,s'. match s with |
---|
| 40 | [ dp s p ⇒ |
---|
[1563] | 41 | match s return λs. RTLabs_classify s = cl_call → ? with |
---|
[1537] | 42 | [ Callstate fd args dst stk m ⇒ |
---|
| 43 | λ_. match s' with |
---|
| 44 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ] |
---|
| 45 | | _ ⇒ False |
---|
| 46 | ] |
---|
| 47 | | State f fs m ⇒ λH.⊥ |
---|
| 48 | | _ ⇒ λH.⊥ |
---|
| 49 | ] p |
---|
| 50 | ]). |
---|
[1563] | 51 | [ normalize in H; destruct |
---|
[1565] | 52 | | whd in H:(??%?); |
---|
| 53 | cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; |
---|
| 54 | normalize try #a try #b try #c try #d try #e try #g try #h destruct |
---|
[1563] | 55 | ] qed. |
---|
[1559] | 56 | |
---|
| 57 | (* Before attempting to construct a structured trace, let's show that we can |
---|
| 58 | form flat traces with evidence that they were constructed from an execution. |
---|
| 59 | |
---|
| 60 | For now we don't consider I/O. *) |
---|
| 61 | |
---|
| 62 | |
---|
| 63 | coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ |
---|
| 64 | | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) |
---|
| 65 | | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) |
---|
| 66 | | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). |
---|
| 67 | |
---|
| 68 | (* add I/O? *) |
---|
| 69 | coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ |
---|
| 70 | | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s |
---|
| 71 | | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s |
---|
| 72 | | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. |
---|
| 73 | |
---|
| 74 | let corec make_flat_trace ge s |
---|
| 75 | (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : |
---|
| 76 | flat_trace io_out io_in ge s ≝ |
---|
| 77 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
| 78 | match e return λx. e = x → ? with |
---|
| 79 | [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) |
---|
| 80 | | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) |
---|
| 81 | | e_wrong m ⇒ λE. ft_wrong … s m ? |
---|
| 82 | | e_interact o f ⇒ λE. ⊥ |
---|
| 83 | ] (refl ? e). |
---|
| 84 | [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 85 | cases (eval_statement ge s) |
---|
| 86 | [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 87 | | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 88 | >(?:is_final ????? = RTLabs_is_final s1) // |
---|
| 89 | lapply (refl ? (RTLabs_is_final s1)) |
---|
| 90 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
| 91 | [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct |
---|
| 92 | | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl |
---|
| 93 | | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct |
---|
| 94 | ] |
---|
| 95 | | *: #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 96 | ] |
---|
| 97 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 98 | cases (eval_statement ge s) |
---|
| 99 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 100 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 101 | cases (is_final ?????) |
---|
| 102 | [ whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 103 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 104 | ] |
---|
| 105 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 106 | ] |
---|
| 107 | | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; |
---|
| 108 | cases (eval_statement ge s) |
---|
| 109 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 110 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 111 | cases (is_final ?????) |
---|
| 112 | [ whd in ⊢ (??%? → ?); #E |
---|
| 113 | change with (eval_statement ge s1) in E:(??(??????(?????%))?); |
---|
| 114 | destruct |
---|
| 115 | inversion H |
---|
| 116 | [ #a #b #c #E1 destruct |
---|
| 117 | | #trx #sx #ex #H1 #E2 #E3 destruct @H1 |
---|
| 118 | | #m #E1 destruct |
---|
| 119 | ] |
---|
| 120 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 121 | ] |
---|
| 122 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 123 | ] |
---|
| 124 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 125 | cases (eval_statement ge s) |
---|
| 126 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 127 | | * #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
| 128 | cases (is_final ?????) |
---|
| 129 | [ whd in ⊢ (??%? → ?); #E destruct |
---|
| 130 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 131 | ] |
---|
| 132 | | #m whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 133 | ] |
---|
| 134 | | whd in E:(??%?); >E in H; #H |
---|
| 135 | inversion H |
---|
| 136 | [ #a #b #c #E destruct |
---|
| 137 | | #a #b #c #d #E1 destruct |
---|
| 138 | | #m #E1 destruct |
---|
| 139 | ] |
---|
| 140 | ] qed. |
---|
| 141 | |
---|
| 142 | let corec make_whole_flat_trace p s |
---|
| 143 | (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) |
---|
| 144 | (I:make_initial_state ??? p = OK ? s) : |
---|
| 145 | flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ |
---|
| 146 | let ge ≝ make_global … p in |
---|
| 147 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
| 148 | match e return λx. e = x → ? with |
---|
| 149 | [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? |
---|
| 150 | | e_step _ _ e' ⇒ λE. make_flat_trace ge s ? |
---|
| 151 | | e_wrong m ⇒ λE. ⊥ |
---|
| 152 | | e_interact o f ⇒ λE. ⊥ |
---|
| 153 | ] (refl ? e). |
---|
| 154 | [ whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 155 | whd in ⊢ (??%? → ?); |
---|
| 156 | >(?:is_final ????? = RTLabs_is_final s) // |
---|
| 157 | lapply (refl ? (RTLabs_is_final s)) |
---|
| 158 | cases (RTLabs_is_final s) in ⊢ (???% → %); |
---|
| 159 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
| 160 | | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct |
---|
| 161 | ] |
---|
| 162 | | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); |
---|
| 163 | >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) |
---|
| 164 | [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H |
---|
| 165 | [ #a #b #c #E1 destruct |
---|
| 166 | | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) |
---|
| 167 | @H1 |
---|
| 168 | | #m #E1 destruct |
---|
| 169 | ] |
---|
| 170 | | #i whd in ⊢ (??%? → ???% → ?); #E destruct |
---|
| 171 | ] |
---|
| 172 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
| 173 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
| 174 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
| 175 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
| 176 | ] qed. |
---|
| 177 | |
---|
[1563] | 178 | (* Need a way to choose whether a called function terminates. Then, |
---|
| 179 | if the initial function terminates we generate a purely inductive structured trace, |
---|
| 180 | otherwise we start generating the coinductive one, and on every function call |
---|
| 181 | use the choice method again to decide whether to step over or keep going. |
---|
| 182 | |
---|
| 183 | Not quite what we need - have to decide on seeing each label whether we will see |
---|
| 184 | another or hit a non-terminating call? |
---|
| 185 | |
---|
| 186 | Also - need the notion of well-labelled in order to break loops. |
---|
| 187 | |
---|
| 188 | |
---|
| 189 | |
---|
| 190 | outline: |
---|
| 191 | |
---|
| 192 | does function terminate? |
---|
| 193 | - yes, get (bound on the number of steps until return), generate finite |
---|
| 194 | structure using bound as termination witness |
---|
| 195 | - no, get (¬ bound on steps to return), start building infinite trace out of |
---|
| 196 | finite steps. At calls, check for termination, generate appr. form. |
---|
| 197 | |
---|
| 198 | generating the finite parts: |
---|
| 199 | |
---|
| 200 | We start with the status after the call has been executed; well-labelling tells |
---|
| 201 | us that this is a labelled state. Now we want to generate a trace_label_return |
---|
| 202 | and also return the remainder of the flat trace. |
---|
| 203 | |
---|
| 204 | *) |
---|
| 205 | |
---|
| 206 | (* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from |
---|
| 207 | [s] we reach the return state for the current function. [depth] performs |
---|
| 208 | the call/return counting necessary for handling deeper function calls. |
---|
| 209 | It should be zero at the top level. *) |
---|
| 210 | inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝ |
---|
| 211 | | nir_step : ∀n,s,tr,s',depth,EX,trace. |
---|
[1565] | 212 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
[1563] | 213 | nth_is_return ge n depth s' trace → |
---|
| 214 | nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace) |
---|
| 215 | | nir_call : ∀n,s,tr,s',depth,EX,trace. |
---|
| 216 | RTLabs_classify s = cl_call → |
---|
| 217 | nth_is_return ge n (S depth) s' trace → |
---|
| 218 | nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace) |
---|
| 219 | | nir_ret : ∀n,s,tr,s',depth,EX,trace. |
---|
| 220 | RTLabs_classify s = cl_return → |
---|
| 221 | nth_is_return ge n depth s' trace → |
---|
| 222 | nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace) |
---|
[1583] | 223 | (* Note that we require the ability to make a step after the return (this |
---|
| 224 | corresponds to somewhere that will be guaranteed to be a label at the |
---|
| 225 | end of the compilation chain). *) |
---|
| 226 | | nir_base : ∀s,tr,s',EX,trace. |
---|
[1563] | 227 | RTLabs_classify s = cl_return → |
---|
[1583] | 228 | nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace) |
---|
[1563] | 229 | . |
---|
| 230 | |
---|
| 231 | discriminator nat. |
---|
| 232 | |
---|
| 233 | (* Find time until a nested call completes. *) |
---|
| 234 | lemma nth_is_return_down : ∀ge,n,depth,s,trace. |
---|
| 235 | nth_is_return ge n (S depth) s trace → |
---|
| 236 | ∃m. nth_is_return ge m depth s trace. |
---|
| 237 | #ge #n elim n |
---|
| 238 | (* It's impossible to run out of time... *) |
---|
| 239 | [ #depth #s #trace #H inversion H |
---|
| 240 | [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct |
---|
| 241 | | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct |
---|
| 242 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct |
---|
| 243 | | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct |
---|
| 244 | ] |
---|
| 245 | | #n' #IH #depth #s #trace #H inversion H |
---|
| 246 | [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
| 247 | cases (IH depth s1' trace1 ?) |
---|
| 248 | [ #m' #H' %{(S m')} %1 // |
---|
| 249 | | // |
---|
| 250 | ] |
---|
| 251 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
| 252 | cases (IH (S depth) s1' trace1 ?) |
---|
| 253 | [ #m' #H' %{(S m')} %2 // |
---|
| 254 | | // |
---|
| 255 | ] |
---|
| 256 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
| 257 | cases (depth1) in H2 ⊢ %; |
---|
| 258 | [ #H2 %{O} %4 // |
---|
| 259 | | #depth' #H2 cases (IH depth' s1' trace1 ?) |
---|
| 260 | [ #m' #H' %{(S m')} %3 // |
---|
| 261 | | // |
---|
| 262 | ] |
---|
| 263 | ] |
---|
| 264 | | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct |
---|
| 265 | ] |
---|
| 266 | ] qed. |
---|
| 267 | |
---|
| 268 | lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace. |
---|
| 269 | RTLabs_classify s = cl_call → |
---|
| 270 | nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → |
---|
| 271 | ∃m. nth_is_return ge m O s' trace. |
---|
| 272 | #ge #n #s #tr #s' #EX #trace #CLASS #H |
---|
| 273 | inversion H |
---|
[1565] | 274 | [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥ |
---|
[1563] | 275 | -H2 destruct >H1 in CLASS; #E destruct |
---|
| 276 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
| 277 | @nth_is_return_down // |
---|
| 278 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ |
---|
| 279 | -H2 destruct |
---|
[1583] | 280 | | #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct |
---|
[1563] | 281 | ] qed. |
---|
| 282 | |
---|
[1583] | 283 | lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace. |
---|
| 284 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
| 285 | nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → |
---|
| 286 | nth_is_return ge (pred n) O s' trace. |
---|
| 287 | #ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM |
---|
| 288 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // |
---|
| 289 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct |
---|
| 290 | | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct |
---|
| 291 | | #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct |
---|
| 292 | | #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct // |
---|
| 293 | | #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct |
---|
| 294 | | #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct |
---|
| 295 | | #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct |
---|
| 296 | ] qed. |
---|
| 297 | |
---|
[1565] | 298 | (* We require that labels appear after branch instructions and at the start of |
---|
[1574] | 299 | functions. The first is required for preciseness, the latter for soundness. |
---|
| 300 | We will make a separate requirement for there to be a finite number of steps |
---|
| 301 | between labels to catch loops for soundness (is this sufficient?). *) |
---|
[1565] | 302 | |
---|
| 303 | definition is_cost_label : statement → Prop ≝ |
---|
| 304 | λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ]. |
---|
| 305 | |
---|
| 306 | let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝ |
---|
| 307 | match l return λl.All A P l → Prop with |
---|
| 308 | [ nil ⇒ λ_. True |
---|
| 309 | | cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H) |
---|
| 310 | ] H. |
---|
| 311 | |
---|
| 312 | definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ |
---|
| 313 | λf,s. match s return λs. labels_present ? s → Prop with |
---|
| 314 | [ St_cond _ l1 l2 ⇒ λH. |
---|
| 315 | is_cost_label (lookup_present … (f_graph f) l1 ?) ∧ |
---|
| 316 | is_cost_label (lookup_present … (f_graph f) l2 ?) |
---|
| 317 | | St_jumptable _ ls ⇒ λH. |
---|
| 318 | All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H |
---|
| 319 | | _ ⇒ λ_. True |
---|
| 320 | ]. whd in H; |
---|
| 321 | [ @(proj1 … H) |
---|
| 322 | | @(proj2 … H) |
---|
| 323 | ] qed. |
---|
| 324 | |
---|
| 325 | definition well_cost_labelled_fn : internal_function → Prop ≝ |
---|
| 326 | λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s. |
---|
| 327 | well_cost_labelled_statement f s (f_closed f …)) ∧ |
---|
| 328 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). |
---|
| 329 | [ 2: @H | skip | cases (f_entry f) // ] qed. |
---|
| 330 | |
---|
| 331 | (* We need to ensure that any code we come across is well-cost-labelled. We may |
---|
| 332 | get function code from either the global environment or the state. *) |
---|
| 333 | |
---|
| 334 | definition well_cost_labelled_ge : genv → Prop ≝ |
---|
[1583] | 335 | λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. |
---|
[1565] | 336 | |
---|
| 337 | definition well_cost_labelled_state : state → Prop ≝ |
---|
| 338 | λs. match s with |
---|
| 339 | [ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
| 340 | | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧ |
---|
| 341 | All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
| 342 | | Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
| 343 | ]. |
---|
| 344 | |
---|
[1583] | 345 | lemma well_cost_labelled_state_step : ∀ge,s,tr,s'. |
---|
| 346 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 347 | well_cost_labelled_ge ge → |
---|
| 348 | well_cost_labelled_state s → |
---|
| 349 | well_cost_labelled_state s'. |
---|
| 350 | #ge #s #tr' #s' #EV cases (eval_perserves … EV) |
---|
| 351 | [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // |
---|
| 352 | | #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ |
---|
| 353 | | #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ |
---|
| 354 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ |
---|
| 355 | | #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 |
---|
| 356 | | #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // |
---|
| 357 | ] qed. |
---|
| 358 | |
---|
[1574] | 359 | (* Don't need to know that labels break loops because we have termination. *) |
---|
| 360 | |
---|
| 361 | record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ { |
---|
| 362 | new_state : state; |
---|
| 363 | termination_count : nat; |
---|
| 364 | remainder : flat_trace io_out io_in ge new_state; |
---|
| 365 | terminates : nth_is_return ge termination_count O new_state remainder; |
---|
| 366 | cost_labelled : well_cost_labelled_state new_state; |
---|
| 367 | new_trace : T new_state |
---|
| 368 | }. |
---|
| 369 | |
---|
| 370 | definition replace_new_trace : ∀ge,T1,T2. |
---|
| 371 | ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝ |
---|
| 372 | λge,T1,T2,r,trace. |
---|
| 373 | mk_make_result ge T2 |
---|
| 374 | (new_state … r) |
---|
| 375 | (termination_count … r) |
---|
| 376 | (remainder … r) |
---|
| 377 | (terminates … r) |
---|
| 378 | (cost_labelled … r) |
---|
| 379 | trace. |
---|
| 380 | |
---|
[1563] | 381 | let rec make_label_return n ge s |
---|
[1565] | 382 | (trace: flat_trace io_out io_in ge s) |
---|
| 383 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
[1574] | 384 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
[1583] | 385 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
[1565] | 386 | (TERMINATES: nth_is_return ge n O s trace) |
---|
[1574] | 387 | : make_result ge (trace_label_return (RTLabs_status ge) s) ≝ |
---|
| 388 | |
---|
| 389 | let r ≝ make_label_label n ge s trace ???? in |
---|
| 390 | match new_trace … r with |
---|
| 391 | [ dp ends tll ⇒ |
---|
| 392 | match ends return λx. trace_label_label ? x ?? → ? with |
---|
| 393 | [ ends_with_ret ⇒ λtll. |
---|
| 394 | replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll) |
---|
| 395 | | doesnt_end_with_ret ⇒ λtll. |
---|
| 396 | let r' ≝ make_label_return (termination_count … r) ge (new_state … r) |
---|
| 397 | (remainder … r) ??? (terminates … r) in |
---|
| 398 | replace_new_trace … r' |
---|
| 399 | (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r')) |
---|
| 400 | ] tll |
---|
| 401 | ] |
---|
| 402 | |
---|
| 403 | and make_label_label n ge s |
---|
| 404 | (trace: flat_trace io_out io_in ge s) |
---|
| 405 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 406 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
[1583] | 407 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
[1574] | 408 | (TERMINATES: nth_is_return ge n O s trace) |
---|
| 409 | : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝ |
---|
| 410 | let r ≝ make_any_label n ge s trace ??? in |
---|
| 411 | match new_trace … r with |
---|
| 412 | [ dp ends tr ⇒ |
---|
| 413 | replace_new_trace ??? r |
---|
| 414 | (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL)) |
---|
| 415 | ] |
---|
| 416 | |
---|
| 417 | and make_any_label n ge s |
---|
| 418 | (trace: flat_trace io_out io_in ge s) |
---|
| 419 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 420 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
| 421 | (TERMINATES: nth_is_return ge n O s trace) |
---|
| 422 | : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝ |
---|
[1583] | 423 | match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with |
---|
| 424 | [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? |
---|
| 425 | | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. |
---|
| 426 | match RTLabs_classify start return λx. RTLabs_classify start = x → ? with |
---|
| 427 | [ cl_other ⇒ λCL. |
---|
| 428 | match RTLabs_cost next return λx. RTLabs_cost next = x → ? with |
---|
| 429 | [ true ⇒ λCS. |
---|
| 430 | mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???)) |
---|
| 431 | | false ⇒ λCS. |
---|
| 432 | let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in |
---|
| 433 | match new_trace … r with |
---|
| 434 | [ dp ends trc ⇒ |
---|
| 435 | replace_new_trace ??? r |
---|
| 436 | (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??)) |
---|
| 437 | ] |
---|
| 438 | ] (refl ??) |
---|
| 439 | | cl_jump ⇒ λCL. ? |
---|
| 440 | | cl_call ⇒ λCL. ? |
---|
| 441 | | cl_return ⇒ λCL. ? |
---|
| 442 | ] (refl ? (RTLabs_classify start)) |
---|
| 443 | | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ |
---|
| 444 | ] STATE_COSTLABELLED TERMINATES. |
---|
[1574] | 445 | |
---|
| 446 | [ // |
---|
| 447 | | // |
---|
| 448 | | @(trace_label_label_label … tll) |
---|
| 449 | | // |
---|
| 450 | | // |
---|
| 451 | | // |
---|
| 452 | | // |
---|
| 453 | | // |
---|
| 454 | | // |
---|
| 455 | | // |
---|
| 456 | | |
---|
| 457 | | |
---|
[1583] | 458 | | |
---|
| 459 | | |
---|
| 460 | | @(nth_is_return_notfn … TERMINATES) %1 @CL |
---|
| 461 | | @(well_cost_labelled_state_step … EV) // |
---|
| 462 | | %{tr} @EV |
---|
| 463 | | |
---|
| 464 | | @CS |
---|
| 465 | | %{tr} @EV |
---|
| 466 | | @CL |
---|
| 467 | | % whd in ⊢ (% → ?); >CS #E destruct |
---|
| 468 | | @(well_cost_labelled_state_step … EV) // |
---|
| 469 | | @(nth_is_return_notfn … TERMINATES) %1 @CL |
---|
[1574] | 470 | | inversion TERMINATES |
---|
| 471 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct |
---|
| 472 | | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct |
---|
| 473 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct |
---|
[1583] | 474 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct |
---|
| 475 | ] |
---|
| 476 | | |
---|
| 477 | |
---|
| 478 | |
---|
[1574] | 479 | |
---|
[1583] | 480 | (* FIXME: there's trouble at the end of the program because we can't make a step |
---|
| 481 | away from the final return. *) |
---|