source: src/RTLabs/MeasurableToStructured.ma @ 2894

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

Some progress on showing that the change to structured traces preserves
observables.

File size: 25.7 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
49definition RTLabs_ext_exec : trans_system io_out io_in ≝
50  mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement.
51
52definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
53λp.
54  let ge ≝ make_global p in
55  do m ← init_mem … (λx.[Init_space x]) p;
56  let main ≝ prog_main ?? p in
57  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
58  do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
59  let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
60  return (mk_RTLabs_ext_state (make_global p) s [b] ?).
61% [ @Ef | % ]
62qed.
63
64lemma initial_states_OK : ∀p,s.
65  make_ext_initial_state p = return s →
66  make_initial_state p = return (Ras_state … s).
67#p #s #E
68cases (bind_inversion ????? E) -E #m * #E1 #E
69cases (bind_inversion ????? E) -E #b * #E2 #E
70cases (bind_as_inversion ????? E) -E #f * #Ef #E
71whd in ⊢ (??%?); >E1
72whd in ⊢ (??%?); >E2
73whd in ⊢ (??%?); >Ef
74whd in E:(??%%) ⊢ (??%?); destruct
75%
76qed.
77
78lemma initial_states_OK' : ∀p,s.
79  make_initial_state p = return s →
80  ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M).
81#p #s #E
82cases (bind_inversion ????? E) -E #m * #E1 #E
83cases (bind_inversion ????? E) -E #b * #E2 #E
84cases (bind_inversion ????? E) -E #f * #Ef #E
85whd in E:(??%%); destruct
86%{[b]} % [ % [ @Ef | % ] ]
87whd in ⊢ (??%?); >E1
88whd in ⊢ (??%?); >E2
89whd in ⊢ (??%?); generalize in match (refl ??);
90>Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' %
91qed.
92
93
94definition RTLabs_ext_fullexec : fullexec io_out io_in ≝
95  mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state.
96
97definition RTLabs_ext_pcsys ≝ mk_preclassified_system
98  RTLabs_ext_fullexec
99  (λg,s. RTLabs_cost (Ras_state … s))
100  (λg,s. RTLabs_classify (Ras_state … s))
101  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
102
103definition lift_some : ∀A,B:Type[0]. (A → B) → A → option B ≝
104λA,B,f,a. Some B (f a).
105
106definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → nat → nat ≝
107λS,s1,s2,tlr,stack_cost,currentfn,initial.
108  maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)).
109
110(* A bit of mucking around because we're going to build a will_return in Type[0].
111   In principle we could drop the alternative form of will_return entirely, but
112   time pressures don't really allow for that. *)
113record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ {
114  cft_tr : trace;
115  cft_s  : state;
116  cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉;
117  cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉;
118  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)
119}.
120
121lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
122  ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.
123  cft ge n s hd trace s' EX.
124#ge #n #s #hd #trace #s' #EX
125lapply (refl ? (eval_statement ge s))
126cases (eval_statement ge s) in ⊢ (???% → ?);
127[ #o #k | 3: #m ]
128[ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct
129  change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
130] * #tr #s1 #EV
131@(mk_cft … tr s1 EV)
132[ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
133  change with (eval_statement ??) in ⊢ (??%? → ?);
134  >EV in ⊢ (% → ?); #E destruct #EX' @EX'
135| whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
136  >EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
137  #ST' whd in ⊢ (??%?); %
138] qed.
139
140lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
141  will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace →
142  will_return ge depth s (make_flat_trace ge n s trace s' EX).
143#ge #trace0 elim trace0
144[ #depth #n #s #s' #EX *
145| * #s1 #tr1 #tl #IH #depth #n #s #s' #EX
146  lapply (exec_steps_length … EX) #E1
147  lapply (exec_steps_first … EX) #E2
148  lapply (refl ? (eval_statement ge s))
149  cases (eval_statement ge s) in ⊢ (???% → ?);
150  [ #o #k destruct #EV @⊥
151    whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX;
152    [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????);
153      >EV #EX whd in EX:(??%%); destruct
154    | #r #EX whd in EX:(??%%); destruct
155    ]
156  | 3: #m #EV @⊥ destruct
157    whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX;
158    [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????);
159      >EV #EX whd in EX:(??%%); destruct
160    | #r #EX whd in EX:(??%%); destruct
161    ]
162  ] * #tr2 #s2 #EV >E1 in EX; #EX
163  whd in ⊢ (?% → ?);
164  lapply (refl ? (cs_classify ? s1))
165  cases (cs_classify ??) in ⊢ (???% → %);
166  #CL whd in ⊢ (?% → ?);
167  [ cases depth
168    [ whd in ⊢ (?% → ?); cases tl in EX ⊢ %;
169      [ #EX #_
170        lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
171        @wr_base
172        destruct @CL
173      | * #s3 #tr3 #tl3 #EX *
174      ]
175    | #depth' whd in ⊢ (?% → ?); #H
176      lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
177      @wr_ret
178      [ destruct @CL
179      | @IH @H
180      ]
181    ]
182  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
183    @wr_step [ %2 destruct @CL | @IH @H ]
184  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
185    @wr_call [ destruct @CL | @IH @H ]
186  | cases (RTLabs_notail … CL)
187  | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT)
188    @wr_step [ %1 destruct @CL | @IH @H ]
189  ]
190] qed.
191
192lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'.
193  eval_statement ge s = return 〈tr,s'〉 →
194  ∃S,M. eval_ext_statement ge s = return 〈tr,mk_RTLabs_ext_state … s' S M〉.
195#ge #s #tr #s' #EV
196whd in match (eval_ext_statement ??);
197letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
198cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
199[ // ]
200generalize in match f; -f
201>EV #next #NEXT whd in ⊢ (??(λ_.??(λ_.??%?)));
202lapply (NEXT … (refl ??))
203cases (next s' tr ?) #s'' #S'' #M'' #E destruct %{S''} %{M''} %
204qed.
205
206lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.
207  exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 →
208  ∃trace',S,M. exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉.
209#ge #n0 elim n0
210[ #s #trace #s' #E whd in E:(??%%); destruct %{[ ]} cases s #s' #S #M
211  %{S} %{M} %
212| #n #IH #s #trace #s' #EX
213  cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX'
214  lapply (refl ? (eval_ext_statement ge s))
215  whd in ⊢ (???% → ?);
216  change with (eval_statement ge s) in STEP:(??%?);
217  letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
218  cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
219  [ // ]
220  generalize in match f; -f
221  >STEP #next #NEXT whd in ⊢ (???% → ?); letin s1' ≝ (next s1 tr ?) #STEP'
222  <(NEXT … (refl ??)) in EX'; #EX'
223  cases (IH s1' … EX')
224  #tl' * #S'' * #M'' #STEPS''
225  %{(〈s,tr〉::tl')} %{S''} %{M''}
226  whd in ⊢ (??%?);
227  change with (RTLabs_is_final s) in match (is_final ?????);
228  change with (RTLabs_is_final s) in match (is_final ?????) in NF;
229  >NF whd in ⊢ (??%?);
230  change with (eval_ext_statement ??) in match (step ?????);
231  >STEP' whd in ⊢ (??%?);
232  >STEPS'' %
233] qed.
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_ext_fullexec ge s1 = Value ??? 〈tr,s2'〉 →
295  s2 = s2'.
296#ge #s1 #s2 #tr #s2' * #tr * #EX
297whd in ⊢ (? → ??%? → ?);
298letin f ≝ (next_state ge s1) change with (f (Ras_state … s2) tr EX) in ⊢ (??%? → ?);
299generalize in ⊢ (??(%???)? → ??(?%)? → ?); >EX in ⊢ (% → % → ??(match % with [_⇒?|_⇒?|_⇒?]?)? → ?);
300#next #NEXT whd in ⊢ (??%? → ?); #E destruct >NEXT %
301qed.
302
303include alias "basics/logic.ma". (* For ∧ *)
304
305let rec eq_end_tlr ge s trace' s' tlr s'' on tlr :
306  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
307  s' = s'' ≝ ?
308and eq_end_tll ge s trace' s' ends tll s'' on tll :
309  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
310  s' = s'' ≝ ?
311and eq_end_tal ge s trace' s' ends tal s'' on tal :
312  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s''〉 →
313  s' = s'' ≝ ?.
314[ cases tlr
315  [ #s1 #s2 #tll @eq_end_tll
316  | #s1 #s2 #s3 #tll #tlr' #EX
317    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1
318    <(eq_end_tll … EX1) #EX2 #E
319    @(eq_end_tlr … EX2)
320  ]
321| cases tll
322  #ends' #s1 #s2 #tal #CS
323  @eq_end_tal
324| cases tal
325  [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX'
326    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
327    whd in EX':(??%%); destruct
328    @(as_exec_eq_step … EX ST)
329  | #s1 #s2 #EX #CL #EX'
330    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
331    whd in EX':(??%%); destruct
332    @(as_exec_eq_step … EX ST)
333  | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX'
334    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
335    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
336    @(eq_end_tlr … tlr … EX')
337  | #s1 #s2 #s3 #EX #CL #tlr #EX'
338    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
339    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
340    @(eq_end_tlr … tlr … EX')
341  | #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX'
342    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
343    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
344    cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3
345    lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3
346    @(eq_end_tal … EX3)
347  | #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX'
348    cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX'
349    lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX'
350    @(eq_end_tal … EX')
351  ]
352] qed.
353
354definition maybe_label ≝
355λge,s,obs.
356  match as_label (RTLabs_status ge) s with
357  [ None ⇒ obs
358  | Some cl ⇒ (IEVcost cl)::obs
359  ].
360
361lemma definitely_maybe_label : ∀ge,s,CS,tl.
362  (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl.
363#ge #s #CS #tl
364whd in ⊢ (???%); whd in match (as_label_safe ??);
365>(opt_to_opt_safe … CS) in ⊢ (???%);
366%
367qed.
368
369lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'.
370  eval_statement ge s = Value ??? 〈tr,s'〉 →
371  (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨
372  (tr = [ ] ∧ RTLabs_cost_label s = None ?).
373#ge *
374[ #f #fs #m #tr #s' whd in ⊢ (??%? → ?);
375  whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?);
376  cases (next_instruction f)
377  [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % %
378  | #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % %
379  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % %
380  | #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 % %
381  | #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 % %
382  | #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 % %
383  | #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 % %
384  | #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 % %
385  | #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 % %
386  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % %
387  | #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 % %
388  ]
389| #vf * #fn #args #retdst #stk #m #tr #s'
390  whd in ⊢ (??%? → ?);
391  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
392    #E destruct %2 % %
393  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % %
394  ]
395| #v #r * [2: #f #fs ] #m #tr #s'
396  whd in ⊢ (??%? → ?);
397  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % %
398  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct %2 % % | *: normalize #a try #b destruct ] ]
399  ]
400| #r #tr #s' normalize #E destruct
401] qed.
402
403lemma drop_exec_ext : ∀ge,s,tr,s'.
404  eval_ext_statement ge s = return 〈tr,s'〉 →
405  eval_statement ge s = return 〈tr,Ras_state … s'〉.
406#ge #s #tr #s'
407whd in ⊢ (??%? → ?);
408letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)
409cut (∀s',t,EV. Ras_state … (f s' t EV) = s')
410[ // ]
411generalize in match f; -f
412cases (eval_statement ge s)
413[ #o #k #n #N #E whd in E:(??%%); destruct
414| * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //
415| #m #n #N #E whd in E:(??%%); destruct
416] qed.
417
418lemma RTLabs_as_label : ∀ge,s.
419  RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s.
420cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE
421#ge * *
422[ * #func #locals #next #nok #sp #r #fs #m #stk #mtc
423  whd in ⊢ (???%);
424  whd in match (as_pc_of ??);
425  cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2
426  whd in ⊢ (???%); >M1 whd in ⊢ (???%);
427  whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?);
428  >(lookup_lookup_present … nok) whd in ⊢ (??%%);
429  %
430| #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); %
431| #v #dst #fs #m * [2: #fn #stk] #mtc %
432| // #r #stk #mtc %
433] qed.
434
435 
436
437lemma step_cost_event : ∀ge,s,tr,s',obs.
438  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
439  maybe_label ge s obs = intensional_events_of_events tr@obs.
440#ge #s #tr #s' #obs #ST
441cases (only_plain_step_events_is_one_cost … (drop_exec_ext … ST))
442[ * #cl * #E1 #CS whd in ⊢ (??%?);
443  <RTLabs_as_label >CS destruct %
444| * #E #CS whd in ⊢ (??%?);
445  <RTLabs_as_label >CS destruct %
446] qed.
447
448lemma call_ret_event : ∀ge,s,tr,s',obs.
449  step … RTLabs_ext_fullexec ge s = Value ??? 〈tr,s'〉 →
450  (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) →
451  maybe_label ge s obs = obs ∧ tr = [ ].
452#ge * *
453[ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??);
454  cases (next_instruction f) normalize
455  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
456| #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_
457  letin s ≝ (Callstate ??????)
458  cut (RTLabs_cost_label s = None ?)
459  [ 1,3: // ] #CS %
460  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
461  lapply (drop_exec_ext … ST)
462  whd in ⊢ (??%? → ?);
463  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
464    #E destruct %
465  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
466  ]
467| #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs
468  letin s ≝ (Returnstate ????) #ST #_
469  cut (RTLabs_cost_label s = None ?)
470  [ 1,3: // ] #CS %
471  [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ]
472  lapply (drop_exec_ext … ST)
473  whd in ⊢ (??%? → ?);
474  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %
475  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct % | *: normalize #a try #b destruct ] ]
476  ]
477| #r #S #M #tr #s' #obs normalize #E destruct
478] qed.
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 ⊢ (??%? → ?);
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
493(* WIP
494lemma as_call_cs_callee : ∀ge,s,CL,CL'.
495  as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ext_pcsys ge) s CL'.
496#ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E
497destruct cases S in M CL' ⊢ %; [ * ] #fn' #S' * #M1 #M' #CL'
498whd in ⊢ (??%%); cases (symbol_for_block ??)
499
500
501(* observables_trace_label_label emits the cost label for the first step of the
502   enclosed tal, so we have to add that label if it exists to the front of the
503   events from the structured trace *)
504let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr :
505  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace',s'〉 →
506  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →
507  pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
508and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
509  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
510  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
511  pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
512and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
513  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ext_fullexec ge s = OK ? 〈trace1,s'〉 →
514  intensional_trace_of_trace (pcs_to_cs RTLabs_ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →
515  maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
516[ cases tlr
517  [ #s1 #s2 #tll @eq_obs_tll
518  | #s1 #s2 #s3 #tll #tlr #EX #ITOT
519    cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E
520    >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs
521    lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1
522    cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2
523    cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % %
524  ]
525| cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?);
526  whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS)
527  @(eq_obs_tal … EX ITOT)
528| cases tal
529  [ #s1 #s2 #ST * #CL #CS #EX
530    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
531    whd in EX:(??%?); destruct
532    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
533    whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
534    whd in ⊢ (? → ? → ?(??(???%)?)?);
535    >CL #call whd in ⊢ (??%? → ?); #E destruct
536    % [ 1,3: @(step_cost_event … ST') | 2,4: % ]
537  | #s1 #s2 #ST #CL #EX
538    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
539    whd in EX:(??%?); destruct
540    whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?);
541    whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?);
542    whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct
543    cases (call_ret_event … ST')
544    [ #E1 #E2 >E1 >E2 % %
545    | skip
546    | %2 @CL
547    ]
548  | #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX
549    cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX
550    whd in EX:(??%?); destruct cases (call_ret_event … ST')
551    [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT
552    cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ? = ?) in CL; >CL % ]
553    #obs' * #E3 #ITOT'
554    <(as_exec_eq_step … ST ST') in EX; #EX
555    cases (eq_obs_tlr … EX ITOT')
556    #OBS' #E4 <E4 %
557    [ >E3 <OBS' whd in ⊢ (??%?);
558
559   
560   
561
562] qed.
563*)
564
565
566
567(* I'm not entirely certain that existentially quantifying fn is the right thing
568   to do.  In principle we must provide the right one to satisfy the condition
569   about observables, but perhaps we ought to show how to produce it explicitly.
570   *)
571
572
573theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting.
574  well_cost_labelled_program p →
575  measurable RTLabs_pcsys p m n stack_cost max →
576  observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 →
577  let midstack ≝ \fst (measure_stack stack_cost 0 prefix) in
578  ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn.
579  state_at RTLabs_ext_pcsys p m = return sm ∧
580  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
581  le (max_stack_of_tlr ??? tlr (lift_some … stack_cost) fn midstack) max ∧
582  pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
583#p #m #n #stack_cost #max #prefix #interesting
584#WCLP cases (well_cost_labelled_make_global p WCLP)
585change with (make_global … RTLabs_fullexec p) in match (make_global p);
586#WCLge #SLge
587* #s0 * #prefix' * #s1 * #interesting' * #s2
588letin ge ≝ (make_global … RTLabs_fullexec p)
589* * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK
590whd in ⊢ (??%? → ?); >INIT
591whd in ⊢ (??%? → ?); >EXEC1
592whd in ⊢ (??%? → ?); >EXEC2
593whd in ⊢ (??%? → ?); @breakup_pair #E whd in E:(??%%); destruct
594cases (initial_states_OK' … INIT) #S * #M #INIT'
595cases (extend_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)
596#prefix'' * #S1 * #M1 letin s1' ≝ (mk_RTLabs_ext_state ? s1 S1 M1) #EXEC1'
597lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????)
598[ @will_return_equiv assumption
599| @(label_to_return_state_labelled … LABEL_TO_RETURN EXEC2)
600| @(well_cost_labelled_exec_steps … EXEC1)
601  [ assumption
602  | @(proj1 … (well_cost_labelled_initial … INIT WCLP))
603  ]
604| @WCLge
605| * #s2' #rem #_ #tlr #LEN #STACK #_
606%{s1'} %{s2'} % [2: %{tlr}
607% [ % [ %
608  [ whd in ⊢ (??%?);
609    change with (make_ext_initial_state p) in match (make_initial_state ????);
610    >INIT' whd in ⊢ (??%?);
611    >EXEC1' %
612  | @tlr_sound_unrepeating
613    [ @SLge
614    | @(soundly_labelled_exec_steps … EXEC1)
615      [ @SLge
616      | @(proj2 … (well_cost_labelled_initial … INIT WCLP))
617      ]
618    ]
619 ]|
620 ]|
621  ]
622]]
623
624
Note: See TracBrowser for help on using the repository browser.