RTLpathLivegen: proof of preservation

4 files changed, 294 insertions, 169 deletions

diff --git a/configure b/configure
index da20d0dc..ddcc6619 100755
--- a/configure
+++ b/configure
@@ -849,7 +849,7 @@ ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
 EXECUTE=k1-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __K1C_COS__
 SIMU=k1-cluster -- 
-BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathSE_theory.v\\
+BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v RTLpath.v RTLpathLivegen.v RTLpathSE_theory.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index eced2635..37ee5e70 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -981,7 +981,6 @@ Proof.
     intros (idx' & s2' & H0 & H1).
     eexists; eexists; eauto.
     destruct H0 as [H0|[H0|(path'&H0)]]; intuition subst; eauto.
-    
   - intros; exploit step_noninst_complete; eauto.
     intros (s2' & STEP & (idx0 & MATCH)).
     exists idx0; exists s2'; intuition auto.
diff --git a/mppa_k1c/lib/RTLpathLivegen.v b/mppa_k1c/lib/RTLpathLivegen.v
index ab8a250e..d4ae9290 100644
--- a/mppa_k1c/lib/RTLpathLivegen.v
+++ b/mppa_k1c/lib/RTLpathLivegen.v
@@ -9,13 +9,11 @@ Require Import AST.
 Require Import Op.
 Require Import Registers.
 Require Import Globalenvs Smallstep RTL RTLpath.
-Require Import Bool Errors.
+Require Import Bool Errors Linking Values Events.
 Require Import Program.
 
 Local Open Scope lazy_bool_scope.
 
-Local Notation ext alive := (fun r => Regset.In r alive).
-
 Local Open Scope option_monad_scope.
 
 Axiom build_path_map: RTL.function -> path_map.
@@ -285,195 +283,137 @@ Qed.
 Definition transf_program (p: RTL.program) : res program :=
   transform_partial_program transf_fundef p.
 
-(* TODO: suite à déplacer dans un autre fichier ? *)
-
-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.
-
-(*
-Lemma regset_remove_spec live r1 r2: Regset.In r1 (Regset.remove r2 live) <-> (Regset.In r1 live /\ r1 <> r2).
-Proof.
-  intuition.
-  - eapply Regset.remove_3; eauto.
-  - eapply Regset.remove_1; [| eauto]. auto.
-  - eapply Regset.remove_2; eauto.
-Qed.
+Definition match_prog (p: RTL.program) (tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
 
-Lemma reg_list_live_spec args r: forall live, Regset.In r (reg_list_live args live) <-> List.In r args \/ (Regset.In r live).
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
 Proof.
-  induction args; simpl.
-  + intuition.
-  + intros; rewrite IHargs, regset_add_spec. intuition.
+  intros. eapply match_transform_partial_program_contextual; eauto.
 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.
+Section PRESERVATION.
 
-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.
+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 (program_RTL tprog).
 
-Lemma eqlive_reg_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs3 -> eqlive_reg alive rs1 rs3.
+Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
-  unfold eqlive_reg; intros H0 H1 r H. rewrite H0; eauto.
+  rewrite <- (Genv.find_symbol_match TRANSL).
+  apply (Genv.find_symbol_match (match_prog_RTL tprog)).
 Qed.
 
-Lemma eqlive_reg_notin alive rs r v: ~(alive r) -> eqlive_reg alive rs (rs # r <- v).
+Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
 Proof.
-  unfold eqlive_reg; intros NOTALIVE r0 ALIVE.
-  destruct (Pos.eq_dec r r0) as [H|H].
-  - subst; tauto.
-  - rewrite Regmap.gso; auto.
+  unfold Senv.equiv. intuition congruence.
 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).
+Lemma senv_preserved: Senv.equiv ge tge.
 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.
+  eapply senv_transitivity. { eapply (Genv.senv_match TRANSL). }
+  eapply RTLpath.senv_preserved.
 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.
+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.
-  unfold eqlive_reg; intuition.
+  intros; apply (Genv.find_funct_ptr_transf_partial TRANSL); 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.
+Lemma function_ptr_RTL_preserved v f: Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some f.
 Proof.
-  destruct b1; simpl; intuition.
+  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 list_mem_correct (rl: list reg) (alive: Regset.t):
-  list_mem rl alive = true -> forall r, List.In r rl -> ext alive r.
+Lemma find_function_preserved ros rs fd:
+  RTL.find_function ge ros rs = Some fd -> RTL.find_function tge ros rs = Some fd.
 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.
+  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.
+
+Theorem transf_program_RTL_correct: 
+  forward_simulation (RTL.semantics prog) (RTL.semantics (program_RTL tprog)).
 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.
+  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 (program_RTL 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.
+    + (* 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.
-  intros; eapply eqlive_reg_list; eauto.
-  intros; eapply list_mem_correct; eauto.
+  eapply compose_forward_simulations.
+  + eapply transf_program_RTL_correct.
+  + eapply RTLpath_complete.
 Qed.
 
-
-(* TODO: suite à revoir... *)
-
-Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
-  | eqlive_stackframe_intro path res f sp pc rs1 rs2
-      (PATH: f.(fn_path)!pc = Some path)
-      (LIVE: path_checker f pc path <> None)
-      (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2):
-       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)
-      (PATH: f.(fn_path)!pc = Some path)
-      (LIVE: path_checker f pc path <> None)
-      (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
-      (* TODO: add info on 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
-      (* TODO: add info on f *)
-      (STACKS: list_forall2 eqlive_stackframes st1 st2):
-      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).
-
-(* ESSAIS *)
-
-Section PRESERVATION.
-
-Variable prog: program.
-
-Let pge := Genv.globalenv prog.
-Let ge := Genv.globalenv (program_RTL prog).
-
-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.
-    admit.
-  - intros EQLIVE; inv EQLIVE.
-    eexists; split.
-    * eapply exec_function_internal; eauto.
-    * eapply eqlive_states_intro; eauto.
-Qed.
-
-(*
-path : path_info
-stack : list stackframe
-f : function
-sp : Values.val
-rs : regset
-m : Memory.Mem.mem
-pc : positive
-t : Events.trace
-s : state
-STEP : path_step ge pge (psize path) stack f sp rs m pc t s
-st2 : list stackframe
-rs2 : regset
-STACKS : list_forall2 eqlive_stackframes stack st2
-EQUIV : eqlive_reg (ext (input_regs path)) rs rs2
-LIVE : path_checker f pc path <> None
-PATH : (fn_path f) ! pc = Some path
-______________________________________(1/1)
-exists s2' : state, step ge pge (State st2 f sp pc rs2 m) t s2' /\ eqlive_states s s2'
-*)
-
 End PRESERVATION.
-
-(*
-
-Definition is_live (live: PMap.t Regset.t) (f: RTL.function): Prop 
-  := False.
-
-
-Lemma is_live_eqlive_reg pc' f live pc i rs1 rs2:
-  f.(fn_code)!pc = Some i ->
-  is_live live f ->
-  In pc' (successors_instr i) ->
-  eqlive_reg (ext live#pc) rs1 rs2 ->
-  eqlive_reg (ext (transfer f pc' live#pc')) rs1 rs2.
-Proof.
-  unfold is_live; intro PC; intros.
-  eapply eqlive_reg_monotonic; eauto.
-  eapply Liveness.analyze_solution; eauto.
-Qed.
-
-Ltac exploit_liveness pc' := refine (modusponens _ _ (is_live_eqlive_reg pc' _ _ _ _ _ _ _ _ _ _) _); [ eauto | eauto | try (simpl; intuition) | eauto | eauto].
-
-(* Y aura-t-il besoin de chose comme ça ? *)
-
-*)
\ No newline at end of file
diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v
new file mode 100644
index 00000000..0701c598
--- /dev/null
+++ b/mppa_k1c/lib/RTLpathLiveproofs.v
@@ -0,0 +1,186 @@
+(** Building a RTLpath program with liveness annotation.
+*)
+
+
+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.
+Require Import Program.
+
+
+Local Open Scope lazy_bool_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.
+
+(*
+Lemma regset_remove_spec live r1 r2: Regset.In r1 (Regset.remove r2 live) <-> (Regset.In r1 live /\ r1 <> r2).
+Proof.
+  intuition.
+  - eapply Regset.remove_3; eauto.
+  - eapply Regset.remove_1; [| eauto]. auto.
+  - eapply Regset.remove_2; eauto.
+Qed.
+
+Lemma reg_list_live_spec args r: forall live, Regset.In r (reg_list_live args live) <-> List.In r args \/ (Regset.In r live).
+Proof.
+  induction args; simpl.
+  + intuition.
+  + intros; rewrite IHargs, regset_add_spec. intuition.
+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_notin alive rs r v: ~(alive r) -> eqlive_reg alive rs (rs # r <- v).
+Proof.
+  unfold eqlive_reg; intros NOTALIVE r0 ALIVE.
+  destruct (Pos.eq_dec r r0) as [H|H].
+  - subst; tauto.
+  - rewrite Regmap.gso; auto.
+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.
+
+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.
+
+
+(* TODO: suite à revoir... 
+
+Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
+  | eqlive_stackframe_intro path res f sp pc rs1 rs2
+      (PATH: f.(fn_path)!pc = Some path)
+      (LIVE: path_checker f pc path <> None)
+      (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2):
+       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)
+      (PATH: f.(fn_path)!pc = Some path)
+      (LIVE: path_checker f pc path <> None)
+      (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
+      (* TODO: add info on 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
+      (* TODO: add info on f *)
+      (STACKS: list_forall2 eqlive_stackframes st1 st2):
+      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).
+
+(* ESSAIS *)
+
+Section PRESERVATION.
+
+Variable prog: program.
+
+Let pge := Genv.globalenv prog.
+Let ge := Genv.globalenv (program_RTL prog).
+
+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.
+    admit.
+  - intros EQLIVE; inv EQLIVE.
+    eexists; split.
+    * eapply exec_function_internal; eauto.
+    * eapply eqlive_states_intro; eauto.
+Qed.
+
+(*
+path : path_info
+stack : list stackframe
+f : function
+sp : Values.val
+rs : regset
+m : Memory.Mem.mem
+pc : positive
+t : Events.trace
+s : state
+STEP : path_step ge pge (psize path) stack f sp rs m pc t s
+st2 : list stackframe
+rs2 : regset
+STACKS : list_forall2 eqlive_stackframes stack st2
+EQUIV : eqlive_reg (ext (input_regs path)) rs rs2
+LIVE : path_checker f pc path <> None
+PATH : (fn_path f) ! pc = Some path
+______________________________________(1/1)
+exists s2' : state, step ge pge (State st2 f sp pc rs2 m) t s2' /\ eqlive_states s s2'
+*)
+
+End PRESERVATION.
+*)
\ No newline at end of file