source: src/common/Measurable.ma

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

Use single definition for stack measurement.

File size: 15.2 KB
Line 
1include "common/Executions.ma".
2include "common/stacksize.ma".
3
4(* A small-step executable semantics, together with some kind of global
5   environment, notion of cost labelled state, classification function and
6   stack costs. *)
7
8record classified_system : Type[2] ≝ {
9  cs_exec :> fullexec io_out io_in;
10  cs_global : global … cs_exec;
11  cs_labelled : state … cs_exec cs_global → bool;
12  cs_classify : state … cs_exec cs_global → status_class;
13  cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True | _ ⇒ False ] → ident
14}.
15
16definition cs_state : classified_system → Type[0] ≝
17λC. state … C (cs_global … C).
18
19(* Ideally we would also allow measurable traces to be from one cost label to
20   another (in the same function call), but due to time constraints we'll stick
21   to ending measurable traces at the end of the function only.
22 *)
23
24definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
25λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
26
27(* Construction of the trace of intensional events.
28
29   It might be possible to merge these with the plain events, but for now we
30   combine those with call/return information taken from the states.
31   
32   The build_* results help with the proof that measurable subtraces are
33   preserved in the front-end. *)
34
35definition intensional_event_of_event : event → list intensional_event ≝
36λev. match ev with
37[ EVcost l ⇒ [ IEVcost l ]
38| EVextcall _ _ _ ⇒ [ ]  (* No equivalent, but there shouldn't be any for now *)
39].
40
41definition intensional_events_of_events : trace → list intensional_event ≝
42λtr. flatten ? (map ?? intensional_event_of_event tr).
43
44definition intensional_state_change ≝
45λC,callstack,s.
46    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
47    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
48    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
49    | _ ⇒ λ_. 〈callstack, [ ]〉
50    ] (cs_callee C s).
51
52let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
53match trace with
54[ nil ⇒ 〈callstack, [ ]〉
55| cons str tl ⇒
56  let 〈s,tr〉 ≝ str in
57  let 〈callstack, call_event〉 ≝ intensional_state_change C callstack s in
58  let other_events ≝ intensional_events_of_events tr in
59  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
60    〈callstack, call_event@other_events@rem〉
61].
62
63definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
64λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
65
66lemma normal_state_inv : ∀C,s.
67  normal_state C s →
68  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
69#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
70qed.
71
72lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
73  normal_state C s →
74  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
75    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
76      〈stk', (intensional_events_of_events tr)@tl〉).
77#C #callstack #s #tr #trace #NORMAL
78whd in ⊢ (??%?); whd in match (intensional_state_change ???);
79generalize in match (cs_callee C s);
80cases (normal_state_inv … NORMAL)
81#CL >CL normalize nodelta #_
82cases (intensional_trace_of_trace C callstack trace)
83#callstack' #tl normalize nodelta
84%
85qed.
86
87
88lemma int_events_append : ∀tr1,tr2.
89  intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2).
90#tr1 #tr2
91change with (flatten ??) in ⊢ (??%(??%%));
92<map_append >flatten_append %
93qed.
94
95
96lemma int_trace_irr : ∀C,callstack,s,trace.
97  normal_state C s →
98  intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace.
99#C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL)
100cases (intensional_trace_of_trace ???) //
101qed.
102
103lemma int_trace_append : ∀C,callstack,s,t1,t2,trace.
104  normal_state C s →
105  intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace).
106#C #callstack #s #t1 #t2 #trace #NORMAL
107>(int_trace_of_normal … NORMAL)
108>(int_trace_of_normal … NORMAL)
109>(int_trace_of_normal … NORMAL)
110cases (intensional_trace_of_trace ???) #callstack' #trace'
111normalize nodelta
112>int_events_append
113>associative_append %
114qed.
115
116lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'.
117  normal_state C s →
118  all … (λstr. normal_state C' (\fst str)) trace →
119  intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' →
120  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
121#C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL'
122>(int_trace_of_normal … NORMAL)
123cases (intensional_trace_of_trace C callstack rem) #callstack' #trace'
124#REM whd in ⊢ (??%?);
125elim trace in NORMAL' ⊢ %;
126[ #_ @REM
127| * #s' #tr' #tl #IH #NORMAL'
128  cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl
129  >int_trace_of_normal
130  [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%);
131    >int_events_append >associative_append %
132  | @NORMALs
133  ]
134] qed.
135
136lemma int_trace_append' : ∀C,t1,t2,callstack.
137  intensional_trace_of_trace C callstack (t1@t2) =
138    (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in
139     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in
140     〈cs'', t1'@t2'〉).
141#C #t1 #t2 elim t1
142[ #callstack whd in match ([ ]@t2); whd in ⊢ (???%);
143  cases (intensional_trace_of_trace ???) #cs' #trace' %
144| * #s #tr #tl #IH
145  #callstack
146  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
147  whd in match (intensional_trace_of_trace ???); whd in match (intensional_state_change ???);
148  generalize in match (cs_callee C s);
149  cases (cs_classify C s)
150  normalize nodelta #callee
151  [ cases callstack [2: #cshd #cdtl] normalize nodelta ]
152  >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl'
153  normalize nodelta
154  cases (intensional_trace_of_trace C ? t2) #cs'' #tl''
155  normalize nodelta >associative_append >associative_append
156  %
157] qed.
158
159lemma int_trace_normal_cs : ∀C,callstack,trace.
160  all ? (λstr. normal_state C (\fst str)) trace →
161  callstack = \fst (intensional_trace_of_trace C callstack trace).
162#C #callstack #trace elim trace
163[ //
164| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
165  >(int_trace_of_normal … N1)
166  >(IH Ntl) in ⊢ (??%?);
167  cases (intensional_trace_of_trace ???) /2/
168] qed.
169
170lemma int_trace_append_normal : ∀C,t1,t2,callstack.
171  all ? (λstr. normal_state C (\fst str)) t1 →
172  intensional_trace_of_trace C callstack (t1@t2) =
173    (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in
174     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in
175     〈cs'', t1'@t2'〉).
176#C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack)
177lapply (int_trace_normal_cs C callstack t1 NORMAL)
178cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct //
179qed.
180
181lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'.
182  cs_classify C s = cl_return →
183  cs_classify C' s' = cl_return →
184  all ? (λstr. normal_state C' (\fst str)) trace' →
185  intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' →
186  let trace ≝ 〈s',tr〉::trace' in
187  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
188#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
189whd
190whd in ⊢ (??%%);
191whd in match (intensional_state_change ???);
192whd in match (intensional_state_change C' ??);
193normalize nodelta
194generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
195>CL >CL' normalize nodelta #_ #_
196cases callstack in E ⊢ %; [2: #stkhd #stktl]
197normalize nodelta
198cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta
199>(int_trace_append_normal … NORMAL) normalize nodelta
200cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
201destruct @eq_f @eq_f
202whd in match (gather_trace ??); >int_events_append
203>associative_append @eq_f
204elim trace in NORMAL ⊢ %;
205[ 1,3: #_ %
206| 2,4:
207  * #s1 #tr1 #tl #IH
208  #N cases (andb_Prop_true … N) #N1 #Ntl
209  whd in match (gather_trace ??); >int_events_append
210  >associative_append >(IH Ntl)
211  >(int_trace_of_normal … N1)
212  cases (intensional_trace_of_trace ?? tl)
213  #cs' #tl' >associative_append %
214] qed.
215
216(* I had a little trouble doing this directly. *)
217lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
218  (∀f. P f (f H)) →
219  P (cs_callee C s) (cs_callee C s H).
220#C #s #H #P #f @f
221qed.
222
223lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
224  all ? (λstr. normal_state C' (\fst str)) trace' →
225  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
226  cs_callee C s H = cs_callee C' s' H' →
227  let trace ≝ 〈s',tr〉::trace' in
228  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
229#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
230whd in ⊢ (? → ? → %);
231whd in ⊢ (? → ? → ??%%);
232whd in match (intensional_state_change ???);
233whd in match (intensional_state_change C' ??);
234normalize nodelta
235@generalize_callee
236@generalize_callee
237cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
238normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
239cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
240>(int_trace_append_normal … NORMAL) normalize nodelta
241cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
242destruct @eq_f @eq_f
243whd in match (gather_trace ??); >int_events_append
244>associative_append @eq_f
245elim trace in NORMAL ⊢ %;
246[ 1,3: #_ %
247| 2,4:
248  * #s1 #tr1 #tl #IH
249  #N cases (andb_Prop_true … N) #N1 #Ntl
250  whd in match (gather_trace ??); >int_events_append
251  >associative_append >(IH Ntl)
252  >(int_trace_of_normal … N1)
253  cases (intensional_trace_of_trace ?? tl)
254  #cs' #tl' >associative_append %
255] qed.
256
257(* Measuring stack usage.  The intensional_event to cost part is handled by a
258   common function with the structured traces version in common/stacksize.ma. *) 
259
260definition measure_stack : (ident → option nat) → stacksize_info → list intensional_event → stacksize_info ≝
261λcosts,start,ev.
262  update_stacksize_info costs start (extract_call_ud_from_observables ev).
263
264
265(* Check that the trace ends with the return from the starting function and one
266   further state. *)
267
268let rec will_return_aux C (depth:nat)
269                        (trace:list (cs_state … C × trace)) on trace : bool ≝
270match trace with
271[ nil ⇒ false
272| cons h tl ⇒
273  let 〈s,tr〉 ≝ h in
274  match cs_classify C s with
275  [ cl_call ⇒ will_return_aux C (S depth) tl
276  | cl_return ⇒
277      match depth with
278       (* The state after the return will appear in the structured trace, but
279          not here because it is the second part of the pair returned by
280          exec_steps. *)
281      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
282      | S d ⇒ will_return_aux C d tl
283      ]
284  | _ ⇒ will_return_aux C depth tl
285  ]
286].
287definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
288
289(* Like classified_system, but we don't fix the global environment so that we
290   talk about the program separately. *)
291
292record preclassified_system : Type[2] ≝ {
293  pcs_exec :> fullexec io_out io_in;
294  pcs_labelled : ∀g. state … pcs_exec g → bool;
295  pcs_classify : ∀g. state … pcs_exec g → status_class;
296  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
297}.
298
299definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
300λC,g.
301  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
302
303
304
305definition measurable : ∀C:preclassified_system.
306  ∀p:program ?? C. nat → nat →
307  (ident → option nat) (* stack cost *) →
308  nat → Prop ≝
309λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
310  let g ≝ make_global … (pcs_exec … C) p in
311  let C' ≝ pcs_to_cs C g in
312  make_initial_state … p = OK ? s0 ∧
313  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
314  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
315  trace_is_label_to_return C' interesting ∧
316  bool_to_Prop (will_return' C' interesting) ∧
317  le (maximum (measure_stack stack_cost (mk_stacksize_info 0 0) (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting))))) max_allowed_stack.
318
319
320
321definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
322λC,p,m,n.
323  let g ≝ make_global … (pcs_exec … C) p in
324  let C' ≝ pcs_to_cs C g in
325  ! s0 ← make_initial_state … p;
326  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
327  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
328  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
329  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
330
331(* CSC: Main debug function for the extracted code.
332   It returns the list of all observed states and their observables,
333   the last state and the reason for stopping execution. If the last
334   state is final, it also returns the exit value. *)
335let rec observe_all_in_measurable (n:nat) (fx:classified_system)
336 (observe: intensional_event → unit) (callstack: list ident)
337 (s:state … fx (cs_global fx)) :
338 list intensional_event × (res int) ≝
339match n with
340[ O ⇒
341  let res ≝
342   match is_final … fx (cs_global … fx) s with
343   [ Some r ⇒ OK … r
344   | None ⇒ Error … (msg NotTerminated) ]
345  in
346   〈[ ],res〉
347| S m ⇒
348  match is_final … fx (cs_global … fx) s with
349  [ Some r ⇒ 〈[ ],OK … r〉
350  | None ⇒
351    match step … fx (cs_global … fx) s with
352    [ Value trs ⇒
353        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
354        let 〈callstack,callevent〉 ≝
355         match cs_classify fx s
356         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
357                 list ident × (list intensional_event)
358         with
359         [ cl_call ⇒
360            λcallee. let id ≝ callee I in
361            〈id::callstack,[IEVcall id]〉
362         | cl_return ⇒ λ_.
363            match callstack with
364            [ nil ⇒ 〈[ ],[ ]〉
365            | cons id tl ⇒ 〈tl,[IEVret id]〉]
366         | _ ⇒ λ_. 〈callstack, [ ]〉
367         ] (cs_callee fx s) in
368        let events ≝ costevents@callevent in
369        let dummy : list unit ≝ map ?? observe events in
370        let 〈tl,res〉 ≝
371         observe_all_in_measurable m fx observe callstack (\snd trs) in
372         〈events@tl,res〉
373    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
374    | Wrong m ⇒ 〈[ ],Error … m〉
375    ]
376  ]
377].
Note: See TracBrowser for help on using the repository browser.