Context Navigation

Traces.ma @ 2407

Last change on this file since 2407 was 2314, checked in by campbell, 9 years ago
Move generic definitions from recent commit to appropriate places.
File size: 132.5 KB

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

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

Download in other formats:

Original Format