Library examples.vertex_fibonacci

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
  fibonacci
  vertex_fibonacci__code.
From zoo Require Import
  options.

Implicit Types r : location.
Implicit Types v ctx vtx : val.

Class VertexFibonacciG Σ `{zoo_G : !ZooG Σ} :=
  { #[local] vertex_fibonacci_G_pool_G :: PoolG Σ
  ; #[local] vertex_fibonacci_G_vertex_G :: VertexG Σ
  ; #[local] vertex_fibonacci_G_ivar_G :: Ivar4G Σ
  ; #[local] vertex_fibonacci_G_saved_prop_G :: SavedPropG Σ
  }.

Definition vertex_fibonacci_Σ :=
  #[pool_Σ
  ; vertex_Σ
  ; ivar_4_Σ
  ; saved_prop_Σ
  ].
#[global] Instance subG_vertex_fibonacci_Σ Σ `{zoo_G : !ZooG Σ} :
  subG vertex_fibonacci_Σ Σ →
  VertexFibonacciG Σ.

Section vertex_fibonacci_G.
  Context `{vertex_fibonacci_G : VertexFibonacciG Σ}.

  #[local] Lemma vertex_fibonacci٠main₀𑁒spec vtx iter r n :
    vertex_inv vtx (r ↦ᵣ #(fibonacci n)) True -∗
    r ↦ᵣ 0 -∗
    vertex_wp
      vtx
      (r ↦ᵣ #(fibonacci n))
      True
      (fun: "ctx" ⇒ vertex_fibonacci٠main₀ "ctx" vtx #r #n)
      iter.

  Lemma vertex_fibonacci٠main𑁒spec (num_dom n : nat) :
    {{{
      True
    }}}
      vertex_fibonacci٠main #num_dom #n
    {{{
      RET #(fibonacci n);
      True
    }}}.
End vertex_fibonacci_G.

From examples Require
  vertex_fibonacci__opaque.