Module InjectWellBehaved

Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import ExprEval.
Require Import Memory.
Require Import Psatz.
Require Import MemRel Align Tactics.
Require Import Permutation MemReserve BlockAppears ForgetNorm ListUtils.

Definition inject_well_behaved (f: meminj) (m: mem) :=
  forall b, f b = None -> Mem.size_block m b <= 8 /\ (Mem.mask m b <= 3)%nat.

Definition is_injected (f: meminj) (b: block * Z) :=
  match f (fst b) with
    Some b2 => true
  | None => false
  end.

Record inj_well_behaved f m1 m2 :=
  {
    iwb_o2o: Mem.one2oneinject f;
    iwb_wb: inject_well_behaved f m1;
    iwb_bounds: forall b b' delta, f b = Some (b',delta) -> Mem.size_block m1 b = Mem.size_block m2 b';
    iwb_mask: forall b b' delta, f b = Some (b',delta) -> Mem.mask m1 b = Mem.mask m2 b';
    iwb_no_oota: forall b', Mem.valid_block m2 b' -> exists b delta, f b = Some (b', delta);
    iwb_inj: forall b1 b2 b' delta1 delta2, f b1 = Some (b', delta1) -> f b2 = Some (b', delta2) -> b1 = b2
  }.

Definition inj_block (f: meminj) :=
  (fun b : block =>
     match f b with
       Some (b',delta) => Some b'
     | None => None
     end).


Let B1 be the list of blocks of m1. We can split those blocks into l1 and l2, where l1 keeps the blocks that are injected by f, and l2 keeps the other blocks. This theorem shows that the blocks of m2 are the blocks of m1, with injection applied.

Lemma part_inj_permut:
  forall sm ei f m1 m2
    (IWB: inj_well_behaved f m1 m2)
    (MINJ: Mem.inject sm ei f m1 m2),
    Permutation
      (map fst (Mem.mk_block_list m2))
      (filter_map (inj_block f) (map fst (Mem.mk_block_list m1))).
Proof.
  intros.
  destruct (partition (is_injected f) (Mem.mk_block_list m1)) as [linj lnoinj] eqn:PI.
  pose proof (partition_app_perm _ _ _ _ PI) as P.

  rewrite <- permut_filter_map.
  2: apply Permutation_sym; apply Permutation_map; apply P.
  rewrite map_app.
  rewrite filter_map_app.
  assert (EQnil: filter_map (inj_block f) (map fst lnoinj) = nil).
  {
    apply not_inj_filter_map. intro b.
    rewrite ! in_map_iff.
    intros ((bb & z) & EQ & IN). simpl in EQ. subst.
    rewrite (in_partition_r _ _ _ _ PI (b,z)) in IN.
    destruct IN as (IN & NINJ).
    unfold is_injected in NINJ; unfold inj_block. simpl in *.
    destr_in NINJ.
  }
  rewrite EQnil, app_nil_r.
  clear EQnil.
  assert (LNRL1: list_norepet (map fst linj)).
  {
    eapply lnr_partition' in PI. destr.
    apply lnr_mbl.
  }
  assert (LNRL1': list_norepet (filter_map (inj_block f) (map fst linj))).
  {
    apply list_norepet_filter_map; auto.
    unfold inj_block; intros a1 a2 b1 b2 F1 F2 DIFF EQ; apply DIFF; subst.
    repeat destr_in F1; repeat destr_in F2.
    inv F2; inv F1.
    eapply iwb_inj; eauto.
  }
  assert (LNRM2: list_norepet (map fst (Mem.mk_block_list m2))).
  {
    apply lnr_mbl.
  }
  apply Permutation_intro; auto. apply peq.
  intro b.
  rewrite in_map_filter.
  setoid_rewrite in_map_iff.
  setoid_rewrite (in_partition_l _ _ _ _ PI).
  unfold inj_block, is_injected.
  split.
  - intros ((bb & z) & EQ & IN). simpl in EQ; subst.
    exploit in_bl. apply IN. intro LE.
    assert (VB: Mem.valid_block m2 b). red. apply Pos2Nat.inj_lt. lia.
    destruct (iwb_no_oota _ _ _ IWB _ VB) as (bb & delta & FB).
    eexists; split.
    eexists (bb, _); split; eauto.
    simpl; rewrite FB. split; auto.
    2: simpl; rewrite FB; auto.
    apply mbla_below_in'.
    exploit Mem.valid_block_inject_1. apply FB. eauto. intro v.
    red in v. rewrite Pos2Nat.inj_lt in v. lia.
  - intros (bb & ((bbb & z) & EQ & INJ) & INJB).
    destruct INJ as [IN FB]. simpl in *. subst.
    des (f bb). des p. inv INJB.
    eexists (b, _); split; eauto.
    eapply mbla_below_in'.
    exploit Mem.mi_mappedblocks. eauto. eauto. intros.
    apply Pos2Nat.inj_lt in H. lia.
Qed.

Lemma inject_well_behaved_diff_blocks:
  forall sm ei f m1 m2
    (MINJ: Mem.inject sm ei f m1 m2)
    (IWB: inj_well_behaved f m1 m2)
    l0 l1
    (PART: partition (is_injected f) (Mem.mk_block_list m1) = (l0,l1)),
    (num_boxes (boxes (canon_cm m2) (Mem.mk_block_list m2)) +
     sum (map (box_span m1 (canon_cm m1)) (map fst l1)))%nat =
    num_boxes (boxes (canon_cm m1) (Mem.mk_block_list m1)).
Proof.
  intros.
  generalize (part_inj_permut _ _ _ _ _ IWB MINJ).
  intro PIP.
  exploit (partition_app_perm (A:= block*Z)). eauto. intro PERM.
  setoid_rewrite box_range'_eq.
  setoid_rewrite length_concat.
  rewrite ! (map_map (box_range' _ _) (@length _)).
  generalize (Permutation_map (fun x => length (box_range' m1 (canon_cm m1) x))
                              (Permutation_map fst PERM)). intro P.
  rewrite (sum_permut _ _ P).
  rewrite map_app.
  rewrite map_app.
  rewrite sum_app. f_equal.
  generalize (Permutation_map (fun x => length (box_range' m2 (canon_cm m2) x)) PIP). intro P'.
  rewrite (sum_permut _ _ P').
  rewrite (partition_l _ _ _ _ PART).
  erewrite map_filter_map with (f':=fst) (g':=fun b => match f b with
                                                      Some (b',delta) => Some b
                                                    | None => None
                                                    end).
  Focus 2.
  intros a b INJ. exists (fst a). unfold is_injected in INJ. repeat destr.
  Focus 2.
  intros. exists a; unfold is_injected. repeat destr_in H.
  f_equal.
  erewrite ! map_filter_map'.
  apply filter_map_ext.
  clear - IWB.
  intros. unfold inj_block. des (f x). des p.
  unfold box_range'.
  erewrite <- iwb_bounds; eauto.
  destruct (zlt 0 (Mem.size_block m1 x)).
  rewrite ! length_box_range_canon_cm; auto.
  unfold box_range.
  destr.
Qed.

Lemma inject_well_behaved_diff_blocks_num:
  forall sm ei f m1 m2
    (MINJ: Mem.inject sm ei f m1 m2)
    (IWB: inj_well_behaved f m1 m2)
    l0 l1
    (PART: partition (is_injected f) (Mem.mk_block_list m1) = (l0,l1)),
    (nb_boxes_used_cm m2 (canon_cm m2) + sum (map (box_span m1 (canon_cm m1)) (map fst l1)) = nb_boxes_used_cm m1 (canon_cm m1))%nat.
Proof.
  intros.
  unfold nb_boxes_used_cm.
  rewrite ! (lnr_remove _ (lnr_canon _)).
  fold (boxes (canon_cm m2) (Mem.mk_block_list m2)).
  fold (boxes (canon_cm m1) (Mem.mk_block_list m1)).
  eapply inject_well_behaved_diff_blocks. eauto. eauto. eauto.
Qed.

Lemma iwb_in_bound:
  forall f m1 m2 (IWF: inj_well_behaved f m1 m2)
    b b0 z (FB: f b = Some (b0,z))
    o (IB: in_bound o (Mem.bounds_of_block m1 b)),
    in_bound o (Mem.bounds_of_block m2 b0).
Proof.
  intros.
  rewrite bounds_eq in *.
  erewrite <- iwb_bounds; eauto.
Qed.

Lemma not_inj_in_bound_in_filter_map:
  forall f m1 l l0 b' o'
    (PART: partition (is_injected f) (Mem.mk_block_list m1) = (l,l0))
    (FB: f b' = None)
    (IB: in_bound (Int.unsigned o') (Mem.bounds_of_block m1 b')),
    In b' (filter_map (fun bsz : block * Z => let (b,sz) := bsz in
                                           if zlt 0 sz
                                           then Some b
                                           else None) l0).
Proof.
  intros.
  rewrite in_map_filter. exists (b', Mem.size_block m1 b'). simpl; split; auto.
  rewrite in_partition_r; eauto. split.
  eapply mbla_below_in'.
  eapply Mem.in_bound_valid in IB. red in IB. apply Pos2Nat.inj_lt in IB. lia.
  unfold is_injected; simpl; rewrite FB. auto.
  rewrite bounds_eq in IB. red in IB. destr. lia.
Qed.



Lemma length_filter_map_fold_right:
  forall f m1 m2 l l0
    (IWB: inj_well_behaved f m1 m2)
    (PART: partition (is_injected f) (Mem.mk_block_list m1) = (l,l0)),
    length (filter_map (fun bsz : block * Z => let (b0, sz) := bsz in if zlt 0 sz then Some b0 else None) l0)
    = fold_right Peano.plus 0%nat (map (fun x : block => length (box_range' m1 (canon_cm m1) x)) (map fst l0)).
Proof.
  intros. generalize (fun b => (proj1 (in_partition_r _ _ _ _ PART b))).
  clear - IWB.
  induction l0; simpl; intros; eauto.
  des a.
  destr.
  rewrite IHl0. simpl.
  replace (length (box_range' m1 (canon_cm m1) b)) with 1%nat. lia.
  unfold box_range'.
  unfold is_injected in H.
  specialize (H _ (or_introl eq_refl)). Opaque box_range.
  destr_in H.
  destruct H.
  unfold Mem.mk_block_list in H. eapply mbla_in in H. subst.
  rewrite length_box_range_canon_cm.
  rewrite Z.div_small. reflexivity.
  exploit iwb_wb; eauto. lia. lia.
  intros; apply H; eauto.
  rewrite IHl0. 2: intros; apply H; auto.
  replace (length (box_range' m1 (canon_cm m1) b)) with O. lia.
  unfold box_range'. Transparent box_range. simpl. destr. exfalso.
  unfold is_injected in H.
  specialize (H _ (or_introl eq_refl)). Opaque box_range.
  destr_in H.
  destruct H.
  unfold Mem.mk_block_list in H. eapply mbla_in in H. subst.
  lia.
Qed.

Lemma not_inj_in_bound_get_addr:
  forall f m1 m2 l l0 b' o'
    (IWB: inj_well_behaved f m1 m2)
    (PART: partition (is_injected f) (Mem.mk_block_list m1) = (l,l0))
    (FB: f b' = None)
    (IB: in_bound (Int.unsigned o') (Mem.bounds_of_block m1 b')),
    let l' := (filter_map (fun bsz : block * Z => let (b,sz) := bsz in
                                               if zlt 0 sz
                                               then Some b
                                               else None) l0) in
    forall l1 (LEN: (length l1 >= fold_right Peano.plus 0%nat (map (fun x : block => length (box_range' m1 (canon_cm m1) x)) (map fst l0)))%nat),
    exists n (x: Z),
      find peq b' l' = Some n /\
      (n < length l')%nat /\
      list_nth_z l1 (Z.of_nat n) = Some x
.
Proof.
  intros.
  exploit not_inj_in_bound_in_filter_map; eauto. intro H.
  destruct (find_in peq _ _ H) as (n & EQ & LT). unfold l'. rewrite EQ.
  destruct (list_nth_z_succeeds l1 (Z.of_nat n)) as (A & EQA).
  split. lia. apply inj_lt.
  eapply lt_le_trans. apply LT.
  erewrite length_filter_map_fold_right;eauto.
  eexists; eexists; eauto.
Qed.

Opaque Z.mul.


Theorem forget_compat:
  forall sm ei f m1 m2
    (MINJ: Mem.inject sm ei f m1 m2)
    (IWB: inj_well_behaved f m1 m2)
    cm2
    (COMP: Mem.compat_m m2 Mem.M32 cm2),
  exists cm1,
    Mem.compat_m m1 Mem.M32 cm1 /\
    (forall b b' : block, f b = Some (b',0) -> cm1 b = cm2 b').
Proof.
  intros.
  des (partition (is_injected f) (Mem.mk_block_list m1)).
  assert (has_free_boxes
            m2 cm2
            (sum (map (fun x : block => length (box_range' m1 (canon_cm m1) x)) (map fst l0)))).
  {
    red.
    eapply le_lt_trans.
    eapply NPeano.Nat.add_le_mono.
    eapply canon_cm_more_boxes. eauto. apply eq_le; eauto.
    rewrite plus_0_r. setoid_rewrite inject_well_behaved_diff_blocks_num; eauto.
    eapply le_lt_trans.
    eapply nb_boxes_used_cm_nb_boxes_used_m.
    apply mult_lt_le_mono; [|split; [apply two_power|lia]].
    apply Nat2Z.inj_lt. rewrite Z2Nat.id.
    apply Mem.wfm_alloc.
    apply Mem.nb_boxes_max_pos.
  }
  apply has_free_boxes_correct in H.
  destruct H as (l1 & LEN & LNR & PROP & ADDRSPACE & ALIGN).
  exists (fun b =>
       match f b with
         Some (b', delta) => cm2 b'
       | None =>
         match
           map_option
             (fun n => list_nth_z l1 (Z.of_nat n))
             (find peq b (filter_map (fun bsz : block * Z =>
                                        let (b,sz) := bsz in
                                        if zlt 0 sz
                                        then Some b
                                        else None) l0)) with
           Some A => Int.repr A
         | None => Int.zero
         end
       end
    ).
  split.
  - constructor.
    + intros b o IB.
      destr. des p.
      *
        inv COMP. apply addr_space.
        eapply iwb_in_bound; eauto.
      *
        exploit not_inj_in_bound_get_addr. eauto. eauto. eauto. eauto. apply LEN.
        intros (n & A & EQ & LT & EQA).
        rewrite EQ. simpl. rewrite EQA.
        rewrite Forall_forall in ADDRSPACE.
        trim (ADDRSPACE A).
        eapply list_nth_z_in; eauto.

        generalize (ADDRSPACE o). intro AO. trim AO.
        rewrite bounds_eq in IB.
        red in IB. simpl in IB.
        exploit iwb_wb; eauto. lia.

        generalize (ADDRSPACE Int.zero). intro A0. trim A0.
        rewrite Int.unsigned_zero. lia.
        rewrite Int.unsigned_zero in A0.

        rewrite Int.add_unsigned.
        rewrite (Int.unsigned_repr A) by lia.
        rewrite Int.unsigned_repr; lia.

    + intros b b' o o' DIFF IB IB'.
      destr. des p.
      * destr. des p.
        {
          inv COMP. apply overlap; auto.
          intro; subst.
          exploit iwb_inj. eauto. apply Heqo1. apply Heqo0. destr.
          eapply iwb_in_bound; eauto.
          eapply iwb_in_bound; eauto.
        }
        {
          exploit not_inj_in_bound_get_addr. eauto. eauto. eauto. eauto. apply LEN.
          intros (n & A & EQ & LT & EQA).
          rewrite EQ. simpl. rewrite EQA.
          rewrite Forall_forall in PROP. apply PROP.
          eapply list_nth_z_in; eauto.
          eapply iwb_in_bound; eauto.
          rewrite bounds_eq in IB'.
          red in IB'. simpl in IB'.
          exploit iwb_wb; eauto. lia.
        }
      * destr.
        {
          exploit not_inj_in_bound_get_addr. eauto. eauto. eauto. eauto. apply LEN.
          intros (n & A & EQ & LT & EQA).
          revert Heqo1. rewrite EQ. simpl. rewrite EQA. intro B; inv B.
          rewrite Forall_forall in PROP.
          generalize (PROP z). intro PZ.
          trim PZ. eapply list_nth_z_in; eauto.
          specialize (fun LT b2 d pf => PZ _ _ o (iwb_in_bound _ _ _ IWB b' b2 d pf _ IB') LT).
          trim PZ.
          rewrite bounds_eq in IB.
          red in IB. simpl in IB.
          exploit iwb_wb; eauto. lia.
          destr.
          {
            des p. specialize (PZ _ _ eq_refl). auto.
          }
          {
            exploit not_inj_in_bound_get_addr. eauto. eauto. apply Heqo1. eauto. apply LEN.
            intros (n2 & A2 & EQ2 & LT2 & EQA2).
            rewrite EQ2. simpl. rewrite EQA2. intro B; inv B.
            assert (n <> n2) by eauto using find_diff_diff.
            rewrite bounds_eq in IB, IB'.
            red in IB, IB'. simpl in IB, IB'.
            exploit iwb_wb. eauto. apply Heqo0.
            exploit iwb_wb. eauto. apply Heqo1.
            assert (z <> A2) by (eapply lnr_list_nth_z_diff; eauto; lia).
            intros.
            rewrite Forall_forall in ADDRSPACE.
            specialize (fun o pf x pf' => ADDRSPACE x pf' o pf).
            generalize (ADDRSPACE o). intro ASo.
            trim ASo. lia.
            trim (ASo z).
            eapply list_nth_z_in; eauto.
            generalize (ADDRSPACE o'). intro ASo'.
            trim ASo'. lia.
            trim (ASo' A2).
            eapply list_nth_z_in; eauto.
            generalize (ADDRSPACE Int.zero). intro AS0.
            trim AS0. rewrite Int.unsigned_zero. lia.
            generalize (AS0 _ (list_nth_z_in _ _ EQA)).
            generalize (AS0 _ (list_nth_z_in _ _ EQA2)). rewrite Int.unsigned_zero. intros A2rng Zrng.
            intros; revert H0.
            unfold Int.add.
            rewrite (Int.unsigned_repr z) by lia.
            rewrite (Int.unsigned_repr A2) by lia.
            rewrite ! Int.unsigned_repr by lia.
            rewrite Forall_forall in ALIGN.
            destruct (ALIGN _ (list_nth_z_in _ _ EQA)) as (k & EQk).
            destruct (ALIGN _ (list_nth_z_in _ _ EQA2)) as (k2 & EQk2).
            subst.
            clear - H1 H2 H3 IB IB'. lia.
          }
        }
        {
          des (find peq b (filter_map (fun bsz : block * Z => let (b0, sz) := bsz in if zlt 0 sz then Some b0 else None) l0)).
          eapply find_some_range in Heqo2.
          erewrite length_filter_map_fold_right in Heqo2; eauto.
          exploit (list_nth_z_succeeds (A:=Z)). split.
          2: eapply Z.lt_le_trans. 2: apply Heqo2. lia.
          apply inj_le. instantiate (1 := l1).
          unfold sum in LEN. lia.
          intros (x & EQ). destr.

          assert (~ In b (filter_map (fun bsz : block * Z =>
                                        let (b0, sz) := bsz in
                                        if zlt 0 sz
                                        then Some b0
                                        else None) l0)).
          intro IN.
          eapply find_in with (eq_dec:=peq) (x:=b) in IN. dex; destr.
          rewrite in_map_filter in H.
          exfalso; apply H.
          exists (b, Mem.size_block m1 b).
          rewrite in_partition_r. 2: eauto. unfold is_injected. simpl. rewrite Heqo0.
          repSplit; auto.
          eapply mbla_below_in'.
          eapply Mem.in_bound_valid in IB. red in IB. apply Pos2Nat.inj_lt in IB. lia.
          destr.
          contradict IB. rewrite bounds_eq. unfold in_bound. simpl. lia.
        }
    + intros.
      destr. des p.
      *
        unfold Mem.nat_mask. erewrite iwb_mask; eauto.
        inv COMP; eauto.
      *
        destr.
        des (find peq b (filter_map (fun bsz : block * Z => let (b0, sz) := bsz in if zlt 0 sz then Some b0 else None) l0)).
        rewrite Forall_forall in ALIGN.
        destruct (ALIGN _ (list_nth_z_in _ _ Heqo0)) as (k & EQk).
        subst.
        exploit iwb_wb; eauto. intros (B & M).
        IntFacts.solve_int.
        rewrite Int.testbit_repr; auto.
        replace (8*k) with (k * 2 ^ 3) by lia.
        rewrite Z.mul_pow2_bits by lia.
        des (Z.testbit k (i-3)).
        assert (i-3 >= 0). destruct (zle 0 (i-3)). lia. rewrite Z.testbit_neg_r in Heqb0. congruence. lia.
        unfold Mem.nat_mask.
        rewrite Int.bits_not; auto. rewrite Int.testbit_repr; auto.
        rewrite two_power_nat_two_p, Int.Ztestbit_two_p_m1; auto. destr. lia. lia.
  - intros. rewrite H. auto.
  - auto.
Qed.



Lemma forget_norm:
  forall sm ei (wf: wf_inj ei) (f : meminj) (m1 m2 : mem),
    Mem.inject sm ei f m1 m2 ->
    inj_well_behaved f m1 m2 ->
    forall e1 e2 (EI: ei f e1 e2) (BA: sep_inj m1 f e1),
      val_inject f (Mem.mem_norm m1 e1) (Mem.mem_norm m2 e2).
Proof.
  intros.
  destruct (Val.eq_val_dec (Mem.mem_norm m1 e1) Vundef) as [MN|NMN]; auto.
  rewrite MN; auto.
  assert (exists x, val_inject f (Mem.mem_norm m1 e1) x /\ x <> Vundef).
  {
    des (Mem.mem_norm m1 e1); eauto.
    des (f b). des p. eexists; econstructor. econstructor; eauto. destr.
    exploit BA; eauto. 2: easy.
    red; red; intros.
    generalize (Mem.norm_ld _ _ _ Heqv _ em COMP). generalize (Mem.norm_ld _ _ _ Heqv _ em COMP').
    simpl. intros A B; inv A; inv B.
    intro C. apply inj_vint in C.
    rewrite <- ! (Int.add_commut i) in C. apply int_add_eq_l in C. destr.
  }
  dex. des H1.
  replace x with (Mem.mem_norm m2 e2) in v. auto.
  apply Mem.eq_norm; auto.
  constructor.
  intros cm2 em COMPAT.
  exploit forget_compat; eauto.
  intros [cm1 [A B]].
  assert (eSval cm2 x = eSval cm1 (Mem.mem_norm m1 e1)).
  des (Mem.mem_norm m1 e1); inv v; simpl; auto.
  exploit iwb_o2o; eauto. intros; subst.
  erewrite B; eauto. rewrite Int.add_zero; auto.
  simpl; rewrite H1.
  eapply Values.Val.lessdef_trans. eapply Mem.norm_ld. eauto. eauto.
  eapply ei_ld'_expr; eauto.
  red; intros. exploit iwb_o2o; eauto; intros; subst. subst.
  rewrite Int.add_zero; eauto.
  apply em_inj_inj_em.
Qed.

Lemma norm_forget:
  forall sm ei (wf: wf_inj ei) f m m' e1 v1 e1'
    (O2O: inj_well_behaved f m m')
    (INJ: Mem.inject sm ei f m m')
    (EI: ei f e1 e1')
    (NU: v1 <> Vundef),
  forall (MN:Mem.mem_norm m e1 = v1) (BA: sep_inj m f e1),
    Mem.mem_norm m' e1' <> Vundef /\
    ei f (Eval v1) (Eval (Mem.mem_norm m' e1')).
Proof.
  intros.
  pose proof (Mem.norm_ld m e1 _ MN) as N.
  pose proof (Mem.norm_gr m e1) as GR. rewrite MN in GR.
  destruct (Val.apply_inj f (Eval v1)) eqn:?; try congruence.
  - clear MN. destruct (inj_eval_eval _ _ _ Heqo). subst.
    cut (Mem.mem_norm m' e1' = x).
    intro MNV; subst.
    + split.
      * unfold Val.apply_inj, Val.inj_ptr in Heqo.
        intro H. rewrite H in Heqo.
        des v1. des (f b). des p.
      * apply vi_ei. auto. auto.
    + apply Mem.eq_norm. constructor.
      * intros cm2 em COMPAT.
        exploit forget_compat; eauto.
        intros [cm1 [A B]].
        assert (eSval cm2 x = eSval cm1 v1).
        des v1; inv Heqo; simpl; auto.
        unfold Val.inj_ptr in H0; des (f b); des p.
        inv H0. simpl.
        exploit iwb_o2o; eauto. intros; subst.
        erewrite B; eauto. rewrite Int.add_zero; auto.
        simpl; rewrite H.
        eapply Values.Val.lessdef_trans. apply N. auto.
        eapply ei_ld'_expr; eauto.
        red; intros. exploit iwb_o2o; eauto; intros; subst. subst.
        rewrite Int.add_zero; eauto.
        apply em_inj_inj_em.
      * des v1. unfold Val.inj_ptr in Heqo; des (f b); des p.
  - exfalso.
    des v1;
      unfold Val.inj_ptr in Heqo;
      des (f b); try des p.
    exploit BA; eauto.
Qed.

Lemma storev_inject:
  forall sm ei (wf: wf_inj ei) f chunk m1 a1 v1 n1 m2 a2 v2
    (IWB: inj_well_behaved f m1 m2)
    (INJ: Mem.inject sm ei f m1 m2)
    (STOREV: Mem.storev chunk m1 a1 v1 = Some n1)
    (EIaddr: ei f a1 a2)
    (SI: sep_inj m1 f a1)
    (EIval: ei f v1 v2),
  exists n2,
    Mem.storev chunk m2 a2 v2 = Some n2 /\ Mem.inject sm ei f n1 n2.
Proof.
  intros.
  unfold Mem.storev in *; revert STOREV; destr.
  generalize (forget_norm _ _ wf _ _ _ INJ IWB _ _ EIaddr SI).
  rewrite Heqv; intro A; inv A. intro.
  exploit Mem.store_mapped_inject; eauto.
  intros [n2 [A B]]; exists n2; split; auto.
  rewrite <- A.
  f_equal.
  eapply Mem.address_inject'; eauto.
  eapply Mem.store_valid_access_1; eauto.
  eapply Mem.valid_access_implies; eauto.
  eapply Mem.store_valid_access_3; eauto.
  constructor.
Qed.

Lemma loadv_inject:
  forall sm ei (wf: wf_inj ei) f chunk m1 a1 v1 m2 a2
    (IWB: inj_well_behaved f m1 m2)
    (INJ: Mem.inject sm ei f m1 m2)
    (LOADV: Mem.loadv chunk m1 a1 = Some v1)
    (EIaddr: ei f a1 a2)
    (SI: sep_inj m1 f a1),
  exists v2,
    Mem.loadv chunk m2 a2 = Some v2 /\ ei f v1 v2.
Proof.
  intros.
  unfold Mem.loadv in *; destr_in LOADV.
  generalize (forget_norm _ _ wf _ _ _ INJ IWB _ _ EIaddr SI).
  rewrite Heqv; intro A; inv A.
  exploit Mem.load_inject; eauto.
  intros [v2 [A B]]; exists v2; split; auto.
  rewrite <- A.
  f_equal.
  eapply Mem.address_inject'; eauto.
  eapply Mem.valid_access_implies; eauto.
  eapply Mem.load_valid_access; eauto.
  constructor.
Qed.

Lemma o2oinj_inverse:
  forall f m tm (IWB: inj_well_behaved f m tm)
    sm ei (MINJ: Mem.inject sm ei f m tm),
  exists g, forall b b', f b = Some (b',0) -> g b' = Some b.
Proof.
  intros.
  set (bl := Alloc.list_ints (Pos.to_nat (Mem.nextblock m))).
  set (bl' := map (fun x => let b := Pos.of_nat x in (b, f b)) bl).
  set (filter_fun := fun (b:block) (x: block * option (block*Z)) =>
                       match snd x with
                         Some (b',delta) => if peq b b' then true else false
                       | _ => false
                       end).
  exists (fun b => head (map fst (filter (filter_fun b) bl'))).
  intros.
  assert (ISIN: In (b, Some (b', 0)) bl').
  {
    destruct (Mem.valid_block_dec m b).
    apply in_map_iff.
    exists (Pos.to_nat b).
    rewrite Pos2Nat.id. simpl. unfold block. split; auto.
    f_equal; auto.
    apply list_ints_le.
    split. zify; omega.
    apply Pos2Nat.inj_le.
    unfold Mem.valid_block in v. xomega.
    eapply Mem.mi_freeblocks in n; eauto. congruence.
  }
  assert (UNIQUE: forall bb delta, In (bb, Some (b', delta)) bl' -> b = bb /\ delta = 0).
  {
    intros bb delta IN.
    generalize IN; intro IN'.
    unfold bl' in IN. rewrite in_map_iff in IN.
    dex; destr. des IN. inv e.
    exploit iwb_o2o; eauto. intros; subst.
    destruct (peq b (Pos.of_nat x)); auto.
    exploit iwb_inj. eauto. apply H. apply H2. auto.
  }
  assert (ALL: Forall (fun x => x = (b, Some (b',0))) (filter (filter_fun b') bl')). {
    rewrite Forall_forall.
    intros x IN.
    apply filter_charact in IN. destruct IN as [IN INEQ].
    revert INEQ. unfold filter_fun; simpl.
    des x. des o. des p. destr. intros _. subst. apply UNIQUE in IN. destr.
  }
  des (filter (filter_fun b') bl').
  generalize (filter_charact _ (filter_fun b') (b , Some (b',0)) bl').
  rewrite Heql. destr. intros [A B].
  exfalso; apply B; unfold filter_fun; simpl. rewrite peq_true; auto.
  inv ALL; reflexivity.
Qed.

Lemma o2oinj_cm_inj:
  forall f sm ei m tm
    (IWB: inj_well_behaved f m tm)
    (MINJ: Mem.inject sm ei f m tm) cm,
  exists cm',
    cm_inj cm' f cm.
Proof.
  intros.
  exploit o2oinj_inverse; eauto.
  intros [g SPEC].
  exists (fun bb => match g bb with
              Some b => cm b
            | None => Int.zero
            end); simpl.
  red; intros.
  exploit iwb_o2o; eauto. intros; subst. rewrite Int.add_zero.
  erewrite SPEC; eauto.
Qed.

Lemma o2oinj_em_inj:
  forall f sm ei m tm
    (IWB: inj_well_behaved f m tm)
    (MINJ: Mem.inject sm ei f m tm)
    em,
  exists em',
    em_inj em' f em.
Proof.
  intros.
  exploit o2oinj_inverse; eauto.
  intros [g SPEC].
  exists (fun bb i => match g bb with
                Some b => em b i
              | None => Byte.zero
              end); simpl.
  red; intros.
  exploit iwb_o2o; eauto. intros; subst. rewrite Int.add_zero.
  erewrite SPEC; eauto.
Qed.


Lemma expr_inj_se_not_dep:
  forall sm ei f m tm v v'
    (IWB: inj_well_behaved f m tm)
    (MINJ: Mem.inject sm ei f m tm)
    (EI: expr_inj_se f v v'),
    sep_inj m f v.
Proof.
  intros sm ei f m tm v v' IWB MINJ (a & b & A & B & C).
  red. intros b0 Fb.
  generalize (expr_inj_not_dep _ _ _ C _ Fb). intros NBA DEP.
  eapply (dep_block_appears' m) in NBA; eauto.
  apply NBA.
  red; red; intros.
  specialize (DEP _ COMP _ COMP' SameB em).
  destruct (o2oinj_inverse _ _ _ IWB _ ei MINJ) as [g SPEC].
  intros.
  edestruct (o2oinj_em_inj) with (em:=em) as [em' EMINJ]; eauto.
  edestruct (o2oinj_cm_inj) with (cm:=cm) as [dep_cmi CMINJ]; eauto.
  edestruct (o2oinj_cm_inj) with (cm:=cm') as [dep_cmi' CMINJ']; eauto.
  erewrite <- ! A; eauto.
Qed.

Lemma list_expr_inj_se_not_dep:
  forall sm ei f m tm v v'
    (IWB: inj_well_behaved f m tm)
    (MINJ: Mem.inject sm ei f m tm)
    (EI: list_ei expr_inj_se f v v'),
    Forall (sep_inj m f) v.
Proof.
  induction 3;simpl; intros; auto.
  constructor; auto.
  eapply expr_inj_se_not_dep; eauto.
Qed.

Lemma iwb_inv:
  forall f m tm (IWB: inj_well_behaved f m tm)
    m' tm'
    (BND: forall b, Mem.bounds_of_block m b = Mem.bounds_of_block m' b)
    (BNDt: forall b, Mem.bounds_of_block tm b = Mem.bounds_of_block tm' b)
    (MSK: forall b, Mem.mask m b = Mem.mask m' b)
    (MSKt: forall b, Mem.mask tm b = Mem.mask tm' b)
    (PLE: forall b', Ple (Mem.nextblock tm) b' -> Plt b' (Mem.nextblock tm') ->
                exists b delta, f b = Some (b', delta)),
    inj_well_behaved f m' tm'.
Proof.
  intros.
  inv IWB; constructor; auto.
  - red in iwb_wb0 |- *; intros.
    rewrite <- Mem.size_block_snd.
    rewrite <- BND, <- MSK.
    rewrite Mem.size_block_snd.
    eauto.
  - intros.
    rewrite <- ! Mem.size_block_snd.
    rewrite <- BND, <- BNDt.
    rewrite ! Mem.size_block_snd.
    eauto.
  - intros; rewrite <- MSK, <- MSKt. eauto.
  - intros.
    unfold Mem.valid_block in iwb_no_oota0, H.
    destruct (plt b' (Mem.nextblock tm)). auto.
    apply PLE; auto. xomega.
Qed.

Lemma free_inject:
  forall f sm
    m tm (ME: Mem.inject sm expr_inj_se f m tm)
    (IWB: inj_well_behaved f m tm)
    b lo hi
    m' (FREE: Mem.free m b lo hi = Some m')
    b'
    (FB: f b = Some (b',0))
    tm'
    (FREE': Mem.free tm b' lo hi = Some tm'),
    Mem.inject sm expr_inj_se f m' tm' /\
    inj_well_behaved f m' tm'.
Proof.
  clear.
  intros. Transparent Mem.free.
  unfold Mem.free in *.
  repeat destr_in FREE. repeat destr_in FREE'.
  inv FREE; inv FREE'.
  inv ME.
  split.
  constructor; simpl; intros; auto.
  - inv mi_inj; constructor; simpl; intros; auto.
    + rewrite Mem.perm_unchecked_free in H0; try reflexivity; auto.
       rewrite Mem.perm_unchecked_free; try reflexivity.
       destruct H0.
       split.
       intro; subst. exploit (iwb_inj _ _ _ IWB b b1); eauto.
       exploit iwb_o2o; eauto.
       eapply Mem.has_bounds_bounds; eauto.
       eapply Mem.has_bounds_bounds; eauto.
    + red in H0; red.
      rewrite Mem.unchecked_free_bounds' in *.
      repeat destr_in H0.
      * red in H0. simpl in H0. lia.
      * red in H0. simpl in H0.
        eapply Mem.has_bounds_bounds in Heqb0; eauto. rewrite Heqb0 in Heqp. inv Heqp.
        des (zeq z z); des (zeq z0 z0).
      * apply Mem.has_bounds_bounds in Heqb0. apply Mem.has_bounds_bounds in Heqb1.
        rewrite Heqb1.
        destr. subst.
        exploit iwb_inj. eauto. apply FB. apply H. intro; subst. destr.
        exploit iwb_o2o; eauto. intro; subst.
        eapply mi_bounds; eauto.
    + rewrite ! Mem.unchecked_free_mask. eauto.
    + eapply mi_memval; eauto.
      rewrite Mem.perm_unchecked_free in H0; try reflexivity; eauto. destr.
      eapply Mem.has_bounds_bounds; eauto.
    + generalize (unchecked_free_nb_boxes m b _ _ (Mem.has_bounds_bounds _ _ _ _ Heqb0)).
      generalize (unchecked_free_nb_boxes tm b' _ _ (Mem.has_bounds_bounds _ _ _ _ Heqb1)).
      intuition omega.
  - red; unfold Mem.unchecked_free; simpl.
    eapply mi_mappedblocks in H; eauto.
  - red. intros b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 diff FB1 FB2 IB1 IB2.
    red in IB1, IB2.
    rewrite Mem.unchecked_free_bounds' in *.
    rewrite (Mem.has_bounds_bounds _ _ _ _ Heqb0) in *.
    des (zeq lo lo); des (zeq hi hi).
    red in IB1, IB2.
    des (eq_block b1 b); des (eq_block b2 b); try omega.
    eapply mi_no_overlap'.
    2: eauto. 2: eauto. auto. red. red. omega.
    red; red; auto.
  - eapply mi_delta_pos; eauto.
  - specialize (mi_inj_dynamic _ _ _ H). des mi_inj_dynamic. des a.
    repSplit. eauto.
    intros. trim a0. auto. repSplit; destr.
    rewrite ! Mem.unchecked_free_bounds'.
    destr. subst. rewrite H in FB; inv FB. rewrite peq_true. des a0.
    rewrite e1. destr.
    destr. subst. trim e; destr. apply e in FB. destr.
    intros. apply e in H1; auto.
  - inv IWB; constructor; simpl; intros; eauto.
    + red in iwb_wb0 |- *. intros.
      rewrite <- ! Mem.size_block_snd, ! Mem.unchecked_free_bounds'.
      destr. rewrite Mem.unchecked_free_mask.
      rewrite Mem.size_block_snd. eauto.
    + rewrite <- ! Mem.size_block_snd, ! Mem.unchecked_free_bounds'.
      destr.
      * subst. assert (b' = b'0) by destr. subst.
        rewrite peq_true. apply Mem.has_bounds_bounds in Heqb1. rewrite Heqb1.
        apply Mem.has_bounds_bounds in Heqb0; rewrite Heqb0. auto.
      * assert (b' <> b'0). intro; subst. exploit iwb_inj0. apply H. apply FB. destr.
        destr. rewrite ! Mem.size_block_snd; eauto.
    + rewrite ! Mem.unchecked_free_mask. eauto.
Qed.

Lemma iwb_ext:
  forall j j' m tm (IWB: inj_well_behaved j m tm)
    (EXT: forall b, j b = j' b),
    inj_well_behaved j' m tm.
Proof.
  intros; inv IWB; constructor; simpl; intros; eauto.
  - red in iwb_o2o0 |- *; simpl; intros; eauto.
    eapply iwb_o2o0. rewrite EXT. eauto.
  - red in iwb_wb0 |- *; simpl; intros; eauto.
    eapply iwb_wb0. rewrite EXT; auto.
  - rewrite <- EXT in H; eauto.
  - rewrite <- EXT in H; eauto.
  - apply iwb_no_oota0 in H. dex. rewrite EXT in H; eauto.
  - rewrite <- EXT in *; eauto.
Qed.
Generated by coq2html