source: src/RTLabs/Traces.ma @ 2294

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

Add instruction pointer for call states in RTLabs.

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