Module BlockAppears

Require Import Coqlib AST.

Require Import Values Values_symbolictype Values_symbolic ExprEval.
Require Import NormaliseSpec Integers.
Require Import Memdata Memory.

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

Proof.

  induction 1; simpl; intros; eauto.
  - des v1. subst. inv VI. congruence.
  - intro A; intuition try congruence; eauto.
Qed.

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.

Proof.

  induction e; simpl; intros; auto.
  - des v.
    rewrite same_other; auto.
  - erewrite IHe; eauto.
  - erewrite IHe1, IHe2; eauto.
Qed.

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.

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

Proof.

  intros. red in dep.
  destruct (block_appears_dec b e); auto.
  exfalso.
  destruct (Mem.exists_two_cms m b) as [cm [cm' [A [B [C D]]]]].
  specialize (dep _ A _ B C Normalise.dummy_em).
  exfalso. apply dep.
  eapply not_block_appears_same_eval; eauto.
Qed.

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

Proof.

  intros.
  eapply norm_unforgeable; eauto.
  unfold Mem.nat_mask; intros; eauto.
  instantiate (1:=o); rewrite <- MN; apply Normalise.norm_correct.
Qed.

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

Proof.

red; intros.
eapply dep_block_appears in H0; eauto.
Qed.

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

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

Proof.

  unfold sep_inj; simpl; intros.
  intro DEP.
  eapply SI; eauto.
  red; red; intros.
  specialize (DEP _ COMP _ COMP' SameB em).
  intro EQ. apply DEP.
  des chunk.
  rewrite EQ; auto.
  repeat destr.
Qed.