source: src/RTLabs/MeasurableToStructured.ma

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

Rebuild prefix traces in back-end's preferred form.

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