Require Import Vbase Varith.
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 ihc initread.
Require Import GpsSepAlg.

Set Implicit Arguments.

Definition preciseish PS PSg P :=
  ∀ hP (SEM: assn_sem P hP) hP' (SEM': assn_sem P hP')
         hF (DEF: hplus hP hF ≠ @Hundef PS PSg) hF' (EQ: hplus hP hF = hplus hP' hF'),
  hP = hP' ∧ Hsim hF hF'.

Lemma precise_nabla PS PSg (P: assn PS PSg): precise P → preciseish (Anabla P).

Theorem rule_load_acq PS PSg typ E QQ
                     (PREC: ∀ v, @precise PS PSg (QQ v))
                     (NORM: ∀ v, normalizable (QQ v))
                     (TYP : acquire_typ typ) :
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload typ E)
         (fun v ⇒ Astar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (QQ v))).

Theorem rule_load_rlx PS PSg typ E QQ
    (PREC: ∀ v, @precise PS PSg (QQ v))
    (NORM: ∀ v, normalizable (QQ v))
    (AT: typ ≠ ATna):
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload typ E)
         (fun v ⇒ Astar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (Anabla (QQ v)))).