Changeset 3145 for src/RTLabs


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (6 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
Location:
src/RTLabs
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r3031 r3145  
    514514  exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 →
    515515  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace' = 〈cs',obs〉 →
    516   pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ?
     516  observables_trace_label_return (RTLabs_status ge) s s' tlr fn = obs ∧ cs = cs' ≝ ?
    517517and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll :
    518518  exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    519519  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    520   pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ?
     520  observables_trace_label_label (RTLabs_status ge) ends s s' tll fn = obs ∧ cs_change ends fn cs cs' ≝ ?
    521521and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal :
    522522  exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 →
    523523  intensional_trace_of_trace (pcs_to_cs RTLabs_pcs ge) (fn::cs) trace1 = 〈cs',obs〉 →
    524   maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?.
     524  maybe_label ge s (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn) = obs ∧ cs_change ends fn cs cs' ≝ ?.
    525525[ cases tlr
    526526  [ #s1 #s2 #tll @eq_obs_tll
     
    648648  tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧
    649649  le (maximum (update_stacksize_info stack_cost (mk_stacksize_info 0 0) (extract_call_ud_from_observables (prefix@interesting)))) max ∧
    650   pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting.
     650  observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn = interesting.
    651651#p #m #n #stack_cost #max #prefix #interesting
    652652#WCLP cases (well_cost_labelled_make_global p WCLP)
  • src/RTLabs/RTLabsToRTL.ma

    r3037 r3145  
    44include "common/Graphs.ma".
    55include "joint/TranslateUtils.ma".
     6include "joint/joint_stacksizes.ma".
    67include alias "ASM/BitVector.ma".
    78include alias "arithmetics/nat.ma".
     
    10841085  let entry' ≝ pi1 … (f_entry def) in
    10851086  let init ≝ mk_joint_internal_function RTL globals
    1086     luniverse' runiverse' [ ] [ ] stack_size' stack_size'
     1087    luniverse' runiverse' [ ] [ ] 0 0
    10871088    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10881089  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     
    10961097    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
    10971098    ] (dpi2 … pr) in
    1098   foldi … f_trans (f_graph def) init'.
     1099  let def ≝ foldi … f_trans (f_graph def) init' in
     1100  mk_joint_internal_function ??
     1101    (joint_if_luniverse … def)
     1102    (joint_if_runiverse … def)
     1103    (joint_if_result … def)
     1104    (joint_if_params … def)
     1105    stack_size' stack_size'
     1106    (joint_if_code … def)
     1107    (joint_if_entry … def).
    10991108(* TODO *) cases daemon
    11001109qed.
     
    11111120    ?.
    11121121@hide_prf @transform_prog_funct_names qed.
     1122
     1123definition rtlabs_stack_cost : RTLabs_program → stack_cost_model ≝
     1124λp.list_map_opt … (λi_f.
     1125  match \snd i_f with [ Internal def ⇒ Some ? 〈\fst i_f, f_stacksize def〉
     1126                      | External _ ⇒ None ?]) (prog_funct … p).
     1127
     1128lemma RTLabsToRTL_monotone_stacksizes :
     1129∀cost,p_in.let p_out ≝ rtlabs_to_rtl cost p_in in
     1130stack_cost_model_le (rtlabs_stack_cost p_in) (stack_cost ? p_out).
     1131#cost #p_in whd
     1132@list_map_opt_All2
     1133[ @(λid_def1,id_def2.
     1134   match \snd id_def1 with
     1135   [ Internal f1 ⇒
     1136     match \snd id_def2 with
     1137     [ Internal f2 ⇒
     1138       \fst id_def1 = \fst id_def2 ∧
     1139       le (f_stacksize … f1) (joint_if_stacksize … f2)
     1140     | _ ⇒ False
     1141     ]
     1142   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     1143   ])
     1144| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     1145  ** #H %{H} % ]
     1146@All2_of_map * #id * #f normalize nodelta [2: %]
     1147% [%] whd in match translate_internal; normalize nodelta
     1148cases (initialize_locals_params_ret ?????) normalize nodelta #a #b %1
     1149qed.
  • src/RTLabs/RTLabsToRTLAxiom.ma

    r3096 r3145  
    2020include "RTLabs/MeasurableToStructured.ma". (* for make_ext_initial_state *)
    2121
    22 definition RTLabsToRTLstacksizes_ok : (ident → option ℕ) → RTLabs_program → Prop ≝
    23 λstack_sizes,p.
    24 All …
    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).
     22definition RTLabsToRTLstacksizes_ok : RTLabs_program → stack_cost_model → Prop ≝
     23λp.stack_cost_model_le (rtlabs_stack_cost p).
    3124
    3225axiom RTLabsToRTL_ok :
    33 ∀stacksizes : ident → option ℕ.
     26∀stack_model : stack_cost_model.
    3427∀cost.
    3528∀p_in : RTLabs_program.
    36 RTLabsToRTLstacksizes_ok stacksizes p_in
     29RTLabsToRTLstacksizes_ok p_in stack_model
    3730let p_out ≝ rtlabs_to_rtl cost p_in in
     31let stacksizes ≝ stack_sizes stack_model in
    3832∀init_in.make_ext_initial_state p_in = OK … init_in →
    3933∃init_out : state_pc RTL_semantics_separate.
Note: See TracChangeset for help on using the changeset viewer.