Library zoo_std.mvar

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.base_logic Require Import
  lib.excl
  lib.oneshot.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  mvar__code.
From zoo_std Require Import
  option.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types v : val.
Implicit Types 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 Types t : location.
    Implicit Types Ψ : val → iProp Σ.

    Record mvar_name :=
      { mvar_name_lstate : gname
      ; mvar_name_consumer : gname
      }.
    Implicit Types γ : 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_1 γ Ψ v : iProp Σ :=
        Ψ v
      ∨ consumer γ.
    #[local] Instance : CustomIpat "inv_state_set_1" :=
      " [ HΨ | Hconsumer{_{}} ] ".
    #[local] Definition inv_state_set_2 γ Ψ v : iProp Σ :=
      lstate_set γ ∗
      inv_state_set_1 γ Ψ v.
    #[local] Instance : CustomIpat "inv_state_set_2" :=
      " ( {>;}#Hlstate_set{_{}} & Hstate ) ".
    #[local] Definition inv_state γ Ψ state :=
      match state with
      | None ⇒
          inv_state_unset γ
      | Some v ⇒
          inv_state_set_2 γ Ψ 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.

From zoo_std Require
  mvar__opaque.

Section mvar_G.
  Context `{mvar_G : MvarG Σ}.

  Implicit Types 𝑡 : location.
  Implicit Types t : val.
  Implicit Types γ : base.mvar_name.
  Implicit Types Ψ : val → iProp Σ.

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

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

  Definition mvar_resolved t : iProp Σ :=
    ∃ 𝑡 γ,
    ⌜t = #𝑡⌝ ∗
    meta 𝑡 nroot γ ∗
    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.