From 8a0cdda5766a190bea851a5c8d8833b1f5caa32e Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 19 Dec 2016 19:18:16 +0100
Subject: [PATCH] add Sync; get rid of Send and Copy for type contexts

---
 theories/typing/function.v     | 13 ++++-----
 theories/typing/type.v         | 10 ++++++-
 theories/typing/type_context.v | 48 ++++++++++++++--------------------
 theories/typing/uniq_bor.v     |  7 ++++-
 4 files changed, 42 insertions(+), 36 deletions(-)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index 4969c06d..323a37ce 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -1,6 +1,5 @@
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
 From lrust.typing Require Import programs.
@@ -117,13 +116,15 @@ Section fn.
     - (* TODO: The IH is not usable here. What we really want is to do induction over "how many of the arguments still need to be evaluated", so the base case has all the ps evaluated and the inductive case evaluates one of them. *)
   Abort.
 
-  Lemma typed_fn {A n} E L T E' (tys : A → vec type n) ty fb kb
-        (argsb : vec binder n) ef e `{!CopyC T, !SendC T} :
+  Lemma typed_fn {A n m} E L E' (tys : A → vec type n) ty fb kb (argsb : vec binder n) ef e
+       (cps : vec path m) (ctyl : vec type m) `{!LstCopy ctyl, !LstSend ctyl} :
     ef = Rec fb (kb :: argsb) e → Closed (fb :b: kb :b: argsb +b+ []) e →
     (∀ x f k (args : vec val n), typed_body (E' x) [] [CctxElt k [] 1 (λ v, [TCtx_hasty (v!!!0) (ty x)])]
-                 (TCtx_hasty f (fn E' tys ty) :: zip_with (TCtx_hasty ∘ of_val) args (tys x) ++ T)
+                 (TCtx_hasty f (fn E' tys ty) ::
+                  zip_with (TCtx_hasty ∘ of_val) args (tys x) ++
+                  zip_with TCtx_hasty cps ctyl)
                  (subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
-    typed_instruction_ty E L T ef (fn E' tys ty).
+    typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl) ef (fn E' tys ty).
   Proof.
     iIntros (-> Hc Hbody). iIntros (tid qE) "!# #LFT $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
@@ -137,6 +138,6 @@ Section fn.
     rewrite [elctx_interp]lock [llctx_interp]lock [tctx_interp]lock.
     wp_rec. unlock. subst eb. iApply (Hbody with "* LFT HE HL HC").
     rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
-    iApply sendc_change_tid. done.
+    iApply tctx_send. done.
   Qed.
 End fn.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index f01a0d3a..34bccb46 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -108,7 +108,7 @@ Section type.
   Global Instance lst_copy_cons ty tys :
     Copy ty → LstCopy tys → LstCopy (ty::tys) := List.Forall_cons _ _ _.
 
-  (** Send types *)
+  (** Send and Sync types *)
   Class Send (t : type) :=
     send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 
@@ -117,6 +117,14 @@ Section type.
   Global Instance lst_send_cons ty tys :
     Send ty → LstSend tys → LstSend (ty::tys) := List.Forall_cons _ _ _.
 
+  Class Sync (t : type) :=
+    sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
+
+  Class LstSync (tys : list type) := lst_sync : Forall Sync tys.
+  Global Instance lst_sync_nil : LstSync [] := List.Forall_nil _.
+  Global Instance lst_sync_cons ty tys :
+    Sync ty → LstSync tys → LstSync (ty::tys) := List.Forall_cons _ _ _.
+
   (** Simple types *)
   (* We are repeating the typeclass parameter here just to make sure
      that simple_type does depend on it. Otherwise, the coercion defined
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 2ddb488b..225d2457 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -57,37 +57,28 @@ Section type_context.
     tctx_interp tid [x] ≡ tctx_elt_interp tid x.
   Proof. rewrite tctx_interp_cons tctx_interp_nil right_id //. Qed.
 
-  (** Copy typing contexts *)
-  Class CopyC (T : tctx) :=
-    copyc_persistent tid : PersistentP (tctx_interp tid T).
-  Global Existing Instances copyc_persistent.
-
-  Global Instance tctx_nil_copy : CopyC [].
-  Proof. rewrite /CopyC. apply _. Qed.
-
-  Global Instance tctx_ty_copy T p ty :
-    CopyC T → Copy ty → CopyC (TCtx_hasty p ty :: T).
+  Global Instance tctx_persistent cps ctyl tid :
+    LstCopy ctyl → PersistentP (tctx_interp tid $ zip_with TCtx_hasty cps ctyl).
   Proof.
+    intros Hcopy. revert cps; induction Hcopy; intros cps;
+      first by (rewrite zip_with_nil_r tctx_interp_nil; apply _).
+    destruct cps; first by (rewrite tctx_interp_nil; apply _). simpl.
     (* TODO RJ: Should we have instances that PersistentP respects equiv? *)
-    intros ???. rewrite /PersistentP tctx_interp_cons.
+    rewrite /PersistentP tctx_interp_cons.
     apply uPred.sep_persistent; by apply _.
   Qed.
 
-  (** Send typing contexts *)
-  Class SendC (T : tctx) :=
-    sendc_change_tid tid1 tid2 : tctx_interp tid1 T -∗ tctx_interp tid2 T.
-
-  Global Instance tctx_nil_send : SendC [].
-  Proof. done. Qed.
-
-  Global Instance tctx_ty_send T p ty :
-    SendC T → Send ty → SendC (TCtx_hasty p ty :: T).
+  Lemma tctx_send cps ctyl tid1 tid2 {Hcopy : LstSend ctyl} :
+    tctx_interp tid1 $ zip_with TCtx_hasty cps ctyl -∗
+                tctx_interp tid2 $ zip_with TCtx_hasty cps ctyl.
   Proof.
-    iIntros (HT Hty ??). rewrite !tctx_interp_cons.
-    iIntros "[Hty HT]". iSplitR "HT".
+    revert cps; induction Hcopy; intros cps;
+      first by rewrite zip_with_nil_r !tctx_interp_nil.
+    destruct cps; first by rewrite !tctx_interp_nil. simpl.
+    rewrite !tctx_interp_cons. iIntros "[Hty HT]". iSplitR "HT".
     - iDestruct "Hty" as (?) "[% Hty]". iExists _. iSplit; first done.
-      by iApply Hty.
-    - by iApply HT.
+      by iApply send_change_tid.
+    - by iApply IHHcopy.
   Qed.
 
   (** Type context inclusion *)
@@ -151,10 +142,11 @@ Section type_context.
     by iApply (Hincl with "LFT HE HL").
   Qed.
 
-  Lemma copy_tctx_incl E L T `{!CopyC T} :
-    tctx_incl E L T (T ++ T).
-  Proof.
-    iIntros (???) "_ $ $ * #?". rewrite tctx_interp_app. by iSplitL.
+  Lemma copy_tctx_incl E L p `{!Copy ty} :
+    tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty].
+   Proof.
+    iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
+    by iIntros "[#$ $]".
   Qed.
 
   Lemma subtype_tctx_incl E L p ty1 ty2 :
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 3d5faf02..be386813 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -13,7 +13,12 @@ Section uniq_bor.
   Program Definition uniq_bor (κ:lft) (ty:type) :=
     {| ty_size := 1;
        (* We quantify over [P]s so that the Proper lemma
-          (wrt. subtyping) works without an update. *)
+          (wrt. subtyping) works without an update.
+
+          An obvious alternative definition would be to allow
+          an update in the ownership here, i.e. `|={lftE}=> &{κ} P`.
+          The trouble with this definition is that bor_unnest as proven is too
+          weak. The original unnesting with open borrows was strong enough. *)
        ty_own tid vl :=
          (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
        ty_shr κ' tid l :=
-- 
GitLab