1 | |
---|
2 | include "RTLabs/semantics.ma". |
---|
3 | include "common/StructuredTraces.ma". |
---|
4 | |
---|
5 | discriminator status_class. |
---|
6 | |
---|
7 | (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps |
---|
8 | will be added later (LTL → LIN). *) |
---|
9 | |
---|
10 | definition RTLabs_classify : state → status_class ≝ |
---|
11 | λs. match s with |
---|
12 | [ State f _ _ ⇒ |
---|
13 | match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with |
---|
14 | [ St_cond _ _ _ ⇒ cl_jump |
---|
15 | | St_jumptable _ _ ⇒ cl_jump |
---|
16 | | _ ⇒ cl_other |
---|
17 | ] |
---|
18 | | Callstate _ _ _ _ _ ⇒ cl_call |
---|
19 | | Returnstate _ _ _ _ ⇒ cl_return |
---|
20 | ]. |
---|
21 | |
---|
22 | definition is_cost_label : statement → bool ≝ |
---|
23 | λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. |
---|
24 | |
---|
25 | definition RTLabs_cost : state → bool ≝ |
---|
26 | λs. match s with |
---|
27 | [ State f fs m ⇒ |
---|
28 | is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) |
---|
29 | | _ ⇒ false |
---|
30 | ]. |
---|
31 | |
---|
32 | definition RTLabs_status : genv → abstract_status ≝ |
---|
33 | λge. |
---|
34 | mk_abstract_status |
---|
35 | state |
---|
36 | (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) |
---|
37 | (λs,c. RTLabs_classify s = c) |
---|
38 | (λs. RTLabs_cost s = true) |
---|
39 | (λs,s'. match s with |
---|
40 | [ mk_Sig s p ⇒ |
---|
41 | match s return λs. RTLabs_classify s = cl_call → ? with |
---|
42 | [ Callstate fd args dst stk m ⇒ |
---|
43 | λ_. match s' with |
---|
44 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ] |
---|
45 | | _ ⇒ False |
---|
46 | ] |
---|
47 | | State f fs m ⇒ λH.⊥ |
---|
48 | | _ ⇒ λH.⊥ |
---|
49 | ] p |
---|
50 | ]). |
---|
51 | [ normalize in H; destruct |
---|
52 | | whd in H:(??%?); |
---|
53 | cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; |
---|
54 | normalize try #a try #b try #c try #d try #e try #g try #h destruct |
---|
55 | ] qed. |
---|
56 | |
---|
57 | lemma RTLabs_not_cost : ∀ge,s. |
---|
58 | RTLabs_cost s = false → |
---|
59 | ¬ as_costed (RTLabs_status ge) s. |
---|
60 | #ge #s #E % whd in ⊢ (% → ?); >E #E' destruct |
---|
61 | qed. |
---|
62 | |
---|
63 | (* Before attempting to construct a structured trace, let's show that we can |
---|
64 | form flat traces with evidence that they were constructed from an execution. |
---|
65 | |
---|
66 | For now we don't consider I/O. *) |
---|
67 | |
---|
68 | |
---|
69 | coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ |
---|
70 | | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) |
---|
71 | | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) |
---|
72 | | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). |
---|
73 | |
---|
74 | (* add I/O? *) |
---|
75 | coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ |
---|
76 | | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s |
---|
77 | | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s |
---|
78 | | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. |
---|
79 | |
---|
80 | let corec make_flat_trace ge s |
---|
81 | (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : |
---|
82 | flat_trace io_out io_in ge s ≝ |
---|
83 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
84 | match e return λx. e = x → ? with |
---|
85 | [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) |
---|
86 | | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) |
---|
87 | | e_wrong m ⇒ λE. ft_wrong … s m ? |
---|
88 | | e_interact o f ⇒ λE. ⊥ |
---|
89 | ] (refl ? e). |
---|
90 | [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
91 | cases (eval_statement ge s) |
---|
92 | [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
93 | | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); |
---|
94 | >(?:is_final ????? = RTLabs_is_final s1) // |
---|
95 | lapply (refl ? (RTLabs_is_final s1)) |
---|
96 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
97 | [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct |
---|
98 | | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl |
---|
99 | | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct |
---|
100 | ] |
---|
101 | | *: #m whd in ⊢ (??%? → ?); #E destruct |
---|
102 | ] |
---|
103 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
104 | cases (eval_statement ge s) |
---|
105 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
106 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
107 | cases (is_final ?????) |
---|
108 | [ whd in ⊢ (??%? → ?); #E destruct @refl |
---|
109 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
110 | ] |
---|
111 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
112 | ] |
---|
113 | | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; |
---|
114 | cases (eval_statement ge s) |
---|
115 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
116 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
117 | cases (is_final ?????) |
---|
118 | [ whd in ⊢ (??%? → ?); #E |
---|
119 | change with (eval_statement ge s1) in E:(??(??????(?????%))?); |
---|
120 | destruct |
---|
121 | inversion H |
---|
122 | [ #a #b #c #E1 destruct |
---|
123 | | #trx #sx #ex #H1 #E2 #E3 destruct @H1 |
---|
124 | | #m #E1 destruct |
---|
125 | ] |
---|
126 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
127 | ] |
---|
128 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
129 | ] |
---|
130 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
131 | cases (eval_statement ge s) |
---|
132 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
133 | | * #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
134 | cases (is_final ?????) |
---|
135 | [ whd in ⊢ (??%? → ?); #E destruct |
---|
136 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
137 | ] |
---|
138 | | #m whd in ⊢ (??%? → ?); #E destruct @refl |
---|
139 | ] |
---|
140 | | whd in E:(??%?); >E in H; #H |
---|
141 | inversion H |
---|
142 | [ #a #b #c #E destruct |
---|
143 | | #a #b #c #d #E1 destruct |
---|
144 | | #m #E1 destruct |
---|
145 | ] |
---|
146 | ] qed. |
---|
147 | |
---|
148 | let corec make_whole_flat_trace p s |
---|
149 | (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) |
---|
150 | (I:make_initial_state ??? p = OK ? s) : |
---|
151 | flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ |
---|
152 | let ge ≝ make_global … p in |
---|
153 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
154 | match e return λx. e = x → ? with |
---|
155 | [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? |
---|
156 | | e_step _ _ e' ⇒ λE. make_flat_trace ge s ? |
---|
157 | | e_wrong m ⇒ λE. ⊥ |
---|
158 | | e_interact o f ⇒ λE. ⊥ |
---|
159 | ] (refl ? e). |
---|
160 | [ whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
161 | whd in ⊢ (??%? → ?); |
---|
162 | >(?:is_final ????? = RTLabs_is_final s) // |
---|
163 | lapply (refl ? (RTLabs_is_final s)) |
---|
164 | cases (RTLabs_is_final s) in ⊢ (???% → %); |
---|
165 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
166 | | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct |
---|
167 | ] |
---|
168 | | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); |
---|
169 | >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) |
---|
170 | [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H |
---|
171 | [ #a #b #c #E1 destruct |
---|
172 | | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) |
---|
173 | @H1 |
---|
174 | | #m #E1 destruct |
---|
175 | ] |
---|
176 | | #i whd in ⊢ (??%? → ???% → ?); #E destruct |
---|
177 | ] |
---|
178 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
179 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
180 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
181 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
182 | ] qed. |
---|
183 | |
---|
184 | (* Need a way to choose whether a called function terminates. Then, |
---|
185 | if the initial function terminates we generate a purely inductive structured trace, |
---|
186 | otherwise we start generating the coinductive one, and on every function call |
---|
187 | use the choice method again to decide whether to step over or keep going. |
---|
188 | |
---|
189 | Not quite what we need - have to decide on seeing each label whether we will see |
---|
190 | another or hit a non-terminating call? |
---|
191 | |
---|
192 | Also - need the notion of well-labelled in order to break loops. |
---|
193 | |
---|
194 | |
---|
195 | |
---|
196 | outline: |
---|
197 | |
---|
198 | does function terminate? |
---|
199 | - yes, get (bound on the number of steps until return), generate finite |
---|
200 | structure using bound as termination witness |
---|
201 | - no, get (¬ bound on steps to return), start building infinite trace out of |
---|
202 | finite steps. At calls, check for termination, generate appr. form. |
---|
203 | |
---|
204 | generating the finite parts: |
---|
205 | |
---|
206 | We start with the status after the call has been executed; well-labelling tells |
---|
207 | us that this is a labelled state. Now we want to generate a trace_label_return |
---|
208 | and also return the remainder of the flat trace. |
---|
209 | |
---|
210 | *) |
---|
211 | |
---|
212 | (* [will_return ge depth s trace] says that after a finite number of steps of |
---|
213 | [trace] from [s] we reach the return state for the current function. [depth] |
---|
214 | performs the call/return counting necessary for handling deeper function |
---|
215 | calls. It should be zero at the top level. *) |
---|
216 | inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝ |
---|
217 | | wr_step : ∀s,tr,s',depth,EX,trace. |
---|
218 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
219 | will_return ge depth s' trace → |
---|
220 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
221 | | wr_call : ∀s,tr,s',depth,EX,trace. |
---|
222 | RTLabs_classify s = cl_call → |
---|
223 | will_return ge (S depth) s' trace → |
---|
224 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
225 | | wr_ret : ∀s,tr,s',depth,EX,trace. |
---|
226 | RTLabs_classify s = cl_return → |
---|
227 | will_return ge depth s' trace → |
---|
228 | will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace) |
---|
229 | (* Note that we require the ability to make a step after the return (this |
---|
230 | corresponds to somewhere that will be guaranteed to be a label at the |
---|
231 | end of the compilation chain). *) |
---|
232 | | wr_base : ∀s,tr,s',EX,trace. |
---|
233 | RTLabs_classify s = cl_return → |
---|
234 | will_return ge O s (ft_step ?? ge s tr s' EX trace) |
---|
235 | . |
---|
236 | |
---|
237 | (* The way we will use [will_return] won't satisfy Matita's guardedness check, |
---|
238 | so we will measure the length of these termination proofs and use an upper |
---|
239 | bound to show termination of the finite structured trace construction |
---|
240 | functions. *) |
---|
241 | |
---|
242 | let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝ |
---|
243 | match T with |
---|
244 | [ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
245 | | wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
246 | | wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') |
---|
247 | | wr_base _ _ _ _ _ _ ⇒ S O |
---|
248 | ]. |
---|
249 | |
---|
250 | include alias "arithmetics/nat.ma". |
---|
251 | |
---|
252 | (* Specialised to the particular situation it is used in. *) |
---|
253 | lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False. |
---|
254 | #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] |
---|
255 | whd in ⊢ (??(??%) → ?); |
---|
256 | >commutative_times |
---|
257 | #H lapply (le_plus_b … H) |
---|
258 | #H lapply (le_to_leb_true … H) |
---|
259 | normalize #E destruct |
---|
260 | qed. |
---|
261 | |
---|
262 | (* Inversion lemmas on [will_return] that also note the effect on the length |
---|
263 | of the proof. *) |
---|
264 | lemma will_return_call : ∀ge,d,s,tr,s',EX,trace. |
---|
265 | RTLabs_classify s = cl_call → |
---|
266 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
267 | ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'. |
---|
268 | #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM |
---|
269 | [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct |
---|
270 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % // |
---|
271 | | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct |
---|
272 | | #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct |
---|
273 | ] qed. |
---|
274 | |
---|
275 | lemma will_return_return : ∀ge,d,s,tr,s',EX,trace. |
---|
276 | RTLabs_classify s = cl_return → |
---|
277 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
278 | match d with |
---|
279 | [ O ⇒ True |
---|
280 | | S d' ⇒ |
---|
281 | ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' |
---|
282 | ]. |
---|
283 | #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM |
---|
284 | [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct |
---|
285 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥ destruct >CL in H39; #E destruct |
---|
286 | | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % // |
---|
287 | | #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I |
---|
288 | ] qed. |
---|
289 | |
---|
290 | lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace. |
---|
291 | (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) → |
---|
292 | ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). |
---|
293 | ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'. |
---|
294 | #ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM |
---|
295 | [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % // |
---|
296 | | #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct |
---|
297 | | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct |
---|
298 | | #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct |
---|
299 | | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % // |
---|
300 | | #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct |
---|
301 | | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct |
---|
302 | | #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct |
---|
303 | ] qed. |
---|
304 | |
---|
305 | (* We require that labels appear after branch instructions and at the start of |
---|
306 | functions. The first is required for preciseness, the latter for soundness. |
---|
307 | We will make a separate requirement for there to be a finite number of steps |
---|
308 | between labels to catch loops for soundness (is this sufficient?). *) |
---|
309 | |
---|
310 | definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ |
---|
311 | λf,s. match s return λs. labels_present ? s → Prop with |
---|
312 | [ St_cond _ l1 l2 ⇒ λH. |
---|
313 | is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧ |
---|
314 | is_cost_label (lookup_present … (f_graph f) l2 ?) = true |
---|
315 | | St_jumptable _ ls ⇒ λH. |
---|
316 | (* I did have a dependent version of All here, but it's a pain. *) |
---|
317 | All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls |
---|
318 | | _ ⇒ λ_. True |
---|
319 | ]. whd in H; |
---|
320 | [ @(proj1 … H) |
---|
321 | | @(proj2 … H) |
---|
322 | ] qed. |
---|
323 | |
---|
324 | definition well_cost_labelled_fn : internal_function → Prop ≝ |
---|
325 | λf. (∀l. ∀H:present … (f_graph f) l. |
---|
326 | well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧ |
---|
327 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true. |
---|
328 | [ @lookup_lookup_present | cases (f_entry f) // ] qed. |
---|
329 | |
---|
330 | (* We need to ensure that any code we come across is well-cost-labelled. We may |
---|
331 | get function code from either the global environment or the state. *) |
---|
332 | |
---|
333 | definition well_cost_labelled_ge : genv → Prop ≝ |
---|
334 | λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. |
---|
335 | |
---|
336 | definition well_cost_labelled_state : state → Prop ≝ |
---|
337 | λs. match s with |
---|
338 | [ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
339 | | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧ |
---|
340 | All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
341 | | Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
342 | ]. |
---|
343 | |
---|
344 | lemma well_cost_labelled_state_step : ∀ge,s,tr,s'. |
---|
345 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
346 | well_cost_labelled_ge ge → |
---|
347 | well_cost_labelled_state s → |
---|
348 | well_cost_labelled_state s'. |
---|
349 | #ge #s #tr' #s' #EV cases (eval_perserves … EV) |
---|
350 | [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // |
---|
351 | | #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ |
---|
352 | (* |
---|
353 | | #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ |
---|
354 | *) |
---|
355 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ |
---|
356 | | #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 |
---|
357 | | #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // |
---|
358 | ] qed. |
---|
359 | |
---|
360 | lemma rtlabs_jump_inv : ∀s. |
---|
361 | RTLabs_classify s = cl_jump → |
---|
362 | ∃f,fs,m. s = State f fs m ∧ |
---|
363 | let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in |
---|
364 | (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls). |
---|
365 | * |
---|
366 | [ #f #fs #m #E |
---|
367 | %{f} %{fs} %{m} % |
---|
368 | [ @refl |
---|
369 | | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; |
---|
370 | try (normalize try #A try #B try #C try #D try #F try #G try #H destruct) |
---|
371 | [ %1 %{A} %{B} %{C} @refl |
---|
372 | | %2 %{A} %{B} @refl |
---|
373 | ] |
---|
374 | ] |
---|
375 | | normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct |
---|
376 | | normalize #H8 #H9 #H10 #H11 #H12 destruct |
---|
377 | ] qed. |
---|
378 | |
---|
379 | lemma well_cost_labelled_jump : ∀ge,s,tr,s'. |
---|
380 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
381 | well_cost_labelled_state s → |
---|
382 | RTLabs_classify s = cl_jump → |
---|
383 | RTLabs_cost s' = true. |
---|
384 | #ge #s #tr #s' #EV #H #CL |
---|
385 | cases (rtlabs_jump_inv s CL) |
---|
386 | #fr * #fs * #m * #Es * |
---|
387 | [ * #r * #l1 * #l2 #Estmt |
---|
388 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
389 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
390 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
391 | (* replace with lemma on successors? *) |
---|
392 | @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct |
---|
393 | lapply (Hbody (next fr) (next_ok fr)) |
---|
394 | generalize in ⊢ (???% → ?); |
---|
395 | >Estmt #LP' |
---|
396 | whd in ⊢ (% → ?); |
---|
397 | * #H1 #H2 [ @H1 | @H2 ] |
---|
398 | | * #r * #ls #Estmt |
---|
399 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
400 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
401 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
402 | (* replace with lemma on successors? *) |
---|
403 | @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ] #Ea whd in ⊢ (??%? → ?); |
---|
404 | [ 2: (* later *) |
---|
405 | | *: #E destruct |
---|
406 | ] |
---|
407 | lapply (Hbody (next fr) (next_ok fr)) |
---|
408 | generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP |
---|
409 | generalize in ⊢ (??(?%)? → ?); |
---|
410 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
411 | [ #E1 #E2 whd in E2:(??%?); destruct |
---|
412 | | #l' #E1 #E2 whd in E2:(??%?); destruct |
---|
413 | cases (All_nth ???? CP ? E1) |
---|
414 | #H1 #H2 @H2 |
---|
415 | ] |
---|
416 | ] qed. |
---|
417 | |
---|
418 | lemma rtlabs_call_inv : ∀s. |
---|
419 | RTLabs_classify s = cl_call → |
---|
420 | ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m. |
---|
421 | * [ #f #fs #m whd in ⊢ (??%? → ?); |
---|
422 | cases (lookup_present … (next f) (next_ok f)) normalize |
---|
423 | try #A try #B try #C try #D try #E try #F try #G destruct |
---|
424 | | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl |
---|
425 | | normalize #H411 #H412 #H413 #H414 #H415 destruct |
---|
426 | ] qed. |
---|
427 | |
---|
428 | lemma well_cost_labelled_call : ∀ge,s,tr,s'. |
---|
429 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
430 | well_cost_labelled_state s → |
---|
431 | RTLabs_classify s = cl_call → |
---|
432 | RTLabs_cost s' = true. |
---|
433 | #ge #s #tr #s' #EV #WCL #CL |
---|
434 | cases (rtlabs_call_inv s CL) |
---|
435 | #fd * #args * #dst * #stk * #m #E >E in EV WCL; |
---|
436 | whd in ⊢ (??%? → % → ?); |
---|
437 | cases fd |
---|
438 | [ #fn whd in ⊢ (??%? → % → ?); |
---|
439 | @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any) |
---|
440 | #m' #b whd in ⊢ (??%? → ?); #E' destruct |
---|
441 | * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 |
---|
442 | @WCL2 |
---|
443 | | #fn whd in ⊢ (??%? → % → ?); |
---|
444 | @bindIO_value #evargs #Eargs |
---|
445 | whd in ⊢ (??%? → ?); |
---|
446 | #E' destruct |
---|
447 | ] qed. |
---|
448 | |
---|
449 | |
---|
450 | (* The preservation of (most of) the stack is useful to show as_after_return. |
---|
451 | We do this by showing that during the execution of a function the lower stack |
---|
452 | frames never change, and that after returning from the function we preserve |
---|
453 | the identity of the next instruction to execute. |
---|
454 | *) |
---|
455 | |
---|
456 | inductive stack_of_state : list frame → state → Prop ≝ |
---|
457 | | sos_State : ∀f,fs,m. stack_of_state fs (State f fs m) |
---|
458 | | sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m) |
---|
459 | | sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m) |
---|
460 | . |
---|
461 | |
---|
462 | inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝ |
---|
463 | | sp_normal : ∀fs,s1,s2. |
---|
464 | stack_of_state fs s1 → |
---|
465 | stack_of_state fs s2 → |
---|
466 | stack_preserved doesnt_end_with_ret s1 s2 |
---|
467 | | sp_finished : ∀s1,f,f',fs,m. |
---|
468 | next f = next f' → |
---|
469 | stack_of_state (f::fs) s1 → |
---|
470 | stack_preserved ends_with_ret s1 (State f' fs m). |
---|
471 | |
---|
472 | discriminator list. |
---|
473 | |
---|
474 | lemma stack_of_state_eq : ∀fs,fs',s. |
---|
475 | stack_of_state fs s → |
---|
476 | stack_of_state fs' s → |
---|
477 | fs = fs'. |
---|
478 | #fs0 #fs0' #s0 * |
---|
479 | [ #f #fs #m #H inversion H |
---|
480 | #a #b #c #d #e #g try #h try #i try #j destruct @refl |
---|
481 | | #fd #args #dst #f #fs #m #H inversion H |
---|
482 | #a #b #c #d #e #g try #h try #i try #j destruct @refl |
---|
483 | | #rtv #dst #fs #m #H inversion H |
---|
484 | #a #b #c #d #e #g try #h try #i try #j destruct @refl |
---|
485 | ] qed. |
---|
486 | |
---|
487 | lemma stack_preserved_join : ∀e,s1,s2,s3. |
---|
488 | stack_preserved doesnt_end_with_ret s1 s2 → |
---|
489 | stack_preserved e s2 s3 → |
---|
490 | stack_preserved e s1 s3. |
---|
491 | #e1 #s1 #s2 #s3 #H1 inversion H1 |
---|
492 | [ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct |
---|
493 | #H2 inversion H2 |
---|
494 | [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct |
---|
495 | @(sp_normal fs) // <(stack_of_state_eq … S1' S2) // |
---|
496 | | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct |
---|
497 | @(sp_finished … N) >(stack_of_state_eq … S1' S2) // |
---|
498 | ] |
---|
499 | | #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct |
---|
500 | ] qed. |
---|
501 | |
---|
502 | lemma stack_preserved_return : ∀ge,s1,s2,tr. |
---|
503 | RTLabs_classify s1 = cl_return → |
---|
504 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
505 | stack_preserved ends_with_ret s1 s2. |
---|
506 | #ge * |
---|
507 | [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?); |
---|
508 | cases (lookup_present ??? (next f) (next_ok f)) in E; |
---|
509 | normalize #a try #b try #c try #d try #e try #f try #g destruct |
---|
510 | | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct |
---|
511 | | #res #dst * |
---|
512 | [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct |
---|
513 | | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV |
---|
514 | whd in EV:(??%?); destruct @(sp_finished ? f) // |
---|
515 | ] |
---|
516 | ] qed. |
---|
517 | |
---|
518 | lemma stack_preserved_step : ∀ge,s1,s2,tr. |
---|
519 | RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump → |
---|
520 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
521 | stack_preserved doesnt_end_with_ret s1 s2. |
---|
522 | #ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV) |
---|
523 | [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/ |
---|
524 | | #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/ |
---|
525 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct |
---|
526 | normalize in CL; cases CL #E destruct |
---|
527 | | #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/ |
---|
528 | | #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL |
---|
529 | #E normalize in E; destruct |
---|
530 | ] qed. |
---|
531 | |
---|
532 | lemma stack_preserved_call : ∀ge,s1,s2,s3,tr. |
---|
533 | RTLabs_classify s1 = cl_call → |
---|
534 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
535 | stack_preserved ends_with_ret s2 s3 → |
---|
536 | stack_preserved doesnt_end_with_ret s1 s3. |
---|
537 | #ge #s1 #s2 #s3 #tr #CL #EV #SP |
---|
538 | cases (rtlabs_call_inv … CL) |
---|
539 | #fd * #args * #dst * #stk * #m #E destruct |
---|
540 | inversion SP |
---|
541 | [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct |
---|
542 | | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct |
---|
543 | inversion (eval_perserves … EV) |
---|
544 | [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct |
---|
545 | | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct |
---|
546 | | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct |
---|
547 | inversion S |
---|
548 | [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ |
---|
549 | | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct |
---|
550 | | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct |
---|
551 | ] |
---|
552 | | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct |
---|
553 | | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct |
---|
554 | ] |
---|
555 | ] qed. |
---|
556 | |
---|
557 | lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr. |
---|
558 | ∀CL : RTLabs_classify s1 = cl_call. |
---|
559 | eval_statement ge s1 = Value ??? 〈tr,s2〉 → |
---|
560 | stack_preserved ends_with_ret s2 s3 → |
---|
561 | as_after_return (RTLabs_status ge) «s1,CL» s3. |
---|
562 | #ge #s1 #s2 #s3 #tr #CL #EV #S23 |
---|
563 | cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct |
---|
564 | inversion S23 |
---|
565 | [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct |
---|
566 | | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct |
---|
567 | inversion (eval_perserves … EV) |
---|
568 | [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct |
---|
569 | | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct |
---|
570 | | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct |
---|
571 | inversion S |
---|
572 | [ #fy #fsy #my #E1 #E2 #E3 destruct @N |
---|
573 | | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct |
---|
574 | | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct |
---|
575 | ] |
---|
576 | | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct |
---|
577 | | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct |
---|
578 | ] |
---|
579 | ] qed. |
---|
580 | |
---|
581 | (* Don't need to know that labels break loops because we have termination. *) |
---|
582 | |
---|
583 | (* A bit of mucking around with the depth to avoid proving termination after |
---|
584 | termination. Note that we keep a proof that our upper bound on the length |
---|
585 | of the termination proof is respected. *) |
---|
586 | record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ { |
---|
587 | new_state : state; |
---|
588 | remainder : flat_trace io_out io_in ge new_state; |
---|
589 | cost_labelled : well_cost_labelled_state new_state; |
---|
590 | new_trace : T new_state; |
---|
591 | stack_ok : stack_preserved ends start new_state; |
---|
592 | terminates : match depth with |
---|
593 | [ O ⇒ True |
---|
594 | | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM |
---|
595 | ] |
---|
596 | }. |
---|
597 | |
---|
598 | (* The same with a flag indicating whether the function returned, as opposed to |
---|
599 | encountering a label. *) |
---|
600 | record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ { |
---|
601 | ends : trace_ends_with_ret; |
---|
602 | trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start (T ends) limit |
---|
603 | }. |
---|
604 | |
---|
605 | (* We often return the result from a recursive call with an addition to the |
---|
606 | structured trace, so we define a couple of functions to help. The bound on |
---|
607 | the size of the termination proof might need to be relaxed, too. *) |
---|
608 | |
---|
609 | definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → |
---|
610 | ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝ |
---|
611 | λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. |
---|
612 | mk_trace_result ge d e2 s2 T2 l2 |
---|
613 | (new_state … r) |
---|
614 | (remainder … r) |
---|
615 | (cost_labelled … r) |
---|
616 | trace |
---|
617 | SP |
---|
618 | (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → |
---|
619 | match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with |
---|
620 | [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r)) |
---|
621 | . @(transitive_le … lGE) @(pi2 … TM) qed. |
---|
622 | |
---|
623 | definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → |
---|
624 | ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝ |
---|
625 | λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. |
---|
626 | mk_sub_trace_result ge d s2 T2 l2 |
---|
627 | (ends … r) |
---|
628 | (replace_trace … lGE … r trace SP). |
---|
629 | |
---|
630 | (* Small syntax hack to avoid ambiguous input problems. *) |
---|
631 | definition myge : nat → nat → Prop ≝ ge. |
---|
632 | |
---|
633 | let rec make_label_return ge depth s |
---|
634 | (trace: flat_trace io_out io_in ge s) |
---|
635 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
636 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
637 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
638 | (TERMINATES: will_return ge depth s trace) |
---|
639 | (TIME: nat) |
---|
640 | (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) |
---|
641 | on TIME : trace_result ge depth ends_with_ret s |
---|
642 | (trace_label_return (RTLabs_status ge) s) |
---|
643 | (will_return_length … TERMINATES) ≝ |
---|
644 | |
---|
645 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
646 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
647 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
648 | |
---|
649 | let r ≝ make_label_label ge depth s |
---|
650 | trace |
---|
651 | ENV_COSTLABELLED |
---|
652 | STATE_COSTLABELLED |
---|
653 | STATEMENT_COSTLABEL |
---|
654 | TERMINATES |
---|
655 | TIME ? in |
---|
656 | match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with |
---|
657 | [ ends_with_ret ⇒ λr. |
---|
658 | replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r) |
---|
659 | | doesnt_end_with_ret ⇒ λr. |
---|
660 | let r' ≝ make_label_return ge depth (new_state … r) |
---|
661 | (remainder … r) |
---|
662 | ENV_COSTLABELLED |
---|
663 | (cost_labelled … r) ? |
---|
664 | (pi1 … (terminates … r)) TIME ? in |
---|
665 | replace_trace … r' |
---|
666 | (tlr_step (RTLabs_status ge) s (new_state … r) |
---|
667 | (new_state … r') (new_trace … r) (new_trace … r')) ? |
---|
668 | ] (trace_res … r) |
---|
669 | |
---|
670 | ] TERMINATES_IN_TIME |
---|
671 | |
---|
672 | |
---|
673 | and make_label_label ge depth s |
---|
674 | (trace: flat_trace io_out io_in ge s) |
---|
675 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
676 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
677 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
678 | (TERMINATES: will_return ge depth s trace) |
---|
679 | (TIME: nat) |
---|
680 | (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) |
---|
681 | on TIME : sub_trace_result ge depth s |
---|
682 | (λends. trace_label_label (RTLabs_status ge) ends s) |
---|
683 | (will_return_length … TERMINATES) ≝ |
---|
684 | |
---|
685 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
686 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
687 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
688 | |
---|
689 | let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in |
---|
690 | replace_sub_trace … r |
---|
691 | (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r) |
---|
692 | |
---|
693 | ] TERMINATES_IN_TIME |
---|
694 | |
---|
695 | |
---|
696 | and make_any_label ge depth s |
---|
697 | (trace: flat_trace io_out io_in ge s) |
---|
698 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
699 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
700 | (TERMINATES: will_return ge depth s trace) |
---|
701 | (TIME: nat) |
---|
702 | (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) |
---|
703 | on TIME : sub_trace_result ge depth s |
---|
704 | (λends. trace_any_label (RTLabs_status ge) ends s) |
---|
705 | (will_return_length … TERMINATES) ≝ |
---|
706 | |
---|
707 | match TIME return λTIME. TIME ≥ ? → ? with |
---|
708 | [ O ⇒ λTERMINATES_IN_TIME. ⊥ |
---|
709 | | S TIME ⇒ λTERMINATES_IN_TIME. |
---|
710 | |
---|
711 | match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with |
---|
712 | [ ft_stop st FINAL ⇒ |
---|
713 | λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ? |
---|
714 | |
---|
715 | | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. |
---|
716 | match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
717 | [ cl_other ⇒ λCL. |
---|
718 | match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
719 | (* We're about to run into a label. *) |
---|
720 | [ true ⇒ λCS. |
---|
721 | mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
722 | doesnt_end_with_ret |
---|
723 | (mk_trace_result ge … next trace' ? |
---|
724 | (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??) |
---|
725 | (* An ordinary step, keep going. *) |
---|
726 | | false ⇒ λCS. |
---|
727 | let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in |
---|
728 | replace_sub_trace … r |
---|
729 | (tal_step_default (RTLabs_status ge) (ends … r) |
---|
730 | start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ? |
---|
731 | ] (refl ??) |
---|
732 | |
---|
733 | | cl_jump ⇒ λCL. |
---|
734 | mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
735 | doesnt_end_with_ret |
---|
736 | (mk_trace_result ge ????? next trace' ? |
---|
737 | (tal_base_not_return (RTLabs_status ge) start next ???) ??) |
---|
738 | |
---|
739 | | cl_call ⇒ λCL. |
---|
740 | let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in |
---|
741 | match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with |
---|
742 | (* We're about to run into a label, use base case for call *) |
---|
743 | [ true ⇒ λCS. |
---|
744 | mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
745 | doesnt_end_with_ret |
---|
746 | (replace_trace … r |
---|
747 | (tal_base_call (RTLabs_status ge) start next (new_state … r) |
---|
748 | ? CL ? (new_trace … r) CS) ?) |
---|
749 | (* otherwise use step case *) |
---|
750 | | false ⇒ λCS. |
---|
751 | let r' ≝ make_any_label ge depth |
---|
752 | (new_state … r) (remainder … r) ENV_COSTLABELLED ? |
---|
753 | (pi1 … (terminates … r)) TIME ? in |
---|
754 | replace_sub_trace … r' |
---|
755 | (tal_step_call (RTLabs_status ge) (ends … r') |
---|
756 | start next (new_state … r) (new_state … r') ? CL ? |
---|
757 | (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? |
---|
758 | ] (refl ??) |
---|
759 | |
---|
760 | | cl_return ⇒ λCL. |
---|
761 | mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? |
---|
762 | ends_with_ret |
---|
763 | (mk_trace_result ge ????? |
---|
764 | next |
---|
765 | trace' |
---|
766 | ? |
---|
767 | (tal_base_return (RTLabs_status ge) start next ? CL) |
---|
768 | ? |
---|
769 | ?) |
---|
770 | ] (refl ? (RTLabs_classify start)) |
---|
771 | |
---|
772 | | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ |
---|
773 | |
---|
774 | ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME |
---|
775 | ] TERMINATES_IN_TIME. |
---|
776 | |
---|
777 | [ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] |
---|
778 | | // |
---|
779 | | cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le |
---|
780 | | @(stack_preserved_join … (stack_ok … r)) // |
---|
781 | | @(trace_label_label_label … (new_trace … r)) |
---|
782 | | cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT |
---|
783 | @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) |
---|
784 | @(transitive_le … (3*(will_return_length … TERMINATES))) |
---|
785 | [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times |
---|
786 | @(monotonic_le_times_r 3 … LT) |
---|
787 | | @le_S @le_S @le_n |
---|
788 | ] |
---|
789 | | @le_S_S_to_le @TERMINATES_IN_TIME |
---|
790 | | cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] |
---|
791 | | @le_n |
---|
792 | | @le_S_S_to_le @TERMINATES_IN_TIME |
---|
793 | | @(wrl_nonzero … TERMINATES_IN_TIME) |
---|
794 | | (* Bad - we've reached the end of the trace; need to fix semantics so that |
---|
795 | this can't happen *) |
---|
796 | | @(will_return_return … CL TERMINATES) |
---|
797 | | /2 by stack_preserved_return/ |
---|
798 | | %{tr} @EV |
---|
799 | | @(well_cost_labelled_state_step … EV) // |
---|
800 | | whd @(will_return_notfn … TERMINATES) %2 @CL |
---|
801 | | @stack_preserved_step /2/ |
---|
802 | | %{tr} @EV |
---|
803 | | %1 whd @CL |
---|
804 | | @(well_cost_labelled_jump … EV) // |
---|
805 | | @(well_cost_labelled_state_step … EV) // |
---|
806 | | @(stack_preserved_call … EV (stack_ok … r)) // |
---|
807 | | %{tr} @EV |
---|
808 | | @RTLabs_after_call // |
---|
809 | | cases (will_return_call … TERMINATES) #H @le_S_to_le |
---|
810 | | cases r #H1 #H2 #H3 #H4 #H5 * #H6 |
---|
811 | cases (will_return_call … CL TERMINATES) |
---|
812 | #TM #X #Y @le_S_to_le @(transitive_lt … Y X) |
---|
813 | | @RTLabs_after_call // |
---|
814 | | %{tr} @EV |
---|
815 | | @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // |
---|
816 | | @(cost_labelled … r) |
---|
817 | | cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78 |
---|
818 | @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) |
---|
819 | cases (will_return_call … TERMINATES) in H78; |
---|
820 | #X #Y #Z |
---|
821 | @(transitive_le … (monotonic_lt_times_r 3 … Y)) |
---|
822 | [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) // |
---|
823 | | // |
---|
824 | ] |
---|
825 | | @(well_cost_labelled_state_step … EV) // |
---|
826 | | @(well_cost_labelled_call … EV) // |
---|
827 | | skip |
---|
828 | | cases (will_return_call … TERMINATES) |
---|
829 | #TM #GT @le_S_S_to_le |
---|
830 | >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times |
---|
831 | @(transitive_le … TERMINATES_IN_TIME) |
---|
832 | @(monotonic_le_times_r 3 … GT) |
---|
833 | | whd @(will_return_notfn … TERMINATES) %1 @CL |
---|
834 | | @(stack_preserved_step … EV) /2/ |
---|
835 | | %{tr} @EV |
---|
836 | | %2 whd @CL |
---|
837 | | @(well_cost_labelled_state_step … EV) // |
---|
838 | | cases (will_return_notfn … TERMINATES) #TM @le_S_to_le |
---|
839 | | @CL |
---|
840 | | %{tr} @EV |
---|
841 | | @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/ |
---|
842 | | @(well_cost_labelled_state_step … EV) // |
---|
843 | | %1 @CL |
---|
844 | | cases (will_return_notfn … TERMINATES) #TM #GT |
---|
845 | @le_S_S_to_le |
---|
846 | @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME) |
---|
847 | // |
---|
848 | | inversion TERMINATES |
---|
849 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct |
---|
850 | | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct |
---|
851 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct |
---|
852 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct |
---|
853 | ] |
---|
854 | ] cases daemon qed. |
---|
855 | |
---|
856 | (* We can initialise TIME with a suitably large value based on the length of the |
---|
857 | termination proof. *) |
---|
858 | let rec make_label_return' ge depth s |
---|
859 | (trace: flat_trace io_out io_in ge s) |
---|
860 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
861 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
862 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
863 | (TERMINATES: will_return ge depth s trace) |
---|
864 | : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ |
---|
865 | make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES |
---|
866 | (2 + 3 * will_return_length … TERMINATES) ?. |
---|
867 | @le_n |
---|
868 | qed. |
---|
869 | |
---|
870 | (* FIXME: there's trouble at the end of the program because we can't make a step |
---|
871 | away from the final return. |
---|
872 | |
---|
873 | We need to show that the "next pc" is preserved through a function call. |
---|
874 | |
---|
875 | Tail-calls are not handled properly (which means that if we try to show the |
---|
876 | full version with non-termination we'll fail because calls and returns aren't |
---|
877 | balanced. |
---|
878 | *) |
---|
879 | |
---|
880 | inductive inhabited (T:Type[0]) : Prop ≝ |
---|
881 | | witness : T → inhabited T. |
---|
882 | |
---|
883 | (* We also require that program's traces are soundly labelled: for any state |
---|
884 | in the execution, we can give a distance to a labelled state or termination. |
---|
885 | |
---|
886 | Note that this differs from the syntactic notions in earlier languages |
---|
887 | because it is a global property. In principle, we would have a loop broken |
---|
888 | only by a call to a function (which necessarily has a label) and no local |
---|
889 | cost label. |
---|
890 | *) |
---|
891 | |
---|
892 | let rec nth_state ge s |
---|
893 | (trace: flat_trace io_out io_in ge s) |
---|
894 | n |
---|
895 | on n : option state ≝ |
---|
896 | match n with |
---|
897 | [ O ⇒ Some ? s |
---|
898 | | S n' ⇒ |
---|
899 | match trace with |
---|
900 | [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n' |
---|
901 | | _ ⇒ None ? |
---|
902 | ] |
---|
903 | ]. |
---|
904 | |
---|
905 | definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝ |
---|
906 | λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true. |
---|
907 | |
---|
908 | lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'. |
---|
909 | soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') → |
---|
910 | soundly_labelled_trace ge s' trace'. |
---|
911 | #ge #s #tr #s' #EV #trace' #H |
---|
912 | #n cases (H (S n)) #m #H' %{m} @H' |
---|
913 | qed. |
---|
914 | |
---|
915 | (* Define a notion of sound labellings of RTLabs programs. *) |
---|
916 | |
---|
917 | let rec successors (s : statement) : list label ≝ |
---|
918 | match s with |
---|
919 | [ St_skip l ⇒ [l] |
---|
920 | | St_cost _ l ⇒ [l] |
---|
921 | | St_const _ _ l ⇒ [l] |
---|
922 | | St_op1 _ _ _ _ _ l ⇒ [l] |
---|
923 | | St_op2 _ _ _ _ l ⇒ [l] |
---|
924 | | St_load _ _ _ l ⇒ [l] |
---|
925 | | St_store _ _ _ l ⇒ [l] |
---|
926 | | St_call_id _ _ _ l ⇒ [l] |
---|
927 | | St_call_ptr _ _ _ l ⇒ [l] |
---|
928 | (* |
---|
929 | | St_tailcall_id _ _ ⇒ [ ] |
---|
930 | | St_tailcall_ptr _ _ ⇒ [ ] |
---|
931 | *) |
---|
932 | | St_cond _ l1 l2 ⇒ [l1; l2] |
---|
933 | | St_jumptable _ ls ⇒ ls |
---|
934 | | St_return ⇒ [ ] |
---|
935 | ]. |
---|
936 | |
---|
937 | definition actual_successor : state → option label ≝ |
---|
938 | λs. match s with |
---|
939 | [ State f fs m ⇒ Some ? (next f) |
---|
940 | | Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ] |
---|
941 | | Returnstate _ _ _ _ ⇒ None ? |
---|
942 | ]. |
---|
943 | |
---|
944 | lemma nth_opt_Exists : ∀A,n,l,a. |
---|
945 | nth_opt A n l = Some A a → |
---|
946 | Exists A (λa'. a' = a) l. |
---|
947 | #A #n elim n |
---|
948 | [ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ] |
---|
949 | | #m #IH * |
---|
950 | [ #a #E normalize in E; destruct |
---|
951 | | #a #l #a' #E %2 @IH @E |
---|
952 | ] |
---|
953 | ] qed. |
---|
954 | |
---|
955 | lemma eval_successor : ∀ge,f,fs,m,tr,s'. |
---|
956 | eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → |
---|
957 | RTLabs_classify s' = cl_return ∨ |
---|
958 | ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))). |
---|
959 | #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' |
---|
960 | whd in ⊢ (??%? → ?); |
---|
961 | generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) |
---|
962 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
963 | | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
964 | | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
965 | | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
966 | | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
967 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
968 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
969 | | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
970 | | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // |
---|
971 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] // |
---|
972 | | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev |
---|
973 | cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] |
---|
974 | whd in ⊢ (??%? → ?); |
---|
975 | generalize in ⊢ (??(?%)? → ?); |
---|
976 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?); |
---|
977 | [ #e #E normalize in E; destruct |
---|
978 | | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) |
---|
979 | ] |
---|
980 | | #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl |
---|
981 | ] qed. |
---|
982 | |
---|
983 | definition steps_for_statement : statement → nat ≝ |
---|
984 | λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]). |
---|
985 | |
---|
986 | inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ |
---|
987 | | stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n) |
---|
988 | | stlb_step : ∀l,n,H. |
---|
989 | let stmt ≝ lookup_present … g l H in |
---|
990 | (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) → |
---|
991 | steps_to_label_bound g l (steps_for_statement stmt + n). |
---|
992 | |
---|
993 | discriminator nat. |
---|
994 | |
---|
995 | lemma steps_to_label_bound_inv_step : ∀g,l,n. |
---|
996 | steps_to_label_bound g l n → |
---|
997 | ∀H. |
---|
998 | let stmt ≝ lookup_present … g l H in |
---|
999 | ¬ (bool_to_Prop (is_cost_label stmt)) → |
---|
1000 | (∀l'. Exists label (λl0. l0 = l') (successors stmt) → |
---|
1001 | ∃n'. n = n' + steps_for_statement stmt ∧ |
---|
1002 | steps_to_label_bound g l' n'). |
---|
1003 | #g #l0 #n0 #H1 inversion H1 |
---|
1004 | [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4) |
---|
1005 | | #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX |
---|
1006 | % [2: % [ @commutative_plus | @IH // ] ] |
---|
1007 | ] qed. |
---|
1008 | |
---|
1009 | definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. |
---|
1010 | |
---|
1011 | let rec soundly_labelled_fn (fn : internal_function) : Prop ≝ |
---|
1012 | soundly_labelled_pc (f_graph fn) (f_entry fn). |
---|
1013 | |
---|
1014 | |
---|
1015 | definition soundly_labelled_frame : frame → Prop ≝ |
---|
1016 | λf. soundly_labelled_pc (f_graph (func f)) (next f). |
---|
1017 | |
---|
1018 | definition soundly_labelled_state : state → Prop ≝ |
---|
1019 | λs. match s with |
---|
1020 | [ State f _ _ ⇒ soundly_labelled_frame f |
---|
1021 | | Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] |
---|
1022 | | Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] |
---|
1023 | ]. |
---|
1024 | |
---|
1025 | definition frame_steps_to_label_bound : frame → nat → Prop ≝ |
---|
1026 | λf. steps_to_label_bound (f_graph (func f)) (next f). |
---|
1027 | |
---|
1028 | inductive state_steps_to_label_bound : state → nat → Prop ≝ |
---|
1029 | | sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n |
---|
1030 | | sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n) |
---|
1031 | | sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n) |
---|
1032 | . |
---|
1033 | |
---|
1034 | lemma state_steps_to_label_bound_zero : ∀s. |
---|
1035 | ¬ state_steps_to_label_bound s O. |
---|
1036 | #s % #H inversion H |
---|
1037 | [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct |
---|
1038 | inversion H52 |
---|
1039 | [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct |
---|
1040 | | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct |
---|
1041 | ] |
---|
1042 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct |
---|
1043 | | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct |
---|
1044 | ] qed. |
---|
1045 | |
---|
1046 | lemma eval_steps : ∀ge,f,fs,m,tr,s'. |
---|
1047 | eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → |
---|
1048 | steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) = |
---|
1049 | match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 ]. |
---|
1050 | #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' |
---|
1051 | whd in ⊢ (??%? → ?); |
---|
1052 | generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) |
---|
1053 | [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1054 | | #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1055 | | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1056 | | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1057 | | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1058 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1059 | | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1060 | | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1061 | | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1062 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1063 | | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev |
---|
1064 | cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ] |
---|
1065 | whd in ⊢ (??%? → ?); |
---|
1066 | generalize in ⊢ (??(?%)? → ?); |
---|
1067 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?); |
---|
1068 | [ #e #E normalize in E; destruct |
---|
1069 | | #l #El whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1070 | ] |
---|
1071 | | #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl |
---|
1072 | ] qed. |
---|
1073 | |
---|
1074 | lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n. |
---|
1075 | state_steps_to_label_bound s (S n) → |
---|
1076 | eval_statement ge s = Value ??? 〈tr, s'〉 → |
---|
1077 | RTLabs_cost s = false → |
---|
1078 | (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ |
---|
1079 | state_steps_to_label_bound s' n. |
---|
1080 | #ge #s #tr #s' #n #STEPS inversion STEPS |
---|
1081 | [ #f #fs #m #m #FS #E1 #E2 #_ destruct |
---|
1082 | #EVAL cases (eval_successor … EVAL) |
---|
1083 | [ /3/ |
---|
1084 | | * #l * #S1 #S2 #NC %2 |
---|
1085 | cases (steps_to_label_bound_inv_step … FS … l S2) |
---|
1086 | [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ] |
---|
1087 | #n' |
---|
1088 | inversion (eval_perserves … EVAL) |
---|
1089 | [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct |
---|
1090 | >(eval_steps … EVAL) * >commutative_plus #En normalize in En; |
---|
1091 | whd in S1:(??%?); |
---|
1092 | #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct |
---|
1093 | %1 @H |
---|
1094 | | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct |
---|
1095 | >(eval_steps … EVAL) * >commutative_plus #En normalize in En; |
---|
1096 | whd in S1:(??%?); |
---|
1097 | #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct |
---|
1098 | %2 // |
---|
1099 | | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 |
---|
1100 | destruct |
---|
1101 | | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct |
---|
1102 | normalize in S1; destruct |
---|
1103 | | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct |
---|
1104 | ] |
---|
1105 | ] |
---|
1106 | | #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct |
---|
1107 | /3/ |
---|
1108 | | #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct |
---|
1109 | #EVAL #NC %2 inversion (eval_perserves … EVAL) |
---|
1110 | [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct |
---|
1111 | | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct |
---|
1112 | | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct |
---|
1113 | | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct |
---|
1114 | | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct |
---|
1115 | %1 whd in FS ⊢ %; |
---|
1116 | inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ] |
---|
1117 | #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE |
---|
1118 | inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ] |
---|
1119 | inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct |
---|
1120 | @FS |
---|
1121 | ] |
---|
1122 | ] qed. |
---|
1123 | |
---|
1124 | |
---|
1125 | (* |
---|
1126 | lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'. |
---|
1127 | state_steps_to_label_bound (State f fs m) (S (S n)) → |
---|
1128 | ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) → |
---|
1129 | eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → |
---|
1130 | state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]). |
---|
1131 | #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H |
---|
1132 | [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct |
---|
1133 | cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ] |
---|
1134 | #NC whd in ⊢ (??%? → ?); |
---|
1135 | generalize in ⊢ (??(?%)? → ?); |
---|
1136 | lapply (steps_to_label_bound_inv_step … H1 next_ok NC) |
---|
1137 | cases (lookup_present ??? next next_ok) |
---|
1138 | [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl |
---|
1139 | | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl |
---|
1140 | | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl |
---|
1141 | | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl |
---|
1142 | | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl |
---|
1143 | | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl |
---|
1144 | | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl |
---|
1145 | | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl |
---|
1146 | | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl |
---|
1147 | | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl |
---|
1148 | | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] |
---|
1149 | | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % |
---|
1150 | | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ] |
---|
1151 | | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 |
---|
1152 | ] |
---|
1153 | *) |
---|
1154 | (* When constructing an infinite trace, we need to be able to grab the finite |
---|
1155 | portion of the trace for the next [trace_label_diverges] constructor. We |
---|
1156 | use the fact that the trace is soundly labelled to achieve this. *) |
---|
1157 | |
---|
1158 | inductive finite_prefix (ge:genv) : state → Prop ≝ |
---|
1159 | | fp_tal : ∀s,s'. |
---|
1160 | trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → |
---|
1161 | flat_trace io_out io_in ge s' → |
---|
1162 | finite_prefix ge s |
---|
1163 | | fp_tac : ∀s,s'. |
---|
1164 | trace_any_call (RTLabs_status ge) s s' → |
---|
1165 | flat_trace io_out io_in ge s' → |
---|
1166 | finite_prefix ge s |
---|
1167 | . |
---|
1168 | |
---|
1169 | definition fp_add_default : ∀ge,s,s'. |
---|
1170 | RTLabs_classify s = cl_other → |
---|
1171 | finite_prefix ge s' → |
---|
1172 | (∃t. eval_statement ge s = Value ??? 〈t,s'〉) → |
---|
1173 | RTLabs_cost s' = false → |
---|
1174 | finite_prefix ge s ≝ |
---|
1175 | λge,s,s',OTHER,fp. |
---|
1176 | match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with |
---|
1177 | [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf |
---|
1178 | (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) |
---|
1179 | rem |
---|
1180 | | fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf |
---|
1181 | (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem |
---|
1182 | ]. |
---|
1183 | |
---|
1184 | definition fp_add_terminating_call : ∀ge,s,s1,s'. |
---|
1185 | (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → |
---|
1186 | ∀CALL:RTLabs_classify s = cl_call. |
---|
1187 | finite_prefix ge s' → |
---|
1188 | trace_label_return (RTLabs_status ge) s1 s' → |
---|
1189 | as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' → |
---|
1190 | RTLabs_cost s' = false → |
---|
1191 | finite_prefix ge s ≝ |
---|
1192 | λge,s,s1,s',EVAL,CALL,fp. |
---|
1193 | match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with |
---|
1194 | [ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf |
---|
1195 | (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) |
---|
1196 | rem |
---|
1197 | | fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf |
---|
1198 | (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) |
---|
1199 | rem |
---|
1200 | ]. |
---|
1201 | |
---|
1202 | definition termination_oracle ≝ ∀ge,depth,s,trace. |
---|
1203 | inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). |
---|
1204 | |
---|
1205 | let rec finite_segment ge s n trace |
---|
1206 | (ORACLE: termination_oracle) |
---|
1207 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
1208 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
1209 | (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) |
---|
1210 | (LABEL_LIMIT: state_steps_to_label_bound s n) |
---|
1211 | on n : finite_prefix ge s ≝ |
---|
1212 | match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with |
---|
1213 | [ O ⇒ λLABEL_LIMIT. ⊥ |
---|
1214 | | S n' ⇒ |
---|
1215 | match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with |
---|
1216 | [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ |
---|
1217 | | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. |
---|
1218 | match RTLabs_classify start return λx. RTLabs_classify start = x → ? with |
---|
1219 | [ cl_other ⇒ λCL. |
---|
1220 | match RTLabs_cost next return λx. RTLabs_cost next = x → ? with |
---|
1221 | [ true ⇒ λCS. |
---|
1222 | fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' |
---|
1223 | | false ⇒ λCS. |
---|
1224 | let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in |
---|
1225 | fp_add_default ge ?? CL fs ? CS |
---|
1226 | ] (refl ??) |
---|
1227 | | cl_jump ⇒ λCL. |
---|
1228 | fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' |
---|
1229 | | cl_call ⇒ λCL.?(* |
---|
1230 | match ORACLE ge O next trace' return λ_. finite_prefix ge start with |
---|
1231 | [ or_introl TERMINATES ⇒ |
---|
1232 | match TERMINATES with [ witness TERMINATES ⇒ |
---|
1233 | let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in |
---|
1234 | match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with |
---|
1235 | [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) |
---|
1236 | | false ⇒ λCS. ? (* broken - we don't know the new value of n *) |
---|
1237 | (*let fs ≝ finite_segment ge (new_status … tlr) ?????????????? |
---|
1238 | fp_add_terminating_call … (new_trace … tlr) ? CS*) |
---|
1239 | ] (refl ??) |
---|
1240 | ] |
---|
1241 | | or_intror NO_TERMINATION ⇒ |
---|
1242 | fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') |
---|
1243 | ]*) |
---|
1244 | | cl_return ⇒ λCL. ⊥ |
---|
1245 | ] (refl ??) |
---|
1246 | | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ |
---|
1247 | ] STATE_COSTLABELLED NO_TERMINATION |
---|
1248 | ] LABEL_LIMIT. |
---|
1249 | [ cases (state_steps_to_label_bound_zero s) /2/ |
---|
1250 | | (* TODO: how do we know that we're not at the final state? *) |
---|
1251 | | @(absurd ?? NO_TERMINATION) |
---|
1252 | %{0} % @wr_base // |
---|
1253 | | @(well_cost_labelled_jump … EV) // |
---|
1254 | | 5,6,8,9,10: /2/ |
---|
1255 | | |
---|
1256 | | @(well_cost_labelled_state_step … EV) // |
---|
1257 | | @(not_to_not … NO_TERMINATION) |
---|
1258 | * #depth * #TERM %{depth} % @wr_step /2/ |
---|
1259 | | cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?) |
---|
1260 | |
---|
1261 | @(well_cost_labelled_call … EV) // |
---|
1262 | | |
---|
1263 | 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct |
---|
1264 | | 5,6,8: /2/ |
---|
1265 | | |
---|
1266 | |*) |
---|
1267 | | 12,13,14: /2/ |
---|
1268 | | @(well_cost_labelled_state_step … EV) // |
---|
1269 | | @(not_to_not … NO_TERMINATION) |
---|
1270 | * #depth * #TERM %{depth} % @wr_step /2/ |
---|
1271 | ] cases daemon qed. |
---|
1272 | |
---|
1273 | (* |
---|
1274 | let corec make_label_diverges ge s |
---|
1275 | (trace: flat_trace io_out io_in ge s) |
---|
1276 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
1277 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
1278 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
1279 | (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace) |
---|
1280 | (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) |
---|
1281 | : trace_label_diverges (RTLabs_status ge) s ≝ ? |
---|
1282 | . |
---|
1283 | *) |
---|