| 1 | include "RTL/RTL_semantics.ma". |
|---|
| 2 | include "joint/Traces.ma". |
|---|
| 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. |
|---|
| 20 | |
|---|
| 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 | |
|---|
| 32 | definition good_stack_usage_tll : |
|---|
| 33 | ∀p, stacksizes.∀fl. |
|---|
| 34 | ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes. |
|---|
| 35 | ident → trace_label_label … fl st1 st2 → Prop ≝ |
|---|
| 36 | λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tll. |
|---|
| 37 | ∀m : ℕ.m < 2^16 → |
|---|
| 38 | let info ≝ mk_stacksize_info (stack_usage … st1) m in |
|---|
| 39 | let info' ≝ update_stacksize_info stacksizes info |
|---|
| 40 | (extract_call_ud_from_tll … tll curr_id) in |
|---|
| 41 | maximum info' < 2^16. |
|---|
| 42 | |
|---|
| 43 | definition extract_call_ud_from_tal : |
|---|
| 44 | ∀S,fl,st1,st2.trace_any_label fl S st1 st2 → ident → list call_ud ≝ |
|---|
| 45 | λS,fl,st1,st2,tal,curr. |
|---|
| 46 | extract_call_ud_from_observables … (observables_trace_any_label … tal curr). |
|---|
| 47 | |
|---|
| 48 | definition good_stack_usage_tal : |
|---|
| 49 | ∀p, stacksizes.∀fl. |
|---|
| 50 | ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes. |
|---|
| 51 | ident → trace_any_label … fl st1 st2 → Prop ≝ |
|---|
| 52 | λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tal. |
|---|
| 53 | ∀m : ℕ.m < 2^16 → |
|---|
| 54 | let info ≝ mk_stacksize_info (stack_usage … st1) m in |
|---|
| 55 | let info' ≝ update_stacksize_info stacksizes info |
|---|
| 56 | (extract_call_ud_from_tal … tal curr_id) in |
|---|
| 57 | maximum info' < 2^16. |
|---|
| 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 | (* |
|---|
| 75 | axiom RTL_separate_to_overflow_produce_tlr : |
|---|
| 76 | ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) |
|---|
| 77 | ∀p_in : rtl_program. |
|---|
| 78 | let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in |
|---|
| 79 | let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in |
|---|
| 80 | ∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *) |
|---|
| 81 | ∀curr_id : ident. |
|---|
| 82 | ∀tlr : trace_label_return S1 s1 s2. |
|---|
| 83 | good_stack_usage_tlr … curr_id tlr → |
|---|
| 84 | trace_label_return S2 s1 s2. |
|---|
| 85 | |
|---|
| 86 | axiom RTL_separate_to_overflow_produce_tll : |
|---|
| 87 | ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) |
|---|
| 88 | ∀p_in : rtl_program. |
|---|
| 89 | let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in |
|---|
| 90 | let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in |
|---|
| 91 | ∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *) |
|---|
| 92 | ∀curr_id : ident. |
|---|
| 93 | ∀tll : trace_label_label S1 fl s1 s2. |
|---|
| 94 | good_stack_usage_tll … curr_id tll → |
|---|
| 95 | trace_label_label S2 fl s1 s2. |
|---|
| 96 | |
|---|
| 97 | axiom RTL_separate_to_overflow_produce_tal : |
|---|
| 98 | ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) |
|---|
| 99 | ∀p_in : rtl_program. |
|---|
| 100 | let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in |
|---|
| 101 | let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in |
|---|
| 102 | ∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *) |
|---|
| 103 | ∀curr_id : ident. |
|---|
| 104 | ∀tal : trace_any_label S1 fl s1 s2. |
|---|
| 105 | good_stack_usage_tal … curr_id tal → |
|---|
| 106 | trace_any_label S2 fl s1 s2. |
|---|
| 107 | *) |
|---|
