Library examples.vertex_fibonacci

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.fibonacci.
Require Export examples.vertex_fibonacci__code.
Require Import examples.vertex_fibonacci__types.
Require Import zoo.options.

Implicit Type r : location.
Implicit Type 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
      (𝗳𝘂𝗻 "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.

Require examples.vertex_fibonacci__opaque.