source: src/common/Measurable.ma @ 2668

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

Intermediate measurable proof check-in before I change its traces again.

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. execution_prefix (cs_state … C) → Prop ≝
25λC,x. ∃tr1,s1,x',tr2,s2,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
26
27definition measure_stack_aux ≝
28λC. (λx. λtrs:trace × (cs_state … C).
29    let 〈current,max_stack〉 ≝ x in
30    let 〈tr,s〉 ≝ trs 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 → execution_prefix (cs_state … C) → nat × nat ≝
40λC,current.
41  foldl … (measure_stack_aux C) 〈current,0〉.
42
43definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝
44λC,current,x. \fst (measure_stack C current x).
45
46definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → 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〉 〈tr,s〉 = 〈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',trs.
68  measure_stack_aux C 〈a,m1〉 trs = 〈a1',m1'〉 →
69  measure_stack_aux C 〈a,m2〉 trs = 〈a2',m2'〉 →
70  a1' = a2'.
71#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #tr #s
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:execution_prefix (cs_state … C)) on trace : bool ≝
227match trace with
228[ nil ⇒ false
229| cons h tl ⇒
230  let 〈tr,s〉 ≝ 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       (* We need to see the state after the return to build the structured
236          trace. *)
237      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
238      | S d ⇒ will_return_aux C d tl
239      ]
240  | _ ⇒ will_return_aux C depth tl
241  ]
242].
243definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
244
245(* Like classified_system, but we don't fix the global environment so that we
246   talk about the program separately. *)
247
248record preclassified_system : Type[2] ≝ {
249  pcs_exec :> fullexec io_out io_in;
250  pcs_labelled : ∀g. state … pcs_exec g → bool;
251  pcs_classify : ∀g. state … pcs_exec g → status_class;
252  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
253}.
254
255definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝
256λC,g,stack_cost.
257  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?).
258
259(* FIXME: this definition is unreasonable because it presumes we can easily
260   identify the change in stack usage from return states, but that information
261   is rather implicit (we only really record the function called in the
262   extended RTLabs states when building the structured traces). *)
263
264definition measurable : ∀C:preclassified_system.
265  ∀p:program ?? C. nat → nat →
266  (ident → nat) (* stack cost *) →
267  nat → Prop ≝
268λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
269  let g ≝ make_global … (pcs_exec … C) p in
270  let C' ≝ pcs_to_cs C g stack_cost in
271  make_initial_state … p = OK ? s0 ∧
272  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
273  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
274  trace_is_label_to_return C' interesting ∧
275  bool_to_Prop (will_return' C' interesting) ∧
276  le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.
277
278(* TODO: probably ought to be elsewhere; use exec_steps instead
279
280   Note that this does not include stack space
281 *)
282
283definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
284λFE,p,m,n.
285  let trace ≝ exec_inf … FE p in
286  match split_trace … trace m with
287  [ Some x ⇒
288    let 〈prefix,suffix〉 ≝ x in
289    match split_trace … suffix n with
290    [ Some y ⇒
291      let interesting ≝ \fst y in
292      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
293    | _ ⇒ None ?
294    ]
295  | _ ⇒ None ?
296  ].
297
298definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
299λFE,p,m.
300  let trace ≝ exec_inf … FE p in
301  match split_trace … trace m with
302  [ Some x ⇒
303    match \snd x with
304    [ e_step _ s _ ⇒ Some ? s
305    | e_stop _ _ s ⇒ Some ? s
306    | _ ⇒ None ?
307    ]
308  | _ ⇒ None ?
309  ].
Note: See TracBrowser for help on using the repository browser.