source: src/common/Measurable.ma @ 2783

Last change on this file since 2783 was 2756, checked in by sacerdot, 7 years ago

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File size: 15.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
27definition intensional_event_of_event : event → list intensional_event ≝
28λev. match ev with
29[ EVcost l ⇒ [ IEVcost l ]
30| EVextcall _ _ _ ⇒ [ ]  (* No equivalent, but there shouldn't be any for now *)
31].
32
33definition intensional_events_of_events : trace → list intensional_event ≝
34λtr. flatten ? (map ?? intensional_event_of_event tr).
35
36let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
37match trace with
38[ nil ⇒ 〈callstack, [ ]〉
39| cons str tl ⇒
40  let 〈s,tr〉 ≝ str in
41  let 〈callstack, call_event〉 ≝
42    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
43    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
44    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
45    | _ ⇒ λ_. 〈callstack, [ ]〉
46    ] (cs_callee C s) in
47  let other_events ≝ intensional_events_of_events tr in
48  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
49    〈callstack, call_event@other_events@rem〉
50].
51
52definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
53λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
54
55lemma normal_state_inv : ∀C,s.
56  normal_state C s →
57  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
58#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
59qed.
60
61lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
62  normal_state C s →
63  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
64    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
65      〈stk', (intensional_events_of_events tr)@tl〉).
66#C #callstack #s #tr #trace #NORMAL
67whd in ⊢ (??%?);
68generalize in match (cs_callee C s);
69cases (normal_state_inv … NORMAL)
70#CL >CL normalize nodelta #_
71cases (intensional_trace_of_trace C callstack trace)
72#callstack' #tl normalize nodelta
73%
74qed.
75
76lemma flatten_append : ∀A,l1,l2.
77  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
78#A #l1 #l2
79elim l1
80[ %
81| #h #t #IH whd in ⊢ (??%(??%?));
82  change with (flatten ??) in match (foldr ?????); >IH
83  change with (flatten ??) in match (foldr ?????);
84  >associative_append %
85] qed.
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 ???);
147  whd in match (intensional_trace_of_trace ???);
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 ⊢ (??%%); normalize nodelta
191generalize in match (cs_callee C s); generalize in match (cs_callee C' s');
192>CL >CL' normalize nodelta #_ #_
193cases callstack in E ⊢ %; [2: #stkhd #stktl]
194normalize nodelta
195cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta
196>(int_trace_append_normal … NORMAL) normalize nodelta
197cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
198destruct @eq_f @eq_f
199whd in match (gather_trace ??); >int_events_append
200>associative_append @eq_f
201elim trace in NORMAL ⊢ %;
202[ 1,3: #_ %
203| 2,4:
204  * #s1 #tr1 #tl #IH
205  #N cases (andb_Prop_true … N) #N1 #Ntl
206  whd in match (gather_trace ??); >int_events_append
207  >associative_append >(IH Ntl)
208  >(int_trace_of_normal … N1)
209  cases (intensional_trace_of_trace ?? tl)
210  #cs' #tl' >associative_append %
211] qed.
212
213lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
214  (∀f. P f (f H)) →
215  P (cs_callee C s) (cs_callee C s H).
216#C #s #H #P #f @f
217qed.
218
219lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
220  all ? (λstr. normal_state C' (\fst str)) trace' →
221  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
222  cs_callee C s H = cs_callee C' s' H' →
223  let trace ≝ 〈s',tr〉::trace' in
224  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
225#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
226whd in ⊢ (? → ? → %);
227whd in ⊢ (? → ? → ??%%); normalize nodelta
228@generalize_callee
229@generalize_callee
230cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
231normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
232cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
233>(int_trace_append_normal … NORMAL) normalize nodelta
234cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
235destruct @eq_f @eq_f
236whd in match (gather_trace ??); >int_events_append
237>associative_append @eq_f
238elim trace in NORMAL ⊢ %;
239[ 1,3: #_ %
240| 2,4:
241  * #s1 #tr1 #tl #IH
242  #N cases (andb_Prop_true … N) #N1 #Ntl
243  whd in match (gather_trace ??); >int_events_append
244  >associative_append >(IH Ntl)
245  >(int_trace_of_normal … N1)
246  cases (intensional_trace_of_trace ?? tl)
247  #cs' #tl' >associative_append %
248] qed.
249 
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(* FIXME: this definition is unreasonable because it presumes we can easily
369   identify the change in stack usage from return states, but that information
370   is rather implicit (we only really record the function called in the
371   extended RTLabs states when building the structured traces). *)
372
373definition measurable : ∀C:preclassified_system.
374  ∀p:program ?? C. nat → nat →
375  (ident → nat) (* stack cost *) →
376  nat → Prop ≝
377λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
378  let g ≝ make_global … (pcs_exec … C) p in
379  let C' ≝ pcs_to_cs C g in
380  make_initial_state … p = OK ? s0 ∧
381  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
382  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
383  trace_is_label_to_return C' interesting ∧
384  bool_to_Prop (will_return' C' interesting) ∧
385  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
386
387(* TODO: probably ought to be elsewhere; use exec_steps instead
388
389   Note that this does not include stack space
390 *)
391
392definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
393λC,p,m,n.
394  let g ≝ make_global … (pcs_exec … C) p in
395  let C' ≝ pcs_to_cs C g in
396  ! s0 ← make_initial_state … p;
397  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
398  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
399  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
400  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
401
Note: See TracBrowser for help on using the repository browser.