From cd13e4ce4ccfa4b1be5f884bf91bb583234191f0 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Tue, 8 Nov 2016 20:14:35 +0100 Subject: [PATCH] Split lifetime.v in smaller files. --- _CoqProject | 3 + theories/frac_borrow.v | 120 ++++++++++++++++++++++ theories/lifetime.v | 222 +---------------------------------------- theories/perm.v | 6 +- theories/perm_incl.v | 4 +- theories/shr_borrow.v | 54 ++++++++++ theories/tl_borrow.v | 50 ++++++++++ theories/type.v | 37 ++++--- theories/type_incl.v | 2 +- theories/typing.v | 4 +- 10 files changed, 259 insertions(+), 243 deletions(-) create mode 100644 theories/frac_borrow.v create mode 100644 theories/shr_borrow.v create mode 100644 theories/tl_borrow.v diff --git a/_CoqProject b/_CoqProject index c4ae5b38..cd1cc58d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -12,6 +12,9 @@ theories/races.v theories/tactics.v theories/wp_tactics.v theories/lifetime.v +theories/tl_borrow.v +theories/shr_borrow.v +theories/frac_borrow.v theories/type.v theories/type_incl.v theories/perm.v diff --git a/theories/frac_borrow.v b/theories/frac_borrow.v new file mode 100644 index 00000000..fa85e2aa --- /dev/null +++ b/theories/frac_borrow.v @@ -0,0 +1,120 @@ +From Coq Require Import Qcanon. +From iris.proofmode Require Import tactics. +From iris.algebra Require Import frac. +From lrust Require Export lifetime shr_borrow. + +Class frac_borrowG Σ := frac_borrowG_inG :> inG Σ fracR. + +Definition frac_borrow `{invG Σ, lifetimeG Σ, frac_borrowG Σ} κ (Φ : Qp → iProp Σ) := + (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗ + (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I. +Notation "&frac{ κ } P" := (frac_borrow κ P) + (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope. + +Section frac_borrow. + + Context `{invG Σ, lifetimeG Σ, frac_borrowG Σ}. + + Global Instance frac_borrow_proper : + Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ). + Proof. solve_proper. Qed. + Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _. + + Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ: + &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ. + Proof. + iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done. + iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H†Hclose]]". done. + - iMod ("Hclose" with "*[-]") as "Hφ"; last first. + { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ"). + iApply lft_incl_refl. } + iSplitL. by iExists 1%Qp; iFrame; auto. + iIntros "!>[H†Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst. + iDestruct "Hκ" as (q'') "[_ Hκ]". + iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]". + - iMod ("Hclose" with "*") as "Hφ"; last first. + iExists γ, κ. iSplitR. by iApply lft_incl_refl. + iMod (borrow_fake with "H†"). done. by iApply borrow_share. + Qed. + + Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ: + &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, â–· φ q ∗ (â–· φ q ={E∖lftN,E}=∗ True)) + ∨ [†κ] ∗ |={E∖lftN,E}=> True. + Proof. + iIntros "#Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]". + iMod (shr_borrow_acc with "Hshr") as "[[Hφ Hclose]|[H†Hclose]]". done. + - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame. + iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame. + - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done. + iApply fupd_intro_mask. set_solver. done. + Qed. + + Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ: + â–¡ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢ + &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', â–· φ q' ∗ (â–· φ q' ={E}=∗ q.[κ]). + Proof. + iIntros "#Hφ Hfrac Hκ". unfold frac_borrow. + iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]". + iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done. + iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done. + iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)". + destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ). + iExists qq. + iAssert (â–· φ qq ∗ â–· φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]". + { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. } + rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'. + iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]". + iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1". + { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]". + - subst. iExists qq. iIntros "{$Hκq}!%". + by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2. + - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp. + rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%". + by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. } + clear Hqφ qφ qφ0. iIntros "!>Hqφ". + iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done. + iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])". + { subst. iCombine "Hown" "Hownq" as "Hown". + by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. } + iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown". + iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'. + assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-]. + { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'. + rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval. + destruct Hval as [Hval|Hval]. + by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. } + - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. } + iDestruct "Hq'κ" as "[Hq'qκ Hqκ]". + iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2". + { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame. + iRight. iExists _. iIntros "{$Hq'qκ}!%". + revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. } + iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame. + - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2". + { iNext. iExists (qφ â‹… qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. } + iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame. + Qed. + + Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ. + Proof. + iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame. + iApply lft_incl_trans. iFrame. + Qed. + + Lemma frac_borrow_incl κ κ' q: + &frac{κ}(λ q', (q * q').[κ']) ⊢ κ ⊑ κ'. + Proof. + iIntros "#Hbor!#". iSplitR. + - iIntros (q') "Hκ'". + iMod (frac_borrow_acc with "[] Hbor Hκ'") as (q'') "[>? Hclose]". done. + + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto. + + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto. + - iIntros "H†'". + iMod (frac_borrow_atomic_acc with "Hbor") as "[H|[$ $]]". done. + iDestruct "H" as (q') "[>Hκ' _]". + iDestruct (lft_own_dead with "[$H†' $Hκ']") as "[]". + Qed. + +End frac_borrow. + +Typeclasses Opaque frac_borrow. diff --git a/theories/lifetime.v b/theories/lifetime.v index f0a3d50b..2956516d 100644 --- a/theories/lifetime.v +++ b/theories/lifetime.v @@ -1,8 +1,6 @@ -From iris.algebra Require Import csum auth frac. +From iris.algebra Require Import csum auth frac gmap. From iris.base_logic.lib Require Export fancy_updates invariants namespaces. -From iris.base_logic.lib Require Import thread_local. From iris.proofmode Require Import tactics. -From Coq Require Import Qcanon. Definition lftN := nroot .@ "lft". @@ -19,7 +17,6 @@ Definition borrow_tokUR : ucmraT := Class lifetimeG Σ := LifetimeG { lft_tok_inG :> inG Σ lft_tokUR; borrow_tok_inG :> inG Σ borrow_tokUR; - frac_inG :> inG Σ fracR; lft_toks_name : gname; borrow_tok_name : gname }. @@ -347,220 +344,3 @@ Section incl. End incl. Typeclasses Opaque lft_incl. - -(*** Derived notions *) - -(** Shared borrows *) -Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) := - (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I. -Notation "&shr{ κ } P" := (shr_borrow κ P) - (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope. - -Section shared_borrows. - Context `{invG Σ, lifetimeG Σ} (P : iProp Σ). - - Global Instance shr_borrow_proper : - Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ). - Proof. solve_proper. Qed. - Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _. - - Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P. - Proof. - iIntros "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)". - iExists i. iFrame "#". iApply inv_alloc. auto. - Qed. - - Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ : - &shr{κ}P ={E,E∖lftN}=∗ â–·P ∗ (â–·P ={E∖lftN,E}=∗ True) ∨ - [†κ] ∗ |={E∖lftN,E}=> True. - Proof. - iIntros "#HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)". - iInv lftN as (q') ">Hq'" "Hclose". - rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op. - iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto. - iMod (idx_borrow_atomic_acc with "Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]". done. - - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP"). - - iRight. iFrame. iIntros "!>". by iMod "Hclose". - Qed. - - Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ : - &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ â–·P ∗ (â–·P ={E∖lftN,E}=∗ q.[κ]). - Proof. - iIntros "#Hshr Hκ". iMod (shr_borrow_acc with "Hshr") as "[[$ Hclose]|[H†_]]". done. - - iIntros "!>HP". by iMod ("Hclose" with "HP"). - - iDestruct (lft_own_dead with "[-]") as "[]". by iFrame. - Qed. - - Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P. - Proof. - iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame. - by iApply (idx_borrow_shorten with "H⊑"). - Qed. - -End shared_borrows. - -Typeclasses Opaque shr_borrow. - -(** Fractured borrows *) -Definition frac_borrow `{invG Σ, lifetimeG Σ} κ (Φ : Qp → iProp Σ) := - (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗ - (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I. -Notation "&frac{ κ } P" := (frac_borrow κ P) - (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope. - -Section frac_borrow. - - Context `{invG Σ, lifetimeG Σ}. - - Global Instance frac_borrow_proper : - Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (frac_borrow κ). - Proof. solve_proper. Qed. - Global Instance frac_borrow_persistent : PersistentP (&frac{κ}φ) := _. - - Lemma borrow_fracture φ `(nclose lftN ⊆ E) κ: - &{κ}(φ 1%Qp) ={E}=∗ &frac{κ}φ. - Proof. - iIntros "Hφ". iMod (own_alloc 1%Qp) as (γ) "?". done. - iMod (borrow_acc_atomic_strong with "Hφ") as "[[Hφ Hclose]|[H†Hclose]]". done. - - iMod ("Hclose" with "*[-]") as "Hφ"; last first. - { iExists γ, κ. iSplitR; last by iApply (borrow_share with "Hφ"). - iApply lft_incl_refl. } - iSplitL. by iExists 1%Qp; iFrame; auto. - iIntros "!>[H†Hφ]!>". iNext. iDestruct "Hφ" as (q') "(Hφ & _ & [%|Hκ])". by subst. - iDestruct "Hκ" as (q'') "[_ Hκ]". - iDestruct (lft_own_dead with "[$Hκ $H†]") as "[]". - - iMod ("Hclose" with "*") as "Hφ"; last first. - iExists γ, κ. iSplitR. by iApply lft_incl_refl. - iMod (borrow_fake with "H†"). done. by iApply borrow_share. - Qed. - - Lemma frac_borrow_atomic_acc `(nclose lftN ⊆ E) κ φ: - &frac{κ}φ ={E,E∖lftN}=∗ (∃ q, â–· φ q ∗ (â–· φ q ={E∖lftN,E}=∗ True)) - ∨ [†κ] ∗ |={E∖lftN,E}=> True. - Proof. - iIntros "#Hφ". iDestruct "Hφ" as (γ κ') "[Hκκ' Hshr]". - iMod (shr_borrow_acc with "Hshr") as "[[Hφ Hclose]|[H†Hclose]]". done. - - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame. - iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame. - - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done. - iApply fupd_intro_mask. set_solver. done. - Qed. - - Lemma frac_borrow_acc `(nclose lftN ⊆ E) q κ φ: - â–¡ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢ - &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', â–· φ q' ∗ (â–· φ q' ={E}=∗ q.[κ]). - Proof. - iIntros "#Hφ Hfrac Hκ". unfold frac_borrow. - iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]". - iMod (lft_incl_acc with "Hκκ' Hκ") as (qκ') "[[Hκ1 Hκ2] Hclose]". done. - iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done. - iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)". - destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ). - iExists qq. - iAssert (â–· φ qq ∗ â–· φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]". - { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. } - rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'. - iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]". - iMod ("Hclose'" with "[Hqφ Hq Hown Hκq]") as "Hκ1". - { iNext. iExists _. iFrame. iRight. iDestruct "Hq" as "[%|Hq]". - - subst. iExists qq. iIntros "{$Hκq}!%". - by rewrite (comm _ qφ0) -assoc (comm _ qφ0) -Hqφ Qp_div_2. - - iDestruct "Hq" as (q') "[% Hq'κ]". iExists (qq + q')%Qp. - rewrite lft_own_frac_op. iIntros "{$Hκq $Hq'κ}!%". - by rewrite assoc (comm _ _ qq) assoc -Hqφ Qp_div_2. } - clear Hqφ qφ qφ0. iIntros "!>Hqφ". - iMod (shr_borrow_acc_tok with "Hshr Hκ1") as "[H Hclose']". done. - iDestruct "H" as (qφ) "(Hφqφ & >Hown & >[%|Hq])". - { subst. iCombine "Hown" "Hownq" as "Hown". - by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. } - iDestruct "Hq" as (q') "[Hqφq' Hq'κ]". iCombine "Hown" "Hownq" as "Hown". - iDestruct (own_valid with "Hown") as %Hval. iDestruct "Hqφq'" as %Hqφq'. - assert (0 < q'-qq ∨ qq = q')%Qc as [Hq'q|<-]. - { change (qφ + qq ≤ 1)%Qc in Hval. apply Qp_eq in Hqφq'. simpl in Hval, Hqφq'. - rewrite <-Hqφq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval. - destruct Hval as [Hval|Hval]. - by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. } - - assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. } - iDestruct "Hq'κ" as "[Hq'qκ Hqκ]". - iMod ("Hclose'" with "[Hqφ Hφqφ Hown Hq'qκ]") as "Hqκ2". - { iNext. iExists (qφ + qq)%Qp. iFrame. iSplitR "Hq'qκ". by iApply "Hφ"; iFrame. - iRight. iExists _. iIntros "{$Hq'qκ}!%". - revert Hqφq'. rewrite !Qp_eq. move=>/=<-. ring. } - iApply "Hclose". iFrame. rewrite Hqκ' !lft_own_frac_op. by iFrame. - - iMod ("Hclose'" with "[Hqφ Hφqφ Hown]") as "Hqκ2". - { iNext. iExists (qφ â‹… qq)%Qp. iFrame. iSplitL. by iApply "Hφ"; iFrame. auto. } - iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame. - Qed. - - Lemma frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ. - Proof. - iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame. - iApply lft_incl_trans. iFrame. - Qed. - - Lemma frac_borrow_incl κ κ' q: - &frac{κ}(λ q', (q * q').[κ']) ⊢ κ ⊑ κ'. - Proof. - iIntros "#Hbor!#". iSplitR. - - iIntros (q') "Hκ'". - iMod (frac_borrow_acc with "[] Hbor Hκ'") as (q'') "[>? Hclose]". done. - + iIntros "/=!#*". rewrite Qp_mult_plus_distr_r lft_own_frac_op. iSplit; auto. - + iExists _. iFrame. iIntros "!>Hκ'". iApply "Hclose". auto. - - iIntros "H†'". - iMod (frac_borrow_atomic_acc with "Hbor") as "[H|[$ $]]". done. - iDestruct "H" as (q') "[>Hκ' _]". - iDestruct (lft_own_dead with "[$H†' $Hκ']") as "[]". - Qed. - -End frac_borrow. - -Typeclasses Opaque frac_borrow. - -(** Thread local borrows *) - -Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ} - (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) := - (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I. - -Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P) - (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope. - -Section tl_borrow. - Context `{invG Σ, lifetimeG Σ, thread_localG Σ} - (tid : thread_id) (N : namespace) (P : iProp Σ). - - Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _. - Global Instance tl_borrow_proper κ : - Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N). - Proof. - intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ. - Qed. - - Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P. - Proof. - iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]". - iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto. - Qed. - - Lemma tl_borrow_acc q κ E F : - nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F → - &tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ â–·P ∗ tl_own tid (F ∖ N) ∗ - (â–·P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F). - Proof. - iIntros (???) "#HP[Hκ Htlown]". - iDestruct "HP" as (i) "(#Hpers&#Hinv)". - iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done. - iMod (idx_borrow_acc with "Hpers [$Hown $Hκ]") as "[HP Hclose']". done. - iIntros "{$HP $Htlown}!>[HP Htlown]". - iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame. - Qed. - - Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P. - Proof. - iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame. - iApply (idx_borrow_shorten with "Hκκ' H"). - Qed. - -End tl_borrow. - -Typeclasses Opaque tl_borrow. diff --git a/theories/perm.v b/theories/perm.v index c6cc6caa..e268dacd 100644 --- a/theories/perm.v +++ b/theories/perm.v @@ -8,7 +8,7 @@ Module Perm. Section perm. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. Fixpoint eval_expr (ν : expr) : option val := match ν with @@ -70,7 +70,7 @@ Infix "∗" := sep (at level 80, right associativity) : perm_scope. Section duplicable. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. Class Duplicable (Ï : @perm Σ) := duplicable_persistent tid : PersistentP (Ï tid). @@ -93,7 +93,7 @@ End duplicable. Section has_type. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. Lemma has_type_value (v : val) ty tid : (v â— ty)%P tid ⊣⊢ ty.(ty_own) tid [v]. diff --git a/theories/perm_incl.v b/theories/perm_incl.v index 93de38c1..cca2d892 100644 --- a/theories/perm_incl.v +++ b/theories/perm_incl.v @@ -6,7 +6,7 @@ Import Perm Types. Section defs. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. (* Definitions *) Definition perm_incl (Ï1 Ï2 : perm) := @@ -29,7 +29,7 @@ Notation "(⇔)" := (equiv (A:=perm)) (only parsing) : C_scope. Section props. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. (* Properties *) Global Instance perm_incl_preorder : PreOrder (⇒). diff --git a/theories/shr_borrow.v b/theories/shr_borrow.v new file mode 100644 index 00000000..b586f64c --- /dev/null +++ b/theories/shr_borrow.v @@ -0,0 +1,54 @@ +From iris.algebra Require Import gmap auth frac. +From iris.proofmode Require Import tactics. +From lrust Require Export lifetime. + +(** Shared borrows *) +Definition shr_borrow `{invG Σ, lifetimeG Σ} κ (P : iProp Σ) := + (∃ i, idx_borrow κ i P ∗ inv lftN (∃ q, idx_borrow_own q i))%I. +Notation "&shr{ κ } P" := (shr_borrow κ P) + (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope. + +Section shared_borrows. + Context `{invG Σ, lifetimeG Σ} (P : iProp Σ). + + Global Instance shr_borrow_proper : + Proper ((⊣⊢) ==> (⊣⊢)) (shr_borrow κ). + Proof. solve_proper. Qed. + Global Instance shr_borrow_persistent : PersistentP (&shr{κ} P) := _. + + Lemma borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P. + Proof. + iIntros "HP". unfold borrow. iDestruct "HP" as (i) "(#?&Hown)". + iExists i. iFrame "#". iApply inv_alloc. auto. + Qed. + + Lemma shr_borrow_acc `(nclose lftN ⊆ E) κ : + &shr{κ}P ={E,E∖lftN}=∗ â–·P ∗ (â–·P ={E∖lftN,E}=∗ True) ∨ + [†κ] ∗ |={E∖lftN,E}=> True. + Proof. + iIntros "#HP". iDestruct "HP" as (i) "(#Hidx&#Hinv)". + iInv lftN as (q') ">Hq'" "Hclose". + rewrite -(Qp_div_2 q') /idx_borrow_own -op_singleton auth_frag_op own_op. + iDestruct "Hq'" as "[Hq'0 Hq'1]". iMod ("Hclose" with "[Hq'1]") as "_". by eauto. + iMod (idx_borrow_atomic_acc with "Hidx Hq'0") as "[[HP Hclose]|[H†Hclose]]". done. + - iLeft. iFrame. iIntros "!>HP". by iMod ("Hclose" with "HP"). + - iRight. iFrame. iIntros "!>". by iMod "Hclose". + Qed. + + Lemma shr_borrow_acc_tok `(nclose lftN ⊆ E) q κ : + &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ â–·P ∗ (â–·P ={E∖lftN,E}=∗ q.[κ]). + Proof. + iIntros "#Hshr Hκ". iMod (shr_borrow_acc with "Hshr") as "[[$ Hclose]|[H†_]]". done. + - iIntros "!>HP". by iMod ("Hclose" with "HP"). + - iDestruct (lft_own_dead with "[-]") as "[]". by iFrame. + Qed. + + Lemma shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P. + Proof. + iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame. + by iApply (idx_borrow_shorten with "H⊑"). + Qed. + +End shared_borrows. + +Typeclasses Opaque shr_borrow. diff --git a/theories/tl_borrow.v b/theories/tl_borrow.v new file mode 100644 index 00000000..41bfa9b5 --- /dev/null +++ b/theories/tl_borrow.v @@ -0,0 +1,50 @@ +From lrust Require Export lifetime. +From iris.base_logic.lib Require Export thread_local. +From iris.proofmode Require Import tactics. + +Definition tl_borrow `{invG Σ, lifetimeG Σ, thread_localG Σ} + (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) := + (∃ i, idx_borrow κ i P ∗ tl_inv tid N (idx_borrow_own 1 i))%I. + +Notation "&tl{ κ | tid | N } P" := (tl_borrow κ tid N P) + (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope. + +Section tl_borrow. + Context `{invG Σ, lifetimeG Σ, thread_localG Σ} + (tid : thread_id) (N : namespace) (P : iProp Σ). + + Global Instance tl_borrow_persistent κ : PersistentP (&tl{κ|tid|N} P) := _. + Global Instance tl_borrow_proper κ : + Proper ((⊣⊢) ==> (⊣⊢)) (tl_borrow κ tid N). + Proof. + intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ. + Qed. + + Lemma borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P. + Proof. + iIntros "HP". unfold borrow. iDestruct "HP" as (i) "[#? Hown]". + iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto. + Qed. + + Lemma tl_borrow_acc q κ E F : + nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F → + &tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ â–·P ∗ tl_own tid (F ∖ N) ∗ + (â–·P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F). + Proof. + iIntros (???) "#HP[Hκ Htlown]". + iDestruct "HP" as (i) "(#Hpers&#Hinv)". + iMod (tl_inv_open with "Hinv Htlown") as "(>Hown&Htlown&Hclose)"; try done. + iMod (idx_borrow_acc with "Hpers [$Hown $Hκ]") as "[HP Hclose']". done. + iIntros "{$HP $Htlown}!>[HP Htlown]". + iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame. + Qed. + + Lemma tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P. + Proof. + iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame. + iApply (idx_borrow_shorten with "Hκκ' H"). + Qed. + +End tl_borrow. + +Typeclasses Opaque tl_borrow. diff --git a/theories/type.v b/theories/type.v index be61b1d5..46231d46 100644 --- a/theories/type.v +++ b/theories/type.v @@ -1,7 +1,14 @@ From iris.base_logic Require Import big_op. From iris.base_logic.lib Require Export thread_local. From iris.program_logic Require Import hoare. -From lrust Require Export notation lifetime heap. +From lrust Require Export notation lifetime frac_borrow heap. + +Class iris_typeG Σ := Iris_typeG { + type_heapG :> heapG Σ; + type_lifetimeG :> lifetimeG Σ; + type_thread_localG :> thread_localG Σ; + type_frac_borrowG Σ :> frac_borrowG Σ +}. Definition mgmtE := nclose tlN ∪ lftN. Definition lrustN := nroot .@ "lrust". @@ -9,12 +16,11 @@ Definition lrustN := nroot .@ "lrust". (* [perm] is defined here instead of perm.v in order to define [cont] *) Definition perm {Σ} := thread_id → iProp Σ. -(* We would like to put the defintions of [type] and [simple_type] in - a section to generalize over [Σ] and all the [xxxG], but - [simple_type] would not depend on all that and this would make us - unable to define [ty_of_st] as a coercion... *) +Section type. + +Context `{iris_typeG Σ}. -Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} := +Record type := { ty_size : nat; ty_dup : bool; ty_own : thread_id → list val → iProp Σ; ty_shr : lifetime → thread_id → namespace → loc → iProp Σ; @@ -44,7 +50,10 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} := }. Global Existing Instances ty_shr_persistent ty_dup_persistent. -Record simple_type `{heapG Σ, lifetimeG Σ, thread_localG Σ} := +(* We are repeating the typeclass parameter here jsut to make sure + that simple_type does depend on it. Otherwise, the coercion defined + bellow will not be acceptable by Coq. *) +Record simple_type `{iris_typeG Σ} := { st_size : nat; st_own : thread_id → list val → iProp Σ; @@ -52,8 +61,7 @@ Record simple_type `{heapG Σ, lifetimeG Σ, thread_localG Σ} := st_own_persistent tid vl : PersistentP (st_own tid vl) }. Global Existing Instance st_own_persistent. -Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ} - (st : simple_type) : type := +Program Coercion ty_of_st (st : simple_type) : type := {| ty_size := st.(st_size); ty_dup := true; ty_own := st.(st_own); @@ -65,7 +73,7 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ} |}. Next Obligation. intros. apply st_size_eq. Qed. Next Obligation. - intros Σ ??? st E N κ l tid q ??. iIntros "Hmt Htok". + intros st E N κ l tid q ? ?. iIntros "Hmt Htok". iMod (borrow_exists with "Hmt") as (vl) "Hmt". set_solver. iMod (borrow_split with "Hmt") as "[Hmt Hown]". set_solver. iMod (borrow_persistent with "Hown Htok") as "[Hown $]". set_solver. @@ -74,12 +82,11 @@ Next Obligation. done. set_solver. Qed. Next Obligation. - intros Σ???. iIntros (st κ κ' tid N l) "#Hord H". - iDestruct "H" as (vl) "[Hf Hown]". + iIntros (st κ κ' tid N l) "#Hord H". iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame. by iApply (frac_borrow_shorten with "Hord"). Qed. Next Obligation. - intros Σ??? st κ tid N E l q ??. iIntros "#Hshr[Hlft $]". + intros st κ tid N E l q ??. iIntros "#Hshr[Hlft $]". iDestruct "Hshr" as (vl) "[Hf Hown]". iMod (frac_borrow_acc with "[] Hf Hlft") as (q') "[Hmt Hclose]"; first set_solver. @@ -97,13 +104,15 @@ Next Obligation. iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose". Qed. +End type. + Delimit Scope lrust_type_scope with T. Bind Scope lrust_type_scope with type. Module Types. Section types. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. (* [emp] cannot be defined using [ty_of_st], because the least we would be able to prove from its [ty_shr] would be [â–· False], but diff --git a/theories/type_incl.v b/theories/type_incl.v index 5366276b..2c8a0c1c 100644 --- a/theories/type_incl.v +++ b/theories/type_incl.v @@ -6,7 +6,7 @@ Import Types. Section ty_incl. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. Definition ty_incl (Ï : perm) (ty1 ty2 : type) := ∀ tid, Ï tid ={⊤}=∗ diff --git a/theories/typing.v b/theories/typing.v index b8249aa1..9e8d0a00 100644 --- a/theories/typing.v +++ b/theories/typing.v @@ -6,7 +6,7 @@ Import Types Perm. Section typing. - Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}. + Context `{iris_typeG Σ}. (* TODO : good notations for [typed_step] and [typed_step_ty] ? *) Definition typed_step (Ï : perm) e (θ : val → perm) := @@ -150,7 +150,7 @@ Section typing. Proof. iIntros (? tid) "!#(#HEAP&_&$)". wp_alloc l vl as "H↦" "H†". iIntros "!>". iExists _. iSplit. done. iNext. rewrite Nat2Z.id. iFrame. - apply (inj Z.of_nat) in H3. iExists _. iFrame. auto. + iExists _. iFrame. iPureIntro. by apply (inj Z.of_nat). Qed. Lemma typed_free ty (ν : expr): -- GitLab