source: src/RTLabs/RTLabs_partial_traces.ma @ 2897

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

Minor tidying.

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