source: src/RTLabs/Traces.ma @ 2307

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

Half the proofs for sound cost labelling check.

File size: 136.1 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "RTLabs/CostSpec.ma".
4include "common/StructuredTraces.ma".
5include "common/Executions.ma".
6include "utilities/deqsets.ma".
7
8discriminator status_class.
9
10(* We augment states with a stack of function blocks (i.e. pointers) so that we
11   can make sensible "program counters" for the abstract state definition, along
12   with a proof that we will get the correct code when we do the lookup (which
13   is done to find cost labels given a pc).
14   
15   Adding them to the semantics is an alternative, more direct approach.
16   However, it makes animating the semantics extremely difficult, because it
17   is hard to avoid normalising and displaying irrelevant parts of the global
18   environment and proofs.
19   
20   We use blocks rather than identifiers because the global environments go
21
22     identifier → block → definition
23   
24   and we'd have to introduce backwards lookups to find identifiers for
25   function pointers.
26 *)
27
28definition Ras_Fn_Match ≝
29λge,state,fn_stack.
30  match state with
31  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
32  | Callstate fd _ _ fs _ ⇒
33      match fn_stack with
34      [ nil ⇒ False
35      | cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧
36        All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t
37      ]
38  | Returnstate _ _ fs _ ⇒
39      All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack
40  | Finalstate _ ⇒ fn_stack = [ ]
41  ].
42
43record RTLabs_state (ge:genv) : Type[0] ≝ {
44  Ras_state :> state;
45  Ras_fn_stack : list block;
46  Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack
47}.
48
49(* Given a plain step of the RTLabs semantics, give the next state along with
50   the shadow stack of function block numbers.  Carefully defined so that the
51   coercion back to the plain state always reduces. *)
52definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.
53  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝
54λge,s,s',t,EX. mk_RTLabs_state ge s'
55 (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)
56 ?.
57cases s' in EX ⊢ %;
58[ -s' #f #fs #m cases s -s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)
59  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
60    whd cases stk in mtc ⊢ %; [ * ]
61    #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //
62    | @M2 ]
63  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
64  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
65    whd cases stk in mtc ⊢ %; [ * ]
66    #hd #tl #H @H
67  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
68  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
69    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
70    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
71  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
72  ]
73| -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
74  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
75  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
76  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
77    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
78    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
79  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
80  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
81  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
82  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
83  ]
84| -s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
85  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
86  | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
87  | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
88  | #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct
89    cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H
90  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
91  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
92  ]
93| #r #EX whd @refl
94] qed.
95
96
97(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
98       will be added later (LTL → LIN). *)
99
100definition RTLabs_classify : state → status_class ≝
101λs. match s with
102[ State f _ _ ⇒
103    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
104    [ St_cond _ _ _ ⇒ cl_jump
105(*    | St_jumptable _ _ ⇒ cl_jump*)
106    | _ ⇒ cl_other
107    ]
108| Callstate _ _ _ _ _ ⇒ cl_call
109| Returnstate _ _ _ _ ⇒ cl_return
110| Finalstate _ ⇒ cl_other
111].
112
113(* As with is_cost_label/cost_label_of we define a boolean function as well
114   as one which extracts the cost label so that we can use it in hypotheses
115   without naming the cost label. *)
116
117definition RTLabs_cost : state → bool ≝
118λs. match s with
119[ State f fs m ⇒
120    is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
121| _ ⇒ false
122].
123
124definition RTLabs_cost_label : state → option costlabel ≝
125λs. match s with
126[ State f fs m ⇒
127    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
128| _ ⇒ None ?
129].
130
131(* "Program counters" need to identify the current state, either as a pair of
132   the function and current instruction, or the function being entered or
133   left.  Functions are identified by their function pointer block because
134   this avoids introducing functions to map back pointers to function ids using
135   the global environment.  (See the comment at the start of this file, too.)
136   
137   Calls also get the caller's instruction label (or None for the initial call)
138   so that we can distinguish different calls.  This is used only for the
139   t.*_unrepeating property, which includes the pc for call states.
140    *)
141
142inductive RTLabs_pc : Type[0] ≝
143| rapc_state : block → label → RTLabs_pc
144| rapc_call : option label → block → RTLabs_pc
145| rapc_ret : option block → RTLabs_pc
146| rapc_fin : RTLabs_pc
147.
148
149definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
150λx,y. match x with
151[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
152| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
153    eqb ? o1 o2
154    ∧ eq_block b1 b2
155  | _ ⇒ false ]
156| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
157| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
158].
159
160definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
161whd in match RTLabs_pc_eq;
162* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
163* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
164normalize nodelta
165[ @eq_block_elim [ #E destruct | * #NE ] ]
166[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
167[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
168[ @eq_block_elim [ #E destruct | * #NE ] ]
169normalize % #E destruct try (cases (NE (refl ??))) @refl
170qed.
171
172definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝
173λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒
174match s' return λs'. Ras_Fn_Match ? s' ? → ? with
175[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
176| 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 ]
177| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
178| Finalstate _ ⇒ λmtc. rapc_fin
179] mtc0 ].
180whd in mtc; cases mtc
181qed.
182
183definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝
184λge,pc.
185match pc with
186[ rapc_state b l ⇒
187  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
188    match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s | _ ⇒ None ? ] | _ ⇒ None ? ] ]
189| _ ⇒ None ?
190].
191
192(* After returning from a function, we should be ready to execute the next
193   instruction of the caller and the shadow stack should be preserved (we have
194   to take the top element off because the Callstate includes the callee); *or*
195   we're in the final state.
196 *)
197
198definition RTLabs_after_return : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → RTLabs_state ge → Prop ≝
199λge,s,s'.
200  match s with
201  [ mk_Sig s p ⇒
202    match s return λs. RTLabs_classify s = cl_call → ? with
203    [ Callstate fd args dst stk m ⇒
204      λ_. match s' with
205      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
206          next h = next f ∧
207          f_graph (func h) = f_graph (func f) ∧
208          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
209      | Finalstate r ⇒ stk = [ ]
210      | _ ⇒ False
211      ]
212   | State f fs m ⇒ λH.⊥
213   | _ ⇒ λH.⊥
214   ] p
215 ].
216[ whd in H:(??%?);
217  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
218  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
219| normalize in H; destruct
220| normalize in H; destruct
221] qed.
222
223
224definition RTLabs_status : genv → abstract_status ≝
225λge.
226  mk_abstract_status
227    (RTLabs_state ge)
228    (λs,s'. ∃t,EX. next_state ge s s' t EX = s')
229    RTLabs_deqset
230    (RTLabs_state_to_pc ge)
231    (λs,c. RTLabs_classify s = c)
232    (RTLabs_pc_to_cost_label ge)
233    (RTLabs_after_return ge)
234  (λs. RTLabs_is_final s ≠ None ?).
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 #N * #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' #WS
726  cases (andb_Prop_true … WS) #H1 #H2 [ @H1 | @H2 ]
727(*| * #r * #ls #Estmt
728  >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs
729  >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
730  >Estmt #LP whd in ⊢ (??%? → ?);
731  (* replace with lemma on successors? *)
732  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
733  [ 2: (* later *)
734  | *: #E destruct
735  ]
736  lapply (Hbody (next fr) (next_ok fr))
737  generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP
738  generalize in ⊢ (??(?%)? → ?);
739  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
740  [ #E1 #E2 whd in E2:(??%?); destruct
741  | #l' #E1 #E2 whd in E2:(??%?); destruct
742    cases (All_nth ???? CP ? E1)
743    #H1 #H2 @H2
744  ]
745]*) qed.
746
747lemma rtlabs_call_inv : ∀s.
748  RTLabs_classify s = cl_call →
749  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
750* [ #f #fs #m whd in ⊢ (??%? → ?);
751    cases (lookup_present … (next f) (next_ok f)) normalize
752    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
753  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
754  | normalize #H411 #H412 #H413 #H414 #H415 destruct
755  | normalize #H1 #H2 destruct
756  ] qed.
757
758lemma well_cost_labelled_call : ∀ge,s,tr,s'.
759  eval_statement ge s = Value ??? 〈tr,s'〉 →
760  well_cost_labelled_state s →
761  RTLabs_classify s = cl_call →
762  RTLabs_cost s' = true.
763#ge #s #tr #s' #EV #WCL #CL
764cases (rtlabs_call_inv s CL)
765#fd * #args * #dst * #stk * #m #E >E in EV WCL;
766whd in ⊢ (??%? → % → ?);
767cases fd
768[ #fn whd in ⊢ (??%? → % → ?);
769  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
770  #m' #b whd in ⊢ (??%? → ?); #E' destruct
771  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
772  @WCL2
773| #fn whd in ⊢ (??%? → % → ?);
774  @bindIO_value #evargs #Eargs
775  whd in ⊢ (??%? → ?);
776  #E' destruct
777] qed.
778
779
780(* Extend our information about steps to states extended with the shadow stack. *)
781
782inductive state_rel_ext : ∀ge:genv. RTLabs_state ge → RTLabs_state ge → Prop ≝
783| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (State f' fs m') S M')
784| xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M')
785| xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
786| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) (mk_RTLabs_state ge (Returnstate rtv dst fs m') S M')
787| xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_state ge (State f' fs m) S M')
788| xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_state ge (Finalstate r) [ ] M')
789.
790
791lemma eval_preserves_ext : ∀ge,s,s'.
792  as_execute (RTLabs_status ge) s s' →
793  state_rel_ext ge s s'.
794#ge0 * #s #S #M * #s' #S' #M' * #tr * #EX
795generalize in match M'; -M'
796generalize in match M; -M
797generalize in match EX;
798inversion (eval_preserves … EX)
799[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct
800  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
801  %1 //
802| #ge #f #fs #m #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
803  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
804  %2 //
805| #ge #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
806  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
807  %3
808| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
809  cases S [ #EX' * ] #fn #S
810  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
811  %4
812| #ge #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
813  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
814  %5 //
815| #ge #r #dst #m #E1 #E2 #E3 #E4 destruct
816  cases S [ 2: #h #t #EX' * ]
817  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
818  %6
819] qed.
820
821
822
823(* The preservation of (most of) the stack is useful to show as_after_return.
824   We do this by showing that during the execution of a function the lower stack
825   frames never change, and that after returning from the function we preserve
826   the identity of the next instruction to execute.
827   
828   We also show preservation of the shadow stack of function pointers.  As with
829   the real stack, we ignore the current function.
830 *)
831
832inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_state ge → Prop ≝
833| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (State f fs m) (fn::S) M)
834| sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
835| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Returnstate rtv dst fs m) S M)
836.
837
838inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_state ge → RTLabs_state ge → Prop ≝
839| sp_normal : ∀fs,S,s1,s2.
840    stack_of_state ge fs S s1 →
841    stack_of_state ge fs S s2 →
842    stack_preserved ge doesnt_end_with_ret s1 s2
843| sp_finished : ∀s1,f,f',fs,m,fn,S,M.
844    next f = next f' →
845    frame_rel f f' →
846    stack_of_state ge (f::fs) (fn::S) s1 →
847    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (State f' fs m) (fn::S) M)
848| sp_stop : ∀s1,r,M.
849    stack_of_state ge [ ] [ ] s1 →
850    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (Finalstate r) [ ] M)
851| sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
852    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_state ge (Finalstate r) [ ] M2)
853.
854
855discriminator list.
856
857lemma stack_of_state_eq : ∀ge,fs,fs',S,S',s.
858  stack_of_state ge fs S s →
859  stack_of_state ge fs' S' s →
860  fs = fs' ∧ S = S'.
861#ge #fs0 #fs0' #S0 #S0' #s0 *
862[ #f #fs #m #fn #S #M #H inversion H
863  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
864| #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
865  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o destruct /2/
866| #rtv #dst #fs #m #S #M #H inversion H
867  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
868] qed.
869
870lemma stack_preserved_final : ∀ge,e,r,S,M,s.
871  ¬stack_preserved ge e (mk_RTLabs_state ge (Finalstate r) S M) s.
872#ge #e #r #S #M #s % #H inversion H
873[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
874  inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m destruct
875| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
876  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m destruct
877| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
878  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o destruct
879| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
880] qed.
881
882lemma stack_preserved_join : ∀ge,e,s1,s2,s3.
883  stack_preserved ge doesnt_end_with_ret s1 s2 →
884  stack_preserved ge e s2 s3 →
885  stack_preserved ge e s1 s3.
886#ge #e1 #s1 #s2 #s3 #H1 inversion H1
887[ #fs #S #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
888  #H2 inversion H2
889  [ #fs' #S' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
890    @(sp_normal ge fs S) // cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
891  | #s1'' #f #f' #fs' #m #fn #S' #M #N #F #S1' #E1 #E2 #E3 #E4 destruct
892    @(sp_finished … fn … N) cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
893  | #s1'' #r #M #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop cases (stack_of_state_eq … S1'' S2) #E1 #E2 destruct //
894  | #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
895    inversion S2
896    [ #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
897    | #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
898    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
899    ]
900  ]
901| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
902| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
903| #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
904  @(absurd … F) //
905] qed.
906
907(* Proof that steps preserve the stack.  For calls we show that a stack
908   preservation proof for the called function gives us enough to show
909   stack preservation for the caller between the call and the state after
910   returning. *)
911
912lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_state ge.∀cl.
913  RTLabs_classify s1 = cl →
914  as_execute (RTLabs_status ge) s1 s2 →
915  match cl with
916  [ cl_call ⇒ ∀s3. stack_preserved ge ends_with_ret s2 s3 →
917                   stack_preserved ge doesnt_end_with_ret s1 s3
918  | cl_return ⇒ stack_preserved ge ends_with_ret s1 s2
919  | _ ⇒ stack_preserved ge doesnt_end_with_ret s1 s2
920  ].
921#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
922[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
923  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
924| #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
925  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
926| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
927  * #s3 #S3 #M3 #SP inversion SP
928  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
929  | #s1 #f #f' #fs' #m3 #fn3 #S3' #M3' #E1 #E2 #SOS #E4 #E5 #E6 #E7 destruct
930    @(sp_normal … fs' S3') //
931    inversion SOS
932    [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct //
933    | #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
934    | #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
935    ]
936  | #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
937    cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 destruct /3/ ]
938    * #fn * #E1 #E2 destruct
939    @sp_top
940  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
941  ]
942| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
943  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) /2/
944| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
945  cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
946| #ge #r #dst #m #M #M' #E1 #E2 #E3 #E4 destruct whd /2/
947] qed.
948
949lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_state ge.∀s2,tr.
950  ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
951  as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
952#ge #s1 #s2 #tr #EV %{tr} %{EV} %
953qed.
954
955lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.
956  ∀CL : RTLabs_classify s1 = cl_call.
957  as_execute (RTLabs_status ge) s1 s2 →
958  stack_preserved ge ends_with_ret s2 s3 →
959  as_after_return (RTLabs_status ge) «s1,CL» s3.
960#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
961cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
962whd
963inversion S23
964[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
965| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
966  inversion (eval_preserves_ext … EV)
967  [ 3: #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
968    inversion S
969    [ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N | inversion F // ] | whd % ]
970    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 destruct
971    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
972    ]
973  | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 destruct
974  ]
975| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
976  inversion (eval_preserves_ext … EV)
977  [ 3: #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
978    inversion S1
979    [ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
980    | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 destruct
981    ]
982  | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 destruct
983  ]
984| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
985] qed.
986
987(* Don't need to know that labels break loops because we have termination. *)
988
989(* A bit of mucking around with the depth to avoid proving termination after
990   termination.  Note that we keep a proof that our upper bound on the length
991   of the termination proof is respected. *)
992record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret)
993  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
994  (original_terminates: will_return ge depth start full)
995  (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
996{
997  new_state : RTLabs_state ge;
998  remainder : flat_trace io_out io_in ge new_state;
999  cost_labelled : well_cost_labelled_state new_state;
1000  new_trace : T new_state;
1001  stack_ok : stack_preserved ge ends start new_state;
1002  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
1003               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
1004               | S d ⇒ ΣTM:will_return ge d new_state remainder.
1005                         gt limit (will_return_length … TM) ∧
1006                         will_return_end … original_terminates = will_return_end … TM
1007               ]
1008}.
1009
1010(* The same with a flag indicating whether the function returned, as opposed to
1011   encountering a label. *)
1012record sub_trace_result (ge:genv) (depth:nat)
1013  (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start)
1014  (original_terminates: will_return ge depth start full)
1015  (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝
1016{
1017  ends : trace_ends_with_ret;
1018  trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
1019}.
1020
1021(* We often return the result from a recursive call with an addition to the
1022   structured trace, so we define a couple of functions to help.  The bound on
1023   the size of the termination proof might need to be relaxed, too. *)
1024
1025definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
1026  ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
1027    will_return_end … TM1 = will_return_end … TM2 →
1028    T2 (new_state … r) →
1029    stack_preserved ge e s2 (new_state … r) →
1030    trace_result ge d e s2 t2 TM2 T2 l2 ≝
1031λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1032  mk_trace_result ge d e s2 t2 TM2 T2 l2
1033    (new_state … r)
1034    (remainder … r)
1035    (cost_labelled … r)
1036    trace
1037    SP
1038    ?
1039    (*(match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
1040                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
1041     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*)
1042.
1043cases e in r ⊢ %;
1044[ <TME -TME * cases d in TM1 TM2 ⊢ %;
1045  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
1046  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
1047    %{TMa} % // @(transitive_le … lGE) @L1
1048  ]
1049| <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
1050   * #TMa * #L1 #TME
1051    %{TMa} % // @(transitive_le … lGE) @L1
1052] qed.
1053
1054definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
1055  ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
1056    will_return_end … TM1 = will_return_end … TM2 →
1057    T2 (ends … r) (new_state … r) →
1058    stack_preserved ge (ends … r) s2 (new_state … r) →
1059    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
1060λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
1061  mk_sub_trace_result ge d s2 t2 TM2 T2 l2
1062    (ends … r)
1063    (replace_trace … lGE … r TME trace SP).
1064
1065(* Small syntax hack to avoid ambiguous input problems. *)
1066definition myge : nat → nat → Prop ≝ ge.
1067
1068let rec make_label_return ge depth (s:RTLabs_state ge)
1069  (trace: flat_trace io_out io_in ge s)
1070  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1071  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1072  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1073  (TERMINATES: will_return ge depth s trace)
1074  (TIME: nat)
1075  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
1076  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
1077              (trace_label_return (RTLabs_status ge) s)
1078              (will_return_length … TERMINATES) ≝
1079             
1080match TIME return λTIME. TIME ≥ ? → ? with
1081[ O ⇒ λTERMINATES_IN_TIME. ⊥
1082| S TIME ⇒ λTERMINATES_IN_TIME.
1083
1084  let r ≝ make_label_label ge depth s
1085            trace
1086            ENV_COSTLABELLED
1087            STATE_COSTLABELLED
1088            STATEMENT_COSTLABEL
1089            TERMINATES
1090            TIME ? in
1091  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
1092                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
1093  [ ends_with_ret ⇒ λr.
1094      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
1095  | doesnt_end_with_ret ⇒ λr.
1096      let r' ≝ make_label_return ge depth (new_state … r)
1097                 (remainder … r)
1098                 ENV_COSTLABELLED
1099                 (cost_labelled … r) ?
1100                 (pi1 … (terminates … r)) TIME ? in
1101        replace_trace … r' ?
1102          (tlr_step (RTLabs_status ge) s (new_state … r)
1103            (new_state … r') (new_trace … r) (new_trace … r')) ?
1104  ] (trace_res … r)
1105
1106] TERMINATES_IN_TIME
1107
1108
1109and make_label_label ge depth (s:RTLabs_state ge)
1110  (trace: flat_trace io_out io_in ge s)
1111  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1112  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1113  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1114  (TERMINATES: will_return ge depth s trace)
1115  (TIME: nat)
1116  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
1117  on TIME : sub_trace_result ge depth s trace TERMINATES
1118              (λends. trace_label_label (RTLabs_status ge) ends s)
1119              (will_return_length … TERMINATES) ≝
1120             
1121match TIME return λTIME. TIME ≥ ? → ? with
1122[ O ⇒ λTERMINATES_IN_TIME. ⊥
1123| S TIME ⇒ λTERMINATES_IN_TIME.
1124
1125let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
1126  replace_sub_trace … r ?
1127    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
1128
1129] TERMINATES_IN_TIME
1130
1131
1132and make_any_label ge depth (s0:RTLabs_state ge)
1133  (trace: flat_trace io_out io_in ge s0)
1134  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1135  (STATE_COSTLABELLED: well_cost_labelled_state s0)  (* functions in the state *)
1136  (TERMINATES: will_return ge depth s0 trace)
1137  (TIME: nat)
1138  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
1139  on TIME : sub_trace_result ge depth s0 trace TERMINATES
1140              (λends. trace_any_label (RTLabs_status ge) ends s0)
1141              (will_return_length … TERMINATES) ≝
1142
1143match TIME return λTIME. TIME ≥ ? → ? with
1144[ O ⇒ λTERMINATES_IN_TIME. ⊥
1145| S TIME ⇒ λTERMINATES_IN_TIME.
1146  match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1147                                      well_cost_labelled_state s →
1148                                      ∀TM:will_return ??? trace.
1149                                      myge ? (times 3 (will_return_length ??? trace TM)) →
1150                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
1151  with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace.
1152  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1153                               well_cost_labelled_state s →
1154                               ∀TM:will_return ??? trace.
1155                               myge ? (times 3 (will_return_length ??? trace TM)) →
1156                               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
1157  [ ft_stop st FINAL ⇒
1158      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
1159
1160  | ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
1161    let start' ≝ mk_RTLabs_state ge start stk mtc in
1162    let next' ≝ next_state ? start' ?? EV in
1163    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
1164    [ cl_other ⇒ λCL.
1165        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
1166        (* We're about to run into a label. *)
1167        [ true ⇒ λCS.
1168            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1169              doesnt_end_with_ret
1170              (mk_trace_result ge … next' trace' ?
1171                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
1172        (* An ordinary step, keep going. *)
1173        | false ⇒ λCS.
1174            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
1175                replace_sub_trace ????????????? r ?
1176                  (tal_step_default (RTLabs_status ge) (ends … r)
1177                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
1178        ] (refl ??)
1179       
1180    | cl_jump ⇒ λCL.
1181        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1182          doesnt_end_with_ret
1183          (mk_trace_result ge … next' trace' ?
1184            (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
1185           
1186    | cl_call ⇒ λCL.
1187        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in
1188        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
1189        (* We're about to run into a label, use base case for call *)
1190        [ true ⇒ λCS.
1191            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1192            doesnt_end_with_ret
1193            (mk_trace_result ge …
1194              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
1195                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
1196        (* otherwise use step case *)
1197        | false ⇒ λCS.
1198            let r' ≝ make_any_label ge depth
1199                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
1200                       (pi1 … (terminates … r)) TIME ? in
1201            replace_sub_trace … r' ?
1202              (tal_step_call (RTLabs_status ge) (ends … r')
1203                start' next' (new_state … r) (new_state … r') ? CL ?
1204                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
1205        ] (refl ??)
1206
1207    | cl_return ⇒ λCL.
1208        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
1209          ends_with_ret
1210          (mk_trace_result ge …
1211            next'
1212            trace'
1213            ?
1214            (tal_base_return (RTLabs_status ge) start' next' ? CL)
1215            ?
1216            ?)
1217    ] (refl ? (RTLabs_classify start))
1218   
1219  ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME
1220] TERMINATES_IN_TIME.
1221
1222[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1223| //
1224| //
1225| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
1226| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
1227| @(stack_preserved_join … (stack_ok … r)) //
1228| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
1229| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
1230  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1231  @(transitive_le …  (3*(will_return_length … TERMINATES)))
1232  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1233    @(monotonic_le_times_r 3 … LT)
1234  | @le_S @le_S @le_n
1235  ]
1236| @le_S_S_to_le @TERMINATES_IN_TIME
1237| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
1238| @le_n
1239| //
1240| @(proj1 … (RTLabs_costed …)) //
1241| @le_S_S_to_le @TERMINATES_IN_TIME
1242| @(wrl_nonzero … TERMINATES_IN_TIME)
1243| (* We can't reach the final state because the function terminates with a
1244     return *)
1245  inversion TERMINATES
1246  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
1247  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
1248  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
1249  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
1250  ]
1251| @(will_return_return … CL TERMINATES)
1252| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1253| %{tr} %{EV} @refl
1254| @(well_cost_labelled_state_step  … EV) //
1255| whd @(will_return_notfn … TERMINATES) %2 @CL
1256| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1257| %{tr} %{EV} %
1258| %1 whd @CL
1259| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
1260| @(well_cost_labelled_state_step  … EV) //
1261| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
1262  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
1263    #TMx * #LT' #_ @LT'
1264  | <EQr cases (will_return_call … CL TERMINATES)
1265    #TM' * #_ #EQ' @EQ'
1266  ]
1267| @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
1268| %{tr} %{EV} %
1269| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
1270| @(cost_labelled … r)
1271| skip
1272| cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
1273  @(transitive_lt … LT)
1274  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
1275| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
1276  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
1277| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
1278| %{tr} %{EV} %
1279| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
1280| @(cost_labelled … r)
1281| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
1282  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
1283  cases (will_return_call … TERMINATES) in GT;
1284  #X * #Y #_ #Z
1285  @(transitive_le … (monotonic_lt_times_r 3 … Y))
1286  [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) //
1287  | //
1288  ]
1289| @(well_cost_labelled_state_step  … EV) //
1290| @(well_cost_labelled_call … EV) //
1291| cases (will_return_call … TERMINATES)
1292  #TM * #GT #_ @le_S_S_to_le
1293  >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
1294  @(transitive_le … TERMINATES_IN_TIME)
1295  @(monotonic_le_times_r 3 … GT)
1296| whd @(will_return_notfn … TERMINATES) %1 @CL
1297| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1298| %{tr} %{EV} %
1299| %2 whd @CL
1300| @(well_cost_labelled_state_step  … EV) //
1301| cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT)
1302| cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ
1303| @CL
1304| %{tr} %{EV} %
1305| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
1306| @(well_cost_labelled_state_step  … EV) //
1307| %1 @CL
1308| cases (will_return_notfn … TERMINATES) #TM * #GT #_
1309  @le_S_S_to_le
1310  @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME)
1311  //
1312] qed.
1313
1314(* We can initialise TIME with a suitably large value based on the length of the
1315   termination proof. *)
1316let rec make_label_return' ge depth (s:RTLabs_state ge)
1317  (trace: flat_trace io_out io_in ge s)
1318  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1319  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
1320  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1321  (TERMINATES: will_return ge depth s trace)
1322  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
1323make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
1324  (2 + 3 * will_return_length … TERMINATES) ?.
1325@le_n
1326qed.
1327 
1328(* Tail-calls would not be handled properly (which means that if we try to show the
1329   full version with non-termination we'll fail because calls and returns aren't
1330   balanced.
1331 *)
1332
1333inductive inhabited (T:Type[0]) : Prop ≝
1334| witness : T → inhabited T.
1335
1336
1337(* Define a notion of sound labellings of RTLabs programs. *)
1338
1339definition actual_successor : state → option label ≝
1340λs. match s with
1341[ State f fs m ⇒ Some ? (next f)
1342| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
1343| Returnstate _ _ _ _ ⇒ None ?
1344| Finalstate _ ⇒ None ?
1345].
1346
1347lemma nth_opt_Exists : ∀A,n,l,a.
1348  nth_opt A n l = Some A a →
1349  Exists A (λa'. a' = a) l.
1350#A #n elim n
1351[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
1352| #m #IH *
1353  [ #a #E normalize in E; destruct
1354  | #a #l #a' #E %2 @IH @E
1355  ]
1356] qed.
1357
1358lemma eval_successor : ∀ge,f,fs,m,tr,s'.
1359  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1360  (RTLabs_classify s' = cl_return ∧ successors (lookup_present … (f_graph (func f)) (next f) (next_ok f)) = [ ]) ∨
1361  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
1362#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1363whd in ⊢ (??%? → ?);
1364generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1365[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1366| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1367| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
1368| #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} % // % //
1369| #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} % // % //
1370| #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} % // % //
1371| #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} % // % //
1372| #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} % // % //
1373| #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} % // % //
1374| #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 %] //
1375(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1376  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 ]
1377  whd in ⊢ (??%? → ?);
1378  generalize in ⊢ (??(?%)? → ?);
1379  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1380  [ #e #E normalize in E; destruct
1381  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
1382  ]*)
1383| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 % %
1384] qed.
1385
1386(* Establish a link between the number of instructions until the next cost
1387   label and the number of states. *)
1388
1389
1390definition steps_for_statement : statement → nat ≝
1391λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]).
1392
1393inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝
1394| bostc_here : ∀l,n,H.
1395    is_cost_label (lookup_present … g l H) →
1396    bound_on_steps_to_cost g l n
1397| bostc_later : ∀l,n,H.
1398    ¬ is_cost_label (lookup_present … g l H) →
1399    bound_on_steps_to_cost1 g l n →
1400    bound_on_steps_to_cost g l n
1401with bound_on_steps_to_cost1 : label → nat → Prop ≝
1402| bostc_step : ∀l,n,H.
1403    let stmt ≝ lookup_present … g l H in
1404    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
1405          bound_on_steps_to_cost g l' n) →
1406    bound_on_steps_to_cost1 g l (steps_for_statement stmt + n).
1407
1408let rec bound_on_steps_succ g l n (H:bound_on_steps_to_cost g l n) on H
1409 : bound_on_steps_to_cost g l (S n) ≝
1410match H with
1411[ bostc_here l n Pr Cs ⇒ ?
1412| bostc_later l n H' CS B ⇒ ?
1413] and bound_on_steps1_succ g l n (H:bound_on_steps_to_cost1 g l n) on H
1414: bound_on_steps_to_cost1 g l (S n) ≝
1415match H with
1416[ bostc_step l n Pr Sc ⇒ ?
1417].
1418[ %1 //
1419| %2 /2/
1420| >plus_n_Sm % /3/
1421] qed.
1422
1423let rec bound_on_steps_stmt g l n P (H:bound_on_steps_to_cost1 g l (plus (steps_for_statement (lookup_present … g l P)) n))
1424: bound_on_steps_to_cost1 g l (S (S n)) ≝ ?.
1425cases (lookup_present ? statement ???) in H; /2/
1426qed.
1427
1428let rec bound_on_instrs_to_steps g l n
1429  (B:bound_on_instrs_to_cost g l n)
1430on B : bound_on_steps_to_cost1 g l (times n 2) ≝ ?
1431and bound_on_instrs_to_steps' g l n
1432  (B:bound_on_instrs_to_cost' g l n)
1433on B : bound_on_steps_to_cost g l (times n 2) ≝ ?.
1434[ cases B #l' #n' #H #EX @bound_on_steps_stmt [ @H | % #l'' #SC @bound_on_instrs_to_steps' @EX @SC ]
1435| cases B
1436  [ #l' #n' #H #CS %1 //
1437  | #l' #n' #H #CS #B' %2 [ @H | @CS | @bound_on_instrs_to_steps @B' ]
1438  ]
1439] qed.
1440
1441
1442definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝
1443λf. bound_on_steps_to_cost (f_graph (func f)) (next f).
1444definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝
1445λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f).
1446
1447inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
1448| 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
1449| 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)
1450| 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)
1451.
1452
1453lemma state_bound_on_steps_to_cost_zero : ∀s.
1454  ¬ state_bound_on_steps_to_cost s O.
1455#s % #H inversion H
1456[ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct
1457  whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*)
1458  #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct
1459| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
1460| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1461] qed.
1462
1463lemma eval_steps : ∀ge,f,fs,m,tr,s'.
1464  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
1465  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
1466  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
1467#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
1468whd in ⊢ (??%? → ?);
1469generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok)
1470[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1471| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
1472| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
1473| #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
1474| #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
1475| #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
1476| #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
1477| #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
1478| #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
1479| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
1480(*| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
1481  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 ]
1482  whd in ⊢ (??%? → ?);
1483  generalize in ⊢ (??(?%)? → ?);
1484  cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ? | _ ⇒ ? ] ?)? → ?);
1485  [ #e #E normalize in E; destruct
1486  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
1487  ]*)
1488| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
1489] qed.
1490
1491lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n.
1492  state_bound_on_steps_to_cost s (S n) →
1493  ∀CL:RTLabs_classify s = cl_call.
1494  as_after_return (RTLabs_status ge) «s, CL» s' →
1495  RTLabs_cost s' = false →
1496  state_bound_on_steps_to_cost s' n.
1497#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL -CL inversion H
1498[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
1499  #fn * #args * #dst * #stk * #m' #E destruct
1500| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
1501  whd in S; #CL cases s'
1502  [ #f' #fs' #m' * * #N #F #STK #CS
1503    %1 whd
1504    inversion S
1505    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
1506      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
1507    | #l #n #H #CS' #B #E1 #E2 #_ destruct <N <F @B
1508    ]
1509  | #fd' #args' #dst' #fs' #m' *
1510  | #rv #dst' #fs' #m' *
1511  | #r #E normalize in E; destruct
1512  ]
1513| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
1514] qed.
1515
1516lemma bound_after_step : ∀ge,s,tr,s',n.
1517  state_bound_on_steps_to_cost s (S n) →
1518  eval_statement ge s = Value ??? 〈tr, s'〉 →
1519  RTLabs_cost s' = false →
1520  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
1521   state_bound_on_steps_to_cost s' n.
1522#ge #s #tr #s' #n #BOUND1 inversion BOUND1
1523[ #f #fs #m #m #FS #E1 #E2 #_ destruct
1524  #EVAL cases (eval_successor … EVAL)
1525  [ * /3/
1526  | * #l * #S1 #S2 #NC %2
1527  (*
1528    cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ]
1529    *)
1530    @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct
1531    inversion (eval_preserves … EVAL)
1532    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct
1533      >(eval_steps … EVAL) in E2; #En normalize in En;
1534      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1535      %1 inversion (IH … S2)
1536      [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1537        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
1538        whd in S1:(??%?); destruct >NC in CSx; *
1539      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 destruct @H75
1540      ]
1541    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
1542      >(eval_steps … EVAL) in E2; #En normalize in En;
1543      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
1544      %2 @IH normalize in S1; destruct @S2
1545    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28
1546      destruct
1547    | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
1548      normalize in S1; destruct
1549    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
1550    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
1551    ]
1552  ]
1553| #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
1554  /3/
1555| #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct
1556  #EVAL #NC %2 inversion (eval_preserves … EVAL)
1557  [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1558  | #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct
1559  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
1560  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
1561  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #N #F #E1 #E2 #E3 #_ destruct
1562    %1 whd in FS ⊢ %;
1563    <N
1564    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
1565    inversion FS
1566    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
1567        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs' m')) in CSx:(?%);
1568        >NC in CSx; *
1569    | #lx #nx #P #CS #H #E1x #E2x #_ destruct @H
1570    ]
1571  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
1572  ]
1573] qed.
1574
1575
1576
1577
1578definition soundly_labelled_ge : genv → Prop ≝
1579λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → soundly_labelled_fn f.
1580
1581definition soundly_labelled_state : state → Prop ≝
1582λs. match s with
1583[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
1584| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
1585                          All ? (λf. soundly_labelled_fn (func f)) fs
1586| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
1587| Finalstate _ ⇒ True
1588].
1589
1590lemma steps_from_sound : ∀s.
1591  RTLabs_cost s = true →
1592  soundly_labelled_state s →
1593  ∃n. state_bound_on_steps_to_cost s n.
1594* [ #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 ]
1595whd in ⊢ (% → ?); * #SLF #_
1596cases (SLF (next f) (next_ok f)) #n #B1
1597% [2: % /2/ | skip ]
1598qed.
1599
1600lemma soundly_labelled_state_step : ∀ge,s,tr,s'.
1601  soundly_labelled_ge ge →
1602  eval_statement ge s = Value ??? 〈tr,s'〉 →
1603  soundly_labelled_state s →
1604  soundly_labelled_state s'.
1605#ge #s #tr #s' #ENV #EV #S
1606inversion (eval_preserves … EV)
1607[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
1608  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1609| #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
1610  whd in S ⊢ %; %
1611  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
1612  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
1613  ]
1614| #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
1615  whd in S ⊢ %; @S
1616| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
1617  whd in S ⊢ %; cases S //
1618| #ge' #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
1619  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
1620| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
1621] qed.
1622
1623lemma soundly_labelled_state_preserved : ∀ge,s,s'.
1624  stack_preserved ge ends_with_ret s s' →
1625  soundly_labelled_state s →
1626  soundly_labelled_state s'.
1627#ge #s0 #s0' #SP inversion SP
1628[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
1629| #s1 #f #f' #fs #m #fn #S #M #N #F #S1 #E1 #E2 #E3 #E4 destruct
1630  inversion S1
1631  [ #f1 #fs1 #m1 #fn1 #S1 #M1 #E1 #E2 #E3 #E4 destruct
1632    * #_ #S whd in S;
1633    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1634    destruct @S
1635  | #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
1636    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1637    destruct @S
1638  | #rtv #dst #fs1 #m1 #S1 #M1 #E1 #E2 #E3 #E4 destruct #S
1639    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
1640    destruct @S
1641  ]
1642| //
1643| //
1644] qed.
1645
1646(* When constructing an infinite trace, we need to be able to grab the finite
1647   portion of the trace for the next [trace_label_diverges] constructor.  We
1648   use the fact that the trace is soundly labelled to achieve this. *)
1649
1650record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
1651  ro_well_cost_labelled: well_cost_labelled_state s;
1652  ro_soundly_labelled: soundly_labelled_state s;
1653  ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
1654  ro_not_final: RTLabs_is_final s = None ?
1655}.
1656
1657inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝
1658| fp_tal : ∀s,s':RTLabs_state ge.
1659           trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
1660           ∀t:flat_trace io_out io_in ge s'.
1661           remainder_ok ge s' t →
1662           finite_prefix ge s
1663| fp_tac : ∀s1,s2,s3:RTLabs_state ge.
1664           trace_any_call (RTLabs_status ge) s1 s2 →
1665           well_cost_labelled_state s2 →
1666           as_execute (RTLabs_status ge) s2 s3 →
1667           ∀t:flat_trace io_out io_in ge s3.
1668           remainder_ok ge s3 t →
1669           finite_prefix ge s1
1670.
1671
1672definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge.
1673  RTLabs_classify s = cl_other →
1674  finite_prefix ge s' →
1675  as_execute (RTLabs_status ge) s s' →
1676  RTLabs_cost s' = false →
1677  finite_prefix ge s ≝
1678λge,s,s',OTHER,fp.
1679match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
1680[ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
1681    (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
1682    rem rok
1683| fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
1684    (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
1685    WCL2 EV rem rok
1686].
1687
1688definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge.
1689  as_execute (RTLabs_status ge) s s1 →
1690  ∀CALL:RTLabs_classify s = cl_call.
1691  finite_prefix ge s'' →
1692  trace_label_return (RTLabs_status ge) s1 s'' →
1693  as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' →
1694  RTLabs_cost s'' = false →
1695  finite_prefix ge s ≝
1696λge,s,s1,s'',EVAL,CALL,fp.
1697match 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
1698[ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
1699    (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
1700    rem rok
1701| fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
1702    (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)
1703    WCL2 EV rem rok
1704].
1705
1706lemma not_return_to_not_final : ∀ge,s,tr,s'.
1707  eval_statement ge s = Value ??? 〈tr, s'〉 →
1708  RTLabs_classify s ≠ cl_return →
1709  RTLabs_is_final s' = None ?.
1710#ge #s #tr #s' #EV
1711inversion (eval_preserves … EV) //
1712#H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
1713@⊥ @(absurd ?? CL) @refl
1714qed.
1715
1716definition termination_oracle ≝ ∀ge,depth,s,trace.
1717  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
1718
1719let rec finite_segment ge (s:RTLabs_state ge) n trace
1720  (ORACLE: termination_oracle)
1721  (TRACE_OK: remainder_ok ge s trace)
1722  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1723  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1724  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
1725  on n : finite_prefix ge s ≝
1726match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
1727[ O ⇒ λLABEL_LIMIT. ⊥
1728| S n' ⇒
1729  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'.
1730    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
1731    [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
1732    | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
1733        let start' ≝ mk_RTLabs_state ge start stk mtc in
1734        let next' ≝ next_state ge start' next tr EV in
1735        match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
1736        [ cl_other ⇒ λCL.
1737            let TRACE_OK' ≝ ? in
1738            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
1739            [ true ⇒ λCS.
1740                fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
1741            | false ⇒ λCS.
1742                let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1743                fp_add_default ge start' next' CL fs ? CS
1744            ] (refl ??)
1745        | cl_jump ⇒ λCL.
1746            fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
1747        | cl_call ⇒ λCL.
1748            match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
1749            [ or_introl TERMINATES ⇒
1750              match TERMINATES with [ witness TERMINATES ⇒
1751                let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1752                let TRACE_OK' ≝ ? in
1753                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
1754                [ 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'
1755                | false ⇒ λCS.
1756                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1757                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
1758                ] (refl ??)
1759              ]
1760            | or_intror NO_TERMINATION ⇒
1761                fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?
1762            ]
1763        | cl_return ⇒ λCL. ⊥
1764        ] (refl ??)
1765    ] mtc0
1766  ] trace TRACE_OK
1767] LABEL_LIMIT.
1768[ cases (state_bound_on_steps_to_cost_zero s) /2/
1769| @(absurd …  (ro_not_final … TRACE_OK) FINAL)
1770| @(absurd ?? (ro_no_termination … TRACE_OK))
1771     %{0} % @wr_base //
1772| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
1773| 5,6,9,10,11: /3/
1774| cases TRACE_OK #H1 #H2 #H3 #H4
1775  % [ @(well_cost_labelled_state_step … EV) //
1776    | @(soundly_labelled_state_step … EV) //
1777    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
1778    | @(not_return_to_not_final … EV) >CL % #E destruct
1779    ]
1780| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1781| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1782| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
1783  @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
1784| % [ /2/
1785    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
1786      @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
1787    | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
1788      @wr_call //
1789      @(will_return_prepend … TERMINATES … TM1)
1790      cases (terminates … tlr) //
1791    | (* By stack preservation we cannot be in the final state *)
1792      inversion (stack_ok … tlr)
1793      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
1794      | #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
1795      | #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s0
1796        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
1797        inversion (eval_preserves … EV)
1798        [ 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 ]
1799        #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
1800        inversion S
1801        [ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 [ whd in H5:(??%?%); | whd in H2:(??%?%); ] destruct ]
1802        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
1803           so we can use it as a witness that at least one frame exists *)
1804        inversion LABEL_LIMIT
1805        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
1806      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
1807      ]
1808    ]
1809| @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
1810| @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
1811| /2/
1812| %{tr} %{EV} %
1813| cases TRACE_OK #H1 #H2 #H3 #H4
1814  % [ @(well_cost_labelled_state_step … EV) /2/
1815    | @(soundly_labelled_state_step … EV) /2/
1816    | @(not_to_not … NO_TERMINATION) * #depth * #TM %
1817      @(will_return_lower … TM) //
1818    | @(not_return_to_not_final … EV) >CL % #E destruct
1819    ]
1820| %2 @CL
1821| 21,22: %{tr} %{EV} %
1822| cases (bound_after_step … LABEL_LIMIT EV ?)
1823  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
1824    inversion trace'
1825    [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
1826      @(absurd ?? FINAL) @(not_return_to_not_final … EV)
1827      % >CL #E destruct
1828    | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
1829      @wr_base //
1830    ]
1831    ]
1832    | >CL #E destruct
1833    ]
1834  | //
1835  | //
1836  ]
1837| cases TRACE_OK #H1 #H2 #H3 #H4
1838  % [ @(well_cost_labelled_state_step … EV) //
1839    | @(soundly_labelled_state_step … EV) //
1840    | @(not_to_not … (ro_no_termination … TRACE_OK))
1841      * #depth * #TERM %{depth} % @wr_step /2/
1842    | @(not_return_to_not_final … EV) >CL % #E destruct
1843    ]
1844] qed.
1845
1846(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
1847       a trace_label_diverges value, but I only know how to construct those
1848       using a cofixpoint in Type[0], which means I can't use the termination
1849       oracle.
1850*)
1851
1852let corec make_label_diverges ge (s:RTLabs_state ge)
1853  (trace: flat_trace io_out io_in ge s)
1854  (ORACLE: termination_oracle)
1855  (TRACE_OK: remainder_ok ge s trace)
1856  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1857  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1858  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
1859  : trace_label_diverges_exists (RTLabs_status ge) s ≝
1860match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
1861[ ex_intro n B ⇒
1862    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
1863      return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
1864    with
1865    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
1866        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1867            tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T'
1868(*
1869        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1870        [ ex_intro T' _ ⇒
1871            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
1872        ]*)
1873    | fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
1874        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
1875            tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T'
1876(*
1877        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
1878        [ ex_intro T' _ ⇒
1879            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
1880        ]*)
1881    ] STATEMENT_COSTLABEL
1882].
1883[ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T)
1884| @EV
1885| @(trace_any_call_call … T)
1886| cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T)
1887] qed.
1888
1889lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_state ge.
1890  as_execute (RTLabs_status ge) s1 s2 →
1891  make_initial_state p = OK ? s1 →
1892  stack_preserved ge ends_with_ret s2 s' →
1893  RTLabs_is_final s' ≠ None ?.
1894#ge #p * #s1 #S1 #M1 * #s2 #S2 #M2 * #s' #S' #M' #EV whd in ⊢ (??%? → ?);
1895@bind_ok #m #_
1896@bind_ok #b #_
1897@bind_ok #f #_
1898#E destruct
1899#SP inversion (eval_preserves_ext … EV)
1900[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
1901     inversion SP
1902     [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
1903     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥
1904          inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 destruct
1905     ]
1906| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 destruct
1907] qed.
1908
1909lemma initial_state_is_call : ∀p,s.
1910  make_initial_state p = OK ? s →
1911  RTLabs_classify s = cl_call.
1912#p #s whd in ⊢ (??%? → ?);
1913@bind_ok #m #_
1914@bind_ok #b #_
1915@bind_ok #f #_
1916#E destruct
1917@refl
1918qed.
1919
1920let rec whole_structured_trace_exists ge p (s:RTLabs_state ge)
1921  (ORACLE: termination_oracle)
1922  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
1923  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
1924  : ∀trace: flat_trace io_out io_in ge s.
1925    ∀INITIAL: make_initial_state p = OK state s.
1926    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
1927    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
1928    trace_whole_program_exists (RTLabs_status ge) s ≝
1929match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s.
1930                   make_initial_state p = OK ? s →
1931                   well_cost_labelled_state s →
1932                   soundly_labelled_state s →
1933                   trace_whole_program_exists (RTLabs_status ge) s with
1934[ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace.
1935match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
1936                             make_initial_state p = OK state s →
1937                             well_cost_labelled_state s →
1938                             soundly_labelled_state s →
1939                             trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with
1940[ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
1941    let IS_CALL ≝ initial_state_is_call … INITIAL in
1942    let s' ≝ mk_RTLabs_state ge s stk mtc in
1943    let next' ≝ next_state ge s' next tr EV in
1944    match ORACLE ge O next trace' with
1945    [ or_introl TERMINATES ⇒
1946        match TERMINATES with
1947        [ witness TERMINATES ⇒
1948          let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
1949          twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ?
1950        ]
1951    | or_intror NO_TERMINATION ⇒
1952        twp_diverges (RTLabs_status ge) s' next' IS_CALL ?
1953         (make_label_diverges ge next' trace' ORACLE ?
1954            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
1955    ]
1956| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
1957] mtc0 ].
1958[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
1959  cases FINAL #E @E @refl
1960| %{tr} %{EV} %
1961| @(after_the_initial_call_is_the_final_state … p s' next')
1962  [ %{tr} %{EV} % | @INITIAL | @(stack_ok … tlr) ]
1963| @(well_cost_labelled_state_step … EV) //
1964| @(well_cost_labelled_call … EV) //
1965| %{tr} %{EV} %
1966| @(well_cost_labelled_call … EV) //
1967| % [ @(well_cost_labelled_state_step … EV) //
1968    | @(soundly_labelled_state_step … EV) //
1969    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
1970    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
1971    ]
1972] qed.
1973
1974lemma init_state_is : ∀p,s.
1975  make_initial_state p = OK ? s →
1976  𝚺b. match s with [ Callstate fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
1977   | _ ⇒ False ].
1978#p #s
1979@bind_ok #m #Em
1980@bind_ok #b #Eb
1981@bind_ok #f #Ef
1982#E whd in E:(??%%); destruct
1983%{b} whd
1984% // @Ef
1985qed.
1986
1987definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_state (make_global p) ≝
1988λp,s,I. mk_RTLabs_state (make_global p) s [init_state_is p s I] ?.
1989cases (init_state_is p s I) #b
1990cases s
1991[ #f #fs #m *
1992| #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
1993| #rv #rr #fs #m *
1994| #r *
1995] qed.
1996
1997lemma well_cost_labelled_initial : ∀p,s.
1998  make_initial_state p = OK ? s →
1999  well_cost_labelled_program p →
2000  well_cost_labelled_state s ∧ soundly_labelled_state s.
2001#p #s
2002@bind_ok #m #Em
2003@bind_ok #b #Eb
2004@bind_ok #f #Ef
2005#E destruct
2006whd in ⊢ (% → %);
2007#WCL
2008@(find_funct_ptr_All ??????? Ef)
2009@(All_mp … WCL)
2010* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
2011qed.
2012
2013lemma well_cost_labelled_make_global : ∀p.
2014  well_cost_labelled_program p →
2015  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
2016#p whd in ⊢ (% → ?%%);
2017#WCL %
2018#b #f #FFP
2019[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
2020| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
2021] @(All_mp … WCL)
2022* #id * #fn // * /2/
2023qed.
2024
2025theorem program_trace_exists :
2026  termination_oracle →
2027  ∀p:RTLabs_program.
2028  well_cost_labelled_program p →
2029  ∀s:state.
2030  ∀I: make_initial_state p = OK ? s.
2031 
2032  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
2033 
2034  ∀NOIO:exec_no_io … plain_trace.
2035  ∀NW:not_wrong … plain_trace.
2036 
2037  let flat_trace ≝ make_whole_flat_trace p s NOIO NW I in
2038 
2039  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
2040
2041#ORACLE #p #WCL #s #I
2042letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
2043#NOIO #NW
2044letin flat_trace ≝ (make_whole_flat_trace p s NOIO NW I)
2045whd
2046@(whole_structured_trace_exists (make_global p) p ? ORACLE)
2047[ @(proj1 … (well_cost_labelled_make_global … WCL))
2048| @(proj2 … (well_cost_labelled_make_global … WCL))
2049| @flat_trace
2050| @I
2051| @(proj1 ?? (well_cost_labelled_initial … I WCL))
2052| @(proj2 ?? (well_cost_labelled_initial … I WCL))
2053] qed.
2054
2055
2056lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge.
2057  as_execute (RTLabs_status ge) s s' →
2058  ∃tr. eval_statement ge s = Value … 〈tr,s'〉.
2059#ge #s #s' * #tr * #EX #_ %{tr} @EX
2060qed.
2061
2062(* as_execute might be in Prop, but because the semantics is deterministic
2063   we can retrieve the event trace anyway. *)
2064
2065let rec deprop_execute ge (s,s':state)
2066  (X:∃t. eval_statement ge s = Value … 〈t,s'〉)
2067: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
2068match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with
2069[ Value ts ⇒ λY. «fst … ts, ?»
2070| _ ⇒ λY. ⊥
2071] X.
2072[ 1,3: cases Y #x #E destruct
2073| cases Y #trP #E destruct @refl
2074] qed.
2075
2076let rec deprop_as_execute ge (s,s':RTLabs_state ge)
2077  (X:as_execute (RTLabs_status ge) s s')
2078: Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝
2079deprop_execute ge s s' ?.
2080cases X #tr * #EX #_ %{tr} @EX
2081qed.
2082
2083(* A non-empty finite section of a flat_trace *)
2084inductive partial_flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → state → Type[0] ≝
2085| pft_base : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → partial_flat_trace o i ge s s'
2086| 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''.
2087
2088let rec append_partial_flat_trace o i ge s1 s2 s3
2089  (tr1:partial_flat_trace o i ge s1 s2)
2090on tr1 : partial_flat_trace o i ge s2 s3 → partial_flat_trace o i ge s1 s3 ≝
2091match tr1 with
2092[ pft_base s tr s' EX ⇒ pft_step … s tr s' s3 EX
2093| pft_step s tr s' s'' EX tr' ⇒ λtr2. pft_step … s tr s' s3 EX (append_partial_flat_trace … tr' tr2)
2094].
2095
2096let rec partial_to_flat_trace o i ge s1 s2
2097  (tr:partial_flat_trace o i ge s1 s2)
2098on tr : flat_trace o i ge s2 → flat_trace o i ge s1 ≝
2099match tr with
2100[ pft_base s tr s' EX ⇒ ft_step … EX
2101| pft_step s tr s' s'' EX tr' ⇒ λtr''. ft_step … EX (partial_to_flat_trace … tr' tr'')
2102].
2103
2104(* Extract a flat trace from a structured one. *)
2105let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge)
2106  (tr:trace_label_return (RTLabs_status ge) s s')
2107on tr :
2108  partial_flat_trace io_out io_in ge s s' ≝
2109match tr with
2110[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
2111| tlr_step s1 s2 s3 tll tlr ⇒
2112  append_partial_flat_trace …
2113    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
2114    (flat_trace_of_label_return ge s2 s3 tlr)
2115]
2116and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge)
2117  (tr:trace_label_label (RTLabs_status ge) ends s s')
2118on tr :
2119  partial_flat_trace io_out io_in ge s s' ≝
2120match tr with
2121[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
2122]
2123and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge)
2124  (tr:trace_any_label (RTLabs_status ge) ends s s')
2125on tr :
2126  partial_flat_trace io_out io_in ge s s' ≝
2127match tr with
2128[ tal_base_not_return s1 s2 EX CL CS ⇒
2129    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2130    pft_base … EX' ]
2131| tal_base_return s1 s2 EX CL ⇒
2132    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2133    pft_base … EX' ]
2134| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
2135    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
2136    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2137    pft_step … EX' suffix' ]
2138| tal_step_call ends s1 s2 s3 s4 EX CL AR tlr CS tal ⇒
2139    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2140    pft_step … EX'
2141      (append_partial_flat_trace …
2142        (flat_trace_of_label_return ge ?? tlr)
2143        (flat_trace_of_any_label ge ??? tal))
2144    ]
2145| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
2146    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2147      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
2148    ]
2149].
2150
2151
2152(* We take an extra step so that we can always return a non-empty trace to
2153   satisfy the guardedness condition in the cofixpoint. *)
2154let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et
2155  (tr:trace_any_call (RTLabs_status ge) s s')
2156  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2157on tr :
2158  partial_flat_trace io_out io_in ge s s'' ≝
2159match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with
2160[ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX''
2161| tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''.
2162    match deprop_as_execute ge ?? EX with [ mk_Sig et EX' ⇒
2163    pft_step … EX'
2164      (append_partial_flat_trace …
2165        (flat_trace_of_label_return ge ?? tlr)
2166        (flat_trace_of_any_call ge … tac EX''))
2167    ]
2168| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
2169    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2170    pft_step … EX'
2171     (flat_trace_of_any_call ge … tal EX'')
2172    ]
2173] EX''.
2174
2175let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et
2176  (tr:trace_label_call (RTLabs_status ge) s s')
2177  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
2178on tr :
2179  partial_flat_trace io_out io_in ge s s'' ≝
2180match tr with
2181[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
2182] EX''.
2183
2184(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
2185   to take care to satisfy the guardedness condition by witnessing the fact that
2186   the partial traces are non-empty. *)
2187let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge)
2188  (tr:trace_label_diverges (RTLabs_status ge) s)
2189: flat_trace io_out io_in ge s ≝
2190match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
2191[ tld_step sx sy tll tld ⇒
2192  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 ⇒
2193    λtll.
2194    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
2195    [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2196    | 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)
2197    ] mtc0 ] tll tld
2198| tld_base s1 s2 s3 tlc EX CL tld ⇒
2199  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 ⇒
2200    λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2201      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
2202      [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
2203      | 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)
2204      ] mtc0
2205    ]
2206  ] EX tld
2207]
2208(* Helper to keep adding the partial trace without violating the guardedness
2209   condition. *)
2210and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge)
2211: partial_flat_trace io_out io_in ge s s' →
2212  trace_label_diverges (RTLabs_status ge) s' →
2213  flat_trace io_out io_in ge s ≝
2214match 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 ⇒
2215λ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
2216[ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
2217| 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)
2218] mtc ]
2219.
2220
2221
2222coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
2223| eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
2224| 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).
2225
2226let corec flat_traces_are_determined_by_starting_point ge s tr1
2227: ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
2228match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
2229[ ft_stop s F ⇒ λtr2. ?
2230| ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
2231    match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
2232    [ ft_stop s F ⇒ λEX. ?
2233    | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
2234    ] EX0
2235].
2236[ inversion tr2 in tr1 F;
2237  [ #s #F #_ #_ #tr1 #F' @eft_stop
2238  | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
2239    cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
2240  ]
2241| @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
2242| -EX0
2243  cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2244  @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
2245  -E -EX' -tr2' #tr2' #EX'
2246  cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
2247  @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
2248  -E -EX' #EX'
2249    @eft_step @flat_traces_are_determined_by_starting_point
2250] qed.
2251
2252let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
2253  (str:trace_label_diverges (RTLabs_status ge) s)
2254  (tr:flat_trace io_out io_in ge s)
2255: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
2256@flat_traces_are_determined_by_starting_point
2257qed.
2258
2259let rec flat_trace_of_whole_program ge (s:RTLabs_state ge)
2260  (tr:trace_whole_program (RTLabs_status ge) s)
2261on tr : flat_trace io_out io_in ge s ≝
2262match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with
2263[ twp_terminating s1 s2 sf CL EX tlr F ⇒
2264    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2265      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
2266    ]
2267| twp_diverges s1 s2 CL EX tld ⇒
2268    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
2269      ft_step … EX' (flat_trace_of_label_diverges … tld)
2270    ]
2271].
2272
2273let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge)
2274  (str:trace_whole_program (RTLabs_status ge) s)
2275  (tr:flat_trace io_out io_in ge s)
2276: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
2277@flat_traces_are_determined_by_starting_point
2278qed.
2279
2280
2281
2282
2283
2284(* We still need to link tal_unrepeating to our definition of cost soundness. *)
2285
2286
2287(* Extract the "current" function from a state. *)
2288definition state_fn : ∀ge. RTLabs_status ge → option block ≝
2289λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
2290  match Ras_state … s with
2291  [ Callstate _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
2292  | _ ⇒  Some ? h ] ].
2293
2294(* Some results to invert the classification of states *)
2295
2296lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge.
2297  as_execute (RTLabs_status ge) s s' →
2298  RTLabs_classify s = cl →
2299  match cl with
2300  [ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
2301  | cl_return ⇒ ∀fn. P (rapc_ret fn)
2302  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
2303  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
2304  ] → P (as_pc_of (RTLabs_status ge) s).
2305#ge #cl #P * *
2306[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
2307  cases (lookup_present ???? (next_ok f)) normalize
2308  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
2309| #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
2310| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
2311| #r #S #M #s' * #tr * #EX normalize in EX; destruct
2312] qed.
2313
2314lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_state ge.
2315  as_execute (RTLabs_status ge) s s' →
2316  RTLabs_classify s = cl →
2317  match cl with
2318  [ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
2319  | cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
2320  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2321  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
2322  ] .
2323#ge * #s #s' #EX #CL whd
2324@(declassify_pc … EX CL) whd
2325[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | #fn #l %{fn} %{l} % ]
2326qed.
2327
2328lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_state ge.
2329  as_execute (RTLabs_status ge) s s' →
2330  RTLabs_classify s = cl →
2331  match cl with
2332  [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_state ge (Callstate fd args dst fs m) S M
2333  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_state ge (Returnstate ret dst fs m) S M
2334  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_state ge (State f fs m) S M
2335  ] .
2336#ge #cl * * [ #f #fs #m | #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
2337#S #M * #s' #S' #M' #EX #CL
2338whd in CL:(??%?);
2339[ cut (cl = cl_other ∨ cl = cl_jump)
2340  [ cases (lookup_present … (next_ok … f)) in CL;
2341    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
2342  * #E >E %{f} %{fs} %{m} %{S} %{M} %
2343| <CL %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
2344| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
2345| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
2346] qed.
2347
2348lemma State_not_callreturn : ∀f,fs,m,cl.
2349  RTLabs_classify (State f fs m) = cl →
2350  match cl with
2351  [ cl_return ⇒ False
2352  | cl_call ⇒ False
2353  | _ ⇒ True
2354  ].
2355#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
2356cases (lookup_present … (next_ok f)) //
2357qed.
2358
2359(* And some about traces *)
2360
2361lemma tal_not_final : ∀ge,fl,s1,s2.
2362  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2363  RTLabs_is_final (Ras_state … s1) = None ?.
2364#ge #flx #s1x #s2x *
2365[ #s1 #s2 * #tr * #EX #NX #CL #CS
2366| #s1 #s2 * #tr * #EX #NX #CL
2367| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
2368| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
2369| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
2370] @(step_not_final … EX)
2371qed.
2372
2373(* invert traces ending in a return *)
2374
2375lemma tal_return : ∀ge,fl,s1,s2.
2376  as_classifier (RTLabs_status ge) s1 cl_return →
2377  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
2378  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
2379#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
2380[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
2381  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
2382| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
2383  %{EX} %{CL} % %
2384| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
2385  whd in CL CL'; >CL in CL'; #E destruct
2386| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
2387  whd in CL CL'; >CL in CL'; #E destruct
2388| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
2389  whd in CL CL'; >CL in CL'; #E destruct
2390] qed.
2391
2392(* TODO: move *)
2393lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
2394  Exists S (λy. y = x) l →
2395  x ∈ l.
2396#S #x #l elim l
2397[ //
2398| #h #t #IH
2399  normalize lapply (eqb_true … x h)
2400  cases (x==h) *
2401  [ #E #_ >(E (refl ??)) //
2402  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
2403            | #H @IH @H
2404            ]
2405  ]
2406] qed.
2407
2408(* We aim to extract a loop without a cost label to contradict the reappearance
2409   of a pc within a trace_any_label.  This data structure represents the tail
2410   of a loop purely in terms of the RTLabs function body graph. *)
2411
2412inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝
2413| gl_end : bad_label_list g head head
2414| gl_step : ∀l1,l2,H.
2415    l2 ∈ successors (lookup_present … g l1 H) →
2416    ¬ is_cost_label (lookup_present … g l1 H) →
2417    bad_label_list g head l2 →
2418    bad_label_list g head l1.
2419
2420(* We need to link the pcs, states of the semantics with the labels and graphs
2421   of the syntax. *)
2422
2423inductive pc_label : RTLabs_pc → label → Prop ≝
2424| pl_state : ∀fn,l. pc_label (rapc_state fn l) l
2425| pl_call : ∀l,fn. pc_label (rapc_call (Some ? l) fn) l.
2426
2427discriminator option.
2428
2429lemma pc_label_eq : ∀pc,l1,l2.
2430  pc_label pc l1 →
2431  pc_label pc l2 →
2432  l1 = l2.
2433#pcx #l1x #l2 * #A #B #H inversion H #C #D #E1 #E2 #E3 destruct %
2434qed.
2435
2436lemma pc_label_call_eq : ∀l,fn,l'.
2437  pc_label (rapc_call (Some ? l) fn) l' →
2438  l = l'.
2439#l #fn #l' #PC inversion PC
2440#a #b #E1 #E2 #E3 destruct
2441%
2442qed.
2443
2444inductive graph_fn (ge:genv) : option block → graph statement → Prop ≝
2445| gf : ∀b,fn.
2446    find_funct_ptr … ge b = Some ? (Internal ? fn) →
2447    graph_fn ge (Some ? b) (f_graph … fn).
2448
2449lemma graph_fn_state : ∀ge,f,fs,m,S,M,g.
2450  graph_fn ge (state_fn ge (mk_RTLabs_state ge (State f fs m) S M)) g →
2451  g = f_graph (func f).
2452#ge #f #fs #m * [*] #fn #S * #FFP #M #g #G
2453inversion G
2454#b #fn' #FFP' normalize #E1 #E2 #E3 destruct >FFP in FFP'; #E destruct
2455%
2456qed.
2457
2458lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l.
2459  let s ≝ mk_RTLabs_state ge (State f fs m) S M in
2460  ∀EV:eval_statement ge s = Value … 〈tr,s'〉.
2461  actual_successor s' = Some ? l →
2462  state_fn ge s = state_fn ge (next_state ge s s' tr EV).
2463#ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS
2464change with (Ras_state ? (next_state ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);
2465inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_state ge (State f fs m) ? M) … EV))
2466[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2467| #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
2468| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
2469| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
2470  >H33 in AS; normalize #AS destruct
2471| #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2472| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 destruct
2473] qed.
2474
2475lemma pc_after_return' : ∀ge,pre,post,CL,ret,callee.
2476  as_after_return (RTLabs_status ge) «pre,CL» post →
2477  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
2478  match ret with
2479  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
2480  | Some retl ⇒
2481    state_fn … pre = state_fn … post ∧
2482    pc_label (as_pc_of (RTLabs_status ge) post) retl
2483  ].
2484#ge #pre #post #CL #ret #callee #AF
2485cases pre in CL AF ⊢ %;
2486* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
2487    cases (lookup_present ???? (next_ok f)) in CL;
2488    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
2489  | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
2490  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
2491  | #r #S #M #CL normalize in CL; destruct
2492  ]
2493cases post
2494* [ #postf #postfs #postm * [*] #fn' #S' #M'
2495  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
2496  | 2,6: #A #B #C #D #E #F #G *
2497  | 3,7: #A #B #C #D #E #F *
2498  | #r #S' #M' #AF whd in AF; destruct
2499  | #r #S' #M'
2500  ]
2501#AF #PC normalize in PC; destruct whd
2502[ cases AF * #A #B #C destruct % [ % | normalize >A // ]
2503| % #E normalize in E; destruct
2504] qed.
2505
2506lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_state ge. ∀l.
2507  actual_successor s = Some ? l →
2508  pc_label (as_pc_of (RTLabs_status ge) s) l.
2509#ge * *
2510[ #f #fs #m * [*] #fn #S #M #l #AS
2511| #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
2512| #ret #dst #fs #m #S #M #l #AS
2513| #r #S #M #l #AS
2514] whd in AS:(??%?); destruct //
2515qed.
2516
2517include alias "utilities/deqsets.ma".
2518
2519(* Build the tail of the "bad" loop using the reappearance of the original pc,
2520   ignoring the rest of the trace_any_label once we see that pc. *)
2521
2522let rec tal_pc_loop_tail ge flX s1X s2X
2523  (pc:as_pc (RTLabs_status ge)) g l
2524  (PC0:pc_label pc l)
2525  (tal: trace_any_label (RTLabs_status ge) flX s1X s2X)
2526on tal :
2527  ∀l1.
2528  pc_label (as_pc_of (RTLabs_status ge) s1X) l1 →
2529  graph_fn ge (state_fn … s1X) g →
2530  Not (as_costed (RTLabs_status ge) s1X) →
2531  pc ∈ tal_pc_list (RTLabs_status ge) flX s1X s2X tal →
2532  bad_label_list g l l1 ≝ ?.
2533cases tal
2534[ #s1 #s2 #EX #CL #CS
2535  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2536  >(pc_label_eq … PC0 PC1) %1
2537| #s1 #s2 #EX #CL
2538  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2539  >(pc_label_eq … PC0 PC1) %1
2540| #pre #start #final #EX #CL #AF #tlr #CS
2541  #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct
2542  >(pc_label_eq … PC0 PC1) %1
2543| #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
2544  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2545  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2546  | #NE #IN
2547    lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1
2548    [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G
2549      lapply (pc_label_call_eq … PC1) #E destruct
2550      @(tal_pc_loop_tail … PC0 tal' l1 PC' G CS IN)
2551    | @⊥ inversion PC1 #a #b #E1 #E2 #E3 destruct
2552    ]
2553  ]
2554| #fl #pre #init #end #EX #tal' #CL #CS
2555  #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim
2556  [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1
2557  | #NE #IN
2558    cases (declassify_state … EX CL)
2559    #f * #fs * #m * #S * #M #E destruct
2560    cut (l1 = next f)
2561    [ whd in PC1:(?%?); cases S in M PC1; [*] #fn #S #M whd in ⊢ (?%? → ?); #PC1
2562      inversion PC1 normalize #a #b #E1 #E2 #E3 destruct % ] #E destruct
2563    cases EX #tr * #EV #NX
2564    cases (eval_successor … EV)
2565    [ * #CL' @⊥ cases (tal_return … CL' tal') #EX' * #CL'' * #E1 #E2 destruct
2566      lapply (memb_single … IN) @(declassify_pc … EX' CL'') whd
2567      #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct
2568    | * #l' * #AS #SC
2569      lapply (graph_fn_state … G) #E destruct
2570      @(gl_step … l')
2571      [ @(next_ok f)
2572      | @Exists_memb @SC
2573      | @notb_Prop @(not_to_not … NCS) #ISL @(proj1 ?? (RTLabs_costed ??))
2574        @ISL
2575      | @(tal_pc_loop_tail … PC0 tal' … (actual_successor_pc_label … AS))
2576        [ <NX in AS ⊢ %; #AS <(state_fn_next … EV AS) @G
2577        | *: //
2578        ]
2579      ]
2580    ]
2581  ]
2582] qed.
2583
2584(* Some inversion lemmas on the bounds.
2585
2586   For the first step just get a bound after the step; we don't care what it is,
2587   just that it exists. *)
2588   
2589lemma bound_step1 : ∀g,l1,n.
2590  bound_on_instrs_to_cost g l1 n →
2591  ∀l2,H. Exists ? (λl.l = l2) (successors (lookup_present … g l1 H)) →
2592  ∃m. bound_on_instrs_to_cost' g l2 m.
2593#g #l1X #nX * #l #n #H #EX #l2 #H' #EX' %{n} @EX @EX'
2594qed.
2595
2596lemma bound_zero1 : ∀g,l.
2597  ¬ bound_on_instrs_to_cost g l 0.
2598#g #l % #B lapply (refl ? O) cases B in ⊢ (???% → ?);
2599#l' #n #H #_ whd in ⊢ (???% → ?); #E destruct
2600qed.
2601
2602lemma bound_zero : ∀g,l.
2603  bound_on_instrs_to_cost' g l 0 →
2604  ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)).
2605#g #l #B
2606@(match B return λl,n,B. n = O → ∃H. bool_to_Prop (is_cost_label (lookup_present … g l H)) with
2607  [ boitc_here l n H CS ⇒ ?
2608  | boitc_later _ _ _ _ B' ⇒ ?
2609  ] (refl ? O))
2610[ #E >E %{H} @CS
2611| #E >E in B'; #B' @⊥ @(absurd … B' (bound_zero1 …))
2612] qed.
2613
2614lemma bound_step : ∀g,l,n.
2615  bound_on_instrs_to_cost' g l (S n) →
2616  ∃H. (bool_to_Prop (is_cost_label (lookup_present … g l H)) ∨
2617       (let stmt ≝ lookup_present … g l H in
2618        ∀l'. Exists label (λl0. l0 = l') (successors stmt) →
2619             bound_on_instrs_to_cost' g l' n)).
2620#g #lX #n #B lapply (refl ? (S n)) cases B in ⊢ (???% → %);
2621[ #l #n #H #CS #E %{H} %1 @CS
2622| #l #m #H #CS *
2623  #l' #n' #H' #EX #E destruct %{H'} %2
2624  #l'' #EX' @EX @EX'
2625] qed.
2626
2627lemma bad_label_list_no_cost : ∀g,l1,l2.
2628  bad_label_list g l1 l2 →
2629  ∀H1. ¬ is_cost_label (lookup_present … g l1 H1) →
2630  ∃H2. bool_to_Prop (¬ is_cost_label (lookup_present … g l2 H2)).
2631#g #l1 #l2 * /2/
2632qed.
2633
2634(* Show that a bad_label_list is incompatible with a bound on the number of
2635   instructions to a cost label, by induction on the bound and the invariant
2636   that none of the instructions involved are a cost label. *)
2637   
2638lemma loop_soundness_contradiction : ∀g,l1,l2,H1.
2639  Exists ? (λl.l = l2) (successors (lookup_present … g l1 H1)) →
2640  ¬ is_cost_label (lookup_present … g l1 H1) →
2641  bad_label_list g l1 l2 →
2642  ∀n,l'.
2643  bad_label_list g l1 l' →
2644  ¬ bound_on_instrs_to_cost' g l' n.
2645#g #l1 #l2 #H1 #SC1 #NCS1 #BLL2
2646#n elim n
2647[ #l #BLL % #BOUND
2648  cases (bound_zero … BOUND) #H' #ICS
2649  cases (bad_label_list_no_cost … BLL H1 NCS1) #H''
2650  >ICS *
2651| #m #IH #l #BLL % #BOUND
2652  cases (bound_step … BOUND) #H' *
2653  [ #ICS cases (bad_label_list_no_cost … BLL H1 NCS1) #H'' >ICS *
2654  | #EX_BOUND inversion BLL
2655    [ #E1 #E2 destruct
2656      lapply (IH l2 BLL2)
2657      lapply (EX_BOUND … SC1)
2658      @absurd
2659    | #l3 #l4 #H3 #SC2 #NCS3 #BLL4 #_ #E1 #E2 destruct
2660      lapply (IH l4 BLL4)
2661      cut (Exists ? (λl.l=l4) (successors (lookup_present … H3)))
2662      [ cases (memb_exists … SC2) #left * #right #E >E @Exists_mid % ]
2663      #SC2' lapply (EX_BOUND … SC2')
2664      @absurd
2665    ]
2666  ]
2667] qed.
2668
2669(* Combine the above results to show that the pc of a normal instruction
2670   execution state can't be repeated within a trace_any_label. *)
2671
2672lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_state ge. ∀fl,tal.
2673  soundly_labelled_state s1 →
2674  RTLabs_classify s1 = cl_other →
2675  as_execute (RTLabs_status ge) s1 s2 →
2676  ¬ as_costed (RTLabs_status ge) s2 →
2677  ¬ as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s3 tal.
2678#ge #s1 #s2 #s3 #fl #tal #S1 #CL #EX #CS2 cases (declassify_state … EX CL)
2679#f * #fs * #m * * [* *] #fn #S * * #FFP #M #E destruct
2680cases EX #tr * #EV #NX
2681cases (eval_successor … EV)
2682[ * #CL2 #SC
2683  cases (tal_return … CL2 tal) #EX2 * #CL2' * #E1 #E2 destruct
2684  @notb_Prop % whd in match (tal_pc_list ?????); #IN
2685  lapply (memb_single … IN) cases (declassify_state … EX2 CL2)
2686  #ret * #dst * #fs2 * #m2 * * [2: #fn2 #S2] * #M2 #E destruct
2687  normalize #E destruct
2688| * #l2 * #AS2 #SC1 @notb_Prop % #IN
2689  (* Two cases: either s1 is a cost label, and it's pc's appearence later on
2690     is impossible because nothing later in tal can be a cost label; or it
2691     isn't and we get a loop of successor instruction labels that breaks the
2692     soundness of the cost labelling. *)
2693  cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M)))
2694  [ * #H @H
2695    cases (memb_exists … IN) #left * #right #E
2696    @(All_split … (tal_tail_not_costed … tal CS2) … E)
2697  | (* Now show that the loop invalidates soundness. *)
2698    cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))
2699    [ %1 ] #PC1
2700    cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2)
2701    [ /2/ ] #PC2
2702    lapply (tal_pc_loop_tail … (f_graph (func f)) … PC1 … PC2 … CS2 IN)
2703    [ <NX <(state_fn_next … EV AS2) % // ]
2704    cases S1 #SLF #_ cases (SLF (next f) (next_ok f))
2705    #bound1 #BOUND1 #BLL #CS1
2706    cases (bound_step1 … BOUND1 … SC1)
2707    #bound2 #BOUND2 @(absurd … BOUND2)
2708    @(loop_soundness_contradiction … BLL … BLL)
2709    [ @(next_ok f)
2710    | @SC1
2711    | @notb_Prop @(not_to_not … CS1) #CS
2712      @(proj1 … (RTLabs_costed …)) @CS
2713    ]
2714  ]
2715] qed.
2716
2717(* We need a similar result for call states.  We'll do this by showing that
2718   the state following the call state is a normal instruction state and using
2719   the previous result. *)
2720
2721lemma pc_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2722  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2723  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2724  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2725  state_fn … s1 = state_fn … s2 →
2726  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
2727#ge * #s1 #S1 #M1 #CL1
2728cases (rtlabs_call_inv … CL1) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
2729* #s2 #S2 #M2 #CL2
2730cases (rtlabs_call_inv … CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
2731* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
2732* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
2733whd in ⊢ (% → ?);
2734[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
2735    * * #N1 #F1 #STK1
2736    whd in STK1 ⊢ (% → ?);
2737    [ cases fs2 in M2 ⊢ %; [ #M2 * ] #f2' #fs2 cases S2 [*] #fn2 * [* #X *] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2738      normalize in ⊢ (% → % → ?); #E1 #E2
2739      cases S3 in M3 STK1 ⊢ %; [ * ] #fn3 #S3' #M3 #STK1
2740      cases S4 in M4 STK2 ⊢ %; [ * ] #fn4 #S4' #M4 #STK2
2741      whd in ⊢ (??%%); <N2 <N1 destruct >e1 %
2742    | #E destruct whd in ⊢ (??%% → ??%% → ?); cases S2 in M2 ⊢ %; [ * ] #fn2 #S2' #M2 normalize in ⊢ (% → ?);
2743      #X destruct
2744    ]
2745| #F destruct whd in ⊢ (% → ?); cases fs2 in M2 ⊢ %; [ #M *] #f2 #fs2' cases S2 [*] #fn2 #S2' #M2 * * #N2 #F2 #STK2
2746  cases S1 in M1 ⊢ %; [*] #fn1 #S1' #M1
2747  normalize in ⊢ (% → ?); #E destruct
2748| #F destruct whd in ⊢ (% → ?); #F destruct #_ #_ %
2749] qed.
2750
2751lemma eq_pc_eq_classify : ∀ge,s1,s2.
2752  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2753  RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
2754#ge
2755* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
2756* * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
2757whd in ⊢ (??%% → ?); #E destruct try %
2758[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
2759  cases (lookup_present … next2 nok1)
2760  normalize //
2761| 2,3,7: cases S1 in M1 E; [2,4,6:#fn1' #S1'] #M1 whd in ⊢ (??%% → ?); #E destruct
2762| 4,5,6: cases S2 in M2 E; [2,4,6:#fn2' #S2'] #M2 whd in ⊢ (??%% → ?); #E destruct
2763] qed.
2764
2765lemma classify_after_return_eq : ∀ge,s1,CL1,s2,CL2,s3,s4.
2766  as_after_return (RTLabs_status ge) «s1,CL1» s3 →
2767  as_after_return (RTLabs_status ge) «s2,CL2» s4 →
2768  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2769  state_fn … s1 = state_fn … s2 →
2770  RTLabs_classify (Ras_state … s3) = RTLabs_classify (Ras_state … s4).
2771#ge #s1 #CL1 #s2 #CL2 #s3 #s4 #AF1 #AF2 #PC #FN
2772@eq_pc_eq_classify
2773@(pc_after_return_eq … AF1 AF2 PC FN)
2774qed.
2775
2776lemma cost_labels_are_other : ∀ge,s.
2777  as_costed (RTLabs_status ge) s →
2778  RTLabs_classify (Ras_state … s) = cl_other.
2779#ge * * [ #f #fs #m #S #M | #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
2780#CS lapply (proj2 … (RTLabs_costed …) … CS)
2781whd in ⊢ (??%? → %);
2782[ whd in ⊢ (? → ??%?); cases (lookup_present … (next_ok f)) normalize
2783  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct %
2784| *: #E destruct
2785] qed.
2786
2787lemma eq_pc_cost : ∀ge,s1,s2.
2788  as_pc_of (RTLabs_status ge) s1 = as_pc_of (RTLabs_status ge) s2 →
2789  as_costed (RTLabs_status ge) s1 →
2790  as_costed (RTLabs_status ge) s2.
2791#ge
2792* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 #S1 #M1 ]
2793[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
2794* * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2 | 2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 * [2: #fn2 #S2] #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
2795whd in ⊢ (??%% → ?); #E destruct
2796#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
2797cases M1 #FFP1 #M1' cases M2 >FFP1 #E #M2' destruct #H @H
2798qed.
2799
2800lemma first_state_in_tal_pc_list : ∀ge,fl,s1,s2,tal.
2801  RTLabs_classify (Ras_state … s1) = cl_other →
2802  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s1 s2 tal.
2803#ge #flX #s1X #s2X *
2804[ #s1 #s2 #EX *
2805  [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥  >CL in CL'; #CL' destruct
2806  | #CL #CS #CL' @eq_true_to_b @memb_hd
2807  ]
2808| #s1 #s2 #EX #CL whd in CL; #CL' @⊥ >CL in CL'; #CL' destruct
2809| #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct
2810| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ whd in CL; >CL in CL'; #CL' destruct
2811| #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd
2812] qed.
2813
2814lemma state_fn_after_return : ∀ge,pre,post,CL.
2815  as_after_return (RTLabs_status ge) «pre,CL» post →
2816  state_fn … pre = state_fn … post.
2817#ge * #pre #preS #preM * #post #postS #postM #CL #AF
2818cases (rtlabs_call_inv … CL) #fd * #args * #dst * #fs * #m #E destruct
2819cases post in postM AF ⊢ %;
2820[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
2821  cases preS in preM AF ⊢ %; [*]
2822  #fn *
2823  [ cases fs [ #M * ]
2824    #f #fs' * #FFP *
2825  | #fn' #S cases fs [ #M * ]
2826    #f #fs' #M * * #N #F #PC destruct %
2827  ]
2828| #A #B #C #D #E #F *
2829| #A #B #C #D #E *
2830| #r #M' #AF whd in AF; destruct
2831  cases preS in preM ⊢ %;
2832  [ // | #fn * [ // | #fn' #S * #FFP * ] ]
2833] qed.
2834
2835lemma state_fn_other : ∀ge,s1,s2.
2836  RTLabs_classify (Ras_state … s1) = cl_other →
2837  as_execute (RTLabs_status ge) s1 s2 →
2838  RTLabs_classify (Ras_state … s2) = cl_return ∨
2839  state_fn … s1 = state_fn … s2.
2840#ge #s1 #s2 #CL #EX
2841cases (declassify_state … EX CL)
2842#f * #fs * #m * * [**] #fn #S * #M #E destruct
2843inversion (eval_preserves_ext … EX)
2844[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
2845| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct %2 %
2846| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
2847| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
2848| #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
2849| #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 destruct
2850] qed.
2851
2852(* The main part of the proof is to walk down the trace_any_label and find the
2853   repeated call state, then show that its successor appears as well. *)
2854
2855let rec pc_after_call_repeats_aux ge s1 s1' s2 s3 s4 CL1 fl tal
2856  (AF1:as_after_return (RTLabs_status ge) «s1,CL1» s2)
2857  (CL2:RTLabs_classify (Ras_state … s2) = cl_other)
2858  (CS2:Not (as_costed (RTLabs_status ge) s2))
2859  (EX1:as_execute (RTLabs_status ge) s1 s1') on tal :
2860  state_fn … s1 = state_fn … s3 →
2861  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal →
2862  as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal ≝ ?.
2863cases tal
2864[ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥
2865  whd in match (tal_pc_list ?????) in IN;
2866  lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee
2867  cases CL3 #CL3' @(declassify_pc … EX3 CL3') #fn #l
2868  #IN' destruct
2869| #s2 #s4 #EX2 #CL2 #FN #IN @⊥
2870  lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee
2871  @(declassify_pc … EX2 CL2) whd #fn
2872  #IN' destruct
2873| #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN
2874  lapply (memb_single … IN) #E
2875  lapply (pc_after_return_eq … AF1 AF3 E FN) #PC
2876  @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) //
2877| #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN
2878  whd in ⊢ (?% → ?); @eqb_elim
2879  [ #PC #_
2880    >(pc_after_return_eq … AF1 AF3 PC FN) @eq_true_to_b @memb_cons @first_state_in_tal_pc_list
2881    <(classify_after_return_eq … AF1 AF3 PC FN) assumption
2882  | #NPC #IN whd in IN:(?%); @eq_true_to_b @memb_cons
2883    @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1 … IN)
2884    >FN @(state_fn_after_return … AF3)
2885  ]
2886| #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN
2887  @eq_true_to_b @memb_cons
2888  @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1)
2889  [ >FN cases (state_fn_other … CL3 EX3)
2890    [ #CL3' @⊥
2891      cases (tal_return … CL3' tal3')
2892      #EX3' * #CL3'' * #E1 #E2 destruct
2893      whd in IN:(?%); lapply IN @eqb_elim
2894      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct
2895      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1 >CL3' #E destruct
2896      ]
2897    | //
2898    ]
2899  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2900    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3 #E destruct
2901    | #NE #IN @IN
2902    ]
2903  ]
2904] qed.
2905
2906(* Then we can start the proof by finding the original successor state... *)
2907
2908lemma pc_after_call_repeats : ∀ge,s1,s1',CL,fl,s2,s4,tal.
2909  as_execute (RTLabs_status ge) s1 s1' →
2910  as_after_return (RTLabs_status ge) «s1,CL» s2 →
2911  ¬as_costed (RTLabs_status ge) s2 →
2912  as_pc_of (RTLabs_status ge) s1 ∈ tal_pc_list (RTLabs_status ge) fl s2 s4 tal →
2913  ∃s3,EX,CL',CS,tal'.
2914    tal = tal_step_default (RTLabs_status ge) fl s2 s3 s4 EX tal' CL' CS ∧
2915    bool_to_Prop (as_pc_of (RTLabs_status ge) s2 ∈ tal_pc_list (RTLabs_status ge) fl s3 s4 tal').
2916#ge #s1 #s1' #CL #flX #s2X #s4X *
2917[ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥
2918  whd in match (tal_pc_list ?????) in IN;
2919  lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee
2920  cases CL2 #CL2' @(declassify_pc … EX2 CL2') #fn #l
2921  #IN' destruct
2922| #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥
2923  lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee
2924  @(declassify_pc … EX2 CL2) whd #fn
2925  #IN' destruct
2926| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
2927  cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2928  cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2929  cases AF1
2930| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
2931  cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
2932  cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
2933  cases AF1
2934| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
2935  %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ]
2936  (* Now that we've inverted the first part of the trace, look for the repeat. *)
2937  @(pc_after_call_repeats_aux … CL … AF1 CL2 CS2 EX1)
2938  [ >(state_fn_after_return … AF1)
2939    cases (state_fn_other … CL2 EX2)
2940    [ #CL3 @⊥
2941      cases (tal_return … CL3 tal3)
2942      #EX3 * #CL3' * #E1 #E2 destruct
2943      whd in IN:(?%); lapply IN @eqb_elim
2944      [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct
2945      | #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL >CL3' #E destruct
2946      ]
2947    | //
2948    ]
2949  | lapply IN whd in ⊢ (?% → ?); @eqb_elim
2950    [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2 #E destruct
2951    | #NE #IN @IN
2952    ]
2953  ]
2954] qed.
2955
2956(* And then we get our counterpart to no_loops_in_tal for calls: *)
2957
2958lemma no_repeats_of_calls : ∀ge,pre,start,after,final,fl,CL.
2959  ∀tal:trace_any_label (RTLabs_status ge) fl after final.
2960  as_execute (RTLabs_status ge) pre start →
2961  as_after_return (RTLabs_status ge) «pre,CL» after →
2962  ¬as_costed (RTLabs_status ge) after →
2963  soundly_labelled_state (Ras_state ge after) →
2964  ¬as_pc_of (RTLabs_status ge) pre ∈ tal_pc_list (RTLabs_status ge) fl after final tal.
2965#ge #pre #start #after #final #fl #CL #tal #EX #AF #CS #SOUND @notb_Prop % #IN
2966cases (pc_after_call_repeats … EX AF CS IN)
2967#s * #EX * #CL' * #CSx * #tal' * #E #IN'
2968@(absurd ? IN')
2969@Prop_notb
2970@no_loops_in_tal assumption
2971qed.
2972
2973(* Show that if a state is soundly labelled, then so are the states following
2974   it in a trace. *)
2975
2976lemma soundly_step : ∀ge,s1,s2.
2977  soundly_labelled_ge ge →
2978  as_execute (RTLabs_status ge) s1 s2 →
2979  soundly_labelled_state (Ras_state … s1) →
2980  soundly_labelled_state (Ras_state … s2).
2981#ge #s1 #s2 #GE * #tr * #EX #NX
2982@(soundly_labelled_state_step … GE … EX)
2983qed.
2984
2985let rec tlr_sound ge s1 s2
2986  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
2987  (GE:soundly_labelled_ge ge)
2988on tlr : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2989match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) with
2990[ tlr_base _ _ tll ⇒ λS1. tll_sound … tll GE S1
2991| tlr_step _ _ _ tll tlr' ⇒ λS1. let S2 ≝ tll_sound ge … tll GE S1 in
2992                            tlr_sound … tlr' GE S2
2993]
2994and tll_sound ge fl s1 s2
2995  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
2996  (GE:soundly_labelled_ge ge)
2997on tll : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
2998match tll with
2999[ tll_base _ _ _ tal _ ⇒ tal_sound … tal GE
3000]
3001and tal_sound ge fl s1 s2
3002  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
3003  (GE:soundly_labelled_ge ge)
3004on tal : soundly_labelled_state (Ras_state … s1) → soundly_labelled_state (Ras_state … s2) ≝
3005match tal with
3006[ tal_base_not_return _ _ EX _ _ ⇒ λS1. soundly_step … GE EX S1
3007| tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1
3008| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1)
3009| tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1))
3010| tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1)
3011].
3012
3013(* And join everything up to show that soundly labelled states give unrepeating
3014   traces. *)
3015
3016let rec tlr_sound_unrepeating ge
3017  (s1,s2:RTLabs_status ge)
3018  (GE:soundly_labelled_ge ge)
3019  (tlr:trace_label_return (RTLabs_status ge) s1 s2)
3020on tlr : soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) … tlr ≝
3021match tlr return λs1,s2,tlr. soundly_labelled_state (Ras_state … s1) → tlr_unrepeating (RTLabs_status ge) s1 s2 tlr with
3022[ tlr_base _ _ tll ⇒ λS1. tll_sound_unrepeating … GE tll S1
3023| tlr_step _ _ _ tll tlr' ⇒ λS1. conj ?? (tll_sound_unrepeating ge … GE tll S1) (tlr_sound_unrepeating … GE tlr' (tll_sound … tll GE S1))
3024]
3025and tll_sound_unrepeating ge fl
3026  (s1,s2:RTLabs_status ge)
3027  (GE:soundly_labelled_ge ge)
3028  (tll:trace_label_label (RTLabs_status ge) fl s1 s2)
3029on tll : soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) … tll ≝
3030match tll return λfl,s1,s2,tll. soundly_labelled_state (Ras_state … s1) → tll_unrepeating (RTLabs_status ge) fl s1 s2 tll with
3031[ tll_base _ _ _ tal _ ⇒ tal_sound_unrepeating … GE tal
3032]
3033and tal_sound_unrepeating ge fl
3034  (s1,s2:RTLabs_status ge)
3035  (GE:soundly_labelled_ge ge)
3036  (tal:trace_any_label (RTLabs_status ge) fl s1 s2)
3037on tal : soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) … tal ≝
3038match tal return λfl,s1,s2,tal. soundly_labelled_state (Ras_state … s1) → tal_unrepeating (RTLabs_status ge) fl s1 s2 tal with
3039[ tal_base_not_return _ _ EX _ _ ⇒ λS1. I
3040| tal_base_return _ _ EX _ ⇒ λS1. I
3041| tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1.
3042    tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1)
3043| tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1.
3044    conj ?? (conj ???
3045     (tal_sound_unrepeating … GE tal (tlr_sound … tlr GE (soundly_step … GE EX S1))))
3046     (tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1))
3047| tal_step_default _ pre init end EX tal CL _ ⇒ λS1.
3048    conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1))
3049].
3050[ @(no_repeats_of_calls … EX AF) [ assumption |
3051  @(tlr_sound … tlr) [ assumption | @(soundly_step … GE EX S1) ] ]
3052| @no_loops_in_tal //
3053] qed.
3054
Note: See TracBrowser for help on using the repository browser.