source: src/RTLabs/MeasurableToStructured.ma @ 3096

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

Tidy up RTLabs preclassified_system definitions.

File size: 30.5 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  pi1 … (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  pi1 … (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 (pi1 … (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(* TODO: move to somewhere common *)
627definition exec_steps_with_obs : ∀C:preclassified_system. ∀p:program ?? C. nat → res ((state … C (make_global … C p)) × (list intensional_event)) ≝
628λC,p,m.
629  let g ≝ make_global … (pcs_exec … C) p in
630  let C' ≝ pcs_to_cs C g in
631  ! s0 ← make_initial_state … p;
632  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
633  return 〈s1, \snd (intensional_trace_of_trace C' [ ] prefix)〉.
634
635
636(* I'm not entirely certain that existentially quantifying fn is the right thing
637   to do.  In principle we must provide the right one to satisfy the condition
638   about observables, but perhaps we ought to show how to produce it explicitly.
639   *)
640
641
642theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
643  well_cost_labelled_program p →
644  measurable RTLabs_pcs p m n stack_cost max →
645  observables RTLabs_pcs p m n = return 〈prefix,interesting〉 →
646  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
647  exec_steps_with_obs RTLabs_ext_pcs p m = return 〈sm, prefix〉 ∧
648  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
649  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
650  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
651#p #m #n #stack_cost #max #prefix #interesting
652#WCLP cases (well_cost_labelled_make_global p WCLP)
653change with (make_global … RTLabs_fullexec p) in match (make_global p);
654#WCLge #SLge
655* #s0 * #prefix' * #s1 * #interesting' * #s2
656letin ge ≝ (make_global … RTLabs_fullexec p)
657* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #MAXSTACK
658whd in ⊢ (??%? → ?); >INIT
659whd in ⊢ (??%? → ?); >EXEC1
660whd in ⊢ (??%? → ?); >EXEC2
661whd in ⊢ (??%? → ?);
662@pair_elim #cs1 #prefix1 #ITOT1
663lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting'))
664cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ?) cs1 interesting') in ⊢ (???% → %);
665#cs2 #interesting'' #ITOT2
666#E whd in E:(??%%); destruct
667cases (initial_states_OK' … INIT) #S * #M #INIT'
668cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT')
669#prefix'' * #S1 * #M1 * *
670lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1
671lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct
672letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #ITOT1' #CALLSTACK1
673cut (∃cs1'. cs1 = fn::cs1')
674[ >(cost_state_intensional_state_change … CS1) in CALLSTACK1;
675  cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} %
676] * #cs1' #Ecs destruct
677cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END
678lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
679[ @RETURNS'
680| @CS1
681| @(well_cost_labelled_exec_steps … EXEC1)
682  [ assumption
683  | @(proj1 … (well_cost_labelled_initial … INIT WCLP))
684  ]
685| @WCLge
686| * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?);
687>RETURNS_END #E destruct
688%{s1'} %{s2'} %{fn} %{tlr}
689% [ % [ %
690  [ whd in ⊢ (??%?);
691    change with (make_ext_initial_state p) in match (make_initial_state ????);
692    >INIT' whd in ⊢ (??%?);
693    >EXEC1' whd in ⊢ (??%?); >ITOT1' %
694  | @tlr_sound_unrepeating
695    [ @SLge
696    | @(soundly_labelled_exec_steps … EXEC1)
697      [ @SLge
698      | @(proj2 … (well_cost_labelled_initial … INIT WCLP))
699      ]
700    ]
701 ]| >int_trace_append' in MAXSTACK; >ITOT1 normalize nodelta >ITOT2 @(λx.x)
702 ]| cut (length_tlr … tlr = n)
703    [ lapply (make_flat_trace_length ????? EXEC2) <LEN
704      <plus_n_O @(λx.x) ]
705    #LEN' <LEN' in EXEC2; #EXEC2
706    lapply (eq_obs_tlr ????????? EXEC2 ITOT2)
707    * //
708  ]
709] qed.
710
Note: See TracBrowser for help on using the repository browser.