source: src/RTLabs/Traces.ma @ 1586

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

RTLabs structured traces: cost labels after jumps.

File size: 21.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      [ dp 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
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
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.
212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
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)
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.
227    RTLabs_classify s = cl_return →
228    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
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
274[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
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
280| #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
281] qed.
282
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
298(* We require that labels appear after branch instructions and at the start of
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?). *)
302
303definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
304λf,s. match s return λs. labels_present ? s → Prop with
305[ St_cond _ l1 l2 ⇒ λH.
306    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
307    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
308| St_jumptable _ ls ⇒ λH.
309    (* I did have a dependent version of All here, but it's a pain. *)
310    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
311| _ ⇒ λ_. True
312]. whd in H;
313[ @(proj1 … H)
314| @(proj2 … H)
315] qed.
316
317definition well_cost_labelled_fn : internal_function → Prop ≝
318λf. (∀l. ∀H:present … (f_graph f) l.
319         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
320    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
321[ @lookup_lookup_present | cases (f_entry f) // ] qed.
322
323(* We need to ensure that any code we come across is well-cost-labelled.  We may
324   get function code from either the global environment or the state. *)
325
326definition well_cost_labelled_ge : genv → Prop ≝
327λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
328
329definition well_cost_labelled_state : state → Prop ≝
330λs. match s with
331[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
332| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
333                          All ? (λf. well_cost_labelled_fn (func f)) fs
334| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
335].
336
337lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
338  eval_statement ge s = Value ??? 〈tr,s'〉 →
339  well_cost_labelled_ge ge →
340  well_cost_labelled_state s →
341  well_cost_labelled_state s'.
342#ge #s #tr' #s' #EV cases (eval_perserves … EV)
343[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
344| #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/
345| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
346| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
347| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
348| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
349] qed.
350
351lemma rtlabs_jump_inv : ∀s.
352  RTLabs_classify s = cl_jump →
353  ∃f,fs,m. s = State f fs m ∧
354  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
355  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
356*
357[ #f #fs #m #E
358  %{f} %{fs} %{m} %
359  [ @refl
360  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
361    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
362    [ %1 %{A} %{B} %{C} @refl
363    | %2 %{A} %{B} @refl
364    ]
365  ]
366| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
367| normalize #H8 #H9 #H10 #H11 #H12 destruct
368] qed.
369
370lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
371  eval_statement ge s = Value ??? 〈tr,s'〉 →
372  well_cost_labelled_state s →
373  RTLabs_classify s = cl_jump →
374  RTLabs_cost s' = true.
375#ge #s #tr #s' #EV #H #CL
376cases (rtlabs_jump_inv s CL)
377#fr * #fs * #m * #Es *
378[ * #r * #l1 * #l2 #Estmt
379  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
380  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
381  >Estmt #LP whd in ⊢ (??%? → ?);
382  (* replace with lemma on successors? *)
383  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
384  lapply (Hbody (next fr) (next_ok fr))
385  generalize in ⊢ (???% → ?);
386  >Estmt #LP'
387  whd in ⊢ (% → ?);
388  * #H1 #H2 [ @H1 | @H2 ]
389| * #r * #ls #Estmt
390  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
391  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
392  >Estmt #LP whd in ⊢ (??%? → ?);
393  (* replace with lemma on successors? *)
394  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
395  [ 2: (* later *)
396  | *: #E destruct
397  ]
398  lapply (Hbody (next fr) (next_ok fr))
399  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
400  generalize in ⊢ (??(?%)? → ?);
401  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
402  [ #E1 #E2 whd in E2:(??%?); destruct
403  | #l' #E1 #E2 whd in E2:(??%?); destruct
404    cases (All_nth ???? CP ? E1)
405    #H1 #H2 @H2
406  ]
407] qed.
408
409
410(* Don't need to know that labels break loops because we have termination. *)
411
412record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
413  new_state : state;
414  termination_count : nat;
415  remainder : flat_trace io_out io_in ge new_state;
416  terminates : nth_is_return ge termination_count O new_state remainder;
417  cost_labelled : well_cost_labelled_state new_state;
418  new_trace : T new_state
419}.
420
421definition replace_new_trace : ∀ge,T1,T2.
422  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
423λge,T1,T2,r,trace.
424  mk_make_result ge T2
425    (new_state … r)
426    (termination_count … r)
427    (remainder … r)
428    (terminates … r)
429    (cost_labelled … r)
430    trace.
431
432let rec make_label_return n ge s
433  (trace: flat_trace io_out io_in ge s)
434  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
435  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
436  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
437  (TERMINATES: nth_is_return ge n O s trace)
438  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
439
440  let r ≝ make_label_label n ge s trace ???? in
441  match new_trace … r with
442  [ dp ends tll ⇒
443    match ends return λx. trace_label_label ? x ?? → ? with
444    [ ends_with_ret ⇒ λtll.
445        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
446    | doesnt_end_with_ret ⇒ λtll.
447        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
448                   (remainder … r) ??? (terminates … r) in
449          replace_new_trace … r'
450            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
451    ] tll
452  ]
453
454and make_label_label n ge s
455  (trace: flat_trace io_out io_in ge s)
456  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
457  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
458  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
459  (TERMINATES: nth_is_return ge n O s trace)
460  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
461let r ≝ make_any_label n ge s trace ??? in
462match new_trace … r with
463[ dp ends tr ⇒
464  replace_new_trace ??? r
465    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
466]
467
468and make_any_label n ge s
469  (trace: flat_trace io_out io_in ge s)
470  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
471  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
472  (TERMINATES: nth_is_return ge n O s trace)
473  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
474match 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
475[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
476| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
477    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
478    [ cl_other ⇒ λCL.
479        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
480        [ true ⇒ λCS.
481            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 ???))
482        | false ⇒ λCS.
483            let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
484            match new_trace … r with
485            [ dp ends trc ⇒
486                replace_new_trace ??? r
487                  (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??))
488            ]
489        ] (refl ??)
490    | cl_jump ⇒ λCL.
491        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 ???))
492    | cl_call ⇒ λCL. ?
493    | cl_return ⇒ λCL. ?
494    ] (refl ? (RTLabs_classify start))
495| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
496] STATE_COSTLABELLED TERMINATES.
497
498[ //
499| //
500| @(trace_label_label_label … tll)
501| //
502| //
503| //
504| //
505| //
506| //
507| //
508|
509|
510| @(nth_is_return_notfn … TERMINATES) %2 @CL
511| @(well_cost_labelled_state_step  … EV) //
512| %{tr} @EV
513| % whd in ⊢ (% → ?); >CL #E destruct
514| @(well_cost_labelled_jump … EV) //
515|
516| @(nth_is_return_notfn … TERMINATES) %1 @CL
517| @(well_cost_labelled_state_step  … EV) //
518| %{tr} @EV
519| % whd in ⊢ (% → ?); >CL #E destruct
520| @CS
521| %{tr} @EV
522| @CL
523| % whd in ⊢ (% → ?); >CS #E destruct
524| @(well_cost_labelled_state_step … EV) //
525| @(nth_is_return_notfn … TERMINATES) %1 @CL
526| inversion TERMINATES
527  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
528  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
529  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
530  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct
531  ]
532|
533
534
535 
536(* FIXME: there's trouble at the end of the program because we can't make a step
537   away from the final return. *)
Note: See TracBrowser for help on using the repository browser.