source: src/RTLabs/Traces.ma @ 1583

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

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

File size: 19.1 KB
RevLine 
[1537]1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
[1552]5discriminator status_class.
[1537]6
[1565]7(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
8       will be added later (LTL → LIN). *)
[1552]9
[1563]10definition RTLabs_classify : state → status_class ≝
11λs. match s with
[1565]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    ]
[1563]18| Callstate _ _ _ _ _ ⇒ cl_call
19| Returnstate _ _ _ _ ⇒ cl_return
20].
[1552]21
[1583]22definition RTLabs_cost : state → bool ≝
23λs. match s with
24[ State f fs m ⇒
25    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
26    [ St_cost c l ⇒ true
27    | _ ⇒ false
28    ]
29| _ ⇒ false
30].
[1552]31
[1537]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'〉)
[1563]37    (λs,c. RTLabs_classify s = c)
[1583]38    (λs. RTLabs_cost s = true)
[1537]39    (λs,s'. match s with
40      [ dp s p ⇒
[1563]41        match s return λs. RTLabs_classify s = cl_call → ? with
[1537]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      ]).
[1563]51[ normalize in H; destruct
[1565]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
[1563]55] qed.
[1559]56
57(* Before attempting to construct a structured trace, let's show that we can
58   form flat traces with evidence that they were constructed from an execution.
59   
60   For now we don't consider I/O. *)
61
62
63coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
64| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
65| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
66| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
67
68(* add I/O? *)
69coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
70| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
71| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
72| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
73
74let corec make_flat_trace ge s
75  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
76  flat_trace io_out io_in ge s ≝
77let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
78match e return λx. e = x → ? with
79[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
80| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
81| e_wrong m ⇒ λE. ft_wrong … s m ?
82| e_interact o f ⇒ λE. ⊥
83] (refl ? e).
84[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
85  cases (eval_statement ge s)
86  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
87  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
88    >(?:is_final ????? = RTLabs_is_final s1) //
89    lapply (refl ? (RTLabs_is_final s1))
90    cases (RTLabs_is_final s1) in ⊢ (???% → %);
91    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
92    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
93    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
94    ]
95  | *: #m whd in ⊢ (??%? → ?); #E destruct
96  ]
97| whd in E:(??%?); >exec_inf_aux_unfold in E;
98  cases (eval_statement ge s)
99  [ #O #K whd in ⊢ (??%? → ?); #E destruct
100  | * #tr #s1 whd in ⊢ (??%? → ?);
101    cases (is_final ?????)
102    [ whd in ⊢ (??%? → ?); #E destruct @refl
103    | #i whd in ⊢ (??%? → ?); #E destruct
104    ]
105  | #m whd in ⊢ (??%? → ?); #E destruct
106  ]
107| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
108  cases (eval_statement ge s)
109  [ #O #K whd in ⊢ (??%? → ?); #E destruct
110  | * #tr #s1 whd in ⊢ (??%? → ?);
111    cases (is_final ?????)
112    [ whd in ⊢ (??%? → ?); #E
113      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
114      destruct
115      inversion H
116      [ #a #b #c #E1 destruct
117      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
118      | #m #E1 destruct
119      ]
120    | #i whd in ⊢ (??%? → ?); #E destruct
121    ]
122  | #m whd in ⊢ (??%? → ?); #E destruct
123  ]
124| whd in E:(??%?); >exec_inf_aux_unfold in E;
125  cases (eval_statement ge s)
126  [ #O #K whd in ⊢ (??%? → ?); #E destruct
127  | * #tr1 #s1 whd in ⊢ (??%? → ?);
128    cases (is_final ?????)
129    [ whd in ⊢ (??%? → ?); #E destruct
130    | #i whd in ⊢ (??%? → ?); #E destruct
131    ]
132  | #m whd in ⊢ (??%? → ?); #E destruct @refl
133  ]
134| whd in E:(??%?); >E in H; #H
135  inversion H
136  [ #a #b #c #E destruct
137  | #a #b #c #d #E1 destruct
138  | #m #E1 destruct
139  ]
140] qed.
141
142let corec make_whole_flat_trace p s
143  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
144  (I:make_initial_state ??? p = OK ? s) :
145  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
146let ge ≝ make_global … p in
147let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
148match e return λx. e = x → ? with
149[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
150| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
151| e_wrong m ⇒ λE. ⊥
152| e_interact o f ⇒ λE. ⊥
153] (refl ? e).
154[ whd in E:(??%?); >exec_inf_aux_unfold in E;
155  whd in ⊢ (??%? → ?);
156  >(?:is_final ????? = RTLabs_is_final s) //
157  lapply (refl ? (RTLabs_is_final s))
158  cases (RTLabs_is_final s) in ⊢ (???% → %);
159  [ #_ whd in ⊢ (??%? → ?); #E destruct
160  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
161  ]
162| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
163  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
164  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
165    [ #a #b #c #E1 destruct
166    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
167      @H1
168    | #m #E1 destruct
169    ]
170  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
171  ]
172| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
173  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
174| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
175  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
176] qed.
177
[1563]178(* Need a way to choose whether a called function terminates.  Then,
179     if the initial function terminates we generate a purely inductive structured trace,
180     otherwise we start generating the coinductive one, and on every function call
181       use the choice method again to decide whether to step over or keep going.
182
183Not quite what we need - have to decide on seeing each label whether we will see
184another or hit a non-terminating call?
185
186Also - need the notion of well-labelled in order to break loops.
187
188
189
190outline:
191
192 does function terminate?
193 - yes, get (bound on the number of steps until return), generate finite
194        structure using bound as termination witness
195 - no,  get (¬ bound on steps to return), start building infinite trace out of
196        finite steps.  At calls, check for termination, generate appr. form.
197
198generating the finite parts:
199
200We start with the status after the call has been executed; well-labelling tells
201us that this is a labelled state.  Now we want to generate a trace_label_return
202and also return the remainder of the flat trace.
203
204*)
205
206(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
207   [s] we reach the return state for the current function.  [depth] performs
208   the call/return counting necessary for handling deeper function calls.
209   It should be zero at the top level. *)
210inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
211| nir_step : ∀n,s,tr,s',depth,EX,trace.
[1565]212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
[1563]213    nth_is_return ge n depth s' trace →
214    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
215| nir_call : ∀n,s,tr,s',depth,EX,trace.
216    RTLabs_classify s = cl_call →
217    nth_is_return ge n (S depth) s' trace →
218    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
219| nir_ret : ∀n,s,tr,s',depth,EX,trace.
220    RTLabs_classify s = cl_return →
221    nth_is_return ge n depth s' trace →
222    nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
[1583]223    (* Note that we require the ability to make a step after the return (this
224       corresponds to somewhere that will be guaranteed to be a label at the
225       end of the compilation chain). *)
226| nir_base : ∀s,tr,s',EX,trace.
[1563]227    RTLabs_classify s = cl_return →
[1583]228    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
[1563]229.
230
231discriminator nat.
232
233(* Find time until a nested call completes. *)
234lemma nth_is_return_down : ∀ge,n,depth,s,trace.
235  nth_is_return ge n (S depth) s trace →
236  ∃m. nth_is_return ge m depth s trace.
237#ge #n elim n
238(* It's impossible to run out of time... *)
239[ #depth #s #trace #H inversion H
240  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
241  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
242  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
243  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
244  ]
245| #n' #IH #depth #s #trace #H inversion H
246  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
247    cases (IH depth s1' trace1 ?)
248    [ #m' #H' %{(S m')} %1 //
249    | //
250    ]
251  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
252    cases (IH (S depth) s1' trace1 ?)
253    [ #m' #H' %{(S m')} %2 //
254    | //
255    ]
256  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
257    cases (depth1) in H2 ⊢ %;
258    [ #H2 %{O} %4 //
259    | #depth' #H2 cases (IH depth' s1' trace1 ?)
260      [ #m' #H' %{(S m')} %3 //
261      | //
262      ]
263    ]
264  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
265  ]
266] qed.
267
268lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
269  RTLabs_classify s = cl_call →
270  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
271  ∃m. nth_is_return ge m O s' trace.
272#ge #n #s #tr #s' #EX #trace #CLASS #H
273inversion H
[1565]274[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
[1563]275  -H2 destruct >H1 in CLASS; #E destruct
276| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
277  @nth_is_return_down //
278| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
279  -H2 destruct
[1583]280| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
[1563]281] qed.
282
[1583]283lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace.
284  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
285  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
286  nth_is_return ge (pred n) O s' trace.
287#ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM
288[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct //
289| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct
290| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct
291| #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct
292| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct //
293| #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct
294| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
295| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
296] qed.
297
[1565]298(* We require that labels appear after branch instructions and at the start of
[1574]299   functions.  The first is required for preciseness, the latter for soundness.
300   We will make a separate requirement for there to be a finite number of steps
301   between labels to catch loops for soundness (is this sufficient?). *)
[1565]302
303definition is_cost_label : statement → Prop ≝
304λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
305
306let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
307match l return λl.All A P l → Prop with
308[ nil ⇒ λ_. True
309| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
310] H.
311
312definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
313λf,s. match s return λs. labels_present ? s → Prop with
314[ St_cond _ l1 l2 ⇒ λH.
315    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
316    is_cost_label (lookup_present … (f_graph f) l2 ?)
317| St_jumptable _ ls ⇒ λH.
318    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
319| _ ⇒ λ_. True
320]. whd in H;
321[ @(proj1 … H)
322| @(proj2 … H)
323] qed.
324
325definition well_cost_labelled_fn : internal_function → Prop ≝
326λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
327          well_cost_labelled_statement f s (f_closed f …)) ∧
328    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
329[ 2: @H | skip | cases (f_entry f) // ] qed.
330
331(* We need to ensure that any code we come across is well-cost-labelled.  We may
332   get function code from either the global environment or the state. *)
333
334definition well_cost_labelled_ge : genv → Prop ≝
[1583]335λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
[1565]336
337definition well_cost_labelled_state : state → Prop ≝
338λs. match s with
339[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
340| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
341                          All ? (λf. well_cost_labelled_fn (func f)) fs
342| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
343].
344
[1583]345lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
346  eval_statement ge s = Value ??? 〈tr,s'〉 →
347  well_cost_labelled_ge ge →
348  well_cost_labelled_state s →
349  well_cost_labelled_state s'.
350#ge #s #tr' #s' #EV cases (eval_perserves … EV)
351[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
352| #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/
353| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
354| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
355| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
356| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
357] qed.
358
[1574]359(* Don't need to know that labels break loops because we have termination. *)
360
361record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
362  new_state : state;
363  termination_count : nat;
364  remainder : flat_trace io_out io_in ge new_state;
365  terminates : nth_is_return ge termination_count O new_state remainder;
366  cost_labelled : well_cost_labelled_state new_state;
367  new_trace : T new_state
368}.
369
370definition replace_new_trace : ∀ge,T1,T2.
371  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
372λge,T1,T2,r,trace.
373  mk_make_result ge T2
374    (new_state … r)
375    (termination_count … r)
376    (remainder … r)
377    (terminates … r)
378    (cost_labelled … r)
379    trace.
380
[1563]381let rec make_label_return n ge s
[1565]382  (trace: flat_trace io_out io_in ge s)
383  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
[1574]384  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
[1583]385  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
[1565]386  (TERMINATES: nth_is_return ge n O s trace)
[1574]387  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
388
389  let r ≝ make_label_label n ge s trace ???? in
390  match new_trace … r with
391  [ dp ends tll ⇒
392    match ends return λx. trace_label_label ? x ?? → ? with
393    [ ends_with_ret ⇒ λtll.
394        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
395    | doesnt_end_with_ret ⇒ λtll.
396        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
397                   (remainder … r) ??? (terminates … r) in
398          replace_new_trace … r'
399            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
400    ] tll
401  ]
402
403and make_label_label n ge s
404  (trace: flat_trace io_out io_in ge s)
405  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
406  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
[1583]407  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
[1574]408  (TERMINATES: nth_is_return ge n O s trace)
409  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
410let r ≝ make_any_label n ge s trace ??? in
411match new_trace … r with
412[ dp ends tr ⇒
413  replace_new_trace ??? r
414    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
415]
416
417and make_any_label n ge s
418  (trace: flat_trace io_out io_in ge s)
419  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
420  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
421  (TERMINATES: nth_is_return ge n O s trace)
422  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
[1583]423match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with
424[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
425| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
426    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
427    [ cl_other ⇒ λCL.
428        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
429        [ true ⇒ λCS.
430            mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???))
431        | false ⇒ λCS.
432            let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
433            match new_trace … r with
434            [ dp ends trc ⇒
435                replace_new_trace ??? r
436                  (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??))
437            ]
438        ] (refl ??)
439    | cl_jump ⇒ λCL. ?
440    | cl_call ⇒ λCL. ?
441    | cl_return ⇒ λCL. ?
442    ] (refl ? (RTLabs_classify start))
443| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
444] STATE_COSTLABELLED TERMINATES.
[1574]445
446[ //
447| //
448| @(trace_label_label_label … tll)
449| //
450| //
451| //
452| //
453| //
454| //
455| //
456|
457|
[1583]458|
459|
460| @(nth_is_return_notfn … TERMINATES) %1 @CL
461| @(well_cost_labelled_state_step  … EV) //
462| %{tr} @EV
463|
464| @CS
465| %{tr} @EV
466| @CL
467| % whd in ⊢ (% → ?); >CS #E destruct
468| @(well_cost_labelled_state_step … EV) //
469| @(nth_is_return_notfn … TERMINATES) %1 @CL
[1574]470| inversion TERMINATES
471  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
472  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
473  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
[1583]474  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
475  ]
476|
477
478
[1574]479 
[1583]480(* FIXME: there's trouble at the end of the program because we can't make a step
481   away from the final return. *)
Note: See TracBrowser for help on using the repository browser.