Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple fsltriple2.
Require Import ihc initread.
Set Implicit Arguments.

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

Lemma precise_nabla P: precise P → preciseish (Anabla P).

Theorem rule_load_acq typ E QQ (PREC: ∀ v, precise (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 E QQ (PREC: ∀ v, precise (QQ v)) (NORM: ∀ v, normalizable (QQ v)) :
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload ATrlx E)
         (fun v ⇒ Astar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (Anabla (QQ v)))).