source: src/RTL/RTL_overflow_to_unique.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: 647 bytes
Line 
1include "RTL/RTL_semantics.ma".
2include "joint/Traces.ma".
3include "common/StatusSimulation.ma".
4
5axiom RTL_separate_to_unique_ok :
6∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
7∀p_in : rtl_program.
8∀init_in.make_initial_state
9  (mk_prog_params RTL_semantics_separate_overflow p_in stacksizes) = OK … init_in →
10∃init_out.
11  make_initial_state
12   (mk_prog_params RTL_semantics_unique p_in stacksizes) =
13    OK ? init_out ∧
14∃[1] R.
15  status_simulation_with_init
16    (joint_status RTL_semantics_separate_overflow p_in stacksizes)
17    (joint_status RTL_semantics_unique p_in stacksizes)
18    R init_in init_out.
Note: See TracBrowser for help on using the repository browser.