source: src/RTLabs/MeasurableToStructured.ma @ 2897

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

Minor tidying.

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