source: src/RTLabs/Traces.ma @ 1712

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

Show that constructing an RTLabs structure trace really does use a prefix of the flat trace.

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