include "ASM/Interpret2.ma".
include "common/FlatTraces.ma".

lemma OC_class_to_uncosted' : ∀loc.
let S ≝ OC_abstract_status loc in
∀st,cl.as_classify S st = cl →
match cl with
[ cl_other ⇒ True | _ ⇒ ¬as_costed … st ].
#loc #st #cl * @OC_class_to_uncosted qed.

lemma status_class_dep_match_elim'' :
∀A : Type[0].∀P : A → Prop.∀Q : status_class → Type[0].
∀c_return,c_jump,c_call,c_tailcall,c_other.
∀cl.∀d : Q cl.
(cl = cl_return → ∀d' : Q cl_return.d' ≃ d → P (c_return d')) →
(cl = cl_jump → ∀d' : Q cl_jump.d' ≃ d →P (c_jump d')) →
(cl = cl_call → ∀d' : Q cl_call.d' ≃ d →P (c_call d')) →
(cl = cl_tailcall → ∀d' : Q cl_tailcall.d' ≃ d →P (c_tailcall d')) →
(cl = cl_other → ∀d' : Q cl_other.d' ≃ d → P (c_other d')) →
P (match cl return λcl.Q cl → A with
   [ cl_return ⇒ c_return
   | cl_jump ⇒ c_jump
   | cl_call ⇒ c_call
   | cl_tailcall ⇒ c_tailcall
   | cl_other ⇒ c_other
   ] d).
#A #P #Q #c1 #c2 #c3 #c4 #c5 * /2 by / qed.

lemma execute_plus : ∀n1,n2,cm,s.execute (n1+n2) cm s = execute n2 cm (execute n1 cm s).
#n1 elim n1 -n1 [//] #n1 #IH #n2 #cm #s whd in match (S ? + ?); whd in ⊢ (??%?);
>IH % qed.

lemma OC_ft_to_execute :
∀p : labelled_object_code.
∀st1,st2 : Status (cm p).∀ft : flat_trace (OC_abstract_status p) st1 st2.
execute (ft_length … ft) ? st1 = st2.
#p #st1 #st2 #ft elim ft -st2
[ % ]
#st2 #st3 #pre * #no_result #ex #ncost #IH
change with (1 + ?) in match (ft_length ????);
>commutative_plus >execute_plus >IH @ex
qed.

lemma OC_ft_to_exec :
∀p : labelled_object_code.
∀st1,st2 : Status (cm p).∀ft : flat_trace (OC_abstract_status p) st1 st2.
let C ≝ OC_preclassified_system p in
let g ≝ make_global … C p in
let C' ≝ pcs_to_cs C g in
∃tr.
exec_steps (ft_length … ft) io_out io_in C' g st1 = return 〈tr, st2〉 ∧
intensional_trace_of_trace C' [ ] tr = ft_stack_observables … ft.
#p #st1 #st2 #ft elim ft -st2 normalize nodelta
[ %{[ ]} % % ]
#st2 #st3 #pre whd in ⊢ (%→?); * #no_result #EQ_ex #cost * #tr * #H1 #H2
%{(tr @ [ 〈st2, ?〉 ])}
[2:
% whd in match (ft_length ????);
[ cut (∀n.S n = n + 1) [//] #aux >aux -aux
  @(exec_steps_join … H1) whd in ⊢ (??%?);
  change with (OC_result p st2)
    in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? ])?);
  >no_result in ⊢ (??%?); normalize nodelta 
  >m_return_bind >EQ_ex in ⊢ (??%?); %
] |*: ]
>int_trace_append' @pair_elim' @pair_elim'
>H2 whd in match (intensional_trace_of_trace ???);
@pair_elim' normalize nodelta
whd in match (intensional_state_change ???);
@status_class_dep_match_elim''
change with (as_classify (OC_abstract_status p) st2) in ⊢ (??%?→?); #cl
[4: cases (absurd ? cl (OC_exclude_tailcall …)) ]
#callee #callee_eq
@sym_eq
whd in match (ft_stack_observables ????); @pair_elim' normalize nodelta
>(status_class_dep_match_rewrite … cl) normalize nodelta
lapply (OC_class_to_uncosted' … cl) normalize nodelta
[2,4: #_ @eq_f @eq_f >append_nil cases (as_label ? st2) // ]
#ncost >(not_costed_no_label … ncost) >append_nil
cases (\fst (ft_stack_observables … pre)) [2,4: #f #stack' ]
normalize nodelta [ % |3: >append_nil % ]
cases (? : callee I = as_call_ident … «st2, cl») try %
lapply callee_eq whd in match (cs_callee ??);
change with (as_classify (OC_abstract_status p) st2) in
  ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?)?→?);
change with (λprf.as_call_ident ? «st2, (λ_.?) prf») in
  ⊢ (????%→?); generalize in  ⊢ (????(λ_.??(????(%?)))→?);
lapply (refl ? (match as_classify … st2 with [ cl_call ⇒ True | _ ⇒ False ]))
try >cl in ⊢ (??%?→?); * #f #EQ' >EQ' %
qed.

axiom OC_tlr_to_execute :
∀p : labelled_object_code.
∀st1,st2 : Status (cm p).∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
execute (tlr_length … tlr) ? st1 = st2.

axiom OC_tlr_to_exec :
∀p : labelled_object_code.
∀st1,st2 : Status (cm p).∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
let C ≝ OC_preclassified_system p in
let g ≝ make_global … C p in
let C' ≝ pcs_to_cs C g in
∀f,stack.
∃tr.
exec_steps (tlr_length … tlr) io_out io_in C' g st1 = return 〈tr, st2〉 ∧
intensional_trace_of_trace C' (f :: stack) tr =
 〈stack, observables_trace_label_return … tlr f〉.

lemma OC_traces_to_observables :
∀p : labelled_object_code.
let init ≝ initialise_status … (cm p) in
∀st1,st2 : Status (cm p).
∀ft : flat_trace (OC_abstract_status p) init st1.
∀tlr : trace_label_return (OC_abstract_status p) st1 st2.
∀fn.ft_current_function … ft = Some ? fn →
let C ≝ OC_preclassified_system p in
observables C p (ft_length … ft) (tlr_length … tlr) =
  return 〈ft_observables … ft, observables_trace_label_return … tlr fn〉.
#p #st1 #st2 #ft #tlr #fn #EQ_fn
whd
cases (OC_ft_to_exec … ft) #tr1 * #exec1 #eq_tr1
letin stack ≝ (tail … (\fst (ft_stack_observables … ft)))
cut (\fst (ft_stack_observables … ft) = fn :: tail … (\fst (ft_stack_observables … ft)))
[ lapply EQ_fn whd in ⊢ (??%?→?); whd in match ft_stack; normalize nodelta
  cases (\fst (ft_stack_observables … ft)) normalize
  [2: #f' #stack ] #EQ destruct % ] #EQ_stack
cases (OC_tlr_to_exec … tlr fn stack) #tr2 * #exec2 #eq_tr2

whd in match observables; normalize nodelta >m_return_bind
>exec1 >m_return_bind >exec2 >m_return_bind
>eq_tr1 @pair_elim' >EQ_stack
>eq_tr2 %
qed.