bump iris to 4.4.0

Makefile

@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0
+COQVERSION= 8.19.1 or-else 8.19.2 or-else 8.20.0 or-else 8.20.1 or-else 9.0.0 or-else 9.0.1 or-else 9.1.0
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)

builddep/coq-vst-on-iris-builddep.opam

@@ -25,10 +25,10 @@ bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE"
 
 depends: [
-  "coq" {>= "8.19.1" & <= "8.20.0"}
-  "coq-compcert" {>= "3.11"}
+  "coq" { (>= "8.19" ) }
+  "coq-iris" { (>= "4.4.0") }
+  "coq-compcert" {= "3.15"}
   "coq-vst-zlist" {>= "2.11"}
   "coq-flocq" {>= "4.1.0"}
-  "coq-iris" {="4.3.0"}
-  "coq-vst-ora" {="1.1"}
+  "coq-iris-ora" {(= "1.3.0") | (= "~dev")}
 ]

floyd/canon.v

@@ -157,7 +157,7 @@ Proof.
   induction H; simpl; f_equiv; done.
 Qed.
 
-#[global] Instance LOCALx_proper : Proper (equiv(Equiv := list.list_equiv(H := equivL)) ==> equiv ==> equiv) (LOCALx).
+#[global] Instance LOCALx_proper : Proper (equiv(Equiv := list_relations.list_equiv(H := equivL)) ==> equiv ==> equiv) (LOCALx).
 Proof.
   intros ??????.
   rewrite /LOCALx; f_equiv; last done.

floyd/closed_lemmas.v

@@ -126,7 +126,7 @@ Qed.
 Lemma closed_wrt_map_subst:
    forall id e `(Q: list (environ -d> A)),
          Forall (closed_wrt_vars (eq id)) Q ->
-          @equiv _ (list.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q.
+          @equiv _ (list_relations.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q.
 Proof.
 induction Q; intros.
 simpl; constructor.
@@ -139,7 +139,7 @@ Qed.
 Lemma closed_wrt_map_subst' `{!heapGS Σ}:
    forall id e (Q: list (environ -d> mpred)),
          Forall (closed_wrt_vars (eq id)) Q ->
-          @equiv _ (list.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q.
+          @equiv _ (list_relations.list_equiv(H:=discrete_fun_equiv)) (map (subst id e) Q) Q.
 Proof.
 intros.
 apply closed_wrt_map_subst. done.

ivst.md

@@ -6,15 +6,17 @@
 Install opam:
 
 ```(bash)
-opam switch create vst_on_iris ocaml-variants.4.14.1+options ocaml-option-flambda
+opam switch create ccris ocaml-variants.4.14.2+options ocaml-option-flambda
+eval $(opam env)
 ```
 
 Install dependencies:
 
 ```(bash)
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-opam pin add builddep/
+opam update
+opam pin add builddep/ -y
 ```
 
 Download submodules:
@@ -26,7 +28,7 @@ At this point, we use [`Makefile`](./Makefile)
 ```(bash)
 make
 ```
-Addtionally, to generate `_CoqProject`:
+Additionally, to generate `_CoqProject`:
 
 ```(bash)
 make _CoqProject

shared/dshare.v

@@ -30,9 +30,9 @@ Notation "" := (DfracOwn (Share share_top)) (in custom dfrac).
 
 Section dfrac.
 
-Context `{ST : ShareType}.
+Context {SI : sidx} `{ST : ShareType}.
 Set Warnings "-redundant-canonical-projection".
-  Canonical Structure dfracO := leibnizO dfrac.
+  Canonical Structure dfracO  := ofe.leibnizO dfrac.
 Set Warnings "redundant-canonical-projection".
 
   Implicit Types p q : share_car.
@@ -84,15 +84,18 @@ Set Warnings "redundant-canonical-projection".
   Lemma dfrac_op_own q p : DfracOwn p ⋅ DfracOwn q = DfracOwn (p ⋅ q).
   Proof. done. Qed.
 
+  (* Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances. *)
+
   Lemma dfrac_op_discarded :
     DfracDiscarded ⋅ DfracDiscarded = DfracDiscarded.
-  Proof. rewrite /op /dfrac_op_instance /= left_id //. Qed.
+  Proof. rewrite /op /dfrac_op_instance /=
+    (left_id _ _ (LeftId:=ucmra_unit_left_id)) //. Qed.
 
   Lemma dfrac_op_own_discarded q : DfracOwn q ⋅ DfracDiscarded = DfracBoth q.
-  Proof. rewrite /op /= right_id //. Qed.
+  Proof. rewrite /op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed.
 
   Lemma dfrac_op_both_discarded q : DfracBoth q ⋅ DfracDiscarded = DfracBoth q.
-  Proof. rewrite /op /= right_id //. Qed.
+  Proof. rewrite /op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) //. Qed.
 
   Lemma dfrac_included_eq dq dp : dq ≼ dp ↔ match dq, dp with
     | DfracOwn q, DfracOwn p | DfracOwn q, DfracBoth p | DfracBoth q, DfracBoth p => q ≼ p
@@ -144,9 +147,9 @@ Set Warnings "redundant-canonical-projection".
   Proof.
     apply: discrete_cancelable.
     intros [q1|q1] [q2|q2] ? [=]; simplify_eq/=; try done.
-    - by apply (share_cancelable _ 0) in H1 as ->.
+    - by apply (share_cancelable _ 0ᵢ) in H1 as ->.
     - destruct H as (? & J & ?).
-      apply (share_cancelable _ 0) in H1 as ->; try done.
+      apply (share_cancelable _ 0ᵢ) in H1 as ->; try done.
       rewrite J; hnf; eauto.
   Qed.
 
@@ -166,15 +169,15 @@ Set Warnings "redundant-canonical-projection".
   Proof.
     intros ??? ->%dfrac_full_exclusive H.
     destruct z; last done.
-    rewrite /op /cmra_op /= right_id in H; injection H as H.
+    rewrite /op /cmra_op /= (right_id _ _ (RightId:=ucmra_unit_right_id)) in H; injection H as H.
     symmetry in H; apply share_op_join in H as (? & ? & [=] & ? & J); subst.
     rewrite share_op_comm in J; apply share_op_top' in J as (_ & ->); done.
   Qed.
 
   Definition dfrac_ucmra_mixin : UcmraMixin dfrac.
   Proof.
     split; try done.
-    intros [|]; rewrite /op /dfrac_op_instance /= left_id //.
+    intros [|]; rewrite /op /dfrac_op_instance /= (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
   Qed.
 Set Warnings "-redundant-canonical-projection".
   Canonical Structure dfracUC := Ucmra dfrac dfrac_ucmra_mixin.
@@ -210,7 +213,7 @@ Set Warnings "redundant-canonical-projection".
     ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ ∃ sh, q = Share sh ∧ ~share_writable sh.
   Proof.
     rewrite /op /= /valid /=.
-    rewrite right_id //.
+    rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)) //.
   Qed.
 
   Definition readable_dfrac (dq : dfrac) :=
@@ -229,7 +232,7 @@ Set Warnings "redundant-canonical-projection".
   Qed.
 
   Global Instance dfrac_is_op q q1 q2 :
-    @IsOp shareR q q1 q2 →
+    @IsOp _ shareR q q1 q2 →
     IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
   Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
 
@@ -262,7 +265,7 @@ Set Warnings "redundant-canonical-projection".
     - inversion 1; hnf; auto.
     - intros ?? [?|?]; subst.
       + by left.
-      + right; destruct x; rewrite /op /= left_id //.
+      + right; destruct x; rewrite /op /= (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
     - intros ??? [?|?] [?|?]; subst; hnf; auto.
       right; destruct x; rewrite !dfrac_op_both_discarded //.
     - intros ??? [?|?]; subst; hnf; auto.

shared/share_alg.v

@@ -36,7 +36,7 @@ Inductive share_car `{ShareType} :=
 
 Section share.
 
-  Context `{ST : ShareType}.
+  Context {SI : sidx} `{ST : ShareType}.
 
   Lemma share_op_top' a b : share_op a share_top = Some b -> b = share_top /\ a = share_bot.
   Proof.

shared/shared.v

@@ -11,7 +11,7 @@ From iris.prelude Require Import options.
 
 Section shared.
 
-Context `{ST : ShareType}.
+Context {SI : sidx} `{ST : ShareType}.
 
 Definition readable_share' (s : shareO) := match s with Share sh => share_readable sh | _ => False end.
 
@@ -50,9 +50,9 @@ Local Instance shared_equiv : Equiv shared := λ x y,
 Definition shared_ofe_mixin : OfeMixin shared.
 Proof.
   split.
-  - destruct x, y; intuition; try split; try pose proof (H 0) as H'; try destruct H; try destruct H'; try done.
+  - destruct x, y; intuition; try split; try pose proof (H 0ᵢ) as H'; try destruct H; try destruct H'; try done.
     + intros n; specialize (H n); destruct H; done.
-    + apply O.
+    + apply 0ᵢ.
   - intros n; split; rewrite /dist /shared_dist.
     + intros x; destruct x; done.
     + intros [|] [|]; try done.
@@ -62,7 +62,7 @@ Proof.
       * by intros ->.
   - intros ?? [|] [|]; try done.
     intros [??]; split; first done.
-    eapply dist_lt; eauto.
+    eapply dist_le; eauto.
 Qed.
 Canonical Structure sharedO := Ofe shared shared_ofe_mixin.
 
@@ -390,7 +390,7 @@ Proof. intros [|] ?; done. Qed.
 
 Lemma dfrac_error_discarded : forall x, dfrac_error (DfracDiscarded ⋅ x) = dfrac_error x.
 Proof.
-  destruct x; simpl; rewrite left_id //.
+  destruct x; simpl; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
 Qed.
 
 Lemma share_op_None : forall (s : shareO), s ⋅ ShareBot = ShareBot.
@@ -401,9 +401,9 @@ Qed.
 Local Instance shared_unit_left_id : LeftId equiv (ε : shared) op.
 Proof.
   intros [|]; rewrite /op /=.
-  - rewrite right_id.
+  - rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)).
     destruct (readable_dfrac_dec _); done.
-  - hnf; rewrite left_id //.
+  - hnf; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
 Qed.
 
 Definition shared_cmra_mixin : CmraMixin shared.
@@ -428,9 +428,9 @@ Proof.
   - intros [|]; intuition.
     + by destruct H.
     + split; apply cmra_valid_validN, H.
-    + apply (H 0).
-  - intros ? [|]; try done.
-    intros [??]; split; last apply cmra_validN_S; done.
+    + apply (H 0ᵢ).
+  - intros ?? [|]; try done.
+    intros [??]; split; last eapply cmra_validN_le; done.
   - intros ???.
     pose proof (shared_op_alt x (y ⋅ z)) as Hop1.
     pose proof (shared_op_alt (x ⋅ y) z) as Hop2.
@@ -467,7 +467,7 @@ Proof.
       destruct shyz; last by rewrite share_op_None in H; destruct H.
       destruct Hop3 as (? & ? & ? & ? & -> & -> & [=] & ?); simpl in *; subst.
       rewrite /op /shared_op_instance; hnf.
-      apply (@cmra_assoc shareR).
+      apply (@cmra_assoc _ shareR).
   - intros ??.
     pose proof (shared_op_alt x y) as Hop1.
     pose proof (shared_op_alt y x) as Hop2.
@@ -479,11 +479,11 @@ Proof.
       by inversion Hv; subst.
     + destruct (dfrac_error _) eqn: Herr; first by rewrite Hop1 Hop2.
       destruct Hop1 as (? & ? & ? & ? & -> & -> & -> & ?), Hop2 as (? & ? & ? & ? & [=] & [=] & -> & ?); subst.
-      hnf; by rewrite (@cmra_comm shareR).
+      hnf; by rewrite (@cmra_comm _ shareR).
   - intros [|].
     + rewrite /op /shared_op_instance /core /pcore /shared_pcore_instance /=.
       destruct dq.
-      * rewrite /ε /shared_unit_instance right_id.
+      * rewrite /ε /shared_unit_instance (right_id _ _ (RightId:=ucmra_unit_right_id)).
         destruct (readable_dfrac_dec _); done.
       * rewrite comm dfrac_op_both_discarded.
         destruct (readable_dfrac_dec _); try done.
@@ -507,7 +507,7 @@ Proof.
         { destruct z as [[|]|]; done. }
         exists (YES DfracDiscarded I v0).
         unshelve rewrite YES_op /=; last split; rewrite ?dfrac_op_both_discarded //.
-        rewrite -agree_included H -Some_included_total -Hval; eexists; done.
+        rewrite H -agree_included -Some_included_total -Hval; eexists; done.
       * destruct (dfrac_error _) eqn: Herr; last by destruct Hop as (? & ? & ? & ? & ? & ?).
         rewrite Hop in H; destruct y; inversion H; subst.
         exists err; done.
@@ -682,13 +682,13 @@ Proof.
   rewrite dfrac_of_op' val_of_op'; simpl.
   destruct (dfrac_error _) eqn: Herr; [left | right].
   - by apply dfrac_error_fail.
-  - rewrite !left_id //.
+  - rewrite !(left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
 Qed.
 
 Lemma readable_dfrac_order : forall dq dq', dq ≼ₒ dq' -> readable_dfrac dq -> readable_dfrac dq'.
 Proof.
   intros ?? [-> | <-]; try done.
-  destruct dq as [[|]|[|]]; try done; simpl; rewrite right_id //.
+  destruct dq as [[|]|[|]]; try done; simpl; rewrite (right_id _ _ (RightId:=ucmra_unit_right_id)) //.
 Qed.
 
 Lemma dfrac_error_order : forall dq dq', dq ≼ₒ dq' -> dfrac_error dq = dfrac_error dq'.
@@ -697,7 +697,7 @@ Proof.
   rewrite (comm _ dq) dfrac_error_discarded //.
 Qed.
 
-Lemma shared_orderN_op : ∀ (n : nat) (x x' y : shared), x ≼ₒ{n} x' → x ⋅ y ≼ₒ{n} x' ⋅ y.
+Lemma shared_orderN_op : ∀ (n : SI) (x x' y : shared), x ≼ₒ{n} x' → x ⋅ y ≼ₒ{n} x' ⋅ y.
 Proof.
   intros.
   destruct H as [H | [??]].
@@ -758,12 +758,12 @@ Proof.
     rewrite /core /=; destruct x, y; try done; simpl in *.
     + right; destruct Hd as [<- | <-], dq; rewrite ?dfrac_op_own_discarded ?dfrac_op_both_discarded // /=.
       split.
-      * right; rewrite left_id //.
+      * right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
       * apply agree_increasing.
     + right; destruct Hd as [<- | <-]; try done.
       rewrite dfrac_op_own_discarded.
       destruct sh; split; try done.
-      right; rewrite left_id //.
+      right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)) //.
     + destruct Hd as [[=] | ?]; subst; try done.
       destruct sh0; [right | left]; done.
   - intros ???? Hvalid [? | [Hd Hv]].
@@ -801,9 +801,9 @@ Proof.
     + eexists; split; first right; done.
   - intros ??? [Hd Hv]%shared_dist_implies.
     right; split; [hnf; auto | by apply ora_dist_orderN].
-  - intros ??? [H | [? ?%ora_orderN_S]].
+  - intros ???? [H | [? ?]].
     + destruct y; inversion H; subst; by left.
-    + by right.
+    + intros. eapply ora_orderN_le in H0; eauto. by right.
   - intros ???? Hord [H | [Hd Hv]].
     { destruct z; inversion H; subst; by left. }
     destruct Hord as [Hy | [??]].
@@ -820,7 +820,7 @@ Proof.
   - split.
     + intros [? | [??]] ?; first by left.
       right; split; last apply ora_order_orderN; done.
-    + intros H; pose proof (H 0) as H0; destruct H0 as [? | [??]]; first by left.
+    + intros H; pose proof (H 0ᵢ) as H0; destruct H0 as [? | [??]]; first by left.
       right; split; try done.
       apply ora_order_orderN; intros n1.
       destruct (H n1) as [? | [??]]; first destruct y; done.
@@ -832,12 +832,12 @@ Proof.
       destruct x; simpl in *.
       * right; destruct dq, cx; inversion Heq; subst; simpl.
         -- destruct (_ ⋅ _); try done.
-           split; first by right; rewrite left_id.
+           split; first by right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)).
            apply agree_increasing.
         -- destruct (dfrac_of y); split; simpl; try done; rewrite -H0 -Hv Some_op_opM Some_order; destruct (val_of y); try done; rewrite /= comm; apply agree_increasing.
       * destruct sh, cx; inversion Heq; subst; simpl.
         -- right; destruct (_ ⋅ _); try done; simpl.
-           split; first by right; rewrite left_id.
+           split; first by right; rewrite (left_id _ _ (LeftId:=ucmra_unit_left_id)).
            apply agree_increasing.
         -- destruct (dfrac_of y); done.
     + destruct (dfrac_error _) eqn: Herr; first by destruct (x ⋅ y); inversion Hop; subst; left.
@@ -887,7 +887,7 @@ Qed.
 
 End shared.
 
-Arguments YES {_ _ _} _ _ _.
-Arguments NO {_ _ _} _ _.
-Arguments dfrac_of {_ _ _} _.
-Arguments val_of {_ _ _} _.
+Arguments YES {_ _ _ _} _ _ _.
+Arguments NO {_ _ _ _} _ _.
+Arguments dfrac_of {_ _ _ _} _.
+Arguments val_of {_ _ _ _} _.

veric/external_state.v

@@ -11,15 +11,15 @@ Class externalGS (Z : Type) (Σ : gFunctors) := ExternalGS {
 }.
 
 Definition has_ext {Z : Type} `{!externalGS Z Σ} (z : Z) : iProp Σ :=
-  own(inG0 := external_inG) external_name (auth_frag(A := optionUR (@exclR (leibnizO Z))) (Excl' z)).
+  own(inG0 := external_inG) external_name (auth_frag(A := optionUR (@exclR _(leibnizO Z))) (Excl' z)).
 
 Definition ext_auth {Z : Type} `{!externalGS Z Σ} (z : Z) : iProp Σ :=
-  own(inG0 := external_inG) external_name (auth_auth(A := optionUR (@exclR (leibnizO Z))) (DfracOwn 1) (Excl' z)).
+  own(inG0 := external_inG) external_name (auth_auth(A := optionUR (@exclR _(leibnizO Z))) (DfracOwn 1) (Excl' z)).
 
 Lemma ext_alloc {Z : Type} `{!inG Σ (excl_authR (leibnizO Z))} (z : Z) : ⊢ |==> ∃ _ : externalGS Z Σ, ext_auth z ∗ has_ext z.
 Proof.
   rewrite /ext_auth /has_ext.
-  iMod (own_alloc (●E (z : leibnizO Z) ⋅ ◯E (z : leibnizO Z) : excl_authR (leibnizO Z))) as (γ) "?".
+  iMod (own_alloc (●E (z : leibnizO Z) ⋅ ◯E (z : leibnizO Z) : @excl_authR natSI (leibnizO Z))) as (γ) "?".
   { apply excl_auth_valid. }
   iExists (ExternalGS _ _ _ γ).
   rewrite own_op //.

veric/juicy_mem.v

@@ -1015,7 +1015,7 @@ Section mpred.
     apply shared_valid in Hv as (_ & Hv).
     apply option_included_total in H as [-> | (? & ? & -> & Heq & H)]; auto.
     rewrite Heq /= in Hv |- *.
-    assert (✓{0} x2) by (by apply cmra_valid_validN).
+    assert (✓{0ᵢ} x2) by (by apply cmra_valid_validN).
     right; f_equal; symmetry; apply (elem_of_agree_ne' O); first done.
     symmetry; apply agree_valid_includedN; first done.
     by apply @cmra_included_includedN.