Module MemInterpolant

Require Import Coqlib Values Globalenvs
        Blockset Footprint GMemory Memory MemAux.

Require Import LDSimDefs LDSim LDSim_local.

Require Import Maps FiniteMaps.


Lemma ptrofs_add_0:
  forall ofs, Integers.Ptrofs.add ofs (Integers.Ptrofs.repr 0) = ofs.

Lemma inj_to_meminj_some:
  forall j b b' delta, Bset.inj_to_meminj j b = Some (b', delta) ->
                  j b = Some b' /\ delta = 0.

Lemma eq_valid_eq_nextblock:
  forall m m',
    (forall b, Mem.valid_block m b <-> Mem.valid_block m' b) ->
    Mem.nextblock m = Mem.nextblock m'.

Lemma mem_access_default:
  forall m ofs K, fst (Mem.mem_access m) ofs K = None.


Inductive val_inject_strict (mi: meminj) : val -> val -> Prop :=
  inject_int : forall i : Integers.Int.int, val_inject_strict mi (Vint i) (Vint i)
| inject_long : forall i : Integers.Int64.int, val_inject_strict mi (Vlong i) (Vlong i)
| inject_float : forall f : Floats.float, val_inject_strict mi (Vfloat f) (Vfloat f)
| inject_single : forall f : Floats.float32, val_inject_strict mi (Vsingle f) (Vsingle f)
| inject_ptr : forall (b1 : block) (ofs1 : Integers.Ptrofs.int) (b2 : block)
                 (ofs2 : Integers.Ptrofs.int) (delta : BinNums.Z),
    mi b1 = Some (b2, delta) ->
    ofs2 = Integers.Ptrofs.add ofs1 (Integers.Ptrofs.repr delta) ->
    val_inject_strict mi (Vptr b1 ofs1) (Vptr b2 ofs2)
| val_inject_undef : val_inject_strict mi Vundef Vundef.

Inductive memval_inject_strict (f: meminj) : memval -> memval -> Prop :=
  memval_inject_byte': forall n, memval_inject_strict f (Byte n) (Byte n)
| memval_inject_frag': forall v1 v2 q n, val_inject_strict f v1 v2 ->
                                    memval_inject_strict f (Fragment v1 q n) (Fragment v2 q n)
| memval_inject_undef': memval_inject_strict f Undef Undef.

Lemma memval_eq_inject_strict_eq:
  forall mi mv mv1 mv2,
    memval_inject_strict mi mv mv1 ->
    memval_inject_strict mi mv mv2 ->
    mv1 = mv2.

Lemma memval_eq_inject_strict_eq':
  forall j mv1 mv2 mv,
    Bset.inj_inject j ->
    memval_inject_strict (Bset.inj_to_meminj j) mv1 mv ->
    memval_inject_strict (Bset.inj_to_meminj j) mv2 mv ->
    mv1 = mv2.
        
Lemma finite_bset_inject_revert:
  forall j (bs bs': Bset.t) bound
    (FINITE: forall b, bs b -> Plt b bound),
    Bset.inject j bs bs' ->
    exists j', Bset.inject j' bs' bs /\
          (forall b b', j b = Some b' <-> j' b' = Some b).


Lemma bset_inject_revert:
  forall j bound,
    let bs := (fun b => Plt b bound) in
    Bset.inject j bs bs ->
    exists j', Bset.inject j' bs bs /\
          (forall b b', j b = Some b' <-> j' b' = Some b).






Lemma memval_inject_strict_revert:
  forall j j',
    (forall b b', j b = Some b' <-> j' b' = Some b) ->
    forall v v',
      memval_inject_strict (Bset.inj_to_meminj j) v v' ->
      memval_inject_strict (Bset.inj_to_meminj j') v' v.

Definition inject_value (j: Bset.inj) (v: val) : val :=
  match v with
  | Vptr b ofs =>
    match j b with
    | Some b' => Vptr b' ofs
    | None => Vundef
    end
  | _ => v
  end.

Lemma inject_value_func_wd:
  forall (j: Bset.inj) v,
    G_arg (fun b => if j b then True else False) v ->
    val_inject_strict (Bset.inj_to_meminj j) v (inject_value j v) .

Definition inject_memval (j: Bset.inj) (mv: memval) : memval :=
  match mv with
  | Undef => Undef
  | Byte n => Byte n
  | Fragment v q n => Fragment (inject_value j v) q n
  end.

Definition G_memval (bs: Bset.t) (mv: memval) : Prop :=
  match mv with
  | Fragment v _ _ => G_arg bs v
  | _ => True
  end.

Lemma inject_memval_func_wd:
  forall (j: Bset.inj) mv,
    G_memval (fun b => if j b then True else False) mv ->
    memval_inject_strict (Bset.inj_to_meminj j) mv (inject_memval j mv).

Definition inject_zmap_memval (j: Bset.inj) (m: ZMap.t memval) (z: Z) : memval :=
  (inject_memval j (ZMap.get z m)).

Program Definition inject_zmap_memval_c (j: Bset.inj) (m: ZMap.t memval) :=
  @zmap_construct_c memval (fun z => inject_zmap_memval j m z)
                    (fst (zmap_finite_c memval m)) (snd (zmap_finite_c memval m))
                    (inject_memval j (fst m)) _.


Definition inject_content (j j': Bset.inj) (bound: block)
           (original_content update_content: PMap.t (ZMap.t memval))
           (b: block) : ZMap.t memval :=
  if plt b bound
  then
    match j b with
    | Some b' => proj1_sig (inject_zmap_memval_c j' (update_content!!b'))
    | _ => original_content!!b
    end
  else
    original_content!!b
.

Program Definition inject_content_c (j j': Bset.inj) (bound: block)
        (original_content update_content: PMap.t (ZMap.t memval)) :=
  pmap_construct_c
    _ (fun b => inject_content j j' bound original_content update_content b)
    (Pos.max (pmap_finite_c _ original_content) bound)
    (fst original_content) _.




Definition update_access_func (j: Bset.inj) (bound: block)
           (m2 m1': PMap.t (Z -> perm_kind -> option permission))
           (b: block) : Z -> perm_kind -> option permission :=
  if plt b bound then
    match j b with
    | Some b' => m1' !! b'
    | None => m2 !! b
    end
  else m2 !! b.

Program Definition update_access_c (j: Bset.inj) (bound: block)
        (m2 m1' : PMap.t (Z -> perm_kind -> option permission)) :=
  pmap_construct_c _ (update_access_func j bound m2 m1')
                   (Pos.max (pmap_finite_c _ m2) bound) (fst m2) _.

Program Definition update_memory (j21 j12: Bset.inj) (bound: block)
        (m2 m1': Mem.mem) : Mem.mem :=
  Mem.mkmem (proj1_sig (inject_content_c j21 j12 bound (Mem.mem_contents m2) (Mem.mem_contents m1')))
            (proj1_sig (update_access_c j21 bound (Mem.mem_access m2) (Mem.mem_access m1')))
            (Pos.max (Mem.nextblock m2) bound)
            _ _ _.