source: src/RTLabs/Traces.ma @ 1808

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

Create a Prop version of the non-terminating structured traces so that
I can at least show existence.

File size: 76.8 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
429lemma will_return_lower : ∀ge,d,s,t.
430  will_return ge d s t →
431  ∀d'. d' ≤ d →
432  will_return ge d' s t.
433#ge #d0 #s0 #t0 #TM elim TM
434[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
435| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
436| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
437  [ #LE @wr_base //
438  | #d' #LE %3 // @IH /2/
439  ]
440| #s #tr #s' #EX #tr #CL *
441  [ #_ @wr_base //
442  | #d' #LE @⊥ /2/
443  ]
444] qed.
445
446(* We require that labels appear after branch instructions and at the start of
447   functions.  The first is required for preciseness, the latter for soundness.
448   We will make a separate requirement for there to be a finite number of steps
449   between labels to catch loops for soundness (is this sufficient?). *)
450
451definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
452λf,s. match s return λs. labels_present ? s → Prop with
453[ St_cond _ l1 l2 ⇒ λH.
454    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
455    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
456| St_jumptable _ ls ⇒ λH.
457    (* I did have a dependent version of All here, but it's a pain. *)
458    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
459| _ ⇒ λ_. True
460]. whd in H;
461[ @(proj1 … H)
462| @(proj2 … H)
463] qed.
464
465definition well_cost_labelled_fn : internal_function → Prop ≝
466λf. (∀l. ∀H:present … (f_graph f) l.
467         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
468    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
469[ @lookup_lookup_present | cases (f_entry f) // ] qed.
470
471(* We need to ensure that any code we come across is well-cost-labelled.  We may
472   get function code from either the global environment or the state. *)
473
474definition well_cost_labelled_ge : genv → Prop ≝
475λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
476
477definition well_cost_labelled_state : state → Prop ≝
478λs. match s with
479[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
480| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
481                          All ? (λf. well_cost_labelled_fn (func f)) fs
482| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
483| Finalstate _ ⇒ True
484].
485
486lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
487  eval_statement ge s = Value ??? 〈tr,s'〉 →
488  well_cost_labelled_ge ge →
489  well_cost_labelled_state s →
490  well_cost_labelled_state s'.
491#ge #s #tr' #s' #EV cases (eval_perserves … EV)
492[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
493| #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/
494(*
495| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
496*)
497| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
498| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
499| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
500| //
501] qed.
502
503lemma rtlabs_jump_inv : ∀s.
504  RTLabs_classify s = cl_jump →
505  ∃f,fs,m. s = State f fs m ∧
506  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
507  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
508*
509[ #f #fs #m #E
510  %{f} %{fs} %{m} %
511  [ @refl
512  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
513    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
514    [ %1 %{A} %{B} %{C} @refl
515    | %2 %{A} %{B} @refl
516    ]
517  ]
518| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
519| normalize #H8 #H9 #H10 #H11 #H12 destruct
520| #r #E normalize in E; destruct
521] qed.
522
523lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
524  eval_statement ge s = Value ??? 〈tr,s'〉 →
525  well_cost_labelled_state s →
526  RTLabs_classify s = cl_jump →
527  RTLabs_cost s' = true.
528#ge #s #tr #s' #EV #H #CL
529cases (rtlabs_jump_inv s CL)
530#fr * #fs * #m * #Es *
531[ * #r * #l1 * #l2 #Estmt
532  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
533  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
534  >Estmt #LP whd in ⊢ (??%? → ?);
535  (* replace with lemma on successors? *)
536  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
537  lapply (Hbody (next fr) (next_ok fr))
538  generalize in ⊢ (???% → ?);
539  >Estmt #LP'
540  whd in ⊢ (% → ?);
541  * #H1 #H2 [ @H1 | @H2 ]
542| * #r * #ls #Estmt
543  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
544  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
545  >Estmt #LP whd in ⊢ (??%? → ?);
546  (* replace with lemma on successors? *)
547  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
548  [ 2: (* later *)
549  | *: #E destruct
550  ]
551  lapply (Hbody (next fr) (next_ok fr))
552  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
553  generalize in ⊢ (??(?%)? → ?);
554  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
555  [ #E1 #E2 whd in E2:(??%?); destruct
556  | #l' #E1 #E2 whd in E2:(??%?); destruct
557    cases (All_nth ???? CP ? E1)
558    #H1 #H2 @H2
559  ]
560] qed.
561
562lemma rtlabs_call_inv : ∀s.
563  RTLabs_classify s = cl_call →
564  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
565* [ #f #fs #m whd in ⊢ (??%? → ?);
566    cases (lookup_present … (next f) (next_ok f)) normalize
567    try #A try #B try #C try #D try #E try #F try #G destruct
568  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
569  | normalize #H411 #H412 #H413 #H414 #H415 destruct
570  | normalize #H1 #H2 destruct
571  ] qed.
572
573lemma well_cost_labelled_call : ∀ge,s,tr,s'.
574  eval_statement ge s = Value ??? 〈tr,s'〉 →
575  well_cost_labelled_state s →
576  RTLabs_classify s = cl_call →
577  RTLabs_cost s' = true.
578#ge #s #tr #s' #EV #WCL #CL
579cases (rtlabs_call_inv s CL)
580#fd * #args * #dst * #stk * #m #E >E in EV WCL;
581whd in ⊢ (??%? → % → ?);
582cases fd
583[ #fn whd in ⊢ (??%? → % → ?);
584  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
585  #m' #b whd in ⊢ (??%? → ?); #E' destruct
586  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
587  @WCL2
588| #fn whd in ⊢ (??%? → % → ?);
589  @bindIO_value #evargs #Eargs
590  whd in ⊢ (??%? → ?);
591  #E' destruct
592] qed.
593
594
595(* The preservation of (most of) the stack is useful to show as_after_return.
596   We do this by showing that during the execution of a function the lower stack
597   frames never change, and that after returning from the function we preserve
598   the identity of the next instruction to execute.
599 *)
600
601inductive stack_of_state : list frame → state → Prop ≝
602| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
603| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
604| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
605.
606
607inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
608| sp_normal : ∀fs,s1,s2.
609    stack_of_state fs s1 →
610    stack_of_state fs s2 →
611    stack_preserved doesnt_end_with_ret s1 s2
612| sp_finished : ∀s1,f,f',fs,m.
613    next f = next f' →
614    frame_rel f f' →
615    stack_of_state (f::fs) s1 →
616    stack_preserved ends_with_ret s1 (State f' fs m)
617| sp_stop : ∀s1,r.
618    stack_of_state [ ] s1 →
619    stack_preserved ends_with_ret s1 (Finalstate r)
620| sp_top : ∀fd,args,dst,m,r.
621    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
622.
623
624discriminator list.
625
626lemma stack_of_state_eq : ∀fs,fs',s.
627  stack_of_state fs s →
628  stack_of_state fs' s →
629  fs = fs'.
630#fs0 #fs0' #s0 *
631[ #f #fs #m #H inversion H
632  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
633| #fd #args #dst #f #fs #m #H inversion H
634  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
635| #rtv #dst #fs #m #H inversion H
636  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
637] qed.
638
639lemma stack_preserved_final : ∀e,r,s.
640  ¬stack_preserved e (Finalstate r) s.
641#e #r #s % #H inversion H
642[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
643  inversion SOS #a #b #c #d #e #f try #g try #h destruct
644| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
645  inversion SOS #a #b #c #d #e #f try #g try #h destruct
646| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
647  inversion SOS #a #b #c #d #e #f try #g try #h destruct
648| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
649] qed.
650
651lemma stack_preserved_join : ∀e,s1,s2,s3.
652  stack_preserved doesnt_end_with_ret s1 s2 →
653  stack_preserved e s2 s3 →
654  stack_preserved e s1 s3.
655#e1 #s1 #s2 #s3 #H1 inversion H1
656[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
657  #H2 inversion H2
658  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
659    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
660  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
661    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
662  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
663  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
664    inversion S2
665    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
666    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
667    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
668    ]
669  ]
670| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
671| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
672  cases (stack_preserved_final … H) #r #E destruct
673| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
674  @(absurd … F) //
675] qed.
676
677lemma stack_preserved_return : ∀ge,s1,s2,tr.
678  RTLabs_classify s1 = cl_return →
679  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
680  stack_preserved ends_with_ret s1 s2.
681#ge *
682[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
683  cases (lookup_present ??? (next f) (next_ok f)) in E;
684  normalize #a try #b try #c try #d try #e try #f try #g destruct
685| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
686| #res #dst *
687  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
688    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
689  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
690    whd in EV:(??%?); destruct @(sp_finished ? f) //
691    cases f //
692  ]
693| #r #s2 #tr #E normalize in E; destruct
694] qed.
695
696lemma stack_preserved_step : ∀ge,s1,s2,tr.
697  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
698  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
699  stack_preserved doesnt_end_with_ret s1 s2.
700#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
701[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
702| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
703| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
704  normalize in CL; cases CL #E destruct
705| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
706| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
707  #E normalize in E; destruct
708| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
709] qed.
710
711lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
712  RTLabs_classify s1 = cl_call →
713  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
714  stack_preserved ends_with_ret s2 s3 →
715  stack_preserved doesnt_end_with_ret s1 s3.
716#ge #s1 #s2 #s3 #tr #CL #EV #SP
717cases (rtlabs_call_inv … CL)
718#fd * #args * #dst * #stk * #m #E destruct
719inversion SP
720[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
721| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
722  inversion (eval_perserves … EV)
723  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
724  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
725  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
726    inversion S
727    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
728    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
729    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
730    ]
731  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
732  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
733  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
734  ]
735| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
736  inversion (eval_perserves … EV)
737  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
738  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
739  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
740    inversion S1
741    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
742    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
743    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
744    ]
745  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
746  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
747  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
748  ]
749| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
750] qed.
751 
752lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
753  ∀CL : RTLabs_classify s1 = cl_call.
754  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
755  stack_preserved ends_with_ret s2 s3 →
756  as_after_return (RTLabs_status ge) «s1,CL» s3.
757#ge #s1 #s2 #s3 #tr #CL #EV #S23
758cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
759inversion S23
760[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
761| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
762  inversion (eval_perserves … EV)
763  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
764  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
765  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
766    inversion S
767    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
768    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
769    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
770    ]
771  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
772  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
773  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
774  ]
775| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
776  inversion (eval_perserves … EV)
777  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
778  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
779  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
780    inversion S1
781    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
782    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
783    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
784    ]
785  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
786  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
787  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
788  ]
789| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
790] qed.
791
792(* Don't need to know that labels break loops because we have termination. *)
793
794(* A bit of mucking around with the depth to avoid proving termination after
795   termination.  Note that we keep a proof that our upper bound on the length
796   of the termination proof is respected. *)
797record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
798  (start:state) (full:flat_trace io_out io_in ge start)
799  (original_terminates: will_return ge depth start full)
800  (T:state → Type[0]) (limit:nat) : Type[0] ≝
801{
802  new_state : state;
803  remainder : flat_trace io_out io_in ge new_state;
804  cost_labelled : well_cost_labelled_state new_state;
805  new_trace : T new_state;
806  stack_ok : stack_preserved ends start new_state;
807  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
808               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
809               | S d ⇒ ΣTM:will_return ge d new_state remainder.
810                         limit > will_return_length … TM ∧
811                         will_return_end … original_terminates = will_return_end … TM
812               ]
813}.
814
815(* The same with a flag indicating whether the function returned, as opposed to
816   encountering a label. *)
817record sub_trace_result (ge:genv) (depth:nat)
818  (start:state) (full:flat_trace io_out io_in ge start)
819  (original_terminates: will_return ge depth start full)
820  (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
821{
822  ends : trace_ends_with_ret;
823  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
824}.
825
826(* We often return the result from a recursive call with an addition to the
827   structured trace, so we define a couple of functions to help.  The bound on
828   the size of the termination proof might need to be relaxed, too. *)
829
830definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
831  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
832    will_return_end … TM1 = will_return_end … TM2 →
833    T2 (new_state … r) →
834    stack_preserved e s2 (new_state … r) →
835    trace_result ge d e s2 t2 TM2 T2 l2 ≝
836λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
837  mk_trace_result ge d e s2 t2 TM2 T2 l2
838    (new_state … r)
839    (remainder … r)
840    (cost_labelled … r)
841    trace
842    SP
843    ?
844    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
845                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
846     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
847.
848cases e in r ⊢ %;
849[ <TME -TME * cases d in TM1 TM2 ⊢ %;
850  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
851  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
852    %{TMa} % // @(transitive_le … lGE) @L1
853  ]
854| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
855   * #TMa * #L1 #TME
856    %{TMa} % // @(transitive_le … lGE) @L1
857] qed.
858
859definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
860  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
861    will_return_end … TM1 = will_return_end … TM2 →
862    T2 (ends … r) (new_state … r) →
863    stack_preserved (ends … r) s2 (new_state … r) →
864    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
865λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
866  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
867    (ends … r)
868    (replace_trace … lGE … r TME trace SP).
869
870(* Small syntax hack to avoid ambiguous input problems. *)
871definition myge : nat → nat → Prop ≝ ge.
872
873let rec make_label_return ge depth s
874  (trace: flat_trace io_out io_in ge s)
875  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
876  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
877  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
878  (TERMINATES: will_return ge depth s trace)
879  (TIME: nat)
880  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
881  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
882              (trace_label_return (RTLabs_status ge) s)
883              (will_return_length … TERMINATES) ≝
884             
885match TIME return λTIME. TIME ≥ ? → ? with
886[ O ⇒ λTERMINATES_IN_TIME. ⊥
887| S TIME ⇒ λTERMINATES_IN_TIME.
888
889  let r ≝ make_label_label ge depth s
890            trace
891            ENV_COSTLABELLED
892            STATE_COSTLABELLED
893            STATEMENT_COSTLABEL
894            TERMINATES
895            TIME ? in
896  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
897                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
898  [ ends_with_ret ⇒ λr.
899      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
900  | doesnt_end_with_ret ⇒ λr.
901      let r' ≝ make_label_return ge depth (new_state … r)
902                 (remainder … r)
903                 ENV_COSTLABELLED
904                 (cost_labelled … r) ?
905                 (pi1 … (terminates … r)) TIME ? in
906        replace_trace … r' ?
907          (tlr_step (RTLabs_status ge) s (new_state … r)
908            (new_state … r') (new_trace … r) (new_trace … r')) ?
909  ] (trace_res … r)
910
911] TERMINATES_IN_TIME
912
913
914and make_label_label ge depth s
915  (trace: flat_trace io_out io_in ge s)
916  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
917  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
918  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
919  (TERMINATES: will_return ge depth s trace)
920  (TIME: nat)
921  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
922  on TIME : sub_trace_result ge depth s trace TERMINATES
923              (λends. trace_label_label (RTLabs_status ge) ends s)
924              (will_return_length … TERMINATES) ≝
925             
926match TIME return λTIME. TIME ≥ ? → ? with
927[ O ⇒ λTERMINATES_IN_TIME. ⊥
928| S TIME ⇒ λTERMINATES_IN_TIME.
929
930let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
931  replace_sub_trace … r ?
932    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
933
934] TERMINATES_IN_TIME
935
936
937and make_any_label ge depth s
938  (trace: flat_trace io_out io_in ge s)
939  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
940  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
941  (TERMINATES: will_return ge depth s trace)
942  (TIME: nat)
943  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
944  on TIME : sub_trace_result ge depth s trace TERMINATES
945              (λends. trace_any_label (RTLabs_status ge) ends s)
946              (will_return_length … TERMINATES) ≝
947
948match TIME return λTIME. TIME ≥ ? → ? with
949[ O ⇒ λTERMINATES_IN_TIME. ⊥
950| S TIME ⇒ λTERMINATES_IN_TIME.
951
952  match trace return λs,trace. well_cost_labelled_state s →
953                               ∀TM:will_return ??? trace.
954                               myge ? (times 3 (will_return_length ??? trace TM)) →
955                               sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
956  [ ft_stop st FINAL ⇒
957      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
958
959  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
960    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
961    [ cl_other ⇒ λCL.
962        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
963        (* We're about to run into a label. *)
964        [ true ⇒ λCS.
965            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
966              doesnt_end_with_ret
967              (mk_trace_result ge … next trace' ?
968                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
969        (* An ordinary step, keep going. *)
970        | false ⇒ λCS.
971            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
972                replace_sub_trace … r ?
973                  (tal_step_default (RTLabs_status ge) (ends … r)
974                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
975        ] (refl ??)
976       
977    | cl_jump ⇒ λCL.
978        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
979          doesnt_end_with_ret
980          (mk_trace_result ge … next trace' ?
981            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
982           
983    | cl_call ⇒ λCL.
984        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
985        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
986        (* We're about to run into a label, use base case for call *)
987        [ true ⇒ λCS.
988            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
989            doesnt_end_with_ret
990            (mk_trace_result ge …
991              (tal_base_call (RTLabs_status ge) start next (new_state … r)
992                ? CL ? (new_trace … r) CS) ??)
993        (* otherwise use step case *)
994        | false ⇒ λCS.
995            let r' ≝ make_any_label ge depth
996                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
997                       (pi1 … (terminates … r)) TIME ? in
998            replace_sub_trace … r' ?
999              (tal_step_call (RTLabs_status ge) (ends … r')
1000                start next (new_state … r) (new_state … r') ? CL ?
1001                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
1002        ] (refl ??)
1003
1004    | cl_return ⇒ λCL.
1005        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1006          ends_with_ret
1007          (mk_trace_result ge …
1008            next
1009            trace'
1010            ?
1011            (tal_base_return (RTLabs_status ge) start next ? CL)
1012            ?
1013            ?)
1014    ] (refl ? (RTLabs_classify start))
1015   
1016  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
1017 
1018  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
1019] TERMINATES_IN_TIME.
1020
1021[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1022| //
1023| //
1024| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1025| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1026| @(stack_preserved_join … (stack_ok … r)) //
1027| @(trace_label_label_label … (new_trace … r))
1028| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1029  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1030  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1031  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1032    @(monotonic_le_times_r 3 … LT)
1033  | @le_S @le_S @le_n
1034  ]
1035| @le_S_S_to_le @TERMINATES_IN_TIME
1036| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1037| @le_n
1038| //
1039| @le_S_S_to_le @TERMINATES_IN_TIME
1040| @(wrl_nonzero … TERMINATES_IN_TIME)
1041| (* We can't reach the final state because the function terminates with a
1042     return *)
1043  inversion TERMINATES
1044  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1045  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1046  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1047  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1048  ]
1049| @(will_return_return … CL TERMINATES)
1050| /2 by stack_preserved_return/
1051| %{tr} @EV
1052| @(well_cost_labelled_state_step  … EV) //
1053| whd @(will_return_notfn … TERMINATES) %2 @CL
1054| @stack_preserved_step /2/
1055| %{tr} @EV
1056| %1 whd @CL
1057| @(well_cost_labelled_jump … EV) //
1058| @(well_cost_labelled_state_step  … EV) //
1059| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1060  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1061    #TMx * #LT' #_ @LT'
1062  | <EQr cases (will_return_call … CL TERMINATES)
1063    #TM' * #_ #EQ' @EQ'
1064  ]
1065| @(stack_preserved_call … EV (stack_ok … r)) //
1066| %{tr} @EV
1067| @RTLabs_after_call //
1068| @(cost_labelled … r)
1069| skip
1070| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1071  @(transitive_lt … LT)
1072  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1073| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1074  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
1075| @RTLabs_after_call //
1076| %{tr} @EV
1077| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
1078| @(cost_labelled … r)
1079| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1080  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1081  cases (will_return_call … TERMINATES) in GT;
1082  #X * #Y #_ #Z
1083  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1084  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1085  | //
1086  ]
1087| @(well_cost_labelled_state_step  … EV) //
1088| @(well_cost_labelled_call … EV) //
1089| cases (will_return_call … TERMINATES)
1090  #TM * #GT #_ @le_S_S_to_le
1091  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1092  @(transitive_le … TERMINATES_IN_TIME)
1093  @(monotonic_le_times_r 3 … GT)
1094| whd @(will_return_notfn … TERMINATES) %1 @CL
1095| @(stack_preserved_step … EV) /2/
1096| %{tr} @EV
1097| %2 whd @CL
1098| @(well_cost_labelled_state_step  … EV) //
1099| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1100| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
1101| @CL
1102| %{tr} @EV
1103| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
1104| @(well_cost_labelled_state_step  … EV) //
1105| %1 @CL
1106| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1107  @le_S_S_to_le
1108  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1109  //
1110| inversion TERMINATES
1111  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
1112  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
1113  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
1114  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
1115  ]
1116] qed.
1117
1118(* We can initialise TIME with a suitably large value based on the length of the
1119   termination proof. *)
1120let rec make_label_return' ge depth s
1121  (trace: flat_trace io_out io_in ge s)
1122  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1123  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1124  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1125  (TERMINATES: will_return ge depth s trace)
1126  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1127make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1128  (2 + 3 * will_return_length … TERMINATES) ?.
1129@le_n
1130qed.
1131 
1132(* Tail-calls would not be handled properly (which means that if we try to show the
1133   full version with non-termination we'll fail because calls and returns aren't
1134   balanced.
1135 *)
1136
1137inductive inhabited (T:Type[0]) : Prop ≝
1138| witness : T → inhabited T.
1139
1140(* We also require that program's traces are soundly labelled: for any state
1141   in the execution, we can give a distance to a labelled state or termination.
1142   
1143   Note that this differs from the syntactic notions in earlier languages
1144   because it is a global property.  In principle, we would have a loop broken
1145   only by a call to a function (which necessarily has a label) and no local
1146   cost label.
1147 *)
1148
1149let rec nth_state ge s
1150  (trace: flat_trace io_out io_in ge s)
1151  n
1152  on n : option state ≝
1153match n with
1154[ O ⇒ Some ? s
1155| S n' ⇒
1156  match trace with
1157  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
1158  | _ ⇒ None ?
1159  ]
1160].
1161
1162definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
1163λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
1164
1165lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
1166  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
1167  soundly_labelled_trace ge s' trace'.
1168#ge #s #tr #s' #EV #trace' #H
1169#n cases (H (S n)) #m #H' %{m} @H'
1170qed.
1171
1172(* Define a notion of sound labellings of RTLabs programs. *)
1173
1174let rec successors (s : statement) : list label ≝
1175match s with
1176[ St_skip l ⇒ [l]
1177| St_cost _ l ⇒ [l]
1178| St_const _ _ l ⇒ [l]
1179| St_op1 _ _ _ _ _ l ⇒ [l]
1180| St_op2 _ _ _ _ l ⇒ [l]
1181| St_load _ _ _ l ⇒ [l]
1182| St_store _ _ _ l ⇒ [l]
1183| St_call_id _ _ _ l ⇒ [l]
1184| St_call_ptr _ _ _ l ⇒ [l]
1185(*
1186| St_tailcall_id _ _ ⇒ [ ]
1187| St_tailcall_ptr _ _ ⇒ [ ]
1188*)
1189| St_cond _ l1 l2 ⇒ [l1; l2]
1190| St_jumptable _ ls ⇒ ls
1191| St_return ⇒ [ ]
1192].
1193
1194definition actual_successor : state → option label ≝
1195λs. match s with
1196[ State f fs m ⇒ Some ? (next f)
1197| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1198| Returnstate _ _ _ _ ⇒ None ?
1199| Finalstate _ ⇒ None ?
1200].
1201
1202lemma nth_opt_Exists : ∀A,n,l,a.
1203  nth_opt A n l = Some A a →
1204  Exists A (λa'. a' = a) l.
1205#A #n elim n
1206[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1207| #m #IH *
1208  [ #a #E normalize in E; destruct
1209  | #a #l #a' #E %2 @IH @E
1210  ]
1211] qed.
1212
1213lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1214  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1215  RTLabs_classify s' = cl_return ∨
1216  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1217#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1218whd in ⊢ (??%? → ?);
1219generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1220[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1221| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1222| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1223| #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} % // % //
1224| #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} % // % //
1225| #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} % // % //
1226| #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} % // % //
1227| #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} % // % //
1228| #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} % // % //
1229| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
1230| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
1231  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 ]
1232  whd in ⊢ (??%? → ?);
1233  generalize in ⊢ (??(?%)? → ?);
1234  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1235  [ #e #E normalize in E; destruct
1236  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1237  ]
1238| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
1239] qed.
1240
1241definition steps_for_statement : statement → nat ≝
1242λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
1243
1244inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
1245| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
1246| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
1247with bound_on_steps_to_cost1 : label → nat → Prop ≝
1248| bostc_step : ∀l,n,H.
1249    let stmt ≝ lookup_present … g l H in
1250    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1251          bound_on_steps_to_cost g l' n) →
1252    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
1253
1254(*
1255lemma steps_to_label_bound_inv : ∀g,l,n.
1256  steps_to_label_bound g l n →
1257  ∀H. let stmt ≝ lookup_present … g l H in
1258  ∃n'. n = steps_for_statement stmt + n' ∧
1259  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1260        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
1261        steps_to_label_bound g l' n').
1262#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
1263% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
1264qed.
1265  *) 
1266
1267(*
1268definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1269
1270let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1271  soundly_labelled_pc (f_graph fn) (f_entry fn).
1272
1273
1274definition soundly_labelled_frame : frame → Prop ≝
1275λf. soundly_labelled_pc (f_graph (func f)) (next f).
1276
1277definition soundly_labelled_state : state → Prop ≝
1278λs. match s with
1279[ State f _ _ ⇒ soundly_labelled_frame f
1280| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1281| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1282].
1283*)
1284definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1285λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1286definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1287λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1288
1289inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1290| 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
1291| 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)
1292| 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)
1293.
1294
1295lemma state_bound_on_steps_to_cost_zero : ∀s.
1296  ¬ state_bound_on_steps_to_cost s O.
1297#s % #H inversion H
1298[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1299  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1300  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1301| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1302| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1303] qed.
1304
1305lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1306  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1307  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1308  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
1309#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1310whd in ⊢ (??%? → ?);
1311generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1312[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1313| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1314| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1315| #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
1316| #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
1317| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1318| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1319| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1320| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1321| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1322| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
1323  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 ]
1324  whd in ⊢ (??%? → ?);
1325  generalize in ⊢ (??(?%)? → ?);
1326  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1327  [ #e #E normalize in E; destruct
1328  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1329  ]
1330| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1331] qed.
1332
1333lemma bound_after_call : ∀ge,s,s',n.
1334  state_bound_on_steps_to_cost s (S n) →
1335  ∀CL:RTLabs_classify s = cl_call.
1336  as_after_return (RTLabs_status ge) «s, CL» s' →
1337  RTLabs_cost s' = false →
1338  state_bound_on_steps_to_cost s' n.
1339#ge #s #s' #n #H inversion H
1340[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1341  #fn * #args * #dst * #stk * #m' #E destruct
1342| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1343  whd in S; #CL cases s'
1344  [ #f' #fs' #m' * #N #F #CS
1345    %1 whd
1346    inversion S
1347    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1348      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1349    | #l #n #B #E1 #E2 #_ destruct <N <F @B
1350    ]
1351  | #fd' #args' #dst' #fs' #m' *
1352  | #rv #dst' #fs' #m' *
1353  | #r #E normalize in E; destruct
1354  ]
1355| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1356] qed.
1357
1358lemma bound_after_step : ∀ge,s,tr,s',n.
1359  state_bound_on_steps_to_cost s (S n) →
1360  eval_statement ge s = Value ??? 〈tr, s'〉 →
1361  RTLabs_cost s' = false →
1362  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1363   state_bound_on_steps_to_cost s' n.
1364#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1365[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1366  #EVAL cases (eval_successor … EVAL)
1367  [ /3/
1368  | * #l * #S1 #S2 #NC %2
1369  (*
1370    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1371    *)
1372    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1373    inversion (eval_perserves … EVAL)
1374    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1375      >(eval_steps … EVAL) in E2; #En normalize in En;
1376      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1377      %1 inversion (IH … S2)
1378      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1379        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1380        whd in S1:(??%?); destruct >NC in CSx; *
1381      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
1382      ]
1383    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1384      >(eval_steps … EVAL) in E2; #En normalize in En;
1385      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1386      %2 @IH normalize in S1; destruct @S2
1387    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1388      destruct
1389    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1390      normalize in S1; destruct
1391    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1392    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1393    ]
1394  ]
1395| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1396  /3/
1397| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1398  #EVAL #NC %2 inversion (eval_perserves … EVAL)
1399  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1400  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1401  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1402  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1403  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1404    %1 whd in FS ⊢ %;
1405    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
1406    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
1407    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 ]
1408    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1409    inversion FS
1410    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1411        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
1412        >NC in CSx; *
1413    | #lx #nx #H #E1x #E2x #_ destruct @H
1414    ]
1415  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1416  ]
1417] qed.
1418
1419
1420
1421
1422definition soundly_labelled_fn : internal_function → Prop ≝
1423λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
1424
1425definition soundly_labelled_ge : genv → Prop ≝
1426λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1427
1428definition soundly_labelled_state : state → Prop ≝
1429λs. match s with
1430[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1431| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1432                          All ? (λf. soundly_labelled_fn (func f)) fs
1433| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1434| Finalstate _ ⇒ True
1435].
1436
1437lemma steps_from_sound : ∀s.
1438  RTLabs_cost s = true →
1439  soundly_labelled_state s →
1440  ∃n. state_bound_on_steps_to_cost s n.
1441* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
1442whd in ⊢ (% → ?); * #SLF #_
1443cases (SLF (next f) (next_ok f)) #n #B1
1444%{n} % @B1
1445qed.
1446
1447lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1448  soundly_labelled_ge ge →
1449  eval_statement ge s = Value ??? 〈tr,s'〉 →
1450  soundly_labelled_state s →
1451  soundly_labelled_state s'.
1452#ge #s #tr #s' #ENV #EV #S
1453inversion (eval_perserves … EV)
1454[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1455  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1456| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1457  whd in S ⊢ %; %
1458  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1459  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1460  ]
1461| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1462  whd in S ⊢ %; @S
1463| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1464  whd in S ⊢ %; cases S //
1465| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
1466  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1467| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1468] qed.
1469
1470lemma soundly_labelled_state_preserved : ∀s,s'.
1471  stack_preserved ends_with_ret s s' →
1472  soundly_labelled_state s →
1473  soundly_labelled_state s'.
1474#s0 #s0' #SP inversion SP
1475[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1476| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
1477  inversion S1
1478  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
1479    * #_ #S whd in S;
1480    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1481    destruct @S
1482  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
1483    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1484    destruct @S
1485  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
1486    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1487    destruct @S
1488  ]
1489| //
1490| //
1491] qed.
1492
1493(* When constructing an infinite trace, we need to be able to grab the finite
1494   portion of the trace for the next [trace_label_diverges] constructor.  We
1495   use the fact that the trace is soundly labelled to achieve this. *)
1496
1497record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1498  ro_well_cost_labelled: well_cost_labelled_state s;
1499  ro_soundly_labelled: soundly_labelled_state s;
1500  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1501  ro_not_undefined: not_wrong … t;
1502  ro_not_final: RTLabs_is_final s = None ?
1503}.
1504
1505inductive finite_prefix (ge:genv) : state → Prop ≝
1506| fp_tal : ∀s,s'.
1507           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1508           ∀t:flat_trace io_out io_in ge s'.
1509           remainder_ok ge s' t →
1510           finite_prefix ge s
1511| fp_tac : ∀s1,s2,s3,tr.
1512           trace_any_call (RTLabs_status ge) s1 s2 →
1513           well_cost_labelled_state s2 →
1514           eval_statement ge s2 = Value ??? 〈tr,s3〉 →
1515           ∀t:flat_trace io_out io_in ge s3.
1516           remainder_ok ge s3 t →
1517           finite_prefix ge s1
1518.
1519
1520definition fp_add_default : ∀ge,s,s'.
1521  RTLabs_classify s = cl_other →
1522  finite_prefix ge s' →
1523  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
1524  RTLabs_cost s' = false →
1525  finite_prefix ge s ≝
1526λge,s,s',OTHER,fp.
1527match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
1528[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1529    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1530    rem rok
1531| fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr
1532    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1533    WCL2 EV rem rok
1534].
1535
1536definition fp_add_terminating_call : ∀ge,s,s1,s''.
1537  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
1538  ∀CALL:RTLabs_classify s = cl_call.
1539  finite_prefix ge s'' →
1540  trace_label_return (RTLabs_status ge) s1 s'' →
1541  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1542  RTLabs_cost s'' = false →
1543  finite_prefix ge s ≝
1544λge,s,s1,s'',EVAL,CALL,fp.
1545match 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
1546[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1547    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1548    rem rok
1549| fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr
1550    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1551    WCL2 EV rem rok
1552].
1553
1554lemma not_return_to_not_final : ∀ge,s,tr,s'.
1555  eval_statement ge s = Value ??? 〈tr, s'〉 →
1556  RTLabs_classify s ≠ cl_return →
1557  RTLabs_is_final s' = None ?.
1558#ge #s #tr #s' #EV
1559inversion (eval_perserves … EV) //
1560#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1561@⊥ @(absurd ?? CL) @refl
1562qed.
1563
1564definition termination_oracle ≝ ∀ge,depth,s,trace.
1565  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1566
1567let rec finite_segment ge s n trace
1568  (ORACLE: termination_oracle)
1569  (TRACE_OK: remainder_ok ge s trace)
1570  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1571  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1572  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
1573  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1574  on n : finite_prefix ge s ≝
1575match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1576[ O ⇒ λLABEL_LIMIT. ⊥
1577| S n' ⇒
1578    match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
1579    [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1580    | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT.
1581        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1582        [ cl_other ⇒ λCL.
1583            let TRACE_OK' ≝ ? in
1584            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1585            [ true ⇒ λCS.
1586                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
1587            | false ⇒ λCS.
1588                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
1589                fp_add_default ge ?? CL fs ? CS
1590            ] (refl ??)
1591        | cl_jump ⇒ λCL.
1592            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ?
1593        | cl_call ⇒ λCL.
1594            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
1595            [ or_introl TERMINATES ⇒
1596              match TERMINATES with [ witness TERMINATES ⇒
1597                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1598                let TRACE_OK' ≝ ? in
1599                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
1600                [ 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) TRACE_OK'
1601                | false ⇒ λCS.
1602                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
1603                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
1604                ] (refl ??)
1605              ]
1606            | or_intror NO_TERMINATION ⇒
1607                fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ?
1608            ]
1609        | cl_return ⇒ λCL. ⊥
1610        ] (refl ??)
1611    | ft_wrong start m EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1612    ] TRACE_OK
1613] LABEL_LIMIT.
1614[ cases (state_bound_on_steps_to_cost_zero s) /2/
1615| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1616| @(absurd ?? (ro_no_termination … TRACE_OK))
1617     %{0} % @wr_base //
1618| @(well_cost_labelled_jump … EV) /2/
1619| 5,6,8,9,10,11: /3/
1620| % [ @(well_cost_labelled_state_step … EV) /2/
1621    | @(soundly_labelled_state_step … EV) /2/
1622    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1623    | @(still_not_wrong … EV) /2/
1624    | @(not_return_to_not_final … EV) >CL % #E destruct
1625    ]
1626| /2/
1627| @(soundly_labelled_state_preserved … (stack_ok … tlr))
1628  @(soundly_labelled_state_step … EV) /2/
1629| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
1630  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
1631| % [ /2/
1632    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
1633      @(soundly_labelled_state_step … EV) /2/
1634    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1635      @wr_call //
1636      @(will_return_prepend … TERMINATES … TM1)
1637      cases (terminates … tlr) //
1638    | @(will_return_not_wrong … TERMINATES)
1639      [ @(still_not_wrong … EV) /2/
1640      | cases (terminates … tlr) //
1641      ]
1642    | (* By stack preservation we cannot be in the final state *)
1643      inversion (stack_ok … tlr)
1644      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1645      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1646      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
1647        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
1648        inversion (eval_perserves … EV)
1649        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
1650        #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1651        inversion S
1652        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
1653        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1654           so we can use it as a witness that at least one frame exists *)
1655        inversion LABEL_LIMIT
1656        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1657      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1658      ]
1659    ]
1660| @(well_cost_labelled_state_step … EV) /2/
1661| @(well_cost_labelled_call … EV) /2/
1662| /2/
1663| % [ @(well_cost_labelled_state_step … EV) /2/
1664    | @(soundly_labelled_state_step … EV) /2/
1665    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1666      @(will_return_lower … TM) //
1667    | @(still_not_wrong … EV) /2/
1668    | @(not_return_to_not_final … EV) >CL % #E destruct
1669    ]
1670| 20,21,22: /2/
1671| @(soundly_labelled_state_step … EV) /2/
1672| cases (bound_after_step … LABEL_LIMIT EV ?)
1673  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
1674    inversion trace'
1675    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1676      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1677      % >CL #E destruct
1678    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1679      @wr_base //
1680    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
1681      inversion (ro_not_undefined … TRACE_OK)
1682      [ #H137 #H138 #H139 #H140 #H141 destruct
1683      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct
1684        inversion H148
1685        [ #H153 #H154 #H155 #H156 #H157 destruct
1686        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
1687        ]
1688      ]
1689    ]
1690    ]
1691    | >CL #E destruct
1692    ]
1693  | //
1694  | //
1695  ]
1696| % [ @(well_cost_labelled_state_step … EV) /2/
1697    | @(soundly_labelled_state_step … EV) /2/
1698    | @(not_to_not … (ro_no_termination … TRACE_OK))
1699      * #depth * #TERM %{depth} % @wr_step /2/
1700    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
1701    | @(not_return_to_not_final … EV) >CL % #E destruct
1702    ]
1703| inversion (ro_not_undefined … TRACE_OK)
1704  [ #H169 #H170 #H171 #H172 #H173 destruct
1705  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
1706  ]
1707] qed.
1708
1709(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1710       a trace_label_diverges value, but I only know how to construct those
1711       using a cofixpoint in Type[0], which means I can't use the termination
1712       oracle.
1713*)
1714
1715let corec make_label_diverges ge s
1716  (trace: flat_trace io_out io_in ge s)
1717  (ORACLE: termination_oracle)
1718  (TRACE_OK: remainder_ok ge s trace)
1719  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1720  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1721  (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
1722  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1723  : trace_label_diverges_exists (RTLabs_status ge) s ≝
1724match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
1725[ ex_intro n B ⇒
1726    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B
1727      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1728    with
1729    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1730        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
1731            tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
1732(*
1733        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
1734        [ ex_intro T' _ ⇒
1735            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1736        ]*)
1737    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1738        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
1739            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
1740(*
1741        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
1742        [ ex_intro T' _ ⇒
1743            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1744        ]*)
1745    ] STATEMENT_COSTLABEL
1746].
1747[ /2/
1748| @(trace_any_label_label … T)
1749| %{tr} @EV
1750| @(trace_any_call_call … T)
1751| /2/
1752| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
1753] qed.
Note: See TracBrowser for help on using the repository browser.