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