source: src/RTLabs/Traces.ma @ 1707

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

Progress on finite segments of infinite RTLabs structured trace.

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