source: src/RTLabs/Traces.ma @ 1612

Last change on this file since 1612 was 1601, checked in by sacerdot, 8 years ago

Files ported to new version of the standard library.

File size: 23.5 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
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(* [will_return ge depth s trace] says that after a finite number of steps of
207   [trace] from [s] we reach the return state for the current function.  [depth]
208   performs the call/return counting necessary for handling deeper function
209   calls.  It should be zero at the top level. *)
210inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
211| wr_step : ∀s,tr,s',depth,EX,trace.
212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
213    will_return ge depth s' trace →
214    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
215| wr_call : ∀s,tr,s',depth,EX,trace.
216    RTLabs_classify s = cl_call →
217    will_return ge (S depth) s' trace →
218    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
219| wr_ret : ∀s,tr,s',depth,EX,trace.
220    RTLabs_classify s = cl_return →
221    will_return ge depth s' trace →
222    will_return ge (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| wr_base : ∀s,tr,s',EX,trace.
227    RTLabs_classify s = cl_return →
228    will_return ge O s (ft_step ?? ge s tr s' EX trace)
229.
230
231discriminator nat.
232
233lemma will_return_call : ∀ge,depth,s,trace.
234  will_return ge depth s trace →
235  will_return ge (pred depth) s trace.
236#ge #depth #s #trace #H elim H
237[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
238| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
239  cases d in H1 H2 ⊢ %; //
240| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
241  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
242| #s1 #tr #s2 #EX #trc #CL %4 //
243] qed.
244
245
246lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
247  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
248  will_return ge d s (ft_step ?? ge s tr s' EX trace) →
249  will_return ge d s' trace.
250#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
251[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
252| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
253| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct
254| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
255| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
256| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
257| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct
258| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
259] qed.
260
261(* We require that labels appear after branch instructions and at the start of
262   functions.  The first is required for preciseness, the latter for soundness.
263   We will make a separate requirement for there to be a finite number of steps
264   between labels to catch loops for soundness (is this sufficient?). *)
265
266definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
267λf,s. match s return λs. labels_present ? s → Prop with
268[ St_cond _ l1 l2 ⇒ λH.
269    is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧
270    is_cost_label (lookup_present … (f_graph f) l2 ?) = true
271| St_jumptable _ ls ⇒ λH.
272    (* I did have a dependent version of All here, but it's a pain. *)
273    All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls
274| _ ⇒ λ_. True
275]. whd in H;
276[ @(proj1 … H)
277| @(proj2 … H)
278] qed.
279
280definition well_cost_labelled_fn : internal_function → Prop ≝
281λf. (∀l. ∀H:present … (f_graph f) l.
282         well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧
283    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true.
284[ @lookup_lookup_present | cases (f_entry f) // ] qed.
285
286(* We need to ensure that any code we come across is well-cost-labelled.  We may
287   get function code from either the global environment or the state. *)
288
289definition well_cost_labelled_ge : genv → Prop ≝
290λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
291
292definition well_cost_labelled_state : state → Prop ≝
293λs. match s with
294[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
295| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
296                          All ? (λf. well_cost_labelled_fn (func f)) fs
297| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
298].
299
300lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
301  eval_statement ge s = Value ??? 〈tr,s'〉 →
302  well_cost_labelled_ge ge →
303  well_cost_labelled_state s →
304  well_cost_labelled_state s'.
305#ge #s #tr' #s' #EV cases (eval_perserves … EV)
306[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
307| #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/
308| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
309| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
310| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
311| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
312] qed.
313
314lemma rtlabs_jump_inv : ∀s.
315  RTLabs_classify s = cl_jump →
316  ∃f,fs,m. s = State f fs m ∧
317  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
318  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
319*
320[ #f #fs #m #E
321  %{f} %{fs} %{m} %
322  [ @refl
323  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
324    try (normalize try #A try #B try #C try #D try #F try #G try #H destruct)
325    [ %1 %{A} %{B} %{C} @refl
326    | %2 %{A} %{B} @refl
327    ]
328  ]
329| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
330| normalize #H8 #H9 #H10 #H11 #H12 destruct
331] qed.
332
333lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
334  eval_statement ge s = Value ??? 〈tr,s'〉 →
335  well_cost_labelled_state s →
336  RTLabs_classify s = cl_jump →
337  RTLabs_cost s' = true.
338#ge #s #tr #s' #EV #H #CL
339cases (rtlabs_jump_inv s CL)
340#fr * #fs * #m * #Es *
341[ * #r * #l1 * #l2 #Estmt
342  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
343  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
344  >Estmt #LP whd in ⊢ (??%? → ?);
345  (* replace with lemma on successors? *)
346  @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
347  lapply (Hbody (next fr) (next_ok fr))
348  generalize in ⊢ (???% → ?);
349  >Estmt #LP'
350  whd in ⊢ (% → ?);
351  * #H1 #H2 [ @H1 | @H2 ]
352| * #r * #ls #Estmt
353  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
354  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
355  >Estmt #LP whd in ⊢ (??%? → ?);
356  (* replace with lemma on successors? *)
357  @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
358  [ 2: (* later *)
359  | *: #E destruct
360  ]
361  lapply (Hbody (next fr) (next_ok fr))
362  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
363  generalize in ⊢ (??(?%)? → ?);
364  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
365  [ #E1 #E2 whd in E2:(??%?); destruct
366  | #l' #E1 #E2 whd in E2:(??%?); destruct
367    cases (All_nth ???? CP ? E1)
368    #H1 #H2 @H2
369  ]
370] qed.
371
372lemma rtlabs_call_inv : ∀s.
373  RTLabs_classify s = cl_call →
374  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
375* [ #f #fs #m whd in ⊢ (??%? → ?);
376    cases (lookup_present … (next f) (next_ok f)) normalize
377    try #A try #B try #C try #D try #E try #F try #G destruct
378  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
379  | normalize #H411 #H412 #H413 #H414 #H415 destruct
380  ] qed.
381
382lemma well_cost_labelled_call : ∀ge,s,tr,s'.
383  eval_statement ge s = Value ??? 〈tr,s'〉 →
384  well_cost_labelled_state s →
385  RTLabs_classify s = cl_call →
386  RTLabs_cost s' = true.
387#ge #s #tr #s' #EV #WCL #CL
388cases (rtlabs_call_inv s CL)
389#fd * #args * #dst * #stk * #m #E >E in EV WCL;
390whd in ⊢ (??%? → % → ?);
391cases fd
392[ #fn whd in ⊢ (??%? → % → ?);
393  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
394  #m' #b whd in ⊢ (??%? → ?); #E' destruct
395  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
396  @WCL2
397| #fn whd in ⊢ (??%? → % → ?);
398  @bindIO_value #evargs #Eargs
399  @bindIO_value #evres #Eres
400  normalize in Eres; destruct
401] qed.
402
403(* Don't need to know that labels break loops because we have termination. *)
404
405(* A bit of mucking around with the depth to avoid proving termination after
406  termination. *)
407record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ {
408  new_state : state;
409  remainder : flat_trace io_out io_in ge new_state;
410  cost_labelled : well_cost_labelled_state new_state;
411  new_trace : T new_state;
412  terminates : match depth with
413               [ O ⇒ True
414               | S d ⇒ will_return ge d new_state remainder
415               ]
416}.
417
418record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {
419  ends : trace_ends_with_ret;
420  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends)
421}.
422
423definition replace_sub_trace : ∀ge,trm,T1,T2.
424  ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝
425λge,trm,T1,T2,r,trace.
426  mk_sub_trace_result ge trm T2
427    (ends … r)
428    (mk_trace_result ge ? (T2 (ends … r))
429      (new_state … r)
430      (remainder … r)
431      (cost_labelled … r)
432      trace
433      (terminates … r)
434    )
435.
436
437definition replace_trace : ∀ge,trm,T1,T2.
438  ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝
439λge,trm,T1,T2,r,trace.
440  mk_trace_result ge trm T2
441    (new_state … r)
442    (remainder … r)
443    (cost_labelled … r)
444    trace
445    (terminates … r)
446.
447
448let rec make_label_return ge depth s
449  (trace: flat_trace io_out io_in ge s)
450  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
451  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
452  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
453  (TERMINATES: will_return ge depth s trace)
454  : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝
455
456  let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
457  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) → ? with
458  [ ends_with_ret ⇒ λr.
459      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r))
460  | doesnt_end_with_ret ⇒ λr.
461      let r' ≝ make_label_return ge depth (new_state … r)
462                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (terminates ??? r) in
463        replace_trace … r'
464          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r'))
465  ] (trace_res … r)
466
467and make_label_label ge depth s
468  (trace: flat_trace io_out io_in ge s)
469  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
470  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
471  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
472  (TERMINATES: will_return ge depth s trace)
473  : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝
474let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
475  replace_sub_trace … r
476    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
477
478and make_any_label ge depth s
479  (trace: flat_trace io_out io_in ge s)
480  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
481  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
482  (TERMINATES: will_return ge depth s trace)
483  : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝
484match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with
485[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
486| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
487    match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
488    [ cl_other ⇒ λCL.
489        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
490        [ true ⇒ λCS.
491            mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
492              doesnt_end_with_ret
493              (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
494        | false ⇒ λCS.
495            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in
496                replace_sub_trace … r
497                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
498        ] (refl ??)
499    | cl_jump ⇒ λCL.
500        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
501          doesnt_end_with_ret
502          (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)
503    | cl_call ⇒ λCL.
504        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in
505        let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
506        replace_sub_trace ???? r'
507          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
508    | cl_return ⇒ λCL.
509        mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start)
510          ends_with_ret
511          (mk_trace_result ge ??
512            next
513            trace'
514            ?
515            (tal_base_return (RTLabs_status ge) start next ? CL)
516            ?)
517    ] (refl ? (RTLabs_classify start))
518| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
519] STATE_COSTLABELLED TERMINATES.
520
521[ @(trace_label_label_label … (new_trace … r))
522|
523| inversion TERMINATES
524  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct >CL in H7; * #E destruct
525  | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 -TERMINATES destruct >CL in H21; #E destruct
526  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 -TERMINATES destruct @H36
527  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I
528  ]
529| %{tr} @EV
530| @(well_cost_labelled_state_step  … EV) //
531| whd @(will_return_notfn … TERMINATES) %2 @CL
532| %{tr} @EV
533| % whd in ⊢ (% → ?); >CL #E destruct
534| @(well_cost_labelled_jump … EV) //
535| @(well_cost_labelled_state_step  … EV) //
536| (* oh dear *)
537| %{tr} @EV
538| @(cost_labelled … r)
539| @(terminates … r)
540| @(well_cost_labelled_state_step  … EV) //
541| @(well_cost_labelled_call … EV) //
542| inversion TERMINATES
543  [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 -TERMINATES destruct >CL in H60; * #E destruct
544  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 -TERMINATES destruct @H75
545  | #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 -TERMINATES destruct >CL in H88; #E destruct
546  | #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 -TERMINATES destruct >CL in H101; #E destruct
547  ]
548| whd @(will_return_notfn … TERMINATES) %1 @CL
549| %{tr} @EV
550| % whd in ⊢ (% → ?); >CL #E destruct
551| @CS
552| @(well_cost_labelled_state_step  … EV) //
553| % whd in ⊢ (% → ?); >CS #E destruct
554| @CL
555| %{tr} @EV
556| @(well_cost_labelled_state_step  … EV) //
557| @(will_return_notfn … TERMINATES) %1 @CL
558| inversion TERMINATES
559  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 -TERMINATES destruct
560  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 -TERMINATES destruct
561  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 -TERMINATES destruct
562  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES destruct
563  ]
564|
565
566
567 
568(* FIXME: there's trouble at the end of the program because we can't make a step
569   away from the final return. *)
Note: See TracBrowser for help on using the repository browser.