Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
Require Import Errors RTL BTL BTLmatchRTL.


Local Open Scope lazy_bool_scope.

Local Open Scope option_monad_scope.

Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
  match rl with
  | nil => true
  | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
  end.

Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
  match or with None => true | Some r => Regset.mem r alive end.

Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) :=
  match ros with inl r => Regset.mem r alive | inr s => true end.

(* NB: definition following [regmap_setres] in [RTL.step] semantics *)
Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
  match res with
  | BR r => Regset.add r alive
  | _ => alive
  end.

Definition exit_checker (btl: code) (alive: Regset.t) (s: node): option unit :=
  SOME next <- btl!s IN
  ASSERT Regset.subset next.(input_regs) alive IN
  Some tt.

Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool :=
   match l with
   | nil => true
   | s :: l' => exit_checker btl alive s &&& exit_list_checker btl alive l'
   end.

Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit :=
  match fin with
  | Bgoto s =>
      exit_checker btl alive s
  | Breturn oreg =>
      ASSERT reg_option_mem oreg alive IN Some tt
  | Bcall _ ros args res s =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      exit_checker btl (Regset.add res alive) s
  | Btailcall _ ros args =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN Some tt
  | Bbuiltin _ args res s =>
      ASSERT list_mem (params_of_builtin_args args) alive IN
      exit_checker btl (reg_builtin_res res alive) s
  | Bjumptable arg tbl =>
      ASSERT Regset.mem arg alive IN
      ASSERT exit_list_checker btl alive tbl IN Some tt
  end.

(* This definition is the meet (infimum) subset of alive registers,
   used for conditions by the below checker.
   A None argument represents the neutral element for intersection. *)
Definition meet (o1 o2: option Regset.t): option Regset.t :=
  match o1, o2 with
  | None, _ => o2
  | _, None => o1
  | Some alive1, Some alive2 => Some (Regset.inter alive1 alive2)
  end.

Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (option Regset.t) :=
  match ib with
  | Bseq ib1 ib2 =>
      SOME oalive1 <- body_checker btl ib1 alive IN
      SOME alive1 <- oalive1 IN
      body_checker btl ib2 alive1
  | Bnop _ => Some (Some alive)
  | Bop _ args dest _ =>
      ASSERT list_mem args alive IN
      Some (Some (Regset.add dest alive))
  | Bload _ _ _ args dest _ =>
      ASSERT list_mem args alive IN
      Some (Some (Regset.add dest alive))
  | Bstore _ _ args src _ =>
      ASSERT Regset.mem src alive IN
      ASSERT list_mem args alive IN
      Some (Some alive)
  | Bcond _ args ib1 ib2 _ =>
      ASSERT list_mem args alive IN
      SOME oalive1 <- body_checker btl ib1 alive IN
      SOME oalive2 <- body_checker btl ib2 alive IN
      Some (meet oalive1 oalive2)
  | BF fin _ =>
      SOME _ <- final_inst_checker btl alive fin IN
      Some None
  end.

(* This definition simply convert the result in an option unit *)
Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit :=
  SOME _ <- body_checker btl ib alive IN Some tt.

Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
  match l with
  | nil => true
  | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l'
  end.

Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
Proof.
  destruct o; simpl; intuition. 
  - eauto.
  - firstorder. try_simplify_someHyps.
Qed.

Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
Proof.
   intros; rewrite lazy_and_Some_true; firstorder.
   destruct x; auto.
Qed.

Lemma list_iblock_checker_correct btl l:
  list_iblock_checker btl l = true ->
  forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt.
Proof.
  intros CHECKER e H; induction l as [|(n & ibf) l]; intuition.
  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.

Definition liveness_checker_bool (f: BTL.function): bool :=
  f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)).

Definition liveness_checker (f: BTL.function): res unit :=
  match liveness_checker_bool f with
  | true => OK tt
  | false => Error (msg "BTL_Livecheck: liveness_checker failed")
  end.

Lemma decomp_liveness_checker f:
  liveness_checker f = OK tt ->
  exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\
  list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true.
Proof.
  intros LIVE; unfold liveness_checker in LIVE.
  destruct liveness_checker_bool eqn:EQL; try congruence.
  clear LIVE. unfold liveness_checker_bool in EQL.
  rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST].
  eexists; split; eauto.
Qed.

Lemma liveness_checker_correct f n ibf:
  liveness_checker f = OK tt ->
  f.(fn_code)!n = Some ibf ->
  iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt.
Proof.
  intros LIVE PC.
  apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
  exploit list_iblock_checker_correct; eauto.
  - eapply PTree.elements_correct; eauto.
  - simpl; auto.
Qed.

Lemma liveness_checker_entrypoint f:
  liveness_checker f = OK tt ->
  f.(fn_code)!(f.(fn_entrypoint)) <> None.
Proof.
  intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
  unfold not; intros CONTRA. congruence.
Qed.

Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.

Inductive liveness_ok_fundef: fundef -> Prop :=
  | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f)
  | liveness_ok_External ef: liveness_ok_fundef (External ef).


Local Notation ext alive := (fun r => Regset.In r alive).

Definition ext_opt (oalive: option Regset.t): Regset.elt -> Prop :=
  match oalive with
  | Some alive => ext alive
  | None => fun _ => True
  end.

Lemma ext_opt_meet: forall r oalive1 oalive2,
  ext_opt (meet oalive1 oalive2) r ->
  ext_opt oalive1 r /\ ext_opt oalive2 r.
Proof.
  intros. destruct oalive1, oalive2;
  simpl in *; intuition.
  eapply Regset.inter_1; eauto.
  eapply Regset.inter_2; eauto.
Qed.

Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
  destruct (Pos.eq_dec r1 r2).
  - subst. intuition; eapply Regset.add_1; auto.
  - intuition. 
    * right. eapply Regset.add_3; eauto.
    * eapply Regset.add_2; auto.
Qed.

Local Hint Resolve Regset.mem_2 Regset.subset_2: core.

Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
Proof.
  destruct b1; simpl; intuition.
Qed.

Lemma list_mem_correct (rl: list reg) (alive: Regset.t):
  list_mem rl alive = true -> forall r, List.In r rl -> ext alive r.
Proof.
  induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto.
Qed.

Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
 forall r, (alive r) -> rs1#r = rs2#r.

Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v).
Proof.
  unfold eqlive_reg; intros EQLIVE r0 ALIVE.
  destruct (Pos.eq_dec r r0) as [H|H].
  - subst. rewrite! Regmap.gss. auto.
  - rewrite! Regmap.gso; auto.
Qed.

Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) ->  eqlive_reg alive1 rs1 rs2.
Proof.
  unfold eqlive_reg; intuition.
Qed.

Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args.
Proof.
  induction args; simpl; auto.
  intros EQLIVE ALIVE; rewrite IHargs; auto.
  unfold eqlive_reg in EQLIVE.
  rewrite EQLIVE; auto.
Qed.

Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args.
Proof.
  intros; eapply eqlive_reg_list; eauto.
  intros; eapply list_mem_correct; eauto.
Qed.

Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
  | eqlive_stackframes_intro ibf res f sp pc rs1 rs2
      (LIVE: liveness_ok_function f)
      (ENTRY: f.(fn_code)!pc = Some ibf)
      (EQUIV: forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
       eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). 

Inductive eqlive_states: state -> state -> Prop :=
  | eqlive_states_intro 
      ibf st1 st2 f sp pc rs1 rs2 m
      (STACKS: list_forall2 eqlive_stackframes st1 st2)
      (LIVE: liveness_ok_function f)
      (PATH: f.(fn_code)!pc = Some ibf)
      (EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2):
      eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m)
  | eqlive_states_call st1 st2 f args m
      (LIVE: liveness_ok_fundef f)
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Callstate st1 f args m) (Callstate st2 f args m)
  | eqlive_states_return st1 st2 v m
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).

Section FSEM_SIMULATES_CFGSEM.

Variable prog: BTL.program.

Let ge := Genv.globalenv prog.

Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f.

Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.

Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val,
  eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v ->
  res <> r -> Regset.In r alive ->
  rs1 # r = rs2 # r.
Proof.
  intros v REGS NRES INR. unfold eqlive_reg in REGS.
  specialize REGS with r. apply REGS in INR.
  rewrite !Regmap.gso in INR; auto.
Qed.

Lemma find_funct_liveness_ok v fd:
  Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd.
Proof.
  unfold Genv.find_funct.
  destruct v; try congruence.
  destruct (Integers.Ptrofs.eq_dec _ _); try congruence.
  eapply all_fundef_liveness_ok; eauto.
Qed.

Lemma find_function_liveness_ok ros rs f:
  find_function ge ros rs = Some f -> liveness_ok_fundef f.
Proof.
  destruct ros as [r|i]; simpl.
  - intros; eapply find_funct_liveness_ok; eauto.
  - destruct (Genv.find_symbol ge i); try congruence.
    eapply all_fundef_liveness_ok; eauto.
Qed.

Lemma find_function_eqlive alive ros rs1 rs2:
  eqlive_reg (ext alive) rs1 rs2 ->
  reg_sum_mem ros alive = true ->
  find_function ge ros rs1 = find_function ge ros rs2.
Proof.
  intros EQLIVE.
  destruct ros; simpl; auto.
  intros H; erewrite (EQLIVE r); eauto.
Qed.

Lemma exit_checker_eqlive (btl: code) (alive: Regset.t) (pc: node) rs1 rs2:
  exit_checker btl alive pc = Some tt ->
  eqlive_reg (ext alive) rs1 rs2 -> 
  exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2.
Proof.
  unfold exit_checker.
  inversion_SOME next.
  inversion_ASSERT. try_simplify_someHyps.
  repeat (econstructor; eauto).
  intros; eapply eqlive_reg_monotonic; eauto.
  intros; exploit Regset.subset_2; eauto.
Qed.

Lemma exit_list_checker_eqlive (btl: code) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n,
  exit_list_checker btl alive tbl = true ->  
  eqlive_reg (ext alive) rs1 rs2 -> 
  list_nth_z tbl n = Some pc ->
  exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2.
Proof.
  induction tbl; simpl.
  - intros; try congruence.
  - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn.
    * try_simplify_someHyps; intuition.
      exploit exit_checker_eqlive; eauto.
    * intuition. eapply IHtbl; eauto.
Qed.

Lemma exit_checker_eqlive_update (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2:
  exit_checker btl (Regset.add r alive) pc = Some tt ->  
  eqlive_reg (ext alive) rs1 rs2 ->
  exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)).
Proof.
  unfold exit_checker.
  inversion_SOME next.
  inversion_ASSERT. try_simplify_someHyps.
  repeat (econstructor; eauto).
  intros; eapply eqlive_reg_update; eauto.
  eapply eqlive_reg_monotonic; eauto.
  intros r0 [X1 X2]; exploit Regset.subset_2; eauto.
  rewrite regset_add_spec. intuition subst.
Qed.

Lemma exit_checker_eqlive_builtin_res (btl: code) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg):
  exit_checker btl (reg_builtin_res res alive) pc = Some tt ->
  eqlive_reg (ext alive) rs1 rs2 ->
  exists ibf, btl!pc = Some ibf /\ (forall vres, eqlive_reg (ext ibf.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)).
Proof.
  destruct res; simpl.
  - intros; exploit exit_checker_eqlive_update; eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (ibf & PC & REGS).
    eexists; intuition eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (ibf & PC & REGS).
    eexists; intuition eauto.
Qed.

Local Hint Resolve in_or_app: local.
Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs:
  eqlive_reg alive rs1 rs2 ->
  Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs ->
  (forall r, List.In r (params_of_builtin_args args) -> alive r) ->
  Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs.
Proof.
  unfold Events.eval_builtin_args.
  intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl.
  { econstructor; eauto. }
  intro X. 
  assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2).
  { eapply eqlive_reg_monotonic; eauto with local. }
  lapply IHEVALL; eauto with local.
  clear X IHEVALL; intro X. econstructor; eauto.
  generalize X1; clear EVALL X1 X.
  induction EVAL1; simpl; try (econstructor; eauto; fail).
  - intros X1; erewrite X1; [ econstructor; eauto | eauto ].
  - intros; econstructor.
    + eapply IHEVAL1_1; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
    + eapply IHEVAL1_2; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
  - intros; econstructor.
    + eapply IHEVAL1_1; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
    + eapply IHEVAL1_2; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
Qed.

Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2
  (PC: (fn_code f) ! pc = Some ibf)
  (REGS: eqlive_reg (ext (input_regs ibf)) rs1 rs2)
  :eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1)
    (tr_inputs f (pc :: tbl) None rs2).
Proof.
  unfold eqlive_reg. intros r INR.
  unfold tid. rewrite tr_inputs_get.
  simpl. rewrite PC.
  exploit Regset.union_3. eapply INR.
  intros INRU. eapply Regset.mem_1 in INRU.
  erewrite INRU; eauto.
Qed.

Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2
  (REGS1: eqlive_reg (ext alive) rs1 rs2)
  (EXIT_LIST: exit_list_checker (fn_code f) alive tbl = true)
  (LIST: list_nth_z tbl n = Some pc)
  (PC: (fn_code f) ! pc = Some ibf)
  (REGS2: eqlive_reg (ext (input_regs ibf)) rs1 rs2),
  eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1)
    (tr_inputs f tbl None rs2).
Proof.
  induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps.
  autodestruct; try_simplify_someHyps.
  - intros; eapply tr_inputs_eqlive_None; eauto.
  - rewrite lazy_and_Some_tt_true in EXIT_LIST.
    destruct EXIT_LIST as [EXIT EXIT_REM].
    intros. unfold eqlive_reg. intros r INR.
    exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto.
    unfold tid. rewrite !tr_inputs_get.
    exploit exit_checker_eqlive; eauto.
    intros (ibf' & PC' & REGS3).
    simpl; rewrite PC'. autodestruct.
    + intro INRU. apply Regset.mem_2 in INRU.
      intros EQR. eapply Regset.union_2 in INRU.
      eapply Regset.mem_1 in INRU. erewrite INRU; auto.
    + intros. autodestruct.
      rewrite (REGS2 r); auto.
Qed.

Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res
  (PC: (fn_code f) ! pc = Some ibf)
  :forall (v: val)
    (REGS: eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v),
  eqlive_reg (ext (input_regs ibf))
    (tid f (pc :: nil) (Some res) rs1) # res <- v
    (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v.
Proof.
  intros. apply eqlive_reg_update.
  unfold eqlive_reg. intros r (NRES & INR).
  unfold tid. rewrite tr_inputs_get.
  simpl. rewrite PC. assert (NRES': res <> r) by auto.
  clear NRES. exploit Regset.union_3. eapply INR.
  intros INRU. exploit Regset.remove_2; eauto.
  intros INRU_RES. eapply Regset.mem_1 in INRU_RES.
  erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto.
Qed.

Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core.
Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2
  (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s)
  (LIVE: liveness_ok_function f)
  (REGS: eqlive_reg (ext alive) rs1 rs2)
  (FCHK: final_inst_checker (fn_code f) alive fin = Some tt)
  (STACKS: list_forall2 eqlive_stackframes stk1 stk2)
  :exists s',
    final_step tr_inputs ge stk2 f sp rs2 m fin t s'
    /\ eqlive_states s s'.
Proof.
  destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros.
  - (* Bgoto *)
    eexists; split.
    + econstructor; eauto.
    + exploit exit_checker_eqlive; eauto.
      intros (ibf & PC & REGS').
      econstructor; eauto.
  - (* Breturn *)
    eexists; split. econstructor; eauto.
    destruct or; simpl in *;
    try erewrite (REGS r); eauto.
  - (* Bcall *)
    exploit exit_checker_eqlive_update; eauto.
    intros (ibf & PC & REGS').
    eexists; split.
    + econstructor; eauto.
      erewrite <- find_function_eqlive; eauto.
    + erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
      eapply find_function_liveness_ok; eauto.
  - (* Btailcall *)
    eexists; split.
    + econstructor; eauto.
      erewrite <- find_function_eqlive; eauto.
    + erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
      eapply find_function_liveness_ok; eauto.
  - (* Bbuiltin *)
    exploit exit_checker_eqlive_builtin_res; eauto.
    intros (ibf & PC & REGS').
    eexists; split.
    + econstructor; eauto.
      eapply eqlive_eval_builtin_args; eauto.
      intros; eapply list_mem_correct; eauto.
    + repeat (econstructor; simpl; eauto).
      unfold regmap_setres. destruct res; simpl in *; eauto.
  - (* Bjumptable *)
    exploit exit_list_checker_eqlive; eauto.
    intros (ibf & PC & REGS').
    eexists; split.
    + econstructor; eauto.
      erewrite <- REGS; eauto.
    + repeat (econstructor; simpl; eauto).
      apply (tr_inputs_eqlive_list_None tbl f pc' (Int.unsigned n) alive ibf rs1 rs2);
      auto.
Qed.

Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'
  (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None)
  alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2)
  (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)),
  exists rs2',
    iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' None)
    /\ eqlive_reg (ext_opt oalive2) rs1' rs2'.
Proof.
  induction ib; intros; try_simplify_someHyps;
  repeat inversion_ASSERT; intros; inv ISTEP.
  - (* Bnop *)
    inv BDY; eauto.
  - (* Bop *)
    erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps; intros.
    repeat econstructor.
    apply eqlive_reg_update.
    eapply eqlive_reg_monotonic; eauto.
    intros r0; rewrite regset_add_spec. 
    intuition.
  - (* Bload *)
    erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps; intros.
    destruct trap; inv LOAD;
    rewrite EVAL, LOAD0 || (autodestruct; try rewrite LOAD0; auto).
    all:
      repeat econstructor;
      apply eqlive_reg_update;
      eapply eqlive_reg_monotonic; eauto;
      intros r0; rewrite regset_add_spec; 
      intuition.
  - (* Bstore *)
    erewrite <- eqlive_reg_listmem; eauto.
    rewrite <- (REGS src); auto.
    try_simplify_someHyps; intros.
    rewrite STORE; eauto.
  - (* Bseq continue *)
    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
    generalize BDY; clear BDY.
    inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE.
    exploit IHib1; eauto.
    intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl.
    eapply IHib2; eauto.
  - (* Bcond *)
    generalize BDY; clear BDY.
    inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN.
    erewrite <- eqlive_reg_listmem; eauto.
    rewrite EVAL.
    destruct b; [ exploit IHib1; eauto | exploit IHib2; eauto].
    all:
      intros (rs2' & ISTEP1 & REGS1);
      econstructor; split; eauto; inv JOIN;
      eapply eqlive_reg_monotonic; eauto;
      intros r EXTM; apply ext_opt_meet in EXTM; intuition.
Qed.

Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' fin
  (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' (Some fin))
  (FSTEP: final_step tid ge stk1 f sp rs1' m' fin t s)
  alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2)
  (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2))
  (LIVE: liveness_ok_function f)
  (STACKS: list_forall2 eqlive_stackframes stk1 stk2),
  exists rs2' s',
    iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin))
    /\ final_step tr_inputs ge stk2 f sp rs2' m' fin t s'
    /\ eqlive_states s s'.
Proof.
  induction ib; simpl; try_simplify_someHyps;
  repeat inversion_ASSERT; intros; inv ISTEP.
  - (* BF *)
    generalize BDY; clear BDY.
    inversion_SOME x; try_simplify_someHyps; intros FCHK.
    destruct x; exploit cfgsem2fsem_finalstep_simu; eauto.
    intros (s2 & FSTEP' & STATES); eauto.
  - (* Bseq stop *)
    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
    generalize BDY; clear BDY.
    inversion_SOME aliveMid. intros OALIVE BDY2. inv OALIVE.
    exploit IHib1; eauto. intros (rs2' & s' & ISTEP1 & FSTEP1 & STATES).
    rewrite ISTEP1; simpl.
    do 2 eexists; intuition eauto.
  - (* Bseq continue *)
    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
    generalize BDY; clear BDY.
    inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE.
    exploit cfgsem2fsem_ibistep_simu_None; eauto.
    intros (rs2' & ISTEP1 & REGS'). rewrite ISTEP1; simpl; eauto.
  - (* Bcond *)
    generalize BDY; clear BDY.
    inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN.
    erewrite <- eqlive_reg_listmem; eauto. rewrite EVAL.
    destruct b; eauto.
Qed.

Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
  iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 ->
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
  liveness_ok_function f ->
  (fn_code f) ! pc = Some ibf ->
  exists s2 : state,
    iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m ibf.(entry) t s2 /\
    eqlive_states s1 s2.
Proof.
  intros STEP STACKS EQLIVE LIVE PC.
  assert (CHECKER: liveness_ok_function f) by auto.
  unfold liveness_ok_function in CHECKER.
  apply decomp_liveness_checker in CHECKER; destruct CHECKER as [ibf' [ENTRY LIST]].
  eapply PTree.elements_correct in PC as PCIN.
  eapply list_iblock_checker_correct in LIST as IBC; eauto.
  unfold iblock_checker in IBC. generalize IBC; clear IBC.
  inversion_SOME alive; intros BODY _.
  destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP).
  exploit cfgsem2fsem_ibistep_simu_Some; eauto.
  intros (rs2' & s' & ISTEP' & FSTEP' & REGS).
  rewrite <- iblock_istep_run_equiv in ISTEP'. clear ISTEP.
  unfold iblock_step. repeat eexists; eauto.
Qed.

Local Hint Constructors step: core.

Lemma cfgsem2fsem_step_simu s1 s1' t s2:
  step tid (Genv.globalenv prog) s1 t s1' ->
  eqlive_states s1 s2 ->
  exists s2' : state,
    step tr_inputs (Genv.globalenv prog) s2 t s2' /\
    eqlive_states s1' s2'.
Proof.
  destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES.
  - (* iblock *)
    inv STATES; simplify_someHyps.
    intros.
    exploit cfgsem2fsem_ibstep_simu; eauto.
    intros (s2 & STEP2 & EQUIV2). 
    eexists; split; eauto.
  - (* function internal *)
    inv STATES; inv LIVE.
    apply liveness_checker_entrypoint in H0 as ENTRY.
    destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto.
    eexists; split; repeat econstructor; eauto.
  - (* function external *)
    inv STATES; inv LIVE; eexists; split; econstructor; eauto.
  - (* return *)
    inv STATES.
    inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS.
    inv STACK.
    exists (State s2 f sp pc (rs2 # res <- vres) m); split.
    * apply exec_return.
    * eapply eqlive_states_intro; eauto.
Qed.

Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
Proof.
  eapply forward_simulation_step with eqlive_states; simpl; eauto.
  - destruct 1, f; intros; eexists; intuition eauto;
    repeat (econstructor; eauto).
  - intros s1 s2 r STATES FINAL; destruct FINAL.
    inv STATES; inv STACKS; constructor.
  - intros. eapply cfgsem2fsem_step_simu; eauto.
Qed.

End FSEM_SIMULATES_CFGSEM.