Context Navigation

RTLabs_traces.ma @ 2695

Last change on this file since 2695 was 2677, checked in by campbell, 8 years ago
Retain the pointer for the function called in front-end call states so that we can do sensible stack costs.
File size: 126.4 KB

Line
1
2	include "RTLabs/RTLabs_abstract.ma".
3	include "RTLabs/CostSpec.ma".
4	include "RTLabs/CostMisc.ma".
5	include "common/Executions.ma".
6	include "utilities/listb.ma".
7
8
9	(* Allow us to move between the different notions of when a state is cost
10	labelled. *)
11
12	lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
13	RTLabs_cost s = true ↔
14	as_costed (RTLabs_status ge) s.
15	cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
16	#ge * *
17	[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
18	whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
19	whd in match (as_pc_of ??);
20	cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
21	whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
22	whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
23	>(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
24	% cases (lookup_present ?? (f_graph func) ??) normalize
25	#A try #B try #C try #D try #E try #F try #G try #H try #G destruct
26	try (% #E' destruct)
27	cases (NONE ?) assumption
28	\| #vf #fd #args #dst #fs #m #stk #mtc %
29	[ #E normalize in E; destruct
30	\| whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
31	cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
32	#H cases (NONE H)
33	]
34	\| #v #dst #fs #m #stk #mtc %
35	[ #E normalize in E; destruct
36	\| whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
37	cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
38	#H cases (NONE H)
39	]
40	\| #r #stk #mtc %
41	[ #E normalize in E; destruct
42	\| #E normalize in E; cases (NONE E)
43	]
44	] qed.
45
46	lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
47	RTLabs_cost s = false →
48	¬ as_costed (RTLabs_status ge) s.
49	#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
50	qed.
51
52	(* Before attempting to construct a structured trace, let's show that we can
53	form flat traces with evidence that they were constructed from an execution.
54	As with the structured traces, we only consider good traces (i.e., ones
55	which don't go wrong).
56
57	For now we don't consider I/O. *)
58
59
60	coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
61	\| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
62	\| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
63	\| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
64
65	(* add I/O? *)
66	coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
67	\| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
68	\| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s.
69
70	let corec make_flat_trace ge s
71	(NF:RTLabs_is_final s = None ?)
72	(NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s)))
73	(H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
74	flat_trace io_out io_in ge s ≝
75	let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
76	match e return λx. e = x → ? with
77	[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
78	\| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???)
79	\| e_wrong m ⇒ λE. ⊥
80	\| e_interact o f ⇒ λE. ⊥
81	] (refl ? e).
82	[ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E;
83	cases (eval_statement ge s)
84	[ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
85	\| 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
86	>(?:is_final ????? = RTLabs_is_final s1) //
87	lapply (refl ? (RTLabs_is_final s1))
88	cases (RTLabs_is_final s1) in ⊢ (???% → %);
89	[ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
90	\| #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
91	\| #i #E whd in ⊢ (??%? → ?); #E2 destruct
92	]
93	\| *: #m whd in ⊢ (??%? → ?); #E destruct
94	]
95	\| whd in E:(??%?); >exec_inf_aux_unfold in E;
96	cases (eval_statement ge s)
97	[ #o #K whd in ⊢ (??%? → ?); #E destruct
98	\| * #tr #s1 whd in ⊢ (??%? → ?);
99	lapply (refl ? (RTLabs_is_final s1))
100	change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?\|_⇒?])? → ?);
101	cases (RTLabs_is_final s1) in ⊢ (???% → %);
102	[ #F #E whd in E:(??%?); destruct
103	\| #r #F #E whd in E:(??%?); destruct >F % #E destruct
104	]
105	\| #m #E whd in E:(??%?); destruct
106	]
107	\| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
108	cases (eval_statement ge s)
109	[ #O #K whd in ⊢ (??%? → ?); #E destruct
110	\| * #tr #s1 whd in ⊢ (??%? → ?);
111	cases (is_final ?????)
112	[ whd in ⊢ (??%? → ?); #E
113	change with (eval_statement ge s1) in E:(??(??????(?????%))?);
114	destruct
115	inversion H
116	[ #a #b #c #E1 destruct
117	\| #trx #sx #ex #H1 #E2 #E3 destruct @H1
118	\| #m #E1 destruct
119	]
120	\| #i whd in ⊢ (??%? → ?); #E destruct
121	]
122	\| #m whd in ⊢ (??%? → ?); #E destruct
123	]
124	\| whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E;
125	cases (eval_statement ge s)
126	[ #O #K whd in ⊢ (??%? → ?); #E destruct
127	\| * #tr #s1 whd in ⊢ (??%? → ?);
128	cases (is_final ?????)
129	[ whd in ⊢ (??%? → ?); #E
130	change with (eval_statement ge s1) in E:(??(??????(?????%))?);
131	destruct
132	inversion NW
133	[ #a #b #c #E1 #_ destruct
134	\| #trx #sx #ex #H1 #E2 #E3 destruct @H1
135	\| #o #k #K #E1 destruct
136	]
137	\| #i whd in ⊢ (??%? → ?); #E destruct
138	]
139	\| #m whd in ⊢ (??%? → ?); #E destruct
140	]
141	\| whd in E:(??%?); >exec_inf_aux_unfold in E;
142	cases (eval_statement ge s)
143	[ #o #K whd in ⊢ (??%? → ?); #E destruct
144	\| * #tr #s1 whd in ⊢ (??%? → ?);
145	lapply (refl ? (RTLabs_is_final s1))
146	change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?\|_⇒?])? → ?);
147	cases (RTLabs_is_final s1) in ⊢ (???% → %);
148	[ #F #E whd in E:(??%?); destruct @F
149	\| #r #F #E whd in E:(??%?); destruct
150	]
151	\| #m #E whd in E:(??%?); destruct
152	]
153	\| whd in E:(??%?); >E in NW; #X inversion X
154	#A #B #C #D #E destruct
155	\| whd in E:(??%?); >E in H; #H inversion H
156	#A #B #C try #D try #E destruct
157	] qed.
158
159	definition make_whole_flat_trace : ∀p,s.
160	exec_no_io … (exec_inf … RTLabs_fullexec p) →
161	not_wrong … (exec_inf … RTLabs_fullexec p) →
162	make_initial_state ??? p = OK ? s →
163	flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
164	λp,s,H,NW,I.
165	let ge ≝ make_global … p in
166	let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
167	match e return λx. e = x → ? with
168	[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
169	\| e_step _ _ e' ⇒ λE. make_flat_trace ge s ???
170	\| e_wrong m ⇒ λE. ⊥
171	\| e_interact o f ⇒ λE. ⊥
172	] (refl ? e).
173	[ whd in E:(??%?); >exec_inf_aux_unfold in E;
174	whd in ⊢ (??%? → ?);
175	change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?\|_⇒?])? → ?);
176	cases (RTLabs_is_final s)
177	[ #E whd in E:(??%?); destruct
178	\| #r #E % #E' destruct
179	]
180	\| @(initial_state_is_not_final … I)
181	\| whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?);
182	>exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????)
183	[ whd in ⊢ (??%? → ??% → ?); #E #H inversion H
184	[ #a #b #c #E1 destruct
185	\| #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
186	@H1
187	\| #o #k #K #E1 destruct
188	]
189	\| #i whd in ⊢ (??%? → ??% → ?); #E destruct
190	]
191	\| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
192	>exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
193	[ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
194	[ #a #b #c #E1 destruct
195	\| #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
196	@H1
197	\| #m #E1 destruct
198	]
199	\| #i whd in ⊢ (??%? → ???% → ?); #E destruct
200	]
201	\| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
202	cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
203	\| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
204	cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
205	] qed.
206
207	(* Need a way to choose whether a called function terminates. Then,
208	if the initial function terminates we generate a purely inductive structured trace,
209	otherwise we start generating the coinductive one, and on every function call
210	use the choice method again to decide whether to step over or keep going.
211
212	Not quite what we need - have to decide on seeing each label whether we will see
213	another or hit a non-terminating call?
214
215	Also - need the notion of well-labelled in order to break loops.
216
217
218
219	outline:
220
221	does function terminate?
222	- yes, get (bound on the number of steps until return), generate finite
223	structure using bound as termination witness
224	- no, get (¬ bound on steps to return), start building infinite trace out of
225	finite steps. At calls, check for termination, generate appr. form.
226
227	generating the finite parts:
228
229	We start with the status after the call has been executed; well-labelling tells
230	us that this is a labelled state. Now we want to generate a trace_label_return
231	and also return the remainder of the flat trace.
232
233	*)
234
235	(* [will_return ge depth s trace] says that after a finite number of steps of
236	[trace] from [s] we reach the return state for the current function. [depth]
237	performs the call/return counting necessary for handling deeper function
238	calls. It should be zero at the top level. *)
239	inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
240	\| wr_step : ∀s,tr,s',depth,EX,trace.
241	RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
242	will_return ge depth s' trace →
243	will_return ge depth s (ft_step ?? ge s tr s' EX trace)
244	\| wr_call : ∀s,tr,s',depth,EX,trace.
245	RTLabs_classify s = cl_call →
246	will_return ge (S depth) s' trace →
247	will_return ge depth s (ft_step ?? ge s tr s' EX trace)
248	\| wr_ret : ∀s,tr,s',depth,EX,trace.
249	RTLabs_classify s = cl_return →
250	will_return ge depth s' trace →
251	will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
252	(* Note that we require the ability to make a step after the return (this
253	corresponds to somewhere that will be guaranteed to be a label at the
254	end of the compilation chain). *)
255	\| wr_base : ∀s,tr,s',EX,trace.
256	RTLabs_classify s = cl_return →
257	will_return ge O s (ft_step ?? ge s tr s' EX trace)
258	.
259
260	(* The way we will use [will_return] won't satisfy Matita's guardedness check,
261	so we will measure the length of these termination proofs and use an upper
262	bound to show termination of the finite structured trace construction
263	functions. *)
264
265	let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
266	match T with
267	[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
268	\| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
269	\| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
270	\| wr_base _ _ _ _ _ _ ⇒ S O
271	].
272
273	include alias "arithmetics/nat.ma".
274
275	(* Specialised to the particular situation it is used in. *)
276	lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
277	#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
278	whd in ⊢ (??(??%) → ?);
279	>commutative_times
280	#H lapply (le_plus_b … H)
281	#H lapply (le_to_leb_true … H)
282	normalize #E destruct
283	qed.
284
285	let 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' ≝
286	match T with
287	[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
288	\| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
289	\| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
290	\| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
291	].
292
293	(* Inversion lemmas on [will_return] that also note the effect on the length
294	of the proof. *)
295	lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
296	RTLabs_classify s = cl_call →
297	∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
298	ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
299	#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
300	[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
301	\| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
302	\| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
303	\| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
304	] qed.
305
306	lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
307	RTLabs_classify s = cl_return →
308	∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
309	match d with
310	[ O ⇒ will_return_end … TM = ❬s', trace❭
311	\| S d' ⇒
312	ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
313	].
314	#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
315	[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
316	\| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥ destruct >CL in H39; #E destruct
317	\| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
318	\| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
319	] qed.
320
321	lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
322	(RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
323	∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
324	ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
325	#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
326	[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
327	\| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
328	\| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
329	\| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
330	\| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
331	\| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
332	\| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
333	\| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
334	] qed.
335
336	(* When it comes to building bits of nonterminating executions we'll need to be
337	able to glue termination proofs together. *)
338
339	lemma will_return_prepend : ∀ge,d1,s1,t1.
340	∀T1:will_return ge d1 s1 t1.
341	∀d2,s2,t2.
342	will_return ge d2 s2 t2 →
343	will_return_end … T1 = ❬s2, t2❭ →
344	will_return ge (d1 + S d2) s1 t1.
345	#ge #d1 #s1 #tr1 #T1 elim T1
346	[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
347	%1 // @(IH … T2) @E
348	\| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
349	\| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
350	\| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
351	] qed.
352
353	discriminator nat.
354
355	lemma will_return_remove_call : ∀ge,d1,s1,t1.
356	∀T1:will_return ge d1 s1 t1.
357	∀d2.
358	will_return ge (d1 + S d2) s1 t1 →
359	∀s2,t2.
360	will_return_end … T1 = ❬s2, t2❭ →
361	will_return ge d2 s2 t2.
362	(* The key part of the proof is to show that the two termination proofs follow
363	the same pattern. *)
364	#ge #d1x #s1x #t1x #T1 elim T1
365	[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
366	[ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
367	\| #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
368	>H21 in CL; * #E destruct
369	\| #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
370	>H35 in CL; * #E destruct
371	\| #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
372	>H48 in CL; * #E destruct
373	]
374	\| @E
375	]
376	\| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
377	[ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
378	>CL in H7; * #E destruct
379	\| #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
380	\| #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
381	>H35 in CL; #E destruct
382	\| #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
383	>H48 in CL; #E destruct
384	]
385	\| @E
386	]
387	\| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
388	[ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
389	>CL in H7; * #E destruct
390	\| #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
391	>H21 in CL; #E destruct
392	\| #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
393	whd in H38:(??%??); destruct //
394	\| #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
395	whd in H49:(??%??); @⊥ destruct
396	]
397	\| @E
398	]
399	\| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
400	inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
401	>CL in H7; * #E destruct
402	\| #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
403	>H21 in CL; #E destruct
404	\| #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
405	whd in H38:(??%??); destruct //
406	\| #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
407	whd in H49:(??%??); @⊥ destruct
408	]
409	] qed.
410
411
412
413	lemma will_return_lower : ∀ge,d,s,t.
414	will_return ge d s t →
415	∀d'. d' ≤ d →
416	will_return ge d' s t.
417	#ge #d0 #s0 #t0 #TM elim TM
418	[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
419	\| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
420	\| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
421	[ #LE @wr_base //
422	\| #d' #LE %3 // @IH /2/
423	]
424	\| #s #tr #s' #EX #tr #CL *
425	[ #_ @wr_base //
426	\| #d' #LE @⊥ /2/
427	]
428	] qed.
429
430	(* We need to ensure that any code we come across is well-cost-labelled. We may
431	get function code from either the global environment or the state. *)
432
433	definition well_cost_labelled_ge : genv → Prop ≝
434	λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
435
436	definition well_cost_labelled_state : state → Prop ≝
437	λs. match s with
438	[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
439	\| Callstate _ fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn \| External _ ⇒ True ] ∧
440	All ? (λf. well_cost_labelled_fn (func f)) fs
441	\| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
442	\| Finalstate _ ⇒ True
443	].
444
445	lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
446	eval_statement ge s = Value ??? 〈tr,s'〉 →
447	well_cost_labelled_ge ge →
448	well_cost_labelled_state s →
449	well_cost_labelled_state s'.
450	#ge #s #tr' #s' #EV cases (eval_preserves … EV)
451	[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
452	\| #ge #f #fs #m #vf * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
453	(*
454	\| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
455	*)
456	\| #ge #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
457	\| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
458	\| #ge #f #fs #rtv #dst #f' #m #N * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
459	\| //
460	] qed.
461
462	lemma rtlabs_jump_inv : ∀s.
463	RTLabs_classify s = cl_jump →
464	∃f,fs,m. s = State f fs m ∧
465	(∃r,l1,l2. next_instruction f = St_cond r l1 l2) (∨ (∃r,ls. stmt = St_jumptable r ls)).
466	*
467	[ #f #fs #m #E
468	%{f} %{fs} %{m} %
469	[ @refl
470	\| whd in E:(??%?); cases (next_instruction f) in E ⊢ %;
471	try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
472	([ %1) %{A} %{B} %{C} @refl
473	(* \| %2 %{A} %{B} @refl
474	]*)
475	]
476	\| normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct
477	\| normalize #H8 #H9 #H10 #H11 #H12 destruct
478	\| #r #E normalize in E; destruct
479	] qed.
480
481	lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
482	eval_statement ge s = Value ??? 〈tr,s'〉 →
483	well_cost_labelled_state s →
484	RTLabs_classify s = cl_jump →
485	RTLabs_cost s' = true.
486	#ge #s #tr #s' #EV #H #CL
487	cases (rtlabs_jump_inv s CL)
488	#fr * #fs * #m * #Es(* *
489	[) #r * #l1 * #l2 #Estmt
490	>Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
491	>Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
492	>Estmt #LP whd in ⊢ (??%? → ?);
493	(* replace with lemma on successors? *)
494	@bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
495	lapply (Hbody (next fr) (next_ok fr))
496	generalize in ⊢ (?(???%) → ?);
497	change with (next_instruction fr) in match (lookup_present ?????);
498	>Estmt #LP' #WS
499	cases (andb_Prop_true … WS) #H1 #H2 [ @H1 \| @H2 ]
500	(\| #r * #ls #Estmt
501	>Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
502	>Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
503	>Estmt #LP whd in ⊢ (??%? → ?);
504	(* replace with lemma on successors? *)
505	@bind_res_value #a cases a [ \| #sz #i \| #f \| \| #ptr ] #Ea whd in ⊢ (??%? → ?);
506	[ 2: (* later *)
507	\| *: #E destruct
508	]
509	lapply (Hbody (next fr) (next_ok fr))
510	generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
511	generalize in ⊢ (??(?%)? → ?);
512	cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?\|_⇒?]?)? → ?);
513	[ #E1 #E2 whd in E2:(??%?); destruct
514	\| #l' #E1 #E2 whd in E2:(??%?); destruct
515	cases (All_nth ???? CP ? E1)
516	#H1 #H2 @H2
517	]
518	]*) qed.
519
520	lemma rtlabs_call_inv : ∀s.
521	RTLabs_classify s = cl_call →
522	∃vf,fd,args,dst,stk,m. s = Callstate vf fd args dst stk m.
523	* [ #f #fs #m whd in ⊢ (??%? → ?);
524	cases (next_instruction f) normalize
525	try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
526	\| #vf #fd #args #dst #stk #m #E %{vf} %{fd} %{args} %{dst} %{stk} %{m} @refl
527	\| normalize #H411 #H412 #H413 #H414 #H415 destruct
528	\| normalize #H1 #H2 destruct
529	] qed.
530
531	lemma well_cost_labelled_call : ∀ge,s,tr,s'.
532	eval_statement ge s = Value ??? 〈tr,s'〉 →
533	well_cost_labelled_state s →
534	RTLabs_classify s = cl_call →
535	RTLabs_cost s' = true.
536	#ge #s #tr #s' #EV #WCL #CL
537	cases (rtlabs_call_inv s CL)
538	#vf * #fd * #args * #dst * #stk * #m #E >E in EV WCL;
539	whd in ⊢ (??%? → % → ?);
540	cases fd
541	[ #fn whd in ⊢ (??%? → % → ?);
542	@bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) (XData))
543	#m' #b whd in ⊢ (??%? → ?); #E' destruct
544	* whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
545	@WCL2
546	\| #fn whd in ⊢ (??%? → % → ?);
547	@bindIO_value #evargs #Eargs
548	whd in ⊢ (??%? → ?);
549	#E' destruct
550	] qed.
551
552
553	(* Extend our information about steps to states extended with the shadow stack. *)
554
555	inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
556	\| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (State f' fs m') S M')
557	\| xto_call : ∀ge,f,fs,m,vf,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f'::fs) m) (fn::S) M')
558	\| xfrom_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate vf (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
559	\| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m') S M')
560	\| xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_ext_state ge (State f' fs m) S M')
561	\| xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M')
562	.
563
564	lemma eval_preserves_ext : ∀ge,s,s'.
565	as_execute (RTLabs_status ge) s s' →
566	state_rel_ext ge s s'.
567	#ge0 * #s #S #M * #s' #S' #M' * #tr * #EX
568	generalize in match M'; -M'
569	generalize in match M; -M
570	generalize in match EX;
571	inversion (eval_preserves … EX)
572	[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct
573	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
574	%1 //
575	\| #ge #f #fs #m #vf #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
576	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
577	%2 //
578	\| #ge #vf #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
579	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
580	%3
581	\| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
582	cases S [ #EX' * ] #fn #S
583	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
584	%4
585	\| #ge #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
586	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
587	%5 //
588	\| #ge #r #dst #m #E1 #E2 #E3 #E4 destruct
589	cases S [ 2: #h #t #EX' * ]
590	#EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
591	%6
592	] qed.
593
594
595
596	(* The preservation of (most of) the stack is useful to show as_after_return.
597	We do this by showing that during the execution of a function the lower stack
598	frames never change, and that after returning from the function we preserve
599	the identity of the next instruction to execute.
600
601	We also show preservation of the shadow stack of function pointers. As with
602	the real stack, we ignore the current function.
603	*)
604
605	inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
606	\| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M)
607	\| sos_Callstate : ∀vf,fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f::fs) m) (fn::fn'::S) M)
608	\| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m) S M)
609	.
610
611	inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
612	\| sp_normal : ∀fs,S,s1,s2.
613	stack_of_state ge fs S s1 →
614	stack_of_state ge fs S s2 →
615	stack_preserved ge doesnt_end_with_ret s1 s2
616	\| sp_finished : ∀s1,f,f',fs,m,fn,S,M.
617	next f = next f' →
618	frame_rel f f' →
619	stack_of_state ge (f::fs) (fn::S) s1 →
620	stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M)
621	\| sp_stop : ∀s1,r,M.
622	stack_of_state ge [ ] [ ] s1 →
623	stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
624	\| sp_top : ∀vf,fd,args,dst,m,r,fn,M1,M2.
625	stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate vf fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
626	.
627
628	discriminator list.
629
630	lemma stack_of_state_eq : ∀ge,fs,fs',S,S',s.
631	stack_of_state ge fs S s →
632	stack_of_state ge fs' S' s →
633	fs = fs' ∧ S = S'.
634	#ge #fs0 #fs0' #S0 #S0' #s0 *
635	[ #f #fs #m #fn #S #M #H inversion H
636	#a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
637	\| #vf #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
638	#a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o try #p destruct /2/
639	\| #rtv #dst #fs #m #S #M #H inversion H
640	#a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
641	] qed.
642
643	lemma stack_preserved_final : ∀ge,e,r,S,M,s.
644	¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s.
645	#ge #e #r #S #M #s % #H inversion H
646	[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
647	inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m try #o destruct
648	\| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
649	inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m try #p destruct
650	\| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
651	inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o try #p destruct
652	\| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
653	] qed.
654
655	lemma stack_preserved_join : ∀ge,e,s1,s2,s3.
656	stack_preserved ge doesnt_end_with_ret s1 s2 →
657	stack_preserved ge e s2 s3 →
658	stack_preserved ge e s1 s3.
659	#ge #e1 #s1 #s2 #s3 #H1 inversion H1
660	[ #fs #S #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
661	#H2 inversion H2
662	[ #fs' #S' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
663	@(sp_normal ge fs S) // cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
664	\| #s1'' #f #f' #fs' #m #fn #S' #M #N #F #S1' #E1 #E2 #E3 #E4 destruct
665	@(sp_finished … fn … N) cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
666	\| #s1'' #r #M #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop cases (stack_of_state_eq … S1'' S2) #E1 #E2 destruct //
667	\| #vf #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
668	inversion S2
669	[ #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
670	\| #vf' #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
671	\| #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
672	]
673	]
674	\| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
675	\| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
676	\| #vf #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
677	@(absurd … F) //
678	] qed.
679
680	(* Proof that steps preserve the stack. For calls we show that a stack
681	preservation proof for the called function gives us enough to show
682	stack preservation for the caller between the call and the state after
683	returning. *)
684
685	lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl.
686	RTLabs_classify s1 = cl →
687	as_execute (RTLabs_status ge) s1 s2 →
688	match cl with
689	[ cl_call ⇒ ∀s3. stack_preserved ge ends_with_ret s2 s3 →
690	stack_preserved ge doesnt_end_with_ret s1 s3
691	\| cl_return ⇒ stack_preserved ge ends_with_ret s1 s2
692	\| _ ⇒ stack_preserved ge doesnt_end_with_ret s1 s2
693	].
694	#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
695	[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
696	whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
697	\| #ge #f #fs #m #vf #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
698	whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
699	\| #ge #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
700	* #s3 #S3 #M3 #SP inversion SP
701	[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
702	\| #s1 #f #f' #fs' #m3 #fn3 #S3' #M3' #E1 #E2 #SOS #E4 #E5 #E6 #E7 destruct
703	@(sp_normal … fs' S3') //
704	inversion SOS
705	[ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct //
706	\| #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
707	\| #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
708	]
709	\| #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
710	cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 try #H108 destruct /3/ ]
711	* #fn * #E1 #E2 destruct
712	@sp_top
713	\| #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
714	]
715	\| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
716	whd in match (RTLabs_classify ?); cases (next_instruction f) /2/
717	\| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
718	cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
719	\| #ge #r #dst #m #M #M' #E1 #E2 #E3 #E4 destruct whd /2/
720	] qed.
721
722	lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr.
723	∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
724	as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
725	#ge #s1 #s2 #tr #EV %{tr} %{EV} %
726	qed.
727
728	definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E.
729
730	lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
731	∀CL : RTLabs_classify s1 = cl_call.
732	as_execute (RTLabs_status ge) s1 s2 →
733	stack_preserved ge ends_with_ret s2 s3 →
734	as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
735	#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
736	cases (rtlabs_call_inv … CL) #vf * #fn * #args * #dst * #stk * #m #E destruct
737	whd
738	inversion S23
739	[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
740	\| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
741	inversion (eval_preserves_ext … EV)
742	[ 3: #gex #vfx #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
743	inversion S
744	[ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N \| inversion F // ] \| whd % ]
745	\| #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 destruct
746	\| #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
747	]
748	\| *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
749	]
750	\| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
751	inversion (eval_preserves_ext … EV)
752	[ 3: #ge' #vf' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
753	inversion S1
754	[ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
755	\| *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 try #H123 destruct
756	]
757	\| *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
758	]
759	\| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
760	] qed.
761
762	(* Don't need to know that labels break loops because we have termination. *)
763
764	(* A bit of mucking around with the depth to avoid proving termination after
765	termination. Note that we keep a proof that our upper bound on the length
766	of the termination proof is respected. *)
767	record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
768	(start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
769	(original_terminates: will_return ge depth start full)
770	(T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
771	{
772	new_state : RTLabs_ext_state ge;
773	remainder : flat_trace io_out io_in ge new_state;
774	cost_labelled : well_cost_labelled_state new_state;
775	new_trace : T new_state;
776	stack_ok : stack_preserved ge ends start new_state;
777	terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth \| _ ⇒ depth ]) with
778	[ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
779	\| S d ⇒ ΣTM:will_return ge d new_state remainder.
780	gt limit (will_return_length … TM) ∧
781	will_return_end … original_terminates = will_return_end … TM
782	]
783	}.
784
785	(* The same with a flag indicating whether the function returned, as opposed to
786	encountering a label. *)
787	record sub_trace_result (ge:genv) (depth:nat)
788	(start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
789	(original_terminates: will_return ge depth start full)
790	(T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
791	{
792	ends : trace_ends_with_ret;
793	trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
794	}.
795
796	(* We often return the result from a recursive call with an addition to the
797	structured trace, so we define a couple of functions to help. The bound on
798	the size of the termination proof might need to be relaxed, too. *)
799
800	definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
801	∀r:trace_result ge d e s1 t1 TM1 T1 l1.
802	will_return_end … TM1 = will_return_end … TM2 →
803	T2 (new_state … r) →
804	stack_preserved ge e s2 (new_state … r) →
805	trace_result ge d e s2 t2 TM2 T2 l2 ≝
806	λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
807	mk_trace_result ge d e s2 t2 TM2 T2 l2
808	(new_state … r)
809	(remainder … r)
810	(cost_labelled … r)
811	trace
812	SP
813	?
814	(*(match d return λd'.match d' with [ O ⇒ True \| S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
815	match d' with [ O ⇒ True \| S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
816	[O ⇒ λ_. I \| _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
817	.
818	cases e in r ⊢ %;
819	[ <TME -TME * cases d in TM1 TM2 ⊢ %;
820	[ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
821	\| #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
822	%{TMa} % // @(transitive_le … lGE) @L1
823	]
824	\| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
825	* #TMa * #L1 #TME
826	%{TMa} % // @(transitive_le … lGE) @L1
827	] qed.
828
829	definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
830	∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
831	will_return_end … TM1 = will_return_end … TM2 →
832	T2 (ends … r) (new_state … r) →
833	stack_preserved ge (ends … r) s2 (new_state … r) →
834	sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
835	λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
836	mk_sub_trace_result ge d s2 t2 TM2 T2 l2
837	(ends … r)
838	(replace_trace … lGE … r TME trace SP).
839
840	(* Small syntax hack to avoid ambiguous input problems. *)
841	definition myge : nat → nat → Prop ≝ ge.
842
843	(* RTLabs_classify isn't exactly as_classifier *)
844	definition lift_cl ≝ eq_f ?? (Some status_class).
845
846	let rec make_label_return ge depth (s:RTLabs_ext_state ge)
847	(trace: flat_trace io_out io_in ge s)
848	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
849	(STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *)
850	(STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *)
851	(TERMINATES: will_return ge depth s trace)
852	(TIME: nat)
853	(TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
854	on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
855	(trace_label_return (RTLabs_status ge) s)
856	(will_return_length … TERMINATES) ≝
857
858	match TIME return λTIME. TIME ≥ ? → ? with
859	[ O ⇒ λTERMINATES_IN_TIME. ⊥
860	\| S TIME ⇒ λTERMINATES_IN_TIME.
861
862	let r ≝ make_label_label ge depth s
863	trace
864	ENV_COSTLABELLED
865	STATE_COSTLABELLED
866	STATEMENT_COSTLABEL
867	TERMINATES
868	TIME ? in
869	match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
870	trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
871	[ ends_with_ret ⇒ λr.
872	replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
873	\| doesnt_end_with_ret ⇒ λr.
874	let r' ≝ make_label_return ge depth (new_state … r)
875	(remainder … r)
876	ENV_COSTLABELLED
877	(cost_labelled … r) ?
878	(pi1 … (terminates … r)) TIME ? in
879	replace_trace … r' ?
880	(tlr_step (RTLabs_status ge) s (new_state … r)
881	(new_state … r') (new_trace … r) (new_trace … r')) ?
882	] (trace_res … r)
883
884	] TERMINATES_IN_TIME
885
886
887	and make_label_label ge depth (s:RTLabs_ext_state ge)
888	(trace: flat_trace io_out io_in ge s)
889	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
890	(STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *)
891	(STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *)
892	(TERMINATES: will_return ge depth s trace)
893	(TIME: nat)
894	(TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
895	on TIME : sub_trace_result ge depth s trace TERMINATES
896	(λends. trace_label_label (RTLabs_status ge) ends s)
897	(will_return_length … TERMINATES) ≝
898
899	match TIME return λTIME. TIME ≥ ? → ? with
900	[ O ⇒ λTERMINATES_IN_TIME. ⊥
901	\| S TIME ⇒ λTERMINATES_IN_TIME.
902
903	let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
904	replace_sub_trace … r ?
905	(tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
906
907	] TERMINATES_IN_TIME
908
909
910	and make_any_label ge depth (s0:RTLabs_ext_state ge)
911	(trace: flat_trace io_out io_in ge s0)
912	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
913	(STATE_COSTLABELLED: well_cost_labelled_state s0) (* functions in the state *)
914	(TERMINATES: will_return ge depth s0 trace)
915	(TIME: nat)
916	(TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
917	on TIME : sub_trace_result ge depth s0 trace TERMINATES
918	(λends. trace_any_label (RTLabs_status ge) ends s0)
919	(will_return_length … TERMINATES) ≝
920
921	match TIME return λTIME. TIME ≥ ? → ? with
922	[ O ⇒ λTERMINATES_IN_TIME. ⊥
923	\| S TIME ⇒ λTERMINATES_IN_TIME.
924	match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
925	well_cost_labelled_state s →
926	∀TM:will_return ??? trace.
927	myge ? (times 3 (will_return_length ??? trace TM)) →
928	sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
929	with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
930	match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
931	well_cost_labelled_state s →
932	∀TM:will_return ??? trace.
933	myge ? (times 3 (will_return_length ??? trace TM)) →
934	sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
935	[ ft_stop st FINAL ⇒
936	λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
937
938	\| ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
939	let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
940	let next' ≝ next_state ? start' ?? EV in
941	match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
942	[ cl_other ⇒ λCL.
943	match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
944	(* We're about to run into a label. *)
945	[ true ⇒ λCS.
946	mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
947	doesnt_end_with_ret
948	(mk_trace_result ge … next' trace' ?
949	(tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
950	(* An ordinary step, keep going. *)
951	\| false ⇒ λCS.
952	let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
953	replace_sub_trace ????????????? r ?
954	(tal_step_default (RTLabs_status ge) (ends … r)
955	start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
956	] (refl ??)
957
958	\| cl_jump ⇒ λCL.
959	mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
960	doesnt_end_with_ret
961	(mk_trace_result ge … next' trace' ?
962	(tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
963
964	\| cl_call ⇒ λCL.
965	let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
966	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
967	(* We're about to run into a label, use base case for call *)
968	[ true ⇒ λCS.
969	mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
970	doesnt_end_with_ret
971	(mk_trace_result ge …
972	(tal_base_call (RTLabs_status ge) start' next' (new_state … r)
973	? (lift_cl … CL) ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
974	(* otherwise use step case *)
975	\| false ⇒ λCS.
976	let r' ≝ make_any_label ge depth
977	(new_state … r) (remainder … r) ENV_COSTLABELLED ?
978	(pi1 … (terminates … r)) TIME ? in
979	replace_sub_trace … r' ?
980	(tal_step_call (RTLabs_status ge) (ends … r')
981	start' next' (new_state … r) (new_state … r') ? (lift_cl … CL) ?
982	(new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
983	] (refl ??)
984
985	\| cl_return ⇒ λCL.
986	mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
987	ends_with_ret
988	(mk_trace_result ge ???????
989	next'
990	trace'
991	?
992	(tal_base_return (RTLabs_status ge) start' next' ? (lift_cl … CL))
993	?
994	?)
995	\| cl_tailcall ⇒ λCL. ⊥
996	] (refl ? (RTLabs_classify start))
997
998	] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
999	] TERMINATES_IN_TIME.
1000
1001	[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1002	\| //
1003	\| //
1004	\| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1005	\| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1006	\| @(stack_preserved_join … (stack_ok … r)) //
1007	\| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
1008	\| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1009	@(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1010	@(transitive_le … (3*(will_return_length … TERMINATES)))
1011	[ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1012	@(monotonic_le_times_r 3 … LT)
1013	\| @le_S @le_S @le_n
1014	]
1015	\| @le_S_S_to_le @TERMINATES_IN_TIME
1016	\| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1017	\| @le_n
1018	\| //
1019	\| @(proj1 … (RTLabs_costed …)) //
1020	\| @le_S_S_to_le @TERMINATES_IN_TIME
1021	\| @(wrl_nonzero … TERMINATES_IN_TIME)
1022	\| (* We can't reach the final state because the function terminates with a
1023	return *)
1024	inversion TERMINATES
1025	[ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1026	\| #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1027	\| #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1028	\| #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1029	]
1030	\| @(will_return_return … CL TERMINATES)
1031	\| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1032	\| %{tr} %{EV} @refl
1033	\| @(well_cost_labelled_state_step … EV) //
1034	\| whd @(will_return_notfn … TERMINATES) %2 @CL
1035	\| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1036	\| %{tr} %{EV} %
1037	\| %1 whd @(lift_cl … CL)
1038	\| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
1039	\| @(well_cost_labelled_state_step … EV) //
1040	\| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1041	[ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1042	#TMx * #LT' #_ @LT'
1043	\| <EQr cases (will_return_call … CL TERMINATES)
1044	#TM' * #_ #EQ' @EQ'
1045	]
1046	\| @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
1047	\| %{tr} %{EV} %
1048	\| @(RTLabs_after_call … next') [ @eval_to_as_exec \| // ]
1049	\| @(cost_labelled … r)
1050	\| skip
1051	\| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1052	@(transitive_lt … LT)
1053	cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1054	\| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1055	cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
1056	\| @(RTLabs_after_call … next') [ @eval_to_as_exec \| // ]
1057	\| %{tr} %{EV} %
1058	\| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
1059	\| @(cost_labelled … r)
1060	\| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1061	@(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1062	cases (will_return_call … TERMINATES) in GT;
1063	#X * #Y #_ #Z
1064	@(transitive_le … (monotonic_lt_times_r 3 … Y))
1065	[ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1066	\| //
1067	]
1068	\| @(well_cost_labelled_state_step … EV) //
1069	\| @(well_cost_labelled_call … EV) //
1070	\| skip
1071	\| cases (will_return_call … TERMINATES)
1072	#TM * #GT #_ @le_S_S_to_le
1073	>commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1074	@(transitive_le … TERMINATES_IN_TIME)
1075	@(monotonic_le_times_r 3 … GT)
1076	\| @(RTLabs_notail … CL)
1077	\| whd @(will_return_notfn … TERMINATES) %1 @CL
1078	\| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1079	\| %{tr} %{EV} %
1080	\| %2 whd @(lift_cl … CL)
1081	\| @(well_cost_labelled_state_step … EV) //
1082	\| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1083	\| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
1084	\| @(lift_cl … CL)
1085	\| %{tr} %{EV} %
1086	\| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1087	\| @(well_cost_labelled_state_step … EV) //
1088	\| %1 @CL
1089	\| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1090	@le_S_S_to_le
1091	@(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1092	//
1093	] qed.
1094
1095	(* We can initialise TIME with a suitably large value based on the length of the
1096	termination proof. *)
1097	let rec make_label_return' ge depth (s:RTLabs_ext_state ge)
1098	(trace: flat_trace io_out io_in ge s)
1099	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
1100	(STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *)
1101	(STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *)
1102	(TERMINATES: will_return ge depth s trace)
1103	: trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1104	make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1105	(2 + 3 * will_return_length … TERMINATES) ?.
1106	@le_n
1107	qed.
1108
1109	(* Tail-calls would not be handled properly (which means that if we try to show the
1110	full version with non-termination we'll fail because calls and returns aren't
1111	balanced.
1112	*)
1113
1114	inductive inhabited (T:Type[0]) : Prop ≝
1115	\| witness : T → inhabited T.
1116
1117
1118	(* Define a notion of sound labellings of RTLabs programs. *)
1119
1120	definition actual_successor : state → option label ≝
1121	λs. match s with
1122	[ State f fs m ⇒ Some ? (next f)
1123	\| Callstate _ _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) \| _ ⇒ None ? ]
1124	\| Returnstate _ _ _ _ ⇒ None ?
1125	\| Finalstate _ ⇒ None ?
1126	].
1127
1128	lemma nth_opt_Exists : ∀A,n,l,a.
1129	nth_opt A n l = Some A a →
1130	Exists A (λa'. a' = a) l.
1131	#A #n elim n
1132	[ * [ #a #E normalize in E; destruct \| #a #l #a' #E normalize in E; destruct % // ]
1133	\| #m #IH *
1134	[ #a #E normalize in E; destruct
1135	\| #a #l #a' #E %2 @IH @E
1136	]
1137	] qed.
1138
1139	lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1140	eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1141	(RTLabs_classify s' = cl_return ∧ successors (next_instruction f) = [ ]) ∨
1142	∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (next_instruction f)).
1143	#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1144	whd in ⊢ (??%? → ?);
1145	generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
1146	[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1147	\| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1148	\| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1149	\| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1150	\| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1151	\| #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1152	\| #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1153	\| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1154	\| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1155	\| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} \| %{l2} ] % // [ % \| %2 %] //
1156	(*\| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1157	cases v [ #E normalize in E; destruct \| #sz #i \| #f #E normalize in E; destruct \| #E normalize in E; destruct \| #p #E normalize in E; destruct ]
1158	whd in ⊢ (??%? → ?);
1159	generalize in ⊢ (??(?%)? → ?);
1160	cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? \| _ ⇒ ? ] ?)? → ?);
1161	[ #e #E normalize in E; destruct
1162	\| #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1163	]*)
1164	\| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 % %
1165	] qed.
1166
1167	(* Establish a link between the number of instructions until the next cost
1168	label and the number of states. *)
1169
1170
1171	definition steps_for_statement : statement → nat ≝
1172	λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 \| St_call_ptr _ _ _ _ ⇒ 1 \| St_return ⇒ 1 \| _ ⇒ 0 ]).
1173
1174	inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
1175	\| bostc_here : ∀l,n,H.
1176	is_cost_label (lookup_present … g l H) →
1177	bound_on_steps_to_cost g l n
1178	\| bostc_later : ∀l,n,H.
1179	¬ is_cost_label (lookup_present … g l H) →
1180	bound_on_steps_to_cost1 g l n →
1181	bound_on_steps_to_cost g l n
1182	with bound_on_steps_to_cost1 : label → nat → Prop ≝
1183	\| bostc_step : ∀l,n,H.
1184	let stmt ≝ lookup_present … g l H in
1185	(∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1186	bound_on_steps_to_cost g l' n) →
1187	bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
1188
1189	let rec bound_on_steps_succ g l n (H:bound_on_steps_to_cost g l n) on H
1190	: bound_on_steps_to_cost g l (S n) ≝
1191	match H with
1192	[ bostc_here l n Pr Cs ⇒ ?
1193	\| bostc_later l n H' CS B ⇒ ?
1194	] and bound_on_steps1_succ g l n (H:bound_on_steps_to_cost1 g l n) on H
1195	: bound_on_steps_to_cost1 g l (S n) ≝
1196	match H with
1197	[ bostc_step l n Pr Sc ⇒ ?
1198	].
1199	[ %1 //
1200	\| %2 /2/
1201	\| >plus_n_Sm % /3/
1202	] qed.
1203
1204	let rec bound_on_steps_stmt g l n P (H:bound_on_steps_to_cost1 g l (plus (steps_for_statement (lookup_present … g l P)) n))
1205	: bound_on_steps_to_cost1 g l (S (S n)) ≝ ?.
1206	cases (lookup_present ? statement ???) in H; /2/
1207	qed.
1208
1209	let rec bound_on_instrs_to_steps g l n
1210	(B:bound_on_instrs_to_cost g l n)
1211	on B : bound_on_steps_to_cost1 g l (times n 2) ≝ ?
1212	and bound_on_instrs_to_steps' g l n
1213	(B:bound_on_instrs_to_cost' g l n)
1214	on B : bound_on_steps_to_cost g l (times n 2) ≝ ?.
1215	[ cases B #l' #n' #H #EX @bound_on_steps_stmt [ @H \| % #l'' #SC @bound_on_instrs_to_steps' @EX @SC ]
1216	\| cases B
1217	[ #l' #n' #H #CS %1 //
1218	\| #l' #n' #H #CS #B' %2 [ @H \| @CS \| @bound_on_instrs_to_steps @B' ]
1219	]
1220	] qed.
1221
1222
1223	definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1224	λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1225	definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1226	λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1227
1228	inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1229	\| 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
1230	\| sbostc_call : ∀vf,fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate vf fd args dst (f::fs) m) (S n)
1231	\| 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)
1232	.
1233
1234	lemma state_bound_on_steps_to_cost_zero : ∀s.
1235	¬ state_bound_on_steps_to_cost s O.
1236	#s % #H inversion H
1237	[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1238	whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1239	#H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1240	\| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1241	\| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1242	] qed.
1243
1244	lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1245	eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1246	steps_for_statement (next_instruction f) =
1247	match s' with [ State _ _ _ ⇒ 1 \| Callstate _ _ _ _ _ _ ⇒ 2 \| Returnstate _ _ _ _ ⇒ 2 \| Finalstate _ ⇒ 1 ].
1248	#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1249	whd in ⊢ (??%? → ?);
1250	generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?)
1251	[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1252	\| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1253	\| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1254	\| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1255	\| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1256	\| #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1257	\| #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1258	\| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1259	\| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1260	\| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1261	(*\| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1262	cases v [ #E normalize in E; destruct \| #sz #i \| #f #E normalize in E; destruct \| #E normalize in E; destruct \| #p #E normalize in E; destruct ]
1263	whd in ⊢ (??%? → ?);
1264	generalize in ⊢ (??(?%)? → ?);
1265	cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? \| _ ⇒ ? ] ?)? → ?);
1266	[ #e #E normalize in E; destruct
1267	\| #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1268	]*)
1269	\| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1270	] qed.
1271
1272	lemma bound_after_call : ∀ge.∀s,s':RTLabs_ext_state ge.∀n.
1273	state_bound_on_steps_to_cost s (S n) →
1274	∀CL:RTLabs_classify s = cl_call.
1275	as_after_return (RTLabs_status ge) «s, lift_cl … CL» s' →
1276	RTLabs_cost s' = false →
1277	state_bound_on_steps_to_cost s' n.
1278	#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL -CL inversion H
1279	[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1280	#vf * #fn * #args * #dst * #stk * #m' @jmeq_hackT #E destruct
1281	\| #vf #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1282	whd in S; #CL cases s'
1283	[ #f' #fs' #m' * * #N #F #STK #CS
1284	%1 whd
1285	inversion S
1286	[ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1287	change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1288	\| #l #n #H #CS' #B #E1 #E2 #_ destruct <N <F @B
1289	]
1290	\| #vf' #fd' #args' #dst' #fs' #m' *
1291	\| #rv #dst' #fs' #m' *
1292	\| #r #E normalize in E; destruct
1293	]
1294	\| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1295	] qed.
1296
1297	lemma bound_after_step : ∀ge,s,tr,s',n.
1298	state_bound_on_steps_to_cost s (S n) →
1299	eval_statement ge s = Value ??? 〈tr, s'〉 →
1300	RTLabs_cost s' = false →
1301	(RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1302	state_bound_on_steps_to_cost s' n.
1303	#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1304	[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1305	#EVAL cases (eval_successor … EVAL)
1306	[ * /3/
1307	\| * #l * #S1 #S2 #NC %2
1308	(*
1309	cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1310	*)
1311	@(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1312	inversion (eval_preserves … EVAL)
1313	[ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1314	>(eval_steps … EVAL) in E2; #En normalize in En;
1315	inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1316	%1 inversion (IH … S2)
1317	[ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1318	change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1319	whd in S1:(??%?); destruct >NC in CSx; *
1320	\| whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 destruct @H75
1321	]
1322	\| #ge0 #f0 #fs' #m0 #vf #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1323	>(eval_steps … EVAL) in E2; #En normalize in En;
1324	inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1325	%2 @IH normalize in S1; destruct @S2
1326	\| #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1327	destruct
1328	\| #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1329	normalize in S1; destruct
1330	\| #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1331	\| #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1332	]
1333	]
1334	\| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1335	/3/
1336	\| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1337	#EVAL #NC %2 inversion (eval_preserves … EVAL)
1338	[ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1339	\| #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1340	\| #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1341	\| #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1342	\| #ge' #f' #fs' #rtv' #dst' #f'' #m' #N #F #E1 #E2 #E3 #_ destruct
1343	%1 whd in FS ⊢ %;
1344	<N
1345	inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1346	inversion FS
1347	[ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1348	change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs' m')) in CSx:(?%);
1349	>NC in CSx; *
1350	\| #lx #nx #P #CS #H #E1x #E2x #_ destruct @H
1351	]
1352	\| #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1353	]
1354	] qed.
1355
1356
1357
1358
1359	definition soundly_labelled_ge : genv → Prop ≝
1360	λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1361
1362	definition soundly_labelled_state : state → Prop ≝
1363	λs. match s with
1364	[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1365	\| Callstate _ fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn \| External _ ⇒ True ] ∧
1366	All ? (λf. soundly_labelled_fn (func f)) fs
1367	\| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1368	\| Finalstate _ ⇒ True
1369	].
1370
1371	lemma steps_from_sound : ∀s.
1372	RTLabs_cost s = true →
1373	soundly_labelled_state s →
1374	∃n. state_bound_on_steps_to_cost s n.
1375	* [ #f #fs #m #CS \| #a #b #c #d #e #f #E normalize in E; destruct \| #a #b #c #d #E normalize in E; destruct \| #a #E normalize in E; destruct ]
1376	whd in ⊢ (% → ?); * #SLF #_
1377	cases (SLF (next f) (next_ok f)) #n #B1
1378	% [2: % /2/ \| skip ]
1379	qed.
1380
1381	lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1382	soundly_labelled_ge ge →
1383	eval_statement ge s = Value ??? 〈tr,s'〉 →
1384	soundly_labelled_state s →
1385	soundly_labelled_state s'.
1386	#ge #s #tr #s' #ENV #EV #S
1387	inversion (eval_preserves … EV)
1388	[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1389	whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1390	\| #ge' #f #fs #m #vf #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1391	whd in S ⊢ %; %
1392	[ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1393	\| inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1394	]
1395	\| #ge' #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1396	whd in S ⊢ %; @S
1397	\| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1398	whd in S ⊢ %; cases S //
1399	\| #ge' #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
1400	whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1401	\| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1402	] qed.
1403
1404	lemma soundly_labelled_state_preserved : ∀ge,s,s'.
1405	stack_preserved ge ends_with_ret s s' →
1406	soundly_labelled_state s →
1407	soundly_labelled_state s'.
1408	#ge #s0 #s0' #SP inversion SP
1409	[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1410	\| #s1 #f #f' #fs #m #fn #S #M #N #F #S1 #E1 #E2 #E3 #E4 destruct
1411	inversion S1
1412	[ #f1 #fs1 #m1 #fn1 #S1 #M1 #E1 #E2 #E3 #E4 destruct
1413	* #_ #S whd in S;
1414	inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1415	destruct @S
1416	\| #vf #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
1417	inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1418	destruct @S
1419	\| #rtv #dst #fs1 #m1 #S1 #M1 #E1 #E2 #E3 #E4 destruct #S
1420	inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1421	destruct @S
1422	]
1423	\| //
1424	\| //
1425	] qed.
1426
1427	(* When constructing an infinite trace, we need to be able to grab the finite
1428	portion of the trace for the next [trace_label_diverges] constructor. We
1429	use the fact that the trace is soundly labelled to achieve this. *)
1430
1431	record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1432	ro_well_cost_labelled: well_cost_labelled_state s;
1433	ro_soundly_labelled: soundly_labelled_state s;
1434	ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1435	ro_not_final: RTLabs_is_final s = None ?
1436	}.
1437
1438	inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝
1439	\| fp_tal : ∀s,s':RTLabs_ext_state ge.
1440	trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1441	∀t:flat_trace io_out io_in ge s'.
1442	remainder_ok ge s' t →
1443	finite_prefix ge s
1444	\| fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge.
1445	trace_any_call (RTLabs_status ge) s1 s2 →
1446	well_cost_labelled_state s2 →
1447	as_execute (RTLabs_status ge) s2 s3 →
1448	∀t:flat_trace io_out io_in ge s3.
1449	remainder_ok ge s3 t →
1450	finite_prefix ge s1
1451	.
1452
1453	definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge.
1454	RTLabs_classify s = cl_other →
1455	finite_prefix ge s' →
1456	as_execute (RTLabs_status ge) s s' →
1457	RTLabs_cost s' = false →
1458	finite_prefix ge s ≝
1459	λge,s,s',OTHER,fp.
1460	match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
1461	[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1462	(tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
1463	rem rok
1464	\| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
1465	(tac_step_default (RTLabs_status ge) ??? EVAL TAC (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST))
1466	WCL2 EV rem rok
1467	].
1468
1469	definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge.
1470	as_execute (RTLabs_status ge) s s1 →
1471	∀CALL:RTLabs_classify s = cl_call.
1472	finite_prefix ge s'' →
1473	trace_label_return (RTLabs_status ge) s1 s'' →
1474	as_after_return (RTLabs_status ge) «s, lift_cl … CALL» s'' →
1475	RTLabs_cost s'' = false →
1476	finite_prefix ge s ≝
1477	λge,s,s1,s'',EVAL,CALL,fp.
1478	match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
1479	[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1480	(tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1481	rem rok
1482	\| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
1483	(tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1484	WCL2 EV rem rok
1485	].
1486
1487	lemma not_return_to_not_final : ∀ge,s,tr,s'.
1488	eval_statement ge s = Value ??? 〈tr, s'〉 →
1489	RTLabs_classify s ≠ cl_return →
1490	RTLabs_is_final s' = None ?.
1491	#ge #s #tr #s' #EV
1492	inversion (eval_preserves … EV) //
1493	#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1494	@⊥ @(absurd ?? CL) @refl
1495	qed.
1496
1497	definition termination_oracle ≝ ∀ge,depth,s,trace.
1498	inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1499
1500	let rec finite_segment ge (s:RTLabs_ext_state ge) n trace
1501	(ORACLE: termination_oracle)
1502	(TRACE_OK: remainder_ok ge s trace)
1503	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
1504	(ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1505	(LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1506	on n : finite_prefix ge s ≝
1507	match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1508	[ O ⇒ λLABEL_LIMIT. ⊥
1509	\| S n' ⇒
1510	match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace'.
1511	match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_ext_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_ext_state ge s ? mtc) with
1512	[ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
1513	\| ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
1514	let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
1515	let next' ≝ next_state ge start' next tr EV in
1516	match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1517	[ cl_other ⇒ λCL.
1518	let TRACE_OK' ≝ ? in
1519	match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1520	[ true ⇒ λCS.
1521	fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
1522	\| false ⇒ λCS.
1523	let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1524	fp_add_default ge start' next' CL fs ? CS
1525	] (refl ??)
1526	\| cl_jump ⇒ λCL.
1527	fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
1528	\| cl_call ⇒ λCL.
1529	match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
1530	[ or_introl TERMINATES ⇒
1531	match TERMINATES with [ witness TERMINATES ⇒
1532	let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1533	let TRACE_OK' ≝ ? in
1534	match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
1535	[ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (lift_cl … CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
1536	\| false ⇒ λCS.
1537	let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1538	fp_add_terminating_call … fs (new_trace … tlr) ? CS
1539	] (refl ??)
1540	]
1541	\| or_intror NO_TERMINATION ⇒
1542	fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (lift_cl … CL))) ?? trace' ?
1543	]
1544	\| cl_return ⇒ λCL. ⊥
1545	\| cl_tailcall ⇒ λCL. ⊥
1546	] (refl ??)
1547	] mtc0
1548	] trace TRACE_OK
1549	] LABEL_LIMIT.
1550	[ cases (state_bound_on_steps_to_cost_zero s) /2/
1551	\| @(absurd … (ro_not_final … TRACE_OK) FINAL)
1552	\| @(absurd ?? (ro_no_termination … TRACE_OK))
1553	%{0} % @wr_base //
1554	\| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) \| // ]
1555	\| %1 @(lift_cl … CL)
1556	\| 6,9,10,11: /3/
1557	\| cases TRACE_OK #H1 #H2 #H3 #H4
1558	% [ @(well_cost_labelled_state_step … EV) //
1559	\| @(soundly_labelled_state_step … EV) //
1560	\| @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1561	\| @(not_return_to_not_final … EV) >CL % #E destruct
1562	]
1563	\| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1564	\| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1565	\| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
1566	@(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1567	\| % [ /2/
1568	\| @(soundly_labelled_state_preserved … (stack_ok … tlr))
1569	@(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
1570	\| @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1571	@wr_call //
1572	@(will_return_prepend … TERMINATES … TM1)
1573	cases (terminates … tlr) //
1574	\| (* By stack preservation we cannot be in the final state *)
1575	inversion (stack_ok … tlr)
1576	[ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1577	\| #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1578	\| #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s0
1579	cases (rtlabs_call_inv … CL) #vf * #fd * #args * #dst * #stk * #m #E destruct
1580	inversion (eval_preserves … EV)
1581	[ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 try #H124 @⊥ -next destruct ]
1582	#ge' #vf' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1583	inversion S
1584	[ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct \| *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 try #H6 [ whd in H6:(??%?%); \| whd in H2:(??%?%); ] destruct ]
1585	(* state_bound_on_steps_to_cost needs to know about the current stack frame,
1586	so we can use it as a witness that at least one frame exists *)
1587	inversion LABEL_LIMIT
1588	#H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 try #H151 destruct
1589	\| #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 destruct
1590	]
1591	]
1592	\| @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
1593	\| @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) \| // ]
1594	\| /2/
1595	\| %{tr} %{EV} %
1596	\| cases TRACE_OK #H1 #H2 #H3 #H4
1597	% [ @(well_cost_labelled_state_step … EV) /2/
1598	\| @(soundly_labelled_state_step … EV) /2/
1599	\| @(not_to_not … NO_TERMINATION) * #depth * #TM %
1600	@(will_return_lower … TM) //
1601	\| @(not_return_to_not_final … EV) >CL % #E destruct
1602	]
1603	\| @(RTLabs_notail … CL)
1604	\| %2 @(lift_cl … CL)
1605	\| 21,22: %{tr} %{EV} %
1606	\| cases (bound_after_step … LABEL_LIMIT EV ?)
1607	[ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // \|
1608	inversion trace'
1609	[ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1610	@(absurd ?? FINAL) @(not_return_to_not_final … EV)
1611	% >CL #E destruct
1612	\| #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1613	@wr_base //
1614	]
1615	]
1616	\| >CL #E destruct
1617	]
1618	\| //
1619	\| //
1620	]
1621	\| cases (bound_after_step … LABEL_LIMIT EV ?)
1622	[ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // \|
1623	inversion trace'
1624	[ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1625	@(absurd ?? FINAL) @(not_return_to_not_final … EV)
1626	% >CL #E destruct
1627	\| #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1628	@wr_base //
1629	]
1630	]
1631	\| >CL #E destruct
1632	]
1633	\| //
1634	\| //
1635	]
1636	\| cases TRACE_OK #H1 #H2 #H3 #H4
1637	% [ @(well_cost_labelled_state_step … EV) //
1638	\| @(soundly_labelled_state_step … EV) //
1639	\| @(not_to_not … (ro_no_termination … TRACE_OK))
1640	* #depth * #TERM %{depth} % @wr_step /2/
1641	\| @(not_return_to_not_final … EV) >CL % #E destruct
1642	]
1643	] qed.
1644
1645	lemma simplify_cl : ∀ge,s,c.
1646	as_classifier (RTLabs_status ge) s c →
1647	RTLabs_classify (Ras_state … s) = c.
1648	#ge * #s #S #M #c #CL
1649	whd in CL; whd in CL:(??%?);
1650	destruct //
1651	qed.
1652
1653	(* NB: This isn't quite what I'd like. Ideally, we'd show the existence of
1654	a trace_label_diverges value, but I only know how to construct those
1655	using a cofixpoint in Type[0], which means I can't use the termination
1656	oracle.
1657	*)
1658
1659	let corec make_label_diverges ge (s:RTLabs_ext_state ge)
1660	(trace: flat_trace io_out io_in ge s)
1661	(ORACLE: termination_oracle)
1662	(TRACE_OK: remainder_ok ge s trace)
1663	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
1664	(ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1665	(STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *)
1666	: trace_label_diverges_exists (RTLabs_status ge) s ≝
1667	match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
1668	[ ex_intro n B ⇒
1669	match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
1670	return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1671	with
1672	[ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1673	let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1674	tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
1675	(*
1676	match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1677	[ ex_intro T' _ ⇒
1678	ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1679	]*)
1680	\| fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1681	let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1682	tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
1683	(*
1684	match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1685	[ ex_intro T' _ ⇒
1686	ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1687	]*)
1688	] STATEMENT_COSTLABEL
1689	].
1690	[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
1691	\| @EV
1692	\| cases (trace_any_call_call … T) // #CL cases (RTLabs_notail' … CL)
1693	\| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') //
1694	cases (trace_any_call_call … T) #CL
1695	[ @simplify_cl @CL
1696	\| @⊥ @(RTLabs_notail' … CL)
1697	]
1698	] qed.
1699
1700	lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge.
1701	as_execute (RTLabs_status ge) s1 s2 →
1702	make_initial_state p = OK ? s1 →
1703	stack_preserved ge ends_with_ret s2 s' →
1704	RTLabs_is_final s' ≠ None ?.
1705	#ge #p * #s1 #S1 #M1 * #s2 #S2 #M2 * #s' #S' #M' #EV whd in ⊢ (??%? → ?);
1706	@bind_ok #m #_
1707	@bind_ok #b #_
1708	@bind_ok #f #_
1709	#E destruct
1710	#SP inversion (eval_preserves_ext … EV)
1711	[ 3: #ge' #vf #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
1712	inversion SP
1713	[ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
1714	\| *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥
1715	inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 try #H75 destruct
1716	]
1717	\| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 try #H113 destruct
1718	] qed.
1719
1720	lemma initial_state_is_call : ∀p,s.
1721	make_initial_state p = OK ? s →
1722	RTLabs_classify s = cl_call.
1723	#p #s whd in ⊢ (??%? → ?);
1724	@bind_ok #m #_
1725	@bind_ok #b #_
1726	@bind_ok #f #_
1727	#E destruct
1728	@refl
1729	qed.
1730
1731	let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge)
1732	(ORACLE: termination_oracle)
1733	(ENV_COSTLABELLED: well_cost_labelled_ge ge)
1734	(ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1735	: ∀trace: flat_trace io_out io_in ge s.
1736	∀INITIAL: make_initial_state p = OK state s.
1737	∀STATE_COSTLABELLED: well_cost_labelled_state s.
1738	∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
1739	trace_whole_program_exists (RTLabs_status ge) s ≝
1740	match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
1741	make_initial_state p = OK ? s →
1742	well_cost_labelled_state s →
1743	soundly_labelled_state s →
1744	trace_whole_program_exists (RTLabs_status ge) s with
1745	[ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace.
1746	match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1747	make_initial_state p = OK state s →
1748	well_cost_labelled_state s →
1749	soundly_labelled_state s →
1750	trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with
1751	[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
1752	let IS_CALL ≝ initial_state_is_call … INITIAL in
1753	let s' ≝ mk_RTLabs_ext_state ge s stk mtc in
1754	let next' ≝ next_state ge s' next tr EV in
1755	match ORACLE ge O next trace' with
1756	[ or_introl TERMINATES ⇒
1757	match TERMINATES with
1758	[ witness TERMINATES ⇒
1759	let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1760	twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (lift_cl … IS_CALL) ? (new_trace … tlr) ?
1761	]
1762	\| or_intror NO_TERMINATION ⇒
1763	twp_diverges (RTLabs_status ge) s' next' (lift_cl … IS_CALL) ?
1764	(make_label_diverges ge next' trace' ORACLE ?
1765	ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1766	]
1767	\| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
1768	] mtc0 ].
1769	[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #vf * #fn * #args * #dst * #stk * #m #E destruct
1770	cases FINAL #E @E @refl
1771	\| %{tr} %{EV} %
1772	\| @(after_the_initial_call_is_the_final_state … p s' next')
1773	[ %{tr} %{EV} % \| @INITIAL \| @(stack_ok … tlr) ]
1774	\| @(well_cost_labelled_state_step … EV) //
1775	\| @(well_cost_labelled_call … EV) //
1776	\| %{tr} %{EV} %
1777	\| @(well_cost_labelled_call … EV) //
1778	\| % [ @(well_cost_labelled_state_step … EV) //
1779	\| @(soundly_labelled_state_step … EV) //
1780	\| @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1781	\| @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1782	]
1783	] qed.
1784
1785	lemma init_state_is : ∀p,s.
1786	make_initial_state p = OK ? s →
1787	𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
1788	\| _ ⇒ False ].
1789	#p #s
1790	@bind_ok #m #Em
1791	@bind_ok #b #Eb
1792	@bind_ok #f #Ef
1793	#E whd in E:(??%%); destruct
1794	%{b} whd
1795	% // @Ef
1796	qed.
1797
1798	definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
1799	λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
1800	cases (init_state_is p s I) #b
1801	cases s
1802	[ #f #fs #m *
1803	\| #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
1804	\| #rv #rr #fs #m *
1805	\| #r *
1806	] qed.
1807
1808	lemma well_cost_labelled_initial : ∀p,s.
1809	make_initial_state p = OK ? s →
1810	well_cost_labelled_program p →
1811	well_cost_labelled_state s ∧ soundly_labelled_state s.
1812	#p #s
1813	@bind_ok #m #Em
1814	@bind_ok #b #Eb
1815	@bind_ok #f #Ef
1816	#E destruct
1817	whd in ⊢ (% → %);
1818	#WCL
1819	@(find_funct_ptr_All ??????? Ef)
1820	@(All_mp … WCL)
1821	* #id * /3/ #fn * #W #S % [ /2/ \| whd % // @S ]
1822	qed.
1823
1824	lemma well_cost_labelled_make_global : ∀p.
1825	well_cost_labelled_program p →
1826	well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
1827	#p whd in ⊢ (% → ?%%);
1828	#WCL %
1829	#b #f #FFP
1830	[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f \| _ ⇒ True]) FFP)
1831	\| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f \| _ ⇒ True]) FFP)
1832	] @(All_mp … WCL)
1833	* #id * #fn // * /2/
1834	qed.
1835
1836	theorem program_trace_exists :
1837	termination_oracle →
1838	∀p:RTLabs_program.
1839	well_cost_labelled_program p →
1840	∀s:state.
1841	∀I: make_initial_state p = OK ? s.
1842
1843	let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1844
1845	∀NOIO:exec_no_io … plain_trace.
1846	∀NW:not_wrong … plain_trace.
1847
1848	let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
1849
1850	trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
1851
1852	#ORACLE #p #WCL #s #I
1853	letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1854	#NOIO #NW
1855	letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
1856	whd
1857	@(whole_structured_trace_exists (make_global p) p ? ORACLE)
1858	[ @(proj1 … (well_cost_labelled_make_global … WCL))
1859	\| @(proj2 … (well_cost_labelled_make_global … WCL))
1860	\| @flat_trace
1861	\| @I
1862	\| @(proj1 ?? (well_cost_labelled_initial … I WCL))
1863	\| @(proj2 ?? (well_cost_labelled_initial … I WCL))
1864	] qed.
1865
1866
1867	lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
1868	as_execute (RTLabs_status ge) s s' →
1869	∃tr. eval_statement ge s = Value … 〈tr,s'〉.
1870	#ge #s #s' * #tr * #EX #_ %{tr} @EX
1871	qed.
1872
1873	(* as_execute might be in Prop, but because the semantics is deterministic
1874	we can retrieve the event trace anyway. *)
1875
1876	let rec deprop_execute ge (s,s':state)
1877	(X:∃t. eval_statement ge s = Value … 〈t,s'〉)
1878	: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1879	match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
1880	[ Value ts ⇒ λY. «fst … ts, ?»
1881	\| _ ⇒ λY. ⊥
1882	] X.
1883	[ 1,3: cases Y #x #E destruct
1884	\| cases Y #trP #E destruct @refl
1885	] qed.
1886
1887	let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
1888	(X:as_execute (RTLabs_status ge) s s')
1889	: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1890	deprop_execute ge s s' ?.
1891	cases X #tr * #EX #_ %{tr} @EX
1892	qed.
1893
1894	(* A non-empty finite section of a flat_trace *)
1895	inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1896	\| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1897	\| 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''.
1898
1899	let rec append_partial_flat_trace o i ge s1 s2 s3
1900	(tr1:partial_flat_trace o i ge s1 s2)
1901	on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1902	match tr1 with
1903	[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1904	\| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1905	].
1906
1907	let rec partial_to_flat_trace o i ge s1 s2
1908	(tr:partial_flat_trace o i ge s1 s2)
1909	on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1910	match tr with
1911	[ pft_base s tr s' EX ⇒ ft_step … EX
1912	\| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1913	].
1914
1915	(* Extract a flat trace from a structured one. *)
1916	let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
1917	(tr:trace_label_return (RTLabs_status ge) s s')
1918	on tr :
1919	partial_flat_trace io_out io_in ge s s' ≝
1920	match tr with
1921	[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
1922	\| tlr_step s1 s2 s3 tll tlr ⇒
1923	append_partial_flat_trace …
1924	(flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
1925	(flat_trace_of_label_return ge s2 s3 tlr)
1926	]
1927	and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
1928	(tr:trace_label_label (RTLabs_status ge) ends s s')
1929	on tr :
1930	partial_flat_trace io_out io_in ge s s' ≝
1931	match tr with
1932	[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
1933	]
1934	and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
1935	(tr:trace_any_label (RTLabs_status ge) ends s s')
1936	on tr :
1937	partial_flat_trace io_out io_in ge s s' ≝
1938	match tr with
1939	[ tal_base_not_return s1 s2 EX CL CS ⇒
1940	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1941	pft_base … EX' ]
1942	\| tal_base_return s1 s2 EX CL ⇒
1943	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1944	pft_base … EX' ]
1945	\| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
1946	let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
1947	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1948	pft_step … EX' suffix' ]
1949	\| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
1950	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1951	pft_step … EX'
1952	(append_partial_flat_trace …
1953	(flat_trace_of_label_return ge ?? tlr)
1954	(flat_trace_of_any_label ge ??? tal))
1955	]
1956	\| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
1957	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1958	pft_step … EX' (flat_trace_of_any_label ge ??? tal)
1959	]
1960	\| tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥
1961	].
1962	@(RTLabs_notail' … CL)
1963	qed.
1964
1965	(* We take an extra step so that we can always return a non-empty trace to
1966	satisfy the guardedness condition in the cofixpoint. *)
1967	let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
1968	(tr:trace_any_call (RTLabs_status ge) s s')
1969	(EX'':eval_statement ge s' = Value … 〈et,s''〉)
1970	on tr :
1971	partial_flat_trace io_out io_in ge s s'' ≝
1972	match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
1973	[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
1974	\| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
1975	match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
1976	pft_step … EX'
1977	(append_partial_flat_trace …
1978	(flat_trace_of_label_return ge ?? tlr)
1979	(flat_trace_of_any_call ge … tac EX''))
1980	]
1981	\| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
1982	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1983	pft_step … EX'
1984	(flat_trace_of_any_call ge … tal EX'')
1985	]
1986	] EX''.
1987
1988	let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
1989	(tr:trace_label_call (RTLabs_status ge) s s')
1990	(EX'':eval_statement ge s' = Value … 〈et,s''〉)
1991	on tr :
1992	partial_flat_trace io_out io_in ge s s'' ≝
1993	match tr with
1994	[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
1995	] EX''.
1996
1997	(* Now reconstruct the flat_trace of a diverging execution. Note that we need
1998	to take care to satisfy the guardedness condition by witnessing the fact that
1999	the partial traces are non-empty. *)
2000	let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)
2001	(tr:trace_label_diverges (RTLabs_status ge) s)
2002	: flat_trace io_out io_in ge s ≝
2003	match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
2004	[ tld_step sx sy tll tld ⇒
2005	match sy in RTLabs_ext_state return λsy:RTLabs_ext_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state sy' stk mtc0 ⇒
2006	λtll.
2007	match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s2 stk mtc) → flat_trace ??? s1 with
2008	[ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2009	\| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
2010	] mtc0 ] tll tld
2011	\| tld_base s1 s2 s3 tlc EX CL tld ⇒
2012	match s3 in RTLabs_ext_state return λs3:RTLabs_ext_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state s3' stk mtc0 ⇒
2013	λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2014	match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s3 stk mtc) → flat_trace ??? s1 with
2015	[ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2016	\| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
2017	] mtc0
2018	]
2019	] EX tld
2020	]
2021	(* Helper to keep adding the partial trace without violating the guardedness
2022	condition. *)
2023	and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge)
2024	: partial_flat_trace io_out io_in ge s s' →
2025	trace_label_diverges (RTLabs_status ge) s' →
2026	flat_trace io_out io_in ge s ≝
2027	match s' return λs':RTLabs_ext_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_ext_state sx stk mtc ⇒
2028	λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s' ? mtc) → flat_trace io_out io_in ge s with
2029	[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
2030	\| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ext_state ge s3 stk mtc) tr' tr)
2031	] mtc ]
2032	.
2033
2034
2035	coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2036	\| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2037	\| 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).
2038
2039	let corec flat_traces_are_determined_by_starting_point ge s tr1
2040	: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2041	match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2042	[ ft_stop s F ⇒ λtr2. ?
2043	\| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2044	match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2045	[ ft_stop s F ⇒ λEX. ?
2046	\| ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2047	] EX0
2048	].
2049	[ inversion tr2 in tr1 F;
2050	[ #s #F #_ #_ #tr1 #F' @eft_stop
2051	\| #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2052	cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2053	]
2054	\| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2055	\| -EX0
2056	cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2057	@(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2058	-E -EX' -tr2' #tr2' #EX'
2059	cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2060	@(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2061	-E -EX' #EX'
2062	@eft_step @flat_traces_are_determined_by_starting_point
2063	] qed.
2064
2065	let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
2066	(str:trace_label_diverges (RTLabs_status ge) s)
2067	(tr:flat_trace io_out io_in ge s)
2068	: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
2069	@flat_traces_are_determined_by_starting_point
2070	qed.
2071
2072	let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)
2073	(tr:trace_whole_program (RTLabs_status ge) s)
2074	on tr : flat_trace io_out io_in ge s ≝
2075	match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with
2076	[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2077	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2078	ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
2079	]
2080	\| twp_diverges s1 s2 CL EX tld ⇒
2081	match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2082	ft_step … EX' (flat_trace_of_label_diverges … tld)
2083	]
2084	].
2085
2086	let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
2087	(str:trace_whole_program (RTLabs_status ge) s)
2088	(tr:flat_trace io_out io_in ge s)
2089	: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
2090	@flat_traces_are_determined_by_starting_point
2091	qed.
2092
2093
2094
2095
2096
2097	(* We still need to link tal_unrepeating to our definition of cost soundness. *)
2098
2099
2100	(* Extract the "current" function from a state. *)
2101	definition state_fn : ∀ge. RTLabs_status ge → option block ≝
2102	λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? \| cons h t ⇒
2103	match Ras_state … s with
2104	[ Callstate _ _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' \| nil ⇒ None ? ]
2105	\| _ ⇒ Some ? h ] ].
2106
2107	(* Some results to invert the classification of states *)
2108
2109	lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
2110	as_execute (RTLabs_status ge) s s' →
2111	RTLabs_classify s = cl →
2112	match cl with
2113	[ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
2114	\| cl_return ⇒ ∀fn. P (rapc_ret fn)
2115	\| cl_other ⇒ ∀fn,l. P (rapc_state fn l)
2116	\| cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
2117	\| cl_tailcall ⇒ True
2118	] → P (as_pc_of (RTLabs_status ge) s).
2119	#ge #cl #P * *
2120	[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
2121	cases (next_instruction f) normalize
2122	#A #B try #C try #D try #E try #F try #G try #H try #J destruct //
2123	\| #vf #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
2124	\| #ret #dst #fs #m * [ \| #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
2125	\| #r #S #M #s' * #tr * #EX normalize in EX; destruct
2126	] qed.
2127
2128	definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL).
2129
2130	lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
2131	as_execute (RTLabs_status ge) s s' →
2132	RTLabs_classify s = cl →
2133	match cl with
2134	[ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
2135	\| cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
2136	\| cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2137	\| cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2138	\| cl_tailcall ⇒ False
2139	] .
2140	#ge * #s #s' #EX #CL whd
2141	@(declassify_pc … EX CL) whd
2142	[ #fn %{fn} % \| #fn #l %{fn} %{l} % \| #caller #callee %{caller} %{callee} % \| @I \| #fn #l %{fn} %{l} % ]
2143	qed.
2144
2145	lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
2146	as_execute (RTLabs_status ge) s s' →
2147	RTLabs_classify s = cl →
2148	match cl with
2149	[ cl_call ⇒ ∃vf,fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate vf fd args dst fs m) S M
2150	\| cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
2151	\| _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
2152	] .
2153	#ge #cl * * [ #f #fs #m \| #vf #fd #args #dst #fs #m \| #ret #dst #fs #m \| #r ]
2154	#S #M * #s' #S' #M' #EX #CL
2155	whd in CL:(??%?);
2156	[ cut (cl = cl_other ∨ cl = cl_jump)
2157	[ cases (next_instruction f) in CL;
2158	normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
2159	* #E >E %{f} %{fs} %{m} %{S} %{M} %
2160	\| <CL %{vf} %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
2161	\| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
2162	\| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
2163	] qed.
2164
2165	lemma State_not_callreturn : ∀f,fs,m,cl.
2166	RTLabs_classify (State f fs m) = cl →
2167	match cl with
2168	[ cl_return ⇒ False
2169	\| cl_call ⇒ False
2170	\| _ ⇒ True
2171	].
2172	#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
2173	cases (next_instruction f) //
2174	qed.
2175
2176	(* And some about traces *)
2177
2178	lemma tal_not_final : ∀ge,fl,s1,s2.
2179	∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2180	RTLabs_is_final (Ras_state … s1) = None ?.
2181	#ge #flx #s1x #s2x *
2182	[ #s1 #s2 * #tr * #EX #NX #CL #CS
2183	\| #s1 #s2 * #tr * #EX #NX #CL
2184	\| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
2185	\| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
2186	\| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
2187	\| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
2188	] @(step_not_final … EX)
2189	qed.
2190
2191	(* invert traces ending in a return *)
2192
2193	lemma tal_return : ∀ge,fl,s1,s2.
2194	as_classifier (RTLabs_status ge) s1 cl_return →
2195	∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2196	∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
2197	#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
2198	[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
2199	whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
2200	\| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
2201	%{EX} %{CL} % %
2202	\| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
2203	whd in CL CL'; >CL in CL'; #E destruct
2204	\| #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL')
2205	\| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
2206	whd in CL CL'; >CL in CL'; #E destruct
2207	\| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
2208	whd in CL CL'; >CL in CL'; #E destruct
2209	] qed.
2210
2211
2212	(* We need to link the pcs, states of the semantics with the labels and graphs
2213	of the syntax. *)
2214
2215	inductive pc_label : RTLabs_pc → label → Prop ≝
2216	\| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
2217	\| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
2218
2219	discriminator option.
2220
2221	lemma pc_label_eq : ∀pc,l1,l2.
2222	pc_label pc l1 →
2223	pc_label pc l2 →
2224	l1 = l2.
2225	#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
2226	qed.
2227
2228	lemma pc_label_call_eq : ∀l,fn,l'.
2229	pc_label (rapc_call (Some ? l) fn) l' →
2230	l = l'.
2231	#l #fn #l' #PC inversion PC
2232	#a #b #E1 #E2 #E3 destruct
2233	%
2234	qed.
2235
2236	inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
2237	\| gf : ∀b,fn.
2238	find_funct_ptr … ge b = Some ? (Internal ? fn) →
2239	graph_fn ge (Some ? b) (f_graph … fn).
2240
2241	lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
2242	graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
2243	g = f_graph (func f).
2244	#ge #f #fs #m * [] #fn #S #FFP #M #g #G
2245	inversion G
2246	#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
2247	%
2248	qed.
2249
2250	lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
2251	let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
2252	∀EV:eval_statement ge s = Value … 〈tr,s'〉.
2253	actual_successor s' = Some ? l →
2254	state_fn ge s = state_fn ge (next_state ge s s' tr EV).
2255	#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
2256	change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
2257	inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
2258	[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2259	\| #ge' #f' #f'' #m' #vf #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2260	\| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
2261	\| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
2262	>H33 in AS; normalize #AS destruct
2263	\| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2264	\| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
2265	] qed.
2266
2267	lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
2268	as_after_return (RTLabs_status ge) «pre,CL» post →
2269	as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
2270	match ret with
2271	[ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
2272	\| Some retl ⇒
2273	state_fn … pre = state_fn … post ∧
2274	pc_label (as_pc_of (RTLabs_status ge) post) retl
2275	].
2276	#ge #pre #post #CL #ret #callee #AF
2277	cases pre in CL AF ⊢ %;
2278	* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?);
2279	cases (next_instruction f) in CL;
2280	normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
2281	\| #vf #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
2282	\| #ret #dst #fs #m #S #M #CL normalize in CL; destruct
2283	\| #r #S #M #CL normalize in CL; destruct
2284	]
2285	cases post
2286	* [ #postf #postfs #postm * [*] #fn' #S' #M'
2287	\| 5: #postf #postfs #postm * [] #fn' #S' #M'
2288	\| 2,6: #A #B #C #D #E #F #G #H *
2289	\| 3,7: #A #B #C #D #E #F *
2290	\| #r #S' #M' #AF whd in AF; destruct
2291	\| #r #S' #M'
2292	]
2293	#AF #PC normalize in PC; destruct whd
2294	[ cases AF * #A #B #C destruct % [ % \| normalize >A // ]
2295	\| % #E normalize in E; destruct
2296	] qed.
2297
2298	lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
2299	actual_successor s = Some ? l →
2300	pc_label (as_pc_of (RTLabs_status ge) s) l.
2301	#ge * *
2302	[ #f #fs #m * [*] #fn #S #M #l #AS
2303	\| #vf #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
2304	\| #ret #dst #fs #m #S #M #l #AS
2305	\| #r #S #M #l #AS
2306	] whd in AS:(??%?); destruct //
2307	qed.
2308
2309	include alias "utilities/deqsets.ma".
2310
2311	(* Build the tail of the "bad" loop using the reappearance of the original pc,
2312	ignoring the rest of the trace_any_label once we see that pc. *)
2313
2314	let rec tal_pc_loop_tail ge flX s1X s2X
2315	(pc:as_pc (RTLabs_status ge)) g l
2316	(PC0:pc_label pc l)
2317	(tal: trace_any_label (RTLabs_status ge) flX s1X s2X)
2318	on tal :
2319	∀l1.
2320	pc_label (as_pc_of (RTLabs_status ge) s1X) l1 →
2321	graph_fn ge (state_fn … s1X) g →
2322	Not (as_costed (RTLabs_status ge) s1X) →
2323	pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal →
2324	bad_label_list g l l1 ≝ ?.
2325	cases tal
2326	[ #s1 #s2 #EX #CL #CS
2327	#l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2328	>(pc_label_eq … PC0 PC1) %1
2329	\| #s1 #s2 #EX #CL
2330	#l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2331	>(pc_label_eq … PC0 PC1) %1
2332	\| #pre #start #final #EX #CL #AF #tlr #CS
2333	#l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2334	>(pc_label_eq … PC0 PC1) %1
2335	\| #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL)
2336	\| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
2337	#l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2338	[ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2339	\| #NE #IN
2340	lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
2341	[ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
2342	lapply (pc_label_call_eq … PC1) #E destruct
2343	@(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN)
2344	\| @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct
2345	]
2346	]
2347	\| #fl #pre #init #end #EX #tal' #CL #CS
2348	#l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2349	[ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2350	\| #NE #IN
2351	cases (declassify_state … EX (simplify_cl … CL))
2352	#f * #fs * #m * #S * #M #E destruct
2353	cut (l1 = next f)
2354	[ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1
2355	inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct
2356	cases EX #tr * #EV #NX
2357	cases (eval_successor … EV)
2358	[ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct
2359	lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
2360	#fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
2361	\| * #l' * #AS #SC
2362	lapply (graph_fn_state … G) #E destruct
2363	@(gl_step … l')
2364	[ @(next_ok f)
2365	\| @Exists_memb @SC
2366	\| @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??))
2367	@ISL
2368	\| @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS))
2369	[ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G
2370	\| *: //
2371	]
2372	]
2373	]
2374	]
2375	] qed.
2376
2377	(* Combine the above result with the result on bad loops in CostMisc.ma to show
2378	that the pc of a normal instruction execution state can't be repeated within
2379	a trace_any_label. *)
2380
2381	lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
2382	soundly_labelled_state s1 →
2383	RTLabs_classify s1 = cl_other →
2384	as_execute (RTLabs_status ge) s1 s2 →
2385	¬ as_costed (RTLabs_status ge) s2 →
2386	¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal.
2387	#ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL)
2388	#f * #fs * #m * * [* ] #fn #S * #FFP #M #E destruct
2389	cases EX #tr * #EV #NX
2390	cases (eval_successor … EV)
2391	[ * #CL2 #SC
2392	cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
2393	@notb_Prop % whd in match (tal_pc_list ?????); #IN
2394	lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
2395	#ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct
2396	normalize #E destruct
2397	\| * #l2 * #AS2 #SC1 @notb_Prop % #IN
2398	(* Two cases: either s1 is a cost label, and it's pc's appearence later on
2399	is impossible because nothing later in tal can be a cost label; or it
2400	isn't and we get a loop of successor instruction labels that breaks the
2401	soundness of the cost labelling. *)
2402	cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
2403	[ * #H @H
2404	cases (memb_exists … IN) #left * #right #E
2405	@(All_split … (tal_tail_not_costed … tal CS2) … E)
2406	\| (* Now show that the loop invalidates soundness. *)
2407	cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
2408	[ %1 ] #PC1
2409	cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
2410	[ /2/ ] #PC2
2411	lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN)
2412	[ <NX <(state_fn_next … EV AS2) % // ]
2413	cases S1 #SLF #_ cases (SLF (next f) (next_ok f))
2414	#bound1 #BOUND1 #BLL #CS1
2415	cases (bound_step1 … BOUND1 … SC1)
2416	#bound2 #BOUND2 @(absurd … BOUND2)
2417	@(loop_soundness_contradiction … BLL)
2418	[ @(next_ok f)
2419	\| @SC1
2420	\| @notb_Prop @(not_to_not … CS1) #CS
2421	@(proj1 … (RTLabs_costed …)) @CS
2422	]
2423	]
2424	] qed.
2425
2426	(* We need a similar result for call states. We'll do this by showing that
2427	the state following the call state is a normal instruction state and using
2428	the previous result. *)
2429
2430	lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2431	as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2432	as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2433	as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2434	state_fn … s1 = state_fn … s2 →
2435	as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
2436	#ge * #s1 #S1 #M1 #CL1
2437	cases (rtlabs_call_inv … (simplify_cl … CL1)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
2438	* #s2 #S2 #M2 #CL2
2439	cases (rtlabs_call_inv … (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
2440	* * [ #f3 #fs3 #m3 #S3 #M3 \| #a #b #c #d #e #f #g #h #i * \| #a #b #c #d #e #f #g * \| #r3 #S3 #M3 ]
2441	* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 \| 2,6: #a #b #c #d #e #f #g #h #i * \| 3,7: #a #b #c #d #e #f #g * \| 4,8: #r4 #S4 #M4 ]
2442	whd in ⊢ (% → ?);
2443	[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M ] #f1' #fs1 cases S1 [1,3:] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
2444	* * #N1 #F1 #STK1
2445	whd in STK1 ⊢ (% → ?);
2446	[ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [] #fn2 [* #X ] #fn2 #S2' #M2 * #N2 #F2 #STK2
2447	normalize in ⊢ (% → % → ?); #E1 #E2
2448	cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1
2449	cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2
2450	whd in ⊢ (??%%); <N2 <N1 destruct >e1 %
2451	\| #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?);
2452	#X destruct
2453	]
2454	\| #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M ] #f2 #fs2' cases S2 [] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2455	cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1
2456	normalize in ⊢ (% → ?); #E destruct
2457	\| #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ %
2458	] qed.
2459
2460	lemma eq_pc_eq_classify : ∀ge,s1,s2.
2461	as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2462	RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
2463	#ge
2464	* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [] #fn1 #S1 #M1 \| #vf1 #fd1 #args1 #dst1 #fs1 #m1 [] #fn1 #S1 #M1 \| #ret1 #dst1 #fs1 #m1 #S1 #M1 \| #r1 [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
2465	* * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:] #fn2 #S2 #M2 \| 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 [1,3,5,7:] #fn2 #S2 #M2 \| 3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2 \| 4,8,12,16: #r2 [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
2466	whd in ⊢ (??%% → ?); #E destruct try %
2467	[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
2468	change with (lookup_present … next2 nok1) in match (next_instruction ?);
2469	cases (lookup_present … next2 nok1)
2470	normalize //
2471	\| 2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct
2472	\| 4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct
2473	] qed.
2474
2475	lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2476	as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2477	as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2478	as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2479	state_fn … s1 = state_fn … s2 →
2480	RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4).
2481	#ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN
2482	@eq_pc_eq_classify
2483	@(pc_after_return_eq … AF1 AF2 PC FN)
2484	qed.
2485
2486	lemma cost_labels_are_other : ∀ge,s.
2487	as_costed (RTLabs_status ge) s →
2488	RTLabs_classify (Ras_state … s) = cl_other.
2489	#ge * * [ #f #fs #m #S #M \| #vf #fd #args #dst #fs #m #S #M \| #ret #dst #fs #m #S #M \| #r #S #M ]
2490	#CS lapply (proj2 … (RTLabs_costed …) … CS)
2491	whd in ⊢ (??%? → %);
2492	[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
2493	#A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
2494	\| *: #E destruct
2495	] qed.
2496
2497	lemma eq_pc_cost : ∀ge,s1,s2.
2498	as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2499	as_costed (RTLabs_status ge) s1 →
2500	as_costed (RTLabs_status ge) s2.
2501	#ge
2502	* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 \| #vf1 #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 \| #ret1 #dst1 #fs1 #m1 #S1 #M1 \| #r1 #S1 #M1 ]
2503	[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
2504	* * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [] #fn2 #S2 #M2 \| 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 [1,3,5,7:] #fn2 #S2 #M2 \| 3,7,11,15: #ret2 #dst2 #fs2 #m2 [2: #fn2 #S2] #M2 \| 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
2505	whd in ⊢ (??%% → ?); #E destruct
2506	#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
2507	cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
2508	qed.
2509
2510	lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal.
2511	RTLabs_classify (Ras_state … s1) = cl_other →
2512	as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal.
2513	#ge #flX #s1X #s2X *
2514	[ #s1 #s2 #EX *
2515	[ whd in ⊢ (% → ?); #CL #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2516	\| #CL #CS #CL' @eq_true_to_b @memb_hd
2517	]
2518	\| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2519	\| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2520	\| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
2521	\| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2522	\| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
2523	] qed.
2524
2525	lemma state_fn_after_return : ∀ge,pre,post,CL.
2526	as_after_return (RTLabs_status ge) «pre,CL» post →
2527	state_fn … pre = state_fn … post.
2528	#ge * #pre #preS #preM * #post #postS #postM #CL #AF
2529	cases (rtlabs_call_inv … (simplify_cl … CL)) #vf * #fd * #args * #dst * #fs * #m #E destruct
2530	cases post in postM AF ⊢ %;
2531	[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
2532	cases preS in preM AF ⊢ %; [*]
2533	#fn *
2534	[ cases fs [ #M * ]
2535	#f #fs' * #FFP *
2536	\| #fn' #S cases fs [ #M * ]
2537	#f #fs' #M * * #N #F #PC destruct %
2538	]
2539	\| #A #B #C #D #E #F #G *
2540	\| #A #B #C #D #E *
2541	\| #r #M' #AF whd in AF; destruct
2542	cases preS in preM ⊢ %;
2543	[ // \| #fn * [ // \| #fn' #S * #FFP * ] ]
2544	] qed.
2545
2546	lemma state_fn_other : ∀ge,s1,s2.
2547	RTLabs_classify (Ras_state … s1) = cl_other →
2548	as_execute (RTLabs_status ge) s1 s2 →
2549	RTLabs_classify (Ras_state … s2) = cl_return ∨
2550	state_fn … s1 = state_fn … s2.
2551	#ge #s1 #s2 #CL #EX
2552	cases (declassify_state … EX CL)
2553	#f * #fs * #m * * [*] #fn #S #M #E destruct
2554	inversion (eval_preserves_ext … EX)
2555	[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
2556	\| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct %2 %
2557	\| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2558	\| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
2559	\| #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
2560	\| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
2561	] qed.
2562
2563	(* The main part of the proof is to walk down the trace_any_label and find the
2564	repeated call state, then show that its successor appears as well. *)
2565
2566	let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
2567	(AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2)
2568	(CL2:RTLabs_classify (Ras_state … s2) = cl_other)
2569	(CS2:Not (as_costed (RTLabs_status ge) s2))
2570	(EX1:as_execute (RTLabs_status ge) s1 s1') on tal :
2571	state_fn … s1 = state_fn … s3 →
2572	as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal →
2573	as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?.
2574	cases tal
2575	[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
2576	whd in match (tal_pc_list ?????) in IN;
2577	lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2578	cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l
2579	#IN' destruct
2580	\| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
2581	lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2582	@(declassify_pc_cl … EX2 CL2) whd #fn
2583	#IN' destruct
2584	\| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
2585	lapply (memb_single … IN) #E
2586	lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
2587	@⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
2588	\| #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL)
2589	\| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
2590	whd in ⊢ (?% → ?); @eqb_elim
2591	[ #PC #_
2592	>(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list
2593	<(classify_after_return_eq … AF1 AF3 PC FN) assumption
2594	\| #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons
2595	@(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN)
2596	>FN @(state_fn_after_return … AF3)
2597	]
2598	\| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
2599	lapply (simplify_cl … CL1) #CL1'
2600	lapply (simplify_cl … CL3) #CL3'
2601	@eq_true_to_b @memb_cons
2602	@(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
2603	[ >FN cases (state_fn_other … CL3' EX3)
2604	[ #CL3'' @⊥
2605	cases (tal_return … (lift_cl … CL3'') tal3')
2606	#EX3' * #CL3''' * #E1 #E2 destruct
2607	whd in IN:(?%); lapply IN @eqb_elim
2608	[ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2609	\| #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct
2610	]
2611	\| //
2612	]
2613	\| lapply IN whd in ⊢ (?% → ?); @eqb_elim
2614	[ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2615	\| #NE #IN @IN
2616	]
2617	]
2618	] qed.
2619
2620	(* Then we can start the proof by finding the original successor state... *)
2621
2622	lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
2623	as_execute (RTLabs_status ge) s1 s1' →
2624	as_after_return (RTLabs_status ge) «s1,CL» s2 →
2625	¬as_costed (RTLabs_status ge) s2 →
2626	as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal →
2627	∃s3,EX,CL',CS,tal'.
2628	tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
2629	bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
2630	#ge #s1 #s1' #CL #flX #s2X #s4X *
2631	[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
2632	whd in match (tal_pc_list ?????) in IN;
2633	lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2634	cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l
2635	#IN' destruct
2636	\| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
2637	lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2638	@(declassify_pc_cl … EX2 CL2) whd #fn
2639	#IN' destruct
2640	\| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
2641	cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2642	cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2643	cases AF1
2644	\| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
2645	\| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
2646	cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2647	cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2648	cases AF1
2649	\| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
2650	lapply (simplify_cl … CL) #CL'
2651	lapply (simplify_cl … CL2) #CL2'
2652	%{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
2653	(* Now that we've inverted the first part of the trace, look for the repeat. *)
2654	@(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1)
2655	[ >(state_fn_after_return … AF1)
2656	cases (state_fn_other … CL2' EX2)
2657	[ #CL3 @⊥
2658	cases (tal_return … (lift_cl … CL3) tal3)
2659	#EX3 * #CL3' * #E1 #E2 destruct
2660	lapply (simplify_cl … CL3') #CL3''
2661	whd in IN:(?%); lapply IN @eqb_elim
2662	[ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2663	\| #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct
2664	]
2665	\| //
2666	]
2667	\| lapply IN whd in ⊢ (?% → ?); @eqb_elim
2668	[ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2669	\| #NE #IN @IN
2670	]
2671	]
2672	] qed.
2673
2674	(* And then we get our counterpart to no_loops_in_tal for calls: *)
2675
2676	lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
2677	∀tal:trace_any_label (RTLabs_status ge) fl after final.
2678	as_execute (RTLabs_status ge) pre start →
2679	as_after_return (RTLabs_status ge) «pre,CL» after →
2680	¬as_costed (RTLabs_status ge) after →
2681	soundly_labelled_state (Ras_state ge after) →
2682	¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal.
2683	#ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN
2684	cases (pc_after_call_repeats … EX AF CS IN)
2685	#s * #EX * #CL' * #CSx * #tal' * #E #IN'
2686	@(absurd ? IN')
2687	@Prop_notb
2688	@no_loops_in_tal /2/
2689	qed.
2690
2691	(* Show that if a state is soundly labelled, then so are the states following
2692	it in a trace. *)
2693
2694	lemma soundly_step : ∀ge,s1,s2.
2695	soundly_labelled_ge ge →
2696	as_execute (RTLabs_status ge) s1 s2 →
2697	soundly_labelled_state (Ras_state … s1) →
2698	soundly_labelled_state (Ras_state … s2).
2699	#ge #s1 #s2 #GE * #tr * #EX #NX
2700	@(soundly_labelled_state_step … GE … EX)
2701	qed.
2702
2703	let rec tlr_sound ge s1 s2
2704	(tlr:trace_label_return (RTLabs_status ge) s1 s2)
2705	(GE:soundly_labelled_ge ge)
2706	on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2707	match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with
2708	[ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1
2709	\| tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in
2710	tlr_sound … tlr' GE S2
2711	]
2712	and tll_sound ge fl s1 s2
2713	(tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2714	(GE:soundly_labelled_ge ge)
2715	on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2716	match tll with
2717	[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
2718	]
2719	and tal_sound ge fl s1 s2
2720	(tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2721	(GE:soundly_labelled_ge ge)
2722	on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2723	match tal with
2724	[ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1
2725	\| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
2726	\| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
2727	\| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2728	\| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
2729	\| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
2730	].
2731	@(RTLabs_notail' … CL)
2732	qed.
2733
2734	(* And join everything up to show that soundly labelled states give unrepeating
2735	traces. *)
2736
2737	let rec tlr_sound_unrepeating ge
2738	(s1,s2:RTLabs_status ge)
2739	(GE:soundly_labelled_ge ge)
2740	(tlr:trace_label_return (RTLabs_status ge) s1 s2)
2741	on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝
2742	match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with
2743	[ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1
2744	\| tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1))
2745	]
2746	and tll_sound_unrepeating ge fl
2747	(s1,s2:RTLabs_status ge)
2748	(GE:soundly_labelled_ge ge)
2749	(tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2750	on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
2751	match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with
2752	[ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal
2753	]
2754	and tal_sound_unrepeating ge fl
2755	(s1,s2:RTLabs_status ge)
2756	(GE:soundly_labelled_ge ge)
2757	(tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2758	on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
2759	match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with
2760	[ tal_base_not_return _ _ EX _ _ ⇒ λS1. I
2761	\| tal_base_return _ _ EX _ ⇒ λS1. I
2762	\| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
2763	tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
2764	\| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2765	\| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
2766	conj ?? (conj ???
2767	(tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1))))
2768	(tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1))
2769	\| tal_step_default _ pre init end EX tal CL _ ⇒ λS1.
2770	conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
2771	].
2772	[ @(RTLabs_notail' … CL)
2773	\| @(no_repeats_of_calls … EX AF) [ assumption \|
2774	@(tlr_sound … tlr) [ assumption \| @(soundly_step … GE EX S1) ] ]
2775	\| @no_loops_in_tal // @simplify_cl @CL
2776	] qed.
2777

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format