source: src/RTLabs/RTLabs_partial_traces.ma @ 2839

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

Basic structure of RTLabs measurable to structured traces results.

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