Library zoo_std.ivar_2

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.iris.base_logic.lib.subpreds.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.ivar_2__code.
Require Import zoo_std.ivar_2__types.
Require Import zoo.options.

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

Class Ivar2G Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] ivar_2۰G۰mutex۰G :: MutexG Σ
  ; #[local] ivar_2۰G۰lstate۰G :: OneshotG Σ unit val
  ; #[local] ivar_2۰G۰consumer۰G :: SubpredsG Σ val
  }.

Definition ivar_2۰Σ :=
  #[mutex۰Σ
  ; oneshot۰Σ unit val
  ; subpreds۰Σ val
  ].
#[global] Instance subGｰivar_2۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG ivar_2۰Σ Σ →
  Ivar2G Σ .

Module base.
  Section ivar_2۰G.
    Context `{ivar_2۰G : Ivar2G Σ}.

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

    Record ivar_2۰name :=
      { ivar_2۰name۰mutex : val
      ; ivar_2۰name۰condition : val
      ; ivar_2۰name۰lstate : gname
      ; ivar_2۰name۰consumer : gname
      }.
    Implicit Type γ : ivar_2۰name.

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

    #[local] Definition lstate۰unset₁' γ_lstate :=
      oneshot۰pending γ_lstate (DfracOwn (1/3)) ().
    #[local] Definition lstate۰unset₁ γ :=
      lstate۰unset₁' γ.(ivar_2۰name۰lstate).
    #[local] Definition lstate۰unset₂' γ_lstate :=
      oneshot۰pending γ_lstate (DfracOwn (2/3)) ().
    #[local] Definition lstate۰unset₂ γ :=
      lstate۰unset₂' γ.(ivar_2۰name۰lstate).
    #[local] Definition lstate۰set γ :=
      oneshot۰shot γ.(ivar_2۰name۰lstate).

    #[local] Definition consumer۰auth' :=
      subpreds۰auth.
    #[local] Definition consumer۰auth γ :=
      consumer۰auth' γ.(ivar_2۰name۰consumer).
    #[local] Definition consumer۰frag' :=
      subpreds۰frag.
    #[local] Definition consumer۰frag γ :=
      consumer۰frag' γ.(ivar_2۰name۰consumer).

    #[local] Definition inv۰state۰unset γ :=
      lstate۰unset₁ γ.
    #[local] Instance : CustomIpat "inv۰state۰unset" :=
      " {>;}Hlstate_unset₁ ".
    #[local] Definition inv۰state۰set γ Ξ v : iProp Σ :=
      lstate۰set γ v ∗
      □ Ξ v.
    #[local] Instance : CustomIpat "inv۰state۰set" :=
      " ( {>;}#Hlstate_set{_{}} & #HΞ{_{}} ) ".
    #[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.[result] ↦ state ∗
      consumer۰auth γ Ψ state ∗
      inv۰state γ Ξ state.
    #[local] Instance : CustomIpat "inv۰inner" :=
      " ( %state & H𝑡_result & Hconsumer_auth & Hstate ) ".
    Definition ivar_2۰inv t γ Ψ Ξ : iProp Σ :=
      t.[mutex] ↦□ γ.(ivar_2۰name۰mutex) ∗
      mutex۰inv γ.(ivar_2۰name۰mutex) True ∗
      t.[condition] ↦□ γ.(ivar_2۰name۰condition) ∗
      condition۰inv γ.(ivar_2۰name۰condition) ∗
      inv nroot (inv۰inner t γ Ψ Ξ).
    #[local] Instance : CustomIpat "inv" :=
      " ( #Ht_mutex & #Hmutex_inv & #Ht_condition & #Hcondition_inv & #Hinv ) ".

    Definition ivar_2۰producer :=
      lstate۰unset₂.
    #[local] Instance : CustomIpat "producer" :=
      " Hlstate_unset₂{_{}} ".

    Definition ivar_2۰consumer :=
      consumer۰frag.
    #[local] Instance : CustomIpat "consumer" :=
      " Hconsumer{}_frag ".

    Definition ivar_2۰result :=
      lstate۰set.
    #[local] Instance : CustomIpat "result" :=
      " #Hlstate_set{_{}} ".
    Definition ivar_2۰resolved γ : iProp Σ :=
      ∃ v,
      ivar_2۰result γ v.

    Definition ivar_2۰synchronized γ : iProp Σ :=
      True.

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

    #[global] Instance ivar_2۰producerｰtimeless γ :
      Timeless (ivar_2۰producer γ).
    #[global] Instance ivar_2۰resultｰtimeless γ v :
      Timeless (ivar_2۰result γ v).
    #[global] Instance ivar_2۰synchronizedｰtimeless γ :
      Timeless (ivar_2۰synchronized γ).

    #[global] Instance ivar_2۰invｰpersistent t γ Ψ Ξ :
      Persistent (ivar_2۰inv t γ Ψ Ξ).
    #[global] Instance ivar_2۰resultｰpersistent γ v :
      Persistent (ivar_2۰result γ v).
    #[global] Instance ivar_2۰synchronizedｰpersistent γ :
      Persistent (ivar_2۰synchronized γ).

    #[local] Lemma lstateｰalloc :
      ⊢ |==>
        ∃ γ_lstate,
        lstate۰unset₁' γ_lstate ∗
        lstate۰unset₂' γ_lstate.
    #[local] Lemma lstate۰unset₂ｰexclusive γ :
      lstate۰unset₂ γ -∗
      lstate۰unset₂ γ -∗
      False.
    #[local] Lemma lstate۰setｰagree γ v1 v2 :
      lstate۰set γ v1 -∗
      lstate۰set γ v2 -∗
      ⌜v1 = v2⌝.
    #[local] Lemma lstateｰunset₁ｰset γ v :
      lstate۰unset₁ γ -∗
      lstate۰set γ v -∗
      False.
    #[local] Lemma lstateｰunset₂ｰset γ v :
      lstate۰unset₂ γ -∗
      lstate۰set γ v -∗
      False.
    #[local] Lemma lstateｰupdate {γ} v :
      lstate۰unset₁ γ -∗
      lstate۰unset₂ γ ==∗
      lstate۰set γ v.

    #[local] Lemma consumerｰalloc Ψ :
      ⊢ |==>
        ∃ γ_consumer,
        consumer۰auth' γ_consumer Ψ None ∗
        consumer۰frag' γ_consumer Ψ.
    #[local] Lemma consumerｰwand {γ Ψ state Χ1} Χ2 E :
      ▷ consumer۰auth γ Ψ state -∗
      consumer۰frag γ Χ1 -∗
      (∀ v, Χ1 v -∗ Χ2 v) ={E}=∗
        ▷ consumer۰auth γ Ψ state ∗
        consumer۰frag γ Χ2.
    #[local] Lemma consumerｰdivide {γ Ψ state} Χs E :
      ▷ consumer۰auth γ Ψ state -∗
      consumer۰frag γ (λ v, [∗ list] Χ ∈ Χs, Χ v) ={E}=∗
        ▷ consumer۰auth γ Ψ state ∗
        [∗ list] Χ ∈ Χs, consumer۰frag γ Χ.
    #[local] Lemma consumerｰproduce {γ Ψ} v :
      consumer۰auth γ Ψ None -∗
      Ψ v -∗
      consumer۰auth γ Ψ (Some v).
    #[local] Lemma consumerｰconsume γ Ψ v Χ E :
      ▷ consumer۰auth γ Ψ (Some v) -∗
      consumer۰frag γ Χ ={E}=∗
        ▷ consumer۰auth γ Ψ (Some v) ∗
        ▷^2 Χ v.

    Lemma ivar_2۰producerｰexclusive γ :
      ivar_2۰producer γ -∗
      ivar_2۰producer γ -∗
      False.

    Lemma ivar_2۰consumerｰwand {t γ Ψ Ξ Χ1} Χ2 :
      ivar_2۰inv t γ Ψ Ξ -∗
      ivar_2۰consumer γ Χ1 -∗
      (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
      ivar_2۰consumer γ Χ2.
    Lemma ivar_2۰consumerｰdivide {t γ Ψ Ξ} Χs :
      ivar_2۰inv t γ Ψ Ξ -∗
      ivar_2۰consumer γ (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
      [∗ list] Χ ∈ Χs, ivar_2۰consumer γ Χ.

    Lemma ivar_2۰resultｰagree γ v1 v2 :
      ivar_2۰result γ v1 -∗
      ivar_2۰result γ v2 -∗
      ⌜v1 = v2⌝.

    Lemma ivar_2ｰproducerｰresult γ v :
      ivar_2۰producer γ -∗
      ivar_2۰result γ v -∗
      False.

    Lemma ivar_2ｰinvｰresult t γ Ψ Ξ v :
      ivar_2۰inv t γ Ψ Ξ -∗
      ivar_2۰result γ v -∗
      ivar_2۰synchronized γ ={⊤}=∗
      ▷ □ Ξ v.
    Lemma ivar_2ｰinvｰresultｰconsumer t γ Ψ Ξ v Χ :
      ivar_2۰inv t γ Ψ Ξ -∗
      ivar_2۰result γ v -∗
      ivar_2۰synchronized γ -∗
      ivar_2۰consumer γ Χ ={⊤}=∗
        ▷^2 Χ v ∗
        ▷ □ Ξ v.

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

    Lemma ivar_2٠makeｰspec Ψ Ξ v :
      {{{
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}}
        ivar_2٠make v
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰result γ v ∗
        ivar_2۰synchronized γ ∗
        ivar_2۰consumer γ Ψ
      }}}.

    Lemma ivar_2٠try_getｰspec t γ Ψ Ξ :
      {{{
        ivar_2۰inv t γ Ψ Ξ
      }}}
        ivar_2٠try_get #t
      {{{
        o
      , RET o;
        if o is Some v then
          £ 2 ∗
          ivar_2۰result γ v ∗
          ivar_2۰synchronized γ
        else
          True
      }}}.
    Lemma ivar_2٠try_getｰspecｰresult t γ Ψ Ξ v :
      {{{
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰result γ v
      }}}
        ivar_2٠try_get #t
      {{{
        RET Some v;
        £ 2 ∗
        ivar_2۰synchronized γ
      }}}.

    Lemma ivar_2٠is_unsetｰspec t γ Ψ Ξ :
      {{{
        ivar_2۰inv t γ Ψ Ξ
      }}}
        ivar_2٠is_unset #t
      {{{
        b
      , RET #b;
        if b then
          True
        else
          £ 2 ∗
          ivar_2۰resolved γ
      }}}.
    Lemma ivar_2٠is_unsetｰspecｰresult t γ Ψ Ξ v :
      {{{
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰result γ v
      }}}
        ivar_2٠is_unset #t
      {{{
        RET false;
        £ 2
      }}}.

    Lemma ivar_2٠is_setｰspec t γ Ψ Ξ :
      {{{
        ivar_2۰inv t γ Ψ Ξ
      }}}
        ivar_2٠is_set #t
      {{{
        b
      , RET #b;
        if b then
          £ 2 ∗
          ivar_2۰resolved γ
        else
          True
      }}}.
    Lemma ivar_2٠is_setｰspecｰresult t γ Ψ Ξ v :
      {{{
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰result γ v
      }}}
        ivar_2٠is_set #t
      {{{
        RET true;
        £ 2
      }}}.

    Lemma ivar_2٠getｰspec t γ Ψ Ξ :
      {{{
        ivar_2۰inv t γ Ψ Ξ
      }}}
        ivar_2٠get #t
      {{{
        v
      , RET v;
        £ 2 ∗
        ivar_2۰result γ v ∗
        ivar_2۰synchronized γ
      }}}.
    Lemma ivar_2٠getｰspecｰresult t γ Ψ Ξ v :
      {{{
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰result γ v
      }}}
        ivar_2٠get #t
      {{{
        RET v;
        £ 2 ∗
        ivar_2۰synchronized γ
      }}}.

    Lemma ivar_2٠setｰspec t γ Ψ Ξ v :
      {{{
        ivar_2۰inv t γ Ψ Ξ ∗
        ivar_2۰producer γ ∗
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}}
        ivar_2٠set #t v
      {{{
        RET ();
        ivar_2۰result γ v
      }}}.
  End ivar_2۰G.

  #[global] Opaque ivar_2۰inv.
  #[global] Opaque ivar_2۰producer.
  #[global] Opaque ivar_2۰consumer.
  #[global] Opaque ivar_2۰result.
  #[global] Opaque ivar_2۰synchronized.
End base.

Require zoo_std.ivar_2__opaque.

Section ivar_2۰G.
  Context `{ivar_2۰G : Ivar2G Σ}.

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

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

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

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

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

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

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

  #[global] Instance ivar_2۰producerｰtimeless t :
    Timeless (ivar_2۰producer t).
  #[global] Instance ivar_2۰resultｰtimeless t v :
    Timeless (ivar_2۰result t v).
  #[global] Instance ivar_2۰synchronizedｰtimeless t :
    Timeless (ivar_2۰synchronized t).

  #[global] Instance ivar_2۰invｰpersistent t Ψ Ξ :
    Persistent (ivar_2۰inv t Ψ Ξ).
  #[global] Instance ivar_2۰resultｰpersistent t v :
    Persistent (ivar_2۰result t v).
  #[global] Instance ivar_2۰synchronizedｰpersistent t :
    Persistent (ivar_2۰synchronized t).

  Lemma ivar_2۰producerｰexclusive t :
    ivar_2۰producer t -∗
    ivar_2۰producer t -∗
    False.

  Lemma ivar_2۰consumerｰwand {t Ψ Ξ Χ1} Χ2 :
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰consumer t Χ1 -∗
    (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
    ivar_2۰consumer t Χ2.
  Lemma ivar_2۰consumerｰdivide {t Ψ Ξ} Χs :
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰consumer t (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
    [∗ list] Χ ∈ Χs, ivar_2۰consumer t Χ.
  Lemma ivar_2۰consumerｰsplit {t Ψ Ξ} Χ1 Χ2 :
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
      ivar_2۰consumer t Χ1 ∗
      ivar_2۰consumer t Χ2.
  Lemma ivar_2۰resultｰagree t v1 v2 :
    ivar_2۰result t v1 -∗
    ivar_2۰result t v2 -∗
    ⌜v1 = v2⌝.

  Lemma ivar_2ｰproducerｰresult t v :
    ivar_2۰producer t -∗
    ivar_2۰result t v -∗
    False.

  Lemma ivar_2ｰinvｰresult t Ψ Ξ v :
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰result t v -∗
    ivar_2۰synchronized t ={⊤}=∗
    ▷ □ Ξ v.
  Lemma ivar_2ｰinvｰresult' t Ψ Ξ v :
    £ 1 -∗
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰result t v -∗
    ivar_2۰synchronized t ={⊤}=∗
    □ Ξ v.
  Lemma ivar_2ｰinvｰresultｰconsumer t Ψ Ξ v Χ :
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰result t v -∗
    ivar_2۰synchronized t -∗
    ivar_2۰consumer t Χ ={⊤}=∗
      ▷^2 Χ v ∗
      ▷ □ Ξ v.
  Lemma ivar_2ｰinvｰresultｰconsumer' t Ψ Ξ v Χ :
    £ 2 -∗
    ivar_2۰inv t Ψ Ξ -∗
    ivar_2۰result t v -∗
    ivar_2۰synchronized t -∗
    ivar_2۰consumer t Χ ={⊤}=∗
      Χ v ∗
      □ Ξ v.

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

  Lemma ivar_2٠makeｰspec Ψ Ξ v :
    {{{
      ▷ Ψ v ∗
      ▷ □ Ξ v
    }}}
      ivar_2٠make v
    {{{
      t
    , RET t;
      ivar_2۰inv t Ψ Ξ ∗
      ivar_2۰result t v ∗
      ivar_2۰consumer t Ψ
    }}}.

  Lemma ivar_2٠try_getｰspec t Ψ Ξ :
    {{{
      ivar_2۰inv t Ψ Ξ
    }}}
      ivar_2٠try_get t
    {{{
      o
    , RET o;
      if o is Some v then
        £ 2 ∗
        ivar_2۰result t v ∗
        ivar_2۰synchronized t
      else
        True
    }}}.
  Lemma ivar_2٠try_getｰspecｰresult t Ψ Ξ v :
    {{{
      ivar_2۰inv t Ψ Ξ ∗
      ivar_2۰result t v
    }}}
      ivar_2٠try_get t
    {{{
      RET Some v;
      £ 2 ∗
      ivar_2۰synchronized t
    }}}.

  Lemma ivar_2٠is_unsetｰspec t Ψ Ξ :
    {{{
      ivar_2۰inv t Ψ Ξ
    }}}
      ivar_2٠is_unset t
    {{{
      b
    , RET #b;
      if b then
        True
      else
        £ 2 ∗
        ivar_2۰resolved t
    }}}.
  Lemma ivar_2٠is_unsetｰspecｰresult t Ψ Ξ v :
    {{{
      ivar_2۰inv t Ψ Ξ ∗
      ivar_2۰result t v
    }}}
      ivar_2٠is_unset t
    {{{
      RET false;
      £ 2
    }}}.

  Lemma ivar_2٠is_setｰspec t Ψ Ξ :
    {{{
      ivar_2۰inv t Ψ Ξ
    }}}
      ivar_2٠is_set t
    {{{
      b
    , RET #b;
      if b then
        £ 2 ∗
        ivar_2۰resolved t
      else
        True
    }}}.
  Lemma ivar_2٠is_setｰspecｰresult t Ψ Ξ v :
    {{{
      ivar_2۰inv t Ψ Ξ ∗
      ivar_2۰result t v
    }}}
      ivar_2٠is_set t
    {{{
      RET true;
      £ 2
    }}}.

  Lemma ivar_2٠getｰspec t Ψ Ξ :
    {{{
      ivar_2۰inv t Ψ Ξ
    }}}
      ivar_2٠get t
    {{{
      v
    , RET v;
      £ 2 ∗
      ivar_2۰result t v ∗
      ivar_2۰synchronized t
    }}}.

  Lemma ivar_2٠setｰspec t Ψ Ξ v :
    {{{
      ivar_2۰inv t Ψ Ξ ∗
      ivar_2۰producer t ∗
      ▷ Ψ v ∗
      ▷ □ Ξ v
    }}}
      ivar_2٠set t v
    {{{
      RET ();
      ivar_2۰result t v
    }}}.
End ivar_2۰G.

#[global] Opaque ivar_2۰inv.
#[global] Opaque ivar_2۰producer.
#[global] Opaque ivar_2۰consumer.
#[global] Opaque ivar_2۰result.
#[global] Opaque ivar_2۰synchronized.