source: src/RTLabs/MeasurableToStructured.ma @ 2895

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

Match up function id from RTLabs Callstate with shadow stack,
use in observables proof.

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