Changeset 3096 for src/RTLabs


Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

Location:
src/RTLabs
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r2946 r3096  
    1818include "RTLabs/RTLabs_abstract.ma".
    1919include "RTL/RTL_semantics.ma".
     20include "RTLabs/MeasurableToStructured.ma". (* for make_ext_initial_state *)
    2021
    21 (* this is in incomplete RTLabs/MeasurableToStructured.ma *)
    22 definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝
    23 λp.
    24   let ge ≝ make_global p in
    25   do m ← init_mem … (λx.[Init_space x]) p;
    26   let main ≝ prog_main ?? p in
    27   do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    28   do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    29   let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in
    30   return (mk_RTLabs_ext_state (make_global p) s [b] ?).
    31 % [ @Ef | % ]
    32 qed.
    33 
    34 (* this should say something like λf,p.∀〈i, Internal f〉 ∈ functs p.f i ≥ stacksize f. *)
    35 axiom RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop.
     22definition RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop ≝
     23λstack_sizes,p.
     24All …
     25  (λi_f.let 〈i, f〉 ≝ i_f in
     26    match f with
     27    [ External _ ⇒ True
     28    | Internal def ⇒
     29      ∃sz.stack_sizes i = Some ? sz ∧ f_stacksize … def ≤ sz
     30    ]) (prog_funct … p).
    3631
    3732axiom RTLabsToRTL_ok :
    3833∀stacksizes : ident → option ℕ.
     34∀cost.
    3935∀p_in : RTLabs_program.
    4036RTLabsToRTLstacksizes_ok stacksizes p_in →
    41 let p_out ≝ rtlabs_to_rtl p_in in
     37let p_out ≝ rtlabs_to_rtl cost p_in in
     38∀init_in.make_ext_initial_state p_in = OK … init_in →
     39∃init_out : state_pc RTL_semantics_separate.
     40  make_initial_state
     41   (mk_prog_params RTL_semantics_separate p_out stacksizes) =
     42    OK ? init_out ∧
    4243∃[1] R.
    43   status_simulation
     44  status_simulation_with_init
    4445    (RTLabs_status (make_global … p_in))
    45     (joint_status RTL_semantics_separate p_out stacksizes) R ∧
    46   ∀init_in.make_ext_initial_state p_in = OK … init_in →
    47   ∃init_out : state_pc RTL_semantics_separate.
    48     make_initial_state
    49      (mk_prog_params RTL_semantics_separate p_out stacksizes) =
    50       OK ? init_out ∧
    51    R init_in init_out.
     46    (joint_status RTL_semantics_separate p_out stacksizes) R
     47    init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.