source: src/RTLabs/Traces.ma @ 2025

Last change on this file since 2025 was 2025, checked in by campbell, 8 years ago

Silly typo and old comment.

File size: 93.0 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5discriminator status_class.
6
7(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
8       will be added later (LTL → LIN). *)
9
10definition RTLabs_classify : state → status_class ≝
11λs. match s with
12[ State f _ _ ⇒
13    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
14    [ St_cond _ _ _ ⇒ cl_jump
15    | St_jumptable _ _ ⇒ cl_jump
16    | _ ⇒ cl_other
17    ]
18| Callstate _ _ _ _ _ ⇒ cl_call
19| Returnstate _ _ _ _ ⇒ cl_return
20| Finalstate _ ⇒ cl_other
21].
22
23(* We define a straight "is this a cost label" pair of functions, which is
24   convenient for most of our uses here (because we can make a hypothesis of
25   it without naming the label), and a pair which return the label to fit the
26   definition of abstract_status. *)
27   
28definition is_cost_label : statement → bool ≝
29λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
30
31definition RTLabs_cost : state → bool ≝
32λs. match s with
33[ State f fs m ⇒
34    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
35| _ ⇒ false
36].
37
38definition cost_label_of : statement → option costlabel ≝
39λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
40
41definition RTLabs_cost_label : state → option costlabel ≝
42λs. match s with
43[ State f fs m ⇒
44    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
45| _ ⇒ None ?
46].
47
48(* At the moment we don't need to talk about the program counter, so we just
49   use unit. *)
50definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?.
51* * % //
52qed.
53
54definition RTLabs_status : genv → abstract_status ≝
55λge.
56  mk_abstract_status
57    state
58    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
59    unit_deqset
60    (λ_. it)
61    (λs,c. RTLabs_classify s = c)
62    RTLabs_cost_label
63    (λs,s'. match s with
64      [ mk_Sig s p ⇒
65        match s return λs. RTLabs_classify s = cl_call → ? with
66        [ Callstate fd args dst stk m ⇒
67          λ_. match s' with
68          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
69          | Finalstate r ⇒ stk = [ ]
70          | _ ⇒ False
71          ]
72        | State f fs m ⇒ λH.⊥
73        | _ ⇒ λH.⊥
74        ] p
75      ])
76  (λs. RTLabs_is_final s ≠ None ?).
77[ normalize in H; destruct
78| normalize in H; destruct
79| whd in H:(??%?);
80  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
81  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
82] qed.
83
84(* Allow us to move between the different notions of when a state is cost
85   labelled. *)
86
87lemma RTLabs_costed : ∀ge,s.
88  RTLabs_cost s = true →
89  as_costed (RTLabs_status ge) s.
90#ge *
91[ * #func #locals #next #nok #b #r #fs #m
92  whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?));
93  cases (lookup_present ?? (f_graph func) ??) normalize
94  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
95  % #E' destruct
96| normalize #fd #args #r #fs #m #E destruct
97| normalize #A #B #C #D #E destruct
98| normalize #A #B destruct
99] qed.
100
101lemma costed_RTLabs : ∀ge,s.
102  as_costed (RTLabs_status ge) s →
103  RTLabs_cost s = true.
104#ge
105cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H
106*
107[ * #func #locals #next #nok #b #r #fs #m
108  whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?);
109  cases (lookup_present ?? (f_graph func) ??) normalize //
110  #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) //
111| *: normalize #A #B try #C try #D try #E try #F cases (H ?) //
112] qed.
113
114lemma RTLabs_not_cost : ∀ge,s.
115  RTLabs_cost s = false →
116  ¬ as_costed (RTLabs_status ge) s.
117#ge *
118[ * #func #locals #next #nok #b #r #fs #m
119  whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?)));
120  cases (lookup_present ?? (f_graph func) ??) normalize
121  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
122  % * #J @J @refl
123| *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl
124] qed.
125
126(* Before attempting to construct a structured trace, let's show that we can
127   form flat traces with evidence that they were constructed from an execution.
128   
129   For now we don't consider I/O. *)
130
131
132coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
133| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
134| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
135| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
136
137(* add I/O? *)
138coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
139| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
140| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
141| ft_wrong : ∀s,m. RTLabs_is_final s = None ? → eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
142
143coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝
144| nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H)
145| nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr').
146
147lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'.
148  not_wrong o i ge s (ft_step o i ge s tr s' H tr') →
149  not_wrong o i ge s' tr'.
150#o #i #ge #s #tr #s' #H #tr' #NW inversion NW
151[ #H105 #H106 #H107 #H108 #H109 destruct
152| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
153] qed.
154
155let corec make_flat_trace ge s
156  (NF:RTLabs_is_final s = None ?)
157  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
158  flat_trace io_out io_in ge s ≝
159let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
160match e return λx. e = x → ? with
161[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
162| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ??)
163| e_wrong m ⇒ λE. ft_wrong … s m ??
164| e_interact o f ⇒ λE. ⊥
165] (refl ? e).
166[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
167  cases (eval_statement ge s)
168  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
169  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
170    >(?:is_final ????? = RTLabs_is_final s1) //
171    lapply (refl ? (RTLabs_is_final s1))
172    cases (RTLabs_is_final s1) in ⊢ (???% → %);
173    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
174    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
175    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
176    ]
177  | *: #m whd in ⊢ (??%? → ?); #E destruct
178  ]
179| whd in E:(??%?); >exec_inf_aux_unfold in E;
180  cases (eval_statement ge s)
181  [ #O #K whd in ⊢ (??%? → ?); #E destruct
182  | * #tr #s1 whd in ⊢ (??%? → ?);
183    cases (is_final ?????)
184    [ whd in ⊢ (??%? → ?); #E destruct @refl
185    | #i whd in ⊢ (??%? → ?); #E destruct
186    ]
187  | #m whd in ⊢ (??%? → ?); #E destruct
188  ]
189| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
190  cases (eval_statement ge s)
191  [ #O #K whd in ⊢ (??%? → ?); #E destruct
192  | * #tr #s1 whd in ⊢ (??%? → ?);
193    cases (is_final ?????)
194    [ whd in ⊢ (??%? → ?); #E
195      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
196      destruct
197      inversion H
198      [ #a #b #c #E1 destruct
199      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
200      | #m #E1 destruct
201      ]
202    | #i whd in ⊢ (??%? → ?); #E destruct
203    ]
204  | #m whd in ⊢ (??%? → ?); #E destruct
205  ]
206| whd in E:(??%?); >exec_inf_aux_unfold in E;
207  cases (eval_statement ge s)
208  [ #o #K whd in ⊢ (??%? → ?); #E destruct
209  | * #tr #s1 whd in ⊢ (??%? → ?);
210    lapply (refl ? (RTLabs_is_final s1))
211    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
212    cases (RTLabs_is_final s1) in ⊢ (???% → %);
213    [ #F #E whd in E:(??%?); destruct @F
214    | #r #F #E whd in E:(??%?); destruct
215    ]
216  | #m #E whd in E:(??%?); destruct
217  ]
218| @NF
219| whd in E:(??%?); >exec_inf_aux_unfold in E;
220  cases (eval_statement ge s)
221  [ #O #K whd in ⊢ (??%? → ?); #E destruct
222  | * #tr1 #s1 whd in ⊢ (??%? → ?);
223    cases (is_final ?????)
224    [ whd in ⊢ (??%? → ?); #E destruct
225    | #i whd in ⊢ (??%? → ?); #E destruct
226    ]
227  | #m whd in ⊢ (??%? → ?); #E destruct @refl
228  ]
229| whd in E:(??%?); >E in H; #H
230  inversion H
231  [ #a #b #c #E destruct
232  | #a #b #c #d #E1 destruct
233  | #m #E1 destruct
234  ]
235] qed.
236
237let corec make_whole_flat_trace p s
238  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
239  (I:make_initial_state ??? p = OK ? s) :
240  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
241let ge ≝ make_global … p in
242let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
243match e return λx. e = x → ? with
244[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
245| e_step _ _ e' ⇒ λE. make_flat_trace ge s ??
246| e_wrong m ⇒ λE. ⊥
247| e_interact o f ⇒ λE. ⊥
248] (refl ? e).
249[ whd in E:(??%?); >exec_inf_aux_unfold in E;
250  whd in ⊢ (??%? → ?);
251  change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
252  cases (RTLabs_is_final s)
253  [ #E whd in E:(??%?); destruct
254  | #r #E % #E' destruct
255  ]
256| @(initial_state_is_not_final … I)
257| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
258  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
259  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
260    [ #a #b #c #E1 destruct
261    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
262      @H1
263    | #m #E1 destruct
264    ]
265  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
266  ]
267| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
268  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
269| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
270  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
271] qed.
272
273(* Need a way to choose whether a called function terminates.  Then,
274     if the initial function terminates we generate a purely inductive structured trace,
275     otherwise we start generating the coinductive one, and on every function call
276       use the choice method again to decide whether to step over or keep going.
277
278Not quite what we need - have to decide on seeing each label whether we will see
279another or hit a non-terminating call?
280
281Also - need the notion of well-labelled in order to break loops.
282
283
284
285outline:
286
287 does function terminate?
288 - yes, get (bound on the number of steps until return), generate finite
289        structure using bound as termination witness
290 - no,  get (¬ bound on steps to return), start building infinite trace out of
291        finite steps.  At calls, check for termination, generate appr. form.
292
293generating the finite parts:
294
295We start with the status after the call has been executed; well-labelling tells
296us that this is a labelled state.  Now we want to generate a trace_label_return
297and also return the remainder of the flat trace.
298
299*)
300
301(* [will_return ge depth s trace] says that after a finite number of steps of
302   [trace] from [s] we reach the return state for the current function.  [depth]
303   performs the call/return counting necessary for handling deeper function
304   calls.  It should be zero at the top level. *)
305inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
306| wr_step : ∀s,tr,s',depth,EX,trace.
307    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
308    will_return ge depth s' trace →
309    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
310| wr_call : ∀s,tr,s',depth,EX,trace.
311    RTLabs_classify s = cl_call →
312    will_return ge (S depth) s' trace →
313    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
314| wr_ret : ∀s,tr,s',depth,EX,trace.
315    RTLabs_classify s = cl_return →
316    will_return ge depth s' trace →
317    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
318    (* Note that we require the ability to make a step after the return (this
319       corresponds to somewhere that will be guaranteed to be a label at the
320       end of the compilation chain). *)
321| wr_base : ∀s,tr,s',EX,trace.
322    RTLabs_classify s = cl_return →
323    will_return ge O s (ft_step ?? ge s tr s' EX trace)
324.
325
326(* The way we will use [will_return] won't satisfy Matita's guardedness check,
327   so we will measure the length of these termination proofs and use an upper
328   bound to show termination of the finite structured trace construction
329   functions. *)
330
331let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
332match T with
333[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
334| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
335| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
336| wr_base _ _ _ _ _ _ ⇒ S O
337].
338
339include alias "arithmetics/nat.ma".
340
341(* Specialised to the particular situation it is used in. *)
342lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
343#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
344whd in ⊢ (??(??%) → ?);
345>commutative_times
346#H lapply (le_plus_b … H)
347#H lapply (le_to_leb_true … H)
348normalize #E destruct
349qed.
350   
351let 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' ≝
352match T with
353[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
354| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
355| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
356| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
357].
358
359(* Inversion lemmas on [will_return] that also note the effect on the length
360   of the proof. *)
361lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
362  RTLabs_classify s = cl_call →
363  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
364  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
365#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
366[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
367| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
368| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
369| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
370] qed.
371
372lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
373  RTLabs_classify s = cl_return →
374  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
375  match d with
376  [ O ⇒ will_return_end … TM = ❬s', trace❭
377  | S d' ⇒
378      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
379  ].
380#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
381[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
382| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
383| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
384| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
385] qed.
386
387lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
388  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
389  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
390  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
391#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
392[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
393| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
394| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
395| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
396| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
397| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
398| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
399| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
400] qed.
401
402(* When it comes to building bits of nonterminating executions we'll need to be
403   able to glue termination proofs together. *)
404
405lemma will_return_prepend : ∀ge,d1,s1,t1.
406  ∀T1:will_return ge d1 s1 t1.
407  ∀d2,s2,t2.
408  will_return ge d2 s2 t2 →
409  will_return_end … T1 = ❬s2, t2❭ →
410  will_return ge (d1 + S d2) s1 t1.
411#ge #d1 #s1 #tr1 #T1 elim T1
412[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
413  %1 // @(IH … T2) @E
414| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
415| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
416| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
417] qed.
418
419discriminator nat.
420
421lemma will_return_remove_call : ∀ge,d1,s1,t1.
422  ∀T1:will_return ge d1 s1 t1.
423  ∀d2.
424  will_return ge (d1 + S d2) s1 t1 →
425  ∀s2,t2.
426  will_return_end … T1 = ❬s2, t2❭ →
427  will_return ge d2 s2 t2.
428(* The key part of the proof is to show that the two termination proofs follow
429   the same pattern. *)
430#ge #d1x #s1x #t1x #T1 elim T1
431[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
432  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
433                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
434                   >H21 in CL; * #E destruct
435                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
436                   >H35 in CL; * #E destruct
437                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
438                   >H48 in CL; * #E destruct
439                 ]
440  | @E
441  ]
442| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
443  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
444                   >CL in H7; * #E destruct
445                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
446                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
447                   >H35 in CL; #E destruct
448                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
449                   >H48 in CL; #E destruct
450                 ]
451  | @E
452  ]
453| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
454  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
455                   >CL in H7; * #E destruct
456                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
457                   >H21 in CL; #E destruct
458                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
459                   whd in H38:(??%??); destruct //
460                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
461                   whd in H49:(??%??); @⊥ destruct
462                 ]
463  | @E
464  ]
465| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
466  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
467                 >CL in H7; * #E destruct
468               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
469                 >H21 in CL; #E destruct
470               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
471                 whd in H38:(??%??); destruct //
472               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
473                 whd in H49:(??%??); @⊥ destruct
474               ]
475] qed.
476
477lemma will_return_not_wrong : ∀ge,d,s,t,s',t'.
478  ∀T:will_return ge d s t.
479  not_wrong io_out io_in ge s t →
480  will_return_end … T = ❬s', t'❭ →
481  not_wrong io_out io_in ge s' t'.
482#ge #d #s #t #s' #t' #T elim T
483[ #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
484  [ inversion NW
485    [ #H1 #H2 #H3 #H4 #H5 destruct
486    | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
487    ]
488  | @E
489  ]
490| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
491  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
492  | @E
493  ]
494| #s #tr #s' #d #EV #t1 #CL #T' #IH #NW #E @IH
495  [ inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
496  | @E
497  ]
498| #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct
499  inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct | #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ]
500] qed.
501
502
503lemma will_return_lower : ∀ge,d,s,t.
504  will_return ge d s t →
505  ∀d'. d' ≤ d →
506  will_return ge d' s t.
507#ge #d0 #s0 #t0 #TM elim TM
508[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
509| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
510| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
511  [ #LE @wr_base //
512  | #d' #LE %3 // @IH /2/
513  ]
514| #s #tr #s' #EX #tr #CL *
515  [ #_ @wr_base //
516  | #d' #LE @⊥ /2/
517  ]
518] qed.
519
520(* We require that labels appear after branch instructions and at the start of
521   functions.  The first is required for preciseness, the latter for soundness.
522   We will make a separate requirement for there to be a finite number of steps
523   between labels to catch loops for soundness (is this sufficient?). *)
524
525definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
526λf,s. match s return λs. labels_present ? s → Prop with
527[ St_cond _ l1 l2 ⇒ λH.
528    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
529    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
530| St_jumptable _ ls ⇒ λH.
531    (* I did have a dependent version of All here, but it's a pain. *)
532    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
533| _ ⇒ λ_. True
534]. whd in H;
535[ @(proj1 … H)
536| @(proj2 … H)
537] qed.
538
539definition well_cost_labelled_fn : internal_function → Prop ≝
540λf. (∀l. ∀H:present … (f_graph f) l.
541         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
542    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
543[ @lookup_lookup_present | cases (f_entry f) // ] qed.
544
545(* We need to ensure that any code we come across is well-cost-labelled.  We may
546   get function code from either the global environment or the state. *)
547
548definition well_cost_labelled_ge : genv → Prop ≝
549λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
550
551definition well_cost_labelled_state : state → Prop ≝
552λs. match s with
553[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
554| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
555                          All ? (λf. well_cost_labelled_fn (func f)) fs
556| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
557| Finalstate _ ⇒ True
558].
559
560lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
561  eval_statement ge s = Value ??? 〈tr,s'〉 →
562  well_cost_labelled_ge ge →
563  well_cost_labelled_state s →
564  well_cost_labelled_state s'.
565#ge #s #tr' #s' #EV cases (eval_preserves … EV)
566[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
567| #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
568(*
569| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
570*)
571| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
572| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
573| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
574| //
575] qed.
576
577lemma rtlabs_jump_inv : ∀s.
578  RTLabs_classify s = cl_jump →
579  ∃f,fs,m. s = State f fs m ∧
580  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
581  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
582*
583[ #f #fs #m #E
584  %{f} %{fs} %{m} %
585  [ @refl
586  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
587    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
588    [ %1 %{A} %{B} %{C} @refl
589    | %2 %{A} %{B} @refl
590    ]
591  ]
592| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
593| normalize #H8 #H9 #H10 #H11 #H12 destruct
594| #r #E normalize in E; destruct
595] qed.
596
597lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
598  eval_statement ge s = Value ??? 〈tr,s'〉 →
599  well_cost_labelled_state s →
600  RTLabs_classify s = cl_jump →
601  RTLabs_cost s' = true.
602#ge #s #tr #s' #EV #H #CL
603cases (rtlabs_jump_inv s CL)
604#fr * #fs * #m * #Es *
605[ * #r * #l1 * #l2 #Estmt
606  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
607  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
608  >Estmt #LP whd in ⊢ (??%? → ?);
609  (* replace with lemma on successors? *)
610  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
611  lapply (Hbody (next fr) (next_ok fr))
612  generalize in ⊢ (???% → ?);
613  >Estmt #LP'
614  whd in ⊢ (% → ?);
615  * #H1 #H2 [ @H1 | @H2 ]
616| * #r * #ls #Estmt
617  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
618  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
619  >Estmt #LP whd in ⊢ (??%? → ?);
620  (* replace with lemma on successors? *)
621  @bind_res_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
622  [ 2: (* later *)
623  | *: #E destruct
624  ]
625  lapply (Hbody (next fr) (next_ok fr))
626  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
627  generalize in ⊢ (??(?%)? → ?);
628  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
629  [ #E1 #E2 whd in E2:(??%?); destruct
630  | #l' #E1 #E2 whd in E2:(??%?); destruct
631    cases (All_nth ???? CP ? E1)
632    #H1 #H2 @H2
633  ]
634] qed.
635
636lemma rtlabs_call_inv : ∀s.
637  RTLabs_classify s = cl_call →
638  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
639* [ #f #fs #m whd in ⊢ (??%? → ?);
640    cases (lookup_present … (next f) (next_ok f)) normalize
641    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
642  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
643  | normalize #H411 #H412 #H413 #H414 #H415 destruct
644  | normalize #H1 #H2 destruct
645  ] qed.
646
647lemma well_cost_labelled_call : ∀ge,s,tr,s'.
648  eval_statement ge s = Value ??? 〈tr,s'〉 →
649  well_cost_labelled_state s →
650  RTLabs_classify s = cl_call →
651  RTLabs_cost s' = true.
652#ge #s #tr #s' #EV #WCL #CL
653cases (rtlabs_call_inv s CL)
654#fd * #args * #dst * #stk * #m #E >E in EV WCL;
655whd in ⊢ (??%? → % → ?);
656cases fd
657[ #fn whd in ⊢ (??%? → % → ?);
658  @bind_res_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
659  #m' #b whd in ⊢ (??%? → ?); #E' destruct
660  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
661  @WCL2
662| #fn whd in ⊢ (??%? → % → ?);
663  @bindIO_value #evargs #Eargs
664  whd in ⊢ (??%? → ?);
665  #E' destruct
666] qed.
667
668
669(* The preservation of (most of) the stack is useful to show as_after_return.
670   We do this by showing that during the execution of a function the lower stack
671   frames never change, and that after returning from the function we preserve
672   the identity of the next instruction to execute.
673 *)
674
675inductive stack_of_state : list frame → state → Prop ≝
676| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
677| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
678| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
679.
680
681inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
682| sp_normal : ∀fs,s1,s2.
683    stack_of_state fs s1 →
684    stack_of_state fs s2 →
685    stack_preserved doesnt_end_with_ret s1 s2
686| sp_finished : ∀s1,f,f',fs,m.
687    next f = next f' →
688    frame_rel f f' →
689    stack_of_state (f::fs) s1 →
690    stack_preserved ends_with_ret s1 (State f' fs m)
691| sp_stop : ∀s1,r.
692    stack_of_state [ ] s1 →
693    stack_preserved ends_with_ret s1 (Finalstate r)
694| sp_top : ∀fd,args,dst,m,r.
695    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
696.
697
698discriminator list.
699
700lemma stack_of_state_eq : ∀fs,fs',s.
701  stack_of_state fs s →
702  stack_of_state fs' s →
703  fs = fs'.
704#fs0 #fs0' #s0 *
705[ #f #fs #m #H inversion H
706  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
707| #fd #args #dst #f #fs #m #H inversion H
708  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
709| #rtv #dst #fs #m #H inversion H
710  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
711] qed.
712
713lemma stack_preserved_final : ∀e,r,s.
714  ¬stack_preserved e (Finalstate r) s.
715#e #r #s % #H inversion H
716[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
717  inversion SOS #a #b #c #d #e #f try #g try #h destruct
718| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
719  inversion SOS #a #b #c #d #e #f try #g try #h destruct
720| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
721  inversion SOS #a #b #c #d #e #f try #g try #h destruct
722| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
723] qed.
724
725lemma stack_preserved_join : ∀e,s1,s2,s3.
726  stack_preserved doesnt_end_with_ret s1 s2 →
727  stack_preserved e s2 s3 →
728  stack_preserved e s1 s3.
729#e1 #s1 #s2 #s3 #H1 inversion H1
730[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
731  #H2 inversion H2
732  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
733    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
734  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
735    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
736  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
737  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
738    inversion S2
739    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
740    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
741    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
742    ]
743  ]
744| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
745| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
746  cases (stack_preserved_final … H) #r #E destruct
747| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
748  @(absurd … F) //
749] qed.
750
751lemma stack_preserved_return : ∀ge,s1,s2,tr.
752  RTLabs_classify s1 = cl_return →
753  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
754  stack_preserved ends_with_ret s1 s2.
755#ge *
756[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
757  cases (lookup_present ??? (next f) (next_ok f)) in E;
758  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
759| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
760| #res #dst *
761  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
762    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
763  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV
764    whd in EV:(??%?); destruct @(sp_finished ? f) //
765    cases f //
766  ]
767| #r #s2 #tr #E normalize in E; destruct
768] qed.
769
770lemma stack_preserved_step : ∀ge,s1,s2,tr.
771  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
772  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
773  stack_preserved doesnt_end_with_ret s1 s2.
774#ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
775[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
776| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
777| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
778  normalize in CL; cases CL #E destruct
779| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
780| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
781  #E normalize in E; destruct
782| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
783] qed.
784
785lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
786  RTLabs_classify s1 = cl_call →
787  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
788  stack_preserved ends_with_ret s2 s3 →
789  stack_preserved doesnt_end_with_ret s1 s3.
790#ge #s1 #s2 #s3 #tr #CL #EV #SP
791cases (rtlabs_call_inv … CL)
792#fd * #args * #dst * #stk * #m #E destruct
793inversion SP
794[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
795| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
796  inversion (eval_preserves … EV)
797  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
798  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
799  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
800    inversion S
801    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
802    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
803    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
804    ]
805  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
806  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
807  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
808  ]
809| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
810  inversion (eval_preserves … EV)
811  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
812  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
813  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
814    inversion S1
815    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
816    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
817    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
818    ]
819  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
820  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
821  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
822  ]
823| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
824] qed.
825 
826lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
827  ∀CL : RTLabs_classify s1 = cl_call.
828  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
829  stack_preserved ends_with_ret s2 s3 →
830  as_after_return (RTLabs_status ge) «s1,CL» s3.
831#ge #s1 #s2 #s3 #tr #CL #EV #S23
832cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
833inversion S23
834[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
835| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
836  inversion (eval_preserves … EV)
837  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
838  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
839  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
840    inversion S
841    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
842    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
843    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
844    ]
845  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
846  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
847  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
848  ]
849| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
850  inversion (eval_preserves … EV)
851  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
852  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
853  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
854    inversion S1
855    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
856    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
857    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
858    ]
859  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
860  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
861  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
862  ]
863| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
864] qed.
865
866(* Don't need to know that labels break loops because we have termination. *)
867
868(* A bit of mucking around with the depth to avoid proving termination after
869   termination.  Note that we keep a proof that our upper bound on the length
870   of the termination proof is respected. *)
871record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
872  (start:state) (full:flat_trace io_out io_in ge start)
873  (original_terminates: will_return ge depth start full)
874  (T:state → Type[0]) (limit:nat) : Type[0] ≝
875{
876  new_state : state;
877  remainder : flat_trace io_out io_in ge new_state;
878  cost_labelled : well_cost_labelled_state new_state;
879  new_trace : T new_state;
880  stack_ok : stack_preserved ends start new_state;
881  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
882               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
883               | S d ⇒ ΣTM:will_return ge d new_state remainder.
884                         limit > will_return_length … TM ∧
885                         will_return_end … original_terminates = will_return_end … TM
886               ]
887}.
888
889(* The same with a flag indicating whether the function returned, as opposed to
890   encountering a label. *)
891record sub_trace_result (ge:genv) (depth:nat)
892  (start:state) (full:flat_trace io_out io_in ge start)
893  (original_terminates: will_return ge depth start full)
894  (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝
895{
896  ends : trace_ends_with_ret;
897  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
898}.
899
900(* We often return the result from a recursive call with an addition to the
901   structured trace, so we define a couple of functions to help.  The bound on
902   the size of the termination proof might need to be relaxed, too. *)
903
904definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
905  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
906    will_return_end … TM1 = will_return_end … TM2 →
907    T2 (new_state … r) →
908    stack_preserved e s2 (new_state … r) →
909    trace_result ge d e s2 t2 TM2 T2 l2 ≝
910λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
911  mk_trace_result ge d e s2 t2 TM2 T2 l2
912    (new_state … r)
913    (remainder … r)
914    (cost_labelled … r)
915    trace
916    SP
917    ?
918    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
919                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
920     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
921.
922cases e in r ⊢ %;
923[ <TME -TME * cases d in TM1 TM2 ⊢ %;
924  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
925  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
926    %{TMa} % // @(transitive_le … lGE) @L1
927  ]
928| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
929   * #TMa * #L1 #TME
930    %{TMa} % // @(transitive_le … lGE) @L1
931] qed.
932
933definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
934  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
935    will_return_end … TM1 = will_return_end … TM2 →
936    T2 (ends … r) (new_state … r) →
937    stack_preserved (ends … r) s2 (new_state … r) →
938    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
939λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
940  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
941    (ends … r)
942    (replace_trace … lGE … r TME trace SP).
943
944(* Small syntax hack to avoid ambiguous input problems. *)
945definition myge : nat → nat → Prop ≝ ge.
946
947let rec make_label_return ge depth s
948  (trace: flat_trace io_out io_in ge s)
949  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
950  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
951  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
952  (TERMINATES: will_return ge depth s trace)
953  (TIME: nat)
954  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
955  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
956              (trace_label_return (RTLabs_status ge) s)
957              (will_return_length … TERMINATES) ≝
958             
959match TIME return λTIME. TIME ≥ ? → ? with
960[ O ⇒ λTERMINATES_IN_TIME. ⊥
961| S TIME ⇒ λTERMINATES_IN_TIME.
962
963  let r ≝ make_label_label ge depth s
964            trace
965            ENV_COSTLABELLED
966            STATE_COSTLABELLED
967            STATEMENT_COSTLABEL
968            TERMINATES
969            TIME ? in
970  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
971                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
972  [ ends_with_ret ⇒ λr.
973      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
974  | doesnt_end_with_ret ⇒ λr.
975      let r' ≝ make_label_return ge depth (new_state … r)
976                 (remainder … r)
977                 ENV_COSTLABELLED
978                 (cost_labelled … r) ?
979                 (pi1 … (terminates … r)) TIME ? in
980        replace_trace … r' ?
981          (tlr_step (RTLabs_status ge) s (new_state … r)
982            (new_state … r') (new_trace … r) (new_trace … r')) ?
983  ] (trace_res … r)
984
985] TERMINATES_IN_TIME
986
987
988and make_label_label ge depth s
989  (trace: flat_trace io_out io_in ge s)
990  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
991  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
992  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
993  (TERMINATES: will_return ge depth s trace)
994  (TIME: nat)
995  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
996  on TIME : sub_trace_result ge depth s trace TERMINATES
997              (λends. trace_label_label (RTLabs_status ge) ends s)
998              (will_return_length … TERMINATES) ≝
999             
1000match TIME return λTIME. TIME ≥ ? → ? with
1001[ O ⇒ λTERMINATES_IN_TIME. ⊥
1002| S TIME ⇒ λTERMINATES_IN_TIME.
1003
1004let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
1005  replace_sub_trace … r ?
1006    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
1007
1008] TERMINATES_IN_TIME
1009
1010
1011and make_any_label ge depth s
1012  (trace: flat_trace io_out io_in ge s)
1013  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1014  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1015  (TERMINATES: will_return ge depth s trace)
1016  (TIME: nat)
1017  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
1018  on TIME : sub_trace_result ge depth s trace TERMINATES
1019              (λends. trace_any_label (RTLabs_status ge) ends s)
1020              (will_return_length … TERMINATES) ≝
1021
1022match TIME return λTIME. TIME ≥ ? → ? with
1023[ O ⇒ λTERMINATES_IN_TIME. ⊥
1024| S TIME ⇒ λTERMINATES_IN_TIME.
1025
1026  match trace return λs,trace. well_cost_labelled_state s →
1027                               ∀TM:will_return ??? trace.
1028                               myge ? (times 3 (will_return_length ??? trace TM)) →
1029                               sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
1030  [ ft_stop st FINAL ⇒
1031      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
1032
1033  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
1034    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
1035    [ cl_other ⇒ λCL.
1036        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
1037        (* We're about to run into a label. *)
1038        [ true ⇒ λCS.
1039            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1040              doesnt_end_with_ret
1041              (mk_trace_result ge … next trace' ?
1042                (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) ??)
1043        (* An ordinary step, keep going. *)
1044        | false ⇒ λCS.
1045            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
1046                replace_sub_trace … r ?
1047                  (tal_step_default (RTLabs_status ge) (ends … r)
1048                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
1049        ] (refl ??)
1050       
1051    | cl_jump ⇒ λCL.
1052        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1053          doesnt_end_with_ret
1054          (mk_trace_result ge … next trace' ?
1055            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
1056           
1057    | cl_call ⇒ λCL.
1058        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
1059        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
1060        (* We're about to run into a label, use base case for call *)
1061        [ true ⇒ λCS.
1062            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1063            doesnt_end_with_ret
1064            (mk_trace_result ge …
1065              (tal_base_call (RTLabs_status ge) start next (new_state … r)
1066                ? CL ? (new_trace … r) (RTLabs_costed … CS)) ??)
1067        (* otherwise use step case *)
1068        | false ⇒ λCS.
1069            let r' ≝ make_any_label ge depth
1070                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
1071                       (pi1 … (terminates … r)) TIME ? in
1072            replace_sub_trace … r' ?
1073              (tal_step_call (RTLabs_status ge) (ends … r')
1074                start next (new_state … r) (new_state … r') ? CL ?
1075                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
1076        ] (refl ??)
1077
1078    | cl_return ⇒ λCL.
1079        mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
1080          ends_with_ret
1081          (mk_trace_result ge …
1082            next
1083            trace'
1084            ?
1085            (tal_base_return (RTLabs_status ge) start next ? CL)
1086            ?
1087            ?)
1088    ] (refl ? (RTLabs_classify start))
1089   
1090  | ft_wrong start m NF EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
1091 
1092  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
1093] TERMINATES_IN_TIME.
1094
1095[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1096| //
1097| //
1098| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1099| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1100| @(stack_preserved_join … (stack_ok … r)) //
1101| @(costed_RTLabs ge) @(trace_label_label_label … (new_trace … r))
1102| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1103  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1104  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1105  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1106    @(monotonic_le_times_r 3 … LT)
1107  | @le_S @le_S @le_n
1108  ]
1109| @le_S_S_to_le @TERMINATES_IN_TIME
1110| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1111| @le_n
1112| //
1113| @RTLabs_costed //
1114| @le_S_S_to_le @TERMINATES_IN_TIME
1115| @(wrl_nonzero … TERMINATES_IN_TIME)
1116| (* We can't reach the final state because the function terminates with a
1117     return *)
1118  inversion TERMINATES
1119  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1120  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1121  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1122  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1123  ]
1124| @(will_return_return … CL TERMINATES)
1125| /2 by stack_preserved_return/
1126| %{tr} @EV
1127| @(well_cost_labelled_state_step  … EV) //
1128| whd @(will_return_notfn … TERMINATES) %2 @CL
1129| @stack_preserved_step /2/
1130| %{tr} @EV
1131| %1 whd @CL
1132| @RTLabs_costed @(well_cost_labelled_jump … EV) //
1133| @(well_cost_labelled_state_step  … EV) //
1134| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1135  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1136    #TMx * #LT' #_ @LT'
1137  | <EQr cases (will_return_call … CL TERMINATES)
1138    #TM' * #_ #EQ' @EQ'
1139  ]
1140| @(stack_preserved_call … EV (stack_ok … r)) //
1141| %{tr} @EV
1142| @RTLabs_after_call //
1143| @(cost_labelled … r)
1144| skip
1145| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1146  @(transitive_lt … LT)
1147  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1148| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1149  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //
1150| @RTLabs_after_call //
1151| %{tr} @EV
1152| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
1153| @(cost_labelled … r)
1154| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1155  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1156  cases (will_return_call … TERMINATES) in GT;
1157  #X * #Y #_ #Z
1158  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1159  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1160  | //
1161  ]
1162| @(well_cost_labelled_state_step  … EV) //
1163| @(well_cost_labelled_call … EV) //
1164| cases (will_return_call … TERMINATES)
1165  #TM * #GT #_ @le_S_S_to_le
1166  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1167  @(transitive_le … TERMINATES_IN_TIME)
1168  @(monotonic_le_times_r 3 … GT)
1169| whd @(will_return_notfn … TERMINATES) %1 @CL
1170| @(stack_preserved_step … EV) /2/
1171| %{tr} @EV
1172| %2 whd @CL
1173| @(well_cost_labelled_state_step  … EV) //
1174| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1175| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //
1176| @CL
1177| %{tr} @EV
1178| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
1179| @(well_cost_labelled_state_step  … EV) //
1180| %1 @CL
1181| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1182  @le_S_S_to_le
1183  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1184  //
1185| inversion TERMINATES
1186  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
1187  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
1188  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
1189  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
1190  ]
1191] qed.
1192
1193(* We can initialise TIME with a suitably large value based on the length of the
1194   termination proof. *)
1195let rec make_label_return' ge depth s
1196  (trace: flat_trace io_out io_in ge s)
1197  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1198  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1199  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1200  (TERMINATES: will_return ge depth s trace)
1201  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1202make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1203  (2 + 3 * will_return_length … TERMINATES) ?.
1204@le_n
1205qed.
1206 
1207(* Tail-calls would not be handled properly (which means that if we try to show the
1208   full version with non-termination we'll fail because calls and returns aren't
1209   balanced.
1210 *)
1211
1212inductive inhabited (T:Type[0]) : Prop ≝
1213| witness : T → inhabited T.
1214
1215(* We also require that program's traces are soundly labelled: for any state
1216   in the execution, we can give a distance to a labelled state or termination.
1217   
1218   Note that this differs from the syntactic notions in earlier languages
1219   because it is a global property.  In principle, we would have a loop broken
1220   only by a call to a function (which necessarily has a label) and no local
1221   cost label.
1222 *)
1223
1224let rec nth_state ge s
1225  (trace: flat_trace io_out io_in ge s)
1226  n
1227  on n : option state ≝
1228match n with
1229[ O ⇒ Some ? s
1230| S n' ⇒
1231  match trace with
1232  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
1233  | _ ⇒ None ?
1234  ]
1235].
1236
1237definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
1238λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
1239
1240lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
1241  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
1242  soundly_labelled_trace ge s' trace'.
1243#ge #s #tr #s' #EV #trace' #H
1244#n cases (H (S n)) #m #H' %{m} @H'
1245qed.
1246
1247(* Define a notion of sound labellings of RTLabs programs. *)
1248
1249let rec successors (s : statement) : list label ≝
1250match s with
1251[ St_skip l ⇒ [l]
1252| St_cost _ l ⇒ [l]
1253| St_const _ _ _ l ⇒ [l]
1254| St_op1 _ _ _ _ _ l ⇒ [l]
1255| St_op2 _ _ _ _ _ _ _ l ⇒ [l]
1256| St_load _ _ _ l ⇒ [l]
1257| St_store _ _ _ l ⇒ [l]
1258| St_call_id _ _ _ l ⇒ [l]
1259| St_call_ptr _ _ _ l ⇒ [l]
1260(*
1261| St_tailcall_id _ _ ⇒ [ ]
1262| St_tailcall_ptr _ _ ⇒ [ ]
1263*)
1264| St_cond _ l1 l2 ⇒ [l1; l2]
1265| St_jumptable _ ls ⇒ ls
1266| St_return ⇒ [ ]
1267].
1268
1269definition actual_successor : state → option label ≝
1270λs. match s with
1271[ State f fs m ⇒ Some ? (next f)
1272| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1273| Returnstate _ _ _ _ ⇒ None ?
1274| Finalstate _ ⇒ None ?
1275].
1276
1277lemma nth_opt_Exists : ∀A,n,l,a.
1278  nth_opt A n l = Some A a →
1279  Exists A (λa'. a' = a) l.
1280#A #n elim n
1281[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1282| #m #IH *
1283  [ #a #E normalize in E; destruct
1284  | #a #l #a' #E %2 @IH @E
1285  ]
1286] qed.
1287
1288lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1289  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1290  RTLabs_classify s' = cl_return ∨
1291  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1292#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1293whd in ⊢ (??%? → ?);
1294generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1295[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1296| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1297| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1298| #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} % // % //
1299| #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} % // % //
1300| #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} % // % //
1301| #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} % // % //
1302| #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} % // % //
1303| #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} % // % //
1304| #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 %] //
1305| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1306  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
1307  whd in ⊢ (??%? → ?);
1308  generalize in ⊢ (??(?%)? → ?);
1309  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1310  [ #e #E normalize in E; destruct
1311  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1312  ]
1313| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
1314] qed.
1315
1316definition steps_for_statement : statement → nat ≝
1317λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
1318
1319inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
1320| bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n
1321| bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n
1322with bound_on_steps_to_cost1 : label → nat → Prop ≝
1323| bostc_step : ∀l,n,H.
1324    let stmt ≝ lookup_present … g l H in
1325    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1326          bound_on_steps_to_cost g l' n) →
1327    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
1328
1329(*
1330lemma steps_to_label_bound_inv : ∀g,l,n.
1331  steps_to_label_bound g l n →
1332  ∀H. let stmt ≝ lookup_present … g l H in
1333  ∃n'. n = steps_for_statement stmt + n' ∧
1334  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1335        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
1336        steps_to_label_bound g l' n').
1337#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
1338% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
1339qed.
1340  *) 
1341
1342(*
1343definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1344
1345let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1346  soundly_labelled_pc (f_graph fn) (f_entry fn).
1347
1348
1349definition soundly_labelled_frame : frame → Prop ≝
1350λf. soundly_labelled_pc (f_graph (func f)) (next f).
1351
1352definition soundly_labelled_state : state → Prop ≝
1353λs. match s with
1354[ State f _ _ ⇒ soundly_labelled_frame f
1355| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1356| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1357].
1358*)
1359definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1360λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1361definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1362λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1363
1364inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1365| 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
1366| sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
1367| 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)
1368.
1369
1370lemma state_bound_on_steps_to_cost_zero : ∀s.
1371  ¬ state_bound_on_steps_to_cost s O.
1372#s % #H inversion H
1373[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1374  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1375  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1376| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1377| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1378] qed.
1379
1380lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1381  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1382  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1383  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
1384#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1385whd in ⊢ (??%? → ?);
1386generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1387[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1388| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1389| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1390| #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
1391| #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
1392| #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
1393| #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
1394| #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
1395| #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
1396| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1397| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1398  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
1399  whd in ⊢ (??%? → ?);
1400  generalize in ⊢ (??(?%)? → ?);
1401  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1402  [ #e #E normalize in E; destruct
1403  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1404  ]
1405| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1406] qed.
1407
1408lemma bound_after_call : ∀ge,s,s',n.
1409  state_bound_on_steps_to_cost s (S n) →
1410  ∀CL:RTLabs_classify s = cl_call.
1411  as_after_return (RTLabs_status ge) «s, CL» s' →
1412  RTLabs_cost s' = false →
1413  state_bound_on_steps_to_cost s' n.
1414#ge #s #s' #n #H inversion H
1415[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1416  #fn * #args * #dst * #stk * #m' #E destruct
1417| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1418  whd in S; #CL cases s'
1419  [ #f' #fs' #m' * #N #F #CS
1420    %1 whd
1421    inversion S
1422    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1423      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1424    | #l #n #B #E1 #E2 #_ destruct <N <F @B
1425    ]
1426  | #fd' #args' #dst' #fs' #m' *
1427  | #rv #dst' #fs' #m' *
1428  | #r #E normalize in E; destruct
1429  ]
1430| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1431] qed.
1432
1433lemma bound_after_step : ∀ge,s,tr,s',n.
1434  state_bound_on_steps_to_cost s (S n) →
1435  eval_statement ge s = Value ??? 〈tr, s'〉 →
1436  RTLabs_cost s' = false →
1437  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1438   state_bound_on_steps_to_cost s' n.
1439#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1440[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1441  #EVAL cases (eval_successor … EVAL)
1442  [ /3/
1443  | * #l * #S1 #S2 #NC %2
1444  (*
1445    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1446    *)
1447    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1448    inversion (eval_preserves … EVAL)
1449    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1450      >(eval_steps … EVAL) in E2; #En normalize in En;
1451      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1452      %1 inversion (IH … S2)
1453      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1454        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1455        whd in S1:(??%?); destruct >NC in CSx; *
1456      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
1457      ]
1458    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1459      >(eval_steps … EVAL) in E2; #En normalize in En;
1460      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1461      %2 @IH normalize in S1; destruct @S2
1462    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1463      destruct
1464    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1465      normalize in S1; destruct
1466    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1467    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1468    ]
1469  ]
1470| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1471  /3/
1472| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1473  #EVAL #NC %2 inversion (eval_preserves … EVAL)
1474  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1475  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1476  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1477  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1478  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1479    %1 whd in FS ⊢ %;
1480    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
1481    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
1482    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
1483    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1484    inversion FS
1485    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1486        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
1487        >NC in CSx; *
1488    | #lx #nx #H #E1x #E2x #_ destruct @H
1489    ]
1490  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1491  ]
1492] qed.
1493
1494
1495
1496
1497definition soundly_labelled_fn : internal_function → Prop ≝
1498λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n.
1499
1500definition soundly_labelled_ge : genv → Prop ≝
1501λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1502
1503definition soundly_labelled_state : state → Prop ≝
1504λs. match s with
1505[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1506| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1507                          All ? (λf. soundly_labelled_fn (func f)) fs
1508| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1509| Finalstate _ ⇒ True
1510].
1511
1512lemma steps_from_sound : ∀s.
1513  RTLabs_cost s = true →
1514  soundly_labelled_state s →
1515  ∃n. state_bound_on_steps_to_cost s n.
1516* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
1517whd in ⊢ (% → ?); * #SLF #_
1518cases (SLF (next f) (next_ok f)) #n #B1
1519%{n} % @B1
1520qed.
1521
1522lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1523  soundly_labelled_ge ge →
1524  eval_statement ge s = Value ??? 〈tr,s'〉 →
1525  soundly_labelled_state s →
1526  soundly_labelled_state s'.
1527#ge #s #tr #s' #ENV #EV #S
1528inversion (eval_preserves … EV)
1529[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1530  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1531| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1532  whd in S ⊢ %; %
1533  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1534  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1535  ]
1536| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1537  whd in S ⊢ %; @S
1538| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1539  whd in S ⊢ %; cases S //
1540| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
1541  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1542| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1543] qed.
1544
1545lemma soundly_labelled_state_preserved : ∀s,s'.
1546  stack_preserved ends_with_ret s s' →
1547  soundly_labelled_state s →
1548  soundly_labelled_state s'.
1549#s0 #s0' #SP inversion SP
1550[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1551| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
1552  inversion S1
1553  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
1554    * #_ #S whd in S;
1555    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1556    destruct @S
1557  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
1558    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1559    destruct @S
1560  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
1561    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1562    destruct @S
1563  ]
1564| //
1565| //
1566] qed.
1567
1568(* When constructing an infinite trace, we need to be able to grab the finite
1569   portion of the trace for the next [trace_label_diverges] constructor.  We
1570   use the fact that the trace is soundly labelled to achieve this. *)
1571
1572record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1573  ro_well_cost_labelled: well_cost_labelled_state s;
1574  ro_soundly_labelled: soundly_labelled_state s;
1575  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1576  ro_not_undefined: not_wrong … t;
1577  ro_not_final: RTLabs_is_final s = None ?
1578}.
1579
1580inductive finite_prefix (ge:genv) : state → Prop ≝
1581| fp_tal : ∀s,s'.
1582           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1583           ∀t:flat_trace io_out io_in ge s'.
1584           remainder_ok ge s' t →
1585           finite_prefix ge s
1586| fp_tac : ∀s1,s2,s3,tr.
1587           trace_any_call (RTLabs_status ge) s1 s2 →
1588           well_cost_labelled_state s2 →
1589           eval_statement ge s2 = Value ??? 〈tr,s3〉 →
1590           ∀t:flat_trace io_out io_in ge s3.
1591           remainder_ok ge s3 t →
1592           finite_prefix ge s1
1593.
1594
1595definition fp_add_default : ∀ge,s,s'.
1596  RTLabs_classify s = cl_other →
1597  finite_prefix ge s' →
1598  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
1599  RTLabs_cost s' = false →
1600  finite_prefix ge s ≝
1601λge,s,s',OTHER,fp.
1602match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
1603[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1604    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1605    rem rok
1606| fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr
1607    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1608    WCL2 EV rem rok
1609].
1610
1611definition fp_add_terminating_call : ∀ge,s,s1,s''.
1612  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
1613  ∀CALL:RTLabs_classify s = cl_call.
1614  finite_prefix ge s'' →
1615  trace_label_return (RTLabs_status ge) s1 s'' →
1616  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1617  RTLabs_cost s'' = false →
1618  finite_prefix ge s ≝
1619λge,s,s1,s'',EVAL,CALL,fp.
1620match fp return λs''.λ_. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
1621[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1622    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1623    rem rok
1624| fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr
1625    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1626    WCL2 EV rem rok
1627].
1628
1629lemma not_return_to_not_final : ∀ge,s,tr,s'.
1630  eval_statement ge s = Value ??? 〈tr, s'〉 →
1631  RTLabs_classify s ≠ cl_return →
1632  RTLabs_is_final s' = None ?.
1633#ge #s #tr #s' #EV
1634inversion (eval_preserves … EV) //
1635#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1636@⊥ @(absurd ?? CL) @refl
1637qed.
1638
1639definition termination_oracle ≝ ∀ge,depth,s,trace.
1640  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1641
1642let rec finite_segment ge s n trace
1643  (ORACLE: termination_oracle)
1644  (TRACE_OK: remainder_ok ge s trace)
1645  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1646  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1647  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1648  on n : finite_prefix ge s ≝
1649match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1650[ O ⇒ λLABEL_LIMIT. ⊥
1651| S n' ⇒
1652    match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with
1653    [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1654    | ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT.
1655        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1656        [ cl_other ⇒ λCL.
1657            let TRACE_OK' ≝ ? in
1658            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1659            [ true ⇒ λCS.
1660                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) trace' TRACE_OK'
1661            | false ⇒ λCS.
1662                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1663                fp_add_default ge ?? CL fs ? CS
1664            ] (refl ??)
1665        | cl_jump ⇒ λCL.
1666            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ?
1667        | cl_call ⇒ λCL.
1668            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
1669            [ or_introl TERMINATES ⇒
1670              match TERMINATES with [ witness TERMINATES ⇒
1671                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1672                let TRACE_OK' ≝ ? in
1673                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
1674                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed … CS)) (remainder … tlr) TRACE_OK'
1675                | false ⇒ λCS.
1676                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1677                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
1678                ] (refl ??)
1679              ]
1680            | or_intror NO_TERMINATION ⇒
1681                fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ?
1682            ]
1683        | cl_return ⇒ λCL. ⊥
1684        ] (refl ??)
1685    | ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥
1686    ] TRACE_OK
1687] LABEL_LIMIT.
1688[ cases (state_bound_on_steps_to_cost_zero s) /2/
1689| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1690| @(absurd ?? (ro_no_termination … TRACE_OK))
1691     %{0} % @wr_base //
1692| @RTLabs_costed @(well_cost_labelled_jump … EV) /2/
1693| 5,6,8,9,10,11: /3/
1694| % [ @(well_cost_labelled_state_step … EV) /2/
1695    | @(soundly_labelled_state_step … EV) /2/
1696    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1697    | @(still_not_wrong … EV) /2/
1698    | @(not_return_to_not_final … EV) >CL % #E destruct
1699    ]
1700| /2/
1701| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
1702  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
1703| % [ /2/
1704    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
1705      @(soundly_labelled_state_step … EV) /2/
1706    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1707      @wr_call //
1708      @(will_return_prepend … TERMINATES … TM1)
1709      cases (terminates … tlr) //
1710    | @(will_return_not_wrong … TERMINATES)
1711      [ @(still_not_wrong … EV) /2/
1712      | cases (terminates … tlr) //
1713      ]
1714    | (* By stack preservation we cannot be in the final state *)
1715      inversion (stack_ok … tlr)
1716      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1717      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1718      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct
1719        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
1720        inversion (eval_preserves … EV)
1721        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 -TRACE_OK destruct ]
1722        #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1723        inversion S
1724        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
1725        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1726           so we can use it as a witness that at least one frame exists *)
1727        inversion LABEL_LIMIT
1728        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1729      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1730      ]
1731    ]
1732| @(well_cost_labelled_state_step … EV) /2/
1733| @(well_cost_labelled_call … EV) /2/
1734| /2/
1735| % [ @(well_cost_labelled_state_step … EV) /2/
1736    | @(soundly_labelled_state_step … EV) /2/
1737    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1738      @(will_return_lower … TM) //
1739    | @(still_not_wrong … EV) /2/
1740    | @(not_return_to_not_final … EV) >CL % #E destruct
1741    ]
1742| 19,20,21: /2/
1743| cases (bound_after_step … LABEL_LIMIT EV ?)
1744  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
1745    inversion trace'
1746    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1747      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1748      % >CL #E destruct
1749    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1750      @wr_base //
1751    | #H99 #H100 #H101 #H102 #H103 -TRACE_OK' destruct
1752      inversion (ro_not_undefined … TRACE_OK)
1753      [ #H137 #H138 #H139 #H140 #H141 destruct
1754      | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 destruct
1755        inversion H148
1756        [ #H153 #H154 #H155 #H156 #H157 destruct
1757        | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct
1758        ]
1759      ]
1760    ]
1761    ]
1762    | >CL #E destruct
1763    ]
1764  | //
1765  | //
1766  ]
1767| % [ @(well_cost_labelled_state_step … EV) /2/
1768    | @(soundly_labelled_state_step … EV) /2/
1769    | @(not_to_not … (ro_no_termination … TRACE_OK))
1770      * #depth * #TERM %{depth} % @wr_step /2/
1771    | @(still_not_wrong … (ro_not_undefined … TRACE_OK))
1772    | @(not_return_to_not_final … EV) >CL % #E destruct
1773    ]
1774| inversion (ro_not_undefined … TRACE_OK)
1775  [ #H169 #H170 #H171 #H172 #H173 destruct
1776  | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
1777  ]
1778] qed.
1779
1780(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1781       a trace_label_diverges value, but I only know how to construct those
1782       using a cofixpoint in Type[0], which means I can't use the termination
1783       oracle.
1784*)
1785
1786let corec make_label_diverges ge s
1787  (trace: flat_trace io_out io_in ge s)
1788  (ORACLE: termination_oracle)
1789  (TRACE_OK: remainder_ok ge s trace)
1790  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1791  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1792  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1793  : trace_label_diverges_exists (RTLabs_status ge) s ≝
1794match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
1795[ ex_intro n B ⇒
1796    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
1797      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1798    with
1799    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1800        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1801            tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) T'
1802(*
1803        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1804        [ ex_intro T' _ ⇒
1805            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1806        ]*)
1807    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1808        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1809            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) ?? T'
1810(*
1811        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1812        [ ex_intro T' _ ⇒
1813            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1814        ]*)
1815    ] STATEMENT_COSTLABEL
1816].
1817[ @(costed_RTLabs ge) @(trace_any_label_label … T)
1818| %{tr} @EV
1819| @(trace_any_call_call … T)
1820| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
1821] qed.
1822
1823lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'.
1824  make_initial_state p = OK ? s1 →
1825  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
1826  stack_preserved ends_with_ret s2 s' →
1827  RTLabs_is_final s' ≠ None ?.
1828#ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?);
1829@bind_ok #m #_
1830@bind_ok #b #_
1831@bind_ok #f #_
1832#E destruct
1833#EV #SP inversion (eval_preserves … EV)
1834[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
1835     inversion SP
1836     [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct
1837     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct
1838          inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct
1839     ]
1840| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct
1841] qed.
1842
1843lemma initial_state_is_call : ∀p,s.
1844  make_initial_state p = OK ? s →
1845  RTLabs_classify s = cl_call.
1846#p #s whd in ⊢ (??%? → ?);
1847@bind_ok #m #_
1848@bind_ok #b #_
1849@bind_ok #f #_
1850#E destruct
1851@refl
1852qed.
1853
1854let rec whole_structured_trace_exists ge p s
1855  (trace: flat_trace io_out io_in ge s)
1856  (ORACLE: termination_oracle)
1857  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1858  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1859  : ∀INITIAL: make_initial_state p = OK ? s.
1860    ∀NOT_WRONG: not_wrong ??? s trace.
1861    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
1862    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
1863    trace_whole_program_exists (RTLabs_status ge) s ≝
1864match trace return λs,trace. make_initial_state p = OK ? s →
1865                             not_wrong ??? s trace →
1866                             well_cost_labelled_state s →
1867                             soundly_labelled_state s →
1868                             trace_whole_program_exists (RTLabs_status ge) s with
1869[ ft_step s tr next EV trace' ⇒ λINITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
1870    let IS_CALL ≝ initial_state_is_call … INITIAL in
1871    match ORACLE ge O next trace' with
1872    [ or_introl TERMINATES ⇒
1873        match TERMINATES with
1874        [ witness TERMINATES ⇒
1875          let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1876          twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
1877        ]
1878    | or_intror NO_TERMINATION ⇒
1879        twp_diverges (RTLabs_status ge) s next IS_CALL ?
1880         (make_label_diverges ge next trace' ORACLE ?
1881            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1882    ]
1883| ft_stop st FINAL ⇒ λINITIAL,NOT_WRONG. ⊥
1884| ft_wrong start m NF EV ⇒ λINITIAL,NOT_WRONG. ⊥
1885].
1886[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
1887  cases FINAL #E @E @refl
1888| %{tr} @EV
1889| @(after_the_initial_call_is_the_final_state … INITIAL EV)
1890  @(stack_ok … tlr)
1891| @(well_cost_labelled_state_step … EV) //
1892| @(well_cost_labelled_call … EV) //
1893| %{tr} @EV
1894| @(well_cost_labelled_call … EV) //
1895| % [ @(well_cost_labelled_state_step … EV) //
1896    | @(soundly_labelled_state_step … EV) //
1897    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1898    | @(still_not_wrong … NOT_WRONG)
1899    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1900    ]
1901| inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
1902] qed.
1903
1904definition well_cost_labelled_program : RTLabs_program → Prop ≝
1905  λp. All ? (λx. let 〈id,fd〉 ≝ x in
1906                 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
1907(*
1908theorem program_trace_exists :
1909  termination_oracle →
1910  ∀p:RTLabs_program.
1911  ∀s:state.
1912  ∀I: make_initial_state p = OK ? s.
1913 
1914  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1915 
1916  ∀NOIO:exec_no_io … plain_trace.
1917 
1918  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
1919 
1920  trace_whole_program_exists (RTLabs_status (make_global p)) s.
1921#ORACLE #p #s #I
1922letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1923#NOIO
1924letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
1925whd
1926@(whole_structured_trace_exists … flat_trace)
1927//
1928[ whd
1929*)
1930
1931(* as_execute might be in Prop, but because the semantics is deterministic
1932   we can retrieve the event trace anyway. *)
1933let rec deprop_as_execute ge s s'
1934  (X:as_execute (RTLabs_status ge) s s')
1935: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1936match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ? with
1937[ Value ts ⇒ λY. «fst … ts, ?»
1938| _ ⇒ λY. ⊥
1939] X.
1940[ 1,3: cases Y #x #E destruct
1941| cases Y #trP #E destruct @refl
1942] qed.
1943
1944(* A non-empty finite section of a flat_trace *)
1945inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1946| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1947| 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''.
1948
1949let rec append_partial_flat_trace o i ge s1 s2 s3
1950  (tr1:partial_flat_trace o i ge s1 s2)
1951on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1952match tr1 with
1953[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1954| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1955].
1956
1957let rec partial_to_flat_trace o i ge s1 s2
1958  (tr:partial_flat_trace o i ge s1 s2)
1959on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1960match tr with
1961[ pft_base s tr s' EX ⇒ ft_step … EX
1962| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1963].
1964
1965(* Extract a flat trace from a structured one. *)
1966let rec flat_trace_of_label_return ge s s'
1967  (tr:trace_label_return (RTLabs_status ge) s s')
1968on tr :
1969  partial_flat_trace io_out io_in ge s s' ≝
1970match tr with
1971[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
1972| tlr_step s1 s2 s3 tll tlr ⇒
1973  append_partial_flat_trace …
1974    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
1975    (flat_trace_of_label_return ge s2 s3 tlr)
1976]
1977and flat_trace_of_label_label ge ends s s'
1978  (tr:trace_label_label (RTLabs_status ge) ends s s')
1979on tr :
1980  partial_flat_trace io_out io_in ge s s' ≝
1981match tr with
1982[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
1983]
1984and flat_trace_of_any_label ge ends s s'
1985  (tr:trace_any_label (RTLabs_status ge) ends s s')
1986on tr :
1987  partial_flat_trace io_out io_in ge s s' ≝
1988match tr with
1989[ tal_base_not_return s1 s2 EX CL CS ⇒
1990    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1991    pft_base … EX' ]
1992| tal_base_return s1 s2 EX CL ⇒
1993    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1994    pft_base … EX' ]
1995| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
1996    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
1997    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
1998    pft_step … EX' suffix' ]
1999| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
2000    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2001    pft_step … EX'
2002      (append_partial_flat_trace …
2003        (flat_trace_of_label_return ge ?? tlr)
2004        (flat_trace_of_any_label ge ??? tal))
2005    ]
2006| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
2007    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2008      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
2009    ]
2010].
2011
2012
2013(* We take an extra step so that we can always return a non-empty trace to
2014   satisfy the guardedness condition in the cofixpoint. *)
2015let rec flat_trace_of_any_call ge s s' s'' et
2016  (tr:trace_any_call (RTLabs_status ge) s s')
2017  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2018on tr :
2019  partial_flat_trace io_out io_in ge s s'' ≝
2020match tr return λs,s'.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
2021[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
2022| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
2023    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
2024    pft_step … EX'
2025      (append_partial_flat_trace …
2026        (flat_trace_of_label_return ge ?? tlr)
2027        (flat_trace_of_any_call ge … tac EX''))
2028    ]
2029| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
2030    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2031    pft_step … EX'
2032     (flat_trace_of_any_call ge … tal EX'')
2033    ]
2034] EX''.
2035
2036let rec flat_trace_of_label_call ge s s' s'' et
2037  (tr:trace_label_call (RTLabs_status ge) s s')
2038  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2039on tr :
2040  partial_flat_trace io_out io_in ge s s'' ≝
2041match tr with
2042[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
2043] EX''.
2044
2045(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
2046   to take care to satisfy the guardedness condition by witnessing the fact that
2047   the partial traces are non-empty. *)
2048let corec flat_trace_of_label_diverges ge s
2049  (tr:trace_label_diverges (RTLabs_status ge) s)
2050: flat_trace io_out io_in ge s ≝
2051match tr with
2052[ tld_step sx sy tll tld ⇒
2053    match flat_trace_of_label_label ge … tll with
2054    [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2055    | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
2056    ] tld
2057| tld_base s1 s2 s3 tlc EX CL tld ⇒
2058    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2059      match flat_trace_of_label_call … tlc EX' with
2060      [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2061      | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
2062      ] tld
2063    ]
2064]
2065(* Helper to keep adding the partial trace without violating the guardedness
2066   condition. *)
2067and add_partial_flat_trace ge s s'
2068  (ptr:partial_flat_trace io_out io_in ge s s')
2069  (tr:trace_label_diverges (RTLabs_status ge) s')
2070: flat_trace io_out io_in ge s ≝
2071match ptr with
2072[ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr)
2073| pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr)
2074] tr
2075.
2076
2077coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2078| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2079| 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)
2080| eft_wrong : ∀s,m,NF,EX. equal_flat_traces ge s (ft_wrong … s m NF EX) (ft_wrong … s m NF EX).
2081
2082(* XXX move to semantics *)
2083lemma final_cannot_move : ∀ge,s.
2084  RTLabs_is_final s ≠ None ? →
2085  ∃err. eval_statement ge s = Wrong ??? err.
2086#ge *
2087[ #f #fs #m * #F cases (F ?) @refl
2088| #a #b #c #d #e * #F cases (F ?) @refl
2089| #a #b #c #d * #F cases (F ?) @refl
2090| #r #F % [2: @refl | skip ]
2091] qed.
2092
2093let corec flat_traces_are_determined_by_starting_point ge s tr1
2094: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2095match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2096[ ft_stop s F ⇒ λtr2. ?
2097| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2098    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2099    [ ft_stop s F ⇒ λEX. ?
2100    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2101    | ft_wrong s m NF EX' ⇒ λEX. ?
2102    ] EX0
2103| ft_wrong s m NF EX ⇒ λtr2. ?
2104].
2105[ inversion tr2 in tr1 F;
2106  [ #s #F #_ #_ #tr1 #F' @eft_stop
2107  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2108    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2109  | #s #m #NF #EX #_ #_ #_ #F @⊥ >NF in F; * /2/
2110  ]
2111| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2112| -EX0
2113  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2114  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2115  -E -EX' -tr2' #tr2' #EX'
2116  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2117  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2118  -E -EX' #EX'
2119    @eft_step @flat_traces_are_determined_by_starting_point
2120| @⊥ >EX in EX'; #E destruct
2121| inversion tr2 in NF EX;
2122  [ #s #F #_ #_ #NF @⊥ >NF in F; * /2/
2123  | #s1 #tr #s2 #EX #tr1 #E1 #_ #NF #EX' @⊥ >EX in EX'; #E destruct
2124  | #sx #m' #NF #EX #_ #_ #NF' #EX' cut (m=m'). >EX in EX'; #E destruct @refl.
2125    #E destruct
2126    @eft_wrong
2127  ]
2128] qed.
2129
2130let corec diverging_traces_have_unique_flat_trace ge s
2131  (str:trace_label_diverges (RTLabs_status ge) s)
2132  (tr:flat_trace io_out io_in ge s)
2133: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
2134@flat_traces_are_determined_by_starting_point
2135qed.
2136
2137let rec flat_trace_of_whole_program ge s
2138  (tr:trace_whole_program (RTLabs_status ge) s)
2139on tr : flat_trace io_out io_in ge s ≝
2140match tr with
2141[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2142    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2143      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sf F))
2144    ]
2145| twp_diverges s1 s2 CL EX tld ⇒
2146    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2147      ft_step … EX' (flat_trace_of_label_diverges … tld)
2148    ]
2149].
2150
2151let corec whole_traces_have_unique_flat_trace ge s
2152  (str:trace_whole_program (RTLabs_status ge) s)
2153  (tr:flat_trace io_out io_in ge s)
2154: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
2155@flat_traces_are_determined_by_starting_point
2156qed.
Note: See TracBrowser for help on using the repository browser.