Changeset 3145 for src/RTL


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (7 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/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r3037 r3145  
    44include "ERTL/ERTL.ma".
    55include "joint/TranslateUtils.ma".
     6include "joint/joint_stacksizes.ma".
    67
    78include alias "basics/lists/list.ma".
     
    384385definition rtl_to_ertl : rtl_program → ertl_program ≝
    385386  b_graph_transform_program … translate_data.
     387
     388lemma RTLToERTL_monotone_stacksizes :
     389∀p_in.let p_out ≝ rtl_to_ertl p_in in
     390stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
     391#p_in whd
     392@list_map_opt_All2
     393[ @(λid_def1,id_def2.
     394   match \snd id_def1 with
     395   [ Internal f1 ⇒
     396     match \snd id_def2 with
     397     [ Internal f2 ⇒
     398       \fst id_def1 = \fst id_def2 ∧
     399       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
     400     | _ ⇒ False
     401     ]
     402   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     403   ])
     404| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     405  ** #H %{H} % ]
     406@All2_of_map * #id * #f normalize nodelta [2: %]
     407% [%]
     408cases (b_graph_translate ?????) #f_out * #data
     409* *[2:#r1*[2:#r2*[2:#r3*[2:#r4*[2:#r5*[2:#r6*[2:#r7*[2:#r8*
     410  [2:#r9*[2:#r10*[2:#r11*[2:#r12*[2:#r13*[2:#r14 #tl]]]]]]]]]]]]]]
     411* #f_lbls * #f_regs * try ( * @False) whd in ⊢ (%→?); #EQ_data
     412#props >(ss_def_out_eq … props) >EQ_data
     413generalize in match (joint_if_stacksize ???); generalize in match (length ??-length ??);
     414-p_in //
     415qed.
  • src/RTL/RTL_separate_to_overflow.ma

    r3096 r3145  
    88  extract_call_ud_from_observables … (ft_observables … ft).
    99
    10 definition good_stack_usage_ft :
    11   ∀p, stacksizes.
    12   ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
    13   flat_trace … st1 st2 → Prop ≝
    14   λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λft.
    15   ∀m : ℕ.m < 2^16
    16   let info ≝ mk_stacksize_info (stack_usage … st1) m in
    17   let info' ≝ update_stacksize_info stacksizes info
    18     (extract_call_ud_from_ft … ft) in
    19   maximum info' < 2^16.
     10definition good_stack_usage_ft_tlr :
     11  ∀pars, p, stacksizes.
     12  ∀st1,st2,st3 : joint_status pars p stacksizes.
     13  ∀f.
     14  ∀ft : flat_trace … st1 st2.trace_label_return … st2 st3 →
     15  make_initial_state … (mk_prog_params pars p stacksizes) = return st1
     16  ft_current_function … ft = Some ? f → Prop ≝
     17  λpars, p, stacksizes.λst1,st2,st3,f.λft,tlr,st1_prf,f_prf.
     18  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
     19    (extract_call_ud_from_ft … ft @ extract_call_ud_from_tlr … tlr f ))) (2^16 - globals_stacksize … p).
    2020
    21 definition good_stack_usage_tlr :
    22   ∀p, stacksizes.
    23   ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
    24   ident → trace_label_return … st1 st2 → Prop ≝
    25   λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tlr.
    26   ∀m : ℕ.m < 2^16 →
    27   let info ≝ mk_stacksize_info (stack_usage … st1) m in
    28   let info' ≝ update_stacksize_info stacksizes info
    29     (extract_call_ud_from_tlr … tlr curr_id) in
    30   maximum info' < 2^16.
    31 
     21(*
    3222definition good_stack_usage_tll :
    3323  ∀p, stacksizes.∀fl.
     
    5646    (extract_call_ud_from_tal … tal curr_id) in
    5747  maximum info' < 2^16.
     48*)
    5849
    5950axiom RTL_separate_to_overflow_produce_ft_and_tlr :
     
    6556∀ft1 : flat_trace S1 st1 st1'.
    6657∀tlr1 : trace_label_return S1 st1' st1''.
    67 good_stack_usage_ft … ft1 →
    68 good_stack_usage_tlr … fn tlr1 →
    69 ∃ft2 : flat_trace S2 st1 st1'.
    70 ∃tlr2 : trace_label_return S2 st1' st1''.
    71 ft_observables … ft1 = ft_observables … ft2 ∧
    72 tlr_rel … tlr1 tlr2.
     58∀st1_prf,fn_prf.
     59good_stack_usage_ft_tlr … fn ft1 tlr1 st1_prf fn_prf →
     60tlr_unrepeating … tlr1 →
     61ft_and_tlr S2 (ft_observables … ft1) (observables_trace_label_return … tlr1 fn) fn st1.
    7362
    7463(*
Note: See TracChangeset for help on using the changeset viewer.