Library zoo_std.lazy

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.base_logic Require Import
  lib.oneshot
  lib.subpreds.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  base
  lazy__code.
From zoo_std Require Import
  lazy__types
  mutex.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types v fn mtx : val.

Class LazyG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] lazy_G_mutex_G :: MutexG Σ
  ; #[local] lazy_G_lstate_G :: OneshotG Σ unit val
  ; #[local] lazy_G_consumer_G :: SubpredsG Σ val
  }.

Definition lazy_Σ :=
  #[mutex_Σ
  ; oneshot_Σ unit val
  ; subpreds_Σ val
  ].
#[global] Instance subG_lazy_Σ Σ `{zoo_G : !ZooG Σ} :
  subG lazy_Σ Σ →
  LazyG Σ .

Module base.
  Section lazy_G.
    Context `{lazy_G : LazyG Σ}.

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

    Record lazy_name :=
      { lazy_name_thunk : val
      ; lazy_name_lstate : gname
      ; lazy_name_consumer : gname
      }.
    Implicit Types γ : lazy_name.

    #[global] Instance lazy_name_eq_dec : EqDecision lazy_name :=
      ltac:(solve_decision).
    #[global] Instance lazy_name_countable :
      Countable lazy_name.

    Variant state :=
      | Unset
      | Setting mtx
      | Set_ v.
    Implicit Types state : state.

    #[local] Instance state_inhabited : Inhabited state :=
      populate Unset.

    #[local] Definition state_to_bool state :=
      match state with
      | Set_ _ ⇒
          true
      | _ ⇒
          false
      end.
    #[local] Definition state_to_option state :=
      match state with
      | Set_ v ⇒
          Some v
      | _ ⇒
          None
      end.
    #[local] Definition state_to_val γ state :=
      match state with
      | Unset ⇒
          ‘Unset( γ.(lazy_name_thunk) )
      | Setting mtx ⇒
          ‘Setting( mtx )
      | Set_ v ⇒
          ‘Set( v )
      end%V.

    #[local] Definition lstate_unset₁' γ_lstate :=
      oneshot_pending γ_lstate (DfracOwn (1/3)) ().
    #[local] Definition lstate_unset₁ γ :=
      lstate_unset₁' γ.(lazy_name_lstate).
    #[local] Definition lstate_unset₂' γ_lstate :=
      oneshot_pending γ_lstate (DfracOwn (2/3)) ().
    #[local] Definition lstate_unset₂ γ :=
      lstate_unset₂' γ.(lazy_name_lstate).
    #[local] Definition lstate_set' γ_lstate :=
      oneshot_shot γ_lstate.
    #[local] Definition lstate_set γ :=
      lstate_set' γ.(lazy_name_lstate).

    #[local] Definition consumer_auth' :=
      subpreds_auth.
    #[local] Definition consumer_auth γ :=
      consumer_auth' γ.(lazy_name_consumer).
    #[local] Definition consumer_frag' :=
      subpreds_frag.
    #[local] Definition consumer_frag γ :=
      consumer_frag' γ.(lazy_name_consumer).

    Definition lazy_result :=
      lstate_set.
    #[local] Instance : CustomIpat "result" :=
      " #Hlstate_set{_{}} ".
    Definition lazy_resolved γ : iProp Σ :=
      ∃ v,
      lazy_result γ v.

    #[local] Definition inv_state_unset γ Ψ Ξ : iProp Σ :=
      lstate_unset₁ γ ∗
      lstate_unset₂ γ ∗
      WP γ.(lazy_name_thunk) () {{ v,
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}.
    #[local] Instance : CustomIpat "inv_state_unset" :=
      " ( {>;}Hlstate_unset₁{_{}} & {>;}Hlstate_unset₂{_{}} & Hthunk ) ".
    #[local] Definition inv_state_setting γ mtx : iProp Σ :=
      lstate_unset₁ γ ∗
      mutex_inv mtx (lazy_resolved γ).
    #[local] Instance : CustomIpat "inv_state_setting" :=
      " ( {>;}Hlstate_unset₁{_{}} & #Hmtx_inv{_{}} ) ".
    #[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
      | Unset ⇒
          inv_state_unset γ Ψ Ξ
      | Setting mtx ⇒
          inv_state_setting γ mtx
      | Set_ v ⇒
          inv_state_set γ Ξ v
      end.

    #[local] Definition inv_inner t γ Ψ Ξ : iProp Σ :=
      ∃ state,
      t ↦ᵣ state_to_val γ state ∗
      consumer_auth γ Ψ (state_to_option state) ∗
      inv_state γ Ψ Ξ state.
    #[local] Instance : CustomIpat "inv_inner" :=
      " ( %state & Ht & Hconsumer_auth & Hstate ) ".
    Definition lazy_inv t γ Ψ Ξ : iProp Σ :=
      inv nroot (inv_inner t γ Ψ Ξ).
    #[local] Instance : CustomIpat "inv" :=
      " #Hinv ".

    Definition lazy_consumer :=
      consumer_frag.
    #[local] Instance : CustomIpat "consumer" :=
      " Hconsumer{}_frag ".

    #[global] Instance lazy_inv_contractive t γ n :
      Proper (
        (pointwise_relation _ (dist_later n)) ==>
        (pointwise_relation _ (dist_later n)) ==>
        (≡{n}≡)
      ) (lazy_inv t γ).
    #[global] Instance lazy_inv_proper t γ :
      Proper (
        (pointwise_relation _ (≡)) ==>
        (pointwise_relation _ (≡)) ==>
        (≡)
      ) (lazy_inv t γ).
    #[global] Instance lazy_consumer_contractive γ n :
      Proper (
        (pointwise_relation _ (dist_later n)) ==>
        (≡{n}≡)
      ) (lazy_consumer γ).
    #[global] Instance lazy_consumer_proper γ :
      Proper (
        (pointwise_relation _ (≡)) ==>
        (≡)
      ) (lazy_consumer γ).

    #[global] Instance lazy_result_timeless γ v :
      Timeless (lazy_result γ v).

    #[global] Instance lazy_inv_persistent t γ Ψ Ξ :
      Persistent (lazy_inv t γ Ψ Ξ).
    #[global] Instance lazy_result_persistent γ v :
      Persistent (lazy_result γ v).

    #[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 : option val} {Χ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 : option val} Χ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.

    #[local] Lemma inv_state_lstate_set γ Ψ Ξ state v :
      ▷ inv_state γ Ψ Ξ state -∗
      lstate_set γ v -∗
      ◇ (
        ⌜state = Set_ v⌝ ∗
        ▷ inv_state_set γ Ξ v
      ).

    Lemma lazy_consumer_wand {t γ Ψ Ξ Χ1} Χ2 :
      lazy_inv t γ Ψ Ξ -∗
      lazy_consumer γ Χ1 -∗
      (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
      lazy_consumer γ Χ2.
    Lemma lazy_consumer_divide {t γ Ψ Ξ} Χs :
      lazy_inv t γ Ψ Ξ -∗
      lazy_consumer γ (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
      [∗ list] Χ ∈ Χs, lazy_consumer γ Χ.

    Lemma lazy_result_agree γ v1 v2 :
      lazy_result γ v1 -∗
      lazy_result γ v2 -∗
      ⌜v1 = v2⌝.

    Lemma lazy_inv_result t γ Ψ Ξ v :
      lazy_inv t γ Ψ Ξ -∗
      lazy_result γ v ={⊤}=∗
      ▷ □ Ξ v.
    Lemma lazy_inv_result_consumer t γ Ψ Ξ v Χ :
      lazy_inv t γ Ψ Ξ -∗
      lazy_result γ v -∗
      lazy_consumer γ Χ ={⊤}=∗
        ▷^2 Χ v ∗
        ▷ □ Ξ v.

    Lemma lazy٠make𑁒spec Ψ Ξ fn :
      {{{
        WP fn () {{ v,
          ▷ Ψ v ∗
          ▷ □ Ξ v
        }}
      }}}
        lazy٠make fn
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        lazy_inv t γ Ψ Ξ ∗
        lazy_consumer γ Ψ
      }}}.

    Lemma lazy٠return𑁒spec Ψ Ξ v :
      {{{
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}}
        lazy٠return v
      {{{
        t γ
      , RET #t;
        meta_token t ⊤ ∗
        lazy_inv t γ Ψ Ξ ∗
        lazy_result γ v ∗
        lazy_consumer γ Ψ
      }}}.

    Lemma lazy٠is_set𑁒spec t γ Ψ Ξ :
      {{{
        lazy_inv t γ Ψ Ξ
      }}}
        lazy٠is_set #t
      {{{
        b
      , RET #b;
        if b then
          £ 2 ∗
          lazy_resolved γ
        else
          True
      }}}.
    Lemma lazy٠is_set𑁒spec_result t γ Ψ Ξ v :
      {{{
        lazy_inv t γ Ψ Ξ ∗
        lazy_result γ v
      }}}
        lazy٠is_set #t
      {{{
        RET true;
        £ 2
      }}}.

    Lemma lazy٠is_unset𑁒spec t γ Ψ Ξ :
      {{{
        lazy_inv t γ Ψ Ξ
      }}}
        lazy٠is_unset #t
      {{{
        b
      , RET #b;
        if b then
          True
        else
          £ 2 ∗
          lazy_resolved γ
      }}}.
    Lemma lazy٠is_unset𑁒spec_result t γ Ψ Ξ v :
      {{{
        lazy_inv t γ Ψ Ξ ∗
        lazy_result γ v
      }}}
        lazy٠is_unset #t
      {{{
        RET false;
        £ 2
      }}}.

    Lemma lazy٠get𑁒spec t γ Ψ Ξ :
      {{{
        lazy_inv t γ Ψ Ξ
      }}}
        lazy٠get #t
      {{{
        v
      , RET v;
        £ 2 ∗
        lazy_result γ v
      }}}.
    Lemma lazy٠get𑁒spec_result t γ Ψ Ξ v :
      {{{
        lazy_inv t γ Ψ Ξ ∗
        lazy_result γ v
      }}}
        lazy٠get #t
      {{{
        RET v;
        £ 2
      }}}.
  End lazy_G.

  #[global] Opaque lazy_inv.
  #[global] Opaque lazy_consumer.
  #[global] Opaque lazy_result.
End base.

From zoo_std Require
  lazy__opaque.

Section lazy_G.
  Context `{lazy_G : LazyG Σ}.

  Implicit Types 𝑡 : location.
  Implicit Types t : val.
  Implicit Types γ : base.lazy_name.
  Implicit Types Ψ Χ Ξ : val → iProp Σ.

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

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

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

  #[global] Instance lazy_inv_contractive t n :
    Proper (
      (pointwise_relation _ (dist_later n)) ==>
      (pointwise_relation _ (dist_later n)) ==>
      (≡{n}≡)
    ) (lazy_inv t).
  #[global] Instance lazy_inv_proper t :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (pointwise_relation _ (≡)) ==>
      (≡)
    ) (lazy_inv t).
  #[global] Instance lazy_consumer_contractive t n :
    Proper (
      (pointwise_relation _ (dist_later n)) ==>
      (≡{n}≡)
    ) (lazy_consumer t).
  #[global] Instance lazy_consumer_proper t :
    Proper (
      (pointwise_relation _ (≡)) ==>
      (≡)
    ) (lazy_consumer t).

  #[global] Instance lazy_result_timeless t v :
    Timeless (lazy_result t v).

  #[global] Instance lazy_inv_persistent t Ψ Ξ :
    Persistent (lazy_inv t Ψ Ξ).
  #[global] Instance lazy_result_persistent t v :
    Persistent (lazy_result t v).

  Lemma lazy_consumer_wand {t Ψ Ξ Χ1} Χ2 :
    lazy_inv t Ψ Ξ -∗
    lazy_consumer t Χ1 -∗
    (∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
    lazy_consumer t Χ2.
  Lemma lazy_consumer_divide {t Ψ Ξ} Χs :
    lazy_inv t Ψ Ξ -∗
    lazy_consumer t (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
    [∗ list] Χ ∈ Χs, lazy_consumer t Χ.
  Lemma lazy_consumer_split {t Ψ Ξ} Χ1 Χ2 :
    lazy_inv t Ψ Ξ -∗
    lazy_consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
      lazy_consumer t Χ1 ∗
      lazy_consumer t Χ2.
  Lemma lazy_result_agree t v1 v2 :
    lazy_result t v1 -∗
    lazy_result t v2 -∗
    ⌜v1 = v2⌝.

  Lemma lazy_inv_result t Ψ Ξ v :
    lazy_inv t Ψ Ξ -∗
    lazy_result t v ={⊤}=∗
    ▷ □ Ξ v.
  Lemma lazy_inv_result' t Ψ Ξ v :
    £ 1 -∗
    lazy_inv t Ψ Ξ -∗
    lazy_result t v ={⊤}=∗
    □ Ξ v.
  Lemma lazy_inv_result_consumer t Ψ Ξ v Χ :
    lazy_inv t Ψ Ξ -∗
    lazy_result t v -∗
    lazy_consumer t Χ ={⊤}=∗
      ▷^2 Χ v ∗
      ▷ □ Ξ v.
  Lemma lazy_inv_result_consumer' t Ψ Ξ v Χ :
    £ 2 -∗
    lazy_inv t Ψ Ξ -∗
    lazy_result t v -∗
    lazy_consumer t Χ ={⊤}=∗
      Χ v ∗
      □ Ξ v.

  Lemma lazy٠make𑁒spec Ψ Ξ fn :
    {{{
      WP fn () {{ v,
        ▷ Ψ v ∗
        ▷ □ Ξ v
      }}
    }}}
      lazy٠make fn
    {{{
      t
    , RET t;
      lazy_inv t Ψ Ξ ∗
      lazy_consumer t Ψ
    }}}.

  Lemma lazy٠return𑁒spec Ψ Ξ v :
    {{{
      ▷ Ψ v ∗
      ▷ □ Ξ v
    }}}
      lazy٠return v
    {{{
      t
    , RET t;
      lazy_inv t Ψ Ξ ∗
      lazy_result t v ∗
      lazy_consumer t Ψ
    }}}.

  Lemma lazy٠is_set𑁒spec t Ψ Ξ :
    {{{
      lazy_inv t Ψ Ξ
    }}}
      lazy٠is_set t
    {{{
      b
    , RET #b;
      if b then
        £ 2 ∗
        lazy_resolved t
      else
        True
    }}}.
  Lemma lazy٠is_set𑁒spec_result t Ψ Ξ v :
    {{{
      lazy_inv t Ψ Ξ ∗
      lazy_result t v
    }}}
      lazy٠is_set t
    {{{
      RET true;
      £ 2
    }}}.

  Lemma lazy٠is_unset𑁒spec t Ψ Ξ :
    {{{
      lazy_inv t Ψ Ξ
    }}}
      lazy٠is_unset t
    {{{
      b
    , RET #b;
      if b then
        True
      else
        £ 2 ∗
        lazy_resolved t
    }}}.
  Lemma lazy٠is_unset𑁒spec_result t Ψ Ξ v :
    {{{
      lazy_inv t Ψ Ξ ∗
      lazy_result t v
    }}}
      lazy٠is_unset t
    {{{
      RET false;
      £ 2
    }}}.

  Lemma lazy٠get𑁒spec t Ψ Ξ :
    {{{
      lazy_inv t Ψ Ξ
    }}}
      lazy٠get t
    {{{
      v
    , RET v;
      £ 2 ∗
      lazy_result t v
    }}}.
  Lemma lazy٠get𑁒spec_result t Ψ Ξ v :
    {{{
      lazy_inv t Ψ Ξ ∗
      lazy_result t v
    }}}
      lazy٠get t
    {{{
      RET v;
      £ 2
    }}}.
End lazy_G.

#[global] Opaque lazy_inv.
#[global] Opaque lazy_consumer.
#[global] Opaque lazy_result.