From 97bb9b8b41a22cfd49a40b313c88e977c955ab7b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2017 14:46:33 +0100
Subject: [PATCH] Prove that Cell<T> is a type and copy if T is copy

---
 theories/lifetime/na_borrow.v | 12 +++---
 theories/typing/uniq_bor.v    |  4 +-
 theories/typing/unsafe/cell.v | 74 +++++++++++++++++++++++++++++++++++
 3 files changed, 82 insertions(+), 8 deletions(-)
 create mode 100644 theories/typing/unsafe/cell.v

diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index d61bac2c..4be5c06e 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/uniq_bor.v b/theories/typing/uniq_bor.v
index cf019f8a..c07ed71e 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -154,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.
@@ -171,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 00000000..bfd5dcbb
--- /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.
-- 
GitLab