source: src/RTLabs/Traces.ma @ 2499

Last change on this file since 2499 was 2499, checked in by campbell, 7 years ago

Separate out the RTLabs abstract status record from the proofs about
structured traces. Tidy up "next instruction" references from
the semantics.

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