Library zoo.program_logic.prophet_wise

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.base_logic Require Import
  lib.agree
  lib.mono_list.
From zoo.language Require Import
  notations.
From zoo.program_logic Require Export
  prophet_typed.
From zoo.diaframe Require Import
  diaframe.
From zoo Require Import
  options.

Class ProphetWiseStrongG Σ `{zoo_G : !ZooG Σ} prophet :=
  { #[local] prophet_wise_strong_G_full_G :: AgreeG Σ (leibnizO (list prophet.(prophet_typed_strong_type)))
  ; #[local] prophet_wise_strong_G_past_G :: MonoListG Σ prophet.(prophet_typed_strong_type)
  }.

Definition prophet_wise_strong_Σ prophet :=
  #[agree_Σ (leibnizO (list prophet.(prophet_typed_strong_type)))
  ; mono_list_Σ prophet.(prophet_typed_strong_type)
  ].
#[global] Instance subG_prophet_wise_strong_Σ Σ `{zoo_G : !ZooG Σ} prophet :
  subG (prophet_wise_strong_Σ prophet) Σ →
  ProphetWiseStrongG Σ prophet.

Section prophet_wise_G.
  Context (prophet : prophet_typed_strong).
  Context `{prophet_wise_G : ProphetWiseStrongG Σ prophet}.

  Record prophet_wise_strong_name :=
    { prophet_wise_strong_name_full : gname
    ; prophet_wise_strong_name_past : gname
    }.

  #[global] Instance prophet_wise_strong_name_eq_dec : EqDecision prophet_wise_strong_name :=
    ltac:(solve_decision).
  #[global] Instance prophet_wise_strong_name_countable :
    Countable prophet_wise_strong_name.

  Definition prophet_wise_strong_full γ prophs : iProp Σ :=
    agree_on γ.(prophet_wise_strong_name_full) prophs.
  #[local] Instance : CustomIpat "full" :=
    " #Hfull{} ".

  Definition prophet_wise_strong_model pid γ past prophs : iProp Σ :=
    prophet_wise_strong_full γ (past ++ prophs) ∗
    mono_list_auth γ.(prophet_wise_strong_name_past) (DfracOwn 1) past ∗
    prophet_typed_strong_model prophet pid prophs.
  #[local] Instance : CustomIpat "model" :=
    " ( #Hfull{} & Hpast{}_auth & Hmodel{} ) ".

  Definition prophet_wise_strong_snapshot γ past prophs : iProp Σ :=
    prophet_wise_strong_full γ (past ++ prophs) ∗
    mono_list_lb γ.(prophet_wise_strong_name_past) past.
  #[local] Instance : CustomIpat "snapshot" :=
    " ( #Hfull{suff} & #Hpast_lb ) ".

  Definition prophet_wise_strong_lb γ lb : iProp Σ :=
    ∃ past,
    prophet_wise_strong_snapshot γ past lb.
  #[local] Instance : CustomIpat "lb" :=
    " ( %past{suff} & Hsnapshot ) ".

  #[global] Instance prophet_wise_strong_full_timeless γ prophs :
    Timeless (prophet_wise_strong_full γ prophs).
  #[global] Instance prophet_wise_strong_model_timeless pid γ past prophs :
    Timeless (prophet_wise_strong_model pid γ past prophs).
  #[global] Instance prophet_wise_strong_snapshot_timeless γ past prophs :
    Timeless (prophet_wise_strong_snapshot γ past prophs).
  #[global] Instance prophet_wise_strong_lb_timeless γ lb :
    Timeless (prophet_wise_strong_lb γ lb).

  #[global] Instance prophet_wise_strong_full_persistent γ prophs :
    Persistent (prophet_wise_strong_full γ prophs).
  #[global] Instance prophet_wise_strong_snapshot_persistent γ past prophs :
    Persistent (prophet_wise_strong_snapshot γ past prophs).
  #[global] Instance prophet_wise_strong_lb_persistent γ lb :
    Persistent (prophet_wise_strong_lb γ lb).

  Lemma prophet_wise_strong_model_exclusive pid γ1 past1 prophs1 γ2 past2 prophs2 :
    prophet_wise_strong_model pid γ1 past1 prophs1 -∗
    prophet_wise_strong_model pid γ2 past2 prophs2 -∗
    False.

  Lemma prophet_wise_strong_full_get pid γ past prophs :
    prophet_wise_strong_model pid γ past prophs ⊢
    prophet_wise_strong_full γ (past ++ prophs).
  Lemma prophet_wise_strong_full_get' pid γ past prophs :
    prophet_wise_strong_model pid γ past prophs ⊢
      ∃ prophs',
      prophet_wise_strong_full γ prophs'.
  Lemma prophet_wise_strong_full_valid pid γ past prophs1 prophs2 :
    prophet_wise_strong_model pid γ past prophs1 -∗
    prophet_wise_strong_full γ prophs2 -∗
    ⌜prophs2 = past ++ prophs1⌝.
  Lemma prophet_wise_strong_full_agree γ prophs1 prophs2 :
    prophet_wise_strong_full γ prophs1 -∗
    prophet_wise_strong_full γ prophs2 -∗
    ⌜prophs1 = prophs2⌝.

  Lemma prophet_wise_strong_snapshot_get pid γ past prophs :
    prophet_wise_strong_model pid γ past prophs ⊢
    prophet_wise_strong_snapshot γ past prophs.
  Lemma prophet_wise_strong_snapshot_valid pid γ past1 prophs1 past2 prophs2 :
    prophet_wise_strong_model pid γ past1 prophs1 -∗
    prophet_wise_strong_snapshot γ past2 prophs2 -∗
      ∃ past3,
      ⌜past1 = past2 ++ past3⌝ ∗
      ⌜prophs2 = past3 ++ prophs1⌝.

  Lemma prophet_wise_strong_lb_get pid γ past prophs :
    prophet_wise_strong_model pid γ past prophs ⊢
    prophet_wise_strong_lb γ prophs.
  Lemma prophet_wise_strong_lb_valid pid γ past prophs lb :
    prophet_wise_strong_model pid γ past prophs -∗
    prophet_wise_strong_lb γ lb -∗
      ∃ past1 past2,
      ⌜past = past1 ++ past2⌝ ∗
      ⌜lb = past2 ++ prophs⌝.

  Lemma prophet_wise_strong_wp_proph E :
    {{{
      True
    }}}
      Proph @ E
    {{{
      pid γ prophs
    , RET #pid;
      prophet_wise_strong_model pid γ [] prophs
    }}}.

  Lemma prophet_wise_strong_wp_resolve e pid v γ past prophs E Φ :
    Atomic e →
    to_val e = None →
    prophet_wise_strong_model pid γ past prophs -∗
    WP e @ E {{ w,
      ∃ proph,
      ⌜(w, v) = prophet.(prophet_typed_strong_to_val) proph⌝ ∗
        ∀ prophs',
        ⌜prophs = proph :: prophs'⌝ -∗
        prophet_wise_strong_model pid γ (past ++ [proph]) prophs' -∗
        Φ w
    }} -∗
    WP Resolve e #pid v @ E {{ Φ }}.
End prophet_wise_G.

#[global] Opaque prophet_wise_strong_full.
#[global] Opaque prophet_wise_strong_model.
#[global] Opaque prophet_wise_strong_snapshot.
#[global] Opaque prophet_wise_strong_lb.

Class ProphetWiseG Σ `{zoo_G : !ZooG Σ} prophet :=
  { #[local] prophet_wise_G :: ProphetWiseStrongG Σ prophet
  }.

Definition prophet_wise_Σ prophet :=
  #[prophet_wise_strong_Σ prophet
  ].
#[global] Instance subG_prophet_wise_Σ Σ `{zoo_G : !ZooG Σ} prophet :
  subG (prophet_wise_Σ prophet) Σ →
  ProphetWiseG Σ prophet.

Section prophet_wise_G.
  Context (prophet : prophet_typed).
  Context `{prophet_wise_G : ProphetWiseG Σ prophet}.

  Definition prophet_wise_name :=
    prophet_wise_strong_name.
  Implicit Types γ : prophet_wise_name.

  Definition prophet_wise_full γ prophs : iProp Σ :=
    ∃ sprophs,
    ⌜prophs = sprophs.*2⌝ ∗
    prophet_wise_strong_full prophet γ sprophs.
  #[local] Instance : CustomIpat "full" :=
    " ( %sprophs{} & -> & Hfull{} ) ".

  Definition prophet_wise_model pid γ past prophs : iProp Σ :=
    ∃ spast sprophs,
    ⌜past = spast.*2⌝ ∗
    ⌜prophs = sprophs.*2⌝ ∗
    prophet_wise_strong_model prophet pid γ spast sprophs.
  #[local] Instance : CustomIpat "model" :=
    " ( %spast{} & %sprophs{} & -> & -> & Hmodel{} ) ".

  Definition prophet_wise_snapshot γ past prophs : iProp Σ :=
    ∃ spast sprophs,
    ⌜past = spast.*2⌝ ∗
    ⌜prophs = sprophs.*2⌝ ∗
    prophet_wise_strong_snapshot prophet γ spast sprophs.
  #[local] Instance : CustomIpat "snapshot" :=
    " ( %spast{} & %sprophs{} & -> & -> & Hsnapshot ) ".

  Definition prophet_wise_lb γ lb : iProp Σ :=
    ∃ slb,
    ⌜lb = slb.*2⌝ ∗
    prophet_wise_strong_lb prophet γ slb.
  #[local] Instance : CustomIpat "lb" :=
    " ( %slb & -> & Hlb ) ".

  #[global] Instance prophet_wise_full_timeless γ prophs :
    Timeless (prophet_wise_full γ prophs).
  #[global] Instance prophet_wise_model_timeless pid γ past prophs :
    Timeless (prophet_wise_model pid γ past prophs).
  #[global] Instance prophet_wise_snapshot_timeless γ past prophs :
    Timeless (prophet_wise_snapshot γ past prophs).
  #[global] Instance prophet_wise_lb_timeless γ lb :
    Timeless (prophet_wise_lb γ lb).
  #[global] Instance prophet_wise_full_persistent γ prophs :
    Persistent (prophet_wise_full γ prophs).
  #[global] Instance prophet_wise_snapshot_persistent γ past prophs :
    Persistent (prophet_wise_snapshot γ past prophs).
  #[global] Instance prophet_wise_lb_persistent γ lb :
    Persistent (prophet_wise_lb γ lb).

  Lemma prophet_wise_model_exclusive pid γ1 past1 prophs1 γ2 past2 prophs2 :
    prophet_wise_model pid γ1 past1 prophs1 -∗
    prophet_wise_model pid γ2 past2 prophs2 -∗
    False.

  Lemma prophet_wise_full_get pid γ past prophs :
    prophet_wise_model pid γ past prophs ⊢
    prophet_wise_full γ (past ++ prophs).
  Lemma prophet_wise_full_get' pid γ past prophs :
    prophet_wise_model pid γ past prophs ⊢
      ∃ prophs',
      prophet_wise_full γ prophs'.
  Lemma prophet_wise_full_valid pid γ past prophs1 prophs2 :
    prophet_wise_model pid γ past prophs1 -∗
    prophet_wise_full γ prophs2 -∗
    ⌜prophs2 = past ++ prophs1⌝.
  Lemma prophet_wise_full_agree γ prophs1 prophs2 :
    prophet_wise_full γ prophs1 -∗
    prophet_wise_full γ prophs2 -∗
    ⌜prophs1 = prophs2⌝.

  Lemma prophet_wise_snapshot_get pid γ past prophs :
    prophet_wise_model pid γ past prophs ⊢
    prophet_wise_snapshot γ past prophs.
  Lemma prophet_wise_snapshot_valid pid γ past1 prophs1 past2 prophs2 :
    prophet_wise_model pid γ past1 prophs1 -∗
    prophet_wise_snapshot γ past2 prophs2 -∗
      ∃ past3,
      ⌜past1 = past2 ++ past3⌝ ∗
      ⌜prophs2 = past3 ++ prophs1⌝.

  Lemma prophet_wise_lb_get pid γ past prophs :
    prophet_wise_model pid γ past prophs -∗
    prophet_wise_lb γ prophs.
  Lemma prophet_wise_lb_valid pid γ past prophs lb :
    prophet_wise_model pid γ past prophs -∗
    prophet_wise_lb γ lb -∗
      ∃ past1 past2,
      ⌜past = past1 ++ past2⌝ ∗
      ⌜lb = past2 ++ prophs⌝.

  Lemma prophet_wise_wp_proph E :
    {{{
      True
    }}}
      Proph @ E
    {{{
      pid γ prophs
    , RET #pid;
      prophet_wise_model pid γ [] prophs
    }}}.

  Lemma prophet_wise_wp_resolve proph e pid v γ past prophs E Φ :
    Atomic e →
    to_val e = None →
    v = prophet.(prophet_typed_to_val) proph →
    prophet_wise_model pid γ past prophs -∗
    WP e @ E {{ w,
      ∀ prophs',
      ⌜prophs = proph :: prophs'⌝ -∗
      prophet_wise_model pid γ (past ++ [proph]) prophs' -∗
      Φ w
    }} -∗
    WP Resolve e #pid v @ E {{ Φ }}.
End prophet_wise_G.

#[global] Opaque prophet_wise_name.
#[global] Opaque prophet_wise_full.
#[global] Opaque prophet_wise_model.
#[global] Opaque prophet_wise_snapshot.
#[global] Opaque prophet_wise_lb.