source: src/RTLabs/RTLabs_traces.ma

Last change on this file was 3050, checked in by piccolo, 7 years ago

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

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