Library zoo_std.chunk
From zoo Require Import
prelude.
From zoo.common Require Import
list
math.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base.
From zoo Require Import
options.
Implicit Types i n : nat.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types 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_1 l dq v :
l ↦{dq} v ⊢
chunk_model l dq [v].
Lemma chunk_model_singleton_2 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_1 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_2 {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_app3 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_app3_1 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_app3_2 {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_1 l dq v vs :
l ↦{dq} v -∗
chunk_model (l +ₗ 1) dq vs -∗
chunk_model l dq (v :: vs).
Lemma chunk_model_cons_2 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_1 l dq v :
l ↦{dq} v ⊢
chunk_span l dq 1.
Lemma chunk_span_singleton_2 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 (S n).
Lemma chunk_span_cons_1 l dq v n :
l ↦{dq} v -∗
chunk_span (l +ₗ 1) dq n -∗
chunk_span l dq (S n).
Lemma chunk_span_cons_2 l dq n :
chunk_span l dq (S 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 (S 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_1 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_2 {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_app3 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_app3_1 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_app3_2 {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 Types 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_1 l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊢
chunk_cslice l sz i dq [v].
Lemma chunk_cslice_singleton_2 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_1 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_2 {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_app3 {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 (S i) dq vs ⊣⊢
chunk_cslice l sz i dq (v :: vs).
Lemma chunk_cslice_cons_1 l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v -∗
chunk_cslice l sz (S i) dq vs -∗
chunk_cslice l sz i dq (v :: vs).
Lemma chunk_cslice_cons_2 l sz i dq v vs :
chunk_cslice l sz i dq (v :: vs) ⊢
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk_cslice l sz (S 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_1 {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_1' {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_1 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_1' {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.
prelude.
From zoo.common Require Import
list
math.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Export
base.
From zoo Require Import
options.
Implicit Types i n : nat.
Implicit Types l : location.
Implicit Types v : val.
Implicit Types 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_1 l dq v :
l ↦{dq} v ⊢
chunk_model l dq [v].
Lemma chunk_model_singleton_2 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_1 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_2 {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_app3 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_app3_1 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_app3_2 {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_1 l dq v vs :
l ↦{dq} v -∗
chunk_model (l +ₗ 1) dq vs -∗
chunk_model l dq (v :: vs).
Lemma chunk_model_cons_2 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_1 l dq v :
l ↦{dq} v ⊢
chunk_span l dq 1.
Lemma chunk_span_singleton_2 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 (S n).
Lemma chunk_span_cons_1 l dq v n :
l ↦{dq} v -∗
chunk_span (l +ₗ 1) dq n -∗
chunk_span l dq (S n).
Lemma chunk_span_cons_2 l dq n :
chunk_span l dq (S 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 (S 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_1 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_2 {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_app3 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_app3_1 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_app3_2 {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 Types 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_1 l sz i dq v :
(l +ₗ i `mod` sz) ↦{dq} v ⊢
chunk_cslice l sz i dq [v].
Lemma chunk_cslice_singleton_2 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_1 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_2 {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_app3 {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 (S i) dq vs ⊣⊢
chunk_cslice l sz i dq (v :: vs).
Lemma chunk_cslice_cons_1 l sz i dq v vs :
(l +ₗ i `mod` sz) ↦{dq} v -∗
chunk_cslice l sz (S i) dq vs -∗
chunk_cslice l sz i dq (v :: vs).
Lemma chunk_cslice_cons_2 l sz i dq v vs :
chunk_cslice l sz i dq (v :: vs) ⊢
(l +ₗ i `mod` sz) ↦{dq} v ∗
chunk_cslice l sz (S 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_1 {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_1' {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_1 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_1' {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.