From 7a487963933779a95fe917640a45f1215d7e9ac2 Mon Sep 17 00:00:00 2001
From: Hai Dang <hai@bedrocksystems.com>
Date: Mon, 5 Jun 2023 11:19:38 +0200
Subject: [PATCH] Update dependencies

---
 coq-lambda-rust.opam                | 2 +-
 theories/lifetime/frac_borrow.v     | 4 +++-
 theories/lifetime/lifetime.v        | 5 +++++
 theories/lifetime/lifetime_sig.v    | 6 +++---
 theories/lifetime/model/primitive.v | 8 ++++----
 theories/typing/lft_contexts.v      | 6 +++---
 theories/typing/lib/brandedvec.v    | 6 ++++--
 7 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 472a350a..228746ee 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2023-05-07.0.9cf7aca0") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-06-05.0.4b355a65") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index 795a764b..a0b313e2 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -103,7 +103,9 @@ Section frac_bor.
     ↑lftN ⊆ E → ⎡lft_ctx⎤ -∗ &{κ}P ={E}=∗ &frac{κ}φ.
   Proof.
     iIntros (?) "#? ?". rewrite [P]as_fractional. iApply bor_fracture'=>//.
-    iIntros "!> !> %%". by rewrite fractional -(bi.iff_refl True%I).
+    iIntros "!> !> %%".
+    assert (Fractional φ). { by apply : as_fractional_fractional. }
+    by rewrite fractional -(bi.iff_refl True%I).
   Qed.
 
   Lemma frac_bor_acc `{LatBottom Lat} φ E q κ :
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index b9bd9420..7a260b4e 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -1,4 +1,5 @@
 From orc11 Require Export base.
+Require Import iris.bi.lib.fractional.
 From lrust.lifetime Require Export lifetime_sig.
 From lrust.lifetime.model Require definitions primitive accessors faking borrow
      borrow_sep reborrow creation in_at_borrow.
@@ -32,6 +33,10 @@ Section derived.
 Context `{!invGS Σ, !lftG Σ Lat userE}.
 Implicit Types κ : lft.
 
+(* TODO: upstream *)
+Global Instance lft_mul_fractional q κ : Fractional (λ q', (q * q').[κ])%I.
+Proof. intros ??. by rewrite Qp.mul_add_distr_l lft_tok_fractional. Qed.
+
 Lemma lft_create E `{LatBottom Lat} :
   ↑lftN ⊆ E →
    ⎡lft_ctx⎤ ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={↑lftN ∪ userE}[userE]▷=∗ [†κ]).
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c41ee4eb..958cb00d 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -110,9 +110,9 @@ Module Type lifetime_sig.
   Global Declare Instance lft_tok_fractional κ : Fractional (λ q, q.[κ])%I.
   Global Declare Instance lft_tok_as_fractional κ q :
     AsFractional q.[κ] (λ q, q.[κ])%I q.
-  Global Declare Instance frame_lft_tok p κ q1 q2 RES :
-    FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-    Frame p q1.[κ] q2.[κ] RES | 5.
+  Global Declare Instance frame_lft_tok p κ q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p q1.[κ] q2.[κ] q.[κ] | 5.
 
   Global Declare Instance positive_to_lft_inj : Inj eq eq positive_to_lft.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 2df819b8..e9f6bbd2 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -325,10 +325,10 @@ Qed.
 Global Instance lft_tok_as_fractional κ q :
   AsFractional (q.[κ]) (λ q, q.[κ])%I q.
 Proof. split; [done|apply _]. Qed.
-Global Instance frame_lft_tok p κ q1 q2 RES :
-  FrameFractionalHyps p q1.[κ] (λ q, q.[κ])%I RES q1 q2 →
-  Frame p q1.[κ] q2.[κ] RES | 5.
-Proof. apply: frame_fractional. Qed.
+Global Instance frame_lft_tok p κ q1 q2 q :
+  FrameFractionalQp q1 q2 q →
+  Frame p q1.[κ] q2.[κ] q.[κ] | 5.
+Proof. apply: (frame_fractional (λ q, q.[κ])%I). Qed.
 
 Lemma lft_tok_split_obj `{LatBottom Lat bot} q1 q2 κ :
   (q1 + q2).[κ] -∗ q1.[κ] ∗ <obj> q2.[κ].
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 7e28f6f8..3fcb7872 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -96,9 +96,9 @@ Section lft_contexts.
   Global Instance llctx_interp_as_fractional qmax L q :
     AsFractional (llctx_interp_noend qmax L q) (llctx_interp_noend qmax L) q.
   Proof. split; first done. apply _. Qed.
-  Global Instance frame_llctx_interp p qmax L q1 q2 RES :
-    FrameFractionalHyps p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L) RES q1 q2 →
-    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2) RES | 5.
+  Global Instance frame_llctx_interp p qmax L q1 q2 q :
+    FrameFractionalQp q1 q2 q →
+    Frame p (llctx_interp_noend qmax L q1) (llctx_interp_noend qmax L q2) (llctx_interp_noend qmax L q) | 5.
   Proof. apply: frame_fractional. Qed.
 
   Global Instance llctx_interp_permut qmax :
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 4c7d6a16..d2d8fc0f 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -46,7 +46,8 @@ Section brandedvec.
     iMod (bor_share brandvecN with "Hghost") as "Hghost"; first solve_ndisj.
     iMod (bor_persistent with "LFT Hown Hκ") as "[> % $]"; first solve_ndisj.
     subst. iExists n. iFrame.
-    by iApply (bor_fracture with "LFT"); first solve_ndisj.
+    by iApply (bor_fracture with "LFT");
+      [apply fractional.fractional_as_fractional, _|solve_ndisj|].
   Qed.
   Next Obligation.
     iIntros (ty ?? tid l) "#H⊑ H".
@@ -93,7 +94,8 @@ Section brandedvec.
     iMod (bor_persistent with "LFT Hghost Hκ") as "[>Hghost $]"; first solve_ndisj.
     iDestruct "Hghost" as (m) "[Hghost %]". subst vl.
     iExists m. iFrame.
-    by iApply (bor_fracture with "LFT"); first solve_ndisj.
+    by iApply (bor_fracture with "LFT");
+      [apply fractional.fractional_as_fractional, _|solve_ndisj|].
   Qed.
   Next Obligation.
     iIntros (ty ?? tid l) "#H⊑ H".
-- 
GitLab