source: src/RTLabs/Traces.ma @ 1713

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

Add a distinguished final state to the front-end languages to match up
with the structured traces.

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