source: src/RTLabs/MeasurableToStructured.ma @ 2896

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

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

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