source: src/common/Measurable.ma @ 2669

Last change on this file since 2669 was 2669, checked in by campbell, 8 years ago

Tweak exec_steps output; show that simulations extend to measurable
subtrace prefixes.

File size: 10.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_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(* TODO: move*)
80lemma max_O_n : ∀n. max O n = n.
81* //
82qed.
83
84lemma max_n_O : ∀n. max n O = n.
85* //
86qed.
87
88lemma associative_max : associative nat max.
89#n #m #o normalize
90@(leb_elim n m)
91[ normalize @(leb_elim m o) normalize #H1 #H2
92  [ >(le_to_leb_true n o) /2/
93  | >(le_to_leb_true n m) //
94  ]
95| normalize @(leb_elim m o) normalize #H1 #H2
96  [ %
97  | >(not_le_to_leb_false … H2)
98    >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
99  ]
100] qed.
101
102
103lemma max_stack_steps : ∀C,trace,a,m.
104  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
105  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
106#C #trace elim trace
107[ #a #m >max_n_O %
108| * #tr #s #tl #IH #a #m
109  whd in match (foldl ?????);
110  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
111  whd in match (foldl ??? 〈a,O〉 ?);
112  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
113  >(IH a'') >IH
114  >(max_stack_step … M)
115  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
116] qed.
117
118(*
119lemma max_stack_step : ∀C,a,m,tr,s.
120  m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉).
121#C #a #m #tr #s
122whd in match (measure_stack_aux ???);
123generalize in match (cs_stack C s); cases (cs_classify C s) normalize
124#f @(leb_elim m) normalize #H /2/
125qed.
126
127lemma max_stack_steps : ∀C. ∀am. ∀trace.
128  \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace).
129#C * #a #m #trace
130@foldl_inv
131[ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step
132| //
133] qed.
134
135lemma max_stack_step' : ∀C,a,m,a',m',tr,s.
136  a ≤ a' → m ≤ m' →
137  \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
138#C #a #m #a' #m' #tr #s #H1 #H2
139whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
140generalize in match (cs_stack C s); cases (cs_classify C s) #f
141whd in ⊢ (?(??%)(??%));
142[ @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'-f I)) /2/ ]
143| 2,4,5: @to_max /2 by max_r, max_l/
144| @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'+f I)) /2/ ]
145] qed.
146
147lemma max_stack_step'' : ∀C,a,m,a',m',tr,s.
148  a ≤ a' →
149  \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
150#C #a #m #a' #m' #tr #s #H1
151whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
152generalize in match (cs_stack C s); cases (cs_classify C s) #f
153whd in ⊢ (?%%); /2/
154qed.
155
156lemma max_stack_steps' : ∀C. ∀trace,am,am'.
157  \fst am ≤ \fst am' → \snd am ≤ \snd am' →
158  \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace).
159#C #trace elim trace
160[ * #a #m * #a' #m' #H1 #H2 @H2
161| * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' // | @max_stack_step' // ]
162] qed.
163
164lemma max_stack_append_l : ∀C,ex1,ex2.
165  max_stack C ex1 ≤ max_stack C (ex1@ex2).
166#C #ex1 #ex2 whd in ⊢ (??%);
167whd in match (measure_stack ? (ex1@ex2));
168>foldl_append
169@max_stack_steps
170qed.
171
172lemma max_stack_append_r : ∀C,ex1,ex2.
173  max_stack C ex2 ≤ max_stack C (ex1@ex2).
174#C #ex1 #ex2 whd in ⊢ (??%);
175whd in match (measure_stack ? (ex1@ex2));
176>foldl_append
177@max_stack_steps' //
178qed.
179*)(*
180lemma max_stack_append : ∀C,ex1,ex2.
181  max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2).
182#C #ex1 #ex2
183whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2));
184whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2));
185generalize in match 〈O,O〉; elim ex1
186[ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps
187
188elim ex1
189[ #ex2 >max_O_n %
190| * #tr #s #tl #IH #ex2
191  whd in match (max_stack ??); whd in match (measure_stack ??);
192  lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉))
193  cases (measure_stack_aux ???) in ⊢ (???% → %);
194  #a #m #M
195 
196 #ex2
197@le_to_le_to_eq
198[ @to_max //
199|
200 whd in ⊢ (???%);
201
202whd in match (measure_stack ? (ex1@ex2));
203>foldl_append
204@max_stack_steps' //
205*)
206lemma max_stack_append : ∀C,c1,ex1,ex2.
207  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
208#C #c1 #ex1 #ex2
209whd in match (max_stack ???); whd in match (stack_after ???);
210whd in match (max_stack ?? (ex1@ex2));
211whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
212generalize in match O; generalize in match c1; elim ex1
213[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
214| * #tr #s #tl #IH #c #m
215  whd in match (foldl ?????); whd in ⊢ (???(???%));
216  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
217  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
218  >IH %
219] qed.
220 
221
222(* Check that the trace ends with the return from the starting function and one
223   further state. *)
224
225let rec will_return_aux C (depth:nat)
226                        (trace:list (cs_state … C × trace)) on trace : bool ≝
227match trace with
228[ nil ⇒ false
229| cons h tl ⇒
230  let 〈s,tr〉 ≝ h in
231  match cs_classify C s with
232  [ cl_call ⇒ will_return_aux C (S depth) tl
233  | cl_return ⇒
234      match depth with
235       (* The state after the return will appear in the structured trace, but
236          not here because it is the second part of the pair returned by
237          exec_steps. *)
238      [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ]
239      | S d ⇒ will_return_aux C d tl
240      ]
241  | _ ⇒ will_return_aux C depth tl
242  ]
243].
244definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O.
245
246(* Like classified_system, but we don't fix the global environment so that we
247   talk about the program separately. *)
248
249record preclassified_system : Type[2] ≝ {
250  pcs_exec :> fullexec io_out io_in;
251  pcs_labelled : ∀g. state … pcs_exec g → bool;
252  pcs_classify : ∀g. state … pcs_exec g → status_class;
253  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
254}.
255
256definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝
257λC,g,stack_cost.
258  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?).
259
260(* FIXME: this definition is unreasonable because it presumes we can easily
261   identify the change in stack usage from return states, but that information
262   is rather implicit (we only really record the function called in the
263   extended RTLabs states when building the structured traces). *)
264
265definition measurable : ∀C:preclassified_system.
266  ∀p:program ?? C. nat → nat →
267  (ident → nat) (* stack cost *) →
268  nat → Prop ≝
269λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
270  let g ≝ make_global … (pcs_exec … C) p in
271  let C' ≝ pcs_to_cs C g stack_cost in
272  make_initial_state … p = OK ? s0 ∧
273  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
274  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
275  trace_is_label_to_return C' interesting ∧
276  bool_to_Prop (will_return' C' interesting) ∧
277  le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.
278
279(* TODO: probably ought to be elsewhere; use exec_steps instead
280
281   Note that this does not include stack space
282 *)
283
284definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
285λFE,p,m,n.
286  let trace ≝ exec_inf … FE p in
287  match split_trace … trace m with
288  [ Some x ⇒
289    let 〈prefix,suffix〉 ≝ x in
290    match split_trace … suffix n with
291    [ Some y ⇒
292      let interesting ≝ \fst y in
293      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
294    | _ ⇒ None ?
295    ]
296  | _ ⇒ None ?
297  ].
298
299definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
300λFE,p,m.
301  let trace ≝ exec_inf … FE p in
302  match split_trace … trace m with
303  [ Some x ⇒
304    match \snd x with
305    [ e_step _ s _ ⇒ Some ? s
306    | e_stop _ _ s ⇒ Some ? s
307    | _ ⇒ None ?
308    ]
309  | _ ⇒ None ?
310  ].
Note: See TracBrowser for help on using the repository browser.