source: src/RTLabs/Traces.ma @ 2223

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

Simplify RTLabs structure traces proofs by getting rid of wrong
executions earlier.

File size: 98.3 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "RTLabs/CostSpec.ma".
4include "common/StructuredTraces.ma".
5include "common/Executions.ma".
6
7discriminator status_class.
8
9(* We augment states with a stack of function blocks (i.e. pointers) so that we
10   can make sensible "program counters" for the abstract state definition, along
11   with a proof that we will get the correct code when we do the lookup (which
12   is done to find cost labels given a pc).
13   
14   Adding them to the semantics is an alternative, more direct approach.
15   However, it makes animating the semantics extremely difficult, because it
16   is hard to avoid normalising and displaying irrelevant parts of the global
17   environment and proofs.
18   
19   We use blocks rather than identifiers because the global environments go
20
21     identifier → block → definition
22   
23   and we'd have to introduce backwards lookups to find identifiers for
24   function pointers.
25 *)
26
27definition Ras_Fn_Match ≝
28λge,state,fn_stack.
29  match state with
30  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
31  | Callstate fd _ _ fs _ ⇒
32      match fn_stack with
33      [ nil ⇒ False
34      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
35        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
36      ]
37  | Returnstate _ _ fs _ ⇒
38      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
39  | Finalstate _ ⇒ fn_stack = [ ]
40  ].
41
42record RTLabs_state (ge:genv) : Type[0] ≝ {
43  Ras_state :> state;
44  Ras_fn_stack : list block;
45  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
46}.
47
48(* Given a plain step of the RTLabs semantics, give the next state along with
49   the shadow stack of function block numbers.  Carefully defined so that the
50   coercion back to the plain state always reduces. *)
51definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
52  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
53λge,s,s',t,EX. mk_RTLabs_state ge s'
54 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
55 ?.
56cases s' in EX ⊢ %;
57[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
58  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
59    whd cases stk in mtc ⊢ %; [ * ]
60    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
61    | @M2 ]
62  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
63  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
64    whd cases stk in mtc ⊢ %; [ * ]
65    #hd #tl #H @H
66  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
67  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
68    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
69    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
70  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
71  ]
72| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
73  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
74  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
75  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
76    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
77    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
78  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
79  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
80  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
81  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
82  ]
83| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
84  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
85  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
86  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
87  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
88    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
89  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
90  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
91  ]
92| #r #EX whd @refl
93] qed.
94
95
96(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
97       will be added later (LTL → LIN). *)
98
99definition RTLabs_classify : state → status_class ≝
100λs. match s with
101[ State f _ _ ⇒
102    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
103    [ St_cond _ _ _ ⇒ cl_jump
104    | St_jumptable _ _ ⇒ cl_jump
105    | _ ⇒ cl_other
106    ]
107| Callstate _ _ _ _ _ ⇒ cl_call
108| Returnstate _ _ _ _ ⇒ cl_return
109| Finalstate _ ⇒ cl_other
110].
111
112(* As with is_cost_label/cost_label_of we define a boolean function as well
113   as one which extracts the cost label so that we can use it in hypotheses
114   without naming the cost label. *)
115
116definition RTLabs_cost : state → bool ≝
117λs. match s with
118[ State f fs m ⇒
119    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
120| _ ⇒ false
121].
122
123definition RTLabs_cost_label : state → option costlabel ≝
124λs. match s with
125[ State f fs m ⇒
126    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
127| _ ⇒ None ?
128].
129
130(* "Program counters" need to identify the current state, either as a pair of
131   the function and current instruction, or the function being entered or
132   left.  Functions are identified by their function pointer block because
133   this avoids introducing functions to map back pointers to function ids using
134   the global environment.  (See the comment at the start of this file, too.) *)
135
136inductive RTLabs_pc : Type[0] ≝
137| rapc_state : block → label → RTLabs_pc
138| rapc_call : block → RTLabs_pc
139| rapc_ret : option block → RTLabs_pc
140| rapc_fin : RTLabs_pc
141.
142
143definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
144λx,y. match x with
145[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
146| rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2 | _ ⇒ false ]
147| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2 | _ ⇒ false ]
148| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
149].
150
151definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
152whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq;
153* [ #b1 #l1 | #b1 | * [2: #b1 ] | ]
154* [ 1,5,9,13,17: #b2 #l2 | 2,6,10,14,18: #b2 | 3,7,11,15,19: * [2,4,6,8,10: #b2] | *: ]
155normalize nodelta
156[ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct | *: * #NE ] ]
157[ 1,4: @eq_identifier_elim [ 1,3: #E destruct | *: * #NE ] ]
158normalize % #E destruct try (cases (NE (refl ??))) @refl
159qed.
160
161definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
162λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
163match s' return λs'. Ras_Fn_Match ? s' ? → ? with
164[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
165| Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call b ]
166| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
167| Finalstate _ ⇒ λmtc. rapc_fin
168] mtc0 ].
169whd in mtc; cases mtc
170qed.
171
172definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
173λge,pc.
174match pc with
175[ rapc_state b l ⇒
176  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
177    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
178| _ ⇒ None ?
179].
180
181definition RTLabs_status : genv → abstract_status ≝
182λge.
183  mk_abstract_status
184    (RTLabs_state ge)
185    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
186    RTLabs_deqset
187    (RTLabs_state_to_pc ge)
188    (λs,c. RTLabs_classify s = c)
189    (RTLabs_pc_to_cost_label ge)
190    (λs,s'. match s with
191      [ mk_Sig s p ⇒
192        match s return λs. RTLabs_classify s = cl_call → ? with
193        [ Callstate fd args dst stk m ⇒
194          λ_. match s' with
195          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
196          | Finalstate r ⇒ stk = [ ]
197          | _ ⇒ False
198          ]
199        | State f fs m ⇒ λH.⊥
200        | _ ⇒ λH.⊥
201        ] p
202      ])
203  (λs. RTLabs_is_final s ≠ None ?).
204[ normalize in H; destruct
205| normalize in H; destruct
206| whd in H:(??%?);
207  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
208  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
209] qed.
210
211(* Allow us to move between the different notions of when a state is cost
212   labelled. *)
213
214lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge.
215  RTLabs_cost s = true ↔
216  as_costed (RTLabs_status ge) s.
217cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
218#ge * *
219[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
220  whd in ⊢ (??%); whd in ⊢ (??(?(??%?)));
221  whd in match (as_pc_of ??);
222  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
223  whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?)));
224  >(lookup_lookup_present … nok)
225  whd in ⊢ (?(??%?)(?(??%?)));
226  % cases (lookup_present ?? (f_graph func) ??) normalize
227  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
228  try (% #E' destruct)
229  cases (NONE ?) assumption
230| #fd #args #dst #fs #m #stk #mtc %
231  [ #E normalize in E; destruct
232  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
233    cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?);
234    #H cases (NONE H)
235  ]
236| #v #dst #fs #m #stk #mtc %
237  [ #E normalize in E; destruct
238  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
239    cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?);
240    #H cases (NONE H)
241  ]
242| #r #stk #mtc %
243  [ #E normalize in E; destruct
244  | #E normalize in E; cases (NONE E)
245  ]
246] qed.
247
248lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge.
249  RTLabs_cost s = false →
250  ¬ as_costed (RTLabs_status ge) s.
251#ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct
252qed.
253
254(* Before attempting to construct a structured trace, let's show that we can
255   form flat traces with evidence that they were constructed from an execution.
256   As with the structured traces, we only consider good traces (i.e., ones
257   which don't go wrong).
258   
259   For now we don't consider I/O. *)
260
261
262coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
263| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
264| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
265| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
266
267(* add I/O? *)
268coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
269| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
270| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s.
271
272let corec make_flat_trace ge s
273  (NF:RTLabs_is_final s = None ?)
274  (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s)))
275  (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
276  flat_trace io_out io_in ge s ≝
277let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
278match e return λx. e = x → ? with
279[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
280| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???)
281| e_wrong m ⇒ λE. ⊥
282| e_interact o f ⇒ λE. ⊥
283] (refl ? e).
284[ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E;
285  cases (eval_statement ge s)
286  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
287  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
288    >(?:is_final ????? = RTLabs_is_final s1) //
289    lapply (refl ? (RTLabs_is_final s1))
290    cases (RTLabs_is_final s1) in ⊢ (???% → %);
291    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
292    | #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
293    | #i #E whd in ⊢ (??%? → ?); #E2 destruct
294    ]
295  | *: #m whd in ⊢ (??%? → ?); #E destruct
296  ]
297| whd in E:(??%?); >exec_inf_aux_unfold in E;
298  cases (eval_statement ge s)
299  [ #o #K whd in ⊢ (??%? → ?); #E destruct
300  | * #tr #s1 whd in ⊢ (??%? → ?);
301    lapply (refl ? (RTLabs_is_final s1))
302    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
303    cases (RTLabs_is_final s1) in ⊢ (???% → %);
304    [ #F #E whd in E:(??%?); destruct
305    | #r #F #E whd in E:(??%?); destruct >F % #E destruct
306    ]
307  | #m #E whd in E:(??%?); destruct
308  ]
309| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
310  cases (eval_statement ge s)
311  [ #O #K whd in ⊢ (??%? → ?); #E destruct
312  | * #tr #s1 whd in ⊢ (??%? → ?);
313    cases (is_final ?????)
314    [ whd in ⊢ (??%? → ?); #E
315      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
316      destruct
317      inversion H
318      [ #a #b #c #E1 destruct
319      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
320      | #m #E1 destruct
321      ]
322    | #i whd in ⊢ (??%? → ?); #E destruct
323    ]
324  | #m whd in ⊢ (??%? → ?); #E destruct
325  ]
326| whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E;
327  cases (eval_statement ge s)
328  [ #O #K whd in ⊢ (??%? → ?); #E destruct
329  | * #tr #s1 whd in ⊢ (??%? → ?);
330    cases (is_final ?????)
331    [ whd in ⊢ (??%? → ?); #E
332      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
333      destruct
334      inversion NW
335      [ #a #b #c #E1 #_ destruct
336      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
337      | #o #k #K #E1 destruct
338      ]
339    | #i whd in ⊢ (??%? → ?); #E destruct
340    ]
341  | #m whd in ⊢ (??%? → ?); #E destruct
342  ]
343| whd in E:(??%?); >exec_inf_aux_unfold in E;
344  cases (eval_statement ge s)
345  [ #o #K whd in ⊢ (??%? → ?); #E destruct
346  | * #tr #s1 whd in ⊢ (??%? → ?);
347    lapply (refl ? (RTLabs_is_final s1))
348    change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
349    cases (RTLabs_is_final s1) in ⊢ (???% → %);
350    [ #F #E whd in E:(??%?); destruct @F
351    | #r #F #E whd in E:(??%?); destruct
352    ]
353  | #m #E whd in E:(??%?); destruct
354  ]
355| whd in E:(??%?); >E in NW; #X inversion X
356  #A #B #C #D #E destruct
357| whd in E:(??%?); >E in H; #H inversion H
358  #A #B #C try #D try #E destruct
359] qed.
360
361definition make_whole_flat_trace : ∀p,s.
362  exec_no_io … (exec_inf … RTLabs_fullexec p) →
363  not_wrong … (exec_inf … RTLabs_fullexec p) →
364  make_initial_state ??? p = OK ? s →
365  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
366λp,s,H,NW,I.
367let ge ≝ make_global … p in
368let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
369match e return λx. e = x → ? with
370[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
371| e_step _ _ e' ⇒ λE. make_flat_trace ge s ???
372| e_wrong m ⇒ λE. ⊥
373| e_interact o f ⇒ λE. ⊥
374] (refl ? e).
375[ whd in E:(??%?); >exec_inf_aux_unfold in E;
376  whd in ⊢ (??%? → ?);
377  change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
378  cases (RTLabs_is_final s)
379  [ #E whd in E:(??%?); destruct
380  | #r #E % #E' destruct
381  ]
382| @(initial_state_is_not_final … I)
383| whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?);
384  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????)
385  [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H
386    [ #a #b #c #E1 destruct
387    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
388      @H1
389    | #o #k #K #E1 destruct
390    ]
391  | #i whd in ⊢ (??%? → ??% → ?); #E destruct
392  ]
393| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
394  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
395  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
396    [ #a #b #c #E1 destruct
397    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
398      @H1
399    | #m #E1 destruct
400    ]
401  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
402  ]
403| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
404  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
405| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
406  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
407] qed.
408
409(* Need a way to choose whether a called function terminates.  Then,
410     if the initial function terminates we generate a purely inductive structured trace,
411     otherwise we start generating the coinductive one, and on every function call
412       use the choice method again to decide whether to step over or keep going.
413
414Not quite what we need - have to decide on seeing each label whether we will see
415another or hit a non-terminating call?
416
417Also - need the notion of well-labelled in order to break loops.
418
419
420
421outline:
422
423 does function terminate?
424 - yes, get (bound on the number of steps until return), generate finite
425        structure using bound as termination witness
426 - no,  get (¬ bound on steps to return), start building infinite trace out of
427        finite steps.  At calls, check for termination, generate appr. form.
428
429generating the finite parts:
430
431We start with the status after the call has been executed; well-labelling tells
432us that this is a labelled state.  Now we want to generate a trace_label_return
433and also return the remainder of the flat trace.
434
435*)
436
437(* [will_return ge depth s trace] says that after a finite number of steps of
438   [trace] from [s] we reach the return state for the current function.  [depth]
439   performs the call/return counting necessary for handling deeper function
440   calls.  It should be zero at the top level. *)
441inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝
442| wr_step : ∀s,tr,s',depth,EX,trace.
443    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
444    will_return ge depth s' trace →
445    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
446| wr_call : ∀s,tr,s',depth,EX,trace.
447    RTLabs_classify s = cl_call →
448    will_return ge (S depth) s' trace →
449    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
450| wr_ret : ∀s,tr,s',depth,EX,trace.
451    RTLabs_classify s = cl_return →
452    will_return ge depth s' trace →
453    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
454    (* Note that we require the ability to make a step after the return (this
455       corresponds to somewhere that will be guaranteed to be a label at the
456       end of the compilation chain). *)
457| wr_base : ∀s,tr,s',EX,trace.
458    RTLabs_classify s = cl_return →
459    will_return ge O s (ft_step ?? ge s tr s' EX trace)
460.
461
462(* The way we will use [will_return] won't satisfy Matita's guardedness check,
463   so we will measure the length of these termination proofs and use an upper
464   bound to show termination of the finite structured trace construction
465   functions. *)
466
467let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝
468match T with
469[ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
470| wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
471| wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T')
472| wr_base _ _ _ _ _ _ ⇒ S O
473].
474
475include alias "arithmetics/nat.ma".
476
477(* Specialised to the particular situation it is used in. *)
478lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False.
479#ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH]
480whd in ⊢ (??(??%) → ?);
481>commutative_times
482#H lapply (le_plus_b … H)
483#H lapply (le_to_leb_true … H)
484normalize #E destruct
485qed.
486   
487let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝
488match T with
489[ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
490| wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
491| wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T'
492| wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr'
493].
494
495(* Inversion lemmas on [will_return] that also note the effect on the length
496   of the proof. *)
497lemma will_return_call : ∀ge,d,s,tr,s',EX,trace.
498  RTLabs_classify s = cl_call →
499  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
500  ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
501#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
502[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
503| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/
504| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct
505| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct
506] qed.
507
508lemma will_return_return : ∀ge,d,s,tr,s',EX,trace.
509  RTLabs_classify s = cl_return →
510  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
511  match d with
512  [ O ⇒ will_return_end … TM = ❬s', trace❭
513  | S d' ⇒
514      ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'
515  ].
516#ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM
517[ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct
518| #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥  destruct >CL in H39; #E destruct
519| #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/
520| #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl
521] qed.
522
523lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace.
524  (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) →
525  ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace).
526  ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'.
527#ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM
528[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/
529| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct
530| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct
531| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct
532| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/
533| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct
534| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct
535| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct
536] qed.
537
538(* When it comes to building bits of nonterminating executions we'll need to be
539   able to glue termination proofs together. *)
540
541lemma will_return_prepend : ∀ge,d1,s1,t1.
542  ∀T1:will_return ge d1 s1 t1.
543  ∀d2,s2,t2.
544  will_return ge d2 s2 t2 →
545  will_return_end … T1 = ❬s2, t2❭ →
546  will_return ge (d1 + S d2) s1 t1.
547#ge #d1 #s1 #tr1 #T1 elim T1
548[ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E
549  %1 // @(IH … T2) @E
550| #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E
551| #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E
552| #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 //
553] qed.
554
555discriminator nat.
556
557lemma will_return_remove_call : ∀ge,d1,s1,t1.
558  ∀T1:will_return ge d1 s1 t1.
559  ∀d2.
560  will_return ge (d1 + S d2) s1 t1 →
561  ∀s2,t2.
562  will_return_end … T1 = ❬s2, t2❭ →
563  will_return ge d2 s2 t2.
564(* The key part of the proof is to show that the two termination proofs follow
565   the same pattern. *)
566#ge #d1x #s1x #t1x #T1 elim T1
567[ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
568  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct //
569                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
570                   >H21 in CL; * #E destruct
571                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
572                   >H35 in CL; * #E destruct
573                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
574                   >H48 in CL; * #E destruct
575                 ]
576  | @E
577  ]
578| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
579  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
580                   >CL in H7; * #E destruct
581                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct //
582                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct
583                   >H35 in CL; #E destruct
584                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct
585                   >H48 in CL; #E destruct
586                 ]
587  | @E
588  ]
589| #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH
590  [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
591                   >CL in H7; * #E destruct
592                 | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
593                   >H21 in CL; #E destruct
594                 | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
595                   whd in H38:(??%??); destruct //
596                 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
597                   whd in H49:(??%??); @⊥ destruct
598                 ]
599  | @E
600  ]
601| #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct
602  inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct
603                 >CL in H7; * #E destruct
604               | #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct
605                 >H21 in CL; #E destruct
606               | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41
607                 whd in H38:(??%??); destruct //
608               | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52
609                 whd in H49:(??%??); @⊥ destruct
610               ]
611] qed.
612
613
614
615lemma will_return_lower : ∀ge,d,s,t.
616  will_return ge d s t →
617  ∀d'. d' ≤ d →
618  will_return ge d' s t.
619#ge #d0 #s0 #t0 #TM elim TM
620[ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/
621| #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/
622| #s #tr #s' #d #EX #tr #CL #TM1 #IH *
623  [ #LE @wr_base //
624  | #d' #LE %3 // @IH /2/
625  ]
626| #s #tr #s' #EX #tr #CL *
627  [ #_ @wr_base //
628  | #d' #LE @⊥ /2/
629  ]
630] qed.
631
632(* We need to ensure that any code we come across is well-cost-labelled.  We may
633   get function code from either the global environment or the state. *)
634
635definition well_cost_labelled_ge : genv → Prop ≝
636λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.
637
638definition well_cost_labelled_state : state → Prop ≝
639λs. match s with
640[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
641| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
642                          All ? (λf. well_cost_labelled_fn (func f)) fs
643| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
644| Finalstate _ ⇒ True
645].
646
647lemma well_cost_labelled_state_step : ∀ge,s,tr,s'.
648  eval_statement ge s = Value ??? 〈tr,s'〉 →
649  well_cost_labelled_ge ge →
650  well_cost_labelled_state s →
651  well_cost_labelled_state s'.
652#ge #s #tr' #s' #EV cases (eval_preserves … EV)
653[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
654| #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/
655(*
656| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
657*)
658| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
659| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
660| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
661| //
662] qed.
663
664lemma rtlabs_jump_inv : ∀s.
665  RTLabs_classify s = cl_jump →
666  ∃f,fs,m. s = State f fs m ∧
667  let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
668  (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls).
669*
670[ #f #fs #m #E
671  %{f} %{fs} %{m} %
672  [ @refl
673  | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %;
674    try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct)
675    [ %1 %{A} %{B} %{C} @refl
676    | %2 %{A} %{B} @refl
677    ]
678  ]
679| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
680| normalize #H8 #H9 #H10 #H11 #H12 destruct
681| #r #E normalize in E; destruct
682] qed.
683
684lemma well_cost_labelled_jump : ∀ge,s,tr,s'.
685  eval_statement ge s = Value ??? 〈tr,s'〉 →
686  well_cost_labelled_state s →
687  RTLabs_classify s = cl_jump →
688  RTLabs_cost s' = true.
689#ge #s #tr #s' #EV #H #CL
690cases (rtlabs_jump_inv s CL)
691#fr * #fs * #m * #Es *
692[ * #r * #l1 * #l2 #Estmt
693  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
694  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
695  >Estmt #LP whd in ⊢ (??%? → ?);
696  (* replace with lemma on successors? *)
697  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
698  lapply (Hbody (next fr) (next_ok fr))
699  generalize in ⊢ (???% → ?);
700  >Estmt #LP'
701  whd in ⊢ (% → ?);
702  * #H1 #H2 [ @H1 | @H2 ]
703| * #r * #ls #Estmt
704  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
705  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
706  >Estmt #LP whd in ⊢ (??%? → ?);
707  (* replace with lemma on successors? *)
708  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
709  [ 2: (* later *)
710  | *: #E destruct
711  ]
712  lapply (Hbody (next fr) (next_ok fr))
713  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
714  generalize in ⊢ (??(?%)? → ?);
715  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
716  [ #E1 #E2 whd in E2:(??%?); destruct
717  | #l' #E1 #E2 whd in E2:(??%?); destruct
718    cases (All_nth ???? CP ? E1)
719    #H1 #H2 @H2
720  ]
721] qed.
722
723lemma rtlabs_call_inv : ∀s.
724  RTLabs_classify s = cl_call →
725  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
726* [ #f #fs #m whd in ⊢ (??%? → ?);
727    cases (lookup_present … (next f) (next_ok f)) normalize
728    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
729  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
730  | normalize #H411 #H412 #H413 #H414 #H415 destruct
731  | normalize #H1 #H2 destruct
732  ] qed.
733
734lemma well_cost_labelled_call : ∀ge,s,tr,s'.
735  eval_statement ge s = Value ??? 〈tr,s'〉 →
736  well_cost_labelled_state s →
737  RTLabs_classify s = cl_call →
738  RTLabs_cost s' = true.
739#ge #s #tr #s' #EV #WCL #CL
740cases (rtlabs_call_inv s CL)
741#fd * #args * #dst * #stk * #m #E >E in EV WCL;
742whd in ⊢ (??%? → % → ?);
743cases fd
744[ #fn whd in ⊢ (??%? → % → ?);
745  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
746  #m' #b whd in ⊢ (??%? → ?); #E' destruct
747  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
748  @WCL2
749| #fn whd in ⊢ (??%? → % → ?);
750  @bindIO_value #evargs #Eargs
751  whd in ⊢ (??%? → ?);
752  #E' destruct
753] qed.
754
755
756(* The preservation of (most of) the stack is useful to show as_after_return.
757   We do this by showing that during the execution of a function the lower stack
758   frames never change, and that after returning from the function we preserve
759   the identity of the next instruction to execute.
760   
761   Note: since this was first written I've introduced the shadow stack of
762   function blocks.  It might be possible to replace some or all of the stack
763   preservation with that.
764 *)
765
766inductive stack_of_state : list frame → state → Prop ≝
767| sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
768| sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
769| sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
770.
771
772inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
773| sp_normal : ∀fs,s1,s2.
774    stack_of_state fs s1 →
775    stack_of_state fs s2 →
776    stack_preserved doesnt_end_with_ret s1 s2
777| sp_finished : ∀s1,f,f',fs,m.
778    next f = next f' →
779    frame_rel f f' →
780    stack_of_state (f::fs) s1 →
781    stack_preserved ends_with_ret s1 (State f' fs m)
782| sp_stop : ∀s1,r.
783    stack_of_state [ ] s1 →
784    stack_preserved ends_with_ret s1 (Finalstate r)
785| sp_top : ∀fd,args,dst,m,r.
786    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
787.
788
789discriminator list.
790
791lemma stack_of_state_eq : ∀fs,fs',s.
792  stack_of_state fs s →
793  stack_of_state fs' s →
794  fs = fs'.
795#fs0 #fs0' #s0 *
796[ #f #fs #m #H inversion H
797  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
798| #fd #args #dst #f #fs #m #H inversion H
799  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
800| #rtv #dst #fs #m #H inversion H
801  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
802] qed.
803
804lemma stack_preserved_final : ∀e,r,s.
805  ¬stack_preserved e (Finalstate r) s.
806#e #r #s % #H inversion H
807[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
808  inversion SOS #a #b #c #d #e #f try #g try #h destruct
809| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
810  inversion SOS #a #b #c #d #e #f try #g try #h destruct
811| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
812  inversion SOS #a #b #c #d #e #f try #g try #h destruct
813| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
814] qed.
815
816lemma stack_preserved_join : ∀e,s1,s2,s3.
817  stack_preserved doesnt_end_with_ret s1 s2 →
818  stack_preserved e s2 s3 →
819  stack_preserved e s1 s3.
820#e1 #s1 #s2 #s3 #H1 inversion H1
821[ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
822  #H2 inversion H2
823  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
824    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
825  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
826    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
827  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
828  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
829    inversion S2
830    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
831    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
832    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
833    ]
834  ]
835| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
836| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
837  cases (stack_preserved_final … H) #r #E destruct
838| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
839  @(absurd … F) //
840] qed.
841
842lemma stack_preserved_return : ∀ge,s1,s2,tr.
843  RTLabs_classify s1 = cl_return →
844  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
845  stack_preserved ends_with_ret s1 s2.
846#ge *
847[ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
848  cases (lookup_present ??? (next f) (next_ok f)) in E;
849  normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
850| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
851| #res #dst *
852  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
853    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
854  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV
855    whd in EV:(??%?); destruct @(sp_finished ? f) //
856    cases f //
857  ]
858| #r #s2 #tr #E normalize in E; destruct
859] qed.
860
861lemma stack_preserved_step : ∀ge,s1,s2,tr.
862  RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
863  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
864  stack_preserved doesnt_end_with_ret s1 s2.
865#ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
866[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
867| #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
868| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
869  normalize in CL; cases CL #E destruct
870| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
871| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
872  #E normalize in E; destruct
873| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
874] qed.
875
876lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
877  RTLabs_classify s1 = cl_call →
878  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
879  stack_preserved ends_with_ret s2 s3 →
880  stack_preserved doesnt_end_with_ret s1 s3.
881#ge #s1 #s2 #s3 #tr #CL #EV #SP
882cases (rtlabs_call_inv … CL)
883#fd * #args * #dst * #stk * #m #E destruct
884inversion SP
885[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
886| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
887  inversion (eval_preserves … EV)
888  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
889  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
890  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
891    inversion S
892    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
893    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
894    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
895    ]
896  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
897  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
898  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
899  ]
900| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
901  inversion (eval_preserves … EV)
902  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
903  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
904  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
905    inversion S1
906    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
907    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
908    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
909    ]
910  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
911  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
912  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
913  ]
914| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
915] qed.
916 
917lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.∀tr.
918  ∀CL : RTLabs_classify s1 = cl_call.
919  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
920  stack_preserved ends_with_ret s2 s3 →
921  as_after_return (RTLabs_status ge) «s1,CL» s3.
922#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #tr #CL #EV #S23
923cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
924whd
925inversion S23
926[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
927| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct whd
928  inversion (eval_preserves … EV)
929  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
930  | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
931  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
932    inversion S
933    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
934    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
935    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
936    ]
937  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
938  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
939  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
940  ]
941| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
942  inversion (eval_preserves … EV)
943  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
944  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
945  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
946    inversion S1
947    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
948    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
949    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
950    ]
951  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
952  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
953  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
954  ]
955| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
956] qed.
957
958(* Don't need to know that labels break loops because we have termination. *)
959
960(* A bit of mucking around with the depth to avoid proving termination after
961   termination.  Note that we keep a proof that our upper bound on the length
962   of the termination proof is respected. *)
963record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
964  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
965  (original_terminates: will_return ge depth start full)
966  (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
967{
968  new_state : RTLabs_state ge;
969  remainder : flat_trace io_out io_in ge new_state;
970  cost_labelled : well_cost_labelled_state new_state;
971  new_trace : T new_state;
972  stack_ok : stack_preserved ends start new_state;
973  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
974               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
975               | S d ⇒ ΣTM:will_return ge d new_state remainder.
976                         gt limit (will_return_length … TM) ∧
977                         will_return_end … original_terminates = will_return_end … TM
978               ]
979}.
980
981(* The same with a flag indicating whether the function returned, as opposed to
982   encountering a label. *)
983record sub_trace_result (ge:genv) (depth:nat)
984  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
985  (original_terminates: will_return ge depth start full)
986  (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
987{
988  ends : trace_ends_with_ret;
989  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
990}.
991
992(* We often return the result from a recursive call with an addition to the
993   structured trace, so we define a couple of functions to help.  The bound on
994   the size of the termination proof might need to be relaxed, too. *)
995
996definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
997  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
998    will_return_end … TM1 = will_return_end … TM2 →
999    T2 (new_state … r) →
1000    stack_preserved e s2 (new_state … r) →
1001    trace_result ge d e s2 t2 TM2 T2 l2 ≝
1002λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1003  mk_trace_result ge d e s2 t2 TM2 T2 l2
1004    (new_state … r)
1005    (remainder … r)
1006    (cost_labelled … r)
1007    trace
1008    SP
1009    ?
1010    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
1011                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
1012     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
1013.
1014cases e in r ⊢ %;
1015[ <TME -TME * cases d in TM1 TM2 ⊢ %;
1016  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
1017  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
1018    %{TMa} % // @(transitive_le … lGE) @L1
1019  ]
1020| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
1021   * #TMa * #L1 #TME
1022    %{TMa} % // @(transitive_le … lGE) @L1
1023] qed.
1024
1025definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
1026  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
1027    will_return_end … TM1 = will_return_end … TM2 →
1028    T2 (ends … r) (new_state … r) →
1029    stack_preserved (ends … r) s2 (new_state … r) →
1030    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
1031λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1032  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
1033    (ends … r)
1034    (replace_trace … lGE … r TME trace SP).
1035
1036(* Small syntax hack to avoid ambiguous input problems. *)
1037definition myge : nat → nat → Prop ≝ ge.
1038
1039let rec make_label_return ge depth (s:RTLabs_state ge)
1040  (trace: flat_trace io_out io_in ge s)
1041  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1042  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1043  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1044  (TERMINATES: will_return ge depth s trace)
1045  (TIME: nat)
1046  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
1047  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
1048              (trace_label_return (RTLabs_status ge) s)
1049              (will_return_length … TERMINATES) ≝
1050             
1051match TIME return λTIME. TIME ≥ ? → ? with
1052[ O ⇒ λTERMINATES_IN_TIME. ⊥
1053| S TIME ⇒ λTERMINATES_IN_TIME.
1054
1055  let r ≝ make_label_label ge depth s
1056            trace
1057            ENV_COSTLABELLED
1058            STATE_COSTLABELLED
1059            STATEMENT_COSTLABEL
1060            TERMINATES
1061            TIME ? in
1062  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
1063                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
1064  [ ends_with_ret ⇒ λr.
1065      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
1066  | doesnt_end_with_ret ⇒ λr.
1067      let r' ≝ make_label_return ge depth (new_state … r)
1068                 (remainder … r)
1069                 ENV_COSTLABELLED
1070                 (cost_labelled … r) ?
1071                 (pi1 … (terminates … r)) TIME ? in
1072        replace_trace … r' ?
1073          (tlr_step (RTLabs_status ge) s (new_state … r)
1074            (new_state … r') (new_trace … r) (new_trace … r')) ?
1075  ] (trace_res … r)
1076
1077] TERMINATES_IN_TIME
1078
1079
1080and make_label_label ge depth (s:RTLabs_state ge)
1081  (trace: flat_trace io_out io_in ge s)
1082  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1083  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1084  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1085  (TERMINATES: will_return ge depth s trace)
1086  (TIME: nat)
1087  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
1088  on TIME : sub_trace_result ge depth s trace TERMINATES
1089              (λends. trace_label_label (RTLabs_status ge) ends s)
1090              (will_return_length … TERMINATES) ≝
1091             
1092match TIME return λTIME. TIME ≥ ? → ? with
1093[ O ⇒ λTERMINATES_IN_TIME. ⊥
1094| S TIME ⇒ λTERMINATES_IN_TIME.
1095
1096let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
1097  replace_sub_trace … r ?
1098    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
1099
1100] TERMINATES_IN_TIME
1101
1102
1103and make_any_label ge depth (s0:RTLabs_state ge)
1104  (trace: flat_trace io_out io_in ge s0)
1105  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1106  (STATE_COSTLABELLED: well_cost_labelled_state s0)  (* functions in the state *)
1107  (TERMINATES: will_return ge depth s0 trace)
1108  (TIME: nat)
1109  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
1110  on TIME : sub_trace_result ge depth s0 trace TERMINATES
1111              (λends. trace_any_label (RTLabs_status ge) ends s0)
1112              (will_return_length … TERMINATES) ≝
1113
1114match TIME return λTIME. TIME ≥ ? → ? with
1115[ O ⇒ λTERMINATES_IN_TIME. ⊥
1116| S TIME ⇒ λTERMINATES_IN_TIME.
1117  match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1118                                      well_cost_labelled_state s →
1119                                      ∀TM:will_return ??? trace.
1120                                      myge ? (times 3 (will_return_length ??? trace TM)) →
1121                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
1122  with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
1123  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1124                               well_cost_labelled_state s →
1125                               ∀TM:will_return ??? trace.
1126                               myge ? (times 3 (will_return_length ??? trace TM)) →
1127                               sub_trace_result ge depth (mk_RTLabs_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_state ge s stk mtc)) (will_return_length … TM) with
1128  [ ft_stop st FINAL ⇒
1129      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
1130
1131  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
1132    let start' ≝ mk_RTLabs_state ge start stk mtc in
1133    let next' ≝ next_state ? start' ?? EV in
1134    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
1135    [ cl_other ⇒ λCL.
1136        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
1137        (* We're about to run into a label. *)
1138        [ true ⇒ λCS.
1139            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1140              doesnt_end_with_ret
1141              (mk_trace_result ge … next' trace' ?
1142                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
1143        (* An ordinary step, keep going. *)
1144        | false ⇒ λCS.
1145            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
1146                replace_sub_trace ????????????? r ?
1147                  (tal_step_default (RTLabs_status ge) (ends … r)
1148                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
1149        ] (refl ??)
1150       
1151    | cl_jump ⇒ λCL.
1152        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1153          doesnt_end_with_ret
1154          (mk_trace_result ge … next' trace' ?
1155            (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
1156           
1157    | cl_call ⇒ λCL.
1158        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
1159        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
1160        (* We're about to run into a label, use base case for call *)
1161        [ true ⇒ λCS.
1162            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1163            doesnt_end_with_ret
1164            (mk_trace_result ge …
1165              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
1166                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
1167        (* otherwise use step case *)
1168        | false ⇒ λCS.
1169            let r' ≝ make_any_label ge depth
1170                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
1171                       (pi1 … (terminates … r)) TIME ? in
1172            replace_sub_trace … r' ?
1173              (tal_step_call (RTLabs_status ge) (ends … r')
1174                start' next' (new_state … r) (new_state … r') ? CL ?
1175                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
1176        ] (refl ??)
1177
1178    | cl_return ⇒ λCL.
1179        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1180          ends_with_ret
1181          (mk_trace_result ge …
1182            next'
1183            trace'
1184            ?
1185            (tal_base_return (RTLabs_status ge) start' next' ? CL)
1186            ?
1187            ?)
1188    ] (refl ? (RTLabs_classify start))
1189   
1190  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
1191] TERMINATES_IN_TIME.
1192
1193[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1194| //
1195| //
1196| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1197| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1198| @(stack_preserved_join … (stack_ok … r)) //
1199| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
1200| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1201  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1202  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1203  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1204    @(monotonic_le_times_r 3 … LT)
1205  | @le_S @le_S @le_n
1206  ]
1207| @le_S_S_to_le @TERMINATES_IN_TIME
1208| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1209| @le_n
1210| //
1211| @(proj1 … (RTLabs_costed …)) //
1212| @le_S_S_to_le @TERMINATES_IN_TIME
1213| @(wrl_nonzero … TERMINATES_IN_TIME)
1214| (* We can't reach the final state because the function terminates with a
1215     return *)
1216  inversion TERMINATES
1217  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1218  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1219  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1220  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1221  ]
1222| @(will_return_return … CL TERMINATES)
1223| @(stack_preserved_return … EV) //
1224| %{tr} %{EV} @refl
1225| @(well_cost_labelled_state_step  … EV) //
1226| whd @(will_return_notfn … TERMINATES) %2 @CL
1227| @(stack_preserved_step … EV) /2/
1228| %{tr} %{EV} %
1229| %1 whd @CL
1230| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
1231| @(well_cost_labelled_state_step  … EV) //
1232| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1233  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1234    #TMx * #LT' #_ @LT'
1235  | <EQr cases (will_return_call … CL TERMINATES)
1236    #TM' * #_ #EQ' @EQ'
1237  ]
1238| @(stack_preserved_call … EV (stack_ok … r)) //
1239| %{tr} %{EV} %
1240| @(RTLabs_after_call … next') [2: @EV | skip | // ]
1241| @(cost_labelled … r)
1242| skip
1243| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1244  @(transitive_lt … LT)
1245  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1246| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1247  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
1248| @(RTLabs_after_call … next') [2: @EV | skip | // ]
1249| %{tr} %{EV} %
1250| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
1251| @(cost_labelled … r)
1252| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1253  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1254  cases (will_return_call … TERMINATES) in GT;
1255  #X * #Y #_ #Z
1256  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1257  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1258  | //
1259  ]
1260| @(well_cost_labelled_state_step  … EV) //
1261| @(well_cost_labelled_call … EV) //
1262| cases (will_return_call … TERMINATES)
1263  #TM * #GT #_ @le_S_S_to_le
1264  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1265  @(transitive_le … TERMINATES_IN_TIME)
1266  @(monotonic_le_times_r 3 … GT)
1267| whd @(will_return_notfn … TERMINATES) %1 @CL
1268| @(stack_preserved_step … EV) /2/
1269| %{tr} %{EV} %
1270| %2 whd @CL
1271| @(well_cost_labelled_state_step  … EV) //
1272| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1273| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
1274| @CL
1275| %{tr} %{EV} %
1276| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
1277| @(well_cost_labelled_state_step  … EV) //
1278| %1 @CL
1279| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1280  @le_S_S_to_le
1281  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1282  //
1283] qed.
1284
1285(* We can initialise TIME with a suitably large value based on the length of the
1286   termination proof. *)
1287let rec make_label_return' ge depth (s:RTLabs_state ge)
1288  (trace: flat_trace io_out io_in ge s)
1289  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1290  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1291  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1292  (TERMINATES: will_return ge depth s trace)
1293  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1294make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1295  (2 + 3 * will_return_length … TERMINATES) ?.
1296@le_n
1297qed.
1298 
1299(* Tail-calls would not be handled properly (which means that if we try to show the
1300   full version with non-termination we'll fail because calls and returns aren't
1301   balanced.
1302 *)
1303
1304inductive inhabited (T:Type[0]) : Prop ≝
1305| witness : T → inhabited T.
1306
1307
1308(* Define a notion of sound labellings of RTLabs programs. *)
1309
1310definition actual_successor : state → option label ≝
1311λs. match s with
1312[ State f fs m ⇒ Some ? (next f)
1313| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1314| Returnstate _ _ _ _ ⇒ None ?
1315| Finalstate _ ⇒ None ?
1316].
1317
1318lemma nth_opt_Exists : ∀A,n,l,a.
1319  nth_opt A n l = Some A a →
1320  Exists A (λa'. a' = a) l.
1321#A #n elim n
1322[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1323| #m #IH *
1324  [ #a #E normalize in E; destruct
1325  | #a #l #a' #E %2 @IH @E
1326  ]
1327] qed.
1328
1329lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1330  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1331  RTLabs_classify s' = cl_return ∨
1332  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1333#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1334whd in ⊢ (??%? → ?);
1335generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1336[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1337| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1338| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1339| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1340| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1341| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1342| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1343| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1344| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1345| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
1346| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1347  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
1348  whd in ⊢ (??%? → ?);
1349  generalize in ⊢ (??(?%)? → ?);
1350  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1351  [ #e #E normalize in E; destruct
1352  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1353  ]
1354| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
1355] qed.
1356
1357(*
1358lemma steps_to_label_bound_inv : ∀g,l,n.
1359  steps_to_label_bound g l n →
1360  ∀H. let stmt ≝ lookup_present … g l H in
1361  ∃n'. n = steps_for_statement stmt + n' ∧
1362  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1363        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
1364        steps_to_label_bound g l' n').
1365#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
1366% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
1367qed.
1368  *) 
1369
1370(*
1371definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
1372
1373let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
1374  soundly_labelled_pc (f_graph fn) (f_entry fn).
1375
1376
1377definition soundly_labelled_frame : frame → Prop ≝
1378λf. soundly_labelled_pc (f_graph (func f)) (next f).
1379
1380definition soundly_labelled_state : state → Prop ≝
1381λs. match s with
1382[ State f _ _ ⇒ soundly_labelled_frame f
1383| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1384| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
1385].
1386*)
1387definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1388λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1389definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1390λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1391
1392inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1393| sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n
1394| sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
1395| sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n)
1396.
1397
1398lemma state_bound_on_steps_to_cost_zero : ∀s.
1399  ¬ state_bound_on_steps_to_cost s O.
1400#s % #H inversion H
1401[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1402  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1403  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1404| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1405| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1406] qed.
1407
1408lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1409  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1410  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1411  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
1412#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1413whd in ⊢ (??%? → ?);
1414generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1415[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1416| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1417| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1418| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1419| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1420| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1421| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
1422| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1423| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
1424| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1425| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1426  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
1427  whd in ⊢ (??%? → ?);
1428  generalize in ⊢ (??(?%)? → ?);
1429  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1430  [ #e #E normalize in E; destruct
1431  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1432  ]
1433| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1434] qed.
1435
1436lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
1437  state_bound_on_steps_to_cost s (S n) →
1438  ∀CL:RTLabs_classify s = cl_call.
1439  as_after_return (RTLabs_status ge) «s, CL» s' →
1440  RTLabs_cost s' = false →
1441  state_bound_on_steps_to_cost s' n.
1442#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); -stk -stk' lapply CL -CL inversion H
1443[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1444  #fn * #args * #dst * #stk * #m' #E destruct
1445| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1446  whd in S; #CL cases s'
1447  [ #f' #fs' #m' * #N #F #CS
1448    %1 whd
1449    inversion S
1450    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1451      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1452    | #l #n #B #E1 #E2 #_ destruct <N <F @B
1453    ]
1454  | #fd' #args' #dst' #fs' #m' *
1455  | #rv #dst' #fs' #m' *
1456  | #r #E normalize in E; destruct
1457  ]
1458| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1459] qed.
1460
1461lemma bound_after_step : ∀ge,s,tr,s',n.
1462  state_bound_on_steps_to_cost s (S n) →
1463  eval_statement ge s = Value ??? 〈tr, s'〉 →
1464  RTLabs_cost s' = false →
1465  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1466   state_bound_on_steps_to_cost s' n.
1467#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1468[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1469  #EVAL cases (eval_successor … EVAL)
1470  [ /3/
1471  | * #l * #S1 #S2 #NC %2
1472  (*
1473    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1474    *)
1475    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1476    inversion (eval_preserves … EVAL)
1477    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1478      >(eval_steps … EVAL) in E2; #En normalize in En;
1479      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1480      %1 inversion (IH … S2)
1481      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1482        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1483        whd in S1:(??%?); destruct >NC in CSx; *
1484      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
1485      ]
1486    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1487      >(eval_steps … EVAL) in E2; #En normalize in En;
1488      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1489      %2 @IH normalize in S1; destruct @S2
1490    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1491      destruct
1492    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1493      normalize in S1; destruct
1494    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1495    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1496    ]
1497  ]
1498| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1499  /3/
1500| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1501  #EVAL #NC %2 inversion (eval_preserves … EVAL)
1502  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1503  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1504  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1505  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1506  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
1507    %1 whd in FS ⊢ %;
1508    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
1509    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
1510    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
1511    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1512    inversion FS
1513    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1514        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
1515        >NC in CSx; *
1516    | #lx #nx #H #E1x #E2x #_ destruct @H
1517    ]
1518  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1519  ]
1520] qed.
1521
1522
1523
1524
1525definition soundly_labelled_ge : genv → Prop ≝
1526λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1527
1528definition soundly_labelled_state : state → Prop ≝
1529λs. match s with
1530[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1531| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1532                          All ? (λf. soundly_labelled_fn (func f)) fs
1533| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1534| Finalstate _ ⇒ True
1535].
1536
1537lemma steps_from_sound : ∀s.
1538  RTLabs_cost s = true →
1539  soundly_labelled_state s →
1540  ∃n. state_bound_on_steps_to_cost s n.
1541* [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
1542whd in ⊢ (% → ?); * #SLF #_
1543cases (SLF (next f) (next_ok f)) #n #B1
1544%{n} % @B1
1545qed.
1546
1547lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1548  soundly_labelled_ge ge →
1549  eval_statement ge s = Value ??? 〈tr,s'〉 →
1550  soundly_labelled_state s →
1551  soundly_labelled_state s'.
1552#ge #s #tr #s' #ENV #EV #S
1553inversion (eval_preserves … EV)
1554[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1555  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1556| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1557  whd in S ⊢ %; %
1558  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1559  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1560  ]
1561| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1562  whd in S ⊢ %; @S
1563| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1564  whd in S ⊢ %; cases S //
1565| #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
1566  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1567| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1568] qed.
1569
1570lemma soundly_labelled_state_preserved : ∀s,s'.
1571  stack_preserved ends_with_ret s s' →
1572  soundly_labelled_state s →
1573  soundly_labelled_state s'.
1574#s0 #s0' #SP inversion SP
1575[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1576| #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
1577  inversion S1
1578  [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
1579    * #_ #S whd in S;
1580    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1581    destruct @S
1582  | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
1583    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1584    destruct @S
1585  | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
1586    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1587    destruct @S
1588  ]
1589| //
1590| //
1591] qed.
1592
1593(* When constructing an infinite trace, we need to be able to grab the finite
1594   portion of the trace for the next [trace_label_diverges] constructor.  We
1595   use the fact that the trace is soundly labelled to achieve this. *)
1596
1597record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1598  ro_well_cost_labelled: well_cost_labelled_state s;
1599  ro_soundly_labelled: soundly_labelled_state s;
1600  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1601  ro_not_final: RTLabs_is_final s = None ?
1602}.
1603
1604inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
1605| fp_tal : ∀s,s':RTLabs_state ge.
1606           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1607           ∀t:flat_trace io_out io_in ge s'.
1608           remainder_ok ge s' t →
1609           finite_prefix ge s
1610| fp_tac : ∀s1,s2,s3:RTLabs_state ge.
1611           trace_any_call (RTLabs_status ge) s1 s2 →
1612           well_cost_labelled_state s2 →
1613           as_execute (RTLabs_status ge) s2 s3 →
1614           ∀t:flat_trace io_out io_in ge s3.
1615           remainder_ok ge s3 t →
1616           finite_prefix ge s1
1617.
1618
1619definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
1620  RTLabs_classify s = cl_other →
1621  finite_prefix ge s' →
1622  as_execute (RTLabs_status ge) s s' →
1623  RTLabs_cost s' = false →
1624  finite_prefix ge s ≝
1625λge,s,s',OTHER,fp.
1626match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
1627[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1628    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1629    rem rok
1630| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
1631    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1632    WCL2 EV rem rok
1633].
1634
1635definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
1636  as_execute (RTLabs_status ge) s s1 →
1637  ∀CALL:RTLabs_classify s = cl_call.
1638  finite_prefix ge s'' →
1639  trace_label_return (RTLabs_status ge) s1 s'' →
1640  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1641  RTLabs_cost s'' = false →
1642  finite_prefix ge s ≝
1643λge,s,s1,s'',EVAL,CALL,fp.
1644match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with
1645[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1646    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1647    rem rok
1648| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
1649    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1650    WCL2 EV rem rok
1651].
1652
1653lemma not_return_to_not_final : ∀ge,s,tr,s'.
1654  eval_statement ge s = Value ??? 〈tr, s'〉 →
1655  RTLabs_classify s ≠ cl_return →
1656  RTLabs_is_final s' = None ?.
1657#ge #s #tr #s' #EV
1658inversion (eval_preserves … EV) //
1659#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1660@⊥ @(absurd ?? CL) @refl
1661qed.
1662
1663definition termination_oracle ≝ ∀ge,depth,s,trace.
1664  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1665
1666let rec finite_segment ge (s:RTLabs_state ge) n trace
1667  (ORACLE: termination_oracle)
1668  (TRACE_OK: remainder_ok ge s trace)
1669  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1670  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1671  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1672  on n : finite_prefix ge s ≝
1673match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1674[ O ⇒ λLABEL_LIMIT. ⊥
1675| S n' ⇒
1676  match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace'.
1677    match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_state ge s ? mtc) with
1678    [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
1679    | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
1680        let start' ≝ mk_RTLabs_state ge start stk mtc in
1681        let next' ≝ next_state ge start' next tr EV in
1682        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1683        [ cl_other ⇒ λCL.
1684            let TRACE_OK' ≝ ? in
1685            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1686            [ true ⇒ λCS.
1687                fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
1688            | false ⇒ λCS.
1689                let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1690                fp_add_default ge start' next' CL fs ? CS
1691            ] (refl ??)
1692        | cl_jump ⇒ λCL.
1693            fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
1694        | cl_call ⇒ λCL.
1695            match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
1696            [ or_introl TERMINATES ⇒
1697              match TERMINATES with [ witness TERMINATES ⇒
1698                let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1699                let TRACE_OK' ≝ ? in
1700                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
1701                [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'
1702                | false ⇒ λCS.
1703                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1704                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
1705                ] (refl ??)
1706              ]
1707            | or_intror NO_TERMINATION ⇒
1708                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?
1709            ]
1710        | cl_return ⇒ λCL. ⊥
1711        ] (refl ??)
1712    ] mtc0
1713  ] trace TRACE_OK
1714] LABEL_LIMIT.
1715[ cases (state_bound_on_steps_to_cost_zero s) /2/
1716| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1717| @(absurd ?? (ro_no_termination … TRACE_OK))
1718     %{0} % @wr_base //
1719| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
1720| 5,6,9,10,11: /3/
1721| cases TRACE_OK #H1 #H2 #H3 #H4
1722  % [ @(well_cost_labelled_state_step … EV) //
1723    | @(soundly_labelled_state_step … EV) //
1724    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1725    | @(not_return_to_not_final … EV) >CL % #E destruct
1726    ]
1727| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
1728| @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
1729| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
1730  @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
1731| % [ /2/
1732    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
1733      @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
1734    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1735      @wr_call //
1736      @(will_return_prepend … TERMINATES … TM1)
1737      cases (terminates … tlr) //
1738    | (* By stack preservation we cannot be in the final state *)
1739      inversion (stack_ok … tlr)
1740      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1741      | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1742      | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct whd in S:(??%); -next' -s0
1743        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
1744        inversion (eval_preserves … EV)
1745        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 @⊥ -next destruct ]
1746        #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1747        inversion S
1748        [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
1749        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1750           so we can use it as a witness that at least one frame exists *)
1751        inversion LABEL_LIMIT
1752        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1753      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1754      ]
1755    ]
1756| @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
1757| @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
1758| /2/
1759| %{tr} %{EV} %
1760| cases TRACE_OK #H1 #H2 #H3 #H4
1761  % [ @(well_cost_labelled_state_step … EV) /2/
1762    | @(soundly_labelled_state_step … EV) /2/
1763    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1764      @(will_return_lower … TM) //
1765    | @(not_return_to_not_final … EV) >CL % #E destruct
1766    ]
1767| %2 @CL
1768| 21,22: %{tr} %{EV} %
1769| cases (bound_after_step … LABEL_LIMIT EV ?)
1770  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
1771    inversion trace'
1772    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1773      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1774      % >CL #E destruct
1775    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1776      @wr_base //
1777    ]
1778    ]
1779    | >CL #E destruct
1780    ]
1781  | //
1782  | //
1783  ]
1784| cases TRACE_OK #H1 #H2 #H3 #H4
1785  % [ @(well_cost_labelled_state_step … EV) //
1786    | @(soundly_labelled_state_step … EV) //
1787    | @(not_to_not … (ro_no_termination … TRACE_OK))
1788      * #depth * #TERM %{depth} % @wr_step /2/
1789    | @(not_return_to_not_final … EV) >CL % #E destruct
1790    ]
1791] qed.
1792
1793(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1794       a trace_label_diverges value, but I only know how to construct those
1795       using a cofixpoint in Type[0], which means I can't use the termination
1796       oracle.
1797*)
1798
1799let corec make_label_diverges ge (s:RTLabs_state ge)
1800  (trace: flat_trace io_out io_in ge s)
1801  (ORACLE: termination_oracle)
1802  (TRACE_OK: remainder_ok ge s trace)
1803  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1804  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1805  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1806  : trace_label_diverges_exists (RTLabs_status ge) s ≝
1807match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
1808[ ex_intro n B ⇒
1809    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
1810      return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1811    with
1812    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1813        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1814            tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
1815(*
1816        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1817        [ ex_intro T' _ ⇒
1818            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1819        ]*)
1820    | fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1821        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1822            tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
1823(*
1824        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1825        [ ex_intro T' _ ⇒
1826            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1827        ]*)
1828    ] STATEMENT_COSTLABEL
1829].
1830[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
1831| @EV
1832| @(trace_any_call_call … T)
1833| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T)
1834] qed.
1835
1836lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'.
1837  make_initial_state p = OK ? s1 →
1838  eval_statement ge s1 = Value ??? 〈tr,s2〉 →
1839  stack_preserved ends_with_ret s2 s' →
1840  RTLabs_is_final s' ≠ None ?.
1841#ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?);
1842@bind_ok #m #_
1843@bind_ok #b #_
1844@bind_ok #f #_
1845#E destruct
1846#EV #SP inversion (eval_preserves … EV)
1847[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
1848     inversion SP
1849     [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct
1850     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct
1851          inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct
1852     ]
1853| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct
1854] qed.
1855
1856lemma initial_state_is_call : ∀p,s.
1857  make_initial_state p = OK ? s →
1858  RTLabs_classify s = cl_call.
1859#p #s whd in ⊢ (??%? → ?);
1860@bind_ok #m #_
1861@bind_ok #b #_
1862@bind_ok #f #_
1863#E destruct
1864@refl
1865qed.
1866
1867let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
1868  (ORACLE: termination_oracle)
1869  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1870  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1871  : ∀trace: flat_trace io_out io_in ge s.
1872    ∀INITIAL: make_initial_state p = OK state s.
1873    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
1874    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
1875    trace_whole_program_exists (RTLabs_status ge) s ≝
1876match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1877                   make_initial_state p = OK ? s →
1878                   well_cost_labelled_state s →
1879                   soundly_labelled_state s →
1880                   trace_whole_program_exists (RTLabs_status ge) s with
1881[ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace.
1882match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1883                             make_initial_state p = OK state s →
1884                             well_cost_labelled_state s →
1885                             soundly_labelled_state s →
1886                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
1887[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
1888    let IS_CALL ≝ initial_state_is_call … INITIAL in
1889    let s' ≝ mk_RTLabs_state ge s stk mtc in
1890    let next' ≝ next_state ge s' next tr EV in
1891    match ORACLE ge O next trace' with
1892    [ or_introl TERMINATES ⇒
1893        match TERMINATES with
1894        [ witness TERMINATES ⇒
1895          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1896          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
1897        ]
1898    | or_intror NO_TERMINATION ⇒
1899        twp_diverges (RTLabs_status ge) s' next' IS_CALL ?
1900         (make_label_diverges ge next' trace' ORACLE ?
1901            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1902    ]
1903| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
1904] mtc0 ].
1905[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
1906  cases FINAL #E @E @refl
1907| %{tr} %{EV} %
1908| @(after_the_initial_call_is_the_final_state … INITIAL EV)
1909  @(stack_ok … tlr)
1910| @(well_cost_labelled_state_step … EV) //
1911| @(well_cost_labelled_call … EV) //
1912| %{tr} %{EV} %
1913| @(well_cost_labelled_call … EV) //
1914| % [ @(well_cost_labelled_state_step … EV) //
1915    | @(soundly_labelled_state_step … EV) //
1916    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1917    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1918    ]
1919] qed.
1920
1921(*
1922theorem program_trace_exists :
1923  termination_oracle →
1924  ∀p:RTLabs_program.
1925  ∀s:state.
1926  ∀I: make_initial_state p = OK ? s.
1927 
1928  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
1929 
1930  ∀NOIO:exec_no_io … plain_trace.
1931 
1932  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
1933 
1934  trace_whole_program_exists (RTLabs_status (make_global p)) s.
1935#ORACLE #p #s #I
1936letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
1937#NOIO
1938letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
1939whd
1940@(whole_structured_trace_exists … flat_trace)
1941//
1942[ whd
1943*)
1944
1945lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
1946  as_execute (RTLabs_status ge) s s' →
1947  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
1948#ge #s #s' * #tr * #EX #_ %{tr} @EX
1949qed.
1950
1951(* as_execute might be in Prop, but because the semantics is deterministic
1952   we can retrieve the event trace anyway. *)
1953
1954let rec deprop_execute ge (s,s':state)
1955  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
1956: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1957match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
1958[ Value ts ⇒ λY. «fst … ts, ?»
1959| _ ⇒ λY. ⊥
1960] X.
1961[ 1,3: cases Y #x #E destruct
1962| cases Y #trP #E destruct @refl
1963] qed.
1964
1965let rec deprop_as_execute ge (s,s':RTLabs_state ge)
1966  (X:as_execute (RTLabs_status ge) s s')
1967: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
1968deprop_execute ge s s' ?.
1969cases X #tr * #EX #_ %{tr} @EX
1970qed.
1971
1972(* A non-empty finite section of a flat_trace *)
1973inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
1974| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
1975| pft_step : ∀s,tr,s',s''. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s' s'' → partial_flat_trace o i ge s s''.
1976
1977let rec append_partial_flat_trace o i ge s1 s2 s3
1978  (tr1:partial_flat_trace o i ge s1 s2)
1979on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
1980match tr1 with
1981[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
1982| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
1983].
1984
1985let rec partial_to_flat_trace o i ge s1 s2
1986  (tr:partial_flat_trace o i ge s1 s2)
1987on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
1988match tr with
1989[ pft_base s tr s' EX ⇒ ft_step … EX
1990| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
1991].
1992
1993(* Extract a flat trace from a structured one. *)
1994let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
1995  (tr:trace_label_return (RTLabs_status ge) s s')
1996on tr :
1997  partial_flat_trace io_out io_in ge s s' ≝
1998match tr with
1999[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
2000| tlr_step s1 s2 s3 tll tlr ⇒
2001  append_partial_flat_trace …
2002    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
2003    (flat_trace_of_label_return ge s2 s3 tlr)
2004]
2005and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
2006  (tr:trace_label_label (RTLabs_status ge) ends s s')
2007on tr :
2008  partial_flat_trace io_out io_in ge s s' ≝
2009match tr with
2010[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
2011]
2012and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
2013  (tr:trace_any_label (RTLabs_status ge) ends s s')
2014on tr :
2015  partial_flat_trace io_out io_in ge s s' ≝
2016match tr with
2017[ tal_base_not_return s1 s2 EX CL CS ⇒
2018    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2019    pft_base … EX' ]
2020| tal_base_return s1 s2 EX CL ⇒
2021    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2022    pft_base … EX' ]
2023| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
2024    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
2025    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2026    pft_step … EX' suffix' ]
2027| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
2028    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2029    pft_step … EX'
2030      (append_partial_flat_trace …
2031        (flat_trace_of_label_return ge ?? tlr)
2032        (flat_trace_of_any_label ge ??? tal))
2033    ]
2034| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
2035    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2036      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
2037    ]
2038].
2039
2040
2041(* We take an extra step so that we can always return a non-empty trace to
2042   satisfy the guardedness condition in the cofixpoint. *)
2043let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
2044  (tr:trace_any_call (RTLabs_status ge) s s')
2045  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2046on tr :
2047  partial_flat_trace io_out io_in ge s s'' ≝
2048match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
2049[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
2050| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
2051    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
2052    pft_step … EX'
2053      (append_partial_flat_trace …
2054        (flat_trace_of_label_return ge ?? tlr)
2055        (flat_trace_of_any_call ge … tac EX''))
2056    ]
2057| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
2058    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2059    pft_step … EX'
2060     (flat_trace_of_any_call ge … tal EX'')
2061    ]
2062] EX''.
2063
2064let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
2065  (tr:trace_label_call (RTLabs_status ge) s s')
2066  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2067on tr :
2068  partial_flat_trace io_out io_in ge s s'' ≝
2069match tr with
2070[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
2071] EX''.
2072
2073(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
2074   to take care to satisfy the guardedness condition by witnessing the fact that
2075   the partial traces are non-empty. *)
2076let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
2077  (tr:trace_label_diverges (RTLabs_status ge) s)
2078: flat_trace io_out io_in ge s ≝
2079match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
2080[ tld_step sx sy tll tld ⇒
2081  match sy in RTLabs_state return λsy:RTLabs_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_state sy' stk mtc0 ⇒
2082    λtll.
2083    match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s2 stk mtc) → flat_trace ??? s1 with
2084    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2085    | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
2086    ] mtc0 ] tll tld
2087| tld_base s1 s2 s3 tlc EX CL tld ⇒
2088  match s3 in RTLabs_state return λs3:RTLabs_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_state s3' stk mtc0 ⇒
2089    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2090      match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s3 stk mtc) → flat_trace ??? s1 with
2091      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2092      | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_state ge s3 stk mtc) tr' tld)
2093      ] mtc0
2094    ]
2095  ] EX tld
2096]
2097(* Helper to keep adding the partial trace without violating the guardedness
2098   condition. *)
2099and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
2100: partial_flat_trace io_out io_in ge s s' →
2101  trace_label_diverges (RTLabs_status ge) s' →
2102  flat_trace io_out io_in ge s ≝
2103match s' return λs':RTLabs_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_state sx stk mtc ⇒
2104λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_state ge s' ? mtc) → flat_trace io_out io_in ge s with
2105[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
2106| pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_state ge s3 stk mtc) tr' tr)
2107] mtc ]
2108.
2109
2110
2111coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2112| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2113| eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2).
2114
2115(* XXX move to semantics *)
2116lemma final_cannot_move : ∀ge,s.
2117  RTLabs_is_final s ≠ None ? →
2118  ∃err. eval_statement ge s = Wrong ??? err.
2119#ge *
2120[ #f #fs #m * #F cases (F ?) @refl
2121| #a #b #c #d #e * #F cases (F ?) @refl
2122| #a #b #c #d * #F cases (F ?) @refl
2123| #r #F % [2: @refl | skip ]
2124] qed.
2125
2126let corec flat_traces_are_determined_by_starting_point ge s tr1
2127: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2128match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2129[ ft_stop s F ⇒ λtr2. ?
2130| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2131    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2132    [ ft_stop s F ⇒ λEX. ?
2133    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2134    ] EX0
2135].
2136[ inversion tr2 in tr1 F;
2137  [ #s #F #_ #_ #tr1 #F' @eft_stop
2138  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2139    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2140  ]
2141| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2142| -EX0
2143  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2144  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2145  -E -EX' -tr2' #tr2' #EX'
2146  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2147  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2148  -E -EX' #EX'
2149    @eft_step @flat_traces_are_determined_by_starting_point
2150] qed.
2151
2152let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
2153  (str:trace_label_diverges (RTLabs_status ge) s)
2154  (tr:flat_trace io_out io_in ge s)
2155: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
2156@flat_traces_are_determined_by_starting_point
2157qed.
2158
2159let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
2160  (tr:trace_whole_program (RTLabs_status ge) s)
2161on tr : flat_trace io_out io_in ge s ≝
2162match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
2163[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2164    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2165      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
2166    ]
2167| twp_diverges s1 s2 CL EX tld ⇒
2168    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2169      ft_step … EX' (flat_trace_of_label_diverges … tld)
2170    ]
2171].
2172
2173let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
2174  (str:trace_whole_program (RTLabs_status ge) s)
2175  (tr:flat_trace io_out io_in ge s)
2176: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
2177@flat_traces_are_determined_by_starting_point
2178qed.
Note: See TracBrowser for help on using the repository browser.