source: src/common/Measurable.ma @ 2725

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

Add observables to FEMeasurable proof; fix silly typo.

File size: 15.9 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  cs_classify C s = cl_call →
224  cs_classify C' s' = cl_call →
225  all ? (λstr. normal_state C' (\fst str)) trace' →
226  intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' →
227  cs_callee C s H = cs_callee C' s' H' →
228  let trace ≝ 〈s',tr〉::trace' in
229  intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem').
230#C #C' #callstack #s #s' #tr #trace #rem #rem' #H #H' #CL #CL' #NORMAL
231whd in ⊢ (? → ? → %);
232whd in ⊢ (? → ? → ??%%); normalize nodelta
233@generalize_callee
234@generalize_callee
235>CL in H ⊢ %; * >CL' in H' ⊢ %; * normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE
236cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta
237>(int_trace_append_normal … NORMAL) normalize nodelta
238cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E
239destruct @eq_f @eq_f
240whd in match (gather_trace ??); >int_events_append
241>associative_append @eq_f
242elim trace in NORMAL ⊢ %;
243[ 1,3: #_ %
244| 2,4:
245  * #s1 #tr1 #tl #IH
246  #N cases (andb_Prop_true … N) #N1 #Ntl
247  whd in match (gather_trace ??); >int_events_append
248  >associative_append >(IH Ntl)
249  >(int_trace_of_normal … N1)
250  cases (intensional_trace_of_trace ?? tl)
251  #cs' #tl' >associative_append %
252] qed.
253 
254
255definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝
256λcosts,start.
257  foldl ?? (λx. λev.
258    match ev with
259    [ IEVcall id ⇒
260        let 〈current_stack,max_stack〉 ≝ x in
261        let new_stack ≝ current_stack + costs id in
262        〈new_stack, max new_stack max_stack〉
263    | IEVret id ⇒
264        let 〈current_stack,max_stack〉 ≝ x in
265        〈current_stack - costs id, max_stack〉
266    | _ ⇒ x
267    ]) 〈start,start〉.
268
269definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝
270λcosts, start, trace. \snd (measure_stack costs start trace).
271
272lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
273  (∀acc,el. P acc → P (f acc el)) →
274  ∀l,acc. P acc →
275  P (foldl A B f acc l).
276#A #B #P #f #IH #l elim l
277[ //
278| #h #t #IH' #acc #H @IH' @IH @H
279] qed.
280(*
281lemma max_stack_step : ∀C,a,m,a',m',tr,s.
282  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
283  m' = max m a'.
284#C #a #m #a' #m' #tr #s
285whd in match (measure_stack_aux ???);
286generalize in match (cs_stack C s); cases (cs_classify C s) #f
287normalize nodelta #E destruct //
288qed.
289
290lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
291  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
292  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
293  a1' = a2'.
294#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
295whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
296generalize in match (cs_stack C s); cases (cs_classify C s) #f
297normalize nodelta
298#E1 #E2 destruct
299%
300qed.
301
302
303lemma max_stack_steps : ∀C,trace,a,m.
304  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
305  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
306#C #trace elim trace
307[ #a #m >max_n_O %
308| * #tr #s #tl #IH #a #m
309  whd in match (foldl ?????);
310  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
311  whd in match (foldl ??? 〈a,O〉 ?);
312  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
313  >(IH a'') >IH
314  >(max_stack_step … M)
315  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
316] qed.
317
318lemma max_stack_append : ∀C,c1,ex1,ex2.
319  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
320#C #c1 #ex1 #ex2
321whd in match (max_stack ???); whd in match (stack_after ???);
322whd in match (max_stack ?? (ex1@ex2));
323whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
324generalize in match O; generalize in match c1; elim ex1
325[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
326| * #tr #s #tl #IH #c #m
327  whd in match (foldl ?????); whd in ⊢ (???(???%));
328  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
329  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
330  >IH %
331] qed.
332*) 
333
334(* Check that the trace ends with the return from the starting function and one
335   further state. *)
336
337let rec will_return_aux C (depth:nat)
338                        (trace:list (cs_state … C × trace)) on trace : bool ≝
339match trace with
340[ nil ⇒ false
341| cons h tl ⇒
342  let 〈s,tr〉 ≝ h in
343  match cs_classify C s with
344  [ cl_call ⇒ will_return_aux C (S depth) tl
345  | cl_return ⇒
346      match depth with
347       (* The state after the return will appear in the structured trace, but
348          not here because it is the second part of the pair returned by
349          exec_steps. *)
350      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
351      | S d ⇒ will_return_aux C d tl
352      ]
353  | _ ⇒ will_return_aux C depth tl
354  ]
355].
356definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
357
358(* Like classified_system, but we don't fix the global environment so that we
359   talk about the program separately. *)
360
361record preclassified_system : Type[2] ≝ {
362  pcs_exec :> fullexec io_out io_in;
363  pcs_labelled : ∀g. state … pcs_exec g → bool;
364  pcs_classify : ∀g. state … pcs_exec g → status_class;
365  pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident
366}.
367
368definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝
369λC,g.
370  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?).
371
372(* FIXME: this definition is unreasonable because it presumes we can easily
373   identify the change in stack usage from return states, but that information
374   is rather implicit (we only really record the function called in the
375   extended RTLabs states when building the structured traces). *)
376
377definition measurable : ∀C:preclassified_system.
378  ∀p:program ?? C. nat → nat →
379  (ident → nat) (* stack cost *) →
380  nat → Prop ≝
381λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
382  let g ≝ make_global … (pcs_exec … C) p in
383  let C' ≝ pcs_to_cs C g in
384  make_initial_state … p = OK ? s0 ∧
385  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
386  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
387  trace_is_label_to_return C' interesting ∧
388  bool_to_Prop (will_return' C' interesting) ∧
389  le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack.
390
391(* TODO: probably ought to be elsewhere; use exec_steps instead
392
393   Note that this does not include stack space
394 *)
395
396definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
397λC,p,m,n.
398  let g ≝ make_global … (pcs_exec … C) p in
399  let C' ≝ pcs_to_cs C g in
400  ! s0 ← make_initial_state … p;
401  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
402  ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1;
403  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
404  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
405
Note: See TracBrowser for help on using the repository browser.