Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import fslassnlemmas2.
Require Import fsl load store rmw ghosts.
Require Import Omega.

Set Implicit Arguments.

Lemma triple_false PS PSg E QQ :
  triple (@Afalse PS PSg) E QQ.
Proof.
  done.
Qed.

Lemma rule_conseq_pre PS PSg:
  ∀ (P : assn PS PSg) (E : cexp) (QQ : nat → assn PS PSg),
    triple P E QQ →
    ∀ P' : assn PS PSg,
      implies P' P →
      triple P' E QQ.
Proof.
  ins; eapply rule_conseq; eauto using implies_refl.
Qed.

Lemma rule_conseq_post PS PSg:
  ∀ (P : assn PS PSg) (E : cexp) (QQ : nat → assn PS PSg),
    triple P E QQ →
    ∀ QQ' : val → assn PS PSg,
      (∀ y, implies (QQ y) (QQ' y)) →
      triple P E QQ'.
Proof.
  ins; eapply rule_conseq; eauto using implies_refl.
Qed.

Lemma rule_repeat2 PS PSg (P: assn PS PSg) E QQ QQ' :
  triple P E QQ' →
  implies (QQ' 0%nat) P →
  (∀ x (NZ: x ≠ 0%nat), implies (QQ' x) (QQ x)) →
  triple P (Erepeat E) QQ.
Proof.
  ins; eapply rule_conseq; [eby apply rule_repeat|done|].
  ins; desf; ins; eauto.
Qed.

Lemma rule_value_simple PS PSg (P: assn PS PSg) v:
  triple P (Evalue v) (fun x ⇒ if (x == v)%bool then P else Afalse).
Proof.
  eapply rule_conseq_pre.
    by apply rule_value.
  desf; desf.
Qed.

Lemma rule_alloc_atom_rmwacq_frame PS PSg (P: assn PS PSg) QQ :
  triple P (Ealloc) (fun x ⇒ Arel x QQ &*& Armwacq x QQ &*& P).
Proof.
  eapply rule_conseq_pre.
    2: by apply star_emp_l.
  eapply rule_conseq.
  2: by apply implies_refl.
  by apply rule_frame, rule_alloc_atom_rmwacq.
  by ins; apply equivalent_starA.
Qed.

Theorem rule_store_rlx_rmw PS PSg E E' (QQ: val → assn PS PSg) :
  triple (Arel E QQ &*& Armwacq E QQ &*& Atriangle (QQ E'))
         (Estore ATrlx E E')
         (fun _ ⇒ RMW E QQ).
Proof.
  eapply rule_conseq.
    2: by apply implies_star_l, Arel_split1.

  eapply rule_conseq_pre.
  Focus 2.
    rewrite equivalent_starA.
    rewrite equivalent_starAC.
    apply implies_star_r.
    eby rewrite <- equivalent_starA, equivalent_starC.
  eapply rule_conseq_pre.
    2: eby rewrite <- equivalent_starA.

  by apply rule_frame, rule_store_rlx.

  by ins; rewrite equivalent_starC, equivalent_starA.
Qed.

Lemma rule_load_rlx_rmw PS PSg typ (P: assn PS PSg) E QQrel QQacq:
  typ ≠ ATna → triple (rmw_precondition P E QQrel QQacq)
                        (Eload typ E)
                        (fun _ ⇒ rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_conseq.

  Focus 2.
    unfold rmw_precondition.
    rewrite Armw_acq_split with (QQ := fun _ ⇒ Aemp); eauto.
    rewrite equivalent_starA, !(equivalent_starAC (Arainit _)), !(equivalent_starAC (Aacq _ _)),
            <- equivalent_starA.
    by apply implies_refl.

  by apply rule_frame, rule_load_rlx.

  ins; rewrite nabla_emp, <- star_emp_r, equivalent_starA, !(equivalent_starAC (Armwacq _ _)),
        <- equivalent_starA, <- Armw_acq_split.
  by rewrite !(equivalent_starAC (Arel _ _)); apply implies_refl.
  by ins; unfold hupd; desf; desf; eauto.
Qed.

Theorem rule_cas_ar_simple PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AR: acquire_release_typ rmw_typ) (ATL: load_typ ≠ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if (x == E' )%bool
                   then Aexists (satisfying phi AA)
                   else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_ar; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_rel_simple PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi: val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (REL: release_typ rmw_typ) (ATL: load_typ ≠ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if (x == E')%bool
                   then Aexists (satisfying phi (fun y ⇒ Anabla (AA y)))
                   else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_rel; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_acq_simple PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (ACQ: acquire_typ rmw_typ) (ATL: load_typ ≠ ATna),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if (x == E' )%bool
                   then Aexists (satisfying phi AA)
                   else rmw_precondition (Atriangle P) E QQrel QQacq).
Proof.
  ins; eapply rule_cas_acq; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_rlx_simple PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AT: rmw_typ ≠ ATna) (ATL: load_typ ≠ ATna),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if (x == E')%bool
                   then Aexists (satisfying phi (fun y ⇒ Anabla (AA y)))
                   else rmw_precondition (Atriangle P) E QQrel QQacq).
Proof.
  ins; eapply rule_cas_rlx; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Theorem rule_cas_shortcut_simple PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq
    (UNSAT: implies (Astar (QQacq E') P) Afalse)
    (ATL: load_typ ≠ ATna),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if (x == E')%bool then Afalse else rmw_precondition P E QQrel QQacq).
Proof.
  ins; eapply rule_cas_shortcut; try edone.
  eapply rule_conseq_post.
    by apply rule_load_rlx_rmw.
  ins; desf; desf.
  apply implies_true.
Qed.

Definition fetch_and_modify rmw_typ load_typ l (f: val → val) :=
 LET r <- REPEAT
            LET t <- {{ l }}_ ATrlx in
            LET u <- Ecas rmw_typ load_typ l t (f t) in
            Evalue (if (u == t)%bool then u + 1 else 0)
          END
 in Evalue (Peano.pred r).

Definition increment rmw_typ l := fetch_and_modify rmw_typ ATrlx l (fun x ⇒ (x + 1)%nat).

Definition decrement rmw_typ l := fetch_and_modify rmw_typ ATrlx l (fun x ⇒ Peano.pred x).

Lemma rmw_precondition_star_split PS PSg (P Psend Pkeep: assn PS PSg) E QQrel QQacq:
  equivalent P (Psend &*& Pkeep) →
  equivalent (rmw_precondition P E QQrel QQacq) (rmw_precondition Psend E QQrel QQacq &*& Pkeep).
Proof.
  ins; unfold rmw_precondition; rewrite H, !equivalent_starA; apply equivalent_refl.
Qed.

Theorem rule_fetch_and_modify PS PSg:
  ∀ (P: assn PS PSg) Psend Pkeep E rmw_typ load_typ QQacq QQrel RR f
    (SPLIT: ∀ v, equivalent P (Psend v &*& Pkeep v))
    (CAS: ∀ t, triple (rmw_precondition (Psend t) E QQrel QQacq)
                           (Ecas rmw_typ load_typ E t (f t))
                           (fun x ⇒ if (x == t)%bool then RR t else rmw_precondition (Psend t) E QQrel QQacq)),
    triple (rmw_precondition P E QQrel QQacq)
           (fetch_and_modify rmw_typ load_typ E f)
           (fun x ⇒ RR x &*& Pkeep x).
Proof.
  ins; apply rule_let with (QQ := fun x ⇒ RR (Peano.pred x) &*& Pkeep (Peano.pred x)).
    2: by ins; eapply rule_conseq_pre; [apply rule_value |].
  eapply rule_repeat2.
  instantiate (1 := fun x ⇒ if ((x == 0%nat)%bool)
                             then rmw_precondition P E QQrel QQacq
                             else RR (Peano.pred x) &*& Pkeep (Peano.pred x)).
    2: done.
    2: by ins; desf; desf.
  eapply rule_let.
    by apply rule_load_rlx_rmw.
  intro t; ins.
  eapply rule_let.
  eapply rule_conseq_pre.
    2: by apply rmw_precondition_star_split, (SPLIT t).
    by apply rule_frame, CAS.
  intro u; ins.
  eapply rule_conseq_pre; [by apply rule_value |].
  desf; desf; try omega.
  by rewrite Plus.plus_comm.
  eby rewrite <- rmw_precondition_star_split.
Qed.

Lemma rmw_permission_rmw_precondition PS PSg x QQ (P: assn PS PSg):
  equivalent (RMW x QQ &*& P) (rmw_precondition P x QQ QQ).
Proof.
  unfold RMW, rmw_precondition; rewrite !equivalent_starA; apply equivalent_refl.
Qed.