source: src/common/Measurable.ma @ 2618

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

Tidy up measurable a little.

File size: 5.1 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 : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
28λC.
29  foldl … (λx, trs.
30    let 〈current,max_stack〉 ≝ x in
31    let 〈tr,s〉 ≝ trs in
32    let new ≝
33      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
34      [ cl_call ⇒ λsc. current + sc I
35      | cl_return ⇒ λsc. current - sc I
36      | _ ⇒ λ_. current
37      ] (cs_stack C s) in
38    〈new, max max_stack new〉) 〈0,0〉.
39
40definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
41λC,x. \fst (measure_stack C x).
42
43definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
44λC,x. \snd (measure_stack C x).
45
46(* Check that the trace ends with the return from the starting function and one
47   further state. *)
48
49let rec will_return_aux C (depth:nat)
50                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
51match trace with
52[ nil ⇒ false
53| cons h tl ⇒
54  let 〈tr,s〉 ≝ h in
55  match cs_classify C s with
56  [ cl_call ⇒ will_return_aux C (S depth) tl
57  | cl_return ⇒
58      match depth with
59       (* We need to see the state after the return to build the structured
60          trace. *)
61      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
62      | S d ⇒ will_return_aux C d tl
63      ]
64  | _ ⇒ will_return_aux C depth tl
65  ]
66].
67definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
68
69(* Like classified_system, but we don't fix the global environment so that we
70   talk about the program separately. *)
71
72record preclassified_system : Type[2] ≝ {
73  pcs_exec :> fullexec io_out io_in;
74  pcs_labelled : ∀g. state … pcs_exec g → bool;
75  pcs_classify : ∀g. state … pcs_exec g → status_class;
76  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
77}.
78
79definition pcs_to_cs : ∀C:preclassified_system. global … C → (ident → nat) → classified_system ≝
80λC,g,stack_cost.
81  mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?).
82
83(* FIXME: this definition is unreasonable because it presumes we can easily
84   identify the change in stack usage from return states, but that information
85   is rather implicit (we only really record the function called in the
86   extended RTLabs states when building the structured traces). *)
87
88definition measurable : ∀C:preclassified_system.
89  ∀p:program ?? C. nat → nat →
90  (ident → nat) (* stack cost *) →
91  nat → Prop ≝
92λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
93  let C' ≝ pcs_to_cs C (make_global … p) stack_cost in
94  let cl_trace ≝ exec_inf … (cs_exec … C') p in
95  split_trace … cl_trace m = Some ? 〈prefix,suffix〉 ∧
96  split_trace … suffix n = Some ? 〈interesting,remainder〉 ∧
97  trace_is_label_to_return C' interesting ∧
98  bool_to_Prop (will_return' C' interesting) ∧
99  le (max_stack C' (prefix@interesting)) max_allowed_stack.
100
101(* TODO: probably ought to be elsewhere
102
103   Note that this does not include stack space
104 *)
105
106definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
107λFE,p,m,n.
108  let trace ≝ exec_inf … FE p in
109  match split_trace … trace m with
110  [ Some x ⇒
111    let 〈prefix,suffix〉 ≝ x in
112    match split_trace … suffix n with
113    [ Some y ⇒
114      let interesting ≝ \fst y in
115      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
116    | _ ⇒ None ?
117    ]
118  | _ ⇒ None ?
119  ].
120
121definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
122λFE,p,m.
123  let trace ≝ exec_inf … FE p in
124  match split_trace … trace m with
125  [ Some x ⇒
126    match \snd x with
127    [ e_step _ s _ ⇒ Some ? s
128    | e_stop _ _ s ⇒ Some ? s
129    | _ ⇒ None ?
130    ]
131  | _ ⇒ None ?
132  ].
Note: See TracBrowser for help on using the repository browser.