source: src/RTLabs/RTLabs_traces.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 125.9 KB
Line 
1
2include "RTLabs/RTLabs_abstract.ma".
3include "RTLabs/CostSpec.ma".
4include "RTLabs/CostMisc.ma".
5include "common/Executions.ma".
6include "utilities/listb.ma".
7
8
9(* Allow us to move between the different notions of when a state is cost
10   labelled. *)
11
12lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge.
13  RTLabs_cost s = true ↔
14  as_costed (RTLabs_status ge) s.
15cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
16#ge * *
17[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
18  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
19  whd in match (as_pc_of ??);
20  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
21  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
22  whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?);
23  >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?)));
24  % cases (lookup_present ?? (f_graph func) ??) normalize
25  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
26  try (% #E' destruct)
27  cases (NONE ?) assumption
28| #fd #args #dst #fs #m #stk #mtc %
29  [ #E normalize in E; destruct
30  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
31    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
32    #H cases (NONE H)
33  ]
34| #v #dst #fs #m #stk #mtc %
35  [ #E normalize in E; destruct
36  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
37    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
38    #H cases (NONE H)
39  ]
40| #r #stk #mtc %
41  [ #E normalize in E; destruct
42  | #E normalize in E; cases (NONE E)
43  ]
44] qed.
45
46lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge.
47  RTLabs_cost s = false →
48  ¬ as_costed (RTLabs_status ge) s.
49#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
50qed.
51
52(* Before attempting to construct a structured trace, let's show that we can
53   form flat traces with evidence that they were constructed from an execution.
54   As with the structured traces, we only consider good traces (i.e., ones
55   which don't go wrong).
56   
57   For now we don't consider I/O. *)
58
59
60coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
61| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
62| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
63| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
64
65(* add I/O? *)
66coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
67| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
68| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s.
69
70let corec make_flat_trace ge s
71  (NF:RTLabs_is_final s = None ?)
72  (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s)))
73  (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
74  flat_trace io_out io_in ge s ≝
75let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
76match e return λx. e = x → ? with
77[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
78| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???)
79| e_wrong m ⇒ λE. ⊥
80| e_interact o f ⇒ λE. ⊥
81] (refl ? e).
82[ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E;
83  cases (eval_statement ge s)
84  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
85  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
86    >(?:is_final ????? = RTLabs_is_final s1) //
87    lapply (refl ? (RTLabs_is_final s1))
88    cases (RTLabs_is_final s1) in ⊢ (???% → %);
89    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
90    | #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
91    | #i #E whd in ⊢ (??%? → ?); #E2 destruct
92    ]
93  | *: #m whd in ⊢ (??%? → ?); #E destruct
94  ]
95| whd in E:(??%?); >exec_inf_aux_unfold in E;
96  cases (eval_statement ge s)
97  [ #o #K whd in ⊢ (??%? → ?); #E destruct
98  | * #tr #s1 whd in ⊢ (??%? → ?);
99    lapply (refl ? (RTLabs_is_final s1))
100    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
101    cases (RTLabs_is_final s1) in ⊢ (???% → %);
102    [ #F #E whd in E:(??%?); destruct
103    | #r #F #E whd in E:(??%?); destruct >F % #E destruct
104    ]
105  | #m #E whd in E:(??%?); destruct
106  ]
107| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
108  cases (eval_statement ge s)
109  [ #O #K whd in ⊢ (??%? → ?); #E destruct
110  | * #tr #s1 whd in ⊢ (??%? → ?);
111    cases (is_final ?????)
112    [ whd in ⊢ (??%? → ?); #E
113      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
114      destruct
115      inversion H
116      [ #a #b #c #E1 destruct
117      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
118      | #m #E1 destruct
119      ]
120    | #i whd in ⊢ (??%? → ?); #E destruct
121    ]
122  | #m whd in ⊢ (??%? → ?); #E destruct
123  ]
124| whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E;
125  cases (eval_statement ge s)
126  [ #O #K whd in ⊢ (??%? → ?); #E destruct
127  | * #tr #s1 whd in ⊢ (??%? → ?);
128    cases (is_final ?????)
129    [ whd in ⊢ (??%? → ?); #E
130      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
131      destruct
132      inversion NW
133      [ #a #b #c #E1 #_ destruct
134      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
135      | #o #k #K #E1 destruct
136      ]
137    | #i whd in ⊢ (??%? → ?); #E destruct
138    ]
139  | #m whd in ⊢ (??%? → ?); #E destruct
140  ]
141| whd in E:(??%?); >exec_inf_aux_unfold in E;
142  cases (eval_statement ge s)
143  [ #o #K whd in ⊢ (??%? → ?); #E destruct
144  | * #tr #s1 whd in ⊢ (??%? → ?);
145    lapply (refl ? (RTLabs_is_final s1))
146    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
147    cases (RTLabs_is_final s1) in ⊢ (???% → %);
148    [ #F #E whd in E:(??%?); destruct @F
149    | #r #F #E whd in E:(??%?); destruct
150    ]
151  | #m #E whd in E:(??%?); destruct
152  ]
153| whd in E:(??%?); >E in NW; #X inversion X
154  #A #B #C #D #E destruct
155| whd in E:(??%?); >E in H; #H inversion H
156  #A #B #C try #D try #E destruct
157] qed.
158
159definition make_whole_flat_trace : ∀p,s.
160  exec_no_io … (exec_inf … RTLabs_fullexec p) →
161  not_wrong … (exec_inf … RTLabs_fullexec p) →
162  make_initial_state ??? p = OK ? s →
163  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
164λp,s,H,NW,I.
165let ge ≝ make_global … p in
166let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
167match e return λx. e = x → ? with
168[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
169| e_step _ _ e' ⇒ λE. make_flat_trace ge s ???
170| e_wrong m ⇒ λE. ⊥
171| e_interact o f ⇒ λE. ⊥
172] (refl ? e).
173[ whd in E:(??%?); >exec_inf_aux_unfold in E;
174  whd in ⊢ (??%? → ?);
175  change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
176  cases (RTLabs_is_final s)
177  [ #E whd in E:(??%?); destruct
178  | #r #E % #E' destruct
179  ]
180| @(initial_state_is_not_final … I)
181| whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?);
182  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????)
183  [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H
184    [ #a #b #c #E1 destruct
185    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
186      @H1
187    | #o #k #K #E1 destruct
188    ]
189  | #i whd in ⊢ (??%? → ??% → ?); #E destruct
190  ]
191| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
192  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
193  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
194    [ #a #b #c #E1 destruct
195    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
196      @H1
197    | #m #E1 destruct
198    ]
199  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
200  ]
201| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
202  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
203| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
204  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
205] qed.
206
207(* Need a way to choose whether a called function terminates.  Then,
208     if the initial function terminates we generate a purely inductive structured trace,
209     otherwise we start generating the coinductive one, and on every function call
210       use the choice method again to decide whether to step over or keep going.
211
212Not quite what we need - have to decide on seeing each label whether we will see
213another or hit a non-terminating call?
214
215Also - need the notion of well-labelled in order to break loops.
216
217
218
219outline:
220
221 does function terminate?
222 - yes, get (bound on the number of steps until return), generate finite
223        structure using bound as termination witness
224 - no,  get (¬ bound on steps to return), start building infinite trace out of
225        finite steps.  At calls, check for termination, generate appr. form.
226
227generating the finite parts:
228
229We start with the status after the call has been executed; well-labelling tells
230us that this is a labelled state.  Now we want to generate a trace_label_return
231and also return the remainder of the flat trace.
232
233*)
234
235(* [will_return ge depth s trace] says that after a finite number of steps of
236   [trace] from [s] we reach the return state for the current function.  [depth]
237   performs the call/return counting necessary for handling deeper function
238   calls.  It should be zero at the top level. *)
239inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
240| wr_step : ∀s,tr,s',depth,EX,trace.
241    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
242    will_return ge depth s' trace →
243    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
244| wr_call : ∀s,tr,s',depth,EX,trace.
245    RTLabs_classify s = cl_call →
246    will_return ge (S depth) s' trace →
247    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
248| wr_ret : ∀s,tr,s',depth,EX,trace.
249    RTLabs_classify s = cl_return →
250    will_return ge depth s' trace →
251    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
252    (* Note that we require the ability to make a step after the return (this
253       corresponds to somewhere that will be guaranteed to be a label at the
254       end of the compilation chain). *)
255| wr_base : ∀s,tr,s',EX,trace.
256    RTLabs_classify s = cl_return →
257    will_return ge O s (ft_step ?? ge s tr s' EX trace)
258.
259
260(* The way we will use [will_return] won't satisfy Matita's guardedness check,
261   so we will measure the length of these termination proofs and use an upper
262   bound to show termination of the finite structured trace construction
263   functions. *)
264
265let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
266match T with
267[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
268| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
269| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
270| wr_base _ _ _ _ _ _ ⇒ S O
271].
272
273include alias "arithmetics/nat.ma".
274
275(* Specialised to the particular situation it is used in. *)
276lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
277#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
278whd in ⊢ (??(??%) → ?);
279>commutative_times
280#H lapply (le_plus_b … H)
281#H lapply (le_to_leb_true … H)
282normalize #E destruct
283qed.
284   
285let 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' ≝
286match T with
287[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
288| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
289| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
290| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
291].
292
293(* Inversion lemmas on [will_return] that also note the effect on the length
294   of the proof. *)
295lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
296  RTLabs_classify s = cl_call →
297  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
298  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
299#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
300[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
301| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
302| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
303| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
304] qed.
305
306lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
307  RTLabs_classify s = cl_return →
308  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
309  match d with
310  [ O ⇒ will_return_end … TM = ❬s', trace❭
311  | S d' ⇒
312      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
313  ].
314#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
315[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
316| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
317| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
318| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
319] qed.
320
321lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
322  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
323  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
324  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
325#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
326[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
327| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
328| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
329| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
330| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
331| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
332| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
333| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
334] qed.
335
336(* When it comes to building bits of nonterminating executions we'll need to be
337   able to glue termination proofs together. *)
338
339lemma will_return_prepend : ∀ge,d1,s1,t1.
340  ∀T1:will_return ge d1 s1 t1.
341  ∀d2,s2,t2.
342  will_return ge d2 s2 t2 →
343  will_return_end … T1 = ❬s2, t2❭ →
344  will_return ge (d1 + S d2) s1 t1.
345#ge #d1 #s1 #tr1 #T1 elim T1
346[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
347  %1 // @(IH … T2) @E
348| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
349| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
350| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
351] qed.
352
353discriminator nat.
354
355lemma will_return_remove_call : ∀ge,d1,s1,t1.
356  ∀T1:will_return ge d1 s1 t1.
357  ∀d2.
358  will_return ge (d1 + S d2) s1 t1 →
359  ∀s2,t2.
360  will_return_end … T1 = ❬s2, t2❭ →
361  will_return ge d2 s2 t2.
362(* The key part of the proof is to show that the two termination proofs follow
363   the same pattern. *)
364#ge #d1x #s1x #t1x #T1 elim T1
365[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
366  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
367                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
368                   >H21 in CL; * #E destruct
369                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
370                   >H35 in CL; * #E destruct
371                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
372                   >H48 in CL; * #E destruct
373                 ]
374  | @E
375  ]
376| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
377  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
378                   >CL in H7; * #E destruct
379                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
380                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
381                   >H35 in CL; #E destruct
382                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
383                   >H48 in CL; #E destruct
384                 ]
385  | @E
386  ]
387| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
388  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
389                   >CL in H7; * #E destruct
390                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
391                   >H21 in CL; #E destruct
392                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
393                   whd in H38:(??%??); destruct //
394                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
395                   whd in H49:(??%??); @⊥ destruct
396                 ]
397  | @E
398  ]
399| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
400  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
401                 >CL in H7; * #E destruct
402               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
403                 >H21 in CL; #E destruct
404               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
405                 whd in H38:(??%??); destruct //
406               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
407                 whd in H49:(??%??); @⊥ destruct
408               ]
409] qed.
410
411
412
413lemma will_return_lower : ∀ge,d,s,t.
414  will_return ge d s t →
415  ∀d'. d' ≤ d →
416  will_return ge d' s t.
417#ge #d0 #s0 #t0 #TM elim TM
418[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
419| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
420| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
421  [ #LE @wr_base //
422  | #d' #LE %3 // @IH /2/
423  ]
424| #s #tr #s' #EX #tr #CL *
425  [ #_ @wr_base //
426  | #d' #LE @⊥ /2/
427  ]
428] qed.
429
430(* We need to ensure that any code we come across is well-cost-labelled.  We may
431   get function code from either the global environment or the state. *)
432
433definition well_cost_labelled_ge : genv → Prop ≝
434λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
435
436definition well_cost_labelled_state : state → Prop ≝
437λs. match s with
438[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
439| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
440                          All ? (λf. well_cost_labelled_fn (func f)) fs
441| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
442| Finalstate _ ⇒ True
443].
444
445lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
446  eval_statement ge s = Value ??? 〈tr,s'〉 →
447  well_cost_labelled_ge ge →
448  well_cost_labelled_state s →
449  well_cost_labelled_state s'.
450#ge #s #tr' #s' #EV cases (eval_preserves … EV)
451[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
452| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
453(*
454| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
455*)
456| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
457| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
458| #ge #f #fs #rtv #dst #f' #m #N * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
459| //
460] qed.
461
462lemma rtlabs_jump_inv : ∀s.
463  RTLabs_classify s = cl_jump →
464  ∃f,fs,m. s = State f fs m ∧
465  (∃r,l1,l2. next_instruction f = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*).
466*
467[ #f #fs #m #E
468  %{f} %{fs} %{m} %
469  [ @refl
470  | whd in E:(??%?); cases (next_instruction f) in E ⊢ %;
471    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
472    (*[ %1*) %{A} %{B} %{C} @refl
473(*    | %2 %{A} %{B} @refl
474    ]*)
475  ]
476| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
477| normalize #H8 #H9 #H10 #H11 #H12 destruct
478| #r #E normalize in E; destruct
479] qed.
480
481lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
482  eval_statement ge s = Value ??? 〈tr,s'〉 →
483  well_cost_labelled_state s →
484  RTLabs_classify s = cl_jump →
485  RTLabs_cost s' = true.
486#ge #s #tr #s' #EV #H #CL
487cases (rtlabs_jump_inv s CL)
488#fr * #fs * #m * #Es(* *
489[*) * #r * #l1 * #l2 #Estmt
490  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
491  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
492  >Estmt #LP whd in ⊢ (??%? → ?);
493  (* replace with lemma on successors? *)
494  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
495  lapply (Hbody (next fr) (next_ok fr))
496  generalize in ⊢ (?(???%) → ?);
497  change with (next_instruction fr) in match (lookup_present ?????);
498  >Estmt #LP' #WS
499  cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
500(*| * #r * #ls #Estmt
501  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
502  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
503  >Estmt #LP whd in ⊢ (??%? → ?);
504  (* replace with lemma on successors? *)
505  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
506  [ 2: (* later *)
507  | *: #E destruct
508  ]
509  lapply (Hbody (next fr) (next_ok fr))
510  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
511  generalize in ⊢ (??(?%)? → ?);
512  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
513  [ #E1 #E2 whd in E2:(??%?); destruct
514  | #l' #E1 #E2 whd in E2:(??%?); destruct
515    cases (All_nth ???? CP ? E1)
516    #H1 #H2 @H2
517  ]
518]*) qed.
519
520lemma rtlabs_call_inv : ∀s.
521  RTLabs_classify s = cl_call →
522  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
523* [ #f #fs #m whd in ⊢ (??%? → ?);
524    cases (next_instruction f) normalize
525    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
526  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
527  | normalize #H411 #H412 #H413 #H414 #H415 destruct
528  | normalize #H1 #H2 destruct
529  ] qed.
530
531lemma well_cost_labelled_call : ∀ge,s,tr,s'.
532  eval_statement ge s = Value ??? 〈tr,s'〉 →
533  well_cost_labelled_state s →
534  RTLabs_classify s = cl_call →
535  RTLabs_cost s' = true.
536#ge #s #tr #s' #EV #WCL #CL
537cases (rtlabs_call_inv s CL)
538#fd * #args * #dst * #stk * #m #E >E in EV WCL;
539whd in ⊢ (??%? → % → ?);
540cases fd
541[ #fn whd in ⊢ (??%? → % → ?);
542  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
543  #m' #b whd in ⊢ (??%? → ?); #E' destruct
544  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
545  @WCL2
546| #fn whd in ⊢ (??%? → % → ?);
547  @bindIO_value #evargs #Eargs
548  whd in ⊢ (??%? → ?);
549  #E' destruct
550] qed.
551
552
553(* Extend our information about steps to states extended with the shadow stack. *)
554
555inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
556| 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')
557| xto_call : ∀ge,f,fs,m,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 fd args dst (f'::fs) m) (fn::S) M')
558| xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate (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')
559| 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')
560| 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')
561| 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')
562.
563
564lemma eval_preserves_ext : ∀ge,s,s'.
565  as_execute (RTLabs_status ge) s s' →
566  state_rel_ext ge s s'.
567#ge0 * #s #S #M * #s' #S' #M' * #tr * #EX
568generalize in match M'; -M'
569generalize in match M; -M
570generalize in match EX;
571inversion (eval_preserves … EX)
572[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct
573  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
574  %1 //
575| #ge #f #fs #m #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
576  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
577  %2 //
578| #ge #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
579  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
580  %3
581| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
582  cases S [ #EX' * ] #fn #S
583  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
584  %4
585| #ge #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
586  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
587  %5 //
588| #ge #r #dst #m #E1 #E2 #E3 #E4 destruct
589  cases S [ 2: #h #t #EX' * ]
590  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
591  %6
592] qed.
593
594
595
596(* The preservation of (most of) the stack is useful to show as_after_return.
597   We do this by showing that during the execution of a function the lower stack
598   frames never change, and that after returning from the function we preserve
599   the identity of the next instruction to execute.
600   
601   We also show preservation of the shadow stack of function pointers.  As with
602   the real stack, we ignore the current function.
603 *)
604
605inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
606| 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)
607| sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
608| 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)
609.
610
611inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
612| sp_normal : ∀fs,S,s1,s2.
613    stack_of_state ge fs S s1 →
614    stack_of_state ge fs S s2 →
615    stack_preserved ge doesnt_end_with_ret s1 s2
616| sp_finished : ∀s1,f,f',fs,m,fn,S,M.
617    next f = next f' →
618    frame_rel f f' →
619    stack_of_state ge (f::fs) (fn::S) s1 →
620    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M)
621| sp_stop : ∀s1,r,M.
622    stack_of_state ge [ ] [ ] s1 →
623    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
624| sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
625    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
626.
627
628discriminator list.
629
630lemma stack_of_state_eq : ∀ge,fs,fs',S,S',s.
631  stack_of_state ge fs S s →
632  stack_of_state ge fs' S' s →
633  fs = fs' ∧ S = S'.
634#ge #fs0 #fs0' #S0 #S0' #s0 *
635[ #f #fs #m #fn #S #M #H inversion H
636  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
637| #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
638  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o destruct /2/
639| #rtv #dst #fs #m #S #M #H inversion H
640  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
641] qed.
642
643lemma stack_preserved_final : ∀ge,e,r,S,M,s.
644  ¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s.
645#ge #e #r #S #M #s % #H inversion H
646[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
647  inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m destruct
648| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
649  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m destruct
650| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
651  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o destruct
652| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
653] qed.
654
655lemma stack_preserved_join : ∀ge,e,s1,s2,s3.
656  stack_preserved ge doesnt_end_with_ret s1 s2 →
657  stack_preserved ge e s2 s3 →
658  stack_preserved ge e s1 s3.
659#ge #e1 #s1 #s2 #s3 #H1 inversion H1
660[ #fs #S #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
661  #H2 inversion H2
662  [ #fs' #S' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
663    @(sp_normal ge fs S) // cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
664  | #s1'' #f #f' #fs' #m #fn #S' #M #N #F #S1' #E1 #E2 #E3 #E4 destruct
665    @(sp_finished … fn … N) cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
666  | #s1'' #r #M #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop cases (stack_of_state_eq … S1'' S2) #E1 #E2 destruct //
667  | #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
668    inversion S2
669    [ #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
670    | #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
671    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
672    ]
673  ]
674| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
675| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
676| #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
677  @(absurd … F) //
678] qed.
679
680(* Proof that steps preserve the stack.  For calls we show that a stack
681   preservation proof for the called function gives us enough to show
682   stack preservation for the caller between the call and the state after
683   returning. *)
684
685lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl.
686  RTLabs_classify s1 = cl →
687  as_execute (RTLabs_status ge) s1 s2 →
688  match cl with
689  [ cl_call ⇒ ∀s3. stack_preserved ge ends_with_ret s2 s3 →
690                   stack_preserved ge doesnt_end_with_ret s1 s3
691  | cl_return ⇒ stack_preserved ge ends_with_ret s1 s2
692  | _ ⇒ stack_preserved ge doesnt_end_with_ret s1 s2
693  ].
694#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
695[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
696  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
697| #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
698  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
699| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
700  * #s3 #S3 #M3 #SP inversion SP
701  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
702  | #s1 #f #f' #fs' #m3 #fn3 #S3' #M3' #E1 #E2 #SOS #E4 #E5 #E6 #E7 destruct
703    @(sp_normal … fs' S3') //
704    inversion SOS
705    [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct //
706    | #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
707    | #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
708    ]
709  | #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
710    cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 destruct /3/ ]
711    * #fn * #E1 #E2 destruct
712    @sp_top
713  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
714  ]
715| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
716  whd in match (RTLabs_classify ?); cases (next_instruction f) /2/
717| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
718  cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
719| #ge #r #dst #m #M #M' #E1 #E2 #E3 #E4 destruct whd /2/
720] qed.
721
722lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr.
723  ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
724  as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
725#ge #s1 #s2 #tr #EV %{tr} %{EV} %
726qed.
727
728definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E.
729
730lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge.
731  ∀CL : RTLabs_classify s1 = cl_call.
732  as_execute (RTLabs_status ge) s1 s2 →
733  stack_preserved ge ends_with_ret s2 s3 →
734  as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
735#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
736cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
737whd
738inversion S23
739[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
740| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
741  inversion (eval_preserves_ext … EV)
742  [ 3: #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
743    inversion S
744    [ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N | inversion F // ] | whd % ]
745    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 destruct
746    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
747    ]
748  | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 destruct
749  ]
750| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
751  inversion (eval_preserves_ext … EV)
752  [ 3: #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
753    inversion S1
754    [ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
755    | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 destruct
756    ]
757  | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 destruct
758  ]
759| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
760] qed.
761
762(* Don't need to know that labels break loops because we have termination. *)
763
764(* A bit of mucking around with the depth to avoid proving termination after
765   termination.  Note that we keep a proof that our upper bound on the length
766   of the termination proof is respected. *)
767record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
768  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
769  (original_terminates: will_return ge depth start full)
770  (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
771{
772  new_state : RTLabs_ext_state ge;
773  remainder : flat_trace io_out io_in ge new_state;
774  cost_labelled : well_cost_labelled_state new_state;
775  new_trace : T new_state;
776  stack_ok : stack_preserved ge ends start new_state;
777  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
778               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
779               | S d ⇒ ΣTM:will_return ge d new_state remainder.
780                         gt limit (will_return_length … TM) ∧
781                         will_return_end … original_terminates = will_return_end … TM
782               ]
783}.
784
785(* The same with a flag indicating whether the function returned, as opposed to
786   encountering a label. *)
787record sub_trace_result (ge:genv) (depth:nat)
788  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
789  (original_terminates: will_return ge depth start full)
790  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
791{
792  ends : trace_ends_with_ret;
793  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
794}.
795
796(* We often return the result from a recursive call with an addition to the
797   structured trace, so we define a couple of functions to help.  The bound on
798   the size of the termination proof might need to be relaxed, too. *)
799
800definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
801  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
802    will_return_end … TM1 = will_return_end … TM2 →
803    T2 (new_state … r) →
804    stack_preserved ge e s2 (new_state … r) →
805    trace_result ge d e s2 t2 TM2 T2 l2 ≝
806λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
807  mk_trace_result ge d e s2 t2 TM2 T2 l2
808    (new_state … r)
809    (remainder … r)
810    (cost_labelled … r)
811    trace
812    SP
813    ?
814    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
815                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
816     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
817.
818cases e in r ⊢ %;
819[ <TME -TME * cases d in TM1 TM2 ⊢ %;
820  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
821  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
822    %{TMa} % // @(transitive_le … lGE) @L1
823  ]
824| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
825   * #TMa * #L1 #TME
826    %{TMa} % // @(transitive_le … lGE) @L1
827] qed.
828
829definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
830  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
831    will_return_end … TM1 = will_return_end … TM2 →
832    T2 (ends … r) (new_state … r) →
833    stack_preserved ge (ends … r) s2 (new_state … r) →
834    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
835λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
836  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
837    (ends … r)
838    (replace_trace … lGE … r TME trace SP).
839
840(* Small syntax hack to avoid ambiguous input problems. *)
841definition myge : nat → nat → Prop ≝ ge.
842
843(* RTLabs_classify isn't exactly as_classifier *)
844definition lift_cl ≝ eq_f ?? (Some status_class).
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                ? (lift_cl … 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') ? (lift_cl … 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' ? (lift_cl … 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 @(lift_cl … 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 @(lift_cl … 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| @(lift_cl … 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 : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate 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, lift_cl … 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  #fn * #args * #dst * #stk * #m' #E destruct
1281| #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  | #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 #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 #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 #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' #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  | #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 (lift_cl … 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 (lift_cl … 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, lift_cl … 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 (lift_cl … 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 (lift_cl … 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) ? (lift_cl … 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 … (lift_cl … 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 @(lift_cl … 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) #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 @⊥ -next destruct ]
1582        #ge' #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 [ whd in H5:(??%?%); | 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 destruct
1589      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 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 @(lift_cl … 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' #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 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 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) (lift_cl … IS_CALL) ? (new_trace … tlr) ?
1761        ]
1762    | or_intror NO_TERMINATION ⇒
1763        twp_diverges (RTLabs_status ge) s' next' (lift_cl … 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)) #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 fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
1788   | _ ⇒ False ].
1789#p #s
1790@bind_ok #m #Em
1791@bind_ok #b #Eb
1792@bind_ok #f #Ef
1793#E whd in E:(??%%); destruct
1794%{b} whd
1795% // @Ef
1796qed.
1797
1798definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝
1799λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?.
1800cases (init_state_is p s I) #b
1801cases s
1802[ #f #fs #m *
1803| #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
1804| #rv #rr #fs #m *
1805| #r *
1806] qed.
1807
1808lemma well_cost_labelled_initial : ∀p,s.
1809  make_initial_state p = OK ? s →
1810  well_cost_labelled_program p →
1811  well_cost_labelled_state s ∧ soundly_labelled_state s.
1812#p #s
1813@bind_ok #m #Em
1814@bind_ok #b #Eb
1815@bind_ok #f #Ef
1816#E destruct
1817whd in ⊢ (% → %);
1818#WCL
1819@(find_funct_ptr_All ??????? Ef)
1820@(All_mp … WCL)
1821* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
1822qed.
1823
1824lemma well_cost_labelled_make_global : ∀p.
1825  well_cost_labelled_program p →
1826  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
1827#p whd in ⊢ (% → ?%%);
1828#WCL %
1829#b #f #FFP
1830[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
1831| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
1832] @(All_mp … WCL)
1833* #id * #fn // * /2/
1834qed.
1835
1836theorem program_trace_exists :
1837  termination_oracle →
1838  ∀p:RTLabs_program.
1839  well_cost_labelled_program p →
1840  ∀s:state.
1841  ∀I: make_initial_state p = OK ? s.
1842 
1843  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1844 
1845  ∀NOIO:exec_no_io … plain_trace.
1846  ∀NW:not_wrong … plain_trace.
1847 
1848  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
1849 
1850  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
1851
1852#ORACLE #p #WCL #s #I
1853letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1854#NOIO #NW
1855letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
1856whd
1857@(whole_structured_trace_exists (make_global p) p ? ORACLE)
1858[ @(proj1 … (well_cost_labelled_make_global … WCL))
1859| @(proj2 … (well_cost_labelled_make_global … WCL))
1860| @flat_trace
1861| @I
1862| @(proj1 ?? (well_cost_labelled_initial … I WCL))
1863| @(proj2 ?? (well_cost_labelled_initial … I WCL))
1864] qed.
1865
1866
1867lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
1868  as_execute (RTLabs_status ge) s s' →
1869  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
1870#ge #s #s' * #tr * #EX #_ %{tr} @EX
1871qed.
1872
1873(* as_execute might be in Prop, but because the semantics is deterministic
1874   we can retrieve the event trace anyway. *)
1875
1876let rec deprop_execute ge (s,s':state)
1877  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
1878: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1879match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
1880[ Value ts ⇒ λY. «fst … ts, ?»
1881| _ ⇒ λY. ⊥
1882] X.
1883[ 1,3: cases Y #x #E destruct
1884| cases Y #trP #E destruct @refl
1885] qed.
1886
1887let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge)
1888  (X:as_execute (RTLabs_status ge) s s')
1889: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1890deprop_execute ge s s' ?.
1891cases X #tr * #EX #_ %{tr} @EX
1892qed.
1893
1894(* A non-empty finite section of a flat_trace *)
1895inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1896| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1897| 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''.
1898
1899let rec append_partial_flat_trace o i ge s1 s2 s3
1900  (tr1:partial_flat_trace o i ge s1 s2)
1901on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1902match tr1 with
1903[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1904| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1905].
1906
1907let rec partial_to_flat_trace o i ge s1 s2
1908  (tr:partial_flat_trace o i ge s1 s2)
1909on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1910match tr with
1911[ pft_base s tr s' EX ⇒ ft_step … EX
1912| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1913].
1914
1915(* Extract a flat trace from a structured one. *)
1916let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge)
1917  (tr:trace_label_return (RTLabs_status ge) s s')
1918on tr :
1919  partial_flat_trace io_out io_in ge s s' ≝
1920match tr with
1921[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
1922| tlr_step s1 s2 s3 tll tlr ⇒
1923  append_partial_flat_trace …
1924    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
1925    (flat_trace_of_label_return ge s2 s3 tlr)
1926]
1927and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge)
1928  (tr:trace_label_label (RTLabs_status ge) ends s s')
1929on tr :
1930  partial_flat_trace io_out io_in ge s s' ≝
1931match tr with
1932[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
1933]
1934and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge)
1935  (tr:trace_any_label (RTLabs_status ge) ends s s')
1936on tr :
1937  partial_flat_trace io_out io_in ge s s' ≝
1938match tr with
1939[ tal_base_not_return s1 s2 EX CL CS ⇒
1940    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1941    pft_base … EX' ]
1942| tal_base_return s1 s2 EX CL ⇒
1943    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1944    pft_base … EX' ]
1945| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
1946    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
1947    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1948    pft_step … EX' suffix' ]
1949| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
1950    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1951    pft_step … EX'
1952      (append_partial_flat_trace …
1953        (flat_trace_of_label_return ge ?? tlr)
1954        (flat_trace_of_any_label ge ??? tal))
1955    ]
1956| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
1957    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1958      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
1959    ]
1960| tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥
1961].
1962@(RTLabs_notail' … CL)
1963qed.
1964
1965(* We take an extra step so that we can always return a non-empty trace to
1966   satisfy the guardedness condition in the cofixpoint. *)
1967let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et
1968  (tr:trace_any_call (RTLabs_status ge) s s')
1969  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1970on tr :
1971  partial_flat_trace io_out io_in ge s s'' ≝
1972match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
1973[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
1974| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
1975    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
1976    pft_step … EX'
1977      (append_partial_flat_trace …
1978        (flat_trace_of_label_return ge ?? tlr)
1979        (flat_trace_of_any_call ge … tac EX''))
1980    ]
1981| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
1982    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1983    pft_step … EX'
1984     (flat_trace_of_any_call ge … tal EX'')
1985    ]
1986] EX''.
1987
1988let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et
1989  (tr:trace_label_call (RTLabs_status ge) s s')
1990  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
1991on tr :
1992  partial_flat_trace io_out io_in ge s s'' ≝
1993match tr with
1994[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
1995] EX''.
1996
1997(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
1998   to take care to satisfy the guardedness condition by witnessing the fact that
1999   the partial traces are non-empty. *)
2000let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)
2001  (tr:trace_label_diverges (RTLabs_status ge) s)
2002: flat_trace io_out io_in ge s ≝
2003match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
2004[ tld_step sx sy tll tld ⇒
2005  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 ⇒
2006    λtll.
2007    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
2008    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2009    | 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)
2010    ] mtc0 ] tll tld
2011| tld_base s1 s2 s3 tlc EX CL tld ⇒
2012  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 ⇒
2013    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2014      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
2015      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2016      | 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)
2017      ] mtc0
2018    ]
2019  ] EX tld
2020]
2021(* Helper to keep adding the partial trace without violating the guardedness
2022   condition. *)
2023and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge)
2024: partial_flat_trace io_out io_in ge s s' →
2025  trace_label_diverges (RTLabs_status ge) s' →
2026  flat_trace io_out io_in ge s ≝
2027match 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 ⇒
2028λ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
2029[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
2030| 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)
2031] mtc ]
2032.
2033
2034
2035coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2036| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2037| 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).
2038
2039let corec flat_traces_are_determined_by_starting_point ge s tr1
2040: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2041match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2042[ ft_stop s F ⇒ λtr2. ?
2043| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2044    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2045    [ ft_stop s F ⇒ λEX. ?
2046    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2047    ] EX0
2048].
2049[ inversion tr2 in tr1 F;
2050  [ #s #F #_ #_ #tr1 #F' @eft_stop
2051  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2052    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2053  ]
2054| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2055| -EX0
2056  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2057  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2058  -E -EX' -tr2' #tr2' #EX'
2059  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2060  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2061  -E -EX' #EX'
2062    @eft_step @flat_traces_are_determined_by_starting_point
2063] qed.
2064
2065let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
2066  (str:trace_label_diverges (RTLabs_status ge) s)
2067  (tr:flat_trace io_out io_in ge s)
2068: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
2069@flat_traces_are_determined_by_starting_point
2070qed.
2071
2072let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)
2073  (tr:trace_whole_program (RTLabs_status ge) s)
2074on tr : flat_trace io_out io_in ge s ≝
2075match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with
2076[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2077    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2078      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
2079    ]
2080| twp_diverges s1 s2 CL EX tld ⇒
2081    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2082      ft_step … EX' (flat_trace_of_label_diverges … tld)
2083    ]
2084].
2085
2086let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
2087  (str:trace_whole_program (RTLabs_status ge) s)
2088  (tr:flat_trace io_out io_in ge s)
2089: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
2090@flat_traces_are_determined_by_starting_point
2091qed.
2092
2093
2094
2095
2096
2097(* We still need to link tal_unrepeating to our definition of cost soundness. *)
2098
2099
2100(* Extract the "current" function from a state. *)
2101definition state_fn : ∀ge. RTLabs_status ge → option block ≝
2102λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
2103  match Ras_state … s with
2104  [ Callstate _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
2105  | _ ⇒  Some ? h ] ].
2106
2107(* Some results to invert the classification of states *)
2108
2109lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge.
2110  as_execute (RTLabs_status ge) s s' →
2111  RTLabs_classify s = cl →
2112  match cl with
2113  [ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
2114  | cl_return ⇒ ∀fn. P (rapc_ret fn)
2115  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
2116  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
2117  | cl_tailcall ⇒ True
2118  ] → P (as_pc_of (RTLabs_status ge) s).
2119#ge #cl #P * *
2120[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
2121  cases (next_instruction f) normalize
2122  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
2123| #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
2124| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
2125| #r #S #M #s' * #tr * #EX normalize in EX; destruct
2126] qed.
2127
2128definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL).
2129
2130lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
2131  as_execute (RTLabs_status ge) s s' →
2132  RTLabs_classify s = cl →
2133  match cl with
2134  [ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
2135  | cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
2136  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2137  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2138  | cl_tailcall ⇒ False
2139  ] .
2140#ge * #s #s' #EX #CL whd
2141@(declassify_pc … EX CL) whd
2142[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | @I | #fn #l %{fn} %{l} % ]
2143qed.
2144
2145lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge.
2146  as_execute (RTLabs_status ge) s s' →
2147  RTLabs_classify s = cl →
2148  match cl with
2149  [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate fd args dst fs m) S M
2150  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
2151  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
2152  ] .
2153#ge #cl * * [ #f #fs #m | #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
2154#S #M * #s' #S' #M' #EX #CL
2155whd in CL:(??%?);
2156[ cut (cl = cl_other ∨ cl = cl_jump)
2157  [ cases (next_instruction f) in CL;
2158    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
2159  * #E >E %{f} %{fs} %{m} %{S} %{M} %
2160| <CL %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
2161| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
2162| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
2163] qed.
2164
2165lemma State_not_callreturn : ∀f,fs,m,cl.
2166  RTLabs_classify (State f fs m) = cl →
2167  match cl with
2168  [ cl_return ⇒ False
2169  | cl_call ⇒ False
2170  | _ ⇒ True
2171  ].
2172#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
2173cases (next_instruction f) //
2174qed.
2175
2176(* And some about traces *)
2177
2178lemma tal_not_final : ∀ge,fl,s1,s2.
2179  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2180  RTLabs_is_final (Ras_state … s1) = None ?.
2181#ge #flx #s1x #s2x *
2182[ #s1 #s2 * #tr * #EX #NX #CL #CS
2183| #s1 #s2 * #tr * #EX #NX #CL
2184| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
2185| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
2186| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
2187| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
2188] @(step_not_final … EX)
2189qed.
2190
2191(* invert traces ending in a return *)
2192
2193lemma tal_return : ∀ge,fl,s1,s2.
2194  as_classifier (RTLabs_status ge) s1 cl_return →
2195  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2196  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
2197#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
2198[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
2199  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
2200| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
2201  %{EX} %{CL} % %
2202| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
2203  whd in CL CL'; >CL in CL'; #E destruct
2204| #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL')
2205| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
2206  whd in CL CL'; >CL in CL'; #E destruct
2207| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
2208  whd in CL CL'; >CL in CL'; #E destruct
2209] qed.
2210
2211
2212(* We need to link the pcs, states of the semantics with the labels and graphs
2213   of the syntax. *)
2214
2215inductive pc_label : RTLabs_pc → label → Prop ≝
2216| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
2217| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
2218
2219discriminator option.
2220
2221lemma pc_label_eq : ∀pc,l1,l2.
2222  pc_label pc l1 →
2223  pc_label pc l2 →
2224  l1 = l2.
2225#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
2226qed.
2227
2228lemma pc_label_call_eq : ∀l,fn,l'.
2229  pc_label (rapc_call (Some ? l) fn) l' →
2230  l = l'.
2231#l #fn #l' #PC inversion PC
2232#a #b #E1 #E2 #E3 destruct
2233%
2234qed.
2235
2236inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
2237| gf : ∀b,fn.
2238    find_funct_ptr … ge b = Some ? (Internal ? fn) →
2239    graph_fn ge (Some ? b) (f_graph … fn).
2240
2241lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
2242  graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g →
2243  g = f_graph (func f).
2244#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
2245inversion G
2246#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
2247%
2248qed.
2249
2250lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
2251  let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in
2252  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
2253  actual_successor s' = Some ? l →
2254  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
2255#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
2256change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
2257inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
2258[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2259| #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2260| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
2261| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
2262  >H33 in AS; normalize #AS destruct
2263| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2264| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
2265] qed.
2266
2267lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
2268  as_after_return (RTLabs_status ge) «pre,CL» post →
2269  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
2270  match ret with
2271  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
2272  | Some retl ⇒
2273    state_fn … pre = state_fn … post ∧
2274    pc_label (as_pc_of (RTLabs_status ge) post) retl
2275  ].
2276#ge #pre #post #CL #ret #callee #AF
2277cases pre in CL AF ⊢ %;
2278* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?);
2279    cases (next_instruction f) in CL;
2280    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
2281  | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
2282  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
2283  | #r #S #M #CL normalize in CL; destruct
2284  ]
2285cases post
2286* [ #postf #postfs #postm * [*] #fn' #S' #M'
2287  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
2288  | 2,6: #A #B #C #D #E #F #G *
2289  | 3,7: #A #B #C #D #E #F *
2290  | #r #S' #M' #AF whd in AF; destruct
2291  | #r #S' #M'
2292  ]
2293#AF #PC normalize in PC; destruct whd
2294[ cases AF * #A #B #C destruct % [ % | normalize >A // ]
2295| % #E normalize in E; destruct
2296] qed.
2297
2298lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l.
2299  actual_successor s = Some ? l →
2300  pc_label (as_pc_of (RTLabs_status ge) s) l.
2301#ge * *
2302[ #f #fs #m * [*] #fn #S #M #l #AS
2303| #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
2304| #ret #dst #fs #m #S #M #l #AS
2305| #r #S #M #l #AS
2306] whd in AS:(??%?); destruct //
2307qed.
2308
2309include alias "utilities/deqsets.ma".
2310
2311(* Build the tail of the "bad" loop using the reappearance of the original pc,
2312   ignoring the rest of the trace_any_label once we see that pc. *)
2313
2314let rec tal_pc_loop_tail ge flX s1X s2X
2315  (pc:as_pc (RTLabs_status ge)) g l
2316  (PC0:pc_label pc l)
2317  (tal: trace_any_label (RTLabs_status ge) flX s1X s2X)
2318on tal :
2319  ∀l1.
2320  pc_label (as_pc_of (RTLabs_status ge) s1X) l1 →
2321  graph_fn ge (state_fn … s1X) g →
2322  Not (as_costed (RTLabs_status ge) s1X) →
2323  pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal →
2324  bad_label_list g l l1 ≝ ?.
2325cases tal
2326[ #s1 #s2 #EX #CL #CS
2327  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2328  >(pc_label_eq … PC0 PC1) %1
2329| #s1 #s2 #EX #CL
2330  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2331  >(pc_label_eq … PC0 PC1) %1
2332| #pre #start #final #EX #CL #AF #tlr #CS
2333  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2334  >(pc_label_eq … PC0 PC1) %1
2335| #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL)
2336| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
2337  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2338  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2339  | #NE #IN
2340    lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
2341    [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
2342      lapply (pc_label_call_eq … PC1) #E destruct
2343      @(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN)
2344    | @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct
2345    ]
2346  ]
2347| #fl #pre #init #end #EX #tal' #CL #CS
2348  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2349  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2350  | #NE #IN
2351    cases (declassify_state … EX (simplify_cl … CL))
2352    #f * #fs * #m * #S * #M #E destruct
2353    cut (l1 = next f)
2354    [ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1
2355      inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct
2356    cases EX #tr * #EV #NX
2357    cases (eval_successor … EV)
2358    [ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct
2359      lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd
2360      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
2361    | * #l' * #AS #SC
2362      lapply (graph_fn_state … G) #E destruct
2363      @(gl_step … l')
2364      [ @(next_ok f)
2365      | @Exists_memb @SC
2366      | @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??))
2367        @ISL
2368      | @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS))
2369        [ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G
2370        | *: //
2371        ]
2372      ]
2373    ]
2374  ]
2375] qed.
2376
2377(* Combine the above result with the result on bad loops in CostMisc.ma to show
2378   that the pc of a normal instruction execution state can't be repeated within
2379   a trace_any_label. *)
2380
2381lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal.
2382  soundly_labelled_state s1 →
2383  RTLabs_classify s1 = cl_other →
2384  as_execute (RTLabs_status ge) s1 s2 →
2385  ¬ as_costed (RTLabs_status ge) s2 →
2386  ¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal.
2387#ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL)
2388#f * #fs * #m * * [* *] #fn #S * * #FFP #M #E destruct
2389cases EX #tr * #EV #NX
2390cases (eval_successor … EV)
2391[ * #CL2 #SC
2392  cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct
2393  @notb_Prop % whd in match (tal_pc_list ?????); #IN
2394  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
2395  #ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct
2396  normalize #E destruct
2397| * #l2 * #AS2 #SC1 @notb_Prop % #IN
2398  (* Two cases: either s1 is a cost label, and it's pc's appearence later on
2399     is impossible because nothing later in tal can be a cost label; or it
2400     isn't and we get a loop of successor instruction labels that breaks the
2401     soundness of the cost labelling. *)
2402  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
2403  [ * #H @H
2404    cases (memb_exists … IN) #left * #right #E
2405    @(All_split … (tal_tail_not_costed … tal CS2) … E)
2406  | (* Now show that the loop invalidates soundness. *)
2407    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))
2408    [ %1 ] #PC1
2409    cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
2410    [ /2/ ] #PC2
2411    lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN)
2412    [ <NX <(state_fn_next … EV AS2) % // ]
2413    cases S1 #SLF #_ cases (SLF (next f) (next_ok f))
2414    #bound1 #BOUND1 #BLL #CS1
2415    cases (bound_step1 … BOUND1 … SC1)
2416    #bound2 #BOUND2 @(absurd … BOUND2)
2417    @(loop_soundness_contradiction … BLL)
2418    [ @(next_ok f)
2419    | @SC1
2420    | @notb_Prop @(not_to_not … CS1) #CS
2421      @(proj1 … (RTLabs_costed …)) @CS
2422    ]
2423  ]
2424] qed.
2425
2426(* We need a similar result for call states.  We'll do this by showing that
2427   the state following the call state is a normal instruction state and using
2428   the previous result. *)
2429
2430lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2431  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2432  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2433  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2434  state_fn … s1 = state_fn … s2 →
2435  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
2436#ge * #s1 #S1 #M1 #CL1
2437cases (rtlabs_call_inv … (simplify_cl … CL1)) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
2438* #s2 #S2 #M2 #CL2
2439cases (rtlabs_call_inv … (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
2440* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
2441* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
2442whd in ⊢ (% → ?);
2443[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
2444    * * #N1 #F1 #STK1
2445    whd in STK1 ⊢ (% → ?);
2446    [ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [*] #fn2 * [* #X *] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2447      normalize in ⊢ (% → % → ?); #E1 #E2
2448      cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1
2449      cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2
2450      whd in ⊢ (??%%); <N2 <N1 destruct >e1 %
2451    | #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?);
2452      #X destruct
2453    ]
2454| #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M *] #f2 #fs2' cases S2 [*] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2455  cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1
2456  normalize in ⊢ (% → ?); #E destruct
2457| #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ %
2458] qed.
2459
2460lemma eq_pc_eq_classify : ∀ge,s1,s2.
2461  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2462  RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
2463#ge
2464* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
2465* * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 2,6,10,14: #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 ]
2466whd in ⊢ (??%% → ?); #E destruct try %
2467[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
2468  change with (lookup_present … next2 nok1) in match (next_instruction ?);
2469  cases (lookup_present … next2 nok1)
2470  normalize //
2471| 2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct
2472| 4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct
2473] qed.
2474
2475lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2476  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2477  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2478  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2479  state_fn … s1 = state_fn … s2 →
2480  RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4).
2481#ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN
2482@eq_pc_eq_classify
2483@(pc_after_return_eq … AF1 AF2 PC FN)
2484qed.
2485
2486lemma cost_labels_are_other : ∀ge,s.
2487  as_costed (RTLabs_status ge) s →
2488  RTLabs_classify (Ras_state … s) = cl_other.
2489#ge * * [ #f #fs #m #S #M | #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
2490#CS lapply (proj2 … (RTLabs_costed …) … CS)
2491whd in ⊢ (??%? → %);
2492[ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize
2493  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
2494| *: #E destruct
2495] qed.
2496
2497lemma eq_pc_cost : ∀ge,s1,s2.
2498  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2499  as_costed (RTLabs_status ge) s1 →
2500  as_costed (RTLabs_status ge) s2.
2501#ge
2502* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 #S1 #M1 ]
2503[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
2504* * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2 | 2,6,10,14: #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 ]
2505whd in ⊢ (??%% → ?); #E destruct
2506#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
2507cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
2508qed.
2509
2510lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal.
2511  RTLabs_classify (Ras_state … s1) = cl_other →
2512  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal.
2513#ge #flX #s1X #s2X *
2514[ #s1 #s2 #EX *
2515  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2516  | #CL #CS #CL' @eq_true_to_b @memb_hd
2517  ]
2518| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2519| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2520| #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL)
2521| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct
2522| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
2523] qed.
2524
2525lemma state_fn_after_return : ∀ge,pre,post,CL.
2526  as_after_return (RTLabs_status ge) «pre,CL» post →
2527  state_fn … pre = state_fn … post.
2528#ge * #pre #preS #preM * #post #postS #postM #CL #AF
2529cases (rtlabs_call_inv … (simplify_cl … CL)) #fd * #args * #dst * #fs * #m #E destruct
2530cases post in postM AF ⊢ %;
2531[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
2532  cases preS in preM AF ⊢ %; [*]
2533  #fn *
2534  [ cases fs [ #M * ]
2535    #f #fs' * #FFP *
2536  | #fn' #S cases fs [ #M * ]
2537    #f #fs' #M * * #N #F #PC destruct %
2538  ]
2539| #A #B #C #D #E #F *
2540| #A #B #C #D #E *
2541| #r #M' #AF whd in AF; destruct
2542  cases preS in preM ⊢ %;
2543  [ // | #fn * [ // | #fn' #S * #FFP * ] ]
2544] qed.
2545
2546lemma state_fn_other : ∀ge,s1,s2.
2547  RTLabs_classify (Ras_state … s1) = cl_other →
2548  as_execute (RTLabs_status ge) s1 s2 →
2549  RTLabs_classify (Ras_state … s2) = cl_return ∨
2550  state_fn … s1 = state_fn … s2.
2551#ge #s1 #s2 #CL #EX
2552cases (declassify_state … EX CL)
2553#f * #fs * #m * * [**] #fn #S * #M #E destruct
2554inversion (eval_preserves_ext … EX)
2555[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
2556| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct %2 %
2557| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2558| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
2559| #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
2560| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
2561] qed.
2562
2563(* The main part of the proof is to walk down the trace_any_label and find the
2564   repeated call state, then show that its successor appears as well. *)
2565
2566let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
2567  (AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2)
2568  (CL2:RTLabs_classify (Ras_state … s2) = cl_other)
2569  (CS2:Not (as_costed (RTLabs_status ge) s2))
2570  (EX1:as_execute (RTLabs_status ge) s1 s1') on tal :
2571  state_fn … s1 = state_fn … s3 →
2572  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal →
2573  as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?.
2574cases tal
2575[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
2576  whd in match (tal_pc_list ?????) in IN;
2577  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2578  cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l
2579  #IN' destruct
2580| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
2581  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee
2582  @(declassify_pc_cl … EX2 CL2) whd #fn
2583  #IN' destruct
2584| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
2585  lapply (memb_single … IN) #E
2586  lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
2587  @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
2588| #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL)
2589| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
2590  whd in ⊢ (?% → ?); @eqb_elim
2591  [ #PC #_
2592    >(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list
2593    <(classify_after_return_eq … AF1 AF3 PC FN) assumption
2594  | #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons
2595    @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN)
2596    >FN @(state_fn_after_return … AF3)
2597  ]
2598| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
2599  lapply (simplify_cl … CL1) #CL1'
2600  lapply (simplify_cl … CL3) #CL3'
2601  @eq_true_to_b @memb_cons
2602  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
2603  [ >FN cases (state_fn_other … CL3' EX3)
2604    [ #CL3'' @⊥
2605      cases (tal_return … (lift_cl … CL3'') tal3')
2606      #EX3' * #CL3''' * #E1 #E2 destruct
2607      whd in IN:(?%); lapply IN @eqb_elim
2608      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2609      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct
2610      ]
2611    | //
2612    ]
2613  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2614    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct
2615    | #NE #IN @IN
2616    ]
2617  ]
2618] qed.
2619
2620(* Then we can start the proof by finding the original successor state... *)
2621
2622lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
2623  as_execute (RTLabs_status ge) s1 s1' →
2624  as_after_return (RTLabs_status ge) «s1,CL» s2 →
2625  ¬as_costed (RTLabs_status ge) s2 →
2626  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal →
2627  ∃s3,EX,CL',CS,tal'.
2628    tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
2629    bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
2630#ge #s1 #s1' #CL #flX #s2X #s4X *
2631[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
2632  whd in match (tal_pc_list ?????) in IN;
2633  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2634  cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l
2635  #IN' destruct
2636| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
2637  lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee
2638  @(declassify_pc_cl … EX2 CL2) whd #fn
2639  #IN' destruct
2640| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
2641  cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2642  cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2643  cases AF1
2644| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
2645| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
2646  cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2647  cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2648  cases AF1
2649| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
2650  lapply (simplify_cl … CL) #CL'
2651  lapply (simplify_cl … CL2) #CL2'
2652  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
2653  (* Now that we've inverted the first part of the trace, look for the repeat. *)
2654  @(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1)
2655  [ >(state_fn_after_return … AF1)
2656    cases (state_fn_other … CL2' EX2)
2657    [ #CL3 @⊥
2658      cases (tal_return … (lift_cl … CL3) tal3)
2659      #EX3 * #CL3' * #E1 #E2 destruct
2660      lapply (simplify_cl … CL3') #CL3''
2661      whd in IN:(?%); lapply IN @eqb_elim
2662      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2663      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct
2664      ]
2665    | //
2666    ]
2667  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2668    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct
2669    | #NE #IN @IN
2670    ]
2671  ]
2672] qed.
2673
2674(* And then we get our counterpart to no_loops_in_tal for calls: *)
2675
2676lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
2677  ∀tal:trace_any_label (RTLabs_status ge) fl after final.
2678  as_execute (RTLabs_status ge) pre start →
2679  as_after_return (RTLabs_status ge) «pre,CL» after →
2680  ¬as_costed (RTLabs_status ge) after →
2681  soundly_labelled_state (Ras_state ge after) →
2682  ¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal.
2683#ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN
2684cases (pc_after_call_repeats … EX AF CS IN)
2685#s * #EX * #CL' * #CSx * #tal' * #E #IN'
2686@(absurd ? IN')
2687@Prop_notb
2688@no_loops_in_tal /2/
2689qed.
2690
2691(* Show that if a state is soundly labelled, then so are the states following
2692   it in a trace. *)
2693
2694lemma soundly_step : ∀ge,s1,s2.
2695  soundly_labelled_ge ge →
2696  as_execute (RTLabs_status ge) s1 s2 →
2697  soundly_labelled_state (Ras_state … s1) →
2698  soundly_labelled_state (Ras_state … s2).
2699#ge #s1 #s2 #GE * #tr * #EX #NX
2700@(soundly_labelled_state_step … GE … EX)
2701qed.
2702
2703let rec tlr_sound ge s1 s2
2704  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
2705  (GE:soundly_labelled_ge ge)
2706on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2707match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with
2708[ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1
2709| tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in
2710                            tlr_sound … tlr' GE S2
2711]
2712and tll_sound ge fl s1 s2
2713  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2714  (GE:soundly_labelled_ge ge)
2715on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2716match tll with
2717[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
2718]
2719and tal_sound ge fl s1 s2
2720  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2721  (GE:soundly_labelled_ge ge)
2722on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2723match tal with
2724[ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1
2725| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
2726| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
2727| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2728| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
2729| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
2730].
2731@(RTLabs_notail' … CL)
2732qed.
2733
2734(* And join everything up to show that soundly labelled states give unrepeating
2735   traces. *)
2736
2737let rec tlr_sound_unrepeating ge
2738  (s1,s2:RTLabs_status ge)
2739  (GE:soundly_labelled_ge ge)
2740  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
2741on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝
2742match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with
2743[ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1
2744| tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1))
2745]
2746and tll_sound_unrepeating ge fl
2747  (s1,s2:RTLabs_status ge)
2748  (GE:soundly_labelled_ge ge)
2749  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2750on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
2751match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with
2752[ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal
2753]
2754and tal_sound_unrepeating ge fl
2755  (s1,s2:RTLabs_status ge)
2756  (GE:soundly_labelled_ge ge)
2757  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
2758on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
2759match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with
2760[ tal_base_not_return _ _ EX _ _ ⇒ λS1. I
2761| tal_base_return _ _ EX _ ⇒ λS1. I
2762| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
2763    tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
2764| tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥
2765| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
2766    conj ?? (conj ???
2767     (tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1))))
2768     (tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1))
2769| tal_step_default _ pre init end EX tal CL _ ⇒ λS1.
2770    conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
2771].
2772[ @(RTLabs_notail' … CL)
2773| @(no_repeats_of_calls … EX AF) [ assumption |
2774  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
2775| @no_loops_in_tal // @simplify_cl @CL
2776] qed.
2777
Note: See TracBrowser for help on using the repository browser.