source: src/common/Measurable.ma @ 2755

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

Remove a couple of redundant hypotheses.

File size: 15.8 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(* For intensional_event; should separate out definition *)
28include "common/StatusSimulation.ma".
29
30definition intensional_event_of_event : event → list intensional_event ≝
31λev. match ev with
32[ EVcost l ⇒ [ IEVcost l ]
33| EVextcall _ _ _ ⇒ [ ]  (* No equivalent, but there shouldn't be any for now *)
34].
35
36definition intensional_events_of_events : trace → list intensional_event ≝
37λtr. flatten ? (map ?? intensional_event_of_event tr).
38
39let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝
40match trace with
41[ nil ⇒ 〈callstack, [ ]〉
42| cons str tl ⇒
43  let 〈s,tr〉 ≝ str in
44  let 〈callstack, call_event〉 ≝
45    match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with
46    [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉
47    | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ]
48    | _ ⇒ λ_. 〈callstack, [ ]〉
49    ] (cs_callee C s) in
50  let other_events ≝ intensional_events_of_events tr in
51  let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in
52    〈callstack, call_event@other_events@rem〉
53].
54
55definition normal_state : ∀C:classified_system. cs_state … C → bool ≝
56λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ].
57
58lemma normal_state_inv : ∀C,s.
59  normal_state C s →
60  cs_classify C s = cl_other ∨ cs_classify C s = cl_jump.
61#C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ *
62qed.
63
64lemma int_trace_of_normal : ∀C,callstack,s,tr,trace.
65  normal_state C s →
66  intensional_trace_of_trace C callstack (〈s,tr〉::trace) =
67    (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in
68      〈stk', (intensional_events_of_events tr)@tl〉).
69#C #callstack #s #tr #trace #NORMAL
70whd in ⊢ (??%?);
71generalize in match (cs_callee C s);
72cases (normal_state_inv … NORMAL)
73#CL >CL normalize nodelta #_
74cases (intensional_trace_of_trace C callstack trace)
75#callstack' #tl normalize nodelta
76%
77qed.
78
79lemma flatten_append : ∀A,l1,l2.
80  flatten A (l1@l2) = (flatten A l1)@(flatten A l2).
81#A #l1 #l2
82elim l1
83[ %
84| #h #t #IH whd in ⊢ (??%(??%?));
85  change with (flatten ??) in match (foldr ?????); >IH
86  change with (flatten ??) in match (foldr ?????);
87  >associative_append %
88] qed.
89
90
91lemma int_events_append : ∀tr1,tr2.
92  intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2).
93#tr1 #tr2
94change with (flatten ??) in ⊢ (??%(??%%));
95<map_append >flatten_append %
96qed.
97
98
99lemma int_trace_irr : ∀C,callstack,s,trace.
100  normal_state C s →
101  intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace.
102#C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL)
103cases (intensional_trace_of_trace ???) //
104qed.
105
106lemma int_trace_append : ∀C,callstack,s,t1,t2,trace.
107  normal_state C s →
108  intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace).
109#C #callstack #s #t1 #t2 #trace #NORMAL
110>(int_trace_of_normal … NORMAL)
111>(int_trace_of_normal … NORMAL)
112>(int_trace_of_normal … NORMAL)
113cases (intensional_trace_of_trace ???) #callstack' #trace'
114normalize nodelta
115>int_events_append
116>associative_append %
117qed.
118
119lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'.
120  normal_state C s →
121  all … (λstr. normal_state C' (\fst str)) trace →
122  intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' →
123  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
124#C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL'
125>(int_trace_of_normal … NORMAL)
126cases (intensional_trace_of_trace C callstack rem) #callstack' #trace'
127#REM whd in ⊢ (??%?);
128elim trace in NORMAL' ⊢ %;
129[ #_ @REM
130| * #s' #tr' #tl #IH #NORMAL'
131  cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl
132  >int_trace_of_normal
133  [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%);
134    >int_events_append >associative_append %
135  | @NORMALs
136  ]
137] qed.
138
139lemma int_trace_append' : ∀C,t1,t2,callstack.
140  intensional_trace_of_trace C callstack (t1@t2) =
141    (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in
142     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in
143     〈cs'', t1'@t2'〉).
144#C #t1 #t2 elim t1
145[ #callstack whd in match ([ ]@t2); whd in ⊢ (???%);
146  cases (intensional_trace_of_trace ???) #cs' #trace' %
147| * #s #tr #tl #IH
148  #callstack
149  whd in match (intensional_trace_of_trace ???);
150  whd in match (intensional_trace_of_trace ???);
151  generalize in match (cs_callee C s);
152  cases (cs_classify C s)
153  normalize nodelta #callee
154  [ cases callstack [2: #cshd #cdtl] normalize nodelta ]
155  >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl'
156  normalize nodelta
157  cases (intensional_trace_of_trace C ? t2) #cs'' #tl''
158  normalize nodelta >associative_append >associative_append
159  %
160] qed.
161
162lemma int_trace_normal_cs : ∀C,callstack,trace.
163  all ? (λstr. normal_state C (\fst str)) trace →
164  callstack = \fst (intensional_trace_of_trace C callstack trace).
165#C #callstack #trace elim trace
166[ //
167| * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl
168  >(int_trace_of_normal … N1)
169  >(IH Ntl) in ⊢ (??%?);
170  cases (intensional_trace_of_trace ???) /2/
171] qed.
172
173lemma int_trace_append_normal : ∀C,t1,t2,callstack.
174  all ? (λstr. normal_state C (\fst str)) t1 →
175  intensional_trace_of_trace C callstack (t1@t2) =
176    (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in
177     let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in
178     〈cs'', t1'@t2'〉).
179#C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack)
180lapply (int_trace_normal_cs C callstack t1 NORMAL)
181cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct //
182qed.
183
184lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'.
185  cs_classify C s = cl_return →
186  cs_classify C' s' = cl_return →
187  all ? (λstr. normal_state C' (\fst str)) trace' →
188  intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' →
189  let trace ≝ 〈s',tr〉::trace' in
190  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
191#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E
192whd
193whd in ⊢ (??%%); normalize 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
216lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop.
217  (∀f. P f (f H)) →
218  P (cs_callee C s) (cs_callee C s H).
219#C #s #H #P #f @f
220qed.
221
222lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'.
223  all ? (λstr. normal_state C' (\fst str)) trace' →
224  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
225  cs_callee C s H = cs_callee C' s' H' →
226  let trace ≝ 〈s',tr〉::trace' in
227  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
228#C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL
229whd in ⊢ (? → ? → %);
230whd in ⊢ (? → ? → ??%%); normalize nodelta
231@generalize_callee
232@generalize_callee
233cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; *
234normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
235cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
236>(int_trace_append_normal … NORMAL) normalize nodelta
237cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
238destruct @eq_f @eq_f
239whd in match (gather_trace ??); >int_events_append
240>associative_append @eq_f
241elim trace in NORMAL ⊢ %;
242[ 1,3: #_ %
243| 2,4:
244  * #s1 #tr1 #tl #IH
245  #N cases (andb_Prop_true … N) #N1 #Ntl
246  whd in match (gather_trace ??); >int_events_append
247  >associative_append >(IH Ntl)
248  >(int_trace_of_normal … N1)
249  cases (intensional_trace_of_trace ?? tl)
250  #cs' #tl' >associative_append %
251] qed.
252 
253
254definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
255λcosts,start.
256  foldl ?? (λx. λev.
257    match ev with
258    [ IEVcall id ⇒
259        let 〈current_stack,max_stack〉 ≝ x in
260        let new_stack ≝ current_stack + costs id in
261        〈new_stack, max new_stack max_stack〉
262    | IEVret id ⇒
263        let 〈current_stack,max_stack〉 ≝ x in
264        〈current_stack - costs id, max_stack〉
265    | _ ⇒ x
266    ]) 〈start,start〉.
267
268definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
269λcosts, start, trace. \snd (measure_stack costs start trace).
270
271lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
272  (∀acc,el. P acc → P (f acc el)) →
273  ∀l,acc. P acc →
274  P (foldl A B f acc l).
275#A #B #P #f #IH #l elim l
276[ //
277| #h #t #IH' #acc #H @IH' @IH @H
278] qed.
279(*
280lemma max_stack_step : ∀C,a,m,a',m',tr,s.
281  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
282  m' = max m a'.
283#C #a #m #a' #m' #tr #s
284whd in match (measure_stack_aux ???);
285generalize in match (cs_stack C s); cases (cs_classify C s) #f
286normalize nodelta #E destruct //
287qed.
288
289lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
290  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
291  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
292  a1' = a2'.
293#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
294whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
295generalize in match (cs_stack C s); cases (cs_classify C s) #f
296normalize nodelta
297#E1 #E2 destruct
298%
299qed.
300
301
302lemma max_stack_steps : ∀C,trace,a,m.
303  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
304  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
305#C #trace elim trace
306[ #a #m >max_n_O %
307| * #tr #s #tl #IH #a #m
308  whd in match (foldl ?????);
309  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
310  whd in match (foldl ??? 〈a,O〉 ?);
311  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
312  >(IH a'') >IH
313  >(max_stack_step … M)
314  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
315] qed.
316
317lemma max_stack_append : ∀C,c1,ex1,ex2.
318  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
319#C #c1 #ex1 #ex2
320whd in match (max_stack ???); whd in match (stack_after ???);
321whd in match (max_stack ?? (ex1@ex2));
322whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
323generalize in match O; generalize in match c1; elim ex1
324[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
325| * #tr #s #tl #IH #c #m
326  whd in match (foldl ?????); whd in ⊢ (???(???%));
327  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
328  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
329  >IH %
330] qed.
331*) 
332
333(* Check that the trace ends with the return from the starting function and one
334   further state. *)
335
336let rec will_return_aux C (depth:nat)
337                        (trace:list (cs_state … C × trace)) on trace : bool ≝
338match trace with
339[ nil ⇒ false
340| cons h tl ⇒
341  let 〈s,tr〉 ≝ h in
342  match cs_classify C s with
343  [ cl_call ⇒ will_return_aux C (S depth) tl
344  | cl_return ⇒
345      match depth with
346       (* The state after the return will appear in the structured trace, but
347          not here because it is the second part of the pair returned by
348          exec_steps. *)
349      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
350      | S d ⇒ will_return_aux C d tl
351      ]
352  | _ ⇒ will_return_aux C depth tl
353  ]
354].
355definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
356
357(* Like classified_system, but we don't fix the global environment so that we
358   talk about the program separately. *)
359
360record preclassified_system : Type[2] ≝ {
361  pcs_exec :> fullexec io_out io_in;
362  pcs_labelled : ∀g. state … pcs_exec g → bool;
363  pcs_classify : ∀g. state … pcs_exec g → status_class;
364  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
365}.
366
367definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
368λC,g.
369  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
370
371(* FIXME: this definition is unreasonable because it presumes we can easily
372   identify the change in stack usage from return states, but that information
373   is rather implicit (we only really record the function called in the
374   extended RTLabs states when building the structured traces). *)
375
376definition measurable : ∀C:preclassified_system.
377  ∀p:program ?? C. nat → nat →
378  (ident → nat) (* stack cost *) →
379  nat → Prop ≝
380λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
381  let g ≝ make_global … (pcs_exec … C) p in
382  let C' ≝ pcs_to_cs C g in
383  make_initial_state … p = OK ? s0 ∧
384  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
385  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
386  trace_is_label_to_return C' interesting ∧
387  bool_to_Prop (will_return' C' interesting) ∧
388  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
389
390(* TODO: probably ought to be elsewhere; use exec_steps instead
391
392   Note that this does not include stack space
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
Note: See TracBrowser for help on using the repository browser.