Module ValRels

Require Import Coqlib Maps Integers Values Memdata AST Globalenvs.
Require Import Blockset Footprint FMemOpFP GMemory MemAux CUAST LDSimDefs Localize MemInterpolant val_casted FMemPerm.
Require Import Lia.


Inductive val_related (j: Bset.inj) : val -> val -> Prop :=
| rel_vundef: val_related j Vundef Vundef
| rel_int: forall i, val_related j (Vint i) (Vint i)
| rel_long : forall i, val_related j (Vlong i) (Vlong i)
| rel_float : forall f, val_related j (Vfloat f) (Vfloat f)
| rel_single : forall f, val_related j (Vsingle f) (Vsingle f)
| rel_ptr : forall b b' ofs, j b = Some b' -> val_related j (Vptr b ofs) (Vptr b' ofs).

Lemma val_related_incr:
  forall j j',
    inject_incr (Bset.inj_to_meminj j) (Bset.inj_to_meminj j') ->
    (forall v v', val_related j v v' -> val_related j' v v').

Lemma val_related_val_inject_strict:
  forall j v v',
    val_related j v v' <->
    val_inject_strict (Bset.inj_to_meminj j) v v'.

Inductive memval_related (j: Bset.inj) : memval -> memval -> Prop :=
| rel_undef: memval_related j Undef Undef
| rel_byte: forall b, memval_related j (Byte b) (Byte b)
| rel_frag: forall v v' q n, val_related j v v' -> memval_related j (Fragment v q n) (Fragment v' q n).
               
Lemma memval_related_memval_inject_strict:
  forall j mv mv',
    memval_related j mv mv' <-> memval_inject_strict (Bset.inj_to_meminj j) mv mv'.

Lemma inj_value_pointer:
  forall j b b' ofs bl ,
    Bset.inj_inject j ->
    j b = Some b' ->
    list_forall2 (memval_related j) bl (inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b' ofs)) ->
    bl = inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs).

Lemma G_arg_exists_arg_related:
  forall v Shared j,
    G_arg Shared v ->
    Bset.inject j Shared Shared ->
    exists v', val_related j v v'.

Lemma G_arg_exists_arg_related':
  forall v' Shared j,
    G_arg Shared v' ->
    Bset.inject j Shared Shared ->
    exists v, val_related j v v'.

Lemma G_args_exists_args_related:
  forall vl Shared j,
    G_args Shared vl ->
    Bset.inject j Shared Shared ->
    exists vl', list_forall2 (val_related j) vl vl'.

Lemma G_args_exists_args_related':
  forall vl' Shared j,
    G_args Shared vl' ->
    Bset.inject j Shared Shared ->
    exists vl, list_forall2 (val_related j) vl vl'.

Definition uop_val_related (uop: val -> val) : Prop :=
  forall j v v', val_related j v v' -> val_related j (uop v) (uop v').
Ltac solvuop := intros until v'; intros A; inv A; constructor; auto.
Definition uop_option_val_related (uop: val -> option val) : Prop :=
  forall j v v', val_related j v v' -> option_rel (val_related j) (uop v) (uop v').
Ltac solvuopopt := intros until v'; intros A; inv A; simpl; repeat econstructor; eauto;
                   try match goal with |- context[option_map _ ?x] => destruct x; repeat constructor; auto end.
Definition binop_val_related (bop: val -> val -> val) : Prop :=
  forall j v1 v1' v2 v2',
    Bset.inj_inject j ->
    val_related j v1 v1' ->
    val_related j v2 v2' ->
    val_related j (bop v1 v2) (bop v1' v2').
Ltac solvbinop := intros until v2'; intros INJECT A B; inv A; inv B; simpl;
                  repeat match goal with |- context[match ?x with _ => _ end] => destruct x end;
                  try constructor; try congruence; auto;
                  try (exfalso; match goal with H: ~ _ |- _ => apply H; subst; eapply INJECT; eauto end; fail).

Lemma offset_ptr_val_related: forall ofs, uop_val_related (fun v => Val.offset_ptr v ofs). Proof. solvuop. Qed.