Library zoo_parabs.algo

Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.algo__code.
Require Import zoo_parabs.algo__types.
Require Import zoo.options.

Implicit Type b : bool.
Implicit Type v pool ctx task pred found body op zero acc : val.
Implicit Type 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 ˖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 ˖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 ˖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 ˖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 ˖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 ˖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.

Require zoo_parabs.algo__opaque.