Library examples.vertex_simple

Require Import zoo.prelude.
Require Import zoo.iris.base_logic.lib.fupd.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.base.
Require Export examples.vertex_simple__code.
Require Import examples.vertex_simple__types.
Require Import zoo.options.

Implicit Type v ctx a b c d : val.

Class VertexSimpleG Σ `{zoo۰G : !ZooG Σ} :=
  { #[local] vertex_simple۰G۰pool۰G :: PoolG Σ
  ; #[local] vertex_simple۰G۰vertex۰G :: VertexG Σ
  ; #[local] vertex_simple۰G۰ivar۰G :: Ivar4G Σ
  ; #[local] vertex_simple۰G۰saved_prop۰G :: SavedPropG Σ
  }.

Definition vertex_simple۰Σ :=
  #[pool۰Σ
  ; vertex۰Σ
  ; ivar_4۰Σ
  ; saved_prop۰Σ
  ].
#[global] Instance subGｰvertex_simple۰Σ Σ `{zoo۰G : !ZooG Σ} :
  subG vertex_simple۰Σ Σ →
  VertexSimpleG Σ.

Section vertex_simple۰G.
  Context `{vertex_simple۰G : VertexSimpleG Σ}.

  Implicit Type P_ab P_ac P_b P_c P_d : iProp Σ.

  Lemma vertex_simple٠mainｰspec P_ab P_ac P_b P_c P_d (num_dom : nat) a b c d :
    {{{
      WP a () {{ res, ⌜res = ()%V⌝ ∗ P_ab ∗ P_ac }} ∗
      (P_ab -∗ WP b () {{ res, ⌜res = ()%V⌝ ∗ P_b }}) ∗
      (P_ac -∗ WP c () {{ res, ⌜res = ()%V⌝ ∗ P_c }}) ∗
      (P_b -∗ P_c -∗ WP d () {{ res, ⌜res = ()%V⌝ ∗ P_d }})
    }}}
      vertex_simple٠main #num_dom a b c d
    {{{
      RET ();
      P_d
    }}}.
End vertex_simple۰G.

Require examples.vertex_simple__opaque.