Require Import Coqlib Maps AST Integers Values Memory Events Globalenvs Smallstep.
Require Import Op Machregs Locations Stacklayout Conventions.
Require Import Mach Machblock OptionMonad.
Require Import Errors Datatypes PseudoAsmblock IterList.

(** Tiny translation from Machblock semantics to PseudoAsmblock semantics (needs additional checks) 
*)

Section TRANSLATION.

(* In the actual Asmblock code, the prologue will be inserted in the first block of the function.
   But, this block should have an empty header.
*)

Definition has_header (c: code) : bool :=
  match c with
  | nil => false
  | bb::_ => match header bb with
             | nil => false
             | _ => true
             end
  end.

Definition insert_implicit_prologue c :=
 if has_header c then {| header := nil; body := nil; exit := None |}::c else c.

Definition transl_function (f: function) : function :=
  {| fn_sig:=fn_sig f;
     fn_code:=insert_implicit_prologue (fn_code f);
     fn_stacksize := fn_stacksize f;
     fn_link_ofs := fn_link_ofs f;
     fn_retaddr_ofs := fn_retaddr_ofs f
 |}.

Definition transf_function (f: function) : res function :=
  let tf := transl_function f in
  (* removed because it is simpler or/and more efficient to perform this test in Asmblockgen !
  if zlt Ptrofs.max_unsigned (max_pos tf)
  then Error (msg "code size exceeded")
  else *) 
  OK tf.

Definition transf_fundef (f: fundef) : res fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: program) : res program :=
  transform_partial_program transf_fundef p.

End TRANSLATION.

(** Proof of the translation
*)

Require Import Linking.
Import PseudoAsmblock.AsmNotations.

Section PRESERVATION.

Definition match_prog (p: program) (tp: 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.
  intros. eapply match_transform_partial_program; eauto.
Qed.

Local Open Scope Z_scope.
Local Open Scope option_monad_scope.

Variable prog: program.
Variable tprog: program.

Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Variable next: function -> Z -> Z.

Hypothesis next_progress: forall (f:function) (pos:Z), (pos < (next f pos))%Z.

Definition max_pos (f:function) := iter (S (length f.(fn_code))) (next f) 0.

(* This hypothesis expresses that Asmgen checks for each tf 
   that (max_pos tf) represents a valid address
*)
Hypothesis functions_bound_max_pos: forall fb tf,
  Genv.find_funct_ptr tge fb = Some (Internal tf) ->
  (max_pos tf) <= Ptrofs.max_unsigned.

(** * Agreement between Mach registers and PseudoAsm registers *)
Record agree (ms: Mach.regset) (sp: val) (rs: regset) : Prop := mkagree {
  agree_sp: rs#SP = sp;
  agree_sp_def: sp <> Vundef;
  agree_mregs: forall r: mreg, (ms r)=(rs#r)
}.

(** [transl_code_at_pc pc fb f tf c] holds if the code pointer [pc] points
  within the code generated by Machblock function (originally [f] -- but translated as [tf]),
  and [c] is the tail of the code at the position corresponding to the code pointer [pc].
*)
Inductive transl_code_at_pc (b:block) (f:function) (tf:function) (c:code): val -> Prop :=
  transl_code_at_pc_intro ofs:
    Genv.find_funct_ptr ge b = Some (Internal f) ->
    transf_function f = OK tf ->
    (* we have passed the first block containing the prologue *)
    (0 < (Ptrofs.unsigned ofs))%Z -> 
    (* the code is identical in the two functions *)
    is_pos next tf (Ptrofs.unsigned ofs) c ->
    transl_code_at_pc b f tf c (Vptr b ofs).

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

(** Semantic preservation is proved using simulation diagrams
  of the following form.
<<
           s1 ---------------- s2
            |                   |
           t|                  *|t
            |                   |
            v                   v
           s1'---------------- s2'
>>
  The invariant is the [match_states] predicate below...

*)

Inductive match_states: Machblock.state -> state -> Prop :=
  | match_states_internal s fb sp c ms m rs f tf
        (STACKS: match_stack s)
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (AT: transl_code_at_pc fb f tf c (rs PC))
        (AG: agree ms sp rs):
      match_states (Machblock.State s fb sp c ms m)
                   (State rs m)
  | match_states_prologue s sp fb ms rs0 m0 f rs1 m1 
        (STACKS: match_stack s)
        (AG: agree ms sp rs1)
        (ATPC: rs0 PC = Vptr fb Ptrofs.zero)
        (ATLR: rs0 RA = parent_ra s)
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (PROL: exec_prologue f 0 rs0 m0 = Next rs1 m1):
      match_states (Machblock.State s fb sp (fn_code f) ms m1)
                   (State rs0 m0)
  | match_states_call s fb ms m rs
        (STACKS: match_stack s)
        (AG: agree ms (parent_sp s) rs)
        (ATPC: rs PC = Vptr fb Ptrofs.zero)
        (ATLR: rs RA = parent_ra s):
      match_states (Machblock.Callstate s fb ms m)
                   (State rs m)
  | match_states_return s ms m rs
        (STACKS: match_stack s)
        (AG: agree ms (parent_sp s) rs)
        (ATPC: rs PC = parent_ra s):
      match_states (Machblock.Returnstate s ms m)
                   (State rs m).

Definition measure (s: Machblock.state) : nat :=
  match s with
  | Machblock.State _ _ _ _ _ _ => 0%nat
  | Machblock.Callstate _ _ _ _ => 1%nat
  | Machblock.Returnstate _ _ _ => 1%nat
  end.

Definition rao (f: function) (c: code) (ofs: ptrofs) : Prop :=
  forall tf,
  transf_function f = OK tf ->
  is_pos next tf (Ptrofs.unsigned ofs) c.

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 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 functions_transl fb f tf:
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  transf_function f = OK tf ->
  Genv.find_funct_ptr tge fb = Some (Internal tf).
Proof.
  intros. exploit functions_translated; eauto. intros [tf' [A B]].
  monadInv B. inv H0; auto.
Qed.

Lemma function_bound fb f tf:
  Genv.find_funct_ptr ge fb = Some (Internal f) -> transf_function f = OK tf -> (max_pos tf) <= Ptrofs.max_unsigned.
Proof.
  intros; eapply functions_bound_max_pos; eauto.
  eapply functions_transl; eauto.
Qed.

Lemma transf_function_def f tf:
  transf_function f = OK tf -> tf.(fn_code) = insert_implicit_prologue f.(fn_code).
Proof.
  unfold transf_function.
  intros EQ; inv EQ.
  auto.
Qed.

Lemma stackinfo_preserved f tf:
  transf_function f = OK tf ->
  tf.(fn_stacksize) = f.(fn_stacksize) 
  /\ tf.(fn_retaddr_ofs) = f.(fn_retaddr_ofs)
   /\ tf.(fn_link_ofs) = f.(fn_link_ofs).
Proof.
  unfold transf_function.
  intros EQ0; inv EQ0. simpl; intuition.
Qed.

Lemma transf_initial_states st1: Machblock.initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intro H. inversion H. unfold ge0 in *.
  econstructor; split.
  - econstructor.
    eapply (Genv.init_mem_transf_partial TRANSF); eauto.
  - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero)
     with (Vptr fb Ptrofs.zero).
    + econstructor; eauto.
      * constructor.
      * split; auto; simpl; unfold Vnullptr; destruct Archi.ptr64; congruence.
    + unfold Genv.symbol_address.
      rewrite (match_program_main TRANSF).
      rewrite symbols_preserved.
      unfold ge. simplify_someHyp. auto.
Qed.

Lemma transf_final_states st1 st2 r:
  match_states st1 st2 -> Machblock.final_state st1 r -> final_state st2 r.
Proof.
  intros H H0. inv H0. inv H.
  econstructor; eauto.
  exploit agree_mregs; eauto.
  erewrite H2. intro H3; inversion H3.
  auto.
Qed.

(** Lemma on [is_pos]. *)

Lemma is_pos_alt_def f pos code: is_pos next f pos code -> 
  exists n, (n <= List.length (fn_code f))%nat /\ pos = (iter n (next f) 0) /\ code = iter_tail n (fn_code f).
Proof.
  induction 1.
  - unfold iter_tail; exists O; simpl; intuition.
  - destruct IHis_pos as (n & H0 & H1 & H2).
    exists (S n). repeat split.
    + rewrite (length_iter_tail n); eauto.
      rewrite <- H2; simpl; omega.
    + rewrite iter_S; congruence.
    + unfold iter_tail in *; rewrite iter_S, <- H2; auto.
Qed.

Local Hint Resolve First_pos Next_pos: core.

Lemma is_pos_alt_def_recip f n: (n <= List.length (fn_code f))%nat ->
  is_pos next f (iter n (next f) 0) (iter_tail n (fn_code f)).
Proof.
  induction n.
  - unfold iter_tail; simpl; eauto.
  - intros H; destruct (iter_tail_S_ex n (fn_code f)) as (x & H1); try omega.
    rewrite iter_S; lapply IHn; try omega.
    rewrite H1; eauto.
Qed.

Lemma is_pos_inject1 f pos1 pos2 code:
  is_pos next f pos1 code -> is_pos next f pos2 code -> pos1=pos2.
Proof.
  intros H1 H2.
  destruct (is_pos_alt_def f pos1 code) as (n1 & B1 & POS1 & CODE1); eauto.
  destruct (is_pos_alt_def f pos2 code) as (n2 & B2 & POS2 & CODE2); eauto.
  clear H1 H2; subst.
  erewrite (iter_tail_inject1 n1 n2); eauto.
Qed.

Lemma iter_next_strict_monotonic f n m x: (n < m)%nat -> iter n (next f) x < iter m (next f) x.
Proof.
  induction 1; rewrite iter_S; auto.
  generalize (next_progress f (iter m (next f) x)).
  omega.
Qed.

Lemma iter_next_monotonic f n m x: (n <= m)%nat -> iter n (next f) x <= iter m (next f) x.
Proof.
  destruct 1.
  - omega.
  - generalize (iter_next_strict_monotonic f n (S m) x). omega.
Qed.

Lemma is_pos_bound_pos f pos code:
  is_pos next f pos code -> 0 <= pos <= max_pos f.
Proof.
  intros H; exploit is_pos_alt_def; eauto.
  intros (n & H1 & H2 & H3).
  rewrite H2. unfold max_pos. split.
  - cutrewrite (0 = iter O (next f) 0); auto.
    apply iter_next_monotonic; omega.
  - apply iter_next_monotonic; omega.
Qed.

Lemma is_pos_unsigned_repr f pos code:
  is_pos next f pos code -> 
  max_pos f <= Ptrofs.max_unsigned ->
  Ptrofs.unsigned (Ptrofs.repr pos) = pos.
Proof.
  intros; eapply Ptrofs.unsigned_repr.
  exploit is_pos_bound_pos; eauto.
  omega.
Qed.

Lemma is_pos_simplify f pos code:
  is_pos next f pos code -> 
  max_pos f <= Ptrofs.max_unsigned ->
  is_pos next f (Ptrofs.unsigned (Ptrofs.repr pos)) code.
Proof.
  intros; erewrite is_pos_unsigned_repr; eauto.
Qed.

Lemma find_label_label_pos f lbl c: forall pos c',
  find_label lbl c = Some c' ->
  exists n,
  label_pos next f lbl pos c = Some (iter n (next f) pos)
  /\ c' = iter_tail n c
  /\ (n <= List.length c)%nat.
Proof.
  induction c.
  - simpl; intros. discriminate.
  - simpl; intros pos c'.
    destruct (is_label lbl a).
    + intro EQ; injection EQ; intro; subst c'.
      exists O; simpl; intuition.
    + intros. generalize (IHc (next f pos) c' H). intros (n' & A & B & C).
       exists (S n'). intuition.
Qed.

Lemma find_label_insert_implicit_prologue lbl c:
  find_label lbl c = find_label lbl (insert_implicit_prologue c).
Proof.
  unfold insert_implicit_prologue.
  destruct (has_header c); simpl; auto.
  unfold is_label; simpl.
  destruct (in_dec lbl nil); auto.
  simpl in *. tauto.
Qed.

Lemma no_header_insert_implicit_prologue c:
  has_header (insert_implicit_prologue c) = false.
Proof.
  unfold insert_implicit_prologue.
  destruct (has_header c) eqn: H; simpl; auto.
Qed.

Lemma find_label_has_header lbl c c':
  find_label lbl c = Some c' -> 
  has_header c' = true.
Proof.
  induction c; simpl; try congruence.
  destruct (is_label lbl a) eqn:LAB; auto.
  intros X; inv X; simpl.
  unfold is_label in LAB.
  destruct (in_dec lbl (header a)); try congruence.
  destruct (header a); try congruence.
  simpl in *; tauto.
Qed.

Lemma find_label_label_pos_no_header f lbl c pos c':
  (has_header c) = false ->
  find_label lbl c = Some c' ->
  exists n,
  label_pos next f lbl pos c = Some (iter (S n) (next f) pos)
  /\ c' = iter_tail (S n) c
  /\ ((S n) <= List.length c)%nat.
Proof.
  intros H H0; exploit find_label_label_pos; eauto.
  intros ([|n] & H1 & H2 & H3); try (exists n; intuition eauto).
  unfold iter_tail in *; simpl in *; subst.
  erewrite find_label_has_header in H; eauto.
  congruence.
Qed.

Hint Resolve is_pos_simplify is_pos_alt_def_recip function_bound: core.

Lemma find_label_goto_label f tf lbl rs c' b ofs:
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  transf_function f = OK tf ->
  Vptr b ofs = rs PC ->
  find_label lbl f.(fn_code) = Some c' ->
  exists pc,
     goto_label next tf lbl rs = Some pc
  /\ transl_code_at_pc b f tf c' pc.
Proof.
  intros FINDF T HPC FINDL.
  erewrite find_label_insert_implicit_prologue, <- transf_function_def in FINDL; eauto.
  exploit find_label_label_pos_no_header; eauto.
  { erewrite transf_function_def; eauto.
    apply no_header_insert_implicit_prologue.
  }
  intros (n & LAB & CODE & BOUND); subst.
  exists (Vptr b (Ptrofs.repr (iter (S n) (next tf) 0))).
  unfold goto_label; intuition.
  - simplify_someHyps; rewrite <- HPC. auto.
  - econstructor; eauto.
    erewrite is_pos_unsigned_repr; eauto.
    generalize (iter_next_strict_monotonic tf O (S n) 0); simpl.
    omega.
Qed.

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

Lemma agree_mregs_list ms sp rs:
  agree ms sp rs ->
  forall l, (ms##l)=(to_Machrs rs)##l.
Proof.
  unfold to_Machrs. intros AG; induction l; simpl; eauto.
  erewrite agree_mregs; eauto.
  congruence.
Qed.

Lemma agree_set_mreg ms sp rs r v rs':
  agree ms sp rs ->
  v=(rs'#(preg_of r)) ->
  (forall r', r' <> preg_of r -> rs'#r' = rs#r') ->
  agree (Regmap.set r v ms) sp rs'.
Proof.
  intros H H0 H1. destruct H. split; auto.
  - rewrite H1; auto. destruct r; simpl; congruence.
  - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence.
    rewrite H1; auto. destruct r; simpl; congruence.
Qed.

Corollary agree_set_mreg_parallel:
  forall ms sp rs r v,
  agree ms sp rs ->
  agree (Regmap.set r v ms) sp (Pregmap.set (preg_of r) v rs).
Proof.
  intros. eapply agree_set_mreg; eauto. 
  - rewrite Pregmap.gss; auto. 
  - intros; apply Pregmap.gso; auto.
Qed.

Corollary agree_set_mreg_parallel2:
  forall ms sp rs r v ms',
  agree ms sp (set_from_Machrs ms' rs)->
  agree (Regmap.set r v ms) sp (set_from_Machrs (Regmap.set r v ms') rs).
Proof.
  intros. unfold set_from_Machrs in *. eapply agree_set_mreg; eauto.
  - rewrite Regmap.gss; auto. 
  - intros r' X. destruct r'; try congruence. rewrite Regmap.gso; try congruence.
Qed.

Definition data_preg (r: preg) : bool :=
  match r with
  | preg_of _ | SP => true
  | _ => false
  end.

Lemma agree_exten ms sp rs rs':
  agree ms sp rs ->
  (forall r, data_preg r = true -> rs'#r = rs#r) ->
  agree ms sp rs'.
Proof.
  intros H H0. destruct H. split; intros; try rewrite H0; auto.
Qed.

Lemma agree_set_from_Machrs ms sp ms' rs:
  agree ms sp rs ->
  (forall (r:mreg), (ms' r) = rs#r) ->
  agree ms sp (set_from_Machrs ms' rs).
Proof.
  unfold set_from_Machrs; intros.
  eapply agree_exten; eauto.
  intros r; destruct r; simpl; try congruence.
Qed.

Lemma agree_set_other ms sp rs r v:
  agree ms sp rs ->
  data_preg r = false ->
  agree ms sp (rs#r <- v).
Proof.
  intros; apply agree_exten with rs; auto.
  intros. apply Pregmap.gso. congruence.
Qed.


Lemma agree_next_addr f ms sp b pos rs:
  agree ms sp rs ->
  agree ms sp (rs#PC <- (Vptr b (Ptrofs.repr (next f pos)))).
Proof.
  intros. apply agree_set_other; auto.
Qed.

Local Hint Resolve agree_set_mreg_parallel2: core.

Lemma agree_set_pair sp p v ms ms' rs:
  agree ms sp (set_from_Machrs ms' rs) ->
  agree (set_pair p v ms) sp (set_from_Machrs (set_pair p v ms') rs).
Proof.
  intros H; destruct p; simpl; auto.
Qed.

Lemma agree_undef_caller_save_regs:
  forall ms sp ms' rs,
  agree ms sp (set_from_Machrs ms' rs) ->
  agree (undef_caller_save_regs ms) sp (set_from_Machrs (undef_caller_save_regs ms') rs).
Proof.
  intros. destruct H as [H0 H1 H2]. unfold undef_caller_save_regs. split; auto.
  intros.
  unfold set_from_Machrs in * |- *.
  rewrite H2. auto.
Qed.

Lemma agree_change_sp ms sp rs sp':
  agree ms sp rs -> sp' <> Vundef ->
  agree ms sp' (rs#SP <- sp').
Proof.
  intros H H0. inv H. split; auto.
Qed.

Lemma agree_undef_regs ms sp rl ms' rs:
  agree ms sp (set_from_Machrs ms' rs) ->
  agree (Mach.undef_regs rl ms) sp (set_from_Machrs (Mach.undef_regs rl ms') rs).
Proof.
  unfold set_from_Machrs; intros H. destruct H; subst. split; auto.
  intros. destruct (In_dec mreg_eq r rl).
  + rewrite! undef_regs_same; auto.
  + rewrite! undef_regs_other; auto.
Qed.

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

Remark builtin_arg_match:
  forall ms rs sp m a v,
  agree ms sp rs ->
  eval_builtin_arg ge ms sp m a v ->
  eval_builtin_arg ge (to_Machrs rs) sp m a v.
Proof.
  induction 2; simpl; eauto with barg.
  unfold to_Machrs; erewrite agree_mregs; eauto.
  econstructor.
Qed.

Lemma builtin_args_match: 
  forall ms sp rs m,
  agree ms sp rs ->
  forall al vl, eval_builtin_args ge ms sp m al vl ->
  eval_builtin_args ge (to_Machrs rs) sp m al vl.
Proof.
  induction 2; intros; simpl; try (constructor; auto).
  eapply eval_builtin_arg_preserved; eauto.
  eapply builtin_arg_match; eauto.
Qed.

Lemma agree_set_res res: forall ms sp rs v ms',
  agree ms sp (set_from_Machrs ms' rs) ->
  agree (set_res res v ms) sp (set_from_Machrs (set_res res v ms') rs).
Proof.
  induction res; simpl; auto.
Qed.

Lemma find_function_ptr_agree ros ms rs sp b: 
  agree ms sp rs ->
  Machblock.find_function_ptr ge ros ms = Some b ->
  find_function_ptr tge ros rs = Some (Vptr b Ptrofs.zero).
Proof.
  intros AG; unfold Mach.find_function_ptr; destruct ros as [r|s]; simpl; auto.
  - generalize (agree_mregs _ _ _ AG r). destruct (ms r); simpl; try congruence.
    intros H; inv H; try congruence.
    inversion_ASSERT. intros H; rewrite (Ptrofs.same_if_eq _ _ H); eauto.
    try_simplify_someHyps.
  - intros H; rewrite symbols_preserved, H. auto.
Qed.

Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef.
Proof.
  induction 1; simpl.
  unfold Vnullptr; destruct Archi.ptr64; congruence.
  auto.
Qed.

Lemma extcall_arg_match ms sp rs m l v:
  agree ms sp rs ->
  extcall_arg ms m sp l v ->
  extcall_arg rs m (rs#SP) l v.
Proof.
  destruct 2.
  - erewrite agree_mregs; eauto. constructor.
  - unfold load_stack in *. econstructor; eauto.
    erewrite agree_sp; eauto.
Qed.

Local Hint Resolve extcall_arg_match: core.

Lemma extcall_arg_pair_match:
  forall ms sp rs m p v,
  agree ms sp rs ->
  extcall_arg_pair ms m sp p v ->
  extcall_arg_pair rs m (rs#SP) p v.
Proof.
  destruct 2; constructor; eauto.
Qed.

Local Hint Resolve extcall_arg_pair_match: core.

Lemma extcall_args_match:
  forall ms sp rs m, agree ms sp rs ->
  forall ll vl,
  list_forall2 (extcall_arg_pair ms m sp) ll vl ->
  list_forall2 (extcall_arg_pair rs m rs#SP) ll vl.
Proof.
  induction 2; constructor; eauto.
Qed.

Lemma extcall_arguments_match:
  forall ms m sp rs sg args,
  agree ms sp rs ->
  extcall_arguments ms m sp sg args ->
  extcall_arguments rs m (rs#SP) sg args.
Proof.
  unfold extcall_arguments, extcall_arguments; intros.
  eapply extcall_args_match; eauto.
Qed.

(** A few tactics *)

Local Hint Resolve functions_transl symbols_preserved
  agree_next_addr agree_mregs agree_set_mreg_parallel agree_undef_regs agree_set_other agree_change_sp
  agree_sp_def agree_set_from_Machrs agree_set_pair agree_undef_caller_save_regs agree_set_res f_equal Ptrofs.repr_unsigned parent_sp_def
  builtin_args_match external_call_symbols_preserved: core.

Ltac simplify_regmap :=
  repeat (rewrite ?Pregmap.gss; try (rewrite Pregmap.gso; try congruence)).

Ltac simplify_next_addr :=
  match goal with
  | [ HPC: Vptr _ _ = _ PC |- _ ] => try (unfold next_addr, Val.offset_ptr); simplify_regmap; try (rewrite <- HPC)
  end.

Ltac discharge_match_states :=
   econstructor; eauto; try ( simplify_next_addr; econstructor; eauto ).


(** Instruction step simulation lemma: the simulation lemma for stepping one instruction 

<<
           s1 ---------------- s2
            |                   |
           t|                  +|t
            |                   |
            v                   v
           s1'---------------- s2'
>>

*)

Lemma trivial_exec_prologue:
  forall tf ofs rs m,
  0 < Ptrofs.unsigned ofs ->
  exec_prologue tf (Ptrofs.unsigned ofs) rs m = Next rs m.
Proof.
  unfold exec_prologue. intros.
  destruct (Z.eq_dec); eauto. omega.
Qed.

Lemma basic_step_simulation: forall ms sp rs s f tf fb ms' bi m m',
  agree ms sp rs ->
  match_stack s ->
  transf_function f = OK tf ->
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  Machblock.basic_step ge s fb sp ms m bi ms' m' ->
  exists rs', basic_step tge tf rs m bi rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC.
Proof.
  destruct 5.
  (* MBgetstack *)
  - eexists; split.
    + econstructor; eauto. erewrite agree_sp; eauto.
    + eauto.
  (* MBsetstack *)
  - eexists; split.
    + econstructor; eauto.
      erewrite agree_sp; eauto.
      erewrite <- agree_mregs; eauto.
    + rewrite H4; split; eauto.
  (* MBgetparam *)
  - eexists; split.
    + econstructor; eauto.
      erewrite agree_sp; eauto.
      assert (f = f0). { rewrite H2 in H3. inversion H3. reflexivity. }
      assert (fn_link_ofs tf = fn_link_ofs f0). {
        rewrite <- H7.
        eapply stackinfo_preserved. eauto.
      }
      rewrite H8. eauto.
    + rewrite H6; split; eauto.
  (* MBop *)
  - eexists; split.
    + econstructor; eauto.
      erewrite agree_sp; eauto.
      erewrite agree_mregs_list in H3.
      * erewrite <- H3.
        eapply eval_operation_preserved; trivial.
      * eauto.
    + rewrite H4; split; eauto.
  (* MBload *)
  - eexists; split.
    + econstructor; eauto.
      erewrite agree_sp; eauto. erewrite <- agree_mregs_list; eauto.
      erewrite <- H3.
      eapply eval_addressing_preserved; trivial.
    + rewrite H5; split; eauto.
  (* MBload notrap1 *)
  - eexists; split.
    + eapply exec_MBload_notrap1; eauto.
      erewrite agree_sp; eauto.
      erewrite agree_mregs_list in H3; eauto.
      * erewrite eval_addressing_preserved; eauto.
    + rewrite H4; eauto.
  (* MBload notrap2 *)
  - eexists; split.
    + eapply exec_MBload_notrap2; eauto.
      erewrite agree_sp; eauto.
      erewrite agree_mregs_list in H3; eauto.
      * erewrite eval_addressing_preserved; eauto.
    + rewrite H5; eauto.
  (* MBstore *)
  - eexists; split.
    + econstructor; eauto.
      * erewrite agree_sp; eauto.
        erewrite agree_mregs_list in H3.
        erewrite eval_addressing_preserved; eauto.
        eauto.
      * erewrite <- agree_mregs; eauto.
    + rewrite H5; eauto.
Qed.

Lemma body_step_simulation: forall ms sp s f tf fb ms' bb m m',
  match_stack s ->
  transf_function f = OK tf ->
  Genv.find_funct_ptr ge fb = Some (Internal f) ->
  Machblock.body_step ge s fb sp bb ms m ms' m' ->
  forall rs, agree ms sp rs ->
  exists rs', body_step tge tf bb rs m rs' m' /\ agree ms' sp rs' /\ rs' PC = rs PC.
Proof.
  induction 4.
  - repeat (econstructor; eauto).
  - intros. exploit basic_step_simulation; eauto.
    intros (rs'0 & BASIC & AG1' & AGPC1).
    exploit IHbody_step; eauto.
    intros (rs'1 & BODY & AG2' & AGPC2).
    repeat (econstructor; eauto).
    congruence.
Qed.

Local Hint Resolve trivial_exec_prologue: core.

Lemma exit_step_simulation s fb f sp c t bb ms m s1' tf rs pc
  (STEP: Machblock.exit_step rao ge (exit bb) (Machblock.State s fb sp (bb :: c) ms m) t s1')
  (STACKS: match_stack s)
  (AG: agree ms sp rs)
  (NXT: next_addr next tf rs = Some pc)
  (AT: transl_code_at_pc fb f tf c pc):
  exists rs' m', exit_step next tge tf (exit bb) (rs#PC <- pc) m t rs' m' /\ match_states s1' (State rs' m').
Proof.
  inv AT.
  inv STEP.
  (* cfi_step currently only defined for exec_MBcall, exec_MBreturn, and exec_MBgoto *)
  - inversion H4; subst. clear H4. (* inversion_clear H4 does not work so well: it clears an important hypothesis about "sp" in the Mreturn case *)
    (* MBcall *)
    + eexists. eexists. split.
      * apply exec_Some_exit.
        apply exec_MBcall.
        eapply find_function_ptr_agree; eauto.
      * assert (f0 = f). { congruence. } subst.
        assert (Ptrofs.unsigned ra = Ptrofs.unsigned ofs). {
          eapply is_pos_inject1; eauto.
        }
        assert (ofs = ra). {
          apply Ptrofs.same_if_eq. unfold Ptrofs.eq.
          rewrite H4. rewrite zeq_true. reflexivity.
        }
        repeat econstructor; eauto.
        -- unfold rao in *. congruence.
        -- simpl. simplify_regmap.
           erewrite agree_sp; eauto.
        -- simpl. simplify_regmap. auto.
    (* MBtailcall *)
    + assert (f0 = f). { congruence. } subst.
      eexists. eexists. split.
      * repeat econstructor.
        -- eapply find_function_ptr_agree; eauto.
        -- unfold exec_epilogue. erewrite agree_sp; eauto.
           apply stackinfo_preserved in H0 as ( SS & RA & LO ).
           rewrite SS, RA, LO.
           try_simplify_someHyps.
      * repeat econstructor; eauto.
        intros r.
        eapply agree_mregs; eapply agree_set_other; eauto.
    (* MBbuiltin *)
    +eexists. eexists. split.
      * repeat econstructor.
        -- simplify_regmap. erewrite agree_sp; eauto.
           eapply eval_builtin_args_preserved; eauto.
        -- eapply external_call_symbols_preserved; eauto.
           exact senv_preserved.
      * repeat econstructor; eauto.
        -- assert (transl_function f = tf). {
             unfold transf_function in *. congruence.
           }
           erewrite H5. assumption.
        -- eapply agree_sp. eapply agree_set_res. eapply agree_undef_regs.
           eapply agree_set_from_Machrs; eauto.
        -- intros; simpl.
           eapply agree_set_res. eapply agree_undef_regs.
           eapply agree_set_from_Machrs; eauto.
    (* MBgoto *)
    + simplify_someHyps. intros.
      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
        rewrite Pregmap.gss. reflexivity.
      }
      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
        eapply find_label_goto_label; eauto.
      }
      eexists. eexists. split.
      * apply exec_Some_exit.
        apply exec_MBgoto.
        rewrite GOTO_LABEL. trivial.
      * repeat econstructor; eauto.
        -- simplify_regmap.
           exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
           assert(pc' = pc). { congruence. } subst. eauto.
        -- simplify_regmap. erewrite agree_sp; eauto.
    (* MBcond true *)
    (* Mostly copy and paste from MBgoto *)
    + simplify_someHyps. intros.
      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
        rewrite Pregmap.gss. reflexivity.
      }
      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
        eapply find_label_goto_label; eauto.
      }
      eexists. eexists. split.
      * apply exec_Some_exit. eapply exec_MBcond_true; eauto.
        erewrite agree_mregs_list in H14; eauto.
      * repeat econstructor; eauto.
        -- simplify_regmap.
           exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
           assert(pc' = pc). { congruence. } subst. eauto.
        -- simplify_regmap. erewrite agree_sp; eauto.
    (* MBcond false *)
    + inv H0. eexists. eexists. split. 
      * apply exec_Some_exit. apply exec_MBcond_false.
        -- erewrite agree_mregs_list in H15; eauto.
        -- trivial.
      * repeat econstructor; eauto. erewrite agree_sp; eauto.
    (* MBjumptable *)
    + simplify_someHyps. intros.
      assert ((rs # PC <- (Vptr fb ofs)) PC = Vptr fb ofs). {
        rewrite Pregmap.gss. reflexivity.
      }
      eassert (exists pc, goto_label next tf lbl rs # PC <- (Vptr fb ofs) = Some pc
               /\ transl_code_at_pc fb f tf c' pc) as (pc & GOTO_LABEL & _). {
        eapply find_label_goto_label; eauto.
      }
      eexists. eexists. split.
      * repeat econstructor; eauto.
        rewrite <- H14.
        symmetry. eapply agree_mregs. eapply agree_set_other; eauto.
      * repeat econstructor; eauto.
        (* copy paste from MBgoto *)
        --  simplify_regmap.
            exploit find_label_goto_label; eauto. intros (pc' & GOTO_LABEL' & TRANSL).
            assert(pc' = pc). { congruence. } subst. eauto.
        -- simplify_regmap. erewrite agree_sp; eauto.
        -- intros; simplify_regmap. eauto.
    + (* MBreturn *)
      try_simplify_someHyps.
      eexists. eexists. split.
      * apply exec_Some_exit.
        apply exec_MBreturn.
        unfold exec_epilogue.
        erewrite agree_sp; eauto.
        apply stackinfo_preserved in H0 as ( SS & RA & LO ).
        rewrite SS, RA, LO.
        try_simplify_someHyps.
      * repeat econstructor; eauto. intros r.
        simplify_regmap. eapply agree_mregs; eauto.
  - inv H0; repeat econstructor; eauto.
    erewrite agree_sp; eauto.
Qed.

Lemma inst_step_simulation s fb f sp c t ms m s1' tf rs
  (STEP: Machblock.step rao ge (Machblock.State s fb sp c ms m) t s1')
  (STACKS: match_stack s)
  (AT: transl_code_at_pc fb f tf c (rs PC))
  (AG: agree ms sp rs):
  exists s2' : state, plus (step next) tge (State rs m) t s2' /\ match_states s1' s2'.
Proof.
  inv STEP.
  inv AT.
  exploit body_step_simulation; eauto. intros (rs0' & BODY & AG0 & AGPC).
  assert (NXT: next_addr next tf rs0' = Some (Vptr fb (Ptrofs.repr (next tf (Ptrofs.unsigned ofs))))).
  { unfold next_addr; rewrite AGPC, <- H; simpl; eauto. }
  exploit exit_step_simulation; eauto.
  { econstructor; eauto.
    erewrite is_pos_unsigned_repr; eauto.
    generalize (next_progress tf (Ptrofs.unsigned ofs)); omega. }
  intros (rs2 & m2 & STEP & MS).
  eexists.
  split; eauto.
  eapply plus_one.
  eapply exec_step_internal; eauto.
  econstructor; eauto.
Qed.

Lemma prologue_preserves_pc: forall f rs0 m0 rs1 m1,
  exec_prologue f 0 rs0 m0 = Next rs1 m1 ->
  rs1 PC = rs0 PC.
Proof.
  unfold exec_prologue; simpl;
  intros f rs0 m0 rs1 m1 H.
  destruct (Mem.alloc m0 0 (fn_stacksize f)) in H; unfold Next in H.
  simplify_someHyps; inversion_SOME ignored; inversion_SOME ignored';
  intros ? ? H'; inversion H'; trivial.
Qed.

Lemma is_pos_next_zero bb c fb f
  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
  (FN_HEAD : bb :: c = fn_code f):
  is_pos next (transl_function f) (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)) (if has_header (fn_code f) then bb::c else c).
Proof.
  exploit (transf_function_def f). unfold transf_function; auto.
  unfold insert_implicit_prologue.
  intros fn_code_tf; destruct (has_header (fn_code f));
  eapply Next_pos; rewrite Ptrofs.unsigned_zero;
  rewrite FN_HEAD; rewrite <- fn_code_tf; apply First_pos.
Qed.

Lemma prologue_simulation_no_header_step t s1' s sp fb ms f m1 rs0 m0 rs1
  (STACKS : match_stack s)
  (AG : agree ms sp rs1)
  (ATPC : rs0 PC = Vptr fb Ptrofs.zero)
  (ATLR : rs0 RA = parent_ra s)
  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
  (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1)
  (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1')
  (NO_HEADER: has_header (fn_code f) = false):
  exists s2' : state, step next tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'.
Proof.
  inv STEP.

  exploit functions_translated; eauto;
  intros (tf & FINDtf & TRANSf); monadInv TRANSf.
  assert (fn_code f = fn_code (transl_function f)) as TF_CODE. {
    unfold transl_function; simpl; unfold insert_implicit_prologue;
    rewrite NO_HEADER; trivial.
  }

  exploit body_step_simulation; eauto; unfold transf_function; auto.
  intros (rs0' & BODY & AG0 & AGPC).

  exploit prologue_preserves_pc; eauto.
  intros AGPC'.

  exploit is_pos_next_zero; eauto; rewrite NO_HEADER.
  intros IS_POS.

  exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. {
    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
  } intros TRANSL_CODE.

  assert (next_addr next (transl_function f) rs0' =
          Some (Vptr fb (Ptrofs.repr (next (transl_function f)
                        (Ptrofs.unsigned Ptrofs.zero))))) as NEXT_ADDR. {
    unfold next_addr; rewrite AGPC; rewrite AGPC'; rewrite ATPC; reflexivity.
  }

  exploit exit_step_simulation; eauto.
  intros (? & ? & EXIT_STEP & MATCH_EXIT).

  exploit exec_bblock_all; eauto.
  intros EXEC_BBLOCK.

  exploit exec_step_internal; eauto.
  apply is_pos_simplify; eauto. rewrite H3; rewrite TF_CODE; apply First_pos.
Qed.

Lemma prologue_simulation_header_step t s1' s sp fb ms f m1 rs0 m0 rs1
  (STACKS : match_stack s)
  (AG : agree ms sp rs1)
  (ATPC : rs0 PC = Vptr fb Ptrofs.zero)
  (ATLR : rs0 RA = parent_ra s)
  (FIND : Genv.find_funct_ptr ge fb = Some (Internal f))
  (PROL : exec_prologue f 0 rs0 m0 = Next rs1 m1)
  (STEP : Machblock.step rao ge (Machblock.State s fb sp (fn_code f) ms m1) t s1')
  (HEADER: has_header (fn_code f) = true):
  exists s2' : state, plus (step next) tge {| _rs := rs0; _m := m0 |} t s2' /\ match_states s1' s2'.
Proof.
  inv STEP.

  (* FIRST STEP *)
  exploit functions_translated; eauto;
  intros (tf & FINDtf & TRANSf); monadInv TRANSf.
  exploit transf_function_def; eauto; unfold transf_function; auto;
  unfold insert_implicit_prologue; rewrite HEADER; intros TF_CODE.

  exploit is_pos_next_zero; eauto; rewrite HEADER; rewrite H3;
  intros IS_POS.

  exploit prologue_preserves_pc; eauto.
  intros AGPC'.

  assert ( next_addr next (transl_function f) rs1
         = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero))))
         ) as NEXT_ADDR0. { unfold next_addr; rewrite AGPC'; rewrite ATPC; trivial. }

  exploit exec_nil_body; intros BODY0.
  assert ((body {| header := nil; body := nil; exit := None |}) = nil) as NIL; auto.
  rewrite <- NIL in BODY0.

  exploit exec_None_exit; intros EXIT0.
  assert ((exit {| header := nil; body := nil; exit := None |}) = None) as NONE; auto.
  rewrite <- NONE in EXIT0.

  exploit exec_bblock_all; eauto;
  intros BBLOCK0.

  exploit exec_step_internal; eauto. rewrite <- TF_CODE; apply First_pos.
  intros STEP0.

  clear BODY0 BBLOCK0 EXIT0.

  (* SECOND step *)

  exploit (mkagree ms sp
            (rs1 # PC <- (Vptr fb (Ptrofs.repr (next (transl_function f)
                         (Ptrofs.unsigned Ptrofs.zero)))))); eauto.
  apply (agree_sp ms); apply agree_set_other; eauto.
  intros AG'.

  exploit body_step_simulation; eauto; unfold transf_function; auto.
  intros (rs1' & BODY1 & AGRS1' & AGPC).

  assert ( next_addr next (transl_function f) rs1'
         = Some (Vptr fb (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned
           (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))))))
         ) as NEXT_ADDR1. { unfold next_addr; rewrite AGPC; reflexivity. }

  assert (IS_POS' := IS_POS).
  rewrite <- H3 in IS_POS'; apply Next_pos in IS_POS'.
  exploit transl_code_at_pc_intro; eauto; unfold transf_function; auto. {
    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
    assert (0 < next (transl_function f) 0) as Z0. { apply next_progress. }
    assert ( next (transl_function f) 0
           < next (transl_function f) (next (transl_function f) 0)
           ) as Z1. { apply next_progress. }
    rewrite <- Z1. exact Z0.
  } intros TRANSL_CODE1.

  exploit exit_step_simulation; eauto.
  rewrite Ptrofs.unsigned_repr.
  2: {
    assert(max_pos (transl_function f) <= Ptrofs.max_unsigned) as MAX_POS. {
      eapply functions_bound_max_pos; eauto.
    }
    rewrite <- MAX_POS.
    eapply is_pos_bound_pos; eauto.
  }
  exact TRANSL_CODE1.
  intros (? & ? & EXIT_STEP & MATCH_EXIT).

  exploit (trivial_exec_prologue (transl_function f) (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))). {
    rewrite Ptrofs.unsigned_zero; erewrite is_pos_unsigned_repr; eauto.
  } intros NO_PROL.

  exploit exec_bblock_all; eauto; intros BBLOCK1.

  clear AGPC.
  rewrite <- H3 in IS_POS.
  exploit (exec_step_internal next tge fb
                              (Ptrofs.repr (next (transl_function f) (Ptrofs.unsigned Ptrofs.zero)))
                              (transl_function f)
                              bb c); simplify_regmap; eauto.

  intros STEP1.

  eexists; split.
  + eapply plus_two.
    * exact STEP0.
    * exact STEP1.
    * trivial.
  + assumption.
Qed.

Lemma step_simulation s1 t s1':
  Machblock.step rao ge s1 t s1' ->
  forall s2, match_states s1 s2 ->
  (exists s2', plus (step next) tge s2 t s2' /\ match_states s1' s2') \/ ((measure s1' < measure s1)%nat /\ t = E0 /\ match_states s1' s2).
Proof.
  intros STEP s2 MATCH; destruct MATCH.
  - exploit inst_step_simulation; eauto.
  - left.
    destruct (has_header (fn_code f)) eqn:NO_HEADER.
    + eapply prologue_simulation_header_step; eauto.
    + exploit prologue_simulation_no_header_step; eauto;
      intros (s2' & NO_HEADER_STEP & MATCH_STATES).
      eexists; split; eauto.
      apply plus_one; eauto.
  - inv STEP; simpl; exploit functions_translated; eauto;
    intros (tf0 & FINDtf & TRANSf);
    monadInv TRANSf.
    * (* internal calls *)
      right.
      intuition.
      econstructor; eauto.
      -- exploit
           (mkagree (undef_regs destroyed_at_function_entry ms)
                    sp
                    (set_from_Machrs (undef_regs destroyed_at_function_entry rs) rs) # SP <- sp
           ); eauto.
      ++ unfold sp; discriminate.
      ++ intros mr; unfold undef_regs;
         induction destroyed_at_function_entry as [ | ? ? IH].
         ** inversion AG as [_ _ AG_MREGS]; apply AG_MREGS.
         ** fold undef_regs in *;
            unfold Regmap.set; simpl; rewrite IH; reflexivity.
      -- unfold exec_prologue;
         inversion AG as (RS_SP & ?); rewrite RS_SP; fold sp;
         rewrite H4; fold sp; rewrite H7; rewrite ATLR; rewrite H8; eauto.
    * (* external calls *)
      left.
      exploit extcall_arguments_match; eauto.
      eexists; split.
      + eapply plus_one.
        eapply exec_step_external; eauto.
        eapply external_call_symbols_preserved; eauto. apply senv_preserved.
      + econstructor; eauto.
  - (* Returnstate *)
   inv STEP; simpl; right.
   inv STACKS; simpl in *; subst.
   repeat (econstructor; eauto).
Qed.

(** * The main simulation theorem *)

Theorem transf_program_correct:
  forward_simulation (Machblock.semantics rao prog) (semantics next tprog).
Proof.
  eapply forward_simulation_star with (measure := measure).
  apply senv_preserved.
  - eexact transf_initial_states.
  - eexact transf_final_states.
  - eexact step_simulation.
Qed.

End PRESERVATION.