source: src/RTL/RTL_separate_to_overflow.ma @ 3255

Last change on this file since 3255 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 4.1 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_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).
20
21(*
22definition good_stack_usage_tll :
23  ∀p, stacksizes.∀fl.
24  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
25  ident → trace_label_label … fl st1 st2 → Prop ≝
26  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tll.
27  ∀m : ℕ.m < 2^16 →
28  let info ≝ mk_stacksize_info (stack_usage … st1) m in
29  let info' ≝ update_stacksize_info stacksizes info
30    (extract_call_ud_from_tll … tll curr_id) in
31  maximum info' < 2^16.
32
33definition extract_call_ud_from_tal :
34  ∀S,fl,st1,st2.trace_any_label fl S st1 st2 → ident → list call_ud ≝
35λS,fl,st1,st2,tal,curr.
36  extract_call_ud_from_observables … (observables_trace_any_label … tal curr).
37
38definition good_stack_usage_tal :
39  ∀p, stacksizes.∀fl.
40  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
41  ident → trace_any_label … fl st1 st2 → Prop ≝
42  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tal.
43  ∀m : ℕ.m < 2^16 →
44  let info ≝ mk_stacksize_info (stack_usage … st1) m in
45  let info' ≝ update_stacksize_info stacksizes info
46    (extract_call_ud_from_tal … tal curr_id) in
47  maximum info' < 2^16.
48*)
49
50axiom RTL_separate_to_overflow_produce_ft_and_tlr :
51∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
52∀p_in : rtl_program.
53let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
54let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
55∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate.
56∀ft1 : flat_trace S1 st1 st1'.
57∀tlr1 : trace_label_return S1 st1' st1''.
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.
62
63(*
64axiom RTL_separate_to_overflow_produce_tlr :
65∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
66∀p_in : rtl_program.
67let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
68let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
69∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
70∀curr_id : ident.
71∀tlr : trace_label_return S1 s1 s2.
72good_stack_usage_tlr … curr_id tlr →
73trace_label_return S2 s1 s2.
74
75axiom RTL_separate_to_overflow_produce_tll :
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∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
81∀curr_id : ident.
82∀tll : trace_label_label S1 fl s1 s2.
83good_stack_usage_tll … curr_id tll →
84trace_label_label S2 fl s1 s2.
85
86axiom RTL_separate_to_overflow_produce_tal :
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∀tal : trace_any_label S1 fl s1 s2.
94good_stack_usage_tal … curr_id tal →
95trace_any_label S2 fl s1 s2.
96*)
Note: See TracBrowser for help on using the repository browser.