Skip to content
Snippets Groups Projects
Commit e7af3dc7 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Product types.

parent f2612510
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
lifetime.v
+ 51
− 5
View file @ e7af3dc7
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Export viewshifts pviewshifts.
From iris.program_logic Require Import invariants namespaces thread_local.
From iris.prelude Require Import strings.
......@@ -60,12 +61,25 @@ Section lft.
Axiom lft_incl_persistent : ∀ κ κ', PersistentP (κ ⊑ κ').
Global Existing Instance lft_incl_persistent.
Axiom lft_extract_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_extract κ).
Global Existing Instance lft_extract_proper.
Axiom lft_borrow_proper : ∀ κ, Proper ((⊣⊢) ==> (⊣⊢)) (lft_borrow κ).
Global Existing Instance lft_borrow_proper.
Axiom lft_open_borrow_proper :
∀ κ q, Proper ((⊣⊢) ==> (⊣⊢)) (lft_open_borrow κ q).
Global Existing Instance lft_open_borrow_proper.
Axiom lft_frac_borrow_persistent : ∀ κ P, PersistentP (lft_frac_borrow κ P).
Global Existing Instance lft_frac_borrow_persistent.
Axiom lft_pers_borrow_persistent :
∀ κ i P, PersistentP (lft_pers_borrow κ i P).
Global Existing Instance lft_pers_borrow_persistent.
Axiom lft_pers_borrow_proper :
∀ κ i, Proper ((⊣⊢) ==> (⊣⊢)) (lft_pers_borrow κ i).
Global Existing Instance lft_pers_borrow_proper.
Axiom lft_pers_borrow_own_timeless :
∀ i κ, TimelessP (lft_pers_borrow_own i κ).
......@@ -92,7 +106,7 @@ Section lft.
▷ P ★ lft_open_borrow κ q P ={E}=> &{κ}P ★ [κ]{q}.
Axiom lft_open_borrow_contravar :
∀ `(nclose lftN ⊆ E) κ P Q q,
▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P) ★ lft_open_borrow κ q P
lft_open_borrow κ q P ★ ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P)
={E}=> lft_open_borrow κ q Q.
Axiom lft_reborrow :
∀ `(nclose lftN ⊆ E) κ κ' P, κ' ⊑ κ ⊢ &{κ}P ={E}=> &{κ'}P ★ κ' ∋ &{κ}P.
......@@ -139,6 +153,13 @@ Section lft.
(*** Derived lemmas *)
Lemma lft_own_split κ q : [κ]{q} ⊣⊢ ([κ]{q/2} ★ [κ]{q/2}).
Proof. by rewrite lft_own_op Qp_div_2. Qed.
Global Instance into_and_lft_own κ q :
IntoAnd false ([κ]{q}) ([κ]{q/2}) ([κ]{q/2}).
Proof. by rewrite /IntoAnd lft_own_split. Qed.
Lemma lft_borrow_open' E κ P q :
nclose lftN ⊆ E →
&{κ}P ★ [κ]{q} ={E}=> ▷ P ★ (▷ P ={E}=★ &{κ}P ★ [κ]{q}).
......@@ -157,6 +178,24 @@ Section lft.
iFrame. by iApply (lft_mkincl with "Hκ [-]").
Qed.
Lemma lft_borrow_close_stronger `(nclose lftN ⊆ E) κ P Q q :
▷ Q ★ lft_open_borrow κ q P ★ ▷ (▷Q ={⊤ ∖ nclose lftN}=★ ▷P)
={E}=> &{κ}Q ★ [κ]{q}.
Proof.
iIntros "[HP Hvsob]".
iVs (lft_open_borrow_contravar with "Hvsob"). set_solver.
iApply (lft_borrow_close with "[-]"). set_solver. by iSplitL "HP".
Qed.
Lemma lft_borrow_big_sepL_split `(nclose lftN ⊆ E) {A} κ Φ (l : list A) :
&{κ}([★ list] k↦y ∈ l, Φ k y) ={E}=> [★ list] k↦y ∈ l, &{κ}(Φ k y).
Proof.
revert Φ. induction l=>Φ; iIntros. by rewrite !big_sepL_nil.
rewrite !big_sepL_cons.
iVs (lft_borrow_split with "[-]") as "[??]"; try done.
iFrame. by iVs (IHl with "[-]").
Qed.
End lft.
(*** Derived notions *)
......@@ -174,8 +213,10 @@ Section shared_borrows.
Context `{irisG Λ Σ, lifetimeG Σ}
(κ : lifetime) (N : namespace) (P : iProp Σ).
Instance lft_shr_borrow_persistent :
PersistentP (&shr{κ | N} P) := _.
Global Instance lft_shr_borrow_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (lft_shr_borrow κ N).
Proof. solve_proper. Qed.
Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ | N} P) := _.
Lemma lft_borrow_share E :
lftN ⊥ N → &{κ}P ={E}=> &shr{κ|N}P.
......@@ -229,8 +270,13 @@ Section tl_borrows.
Context `{irisG Λ Σ, lifetimeG Σ, thread_localG Σ}
(κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ).
Instance lft_tl_borrow_persistent :
PersistentP (&tl{κ|tid|N} P) := _.
Global Instance lft_tl_borrow_persistent : PersistentP (&tl{κ|tid|N} P) := _.
Global Instance lft_tl_borrow_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (lft_tl_borrow κ tid N).
Proof.
intros P1 P2 EQ. apply uPred.exist_proper. intros κ'.
apply uPred.exist_proper. intros i. by rewrite EQ.
Qed.
Lemma lft_borrow_share_tl E :
lftN ⊥ N → &{κ}P ={E}=> &tl{κ|tid|N}P.
......
types.v
+ 265
− 70
View file @ e7af3dc7
From Coq Require Import Qcanon.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import thread_local.
From lrust Require Export notation.
From lrust Require Import lifetime heap.
Definition mgmtE := nclose tlN ∪ lftN.
Definition lrustN := nroot .@ "lrust".
Section defs.
......@@ -11,25 +14,32 @@ Section defs.
Record type :=
{ ty_size : nat; ty_dup : bool;
ty_own : thread_id → list val → iProp Σ;
ty_shr : lifetime → thread_id → coPset → loc → iProp Σ;
(* TODO : the document says ty_shr takes a mask, but it is never
used with anything else than namespaces. *)
ty_shr : lifetime → thread_id → namespace → loc → iProp Σ;
ty_shr_persistent κ tid N l : PersistentP (ty_shr κ tid N l);
ty_size_eq tid vl : ty_own tid vl ⊢ length vl = ty_size;
ty_dup_dup tid vl : ty_dup → ty_own tid vl ⊢ ty_own tid vl ★ ty_own tid vl;
(* The mask for starting the sharing does /not/ include the
namespace N, because sharing can be triggered in a context
where N is open. This should not be harmful, since sharing
typically creates invariants, which does not need the mask. *)
ty_share E N κ l tid q : nclose N ⊥ mgmtE → mgmtE ⊆ E →
namespace N, for allowing more flexibility for the user of
this type (typically for the [own] type). AFAIK, there is no
fundamental reason for this.
This should not be harmful, since sharing typically creates
invariants, which does not need the mask. Moreover, it is
more consistent with thread-local tokens, which we do not
give any. *)
ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
&{κ} (l ↦★: ty_own tid) ★ [κ]{q} ={E}=> ty_shr κ tid N l ★ [κ]{q};
ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
κ' ⊑ κ ⊢ ty_shr κ tid E l → ty_shr κ' tid E' l;
ty_shr_acc κ tid E E' l q :
E ⊆ E' → mgmtE ⊆ E' → ty_dup →
ty_shr κ tid E l ⊢
[κ]{q} ★ tl_own tid E ={E'}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
(▷l ↦★{q'}: ty_own tid ={E'}=★ [κ]{q} ★ tl_own tid E)
ty_shr_mono κ κ' tid N l :
κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
ty_shr_acc κ tid N E l q :
nclose N ⊆ E → mgmtE ⊆ E → ty_dup →
ty_shr κ tid N l ⊢
[κ]{q} ★ tl_own tid N ={E}=> ∃ q', ▷l ↦★{q'}: ty_own tid ★
(▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
}.
Global Existing Instance ty_shr_persistent.
......@@ -58,10 +68,10 @@ Section defs.
iVs (lft_borrow_fracture with "[Hmt]"); last by iFrame. done.
Qed.
Next Obligation.
iIntros (st κ κ' tid E E' l _) "#Hord". by iApply lft_frac_borrow_incl.
iIntros (st κ κ' tid N l) "#Hord". by iApply lft_frac_borrow_incl.
Qed.
Next Obligation.
intros st κ tid E E' l q ???. iIntros "#Hshr!#[Hlft Htlown]".
intros st κ tid N E l q ???. iIntros "#Hshr!#[Hlft Htlown]".
iVs (lft_frac_borrow_open with "[] Hlft"); first set_solver; last by iFrame.
iSplit; last done. iIntros "!#". iIntros (q1 q2). iSplit; iIntros "H".
- iDestruct "H" as (vl) "[Hq1q2 Hown]".
......@@ -86,28 +96,28 @@ Section types.
Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
Program Definition bot : type :=
Program Definition bot :=
ty_of_st {| st_size := 1; st_dup := true;
st_own tid vl := False%I
|}.
Next Obligation. iIntros (tid vl) "[]". Qed.
Next Obligation. iIntros (tid vl _) "[]". Qed.
Program Definition unit : type :=
Program Definition unit :=
ty_of_st {| st_size := 0; st_dup := true;
st_own tid vl := (vl = [])%I
|}.
Next Obligation. iIntros (tid vl) "%". by subst. Qed.
Next Obligation. iIntros (tid vl _) "%". auto. Qed.
Program Definition bool : type :=
Program Definition bool :=
ty_of_st {| st_size := 1; st_dup := true;
st_own tid vl := (∃ z:bool, vl = [ #z ])%I
|}.
Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
Next Obligation. iIntros (tid vl _) "H". auto. Qed.
Program Definition int : type :=
Program Definition int :=
ty_of_st {| st_size := 1; st_dup := true;
st_own tid vl := (∃ z:Z, vl = [ #z ])%I
|}.
......@@ -116,14 +126,14 @@ Section types.
(* TODO own and uniq_borrow are very similar. They could probably
somehow share some bits.. *)
Program Definition own (q:Qp) (ty:type) :=
Program Definition own (q : Qp) (ty : type) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl :=
(∃ l:loc, vl = [ #l ] ★ †{q}l…ty.(ty_size)
★ ▷ l ↦★: ty.(ty_own) tid)%I;
ty_shr κ tid E l :=
ty_shr κ tid N l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
∀ q', □ ([κ]{q'} →|={E ∪ mgmtE, mgmtE}▷=> ty.(ty_shr) κ tid E l' ★ [κ]{q'}))%I
∀ q', □ ([κ]{q'} →|={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
......@@ -133,46 +143,38 @@ Section types.
intros q ty E N κ l tid q' ?? =>/=. iIntros "[Hshr Hq']".
iVs (lft_borrow_open with "[Hshr Hq']") as "[Hown Hob]". set_solver. by iFrame.
iDestruct "Hown" as (vl) "[Hmt Hvl]". iDestruct "Hvl" as (l') "(>%&Hf&Hown)". subst.
iVs (lft_open_borrow_contravar with "[Hob Hf]") as "Hob". set_solver.
{ iSplitR "Hob"; last done. iIntros "!>[Hmt1 Hmt2]!==>!>". iExists [ #l' ].
rewrite heap_mapsto_vec_singleton. iSplitL "Hmt1"; first done.
iExists _. iSplit; [|by iSplitR "Hmt2"]. done. }
iVs (lft_borrow_close with "[Hmt Hown Hob]") as "[Hb Htok]". set_solver.
{ rewrite heap_mapsto_vec_singleton. iSplitR "Hob"; last done.
by iIntros "!>{$Hmt$Hown}". }
iCombine "Hown" "Hmt" as "Hown". rewrite heap_mapsto_vec_singleton.
iVs (lft_borrow_close_stronger with "[-]") as "[Hb Htok]". set_solver.
{ iIntros "{$Hown $Hob}!>[Hmt1 Hmt2]!==>!>". iExists [ #l'].
rewrite heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame. }
iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
rewrite lft_borrow_persist.
iDestruct "Hb2" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb2") as "Hbf".
rewrite lft_borrow_persist. iDestruct "Hb1" as (κ0 i) "(#Hord&#Hpb&Hpbown)".
iVs (inv_alloc N _ (lft_pers_borrow_own i κ0 ∨ ty_shr ty κ tid N l')%I
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!==>{$Htok}". iExists l'. iFrame. iIntros (q'') "!#Htok".
iVs (inv_open with "Hinv") as "[[>Hbtok|#Hshr] Hclose]". set_solver.
- replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
iVs (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. eauto. }
iVs (lft_borrow_open with "[Hb Htok]") as "[Hown Hob]". set_solver. by iFrame.
iVs (lft_open_borrow_contravar with "[Hob]") as "Hob". set_solver.
{ iSplitR "Hob"; last done. instantiate (1:=(l' ↦★: ty_own ty tid)%I). eauto 10. }
iIntros "!==>!>".
iVs (lft_borrow_close with "[Hown Hob]") as "[Hb Htok]". set_solver.
by iFrame "Hown".
iVs (ty.(ty_share) with "[Hb Htok]") as "[#Hshr Htok]"; try done. by iFrame.
iVs (lft_borrow_close_stronger with "[Hown Hob]") as "Hbtok". set_solver.
{ iFrame "Hown Hob". eauto 10. }
iVs (ty.(ty_share) with "Hbtok") as "[#Hshr Htok]"; try done.
iVs ("Hclose" with "[]") as "_"; by eauto.
- replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
iIntros "!==>!>". iVs ("Hclose" with "[]") as "_"; by eauto.
- iIntros "!==>!>". iVs ("Hclose" with "[]") as "_"; by eauto.
Qed.
Next Obligation.
intros _ ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iExists l'.
iSplit. by iApply (lft_frac_borrow_incl with "[]").
iIntros (_ ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
iIntros (q') "!#Htok".
iVs (lft_incl_trade with "Hκ Htok") as (q'') "[Htok Hclose]". set_solver.
iApply (pvs_trans _ (E ∪ mgmtE)). iApply pvs_intro'. set_solver.
iIntros "Hclose'". iVs ("Hvs" $! q'' with "Htok") as "Hvs'".
iIntros "!==>!>". iVs "Hvs'" as "[Hshr Htok]". iVs "Hclose'".
iVs ("Hvs" $! q'' with "Htok") as "Hvs'".
iIntros "!==>!>". iVs "Hvs'" as "[Hshr Htok]".
iVs ("Hclose" with "Htok"). iFrame.
iApply (ty.(ty_shr_mono) with "Hκ"); last done. done.
by iApply (ty.(ty_shr_mono) with "Hκ").
Qed.
Next Obligation. done. Qed.
......@@ -180,10 +182,10 @@ Section types.
{| ty_size := 1; ty_dup := false;
ty_own tid vl :=
(∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
ty_shr κ' tid E l :=
ty_shr κ' tid N l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'} →
|={E ∪ mgmtE, mgmtE}▷=> ty.(ty_shr) κ'' tid E l' ★ [κ'']{q'}))%I
|={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
......@@ -193,13 +195,10 @@ Section types.
intros κ ty E N κ' l tid q' ?? =>/=. iIntros "[Hshr Hq']".
iVs (lft_borrow_open with "[Hshr Hq']") as "[Hown Hob]". set_solver. by iFrame.
iDestruct "Hown" as (vl) "[Hmt Hvl]". iDestruct "Hvl" as (l') "(>%&Hown)". subst.
iVs (lft_open_borrow_contravar with "[Hob]") as "Hob". set_solver.
{ iSplitR "Hob"; last done. iIntros "!>[Hmt1 Hmt2]!==>!>". iExists [ #l' ].
rewrite heap_mapsto_vec_singleton. iSplitL "Hmt1"; first done.
iExists _. by iSplitR "Hmt2". }
iVs (lft_borrow_close with "[Hmt Hown Hob]") as "[Hb Htok]". set_solver.
{ rewrite heap_mapsto_vec_singleton. iSplitR "Hob"; last done.
by iIntros "!>{$Hmt$Hown}". }
iCombine "Hmt" "Hown" as "Hown". rewrite heap_mapsto_vec_singleton.
iVs (lft_borrow_close_stronger with "[-]") as "[Hb Htok]". set_solver.
{ iIntros "{$Hown $Hob}!>[Hmt1 Hmt2]!==>!>". iExists [ #l'].
rewrite heap_mapsto_vec_singleton. iFrame. iExists _. by iFrame. }
iVs (lft_borrow_split with "Hb") as "[Hb1 Hb2]". set_solver.
iVs (lft_borrow_fracture _ _ (λ q, l ↦{q} #l')%I with "Hb1") as "Hbf".
rewrite lft_borrow_persist.
......@@ -208,9 +207,10 @@ Section types.
with "[Hpbown]") as "#Hinv"; first by eauto.
iIntros "!==>{$Htok}". iExists l'. iFrame.
iIntros (q'' κ'') "!#(#Hκ''κ & #Hκ''κ' & Htok)".
iVs (inv_open with "Hinv") as "[[>Hbtok|#Hshr] Hclose]". set_solver.
- replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
iVs (inv_open with "Hinv") as "[INV Hclose]". set_solver.
replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
iDestruct "INV" as "[>Hbtok|#Hshr]".
- iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
{ iApply lft_borrow_persist. iExists κ0, i. iFrame "★ #".
iApply lft_incl_trans. eauto. }
iVs (lft_borrow_open with "[Hb Htok]") as "[Hown Hob]". set_solver. by iFrame.
......@@ -226,26 +226,221 @@ Section types.
need a lifetime that would be the union of κ and κ'. *)
admit.
by eauto.
- replace ((nclose N ∪ mgmtE) ∖ N) with mgmtE by set_solver.
iIntros "!==>!>". iVs ("Hclose" with "[]") as "_". by eauto.
- iIntros "!==>!>". iVs ("Hclose" with "[]") as "_". by eauto.
iIntros "!==>{$Htok}". by iApply (ty.(ty_shr_mono) with "Hκ''κ'").
Admitted.
Next Obligation.
intros κ0 ty κ κ' tid E E' l ?. iIntros "#Hκ #H".
iDestruct "H" as (l') "[Hfb Hvs]". iExists l'.
iSplit. by iApply (lft_frac_borrow_incl with "[]").
iIntros (κ0 ty κ κ' tid N l) "#Hκ #H". iDestruct "H" as (l') "[Hfb Hvs]".
iExists l'. iSplit. by iApply (lft_frac_borrow_incl with "[]").
iIntros (q' κ'') "!#(#Hκ0 & #Hκ' & Htok)".
iApply (pvs_trans _ (E ∪ mgmtE)). iApply pvs_intro'. set_solver.
iIntros "Hclose'". iVs ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
iVs ("Hvs" $! q' κ'' with "[Htok]") as "Hclose".
{ iFrame. iSplit. done. iApply lft_incl_trans. eauto. }
iIntros "!==>!>". iVs "Hclose" as "[Hshr Htok]". iVs "Hclose'".
iIntros "!==>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr"). done.
iIntros "!==>!>". iVs "Hclose" as "[Hshr Htok]".
iIntros "!==>{$Htok}". iApply (ty.(ty_shr_mono) with "[] Hshr").
iApply lft_incl_refl.
Qed.
Next Obligation. done. Qed.
Program Definition shared_borrow (κ : lifetime) (ty : type) :=
ty_of_st {| st_size := 1; st_dup := true;
st_own tid vl := (∃ l:loc, vl = [ #l ] ★ ty.(ty_shr) κ tid lrustN l)%I
|}.
Next Obligation.
iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
Qed.
Next Obligation. iIntros (κ ty tid vl _) "H". auto. Qed.
Fixpoint combine_accu_size (tyl : list type) (accu : nat) :=
match tyl with
| [] => []
| ty :: q => (ty, accu) :: combine_accu_size q (accu + ty.(ty_size))
end.
Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
length tyl = length vll →
([★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
⊢ length (concat vll) = sum_list_with ty_size tyl.
Proof.
revert vll; induction tyl as [|ty tyq IH]; destruct vll;
iIntros (EQ) "Hown"; try done.
rewrite big_sepL_cons app_length /=. iDestruct "Hown" as "[Hown Hownq]".
iDestruct (ty.(ty_size_eq) with "Hown") as %->.
iDestruct (IH with "[-]") as %->; auto.
Qed.
Fixpoint nat_rec_shift {A : Type} (x : A) (f : nat → A → A) (n0 n : nat) :=
match n with
| O => x
| S n => f n0 (nat_rec_shift x f (S n0) n)
end.
Lemma split_prod_namespace tid (N : namespace) n :
∃ E, (tl_own tid N ⊣⊢ tl_own tid E
★ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ★ P) 0%nat n)
∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat.
Proof.
generalize 0%nat. induction n as [|n IH].
- eexists. split. by rewrite right_id. intros. apply nclose_subseteq.
- intros i. destruct (IH (S i)) as [E [IH1 IH2]].
eexists (E ∖ (N .@ i))%I. split.
+ simpl. rewrite IH1 assoc -tl_own_union; last set_solver.
f_equiv; last done. f_equiv. rewrite (comm union).
apply union_difference_L. apply IH2. lia.
+ intros. assert (i0 ≠ i)%nat by lia. solve_ndisj.
Qed.
Program Definition product (tyl : list type) :=
{| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl;
ty_own tid vl :=
(∃ vll, vl = concat vll ★ length tyl = length vll ★
[★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
ty_shr κ tid N l :=
([★ list] i ↦ tyoffs ∈ combine_accu_size tyl 0,
tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
|}.
Next Obligation.
iIntros (tyl tid vl) "Hown". iDestruct "Hown" as (vll) "(%&%&Hown)".
subst. by iApply (list_ty_type_eq with "Hown").
Qed.
Next Obligation.
induction tyl as [|ty tyq IH]; iIntros (tid vl Hfa) "H";
iDestruct "H" as ([|vl0 vlq]) "(%&#Hlen&Hown)"; subst vl;
iDestruct "Hlen" as %Hlen; inversion Hlen; simpl in *.
- iSplit; iExists []; by repeat iSplit.
- apply andb_prop_elim in Hfa. destruct Hfa as [Hfah Hfaq].
iDestruct (big_sepL_cons with "Hown") as "[Hh Hq]".
iDestruct (ty_dup_dup with "Hh") as "[Hh1 Hh2]". done.
iDestruct (IH tid (concat vlq) Hfaq with "[Hq]") as "[Hq1 Hq2]". by eauto.
iSplitL "Hh1 Hq1".
+ iDestruct "Hq1" as (vllq) "(%&%&?)". iExists (vl0::vllq).
rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
+ iDestruct "Hq2" as (vllq) "(%&%&?)". iExists (vl0::vllq).
rewrite big_sepL_cons/=. iFrame. iSplit; iPureIntro; congruence.
Qed.
Next Obligation.
intros tyl E N κ l tid q ??. iIntros "[Hown Htok]".
match goal with
| |- context [(&{κ}(?P))%I] =>
assert (P ⊣⊢ [★ list] i↦tyoffs ∈ combine_accu_size tyl 0,
(shift_loc l (tyoffs.2)) ↦★: ty_own (tyoffs.1) tid) as ->
end.
{ rewrite -{1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0).
generalize 0%nat. induction tyl as [|ty tyl IH]=>/= offs.
- iSplit; iIntros "_". by iApply big_sepL_nil.
iExists []. iSplit. by iApply heap_mapsto_vec_nil.
iExists []. repeat iSplit; try done. by iApply big_sepL_nil.
- rewrite big_sepL_cons -IH. iSplit.
+ iIntros "H". iDestruct "H" as (vl) "[Hmt H]".
iDestruct "H" as ([|vl0 vll]) "(%&Hlen&Hown)";
iDestruct "Hlen" as %Hlen; inversion Hlen; subst.
rewrite big_sepL_cons heap_mapsto_vec_app/=.
iDestruct "Hmt" as "[Hmth Hmtq]"; iDestruct "Hown" as "[Hownh Hownq]".
iDestruct (ty.(ty_size_eq) with "#Hownh") as %->.
iSplitL "Hmth Hownh". iExists vl0. by iFrame.
iExists (concat vll). iSplitL "Hmtq"; last by eauto.
by rewrite shift_loc_assoc Nat2Z.inj_add.
+ iIntros "[Hmth H]". iDestruct "H" as (vl) "[Hmtq H]".
iDestruct "H" as (vll) "(%&Hlen&Hownq)". subst.
iDestruct "Hmth" as (vlh) "[Hmth Hownh]". iDestruct "Hlen" as %->.
iExists (vlh ++ concat vll).
rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add.
iDestruct (ty.(ty_size_eq) with "#Hownh") as %->. iFrame.
iExists (vlh :: vll). rewrite big_sepL_cons. iFrame. auto. }
iVs (lft_borrow_big_sepL_split with "Hown") as "Hown". set_solver.
(* FIXME : revert the (empty) proofmode context in the induction hypothesis. *)
iRevert "Htok Hown".
change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat). generalize O at 3.
induction (combine_accu_size tyl 0) as [|[ty offs] ll IH].
- iIntros (?) "$ _ !==>". by rewrite big_sepL_nil.
- iIntros (i) "Htoks Hown". iDestruct (big_sepL_cons with "Hown") as "[Hownh Hownq]".
iVs (IH (S i)%nat with "[] Htoks Hownq") as "[#Hshrq Htoks]". done.
iVs (ty.(ty_share) _ (N .@ (i+0)%nat) with "[Hownh Htoks]") as "[#Hshrh $]".
solve_ndisj. done. by iFrame.
iVsIntro. rewrite big_sepL_cons. iFrame "#".
iApply big_sepL_mono; last done. intros. by rewrite /= Nat.add_succ_r.
Qed.
Next Obligation.
iIntros (tyl κ κ' tid N l) "#Hκ #H". iApply big_sepL_impl.
iSplit; last done. iIntros "!#*/=_#H'". by iApply (ty_shr_mono with "Hκ").
Qed.
Next Obligation.
intros tyl κ tid N E l q ?? DUP. simpl.
rewrite -{-1}(shift_loc_0 l). change 0%Z with (Z.of_nat 0). generalize 0%nat.
change (ndot (A:=nat)) with (λ N i, N .@ (0+i)%nat).
destruct (split_prod_namespace tid N (length tyl)) as [Ef [EQ _]].
setoid_rewrite ->EQ. clear EQ. generalize 0%nat.
revert q. induction tyl as [|tyh tyq IH].
- iIntros (q i offs) "_!#$!==>". iExists 1%Qp. iSplitR; last by eauto.
iNext. iExists []. rewrite heap_mapsto_vec_nil. iSplit; first done.
simpl. iExists []. rewrite big_sepL_nil. eauto.
- simpl in DUP. destruct (andb_prop_elim _ _ DUP) as [DUPh DUPq]. simpl.
iIntros (q i offs) "#Hshr!#([Htokh Htokq]&Htlf&Htlh&Htlq)".
rewrite big_sepL_cons Nat.add_0_r.
iDestruct "Hshr" as "[Hshrh Hshrq]". setoid_rewrite <-Nat.add_succ_comm.
iVs (IH with "Hshrq [Htokq Htlf Htlq]") as (q'q) "[Hownq Hcloseq]". done. by iFrame.
iDestruct "Hownq" as (vlq) "[Hmtq Hownq]".
iDestruct "Hownq" as (vllq) "(>%&>%&Hownq)". subst vlq.
iDestruct (uPred.later_mono _ (_ = _) with "#Hownq") as ">Hlenvlq".
by apply list_ty_type_eq.
iDestruct "Hlenvlq" as %Hlenvlq.
iVs (tyh.(ty_shr_acc) with "Hshrh [Htokh Htlh]") as (q'h) "[Hownh Hcloseh]"; try done.
by pose proof (nclose_subseteq N i); set_solver. by iFrame.
iDestruct "Hownh" as (vlh) "[Hmth Hownh]".
iDestruct (uPred.later_mono _ (_ = _) with "#Hownh") as ">Hlenvlh". apply ty_size_eq.
iDestruct "Hlenvlh" as %Hlenvlh.
(** TODO : extract and simplify this arithmetic proof. *)
assert (∃ q' q'0h q'0q, q'h = q' + q'0h ∧ q'q = q' + q'0q)%Qp
as (q' & q'0h & q'0q & -> & ->).
{ destruct (Qc_le_dec q'h q'q) as [LE0|LE0%Qclt_nge%Qclt_le_weak].
- destruct (q'q - q'h / 2)%Qp as [q'0q|] eqn:EQ; unfold Qp_minus in EQ;
destruct decide as [LT|LE%Qcnot_lt_le] in EQ; inversion EQ.
+ exists (q'h / 2)%Qp, (q'h / 2)%Qp, q'0q. split; apply Qp_eq.
by rewrite Qp_div_2. subst; simpl; ring.
+ apply (Qcplus_le_mono_r _ _ (-(q'h/2))%Qc) in LE0.
eapply Qcle_trans in LE; last apply LE0.
replace (q'h - q'h / 2)%Qc with (Qcmult q'h (1 - 1/2))%Qc in LE by ring.
replace 0%Qc with (Qcmult 0 (1-1/2)) in LE by ring.
by apply Qcmult_lt_0_le_reg_r, Qcle_not_lt in LE.
- destruct (q'h - q'q / 2)%Qp as [q'0h|] eqn:EQ; unfold Qp_minus in EQ;
destruct decide as [LT|LE%Qcnot_lt_le] in EQ; inversion EQ.
+ exists (q'q / 2)%Qp, q'0h, (q'q / 2)%Qp. split; apply Qp_eq.
subst; simpl; ring. by rewrite Qp_div_2.
+ apply (Qcplus_le_mono_r _ _ (-(q'q/2))%Qc) in LE0.
eapply Qcle_trans in LE; last apply LE0.
replace (q'q - q'q / 2)%Qc with (Qcmult q'q (1 - 1/2))%Qc in LE by ring.
replace 0%Qc with (Qcmult 0 (1-1/2)) in LE by ring.
by apply Qcmult_lt_0_le_reg_r, Qcle_not_lt in LE. }
iExists q'. iVsIntro. rewrite -!heap_mapsto_vec_op_eq.
iDestruct "Hmth" as "[Hmth0 Hmth1]". iDestruct "Hmtq" as "[Hmtq0 Hmtq1]".
iSplitR "Hcloseq Hcloseh Hmtq1 Hmth1".
+ iNext. iExists (vlh ++ concat vllq). iDestruct (ty_size_eq with "#Hownh") as %Hlenh.
iSplitL "Hmtq0 Hmth0".
rewrite heap_mapsto_vec_app shift_loc_assoc Nat2Z.inj_add Hlenh; by iFrame.
iExists (vlh::vllq). iSplit. done. iSplit. iPureIntro; simpl; congruence.
rewrite big_sepL_cons. by iFrame.
+ iIntros "H". iDestruct "H" as (vl) "[Hmt H]".
iDestruct "H" as ([|vllh' vllq']) "(>%&>%&Hown)". done. subst.
rewrite big_sepL_cons. iDestruct "Hown" as "[Hownh Hownq]".
iDestruct (uPred.later_mono _ (_ = _) with "#Hownq") as ">Hlenvlq'".
apply list_ty_type_eq; simpl in *; congruence.
iDestruct "Hlenvlq'" as %Hlenvlq'.
rewrite heap_mapsto_vec_app. iDestruct "Hmt" as "[Hmth0 Hmtq0]".
iCombine "Hmth0" "Hmth1" as "Hmth".
iDestruct (uPred.later_mono _ (_ = _) with "#Hownh") as ">Hlenvlh'".
apply ty_size_eq. iDestruct "Hlenvlh'" as %Hlenvlh'.
rewrite heap_mapsto_vec_op; last first. simpl in *; congruence.
iDestruct "Hmth" as "[>% Hmth]". subst.
iVs ("Hcloseh" with "[Hmth Hownh]") as "[Htokh $]".
{ iNext. iExists _. by iFrame. }
iCombine "Hmtq0" "Hmtq1" as "Hmtq".
rewrite shift_loc_assoc Hlenvlh Nat2Z.inj_add heap_mapsto_vec_op; last congruence.
iDestruct "Hmtq" as "[>% Hmtq]".
iVs ("Hcloseq" with "[-Htokh]") as "[Htokq $]".
{ iNext. iExists _. iFrame. iExists _. iFrame. iSplit. done.
simpl in *. iPureIntro. congruence. }
rewrite (lft_own_split _ q). by iFrame.
Qed.
End types.
End Types.
\ No newline at end of file
End Types.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment