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