Library zoo_std.chunk
Require Import zoo.prelude.
Require Import zoo.common.list.
Require Import zoo.common.math.
Require Import zoo.base.
Require Import zoo.options.
Implicit Type i n : nat.
Implicit Type l : location.
Implicit Type v : val.
Implicit Type vs : list val.
Section zoo۰G.
Context `{zoo۰G : !ZooG Σ}.
Section chunk۰model.
Definition chunk۰model l dq vs : iProp Σ :=
l ↦∗{dq} vs.
#[global] Instance chunk۰modelｰtimeless l dq vs :
Timeless (chunk۰model l dq vs).
#[global] Instance chunk۰modelｰpersistent l vs :
Persistent (chunk۰model l DfracDiscarded vs).
#[global] Instance chunk۰modelｰfractional l vs :
Fractional (λ q, chunk۰model l (DfracOwn q) vs).
#[global] Instance chunk۰modelｰas_fractional l q vs :
AsFractional (chunk۰model l (DfracOwn q) vs) (λ q, chunk۰model l (DfracOwn q) vs) q.
Lemma chunk۰modelｰnil l dq :
⊢ chunk۰model l dq [].
Lemma chunk۰modelｰsingleton l dq v :
l ↦{dq} v ⊣⊢
chunk۰model l dq [v].
Lemma chunk۰modelｰsingleton₁ l dq v :
l ↦{dq} v ⊢
chunk۰model l dq [v].
Lemma chunk۰modelｰsingleton₂ l dq v :
chunk۰model l dq [v] ⊢
l ↦{dq} v.
Lemma chunk۰modelｰapp l dq vs1 vs2 :
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ⊣⊢
chunk۰model l dq (vs1 ++ vs2).
Lemma chunk۰modelｰapp₁ dq l1 vs1 l2 vs2 :
l2 = l1 +ₗ length vs1 →
chunk۰model l1 dq vs1 -∗
chunk۰model l2 dq vs2 -∗
chunk۰model l1 dq (vs1 ++ vs2).
Lemma chunk۰modelｰapp₂ {l dq vs} vs1 vs2 :
vs = vs1 ++ vs2 →
chunk۰model l dq vs ⊢
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2.
Lemma chunk۰modelｰappｰ3 l dq vs1 vs2 vs3 :
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ∗
chunk۰model (l +ₗ ⁺(length vs1 + length vs2)) dq vs3 ⊣⊢
chunk۰model l dq (vs1 ++ vs2 ++ vs3).
Lemma chunk۰modelｰappｰ3₁ dq l1 vs1 l2 vs2 l3 vs3 :
l2 = l1 +ₗ length vs1 →
l3 = l1 +ₗ ⁺(length vs1 + length vs2) →
chunk۰model l1 dq vs1 -∗
chunk۰model l2 dq vs2 -∗
chunk۰model l3 dq vs3 -∗
chunk۰model l1 dq (vs1 ++ vs2 ++ vs3).
Lemma chunk۰modelｰappｰ3₂ {l dq vs} vs1 vs2 vs3 :
vs = vs1 ++ vs2 ++ vs3 →
chunk۰model l dq vs ⊢
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ∗
chunk۰model (l +ₗ ⁺(length vs1 + length vs2)) dq vs3.
Lemma chunk۰modelｰcons l dq v vs :
l ↦{dq} v ∗
chunk۰model (l +ₗ 1) dq vs ⊣⊢
chunk۰model l dq (v :: vs).
Lemma chunk۰modelｰcons₁ l dq v vs :
l ↦{dq} v -∗
chunk۰model (l +ₗ 1) dq vs -∗
chunk۰model l dq (v :: vs).
Lemma chunk۰modelｰcons₂ l dq v vs :
chunk۰model l dq (v :: vs) ⊢
l ↦{dq} v ∗
chunk۰model (l +ₗ 1) dq vs.
#[global] Instance chunk۰modelｰconsｰframe l dq v vs R Q :
Frame false R (l ↦{dq} v ∗ chunk۰model (l +ₗ 1) dq vs) Q →
Frame false R (chunk۰model l dq (v :: vs)) Q
| 2.
Lemma chunk۰modelｰupdate {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v ∗
( ∀ w,
(l +ₗ i) ↦{dq} w -∗
chunk۰model l dq (<[i_ := w]> vs)
).
Lemma chunk۰modelｰlookupｰacc {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v ∗
( (l +ₗ i) ↦{dq} v -∗
chunk۰model l dq vs
).
Lemma chunk۰modelｰlookup {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v.
Lemma chunk۰modelｰupdate' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v ∗
( ∀ w,
(l +ₗ j) ↦{dq} w -∗
chunk۰model (l +ₗ i) dq (<[k := w]> vs)
).
Lemma chunk۰modelｰlookupｰacc' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v ∗
( (l +ₗ j) ↦{dq} v -∗
chunk۰model (l +ₗ i) dq vs
).
Lemma chunk۰modelｰlookup' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v.
Lemma chunk۰modelｰvalid l dq vs :
0 < length vs →
chunk۰model l dq vs ⊢
⌜✓ dq⌝.
Lemma chunk۰modelｰcombine l dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜vs1 = vs2⌝ ∗
chunk۰model l (dq1 ⋅ dq2) vs1.
Lemma chunk۰modelｰvalidｰ2 l dq1 vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜vs1 = vs2⌝.
Lemma chunk۰modelｰagree l dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜vs1 = vs2⌝.
Lemma chunk۰modelｰdfracｰne l1 dq1 vs1 l2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰model l1 dq1 vs1 -∗
chunk۰model l2 dq2 vs2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰modelｰne l1 vs1 l2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l1 (DfracOwn 1) vs1 -∗
chunk۰model l2 dq2 vs2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰modelｰexclusive l vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l (DfracOwn 1) vs1 -∗
chunk۰model l dq2 vs2 -∗
False.
Lemma chunk۰modelｰpersist l dq vs :
chunk۰model l dq vs ⊢ |==>
chunk۰model l DfracDiscarded vs.
End chunk۰model.
Section chunk۰span.
Definition chunk۰span l dq n : iProp Σ :=
∃ vs,
⌜length vs = n⌝ ∗
chunk۰model l dq vs.
#[global] Instance chunk۰spanｰtimeless l dq n :
Timeless (chunk۰span l dq n).
#[global] Instance chunk۰spanｰpersistent l n :
Persistent (chunk۰span l DfracDiscarded n).
#[global] Instance chunk۰spanｰfractional l n :
Fractional (λ q, chunk۰span l (DfracOwn q) n).
#[global] Instance chunk۰spanｰas_fractional l q n :
AsFractional (chunk۰span l (DfracOwn q) n) (λ q, chunk۰span l (DfracOwn q) n) q.
Lemma chunk۰spanｰsingleton l dq :
( ∃ v,
l ↦{dq} v
) ⊣⊢
chunk۰span l dq 1.
Lemma chunk۰spanｰsingleton₁ l dq v :
l ↦{dq} v ⊢
chunk۰span l dq 1.
Lemma chunk۰spanｰsingleton₂ l dq :
chunk۰span l dq 1 ⊢
∃ v,
l ↦{dq} v.
Lemma chunk۰spanｰcons l dq n :
( ∃ v,
l ↦{dq} v ∗
chunk۰span (l +ₗ 1) dq n
) ⊣⊢
chunk۰span l dq ˖n.
Lemma chunk۰spanｰcons₁ l dq v n :
l ↦{dq} v -∗
chunk۰span (l +ₗ 1) dq n -∗
chunk۰span l dq ˖n.
Lemma chunk۰spanｰcons₂ l dq n :
chunk۰span l dq ˖n ⊢
∃ v,
l ↦{dq} v ∗
chunk۰span (l +ₗ 1) dq n.
#[global] Instance chunk۰spanｰconsｰframe l dq v n R Q :
Frame false R (l ↦{dq} v ∗ chunk۰span (l +ₗ 1) dq n) Q →
Frame false R (chunk۰span l dq ˖n) Q
| 2.
Lemma chunk۰spanｰapp l dq n1 n2 :
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ⊣⊢
chunk۰span l dq (n1 + n2).
Lemma chunk۰spanｰapp₁ dq l1 (n1 : nat) l2 n2 :
l2 = l1 +ₗ n1 →
chunk۰span l1 dq n1 -∗
chunk۰span l2 dq n2 -∗
chunk۰span l1 dq (n1 + n2).
Lemma chunk۰spanｰapp₂ {l dq n} n1 n2 :
n = n1 + n2 →
chunk۰span l dq n ⊢
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2.
Lemma chunk۰spanｰappｰ3 l dq n1 (n2 : nat) n3 :
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ∗
chunk۰span (l +ₗ ⁺(n1 + n2)) dq n3 ⊣⊢
chunk۰span l dq (n1 + n2 + n3).
Lemma chunk۰spanｰappｰ3₁ dq l1 n1 l2 n2 l3 n3 :
l2 = l1 +ₗ n1 →
l3 = l1 +ₗ ⁺(n1 + n2) →
chunk۰span l1 dq n1 -∗
chunk۰span l2 dq n2 -∗
chunk۰span l3 dq n3 -∗
chunk۰span l1 dq (n1 + n2 + n3).
Lemma chunk۰spanｰappｰ3₂ {l dq n} n1 n2 n3 :
n = n1 + n2 + n3 →
chunk۰span l dq n ⊢
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ∗
chunk۰span (l +ₗ ⁺(n1 + n2)) dq n3.
Lemma chunk۰spanｰupdate {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v ∗
( ∀ w,
(l +ₗ i) ↦{dq} w -∗
chunk۰span l dq n
).
Lemma chunk۰spanｰlookupｰacc {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v ∗
( (l +ₗ i) ↦{dq} v -∗
chunk۰span l dq n
).
Lemma chunk۰spanｰlookup {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v.
Lemma chunk۰spanｰupdate' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v ∗
( ∀ w,
(l +ₗ j) ↦{dq} w -∗
chunk۰span (l +ₗ i) dq n
).
Lemma chunk۰spanｰlookupｰacc' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v ∗
( (l +ₗ j) ↦{dq} v -∗
chunk۰span (l +ₗ i) dq n
).
Lemma chunk۰spanｰlookup' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v.
Lemma chunk۰spanｰvalid l dq n :
0 < n →
chunk۰span l dq n ⊢
⌜✓ dq⌝.
Lemma chunk۰spanｰcombine l dq1 n1 dq2 n2 :
n1 = n2 →
chunk۰span l dq1 n1 -∗
chunk۰span l dq2 n2 -∗
chunk۰span l (dq1 ⋅ dq2) n1.
Lemma chunk۰spanｰvalidｰ2 l dq1 n1 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l dq1 n1 -∗
chunk۰span l dq2 n2 -∗
⌜✓ (dq1 ⋅ dq2)⌝.
Lemma chunk۰spanｰdfracｰne l1 dq1 n1 l2 dq2 n2 :
n1 = n2 →
0 < n1 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰span l1 dq1 n1 -∗
chunk۰span l2 dq2 n2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰spanｰne l1 n1 l2 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l1 (DfracOwn 1) n1 -∗
chunk۰span l2 dq2 n2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰spanｰexclusive l n1 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l (DfracOwn 1) n1 -∗
chunk۰span l dq2 n2 -∗
False.
Lemma chunk۰spanｰpersist l dq n :
chunk۰span l dq n ⊢ |==>
chunk۰span l DfracDiscarded n.
End chunk۰span.
Section chunk۰cslice.
Implicit Type sz : nat.
Definition chunk۰cslice l sz i dq vs : iProp Σ :=
[∗ list] k ↦ v ∈ vs, (l +ₗ (i + k) `mod` sz) ↦{dq} v.
#[global] Instance chunk۰csliceｰtimeless l sz i dq vs :
Timeless (chunk۰cslice l sz i dq vs).
#[global] Instance chunk۰csliceｰpersistent l sz i vs :
Persistent (chunk۰cslice l sz i DfracDiscarded vs).
#[global] Instance chunk۰csliceｰfractional l sz i vs :
Fractional (λ q, chunk۰cslice l sz i (DfracOwn q) vs).
#[global] Instance chunk۰csliceｰas_fractionak l sz i q vs :
AsFractional (chunk۰cslice l sz i (DfracOwn q) vs) (λ q, chunk۰cslice l sz i (DfracOwn q) vs) q.
Lemma chunk۰modelｰtoｰcslice l dq vs :
chunk۰model l dq vs ⊢
chunk۰cslice l (length vs) 0 dq vs.
Lemma chunkｰmodelｰcsliceｰcell l i sz dq v :
chunk۰model (l +ₗ i `mod` sz) dq [v] ⊣⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰnil l sz i dq :
⊢ chunk۰cslice l sz i dq [].
Lemma chunk۰csliceｰsingleton l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊣⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰsingleton₁ l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰsingleton₂ l sz i dq v :
chunk۰cslice l sz i dq [v] ⊢
(l +ₗ i `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰapp l sz i dq vs1 vs2 :
chunk۰cslice l sz i dq vs1 ∗
chunk۰cslice l sz (i + length vs1) dq vs2 ⊣⊢
chunk۰cslice l sz i dq (vs1 ++ vs2).
Lemma chunk۰csliceｰapp₁ l sz dq i1 vs1 i2 vs2 :
i2 = i1 + length vs1 →
chunk۰cslice l sz i1 dq vs1 -∗
chunk۰cslice l sz i2 dq vs2 -∗
chunk۰cslice l sz i1 dq (vs1 ++ vs2).
Lemma chunk۰csliceｰapp₂ {l sz i dq vs} vs1 vs2 :
vs = vs1 ++ vs2 →
chunk۰cslice l sz i dq vs ⊢
chunk۰cslice l sz i dq vs1 ∗
chunk۰cslice l sz (i + length vs1) dq vs2.
Lemma chunk۰csliceｰappｰ3 {l sz i dq vs} n1 i1 n2 i2 :
i1 = i + n1 →
i2 = i1 + n2 →
n1 ≤ length vs →
n1 + n2 ≤ length vs →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz i dq (take n1 vs) ∗
chunk۰cslice l sz i1 dq (take n2 $ drop n1 vs) ∗
chunk۰cslice l sz i2 dq (drop (n1 + n2) vs).
Lemma chunk۰csliceｰcons l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk۰cslice l sz ˖i dq vs ⊣⊢
chunk۰cslice l sz i dq (v :: vs).
Lemma chunk۰csliceｰcons₁ l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz ˖i dq vs -∗
chunk۰cslice l sz i dq (v :: vs).
Lemma chunk۰csliceｰcons₂ l sz i dq v vs :
chunk۰cslice l sz i dq (v :: vs) ⊢
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk۰cslice l sz ˖i dq vs.
Lemma chunk۰csliceｰupdate {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v ∗
( ∀ w,
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} w -∗
chunk۰cslice l sz i dq (<[k := w]> vs)
).
Lemma chunk۰csliceｰlookupｰacc {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v ∗
( (l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz i dq vs
).
Lemma chunk۰csliceｰlookup {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰupdate' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v ∗
( ∀ w,
(l +ₗ j `mod` sz) ↦{dq} w -∗
chunk۰cslice l sz i dq (<[k := w]> vs)
).
Lemma chunk۰csliceｰlookupｰacc' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v ∗
( (l +ₗ j `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz i dq vs
).
Lemma chunk۰csliceｰlookup' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰshift l sz i dq vs :
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + sz) dq vs.
Lemma chunk۰csliceｰshiftｰright l sz i dq vs :
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + sz) dq vs.
Lemma chunk۰csliceｰshiftｰleft l sz i dq vs :
sz ≤ i →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i - sz) dq vs.
Lemma chunk۰csliceｰmod l sz i dq vs :
0 < sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i `mod` sz) dq vs.
#[local] Lemma chunk۰csliceｰtoｰmodelｰaux l sz i dq vs :
0 < sz →
i + length vs ≤ sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model (l +ₗ i) dq vs.
Lemma chunk۰csliceｰtoｰmodel l sz i dq vs :
0 < sz →
length vs ≤ sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model (l +ₗ ⁺(i `mod` sz)) dq (take (sz - i `mod` sz) vs) ∗
chunk۰model l dq (drop (sz - i `mod` sz) vs).
Lemma chunk۰csliceｰtoｰmodelｰfull l sz i dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model l dq (rotation (sz - i `mod` sz) vs).
#[local] Lemma chunk۰csliceｰrotationｰrightｰaux {l sz} i1 i2 dq vs :
0 < sz →
length vs = sz →
i1 `mod` sz ≤ i2 `mod` sz →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (i2 `mod` sz - i1 `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright {l sz i dq vs} n :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + n) dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright₁ {l sz i dq vs} n :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊢
chunk۰cslice l sz (i + n) dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰrightｰ0 {l sz dq vs} i :
0 < sz →
length vs = sz →
chunk۰cslice l sz 0 dq vs ⊣⊢
chunk۰cslice l sz i dq (rotation (i `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i2 = i1 + n →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright₁' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i2 = i1 + n →
chunk۰cslice l sz i1 dq vs ⊢
chunk۰cslice l sz i2 dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft l sz i n dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz (i + n) dq vs ⊣⊢
chunk۰cslice l sz i dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft₁ l sz i n dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz (i + n) dq vs ⊢
chunk۰cslice l sz i dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleftｰ0 l sz i dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz 0 dq (rotation (sz - i `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i1 = i2 + n →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft₁' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i1 = i2 + n →
chunk۰cslice l sz i1 dq vs ⊢
chunk۰cslice l sz i2 dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrebase {l sz i1 dq vs1} i2 :
0 < sz →
length vs1 = sz →
chunk۰cslice l sz i1 dq vs1 ⊢
∃ vs2 n,
⌜vs2 = rotation n vs1⌝ ∗
chunk۰cslice l sz i2 dq vs2 ∗
( chunk۰cslice l sz i2 dq vs2 -∗
chunk۰cslice l sz i1 dq vs1
).
Lemma chunk۰csliceｰvalid l sz i dq vs :
0 < length vs →
chunk۰cslice l sz i dq vs ⊢
⌜✓ dq⌝.
Lemma chunk۰csliceｰcombine l sz i dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜vs1 = vs2⌝ ∗
chunk۰cslice l sz i (dq1 ⋅ dq2) vs1.
Lemma chunk۰csliceｰvalidｰ2 l sz i dq1 vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜vs1 = vs2⌝.
Lemma chunk۰csliceｰagree l sz i dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜vs1 = vs2⌝.
Lemma chunk۰csliceｰdfracｰne l sz i1 dq1 vs1 i2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰cslice l sz i1 dq1 vs1 -∗
chunk۰cslice l sz i2 dq2 vs2 -∗
⌜i1 ≠ i2⌝.
Lemma chunk۰csliceｰne l sz i1 vs1 i2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i1 (DfracOwn 1) vs1 -∗
chunk۰cslice l sz i2 dq2 vs2 -∗
⌜i1 ≠ i2⌝.
Lemma chunk۰csliceｰexclusive l sz i vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i (DfracOwn 1) vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
False.
Lemma chunk۰csliceｰpersist l sz i dq vs :
chunk۰cslice l sz i dq vs ⊢ |==>
chunk۰cslice l sz i DfracDiscarded vs.
Lemma chunk۰csliceｰlength l sz i vs :
0 < sz →
chunk۰cslice l sz i (DfracOwn 1) vs ⊢
⌜length vs ≤ sz⌝.
End chunk۰cslice.
Section itype۰chunk.
Definition itype۰chunk τ `{!iType _ τ} sz l : iProp Σ :=
inv nroot (
∃ vs,
⌜sz = length vs⌝ ∗
chunk۰model l (DfracOwn 1) vs ∗
[∗ list] v ∈ vs, τ v
).
#[global] Instance itype۰chunkｰpersistent τ `{!iType _ τ} sz l :
Persistent (itype۰chunk τ sz l).
Lemma itype۰chunkｰ0 τ `{!iType _ τ} l :
⊢ |={⊤}=>
itype۰chunk τ 0 l.
Lemma itype۰chunkｰshift (i : Z) τ `{!iType _ τ} (sz : nat) l :
(0 ≤ i ≤ sz)%Z →
itype۰chunk τ sz l ⊢
itype۰chunk τ (sz - ₊i) (l +ₗ i).
Lemma itype۰chunkｰle sz' τ `{!iType _ τ} sz l :
(sz' ≤ sz) →
itype۰chunk τ sz l ⊢
itype۰chunk τ sz' l.
End itype۰chunk.
End zoo۰G.
#[global] Opaque chunk۰model.
#[global] Opaque chunk۰span.
#[global] Opaque chunk۰cslice.
Require Import zoo.common.list.
Require Import zoo.common.math.
Require Import zoo.base.
Require Import zoo.options.
Implicit Type i n : nat.
Implicit Type l : location.
Implicit Type v : val.
Implicit Type vs : list val.
Section zoo۰G.
Context `{zoo۰G : !ZooG Σ}.
Section chunk۰model.
Definition chunk۰model l dq vs : iProp Σ :=
l ↦∗{dq} vs.
#[global] Instance chunk۰modelｰtimeless l dq vs :
Timeless (chunk۰model l dq vs).
#[global] Instance chunk۰modelｰpersistent l vs :
Persistent (chunk۰model l DfracDiscarded vs).
#[global] Instance chunk۰modelｰfractional l vs :
Fractional (λ q, chunk۰model l (DfracOwn q) vs).
#[global] Instance chunk۰modelｰas_fractional l q vs :
AsFractional (chunk۰model l (DfracOwn q) vs) (λ q, chunk۰model l (DfracOwn q) vs) q.
Lemma chunk۰modelｰnil l dq :
⊢ chunk۰model l dq [].
Lemma chunk۰modelｰsingleton l dq v :
l ↦{dq} v ⊣⊢
chunk۰model l dq [v].
Lemma chunk۰modelｰsingleton₁ l dq v :
l ↦{dq} v ⊢
chunk۰model l dq [v].
Lemma chunk۰modelｰsingleton₂ l dq v :
chunk۰model l dq [v] ⊢
l ↦{dq} v.
Lemma chunk۰modelｰapp l dq vs1 vs2 :
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ⊣⊢
chunk۰model l dq (vs1 ++ vs2).
Lemma chunk۰modelｰapp₁ dq l1 vs1 l2 vs2 :
l2 = l1 +ₗ length vs1 →
chunk۰model l1 dq vs1 -∗
chunk۰model l2 dq vs2 -∗
chunk۰model l1 dq (vs1 ++ vs2).
Lemma chunk۰modelｰapp₂ {l dq vs} vs1 vs2 :
vs = vs1 ++ vs2 →
chunk۰model l dq vs ⊢
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2.
Lemma chunk۰modelｰappｰ3 l dq vs1 vs2 vs3 :
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ∗
chunk۰model (l +ₗ ⁺(length vs1 + length vs2)) dq vs3 ⊣⊢
chunk۰model l dq (vs1 ++ vs2 ++ vs3).
Lemma chunk۰modelｰappｰ3₁ dq l1 vs1 l2 vs2 l3 vs3 :
l2 = l1 +ₗ length vs1 →
l3 = l1 +ₗ ⁺(length vs1 + length vs2) →
chunk۰model l1 dq vs1 -∗
chunk۰model l2 dq vs2 -∗
chunk۰model l3 dq vs3 -∗
chunk۰model l1 dq (vs1 ++ vs2 ++ vs3).
Lemma chunk۰modelｰappｰ3₂ {l dq vs} vs1 vs2 vs3 :
vs = vs1 ++ vs2 ++ vs3 →
chunk۰model l dq vs ⊢
chunk۰model l dq vs1 ∗
chunk۰model (l +ₗ length vs1) dq vs2 ∗
chunk۰model (l +ₗ ⁺(length vs1 + length vs2)) dq vs3.
Lemma chunk۰modelｰcons l dq v vs :
l ↦{dq} v ∗
chunk۰model (l +ₗ 1) dq vs ⊣⊢
chunk۰model l dq (v :: vs).
Lemma chunk۰modelｰcons₁ l dq v vs :
l ↦{dq} v -∗
chunk۰model (l +ₗ 1) dq vs -∗
chunk۰model l dq (v :: vs).
Lemma chunk۰modelｰcons₂ l dq v vs :
chunk۰model l dq (v :: vs) ⊢
l ↦{dq} v ∗
chunk۰model (l +ₗ 1) dq vs.
#[global] Instance chunk۰modelｰconsｰframe l dq v vs R Q :
Frame false R (l ↦{dq} v ∗ chunk۰model (l +ₗ 1) dq vs) Q →
Frame false R (chunk۰model l dq (v :: vs)) Q
| 2.
Lemma chunk۰modelｰupdate {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v ∗
( ∀ w,
(l +ₗ i) ↦{dq} w -∗
chunk۰model l dq (<[i_ := w]> vs)
).
Lemma chunk۰modelｰlookupｰacc {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v ∗
( (l +ₗ i) ↦{dq} v -∗
chunk۰model l dq vs
).
Lemma chunk۰modelｰlookup {l dq vs} (i : Z) i_ v :
(0 ≤ i)%Z →
vs !! i_ = Some v →
i_ = ₊i →
chunk۰model l dq vs ⊢
(l +ₗ i) ↦{dq} v.
Lemma chunk۰modelｰupdate' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v ∗
( ∀ w,
(l +ₗ j) ↦{dq} w -∗
chunk۰model (l +ₗ i) dq (<[k := w]> vs)
).
Lemma chunk۰modelｰlookupｰacc' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v ∗
( (l +ₗ j) ↦{dq} v -∗
chunk۰model (l +ₗ i) dq vs
).
Lemma chunk۰modelｰlookup' {l} {i : Z} {dq vs} j k v :
(0 ≤ i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - ₊i →
chunk۰model (l +ₗ i) dq vs ⊢
(l +ₗ j) ↦{dq} v.
Lemma chunk۰modelｰvalid l dq vs :
0 < length vs →
chunk۰model l dq vs ⊢
⌜✓ dq⌝.
Lemma chunk۰modelｰcombine l dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜vs1 = vs2⌝ ∗
chunk۰model l (dq1 ⋅ dq2) vs1.
Lemma chunk۰modelｰvalidｰ2 l dq1 vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜vs1 = vs2⌝.
Lemma chunk۰modelｰagree l dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰model l dq1 vs1 -∗
chunk۰model l dq2 vs2 -∗
⌜vs1 = vs2⌝.
Lemma chunk۰modelｰdfracｰne l1 dq1 vs1 l2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰model l1 dq1 vs1 -∗
chunk۰model l2 dq2 vs2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰modelｰne l1 vs1 l2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l1 (DfracOwn 1) vs1 -∗
chunk۰model l2 dq2 vs2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰modelｰexclusive l vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰model l (DfracOwn 1) vs1 -∗
chunk۰model l dq2 vs2 -∗
False.
Lemma chunk۰modelｰpersist l dq vs :
chunk۰model l dq vs ⊢ |==>
chunk۰model l DfracDiscarded vs.
End chunk۰model.
Section chunk۰span.
Definition chunk۰span l dq n : iProp Σ :=
∃ vs,
⌜length vs = n⌝ ∗
chunk۰model l dq vs.
#[global] Instance chunk۰spanｰtimeless l dq n :
Timeless (chunk۰span l dq n).
#[global] Instance chunk۰spanｰpersistent l n :
Persistent (chunk۰span l DfracDiscarded n).
#[global] Instance chunk۰spanｰfractional l n :
Fractional (λ q, chunk۰span l (DfracOwn q) n).
#[global] Instance chunk۰spanｰas_fractional l q n :
AsFractional (chunk۰span l (DfracOwn q) n) (λ q, chunk۰span l (DfracOwn q) n) q.
Lemma chunk۰spanｰsingleton l dq :
( ∃ v,
l ↦{dq} v
) ⊣⊢
chunk۰span l dq 1.
Lemma chunk۰spanｰsingleton₁ l dq v :
l ↦{dq} v ⊢
chunk۰span l dq 1.
Lemma chunk۰spanｰsingleton₂ l dq :
chunk۰span l dq 1 ⊢
∃ v,
l ↦{dq} v.
Lemma chunk۰spanｰcons l dq n :
( ∃ v,
l ↦{dq} v ∗
chunk۰span (l +ₗ 1) dq n
) ⊣⊢
chunk۰span l dq ˖n.
Lemma chunk۰spanｰcons₁ l dq v n :
l ↦{dq} v -∗
chunk۰span (l +ₗ 1) dq n -∗
chunk۰span l dq ˖n.
Lemma chunk۰spanｰcons₂ l dq n :
chunk۰span l dq ˖n ⊢
∃ v,
l ↦{dq} v ∗
chunk۰span (l +ₗ 1) dq n.
#[global] Instance chunk۰spanｰconsｰframe l dq v n R Q :
Frame false R (l ↦{dq} v ∗ chunk۰span (l +ₗ 1) dq n) Q →
Frame false R (chunk۰span l dq ˖n) Q
| 2.
Lemma chunk۰spanｰapp l dq n1 n2 :
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ⊣⊢
chunk۰span l dq (n1 + n2).
Lemma chunk۰spanｰapp₁ dq l1 (n1 : nat) l2 n2 :
l2 = l1 +ₗ n1 →
chunk۰span l1 dq n1 -∗
chunk۰span l2 dq n2 -∗
chunk۰span l1 dq (n1 + n2).
Lemma chunk۰spanｰapp₂ {l dq n} n1 n2 :
n = n1 + n2 →
chunk۰span l dq n ⊢
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2.
Lemma chunk۰spanｰappｰ3 l dq n1 (n2 : nat) n3 :
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ∗
chunk۰span (l +ₗ ⁺(n1 + n2)) dq n3 ⊣⊢
chunk۰span l dq (n1 + n2 + n3).
Lemma chunk۰spanｰappｰ3₁ dq l1 n1 l2 n2 l3 n3 :
l2 = l1 +ₗ n1 →
l3 = l1 +ₗ ⁺(n1 + n2) →
chunk۰span l1 dq n1 -∗
chunk۰span l2 dq n2 -∗
chunk۰span l3 dq n3 -∗
chunk۰span l1 dq (n1 + n2 + n3).
Lemma chunk۰spanｰappｰ3₂ {l dq n} n1 n2 n3 :
n = n1 + n2 + n3 →
chunk۰span l dq n ⊢
chunk۰span l dq n1 ∗
chunk۰span (l +ₗ n1) dq n2 ∗
chunk۰span (l +ₗ ⁺(n1 + n2)) dq n3.
Lemma chunk۰spanｰupdate {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v ∗
( ∀ w,
(l +ₗ i) ↦{dq} w -∗
chunk۰span l dq n
).
Lemma chunk۰spanｰlookupｰacc {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v ∗
( (l +ₗ i) ↦{dq} v -∗
chunk۰span l dq n
).
Lemma chunk۰spanｰlookup {l dq n} (i : Z) :
(0 ≤ i < n)%Z →
chunk۰span l dq n ⊢
∃ v,
(l +ₗ i) ↦{dq} v.
Lemma chunk۰spanｰupdate' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v ∗
( ∀ w,
(l +ₗ j) ↦{dq} w -∗
chunk۰span (l +ₗ i) dq n
).
Lemma chunk۰spanｰlookupｰacc' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v ∗
( (l +ₗ j) ↦{dq} v -∗
chunk۰span (l +ₗ i) dq n
).
Lemma chunk۰spanｰlookup' {l} {i : Z} {dq n} j :
(0 ≤ i ≤ j ∧ j < i + n)%Z →
chunk۰span (l +ₗ i) dq n ⊢
∃ v,
(l +ₗ j) ↦{dq} v.
Lemma chunk۰spanｰvalid l dq n :
0 < n →
chunk۰span l dq n ⊢
⌜✓ dq⌝.
Lemma chunk۰spanｰcombine l dq1 n1 dq2 n2 :
n1 = n2 →
chunk۰span l dq1 n1 -∗
chunk۰span l dq2 n2 -∗
chunk۰span l (dq1 ⋅ dq2) n1.
Lemma chunk۰spanｰvalidｰ2 l dq1 n1 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l dq1 n1 -∗
chunk۰span l dq2 n2 -∗
⌜✓ (dq1 ⋅ dq2)⌝.
Lemma chunk۰spanｰdfracｰne l1 dq1 n1 l2 dq2 n2 :
n1 = n2 →
0 < n1 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰span l1 dq1 n1 -∗
chunk۰span l2 dq2 n2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰spanｰne l1 n1 l2 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l1 (DfracOwn 1) n1 -∗
chunk۰span l2 dq2 n2 -∗
⌜l1 ≠ l2⌝.
Lemma chunk۰spanｰexclusive l n1 dq2 n2 :
n1 = n2 →
0 < n1 →
chunk۰span l (DfracOwn 1) n1 -∗
chunk۰span l dq2 n2 -∗
False.
Lemma chunk۰spanｰpersist l dq n :
chunk۰span l dq n ⊢ |==>
chunk۰span l DfracDiscarded n.
End chunk۰span.
Section chunk۰cslice.
Implicit Type sz : nat.
Definition chunk۰cslice l sz i dq vs : iProp Σ :=
[∗ list] k ↦ v ∈ vs, (l +ₗ (i + k) `mod` sz) ↦{dq} v.
#[global] Instance chunk۰csliceｰtimeless l sz i dq vs :
Timeless (chunk۰cslice l sz i dq vs).
#[global] Instance chunk۰csliceｰpersistent l sz i vs :
Persistent (chunk۰cslice l sz i DfracDiscarded vs).
#[global] Instance chunk۰csliceｰfractional l sz i vs :
Fractional (λ q, chunk۰cslice l sz i (DfracOwn q) vs).
#[global] Instance chunk۰csliceｰas_fractionak l sz i q vs :
AsFractional (chunk۰cslice l sz i (DfracOwn q) vs) (λ q, chunk۰cslice l sz i (DfracOwn q) vs) q.
Lemma chunk۰modelｰtoｰcslice l dq vs :
chunk۰model l dq vs ⊢
chunk۰cslice l (length vs) 0 dq vs.
Lemma chunkｰmodelｰcsliceｰcell l i sz dq v :
chunk۰model (l +ₗ i `mod` sz) dq [v] ⊣⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰnil l sz i dq :
⊢ chunk۰cslice l sz i dq [].
Lemma chunk۰csliceｰsingleton l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊣⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰsingleton₁ l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊢
chunk۰cslice l sz i dq [v].
Lemma chunk۰csliceｰsingleton₂ l sz i dq v :
chunk۰cslice l sz i dq [v] ⊢
(l +ₗ i `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰapp l sz i dq vs1 vs2 :
chunk۰cslice l sz i dq vs1 ∗
chunk۰cslice l sz (i + length vs1) dq vs2 ⊣⊢
chunk۰cslice l sz i dq (vs1 ++ vs2).
Lemma chunk۰csliceｰapp₁ l sz dq i1 vs1 i2 vs2 :
i2 = i1 + length vs1 →
chunk۰cslice l sz i1 dq vs1 -∗
chunk۰cslice l sz i2 dq vs2 -∗
chunk۰cslice l sz i1 dq (vs1 ++ vs2).
Lemma chunk۰csliceｰapp₂ {l sz i dq vs} vs1 vs2 :
vs = vs1 ++ vs2 →
chunk۰cslice l sz i dq vs ⊢
chunk۰cslice l sz i dq vs1 ∗
chunk۰cslice l sz (i + length vs1) dq vs2.
Lemma chunk۰csliceｰappｰ3 {l sz i dq vs} n1 i1 n2 i2 :
i1 = i + n1 →
i2 = i1 + n2 →
n1 ≤ length vs →
n1 + n2 ≤ length vs →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz i dq (take n1 vs) ∗
chunk۰cslice l sz i1 dq (take n2 $ drop n1 vs) ∗
chunk۰cslice l sz i2 dq (drop (n1 + n2) vs).
Lemma chunk۰csliceｰcons l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk۰cslice l sz ˖i dq vs ⊣⊢
chunk۰cslice l sz i dq (v :: vs).
Lemma chunk۰csliceｰcons₁ l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz ˖i dq vs -∗
chunk۰cslice l sz i dq (v :: vs).
Lemma chunk۰csliceｰcons₂ l sz i dq v vs :
chunk۰cslice l sz i dq (v :: vs) ⊢
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk۰cslice l sz ˖i dq vs.
Lemma chunk۰csliceｰupdate {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v ∗
( ∀ w,
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} w -∗
chunk۰cslice l sz i dq (<[k := w]> vs)
).
Lemma chunk۰csliceｰlookupｰacc {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v ∗
( (l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz i dq vs
).
Lemma chunk۰csliceｰlookup {l sz i dq vs} k v :
vs !! k = Some v →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ ⁺(i + k) `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰupdate' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v ∗
( ∀ w,
(l +ₗ j `mod` sz) ↦{dq} w -∗
chunk۰cslice l sz i dq (<[k := w]> vs)
).
Lemma chunk۰csliceｰlookupｰacc' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v ∗
( (l +ₗ j `mod` sz) ↦{dq} v -∗
chunk۰cslice l sz i dq vs
).
Lemma chunk۰csliceｰlookup' {l sz i dq vs} j k v :
(i ≤ j)%Z →
vs !! k = Some v →
k = ₊j - i →
chunk۰cslice l sz i dq vs ⊢
(l +ₗ j `mod` sz) ↦{dq} v.
Lemma chunk۰csliceｰshift l sz i dq vs :
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + sz) dq vs.
Lemma chunk۰csliceｰshiftｰright l sz i dq vs :
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + sz) dq vs.
Lemma chunk۰csliceｰshiftｰleft l sz i dq vs :
sz ≤ i →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i - sz) dq vs.
Lemma chunk۰csliceｰmod l sz i dq vs :
0 < sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i `mod` sz) dq vs.
#[local] Lemma chunk۰csliceｰtoｰmodelｰaux l sz i dq vs :
0 < sz →
i + length vs ≤ sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model (l +ₗ i) dq vs.
Lemma chunk۰csliceｰtoｰmodel l sz i dq vs :
0 < sz →
length vs ≤ sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model (l +ₗ ⁺(i `mod` sz)) dq (take (sz - i `mod` sz) vs) ∗
chunk۰model l dq (drop (sz - i `mod` sz) vs).
Lemma chunk۰csliceｰtoｰmodelｰfull l sz i dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰model l dq (rotation (sz - i `mod` sz) vs).
#[local] Lemma chunk۰csliceｰrotationｰrightｰaux {l sz} i1 i2 dq vs :
0 < sz →
length vs = sz →
i1 `mod` sz ≤ i2 `mod` sz →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (i2 `mod` sz - i1 `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright {l sz i dq vs} n :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz (i + n) dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright₁ {l sz i dq vs} n :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊢
chunk۰cslice l sz (i + n) dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰrightｰ0 {l sz dq vs} i :
0 < sz →
length vs = sz →
chunk۰cslice l sz 0 dq vs ⊣⊢
chunk۰cslice l sz i dq (rotation (i `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i2 = i1 + n →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰright₁' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i2 = i1 + n →
chunk۰cslice l sz i1 dq vs ⊢
chunk۰cslice l sz i2 dq (rotation (n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft l sz i n dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz (i + n) dq vs ⊣⊢
chunk۰cslice l sz i dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft₁ l sz i n dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz (i + n) dq vs ⊢
chunk۰cslice l sz i dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleftｰ0 l sz i dq vs :
0 < sz →
length vs = sz →
chunk۰cslice l sz i dq vs ⊣⊢
chunk۰cslice l sz 0 dq (rotation (sz - i `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i1 = i2 + n →
chunk۰cslice l sz i1 dq vs ⊣⊢
chunk۰cslice l sz i2 dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrotationｰleft₁' {l sz i1 dq vs} i2 n :
0 < sz →
length vs = sz →
i1 = i2 + n →
chunk۰cslice l sz i1 dq vs ⊢
chunk۰cslice l sz i2 dq (rotation (sz - n `mod` sz) vs).
Lemma chunk۰csliceｰrebase {l sz i1 dq vs1} i2 :
0 < sz →
length vs1 = sz →
chunk۰cslice l sz i1 dq vs1 ⊢
∃ vs2 n,
⌜vs2 = rotation n vs1⌝ ∗
chunk۰cslice l sz i2 dq vs2 ∗
( chunk۰cslice l sz i2 dq vs2 -∗
chunk۰cslice l sz i1 dq vs1
).
Lemma chunk۰csliceｰvalid l sz i dq vs :
0 < length vs →
chunk۰cslice l sz i dq vs ⊢
⌜✓ dq⌝.
Lemma chunk۰csliceｰcombine l sz i dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜vs1 = vs2⌝ ∗
chunk۰cslice l sz i (dq1 ⋅ dq2) vs1.
Lemma chunk۰csliceｰvalidｰ2 l sz i dq1 vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜✓ (dq1 ⋅ dq2)⌝ ∗
⌜vs1 = vs2⌝.
Lemma chunk۰csliceｰagree l sz i dq1 vs1 dq2 vs2 :
length vs1 = length vs2 →
chunk۰cslice l sz i dq1 vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
⌜vs1 = vs2⌝.
Lemma chunk۰csliceｰdfracｰne l sz i1 dq1 vs1 i2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
¬ ✓ (dq1 ⋅ dq2) →
chunk۰cslice l sz i1 dq1 vs1 -∗
chunk۰cslice l sz i2 dq2 vs2 -∗
⌜i1 ≠ i2⌝.
Lemma chunk۰csliceｰne l sz i1 vs1 i2 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i1 (DfracOwn 1) vs1 -∗
chunk۰cslice l sz i2 dq2 vs2 -∗
⌜i1 ≠ i2⌝.
Lemma chunk۰csliceｰexclusive l sz i vs1 dq2 vs2 :
0 < length vs1 →
length vs1 = length vs2 →
chunk۰cslice l sz i (DfracOwn 1) vs1 -∗
chunk۰cslice l sz i dq2 vs2 -∗
False.
Lemma chunk۰csliceｰpersist l sz i dq vs :
chunk۰cslice l sz i dq vs ⊢ |==>
chunk۰cslice l sz i DfracDiscarded vs.
Lemma chunk۰csliceｰlength l sz i vs :
0 < sz →
chunk۰cslice l sz i (DfracOwn 1) vs ⊢
⌜length vs ≤ sz⌝.
End chunk۰cslice.
Section itype۰chunk.
Definition itype۰chunk τ `{!iType _ τ} sz l : iProp Σ :=
inv nroot (
∃ vs,
⌜sz = length vs⌝ ∗
chunk۰model l (DfracOwn 1) vs ∗
[∗ list] v ∈ vs, τ v
).
#[global] Instance itype۰chunkｰpersistent τ `{!iType _ τ} sz l :
Persistent (itype۰chunk τ sz l).
Lemma itype۰chunkｰ0 τ `{!iType _ τ} l :
⊢ |={⊤}=>
itype۰chunk τ 0 l.
Lemma itype۰chunkｰshift (i : Z) τ `{!iType _ τ} (sz : nat) l :
(0 ≤ i ≤ sz)%Z →
itype۰chunk τ sz l ⊢
itype۰chunk τ (sz - ₊i) (l +ₗ i).
Lemma itype۰chunkｰle sz' τ `{!iType _ τ} sz l :
(sz' ≤ sz) →
itype۰chunk τ sz l ⊢
itype۰chunk τ sz' l.
End itype۰chunk.
End zoo۰G.
#[global] Opaque chunk۰model.
#[global] Opaque chunk۰span.
#[global] Opaque chunk۰cslice.