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