Library zoo.program_logic.ghost_state

Require Export iris.bi.lib.fractional.
Require Import iris.base_logic.lib.ghost_map.
Require Import iris.base_logic.lib.invariants.

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.ghost_heap.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.diaframe.
Require Export zoo.language.language.
Require Import zoo.language.notations.
Require Import zoo.options.

Implicit Type cnt ns nt : nat.
Implicit Type pid : prophet_id.
Implicit Type tid : thread_id.
Implicit Type l : location.
Implicit Type v : val.
Implicit Type vs : list val.
Implicit Type hdr : header.
Implicit Type hdrs : gmap location header.
Implicit Type σ : state.
Implicit Type proph : val × val.
Implicit Type prophs : list (val × val).
Implicit Type prophets : gmap prophet_id (list (val × val)).
Implicit Type κ κs : list observation.

Parameter zoo_counter : location.

Class ZooG₀ Σ :=
  { #[local] zoo ۰ G₀ ۰ headers ۰ G :: GhostHeapG Σ location header
  ; #[local] zoo ۰ G₀ ۰ heap ۰ G :: ghost_mapG Σ location val
  ; #[local] zoo ۰ G₀ ۰ prophets ۰ G :: ghost_mapG Σ prophet_id (list (val × val))
  ; #[local] zoo ۰ G₀ ۰ steps ۰ G :: AuthNatMaxG Σ
  ; #[local] zoo ۰ G₀ ۰ locals ۰ G :: GhostListG Σ val
  ; #[local] zoo ۰ G₀ ۰ counter ۰ G :: MonoListG Σ val
  }.

#[local] Definition zoo ۰ Σ₀ :=
  #[ghost_heap ۰ Σ location header
  ; ghost_mapΣ location val
  ; ghost_mapΣ prophet_id (list (val × val))
  ; auth_nat_max ۰ Σ
  ; ghost_list ۰ Σ val
  ; mono_list ۰ Σ val
  ].
#[local] Instance subG ｰ zoo ۰ Σ₀ Σ :
  subG zoo ۰ Σ₀ Σ →
  ZooG₀ Σ.

Class ZooGpre Σ :=
  { #[global] zoo ۰ Gpre ۰ inv ۰ Gpre :: invGpreS Σ
  ; #[local] zoo ۰ Gpre ۰ G₀ :: ZooG₀ Σ
  }.

Definition zoo ۰ Σ :=
  #[invΣ
  ; zoo ۰ Σ₀
  ].
#[global] Instance subG ｰ zoo ۰ Σ Σ :
  subG zoo ۰ Σ Σ →
  ZooGpre Σ.

Class ZooG Σ :=
  { #[global] zoo ۰ G ۰ inv ۰ G :: invGS Σ
  ; #[local] zoo ۰ G ۰ G₀ :: ZooG₀ Σ
  ; zoo ۰ G ۰ headers ۰ name : ghost_heap ۰ name
  ; zoo ۰ G ۰ heap ۰ name : gname
  ; zoo ۰ G ۰ prophets ۰ name : gname
  ; zoo ۰ G ۰ steps ۰ name : gname
  ; zoo ۰ G ۰ locals ۰ name : gname
  ; zoo ۰ G ۰ counter ۰ name : gname
  }.
#[global] Arguments Build_ZooG {_ _ _} _ _ _ _ _ _ : assert.

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

  #[local] Definition headers ۰ auth' γ_headers hdrs :=
    ghost_heap ۰ auth γ_headers hdrs.
  #[local] Definition headers ۰ at' γ_headers l hdr :=
    ghost_heap ۰ at γ_headers l DfracDiscarded hdr.

  #[local] Definition meta_token' γ_headers l E :=
    ghost_heap ۰ meta_token γ_headers l E.
  #[local] Definition meta' `{Countable A} γ_headers l ι (x : A) :=
    ghost_heap ۰ meta γ_headers l ι x.

  #[local] Lemma headers ｰ alloc hdrs :
    ⊢ |==>
      ∃ γ_headers ,
      headers ۰ auth' γ_headers hdrs.
End zoo ۰ G₀.

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

  Definition headers ۰ auth :=
    headers ۰ auth' zoo ۰ G ۰ headers ۰ name.
  Definition headers ۰ at :=
    headers ۰ at' zoo ۰ G ۰ headers ۰ name.

  Definition meta_token :=
    meta_token' zoo ۰ G ۰ headers ۰ name.
  Definition meta `{Countable A} :=
    meta' (A := A) zoo ۰ G ۰ headers ۰ name.
End zoo ۰ G.

Notation "l ↦ₕ hdr" := (
  headers ۰ at l hdr
)(at level 20,
  format "l ↦ₕ hdr"
) : bi_scope.

Notation "l ↪[ ι ] x" := (
  meta l ι x
)(at level 20,
  format "l ↪[ ι ] x"
) : bi_scope.
Notation "l ↪ x" := (
  meta l nroot x
)(at level 20,
  format "l ↪ x"
) : bi_scope.

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

  #[global] Instance headers ۰ at ｰ timeless l hdr :
    Timeless (l ↦ₕ hdr).

  #[global] Instance headers ۰ at ｰ persistent l hdr :
    Persistent (l ↦ₕ hdr).

  Lemma headers ۰ at ｰ agree l hdr1 hdr2 :
    l ↦ₕ hdr1 -∗
    l ↦ₕ hdr2 -∗
    ⌜hdr1 = hdr2 ⌝.
End zoo ۰ G.

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

  #[global] Instance meta_token ｰ timeless l N :
    Timeless (meta_token l N).
  #[global] Instance meta ｰ timeless `{Countable A} l ι (x : A) :
    Timeless (l ↪[ι ] x).

  #[global] Instance meta ｰ persistent `{Countable A} l ι (x : A) :
    Persistent (l ↪[ι ] x).

  Lemma meta_token ｰ difference {l} E1 E2 :
    E1 ⊆ E2 →
    meta_token l E2 ⊣⊢
      meta_token l E1 ∗
      meta_token l (E2 ∖ E1).

  Lemma meta ｰ set `{Countable A} {l E} (x : A) ι :
    ↑ ι ⊆ E →
    meta_token l E ⊢ |==>
    l ↪[ι ] x.
  Lemma meta ｰ agree `{Countable A} l ι (x1 x2 : A) :
    l ↪[ι ] x1 -∗
    l ↪[ι ] x2 -∗
    ⌜x1 = x2 ⌝.

  Lemma headers ｰ lookup hdrs l hdr :
    headers ۰ auth hdrs -∗
    l ↦ₕ hdr -∗
    ⌜hdrs !! l = Some hdr ⌝.

  Lemma headers ｰ insert {hdrs} l hdr :
    hdrs !! l = None →
    headers ۰ auth hdrs ⊢ |==>
      headers ۰ auth (<[l := hdr ]> hdrs) ∗
      l ↦ₕ hdr ∗
      meta_token l ⊤.
End zoo ۰ G.

#[global] Opaque headers ۰ auth'.
#[global] Opaque headers ۰ at'.
#[global] Opaque meta_token'.
#[global] Opaque meta'.

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

  #[local] Definition heap ۰ auth' γ_heap h :=
    ghost_map_auth (V := val) γ_heap 1 h.
  #[local] Definition pointsto' γ_heap l dq v :=
    ghost_map_elem (V := val) γ_heap l dq v.

  #[local] Lemma heap ｰ alloc h :
    ⊢ |==>
      ∃ γ_heap ,
      heap ۰ auth' γ_heap h ∗
      [∗ map ] l ↦ v ∈ h , pointsto' γ_heap l (DfracOwn 1) v.
End zoo ۰ G₀.

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

  Definition heap ۰ auth :=
    heap ۰ auth' zoo ۰ G ۰ heap ۰ name.
  Definition pointsto :=
    pointsto' zoo ۰ G ۰ heap ۰ name.
End zoo ۰ G.

Notation "l ↦ dq v" := (
  pointsto l dq v%V
)(at level 20,
  dq custom dfrac at level 1,
  format "l ↦ dq v"
) : bi_scope.
Notation "l ↦-" := (
  (∃ v , l ↦ v)%I
)(at level 20,
  format "l ↦-"
) : bi_scope.

Notation "l ↦∗ dq vs" :=
  ([∗ list ] i ↦ v ∈ vs, (l +ₗ i ) ↦{dq} v)%I
( at level 20,
  dq custom dfrac at level 1,
  format "l ↦∗ dq vs"
) : bi_scope.
Notation "l ↦∗-" :=
  (∃ vs , l ↦∗ vs)%I
( at level 20,
  format "l ↦∗-"
) : bi_scope.

Notation "l ↦ᵣ dq v" := (
  pointsto (location ۰ add l (Z.of_nat (in_type "ref" 0))) dq v%V
)(at level 20,
  dq custom dfrac at level 1,
  format "l ↦ᵣ dq v"
) : bi_scope.
Notation "l ↦ᵣ-" := (
  (∃ v , l ↦ᵣ v)%I
)(at level 20,
  format "l ↦ᵣ-"
) : bi_scope.

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

  #[global] Instance pointsto ｰ timeless l dq v :
    Timeless (l ↦{dq } v).

  #[global] Instance pointsto ｰ persistent l v :
    Persistent (l ↦□ v).

  #[global] Instance pointsto ｰ fractional l v :
    Fractional (λ q, l ↦{#q } v)%I.
  #[global] Instance pointsto ｰ as_fractional l q v :
    AsFractional (l ↦{#q } v) (λ q, l ↦{#q } v)%I q.

  Lemma pointsto ｰ valid l dq v :
    l ↦{dq } v ⊢
    ⌜✓ dq ⌝.
  Lemma pointsto ｰ combine l dq1 v1 dq2 v2 :
    l ↦{dq1 } v1 -∗
    l ↦{dq2 } v2 -∗
      ⌜v1 = v2 ⌝ ∗
      l ↦{dq1 ⋅ dq2 } v1.
  Lemma pointsto ｰ valid ｰ2 l dq1 v1 dq2 v2 :
    l ↦{dq1 } v1 -∗
    l ↦{dq2 } v2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜v1 = v2 ⌝.
  Lemma pointsto ｰ agree l dq2 v1 dq1 v2 :
    l ↦{dq1 } v1 -∗
    l ↦{dq2 } v2 -∗
    ⌜v1 = v2 ⌝.
  Lemma pointsto ｰ dfrac ｰ ne l1 dq1 v1 l2 dq2 v2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    l1 ↦{dq1 } v1 -∗
    l2 ↦{dq2 } v2 -∗
    ⌜l1 ≠ l2 ⌝.
  Lemma pointsto ｰ ne l1 v1 l2 dq2 v2 :
    l1 ↦ v1 -∗
    l2 ↦{dq2 } v2 -∗
    ⌜l1 ≠ l2 ⌝.
  Lemma pointsto ｰ exclusive l v1 dq2 v2 :
    l ↦ v1 -∗
    l ↦{dq2 } v2 -∗
    False.
  Lemma pointsto ｰ persist l dq v :
    l ↦{dq } v ⊢ |==>
    l ↦□ v.

  #[global] Instance pointsto ｰ combine_sep_gives l dq1 v1 dq2 v2 :
    CombineSepGives (l ↦{dq1 } v1) (l ↦{dq2 } v2) ⌜✓ (dq1 ⋅ dq2 ) ∧ v1 = v2 ⌝
  | 30.
  #[global] Instance pointsto ｰ combine_as l dq1 dq2 v1 v2 :
    CombineSepAs (l ↦{dq1 } v1) (l ↦{dq2 } v2) (l ↦{dq1 ⋅ dq2 } v1)
  | 60.
  #[global] Instance frame ｰ pointsto p l v q1 q2 q :
    FrameFractionalQp q1 q2 q →
    Frame p (l ↦{#q1 } v) (l ↦{#q2 } v) (l ↦{#q } v)
  | 5.

  Lemma heap ｰ lookup h a dq c :
    heap ۰ auth h -∗
    a ↦{dq } c -∗
    ⌜h !! a = Some c ⌝.
  Lemma heap ｰ insert {h1} h2 :
    h2 ##ₘ h1 →
    heap ۰ auth h1 ⊢ |==>
      heap ۰ auth (h2 ∪ h1) ∗
      [∗ map ] l ↦ v ∈ h2 , l ↦ v.
  Lemma heap ｰ update {h a c1} c2 :
    heap ۰ auth h -∗
    a ↦ c1 ==∗
      heap ۰ auth (<[a := c2 ]> h) ∗
      a ↦ c2.
End zoo ۰ G.

#[global] Opaque heap ۰ auth'.
#[global] Opaque pointsto'.

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

  Lemma big_sepL2 ｰ pointsto ｰ agree ls dq1 vs1 dq2 vs2 :
    ([∗ list ] l ; v ∈ ls ; vs1 , l ↦{dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls ; vs2 , l ↦{dq2 } v ) -∗
    ⌜vs1 = vs2 ⌝.
  Lemma big_sepL2 ｰ ref ｰ pointsto ｰ agree ls dq1 vs1 dq2 vs2 :
    ([∗ list ] l ; v ∈ ls ; vs1 , l ↦ᵣ {dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls ; vs2 , l ↦ᵣ {dq2 } v ) -∗
    ⌜vs1 = vs2 ⌝.

  Lemma big_sepL2 ｰ pointsto ｰ prefix ls1 dq1 vs1 ls2 dq2 vs2 :
    ls1 `prefix_of ` ls2 →
    ([∗ list ] l ; v ∈ ls1 ; vs1 , l ↦{dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls2 ; vs2 , l ↦{dq2 } v ) -∗
    ⌜vs1 `prefix_of ` vs2 ⌝.
  Lemma big_sepL2 ｰ ref ｰ pointsto ｰ prefix ls1 dq1 vs1 ls2 dq2 vs2 :
    ls1 `prefix_of ` ls2 →
    ([∗ list ] l ; v ∈ ls1 ; vs1 , l ↦ᵣ {dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls2 ; vs2 , l ↦ᵣ {dq2 } v ) -∗
    ⌜vs1 `prefix_of ` vs2 ⌝.

  Lemma big_sepL2 ｰ pointsto ｰ suffix ls1 dq1 vs1 ls2 dq2 vs2 :
    ls1 `suffix_of ` ls2 →
    ([∗ list ] l ; v ∈ ls1 ; vs1 , l ↦{dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls2 ; vs2 , l ↦{dq2 } v ) -∗
    ⌜vs1 `suffix_of ` vs2 ⌝.
  Lemma big_sepL2 ｰ ref ｰ pointsto ｰ suffix ls1 dq1 vs1 ls2 dq2 vs2 :
    ls1 `suffix_of ` ls2 →
    ([∗ list ] l ; v ∈ ls1 ; vs1 , l ↦ᵣ {dq1 } v ) -∗
    ([∗ list ] l ; v ∈ ls2 ; vs2 , l ↦ᵣ {dq2 } v ) -∗
    ⌜vs1 `suffix_of ` vs2 ⌝.
End zoo ۰ G.

Section resolve_prophecies.
  #[local] Fixpoint resolve_prophecies κs pid :=
    match κs with
    | [] ⇒
        []
    | κ :: κs ⇒
        if decide (pid = κ.1) then
          κ.2 :: resolve_prophecies κs pid
        else
          resolve_prophecies κs pid
    end.

  #[local] Definition resolve_prophets prophets κs :=
    map_Forall (λ pid prophs, prophs = resolve_prophecies κs pid) prophets.

  #[local] Lemma resolve_prophets ｰ insert κs pid prophets :
    resolve_prophets prophets κs →
    pid ∉ dom prophets →
    resolve_prophets (<[pid := resolve_prophecies κs pid ]> prophets) κs.
End resolve_prophecies.

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

  #[local] Definition prophets ۰ auth' γ_prophets κs pids : iProp Σ :=
    ∃ prophets ,
    ⌜resolve_prophets prophets κs ⌝ ∗
    ⌜dom prophets ⊆ pids ⌝ ∗
    ghost_map_auth γ_prophets 1 prophets.
  #[local] Definition prophet ۰ model' γ_prophets pid prophs :=
    ghost_map_elem γ_prophets pid (DfracOwn 1) prophs.

  #[local] Lemma prophets ｰ alloc κs pids :
    ⊢ |==>
      ∃ γ_prophets ,
      prophets ۰ auth' γ_prophets κs pids.
End zoo ۰ G₀.

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

  Definition prophets ۰ auth :=
    prophets ۰ auth' zoo ۰ G ۰ prophets ۰ name.
  Definition prophet ۰ model :=
    prophet ۰ model' zoo ۰ G ۰ prophets ۰ name.

  #[global] Instance prophet ۰ model ｰ timeless pid prophs :
    Timeless (prophet ۰ model pid prophs).

  Lemma prophet ۰ model ｰ exclusive pid prophs1 prophs2 :
    prophet ۰ model pid prophs1 -∗
    prophet ۰ model pid prophs2 -∗
    False.

  Lemma prophets ｰ new {κs pids} pid :
    pid ∉ pids →
    prophets ۰ auth κs pids ⊢ |==>
      ∃ prophs ,
      prophets ۰ auth κs ({[pid ]} ∪ pids) ∗
      prophet ۰ model pid prophs.

  Lemma prophets ｰ resolve pid proph κs pids prophs :
    prophets ۰ auth ((pid , proph ) :: κs) pids -∗
    prophet ۰ model pid prophs ==∗
      ∃ prophs',
      ⌜prophs = proph :: prophs'⌝ ∗
      prophets ۰ auth κs pids ∗
      prophet ۰ model pid prophs'.
End zoo ۰ G.

#[global] Opaque prophets ۰ auth'.
#[global] Opaque prophet ۰ model'.

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

  #[local] Definition steps ۰ auth' γ_steps :=
    auth_nat_max ۰ auth γ_steps (DfracOwn 1).
  #[local] Definition steps ۰ lb' :=
    auth_nat_max ۰ lb.

  #[local] Lemma steps ｰ alloc :
    ⊢ |==>
      ∃ γ_steps ,
      steps ۰ auth' γ_steps 0.
End zoo ۰ G₀.

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

  Definition steps ۰ auth :=
    steps ۰ auth' zoo ۰ G ۰ steps ۰ name.
  Definition steps ۰ lb :=
    auth_nat_max ۰ lb zoo ۰ G ۰ steps ۰ name.
End zoo ۰ G.

Notation "⧖ n" := (
  steps ۰ lb n
)(at level 1,
  format "⧖ n"
) : bi_scope.

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

  #[global] Instance steps ۰ auth ｰ timeless ns :
    Timeless (steps ۰ auth ns).
  #[global] Instance steps ۰ lb ｰ timeless ns :
    Timeless (⧖ ns).

  #[global] Instance steps ۰ lb ｰ persistent ns :
    Persistent (⧖ ns).

  Lemma steps ۰ lb ｰ0 :
    ⊢ |==>
      ⧖ 0.
  Lemma steps ۰ lb ｰ le ns1 ns2 :
    ns2 ≤ ns1 →
    ⧖ ns1 ⊢
    ⧖ ns2.
  Lemma steps ۰ lb ｰ max ns1 ns2 :
    ⧖ ns1 -∗
    ⧖ ns2 -∗
    ⧖ (ns1 `max ` ns2 ).

  Lemma steps ۰ lb ｰ get ns :
    steps ۰ auth ns ⊢
    ⧖ ns.
  Lemma steps ۰ lb ｰ valid ns1 ns2 :
    steps ۰ auth ns1 -∗
    ⧖ ns2 -∗
    ⌜ns2 ≤ ns1 ⌝.

  Lemma steps ｰ update ns :
    steps ۰ auth ns ⊢ |==>
    steps ۰ auth ˖ns.

  #[global] Instance hint ｰ steps ۰ lb ｰ le ns1 ns2 :
    SolveSepSideCondition (ns1 ≤ ns2) →
    HINT
      ⧖ ns2
    ✱ [- ;
      emp
    ] ⊫ [id];
      ⧖ ns1
    ✱ [
      emp
    ]
    | 60.
  #[global] Instance merge ｰ steps ۰ lb ns1 ns2 :
    MergableConsume (⧖ ns1) true (λ p Pin Pout,
      TCAnd (
        TCEq Pin (⧖ ns2)%I
      ) (
        TCEq Pout (⧖ (ns1 `max ` ns2 ))%I
      )
    ).
End zoo ۰ G.

#[global] Opaque steps ۰ auth'.
#[global] Opaque steps ۰ lb'.

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

  #[local] Definition locals ۰ auth' γ_locals vs :=
    ghost_list ۰ auth γ_locals vs.
  #[local] Definition local_pointsto' γ_locals tid dq v :=
    ghost_list ۰ at γ_locals tid dq v.

  #[local] Lemma locals ｰ alloc vs :
    ⊢ |==>
      ∃ γ_locals ,
      locals ۰ auth' γ_locals vs ∗
      [∗ list ] tid ↦ v ∈ vs , local_pointsto' γ_locals tid (DfracOwn 1) v.
End zoo ۰ G₀.

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

  Definition locals ۰ auth :=
    locals ۰ auth' zoo ۰ G ۰ locals ۰ name.
  Definition local_pointsto :=
    local_pointsto' zoo ۰ G ۰ locals ۰ name.
End zoo ۰ G.

Notation "tid ↦ₗ dq v" := (
  local_pointsto tid dq v%V
)(at level 20,
  dq custom dfrac at level 1,
  format "tid ↦ₗ dq v"
) : bi_scope.
Notation "tid ↦ₗ-" := (
  (∃ v , tid ↦ₗ v)%I
)(at level 20,
  format "tid ↦ₗ-"
) : bi_scope.

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

  #[global] Instance local_pointsto ｰ timeless tid dq v :
    Timeless (tid ↦ₗ {dq } v).

  #[global] Instance local_pointsto ｰ persistent tid v :
    Persistent (tid ↦ₗ □ v).

  #[global] Instance local_pointsto ｰ fractional tid v :
    Fractional (λ q, tid ↦ₗ {#q } v)%I.
  #[global] Instance local_pointsto ｰ as_fractional tid q v :
    AsFractional (tid ↦ₗ {#q } v) (λ q, tid ↦ₗ {#q } v)%I q.

  Lemma local_pointsto ｰ valid tid dq v :
    tid ↦ₗ {dq } v ⊢
    ⌜✓ dq ⌝.
  Lemma local_pointsto ｰ combine tid dq1 v1 dq2 v2 :
    tid ↦ₗ {dq1 } v1 -∗
    tid ↦ₗ {dq2 } v2 -∗
      ⌜v1 = v2 ⌝ ∗
      tid ↦ₗ {dq1 ⋅ dq2 } v1.
  Lemma local_pointsto ｰ valid ｰ2 tid dq1 v1 dq2 v2 :
    tid ↦ₗ {dq1 } v1 -∗
    tid ↦ₗ {dq2 } v2 -∗
      ⌜✓ (dq1 ⋅ dq2 )⌝ ∗
      ⌜v1 = v2 ⌝.
  Lemma local_pointsto ｰ agree tid dq2 v1 dq1 v2 :
    tid ↦ₗ {dq1 } v1 -∗
    tid ↦ₗ {dq2 } v2 -∗
    ⌜v1 = v2 ⌝.
  Lemma local_pointsto ｰ dfrac ｰ ne tid1 dq1 v1 tid2 dq2 v2 :
    ¬ ✓ (dq1 ⋅ dq2 ) →
    tid1 ↦ₗ {dq1 } v1 -∗
    tid2 ↦ₗ {dq2 } v2 -∗
    ⌜tid1 ≠ tid2 ⌝.
  Lemma local_pointsto ｰ ne tid1 v1 tid2 dq2 v2 :
    tid1 ↦ₗ v1 -∗
    tid2 ↦ₗ {dq2 } v2 -∗
    ⌜tid1 ≠ tid2 ⌝.
  Lemma local_pointsto ｰ exclusive tid v1 dq2 v2 :
    tid ↦ₗ v1 -∗
    tid ↦ₗ {dq2 } v2 -∗
    False.
  Lemma local_pointsto ｰ persist tid dq v :
    tid ↦ₗ {dq } v ⊢ |==>
    tid ↦ₗ □ v.

  Lemma locals ｰ lookup vs tid dq v :
    locals ۰ auth vs -∗
    tid ↦ₗ {dq } v -∗
    ⌜vs !! tid = Some v ⌝.

  Lemma locals ｰ update ｰ push {vs} v :
    locals ۰ auth vs ⊢ |==>
      locals ۰ auth (vs ++ [v]) ∗
      length vs ↦ₗ v.
  Lemma locals ｰ update ｰ pointsto {vs tid v} v' :
    locals ۰ auth vs -∗
    tid ↦ₗ v ==∗
      locals ۰ auth (<[tid := v']> vs) ∗
      tid ↦ₗ v'.
End zoo ۰ G.

#[global] Opaque locals ۰ auth'.
#[global] Opaque local_pointsto'.

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

  #[local] Definition zoo_counter ۰ auth' γ_counter vs :=
    mono_list ۰ auth γ_counter (DfracOwn 1) vs.
  #[local] Definition zoo_counter ۰ at' γ_counter id v :=
    mono_list ۰ at γ_counter id v.

  #[local] Lemma zoo_counter ｰ alloc :
    ⊢ |==>
      ∃ γ_counter ,
      zoo_counter ۰ auth' γ_counter (replicate 0 inhabitant).
End zoo ۰ G₀.

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

  Definition zoo_counter ۰ auth :=
    zoo_counter ۰ auth' zoo ۰ G ۰ counter ۰ name.
  Definition zoo_counter ۰ at :=
    zoo_counter ۰ at' zoo ۰ G ۰ counter ۰ name.

  #[global] Instance zoo_counter ۰ auth ｰ timeless vs :
    Timeless (zoo_counter ۰ auth vs).
  #[global] Instance zoo_counter ۰ at ｰ timeless id v :
    Timeless (zoo_counter ۰ at id v).

  #[global] Instance zoo_counter ۰ at ｰ persistent id v :
    Persistent (zoo_counter ۰ at id v).

  Lemma zoo_counter ۰ at ｰ get {vs} id v :
    vs !! id = Some v →
    zoo_counter ۰ auth vs ⊢
    zoo_counter ۰ at id v.
  Lemma zoo_counter ۰ at ｰ valid vs id v :
    zoo_counter ۰ auth vs -∗
    zoo_counter ۰ at id v -∗
    ⌜vs !! id = Some v ⌝.
  Lemma zoo_counter ۰ at ｰ agree id v1 v2 :
    zoo_counter ۰ at id v1 -∗
    zoo_counter ۰ at id v2 -∗
    ⌜v1 = v2 ⌝.

  Lemma zoo_counter ｰ update {vs} v :
    zoo_counter ۰ auth vs ⊢ |==>
    zoo_counter ۰ auth (vs ++ [v]).
End zoo ۰ G.

#[global] Opaque zoo_counter ۰ auth'.
#[global] Opaque zoo_counter ۰ at'.

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

  Definition zoo_counter ۰ name :=
    zoo ۰ G ۰ counter ۰ name.
  Definition zoo_counter ۰ inv ۰ inner : iProp Σ :=
    ∃ cnt vs ,
    zoo_counter ↦ᵣ #cnt ∗
    zoo_counter ۰ auth vs ∗
    ⌜length vs = cnt ⌝.
  Definition zoo_counter ۰ inv :=
    inv nroot zoo_counter ۰ inv ۰ inner.
End zoo ۰ G.

Lemma zoo ｰ init `{zoo ۰ Gpre : !ZooGpre Σ} `{inv ۰ G : !invGS Σ} hdrs h pids vs κs :
  h !! zoo_counter = Some 0%V →
  ⊢ |={⊤}=>
    ∃ zoo ۰ G : ZooG Σ ,
    ⌜zoo ۰ G.(zoo ۰ G ۰ inv ۰ G) = inv ۰ G ⌝ ∗
    headers ۰ auth hdrs ∗
    heap ۰ auth h ∗
    prophets ۰ auth κs pids ∗
    steps ۰ auth 0 ∗
    locals ۰ auth vs ∗
    zoo_counter ۰ inv ∗
    ([∗ map ] l ↦ v ∈ delete zoo_counter h , l ↦ v ) ∗
    ([∗ list ] tid ↦ v ∈ vs , tid ↦ₗ v ).

#[global] Opaque headers ۰ auth.
#[global] Opaque headers ۰ at.
#[global] Opaque meta_token.
#[global] Opaque meta.
#[global] Opaque heap ۰ auth.
#[global] Opaque pointsto.
#[global] Opaque prophets ۰ auth.
#[global] Opaque prophet ۰ model.
#[global] Opaque steps ۰ auth.
#[global] Opaque steps ۰ lb.
#[global] Opaque locals ۰ auth.
#[global] Opaque local_pointsto.
#[global] Opaque zoo_counter ۰ auth.
#[global] Opaque zoo_counter ۰ at.

Variant ownership :=
  | Own
  | Discard.

Coercion ownership ۰ to_dfrac own :=
  match own with
  | Own ⇒
      DfracOwn 1
  | Discard ⇒
      DfracDiscarded
  end.