source: src/RTLabs/MeasurableToStructured.ma @ 3022

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

Finish up measurable to structured proof, exposing the prefix and keeping
reasoning about the stack space purely in terms of the preserved
observables.

File size: 34.4 KB
Line 
1
2include "RTLabs/RTLabs_partial_traces.ma".
3include "common/Measurable.ma".
4include "common/stacksize.ma".
5
6definition RTLabs_stack_ident :
7  genv →
8  ∀s:state.
9  match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
10  ident ≝
11λge,s.
12match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
13[ Callstate id _ _ _ _ _ ⇒ λ_. id
14| State f fs m ⇒ λH.⊥
15| _ ⇒ λH.⊥
16].
17try @H
18whd in match (RTLabs_classify ?) in H;
19cases (next_instruction f) in H;
20normalize //
21qed.
22
23definition RTLabs_pcsys ≝ mk_preclassified_system
24  RTLabs_fullexec
25  (λ_.RTLabs_cost)
26  (λ_.RTLabs_classify)
27  RTLabs_stack_ident.
28
29definition state_at : ∀C:preclassified_system.
30  ∀p:program ?? C. nat →
31  res (state … C (make_global … C p)) ≝
32λC,p,n.
33  let g ≝ make_global … (pcs_exec … C) p in
34  let C' ≝ pcs_to_cs C g in
35  ! s0 ← make_initial_state … p;
36  ! 〈prefix,s1〉 ← exec_steps n ?? (cs_exec … C') g s0;
37  return s1.
38
39definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝
40λge,s.
41match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with
42[ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉
43| Wrong m ⇒ λ_. Wrong ??? m
44| Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO)
45] (next_state ge s).
46//
47qed.
48
49lemma drop_exec_ext : ∀ge,s,tr,s'.
50  eval_ext_statement ge s = return 〈tr,s'〉 →
51  eval_statement ge s = return 〈tr,Ras_state … s'〉.
52#ge #s #tr #s'
53whd in ⊢ (??%? → ?);
54letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
55cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
56[ // ]
57generalize in match f; -f
58cases (eval_statement ge s)
59[ #o #k #n #N #E whd in E:(??%%); destruct
60| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
61| #m #n #N #E whd in E:(??%%); destruct
62] qed.
63
64lemma as_eval_ext_statement : ∀ge,s,tr,s'.
65  eval_ext_statement ge s = Value … 〈tr,s'〉 →
66  as_execute (RTLabs_status ge) s s'.
67#ge #s #tr #s' #EX
68whd %{tr} %{(drop_exec_ext … EX)}
69whd in EX:(??%?);
70letin ns ≝ (next_state ge s) in EX; #EX
71change with (ns s' tr ?) in match (next_state ge s s' tr ?);
72generalize in match (drop_exec_ext ?????);
73#EX'
74generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %);
75#E destruct @e1
76qed.
77
78definition RTLabs_ext_exec : trans_system io_out io_in ≝
79  mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement.
80
81definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
82λp.
83  let ge ≝ make_global p in
84  do m ← init_mem … (λx.x) p;
85  let main ≝ prog_main ?? p in
86  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
87  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
88  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
89  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
90% [ % assumption | % ]
91qed.
92
93lemma initial_states_OK : ∀p,s.
94  make_ext_initial_state p = return s →
95  make_initial_state p = return (Ras_state … s).
96#p #s #E
97cases (bind_inversion ????? E) -E #m * #E1 #E
98cases (bind_as_inversion ????? E) -E #b * #Eb #E
99cases (bind_as_inversion ????? E) -E #f * #Ef #E
100whd in ⊢ (??%?); >E1
101whd in ⊢ (??%?); >Eb
102whd in ⊢ (??%?); >Ef
103whd in E:(??%%) ⊢ (??%?); destruct
104%
105qed.
106
107lemma initial_states_OK' : ∀p,s.
108  make_initial_state p = return s →
109  ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M).
110#p #s #E
111cases (bind_inversion ????? E) -E #m * #E1 #E
112cases (bind_inversion ????? E) -E #b * #Eb #E
113cases (bind_inversion ????? E) -E #f * #Ef #E
114whd in E:(??%%); destruct
115%{[b]} % [ % [ % assumption | % ] ]
116whd in ⊢ (??%?); >E1
117whd in ⊢ (??%?); generalize in match (refl ??);
118>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
119whd in ⊢ (??%?); generalize in match (refl ??);
120>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
121qed.
122
123
124definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
125  mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
126
127definition RTLabs_ext_pcsys ≝ mk_preclassified_system
128  RTLabs_ext_fullexec
129  (λg,s. RTLabs_cost (Ras_state … s))
130  (λg,s. RTLabs_classify (Ras_state … s))
131  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
132
133lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
134  will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
135  ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX).
136    will_return_end … WR = ?.
137[2: %{s'} @ft_stop ] (* XXX replace ? above? *)
138#ge #trace0 elim trace0
139[ #depth #n #s #s' #EX *
140| * #s1 #tr1 #tl #IH #depth #n #s #s' #EX
141  lapply (exec_steps_length … EX) #E1
142  lapply (exec_steps_first … EX) #E2
143  lapply (refl ? (eval_statement ge s))
144  cases (eval_statement ge s) in ⊢ (???% → ?);
145  [ #o #k destruct #EV @⊥
146    whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX;
147    [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????);
148      >EV #EX whd in EX:(??%%); destruct
149    | #r #EX whd in EX:(??%%); destruct
150    ]
151  | 3: #m #EV @⊥ destruct
152    whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX;
153    [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????);
154      >EV #EX whd in EX:(??%%); destruct
155    | #r #EX whd in EX:(??%%); destruct
156    ]
157  ] * #tr2 #s2 #EV >E1 in EX; #EX
158  whd in ⊢ (?% → ?);
159  lapply (refl ? (cs_classify ? s1))
160  cases (cs_classify ??) in ⊢ (???% → %);
161  #CL whd in ⊢ (?% → ?);
162  [ cases depth
163    [ whd in ⊢ (?% → ?); cases tl in EX ⊢ %;
164      [ #EX #_
165        lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
166        %{(wr_base …)}
167        [ destruct @CL
168        | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?);
169          whd in cEX:(??%%); destruct %
170        ]
171      | * #s3 #tr3 #tl3 #EX *
172      ]
173    | #depth' whd in ⊢ (?% → ?); #H
174      lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
175      cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
176      %{(wr_ret …)}
177      [ @WR'
178      | destruct @CL
179      | @WRe
180      ]
181    ]
182  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
183    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
184    %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ]
185  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
186    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
187    %{(wr_call …)} [ @WR' | destruct @CL | @WRe ]
188  | cases (RTLabs_notail … CL)
189  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
190    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
191    %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ]
192  ]
193] qed.
194
195
196lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
197  eval_statement ge s = return 〈tr,s'〉 →
198  ∃S,M. eval_ext_statement ge s = return 〈tr,mk_RTLabs_ext_state … s' S M〉.
199#ge #s #tr #s' #EV
200whd in match (eval_ext_statement ??);
201letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
202cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
203[ // ]
204generalize in match f; -f
205>EV #next #NEXT whd in ⊢ (??(λ_.??(λ_.??%?)));
206lapply (NEXT … (refl ??))
207cases (next s' tr ?) #s'' #S'' #M'' #E destruct %{S''} %{M''} %
208qed.
209
210lemma intensional_state_change_State : ∀ge,cs,f,fs,m.
211  intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (State f fs m) = 〈cs,[ ]〉.
212#ge #cs #f #fs #m
213whd in ⊢ (??%?);
214generalize in match (cs_callee ??);
215whd in match (cs_classify ??); cases (next_instruction f) //
216qed.
217
218lemma final_pre_S : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
219  eval_statement ge s = Value ??? 〈tr,s'〉 →
220  match s' with [Finalstate _ ⇒ Ras_fn_stack … s = [ ] | _ ⇒ True].
221#ge #s #tr #s' #EV
222cases (extend_RTLabs_eval_statement … EV) #S * #M #EV'
223inversion (eval_preserves_ext … (as_eval_ext_statement … EV'))
224[ 6: #ge' #r #dst #m #M1 #M2 #E1 #E2 #E3 #E4 destruct whd %
225| *: #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 try #x15 try #x16 try #x17 try #x18 destruct //
226] qed.
227
228lemma extend_RTLabs_step : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s',cs.
229  eval_statement ge s = Value … 〈tr,s'〉 →
230  All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) cs →
231  ∃S',M'.
232    eval_ext_statement ge s = Value … 〈tr,mk_RTLabs_ext_state … s' S' M'〉 ∧
233    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s')).
234#ge #s #tr #s' #cs #EV #STACK
235whd in match (eval_ext_statement ??);
236letin ns ≝ (next_state ge s)
237cut (∀s',t,EV. Ras_state … (ns s' t EV) = s' ∧
238  match s' with
239   [ State _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s
240   | Callstate fid _ _ _ _ _ ⇒ ∃b. symbol_for_block … ge b = Some ? fid ∧ Ras_fn_stack … (ns s' t EV) = b::(Ras_fn_stack … s)
241   | Returnstate _ _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = tail … (Ras_fn_stack … s)
242   | Finalstate _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s
243   ])
244[ #s'' #t #EV' % [ % |
245    cases s'' in EV' ⊢ %; //
246    [ #fid #fn #args #ret #fs #m #EV''
247      %{(func_block_of_exec … EV'')} %
248      [ cases (func_block_of_exec … EV'') #b * #FS #FFP
249        @(symbol_for_block_fn … FS FFP)
250      | %
251      ]
252    | #r #EV whd lapply (final_pre_S … EV) whd in ⊢ (% → ?); #E >E %
253    ]
254  ]
255]
256generalize in match ns; -ns
257>EV #next #NEXT cases (NEXT … (refl ??))
258lapply (refl ? (next s' tr (refl ??)))
259cases (next s' tr ?) in ⊢ (???% → ?);
260#s'' #S'' #M''
261#Enext1 >Enext1 #Enext2 destruct #Snext %{S''} %{M''}
262%
263[ whd in ⊢ (??%%); >Enext1 %
264| cases s' in Snext ⊢ %;
265  [ #f #fs #m whd in ⊢ (% → ?); #E destruct
266    >intensional_state_change_State @STACK
267  | #fid #fn #args #ret #fs #m whd in ⊢ (% → ?); * #b * #SYM #ES destruct
268    whd in match (intensional_state_change ???);
269    whd in match (cs_callee ???);
270    % [ @SYM | @STACK ]
271  | #rv #rr #fs #m whd in ⊢ (% → ?); #ES destruct
272    whd in match (intensional_state_change ???);
273    >(?:\fst ? = tail ? cs)
274    [2: cases cs // ]
275    @All2_tail
276    @STACK
277  | #r whd in ⊢ (% → ?); #E destruct
278    whd in match (intensional_state_change ???);
279    @STACK
280  ]
281] qed.
282
283lemma callee_ext : ∀ge,s,S,M.
284  cs_callee (pcs_to_cs RTLabs_pcsys ge) s = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) (mk_RTLabs_ext_state ge s S M).
285#ge * //
286qed.
287
288lemma int_state_change_ext : ∀ge,cs,s,S,M.
289  intensional_state_change (pcs_to_cs RTLabs_pcsys ge) cs s =
290  intensional_state_change (pcs_to_cs RTLabs_ext_pcsys ge) cs (mk_RTLabs_ext_state ge s S M).
291#ge #cs #s #S #M
292whd in ⊢ (??%%);
293<callee_ext %
294qed.
295
296lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace.
297  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
298  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 →
299  All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (Ras_state … s))) →
300  ∃trace',S,M.
301    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
302    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) cs trace' = 〈cs',itrace〉 ∧
303    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
304#ge #n0 elim n0
305[ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct
306  #E whd in E:(??%%); destruct
307  #CS %{[ ]}
308  %{S} %{M} % [ % [ % | % ] | @CS ]
309| #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX
310  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
311  >E whd in ⊢ (??%? → ?); @pair_elim #cs1 #itrace1 #ITOT1
312  whd in ⊢ (??%? → ?); @pair_elim #cs2 #itrace2 #ITOT2 #E' destruct
313  #STACK
314  cases (extend_RTLabs_step ge (mk_RTLabs_ext_state ge s S M) ??? STEP STACK)
315  #S' * #M' * #STEP' #STACK'
316  cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK')
317  #tl' * #S'' * #M'' * * #EX'' #ITOT'' #STACK''
318  %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''}
319  % [ %
320  [ whd in ⊢ (??%?);
321    change with (RTLabs_is_final s) in match (is_final ?????);
322    change with (RTLabs_is_final s) in match (is_final ?????) in NF;
323    >NF whd in ⊢ (??%?);
324    change with (eval_ext_statement ??) in match (step ?????);
325    >STEP' whd in ⊢ (??%?);
326    >EX'' %
327  | whd in ⊢ (??%?); <int_state_change_ext >ITOT1
328    whd in ⊢ (??%?); >ITOT'' %
329 ]| @STACK''
330  ]
331] qed.
332
333lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace.
334  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
335  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 →
336  make_ext_initial_state p = OK ? s →
337  ∃trace',S,M.
338    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
339    intensional_trace_of_trace (pcs_to_cs … RTLabs_ext_pcsys ge) [ ] trace' = 〈cs',itrace〉 ∧
340    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
341#p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT
342@(extend_RTLabs_exec_steps … EXEC ITOT)
343cases (bind_inversion ????? INIT) -INIT #m * #E1 #INIT
344cases (bind_as_inversion ????? INIT) -INIT #b * #Eb #INIT
345cases (bind_as_inversion ????? INIT) -INIT #f * #Ef #INIT
346whd in INIT:(??%%); lapply (Ras_fn_match … s) destruct
347* * #FS #FFP #_
348% [ >(symbol_for_block_fn … FS FFP) % | % ]
349qed.
350
351lemma label_to_return_state_labelled : ∀C,n,s,trace,s'.
352  trace_is_label_to_return C trace →
353  exec_steps n ?? C ? s = OK ? 〈trace,s'〉 →
354  cs_labelled C s.
355#C #n #s #trace #s'
356* #tr * #s1 * #trace' * #tr' * #s2 * * #E #CS #_ destruct
357#EX >(exec_steps_first … EX)
358@CS
359qed.
360
361lemma well_cost_labelled_exec_steps : ∀n,g,s,trace,s'.
362  well_cost_labelled_ge g →
363  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
364  well_cost_labelled_state s →
365  well_cost_labelled_state s'.
366#n #g elim n
367[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
368| #m #IH #s #trace #s' #WCLge #EX
369  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
370  #WCLs @(IH … WCLge … EX')
371  @(well_cost_labelled_state_step … STEP WCLge WCLs)
372] qed.
373
374lemma soundly_labelled_exec_steps : ∀n,g,s,trace,s'.
375  soundly_labelled_ge g →
376  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
377  soundly_labelled_state s →
378  soundly_labelled_state s'.
379#n #g elim n
380[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
381| #m #IH #s #trace #s' #SLge #EX
382  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
383  #SLs @(IH … SLge … EX')
384  @(soundly_labelled_state_step … SLge STEP SLs)
385] qed.
386
387lemma int_trace_split : ∀C,t1,t2,callstack,cs2,obs.
388  intensional_trace_of_trace C callstack (t1@t2) = 〈cs2,obs〉 →
389  ∃cs1,t1',t2'.
390  intensional_trace_of_trace C callstack t1 = 〈cs1,t1'〉 ∧
391  intensional_trace_of_trace C cs1 t2 = 〈cs2,t2'〉 ∧
392  obs = t1'@t2'.
393#C #t1 #t2 #cs0 #cs2 #obs >int_trace_append'
394cases (intensional_trace_of_trace C cs0 t1) #cs1 #t1'
395normalize nodelta #E %{cs1} %{t1'}
396cases (intensional_trace_of_trace C cs1 t2) in E ⊢ %; #cs2 #t2'
397normalize nodelta #E destruct
398%{t2'}
399/3/
400qed.
401
402definition cs_change : trace_ends_with_ret → ident → list ident → list ident → Prop ≝ λends,fn,cs,cs'.
403match ends with
404[ ends_with_ret ⇒ cs = cs'
405| doesnt_end_with_ret ⇒ fn::cs = cs'
406].
407
408lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'.
409  as_execute (RTLabs_status ge) s1 s2 →
410  step io_out io_in RTLabs_fullexec ge (Ras_state … s1) = Value ??? 〈tr,s2'〉 →
411  Ras_state … s2 = s2'.
412#ge #s1 #s2 #tr #s2' * #tr * #EX #NX
413change with (eval_statement ge (Ras_state … s1)) in ⊢ (??%? → ?); >EX #E destruct
414%
415qed.
416
417include alias "basics/logic.ma". (* For ∧ *)
418
419let rec eq_end_tlr ge s trace' s' tlr s'' on tlr :
420  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
421  (Ras_state … s') = s'' ≝ ?
422and eq_end_tll ge s trace' s' ends tll s'' on tll :
423  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
424  (Ras_state … s') = s'' ≝ ?
425and eq_end_tal ge s trace' s' ends tal s'' on tal :
426  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
427  (Ras_state … s') = s'' ≝ ?.
428[ cases tlr
429  [ #s1 #s2 #tll @eq_end_tll
430  | #s1 #s2 #s3 #tll #tlr' #EX
431    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1
432    <(eq_end_tll … EX1) #EX2 #E
433    @(eq_end_tlr … EX2)
434  ]
435| cases tll
436  #ends' #s1 #s2 #tal #CS
437  @eq_end_tal
438| cases tal
439  [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX'
440    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
441    whd in EX':(??%%); destruct
442    @(as_exec_eq_step … EX ST)
443  | #s1 #s2 #EX #CL #EX'
444    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
445    whd in EX':(??%%); destruct
446    @(as_exec_eq_step … EX ST)
447  | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX'
448    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
449    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
450    @(eq_end_tlr … tlr … EX')
451  | #s1 #s2 #s3 #EX #CL #tlr #EX'
452    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
453    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
454    @(eq_end_tlr … tlr … EX')
455  | #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX'
456    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
457    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
458    cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3
459    lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3
460    @(eq_end_tal … EX3)
461  | #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX'
462    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
463    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
464    @(eq_end_tal … EX')
465  ]
466] qed.
467
468definition maybe_label ≝
469λge,s,obs.
470  match as_label (RTLabs_status ge) s with
471  [ None ⇒ obs
472  | Some cl ⇒ (IEVcost cl)::obs
473  ].
474
475lemma definitely_maybe_label : ∀ge,s,CS,tl.
476  (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl.
477#ge #s #CS #tl
478whd in ⊢ (???%); whd in match (as_label_safe ??);
479>(opt_to_opt_safe … CS) in ⊢ (???%);
480%
481qed.
482
483lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'.
484  eval_statement ge s = Value ??? 〈tr,s'〉 →
485  (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨
486  (tr = [ ] ∧ RTLabs_cost_label s = None ?).
487#ge *
488[ #f #fs #m #tr #s' whd in ⊢ (??%? → ?);
489  whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?);
490  cases (next_instruction f)
491  [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % %
492  | #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % %
493  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % %
494  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
495  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
496  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
497  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct %2 % %
498  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 % %
499  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 % %
500  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % %
501  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result ?) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %2 % %
502  ]
503| #vf * #fn #args #retdst #stk #m #tr #s'
504  whd in ⊢ (??%? → ?);
505  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
506    #E destruct %2 % %
507  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % %
508  ]
509| #v #r * [2: #f #fs ] #m #tr #s'
510  whd in ⊢ (??%? → ?);
511  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % %
512  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct %2 % % | *: normalize #a try #b destruct ] ]
513  ]
514| #r #tr #s' normalize #E destruct
515] qed.
516
517lemma RTLabs_as_label : ∀ge,s.
518  RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s.
519cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
520#ge * *
521[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
522  whd in ⊢ (???%);
523  whd in match (as_pc_of ??);
524  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
525  whd in ⊢ (???%); >M1 whd in ⊢ (???%);
526  whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?);
527  >(lookup_lookup_present … nok) whd in ⊢ (??%%);
528  %
529| #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); %
530| #v #dst #fs #m * [2: #fn #stk] #mtc %
531| // #r #stk #mtc %
532] qed.
533
534 
535
536lemma step_cost_event : ∀ge,s,tr,s',obs.
537  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
538  maybe_label ge s obs = intensional_events_of_events tr@obs.
539#ge #s #tr #s' #obs #ST
540cases (only_plain_step_events_is_one_cost … ST)
541[ * #cl * #E1 #CS whd in ⊢ (??%?);
542  <RTLabs_as_label >CS destruct %
543| * #E #CS whd in ⊢ (??%?);
544  <RTLabs_as_label >CS destruct %
545] qed.
546
547lemma really_no_label : ∀ge,s,obs.
548  ¬as_costed (RTLabs_status ge) s →
549  maybe_label ge s obs = obs.
550#ge #s #obs
551whd in ⊢ (?% → ??%?);
552cases (as_label ??)
553[ //
554| #l * #H @⊥ @H % #E destruct
555] qed.
556
557
558lemma call_ret_event : ∀ge,s,tr,s',obs.
559  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
560  (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) →
561  maybe_label ge s obs = obs ∧ tr = [ ].
562#ge * *
563[ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??);
564  cases (next_instruction f) normalize
565  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
566| #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_
567  letin s ≝ (Callstate ??????)
568  cut (RTLabs_cost_label s = None ?)
569  [ 1,3: // ] #CS %
570  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
571  lapply ST
572  whd in ⊢ (??%? → ?);
573  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
574    #E destruct %
575  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
576  ]
577| #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs
578  letin s ≝ (Returnstate ????) #ST #_
579  cut (RTLabs_cost_label s = None ?)
580  [ 1,3: // ] #CS %
581  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
582  lapply ST
583  whd in ⊢ (??%? → ?);
584  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %
585  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct % | *: normalize #a try #b destruct ] ]
586  ]
587| #r #S #M #tr #s' #obs normalize #E destruct
588] qed.
589
590lemma as_call_cs_callee : ∀ge,s,CL,CL'.
591  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'.
592#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
593destruct %
594qed.
595
596lemma itot_call : ∀C,cs,s,rem,cs',trace.
597  ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
598  intensional_trace_of_trace C cs (〈s,E0〉::rem) = 〈cs',trace〉 →
599  ∃trace'.
600    trace = (IEVcall (cs_callee C s CL))::trace' ∧
601    intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉.
602#C #cs #s #rem #cs' #trace #CL
603whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
604@generalize_callee cases (cs_classify C s) in CL ⊢ %; *
605#name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem)
606#cs' #trace' #E whd in E:(??%?); destruct %{trace'} % %
607qed.
608
609lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
610  as_classifier (RTLabs_status ge) s cl_other →
611  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
612  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 →
613  ∃obs'.
614    obs = (intensional_events_of_events tr) @ obs' ∧
615    intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉.
616#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
617whd in ⊢ (??%? → ?);
618whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??);
619generalize in match (cs_callee ??) in ⊢ (% → ?);
620whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?);
621>CL #name whd in ⊢ (??%? → ?);
622cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
623%{trace''} /2/
624qed.
625
626(* observables_trace_label_label emits the cost label for the first step of the
627   enclosed tal, so we have to add that label if it exists to the front of the
628   events from the structured trace *)
629let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
630  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
631  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
632  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
633and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
634  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
635  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
636  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
637and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
638  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
639  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
640  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
641[ cases tlr
642  [ #s1 #s2 #tll @eq_obs_tll
643  | #s1 #s2 #s3 #tll #tlr #EX #ITOT
644    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E
645    >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
646    lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1
647    cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2
648    cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % %
649  ]
650| cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?);
651  whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS)
652  @(eq_obs_tal … EX ITOT)
653| cases tal
654  [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL
655    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
656    whd in EX:(??%?); destruct
657    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
658    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
659    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
660    whd in ⊢ (? → ? → ?(??(???%)?)?);
661    >CL #call whd in ⊢ (??%? → ?); #E destruct
662    % [ 1,3: @(step_cost_event … ST') | 2,4: % ]
663  | #s1 #s2 #ST #CL #EX
664    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
665    whd in EX:(??%?); destruct
666    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
667    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
668    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
669    whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct
670    cases (call_ret_event … ST')
671    [ #E1 #E2 >E1 >E2 % %
672    | skip
673    | %2 @CL
674    ]
675  | #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX
676    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
677    whd in EX:(??%?); destruct cases (call_ret_event … ST')
678    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
679    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
680    #obs' * #E3 #ITOT'
681    <(as_exec_eq_step … ST ST') in EX; #EX
682    cases (eq_obs_tlr … EX ITOT')
683    #OBS' #E4 <E4 %
684    [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) %
685    | %
686    ]
687  | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL)
688  | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX
689    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
690    cases (call_ret_event … ST')
691    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
692    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
693    #obs' * #E4 #ITOT'
694    <(as_exec_eq_step … ST ST') in EX; #EX
695    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E
696    >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
697    lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1
698    cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2
699    cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' %
700    [ >E4 whd in ⊢ (??%?);
701      <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1'
702      >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2'
703      <Eobs %
704    | @CS_CH'
705    ]
706  | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX
707    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
708    #ITOT  cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT'
709    <(as_exec_eq_step … ST ST') in EX; #EX
710    cases (eq_obs_tal … EX ITOT')
711    >(really_no_label … CS) #OBS' #CS_CH
712    >(step_cost_event … ST') <OBS'
713    % [ % | @CS_CH ]
714  ]
715] qed.
716
717
718
719
720lemma cost_state_is_in_function : ∀ge,s,S,M.
721  RTLabs_cost (mk_RTLabs_ext_state ge s S M) →
722  ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id.
723#ge *
724[ #f #fs #m * [*] #fn #S' * #FFP #M #_
725  %{fn} %{S'} %{(symbol_of_function_block' … FFP)}
726  % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ]
727| #fid #fn #args #ret #fs #m #S #M *
728| #rv #rr #fs #m #S #M *
729| #r #S #M *
730] qed.
731
732lemma cost_state_intensional_state_change : ∀ge,s,cs.
733  RTLabs_cost s →
734  \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs.
735#ge *
736[ #f #fs #m #cs //
737| #fid #fn #args #ret #fs #m #cs *
738| #rv #rr #fs #m #cs *
739| #r #cs *
740] qed.
741
742(* TODO: move to somewhere common *)
743definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
744λC,p,m.
745  let g ≝ make_global … (pcs_exec … C) p in
746  let C' ≝ pcs_to_cs C g in
747  ! s0 ← make_initial_state … p;
748  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
749  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
750
751
752(* I'm not entirely certain that existentially quantifying fn is the right thing
753   to do.  In principle we must provide the right one to satisfy the condition
754   about observables, but perhaps we ought to show how to produce it explicitly.
755   *)
756
757
758theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
759  well_cost_labelled_program p →
760  measurable RTLabs_pcsys p m n stack_cost max →
761  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
762  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
763  exec_steps_with_obs RTLabs_ext_pcsys p m = return 〈sm, prefix〉 ∧
764  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
765  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
766  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
767#p #m #n #stack_cost #max #prefix #interesting
768#WCLP cases (well_cost_labelled_make_global p WCLP)
769change with (make_global … RTLabs_fullexec p) in match (make_global p);
770#WCLge #SLge
771* #s0 * #prefix' * #s1 * #interesting' * #s2
772letin ge ≝ (make_global … RTLabs_fullexec p)
773* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #MAXSTACK
774whd in ⊢ (??%? → ?); >INIT
775whd in ⊢ (??%? → ?); >EXEC1
776whd in ⊢ (??%? → ?); >EXEC2
777whd in ⊢ (??%? → ?);
778@pair_elim #cs1 #prefix1 #ITOT1
779lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting'))
780cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %);
781#cs2 #interesting'' #ITOT2
782#E whd in E:(??%%); destruct
783cases (initial_states_OK' … INIT) #S * #M #INIT'
784cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT')
785#prefix'' * #S1 * #M1 * *
786lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
787lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
788letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #ITOT1' #CALLSTACK1
789cut (∃cs1'. cs1 = fn::cs1')
790[ >(cost_state_intensional_state_change … CS1) in CALLSTACK1;
791  cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} %
792] * #cs1' #Ecs destruct
793cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
794lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
795[ @RETURNS'
796| @CS1
797| @(well_cost_labelled_exec_steps … EXEC1)
798  [ assumption
799  | @(proj1 … (well_cost_labelled_initial … INIT WCLP))
800  ]
801| @WCLge
802| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
803>RETURNS_END #E destruct
804%{s1'} %{s2'} %{fn} %{tlr}
805% [ % [ %
806  [ whd in ⊢ (??%?);
807    change with (make_ext_initial_state p) in match (make_initial_state ????);
808    >INIT' whd in ⊢ (??%?);
809    >EXEC1' whd in ⊢ (??%?); >ITOT1' %
810  | @tlr_sound_unrepeating
811    [ @SLge
812    | @(soundly_labelled_exec_steps … EXEC1)
813      [ @SLge
814      | @(proj2 … (well_cost_labelled_initial … INIT WCLP))
815      ]
816    ]
817 ]| >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)
818 ]| cut (length_tlr … tlr = n)
819    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
820      <plus_n_O @(λx.x) ]
821    #LEN' <LEN' in EXEC2; #EXEC2
822    lapply (eq_obs_tlr ????????? EXEC2 ITOT2)
823    * //
824  ]
825] qed.
826
Note: See TracBrowser for help on using the repository browser.