source: src/RTLabs/Traces.ma @ 2295

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

Start on showing unrepeating property of RTLabs structured traces: shadow
stack of function ids is preserved, traces follow successive instructions.

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