WIP: arc typing proof

_CoqProject

@@ -21,6 +21,7 @@ theories/lang/new_delete.v
 theories/lang/swap.v
 theories/lang/lock.v
 theories/lang/spawn.v
+theories/lang/arc_cmra.v
 theories/lang/arc.v
 theories/typing/base.v
 theories/typing/lft_contexts.v

theories/typing/lib/arc.v

+From Coq.QArith Require Import Qcanon.
+
+From iris.proofmode Require Import tactics.
+From iris.algebra Require Import auth csum frac agree.
+From iris.bi Require Import fractional.
+
+From lrust.lang Require Import memcpy arc.
+From lrust.lifetime Require Import at_borrow.
+From lrust.typing Require Export type.
+From lrust.typing Require Import typing option.
+
+From gpfsl.gps Require Import middleware protocols.
+
+Set Default Proof Using "Type".
+
+Definition arcN := lrustN .@ "arc".
+Definition arc_invN := arcN .@ "inv".
+Definition arc_shrN := arcN .@ "shr".
+Definition arc_endN := arcN .@ "end".
+
+Section arc.
+  Context `{!typeG Σ, !arcG Σ}.
+  Local Notation vProp := (vProp Σ).
+
+  (* Preliminary definitions. *)
+  Let P1 ν q := (q.[ν])%I.
+  Instance P1_fractional ν : Fractional (P1 ν).
+  Proof. unfold P1. apply _. Qed.
+  Let P2 l n := (⎡ † l…(2 + n) ⎤ ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
+
+  Definition arc_persist tid ν (γs γw γsw : gname) (l : loc) (ty : type) : vProp  :=
+    (is_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN γs γw γsw l ∗
+     (* We use this disjunction, and not simply [ty_shr] here, *)
+     (*    because [weak_new] cannot prove ty_shr, even for a dead *)
+     (*    lifetime. *)
+     (ty.(ty_shr) ν tid (l +ₗ 2) ∨ [†ν]) ∗
+     □ (1.[ν] ={↑lftN ∪ ↑arc_endN,∅}▷=∗
+          [†ν] ∗ ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid ∗ ⎡ † l…(2 + ty.(ty_size)) ⎤))%I.
+
+  Global Instance arc_persist_ne tid ν γs γw γsw l n :
+    Proper (type_dist2 n ==> dist n) (arc_persist tid ν γs γw γsw l).
+  Proof.
+    unfold arc_persist, P1, P2. move => ???.
+    apply bi.sep_ne.
+    - apply is_arc_contractive; eauto. done.
+      solve_proper_core ltac:(fun _ => f_type_equiv || f_equiv).
+    - solve_proper_core ltac:(fun _ => exact: type_dist2_S || exact: type_dist2_dist ||
+                                     f_type_equiv || f_contractive || f_equiv).
+  Qed.
+
+  Lemma arc_persist_type_incl tid ν γs γw γsw l ty1 ty2:
+    type_incl ty1 ty2 -∗ arc_persist tid ν γs γw γsw l ty1 -∗ arc_persist tid ν γs γw γsw l ty2.
+  Proof.
+    iIntros "#(Heqsz & Hinclo & Hincls) #(?& Hs & Hvs)".
+    iDestruct "Heqsz" as %->. iFrame "#". iSplit.
+    - iDestruct "Hs" as "[?|?]"; last auto. iLeft. by iApply "Hincls".
+    - iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+      iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "[??]". iExists _.
+      iFrame. by iApply "Hinclo".
+  Qed.
+
+  Lemma arc_persist_send tid tid' ν γs γw γsw l ty `{!Send ty,!Sync ty} :
+    arc_persist tid ν γs γw γsw l ty -∗ arc_persist tid' ν γs γw γsw l ty.
+  Proof.
+    iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
+    iIntros "!# Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
+    iMod "H" as "($ & H & $)". iDestruct "H" as (vl) "?". iExists _.
+    by rewrite send_change_tid.
+  Qed.
+
+  (* Model of arc *)
+  (* The ty_own part of the arc type cointains either the
+     shared protocol or the full ownership of the
+     content. The reason is that get_mut does not have the
+     masks to rebuild the invariants. *)
+  Definition full_arc_own l ty tid : vProp :=
+    (l ↦ #1 ∗ (l +ₗ 1) ↦ #1 ∗ ⎡ † l…(2 + ty.(ty_size)) ⎤ ∗
+       ▷ (l +ₗ 2) ↦∗: ty.(ty_own) tid)%I.
+  Definition shared_arc_own l ty tid : vProp :=
+    (∃ γs γw γsw ν q, arc_persist tid ν γs γw γsw l ty ∗
+                       strong_arc q l γs γw γsw ∗ q.[ν])%I.
+  Lemma arc_own_share E l ty tid :
+    ↑lftN ⊆ E →
+    ⎡ lft_ctx ⎤ -∗ full_arc_own l ty tid ={E}=∗ shared_arc_own l ty tid.
+  Proof.
+    iIntros (?) "#LFT (Hl1 & Hl2 & H† & Hown)".
+    iMod (lft_create with "LFT") as (ν) "[Hν #Hν†]"=>//.
+    (* TODO: We should consider changing the statement of
+       bor_create to dis-entangle the two masks such that this is no
+      longer necessary. *)
+    iApply fupd_trans. iApply (fupd_mask_mono (↑lftN))=>//.
+    iMod (bor_create _ ν with "LFT Hown") as "[HP HPend]"=>//. iModIntro.
+    iMod (ty_share with "LFT HP Hν") as "[#? Hν]"; first solve_ndisj.
+    iMod (create_arc (P1 ν) (P2 l ty.(ty_size)) arc_invN with "Hl1 Hl2 Hν")
+      as (γ q') "(#? & ? & ?)".
+    iExists _, _, _. iFrame "∗#". iCombine "H†" "HPend" as "H".
+    iMod (inv_alloc arc_endN _ ([†ν] ∨ _)%I with "[H]") as "#INV";
+      first by iRight; iApply "H". iIntros "!> !# Hν".
+    iMod (inv_open with "INV") as "[[H†|[$ Hvs]] Hclose]";
+      [set_solver|iDestruct (lft_tok_dead with "Hν H†") as ">[]"|].
+    rewrite difference_union_distr_l_L difference_diag_L right_id_L
+            difference_disjoint_L; last solve_ndisj.
+    iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
+    iMod "H" as "#Hν". iMod ("Hvs" with "Hν") as "$". iIntros "{$Hν} !>".
+    iApply "Hclose". auto.
+  Qed.
+  
+End arc.
\ No newline at end of file