source: src/RTLabs/Traces.ma @ 1670

Last change on this file since 1670 was 1670, checked in by campbell, 7 years ago

Snapshot of non-terminating RTLabs structured traces work.

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