.gitignore

@@ -23,3 +23,5 @@ Makefile.coq.conf
 Makefile.package.*
 .Makefile.package.*
 _opam
+_build
+*.install

.gitlab-ci.yml

@@ -67,6 +67,14 @@ build-coq.8.19.1-mr:
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
 
+# Also ensure Dune works.
+build-coq.8.19.1-dune:
+  <<: *template
+  <<: *branches_and_mr
+  variables:
+    OPAM_PINS: "coq version 8.19.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
+
 # The oldest version runs in MRs, without name mangling.
 build-coq.8.18.0:
   <<: *template

CHANGELOG.md

@@ -5,10 +5,35 @@ lemma.
 
 ## Iris master
 
+**Changes in `algebra`:**
+* Add lemmas `big_opS_gset_to_gmap`, `big_opS_gset_to_gmap_L` which rewrite
+  between `gset_to_gmap` and big set ops of singleton maps.  (by Isaac van
+  Bakel)
+
+**Changes in `proofmode`:**
+
+* Remove the `*` specialization pattern. This pattern has been deprecated and a
+  no-op since 2017. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/41.
+* Improve the error message of `iInv` in case the goal does not support
+  invariant opening.
+* Change `iInduction` to always generate a magic wand instead of sometimes
+  generating an implication for reverted hypotheses.
+
 **Changes in `base_logic`:**
 
 * Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
   non-atomic invariant tokens. (by Benjamin Peters)
+* Add instances `big_sepL_flip_mono'`, `big_sepM_flip_mono'`, etc., which are
+  wrappers of instances `big_sep*_mono'` for `flip (⊢)` instead of `(⊢)`. (by
+  Yusuke Matsushita)
+
+**Changes in `heap_lang`:**
+
+* Make `wp_cmpxchg_fail` work when the points-to is in the persistent context.
+
+**Infrastructure:**
+
+* Add support for compiling the packages with dune. (by Rodolphe Lepigre) 
 
 ## Iris 4.2.0 (2024-04-12)
 

Makefile

@@ -3,6 +3,12 @@ all: Makefile.coq
 	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
 # Permit local customization
 -include Makefile.local
 

Makefile.coq.local

@@ -29,7 +29,7 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
 # These versions of Coq are known to have different output so we don't test them.
 # Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
 # Make sure to recognize both 8.$NUM.0 and 8.$NUM+alpha.
-COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20)[.+]" -q && echo 1)
+COQ_NOREF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(16|17|18|20|21)[.+]" -q && echo 1)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'

_CoqProject

@@ -10,6 +10,8 @@
 -Q iris_heap_lang iris.heap_lang
 -Q iris_unstable iris.unstable
 -Q iris_deprecated iris.deprecated
+
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures

coq-iris.opam

@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2024-04-19.0.e40779e3") | (= "dev") }
+  "coq-stdpp" { (= "dev.2024-06-17.2.2bcaf3c5") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -notation-overridden
+     -w -redundant-canonical-projection
+     -w -unknown-warning
+     -w -argument-scope-delimiter)))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)

iris/bi/big_op.v

@@ -130,6 +130,10 @@ Section sep_list.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opL (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_sepL_mono; intros; apply Hf. Qed.
+  Global Instance big_sepL_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
+           (big_opL (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepL_id_mono' :
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep PROP) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
@@ -606,6 +610,11 @@ Section sep_list2.
       ==> (=) ==> (=) ==> (⊢))
            (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
   Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepL2_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
+            ==> (=) ==> (=) ==> flip (⊢))
+           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepL2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
       ==> (=) ==> (=) ==> (⊣⊢))
@@ -1352,6 +1361,10 @@ Section sep_map.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_sepM_mono; intros; apply Hf. Qed.
+  Global Instance big_sepM_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
+           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
@@ -2082,9 +2095,15 @@ Section map2.
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
       ==> (=) ==> (=) ==> (⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepM2_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
+            ==> (=) ==> (=) ==> flip (⊢))
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepM2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
-      ==> (=) ==> (=) ==> (⊣⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+            ==> (=) ==> (=) ==> (⊣⊢))
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
 
   (** Shows that some property [P] is closed under [big_sepM2]. Examples of [P]
@@ -2592,6 +2611,10 @@ Section gset.
   Global Instance big_sepS_mono' :
     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
+  Global Instance big_sepS_flip_mono' :
+    Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
+           (big_opS (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
@@ -2931,6 +2954,10 @@ Section gmultiset.
   Global Instance big_sepMS_mono' :
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.
+  Global Instance big_sepMS_flip_mono' :
+     Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
+            (big_opMS (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).

iris/dune

+(include_subdirs qualified)
+(coq.theory
+ (name iris)
+ (package coq-iris)
+ (theories Ltac2 stdpp))

iris/proofmode/coq_tactics.v

@@ -175,11 +175,11 @@ Proof.
 Qed.
 
 Lemma tac_pure_revert Δ φ P Q :
-  FromAffinely P ⌜ φ ⌝ →
+  MakeAffinely ⌜ φ ⌝ P →
   envs_entails Δ (P -∗ Q) →
   (φ → envs_entails Δ Q).
 Proof.
-  rewrite /FromAffinely envs_entails_unseal. intros <- -> ?.
+  rewrite /MakeAffinely envs_entails_unseal. intros <- -> ?.
   by rewrite pure_True // affinely_True_emp left_id.
 Qed.
 
@@ -474,9 +474,14 @@ Proof. by rewrite envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
-Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
-  IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q) | 1.
-Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
+Global Instance into_ih_impl (φ ψ : Prop) Δ P Q :
+  MakeAffinely ⌜ φ ⌝ P →
+  IntoIH ψ Δ Q → IntoIH (φ → ψ) Δ (P -∗ Q) | 1.
+Proof.
+  rewrite /IntoIH /MakeAffinely=> <- HΔ ?.
+  rewrite -persistent_impl_wand_affinely. apply impl_intro_l, pure_elim_l. auto.
+Qed.
+
 (** The instances [into_ih_Forall] and [into_ih_Forall2] are used to support
 induction principles for mutual inductive types such as finitely branching trees:
 

iris/proofmode/ltac_tactics.v

@@ -605,7 +605,7 @@ Ltac iForallRevert x :=
   | Prop =>
      revert x; first
        [eapply tac_pure_revert;
-         [tc_solve (* [FromAffinely], should never fail *)
+         [tc_solve (* [MakeAffinely], should never fail *)
          |]
        |err x]
   | _ =>
@@ -813,9 +813,6 @@ Ltac iSpecializePat_go H1 pats :=
   let Δ := iGetCtx in
   lazymatch pats with
     | [] => idtac
-    | SForall :: ?pats =>
-       idtac "[IPM] The * specialization pattern is deprecated because it is applied implicitly.";
-       iSpecializePat_go H1 pats
     | SIdent ?H2 [] :: ?pats =>
        (* If we not need to specialize [H2] we can avoid a lot of unncessary
        context manipulation. *)
@@ -974,7 +971,7 @@ Fixpoint use_tac_specialize_intuitionistic_helper {M}
     (Δ : envs M) (pats : list spec_pat) : bool :=
   match pats with
   | [] => false
-  | (SForall | SPureGoal _) :: pats =>
+  | SPureGoal _ :: pats =>
      use_tac_specialize_intuitionistic_helper Δ pats
   | SAutoFrame _ :: _ => true
   | SIdent H _ :: pats =>
@@ -1992,7 +1989,9 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
   end;
     [tc_solve ||
      let I := match goal with |- ElimInv _ ?I  _ _ _ _ _ => I end in
-     fail "iInv: cannot eliminate invariant" I
+     fail "iInv: cannot open invariant" I "in the current goal"
+       "(the goal should be a fancy update or WP,"
+       "or another modality that supports invariant opening)"
     |iSolveSideCondition
     |let R := fresh in intros R; pm_reduce;
      (* Now we are left proving [envs_entails Δ'' R]. *)

iris/proofmode/spec_patterns.v

@@ -13,7 +13,6 @@ Record spec_goal := SpecGoal {
 }.
 
 Inductive spec_pat :=
-  | SForall : spec_pat
   | SIdent : ident → list spec_pat → spec_pat
   | SPureGoal (perform_done : bool) : spec_pat
   | SGoal : spec_goal → spec_pat
@@ -67,7 +66,6 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
   | TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
   | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
   | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
-  | TForall :: ts => parse_go ts (StPat SForall :: k)
   | _ => None
   end
 with parse_goal (ts : list token)

iris_deprecated/dune

+(include_subdirs qualified)
+(coq.theory
+ (name iris.deprecated)
+ (package coq-iris-deprecated)
+ (theories stdpp iris))

iris_heap_lang/dune

+(include_subdirs qualified)
+(coq.theory
+ (name iris.heap_lang)
+ (package coq-iris-heap-lang)
+ (theories stdpp iris))

iris_heap_lang/proofmode.v

@@ -378,8 +378,8 @@ Proof.
   * iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
   * by apply sep_mono_r, wand_mono.
 Qed.
-Lemma tac_twp_load Δ s E i K b l q v Φ :
-  envs_lookup i Δ = Some (b, l ↦{q} v)%I →
+Lemma tac_twp_load Δ s E i K b l dq v Φ :
+  envs_lookup i Δ = Some (b, l ↦{dq} v)%I →
   envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
 Proof.
@@ -504,28 +504,33 @@ Proof.
     apply sep_mono_r. apply wand_mono; auto.
 Qed.
 
-Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
+Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K b l dq v v1 v2 Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
-  envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
+  envs_lookup i Δ' = Some (b, l ↦{dq} v)%I →
   v ≠ v1 → vals_compare_safe v v1 →
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
-  rewrite envs_entails_unseal=> ?????.
+  rewrite envs_entails_unseal=> ???? Hi.
   rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_cmpxchg_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
-  by apply later_mono, sep_mono_r, wand_mono.
+  apply later_mono. destruct b; simpl.
+  - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
+  - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl".
 Qed.
-Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
-  envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+Lemma tac_twp_cmpxchg_fail Δ s E i K b l dq v v1 v2 Φ :
+  envs_lookup i Δ = Some (b, l ↦{dq} v)%I →
   v ≠ v1 → vals_compare_safe v v1 →
   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite envs_entails_unseal. intros. rewrite -twp_bind.
+  rewrite envs_entails_unseal. intros ??? Hi. rewrite -twp_bind.
   eapply wand_apply; first by apply wand_entails, twp_cmpxchg_fail.
   (* [//] solves some evars and enables further simplification. *)
-  rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
+  rewrite envs_lookup_split /= // /=.
+  destruct b; simpl.
+  - iIntros "[#$ He]". iIntros "_". iApply Hi. iApply "He". iFrame "#".
+  - iIntros "[$ He]". iIntros "Hl". iApply Hi. iApply "He". iFrame "Hl".
 Qed.
 
 Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :

iris_unstable/dune

+(include_subdirs qualified)
+(coq.theory
+ (name iris.unstable)
+ (package coq-iris-unstable)
+ (theories stdpp iris iris.heap_lang))

tests/bi.v

@@ -17,6 +17,20 @@ Proof.
   pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
 Abort.
 
+(** Rewriting on big ops. *)
+Goal ∀ {PROP : bi} {l : list nat} {Φ Ψ} {R : PROP},
+  (∀ k i, Φ k i ⊢ Ψ k i) → (R ⊢ [∗ list] k↦i ∈ l, Φ k i) →
+  R ⊢ [∗ list] k↦i ∈ l, Ψ k i.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+Goal ∀ {PROP : bi} {m : gmap nat nat} {Φ Ψ} {R : PROP},
+  (∀ k i, Φ k i ⊢ Ψ k i) → (R ⊢ [∗ map] k↦i ∈ m, Φ k i) →
+  R ⊢ [∗ map] k↦i ∈ m, Ψ k i.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+Goal ∀ {PROP : bi} {m1 m2 : gmap nat nat} {Φ Ψ} {R : PROP},
+  (∀ k i j, Φ k i j ⊢ Ψ k i j) → (R ⊢ [∗ map] k↦i;j ∈ m1;m2, Φ k i j) →
+  R ⊢ [∗ map] k↦i;j ∈ m1;m2, Ψ k i j.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+
 (** Some basic tests to make sure patterns work in big ops. *)
 Definition big_sepM_pattern_value
     {PROP : bi} (m : gmap nat (nat * nat)) : PROP :=