From e17bb1db997ed341c51fdbf23028ec34bf4429c0 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 16 Jul 2021 14:05:17 +0200
Subject: [PATCH] Ensure `Frame` instances are not tried before `frame_here`

---
 CHANGELOG.md                     |  2 ++
 iris/proofmode/frame_instances.v | 56 ++++++++++++++++++--------------
 2 files changed, 33 insertions(+), 25 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 27839101b..49a78c044 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 * `iMod`/`iModIntro` show proper error messages when they fail due to mask
   mismatches. To support this, the proofmode typeclass `FromModal` now takes an
   additional pure precondition.
+* Fix performance of `iFrame` in logics without `BiAffine`. (by Paolo G.
+  Giarrusso, BedRock Systems)
 
 **Changes in `bi`:**
 
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 178576f4d..3246c61e1 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -19,6 +19,12 @@ Section bi.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 (* Frame *)
+(**
+When framing [R] against itself, we leave [True] if possible (via
+[frame_here_absorbing] or [frame_affinely_here_absorbing]) since it is a weaker
+goal. Otherwise we leave [emp] via [frame_here].
+Only if all those options fail, we start decomposing [R], via instances like
+[frame_exist]. To ensure that, all other instances must have priority > 1. *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
 Proof. intros. by rewrite /Frame intuitionistically_if_elim sep_elim_l. Qed.
 Global Instance frame_here p R : Frame p R R emp | 1.
@@ -36,7 +42,7 @@ Proof.
 Qed.
 
 Global Instance frame_here_pure_persistent a φ Q :
-  FromPure a Q φ → Frame true ⌜φ⌝ Q emp.
+  FromPure a Q φ → Frame true ⌜φ⌝ Q emp | 2.
 Proof.
   rewrite /FromPure /Frame /= => <-. rewrite right_id.
   by rewrite -affinely_affinely_if intuitionistically_affinely.
@@ -44,7 +50,7 @@ Qed.
 Global Instance frame_here_pure a φ Q :
   FromPure a Q φ →
   TCOr (TCEq a false) (BiAffine PROP) →
-  Frame false ⌜φ⌝ Q emp.
+  Frame false ⌜φ⌝ Q emp | 2. (* Same prio as default. *)
 Proof.
   rewrite /FromPure /Frame => <- [->|?] /=.
   - by rewrite right_id.
@@ -62,13 +68,13 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
 Proof. by rewrite /MakeEmbed. Qed.
 
 Global Instance frame_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
-  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
+  Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
   rewrite embed_sep embed_intuitionistically_if_2 => //.
 Qed.
 Global Instance frame_pure_embed `{BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
-  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
+  Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q' | 2. (* Same prio as default. *)
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
 Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
@@ -102,20 +108,20 @@ Qed.
 Global Instance frame_big_sepL_cons {A} p (Φ : nat → A → PROP) R Q l x l' :
   IsCons l x l' →
   Frame p R (Φ 0 x ∗ [∗ list] k ↦ y ∈ l', Φ (S k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
 Proof. rewrite /IsCons=>->. by rewrite /Frame big_sepL_cons. Qed.
 Global Instance frame_big_sepL_app {A} p (Φ : nat → A → PROP) R Q l l1 l2 :
   IsApp l l1 l2 →
   Frame p R (([∗ list] k ↦ y ∈ l1, Φ k y) ∗
            [∗ list] k ↦ y ∈ l2, Φ (length l1 + k) y) Q →
-  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q.
+  Frame p R ([∗ list] k ↦ y ∈ l, Φ k y) Q | 2. (* Same prio as default. *)
 Proof. rewrite /IsApp=>->. by rewrite /Frame big_sepL_app. Qed.
 
 Global Instance frame_big_sepL2_cons {A B} p (Φ : nat → A → B → PROP)
     R Q l1 x1 l1' l2 x2 l2' :
   IsCons l1 x1 l1' → IsCons l2 x2 l2' →
   Frame p R (Φ 0 x1 x2 ∗ [∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2) Q →
-  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
+  Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q. (* Default prio > 1. *)
 Proof. rewrite /IsCons=>-> ->. by rewrite /Frame big_sepL2_cons. Qed.
 Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
     R Q l1 l1' l1'' l2 l2' l2'' :
@@ -127,7 +133,7 @@ Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
 Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
   Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
-  Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q.
+  Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
 Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
 
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
@@ -192,7 +198,7 @@ Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
 Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
 
 Global Instance frame_wand p R P1 P2 Q2 :
-  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2).
+  Frame p R P2 Q2 → Frame p R (P1 -∗ P2) (P1 -∗ Q2) | 2.
 Proof.
   rewrite /Frame=> ?. apply wand_intro_l.
   by rewrite assoc (comm _ P1) -assoc wand_elim_r.
@@ -207,7 +213,7 @@ Proof. by rewrite /MakeAffinely. Qed.
 
 Global Instance frame_affinely p R P Q Q' :
   TCOr (TCEq p true) (Affine R) →
-  Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
+  Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
     by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
@@ -230,7 +236,7 @@ Global Instance make_intuitionistically_default P :
 Proof. by rewrite /MakeIntuitionistically. Qed.
 
 Global Instance frame_intuitionistically R P Q Q' :
-  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q'.
+  Frame true R P Q → MakeIntuitionistically Q Q' → Frame true R (□ P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeIntuitionistically=> <- <- /=.
   rewrite -intuitionistically_sep_2 intuitionistically_idemp //.
@@ -247,7 +253,7 @@ Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 10
 Proof. by rewrite /MakeAbsorbingly. Qed.
 
 Global Instance frame_absorbingly p R P Q Q' :
-  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q'.
+  Frame p R P Q → MakeAbsorbingly Q Q' → Frame p R (<absorb> P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakeAbsorbingly=> <- <- /=. by rewrite absorbingly_sep_r.
 Qed.
@@ -264,7 +270,7 @@ Global Instance make_persistently_default P :
 Proof. by rewrite /MakePersistently. Qed.
 
 Global Instance frame_persistently R P Q Q' :
-  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q'.
+  Frame true R P Q → MakePersistently Q Q' → Frame true R (<pers> P) Q' | 2. (* Same prio as default. *)
 Proof.
   rewrite /Frame /MakePersistently=> <- <- /=.
   rewrite -persistently_and_intuitionistically_sep_l.
@@ -273,20 +279,20 @@ Proof.
 Qed.
 
 Global Instance frame_exist {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x).
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∃ x, Φ x) (∃ x, Ψ x) | 2.
 Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
 Global Instance frame_texist {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x).
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∃.. x, Φ x) (∃.. x, Ψ x) | 2.
 Proof. rewrite /Frame !bi_texist_exist. apply frame_exist. Qed.
 Global Instance frame_forall {A} p R (Φ Ψ : A → PROP) :
-  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x).
+  (∀ a, Frame p R (Φ a) (Ψ a)) → Frame p R (∀ x, Φ x) (∀ x, Ψ x) | 2.
 Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
 Global Instance frame_tforall {TT : tele} p R (Φ Ψ : TT → PROP) :
-  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x).
+  (∀ x, Frame p R (Φ x) (Ψ x)) → Frame p R (∀.. x, Φ x) (∀.. x, Ψ x) | 2.
 Proof. rewrite /Frame !bi_tforall_forall. apply frame_forall. Qed.
 
 Global Instance frame_impl_persistent R P1 P2 Q2 :
-  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2).
+  Frame true R P2 Q2 → Frame true R (P1 → P2) (P1 → Q2) | 2.
 Proof.
   rewrite /Frame /= => ?. apply impl_intro_l.
   by rewrite -persistently_and_intuitionistically_sep_l assoc (comm _ P1) -assoc impl_elim_r
@@ -294,7 +300,7 @@ Proof.
 Qed.
 Global Instance frame_impl R P1 P2 Q2 :
   Persistent P1 → Absorbing P1 →
-  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2).
+  Frame false R P2 Q2 → Frame false R (P1 → P2) (P1 → Q2). (* Default prio > 1 *)
 Proof.
   rewrite /Frame /==> ???. apply impl_intro_l.
   rewrite {1}(persistent P1) persistently_and_intuitionistically_sep_l assoc.
@@ -305,7 +311,7 @@ Qed.
 Global Instance frame_eq_embed `{!BiEmbed PROP PROP', !BiInternalEq PROP,
     !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
     p P Q (Q' : PROP') {A : ofe} (a b : A) :
-  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
+  Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'. (* Default prio > 1 *)
 Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
 
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
@@ -318,24 +324,24 @@ Proof. by rewrite /MakeLaterN. Qed.
 
 Global Instance frame_later p R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true 1 R' R) →
-  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'.
+  Frame p R P Q → MakeLaterN 1 Q Q' → Frame p R' (▷ P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite later_intuitionistically_if_2 later_sep.
 Qed.
 Global Instance frame_laterN p n R R' P Q Q' :
   TCNoBackTrack (MaybeIntoLaterN true n R' R) →
-  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'.
+  Frame p R P Q → MakeLaterN n Q Q' → Frame p R' (▷^n P) Q'. (* Default prio > 1 *)
 Proof.
   rewrite /Frame /MakeLaterN /MaybeIntoLaterN=>-[->] <- <-.
   by rewrite laterN_intuitionistically_if_2 laterN_sep.
 Qed.
 
 Global Instance frame_bupd `{BiBUpd PROP} p R P Q :
-  Frame p R P Q → Frame p R (|==> P) (|==> Q).
+  Frame p R P Q → Frame p R (|==> P) (|==> Q) | 2.
 Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
 Global Instance frame_fupd `{BiFUpd PROP} p E1 E2 R P Q :
-  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
+  Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 2.
 Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
 
 Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
@@ -344,7 +350,7 @@ Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
 Proof. by rewrite /MakeExcept0. Qed.
 
 Global Instance frame_except_0 p R P Q Q' :
-  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
+  Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q' | 2. (* Same prio as default *)
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
   by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
-- 
GitLab