Library zoo.program_logic.counter

From iris.base_logic Require Import
  lib.invariants.

From zoo Require Import
  prelude.
From zoo.iris.bi Require Import
  big_op.
From zoo.language Require Import
  notations.
From zoo.program_logic Require Export
  wp.
From zoo.diaframe Require Import
  diaframe.
From zoo Require Import
  options.

Definition zoo_counter٠incr : val :=
  fun: ≠ ⇒
    FAA (#zoo_counter).[contents] 1.

Section zoo_G.
  Context `{zoo_G : !ZooG Σ}.

  Lemma zoo_counter٠incr𑁒spec ids v :
    {{{
      [∗ list] id ∈ ids,
        ∃ v,
        zoo_counter_at id v
    }}}
      zoo_counter٠incr ()
    {{{
      id
    , RET #id;
      zoo_counter_at id v ∗
      ⌜Forall (.≠ id) ids⌝
    }}}.
End zoo_G.