source: src/common/Measurable.ma @ 2800

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

Tidy up Measurable.ma a little, get rid of obsolete comments.

File size: 17.3 KB
Line 
1include "common/Executions.ma".
2include "common/StructuredTraces.ma".  (* just for status_class *)
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
44let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
45match trace with
46[ nil ⇒ 〈callstack, [ ]〉
47| cons str tl ⇒
48  let 〈s,tr〉 ≝ str in
49  let 〈callstack, call_event〉 ≝
50    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
51    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
52    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
53    | _ ⇒ λ_. 〈callstack, [ ]〉
54    ] (cs_callee C s) in
55  let other_events ≝ intensional_events_of_events tr in
56  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
57    〈callstack, call_event@other_events@rem〉
58].
59
60definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
61λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
62
63lemma normal_state_inv : ∀C,s.
64  normal_state C s →
65  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
66#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
67qed.
68
69lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
70  normal_state C s →
71  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
72    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
73      〈stk', (intensional_events_of_events tr)@tl〉).
74#C #callstack #s #tr #trace #NORMAL
75whd in ⊢ (??%?);
76generalize in match (cs_callee C s);
77cases (normal_state_inv … NORMAL)
78#CL >CL normalize nodelta #_
79cases (intensional_trace_of_trace C callstack trace)
80#callstack' #tl normalize nodelta
81%
82qed.
83
84
85lemma int_events_append : ∀tr1,tr2.
86  intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2).
87#tr1 #tr2
88change with (flatten ??) in ⊢ (??%(??%%));
89<map_append >flatten_append %
90qed.
91
92
93lemma int_trace_irr : ∀C,callstack,s,trace.
94  normal_state C s →
95  intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace.
96#C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL)
97cases (intensional_trace_of_trace ???) //
98qed.
99
100lemma int_trace_append : ∀C,callstack,s,t1,t2,trace.
101  normal_state C s →
102  intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace).
103#C #callstack #s #t1 #t2 #trace #NORMAL
104>(int_trace_of_normal … NORMAL)
105>(int_trace_of_normal … NORMAL)
106>(int_trace_of_normal … NORMAL)
107cases (intensional_trace_of_trace ???) #callstack' #trace'
108normalize nodelta
109>int_events_append
110>associative_append %
111qed.
112
113lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'.
114  normal_state C s →
115  all … (λstr. normal_state C' (\fst str)) trace →
116  intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' →
117  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
118#C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL'
119>(int_trace_of_normal … NORMAL)
120cases (intensional_trace_of_trace C callstack rem) #callstack' #trace'
121#REM whd in ⊢ (??%?);
122elim trace in NORMAL' ⊢ %;
123[ #_ @REM
124| * #s' #tr' #tl #IH #NORMAL'
125  cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl
126  >int_trace_of_normal
127  [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%);
128    >int_events_append >associative_append %
129  | @NORMALs
130  ]
131] qed.
132
133lemma int_trace_append' : ∀C,t1,t2,callstack.
134  intensional_trace_of_trace C callstack (t1@t2) =
135    (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in
136     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in
137     〈cs'', t1'@t2'〉).
138#C #t1 #t2 elim t1
139[ #callstack whd in match ([ ]@t2); whd in ⊢ (???%);
140  cases (intensional_trace_of_trace ???) #cs' #trace' %
141| * #s #tr #tl #IH
142  #callstack
143  whd in match (intensional_trace_of_trace ???);
144  whd in match (intensional_trace_of_trace ???);
145  generalize in match (cs_callee C s);
146  cases (cs_classify C s)
147  normalize nodelta #callee
148  [ cases callstack [2: #cshd #cdtl] normalize nodelta ]
149  >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl'
150  normalize nodelta
151  cases (intensional_trace_of_trace C ? t2) #cs'' #tl''
152  normalize nodelta >associative_append >associative_append
153  %
154] qed.
155
156lemma int_trace_normal_cs : ∀C,callstack,trace.
157  all ? (λstr. normal_state C (\fst str)) trace →
158  callstack = \fst (intensional_trace_of_trace C callstack trace).
159#C #callstack #trace elim trace
160[ //
161| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
162  >(int_trace_of_normal … N1)
163  >(IH Ntl) in ⊢ (??%?);
164  cases (intensional_trace_of_trace ???) /2/
165] qed.
166
167lemma int_trace_append_normal : ∀C,t1,t2,callstack.
168  all ? (λstr. normal_state C (\fst str)) t1 →
169  intensional_trace_of_trace C callstack (t1@t2) =
170    (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in
171     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in
172     〈cs'', t1'@t2'〉).
173#C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack)
174lapply (int_trace_normal_cs C callstack t1 NORMAL)
175cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct //
176qed.
177
178lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'.
179  cs_classify C s = cl_return →
180  cs_classify C' s' = cl_return →
181  all ? (λstr. normal_state C' (\fst str)) trace' →
182  intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' →
183  let trace ≝ 〈s',tr〉::trace' in
184  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
185#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
186whd
187whd in ⊢ (??%%); normalize nodelta
188generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
189>CL >CL' normalize nodelta #_ #_
190cases callstack in E ⊢ %; [2: #stkhd #stktl]
191normalize nodelta
192cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta
193>(int_trace_append_normal … NORMAL) normalize nodelta
194cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
195destruct @eq_f @eq_f
196whd in match (gather_trace ??); >int_events_append
197>associative_append @eq_f
198elim trace in NORMAL ⊢ %;
199[ 1,3: #_ %
200| 2,4:
201  * #s1 #tr1 #tl #IH
202  #N cases (andb_Prop_true … N) #N1 #Ntl
203  whd in match (gather_trace ??); >int_events_append
204  >associative_append >(IH Ntl)
205  >(int_trace_of_normal … N1)
206  cases (intensional_trace_of_trace ?? tl)
207  #cs' #tl' >associative_append %
208] qed.
209
210(* I had a little trouble doing this directly. *)
211lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
212  (∀f. P f (f H)) →
213  P (cs_callee C s) (cs_callee C s H).
214#C #s #H #P #f @f
215qed.
216
217lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
218  all ? (λstr. normal_state C' (\fst str)) trace' →
219  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
220  cs_callee C s H = cs_callee C' s' H' →
221  let trace ≝ 〈s',tr〉::trace' in
222  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
223#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
224whd in ⊢ (? → ? → %);
225whd in ⊢ (? → ? → ??%%); normalize nodelta
226@generalize_callee
227@generalize_callee
228cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
229normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
230cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
231>(int_trace_append_normal … NORMAL) normalize nodelta
232cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
233destruct @eq_f @eq_f
234whd in match (gather_trace ??); >int_events_append
235>associative_append @eq_f
236elim trace in NORMAL ⊢ %;
237[ 1,3: #_ %
238| 2,4:
239  * #s1 #tr1 #tl #IH
240  #N cases (andb_Prop_true … N) #N1 #Ntl
241  whd in match (gather_trace ??); >int_events_append
242  >associative_append >(IH Ntl)
243  >(int_trace_of_normal … N1)
244  cases (intensional_trace_of_trace ?? tl)
245  #cs' #tl' >associative_append %
246] qed.
247
248(* Measuring stack usage.  TODO: I think there's another version of this from
249   the back-end that should be merged. *) 
250
251definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
252λcosts,start.
253  foldl ?? (λx. λev.
254    match ev with
255    [ IEVcall id ⇒
256        let 〈current_stack,max_stack〉 ≝ x in
257        let new_stack ≝ current_stack + costs id in
258        〈new_stack, max new_stack max_stack〉
259    | IEVret id ⇒
260        let 〈current_stack,max_stack〉 ≝ x in
261        〈current_stack - costs id, max_stack〉
262    | _ ⇒ x
263    ]) 〈start,start〉.
264
265definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
266λcosts, start, trace. \snd (measure_stack costs start trace).
267
268lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
269  (∀acc,el. P acc → P (f acc el)) →
270  ∀l,acc. P acc →
271  P (foldl A B f acc l).
272#A #B #P #f #IH #l elim l
273[ //
274| #h #t #IH' #acc #H @IH' @IH @H
275] qed.
276(*
277lemma max_stack_step : ∀C,a,m,a',m',tr,s.
278  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
279  m' = max m a'.
280#C #a #m #a' #m' #tr #s
281whd in match (measure_stack_aux ???);
282generalize in match (cs_stack C s); cases (cs_classify C s) #f
283normalize nodelta #E destruct //
284qed.
285
286lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
287  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
288  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
289  a1' = a2'.
290#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
291whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
292generalize in match (cs_stack C s); cases (cs_classify C s) #f
293normalize nodelta
294#E1 #E2 destruct
295%
296qed.
297
298
299lemma max_stack_steps : ∀C,trace,a,m.
300  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
301  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
302#C #trace elim trace
303[ #a #m >max_n_O %
304| * #tr #s #tl #IH #a #m
305  whd in match (foldl ?????);
306  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
307  whd in match (foldl ??? 〈a,O〉 ?);
308  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
309  >(IH a'') >IH
310  >(max_stack_step … M)
311  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
312] qed.
313
314lemma max_stack_append : ∀C,c1,ex1,ex2.
315  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
316#C #c1 #ex1 #ex2
317whd in match (max_stack ???); whd in match (stack_after ???);
318whd in match (max_stack ?? (ex1@ex2));
319whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
320generalize in match O; generalize in match c1; elim ex1
321[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
322| * #tr #s #tl #IH #c #m
323  whd in match (foldl ?????); whd in ⊢ (???(???%));
324  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
325  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
326  >IH %
327] qed.
328*) 
329
330(* Check that the trace ends with the return from the starting function and one
331   further state. *)
332
333let rec will_return_aux C (depth:nat)
334                        (trace:list (cs_state … C × trace)) on trace : bool ≝
335match trace with
336[ nil ⇒ false
337| cons h tl ⇒
338  let 〈s,tr〉 ≝ h in
339  match cs_classify C s with
340  [ cl_call ⇒ will_return_aux C (S depth) tl
341  | cl_return ⇒
342      match depth with
343       (* The state after the return will appear in the structured trace, but
344          not here because it is the second part of the pair returned by
345          exec_steps. *)
346      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
347      | S d ⇒ will_return_aux C d tl
348      ]
349  | _ ⇒ will_return_aux C depth tl
350  ]
351].
352definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
353
354(* Like classified_system, but we don't fix the global environment so that we
355   talk about the program separately. *)
356
357record preclassified_system : Type[2] ≝ {
358  pcs_exec :> fullexec io_out io_in;
359  pcs_labelled : ∀g. state … pcs_exec g → bool;
360  pcs_classify : ∀g. state … pcs_exec g → status_class;
361  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
362}.
363
364definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
365λC,g.
366  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
367
368
369
370definition measurable : ∀C:preclassified_system.
371  ∀p:program ?? C. nat → nat →
372  (ident → nat) (* stack cost *) →
373  nat → Prop ≝
374λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
375  let g ≝ make_global … (pcs_exec … C) p in
376  let C' ≝ pcs_to_cs C g in
377  make_initial_state … p = OK ? s0 ∧
378  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
379  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
380  trace_is_label_to_return C' interesting ∧
381  bool_to_Prop (will_return' C' interesting) ∧
382  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
383
384
385
386definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
387λC,p,m,n.
388  let g ≝ make_global … (pcs_exec … C) p in
389  let C' ≝ pcs_to_cs C g in
390  ! s0 ← make_initial_state … p;
391  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
392  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
393  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
394  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
395
396(* CSC: Main debug function for the extracted code.
397   It returns the list of all observed states and their observables,
398   the last state and the reason for stopping execution. If the last
399   state is final, it also returns the exit value. *)
400let rec observe_all_in_measurable (n:nat) (fx:classified_system)
401 (observe: intensional_event → unit) (callstack: list ident)
402 (s:state … fx (cs_global fx)) :
403 list intensional_event × (res int) ≝
404match n with
405[ O ⇒
406  let res ≝
407   match is_final … fx (cs_global … fx) s with
408   [ Some r ⇒ OK … r
409   | None ⇒ Error … (msg NotTerminated) ]
410  in
411   〈[ ],res〉
412| S m ⇒
413  match is_final … fx (cs_global … fx) s with
414  [ Some r ⇒ 〈[ ],OK … r〉
415  | None ⇒
416    match step … fx (cs_global … fx) s with
417    [ Value trs ⇒
418        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
419        let 〈callstack,callevent〉 ≝
420         match cs_classify fx s
421         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
422                 list ident × (list intensional_event)
423         with
424         [ cl_call ⇒
425            λcallee. let id ≝ callee I in
426            〈id::callstack,[IEVcall id]〉
427         | cl_return ⇒ λ_.
428            match callstack with
429            [ nil ⇒ 〈[ ],[ ]〉
430            | cons id tl ⇒ 〈tl,[IEVret id]〉]
431         | _ ⇒ λ_. 〈callstack, [ ]〉
432         ] (cs_callee fx s) in
433        let events ≝ costevents@callevent in
434        let dummy : list unit ≝ map ?? observe events in
435        let 〈tl,res〉 ≝
436         observe_all_in_measurable m fx observe callstack (\snd trs) in
437         〈events@tl,res〉
438    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
439    | Wrong m ⇒ 〈[ ],Error … m〉
440    ]
441  ]
442].
Note: See TracBrowser for help on using the repository browser.