Changeset 2596


Ignore:
Timestamp:
Jan 31, 2013, 12:06:58 PM (6 years ago)
Author:
campbell
Message:

Use a simpler stack cost map, and then specialise to each semantics.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2534 r2596  
    8686  pcs_exec :> fullexec io_out io_in;
    8787  pcs_labelled : ∀g. state … pcs_exec g → bool;
    88   pcs_classify : ∀g. state … pcs_exec g → status_class
     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
    8990}.
    9091
     
    9697definition measurable : ∀C:preclassified_system.
    9798  ∀p:program ?? C. nat → nat →
    98   (∀s. match pcs_classify … (make_global … p) s with  [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat) →
     99  (ident → nat) (* stack cost *) →
    99100  nat → Prop ≝
    100101λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
    101   let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) stack_cost in
     102  let C' ≝ mk_classified_system (pcs_exec C) (make_global … p) (pcs_labelled C ?) (pcs_classify C ?) (pcs_stack C stack_cost ?) in
    102103  let cl_trace ≝ exec_inf … (cs_exec … C') p in
    103104  split_trace C' ? cl_trace m = Some ? 〈prefix,suffix〉 ∧
  • src/correctness.ma

    r2513 r2596  
    4141include "common/Measurable.ma".
    4242
    43 definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
     43(* We could restrict this function to identifiers that are function names in the
     44   program and lift it (like the lift_cost_map_back_to_front function), but
     45   let's go with the easier notion of having a total map and ignore all the
     46   extra stuff. *)
     47definition stack_cost_T ≝ ident → nat.
     48
     49axiom Clight_stack_cost :
     50  stack_cost_T →
     51  ∀s:Clight_state.
     52  match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] →
     53  nat.
    4454
    4555definition Clight_pcs : preclassified_system ≝
     
    4757  clight_fullexec
    4858  (λ_.Clight_labelled)
    49   (λ_.Clight_classify).
     59  (λ_.Clight_classify)
     60  (λf,g. Clight_stack_cost f).
    5061
    5162(* From measurable on Clight, we will end up with an RTLabs flat trace where
     
    107118
    108119definition simulates ≝
    109   λstack_cost : Clight_stack_T.  λ stack_bound, labelled, object_code, cost_map.
     120  λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map.
    110121  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
    111122  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
     
    115126
    116127axiom compile' : clight_program → res (object_code × costlabel_map ×
    117   (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat).
     128  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × stack_cost_T × nat).
    118129
    119130theorem correct' :
Note: See TracChangeset for help on using the changeset viewer.