include "common/SmallstepExec.ma".
include "common/IO.ma".

(* Equivalences of execution traces. *)

(* A finite trace is produced by some prefix of an execution. *)

inductive steps (state:Type[0]) : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
| steps_stop : ∀tr,s,r. steps state tr (e_stop … tr s r) (e_stop … tr s r)
| steps_step : ∀tr,s,e. steps state tr (e_step … tr s e) e
| steps_steps : ∀tr,s,e,tr',e'. steps state tr e e' → steps state (tr'⧺tr) (e_step … tr' s e) e'.

(* Go from individual steps to part of an execution trace. *)
lemma plus_exec : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s'.
  plus … FE gl s tr s' →
  is_final … FE gl s' = None ? →
  steps (state … gl) tr
    (exec_inf_aux … FE gl (step … FE gl s))
    (exec_inf_aux … FE gl (step … FE gl s')).
#FE #gl #s0 #tr0 #s0' #P elim P
[ #s1 #tr #s2 #NF1 #EX #NF2 >EX >exec_inf_aux_unfold
  whd in ⊢ (???%?); >NF2
  %2
| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #NF3
  >EX1 >exec_inf_aux_unfold
  whd in ⊢ (???%?); >(plus_not_final … P2) /3/
] qed.

lemma plus_final : ∀FE:fullexec io_out io_in. ∀gl,s,tr,s',r.
  plus … FE gl s tr s' →
  is_final … FE gl s' = Some ? r →
  ∃tr'. steps (state … gl) tr
    (exec_inf_aux … FE gl (step … FE gl s))
    (e_stop … tr' r s'). 
#FE #gl #s0 #tr0 #s0' #r #P elim P
[ #s1 #tr #s2 #NF1 #EX #F2 >EX >exec_inf_aux_unfold
  whd in ⊢ (??(λ_.???%?)); >F2
  %{tr} %1
| #s1 #tr #s2 #tr' #s3 #NF1 #EX1 #P2 #IH #F3
  >EX1 >exec_inf_aux_unfold
  whd in ⊢ (??(λ_.???%?)); >(plus_not_final … P2)
  cases (IH F3) #tr'' #S' %{tr''} /2/
] qed.

(* And similarly for after_n_steps *)

lemma after_inv : ∀FE:fullexec io_out io_in.
 ∀n,g,inv,P,s.
  after_n_steps (S n) … FE g s inv P →
  ∃tr,s'.
    P tr s' ∧
    match is_final ?? FE g s' with
    [ Some r ⇒ ∃tr'.
      steps ? tr (exec_inf_aux … FE g (step … FE g s))
                 (e_stop ??? tr' r s')
    | None ⇒ 
      steps ? tr (exec_inf_aux … FE g (step … FE g s))
                 (exec_inf_aux … FE g (step … FE g s'))
    ].
#FE #n #g #inv #P
(* Rather nasty generalisation *)
#s whd in ⊢ (% → ?); cases (is_final … s) [2: #r * ] whd in ⊢ (% → ?); #AW
cut (∃tr,s'. P (E0⧺tr) s' ∧ ?) [3: #H @H | skip ] 
generalize in match E0 in AW ⊢ %; generalize in match s; -s
elim n
[ #s #tr whd in ⊢ (% → %);
  cases (step … s) [ #o #K * | 3: #m * ]
  * #tr' #s'
  whd in ⊢ (% → ?); cases (inv s') [2: *]
  #AW %{tr'} %{s'} %{AW}
  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
  [ #NF whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF @steps_step
  | #r #F whd %{tr'} >exec_inf_aux_unfold whd in ⊢ (???%?); >F whd in ⊢ (???%?); @steps_stop
  ]
| #n' #IH #s #tr whd in ⊢ (% → ?);
  cases (step … s) [ #o #K * | 3: #m * ] * #tr1 #s1
  whd in ⊢ (% → ?); cases (inv s1) [2: *]
  whd in ⊢ (% → ?); lapply (refl ? (is_final … s1)) cases (is_final … s1) in ⊢ (???% → %);
  [ 2: #r #_ * ] #NF1 whd in ⊢ (% → ?); #AW1
  cases (IH s1 ? AW1)
  #tr' * #s' * #p #H1 %{(tr1⧺tr')} %{s'}
  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
  [ #NF <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (???%?); >NF1
    @steps_steps >NF in H1; //
  | #r #F <Eapp_assoc %{p} whd >exec_inf_aux_unfold whd in ⊢ (??(λ_.???%?)); >NF1
    >F in H1; whd in ⊢ (% → ?); * #tr1 #H1 %{tr1}
    @steps_steps @H1
  ]
] qed.

(* In some places we do not consider wrong executions. *)

coinductive not_wrong (state:Type[0]) : execution state io_out io_in → Prop ≝
| nw_stop : ∀tr,i,s. not_wrong state (e_stop … tr i s)
| nw_step : ∀tr,s,e. not_wrong state e → not_wrong state (e_step … tr s e)
| nw_interact : ∀o,k. (∀i. not_wrong state (k i)) → not_wrong state (e_interact … o k).

lemma not_wrong_not_wrong : ∀state,m.
  ¬ (not_wrong state (e_wrong … m)).
#state #m % #NW inversion NW
#A #B #C #D #E destruct
qed.

lemma not_wrong_steps : ∀state,e,e',tr.
  steps state tr e e' →
  not_wrong state e →
  not_wrong state e'.
#state #e0 #e0' #tr0 #S elim S
[ //
| #tr #s #e #NW inversion NW 
  #A #B #C #D #E try #F destruct //
| #tr #s #e #tr' #e' #S' #IH #NW @IH
  inversion NW 
  #A #B #C #D #E try #F destruct //
] qed.

lemma not_wrong_init : ∀FE,p.
  not_wrong ? (exec_inf … FE p) →
  ∃s. make_initial_state … p = OK ? s.
#FE #p whd in ⊢ (??% → ?);
cases (make_initial_state ??? p)
[ /2/
| normalize #m #NW @⊥
  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
] qed.


(* One execution is simulated by another, but possibly using a different number
   of steps.  Note that we have to allow for several steps at the end to make
   the trace match up.
   
   This assumes that the overall traces are exactly the same; this may not be
   the case everywhere and we might have to add a cost label map.  (There is
   a separate definition for the cost labelling stage, see
   Clight/labelSpecification.ma.)
 *)

coinductive simulates (S1,S2:Type[0]) : execution S1 io_out io_in → execution S2 io_out io_in → Prop ≝
| sim_stop : ∀tr,r,s1,s2,e1,e2,tr1,tr2.
    steps S1 tr e1 (e_stop … tr1 r s1) →
    steps S2 tr e2 (e_stop … tr2 r s2) →
    simulates S1 S2 e1 e2
| sim_steps : ∀tr,e1,e1',e2,e2'.
    steps S1 tr e1 e1' →
    steps S2 tr e2 e2' →
    simulates S1 S2 e1' e2' →
    simulates S1 S2 e1 e2
| sim_interact : ∀o,k1,k2.
    (∀i. simulates S1 S2 (k1 i) (k2 i)) →
    simulates S1 S2 (e_interact … o k1) (e_interact … o k2).


(* Result for lifting simulations on states to simulations on execution traces.
   At the time of writing this hasn't been used in anger yet...
   
   This probably isn't the best route for the stages of the compiler that have
   results in terms of structured traces, but it should be good for the
   front-end.
 *)

let corec build_cofix_simulation
  (FS1,FS2:fullexec io_out io_in)
  (g1:global … FS1) (g2:global … FS2)
  (SIM:state … g1 → state … g2 → Prop)
  (s1:state … g1) (s2:state … g2)
  (NF:is_final … FS1 g1 s1 = None ?)
  (S:SIM s1 s2)
  (SIM_FINAL: ∀x,y. SIM x y → is_final … FS1 g1 x = is_final … FS2 g2 y)
  (SIM_GOOD: ∀x,y. SIM x y →
         not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 x)) →
         is_final … FS1 g1 x = None ? →
         ∃tr,x',y'. And (plus … FS1 g1 x tr x') (And (plus … FS2 g2 y tr y') (SIM x' y')) )
  (NW:not_wrong ? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)))
: simulates ?? (exec_inf_aux … FS1 g1 (step … FS1 g1 s1)) (exec_inf_aux ?? FS2 g2 (step … FS2 g2 s2)) ≝ ?.
lapply (SIM_GOOD … S NW NF)
* #tr * #s1' * #s2' * #P1 * #P2 #S'
lapply (refl ? (is_final … FS1 g1 s1'))
cases (is_final … s1') in ⊢ (???% → ?);
[ #NF1
  @(sim_steps … tr … (build_cofix_simulation … S' SIM_FINAL SIM_GOOD ?))
  [ @(plus_exec … P1) //
  | @(plus_exec … P2) <SIM_FINAL //
  | @(not_wrong_steps … (plus_exec … P1 …)) //
  | //
  ]
| #r #F1
  cases (plus_final … P1 F1) #tr1' #S1
  cases (plus_final … P2 ?) [ 3: <SIM_FINAL [ @F1 | // | skip ] | 2: skip ] #tr2' #S2
  @(sim_stop … S1 S2)
] qed.

theorem lift_simulation : ∀FE1,FE2:fullexec io_out io_in.
  ∀p1:program … FE1.  ∀p2:program … FE2.
  let g1 ≝ make_global … p1 in
  let g2 ≝ make_global … p2 in
  ∀SIM: state … g1 → state … g2 → Prop.
  ∀SIM_INIT: ∀s1. make_initial_state … p1 = OK ? s1 →
             ∃s2. And (make_initial_state … p2 = OK ? s2) (SIM s1 s2).
  ∀SIM_FINAL: ∀x,y. SIM x y → is_final … FE1 g1 x = is_final … FE2 g2 y.
  ∀SIM_GOOD: ∀x,y. SIM x y →
         not_wrong ? (exec_inf_aux … FE1 g1 (step … FE1 g1 x)) →
         is_final … FE1 g1 x = None ? →
         ∃tr,x',y'. And (plus … FE1 g1 x tr x') (And (plus … FE2 g2 y tr y') (SIM x' y')).
  let e1 ≝ exec_inf … FE1 p1 in
  let e2 ≝ exec_inf … FE2 p2 in
  not_wrong … e1 →
  simulates … e1 e2.

#FE1 #FE2 #p1 #p2
letin g1 ≝ (make_global … p1)
letin g2 ≝ (make_global … p2)
#SIM #SIM_INIT #SIM_FINAL #SIM_GOOD
#NW
cases (not_wrong_init … p1 NW)
#s1 #I1
cases (SIM_INIT … I1) #s2 * #I2 #S
whd in NW:(??%) ⊢ (???%%);
>I1 in NW ⊢ %; >I2 whd in ⊢ (??% → ???%%);
change with g1 in match (make_global … p1);
change with g2 in match (make_global … p2);

>exec_inf_aux_unfold whd in ⊢ (??% → ???%?);
lapply (SIM_FINAL … S)
lapply (refl ? (is_final … s1))
cases (is_final … s1) in ⊢ (???% → %);
[ #F1 #F2 >(exec_inf_aux_unfold … FE2) whd in ⊢ (??% → ???%%);
  <F2 whd in ⊢ (? → ???%%); #NW
  @(sim_steps … E0 … (build_cofix_simulation … SIM_FINAL SIM_GOOD …)) try assumption
  [ // | // | inversion NW #A #B #C #D #E try #F destruct assumption ]
| #r #F1 #F2 #NW whd in ⊢ (???%%);
  >exec_inf_aux_unfold whd in ⊢ (???%%);
  <F2 whd in ⊢ (???%%);
  @(sim_stop … (steps_stop …) (steps_stop …))
] qed.