source: src/RTLabs/Traces.ma @ 1736

Last change on this file since 1736 was 1736, checked in by campbell, 9 years ago

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