source: src/common/Measurable.ma @ 2486

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

First go at a generalised version of measurable.

File size: 3.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 : classified_system → Type[0] ≝ λC. list (trace × (cs_state C)).
16
17let rec split_trace C (x:execution (cs_state C) io_out io_in) (n:nat) on n : option (execution_prefix C × (execution (cs_state C) 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 C x' n';
24    Some ? 〈〈tr,s〉::pre,x''〉
25  | _ ⇒ None ?
26  ]
27].
28
29definition trace_labelled : ∀C. execution_prefix C → Prop ≝
30λC,x. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ bool_to_Prop (cs_labelled C s2).
31
32definition measure_stack : ∀C. execution_prefix C → nat × nat ≝
33λC.
34  foldl … (λx, trs.
35    let 〈current,max_stack〉 ≝ x in
36    let 〈tr,s〉 ≝ trs in
37    let new ≝
38      match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
39      [ cl_call ⇒ λsc. current + sc I
40      | cl_return ⇒ λsc. current - sc I
41      | _ ⇒ λ_. current
42      ] (cs_stack C s) in
43    〈new, max max_stack new〉) 〈0,0〉.
44
45definition stack_after : ∀C. execution_prefix C → nat ≝
46λC,x. \fst (measure_stack C x).
47
48definition max_stack : ∀C. execution_prefix C → nat ≝
49λC,x. \snd (measure_stack C x).
50
51let rec will_return_aux C (depth:nat)
52                        (trace:execution_prefix C) on trace : bool ≝
53match trace with
54[ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
55| cons h tl ⇒
56  let 〈tr,s〉 ≝ h in
57  match cs_classify C s with
58  [ cl_call ⇒ will_return_aux C (S depth) tl
59  | cl_return ⇒
60      match depth with
61      [ O ⇒ 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 C → bool ≝ λC. will_return_aux C O.
68
69record preclassified_system : Type[2] ≝ {
70  pcs_exec :> fullexec io_out io_in;
71  pcs_labelled : ∀g. state … pcs_exec g → bool;
72  pcs_classify : ∀g. state … pcs_exec g → status_class
73}.
74
75definition measurable : ∀C:preclassified_system.
76  ∀p:program ?? C. nat → nat →
77  (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
78  nat → Prop ≝
79λC,p,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
80  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
81  let cl_trace ≝ exec_inf … (cs_exec … C') p in
82  split_trace C' cl_trace m = Some ? 〈prefix,suffix〉 ∧
83  split_trace C' suffix n = Some ? 〈interesting,remainder〉 ∧
84  trace_labelled C' interesting ∧
85  bool_to_Prop (will_return' C' interesting) ∧
86  le (max_stack C' (prefix@interesting)) max_allowed_stack.
Note: See TracBrowser for help on using the repository browser.