Library zoo_std.inf_array

Require Import Stdlib.Logic.FunctionalExtensionality.

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.function.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Export zoo_std.inf_array__code.
Require Import zoo_std.inf_array__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type l : location.
Implicit Type pid : prophet_id.
Implicit Type v v_resolve t fn : val.
Implicit Type us : list val.
Implicit Type vs : nat → val.

Class InfArrayG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] inf_array ۰ G ۰ mutex ۰ G :: MutexG Σ
  ; #[local] inf_array ۰ G ۰ model ۰ G :: TwinsG Σ (nat -d > val_O)
  }.

Definition inf_array ۰ Σ :=
  #[mutex ۰ Σ
  ; twins ۰ Σ (nat -d > val_O)
  ].
#[global] Instance subG ｰ inf_array ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG inf_array ۰ Σ Σ →
  InfArrayG Σ .

Section inf_array ۰ G.
  Context `{inf_array ۰ G : InfArrayG Σ}.

  Record metadata :=
    { metadata ۰ default : val
    ; metadata ۰ model : gname
    }.
  Implicit Type γ : metadata.

  #[local] Instance metadata ｰ eq_dec : EqDecision metadata :=
    ltac:(solve_decision).
  #[local] Instance metadata ｰ countable :
    Countable metadata.

  #[local] Definition model₁' γ_model vs :=
    twins ۰ twin₁ γ_model (DfracOwn 1) vs.
  #[local] Definition model₁ γ vs :=
    model₁' γ.(metadata ۰ model) vs.
  #[local] Definition model₂' γ_model vs :=
    twins ۰ twin₂ γ_model vs.
  #[local] Definition model₂ γ vs :=
    model₂' γ.(metadata ۰ model) vs.

  #[local] Definition inv₂ l γ us : iProp Σ :=
    ∃ data vs ,
    l .[data ] ↦ data ∗
    array ۰ model data (DfracOwn 1) us ∗
    model₂ γ vs ∗
    ⌜vs = λ i, if decide (i < length us) then us !!! i else γ.(metadata ۰ default)⌝.
  #[local] Instance : CustomIpat "inv₂" :=
    " ( %data & %vs & Hl_data & Hdata & Hmodel₂ & %Hvs ) ".
  #[local] Definition inv₁ l γ : iProp Σ :=
    ∃ us ,
    inv₂ l γ us.
  #[local] Instance : CustomIpat "inv₁" :=
    " ( %us{} & {{lazy}Hinv;(:inv₂)} ) ".
  Definition inf_array ۰ inv t : iProp Σ :=
    ∃ l γ mtx ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    l .[default ] ↦□ γ.(metadata ۰ default) ∗
    l .[mutex ] ↦□ mtx ∗
    mutex ۰ inv mtx (inv₁ l γ).
  #[local] Instance : CustomIpat "inv" :=
    " ( %l & %γ & %mtx & -> & #Hmeta & #Hl_mtx & #Hl_default & #Hmtx_inv ) ".

  Definition inf_array ۰ model t vs : iProp Σ :=
    ∃ l γ ,
    ⌜t = #l ⌝ ∗
    l ↪ γ ∗
    model₁ γ vs.
  #[local] Instance : CustomIpat "model" :=
    " ( %l_ & %γ_ & %Heq & #Hmeta_ & Hmodel₁ ) ".
  Definition inf_array ۰ model' t vs ₗ vs ᵣ :=
    inf_array ۰ model t (
      λ i,
        if decide (i < length vs ₗ) then vs ₗ !!! i else vs ᵣ (i - length vs ₗ)
    ).

  #[global] Instance inf_array ۰ inv ｰ persistent t :
    Persistent (inf_array ۰ inv t).

  #[global] Instance inf_array ۰ model ｰ ne t n :
    Proper (pointwise_relation nat (=) ==> (≡{n }≡)) (inf_array ۰ model t).
  #[global] Instance inf_array ۰ model ｰ proper t :
    Proper (pointwise_relation nat (=) ==> (≡)) (inf_array ۰ model t).

  #[global] Instance inf_array ۰ model ｰ timeless t vs :
    Timeless (inf_array ۰ model t vs).

  #[global] Instance inf_array ۰ model'ｰ ne t n :
    Proper ((=) ==> pointwise_relation nat (=) ==> (≡{n }≡)) (inf_array ۰ model' t).
  #[global] Instance inf_array ۰ model'ｰ proper t :
    Proper ((=) ==> pointwise_relation nat (=) ==> (≡)) (inf_array ۰ model' t).

  #[global] Instance inf_array ۰ model'ｰ timeless t vs ₗ vs ᵣ :
    Timeless (inf_array ۰ model' t vs ₗ vs ᵣ).

  #[local] Lemma model ｰ alloc default :
    ⊢ |==>
      ∃ γ_model ,
      model₁' γ_model (λ _, default) ∗
      model₂' γ_model (λ _, default).
  #[local] Lemma model ｰ agree γ vs1 vs2 :
    model₁ γ vs1 -∗
    model₂ γ vs2 -∗
    ⌜vs1 = vs2 ⌝.
  #[local] Lemma model ｰ update {γ vs1 vs2} vs :
    model₁ γ vs1 -∗
    model₂ γ vs2 ==∗
      model₁ γ vs ∗
      model₂ γ vs.

  Lemma inf_array ۰ model ｰ to ｰ model' {t vs} vs ₗ :
    (∀ i v, vs ₗ !! i = Some v → vs i = v) →
    inf_array ۰ model t vs ⊢
    inf_array ۰ model' t vs ₗ (λ i, vs (length vs ₗ + i)).
  Lemma inf_array ۰ model ｰ to ｰ model'ｰ replicate {t vs} n v :
    (∀ i, i < n → vs i = v) →
    inf_array ۰ model t vs ⊢
    inf_array ۰ model' t (replicate n v) (λ i, vs (n + i)).
  Lemma inf_array ۰ model ｰ to ｰ model'ｰ constant {t v} n :
    inf_array ۰ model t (λ _, v) ⊢
    inf_array ۰ model' t (replicate n v) (λ _, v).

  Lemma inf_array ۰ model'ｰ shift t vs ₗ v vs ᵣ :
    inf_array ۰ model' t (vs ₗ ++ [v]) vs ᵣ ⊣⊢
    inf_array ۰ model' t vs ₗ (v .: vs ᵣ).
  Lemma inf_array ۰ model'ｰ shift ｰ r t vs ₗ v vs ᵣ :
    inf_array ۰ model' t (vs ₗ ++ [v]) vs ᵣ ⊢
    inf_array ۰ model' t vs ₗ (v .: vs ᵣ).
  Lemma inf_array ۰ model'ｰ shift ｰ l t vs ₗ vs ᵣ v vs ᵣ' :
    vs ᵣ ≡ᶠ v .: vs ᵣ' →
    inf_array ۰ model' t vs ₗ vs ᵣ ⊢
    inf_array ۰ model' t (vs ₗ ++ [v]) vs ᵣ'.
  Lemma inf_array ۰ model'ｰ shift ｰ l' t vs ₗ vs ᵣ :
    inf_array ۰ model' t vs ₗ vs ᵣ ⊢
    inf_array ۰ model' t (vs ₗ ++ [vs ᵣ 0]) (vs ᵣ ∘ S).

  Lemma inf_array ٠ create ｰ spec default :
    {{{
      True
    }}}
      inf_array ٠ create default
    {{{
      t
    , RET t ;
      inf_array ۰ inv t ∗
      inf_array ۰ model t (λ _, default)
    }}}.

  #[local] Lemma inf_array ٠ next_capacity ｰ spec n :
    (0 ≤ n)%Z →
    {{{
      True
    }}}
      inf_array ٠ next_capacity #n
    {{{
      m
    , RET #m ;
      ⌜n ≤ m ⌝%Z
    }}}.
  #[local] Lemma inf_array ٠ reserve ｰ spec l γ us n :
    (0 ≤ n)%Z →
    {{{
      l .[default ] ↦□ γ.(metadata ۰ default) ∗
      inv₂ l γ us
    }}}
      inf_array ٠ reserve #l #n
    {{{
      us
    , RET ();
      inv₂ l γ us ∗
      ⌜₊n ≤ length us ⌝
    }}}.

  Lemma inf_array ٠ get ｰ spec t i :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ,
      inf_array ۰ model t vs
    >>>
      inf_array ٠ get t #i
    <<<
      inf_array ۰ model t vs
    | RET vs ₊i ;
      £ 1
    >>>.
  Lemma inf_array ٠ get ｰ spec' t i :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ₗ vs ᵣ ,
      inf_array ۰ model' t vs ₗ vs ᵣ
    >>>
      inf_array ٠ get t #i
    <<<
      inf_array ۰ model' t vs ₗ vs ᵣ
    | RET
        if decide (₊i < length vs ₗ) then
          vs ₗ !!! ₊i
        else
          vs ᵣ (₊i - length vs ₗ);
      £ 1
    >>>.

  Lemma inf_array ٠ update ｰ spec Ψ1 Ψ2 t i fn :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t ∗
      (∀ v , Ψ1 v -∗ WP fn v {{ Ψ2 v }})
    | ∀∀ vs ,
      inf_array ۰ model t vs ∗
      □ Ψ1 (vs ₊i)
    >>>
      inf_array ٠ update t #i fn
    <<<
      ∃∃ v ,
      inf_array ۰ model t (<[₊i := v ]> vs) ∗
      Ψ2 (vs ₊i) v
    | RET vs ₊i ;
      £ 1
    >>>.

  Lemma inf_array ٠ xchg ｰ spec t i v :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ,
      inf_array ۰ model t vs
    >>>
      inf_array ٠ xchg t #i v
    <<<
      inf_array ۰ model t (<[₊i := v ]> vs)
    | RET vs ₊i ;
      £ 1
    >>>.

  Lemma inf_array ٠ xchg_resolve ｰ spec t i v pid v_resolve Φ E :
    (0 ≤ i)%Z →
    inf_array ۰ inv t -∗
    ( |={⊤,E }=>
      ∃ vs ,
      inf_array ۰ model t vs ∗
      ( ∀ e ,
        ⌜PureExec True 1 e ()⌝ -∗
        ⌜to_val e = None ⌝ -∗
        inf_array ۰ model t (<[₊i := v ]> vs) -∗
        WP Resolve e #pid v_resolve @ E {{ _,
          |={E ,⊤}=>
          Φ (vs ₊i)
        }}
      )
    ) -∗
    WP inf_array ٠ xchg_resolve t #i v #pid v_resolve {{ Φ }}.

  Lemma inf_array ٠ set ｰ spec t i v :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ,
      inf_array ۰ model t vs
    >>>
      inf_array ٠ set t #i v
    <<<
      inf_array ۰ model t (<[₊i := v ]> vs)
    | RET ();
      £ 1
    >>>.
  Lemma inf_array ٠ set ｰ spec' t i v :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ₗ vs ᵣ ,
      inf_array ۰ model' t vs ₗ vs ᵣ
    >>>
      inf_array ٠ set t #i v
    <<<
      if decide (₊i < length vs ₗ) then
        inf_array ۰ model' t (<[₊i := v ]> vs ₗ) vs ᵣ
      else
        inf_array ۰ model' t vs ₗ (<[₊i - length vs ₗ := v ]> vs ᵣ)
    | RET ();
      £ 1
    >>>.

  Lemma inf_array ٠ cas ｰ spec t i v1 v2 :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs ,
      inf_array ۰ model t vs
    >>>
      inf_array ٠ cas t #i v1 v2
    <<<
      ∃∃ b ,
      ⌜(if b then (≈) else (≉)) (vs ₊i ) v1 ⌝ ∗
      inf_array ۰ model t (if b then <[₊i := v2 ]> vs else vs)
    | RET #b ;
      £ 1
    >>>.

  Lemma inf_array ٠ cas_resolve ｰ spec t i v1 v2 pid v_resolve Φ E :
    (0 ≤ i)%Z →
    inf_array ۰ inv t -∗
    ( |={⊤,E }=>
      ∃ vs ,
      inf_array ۰ model t vs ∗
      ( ∀ e b ,
        ⌜PureExec True 1 e ()⌝ -∗
        ⌜to_val e = None ⌝ -∗
        ⌜(if b then (≈) else (≉)) (vs ₊i ) v1 ⌝ -∗
        inf_array ۰ model t (if b then <[₊i := v2 ]> vs else vs) -∗
        WP Resolve e #pid v_resolve @ E {{ _,
          |={E ,⊤}=>
          Φ #b
        }}
      )
    ) -∗
    WP inf_array ٠ cas_resolve t #i v1 v2 #pid v_resolve {{ Φ }}.

  Lemma inf_array ٠ faa ｰ spec t i (incr : Z) :
    (0 ≤ i)%Z →
    <<<
      inf_array ۰ inv t
    | ∀∀ vs (n : Z ),
      ⌜vs ₊i = #n ⌝ ∗
      inf_array ۰ model t vs
    >>>
      inf_array ٠ faa t #i #incr
    <<<
      inf_array ۰ model t (<[₊i := #(n + incr )]> vs)
    | RET vs ₊i ;
      £ 1
    >>>.
End inf_array ۰ G.

Require zoo_std.inf_array__opaque.

#[global] Opaque inf_array ۰ inv.
#[global] Opaque inf_array ۰ model.
#[global] Opaque inf_array ۰ model'.