From ae415dea889ac907987961d64ce5797baff226e3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Mar 2025 17:42:30 +0100
Subject: [PATCH] Bump Iris (Transfinite algebra).

---
 coq-gpfsl.opam                              | 2 +-
 gpfsl-examples/algebra/mono_list_list.v     | 2 +-
 gpfsl-examples/lock/proof_ticket_lock_gps.v | 2 +-
 gpfsl-examples/queue/proof_ms_gps.v         | 2 +-
 gpfsl/algebra/to_agree.v                    | 2 +-
 gpfsl/gps/model_defs.v                      | 2 +-
 gpfsl/logic/na_invariants.v                 | 8 ++++----
 7 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/coq-gpfsl.opam b/coq-gpfsl.opam
index 2dd7897b..bcce9cd5 100644
--- a/coq-gpfsl.opam
+++ b/coq-gpfsl.opam
@@ -10,7 +10,7 @@ version: "dev"
 synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
 
 depends: [
-  "coq-iris"  { (= "dev.2025-03-25.0.79d33e24") | (= "dev") }
+  "coq-iris"  { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
 ]
 
 build: ["./make-package" "gpfsl" "-j%{jobs}%"]
diff --git a/gpfsl-examples/algebra/mono_list_list.v b/gpfsl-examples/algebra/mono_list_list.v
index 83a9b2fb..3a8fa9b0 100644
--- a/gpfsl-examples/algebra/mono_list_list.v
+++ b/gpfsl-examples/algebra/mono_list_list.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export auth max_prefix_list.
+From iris.algebra Require Export auth max_prefix_list stepindex_finite.
 From iris.algebra Require Import updates local_updates proofmode_classes.
 
 From iris.prelude Require Import options.
diff --git a/gpfsl-examples/lock/proof_ticket_lock_gps.v b/gpfsl-examples/lock/proof_ticket_lock_gps.v
index 44bd1a55..ed195f7f 100644
--- a/gpfsl-examples/lock/proof_ticket_lock_gps.v
+++ b/gpfsl-examples/lock/proof_ticket_lock_gps.v
@@ -370,7 +370,7 @@ Proof.
   apply bi.sep_ne; [done|].
   repeat (apply bi.exist_ne => ?).
   apply GPS_iSP_Writer_contractive; [done|].
-  dist_later_fin_intro. eapply H; si_solver.
+  dist_later_fin_intro. eapply H, SIdx.lt_succ_diag_r.
 Qed.
 
 Definition NSP P γ : interpO Σ natProtocol := fixpoint (NSP' P γ).
diff --git a/gpfsl-examples/queue/proof_ms_gps.v b/gpfsl-examples/queue/proof_ms_gps.v
index f885eb5a..9628ad16 100644
--- a/gpfsl-examples/queue/proof_ms_gps.v
+++ b/gpfsl-examples/queue/proof_ms_gps.v
@@ -83,7 +83,7 @@ Proof.
   apply bi.sep_ne; [done|].
   do 2 (apply bi.exist_ne => ?).
   apply GPS_iPP_contractive.
-  dist_later_fin_intro. eapply H; si_solver.
+  dist_later_fin_intro. eapply H, SIdx.lt_succ_diag_r.
 Qed.
 
 Definition Link : ∀ γ, interpO Σ LinkProtocol := fixpoint Link'.
diff --git a/gpfsl/algebra/to_agree.v b/gpfsl/algebra/to_agree.v
index 24787c53..80f55dac 100644
--- a/gpfsl/algebra/to_agree.v
+++ b/gpfsl/algebra/to_agree.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import agree gmap local_updates.
+From iris.algebra Require Import agree gmap local_updates stepindex_finite.
 
 Require Import iris.prelude.options.
 
diff --git a/gpfsl/gps/model_defs.v b/gpfsl/gps/model_defs.v
index a17804bd..88070ce9 100644
--- a/gpfsl/gps/model_defs.v
+++ b/gpfsl/gps/model_defs.v
@@ -454,7 +454,7 @@ Section recursive.
   Proof. constructor; repeat intro; exact True%I. Qed.
 End recursive.
 Program Example intExample Σ : interpO Σ unitProtocol :=
-  @fixpoint _ _ _
+  @fixpoint _ _ _ _
     (λ (F : interpO Σ unitProtocol) b l γ t s v, ∃ c, ⌜c = #1⌝ ∗ ▷ F b l γ t s v)%I _.
 Next Obligation.
   intros ???? H. repeat intro.
diff --git a/gpfsl/logic/na_invariants.v b/gpfsl/logic/na_invariants.v
index 090ebb98..b87498d3 100644
--- a/gpfsl/logic/na_invariants.v
+++ b/gpfsl/logic/na_invariants.v
@@ -11,12 +11,12 @@ Require Import iris.prelude.options.
 Definition na_inv_pool_name := gname.
 
 Class na_invG Vw `{!LatBottom bot} Σ :=
-  { na_inv_enable_inG : inG Σ (@discrete_funR positive (λ _, authUR (latUR Vw)));
+  { na_inv_enable_inG : inG Σ (discrete_funR (λ _ : positive, authUR (latUR Vw)));
     na_inv_disable_inG : inG Σ (excl_authR (latO Vw)) }.
 Local Existing Instances na_inv_enable_inG na_inv_disable_inG.
 
 Definition na_invΣ Vw `{!LatBottom bot} : gFunctors :=
-  #[ GFunctor (constRF (@discrete_funR positive (λ _, authUR (latUR Vw))));
+  #[ GFunctor (constRF (discrete_funR (λ _ : positive, authUR (latUR Vw))));
      GFunctor (constRF (excl_authR (latO Vw))) ].
 Global Instance subG_na_invG Vw `{!LatBottom bot} Σ :
   subG (na_invΣ Vw) Σ → na_invG Vw Σ.
@@ -109,7 +109,7 @@ Section proofs.
   Proof.
     iIntros "HP".
     iDestruct (monPred_in_intro with "HP") as (V) "[#HV HP]".
-    iMod (own_unit (@discrete_funUR positive (λ _, authUR (latUR Vw))) p) as "Hempty".
+    iMod (own_unit (discrete_funUR (λ _ : positive, authUR (latUR Vw))) p) as "Hempty".
     iMod (own_alloc (● None)) as (γ) "Hdis"; [by apply auth_auth_valid|].
     destruct (fresh_inv_name ∅ N) as (i & _ & HiN). unfold na_inv.
     iExists i, V, γ. iFrame "# %". iMod (inv_alloc N with "[-]") as "$"; [|done].
@@ -156,7 +156,7 @@ Section proofs.
     iDestruct "Htoki" as (Vi) "[Hown Hdis1]".
     iCombine "Hdis1 Hdis2" gives %EQVi%excl_auth_agree%(inj to_latT).
     (* FIXME : rewrite EQVi should work. *)
-    assert (@discrete_fun_singleton _ _ (λ _, _) i (● to_latT Vi) ≡
+    assert (@discrete_fun_singleton _ _ _ (λ _, _) i (● to_latT Vi) ≡
             discrete_fun_singleton i (● to_latT (Vs i))) as -> by by f_equiv; rewrite EQVi.
     iMod (own_update_2 with "Hdis1 Hdis2") as "Hdis".
     { apply auth_update_dealloc, delete_option_local_update, _. }
-- 
GitLab