diff --git a/_CoqProject b/_CoqProject
index 40d481ed0ed5287dcf7f21ec2690d2545e5d70d3..28a244a52fc3f4023e523ab031b6fb6cb2b05dd8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -48,3 +48,4 @@ theories/typing/tests/rebor.v
theories/typing/tests/unbox.v
theories/typing/tests/init_prod.v
theories/typing/tests/option_as_mut.v
+theories/typing/unsafe/cell.v
diff --git a/awk.Makefile b/awk.Makefile
index 526cf3c4ed7895f7197fb248bc1fecb60928e238..09ded0aa64f3a85ee4a55668d21ee17bb9a362f0 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -13,7 +13,7 @@
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
/^uninstall:/ {
print "uninstall:";
- print "\tif [ -d \"$$(DSTROOT)\"$$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$$(DSTROOT)\"$$(COQLIBINSTALL)/"PROJECT"/ -name \"*.vo\" -print -delete; fi";
+ print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
getline;
next
}
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 9ee11aa4c200efc1d625349a64ed0421bec0ec8e..c618222fcf06405e257584fc78eeb728a7a77c80 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -104,4 +104,3 @@ Proof.
- iIntros "Hst". by iDestruct (lft_dead_static with "Hst") as "[]".
Qed.
End derived.
-
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index aea0750cc29e55084d8b45700c722b2d83ca56c0..52fdd1f33ec16810db02af1ec5e1be26f2237a5c 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import csum auth frac gmap agree gset.
+From iris.algebra Require Import frac.
From iris.prelude Require Export gmultiset strings.
From iris.base_logic.lib Require Export invariants.
From iris.base_logic.lib Require Import boxes fractional.
@@ -13,57 +13,16 @@ Definition atomic_lft := positive.
Notation lft := (gmultiset positive).
Definition static : lft := ∅.
-Inductive bor_state :=
- | Bor_in
- | Bor_open (q : frac)
- | Bor_rebor (κ : lft).
-Instance bor_state_eq_dec : EqDecision bor_state.
-Proof. solve_decision. Defined.
-Canonical bor_stateC := leibnizC bor_state.
-
-Record lft_names := LftNames {
- bor_name : gname;
- cnt_name : gname;
- inh_name : gname
-}.
-Instance lft_names_eq_dec : EqDecision lft_names.
-Proof. solve_decision. Defined.
-Canonical lft_namesC := leibnizC lft_names.
-
-Definition lft_stateR := csumR fracR unitR.
-Definition alftUR := gmapUR atomic_lft lft_stateR.
-Definition ilftUR := gmapUR lft (agreeR lft_namesC).
-Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
-Definition inhUR := gset_disjUR slice_name.
-
-Class lftG Σ := LftG {
- lft_box :> boxG Σ;
- alft_inG :> inG Σ (authR alftUR);
- alft_name : gname;
- ilft_inG :> inG Σ (authR ilftUR);
- ilft_name : gname;
- lft_bor_inG :> inG Σ (authR borUR);
- lft_cnt_inG :> inG Σ (authR natUR);
- lft_inh_inG :> inG Σ (authR inhUR);
-}.
-
-Class lftPreG Σ := LftPreG {
- lft_preG_box :> boxG Σ;
- alft_preG_inG :> inG Σ (authR alftUR);
- ilft_preG_inG :> inG Σ (authR ilftUR);
- lft_preG_bor_inG :> inG Σ (authR borUR);
- lft_preG_cnt_inG :> inG Σ (authR natUR);
- lft_preG_inh_inG :> inG Σ (authR inhUR);
-}.
-
-Definition lftΣ : gFunctors :=
- #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
- GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_stsΣ Σ :
- subG lftΣ Σ → lftPreG Σ.
-Proof. solve_inG. Qed.
-
Module Type lifetime_sig.
+ (** CMRAs needed by the lifetime logic *)
+ (* We can't instantie the module parameters with inductive types, so we have aliases here. *)
+ Parameter lftG' : gFunctors → Set.
+ Global Notation lftG := lftG'.
+ Existing Class lftG'.
+ Parameter lftPreG' : gFunctors → Set.
+ Global Notation lftPreG := lftPreG'.
+ Existing Class lftPreG'.
+
(** Definitions *)
Parameter lft_ctx : ∀ `{invG, lftG Σ}, iProp Σ.
@@ -76,7 +35,8 @@ Module Type lifetime_sig.
Parameter bor_idx : Type.
Parameter idx_bor_own : ∀ `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
Parameter idx_bor : ∀ `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
-
+
+ (** Notation *)
Notation "q .[ κ ]" := (lft_tok q κ)
(format "q .[ κ ]", at level 0) : uPred_scope.
Notation "[†κ ]" := (lft_dead κ) (format "[†κ ]"): uPred_scope.
@@ -190,6 +150,9 @@ Module Type lifetime_sig.
End properties.
+ Parameter lftΣ : gFunctors.
+ Global Declare Instance subG_lftΣ Σ : subG lftΣ Σ → lftPreG Σ.
+
Parameter lft_init : ∀ `{invG Σ, !lftPreG Σ} E, ↑lftN ⊆ E →
True ={E}=∗ ∃ _ : lftG Σ, lft_ctx.
End lifetime_sig.
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 97a5cde305b35e9e2d5d0d30269b4b24a4c9cd8b..a84788de8bb7c3fb1653c245f848e51526f2b5d7 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -1,3 +1,4 @@
+From iris.algebra Require Import csum auth frac gmap agree gset.
From iris.algebra Require Import csum auth frac agree gset.
From iris.base_logic Require Import big_op.
From iris.base_logic.lib Require Import boxes.
@@ -5,6 +6,57 @@ From lrust.lifetime Require Export lifetime_sig.
Set Default Proof Using "Type".
Import uPred.
+Inductive bor_state :=
+ | Bor_in
+ | Bor_open (q : frac)
+ | Bor_rebor (κ : lft).
+Instance bor_state_eq_dec : EqDecision bor_state.
+Proof. solve_decision. Defined.
+Canonical bor_stateC := leibnizC bor_state.
+
+Record lft_names := LftNames {
+ bor_name : gname;
+ cnt_name : gname;
+ inh_name : gname
+}.
+Instance lft_names_eq_dec : EqDecision lft_names.
+Proof. solve_decision. Defined.
+Canonical lft_namesC := leibnizC lft_names.
+
+Definition lft_stateR := csumR fracR unitR.
+Definition alftUR := gmapUR atomic_lft lft_stateR.
+Definition ilftUR := gmapUR lft (agreeR lft_namesC).
+Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateC)).
+Definition inhUR := gset_disjUR slice_name.
+
+Class lftG Σ := LftG {
+ lft_box :> boxG Σ;
+ alft_inG :> inG Σ (authR alftUR);
+ alft_name : gname;
+ ilft_inG :> inG Σ (authR ilftUR);
+ ilft_name : gname;
+ lft_bor_inG :> inG Σ (authR borUR);
+ lft_cnt_inG :> inG Σ (authR natUR);
+ lft_inh_inG :> inG Σ (authR inhUR);
+}.
+Definition lftG' := lftG.
+
+Class lftPreG Σ := LftPreG {
+ lft_preG_box :> boxG Σ;
+ alft_preG_inG :> inG Σ (authR alftUR);
+ ilft_preG_inG :> inG Σ (authR ilftUR);
+ lft_preG_bor_inG :> inG Σ (authR borUR);
+ lft_preG_cnt_inG :> inG Σ (authR natUR);
+ lft_preG_inh_inG :> inG Σ (authR inhUR);
+}.
+Definition lftPreG' := lftPreG.
+
+Definition lftΣ : gFunctors :=
+ #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
+ GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
+Instance subG_lftΣ Σ :
+ subG lftΣ Σ → lftPreG Σ.
+Proof. solve_inG. Qed.
Definition bor_filled (s : bor_state) : bool :=
match s with Bor_in => true | _ => false end.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index d61bac2c178ca6a9a5ba1fc4edb0e591cb56c265..4be5c06e01b45d141320dc64165f1f6d8209ed54 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -30,13 +30,13 @@ Section na_bor.
iExists i. iFrame "#". iApply (na_inv_alloc tid E N with "[Hown]"). auto.
Qed.
- Lemma na_bor_acc q κ E :
- ↑lftN ⊆ E → ↑N ⊆ E →
- lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid E ={E}=∗
- ▷P ∗ na_own tid (E ∖ ↑N) ∗
- (▷P -∗ na_own tid (E ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid E).
+ Lemma na_bor_acc q κ E F :
+ ↑lftN ⊆ E → ↑N ⊆ E → ↑N ⊆ F →
+ lft_ctx -∗ &na{κ,tid,N}P -∗ q.[κ] -∗ na_own tid F ={E}=∗
+ ▷P ∗ na_own tid (F ∖ ↑N) ∗
+ (▷P -∗ na_own tid (F ∖ ↑N) ={E}=∗ q.[κ] ∗ na_own tid F).
Proof.
- iIntros (??) "#LFT#HP Hκ Hnaown".
+ iIntros (???) "#LFT#HP Hκ Hnaown".
iDestruct "HP" as (i) "(#Hpers&#Hinv)".
iMod (na_inv_open with "Hinv Hnaown") as "(>Hown&Hnaown&Hclose)"; try done.
iMod (idx_bor_acc with "LFT Hpers Hown Hκ") as "[HP Hclose']". done.
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 154dca9f6e688d6fe2a454e22aea104ebfccb38f..dce282b4072ed5075cd5bac4c9e8f6b310d8c405 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -95,6 +95,7 @@ Section product_split.
iDestruct "H" as (vl1 vl2) "(>% & H1 & H2)". subst.
rewrite heap_mapsto_vec_app -freeable_sz_split.
iDestruct "H†" as "[H†1 H†2]". iDestruct "H↦" as "[H↦1 H↦2]".
+ (* FIXME: I found no way to use ty_size_eq_later here to avoid the assert. *)
iAssert (â–· ⌜length vl1 = ty_size ty1âŒ)%I with "[#]" as ">EQ".
{ iNext. by iApply ty_size_eq. }
iDestruct "EQ" as %->. iSplitL "H↦1 H†1 H1".
diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index d8e86466bed6e7cdccffcfc82d25dfa2e229dd57..bbc5971228d8133b44ce98824aa62cb1080b090c 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
Section get_x.
Context `{typeG Σ}.
- Definition get_x :=
- (funrec: <> ["p"] :=
+ Definition get_x : val :=
+ funrec: <> ["p"] :=
let: "p'" := !"p" in
letalloc: "r" <- "p'" +â‚— #0 in
- delete [ #1; "p"] ;; "return" ["r":expr])%E.
+ delete [ #1; "p"] ;; "return" ["r":expr].
Lemma get_x_type :
typed_instruction_ty [] [] [] get_x
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index f8cd890a92b0e7f2cc6db738a1debba94d9ecbb9..827d339702e296f7e106272180e39aa2ae617548 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -7,12 +7,12 @@ Set Default Proof Using "Type".
Section rebor.
Context `{typeG Σ}.
- Definition init_prod :=
- (funrec: <> ["x"; "y"] :=
+ Definition init_prod : val :=
+ funrec: <> ["x"; "y"] :=
let: "x'" := !"x" in let: "y'" := !"y" in
let: "r" := new [ #2] in
"r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
- delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr])%E.
+ delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr].
Lemma init_prod_type :
typed_instruction_ty [] [] [] init_prod
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index 1526e3a98130e8361e07b35e9b2d081cd611bb1c..24caf373b86639068f7af58ba8b99c120833f61e 100644
--- a/theories/typing/tests/rebor.v
+++ b/theories/typing/tests/rebor.v
@@ -7,8 +7,8 @@ Set Default Proof Using "Type".
Section rebor.
Context `{typeG Σ}.
- Definition rebor :=
- (funrec: <> ["t1"; "t2"] :=
+ Definition rebor : val :=
+ funrec: <> ["t1"; "t2"] :=
Newlft;;
letalloc: "x" <- "t1" in
let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
@@ -16,7 +16,7 @@ Section rebor.
let: "y'" := !"y" in
letalloc: "r" <- "y'" in
Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
- delete [ #1; "x"] ;; "return" ["r":expr])%E.
+ delete [ #1; "x"] ;; "return" ["r":expr].
Lemma rebor_type :
typed_instruction_ty [] [] [] rebor
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index 27f8c3b8e2b41d11a91d4a5647fdea4757158213..ff4a5a7b466d1856225254f960c1138b356f23c6 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
Section unbox.
Context `{typeG Σ}.
- Definition unbox :=
- (funrec: <> ["b"] :=
+ Definition unbox : val :=
+ funrec: <> ["b"] :=
let: "b'" := !"b" in let: "bx" := !"b'" in
letalloc: "r" <- "bx" +â‚— #0 in
- delete [ #1; "b"] ;; "return" ["r":expr])%E.
+ delete [ #1; "b"] ;; "return" ["r":expr].
Lemma ubox_type :
typed_instruction_ty [] [] [] unbox
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 89ffb4c61faeb4826c5af1cb7ec3fe6b839cd05b..31c53a2ba69ac68706f8e9afea4cd88d16030cca 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,6 +50,11 @@ Section type.
}.
Global Existing Instances ty_shr_persistent.
+ Lemma ty_size_eq_later (ty : type) tid vl :
+ â–· ty.(ty_own) tid vl -∗ â–· ⌜length vl = ty.(ty_size)âŒ.
+ Proof. iIntros "Hown". iApply ty_size_eq. done. Qed.
+
+ (** Copy types *)
Fixpoint shr_locsE (l : loc) (n : nat) : coPset :=
match n with
| 0%nat => ∅
@@ -99,7 +104,6 @@ Section type.
rewrite shr_locsE_shift na_own_union //. apply shr_locsE_disj.
Qed.
- (** Copy types *)
Class Copy (t : type) := {
copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
copy_shr_acc κ tid E F l q :
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index e20a4f686fd994568680be66400a4c179b702df4..c07ed71e55555ef1fafbf359485690d9cfa30ff8 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -7,7 +7,6 @@ Set Default Proof Using "Type".
Section uniq_bor.
Context `{typeG Σ}.
-
Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
Program Definition uniq_bor (κ:lft) (ty:type) :=
@@ -155,7 +154,7 @@ Section typing.
Proof.
iIntros (Hκ ???) "#LFT HE HL Huniq".
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; [try done..|].
- rewrite /tctx_interp !big_sepL_singleton /=.
+ rewrite !tctx_interp_singleton /=.
iDestruct "Huniq" as (v) "[% Huniq]".
iDestruct "Huniq" as (l P) "[[% #HPiff] HP]".
iMod (bor_iff with "LFT [] HP") as "H↦". set_solver. by eauto.
@@ -172,7 +171,7 @@ Section typing.
iDestruct (elctx_interp_persist with "HE") as "#HE'".
iDestruct (llctx_interp_persist with "HL") as "#HL'". iFrame "HE HL".
iDestruct (Hκκ' with "HE' HL'") as "Hκκ'".
- rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+ rewrite tctx_interp_singleton tctx_interp_cons tctx_interp_singleton.
iDestruct "H" as (v) "[% Hown]". iDestruct "Hown" as (l P) "[[EQ #Hiff] Hb]".
iDestruct "EQ" as %[=->]. iMod (bor_iff with "LFT [] Hb") as "Hb". done. by eauto.
iMod (rebor with "LFT Hκκ' Hb") as "[Hb Hext]". done. iModIntro. iSplitL "Hb".
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
new file mode 100644
index 0000000000000000000000000000000000000000..bfd5dcbbfaf7b7cf4632c406dcaa88d4d876accc
--- /dev/null
+++ b/theories/typing/unsafe/cell.v
@@ -0,0 +1,74 @@
+From iris.proofmode Require Import tactics.
+From lrust.lifetime Require Import na_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import type_context programs.
+Set Default Proof Using "Type".
+
+Section cell.
+ Context `{typeG Σ}.
+ Local Hint Extern 1000 (_ ⊆ _) => set_solver : ndisj.
+
+ Program Definition cell (ty : type) :=
+ {| ty_size := ty.(ty_size);
+ ty_own := ty.(ty_own);
+ ty_shr κ tid l := (&na{κ, tid, shrN.@l} l ↦∗: ty.(ty_own) tid)%I |}.
+ Next Obligation. apply ty_size_eq. Qed.
+ Next Obligation.
+ iIntros (ty E κ l tid q ?) "#LFT Hown $". by iApply bor_na.
+ Qed.
+ Next Obligation.
+ iIntros (ty ?? tid l) "#LFT". iApply na_bor_shorten.
+ Qed.
+
+ (* TODO: non-expansiveness, proper wrt. eqtype *)
+
+ Global Instance cell_type :
+ Copy ty → Copy (cell ty).
+ Proof.
+ intros ty Hcopy. split; first by intros; simpl; apply _.
+ iIntros (κ tid E F l q ??) "#LFT #Hshr Htl Htok". iExists 1%Qp. simpl in *.
+ (* Size 0 needs a special case as we can't keep the thread-local invariant open. *)
+ destruct (ty_size ty) as [|sz] eqn:Hsz.
+ { iMod (na_bor_acc with "LFT Hshr Htok Htl") as "(Hown & Htl & Hclose)"; [solve_ndisj..|].
+ iDestruct "Hown" as (vl) "[H↦ #Hown]".
+ simpl. assert (F ∖ ∅ = F) as -> by set_solver+.
+ iAssert (â–· ⌜length vl = ty_size tyâŒ)%I with "[#]" as ">EQ".
+ { iNext. by iApply ty_size_eq. }
+ rewrite Hsz. iDestruct "EQ" as %EQ. iMod ("Hclose" with "[H↦] Htl") as "[$ $]".
+ { iExists vl. by iFrame. }
+ iModIntro. iSplitL "".
+ { iNext. iExists vl. destruct vl; last done. iFrame "Hown".
+ by iApply heap_mapsto_vec_nil. }
+ by iIntros "$ _". }
+ (* Now we are in the non-0 case. *)
+ iMod (na_bor_acc with "LFT Hshr Htok Htl") as "($ & Htl & Hclose)"; [solve_ndisj..|].
+ iDestruct (na_own_acc with "Htl") as "($ & Hclose')"; first by set_solver.
+ iIntros "!> Htl Hown". iPoseProof ("Hclose'" with "Htl") as "Htl".
+ iMod ("Hclose" with "Hown Htl") as "[$ $]". done.
+ Qed.
+
+ Global Instance cell_send :
+ Send ty → Send (cell ty).
+ Proof. intros. split. simpl. apply send_change_tid. Qed.
+
+End cell.
+
+Section typing.
+ Context `{typeG Σ}.
+
+ (* Constructing a cell is a coercion. *)
+ Lemma tctx_mk_cell E L ty p :
+ tctx_incl E L [p â— ty] [p â— cell ty].
+ Proof.
+ iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
+ Qed.
+
+ (* Same for the other direction *)
+ Lemma tctx_unmk_cell E L ty p :
+ tctx_incl E L [p â— ty] [p â— cell ty].
+ Proof.
+ iIntros (???) "#LFT $ $ Hty". rewrite !tctx_interp_singleton /=. done.
+ Qed.
+
+ (* TODO: get, set; potentially more operations? *)
+End typing.