source: src/ERTLptr/ERTLptrToLTLAxiom.ma @ 3008

Last change on this file since 3008 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: 1003 bytes
Line 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8(* Inefficient, replace with Trie lookup *)
9definition lookup_stack_cost ≝
10 λp.λid : ident.
11  assoc_list_lookup ? ℕ id (eq_identifier …) p.
12
13axiom ERTLptrToLTL_ok :
14∀fix_comp : fixpoint_computer.
15∀colour : coloured_graph_computer.
16∀p_in : ertlptr_program.
17let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
18(* what should we do with n? *)
19let stacksizes ≝ lookup_stack_cost m in
20∃[1] R.
21  status_simulation
22    (joint_status ERTLptr_semantics p_in stacksizes)
23    (joint_status LTL_semantics p_out stacksizes)
24    R ∧
25  ∀init_in.make_initial_state
26    (mk_prog_params ERTLptr_semantics p_in stacksizes) = OK … init_in →
27  ∃init_out.
28    make_initial_state
29     (mk_prog_params LTL_semantics p_out stacksizes) =
30      OK ? init_out ∧
31   R init_in init_out.
Note: See TracBrowser for help on using the repository browser.