Changeset 2618 for src


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

Tidy up measurable a little.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2597 r2618  
    1313  ms_C2 : preclassified_system;
    1414  ms_compiled : program … ms_C1 → program … ms_C2 → Prop;
    15   ms_inv : ? → ? → Prop;
     15  ms_inv : ? → ? → Type[0];
     16  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    1617  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
    1718  sim_normal :
     
    7374  ms_rel MS g1 g2 INV s1 s1' →
    7475  ∀m,prefix,suffix.
    75   split_trace (ms_C1 MS) ? trace m = Some ? 〈prefix,suffix〉 →
    76   le (max_stack (ms_C1 MS) prefix) max_allowed_stack →
     76  split_trace ? trace m = Some ? 〈prefix,suffix〉 →
     77  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
    7778  ∃m',prefix',suffix'.
    78   split_trace (ms_C2 MS) ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
    79   le (max_stack (ms_C1 MS) prefix') max_allowed_stack ∧
     79  split_trace ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
     80  le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
    8081  ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧
    81     ms_rel g1 g2 INV s2 s2'.
     82    ms_rel MS g1 g2 INV s2 s2'.
    8283
    8384theorem measured_subtrace_preserved :
  • 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
  • src/common/SmallstepExec.ma

    r2487 r2618  
    355355
    356356
     357
     358
     359definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
     360
     361let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝
     362match n with
     363[ O ⇒ Some ? 〈[ ], x〉
     364| S n' ⇒
     365  match x with
     366  [ e_step tr s x' ⇒
     367    ! 〈pre,x''〉 ← split_trace ?? state x' n';
     368    Some ? 〈〈tr,s〉::pre,x''〉
     369    (* Necessary for a measurable trace at the end of the program *)
     370  | e_stop tr r s ⇒
     371    match n' with
     372    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
     373    | _ ⇒ None ?
     374    ]
     375  | _ ⇒ None ?
     376  ]
     377].
     378
     379
Note: See TracChangeset for help on using the changeset viewer.