Upate to work with the latest Iris

.github/workflows/build.yml

@@ -11,14 +11,14 @@ jobs:
     - uses: cachix/install-nix-action@v24
       with:
         github_access_token: ${{ secrets.GITHUB_TOKEN }}
-    - run: nix build .#coq-artifact
+    - run: nix build .#rocq-artifact
 
   build:
     runs-on: ubuntu-latest
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.2'
       max-parallel: 4
       fail-fast: false
 

Makefile

@@ -22,7 +22,7 @@ clean: Makefile.coq
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
+	"$(COQBIN)rocq" makefile -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
 OPAMFILES=$(wildcard *.opam)

flake.nix

@@ -1,34 +1,34 @@
 {
   description = "gitrees";
   inputs = {
-    nixpkgs.url = github:NixOS/nixpkgs/nixos-24.11;
+    nixpkgs.url = github:NixOS/nixpkgs/nixos-26.05;
     flake-utils.url = github:numtide/flake-utils;
   };
   outputs = { self, nixpkgs, flake-utils }:
     with flake-utils.lib; eachSystem allSystems (system:
       let
         pkgs = nixpkgs.legacyPackages.${system};
         lib = pkgs.lib;
-        coq = pkgs.coq_8_20;
-        coqPkgs = pkgs.coqPackages_8_20;
+        rocq = pkgs.rocq-core_9_2;
+        rocqPkgs = pkgs.rocqPackages_9_2;
       in {
         packages = {
-          coq-artifact = coqPkgs.mkCoqDerivation {
-            pname = "coq-artifact";
+          rocq-artifact = rocqPkgs.mkRocqDerivation {
+            pname = "rocq-artifact";
             version = "main";
             src = ./.;
             buildPhase = "make";
             propagatedBuildInputs = [
-              coqPkgs.stdpp
-              coqPkgs.iris
+              rocqPkgs.stdpp
+              rocqPkgs.iris
             ];
           };
         };
         devShell = pkgs.mkShell {
           buildInputs = with pkgs; [
-            coq
+            rocq
           ];
-          inputsFrom = [ self.packages.${system}.coq-artifact ];
+          inputsFrom = [ self.packages.${system}.rocq-artifact ];
         };
       });
 }

theories/effects/callcc.v

@@ -15,30 +15,33 @@ Program Definition throwE : opInterp :=
 
 Definition contE := @[callccE;throwE].
 
-Definition reify_callcc X `{Cofe X} : ((laterO X -n> laterO X) -n> laterO X) *
+Definition reify_callcc X `{!Cofe X} : ((laterO X -n> laterO X) -n> laterO X) *
                                         unitO * (laterO X -n> laterO X) →
                                       option (laterO X * unitO * listO (laterO X)) :=
   λ '(f, σ, k), Some ((k (f k): laterO X), σ : unitO, []).
-#[export] Instance reify_callcc_ne X `{Cofe X} :
+#[export] Instance reify_callcc_ne X `{!Cofe X} :
   NonExpansive (reify_callcc X :
     prodO (prodO ((laterO X -n> laterO X) -n> laterO X) unitO)
       (laterO X -n> laterO X) →
     optionO ((laterO X) * unitO * listO (laterO X))%type).
 Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed.
 
-Definition reify_throw X `{Cofe X} :
+Definition reify_throw X `{!Cofe X} :
   ((laterO X * (laterO (X -n> X))) * unitO * (Empty_setO -n> laterO X)) →
   option (laterO X * unitO * listO (laterO X)) :=
   λ '((e, k'), σ, _),
     Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), σ : unitO, []).
-#[export] Instance reify_throw_ne X `{Cofe X} :
+#[export] Instance reify_throw_ne X `{!Cofe X} :
   NonExpansive (reify_throw X :
       prodO (prodO (prodO (laterO X) (laterO (X -n> X))) unitO)
         (Empty_setO -n> laterO X) →
     optionO ((laterO X) * (unitO) * listO (laterO X))%type).
 Proof.
-  intros ?[[[]]][[[]]]?. rewrite /reify_throw.
-  repeat f_equiv; apply H0.
+  intros n [[[e1 k1] []] h1] [[[e2 k2] []] h2] [[[He Hk] _] _].
+  rewrite /reify_throw /=.
+  do 3 f_equiv.
+  etrans; first exact (later_ap_ne n k1 k2 Hk e1).
+  apply (later_ap k2). exact He.
 Qed.
 
 Program Canonical Structure reify_cont : sReifier CtxDep :=

theories/effects/coroutines.v

@@ -1,7 +1,7 @@
 (** Coroutines effects *)
 From iris.algebra Require Import gmap excl auth gmap_view list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra cmra.
 From iris.heap_lang Require Export locations.
 From gitrees Require Import prelude gitree hom.
 
@@ -92,7 +92,7 @@ Proof.
   apply Next_contractive.
   destruct n; first apply dist_later_0.
   apply dist_later_S.
-  f_equiv; first (apply Hp; lia).
+  f_equiv; first (apply Hp; apply SIdx.lt_succ_diag_r).
   apply (compose (proj2 (dist_later_S _ _ _)) (later_car_anti_contractive (S n) (_ q1) (_ q2))).
   by f_equiv.
 Qed.
@@ -382,7 +382,7 @@ Section program_logic.
     iDestruct (auth_both_validI with "J") as "((%c & #J1) & J2)".
     rewrite /op /cmra_op /= /excl_op_instance /= /ucmra_op /=.
     iRewrite "J1" in "J2".
-    iDestruct (uPred.cmra_valid_elim with "J2") as "%J".
+    iDestruct (internal_cmra_valid_elim with "J2") as "%J".
     destruct c as [[c|] |].
     - iExFalso.
       iPureIntro.
@@ -733,9 +733,9 @@ Section lib.
     reflexivity.
   Qed.
   Local Instance REC_val body : IntoVal (REC body) (RECV body).
-  Proof.
+  Proof using CR R n rs Σ.
     rewrite /IntoVal.
-    apply bi.siProp.internal_eq_soundness.
+    apply (@bi.internal_eq.internal_eq_soundness iProp _).
     iLöb as "IH".
     iEval (rewrite REC_unfold RECV_unfold).
     iApply f_equivI.

theories/effects/exceptions.v

@@ -68,27 +68,27 @@ Module Exc (Errors : ExcSig).
   Definition exceptE := @[regE;popE;throwE].
 
   (** Register a handler : Push the handler and current context on the stack **)
-  Definition reify_reg X `{Cofe X} :
+  Definition reify_reg X `{!Cofe X} :
     excO * (laterO X -n> laterO X) * (laterO X)
     * (stateF ♯ X) * (laterO X -n> laterO X) →
     option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
       λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ, []).
 
-  #[export] Instance reify_reg_ne X `{Cofe X}
+  #[export] Instance reify_reg_ne X `{!Cofe X}
     : NonExpansive (reify_reg X : excO * (laterO X -n> laterO X)
                                   * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X)
                                   → option (laterO X * (stateF ♯ X) * listO (laterO X))).
   Proof.
     solve_proper_prepare.
     destruct x as [[[[? ?] ?] ?] ?].
     destruct y as [[[[? ?] ?] ?] ?].
-      repeat rewrite e pair_dist in H0.
-      destruct H0 as [[[[? ?] ?] ?] ?].
+      repeat rewrite e pair_dist in H.
+      destruct H as [[[[? ?] ?] ?] ?].
       repeat f_equiv; done.
   Qed.
 
   (** Unregister a handler : Remove the topmost handler, restore the ambient context from when it was registered **)
-  Definition reify_pop X `{Cofe X} :
+  Definition reify_pop X `{!Cofe X} :
     excO * (stateF ♯ X) * (unitO -n> laterO X)
     → option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
     λ '(err, σ, k), match σ with
@@ -99,7 +99,7 @@ Module Exc (Errors : ExcSig).
                          else None)
                     end.
 
-  #[export] Instance reify_pop_ne X `{Cofe X} :
+  #[export] Instance reify_pop_ne X `{!Cofe X} :
     NonExpansive (reify_pop X :
         excO * (stateF ♯ X) * (unitO -n> laterO X)
         → option (laterO X * (stateF ♯ X) * listO (laterO X))).
@@ -200,7 +200,7 @@ Module Exc (Errors : ExcSig).
   Qed.
 
   (** Raise an error : Find the most recent handler handling this error and remove all handlers registered after it from the stack then invoke the handler inside the context from when it was registered **)
-  Definition reify_throw X `{Cofe X} :
+  Definition reify_throw X `{!Cofe X} :
     (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
     → option (laterO X * (stateF ♯ X) * listO (laterO X)) :=
     λ '(x, σ, _), let (err,v) := x in
@@ -209,15 +209,15 @@ Module Exc (Errors : ExcSig).
                   | Some (_, h, k, σ') => Some (k (h v), σ', [])
                   end.
 
-  #[export] Instance reify_throw_ne X `{Cofe X} :
+  #[export] Instance reify_throw_ne X `{!Cofe X} :
     NonExpansive (reify_throw X :
         (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X)
         → option (laterO X * (stateF ♯ X) * listO (laterO X))).
   Proof.
-    solve_proper_prepare.
+    intros n x y Hxy.
     destruct x as [[[e v] σ] k].
     destruct y as [[[e' v'] σ'] k'].
-    destruct H0 as [[[He Hv] Hσ] Hk].
+    destruct Hxy as [[[He Hv] Hσ] Hk].
     simpl in *.
     generalize dependent σ'.
     induction σ as [|[[err hand] kont] σ].

theories/effects/fork.v

@@ -15,10 +15,10 @@ Program Definition forkI : opInterp :=
 Definition concE := @[forkI].
 
 (* FORK *)
-Definition reify_fork' X `{Cofe X} : (laterO X) * stateO →
+Definition reify_fork' X `{!Cofe X} : (laterO X) * stateO →
                                       option (unitO * stateO * listO (laterO X)) :=
     λ '(o, σ), Some ((), σ, [o]).
-#[export] Instance reify_fork'_ne X `{Cofe X} :
+#[export] Instance reify_fork'_ne X `{!Cofe X} :
   NonExpansive (reify_fork' X).
 Proof.
   intros ?[? []] [? []] G.

theories/effects/io_tape.v

@@ -34,21 +34,21 @@ Program Definition outputE : opInterp :=
 Definition ioE := @[inputE;outputE].
 
 (* INPUT *)
-Definition reify_input X `{Cofe X} : unitO * stateO →
+Definition reify_input X `{!Cofe X} : unitO * stateO →
                                       option (natO * stateO * listO (laterO X)) :=
     λ '(o, σ), Some (update_input σ : prodO natO stateO, []).
-#[export] Instance reify_input_ne X `{Cofe X} :
+#[export] Instance reify_input_ne X `{!Cofe X} :
   NonExpansive (reify_input X).
 Proof.
   intros ?[[]][[]][_?]. simpl in *. f_equiv.
   repeat f_equiv. done.
 Qed.
 
 (* OUTPUT *)
-Definition reify_output X `{Cofe X} : (natO * stateO) →
+Definition reify_output X `{!Cofe X} : (natO * stateO) →
                                        option (unitO * stateO * listO (laterO X)) :=
   λ '(n, σ), Some((), update_output n σ : stateO, []).
-#[export] Instance reify_output_ne X `{Cofe X} :
+#[export] Instance reify_output_ne X `{!Cofe X} :
   NonExpansive (reify_output X).
 Proof.
   intros ?[][][]. simpl in *.

theories/effects/store.v

@@ -1,7 +1,7 @@
 (** Higher-order store effect *)
 From iris.algebra Require Import gmap excl auth gmap_view list.
-From iris.proofmode Require Import classes tactics.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import classes proofmode.
+From iris.bi Require Import algebra.
 From iris.heap_lang Require Export locations.
 From gitrees Require Import prelude.
 From gitrees Require Import gitree.
@@ -36,7 +36,7 @@ Lemma gen_fresh_slice_val {A} (σ : gmap loc A) p a x y :
 Proof.
   induction p as [| ? IH].
   - simpl; intros H; inversion H.
-  - simpl; intros [H | H%elem_of_list_singleton]%elem_of_app;
+  - simpl; intros [H | H%list_elem_of_singleton]%elem_of_app;
       first by apply IH.
     by inversion H; subst.
 Qed.
@@ -49,9 +49,9 @@ Proof.
   - simpl; intros H.
     rewrite fmap_app in H.
     apply elem_of_app in H.
-    destruct H as [H | ->%elem_of_list_singleton].
+    destruct H as [H | ->%list_elem_of_singleton].
     + by apply elem_of_app; left; apply IH.
-    + by apply elem_of_app; right; simpl; apply elem_of_list_singleton.
+    + by apply elem_of_app; right; simpl; apply list_elem_of_singleton.
 Qed.
 
 Lemma gen_fresh_slice_no_dup {A} (σ : gmap loc A) p a :
@@ -67,13 +67,13 @@ Proof.
   simpl; apply NoDup_app.
   split; first done.
   split; last apply NoDup_singleton.
-  intros x H ->%elem_of_list_singleton.
+  intros x H ->%list_elem_of_singleton.
   assert (∀ i : nat, (Loc.fresh (dom σ) +ₗ (p + i)%nat, a) ∉ gen_fresh_slice σ p a) as J.
   {
     clear.
     induction p as [| ? IH].
     - set_solver.
-    - simpl; intros i [H | H%elem_of_list_singleton]%elem_of_app.
+    - simpl; intros i [H | H%list_elem_of_singleton]%elem_of_app.
       + rewrite -PeanoNat.Nat.add_succ_r in H.
         by apply (IH (S i)).
       + inversion H as [J]; subst.
@@ -218,8 +218,8 @@ Proof.
       * apply dist_later_0.
       * apply dist_later_S.
         do 2 f_equiv.
-        -- apply Hk; lia.
-        -- apply Hxy; lia.
+        -- apply Hk; apply SIdx.lt_succ_diag_r.
+        -- apply Hxy; apply SIdx.lt_succ_diag_r.
     + rewrite !later_map_Next.
       rewrite Hm.
       f_equiv; last done.
@@ -228,8 +228,8 @@ Proof.
       -- apply dist_later_0.
       -- apply dist_later_S.
          do 2 f_equiv.
-         ++ apply Hk; lia.
-         ++ apply Hxy; lia.
+         ++ apply Hk; apply SIdx.lt_succ_diag_r.
+         ++ apply Hxy; apply SIdx.lt_succ_diag_r.
   - by rewrite Hp Hm.
 Qed.
 
@@ -919,14 +919,14 @@ Section wp.
             * apply dist_later_0.
             * apply dist_later_S.
               f_equiv.
-              apply H; lia.
+              apply H; apply SIdx.lt_succ_diag_r.
           + do 2 f_equiv.
             apply Next_contractive.
             destruct m.
             * apply dist_later_0.
             * apply dist_later_S.
               f_equiv.
-              apply H; lia.
+              apply H; apply SIdx.lt_succ_diag_r.
         - done.
       }
       {
@@ -1110,14 +1110,14 @@ Module xchg_wp.
               * apply dist_later_0.
               * apply dist_later_S.
                 f_equiv.
-                apply H; lia.
+                apply H; apply SIdx.lt_succ_diag_r.
             + do 2 f_equiv.
               apply Next_contractive.
               destruct m.
               * apply dist_later_0.
               * apply dist_later_S.
                 f_equiv.
-                apply H; lia.
+                apply H; apply SIdx.lt_succ_diag_r.
           - done.
         }
         {

theories/examples/affine_lang/logrel2.v

@@ -408,7 +408,7 @@ Section glue.
     iClear "Hl". clear l.
     iApply fupd_wp.
     { solve_proper. }
-    iMod (inv_alloc (nroot.@"yolo") _ (∃ n, pointsto l' (Ret n)) with "[Hl']") as "#Hinv".
+    iMod (inv_alloc (nroot.@"yolo") _ (∃ n : natO, pointsto l' (Ret n : IT)) with "[Hl']") as "#Hinv".
     { iNext. iExists _; done. }
     iPoseProof ("Ha" $! (thunkedV (IT_of_V β'v) l') with "[-Has]") as "H1".
     {
@@ -422,7 +422,7 @@ Section glue.
                 (⊤∖ nclose (nroot.@"storeE")) _ _ _ idfun with "Hctx").
       { set_solver. }
       iInv (nroot.@"yolo") as (n) "Hl'" "Hcl".
-      iModIntro. iExists (Ret n). iFrame.
+      iModIntro. iExists (Ret n : IT). iFrame.
       iNext. iNext. iIntros "Hl'".
       iMod ("Hcl" with "[Hl']") as "_".
       { iNext. eauto with iFrame. }

theories/examples/delim_lang/example.v

@@ -3,8 +3,8 @@ From gitrees Require Import gitree lang_generic.
 From gitrees.effects Require Import delim store.
 From gitrees.lib Require Import pairs.
 From gitrees.examples.delim_lang Require Import lang interp.
-From iris.proofmode Require Import base classes tactics environments.
-From iris.base_logic Require Import algebra.
+From iris.proofmode Require Import base classes proofmode environments.
+From iris.bi Require Import algebra.
 
 Open Scope syn_scope.