(* *********************************************************************)
(*                                                                     *)
(*              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 Asm generation: machine-independent framework *)

Require Import Coqlib.
Require Intv.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Locations.
Require Import Mach.
Require Import Asm.
Require Import Asmgen.
Require Import Conventions.

(** * Processor registers and register states *)

Hint Extern 2 (_ <> _) => congruence: asmgen.

Lemma ireg_of_eq:
  forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
Proof.
(* Goal: forall (r : mreg) (r' : ireg) (_ : @eq (res ireg) (ireg_of r) (@OK ireg r')), @eq preg (preg_of r) (IR r') *)
  unfold ireg_of; intros. destruct (preg_of r); inv H; auto.
Qed.

Lemma freg_of_eq:
  forall r r', freg_of r = OK r' -> preg_of r = FR r'.
Proof.
(* Goal: @eq preg (preg_of r) (FR r') *)
  unfold freg_of; intros. destruct (preg_of r); inv H; auto.
Qed.

Lemma preg_of_injective:
  forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
Proof.
(* Goal: forall (r1 r2 : mreg) (_ : @eq preg (preg_of r1) (preg_of r2)), @eq mreg r1 r2 *)
  destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
Qed.

Lemma preg_of_data:
  forall r, data_preg (preg_of r) = true.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct r; reflexivity.
Qed.
Hint Resolve preg_of_data: asmgen.

Lemma data_diff:
  forall r r',
  data_preg r = true -> data_preg r' = false -> r <> r'.
Proof.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  congruence.
Qed.
Hint Resolve data_diff: asmgen.

Lemma preg_of_not_SP:
  forall r, preg_of r <> SP.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold preg_of; destruct r; simpl; congruence.
Qed.

Lemma preg_of_not_PC:
  forall r, preg_of r <> PC.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply data_diff; auto with asmgen.
Qed.

Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.

Lemma nextinstr_pc:
  forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply Pregmap.gss.
Qed.

Lemma nextinstr_inv:
  forall r rs, r <> PC -> (nextinstr rs)#r = rs#r.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto.
Qed.

Lemma nextinstr_inv1:
  forall r rs, data_preg r = true -> (nextinstr rs)#r = rs#r.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply nextinstr_inv. red; intro; subst; discriminate.
Qed.

Lemma nextinstr_set_preg:
  forall rs m v,
  (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold nextinstr. rewrite Pregmap.gss.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite Pregmap.gso. auto. apply not_eq_sym. apply preg_of_not_PC.
Qed.

Lemma undef_regs_other:
  forall r rl rs,
  (forall r', In r' rl -> r <> r') ->
  undef_regs rl rs r = rs r.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction rl; simpl; intros. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite IHrl by auto. rewrite Pregmap.gso; auto.
Qed.

Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop :=
  match rl with
  | nil => True
  | r1 :: nil => r <> preg_of r1
  | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl
  end.

Remark preg_notin_charact:
  forall r rl,
  preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction rl; simpl; intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  tauto.
(* Goal: iff match rl with | nil => not (@eq preg r (preg_of a)) | cons m l => and (not (@eq preg r (preg_of a))) (preg_notin r rl) end (forall (mr : mreg) (_ : or (@eq mreg a mr) (@In mreg mr rl)), not (@eq preg r (preg_of mr))) *)
  destruct rl.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  simpl. split. intros. intuition congruence. auto.
(* Goal: and (@eq val (rs2 PC) (Vptr b (Ptrofs.add ofs Ptrofs.one))) (code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) (fn_code fn) c) *)
(* Goal: @ex Ptrofs.int (fun ofs' : Ptrofs.int => and (@eq val (rs3 PC) (Vptr b ofs')) (code_tail (Ptrofs.unsigned ofs') (fn_code fn) c')) *)
  rewrite IHrl. split.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros [A B]. intros. destruct H. congruence. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto.
Qed.

Lemma undef_regs_other_2:
  forall r rl rs,
  preg_notin r rl ->
  undef_regs (map preg_of rl) rs r = rs r.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply undef_regs_other. intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite preg_notin_charact in H. auto.
Qed.

(** * Agreement between Mach registers and processor registers *)

Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree {
  agree_sp: rs#SP = sp;
  agree_sp_def: sp <> Vundef;
  agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r))
}.

Lemma preg_val:
  forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. auto.
Qed.

Lemma preg_vals:
  forall ms sp rs, agree ms sp rs ->
  forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)).
Proof.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto.
Qed.

Lemma sp_val:
  forall ms sp rs, agree ms sp rs -> sp = rs#SP.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H; auto.
Qed.

Lemma ireg_val:
  forall ms sp rs r r',
  agree ms sp rs ->
  ireg_of r = OK r' ->
  Val.lessdef (ms r) rs#r'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto.
Qed.

Lemma freg_val:
  forall ms sp rs r r',
  agree ms sp rs ->
  freg_of r = OK r' ->
  Val.lessdef (ms r) (rs#r').
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto.
Qed.

Lemma agree_exten:
  forall ms sp rs rs',
  agree ms sp rs ->
  (forall r, data_preg r = true -> rs'#r = rs#r) ->
  agree ms sp rs'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. split; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite H0; auto. auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite H0; auto. apply preg_of_data.
Qed.

(** Preservation of register agreement under various assignments. *)

Lemma agree_set_mreg:
  forall ms sp rs r v rs',
  agree ms sp rs ->
  Val.lessdef v (rs'#(preg_of r)) ->
  (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') ->
  agree (Regmap.set r v ms) sp rs'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. split; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite H1. auto. apply preg_of_data.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  red; intros; elim n. eapply preg_of_injective; eauto.
Qed.

Corollary agree_set_mreg_parallel:
  forall ms sp rs r v v',
  agree ms sp rs ->
  Val.lessdef v v' ->
  agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto.
Qed.

Lemma agree_set_other:
  forall ms sp rs r v,
  agree ms sp rs ->
  data_preg r = false ->
  agree ms sp (rs#r <- v).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply agree_exten with rs. auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply Pregmap.gso. congruence.
Qed.

Lemma agree_nextinstr:
  forall ms sp rs,
  agree ms sp rs -> agree ms sp (nextinstr rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold nextinstr. apply agree_set_other. auto. auto.
Qed.

Lemma agree_set_pair:
  forall sp p v v' ms rs,
  agree ms sp rs ->
  Val.lessdef v v' ->
  agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct p; simpl.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- apply agree_set_mreg_parallel; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
Qed.

Lemma agree_undef_nondata_regs:
  forall ms sp rl rs,
  agree ms sp rs ->
  (forall r, In r rl -> data_preg r = false) ->
  agree ms sp (undef_regs rl rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction rl; simpl; intros. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply IHrl. apply agree_exten with rs; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply Pregmap.gso. red; intros; subst.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  assert (data_preg a = false) by auto. congruence.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply H0; auto.
Qed.

Lemma agree_undef_regs:
  forall ms sp rl rs rs',
  agree ms sp rs ->
  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
  agree (Mach.undef_regs rl ms) sp rs'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. split; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite <- agree_sp0. apply H0; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct (In_dec mreg_eq r rl).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite Mach.undef_regs_same; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite Mach.undef_regs_other; auto. rewrite H0; auto.
(* Goal: @eq bool (data_preg (preg_of r)) true *)
(* Goal: preg_notin (preg_of r) rl *)
  apply preg_of_data.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  rewrite preg_notin_charact. intros; red; intros. elim n.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  exploit preg_of_injective; eauto. congruence.
Qed.

Lemma agree_undef_regs2:
  forall ms sp rl rs rs',
  agree (Mach.undef_regs rl ms) sp rs ->
  (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') ->
  agree (Mach.undef_regs rl ms) sp rs'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. split; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite <- agree_sp0. apply H0; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct (In_dec mreg_eq r rl).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite Mach.undef_regs_same; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite H0; auto.
(* Goal: @eq bool (data_preg (preg_of r)) true *)
(* Goal: preg_notin (preg_of r) rl *)
  apply preg_of_data.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  rewrite preg_notin_charact. intros; red; intros. elim n.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  exploit preg_of_injective; eauto. congruence.
Qed.

Lemma agree_set_undef_mreg:
  forall ms sp rs r v rl rs',
  agree ms sp rs ->
  Val.lessdef v (rs'#(preg_of r)) ->
  (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') ->
  agree (Regmap.set r v (Mach.undef_regs rl ms)) sp rs'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply agree_undef_regs with rs; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)).
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  congruence. auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite Pregmap.gso; auto.
Qed.

Lemma agree_undef_caller_save_regs:
  forall ms sp rs,
  agree ms sp rs ->
  agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- unfold proj_sumbool; rewrite dec_eq_true. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
+ apply list_in_map_inv in i. destruct i as (mr & A & B). 
(* Goal: Val.lessdef (if is_callee_save r then ms r else Vundef) (rs (preg_of r)) *)
  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
+ destruct (is_callee_save r) eqn:CS; auto.
(* Goal: Val.lessdef (ms r) Vundef *)
  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
Qed.

Lemma agree_change_sp:
  forall ms sp rs sp',
  agree ms sp rs -> sp' <> Vundef ->
  agree ms sp' (rs#SP <- sp').
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H. split; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite Pregmap.gso; auto with asmgen.
Qed.

(** Connection between Mach and Asm calling conventions for external
    functions. *)

Lemma extcall_arg_match:
  forall ms sp rs m m' l v,
  agree ms sp rs ->
  Mem.extends m m' ->
  Mach.extcall_arg ms m sp l v ->
  exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H1.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto.
  unfold load_stack in H2.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit Mem.loadv_extends; eauto. intros [v' [A B]].
  rewrite (sp_val _ _ _ H) in A.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists v'; split; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  econstructor. eauto. assumption.
Qed.

Lemma extcall_arg_pair_match:
  forall ms sp rs m m' p v,
  agree ms sp rs ->
  Mem.extends m m' ->
  Mach.extcall_arg_pair ms m sp p v ->
  exists v', Asm.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H1.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
Qed.

Lemma extcall_args_match:
  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
  forall ll vl,
  list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl ->
  exists vl', list_forall2 (Asm.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 3; intros.
(* Goal: and (@eq val (rs2 PC) (Vptr b (Ptrofs.add ofs Ptrofs.one))) (code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) (fn_code fn) c) *)
(* Goal: @ex Ptrofs.int (fun ofs' : Ptrofs.int => and (@eq val (rs3 PC) (Vptr b ofs')) (code_tail (Ptrofs.unsigned ofs') (fn_code fn) c')) *)
  exists (@nil val); split. constructor. constructor.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit extcall_arg_pair_match; eauto. intros [v1' [A B]].
(* Goal: @ex (list val) (fun vl' : list val => and (@eval_builtin_args PregEq.t ge rs sp m' (@cons (builtin_arg preg) (@map_builtin_arg mreg preg preg_of a1) (@map (builtin_arg mreg) (builtin_arg preg) (@map_builtin_arg mreg preg preg_of) al)) vl') (Val.lessdef_list (@cons val b1 bl) vl')) *)
  destruct IHlist_forall2 as [vl' [C D]].
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists (v1' :: vl'); split; constructor; auto.
Qed.

Lemma extcall_arguments_match:
  forall ms m m' sp rs sg args,
  agree ms sp rs -> Mem.extends m m' ->
  Mach.extcall_arguments ms m sp sg args ->
  exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  unfold Mach.extcall_arguments, Asm.extcall_arguments; intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eapply extcall_args_match; eauto.
Qed.

(** Translation of arguments and results to builtins. *)

Remark builtin_arg_match:
  forall ge (rs: regset) sp m a v,
  eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v ->
  eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v.
Proof.
(* Goal: forall (ge : Senv.t) (rs : regset) (sp : val) (m : Mem.mem) (a : builtin_arg mreg) (v : val) (_ : @eval_builtin_arg mreg ge (fun r : mreg => rs (preg_of r)) sp m a v), @eval_builtin_arg PregEq.t ge rs sp m (@map_builtin_arg mreg preg preg_of a) v *)
  induction 1; simpl; eauto with barg.
Qed.

Lemma builtin_args_match:
  forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
  forall al vl, eval_builtin_args ge ms sp m al vl ->
  exists vl', eval_builtin_args ge rs sp m' (map (map_builtin_arg preg_of) al) vl'
           /\ Val.lessdef_list vl vl'.
Proof.
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction 3; intros; simpl.
(* Goal: code_tail (Z.add (Z.sub pos' (Z.add pos (Zpos xH))) (Zpos xH)) (@cons instruction a c) c' *)
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c)))) *)
  exists (@nil val); split; constructor.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  intros; eapply preg_val; eauto.
(* Goal: forall _ : @ex val (fun v2 : val => and (@eval_builtin_arg RegEq.t ge (fun r : RegEq.t => rs (preg_of r)) sp m' a1 v2) (Val.lessdef b1 v2)), @ex (list val) (fun vl' : list val => and (@eval_builtin_args PregEq.t ge rs sp m' (@cons (builtin_arg preg) (@map_builtin_arg mreg preg preg_of a1) (@map (builtin_arg mreg) (builtin_arg preg) (@map_builtin_arg mreg preg preg_of) al)) vl') (Val.lessdef_list (@cons val b1 bl) vl')) *)
  intros (v1' & A & B).
(* Goal: @ex (list val) (fun vl' : list val => and (@eval_builtin_args PregEq.t ge rs sp m' (@cons (builtin_arg preg) (@map_builtin_arg mreg preg preg_of a1) (@map (builtin_arg mreg) (builtin_arg preg) (@map_builtin_arg mreg preg preg_of) al)) vl') (Val.lessdef_list (@cons val b1 bl) vl')) *)
  destruct IHlist_forall2 as [vl' [C D]].
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto.
Qed.

Lemma agree_set_res:
  forall res ms sp rs v v',
  agree ms sp rs ->
  Val.lessdef v v' ->
  agree (Mach.set_res res v ms) sp (Asm.set_res (map_builtin_res preg_of res) v' rs).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction res; simpl; intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply Pregmap.gso; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- apply IHres2. apply IHres1. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply Val.hiword_lessdef; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply Val.loword_lessdef; auto.
Qed.

Lemma set_res_other:
  forall r res v rs,
  data_preg r = false ->
  set_res (map_builtin_res preg_of res) v rs r = rs r.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction res; simpl; intros.
(* Goal: @eq val (@Pregmap.set val (preg_of x) v rs r) (rs r) *)
- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
- rewrite IHres2, IHres1; auto.
Qed.

(** * Correspondence between Mach code and Asm code *)

Lemma find_instr_in:
  forall c pos i,
  find_instr pos c = Some i -> In i c.
Proof.
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction c; simpl. intros; discriminate.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros until i. case (zeq pos 0); intros.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  left; congruence. right; eauto.
Qed.

(** The ``code tail'' of an instruction list [c] is the list of instructions
  starting at PC [pos]. *)

Inductive code_tail: Z -> code -> code -> Prop :=
  | code_tail_0: forall c,
      code_tail 0 c c
  | code_tail_S: forall pos i c1 c2,
      code_tail pos c1 c2 ->
      code_tail (pos + 1) (i :: c1) c2.

Lemma code_tail_pos:
  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
Proof.
(* Goal: forall (c1 c2 : list instruction) (_ : @is_tail instruction c1 c2), @ex Z (fun ofs : Z => code_tail ofs c2 c1) *)
  induction 1. omega. omega.
Qed.

Lemma find_instr_tail:
  forall c1 i c2 pos,
  code_tail pos c1 (i :: c2) ->
  find_instr pos c1 = Some i.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction c1; simpl; intros.
(* Goal: @eq (option instruction) (find_instr (Z.sub pos (Zpos xH)) c1) (@Some instruction i) *)
  inv H.
(* Goal: @eq (option instruction) (if zeq pos Z0 then @Some instruction a else find_instr (Z.sub pos (Zpos xH)) c1) (@Some instruction i) *)
  destruct (zeq pos 0). subst pos.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  inv H. auto. generalize (code_tail_pos _ _ _ H4). intro. omegaContradiction.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  inv H. congruence. replace (pos0 + 1 - 1) with pos0 by omega.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eauto.
Qed.

Remark code_tail_bounds_1:
  forall fn ofs c,
  code_tail ofs fn c -> 0 <= ofs <= list_length_z fn.
Proof.
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction 1; intros; simpl.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  generalize (list_length_z_pos c). omega.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  rewrite list_length_z_cons. omega.
Qed.

Remark code_tail_bounds_2:
  forall fn ofs i c,
  code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
Proof.
  assert (forall ofs fn c, code_tail ofs fn c ->
          forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction 1; intros; simpl.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eauto.
Qed.

Lemma code_tail_next:
  forall fn ofs i c,
  code_tail ofs fn (i :: c) ->
  code_tail (ofs + 1) fn c.
Proof.
  assert (forall ofs fn c, code_tail ofs fn c ->
          forall i c', c = i :: c' -> code_tail (ofs + 1) fn c').
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 1; intros.
(* Goal: code_tail (Z.add (Z.sub pos' (Z.add pos (Zpos xH))) (Zpos xH)) (@cons instruction a c) c' *)
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c)))) *)
  subst c. constructor. constructor.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  constructor. eauto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eauto.
Qed.

Lemma code_tail_next_int:
  forall fn ofs i c,
  list_length_z fn <= Ptrofs.max_unsigned ->
  code_tail (Ptrofs.unsigned ofs) fn (i :: c) ->
  code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) fn c.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  generalize (code_tail_bounds_2 _ _ _ _ H0). omega.
Qed.

(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points
  within the Asm code generated by translating Mach function [f],
  and [tc] is the tail of the generated code at the position corresponding
  to the code pointer [pc]. *)

Inductive transl_code_at_pc (ge: Mach.genv):
    val -> block -> Mach.function -> Mach.code -> bool -> Asm.function -> Asm.code -> Prop :=
  transl_code_at_pc_intro:
    forall b ofs f c ep tf tc,
    Genv.find_funct_ptr ge b = Some(Internal f) ->
    transf_function f = Errors.OK tf ->
    transl_code f c ep = OK tc ->
    code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc ->
    transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc.

(** Equivalence between [transl_code] and [transl_code']. *)

Local Open Scope error_monad_scope.

Lemma transl_code_rec_transl_code:
  forall f il ep k,
  transl_code_rec f il ep k = (do c <- transl_code f il ep; k c).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction il; simpl; intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto.
(* Goal: @eq (res code) (transl_code_rec f il (it1_is_parent ep a) (fun c1 : code => @bind (list instruction) code (transl_instr f a ep c1) (fun c2 : list instruction => k c2))) (@bind (list instruction) code (@bind (list instruction) (list instruction) (transl_code f il (it1_is_parent ep a)) (fun k : list instruction => transl_instr f a ep k)) (fun c : list instruction => k c)) *)
  rewrite IHil.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  destruct (transl_code f il (it1_is_parent ep a)); simpl; auto.
Qed.

Lemma transl_code'_transl_code:
  forall f il ep,
  transl_code' f il ep = transl_code f il ep.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. unfold transl_code'. rewrite transl_code_rec_transl_code.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  destruct (transl_code f il ep); auto.
Qed.

(** Predictor for return addresses in generated Asm code.

  The [return_address_offset] predicate defined here is used in the
  semantics for Mach to determine the return addresses that are
  stored in activation records. *)

(** Consider a Mach function [f] and a sequence [c] of Mach instructions
  representing the Mach code that remains to be executed after a
  function call returns.  The predicate [return_address_offset f c ofs]
  holds if [ofs] is the integer offset of the PPC instruction
  following the call in the Asm code obtained by translating the
  code of [f]. Graphically:
<<
     Mach function f    |--------- Mcall ---------|
         Mach code c    |                |--------|
                        |                 \        \
                        |                  \        \
                        |                   \        \
     Asm code           |                    |--------|
     Asm function       |------------- Pcall ---------|

                        <-------- ofs ------->
>>
*)

Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
  forall tf tc,
  transf_function f = OK tf ->
  transl_code f c false = OK tc ->
  code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc.

(** We now show that such an offset always exists if the Mach code [c]
  is a suffix of [f.(fn_code)].  This holds because the translation
  from Mach to PPC is compositional: each Mach instruction becomes
  zero, one or several PPC instructions, but the order of instructions
  is preserved. *)

Lemma is_tail_code_tail:
  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
Proof.
(* Goal: code_tail (Z.add (Z.sub pos' (Z.add pos (Zpos xH))) (Zpos xH)) (@cons instruction a c) c' *)
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c)))) *)
  induction 1. exists 0; constructor.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  destruct IHis_tail as [ofs CT]. exists (ofs + 1); constructor; auto.
Qed.

Section RETADDR_EXISTS.

Hypothesis transl_instr_tail:
  forall f i ep k c, transl_instr f i ep k = OK c -> is_tail k c.
Hypothesis transf_function_inv:
  forall f tf, transf_function f = OK tf ->
  exists tc, exists ep, transl_code f (Mach.fn_code f) ep = OK tc /\ is_tail tc (fn_code tf).
Hypothesis transf_function_len:
  forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned.

Lemma transl_code_tail:
  forall f c1 c2, is_tail c1 c2 ->
  forall tc2 ep2, transl_code f c2 ep2 = OK tc2 ->
  exists tc1, exists ep1, transl_code f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 1; simpl; intros.
(* Goal: @ex (list instruction) (fun tc1 : list instruction => @ex bool (fun ep1 : bool => and (@eq (res (list instruction)) (transl_code f c ep1) (@OK (list instruction) tc1)) (@is_tail instruction tc1 tc2))) *)
(* Goal: @ex (list instruction) (fun tc1 : list instruction => @ex bool (fun ep1 : bool => and (@eq (res (list instruction)) (transl_code f c1 ep1) (@OK (list instruction) tc1)) (@is_tail instruction tc1 tc2))) *)
  exists tc2; exists ep2; split; auto with coqlib.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  monadInv H0. exploit IHis_tail; eauto. intros [tc1 [ep1 [A B]]].
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists tc1; exists ep1; split. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply is_tail_trans with x. auto. eapply transl_instr_tail; eauto.
Qed.

Lemma return_address_exists:
  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
  exists ra, return_address_offset f c ra.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct (transf_function f) as [tf|] eqn:TF.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
+ exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit transl_code_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
Opaque transl_instr.
  monadInv TR2.
  assert (TL3: is_tail x (fn_code tf)).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  { apply is_tail_trans with tc1; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
    apply is_tail_trans with tc2; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
    eapply transl_instr_tail; eauto. }
  exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  exists (Ptrofs.repr ofs). red; intros.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  rewrite Ptrofs.unsigned_repr. congruence.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit code_tail_bounds_1; eauto.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  apply transf_function_len in TF. omega.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
+ exists Ptrofs.zero; red; intros. congruence.
Qed.

End RETADDR_EXISTS.

Remark code_tail_no_bigger:
  forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat.
Proof.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  induction 1; simpl; omega.
Qed.

Remark code_tail_unique:
  forall fn c pos pos',
  code_tail pos fn c -> code_tail pos' fn c -> pos = pos'.
Proof.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  f_equal. eauto.
Qed.

Lemma return_address_offset_correct:
  forall ge b ofs fb f c tf tc ofs',
  transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc ->
  return_address_offset f c ofs' ->
  ofs' = ofs.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H. red in H0.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exploit code_tail_unique. eexact H12. eapply H0; eauto. intro.
  rewrite <- (Ptrofs.repr_unsigned ofs).
  rewrite <- (Ptrofs.repr_unsigned ofs').
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  congruence.
Qed.

(** The [find_label] function returns the code tail starting at the
  given label.  A connection with [code_tail] is then established. *)

Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
  match c with
  | nil => None
  | instr :: c' =>
      if is_label lbl instr then Some c' else find_label lbl c'
  end.

Lemma label_pos_code_tail:
  forall lbl c pos c',
  find_label lbl c = Some c' ->
  exists pos',
  label_pos lbl pos c = Some pos'
  /\ code_tail (pos' - pos) c c'
  /\ pos < pos' <= pos + list_length_z c.
Proof.
(* Goal: forall (lbl : label) (c : code) (pos : Z) (c' : code) (_ : @eq (option code) (find_label lbl c) (@Some code c')), @ex Z (fun pos' : Z => and (@eq (option Z) (label_pos lbl pos c) (@Some Z pos')) (and (code_tail (Z.sub pos' pos) c c') (and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction c)))))) *)
  induction c.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  simpl; intros. discriminate.
(* Goal: forall (pos : Z) (c' : code) (_ : @eq (option code) (find_label lbl (@cons instruction a c)) (@Some code c')), @ex Z (fun pos' : Z => and (@eq (option Z) (label_pos lbl pos (@cons instruction a c)) (@Some Z pos')) (and (code_tail (Z.sub pos' pos) (@cons instruction a c) c') (and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c))))))) *)
  simpl; intros until c'.
(* Goal: forall _ : @eq (option code) (if is_label lbl a then @Some (list instruction) c else find_label lbl c) (@Some code c'), @ex Z (fun pos' : Z => and (@eq (option Z) (if is_label lbl a then @Some Z (Z.add pos (Zpos xH)) else label_pos lbl (Z.add pos (Zpos xH)) c) (@Some Z pos')) (and (code_tail (Z.sub pos' pos) (@cons instruction a c) c') (and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c))))))) *)
  case (is_label lbl a).
(* Goal: forall _ : @eq (option code) (@Some (list instruction) c) (@Some code c'), @ex Z (fun pos' : Z => and (@eq (option Z) (@Some Z (Z.add pos (Zpos xH))) (@Some Z pos')) (and (code_tail (Z.sub pos' pos) (@cons instruction a c) c') (and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c))))))) *)
(* Goal: forall _ : @eq (option code) (find_label lbl c) (@Some code c'), @ex Z (fun pos' : Z => and (@eq (option Z) (label_pos lbl (Z.add pos (Zpos xH)) c) (@Some Z pos')) (and (code_tail (Z.sub pos' pos) (@cons instruction a c) c') (and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c))))))) *)
  intro EQ; injection EQ; intro; subst c'.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists (pos + 1). split. auto. split.
(* Goal: code_tail (Z.add (Z.sub pos' (Z.add pos (Zpos xH))) (Zpos xH)) (@cons instruction a c) c' *)
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (@list_length_z instruction (@cons instruction a c)))) *)
  replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  rewrite list_length_z_cons. generalize (list_length_z_pos c). omega.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  exists pos'. split. auto. split.
  replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  constructor. auto.
(* Goal: and (Z.lt pos pos') (Z.le pos' (Z.add pos (Z.add (@list_length_z instruction c) (Zpos xH)))) *)
  rewrite list_length_z_cons. omega.
Qed.

(** Helper lemmas to reason about
- the "code is tail of" property
- correct translation of labels. *)

Definition tail_nolabel (k c: code) : Prop :=
  is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k.

Lemma tail_nolabel_refl:
  forall c, tail_nolabel c c.
Proof.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  intros; split. apply is_tail_refl. auto.
Qed.

Lemma tail_nolabel_trans:
  forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H; destruct H0; split.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eapply is_tail_trans; eauto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. rewrite H1; auto.
Qed.

Definition nolabel (i: instruction) :=
  match i with Plabel _ => False | _ => True end.

Hint Extern 1 (nolabel _) => exact I : labels.

Lemma tail_nolabel_cons:
  forall i c k,
  nolabel i -> tail_nolabel k c -> tail_nolabel k (i :: c).
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H0. split.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  constructor; auto.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
Qed.

Hint Resolve tail_nolabel_refl: labels.

Ltac TailNoLabel :=
  eauto with labels;
  match goal with
  | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel]
  | [ H: Error _ = OK _ |- _ ] => discriminate
  | [ H: assertion_failed = OK _ |- _ ] => discriminate
  | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel
  | [ H: bind _ _ = OK _ |- _ ] => monadInv H;  TailNoLabel
  | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel
  | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel
  | _ => idtac
  end.

Remark tail_nolabel_find_label:
  forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. auto.
Qed.

Remark tail_nolabel_is_tail:
  forall k c, tail_nolabel k c -> is_tail k c.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. destruct H. auto.
Qed.

(** * Execution of straight-line code *)

Section STRAIGHTLINE.

Variable ge: genv.
Variable fn: function.

(** Straight-line code is composed of processor instructions that execute
  in sequence (no branches, no function calls and returns).
  The following inductive predicate relates the machine states
  before and after executing a straight-line sequence of instructions.
  Instructions are taken from the first list instead of being fetched
  from memory. *)

Inductive exec_straight: code -> regset -> mem ->
                         code -> regset -> mem -> Prop :=
  | exec_straight_one:
      forall i1 c rs1 m1 rs2 m2,
      exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
      rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
      exec_straight (i1 :: c) rs1 m1 c rs2 m2
  | exec_straight_step:
      forall i c rs1 m1 rs2 m2 c' rs3 m3,
      exec_instr ge fn i rs1 m1 = Next rs2 m2 ->
      rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
      exec_straight c rs2 m2 c' rs3 m3 ->
      exec_straight (i :: c) rs1 m1 c' rs3 m3.

Lemma exec_straight_trans:
  forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
  exec_straight c1 rs1 m1 c2 rs2 m2 ->
  exec_straight c2 rs2 m2 c3 rs3 m3 ->
  exec_straight c1 rs1 m1 c3 rs3 m3.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 1; intros.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply exec_straight_step with rs2 m2; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply exec_straight_step with rs2 m2; auto.
Qed.

Lemma exec_straight_two:
  forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
  exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
  exec_instr ge fn i2 rs2 m2 = Next rs3 m3 ->
  rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
  rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one ->
  exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply exec_straight_step with rs2 m2; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply exec_straight_one; auto.
Qed.

Lemma exec_straight_three:
  forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
  exec_instr ge fn i1 rs1 m1 = Next rs2 m2 ->
  exec_instr ge fn i2 rs2 m2 = Next rs3 m3 ->
  exec_instr ge fn i3 rs3 m3 = Next rs4 m4 ->
  rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
  rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one ->
  rs4#PC = Val.offset_ptr rs3#PC Ptrofs.one ->
  exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. apply exec_straight_step with rs2 m2; auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eapply exec_straight_two; eauto.
Qed.

(** The following lemmas show that straight-line executions
  (predicate [exec_straight]) correspond to correct Asm executions. *)

Lemma exec_straight_steps_1:
  forall c rs m c' rs' m',
  exec_straight c rs m c' rs' m' ->
  list_length_z (fn_code fn) <= Ptrofs.max_unsigned ->
  forall b ofs,
  rs#PC = Vptr b ofs ->
  Genv.find_funct_ptr ge b = Some (Internal fn) ->
  code_tail (Ptrofs.unsigned ofs) (fn_code fn) c ->
  plus step ge (State rs m) E0 (State rs' m').
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 1; intros.
  apply plus_one.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  econstructor; eauto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eapply find_instr_tail. eauto.
  eapply plus_left'.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  econstructor; eauto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  eapply find_instr_tail. eauto.
  apply IHexec_straight with b (Ptrofs.add ofs Ptrofs.one).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto. rewrite H0. rewrite H3. reflexivity.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply code_tail_next_int with i; auto.
  traceEq.
Qed.

Lemma exec_straight_steps_2:
  forall c rs m c' rs' m',
  exec_straight c rs m c' rs' m' ->
  list_length_z (fn_code fn) <= Ptrofs.max_unsigned ->
  forall b ofs,
  rs#PC = Vptr b ofs ->
  Genv.find_funct_ptr ge b = Some (Internal fn) ->
  code_tail (Ptrofs.unsigned ofs) (fn_code fn) c ->
  exists ofs',
     rs'#PC = Vptr b ofs'
  /\ code_tail (Ptrofs.unsigned ofs') (fn_code fn) c'.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  induction 1; intros.
(* Goal: and (@eq val (rs2 PC) (Vptr b (Ptrofs.add ofs Ptrofs.one))) (code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) (fn_code fn) c) *)
(* Goal: @ex Ptrofs.int (fun ofs' : Ptrofs.int => and (@eq val (rs3 PC) (Vptr b ofs')) (code_tail (Ptrofs.unsigned ofs') (fn_code fn) c')) *)
  exists (Ptrofs.add ofs Ptrofs.one). split.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  rewrite H0. rewrite H2. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply code_tail_next_int with i1; auto.
(* Goal: @ex Ptrofs.int (fun ofs' : Ptrofs.int => and (@eq val (rs3 PC) (Vptr b ofs')) (code_tail (Ptrofs.unsigned ofs') (fn_code fn) c')) *)
  apply IHexec_straight with (Ptrofs.add ofs Ptrofs.one).
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto. rewrite H0. rewrite H3. reflexivity. auto.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  apply code_tail_next_int with i; auto.
Qed.

End STRAIGHTLINE.

(** * Properties of the Mach call stack *)

Section MATCH_STACK.

Variable ge: Mach.genv.

Inductive match_stack: list Mach.stackframe -> Prop :=
  | match_stack_nil:
      match_stack nil
  | match_stack_cons: forall fb sp ra c s f tf tc,
      Genv.find_funct_ptr ge fb = Some (Internal f) ->
      transl_code_at_pc ge ra fb f c false tf tc ->
      sp <> Vundef ->
      match_stack s ->
      match_stack (Stackframe fb sp ra c :: s).

Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
Proof.
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction 1; simpl.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  unfold Vnullptr; destruct Archi.ptr64; congruence.
(* Goal: @eq val (parent_ra s) (parent_ra s) *)
(* Goal: @eq val v Vundef *)
  auto.
Qed.

Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef.
Proof.
(* Goal: @eq (option code) (find_label lbl (@cons instruction i c)) (find_label lbl k) *)
  induction 1; simpl.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  unfold Vnullptr; destruct Archi.ptr64; congruence.
(* Goal: not (@eq val (Vptr fb ofs) Vundef) *)
  inv H0. congruence.
Qed.

Lemma lessdef_parent_sp:
  forall s v,
  match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H0. auto. exploit parent_sp_def; eauto. tauto.
Qed.

Lemma lessdef_parent_ra:
  forall s v,
  match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s.
Proof.
(* Goal: forall (s : list stackframe) (v : val) (_ : match_stack s) (_ : Val.lessdef (parent_ra s) v), @eq val v (parent_ra s) *)
  intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
Qed.

End MATCH_STACK.

