source: src/RTLabs/RTLabs_traces.ma @ 2895

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

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

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