source: src/RTL/RTLToERTLAxiom.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: 702 bytes
Line 
1include "RTL/RTLToERTL.ma".
2include "RTL/RTL_semantics.ma".
3include "ERTL/ERTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6
7axiom RTLToERTL_ok :
8∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
9∀p_in : rtl_program.
10let 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 ∧
17∃[1] R.
18  status_simulation_with_init
19    (joint_status RTL_semantics_unique p_in stacksizes)
20    (joint_status ERTL_semantics p_out stacksizes)
21    R init_in init_out.
Note: See TracBrowser for help on using the repository browser.