source: src/RTL/RTL_separate_to_overflow.ma @ 3096

Last change on this file since 3096 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

File size: 4.5 KB
Line 
1include "RTL/RTL_semantics.ma".
2include "joint/Traces.ma".
3include "common/stacksize.ma".
4include "common/StatusSimulation.ma".
5
6definition 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
10definition 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
21definition 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
32definition 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
43definition 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
48definition 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
59axiom RTL_separate_to_overflow_produce_ft_and_tlr :
60∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
61∀p_in : rtl_program.
62let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
63let 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''.
67good_stack_usage_ft … ft1 →
68good_stack_usage_tlr … fn tlr1 →
69∃ft2 : flat_trace S2 st1 st1'.
70∃tlr2 : trace_label_return S2 st1' st1''.
71ft_observables … ft1 = ft_observables … ft2 ∧
72tlr_rel … tlr1 tlr2.
73
74(*
75axiom RTL_separate_to_overflow_produce_tlr :
76∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
77∀p_in : rtl_program.
78let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
79let 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.
83good_stack_usage_tlr … curr_id tlr →
84trace_label_return S2 s1 s2.
85
86axiom RTL_separate_to_overflow_produce_tll :
87∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
88∀p_in : rtl_program.
89let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
90let 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.
94good_stack_usage_tll … curr_id tll →
95trace_label_label S2 fl s1 s2.
96
97axiom RTL_separate_to_overflow_produce_tal :
98∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
99∀p_in : rtl_program.
100let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
101let 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.
105good_stack_usage_tal … curr_id tal →
106trace_any_label S2 fl s1 s2.
107*)
Note: See TracBrowser for help on using the repository browser.