source: src/RTL/RTL_separate_to_overflow.ma @ 2946

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

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 3.2 KB
Line 
1include "RTL/RTL_semantics.ma".
2include "joint/Traces.ma".
3include "common/stacksize.ma".
4
5definition good_stack_usage_tlr :
6  ∀p, stacksizes.
7  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
8  ident → trace_label_return … st1 st2 → Prop ≝
9  λp, stacksizes.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tlr.
10  ∀m : ℕ.m < 2^16 →
11  let info ≝ mk_stacksize_info (stack_usage … st1) m in
12  let info' ≝ update_stacksize_info stacksizes info
13    (extract_call_ud_from_tlr … tlr curr_id) in
14  maximum info' < 2^16.
15
16definition good_stack_usage_tll :
17  ∀p, stacksizes.∀fl.
18  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
19  ident → trace_label_label … fl st1 st2 → Prop ≝
20  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tll.
21  ∀m : ℕ.m < 2^16 →
22  let info ≝ mk_stacksize_info (stack_usage … st1) m in
23  let info' ≝ update_stacksize_info stacksizes info
24    (extract_call_ud_from_tll … tll curr_id) in
25  maximum info' < 2^16.
26
27definition extract_call_ud_from_tal :
28  ∀S,fl,st1,st2.trace_any_label fl S st1 st2 → ident → list call_ud ≝
29λS,fl,st1,st2,tal,curr.
30  extract_call_ud_from_observables … (observables_trace_any_label … tal curr).
31
32definition good_stack_usage_tal :
33  ∀p, stacksizes.∀fl.
34  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
35  ident → trace_any_label … fl st1 st2 → Prop ≝
36  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tal.
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_tal … tal curr_id) in
41  maximum info' < 2^16.
42
43axiom RTL_separate_to_overflow_produce_tlr :
44∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
45∀p_in : rtl_program.
46let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
47let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
48∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
49∀curr_id : ident.
50∀tlr : trace_label_return S1 s1 s2.
51good_stack_usage_tlr … curr_id tlr →
52trace_label_return S2 s1 s2.
53
54axiom RTL_separate_to_overflow_produce_tll :
55∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
56∀p_in : rtl_program.
57let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
58let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
59∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
60∀curr_id : ident.
61∀tll : trace_label_label S1 fl s1 s2.
62good_stack_usage_tll … curr_id tll →
63trace_label_label S2 fl s1 s2.
64
65axiom RTL_separate_to_overflow_produce_tal :
66∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
67∀p_in : rtl_program.
68let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
69let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
70∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
71∀curr_id : ident.
72∀tal : trace_any_label S1 fl s1 s2.
73good_stack_usage_tal … curr_id tal →
74trace_any_label S2 fl s1 s2.
75
76
77
78
Note: See TracBrowser for help on using the repository browser.