source: src/common/Measurable.ma @ 2896

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

Complete part of measurable to structured subtraces proof that
shows observables are preserved.

File size: 17.7 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
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.  TODO: I think there's another version of this from
258   the back-end that should be merged. *) 
259
260definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
261λcosts,start.
262  foldl ?? (λx. λev.
263    match ev with
264    [ IEVcall id ⇒
265        let 〈current_stack,max_stack〉 ≝ x in
266        let new_stack ≝ current_stack + costs id in
267        〈new_stack, max new_stack max_stack〉
268    | IEVret id ⇒
269        let 〈current_stack,max_stack〉 ≝ x in
270        〈current_stack - costs id, max_stack〉
271    | _ ⇒ x
272    ]) 〈start,start〉.
273
274definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
275λcosts, start, trace. \snd (measure_stack costs start trace).
276
277lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
278  (∀acc,el. P acc → P (f acc el)) →
279  ∀l,acc. P acc →
280  P (foldl A B f acc l).
281#A #B #P #f #IH #l elim l
282[ //
283| #h #t #IH' #acc #H @IH' @IH @H
284] qed.
285(*
286lemma max_stack_step : ∀C,a,m,a',m',tr,s.
287  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
288  m' = max m a'.
289#C #a #m #a' #m' #tr #s
290whd in match (measure_stack_aux ???);
291generalize in match (cs_stack C s); cases (cs_classify C s) #f
292normalize nodelta #E destruct //
293qed.
294
295lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
296  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
297  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
298  a1' = a2'.
299#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
300whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
301generalize in match (cs_stack C s); cases (cs_classify C s) #f
302normalize nodelta
303#E1 #E2 destruct
304%
305qed.
306
307
308lemma max_stack_steps : ∀C,trace,a,m.
309  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
310  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
311#C #trace elim trace
312[ #a #m >max_n_O %
313| * #tr #s #tl #IH #a #m
314  whd in match (foldl ?????);
315  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
316  whd in match (foldl ??? 〈a,O〉 ?);
317  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
318  >(IH a'') >IH
319  >(max_stack_step … M)
320  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
321] qed.
322
323lemma max_stack_append : ∀C,c1,ex1,ex2.
324  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
325#C #c1 #ex1 #ex2
326whd in match (max_stack ???); whd in match (stack_after ???);
327whd in match (max_stack ?? (ex1@ex2));
328whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
329generalize in match O; generalize in match c1; elim ex1
330[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
331| * #tr #s #tl #IH #c #m
332  whd in match (foldl ?????); whd in ⊢ (???(???%));
333  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
334  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
335  >IH %
336] qed.
337*) 
338
339(* Check that the trace ends with the return from the starting function and one
340   further state. *)
341
342let rec will_return_aux C (depth:nat)
343                        (trace:list (cs_state … C × trace)) on trace : bool ≝
344match trace with
345[ nil ⇒ false
346| cons h tl ⇒
347  let 〈s,tr〉 ≝ h in
348  match cs_classify C s with
349  [ cl_call ⇒ will_return_aux C (S depth) tl
350  | cl_return ⇒
351      match depth with
352       (* The state after the return will appear in the structured trace, but
353          not here because it is the second part of the pair returned by
354          exec_steps. *)
355      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
356      | S d ⇒ will_return_aux C d tl
357      ]
358  | _ ⇒ will_return_aux C depth tl
359  ]
360].
361definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
362
363(* Like classified_system, but we don't fix the global environment so that we
364   talk about the program separately. *)
365
366record preclassified_system : Type[2] ≝ {
367  pcs_exec :> fullexec io_out io_in;
368  pcs_labelled : ∀g. state … pcs_exec g → bool;
369  pcs_classify : ∀g. state … pcs_exec g → status_class;
370  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
371}.
372
373definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
374λC,g.
375  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
376
377
378
379definition measurable : ∀C:preclassified_system.
380  ∀p:program ?? C. nat → nat →
381  (ident → nat) (* stack cost *) →
382  nat → Prop ≝
383λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
384  let g ≝ make_global … (pcs_exec … C) p in
385  let C' ≝ pcs_to_cs C g in
386  make_initial_state … p = OK ? s0 ∧
387  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
388  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
389  trace_is_label_to_return C' interesting ∧
390  bool_to_Prop (will_return' C' interesting) ∧
391  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
392
393
394
395definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
396λC,p,m,n.
397  let g ≝ make_global … (pcs_exec … C) p in
398  let C' ≝ pcs_to_cs C g in
399  ! s0 ← make_initial_state … p;
400  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
401  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
402  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
403  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
404
405(* CSC: Main debug function for the extracted code.
406   It returns the list of all observed states and their observables,
407   the last state and the reason for stopping execution. If the last
408   state is final, it also returns the exit value. *)
409let rec observe_all_in_measurable (n:nat) (fx:classified_system)
410 (observe: intensional_event → unit) (callstack: list ident)
411 (s:state … fx (cs_global fx)) :
412 list intensional_event × (res int) ≝
413match n with
414[ O ⇒
415  let res ≝
416   match is_final … fx (cs_global … fx) s with
417   [ Some r ⇒ OK … r
418   | None ⇒ Error … (msg NotTerminated) ]
419  in
420   〈[ ],res〉
421| S m ⇒
422  match is_final … fx (cs_global … fx) s with
423  [ Some r ⇒ 〈[ ],OK … r〉
424  | None ⇒
425    match step … fx (cs_global … fx) s with
426    [ Value trs ⇒
427        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
428        let 〈callstack,callevent〉 ≝
429         match cs_classify fx s
430         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
431                 list ident × (list intensional_event)
432         with
433         [ cl_call ⇒
434            λcallee. let id ≝ callee I in
435            〈id::callstack,[IEVcall id]〉
436         | cl_return ⇒ λ_.
437            match callstack with
438            [ nil ⇒ 〈[ ],[ ]〉
439            | cons id tl ⇒ 〈tl,[IEVret id]〉]
440         | _ ⇒ λ_. 〈callstack, [ ]〉
441         ] (cs_callee fx s) in
442        let events ≝ costevents@callevent in
443        let dummy : list unit ≝ map ?? observe events in
444        let 〈tl,res〉 ≝
445         observe_all_in_measurable m fx observe callstack (\snd trs) in
446         〈events@tl,res〉
447    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
448    | Wrong m ⇒ 〈[ ],Error … m〉
449    ]
450  ]
451].
Note: See TracBrowser for help on using the repository browser.