Changeset 2596 for src/correctness.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.