Context Navigation

Traces.ma @ 2184

Last change on this file since 2184 was 2184, checked in by campbell, 7 years ago
Minor fix ups.
File size: 107.5 KB

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

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

Download in other formats:

Original Format