Module Tailrecproof


Require Import Coqlib Wfsimpl Maps Errors Integers.
Require Import AST Linking Values Memory Globalenvs Events Smallstep.
Require Import Op Registers RTL.
Require Import Tailrec.

Lemma mem_free_perm_4:
  forall (m1 : mem) (bf : block) (lo hi : Z) (m2 : mem),
    Mem.free m1 bf lo hi = Some m2 ->
    forall (ofs : Z) (k : perm_kind) (p : permission),
      lo <= ofs < hi -> Mem.perm m1 bf ofs k p.
Proof.
  Local Transparent Mem.free.
  unfold Mem.free.
  intros.
  destruct Mem.range_perm_dec. 2: discriminate.
  unfold Mem.range_perm in *.
  apply Mem.perm_implies with (p1 := Freeable).
  2: apply perm_F_any; fail.
  apply Mem.perm_cur. auto.
Qed.

Lemma successors_inside_sound :
  forall f
         (INSIDE : successors_inside f = true)
         pc instr pc'
         (AT : (fn_code f) ! pc = Some instr)
         (IN : In pc' (successors_instr instr)),
    (pc' <= max_pc_function f)%positive.
Proof.
  unfold successors_inside. intros.
  rewrite List.forallb_forall in INSIDE.
  pose proof (INSIDE _ (PTree.elements_correct _ _ AT)) as SUCCESSORS.
  cbn in SUCCESSORS.
  rewrite List.forallb_forall in SUCCESSORS.
  apply Pos.leb_le.
  apply SUCCESSORS. assumption.
Qed.

Lemma transf_function_successors:
  forall ge id f tf
         (TRANSF : (transf_function ge id f) = OK tf) pc
         instr (AT : (fn_code f) ! pc = Some instr)
         pc' (IN : In pc' (successors_instr instr)),
    (pc' <= max_pc_function f)%positive.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f) eqn:TEST. 2: discriminate.
  clear TRANSF.
  apply successors_inside_sound with (pc := pc) (instr := instr); trivial.
Qed.

Remark succ_le: forall a b, ((Pos.succ a) <= b)%positive -> (a <= b)%positive.
Proof.
  intros. lia.
Qed.

Lemma copy_to_temps_increases:
  forall srcregs tmpreg pc prec_code,
    (pc <=
    (fst (copy_to_temps srcregs tmpreg pc prec_code)))%positive.
Proof.
  induction srcregs; cbn in *; intros.
  lia.
  apply succ_le. apply IHsrcregs.
Qed.

Lemma copy_from_temps_increases:
  forall params tmpreg pc prec_code,
    (pc <=
    (fst (copy_from_temps params tmpreg pc prec_code)))%positive.
Proof.
  induction params; cbn in *; intros.
  lia.
  apply succ_le. apply IHparams.
Qed.

Lemma copy_to_temps_preserves:
  forall srcregs tmpreg pc prec_code pc' (LT : (pc' < pc)%positive),
    (snd (copy_to_temps srcregs tmpreg pc prec_code)) ! pc' =
      prec_code ! pc'.
Proof.
  induction srcregs; cbn in *; intros.
  reflexivity.
  rewrite IHsrcregs by lia.
  rewrite PTree.gso by lia.
  reflexivity.
Qed.
  
Lemma copy_from_temps_preserves:
  forall srcregs tmpreg pc prec_code pc' (LT : (pc' < pc)%positive),
    (snd (copy_from_temps srcregs tmpreg pc prec_code)) ! pc' =
      prec_code ! pc'.
Proof.
  induction srcregs; cbn in *; intros.
  reflexivity.
  rewrite IHsrcregs by lia.
  rewrite PTree.gso by lia.
  reflexivity.
Qed.

Lemma copy_to_temps_set:
  forall srcregs tmpreg pc prec_code k
         (LT : (k < List.length srcregs)%nat),
    (snd (copy_to_temps srcregs tmpreg pc prec_code)) !
       (Pos.of_nat ((Pos.to_nat pc) + k)%nat) = Some
      (Iop Omove ((nth k srcregs 1%positive)::nil)
           (Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)
           (Pos.of_nat ((Pos.to_nat pc) + k + 1)%nat)).
Proof.
  induction srcregs; cbn; intros.
  lia.
  destruct k.
  { rewrite copy_to_temps_preserves by lia.
    replace (Pos.of_nat (Pos.to_nat pc + 0)) with pc by lia.
    rewrite PTree.gss.
    f_equal. f_equal. lia. lia.
  }
  replace (Pos.to_nat pc + S k)%nat with
    (Pos.to_nat (Pos.succ pc) + k)%nat by lia.
  rewrite IHsrcregs by lia.
  f_equal. f_equal. f_equal. lia.
Qed.

Lemma copy_to_temps_end:
  forall srcregs tmpreg pc prec_code,
    (fst (copy_to_temps srcregs tmpreg pc prec_code)) =
      Pos.of_nat ((Pos.to_nat pc) + (List.length srcregs)).
Proof.
  induction srcregs; cbn; intros.
  lia.
  rewrite IHsrcregs. lia.
Qed.

Lemma copy_from_temps_set:
  forall dstregs tmpreg pc prec_code k
         (LT : (k < List.length dstregs)%nat),
    (snd (copy_from_temps dstregs tmpreg pc prec_code)) !
       (Pos.of_nat ((Pos.to_nat pc) + k)%nat) = Some
           (Iop Omove ((Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)::nil)
           (nth k dstregs 1%positive)
           (Pos.of_nat ((Pos.to_nat pc) + k + 1)%nat)).
Proof.
  induction dstregs; cbn; intros.
  lia.
  destruct k.
  { rewrite copy_from_temps_preserves by lia.
    replace (Pos.of_nat (Pos.to_nat pc + 0)) with pc by lia.
    rewrite PTree.gss.
    f_equal. f_equal. f_equal. lia. lia.
  }
  replace (Pos.to_nat pc + S k)%nat with
    (Pos.to_nat (Pos.succ pc) + k)%nat by lia.
  rewrite IHdstregs by lia.
  f_equal. f_equal. f_equal. lia.
Qed.

Lemma copy_from_temps_end:
  forall dstregs tmpreg pc prec_code,
    (fst (copy_from_temps dstregs tmpreg pc prec_code)) =
      Pos.of_nat ((Pos.to_nat pc) + (List.length dstregs)).
Proof.
  induction dstregs; cbn; intros.
  lia.
  rewrite IHdstregs. lia.
Qed.

Lemma build_jump_set1:
  forall start tmpreg srcregs dstregs pc0 code0 k
         (LT : (k < length srcregs)%nat),
    (snd (build_jump start tmpreg srcregs dstregs pc0 code0)) !
       (Pos.of_nat ((Pos.to_nat pc0) + k)%nat) = Some
      (Iop Omove ((nth ((length srcregs) - S k) srcregs 1%positive)::nil)
           (Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)
           (Pos.of_nat ((Pos.to_nat pc0) + k + 1)%nat)).
Proof.
  unfold build_jump. intros.
  pose proof LT as LT0.
  rewrite <- rev_length in LT.
  pose proof (copy_to_temps_set (rev srcregs) tmpreg pc0 code0 k LT) as C1.
  pose proof (copy_to_temps_end (rev srcregs) tmpreg pc0 code0) as E1.
  destruct (copy_to_temps (rev srcregs) tmpreg pc0 code0) as [pc1 code1].
  cbn in *.
  assert ((Pos.of_nat (Pos.to_nat pc0 + k) < pc1)%positive) as LT1 by lia.
  pose proof (copy_from_temps_preserves (rev dstregs) tmpreg pc1 code1
               (Pos.of_nat (Pos.to_nat pc0 + k)) LT1) as C2.
  pose proof (copy_from_temps_end (rev dstregs) tmpreg pc1 code1) as E2.
  destruct (copy_from_temps (rev dstregs) tmpreg pc1 code1) as [pc2 code2].
  cbn in *.
  rewrite PTree.gso by lia.
  rewrite C2. rewrite <- rev_nth by assumption. apply C1.
Qed.

Lemma build_jump_set2:
  forall start tmpreg srcregs dstregs pc0 code0 k
         (LT : (k < length dstregs)%nat),
    (snd (build_jump start tmpreg srcregs dstregs pc0 code0)) !
       (Pos.of_nat ((Pos.to_nat pc0) + (List.length srcregs) + k)%nat) = Some
      (Iop Omove ((Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)::nil)
           (nth ((length dstregs) - S k) dstregs 1%positive)
           (Pos.of_nat ((Pos.to_nat pc0) + (length srcregs) + k + 1)%nat)).
Proof.
  unfold build_jump. intros.
  pose proof LT as LT0.
  rewrite <- rev_length in LT.
  pose proof (copy_to_temps_end (rev srcregs) tmpreg pc0 code0) as E1.
  destruct (copy_to_temps (rev srcregs) tmpreg pc0 code0) as [pc1 code1].
  cbn in *.
  pose proof (copy_from_temps_set (rev dstregs) tmpreg pc1 code1 k LT) as C2.
  pose proof (copy_from_temps_end (rev dstregs) tmpreg pc1 code1) as E2.
  destruct (copy_from_temps (rev dstregs) tmpreg pc1 code1) as [pc2 code2].
  cbn in *.
  rewrite rev_length in E2.
  rewrite rev_length in E1.
  rewrite PTree.gso by lia.
  replace (Pos.of_nat (Pos.to_nat pc0 + Datatypes.length srcregs + k))
    with (Pos.of_nat (Pos.to_nat pc1 + k)) by lia.
  replace (Pos.of_nat (Pos.to_nat pc1 + k + 1)) with
    (Pos.of_nat (Pos.to_nat pc0 + Datatypes.length srcregs + k + 1)) in C2 by lia.
  rewrite C2. rewrite <- rev_nth by assumption. reflexivity.
Qed.

Lemma build_jump_set3:
  forall start tmpreg srcregs dstregs pc0 code0,
    (snd (build_jump start tmpreg srcregs dstregs pc0 code0)) !
                                                              (Pos.of_nat ((Pos.to_nat pc0) + (List.length srcregs) + (List.length dstregs))%nat) = Some (Inop start).
Proof.
  unfold build_jump. intros.
  pose proof (copy_to_temps_end (rev srcregs) tmpreg pc0 code0) as E1.
  destruct (copy_to_temps (rev srcregs) tmpreg pc0 code0) as [pc1 code1].
  cbn in *.
  pose proof (copy_from_temps_end (rev dstregs) tmpreg pc1 code1) as E2.
  destruct (copy_from_temps (rev dstregs) tmpreg pc1 code1) as [pc2 code2].
  cbn in *.
  rewrite rev_length in E1.
  rewrite rev_length in E2.
  replace (Pos.of_nat
             (Pos.to_nat pc0 + Datatypes.length srcregs + Datatypes.length dstregs))
    with pc2 by lia.
  apply PTree.gss.
Qed.

Inductive is_rec_call
  start tmpreg srcregs dstregs pc0 code :=
  is_rec_call_intro
    (TO_TEMPS :
       forall k
         (LT : (k < List.length srcregs)%nat),
    code ! (Pos.of_nat ((Pos.to_nat pc0) + k)%nat) = Some
      (Iop Omove ((nth (length srcregs - S k) srcregs 1%positive)::nil)
           (Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)
           (Pos.of_nat ((Pos.to_nat pc0) + k + 1)%nat)))
    (FROM_TEMPS :
      forall k
       (LT : (k < List.length dstregs)%nat),
    code !
       (Pos.of_nat ((Pos.to_nat pc0) + (List.length srcregs) + k)%nat) = Some
      (Iop Omove ((Pos.of_nat ((Pos.to_nat tmpreg) + k)%nat)::nil)
           (nth (length dstregs - S k) dstregs 1%positive)
           (Pos.of_nat ((Pos.to_nat pc0) + (List.length srcregs) + k + 1)%nat)))
    (BACKJUMP :
      code ! (Pos.of_nat ((Pos.to_nat pc0) +
      (List.length srcregs) + (List.length dstregs))%nat) = Some (Inop start)).

Lemma build_jump_set:
  forall start tmpreg srcregs dstregs pc0 code0,
    is_rec_call start tmpreg srcregs dstregs pc0
                (snd (build_jump start tmpreg srcregs dstregs pc0 code0)).
Proof.
  intros. constructor.
  - apply build_jump_set1.
  - apply build_jump_set2.
  - apply build_jump_set3.
Qed.

Lemma build_jump_end:
  forall start tmpreg srcregs dstregs pc0 code0,
    (fst (build_jump start tmpreg srcregs dstregs pc0 code0)) =
      (Pos.of_nat ((Pos.to_nat pc0) + 1 +
         (List.length srcregs) + (List.length dstregs))%nat).
Proof.
  unfold build_jump. intros.
  pose proof (copy_to_temps_end (rev srcregs) tmpreg pc0 code0) as E1.
  destruct (copy_to_temps (rev srcregs) tmpreg pc0 code0) as [pc1 code1].
  pose proof (copy_from_temps_end (rev dstregs) tmpreg pc1 code1) as E2.
  destruct (copy_from_temps (rev dstregs) tmpreg pc1 code1) as [pc2 code2].
  cbn in *.
  rewrite rev_length in E1. rewrite rev_length in E2.
  lia.
Qed.

Lemma process_instr_preserves:
  forall id start params tmpreg new_pc new_code pc instr pc'
         (LT : (pc' < new_pc)%positive)
         (NEQ : (pc' <> pc)%positive),
  (snd (process_instr id start params tmpreg new_pc new_code pc instr)) ! pc' =
    new_code ! pc'.
Proof.
  unfold process_instr. intros.
  destruct instr; try reflexivity.
  destruct s0. reflexivity.
  destruct (_ && _). 2: reflexivity.
  unfold build_jump.
  pose proof (copy_to_temps_preserves (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code) pc' LT) as REW1.
  pose proof (copy_to_temps_increases (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code)) as INCR1.
  destruct (copy_to_temps (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code)) as [pc1 code1].
  cbn in REW1, INCR1.
  assert (pc' < pc1)%positive as LT1 by lia.
  pose proof (copy_from_temps_preserves (rev params) tmpreg pc1 code1 pc' LT1) as REW2.
  pose proof (copy_from_temps_increases (rev params) tmpreg pc1 code1) as INCR2.
  destruct (copy_from_temps (rev params) tmpreg pc1 code1) as [pc2 code2].
  cbn in REW2, INCR2. cbn.
  rewrite PTree.gso by lia.
  rewrite REW2. rewrite REW1.
  apply PTree.gso. assumption.
Qed.

Lemma process_instr_at:
  forall id start params tmpreg new_pc new_code pc instr
         (LT : (pc < new_pc)%positive),
  (snd (process_instr id start params tmpreg new_pc new_code pc instr)) ! pc =
    match instr with
    | Itailcall sig (inr id') srcregs =>
        if (QualIdent.eq id id') &&
           (Nat.eq_dec (List.length srcregs) (List.length params))
        then Some (Inop new_pc)
        else new_code ! pc
    | _ => new_code ! pc
    end.
Proof.
  unfold process_instr. intros.
  destruct instr; try reflexivity.
  destruct s0. reflexivity.
  destruct (_ && _) eqn:COND. 2: reflexivity.
  unfold build_jump.
  pose proof (copy_to_temps_preserves (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code) pc LT) as REW1.
  pose proof (copy_to_temps_increases (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code)) as INCR1.
  destruct (copy_to_temps (rev l) tmpreg new_pc (PTree.set pc (Inop new_pc) new_code)) as [pc1 code1].
  cbn in REW1, INCR1.
  assert (pc < pc1)%positive as LT1 by lia.
  pose proof (copy_from_temps_preserves (rev params) tmpreg pc1 code1 pc LT1) as REW2.
  pose proof (copy_from_temps_increases (rev params) tmpreg pc1 code1) as INCR2.
  destruct (copy_from_temps (rev params) tmpreg pc1 code1) as [pc2 code2].
  cbn in REW2, INCR2. cbn.
  rewrite PTree.gso by lia.
  rewrite REW2. rewrite REW1.
  apply PTree.gss.
Qed.

Lemma process_instr_increases:
  forall id entrypoint params new_reg new_pc code0 pc instr,
    (new_pc <= (fst (process_instr id entrypoint params new_reg new_pc code0 pc instr)))%positive.
Proof.
  unfold process_instr. intros.
  destruct instr; cbn; try lia.
  destruct s0. cbn; lia.
  destruct (_ && _). 2: cbn; lia.
  unfold build_jump.
  pose proof (copy_to_temps_increases (rev l) new_reg new_pc (PTree.set pc (Inop new_pc) code0)) as INCR1.
  destruct (copy_to_temps (rev l) new_reg new_pc (PTree.set pc (Inop new_pc) code0)) as [pc1 code1].
  pose proof (copy_from_temps_increases (rev params) new_reg pc1 code1) as INCR2.
  destruct (copy_from_temps (rev params) new_reg pc1 code1) as [pc2 code2].
  cbn in *. lia.
Qed.

Lemma fold_process_instr_preserves :
  forall id entrypoint params l new_reg new_pc code0 pc'
         (ALL_LT : forall pc instr,
           In (pc, instr) l -> (pc < new_pc)%positive)
         (NO_OVERRIDE : forall instr,
             In (pc', instr) l ->
             match instr with
             | Itailcall sig (inr id') srcregs =>
                 if (QualIdent.eq id id') &&
                      (Nat.eq_dec (List.length srcregs)
                              (List.length params))
                 then False
                 else True
             | _ => True
             end)
       (LT' : (pc' < new_pc)%positive),
     (snd (fold_left
        (fun (a : node * code) (p : positive * instruction) =>
         let (new_pc, new_code) := a in
         process_instr id entrypoint params
           new_reg new_pc new_code
           (fst p) (snd p)) l
        (new_pc, code0))) ! pc' = code0 ! pc'.
Proof.
  induction l; cbn; intros. reflexivity.
  destruct a as [pc instr]. cbn.
  assert (pc < new_pc)%positive as LT.
  { eapply ALL_LT. left. reflexivity. }
  pose proof (process_instr_at id entrypoint params new_reg new_pc code0 pc instr LT) as AT.
  pose proof (process_instr_preserves id entrypoint params new_reg new_pc code0 pc instr pc' LT') as PRESERVE.
  pose proof (process_instr_increases id entrypoint params new_reg new_pc code0 pc instr) as INCR.
  destruct (process_instr id entrypoint params new_reg new_pc code0 pc instr) as [new_pc1 code1]. (* eqn:PROCESS. *)
  cbn in AT, PRESERVE, INCR.
  rewrite IHl; cycle 1.
  { intros pc0 instr0 IN0.
    assert (pc0 < new_pc)%positive.
    { eapply ALL_LT. right. exact IN0. }
    lia.
  }
  { intros instr0 IN0.
    apply NO_OVERRIDE. right. assumption. }
  lia.
  destruct (peq pc' pc) as [EQ | NEQ] ; cycle 1.
  { exact (PRESERVE NEQ). }
  subst pc'.
  assert (match instr with
                | Itailcall _ (inr id') srcregs =>
                    if
                     QualIdent.eq id id' &&
                     Nat.eq_dec (Datatypes.length srcregs)
                       (Datatypes.length params)
                    then False
                    else True
                | _ => True
                end) as NO.
  { apply NO_OVERRIDE. left. reflexivity. }
  destruct instr; try assumption.
  destruct s0. assumption.
  destruct (_ && _). lia. assumption.
Qed.
                     
Lemma transf_function_preserves: forall ge id f tf pc
    (UNCHANGED :
      match (fn_code f) ! pc with
      | Some (Itailcall sig (inr id') srcregs) =>
          if (QualIdent.eq id id') &&
               (Nat.eq_dec (List.length srcregs) (List.length (fn_params f)))
          then False
          else True
      | Some _ => True
      | None => False
      end)
    (TRANSF : transf_function ge id f = OK tf),
    (fn_code tf) ! pc = (fn_code f) ! pc.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv TRANSF. cbn.
  rewrite PTree.fold_spec.
  rewrite fold_process_instr_preserves.
  reflexivity.
  { intros.
    assert (pc0 <= (max_pc_function f))%positive.
    { apply max_pc_function_sound with (i := instr).
      apply PTree.elements_complete.
      assumption. }
    lia.
  }
  { intros instr IN.
    apply PTree.elements_complete in IN.
    rewrite IN in UNCHANGED.
    exact UNCHANGED.
  }
  assert (pc <= (max_pc_function f))%positive. 2: lia.
  destruct ((fn_code f)!pc) eqn:CODE.
  eapply max_pc_function_sound. eassumption.
  contradiction.
Qed.

Lemma fold_tail_rec:
  forall start reg0 params id sig args at_pc
         (LENGTHS : (length args) = (length params))
         elts (NOREPET: list_norepet (map fst elts)) pc0
         (BELOW : forall pc i, In (pc, i) elts -> (pc < pc0)%positive)
         (code0 : code)
         (IN : In (at_pc, (Itailcall sig (inr id) args)) elts),
  let (next_pc', code') := fold_left
                 (fun (a : node * code) (p : positive * instruction) =>
                    let (new_pc, new_code) := a in
                    process_instr id start
                                  params reg0 new_pc
                                  new_code (fst p) (snd p))
                 elts
                 (pc0, code0) in
  exists next_pc,
    code' ! at_pc = Some (Inop next_pc) /\
      is_rec_call start reg0 args params next_pc code'.
Proof.
  induction elts; intros; inv IN; cbn.
  - destruct (QualIdent.eq id id); [(cbn ; clear e) | contradiction].
    destruct (Nat.eq_dec (Datatypes.length args) (Datatypes.length params)); [(cbn ; clear e) | contradiction].
    destruct fold_left as (next_pc', code') eqn:FOLD. clear IHelts.
    exists pc0.
    set (fold_result :=(fold_left
           (fun (a : node * code) (p : positive * instruction) =>
            let (new_pc, new_code) := a in
            process_instr id start params reg0 new_pc new_code (fst p) (snd p))
           elts
           (build_jump start reg0 args params pc0
                       (PTree.set at_pc (Inop pc0) code0)))) in FOLD.
    assert (at_pc < pc0)%positive as BELOWat.
    { eapply BELOW. cbn. left. reflexivity.
    }
    split.
    + replace code' with (snd fold_result); cycle 1.
      { rewrite FOLD. reflexivity. }
      destruct build_jump eqn:JUMP.
      unfold build_jump in JUMP.
      pose proof (copy_to_temps_preserves (rev args) reg0 pc0
                                          (PTree.set at_pc (Inop pc0) code0) at_pc BELOWat) as COPY1.
      pose proof (copy_to_temps_increases (rev args) reg0 pc0
                                          (PTree.set at_pc (Inop pc0) code0)) as INC1.
      destruct copy_to_temps. cbn in COPY1, INC1.
      rewrite PTree.gss in COPY1.
      assert (at_pc < n0)%positive as AT2 by lia.
      pose proof (copy_from_temps_preserves (rev params) reg0 n0 c0 _ AT2) as COPY2.
      pose proof (copy_from_temps_increases (rev params) reg0 n0 c0) as INC2.
      destruct copy_from_temps. cbn in COPY2, INC2.
      unfold fold_result. inv JUMP.
      rewrite fold_process_instr_preserves.
      * rewrite PTree.gso by lia.
        rewrite COPY2. exact COPY1.
      * intros. assert (pc < pc0)%positive.
        { eapply BELOW. cbn. right. exact H. }
        lia.
      * cbn in NOREPET. inv NOREPET. intros.
        pose proof (in_map fst elts _ H) as Z. cbn in Z.
        contradiction.
      * lia.
    + pose proof (build_jump_end start reg0 args params pc0
                                 (PTree.set at_pc (Inop pc0) code0)) as END.
      destruct (build_jump_set start reg0 args params pc0
                                 (PTree.set at_pc (Inop pc0) code0)).
      destruct build_jump eqn:JUMP. cbn in *.
      replace code' with (snd fold_result); cycle 1.
      { rewrite FOLD. reflexivity. }
      constructor.
      * intros. unfold fold_result.
        rewrite fold_process_instr_preserves.
        -- apply TO_TEMPS; auto.
        -- intros. assert (pc < pc0)%positive.
           { eapply BELOW. cbn. right. exact H. }
           lia.
        -- intros. exfalso.
           assert ((Pos.of_nat (Pos.to_nat pc0 + k)) < pc0)%positive as Z.
           { eapply BELOW. right. exact H. }
           lia.
        -- rewrite END. change reg with positive. lia.
      * intros. unfold fold_result.
        rewrite fold_process_instr_preserves.
        -- apply FROM_TEMPS; auto.
        -- intros. assert (pc < pc0)%positive.
           { eapply BELOW. cbn. right. exact H. }
           lia.
        -- intros. exfalso.
           assert (Pos.of_nat (Pos.to_nat pc0 + Datatypes.length args + k) < pc0)%positive as Z.
           { eapply BELOW. right. exact H. }
           lia.
        -- rewrite END. change reg with positive. lia.
      * unfold fold_result.
        rewrite fold_process_instr_preserves.
        -- assumption.
        -- intros. assert (pc < pc0)%positive.
           { eapply BELOW. cbn. right. exact H. }
           lia.
        -- intros. exfalso.
           assert ((Pos.of_nat
                      (Pos.to_nat pc0 + Datatypes.length args + Datatypes.length params)) < pc0)%positive as Z.
           { eapply BELOW. right. exact H. }
           lia.
        -- rewrite END. change reg with positive. lia.
  - inv NOREPET.
    assert (forall (pc : positive) (i : instruction),
  In (pc, i) elts ->
  (pc < fst (process_instr id start params reg0 pc0 code0 (fst a) (snd a)))%positive) as BELOW'.
    { intros.
      assert (pc0 <= fst (process_instr id start params reg0 pc0 code0 (fst a) (snd a)))%positive as INC.
      { apply process_instr_increases. }
      assert (pc < pc0)%positive.
      { eapply BELOW. right. exact H0. }
      lia.
    }
    pose proof (IHelts H3 (fst (process_instr id start params reg0 pc0 code0 (fst a) (snd a))) BELOW' (snd (process_instr id start params reg0 pc0 code0 (fst a) (snd a))) H).
    destruct process_instr as (pc1, code1). cbn in H0.
    destruct fold_left.
    assumption.
Qed.
    
Lemma transf_function'_tail_rec: forall sig id f tf pc args
    (TRANSF : transf_function' id f = OK tf)
    (AT : (fn_code f) ! pc = Some (Itailcall sig (inr id) args))
    (LENGTHS : (List.length args) = (List.length (fn_params f))),
  exists next_pc,
    (fn_code tf) ! pc = Some (Inop next_pc) /\
      is_rec_call (fn_entrypoint f) (Pos.succ (max_reg_function f))
                  args (fn_params f) next_pc
                  (fn_code tf).
Proof.
  intros.
  unfold transf_function' in *.
  rewrite PTree.fold_spec in *.
  apply PTree.elements_correct in AT.
  pose proof (PTree.elements_keys_norepet (fn_code f)) as NOREPET.
  assert (forall (pc : positive) (i : instruction),
  In (pc, i) (PTree.elements (fn_code f)) ->
  (pc < Pos.succ (max_pc_function f))%positive) as BELOW.
  { intros.
    assert (pc0 <= max_pc_function f)%positive.
    { eapply max_pc_function_sound.
      apply PTree.elements_complete. exact H. }
    lia.
  }
  pose proof (fold_tail_rec (fn_entrypoint f) (Pos.succ (max_reg_function f)) (fn_params f) id sig args pc LENGTHS (PTree.elements (fn_code f)) NOREPET (Pos.succ (max_pc_function f)) BELOW (fn_code f) AT).
  destruct fold_left.
  inv TRANSF. cbn. assumption.
Qed.

Lemma transf_function_tail_rec: forall ge sig id f tf pc args
    (TRANSF : transf_function ge id f = OK tf)
    (AT : (fn_code f) ! pc = Some (Itailcall sig (inr id) args))
    (LENGTHS : (List.length args) = (List.length (fn_params f))),
  exists next_pc,
    (fn_code tf) ! pc = Some (Inop next_pc) /\
      is_rec_call (fn_entrypoint f) (Pos.succ (max_reg_function f))
                  args (fn_params f) next_pc
                  (fn_code tf).
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct successors_inside. 2: discriminate.
  eapply transf_function'_tail_rec; eassumption.
Qed.

Definition block2sp sp := Vptr sp (Ptrofs.repr 0).

Lemma exec_jump1:
  forall tge args
  tf start next_reg next_pc ts trs tm tsp
  (BELOW: Forall (fun r => (r < next_reg)%positive) args)
  (REC_CALL : is_rec_call start next_reg
                  args (fn_params tf) next_pc
                  (fn_code tf))
    k (POSITION : (k <= (length args))%nat),
  exists trs2,
    star step tge (State ts tf (block2sp tsp) next_pc trs tm) E0
       (State ts tf (block2sp tsp) (Pos.of_nat(Pos.to_nat next_pc + k)%nat) trs2 tm) /\
      (forall reg (LOW: (reg < next_reg)%positive),
          trs2#reg = trs#reg) /\
      (forall k' (DONE: (k' < k)%nat),
          trs2#(Pos.of_nat (Pos.to_nat next_reg + k')%nat) =
            trs#(nth (length args - S k')%nat args 1%positive)).
Proof.
  induction k; intros.
  { exists trs. split.
    { replace (Pos.of_nat (Pos.to_nat next_pc + 0)) with next_pc by lia.
      apply star_refl. }
    split. { trivial. }
    intros. lia.
  }
  assert ((k <= Datatypes.length args)%nat) as ZZ by lia.
  destruct (IHk ZZ) as (trs1 & STAR1 & LOW1 & HIGH1).
  clear ZZ. eexists. split.
  { eapply star_right with (t2:=E0).
    exact STAR1. 2: reflexivity.
    eapply exec_Iop.
    destruct REC_CALL.
    rewrite TO_TEMPS.
    replace (Pos.to_nat next_pc + k + 1)%nat with
      (Pos.to_nat next_pc + S k)%nat by lia.
    reflexivity. lia. cbn. reflexivity.
  }
  split.
  { intros.
    rewrite Regmap.gso by lia.
    apply LOW1; auto.
  }
  intros.
  destruct (Nat.eq_dec k' k).
  { subst k'. clear DONE.
    rewrite Regmap.gss.
    assert ((nth (Datatypes.length args - S k)%nat args 1%positive) < next_reg)%positive as ZZ.
    { apply Forall_nth. assumption. lia. }
    apply LOW1. lia.
  }
  rewrite Regmap.gso by lia.
  apply HIGH1. lia.
Qed.

Fixpoint skip_first {X : Type} (n : nat) (l : list X) :=
  match n with
  | O => l
  | S n' => match l with
            | nil => nil
            | _::tail => skip_first n' tail
            end
  end.

Fixpoint assign_regs (vl : list val) (rl : list reg) rs0 {struct rl} : regset :=
  match rl with
  | nil => rs0
  | r1 :: rs =>
      match vl with
      | nil => rs0
      | v1 :: vs => (assign_regs vs rs rs0) # r1 <- v1
      end
  end.
  
Fixpoint reg_sequence (l : nat) (pos0 : reg) : list reg :=
  match l with
  | O => nil
  | S l' => pos0 :: (reg_sequence l' (Pos.succ pos0))
  end.

Remark reg_sequence_length: forall n pos0,
    length (reg_sequence n pos0) = n.
Proof.
  induction n. reflexivity.
  intro. cbn. rewrite IHn. reflexivity.
Qed.

Remark reg_sequence_nth:
  forall l pos0 k (LENGTH : (k < l)%nat) dummy,
    nth k (reg_sequence l pos0) dummy = (Pos.of_nat ((Pos.to_nat pos0) + k) : reg).
Proof.
  induction l; intros; cbn. lia.
  destruct k. lia. rewrite IHl by lia. lia.
Qed.

Lemma skip_first_length: forall {X : Type} (l : list X),
    (skip_first (length l) l) = nil.
Proof.
  induction l. reflexivity.
  cbn. assumption.
Qed.

Lemma skip_first_nth : forall {X : Type} (n : nat) (l : list X)
                        (k : nat) (default : X),
    (nth k (skip_first n l) default) = (nth (n+k)%nat l default).
Proof.
  induction n; intros. reflexivity.
  destruct l as [ | head tail]; cbn.
  { destruct k; reflexivity. }
  apply IHn.
Qed.

Lemma nth_extensionality:
  forall {X : Type} (l1 l2 : list X)
         (LENGTHS: length l1 = length l2)
         dummy1 dummy2
         (ALL: forall k, (k < length l1)%nat -> nth k l1 dummy1 = nth k l2 dummy2),
    l1 = l2.
Proof.
  induction l1; destruct l2; cbn in *; intros.
  reflexivity. lia. lia.
  f_equal.
  { pose proof (ALL O) as ZZ; cbn in ZZ. apply ZZ. lia. }
  apply IHl1 with (dummy1 := dummy1) (dummy2 := dummy2).
  lia.
  intros.
  pose proof (ALL (S k)) as ZZ; cbn in ZZ.
  apply ZZ. lia.
Qed.

Remark rev_reg_sequence_S: forall k next_reg,
    (rev (reg_sequence (S k) next_reg)) =
      (Pos.of_nat (Pos.to_nat next_reg + k)) ::
      (rev (reg_sequence k next_reg)).
Proof.
  intros.
  assert (LENGTHS: length (rev (reg_sequence (S k) next_reg)) =
    length ((Pos.of_nat (Pos.to_nat next_reg + k)) ::
         (rev (reg_sequence k next_reg)))).
  { cbn. rewrite app_length.
    rewrite rev_length. rewrite reg_sequence_length.
    rewrite rev_length. rewrite reg_sequence_length.
    cbn. lia. }
  apply (nth_extensionality _ _ LENGTHS 1%positive 1%positive).
  intros.
  rewrite rev_length in H. rewrite reg_sequence_length in H.
  rewrite rev_nth; cycle 1.
  { rewrite reg_sequence_length. assumption. }
  rewrite reg_sequence_length.
  replace (S k - S k0)%nat with (k - k0)%nat by lia.
  destruct k0; cbn.
  { rewrite Nat.sub_0_r.
    destruct k. lia.
    rewrite reg_sequence_nth by lia. lia.
  }
  assert (k0 < k)%nat by lia.
  destruct (k - S k0)%nat eqn:KK0.
  { rewrite rev_nth; cycle 1.
    { rewrite reg_sequence_length. assumption. }
    rewrite reg_sequence_nth; cycle 1.
    { rewrite reg_sequence_length. lia. }
    rewrite reg_sequence_length. lia. }
  rewrite reg_sequence_nth by lia.
  rewrite rev_nth; cycle 1.
  { rewrite reg_sequence_length. lia. }
  rewrite reg_sequence_nth; cycle 1.
  { rewrite reg_sequence_length. lia. }
  rewrite reg_sequence_length. lia.
Qed.

Remark skip_first_decompose: forall k (l : list reg)
    (LENGTH : (k < length l)%nat),
    (skip_first k l) = (nth k l 1%positive)::(skip_first (S k) l).
Proof.
  induction k; intros.
  { destruct l; cbn in *. lia. reflexivity. }
  cbn. destruct l as [ | head tail].
  { cbn in LENGTH. lia. }
  destruct tail as [ | head' tail' ].
  { cbn in LENGTH. lia. }
  rewrite IHk; cycle 1.
  { cbn in *. lia. }
  reflexivity.
Qed.

Lemma exec_jump2:
  forall tge args
  tf start next_reg next_pc ts trs tm tsp
  (BELOW: Forall (fun r => (r < next_reg)%positive) (fn_params tf))
  (REC_CALL : is_rec_call start next_reg
                  args (fn_params tf) next_pc
                  (fn_code tf))
  k (POSITION : (k <= length (fn_params tf))%nat),
  exists trs2,
    star step tge (State ts tf (block2sp tsp)
         (Pos.of_nat (Pos.to_nat next_pc + length args)%nat) trs tm) E0
         (State ts tf (block2sp tsp)
         (Pos.of_nat(Pos.to_nat next_pc + length args + k)%nat) trs2 tm) /\
      (forall reg (HIGH: (reg >= next_reg)%positive),
          trs2#reg = trs#reg) /\
      trs2 = assign_regs
               (trs ## (rev (reg_sequence k next_reg)))
               (skip_first (length (fn_params tf) - k) (fn_params tf)) trs.
Proof.
  induction k; intros.
  { exists trs. split.
    { rewrite Nat.add_0_r. apply star_refl. }
    split.
    { trivial. }
    rewrite Nat.sub_0_r. rewrite skip_first_length. reflexivity. }
  assert ((k <= length (fn_params tf))%nat) as ZZ by lia.
  destruct (IHk ZZ) as (trs1 & STAR1 & HIGH1 & RES1).
  eexists. split.
  { eapply star_right. exact STAR1. 2: reflexivity.
    eapply exec_Iop.
    { destruct REC_CALL.
      rewrite FROM_TEMPS.
      replace (Pos.to_nat next_pc + Datatypes.length args + k + 1)%nat with
        (Pos.to_nat next_pc + Datatypes.length args + S k)%nat by lia.
      reflexivity.
      change positive with reg in *. lia. }
    reflexivity. }
  split.
  { intro rg. intros. rewrite Regmap.gso.
    { apply HIGH1. assumption. }
    assert (nth (Datatypes.length (fn_params tf) - S k) (fn_params tf) 1%positive < next_reg)%positive as YY.
    { rewrite Forall_forall in BELOW.
      apply BELOW.
      apply nth_In. lia. }
    change positive with reg in *.
    lia. }
  rewrite RES1.
  rewrite RES1 in HIGH1.
  rewrite HIGH1 by lia.
  change ((assign_regs trs ## (rev (reg_sequence k next_reg))
     (skip_first (Datatypes.length (fn_params tf) - k) (fn_params tf)) trs)
  # (nth (length (fn_params tf) - S k) (fn_params tf) 1%positive) <-
            (trs # (Pos.of_nat (Pos.to_nat next_reg + k)))) with
    (assign_regs ((trs # (Pos.of_nat (Pos.to_nat next_reg + k))) ::
                     (trs ## (rev (reg_sequence k next_reg))))
        ((nth (length (fn_params tf) - S k) (fn_params tf) 1%positive) ::
           (skip_first (length (fn_params tf) - k) (fn_params tf))) trs).
  f_equal.
  { rewrite rev_reg_sequence_S. reflexivity. }
  rewrite (skip_first_decompose (Datatypes.length (fn_params tf) - S k)).
  { f_equal. f_equal. lia. }
  lia.
Qed.

Lemma exec_tail_rec_call:
  forall tge tf start next_reg next_pc args ts trs tm tsp
    (BELOW_ARGS: Forall (fun r => (r < next_reg)%positive) args)
    (BELOW_PARAMS: Forall (fun r => (r < next_reg)%positive) (fn_params tf))
    (LENGTHS : (List.length args) = (List.length (fn_params tf)))
    (REC_CALL : is_rec_call start next_reg
                  args (fn_params tf) next_pc
                  (fn_code tf)),
  exists trs1 trs2,
  plus step tge (State ts tf (block2sp tsp) next_pc trs tm) E0
       (State ts tf (block2sp tsp) start trs2 tm) /\
    trs2 = assign_regs (trs##args) (fn_params tf) trs1.
Proof.
  intros.
  destruct (exec_jump1 tge _ _ _ _ _ ts trs tm tsp BELOW_ARGS REC_CALL (length args) (Nat.le_refl (length args))) as (trs1 & STAR1 & PRES1 & SET1).
  exists trs1.
  destruct (exec_jump2 tge _ _ _ _ _ ts trs1 tm tsp BELOW_PARAMS REC_CALL (length (fn_params tf)) (Nat.le_refl (length (fn_params tf)))) as (trs2 & STAR2 & PRES2 & SET2).
  eexists. split.
  { eapply plus_right.
    { eapply star_trans.
      exact STAR1. exact STAR2. reflexivity. }
    apply exec_Inop.
    destruct REC_CALL.
    apply BACKJUMP. reflexivity. }
  rewrite SET2.
  rewrite Nat.sub_diag. cbn. f_equal.
  apply nth_extensionality with
    (dummy1:=trs1#(1%positive))
    (dummy2:=trs#(1%positive)).
  { rewrite map_length. rewrite map_length. rewrite rev_length.
    rewrite reg_sequence_length. congruence. }
  intros.
  rewrite map_length in H. rewrite rev_length in H.
  rewrite reg_sequence_length in H.
  change (trs1 # 1) with ((fun r => trs1#r) (1%positive)).
  rewrite map_nth.
  change (trs # 1) with ((fun r => trs#r) (1%positive)).
  rewrite map_nth.
  rewrite rev_nth; cycle 1.
  { rewrite reg_sequence_length. assumption. }
  rewrite reg_sequence_length.
  rewrite reg_sequence_nth by lia.
  rewrite <- LENGTHS in *.
  rewrite SET1 by lia.
  replace (length args - S (length args - S k))%nat with k; cycle 1.
  { change positive with reg in *. lia. }
  reflexivity.
Qed.

Definition match_fundef (prog : program) (f tf : fundef) :=
  exists cu id, linkorder cu prog /\
    (transf_fundef (Genv.globalenv cu) id f = OK tf).

Definition match_varinfo (v tv: unit) := True.

Definition match_prog (p tp: program) : Prop :=
  match_program_gen match_fundef match_varinfo p p tp.

Lemma transf_program_match:
  forall prog tprog
         (TRANS : transf_program prog = OK tprog), match_prog prog tprog.
Proof.
  unfold transf_program. intros.
  eapply match_transform_partial_program2.
  exact TRANS.
  2: intros; unfold match_varinfo; trivial; fail.
  unfold match_fundef. intros.
  exists prog. exists i. split.
  - apply linkorder_refl.
  - assumption.
Qed.

Section TAILREC.

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

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

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

Lemma function_ptr_translated:
  forall (b: block) (f: fundef)
    (FIND : Genv.find_funct_ptr ge b = Some f),
  exists cu f', linkorder cu prog /\ Genv.find_funct_ptr tge b = Some f' /\ match_fundef cu f f'.
Proof.
  intros.
  destruct (Genv.find_funct_ptr_match TRANSF _ FIND) as (cu & tf & TFIND & MATCH & LINK).
  unfold match_fundef in *.
  destruct MATCH as (cu' & id' & LINK' & TRANS').
  exists cu. exists tf. split. eassumption.
  split. exact TFIND.
  exists cu'. exists id'. split; eassumption.
Qed.

Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct ge v = Some f ->
  exists cu f', linkorder cu prog /\ Genv.find_funct tge v = Some f' /\ match_fundef cu f f'.
Proof.
  unfold Genv.find_funct. intros.
  destruct v; try discriminate.
  destruct Ptrofs.eq_dec. 2: discriminate.
  apply function_ptr_translated; auto.
Qed.

Lemma sig_function_translated:
  forall ge id f f', transf_function ge id f = OK f' -> fn_sig f' = fn_sig f.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv H. reflexivity.
Qed.

Lemma sig_fundef_translated:
  forall ge id f f', transf_fundef ge id f = OK f' -> funsig f' = funsig f.
Proof.
  unfold transf_fundef, transf_partial_fundef. intros.
  intros. destruct f; cycle 1; inv H.
  reflexivity.
  unfold transf_function in H1.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv H1. reflexivity.
Qed.

Lemma stacksize_function_translated:
  forall ge id f f', transf_function ge id f = OK f' -> fn_stacksize f' = fn_stacksize f.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv H. reflexivity.
Qed.

Lemma entrypoint_function_translated:
  forall ge id f f', transf_function ge id f = OK f' -> fn_entrypoint f' = fn_entrypoint f.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv H. reflexivity.
Qed.

Lemma params_function_translated:
  forall ge id f f', transf_function ge id f = OK f' -> fn_params f' = fn_params f.
Proof.
  unfold transf_function. intros.
  destruct option_eq_dec. 2: discriminate.
  destruct (successors_inside f). 2: discriminate.
  inv H. reflexivity.
Qed.

Inductive match_regs (fn : function) (IF : meminj) (rs rs' : regset) :=
  match_regs_intro
  (REG_INJECT : (forall r, (r <= RTL.max_reg_function fn)%positive ->
             Val.inject IF (rs#r) (rs'#r)))
  (REG_UNUSED : (forall r, (r > RTL.max_reg_function fn)%positive -> rs#r = Vundef)).

Lemma match_regs_incr: forall IF IF' (INCR : inject_incr IF IF') fn rs trs
                              (MATCH: match_regs fn IF rs trs),
    match_regs fn IF' rs trs.
Proof.
  intros.
  destruct MATCH. constructor; intros.
  - eapply val_inject_incr. eassumption. auto.
  - auto.
Qed.

Lemma match_copy: forall fn IF rs trs trs1
  (MATCH_REGS: match_regs fn IF rs trs)
  params args
  (BELOW_ARGS: Forall (fun r => (r <= max_reg_function fn)%positive) args)
  (BELOW_PARAMS: Forall (fun r => (r <= max_reg_function fn)%positive) params),
  (match_regs fn IF (init_regs (rs ## args) params)
              (assign_regs (trs ## args) params trs1)).
Proof.
  induction params; intros; cbn.
  - constructor; intros.
    + rewrite Regmap.gi. constructor.
    + apply Regmap.gi.
  - destruct args as [ | hargs targs]; cbn.
    { constructor.
      - intros. rewrite Regmap.gi. constructor.
      - intros. apply Regmap.gi. }
    destruct MATCH_REGS. inv BELOW_ARGS. inv BELOW_PARAMS.
    destruct (IHparams targs H2 H4) as [IND1 IND2].
    constructor; intros.
    + destruct (peq r a).
      * subst r. rewrite Regmap.gss. rewrite Regmap.gss.
        apply REG_INJECT. assumption.
      * rewrite Regmap.gso by congruence.
        rewrite Regmap.gso by congruence.
        apply IND1. assumption.
    + destruct (peq r a).
      * subst r. lia.
      * rewrite Regmap.gso by congruence.
        apply IND2. assumption.
Qed.

Definition match_sp (IF : meminj) sp tsp :=
  IF sp = Some (tsp, 0).

Definition find_function_symbol symb :=
  match Genv.find_symbol ge symb with
  | Some b => Genv.find_funct_ptr ge b
  | None => None
  end.

Record good_meminj (bound: block) (IF: meminj) : Prop :=
  mk_good_meminj {
    good_meminj_find_symbol: forall id b,
        Genv.find_symbol ge id = Some b -> Plt b bound;
    good_meminj_find_def: forall b def,
        Genv.find_def ge b = Some def -> Plt b bound;
    good_meminj_fixes: forall b, Plt b bound -> IF b = Some(b, 0%Z);
    good_meminj_nocollide: forall b b' delta,
        Ple bound b -> IF b = Some(b', delta) -> Ple bound b'
  }.

Lemma good_meminj_preserves_globals:
  forall bound IF (GOOD: good_meminj bound IF),
    (meminj_preserves_globals ge IF).
Proof.
  intros. destruct GOOD.
  constructor; intros.
  - eauto.
  - split; intros.
    + unfold Genv.find_var_info in H.
      destruct (Genv.find_def ge b) as [def | ] eqn:DEF.
      2: discriminate. eauto.
    + unfold Genv.find_var_info in H.
      destruct (Genv.find_def ge b2) as [def | ] eqn:DEF.
      2: discriminate.
      pose proof (good_meminj_find_def0 _ _ DEF) as LT.
      pose proof (good_meminj_fixes0 _ LT).
      assert ((Plt b1 bound) \/ (Ple bound b1)) as CASES by (unfold Plt, Ple; lia).
      destruct CASES as [CASE | CASE].
      * pose proof (good_meminj_fixes0 _ CASE). congruence.
      * pose proof (good_meminj_nocollide0 _ _ _ CASE H0).
        unfold Plt, Ple in *. lia.
Qed.

Inductive match_stackframes (bound : block) (IF : meminj) :
  stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
    forall cu return_reg id f tf sp tsp pc rs trs
           (LINK: linkorder cu prog)
           (BOUND_SP: Ple bound sp)
           (REG_OK : (return_reg <= max_reg_function f)%positive)
           (MATCH_FUNCTIONS : transf_function (Genv.globalenv cu) id f = OK tf)
           (MATCH_REGS : match_regs f IF rs trs)
           (MATCH_SP : match_sp IF sp tsp),
      match_stackframes bound IF
        (Stackframe return_reg f (block2sp sp) pc rs)
        (Stackframe return_reg tf (block2sp tsp) pc trs).

Lemma match_sp_incr:
  forall IF IF' (INCR : inject_incr IF IF') sp sp'
         (MATCH : match_sp IF sp sp'),
    match_sp IF' sp sp'.
Proof.
  unfold match_sp, inject_incr.
  intros.
  auto.
Qed.
           
Lemma match_stackframes_incr:
  forall bound IF IF' (INCR : inject_incr IF IF')
         (a b : stackframe) (MATCH : match_stackframes bound IF a b),
    match_stackframes bound IF' a b.
Proof.
  intros. inv MATCH.
  apply match_stackframes_intro with (cu:=cu) (id:=id); eauto using match_regs_incr, match_sp_incr.
Qed.

Lemma forall2_impl:
  forall {A B : Type} (P : A->B->Prop) (P': A->B->Prop)
         (impl : forall a b, P a b -> P' a b)
         (la : list A) (lb : list B)
         (ALL: List.Forall2 P la lb),
    List.Forall2 P' la lb.
Proof.
  induction la; cbn; intros; inv ALL; constructor; auto.
Qed.

Definition match_stacks bound IF s1 s2 := Forall2 (match_stackframes bound IF) s1 s2.

Lemma match_stacks_incr:
  forall bound IF IF' s ts
    (ALL_IF : match_stacks bound IF s ts)
      (INCR : inject_incr IF IF'),
    match_stacks bound IF' s ts.
Proof.
  unfold match_stacks.
  intros. apply forall2_impl with (P := match_stackframes bound IF).
  2: assumption.
  intros. apply match_stackframes_incr with (IF := IF); assumption.
Qed.

Definition weakly_allocated_block m b lo hi :=
  forall ofs p, (Mem.perm m b ofs Max p -> lo <=ofs <hi).

Lemma alloc_new_weakly_allocated_block:
  forall m lo hi m' b (ALLOC : Mem.alloc m lo hi = (m', b)),
    weakly_allocated_block m' b lo hi.
Proof.
  unfold weakly_allocated_block. intros.
  eapply Mem.perm_alloc_3; eauto.
Qed.

Lemma alloc_keep_weakly_allocated_block:
  forall m b lo hi m' lo' hi' b'
    (VALID: Plt b (Mem.nextblock m))
    (ALLOC : Mem.alloc m lo' hi' = (m', b'))
    (WEAKLY_ALLOCATED: weakly_allocated_block m b lo hi),
    weakly_allocated_block m' b lo hi.
Proof.
  unfold weakly_allocated_block.
  intros.
  eapply WEAKLY_ALLOCATED.
  eapply Mem.perm_alloc_4; eauto.
  rewrite (Mem.alloc_result _ _ _ _ _ ALLOC).
  unfold Plt in *. lia.
Qed.

Lemma free_weakly_allocated_block:
  forall m b lo hi b' lo' hi' m' (FREE : Mem.free m b' lo' hi' = Some m')
         (WEAKLY_ALLOCATED: weakly_allocated_block m b lo hi) (NEQ: b<>b'),
    weakly_allocated_block m' b lo hi.
Proof.
  unfold weakly_allocated_block. intros.
  eapply WEAKLY_ALLOCATED.
  eapply Mem.perm_free_3; eauto.
Qed.

Lemma store_weakly_allocated_block:
  forall m b lo hi (WEAKLY_ALLOCATED: weakly_allocated_block m b lo hi)
         chunk b' ofs' v' m' (STORE: Mem.store chunk m b' ofs' v' = Some m'),
    weakly_allocated_block m' b lo hi.
Proof.
  unfold weakly_allocated_block. intros.
  apply WEAKLY_ALLOCATED with (p:=p).
  eapply Mem.perm_store_2.
  exact STORE. assumption.
Qed.

Lemma storev_weakly_allocated_block:
  forall m b lo hi (WEAKLY_ALLOCATED: weakly_allocated_block m b lo hi)
         chunk ptr' v' m' (STORE: Mem.storev chunk m ptr' v' = Some m'),
    weakly_allocated_block m' b lo hi.
Proof.
  unfold Mem.storev. intros.
  destruct ptr'; try discriminate.
  eapply store_weakly_allocated_block; eassumption.
Qed.

Lemma external_call_weakly_allocated_block:
  forall m1 b lo hi (WEAKLY_ALLOCATED: weakly_allocated_block m1 b lo hi)
         ef ge vargs m2 t vres
         (EXTCALL: external_call ef ge vargs m1 t vres m2)
         (VALID: Mem.valid_block m1 b),
    (weakly_allocated_block m2 b lo hi).
Proof.
  intros. unfold weakly_allocated_block in *. intros.
  apply WEAKLY_ALLOCATED with (p:=p); auto.
  eapply external_call_max_perm; eauto.
Qed.

Inductive ubound_stack : block -> (list stackframe) -> Prop :=
| ubound_stack_nil: forall ub, ubound_stack ub nil
| ubound_stack_cons : forall ub return_reg f sp pc rs tail
  (UBOUND_H : Plt sp ub) (UBOUND_T : ubound_stack sp tail),
  ubound_stack ub
    ((Stackframe return_reg f (block2sp sp) pc rs) :: tail).

Lemma ubound_stack_advance: forall b1 b2 (LE: Ple b1 b2) s
  (UBOUND : ubound_stack b1 s), (ubound_stack b2 s).
Proof.
  induction s; intros. { constructor. }
  inv UBOUND. constructor.
  { unfold Ple, Plt in *. lia. }
  assumption.
Qed.

Inductive weakly_allocated_stackframe : mem -> stackframe -> Prop :=
  weakly_allocated_stackframe_intro:
    forall m return_reg f sp pc rs
           (WEAKLY_ALLOCATED_STACKFRAME: weakly_allocated_block m sp 0 (fn_stacksize f)),
      weakly_allocated_stackframe m
                                  (Stackframe return_reg f (block2sp sp) pc rs).

Definition weakly_allocated_stack m :=
  Forall (weakly_allocated_stackframe m).

Lemma store_weakly_allocated_stack:
  forall m s (WEAKLY_ALLOCATED: weakly_allocated_stack m s)
         chunk b' ofs' v' m' (STORE: Mem.store chunk m b' ofs' v' = Some m'),
    weakly_allocated_stack m' s.
Proof.
  induction s; intros; inv WEAKLY_ALLOCATED; constructor.
  - inv H1. constructor.
    eapply store_weakly_allocated_block; eassumption.
  - eapply IHs; eassumption.
Qed.

Lemma storev_weakly_allocated_stack:
  forall m s (WEAKLY_ALLOCATED: weakly_allocated_stack m s)
         chunk ptr' v' m' (STORE: Mem.storev chunk m ptr' v' = Some m'),
    weakly_allocated_stack m' s.
Proof.
  intros; destruct ptr'; try discriminate.
  eapply store_weakly_allocated_stack; eassumption.
Qed.

Lemma alloc_keep_weakly_allocated_stack:
  forall s m m' lo' hi' b'
    (UBOUND: ubound_stack (Mem.nextblock m) s)
    (ALLOC : Mem.alloc m lo' hi' = (m', b'))
    (WEAKLY_ALLOCATED: weakly_allocated_stack m s),
    weakly_allocated_stack m' s.
Proof.
  induction s; intros; inv WEAKLY_ALLOCATED; inv UBOUND; constructor.
  - inv H1. constructor.
    eapply alloc_keep_weakly_allocated_block; eauto.
  - eapply IHs.
    + eapply ubound_stack_advance with (b2:=Mem.nextblock m).
      2: eassumption.
      unfold Plt, Ple in *. lia.
    + eassumption.
    + eassumption.
Qed.

Definition not_in_stack b' :=
  Forall
    (fun sf => match sf with
               | (Stackframe _ _ (Vptr sp _) _ _) => sp <> b'
               | _ => True
               end).

Lemma ubound_not_in_stack: forall bound s
      (UBOUND: ubound_stack bound s), not_in_stack bound s.
Proof.
  induction s; intros; inv UBOUND; constructor.
  { unfold block2sp, Plt in *. lia. }
  apply IHs.
  apply ubound_stack_advance with (b1:=sp).
  { unfold Plt, Ple in *. lia. }
  assumption.
Qed.

Lemma free_weakly_allocated_stack:
  forall s m m' lo' hi' b'
    (NOT_IN: not_in_stack b' s)
    (ALLOC : Mem.free m b' lo' hi' = Some m')
    (WEAKLY_ALLOCATED: weakly_allocated_stack m s),
    weakly_allocated_stack m' s.
Proof.
  induction s; intros; inv WEAKLY_ALLOCATED; inv NOT_IN; constructor.
  - inv H1. constructor.
    eapply free_weakly_allocated_block; eauto.
  - eapply IHs; eauto.
Qed.

Lemma external_call_weakly_allocated_stack:
  forall m1 s (WEAKLY_ALLOCATED: weakly_allocated_stack m1 s)
         ef ge vargs m2 t vres
         (EXTCALL: external_call ef ge vargs m1 t vres m2)
         (VALID: ubound_stack (Mem.nextblock m1) s),
    (weakly_allocated_stack m2 s).
Proof.
  induction s; intros; inv VALID; inv WEAKLY_ALLOCATED; constructor.
  - inv H1. constructor.
    eapply external_call_weakly_allocated_block; eassumption.
  - eapply IHs. exact H2. eassumption.
    eapply ubound_stack_advance. 2: eassumption.
    unfold Ple, Plt in *. lia.
Qed.

Inductive match_states :
  RTL.state -> RTL.state -> Prop :=
  | match_states_intro:
    forall cu bound IF id s ts f tf sp tsp pc rs trs m tm
        (LINK: linkorder cu prog)
        (WEAKLY_ALLOCATED_FRAME: weakly_allocated_block m sp 0 (fn_stacksize f))
        (UBOUND_SP: Plt sp (Mem.nextblock m))
        (UBOUND_STACK: ubound_stack sp s)
        (WEAKLY_ALLOCATED_STACK: weakly_allocated_stack m s)
        (BOUND_SP: Ple bound sp)
        (NEXT_M: Ple bound (Mem.nextblock m))
        (NEXT_TM: Ple bound (Mem.nextblock tm))
        (GLOBALS : good_meminj bound IF)
        (MATCH_STACKS: match_stacks bound IF s ts)
        (MATCH_FUNCTIONS : transf_function (Genv.globalenv cu) id f = OK tf)
        (MATCH_REGS : match_regs f IF rs trs)
        (MATCH_SP : match_sp IF sp tsp)
        (MATCH_MEM : Mem.inject IF m tm),
      match_states (State s f (block2sp sp) pc rs m)
                   (State ts tf (block2sp tsp) pc trs tm)
  | match_states_call:
    forall cu bound IF id s ts f tf args targs m tm
        (LINK: linkorder cu prog)
        (UBOUND_STACK: ubound_stack (Mem.nextblock m) s)
        (WEAKLY_ALLOCATED_STACK: weakly_allocated_stack m s)
        (NEXT_M: Ple bound (Mem.nextblock m))
        (NEXT_TM: Ple bound (Mem.nextblock tm))
        (GLOBALS : good_meminj bound IF)
        (MATCH_STACKS: match_stacks bound IF s ts)
        (MATCH_FUNCTIONS : transf_fundef (Genv.globalenv cu) id f = OK tf)
        (MATCH_ARGS : Val.inject_list IF args targs)
        (MATCH_MEM : Mem.inject IF m tm),
        match_states (Callstate s f args m)
                     (Callstate ts tf targs tm)
  | match_states_return:
    forall bound IF s ts res tres m tm
        (UBOUND_STACK: ubound_stack (Mem.nextblock m) s)
        (WEAKLY_ALLOCATED_STACK: weakly_allocated_stack m s)
        (NEXT_M: Ple bound (Mem.nextblock m))
        (NEXT_TM: Ple bound (Mem.nextblock tm))
        (GLOBALS : good_meminj bound IF)
        (MATCH_STACKS: match_stacks bound IF s ts)
        (MATCH_RES : Val.inject IF res tres)
        (MATCH_MEM : Mem.inject IF m tm),
        match_states (Returnstate s res m)
                     (Returnstate ts tres tm)
  | match_states_tail_rec:
    forall cu bound IF id fd s ts f tf sp tsp pc rs trs m mfree tm sig args
        (LINK: linkorder cu prog)
        (WEAKLY_ALLOCATED_FRAME: weakly_allocated_block m sp 0 (fn_stacksize f))
        (UBOUND_SP: Plt sp (Mem.nextblock m))
        (UBOUND_STACK: ubound_stack sp s)
        (WEAKLY_ALLOCATED_STACK: weakly_allocated_stack m s)
        (BOUND_SP: Ple bound sp)
        (NEXT_M: Ple bound (Mem.nextblock m))
        (NEXT_TM: Ple bound (Mem.nextblock tm))
        (GLOBALS : good_meminj bound IF)
        (FIND: find_function_symbol id = Some fd)
        (MATCH_STACKS: match_stacks bound IF s ts)
        (MATCH_FUNCTIONS : transf_function (Genv.globalenv cu) id f = OK tf)
        (MATCH_REGS : match_regs f IF rs trs)
        (MATCH_SP : match_sp IF sp tsp)
        (MATCH_MEM : Mem.inject IF m tm)
        (FREE : Mem.free m sp 0 (fn_stacksize f) = Some mfree)
        (LENGTHS : List.length args = List.length (fn_params f))
        (ARGS_OK : (Forall (fun r : positive => (r <= (max_reg_function f)))%positive) args)
        (AT: (fn_code f)!pc = Some (Itailcall sig (inr id) args)),
    match_states (Callstate s (Internal f) rs ## args mfree)
                 (State ts tf (block2sp tsp) pc trs tm).

Lemma val_inject_refl: forall v,
    Val.inject (fun x => Some (x, 0)) v v.
Proof.
  destruct v; try constructor.
  econstructor. reflexivity. symmetry.
  apply Ptrofs.add_zero.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inv H.
  exploit function_ptr_translated; eauto.
  intros (cu & tf & cu_LINK & FIND & TR).
  exists (Callstate nil tf nil m0); split.
  { econstructor.
    { eapply (Genv.init_mem_match TRANSF); eauto. }
    { rewrite symbols_preserved.
      rewrite (match_program_main TRANSF).
      exact H1.
    }
    exact FIND.
    { rewrite <- H3.
      destruct TR as (cu' & id' & LINK' & TRANS').
      eapply sig_fundef_translated. eassumption.
    }
  }
  destruct TR as (cu' & id' & LINK' & TRANS').
  apply match_states_call with (cu := cu') (bound:= Mem.nextblock m0)
                               (IF:=Mem.flat_inj (Mem.nextblock m0)) (id:=id').
  - eapply linkorder_trans; eassumption.
  - constructor.
  - constructor.
  - unfold Ple. lia.
  - unfold Ple. lia.
  - constructor.
    + intros. eapply Genv.find_symbol_not_fresh; eassumption.
    + intros. eapply Genv.find_def_not_fresh; eassumption.
    + intros. unfold Mem.flat_inj.
      destruct plt. reflexivity.
      contradiction.
    + intros. unfold Mem.flat_inj in *.
      destruct plt in H4. 2: discriminate.
      unfold Ple, Plt in *. lia.
  - constructor.
  - assumption.
  - constructor.
  - eapply Genv.initmem_inject. eassumption.
Qed.

Lemma transf_final_states:
  forall st1 st2 r
         (MATCH : match_states st1 st2)
         (FINAL : final_state st1 r),
    final_state st2 r.
Proof.
  intros. inv FINAL. inv MATCH. inv MATCH_STACKS.
  inv MATCH_RES. constructor.
Qed.
                                                  
Definition measure (S: RTL.state) : nat :=
  match S with
  | State _ _ _ _ _ _ => 1%nat
  | Callstate _ _ _ _ | Returnstate _ _ _ => 0%nat
  end.

Lemma match_regs_args : forall args f IF rs trs
      (MATCH_REGS : match_regs f IF rs trs)
      (ARGS_OK : forall r, In r args -> (r <= (max_reg_function f))%positive),
    Val.inject_list IF (rs ## args) (trs ## args).
Proof.
  induction args; intros.
  constructor.
  simpl.
  constructor.
  { inv MATCH_REGS.
    apply REG_INJECT. apply ARGS_OK. left. reflexivity. }
  apply IHargs with (f := f). assumption.
  intros. apply ARGS_OK. right. assumption.
Qed.

Lemma match_regs_params:
  forall params f IF args args'
         (INJECT : Val.inject_list IF args args')
         (ALL : List.Forall (fun x => (x <= max_reg_function f)%positive) params),
         match_regs f IF (init_regs args params)
                    (init_regs args' params).
Proof.
  induction params; intros; cbn.
  { constructor.
    { intros. rewrite Regmap.gi. constructor. }
    intros. apply Regmap.gi.
  }
  destruct args.
  { constructor.
    { intros. rewrite Regmap.gi. constructor. }
    intros. apply Regmap.gi.
  }
  inv INJECT. inv ALL.
  destruct (IHparams f IF args vl' H3 H4) as (LOW & HIGH).
  constructor.
  { intros.
    destruct (peq a r).
    - subst a. rewrite Regmap.gss. rewrite Regmap.gss.
      assumption.
    - rewrite Regmap.gso by lia. rewrite Regmap.gso by lia.
      apply LOW; auto.
  }
  intros.
  destruct (peq a r). lia.
  rewrite Regmap.gso by lia.
  apply HIGH; auto.
Qed.
      
Lemma match_regs_assign :
  forall f IF rs trs res v tv
         (RES_OK : (res <= (max_reg_function f))%positive)
         (MATCH_REGS : match_regs f IF rs trs)
         (INJECT : Val.inject IF v tv),
    match_regs f IF (rs # res <- v) (trs # res <- tv).
Proof.
  intros. inv MATCH_REGS.
  constructor; intros.
  { destruct (peq r res).
    { subst r. rewrite Regmap.gss. rewrite Regmap.gss.
      assumption. }
    rewrite Regmap.gso by lia. rewrite Regmap.gso by lia.
    auto.
  }
  destruct (peq r res). lia.
  rewrite Regmap.gso by lia.
  auto.
Qed.

Lemma imply_forall2:
  forall {A B : Type}
          (P : A->B->Prop)
          (P' : A->B->Prop)
          (IMPL : forall a b, P a b -> P' a b)
         (la : list A) (lb : list B)
         (ALL : Forall2 P la lb), Forall2 P' la lb.
Proof.
  induction la; intros; inv ALL; constructor; auto.
Qed.

Lemma match_sp_inject:
  forall IF sp tsp (MATCH : match_sp IF sp tsp),
    (Val.inject IF (block2sp sp) (block2sp tsp)).
Proof.
  unfold match_sp, block2sp. intros.
  econstructor. eassumption. reflexivity.
Qed.
    
Lemma eval_builtin_arg_inject:
  forall bound IF arg varg rs trs m tm sp tsp
         (GLOBALS: good_meminj bound IF)
         (MATCH_REGS :
           List.Forall (fun r => Val.inject IF (rs#r) (trs#r))
                       (params_of_builtin_arg arg))
         (MATCH_MEM : Mem.inject IF m tm)
         (MATCH_SP : match_sp IF sp tsp)
    (EVAL : eval_builtin_arg tge (fun r : positive => rs # r)
                              (block2sp sp) m arg varg),
  exists tvarg,
  eval_builtin_arg tge (fun r : positive => trs # r)
                    (block2sp tsp) tm arg tvarg /\
    Val.inject IF varg tvarg.
Proof.
  induction arg; cbn; intros; inv EVAL.
  1,2,3,4,5: (inv MATCH_REGS; eexists; split ; [ constructor | trivial]; fail).
  - apply match_sp_inject in MATCH_SP.
    pose proof (Val.offset_ptr_inject IF (block2sp sp) (block2sp tsp) ofs MATCH_SP) as OFFSET.
    destruct (Mem.loadv_inject _ _ _ _ _ _ _ MATCH_MEM H2 OFFSET)
             as (v2 & LOAD2 & INJ2).
    eexists. split.
    + constructor. eassumption.
    + eassumption.
  - apply match_sp_inject in MATCH_SP.
    pose proof (Val.offset_ptr_inject IF (block2sp sp) (block2sp tsp) ofs MATCH_SP) as OFFSET.
    eexists. split. constructor. assumption.
  - destruct (good_meminj_preserves_globals _ _ GLOBALS) as (PRES1 & PRES2 & PRES3).
    unfold Senv.symbol_address in *.
    destruct (Senv.find_symbol tge id) eqn:FIND; cycle 1.
    { cbn in H3. discriminate. }
    destruct senv_preserved as (SENV1 & SENV2 & SENV3).
    rewrite SENV1 in FIND.
    pose proof (PRES1 _ _ FIND) as PRES.
      assert (Val.inject IF (Vptr b ofs) (Vptr b ofs)) as INJ.
    { econstructor. exact PRES.
      rewrite Ptrofs.add_zero. reflexivity. }
    destruct (Mem.loadv_inject _ _ _ _ _ _ _ MATCH_MEM H3 INJ) as (v2 & LD1 & LOD2).
    exists v2. split. 2: assumption.
    constructor. unfold Senv.symbol_address.
    rewrite SENV1. rewrite FIND. assumption.
  - destruct (good_meminj_preserves_globals _ _ GLOBALS) as (PRES1 & PRES2 & PRES3).
    eexists. split. { apply eval_BA_addrglobal. }
    unfold Senv.symbol_address.
    destruct (Senv.find_symbol tge id) eqn:FIND. 2: constructor.
    destruct senv_preserved as (SENV1 & SENV2 & SENV3).
    rewrite SENV1 in FIND.
    pose proof (PRES1 _ _ FIND) as PRES.
    econstructor. exact PRES.
    rewrite Ptrofs.add_zero. reflexivity.
  - apply Forall_app in MATCH_REGS.
    destruct MATCH_REGS as (MATCH_REGS1 & MATCH_REGS2).
    destruct (IHarg1 _ _ trs _ _ _ _ GLOBALS MATCH_REGS1 MATCH_MEM MATCH_SP H1) as (tv1 & X1 & Y1).
    destruct (IHarg2 _ _ trs _ _ _ _ GLOBALS MATCH_REGS2 MATCH_MEM MATCH_SP H3) as (tv2 & X2 & Y2).
    eexists. split.
    + constructor. eassumption. eassumption.
    + apply Val.longofwords_inject; assumption.
  - apply Forall_app in MATCH_REGS.
    destruct MATCH_REGS as (MATCH_REGS1 & MATCH_REGS2).
    destruct (IHarg1 _ _ trs _ _ _ _ GLOBALS MATCH_REGS1 MATCH_MEM MATCH_SP H1) as (tv1 & X1 & Y1).
    destruct (IHarg2 _ _ trs _ _ _ _ GLOBALS MATCH_REGS2 MATCH_MEM MATCH_SP H3) as (tv2 & X2 & Y2).
    eexists. split. constructor. eassumption. eassumption.
    destruct Archi.ptr64.
    + apply Val.addl_inject; assumption.
    + apply Val.add_inject; assumption.
Qed.

Lemma eval_builtin_args_inject:
  forall bound IF args vargs rs trs m tm sp tsp
         (GLOBALS: good_meminj bound IF)
         (MATCH_REGS :
           List.Forall (fun r => Val.inject IF (rs#r) (trs#r))
                       (params_of_builtin_args args))
         (MATCH_MEM : Mem.inject IF m tm)
         (MATCH_SP : match_sp IF sp tsp)
    (EVAL : eval_builtin_args tge (fun r : positive => rs # r)
                              (block2sp sp) m args vargs),
  exists tvargs,
  eval_builtin_args tge (fun r : positive => trs # r)
                    (block2sp tsp) tm args tvargs /\
    Val.inject_list IF vargs tvargs.
Proof.
  unfold eval_builtin_args.
  induction args; cbn; intros; inv EVAL.
  { exists nil. split. constructor. constructor. }
  apply Forall_app in MATCH_REGS.
  destruct MATCH_REGS as (MATCH_REGS_H & MATCH_REGS_T).
  destruct (eval_builtin_arg_inject _ _ _ _ _ _ _ _ _ _ GLOBALS MATCH_REGS_H MATCH_MEM MATCH_SP H1) as (th & XH & YH).
  destruct (IHargs _ _ _ _ _ _ _ GLOBALS MATCH_REGS_T MATCH_MEM MATCH_SP H3) as (tt & XT & YT).
  eexists. split.
  + constructor. exact XH. exact XT.
  + constructor; assumption.
Qed.

Lemma eval_assert_arg_inject:
  forall bound IF arg varg rs trs m tm sp tsp
         (GLOBALS: good_meminj bound IF)
         (MATCH_REGS :
           List.Forall (fun r => Val.inject IF (rs#r) (trs#r))
                       (params_of_assert_arg arg))
         (MATCH_MEM : Mem.inject IF m tm)
         (MATCH_SP : match_sp IF sp tsp)
    (EVAL : eval_assert_arg ge (block2sp sp) rs m arg varg),
  exists tvarg,
  eval_assert_arg tge (block2sp tsp) trs tm arg tvarg /\
    Val.inject IF varg tvarg.
Proof.
  induction arg; cbn; intros; inv EVAL.
  - do 2 esplit; [econstructor|].
    inv MATCH_REGS. eauto.
  - destruct (good_meminj_preserves_globals _ _ GLOBALS) as (PRES1 & PRES2 & PRES3).
    eapply eval_addressing_inject with (vl2:=trs##args) in EVAL0 as (?&?&?); eauto using good_meminj_preserves_globals.
    2:{ clear - MATCH_REGS. induction MATCH_REGS; constructor; auto. }
    eapply Mem.loadv_inject in LOAD as (?&?&?); eauto.
    do 2 esplit; eauto. econstructor; eauto.
    erewrite <-eval_addressing_preserved with (ge2:=tge) in H; eauto using symbols_preserved.
    rewrite eval_shift_stack_addressing in H. auto.
Qed.

Lemma eval_assert_args_inject:
  forall bound IF args vargs rs trs m tm sp tsp
         (GLOBALS: good_meminj bound IF)
         (MATCH_REGS :
           List.Forall (fun r => Val.inject IF (rs#r) (trs#r))
                       (params_of_assert_args args))
         (MATCH_MEM : Mem.inject IF m tm)
         (MATCH_SP : match_sp IF sp tsp)
    (EVAL : eval_assert_args ge (block2sp sp) rs m args vargs),
  exists tvargs,
  eval_assert_args tge (block2sp tsp) trs tm args tvargs /\
    Val.inject_list IF vargs tvargs.
Proof.
  unfold eval_assert_args.
  induction args; cbn; intros; inv EVAL.
  { exists nil. split. constructor. constructor. }
  apply Forall_app in MATCH_REGS.
  destruct MATCH_REGS as (MATCH_REGS_H & MATCH_REGS_T).
  destruct (eval_assert_arg_inject _ _ _ _ _ _ _ _ _ _ GLOBALS MATCH_REGS_H MATCH_MEM MATCH_SP H1) as (th & XH & YH).
  destruct (IHargs _ _ _ _ _ _ _ GLOBALS MATCH_REGS_T MATCH_MEM MATCH_SP H3) as (tt & XT & YT).
  eexists. split.
  + constructor. exact XH. exact XT.
  + constructor; assumption.
Qed.

Definition meminj_subst (IF: meminj) (b b' : block) :=
  fun x => if peq x b' then IF b else IF x.

Definition meminj_subst_incr: forall IF b b' (EMPTY: IF b' = None),
  inject_incr IF (meminj_subst IF b b').
Proof.
  unfold inject_incr, meminj_subst. intros.
  destruct (peq b0 b').
  congruence.
  assumption.
Qed.

Transparent Mem.alloc.

Lemma malloc_undef:
  forall m lo hi malloc next_block ofs
      (ALLOC : Mem.alloc m lo hi = (malloc, next_block)),
    (ZMap.get ofs (Mem.mem_contents malloc) # next_block) = Undef.
Proof.
  unfold Mem.alloc. intros. inv ALLOC. cbn.
  rewrite Regmap.gss.
  apply ZMap.gi.
Qed.

Lemma mem_alloc_contents_before:
  forall m lo hi malloc next_block b
         (ALLOC : Mem.alloc m lo hi = (malloc, next_block))
         (NEQ : b <> next_block),
    (Mem.mem_contents malloc) # b =
      (Mem.mem_contents m) # b.
Proof.
  unfold Mem.alloc. intros. inversion ALLOC. cbn.
  apply Regmap.gso. congruence.
Qed.

Opaque Mem.alloc.

Transparent Mem.free.

Lemma mem_free_contents_before:
  forall m lo hi mfree b b'
    (FREE : Mem.free m b lo hi = Some mfree),
    (Mem.mem_contents mfree) # b' = (Mem.mem_contents m) # b'.
Proof.
  intros. unfold Mem.free in FREE.
  destruct (Mem.range_perm_dec m b lo hi Cur Freeable).
  2: discriminate.
  inv FREE.
  reflexivity.
Qed.

Opaque Mem.free.

Lemma free_alloc_mem_inj:
  forall IF m tm b tb b' lo hi mfree malloc
  (BAD: IF b' = None)
  (BOUNDS': forall ofs k p, (lo <=ofs <hi -> Mem.perm m b ofs k p))
  (MEM_INJ : Mem.mem_inj IF m tm)
  (BLK_INJ: match_sp IF b tb)
  (FREE : Mem.free m b lo hi = Some mfree)
  (ALLOC : Mem.alloc mfree lo hi = (malloc, b')),
  Mem.mem_inj (meminj_subst IF b b') malloc tm.
Proof.
  intros. unfold meminj_subst. destruct MEM_INJ. constructor; intros.
  - destruct (peq b1 b').
    + subst b1.
      apply mi_perm with (b1 := b). assumption.
      apply BOUNDS'.
      eapply Mem.perm_alloc_3. exact ALLOC. exact H0.
    + apply mi_perm with (b1:=b1). assumption.
      eapply Mem.perm_free_3. exact FREE.
      eapply Mem.perm_alloc_4. exact ALLOC. all: auto.
  - destruct (peq b1 b').
    + subst b1.
      eapply mi_align with (ofs:=ofs) (p:=p). exact H.
      intros z zRANGE.
      apply BOUNDS'.
      eapply Mem.perm_alloc_3. exact ALLOC. exact (H0 z zRANGE).
    + eapply mi_align with (ofs:=ofs) (p:=p). exact H.
      intros z zRANGE.
      eapply Mem.perm_free_3. exact FREE.
      eapply Mem.perm_alloc_4. exact ALLOC.
      apply H0. all: auto.
  - destruct (peq b1 b').
    + subst b1. rewrite (malloc_undef _ _ _ _ _ _ ALLOC).
      constructor. (* undef in new block *)
    + rewrite (mem_alloc_contents_before _ _ _ _ _ _ ALLOC) by lia.
      rewrite (mem_free_contents_before _ _ _ _ _ _ FREE).
      pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ H0 n) as PERM_FREE.
      pose proof (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ PERM_FREE) as PERM.
      pose proof ( mi_memval _ _ _ _ H PERM) as INJECT.
      destruct (ZMap.get ofs (Mem.mem_contents m) # b1).
      all: inv INJECT; constructor.
      inv H2; try constructor.
      econstructor; cycle 1. reflexivity.
      destruct (peq b0 b'). 2: assumption.
      subst b0. congruence.
Qed.

Lemma free_alloc_no_overlap:
  forall IF m b b' lo hi mfree malloc
  (BAD: IF b' = None)
  (BOUNDS: forall ofs k p, (Mem.perm m b ofs k p -> lo <=ofs <hi))
  (BOUNDS': forall ofs k p, (lo <=ofs <hi -> Mem.perm m b ofs k p))
  (MEM_INJ : Mem.meminj_no_overlap IF m)
  (FREE : Mem.free m b lo hi = Some mfree)
  (ALLOC : Mem.alloc mfree lo hi = (malloc, b')),
  Mem.meminj_no_overlap (meminj_subst IF b b') malloc.
Proof.
  unfold Mem.meminj_no_overlap, meminj_subst. intros.
  destruct (peq b1 b') as [EQ1 | NEQ1].
  - subst b1.
    pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ H2) as RANGE1.
    pose proof (BOUNDS' _ Max Nonempty RANGE1) as PERM1.
    destruct (peq b2 b') as [EQ2 | NEQ2].
    + subst b2. contradiction.
    + pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ H3 NEQ2) as PERM_FREE2.
      pose proof (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ PERM_FREE2) as PERM2.
      destruct (peq b b2).
      * subst b2.
        exfalso.
        pose proof (BOUNDS _ _ _ PERM2) as RANGE2.
        exact (Mem.perm_free_2 _ _ _ _ _ FREE _ _ _ RANGE2 PERM_FREE2).
      * apply MEM_INJ with (b1:=b) (b2:=b2); trivial.
  - pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ H2 NEQ1) as PERM_FREE1.
    pose proof (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ PERM_FREE1) as PERM1.
    destruct (peq b2 b') as [EQ2 | NEQ2].
    + subst b2. clear H.
      pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ H3) as RANGE2.
      destruct (peq b b1).
      * subst b1.
        pose proof (BOUNDS _ _ _ PERM1) as RANGE1.
        exfalso.
        exact (Mem.perm_free_2 _ _ _ _ _ FREE _ _ _ RANGE1 PERM_FREE1).
      * apply MEM_INJ with (b1:=b1) (b2:=b); trivial.
        congruence.
        apply BOUNDS'. assumption.
    + pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ H3 NEQ2) as PERM_FREE2.
      pose proof (Mem.perm_free_3 _ _ _ _ _ FREE _ _ _ _ PERM_FREE2) as PERM2.
      apply MEM_INJ with (b1:=b1) (b2:=b2); trivial.
Qed.
      
Lemma free_alloc_inject:
  forall IF m tm b tb b' lo hi mfree malloc
  (BOUNDS: forall ofs k p, (Mem.perm m b ofs k p -> lo <=ofs <hi))
  (BOUNDS': forall ofs k p, (lo <=ofs <hi -> Mem.perm m b ofs k p))
  (MEM_INJ : Mem.inject IF m tm)
  (BLK_INJ: match_sp IF b tb)
  (FREE : Mem.free m b lo hi = Some mfree)
  (ALLOC : Mem.alloc mfree lo hi = (malloc, b')),
    Mem.inject (meminj_subst IF b b') malloc tm.
Proof.
  intros.
  pose proof (Mem.nextblock_free _ _ _ _ _ FREE) as BLK_FREE.
  pose proof (Mem.nextblock_alloc _ _ _ _ _ ALLOC) as BLK_ALLOC1.
  pose proof (Mem.alloc_result _ _ _ _ _ ALLOC) as BLK_ALLOC2.
  subst b'.
  intros. destruct MEM_INJ. constructor.
  - eapply free_alloc_mem_inj; try eassumption.
    apply mi_freeblocks. unfold Mem.valid_block. unfold Plt. lia.
  - unfold meminj_subst. intros.
    destruct (peq b0 (Mem.nextblock mfree)).
    { unfold Mem.valid_block, Plt in *. lia. }
    apply mi_freeblocks.
    unfold Mem.valid_block, Plt in *. lia.
  - unfold meminj_subst. intros.
    destruct (peq b0 (Mem.nextblock mfree)).
    { subst b0.
      eapply mi_mappedblocks. exact H. }
    eapply mi_mappedblocks. exact H.
  - eapply free_alloc_no_overlap; try eassumption.
    apply mi_freeblocks. unfold Mem.valid_block. unfold Plt. lia.
  - unfold meminj_subst. intros.
    destruct (peq b0 (Mem.nextblock mfree)).
    + subst b0.
      apply (mi_representable _ _ _ ofs H).
      destruct H0 as [PERM' | PERM'].
      * left.
        pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ PERM') as RANGE.
        pose proof (Mem.free_range_perm _ _ _ _ _ FREE) as RANGE_PERM.
        pose proof (RANGE_PERM _ RANGE) as PERM.
        apply Mem.perm_implies with (p1 := Freeable).
        2: apply perm_F_any.
        apply Mem.perm_cur.
        exact PERM.
      * right.
        pose proof (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ PERM') as RANGE.
        pose proof (Mem.free_range_perm _ _ _ _ _ FREE) as RANGE_PERM.
        pose proof (RANGE_PERM _ RANGE) as PERM.
        apply Mem.perm_implies with (p1 := Freeable).
        2: apply perm_F_any.
        apply Mem.perm_cur.
        exact PERM.
    + eapply mi_representable. exact H.
      destruct H0.
      * left. apply (Mem.perm_free_3 _ _ _ _ _ FREE).
        apply (Mem.perm_alloc_4 _ _ _ _ _ ALLOC); assumption.
      * right. apply (Mem.perm_free_3 _ _ _ _ _ FREE).
        apply (Mem.perm_alloc_4 _ _ _ _ _ ALLOC); assumption.
  - unfold meminj_subst. intros.
    destruct (peq b1 (Mem.nextblock mfree)).
    + assert ((lo <= ofs < hi) \/ ~(lo <= ofs < hi)) as CASES by lia.
      destruct CASES as [IN_RANGE | OUT_OF_RANGE].
      * left. apply Mem.perm_implies with (p1 := Freeable).
        2: apply perm_F_any.
        subst b1.
        apply (Mem.perm_alloc_2 _ _ _ _ _ ALLOC).
        assumption.
      * right. intro Z. apply OUT_OF_RANGE. subst b1.
        exact (Mem.perm_alloc_3 _ _ _ _ _ ALLOC _ _ _ Z).
    + destruct (mi_perm_inv _ _ _ _ _ _ H H0) as [PERM | NPERM].
      * destruct (peq b1 b).
        -- subst b1. right.
           intro ALLOC_PERM.
           pose proof (Mem.perm_alloc_4 _ _ _ _ _ ALLOC _ _ _ _ ALLOC_PERM n) as ALLOC_FREE.
           pose proof (BOUNDS ofs _ _ PERM) as RANGE.
           exact (Mem.perm_free_2 _ _ _ _ _ FREE _ _ _ RANGE ALLOC_FREE).
        -- left.
           eapply Mem.perm_alloc_1. exact ALLOC.
           eapply Mem.perm_free_1. exact FREE.
           { left. assumption. } assumption.
      * right. intro PERM. apply NPERM.
        apply (Mem.perm_free_3 _ _ _ _ _ FREE).
        apply (Mem.perm_alloc_4 _ _ _ _ _ ALLOC). 2: assumption.
        assumption.
Qed.

Lemma good_meminj_def_invariant:
  forall good IF (GOOD: good_meminj good IF) b de
         (FIND: Genv.find_def ge b = Some de),
    (IF b) = Some(b, 0%Z).
Proof.
  intros. destruct GOOD. eauto.
Qed.

Lemma find_function_injects:
  forall good IF (GOOD: good_meminj good IF)
         v tv (INJECT : Val.inject IF v tv)
         fd
         (FIND: Genv.find_funct ge v = Some fd)
         tfd
         (tFIND: Genv.find_funct tge v = Some tfd),
    (Genv.find_funct tge tv = Some tfd).
Proof.
  intros.
  destruct v; cbn in *; try discriminate.
  inv INJECT.
  destruct (Ptrofs.eq_dec i Ptrofs.zero). 2: discriminate. subst i.
  rewrite Ptrofs.add_zero_l. cbn.
  unfold Genv.find_funct_ptr in *.
  destruct (Genv.find_def ge b) eqn:FINDb. 2: discriminate.
  pose proof (good_meminj_def_invariant _ _ GOOD _ _ FINDb).
  replace delta with 0%Z by congruence.
  replace b2 with b by congruence.
  change (Ptrofs.repr 0) with Ptrofs.zero.
  destruct Ptrofs.eq_dec. 2: contradiction.
  exact tFIND.
Qed.

Lemma good_meminj_separated:
  forall bound IF IF' m tm
    (NEXT_TM: Ple bound (Mem.nextblock tm))
    (GOOD: good_meminj bound IF)
    (MATCH_MEM: Mem.inject IF m tm)
    (INCR: inject_incr IF IF')
    (SEPARATED: inject_separated IF IF' m tm),
    (good_meminj bound IF').
Proof.
  intros. destruct GOOD. constructor; intros.
  - eauto.
  - eauto.
  - pose proof (good_meminj_fixes0 _ H) as IFb.
    exact (INCR _ _ _ IFb).
  - destruct (IF b) as [[img_b delta_b] | ] eqn:IFb.
    + pose proof (INCR _ _ _ IFb).
      rewrite H0 in H1. inv H1.
      exact (good_meminj_nocollide0 _ _ _ H IFb).
    + unfold inject_separated in *.
      destruct (SEPARATED _ _ _ IFb H0) as [INVALID INVALID'].
      unfold Mem.valid_block, Plt, Ple in *.
      lia.
Qed.


Remark storev_nextblock:
  forall chunk tm tm2 ta trs,
  (Mem.storev chunk tm ta trs) = Some tm2 ->
  Mem.nextblock tm2 = Mem.nextblock tm.
Proof.
  intros. unfold Mem.storev in H.
  destruct ta; try discriminate.
  eapply Mem.nextblock_store. eassumption.
Qed.

Remark good_meminj_alloc:
  forall bound m tm stk stk'
    (IF IF' : meminj)
    (NEXT_M : Ple bound (Mem.nextblock m))
    (NEXT_TM : Ple bound (Mem.nextblock tm))
    (GLOBALS : good_meminj bound IF)
    (INJECT_INCR : inject_incr IF IF')
    (STK' : IF' stk = Some (stk', 0))
    (BLOCKS : forall b : block, b <> stk -> IF' b = IF b)
    (NSTK : stk = Mem.nextblock m)
    (NSTK' : stk' = Mem.nextblock tm),
    good_meminj bound IF'.
Proof.
  intros. destruct GLOBALS. constructor.
  - eauto.
  - eauto.
  - intros. unfold Plt, Ple in *.
    destruct (peq b stk) as [EQ | NEQ]. lia. rewrite BLOCKS by assumption.
    apply good_meminj_fixes0; assumption.
  - intros. destruct (peq b stk).
    + subst b. rewrite STK' in H0. inv H0. assumption.
    + rewrite BLOCKS in H0 by assumption.
      eapply good_meminj_nocollide0. exact H. exact H0.
Qed.

Remark good_meminj_subst:
  forall bound IF sp stk
  (SP: Ple bound sp)
  (STK : Ple bound stk)
  (GOOD : good_meminj bound IF),
    good_meminj bound (meminj_subst IF sp stk).
Proof.
  intros. destruct GOOD. constructor.
  - eauto.
  - eauto.
  - intros. unfold meminj_subst.
    destruct (peq b stk).
    + unfold Plt, Ple in *. lia.
    + auto.
  - intros. unfold meminj_subst in H0.
    destruct (peq b stk).
    + subst b.
      exact (good_meminj_nocollide0 sp _ _ SP H0).
    + exact (good_meminj_nocollide0 b _ _ H H0).
Qed.

Theorem step_simulation:
  forall S1 t S2,
  step ge S1 t S2 ->
  forall S1' (MS: match_states S1 S1'),
  (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
Proof.
  intros. inv H; inv MS.
  (* Inop *)
  - left. eexists. split.
    + apply plus_one. apply exec_Inop; trivial.
      erewrite transf_function_preserves with (id := id) (f := f).
      1,3: eassumption.
      rewrite H0; trivial.
    + econstructor; eauto.

  (* Iop *)
  - left.
    assert (Val.inject_list IF rs ## args trs ## args) as INJECT.
    { apply match_regs_args with (f := f).
      assumption. intros.
      eapply max_reg_function_use. eassumption.
      assumption. }
    inv MATCH_SP.
    destruct (eval_operation_inject (good_meminj_preserves_globals _ _ GLOBALS) sp0 H2 op INJECT MATCH_MEM H1)
      as (tv & EVAL & INJ).
    rewrite eval_shift_stack_operation in EVAL.
    fold (block2sp tsp) in EVAL.
    eexists. split.
    + apply plus_one.
      apply exec_Iop with (op := op) (args := args) (v := tv).
      { erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         { rewrite H0; trivial. }
      }
      rewrite eval_operation_preserved with (ge1 := ge).
      exact EVAL.
      apply symbols_preserved.
    + apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
      apply match_regs_assign; trivial.
      eapply max_reg_function_def with (pc := pc).
      eassumption. reflexivity.
 
  (* Iload *)
  - left.
    assert (Val.inject_list IF rs ## args trs ## args) as INJECT.
    { apply match_regs_args with (f := f).
      assumption. intros.
      eapply max_reg_function_use. eassumption.
      assumption. }
    inv MATCH_SP.
    inv H1.
    + destruct (eval_addressing_inject (good_meminj_preserves_globals _ _ GLOBALS) sp0 H2 addr INJECT EVAL)
        as (tv & ADDR & INJ).
      rewrite eval_shift_stack_addressing in ADDR.
      fold (block2sp tsp) in ADDR.
      rename tv into ta.
      destruct (Mem.loadv_inject IF m tm chunk _ _ _ MATCH_MEM LOAD INJ)
        as (tv & TLOAD & INJV).
      eexists. split.
      * apply plus_one.
        apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args).
        { erewrite transf_function_preserves with (id := id) (f := f).
           1,3: eassumption.
           rewrite H0; trivial.
        }
        eapply has_loaded_normal.
        { rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved.
          exact ADDR. }
        exact TLOAD.
      * apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
        apply match_regs_assign; trivial.
        eapply max_reg_function_def with (pc := pc).
        eassumption. reflexivity.
    + destruct (eval_addressing tge (block2sp tsp) addr trs ## args) as [ta | ] eqn:TEVAL.
      * destruct (eval_addressing ge (block2sp sp0) addr rs ## args) as [a | ] eqn:EVAL.
        -- destruct (eval_addressing_inject (good_meminj_preserves_globals _ _ GLOBALS) sp0 H2 addr INJECT EVAL)
             as (tv & ADDR & INJ).
           rewrite eval_shift_stack_addressing in ADDR.
           fold (block2sp tsp) in ADDR.
           rename tv into ta2.
           rewrite eval_addressing_preserved with (ge1 := ge) in TEVAL by apply symbols_preserved.
           replace ta2 with ta in INJ by congruence.
           clear ADDR ta2.
           assert (Mem.loadv chunk m a = None) as LOAD_NONE by auto.
           clear LOAD.
           destruct (Mem.loadv chunk tm ta) as [ tv | ] eqn:LOAD'.
           ++ exists (State ts tf (block2sp tsp) pc' trs # dst <- tv tm).
              split.
              ** apply plus_one.
                 apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
                 { erewrite transf_function_preserves with (id := id) (f := f).
                    1,3: eassumption.
                    { rewrite H0; trivial. }
                 }
                 eapply has_loaded_normal.
                 { rewrite <- eval_addressing_preserved with (ge2 := tge) in TEVAL by apply symbols_preserved.
                   exact TEVAL. }
                 exact LOAD'.
              ** apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
                 apply match_regs_assign; trivial.
                 eapply max_reg_function_def with (pc := pc).
                 eassumption. reflexivity.
           ++ exists (State ts tf (block2sp tsp) pc' trs # dst <- Vundef tm).
              split.
              ** apply plus_one.
                 apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
                 { erewrite transf_function_preserves with (id := id) (f := f).
                    1,3: eassumption.
                    { rewrite H0; trivial. }
                 }
                 apply has_loaded_default. 2: reflexivity.
                 intros ta' TEVAL'.
                 rewrite eval_addressing_preserved with (ge1 := ge) in TEVAL' by apply symbols_preserved.
                 replace ta' with ta by congruence.
                 assumption.
              ** apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
                 apply match_regs_assign; trivial.
                 eapply max_reg_function_def with (pc := pc).
                 eassumption. reflexivity.
        -- destruct (Mem.loadv chunk tm ta) as [ tv | ] eqn:LOAD'.
           ++ exists (State ts tf (block2sp tsp) pc' trs # dst <- tv tm).
              split.
              ** apply plus_one.
                 apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
                 { erewrite transf_function_preserves with (id := id) (f := f).
                    1,3: eassumption.
                    { rewrite H0; trivial. }
                 }
                 apply has_loaded_normal with (a:=ta); trivial.
              ** apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
                 apply match_regs_assign; trivial.
                 eapply max_reg_function_def with (pc := pc).
                 eassumption. reflexivity.
           ++ exists (State ts tf (block2sp tsp) pc' trs # dst <- Vundef tm).
              split.
              ** apply plus_one.
                 apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
                 { erewrite transf_function_preserves with (id := id) (f := f).
                    1,3: eassumption.
                    { rewrite H0; trivial. }
                 }
                 apply has_loaded_default.
                 intros ta' TEVAL'.
                 replace ta' with ta by congruence.
                 assumption. reflexivity.
              ** apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
                 apply match_regs_assign; trivial.
                 eapply max_reg_function_def with (pc := pc).
                 eassumption. reflexivity.
      * exists (State ts tf (block2sp tsp) pc' trs # dst <- Vundef tm).
        split.
        ** apply plus_one.
           apply exec_Iload with (trap:=NOTRAP) (chunk:=chunk) (addr:=addr) (args:=args).
           { erewrite transf_function_preserves with (id := id) (f := f).
              1,3: eassumption.
              rewrite H0; trivial.
           }
           apply has_loaded_default.
           intros ta TADDR.
           congruence. reflexivity.
        ** apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
           apply match_regs_assign; trivial.
           eapply max_reg_function_def with (pc := pc). eassumption. reflexivity.
  (* Istore *)
  - left.
    assert (Val.inject_list IF rs ## args trs ## args) as INJECT.
    { apply match_regs_args with (f := f).
      assumption. intros.
      eapply max_reg_function_use. eassumption.
      right.
      assumption. }
    inv MATCH_SP.
    destruct (eval_addressing_inject (good_meminj_preserves_globals _ _ GLOBALS) sp0 H3 addr INJECT H1)
      as (tv & ADDR & INJ).
    rewrite eval_shift_stack_addressing in ADDR.
    fold (block2sp tsp) in ADDR.
    rename tv into ta.
    assert (Val.inject IF rs#src trs#src) as INJECT_SRC.
    { inv MATCH_REGS.
      apply REG_INJECT.
      eapply max_reg_function_use. eassumption. constructor. reflexivity. }
    destruct (Mem.storev_mapped_inject IF _ _ _ _ _ tm _ _ MATCH_MEM H2 INJ INJECT_SRC) as (m2' & STORE & INJm2').
    eexists. split.
    + apply plus_one.
      apply exec_Istore with (chunk:=chunk) (addr:=addr) (args := args) (src := src) (a := ta).
      * erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         rewrite H0; trivial.
      * rewrite eval_addressing_preserved with (ge1 := ge) by apply symbols_preserved.
         exact ADDR.
      * exact STORE.
    + apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); trivial.
      * eapply storev_weakly_allocated_block; eassumption.
      * pose proof (storev_nextblock _ _ _ _ _ H2).
        unfold Plt in *. lia.
      * eapply storev_weakly_allocated_stack; eassumption.
      * pose proof (storev_nextblock _ _ _ _ _ H2).
        unfold Ple in *. lia.
      * pose proof (storev_nextblock _ _ _ _ _ STORE).
        unfold Ple in *. lia.
  (* Icall *)
  - destruct ros as [reg | symbol].
    + left. cbn in H1.
      destruct (functions_translated _ _ H1) as (tcu & tfd & tcu_LINK & FIND_FD & MATCH_FD).
      destruct MATCH_FD as (cu' & id' & LINK' & TRANS').
      eexists. split.
      * apply plus_one. eapply exec_Icall with (ros := inl reg).
        { erewrite transf_function_preserves with (id := id) (f := f).
           1,3: eassumption.
           { rewrite H0; trivial. }
        }
        { eapply find_function_injects. eassumption.
          { destruct MATCH_REGS. apply REG_INJECT.
            eapply max_reg_function_use. eassumption.
            cbn. left. reflexivity. }
          eassumption. eassumption.
        }
        eapply sig_fundef_translated. eassumption.
      * eapply match_states_call with (cu:=cu') (bound:=bound) (IF:=IF) (id:=id'); trivial.
        -- eapply linkorder_trans; eassumption.
        -- constructor; trivial.
        -- constructor. 2: assumption. constructor. assumption.
        -- constructor. 2: assumption.
           apply match_stackframes_intro with (id:=id) (cu:=cu); trivial.
           { eapply max_reg_function_def. eassumption. reflexivity. }
        -- eapply match_regs_args. eassumption.
           intros. eapply max_reg_function_use. eassumption.
           right. assumption.
    + left. simpl in H1.
      destruct (Genv.find_symbol ge symbol) eqn:FIND. 2: discriminate.
      destruct (function_ptr_translated b _ H1) as (tcu' & tcu'_LINK & f' & FIND' & MATCH').
      eexists. split.
      * apply plus_one. eapply exec_Icall with (ros := inr symbol).
        { erewrite transf_function_preserves with (id := id) (f := f).
           1,3: eassumption.
           { rewrite H0; trivial. }
        }
        { simpl.
          rewrite symbols_preserved. rewrite FIND.
          exact FIND'.
        }
        destruct MATCH' as (cu' & id' & LINK' & TRANS').
        exact (sig_fundef_translated _ _ _ _ TRANS').
      * destruct MATCH' as (cu' & id' & LINK' & TRANS').
        apply match_states_call with (cu:=cu') (id:=id') (bound:=bound) (IF:=IF); trivial.
        -- eapply linkorder_trans; eassumption.
        -- constructor; trivial.
        -- constructor. 2: assumption. constructor. assumption.
        -- constructor. 2: assumption.
           apply match_stackframes_intro with (id:=id) (cu:=cu); trivial.
           { eapply max_reg_function_def. eassumption. reflexivity. }
        -- eapply match_regs_args. eassumption.
           intros. eapply max_reg_function_use. eassumption.
           exact H.
  (* Itailcall *)
  - destruct ros as [reg | symbol].
    + left. cbn in H1.
      destruct (functions_translated _ _ H1) as (tcu & tcu_LINK & tfd & FIND_FD & MATCH_FD).
      destruct (Mem.free_parallel_inject IF m tm _ _ _ _ _ _ MATCH_MEM H3 MATCH_SP) as (tm' & FREE & MATCH_MEM').
      change (0 + 0) with 0 in FREE.
      rewrite Z.add_0_r in FREE.
      destruct MATCH_FD as (cu' & id' & LINK' & TRANS').
      eexists. split.
      * apply plus_one. eapply exec_Itailcall with (ros := inl reg).
        -- erewrite transf_function_preserves with (id := id) (f := f).
           1,3: eassumption.
           rewrite H0; trivial.
        -- eapply find_function_injects. eassumption.
           { destruct MATCH_REGS. apply REG_INJECT.
            eapply max_reg_function_use. eassumption.
            cbn. left. reflexivity. }
           eassumption. eassumption.
        -- eapply sig_fundef_translated. eassumption.
        -- erewrite stacksize_function_translated with (id:=id) (f:=f) by eassumption.
           exact FREE.
      * apply match_states_call with (cu:=cu') (bound:=bound) (IF:=IF) (id:=id'); trivial.
        -- eapply linkorder_trans; eassumption.
        -- rewrite (Mem.nextblock_free _ _ _ _ _ H3).
           eapply ubound_stack_advance. 2: eassumption.
           unfold Ple, Plt in *. lia.
        -- eapply free_weakly_allocated_stack.
           ++ apply ubound_not_in_stack. eassumption.
           ++ eassumption.
           ++ eassumption.
        -- pose proof (Mem.nextblock_free _ _ _ _ _ H3).
           unfold Ple in *. lia.
        -- pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
           unfold Ple in *. lia.
        -- eapply match_regs_args. eassumption.
           intros. eapply max_reg_function_use. eassumption. right.
           eassumption.
        
    + destruct ((QualIdent.eq id symbol) &&
                  (Nat.eq_dec (List.length args) (List.length (fn_params f)))) eqn:ACTIVATE.
      * (* That's where we jump to the head *)
        right. split.
        { cbn. lia. }
        split. reflexivity.
        destruct (QualIdent.eq id symbol). 2: discriminate.
        subst symbol.
        destruct (Nat.eq_dec (Datatypes.length args)
                             (Datatypes.length (fn_params f))) as [LENGTHS | ].
        2: discriminate.
        clear ACTIVATE.
        assert (fd = Internal f) as FD.
        {
          unfold find_function in *.
          destruct Genv.find_symbol eqn:SYMBOL. 2: discriminate.
          unfold Genv.find_funct_ptr in *.
          destruct (Genv.find_def ge b) eqn:FIND_DEF. 2: discriminate.
          assert ((prog_defmap prog)!.id = Some g) as DEFMAP.
          { apply Genv.find_def_symbol.
            exists b; auto. }
          destruct g. 2: discriminate. inv H1.
          unfold transf_function in *.
          destruct option_eq_dec as [EQ2 | ]. 2: discriminate.
          clear MATCH_FUNCTIONS.
          unfold find_function in *.
          destruct (Genv.find_symbol (Genv.globalenv cu) id) as [b2 | ] eqn:SYMBOL2. 2: discriminate.
          unfold Genv.find_funct_ptr in *.
          destruct (Genv.find_def (Genv.globalenv cu) b2) eqn:FIND_DEF2. 2: discriminate.
          assert ((prog_defmap cu)!.id = Some g) as DEFMAP2.
          { apply Genv.find_def_symbol.
            exists b2; auto. }
          destruct g. 2: discriminate. inv EQ2.
          destruct (prog_defmap_linkorder _ _ _ _ LINK DEFMAP2) as (gd3 & DEFMAP3 & LINK3).
          rewrite DEFMAP in DEFMAP3. inv DEFMAP3.
          inv LINK3. inv H2. reflexivity.
        }
        rewrite FD.
        eapply match_states_tail_rec with (sp:=stk) (m:=m); try eassumption.
        apply Forall_forall. intros.
        assert (x <= (max_reg_function f))%positive.
        { eapply max_reg_function_use.
          eassumption. cbn. assumption. }
        lia.
      * left. simpl in H1.
        destruct (Genv.find_symbol ge symbol) eqn:FIND. 2: discriminate.
        destruct (function_ptr_translated b _ H1) as (tcu' & tcu'_LINK & f' & FIND' & MATCH').
        destruct (Mem.free_parallel_inject IF m tm _ _ _ _ _ _ MATCH_MEM H3 MATCH_SP) as (tm' & FREE & MATCH_MEM').
        change (0 + 0) with 0 in FREE.
        rewrite Z.add_0_r in FREE.
        eexists. split.
        -- apply plus_one. eapply exec_Itailcall.
           ++ erewrite transf_function_preserves with (id := id) (f := f).
               1,3: eassumption.
               rewrite H0.
               rewrite ACTIVATE.
              trivial.
           ++ simpl.
              rewrite symbols_preserved. rewrite FIND.
              exact FIND'.
           ++ destruct MATCH' as (cu' & id' & LINK' & TRANS').
              exact (sig_fundef_translated _ _ _ _ TRANS').
           ++ erewrite stacksize_function_translated with (id:=id) (f:=f) by eassumption.
              exact FREE.
        -- destruct MATCH' as (cu' & id' & LINK' & TRANS').
           apply match_states_call with (cu:=cu') (bound:=bound) (IF:=IF) (id:=id'); trivial.
           ++ eapply linkorder_trans; eassumption.
           ++ eapply ubound_stack_advance. 2: eassumption.
              pose proof (Mem.nextblock_free _ _ _ _ _ H3).
              unfold Ple, Plt in *. lia.
           ++ eapply free_weakly_allocated_stack.
              ** apply ubound_not_in_stack. eassumption.
              ** eassumption.
              ** eassumption.
           ++ pose proof (Mem.nextblock_free _ _ _ _ _ H3).
              unfold Ple in *. lia.
           ++ pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
              unfold Ple in *. lia.
           ++ eapply match_regs_args. eassumption.
              intros. eapply max_reg_function_use. eassumption.
              assumption.
  (* Ibuiltin *)
  - left.
    assert (Forall (fun r : positive => Val.inject IF rs # r trs # r)
                   (params_of_builtin_args args)) as INJ_ARGS.
    { apply Forall_forall. intros r IN.
      inv MATCH_REGS.
      apply REG_INJECT.
      eapply max_reg_function_use.
      exact H0. exact IN.
    }
    pose proof (eval_builtin_args_preserved _ symbols_preserved H1) as ARGS.
    destruct (eval_builtin_args_inject bound IF args vargs rs trs m tm sp0 tsp GLOBALS INJ_ARGS MATCH_MEM MATCH_SP ARGS) as (tvargs & EVAL' & INJ').
    destruct (external_call_mem_inject _ _ _ _ (good_meminj_preserves_globals _ _ GLOBALS) H2 MATCH_MEM INJ') as
      (IF' & vres' & m2' & CALL' & RES_INJ & MEM_INJ & UNCHANGED1 & UNCHANGED2 & INCR & SEPARATED).
    eexists. split.
    + apply plus_one.
      eapply exec_Ibuiltin with (ef:=ef) (args:=args) (res:=res).
      { erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         { rewrite H0; trivial. }
      }
      exact EVAL'.
      apply external_call_symbols_preserved with (ge1 := ge).
      { apply senv_preserved. }
      exact CALL'.
    + apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF') (id:=id); trivial.
      * eapply external_call_weakly_allocated_block; eassumption.
      * pose proof (external_call_nextblock _ _ _ _ _ _ _ H2).
        unfold Plt, Ple in *. lia.
      * eapply external_call_weakly_allocated_stack; try eassumption.
        eapply ubound_stack_advance. 2: eassumption.
        unfold Plt, Ple in *. lia.
      * pose proof (external_call_nextblock _ _ _ _ _ _ _ H2).
        unfold Plt, Ple in *. lia.
      * pose proof (external_call_nextblock _ _ _ _ _ _ _ CALL').
        unfold Plt, Ple in *. lia.
      * apply good_meminj_separated with (IF:=IF) (m:=m) (tm:=tm); trivial.
      * apply match_stacks_incr with (IF := IF); trivial.
      * destruct res eqn:RES; cbn; trivial.
        apply match_regs_assign; trivial.
        pose proof (max_reg_function_def _ _ _ x H0) as ZZ.
        apply ZZ. reflexivity.
        all: apply match_regs_incr with (IF:=IF); trivial.
      * apply match_sp_incr with (IF:=IF); assumption.
  (* Icond *)
  - left.
    assert (Val.inject_list IF rs ## args trs ## args) as INJECT.
    { apply match_regs_args with (f := f).
      assumption. intros.
      eapply max_reg_function_use. eassumption.
      assumption. }
    inv MATCH_SP.
    pose proof (eval_condition_inject cond INJECT MATCH_MEM H1) as EVAL.
    eexists. split.
    + apply plus_one.
      apply exec_Icond with (cond:=cond) (args:=args)
                            (ifso:=ifso) (ifnot:=ifnot) (b:=b) (predb := predb).
      { erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         rewrite H0; trivial.
      }
      assumption. reflexivity.
    + apply match_states_intro with (cu:=cu) (bound:=bound) (IF := IF) (id := id); trivial.
  (* Ijumptable *)
  - left.
    assert (Val.inject IF rs#arg trs#arg) as INJECT.
    { inv MATCH_REGS.
      apply REG_INJECT.
      eapply max_reg_function_use. eassumption. constructor. reflexivity. }
    eexists. split.
    + apply plus_one. apply exec_Ijumptable with (arg:=arg) (tbl:=tbl) (n:=n).
      { erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         rewrite H0; trivial.
      }
      rewrite H1 in INJECT. inv INJECT.
      reflexivity.
      exact H2.
    + apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF) (id:=id); auto.
  (* Ireturn *)
  - left.
    destruct (Mem.free_parallel_inject IF m tm _ _ _ _ _ _ MATCH_MEM H1 MATCH_SP) as (tm' & FREE & MATCH_MEM').
    rewrite Z.add_0_r in FREE.
    rewrite Z.add_0_r in FREE.
    eexists. split.
    + apply plus_one. apply exec_Ireturn.
      { erewrite transf_function_preserves with (id := id) (f := f).
         1,3: eassumption.
         rewrite H0; trivial.
      }
      erewrite stacksize_function_translated with (id := id) (f := f) by eassumption.
      exact FREE.
    + apply match_states_return with (bound:=bound) (IF:=IF); auto.
      * eapply ubound_stack_advance. 2: eassumption.
        rewrite (Mem.nextblock_free _ _ _ _ _ H1).
        unfold Ple, Plt in *. lia.
      * eapply free_weakly_allocated_stack.
        -- apply ubound_not_in_stack. eassumption.
        -- eassumption.
        -- eassumption.
      * pose proof (Mem.nextblock_free _ _ _ _ _ H1).
        unfold Ple in *. lia.
      * pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
        unfold Ple in *. lia.
      * destruct or; cbn. 2: constructor.
        inv MATCH_REGS. apply REG_INJECT.
        eapply max_reg_function_use. eassumption. constructor. reflexivity.
  (* Iassert *)
  - left.
    eapply eval_assert_args_inject in H1 as (?&EVAL&?); eauto.
    2:{ eapply Forall_forall; intros.
        eapply MATCH_REGS, max_reg_function_use; eauto. }
    do 2 esplit.
    + apply plus_one. eapply exec_Iassert; eauto.
      erewrite transf_function_preserves with (id := id) (f := f); eauto.
      rewrite H0; trivial.
      eapply eval_condition_inject; eauto.
    + econstructor; eauto.
  (* internal call *)
  - monadInv MATCH_FUNCTIONS.
    rename x into tf.
    assert (0 <= 0) as LE0 by lia.
    assert (fn_stacksize f <= fn_stacksize f) as HI by lia.
    destruct (Mem.alloc_parallel_inject IF m tm _ _ _ _ 0 (fn_stacksize f) MATCH_MEM H1 LE0 HI) as (IF' & m2' & stk' & ALLOC' & MATCH_MEM' & INJECT_INCR & STK' & BLOCKS).
    left. eexists. split.
    + apply plus_one.
      apply exec_function_internal.
      * rewrite (sig_function_translated _ _ _ _ EQ).
        eapply Val.has_argtype_list_inject; eassumption.
      * erewrite stacksize_function_translated with (id := id) (f := f) by eassumption.
        exact ALLOC'.
    + erewrite entrypoint_function_translated with (f' := tf) (id := id) (f := f) by eassumption.
      erewrite params_function_translated with (f' := tf) (id := id) (f := f) by eassumption.
      apply match_states_intro with (cu:=cu) (bound:=bound) (IF:=IF') (id:=id); trivial.
      * eapply alloc_new_weakly_allocated_block. exact H1.
      * pose proof (Mem.alloc_result _ _ _ _ _ H1) as NSTK.
        pose proof (Mem.nextblock_alloc _ _ _ _ _ H1).
        unfold Ple, Plt in *. lia.
      * eapply ubound_stack_advance. 2: eassumption.
        pose proof (Mem.alloc_result _ _ _ _ _ H1) as NSTK.
        unfold Ple, Plt in *. lia.
      * eapply alloc_keep_weakly_allocated_stack; eassumption.
      * pose proof (Mem.alloc_result _ _ _ _ _ H1) as NSTK.
        unfold Ple in *. lia.
      * pose proof (Mem.nextblock_alloc _ _ _ _ _ H1).
        unfold Ple in *. lia.
      * pose proof (Mem.nextblock_alloc _ _ _ _ _ ALLOC').
        unfold Ple in *. lia.
      * pose proof (Mem.alloc_result _ _ _ _ _ H1) as NSTK.
        pose proof (Mem.alloc_result _ _ _ _ _ ALLOC') as NSTK'.
        apply (good_meminj_alloc bound m tm stk stk' IF IF'); auto.
      * apply match_stacks_incr with (IF:=IF); trivial.
      * apply match_regs_params.
        eapply val_inject_list_incr. exact INJECT_INCR.
        assumption.
        apply Forall_forall.
        intros.
        apply max_reg_function_params. assumption.
  - (* tail recursion *)
    left.
    destruct (transf_function_tail_rec _ _ _ _ _ _ _ MATCH_FUNCTIONS AT LENGTHS)
      as (next_pc & JUMP1 & REC_CALL).
    rewrite <- (params_function_translated _ _ _ _ MATCH_FUNCTIONS) in LENGTHS.
    rewrite <- (params_function_translated _ _ _ _ MATCH_FUNCTIONS) in REC_CALL.
    assert (Forall
         (fun r : positive => (r <= max_reg_function f)%positive)
         (fn_params f)) as PARAMS_OK.
    { apply Forall_forall. intros.
      apply max_reg_function_params. assumption. }
    assert (Forall
         (fun r : positive => (r < Pos.succ (max_reg_function f))%positive)
         (fn_params f)) as PARAMS_OK'.
    { apply Forall_forall. intros.
      assert (x <= max_reg_function f)%positive.
      { apply max_reg_function_params. assumption. }
      lia.
    }
    assert (Forall
         (fun r : positive => (r < Pos.succ (max_reg_function f))%positive)
         args0) as ARGS_OK'.
    { apply Forall_forall. intros.
      rewrite Forall_forall in ARGS_OK.
      assert (x <= max_reg_function f)%positive by auto.
      lia. }
    erewrite <- params_function_translated in PARAMS_OK' by eassumption.
    destruct (exec_tail_rec_call tge _ _ _ _ _ ts trs tm tsp ARGS_OK' PARAMS_OK' LENGTHS REC_CALL)
      as (trs1 & trs2 & PLUS & FINAL).
    exists (State ts tf (block2sp tsp) (fn_entrypoint f) trs2 tm).
    split.
    + eapply plus_left. apply exec_Inop.
      exact JUMP1. 2: reflexivity.
      apply plus_star. exact PLUS.
    + rewrite FINAL.
      assert (inject_incr IF (meminj_subst IF sp stk)) as INJECT'.
      { apply meminj_subst_incr.
        destruct MATCH_MEM.
        apply mi_freeblocks.
        intro BAD_VALID.
        pose proof (Mem.valid_block_free_1 _ _ _ _ _ FREE _ BAD_VALID) as MEUH.
        pose proof (Mem.fresh_block_alloc _ _ _ _ _ H1).
        contradiction.
      }
      apply match_states_intro with (cu:=cu) (bound:=bound) (id:=id) (IF:=meminj_subst IF sp stk).
      * assumption.
      * eapply alloc_new_weakly_allocated_block; eassumption.
      * rewrite (Mem.alloc_result _ _ _ _ _ H1).
        rewrite (Mem.nextblock_alloc _ _ _ _ _ H1).
        unfold Plt. lia.
      * eapply ubound_stack_advance. 2: eassumption.
        rewrite (Mem.alloc_result _ _ _ _ _ H1).
        rewrite (Mem.nextblock_free _ _ _ _ _ FREE).
        unfold Plt, Ple in *. lia.
      * eapply alloc_keep_weakly_allocated_stack. 2: eassumption.
        -- eapply ubound_stack_advance. 2: eassumption.
           rewrite (Mem.nextblock_free _ _ _ _ _ FREE).
           unfold Plt, Ple in *. lia.
        -- eapply free_weakly_allocated_stack. 2,3: eassumption.
           apply ubound_not_in_stack; eassumption.
      * pose proof (Mem.alloc_result _ _ _ _ _ H1).
        pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
        unfold Ple in *. lia.
      * pose proof (Mem.nextblock_alloc _ _ _ _ _ H1).
        pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
        unfold Ple in *. lia.
      * assumption.
      * pose proof (Mem.alloc_result _ _ _ _ _ H1).
        pose proof (Mem.nextblock_free _ _ _ _ _ FREE).
        apply good_meminj_subst; trivial.
        unfold Ple in *. lia.
      * apply match_stacks_incr with (IF := IF); auto.
      * assumption.
      * rewrite (params_function_translated _ _ _ _ MATCH_FUNCTIONS).
        apply match_copy; trivial.
        apply match_regs_incr with (IF:=IF); auto.
      * unfold match_sp, meminj_subst.
        destruct (peq stk stk). 2: contradiction.
        exact MATCH_SP.
      * eapply free_alloc_inject; try eassumption; intros.
        -- unfold weakly_allocated_block in WEAKLY_ALLOCATED_FRAME.
           eapply WEAKLY_ALLOCATED_FRAME.
           eapply Mem.perm_max.
           eassumption.
        -- eapply mem_free_perm_4; eassumption.
  - (* external call *)
    inv MATCH_FUNCTIONS.
    destruct (external_call_mem_inject ef _ _ _ (good_meminj_preserves_globals _ _ GLOBALS) H0 MATCH_MEM MATCH_ARGS) as (IF' & vres' & m2' & CALL' & MATCH_RES' & MATCH_MEM' & UNCHANGED1 & UNCHANGED2 & INCR & SEPARATED).
    left. eexists. split.
    + apply plus_one.
      apply exec_function_external.
      apply external_call_symbols_preserved with (ge1 := ge).
      { apply senv_preserved. }
      exact CALL'.
    + apply match_states_return with (bound:=bound) (IF := IF'); trivial.
      * pose proof (external_call_nextblock _ _ _ _ _ _ _ H0).
        eapply ubound_stack_advance. 2: eassumption. assumption.
      * eapply external_call_weakly_allocated_stack; eassumption.
      * destruct UNCHANGED1.
        unfold Ple in *. lia.
      * destruct UNCHANGED2.
        unfold Ple in *. lia.
      * apply good_meminj_separated with (IF:=IF) (m:=m) (tm:=tm); trivial.
      * apply match_stacks_incr with (IF := IF); trivial.
  (* return *)
  - inv MATCH_STACKS. inv H1. inv UBOUND_STACK. inv WEAKLY_ALLOCATED_STACK. inv H1.
    left.
    exists (State l' tf (block2sp tsp) pc trs # res <- tres tm).
    split.
    { apply plus_one. constructor. }
    econstructor; eauto.
    apply match_regs_assign; auto.
Qed.

Theorem transf_program_correct:
  forward_simulation (semantics prog) (semantics tprog).
  eapply forward_simulation_star.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  eexact step_simulation.
Qed.

End TAILREC.

Global Instance TransfSelectionLink : TransfLink match_prog.
Proof.
  red; intros.
  destruct (link_linkorder _ _ _ H) as [LO1 LO2].
  eapply link_match_program; eauto.
  intros.
  Local Transparent Linker_fundef.
  Local Opaque transf_function'.
  unfold link. cbn. unfold match_fundef in *.
  destruct H3 as (cu1 & id1 & LINK1 & TRANSF1).
  destruct H4 as (cu2 & id2 & LINK2 & TRANSF2).
  destruct f1; cbn in TRANSF1.
  - destruct f2; cbn in H2. discriminate.
    destruct e; try discriminate. inv H2.
    cbn in TRANSF2. inv TRANSF2.
    unfold transf_fundef, transf_function in *.
    rename f0 into f1.
    destruct (option_eq_dec eq_fundef
                  (find_function (Genv.globalenv cu1)
                     (inr id1) (Regmap.init Vundef))
                  (Some (Internal f1))) as [EQ1 | NEQ1 ] eqn:FIND1; [idtac | discriminate].
    destruct successors_inside eqn:SUCCESSORS; [idtac | discriminate].
    cbn in TRANSF1. monadInv TRANSF1. rename x into f1'.
    simpl. exists (Internal f1'). split. reflexivity.
    left. exists cu1. exists id1. split. assumption.
    rewrite SUCCESSORS. unfold find_function in FIND1. rewrite FIND1.
    rewrite EQ. cbn. reflexivity.
  - destruct f2; cbn in H2.
    + destruct e; try discriminate. inv H2.
      cbn in TRANSF1. inv TRANSF1.
      rename f0 into f2.
      cbn in TRANSF2. inv TRANSF2.
      unfold transf_fundef in H3.
      monadInv H3.
      unfold transf_function in EQ.
      destruct (option_eq_dec eq_fundef
                  (find_function (Genv.globalenv cu2)
                     (inr id2) (Regmap.init Vundef))
                  (Some (Internal f2))) as [EQ2 | NEQ2 ] eqn:FIND2; [idtac | discriminate].
      destruct successors_inside eqn:SUCCESSORS; [idtac | discriminate].
      cbn. rename x into tf2.
      exists (Internal tf2). split. reflexivity. right.
      exists cu2. exists id2. split. assumption.
      unfold transf_function.
      rewrite SUCCESSORS. rewrite FIND2. rewrite EQ.
      reflexivity.
    + destruct (external_function_eq e e0). 2: discriminate.
      subst e0. inv H2. inv TRANSF1. cbn in TRANSF2. inv TRANSF2.
      cbn. destruct (external_function_eq e e). 2: contradiction.
      exists (External e). split. reflexivity.
      left. exists cu1. exists id1. auto.
Qed.
Generated by coq2html