(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Recognition of tail calls: correctness proof *)

Require Import Coqlib Maps Integers AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Registers RTL Conventions Tailcall.

(** * Syntactic properties of the code transformation *)

(** ** Measuring the number of instructions eliminated *)

(** The [return_measure c pc] function counts the number of instructions
  eliminated by the code transformation, where [pc] is the successor
  of a call turned into a tailcall.  This is the length of the
  move/nop/return sequence recognized by the [is_return] boolean function.
*)

Fixpoint return_measure_rec (n: nat) (c: code) (pc: node)
                            {struct n}: nat :=
  match n with
  | O => O
  | S n' =>
      match c!pc with
      | Some(Inop s) => S(return_measure_rec n' c s)
      | Some(Iop op args dst s) => S(return_measure_rec n' c s)
      | _ => O
      end
  end.

Definition return_measure (c: code) (pc: node) :=
  return_measure_rec niter c pc.

Lemma return_measure_bounds:
  forall f pc, (return_measure f pc <= niter)%nat.
Proof.
(* Goal: forall (f : code) (pc : node), le (return_measure f pc) niter *)
  intro f.
(* Goal: forall pc : node, le (return_measure f pc) niter *)
  assert (forall n pc, (return_measure_rec n f pc <= n)%nat).
(* Goal: forall (n : nat) (pc : node), le (return_measure_rec n f pc) n *)
(* Goal: forall pc : node, le (return_measure f pc) niter *)
    induction n; intros; simpl.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    destruct (f!pc); try omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    destruct i; try omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    generalize (IHn n0). omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    generalize (IHn n0). omega.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. unfold return_measure. apply H.
Qed.

Remark return_measure_rec_incr:
  forall f n1 n2 pc,
  (n1 <= n2)%nat ->
  (return_measure_rec n1 f pc <= return_measure_rec n2 f pc)%nat.
Proof.
(* Goal: forall (f : code) (n1 n2 : nat) (pc : node) (_ : le n1 n2), le (return_measure_rec n1 f pc) (return_measure_rec n2 f pc) *)
  induction n1; intros; simpl.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  simpl. destruct f!pc; try omega. destruct i; try omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  generalize (IHn1 n2 n H0). omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  generalize (IHn1 n2 n H0). omega.
Qed.

Lemma is_return_measure_rec:
  forall f n n' pc r,
  is_return n f pc r = true -> (n <= n')%nat ->
  return_measure_rec n f.(fn_code) pc = return_measure_rec n' f.(fn_code) pc.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  induction n; simpl; intros.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  congruence.
(* Goal: @eq nat match @PTree.get instruction pc (fn_code f) with | Some (Inop s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iop op args dst s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iload m a l r n as i) => O | Some (Istore m a l r n as i) => O | Some (Icall s s0 l r n as i) => O | Some (Itailcall s s0 l as i) => O | Some (Ibuiltin e l b n as i) => O | Some (Icond c l n n0 as i) => O | Some (Ijumptable r l as i) => O | Some (Ireturn o as i) => O | None => O end (return_measure_rec O (fn_code f) pc) *)
(* Goal: @eq nat match @PTree.get instruction pc (fn_code f) with | Some (Inop s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iop op args dst s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iload m a l r n as i) => O | Some (Istore m a l r n as i) => O | Some (Icall s s0 l r n as i) => O | Some (Itailcall s s0 l as i) => O | Some (Ibuiltin e l b n as i) => O | Some (Icond c l n n0 as i) => O | Some (Ijumptable r l as i) => O | Some (Ireturn o as i) => O | None => O end (return_measure_rec (S n') (fn_code f) pc) *)
  destruct n'. omegaContradiction. simpl.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  destruct (fn_code f)!pc; try congruence.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  destruct i; try congruence.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  decEq. apply IHn with r. auto. omega.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  destruct (is_move_operation o l); try congruence.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  destruct (Reg.eq r r1); try congruence.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  decEq. apply IHn with r0. auto. omega.
Qed.

(** ** Relational characterization of the code transformation *)

(** The [is_return_spec] characterizes the instruction sequences
  recognized by the [is_return] boolean function.  *)

Inductive is_return_spec (f:function): node -> reg -> Prop :=
  | is_return_none: forall pc r,
      f.(fn_code)!pc = Some(Ireturn None) ->
      is_return_spec f pc r
  | is_return_some: forall pc r,
      f.(fn_code)!pc = Some(Ireturn (Some r)) ->
      is_return_spec f pc r
  | is_return_nop: forall pc r s,
      f.(fn_code)!pc = Some(Inop s) ->
      is_return_spec f s r ->
      (return_measure f.(fn_code) s < return_measure f.(fn_code) pc)%nat ->
      is_return_spec f pc r
  | is_return_move: forall pc r r' s,
      f.(fn_code)!pc = Some(Iop Omove (r::nil) r' s) ->
      is_return_spec f s r' ->
      (return_measure f.(fn_code) s < return_measure f.(fn_code) pc)%nat ->
     is_return_spec f pc r.

Lemma is_return_charact:
  forall f n pc rret,
  is_return n f pc rret = true -> (n <= niter)%nat ->
  is_return_spec f pc rret.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  induction n; intros.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  simpl in H. congruence.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  generalize H. simpl.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  caseEq ((fn_code f)!pc); try congruence.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  intro i. caseEq i; try congruence.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  intros s; intros. eapply is_return_nop; eauto. eapply IHn; eauto. omega.
(* Goal: lt (return_measure (fn_code f) s) (return_measure (fn_code f) pc) *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  unfold return_measure.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite <- (is_return_measure_rec f (S n) niter pc rret); auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite <- (is_return_measure_rec f n niter s rret); auto.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  simpl. rewrite H2. omega. omega.

(* Goal: forall (o : operation) (l : list reg) (r : reg) (n0 : node) (_ : @eq instruction i (Iop o l r n0)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Iop o l r n0))) (_ : @eq bool match @is_move_operation reg o l with | Some src => if Reg.eq rret src then is_return n f n0 r else false | None => false end true), is_return_spec f pc rret *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  intros op args dst s EQ1 EQ2.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  caseEq (is_move_operation op args); try congruence.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  intros src IMO. destruct (Reg.eq rret src); try congruence.
(* Goal: forall _ : @eq bool (is_return n f s dst) true, is_return_spec f pc rret *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  subst rret. intro.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit is_move_operation_correct; eauto. intros [A B]. subst.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  eapply is_return_move; eauto. eapply IHn; eauto. omega.
(* Goal: lt (return_measure (fn_code f) s) (return_measure (fn_code f) pc) *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  unfold return_measure.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite <- (is_return_measure_rec f (S n) niter pc src); auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite <- (is_return_measure_rec f n niter s dst); auto.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  simpl. rewrite EQ2. omega. omega.

(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros or EQ1 EQ2. destruct or; intros.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  assert (r = rret). eapply proj_sumbool_true; eauto. subst r.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply is_return_some; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply is_return_none; auto.
Qed.

(** The [transf_instr_spec] predicate relates one instruction in the
  initial code with its possible transformations in the optimized code. *)

Inductive transf_instr_spec (f: function): instruction -> instruction -> Prop :=
  | transf_instr_tailcall: forall sig ros args res s,
      f.(fn_stacksize) = 0 ->
      is_return_spec f s res ->
      transf_instr_spec f (Icall sig ros args res s) (Itailcall sig ros args)
  | transf_instr_default: forall i,
      transf_instr_spec f i i.

Lemma transf_instr_charact:
  forall f pc instr,
  f.(fn_stacksize) = 0 ->
  transf_instr_spec f instr (transf_instr f pc instr).
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. unfold transf_instr. destruct instr; try constructor.
  caseEq (is_return niter f n r && tailcall_is_possible s &&
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
          opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros.
(* Goal: transf_instr_spec f (Icall s s0 l r n) (Itailcall s s0 l) *)
(* Goal: transf_instr_spec f (Icall s s0 l r n) (Icall s s0 l r n) *)
  destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1).
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply transf_instr_tailcall; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply is_return_charact; eauto.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) m') r *)
  constructor.
Qed.

Lemma transf_instr_lookup:
  forall f pc i,
  f.(fn_code)!pc = Some i ->
  exists i',  (transf_function f).(fn_code)!pc = Some i' /\ transf_instr_spec f i i'.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. unfold transf_function.
(* Goal: @ex instruction (fun i' : instruction => and (@eq (option instruction) (@PTree.get instruction pc (fn_code (if zeq (fn_stacksize f) Z0 then RTL.transf_function (transf_instr f) f else f))) (@Some instruction i')) (transf_instr_spec f i i')) *)
  destruct (zeq (fn_stacksize f) 0).
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  simpl. rewrite PTree.gmap. rewrite H. simpl.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exists (transf_instr f pc i); split. auto. apply transf_instr_charact; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exists i; split. auto. constructor.
Qed.

(** * Semantic properties of the code transformation *)

(** ** The ``less defined than'' relation between register states *)

(** A call followed by a return without an argument can be turned
  into a tail call.  In this case, the original function returns
  [Vundef], while the transformed function can return any value.
  We account for this situation by using the ``less defined than''
  relation between values and between memory states.  We need to
  extend it pointwise to register states. *)

Lemma regs_lessdef_init_regs:
  forall params vl vl',
  Val.lessdef_list vl vl' ->
  regs_lessdef (init_regs vl params) (init_regs vl' params).
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  induction params; intros.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  simpl. red; intros. rewrite Regmap.gi. constructor.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  simpl. inv H.   red; intros. rewrite Regmap.gi. constructor.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply set_reg_lessdef. auto. auto.
Qed.

(** * Proof of semantic preservation *)

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

Lemma transf_program_match:
  forall p, match_prog p (transf_program p).
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. apply match_transform_program; auto.
Qed.

Section PRESERVATION.

Variable prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_transf TRANSL).

Lemma functions_translated:
  forall (v: val) (f: RTL.fundef),
  Genv.find_funct ge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).

Lemma funct_ptr_translated:
  forall (b: block) (f: RTL.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  Genv.find_funct_ptr tge b = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).

Lemma sig_preserved:
  forall f, funsig (transf_fundef f) = funsig f.
Proof.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  destruct f; auto. simpl. unfold transf_function.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  destruct (zeq (fn_stacksize f) 0); auto.
Qed.

Lemma stacksize_preserved:
  forall f, fn_stacksize (transf_function f) = fn_stacksize f.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  unfold transf_function. intros.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  destruct (zeq (fn_stacksize f) 0); auto.
Qed.

Lemma find_function_translated:
  forall ros rs rs' f,
  find_function ge ros rs = Some f ->
  regs_lessdef rs rs' ->
  find_function tge ros rs' = Some (transf_fundef f).
Proof.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  intros until f; destruct ros; simpl.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros.
(* Goal: @eq (option fundef) (@Genv.find_funct fundef unit tge (Regmap.get val r rs')) (@Some fundef (transf_fundef f)) *)
(* Goal: forall (_ : @eq (option fundef) match @Genv.find_symbol fundef unit ge i with | Some b => @Genv.find_funct_ptr fundef unit ge b | None => @None fundef end (@Some fundef f)) (_ : regs_lessdef rs rs'), @eq (option fundef) match @Genv.find_symbol fundef unit tge i with | Some b => @Genv.find_funct_ptr fundef unit tge b | None => @None fundef end (@Some fundef (transf_fundef f)) *)
  assert (rs'#r = rs#r).
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
    exploit Genv.find_funct_inv; eauto. intros [b EQ].
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
    generalize (H0 r). rewrite EQ. intro LD. inv LD. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite H1. apply functions_translated; auto.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  rewrite symbols_preserved. destruct (Genv.find_symbol ge i); intros.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply funct_ptr_translated; auto.
(* Goal: @eq (option fundef) (@None fundef) (@Some fundef (transf_fundef f)) *)
  discriminate.
Qed.

(** Consider an execution of a call/move/nop/return sequence in the
  original code and the corresponding tailcall in the transformed code.
  The transition sequences are of the following form
  (left: original code, right: transformed code).
  [f] is the calling function and [fd] the called function.
<<
     State stk f (Icall instruction)       State stk' f' (Itailcall)

     Callstate (frame::stk) fd args        Callstate stk' fd' args'
            .                                       .
            .                                       .
            .                                       .
     Returnstate (frame::stk) res          Returnstate stk' res'

     State stk f (move/nop/return seq)
            .
            .
            .
     State stk f (return instr)

     Returnstate stk res
>>
The simulation invariant must therefore account for two kinds of
mismatches between the transition sequences:
- The call stack of the original program can contain more frames
  than that of the transformed program (e.g. [frame] in the example above).
- The regular states corresponding to executing the move/nop/return
  sequence must all correspond to the single [Returnstate stk' res']
  state of the transformed program.

We first define the simulation invariant between call stacks.
The first two cases are standard, but the third case corresponds
to a frame that was eliminated by the transformation. *)

Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
  | match_stackframes_nil:
      match_stackframes nil nil
  | match_stackframes_normal: forall stk stk' res sp pc rs rs' f,
      match_stackframes stk stk' ->
      regs_lessdef rs rs' ->
      match_stackframes
        (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
        (Stackframe res (transf_function f) (Vptr sp Ptrofs.zero) pc rs' :: stk')
  | match_stackframes_tail: forall stk stk' res sp pc rs f,
      match_stackframes stk stk' ->
      is_return_spec f pc res ->
      f.(fn_stacksize) = 0 ->
      match_stackframes
        (Stackframe res f (Vptr sp Ptrofs.zero) pc rs :: stk)
        stk'.

(** Here is the invariant relating two states.  The first three
  cases are standard.  Note the ``less defined than'' conditions
  over values and register states, and the corresponding ``extends''
  relation over memory states. *)

Inductive match_states: state -> state -> Prop :=
  | match_states_normal:
      forall s sp pc rs m s' rs' m' f
             (STACKS: match_stackframes s s')
             (RLD: regs_lessdef rs rs')
             (MLD: Mem.extends m m'),
      match_states (State s f (Vptr sp Ptrofs.zero) pc rs m)
                   (State s' (transf_function f) (Vptr sp Ptrofs.zero) pc rs' m')
  | match_states_call:
      forall s f args m s' args' m',
      match_stackframes s s' ->
      Val.lessdef_list args args' ->
      Mem.extends m m' ->
      match_states (Callstate s f args m)
                   (Callstate s' (transf_fundef f) args' m')
  | match_states_return:
      forall s v m s' v' m',
      match_stackframes s s' ->
      Val.lessdef v v' ->
      Mem.extends m m' ->
      match_states (Returnstate s v m)
                   (Returnstate s' v' m')
  | match_states_interm:
      forall s sp pc rs m s' m' f r v'
             (STACKS: match_stackframes s s')
             (MLD: Mem.extends m m'),
      is_return_spec f pc r ->
      f.(fn_stacksize) = 0 ->
      Val.lessdef (rs#r) v' ->
      match_states (State s f (Vptr sp Ptrofs.zero) pc rs m)
                   (Returnstate s' v' m').

(** The last case of [match_states] corresponds to the execution
  of a move/nop/return sequence in the original code that was
  eliminated by the transformation:
<<
     State stk f (move/nop/return seq)  ~~  Returnstate stk' res'
            .
            .
            .
     State stk f (return instr)         ~~  Returnstate stk' res'
>>
  To preserve non-terminating behaviors, we need to make sure
  that the execution of this sequence in the original code cannot
  diverge.  For this, we introduce the following complicated
  measure over states, which will decrease strictly whenever
  the original code makes a transition but the transformed code
  does not. *)

Definition measure (st: state) : nat :=
  match st with
  | State s f sp pc rs m => (List.length s * (niter + 2) + return_measure f.(fn_code) pc + 1)%nat
  | Callstate s f args m => 0%nat
  | Returnstate s v m => (List.length s * (niter + 2))%nat
  end.

Ltac TransfInstr :=
  match goal with
  | H: (PTree.get _ (fn_code _) = _) |- _ =>
      destruct (transf_instr_lookup _ _ _ H) as [i' [TINSTR TSPEC]]; inv TSPEC
  end.

Ltac EliminatedInstr :=
  match goal with
  | H: (is_return_spec _ _ _) |- _ => inv H; try congruence
  | _ => idtac
  end.

(** The proof of semantic preservation, then, is a simulation diagram
  of the ``option'' kind. *)

Lemma transf_step_correct:
  forall s1 t s2, step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1'),
  (exists s2', step tge s1' t s2' /\ match_states s2 s2')
  \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat.
Proof.
  induction 1; intros; inv MS; EliminatedInstr.

- (* nop *)
  TransfInstr. left. econstructor; split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Inop; eauto. constructor; auto.
- (* eliminated nop *)
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  assert (s0 = pc') by congruence. subst s0.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  right. split. simpl. omega. split. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto.

- (* op *)
  TransfInstr.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit eval_operation_lessdef; eauto.
  intros [v' [EVAL' VLD]].
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#res <- v') m'); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Iop; eauto.  rewrite <- EVAL'.
  apply eval_operation_preserved. exact symbols_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto. apply set_reg_lessdef; auto.
- (* eliminated move *)
(* Goal: final_state st2 r *)
  rewrite H1 in H. clear H1. inv H.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  right. split. simpl. omega. split. auto.
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  econstructor; eauto. simpl in H0. rewrite PMap.gss. congruence.

- (* load *)
  TransfInstr.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit eval_addressing_lessdef; eauto.
  intros [a' [ADDR' ALD]].
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit Mem.loadv_extends; eauto.
  intros [v' [LOAD' VLD]].
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Iload with (a := a'). eauto.  rewrite <- ADDR'.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply eval_addressing_preserved. exact symbols_preserved. eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto. apply set_reg_lessdef; auto.

- (* store *)
  TransfInstr.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit eval_addressing_lessdef; eauto.
  intros [a' [ADDR' ALD]].
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit Mem.storev_extends. 2: eexact H1. eauto. eauto. apply RLD.
  intros [m'1 [STORE' MLD']].
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' m'1); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Istore with (a := a'). eauto.  rewrite <- ADDR'.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply eval_addressing_preserved. exact symbols_preserved. eauto.
(* Goal: @eq (option fundef) (@None fundef) (@Some fundef (transf_fundef f)) *)
  destruct a; simpl in H1; try discriminate.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto.

- (* call *)
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit find_function_translated; eauto. intro FIND'.
  TransfInstr.
+ (* call turned tailcall *)
  assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}).
    apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7.
(* Goal: @eq nat match @PTree.get instruction pc (fn_code f) with | Some (Inop s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iop op args dst s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iload m a l r n as i) => O | Some (Istore m a l r n as i) => O | Some (Icall s s0 l r n as i) => O | Some (Itailcall s s0 l as i) => O | Some (Ibuiltin e l b n as i) => O | Some (Icond c l n n0 as i) => O | Some (Ijumptable r l as i) => O | Some (Ireturn o as i) => O | None => O end (return_measure_rec O (fn_code f) pc) *)
(* Goal: @eq nat match @PTree.get instruction pc (fn_code f) with | Some (Inop s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iop op args dst s as i) => S (return_measure_rec n (fn_code f) s) | Some (Iload m a l r n as i) => O | Some (Istore m a l r n as i) => O | Some (Icall s s0 l r n as i) => O | Some (Itailcall s s0 l as i) => O | Some (Ibuiltin e l b n as i) => O | Some (Icond c l n n0 as i) => O | Some (Ijumptable r l as i) => O | Some (Ireturn o as i) => O | None => O end (return_measure_rec (S n') (fn_code f) pc) *)
    red; intros; omegaContradiction.
  destruct X as [m'' FREE].
  left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Itailcall; eauto. apply sig_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. eapply match_stackframes_tail; eauto. apply regs_lessdef_regs; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply Mem.free_right_extends; eauto.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction.
+ (* call that remains a call *)
  left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' :: s')
                          (transf_fundef fd) (rs'##args) m'); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Icall; eauto. apply sig_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. constructor; auto. apply regs_lessdef_regs; auto. auto.

- (* tailcall *)
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit find_function_translated; eauto. intro FIND'.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]].
  TransfInstr.
  left. exists (Callstate s' (transf_fundef fd) (rs'##args) m'1); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Itailcall; eauto. apply sig_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite stacksize_preserved; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. auto.  apply regs_lessdef_regs; auto. auto.

- (* builtin *)
  TransfInstr.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto.
  intros (vargs' & P & Q).
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit external_call_mem_extends; eauto.
  intros [v' [m'1 [A [B [C D]]]]].
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (regmap_setres res v' rs') m'1); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Ibuiltin; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto. apply set_res_lessdef; auto.

- (* cond *)
  TransfInstr.
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Icond; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply eval_condition_lessdef with (rs##args) m; auto. apply regs_lessdef_regs; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor; auto.

- (* jumptable *)
  TransfInstr.
  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' rs' m'); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply exec_Ijumptable; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  generalize (RLD arg). rewrite H0. intro. inv H2. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor; auto.

- (* return *)
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]].
  TransfInstr.
  left. exists (Returnstate s' (regmap_optget or Vundef rs') m'1); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply exec_Ireturn; auto. rewrite stacksize_preserved; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. auto.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  destruct or; simpl. apply RLD. constructor.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  auto.

- (* eliminated return None *)
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  assert (or = None) by congruence. subst or.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  right. split. simpl. omega. split. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. auto.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  simpl. constructor.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply Mem.free_left_extends; eauto.

- (* eliminated return Some *)
(* Goal: is_return_spec f pc rret *)
(* Goal: is_return_spec f pc rret *)
  assert (or = Some r) by congruence. subst or.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  right. split. simpl. omega. split. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor. auto.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  simpl. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply Mem.free_left_extends; eauto.

- (* internal call *)
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit Mem.alloc_extends; eauto.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    instantiate (1 := 0). omega.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
    instantiate (1 := fn_stacksize f). omega.
  intros [m'1 [ALLOC EXT]].
  assert (fn_stacksize (transf_function f) = fn_stacksize f /\
          fn_entrypoint (transf_function f) = fn_entrypoint f /\
          fn_params (transf_function f) = fn_params f).
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
    unfold transf_function. destruct (zeq (fn_stacksize f) 0); auto.
  destruct H0 as [EQ1 [EQ2 EQ3]].
  left. econstructor; split.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite EQ2. rewrite EQ3. constructor; auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  apply regs_lessdef_init_regs. auto.

- (* external call *)
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit external_call_mem_extends; eauto.
  intros [res' [m2' [A [B [C D]]]]].
  left. exists (Returnstate s' res' m2'); split.
(* Goal: @eq signature (funsig (transf_fundef (@Internal function f))) (funsig (@Internal function f)) *)
  simpl. econstructor; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor; auto.

- (* returnstate *)
  inv H2.
+ (* synchronous return in both programs *)
  left. econstructor; split.
  apply exec_return.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  constructor; auto. apply set_reg_lessdef; auto.
+ (* return instr in source program, eliminated because of tailcall *)
  right. split. unfold measure. simpl length.
  change (S (length s) * (niter + 2))%nat
   with ((niter + 2) + (length s) * (niter + 2))%nat.
(* Goal: le n niter *)
(* Goal: forall (o : option reg) (_ : @eq instruction i (Ireturn o)) (_ : @eq (option instruction) (@PTree.get instruction pc (fn_code f)) (@Some instruction (Ireturn o))) (_ : @eq bool match o with | Some r => @proj_sumbool (@eq positive r rret) (not (@eq positive r rret)) (Reg.eq r rret) | None => true end true), is_return_spec f pc rret *)
  generalize (return_measure_bounds (fn_code f) pc). omega.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  split. auto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite Regmap.gss. auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. inv H.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  exploit funct_ptr_translated; eauto. intro FIND.
  exists (Callstate nil (transf_fundef f) nil m0); split.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  econstructor; eauto. apply (Genv.init_mem_transf TRANSL). auto.
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  replace (prog_main tprog) with (prog_main prog).
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  rewrite symbols_preserved. eauto.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  symmetry; eapply match_program_main; eauto.
  rewrite <- H3. apply sig_preserved.
(* Goal: final_state (Returnstate (@nil stackframe) (Vint r) m') r *)
  constructor. constructor. constructor. apply Mem.extends_refl.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
(* Goal: forall (st1 st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : final_state st1 r), final_state st2 r *)
  intros. inv H0. inv H. inv H5. inv H3. constructor.
Qed.


(** The preservation of the observable behavior of the program then
  follows. *)

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
(* Goal: @eq (option Mem.mem) (@Genv.init_mem fundef unit prog) (@Some Mem.mem m0) *)
(* Goal: @eq (option block) (@Genv.find_symbol fundef unit (@Genv.globalenv fundef unit tprog) (@prog_main fundef unit tprog)) (@Some block b) *)
(* Goal: @eq signature (funsig (transf_fundef f)) signature_main *)
(* Goal: match_states (Callstate (@nil stackframe) f (@nil val) m0) (Callstate (@nil stackframe) (transf_fundef f) (@nil val) m0) *)
  eapply forward_simulation_opt with (measure := measure); eauto.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact transf_step_correct.
Qed.

End PRESERVATION.

