Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Floats.
Require Import compcert.common.Values.
Require Import compcert.common.Memory.

Require Import VST.msl.eq_dec.

Definition address : Type := (block * Z)%type.

Instance EqDec_block: EqDec block := eq_block.

Instance EqDec_address: EqDec address.
Proof.
(* Goal: EqDec address *)
 intros [b1 z1] [b2 z2].
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
 destruct (eq_dec b1 b2).
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
 destruct (Z.eq_dec z1 z2).
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
 left; congruence.
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
 right; congruence.
(* Goal: sumbool (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2)) (not (@eq address (@pair block Z b1 z1) (@pair block Z b2 z2))) *)
 right; congruence.
Qed.

Instance EqDec_int: EqDec int := Int.eq_dec.
Instance EqDec_float: EqDec float := Float.eq_dec.

Instance EqDec_val: EqDec val.
Proof.
(* Goal: EqDec val *)
 hnf. decide equality.
(* Goal: sumbool (@eq Int.int i i0) (not (@eq Int.int i i0)) *)
(* Goal: sumbool (@eq Int64.int i i0) (not (@eq Int64.int i i0)) *)
(* Goal: sumbool (@eq float f f0) (not (@eq float f f0)) *)
(* Goal: sumbool (@eq float32 f f0) (not (@eq float32 f f0)) *)
(* Goal: sumbool (@eq Ptrofs.int i i0) (not (@eq Ptrofs.int i i0)) *)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply Int.eq_dec.
(* Goal: sumbool (@eq Int64.int i i0) (not (@eq Int64.int i i0)) *)
(* Goal: sumbool (@eq float f f0) (not (@eq float f f0)) *)
(* Goal: sumbool (@eq float32 f f0) (not (@eq float32 f f0)) *)
(* Goal: sumbool (@eq Ptrofs.int i i0) (not (@eq Ptrofs.int i i0)) *)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply Int64.eq_dec.
(* Goal: sumbool (@eq float f f0) (not (@eq float f f0)) *)
(* Goal: sumbool (@eq float32 f f0) (not (@eq float32 f f0)) *)
(* Goal: sumbool (@eq Ptrofs.int i i0) (not (@eq Ptrofs.int i i0)) *)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply Float.eq_dec.
(* Goal: sumbool (@eq float32 f f0) (not (@eq float32 f f0)) *)
(* Goal: sumbool (@eq Ptrofs.int i i0) (not (@eq Ptrofs.int i i0)) *)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply Float32.eq_dec.
(* Goal: sumbool (@eq Int.int i i0) (not (@eq Int.int i i0)) *)
(* Goal: sumbool (@eq Int64.int i i0) (not (@eq Int64.int i i0)) *)
(* Goal: sumbool (@eq float f f0) (not (@eq float f f0)) *)
(* Goal: sumbool (@eq float32 f f0) (not (@eq float32 f f0)) *)
(* Goal: sumbool (@eq Ptrofs.int i i0) (not (@eq Ptrofs.int i i0)) *)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply Ptrofs.eq_dec. (* apply Int.eq_dec.*)
(* Goal: sumbool (@eq block b b0) (not (@eq block b b0)) *)
 apply eq_block.
Qed.

Definition adr_range (base: address) (size: Z) (loc: address) : Prop :=
 match base, loc with
 | (b, ofs) , (b', ofs') => b=b' /\ (ofs <= ofs' < ofs + size)
 end.

Lemma adr_range_dec: forall base n loc, {adr_range base n loc} + {~adr_range base n loc}.
Proof.
(* Goal: forall (base : address) (n : Z) (loc : address), sumbool (adr_range base n loc) (not (adr_range base n loc)) *)
unfold adr_range; intros.
(* Goal: sumbool (let (b, ofs) := base in let (b', ofs') := loc in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n)))) (not (let (b, ofs) := base in let (b', ofs') := loc in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n))))) *)
destruct base as [b z]; destruct loc as [b' z'].
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
destruct (eq_block b b').
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
subst b'.
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
destruct (zle z z').
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
destruct (zlt z' (z+n)).
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
left; auto.
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
right; intros [? ?]; omega.
(* Goal: sumbool (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b) (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
right; intros [? ?]; omega.
(* Goal: sumbool (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n)))) (not (and (@eq block b b') (and (Z.le z z') (Z.lt z' (Z.add z n))))) *)
right; intros [? ?]; unfold block in *; xomega.
Qed.

(*
Definition size_chunk (chunk: memory_chunk) : Z :=
  match chunk with
  | Mint8signed => 1
  | Mint8unsigned => 1
  | Mint16signed => 2
  | Mint16unsigned => 2
  | Mint32 => 4
  | Mfloat32 => 4
  | Mfloat64 => 8
  | Mfloat64al32 => 4
  end.
*)

Remark size_chunk_pos:
  forall chunk1, size_chunk chunk1 > 0.
Proof.
(* Goal: forall chunk1 : AST.memory_chunk, Z.gt (size_chunk chunk1) Z0 *)
  destruct chunk1; simpl; omega.
Qed.

Lemma zero_in_chunk: forall ch, 0 <= 0 < size_chunk ch.
Proof.
(* Goal: forall ch : AST.memory_chunk, and (Z.le Z0 Z0) (Z.lt Z0 (size_chunk ch)) *)
  intros; generalize (size_chunk_pos ch); omega.
Qed.

Hint Resolve zero_in_chunk : mem.

Definition range_overlap (base1: address) (sz1: Z) (base2: address) (sz2: Z) : Prop :=
  exists loc, adr_range base1 sz1 loc /\ adr_range base2 sz2 loc.

Definition adr_add (loc: address) (ofs: Z) : address := (fst loc, snd loc + ofs).

Definition val2adr (v: val) (l: address) : Prop :=
(*     match v with Vptr b ofs => l = (b, Int.unsigned ofs) | _ => False end.*)
     match v with Vptr b ofs => l = (b, Ptrofs.unsigned ofs) | _ => False end.

Lemma adr_range_non_zero: forall l1 n l2, adr_range l1 n l2 -> n > 0.
Proof.
(* Goal: forall (bl : block) (ofs : Z) (n : nat) (l : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) l), or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) l) (@eq address l (@pair block Z bl ofs)) *)
  intros.
(* Goal: Z.gt n Z0 *)
  unfold adr_range in H.
(* Goal: Z.gt n Z0 *)
  destruct l1, l2.
(* Goal: Z.gt n Z0 *)
  destruct (zlt 0 n); omega.
Qed.

Lemma adr_range_shift_1: forall bl ofs n l, adr_range (bl, ofs + 1) (Z.of_nat n) l -> adr_range (bl, ofs) (Z.of_nat (S n)) l.
Proof.
(* Goal: forall (bl : block) (ofs : Z) (n : nat) (l : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) l), or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) l) (@eq address l (@pair block Z bl ofs)) *)
  intros.
(* Goal: or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) l) (@eq address l (@pair block Z bl ofs)) *)
  destruct l.
(* Goal: or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) (@pair block Z b z)) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  unfold adr_range in *.
(* Goal: and (@eq block bl b) (and (Z.le ofs z) (Z.lt z (Z.add ofs (Z.of_nat (S n))))) *)
  rewrite Nat2Z.inj_succ.
(* Goal: or (and (@eq block bl b) (and (Z.le (Z.add ofs (Zpos xH)) z) (Z.lt z (Z.add (Z.add ofs (Zpos xH)) (Z.of_nat n))))) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  destruct H.
(* Goal: and (@eq block bl b) (and (Z.le ofs z) (Z.lt z (Z.add ofs (Z.succ (Z.of_nat n))))) *)
  repeat split; auto; omega.
Qed.

Lemma adr_range_S_split: forall bl ofs n l, adr_range (bl, ofs) (Z.of_nat (S n)) l -> adr_range (bl, ofs + 1) (Z.of_nat n) l \/ l = (bl, ofs).
Proof.
(* Goal: forall (bl : block) (ofs : Z) (n : nat) (l : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) l), or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) l) (@eq address l (@pair block Z bl ofs)) *)
  intros.
(* Goal: or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) l) (@eq address l (@pair block Z bl ofs)) *)
  destruct l.
(* Goal: or (adr_range (@pair block Z bl (Z.add ofs (Zpos xH))) (Z.of_nat n) (@pair block Z b z)) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  unfold adr_range in *.
(* Goal: or (and (@eq block bl b) (and (Z.le (Z.add ofs (Zpos xH)) z) (Z.lt z (Z.add (Z.add ofs (Zpos xH)) (Z.of_nat n))))) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  rewrite Nat2Z.inj_succ in H.
(* Goal: or (and (@eq block bl b) (and (Z.le (Z.add ofs (Zpos xH)) z) (Z.lt z (Z.add (Z.add ofs (Zpos xH)) (Z.of_nat n))))) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  destruct H.
(* Goal: or (and (@eq block bl b) (and (Z.le (Z.add ofs (Zpos xH)) z) (Z.lt z (Z.add (Z.add ofs (Zpos xH)) (Z.of_nat n))))) (@eq address (@pair block Z b z) (@pair block Z bl ofs)) *)
  subst bl.
(* Goal: or (and (@eq block b b) (and (Z.le (Z.add ofs (Zpos xH)) z) (Z.lt z (Z.add (Z.add ofs (Zpos xH)) (Z.of_nat n))))) (@eq address (@pair block Z b z) (@pair block Z b ofs)) *)
  destruct (zlt ofs z); [left | right].
  + split; auto; omega.
  + f_equal; omega.
Qed.
