- Timestamp:
- Apr 5, 2013, 6:04:14 PM (8 years ago)
- Location:
- src/RTL
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLToERTLAxiom.ma
r2946 r3096 5 5 include "common/StatusSimulation.ma". 6 6 7 axiom RTL absToRTL_ok :7 axiom RTLToERTL_ok : 8 8 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) 9 9 ∀p_in : rtl_program. 10 10 let p_out ≝ rtl_to_ertl p_in in 11 ∀init_in.make_initial_state 12 (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in → 13 ∃init_out. 14 make_initial_state 15 (mk_prog_params ERTL_semantics p_out stacksizes) = 16 OK ? init_out ∧ 11 17 ∃[1] R. 12 status_simulation 18 status_simulation_with_init 13 19 (joint_status RTL_semantics_unique p_in stacksizes) 14 20 (joint_status ERTL_semantics p_out stacksizes) 15 R ∧ 16 ∀init_in.make_initial_state 17 (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in → 18 ∃init_out. 19 make_initial_state 20 (mk_prog_params ERTL_semantics p_out stacksizes) = 21 OK ? init_out ∧ 22 R init_in init_out. 21 R init_in init_out. -
src/RTL/RTL_overflow_to_unique.ma
r2946 r3096 6 6 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) 7 7 ∀p_in : rtl_program. 8 ∀init_in.make_initial_state 9 (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in → 10 ∃init_out. 11 make_initial_state 12 (mk_prog_params RTL_semantics_unique p_in stacksizes) = 13 OK ? init_out ∧ 8 14 ∃[1] R. 9 status_simulation 15 status_simulation_with_init 10 16 (joint_status RTL_semantics_separate_overflow p_in stacksizes) 11 17 (joint_status RTL_semantics_unique p_in stacksizes) 12 R ∧ 13 ∀init_in.make_initial_state 14 (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in → 15 ∃init_out. 16 make_initial_state 17 (mk_prog_params RTL_semantics_unique p_in stacksizes) = 18 OK ? init_out ∧ 19 R init_in init_out. 18 R init_in init_out. -
src/RTL/RTL_separate_to_overflow.ma
r2946 r3096 2 2 include "joint/Traces.ma". 3 3 include "common/stacksize.ma". 4 include "common/StatusSimulation.ma". 5 6 definition extract_call_ud_from_ft ≝ 7 λS : abstract_status.λs1,s2.λft :flat_trace S s1 s2. 8 extract_call_ud_from_observables … (ft_observables … ft). 9 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. 4 20 5 21 definition good_stack_usage_tlr : … … 41 57 maximum info' < 2^16. 42 58 59 axiom RTL_separate_to_overflow_produce_ft_and_tlr : 60 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) 61 ∀p_in : rtl_program. 62 let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in 63 let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in 64 ∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate. 65 ∀ft1 : flat_trace S1 st1 st1'. 66 ∀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. 73 74 (* 43 75 axiom RTL_separate_to_overflow_produce_tlr : 44 76 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) … … 73 105 good_stack_usage_tal … curr_id tal → 74 106 trace_any_label S2 fl s1 s2. 75 76 77 78 107 *)
Note: See TracChangeset
for help on using the changeset viewer.