Module ForgetNorm

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 PpsimplZ MemReserve.

Fixpoint nat_range' lo n : list nat :=
  match n with
    O => lo :: nil
  | S m => lo :: nat_range' (S lo) m
  end.

Definition nat_range lo hi : list nat :=
  if le_dec lo hi then nat_range' lo (hi-lo)%nat else nil.

Opaque minus.
Lemma nat_range_rew: forall lo hi,
    nat_range lo hi =
    if le_dec lo hi
    then lo :: nat_range (S lo) hi
    else nil.

Definition concat {A} := fold_right (@app A) nil.

Fixpoint remove_dbl {A} (D: forall (a b: A), {a = b} + {a <> b}) l :=
  match l with
    nil => nil
  | a::r => if in_dec D a r then remove_dbl D r
           else a :: remove_dbl D r
  end.

Definition box_range cm (bz : block * Z) :=
  let (b,sz) := bz in
  if zlt 0 sz
  then nat_range (Z.to_nat (Int.unsigned (cm b) / 8))
                 (Z.to_nat ((Int.unsigned (cm b) + sz - 1) / 8))
  else nil.

Definition nb_boxes_used_cm m (cm : block -> int) : nat :=
  length
    (remove_dbl eq_nat_dec (concat (map (box_range cm) (Mem.mk_block_list m)))).

Lemma alloc_compat' : forall m l,
    Mem.is_block_list (Mem.mem_blocksize m) (pred (Pos.to_nat (Mem.nextblock m))) l ->
    { al : block -> nat |
      Mem.mk_cm l (Mem.nb_extra m) = Some al /\ Mem.compat_m m Mem.M31 (Mem.box_alloc_to_cm al) }.

Definition canon_cm (m:mem) : block -> int.

Lemma nat_range_same:
  forall n,
    nat_range n n = n :: nil.
Opaque Z.mul.

Lemma canon_cm_mul8:
  forall m b,
    exists k,
      Int.unsigned (canon_cm m b) = 8 * k.

Lemma int_and_two_p_m1_mul:
  forall i n,
    (0 <= n <= MA)%nat ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      i = Int.mul (Int.repr (two_power_nat n)) k.

Lemma int_and_two_p_m1_mul_Z:
  forall i n,
    (n <= MA)%nat ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      Int.unsigned i = (two_power_nat n) * k.


Lemma canon_cm_box_range:
  forall cm m b z,
    Mem.compat_m m Mem.M32 cm ->
    0 < z -> z = Mem.size_block m b ->
    length (box_range cm (b,z)) = length (box_range (canon_cm m) (b,z)).

Lemma canon_cm_box_range':
  forall cm m b z,
    Mem.compat_m m Mem.M32 cm ->
    z = Mem.size_block m b ->
    length (box_range cm (b,z)) = length (box_range (canon_cm m) (b,z)).

Lemma nat_range'_range:
  forall n lo b,
    (In b (nat_range' lo n) ->
     (lo <= b <= lo + n)%nat).

Lemma nat_range_range:
  forall lo hi b,
    (In b (nat_range lo hi) ->
     (lo <= b <= hi)%nat).

Lemma range_nat_range':
  forall n lo b,
    (lo <= b <= lo + n)%nat ->
    In b (nat_range' lo n).

Lemma range_nat_range_range:
  forall lo hi b,
    (lo <= b <= hi)%nat ->
    In b (nat_range lo hi).

Lemma lnr_nat_range':
  forall n lo,
    list_norepet (nat_range' lo n).

Lemma lnr_nat_range:
  forall lo hi,
    list_norepet (nat_range lo hi).

Lemma lnr_box_range:
  forall m a,
    list_norepet (box_range (canon_cm m) a).

Lemma two_p_div_rew:
  forall n m (LE: (m <= n)%nat)
    x y,
    (two_power_nat n * x +y) / two_power_nat m =
    (two_power_nat n * x) / two_power_nat m + y / two_power_nat m.

Lemma two_p_div_rew':
  forall n m (LE: (m <= n)%nat) x,
    (two_power_nat n * x) / two_power_nat m =
    (two_power_nat (n - m) * x).

Lemma in_concat:
  forall {A} l (x:A),
    In x (concat l) <-> exists l', In l' l /\ In x l'.

Lemma lnr_canon:
  forall m,
    list_norepet (concat (map (box_range (canon_cm m)) (Mem.mk_block_list m))).

Lemma lnr_remove:
  forall l,
    list_norepet l ->
    remove_dbl eq_nat_dec l = l.

Lemma length_concat:
  forall {A} (l: list (list A)),
    length (concat l) = fold_right Peano.plus O (map (@length A) l).

Lemma length_remove:
  forall l,
    (length (remove_dbl eq_nat_dec l) <= length l)%nat.

Lemma eq_le: forall (n m: nat), n = m -> (n <= m)%nat.

Lemma canon_cm_more_boxes:
  forall cm m,
    Mem.compat_m m Mem.M32 cm ->
    (nb_boxes_used_cm m cm <= nb_boxes_used_cm m (canon_cm m))%nat.

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
  }.


Lemma in_bl:
  forall m b1 z1
    (i: In (b1, z1) (Mem.mk_block_list m)),
    (Pos.to_nat b1 <= pred (Pos.to_nat (Mem.nextblock m)))%nat.

Lemma nin_list_ints:
  forall n m (ME: (m > n)%nat),
    ~
      In (Pos.of_nat m)
      (map (fun x : nat => Pos.of_nat x) (Alloc.list_ints n)).


Lemma lnr_mbl:
  forall m,
    list_norepet (map fst (Mem.mk_block_list m)).

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),
    let (l1,l2) := partition (is_injected f) (Mem.mk_block_list m1) in
    Permutation (Mem.mk_block_list m1) (l1 ++ l2) ->
    Permutation
      (map fst (Mem.mk_block_list m2))
      (filter_map (fun b : block =>
                     match f b with
                       Some (b',delta) => Some b'
                     | None => None
                     end) (map fst (Mem.mk_block_list m1))).



Definition box_range' m cm b :=
  let sz := (Mem.size_block m b) in
  box_range cm (b,sz).

Lemma box_range'_eq:
  forall cm m,
  map (box_range cm) (Mem.mk_block_list m) =
  map (box_range' m cm) (map fst (Mem.mk_block_list m)).

Lemma perm_concat:
  forall {A} (l l': list (list A)) (P: list_forall2 (@Permutation A) l l'),
    Permutation (concat l) (concat l').

Lemma fold_right_plus_permut:
  forall l l' (P: Permutation l l'),
    fold_right Peano.plus O l = fold_right Peano.plus O l'.

Lemma fold_right_plus_app:
  forall l l' ,
    fold_right Peano.plus O (l ++ l') = (fold_right Peano.plus O l + fold_right Peano.plus O l')%nat.

Lemma filter_map_ext:
  forall {A B} (f f': A -> option B) l
    (EXT: forall x, In x l -> f x = f' x),
    filter_map f l = filter_map f' l.

Lemma partition_l:
  forall {A} (l: list A) f ll lr,
    partition f l = (ll,lr) ->
    ll = filter_map (fun b => if f b then Some b else None) l.

Lemma map_filter_map:
  forall {A B C D}
    (f: B -> C) (g: A -> option B)
    (f': A -> D) (g': D -> option C)
    (EQ: forall a b, g a = Some b -> exists c, g' (f' a) = Some c /\ f b = c)
    (EQ': forall a c, g' (f' a) = Some c -> exists b, g a = Some b)
    (l: list A),
    map f (filter_map g l) = filter_map g' (map f' l).

Lemma map_filter_map':
  forall {A B C} (g: A -> option B) (f: B -> C) l,
    map f (filter_map g l) = filter_map (fun x => match g x with
                                                 Some gx => Some (f gx)
                                               | None => None
                                               end) l.

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))
  ,
      (length ((concat (map (box_range (canon_cm m2)) (Mem.mk_block_list m2)))) +
       fold_right Peano.plus O (map (fun x => length (box_range' m1 (canon_cm m1) x)) (map fst l1)))%nat =
      length (concat (map (box_range (canon_cm m1)) (Mem.mk_block_list m1))).

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) + fold_right Peano.plus O (map (fun x => length (box_range' m1 (canon_cm m1) x)) (map fst l1)) = nb_boxes_used_cm m1 (canon_cm m1))%nat.


Lemma length_box_range_canon_cm:
  forall m b z, 0 < z ->
    length (box_range (canon_cm m) (b,z)) = (S (Z.to_nat ((z - 1)/ 8))).

Lemma nb_boxes_used_cm_nb_boxes_used_m:
  forall m,
    (nb_boxes_used_cm m (canon_cm m) <= Mem.nb_boxes_used_m m * NPeano.pow 2 (MA-3))%nat.

Definition has_free_boxes m cm N :=
  (nb_boxes_used_cm m cm + N < Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA-3))%nat.

Lemma mult_lt_le_mono:
  forall (a b c d: nat),
    (a < c)%nat -> (O < b <= d)%nat ->
    (a * b < c * d)%nat.

Definition nb_boxes8_max := (Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA - 3))%nat.

Definition get_free_boxes m cm :=
  fold_left
    (fun (acc: list nat) b =>
       filter (fun x => negb (in_dec eq_nat_dec x (box_range' m cm b))) acc)
    (map fst (Mem.mk_block_list m))
    (list_ints nb_boxes8_max).

Lemma in_fold_left_filter:
  forall {A B} (f: A -> B -> bool) l lacc x ,
    In x (fold_left (fun acc b => filter (f b) acc) l lacc) ->
    In x lacc /\ Forall (fun y => f y x = true) l.

Lemma in_gfb:
  forall x m cm ,
    In x (get_free_boxes m cm) ->
    In x (list_ints nb_boxes8_max) /\
    Forall (fun y => negb (in_dec eq_nat_dec x (box_range' m cm y)) = true) (map fst (Mem.mk_block_list m)).

Lemma below_in_list_ints:
  forall m b0,
    (0 < b0 <= m)%nat ->
    In b0 (list_ints m).

Lemma below_in_list_ints':
  forall m b0,
    In b0 (list_ints m) ->
    (0 < b0 <= m)%nat.

Lemma list_ints_In:
  forall m b,
    In b (list_ints m) <-> (0 < b <= m)%nat.

Lemma box_span_mu:
  (Mem.box_span Int.max_unsigned - 2)%nat = Z.to_nat Mem.nb_boxes_max.


Lemma in_gfb':
  forall x m cm ,
    Mem.compat_m m Mem.M32 cm ->
    In x (get_free_boxes m cm) ->
    (0 < x <= nb_boxes8_max)%nat /\
    forall b o o',
      Mem.in_bound_m (Int.unsigned o) m b ->
      0 <= Int.unsigned o' < 8 ->
      Int.unsigned (Int.add (cm b) o) <> Int.unsigned (Int.add (Int.repr (8 * Z.of_nat x)) o').


Lemma nin_list_ints' : forall n m : nat,
    (m > n)%nat -> ~ In m (list_ints n).

Lemma lnr_list_ints:
  forall n,
    list_norepet (list_ints n).


Lemma lnr_gfb:
  forall m cm,
    list_norepet (get_free_boxes m cm).


Lemma in_gfb_addrspace:
  forall x m cm ,
    In x (get_free_boxes m cm) ->
    forall o, 0 <= Int.unsigned o < 8 -> 0 < (8 * Z.of_nat x) + Int.unsigned o < Int.max_unsigned.

Lemma list_ints_length:
  forall n,
    length (list_ints n) = n.

Lemma filter_filter:
  forall {A} f f' (l: list A),
    filter f (filter f' l) = filter (fun x => f x && f' x) l.

Lemma filter_ext:
  forall {A} f f' (EXT: forall x, f x = f' x) (l: list A),
    (filter f l) = (filter f' l).

Lemma filter_true:
  forall {A} (l: list A),
    filter (fun x => true) l = l.

Lemma get_free_boxes_filter:
  forall m cm,
  Permutation
    (get_free_boxes m cm)
    (filter
       (fun box => negb
                  (existsb
                     (fun b => in_dec eq_nat_dec box (box_range' m cm b))
                     (map fst (Mem.mk_block_list m))))
       (list_ints nb_boxes8_max)).


Lemma remove_dbl_In:
  forall {A} D (l: list A) a,
    (In a l <-> In a (remove_dbl D l)).

Lemma remove_dbl_lnr:
  forall {A} D (l: list A),
    list_norepet (remove_dbl D l).


Lemma get_used_boxes_filter:
  forall m cm (COMP: Mem.compat_m m Mem.M32 cm),
    Permutation (remove_dbl eq_nat_dec (concat (map (box_range cm) (Mem.mk_block_list m))))
                (filter (fun x : nat => existsb (fun b : block => in_dec eq_nat_dec x (box_range' m cm b)) (map fst (Mem.mk_block_list m)))
                        (list_ints nb_boxes8_max ++ O :: nat_range (S nb_boxes8_max) (Z.to_nat (Int.max_unsigned / 8)))).


Lemma length_filters:
  forall {A} f (l: list A),
    length l = length (filter f l ++ filter (fun x => negb (f x)) l).

Lemma length_get_free_boxes:
  forall m cm,
    Mem.compat_m m Mem.M32 cm ->
    (Z.to_nat Mem.nb_boxes_max * NPeano.pow 2 (MA - 3) <= length (get_free_boxes m cm) + nb_boxes_used_cm m cm)%nat.

Lemma has_free_boxes_correct:
  forall m cm n,
    Mem.compat_m m Mem.M32 cm ->
    has_free_boxes m cm n ->
    exists l,
      (length l >= n)%nat /\
      list_norepet l /\
      Forall (fun z : Z => forall b o o',
                  Mem.in_bound_m (Int.unsigned o) m b ->
                  0 <= Int.unsigned o' < 8 ->
                  Int.unsigned (Int.add (cm b) o) <> Int.unsigned (Int.add (Int.repr z) o')) l /\
      Forall (fun z => forall o, 0 <= Int.unsigned o < 8 -> 0 < z + Int.unsigned o < Int.max_unsigned) l /\
      Forall (fun z => exists k, z = 8 * k) l.


Lemma list_nth_z_succeeds:
  forall {A} (l: list A) n,
    0 <= n < Z.of_nat (length l) ->
    exists x, list_nth_z l n = Some x.

Fixpoint find {A} (eq_dec: forall (a b: A), {a = b} + {a <> b}) x l :=
  match l with
    nil => None
  | a :: r => if eq_dec a x then Some O else option_map S (find eq_dec x r)
  end.


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).

Lemma in_map_filter:
  forall {A B} b0 (f: A -> option B) l,
    In b0 (filter_map f l) <->
    (exists a0, In a0 l /\ f a0 = Some b0).

Lemma find_in:
  forall {A} eq_dec l (x:A),
    In x l ->
    exists n, find eq_dec x l = Some n /\
         (n < length l)%nat.

Lemma lnr_list_nth_z_diff:
  forall {A} (l: list A) (LNR: list_norepet l)
    n1 n2 (d: n1 <> n2)
    x1 x2
    (NTH1: list_nth_z l n1 = Some x1)
    (NTH2: list_nth_z l n2 = Some x2),
    x1 <> x2.

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).

Lemma find_diff_diff:
  forall {A} E (a1 a2:A) (d: a1 <> a2) l n1 n2,
    find E a1 l = Some n1 ->
    find E a2 l = Some n2 ->
    n1 <> n2.

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)).

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
.

Lemma find_some_range:
  forall {A} E (x:A) l n,
    find E x l = Some n ->
    0 <= Z.of_nat n < Z.of_nat (length l).

Lemma nb_boxes_max_pos:
  0 <= Mem.nb_boxes_max.


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').

Definition depends_m (m: mem) (e: expr_sym) (b: block) :=
  depends Int.max_unsigned (Mem.bounds_of_block m) (Mem.nat_mask m) e b.

Definition sep_inj (m: mem) (f: meminj) e :=
  forall b, f b = None -> ~ depends_m m e b.

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).

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')).

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.

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.

Lemma expr_inj_not_dep:
  forall f v v'
    (EI: expr_inj f v v') b
    (Fb: f b = None), ~ block_appears v b.

Lemma not_block_appears_same_eval:
  forall e b (NA: ~ block_appears e b),
  forall cm cm'
    (diff_b: cm b <> cm' b)
    (same_other : forall b' : block, b <> b' -> cm b' = cm' b'),
  forall em,
    eSexpr cm em e = eSexpr cm' em e.

Lemma dep_block_appears:
  forall m e b
    (dep: depends_m m e b),
    block_appears e b.

Lemma norm_unforgeable:
  forall m e b o
    (MN: Mem.mem_norm m e = Vptr b o),
    depends_m m e b.

Lemma dep_block_appears':
  forall m
    (e : expr_sym) (b : block),
    ~ block_appears e b -> ~ depends_m m e b.

Lemma list_ints_le:
  forall m n,
    (0 < n <= m)%nat ->
    In n (Alloc.list_ints m).

Remark filter_charact:
  forall (A: Type) (f: A -> bool) x l,
  In x (List.filter f l) <-> In x l /\ f x = true.

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.

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.

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.

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.

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.

Lemma sep_inj_load_result:
  forall f m v (SI: sep_inj m f v)
    chunk, sep_inj m f (Val.load_result chunk v).

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'.

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'.

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.