(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness proof for the translation from Linear to Mach. *)

(** This file proves semantic preservation for the [Stacking] pass. *)

Require Import Coqlib Errors.
Require Import Integers AST Linking.
Require Import Values Memory Separation Events Globalenvs Smallstep.
Require Import LTL Op Locations Linear Mach.
Require Import Bounds Conventions Stacklayout Lineartyping.
Require Import Stacking.

Local Open Scope sep_scope.

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

Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. eapply match_transform_partial_program; eauto.
Qed.

(** * Basic properties of the translation *)

Lemma typesize_typesize:
  forall ty, AST.typesize ty = 4 * Locations.typesize ty.
Proof.
(* Goal: forall ty : typ, @eq Z (AST.typesize ty) (Z.mul (Zpos (xO (xO xH))) (typesize ty)) *)
  destruct ty; auto.
Qed.

Remark size_type_chunk:
  forall ty, size_chunk (chunk_of_type ty) = AST.typesize ty.
Proof.
(* Goal: forall ty : typ, @eq Z (align_chunk (chunk_of_type ty)) (Z.mul (Zpos (xO (xO xH))) (typealign ty)) *)
  destruct ty; reflexivity.
Qed.

Remark align_type_chunk:
  forall ty, align_chunk (chunk_of_type ty) = 4 * Locations.typealign ty.
Proof.
(* Goal: forall ty : typ, @eq Z (align_chunk (chunk_of_type ty)) (Z.mul (Zpos (xO (xO xH))) (typealign ty)) *)
  destruct ty; reflexivity.
Qed.

Lemma slot_outgoing_argument_valid:
  forall f ofs ty sg,
  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) -> slot_valid f Outgoing ofs ty = true.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. exploit loc_arguments_acceptable_2; eauto. intros [A B].
(* Goal: @eq bool (slot_valid f Outgoing ofs ty) true *)
  unfold slot_valid. unfold proj_sumbool.
(* Goal: @eq bool (andb (if zle Z0 pos then true else false) (if Zdivide_dec (typealign ty) pos (typealign_pos ty) then true else false)) true *)
  rewrite zle_true by omega.
(* Goal: @eq bool (andb true (if Zdivide_dec (typealign ty) pos (typealign_pos ty) then true else false)) true *)
  rewrite pred_dec_true by auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
Qed.

Lemma load_result_inject:
  forall j ty v v',
  Val.inject j v v' -> Val.has_type v ty -> Val.inject j v (Val.load_result (chunk_of_type ty) v').
Proof.
  intros until v'; unfold Val.has_type, Val.load_result; destruct Archi.ptr64;
  destruct 1; intros; auto; destruct ty; simpl;
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  try contradiction; try discriminate; econstructor; eauto.
Qed.

Section PRESERVATION.

Variable return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop.

Hypothesis return_address_offset_exists:
  forall f sg ros c,
  is_tail (Mcall sg ros :: c) (fn_code f) ->
  exists ofs, return_address_offset f c ofs.

Let step := Mach.step return_address_offset.

Variable prog: Linear.program.
Variable tprog: Mach.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Section FRAME_PROPERTIES.

Variable f: Linear.function.
Let b := function_bounds f.
Let fe := make_env b.
Variable tf: Mach.function.
Hypothesis TRANSF_F: transf_function f = OK tf.

Lemma unfold_transf_function:
  tf = Mach.mkfunction
         f.(Linear.fn_sig)
         (transl_body f fe)
         fe.(fe_size)
         (Ptrofs.repr fe.(fe_ofs_link))
         (Ptrofs.repr fe.(fe_ofs_retaddr)).
Proof.
(* Goal: Z.le (fe_size fe) Ptrofs.max_unsigned *)
  generalize TRANSF_F. unfold transf_function.
(* Goal: forall _ : @eq (res function) (if negb (wt_function f) then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
  destruct (wt_function f); simpl negb.
(* Goal: forall _ : @eq (res function) (if false then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
(* Goal: forall _ : @eq (res function) (if true then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
  destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))).
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (@None Linear.code) (@Some Linear.code c')), @is_tail Linear.instruction c' (@nil Linear.instruction) *)
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c) (@Some Linear.code c')), @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  intros; discriminate.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold fe. unfold b. congruence.
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (@None Linear.code) (@Some Linear.code c')), @is_tail Linear.instruction c' (@nil Linear.instruction) *)
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c) (@Some Linear.code c')), @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  intros; discriminate.
Qed.

Lemma transf_function_well_typed:
  wt_function f = true.
Proof.
(* Goal: Z.le (fe_size fe) Ptrofs.max_unsigned *)
  generalize TRANSF_F. unfold transf_function.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (wt_function f); simpl negb. auto. intros; discriminate.
Qed.

Lemma size_no_overflow: fe.(fe_size) <= Ptrofs.max_unsigned.
Proof.
(* Goal: Z.le (fe_size fe) Ptrofs.max_unsigned *)
  generalize TRANSF_F. unfold transf_function.
(* Goal: forall _ : @eq (res function) (if negb (wt_function f) then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
  destruct (wt_function f); simpl negb.
(* Goal: forall _ : @eq (res function) (if false then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
(* Goal: forall _ : @eq (res function) (if true then @Error function (msg (String (Ascii.Ascii true false false true false false true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true true false true false false) (String (Ascii.Ascii false true true false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false false true true false false true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) EmptyString))))))))))))))))))))))) else if zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f))) then @Error function (msg (String (Ascii.Ascii false false true false true false true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true true true false true true false) (String (Ascii.Ascii true false false true true true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii false true false false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii false false true false true true true false) (String (Ascii.Ascii true false false false false true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true true false true false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true false false true true true false) (String (Ascii.Ascii true false false true false true true false) (String (Ascii.Ascii false true false true true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false false true true true true false) (String (Ascii.Ascii true true false false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true false false true true false) EmptyString)))))))))))))))))))))))))))))))))))))))))))))))) else @OK function (mkfunction (Linear.fn_sig f) (transl_body f (make_env (function_bounds f))) (fe_size (make_env (function_bounds f))) (Ptrofs.repr (fe_ofs_link (make_env (function_bounds f)))) (Ptrofs.repr (fe_ofs_retaddr (make_env (function_bounds f)))))) (@OK function tf), Z.le (fe_size fe) Ptrofs.max_unsigned *)
  destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))).
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (@None Linear.code) (@Some Linear.code c')), @is_tail Linear.instruction c' (@nil Linear.instruction) *)
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c) (@Some Linear.code c')), @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  intros; discriminate.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold fe. unfold b. omega.
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (@None Linear.code) (@Some Linear.code c')), @is_tail Linear.instruction c' (@nil Linear.instruction) *)
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c) (@Some Linear.code c')), @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  intros; discriminate.
Qed.

Remark bound_stack_data_stacksize:
  f.(Linear.fn_stacksize) <= b.(bound_stack_data).
Proof.
(* Goal: Z.le (Linear.fn_stacksize f) (bound_stack_data b) *)
  unfold b, function_bounds, bound_stack_data. apply Z.le_max_l.
Qed.

(** * Memory assertions used to describe the contents of stack frames *)

Local Opaque Z.add Z.mul Z.divide.

(** Accessing the stack frame using [load_stack] and [store_stack]. *)

Lemma contains_get_stack:
  forall spec m ty sp ofs,
  m |= contains (chunk_of_type ty) sp ofs spec ->
  exists v, load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v /\ spec v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold load_stack.
(* Goal: @ex Mem.mem (fun m' : Mem.mem => and (@eq (option Mem.mem) (Mem.storev (chunk_of_type ty) m (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) v) (@Some Mem.mem m')) (m_pred (sepconj (contains (chunk_of_type ty) sp ofs spec) P) m')) *)
  replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply loadv_rule; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  simpl. rewrite Ptrofs.add_zero_l; auto.
Qed.

Lemma hasvalue_get_stack:
  forall ty m sp ofs v,
  m |= hasvalue (chunk_of_type ty) sp ofs v ->
  load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. exploit contains_get_stack; eauto. intros (v' & A & B). congruence.
Qed.

Lemma contains_set_stack:
  forall (spec: val -> Prop) v spec1 m ty sp ofs P,
  m |= contains (chunk_of_type ty) sp ofs spec1 ** P ->
  spec (Val.load_result (chunk_of_type ty) v) ->
  exists m',
      store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) v = Some m'
  /\ m' |= contains (chunk_of_type ty) sp ofs spec ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold store_stack.
(* Goal: @ex Mem.mem (fun m' : Mem.mem => and (@eq (option Mem.mem) (Mem.storev (chunk_of_type ty) m (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) v) (@Some Mem.mem m')) (m_pred (sepconj (contains (chunk_of_type ty) sp ofs spec) P) m')) *)
  replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply storev_rule; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  simpl. rewrite Ptrofs.add_zero_l; auto.
Qed.

(** [contains_locations j sp pos bound sl ls] is a separation logic assertion
  that holds if the memory area at block [sp], offset [pos], size [4 * bound],
  reflects the values of the stack locations of kind [sl] given by the
  location map [ls], up to the memory injection [j].

  Two such [contains_locations] assertions will be used later, one to
  reason about the values of [Local] slots, the other about the values of
  [Outgoing] slots. *)

(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
Program Definition contains_locations (j: meminj) (sp: block) (pos bound: Z) (sl: slot) (ls: locset) : massert := {|
  m_pred := fun m =>
    (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Ptrofs.modulus /\
    Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable /\
    forall ofs ty, 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
    exists v, Mem.load (chunk_of_type ty) m sp (pos + 4 * ofs) = Some v
           /\ Val.inject j (ls (S sl ofs ty)) v;
  m_footprint := fun b ofs =>
    b = sp /\ pos <= ofs < pos + 4 * bound
|}.
Next Obligation.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intuition auto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- red; intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- exploit H4; eauto. intros (v & A & B). exists v; split; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply Mem.load_unchanged_on; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  simpl; intros. rewrite size_type_chunk, typesize_typesize in H8.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split; auto. omega.
Qed.
Next Obligation.
(* Goal: Mem.valid_block m sp *)
  eauto with mem.
Qed.

Remark valid_access_location:
  forall m sp pos bound ofs ty p,
  (8 | pos) ->
  Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable ->
  0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
  Mem.valid_access m (chunk_of_type ty) sp (pos + 4 * ofs) p.
Proof.
(* Goal: forall (m : Mem.mem) (sp : block) (pos bound ofs : Z) (ty : typ) (p : permission) (_ : Z.divide (Zpos (xO (xO (xO xH)))) pos) (_ : Mem.range_perm m sp pos (Z.add pos (Z.mul (Zpos (xO (xO xH))) bound)) Cur Freeable) (_ : Z.le Z0 ofs) (_ : Z.le (Z.add ofs (typesize ty)) bound) (_ : Z.divide (typealign ty) ofs), Mem.valid_access m (chunk_of_type ty) sp (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs)) p *)
  intros; split.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- red; intros. apply Mem.perm_implies with Freeable; auto with mem.
(* Goal: forall _ : Z.gt (typesize ty) Z0, and (Z.le Z0 (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs))) (Z.le (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs)) (Z.sub Ptrofs.modulus (Zpos xH))) *)
  apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega.
- rewrite align_type_chunk. apply Z.divide_add_r.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Z.divide_trans with 8; auto.
(* Goal: forall ty : typ, @eq Z (align_chunk (chunk_of_type ty)) (Z.mul (Zpos (xO (xO xH))) (typealign ty)) *)
  exists (8 / (4 * typealign ty)); destruct ty; reflexivity.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Z.mul_divide_mono_l. auto.
Qed.

Lemma get_location:
  forall m j sp pos bound sl ls ofs ty,
  m |= contains_locations j sp pos bound sl ls ->
  0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
  exists v,
     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) = Some v
  /\ Val.inject j (ls (S sl ofs ty)) v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct H as (D & E & F & G & H).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit H; eauto. intros (v & U & V). exists v; split; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto.
(* Goal: forall _ : Z.gt (typesize ty) Z0, and (Z.le Z0 (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs))) (Z.le (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs)) (Z.sub Ptrofs.modulus (Zpos xH))) *)
  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
Qed.

Lemma set_location:
  forall m j sp pos bound sl ls P ofs ty v v',
  m |= contains_locations j sp pos bound sl ls ** P ->
  0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
  Val.inject j v v' ->
  exists m',
     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) v' = Some m'
  /\ m' |= contains_locations j sp pos bound sl (Locmap.set (S sl ofs ty) v ls) ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct H as (A & B & C). destruct A as (D & E & F & G & H).
  edestruct Mem.valid_access_store as [m' STORE].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply valid_access_location; eauto.
  assert (PERM: Mem.range_perm m' sp pos (pos + 4 * bound) Cur Freeable).
(* Goal: Mem.valid_block m sp *)
  { red; intros; eauto with mem. }
  exists m'; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto.
(* Goal: forall _ : Z.gt (typesize ty) Z0, and (Z.le Z0 (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs))) (Z.le (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs)) (Z.sub Ptrofs.modulus (Zpos xH))) *)
  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- simpl. intuition auto.
+ unfold Locmap.set.
  destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))].
* (* same location *)
  inv e. rename ofs0 into ofs. rename ty0 into ty.
  exists (Val.load_result (chunk_of_type ty) v'); split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply Mem.load_store_similar_2; eauto. omega.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.load_result_inject; auto.
* (* different locations *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite <- X; eapply Mem.load_store_other; eauto.
(* Goal: callee_save_loc (S Incoming ofs ty) *)
  destruct d. congruence. right. rewrite ! size_type_chunk, ! typesize_typesize. omega.
* (* overlapping locations *)
  destruct (Mem.valid_access_load m' (chunk_of_type ty0) sp (pos + 4 * ofs0)) as [v'' LOAD].
  apply Mem.valid_access_implies with Writable; auto with mem.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply valid_access_location; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists v''; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
+ apply (m_invar P) with m; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply Mem.store_unchanged_on; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros i; rewrite size_type_chunk, typesize_typesize. intros; red; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eelim C; eauto. simpl. split; auto. omega.
Qed.

Lemma initial_locations:
  forall j sp pos bound P sl ls m,
  m |= range sp pos (pos + 4 * bound) ** P ->
  (8 | pos) ->
  (forall ofs ty, ls (S sl ofs ty) = Vundef) ->
  m |= contains_locations j sp pos bound sl ls ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct H as (A & B & C). destruct A as (D & E & F). split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- simpl; intuition auto. red; intros; eauto with mem.
  destruct (Mem.valid_access_load m (chunk_of_type ty) sp (pos + 4 * ofs)) as [v LOAD].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply valid_access_location; eauto.
(* Goal: Mem.valid_block m sp *)
  red; intros; eauto with mem.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists v; split; auto. rewrite H1; auto.
- split; assumption.
Qed.

Lemma contains_locations_exten:
  forall ls ls' j sp pos bound sl,
  (forall ofs ty, Val.lessdef (ls' (S sl ofs ty)) (ls (S sl ofs ty))) ->
  massert_imp (contains_locations j sp pos bound sl ls)
              (contains_locations j sp pos bound sl ls').
Proof.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; split; simpl; intros; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intuition auto. exploit H5; eauto. intros (v & A & B). exists v; split; auto. 
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  specialize (H ofs ty). inv H. congruence. auto. 
Qed.

Lemma contains_locations_incr:
  forall j j' sp pos bound sl ls,
  inject_incr j j' ->
  massert_imp (contains_locations j sp pos bound sl ls)
              (contains_locations j' sp pos bound sl ls).
Proof.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; split; simpl; intros; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intuition auto. exploit H5; eauto. intros (v & A & B). exists v; eauto.
Qed.

(** [contains_callee_saves j sp pos rl ls] is a memory assertion that holds
  if block [sp], starting at offset [pos], contains the values of the
  callee-save registers [rl] as given by the location map [ls],
  up to the memory injection [j].  The memory layout of the registers in [rl]
  is the same as that implemented by [save_callee_save_rec]. *)

Fixpoint contains_callee_saves (j: meminj) (sp: block) (pos: Z) (rl: list mreg) (ls: locset) : massert :=
  match rl with
  | nil => pure True
  | r :: rl =>
      let ty := mreg_type r in
      let sz := AST.typesize ty in
      let pos1 := align pos sz in
      contains (chunk_of_type ty) sp pos1 (fun v => Val.inject j (ls (R r)) v)
      ** contains_callee_saves j sp (pos1 + sz) rl ls
  end.

Lemma contains_callee_saves_incr:
  forall j j' sp ls,
  inject_incr j j' ->
  forall rl pos,
  massert_imp (contains_callee_saves j sp pos rl ls)
              (contains_callee_saves j' sp pos rl ls).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl as [ | r1 rl]; simpl; intros.
- reflexivity.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply sepconj_morph_1; auto. apply contains_imp. eauto.
Qed.

Lemma contains_callee_saves_exten:
  forall j sp ls ls' rl pos,
  (forall r, In r rl -> ls' (R r) = ls (R r)) ->
  massert_eqv (contains_callee_saves j sp pos rl ls)
              (contains_callee_saves j sp pos rl ls').
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl as [ | r1 rl]; simpl; intros.
- reflexivity.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply sepconj_morph_2; auto. rewrite H by auto. reflexivity.
Qed.

(** Separation logic assertions describing the stack frame at [sp].
  It must contain:
  - the values of the [Local] stack slots of [ls], as per [contains_locations]
  - the values of the [Outgoing] stack slots of [ls], as per [contains_locations]
  - the [parent] pointer representing the back link to the caller's frame
  - the [retaddr] pointer representing the saved return address
  - the initial values of the used callee-save registers as given by [ls0],
    as per [contains_callee_saves].

In addition, we use a nonseparating conjunction to record the fact that
we have full access rights on the stack frame, except the part that
represents the Linear stack data. *)

Definition frame_contents_1 (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) :=
    contains_locations j sp fe.(fe_ofs_local) b.(bound_local) Local ls
 ** contains_locations j sp fe_ofs_arg b.(bound_outgoing) Outgoing ls
 ** hasvalue Mptr sp fe.(fe_ofs_link) parent
 ** hasvalue Mptr sp fe.(fe_ofs_retaddr) retaddr
 ** contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0.

Definition frame_contents (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) :=
  mconj (frame_contents_1 j sp ls ls0 parent retaddr)
        (range sp 0 fe.(fe_stack_data) **
         range sp (fe.(fe_stack_data) + b.(bound_stack_data)) fe.(fe_size)).

(** Accessing components of the frame. *)

Lemma frame_get_local:
  forall ofs ty j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
  exists v,
     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) = Some v
  /\ Val.inject j (ls (S Local ofs ty)) v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans.
(* Goal: @eq (option val) (load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr (fe_ofs_retaddr fe))) (@Some val retaddr) *)
  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_proj1 in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply get_location; eauto.
Qed.

Lemma frame_get_outgoing:
  forall ofs ty j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
  exists v,
     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) = Some v
  /\ Val.inject j (ls (S Outgoing ofs ty)) v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans.
(* Goal: @eq (option val) (load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr (fe_ofs_retaddr fe))) (@Some val retaddr) *)
  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick2 in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply get_location; eauto.
Qed.

Lemma frame_get_parent:
  forall j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_link)) = Some parent.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros.
  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. rewrite <- chunk_of_Tptr in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply hasvalue_get_stack; eauto.
Qed.

Lemma frame_get_retaddr:
  forall j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_retaddr)) = Some retaddr.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros.
  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. rewrite <- chunk_of_Tptr in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply hasvalue_get_stack; eauto.
Qed.

(** Assigning a [Local] or [Outgoing] stack slot. *)

Lemma frame_set_local:
  forall ofs ty v v' j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
  Val.inject j v v' ->
  exists m',
     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) v' = Some m'
  /\ m' |= frame_contents j sp (Locmap.set (S Local ofs ty) v ls) ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold frame_contents in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit mconj_proj1; eauto. unfold frame_contents_1.
  rewrite ! sep_assoc; intros SEP.
(* Goal: @ex val (fun v : val => and (@eq (option val) (load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs))) (@Some val v)) (Val.inject j (ls (S Outgoing ofs ty)) v)) *)
  unfold slot_valid in H1; InvBooleans. simpl in H0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit set_location; eauto. intros (m' & A & B).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists m'; split; auto.
  assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  {  intros. unfold store_stack in A; simpl in A. eapply Mem.perm_store_1; eauto. }
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply frame_mconj. eauto.
  unfold frame_contents_1; rewrite ! sep_assoc; exact B.
  eapply sep_preserved.
  eapply sep_proj1. eapply mconj_proj2. eassumption.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; eapply range_preserved; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; eapply range_preserved; eauto.
Qed.

Lemma frame_set_outgoing:
  forall ofs ty v v' j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
  Val.inject j v v' ->
  exists m',
     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) v' = Some m'
  /\ m' |= frame_contents j sp (Locmap.set (S Outgoing ofs ty) v ls) ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. unfold frame_contents in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit mconj_proj1; eauto. unfold frame_contents_1.
  rewrite ! sep_assoc, sep_swap. intros SEP.
(* Goal: @ex val (fun v : val => and (@eq (option val) (load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs))) (@Some val v)) (Val.inject j (ls (S Outgoing ofs ty)) v)) *)
  unfold slot_valid in H1; InvBooleans. simpl in H0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit set_location; eauto. intros (m' & A & B).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists m'; split; auto.
  assert (forall i k p, Mem.perm m sp i k p -> Mem.perm m' sp i k p).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  {  intros. unfold store_stack in A; simpl in A. eapply Mem.perm_store_1; eauto. }
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply frame_mconj. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold frame_contents_1; rewrite ! sep_assoc, sep_swap; eauto.
  eapply sep_preserved.
  eapply sep_proj1. eapply mconj_proj2. eassumption.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; eapply range_preserved; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; eapply range_preserved; eauto.
Qed.

(** Invariance by change of location maps. *)

Lemma frame_contents_exten:
  forall ls ls0 ls' ls0' j sp parent retaddr P m,
  (forall ofs ty, Val.lessdef (ls' (S Local ofs ty)) (ls (S Local ofs ty))) ->
  (forall ofs ty, Val.lessdef (ls' (S Outgoing ofs ty)) (ls (S Outgoing ofs ty))) ->
  (forall r, In r b.(used_callee_save) -> ls0' (R r) = ls0 (R r)) ->
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  m |= frame_contents j sp ls' ls0' parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite <- ! (contains_locations_exten ls ls') by auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  erewrite  <- contains_callee_saves_exten by eauto.
(* Goal: m_pred (sepconj (mconj (sepconj (contains_locations j sp (fe_ofs_local fe) (bound_local b) Local ls) (sepconj (contains_locations j sp fe_ofs_arg (bound_outgoing b) Outgoing ls) (sepconj (hasvalue Mptr sp (fe_ofs_link fe) parent) (sepconj (hasvalue Mptr sp (fe_ofs_retaddr fe) retaddr) (contains_callee_saves j sp (fe_ofs_callee_save fe) (used_callee_save b) ls0))))) (sepconj (range sp Z0 (fe_stack_data fe)) (range sp (Z.add (fe_stack_data fe) (bound_stack_data b)) (fe_size fe)))) P) m *)
  assumption.
Qed.

(** Invariance by assignment to registers. *)

Corollary frame_set_reg:
  forall r v j sp ls ls0 parent retaddr m P,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  m |= frame_contents j sp (Locmap.set (R r) v ls) ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. apply frame_contents_exten with ls ls0; auto.
Qed.

Corollary frame_undef_regs:
  forall j sp ls ls0 parent retaddr m P rl,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  m |= frame_contents j sp (LTL.undef_regs rl ls) ls0 parent retaddr ** P.
Proof.
Local Opaque sepconj.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply frame_set_reg; auto.
Qed.

Corollary frame_set_regpair:
  forall j sp ls0 parent retaddr m P p v ls,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  m |= frame_contents j sp (Locmap.setpair p v ls) ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct p; simpl.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_set_reg; apply frame_set_reg; auto.
Qed.

Corollary frame_set_res:
  forall j sp ls0 parent retaddr m P res v ls,
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  m |= frame_contents j sp (Locmap.setres res v ls) ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction res; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply frame_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- eauto.
Qed.

(** Invariance by change of memory injection. *)

Lemma frame_contents_incr:
  forall j sp ls ls0 parent retaddr m P j',
  m |= frame_contents j sp ls ls0 parent retaddr ** P ->
  inject_incr j j' ->
  m |= frame_contents j' sp ls ls0 parent retaddr ** P.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold frame_contents, frame_contents_1; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite <- (contains_locations_incr j j') by auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite <- (contains_locations_incr j j') by auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  erewrite  <- contains_callee_saves_incr by eauto.
(* Goal: m_pred (sepconj (mconj (sepconj (contains_locations j sp (fe_ofs_local fe) (bound_local b) Local ls) (sepconj (contains_locations j sp fe_ofs_arg (bound_outgoing b) Outgoing ls) (sepconj (hasvalue Mptr sp (fe_ofs_link fe) parent) (sepconj (hasvalue Mptr sp (fe_ofs_retaddr fe) retaddr) (contains_callee_saves j sp (fe_ofs_callee_save fe) (used_callee_save b) ls0))))) (sepconj (range sp Z0 (fe_stack_data fe)) (range sp (Z.add (fe_stack_data fe) (bound_stack_data b)) (fe_size fe)))) P) m *)
  assumption.
Qed.

(** * Agreement between location sets and Mach states *)

(** Agreement with Mach register states *)

Definition agree_regs (j: meminj) (ls: locset) (rs: regset) : Prop :=
  forall r, Val.inject j (ls (R r)) (rs r).

(** Agreement over locations *)

Record agree_locs (ls ls0: locset) : Prop :=
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  mk_agree_locs {

    (** Unused registers have the same value as in the caller *)
    agree_unused_reg:
       forall r, ~(mreg_within_bounds b r) -> ls (R r) = ls0 (R r);

    (** Incoming stack slots have the same value as the
        corresponding Outgoing stack slots in the caller *)
    agree_incoming:
       forall ofs ty,
       In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters f.(Linear.fn_sig))) ->
       ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty)
}.

(** ** Properties of [agree_regs]. *)

(** Values of registers *)

Lemma agree_reg:
  forall j ls rs r,
  agree_regs j ls rs -> Val.inject j (ls (R r)) (rs r).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. auto.
Qed.

Lemma agree_reglist:
  forall j ls rs rl,
  agree_regs j ls rs -> Val.inject_list j (reglist ls rl) (rs##rl).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto. constructor; auto using agree_reg.
Qed.

Hint Resolve agree_reg agree_reglist: stacking.

(** Preservation under assignments of machine registers. *)

Lemma agree_regs_set_reg:
  forall j ls rs r v v',
  agree_regs j ls rs ->
  Val.inject j v v' ->
  agree_regs j (Locmap.set (R r) v ls) (Regmap.set r v' rs).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros; red; intros.
(* Goal: Val.inject j (Locmap.set (R r) v ls (R r0)) (@Regmap.set val r v' rs r0) *)
  unfold Regmap.set. destruct (RegEq.eq r0 r). subst r0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite Locmap.gss; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite Locmap.gso; auto. red. auto.
Qed.

Lemma agree_regs_set_pair:
  forall j p v v' ls rs,
  agree_regs j ls rs ->
  Val.inject j v v' ->
  agree_regs j (Locmap.setpair p v ls) (set_pair p v' rs).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct p; simpl.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply agree_regs_set_reg. apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.hiword_inject; auto. apply Val.loword_inject; auto.
Qed.

Lemma agree_regs_set_res:
  forall j res v v' ls rs,
  agree_regs j ls rs ->
  Val.inject j v v' ->
  agree_regs j (Locmap.setres res v ls) (set_res res v' rs).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction res; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply IHres2. apply IHres1. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.hiword_inject; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.loword_inject; auto.
Qed.

Lemma agree_regs_exten:
  forall j ls rs ls' rs',
  agree_regs j ls rs ->
  (forall r, ls' (R r) = Vundef \/ ls' (R r) = ls (R r) /\ rs' r = rs r) ->
  agree_regs j ls' rs'.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros; red; intros.
(* Goal: Val.inject j (ls' (R r)) (rs' r) *)
  destruct (H0 r) as [A | [A B]].
(* Goal: Val.inject j (ls' (R r)) (rs' r) *)
(* Goal: Val.inject j (ls' (R r)) (rs' r) *)
  rewrite A. constructor.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite A; rewrite B; auto.
Qed.

Lemma agree_regs_undef_regs:
  forall j rl ls rs,
  agree_regs j ls rs ->
  agree_regs j (LTL.undef_regs rl ls) (Mach.undef_regs rl rs).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg; auto.
Qed.

Lemma agree_regs_undef_caller_save_regs:
  forall j ls rs,
  agree_regs j ls rs ->
  agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros; red; intros. 
(* Goal: Val.inject j (LTL.undef_caller_save_regs ls (R r)) (undef_caller_save_regs rs r) *)
  unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. 
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (is_callee_save r); auto. 
Qed.

(** Preservation under assignment of stack slot *)

Lemma agree_regs_set_slot:
  forall j ls rs sl ofs ty v,
  agree_regs j ls rs ->
  agree_regs j (Locmap.set (S sl ofs ty) v ls) rs.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros; red; intros. rewrite Locmap.gso; auto. red. auto.
Qed.

(** Preservation by increasing memory injections *)

Lemma agree_regs_inject_incr:
  forall j ls rs j',
  agree_regs j ls rs -> inject_incr j j' -> agree_regs j' ls rs.
Proof.
(* Goal: forall (j : Val.meminj) (ls : locset) (rs : regset) (j' : Val.meminj) (_ : agree_regs j ls rs) (_ : inject_incr j j'), agree_regs j' ls rs *)
  intros; red; intros; eauto with stacking.
Qed.

(** Preservation at function entry. *)

Lemma agree_regs_call_regs:
  forall j ls rs,
  agree_regs j ls rs ->
  agree_regs j (call_regs ls) rs.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold call_regs; intros; red; intros; auto.
Qed.

(** ** Properties of [agree_locs] *)

(** Preservation under assignment of machine register. *)

Lemma agree_locs_set_reg:
  forall ls ls0 r v,
  agree_locs ls ls0 ->
  mreg_within_bounds b r ->
  agree_locs (Locmap.set (R r) v ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. inv H; constructor; auto; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite Locmap.gso. auto. red. intuition congruence.
Qed.

Lemma caller_save_reg_within_bounds:
  forall r,
  is_callee_save r = false -> mreg_within_bounds b r.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros; red; intros. congruence.
Qed.

Lemma agree_locs_set_pair:
  forall ls0 p v ls,
  agree_locs ls ls0 ->
  forall_rpair (fun r => is_callee_save r = false) p ->
  agree_locs (Locmap.setpair p v ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros.
  destruct p; simpl in *.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto. apply caller_save_reg_within_bounds; auto.
(* Goal: @eq bool (slot_valid f Outgoing pos ty) true *)
  destruct H0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto. apply agree_locs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply caller_save_reg_within_bounds; auto. apply caller_save_reg_within_bounds; auto.
Qed.

Lemma agree_locs_set_res:
  forall ls0 res v ls,
  agree_locs ls ls0 ->
  (forall r, In r (params_of_builtin_res res) -> mreg_within_bounds b r) ->
  agree_locs (Locmap.setres res v ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction res; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- eapply agree_locs_set_reg; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
- apply IHres2; auto using in_or_app.
Qed.

Lemma agree_locs_undef_regs:
  forall ls0 regs ls,
  agree_locs ls ls0 ->
  (forall r, In r regs -> mreg_within_bounds b r) ->
  agree_locs (LTL.undef_regs regs ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction regs; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto.
Qed.

Lemma agree_locs_undef_locs_1:
  forall ls0 regs ls,
  agree_locs ls ls0 ->
  (forall r, In r regs -> is_callee_save r = false) ->
  agree_locs (LTL.undef_regs regs ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. eapply agree_locs_undef_regs; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. apply caller_save_reg_within_bounds. auto.
Qed.

Lemma agree_locs_undef_locs:
  forall ls0 regs ls,
  agree_locs ls ls0 ->
  existsb is_callee_save regs = false ->
  agree_locs (LTL.undef_regs regs ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. eapply agree_locs_undef_locs_1; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct (is_callee_save r) eqn:CS; auto.
(* Goal: @eq bool true false *)
  assert (existsb is_callee_save regs = true).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  { apply existsb_exists. exists r; auto. }
(* Goal: callee_save_loc (S Incoming ofs ty) *)
  congruence.
Qed.

(** Preservation by assignment to local slot *)

Lemma agree_locs_set_slot:
  forall ls ls0 sl ofs ty v,
  agree_locs ls ls0 ->
  slot_writable sl = true ->
  agree_locs (Locmap.set (S sl ofs ty) v ls) ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct H; constructor; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- rewrite Locmap.gso; auto. red; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- rewrite Locmap.gso; auto. red. left. destruct sl; discriminate.
Qed.

(** Preservation at return points (when [ls] is changed but not [ls0]). *)

Lemma agree_locs_return:
  forall ls ls0 ls',
  agree_locs ls ls0 ->
  agree_callee_save ls' ls ->
  agree_locs ls' ls0.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. red in H0. inv H; constructor; auto; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- rewrite H0; auto. unfold mreg_within_bounds in H. tauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- rewrite <- agree_incoming0 by auto. apply H0. congruence.
Qed.

(** ** Properties of destroyed registers. *)

Definition no_callee_saves (l: list mreg) : Prop :=
  existsb is_callee_save l = false.

Remark destroyed_by_op_caller_save:
  forall op, no_callee_saves (destroyed_by_op op).
Proof.
(* Goal: forall op : operation, no_callee_saves (destroyed_by_op op) *)
  unfold no_callee_saves; destruct op; (reflexivity || destruct c; reflexivity).
Qed.

Remark destroyed_by_load_caller_save:
  forall chunk addr, no_callee_saves (destroyed_by_load chunk addr).
Proof.
(* Goal: @eq bool (andb true true) true *)
  unfold no_callee_saves; destruct chunk; reflexivity.
Qed.

Remark destroyed_by_store_caller_save:
  forall chunk addr, no_callee_saves (destroyed_by_store chunk addr).
Proof.
Local Transparent destroyed_by_store.
(* Goal: @eq bool (andb true true) true *)
  unfold no_callee_saves, destroyed_by_store; intros; destruct chunk; try reflexivity; destruct Archi.ptr64; reflexivity.
Qed.

Remark destroyed_by_cond_caller_save:
  forall cond, no_callee_saves (destroyed_by_cond cond).
Proof.
(* Goal: @eq bool (andb true true) true *)
  unfold no_callee_saves; destruct cond; reflexivity.
Qed.

Remark destroyed_by_jumptable_caller_save:
  no_callee_saves destroyed_by_jumptable.
Proof.
(* Goal: @eq bool (andb true true) true *)
  red; reflexivity.
Qed.

Remark destroyed_by_setstack_caller_save:
  forall ty, no_callee_saves (destroyed_by_setstack ty).
Proof.
(* Goal: forall ty : typ, @eq Z (align_chunk (chunk_of_type ty)) (Z.mul (Zpos (xO (xO xH))) (typealign ty)) *)
  unfold no_callee_saves; destruct ty; reflexivity.
Qed.

Remark destroyed_at_function_entry_caller_save:
  no_callee_saves destroyed_at_function_entry.
Proof.
(* Goal: @eq bool (andb true true) true *)
  red; reflexivity.
Qed.

Hint Resolve destroyed_by_op_caller_save destroyed_by_load_caller_save
    destroyed_by_store_caller_save
    destroyed_by_cond_caller_save destroyed_by_jumptable_caller_save
    destroyed_at_function_entry_caller_save: stacking.

Remark destroyed_by_setstack_function_entry:
  forall ty, incl (destroyed_by_setstack ty) destroyed_at_function_entry.
Proof.
Local Transparent destroyed_by_setstack destroyed_at_function_entry.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold incl; destruct ty; simpl; tauto.
Qed.

Remark transl_destroyed_by_op:
  forall op e, destroyed_by_op (transl_op e op) = destroyed_by_op op.
Proof.
(* Goal: @eq bool (andb true true) true *)
  intros; destruct op; reflexivity.
Qed.

Remark transl_destroyed_by_load:
  forall chunk addr e, destroyed_by_load chunk (transl_addr e addr) = destroyed_by_load chunk addr.
Proof.
(* Goal: @eq bool (andb true true) true *)
  intros; destruct chunk; reflexivity.
Qed.

Remark transl_destroyed_by_store:
  forall chunk addr e, destroyed_by_store chunk (transl_addr e addr) = destroyed_by_store chunk addr.
Proof.
(* Goal: @eq bool (andb true true) true *)
  intros; destruct chunk; reflexivity.
Qed.

(** * Correctness of saving and restoring of callee-save registers *)

(** The following lemmas show the correctness of the register saving
  code generated by [save_callee_save]: after this code has executed,
  the register save areas of the current frame do contain the
  values of the callee-save registers used by the function. *)

Section SAVE_CALLEE_SAVE.

Variable j: meminj.
Variable cs: list stackframe.
Variable fb: block.
Variable sp: block.
Variable ls: locset.

Hypothesis ls_temp_undef:
  forall ty r, In r (destroyed_by_setstack ty) -> ls (R r) = Vundef.

Hypothesis wt_ls: forall r, Val.has_type (ls (R r)) (mreg_type r).

Lemma save_callee_save_rec_correct:
  forall k l pos rs m P,
  (forall r, In r l -> is_callee_save r = true) ->
  m |= range sp pos (size_callee_save_area_rec l pos) ** P ->
  agree_regs j ls rs ->
  exists rs', exists m',
     star step tge
        (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save_rec l pos k) rs m)
     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
  /\ m' |= contains_callee_saves j sp pos l ls ** P
  /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p)
  /\ agree_regs j ls rs'.
Proof.
Local Opaque mreg_type.
  induction l as [ | r l]; simpl; intros until P; intros CS SEP AG.
- exists rs, m.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. apply star_refl.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split. rewrite sep_pure; split; auto. eapply sep_drop; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
- set (ty := mreg_type r) in *.
  set (sz := AST.typesize ty) in *.
  set (pos1 := align pos sz) in *.
  assert (SZPOS: sz > 0) by (apply AST.typesize_pos).
  assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr).
  assert (POS1: pos <= pos1) by (apply align_le; auto).
  assert (AL1: (align_chunk (chunk_of_type ty) | pos1)).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { unfold pos1. apply Z.divide_trans with sz.
    unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply align_divides; auto. }
  apply range_drop_left with (mid := pos1) in SEP; [ | omega ].
  apply range_split with (mid := pos1 + sz) in SEP; [ | omega ].
  unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply range_contains in SEP; auto.
  exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)).
  eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply load_result_inject; auto. apply wt_ls.
  clear SEP; intros (m1 & STORE & SEP).
  set (rs1 := undef_regs (destroyed_by_setstack ty) rs).
  assert (AG1: agree_regs j ls rs1).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  { red; intros. unfold rs1. destruct (In_dec mreg_eq r0 (destroyed_by_setstack ty)).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    erewrite ls_temp_undef by eauto. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    rewrite undef_regs_other by auto. apply AG. }
  rewrite sep_swap in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit (IHl (pos1 + sz) rs1 m1); eauto.
  intros (rs2 & m2 & A & B & C & D).
  exists rs2, m2.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split. eapply star_left; eauto. constructor. exact STORE. auto. traceEq.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. rewrite sep_assoc, sep_swap. exact B.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split. intros. apply C. unfold store_stack in STORE; simpl in STORE. eapply Mem.perm_store_1; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
Qed.

End SAVE_CALLEE_SAVE.

Remark LTL_undef_regs_same:
  forall r rl ls, In r rl -> LTL.undef_regs rl ls (R r) = Vundef.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros. contradiction.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold Locmap.set. destruct (Loc.eq (R a) (R r)). auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (Loc.diff_dec (R a) (R r)); auto.
(* Goal: callee_save_loc (S Incoming ofs ty) *)
  apply IHrl. intuition congruence.
Qed.

Remark LTL_undef_regs_others:
  forall r rl ls, ~In r rl -> LTL.undef_regs rl ls (R r) = ls (R r).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros. auto.
(* Goal: Loc.diff (R a) (R r) *)
  rewrite Locmap.gso. apply IHrl. intuition. red. intuition.
Qed.

Remark LTL_undef_regs_slot:
  forall sl ofs ty rl ls, LTL.undef_regs rl ls (S sl ofs ty) = ls (S sl ofs ty).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite Locmap.gso. apply IHrl. red; auto.
Qed.

Remark undef_regs_type:
  forall ty l rl ls,
  Val.has_type (ls l) ty -> Val.has_type (LTL.undef_regs rl ls l) ty.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction rl; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- unfold Locmap.set. destruct (Loc.eq (R a) l). red; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (Loc.diff_dec (R a) l); auto. red; auto.
Qed.

Lemma save_callee_save_correct:
  forall j ls ls0 rs sp cs fb k m P,
  m |= range sp fe.(fe_ofs_callee_save) (size_callee_save_area b fe.(fe_ofs_callee_save)) ** P ->
  (forall r, Val.has_type (ls (R r)) (mreg_type r)) ->
  agree_callee_save ls ls0 ->
  agree_regs j ls rs ->
  let ls1 := LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) in
  let rs1 := undef_regs destroyed_at_function_entry rs in
  exists rs', exists m',
     star step tge
        (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save fe k) rs1 m)
     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
  /\ m' |= contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0 ** P
  /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p)
  /\ agree_regs j ls1 rs'.
Proof.
  intros until P; intros SEP TY AGCS AG; intros ls1 rs1.
  exploit (save_callee_save_rec_correct j cs fb sp ls1).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- intros. unfold ls1. apply LTL_undef_regs_same. eapply destroyed_by_setstack_function_entry; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- intros. unfold ls1. apply undef_regs_type. apply TY.
- exact b.(used_callee_save_prop).
- eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- instantiate (1 := rs1). apply agree_regs_undef_regs. apply agree_regs_call_regs. auto.
- clear SEP. intros (rs' & m' & EXEC & SEP & PERMS & AG').
  exists rs', m'.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. eexact EXEC.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. rewrite (contains_callee_saves_exten j sp ls0 ls1). exact SEP.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. apply b.(used_callee_save_prop) in H.
    unfold ls1. rewrite LTL_undef_regs_others. unfold call_regs.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply AGCS; auto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
    red; intros.
    assert (existsb is_callee_save destroyed_at_function_entry = false)
       by  (apply destroyed_at_function_entry_caller_save).
    assert (existsb is_callee_save destroyed_at_function_entry = true).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    { apply existsb_exists. exists r; auto. }
(* Goal: callee_save_loc (S Incoming ofs ty) *)
    congruence.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact PERMS. exact AG'.
Qed.

(** As a corollary of the previous lemmas, we obtain the following
  correctness theorem for the execution of a function prologue
  (allocation of the frame + saving of the link and return address +
  saving of the used callee-save registers). *)

Lemma function_prologue_correct:
  forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k P,
  agree_regs j ls rs ->
  agree_callee_save ls ls0 ->
  agree_outgoing_arguments (Linear.fn_sig f) ls ls0 ->
  (forall r, Val.has_type (ls (R r)) (mreg_type r)) ->
  ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
  rs1 = undef_regs destroyed_at_function_entry rs ->
  Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) ->
  Val.has_type parent Tptr -> Val.has_type ra Tptr ->
  m1' |= minjection j m1 ** globalenv_inject ge j ** P ->
  exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5',
     Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
  /\ store_stack m2' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) parent = Some m3'
  /\ store_stack m3' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) ra = Some m4'
  /\ star step tge
         (State cs fb (Vptr sp' Ptrofs.zero) (save_callee_save fe k) rs1 m4')
      E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs' m5')
  /\ agree_regs j' ls1 rs'
  /\ agree_locs ls1 ls0
  /\ m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P
  /\ j' sp = Some(sp', fe.(fe_stack_data))
  /\ inject_incr j j'.
Proof.
  intros until P; intros AGREGS AGCS AGARGS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP.
  rewrite unfold_transf_function.
  unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs.
  (* Stack layout info *)
Local Opaque b fe.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  generalize (frame_env_range b) (frame_env_aligned b). replace (make_env b) with fe by auto. simpl.
  intros LAYOUT1 LAYOUT2.
  (* Allocation step *)
  destruct (Mem.alloc m1' 0 (fe_size fe)) as [m2' sp'] eqn:ALLOC'.
  exploit alloc_parallel_rule_2.
  eexact SEP. eexact ALLOC. eexact ALLOC'.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  instantiate (1 := fe_stack_data fe). tauto.
(* Goal: @eq bool (andb true true) true *)
  reflexivity.
  instantiate (1 := fe_stack_data fe + bound_stack_data b). rewrite Z.max_comm. reflexivity.
(* Goal: forall _ : Z.gt (typesize ty) Z0, and (Z.le Z0 (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs))) (Z.le (Z.add pos (Z.mul (Zpos (xO (xO xH))) ofs)) (Z.sub Ptrofs.modulus (Zpos xH))) *)
  generalize (bound_stack_data_pos b) size_no_overflow; omega.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  tauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  tauto.
  clear SEP. intros (j' & SEP & INCR & SAME).
  (* Remember the freeable permissions using a mconj *)
  assert (SEPCONJ:
    m2' |= mconj (range sp' 0 (fe_stack_data fe) ** range sp' (fe_stack_data fe + bound_stack_data b) (fe_size fe))
                 (range sp' 0 (fe_stack_data fe) ** range sp' (fe_stack_data fe + bound_stack_data b) (fe_size fe))
           ** minjection j' m2 ** globalenv_inject ge j' ** P).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { apply mconj_intro; rewrite sep_assoc; assumption. }
  (* Dividing up the frame *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto.
  (* Store of parent *)
  rewrite sep_swap3 in SEP.
  apply (range_contains Mptr) in SEP; [|tauto].
  exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
  clear SEP; intros (m3' & STORE_PARENT & SEP).
  rewrite sep_swap3 in SEP.
  (* Store of return address *)
  rewrite sep_swap4 in SEP.
  apply (range_contains Mptr) in SEP; [|tauto].
  exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
  clear SEP; intros (m4' & STORE_RETADDR & SEP).
  rewrite sep_swap4 in SEP.
  (* Saving callee-save registers *)
  rewrite sep_swap5 in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit (save_callee_save_correct j' ls ls0 rs); eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_inject_incr with j; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  replace (LTL.undef_regs destroyed_at_function_entry (call_regs ls)) with ls1 by auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  replace (undef_regs destroyed_at_function_entry rs) with rs1 by auto.
  clear SEP; intros (rs2 & m5' & SAVE_CS & SEP & PERMS & AGREGS').
  rewrite sep_swap5 in SEP.
  (* Materializing the Local and Outgoing locations *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit (initial_locations j'). eexact SEP. tauto.
  instantiate (1 := Local). instantiate (1 := ls1).
(* Goal: @eq bool (andb true true) true *)
  intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity.
  clear SEP; intros SEP.
  rewrite sep_swap in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit (initial_locations j'). eexact SEP. tauto.
  instantiate (1 := Outgoing). instantiate (1 := ls1).
(* Goal: @eq bool (andb true true) true *)
  intros; rewrite LS1. rewrite LTL_undef_regs_slot. reflexivity.
  clear SEP; intros SEP.
  rewrite sep_swap in SEP.
  (* Now we frame this *)
  assert (SEPFINAL: m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { eapply frame_mconj. eexact SEPCONJ.
    rewrite chunk_of_Tptr in SEP.
    unfold frame_contents_1; rewrite ! sep_assoc. exact SEP.
    assert (forall ofs k p, Mem.perm m2' sp' ofs k p -> Mem.perm m5' sp' ofs k p).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
    { intros. apply PERMS.
      unfold store_stack in STORE_PARENT, STORE_RETADDR.
      simpl in STORE_PARENT, STORE_RETADDR.
      eauto using Mem.perm_store_1. }
    eapply sep_preserved. eapply sep_proj1. eapply mconj_proj2. eexact SEPCONJ.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    intros; apply range_preserved with m2'; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    intros; apply range_preserved with m2'; auto.
  }
  clear SEP SEPCONJ.
(* Conclusions *)
  exists j', rs2, m2', sp', m3', m4', m5'.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split. auto.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact STORE_PARENT.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact STORE_RETADDR.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. eexact SAVE_CS.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact AGREGS'.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity].
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
    constructor; intros. unfold call_regs. apply AGCS.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    unfold mreg_within_bounds in H; tauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    unfold call_regs. apply AGARGS. apply incoming_slot_in_parameters; auto.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact SEPFINAL.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. exact SAME. exact INCR.
Qed.

(** The following lemmas show the correctness of the register reloading
  code generated by [reload_callee_save]: after this code has executed,
  all callee-save registers contain the same values they had at
  function entry. *)

Section RESTORE_CALLEE_SAVE.

Variable j: meminj.
Variable cs: list stackframe.
Variable fb: block.
Variable sp: block.
Variable ls0: locset.
Variable m: mem.

Definition agree_unused (ls0: locset) (rs: regset) : Prop :=
  forall r, ~(mreg_within_bounds b r) -> Val.inject j (ls0 (R r)) (rs r).

Lemma restore_callee_save_rec_correct:
  forall l ofs rs k,
  m |= contains_callee_saves j sp ofs l ls0 ->
  agree_unused ls0 rs ->
  (forall r, In r l -> mreg_within_bounds b r) ->
  exists rs',
    star step tge
      (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save_rec l ofs k) rs m)
   E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
  /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r))
  /\ (forall r, ~(In r l) -> rs' r = rs r)
  /\ agree_unused ls0 rs'.
Proof.
Local Opaque mreg_type.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction l as [ | r l]; simpl; intros.
- (* base case *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists rs. intuition auto. apply star_refl.
- (* inductive case *)
  set (ty := mreg_type r) in *.
  set (sz := AST.typesize ty) in *.
  set (ofs1 := align ofs sz).
  assert (SZPOS: sz > 0) by (apply AST.typesize_pos).
  assert (OFSLE: ofs <= ofs1) by (apply align_le; auto).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  assert (BOUND: mreg_within_bounds b r) by eauto.
  exploit contains_get_stack.
    eapply sep_proj1; eassumption.
  intros (v & LOAD & SPEC).
  exploit (IHl (ofs1 + sz) (rs#r <- v)).
    eapply sep_proj2; eassumption.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
    red; intros. rewrite Regmap.gso. auto. intuition congruence.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    eauto.
  intros (rs' & A & B & C & D).
  exists rs'.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  split. eapply star_step; eauto.
(* Goal: Val.inject_list j (@nil val) (@nil val) *)
(* Goal: @ex (list val) (fun vl : list val => and (@list_forall2 (rpair loc) val (extcall_arg_pair rs m' (parent_sp cs')) (@cons (rpair loc) a locs) vl) (Val.inject_list j (@cons val (Locmap.getpair a ls) (@map (rpair loc) val (fun p : rpair loc => Locmap.getpair p ls) locs)) vl)) *)
    econstructor. exact LOAD. traceEq.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split. intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    destruct (In_dec mreg_eq r0 l). auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    assert (r = r0) by tauto. subst r0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    rewrite C by auto. rewrite Regmap.gss. exact SPEC.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split. intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    rewrite C by tauto. apply Regmap.gso. intuition auto.
  exact D.
Qed.

End RESTORE_CALLEE_SAVE.

Lemma restore_callee_save_correct:
  forall m j sp ls ls0 pa ra P rs k cs fb,
  m |= frame_contents j sp ls ls0 pa ra ** P ->
  agree_unused j ls0 rs ->
  exists rs',
    star step tge
       (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save fe k) rs m)
    E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
  /\ (forall r,
        is_callee_save r = true -> Val.inject j (ls0 (R r)) (rs' r))
  /\ (forall r,
        is_callee_save r = false -> rs' r = rs r).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros.
  unfold frame_contents, frame_contents_1 in H.
(* Goal: @eq (option val) (load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr (fe_ofs_retaddr fe))) (@Some val retaddr) *)
  apply mconj_proj1 in H. rewrite ! sep_assoc in H. apply sep_pick5 in H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit restore_callee_save_rec_correct; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; unfold mreg_within_bounds; auto.
  intros (rs' & A & B & C & D).
  exists rs'.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. eexact A.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split; intros.
  destruct (In_dec mreg_eq r (used_callee_save b)).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply B; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite C by auto. apply H0. unfold mreg_within_bounds; tauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  apply C. red; intros. apply (used_callee_save_prop b) in H2. congruence.
Qed.

(** As a corollary, we obtain the following correctness result for
  the execution of a function epilogue (reloading of used callee-save
  registers + reloading of the link and return address + freeing
  of the frame). *)

Lemma function_epilogue_correct:
  forall m' j sp' ls ls0 pa ra P m rs sp m1 k cs fb,
  m' |= frame_contents j sp' ls ls0 pa ra ** minjection j m ** P ->
  agree_regs j ls rs ->
  agree_locs ls ls0 ->
  j sp = Some(sp', fe.(fe_stack_data)) ->
  Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 ->
  exists rs1, exists m1',
     load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) = Some pa
  /\ load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) = Some ra
  /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1'
  /\ star step tge
       (State cs fb (Vptr sp' Ptrofs.zero) (restore_callee_save fe k) rs m')
    E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs1 m')
  /\ agree_regs j (return_regs ls0 ls) rs1
  /\ agree_callee_save (return_regs ls0 ls) ls0
  /\ m1' |= minjection j m1 ** P.
Proof.
  intros until fb; intros SEP AGR AGL INJ FREE.
  (* Can free *)
  exploit free_parallel_rule.
    rewrite <- sep_assoc. eapply mconj_proj2. eexact SEP.
    eexact FREE.
    eexact INJ.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    auto. rewrite Z.max_comm; reflexivity.
  intros (m1' & FREE' & SEP').
  (* Reloading the callee-save registers *)
  exploit restore_callee_save_correct.
    eexact SEP.
    instantiate (1 := rs).
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
    red; intros. destruct AGL. rewrite <- agree_unused_reg0 by auto. apply AGR.
  intros (rs' & LOAD_CS & CS & NCS).
  (* Reloading the back link and return address *)
  unfold frame_contents in SEP; apply mconj_proj1 in SEP.
  unfold frame_contents_1 in SEP; rewrite ! sep_assoc in SEP.
  exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick3; eexact SEP. intros LOAD_LINK.
  exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick4; eexact SEP. intros LOAD_RETADDR.
  clear SEP.
  (* Conclusions *)
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  rewrite unfold_transf_function; simpl.
  exists rs', m1'.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. assumption.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. assumption.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. assumption.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  split. eassumption.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split. red; unfold return_regs; intros.
    destruct (is_callee_save r) eqn:C.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply CS; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    rewrite NCS by auto. apply AGR.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  split. red; unfold return_regs; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    destruct l. rewrite H; auto. destruct sl; auto; contradiction. 
(* Goal: m_pred (sepconj (mconj (sepconj (contains_locations j sp (fe_ofs_local fe) (bound_local b) Local ls) (sepconj (contains_locations j sp fe_ofs_arg (bound_outgoing b) Outgoing ls) (sepconj (hasvalue Mptr sp (fe_ofs_link fe) parent) (sepconj (hasvalue Mptr sp (fe_ofs_retaddr fe) retaddr) (contains_callee_saves j sp (fe_ofs_callee_save fe) (used_callee_save b) ls0))))) (sepconj (range sp Z0 (fe_stack_data fe)) (range sp (Z.add (fe_stack_data fe) (bound_stack_data b)) (fe_size fe)))) P) m *)
  assumption.
Qed.

End FRAME_PROPERTIES.

(** * Call stack invariants *)

(** This is the memory assertion that captures the contents of the stack frames
  mentioned in the call stacks. *)

Fixpoint stack_contents (j: meminj) (cs: list Linear.stackframe) (cs': list Mach.stackframe) : massert :=
  match cs, cs' with
  | nil, nil => pure True
  | Linear.Stackframe f _ ls c :: cs, Mach.Stackframe fb (Vptr sp' _) ra c' :: cs' =>
      frame_contents f j sp' ls (parent_locset cs) (parent_sp cs') (parent_ra cs')
      ** stack_contents j cs cs'
  | _, _ => pure False
  end.

(** [match_stacks] captures additional properties (not related to memory)
  of the Linear and Mach call stacks. *)

Inductive match_stacks (j: meminj):
       list Linear.stackframe -> list stackframe -> signature -> Prop :=
  | match_stacks_empty: forall sg,
      tailcall_possible sg ->
      match_stacks j nil nil sg
  | match_stacks_cons: forall f sp ls c cs fb sp' ra c' cs' sg trf
        (TAIL: is_tail c (Linear.fn_code f))
        (FINDF: Genv.find_funct_ptr tge fb = Some (Internal trf))
        (TRF: transf_function f = OK trf)
        (TRC: transl_code (make_env (function_bounds f)) c = c')
        (INJ: j sp = Some(sp', (fe_stack_data (make_env (function_bounds f)))))
        (TY_RA: Val.has_type ra Tptr)
        (AGL: agree_locs f ls (parent_locset cs))
        (ARGS: forall ofs ty,
           In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) ->
           slot_within_bounds (function_bounds f) Outgoing ofs ty)
        (STK: match_stacks j cs cs' (Linear.fn_sig f)),
      match_stacks j
                   (Linear.Stackframe f (Vptr sp Ptrofs.zero) ls c :: cs)
                   (Stackframe fb (Vptr sp' Ptrofs.zero) ra c' :: cs')
                   sg.

(** Invariance with respect to change of memory injection. *)

Lemma stack_contents_change_meminj:
  forall m j j', inject_incr j j' ->
  forall cs cs' P,
  m |= stack_contents j cs cs' ** P ->
  m |= stack_contents j' cs cs' ** P.
Proof.
Local Opaque sepconj.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  induction cs as [ | [] cs]; destruct cs' as [ | [] cs']; simpl; intros; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct sp0; auto.
  rewrite sep_assoc in *.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_contents_incr with (j := j); auto.
(* Goal: m_pred (sepconj (mconj (sepconj (contains_locations j sp (fe_ofs_local fe) (bound_local b) Local ls) (sepconj (contains_locations j sp fe_ofs_arg (bound_outgoing b) Outgoing ls) (sepconj (hasvalue Mptr sp (fe_ofs_link fe) parent) (sepconj (hasvalue Mptr sp (fe_ofs_retaddr fe) retaddr) (contains_callee_saves j sp (fe_ofs_callee_save fe) (used_callee_save b) ls0))))) (sepconj (range sp Z0 (fe_stack_data fe)) (range sp (Z.add (fe_stack_data fe) (bound_stack_data b)) (fe_size fe)))) P) m *)
  rewrite sep_swap. apply IHcs. rewrite sep_swap. assumption.
Qed.

Lemma match_stacks_change_meminj:
  forall j j', inject_incr j j' ->
  forall cs cs' sg,
  match_stacks j cs cs' sg ->
  match_stacks j' cs cs' sg.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction 2; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- constructor; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- econstructor; eauto.
Qed.

(** Invariance with respect to change of signature. *)

Lemma match_stacks_change_sig:
  forall sg1 j cs cs' sg,
  match_stacks j cs cs' sg ->
  tailcall_possible sg1 ->
  match_stacks j cs cs' sg1.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction 1; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  econstructor; eauto. intros. elim (H0 _ H1).
Qed.

(** Typing properties of [match_stacks]. *)

Lemma match_stacks_type_sp:
  forall j cs cs' sg,
  match_stacks j cs cs' sg ->
  Val.has_type (parent_sp cs') Tptr.
Proof.
(* Goal: forall (j : Val.meminj) (cs : list Linear.stackframe) (cs' : list stackframe) (sg : signature) (_ : match_stacks j cs cs' sg), Val.has_type (parent_sp cs') Tptr *)
  induction 1; unfold parent_sp. apply Val.Vnullptr_has_type. apply Val.Vptr_has_type.
Qed.

Lemma match_stacks_type_retaddr:
  forall j cs cs' sg,
  match_stacks j cs cs' sg ->
  Val.has_type (parent_ra cs') Tptr.
Proof.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  induction 1; unfold parent_ra. apply Val.Vnullptr_has_type. auto.
Qed.

(** * Syntactic properties of the translation *)

(** Preservation of code labels through the translation. *)

Section LABELS.

Remark find_label_save_callee_save:
  forall lbl l ofs k,
  Mach.find_label lbl (save_callee_save_rec l ofs k) = Mach.find_label lbl k.
Proof.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  induction l; simpl; auto.
Qed.

Remark find_label_restore_callee_save:
  forall lbl l ofs k,
  Mach.find_label lbl (restore_callee_save_rec l ofs k) = Mach.find_label lbl k.
Proof.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  induction l; simpl; auto.
Qed.

Lemma transl_code_eq:
  forall fe i c, transl_code fe (i :: c) = transl_instr fe i (transl_code fe c).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold transl_code; intros. rewrite list_fold_right_eq. auto.
Qed.

Lemma find_label_transl_code:
  forall fe lbl c,
  Mach.find_label lbl (transl_code fe c) =
    option_map (transl_code fe) (Linear.find_label lbl c).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction c; simpl; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
- rewrite transl_code_eq.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct a; unfold transl_instr; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct s; simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct s; simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold restore_callee_save. rewrite find_label_restore_callee_save. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  simpl. destruct (peq lbl l). reflexivity. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold restore_callee_save. rewrite find_label_restore_callee_save. auto.
Qed.

Lemma transl_find_label:
  forall f tf lbl c,
  transf_function f = OK tf ->
  Linear.find_label lbl f.(Linear.fn_code) = Some c ->
  Mach.find_label lbl tf.(Mach.fn_code) =
    Some (transl_code (make_env (function_bounds f)) c).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. rewrite (unfold_transf_function _ _ H).  simpl.
(* Goal: @eq (option code) (find_label lbl (transl_body f (make_env (function_bounds f)))) (@Some code (transl_code (make_env (function_bounds f)) c)) *)
  unfold transl_body. unfold save_callee_save. rewrite find_label_save_callee_save.
(* Goal: @eq bool (andb true true) true *)
  rewrite find_label_transl_code. rewrite H0. reflexivity.
Qed.

End LABELS.

(** Code tail property for Linear executions. *)

Lemma find_label_tail:
  forall lbl c c',
  Linear.find_label lbl c = Some c' -> is_tail c' c.
Proof.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  induction c; simpl.
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (@None Linear.code) (@Some Linear.code c')), @is_tail Linear.instruction c' (@nil Linear.instruction) *)
(* Goal: forall (c' : Linear.code) (_ : @eq (option Linear.code) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c) (@Some Linear.code c')), @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  intros; discriminate.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intro c'. case (Linear.is_label lbl a); intros.
(* Goal: @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
(* Goal: @is_tail Linear.instruction c' (@cons Linear.instruction a c) *)
  injection H; intro; subst c'. auto with coqlib.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  auto with coqlib.
Qed.

(** Code tail property for translations *)

Lemma is_tail_save_callee_save:
  forall l ofs k,
  is_tail k (save_callee_save_rec l ofs k).
Proof.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  induction l; intros; simpl. auto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  constructor; auto.
Qed.

Lemma is_tail_restore_callee_save:
  forall l ofs k,
  is_tail k (restore_callee_save_rec l ofs k).
Proof.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  induction l; intros; simpl. auto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  constructor; auto.
Qed.

Lemma is_tail_transl_instr:
  forall fe i k,
  is_tail k (transl_instr fe i k).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct i; unfold transl_instr; auto with coqlib.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  destruct s; auto with coqlib.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  destruct s; auto with coqlib.
(* Goal: @eq (option code) (find_label lbl (restore_callee_save fe (@cons instruction Mreturn (transl_code fe c)))) (@option_map (list Linear.instruction) code (transl_code fe) (if Linear.is_label lbl Lreturn then @Some (list Linear.instruction) c else Linear.find_label lbl c)) *)
  unfold restore_callee_save.  eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib.
(* Goal: @eq (option code) (find_label lbl (restore_callee_save fe (@cons instruction Mreturn (transl_code fe c)))) (@option_map (list Linear.instruction) code (transl_code fe) (if Linear.is_label lbl Lreturn then @Some (list Linear.instruction) c else Linear.find_label lbl c)) *)
  unfold restore_callee_save.  eapply is_tail_trans. 2: apply is_tail_restore_callee_save. auto with coqlib.
Qed.

Lemma is_tail_transl_code:
  forall fe c1 c2, is_tail c1 c2 -> is_tail (transl_code fe c1) (transl_code fe c2).
Proof.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  induction 1; simpl. auto with coqlib.
(* Goal: @eq (option code) (find_label lbl (transl_code fe (@cons Linear.instruction a c))) (@option_map (list Linear.instruction) code (transl_code fe) (if Linear.is_label lbl a then @Some (list Linear.instruction) c else Linear.find_label lbl c)) *)
  rewrite transl_code_eq.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply is_tail_trans. eauto. apply is_tail_transl_instr.
Qed.

Lemma is_tail_transf_function:
  forall f tf c,
  transf_function f = OK tf ->
  is_tail c (Linear.fn_code f) ->
  is_tail (transl_code (make_env (function_bounds f)) c) (fn_code tf).
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. rewrite (unfold_transf_function _ _ H). simpl.
  unfold transl_body, save_callee_save.
  eapply is_tail_trans. 2: apply is_tail_save_callee_save.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply is_tail_transl_code; auto.
Qed.

(** * Semantic preservation *)

(** Preservation / translation of global symbols and functions. *)

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

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_transf_partial TRANSF).

Lemma function_ptr_translated:
  forall b f,
  Genv.find_funct_ptr ge b = Some f ->
  exists tf,
  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSF).

Lemma sig_preserved:
  forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f.
Proof.
(* Goal: forall (f : Linear.fundef) (tf : fundef) (_ : @eq (res fundef) (transf_fundef f) (@OK fundef tf)), @eq signature (funsig tf) (Linear.funsig f) *)
  intros until tf; unfold transf_fundef, transf_partial_fundef.
(* Goal: forall _ : @eq (res fundef) match f with | Internal f => @bind function (AST.fundef function) (transf_function f) (fun f' : function => @OK (AST.fundef function) (@Internal function f')) | External ef => @OK (AST.fundef function) (@External function ef) end (@OK fundef tf), @eq signature (funsig tf) (Linear.funsig f) *)
  destruct f; intros; monadInv H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite (unfold_transf_function _ _ EQ). auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
Qed.

Lemma find_function_translated:
  forall j ls rs m ros f,
  agree_regs j ls rs ->
  m |= globalenv_inject ge j ->
  Linear.find_function ge ros ls = Some f ->
  exists bf, exists tf,
     find_function_ptr tge ros rs = Some bf
  /\ Genv.find_funct_ptr tge bf = Some tf
  /\ transf_fundef f = OK tf.
Proof.
(* Goal: forall (j : Val.meminj) (ls : locset) (rs : regset) (m : Mem.mem) (ros : sum mreg ident) (f : Linear.fundef) (_ : agree_regs j ls rs) (_ : m_pred (@globalenv_inject Linear.fundef unit ge j) m) (_ : @eq (option Linear.fundef) (find_function ge ros ls) (@Some Linear.fundef f)), @ex block (fun bf : block => @ex fundef (fun tf : fundef => and (@eq (option block) (find_function_ptr tge ros rs) (@Some block bf)) (and (@eq (option fundef) (@Genv.find_funct_ptr fundef unit tge bf) (@Some fundef tf)) (@eq (res fundef) (transf_fundef f) (@OK fundef tf))))) *)
  intros until f; intros AG [bound [_ [?????]]] FF.
(* Goal: @ex block (fun bf : block => @ex fundef (fun tf : fundef => and (@eq (option block) (find_function_ptr tge ros rs) (@Some block bf)) (and (@eq (option fundef) (@Genv.find_funct_ptr fundef unit tge bf) (@Some fundef tf)) (@eq (res fundef) (transf_fundef f) (@OK fundef tf))))) *)
  destruct ros; simpl in FF.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in FF.
(* Goal: @ex block (fun bf : block => @ex fundef (fun tf : fundef => and (@eq (option block) (find_function_ptr tge (@inl mreg ident m0) rs) (@Some block bf)) (and (@eq (option fundef) (@Genv.find_funct_ptr fundef unit tge bf) (@Some fundef tf)) (@eq (res fundef) (transf_fundef f) (@OK fundef tf))))) *)
  rewrite Genv.find_funct_find_funct_ptr in FF.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_ptr_translated; eauto. intros [tf [A B]].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists b; exists tf; split; auto. simpl.
(* Goal: @eq (option block) match rs m0 with | Vundef => @None block | Vint i => @None block | Vlong i => @None block | Vfloat f => @None block | Vsingle f => @None block | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then @Some block b else @None block end (@Some block b) *)
  generalize (AG m0). rewrite EQ. intro INJ. inv INJ.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto.
- destruct (Genv.find_symbol ge i) as [b|] eqn:?; try discriminate.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_ptr_translated; eauto. intros [tf [A B]].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists b; exists tf; split; auto. simpl.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite symbols_preserved. auto.
Qed.

(** Preservation of the arguments to an external call. *)

Section EXTERNAL_ARGUMENTS.

Variable j: meminj.
Variable cs: list Linear.stackframe.
Variable cs': list stackframe.
Variable sg: signature.
Variables bound bound': block.
Hypothesis MS: match_stacks j cs cs' sg.
Variable ls: locset.
Variable rs: regset.
Hypothesis AGR: agree_regs j ls rs.
Hypothesis AGCS: agree_callee_save ls (parent_locset cs).
Hypothesis AGARGS: agree_outgoing_arguments sg ls (parent_locset cs).
Variable m': mem.
Hypothesis SEP: m' |= stack_contents j cs cs'.

Lemma transl_external_argument:
  forall l,
  In l (regs_of_rpairs (loc_arguments sg)) ->
  exists v, extcall_arg rs m' (parent_sp cs') l v /\ Val.inject j (ls l) v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros.
(* Goal: @ex val (fun v : val => and (extcall_arg rs m' (parent_sp cs') l v) (Val.inject j (ls l) v)) *)
  assert (loc_argument_acceptable l) by (apply loc_arguments_acceptable_2 with sg; auto).
(* Goal: agree_locs ls' ls0 *)
  destruct l; red in H0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- exists (rs r); split. constructor. auto.
- destruct sl; try contradiction.
(* Goal: @ex val (fun v : val => and (extcall_arg rs m' (parent_sp cs') (S Outgoing pos ty) v) (Val.inject j (ls (S Outgoing pos ty)) v)) *)
  inv MS.
+ elim (H1 _ H).
+ simpl in SEP. unfold parent_sp.
(* Goal: @ex val (fun v : val => and (extcall_arg rs m' (Vptr sp' Ptrofs.zero) (S Outgoing pos ty) v) (Val.inject j (ls (S Outgoing pos ty)) v)) *)
  assert (slot_valid f Outgoing pos ty = true).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { destruct H0. unfold slot_valid, proj_sumbool.
(* Goal: @eq bool (andb (if zle Z0 pos then true else false) (if Zdivide_dec (typealign ty) pos (typealign_pos ty) then true else false)) true *)
    rewrite zle_true by omega. rewrite pred_dec_true by auto. reflexivity. }
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit frame_get_outgoing; eauto. intros (v & A & B).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  exists v; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  constructor. exact A. rewrite AGARGS by auto. exact B. 
Qed.

Lemma transl_external_argument_2:
  forall p,
  In p (loc_arguments sg) ->
  exists v, extcall_arg_pair rs m' (parent_sp cs') p v /\ Val.inject j (Locmap.getpair p ls) v.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. destruct p as [l | l1 l2].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- destruct (transl_external_argument l) as (v & A & B). eapply in_regs_of_rpairs; eauto; simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists v; split; auto. constructor; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- destruct (transl_external_argument l1) as (v1 & A1 & B1). eapply in_regs_of_rpairs; eauto; simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (transl_external_argument l2) as (v2 & A2 & B2). eapply in_regs_of_rpairs; eauto; simpl; auto.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  exists (Val.longofwords v1 v2); split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  constructor; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.longofwords_inject; auto.
Qed.

Lemma transl_external_arguments_rec:
  forall locs,
  incl locs (loc_arguments sg) ->
  exists vl,
      list_forall2 (extcall_arg_pair rs m' (parent_sp cs')) locs vl
   /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) locs) vl.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  induction locs; simpl; intros.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  exists (@nil val); split. constructor. constructor.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  exploit transl_external_argument_2; eauto with coqlib. intros [v [A B]].
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  exploit IHlocs; eauto with coqlib. intros [vl [C D]].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists (v :: vl); split; constructor; auto.
Qed.

Lemma transl_external_arguments:
  exists vl,
      extcall_arguments rs m' (parent_sp cs') sg vl
   /\ Val.inject_list j (map (fun p => Locmap.getpair p ls) (loc_arguments sg)) vl.
Proof.
  unfold extcall_arguments.
  apply transl_external_arguments_rec.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  auto with coqlib.
Qed.

End EXTERNAL_ARGUMENTS.

(** Preservation of the arguments to a builtin. *)

Section BUILTIN_ARGUMENTS.

Variable f: Linear.function.
Let b := function_bounds f.
Let fe := make_env b.
Variable tf: Mach.function.
Hypothesis TRANSF_F: transf_function f = OK tf.
Variable j: meminj.
Variables m m': mem.
Variables ls ls0: locset.
Variable rs: regset.
Variables sp sp': block.
Variables parent retaddr: val.
Hypothesis INJ: j sp = Some(sp', fe.(fe_stack_data)).
Hypothesis AGR: agree_regs j ls rs.
Hypothesis SEP: m' |= frame_contents f j sp' ls ls0 parent retaddr ** minjection j m ** globalenv_inject ge j.

Lemma transl_builtin_arg_correct:
  forall a v,
  eval_builtin_arg ge ls (Vptr sp Ptrofs.zero) m a v ->
  (forall l, In l (params_of_builtin_arg a) -> loc_valid f l = true) ->
  (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_arg a) -> slot_within_bounds b sl ofs ty) ->
  exists v',
     eval_builtin_arg ge rs (Vptr sp' Ptrofs.zero) m' (transl_builtin_arg fe a) v'
  /\ Val.inject j v v'.
Proof.
  assert (SYMB: forall id ofs, Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { assert (G: meminj_preserves_globals ge j).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
    { eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. }
    intros; unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    destruct (Genv.find_symbol ge id) eqn:FS; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    destruct G. econstructor. eauto. rewrite Ptrofs.add_zero; auto. }
Local Opaque fe.
(* Goal: forall (al : list (builtin_arg loc)) (vl : list val) (_ : @eval_builtin_args loc (@Genv.to_senv Linear.fundef unit ge) ls (Vptr sp Ptrofs.zero) m al vl) (_ : forall (l : loc) (_ : @In loc l (@params_of_builtin_args loc al)), @eq bool (loc_valid f l) true) (_ : forall (sl : slot) (ofs : Z) (ty : typ) (_ : @In loc (S sl ofs ty) (@params_of_builtin_args loc al)), slot_within_bounds b sl ofs ty), @ex (list val) (fun vl' : list val => and (@eval_builtin_args RegEq.t (@Genv.to_senv Linear.fundef unit ge) rs (Vptr sp' Ptrofs.zero) m' (@map (builtin_arg loc) (builtin_arg mreg) (transl_builtin_arg fe) al) vl') (Val.inject_list j vl vl')) *)
  induction 1; simpl; intros VALID BOUNDS.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- assert (loc_valid f x = true) by auto.
  destruct x as [r | [] ofs ty]; try discriminate.
  + exists (rs r); auto with barg.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  + exploit frame_get_local; eauto. intros (v & A & B).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    exists v; split; auto. constructor; auto.
- econstructor; eauto with barg.
- econstructor; eauto with barg.
- econstructor; eauto with barg.
- econstructor; eauto with barg.
- set (ofs' := Ptrofs.add ofs (Ptrofs.repr (fe_stack_data fe))).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto.
  instantiate (1 := Val.offset_ptr (Vptr sp' Ptrofs.zero) ofs').
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  simpl. rewrite ! Ptrofs.add_zero_l. econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros (v' & A & B). exists v'; split; auto. constructor; auto.
- econstructor; split; eauto with barg.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  unfold Val.offset_ptr. rewrite ! Ptrofs.add_zero_l. econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto.
(* Goal: forall _ : @ex val (fun v0 : val => and (@eq (option val) (load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs)) (@Some val v0)) ((fun v' : val => @eq val v' v) v0)), @eq (option val) (load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs)) (@Some val v) *)
  intros (v' & A & B). exists v'; auto with barg.
- econstructor; split; eauto with barg.
- destruct IHeval_builtin_arg1 as (v1 & A1 & B1); auto using in_or_app.
  destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app.
  exists (Val.longofwords v1 v2); split; auto with barg.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply Val.longofwords_inject; auto.
- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); auto using in_or_app.
  destruct IHeval_builtin_arg2 as (v2' & A2 & B2); auto using in_or_app.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split. eauto with barg.
  destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
Qed.

Lemma transl_builtin_args_correct:
  forall al vl,
  eval_builtin_args ge ls (Vptr sp Ptrofs.zero) m al vl ->
  (forall l, In l (params_of_builtin_args al) -> loc_valid f l = true) ->
  (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_args al) -> slot_within_bounds b sl ofs ty) ->
  exists vl',
     eval_builtin_args ge rs (Vptr sp' Ptrofs.zero) m' (List.map (transl_builtin_arg fe) al) vl'
  /\ Val.inject_list j vl vl'.
Proof.
(* Goal: forall (al : list (builtin_arg loc)) (vl : list val) (_ : @eval_builtin_args loc (@Genv.to_senv Linear.fundef unit ge) ls (Vptr sp Ptrofs.zero) m al vl) (_ : forall (l : loc) (_ : @In loc l (@params_of_builtin_args loc al)), @eq bool (loc_valid f l) true) (_ : forall (sl : slot) (ofs : Z) (ty : typ) (_ : @In loc (S sl ofs ty) (@params_of_builtin_args loc al)), slot_within_bounds b sl ofs ty), @ex (list val) (fun vl' : list val => and (@eval_builtin_args RegEq.t (@Genv.to_senv Linear.fundef unit ge) rs (Vptr sp' Ptrofs.zero) m' (@map (builtin_arg loc) (builtin_arg mreg) (transl_builtin_arg fe) al) vl') (Val.inject_list j vl vl')) *)
  induction 1; simpl; intros VALID BOUNDS.
- exists (@nil val); split; constructor.
- exploit transl_builtin_arg_correct; eauto using in_or_app. intros (v1' & A & B).
(* Goal: @ex (list val) (fun vl' : list val => and (@eval_builtin_args RegEq.t (@Genv.to_senv Linear.fundef unit ge) rs (Vptr sp' Ptrofs.zero) m' (@cons (builtin_arg mreg) (transl_builtin_arg fe a1) (@map (builtin_arg loc) (builtin_arg mreg) (transl_builtin_arg fe) al)) vl') (Val.inject_list j (@cons val b1 bl) vl')) *)
  exploit IHlist_forall2; eauto using in_or_app. intros (vl' & C & D).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists (v1'::vl'); split; constructor; auto.
Qed.

End BUILTIN_ARGUMENTS.

(** The proof of semantic preservation relies on simulation diagrams
  of the following form:
<<
           st1 --------------- st2
            |                   |
           t|                  +|t
            |                   |
            v                   v
           st1'--------------- st2'
>>
  Matching between source and target states is defined by [match_states]
  below.  It implies:
- Satisfaction of the separation logic assertions that describe the contents
  of memory.  This is a separating conjunction of facts about:
-- the current stack frame
-- the frames in the call stack
-- the injection from the Linear memory state into the Mach memory state
-- the preservation of the global environment.
- Agreement between, on the Linear side, the location sets [ls]
  and [parent_locset s] of the current function and its caller,
  and on the Mach side the register set [rs].
- The Linear code [c] is a suffix of the code of the
  function [f] being executed.
- Well-typedness of [f].
*)

Inductive match_states: Linear.state -> Mach.state -> Prop :=
  | match_states_intro:
      forall cs f sp c ls m cs' fb sp' rs m' j tf
        (STACKS: match_stacks j cs cs' f.(Linear.fn_sig))
        (TRANSL: transf_function f = OK tf)
        (FIND: Genv.find_funct_ptr tge fb = Some (Internal tf))
        (AGREGS: agree_regs j ls rs)
        (AGLOCS: agree_locs f ls (parent_locset cs))
        (INJSP: j sp = Some(sp', fe_stack_data (make_env (function_bounds f))))
        (TAIL: is_tail c (Linear.fn_code f))
        (SEP: m' |= frame_contents f j sp' ls (parent_locset cs) (parent_sp cs') (parent_ra cs')
                 ** stack_contents j cs cs'
                 ** minjection j m
                 ** globalenv_inject ge j),
      match_states (Linear.State cs f (Vptr sp Ptrofs.zero) c ls m)
                   (Mach.State cs' fb (Vptr sp' Ptrofs.zero) (transl_code (make_env (function_bounds f)) c) rs m')
  | match_states_call:
      forall cs f ls m cs' fb rs m' j tf
        (STACKS: match_stacks j cs cs' (Linear.funsig f))
        (TRANSL: transf_fundef f = OK tf)
        (FIND: Genv.find_funct_ptr tge fb = Some tf)
        (AGREGS: agree_regs j ls rs)
        (SEP: m' |= stack_contents j cs cs'
                 ** minjection j m
                 ** globalenv_inject ge j),
      match_states (Linear.Callstate cs f ls m)
                   (Mach.Callstate cs' fb rs m')
  | match_states_return:
      forall cs ls m cs' rs m' j sg
        (STACKS: match_stacks j cs cs' sg)
        (AGREGS: agree_regs j ls rs)
        (SEP: m' |= stack_contents j cs cs'
                 ** minjection j m
                 ** globalenv_inject ge j),
      match_states (Linear.Returnstate cs ls m)
                  (Mach.Returnstate cs' rs m').

Theorem transf_step_correct:
  forall s1 t s2, Linear.step ge s1 t s2 ->
  forall (WTS: wt_state s1) s1' (MS: match_states s1 s1'),
  exists s2', plus step tge s1' t s2' /\ match_states s2 s2'.
Proof.
  induction 1; intros;
  try inv MS;
  try rewrite transl_code_eq;
  try (generalize (function_is_within_bounds f _ (is_tail_in TAIL));
       intro BOUND; simpl in BOUND);
  unfold transl_instr.

- (* Lgetstack *)
  destruct BOUND as [BOUND1 BOUND2].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit wt_state_getstack; eauto. intros SV.
  unfold destroyed_by_getstack; destruct sl.
+ (* Lgetstack, local *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit frame_get_local; eauto. intros (v & A & B).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: @eq (option val) (load_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr (Z.add fe_ofs_arg (Z.mul (Zpos (xO (xO xH))) pos)))) (@Some val v) *)
(* Goal: Val.inject j (ls (S Outgoing pos ty)) v *)
  apply plus_one. apply exec_Mgetstack. exact A.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto.
+ (* Lgetstack, incoming *)
  unfold slot_valid in SV. InvBooleans.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit incoming_slot_in_parameters; eauto. intros IN_ARGS.
  inversion STACKS; clear STACKS.
  elim (H1 _ IN_ARGS).
  subst s cs'.
  exploit frame_get_outgoing.
  apply sep_proj2 in SEP. simpl in SEP. rewrite sep_assoc in SEP. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply ARGS; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply slot_outgoing_argument_valid; eauto.
(* Goal: forall _ : @ex val (fun v : val => and (@eq (option val) (load_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr (offset_arg pos))) (@Some val v)) (Val.inject j (ls0 (S Outgoing pos ty)) v)), @ex val (fun v : val => and (extcall_arg rs m' (Vptr sp' Ptrofs.zero) (S Outgoing pos ty) v) (Val.inject j (ls (S Outgoing pos ty)) v)) *)
  intros (v & A & B).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. eapply exec_Mgetparam; eauto.
  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_link_ofs.
  eapply frame_get_parent. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto with coqlib. econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  erewrite agree_incoming by eauto. exact B.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto. apply agree_locs_undef_locs; auto.
+ (* Lgetstack, outgoing *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit frame_get_outgoing; eauto. intros (v & A & B).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: @eq (option val) (load_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr (Z.add fe_ofs_arg (Z.mul (Zpos (xO (xO xH))) pos)))) (@Some val v) *)
(* Goal: Val.inject j (ls (S Outgoing pos ty)) v *)
  apply plus_one. apply exec_Mgetstack. exact A.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto.

- (* Lsetstack *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit wt_state_setstack; eauto. intros (SV & SW).
  set (ofs' := match sl with
               | Local => offset_local (make_env (function_bounds f)) ofs
               | Incoming => 0 (* dummy *)
               | Outgoing => offset_arg ofs
               end).
  eapply frame_undef_regs with (rl := destroyed_by_setstack ty) in SEP.
  assert (A: exists m'',
              store_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr ofs') (rs0 src) = Some m''
           /\ m'' |= frame_contents f j sp' (Locmap.set (S sl ofs ty) (rs (R src))
                                               (LTL.undef_regs (destroyed_by_setstack ty) rs))
                                            (parent_locset s) (parent_sp cs') (parent_ra cs')
                  ** stack_contents j s cs' ** minjection j m ** globalenv_inject ge j).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { unfold ofs'; destruct sl; try discriminate.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    eapply frame_set_local; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    eapply frame_set_outgoing; eauto. }
  clear SEP; destruct A as (m'' & STORE & SEP).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
  apply plus_one. destruct sl; try discriminate.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    econstructor. eexact STORE. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    econstructor. eexact STORE. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor. eauto. eauto. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_slot. apply agree_regs_undef_regs. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_slot. apply agree_locs_undef_locs. auto. apply destroyed_by_setstack_caller_save. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eauto. eauto with coqlib. eauto.

- (* Lop *)
  assert (exists v',
          eval_operation ge (Vptr sp' Ptrofs.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
       /\ Val.inject j v v').
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_operation_inject; eauto.
  eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply agree_reglist; eauto.
  apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. exact SEP.
  destruct H0 as [v' [A B]].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject_list j (@nil val) (@nil val) *)
(* Goal: @ex (list val) (fun vl : list val => and (@list_forall2 (rpair loc) val (extcall_arg_pair rs m' (parent_sp cs')) (@cons (rpair loc) a locs) vl) (Val.inject_list j (@cons val (Locmap.getpair a ls) (@map (rpair loc) val (fun p : rpair loc => Locmap.getpair p ls) locs)) vl)) *)
  apply plus_one. econstructor.
  instantiate (1 := v'). rewrite <- A. apply eval_operation_preserved.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exact symbols_preserved. eauto.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite transl_destroyed_by_op.  apply agree_regs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg; auto. apply agree_locs_undef_locs. auto. apply destroyed_by_op_caller_save.
  apply frame_set_reg. apply frame_undef_regs. exact SEP.

- (* Lload *)
  assert (exists a',
          eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
       /\ Val.inject j a a').
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_addressing_inject; eauto.
  eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply agree_reglist; eauto.
  destruct H1 as [a' [A B]].
  exploit loadv_parallel_rule.
  apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eauto. eauto.
  intros [v' [C D]].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject_list j (@nil val) (@nil val) *)
(* Goal: @ex (list val) (fun vl : list val => and (@list_forall2 (rpair loc) val (extcall_arg_pair rs m' (parent_sp cs')) (@cons (rpair loc) a locs) vl) (Val.inject_list j (@cons val (Locmap.getpair a ls) (@map (rpair loc) val (fun p : rpair loc => Locmap.getpair p ls) locs)) vl)) *)
  apply plus_one. econstructor.
  instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eexact C. eauto.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.

- (* Lstore *)
  assert (exists a',
          eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
       /\ Val.inject j a a').
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_addressing_inject; eauto.
  eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply agree_reglist; eauto.
  destruct H1 as [a' [A B]].
  rewrite sep_swap3 in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit storev_parallel_rule. eexact SEP. eauto. eauto. apply AGREGS.
  clear SEP; intros (m1' & C & SEP).
  rewrite sep_swap3 in SEP.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject_list j (@nil val) (@nil val) *)
(* Goal: @ex (list val) (fun vl : list val => and (@list_forall2 (rpair loc) val (extcall_arg_pair rs m' (parent_sp cs')) (@cons (rpair loc) a locs) vl) (Val.inject_list j (@cons val (Locmap.getpair a ls) (@map (rpair loc) val (fun p : rpair loc => Locmap.getpair p ls) locs)) vl)) *)
  apply plus_one. econstructor.
  instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eexact C. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor. eauto. eauto. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite transl_destroyed_by_store. apply agree_regs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_undef_locs. auto. apply destroyed_by_store_caller_save.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto. eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply frame_undef_regs; eauto.

- (* Lcall *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit find_function_translated; eauto.
    eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
  intros [bf [tf' [A [B C]]]].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit is_tail_transf_function; eauto. intros IST.
  rewrite transl_code_eq in IST. simpl in IST.
  exploit return_address_offset_exists. eexact IST. intros [ra D].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.
(* Goal: Val.has_type (Vptr sp' Ptrofs.zero) Tptr *)
  apply Val.Vptr_has_type.
(* Goal: Loc.diff (R a) (R r) *)
  intros; red.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. 
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply loc_arguments_bounded; auto.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  simpl. rewrite sep_assoc. exact SEP.

- (* Ltailcall *)
  rewrite (sep_swap (stack_contents j s cs')) in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_epilogue_correct; eauto.
  clear SEP. intros (rs1 & m1' & P & Q & R & S & T & U & SEP).
  rewrite sep_swap in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit find_function_translated; eauto.
    eapply sep_proj2. eapply sep_proj2. eexact SEP.
  intros [bf [tf' [A [B C]]]].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply plus_right. eexact S. econstructor; eauto. traceEq.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply match_stacks_change_sig with (Linear.fn_sig f); auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply zero_size_arguments_tailcall_possible. eapply wt_state_tailcall; eauto.

- (* Lbuiltin *)
  destruct BOUND as [BND1 BND2].
  exploit transl_builtin_args_correct.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    eauto. eauto. rewrite sep_swap in SEP; apply sep_proj2 in SEP; eexact SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    eauto. rewrite <- forallb_forall. eapply wt_state_builtin; eauto.
    exact BND2.
  intros [vargs' [P Q]].
  rewrite <- sep_assoc, sep_comm, sep_assoc in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit external_call_parallel_rule; eauto.
  clear SEP; intros (j' & res' & m1' & EC & RES & SEP & INCR & ISEP).
  rewrite <- sep_assoc, sep_comm, sep_assoc in SEP.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  eapply match_states_intro with (j := j'); eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_stacks_change_meminj; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_set_res; auto. apply agree_regs_undef_regs; auto. eapply agree_regs_inject_incr; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_set_res; auto. apply agree_locs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_set_res. apply frame_undef_regs. apply frame_contents_incr with j; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite sep_swap2. apply stack_contents_change_meminj with j; auto. rewrite sep_swap2.
  exact SEP.

- (* Llabel *)
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
  apply plus_one; apply exec_Mlabel.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  econstructor; eauto with coqlib.

- (* Lgoto *)
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one; eapply exec_Mgoto; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply transl_find_label; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply find_label_tail; eauto.

- (* Lcond, true *)
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. eapply exec_Mcond_true; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_condition_inject with (m1 := m). eapply agree_reglist; eauto. apply sep_pick3 in SEP; exact SEP. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply transl_find_label; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor. eauto. eauto. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_undef_locs. auto. apply destroyed_by_cond_caller_save.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply find_label_tail; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_undef_regs; auto.

- (* Lcond, false *)
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. eapply exec_Mcond_false; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply eval_condition_inject with (m1 := m). eapply agree_reglist; eauto. apply sep_pick3 in SEP; exact SEP. auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor. eauto. eauto. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_undef_locs. auto. apply destroyed_by_cond_caller_save.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto. eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_undef_regs; auto.

- (* Ljumptable *)
  assert (rs0 arg = Vint n).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  { generalize (AGREGS arg). rewrite H. intro IJ; inv IJ; auto. }
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one; eapply exec_Mjumptable; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply transl_find_label; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor. eauto. eauto. eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_undef_regs; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_undef_locs. auto. apply destroyed_by_jumptable_caller_save.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto. eapply find_label_tail; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_undef_regs; auto.

- (* Lreturn *)
  rewrite (sep_swap (stack_contents j s cs')) in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_epilogue_correct; eauto.
  intros (rs' & m1' & A & B & C & D & E & F & G).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply plus_right. eexact D. econstructor; eauto. traceEq.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
  rewrite sep_swap; exact G.

- (* internal function *)
  revert TRANSL. unfold transf_fundef, transf_partial_fundef.
(* Goal: callee_save_loc (S Incoming ofs ty) *)
  destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence.
  intros EQ; inversion EQ; clear EQ; subst tf.
  rewrite sep_comm, sep_assoc in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_prologue_correct; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  red; intros; eapply wt_callstate_wt_regs; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_stacks_type_sp; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_stacks_type_retaddr; eauto.
  clear SEP;
  intros (j' & rs' & m2' & sp' & m3' & m4' & m5' & A & B & C & D & E & F & SEP & J & K).
  rewrite (sep_comm (globalenv_inject ge j')) in SEP.
  rewrite (sep_swap (minjection j' m')) in SEP.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply plus_left. econstructor; eauto.
(* Goal: @eq (option code) (find_label lbl (transl_body f (make_env (function_bounds f)))) (@Some code (transl_code (make_env (function_bounds f)) c)) *)
  rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body.
  eexact D. traceEq.
(* Goal: @is_tail instruction k k *)
(* Goal: @is_tail instruction k (@cons instruction (Mgetstack (Ptrofs.repr (align ofs (AST.typesize (mreg_type a)))) (mreg_type a) a) (restore_callee_save_rec l (Z.add (align ofs (AST.typesize (mreg_type a))) (AST.typesize (mreg_type a))) k)) *)
  eapply match_states_intro with (j := j'); eauto with coqlib.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_stacks_change_meminj; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite sep_swap in SEP. rewrite sep_swap. eapply stack_contents_change_meminj; eauto.

- (* external function *)
  simpl in TRANSL. inversion TRANSL; subst tf.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]].
  rewrite sep_comm, sep_assoc in SEP.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit external_call_parallel_rule; eauto.
  intros (j' & res' & m1' & A & B & C & D & E).
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply plus_one. eapply exec_function_external; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  eapply match_states_return with (j := j').
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_stacks_change_meminj; eauto.
  apply agree_regs_set_pair. apply agree_regs_undef_caller_save_regs. 
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_regs_inject_incr with j; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply stack_contents_change_meminj with j; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite sep_comm, sep_assoc; auto.

- (* return *)
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  inv STACKS. exploit wt_returnstate_agree; eauto. intros [AGCS OUTU].
(* Goal: @ex val (fun v : val => and (extcall_arg rs m' (parent_sp (@cons stackframe (Stackframe fb (Vptr sp' Ptrofs.zero) ra (transl_code (make_env (function_bounds f)) c)) cs'0)) (S Outgoing pos ty) v) (Val.inject j (ls (S Outgoing pos ty)) v)) *)
  simpl in AGCS. simpl in SEP. rewrite sep_assoc in SEP.
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
  apply plus_one. apply exec_return.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply agree_locs_return with rs0; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply frame_contents_exten with rs0 (parent_locset s); auto.
(* Goal: callee_save_loc (S Incoming ofs ty) *)
  intros; apply Val.lessdef_same; apply AGCS; red; congruence.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  intros; rewrite (OUTU ty ofs); auto. 
Qed.

Lemma transf_initial_states:
  forall st1, Linear.initial_state prog st1 ->
  exists st2, Mach.initial_state tprog st2 /\ match_states st1 st2.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. inv H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  econstructor; split.
(* Goal: Val.inject_list j (@nil val) (@nil val) *)
(* Goal: @ex (list val) (fun vl : list val => and (@list_forall2 (rpair loc) val (extcall_arg_pair rs m' (parent_sp cs')) (@cons (rpair loc) a locs) vl) (Val.inject_list j (@cons val (Locmap.getpair a ls) (@map (rpair loc) val (fun p : rpair loc => Locmap.getpair p ls) locs)) vl)) *)
  econstructor.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply (Genv.init_mem_transf_partial TRANSF); eauto.
  rewrite (match_program_main TRANSF).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  rewrite symbols_preserved. eauto.
  set (j := Mem.flat_inj (Mem.nextblock m0)).
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply match_states_call with (j := j); eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  red; simpl; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  simpl. rewrite sep_pure. split; auto. split;[|split].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply Genv.initmem_inject; eauto.
(* Goal: @eq (option block) (find_function_ptr tge (@inr mreg ident i) rs) (@Some block b) *)
  simpl. exists (Mem.nextblock m0); split. apply Ple_refl.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  unfold j, Mem.flat_inj; constructor; intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    apply pred_dec_true; auto.
(* Goal: callee_save_loc (S Incoming ofs ty) *)
    destruct (plt b1 (Mem.nextblock m0)); congruence.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
    change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  red; simpl; tauto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros. inv H0. inv H. inv STACKS.
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  assert (R: exists r, loc_result signature_main = One r).
(* Goal: @ex mreg (fun r : mreg => @eq (rpair mreg) (loc_result signature_main) (@One mreg r)) *)
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  { destruct (loc_result signature_main) as [r1 | r1 r2] eqn:LR.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  - exists r1; auto.
  - generalize (loc_result_type signature_main). rewrite LR. discriminate.
  }
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  destruct R as [rres EQ]. rewrite EQ in H1. simpl in H1.
(* Goal: final_state (Returnstate (@nil stackframe) rs0 m') r *)
  generalize (AGREGS rres). rewrite H1. intros A; inv A.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  econstructor; eauto.
Qed.

Lemma wt_prog:
  forall i fd, In (i, Gfun fd) prog.(prog_defs) -> wt_fundef fd.
Proof.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
  intros.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit list_forall2_in_left. eexact (proj1 TRANSF). eauto.
  intros ([i' g] & P & Q & R). simpl in *. inv R. destruct fd; simpl in *.
- monadInv H2. unfold transf_function in EQ.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  destruct (wt_function f). auto. discriminate.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
- auto.
Qed.

Theorem transf_program_correct:
  forward_simulation (Linear.semantics prog) (Mach.semantics return_address_offset tprog).
Proof.
  set (ms := fun s s' => wt_state s /\ match_states s s').
  eapply forward_simulation_plus with (match_states := ms).
- apply senv_preserved.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- intros. exploit transf_initial_states; eauto. intros [st2 [A B]].
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exists st2; split; auto. split; auto.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  apply wt_initial_state with (prog := prog); auto. exact wt_prog.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- intros. destruct H. eapply transf_final_states; eauto.
(* Goal: forall (st1 : Linear.state) (st2 : state) (r : Int.int) (_ : match_states st1 st2) (_ : Linear.final_state st1 r), final_state st2 r *)
- intros. destruct H0.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  exploit transf_step_correct; eauto. intros [s2' [A B]].
(* Goal: m_pred (sepconj (contains_locations j sp pos bound sl ls) P) m *)
  exists s2'; split. exact A. split.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  eapply step_type_preservation; eauto. eexact wt_prog. eexact H.
(* Goal: Val.inject j (ls (R r)) (rs r) *)
  auto.
Qed.

End PRESERVATION.
