Require Import ZArith.
Require Import util.
Require Import util_tactic.
Require Import List.
Require Import machine_int.
Import MachineInt.
Require Import machine_int_spec.
Require Import state.
Require Import mips.
Require Import sum.
Require Import Min.
Open Local Scope asm_heap_scope.
Open Local Scope mips_scope.
Open Local Scope Z_scope.

Ltac Decompose_sepcon id h1 h2:=
  let X := fresh in (inversion_clear id as [h1 X]; 
    (let Y:= fresh in (inversion_clear X as [h2 Y]; decompose [and] Y; clear Y))).

Ltac Compose_sepcon id1 id2:=
  exists id1; exists id2; split; [Disjoint_heap | (split;[ (Equal_heap) | split; idtac])].

Ltac Intro_sepimp id1 id2 := red; intro id1; intro X; inversion_clear X; intro id2; intro.

(*
 * Monotony/Adjunction tactics
 *) 

Ltac assocs_sepcon :=
  match goal with
    | |- ?P -> _  => 
      repeat rewrite sep.con_assoc_equiv
  end.

Ltac rotate_sepcon :=
  match goal with
    | |- ?P -> _ =>
      rewrite sep.con_com_equiv;
	assocs_sepcon
  end.

Ltac try_monotony :=
match goal with
  | |- (?P ** ?PP) ?S ?SS ?M ?H -> (?P ** ?QQ) ?S ?SS ?M ?H => 
    apply monotony; split; [intros; auto | intros; idtac]
  | |- (?P ** ?PP) ?S ?SS ?M ?H -> (?Q ** ?QQ) ?S ?SS ?M ?H => 
    rotate_sepcon; try_monotony
end.

Ltac Monotony Hyp :=
  generalize Hyp; clear Hyp; try_monotony.

Ltac Adjunction Hyp :=
  generalize Hyp; clear Hyp; apply adjunction; intros.

Ltac Rewrite_u2Z_unfold :=
    unfold zero16;
      unfold zero32;
	unfold one16;
	  unfold one32;
	    unfold four16;
	      unfold four32;
		unfold shl2.

Lemma u2Z_sign_extend_imm_val : forall x, 0 <= x < Zpower 2 15 ->
  u2Z (sign_extend_16_32 (Z2u 16 x)) = x.
  intros.
  unfold sign_extend_16_32.
  rewrite sign_extend_Z2u.
  rewrite Z2u_injection.
  auto.
  split.
  omega.
  apply Zlt_trans with (Zpower 2 15).
  intuition.
  apply Zpower_2_lt.
  omega.
  omega.
  intuition.
Qed.

Lemma gpr_gpr_zero_u2Z: forall s,
  u2Z (gpr.lookup gpr_zero s) = 0.
  intros.
  rewrite gpr.gpr_zero_zero32.
  unfold zero32.
  rewrite Z2u_injection.
  auto.
  generalize (Zpower_1 32); omega.
Qed.

Lemma shl_u2Z_tmp: forall (L l: nat) (x: int L),
  (l <= L)%nat ->
  u2Z x < Zpower 2 (L - l) -> u2Z (shl l x) = u2Z x * Zpower 2 l.
  intros.
  eapply shl_u2Z with (L - l)%nat.
  omega.
  auto.
Qed.

Ltac Rewrite_u2Z_uexpr e :=
  match e with
      (* compound expression *)
    | u2Z (?e1 (+) ?e2) => rewrite (add_u2Z e1 e2); 
        [Rewrite_u2Z_uexpr (u2Z e1); Rewrite_u2Z_uexpr (u2Z e2) (*new goal*) | 
	  Rewrite_u2Z_Zexpr (*constraint: overflow?*) ]
    | u2Z (shl ?n ?e) => rewrite (shl_u2Z_tmp _ n e);
        [simpl (Zpower 2 n); Rewrite_u2Z_uexpr (u2Z e) (*new goal*) | 
	  repeat constructor (*nat inequality: do not shift more than the length of the int*) |
	    simpl minus; Rewrite_u2Z_Zexpr (*constraint: the shifted value does not overflow*) ]
    | u2Z (umul ?e1 ?e2) => rewrite (umul_u2Z e1 e2);
      Rewrite_u2Z_uexpr (u2Z e1); Rewrite_u2Z_uexpr (u2Z e2)
    | u2Z (zero_extend_u2Z ?n ?e) => rewrite (zero_extend_u2Z n e);
      Rewrite_u2Z_uexpr (u2Z e)
      (* atoms *)
    | u2Z (Z2u ?l ?z) => rewrite Z2u_injection;
      [idtac (*new goal*) |
	idtac (*constraint: 0 <= z < Zpower 2 l*)]
    | u2Z (sign_extend_16_32 (Z2u 16 ?c)) => rewrite (u2Z_sign_extend_imm_val c);
      [idtac (*new goal*) |
	idtac (*constraint: 0 <= c < Zpower 2 15*)]
    | u2Z (gpr.lookup gpr_zero ?s) => rewrite (gpr_gpr_zero_u2Z s)
      (* don't know cases *)
    | _ => idtac
  end
  with Rewrite_u2Z_Zexpr :=
  match goal with 
    | |- (u2Z (?e1) = u2Z (?e2))  => Rewrite_u2Z_uexpr (u2Z e1); try Rewrite_u2Z_uexpr (u2Z e2)
    | |- (u2Z (?e1) = _) => Rewrite_u2Z_uexpr (u2Z e1)
    | |- (u2Z (?e1) < _) => Rewrite_u2Z_uexpr (u2Z e1)
    | |- (u2Z (?e1) <= _) => Rewrite_u2Z_uexpr (u2Z e1)
    | |- (u2Z (?e1) *  _ = _) => Rewrite_u2Z_uexpr (u2Z e1)
    | |- (u2Z (?e1) + u2Z (?e2) < _) => Rewrite_u2Z_uexpr (u2Z e1); Rewrite_u2Z_uexpr (u2Z e2)
  end.

Require Import listbit.
Import ListBit.
Require Import listbit_correct.
Require Import Max.

Definition pos_lt (a b:positive) : bool :=
  let a' := rev (pos2lst a) in
    let b' := rev (pos2lst b) in
      let max_len := max (length a') (length b') in
	let a'' := zero_extend_lst (max_len - length a') a' in
	  let b'' := zero_extend_lst (max_len - length b') b' in
	    listbit_lt a'' b''.

Lemma pos_lt_correct' : forall p q,
  pos_lt p q = true -> Zpos p < Zpos q.
  intros.
  rewrite <-ulst2Z_rev_poslst.
  rewrite <-ulst2Z_rev_poslst.
  rewrite <-(zero_extend_lst_correct
    (max (length (rev (pos2lst p))) (length (rev (pos2lst q))) - length (rev (pos2lst p)))
    (rev (pos2lst p))).
  rewrite <-(zero_extend_lst_correct
    (max (length (rev (pos2lst p))) (length (rev (pos2lst q))) - length (rev (pos2lst q)))
    (rev (pos2lst q))).
  apply listbit_lt_correct'; auto.
Qed.

Definition Z_lt (a b:Z) : bool :=
  match a with
    Z0 => match b with
	    Z0 => false
	    | Zpos _ => true
	    | Zneg _ => false
	  end
    | Zpos p => match b with
		  Z0 => false
		  | Zpos q => pos_lt p q
		  | Zneg _ => false
		end
    | Zneg p => match b with
		  Z0 => true
		  | Zpos _ => true
		  | Zneg q => pos_lt q p
		end
  end.

Lemma Z_lt_correct : forall a b,
  Z_lt a b = true -> a < b.
  destruct a; destruct b; intros; try discriminate.
  generalize (Zgt_pos_0 p); omega.
  simpl in H.
  apply pos_lt_correct'; auto.
  generalize (Zlt_neg_0 p); omega.
  apply Zlt_neg_pos.
  simpl in H.
  generalize (pos_lt_correct' _ _ H); intro.
  rewrite <-Zopp_neg in H0.
  rewrite <-Zopp_neg in H0.
  omega.
Qed.

Lemma Z_le_correct : forall a b,
  Z_lt a b = true \/ a = b -> a <= b.
  intros.
  inversion_clear H.
  generalize (Z_lt_correct _ _ H0); intro.
  omega.
  subst a.
  apply Zle_refl.
Qed.

Lemma Zgt_pos_0' : forall p, 0 < Zpos p.
  intros.
  generalize (Zgt_pos_0 p); omega.
Qed.

Lemma Zle_neg_0 : forall p, Zneg p <= 0.
  intros.
  generalize (Zlt_neg_0 p); omega.
Qed.

Lemma Zpower_0' : forall n, 0 <= Zpower 2 n.
  intros.
  apply Zle_trans with 1.
  apply Z_le_correct; simpl; auto.
  apply Zpower_1.
Qed.

Lemma Zbeta_0' : forall n, 0 <= Zbeta n.
  intros.
  apply Zle_trans with 1.
  apply Z_le_correct; simpl; auto.
  apply Zbeta_1.
Qed.


Ltac Constraint_constant :=
  match goal with
    | |- (?z <= ?z) => apply Zle_refl
    | |- (0 < Zpower 2 ?n) => apply Zpower_0
    | |- (0 < Zbeta ?n) => apply Zbeta_0
    | |- (0 <= Zpower 2 ?n) => apply Zpower_0'
    | |- (0 <= Zbeta ?n) => apply Zbeta_0'
    | |- (0 <= Z_of_nat ?n) => apply Zle_0_nat
      (* inequalities between two constants *)
    | |- (Zneg _ < Zpos _) => apply Zlt_neg_pos
    | |- (Zneg _ <= Zpos _) => apply Zle_neg_pos
    | |- (Zneg _ < Z0) => apply Zlt_neg_0
    | |- (Zneg _ <= Z0) => apply Zle_neg_0
    | |- (Z0 < Zpos _) => apply Zgt_pos_0'
    | |- (Z0 <= Zpos _) => apply Zle_0_pos
    | |- (Zpos _ < Zpos _) => apply Z_lt_correct; simpl; auto
    | |- (Zpos _ <= Zpos _) => apply Z_le_correct; simpl; auto
    | |- (Zneg _ < Zneg _) => apply Z_lt_correct; simpl; auto
    | |- (Zneg _ <= Zneg _) => apply Z_le_correct; simpl; auto
    | |- (Zneg _ < Zpower 2 ?n) => simpl; Constraint_constant
    | |- (Zneg _ <= Zpower 2 ?n) => simpl; Constraint_constant
    | |- (Zpos _ < Zpower 2 ?n) => simpl; Constraint_constant
    | |- (Zpos _ <= Zpower 2 ?n) => simpl; Constraint_constant
  end.

Ltac Rewrite_u2Z :=
  Rewrite_u2Z_unfold;
  Rewrite_u2Z_Zexpr.

Ltac Nat2Z :=
  match goal with 
    |- (_ < power 2 ?n)%nat =>
      apply Z_of_nat_lt_inj; rewrite <-Zpower_power
  end.

Ltac Mult n :=
  match goal with
    | |- (_ < Zpower 2 ?m) =>
      apply Zmult_gt_0_lt_reg_r with (Zpower 2 n);
	[simpl (*new goal*) | 
	  rewrite <-Zpower_is_exp; simpl plus; simpl (Zpower 2 n) (*multiply the rhs by some power*)]
  end.

Ltac Clean_beta1 :=
  match goal with
    | id: ?ai < Zbeta 1 |- _ =>
      rewrite Zbeta_power1 in id; Clean_beta1
    | |- _ => idtac
  end.

Ltac Constraint_variable :=
  match goal with
      (* non-constant expressions of the form (Z_of_nat ...) *)
    | |- (Z_of_nat ?m < Zpower 2 30) => 
      Clean_beta1; Mult 2%nat; omega
    | |- (Z_of_nat ?m < Zpower 2 32) => 
      Clean_beta1; omega
    | |- (Z_of_nat ?m < Zbeta 1) => 
      omega
      (* other non-constant expressions *)
    | |- (?z < Zpower 2 30) => 
      Clean_beta1; Mult 2%nat; omega
    | |- (?z < Zpower 2 32) => 
      Clean_beta1; omega
    | |- (?z < Zbeta 1) => 
      omega
  end.

Ltac Constraint_compound :=
  match goal with
    | |- (0 <= ?c < _) => 
      ring c;
	match goal with 
	  | |- (0 <= Z0 < _) => split;
	    [apply Zle_refl | Constraint_constant]
	  | |- (0 <= Zpos _ < _) => split;
	    [apply Zle_0_pos | Constraint_constant]
	  | |- (0 <= Z_of_nat _ < _) => split;
	    [apply Zle_0_nat | Constraint_variable]
	  | |- (0 <= u2Z _ < _) => split;
	    [apply min_u2Z | Constraint_variable]
	  (* c is some other expressions containing variables *)
	  | |- (0 <= ?c < _) => split;
	    [Constraint_constant | Constraint_variable]
	end
  end.

Ltac Constraint :=
  match goal with
    | |- (0 <= _ < _) => Constraint_compound
    | |- (?c <= _ ) =>
      ring c;
	match goal with
	  | |- (Z_of_nat _ <= _) => Constraint_variable
	  | |- (u2Z _ <= _) => Constraint_variable
	  | |- (Z0 <= _) => Constraint_constant
	  | |- (Zpos _ <= _) => Constraint_constant
	  | |- (Zneg _ <= _) => Constraint_constant
	  | |- (?c <= _) => Constraint_variable
	end
    | |- (?c < _ ) =>
      ring c;
	match goal with
	  | |- (Z_of_nat _ < _) => Constraint_variable
	  | |- (u2Z _ < _) => Constraint_variable
	  | |- (Z0 < _) => Constraint_constant
	  | |- (Zpos _ < _) => Constraint_constant
	  | |- (Zneg _ < _) => Constraint_constant
	  | |- (?c < _) => Constraint_variable
	end
  end.


  Ltac Decompose_list_32 lst u lst1 lst2 :=
    lapply (list_split'' (int 32) (length lst) lst zero32 (refl_equal (length lst)) u);
      [let X := fresh in 
	(intro X;
	  let Y := fresh in 
	    (inversion_clear X as [lst1 Y];
	      let Z := fresh in 
		let U := fresh in 
		(inversion_clear Y as [Z U];
		inversion_clear U as [lst2]))) | idtac].

  Ltac normalize_left :=
    match goal with 
      | |- ((?P1 ** ?P2) ** ?P3) ?s ?s' ?m ?h -> _ =>
	rewrite (sep.con_assoc_equiv P2 P1 P3); normalize_left
      | |- _ => idtac
    end.

  Ltac normalize_right :=
    match goal with 
      | |- _ -> ((?P1 ** ?P2) ** ?P3) ?s ?s' ?m ?h  =>
	rewrite (sep.con_assoc_equiv P2 P1 P3); normalize_right
      | |- _ => idtac
    end.

  Ltac rotate_left :=
    match goal with
      | |- (?P ** ?Q) ?s ?s' ?m ?h  -> _ =>
	rewrite (sep.con_com_equiv P Q)
      | |- _ => idtac
    end.

  Ltac rotate_right :=
    match goal with
      | |- _ -> (?P ** ?Q) ?s ?s' ?m ?h =>
	rewrite (sep.con_com_equiv P Q)
      | |- _ => idtac
    end.

  Ltac monotony_or_rotate_left n :=
    match n with
      O => rotate_right; normalize_right
      | S ?k =>
	match goal with
	  | |- (?P ** _) ?s ?s' ?m ?h -> (?P ** _) ?s ?s' ?m ?h =>
	    apply monotony; split; [intros; auto | intro; idtac]
	  | |- (_ ** _) ?s ?s' ?m ?h -> (_ ** _) ?s ?s' ?m ?h =>
	    rotate_left; normalize_left; monotony_or_rotate_left k
	end
    end.

  Ltac count_sepcons e :=
    match e with
      (?e1 ** ?e2) => 
      let tmp1 := count_sepcons e1 in
	let tmp2 := count_sepcons e2 in
	  eval compute in (tmp1 + tmp2 + 1)%nat
      | _ => O
    end.

  Ltac count_conjuncts e :=
    let tmp := count_sepcons e in
      eval compute in (tmp + 1)%nat.

  Ltac try_monotony_and_rotate_right n :=
    match n with
      O => idtac
      | S ?k => 
	match goal with 
	  | |- (?e1 ** ?e2) ?s ?s' ?m ?h -> (_ ** _) ?s ?s' ?m ?h => 
	    let left_conjuncts := count_conjuncts (e1 ** e2) in
	      monotony_or_rotate_left left_conjuncts;
	      try_monotony_and_rotate_right k
	  | |- (_ |--> _) ?s ?s' ?m ?h -> (_ |--> _) ?s ?s' ?m ?h => 
	    intros; auto
	  | |- _ =>
	    idtac
	end
    end.

  Ltac assoc_comm H :=
    generalize H; clear H;
    match goal with 
      | |- (_ ** _) ?s ?s' ?m ?h -> (?e1 ** ?e2) ?s ?s' ?m ?h => 
	normalize_right;
	normalize_left;
	let right_conjuncts := count_conjuncts (e1 ** e2) in
	  try_monotony_and_rotate_right right_conjuncts
    end;
    intro H.