Library examples.pool_counter

Require Import iris.algebra.numbers.

Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.cinv.
Require Import zoo.iris.base_logic.lib.auth_frac.
Require Import zoo.base.
Require Export examples.pool_counter__code.
Require Import examples.pool_counter__types.
Require Import zoo.options.

Implicit Type n cnt contrib : nat.
Implicit Type r : location.
Implicit Type γ η : gname.

Class PoolCounterG Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] pool_counter ۰ G ۰ pool ۰ G :: PoolG Σ
  ; #[local] pool_counter ۰ G ۰ cinv ۰ G :: cinvG Σ
  ; #[local] pool_counter ۰ G ۰ tokens ۰ G :: AuthFracG Σ natUR
  }.

Definition pool_counter ۰ Σ :=
  #[pool ۰ Σ
  ; cinvΣ
  ; auth_frac ۰ Σ natUR
  ].
#[global] Instance subG ｰ pool_counter ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG pool_counter ۰ Σ Σ →
  PoolCounterG Σ.

Section pool_counter ۰ G.
  Context `{pool_counter ۰ G : PoolCounterG Σ}.

  #[local] Definition tokens ۰ auth γ cnt :=
    auth_frac ۰ auth γ cnt.
  #[local] Definition tokens ۰ frag γ n contrib :=
    auth_frac ۰ frag γ (1 / Qp ۰ of_nat n) contrib.

  #[local] Definition inv ۰ inner r γ : iProp Σ :=
    ∃ cnt : nat ,
    r ↦ᵣ #cnt ∗
    tokens ۰ auth γ cnt.
  #[local] Instance : CustomIpat "inv۰inner" :=
    " ( %cnt & >Hr & >Htokens_auth ) ".
  #[local] Definition inv r γ η :=
    cinv nroot η (inv ۰ inner r γ).

  #[local] Lemma tokens ｰ alloc n :
    ⊢ |==>
      ∃ γ ,
      tokens ۰ auth γ 0 ∗
      [∗ list ] _ ∈ seq 0 n , tokens ۰ frag γ n 0.
  #[local] Lemma tokens ｰ incr γ cnt n contrib :
    tokens ۰ auth γ cnt -∗
    tokens ۰ frag γ n contrib ==∗
      tokens ۰ auth γ (cnt + 1) ∗
      tokens ۰ frag γ n (contrib + 1).
  #[local] Lemma tokens ｰ agree γ cnt n :
    0 < n →
    tokens ۰ auth γ cnt -∗
    ([∗ list ] _ ∈ seq 0 n , tokens ۰ frag γ n 1) -∗
    ⌜cnt = n ⌝.

  Lemma pool_counter ٠ main ｰ spec (num_dom n : nat) :
    0 < n →
    {{{
      True
    }}}
      pool_counter ٠ main #num_dom #n
    {{{
      RET #n ;
      True
    }}}.
End pool_counter ۰ G.

Require examples.pool_counter__opaque.