Library zoo_std.mvar

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.base_logic.lib.excl.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.mvar__code.
Require Import zoo_std.mvar__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type v : val.
Implicit Type o state : option val.

Class MvarG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] mvar۰G۰lstate۰G :: OneshotG Σ unit unit
  ; #[local] mvar۰G۰consumer۰G :: ExclG Σ unitO
  }.

Definition mvar۰Σ :=
  #[oneshot۰Σ unit unit
  ; excl۰Σ unitO
  ].
#[global] Instance subGｰmvar۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG mvar۰Σ Σ →
  MvarG Σ .

Module base.
  Section mvar۰G.
    Context `{mvar۰G : MvarG Σ}.

    Implicit Type t : location.
    Implicit Type Ψ : val → iProp Σ.

    Record mvar۰name :=
      { mvar۰name۰lstate : gname
      ; mvar۰name۰consumer : gname
      }.
    Implicit Type γ : mvar۰name.

    #[global] Instance mvar۰nameｰeq_dec : EqDecision mvar۰name :=
      ltac:(solve_decision).
    #[global] Instance mvar۰nameｰcountable :
      Countable mvar۰name.

    #[local] Definition lstate۰unset' γ_lstate :=
      oneshot۰pending γ_lstate Own ().
    #[local] Definition lstate۰unset γ :=
      lstate۰unset' γ.(mvar۰name۰lstate).
    #[local] Definition lstate۰set' γ_lstate :=
      oneshot۰shot γ_lstate ().
    #[local] Definition lstate۰set γ :=
      lstate۰set' γ.(mvar۰name۰lstate).

    #[local] Definition consumer' γ_consumer :=
      excl γ_consumer ().
    #[local] Definition consumer γ :=
      consumer' γ.(mvar۰name۰consumer).

    #[local] Definition inv۰state۰unset γ :=
      lstate۰unset γ.
    #[local] Instance : CustomIpat "inv۰state۰unset" :=
      " {>;}Hlstate_unset ".
    #[local] Definition inv۰state۰set₁ γ Ψ v : iProp Σ :=
        Ψ v
      ∨ consumer γ.
    #[local] Instance : CustomIpat "inv۰state۰set₁" :=
      " [ HΨ | Hconsumer{_{}} ] ".
    #[local] Definition inv۰state۰set₂ γ Ψ v : iProp Σ :=
      lstate۰set γ ∗
      inv۰state۰set₁ γ Ψ v.
    #[local] Instance : CustomIpat "inv۰state۰set₂" :=
      " ( {>;}#Hlstate_set{_{}} & Hstate ) ".
    #[local] Definition inv۰state γ Ψ state :=
      match state with
      | None ⇒
          inv۰state۰unset γ
      | Some v ⇒
          inv۰state۰set₂ γ Ψ v
      end.

    #[local] Definition inv۰inner t γ Ψ : iProp Σ :=
      ∃ state,
      t ↦ᵣ state ∗
      inv۰state γ Ψ state.
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %state & Ht & Hstate ) ".
    Definition mvar۰inv t γ Ψ : iProp Σ :=
      inv nroot (inv۰inner t γ Ψ).
    #[local] Instance : CustomIpat "inv" :=
      " #Hinv ".

    Definition mvar۰consumer :=
      consumer.
    #[local] Instance : CustomIpat "consumer" :=
      " Hconsumer{_{}} ".

    Definition mvar۰resolved :=
      lstate۰set.
    #[local] Instance : CustomIpat "resolved" :=
      " #Hlstate_set{_{}} ".

    #[global] Instance mvar۰invｰcontractive t γ n :
      Proper (
        (pointwise_relation _ (dist_later n)) ==>
        (≡{n}≡)
      ) (mvar۰inv t γ).
    #[global] Instance mvar۰invｰproper t γ :
      Proper (
        (pointwise_relation _ (≡)) ==>
        (≡)
      ) (mvar۰inv t γ).

    #[global] Instance mvar۰resolvedｰtimeless γ :
      Timeless (mvar۰resolved γ).

    #[global] Instance mvar۰invｰpersistent t γ Ψ :
      Persistent (mvar۰inv t γ Ψ).
    #[global] Instance mvar۰resolvedｰpersistent γ :
      Persistent (mvar۰resolved γ).

    #[local] Lemma lstateｰalloc :
      ⊢ |==>
        ∃ γ_lstate,
        lstate۰unset' γ_lstate.
    #[local] Lemma lstateｰunsetｰset γ :
      lstate۰unset γ -∗
      lstate۰set γ -∗
      False.
    #[local] Lemma lstateｰupdate γ :
      lstate۰unset γ ⊢ |==>
      lstate۰set γ.

    #[local] Lemma consumerｰalloc :
      ⊢ |==>
        ∃ γ_consumer,
        consumer' γ_consumer.
    #[local] Lemma consumerｰexclusive γ :
      consumer γ -∗
      consumer γ -∗
      False.

    Lemma mvar۰consumerｰexclusive γ :
      mvar۰consumer γ -∗
      mvar۰consumer γ -∗
      False.

    Lemma mvar٠createｰspec Ψ :
      {{{
        True
      }}}
        mvar٠create ()
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        mvar۰inv t γ Ψ ∗
        mvar۰consumer γ
      }}}.

    Lemma mvar٠makeｰspec Ψ v :
      {{{
        ▷ Ψ v
      }}}
        mvar٠make v
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ ∗
        mvar۰consumer γ
      }}}.

    Lemma mvar٠try_getｰspec t γ Ψ :
      {{{
        mvar۰inv t γ Ψ
      }}}
        mvar٠try_get #t
      {{{
        o
      , RET o;
        if o then
          mvar۰resolved γ
        else
          True
      }}}.
    Lemma mvar٠try_getｰspecｰresolved t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ
      }}}
        mvar٠try_get #t
      {{{
        v
      , RET Some v;
        True
      }}}.
    Lemma mvar٠try_getｰspecｰconsumer t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰consumer γ
      }}}
        mvar٠try_get #t
      {{{
        o
      , RET o;
        if o is Some v then
          mvar۰resolved γ ∗
          Ψ v
        else
          True
      }}}.
    Lemma mvar٠try_getｰspecｰresolvedｰconsumer t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ ∗
        mvar۰consumer γ
      }}}
        mvar٠try_get #t
      {{{
        v
      , RET Some v;
        Ψ v
      }}}.

    Lemma mvar٠is_unsetｰspec t γ Ψ :
      {{{
        mvar۰inv t γ Ψ
      }}}
        mvar٠is_unset #t
      {{{
        b
      , RET #b;
        if b then
          True
        else
          mvar۰resolved γ
      }}}.
    Lemma mvar٠is_unsetｰspecｰresolved t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ
      }}}
        mvar٠is_unset #t
      {{{
        RET false;
        True
      }}}.

    Lemma mvar٠is_setｰspec t γ Ψ :
      {{{
        mvar۰inv t γ Ψ
      }}}
        mvar٠is_set #t
      {{{
        b
      , RET #b;
        if b then
          mvar۰resolved γ
        else
          True
      }}}.
    Lemma mvar٠is_setｰspecｰresolved t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ
      }}}
        mvar٠is_set #t
      {{{
        RET true;
        True
      }}}.

    Lemma mvar٠getｰspec t γ Ψ :
      {{{
        mvar۰inv t γ Ψ ∗
        mvar۰resolved γ
      }}}
        mvar٠get #t
      {{{
        v
      , RET v;
        True
      }}}.

    Lemma mvar٠setｰspec t γ Ψ v :
      {{{
        mvar۰inv t γ Ψ ∗
        ▷ Ψ v
      }}}
        mvar٠set #t v
      {{{
        RET ();
        mvar۰resolved γ
      }}}.
  End mvar۰G.

  #[global] Opaque mvar۰inv.
  #[global] Opaque mvar۰consumer.
  #[global] Opaque mvar۰resolved.
End base.

Require zoo_std.mvar__opaque.

Section mvar۰G.
  Context `{mvar۰G : MvarG Σ}.

  Implicit Type 𝑡 : location.
  Implicit Type t : val.
  Implicit Type γ : base.mvar۰name.
  Implicit Type Ψ : val → iProp Σ.

  Definition mvar۰inv t Ψ : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.mvar۰inv 𝑡 γ Ψ.
  #[local] Instance : CustomIpat "inv" :=
    " ( %l{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".

  Definition mvar۰consumer t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.mvar۰consumer γ.
  #[local] Instance : CustomIpat "consumer" :=
    " ( %l{;_} & %γ{;_} & {%Heq{};->} & #Hmeta{_{}} & Hconsumer{_{}} ) ".

  Definition mvar۰resolved t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    𝑡 ↪ γ ∗
    base.mvar۰resolved γ.
  #[local] Instance : CustomIpat "resolved" :=
    " ( %l{;_} & %γ{;_} & {%Heq{};->} & #Hmeta{_{}} & Hresolved{_{}} ) ".

  #[global] Instance mvar۰inv_contractive t n :
    Proper (
      (pointwise_relation _ (dist_later n)) ==>
      (≡{n}≡)
    ) (mvar۰inv t).
  #[global] Instance mvar۰invｰproper t :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (≡)
    ) (mvar۰inv t).

  #[global] Instance mvar۰resolvedｰtimeless t :
    Timeless (mvar۰resolved t).

  #[global] Instance mvar۰invｰpersistent t Ψ :
    Persistent (mvar۰inv t Ψ).
  #[global] Instance mvar۰resolvedｰpersistent t :
    Persistent (mvar۰resolved t).

  Lemma mvar۰consumerｰexclusive t :
    mvar۰consumer t -∗
    mvar۰consumer t -∗
    False.

  Lemma mvar٠createｰspec Ψ :
    {{{
      True
    }}}
      mvar٠create ()
    {{{
      t
    , RET t;
      mvar۰inv t Ψ ∗
      mvar۰consumer t
    }}}.

  Lemma mvar٠makeｰspec Ψ v :
    {{{
      ▷ Ψ v
    }}}
      mvar٠make v
    {{{
      t
    , RET t;
      mvar۰inv t Ψ ∗
      mvar۰resolved t ∗
      mvar۰consumer t
    }}}.

  Lemma mvar٠try_getｰspec t Ψ :
    {{{
      mvar۰inv t Ψ
    }}}
      mvar٠try_get t
    {{{
      o
    , RET o;
      if o is Some v then
        mvar۰resolved t
      else
        True
    }}}.
  Lemma mvar٠try_getｰspecｰresolved t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰resolved t
    }}}
      mvar٠try_get t
    {{{
      v
    , RET Some v;
      True
    }}}.
  Lemma mvar٠try_getｰspecｰconsumer t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰consumer t
    }}}
      mvar٠try_get t
    {{{
      o
    , RET o;
      if o is Some v then
        mvar۰resolved t ∗
        Ψ v
      else
        True
    }}}.
  Lemma mvar٠try_getｰspecｰresolvedｰconsumer t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰resolved t ∗
      mvar۰consumer t
    }}}
      mvar٠try_get t
    {{{
      v
    , RET Some v;
      Ψ v
    }}}.

  Lemma mvar٠is_unsetｰspec t Ψ :
    {{{
      mvar۰inv t Ψ
    }}}
      mvar٠is_unset t
    {{{
      b
    , RET #b;
      if b then
        True
      else
        mvar۰resolved t
    }}}.
  Lemma mvar٠is_unsetｰspecｰresolved t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰resolved t
    }}}
      mvar٠is_unset t
    {{{
      RET false;
      True
    }}}.

  Lemma mvar٠is_setｰspec t Ψ :
    {{{
      mvar۰inv t Ψ
    }}}
      mvar٠is_set t
    {{{
      b
    , RET #b;
      if b then
        mvar۰resolved t
      else
        True
    }}}.
  Lemma mvar٠is_setｰspecｰresolved t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰resolved t
    }}}
      mvar٠is_set t
    {{{
      RET true;
      True
    }}}.

  Lemma mvar٠getｰspec t Ψ :
    {{{
      mvar۰inv t Ψ ∗
      mvar۰resolved t
    }}}
      mvar٠get t
    {{{
      v
    , RET v;
      True
    }}}.

  Lemma mvar٠setｰspec t Ψ v :
    {{{
      mvar۰inv t Ψ ∗
      ▷ Ψ v
    }}}
      mvar٠set t v
    {{{
      RET ();
      mvar۰resolved t
    }}}.
End mvar۰G.

#[global] Opaque mvar۰inv.
#[global] Opaque mvar۰consumer.
#[global] Opaque mvar۰resolved.