source: src/RTLabs/Traces.ma @ 1675

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

Some work on sound labelled for RTLabs.

File size: 42.2 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 RTLabs_cost : state → bool ≝
23λs. match s with
24[ State f fs m ⇒
25    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
26| _ ⇒ false
27].
28
29definition RTLabs_status : genv → abstract_status ≝
30λge.
31  mk_abstract_status
32    state
33    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
34    (λs,c. RTLabs_classify s = c)
35    (λs. RTLabs_cost s = true)
36    (λs,s'. match s with
37      [ mk_Sig s p ⇒
38        match s return λs. RTLabs_classify s = cl_call → ? with
39        [ Callstate fd args dst stk m ⇒
40          λ_. match s' with
41          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
42          | _ ⇒ False
43          ]
44        | State f fs m ⇒ λH.⊥
45        | _ ⇒ λH.⊥
46        ] p
47      ]).
48[ normalize in H; destruct
49| whd in H:(??%?);
50  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
51  normalize try #a try #b try #c try #d try #e try #g try #h destruct
52] qed.
53
54lemma RTLabs_not_cost : ∀ge,s.
55  RTLabs_cost s = false →
56  ¬ as_costed (RTLabs_status ge) s.
57#ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
58qed.
59
60(* Before attempting to construct a structured trace, let's show that we can
61   form flat traces with evidence that they were constructed from an execution.
62   
63   For now we don't consider I/O. *)
64
65
66coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
67| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
68| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
69| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
70
71(* add I/O? *)
72coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
73| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
74| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
75| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
76
77let corec make_flat_trace ge s
78  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
79  flat_trace io_out io_in ge s ≝
80let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
81match e return λx. e = x → ? with
82[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
83| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
84| e_wrong m ⇒ λE. ft_wrong … s m ?
85| e_interact o f ⇒ λE. ⊥
86] (refl ? e).
87[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
88  cases (eval_statement ge s)
89  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
90  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
91    >(?:is_final ????? = RTLabs_is_final s1) //
92    lapply (refl ? (RTLabs_is_final s1))
93    cases (RTLabs_is_final s1) in ⊢ (???% → %);
94    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
95    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
96    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
97    ]
98  | *: #m whd in ⊢ (??%? → ?); #E destruct
99  ]
100| whd in E:(??%?); >exec_inf_aux_unfold in E;
101  cases (eval_statement ge s)
102  [ #O #K whd in ⊢ (??%? → ?); #E destruct
103  | * #tr #s1 whd in ⊢ (??%? → ?);
104    cases (is_final ?????)
105    [ whd in ⊢ (??%? → ?); #E destruct @refl
106    | #i whd in ⊢ (??%? → ?); #E destruct
107    ]
108  | #m whd in ⊢ (??%? → ?); #E destruct
109  ]
110| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
111  cases (eval_statement ge s)
112  [ #O #K whd in ⊢ (??%? → ?); #E destruct
113  | * #tr #s1 whd in ⊢ (??%? → ?);
114    cases (is_final ?????)
115    [ whd in ⊢ (??%? → ?); #E
116      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
117      destruct
118      inversion H
119      [ #a #b #c #E1 destruct
120      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
121      | #m #E1 destruct
122      ]
123    | #i whd in ⊢ (??%? → ?); #E destruct
124    ]
125  | #m whd in ⊢ (??%? → ?); #E destruct
126  ]
127| whd in E:(??%?); >exec_inf_aux_unfold in E;
128  cases (eval_statement ge s)
129  [ #O #K whd in ⊢ (??%? → ?); #E destruct
130  | * #tr1 #s1 whd in ⊢ (??%? → ?);
131    cases (is_final ?????)
132    [ whd in ⊢ (??%? → ?); #E destruct
133    | #i whd in ⊢ (??%? → ?); #E destruct
134    ]
135  | #m whd in ⊢ (??%? → ?); #E destruct @refl
136  ]
137| whd in E:(??%?); >E in H; #H
138  inversion H
139  [ #a #b #c #E destruct
140  | #a #b #c #d #E1 destruct
141  | #m #E1 destruct
142  ]
143] qed.
144
145let corec make_whole_flat_trace p s
146  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
147  (I:make_initial_state ??? p = OK ? s) :
148  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
149let ge ≝ make_global … p in
150let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
151match e return λx. e = x → ? with
152[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
153| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
154| e_wrong m ⇒ λE. ⊥
155| e_interact o f ⇒ λE. ⊥
156] (refl ? e).
157[ whd in E:(??%?); >exec_inf_aux_unfold in E;
158  whd in ⊢ (??%? → ?);
159  >(?:is_final ????? = RTLabs_is_final s) //
160  lapply (refl ? (RTLabs_is_final s))
161  cases (RTLabs_is_final s) in ⊢ (???% → %);
162  [ #_ whd in ⊢ (??%? → ?); #E destruct
163  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
164  ]
165| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
166  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
167  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
168    [ #a #b #c #E1 destruct
169    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
170      @H1
171    | #m #E1 destruct
172    ]
173  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
174  ]
175| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
176  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
177| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
178  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
179] qed.
180
181(* Need a way to choose whether a called function terminates.  Then,
182     if the initial function terminates we generate a purely inductive structured trace,
183     otherwise we start generating the coinductive one, and on every function call
184       use the choice method again to decide whether to step over or keep going.
185
186Not quite what we need - have to decide on seeing each label whether we will see
187another or hit a non-terminating call?
188
189Also - need the notion of well-labelled in order to break loops.
190
191
192
193outline:
194
195 does function terminate?
196 - yes, get (bound on the number of steps until return), generate finite
197        structure using bound as termination witness
198 - no,  get (¬ bound on steps to return), start building infinite trace out of
199        finite steps.  At calls, check for termination, generate appr. form.
200
201generating the finite parts:
202
203We start with the status after the call has been executed; well-labelling tells
204us that this is a labelled state.  Now we want to generate a trace_label_return
205and also return the remainder of the flat trace.
206
207*)
208
209(* [will_return ge depth s trace] says that after a finite number of steps of
210   [trace] from [s] we reach the return state for the current function.  [depth]
211   performs the call/return counting necessary for handling deeper function
212   calls.  It should be zero at the top level. *)
213inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
214| wr_step : ∀s,tr,s',depth,EX,trace.
215    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
216    will_return ge depth s' trace →
217    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
218| wr_call : ∀s,tr,s',depth,EX,trace.
219    RTLabs_classify s = cl_call →
220    will_return ge (S depth) s' trace →
221    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
222| wr_ret : ∀s,tr,s',depth,EX,trace.
223    RTLabs_classify s = cl_return →
224    will_return ge depth s' trace →
225    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
226    (* Note that we require the ability to make a step after the return (this
227       corresponds to somewhere that will be guaranteed to be a label at the
228       end of the compilation chain). *)
229| wr_base : ∀s,tr,s',EX,trace.
230    RTLabs_classify s = cl_return →
231    will_return ge O s (ft_step ?? ge s tr s' EX trace)
232.
233
234(* The way we will use [will_return] won't satisfy Matita's guardedness check,
235   so we will measure the length of these termination proofs and use an upper
236   bound to show termination of the finite structured trace construction
237   functions. *)
238
239let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
240match T with
241[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
242| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
243| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
244| wr_base _ _ _ _ _ _ ⇒ S O
245].
246
247include alias "arithmetics/nat.ma".
248
249(* Specialised to the particular situation it is used in. *)
250lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
251#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
252whd in ⊢ (??(??%) → ?);
253>commutative_times
254#H lapply (le_plus_b … H)
255#H lapply (le_to_leb_true … H)
256normalize #E destruct
257qed.
258
259(* Inversion lemmas on [will_return] that also note the effect on the length
260   of the proof. *)
261lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
262  RTLabs_classify s = cl_call →
263  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
264  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'.
265#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
266[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
267| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % //
268| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
269| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
270] qed.
271
272lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
273  RTLabs_classify s = cl_return →
274  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
275  match d with
276  [ O ⇒ True
277  | S d' ⇒
278      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM'
279  ].
280#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
281[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
282| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
283| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % //
284| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I
285] qed.
286
287lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
288  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
289  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
290  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'.
291#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
292[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % //
293| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
294| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
295| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
296| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % //
297| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
298| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
299| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
300] qed.
301
302(* We require that labels appear after branch instructions and at the start of
303   functions.  The first is required for preciseness, the latter for soundness.
304   We will make a separate requirement for there to be a finite number of steps
305   between labels to catch loops for soundness (is this sufficient?). *)
306
307definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
308λf,s. match s return λs. labels_present ? s → Prop with
309[ St_cond _ l1 l2 ⇒ λH.
310    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
311    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
312| St_jumptable _ ls ⇒ λH.
313    (* I did have a dependent version of All here, but it's a pain. *)
314    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
315| _ ⇒ λ_. True
316]. whd in H;
317[ @(proj1 … H)
318| @(proj2 … H)
319] qed.
320
321definition well_cost_labelled_fn : internal_function → Prop ≝
322λf. (∀l. ∀H:present … (f_graph f) l.
323         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
324    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
325[ @lookup_lookup_present | cases (f_entry f) // ] qed.
326
327(* We need to ensure that any code we come across is well-cost-labelled.  We may
328   get function code from either the global environment or the state. *)
329
330definition well_cost_labelled_ge : genv → Prop ≝
331λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
332
333definition well_cost_labelled_state : state → Prop ≝
334λs. match s with
335[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
336| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
337                          All ? (λf. well_cost_labelled_fn (func f)) fs
338| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
339].
340
341lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
342  eval_statement ge s = Value ??? 〈tr,s'〉 →
343  well_cost_labelled_ge ge →
344  well_cost_labelled_state s →
345  well_cost_labelled_state s'.
346#ge #s #tr' #s' #EV cases (eval_perserves … EV)
347[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
348| #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/
349| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
350| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
351| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
352| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
353] qed.
354
355lemma rtlabs_jump_inv : ∀s.
356  RTLabs_classify s = cl_jump →
357  ∃f,fs,m. s = State f fs m ∧
358  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
359  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
360*
361[ #f #fs #m #E
362  %{f} %{fs} %{m} %
363  [ @refl
364  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
365    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
366    [ %1 %{A} %{B} %{C} @refl
367    | %2 %{A} %{B} @refl
368    ]
369  ]
370| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
371| normalize #H8 #H9 #H10 #H11 #H12 destruct
372] qed.
373
374lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
375  eval_statement ge s = Value ??? 〈tr,s'〉 →
376  well_cost_labelled_state s →
377  RTLabs_classify s = cl_jump →
378  RTLabs_cost s' = true.
379#ge #s #tr #s' #EV #H #CL
380cases (rtlabs_jump_inv s CL)
381#fr * #fs * #m * #Es *
382[ * #r * #l1 * #l2 #Estmt
383  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
384  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
385  >Estmt #LP whd in ⊢ (??%? → ?);
386  (* replace with lemma on successors? *)
387  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
388  lapply (Hbody (next fr) (next_ok fr))
389  generalize in ⊢ (???% → ?);
390  >Estmt #LP'
391  whd in ⊢ (% → ?);
392  * #H1 #H2 [ @H1 | @H2 ]
393| * #r * #ls #Estmt
394  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
395  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
396  >Estmt #LP whd in ⊢ (??%? → ?);
397  (* replace with lemma on successors? *)
398  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
399  [ 2: (* later *)
400  | *: #E destruct
401  ]
402  lapply (Hbody (next fr) (next_ok fr))
403  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
404  generalize in ⊢ (??(?%)? → ?);
405  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
406  [ #E1 #E2 whd in E2:(??%?); destruct
407  | #l' #E1 #E2 whd in E2:(??%?); destruct
408    cases (All_nth ???? CP ? E1)
409    #H1 #H2 @H2
410  ]
411] qed.
412
413lemma rtlabs_call_inv : ∀s.
414  RTLabs_classify s = cl_call →
415  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
416* [ #f #fs #m whd in ⊢ (??%? → ?);
417    cases (lookup_present … (next f) (next_ok f)) normalize
418    try #A try #B try #C try #D try #E try #F try #G destruct
419  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
420  | normalize #H411 #H412 #H413 #H414 #H415 destruct
421  ] qed.
422
423lemma well_cost_labelled_call : ∀ge,s,tr,s'.
424  eval_statement ge s = Value ??? 〈tr,s'〉 →
425  well_cost_labelled_state s →
426  RTLabs_classify s = cl_call →
427  RTLabs_cost s' = true.
428#ge #s #tr #s' #EV #WCL #CL
429cases (rtlabs_call_inv s CL)
430#fd * #args * #dst * #stk * #m #E >E in EV WCL;
431whd in ⊢ (??%? → % → ?);
432cases fd
433[ #fn whd in ⊢ (??%? → % → ?);
434  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
435  #m' #b whd in ⊢ (??%? → ?); #E' destruct
436  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
437  @WCL2
438| #fn whd in ⊢ (??%? → % → ?);
439  @bindIO_value #evargs #Eargs
440  whd in ⊢ (??%? → ?);
441  #E' destruct
442] qed.
443
444(* Don't need to know that labels break loops because we have termination. *)
445
446(* A bit of mucking around with the depth to avoid proving termination after
447   termination.  Note that we keep a proof that our upper bound on the length
448   of the termination proof is respected. *)
449record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
450  new_state : state;
451  remainder : flat_trace io_out io_in ge new_state;
452  cost_labelled : well_cost_labelled_state new_state;
453  new_trace : T new_state;
454  terminates : match depth with
455               [ O ⇒ True
456               | S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM
457               ]
458}.
459
460(* The same with a flag indicating whether the function returned, as opposed to
461   encountering a label. *)
462record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
463  ends : trace_ends_with_ret;
464  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
465}.
466
467(* We often return the result from a recursive call with an addition to the
468   structured trace, so we define a couple of functions to help.  The bound on
469   the size of the termination proof might need to be relaxed, too. *)
470
471definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
472  ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge d T2 l2 ≝
473λge,d,T1,T2,l1,l2,lGE,r,trace.
474  mk_trace_result ge d T2 l2
475    (new_state … r)
476    (remainder … r)
477    (cost_labelled … r)
478    trace
479    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
480                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
481     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r))
482. @(transitive_le … lGE) @(pi2 … TM) qed.
483
484definition replace_sub_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 →
485  ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge d T2 l2 ≝
486λge,d,T1,T2,l1,l2,lGE,r,trace.
487  mk_sub_trace_result ge d T2 l2
488    (ends … r)
489    (replace_trace … lGE … r trace).
490
491(* Small syntax hack to avoid ambiguous input problems. *)
492definition myge : nat → nat → Prop ≝ ge.
493
494let rec make_label_return ge depth s
495  (trace: flat_trace io_out io_in ge s)
496  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
497  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
498  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
499  (TERMINATES: will_return ge depth s trace)
500  (TIME: nat)
501  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
502  on TIME : trace_result ge depth
503              (trace_label_return (RTLabs_status ge) s)
504              (will_return_length … TERMINATES) ≝
505             
506match TIME return λTIME. TIME ≥ ? → ? with
507[ O ⇒ λTERMINATES_IN_TIME. ⊥
508| S TIME ⇒ λTERMINATES_IN_TIME.
509
510  let r ≝ make_label_label ge depth s
511            trace
512            ENV_COSTLABELLED
513            STATE_COSTLABELLED
514            STATEMENT_COSTLABEL
515            TERMINATES
516            TIME ? in
517  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
518  [ ends_with_ret ⇒ λr.
519      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
520  | doesnt_end_with_ret ⇒ λr.
521      let r' ≝ make_label_return ge depth (new_state … r)
522                 (remainder … r)
523                 ENV_COSTLABELLED
524                 (cost_labelled … r) ?
525                 (pi1 … (terminates … r)) TIME ? in
526        replace_trace … r'
527          (tlr_step (RTLabs_status ge) s (new_state … r)
528            (new_state … r') (new_trace … r) (new_trace … r'))
529  ] (trace_res … r)
530
531] TERMINATES_IN_TIME
532
533
534and make_label_label ge depth s
535  (trace: flat_trace io_out io_in ge s)
536  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
537  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
538  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
539  (TERMINATES: will_return ge depth s trace)
540  (TIME: nat)
541  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
542  on TIME : sub_trace_result ge depth
543              (λends. trace_label_label (RTLabs_status ge) ends s)
544              (will_return_length … TERMINATES) ≝
545             
546match TIME return λTIME. TIME ≥ ? → ? with
547[ O ⇒ λTERMINATES_IN_TIME. ⊥
548| S TIME ⇒ λTERMINATES_IN_TIME.
549
550let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
551  replace_sub_trace … r
552    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
553
554] TERMINATES_IN_TIME
555
556
557and make_any_label ge depth s
558  (trace: flat_trace io_out io_in ge s)
559  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
560  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
561  (TERMINATES: will_return ge depth s trace)
562  (TIME: nat)
563  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
564  on TIME : sub_trace_result ge depth
565              (λends. trace_any_label (RTLabs_status ge) ends s)
566              (will_return_length … TERMINATES) ≝
567
568match TIME return λTIME. TIME ≥ ? → ? with
569[ O ⇒ λTERMINATES_IN_TIME. ⊥
570| S TIME ⇒ λTERMINATES_IN_TIME.
571
572  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 (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
573  [ ft_stop st FINAL ⇒
574      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
575
576  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
577    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
578    [ cl_other ⇒ λCL.
579        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
580        (* We're about to run into a label. *)
581        [ true ⇒ λCS.
582            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
583              doesnt_end_with_ret
584              (mk_trace_result ge ??? next trace' ?
585                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ?)
586        (* An ordinary step, keep going. *)
587        | false ⇒ λCS.
588            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
589                replace_sub_trace … r
590                  (tal_step_default (RTLabs_status ge) (ends … r)
591                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS))
592        ] (refl ??)
593       
594    | cl_jump ⇒ λCL.
595        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
596          doesnt_end_with_ret
597          (mk_trace_result ge ??? next trace' ?
598            (tal_base_not_return (RTLabs_status ge) start next ???) ?)
599           
600    | cl_call ⇒ λCL.
601        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
602        match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
603        (* We're about to run into a label, use base case for call *)
604        [ true ⇒ λCS.
605            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
606            doesnt_end_with_ret
607            (replace_trace … r
608              (tal_base_call (RTLabs_status ge) start next (new_state … r)
609                ? CL ? (new_trace … r) CS))
610        (* otherwise use step case *)
611        | false ⇒ λCS.
612            let r' ≝ make_any_label ge depth
613                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
614                       (pi1 … (terminates … r)) TIME ? in
615            replace_sub_trace … r'
616              (tal_step_call (RTLabs_status ge) (ends … r')
617                start next (new_state … r) (new_state … r') ? CL ?
618                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r'))
619        ] (refl ??)
620
621    | cl_return ⇒ λCL.
622        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?
623          ends_with_ret
624          (mk_trace_result ge ???
625            next
626            trace'
627            ?
628            (tal_base_return (RTLabs_status ge) start next ? CL)
629            ?)
630    ] (refl ? (RTLabs_classify start))
631   
632  | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
633 
634  ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
635] TERMINATES_IN_TIME.
636
637[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
638| //
639| cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le
640| @(trace_label_label_label … (new_trace … r))
641| cases r #H1 #H2 #H3 #H4 * #H5 #H6
642  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
643  @(transitive_le …  (3*(will_return_length … TERMINATES)))
644  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
645    @(monotonic_le_times_r 3 … H6)
646  | @le_S @le_S @le_n
647  ]
648| @le_S_S_to_le @TERMINATES_IN_TIME
649| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
650| @le_n
651| @le_S_S_to_le @TERMINATES_IN_TIME
652| @(wrl_nonzero … TERMINATES_IN_TIME)
653| (* Bad - we've reached the end of the trace; need to fix semantics so that
654     this can't happen *)
655| @(will_return_return … CL TERMINATES)
656| %{tr} @EV
657| @(well_cost_labelled_state_step  … EV) //
658| whd @(will_return_notfn … TERMINATES) %2 @CL
659| %{tr} @EV
660| %1 whd @CL
661| @(well_cost_labelled_jump … EV) //
662| @(well_cost_labelled_state_step  … EV) //
663| %{tr} @EV
664| (* TODO oh dear *)
665| cases (will_return_call … TERMINATES) #H @le_S_to_le
666| cases r #H1 #H2 #H3 #H4 * #H5
667  cases (will_return_call … CL TERMINATES)
668  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
669| (* TODO oh dear *)
670| %{tr} @EV
671| @(cost_labelled … r)
672| cases r #H72 #H73 #H74 #H75 * #H76 #H78
673  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
674  cases (will_return_call … TERMINATES) in H78;
675  #X #Y #Z
676  @(transitive_le … (monotonic_lt_times_r 3 … Y))
677  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
678  | //
679  ]
680| @(well_cost_labelled_state_step  … EV) //
681| @(well_cost_labelled_call … EV) //
682| skip
683| cases (will_return_call … TERMINATES)
684  #TM #GT @le_S_S_to_le
685  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
686  @(transitive_le … TERMINATES_IN_TIME)
687  @(monotonic_le_times_r 3 … GT)
688| whd @(will_return_notfn … TERMINATES) %1 @CL
689| %{tr} @EV
690| %2 whd @CL
691| @(well_cost_labelled_state_step  … EV) //
692| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
693| @CL
694| %{tr} @EV
695| @(well_cost_labelled_state_step  … EV) //
696| %1 @CL
697| cases (will_return_notfn … TERMINATES) #TM #GT
698  @le_S_S_to_le
699  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
700  //
701| inversion TERMINATES
702  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES -TERMINATES destruct
703  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES -TERMINATES destruct
704  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES -TERMINATES destruct
705  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
706  ]
707] cases daemon qed.
708
709(* We can initialise TIME with a suitably large value based on the length of the
710   termination proof. *)
711let rec make_label_return' ge depth s
712  (trace: flat_trace io_out io_in ge s)
713  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
714  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
715  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
716  (TERMINATES: will_return ge depth s trace)
717  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
718make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
719  (2 + 3 * will_return_length … TERMINATES) ?.
720@le_n
721qed.
722 
723(* FIXME: there's trouble at the end of the program because we can't make a step
724   away from the final return.
725   
726   We need to show that the "next pc" is preserved through a function call.
727   
728   Tail-calls are not handled properly (which means that if we try to show the
729   full version with non-termination we'll fail because calls and returns aren't
730   balanced.
731 *)
732
733inductive inhabited (T:Type[0]) : Prop ≝
734| witness : T → inhabited T.
735
736(* We also require that program's traces are soundly labelled: for any state
737   in the execution, we can give a distance to a labelled state or termination.
738   
739   Note that this differs from the syntactic notions in earlier languages
740   because it is a global property.  In principle, we would have a loop broken
741   only by a call to a function (which necessarily has a label) and no local
742   cost label.
743 *)
744
745let rec nth_state ge s
746  (trace: flat_trace io_out io_in ge s)
747  n
748  on n : option state ≝
749match n with
750[ O ⇒ Some ? s
751| S n' ⇒
752  match trace with
753  [ ft_step _ _ s' _ trace' ⇒ nth_state ge s' trace' n'
754  | _ ⇒ None ?
755  ]
756].
757
758definition soundly_labelled_trace : ∀ge,s. flat_trace io_out io_in ge s → Prop ≝
759λge,s,trace. ∀n.∃m. ∀s'. nth_state ge s trace (n+m) = Some ? s' → RTLabs_cost s' = true.
760
761lemma soundly_labelled_step : ∀ge,s,tr,s',EV,trace'.
762  soundly_labelled_trace ge s (ft_step … ge s tr s' EV trace') →
763  soundly_labelled_trace ge s' trace'.
764#ge #s #tr #s' #EV #trace' #H
765#n cases (H (S n)) #m #H' %{m} @H'
766qed.
767
768
769
770definition soundly_labelled_frame : frame → Prop ≝
771λf. soundly_labelled_pc (f_graph (func f)) (next f).
772
773definition soundly_labelled_state : state → Prop ≝
774λs. match s with
775[ State f _ _ ⇒ soundly_labelled_frame f
776| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
777| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
778].
779definition frame_steps_to_label_bound : frame → nat → Prop ≝
780λf. steps_to_label_bound (f_graph (func f)) (next f).
781
782inductive state_steps_to_label_bound : state → nat → Prop ≝
783| sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2)
784| 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*2))
785| 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*2))
786.
787
788(*
789lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.
790  state_steps_to_label_bound (State f fs m) (S (S n)) →
791  ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →
792  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
793  state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]).
794#ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H
795[ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct
796  cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ]
797  #NC whd in ⊢ (??%? → ?);
798  generalize in ⊢ (??(?%)? → ?);
799  lapply (steps_to_label_bound_inv_step … H1 next_ok NC)
800  cases (lookup_present ??? next next_ok)
801  [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
802  | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
803  | #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
804  | #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
805  | #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
806  | #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
807  | #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
808  | #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
809  | #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
810  | #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
811  | #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 ]
812  | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
813  | #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 ]
814  | #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
815  ]
816*)
817(* When constructing an infinite trace, we need to be able to grab the finite
818   portion of the trace for the next [trace_label_diverges] constructor.  We
819   use the fact that the trace is soundly labelled to achieve this. *)
820
821inductive finite_prefix (ge:genv) : state → Prop ≝
822| fp_tal : ∀s,s'.
823           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
824           flat_trace io_out io_in ge s' →
825           finite_prefix ge s
826| fp_tac : ∀s,s'.
827           trace_any_call (RTLabs_status ge) s s' →
828           flat_trace io_out io_in ge s' →
829           finite_prefix ge s
830.
831
832definition fp_add_default : ∀ge,s,s'.
833  RTLabs_classify s = cl_other →
834  finite_prefix ge s' →
835  (∃t. eval_statement ge s = Value ??? 〈t,s'〉) →
836  RTLabs_cost s' = false →
837  finite_prefix ge s ≝
838λge,s,s',OTHER,fp.
839match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with
840[ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf
841    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
842    rem
843| fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf
844    (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem
845].
846
847definition fp_add_terminating_call : ∀ge,s,s1,s'.
848  (∃t. eval_statement ge s = Value ??? 〈t,s1〉) →
849  ∀CALL:RTLabs_classify s = cl_call.
850  finite_prefix ge s' →
851  trace_label_return (RTLabs_status ge) s1 s' →
852  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →
853  RTLabs_cost s' = false →
854  finite_prefix ge s ≝
855λge,s,s1,s',EVAL,CALL,fp.
856match 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
857[ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
858    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
859    rem
860| fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf
861    (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
862    rem
863].
864
865definition termination_oracle ≝ ∀ge,depth,s,trace.
866  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
867
868let rec finite_segment ge s n trace
869  (ORACLE: termination_oracle)
870  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
871  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
872  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
873  (LABEL_LIMIT: state_steps_to_label_bound s n)
874  on n : finite_prefix ge s ≝
875match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
876[ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?
877| S n' ⇒
878    match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with
879    [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
880    | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT.
881        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
882        [ cl_other ⇒ λCL.
883            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
884            [ true ⇒ λCS.
885                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace'
886            | false ⇒ λCS.
887                let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in
888                fp_add_default ge ?? CL fs ? CS
889            ] (refl ??)
890        | cl_jump ⇒ λCL.
891            fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace'
892        | cl_call ⇒ λCL.
893            match ORACLE ge O next trace' return λ_. finite_prefix ge start with
894            [ or_introl TERMINATES ⇒
895              match TERMINATES with [ witness TERMINATES ⇒
896                let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
897                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
898                [ 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)
899                | false ⇒ λCS. ? (* broken - we don't know the new value of n *)
900                    (*let fs ≝ finite_segment ge (new_status … tlr) ??????????????
901                    fp_add_terminating_call … (new_trace … tlr) ? CS*)
902                ] (refl ??)
903              ]
904            | or_intror NO_TERMINATION ⇒
905                fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')
906            ]
907        | cl_return ⇒ λCL. ⊥
908        ] (refl ??)
909    | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥
910    ]
911] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT.
912[
913| 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct
914| @(absurd ?? NO_TERMINATION)
915     %{0} % @wr_base //
916| @(well_cost_labelled_jump … EV) //
917| 5,6,8: /2/
918|
919|
920| @(well_cost_labelled_state_step … EV) //
921| @(well_cost_labelled_call … EV) //
922| 12,13,14: /2/
923| @(well_cost_labelled_state_step … EV) //
924| @(not_to_not … NO_TERMINATION)
925  * #depth * #TERM %{depth} % @wr_step /2/
926] cases daemon qed.
927
928(*
929let corec make_label_diverges ge s
930  (trace: flat_trace io_out io_in ge s)
931  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
932  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
933  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
934  (SOUNDLY_COSTLABELLED: soundly_labelled_trace … trace)
935  (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
936  : trace_label_diverges (RTLabs_status ge) s ≝ ?
937.
938*)
Note: See TracBrowser for help on using the repository browser.