Library zoo_std.dynarray_2
From zoo Require Import
prelude.
From zoo.common Require Import
list.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
dynarray_2__code.
From zoo_std Require Import
array
assume
diverge
dynarray_2__types
int.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i : nat.
Implicit Types l elem : location.
Implicit Types elems : list location.
Implicit Types v t data slot fn : val.
Implicit Types vs slots : list val.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Definition element_model elem v : iProp Σ :=
elem ↦ₕ Header 1 §Element ∗
elem.[value] ↦ v.
#[local] Instance : CustomIpat "element_model" :=
" ( Helem_header & Helem_value ) ".
Definition dynarray_2_model t vs : iProp Σ :=
∃ l data elems extra,
⌜t = #l⌝ ∗
l.[size] ↦ #(length vs) ∗
l.[data] ↦ data ∗
array_model data (DfracOwn 1) ((#*@{location} elems) ++ replicate extra §Empty%V) ∗
[∗ list] elem; v ∈ elems; vs, element_model elem v.
#[local] Instance : CustomIpat "model" :=
" ( %l & %data & %elems & %extra & -> & Hl_size & Hl_data & Hmodel & Helems ) ".
#[global] Instance dynarray_2_model_timeless t vs :
Timeless (dynarray_2_model t vs).
#[local] Lemma dynarray_2٠element𑁒spec v :
{{{
True
}}}
dynarray_2٠element v
{{{
elem
, RET #elem;
element_model elem v
}}}.
Lemma dynarray_2٠create𑁒spec' :
{{{
True
}}}
dynarray_2٠create ()
{{{
l
, RET #l;
dynarray_2_model #l [] ∗
meta_token l (↑nroot.@"user")
}}}.
Lemma dynarray_2٠create𑁒spec :
{{{
True
}}}
dynarray_2٠create ()
{{{
t
, RET t;
dynarray_2_model t []
}}}.
Lemma dynarray_2٠make𑁒spec sz v :
{{{
True
}}}
dynarray_2٠make #sz v
{{{
t
, RET t;
⌜0 ≤ sz⌝%Z ∗
dynarray_2_model t (replicate ₊sz v)
}}}.
Lemma dynarray_2٠initi𑁒spec Ψ sz fn :
{{{
▷ Ψ 0 [] ∗
□ (
∀ i vs,
⌜i < ₊sz ∧ i = length vs⌝ -∗
Ψ i vs -∗
WP fn #i {{ v,
▷ Ψ (S i) (vs ++ [v])
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
Ψ ₊sz vs
}}}.
Lemma dynarray_2٠initi𑁒spec' Ψ sz fn :
{{{
▷ Ψ 0 [] ∗
( [∗ list] i ∈ seq 0 ₊sz,
∀ vs,
⌜i = length vs⌝ -∗
Ψ i vs -∗
WP fn #i {{ v,
▷ Ψ (S i) (vs ++ [v])
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
Ψ ₊sz vs
}}}.
Lemma dynarray_2٠initi𑁒spec_disentangled Ψ sz fn :
{{{
□ (
∀ i,
⌜i < ₊sz⌝ -∗
WP fn #i {{ v,
▷ Ψ i v
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠initi𑁒spec_disentangled' Ψ sz fn :
{{{
( [∗ list] i ∈ seq 0 ₊sz,
WP fn #i {{ v,
▷ Ψ i v
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠size𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠size t
{{{
RET #(length vs);
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠capacity𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠capacity t
{{{
cap
, RET #cap;
⌜length vs ≤ cap⌝ ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠is_empty𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠is_empty t
{{{
RET #(bool_decide (vs = []%list));
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠get𑁒spec t vs (i : Z) v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠get t #i
{{{
RET v;
⌜0 ≤ i < length vs⌝%Z ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠set𑁒spec t vs (i : Z) v :
(0 ≤ i < length vs)%Z →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠set t #i v
{{{
RET ();
⌜0 ≤ i < length vs⌝%Z ∗
dynarray_2_model t (<[₊i := v]> vs)
}}}.
#[local] Lemma dynarray_2٠next_capacity𑁒spec n :
(0 ≤ n)%Z →
{{{
True
}}}
dynarray_2٠next_capacity #n
{{{
m
, RET #m;
⌜n ≤ m⌝%Z
}}}.
Lemma dynarray_2٠reserve𑁒spec t vs (n : Z) :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reserve t #n
{{{
RET ();
⌜0 ≤ n⌝%Z ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠reserve_extra𑁒spec t vs (n : Z) :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reserve_extra t #n
{{{
RET ();
⌜0 ≤ n⌝%Z ∗
dynarray_2_model t vs
}}}.
#[local] Lemma dynarray_2٠try_grow𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠try_grow t #sz v
{{{
b
, RET #b;
if b then
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
else
dynarray_2_model t vs
}}}.
#[local] Lemma dynarray_2٠grow₀𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠grow₀ t #sz v
{{{
RET ();
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
}}}.
Lemma dynarray_2٠grow𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠grow t #sz v
{{{
RET ();
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
}}}.
#[local] Lemma dynarray_2٠try_push𑁒spec t vs elem v :
{{{
dynarray_2_model t vs ∗
element_model elem v
}}}
dynarray_2٠try_push t #elem
{{{
b
, RET #b;
if b then
dynarray_2_model t (vs ++ [v])
else
dynarray_2_model t vs ∗
element_model elem v
}}}.
#[local] Lemma dynarray_2٠push₀𑁒spec t vs elem v :
{{{
dynarray_2_model t vs ∗
element_model elem v
}}}
dynarray_2٠push₀ t #elem
{{{
RET ();
dynarray_2_model t (vs ++ [v])
}}}.
Lemma dynarray_2٠push𑁒spec t vs v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠push t v
{{{
RET ();
dynarray_2_model t (vs ++ [v])
}}}.
Lemma dynarray_2٠pop𑁒spec {t vs} vs' v :
vs = vs' ++ [v] →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠pop t
{{{
RET v;
dynarray_2_model t vs'
}}}.
Lemma dynarray_2٠fit_capacity𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠fit_capacity t
{{{
RET ();
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠reset𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reset t
{{{
RET ();
dynarray_2_model t []
}}}.
Lemma dynarray_2٠iteri𑁒spec Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
Ψ i (take i vs) -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iteri𑁒spec' Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i (take i vs) -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iteri𑁒spec_disentangled Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iteri𑁒spec_disentangled' Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iter𑁒spec Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
Ψ i (take i vs) -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iter𑁒spec' Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i (take i vs) -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iter𑁒spec_disentangled Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iter𑁒spec_disentangled' Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Context τ `{!iType (iPropI Σ) τ}.
#[local] Definition itype_element elem : iProp Σ :=
elem ↦ₕ Header 1 §Element ∗
inv nroot (
∃ v,
elem.[value] ↦ v ∗
τ v
).
Lemma element_get𑁒type elem :
{{{
itype_element elem
}}}
(#elem).{value}
{{{
v
, RET v;
τ v
}}}.
Lemma element_set𑁒type elem v :
{{{
itype_element elem ∗
τ v
}}}
#elem <-{value} v
{{{
RET ();
True
}}}.
#[local] Definition itype_slot slot : iProp Σ :=
⌜slot = §Empty%V⌝
∨ ∃ elem,
⌜slot = #elem⌝ ∗
itype_element elem.
#[local] Instance itype_slot_itype :
iType _ itype_slot.
#[local] Lemma wp_match_slot slot e1 x e2 Φ :
itype_slot slot -∗
( WP e1 {{ Φ }} ∧
∀ elem, itype_element elem -∗ WP subst' x #elem e2 {{ Φ }}
) -∗
WP match: slot with Empty ⇒ e1 | Element ≠ as: x ⇒ e2 end {{ Φ }}.
Definition itype_dynarray_2 t : iProp Σ :=
∃ l,
⌜t = #l⌝ ∗
inv nroot (
∃ (sz : nat) cap data,
l.[size] ↦ #sz ∗
l.[data] ↦ data ∗ itype_array itype_slot cap data
).
#[global] Instance itype_dynarray_2_itype :
iType _ itype_dynarray_2.
#[local] Lemma dynarray_2٠element𑁒type v :
{{{
τ v
}}}
dynarray_2٠element v
{{{
slot
, RET slot;
itype_slot slot
}}}.
Lemma dynarray_2٠create𑁒type :
{{{
True
}}}
dynarray_2٠create ()
{{{
t
, RET t;
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠make𑁒type (sz : Z) v :
{{{
τ v
}}}
dynarray_2٠make #sz v
{{{
t
, RET t;
⌜0 ≤ sz⌝%Z ∗
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠initi𑁒type sz fn :
{{{
(itype_nat_upto ₊sz --> τ)%T fn
}}}
dynarray_2٠initi #sz fn
{{{
t
, RET t;
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠size𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠size t
{{{
(sz : nat)
, RET #sz;
True
}}}.
Lemma dynarray_2٠capacity𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠size t
{{{
(cap : nat)
, RET #cap;
True
}}}.
#[local] Lemma dynarray_2٠data𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠data t
{{{
cap data
, RET data;
itype_array itype_slot cap data
}}}.
#[local] Lemma dynarray_2٠set_size𑁒type t sz :
(0 ≤ sz)%Z →
{{{
itype_dynarray_2 t
}}}
dynarray_2٠set_size t #sz
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠set_data𑁒type t cap data :
{{{
itype_dynarray_2 t ∗
itype_array itype_slot cap data
}}}
dynarray_2٠set_data t data
{{{
RET ();
True
}}}.
Lemma dynarray_2٠is_empty𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠is_empty t
{{{
b
, RET #b;
True
}}}.
Lemma dynarray_2٠get𑁒type t (i : Z) :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠get t #i
{{{
v
, RET v;
⌜0 ≤ i⌝%Z ∗
τ v
}}}.
Lemma dynarray_2٠set𑁒type t (i : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠set t #i v
{{{
RET ();
⌜0 ≤ i⌝%Z
}}}.
Lemma dynarray_2٠reserve𑁒type t n :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reserve t #n
{{{
RET ();
⌜0 ≤ n⌝%Z
}}}.
Lemma dynarray_2٠reserve_extra𑁒type t n :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reserve_extra t #n
{{{
RET ();
⌜0 ≤ n⌝%Z
}}}.
#[local] Lemma dynarray_2٠try_grow𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠try_grow t #sz' v
{{{
b
, RET #b;
True
}}}.
#[local] Lemma dynarray_2٠grow₀𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠grow₀ t #sz' v
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠grow𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠grow t #sz' v
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠try_push𑁒type t slot :
{{{
itype_dynarray_2 t ∗
itype_slot slot
}}}
dynarray_2٠try_push t slot
{{{
b
, RET #b;
True
}}}.
#[local] Lemma dynarray_2٠push₀𑁒type t slot :
{{{
itype_dynarray_2 t ∗
itype_slot slot
}}}
dynarray_2٠push₀ t slot
{{{
RET ();
True
}}}.
Lemma dynarray_2٠push𑁒type t v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠push t v
{{{
RET ();
True
}}}.
Lemma dynarray_2٠pop𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠pop t
{{{
v
, RET v;
τ v
}}}.
Lemma dynarray_2٠fit_capacity𑁒type t v :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠fit_capacity t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠reset𑁒type t v :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reset t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠iteri𑁒type fn t :
{{{
itype_dynarray_2 t ∗
(itype_nat --> τ --> itype_unit)%T fn
}}}
dynarray_2٠iteri fn t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠iter𑁒type fn t :
{{{
itype_dynarray_2 t ∗
(τ --> itype_unit)%T fn
}}}
dynarray_2٠iter fn t
{{{
RET ();
True
}}}.
End zoo_G.
From zoo_std Require
dynarray_2__opaque.
#[global] Opaque dynarray_2_model.
#[global] Opaque itype_dynarray_2.
prelude.
From zoo.common Require Import
list.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base
dynarray_2__code.
From zoo_std Require Import
array
assume
diverge
dynarray_2__types
int.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types i : nat.
Implicit Types l elem : location.
Implicit Types elems : list location.
Implicit Types v t data slot fn : val.
Implicit Types vs slots : list val.
Section zoo_G.
Context `{zoo_G : !ZooG Σ}.
#[local] Definition element_model elem v : iProp Σ :=
elem ↦ₕ Header 1 §Element ∗
elem.[value] ↦ v.
#[local] Instance : CustomIpat "element_model" :=
" ( Helem_header & Helem_value ) ".
Definition dynarray_2_model t vs : iProp Σ :=
∃ l data elems extra,
⌜t = #l⌝ ∗
l.[size] ↦ #(length vs) ∗
l.[data] ↦ data ∗
array_model data (DfracOwn 1) ((#*@{location} elems) ++ replicate extra §Empty%V) ∗
[∗ list] elem; v ∈ elems; vs, element_model elem v.
#[local] Instance : CustomIpat "model" :=
" ( %l & %data & %elems & %extra & -> & Hl_size & Hl_data & Hmodel & Helems ) ".
#[global] Instance dynarray_2_model_timeless t vs :
Timeless (dynarray_2_model t vs).
#[local] Lemma dynarray_2٠element𑁒spec v :
{{{
True
}}}
dynarray_2٠element v
{{{
elem
, RET #elem;
element_model elem v
}}}.
Lemma dynarray_2٠create𑁒spec' :
{{{
True
}}}
dynarray_2٠create ()
{{{
l
, RET #l;
dynarray_2_model #l [] ∗
meta_token l (↑nroot.@"user")
}}}.
Lemma dynarray_2٠create𑁒spec :
{{{
True
}}}
dynarray_2٠create ()
{{{
t
, RET t;
dynarray_2_model t []
}}}.
Lemma dynarray_2٠make𑁒spec sz v :
{{{
True
}}}
dynarray_2٠make #sz v
{{{
t
, RET t;
⌜0 ≤ sz⌝%Z ∗
dynarray_2_model t (replicate ₊sz v)
}}}.
Lemma dynarray_2٠initi𑁒spec Ψ sz fn :
{{{
▷ Ψ 0 [] ∗
□ (
∀ i vs,
⌜i < ₊sz ∧ i = length vs⌝ -∗
Ψ i vs -∗
WP fn #i {{ v,
▷ Ψ (S i) (vs ++ [v])
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
Ψ ₊sz vs
}}}.
Lemma dynarray_2٠initi𑁒spec' Ψ sz fn :
{{{
▷ Ψ 0 [] ∗
( [∗ list] i ∈ seq 0 ₊sz,
∀ vs,
⌜i = length vs⌝ -∗
Ψ i vs -∗
WP fn #i {{ v,
▷ Ψ (S i) (vs ++ [v])
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
Ψ ₊sz vs
}}}.
Lemma dynarray_2٠initi𑁒spec_disentangled Ψ sz fn :
{{{
□ (
∀ i,
⌜i < ₊sz⌝ -∗
WP fn #i {{ v,
▷ Ψ i v
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠initi𑁒spec_disentangled' Ψ sz fn :
{{{
( [∗ list] i ∈ seq 0 ₊sz,
WP fn #i {{ v,
▷ Ψ i v
}}
)
}}}
dynarray_2٠initi #sz fn
{{{
t vs
, RET t;
⌜sz = length vs⌝ ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠size𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠size t
{{{
RET #(length vs);
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠capacity𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠capacity t
{{{
cap
, RET #cap;
⌜length vs ≤ cap⌝ ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠is_empty𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠is_empty t
{{{
RET #(bool_decide (vs = []%list));
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠get𑁒spec t vs (i : Z) v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠get t #i
{{{
RET v;
⌜0 ≤ i < length vs⌝%Z ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠set𑁒spec t vs (i : Z) v :
(0 ≤ i < length vs)%Z →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠set t #i v
{{{
RET ();
⌜0 ≤ i < length vs⌝%Z ∗
dynarray_2_model t (<[₊i := v]> vs)
}}}.
#[local] Lemma dynarray_2٠next_capacity𑁒spec n :
(0 ≤ n)%Z →
{{{
True
}}}
dynarray_2٠next_capacity #n
{{{
m
, RET #m;
⌜n ≤ m⌝%Z
}}}.
Lemma dynarray_2٠reserve𑁒spec t vs (n : Z) :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reserve t #n
{{{
RET ();
⌜0 ≤ n⌝%Z ∗
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠reserve_extra𑁒spec t vs (n : Z) :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reserve_extra t #n
{{{
RET ();
⌜0 ≤ n⌝%Z ∗
dynarray_2_model t vs
}}}.
#[local] Lemma dynarray_2٠try_grow𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠try_grow t #sz v
{{{
b
, RET #b;
if b then
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
else
dynarray_2_model t vs
}}}.
#[local] Lemma dynarray_2٠grow₀𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠grow₀ t #sz v
{{{
RET ();
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
}}}.
Lemma dynarray_2٠grow𑁒spec t vs sz v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠grow t #sz v
{{{
RET ();
dynarray_2_model t (vs ++ replicate (₊sz - length vs) v)
}}}.
#[local] Lemma dynarray_2٠try_push𑁒spec t vs elem v :
{{{
dynarray_2_model t vs ∗
element_model elem v
}}}
dynarray_2٠try_push t #elem
{{{
b
, RET #b;
if b then
dynarray_2_model t (vs ++ [v])
else
dynarray_2_model t vs ∗
element_model elem v
}}}.
#[local] Lemma dynarray_2٠push₀𑁒spec t vs elem v :
{{{
dynarray_2_model t vs ∗
element_model elem v
}}}
dynarray_2٠push₀ t #elem
{{{
RET ();
dynarray_2_model t (vs ++ [v])
}}}.
Lemma dynarray_2٠push𑁒spec t vs v :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠push t v
{{{
RET ();
dynarray_2_model t (vs ++ [v])
}}}.
Lemma dynarray_2٠pop𑁒spec {t vs} vs' v :
vs = vs' ++ [v] →
{{{
dynarray_2_model t vs
}}}
dynarray_2٠pop t
{{{
RET v;
dynarray_2_model t vs'
}}}.
Lemma dynarray_2٠fit_capacity𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠fit_capacity t
{{{
RET ();
dynarray_2_model t vs
}}}.
Lemma dynarray_2٠reset𑁒spec t vs :
{{{
dynarray_2_model t vs
}}}
dynarray_2٠reset t
{{{
RET ();
dynarray_2_model t []
}}}.
Lemma dynarray_2٠iteri𑁒spec Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
Ψ i (take i vs) -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iteri𑁒spec' Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i (take i vs) -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iteri𑁒spec_disentangled Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iteri𑁒spec_disentangled' Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
WP fn #i v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iteri fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iter𑁒spec Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
Ψ i (take i vs) -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iter𑁒spec' Ψ fn t vs :
{{{
▷ Ψ 0 [] ∗
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i (take i vs) -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ (S i) (take i vs ++ [v])
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
Ψ (length vs) vs
}}}.
Lemma dynarray_2٠iter𑁒spec_disentangled Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
□ (
∀ i v,
⌜vs !! i = Some v⌝ -∗
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Lemma dynarray_2٠iter𑁒spec_disentangled' Ψ fn t vs :
{{{
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
WP fn v {{ res,
⌜res = ()%V⌝ ∗
▷ Ψ i v
}}
)
}}}
dynarray_2٠iter fn t
{{{
RET ();
dynarray_2_model t vs ∗
( [∗ list] i ↦ v ∈ vs,
Ψ i v
)
}}}.
Context τ `{!iType (iPropI Σ) τ}.
#[local] Definition itype_element elem : iProp Σ :=
elem ↦ₕ Header 1 §Element ∗
inv nroot (
∃ v,
elem.[value] ↦ v ∗
τ v
).
Lemma element_get𑁒type elem :
{{{
itype_element elem
}}}
(#elem).{value}
{{{
v
, RET v;
τ v
}}}.
Lemma element_set𑁒type elem v :
{{{
itype_element elem ∗
τ v
}}}
#elem <-{value} v
{{{
RET ();
True
}}}.
#[local] Definition itype_slot slot : iProp Σ :=
⌜slot = §Empty%V⌝
∨ ∃ elem,
⌜slot = #elem⌝ ∗
itype_element elem.
#[local] Instance itype_slot_itype :
iType _ itype_slot.
#[local] Lemma wp_match_slot slot e1 x e2 Φ :
itype_slot slot -∗
( WP e1 {{ Φ }} ∧
∀ elem, itype_element elem -∗ WP subst' x #elem e2 {{ Φ }}
) -∗
WP match: slot with Empty ⇒ e1 | Element ≠ as: x ⇒ e2 end {{ Φ }}.
Definition itype_dynarray_2 t : iProp Σ :=
∃ l,
⌜t = #l⌝ ∗
inv nroot (
∃ (sz : nat) cap data,
l.[size] ↦ #sz ∗
l.[data] ↦ data ∗ itype_array itype_slot cap data
).
#[global] Instance itype_dynarray_2_itype :
iType _ itype_dynarray_2.
#[local] Lemma dynarray_2٠element𑁒type v :
{{{
τ v
}}}
dynarray_2٠element v
{{{
slot
, RET slot;
itype_slot slot
}}}.
Lemma dynarray_2٠create𑁒type :
{{{
True
}}}
dynarray_2٠create ()
{{{
t
, RET t;
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠make𑁒type (sz : Z) v :
{{{
τ v
}}}
dynarray_2٠make #sz v
{{{
t
, RET t;
⌜0 ≤ sz⌝%Z ∗
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠initi𑁒type sz fn :
{{{
(itype_nat_upto ₊sz --> τ)%T fn
}}}
dynarray_2٠initi #sz fn
{{{
t
, RET t;
itype_dynarray_2 t
}}}.
Lemma dynarray_2٠size𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠size t
{{{
(sz : nat)
, RET #sz;
True
}}}.
Lemma dynarray_2٠capacity𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠size t
{{{
(cap : nat)
, RET #cap;
True
}}}.
#[local] Lemma dynarray_2٠data𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠data t
{{{
cap data
, RET data;
itype_array itype_slot cap data
}}}.
#[local] Lemma dynarray_2٠set_size𑁒type t sz :
(0 ≤ sz)%Z →
{{{
itype_dynarray_2 t
}}}
dynarray_2٠set_size t #sz
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠set_data𑁒type t cap data :
{{{
itype_dynarray_2 t ∗
itype_array itype_slot cap data
}}}
dynarray_2٠set_data t data
{{{
RET ();
True
}}}.
Lemma dynarray_2٠is_empty𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠is_empty t
{{{
b
, RET #b;
True
}}}.
Lemma dynarray_2٠get𑁒type t (i : Z) :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠get t #i
{{{
v
, RET v;
⌜0 ≤ i⌝%Z ∗
τ v
}}}.
Lemma dynarray_2٠set𑁒type t (i : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠set t #i v
{{{
RET ();
⌜0 ≤ i⌝%Z
}}}.
Lemma dynarray_2٠reserve𑁒type t n :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reserve t #n
{{{
RET ();
⌜0 ≤ n⌝%Z
}}}.
Lemma dynarray_2٠reserve_extra𑁒type t n :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reserve_extra t #n
{{{
RET ();
⌜0 ≤ n⌝%Z
}}}.
#[local] Lemma dynarray_2٠try_grow𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠try_grow t #sz' v
{{{
b
, RET #b;
True
}}}.
#[local] Lemma dynarray_2٠grow₀𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠grow₀ t #sz' v
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠grow𑁒type t (sz' : Z) v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠grow t #sz' v
{{{
RET ();
True
}}}.
#[local] Lemma dynarray_2٠try_push𑁒type t slot :
{{{
itype_dynarray_2 t ∗
itype_slot slot
}}}
dynarray_2٠try_push t slot
{{{
b
, RET #b;
True
}}}.
#[local] Lemma dynarray_2٠push₀𑁒type t slot :
{{{
itype_dynarray_2 t ∗
itype_slot slot
}}}
dynarray_2٠push₀ t slot
{{{
RET ();
True
}}}.
Lemma dynarray_2٠push𑁒type t v :
{{{
itype_dynarray_2 t ∗
τ v
}}}
dynarray_2٠push t v
{{{
RET ();
True
}}}.
Lemma dynarray_2٠pop𑁒type t :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠pop t
{{{
v
, RET v;
τ v
}}}.
Lemma dynarray_2٠fit_capacity𑁒type t v :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠fit_capacity t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠reset𑁒type t v :
{{{
itype_dynarray_2 t
}}}
dynarray_2٠reset t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠iteri𑁒type fn t :
{{{
itype_dynarray_2 t ∗
(itype_nat --> τ --> itype_unit)%T fn
}}}
dynarray_2٠iteri fn t
{{{
RET ();
True
}}}.
Lemma dynarray_2٠iter𑁒type fn t :
{{{
itype_dynarray_2 t ∗
(τ --> itype_unit)%T fn
}}}
dynarray_2٠iter fn t
{{{
RET ();
True
}}}.
End zoo_G.
From zoo_std Require
dynarray_2__opaque.
#[global] Opaque dynarray_2_model.
#[global] Opaque itype_dynarray_2.