source: src/RTLabs/RTLabs_partial_traces.ma @ 3096

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

Remove some leftovers.

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