source: src/RTLabs/Traces.ma @ 1880

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

Show that RTLabs flat traces are determined by their starting state, and
that structured traces can be flattened, so must describe the same
execution as a flat trace from the same starting point.

File size: 90.7 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 → final_abstract_status ≝
34λge.
35mk_final_abstract_status
36  (mk_abstract_status
37    state
38    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
39    (λs,c. RTLabs_classify s = c)
40    (λs. RTLabs_cost s = true)
41    (λs,s'. match s with
42      [ mk_Sig s p ⇒
43        match s return λs. RTLabs_classify s = cl_call → ? with
44        [ Callstate fd args dst stk m ⇒
45          λ_. match s' with
46          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
47          | Finalstate r ⇒ stk = [ ]
48          | _ ⇒ False
49          ]
50        | State f fs m ⇒ λH.⊥
51        | _ ⇒ λH.⊥
52        ] p
53      ]))
54  (λs. RTLabs_is_final s ≠ None ?).
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 try #i try #j destruct
58| normalize in H; destruct
59| normalize in H; destruct
60] qed.
61
62lemma RTLabs_not_cost : ∀ge,s.
63  RTLabs_cost s = false →
64  ¬ as_costed (RTLabs_status ge) s.
65#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
66qed.
67
68(* Before attempting to construct a structured trace, let's show that we can
69   form flat traces with evidence that they were constructed from an execution.
70   
71   For now we don't consider I/O. *)
72
73
74coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
75| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
76| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
77| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
78
79(* add I/O? *)
80coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
81| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
82| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
83| ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
84
85coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
86| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
87| 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').
88
89lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
90  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
91  not_wrong o i ge s' tr'.
92#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
93[ #H105 #H106 #H107 #H108 #H109 destruct
94| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
95] qed.
96
97let corec make_flat_trace ge s
98  (NF:RTLabs_is_final s = None ?)
99  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
100  flat_trace io_out io_in ge s ≝
101let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
102match e return λx. e = x → ? with
103[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
104| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??)
105| e_wrong m ⇒ λE. ft_wrong … s m ??
106| e_interact o f ⇒ λE. ⊥
107] (refl ? e).
108[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
109  cases (eval_statement ge s)
110  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
111  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
112    >(?:is_final ????? = RTLabs_is_final s1) //
113    lapply (refl ? (RTLabs_is_final s1))
114    cases (RTLabs_is_final s1) in ⊢ (???% → %);
115    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
116    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
117    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
118    ]
119  | *: #m whd in ⊢ (??%? → ?); #E destruct
120  ]
121| whd in E:(??%?); >exec_inf_aux_unfold in E;
122  cases (eval_statement ge s)
123  [ #O #K whd in ⊢ (??%? → ?); #E destruct
124  | * #tr #s1 whd in ⊢ (??%? → ?);
125    cases (is_final ?????)
126    [ whd in ⊢ (??%? → ?); #E destruct @refl
127    | #i whd in ⊢ (??%? → ?); #E destruct
128    ]
129  | #m whd in ⊢ (??%? → ?); #E destruct
130  ]
131| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
132  cases (eval_statement ge s)
133  [ #O #K whd in ⊢ (??%? → ?); #E destruct
134  | * #tr #s1 whd in ⊢ (??%? → ?);
135    cases (is_final ?????)
136    [ whd in ⊢ (??%? → ?); #E
137      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
138      destruct
139      inversion H
140      [ #a #b #c #E1 destruct
141      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
142      | #m #E1 destruct
143      ]
144    | #i whd in ⊢ (??%? → ?); #E destruct
145    ]
146  | #m whd in ⊢ (??%? → ?); #E destruct
147  ]
148| whd in E:(??%?); >exec_inf_aux_unfold in E;
149  cases (eval_statement ge s)
150  [ #o #K whd in ⊢ (??%? → ?); #E destruct
151  | * #tr #s1 whd in ⊢ (??%? → ?);
152    lapply (refl ? (RTLabs_is_final s1))
153    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
154    cases (RTLabs_is_final s1) in ⊢ (???% → %);
155    [ #F #E whd in E:(??%?); destruct @F
156    | #r #F #E whd in E:(??%?); destruct
157    ]
158  | #m #E whd in E:(??%?); destruct
159  ]
160| @NF
161| whd in E:(??%?); >exec_inf_aux_unfold in E;
162  cases (eval_statement ge s)
163  [ #O #K whd in ⊢ (??%? → ?); #E destruct
164  | * #tr1 #s1 whd in ⊢ (??%? → ?);
165    cases (is_final ?????)
166    [ whd in ⊢ (??%? → ?); #E destruct
167    | #i whd in ⊢ (??%? → ?); #E destruct
168    ]
169  | #m whd in ⊢ (??%? → ?); #E destruct @refl
170  ]
171| whd in E:(??%?); >E in H; #H
172  inversion H
173  [ #a #b #c #E destruct
174  | #a #b #c #d #E1 destruct
175  | #m #E1 destruct
176  ]
177] qed.
178
179let corec make_whole_flat_trace p s
180  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
181  (I:make_initial_state ??? p = OK ? s) :
182  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
183let ge ≝ make_global … p in
184let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
185match e return λx. e = x → ? with
186[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
187| e_step _ _ e' ⇒ λE. make_flat_trace ge s ??
188| e_wrong m ⇒ λE. ⊥
189| e_interact o f ⇒ λE. ⊥
190] (refl ? e).
191[ whd in E:(??%?); >exec_inf_aux_unfold in E;
192  whd in ⊢ (??%? → ?);
193  change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
194  cases (RTLabs_is_final s)
195  [ #E whd in E:(??%?); destruct
196  | #r #E % #E' destruct
197  ]
198| @(initial_state_is_not_final … I)
199| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
200  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
201  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
202    [ #a #b #c #E1 destruct
203    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
204      @H1
205    | #m #E1 destruct
206    ]
207  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
208  ]
209| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
210  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
211| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
212  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
213] qed.
214
215(* Need a way to choose whether a called function terminates.  Then,
216     if the initial function terminates we generate a purely inductive structured trace,
217     otherwise we start generating the coinductive one, and on every function call
218       use the choice method again to decide whether to step over or keep going.
219
220Not quite what we need - have to decide on seeing each label whether we will see
221another or hit a non-terminating call?
222
223Also - need the notion of well-labelled in order to break loops.
224
225
226
227outline:
228
229 does function terminate?
230 - yes, get (bound on the number of steps until return), generate finite
231        structure using bound as termination witness
232 - no,  get (¬ bound on steps to return), start building infinite trace out of
233        finite steps.  At calls, check for termination, generate appr. form.
234
235generating the finite parts:
236
237We start with the status after the call has been executed; well-labelling tells
238us that this is a labelled state.  Now we want to generate a trace_label_return
239and also return the remainder of the flat trace.
240
241*)
242
243(* [will_return ge depth s trace] says that after a finite number of steps of
244   [trace] from [s] we reach the return state for the current function.  [depth]
245   performs the call/return counting necessary for handling deeper function
246   calls.  It should be zero at the top level. *)
247inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
248| wr_step : ∀s,tr,s',depth,EX,trace.
249    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
250    will_return ge depth s' trace →
251    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
252| wr_call : ∀s,tr,s',depth,EX,trace.
253    RTLabs_classify s = cl_call →
254    will_return ge (S depth) s' trace →
255    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
256| wr_ret : ∀s,tr,s',depth,EX,trace.
257    RTLabs_classify s = cl_return →
258    will_return ge depth s' trace →
259    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
260    (* Note that we require the ability to make a step after the return (this
261       corresponds to somewhere that will be guaranteed to be a label at the
262       end of the compilation chain). *)
263| wr_base : ∀s,tr,s',EX,trace.
264    RTLabs_classify s = cl_return →
265    will_return ge O s (ft_step ?? ge s tr s' EX trace)
266.
267
268(* The way we will use [will_return] won't satisfy Matita's guardedness check,
269   so we will measure the length of these termination proofs and use an upper
270   bound to show termination of the finite structured trace construction
271   functions. *)
272
273let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
274match T with
275[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
276| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
277| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
278| wr_base _ _ _ _ _ _ ⇒ S O
279].
280
281include alias "arithmetics/nat.ma".
282
283(* Specialised to the particular situation it is used in. *)
284lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
285#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
286whd in ⊢ (??(??%) → ?);
287>commutative_times
288#H lapply (le_plus_b … H)
289#H lapply (le_to_leb_true … H)
290normalize #E destruct
291qed.
292   
293let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝
294match T with
295[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
296| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
297| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
298| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
299].
300
301(* Inversion lemmas on [will_return] that also note the effect on the length
302   of the proof. *)
303lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
304  RTLabs_classify s = cl_call →
305  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
306  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
307#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
308[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
309| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
310| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
311| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
312] qed.
313
314lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
315  RTLabs_classify s = cl_return →
316  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
317  match d with
318  [ O ⇒ will_return_end … TM = ❬s', trace❭
319  | S d' ⇒
320      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
321  ].
322#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
323[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
324| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
325| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
326| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
327] qed.
328
329lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
330  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
331  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
332  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
333#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
334[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
335| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
336| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
337| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
338| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
339| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
340| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
341| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
342] qed.
343
344(* When it comes to building bits of nonterminating executions we'll need to be
345   able to glue termination proofs together. *)
346
347lemma will_return_prepend : ∀ge,d1,s1,t1.
348  ∀T1:will_return ge d1 s1 t1.
349  ∀d2,s2,t2.
350  will_return ge d2 s2 t2 →
351  will_return_end … T1 = ❬s2, t2❭ →
352  will_return ge (d1 + S d2) s1 t1.
353#ge #d1 #s1 #tr1 #T1 elim T1
354[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
355  %1 // @(IH … T2) @E
356| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
357| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
358| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
359] qed.
360
361discriminator nat.
362
363lemma will_return_remove_call : ∀ge,d1,s1,t1.
364  ∀T1:will_return ge d1 s1 t1.
365  ∀d2.
366  will_return ge (d1 + S d2) s1 t1 →
367  ∀s2,t2.
368  will_return_end … T1 = ❬s2, t2❭ →
369  will_return ge d2 s2 t2.
370(* The key part of the proof is to show that the two termination proofs follow
371   the same pattern. *)
372#ge #d1x #s1x #t1x #T1 elim T1
373[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
374  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
375                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
376                   >H21 in CL; * #E destruct
377                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
378                   >H35 in CL; * #E destruct
379                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
380                   >H48 in CL; * #E destruct
381                 ]
382  | @E
383  ]
384| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
385  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
386                   >CL in H7; * #E destruct
387                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
388                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
389                   >H35 in CL; #E destruct
390                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
391                   >H48 in CL; #E destruct
392                 ]
393  | @E
394  ]
395| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
396  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
397                   >CL in H7; * #E destruct
398                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
399                   >H21 in CL; #E destruct
400                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
401                   whd in H38:(??%??); destruct //
402                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
403                   whd in H49:(??%??); @⊥ destruct
404                 ]
405  | @E
406  ]
407| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
408  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
409                 >CL in H7; * #E destruct
410               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
411                 >H21 in CL; #E destruct
412               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
413                 whd in H38:(??%??); destruct //
414               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
415                 whd in H49:(??%??); @⊥ destruct
416               ]
417] qed.
418
419lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
420  ∀T:will_return ge d s t.
421  not_wrong io_out io_in ge s t →
422  will_return_end … T = ❬s', t'❭ →
423  not_wrong io_out io_in ge s' t'.
424#ge #d #s #t #s' #t' #T elim T
425[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
426  [ inversion NW
427    [ #H1 #H2 #H3 #H4 #H5 destruct
428    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
429    ]
430  | @E
431  ]
432| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
433  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
434  | @E
435  ]
436| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
437  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
438  | @E
439  ]
440| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
441  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
442] qed.
443
444
445lemma will_return_lower : ∀ge,d,s,t.
446  will_return ge d s t →
447  ∀d'. d' ≤ d →
448  will_return ge d' s t.
449#ge #d0 #s0 #t0 #TM elim TM
450[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
451| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
452| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
453  [ #LE @wr_base //
454  | #d' #LE %3 // @IH /2/
455  ]
456| #s #tr #s' #EX #tr #CL *
457  [ #_ @wr_base //
458  | #d' #LE @⊥ /2/
459  ]
460] qed.
461
462(* We require that labels appear after branch instructions and at the start of
463   functions.  The first is required for preciseness, the latter for soundness.
464   We will make a separate requirement for there to be a finite number of steps
465   between labels to catch loops for soundness (is this sufficient?). *)
466
467definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
468λf,s. match s return λs. labels_present ? s → Prop with
469[ St_cond _ l1 l2 ⇒ λH.
470    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
471    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
472| St_jumptable _ ls ⇒ λH.
473    (* I did have a dependent version of All here, but it's a pain. *)
474    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
475| _ ⇒ λ_. True
476]. whd in H;
477[ @(proj1 … H)
478| @(proj2 … H)
479] qed.
480
481definition well_cost_labelled_fn : internal_function → Prop ≝
482λf. (∀l. ∀H:present … (f_graph f) l.
483         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
484    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
485[ @lookup_lookup_present | cases (f_entry f) // ] qed.
486
487(* We need to ensure that any code we come across is well-cost-labelled.  We may
488   get function code from either the global environment or the state. *)
489
490definition well_cost_labelled_ge : genv → Prop ≝
491λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
492
493definition well_cost_labelled_state : state → Prop ≝
494λs. match s with
495[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
496| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
497                          All ? (λf. well_cost_labelled_fn (func f)) fs
498| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
499| Finalstate _ ⇒ True
500].
501
502lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
503  eval_statement ge s = Value ??? 〈tr,s'〉 →
504  well_cost_labelled_ge ge →
505  well_cost_labelled_state s →
506  well_cost_labelled_state s'.
507#ge #s #tr' #s' #EV cases (eval_perserves … EV)
508[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
509| #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/
510(*
511| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
512*)
513| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
514| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
515| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
516| //
517] qed.
518
519lemma rtlabs_jump_inv : ∀s.
520  RTLabs_classify s = cl_jump →
521  ∃f,fs,m. s = State f fs m ∧
522  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
523  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
524*
525[ #f #fs #m #E
526  %{f} %{fs} %{m} %
527  [ @refl
528  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
529    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
530    [ %1 %{A} %{B} %{C} @refl
531    | %2 %{A} %{B} @refl
532    ]
533  ]
534| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
535| normalize #H8 #H9 #H10 #H11 #H12 destruct
536| #r #E normalize in E; destruct
537] qed.
538
539lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
540  eval_statement ge s = Value ??? 〈tr,s'〉 →
541  well_cost_labelled_state s →
542  RTLabs_classify s = cl_jump →
543  RTLabs_cost s' = true.
544#ge #s #tr #s' #EV #H #CL
545cases (rtlabs_jump_inv s CL)
546#fr * #fs * #m * #Es *
547[ * #r * #l1 * #l2 #Estmt
548  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
549  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
550  >Estmt #LP whd in ⊢ (??%? → ?);
551  (* replace with lemma on successors? *)
552  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
553  lapply (Hbody (next fr) (next_ok fr))
554  generalize in ⊢ (???% → ?);
555  >Estmt #LP'
556  whd in ⊢ (% → ?);
557  * #H1 #H2 [ @H1 | @H2 ]
558| * #r * #ls #Estmt
559  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
560  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
561  >Estmt #LP whd in ⊢ (??%? → ?);
562  (* replace with lemma on successors? *)
563  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
564  [ 2: (* later *)
565  | *: #E destruct
566  ]
567  lapply (Hbody (next fr) (next_ok fr))
568  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
569  generalize in ⊢ (??(?%)? → ?);
570  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
571  [ #E1 #E2 whd in E2:(??%?); destruct
572  | #l' #E1 #E2 whd in E2:(??%?); destruct
573    cases (All_nth ???? CP ? E1)
574    #H1 #H2 @H2
575  ]
576] qed.
577
578lemma rtlabs_call_inv : ∀s.
579  RTLabs_classify s = cl_call →
580  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
581* [ #f #fs #m whd in ⊢ (??%? → ?);
582    cases (lookup_present … (next f) (next_ok f)) normalize
583    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
584  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
585  | normalize #H411 #H412 #H413 #H414 #H415 destruct
586  | normalize #H1 #H2 destruct
587  ] qed.
588
589lemma well_cost_labelled_call : ∀ge,s,tr,s'.
590  eval_statement ge s = Value ??? 〈tr,s'〉 →
591  well_cost_labelled_state s →
592  RTLabs_classify s = cl_call →
593  RTLabs_cost s' = true.
594#ge #s #tr #s' #EV #WCL #CL
595cases (rtlabs_call_inv s CL)
596#fd * #args * #dst * #stk * #m #E >E in EV WCL;
597whd in ⊢ (??%? → % → ?);
598cases fd
599[ #fn whd in ⊢ (??%? → % → ?);
600  @bind_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
601  #m' #b whd in ⊢ (??%? → ?); #E' destruct
602  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
603  @WCL2
604| #fn whd in ⊢ (??%? → % → ?);
605  @bindIO_value #evargs #Eargs
606  whd in ⊢ (??%? → ?);
607  #E' destruct
608] qed.
609
610
611(* The preservation of (most of) the stack is useful to show as_after_return.
612   We do this by showing that during the execution of a function the lower stack
613   frames never change, and that after returning from the function we preserve
614   the identity of the next instruction to execute.
615 *)
616
617inductive stack_of_state : list frame → state → Prop ≝
618| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
619| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
620| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
621.
622
623inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
624| sp_normal : ∀fs,s1,s2.
625    stack_of_state fs s1 →
626    stack_of_state fs s2 →
627    stack_preserved doesnt_end_with_ret s1 s2
628| sp_finished : ∀s1,f,f',fs,m.
629    next f = next f' →
630    frame_rel f f' →
631    stack_of_state (f::fs) s1 →
632    stack_preserved ends_with_ret s1 (State f' fs m)
633| sp_stop : ∀s1,r.
634    stack_of_state [ ] s1 →
635    stack_preserved ends_with_ret s1 (Finalstate r)
636| sp_top : ∀fd,args,dst,m,r.
637    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
638.
639
640discriminator list.
641
642lemma stack_of_state_eq : ∀fs,fs',s.
643  stack_of_state fs s →
644  stack_of_state fs' s →
645  fs = fs'.
646#fs0 #fs0' #s0 *
647[ #f #fs #m #H inversion H
648  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
649| #fd #args #dst #f #fs #m #H inversion H
650  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
651| #rtv #dst #fs #m #H inversion H
652  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
653] qed.
654
655lemma stack_preserved_final : ∀e,r,s.
656  ¬stack_preserved e (Finalstate r) s.
657#e #r #s % #H inversion H
658[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
659  inversion SOS #a #b #c #d #e #f try #g try #h destruct
660| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
661  inversion SOS #a #b #c #d #e #f try #g try #h destruct
662| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
663  inversion SOS #a #b #c #d #e #f try #g try #h destruct
664| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
665] qed.
666
667lemma stack_preserved_join : ∀e,s1,s2,s3.
668  stack_preserved doesnt_end_with_ret s1 s2 →
669  stack_preserved e s2 s3 →
670  stack_preserved e s1 s3.
671#e1 #s1 #s2 #s3 #H1 inversion H1
672[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
673  #H2 inversion H2
674  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
675    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
676  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
677    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
678  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
679  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
680    inversion S2
681    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
682    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
683    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
684    ]
685  ]
686| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
687| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
688  cases (stack_preserved_final … H) #r #E destruct
689| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
690  @(absurd … F) //
691] qed.
692
693lemma stack_preserved_return : ∀ge,s1,s2,tr.
694  RTLabs_classify s1 = cl_return →
695  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
696  stack_preserved ends_with_ret s1 s2.
697#ge *
698[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
699  cases (lookup_present ??? (next f) (next_ok f)) in E;
700  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
701| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
702| #res #dst *
703  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
704    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
705  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
706    whd in EV:(??%?); destruct @(sp_finished ? f) //
707    cases f //
708  ]
709| #r #s2 #tr #E normalize in E; destruct
710] qed.
711
712lemma stack_preserved_step : ∀ge,s1,s2,tr.
713  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
714  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
715  stack_preserved doesnt_end_with_ret s1 s2.
716#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
717[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
718| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
719| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
720  normalize in CL; cases CL #E destruct
721| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
722| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
723  #E normalize in E; destruct
724| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
725] qed.
726
727lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
728  RTLabs_classify s1 = cl_call →
729  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
730  stack_preserved ends_with_ret s2 s3 →
731  stack_preserved doesnt_end_with_ret s1 s3.
732#ge #s1 #s2 #s3 #tr #CL #EV #SP
733cases (rtlabs_call_inv … CL)
734#fd * #args * #dst * #stk * #m #E destruct
735inversion SP
736[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
737| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
738  inversion (eval_perserves … EV)
739  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
740  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
741  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
742    inversion S
743    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
744    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
745    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
746    ]
747  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
748  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
749  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
750  ]
751| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
752  inversion (eval_perserves … EV)
753  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
754  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
755  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
756    inversion S1
757    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
758    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
759    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
760    ]
761  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
762  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
763  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
764  ]
765| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
766] qed.
767 
768lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
769  ∀CL : RTLabs_classify s1 = cl_call.
770  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
771  stack_preserved ends_with_ret s2 s3 →
772  as_after_return (RTLabs_status ge) «s1,CL» s3.
773#ge #s1 #s2 #s3 #tr #CL #EV #S23
774cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
775inversion S23
776[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
777| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
778  inversion (eval_perserves … EV)
779  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
780  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
781  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
782    inversion S
783    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
784    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
785    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
786    ]
787  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
788  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
789  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
790  ]
791| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
792  inversion (eval_perserves … EV)
793  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
794  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
795  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
796    inversion S1
797    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
798    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
799    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
800    ]
801  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
802  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
803  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
804  ]
805| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
806] qed.
807
808(* Don't need to know that labels break loops because we have termination. *)
809
810(* A bit of mucking around with the depth to avoid proving termination after
811   termination.  Note that we keep a proof that our upper bound on the length
812   of the termination proof is respected. *)
813record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
814  (start:state) (full:flat_trace io_out io_in ge start)
815  (original_terminates: will_return ge depth start full)
816  (T:state → Type[0]) (limit:nat) : Type[0] ≝
817{
818  new_state : state;
819  remainder : flat_trace io_out io_in ge new_state;
820  cost_labelled : well_cost_labelled_state new_state;
821  new_trace : T new_state;
822  stack_ok : stack_preserved ends start new_state;
823  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
824               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
825               | S d ⇒ ΣTM:will_return ge d new_state remainder.
826                         limit > will_return_length … TM ∧
827                         will_return_end … original_terminates = will_return_end … TM
828               ]
829}.
830
831(* The same with a flag indicating whether the function returned, as opposed to
832   encountering a label. *)
833record sub_trace_result (ge:genv) (depth:nat)
834  (start:state) (full:flat_trace io_out io_in ge start)
835  (original_terminates: will_return ge depth start full)
836  (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
837{
838  ends : trace_ends_with_ret;
839  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
840}.
841
842(* We often return the result from a recursive call with an addition to the
843   structured trace, so we define a couple of functions to help.  The bound on
844   the size of the termination proof might need to be relaxed, too. *)
845
846definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
847  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
848    will_return_end … TM1 = will_return_end … TM2 →
849    T2 (new_state … r) →
850    stack_preserved e s2 (new_state … r) →
851    trace_result ge d e s2 t2 TM2 T2 l2 ≝
852λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
853  mk_trace_result ge d e s2 t2 TM2 T2 l2
854    (new_state … r)
855    (remainder … r)
856    (cost_labelled … r)
857    trace
858    SP
859    ?
860    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
861                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
862     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
863.
864cases e in r ⊢ %;
865[ <TME -TME * cases d in TM1 TM2 ⊢ %;
866  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
867  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
868    %{TMa} % // @(transitive_le … lGE) @L1
869  ]
870| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
871   * #TMa * #L1 #TME
872    %{TMa} % // @(transitive_le … lGE) @L1
873] qed.
874
875definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
876  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
877    will_return_end … TM1 = will_return_end … TM2 →
878    T2 (ends … r) (new_state … r) →
879    stack_preserved (ends … r) s2 (new_state … r) →
880    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
881λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
882  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
883    (ends … r)
884    (replace_trace … lGE … r TME trace SP).
885
886(* Small syntax hack to avoid ambiguous input problems. *)
887definition myge : nat → nat → Prop ≝ ge.
888
889let rec make_label_return ge depth s
890  (trace: flat_trace io_out io_in ge s)
891  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
892  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
893  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
894  (TERMINATES: will_return ge depth s trace)
895  (TIME: nat)
896  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
897  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
898              (trace_label_return (RTLabs_status ge) s)
899              (will_return_length … TERMINATES) ≝
900             
901match TIME return λTIME. TIME ≥ ? → ? with
902[ O ⇒ λTERMINATES_IN_TIME. ⊥
903| S TIME ⇒ λTERMINATES_IN_TIME.
904
905  let r ≝ make_label_label ge depth s
906            trace
907            ENV_COSTLABELLED
908            STATE_COSTLABELLED
909            STATEMENT_COSTLABEL
910            TERMINATES
911            TIME ? in
912  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
913                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
914  [ ends_with_ret ⇒ λr.
915      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
916  | doesnt_end_with_ret ⇒ λr.
917      let r' ≝ make_label_return ge depth (new_state … r)
918                 (remainder … r)
919                 ENV_COSTLABELLED
920                 (cost_labelled … r) ?
921                 (pi1 … (terminates … r)) TIME ? in
922        replace_trace … r' ?
923          (tlr_step (RTLabs_status ge) s (new_state … r)
924            (new_state … r') (new_trace … r) (new_trace … r')) ?
925  ] (trace_res … r)
926
927] TERMINATES_IN_TIME
928
929
930and make_label_label ge depth s
931  (trace: flat_trace io_out io_in ge s)
932  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
933  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
934  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
935  (TERMINATES: will_return ge depth s trace)
936  (TIME: nat)
937  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
938  on TIME : sub_trace_result ge depth s trace TERMINATES
939              (λends. trace_label_label (RTLabs_status ge) ends s)
940              (will_return_length … TERMINATES) ≝
941             
942match TIME return λTIME. TIME ≥ ? → ? with
943[ O ⇒ λTERMINATES_IN_TIME. ⊥
944| S TIME ⇒ λTERMINATES_IN_TIME.
945
946let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
947  replace_sub_trace … r ?
948    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
949
950] TERMINATES_IN_TIME
951
952
953and make_any_label ge depth s
954  (trace: flat_trace io_out io_in ge s)
955  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
956  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
957  (TERMINATES: will_return ge depth s trace)
958  (TIME: nat)
959  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
960  on TIME : sub_trace_result ge depth s trace TERMINATES
961              (λends. trace_any_label (RTLabs_status ge) ends s)
962              (will_return_length … TERMINATES) ≝
963
964match TIME return λTIME. TIME ≥ ? → ? with
965[ O ⇒ λTERMINATES_IN_TIME. ⊥
966| S TIME ⇒ λTERMINATES_IN_TIME.
967
968  match trace return λs,trace. well_cost_labelled_state s →
969                               ∀TM:will_return ??? trace.
970                               myge ? (times 3 (will_return_length ??? trace TM)) →
971                               sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
972  [ ft_stop st FINAL ⇒
973      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
974
975  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
976    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
977    [ cl_other ⇒ λCL.
978        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
979        (* We're about to run into a label. *)
980        [ true ⇒ λCS.
981            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
982              doesnt_end_with_ret
983              (mk_trace_result ge … next trace' ?
984                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
985        (* An ordinary step, keep going. *)
986        | false ⇒ λCS.
987            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
988                replace_sub_trace … r ?
989                  (tal_step_default (RTLabs_status ge) (ends … r)
990                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
991        ] (refl ??)
992       
993    | cl_jump ⇒ λCL.
994        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
995          doesnt_end_with_ret
996          (mk_trace_result ge … next trace' ?
997            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
998           
999    | cl_call ⇒ λCL.
1000        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
1001        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
1002        (* We're about to run into a label, use base case for call *)
1003        [ true ⇒ λCS.
1004            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1005            doesnt_end_with_ret
1006            (mk_trace_result ge …
1007              (tal_base_call (RTLabs_status ge) start next (new_state … r)
1008                ? CL ? (new_trace … r) CS) ??)
1009        (* otherwise use step case *)
1010        | false ⇒ λCS.
1011            let r' ≝ make_any_label ge depth
1012                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
1013                       (pi1 … (terminates … r)) TIME ? in
1014            replace_sub_trace … r' ?
1015              (tal_step_call (RTLabs_status ge) (ends … r')
1016                start next (new_state … r) (new_state … r') ? CL ?
1017                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
1018        ] (refl ??)
1019
1020    | cl_return ⇒ λCL.
1021        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1022          ends_with_ret
1023          (mk_trace_result ge …
1024            next
1025            trace'
1026            ?
1027            (tal_base_return (RTLabs_status ge) start next ? CL)
1028            ?
1029            ?)
1030    ] (refl ? (RTLabs_classify start))
1031   
1032  | ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
1033 
1034  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
1035] TERMINATES_IN_TIME.
1036
1037[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1038| //
1039| //
1040| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1041| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1042| @(stack_preserved_join … (stack_ok … r)) //
1043| @(trace_label_label_label … (new_trace … r))
1044| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1045  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1046  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1047  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1048    @(monotonic_le_times_r 3 … LT)
1049  | @le_S @le_S @le_n
1050  ]
1051| @le_S_S_to_le @TERMINATES_IN_TIME
1052| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1053| @le_n
1054| //
1055| @le_S_S_to_le @TERMINATES_IN_TIME
1056| @(wrl_nonzero … TERMINATES_IN_TIME)
1057| (* We can't reach the final state because the function terminates with a
1058     return *)
1059  inversion TERMINATES
1060  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1061  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1062  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1063  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1064  ]
1065| @(will_return_return … CL TERMINATES)
1066| /2 by stack_preserved_return/
1067| %{tr} @EV
1068| @(well_cost_labelled_state_step  … EV) //
1069| whd @(will_return_notfn … TERMINATES) %2 @CL
1070| @stack_preserved_step /2/
1071| %{tr} @EV
1072| %1 whd @CL
1073| @(well_cost_labelled_jump … EV) //
1074| @(well_cost_labelled_state_step  … EV) //
1075| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1076  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1077    #TMx * #LT' #_ @LT'
1078  | <EQr cases (will_return_call … CL TERMINATES)
1079    #TM' * #_ #EQ' @EQ'
1080  ]
1081| @(stack_preserved_call … EV (stack_ok … r)) //
1082| %{tr} @EV
1083| @RTLabs_after_call //
1084| @(cost_labelled … r)
1085| skip
1086| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1087  @(transitive_lt … LT)
1088  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1089| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1090  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
1091| @RTLabs_after_call //
1092| %{tr} @EV
1093| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
1094| @(cost_labelled … r)
1095| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1096  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1097  cases (will_return_call … TERMINATES) in GT;
1098  #X * #Y #_ #Z
1099  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1100  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1101  | //
1102  ]
1103| @(well_cost_labelled_state_step  … EV) //
1104| @(well_cost_labelled_call … EV) //
1105| cases (will_return_call … TERMINATES)
1106  #TM * #GT #_ @le_S_S_to_le
1107  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1108  @(transitive_le … TERMINATES_IN_TIME)
1109  @(monotonic_le_times_r 3 … GT)
1110| whd @(will_return_notfn … TERMINATES) %1 @CL
1111| @(stack_preserved_step … EV) /2/
1112| %{tr} @EV
1113| %2 whd @CL
1114| @(well_cost_labelled_state_step  … EV) //
1115| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1116| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
1117| @CL
1118| %{tr} @EV
1119| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
1120| @(well_cost_labelled_state_step  … EV) //
1121| %1 @CL
1122| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1123  @le_S_S_to_le
1124  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1125  //
1126| inversion TERMINATES
1127  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
1128  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
1129  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
1130  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
1131  ]
1132] qed.
1133
1134(* We can initialise TIME with a suitably large value based on the length of the
1135   termination proof. *)
1136let rec make_label_return' ge depth s
1137  (trace: flat_trace io_out io_in ge s)
1138  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1139  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1140  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1141  (TERMINATES: will_return ge depth s trace)
1142  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1143make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1144  (2 + 3 * will_return_length … TERMINATES) ?.
1145@le_n
1146qed.
1147 
1148(* Tail-calls would not be handled properly (which means that if we try to show the
1149   full version with non-termination we'll fail because calls and returns aren't
1150   balanced.
1151 *)
1152
1153inductive inhabited (T:Type[0]) : Prop ≝
1154| witness : T → inhabited T.
1155
1156(* We also require that program's traces are soundly labelled: for any state
1157   in the execution, we can give a distance to a labelled state or termination.
1158   
1159   Note that this differs from the syntactic notions in earlier languages
1160   because it is a global property.  In principle, we would have a loop broken
1161   only by a call to a function (which necessarily has a label) and no local
1162   cost label.
1163 *)
1164
1165let rec nth_state ge s
1166  (trace: flat_trace io_out io_in ge s)
1167  n
1168  on n : option state ≝
1169match n with
1170[ O ⇒ Some ? s
1171| S n' ⇒
1172  match trace with
1173  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
1174  | _ ⇒ None ?
1175  ]
1176].
1177
1178definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
1179λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
1180
1181lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
1182  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
1183  soundly_labelled_trace ge s' trace'.
1184#ge #s #tr #s' #EV #trace' #H
1185#n cases (H (S n)) #m #H' %{m} @H'
1186qed.
1187
1188(* Define a notion of sound labellings of RTLabs programs. *)
1189
1190let rec successors (s : statement) : list label ≝
1191match s with
1192[ St_skip l ⇒ [l]
1193| St_cost _ l ⇒ [l]
1194| St_const _ _ _ l ⇒ [l]
1195| St_op1 _ _ _ _ _ l ⇒ [l]
1196| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
1197| St_load _ _ _ l ⇒ [l]
1198| St_store _ _ _ l ⇒ [l]
1199| St_call_id _ _ _ l ⇒ [l]
1200| St_call_ptr _ _ _ l ⇒ [l]
1201(*
1202| St_tailcall_id _ _ ⇒ [ ]
1203| St_tailcall_ptr _ _ ⇒ [ ]
1204*)
1205| St_cond _ l1 l2 ⇒ [l1; l2]
1206| St_jumptable _ ls ⇒ ls
1207| St_return ⇒ [ ]
1208].
1209
1210definition actual_successor : state → option label ≝
1211λs. match s with
1212[ State f fs m ⇒ Some ? (next f)
1213| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1214| Returnstate _ _ _ _ ⇒ None ?
1215| Finalstate _ ⇒ None ?
1216].
1217
1218lemma nth_opt_Exists : ∀A,n,l,a.
1219  nth_opt A n l = Some A a →
1220  Exists A (λa'. a' = a) l.
1221#A #n elim n
1222[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1223| #m #IH *
1224  [ #a #E normalize in E; destruct
1225  | #a #l #a' #E %2 @IH @E
1226  ]
1227] qed.
1228
1229lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1230  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1231  RTLabs_classify s' = cl_return ∨
1232  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1233#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1234whd in ⊢ (??%? → ?);
1235generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1236[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1237| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1238| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1239| #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} % // % //
1240| #ty1 #ty2 #ty' #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} % // % //
1241| #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} % // % //
1242| #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} % // % //
1243| #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} % // % //
1244| #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} % // % //
1245| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
1246| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
1247  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 ]
1248  whd in ⊢ (??%? → ?);
1249  generalize in ⊢ (??(?%)? → ?);
1250  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1251  [ #e #E normalize in E; destruct
1252  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1253  ]
1254| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
1255] qed.
1256
1257definition steps_for_statement : statement → nat ≝
1258λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
1259
1260inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
1261| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
1262| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
1263with bound_on_steps_to_cost1 : label → nat → Prop ≝
1264| bostc_step : ∀l,n,H.
1265    let stmt ≝ lookup_present … g l H in
1266    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1267          bound_on_steps_to_cost g l' n) →
1268    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
1269
1270(*
1271lemma steps_to_label_bound_inv : ∀g,l,n.
1272  steps_to_label_bound g l n →
1273  ∀H. let stmt ≝ lookup_present … g l H in
1274  ∃n'. n = steps_for_statement stmt + n' ∧
1275  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1276        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
1277        steps_to_label_bound g l' n').
1278#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
1279% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
1280qed.
1281  *) 
1282
1283(*
1284definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1285
1286let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1287  soundly_labelled_pc (f_graph fn) (f_entry fn).
1288
1289
1290definition soundly_labelled_frame : frame → Prop ≝
1291λf. soundly_labelled_pc (f_graph (func f)) (next f).
1292
1293definition soundly_labelled_state : state → Prop ≝
1294λs. match s with
1295[ State f _ _ ⇒ soundly_labelled_frame f
1296| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1297| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1298].
1299*)
1300definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1301λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1302definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1303λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1304
1305inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1306| 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
1307| 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)
1308| 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)
1309.
1310
1311lemma state_bound_on_steps_to_cost_zero : ∀s.
1312  ¬ state_bound_on_steps_to_cost s O.
1313#s % #H inversion H
1314[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1315  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1316  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1317| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1318| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1319] qed.
1320
1321lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1322  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1323  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1324  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
1325#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1326whd in ⊢ (??%? → ?);
1327generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1328[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1329| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1330| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1331| #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
1332| #ty1 #ty2 #ty' #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
1333| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1334| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1335| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1336| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1337| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1338| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
1339  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 ]
1340  whd in ⊢ (??%? → ?);
1341  generalize in ⊢ (??(?%)? → ?);
1342  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1343  [ #e #E normalize in E; destruct
1344  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1345  ]
1346| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1347] qed.
1348
1349lemma bound_after_call : ∀ge,s,s',n.
1350  state_bound_on_steps_to_cost s (S n) →
1351  ∀CL:RTLabs_classify s = cl_call.
1352  as_after_return (RTLabs_status ge) «s, CL» s' →
1353  RTLabs_cost s' = false →
1354  state_bound_on_steps_to_cost s' n.
1355#ge #s #s' #n #H inversion H
1356[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1357  #fn * #args * #dst * #stk * #m' #E destruct
1358| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1359  whd in S; #CL cases s'
1360  [ #f' #fs' #m' * #N #F #CS
1361    %1 whd
1362    inversion S
1363    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1364      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1365    | #l #n #B #E1 #E2 #_ destruct <N <F @B
1366    ]
1367  | #fd' #args' #dst' #fs' #m' *
1368  | #rv #dst' #fs' #m' *
1369  | #r #E normalize in E; destruct
1370  ]
1371| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1372] qed.
1373
1374lemma bound_after_step : ∀ge,s,tr,s',n.
1375  state_bound_on_steps_to_cost s (S n) →
1376  eval_statement ge s = Value ??? 〈tr, s'〉 →
1377  RTLabs_cost s' = false →
1378  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1379   state_bound_on_steps_to_cost s' n.
1380#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1381[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1382  #EVAL cases (eval_successor … EVAL)
1383  [ /3/
1384  | * #l * #S1 #S2 #NC %2
1385  (*
1386    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1387    *)
1388    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1389    inversion (eval_perserves … EVAL)
1390    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1391      >(eval_steps … EVAL) in E2; #En normalize in En;
1392      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1393      %1 inversion (IH … S2)
1394      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1395        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1396        whd in S1:(??%?); destruct >NC in CSx; *
1397      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
1398      ]
1399    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1400      >(eval_steps … EVAL) in E2; #En normalize in En;
1401      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1402      %2 @IH normalize in S1; destruct @S2
1403    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1404      destruct
1405    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1406      normalize in S1; destruct
1407    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1408    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1409    ]
1410  ]
1411| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1412  /3/
1413| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1414  #EVAL #NC %2 inversion (eval_perserves … EVAL)
1415  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1416  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1417  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1418  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1419  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1420    %1 whd in FS ⊢ %;
1421    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
1422    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
1423    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 ]
1424    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1425    inversion FS
1426    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1427        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
1428        >NC in CSx; *
1429    | #lx #nx #H #E1x #E2x #_ destruct @H
1430    ]
1431  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1432  ]
1433] qed.
1434
1435
1436
1437
1438definition soundly_labelled_fn : internal_function → Prop ≝
1439λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
1440
1441definition soundly_labelled_ge : genv → Prop ≝
1442λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1443
1444definition soundly_labelled_state : state → Prop ≝
1445λs. match s with
1446[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1447| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1448                          All ? (λf. soundly_labelled_fn (func f)) fs
1449| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1450| Finalstate _ ⇒ True
1451].
1452
1453lemma steps_from_sound : ∀s.
1454  RTLabs_cost s = true →
1455  soundly_labelled_state s →
1456  ∃n. state_bound_on_steps_to_cost s n.
1457* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
1458whd in ⊢ (% → ?); * #SLF #_
1459cases (SLF (next f) (next_ok f)) #n #B1
1460%{n} % @B1
1461qed.
1462
1463lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1464  soundly_labelled_ge ge →
1465  eval_statement ge s = Value ??? 〈tr,s'〉 →
1466  soundly_labelled_state s →
1467  soundly_labelled_state s'.
1468#ge #s #tr #s' #ENV #EV #S
1469inversion (eval_perserves … EV)
1470[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1471  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1472| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1473  whd in S ⊢ %; %
1474  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1475  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1476  ]
1477| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1478  whd in S ⊢ %; @S
1479| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1480  whd in S ⊢ %; cases S //
1481| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
1482  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1483| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1484] qed.
1485
1486lemma soundly_labelled_state_preserved : ∀s,s'.
1487  stack_preserved ends_with_ret s s' →
1488  soundly_labelled_state s →
1489  soundly_labelled_state s'.
1490#s0 #s0' #SP inversion SP
1491[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1492| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
1493  inversion S1
1494  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
1495    * #_ #S whd in S;
1496    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1497    destruct @S
1498  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
1499    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1500    destruct @S
1501  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
1502    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1503    destruct @S
1504  ]
1505| //
1506| //
1507] qed.
1508
1509(* When constructing an infinite trace, we need to be able to grab the finite
1510   portion of the trace for the next [trace_label_diverges] constructor.  We
1511   use the fact that the trace is soundly labelled to achieve this. *)
1512
1513record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1514  ro_well_cost_labelled: well_cost_labelled_state s;
1515  ro_soundly_labelled: soundly_labelled_state s;
1516  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1517  ro_not_undefined: not_wrong … t;
1518  ro_not_final: RTLabs_is_final s = None ?
1519}.
1520
1521inductive finite_prefix (ge:genv) : state → Prop ≝
1522| fp_tal : ∀s,s'.
1523           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1524           ∀t:flat_trace io_out io_in ge s'.
1525           remainder_ok ge s' t →
1526           finite_prefix ge s
1527| fp_tac : ∀s1,s2,s3,tr.
1528           trace_any_call (RTLabs_status ge) s1 s2 →
1529           well_cost_labelled_state s2 →
1530           eval_statement ge s2 = Value ??? 〈tr,s3〉 →
1531           ∀t:flat_trace io_out io_in ge s3.
1532           remainder_ok ge s3 t →
1533           finite_prefix ge s1
1534.
1535
1536definition fp_add_default : ∀ge,s,s'.
1537  RTLabs_classify s = cl_other →
1538  finite_prefix ge s' →
1539  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
1540  RTLabs_cost s' = false →
1541  finite_prefix ge s ≝
1542λge,s,s',OTHER,fp.
1543match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
1544[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1545    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1546    rem rok
1547| fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr
1548    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1549    WCL2 EV rem rok
1550].
1551
1552definition fp_add_terminating_call : ∀ge,s,s1,s''.
1553  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
1554  ∀CALL:RTLabs_classify s = cl_call.
1555  finite_prefix ge s'' →
1556  trace_label_return (RTLabs_status ge) s1 s'' →
1557  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1558  RTLabs_cost s'' = false →
1559  finite_prefix ge s ≝
1560λge,s,s1,s'',EVAL,CALL,fp.
1561match 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
1562[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1563    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1564    rem rok
1565| fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr
1566    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1567    WCL2 EV rem rok
1568].
1569
1570lemma not_return_to_not_final : ∀ge,s,tr,s'.
1571  eval_statement ge s = Value ??? 〈tr, s'〉 →
1572  RTLabs_classify s ≠ cl_return →
1573  RTLabs_is_final s' = None ?.
1574#ge #s #tr #s' #EV
1575inversion (eval_perserves … EV) //
1576#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1577@⊥ @(absurd ?? CL) @refl
1578qed.
1579
1580definition termination_oracle ≝ ∀ge,depth,s,trace.
1581  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1582
1583let rec finite_segment ge s n trace
1584  (ORACLE: termination_oracle)
1585  (TRACE_OK: remainder_ok ge s trace)
1586  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1587  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1588  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1589  on n : finite_prefix ge s ≝
1590match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1591[ O ⇒ λLABEL_LIMIT. ⊥
1592| S n' ⇒
1593    match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
1594    [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1595    | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT.
1596        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1597        [ cl_other ⇒ λCL.
1598            let TRACE_OK' ≝ ? in
1599            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1600            [ true ⇒ λCS.
1601                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
1602            | false ⇒ λCS.
1603                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1604                fp_add_default ge ?? CL fs ? CS
1605            ] (refl ??)
1606        | cl_jump ⇒ λCL.
1607            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ?
1608        | cl_call ⇒ λCL.
1609            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
1610            [ or_introl TERMINATES ⇒
1611              match TERMINATES with [ witness TERMINATES ⇒
1612                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1613                let TRACE_OK' ≝ ? in
1614                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
1615                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) TRACE_OK'
1616                | false ⇒ λCS.
1617                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1618                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
1619                ] (refl ??)
1620              ]
1621            | or_intror NO_TERMINATION ⇒
1622                fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ?
1623            ]
1624        | cl_return ⇒ λCL. ⊥
1625        ] (refl ??)
1626    | ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1627    ] TRACE_OK
1628] LABEL_LIMIT.
1629[ cases (state_bound_on_steps_to_cost_zero s) /2/
1630| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1631| @(absurd ?? (ro_no_termination … TRACE_OK))
1632     %{0} % @wr_base //
1633| @(well_cost_labelled_jump … EV) /2/
1634| 5,6,8,9,10,11: /3/
1635| % [ @(well_cost_labelled_state_step … EV) /2/
1636    | @(soundly_labelled_state_step … EV) /2/
1637    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1638    | @(still_not_wrong … EV) /2/
1639    | @(not_return_to_not_final … EV) >CL % #E destruct
1640    ]
1641| /2/
1642| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
1643  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
1644| % [ /2/
1645    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
1646      @(soundly_labelled_state_step … EV) /2/
1647    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1648      @wr_call //
1649      @(will_return_prepend … TERMINATES … TM1)
1650      cases (terminates … tlr) //
1651    | @(will_return_not_wrong … TERMINATES)
1652      [ @(still_not_wrong … EV) /2/
1653      | cases (terminates … tlr) //
1654      ]
1655    | (* By stack preservation we cannot be in the final state *)
1656      inversion (stack_ok … tlr)
1657      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1658      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1659      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
1660        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
1661        inversion (eval_perserves … EV)
1662        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
1663        #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1664        inversion S
1665        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
1666        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1667           so we can use it as a witness that at least one frame exists *)
1668        inversion LABEL_LIMIT
1669        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1670      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1671      ]
1672    ]
1673| @(well_cost_labelled_state_step … EV) /2/
1674| @(well_cost_labelled_call … EV) /2/
1675| /2/
1676| % [ @(well_cost_labelled_state_step … EV) /2/
1677    | @(soundly_labelled_state_step … EV) /2/
1678    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1679      @(will_return_lower … TM) //
1680    | @(still_not_wrong … EV) /2/
1681    | @(not_return_to_not_final … EV) >CL % #E destruct
1682    ]
1683| 19,20,21: /2/
1684| cases (bound_after_step … LABEL_LIMIT EV ?)
1685  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
1686    inversion trace'
1687    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1688      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1689      % >CL #E destruct
1690    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1691      @wr_base //
1692    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
1693      inversion (ro_not_undefined … TRACE_OK)
1694      [ #H137 #H138 #H139 #H140 #H141 destruct
1695      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
1696        inversion H148
1697        [ #H153 #H154 #H155 #H156 #H157 destruct
1698        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
1699        ]
1700      ]
1701    ]
1702    ]
1703    | >CL #E destruct
1704    ]
1705  | //
1706  | //
1707  ]
1708| % [ @(well_cost_labelled_state_step … EV) /2/
1709    | @(soundly_labelled_state_step … EV) /2/
1710    | @(not_to_not … (ro_no_termination … TRACE_OK))
1711      * #depth * #TERM %{depth} % @wr_step /2/
1712    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
1713    | @(not_return_to_not_final … EV) >CL % #E destruct
1714    ]
1715| inversion (ro_not_undefined … TRACE_OK)
1716  [ #H169 #H170 #H171 #H172 #H173 destruct
1717  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
1718  ]
1719] qed.
1720
1721(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1722       a trace_label_diverges value, but I only know how to construct those
1723       using a cofixpoint in Type[0], which means I can't use the termination
1724       oracle.
1725*)
1726
1727let corec make_label_diverges ge s
1728  (trace: flat_trace io_out io_in ge s)
1729  (ORACLE: termination_oracle)
1730  (TRACE_OK: remainder_ok ge s trace)
1731  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1732  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1733  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1734  : trace_label_diverges_exists (RTLabs_status ge) s ≝
1735match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
1736[ ex_intro n B ⇒
1737    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
1738      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1739    with
1740    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1741        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1742            tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
1743(*
1744        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1745        [ ex_intro T' _ ⇒
1746            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1747        ]*)
1748    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1749        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1750            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
1751(*
1752        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1753        [ ex_intro T' _ ⇒
1754            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1755        ]*)
1756    ] STATEMENT_COSTLABEL
1757].
1758[ @(trace_any_label_label … T)
1759| %{tr} @EV
1760| @(trace_any_call_call … T)
1761| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
1762] qed.
1763
1764lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'.
1765  make_initial_state p = OK ? s1 →
1766  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
1767  stack_preserved ends_with_ret s2 s' →
1768  RTLabs_is_final s' ≠ None ?.
1769#ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?);
1770@bind_ok #m #_
1771@bind_ok #b #_
1772@bind_ok #f #_
1773#E destruct
1774#EV #SP inversion (eval_perserves … EV)
1775[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
1776     inversion SP
1777     [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct
1778     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct
1779          inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct
1780     ]
1781| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct
1782] qed.
1783
1784lemma initial_state_is_call : ∀p,s.
1785  make_initial_state p = OK ? s →
1786  RTLabs_classify s = cl_call.
1787#p #s whd in ⊢ (??%? → ?);
1788@bind_ok #m #_
1789@bind_ok #b #_
1790@bind_ok #f #_
1791#E destruct
1792@refl
1793qed.
1794
1795let rec whole_structured_trace_exists ge p s
1796  (trace: flat_trace io_out io_in ge s)
1797  (ORACLE: termination_oracle)
1798  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1799  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1800  : ∀INITIAL: make_initial_state p = OK ? s.
1801    ∀NOT_WRONG: not_wrong ??? s trace.
1802    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
1803    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
1804    trace_whole_program_exists (RTLabs_status ge) s ≝
1805match trace return λs,trace. make_initial_state p = OK ? s →
1806                             not_wrong ??? s trace →
1807                             well_cost_labelled_state s →
1808                             soundly_labelled_state s →
1809                             trace_whole_program_exists (RTLabs_status ge) s with
1810[ ft_step s tr next EV trace' ⇒ λINITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
1811    let IS_CALL ≝ initial_state_is_call … INITIAL in
1812    match ORACLE ge O next trace' with
1813    [ or_introl TERMINATES ⇒
1814        match TERMINATES with
1815        [ witness TERMINATES ⇒
1816          let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1817          twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
1818        ]
1819    | or_intror NO_TERMINATION ⇒
1820        twp_diverges (RTLabs_status ge) s next IS_CALL ?
1821         (make_label_diverges ge next trace' ORACLE ?
1822            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1823    ]
1824| ft_stop st FINAL ⇒ λINITIAL,NOT_WRONG. ⊥
1825| ft_wrong start m NF EV ⇒ λINITIAL,NOT_WRONG. ⊥
1826].
1827[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
1828  cases FINAL #E @E @refl
1829| %{tr} @EV
1830| @(after_the_initial_call_is_the_final_state … INITIAL EV)
1831  @(stack_ok … tlr)
1832| @(well_cost_labelled_state_step … EV) //
1833| @(well_cost_labelled_call … EV) //
1834| %{tr} @EV
1835| @(well_cost_labelled_call … EV) //
1836| % [ @(well_cost_labelled_state_step … EV) //
1837    | @(soundly_labelled_state_step … EV) //
1838    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1839    | @(still_not_wrong … NOT_WRONG)
1840    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1841    ]
1842| inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
1843] qed.
1844
1845definition well_cost_labelled_program : RTLabs_program → Prop ≝
1846  λp. All ? (λx. let 〈id,fd〉 ≝ x in
1847                 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
1848(*
1849theorem program_trace_exists :
1850  termination_oracle →
1851  ∀p:RTLabs_program.
1852  ∀s:state.
1853  ∀I: make_initial_state p = OK ? s.
1854 
1855  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1856 
1857  ∀NOIO:exec_no_io … plain_trace.
1858 
1859  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
1860 
1861  trace_whole_program_exists (RTLabs_status (make_global p)) s.
1862#ORACLE #p #s #I
1863letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1864#NOIO
1865letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
1866whd
1867@(whole_structured_trace_exists … flat_trace)
1868//
1869[ whd
1870*)
1871
1872(* as_execute might be in Prop, but because the semantics is deterministic
1873   we can retrieve the event trace anyway. *)
1874let rec deprop_as_execute ge s s'
1875  (X:as_execute (RTLabs_status ge) s s')
1876: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1877match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ? with
1878[ Value ts ⇒ λY. «fst … ts, ?»
1879| _ ⇒ λY. ⊥
1880] X.
1881[ 1,3: cases Y #x #E destruct
1882| cases Y #trP #E destruct @refl
1883] qed.
1884
1885(* A non-empty finite section of a flat_trace *)
1886inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1887| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1888| pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''.
1889
1890let rec append_partial_flat_trace o i ge s1 s2 s3
1891  (tr1:partial_flat_trace o i ge s1 s2)
1892on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1893match tr1 with
1894[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1895| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1896].
1897
1898let rec partial_to_flat_trace o i ge s1 s2
1899  (tr:partial_flat_trace o i ge s1 s2)
1900on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1901match tr with
1902[ pft_base s tr s' EX ⇒ ft_step … EX
1903| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1904].
1905
1906(* Extract a flat trace from a structured one. *)
1907let rec flatten_trace_label_return ge s s'
1908  (tr:trace_label_return (RTLabs_status ge) s s')
1909on tr :
1910  partial_flat_trace io_out io_in ge s s' ≝
1911match tr with
1912[ tlr_base s1 s2 tll ⇒ flatten_trace_label_label ge ends_with_ret s1 s2 tll
1913| tlr_step s1 s2 s3 tll tlr ⇒
1914  append_partial_flat_trace …
1915    (flatten_trace_label_label ge doesnt_end_with_ret s1 s2 tll)
1916    (flatten_trace_label_return ge s2 s3 tlr)
1917]
1918and flatten_trace_label_label ge ends s s'
1919  (tr:trace_label_label (RTLabs_status ge) ends s s')
1920on tr :
1921  partial_flat_trace io_out io_in ge s s' ≝
1922match tr with
1923[ tll_base e s1 s2 tal _ ⇒ flatten_trace_any_label ge e s1 s2 tal
1924]
1925and flatten_trace_any_label ge ends s s'
1926  (tr:trace_any_label (RTLabs_status ge) ends s s')
1927on tr :
1928  partial_flat_trace io_out io_in ge s s' ≝
1929match tr with
1930[ tal_base_not_return s1 s2 EX CL CS ⇒
1931    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1932    pft_base … EX' ]
1933| tal_base_return s1 s2 EX CL ⇒
1934    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1935    pft_base … EX' ]
1936| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
1937    let suffix' ≝ flatten_trace_label_return ge ?? tlr in
1938    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1939    pft_step … EX' suffix' ]
1940| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
1941    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1942    pft_step … EX'
1943      (append_partial_flat_trace …
1944        (flatten_trace_label_return ge ?? tlr)
1945        (flatten_trace_any_label ge ??? tal))
1946    ]
1947| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
1948    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1949      pft_step … EX' (flatten_trace_any_label ge ??? tal)
1950    ]
1951].
1952
1953
1954(* We take an extra step so that we can always return a non-empty trace to
1955   satisfy the guardedness condition in the cofixpoint. *)
1956let rec flatten_trace_any_call ge s s' s'' et
1957  (tr:trace_any_call (RTLabs_status ge) s s')
1958  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1959on tr :
1960  partial_flat_trace io_out io_in ge s s'' ≝
1961match tr return λs,s'.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
1962[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
1963| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
1964    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
1965    pft_step … EX'
1966      (append_partial_flat_trace …
1967        (flatten_trace_label_return ge ?? tlr)
1968        (flatten_trace_any_call ge … tac EX''))
1969    ]
1970| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
1971    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1972    pft_step … EX'
1973     (flatten_trace_any_call ge … tal EX'')
1974    ]
1975] EX''.
1976
1977let rec flatten_trace_label_call ge s s' s'' et
1978  (tr:trace_label_call (RTLabs_status ge) s s')
1979  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1980on tr :
1981  partial_flat_trace io_out io_in ge s s'' ≝
1982match tr with
1983[ tlc_base s1 s2 tac CS ⇒ flatten_trace_any_call … tac
1984] EX''.
1985
1986(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
1987   to take care to satisfy the guardedness condition by witnessing the fact that
1988   the partial traces are non-empty. *)
1989let corec flatten_trace_label_diverges ge s
1990  (tr:trace_label_diverges (RTLabs_status ge) s)
1991: flat_trace io_out io_in ge s ≝
1992match tr with
1993[ tld_step sx sy tll tld ⇒
1994    match flatten_trace_label_label ge … tll with
1995    [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld)
1996    | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
1997    ] tld
1998| tld_base s1 s2 s3 tlc EX CL tld ⇒
1999    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2000      match flatten_trace_label_call … tlc EX' with
2001      [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld)
2002      | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
2003      ] tld
2004    ]
2005]
2006(* Helper to keep adding the partial trace without violating the guardedness
2007   condition. *)
2008and add_partial_flat_trace ge s s'
2009  (ptr:partial_flat_trace io_out io_in ge s s')
2010  (tr:trace_label_diverges (RTLabs_status ge) s')
2011: flat_trace io_out io_in ge s ≝
2012match ptr with
2013[ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flatten_trace_label_diverges ge s' tr)
2014| pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr)
2015] tr
2016.
2017
2018coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2019| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2020| eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2)
2021| eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX).
2022
2023(* XXX move to semantics *)
2024lemma final_cannot_move : ∀ge,s.
2025  RTLabs_is_final s ≠ None ? →
2026  ∃err. eval_statement ge s = Wrong ??? err.
2027#ge *
2028[ #f #fs #m * #F cases (F ?) @refl
2029| #a #b #c #d #e * #F cases (F ?) @refl
2030| #a #b #c #d * #F cases (F ?) @refl
2031| #r #F % [2: @refl | skip ]
2032] qed.
2033
2034let corec flat_traces_are_determined_by_starting_point ge s tr1
2035: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2036match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2037[ ft_stop s F ⇒ λtr2. ?
2038| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2039    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2040    [ ft_stop s F ⇒ λEX. ?
2041    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2042    | ft_wrong s m NF EX' ⇒ λEX. ?
2043    ] EX0
2044| ft_wrong s m NF EX ⇒ λtr2. ?
2045].
2046[ inversion tr2 in tr1 F;
2047  [ #s #F #_ #_ #tr1 #F' @eft_stop
2048  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2049    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2050  | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/
2051  ]
2052| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2053| -EX0
2054  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2055  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2056  -E -EX' -tr2' #tr2' #EX'
2057  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2058  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2059  -E -EX' #EX'
2060    @eft_step @flat_traces_are_determined_by_starting_point
2061| @⊥ >EX in EX'; #E destruct
2062| inversion tr2 in NF EX;
2063  [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/
2064  | #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct
2065  | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.
2066    #E destruct
2067    @eft_wrong
2068  ]
2069] qed.
2070
2071let corec diverging_traces_have_unique_flat_trace ge s
2072  (str:trace_label_diverges (RTLabs_status ge) s)
2073  (tr:flat_trace io_out io_in ge s)
2074: equal_flat_traces … (flatten_trace_label_diverges … str) tr ≝ ?.
2075@flat_traces_are_determined_by_starting_point
2076qed.
2077
2078let rec flatten_trace_whole_program ge s
2079  (tr:trace_whole_program (RTLabs_status ge) s)
2080on tr : flat_trace io_out io_in ge s ≝
2081match tr with
2082[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2083    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2084      ft_step … EX' (partial_to_flat_trace … (flatten_trace_label_return … tlr) (ft_stop … sf F))
2085    ]
2086| twp_diverges s1 s2 CL EX tld ⇒
2087    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2088      ft_step … EX' (flatten_trace_label_diverges … tld)
2089    ]
2090].
2091
2092let corec whole_traces_have_unique_flat_trace ge s
2093  (str:trace_whole_program (RTLabs_status ge) s)
2094  (tr:flat_trace io_out io_in ge s)
2095: equal_flat_traces … (flatten_trace_whole_program … str) tr ≝ ?.
2096@flat_traces_are_determined_by_starting_point
2097qed.
Note: See TracBrowser for help on using the repository browser.