source: src/RTLabs/MeasurableToStructured.ma @ 2947

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

Init change in measurable to structured file.

File size: 33.4 KB
RevLine 
[2839]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
[2896]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
[2839]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
[2947]84  do m ← init_mem … (λx.x) p;
[2839]85  let main ≝ prog_main ?? p in
[2895]86  do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
[2839]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] ?).
[2895]90% [ % assumption | % ]
[2839]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
[2895]98cases (bind_as_inversion ????? E) -E #b * #Eb #E
[2839]99cases (bind_as_inversion ????? E) -E #f * #Ef #E
100whd in ⊢ (??%?); >E1
[2895]101whd in ⊢ (??%?); >Eb
[2839]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
[2895]112cases (bind_inversion ????? E) -E #b * #Eb #E
[2839]113cases (bind_inversion ????? E) -E #f * #Ef #E
114whd in E:(??%%); destruct
[2895]115%{[b]} % [ % [ % assumption | % ] ]
[2839]116whd in ⊢ (??%?); >E1
117whd in ⊢ (??%?); generalize in match (refl ??);
[2895]118>Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb'
119whd in ⊢ (??%?); generalize in match (refl ??);
[2839]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 →
[2895]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? *)
[2839]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)
[2895]166        %{(wr_base …)}
167        [ destruct @CL
168        | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?);
169          whd in cEX:(??%%); destruct %
170        ]
[2839]171      | * #s3 #tr3 #tl3 #EX *
172      ]
173    | #depth' whd in ⊢ (?% → ?); #H
174      lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
[2895]175      cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
176      %{(wr_ret …)}
177      [ @WR'
178      | destruct @CL
179      | @WRe
[2839]180      ]
181    ]
182  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
[2895]183    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
184    %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ]
[2839]185  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
[2895]186    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
187    %{(wr_call …)} [ @WR' | destruct @CL | @WRe ]
[2839]188  | cases (RTLabs_notail … CL)
189  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
[2895]190    cases (IH ???? (cft_EX … CFT) H) #WR' #WRe
191    %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ]
[2839]192  ]
193] qed.
194
[2895]195
[2894]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
[2896]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   
283   
284lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace.
[2839]285  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
[2896]286  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 →
287  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))) →
288  ∃trace',S,M.
289    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
290    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
[2839]291#ge #n0 elim n0
[2896]292[ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct
293  #E whd in E:(??%%); destruct
294  #CS %{[ ]}
295  %{S} %{M} % [ % | @CS ]
296| #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX
[2839]297  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
[2896]298  >E whd in ⊢ (??%? → ?); @pair_elim #cs1 #itrace1 #ITOT1
299  whd in ⊢ (??%? → ?); @pair_elim #cs2 #itrace2 #ITOT2 #E' destruct
300  #STACK
301  cases (extend_RTLabs_step ge (mk_RTLabs_ext_state ge s S M) ??? STEP STACK)
302  #S' * #M' * #STEP' #STACK'
303  cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK')
304  #tl' * #S'' * #M'' * #EX'' #STACK''
305  %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''}
306  %
307  [ whd in ⊢ (??%?);
308    change with (RTLabs_is_final s) in match (is_final ?????);
309    change with (RTLabs_is_final s) in match (is_final ?????) in NF;
310    >NF whd in ⊢ (??%?);
311    change with (eval_ext_statement ??) in match (step ?????);
312    >STEP' whd in ⊢ (??%?);
313    >EX'' %
314  | @STACK''
315  ]
[2839]316] qed.
[2892]317
[2896]318lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace.
319  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
320  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 →
321  make_ext_initial_state p = OK ? s →
322  ∃trace',S,M.
323    exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧
324    All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')).
325#p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT
326@(extend_RTLabs_exec_steps … EXEC ITOT)
327cases (bind_inversion ????? INIT) -INIT #m * #E1 #INIT
328cases (bind_as_inversion ????? INIT) -INIT #b * #Eb #INIT
329cases (bind_as_inversion ????? INIT) -INIT #f * #Ef #INIT
330whd in INIT:(??%%); lapply (Ras_fn_match … s) destruct
331* * #FS #FFP #_
332% [ >(symbol_for_block_fn … FS FFP) % | % ]
333qed.
334
[2892]335lemma label_to_return_state_labelled : ∀C,n,s,trace,s'.
336  trace_is_label_to_return C trace →
337  exec_steps n ?? C ? s = OK ? 〈trace,s'〉 →
338  cs_labelled C s.
339#C #n #s #trace #s'
340* #tr * #s1 * #trace' * #tr' * #s2 * * #E #CS #_ destruct
341#EX >(exec_steps_first … EX)
342@CS
343qed.
344
345lemma well_cost_labelled_exec_steps : ∀n,g,s,trace,s'.
346  well_cost_labelled_ge g →
347  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
348  well_cost_labelled_state s →
349  well_cost_labelled_state s'.
350#n #g elim n
351[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
352| #m #IH #s #trace #s' #WCLge #EX
353  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
354  #WCLs @(IH … WCLge … EX')
355  @(well_cost_labelled_state_step … STEP WCLge WCLs)
356] qed.
[2893]357
358lemma soundly_labelled_exec_steps : ∀n,g,s,trace,s'.
359  soundly_labelled_ge g →
360  exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 →
361  soundly_labelled_state s →
362  soundly_labelled_state s'.
363#n #g elim n
364[ #s #trace #s' #_ #E whd in E:(??%%); destruct //
365| #m #IH #s #trace #s' #SLge #EX
366  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
367  #SLs @(IH … SLge … EX')
368  @(soundly_labelled_state_step … SLge STEP SLs)
369] qed.
370
[2894]371lemma int_trace_split : ∀C,t1,t2,callstack,cs2,obs.
372  intensional_trace_of_trace C callstack (t1@t2) = 〈cs2,obs〉 →
373  ∃cs1,t1',t2'.
374  intensional_trace_of_trace C callstack t1 = 〈cs1,t1'〉 ∧
375  intensional_trace_of_trace C cs1 t2 = 〈cs2,t2'〉 ∧
376  obs = t1'@t2'.
377#C #t1 #t2 #cs0 #cs2 #obs >int_trace_append'
378cases (intensional_trace_of_trace C cs0 t1) #cs1 #t1'
379normalize nodelta #E %{cs1} %{t1'}
380cases (intensional_trace_of_trace C cs1 t2) in E ⊢ %; #cs2 #t2'
381normalize nodelta #E destruct
382%{t2'}
383/3/
384qed.
385
386definition cs_change : trace_ends_with_ret → ident → list ident → list ident → Prop ≝ λends,fn,cs,cs'.
387match ends with
388[ ends_with_ret ⇒ cs = cs'
389| doesnt_end_with_ret ⇒ fn::cs = cs'
390].
391
392lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'.
393  as_execute (RTLabs_status ge) s1 s2 →
[2896]394  step io_out io_in RTLabs_fullexec ge (Ras_state … s1) = Value ??? 〈tr,s2'〉 →
395  Ras_state … s2 = s2'.
396#ge #s1 #s2 #tr #s2' * #tr * #EX #NX
397change with (eval_statement ge (Ras_state … s1)) in ⊢ (??%? → ?); >EX #E destruct
398%
[2894]399qed.
400
401include alias "basics/logic.ma". (* For ∧ *)
402
403let rec eq_end_tlr ge s trace' s' tlr s'' on tlr :
[2896]404  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
405  (Ras_state … s') = s'' ≝ ?
[2894]406and eq_end_tll ge s trace' s' ends tll s'' on tll :
[2896]407  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
408  (Ras_state … s') = s'' ≝ ?
[2894]409and eq_end_tal ge s trace' s' ends tal s'' on tal :
[2896]410  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 →
411  (Ras_state … s') = s'' ≝ ?.
[2894]412[ cases tlr
413  [ #s1 #s2 #tll @eq_end_tll
414  | #s1 #s2 #s3 #tll #tlr' #EX
415    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1
416    <(eq_end_tll … EX1) #EX2 #E
417    @(eq_end_tlr … EX2)
418  ]
419| cases tll
420  #ends' #s1 #s2 #tal #CS
421  @eq_end_tal
422| cases tal
423  [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX'
424    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
425    whd in EX':(??%%); destruct
426    @(as_exec_eq_step … EX ST)
427  | #s1 #s2 #EX #CL #EX'
428    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
429    whd in EX':(??%%); destruct
430    @(as_exec_eq_step … EX ST)
431  | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX'
432    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
433    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
434    @(eq_end_tlr … tlr … EX')
435  | #s1 #s2 #s3 #EX #CL #tlr #EX'
436    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
437    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
438    @(eq_end_tlr … tlr … EX')
439  | #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX'
440    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
441    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
442    cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3
443    lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3
444    @(eq_end_tal … EX3)
445  | #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX'
446    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
447    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
448    @(eq_end_tal … EX')
449  ]
450] qed.
451
452definition maybe_label ≝
453λge,s,obs.
454  match as_label (RTLabs_status ge) s with
455  [ None ⇒ obs
456  | Some cl ⇒ (IEVcost cl)::obs
457  ].
458
459lemma definitely_maybe_label : ∀ge,s,CS,tl.
460  (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl.
461#ge #s #CS #tl
462whd in ⊢ (???%); whd in match (as_label_safe ??);
463>(opt_to_opt_safe … CS) in ⊢ (???%);
464%
465qed.
466
467lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'.
468  eval_statement ge s = Value ??? 〈tr,s'〉 →
469  (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨
470  (tr = [ ] ∧ RTLabs_cost_label s = None ?).
471#ge *
472[ #f #fs #m #tr #s' whd in ⊢ (??%? → ?);
473  whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?);
474  cases (next_instruction f)
475  [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % %
476  | #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % %
477  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % %
478  | #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 % %
479  | #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 % %
480  | #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 % %
481  | #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 % %
482  | #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 % %
483  | #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 % %
484  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % %
485  | #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 % %
486  ]
487| #vf * #fn #args #retdst #stk #m #tr #s'
488  whd in ⊢ (??%? → ?);
489  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
490    #E destruct %2 % %
491  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % %
492  ]
493| #v #r * [2: #f #fs ] #m #tr #s'
494  whd in ⊢ (??%? → ?);
495  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % %
496  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct %2 % % | *: normalize #a try #b destruct ] ]
497  ]
498| #r #tr #s' normalize #E destruct
499] qed.
500
501lemma RTLabs_as_label : ∀ge,s.
502  RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s.
503cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
504#ge * *
505[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
506  whd in ⊢ (???%);
507  whd in match (as_pc_of ??);
508  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
509  whd in ⊢ (???%); >M1 whd in ⊢ (???%);
510  whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?);
511  >(lookup_lookup_present … nok) whd in ⊢ (??%%);
512  %
513| #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); %
514| #v #dst #fs #m * [2: #fn #stk] #mtc %
515| // #r #stk #mtc %
516] qed.
517
[2839]518 
519
[2894]520lemma step_cost_event : ∀ge,s,tr,s',obs.
[2896]521  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
[2894]522  maybe_label ge s obs = intensional_events_of_events tr@obs.
523#ge #s #tr #s' #obs #ST
[2896]524cases (only_plain_step_events_is_one_cost … ST)
[2894]525[ * #cl * #E1 #CS whd in ⊢ (??%?);
526  <RTLabs_as_label >CS destruct %
527| * #E #CS whd in ⊢ (??%?);
528  <RTLabs_as_label >CS destruct %
529] qed.
530
[2895]531lemma really_no_label : ∀ge,s,obs.
532  ¬as_costed (RTLabs_status ge) s →
533  maybe_label ge s obs = obs.
534#ge #s #obs
535whd in ⊢ (?% → ??%?);
536cases (as_label ??)
537[ //
538| #l * #H @⊥ @H % #E destruct
539] qed.
540
541
[2894]542lemma call_ret_event : ∀ge,s,tr,s',obs.
[2896]543  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
[2894]544  (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) →
545  maybe_label ge s obs = obs ∧ tr = [ ].
546#ge * *
547[ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??);
548  cases (next_instruction f) normalize
549  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
550| #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_
551  letin s ≝ (Callstate ??????)
552  cut (RTLabs_cost_label s = None ?)
553  [ 1,3: // ] #CS %
554  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
[2896]555  lapply ST
[2894]556  whd in ⊢ (??%? → ?);
557  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
558    #E destruct %
559  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
560  ]
561| #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs
562  letin s ≝ (Returnstate ????) #ST #_
563  cut (RTLabs_cost_label s = None ?)
564  [ 1,3: // ] #CS %
565  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
[2896]566  lapply ST
[2894]567  whd in ⊢ (??%? → ?);
568  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %
569  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct % | *: normalize #a try #b destruct ] ]
570  ]
571| #r #S #M #tr #s' #obs normalize #E destruct
572] qed.
573
[2895]574lemma as_call_cs_callee : ∀ge,s,CL,CL'.
[2896]575  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'.
[2895]576#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
577destruct %
578qed.
579
[2894]580lemma itot_call : ∀C,cs,s,rem,cs',trace.
581  ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ].
582  intensional_trace_of_trace C cs (〈s,E0〉::rem) = 〈cs',trace〉 →
583  ∃trace'.
584    trace = (IEVcall (cs_callee C s CL))::trace' ∧
585    intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉.
586#C #cs #s #rem #cs' #trace #CL
[2896]587whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
[2894]588@generalize_callee cases (cs_classify C s) in CL ⊢ %; *
589#name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem)
590#cs' #trace' #E whd in E:(??%?); destruct %{trace'} % %
591qed.
592
[2895]593lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs.
594  as_classifier (RTLabs_status ge) s cl_other →
[2896]595  step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 →
596  intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 →
[2895]597  ∃obs'.
598    obs = (intensional_events_of_events tr) @ obs' ∧
[2896]599    intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉.
[2895]600#ge #cs #s #tr #s' #rem #cs #obs #CL #EX
[2896]601whd in ⊢ (??%? → ?);
602whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??);
603generalize in match (cs_callee ??) in ⊢ (% → ?);
604whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?);
[2895]605>CL #name whd in ⊢ (??%? → ?);
606cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct
607%{trace''} /2/
608qed.
[2894]609
610(* observables_trace_label_label emits the cost label for the first step of the
611   enclosed tal, so we have to add that label if it exists to the front of the
612   events from the structured trace *)
613let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
[2896]614  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
615  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
[2894]616  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
617and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
[2896]618  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
619  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
[2894]620  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
621and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
[2896]622  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
623  intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
[2894]624  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
625[ cases tlr
626  [ #s1 #s2 #tll @eq_obs_tll
627  | #s1 #s2 #s3 #tll #tlr #EX #ITOT
628    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E
629    >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
630    lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1
631    cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2
632    cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % %
633  ]
634| cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?);
635  whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS)
636  @(eq_obs_tal … EX ITOT)
637| cases tal
[2895]638  [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL
[2894]639    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
640    whd in EX:(??%?); destruct
[2896]641    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
642    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
643    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
[2894]644    whd in ⊢ (? → ? → ?(??(???%)?)?);
645    >CL #call whd in ⊢ (??%? → ?); #E destruct
646    % [ 1,3: @(step_cost_event … ST') | 2,4: % ]
647  | #s1 #s2 #ST #CL #EX
648    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
649    whd in EX:(??%?); destruct
[2896]650    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?);
651    whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???);
652    generalize in match (cs_callee ??) in ⊢ (??%? → ?);
[2894]653    whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct
654    cases (call_ret_event … ST')
655    [ #E1 #E2 >E1 >E2 % %
656    | skip
657    | %2 @CL
658    ]
659  | #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX
660    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
661    whd in EX:(??%?); destruct cases (call_ret_event … ST')
662    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
[2896]663    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
[2894]664    #obs' * #E3 #ITOT'
665    <(as_exec_eq_step … ST ST') in EX; #EX
666    cases (eq_obs_tlr … EX ITOT')
667    #OBS' #E4 <E4 %
[2895]668    [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) %
669    | %
670    ]
671  | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL)
672  | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX
673    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
674    cases (call_ret_event … ST')
675    [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT
[2896]676    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ]
[2895]677    #obs' * #E4 #ITOT'
678    <(as_exec_eq_step … ST ST') in EX; #EX
679    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E
680    >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
681    lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1
682    cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2
683    cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' %
684    [ >E4 whd in ⊢ (??%?);
685      <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1'
686      >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2'
687      <Eobs %
688    | @CS_CH'
689    ]
690  | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX
691    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX
692    #ITOT  cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT'
693    <(as_exec_eq_step … ST ST') in EX; #EX
694    cases (eq_obs_tal … EX ITOT')
695    >(really_no_label … CS) #OBS' #CS_CH
696    >(step_cost_event … ST') <OBS'
697    % [ % | @CS_CH ]
698  ]
699] qed.
[2894]700
701
702
703
[2895]704lemma cost_state_is_in_function : ∀ge,s,S,M.
705  RTLabs_cost (mk_RTLabs_ext_state ge s S M) →
706  ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id.
707#ge *
708[ #f #fs #m * [*] #fn #S' * #FFP #M #_
709  %{fn} %{S'} %{(symbol_of_function_block' … FFP)}
710  % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ]
711| #fid #fn #args #ret #fs #m #S #M *
712| #rv #rr #fs #m #S #M *
713| #r #S #M *
714] qed.
[2894]715
[2896]716lemma cost_state_intensional_state_change : ∀ge,s,cs.
717  RTLabs_cost s →
718  \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs.
719#ge *
720[ #f #fs #m #cs //
721| #fid #fn #args #ret #fs #m #cs *
722| #rv #rr #fs #m #cs *
723| #r #cs *
724] qed.
[2895]725
[2914]726definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → stacksize_info → stacksize_info ≝
727λS,s1,s2,tlr,stack_cost,currentfn,initial.
728  update_stacksize_info stack_cost initial (extract_call_ud_from_tlr S s1 s2 tlr currentfn).
[2896]729
730
[2914]731
[2839]732(* I'm not entirely certain that existentially quantifying fn is the right thing
733   to do.  In principle we must provide the right one to satisfy the condition
734   about observables, but perhaps we ought to show how to produce it explicitly.
735   *)
736
737
738theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
[2892]739  well_cost_labelled_program p →
[2839]740  measurable RTLabs_pcsys p m n stack_cost max →
741  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
[2914]742  let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in
[2839]743  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
744  state_at RTLabs_ext_pcsys p m = return sm ∧
[2893]745  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
[2914]746  le (maximum (max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧
[2839]747  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
748#p #m #n #stack_cost #max #prefix #interesting
[2892]749#WCLP cases (well_cost_labelled_make_global p WCLP)
[2839]750change with (make_global … RTLabs_fullexec p) in match (make_global p);
[2892]751#WCLge #SLge
[2839]752* #s0 * #prefix' * #s1 * #interesting' * #s2
753letin ge ≝ (make_global … RTLabs_fullexec p)
754* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK
755whd in ⊢ (??%? → ?); >INIT
756whd in ⊢ (??%? → ?); >EXEC1
757whd in ⊢ (??%? → ?); >EXEC2
[2896]758whd in ⊢ (??%? → ?);
759@pair_elim #cs1 #prefix1 #ITOT1
760lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting'))
761cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %);
762#cs2 #interesting'' #ITOT2
763#E whd in E:(??%%); destruct
[2839]764cases (initial_states_OK' … INIT) #S * #M #INIT'
[2896]765cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT')
766#prefix'' * #S1 * #M1 *
[2895]767lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
768lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
[2896]769letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #CALLSTACK1
770cut (∃cs1'. cs1 = fn::cs1')
771[ >(cost_state_intensional_state_change … CS1) in CALLSTACK1;
772  cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} %
773] * #cs1' #Ecs destruct
[2895]774cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
[2839]775lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
[2895]776[ @RETURNS'
777| @CS1
[2892]778| @(well_cost_labelled_exec_steps … EXEC1)
779  [ assumption
780  | @(proj1 … (well_cost_labelled_initial … INIT WCLP))
781  ]
782| @WCLge
[2895]783| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
784>RETURNS_END #E destruct
785%{s1'} %{s2'} %{fn} %{tlr}
[2893]786% [ % [ %
[2839]787  [ whd in ⊢ (??%?);
788    change with (make_ext_initial_state p) in match (make_initial_state ????);
789    >INIT' whd in ⊢ (??%?);
790    >EXEC1' %
[2893]791  | @tlr_sound_unrepeating
792    [ @SLge
793    | @(soundly_labelled_exec_steps … EXEC1)
794      [ @SLge
795      | @(proj2 … (well_cost_labelled_initial … INIT WCLP))
796      ]
797    ]
[2839]798 ]|
[2895]799 ]| cut (length_tlr … tlr = n)
800    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
801      <plus_n_O @(λx.x) ]
802    #LEN' <LEN' in EXEC2; #EXEC2
[2896]803    lapply (eq_obs_tlr ????????? EXEC2 ITOT2)
804    * //
[2839]805  ]
[2897]806]
[2839]807
Note: See TracBrowser for help on using the repository browser.