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.

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.

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'.

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.

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

Lemma rmw_permission_rmw_precondition PS PSg x QQ (P: assn PS PSg):
  equivalent (RMW x QQ &*& P) (rmw_precondition P x QQ QQ).