Library examples.pool_counter

From iris.algebra Require Import
  numbers.

From zoo Require Import
  prelude.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Import
  lib.cinv.
From zoo.iris.base_logic Require Import
  lib.auth_frac.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  for_.
From zoo_parabs Require Import
  pool.
From examples Require Export
  pool_counter__code.
From zoo Require Import
  options.

Implicit Types n cnt contrib : nat.
Implicit Types r : location.
Implicit Types γ η : 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.

From examples Require
  pool_counter__opaque.