source: src/RTLabs/RTLabs_partial_traces.ma @ 2895

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

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

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