RTLpathLivegenproof.v

(** Proofs of the liveness properties from the liveness checker of RTLpathLivengen.
*)


Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath RTLpathLivegen.
Require Import Bool Errors Linking Values Events.
Require Import Program.

Definition match_prog (p: RTL.program) (tp: program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

Section PRESERVATION.

Variables prog: RTL.program.
Variables tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.
Let tge := Genv.globalenv (RTLpath.transf_program tprog).

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL).
  apply (Genv.find_symbol_match (match_prog_RTL tprog)).
Qed.

Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_preserved: Senv.equiv ge tge.
Proof.
  eapply senv_transitivity. { eapply (Genv.senv_match TRANSL). }
  eapply RTLpath.senv_preserved.
Qed.

Lemma function_ptr_preserved v f: Genv.find_funct_ptr ge v = Some f -> 
  exists tf, Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros; apply (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.


Lemma function_ptr_RTL_preserved v f: Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some f.
Proof.
  intros; exploit function_ptr_preserved; eauto.
  intros (tf & Htf & TRANS).
  exploit (Genv.find_funct_ptr_match (match_prog_RTL tprog)); eauto.
  intros (cunit & tf0 & X & Y & DUM); subst.
  unfold tge. rewrite X. 
  exploit transf_fundef_correct; eauto. 
  intuition subst; auto.
Qed.

Lemma find_function_preserved ros rs fd:
  RTL.find_function ge ros rs = Some fd -> RTL.find_function tge ros rs = Some fd.
Proof.
  intros H; assert (X: exists tfd, find_function tpge ros rs = Some tfd /\ fd = fundef_RTL tfd). 
  * destruct ros; simpl in * |- *.
    + intros; exploit (Genv.find_funct_match TRANSL); eauto.
      intros (cuint & tf & H1 & H2 & H3); subst; repeat econstructor; eauto.
      exploit transf_fundef_correct; eauto. 
      intuition auto.
    + rewrite <- (Genv.find_symbol_match TRANSL) in H.
    unfold tpge. destruct (Genv.find_symbol _ i); simpl; try congruence.
    exploit function_ptr_preserved; eauto.
    intros (tf & H1 & H2); subst; repeat econstructor; eauto.
    exploit transf_fundef_correct; eauto. 
    intuition auto.
 * destruct X as (tf & X1 & X2); subst.
   eapply find_function_RTL_match; eauto.
Qed.


Local Hint Resolve symbols_preserved senv_preserved: core.

Lemma transf_program_RTL_correct: 
  forward_simulation (RTL.semantics prog) (RTL.semantics (RTLpath.transf_program tprog)).
Proof.
  eapply forward_simulation_step with (match_states:=fun (s1 s2:RTL.state) => s1=s2); simpl; eauto.
  - eapply senv_preserved.
  - (* initial states *)
    intros s1 INIT. destruct INIT as [b f m0 ge0 INIT SYMB PTR SIG]. eexists; intuition eauto.
    econstructor; eauto.
    + intros; eapply (Genv.init_mem_match (match_prog_RTL tprog)). apply (Genv.init_mem_match TRANSL); auto.
    + rewrite symbols_preserved. 
      replace (prog_main (RTLpath.transf_program tprog)) with (prog_main prog).
      * eapply SYMB.
      * erewrite (match_program_main (match_prog_RTL tprog)). erewrite (match_program_main TRANSL); auto.
    + exploit function_ptr_RTL_preserved; eauto.
  - intros; subst; auto.
  - intros s t s2 STEP s1 H; subst.
    eexists; intuition.
    destruct STEP. 
    + (* Inop *) eapply exec_Inop; eauto.
    + (* Iop *) eapply exec_Iop; eauto.
      erewrite eval_operation_preserved; eauto.
    + (* Iload *) eapply exec_Iload; eauto. 
     erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Istore *) eapply exec_Istore; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Icall *)
        eapply RTL.exec_Icall; eauto.
        eapply find_function_preserved; eauto.
    + (* Itailcall *)
        eapply RTL.exec_Itailcall; eauto.
        eapply find_function_preserved; eauto.
    + (* Ibuiltin *)
      eapply RTL.exec_Ibuiltin; eauto.
      * eapply eval_builtin_args_preserved; eauto.
      * eapply external_call_symbols_preserved; eauto.
    + (* Icond *)
      eapply exec_Icond; eauto.
    + (* Ijumptable *)
      eapply RTL.exec_Ijumptable; eauto.
    + (* Ireturn *)
      eapply RTL.exec_Ireturn; eauto.
    + (* exec_function_internal *)
      eapply RTL.exec_function_internal; eauto.
    + (* exec_function_external *)
      eapply RTL.exec_function_external; eauto.
      eapply external_call_symbols_preserved; eauto.
    + (* exec_return *)
      eapply RTL.exec_return; eauto.
Qed.

Theorem transf_program_correct: 
  forward_simulation (RTL.semantics prog) (RTLpath.semantics tprog).
Proof.
  eapply compose_forward_simulations.
  + eapply transf_program_RTL_correct.
  + eapply RTLpath_complete.
Qed.


(* Properties used in hypothesis of [RTLpathLiveproofs.step_eqlive] theorem *)
Theorem all_fundef_liveness_ok b f:
  Genv.find_funct_ptr tpge b = Some f -> liveness_ok_fundef f.
Proof.
  unfold match_prog, match_program in TRANSL.
  unfold Genv.find_funct_ptr, tpge; simpl; intro X.
  destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence.
  destruct y as [tf0|]; try congruence.
  inversion X as [H1]. subst. clear X.
  remember (@Gfun fundef unit f) as f2.
  destruct H as [ctx' f1 f2 H0|]; try congruence.
  inversion Heqf2 as [H2]. subst; clear Heqf2.
  exploit transf_fundef_correct; eauto.
  intuition.
Qed.

End PRESERVATION.

Local Open Scope lazy_bool_scope.
Local Open Scope option_monad_scope.

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

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.

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

Lemma eqlive_reg_refl alive rs: eqlive_reg alive rs rs.
Proof.
  unfold eqlive_reg; auto.
Qed.

Lemma eqlive_reg_symmetry alive rs1 rs2: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs1.
Proof.
  unfold eqlive_reg; intros; symmetry; auto.
Qed.

Lemma eqlive_reg_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs3 -> eqlive_reg alive rs1 rs3.
Proof.
  unfold eqlive_reg; intros H0 H1 r H. rewrite H0; eauto.
Qed.

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_triv rs1 rs2: (forall r, rs1#r = rs2#r) <-> eqlive_reg (fun _ => True) rs1 rs2.
Proof.
  unfold eqlive_reg; intuition.
Qed.

Lemma eqlive_reg_triv_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> (forall r, rs2#r = rs3#r) -> eqlive_reg alive rs1 rs3.
Proof.
  rewrite eqlive_reg_triv; intros; eapply eqlive_reg_trans; eauto.
  eapply eqlive_reg_monotonic; eauto.
  simpl; eauto.
Qed.

Local Hint Resolve Regset.mem_2 Regset.subset_2.

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.

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.

Record eqlive_istate alive (st1 st2: istate): Prop :=
   { eqlive_continue: icontinue st1 = icontinue st2;
     eqlive_ipc: ipc st1 = ipc st2;
     eqlive_irs: eqlive_reg alive (irs st1) (irs st2);
     eqlive_imem: (imem st1) = (imem st2) }.

Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: 
  eqlive_reg (ext alive) rs1 rs2 -> 
  iinst_checker pm alive i = Some res -> 
  istep ge i sp rs1 m = Some st1 -> 
  exists st2, istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2.
Proof.
  intros EQLIVE.
  destruct i; simpl; try_simplify_someHyps.
  - (* Inop *)
    repeat (econstructor; eauto).
  - (* Iop *)
    inversion_ASSERT; try_simplify_someHyps.
    inversion_SOME v. intros EVAL.
    erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
    eapply eqlive_reg_update.
    eapply eqlive_reg_monotonic; eauto.
    intros r0; rewrite regset_add_spec. 
    intuition.
  - (* Iload *)
    inversion_ASSERT; try_simplify_someHyps.
    destruct t. (* TODO - simplify that proof ? *)
    + inversion_SOME a0. intros EVAL.
      erewrite <- eqlive_reg_listmem; eauto.
      try_simplify_someHyps.
      inversion_SOME v; try_simplify_someHyps.
      repeat (econstructor; simpl; eauto).
      eapply eqlive_reg_update.
      eapply eqlive_reg_monotonic; eauto.
      intros r0; rewrite regset_add_spec.
      intuition.
    + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
      destruct (eval_addressing _ _ _ _).
      * destruct (Memory.Mem.loadv _ _ _).
        ** intros. inv H1. repeat (econstructor; simpl; eauto).
           eapply eqlive_reg_update.
           eapply eqlive_reg_monotonic; eauto.
           intros r0; rewrite regset_add_spec.
           intuition.
        ** intros. inv H1. repeat (econstructor; simpl; eauto).
           eapply eqlive_reg_update.
           eapply eqlive_reg_monotonic; eauto.
           intros r0; rewrite regset_add_spec.
           intuition.
      * intros. inv H1. repeat (econstructor; simpl; eauto).
        eapply eqlive_reg_update.
        eapply eqlive_reg_monotonic; eauto.
        intros r0; rewrite regset_add_spec.
        intuition.
  - (* Istore *)
    (repeat inversion_ASSERT); try_simplify_someHyps.
    inversion_SOME a0. intros EVAL.
    erewrite <- eqlive_reg_listmem; eauto.
    rewrite <- (EQLIVE r); auto.
    inversion_SOME v; try_simplify_someHyps.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
  - (* Icond *)
    inversion_ASSERT.
    inversion_SOME b. intros EVAL.
    intros ARGS; erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
    exploit exit_checker_res; eauto.
    intro; subst; simpl. auto.
Qed.

Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: 
  iinst_checker pm alive i = Some res ->
  istep ge i sp rs m = Some st ->
  icontinue st = true ->
  (snd res)=(ipc st).
Proof.
  intros; exploit iinst_checker_default_succ; eauto.
  erewrite istep_normal_exit; eauto.
  congruence.
Qed.

Lemma exit_checker_eqlive A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res rs1 rs2:
  exit_checker pm alive pc v = Some res ->  
  eqlive_reg (ext alive) rs1 rs2 -> 
  exists path, pm!pc = Some path /\ eqlive_reg (ext path.(input_regs)) rs1 rs2.
Proof.
  unfold exit_checker.
  inversion_SOME path.
  inversion_ASSERT. try_simplify_someHyps.
  repeat (econstructor; eauto).
  intros; eapply eqlive_reg_monotonic; eauto.
  intros; exploit Regset.subset_2; eauto.
Qed.

Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1: 
  eqlive_reg (ext alive) rs1 rs2 -> 
  istep ge i sp rs1 m = Some st1 ->
  iinst_checker pm alive i = Some res -> 
  icontinue st1 = false ->
  exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
Proof.
  intros EQLIVE.
  set (tmp := istep ge i sp rs2).
  destruct i; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
  1-3: explore_destruct; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
  (* Icond *)
  unfold tmp; clear tmp; simpl.
  intros EVAL; erewrite <- eqlive_reg_listmem; eauto.
  try_simplify_someHyps.
  destruct b eqn:EQb; simpl in * |-; try congruence.
  intros; exploit exit_checker_eqlive; eauto.
  intros (path & PATH & EQLIVE2).
  repeat (econstructor; simpl; eauto).
Qed.

Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, 
  eqlive_reg (ext alive) rs1 rs2 ->
  ipath_checker ps f pm alive pc = Some res ->
  isteps ge ps f sp rs1 m pc = Some st1 ->
  icontinue st1 = true ->
  exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2.
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps.
  - repeat (econstructor; simpl; eauto).
  - inversion_SOME i; try_simplify_someHyps.
    inversion_SOME res0.
    inversion_SOME st0.
    intros.
    exploit iinst_checker_eqlive; eauto.
    destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
    try_simplify_someHyps.
    rewrite <- CONT, <- MEM, <- PC.
    destruct (icontinue st0) eqn:CONT'.
    * intros; exploit iinst_checker_istep_continue; eauto.
      rewrite <- PC; intros X; rewrite X in * |-. eauto.
    * try_simplify_someHyps.
      congruence.
Qed.

Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, 
  ipath_checker ps f pm alive pc = Some res ->
  isteps ge ps f sp rs m pc = Some st ->
  icontinue st = true ->
  (snd res)=(ipc st).
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps.
  inversion_SOME i; try_simplify_someHyps.
  inversion_SOME res0.
  inversion_SOME st0.
  destruct (icontinue st0) eqn:CONT'.
  - intros; exploit iinst_checker_istep_continue; eauto.
    intros EQ; rewrite EQ in * |-; clear EQ; eauto.
  - try_simplify_someHyps; congruence.
Qed.

Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, 
  eqlive_reg (ext alive) rs1 rs2 -> 
  ipath_checker ps f pm alive pc = Some res -> 
  isteps ge ps f sp rs1 m pc = Some st1 -> 
  icontinue st1 = false ->
  exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence.
  inversion_SOME i; try_simplify_someHyps.
  inversion_SOME res0.
  inversion_SOME st0.
  intros.
  destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros.
  * intros; exploit iinst_checker_eqlive; eauto.
    destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
    exploit iinst_checker_istep_continue; eauto.
    intros PC'.
    try_simplify_someHyps.
    rewrite PC', <- CONT, <- MEM, <- PC, CONT'.
    eauto.
  * intros; exploit iinst_checker_eqlive_stopped; eauto.
    intros EQLIVE; generalize EQLIVE; destruct 1 as (path & st2 & PATH & ISTEP & [CONT PC RS MEM]).
    try_simplify_someHyps.
    rewrite <- CONT, <- MEM, <- PC, CONT'.
    try_simplify_someHyps.
Qed.

Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
  | eqlive_stackframes_intro path res f sp pc rs1 rs2
      (LIVE: liveness_ok_function f)
      (PATH: f.(fn_path)!pc = Some path)
      (EQUIV: forall v, eqlive_reg (ext path.(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 
      path st1 st2 f sp pc rs1 rs2 m
      (STACKS: list_forall2 eqlive_stackframes st1 st2)
      (LIVE: liveness_ok_function f)
      (PATH: f.(fn_path)!pc = Some path)
      (EQUIV: eqlive_reg (ext path.(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 LivenessProperties.

Variable prog: program.

Let pge := Genv.globalenv prog.
Let ge := Genv.globalenv (RTLpath.transf_program prog).

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

Lemma find_funct_liveness_ok v fd:
  Genv.find_funct pge 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 pge 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 pge 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 pge ros rs1 = find_function pge ros rs2.
Proof.
  intros EQLIVE.
  destruct ros; simpl; auto.
  intros H; erewrite (EQLIVE r); eauto.
Qed.

Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
  istep ge i sp rs m = Some st -> 
  inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
Proof.
  destruct i; simpl; try congruence. 
Qed.

Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
  exit_checker pm (Regset.add r alive) pc tt = Some tt ->  
  eqlive_reg (ext alive) rs1 rs2 ->
  exists path, pm!pc = Some path /\ (forall v, eqlive_reg (ext path.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)).
Proof.
  unfold exit_checker.
  inversion_SOME path.
  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.

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 exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg):
  exit_checker pm (reg_builtin_res res alive) pc tt = Some tt ->
  eqlive_reg (ext alive) rs1 rs2 ->
  exists path, pm!pc = Some path /\ (forall vres, eqlive_reg (ext path.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)).
Proof.
  destruct res; simpl.
  - intros; exploit exit_checker_eqlive_ext1; eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE).
    eexists; intuition eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE).
    eexists; intuition eauto.
Qed.

Lemma exit_list_checker_eqlive (pm: path_map) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n,
  exit_list_checker pm alive tbl = true ->  
  eqlive_reg (ext alive) rs1 rs2 -> 
  list_nth_z tbl n = Some pc ->
  exists path, pm!pc = Some path /\ eqlive_reg (ext path.(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 inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext alive) rs1 rs2 -> 
  liveness_ok_function f ->
  (fn_code f) ! pc = Some i ->
  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
  inst_checker (fn_path f) alive i = Some tt -> 
  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
  intros STACKS EQLIVE LIVENESS PC; 
  destruct 1 as [i' sp pc rs1 m st1|
                 sp pc rs1 m sig ros args res pc' fd|
                 st1 pc rs1 m sig ros args fd m'|
                 sp pc rs1 m ef args res pc' vargs t vres m'|
                 sp pc rs1 m arg tbl n pc' |
                 st1 pc rs1 m optr m']; 
  try_simplify_someHyps.
  + (* istate *)
    intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
    inversion_SOME res.
    intros.
    destruct (icontinue st1) eqn: CONT.
    - (* CONT => true *)
      exploit iinst_checker_eqlive; eauto.
      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
      repeat (econstructor; simpl; eauto).
      rewrite <- MEM, <- PC2.
      exploit exit_checker_eqlive; eauto.
      intros (path & PATH & EQLIVE2).
      eapply eqlive_states_intro; eauto.
      erewrite <- iinst_checker_istep_continue; eauto.
    - (* CONT => false *)
      intros; exploit iinst_checker_eqlive_stopped; eauto.
      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
      repeat (econstructor; simpl; eauto).
      rewrite <- MEM, <- PC2.
      eapply eqlive_states_intro; eauto.
  + (* Icall *)
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_ext1; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Icall; eauto.
      erewrite <- find_function_eqlive; eauto.
    - erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
      eapply find_function_liveness_ok; eauto.
      repeat (econstructor; eauto).
  + (* Itailcall *)
    repeat inversion_ASSERT. intros.
    eexists; split.
    - eapply exec_Itailcall; eauto.
      erewrite <- find_function_eqlive; eauto.
    - erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
      eapply find_function_liveness_ok; eauto.
  + (* Ibuiltin *)
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_builtin_res; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Ibuiltin; eauto.
      eapply eqlive_eval_builtin_args; eauto.
      intros; eapply list_mem_correct; eauto.
    - repeat (econstructor; simpl; eauto).
  + (* Ijumptable *)
    repeat inversion_ASSERT. intros.
    exploit exit_list_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Ijumptable; eauto.
      erewrite <- EQLIVE; eauto.
    - repeat (econstructor; simpl; eauto).
  + (* Ireturn *)
    repeat inversion_ASSERT. intros.
    eexists; split.
    - eapply exec_Ireturn; eauto.
    - destruct optr; simpl in * |- *.
      * erewrite (EQLIVE r); eauto.
        eapply eqlive_states_return; eauto.
      * eapply eqlive_states_return; eauto.
Qed.

Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
  path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext (input_regs path)) rs1 rs2 ->
  liveness_ok_function f ->
  (fn_path f) ! pc = Some path ->
   exists s2, path_step ge pge (psize path) stk2 f sp rs2 m pc t s2 /\ eqlive_states s1 s2.
Proof.
  intros STEP STACKS EQLIVE LIVE PC.
  unfold liveness_ok_function in LIVE.
  exploit LIVE; eauto.
  unfold path_checker.
  inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *)
  inversion_SOME i; intros PC'.
  destruct STEP as [st ISTEPS CONT|].
  - (* early_exit *)
    intros; exploit ipath_checker_eqlive_stopped; eauto.
    destruct 1 as (path2 & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
    repeat (econstructor; simpl; eauto).
    rewrite <- MEM, <- PC2.
    eapply eqlive_states_intro; eauto.
  - (* normal_exit *)
    intros; exploit ipath_checker_eqlive_normal; eauto.
    destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
    exploit ipath_checker_isteps_continue; eauto.
    intros PC3; rewrite <- PC3, <- PC2 in * |-.
    exploit inst_checker_eqlive; eauto.
    intros (s2 & LAST_STEP & EQLIVE2).
     eexists; split; eauto.
     eapply exec_normal_exit; eauto.
     rewrite <- PC3, <- MEM; auto.
Qed.

Theorem step_eqlive t s1 s1' s2: 
  step ge pge s1 t s1' ->
  eqlive_states s1 s2 ->
  exists s2', step ge pge s2 t s2' /\ eqlive_states s1' s2'.
Proof.
  destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ].
  - intros EQLIVE; inv EQLIVE; simplify_someHyps. 
    intro PATH.
    exploit path_step_eqlive; eauto.
    intros (s2 & STEP2 & EQUIV2). 
    eexists; split; eauto.
    eapply exec_path; eauto.
  - intros EQLIVE; inv EQLIVE; inv LIVE.
    exploit initialize_path. { eapply fn_entry_point_wf. }
    intros (path & Hpath).
    eexists; split.
    * eapply exec_function_internal; eauto.
    * eapply eqlive_states_intro; eauto.
      eapply eqlive_reg_refl.
  - intros EQLIVE; inv EQLIVE.
    eexists; split.
    * eapply exec_function_external; eauto.
    * eapply eqlive_states_return; eauto.
  - intros EQLIVE; inv EQLIVE.
    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.

End LivenessProperties.