[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 |
---|
[1713] | 20 | | Finalstate _ ⇒ cl_other |
---|
[1563] | 21 | ]. |
---|
[1552] | 22 | |
---|
[1960] | 23 | (* We define a straight "is this a cost label" pair of functions, which is |
---|
| 24 | convenient for most of our uses here (because we can make a hypothesis of |
---|
| 25 | it without naming the label), and a pair which return the label to fit the |
---|
| 26 | definition of abstract_status. *) |
---|
| 27 | |
---|
[1705] | 28 | definition is_cost_label : statement → bool ≝ |
---|
| 29 | λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. |
---|
| 30 | |
---|
[1583] | 31 | definition RTLabs_cost : state → bool ≝ |
---|
| 32 | λs. match s with |
---|
| 33 | [ State f fs m ⇒ |
---|
[1586] | 34 | is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) |
---|
[1583] | 35 | | _ ⇒ false |
---|
| 36 | ]. |
---|
[1552] | 37 | |
---|
[1960] | 38 | definition cost_label_of : statement → option costlabel ≝ |
---|
| 39 | λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ]. |
---|
| 40 | |
---|
| 41 | definition RTLabs_cost_label : state → option costlabel ≝ |
---|
| 42 | λs. match s with |
---|
| 43 | [ State f fs m ⇒ |
---|
| 44 | cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) |
---|
| 45 | | _ ⇒ None ? |
---|
| 46 | ]. |
---|
| 47 | |
---|
| 48 | (* At the moment we don't need to talk about the program counter, so we just |
---|
| 49 | use unit. *) |
---|
| 50 | definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?. |
---|
| 51 | * * % // |
---|
| 52 | qed. |
---|
| 53 | |
---|
| 54 | definition RTLabs_status : genv → abstract_status ≝ |
---|
[1537] | 55 | λge. |
---|
[1960] | 56 | mk_abstract_status |
---|
[1537] | 57 | state |
---|
| 58 | (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) |
---|
[1960] | 59 | unit_deqset |
---|
| 60 | (λ_. it) |
---|
[1563] | 61 | (λs,c. RTLabs_classify s = c) |
---|
[1960] | 62 | RTLabs_cost_label |
---|
[1537] | 63 | (λs,s'. match s with |
---|
[1601] | 64 | [ mk_Sig s p ⇒ |
---|
[1563] | 65 | match s return λs. RTLabs_classify s = cl_call → ? with |
---|
[1537] | 66 | [ Callstate fd args dst stk m ⇒ |
---|
| 67 | λ_. match s' with |
---|
[1736] | 68 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ] |
---|
| 69 | | Finalstate r ⇒ stk = [ ] |
---|
[1537] | 70 | | _ ⇒ False |
---|
| 71 | ] |
---|
| 72 | | State f fs m ⇒ λH.⊥ |
---|
| 73 | | _ ⇒ λH.⊥ |
---|
| 74 | ] p |
---|
[1960] | 75 | ]) |
---|
[1880] | 76 | (λs. RTLabs_is_final s ≠ None ?). |
---|
[1960] | 77 | [ normalize in H; destruct |
---|
| 78 | | normalize in H; destruct |
---|
| 79 | | whd in H:(??%?); |
---|
[1565] | 80 | cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; |
---|
[1877] | 81 | normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct |
---|
[1563] | 82 | ] qed. |
---|
[1559] | 83 | |
---|
[1960] | 84 | (* Allow us to move between the different notions of when a state is cost |
---|
| 85 | labelled. *) |
---|
| 86 | |
---|
| 87 | lemma RTLabs_costed : ∀ge,s. |
---|
| 88 | RTLabs_cost s = true → |
---|
| 89 | as_costed (RTLabs_status ge) s. |
---|
| 90 | #ge * |
---|
| 91 | [ * #func #locals #next #nok #b #r #fs #m |
---|
| 92 | whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?)); |
---|
| 93 | cases (lookup_present ?? (f_graph func) ??) normalize |
---|
| 94 | #A try #B try #C try #D try #E try #F try #G try #H try #G destruct |
---|
| 95 | % #E' destruct |
---|
| 96 | | normalize #fd #args #r #fs #m #E destruct |
---|
| 97 | | normalize #A #B #C #D #E destruct |
---|
| 98 | | normalize #A #B destruct |
---|
| 99 | ] qed. |
---|
| 100 | |
---|
| 101 | lemma costed_RTLabs : ∀ge,s. |
---|
| 102 | as_costed (RTLabs_status ge) s → |
---|
| 103 | RTLabs_cost s = true. |
---|
| 104 | #ge |
---|
| 105 | cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H |
---|
| 106 | * |
---|
| 107 | [ * #func #locals #next #nok #b #r #fs #m |
---|
| 108 | whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?); |
---|
| 109 | cases (lookup_present ?? (f_graph func) ??) normalize // |
---|
| 110 | #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) // |
---|
| 111 | | *: normalize #A #B try #C try #D try #E try #F cases (H ?) // |
---|
| 112 | ] qed. |
---|
| 113 | |
---|
[1670] | 114 | lemma RTLabs_not_cost : ∀ge,s. |
---|
| 115 | RTLabs_cost s = false → |
---|
| 116 | ¬ as_costed (RTLabs_status ge) s. |
---|
[1960] | 117 | #ge * |
---|
| 118 | [ * #func #locals #next #nok #b #r #fs #m |
---|
| 119 | whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?))); |
---|
| 120 | cases (lookup_present ?? (f_graph func) ??) normalize |
---|
| 121 | #A try #B try #C try #D try #E try #F try #G try #H try #I destruct |
---|
| 122 | % * #J @J @refl |
---|
| 123 | | *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl |
---|
| 124 | ] qed. |
---|
[1670] | 125 | |
---|
[1559] | 126 | (* Before attempting to construct a structured trace, let's show that we can |
---|
| 127 | form flat traces with evidence that they were constructed from an execution. |
---|
| 128 | |
---|
| 129 | For now we don't consider I/O. *) |
---|
| 130 | |
---|
| 131 | |
---|
| 132 | coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ |
---|
| 133 | | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) |
---|
| 134 | | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) |
---|
| 135 | | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). |
---|
| 136 | |
---|
| 137 | (* add I/O? *) |
---|
| 138 | coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ |
---|
| 139 | | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s |
---|
| 140 | | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s |
---|
[1880] | 141 | | ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s. |
---|
[1559] | 142 | |
---|
[1707] | 143 | coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝ |
---|
| 144 | | nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H) |
---|
| 145 | | 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'). |
---|
| 146 | |
---|
| 147 | lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'. |
---|
| 148 | not_wrong o i ge s (ft_step o i ge s tr s' H tr') → |
---|
| 149 | not_wrong o i ge s' tr'. |
---|
| 150 | #o #i #ge #s #tr #s' #H #tr' #NW inversion NW |
---|
| 151 | [ #H105 #H106 #H107 #H108 #H109 destruct |
---|
| 152 | | #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct // |
---|
| 153 | ] qed. |
---|
| 154 | |
---|
[1559] | 155 | let corec make_flat_trace ge s |
---|
[1880] | 156 | (NF:RTLabs_is_final s = None ?) |
---|
[1559] | 157 | (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : |
---|
| 158 | flat_trace io_out io_in ge s ≝ |
---|
| 159 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
| 160 | match e return λx. e = x → ? with |
---|
| 161 | [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) |
---|
[1880] | 162 | | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??) |
---|
| 163 | | e_wrong m ⇒ λE. ft_wrong … s m ?? |
---|
[1559] | 164 | | e_interact o f ⇒ λE. ⊥ |
---|
| 165 | ] (refl ? e). |
---|
| 166 | [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 167 | cases (eval_statement ge s) |
---|
| 168 | [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 169 | | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 170 | >(?:is_final ????? = RTLabs_is_final s1) // |
---|
| 171 | lapply (refl ? (RTLabs_is_final s1)) |
---|
| 172 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
| 173 | [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct |
---|
| 174 | | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl |
---|
| 175 | | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct |
---|
| 176 | ] |
---|
| 177 | | *: #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 178 | ] |
---|
| 179 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 180 | cases (eval_statement ge s) |
---|
| 181 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 182 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 183 | cases (is_final ?????) |
---|
| 184 | [ whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 185 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 186 | ] |
---|
| 187 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 188 | ] |
---|
| 189 | | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; |
---|
| 190 | cases (eval_statement ge s) |
---|
| 191 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 192 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 193 | cases (is_final ?????) |
---|
| 194 | [ whd in ⊢ (??%? → ?); #E |
---|
| 195 | change with (eval_statement ge s1) in E:(??(??????(?????%))?); |
---|
| 196 | destruct |
---|
| 197 | inversion H |
---|
| 198 | [ #a #b #c #E1 destruct |
---|
| 199 | | #trx #sx #ex #H1 #E2 #E3 destruct @H1 |
---|
| 200 | | #m #E1 destruct |
---|
| 201 | ] |
---|
| 202 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 203 | ] |
---|
| 204 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
| 205 | ] |
---|
| 206 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 207 | cases (eval_statement ge s) |
---|
[1880] | 208 | [ #o #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 209 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
| 210 | lapply (refl ? (RTLabs_is_final s1)) |
---|
| 211 | change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?); |
---|
| 212 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
| 213 | [ #F #E whd in E:(??%?); destruct @F |
---|
| 214 | | #r #F #E whd in E:(??%?); destruct |
---|
| 215 | ] |
---|
| 216 | | #m #E whd in E:(??%?); destruct |
---|
| 217 | ] |
---|
| 218 | | @NF |
---|
| 219 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 220 | cases (eval_statement ge s) |
---|
[1559] | 221 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
| 222 | | * #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
| 223 | cases (is_final ?????) |
---|
| 224 | [ whd in ⊢ (??%? → ?); #E destruct |
---|
| 225 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
| 226 | ] |
---|
| 227 | | #m whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 228 | ] |
---|
| 229 | | whd in E:(??%?); >E in H; #H |
---|
| 230 | inversion H |
---|
| 231 | [ #a #b #c #E destruct |
---|
| 232 | | #a #b #c #d #E1 destruct |
---|
| 233 | | #m #E1 destruct |
---|
| 234 | ] |
---|
| 235 | ] qed. |
---|
| 236 | |
---|
| 237 | let corec make_whole_flat_trace p s |
---|
| 238 | (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) |
---|
| 239 | (I:make_initial_state ??? p = OK ? s) : |
---|
| 240 | flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ |
---|
| 241 | let ge ≝ make_global … p in |
---|
| 242 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
| 243 | match e return λx. e = x → ? with |
---|
| 244 | [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? |
---|
[1880] | 245 | | e_step _ _ e' ⇒ λE. make_flat_trace ge s ?? |
---|
[1559] | 246 | | e_wrong m ⇒ λE. ⊥ |
---|
| 247 | | e_interact o f ⇒ λE. ⊥ |
---|
| 248 | ] (refl ? e). |
---|
| 249 | [ whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
| 250 | whd in ⊢ (??%? → ?); |
---|
[1880] | 251 | change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?); |
---|
| 252 | cases (RTLabs_is_final s) |
---|
| 253 | [ #E whd in E:(??%?); destruct |
---|
| 254 | | #r #E % #E' destruct |
---|
[1559] | 255 | ] |
---|
[1880] | 256 | | @(initial_state_is_not_final … I) |
---|
[1559] | 257 | | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); |
---|
| 258 | >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) |
---|
| 259 | [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H |
---|
| 260 | [ #a #b #c #E1 destruct |
---|
| 261 | | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) |
---|
| 262 | @H1 |
---|
| 263 | | #m #E1 destruct |
---|
| 264 | ] |
---|
| 265 | | #i whd in ⊢ (??%? → ???% → ?); #E destruct |
---|
| 266 | ] |
---|
| 267 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
| 268 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
| 269 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
| 270 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
| 271 | ] qed. |
---|
| 272 | |
---|
[1563] | 273 | (* Need a way to choose whether a called function terminates. Then, |
---|
| 274 | if the initial function terminates we generate a purely inductive structured trace, |
---|
| 275 | otherwise we start generating the coinductive one, and on every function call |
---|
| 276 | use the choice method again to decide whether to step over or keep going. |
---|
| 277 | |
---|
| 278 | Not quite what we need - have to decide on seeing each label whether we will see |
---|
| 279 | another or hit a non-terminating call? |
---|
| 280 | |
---|
| 281 | Also - need the notion of well-labelled in order to break loops. |
---|
| 282 | |
---|
| 283 | |
---|
| 284 | |
---|
| 285 | outline: |
---|
| 286 | |
---|
| 287 | does function terminate? |
---|
| 288 | - yes, get (bound on the number of steps until return), generate finite |
---|
| 289 | structure using bound as termination witness |
---|
| 290 | - no, get (¬ bound on steps to return), start building infinite trace out of |
---|
| 291 | finite steps. At calls, check for termination, generate appr. form. |
---|
| 292 | |
---|
| 293 | generating the finite parts: |
---|
| 294 | |
---|
| 295 | We start with the status after the call has been executed; well-labelling tells |
---|
| 296 | us that this is a labelled state. Now we want to generate a trace_label_return |
---|
| 297 | and also return the remainder of the flat trace. |
---|
| 298 | |
---|
| 299 | *) |
---|
| 300 | |
---|
[1595] | 301 | (* [will_return ge depth s trace] says that after a finite number of steps of |
---|
| 302 | [trace] from [s] we reach the return state for the current function. [depth] |
---|
| 303 | performs the call/return counting necessary for handling deeper function |
---|
| 304 | calls. It should be zero at the top level. *) |
---|
[1637] | 305 | inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝ |
---|
[1595] | 306 | | wr_step : ∀s,tr,s',depth,EX,trace. |
---|
[1565] | 307 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
[1595] | 308 | will_return ge depth s' trace → |
---|
| 309 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
| 310 | | wr_call : ∀s,tr,s',depth,EX,trace. |
---|
[1563] | 311 | RTLabs_classify s = cl_call → |
---|
[1595] | 312 | will_return ge (S depth) s' trace → |
---|
| 313 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
| 314 | | wr_ret : ∀s,tr,s',depth,EX,trace. |
---|
[1563] | 315 | RTLabs_classify s = cl_return → |
---|
[1595] | 316 | will_return ge depth s' trace → |
---|
| 317 | will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace) |
---|
[1583] | 318 | (* Note that we require the ability to make a step after the return (this |
---|
| 319 | corresponds to somewhere that will be guaranteed to be a label at the |
---|
| 320 | end of the compilation chain). *) |
---|
[1595] | 321 | | wr_base : ∀s,tr,s',EX,trace. |
---|
[1563] | 322 | RTLabs_classify s = cl_return → |
---|
[1595] | 323 | will_return ge O s (ft_step ?? ge s tr s' EX trace) |
---|
[1563] | 324 | . |
---|
| 325 | |
---|
[1638] | 326 | (* The way we will use [will_return] won't satisfy Matita's guardedness check, |
---|
| 327 | so we will measure the length of these termination proofs and use an upper |
---|
| 328 | bound to show termination of the finite structured trace construction |
---|
| 329 | functions. *) |
---|
| 330 | |
---|
[1637] | 331 | let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝ |
---|
| 332 | match T with |
---|
| 333 | [ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
| 334 | | wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
| 335 | | wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
| 336 | | wr_base _ _ _ _ _ _ ⇒ S O |
---|
| 337 | ]. |
---|
[1638] | 338 | |
---|
[1637] | 339 | include alias "arithmetics/nat.ma". |
---|
| 340 | |
---|
[1638] | 341 | (* Specialised to the particular situation it is used in. *) |
---|
[1637] | 342 | lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False. |
---|
| 343 | #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] |
---|
| 344 | whd in ⊢ (??(??%) → ?); |
---|
| 345 | >commutative_times |
---|
| 346 | #H lapply (le_plus_b … H) |
---|
| 347 | #H lapply (le_to_leb_true … H) |
---|
| 348 | normalize #E destruct |
---|
| 349 | qed. |
---|
[1719] | 350 | |
---|
| 351 | let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝ |
---|
| 352 | match T with |
---|
| 353 | [ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T' |
---|
| 354 | | wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T' |
---|
| 355 | | wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T' |
---|
| 356 | | wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr' |
---|
| 357 | ]. |
---|
[1563] | 358 | |
---|
[1638] | 359 | (* Inversion lemmas on [will_return] that also note the effect on the length |
---|
| 360 | of the proof. *) |
---|
| 361 | lemma will_return_call : ∀ge,d,s,tr,s',EX,trace. |
---|
[1637] | 362 | RTLabs_classify s = cl_call → |
---|
| 363 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
[1719] | 364 | ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'. |
---|
[1637] | 365 | #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM |
---|
| 366 | [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct |
---|
[1719] | 367 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/ |
---|
[1637] | 368 | | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct |
---|
| 369 | | #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct |
---|
| 370 | ] qed. |
---|
[1595] | 371 | |
---|
[1637] | 372 | lemma will_return_return : ∀ge,d,s,tr,s',EX,trace. |
---|
| 373 | RTLabs_classify s = cl_return → |
---|
| 374 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
| 375 | match d with |
---|
[1719] | 376 | [ O ⇒ will_return_end … TM = ❬s', trace❭ |
---|
[1637] | 377 | | S d' ⇒ |
---|
[1719] | 378 | ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM' |
---|
[1637] | 379 | ]. |
---|
| 380 | #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM |
---|
| 381 | [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct |
---|
| 382 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥ destruct >CL in H39; #E destruct |
---|
[1719] | 383 | | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/ |
---|
| 384 | | #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl |
---|
[1637] | 385 | ] qed. |
---|
| 386 | |
---|
[1596] | 387 | lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace. |
---|
[1637] | 388 | (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) → |
---|
| 389 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
[1719] | 390 | ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'. |
---|
[1596] | 391 | #ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM |
---|
[1719] | 392 | [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/ |
---|
[1637] | 393 | | #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct |
---|
| 394 | | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct |
---|
| 395 | | #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct |
---|
[1719] | 396 | | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/ |
---|
[1637] | 397 | | #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct |
---|
| 398 | | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct |
---|
| 399 | | #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct |
---|
[1595] | 400 | ] qed. |
---|
| 401 | |
---|
[1719] | 402 | (* When it comes to building bits of nonterminating executions we'll need to be |
---|
| 403 | able to glue termination proofs together. *) |
---|
| 404 | |
---|
| 405 | lemma will_return_prepend : ∀ge,d1,s1,t1. |
---|
| 406 | ∀T1:will_return ge d1 s1 t1. |
---|
| 407 | ∀d2,s2,t2. |
---|
| 408 | will_return ge d2 s2 t2 → |
---|
| 409 | will_return_end … T1 = ❬s2, t2❭ → |
---|
| 410 | will_return ge (d1 + S d2) s1 t1. |
---|
| 411 | #ge #d1 #s1 #tr1 #T1 elim T1 |
---|
| 412 | [ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E |
---|
| 413 | %1 // @(IH … T2) @E |
---|
| 414 | | #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E |
---|
| 415 | | #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E |
---|
| 416 | | #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 // |
---|
| 417 | ] qed. |
---|
| 418 | |
---|
| 419 | discriminator nat. |
---|
| 420 | |
---|
| 421 | lemma will_return_remove_call : ∀ge,d1,s1,t1. |
---|
| 422 | ∀T1:will_return ge d1 s1 t1. |
---|
| 423 | ∀d2. |
---|
| 424 | will_return ge (d1 + S d2) s1 t1 → |
---|
| 425 | ∀s2,t2. |
---|
| 426 | will_return_end … T1 = ❬s2, t2❭ → |
---|
| 427 | will_return ge d2 s2 t2. |
---|
| 428 | (* The key part of the proof is to show that the two termination proofs follow |
---|
| 429 | the same pattern. *) |
---|
| 430 | #ge #d1x #s1x #t1x #T1 elim T1 |
---|
| 431 | [ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH |
---|
| 432 | [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct // |
---|
| 433 | | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct |
---|
| 434 | >H21 in CL; * #E destruct |
---|
| 435 | | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct |
---|
| 436 | >H35 in CL; * #E destruct |
---|
| 437 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct |
---|
| 438 | >H48 in CL; * #E destruct |
---|
| 439 | ] |
---|
| 440 | | @E |
---|
| 441 | ] |
---|
| 442 | | #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH |
---|
| 443 | [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct |
---|
| 444 | >CL in H7; * #E destruct |
---|
| 445 | | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct // |
---|
| 446 | | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct |
---|
| 447 | >H35 in CL; #E destruct |
---|
| 448 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct |
---|
| 449 | >H48 in CL; #E destruct |
---|
| 450 | ] |
---|
| 451 | | @E |
---|
| 452 | ] |
---|
| 453 | | #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH |
---|
| 454 | [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct |
---|
| 455 | >CL in H7; * #E destruct |
---|
| 456 | | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct |
---|
| 457 | >H21 in CL; #E destruct |
---|
| 458 | | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 |
---|
| 459 | whd in H38:(??%??); destruct // |
---|
| 460 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 |
---|
| 461 | whd in H49:(??%??); @⊥ destruct |
---|
| 462 | ] |
---|
| 463 | | @E |
---|
| 464 | ] |
---|
| 465 | | #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct |
---|
| 466 | inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct |
---|
| 467 | >CL in H7; * #E destruct |
---|
| 468 | | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct |
---|
| 469 | >H21 in CL; #E destruct |
---|
| 470 | | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 |
---|
| 471 | whd in H38:(??%??); destruct // |
---|
| 472 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 |
---|
| 473 | whd in H49:(??%??); @⊥ destruct |
---|
| 474 | ] |
---|
| 475 | ] qed. |
---|
| 476 | |
---|
[1764] | 477 | lemma will_return_not_wrong : ∀ge,d,s,t,s',t'. |
---|
| 478 | ∀T:will_return ge d s t. |
---|
| 479 | not_wrong io_out io_in ge s t → |
---|
| 480 | will_return_end … T = ❬s', t'❭ → |
---|
| 481 | not_wrong io_out io_in ge s' t'. |
---|
| 482 | #ge #d #s #t #s' #t' #T elim T |
---|
| 483 | [ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH |
---|
| 484 | [ inversion NW |
---|
| 485 | [ #H1 #H2 #H3 #H4 #H5 destruct |
---|
| 486 | | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // |
---|
| 487 | ] |
---|
| 488 | | @E |
---|
| 489 | ] |
---|
| 490 | | #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH |
---|
| 491 | [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ] |
---|
| 492 | | @E |
---|
| 493 | ] |
---|
| 494 | | #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH |
---|
| 495 | [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ] |
---|
| 496 | | @E |
---|
| 497 | ] |
---|
| 498 | | #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct |
---|
| 499 | inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ] |
---|
| 500 | ] qed. |
---|
| 501 | |
---|
[1806] | 502 | |
---|
| 503 | lemma will_return_lower : ∀ge,d,s,t. |
---|
| 504 | will_return ge d s t → |
---|
| 505 | ∀d'. d' ≤ d → |
---|
| 506 | will_return ge d' s t. |
---|
| 507 | #ge #d0 #s0 #t0 #TM elim TM |
---|
| 508 | [ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/ |
---|
| 509 | | #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/ |
---|
| 510 | | #s #tr #s' #d #EX #tr #CL #TM1 #IH * |
---|
| 511 | [ #LE @wr_base // |
---|
| 512 | | #d' #LE %3 // @IH /2/ |
---|
| 513 | ] |
---|
| 514 | | #s #tr #s' #EX #tr #CL * |
---|
| 515 | [ #_ @wr_base // |
---|
| 516 | | #d' #LE @⊥ /2/ |
---|
| 517 | ] |
---|
| 518 | ] qed. |
---|
| 519 | |
---|
[1565] | 520 | (* We require that labels appear after branch instructions and at the start of |
---|
[1574] | 521 | functions. The first is required for preciseness, the latter for soundness. |
---|
| 522 | We will make a separate requirement for there to be a finite number of steps |
---|
| 523 | between labels to catch loops for soundness (is this sufficient?). *) |
---|
[1565] | 524 | |
---|
| 525 | definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ |
---|
| 526 | λf,s. match s return λs. labels_present ? s → Prop with |
---|
| 527 | [ St_cond _ l1 l2 ⇒ λH. |
---|
[1586] | 528 | is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧ |
---|
| 529 | is_cost_label (lookup_present … (f_graph f) l2 ?) = true |
---|
[1565] | 530 | | St_jumptable _ ls ⇒ λH. |
---|
[1586] | 531 | (* I did have a dependent version of All here, but it's a pain. *) |
---|
| 532 | All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls |
---|
[1565] | 533 | | _ ⇒ λ_. True |
---|
| 534 | ]. whd in H; |
---|
| 535 | [ @(proj1 … H) |
---|
| 536 | | @(proj2 … H) |
---|
| 537 | ] qed. |
---|
| 538 | |
---|
| 539 | definition well_cost_labelled_fn : internal_function → Prop ≝ |
---|
[1586] | 540 | λf. (∀l. ∀H:present … (f_graph f) l. |
---|
| 541 | well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧ |
---|
| 542 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true. |
---|
| 543 | [ @lookup_lookup_present | cases (f_entry f) // ] qed. |
---|
[1565] | 544 | |
---|
| 545 | (* We need to ensure that any code we come across is well-cost-labelled. We may |
---|
| 546 | get function code from either the global environment or the state. *) |
---|
| 547 | |
---|
| 548 | definition well_cost_labelled_ge : genv → Prop ≝ |
---|
[1583] | 549 | λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. |
---|
[1565] | 550 | |
---|
| 551 | definition well_cost_labelled_state : state → Prop ≝ |
---|
| 552 | λs. match s with |
---|
| 553 | [ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
| 554 | | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧ |
---|
| 555 | All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
| 556 | | Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
[1713] | 557 | | Finalstate _ ⇒ True |
---|
[1565] | 558 | ]. |
---|
| 559 | |
---|
[1583] | 560 | lemma well_cost_labelled_state_step : ∀ge,s,tr,s'. |
---|
| 561 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 562 | well_cost_labelled_ge ge → |
---|
| 563 | well_cost_labelled_state s → |
---|
| 564 | well_cost_labelled_state s'. |
---|
[2025] | 565 | #ge #s #tr' #s' #EV cases (eval_preserves … EV) |
---|
[1583] | 566 | [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // |
---|
| 567 | | #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/ |
---|
[1681] | 568 | (* |
---|
[1583] | 569 | | #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ |
---|
[1681] | 570 | *) |
---|
[1583] | 571 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ |
---|
| 572 | | #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 |
---|
| 573 | | #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // |
---|
[1713] | 574 | | // |
---|
[1583] | 575 | ] qed. |
---|
| 576 | |
---|
[1586] | 577 | lemma rtlabs_jump_inv : ∀s. |
---|
| 578 | RTLabs_classify s = cl_jump → |
---|
| 579 | ∃f,fs,m. s = State f fs m ∧ |
---|
| 580 | let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in |
---|
| 581 | (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls). |
---|
| 582 | * |
---|
| 583 | [ #f #fs #m #E |
---|
| 584 | %{f} %{fs} %{m} % |
---|
| 585 | [ @refl |
---|
| 586 | | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; |
---|
[1877] | 587 | try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct) |
---|
[1586] | 588 | [ %1 %{A} %{B} %{C} @refl |
---|
| 589 | | %2 %{A} %{B} @refl |
---|
| 590 | ] |
---|
| 591 | ] |
---|
| 592 | | normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct |
---|
| 593 | | normalize #H8 #H9 #H10 #H11 #H12 destruct |
---|
[1713] | 594 | | #r #E normalize in E; destruct |
---|
[1586] | 595 | ] qed. |
---|
| 596 | |
---|
| 597 | lemma well_cost_labelled_jump : ∀ge,s,tr,s'. |
---|
| 598 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 599 | well_cost_labelled_state s → |
---|
| 600 | RTLabs_classify s = cl_jump → |
---|
| 601 | RTLabs_cost s' = true. |
---|
| 602 | #ge #s #tr #s' #EV #H #CL |
---|
| 603 | cases (rtlabs_jump_inv s CL) |
---|
| 604 | #fr * #fs * #m * #Es * |
---|
| 605 | [ * #r * #l1 * #l2 #Estmt |
---|
| 606 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
| 607 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
| 608 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
| 609 | (* replace with lemma on successors? *) |
---|
[1960] | 610 | @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct |
---|
[1586] | 611 | lapply (Hbody (next fr) (next_ok fr)) |
---|
| 612 | generalize in ⊢ (???% → ?); |
---|
| 613 | >Estmt #LP' |
---|
| 614 | whd in ⊢ (% → ?); |
---|
| 615 | * #H1 #H2 [ @H1 | @H2 ] |
---|
| 616 | | * #r * #ls #Estmt |
---|
| 617 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
| 618 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
| 619 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
| 620 | (* replace with lemma on successors? *) |
---|
[1960] | 621 | @bind_res_value #a cases a [ | #sz #i | #f | #r | #ptr ] #Ea whd in ⊢ (??%? → ?); |
---|
[1586] | 622 | [ 2: (* later *) |
---|
| 623 | | *: #E destruct |
---|
| 624 | ] |
---|
| 625 | lapply (Hbody (next fr) (next_ok fr)) |
---|
| 626 | generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP |
---|
| 627 | generalize in ⊢ (??(?%)? → ?); |
---|
| 628 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
| 629 | [ #E1 #E2 whd in E2:(??%?); destruct |
---|
| 630 | | #l' #E1 #E2 whd in E2:(??%?); destruct |
---|
| 631 | cases (All_nth ???? CP ? E1) |
---|
| 632 | #H1 #H2 @H2 |
---|
| 633 | ] |
---|
| 634 | ] qed. |
---|
| 635 | |
---|
[1595] | 636 | lemma rtlabs_call_inv : ∀s. |
---|
| 637 | RTLabs_classify s = cl_call → |
---|
| 638 | ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m. |
---|
| 639 | * [ #f #fs #m whd in ⊢ (??%? → ?); |
---|
| 640 | cases (lookup_present … (next f) (next_ok f)) normalize |
---|
[1877] | 641 | try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct |
---|
[1595] | 642 | | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl |
---|
| 643 | | normalize #H411 #H412 #H413 #H414 #H415 destruct |
---|
[1713] | 644 | | normalize #H1 #H2 destruct |
---|
[1595] | 645 | ] qed. |
---|
[1586] | 646 | |
---|
[1595] | 647 | lemma well_cost_labelled_call : ∀ge,s,tr,s'. |
---|
| 648 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 649 | well_cost_labelled_state s → |
---|
| 650 | RTLabs_classify s = cl_call → |
---|
| 651 | RTLabs_cost s' = true. |
---|
| 652 | #ge #s #tr #s' #EV #WCL #CL |
---|
| 653 | cases (rtlabs_call_inv s CL) |
---|
| 654 | #fd * #args * #dst * #stk * #m #E >E in EV WCL; |
---|
| 655 | whd in ⊢ (??%? → % → ?); |
---|
| 656 | cases fd |
---|
| 657 | [ #fn whd in ⊢ (??%? → % → ?); |
---|
[1960] | 658 | @bind_res_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any) |
---|
[1595] | 659 | #m' #b whd in ⊢ (??%? → ?); #E' destruct |
---|
| 660 | * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 |
---|
| 661 | @WCL2 |
---|
| 662 | | #fn whd in ⊢ (??%? → % → ?); |
---|
| 663 | @bindIO_value #evargs #Eargs |
---|
[1656] | 664 | whd in ⊢ (??%? → ?); |
---|
| 665 | #E' destruct |
---|
[1595] | 666 | ] qed. |
---|
| 667 | |
---|
[1681] | 668 | |
---|
| 669 | (* The preservation of (most of) the stack is useful to show as_after_return. |
---|
[1682] | 670 | We do this by showing that during the execution of a function the lower stack |
---|
| 671 | frames never change, and that after returning from the function we preserve |
---|
| 672 | the identity of the next instruction to execute. |
---|
| 673 | *) |
---|
| 674 | |
---|
| 675 | inductive stack_of_state : list frame → state → Prop ≝ |
---|
| 676 | | sos_State : ∀f,fs,m. stack_of_state fs (State f fs m) |
---|
| 677 | | sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m) |
---|
| 678 | | sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m) |
---|
| 679 | . |
---|
| 680 | |
---|
[1681] | 681 | inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝ |
---|
[1682] | 682 | | sp_normal : ∀fs,s1,s2. |
---|
| 683 | stack_of_state fs s1 → |
---|
| 684 | stack_of_state fs s2 → |
---|
| 685 | stack_preserved doesnt_end_with_ret s1 s2 |
---|
| 686 | | sp_finished : ∀s1,f,f',fs,m. |
---|
| 687 | next f = next f' → |
---|
[1736] | 688 | frame_rel f f' → |
---|
[1682] | 689 | stack_of_state (f::fs) s1 → |
---|
[1713] | 690 | stack_preserved ends_with_ret s1 (State f' fs m) |
---|
[1736] | 691 | | sp_stop : ∀s1,r. |
---|
| 692 | stack_of_state [ ] s1 → |
---|
| 693 | stack_preserved ends_with_ret s1 (Finalstate r) |
---|
| 694 | | sp_top : ∀fd,args,dst,m,r. |
---|
| 695 | stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r) |
---|
[1713] | 696 | . |
---|
[1681] | 697 | |
---|
[1682] | 698 | discriminator list. |
---|
[1681] | 699 | |
---|
[1682] | 700 | lemma stack_of_state_eq : ∀fs,fs',s. |
---|
| 701 | stack_of_state fs s → |
---|
| 702 | stack_of_state fs' s → |
---|
| 703 | fs = fs'. |
---|
| 704 | #fs0 #fs0' #s0 * |
---|
| 705 | [ #f #fs #m #H inversion H |
---|
[1713] | 706 | #a #b #c #d try #e try #g try #h try #i try #j destruct @refl |
---|
[1682] | 707 | | #fd #args #dst #f #fs #m #H inversion H |
---|
[1713] | 708 | #a #b #c #d try #e try #g try #h try #i try #j destruct @refl |
---|
[1682] | 709 | | #rtv #dst #fs #m #H inversion H |
---|
[1713] | 710 | #a #b #c #d try #e try #g try #h try #i try #j destruct @refl |
---|
[1682] | 711 | ] qed. |
---|
| 712 | |
---|
[1713] | 713 | lemma stack_preserved_final : ∀e,r,s. |
---|
[1736] | 714 | ¬stack_preserved e (Finalstate r) s. |
---|
| 715 | #e #r #s % #H inversion H |
---|
[1713] | 716 | [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct |
---|
| 717 | inversion SOS #a #b #c #d #e #f try #g try #h destruct |
---|
[1736] | 718 | | #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct |
---|
[1713] | 719 | inversion SOS #a #b #c #d #e #f try #g try #h destruct |
---|
[1736] | 720 | | #s' #r' #SOS #E1 #E2 #E3 #E4 destruct |
---|
| 721 | inversion SOS #a #b #c #d #e #f try #g try #h destruct |
---|
| 722 | | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct |
---|
[1713] | 723 | ] qed. |
---|
| 724 | |
---|
[1681] | 725 | lemma stack_preserved_join : ∀e,s1,s2,s3. |
---|
| 726 | stack_preserved doesnt_end_with_ret s1 s2 → |
---|
| 727 | stack_preserved e s2 s3 → |
---|
| 728 | stack_preserved e s1 s3. |
---|
| 729 | #e1 #s1 #s2 #s3 #H1 inversion H1 |
---|
[1682] | 730 | [ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct |
---|
| 731 | #H2 inversion H2 |
---|
| 732 | [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct |
---|
| 733 | @(sp_normal fs) // <(stack_of_state_eq … S1' S2) // |
---|
[1736] | 734 | | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct |
---|
[1682] | 735 | @(sp_finished … N) >(stack_of_state_eq … S1' S2) // |
---|
[1736] | 736 | | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) // |
---|
| 737 | | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct |
---|
| 738 | inversion S2 |
---|
| 739 | [ #H34 #H35 #H36 #H37 #H38 #H39 destruct |
---|
| 740 | | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct |
---|
| 741 | | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct |
---|
| 742 | ] |
---|
[1681] | 743 | ] |
---|
[1682] | 744 | | #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct |
---|
[1713] | 745 | | #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H |
---|
[1736] | 746 | cases (stack_preserved_final … H) #r #E destruct |
---|
| 747 | | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥ |
---|
| 748 | @(absurd … F) // |
---|
[1681] | 749 | ] qed. |
---|
| 750 | |
---|
[1682] | 751 | lemma stack_preserved_return : ∀ge,s1,s2,tr. |
---|
[1681] | 752 | RTLabs_classify s1 = cl_return → |
---|
| 753 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
| 754 | stack_preserved ends_with_ret s1 s2. |
---|
| 755 | #ge * |
---|
| 756 | [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?); |
---|
| 757 | cases (lookup_present ??? (next f) (next_ok f)) in E; |
---|
[1877] | 758 | normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct |
---|
[1681] | 759 | | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct |
---|
| 760 | | #res #dst * |
---|
[1736] | 761 | [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; |
---|
| 762 | [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ] |
---|
[1960] | 763 | | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV |
---|
[1682] | 764 | whd in EV:(??%?); destruct @(sp_finished ? f) // |
---|
[1736] | 765 | cases f // |
---|
[1681] | 766 | ] |
---|
[1713] | 767 | | #r #s2 #tr #E normalize in E; destruct |
---|
[1681] | 768 | ] qed. |
---|
| 769 | |
---|
| 770 | lemma stack_preserved_step : ∀ge,s1,s2,tr. |
---|
| 771 | RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump → |
---|
| 772 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
| 773 | stack_preserved doesnt_end_with_ret s1 s2. |
---|
[2025] | 774 | #ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV) |
---|
[1681] | 775 | [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/ |
---|
| 776 | | #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/ |
---|
| 777 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
| 778 | normalize in CL; cases CL #E destruct |
---|
| 779 | | #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/ |
---|
| 780 | | #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL |
---|
| 781 | #E normalize in E; destruct |
---|
[1713] | 782 | | #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct |
---|
[1681] | 783 | ] qed. |
---|
| 784 | |
---|
| 785 | lemma stack_preserved_call : ∀ge,s1,s2,s3,tr. |
---|
| 786 | RTLabs_classify s1 = cl_call → |
---|
| 787 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
| 788 | stack_preserved ends_with_ret s2 s3 → |
---|
| 789 | stack_preserved doesnt_end_with_ret s1 s3. |
---|
| 790 | #ge #s1 #s2 #s3 #tr #CL #EV #SP |
---|
| 791 | cases (rtlabs_call_inv … CL) |
---|
| 792 | #fd * #args * #dst * #stk * #m #E destruct |
---|
[1682] | 793 | inversion SP |
---|
| 794 | [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct |
---|
[1736] | 795 | | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct |
---|
[2025] | 796 | inversion (eval_preserves … EV) |
---|
[1682] | 797 | [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct |
---|
| 798 | | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct |
---|
| 799 | | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct |
---|
| 800 | inversion S |
---|
| 801 | [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ |
---|
| 802 | | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct |
---|
| 803 | | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct |
---|
| 804 | ] |
---|
| 805 | | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct |
---|
| 806 | | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct |
---|
[1713] | 807 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct |
---|
[1682] | 808 | ] |
---|
[1736] | 809 | | #s1 #r #S1 #E1 #E2 #E3 #_ destruct |
---|
[2025] | 810 | inversion (eval_preserves … EV) |
---|
[1736] | 811 | [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct |
---|
| 812 | | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct |
---|
| 813 | | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct |
---|
| 814 | inversion S1 |
---|
| 815 | [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ |
---|
| 816 | | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct |
---|
| 817 | | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct |
---|
| 818 | ] |
---|
| 819 | | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct |
---|
| 820 | | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct |
---|
| 821 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct |
---|
| 822 | ] |
---|
| 823 | | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct |
---|
[1682] | 824 | ] qed. |
---|
| 825 | |
---|
| 826 | lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr. |
---|
| 827 | ∀CL : RTLabs_classify s1 = cl_call. |
---|
| 828 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
| 829 | stack_preserved ends_with_ret s2 s3 → |
---|
| 830 | as_after_return (RTLabs_status ge) «s1,CL» s3. |
---|
| 831 | #ge #s1 #s2 #s3 #tr #CL #EV #S23 |
---|
| 832 | cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct |
---|
| 833 | inversion S23 |
---|
| 834 | [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct |
---|
[1736] | 835 | | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct |
---|
[2025] | 836 | inversion (eval_preserves … EV) |
---|
[1682] | 837 | [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct |
---|
| 838 | | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct |
---|
| 839 | | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct |
---|
| 840 | inversion S |
---|
[1736] | 841 | [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ] |
---|
[1682] | 842 | | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct |
---|
| 843 | | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct |
---|
| 844 | ] |
---|
| 845 | | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct |
---|
| 846 | | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct |
---|
[1713] | 847 | | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct |
---|
[1682] | 848 | ] |
---|
[1736] | 849 | | #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd |
---|
[2025] | 850 | inversion (eval_preserves … EV) |
---|
[1736] | 851 | [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct |
---|
| 852 | | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct |
---|
| 853 | | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct |
---|
| 854 | inversion S1 |
---|
| 855 | [ #H103 #H104 #H105 #H106 #H107 #H108 destruct // |
---|
| 856 | | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct |
---|
| 857 | | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct |
---|
| 858 | ] |
---|
| 859 | | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct |
---|
| 860 | | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct |
---|
| 861 | | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct |
---|
| 862 | ] |
---|
| 863 | | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct |
---|
[1682] | 864 | ] qed. |
---|
[1681] | 865 | |
---|
[1574] | 866 | (* Don't need to know that labels break loops because we have termination. *) |
---|
| 867 | |
---|
[1596] | 868 | (* A bit of mucking around with the depth to avoid proving termination after |
---|
[1638] | 869 | termination. Note that we keep a proof that our upper bound on the length |
---|
| 870 | of the termination proof is respected. *) |
---|
[1719] | 871 | record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) |
---|
| 872 | (start:state) (full:flat_trace io_out io_in ge start) |
---|
| 873 | (original_terminates: will_return ge depth start full) |
---|
| 874 | (T:state → Type[0]) (limit:nat) : Type[0] ≝ |
---|
| 875 | { |
---|
[1574] | 876 | new_state : state; |
---|
| 877 | remainder : flat_trace io_out io_in ge new_state; |
---|
| 878 | cost_labelled : well_cost_labelled_state new_state; |
---|
[1596] | 879 | new_trace : T new_state; |
---|
[1681] | 880 | stack_ok : stack_preserved ends start new_state; |
---|
[1719] | 881 | terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with |
---|
| 882 | [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭ |
---|
| 883 | | S d ⇒ ΣTM:will_return ge d new_state remainder. |
---|
| 884 | limit > will_return_length … TM ∧ |
---|
| 885 | will_return_end … original_terminates = will_return_end … TM |
---|
[1596] | 886 | ] |
---|
[1574] | 887 | }. |
---|
| 888 | |
---|
[1638] | 889 | (* The same with a flag indicating whether the function returned, as opposed to |
---|
| 890 | encountering a label. *) |
---|
[1719] | 891 | record sub_trace_result (ge:genv) (depth:nat) |
---|
| 892 | (start:state) (full:flat_trace io_out io_in ge start) |
---|
| 893 | (original_terminates: will_return ge depth start full) |
---|
| 894 | (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ |
---|
| 895 | { |
---|
[1594] | 896 | ends : trace_ends_with_ret; |
---|
[1719] | 897 | trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit |
---|
[1594] | 898 | }. |
---|
| 899 | |
---|
[1638] | 900 | (* We often return the result from a recursive call with an addition to the |
---|
| 901 | structured trace, so we define a couple of functions to help. The bound on |
---|
| 902 | the size of the termination proof might need to be relaxed, too. *) |
---|
| 903 | |
---|
[1719] | 904 | definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → |
---|
| 905 | ∀r:trace_result ge d e s1 t1 TM1 T1 l1. |
---|
| 906 | will_return_end … TM1 = will_return_end … TM2 → |
---|
[1712] | 907 | T2 (new_state … r) → |
---|
[1719] | 908 | stack_preserved e s2 (new_state … r) → |
---|
| 909 | trace_result ge d e s2 t2 TM2 T2 l2 ≝ |
---|
| 910 | λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. |
---|
| 911 | mk_trace_result ge d e s2 t2 TM2 T2 l2 |
---|
[1574] | 912 | (new_state … r) |
---|
| 913 | (remainder … r) |
---|
| 914 | (cost_labelled … r) |
---|
[1594] | 915 | trace |
---|
[1681] | 916 | SP |
---|
[1719] | 917 | ? |
---|
| 918 | (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → |
---|
[1637] | 919 | match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with |
---|
[1719] | 920 | [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*) |
---|
| 921 | . |
---|
| 922 | cases e in r ⊢ %; |
---|
| 923 | [ <TME -TME * cases d in TM1 TM2 ⊢ %; |
---|
| 924 | [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS |
---|
| 925 | | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME |
---|
| 926 | %{TMa} % // @(transitive_le … lGE) @L1 |
---|
| 927 | ] |
---|
| 928 | | <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); |
---|
| 929 | * #TMa * #L1 #TME |
---|
| 930 | %{TMa} % // @(transitive_le … lGE) @L1 |
---|
| 931 | ] qed. |
---|
[1574] | 932 | |
---|
[1719] | 933 | definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → |
---|
| 934 | ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1. |
---|
| 935 | will_return_end … TM1 = will_return_end … TM2 → |
---|
[1712] | 936 | T2 (ends … r) (new_state … r) → |
---|
| 937 | stack_preserved (ends … r) s2 (new_state … r) → |
---|
[1719] | 938 | sub_trace_result ge d s2 t2 TM2 T2 l2 ≝ |
---|
| 939 | λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. |
---|
| 940 | mk_sub_trace_result ge d s2 t2 TM2 T2 l2 |
---|
[1637] | 941 | (ends … r) |
---|
[1719] | 942 | (replace_trace … lGE … r TME trace SP). |
---|
[1637] | 943 | |
---|
[1638] | 944 | (* Small syntax hack to avoid ambiguous input problems. *) |
---|
[1637] | 945 | definition myge : nat → nat → Prop ≝ ge. |
---|
| 946 | |
---|
[1596] | 947 | let rec make_label_return ge depth s |
---|
[1565] | 948 | (trace: flat_trace io_out io_in ge s) |
---|
| 949 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
[1574] | 950 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
[1583] | 951 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
[1596] | 952 | (TERMINATES: will_return ge depth s trace) |
---|
[1637] | 953 | (TIME: nat) |
---|
| 954 | (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) |
---|
[1719] | 955 | on TIME : trace_result ge depth ends_with_ret s trace TERMINATES |
---|
[1638] | 956 | (trace_label_return (RTLabs_status ge) s) |
---|
| 957 | (will_return_length … TERMINATES) ≝ |
---|
| 958 | |
---|
[1637] | 959 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
| 960 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
| 961 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
[1638] | 962 | |
---|
| 963 | let r ≝ make_label_label ge depth s |
---|
| 964 | trace |
---|
| 965 | ENV_COSTLABELLED |
---|
| 966 | STATE_COSTLABELLED |
---|
| 967 | STATEMENT_COSTLABEL |
---|
| 968 | TERMINATES |
---|
| 969 | TIME ? in |
---|
[1719] | 970 | match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? → |
---|
| 971 | trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with |
---|
[1596] | 972 | [ ends_with_ret ⇒ λr. |
---|
[1712] | 973 | replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r) |
---|
[1596] | 974 | | doesnt_end_with_ret ⇒ λr. |
---|
| 975 | let r' ≝ make_label_return ge depth (new_state … r) |
---|
[1638] | 976 | (remainder … r) |
---|
| 977 | ENV_COSTLABELLED |
---|
| 978 | (cost_labelled … r) ? |
---|
| 979 | (pi1 … (terminates … r)) TIME ? in |
---|
[1712] | 980 | replace_trace … r' ? |
---|
[1638] | 981 | (tlr_step (RTLabs_status ge) s (new_state … r) |
---|
[1681] | 982 | (new_state … r') (new_trace … r) (new_trace … r')) ? |
---|
[1596] | 983 | ] (trace_res … r) |
---|
[1638] | 984 | |
---|
[1637] | 985 | ] TERMINATES_IN_TIME |
---|
[1574] | 986 | |
---|
[1638] | 987 | |
---|
[1596] | 988 | and make_label_label ge depth s |
---|
[1574] | 989 | (trace: flat_trace io_out io_in ge s) |
---|
| 990 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 991 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
[1583] | 992 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
[1596] | 993 | (TERMINATES: will_return ge depth s trace) |
---|
[1637] | 994 | (TIME: nat) |
---|
| 995 | (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) |
---|
[1719] | 996 | on TIME : sub_trace_result ge depth s trace TERMINATES |
---|
[1638] | 997 | (λends. trace_label_label (RTLabs_status ge) ends s) |
---|
| 998 | (will_return_length … TERMINATES) ≝ |
---|
| 999 | |
---|
[1637] | 1000 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
| 1001 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
| 1002 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
[1638] | 1003 | |
---|
[1637] | 1004 | let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in |
---|
[1712] | 1005 | replace_sub_trace … r ? |
---|
[1960] | 1006 | (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r) |
---|
[1638] | 1007 | |
---|
[1637] | 1008 | ] TERMINATES_IN_TIME |
---|
[1574] | 1009 | |
---|
[1638] | 1010 | |
---|
[1596] | 1011 | and make_any_label ge depth s |
---|
[1574] | 1012 | (trace: flat_trace io_out io_in ge s) |
---|
| 1013 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 1014 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
[1596] | 1015 | (TERMINATES: will_return ge depth s trace) |
---|
[1637] | 1016 | (TIME: nat) |
---|
| 1017 | (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) |
---|
[1719] | 1018 | on TIME : sub_trace_result ge depth s trace TERMINATES |
---|
[1638] | 1019 | (λends. trace_any_label (RTLabs_status ge) ends s) |
---|
| 1020 | (will_return_length … TERMINATES) ≝ |
---|
[1637] | 1021 | |
---|
| 1022 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
| 1023 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
| 1024 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
[1638] | 1025 | |
---|
[1719] | 1026 | match trace return λs,trace. well_cost_labelled_state s → |
---|
| 1027 | ∀TM:will_return ??? trace. |
---|
| 1028 | myge ? (times 3 (will_return_length ??? trace TM)) → |
---|
| 1029 | sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with |
---|
[1638] | 1030 | [ ft_stop st FINAL ⇒ |
---|
[1713] | 1031 | λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ |
---|
[1638] | 1032 | |
---|
[1637] | 1033 | | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. |
---|
[1719] | 1034 | match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
[1583] | 1035 | [ cl_other ⇒ λCL. |
---|
[1719] | 1036 | match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
[1638] | 1037 | (* We're about to run into a label. *) |
---|
[1960] | 1038 | [ true ⇒ λCS. |
---|
[1719] | 1039 | mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
[1596] | 1040 | doesnt_end_with_ret |
---|
[1719] | 1041 | (mk_trace_result ge … next trace' ? |
---|
[1960] | 1042 | (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) ??) |
---|
[1638] | 1043 | (* An ordinary step, keep going. *) |
---|
[1583] | 1044 | | false ⇒ λCS. |
---|
[1638] | 1045 | let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in |
---|
[1712] | 1046 | replace_sub_trace … r ? |
---|
[1638] | 1047 | (tal_step_default (RTLabs_status ge) (ends … r) |
---|
[1681] | 1048 | start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ? |
---|
[1583] | 1049 | ] (refl ??) |
---|
[1638] | 1050 | |
---|
[1586] | 1051 | | cl_jump ⇒ λCL. |
---|
[1719] | 1052 | mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
[1596] | 1053 | doesnt_end_with_ret |
---|
[1719] | 1054 | (mk_trace_result ge … next trace' ? |
---|
[1681] | 1055 | (tal_base_not_return (RTLabs_status ge) start next ???) ??) |
---|
[1638] | 1056 | |
---|
[1595] | 1057 | | cl_call ⇒ λCL. |
---|
[1719] | 1058 | let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in |
---|
| 1059 | match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
[1654] | 1060 | (* We're about to run into a label, use base case for call *) |
---|
| 1061 | [ true ⇒ λCS. |
---|
[1719] | 1062 | mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
[1654] | 1063 | doesnt_end_with_ret |
---|
[1719] | 1064 | (mk_trace_result ge … |
---|
[1654] | 1065 | (tal_base_call (RTLabs_status ge) start next (new_state … r) |
---|
[1960] | 1066 | ? CL ? (new_trace … r) (RTLabs_costed … CS)) ??) |
---|
[1654] | 1067 | (* otherwise use step case *) |
---|
| 1068 | | false ⇒ λCS. |
---|
| 1069 | let r' ≝ make_any_label ge depth |
---|
| 1070 | (new_state … r) (remainder … r) ENV_COSTLABELLED ? |
---|
| 1071 | (pi1 … (terminates … r)) TIME ? in |
---|
[1712] | 1072 | replace_sub_trace … r' ? |
---|
[1654] | 1073 | (tal_step_call (RTLabs_status ge) (ends … r') |
---|
| 1074 | start next (new_state … r) (new_state … r') ? CL ? |
---|
[1681] | 1075 | (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? |
---|
[1654] | 1076 | ] (refl ??) |
---|
[1638] | 1077 | |
---|
[1594] | 1078 | | cl_return ⇒ λCL. |
---|
[1719] | 1079 | mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
[1596] | 1080 | ends_with_ret |
---|
[1719] | 1081 | (mk_trace_result ge … |
---|
[1596] | 1082 | next |
---|
| 1083 | trace' |
---|
| 1084 | ? |
---|
| 1085 | (tal_base_return (RTLabs_status ge) start next ? CL) |
---|
[1681] | 1086 | ? |
---|
[1596] | 1087 | ?) |
---|
[1583] | 1088 | ] (refl ? (RTLabs_classify start)) |
---|
[1638] | 1089 | |
---|
[1880] | 1090 | | ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ |
---|
[1638] | 1091 | |
---|
[1637] | 1092 | ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME |
---|
| 1093 | ] TERMINATES_IN_TIME. |
---|
[1574] | 1094 | |
---|
[1637] | 1095 | [ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] |
---|
| 1096 | | // |
---|
[1712] | 1097 | | // |
---|
[1719] | 1098 | | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT) |
---|
| 1099 | | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ // |
---|
[1681] | 1100 | | @(stack_preserved_join … (stack_ok … r)) // |
---|
[1960] | 1101 | | @(costed_RTLabs ge) @(trace_label_label_label … (new_trace … r)) |
---|
[1719] | 1102 | | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_ |
---|
[1637] | 1103 | @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) |
---|
| 1104 | @(transitive_le … (3*(will_return_length … TERMINATES))) |
---|
| 1105 | [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times |
---|
[1681] | 1106 | @(monotonic_le_times_r 3 … LT) |
---|
[1637] | 1107 | | @le_S @le_S @le_n |
---|
| 1108 | ] |
---|
| 1109 | | @le_S_S_to_le @TERMINATES_IN_TIME |
---|
| 1110 | | cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] |
---|
| 1111 | | @le_n |
---|
[1712] | 1112 | | // |
---|
[1960] | 1113 | | @RTLabs_costed // |
---|
[1637] | 1114 | | @le_S_S_to_le @TERMINATES_IN_TIME |
---|
| 1115 | | @(wrl_nonzero … TERMINATES_IN_TIME) |
---|
[1713] | 1116 | | (* We can't reach the final state because the function terminates with a |
---|
| 1117 | return *) |
---|
| 1118 | inversion TERMINATES |
---|
| 1119 | [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct |
---|
| 1120 | | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct |
---|
| 1121 | | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct |
---|
| 1122 | | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct |
---|
| 1123 | ] |
---|
[1637] | 1124 | | @(will_return_return … CL TERMINATES) |
---|
[1682] | 1125 | | /2 by stack_preserved_return/ |
---|
[1594] | 1126 | | %{tr} @EV |
---|
[1586] | 1127 | | @(well_cost_labelled_state_step … EV) // |
---|
[1596] | 1128 | | whd @(will_return_notfn … TERMINATES) %2 @CL |
---|
[1681] | 1129 | | @stack_preserved_step /2/ |
---|
[1586] | 1130 | | %{tr} @EV |
---|
[1654] | 1131 | | %1 whd @CL |
---|
[1960] | 1132 | | @RTLabs_costed @(well_cost_labelled_jump … EV) // |
---|
[1594] | 1133 | | @(well_cost_labelled_state_step … EV) // |
---|
[1719] | 1134 | | whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} % |
---|
| 1135 | [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES) |
---|
| 1136 | #TMx * #LT' #_ @LT' |
---|
| 1137 | | <EQr cases (will_return_call … CL TERMINATES) |
---|
| 1138 | #TM' * #_ #EQ' @EQ' |
---|
| 1139 | ] |
---|
[1682] | 1140 | | @(stack_preserved_call … EV (stack_ok … r)) // |
---|
[1654] | 1141 | | %{tr} @EV |
---|
[1682] | 1142 | | @RTLabs_after_call // |
---|
[1719] | 1143 | | @(cost_labelled … r) |
---|
| 1144 | | skip |
---|
| 1145 | | cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le |
---|
| 1146 | @(transitive_lt … LT) |
---|
| 1147 | cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT' |
---|
| 1148 | | cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ |
---|
| 1149 | cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' // |
---|
[1682] | 1150 | | @RTLabs_after_call // |
---|
[1595] | 1151 | | %{tr} @EV |
---|
[1682] | 1152 | | @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // |
---|
[1595] | 1153 | | @(cost_labelled … r) |
---|
[1719] | 1154 | | cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78 |
---|
[1637] | 1155 | @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) |
---|
[1719] | 1156 | cases (will_return_call … TERMINATES) in GT; |
---|
| 1157 | #X * #Y #_ #Z |
---|
[1637] | 1158 | @(transitive_le … (monotonic_lt_times_r 3 … Y)) |
---|
| 1159 | [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) // |
---|
| 1160 | | // |
---|
| 1161 | ] |
---|
[1596] | 1162 | | @(well_cost_labelled_state_step … EV) // |
---|
| 1163 | | @(well_cost_labelled_call … EV) // |
---|
[1638] | 1164 | | cases (will_return_call … TERMINATES) |
---|
[1719] | 1165 | #TM * #GT #_ @le_S_S_to_le |
---|
[1637] | 1166 | >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times |
---|
| 1167 | @(transitive_le … TERMINATES_IN_TIME) |
---|
| 1168 | @(monotonic_le_times_r 3 … GT) |
---|
[1596] | 1169 | | whd @(will_return_notfn … TERMINATES) %1 @CL |
---|
[1682] | 1170 | | @(stack_preserved_step … EV) /2/ |
---|
[1596] | 1171 | | %{tr} @EV |
---|
[1654] | 1172 | | %2 whd @CL |
---|
[1596] | 1173 | | @(well_cost_labelled_state_step … EV) // |
---|
[1719] | 1174 | | cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT) |
---|
| 1175 | | cases (will_return_notfn … TERMINATES) #TM * #_ #EQ // |
---|
[1594] | 1176 | | @CL |
---|
[1583] | 1177 | | %{tr} @EV |
---|
[1682] | 1178 | | @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/ |
---|
[1594] | 1179 | | @(well_cost_labelled_state_step … EV) // |
---|
[1638] | 1180 | | %1 @CL |
---|
[1719] | 1181 | | cases (will_return_notfn … TERMINATES) #TM * #GT #_ |
---|
[1637] | 1182 | @le_S_S_to_le |
---|
| 1183 | @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME) |
---|
| 1184 | // |
---|
[1574] | 1185 | | inversion TERMINATES |
---|
[1637] | 1186 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct |
---|
| 1187 | | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct |
---|
| 1188 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct |
---|
| 1189 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct |
---|
[1583] | 1190 | ] |
---|
[1713] | 1191 | ] qed. |
---|
[1583] | 1192 | |
---|
[1638] | 1193 | (* We can initialise TIME with a suitably large value based on the length of the |
---|
| 1194 | termination proof. *) |
---|
[1637] | 1195 | let rec make_label_return' ge depth s |
---|
| 1196 | (trace: flat_trace io_out io_in ge s) |
---|
| 1197 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 1198 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
| 1199 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
| 1200 | (TERMINATES: will_return ge depth s trace) |
---|
[1719] | 1201 | : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ |
---|
[1637] | 1202 | make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES |
---|
| 1203 | (2 + 3 * will_return_length … TERMINATES) ?. |
---|
| 1204 | @le_n |
---|
| 1205 | qed. |
---|
[1574] | 1206 | |
---|
[1713] | 1207 | (* Tail-calls would not be handled properly (which means that if we try to show the |
---|
[1617] | 1208 | full version with non-termination we'll fail because calls and returns aren't |
---|
| 1209 | balanced. |
---|
[1651] | 1210 | *) |
---|
| 1211 | |
---|
| 1212 | inductive inhabited (T:Type[0]) : Prop ≝ |
---|
| 1213 | | witness : T → inhabited T. |
---|
| 1214 | |
---|
| 1215 | (* We also require that program's traces are soundly labelled: for any state |
---|
| 1216 | in the execution, we can give a distance to a labelled state or termination. |
---|
[1617] | 1217 | |
---|
[1651] | 1218 | Note that this differs from the syntactic notions in earlier languages |
---|
| 1219 | because it is a global property. In principle, we would have a loop broken |
---|
| 1220 | only by a call to a function (which necessarily has a label) and no local |
---|
| 1221 | cost label. |
---|
| 1222 | *) |
---|
| 1223 | |
---|
| 1224 | let rec nth_state ge s |
---|
| 1225 | (trace: flat_trace io_out io_in ge s) |
---|
| 1226 | n |
---|
| 1227 | on n : option state ≝ |
---|
| 1228 | match n with |
---|
| 1229 | [ O ⇒ Some ? s |
---|
| 1230 | | S n' ⇒ |
---|
| 1231 | match trace with |
---|
| 1232 | [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n' |
---|
| 1233 | | _ ⇒ None ? |
---|
| 1234 | ] |
---|
| 1235 | ]. |
---|
| 1236 | |
---|
| 1237 | definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝ |
---|
| 1238 | λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true. |
---|
| 1239 | |
---|
| 1240 | lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'. |
---|
| 1241 | soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') → |
---|
| 1242 | soundly_labelled_trace ge s' trace'. |
---|
| 1243 | #ge #s #tr #s' #EV #trace' #H |
---|
| 1244 | #n cases (H (S n)) #m #H' %{m} @H' |
---|
| 1245 | qed. |
---|
| 1246 | |
---|
[1705] | 1247 | (* Define a notion of sound labellings of RTLabs programs. *) |
---|
[1675] | 1248 | |
---|
[1705] | 1249 | let rec successors (s : statement) : list label ≝ |
---|
| 1250 | match s with |
---|
| 1251 | [ St_skip l ⇒ [l] |
---|
| 1252 | | St_cost _ l ⇒ [l] |
---|
[1880] | 1253 | | St_const _ _ _ l ⇒ [l] |
---|
[1705] | 1254 | | St_op1 _ _ _ _ _ l ⇒ [l] |
---|
[1877] | 1255 | | St_op2 _ _ _ _ _ _ _ l ⇒ [l] |
---|
[1705] | 1256 | | St_load _ _ _ l ⇒ [l] |
---|
| 1257 | | St_store _ _ _ l ⇒ [l] |
---|
| 1258 | | St_call_id _ _ _ l ⇒ [l] |
---|
| 1259 | | St_call_ptr _ _ _ l ⇒ [l] |
---|
| 1260 | (* |
---|
| 1261 | | St_tailcall_id _ _ ⇒ [ ] |
---|
| 1262 | | St_tailcall_ptr _ _ ⇒ [ ] |
---|
| 1263 | *) |
---|
| 1264 | | St_cond _ l1 l2 ⇒ [l1; l2] |
---|
| 1265 | | St_jumptable _ ls ⇒ ls |
---|
| 1266 | | St_return ⇒ [ ] |
---|
| 1267 | ]. |
---|
[1675] | 1268 | |
---|
[1705] | 1269 | definition actual_successor : state → option label ≝ |
---|
| 1270 | λs. match s with |
---|
| 1271 | [ State f fs m ⇒ Some ? (next f) |
---|
| 1272 | | Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ] |
---|
| 1273 | | Returnstate _ _ _ _ ⇒ None ? |
---|
[1713] | 1274 | | Finalstate _ ⇒ None ? |
---|
[1705] | 1275 | ]. |
---|
| 1276 | |
---|
| 1277 | lemma nth_opt_Exists : ∀A,n,l,a. |
---|
| 1278 | nth_opt A n l = Some A a → |
---|
| 1279 | Exists A (λa'. a' = a) l. |
---|
| 1280 | #A #n elim n |
---|
| 1281 | [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ] |
---|
| 1282 | | #m #IH * |
---|
| 1283 | [ #a #E normalize in E; destruct |
---|
| 1284 | | #a #l #a' #E %2 @IH @E |
---|
| 1285 | ] |
---|
| 1286 | ] qed. |
---|
| 1287 | |
---|
| 1288 | lemma eval_successor : ∀ge,f,fs,m,tr,s'. |
---|
| 1289 | eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → |
---|
| 1290 | RTLabs_classify s' = cl_return ∨ |
---|
| 1291 | ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))). |
---|
| 1292 | #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' |
---|
| 1293 | whd in ⊢ (??%? → ?); |
---|
| 1294 | generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) |
---|
| 1295 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1296 | | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
[1960] | 1297 | | #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1298 | | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1299 | | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1300 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1301 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1302 | | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1303 | | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
| 1304 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] // |
---|
| 1305 | | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev |
---|
[1705] | 1306 | cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] |
---|
| 1307 | whd in ⊢ (??%? → ?); |
---|
| 1308 | generalize in ⊢ (??(?%)? → ?); |
---|
| 1309 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?); |
---|
| 1310 | [ #e #E normalize in E; destruct |
---|
| 1311 | | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) |
---|
| 1312 | ] |
---|
[1960] | 1313 | | #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl |
---|
[1705] | 1314 | ] qed. |
---|
| 1315 | |
---|
| 1316 | definition steps_for_statement : statement → nat ≝ |
---|
| 1317 | λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]). |
---|
| 1318 | |
---|
[1707] | 1319 | inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝ |
---|
| 1320 | | bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n |
---|
| 1321 | | bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n |
---|
| 1322 | with bound_on_steps_to_cost1 : label → nat → Prop ≝ |
---|
| 1323 | | bostc_step : ∀l,n,H. |
---|
[1705] | 1324 | let stmt ≝ lookup_present … g l H in |
---|
[1706] | 1325 | (∀l'. Exists label (λl0. l0 = l') (successors stmt) → |
---|
[1707] | 1326 | bound_on_steps_to_cost g l' n) → |
---|
| 1327 | bound_on_steps_to_cost1 g l (steps_for_statement stmt + n). |
---|
[1705] | 1328 | |
---|
[1707] | 1329 | (* |
---|
[1706] | 1330 | lemma steps_to_label_bound_inv : ∀g,l,n. |
---|
[1705] | 1331 | steps_to_label_bound g l n → |
---|
[1706] | 1332 | ∀H. let stmt ≝ lookup_present … g l H in |
---|
| 1333 | ∃n'. n = steps_for_statement stmt + n' ∧ |
---|
[1705] | 1334 | (∀l'. Exists label (λl0. l0 = l') (successors stmt) → |
---|
[1706] | 1335 | (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨ |
---|
| 1336 | steps_to_label_bound g l' n'). |
---|
| 1337 | #g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H' |
---|
| 1338 | % [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ] |
---|
| 1339 | qed. |
---|
[1707] | 1340 | *) |
---|
[1719] | 1341 | |
---|
[1707] | 1342 | (* |
---|
[1705] | 1343 | definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. |
---|
| 1344 | |
---|
| 1345 | let rec soundly_labelled_fn (fn : internal_function) : Prop ≝ |
---|
| 1346 | soundly_labelled_pc (f_graph fn) (f_entry fn). |
---|
| 1347 | |
---|
| 1348 | |
---|
[1675] | 1349 | definition soundly_labelled_frame : frame → Prop ≝ |
---|
| 1350 | λf. soundly_labelled_pc (f_graph (func f)) (next f). |
---|
| 1351 | |
---|
| 1352 | definition soundly_labelled_state : state → Prop ≝ |
---|
| 1353 | λs. match s with |
---|
| 1354 | [ State f _ _ ⇒ soundly_labelled_frame f |
---|
| 1355 | | Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] |
---|
| 1356 | | Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] |
---|
| 1357 | ]. |
---|
[1707] | 1358 | *) |
---|
| 1359 | definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝ |
---|
| 1360 | λf. bound_on_steps_to_cost (f_graph (func f)) (next f). |
---|
| 1361 | definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝ |
---|
| 1362 | λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f). |
---|
[1705] | 1363 | |
---|
[1707] | 1364 | inductive state_bound_on_steps_to_cost : state → nat → Prop ≝ |
---|
| 1365 | | sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n |
---|
| 1366 | | sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n) |
---|
| 1367 | | sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n) |
---|
[1675] | 1368 | . |
---|
| 1369 | |
---|
[1707] | 1370 | lemma state_bound_on_steps_to_cost_zero : ∀s. |
---|
| 1371 | ¬ state_bound_on_steps_to_cost s O. |
---|
[1705] | 1372 | #s % #H inversion H |
---|
[1707] | 1373 | [ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct |
---|
| 1374 | whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*) |
---|
| 1375 | #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct |
---|
[1705] | 1376 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct |
---|
| 1377 | | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct |
---|
| 1378 | ] qed. |
---|
| 1379 | |
---|
| 1380 | lemma eval_steps : ∀ge,f,fs,m,tr,s'. |
---|
| 1381 | eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → |
---|
| 1382 | steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) = |
---|
[1713] | 1383 | match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ]. |
---|
[1705] | 1384 | #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' |
---|
| 1385 | whd in ⊢ (??%? → ?); |
---|
| 1386 | generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) |
---|
| 1387 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1388 | | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl |
---|
[1960] | 1389 | | #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1390 | | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1391 | | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1392 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1393 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1394 | | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1395 | | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1396 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1397 | | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev |
---|
[1705] | 1398 | cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] |
---|
| 1399 | whd in ⊢ (??%? → ?); |
---|
| 1400 | generalize in ⊢ (??(?%)? → ?); |
---|
| 1401 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?); |
---|
| 1402 | [ #e #E normalize in E; destruct |
---|
| 1403 | | #l #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
| 1404 | ] |
---|
[1960] | 1405 | | #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl |
---|
[1705] | 1406 | ] qed. |
---|
| 1407 | |
---|
[1736] | 1408 | lemma bound_after_call : ∀ge,s,s',n. |
---|
| 1409 | state_bound_on_steps_to_cost s (S n) → |
---|
| 1410 | ∀CL:RTLabs_classify s = cl_call. |
---|
| 1411 | as_after_return (RTLabs_status ge) «s, CL» s' → |
---|
| 1412 | RTLabs_cost s' = false → |
---|
| 1413 | state_bound_on_steps_to_cost s' n. |
---|
| 1414 | #ge #s #s' #n #H inversion H |
---|
| 1415 | [ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL) |
---|
| 1416 | #fn * #args * #dst * #stk * #m' #E destruct |
---|
| 1417 | | #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct |
---|
| 1418 | whd in S; #CL cases s' |
---|
| 1419 | [ #f' #fs' #m' * #N #F #CS |
---|
| 1420 | %1 whd |
---|
| 1421 | inversion S |
---|
| 1422 | [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥ |
---|
| 1423 | change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P * |
---|
| 1424 | | #l #n #B #E1 #E2 #_ destruct <N <F @B |
---|
| 1425 | ] |
---|
| 1426 | | #fd' #args' #dst' #fs' #m' * |
---|
| 1427 | | #rv #dst' #fs' #m' * |
---|
| 1428 | | #r #E normalize in E; destruct |
---|
| 1429 | ] |
---|
| 1430 | | #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct |
---|
| 1431 | ] qed. |
---|
| 1432 | |
---|
[1707] | 1433 | lemma bound_after_step : ∀ge,s,tr,s',n. |
---|
| 1434 | state_bound_on_steps_to_cost s (S n) → |
---|
[1705] | 1435 | eval_statement ge s = Value ??? 〈tr, s'〉 → |
---|
[1706] | 1436 | RTLabs_cost s' = false → |
---|
[1705] | 1437 | (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ |
---|
[1707] | 1438 | state_bound_on_steps_to_cost s' n. |
---|
| 1439 | #ge #s #tr #s' #n #BOUND1 inversion BOUND1 |
---|
[1705] | 1440 | [ #f #fs #m #m #FS #E1 #E2 #_ destruct |
---|
| 1441 | #EVAL cases (eval_successor … EVAL) |
---|
| 1442 | [ /3/ |
---|
| 1443 | | * #l * #S1 #S2 #NC %2 |
---|
[1707] | 1444 | (* |
---|
| 1445 | cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ] |
---|
| 1446 | *) |
---|
| 1447 | @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct |
---|
[2025] | 1448 | inversion (eval_preserves … EVAL) |
---|
[1707] | 1449 | [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct |
---|
| 1450 | >(eval_steps … EVAL) in E2; #En normalize in En; |
---|
| 1451 | inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct |
---|
| 1452 | %1 inversion (IH … S2) |
---|
| 1453 | [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct |
---|
| 1454 | change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%); |
---|
| 1455 | whd in S1:(??%?); destruct >NC in CSx; * |
---|
| 1456 | | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73 |
---|
[1706] | 1457 | ] |
---|
[1707] | 1458 | | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct |
---|
| 1459 | >(eval_steps … EVAL) in E2; #En normalize in En; |
---|
| 1460 | inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct |
---|
| 1461 | %2 @IH normalize in S1; destruct @S2 |
---|
| 1462 | | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 |
---|
[1705] | 1463 | destruct |
---|
[1707] | 1464 | | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct |
---|
[1705] | 1465 | normalize in S1; destruct |
---|
[1707] | 1466 | | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct |
---|
[1713] | 1467 | | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct |
---|
[1705] | 1468 | ] |
---|
| 1469 | ] |
---|
| 1470 | | #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct |
---|
| 1471 | /3/ |
---|
| 1472 | | #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct |
---|
[2025] | 1473 | #EVAL #NC %2 inversion (eval_preserves … EVAL) |
---|
[1705] | 1474 | [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct |
---|
| 1475 | | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct |
---|
| 1476 | | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct |
---|
| 1477 | | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct |
---|
| 1478 | | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct |
---|
| 1479 | %1 whd in FS ⊢ %; |
---|
[1736] | 1480 | inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ] |
---|
| 1481 | #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE |
---|
[1705] | 1482 | 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 ] |
---|
| 1483 | inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct |
---|
[1707] | 1484 | inversion FS |
---|
| 1485 | [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct |
---|
| 1486 | change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%); |
---|
| 1487 | >NC in CSx; * |
---|
| 1488 | | #lx #nx #H #E1x #E2x #_ destruct @H |
---|
| 1489 | ] |
---|
[1713] | 1490 | | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct |
---|
[1705] | 1491 | ] |
---|
| 1492 | ] qed. |
---|
[1806] | 1493 | |
---|
| 1494 | |
---|
| 1495 | |
---|
| 1496 | |
---|
| 1497 | definition soundly_labelled_fn : internal_function → Prop ≝ |
---|
| 1498 | λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n. |
---|
| 1499 | |
---|
| 1500 | definition soundly_labelled_ge : genv → Prop ≝ |
---|
| 1501 | λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f. |
---|
| 1502 | |
---|
| 1503 | definition soundly_labelled_state : state → Prop ≝ |
---|
| 1504 | λs. match s with |
---|
| 1505 | [ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs |
---|
| 1506 | | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧ |
---|
| 1507 | All ? (λf. soundly_labelled_fn (func f)) fs |
---|
| 1508 | | Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs |
---|
| 1509 | | Finalstate _ ⇒ True |
---|
| 1510 | ]. |
---|
| 1511 | |
---|
| 1512 | lemma steps_from_sound : ∀s. |
---|
| 1513 | RTLabs_cost s = true → |
---|
| 1514 | soundly_labelled_state s → |
---|
| 1515 | ∃n. state_bound_on_steps_to_cost s n. |
---|
| 1516 | * [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ] |
---|
| 1517 | whd in ⊢ (% → ?); * #SLF #_ |
---|
| 1518 | cases (SLF (next f) (next_ok f)) #n #B1 |
---|
| 1519 | %{n} % @B1 |
---|
| 1520 | qed. |
---|
| 1521 | |
---|
| 1522 | lemma soundly_labelled_state_step : ∀ge,s,tr,s'. |
---|
| 1523 | soundly_labelled_ge ge → |
---|
| 1524 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 1525 | soundly_labelled_state s → |
---|
| 1526 | soundly_labelled_state s'. |
---|
| 1527 | #ge #s #tr #s' #ENV #EV #S |
---|
[2025] | 1528 | inversion (eval_preserves … EV) |
---|
[1806] | 1529 | [ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct |
---|
| 1530 | whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S |
---|
| 1531 | | #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct |
---|
| 1532 | whd in S ⊢ %; % |
---|
| 1533 | [ cases fd in FFP ⊢ %; // #fn #FFP @ENV // |
---|
| 1534 | | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S |
---|
| 1535 | ] |
---|
| 1536 | | #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
| 1537 | whd in S ⊢ %; @S |
---|
| 1538 | | #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
| 1539 | whd in S ⊢ %; cases S // |
---|
| 1540 | | #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct |
---|
| 1541 | whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S |
---|
| 1542 | | #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I |
---|
| 1543 | ] qed. |
---|
| 1544 | |
---|
| 1545 | lemma soundly_labelled_state_preserved : ∀s,s'. |
---|
| 1546 | stack_preserved ends_with_ret s s' → |
---|
| 1547 | soundly_labelled_state s → |
---|
| 1548 | soundly_labelled_state s'. |
---|
| 1549 | #s0 #s0' #SP inversion SP |
---|
| 1550 | [ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct |
---|
| 1551 | | #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct |
---|
| 1552 | inversion S1 |
---|
| 1553 | [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct |
---|
| 1554 | * #_ #S whd in S; |
---|
| 1555 | inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 |
---|
| 1556 | destruct @S |
---|
| 1557 | | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S |
---|
| 1558 | inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 |
---|
| 1559 | destruct @S |
---|
| 1560 | | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S |
---|
| 1561 | inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 |
---|
| 1562 | destruct @S |
---|
| 1563 | ] |
---|
| 1564 | | // |
---|
| 1565 | | // |
---|
| 1566 | ] qed. |
---|
| 1567 | |
---|
[1653] | 1568 | (* When constructing an infinite trace, we need to be able to grab the finite |
---|
| 1569 | portion of the trace for the next [trace_label_diverges] constructor. We |
---|
| 1570 | use the fact that the trace is soundly labelled to achieve this. *) |
---|
| 1571 | |
---|
[1805] | 1572 | record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ { |
---|
| 1573 | ro_well_cost_labelled: well_cost_labelled_state s; |
---|
[1806] | 1574 | ro_soundly_labelled: soundly_labelled_state s; |
---|
[1805] | 1575 | ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t)); |
---|
| 1576 | ro_not_undefined: not_wrong … t; |
---|
| 1577 | ro_not_final: RTLabs_is_final s = None ? |
---|
| 1578 | }. |
---|
| 1579 | |
---|
[1670] | 1580 | inductive finite_prefix (ge:genv) : state → Prop ≝ |
---|
[1653] | 1581 | | fp_tal : ∀s,s'. |
---|
| 1582 | trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → |
---|
[1805] | 1583 | ∀t:flat_trace io_out io_in ge s'. |
---|
| 1584 | remainder_ok ge s' t → |
---|
[1653] | 1585 | finite_prefix ge s |
---|
[1806] | 1586 | | fp_tac : ∀s1,s2,s3,tr. |
---|
| 1587 | trace_any_call (RTLabs_status ge) s1 s2 → |
---|
| 1588 | well_cost_labelled_state s2 → |
---|
| 1589 | eval_statement ge s2 = Value ??? 〈tr,s3〉 → |
---|
| 1590 | ∀t:flat_trace io_out io_in ge s3. |
---|
| 1591 | remainder_ok ge s3 t → |
---|
| 1592 | finite_prefix ge s1 |
---|
[1653] | 1593 | . |
---|
| 1594 | |
---|
| 1595 | definition fp_add_default : ∀ge,s,s'. |
---|
| 1596 | RTLabs_classify s = cl_other → |
---|
| 1597 | finite_prefix ge s' → |
---|
| 1598 | (∃t. eval_statement ge s = Value ??? 〈t,s'〉) → |
---|
| 1599 | RTLabs_cost s' = false → |
---|
| 1600 | finite_prefix ge s ≝ |
---|
| 1601 | λge,s,s',OTHER,fp. |
---|
| 1602 | match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with |
---|
[1805] | 1603 | [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf |
---|
[1670] | 1604 | (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) |
---|
[1805] | 1605 | rem rok |
---|
[1806] | 1606 | | fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr |
---|
| 1607 | (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) |
---|
| 1608 | WCL2 EV rem rok |
---|
[1653] | 1609 | ]. |
---|
[1670] | 1610 | |
---|
[1806] | 1611 | definition fp_add_terminating_call : ∀ge,s,s1,s''. |
---|
[1653] | 1612 | (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → |
---|
| 1613 | ∀CALL:RTLabs_classify s = cl_call. |
---|
[1806] | 1614 | finite_prefix ge s'' → |
---|
| 1615 | trace_label_return (RTLabs_status ge) s1 s'' → |
---|
| 1616 | as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' → |
---|
| 1617 | RTLabs_cost s'' = false → |
---|
[1653] | 1618 | finite_prefix ge s ≝ |
---|
[1806] | 1619 | λge,s,s1,s'',EVAL,CALL,fp. |
---|
| 1620 | match fp return λs''.λ_. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with |
---|
| 1621 | [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf |
---|
| 1622 | (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) |
---|
[1805] | 1623 | rem rok |
---|
[1806] | 1624 | | fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr |
---|
| 1625 | (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) |
---|
| 1626 | WCL2 EV rem rok |
---|
[1653] | 1627 | ]. |
---|
[1670] | 1628 | |
---|
[1765] | 1629 | lemma not_return_to_not_final : ∀ge,s,tr,s'. |
---|
| 1630 | eval_statement ge s = Value ??? 〈tr, s'〉 → |
---|
| 1631 | RTLabs_classify s ≠ cl_return → |
---|
| 1632 | RTLabs_is_final s' = None ?. |
---|
| 1633 | #ge #s #tr #s' #EV |
---|
[2025] | 1634 | inversion (eval_preserves … EV) // |
---|
[1765] | 1635 | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL |
---|
| 1636 | @⊥ @(absurd ?? CL) @refl |
---|
| 1637 | qed. |
---|
| 1638 | |
---|
[1670] | 1639 | definition termination_oracle ≝ ∀ge,depth,s,trace. |
---|
[1671] | 1640 | inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). |
---|
[1670] | 1641 | |
---|
| 1642 | let rec finite_segment ge s n trace |
---|
| 1643 | (ORACLE: termination_oracle) |
---|
[1805] | 1644 | (TRACE_OK: remainder_ok ge s trace) |
---|
[1670] | 1645 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
[1806] | 1646 | (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) |
---|
[1707] | 1647 | (LABEL_LIMIT: state_bound_on_steps_to_cost s n) |
---|
[1671] | 1648 | on n : finite_prefix ge s ≝ |
---|
[1707] | 1649 | match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with |
---|
[1705] | 1650 | [ O ⇒ λLABEL_LIMIT. ⊥ |
---|
| 1651 | | S n' ⇒ |
---|
[1805] | 1652 | match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with |
---|
| 1653 | [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ |
---|
| 1654 | | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT. |
---|
[1670] | 1655 | match RTLabs_classify start return λx. RTLabs_classify start = x → ? with |
---|
| 1656 | [ cl_other ⇒ λCL. |
---|
[1805] | 1657 | let TRACE_OK' ≝ ? in |
---|
[1670] | 1658 | match RTLabs_cost next return λx. RTLabs_cost next = x → ? with |
---|
| 1659 | [ true ⇒ λCS. |
---|
[1960] | 1660 | fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) trace' TRACE_OK' |
---|
[1670] | 1661 | | false ⇒ λCS. |
---|
[1812] | 1662 | let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in |
---|
[1670] | 1663 | fp_add_default ge ?? CL fs ? CS |
---|
| 1664 | ] (refl ??) |
---|
| 1665 | | cl_jump ⇒ λCL. |
---|
[1805] | 1666 | fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ? |
---|
[1707] | 1667 | | cl_call ⇒ λCL. |
---|
[1671] | 1668 | match ORACLE ge O next trace' return λ_. finite_prefix ge start with |
---|
| 1669 | [ or_introl TERMINATES ⇒ |
---|
| 1670 | match TERMINATES with [ witness TERMINATES ⇒ |
---|
| 1671 | let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in |
---|
[1805] | 1672 | let TRACE_OK' ≝ ? in |
---|
[1671] | 1673 | match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with |
---|
[1960] | 1674 | [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed … CS)) (remainder … tlr) TRACE_OK' |
---|
[1707] | 1675 | | false ⇒ λCS. |
---|
[1812] | 1676 | let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in |
---|
[1707] | 1677 | fp_add_terminating_call … fs (new_trace … tlr) ? CS |
---|
[1671] | 1678 | ] (refl ??) |
---|
| 1679 | ] |
---|
| 1680 | | or_intror NO_TERMINATION ⇒ |
---|
[1806] | 1681 | fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ? |
---|
[1707] | 1682 | ] |
---|
[1670] | 1683 | | cl_return ⇒ λCL. ⊥ |
---|
| 1684 | ] (refl ??) |
---|
[1880] | 1685 | | ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ |
---|
[1805] | 1686 | ] TRACE_OK |
---|
[1705] | 1687 | ] LABEL_LIMIT. |
---|
[1707] | 1688 | [ cases (state_bound_on_steps_to_cost_zero s) /2/ |
---|
[1805] | 1689 | | @(absurd … (ro_not_final … TRACE_OK) FINAL) |
---|
| 1690 | | @(absurd ?? (ro_no_termination … TRACE_OK)) |
---|
[1670] | 1691 | %{0} % @wr_base // |
---|
[1960] | 1692 | | @RTLabs_costed @(well_cost_labelled_jump … EV) /2/ |
---|
[1805] | 1693 | | 5,6,8,9,10,11: /3/ |
---|
| 1694 | | % [ @(well_cost_labelled_state_step … EV) /2/ |
---|
[1806] | 1695 | | @(soundly_labelled_state_step … EV) /2/ |
---|
[1805] | 1696 | | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/ |
---|
| 1697 | | @(still_not_wrong … EV) /2/ |
---|
| 1698 | | @(not_return_to_not_final … EV) >CL % #E destruct |
---|
| 1699 | ] |
---|
[1707] | 1700 | | /2/ |
---|
[1736] | 1701 | | @(bound_after_call ge … LABEL_LIMIT CL ? CS) |
---|
| 1702 | @(RTLabs_after_call … CL EV) @(stack_ok … tlr) |
---|
[1805] | 1703 | | % [ /2/ |
---|
[1806] | 1704 | | @(soundly_labelled_state_preserved … (stack_ok … tlr)) |
---|
| 1705 | @(soundly_labelled_state_step … EV) /2/ |
---|
[1805] | 1706 | | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % |
---|
| 1707 | @wr_call // |
---|
| 1708 | @(will_return_prepend … TERMINATES … TM1) |
---|
| 1709 | cases (terminates … tlr) // |
---|
| 1710 | | @(will_return_not_wrong … TERMINATES) |
---|
| 1711 | [ @(still_not_wrong … EV) /2/ |
---|
| 1712 | | cases (terminates … tlr) // |
---|
| 1713 | ] |
---|
| 1714 | | (* By stack preservation we cannot be in the final state *) |
---|
| 1715 | inversion (stack_ok … tlr) |
---|
| 1716 | [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct |
---|
| 1717 | | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl |
---|
| 1718 | | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct |
---|
| 1719 | cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct |
---|
[2025] | 1720 | inversion (eval_preserves … EV) |
---|
[1805] | 1721 | [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ] |
---|
| 1722 | #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct |
---|
| 1723 | inversion S |
---|
| 1724 | [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ] |
---|
| 1725 | (* state_bound_on_steps_to_cost needs to know about the current stack frame, |
---|
| 1726 | so we can use it as a witness that at least one frame exists *) |
---|
| 1727 | inversion LABEL_LIMIT |
---|
| 1728 | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct |
---|
| 1729 | | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct |
---|
| 1730 | ] |
---|
| 1731 | ] |
---|
| 1732 | | @(well_cost_labelled_state_step … EV) /2/ |
---|
| 1733 | | @(well_cost_labelled_call … EV) /2/ |
---|
[1806] | 1734 | | /2/ |
---|
| 1735 | | % [ @(well_cost_labelled_state_step … EV) /2/ |
---|
| 1736 | | @(soundly_labelled_state_step … EV) /2/ |
---|
| 1737 | | @(not_to_not … NO_TERMINATION) * #depth * #TM % |
---|
| 1738 | @(will_return_lower … TM) // |
---|
| 1739 | | @(still_not_wrong … EV) /2/ |
---|
| 1740 | | @(not_return_to_not_final … EV) >CL % #E destruct |
---|
| 1741 | ] |
---|
[1812] | 1742 | | 19,20,21: /2/ |
---|
[1707] | 1743 | | cases (bound_after_step … LABEL_LIMIT EV ?) |
---|
[1805] | 1744 | [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // | |
---|
[1707] | 1745 | inversion trace' |
---|
[1805] | 1746 | [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥ |
---|
[1765] | 1747 | @(absurd ?? FINAL) @(not_return_to_not_final … EV) |
---|
| 1748 | % >CL #E destruct |
---|
[1805] | 1749 | | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct |
---|
[1765] | 1750 | @wr_base // |
---|
[1805] | 1751 | | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct |
---|
| 1752 | inversion (ro_not_undefined … TRACE_OK) |
---|
[1707] | 1753 | [ #H137 #H138 #H139 #H140 #H141 destruct |
---|
[1880] | 1754 | | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct |
---|
[1707] | 1755 | inversion H148 |
---|
| 1756 | [ #H153 #H154 #H155 #H156 #H157 destruct |
---|
| 1757 | | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct |
---|
| 1758 | ] |
---|
| 1759 | ] |
---|
| 1760 | ] |
---|
| 1761 | ] |
---|
| 1762 | | >CL #E destruct |
---|
| 1763 | ] |
---|
| 1764 | | // |
---|
| 1765 | | // |
---|
| 1766 | ] |
---|
[1805] | 1767 | | % [ @(well_cost_labelled_state_step … EV) /2/ |
---|
[1806] | 1768 | | @(soundly_labelled_state_step … EV) /2/ |
---|
[1805] | 1769 | | @(not_to_not … (ro_no_termination … TRACE_OK)) |
---|
| 1770 | * #depth * #TERM %{depth} % @wr_step /2/ |
---|
| 1771 | | @(still_not_wrong … (ro_not_undefined … TRACE_OK)) |
---|
| 1772 | | @(not_return_to_not_final … EV) >CL % #E destruct |
---|
| 1773 | ] |
---|
| 1774 | | inversion (ro_not_undefined … TRACE_OK) |
---|
[1707] | 1775 | [ #H169 #H170 #H171 #H172 #H173 destruct |
---|
| 1776 | | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct |
---|
| 1777 | ] |
---|
[1765] | 1778 | ] qed. |
---|
[1670] | 1779 | |
---|
[1808] | 1780 | (* NB: This isn't quite what I'd like. Ideally, we'd show the existence of |
---|
| 1781 | a trace_label_diverges value, but I only know how to construct those |
---|
| 1782 | using a cofixpoint in Type[0], which means I can't use the termination |
---|
| 1783 | oracle. |
---|
[1806] | 1784 | *) |
---|
[1784] | 1785 | |
---|
[1651] | 1786 | let corec make_label_diverges ge s |
---|
| 1787 | (trace: flat_trace io_out io_in ge s) |
---|
[1784] | 1788 | (ORACLE: termination_oracle) |
---|
[1805] | 1789 | (TRACE_OK: remainder_ok ge s trace) |
---|
[1651] | 1790 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
[1784] | 1791 | (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) |
---|
[1651] | 1792 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
[1808] | 1793 | : trace_label_diverges_exists (RTLabs_status ge) s ≝ |
---|
[1812] | 1794 | match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with |
---|
[1784] | 1795 | [ ex_intro n B ⇒ |
---|
[1812] | 1796 | match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B |
---|
[1808] | 1797 | return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s |
---|
[1784] | 1798 | with |
---|
[1805] | 1799 | [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. |
---|
[1812] | 1800 | let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in |
---|
[1960] | 1801 | tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) T' |
---|
[1808] | 1802 | (* |
---|
[1812] | 1803 | match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with |
---|
[1784] | 1804 | [ ex_intro T' _ ⇒ |
---|
| 1805 | ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I |
---|
[1808] | 1806 | ]*) |
---|
[1806] | 1807 | | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL. |
---|
[1812] | 1808 | let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in |
---|
[1960] | 1809 | tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) ?? T' |
---|
[1808] | 1810 | (* |
---|
[1812] | 1811 | match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with |
---|
[1806] | 1812 | [ ex_intro T' _ ⇒ |
---|
| 1813 | ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? |
---|
[1808] | 1814 | ]*) |
---|
[1784] | 1815 | ] STATEMENT_COSTLABEL |
---|
| 1816 | ]. |
---|
[1960] | 1817 | [ @(costed_RTLabs ge) @(trace_any_label_label … T) |
---|
[1808] | 1818 | | %{tr} @EV |
---|
[1806] | 1819 | | @(trace_any_call_call … T) |
---|
| 1820 | | @(well_cost_labelled_call … EV) // @(trace_any_call_call … T) |
---|
[1812] | 1821 | ] qed. |
---|
| 1822 | |
---|
[1880] | 1823 | lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'. |
---|
| 1824 | make_initial_state p = OK ? s1 → |
---|
| 1825 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
| 1826 | stack_preserved ends_with_ret s2 s' → |
---|
| 1827 | RTLabs_is_final s' ≠ None ?. |
---|
| 1828 | #ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?); |
---|
| 1829 | @bind_ok #m #_ |
---|
| 1830 | @bind_ok #b #_ |
---|
| 1831 | @bind_ok #f #_ |
---|
| 1832 | #E destruct |
---|
[2025] | 1833 | #EV #SP inversion (eval_preserves … EV) |
---|
[1880] | 1834 | [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct |
---|
| 1835 | inversion SP |
---|
| 1836 | [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct |
---|
| 1837 | | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct |
---|
| 1838 | inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct |
---|
| 1839 | ] |
---|
| 1840 | | *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct |
---|
| 1841 | ] qed. |
---|
| 1842 | |
---|
| 1843 | lemma initial_state_is_call : ∀p,s. |
---|
| 1844 | make_initial_state p = OK ? s → |
---|
| 1845 | RTLabs_classify s = cl_call. |
---|
| 1846 | #p #s whd in ⊢ (??%? → ?); |
---|
| 1847 | @bind_ok #m #_ |
---|
| 1848 | @bind_ok #b #_ |
---|
| 1849 | @bind_ok #f #_ |
---|
| 1850 | #E destruct |
---|
| 1851 | @refl |
---|
| 1852 | qed. |
---|
| 1853 | |
---|
| 1854 | let rec whole_structured_trace_exists ge p s |
---|
[1812] | 1855 | (trace: flat_trace io_out io_in ge s) |
---|
| 1856 | (ORACLE: termination_oracle) |
---|
| 1857 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
| 1858 | (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) |
---|
[1880] | 1859 | : ∀INITIAL: make_initial_state p = OK ? s. |
---|
| 1860 | ∀NOT_WRONG: not_wrong ??? s trace. |
---|
[1812] | 1861 | ∀STATE_COSTLABELLED: well_cost_labelled_state s. |
---|
| 1862 | ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s. |
---|
| 1863 | trace_whole_program_exists (RTLabs_status ge) s ≝ |
---|
[1880] | 1864 | match trace return λs,trace. make_initial_state p = OK ? s → |
---|
| 1865 | not_wrong ??? s trace → |
---|
[1812] | 1866 | well_cost_labelled_state s → |
---|
| 1867 | soundly_labelled_state s → |
---|
| 1868 | trace_whole_program_exists (RTLabs_status ge) s with |
---|
[1880] | 1869 | [ ft_step s tr next EV trace' ⇒ λINITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. |
---|
| 1870 | let IS_CALL ≝ initial_state_is_call … INITIAL in |
---|
[1812] | 1871 | match ORACLE ge O next trace' with |
---|
| 1872 | [ or_introl TERMINATES ⇒ |
---|
| 1873 | match TERMINATES with |
---|
| 1874 | [ witness TERMINATES ⇒ |
---|
| 1875 | let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in |
---|
[1880] | 1876 | twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) ? |
---|
[1812] | 1877 | ] |
---|
| 1878 | | or_intror NO_TERMINATION ⇒ |
---|
| 1879 | twp_diverges (RTLabs_status ge) s next IS_CALL ? |
---|
| 1880 | (make_label_diverges ge next trace' ORACLE ? |
---|
| 1881 | ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?) |
---|
| 1882 | ] |
---|
[1880] | 1883 | | ft_stop st FINAL ⇒ λINITIAL,NOT_WRONG. ⊥ |
---|
| 1884 | | ft_wrong start m NF EV ⇒ λINITIAL,NOT_WRONG. ⊥ |
---|
[1812] | 1885 | ]. |
---|
[1880] | 1886 | [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct |
---|
[1812] | 1887 | cases FINAL #E @E @refl |
---|
| 1888 | | %{tr} @EV |
---|
[1880] | 1889 | | @(after_the_initial_call_is_the_final_state … INITIAL EV) |
---|
| 1890 | @(stack_ok … tlr) |
---|
[1812] | 1891 | | @(well_cost_labelled_state_step … EV) // |
---|
| 1892 | | @(well_cost_labelled_call … EV) // |
---|
| 1893 | | %{tr} @EV |
---|
| 1894 | | @(well_cost_labelled_call … EV) // |
---|
| 1895 | | % [ @(well_cost_labelled_state_step … EV) // |
---|
| 1896 | | @(soundly_labelled_state_step … EV) // |
---|
| 1897 | | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/ |
---|
| 1898 | | @(still_not_wrong … NOT_WRONG) |
---|
| 1899 | | @(not_return_to_not_final … EV) >IS_CALL % #E destruct |
---|
| 1900 | ] |
---|
| 1901 | | inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct |
---|
| 1902 | ] qed. |
---|
| 1903 | |
---|
| 1904 | definition well_cost_labelled_program : RTLabs_program → Prop ≝ |
---|
| 1905 | λp. All ? (λx. let 〈id,fd〉 ≝ x in |
---|
| 1906 | match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p). |
---|
| 1907 | (* |
---|
| 1908 | theorem program_trace_exists : |
---|
| 1909 | termination_oracle → |
---|
| 1910 | ∀p:RTLabs_program. |
---|
| 1911 | ∀s:state. |
---|
| 1912 | ∀I: make_initial_state p = OK ? s. |
---|
| 1913 | |
---|
| 1914 | let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in |
---|
| 1915 | |
---|
| 1916 | ∀NOIO:exec_no_io … plain_trace. |
---|
| 1917 | |
---|
| 1918 | let flat_trace ≝ make_whole_flat_trace p s NOIO I in |
---|
| 1919 | |
---|
| 1920 | trace_whole_program_exists (RTLabs_status (make_global p)) s. |
---|
| 1921 | #ORACLE #p #s #I |
---|
| 1922 | letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p) |
---|
| 1923 | #NOIO |
---|
| 1924 | letin flat_trace ≝ (make_whole_flat_trace p s NOIO I) |
---|
| 1925 | whd |
---|
| 1926 | @(whole_structured_trace_exists … flat_trace) |
---|
| 1927 | // |
---|
| 1928 | [ whd |
---|
[1880] | 1929 | *) |
---|
| 1930 | |
---|
| 1931 | (* as_execute might be in Prop, but because the semantics is deterministic |
---|
| 1932 | we can retrieve the event trace anyway. *) |
---|
| 1933 | let rec deprop_as_execute ge s s' |
---|
| 1934 | (X:as_execute (RTLabs_status ge) s s') |
---|
| 1935 | : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝ |
---|
| 1936 | match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ? with |
---|
| 1937 | [ Value ts ⇒ λY. «fst … ts, ?» |
---|
| 1938 | | _ ⇒ λY. ⊥ |
---|
| 1939 | ] X. |
---|
| 1940 | [ 1,3: cases Y #x #E destruct |
---|
| 1941 | | cases Y #trP #E destruct @refl |
---|
| 1942 | ] qed. |
---|
| 1943 | |
---|
| 1944 | (* A non-empty finite section of a flat_trace *) |
---|
| 1945 | inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝ |
---|
| 1946 | | pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s' |
---|
| 1947 | | pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''. |
---|
| 1948 | |
---|
| 1949 | let rec append_partial_flat_trace o i ge s1 s2 s3 |
---|
| 1950 | (tr1:partial_flat_trace o i ge s1 s2) |
---|
| 1951 | on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝ |
---|
| 1952 | match tr1 with |
---|
| 1953 | [ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX |
---|
| 1954 | | pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2) |
---|
| 1955 | ]. |
---|
| 1956 | |
---|
| 1957 | let rec partial_to_flat_trace o i ge s1 s2 |
---|
| 1958 | (tr:partial_flat_trace o i ge s1 s2) |
---|
| 1959 | on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝ |
---|
| 1960 | match tr with |
---|
| 1961 | [ pft_base s tr s' EX ⇒ ft_step … EX |
---|
| 1962 | | pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'') |
---|
| 1963 | ]. |
---|
| 1964 | |
---|
| 1965 | (* Extract a flat trace from a structured one. *) |
---|
[1960] | 1966 | let rec flat_trace_of_label_return ge s s' |
---|
[1880] | 1967 | (tr:trace_label_return (RTLabs_status ge) s s') |
---|
| 1968 | on tr : |
---|
| 1969 | partial_flat_trace io_out io_in ge s s' ≝ |
---|
| 1970 | match tr with |
---|
[1960] | 1971 | [ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll |
---|
[1880] | 1972 | | tlr_step s1 s2 s3 tll tlr ⇒ |
---|
| 1973 | append_partial_flat_trace … |
---|
[1960] | 1974 | (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll) |
---|
| 1975 | (flat_trace_of_label_return ge s2 s3 tlr) |
---|
[1880] | 1976 | ] |
---|
[1960] | 1977 | and flat_trace_of_label_label ge ends s s' |
---|
[1880] | 1978 | (tr:trace_label_label (RTLabs_status ge) ends s s') |
---|
| 1979 | on tr : |
---|
| 1980 | partial_flat_trace io_out io_in ge s s' ≝ |
---|
| 1981 | match tr with |
---|
[1960] | 1982 | [ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal |
---|
[1880] | 1983 | ] |
---|
[1960] | 1984 | and flat_trace_of_any_label ge ends s s' |
---|
[1880] | 1985 | (tr:trace_any_label (RTLabs_status ge) ends s s') |
---|
| 1986 | on tr : |
---|
| 1987 | partial_flat_trace io_out io_in ge s s' ≝ |
---|
| 1988 | match tr with |
---|
| 1989 | [ tal_base_not_return s1 s2 EX CL CS ⇒ |
---|
| 1990 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
| 1991 | pft_base … EX' ] |
---|
| 1992 | | tal_base_return s1 s2 EX CL ⇒ |
---|
| 1993 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
| 1994 | pft_base … EX' ] |
---|
| 1995 | | tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒ |
---|
[1960] | 1996 | let suffix' ≝ flat_trace_of_label_return ge ?? tlr in |
---|
[1880] | 1997 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
| 1998 | pft_step … EX' suffix' ] |
---|
| 1999 | | tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒ |
---|
| 2000 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
| 2001 | pft_step … EX' |
---|
| 2002 | (append_partial_flat_trace … |
---|
[1960] | 2003 | (flat_trace_of_label_return ge ?? tlr) |
---|
| 2004 | (flat_trace_of_any_label ge ??? tal)) |
---|
[1880] | 2005 | ] |
---|
| 2006 | | tal_step_default ends s1 s2 s3 EX tal CL CS ⇒ |
---|
| 2007 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
[1960] | 2008 | pft_step … EX' (flat_trace_of_any_label ge ??? tal) |
---|
[1880] | 2009 | ] |
---|
| 2010 | ]. |
---|
| 2011 | |
---|
| 2012 | |
---|
| 2013 | (* We take an extra step so that we can always return a non-empty trace to |
---|
| 2014 | satisfy the guardedness condition in the cofixpoint. *) |
---|
[1960] | 2015 | let rec flat_trace_of_any_call ge s s' s'' et |
---|
[1880] | 2016 | (tr:trace_any_call (RTLabs_status ge) s s') |
---|
| 2017 | (EX'':eval_statement ge s' = Value … 〈et,s''〉) |
---|
| 2018 | on tr : |
---|
| 2019 | partial_flat_trace io_out io_in ge s s'' ≝ |
---|
| 2020 | match tr return λs,s'.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with |
---|
| 2021 | [ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX'' |
---|
| 2022 | | tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''. |
---|
| 2023 | match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒ |
---|
| 2024 | pft_step … EX' |
---|
| 2025 | (append_partial_flat_trace … |
---|
[1960] | 2026 | (flat_trace_of_label_return ge ?? tlr) |
---|
| 2027 | (flat_trace_of_any_call ge … tac EX'')) |
---|
[1880] | 2028 | ] |
---|
| 2029 | | tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''. |
---|
| 2030 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
| 2031 | pft_step … EX' |
---|
[1960] | 2032 | (flat_trace_of_any_call ge … tal EX'') |
---|
[1880] | 2033 | ] |
---|
| 2034 | ] EX''. |
---|
| 2035 | |
---|
[1960] | 2036 | let rec flat_trace_of_label_call ge s s' s'' et |
---|
[1880] | 2037 | (tr:trace_label_call (RTLabs_status ge) s s') |
---|
| 2038 | (EX'':eval_statement ge s' = Value … 〈et,s''〉) |
---|
| 2039 | on tr : |
---|
| 2040 | partial_flat_trace io_out io_in ge s s'' ≝ |
---|
| 2041 | match tr with |
---|
[1960] | 2042 | [ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac |
---|
[1880] | 2043 | ] EX''. |
---|
| 2044 | |
---|
| 2045 | (* Now reconstruct the flat_trace of a diverging execution. Note that we need |
---|
| 2046 | to take care to satisfy the guardedness condition by witnessing the fact that |
---|
| 2047 | the partial traces are non-empty. *) |
---|
[1960] | 2048 | let corec flat_trace_of_label_diverges ge s |
---|
[1880] | 2049 | (tr:trace_label_diverges (RTLabs_status ge) s) |
---|
| 2050 | : flat_trace io_out io_in ge s ≝ |
---|
| 2051 | match tr with |
---|
| 2052 | [ tld_step sx sy tll tld ⇒ |
---|
[1960] | 2053 | match flat_trace_of_label_label ge … tll with |
---|
| 2054 | [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) |
---|
[1880] | 2055 | | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) |
---|
| 2056 | ] tld |
---|
| 2057 | | tld_base s1 s2 s3 tlc EX CL tld ⇒ |
---|
| 2058 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
[1960] | 2059 | match flat_trace_of_label_call … tlc EX' with |
---|
| 2060 | [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) |
---|
[1880] | 2061 | | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) |
---|
| 2062 | ] tld |
---|
| 2063 | ] |
---|
| 2064 | ] |
---|
| 2065 | (* Helper to keep adding the partial trace without violating the guardedness |
---|
| 2066 | condition. *) |
---|
| 2067 | and add_partial_flat_trace ge s s' |
---|
| 2068 | (ptr:partial_flat_trace io_out io_in ge s s') |
---|
| 2069 | (tr:trace_label_diverges (RTLabs_status ge) s') |
---|
| 2070 | : flat_trace io_out io_in ge s ≝ |
---|
| 2071 | match ptr with |
---|
[1960] | 2072 | [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr) |
---|
[1880] | 2073 | | pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr) |
---|
| 2074 | ] tr |
---|
| 2075 | . |
---|
| 2076 | |
---|
| 2077 | coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝ |
---|
| 2078 | | eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F) |
---|
| 2079 | | 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) |
---|
| 2080 | | eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX). |
---|
| 2081 | |
---|
| 2082 | (* XXX move to semantics *) |
---|
| 2083 | lemma final_cannot_move : ∀ge,s. |
---|
| 2084 | RTLabs_is_final s ≠ None ? → |
---|
| 2085 | ∃err. eval_statement ge s = Wrong ??? err. |
---|
| 2086 | #ge * |
---|
| 2087 | [ #f #fs #m * #F cases (F ?) @refl |
---|
| 2088 | | #a #b #c #d #e * #F cases (F ?) @refl |
---|
| 2089 | | #a #b #c #d * #F cases (F ?) @refl |
---|
| 2090 | | #r #F % [2: @refl | skip ] |
---|
| 2091 | ] qed. |
---|
| 2092 | |
---|
| 2093 | let corec flat_traces_are_determined_by_starting_point ge s tr1 |
---|
| 2094 | : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝ |
---|
| 2095 | match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with |
---|
| 2096 | [ ft_stop s F ⇒ λtr2. ? |
---|
| 2097 | | ft_step s1 tr s2 EX0 tr1' ⇒ λtr2. |
---|
| 2098 | match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with |
---|
| 2099 | [ ft_stop s F ⇒ λEX. ? |
---|
| 2100 | | ft_step s tr' s2' EX' tr2' ⇒ λEX. ? |
---|
| 2101 | | ft_wrong s m NF EX' ⇒ λEX. ? |
---|
| 2102 | ] EX0 |
---|
| 2103 | | ft_wrong s m NF EX ⇒ λtr2. ? |
---|
| 2104 | ]. |
---|
| 2105 | [ inversion tr2 in tr1 F; |
---|
| 2106 | [ #s #F #_ #_ #tr1 #F' @eft_stop |
---|
| 2107 | | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct |
---|
| 2108 | cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct |
---|
| 2109 | | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/ |
---|
| 2110 | ] |
---|
| 2111 | | @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct |
---|
| 2112 | | -EX0 |
---|
| 2113 | cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *) |
---|
| 2114 | @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX') |
---|
| 2115 | -E -EX' -tr2' #tr2' #EX' |
---|
| 2116 | cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *) |
---|
| 2117 | @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX') |
---|
| 2118 | -E -EX' #EX' |
---|
| 2119 | @eft_step @flat_traces_are_determined_by_starting_point |
---|
| 2120 | | @⊥ >EX in EX'; #E destruct |
---|
| 2121 | | inversion tr2 in NF EX; |
---|
| 2122 | [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/ |
---|
| 2123 | | #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct |
---|
| 2124 | | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl. |
---|
| 2125 | #E destruct |
---|
| 2126 | @eft_wrong |
---|
| 2127 | ] |
---|
| 2128 | ] qed. |
---|
| 2129 | |
---|
| 2130 | let corec diverging_traces_have_unique_flat_trace ge s |
---|
| 2131 | (str:trace_label_diverges (RTLabs_status ge) s) |
---|
| 2132 | (tr:flat_trace io_out io_in ge s) |
---|
[1960] | 2133 | : equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?. |
---|
[1880] | 2134 | @flat_traces_are_determined_by_starting_point |
---|
| 2135 | qed. |
---|
| 2136 | |
---|
[1960] | 2137 | let rec flat_trace_of_whole_program ge s |
---|
[1880] | 2138 | (tr:trace_whole_program (RTLabs_status ge) s) |
---|
| 2139 | on tr : flat_trace io_out io_in ge s ≝ |
---|
| 2140 | match tr with |
---|
| 2141 | [ twp_terminating s1 s2 sf CL EX tlr F ⇒ |
---|
| 2142 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
[1960] | 2143 | ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sf F)) |
---|
[1880] | 2144 | ] |
---|
| 2145 | | twp_diverges s1 s2 CL EX tld ⇒ |
---|
| 2146 | match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ |
---|
[1960] | 2147 | ft_step … EX' (flat_trace_of_label_diverges … tld) |
---|
[1880] | 2148 | ] |
---|
| 2149 | ]. |
---|
| 2150 | |
---|
| 2151 | let corec whole_traces_have_unique_flat_trace ge s |
---|
| 2152 | (str:trace_whole_program (RTLabs_status ge) s) |
---|
| 2153 | (tr:flat_trace io_out io_in ge s) |
---|
[1960] | 2154 | : equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?. |
---|
[1880] | 2155 | @flat_traces_are_determined_by_starting_point |
---|
| 2156 | qed. |
---|