path: root/aarch64/Asmblockgenproof.v

(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock IterList.
Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
Require Import Lia.

Module MB := Machblock.
Module AB := Asmblock.

Definition match_prog (p: MB.program) (tp: AB.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.

Section PRESERVATION.

Variable lk: aarch64_linker.
Variable prog: Machblock.program.
Variable tprog: Asmblock.program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_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:
  forall 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. rewrite H0 in EQ; inv EQ; auto.
Qed.

Lemma transf_function_no_overflow:
  forall f tf,
  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
Proof.
  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
  lia.
Qed.

Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
  Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.

(** * Proof of semantic preservation *)

(** Semantic preservation is proved using a complex simulation diagram
  of the following form.
<<
                                     MB.step
                      ---------------------------------------->
                      header      body          exit
                  st1 -----> st2 -----> st3 ------------------> st4
                   |          |          |                       |
                   |   (A)    |   (B)    |         (C)           |
   match_codestate |          |          |                       |
                   |  header  |   body1  |  body2                |  match_states
                  cs1 -----> cs2 -----> cs3 ------> cs4          |
                   |                  /                \  exit   |
   match_asmstate  |   ---------------                  --->---  |
                   |  /   match_asmstate                       \ |
                  st'1 ---------------------------------------> st'2
                                     AB.step                  *
>>
  The invariant between each MB.step/AB.step is the [match_states] predicate below.
  However, we also need to introduce an intermediary state [Codestate] which allows
  us to reason on a finer grain, executing header, body and exit separately.

  This [Codestate] consists in a state like [Asmblock.State], except that the
  code is directly stored in the state, much like [Machblock.State]. It also features
  additional useful elements to keep track of while executing a bblock.
*)

Inductive match_states: Machblock.state -> Asm.state -> Prop :=
  | match_states_intro:
      forall s fb sp c ep ms m m' rs f tf tc
        (STACKS: match_stack ge s)
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (MEXT: Mem.extends m m')
        (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
        (AG: agree ms sp rs)
        (DXP: ep = true -> rs#X29 = parent_sp s),
      match_states (Machblock.State s fb sp c ms m)
                   (Asm.State rs m')
  | match_states_call:
      forall s fb ms m m' rs
        (STACKS: match_stack ge s)
        (MEXT: Mem.extends m m')
        (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)
                   (Asm.State rs m')
  | match_states_return:
      forall s ms m m' rs
        (STACKS: match_stack ge s)
        (MEXT: Mem.extends m m')
        (AG: agree ms (parent_sp s) rs)
        (ATPC: rs PC = parent_ra s),
      match_states (Machblock.Returnstate s ms m)
                   (Asm.State rs m').

Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *)

Lemma cons_bblocks_label:
  forall hd bdy ex tbb tc,
  cons_bblocks hd bdy ex = tbb::tc ->
  header tbb = hd.
Proof.
  intros until tc. intros CONSB. unfold cons_bblocks in CONSB.
  destruct ex; try destruct bdy; try destruct c; try destruct i.
  all: inv CONSB; simpl; auto.
Qed.

Lemma cons_bblocks_label2:
  forall hd bdy ex tbb1 tbb2,
  cons_bblocks hd bdy ex = tbb1::tbb2::nil ->
  header tbb2 = nil.
Proof.
  intros until tbb2. intros CONSB. unfold cons_bblocks in CONSB.
  destruct ex; try destruct bdy; try destruct c; try destruct i.
  all: inv CONSB; simpl; auto.
Qed.

Remark in_dec_transl:
  forall lbl hd,
  (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false).
Proof.
  intros. destruct (in_dec lbl hd), (MB.in_dec lbl hd). all: tauto.
Qed.

Lemma transl_is_label:
  forall lbl bb tbb f ep tc,
  transl_block f bb ep = OK (tbb::tc) ->
  is_label lbl tbb = MB.is_label lbl bb.
Proof.
  intros until tc. intros TLB.
  destruct tbb as [thd tbdy tex]; simpl in *.
  monadInv TLB.
  unfold is_label. simpl.
  apply cons_bblocks_label in H0. simpl in H0. subst.
  rewrite in_dec_transl. auto.
Qed.

Lemma transl_is_label_false2:
  forall lbl bb f ep tbb1 tbb2,
  transl_block f bb ep = OK (tbb1::tbb2::nil) ->
  is_label lbl tbb2 = false.
Proof.
  intros until tbb2. intros TLB.
  destruct tbb2 as [thd tbdy tex]; simpl in *.
  monadInv TLB. apply cons_bblocks_label2 in H0. simpl in H0. subst.
  apply is_label_correct_false. simpl. auto.
Qed.

Lemma transl_block_nonil:
  forall f c ep tc,
  transl_block f c ep = OK tc ->
  tc <> nil.
Proof.
  intros. monadInv H. unfold cons_bblocks.
  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
  all: discriminate.
Qed.

Lemma transl_block_limit: forall f bb ep tbb1 tbb2 tbb3 tc,
  ~transl_block f bb ep = OK (tbb1 :: tbb2 :: tbb3 :: tc).
Proof.
  intros. intro. monadInv H.
  unfold cons_bblocks in H0.
  destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i.
  all: discriminate.
Qed.

Lemma find_label_transl_false:
  forall x f lbl bb ep x',
  transl_block f bb ep = OK x ->
  MB.is_label lbl bb = false ->
  find_label lbl (x++x') = find_label lbl x'.
Proof.
  intros until x'. intros TLB MBis; simpl; auto.
  destruct x as [|x0 x1]; simpl; auto.
  destruct x1 as [|x1 x2]; simpl; auto.
  - erewrite <- transl_is_label in MBis; eauto. rewrite MBis. auto.
  - destruct x2 as [|x2 x3]; simpl; auto.
    + erewrite <- transl_is_label in MBis; eauto. rewrite MBis.
      erewrite transl_is_label_false2; eauto.
    + apply transl_block_limit in TLB. destruct TLB.
Qed.

Lemma transl_blocks_label:
  forall lbl f c tc ep,
  transl_blocks f c ep = OK tc ->
  match MB.find_label lbl c with
  | None => find_label lbl tc = None
  | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_blocks f c' false = OK tc'
  end.
Proof.
  induction c; simpl; intros.
  inv H. auto.
  monadInv H.
  destruct (MB.is_label lbl a) eqn:MBis.
  - destruct x as [|tbb tc]. { apply transl_block_nonil in EQ. contradiction. }
    simpl find_label. exploit transl_is_label; eauto. intros ABis. rewrite MBis in ABis.
    rewrite ABis.
    eexists. eexists. split; eauto. simpl transl_blocks.
    assert (MB.header a <> nil).
    { apply MB.is_label_correct_true in MBis.
      destruct (MB.header a). contradiction. discriminate. }
    destruct (MB.header a); try contradiction.
    rewrite EQ. simpl. rewrite EQ1. simpl. auto.
  - apply IHc in EQ1. destruct (MB.find_label lbl c).
    + destruct EQ1 as (tc' & FIND & TLBS). exists tc'; eexists; auto.
      erewrite find_label_transl_false; eauto.
    + erewrite find_label_transl_false; eauto.
Qed.

Lemma find_label_nil:
  forall bb lbl c,
  header bb = nil ->
  find_label lbl (bb::c) = find_label lbl c.
Proof.
  intros. destruct bb as [hd bdy ex]; simpl in *. subst.
  assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false).
  { erewrite <- is_label_correct_false. simpl. auto. }
  rewrite H. auto.
Qed.

Theorem transl_find_label:
  forall lbl f tf,
  transf_function f = OK tf ->
  match MB.find_label lbl f.(MB.fn_code) with
  | None => find_label lbl tf.(fn_blocks) = None
  | Some c => exists tc, find_label lbl tf.(fn_blocks) = Some tc /\ transl_blocks f c false = OK tc
  end.
Proof.
  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); inv EQ0. clear g.
  monadInv EQ. unfold make_prologue. simpl fn_blocks. repeat (rewrite find_label_nil); simpl; auto.
  eapply transl_blocks_label; eauto.
Qed.

End TRANSL_LABEL.

(** A valid branch in a piece of Machblock code translates to a valid ``go to''
  transition in the generated Asmblock code. *)

Lemma find_label_goto_label:
  forall f tf lbl rs m c' b ofs,
  Genv.find_funct_ptr ge b = Some (Internal f) ->
  transf_function f = OK tf ->
  rs PC = Vptr b ofs ->
  MB.find_label lbl f.(MB.fn_code) = Some c' ->
  exists tc', exists rs',
    goto_label tf lbl rs m = Next rs' m
  /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc'
  /\ forall r, r <> PC -> rs'#r = rs#r.
Proof.
  intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2.
  intros (tc & A & B).
  exploit label_pos_code_tail; eauto. instantiate (1 := 0).
  intros [pos' [P [Q R]]].
  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
  split. unfold goto_label. rewrite P. rewrite H1. auto.
  split. rewrite Pregmap.gss. constructor; auto.
  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
  auto. lia.
  generalize (transf_function_no_overflow _ _ H0). lia.
  intros. apply Pregmap.gso; auto.
Qed.

(** Existence of return addresses *)

Lemma return_address_exists:
  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
  exists ra, return_address_offset f c ra.
Proof.
  intros. eapply Asmblockgenproof0.return_address_exists; eauto.

- intros. monadInv H0.
  destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.
  exists x; exists true; split; auto.
  repeat constructor.
- exact transf_function_no_overflow.
Qed.

(* Useful for dealing with the many cases in some proofs *)
Ltac exploreInst :=
  repeat match goal with
  | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var
  | [ H : OK _ = OK _ |- _ ] => monadInv H
  | [ |- context[if ?b then _ else _] ] => destruct b
  | [ |- context[match ?m with | _ => _ end] ] => destruct m
  | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m
  | [ H : bind _ _ = OK _ |- _ ] => monadInv H
  | [ H : Error _ = OK _ |- _ ] => inversion H
  end.

(** Some translation properties *)

Lemma transl_blocks_distrib:
  forall c f bb tbb tc ep,
  transl_blocks f (bb::c) ep = OK (tbb::tc)
  -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil)
  /\ transl_blocks f c false = OK tc.
Proof.
  intros until ep. intros TLBS.
  destruct bb as [hd bdy ex].
  monadInv TLBS. monadInv EQ.
  unfold transl_block.
  rewrite EQ0; simpl.
  simpl in EQ; rewrite EQ; simpl.
  unfold cons_bblocks in *. simpl in EQ0.
  destruct ex.
  - simpl in *. monadInv EQ0.
    destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ1; auto.
  - simpl in *. inv EQ0. destruct (x3 @@ nil) eqn: CBDY; inv H0; inv EQ1; auto.
Qed.

Lemma cons_bblocks_decomp:
  forall thd tbdy tex tbb,
  (tbdy <> nil \/ tex <> None) ->
  cons_bblocks thd tbdy tex = tbb :: nil ->
     header tbb = thd
  /\ body tbb = tbdy
  /\ exit tbb = tex.
Proof.
  intros until tbb. intros Hnonil CONSB. unfold cons_bblocks in CONSB.
  destruct (tex) eqn:ECTL.
  - destruct tbdy; inv CONSB; simpl; auto.
  - inversion Hnonil.
    + destruct tbdy as [|bi tbdy]; [ contradiction H; auto | inv CONSB; auto].
    + contradict H; simpl; auto.
Qed.

Lemma transl_blocks_nonil:
  forall f bb c tc ep,
  transl_blocks f (bb::c) ep = OK tc ->
  exists tbb tc', tc = tbb :: tc'.
Proof.
  intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold cons_bblocks.
  destruct (x2);
  destruct (x3 @@ x1); simpl; eauto.
Qed.

Definition mb_remove_header bb := {| MB.header := nil; MB.body := MB.body bb; MB.exit := MB.exit bb |}.

Definition mb_remove_body (bb: MB.bblock) := 
  {| MB.header := MB.header bb; MB.body := nil; MB.exit := MB.exit bb |}.
  
Definition mbsize (bb: MB.bblock) := (length (MB.body bb) + length_opt (MB.exit bb))%nat.

Lemma mbsize_eqz:
  forall bb, mbsize bb = 0%nat -> MB.body bb = nil /\ MB.exit bb = None.
Proof.
  intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H.
  remember (length _) as a. remember (length_opt _) as b.
  assert (a = 0%nat) by lia. assert (b = 0%nat) by lia. subst. clear H.
  inv H0. inv H1. destruct bdy; destruct ex; auto.
  all: try discriminate.
Qed.

Lemma mbsize_neqz:
  forall bb, mbsize bb <> 0%nat -> (MB.body bb <> nil \/ MB.exit bb <> None).
Proof.
  intros. destruct bb as [hd bdy ex]; simpl in *.
  destruct bdy; destruct ex; try (right; discriminate); try (left; discriminate).
  contradict H. unfold mbsize. simpl. auto.
Qed.

Record codestate :=
  Codestate {     pstate: state;        (**r projection to Asmblock.state *)
                  pheader: list label;
                  pbody1: list basic;   (**r list of basic instructions coming from the translation of the Machblock body *)
                  pbody2: list basic;   (**r list of basic instructions coming from the translation of the Machblock exit *)
                  pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *)
                  ep: bool;             (**r reflects the [ep] variable used in the translation *)
                  rem: list AB.bblock;  (**r remaining bblocks to execute *)
                  cur: bblock           (**r current bblock to execute - to keep track of its size when incrementing PC *)
            }.

(* The part that deals with Machblock <-> Codestate agreement
 * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *)
Inductive match_codestate fb: Machblock.state -> codestate -> Prop :=
  | match_codestate_intro:
      forall s sp ms m rs0 m0 f tc ep c bb tbb tbc1 tbc2 ex
        (STACKS: match_stack ge s)
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (MEXT: Mem.extends m m0)
        (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc1)
        (TIC: transl_exit f (MB.exit bb) = OK (tbc2, ex))
        (TBLS: transl_blocks f c false = OK tc)
        (AG: agree ms sp rs0)
        (DXP: (if MB.header bb then ep else false) = true -> rs0#X29 = parent_sp s)
        ,
      match_codestate fb (Machblock.State s fb sp (bb::c) ms m)
        {|  pstate := (Asm.State rs0 m0);
            pheader := (MB.header bb);
            pbody1 := tbc1;
            pbody2 := tbc2;
            pctl := ex;
            ep := ep;
            rem := tc;
            cur := tbb
        |}
.

(* The part ensuring that the code in Codestate actually resides at [rs PC] *)
Inductive match_asmstate fb: codestate -> Asm.state -> Prop :=
  | match_asmstate_some:
      forall rs f tf tc m tbb ofs ep tbdy1 tbdy2 tex lhd
        (FIND: Genv.find_funct_ptr ge fb = Some (Internal f))
        (TRANSF: transf_function f = OK tf)
        (PCeq: rs PC = Vptr fb ofs)
        (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc))
        ,
      match_asmstate fb 
        {|  pstate := (Asm.State rs m);
            pheader := lhd;
            pbody1 := tbdy1;
            pbody2 := tbdy2;
            pctl := tex;
            ep := ep;
            rem := tc;
            cur := tbb |}
        (Asm.State rs m)
.

Lemma indexed_memory_access_nonil: forall f ofs r i k,
  indexed_memory_access_bc f ofs r i k <> nil.
Proof.
  intros.
  unfold indexed_memory_access_bc, loadimm64, loadimm, loadimm_z, loadimm_n;
  desif; try congruence.
  all: destruct decompose_int; try destruct p; try congruence.
Qed.

Lemma loadimm_nonil: forall sz x n k,
  loadimm sz x n k <> nil.
Proof.
  intros.
  unfold loadimm. desif;
  unfold loadimm_n, loadimm_z.
  all: destruct decompose_int; try destruct p; try congruence.
Qed.

Lemma loadimm32_nonil: forall sz x n,
  loadimm32 sz x n <> nil.
Proof.
  intros.
  unfold loadimm32. desif; try congruence.
  apply loadimm_nonil.
Qed.

Lemma loadimm64_nonil: forall sz x n,
  loadimm64 sz x n <> nil.
Proof.
  intros.
  unfold loadimm64. desif; try congruence.
  apply loadimm_nonil.
Qed.

Lemma loadsymbol_nonil: forall sz x n k,
  loadsymbol sz x n k <> nil.
Proof.
  intros.
  unfold loadsymbol. desif; try congruence.
Qed.

Lemma move_extended_nonil: forall x0 x1 x2 a k,
  move_extended x1 x2 x0 a k <> nil.
Proof.
  intros. unfold move_extended, move_extended_base.
  desif; try congruence.
Qed.

Lemma arith_extended_nonil: forall insnX insnS x0 x1 x2 x3 a k,
  arith_extended insnX insnS x1 x2 x3 x0 a k <> nil.
Proof.
  intros. unfold arith_extended, move_extended_base.
  desif; try congruence.
Qed.

Lemma transl_instr_basic_nonil:
  forall k f bi ep x,
  transl_instr_basic f bi ep k = OK x ->
  x <> nil.
Proof.
  intros until x. intros TIB.
  destruct bi.
  - simpl in TIB. unfold loadind in TIB;
    exploreInst; try discriminate; apply indexed_memory_access_nonil.
  - simpl in TIB. unfold storeind in TIB;
    exploreInst; try discriminate; apply indexed_memory_access_nonil.
  - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate;
    unfold loadptr_bc; apply indexed_memory_access_nonil.
  - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate;
    unfold addimm32, addimm64, shrx32, shrx64,
    logicalimm32, logicalimm64, addimm_aux.
    all: desif; try congruence;
    try apply loadimm32_nonil; try apply loadimm64_nonil; try apply loadsymbol_nonil;
    try apply move_extended_nonil; try apply arith_extended_nonil.
    all: unfold transl_cond in *; exploreInst; try discriminate;
      try apply loadimm32_nonil; try apply loadimm64_nonil.
  - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate;
    unfold transl_addressing in *; exploreInst; try discriminate.
    all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil.
  - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate;
    unfold transl_addressing in *; exploreInst; try discriminate.
    all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil.
Qed.

Lemma transl_basic_code_nonil:
  forall bdy f x ep,
  bdy <> nil ->
  transl_basic_code f bdy ep = OK x ->
  x <> nil.
Proof.
  induction bdy as [|bi bdy].
    intros. contradict H0; auto.
  destruct bdy as [|bi2 bdy].
  - clear IHbdy. intros f x b _ TBC. simpl in TBC. eapply transl_instr_basic_nonil; eauto.
  - intros f x b Hnonil TBC. remember (bi2 :: bdy) as bdy'.
    monadInv TBC.
    assert (x0 <> nil).
      eapply IHbdy; eauto. subst bdy'. discriminate.
    eapply transl_instr_basic_nonil; eauto.
Qed.

Lemma transl_exit_nonil:
  forall ex f bdy x,
  ex <> None ->
  transl_exit f ex = OK(bdy, x) ->
  x <> None.
Proof.
  intros ex f bdy x Hnonil TIC.
  destruct ex as [ex|].
  - clear Hnonil. destruct ex.
    all: try (simpl in TIC; try monadInv TIC; exploreInst; discriminate).
  - contradict Hnonil; auto.
Qed.

Theorem app_nonil: forall A (l1 l2: list A),
  l1 <> nil ->
  l1 @@ l2 <> nil.
Proof.
  induction l2.
  - intros; rewrite app_nil_r; auto.
  - intros. unfold not. intros. symmetry in H0. 
    generalize (app_cons_not_nil); intros. unfold not in H1.
    generalize (H0). apply H1.
Qed.

Theorem match_state_codestate:
  forall mbs abs s fb sp bb c ms m,
  (MB.body bb <> nil \/ MB.exit bb <> None) ->
  mbs = (Machblock.State s fb sp (bb::c) ms m) ->
  match_states mbs abs ->
  exists cs fb f tbb tc ep,
    match_codestate fb mbs cs /\ match_asmstate fb cs abs
    /\ Genv.find_funct_ptr ge fb = Some (Internal f)
    /\ transl_blocks f (bb::c) ep = OK (tbb::tc)
    /\ body tbb = pbody1 cs ++ pbody2 cs
    /\ exit tbb = pctl cs
    /\ cur cs = tbb /\ rem cs = tc
    /\ pstate cs = abs.
Proof.
  intros until m. intros Hnotempty Hmbs MS. subst. inv MS.
  inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst.
  exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2.
  monadInv TLB. exploit cons_bblocks_decomp; eauto.
    { inversion Hnotempty.
      - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail).
        left. apply app_nonil. eapply transl_basic_code_nonil; eauto.
      - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail).
        right. eapply transl_exit_nonil; eauto. }
  intros (Hth & Htbdy & Htexit).
  exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x;
            pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0.
  repeat split. 1-2: econstructor; eauto.
  { destruct (MB.header bb). eauto. discriminate. } eauto.
  unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl.
  rewrite TLBS. simpl. rewrite H2.
  all: simpl; auto.
Qed.

Lemma exec_straight_body:
  forall c c' rs1 m1 rs2 m2,
  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
  exists l,
     c = l ++ c'
  /\ exec_body lk tge l rs1 m1 = Next rs2 m2.
Proof.
  induction c; try (intros; inv H; fail).
  intros until m2. intros EXES. inv EXES.
  - exists (a :: nil). repeat (split; simpl; auto). rewrite H6. auto.
  - eapply IHc in H7; eauto. destruct H7 as (l' & Hc & EXECB). subst.
    exists (a :: l'). repeat (split; simpl; auto).
    rewrite H1. auto.
Qed.

Lemma exec_straight_body2:
  forall c rs1 m1 c' rs2 m2,
  exec_straight tge lk c rs1 m1 c' rs2 m2 ->
  exists body,
     exec_body lk tge body rs1 m1 = Next rs2 m2
  /\ body ++ c' = c.
Proof.
  intros until m2. induction 1.
  - exists (i1::nil). split; auto. simpl. rewrite H. auto.
  - destruct IHexec_straight as (bdy & EXEB & BTC).
    exists (i:: bdy). split; simpl.
    + rewrite H. auto.
    + congruence.
Qed.

Lemma exec_straight_opt_body2:
  forall c rs1 m1 c' rs2 m2,
  exec_straight_opt tge lk c rs1 m1 c' rs2 m2 ->
  exists body,
     exec_body lk tge body rs1 m1 = Next rs2 m2
  /\ body ++ c' = c.
Proof.
  intros until m2. intros EXES.
  inv EXES.
  - exists nil. split; auto.
  - eapply exec_straight_body2. auto.
Qed.

Lemma PC_not_data_preg: forall r ,
  data_preg r = true ->
  r <> PC.
Proof.
  intros. destruct (PregEq.eq r PC); [ rewrite e in H; simpl in H; discriminate | auto ].
Qed.

Lemma X30_not_data_preg: forall r ,
  data_preg r = true ->
  r <> X30.
Proof.
  intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ].
Qed.

Lemma X16_not_data_preg: forall r ,
  data_preg r = true ->
  r <> X16.
Proof.
  intros. destruct (PregEq.eq r X16); [ rewrite e in H; simpl in H; discriminate | auto ].
Qed.

Lemma undef_regs_other_2':
  forall r rl rs,
  data_preg r = true ->
  preg_notin r rl ->
  undef_regs (DR (IR X16) :: DR (IR X30) :: map preg_of rl) rs r = rs r.
Proof.
  intros. apply undef_regs_other. intros. simpl in H1.
  destruct H1 as [HX16 | [HX30 | HDES]]; subst.
  apply X16_not_data_preg; auto. apply X30_not_data_preg; auto.
  exploit list_in_map_inv; eauto. intros [mr [A B]]. subst.
  rewrite preg_notin_charact in H0. auto.
Qed.

Ltac Simpl :=
  rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg.
  
(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are
   unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by
   yourself the steps *)
Theorem step_simu_control:
  forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2,
  MB.body bb' = nil ->
  Genv.find_funct_ptr tge fb = Some (Internal fn) ->
  pstate cs2 = (State rs2 m2) ->
  pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex ->
  cur cs2 = tbb ->
  match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 ->
  match_asmstate fb cs2 (State rs1 m1) ->
  exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' ->
  (exists rs3 m3 rs4 m4,
      exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3
  /\  exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4
  /\  match_states S'' (State rs4 m4)).
Proof.
  intros until cs2. intros Hbody FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP.
  inv ESTEP.
  - inv MCS. inv MAS. simpl in *.
    inv Hpstate.
    destruct ctl.
    + (* MBcall *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0.

      assert (f0 = f) by congruence. subst f0.
      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
        eapply transf_function_no_overflow; eauto.
      destruct s1 as [rf|fid]; simpl in H1.
      * (* Indirect call *)
        monadInv H1. monadInv EQ.
        assert (ms' rf = Vptr f' Ptrofs.zero).
        { unfold find_function_ptr in H12. destruct (ms' rf); try discriminate.
          revert H12; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
        assert (rs2 x = Vptr f' Ptrofs.zero).
        { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }
        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
        remember (Ptrofs.add _ _) as ofs'.
        assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
        { econstructor; eauto. }
        assert (f1 = f) by congruence. subst f1.
        exploit return_address_offset_correct; eauto. intros; subst ra.

        repeat eexists.
        econstructor; eauto. econstructor.
          econstructor; eauto. econstructor; eauto.
          eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
          unfold incrPC; repeat Simpl; auto.
          simpl. unfold incrPC; rewrite Pregmap.gso; auto; try discriminate.
          rewrite !Pregmap.gss. rewrite PCeq. rewrite Heqofs'. simpl. auto.

      * (* Direct call *)
        monadInv H1.
        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
        remember (Ptrofs.add _ _) as ofs'.
        assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
          econstructor; eauto.
        assert (f1 = f) by congruence. subst f1.
        exploit return_address_offset_correct; eauto. intros; subst ra.
        repeat eexists.
        econstructor; eauto. econstructor.
          econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros.
        unfold incrPC; repeat Simpl; auto. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H12. rewrite H12. auto.
        unfold incrPC; simpl; rewrite Pregmap.gso; try discriminate. rewrite !Pregmap.gss.
        subst. unfold Val.offset_ptr. rewrite PCeq. auto.
    + (* MBtailcall *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0.

      assert (f0 = f) by congruence.  subst f0.
      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
        eapply transf_function_no_overflow; eauto.
      exploit Mem.loadv_extends. eauto. eexact H13. auto. simpl. intros [parent' [A B]].
      destruct s1 as [rf|fid]; simpl in H11. 
      * monadInv H1. monadInv EQ.
        assert (ms' rf = Vptr f' Ptrofs.zero).
          { destruct (ms' rf); try discriminate. revert H11. predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. }
        assert (rs2 x = Vptr f' Ptrofs.zero).
          { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. }

        assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
        exploit exec_straight_body; eauto.
        intros (l & MKEPI & EXEB).
        repeat eexists. rewrite app_nil_r in MKEPI.
        rewrite <- MKEPI in EXEB.
        eauto. econstructor. simpl. unfold incrPC.
        rewrite !Pregmap.gso; try discriminate. eauto.
        econstructor; eauto.
          { apply agree_set_other.
            - econstructor; auto with asmgen.
              + apply V.
              + intro r. destruct r; apply V; auto.
            - eauto with asmgen. }
        rewrite Pregmap.gss. rewrite Z; auto; try discriminate.
        eapply ireg_of_not_X30''; eauto.
        eapply ireg_of_not_X16''; eauto.
      * monadInv H1. assert (f = f1) by congruence. subst f1. clear FIND1. clear H12.
        exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
        exploit exec_straight_body; eauto.
        intros (l & MKEPI & EXEB).
        repeat eexists. inv EQ. rewrite app_nil_r in MKEPI.
        rewrite <- MKEPI in EXEB.
        eauto. inv EQ. econstructor. simpl. unfold incrPC.
        eauto.
        econstructor; eauto.
        { apply agree_set_other.
          - econstructor; auto with asmgen.
            + apply V.
            + intro r. destruct r; apply V; auto.
          - eauto with asmgen. }
        { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. }
    + (* MBbuiltin *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      
      assert (f0 = f) by congruence. subst f0.
      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
      eapply transf_function_no_overflow; eauto.
      generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.
      remember (Ptrofs.add _ _) as ofs'.
      assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc).
      econstructor; eauto.
      
      monadInv TBC. monadInv TIC. inv H0.
      
      exploit builtin_args_match; eauto. intros [vargs' [P Q]].
      exploit external_call_mem_extends; eauto.
      intros [vres' [m2' [A [B [C D]]]]].
  
      repeat eexists. econstructor. erewrite <- sp_val by eauto.
      eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
      eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto.
      econstructor; eauto.
      unfold incrPC. rewrite Pregmap.gss.
      rewrite set_res_other. rewrite undef_regs_other. unfold Val.offset_ptr. rewrite PCeq.
      eauto. 
      intros; simpl in *; destruct H as [HX16 | [HX30 | HDES]]; subst; try discriminate;
      exploit list_in_map_inv; eauto; intros [mr [E F]]; subst; discriminate.
      auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto.
      eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2'; auto.
      intros. discriminate.
    + (* MBgoto *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0.

      assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H9.
      remember (incrPC (Ptrofs.repr (size tbb)) rs2) as rs2'.
      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'.
      assert (tf = fn) by congruence. subst tf.
      exploit find_label_goto_label.
        eauto. eauto.
        instantiate (2 := rs2').
        { subst. unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. eauto. }
        eauto.
      intros (tc' & rs' & GOTO & AT2 & INV).

      eexists. eexists. repeat eexists. repeat split.
      econstructor; eauto.
        rewrite Heqrs2' in INV. unfold incrPC in INV.
        rewrite Heqrs2' in GOTO; simpl; eauto.
        econstructor; eauto.
        eapply agree_exten; eauto with asmgen.
        assert (forall r : preg, r <> PC -> rs' r = rs2 r).
        { intros. rewrite Heqrs2' in INV.
          rewrite INV; unfold incrPC; try rewrite Pregmap.gso; auto. }
        eauto with asmgen.
        congruence.
    + (* MBcond *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0. monadInv H1. monadInv EQ.

      * (* MBcond true *)
        assert (f0 = f) by congruence. subst f0.
        exploit eval_condition_lessdef.
          eapply preg_vals; eauto.
          all: eauto.
        intros EC.
        exploit transl_cbranch_correct_1; eauto. intros (rs', H).
        destruct H as [ES [ECFI]].
        exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
        assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
        rewrite PCeq' in PCeq.
        assert (f1 = f) by congruence. subst f1.
        exploit find_label_goto_label.
          4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')).
          unfold incrPC, Val.offset_ptr. rewrite PCeq. rewrite Pregmap.gss. eauto.
        intros (tc' & rs3 & GOTOL & TLPC & Hrs3).
        exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
        assert (tf = fn) by congruence. subst tf.

        repeat eexists.
          rewrite <- BTC. simpl. rewrite app_nil_r. eauto.
          rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto.

        econstructor; eauto.
          eapply agree_exten with rs2; eauto with asmgen.
          { intros. rewrite Hrs3; unfold incrPC. Simpl. rewrite H. all: auto. apply PC_not_data_preg; auto. }
        intros. discriminate.
      * (* MBcond false *)
        assert (f0 = f) by congruence. subst f0. monadInv H1. monadInv EQ.
        exploit eval_condition_lessdef.
          eapply preg_vals; eauto.
          all: eauto.
        intros EC.

        exploit transl_cbranch_correct_1; eauto. intros (rs', H).
        destruct H as [ES [ECFI]].
        exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
        assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
        rewrite PCeq' in PCeq.
        exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'.
        assert (tf = fn) by congruence. subst tf.

        assert (NOOV: size_blocks fn.(fn_blocks) <= Ptrofs.max_unsigned).
          eapply transf_function_no_overflow; eauto.
        generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1.

        repeat eexists.
          rewrite <- BTC. simpl. rewrite app_nil_r. eauto.
          rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto.

        econstructor; eauto.
          unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto.
          eapply agree_exten with rs2; eauto with asmgen.
          { intros. unfold incrPC. Simpl. rewrite H. all: auto. }
        intros. discriminate.
    + (* MBjumptable *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0.

      assert (f0 = f) by congruence. subst f0.
      monadInv H1. monadInv EQ.
      generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV.
      assert (f1 = f) by congruence. subst f1.
      exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef).
        unfold incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. discriminate.
      exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn.

      intros [tc' [rs' [A [B C]]]].
      exploit ireg_val; eauto. rewrite H11. intros LD; inv LD.
      
      repeat eexists. econstructor. simpl. Simpl. 2: { eapply ireg_of_not_X16''; eauto. }
        unfold incrPC. rewrite Pregmap.gso; try discriminate. rewrite <- H1.
        simpl. unfold Mach.label in H12. unfold label. rewrite H12. eapply A.
      econstructor; eauto.
        eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen.
        { unfold incrPC. repeat Simpl; auto. apply X16_not_data_preg; auto. }
        discriminate.
    + (* MBreturn *)
      destruct bb' as [mhd' mbdy' mex']; simpl in *. subst.
      inv TBC. inv TIC. inv H0.

      assert (f0 = f) by congruence. subst f0.
      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
        eapply transf_function_no_overflow; eauto.
      exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z).
      exploit exec_straight_body; eauto.
        simpl. eauto.
      intros EXEB. destruct EXEB as [l [MKEPI EXEB]].
      assert (f1 = f) by congruence. subst f1.
      
      repeat eexists.
        rewrite app_nil_r in MKEPI. rewrite <- MKEPI in EXEB. eauto.
        econstructor. simpl. reflexivity.
      econstructor; eauto.
        unfold incrPC. repeat apply agree_set_other; auto with asmgen.

  - inv MCS. inv MAS. simpl in *. subst. inv Hpstate.
    destruct bb' as [hd' bdy' ex']; simpl in *. subst.
    monadInv TBC. monadInv TIC. simpl in *.
    simpl. repeat eexists.
    econstructor. econstructor. 4: instantiate (3 := false). all:eauto.
      unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq.
      assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
        eapply transf_function_no_overflow; eauto.
      assert (f = f0) by congruence. subst f0. econstructor; eauto.
      generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto.
    eapply agree_exten; eauto. intros. unfold incrPC; Simpl; auto.
    discriminate.
Qed.

(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *)
Theorem step_simu_basic:
  forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy,
  MB.header bb = nil -> MB.body bb = bi::(bdy) ->
  bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} ->
  basic_step ge s fb sp ms m bi ms' m' ->
  pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy ->
  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
  (exists rs2 m2 l cs2 tbdy',
       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1;
                pctl := pctl cs1; ep := it1_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |}
    /\ tbdy = l ++ tbdy'
    /\ exec_body lk tge l rs1 m1 = Next rs2 m2
    /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2).
Proof.
  intros until bdy. intros Hheader Hbody (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS.
  simpl in *. inv Hpstate.
  rewrite Hbody in TBC. monadInv TBC.
  inv BSTEP.

  - (* MBgetstack *)
    simpl in EQ0.
    unfold Mach.load_stack in H.
    exploit Mem.loadv_extends; eauto. intros [v' [A B]].
    rewrite (sp_val _ _ _ AG) in A.
    exploit loadind_correct; eauto with asmgen.
    intros (rs2 & EXECS & Hrs'1 & Hrs'2).
    eapply exec_straight_body in EXECS.
    destruct EXECS as (l & Hlbi & EXECB).
    exists rs2, m1, l.
    eexists. eexists. split. instantiate (1 := x). eauto.
    repeat (split; auto).
    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
    subst. simpl in Hheadereq.

    eapply match_codestate_intro; eauto.
    eapply agree_set_mreg; eauto with asmgen.
    intro Hep. simpl in Hep. discriminate.
  - (* MBsetstack *)
    simpl in EQ0.
    unfold Mach.store_stack in H.
    assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. }
    exploit Mem.storev_extends; eauto. intros [m2' [A B]].
    exploit storeind_correct; eauto with asmgen.
    rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]].

    eapply exec_straight_body in P.
    destruct P as (l & ll & EXECB).
    exists rs', m2', l.
    eexists. eexists. split. instantiate (1 := x). eauto.
    repeat (split; auto).
    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
    subst.
    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
    eapply agree_undef_regs; eauto with asmgen.
    simpl; intros. rewrite Q; auto with asmgen. rewrite Hheader in DXP. auto.
  - (* MBgetparam *)
    simpl in EQ0.

    assert (f0 = f) by congruence; subst f0.
    unfold Mach.load_stack in *.
    exploit Mem.loadv_extends. eauto. eexact H0. auto.
    intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A.
    exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'.
    exploit Mem.loadv_extends. eauto. eexact H1. auto.
    intros [v' [C D]].

    monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP.
    destruct ep0 eqn:EPeq.

  (* X29 contains parent *)
    + exploit loadind_correct. eexact EQ1.
      instantiate (2 := rs1). rewrite DXP; eauto. discriminate.
      intros [rs2 [P [Q R]]].

      eapply exec_straight_body in P.
      destruct P as (l & ll & EXECB).
      exists rs2, m1, l. eexists.
      eexists. split. instantiate (1 := x). eauto.
      repeat (split; auto).
      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
      assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. }
      subst.
      eapply match_codestate_intro; eauto.

      eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
      simpl; intros. rewrite R; auto with asmgen. unfold preg_of.
      apply preg_of_not_X29; auto.

  (* X29 does not contain parent *)
    + rewrite chunk_of_Tptr in A. 
      exploit loadptr_correct. eexact A. discriminate. intros [rs2 [P [Q R]]].
      exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto.
      discriminate.
      intros [rs3 [S [T U]]].

      exploit exec_straight_trans.
        eapply P.
        eapply S.
      intros EXES.

      eapply exec_straight_body in EXES.
      destruct EXES as (l & ll & EXECB).
      exists rs3, m1, l.
      eexists. eexists. split. instantiate (1 := x). eauto.
      repeat (split; auto).
      remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
      assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
      subst.
      eapply match_codestate_intro; eauto.
      eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto.
      instantiate (1 := rs2#X29 <- (rs3#X29)). intros.
      rewrite Pregmap.gso; auto with asmgen.
      congruence.
      intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen.
      simpl; intros. rewrite U; auto with asmgen.
      apply preg_of_not_X29; auto.
  - (* MBop *)
    simpl in EQ0. rewrite Hheader in DXP.
    
    assert (eval_operation tge sp op (map ms args) m' = Some v).
      rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
    exploit eval_operation_lessdef.
      eapply preg_vals; eauto.
      2: eexact H0.
      all: eauto.
    intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A.
    exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].

    eapply exec_straight_body in P.
    destruct P as (l & ll & EXECB).
    exists rs2, m1, l.
    eexists. eexists. split. instantiate (1 := x). eauto.
    repeat (split; auto).
    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
    subst.
    eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto.
    apply agree_set_undef_mreg with rs1; auto. 
    apply Val.lessdef_trans with v'; auto.
    simpl; intros. destruct (andb_prop _ _ H1); clear H1.
    rewrite R; auto. apply preg_of_not_X29; auto.
Local Transparent destroyed_by_op.
    destruct op; simpl; auto; try discriminate.
  - (* MBload *)
    simpl in EQ0. rewrite Hheader in DXP.

    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
    exploit Mem.loadv_extends; eauto. intros [v' [C D]]. destruct trap; try discriminate.
    exploit transl_load_correct; eauto.
    intros [rs2 [P [Q R]]].

    eapply exec_straight_body in P.
    destruct P as (l & ll & EXECB).
    exists rs2, m1, l.
    eexists. eexists. split. instantiate (1 := x). eauto.
    repeat (split; auto).
    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
    subst.
    eapply match_codestate_intro; eauto.
    eapply agree_set_mreg; eauto with asmgen.
    intro Hep. simpl in Hep. discriminate.
  - (* MBload notrap1 *)
    simpl in EQ0. unfold transl_load in EQ0. discriminate.
  - (* MBload notrap2 *)
    simpl in EQ0. unfold transl_load in EQ0. discriminate.
  - (* MBstore *)
    simpl in EQ0. rewrite Hheader in DXP.

    assert (Op.eval_addressing tge sp addr (map ms args) = Some a).
      rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
    exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.
    intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.
    assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.
    exploit Mem.storev_extends; eauto. intros [m2' [C D]].
    exploit transl_store_correct; eauto. intros [rs2 [P Q]].

    eapply exec_straight_body in P.
    destruct P as (l & ll & EXECB).
    exists rs2, m2', l.
    eexists. eexists. split. instantiate (1 := x). eauto.
    repeat (split; auto).
    remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'.
    assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. }
    subst.
    eapply match_codestate_intro; eauto.
    eapply agree_undef_regs; eauto with asmgen.
    intro Hep. simpl in Hep. discriminate.
Qed.

Lemma exec_body_trans:
  forall l l' rs0 m0 rs1 m1 rs2 m2,
  exec_body lk tge l rs0 m0 = Next rs1 m1 ->
  exec_body lk tge l' rs1 m1 = Next rs2 m2 ->
  exec_body lk tge (l++l') rs0 m0 = Next rs2 m2.
Proof.
  induction l.
  - simpl. induction l'. intros.
    + simpl in *. congruence.
    + intros. inv H. auto.
  - intros until m2. intros EXEB1 EXEB2.
    inv EXEB1. destruct (exec_basic _) eqn:EBI; try discriminate.
    simpl. rewrite EBI. eapply IHl; eauto.
Qed.

Lemma exec_body_control:
  forall b t rs1 m1 rs2 m2 rs3 m3 fn,
  exec_body lk tge (body b) rs1 m1 = Next rs2 m2 ->
  exec_exit tge fn (Ptrofs.repr (size b)) rs2 m2 (exit b) t rs3 m3 ->
  exec_bblock lk tge fn b rs1 m1 t rs3 m3.
Proof.
  intros until fn. intros EXEB EXECTL.
  econstructor; eauto.
Qed.

Inductive exec_header: codestate -> codestate -> Prop :=
  | exec_header_cons: forall cs1,
      exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1;
                          pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1;
                          cur := cur cs1 |}.

(* Theorem (A) in the diagram, the easiest of all *)
Theorem step_simu_header:
  forall bb s fb sp c ms m rs1 m1 cs1,
  pstate cs1 = (State rs1 m1) ->
  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
  (exists cs1',
       exec_header cs1 cs1'
    /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1').
Proof.
  intros until cs1. intros Hpstate MCS.
  eexists. split; eauto.
  econstructor; eauto.
  inv MCS. simpl in *. inv Hpstate.
  econstructor; eauto.
Qed.

(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *)
Theorem step_simu_body:
  forall bb s fb sp c ms m rs1 m1 ms' cs1 m',
  MB.header bb = nil ->
  body_step ge s fb sp (MB.body bb) ms m ms' m' ->
  pstate cs1 = (State rs1 m1) ->
  match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 ->
  (exists rs2 m2 cs2 ep,
       cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1;
                pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |}
    /\ exec_body lk tge (pbody1 cs1) rs1 m1 = Next rs2 m2
    /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2).
Proof.
  intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy].
  - intros until m'. intros Hheader BSTEP Hpstate MCS.
    inv BSTEP.
    exists rs1, m1, cs1, (ep cs1).
    inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto).
    econstructor; eauto.
  - intros until m'. intros Hheader BSTEP Hpstate MCS. inv BSTEP.
    rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'.
    exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto.
    intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS').
    simpl in *.
    exploit IHbdy. auto. eapply H6. 2: eapply MCS'. all: eauto. subst; eauto. simpl; auto.
    intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS'').
    exists rs3, m3, cs3, ep.
    repeat (split; simpl; auto). subst. simpl in *. auto.
    rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
Qed.

(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *)
(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *)
Lemma step_simulation_bblock':
  forall t sf f sp bb bb' bb'' rs m rs' m' s'' c S1,
  bb' = mb_remove_header bb ->
  body_step ge sf f sp (Machblock.body bb') rs m rs' m' ->
  bb'' = mb_remove_body bb' ->
  exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' ->
  match_states (Machblock.State sf f sp (bb :: c) rs m) S1 ->
  exists S2 : state, plus (step lk) tge S1 t S2 /\ match_states s'' S2.
Proof.
  intros until S1. intros Hbb' BSTEP Hbb'' ESTEP MS.
  destruct (mbsize bb) eqn:SIZE.
  - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit).
    destruct bb as [hd bdy ex]; simpl in *; subst.
    inv MS. inv AT. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc.
    monadInv H2. simpl in *. inv ESTEP. inv BSTEP.
    eexists. split.
    + eapply plus_one.
      exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'.
      assert (x = tf) by congruence. subst x.
      eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto.
      unfold exec_bblock. simpl.
      eexists; eexists; split; eauto.
      econstructor.
    + econstructor.
      1,2,3: eauto.
      *
      unfold incrPC. rewrite Pregmap.gss.
      unfold Val.offset_ptr. rewrite <- H.
    assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned).
      { eapply transf_function_no_overflow; eauto. }
    econstructor; eauto.
      generalize (code_tail_next_int _ _ _ _ NOOV H3). intro CT1. eauto.
      *
    eapply agree_exten; eauto. intros. unfold incrPC. rewrite Pregmap.gso; auto.
    unfold data_preg in H2. destruct r; try congruence.
   *
    intros. discriminate.
  - subst. exploit mbsize_neqz. { instantiate (1 := bb). rewrite SIZE. discriminate. }
    intros Hnotempty.

    (* initial setting *)
    exploit match_state_codestate.
      eapply Hnotempty.
      all: eauto.
    intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate).

    (* step_simu_header part *)
    assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. }
    destruct H as (rs1 & m1 & Hpstate2). subst.
    assert (f = fb). { inv MCS. auto. } subst fb.
    exploit step_simu_header.
      2: eapply MCS.
      all: eauto.
    intros (cs1' & EXEH & MCS2).

    (* step_simu_body part *)
    assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. }
    exploit step_simu_body.
      2: eapply BSTEP.
      3: eapply MCS2.
      all: eauto. rewrite Hpstate'. eauto.
    intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS').

    (* step_simu_control part *)
    assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)).
    { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. }
    destruct H as (tf & FIND').
    inv EXEH. simpl in *.
    subst. exploit step_simu_control.
      8: eapply MCS'. all: simpl.
      9: eapply ESTEP.
      all: simpl; eauto.
      { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto.
        erewrite exec_body_pc; eauto. }
    intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS').

    (* bringing the pieces together *)
    exploit exec_body_trans.
      eapply EXEB.
      eauto.
    intros EXEB2.
    exploit exec_body_control; eauto.
    rewrite <- Hbody in EXEB2. eauto.
    rewrite Hexit. eauto.
    intros EXECB. (* inv EXECB. *)
    exists (State rs4 m4).
    split; auto. eapply plus_one. rewrite Hpstate2.
    assert (exists ofs, rs1 PC = Vptr f ofs).
    { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. }
    destruct H as (ofs & Hrs1pc).
    eapply exec_step_internal; eauto.

    (* proving the initial find_bblock *)
    rewrite Hpstate2 in MAS. inv MAS. simpl in *. 
    assert (f1 = f0) by congruence. subst f0.
    rewrite PCeq in Hrs1pc. inv Hrs1pc.
    exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''.
    inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ.
    eapply find_bblock_tail; eauto.
Qed.

Theorem step_simulation_bblock:
  forall t sf f sp bb ms m ms' m' S2 c,
  body_step ge sf f sp (Machblock.body bb) ms m ms' m' ->
  exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') t S2 ->
  forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' ->
  exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'.
Proof.
  intros until c. intros BSTEP ESTEP S1' MS.
  eapply step_simulation_bblock'; eauto.
  all: destruct bb as [hd bdy ex]; simpl in *; eauto.
  inv ESTEP.
  - econstructor. inv H; try (econstructor; eauto; fail).
  - econstructor.
Qed.

(* Measure to prove finite stuttering, see the other backends *)
Definition measure (s: MB.state) : nat :=
  match s with
  | MB.State _ _ _ _ _ _ => 0%nat
  | MB.Callstate _ _ _ _ => 0%nat
  | MB.Returnstate _ _ _ => 1%nat
  end.

Lemma next_sep:
  forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'.
Proof.
  congruence.
Qed.

(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs
   for the internal and external function cases *)
Theorem step_simulation:
  forall S1 t S2, MB.step return_address_offset ge S1 t S2 ->
  forall S1' (MS: match_states S1 S1'),
  (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2')
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
Proof.
  induction 1; intros.

- (* bblock *)
  left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0.
  all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; 
            try (rewrite MBE; try discriminate); eauto). 
  + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto.
- (* internal function *)
  inv MS.
  exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
  generalize EQ; intros EQ'. monadInv EQ'.
  destruct (zlt Ptrofs.max_unsigned (size_blocks x0.(fn_blocks))); inversion EQ1. clear EQ1. subst x0.
  unfold Mach.store_stack in *.
  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
  intros [m1' [C D]].
  exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
  intros [m2' [F G]].
  simpl chunk_of_type in F.
  exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
  intros [m3' [P Q]].
  (* Execution of function prologue *)
  monadInv EQ0.
  set (tfbody := make_prologue f x0) in *.
  set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *.
  set (rs2 := rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef).
  exploit (storeptr_correct lk tge XSP (fn_retaddr_ofs f) RA nil m2' m3' rs2).
  { rewrite chunk_of_Tptr in P.
    assert (rs0 X30 = rs2 RA) by auto.
    rewrite <- H3.
    rewrite ATLR.
    change (rs2 XSP) with sp. eexact P. }
  1-2: discriminate.
  intros (rs3 & U & V).
  assert (EXEC_PROLOGUE: exists rs3',
            exec_straight_blocks tge lk tf
              tf.(fn_blocks) rs0 m'
              x0 rs3' m3'
          /\ forall r, r <> PC -> r <> X16 -> rs3' r = rs3 r).
  { eexists. split.
    - change (fn_blocks tf) with tfbody; unfold tfbody.
      econstructor; eauto.
      assert (Archi.ptr64 = true) as SF; auto.
      + unfold exec_bblock. simpl exec_body.
        rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F.
        assert (Mptr = Mint64) by auto. rewrite H3 in F. simpl in F. rewrite F. simpl.
        unfold exec_store_rs_a. repeat Simpl; try discriminate.
        exists rs2. exists m3'. split.
        * unfold eval_addressing. Simpl; try discriminate. rewrite Pregmap.gss.
          rewrite chunk_of_Tptr in P. rewrite H3 in P.
          unfold Val.addl. unfold Val.offset_ptr in P.
          destruct sp; simpl; try discriminate. rewrite SF; simpl.
          rewrite Ptrofs.of_int64_to_int64. unfold Mem.storev in P. rewrite ATLR.
          rewrite P. simpl. apply next_sep; eauto. apply SF.
        * econstructor.
      + eauto.
    - intros. unfold incrPC.
      rewrite Pregmap.gso; auto. rewrite V; auto.
  } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3').
  exploit exec_straight_steps_2; eauto using functions_transl.
  simpl fn_blocks. simpl fn_blocks in g. lia. constructor.
  intros (ofs' & X & Y).
  left; exists (State rs3' m3'); split.
  eapply exec_straight_steps_1; eauto.
  simpl fn_blocks. simpl fn_blocks in g. lia.
  constructor.
  econstructor; eauto.
  rewrite X; econstructor; eauto. 
  apply agree_exten with rs2; eauto with asmgen.
  unfold rs2. 
  apply agree_set_other; auto with asmgen.
  apply agree_change_sp with (parent_sp s). 
  apply agree_undef_regs with rs0. auto.
Local Transparent destroyed_at_function_entry.
  simpl; intros; Simpl. auto.
  assert (r' <> X29). { contradict H3; rewrite H3; unfold data_preg; auto. } auto.
  unfold sp; congruence.

  intros.

  rewrite Heqrs3'. rewrite V. 2-5: try apply X16_not_data_preg; try apply PC_not_data_preg; auto.
  auto.
  intros. rewrite Heqrs3'; try discriminate. rewrite V by auto with asmgen. reflexivity.
- (* external function *)
  inv MS.
  exploit functions_translated; eauto.
  intros [tf [A B]]. simpl in B. inv B.
  exploit extcall_arguments_match; eauto.
  intros [args' [C D]].
  exploit external_call_mem_extends; eauto.
  intros [res' [m2' [P [Q [R S]]]]].
  left; econstructor; split.
  apply plus_one. eapply exec_step_external; eauto.
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  econstructor; eauto.
  unfold loc_external_result.
  apply agree_set_other; auto.
  apply agree_set_pair; auto.
  apply agree_undef_caller_save_regs; auto.

- (* return *) 
  inv MS.
  inv STACKS. simpl in *.
  right. split. lia. split. auto.
  rewrite <- ATPC in H5.
  econstructor; eauto. congruence.
Qed.

Lemma transf_initial_states:
  forall st1, MB.initial_state prog st1 ->
  exists st2, AB.initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. 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.
  apply Mem.extends_refl.
  split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence.
  intros. rewrite Mach.Regmap.gi. auto.
  unfold Genv.symbol_address.
  rewrite (match_program_main TRANSF).
  rewrite symbols_preserved.
  unfold ge; rewrite H1. auto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> MB.final_state st1 r -> AB.final_state st2 r.
Proof.
  intros. inv H0. inv H. constructor. assumption.
  compute in H1. inv H1.
  generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto.
Qed.

Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := 
  Asmblockgenproof0.return_address_offset.

Lemma transf_program_correct:
  forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog).
Proof.
  eapply forward_simulation_star with (measure := measure).
  - apply senv_preserved.
  - eexact transf_initial_states.
  - eexact transf_final_states.
  - exact step_simulation.
Qed.

End PRESERVATION.