source: src/RTLabs/RTLabs_partial_traces.ma @ 2894

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

Some progress on showing that the change to structured traces preserves
observables.

File size: 107.7 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 _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
1491   | _ ⇒ False ].
1492#p #s
1493@bind_ok #m #Em
1494@bind_ok #b #Eb
1495@bind_ok #f #Ef
1496#E whd in E:(??%%); destruct
1497%{b} whd
1498% // @Ef
1499qed.
1500
1501definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
1502λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
1503cases (init_state_is p s I) #b
1504cases s
1505[ #f #fs #m *
1506| #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
1507| #rv #rr #fs #m *
1508| #r *
1509] qed.
1510
1511lemma well_cost_labelled_initial : ∀p,s.
1512  make_initial_state p = OK ? s →
1513  well_cost_labelled_program p →
1514  well_cost_labelled_state s ∧ soundly_labelled_state s.
1515#p #s
1516@bind_ok #m #Em
1517@bind_ok #b #Eb
1518@bind_ok #f #Ef
1519#E destruct
1520whd in ⊢ (% → %);
1521#WCL
1522@(find_funct_ptr_All ??????? Ef)
1523@(All_mp … WCL)
1524* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
1525qed.
1526
1527lemma well_cost_labelled_make_global : ∀p.
1528  well_cost_labelled_program p →
1529  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
1530#p whd in ⊢ (% → ?%%);
1531#WCL %
1532#b #f #FFP
1533[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
1534| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
1535] @(All_mp … WCL)
1536* #id * #fn // * /2/
1537qed.
1538(*
1539theorem program_trace_exists :
1540  termination_oracle →
1541  ∀p:RTLabs_program.
1542  well_cost_labelled_program p →
1543  ∀s:state.
1544  ∀I: make_initial_state p = OK ? s.
1545 
1546  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1547 
1548  ∀NOIO:exec_no_io … plain_trace.
1549  ∀NW:not_wrong … plain_trace.
1550 
1551  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
1552 
1553  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
1554
1555#ORACLE #p #WCL #s #I
1556letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1557#NOIO #NW
1558letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
1559whd
1560@(whole_structured_trace_exists (make_global p) p ? ORACLE)
1561[ @(proj1 … (well_cost_labelled_make_global … WCL))
1562| @(proj2 … (well_cost_labelled_make_global … WCL))
1563| @flat_trace
1564| @I
1565| @(proj1 ?? (well_cost_labelled_initial … I WCL))
1566| @(proj2 ?? (well_cost_labelled_initial … I WCL))
1567] qed.
1568*)
1569
1570lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
1571  as_execute (RTLabs_status ge) s s' →
1572  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
1573#ge #s #s' * #tr * #EX #_ %{tr} @EX
1574qed.
1575
1576(* as_execute might be in Prop, but because the semantics is deterministic
1577   we can retrieve the event trace anyway. *)
1578
1579let rec deprop_execute ge (s,s':state)
1580  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
1581: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1582match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
1583[ Value ts ⇒ λY. «fst … ts, ?»
1584| _ ⇒ λY. ⊥
1585] X.
1586[ 1,3: cases Y #x #E destruct
1587| cases Y #trP #E destruct @refl
1588] qed.
1589
1590let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
1591  (X:as_execute (RTLabs_status ge) s s')
1592: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1593deprop_execute ge s s' ?.
1594cases X #tr * #EX #_ %{tr} @EX
1595qed.
1596
1597(* A non-empty finite section of a flat_trace *)
1598inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1599| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1600| 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''.
1601
1602let rec append_partial_flat_trace o i ge s1 s2 s3
1603  (tr1:partial_flat_trace o i ge s1 s2)
1604on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1605match tr1 with
1606[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1607| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1608].
1609
1610let rec partial_to_flat_trace o i ge s1 s2
1611  (tr:partial_flat_trace o i ge s1 s2)
1612on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1613match tr with
1614[ pft_base s tr s' EX ⇒ ft_step … EX
1615| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1616].
1617
1618(* Extract a flat trace from a structured one. *)
1619let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
1620  (tr:trace_label_return (RTLabs_status ge) s s')
1621on tr :
1622  partial_flat_trace io_out io_in ge s s' ≝
1623match tr with
1624[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
1625| tlr_step s1 s2 s3 tll tlr ⇒
1626  append_partial_flat_trace …
1627    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
1628    (flat_trace_of_label_return ge s2 s3 tlr)
1629]
1630and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
1631  (tr:trace_label_label (RTLabs_status ge) ends s s')
1632on tr :
1633  partial_flat_trace io_out io_in ge s s' ≝
1634match tr with
1635[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
1636]
1637and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
1638  (tr:trace_any_label (RTLabs_status ge) ends s s')
1639on tr :
1640  partial_flat_trace io_out io_in ge s s' ≝
1641match tr with
1642[ tal_base_not_return s1 s2 EX CL CS ⇒
1643    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1644    pft_base … EX' ]
1645| tal_base_return s1 s2 EX CL ⇒
1646    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1647    pft_base … EX' ]
1648| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
1649    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
1650    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1651    pft_step … EX' suffix' ]
1652| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
1653    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1654    pft_step … EX'
1655      (append_partial_flat_trace …
1656        (flat_trace_of_label_return ge ?? tlr)
1657        (flat_trace_of_any_label ge ??? tal))
1658    ]
1659| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
1660    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1661      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
1662    ]
1663| tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥
1664].
1665@(RTLabs_notail' … CL)
1666qed.
1667
1668(* We take an extra step so that we can always return a non-empty trace to
1669   satisfy the guardedness condition in the cofixpoint. *)
1670let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
1671  (tr:trace_any_call (RTLabs_status ge) s s')
1672  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1673on tr :
1674  partial_flat_trace io_out io_in ge s s'' ≝
1675match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
1676[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
1677| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
1678    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
1679    pft_step … EX'
1680      (append_partial_flat_trace …
1681        (flat_trace_of_label_return ge ?? tlr)
1682        (flat_trace_of_any_call ge … tac EX''))
1683    ]
1684| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
1685    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1686    pft_step … EX'
1687     (flat_trace_of_any_call ge … tal EX'')
1688    ]
1689] EX''.
1690
1691let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
1692  (tr:trace_label_call (RTLabs_status ge) s s')
1693  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1694on tr :
1695  partial_flat_trace io_out io_in ge s s'' ≝
1696match tr with
1697[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
1698] EX''.
1699
1700
1701
1702
1703(* We still need to link tal_unrepeating to our definition of cost soundness. *)
1704
1705
1706(* Extract the "current" function from a state. *)
1707definition state_fn : ∀ge. RTLabs_status ge → option block ≝
1708λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
1709  match Ras_state … s with
1710  [ Callstate _ _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
1711  | _ ⇒  Some ? h ] ].
1712
1713(* Some results to invert the classification of states *)
1714
1715lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
1716  as_execute (RTLabs_status ge) s s' →
1717  RTLabs_classify s = cl →
1718  match cl with
1719  [ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
1720  | cl_return ⇒ ∀fn. P (rapc_ret fn)
1721  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
1722  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
1723  | cl_tailcall ⇒ True
1724  ] → P (as_pc_of (RTLabs_status ge) s).
1725#ge #cl #P * *
1726[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
1727  cases (next_instruction f) normalize
1728  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
1729| #vf #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
1730| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
1731| #r #S #M #s' * #tr * #EX normalize in EX; destruct
1732] qed.
1733
1734definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL).
1735
1736lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
1737  as_execute (RTLabs_status ge) s s' →
1738  RTLabs_classify s = cl →
1739  match cl with
1740  [ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
1741  | cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
1742  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
1743  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
1744  | cl_tailcall ⇒ False
1745  ] .
1746#ge * #s #s' #EX #CL whd
1747@(declassify_pc … EX CL) whd
1748[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | @I | #fn #l %{fn} %{l} % ]
1749qed.
1750
1751lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
1752  as_execute (RTLabs_status ge) s s' →
1753  RTLabs_classify s = cl →
1754  match cl with
1755  [ 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
1756  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
1757  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
1758  ] .
1759#ge #cl * * [ #f #fs #m | #vf #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
1760#S #M * #s' #S' #M' #EX #CL
1761whd in CL:(??%?);
1762[ cut (cl = cl_other ∨ cl = cl_jump)
1763  [ cases (next_instruction f) in CL;
1764    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
1765  * #E >E %{f} %{fs} %{m} %{S} %{M} %
1766| <CL %{vf} %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
1767| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
1768| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
1769] qed.
1770
1771lemma State_not_callreturn : ∀f,fs,m,cl.
1772  RTLabs_classify (State f fs m) = cl →
1773  match cl with
1774  [ cl_return ⇒ False
1775  | cl_call ⇒ False
1776  | _ ⇒ True
1777  ].
1778#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
1779cases (next_instruction f) //
1780qed.
1781
1782(* And some about traces *)
1783
1784lemma tal_not_final : ∀ge,fl,s1,s2.
1785  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
1786  RTLabs_is_final (Ras_state … s1) = None ?.
1787#ge #flx #s1x #s2x *
1788[ #s1 #s2 * #tr * #EX #NX #CL #CS
1789| #s1 #s2 * #tr * #EX #NX #CL
1790| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
1791| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
1792| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
1793| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
1794] @(step_not_final … EX)
1795qed.
1796
1797(* invert traces ending in a return *)
1798
1799lemma tal_return : ∀ge,fl,s1,s2.
1800  as_classifier (RTLabs_status ge) s1 cl_return →
1801  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
1802  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
1803#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
1804[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
1805  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
1806| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
1807  %{EX} %{CL} % %
1808| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
1809  whd in CL CL'; >CL in CL'; #E destruct
1810| #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL')
1811| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
1812  whd in CL CL'; >CL in CL'; #E destruct
1813| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
1814  whd in CL CL'; >CL in CL'; #E destruct
1815] qed.
1816
1817
1818(* We need to link the pcs, states of the semantics with the labels and graphs
1819   of the syntax. *)
1820
1821inductive pc_label : RTLabs_pc → label → Prop ≝
1822| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
1823| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
1824
1825discriminator option.
1826
1827lemma pc_label_eq : ∀pc,l1,l2.
1828  pc_label pc l1 →
1829  pc_label pc l2 →
1830  l1 = l2.
1831#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
1832qed.
1833
1834lemma pc_label_call_eq : ∀l,fn,l'.
1835  pc_label (rapc_call (Some ? l) fn) l' →
1836  l = l'.
1837#l #fn #l' #PC inversion PC
1838#a #b #E1 #E2 #E3 destruct
1839%
1840qed.
1841
1842inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
1843| gf : ∀b,fn.
1844    find_funct_ptr … ge b = Some ? (Internal ? fn) →
1845    graph_fn ge (Some ? b) (f_graph … fn).
1846
1847lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
1848  graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
1849  g = f_graph (func f).
1850#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
1851inversion G
1852#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
1853%
1854qed.
1855
1856lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
1857  let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
1858  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
1859  actual_successor s' = Some ? l →
1860  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
1861#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
1862change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
1863inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
1864[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
1865| #ge' #f' #f'' #m' #vf #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
1866| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
1867| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
1868  >H33 in AS; normalize #AS destruct
1869| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
1870| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
1871] qed.
1872
1873lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
1874  as_after_return (RTLabs_status ge) «pre,CL» post →
1875  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
1876  match ret with
1877  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
1878  | Some retl ⇒
1879    state_fn … pre = state_fn … post ∧
1880    pc_label (as_pc_of (RTLabs_status ge) post) retl
1881  ].
1882#ge #pre #post #CL #ret #callee #AF
1883cases pre in CL AF ⊢ %;
1884* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??%?);
1885    cases (next_instruction f) in CL;
1886    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
1887  | #vf #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
1888  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
1889  | #r #S #M #CL normalize in CL; destruct
1890  ]
1891cases post
1892* [ #postf #postfs #postm * [*] #fn' #S' #M'
1893  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
1894  | 2,6: #A #B #C #D #E #F #G #H *
1895  | 3,7: #A #B #C #D #E #F *
1896  | #r #S' #M' #AF whd in AF; destruct
1897  | #r #S' #M'
1898  ]
1899#AF #PC normalize in PC; destruct whd
1900[ cases AF * #A #B #C destruct % [ % | normalize >A // ]
1901| % #E normalize in E; destruct
1902] qed.
1903
1904lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
1905  actual_successor s = Some ? l →
1906  pc_label (as_pc_of (RTLabs_status ge) s) l.
1907#ge * *
1908[ #f #fs #m * [*] #fn #S #M #l #AS
1909| #vf #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
1910| #ret #dst #fs #m #S #M #l #AS
1911| #r #S #M #l #AS
1912] whd in AS:(??%?); destruct //
1913qed.
1914
1915include alias "utilities/deqsets_extra.ma".
1916
1917(* Build the tail of the "bad" loop using the reappearance of the original pc,
1918   ignoring the rest of the trace_any_label once we see that pc. *)
1919
1920let rec tal_pc_loop_tail ge flX s1X s2X
1921  (pc:as_pc (RTLabs_status ge)) g l
1922  (PC0:pc_label pc l)
1923  (tal: trace_any_label (RTLabs_status ge) flX s1X s2X)
1924on tal :
1925  ∀l1.
1926  pc_label (as_pc_of (RTLabs_status ge) s1X) l1 →
1927  graph_fn ge (state_fn … s1X) g →
1928  Not (as_costed (RTLabs_status ge) s1X) →
1929  pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal →
1930  bad_label_list g l l1 ≝ ?.
1931cases tal
1932[ #s1 #s2 #EX #CL #CS
1933  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
1934  >(pc_label_eq … PC0 PC1) %1
1935| #s1 #s2 #EX #CL
1936  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
1937  >(pc_label_eq … PC0 PC1) %1
1938| #pre #start #final #EX #CL #AF #tlr #CS
1939  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
1940  >(pc_label_eq … PC0 PC1) %1
1941| #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL)
1942| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
1943  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
1944  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
1945  | #NE #IN
1946    lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
1947    [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
1948      lapply (pc_label_call_eq … PC1) #E destruct
1949      @(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN)
1950    | @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct
1951    ]
1952  ]
1953| #fl #pre #init #end #EX #tal' #CL #CS
1954  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
1955  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
1956  | #NE #IN
1957    cases (declassify_state … EX (simplify_cl … CL))
1958    #f * #fs * #m * #S * #M #E destruct
1959    cut (l1 = next f)
1960    [ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1
1961      inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct
1962    cases EX #tr * #EV #NX
1963    cases (eval_successor … EV)
1964    [ * #CL' @⊥ cases (tal_return … (CL') tal') #EX' * #CL'' * #E1 #E2 destruct
1965      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
1966      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
1967    | * #l' * #AS #SC
1968      lapply (graph_fn_state … G) #E destruct
1969      @(gl_step … l')
1970      [ @(next_ok f)
1971      | @Exists_memb @SC
1972      | @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??))
1973        @ISL
1974      | @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS))
1975        [ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G
1976        | *: //
1977        ]
1978      ]
1979    ]
1980  ]
1981] qed.
1982
1983(* Combine the above result with the result on bad loops in CostMisc.ma to show
1984   that the pc of a normal instruction execution state can't be repeated within
1985   a trace_any_label. *)
1986
1987lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
1988  soundly_labelled_state s1 →
1989  RTLabs_classify s1 = cl_other →
1990  as_execute (RTLabs_status ge) s1 s2 →
1991  ¬ as_costed (RTLabs_status ge) s2 →
1992  ¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal.
1993#ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL)
1994#f * #fs * #m * * [* *] #fn #S * * #FFP #M #E destruct
1995cases EX #tr * #EV #NX
1996cases (eval_successor … EV)
1997[ * #CL2 #SC
1998  cases (tal_return … (CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
1999  @notb_Prop % whd in match (tal_pc_list ?????); #IN
2000  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
2001  #ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct
2002  normalize #E destruct
2003| * #l2 * #AS2 #SC1 @notb_Prop % #IN
2004  (* Two cases: either s1 is a cost label, and it's pc's appearence later on
2005     is impossible because nothing later in tal can be a cost label; or it
2006     isn't and we get a loop of successor instruction labels that breaks the
2007     soundness of the cost labelling. *)
2008  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
2009  [ * #H @H
2010    cases (memb_exists … IN) #left * #right #E
2011    @(All_split … (tal_tail_not_costed … tal CS2) … E)
2012  | (* Now show that the loop invalidates soundness. *)
2013    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))
2014    [ %1 ] #PC1
2015    cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
2016    [ /2/ ] #PC2
2017    lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN)
2018    [ <NX <(state_fn_next … EV AS2) % // ]
2019    cases S1 #SLF #_ cases (SLF (next f) (next_ok f))
2020    #bound1 #BOUND1 #BLL #CS1
2021    cases (bound_step1 … BOUND1 … SC1)
2022    #bound2 #BOUND2 @(absurd … BOUND2)
2023    @(loop_soundness_contradiction … BLL)
2024    [ @(next_ok f)
2025    | @SC1
2026    | @notb_Prop @(not_to_not … CS1) #CS
2027      @(proj1 … (RTLabs_costed …)) @CS
2028    ]
2029  ]
2030] qed.
2031
2032(* We need a similar result for call states.  We'll do this by showing that
2033   the state following the call state is a normal instruction state and using
2034   the previous result. *)
2035
2036lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2037  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2038  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2039  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2040  state_fn … s1 = state_fn … s2 →
2041  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
2042#ge * #s1 #S1 #M1 #CL1
2043cases (rtlabs_call_inv … (simplify_cl … CL1)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
2044* #s2 #S2 #M2 #CL2
2045cases (rtlabs_call_inv … (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
2046* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h #i * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
2047* * [ 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 ]
2048whd in ⊢ (% → ?);
2049[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
2050    * * #N1 #F1 #STK1
2051    whd in STK1 ⊢ (% → ?);
2052    [ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [*] #fn2 * [* #X *] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2053      normalize in ⊢ (% → % → ?); #E1 #E2
2054      cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1
2055      cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2
2056      whd in ⊢ (??%%); <N2 <N1 destruct >e1 %
2057    | #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?);
2058      #X destruct
2059    ]
2060| #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M *] #f2 #fs2' cases S2 [*] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2061  cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1
2062  normalize in ⊢ (% → ?); #E destruct
2063| #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ %
2064] qed.
2065
2066lemma eq_pc_eq_classify : ∀ge,s1,s2.
2067  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2068  RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
2069#ge
2070* * [ * #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 ]
2071* * [ 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 ]
2072whd in ⊢ (??%% → ?); #E destruct try %
2073[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
2074  change with (lookup_present … next2 nok1) in match (next_instruction ?);
2075  cases (lookup_present … next2 nok1)
2076  normalize //
2077| 2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct
2078| 4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct
2079] qed.
2080
2081lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2082  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2083  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2084  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2085  state_fn … s1 = state_fn … s2 →
2086  RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4).
2087#ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN
2088@eq_pc_eq_classify
2089@(pc_after_return_eq … AF1 AF2 PC FN)
2090qed.
2091
2092lemma cost_labels_are_other : ∀ge,s.
2093  as_costed (RTLabs_status ge) s →
2094  RTLabs_classify (Ras_state … s) = cl_other.
2095#ge * * [ #f #fs #m #S #M | #vf #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
2096#CS lapply (proj2 … (RTLabs_costed …) … CS)
2097whd in ⊢ (??%? → %);
2098[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
2099  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
2100| *: #E destruct
2101] qed.
2102
2103lemma eq_pc_cost : ∀ge,s1,s2.
2104  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2105  as_costed (RTLabs_status ge) s1 →
2106  as_costed (RTLabs_status ge) s2.
2107#ge
2108* * [ * #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 ]
2109[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
2110* * [ * #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 ]
2111whd in ⊢ (??%% → ?); #E destruct
2112#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
2113cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
2114qed.
2115
2116lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal.
2117  RTLabs_classify (Ras_state … s1) = cl_other →
2118  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal.
2119#ge #flX #s1X #s2X *
2120[ #s1 #s2 #EX *
2121  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
2122  | #CL #CS #CL' @eq_true_to_b @memb_hd
2123  ]
2124| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
2125| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL' in CL; #CL destruct
2126| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
2127| #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
2128| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
2129] qed.
2130
2131lemma state_fn_after_return : ∀ge,pre,post,CL.
2132  as_after_return (RTLabs_status ge) «pre,CL» post →
2133  state_fn … pre = state_fn … post.
2134#ge * #pre #preS #preM * #post #postS #postM #CL #AF
2135cases (rtlabs_call_inv … (simplify_cl … CL)) #vf * #fd * #args * #dst * #fs * #m #E destruct
2136cases post in postM AF ⊢ %;
2137[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
2138  cases preS in preM AF ⊢ %; [*]
2139  #fn *
2140  [ cases fs [ #M * ]
2141    #f #fs' * #FFP *
2142  | #fn' #S cases fs [ #M * ]
2143    #f #fs' #M * * #N #F #PC destruct %
2144  ]
2145| #A #B #C #D #E #F #G *
2146| #A #B #C #D #E *
2147| #r #M' #AF whd in AF; destruct
2148  cases preS in preM ⊢ %;
2149  [ // | #fn * [ // | #fn' #S * #FFP * ] ]
2150] qed.
2151
2152lemma state_fn_other : ∀ge,s1,s2.
2153  RTLabs_classify (Ras_state … s1) = cl_other →
2154  as_execute (RTLabs_status ge) s1 s2 →
2155  RTLabs_classify (Ras_state … s2) = cl_return ∨
2156  state_fn … s1 = state_fn … s2.
2157#ge #s1 #s2 #CL #EX
2158cases (declassify_state … EX CL)
2159#f * #fs * #m * * [**] #fn #S * #M #E destruct
2160inversion (eval_preserves_ext … EX)
2161[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
2162| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct %2 %
2163| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2164| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
2165| #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
2166| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
2167] qed.
2168
2169(* The main part of the proof is to walk down the trace_any_label and find the
2170   repeated call state, then show that its successor appears as well. *)
2171
2172let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
2173  (AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2)
2174  (CL2:RTLabs_classify (Ras_state … s2) = cl_other)
2175  (CS2:Not (as_costed (RTLabs_status ge) s2))
2176  (EX1:as_execute (RTLabs_status ge) s1 s1') on tal :
2177  state_fn … s1 = state_fn … s3 →
2178  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal →
2179  as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?.
2180cases tal
2181[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
2182  whd in match (tal_pc_list ?????) in IN;
2183  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2184  cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l
2185  #IN' destruct
2186| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
2187  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2188  @(declassify_pc_cl … EX2 CL2) whd #fn
2189  #IN' destruct
2190| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
2191  lapply (memb_single … IN) #E
2192  lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
2193  @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
2194| #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL)
2195| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
2196  whd in ⊢ (?% → ?); @eqb_elim
2197  [ #PC #_
2198    >(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list
2199    <(classify_after_return_eq … AF1 AF3 PC FN) assumption
2200  | #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons
2201    @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN)
2202    >FN @(state_fn_after_return … AF3)
2203  ]
2204| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
2205  lapply (simplify_cl … CL1) #CL1'
2206  lapply (simplify_cl … CL3) #CL3'
2207  @eq_true_to_b @memb_cons
2208  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
2209  [ >FN cases (state_fn_other … CL3' EX3)
2210    [ #CL3'' @⊥
2211      cases (tal_return … (CL3'') tal3')
2212      #EX3' * #CL3''' * #E1 #E2 destruct
2213      whd in IN:(?%); lapply IN @eqb_elim
2214      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2215      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct
2216      ]
2217    | //
2218    ]
2219  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2220    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2221    | #NE #IN @IN
2222    ]
2223  ]
2224] qed.
2225
2226(* Then we can start the proof by finding the original successor state... *)
2227
2228lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
2229  as_execute (RTLabs_status ge) s1 s1' →
2230  as_after_return (RTLabs_status ge) «s1,CL» s2 →
2231  ¬as_costed (RTLabs_status ge) s2 →
2232  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal →
2233  ∃s3,EX,CL',CS,tal'.
2234    tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
2235    bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
2236#ge #s1 #s1' #CL #flX #s2X #s4X *
2237[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
2238  whd in match (tal_pc_list ?????) in IN;
2239  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2240  cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l
2241  #IN' destruct
2242| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
2243  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2244  @(declassify_pc_cl … EX2 CL2) whd #fn
2245  #IN' destruct
2246| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
2247  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2248  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2249  cases AF1
2250| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
2251| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
2252  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2253  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2254  cases AF1
2255| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
2256  lapply (simplify_cl … CL) #CL'
2257  lapply (simplify_cl … CL2) #CL2'
2258  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
2259  (* Now that we've inverted the first part of the trace, look for the repeat. *)
2260  @(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1)
2261  [ >(state_fn_after_return … AF1)
2262    cases (state_fn_other … CL2' EX2)
2263    [ #CL3 @⊥
2264      cases (tal_return … (CL3) tal3)
2265      #EX3 * #CL3' * #E1 #E2 destruct
2266      lapply (simplify_cl … CL3') #CL3''
2267      whd in IN:(?%); lapply IN @eqb_elim
2268      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2269      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct
2270      ]
2271    | //
2272    ]
2273  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2274    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2275    | #NE #IN @IN
2276    ]
2277  ]
2278] qed.
2279
2280(* And then we get our counterpart to no_loops_in_tal for calls: *)
2281
2282lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
2283  ∀tal:trace_any_label (RTLabs_status ge) fl after final.
2284  as_execute (RTLabs_status ge) pre start →
2285  as_after_return (RTLabs_status ge) «pre,CL» after →
2286  ¬as_costed (RTLabs_status ge) after →
2287  soundly_labelled_state (Ras_state ge after) →
2288  ¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal.
2289#ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN
2290cases (pc_after_call_repeats … EX AF CS IN)
2291#s * #EX * #CL' * #CSx * #tal' * #E #IN'
2292@(absurd ? IN')
2293@Prop_notb
2294@no_loops_in_tal /2/
2295qed.
2296
2297(* Show that if a state is soundly labelled, then so are the states following
2298   it in a trace. *)
2299
2300lemma soundly_step : ∀ge,s1,s2.
2301  soundly_labelled_ge ge →
2302  as_execute (RTLabs_status ge) s1 s2 →
2303  soundly_labelled_state (Ras_state … s1) →
2304  soundly_labelled_state (Ras_state … s2).
2305#ge #s1 #s2 #GE * #tr * #EX #NX
2306@(soundly_labelled_state_step … GE … EX)
2307qed.
2308
2309let rec tlr_sound ge s1 s2
2310  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
2311  (GE:soundly_labelled_ge ge)
2312on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2313match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with
2314[ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1
2315| tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in
2316                            tlr_sound … tlr' GE S2
2317]
2318and tll_sound ge fl s1 s2
2319  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2320  (GE:soundly_labelled_ge ge)
2321on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2322match tll with
2323[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
2324]
2325and tal_sound ge fl s1 s2
2326  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2327  (GE:soundly_labelled_ge ge)
2328on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2329match tal with
2330[ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1
2331| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
2332| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
2333| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2334| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
2335| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
2336].
2337@(RTLabs_notail' … CL)
2338qed.
2339
2340(* And join everything up to show that soundly labelled states give unrepeating
2341   traces. *)
2342
2343let rec tlr_sound_unrepeating ge
2344  (s1,s2:RTLabs_status ge)
2345  (GE:soundly_labelled_ge ge)
2346  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
2347on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝
2348match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with
2349[ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1
2350| tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1))
2351]
2352and tll_sound_unrepeating ge fl
2353  (s1,s2:RTLabs_status ge)
2354  (GE:soundly_labelled_ge ge)
2355  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2356on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
2357match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with
2358[ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal
2359]
2360and tal_sound_unrepeating ge fl
2361  (s1,s2:RTLabs_status ge)
2362  (GE:soundly_labelled_ge ge)
2363  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2364on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
2365match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with
2366[ tal_base_not_return _ _ EX _ _ ⇒ λS1. I
2367| tal_base_return _ _ EX _ ⇒ λS1. I
2368| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
2369    tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
2370| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2371| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
2372    conj ?? (conj ???
2373     (tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1))))
2374     (tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1))
2375| tal_step_default _ pre init end EX tal CL _ ⇒ λS1.
2376    conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
2377].
2378[ @(RTLabs_notail' … CL)
2379| @(no_repeats_of_calls … EX AF) [ assumption |
2380  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
2381| @no_loops_in_tal // @simplify_cl @CL
2382] qed.
Note: See TracBrowser for help on using the repository browser.