Require Import Vbase List extralib.
Require Import Classical ClassicalDescription.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fsl ghosts fsl_addons.
Require Import permission GpsSepAlg.
Require Import QArith helpers_rationals fslassnlemmas2 normalizability.
Require Import arc_permissions arc_ghosts.

Definition arc_assn := assn (Fractional_Permissions :: nil) (TokenMonoid :: nil).

Program Definition Pointsto l q v :=
  match excluded_middle_informative (0 ≤ q ≤ 1) return arc_assn with
    | right _ ⇒ Afalse
    | left _ ⇒ match excluded_middle_informative (q == 0) return arc_assn with
                   | left _ ⇒ Aemp
                   | right _ ⇒ Apt Fractional_Permissions (in_eq _ _) (QP (Qred q) _ (eq_sym (Qred_Qred q))) _ l v
                  end
  end.
Next Obligation. by ins; rewrite Qred_correct. Qed.
Next Obligation.
   split; intro; desf.
   inv H1.
   destruct H0; rewrite <- Qred_correct; congruence.
Qed.

Definition GhostPlus l q :=
  match excluded_middle_informative (0 ≤ Qred q) return arc_assn with
    | left GE ⇒ Aghost TokenMonoid (in_eq _ _) l (TokPlus (Qred q) GE (eq_sym (Qred_Qred q)))
    | right _ ⇒ Afalse
  end.

Definition GhostMinus l q :=
  match excluded_middle_informative (0 ≤ Qred q) return arc_assn with
    | right _ ⇒ Afalse
    | left GE ⇒ Aghost TokenMonoid (in_eq _ _) l (TokMinus (Qred q) GE (eq_sym (Qred_Qred q)))
  end.

Lemma empty_pointsto d v: Pointsto d 0 v = Aemp.
Proof.
  by clear; unfold Pointsto; ins; desf; desf; destruct n.
Qed.

Lemma Pointsto_eq x v f f': f == f' → Pointsto x f v = Pointsto x f' v.
Proof.
  unfold Pointsto; ins; desf; rewrite ?H in *; try done; rewrite <- ?H in *; try done.
  eapply Apt_equal; eq_rect_simpl; try done.
  apply QP_equal.
  by apply Qred_complete.

  Grab Existential Variables. done.
Qed.

Lemma GhostPlus_eq g f f' : f == f' → GhostPlus g f = GhostPlus g f'.
Proof.
  ins; unfold GhostPlus; desf; try solve [by rewrite H in × | by rewrite <- H in *].
  eapply Aghost_equal; eq_rect_simpl; try done.
  by apply Tok_equal, Qred_complete.

  Grab Existential Variables. done.
Qed.

Lemma GhostMinus_eq g f f' : f == f' → GhostMinus g f = GhostMinus g f'.
Proof.
  ins; unfold GhostMinus; desf; try solve [by rewrite H in × | by rewrite <- H in *].
  eapply Aghost_equal; eq_rect_simpl; try done.
  by apply Tok_equal, Qred_complete.

  Grab Existential Variables. done.
Qed.

Lemma triangle_GhostPlus g q: equivalent (Atriangle (GhostPlus g q)) (GhostPlus g q).
Proof.
  unfold GhostPlus; desf.
  × split; red; ins; desf.
    + clear H2; red in H1; desf.
      f_equal. extensionality x; specialize (H2 x).
      red in H2; desf.
    + repeat eexists.
  × split; red; ins; desf.
Qed.

Lemma triangle_GhostMinus g q: equivalent (Atriangle (GhostMinus g q)) (GhostMinus g q).
Proof.
  unfold GhostMinus; desf; split; red; ins; desf.
  × clear H2; red in H1; desf.
    f_equal. extensionality x; specialize (H2 x).
    red in H2; desf.
  × repeat eexists.
Qed.

Lemma nabla_GhostPlus g q: equivalent (Anabla (GhostPlus g q)) (GhostPlus g q).
Proof.
  unfold GhostPlus; desf.
  × split; red; ins; desf.
    + clear H2; red in H1; desf.
      f_equal. extensionality x; specialize (H2 x).
      red in H2; desf.
    + repeat eexists.
  × split; red; ins; desf.
Qed.

Lemma nabla_GhostMinus g q: equivalent (Anabla (GhostMinus g q)) (GhostMinus g q).
Proof.
  unfold GhostMinus; desf; split; red; ins; desf.
  × clear H2; red in H1; desf.
    f_equal. extensionality x; specialize (H2 x).
    red in H2; desf.
  × repeat eexists.
Qed.

Lemma normalizable_GhostPlus: ∀ g q, normalizable (GhostPlus g q).
Proof.
  ins; unfold GhostPlus; desf.
  apply MFPassn_normalizable; vauto.
Qed.

Lemma normalizable_Pointsto: ∀ x q v, normalizable (Pointsto x q v).
Proof.
  ins; unfold Pointsto; desf.
  apply MFPassn_normalizable; vauto.
Qed.

Lemma consume_token g f q: implies (GhostMinus g f &*& GhostPlus g q) (GhostMinus g (f - q)).
Proof.
  unfold GhostMinus, GhostPlus; red; ins; desf; ins; desf.
  × rewrite hplus_unfold; desf; desf.
    + f_equal. clear H.
      unfold gres_plus_total; desf.
      apply gres_ext; ins; desf; desf.
      - unfold gres_plus in Heq; des_eqrefl; desf.
        clear GHOSTcompat; ins.
        inv_lplus n; desf; desf.
        unfold olift_plus in EQ; desf.
        rewrite <- H0; repeat f_equal.
        ins; desf.
        f_equal.
        rewrite <- eq_rect_eq in *; ins; desf.
        by apply Tok_equal, Qred_complete; rewrite !Qred_correct.
      - unfold gres_plus in Heq; des_eqrefl; desf.
        clear GHOSTcompat; ins.
        inv_lplus n; desf; desf.
        unfold olift_plus in EQ; desf.
    + destruct n; split; try done. clear H.
      unfold gres_plus; des_eqrefl; desf.
      inv_lplus2 gg.
      unfold olift_plus in EQ; desf; ins; desf; desf.
      unfold plift_plus in Heq1; desf.
      rewrite <- eq_rect_eq in *; ins; desf.
      by rewrite !Qred_correct in ×.
  × destruct n; rewrite hplus_unfold in H; desf; ins; desf.
    clear H; unfold gres_plus in GHOSTcompat; des_eqrefl; desf; ins.
    clear GHOSTcompat; inv_lplus g.
    rewrite eqxx in EQ; ins; desf.
    rewrite <- eq_rect_eq in *; ins; desf.
    by clear - q3; rewrite !Qred_correct in ×.
Qed.

Lemma consume_token2 g f q: implies (GhostPlus g q &*& GhostMinus g f) (GhostMinus g (f - q)).
Proof.
  rewrite equivalent_starC; apply consume_token.
Qed.

Lemma produce_one_token g q: equivalent (GhostMinus g q) (GhostMinus g (q + 1) &*& GhostPlus g 1).
Proof.
  split.
  Focus 2.
    rewrite consume_token.
    cut(GhostMinus g (q + 1 - 1) = GhostMinus g q).
       by intro G; rewrite G; apply implies_refl.
    apply GhostMinus_eq.
    by unfold Qminus; rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r.

  unfold GhostMinus, GhostPlus, mydec; red; ins; desf; ins; desf.

  { repeat eexists; ins.
    rewrite hplus_unfold; desf; ins; desf.
    × f_equal; unfold gres_plus_total; desf.
      unfold gres_plus in Heq; des_eqrefl; try done; desf; ins.
      clear GHOSTcompat.
      apply gres_ext.
      intro x; ins.
      inv_lplus x; desf; desf.
      + unfold olift_plus in EQ; desf.
        unfold plift_plus in Heq; desf.
        rewrite <- H0; repeat f_equal.
        rewrite <- eq_rect_eq in *; ins; desf.
        apply Tok_equal.
        apply Qred_complete; rewrite !Qred_correct.
        unfold Qminus; rewrite <- Qplus_assoc.
        change (1 + - (1)) with 0.
        by apply Qplus_0_r.
      + unfold olift_plus in EQ; desf.
    × destruct n; split; try done.
      unfold gres_plus; des_eqrefl; try done.
      inv_lplus2 gg.
      unfold olift_plus in EQ; desf.
      ins; desf; desf.
      unfold plift_plus in Heq1; desf.
      rewrite <- eq_rect_eq in Heq; ins; desf.
      destruct n; rewrite !Qred_correct in ×.
      unfold Qminus; rewrite <- Qplus_assoc.
      change (1 + - (1)) with 0.
      by rewrite Qplus_0_r.
  }
        
  by destruct n.

  by destruct n;rewrite Qred_correct in *; apply Qplus_le_compat with (x:=0) (z:=0).

  by destruct n0.
Qed.

Lemma combine_tokens g f q: implies (GhostPlus g f &*& GhostPlus g q) (GhostPlus g (f + q)).
Proof.
  unfold GhostPlus at 1; red; ins; desf; ins; desf.
  unfold GhostPlus in H2; ins; desf; ins; desf.
  unfold GhostPlus; desf; ins.
  × rewrite hplus_unfold in *; desf; desf.
    clear H; f_equal.
    unfold gres_plus_total; desf.
    unfold gres_plus in Heq; des_eqrefl; try done; desf; ins.
    clear GHOSTcompat.
    apply gres_ext; ins; desf; desf.
    + inv_lplus n; rewrite eqxx in EQ; ins; desf; rewrite <- eq_rect_eq in *; ins; desf.
      rewrite <- H0; repeat f_equal; apply Tok_equal.
      by apply Qred_complete; rewrite !Qred_correct.
    + inv_lplus n; ins; desf; desf.
      unfold olift_plus in EQ; desf.
  × clear H; desf; rewrite Qred_correct in ×.
    by destruct n; apply nonnegative_sum.
Qed.

Lemma split_tokens g a b c :
  a == b + c → b ≥ 0 → c ≥ 0 → equivalent (GhostPlus g a) (GhostPlus g b &*& GhostPlus g c).
Proof.
  intros SUM B C; split.
  Focus 2.
    rewrite combine_tokens.
    cut (GhostPlus g (b + c) = GhostPlus g a).
      by intro G; rewrite G; apply implies_refl.
    by apply GhostPlus_eq.

  unfold GhostPlus; ins; desf; ins; desf; try by rewrite Qred_correct in ×.
  red; ins; eexists _, _; repeat split; try edone; desf.
  rewrite hplus_unfold; ins; desf; desf.
  × f_equal; unfold gres_plus_total; desf.
    unfold gres_plus in Heq; des_eqrefl; try done; desf; ins.
    clear GHOSTcompat; apply gres_ext; ins; desf; desf.
    + inv_lplus n; rewrite eqxx in EQ; ins; desf; rewrite <- eq_rect_eq in *; ins; desf.
      rewrite <- H0; repeat f_equal; apply Tok_equal.
      by apply Qred_complete; rewrite !Qred_correct.
    + inv_lplus n; ins; desf; desf.
      unfold olift_plus in EQ; desf.
  × destruct n; split; try done.
    unfold gres_plus; des_eqrefl; try done.
    inv_lplus2 x.
    unfold olift_plus in EQ; desf; ins; desf; desf; ins; desf; rewrite <- eq_rect_eq in *; ins; desf.
Qed.

Lemma empty_ghost_r g a Ghost:
  Ghost = GhostPlus ∨ Ghost = GhostMinus → equivalent (Ghost g a &*& GhostPlus g 0) (Ghost g a).
Proof.
  ins; desf.
  {
    split.
      by rewrite combine_tokens; refl_implies; apply GhostPlus_eq; rewrite Qplus_0_r.
    destruct (classic (a ≥ 0)).
      by rewrite split_tokens at 1; try edone; rewrite Qplus_0_r.
    unfold GhostPlus at 1; desf.
    by exfalso; rewrite Qred_correct in ×.
  }
  { split.
      by rewrite consume_token; refl_implies; apply GhostMinus_eq; unfold Qminus; rewrite Qopp_zero, Qplus_0_r.
    unfold GhostMinus, GhostPlus; red; ins; desf; ins; desf.
      2: by destruct n.
   repeat eexists; ins.
   rewrite hplus_unfold; desf; ins; desf.
   × f_equal; unfold gres_plus_total; desf.
     unfold gres_plus in Heq; des_eqrefl; try done; desf; ins.
     clear GHOSTcompat.
     apply gres_ext.
     intro x; ins.
     inv_lplus x; desf; desf.
     + unfold olift_plus in EQ; desf.
       unfold plift_plus in Heq; desf.
       rewrite <- H0; repeat f_equal.
       rewrite <- eq_rect_eq in *; ins; desf.
       apply Tok_equal.
       by apply Qred_complete; unfold Qminus; rewrite !Qred_correct, Qopp_zero, Qplus_0_r.
     + unfold olift_plus in EQ; desf.
   × destruct n; split; try done.
     unfold gres_plus; des_eqrefl; try done.
     inv_lplus2 gg.
     unfold olift_plus in EQ; desf.
     ins; desf; desf.
     unfold plift_plus in Heq1; desf.
     rewrite <- eq_rect_eq in Heq; ins; desf.
     destruct n; rewrite !Qred_correct in ×.
     by unfold Qminus; rewrite Qopp_zero, Qplus_0_r.
  }
Qed.

Lemma empty_ghost_l g a Ghost:
  Ghost = GhostPlus ∨ Ghost = GhostMinus → equivalent (GhostPlus g 0 &*&Ghost g a) (Ghost g a).
Proof.
  by ins; rewrite equivalent_starC; apply empty_ghost_r.
Qed.

Lemma split_pointsto x v a b c :
  a == b + c → b ≥ 0 → c ≥ 0 → equivalent (Pointsto x a v) (Pointsto x b v &*& Pointsto x c v).
Proof.
  intros SUM B C; split.
  × unfold Pointsto at 2; red; ins; desf.
    + rewrite q, Qplus_0_l in ×.
      rewrite Pointsto_eq with (f' := c) in H; try done.
      eexists _, _; repeat split; try edone.
      eby eapply assn_sem_def.
      by rewrite hplus_emp_l.
    + unfold Pointsto; desf; ins.
      - rewrite q, Qplus_0_r in ×.
        rewrite Pointsto_eq with (f' := b) in H; try done.
        unfold Pointsto in H; ins; desf; ins; desf; desf.
        eexists _, _; repeat split; try edone.
        rewrite !hplus_emp_r.
        clear; f_equal; exten.
        ins; unfold hupd; desf; desf.
        by eapply HVval_equal; eq_rect_simpl; try apply QP_equal.
      - unfold Pointsto in H; desf; desf; ins.
          by symmetry in SUM; rewrite q in SUM; apply nonnegative_sum_eq_zero in SUM; desf.
        rewrite H; clear H.
        repeat eexists; try done.
        rewrite hplus_hsingl; ins; desf;
          try (by destruct n2; rewrite ?Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM).
        { f_equal; exten; ins; unfold hupd; desf; desf.
          eapply HVval_equal; eq_rect_simpl; desf; ins; desf; try apply QP_equal; ins;
            try (by apply Qred_complete; rewrite !Qred_correct; rewrite SUM);
            try (by destruct n2; rewrite !Qred_correct, ?Qplus_0_l, <- ?SUM).
        }
        { destruct n2; desf; unfold permissionsOK; eq_rect_simpl; ins; desf; split; try done; ins; desf;
            try (by destruct n2; rewrite !Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM).
          red; intro; desf.
          apply Qeq_weaken in H; rewrite !Qred_correct, !Qplus_0_l, Qplus_0_r in H.
          apply nonnegative_sum_eq_zero in H; desf.
        }
        { split; [done | red]; eq_rect_simpl; ins; desf; split; try done; ins; desf;
            try (by destruct n2; rewrite ?Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM).
          red; intro; desf.
          apply Qeq_weaken in H; rewrite !Qred_correct, !Qplus_0_l, Qplus_0_r in H.
          apply nonnegative_sum_eq_zero in H; desf.
        }
      - destruct n0; split; try done.
        unfold Pointsto in H; desf.
          by rewrite SUM in q; apply nonnegative_sum_eq_zero in q; desf.
        clear H; desf.
        apply Qopp_le_compat in a3.
        apply Qplus_le_compat with (x := b + c) (y := a) in a3.
          2: by rewrite SUM; apply Qle_refl.
        rewrite Qplus_opp_r in a3.
        apply Qplus_le_compat with (x := -b) (y := 0) in a3.
          2: by rewrite <- Qopp_zero; apply Qopp_le_compat.
        rewrite !Qplus_assoc, Qplus_opp_l, !Qplus_0_l in a3.
        apply Qplus_le_compat with (x := 1) (y := 1) in a3; try done.
        by rewrite Qplus_comm, <- Qplus_assoc, Qplus_opp_r, !Qplus_0_r in a3.
    + destruct n; split; try done.
      unfold Pointsto in H; desf.
        by rewrite SUM in q; apply nonnegative_sum_eq_zero in q; desf; rewrite q.
      clear H; desf.
      apply Qopp_le_compat in a1.
      apply Qplus_le_compat with (x := b + c) (y := a) in a1.
        2: by rewrite SUM; apply Qle_refl.
      rewrite Qplus_opp_r in a1.
      apply Qplus_le_compat with (x := -c) (y := 0) in a1.
        2: by rewrite <- Qopp_zero; apply Qopp_le_compat.
      rewrite (Qplus_comm b), !Qplus_assoc, Qplus_opp_l, !Qplus_0_l in a1.
      apply Qplus_le_compat with (x := 1) (y := 1) in a1; try done.
      by rewrite Qplus_comm, <- Qplus_assoc, Qplus_opp_l, !Qplus_0_r in a1.
  × unfold Pointsto at 1; red; ins; desf; ins; desf; rewrite ?hplus_emp_r, ?hplus_emp_l in ×.
      rewrite Pointsto_eq with (f' := c); try done.
      by rewrite SUM, q, Qplus_0_l.
    unfold Pointsto in H2; desf; ins; desf.
    + rewrite hplus_emp_r.
      rewrite Pointsto_eq with (f' := b).
        2: by rewrite SUM, q, Qplus_0_r.
      unfold Pointsto; desf; ins.
      - f_equal; exten; ins; unfold hupd; desf; desf.
        by eapply HVval_equal; eq_rect_simpl; try apply QP_equal.
      - by destruct n0.
    + unfold Pointsto; desf.
      - rewrite SUM in q; apply nonnegative_sum_eq_zero in q; desf.
      - rewrite hplus_hsingl; ins.
        { f_equal; exten; ins; unfold hupd; desf; desf.
          { eapply HVval_equal; eq_rect_simpl; try done; desf; ins; desf;
              try (by destruct n2; rewrite ?Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM);
              apply QP_equal.
            by apply Qred_complete; rewrite !Qred_correct, SUM.
            by rewrite <- Qred_zero; apply Qred_complete; rewrite Qred_zero, Qplus_0_l.
            by rewrite <- Qred_zero; apply Qred_complete; rewrite Qred_zero, Qplus_0_l.
          }
          { destruct n2; eq_rect_simpl; unfold permissionsOK; desf; ins; desf; split; try done; ins; desf;
              try (by destruct n2; rewrite ?Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM).
            red; intro; desf.
            apply Qeq_weaken in H0; rewrite !Qred_correct, !Qplus_0_l, Qplus_0_r in H0.
            apply nonnegative_sum_eq_zero in H0; desf.
          }
        }
        { desf; split; [done | red]; eq_rect_simpl; ins; desf; split; try done; ins; desf;
            try (by destruct n2; rewrite ?Qred_correct, ?Qplus_0_l, ?Qplus_0_r, <- ?SUM).
          red; intro; desf.
          apply Qeq_weaken in H0; rewrite !Qred_correct, !Qplus_0_l, Qplus_0_r in H0.
          apply nonnegative_sum_eq_zero in H0; desf.
        }
      - destruct H; rewrite hplus_unfold; desf; desf.
        exfalso; specialize (HEAPcompat x); unfold hupd in HEAPcompat; rewrite eqxx in *; ins; desf; eq_rect_simpl;
          ins; desf; try (by clear HEAPcompat0; rewrite !Qred_correct, <- SUM in a4).
        by red in HEAPcompat0; desf.
        by red in HEAPcompat0; desf.

  Grab Existential Variables. all: done.
Qed.

Lemma rule_alloc_na_with_two_ghosts:
  triple Aemp
         Ealloc
         (fun x ⇒ Aexists (fun g ⇒ Aexists (fun g' ⇒ Aptu x &*& GhostMinus g 0 &*& GhostMinus g' 0))).
Proof.
  eapply rule_conseq_post with
    (QQ := (fun x ⇒ (Aptu x &*& Aexists (fun g ⇒ GhostMinus g 0)) &*& Aexists (fun g' ⇒ GhostMinus g' 0))).

  {
    unfold GhostMinus; ins; desf.
    by do 2 apply rule_ghost_intro; apply rule_alloc_na.
    by destruct n.
  }
  
  {
    red. intros x h SEM.
    repeat (rewrite assn_sem_star in *; desc).
    rewrite assn_sem_exists in *; desc.
    eexists; rewrite assn_sem_exists.
    eexists; rewrite assn_sem_star.
    split; try done.
    subst hp; rewrite hplusA in ×.
    eexists _, _; repeat (apply conj; try edone).
    rewrite assn_sem_star.
    split; [ | by repeat (eexists; try edone)].
    eby subst h; eapply hplus_not_undef_r.
  }
Qed.

Lemma rule_load_poinsto x q v:
  0 < q → q ≤ 1 →
  triple (Pointsto x q v) (Eload ATna x) (fun y ⇒ if (y == v)%bool then Pointsto x q v else Afalse).
Proof.
  ins; unfold Pointsto; desf.
    by rewrite q0 in H.
  eapply rule_conseq.
  by apply rule_load_na.
  by refl_implies; eapply Apt_equal.
  ins; desf; desf; try omega.
  by refl_implies; eapply Apt_equal; eq_rect_simpl.

  Grab Existential Variables. all: try done.
  {
    eq_rect_simpl; intro; ins; desf.
    apply Qeq_weaken in H1; rewrite Qred_correct in H1.
    by rewrite H1 in H.
  }
  by apply in_eq.
Qed.