source: src/RTLabs/RTLabs_traces.ma @ 2774

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