source: src/common/Measurable.ma @ 2670

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

Clean up from recent commits.

File size: 7.5 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_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
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 measure_stack_aux ≝
28λC. (λx. λstr:cs_state … C × trace.
29    let 〈current,max_stack〉 ≝ x in
30    let 〈s,tr〉 ≝ str in
31    let new ≝
32      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
33      [ cl_call ⇒ λsc. current + sc I
34      | cl_return ⇒ λsc. current - sc I
35      | _ ⇒ λ_. current
36      ] (cs_stack C s) in
37    〈new, max max_stack new〉).
38
39definition measure_stack : ∀C. nat → list (cs_state … C × trace) → nat × nat ≝
40λC,current.
41  foldl … (measure_stack_aux C) 〈current,0〉.
42
43definition stack_after : ∀C. nat → list (cs_state … C × trace) → nat ≝
44λC,current,x. \fst (measure_stack C current x).
45
46definition max_stack : ∀C. nat → list (cs_state … C × trace) → nat ≝
47λC,current,x. \snd (measure_stack C current x).
48
49lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
50  (∀acc,el. P acc → P (f acc el)) →
51  ∀l,acc. P acc →
52  P (foldl A B f acc l).
53#A #B #P #f #IH #l elim l
54[ //
55| #h #t #IH' #acc #H @IH' @IH @H
56] qed.
57
58lemma max_stack_step : ∀C,a,m,a',m',tr,s.
59  measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 →
60  m' = max m a'.
61#C #a #m #a' #m' #tr #s
62whd in match (measure_stack_aux ???);
63generalize in match (cs_stack C s); cases (cs_classify C s) #f
64normalize nodelta #E destruct //
65qed.
66
67lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str.
68  measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 →
69  measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 →
70  a1' = a2'.
71#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr
72whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
73generalize in match (cs_stack C s); cases (cs_classify C s) #f
74normalize nodelta
75#E1 #E2 destruct
76%
77qed.
78
79
80lemma max_stack_steps : ∀C,trace,a,m.
81  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
82  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
83#C #trace elim trace
84[ #a #m >max_n_O %
85| * #tr #s #tl #IH #a #m
86  whd in match (foldl ?????);
87  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
88  whd in match (foldl ??? 〈a,O〉 ?);
89  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
90  >(IH a'') >IH
91  >(max_stack_step … M)
92  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
93] qed.
94
95lemma max_stack_append : ∀C,c1,ex1,ex2.
96  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
97#C #c1 #ex1 #ex2
98whd in match (max_stack ???); whd in match (stack_after ???);
99whd in match (max_stack ?? (ex1@ex2));
100whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
101generalize in match O; generalize in match c1; elim ex1
102[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
103| * #tr #s #tl #IH #c #m
104  whd in match (foldl ?????); whd in ⊢ (???(???%));
105  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
106  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
107  >IH %
108] qed.
109 
110
111(* Check that the trace ends with the return from the starting function and one
112   further state. *)
113
114let rec will_return_aux C (depth:nat)
115                        (trace:list (cs_state … C × trace)) on trace : bool ≝
116match trace with
117[ nil ⇒ false
118| cons h tl ⇒
119  let 〈s,tr〉 ≝ h in
120  match cs_classify C s with
121  [ cl_call ⇒ will_return_aux C (S depth) tl
122  | cl_return ⇒
123      match depth with
124       (* The state after the return will appear in the structured trace, but
125          not here because it is the second part of the pair returned by
126          exec_steps. *)
127      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
128      | S d ⇒ will_return_aux C d tl
129      ]
130  | _ ⇒ will_return_aux C depth tl
131  ]
132].
133definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
134
135(* Like classified_system, but we don't fix the global environment so that we
136   talk about the program separately. *)
137
138record preclassified_system : Type[2] ≝ {
139  pcs_exec :> fullexec io_out io_in;
140  pcs_labelled : ∀g. state … pcs_exec g → bool;
141  pcs_classify : ∀g. state … pcs_exec g → status_class;
142  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
143}.
144
145definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝
146λC,g,stack_cost.
147  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?).
148
149(* FIXME: this definition is unreasonable because it presumes we can easily
150   identify the change in stack usage from return states, but that information
151   is rather implicit (we only really record the function called in the
152   extended RTLabs states when building the structured traces). *)
153
154definition measurable : ∀C:preclassified_system.
155  ∀p:program ?? C. nat → nat →
156  (ident → nat) (* stack cost *) →
157  nat → Prop ≝
158λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
159  let g ≝ make_global … (pcs_exec … C) p in
160  let C' ≝ pcs_to_cs C g stack_cost in
161  make_initial_state … p = OK ? s0 ∧
162  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
163  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
164  trace_is_label_to_return C' interesting ∧
165  bool_to_Prop (will_return' C' interesting) ∧
166  le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.
167
168(* TODO: probably ought to be elsewhere; use exec_steps instead
169
170   Note that this does not include stack space
171 *)
172
173definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
174λFE,p,m,n.
175  let trace ≝ exec_inf … FE p in
176  match split_trace … trace m with
177  [ Some x ⇒
178    let 〈prefix,suffix〉 ≝ x in
179    match split_trace … suffix n with
180    [ Some y ⇒
181      let interesting ≝ \fst y in
182      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
183    | _ ⇒ None ?
184    ]
185  | _ ⇒ None ?
186  ].
187
188definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
189λFE,p,m.
190  let trace ≝ exec_inf … FE p in
191  match split_trace … trace m with
192  [ Some x ⇒
193    match \snd x with
194    [ e_step _ s _ ⇒ Some ? s
195    | e_stop _ _ s ⇒ Some ? s
196    | _ ⇒ None ?
197    ]
198  | _ ⇒ None ?
199  ].
Note: See TracBrowser for help on using the repository browser.