source: src/common/Measurable.ma @ 2617

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

Trivial simplification on split_trace.

File size: 5.3 KB
Line 
1include "common/Executions.ma".
2include "common/StructuredTraces.ma".  (* just for status_class *)
3
4record classified_system : Type[2] ≝ {
5  cs_exec :> fullexec io_out io_in;
6  cs_global : global … cs_exec;
7  cs_labelled : state … cs_exec cs_global → bool;
8  cs_classify : state … cs_exec cs_global → status_class;
9  cs_stack : ∀s. match cs_classify … s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
10}.
11
12definition cs_state : classified_system → Type[0] ≝
13λC. state … C (cs_global … C).
14
15definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
16
17let rec split_trace (state:Type[0]) (x:execution state io_out io_in) (n:nat) on n : option (execution_prefix state × (execution state io_out io_in)) ≝
18match n with
19[ O ⇒ Some ? 〈[ ], x〉
20| S n' ⇒
21  match x with
22  [ e_step tr s x' ⇒
23    ! 〈pre,x''〉 ← split_trace state x' n';
24    Some ? 〈〈tr,s〉::pre,x''〉
25    (* Necessary for a measurable trace at the end of the program *)
26  | e_stop tr r s ⇒
27    match n' with
28    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
29    | _ ⇒ None ?
30    ]
31  | _ ⇒ None ?
32  ]
33].
34
35(* Ideally we would also allow measurable traces to be from one cost label to
36   another (in the same function call), but due to time constraints we'll stick
37   to ending measurable traces at the end of the function only.
38 *)
39
40definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝
41λ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.
42
43definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
44λC.
45  foldl … (λx, trs.
46    let 〈current,max_stack〉 ≝ x in
47    let 〈tr,s〉 ≝ trs in
48    let new ≝
49      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
50      [ cl_call ⇒ λsc. current + sc I
51      | cl_return ⇒ λsc. current - sc I
52      | _ ⇒ λ_. current
53      ] (cs_stack C s) in
54    〈new, max max_stack new〉) 〈0,0〉.
55
56definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
57λC,x. \fst (measure_stack C x).
58
59definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
60λC,x. \snd (measure_stack C x).
61
62(* Check that the trace ends with the return from the starting function and one
63   further state. *)
64
65let rec will_return_aux C (depth:nat)
66                        (trace:execution_prefix (cs_state … C)) on trace : bool ≝
67match trace with
68[ nil ⇒ false
69| cons h tl ⇒
70  let 〈tr,s〉 ≝ h in
71  match cs_classify C s with
72  [ cl_call ⇒ will_return_aux C (S depth) tl
73  | cl_return ⇒
74      match depth with
75       (* We need to see the state after the return to build the structured
76          trace. *)
77      [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true | _ ⇒ false ] | _ ⇒ false ]
78      | S d ⇒ will_return_aux C d tl
79      ]
80  | _ ⇒ will_return_aux C depth tl
81  ]
82].
83definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
84
85record preclassified_system : Type[2] ≝ {
86  pcs_exec :> fullexec io_out io_in;
87  pcs_labelled : ∀g. state … pcs_exec g → bool;
88  pcs_classify : ∀g. state … pcs_exec g → status_class;
89  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
90}.
91
92(* FIXME: this definition is unreasonable because it presumes we can easily
93   identify the change in stack usage from return states, but that information
94   is rather implicit (we only really record the function called in the
95   extended RTLabs states when building the structured traces). *)
96
97definition measurable : ∀C:preclassified_system.
98  ∀p:program ?? C. nat → nat →
99  (ident → nat) (* stack cost *) →
100  nat → Prop ≝
101λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
102  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?) in
103  let cl_trace ≝ exec_inf … (cs_exec … C') p in
104  split_trace ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
105  split_trace ? suffix n = Some ? 〈interesting,remainder〉 ∧
106  trace_is_label_to_return C' interesting ∧
107  bool_to_Prop (will_return' C' interesting) ∧
108  le (max_stack C' (prefix@interesting)) max_allowed_stack.
109
110(* TODO: probably ought to be elsewhere
111
112   Note that this does not include stack space
113 *)
114
115definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
116λFE,p,m,n.
117  let trace ≝ exec_inf … FE p in
118  match split_trace ? trace m with
119  [ Some x ⇒
120    let 〈prefix,suffix〉 ≝ x in
121    match split_trace ? suffix n with
122    [ Some y ⇒
123      let interesting ≝ \fst y in
124      Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
125    | _ ⇒ None ?
126    ]
127  | _ ⇒ None ?
128  ].
129
130definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
131λFE,p,m.
132  let trace ≝ exec_inf … FE p in
133  match split_trace ? trace m with
134  [ Some x ⇒
135    match \snd x with
136    [ e_step _ s _ ⇒ Some ? s
137    | e_stop _ _ s ⇒ Some ? s
138    | _ ⇒ None ?
139    ]
140  | _ ⇒ None ?
141  ].
Note: See TracBrowser for help on using the repository browser.