Library zoo.program_logic.atomic

From zoo Require Import
  prelude.
From zoo.iris Require Import
  diaframe.
From zoo.iris.bi Require Export
  lib.atomic.
From zoo.program_logic Require Export
  wp.
From zoo Require Import
  options.

Section atomic_acc.
  Context `{BiFUpd PROP} {TA TB : tele}.

  Implicit Types α : TA → PROP.
  Implicit Types P : PROP.
  Implicit Types β Ψ : TA → TB → PROP.

  #[global] Instance atomic_acc_proper Eo Ei :
    Proper (
      pointwise_relation TA (≡) ==>
      (≡) ==>
      pointwise_relation TA (pointwise_relation TB (≡)) ==>
      pointwise_relation TA (pointwise_relation TB (≡)) ==>
      (≡)
    ) (atomic_acc (PROP := PROP) Eo Ei).

  Lemma atomic_acc_frame_l R Eo Ei α P β Ψ :
    R ∗ atomic_acc Eo Ei α P β Ψ ⊢
    atomic_acc Eo Ei α (R ∗ P) β (λ.. x y, R ∗ Ψ x y).
  Lemma atomic_acc_frame_r R Eo Ei α P β Ψ :
    atomic_acc Eo Ei α P β Ψ ∗ R ⊢
    atomic_acc Eo Ei α (P ∗ R) β (λ.. x y, Ψ x y ∗ R).

  #[global] Instance frame_atomic_acc p R Eo Ei α P1 P2 β Ψ1 Ψ2 :
    Frame p R P1 P2 →
    (∀ x y, Frame p R (Ψ1 x y) (Ψ2 x y)) →
    Frame p R (atomic_acc Eo Ei α P1 β (λ.. x y, Ψ1 x y)) (atomic_acc Eo Ei α P2 β (λ.. x y, Ψ2 x y)).

  #[global] Instance is_except_0_atomic_acc Eo Ei α P β Ψ :
    IsExcept0 (atomic_acc Eo Ei α P β Ψ).
End atomic_acc.

Section atomic_update.
  Context `{BiFUpd PROP} {TA TB : tele}.

  Implicit Types α : TA → PROP.
  Implicit Types β Ψ : TA → TB → PROP.

  #[global] Instance atomic_update_proper Eo Ei :
    Proper (
      pointwise_relation TA (≡) ==>
      pointwise_relation TA (pointwise_relation TB (≡)) ==>
      pointwise_relation TA (pointwise_relation TB (≡)) ==>
      (≡)
    ) (atomic_update (PROP := PROP) Eo Ei).

  Lemma atomic_update_mono Eo Ei α β Ψ1 Ψ2 :
    (∀.. x y, Ψ1 x y -∗ Ψ2 x y) -∗
    atomic_update Eo Ei α β Ψ1 -∗
    atomic_update Eo Ei α β Ψ2.
  Lemma atomic_update_wand Eo Ei α β Ψ1 Ψ2 :
    atomic_update Eo Ei α β Ψ1 -∗
    (∀.. x y, Ψ1 x y -∗ Ψ2 x y) -∗
    atomic_update Eo Ei α β Ψ2.

  Lemma atomic_update_frame_l R Eo Ei α β Ψ :
    R ∗ atomic_update Eo Ei α β Ψ ⊢
    atomic_update Eo Ei α β (λ.. x y, R ∗ Ψ x y).
  Lemma atomic_update_frame_r R Eo Ei α β Ψ :
    atomic_update Eo Ei α β Ψ ∗ R ⊢
    atomic_update Eo Ei α β (λ.. x y, Ψ x y ∗ R).

  #[global] Instance frame_atomic_update p R Eo Ei α β Ψ1 Ψ2 :
    (∀ x y, Frame p R (Ψ1 x y) (Ψ2 x y)) →
    Frame p R (atomic_update Eo Ei α β (λ.. x y, Ψ1 x y)) (atomic_update Eo Ei α β (λ.. x y, Ψ2 x y)).

  #[global] Instance is_except_0_atomic_update Eo Ei α β Ψ :
    IsExcept0 (atomic_update Eo Ei α β Ψ).
End atomic_update.

Section atomic_triple.
  Context `{zoo_G : !ZooG Σ} {TA TB TP : tele}.

  Implicit Types P : iProp Σ.
  Implicit Types α : TA → iProp Σ.
  Implicit Types β : TA → TB → iProp Σ.
  Implicit Types Ψ : TA → TB → TP → iProp Σ.
  Implicit Types f : TA → TB → TP → val.

  Definition atomic_triple e tid E P α β Ψ f : iProp Σ :=
    ∀ Φ,
    P -∗
    atomic_update (⊤ ∖ E) ∅ α β (λ.. x y, ∀.. z, Ψ x y z -∗ Φ (f x y z)) -∗
    WP e ∷ tid {{ Φ }}.
  #[global] Arguments atomic_triple e%_E tid E (P α β Ψ f)%_I : assert.

  #[global] Instance atomic_triple_ne e tid E n :
    Proper (
      (≡{n}≡) ==>
      pointwise_relation TA (≡{n}≡) ==>
      pointwise_relation TA (pointwise_relation TB (≡{n}≡)) ==>
      pointwise_relation TA (pointwise_relation TB (pointwise_relation TP (≡{n}≡))) ==>
      pointwise_relation TA (pointwise_relation TB (pointwise_relation TP (=))) ==>
      (≡{n}≡)
    ) (atomic_triple e tid E).
  #[global] Instance atomic_triple_proper e tid E :
    Proper (
      (≡) ==>
      pointwise_relation TA (≡) ==>
      pointwise_relation TA (pointwise_relation TB (≡)) ==>
      pointwise_relation TA (pointwise_relation TB (pointwise_relation TP (≡))) ==>
      pointwise_relation TA (pointwise_relation TB (pointwise_relation TP (=))) ==>
      (≡)
    ) (atomic_triple e tid E).

  Lemma atomic_triple_mono e tid E P α β Ψ1 Ψ2 f :
    (∀.. x y z, Ψ1 x y z -∗ Ψ2 x y z) -∗
    atomic_triple e tid E P α β Ψ1 f -∗
    atomic_triple e tid E P α β Ψ2 f.
  Lemma atomic_triple_wand e tid E P α β Ψ1 Ψ2 f :
    atomic_triple e tid E P α β Ψ1 f -∗
    (∀.. x y z, Ψ1 x y z -∗ Ψ2 x y z) -∗
    atomic_triple e tid E P α β Ψ2 f.

  #[global] Instance frame_atomic_triple p R e tid E P α β Ψ1 Ψ2 f :
    (∀ x y z, Frame p R (Ψ1 x y z) (Ψ2 x y z)) →
    Frame p R (atomic_triple e tid E P α β (λ.. x y, Ψ1 x y) f) (atomic_triple e tid E P α β (λ.. x y, Ψ2 x y) f).
End atomic_triple.

Notation "" := (
  @empty coPset _
)(in custom atomic_triple_mask
).
Notation "@ E" :=
  E
( in custom atomic_triple_mask at level 200,
  E constr,
  format "'/ ' @ E "
).

Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, β%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, Q%I) ..) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, (v%V : val)) ..) ..) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  x1 binder,
  xn binder,
  y1 binder,
  yn binder,
  z1 binder,
  zn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | ∀∀ x1 .. xn , '/ ' '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' ∃∃ y1 .. yn , '/ ' '[' β ']' '/' | z1 .. zn , '/ ' RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, β%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app Q%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  x1 binder,
  xn binder,
  y1 binder,
  yn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | ∀∀ x1 .. xn , '/ ' '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' ∃∃ y1 .. yn , '/ ' '[' β ']' '/' | RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleO)
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app β%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app $ λ z1, .. (λ zn, Q%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app $ λ z1, .. (λ zn, (v%V : val)) ..) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  x1 binder,
  xn binder,
  z1 binder,
  zn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | ∀∀ x1 .. xn , '/ ' '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' '[' β ']' '/' | z1 .. zn , '/ ' RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' β | 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleO)
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app β%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app Q%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app (v%V : val)) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  x1 binder,
  xn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | ∀∀ x1 .. xn , '/ ' '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' '[' β ']' '/' | RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleO)
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, Q%I) ..) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  y1 binder,
  yn binder,
  z1 binder,
  zn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' ∃∃ y1 .. yn , '/ ' '[' β ']' '/' | z1 .. zn , '/ ' RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleO)
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app Q%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  y1 binder,
  yn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' ∃∃ y1 .. yn , '/ ' '[' β ']' '/' | RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleO)
    (TB := TeleO)
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app β%I)
    (tele_app $ tele_app $ tele_app $ λ z1, .. (λ zn, Q%I) ..)
    (tele_app $ tele_app $ tele_app $ λ z1, .. (λ zn, (v%V : val)) ..)
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  z1 binder,
  zn binder,
  format "'[hv' <<< '/ ' '[' P ']' '/' | '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' '[' β ']' '/' | z1 .. zn , '/ ' RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' β | 'RET' v ; Q '>>>'" := (
  atomic_triple
    (TA := TeleO)
    (TB := TeleO)
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app β%I)
    (tele_app $ tele_app $ tele_app Q%I)
    (tele_app $ tele_app $ tele_app (v%V : val))
)(at level 20,
  P, α, e, β, v, Q at level 200,
  tid custom wp_thread_id at level 200,
  E custom atomic_triple_mask at level 200,
  format "'[hv' <<< '/ ' '[' P ']' '/' | '[' α ']' '/' >>> '/ ' '[' e ']' tid E '/' <<< '/ ' '[' β ']' '/' | RET v ; '/ ' '[' Q ']' '/' >>> ']'"
) : bi_scope.

Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, β%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, Q%I) ..) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, (v%V : val)) ..) ..) ..)
) : stdpp_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, β%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app Q%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..) ..)
) : stdpp_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleO)
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app β%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app $ λ z1, .. (λ zn, Q%I) ..) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app $ λ z1, .. (λ zn, (v%V : val)) ..) ..)
) : stdpp_scope.
Notation "'<<<' P | ∀∀ x1 .. xn , α '>>>' e tid E '<<<' β | 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleS (λ x1, .. (TeleS (λ xn, TeleO)) ..))
    (TB := TeleO)
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app $ λ x1, .. (λ xn, α%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app β%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app Q%I) ..)
    (tele_app $ λ x1, .. (λ xn, tele_app $ tele_app (v%V : val)) ..)
) : stdpp_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleO)
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app $ λ z1, .. (λ zn, Q%I) ..) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..)
) : stdpp_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' ∃∃ y1 .. yn , β | 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleO)
    (TB := TeleS (λ y1, .. (TeleS (λ yn, TeleO)) ..))
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app $ λ y1, .. (λ yn, β%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app Q%I) ..)
    (tele_app $ tele_app $ λ y1, .. (λ yn, tele_app (v%V : val)) ..)
) : stdpp_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' β | z1 .. zn , 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleO)
    (TB := TeleO)
    (TP := TeleS (λ z1, .. (TeleS (λ zn, TeleO)) ..))
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app β%I)
    (tele_app $ tele_app $ tele_app $ λ z1, .. (λ zn, Q%I) ..)
    (tele_app $ tele_app $ tele_app $ λ z1, .. (λ zn, (v%V : val)) ..)
) : stdpp_scope.
Notation "'<<<' P | α '>>>' e tid E '<<<' β | 'RET' v ; Q '>>>'" := (
  ⊢ atomic_triple
    (TA := TeleO)
    (TB := TeleO)
    (TP := TeleO)
    e%E
    tid
    E
    P%I
    (tele_app α%I)
    (tele_app $ tele_app β%I)
    (tele_app $ tele_app $ tele_app Q%I)
    (tele_app $ tele_app $ tele_app (v%V : val))
) : stdpp_scope.