include "RTL/RTL_semantics.ma".
include "joint/Traces.ma".
include "common/stacksize.ma".
include "common/StatusSimulation.ma".

definition extract_call_ud_from_ft ≝
  λS : abstract_status.λs1,s2.λft :flat_trace S s1 s2.
  extract_call_ud_from_observables … (ft_observables … ft).

definition good_stack_usage_ft_tlr :
  ∀pars, p, stacksizes.
  ∀st1,st2,st3 : joint_status pars p stacksizes.
  ∀f.
  ∀ft : flat_trace … st1 st2.trace_label_return … st2 st3 →
  make_initial_state … (mk_prog_params pars p stacksizes) = return st1 →
  ft_current_function … ft = Some ? f → Prop ≝
  λpars, p, stacksizes.λst1,st2,st3,f.λft,tlr,st1_prf,f_prf.
  le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0)
    (extract_call_ud_from_ft … ft @ extract_call_ud_from_tlr … tlr f ))) (2^16 - globals_stacksize … p).

(*
definition good_stack_usage_tll :
  ∀p, stacksizes.∀fl.
  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
  ident → trace_label_label … fl st1 st2 → Prop ≝
  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tll.
  ∀m : ℕ.m < 2^16 →
  let info ≝ mk_stacksize_info (stack_usage … st1) m in
  let info' ≝ update_stacksize_info stacksizes info
    (extract_call_ud_from_tll … tll curr_id) in
  maximum info' < 2^16.

definition extract_call_ud_from_tal :
  ∀S,fl,st1,st2.trace_any_label fl S st1 st2 → ident → list call_ud ≝
λS,fl,st1,st2,tal,curr.
  extract_call_ud_from_observables … (observables_trace_any_label … tal curr).

definition good_stack_usage_tal :
  ∀p, stacksizes.∀fl.
  ∀st1,st2 : joint_status RTL_semantics_separate p stacksizes.
  ident → trace_any_label … fl st1 st2 → Prop ≝
  λp, stacksizes,fl.λst1,st2 : state_pc RTL_semantics_separate.λcurr_id,tal.
  ∀m : ℕ.m < 2^16 →
  let info ≝ mk_stacksize_info (stack_usage … st1) m in
  let info' ≝ update_stacksize_info stacksizes info
    (extract_call_ud_from_tal … tal curr_id) in
  maximum info' < 2^16.
*)

axiom RTL_separate_to_overflow_produce_ft_and_tlr :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
∀fn.∀st1,st1',st1'' : state_pc RTL_semantics_separate.
∀ft1 : flat_trace S1 st1 st1'.
∀tlr1 : trace_label_return S1 st1' st1''.
∀st1_prf,fn_prf.
good_stack_usage_ft_tlr … fn ft1 tlr1 st1_prf fn_prf →
tlr_unrepeating … tlr1 →
ft_and_tlr S2 (ft_observables … ft1) (observables_trace_label_return … tlr1 fn) fn st1.

(*
axiom RTL_separate_to_overflow_produce_tlr :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
∀curr_id : ident.
∀tlr : trace_label_return S1 s1 s2.
good_stack_usage_tlr … curr_id tlr →
trace_label_return S2 s1 s2.

axiom RTL_separate_to_overflow_produce_tll :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
∀curr_id : ident.
∀tll : trace_label_label S1 fl s1 s2.
good_stack_usage_tll … curr_id tll →
trace_label_label S2 fl s1 s2.

axiom RTL_separate_to_overflow_produce_tal :
∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
∀p_in : rtl_program.
let S1 ≝ joint_status RTL_semantics_separate p_in stacksizes in
let S2 ≝ joint_status RTL_semantics_separate_overflow p_in stacksizes in
∀fl.∀s1,s2 : state_pc RTL_semantics_separate. (* s1,s2 : state_pc RTL_semantics_separate_overflow too *)
∀curr_id : ident.
∀tal : trace_any_label S1 fl s1 s2.
good_stack_usage_tal … curr_id tal →
trace_any_label S2 fl s1 s2.
*)