source: src/RTLabs/Traces.ma @ 1705

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

Checkpoint RTLabs labelling soundness work.

File size: 58.4 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].
21
22definition is_cost_label : statement → bool ≝
23λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
24
25definition RTLabs_cost : state → bool ≝
26λs. match s with
27[ State f fs m ⇒
28    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
29| _ ⇒ false
30].
31
32definition RTLabs_status : genv → abstract_status ≝
33λge.
34  mk_abstract_status
35    state
36    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
37    (λs,c. RTLabs_classify s = c)
38    (λs. RTLabs_cost s = true)
39    (λs,s'. match s with
40      [ mk_Sig s p ⇒
41        match s return λs. RTLabs_classify s = cl_call → ? with
42        [ Callstate fd args dst stk m ⇒
43          λ_. match s' with
44          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
45          | _ ⇒ False
46          ]
47        | State f fs m ⇒ λH.⊥
48        | _ ⇒ λH.⊥
49        ] p
50      ]).
51[ normalize in H; destruct
52| whd in H:(??%?);
53  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
54  normalize try #a try #b try #c try #d try #e try #g try #h destruct
55] qed.
56
57lemma RTLabs_not_cost : ∀ge,s.
58  RTLabs_cost s = false →
59  ¬ as_costed (RTLabs_status ge) s.
60#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
61qed.
62
63(* Before attempting to construct a structured trace, let's show that we can
64   form flat traces with evidence that they were constructed from an execution.
65   
66   For now we don't consider I/O. *)
67
68
69coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
70| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
71| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
72| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
73
74(* add I/O? *)
75coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
76| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
77| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
78| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
79
80let corec make_flat_trace ge s
81  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
82  flat_trace io_out io_in ge s ≝
83let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
84match e return λx. e = x → ? with
85[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
86| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
87| e_wrong m ⇒ λE. ft_wrong … s m ?
88| e_interact o f ⇒ λE. ⊥
89] (refl ? e).
90[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
91  cases (eval_statement ge s)
92  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
93  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
94    >(?:is_final ????? = RTLabs_is_final s1) //
95    lapply (refl ? (RTLabs_is_final s1))
96    cases (RTLabs_is_final s1) in ⊢ (???% → %);
97    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
98    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
99    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
100    ]
101  | *: #m whd in ⊢ (??%? → ?); #E destruct
102  ]
103| whd in E:(??%?); >exec_inf_aux_unfold in E;
104  cases (eval_statement ge s)
105  [ #O #K whd in ⊢ (??%? → ?); #E destruct
106  | * #tr #s1 whd in ⊢ (??%? → ?);
107    cases (is_final ?????)
108    [ whd in ⊢ (??%? → ?); #E destruct @refl
109    | #i whd in ⊢ (??%? → ?); #E destruct
110    ]
111  | #m whd in ⊢ (??%? → ?); #E destruct
112  ]
113| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
114  cases (eval_statement ge s)
115  [ #O #K whd in ⊢ (??%? → ?); #E destruct
116  | * #tr #s1 whd in ⊢ (??%? → ?);
117    cases (is_final ?????)
118    [ whd in ⊢ (??%? → ?); #E
119      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
120      destruct
121      inversion H
122      [ #a #b #c #E1 destruct
123      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
124      | #m #E1 destruct
125      ]
126    | #i whd in ⊢ (??%? → ?); #E destruct
127    ]
128  | #m whd in ⊢ (??%? → ?); #E destruct
129  ]
130| whd in E:(??%?); >exec_inf_aux_unfold in E;
131  cases (eval_statement ge s)
132  [ #O #K whd in ⊢ (??%? → ?); #E destruct
133  | * #tr1 #s1 whd in ⊢ (??%? → ?);
134    cases (is_final ?????)
135    [ whd in ⊢ (??%? → ?); #E destruct
136    | #i whd in ⊢ (??%? → ?); #E destruct
137    ]
138  | #m whd in ⊢ (??%? → ?); #E destruct @refl
139  ]
140| whd in E:(??%?); >E in H; #H
141  inversion H
142  [ #a #b #c #E destruct
143  | #a #b #c #d #E1 destruct
144  | #m #E1 destruct
145  ]
146] qed.
147
148let corec make_whole_flat_trace p s
149  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
150  (I:make_initial_state ??? p = OK ? s) :
151  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
152let ge ≝ make_global … p in
153let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
154match e return λx. e = x → ? with
155[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
156| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
157| e_wrong m ⇒ λE. ⊥
158| e_interact o f ⇒ λE. ⊥
159] (refl ? e).
160[ whd in E:(??%?); >exec_inf_aux_unfold in E;
161  whd in ⊢ (??%? → ?);
162  >(?:is_final ????? = RTLabs_is_final s) //
163  lapply (refl ? (RTLabs_is_final s))
164  cases (RTLabs_is_final s) in ⊢ (???% → %);
165  [ #_ whd in ⊢ (??%? → ?); #E destruct
166  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
167  ]
168| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
169  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
170  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
171    [ #a #b #c #E1 destruct
172    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
173      @H1
174    | #m #E1 destruct
175    ]
176  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
177  ]
178| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
179  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
180| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
181  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
182] qed.
183
184(* Need a way to choose whether a called function terminates.  Then,
185     if the initial function terminates we generate a purely inductive structured trace,
186     otherwise we start generating the coinductive one, and on every function call
187       use the choice method again to decide whether to step over or keep going.
188
189Not quite what we need - have to decide on seeing each label whether we will see
190another or hit a non-terminating call?
191
192Also - need the notion of well-labelled in order to break loops.
193
194
195
196outline:
197
198 does function terminate?
199 - yes, get (bound on the number of steps until return), generate finite
200        structure using bound as termination witness
201 - no,  get (¬ bound on steps to return), start building infinite trace out of
202        finite steps.  At calls, check for termination, generate appr. form.
203
204generating the finite parts:
205
206We start with the status after the call has been executed; well-labelling tells
207us that this is a labelled state.  Now we want to generate a trace_label_return
208and also return the remainder of the flat trace.
209
210*)
211
212(* [will_return ge depth s trace] says that after a finite number of steps of
213   [trace] from [s] we reach the return state for the current function.  [depth]
214   performs the call/return counting necessary for handling deeper function
215   calls.  It should be zero at the top level. *)
216inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
217| wr_step : ∀s,tr,s',depth,EX,trace.
218    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
219    will_return ge depth s' trace →
220    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
221| wr_call : ∀s,tr,s',depth,EX,trace.
222    RTLabs_classify s = cl_call →
223    will_return ge (S depth) s' trace →
224    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
225| wr_ret : ∀s,tr,s',depth,EX,trace.
226    RTLabs_classify s = cl_return →
227    will_return ge depth s' trace →
228    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
229    (* Note that we require the ability to make a step after the return (this
230       corresponds to somewhere that will be guaranteed to be a label at the
231       end of the compilation chain). *)
232| wr_base : ∀s,tr,s',EX,trace.
233    RTLabs_classify s = cl_return →
234    will_return ge O s (ft_step ?? ge s tr s' EX trace)
235.
236
237(* The way we will use [will_return] won't satisfy Matita's guardedness check,
238   so we will measure the length of these termination proofs and use an upper
239   bound to show termination of the finite structured trace construction
240   functions. *)
241
242let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
243match T with
244[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
245| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
246| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
247| wr_base _ _ _ _ _ _ ⇒ S O
248].
249
250include alias "arithmetics/nat.ma".
251
252(* Specialised to the particular situation it is used in. *)
253lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
254#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
255whd in ⊢ (??(??%) → ?);
256>commutative_times
257#H lapply (le_plus_b … H)
258#H lapply (le_to_leb_true … H)
259normalize #E destruct
260qed.
261
262(* Inversion lemmas on [will_return] that also note the effect on the length
263   of the proof. *)
264lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
265  RTLabs_classify s = cl_call →
266  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
267  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
268#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
269[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
270| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
271| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
272| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
273] qed.
274
275lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
276  RTLabs_classify s = cl_return →
277  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
278  match d with
279  [ O ⇒ True
280  | S d' ⇒
281      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
282  ].
283#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
284[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
285| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
286| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
287| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
288] qed.
289
290lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
291  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
292  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
293  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
294#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
295[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
296| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
297| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
298| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
299| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
300| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
301| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
302| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
303] qed.
304
305(* We require that labels appear after branch instructions and at the start of
306   functions.  The first is required for preciseness, the latter for soundness.
307   We will make a separate requirement for there to be a finite number of steps
308   between labels to catch loops for soundness (is this sufficient?). *)
309
310definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
311λf,s. match s return λs. labels_present ? s → Prop with
312[ St_cond _ l1 l2 ⇒ λH.
313    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
314    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
315| St_jumptable _ ls ⇒ λH.
316    (* I did have a dependent version of All here, but it's a pain. *)
317    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
318| _ ⇒ λ_. True
319]. whd in H;
320[ @(proj1 … H)
321| @(proj2 … H)
322] qed.
323
324definition well_cost_labelled_fn : internal_function → Prop ≝
325λf. (∀l. ∀H:present … (f_graph f) l.
326         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
327    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
328[ @lookup_lookup_present | cases (f_entry f) // ] qed.
329
330(* We need to ensure that any code we come across is well-cost-labelled.  We may
331   get function code from either the global environment or the state. *)
332
333definition well_cost_labelled_ge : genv → Prop ≝
334λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
335
336definition well_cost_labelled_state : state → Prop ≝
337λs. match s with
338[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
339| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
340                          All ? (λf. well_cost_labelled_fn (func f)) fs
341| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
342].
343
344lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
345  eval_statement ge s = Value ??? 〈tr,s'〉 →
346  well_cost_labelled_ge ge →
347  well_cost_labelled_state s →
348  well_cost_labelled_state s'.
349#ge #s #tr' #s' #EV cases (eval_perserves … EV)
350[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
351| #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/
352(*
353| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
354*)
355| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
356| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
357| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
358] qed.
359
360lemma rtlabs_jump_inv : ∀s.
361  RTLabs_classify s = cl_jump →
362  ∃f,fs,m. s = State f fs m ∧
363  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
364  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
365*
366[ #f #fs #m #E
367  %{f} %{fs} %{m} %
368  [ @refl
369  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
370    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
371    [ %1 %{A} %{B} %{C} @refl
372    | %2 %{A} %{B} @refl
373    ]
374  ]
375| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
376| normalize #H8 #H9 #H10 #H11 #H12 destruct
377] qed.
378
379lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
380  eval_statement ge s = Value ??? 〈tr,s'〉 →
381  well_cost_labelled_state s →
382  RTLabs_classify s = cl_jump →
383  RTLabs_cost s' = true.
384#ge #s #tr #s' #EV #H #CL
385cases (rtlabs_jump_inv s CL)
386#fr * #fs * #m * #Es *
387[ * #r * #l1 * #l2 #Estmt
388  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
389  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
390  >Estmt #LP whd in ⊢ (??%? → ?);
391  (* replace with lemma on successors? *)
392  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
393  lapply (Hbody (next fr) (next_ok fr))
394  generalize in ⊢ (???% → ?);
395  >Estmt #LP'
396  whd in ⊢ (% → ?);
397  * #H1 #H2 [ @H1 | @H2 ]
398| * #r * #ls #Estmt
399  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
400  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
401  >Estmt #LP whd in ⊢ (??%? → ?);
402  (* replace with lemma on successors? *)
403  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
404  [ 2: (* later *)
405  | *: #E destruct
406  ]
407  lapply (Hbody (next fr) (next_ok fr))
408  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
409  generalize in ⊢ (??(?%)? → ?);
410  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
411  [ #E1 #E2 whd in E2:(??%?); destruct
412  | #l' #E1 #E2 whd in E2:(??%?); destruct
413    cases (All_nth ???? CP ? E1)
414    #H1 #H2 @H2
415  ]
416] qed.
417
418lemma rtlabs_call_inv : ∀s.
419  RTLabs_classify s = cl_call →
420  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
421* [ #f #fs #m whd in ⊢ (??%? → ?);
422    cases (lookup_present … (next f) (next_ok f)) normalize
423    try #A try #B try #C try #D try #E try #F try #G destruct
424  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
425  | normalize #H411 #H412 #H413 #H414 #H415 destruct
426  ] qed.
427
428lemma well_cost_labelled_call : ∀ge,s,tr,s'.
429  eval_statement ge s = Value ??? 〈tr,s'〉 →
430  well_cost_labelled_state s →
431  RTLabs_classify s = cl_call →
432  RTLabs_cost s' = true.
433#ge #s #tr #s' #EV #WCL #CL
434cases (rtlabs_call_inv s CL)
435#fd * #args * #dst * #stk * #m #E >E in EV WCL;
436whd in ⊢ (??%? → % → ?);
437cases fd
438[ #fn whd in ⊢ (??%? → % → ?);
439  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
440  #m' #b whd in ⊢ (??%? → ?); #E' destruct
441  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
442  @WCL2
443| #fn whd in ⊢ (??%? → % → ?);
444  @bindIO_value #evargs #Eargs
445  whd in ⊢ (??%? → ?);
446  #E' destruct
447] qed.
448
449
450(* The preservation of (most of) the stack is useful to show as_after_return.
451   We do this by showing that during the execution of a function the lower stack
452   frames never change, and that after returning from the function we preserve
453   the identity of the next instruction to execute.
454 *)
455
456inductive stack_of_state : list frame → state → Prop ≝
457| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
458| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
459| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
460.
461
462inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
463| sp_normal : ∀fs,s1,s2.
464    stack_of_state fs s1 →
465    stack_of_state fs s2 →
466    stack_preserved doesnt_end_with_ret s1 s2
467| sp_finished : ∀s1,f,f',fs,m.
468    next f = next f' →
469    stack_of_state (f::fs) s1 →
470    stack_preserved ends_with_ret s1 (State f' fs m).
471
472discriminator list.
473
474lemma stack_of_state_eq : ∀fs,fs',s.
475  stack_of_state fs s →
476  stack_of_state fs' s →
477  fs = fs'.
478#fs0 #fs0' #s0 *
479[ #f #fs #m #H inversion H
480  #a #b #c #d #e #g try #h try #i try #j destruct @refl
481| #fd #args #dst #f #fs #m #H inversion H
482  #a #b #c #d #e #g try #h try #i try #j destruct @refl
483| #rtv #dst #fs #m #H inversion H
484  #a #b #c #d #e #g try #h try #i try #j destruct @refl
485] qed.
486
487lemma stack_preserved_join : ∀e,s1,s2,s3.
488  stack_preserved doesnt_end_with_ret s1 s2 →
489  stack_preserved e s2 s3 →
490  stack_preserved e s1 s3.
491#e1 #s1 #s2 #s3 #H1 inversion H1
492[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
493  #H2 inversion H2
494  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
495    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
496  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
497    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
498  ]
499| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
500] qed.
501
502lemma stack_preserved_return : ∀ge,s1,s2,tr.
503  RTLabs_classify s1 = cl_return →
504  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
505  stack_preserved ends_with_ret s1 s2.
506#ge *
507[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
508  cases (lookup_present ??? (next f) (next_ok f)) in E;
509  normalize #a try #b try #c try #d try #e try #f try #g destruct
510| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
511| #res #dst *
512  [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct
513  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
514    whd in EV:(??%?); destruct @(sp_finished ? f) //
515  ]
516] qed.
517
518lemma stack_preserved_step : ∀ge,s1,s2,tr.
519  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
520  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
521  stack_preserved doesnt_end_with_ret s1 s2.
522#ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV)
523[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
524| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
525| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
526  normalize in CL; cases CL #E destruct
527| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
528| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
529  #E normalize in E; destruct
530] qed.
531
532lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
533  RTLabs_classify s1 = cl_call →
534  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
535  stack_preserved ends_with_ret s2 s3 →
536  stack_preserved doesnt_end_with_ret s1 s3.
537#ge #s1 #s2 #s3 #tr #CL #EV #SP
538cases (rtlabs_call_inv … CL)
539#fd * #args * #dst * #stk * #m #E destruct
540inversion SP
541[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
542| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
543  inversion (eval_perserves … EV)
544  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
545  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
546  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
547    inversion S
548    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
549    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
550    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
551    ]
552  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
553  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
554  ]
555] qed.
556 
557lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr.
558  ∀CL : RTLabs_classify s1 = cl_call.
559  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
560  stack_preserved ends_with_ret s2 s3 →
561  as_after_return (RTLabs_status ge) «s1,CL» s3.
562#ge #s1 #s2 #s3 #tr #CL #EV #S23
563cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
564inversion S23
565[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
566| #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
567  inversion (eval_perserves … EV)
568  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
569  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
570  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
571    inversion S
572    [ #fy #fsy #my #E1 #E2 #E3 destruct @N
573    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
574    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
575    ]
576  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
577  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
578  ]
579] qed.
580
581(* Don't need to know that labels break loops because we have termination. *)
582
583(* A bit of mucking around with the depth to avoid proving termination after
584   termination.  Note that we keep a proof that our upper bound on the length
585   of the termination proof is respected. *)
586record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
587  new_state : state;
588  remainder : flat_trace io_out io_in ge new_state;
589  cost_labelled : well_cost_labelled_state new_state;
590  new_trace : T new_state;
591  stack_ok : stack_preserved ends start new_state;
592  terminates : match depth with
593               [ O ⇒ True
594               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
595               ]
596}.
597
598(* The same with a flag indicating whether the function returned, as opposed to
599   encountering a label. *)
600record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
601  ends : trace_ends_with_ret;
602  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start (T ends) limit
603}.
604
605(* We often return the result from a recursive call with an addition to the
606   structured trace, so we define a couple of functions to help.  The bound on
607   the size of the termination proof might need to be relaxed, too. *)
608
609definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
610  ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝
611λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
612  mk_trace_result ge d e2 s2 T2 l2
613    (new_state … r)
614    (remainder … r)
615    (cost_labelled … r)
616    trace
617    SP
618    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
619                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
620     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r))
621. @(transitive_le … lGE) @(pi2 … TM) qed.
622
623definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
624  ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝
625λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
626  mk_sub_trace_result ge d s2 T2 l2
627    (ends … r)
628    (replace_trace … lGE … r trace SP).
629
630(* Small syntax hack to avoid ambiguous input problems. *)
631definition myge : nat → nat → Prop ≝ ge.
632
633let rec make_label_return ge depth s
634  (trace: flat_trace io_out io_in ge s)
635  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
636  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
637  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
638  (TERMINATES: will_return ge depth s trace)
639  (TIME: nat)
640  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
641  on TIME : trace_result ge depth ends_with_ret s
642              (trace_label_return (RTLabs_status ge) s)
643              (will_return_length … TERMINATES) ≝
644             
645match TIME return λTIME. TIME ≥ ? → ? with
646[ O ⇒ λTERMINATES_IN_TIME. ⊥
647| S TIME ⇒ λTERMINATES_IN_TIME.
648
649  let r ≝ make_label_label ge depth s
650            trace
651            ENV_COSTLABELLED
652            STATE_COSTLABELLED
653            STATEMENT_COSTLABEL
654            TERMINATES
655            TIME ? in
656  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
657  [ ends_with_ret ⇒ λr.
658      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
659  | doesnt_end_with_ret ⇒ λr.
660      let r' ≝ make_label_return ge depth (new_state … r)
661                 (remainder … r)
662                 ENV_COSTLABELLED
663                 (cost_labelled … r) ?
664                 (pi1 … (terminates … r)) TIME ? in
665        replace_trace … r'
666          (tlr_step (RTLabs_status ge) s (new_state … r)
667            (new_state … r') (new_trace … r) (new_trace … r')) ?
668  ] (trace_res … r)
669
670] TERMINATES_IN_TIME
671
672
673and make_label_label ge depth s
674  (trace: flat_trace io_out io_in ge s)
675  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
676  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
677  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
678  (TERMINATES: will_return ge depth s trace)
679  (TIME: nat)
680  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
681  on TIME : sub_trace_result ge depth s
682              (λends. trace_label_label (RTLabs_status ge) ends s)
683              (will_return_length … TERMINATES) ≝
684             
685match TIME return λTIME. TIME ≥ ? → ? with
686[ O ⇒ λTERMINATES_IN_TIME. ⊥
687| S TIME ⇒ λTERMINATES_IN_TIME.
688
689let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
690  replace_sub_trace … r
691    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
692
693] TERMINATES_IN_TIME
694
695
696and make_any_label ge depth s
697  (trace: flat_trace io_out io_in ge s)
698  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
699  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
700  (TERMINATES: will_return ge depth s trace)
701  (TIME: nat)
702  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
703  on TIME : sub_trace_result ge depth s
704              (λends. trace_any_label (RTLabs_status ge) ends s)
705              (will_return_length … TERMINATES) ≝
706
707match TIME return λTIME. TIME ≥ ? → ? with
708[ O ⇒ λTERMINATES_IN_TIME. ⊥
709| S TIME ⇒ λTERMINATES_IN_TIME.
710
711  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
712  [ ft_stop st FINAL ⇒
713      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
714
715  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
716    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
717    [ cl_other ⇒ λCL.
718        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
719        (* We're about to run into a label. *)
720        [ true ⇒ λCS.
721            mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
722              doesnt_end_with_ret
723              (mk_trace_result ge … next trace' ?
724                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
725        (* An ordinary step, keep going. *)
726        | false ⇒ λCS.
727            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
728                replace_sub_trace … r
729                  (tal_step_default (RTLabs_status ge) (ends … r)
730                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
731        ] (refl ??)
732       
733    | cl_jump ⇒ λCL.
734        mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
735          doesnt_end_with_ret
736          (mk_trace_result ge ????? next trace' ?
737            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
738           
739    | cl_call ⇒ λCL.
740        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
741        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
742        (* We're about to run into a label, use base case for call *)
743        [ true ⇒ λCS.
744            mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
745            doesnt_end_with_ret
746            (replace_trace … r
747              (tal_base_call (RTLabs_status ge) start next (new_state … r)
748                ? CL ? (new_trace … r) CS) ?)
749        (* otherwise use step case *)
750        | false ⇒ λCS.
751            let r' ≝ make_any_label ge depth
752                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
753                       (pi1 … (terminates … r)) TIME ? in
754            replace_sub_trace … r'
755              (tal_step_call (RTLabs_status ge) (ends … r')
756                start next (new_state … r) (new_state … r') ? CL ?
757                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
758        ] (refl ??)
759
760    | cl_return ⇒ λCL.
761        mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
762          ends_with_ret
763          (mk_trace_result ge ?????
764            next
765            trace'
766            ?
767            (tal_base_return (RTLabs_status ge) start next ? CL)
768            ?
769            ?)
770    ] (refl ? (RTLabs_classify start))
771   
772  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
773 
774  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
775] TERMINATES_IN_TIME.
776
777[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
778| //
779| cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le
780| @(stack_preserved_join … (stack_ok … r)) //
781| @(trace_label_label_label … (new_trace … r))
782| cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT
783  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
784  @(transitive_le …  (3*(will_return_length … TERMINATES)))
785  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
786    @(monotonic_le_times_r 3 … LT)
787  | @le_S @le_S @le_n
788  ]
789| @le_S_S_to_le @TERMINATES_IN_TIME
790| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
791| @le_n
792| @le_S_S_to_le @TERMINATES_IN_TIME
793| @(wrl_nonzero … TERMINATES_IN_TIME)
794| (* Bad - we've reached the end of the trace; need to fix semantics so that
795     this can't happen *)
796| @(will_return_return … CL TERMINATES)
797| /2 by stack_preserved_return/
798| %{tr} @EV
799| @(well_cost_labelled_state_step  … EV) //
800| whd @(will_return_notfn … TERMINATES) %2 @CL
801| @stack_preserved_step /2/
802| %{tr} @EV
803| %1 whd @CL
804| @(well_cost_labelled_jump … EV) //
805| @(well_cost_labelled_state_step  … EV) //
806| @(stack_preserved_call … EV (stack_ok … r)) //
807| %{tr} @EV
808| @RTLabs_after_call //
809| cases (will_return_call … TERMINATES) #H @le_S_to_le
810| cases r #H1 #H2 #H3 #H4 #H5 * #H6
811  cases (will_return_call … CL TERMINATES)
812  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
813| @RTLabs_after_call //
814| %{tr} @EV
815| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
816| @(cost_labelled … r)
817| cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78
818  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
819  cases (will_return_call … TERMINATES) in H78;
820  #X #Y #Z
821  @(transitive_le … (monotonic_lt_times_r 3 … Y))
822  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
823  | //
824  ]
825| @(well_cost_labelled_state_step  … EV) //
826| @(well_cost_labelled_call … EV) //
827| skip
828| cases (will_return_call … TERMINATES)
829  #TM #GT @le_S_S_to_le
830  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
831  @(transitive_le … TERMINATES_IN_TIME)
832  @(monotonic_le_times_r 3 … GT)
833| whd @(will_return_notfn … TERMINATES) %1 @CL
834| @(stack_preserved_step … EV) /2/
835| %{tr} @EV
836| %2 whd @CL
837| @(well_cost_labelled_state_step  … EV) //
838| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
839| @CL
840| %{tr} @EV
841| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
842| @(well_cost_labelled_state_step  … EV) //
843| %1 @CL
844| cases (will_return_notfn … TERMINATES) #TM #GT
845  @le_S_S_to_le
846  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
847  //
848| inversion TERMINATES
849  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
850  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
851  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
852  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
853  ]
854] cases daemon qed.
855
856(* We can initialise TIME with a suitably large value based on the length of the
857   termination proof. *)
858let rec make_label_return' ge depth s
859  (trace: flat_trace io_out io_in ge s)
860  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
861  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
862  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
863  (TERMINATES: will_return ge depth s trace)
864  : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
865make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
866  (2 + 3 * will_return_length … TERMINATES) ?.
867@le_n
868qed.
869 
870(* FIXME: there's trouble at the end of the program because we can't make a step
871   away from the final return.
872   
873   We need to show that the "next pc" is preserved through a function call.
874   
875   Tail-calls are not handled properly (which means that if we try to show the
876   full version with non-termination we'll fail because calls and returns aren't
877   balanced.
878 *)
879
880inductive inhabited (T:Type[0]) : Prop ≝
881| witness : T → inhabited T.
882
883(* We also require that program's traces are soundly labelled: for any state
884   in the execution, we can give a distance to a labelled state or termination.
885   
886   Note that this differs from the syntactic notions in earlier languages
887   because it is a global property.  In principle, we would have a loop broken
888   only by a call to a function (which necessarily has a label) and no local
889   cost label.
890 *)
891
892let rec nth_state ge s
893  (trace: flat_trace io_out io_in ge s)
894  n
895  on n : option state ≝
896match n with
897[ O ⇒ Some ? s
898| S n' ⇒
899  match trace with
900  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
901  | _ ⇒ None ?
902  ]
903].
904
905definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
906λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
907
908lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
909  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
910  soundly_labelled_trace ge s' trace'.
911#ge #s #tr #s' #EV #trace' #H
912#n cases (H (S n)) #m #H' %{m} @H'
913qed.
914
915(* Define a notion of sound labellings of RTLabs programs. *)
916
917let rec successors (s : statement) : list label ≝
918match s with
919[ St_skip l ⇒ [l]
920| St_cost _ l ⇒ [l]
921| St_const _ _ l ⇒ [l]
922| St_op1 _ _ _ _ _ l ⇒ [l]
923| St_op2 _ _ _ _ l ⇒ [l]
924| St_load _ _ _ l ⇒ [l]
925| St_store _ _ _ l ⇒ [l]
926| St_call_id _ _ _ l ⇒ [l]
927| St_call_ptr _ _ _ l ⇒ [l]
928(*
929| St_tailcall_id _ _ ⇒ [ ]
930| St_tailcall_ptr _ _ ⇒ [ ]
931*)
932| St_cond _ l1 l2 ⇒ [l1; l2]
933| St_jumptable _ ls ⇒ ls
934| St_return ⇒ [ ]
935].
936
937definition actual_successor : state → option label ≝
938λs. match s with
939[ State f fs m ⇒ Some ? (next f)
940| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
941| Returnstate _ _ _ _ ⇒ None ?
942].
943
944lemma nth_opt_Exists : ∀A,n,l,a.
945  nth_opt A n l = Some A a →
946  Exists A (λa'. a' = a) l.
947#A #n elim n
948[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
949| #m #IH *
950  [ #a #E normalize in E; destruct
951  | #a #l #a' #E %2 @IH @E
952  ]
953] qed.
954
955lemma eval_successor : ∀ge,f,fs,m,tr,s'.
956  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
957  RTLabs_classify s' = cl_return ∨
958  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
959#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
960whd in ⊢ (??%? → ?);
961generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
962[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
963| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
964| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
965| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
966| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
967| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
968| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
969| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
970| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
971| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
972| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
973  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 ]
974  whd in ⊢ (??%? → ?);
975  generalize in ⊢ (??(?%)? → ?);
976  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
977  [ #e #E normalize in E; destruct
978  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
979  ]
980| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
981] qed.
982
983definition steps_for_statement : statement → nat ≝
984λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
985
986inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
987| stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n)
988| stlb_step : ∀l,n,H.
989    let stmt ≝ lookup_present … g l H in
990    (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) →
991    steps_to_label_bound g l (steps_for_statement stmt + n).
992   
993discriminator nat.
994
995lemma steps_to_label_bound_inv_step : ∀g,l,n.
996  steps_to_label_bound g l n →
997  ∀H.
998  let stmt ≝ lookup_present … g l H in
999  ¬ (bool_to_Prop (is_cost_label stmt)) →
1000  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1001    ∃n'. n = n' + steps_for_statement stmt ∧
1002          steps_to_label_bound g l' n').
1003#g #l0 #n0 #H1 inversion H1
1004[ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
1005| #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX
1006  % [2: % [ @commutative_plus | @IH // ] ]
1007] qed.
1008
1009definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1010
1011let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1012  soundly_labelled_pc (f_graph fn) (f_entry fn).
1013
1014
1015definition soundly_labelled_frame : frame → Prop ≝
1016λf. soundly_labelled_pc (f_graph (func f)) (next f).
1017
1018definition soundly_labelled_state : state → Prop ≝
1019λs. match s with
1020[ State f _ _ ⇒ soundly_labelled_frame f
1021| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1022| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1023].
1024
1025definition frame_steps_to_label_bound : frame → nat → Prop ≝
1026λf. steps_to_label_bound (f_graph (func f)) (next f).
1027
1028inductive state_steps_to_label_bound : state → nat → Prop ≝
1029| sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n
1030| sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n)
1031| sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n)
1032.
1033
1034lemma state_steps_to_label_bound_zero : ∀s.
1035  ¬ state_steps_to_label_bound s O.
1036#s % #H inversion H
1037[ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1038  inversion H52
1039  [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
1040  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct
1041  ]
1042| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1043| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1044] qed.
1045
1046lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1047  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1048  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1049  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 ].
1050#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1051whd in ⊢ (??%? → ?);
1052generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1053[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1054| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1055| #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1056| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1057| #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1058| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1059| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1060| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1061| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1062| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1063| #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
1064  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 ]
1065  whd in ⊢ (??%? → ?);
1066  generalize in ⊢ (??(?%)? → ?);
1067  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1068  [ #e #E normalize in E; destruct
1069  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1070  ]
1071| #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1072] qed.
1073
1074lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n.
1075  state_steps_to_label_bound s (S n) →
1076  eval_statement ge s = Value ??? 〈tr, s'〉 →
1077  RTLabs_cost s = false →
1078  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1079   state_steps_to_label_bound s' n.
1080#ge #s #tr #s' #n #STEPS inversion STEPS
1081[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1082  #EVAL cases (eval_successor … EVAL)
1083  [ /3/
1084  | * #l * #S1 #S2 #NC %2
1085    cases (steps_to_label_bound_inv_step … FS … l S2)
1086    [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ]
1087    #n'
1088    inversion (eval_perserves … EVAL)
1089    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct
1090      >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
1091      whd in S1:(??%?);
1092      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1093      %1 @H
1094    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1095      >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
1096      whd in S1:(??%?);
1097      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1098      %2 //
1099    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29
1100      destruct
1101    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
1102      normalize in S1; destruct
1103    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct
1104    ]
1105  ]
1106| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1107  /3/
1108| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1109  #EVAL #NC %2 inversion (eval_perserves … EVAL)
1110  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1111  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1112  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1113  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1114  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1115    %1 whd in FS ⊢ %;
1116    inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ]
1117    #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
1118    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 ]
1119    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1120    @FS
1121  ]
1122] qed.
1123 
1124
1125(*
1126lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.
1127  state_steps_to_label_bound (State f fs m) (S (S n)) →
1128  ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →
1129  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1130  state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]).
1131#ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H
1132[ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct
1133  cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ]
1134  #NC whd in ⊢ (??%? → ?);
1135  generalize in ⊢ (??(?%)? → ?);
1136  lapply (steps_to_label_bound_inv_step … H1 next_ok NC)
1137  cases (lookup_present ??? next next_ok)
1138  [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
1139  | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
1140  | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
1141  | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
1142  | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
1143  | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
1144  | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl
1145  | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
1146  | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
1147  | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl
1148  | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
1149  | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
1150  | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
1151  | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
1152  ]
1153*)
1154(* When constructing an infinite trace, we need to be able to grab the finite
1155   portion of the trace for the next [trace_label_diverges] constructor.  We
1156   use the fact that the trace is soundly labelled to achieve this. *)
1157
1158inductive finite_prefix (ge:genv) : state → Prop ≝
1159| fp_tal : ∀s,s'.
1160           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1161           flat_trace io_out io_in ge s' →
1162           finite_prefix ge s
1163| fp_tac : ∀s,s'.
1164           trace_any_call (RTLabs_status ge) s s' →
1165           flat_trace io_out io_in ge s' →
1166           finite_prefix ge s
1167.
1168
1169definition fp_add_default : ∀ge,s,s'.
1170  RTLabs_classify s = cl_other →
1171  finite_prefix ge s' →
1172  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
1173  RTLabs_cost s' = false →
1174  finite_prefix ge s ≝
1175λge,s,s',OTHER,fp.
1176match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
1177[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1178    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1179    rem
1180| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
1181    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
1182].
1183
1184definition fp_add_terminating_call : ∀ge,s,s1,s'.
1185  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
1186  ∀CALL:RTLabs_classify s = cl_call.
1187  finite_prefix ge s' →
1188  trace_label_return (RTLabs_status ge) s1 s' →
1189  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
1190  RTLabs_cost s' = false →
1191  finite_prefix ge s ≝
1192λge,s,s1,s',EVAL,CALL,fp.
1193match 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
1194[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1195    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1196    rem
1197| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
1198    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1199    rem
1200].
1201
1202definition termination_oracle ≝ ∀ge,depth,s,trace.
1203  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1204
1205let rec finite_segment ge s n trace
1206  (ORACLE: termination_oracle)
1207  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1208  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1209  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
1210  (LABEL_LIMIT: state_steps_to_label_bound s n)
1211  on n : finite_prefix ge s ≝
1212match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with
1213[ O ⇒ λLABEL_LIMIT. ⊥
1214| S n' ⇒
1215    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with
1216    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
1217    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
1218        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1219        [ cl_other ⇒ λCL.
1220            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1221            [ true ⇒ λCS.
1222                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
1223            | false ⇒ λCS.
1224                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in
1225                fp_add_default ge ?? CL fs ? CS
1226            ] (refl ??)
1227        | cl_jump ⇒ λCL.
1228            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
1229        | cl_call ⇒ λCL.?(*
1230            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
1231            [ or_introl TERMINATES ⇒
1232              match TERMINATES with [ witness TERMINATES ⇒
1233                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
1234                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
1235                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr)
1236                | false ⇒ λCS. ? (* broken - we don't know the new value of n *)
1237                    (*let fs ≝ finite_segment ge (new_status … tlr) ??????????????
1238                    fp_add_terminating_call … (new_trace … tlr) ? CS*)
1239                ] (refl ??)
1240              ]
1241            | or_intror NO_TERMINATION ⇒
1242                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
1243            ]*)
1244        | cl_return ⇒ λCL. ⊥
1245        ] (refl ??)
1246    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
1247    ] STATE_COSTLABELLED NO_TERMINATION
1248] LABEL_LIMIT.
1249[ cases (state_steps_to_label_bound_zero s) /2/
1250| (* TODO: how do we know that we're not at the final state? *)
1251| @(absurd ?? NO_TERMINATION)
1252     %{0} % @wr_base //
1253| @(well_cost_labelled_jump … EV) //
1254| 5,6,8,9,10: /2/
1255|
1256| @(well_cost_labelled_state_step … EV) //
1257| @(not_to_not … NO_TERMINATION)
1258  * #depth * #TERM %{depth} % @wr_step /2/
1259| cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?)
1260
1261@(well_cost_labelled_call … EV) //
1262|
1263 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
1264| 5,6,8: /2/
1265|
1266|*)
1267| 12,13,14: /2/
1268| @(well_cost_labelled_state_step … EV) //
1269| @(not_to_not … NO_TERMINATION)
1270  * #depth * #TERM %{depth} % @wr_step /2/
1271] cases daemon qed.
1272
1273(*
1274let corec make_label_diverges ge s
1275  (trace: flat_trace io_out io_in ge s)
1276  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1277  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1278  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1279  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
1280  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
1281  : trace_label_diverges (RTLabs_status ge) s ≝ ?
1282.
1283*)
Note: See TracBrowser for help on using the repository browser.