Changeset 2506


Ignore:
Timestamp:
Nov 29, 2012, 6:38:37 PM (7 years ago)
Author:
campbell
Message:

Use common definition of measurable.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2475 r2506  
    3939
    4040include "Clight/abstract.ma".
     41include "common/Measurable.ma".
    4142
    4243definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
    4344
    44 definition execution_prefix : Type[0] ≝ list (trace × Clight_state).
    45 let rec split_trace (x:execution Clight_state io_out io_in) (n:nat) on n : option (execution_prefix × (execution Clight_state io_out io_in)) ≝
    46 match n with
    47 [ O ⇒ Some ? 〈[ ], x〉
    48 | S n' ⇒
    49   match x with
    50   [ e_step tr s x' ⇒
    51     ! 〈pre,x''〉 ← split_trace x' n';
    52     Some ? 〈〈tr,s〉::pre,x''〉
    53   | _ ⇒ None ?
    54   ]
    55 ].
    56 
    57 definition trace_labelled : execution_prefix → Prop ≝
    58 λx. ∃tr1,s1,x',tr2,s2. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉]) ∧ bool_to_Prop (Clight_labelled s1) ∧ bool_to_Prop (Clight_labelled s2).
    59 
    60 definition measure_stack : Clight_stack_T → execution_prefix → nat × nat ≝
    61 λstack_cost.
    62   foldl … (λx, trs.
    63     let 〈current,max_stack〉 ≝ x in
    64     let 〈tr,s〉 ≝ trs in
    65     let new ≝
    66       match Clight_classify s return λcl. (match cl in status_class with [_⇒?] → ?) → ?  with
    67       [ cl_call ⇒ λsc. current + sc I
    68       | cl_return ⇒ λsc. current - sc I
    69       | _ ⇒ λ_. current
    70       ] (stack_cost s) in
    71     〈new, max max_stack new〉) 〈0,0〉.
    72 
    73 definition stack_after : Clight_stack_T → execution_prefix → nat ≝
    74 λsc,x. \fst (measure_stack sc x).
    75 
    76 definition max_stack :  Clight_stack_T → execution_prefix → nat ≝
    77 λsc,x. \snd (measure_stack sc x).
    78 
    79 let rec will_return_aux (depth:nat)
    80                         (trace:execution_prefix) on trace : bool ≝
    81 match trace with
    82 [ nil ⇒ match depth with [ O ⇒ true | _ ⇒ false ]
    83 | cons h tl ⇒
    84   let 〈tr,s〉 ≝ h in
    85   match Clight_classify s with
    86   [ cl_call ⇒ will_return_aux (S depth) tl
    87   | cl_return ⇒
    88       match depth with
    89       [ O ⇒ false
    90       | S d ⇒ will_return_aux d tl
    91       ]
    92   | _ ⇒ will_return_aux depth tl
    93   ]
    94 ].
    95 definition will_return' : execution_prefix → bool ≝ will_return_aux O.
    96 
    97 definition measurable : clight_program → nat → nat → Clight_stack_T → nat → Prop ≝
    98 λp,m,n,stack_cost,max_allowed_stack.  ∀prefix,suffix,interesting,remainder.
    99   let cl_trace ≝ exec_inf … clight_fullexec p in
    100   split_trace cl_trace m = Some ? 〈prefix,suffix〉 ∧
    101   split_trace suffix n = Some ? 〈interesting,remainder〉 ∧
    102   trace_labelled interesting ∧
    103   bool_to_Prop (will_return' interesting) ∧
    104   max_stack stack_cost (prefix@interesting) < max_allowed_stack.
     45definition Clight_pcs : preclassified_system ≝
     46mk_preclassified_system
     47  clight_fullexec
     48  (λ_.Clight_labelled)
     49  (λ_.Clight_classify).
    10550
    10651(* From measurable on Clight, we will end up with an RTLabs flat trace where
     
    11459 *)
    11560
    116 definition observables : clight_program → nat → nat → option ((list trace) × (list trace)) ≝
    117 λp,m,n.
    118   let cl_trace ≝ exec_inf … clight_fullexec p in
    119   match split_trace cl_trace m with
    120   [ Some x ⇒
    121     let 〈prefix,suffix〉 ≝ x in
    122     match split_trace suffix n with
    123     [ Some y ⇒
    124       let interesting ≝ \fst y in
    125       Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
    126     | _ ⇒ None ?
    127     ]
    128   | _ ⇒ None ?
    129   ].
    130 
    13161axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
    13262
    133 definition in_execution_prefix : execution_prefix → costlabel → Prop ≝
     63definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
    13464λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
    13565
     
    15585] qed.
    15686
    157 definition measure_clock : ∀x:execution_prefix. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
     87definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
    15888λx,costmap. foldl_exists … x
    15989 (λclock,trs,H.
     
    16696λp,n,costmap.
    16797  let x ≝ exec_inf … clight_fullexec p in
    168   match split_trace x n with
     98  match split_trace x n with
    16999  [ Some traces ⇒
    170100    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
     
    177107
    178108definition simulates ≝
    179   λstack_cost, stack_bound, labelled, object_code, cost_map.
     109  λstack_cost : Clight_stack_T.  λ stack_bound, labelled, object_code, cost_map.
    180110  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
    181   ∀m1,m2. measurable labelled m1 m2 stack_cost stack_bound →
     111  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    182112  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    183   ∃n1,n2. observables labelled m1 m2 = observables_8051 object_code n1 n2 ∧
     113  ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧
    184114          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    185115
Note: See TracChangeset for help on using the changeset viewer.