Library zoo_parabs.algo

From zoo Require Import
  prelude.
From zoo.common Require Import
  countable.
From zoo.iris.bi Require Import
  big_op.
From zoo.iris.base_logic Require Import
  lib.ghost_var.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Import
  for_
  mvar
  option.
From zoo_parabs Require Export
  base
  algo__code.
From zoo_parabs Require Import
  future
  pool.
From zoo Require Import
  options.

Implicit Types b : bool.
Implicit Types v pool ctx task pred found body op zero acc : val.
Implicit Types o : option val.

Class AlgoG Σ `{pool_G : PoolG Σ} :=
  { #[local] algo_G_future_G :: FutureG Σ
  ; #[local] algo_G_mvar_G :: MvarG Σ
  ; #[local] algo_G_find_G :: GhostVarG Σ unitO
  }.

Definition algo_Σ :=
  #[future_Σ
  ; mvar_Σ
  ; ghost_var_Σ unitO
  ].
#[global] Instance subG_algo_Σ Σ `{pool_G : PoolG Σ} :
  subG algo_Σ Σ →
  AlgoG Σ.

Section algo_G.
  Context `{algo_G : AlgoG Σ}.

  #[local] Lemma algo٠adjust_chunk𑁒spec pool sz ctx scope (beg end_ : Z) chunk :
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk
    }}}
      algo٠adjust_chunk ctx #beg #end_ chunk
    {{{
      (chunk : Z)
    , RET #chunk;
      pool_context pool ctx scope
    }}}.

  #[local] Lemma algo٠for_₀𑁒spec Ψ Χ pool ctx scope beg0 beg end_ end0 (chunk : Z) task :
    (beg0 ≤ beg ≤ end_ ≤ end0)%Z →
    {{{
      pool_context pool ctx scope ∗
      Χ beg ₊(end_ - beg) ∗
      □ (
        ∀ i (n1 n2 : nat),
        ⌜beg0 ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end0⌝%Z -∗
        Χ i (n1 + n2) -∗
          Χ i n1 ∗
          Χ (i + n1)%Z n2
      ) ∗
      □ (
        ∀ ctx scope i (n : nat),
        pool_context pool ctx scope -∗
        ⌜beg0 ≤ i⌝%Z -∗
        ⌜i + n ≤ end0⌝%Z -∗
        Χ i n -∗
        WP task ctx #i #n {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          [∗ list] j ∈ seqZ i n,
            Ψ j
        }}
      )
    }}}
      algo٠for_₀ ctx #beg #end_ #chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_𑁒spec (Ψ : Z → iProp Σ) (Χ : Z → nat → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      Χ beg ₊(end_ - beg) ∗
      □ (
        ∀ i (n1 n2 : nat),
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i (n1 + n2) -∗
          Χ i n1 ∗
          Χ (i + n1)%Z n2
      ) ∗
      □ (
        ∀ ctx scope i (n : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n -∗
        WP task ctx #i #n {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          [∗ list] j ∈ seqZ i n,
            Ψ j
        }}
      )
    }}}
      algo٠for_ ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_𑁒spec_nat (Ψ : nat → iProp Σ) (Χ : Z → nat → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      Χ ₊beg ₊(end_ - beg) ∗
      □ (
        ∀ i n1 n2 : nat,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i (n1 + n2) -∗
          Χ i n1 ∗
          Χ (i + n1) n2
      ) ∗
      □ (
        ∀ ctx scope (i n : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n -∗
        WP task ctx #i #n {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          [∗ list] j ∈ seq i n,
            Ψ j
        }}
      )
    }}}
      algo٠for_ ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_𑁒spec' (Ψ : Z → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope i (n : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        WP task ctx #i #n {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          [∗ list] j ∈ seqZ i n,
            Ψ j
        }}
      )
    }}}
      algo٠for_ ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_𑁒spec_nat' (Ψ : nat → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope (i n : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        WP task ctx #i #n {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          [∗ list] j ∈ seq i n,
            Ψ j
        }}
      )
    }}}
      algo٠for_ ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
        Ψ i
    }}}.

  Lemma algo٠for_each𑁒spec' (Ψ : Z → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP task ctx #i {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          Ψ i
        }}
    }}}
      algo٠for_each ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_each𑁒spec_nat' (Ψ : nat → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      [∗ list] (i : nat) ∈ seq ₊beg ₊(end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP task ctx #i {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          Ψ i
        }}
    }}}
      algo٠for_each ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_each𑁒spec (Ψ : Z → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope i,
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP task ctx #i {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          Ψ i
        }}
      )
    }}}
      algo٠for_each ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seqZ beg (end_ - beg),
        Ψ i
    }}}.
  Lemma algo٠for_each𑁒spec_nat (Ψ : nat → iProp Σ) pool sz ctx scope beg end_ chunk task :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope (i : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP task ctx #i {{ res,
          ⌜res = ()%V⌝ ∗
          pool_context pool ctx scope ∗
          Ψ i
        }}
      )
    }}}
      algo٠for_each ctx #beg #end_ chunk task
    {{{
      RET ();
      pool_context pool ctx scope ∗
      [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
        Ψ i
    }}}.

  #[local] Lemma algo٠fold_seq𑁒spec {Ψ Χ pool ctx scope beg0} beg1 (n : nat) beg end_ end0 body op acc :
    beg = (beg1 + n)%Z →
    (beg0 ≤ beg1 ≤ beg ≤ end_ ≤ end0)%Z →
    {{{
      pool_context pool ctx scope ∗
      ( [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i (n : nat) acc v,
        ⌜beg0 ≤ i⌝%Z -∗
        ⌜i + n ≤ end0⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n)%Z v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      Χ beg1 n acc
    }}}
      algo٠fold_seq ctx #beg #end_ body op acc
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ beg1 ₊(n + end_ - beg) acc
    }}}.
  #[local] Lemma algo٠fold₀𑁒spec Ψ Χ pool ctx scope beg0 beg end_ end0 (chunk : Z) body op zero :
    (beg0 ≤ beg ≤ end_ ≤ end0)%Z →
    {{{
      pool_context pool ctx scope ∗
      ( [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i,
        ⌜beg0 ≤ i ≤ end0⌝%Z -∗
        Χ i 0 zero
      ) ∗
      □ (
        ∀ i (n : nat) acc v,
        ⌜beg0 ≤ i⌝%Z -∗
        ⌜i + n ≤ end0⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n)%Z v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      □ (
        ∀ i (n1 n2 : nat) acc1 acc2,
        ⌜beg0 ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end0⌝%Z -∗
        Χ i n1 acc1 -∗
        Χ (i + n1)%Z n2 acc2 -∗
        WP op acc1 acc2 {{ acc,
          ▷ Χ i (n1 + n2) acc
        }}
      )
    }}}
      algo٠fold₀ ctx #beg #end_ #chunk body op zero
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ beg ₊(end_ - beg) acc
    }}}.
  Lemma algo٠fold𑁒spec' (Ψ : Z → val → iProp Σ) (Χ : Z → nat → val → iProp Σ) pool sz ctx scope beg end_ chunk body op zero :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      ( [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i,
        ⌜beg ≤ i ≤ end_⌝%Z -∗
        Χ i 0 zero
      ) ∗
      □ (
        ∀ i (n : nat) acc v,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n)%Z v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      □ (
        ∀ i (n1 n2 : nat) acc1 acc2,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i n1 acc1 -∗
        Χ (i + n1)%Z n2 acc2 -∗
        WP op acc1 acc2 {{ acc,
          ▷ Χ i (n1 + n2) acc
        }}
      )
    }}}
      algo٠fold ctx #beg #end_ chunk body op zero
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ beg ₊(end_ - beg) acc
    }}}.
  Lemma algo٠fold𑁒spec_nat' (Ψ : nat → val → iProp Σ) (Χ : nat → nat → val → iProp Σ) pool sz ctx scope beg end_ chunk body op zero :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      ( [∗ list] (i : nat) ∈ seq ₊beg ₊(end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i : nat,
        ⌜beg ≤ i ≤ end_⌝%Z -∗
        Χ i 0 zero
      ) ∗
      □ (
        ∀ (i n : nat) acc v,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n) v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      □ (
        ∀ (i n1 n2 : nat) acc1 acc2,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i n1 acc1 -∗
        Χ (i + n1) n2 acc2 -∗
        WP op acc1 acc2 {{ acc,
          ▷ Χ i (n1 + n2) acc
        }}
      )
    }}}
      algo٠fold ctx #beg #end_ chunk body op zero
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ ₊beg ₊(end_ - beg) acc
    }}}.
  Lemma algo٠fold𑁒spec (Ψ : Z → val → iProp Σ) (Χ : Z → nat → val → iProp Σ) pool sz ctx scope beg end_ chunk body op zero :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope i,
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i,
        ⌜beg ≤ i ≤ end_⌝%Z -∗
        Χ i 0 zero
      ) ∗
      □ (
        ∀ i (n : nat) acc v,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n)%Z v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      □ (
        ∀ i (n1 n2 : nat) acc1 acc2,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i n1 acc1 -∗
        Χ (i + n1)%Z n2 acc2 -∗
        WP op acc1 acc2 {{ acc,
          ▷ Χ i (n1 + n2) acc
        }}
      )
    }}}
      algo٠fold ctx #beg #end_ chunk body op zero
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ beg ₊(end_ - beg) acc
    }}}.
  Lemma algo٠fold𑁒spec_nat (Ψ : nat → val → iProp Σ) (Χ : nat → nat → val → iProp Σ) pool sz ctx scope beg end_ chunk body op zero :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope (i : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP body ctx #i {{ v,
          pool_context pool ctx scope ∗
          ▷ Ψ i v
        }}
      ) ∗
      □ (
        ∀ i : nat,
        ⌜beg ≤ i ≤ end_⌝%Z -∗
        Χ i 0 zero
      ) ∗
      □ (
        ∀ (i n : nat) acc v,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n ≤ end_⌝%Z -∗
        Χ i n acc -∗
        Ψ (i + n) v -∗
        WP op acc v {{ acc,
          ▷ Χ i (S n) acc
        }}
      ) ∗
      □ (
        ∀ (i n1 n2 : nat) acc1 acc2,
        ⌜beg ≤ i⌝%Z -∗
        ⌜i + n1 + n2 ≤ end_⌝%Z -∗
        Χ i n1 acc1 -∗
        Χ (i + n1) n2 acc2 -∗
        WP op acc1 acc2 {{ acc,
          ▷ Χ i (n1 + n2) acc
        }}
      )
    }}}
      algo٠fold ctx #beg #end_ chunk body op zero
    {{{
      acc
    , RET acc;
      pool_context pool ctx scope ∗
      Χ ₊beg ₊(end_ - beg) acc
    }}}.

  #[local] Definition find_token γ q :=
    ghost_var γ (DfracOwn q) ().
  #[local] Definition find_inv γ Ψ beg end_ v : iProp Σ :=
    ∃ (i : Z) q,
    ⌜v = #i⌝ ∗
    ⌜beg ≤ i < end_⌝%Z ∗
    find_token γ q ∗
    Ψ i.
  #[local] Instance : CustomIpat "find_inv" :=
    " ( %i & %q & -> & % & Htoken{_{}} & HΨ ) ".
  #[local] Lemma algo٠find_seq𑁒spec pool ctx scope beg0 beg end_ end0 pred Ψ Χ found γ q :
    (beg0 ≤ beg ≤ end_ ≤ end0)%Z →
    {{{
      pool_context pool ctx scope ∗
      mvar_inv found (find_inv γ Ψ beg0 end0) ∗
      find_token γ q ∗
      [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
    }}}
      algo٠find_seq ctx #beg #end_ pred found
    {{{
      RET ();
      pool_context pool ctx scope ∗
      ( mvar_resolved found
      ∨ find_token γ q ∗
        [∗ list] i ∈ seqZ beg (end_ - beg),
          Χ i
      )
    }}}.
  #[local] Lemma algo٠find₀𑁒spec pool ctx scope beg0 beg end_ end0 (chunk : Z) pred Ψ Χ found γ q :
    (beg0 ≤ beg ≤ end_ ≤ end0)%Z →
    {{{
      pool_context pool ctx scope ∗
      mvar_inv found (find_inv γ Ψ beg0 end0) ∗
      find_token γ q ∗
      [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
    }}}
      algo٠find₀ ctx #beg #end_ #chunk pred found
    {{{
      RET ();
      pool_context pool ctx scope ∗
      ( mvar_resolved found
      ∨ find_token γ q ∗
        [∗ list] i ∈ seqZ beg (end_ - beg),
          Χ i
      )
    }}}.
  Lemma algo٠find𑁒spec' (Ψ Χ : Z → iProp Σ) pool sz ctx scope beg end_ chunk pred :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      [∗ list] (i : Z) ∈ seqZ beg (end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
    }}}
      algo٠find ctx #beg #end_ chunk pred
    {{{
      (o : option Z)
    , RET #*@{Z} o : option val;
      pool_context pool ctx scope ∗
      if o is Some i then
        ⌜beg ≤ i < end_⌝%Z ∗
        Ψ i
      else
        [∗ list] i ∈ seqZ beg (end_ - beg),
          Χ i
    }}}.
  Lemma algo٠find𑁒spec_nat' (Ψ Χ : nat → iProp Σ) pool sz ctx scope beg end_ chunk pred :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      [∗ list] (i : nat) ∈ seq ₊beg ₊(end_ - beg),
        ∀ ctx scope,
        pool_context pool ctx scope -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
    }}}
      algo٠find ctx #beg #end_ chunk pred
    {{{
      (o : option nat)
    , RET #*@{nat} o : option val;
      pool_context pool ctx scope ∗
      if o is Some i then
        ⌜beg ≤ i < end_⌝%Z ∗
        Ψ i
      else
        [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
          Χ i
    }}}.
  Lemma algo٠find𑁒spec (Ψ Χ : Z → iProp Σ) pool sz ctx scope beg end_ chunk pred :
    (beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope i,
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
      )
    }}}
      algo٠find ctx #beg #end_ chunk pred
    {{{
      (o : option Z)
    , RET #*@{Z} o : option val;
      pool_context pool ctx scope ∗
      if o is Some i then
        ⌜beg ≤ i < end_⌝%Z ∗
        Ψ i
      else
        [∗ list] i ∈ seqZ beg (end_ - beg),
          Χ i
    }}}.
  Lemma algo٠find𑁒spec_nat (Ψ Χ : nat → iProp Σ) pool sz ctx scope beg end_ chunk pred :
    (0 ≤ beg ≤ end_)%Z →
    {{{
      pool_inv pool sz ∗
      pool_context pool ctx scope ∗
      itype_option itype_int chunk ∗
      □ (
        ∀ ctx scope (i : nat),
        pool_context pool ctx scope -∗
        ⌜beg ≤ i < end_⌝%Z -∗
        WP pred ctx #i {{ res,
          ∃ b,
          ⌜res = #b⌝ ∗
          pool_context pool ctx scope ∗
          if b then
            Ψ i
          else
            Χ i
        }}
      )
    }}}
      algo٠find ctx #beg #end_ chunk pred
    {{{
      (o : option nat)
    , RET #*@{nat} o : option val;
      pool_context pool ctx scope ∗
      if o is Some i then
        ⌜beg ≤ i < end_⌝%Z ∗
        Ψ i
      else
        [∗ list] i ∈ seq ₊beg ₊(end_ - beg),
          Χ i
    }}}.
End algo_G.

From zoo_parabs Require
  algo__opaque.