Library examples.vertex_simple

From zoo Require Import
  prelude.
From zoo.iris.base_logic Require Import
  lib.fupd
  lib.saved_prop.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  ivar_4.
From zoo_parabs Require Import
  pool
  vertex.
From examples Require Export
  vertex_simple__code.
From zoo Require Import
  options.

Implicit Types 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 Types 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.

From examples Require
  vertex_simple__opaque.