Library zoo_std.domain

Require Import iris.base_logic.lib.ghost_map.

Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.common.fin_maps.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo.program_logic.counter.
Require Import zoo_std.dynarray_1.
Require Import zoo_std.ivar_2.
Require Import zoo_std.option.
Require Export zoo_std.domain__code.
Require Import zoo_std.domain__types.
Require Import zoo.options.

Implicit Type id : nat.
Implicit Type l : location.
Implicit Type t fn key : val.
Implicit Type vs : list (option val).
Implicit Type ws : gmap nat (option val).
Implicit Type ids : gmap val nat.

#[local] Notation "'id'" := (
  in_type "key" 0
)(in custom zoo_proj
).
#[local] Notation "'init'" := (
  in_type "key" 1
)(in custom zoo_proj
).

Definition domain٠spawn : val :=
  𝗳𝘂𝗻 "fn" →
    𝗹𝗲𝘁 "t" = ivar_2٠create () 𝗶𝗻
    𝗳𝗼𝗿𝗸 (
      𝗹𝗲𝘁 "local" = dynarray_1٠create () 𝗶𝗻
      𝘀𝗲𝘁𝗹𝗼𝗰𝗮𝗹 "local" ⍮
      ivar_2٠set "t" ("fn" ())
    ) ⍮
    "t".

Definition domain٠join : val :=
  ivar_2٠get.

Definition domain٠local_new : val :=
  𝗳𝘂𝗻 "fn" →
    𝗹𝗲𝘁 "id" = zoo_counter٠incr () 𝗶𝗻
    ("id", "fn").

Definition domain٠key۰id : val :=
  𝗳𝘂𝗻 "key" →
    "key".<id>.
Definition domain٠key_init : val :=
  𝗳𝘂𝗻 "key" →
    "key".<init> ().

Definition domain٠local_get : val :=
  𝗳𝘂𝗻 "key" →
    𝗹𝗲𝘁 "local" = 𝗹𝗼𝗰𝗮𝗹 𝗶𝗻
    𝗹𝗲𝘁 "id" = domain٠key۰id "key" 𝗶𝗻
    dynarray_1٠grow "local" ("id" + 1) §None ⍮
    𝗺𝗮𝘁𝗰𝗵 dynarray_1٠get "local" "id" 𝘄𝗶𝘁𝗵
    | None →
        𝗹𝗲𝘁 "v" = domain٠key_init "key" 𝗶𝗻
        dynarray_1٠set "local" "id" ‘Some( "v" ) ⍮
        "v"
    | Some "v" →
        "v"
    𝗲𝗻𝗱.

Definition domain٠local_set : val :=
  𝗳𝘂𝗻 "key" "v" →
    𝗹𝗲𝘁 "local" = 𝗹𝗼𝗰𝗮𝗹 𝗶𝗻
    𝗹𝗲𝘁 "id" = domain٠key۰id "key" 𝗶𝗻
    dynarray_1٠grow "local" ("id" + 1) §None ⍮
    dynarray_1٠set "local" "id" ‘Some( "v" ).

Class DomainG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] domain۰G۰ivar۰G :: Ivar2G Σ
  ; #[local] domain۰G۰locals۰G :: ghost_mapG Σ nat (option val)
  }.

Definition domain۰Σ :=
  #[ivar_2۰Σ
  ; ghost_mapΣ nat (option val)
  ].
#[global] Instance subGｰdomain۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG domain۰Σ Σ →
  DomainG Σ.

Section consistent.
  #[local] Definition consistent vs ws :=
    map۰oflatten (map_seq 0 vs) = map۰oflatten ws.

  #[local] Lemma consistentｰappｰNone vs ws n :
    consistent vs ws →
    consistent (vs ++ replicate n None) ws.
  #[local] Lemma consistentｰlookupｰNone {vs ws} id o :
    consistent vs ws →
    ws !! id = None →
    vs !! id = Some o →
    o = None.
  #[local] Lemma consistentｰlookupｰSomeｰNone {vs ws} id :
    id < length vs →
    consistent vs ws →
    ws !! id = Some None →
    vs !! id = Some None.
  #[local] Lemma consistentｰlookupｰSomeｰSome {vs ws} id v :
    consistent vs ws →
    ws !! id = Some (Some v) →
    vs !! id = Some (Some v).
  #[local] Lemma consistentｰinsert {vs ws} id :
    ws !! id = None →
    consistent vs ws →
    consistent vs (<[id := None]> ws).
  #[local] Lemma consistentｰupdate {vs ws} id w :
    id < length vs →
    consistent vs ws →
    consistent (<[id := Some w]> vs) (<[id := Some w]> ws).
End consistent.

Opaque consistent.

Section domain۰G.
  Context `{domain۰G : DomainG Σ}.

  Implicit Type Ψ : val → iProp Σ.

  #[local] Definition local۰auth γ :=
    ghost_map_auth γ 1.
  #[local] Definition local۰at :=
    ghost_map_elem.

  Definition domain۰model t Ψ : iProp Σ :=
    ivar_2۰inv t Ψ (λ _, True)%I ∗
    ivar_2۰consumer t Ψ.
  #[local] Instance : CustomIpat "model" :=
    " ( #Hivar_inv & Hivar_consumer ) ".

  #[local] Definition key۰id key id : iProp Σ :=
    ∃ fn,
    ⌜key = (#id, fn)%V⌝ ∗
    zoo_counter۰at id fn.
  #[local] Instance : CustomIpat "key۰id" :=
    " ( %fn{} & %Heq{} & #Hcounter_at{} ) ".

  Definition domain۰key key Ψ : iProp Σ :=
    ∃ id fn,
    ⌜key = (#id, fn)%V⌝ ∗
    zoo_counter۰at id fn ∗
    □ WP fn () {{ Ψ }}.
  #[local] Instance : CustomIpat "key" :=
    " ( %id & %fn{} & -> & Hcounter_at & #Hfn{} ) ".
  Definition domain۰key' key : iProp Σ :=
    ∃ Ψ,
    domain۰key key Ψ.

  Definition domain۰local tid keys : iProp Σ :=
    ∃ l γ vs ws ids,
    tid ↦ₗ□ #l ∗
    l ↪[nroot.@"user"] γ ∗
    dynarray_1۰model #l (option۰to_val <$> vs) ∗
    local۰auth γ ws ∗
    ⌜dom ids = keys⌝ ∗
    ⌜map_img ids = dom ws⌝ ∗
    ([∗ map] key ↦ id ∈ ids, key۰id key id) ∗
    ⌜consistent vs ws⌝.
  #[local] Instance : CustomIpat "local" :=
    " ( %l & %γ & %vs & %ws & %ids & #Hlocal & #Hl_meta & Hl & Hlocal_auth & %Hids_dom & %Hids_img & Hids & %Hconsistent ) ".

  Definition domain۰local_init tid key : iProp Σ :=
    ∃ l γ id,
    tid ↦ₗ□ #l ∗
    l ↪[nroot.@"user"] γ ∗
    key۰id key id ∗
    local۰at γ id (DfracOwn 1) None.
  #[local] Instance : CustomIpat "local_init" :=
    " ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".

  Definition domain۰local_pointsto tid key dq v : iProp Σ :=
    ∃ l γ id,
    tid ↦ₗ□ #l ∗
    l ↪[nroot.@"user"] γ ∗
    key۰id key id ∗
    local۰at γ id dq (Some v).
  #[local] Instance : CustomIpat "local_pointsto" :=
    " ( %l{}{_{suff}} & %γ{}{_{suff}} & %id{} & #Hlocal{}{_{suff}} & #Hl{}_meta{_{suff}} & #Hid{} & Hlocal_at{} ) ".
  Definition domain۰local_pointstopred tid key Ψ : iProp Σ :=
      domain۰local_init tid key ∗
      domain۰key key Ψ
    ∨ ∃ v,
      domain۰local_pointsto tid key (DfracOwn 1) v ∗
      Ψ v.
  #[local] Instance : CustomIpat "local_pointstopred" :=
    " [ ( Hinit & Hkey ) | ( % & Hlocal_pointsto & HΨ ) ] ".

  #[global] Instance domain۰localｰtimeless tid keys :
    Timeless (domain۰local tid keys).
  #[global] Instance domain۰local_initｰtimeless tid key :
    Timeless (domain۰local_init tid key).
  #[global] Instance domain۰local_pointstoｰtimeless tid key dq v :
    Timeless (domain۰local_pointsto tid key dq v).

  #[local] Instance key۰idｰpersistent key id :
    Persistent (key۰id key id).
  #[global] Instance domain۰keyｰpersistent key Ψ :
    Persistent (domain۰key key Ψ).
  #[global] Instance domain۰local_pointstoｰpersistent tid key v :
    Persistent (domain۰local_pointsto tid key DfracDiscarded v).

  #[local] Lemma localｰalloc :
    ⊢ |==>
      ∃ γ,
      local۰auth γ ∅.
  #[local] Lemma local۰atｰvalid γ ws id dq v :
    local۰auth γ ws -∗
    local۰at γ id dq v -∗
    ⌜ws !! id = Some v⌝.
  #[local] Lemma localｰinsert {γ ws} id :
    ws !! id = None →
    local۰auth γ ws ⊢ |==>
      local۰auth γ (<[id := None]> ws) ∗
      local۰at γ id (DfracOwn 1) None.
  #[local] Lemma localｰupdate {γ ws id w} w' :
    local۰auth γ ws -∗
    local۰at γ id (DfracOwn 1) w ==∗
      local۰auth γ (<[id := w']> ws) ∗
      local۰at γ id (DfracOwn 1) w'.

  #[local] Lemma key۰idｰagree key id1 id2 :
    key۰id key id1 -∗
    key۰id key id2 -∗
    ⌜id1 = id2⌝.
  #[local] Lemma key۰idｰinj key1 id1 key2 id2 :
    key1 ≠ key2 →
    key۰id key1 id1 -∗
    key۰id key2 id2 -∗
    ⌜id1 ≠ id2⌝.

  #[local] Lemma domain۰keyｰtoｰid key Ψ :
    domain۰key key Ψ ⊢
      ∃ id,
      key۰id key id.

  #[local] Lemma domain٠key۰idｰspec key id :
    {{{
      key۰id key id
    }}}
      domain٠key۰id key
    {{{
      RET #id;
      True
    }}}.

  #[local] Lemma domain٠key_initｰspec key Ψ :
    {{{
      domain۰key key Ψ
    }}}
      domain٠key_init key
    {{{
      v
    , RET v;
      Ψ v
    }}}.

  Opaque key۰id.

  Lemma domain۰localｰgetｰkey {tid keys} key Ψ :
    key ∉ keys →
    domain۰local tid keys -∗
    domain۰key key Ψ ==∗
      domain۰local tid (keys ∪ {[key]}) ∗
      domain۰local_init tid key.
  #[global] Instance domain۰local_pointstoｰfractional tid key v :
    Fractional (λ q, domain۰local_pointsto tid key (DfracOwn q) v).
  #[global] Instance domain۰local_pointstoｰas_fractional tid key q v :
    AsFractional (domain۰local_pointsto tid key (DfracOwn q) v) (λ q, domain۰local_pointsto tid key (DfracOwn q) v)%I q.

  Lemma domain۰local_pointstoｰvalid tid key dq v :
    domain۰local_pointsto tid key dq v ⊢
    ⌜✓ dq⌝.
  Lemma domain۰local_pointstoｰcombine tid key dq1 v1 dq2 v2 :
    domain۰local_pointsto tid key dq1 v1 -∗
    domain۰local_pointsto tid key dq2 v2 -∗
      ⌜v1 = v2⌝ ∗
      domain۰local_pointsto tid key (dq1 ⋅ dq2) v1.
  Lemma domain۰local_pointstoｰvalidｰ2 tid key dq1 v1 dq2 v2 :
    domain۰local_pointsto tid key dq1 v1 -∗
    domain۰local_pointsto tid key dq2 v2 -∗
      ⌜✓ (dq1 ⋅ dq2)⌝ ∗
      ⌜v1 = v2⌝.
  Lemma domain۰local_pointstoｰagree tid key dq1 v1 dq2 v2 :
    domain۰local_pointsto tid key dq1 v1 -∗
    domain۰local_pointsto tid key dq2 v2 -∗
    ⌜v1 = v2⌝.
  Lemma domain۰local_pointstoｰdfracｰne tid1 key1 dq1 v1 tid2 key2 dq2 v2 :
    ¬ ✓ (dq1 ⋅ dq2) →
    domain۰local_pointsto tid1 key1 dq1 v1 -∗
    domain۰local_pointsto tid2 key2 dq2 v2 -∗
    ⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
  Lemma domain۰local_pointstoｰne tid1 key1 v1 tid2 key2 dq2 v2 :
    domain۰local_pointsto tid1 key1 (DfracOwn 1) v1 -∗
    domain۰local_pointsto tid2 key2 dq2 v2 -∗
    ⌜tid1 ≠ tid2 ∨ key1 ≠ key2⌝.
  Lemma domain۰local_pointstoｰexclusive tid key v1 dq2 v2 :
    domain۰local_pointsto tid key (DfracOwn 1) v1 -∗
    domain۰local_pointsto tid key dq2 v2 -∗
    False.
  Lemma domain۰local_pointstoｰpersist tid key dq v :
    domain۰local_pointsto tid key dq v ⊢ |==>
    domain۰local_pointsto tid key DfracDiscarded v.

  Lemma domain٠spawnｰspec Ψ fn :
    {{{
      ∀ tid,
      domain۰local tid ∅ -∗
      WP fn () ∶ tid {{ Ψ }}
    }}}
      domain٠spawn fn
    {{{
      t
    , RET t;
      domain۰model t Ψ
    }}}.

  Lemma domain٠joinｰspec t Ψ :
    {{{
      domain۰model t Ψ
    }}}
      domain٠join t
    {{{
      v
    , RET v;
      Ψ v
    }}}.

  Lemma domain٠local_newｰspec {fn} Ψ keys :
    {{{
      □ WP fn () {{ Ψ }} ∗
      [∗ list] key ∈ keys, domain۰key' key
    }}}
      domain٠local_new fn
    {{{
      key
    , RET key;
      domain۰key key Ψ ∗
      ⌜Forall (.≠ key) keys⌝
    }}}.

  Lemma domain٠local_getｰspecｰinit keys key Ψ tid :
    {{{
      domain۰local tid keys ∗
      domain۰key key Ψ ∗
      domain۰local_init tid key
    }}}
      domain٠local_get key ∶ tid
    {{{
      v
    , RET v;
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) v ∗
      Ψ v
    }}}.
  Lemma domain٠local_getｰspecｰpointsto keys key dq v tid :
    {{{
      domain۰local tid keys ∗
      domain۰local_pointsto tid key dq v
    }}}
      domain٠local_get key ∶ tid
    {{{
      RET v;
      domain۰local tid keys ∗
      domain۰local_pointsto tid key dq v
    }}}.
  Lemma domain٠local_getｰspecｰpointstopred keys key Ψ tid :
    {{{
      domain۰local tid keys ∗
      domain۰local_pointstopred tid key Ψ
    }}}
      domain٠local_get key ∶ tid
    {{{
      v
    , RET v;
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) v ∗
      Ψ v
    }}}.

  Lemma domain٠local_setｰspecｰinit keys key Ψ v tid :
    {{{
      domain۰local tid keys ∗
      domain۰key key Ψ ∗
      domain۰local_init tid key
    }}}
      domain٠local_set key v ∶ tid
    {{{
      RET ();
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) v
    }}}.
  Lemma domain٠local_setｰspecｰpointsto keys key w v tid :
    {{{
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) w
    }}}
      domain٠local_set key v ∶ tid
    {{{
      RET ();
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) v
    }}}.
  Lemma domain٠local_setｰspecｰpointstopred keys key Ψ v tid :
    {{{
      domain۰local tid keys ∗
      domain۰local_pointstopred tid key Ψ
    }}}
      domain٠local_set key v ∶ tid
    {{{
      RET ();
      domain۰local tid keys ∗
      domain۰local_pointsto tid key (DfracOwn 1) v
    }}}.
End domain۰G.

Axiom domain٠yieldｰspec : ∀ `{zoo۰G : !ZooG Σ} Φ,
  ▷ Φ ()%V ⊢
  WP domain٠yield () {{ Φ }}.

Axiom domain٠self_indexｰspec : ∀ `{zoo۰G : !ZooG Σ} Φ,
  (∀ (i : nat), ▷ Φ #i) ⊢
  WP domain٠self_index () {{ Φ }}.

Axiom domain٠recommended_domain_countｰspec : ∀ `{zoo۰G : !ZooG Σ} Φ,
  (∀ (i : nat), ▷ Φ #i) ⊢
  WP domain٠recommended_domain_count () {{ Φ }}.

Section zoo۰G.
  Context `{zoo۰G : !ZooG Σ}.

  #[global] Instance domain٠yieldｰdiaspec :
    DIASPEC
    {{
      True
    }}
      domain٠yield ()%V
    {{
      RET ();
      True
    }}.

  #[global] Instance domain٠self_indexｰdiaspec :
    DIASPEC
    {{
      True
    }}
      domain٠self_index ()%V
    {{ (i : nat),
      RET #i;
      True
    }}.

  #[global] Instance domain٠recommended_domain_countｰdiaspec :
    DIASPEC
    {{
      True
    }}
      domain٠recommended_domain_count ()%V
    {{ (i : nat),
      RET #i;
      True
    }}.
End zoo۰G.

Require zoo_std.domain__opaque.
#[global] Opaque domain٠spawn.
#[global] Opaque domain٠join.
#[global] Opaque domain٠local_new.
#[global] Opaque domain٠local_get.
#[global] Opaque domain٠local_set.

#[global] Opaque domain۰model.
#[global] Opaque domain۰key.
#[global] Opaque domain۰local.
#[global] Opaque domain۰local_init.
#[global] Opaque domain۰local_pointsto.