source: src/RTLabs/Traces.ma @ 1765

Last change on this file since 1765 was 1765, checked in by campbell, 8 years ago

Rule out final states in non-terminating executions chunks (RTLabs
structured trace).

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