source: src/RTLabs/Traces.ma @ 1681

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

Checkpoint of stack preservation work in RTLabs.

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