Library examples.pool_quicksort

From zoo Require Import
  prelude.
From zoo.common Require Import
  list.
From zoo.language Require Import
  notations.
From zoo.diaframe Require Import
  diaframe.
From zoo_std Require Export
  array.
From zoo_std Require Import
  for_.
From zoo_parabs Require Import
  pool.
From examples Require Export
  pool_quicksort__code.
From zoo Require Import
  options.

Section pool_G.
  Context `{pool_G : PoolG}.

  #[local] Lemma pool_quicksort٠partition𑁒spec arr i i_ xs sz :
    (0 ≤ i)%Z →
    i_ = ₊i →
    (1 < sz)%Z →
    length xs = ₊sz →
    {{{
      array_slice arr i_ (DfracOwn 1) (#*@{Z} xs)
    }}}
      pool_quicksort٠partition arr #i #sz
    {{{
      xs1 p pivot xs2
    , RET #p;
      ⌜p = (i_ + length xs1)%nat⌝ ∗
      ⌜xs ≡ₚ xs1 ++ pivot :: xs2⌝ ∗
      ⌜Forall ((≥)%Z pivot) xs1⌝ ∗
      ⌜Forall ((≤)%Z pivot) xs2⌝ ∗
      array_slice arr i_ (DfracOwn 1) (#*@{Z} xs1 ++ #@{Z} pivot :: #*@{Z} xs2)
    }}}.
  #[local] Lemma pool_quicksort٠main₀𑁒spec pool ctx scope arr i i_ xs sz :
    (0 ≤ i)%Z →
    i_ = ₊i →
    length xs = ₊sz →
    {{{
      pool_context pool ctx scope ∗
      array_slice arr i_ (DfracOwn 1) (#*@{Z} xs)
    }}}
      pool_quicksort٠main₀ ctx arr #i #sz
    {{{
      RET ();
      pool_context pool ctx scope ∗
      pool_consumer pool (
        ∃ xs',
        ⌜xs ≡ₚ xs'⌝ ∗
        ⌜StronglySorted (≤)%Z xs'⌝ ∗
        array_slice arr i_ (DfracOwn 1) (#*@{Z} xs')
      )
    }}}.
  #[local] Lemma pool_quicksort٠main₁𑁒spec pool ctx scope arr xs :
    {{{
      pool_context pool ctx scope ∗
      array_model arr (DfracOwn 1) (#*@{Z} xs)
    }}}
      pool_quicksort٠main₁ ctx arr
    {{{
      RET ();
      pool_context pool ctx scope ∗
      pool_consumer pool (
        ∃ xs',
        ⌜xs ≡ₚ xs'⌝ ∗
        ⌜StronglySorted (≤)%Z xs'⌝ ∗
        array_model arr (DfracOwn 1) (#*@{Z} xs')
      )
    }}}.

  Lemma pool_quicksort٠main𑁒spec (num_dom : nat) arr xs :
    {{{
      array_model arr (DfracOwn 1) (#*@{Z} xs)
    }}}
      pool_quicksort٠main #num_dom arr
    {{{
      xs'
    , RET ();
      ⌜xs ≡ₚ xs'⌝ ∗
      ⌜StronglySorted (≤)%Z xs'⌝ ∗
      array_model arr (DfracOwn 1) (#*@{Z} xs')
    }}}.
End pool_G.

From examples Require
  pool_quicksort__opaque.