(* iris_heap_lang/lib/atomic_heap.v *)
Class atomic_heap
:= AtomicHeap {
  (* -- operations -- *)
  alloc : val;
  free : val;
  load : val;
  store : val;
  cmpxchg : val;
  (** * Ghost state *)
  (** The assumptions about [Σ], and the singleton [gname]s (if needed) *)
  atomic_heapGS : gFunctors → Type;
  (** [heap_inv] is an invariant that is assumed to hold by all operations. It
      can't be allocated through the interface. Instead, implementations should
      provide an initialization lemma that builds [atomic_heapGS] and [heap_inv]
      so that clients can obtain a closed proof (once they have chosen an
      implementation).

      The invariant has to be allocated together with [atomic_heapGS] since it
      is likely to contain singleton ghost state. The initialization lemma is
      not part of the interface as it can only be applied by providing an
      implementation-specific [Σ : gFunctors]. *)
  heap_inv `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} : iProp Σ;
  #[global] heap_inv_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} ::
    Persistent (heap_inv (H:=H));
  (* -- predicates -- *)
  pointsto `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (dq: dfrac) (v : val) : iProp Σ;
  (* -- pointsto properties -- *)
  #[global] pointsto_timeless `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v ::
    Timeless (pointsto (H:=H) l q v);
  #[global] pointsto_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v ::
    Fractional (λ (q : Qp), pointsto (H:=H) l (DfracOwn q) v);
  #[global] pointsto_persistent `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l v ::
    Persistent (pointsto (H:=H) l DfracDiscarded v);
  #[global] pointsto_as_fractional `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l q v ::
    AsFractional (pointsto (H:=H) l (DfracOwn q) v) (λ q, pointsto (H:=H) l (DfracOwn q) v) q;
  #[global] pointsto_combine_sep_gives `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ}
    l dq1 dq2 v1 v2 ::
    CombineSepGives (pointsto (H:=H) l dq1 v1) (pointsto (H:=H) l dq2 v2)
      ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝;
  #[global] pointsto_combine_as `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ}
    l dq1 dq2 v1 v2 ::
    CombineSepAs (pointsto (H:=H) l dq1 v1) (pointsto (H:=H) l dq2 v2)
      (pointsto (H:=H) l (dq1 ⋅ dq2) v1) | 60; (* higher cost than Fractional *)
  pointsto_persist `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} l dq v :
    pointsto (H:=H) l dq v ==∗ pointsto (H:=H) l DfracDiscarded v;
  (* -- operation specs -- *)
  alloc_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (v : val) :
    heap_inv (H:=H) -∗
    {{{ True }}} alloc v {{{ l, RET #l; pointsto (H:=H) l (DfracOwn 1) v }}};
  free_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (v : val) :
    heap_inv (H:=H) -∗
    {{{ pointsto (H:=H) l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
  load_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) :
    heap_inv (H:=H) -∗
    <<{ ∀∀ (v : val) q, pointsto (H:=H) l q v }>>
      load #l @ ↑atomic_heapN
    <<{ pointsto (H:=H) l q v | RET v }>>;
  store_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w : val) :
    heap_inv (H:=H) -∗
    <<{ ∀∀ v, pointsto (H:=H) l (DfracOwn 1) v }>>
      store #l w @ ↑atomic_heapN
    <<{ pointsto (H:=H) l (DfracOwn 1) w | RET #() }>>;
  (* This spec is slightly weaker than it could be: It is sufficient for [w1]
  *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
  is outside the atomic triple, which makes it much easier to use -- and the
  spec is still good enough for all our applications.
  The postcondition deliberately does not use [bool_decide] so that users can
  [destruct (decide (a = b))] and it will simplify in both places. *)
  cmpxchg_spec `{!heapGS_gen hlc Σ} {H : atomic_heapGS Σ} (l : loc) (w1 w2 : val) :
    val_is_unboxed w1 →
    heap_inv (H:=H) -∗
    <<{ ∀∀ v, pointsto (H:=H) l (DfracOwn 1) v }>>
      cmpxchg #l w1 w2 @ ↑atomic_heapN
    <<{ if decide (v = w1)
        then pointsto (H:=H) l (DfracOwn 1) w2 else pointsto (H:=H) l (DfracOwn 1) v
      | RET (v, #(if decide (v = w1) then true else false)) }>>;
}.