Ignore:
Timestamp:
Feb 6, 2013, 5:03:18 PM (7 years ago)
Author:
campbell
Message:

Tidy up measurable a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2617 r2618  
    11include "common/Executions.ma".
    22include "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. *)
    37
    48record classified_system : Type[2] ≝ {
     
    1216definition cs_state : classified_system → Type[0] ≝
    1317λC. state … C (cs_global … C).
    14 
    15 definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
    16 
    17 let 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)) ≝
    18 match 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 ].
    3418
    3519(* Ideally we would also allow measurable traces to be from one cost label to
     
    8367definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.
    8468
     69(* Like classified_system, but we don't fix the global environment so that we
     70   talk about the program separately. *)
     71
    8572record preclassified_system : Type[2] ≝ {
    8673  pcs_exec :> fullexec io_out io_in;
     
    8976  pcs_stack : (ident → nat) → ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat
    9077}.
     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 ?).
    9182
    9283(* FIXME: this definition is unreasonable because it presumes we can easily
     
    10091  nat → Prop ≝
    10192λ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
     93  let C' ≝ pcs_to_cs C (make_global … p) stack_cost in
    10394  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〉 ∧
     95  split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
     96  split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
    10697  trace_is_label_to_return C' interesting ∧
    10798  bool_to_Prop (will_return' C' interesting) ∧
     
    116107λFE,p,m,n.
    117108  let trace ≝ exec_inf … FE p in
    118   match split_trace ? trace m with
     109  match split_trace trace m with
    119110  [ Some x ⇒
    120111    let 〈prefix,suffix〉 ≝ x in
    121     match split_trace ? suffix n with
     112    match split_trace suffix n with
    122113    [ Some y ⇒
    123114      let interesting ≝ \fst y in
     
    131122λFE,p,m.
    132123  let trace ≝ exec_inf … FE p in
    133   match split_trace ? trace m with
     124  match split_trace trace m with
    134125  [ Some x ⇒
    135126    match \snd x with
Note: See TracChangeset for help on using the changeset viewer.