source: src/RTLabs/RTLabs_partial_traces.ma @ 2840

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

Remove irrelevant stuff from RTLabs_partial_traces

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