From bb6452359c6f72091f89aa8f2bf72cb8d9064b6a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2022 11:05:18 +0200
Subject: [PATCH] Make sure that `Make` instances are consistent and "constant
 time".

---
 iris/proofmode/class_instances_make.v | 82 +++++++++++++++++++--------
 iris/proofmode/classes_make.v         |  8 +++
 tests/proofmode.v                     |  4 --
 3 files changed, 65 insertions(+), 29 deletions(-)

diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index 9ccd7acca..85528ee68 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -8,6 +8,29 @@ Section class_instances_make.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
 
+(** Affine *)
+Global Instance bi_affine_quick_affine P : BiAffine PROP → QuickAffine P.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance False_quick_affine : @QuickAffine PROP False.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance emp_quick_affine : @QuickAffine PROP emp.
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance affinely_quick_affine P : QuickAffine (<affine> P).
+Proof. rewrite /QuickAffine. apply _. Qed.
+Global Instance intuitionistically_quick_affine P : QuickAffine (â–¡ P).
+Proof. rewrite /QuickAffine. apply _. Qed.
+
+(** Absorbing *)
+Global Instance bi_affine_quick_absorbing P : BiAffine PROP → QuickAbsorbing P.
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance pure_quick_absorbing φ : @QuickAbsorbing PROP ⌜ φ ⌝.
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance absorbingly_quick_absorbing P : QuickAbsorbing (<absorb> P).
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+Global Instance persistently_quick_absorbing P : QuickAbsorbing (<pers> P).
+Proof. rewrite /QuickAbsorbing. apply _. Qed.
+
+(** Embed *)
 Global Instance make_embed_pure `{BiEmbed PROP PROP'} φ :
   KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
 Proof. apply embed_pure. Qed.
@@ -18,46 +41,63 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
   MakeEmbed P ⎡P⎤ | 100.
 Proof. by rewrite /MakeEmbed. Qed.
 
+(** Sep *)
 Global Instance make_sep_emp_l P : KnownLMakeSep emp P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_sep_emp_r P : KnownRMakeSep P emp P.
 Proof. apply right_id, _. Qed.
-Global Instance make_sep_true_l P : Absorbing P → KnownLMakeSep True P P.
-Proof. intros. apply True_sep, _. Qed.
-Global Instance make_sep_true_r P : Absorbing P → KnownRMakeSep P True P.
-Proof. intros. by rewrite /KnownRMakeSep /MakeSep sep_True. Qed.
+Global Instance make_sep_true_l P : QuickAbsorbing P → KnownLMakeSep True P P.
+Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply True_sep. Qed.
+Global Instance make_sep_true_r P : QuickAbsorbing P →  KnownRMakeSep P True P.
+Proof. rewrite /QuickAbsorbing /KnownLMakeSep /MakeSep=> ?. by apply sep_True. Qed.
 Global Instance make_sep_default P Q : MakeSep P Q (P ∗ Q) | 100.
 Proof. by rewrite /MakeSep. Qed.
 
+(** And *)
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_and_true_r P : KnownRMakeAnd P True P.
 Proof. by rewrite /KnownRMakeAnd /MakeAnd right_id. Qed.
-Global Instance make_and_emp_l P : Affine P → KnownLMakeAnd emp P P.
-Proof. intros. by rewrite /KnownLMakeAnd /MakeAnd emp_and. Qed.
-Global Instance make_and_emp_r P : Affine P → KnownRMakeAnd P emp P.
-Proof. intros. by rewrite /KnownRMakeAnd /MakeAnd and_emp. Qed.
+Global Instance make_and_emp_l P : QuickAffine P → KnownLMakeAnd emp P P.
+Proof. apply emp_and. Qed.
+Global Instance make_and_emp_r P : QuickAffine P → KnownRMakeAnd P emp P.
+Proof. apply and_emp. Qed.
 Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
 Proof. by rewrite /MakeAnd. Qed.
 
+(** Or *)
 Global Instance make_or_true_l P : KnownLMakeOr True P True.
 Proof. apply left_absorb, _. Qed.
 Global Instance make_or_true_r P : KnownRMakeOr P True True.
 Proof. by rewrite /KnownRMakeOr /MakeOr right_absorb. Qed.
-Global Instance make_or_emp_l P : Affine P → KnownLMakeOr emp P emp.
-Proof. intros. by rewrite /KnownLMakeOr /MakeOr emp_or. Qed.
-Global Instance make_or_emp_r P : Affine P → KnownRMakeOr P emp emp.
-Proof. intros. by rewrite /KnownRMakeOr /MakeOr or_emp. Qed.
+Global Instance make_or_emp_l P : QuickAffine P → KnownLMakeOr emp P emp.
+Proof. apply emp_or. Qed.
+Global Instance make_or_emp_r P : QuickAffine P → KnownRMakeOr P emp emp.
+Proof. apply or_emp. Qed.
 Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
 Proof. by rewrite /MakeOr. Qed.
 
-Global Instance make_affinely_emp : @KnownMakeAffinely PROP emp emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_emp. Qed.
+(** Affinely *)
 Global Instance make_affinely_True : @KnownMakeAffinely PROP True emp | 0.
-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
+-Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp. Qed.
+Global Instance make_affinely_affine P :
+  QuickAffine P → MakeAffinely P P | 99.
+Proof. apply affine_affinely. Qed.
 Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
 Proof. by rewrite /MakeAffinely. Qed.
 
+(** Absorbingly *)
+Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
+Proof.
+  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly -absorbingly_emp_True.
+Qed.
+Global Instance make_absorbingly_absorbing P :
+  QuickAbsorbing P → MakeAbsorbingly P P | 99.
+Proof. apply absorbing_absorbingly. Qed.
+Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
+Proof. by rewrite /MakeAbsorbingly. Qed.
+
+(** Intuitionistically *)
 Global Instance make_intuitionistically_emp :
   @KnownMakeIntuitionistically PROP emp emp | 0.
 Proof.
@@ -74,16 +114,7 @@ Global Instance make_intuitionistically_default P :
   MakeIntuitionistically P (â–¡ P) | 100.
 Proof. by rewrite /MakeIntuitionistically. Qed.
 
-Global Instance make_absorbingly_emp : @KnownMakeAbsorbingly PROP emp True | 0.
-Proof.
-  by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly
-     -absorbingly_emp_True.
-Qed.
-Global Instance make_absorbingly_True : @KnownMakeAbsorbingly PROP True True | 0.
-Proof. by rewrite /KnownMakeAbsorbingly /MakeAbsorbingly absorbingly_pure. Qed.
-Global Instance make_absorbingly_default P : MakeAbsorbingly P (<absorb> P) | 100.
-Proof. by rewrite /MakeAbsorbingly. Qed.
-
+(** Later *)
 Global Instance make_laterN_true n : @KnownMakeLaterN PROP n True True | 0.
 Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_True. Qed.
 Global Instance make_laterN_emp `{!BiAffine PROP} n :
@@ -92,6 +123,7 @@ Proof. by rewrite /KnownMakeLaterN /MakeLaterN laterN_emp. Qed.
 Global Instance make_laterN_default n P : MakeLaterN n P (â–·^n P) | 100.
 Proof. by rewrite /MakeLaterN. Qed.
 
+(** Except-0 *)
 Global Instance make_except_0_True : @KnownMakeExcept0 PROP True True.
 Proof. by rewrite /KnownMakeExcept0 /MakeExcept0 except_0_True. Qed.
 Global Instance make_except_0_default P : MakeExcept0 P (â—‡ P) | 100.
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index a0d8f1342..7d0bda7a2 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -39,6 +39,14 @@ that would have this behavior. *)
 From iris.bi Require Export bi.
 From iris.prelude Require Import options.
 
+(** Aliases for [Affine] and [Absorbing], but the instances are severely
+restricted. They only inspect the top-level symbol or check if the whole BI
+is affine. *)
+Class QuickAffine {PROP : bi} (P : PROP) := quick_affine : Affine P.
+Global Hint Mode QuickAffine + ! : typeclass_instances.
+Class QuickAbsorbing {PROP : bi} (P : PROP) := quick_absorbing : Absorbing P.
+Global Hint Mode QuickAbsorbing + ! : typeclass_instances.
+
 Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Global Arguments MakeEmbed {_ _ _} _%I _%I.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index ea515a6b8..8577e06e7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -51,10 +51,6 @@ Proof.
   - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
-Lemma demo_3 P1 P2 P3 :
-  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
-Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
-
 Lemma test_pure_space_separated P1 :
   <affine> ⌜True⌝ ∗ P1 -∗ P1.
 Proof.
-- 
GitLab