diff --git a/coq-simuliris.opam b/coq-simuliris.opam
index 198a64d6b6d336955dc94970bcdf84c8597a24dc..083d814ebdbea26d3ffc8f6e84961678e5f8e874 100644
--- a/coq-simuliris.opam
+++ b/coq-simuliris.opam
@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/simuliris.git"
 synopsis: "Local Simulation proofs, the Iris style"
 
 depends: [
-  "coq-iris" { (= "dev.2025-02-07.0.d68b4fdb") | (= "dev") }
+  "coq-iris" { (= "dev.2025-03-31.0.017605dd") | (= "dev") }
   "coq-equations" { (= "1.3+8.19") | (= "1.3.1+8.20") | (= "1.3.1+9.0") | (= "dev") }
 ]
 
diff --git a/theories/simulation/closed_sim.v b/theories/simulation/closed_sim.v
index 53a7e70beb2c5f36a7c5fce14f4de24319a532f5..a7cd510b22064ff2323b95eccca6aed06136a07b 100644
--- a/theories/simulation/closed_sim.v
+++ b/theories/simulation/closed_sim.v
@@ -19,7 +19,7 @@ Section fix_lang.
     (P_s P_t P: prog Λ)
     (σ_s σ_t σ : state Λ).
 
-  Notation expr_rel := (@exprO Λ -d> @exprO Λ -d> PROP).
+  Notation expr_rel := (@exprO _ Λ -d> @exprO _ Λ -d> PROP).
 
   Local Instance expr_rel_func_ne (F: expr_rel → thread_idO -d> expr_rel) `{Hne: !NonExpansive F}:
     (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) F).
@@ -125,7 +125,7 @@ Section fix_lang.
       destruct y as (((Ψ & π') & e_t') & e_s'); simpl.
       destruct Heq as [[[Heq1 Heq2] Heq3] Heq4]; simpl in Heq1, Heq2, Heq3, Heq4.
       eapply csim_expr_inner_ne; eauto.
-      + intros ?????->%leibniz_equiv. by eapply Hg.
+      + intros ?????->%leibnizO_leibniz. by eapply Hg.
       + intros ????????; rewrite /curry4. eapply Hne.
         repeat split; simpl; done.
   Qed.
diff --git a/theories/simulation/fairness_adequacy.v b/theories/simulation/fairness_adequacy.v
index 020778e7b877aef20ff7669ee24caea7007e8aff..2d41978deac5f747a2f43133b1ff7252511ce389 100644
--- a/theories/simulation/fairness_adequacy.v
+++ b/theories/simulation/fairness_adequacy.v
@@ -79,13 +79,13 @@ Proof.
 Qed.
 
 (* free NonExpansive instances *)
-Local Instance free_discrete_prod_ne (Φ: prodO (prodO (listO (prodO (@exprO Λ) (@exprO Λ))) (gsetO natO)) (gmapO natO natO) → PROP):
+Local Instance free_discrete_prod_ne (Φ: prodO (prodO (listO (prodO (@exprO _ Λ) (@exprO _ Λ))) (gsetO natO)) (gmapO natO natO) → PROP):
   NonExpansive Φ.
 Proof.
   by intros n [[? ?] ?] [[? ?] ?] ->%discrete_iff%leibniz_equiv; last apply _.
 Qed.
 
-Local Instance free_discrete_expr_ne (Φ: listO (prodO (@exprO Λ) (@exprO Λ)) → PROP):
+Local Instance free_discrete_expr_ne (Φ: listO (prodO (@exprO _ Λ) (@exprO _ Λ)) → PROP):
   NonExpansive Φ.
 Proof.
   by intros n ? ? ->%discrete_iff%leibniz_equiv; last apply _.
@@ -151,7 +151,7 @@ Lemma sim_pool_coind F P:
   F P -∗ sim_pool P.
 Proof.
   iIntros "#IH HF". rewrite /sim_pool.
-  iApply (greatest_fixpoint_coiter _ (F: listO (prodO (@exprO Λ) (@exprO Λ)) → PROP) with "[] HF").
+  iApply (greatest_fixpoint_coiter _ (F: listO (prodO (@exprO _ Λ) (@exprO _ Λ)) → PROP) with "[] HF").
   iModIntro. iIntros (L) "HF". rewrite /sim_pool_inner.
   iIntros (D). by iApply "IH".
 Qed.
diff --git a/theories/simulation/language.v b/theories/simulation/language.v
index 8f85c28d58790691bc3f4abe5164eabbbaa2bd2c..504b29de47be4f495ab365056d908bd764e5751a 100644
--- a/theories/simulation/language.v
+++ b/theories/simulation/language.v
@@ -1135,8 +1135,8 @@ End safe_reach.
 
 
 (* discrete OFE instance for expr and thread_id *)
-Definition exprO {Λ : language} := leibnizO (expr Λ).
-Global Instance expr_equiv {Λ} : Equiv (expr Λ). apply exprO. Defined.
+Definition exprO {SI : sidx}{Λ : language} := leibnizO (expr Λ).
+Global Instance expr_equiv {SI : sidx} {Λ} : Equiv (expr Λ). apply exprO. Defined.
 
-Definition thread_idO := leibnizO thread_id.
-Global Instance thread_id_equiv : Equiv thread_id. apply thread_idO. Defined.
+Definition thread_idO {SI : sidx} := leibnizO thread_id.
+Global Instance thread_id_equiv {SI : sidx} : Equiv thread_id. apply thread_idO. Defined.
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index 4be297c1195143f40155c74f59276ed9e4019cde..648d179ac142dba3930f8b8edbef233365e21364 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -1,6 +1,6 @@
 (** * SLSLS, Separation Logic Stuttering Local Simulation *)
-
-From iris.algebra Require Export ofe.
+(* Specialize to finite stepindices *)
+From iris.algebra Require Export ofe stepindex_finite.
 From iris.bi Require Import bi fixpoint_mono.
 From iris.proofmode Require Import proofmode.
 From simuliris.simulation Require Import language.
@@ -35,7 +35,7 @@ Section fix_lang.
     (P_s P_t P: prog Λ)
     (σ_s σ_t σ : state Λ).
 
-  Notation expr_rel := (@exprO Λ -d> @exprO Λ -d> PROP).
+  Notation expr_rel := (@exprO _ Λ -d> @exprO _ Λ -d> PROP).
 
   Local Instance expr_rel_func_ne (F: expr_rel → thread_idO -d> expr_rel) `{Hne: !NonExpansive F}:
     (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) F).
@@ -169,7 +169,7 @@ Section fix_lang.
       destruct y as (((Ψ & π') & e_t') & e_s'); simpl.
       destruct Heq as [[[Heq1 Heq2] Heq3] Heq4]; simpl in Heq1, Heq2, Heq3, Heq4.
       eapply sim_expr_inner_ne; eauto.
-      + intros ?????->%leibniz_equiv. by eapply Hg.
+      + intros ????? ->%leibnizO_leibniz. by eapply Hg.
       + intros ????????; rewrite /curry4. eapply Hne.
         repeat split; simpl; done.
   Qed.
diff --git a/theories/stacked_borrows/lang.v b/theories/stacked_borrows/lang.v
index b3c2bcd4effd446084dc92897f88c37d82380c6c..6bd3950eabb854e641c90a9b4d6b0ff8e2fe6710 100644
--- a/theories/stacked_borrows/lang.v
+++ b/theories/stacked_borrows/lang.v
@@ -1,4 +1,4 @@
-(** This file has been adapted from the Stacked Borrows development, available at 
+(** This file has been adapted from the Stacked Borrows development, available at
   https://gitlab.mpi-sws.org/FP/stacked-borrows
 *)
 
@@ -287,11 +287,11 @@ Global Instance result_inhabited : Inhabited result := populate (ValR [☠]%S).
 Global Instance state_Inhabited : Inhabited state.
 Proof. do 2!econstructor; exact: inhabitant. Qed.
 
-Canonical Structure locO := leibnizO loc.
-Canonical Structure scalarO := leibnizO scalar.
-Canonical Structure resultO := leibnizO result.
-Canonical Structure exprO := leibnizO expr.
-Canonical Structure stateO := leibnizO state.
+Canonical Structure locO {SI : sidx} := leibnizO loc.
+Canonical Structure scalarO {SI : sidx} := leibnizO scalar.
+Canonical Structure resultO {SI : sidx} := leibnizO result.
+Canonical Structure exprO {SI : sidx} := leibnizO expr.
+Canonical Structure stateO {SI : sidx} := leibnizO state.
 
 (** Basic properties about the language *)
 
@@ -357,7 +357,7 @@ Inductive base_step (P : prog) :
   expr → state → expr → state → list expr → Prop :=
   | HeadPureS σ e e' efs
       (ExprStep: pure_expr_step P σ.(shp) e e' efs)
-    : base_step P e σ e' σ efs 
+    : base_step P e σ e' σ efs
   | HeadImpureS σ e e' ev h' α' cids' nxtp' nxtc' efs
       (ExprStep : mem_expr_step σ.(shp) e ev h' e' efs)
       (InstrStep: bor_step σ.(sst) σ.(scs) σ.(snp) σ.(snc)
diff --git a/theories/stacked_borrows/tkmap_view.v b/theories/stacked_borrows/tkmap_view.v
index 57b6c38b108433edaab6d6f7c657b77e3056afa8..dcedbe3064fc866f4e66adddce6e450617910c4b 100644
--- a/theories/stacked_borrows/tkmap_view.v
+++ b/theories/stacked_borrows/tkmap_view.v
@@ -1,4 +1,4 @@
-(** This file has been adapted from the Iris development, available at 
+(** This file has been adapted from the Iris development, available at
   https://gitlab.mpi-sws.org/iris/iris
 *)
 
@@ -12,77 +12,80 @@ From simuliris.stacked_borrows Require Export defs.
 (** An adaption of gmap_view to use tag_kind to control permissions of fragments and to reflect that into the authoritative fragment.
 (gmap_view has since been updated so we could now use it directly, but this code predates the generalized gmap_view for arbitrary CRMA.) *)
 
-(* Currently, we place a strong restriction on the shape of a location's stack:
-  A tag can be of one of two kinds:
-  - tk_pub: the tag is public (can be shared, assertion is persistent)
-  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent).
-  - tk_loc: the tag is local
- *)
-(* TODO: allow a local update from tk_unq to tk_pub *)
-Definition tagKindR := csumR (exclR unitO) (csumR (exclR unitO) unitR).
-
-
-Canonical Structure tag_kindO := leibnizO tag_kind.
-
-Global Instance tagKindR_discrete : CmraDiscrete tagKindR.
-Proof. apply _. Qed.
-
-Definition to_tgkR (tk: tag_kind) : tagKindR :=
-  match tk with
-  | tk_unq => Cinr $ Cinl $ Excl ()
-  | tk_pub => Cinr $ Cinr ()
-  | tk_local => Cinl $ Excl ()
-  end.
-
-Lemma to_tgkR_valid tk : ✓ (to_tgkR tk).
-Proof. destruct tk; done. Qed.
-Lemma to_tgkR_validN tk n : ✓{n} (to_tgkR tk).
-Proof. destruct tk; done. Qed.
-
-Global Instance to_tgkR_inj n : Inj (=) (dist n) to_tgkR.
-Proof.
-  intros [] []; simpl; first [done | inversion 1];
-  match goal with
-  | H : Cinl _ ≡{_}≡ Cinr _ |- _ => inversion H
-  | H : Cinr _ ≡{_}≡ Cinl _ |- _ => inversion H
-  end.
-Qed.
-
-Lemma tgkR_validN_inv tkr n : ✓{n} tkr → ∃ tk, tkr ≡ to_tgkR tk.
-Proof.
-  rewrite -cmra_discrete_valid_iff. destruct tkr as [c | [c|c|] | ]; simpl; try by move => [].
-  - destruct c as [u|]; last move => []. destruct u; intros. exists tk_local. done.
-  - destruct c as [u|]; last move => []. destruct u; intros. exists tk_unq. done.
-  - destruct c. intros. exists tk_pub; done.
-Qed.
-
-Global Instance to_tgkR_unq_excl : Exclusive (to_tgkR tk_unq).
-Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
-Global Instance to_tgkR_local_excl : Exclusive (to_tgkR tk_local).
-Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
-Lemma to_tgkR_op_validN n tk tk' : ✓{n} (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
-Proof. destruct tk, tk'; simpl; by intros []. Qed.
-Lemma to_tgkR_op_valid tk tk' : ✓ (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
-Proof. destruct tk, tk'; simpl; by intros []. Qed.
-
-Lemma tagKindR_incl_eq (k1 k2: tagKindR):
-  ✓ k2 → k1 ≼ k2 → k1 ≡ k2.
-Proof.
-  move => VAL /csum_included
-    [?|[[? [? [? [? INCL]]]]|[x1 [x2 [? [? INCL]]]]]]; subst; [done|..].
-  - exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
-  - move : INCL => /csum_included
-      [? |[[? [? [? [? INCL]]]]|[[] [[] [? [? LE]]]]]]; subst; [done|..|done].
-    exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
-Qed.
-
-
-Local Definition tkmap_view_fragUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+Section tag_kind.
+  Context {SI : sidx}.
+
+  (* Currently, we place a strong restriction on the shape of a location's stack:
+    A tag can be of one of two kinds:
+    - tk_pub: the tag is public (can be shared, assertion is persistent)
+    - tk_unq: the tag is unique (cannot be shared, assertion is not persistent).
+    - tk_loc: the tag is local
+   *)
+  (* TODO: allow a local update from tk_unq to tk_pub *)
+  Definition tagKindR := csumR (exclR unitO) (csumR (exclR unitO) unitR).
+
+
+  Canonical Structure tag_kindO := leibnizO tag_kind.
+
+  Global Instance tagKindR_discrete : CmraDiscrete tagKindR.
+  Proof. apply _. Qed.
+
+  Definition to_tgkR (tk: tag_kind) : tagKindR :=
+    match tk with
+    | tk_unq => Cinr $ Cinl $ Excl ()
+    | tk_pub => Cinr $ Cinr ()
+    | tk_local => Cinl $ Excl ()
+    end.
+
+  Lemma to_tgkR_valid tk : ✓ (to_tgkR tk).
+  Proof. destruct tk; done. Qed.
+  Lemma to_tgkR_validN tk n : ✓{n} (to_tgkR tk).
+  Proof. destruct tk; done. Qed.
+
+  Global Instance to_tgkR_inj n : Inj (=) (dist n) to_tgkR.
+  Proof.
+    intros [] []; simpl; first [done | inversion 1];
+    match goal with
+    | H : Cinl _ ≡{_}≡ Cinr _ |- _ => inversion H
+    | H : Cinr _ ≡{_}≡ Cinl _ |- _ => inversion H
+    end.
+  Qed.
+
+  Lemma tgkR_validN_inv tkr n : ✓{n} tkr → ∃ tk, tkr ≡ to_tgkR tk.
+  Proof.
+    rewrite -cmra_discrete_valid_iff. destruct tkr as [c | [c|c|] | ]; simpl; try by move => [].
+    - destruct c as [u|]; last move => []. destruct u; intros. exists tk_local. done.
+    - destruct c as [u|]; last move => []. destruct u; intros. exists tk_unq. done.
+    - destruct c. intros. exists tk_pub; done.
+  Qed.
+
+  Global Instance to_tgkR_unq_excl : Exclusive (to_tgkR tk_unq).
+  Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
+  Global Instance to_tgkR_local_excl : Exclusive (to_tgkR tk_local).
+  Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
+  Lemma to_tgkR_op_validN n tk tk' : ✓{n} (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
+  Proof. destruct tk, tk'; simpl; by intros []. Qed.
+  Lemma to_tgkR_op_valid tk tk' : ✓ (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
+  Proof. destruct tk, tk'; simpl; by intros []. Qed.
+
+  Lemma tagKindR_incl_eq (k1 k2: tagKindR):
+    ✓ k2 → k1 ≼ k2 → k1 ≡ k2.
+  Proof.
+    move => VAL /csum_included
+      [?|[[? [? [? [? INCL]]]]|[x1 [x2 [? [? INCL]]]]]]; subst; [done|..].
+    - exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
+    - move : INCL => /csum_included
+        [? |[[? [? [? [? INCL]]]]|[[] [[] [? [? LE]]]]]]; subst; [done|..|done].
+      exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
+  Qed.
+End tag_kind.
+
+Local Definition tkmap_view_fragUR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ucmra :=
   gmapUR K (prodR tagKindR (agreeR V)).
 (** View relation. *)
 Section rel.
-  Context (K : Type) `{Countable K} (V : ofe).
-  Implicit Types (m : gmap K (tag_kind * V)) (k : K) (v : V) (n : nat).
+  Context {SI : sidx} (K : Type) `{Countable K} (V : ofe).
+  Implicit Types (m : gmap K (tag_kind * V)) (k : K) (v : V) (n : SI).
   Implicit Types (f : gmap K (tagKindR * agree V)).
 
   Local Definition tkmap_view_rel_raw n m f : Prop :=
@@ -93,7 +96,7 @@ Section rel.
     tkmap_view_rel_raw n1 m1 f1 →
     m1 ≡{n2}≡ m2 →
     f2 ≼{n2} f1 →
-    (n2 <= n1)%nat →
+    (n2 ≤ n1)%sidx →
     tkmap_view_rel_raw n2 m2 f2.
   Proof.
     intros Hrel Hm Hf Hn k [tk va] Hk.
@@ -143,7 +146,8 @@ Section rel.
     ∃ m, tkmap_view_rel_raw n m ε.
   Proof. exists ∅. apply: map_Forall_empty. Qed.
 
-  Local Canonical Structure tkmap_view_rel : view_rel (gmapO K (prodO tag_kindO V)) (tkmap_view_fragUR K V) :=
+  Local Canonical Structure tkmap_view_rel :
+      view_rel (gmapO K (prodO tag_kindO V)) (tkmap_view_fragUR K V) :=
     ViewRel tkmap_view_rel_raw tkmap_view_rel_raw_mono
             tkmap_view_rel_raw_valid tkmap_view_rel_raw_unit.
 
@@ -195,15 +199,15 @@ Local Existing Instance tkmap_view_rel_discrete.
 (** [tkmap_view] is a notation to give canonical structure search the chance
 to infer the right instances (see [auth]). *)
 Notation tkmap_view K V := (view (@tkmap_view_rel_raw K _ _ V)).
-Definition tkmap_viewO (K : Type) `{Countable K} (V : ofe) : ofe :=
+Definition tkmap_viewO {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ofe :=
   viewO (tkmap_view_rel K V).
-Definition tkmap_viewR (K : Type) `{Countable K} (V : ofe) : cmra :=
+Definition tkmap_viewR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : cmra :=
   viewR (tkmap_view_rel K V).
-Definition tkmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+Definition tkmap_viewUR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ucmra :=
   viewUR (tkmap_view_rel K V).
 
 Section definitions.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} {K : Type} `{Countable K} {V : ofe}.
 
   Definition tkmap_view_auth (q : frac) (m : gmap K (tag_kind * V)) : tkmap_viewR K V :=
     ●V{#q} m.
@@ -212,16 +216,16 @@ Section definitions.
 End definitions.
 
 Section lemmas.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K (tag_kind * V)) (k : K) (q : Qp) (t : tag_kind) (v : V).
 
-  Global Instance : Params (@tkmap_view_auth) 5 := {}.
+  Global Instance : Params (@tkmap_view_auth) 6 := {}.
   Global Instance tkmap_view_auth_ne q : NonExpansive (tkmap_view_auth (K:=K) (V:=V) q).
   Proof. solve_proper. Qed.
   Global Instance tkmap_view_auth_proper q : Proper ((≡) ==> (≡)) (tkmap_view_auth (K:=K) (V:=V) q).
   Proof. apply ne_proper, _. Qed.
 
-  Global Instance : Params (@tkmap_view_frag) 6 := {}.
+  Global Instance : Params (@tkmap_view_frag) 7 := {}.
   Global Instance tkmap_view_frag_ne k tk : NonExpansive (tkmap_view_frag (K:=K) (V:=V) k tk).
   Proof. solve_proper. Qed.
   Global Instance tkmap_view_frag_proper k tk : Proper ((≡) ==> (≡)) (tkmap_view_frag (K:=K) (V:=V) k tk).
diff --git a/theories/tree_borrows/lang.v b/theories/tree_borrows/lang.v
index 89d58619b8e159d3b4a1fdfbe481f498ed87e04e..9884b3431a08695e7a22f2996c38518a64ac6c77 100755
--- a/theories/tree_borrows/lang.v
+++ b/theories/tree_borrows/lang.v
@@ -295,11 +295,11 @@ Global Instance result_inhabited : Inhabited result := populate (ValR [☠]%S).
 Global Instance state_Inhabited : Inhabited state.
 Proof. do 2!econstructor; exact: inhabitant. Qed.
 
-Canonical Structure locO := leibnizO loc.
-Canonical Structure scalarO := leibnizO scalar.
-Canonical Structure resultO := leibnizO result.
-Canonical Structure exprO := leibnizO expr.
-Canonical Structure stateO := leibnizO state.
+Canonical Structure locO {SI : sidx} := leibnizO loc.
+Canonical Structure scalarO {SI : sidx} := leibnizO scalar.
+Canonical Structure resultO {SI : sidx} := leibnizO result.
+Canonical Structure exprO {SI : sidx} := leibnizO expr.
+Canonical Structure stateO {SI : sidx} := leibnizO state.
 
 (** Basic properties about the language *)
 
@@ -365,7 +365,7 @@ Inductive base_step (P : prog) :
   expr → state → expr → state → list expr → Prop :=
   | HeadPureS σ e e' efs
       (ExprStep: pure_expr_step P σ.(shp) e e' efs)
-    : base_step P e σ e' σ efs 
+    : base_step P e σ e' σ efs
   | HeadImpureS σ e e' ev h' α' cids' nxtp' nxtc' efs
       (ExprStep : mem_expr_step σ.(shp) e ev h' e' efs)
       (InstrStep: bor_step σ.(strs) σ.(scs) σ.(snp) σ.(snc)
diff --git a/theories/tree_borrows/tkmap_view.v b/theories/tree_borrows/tkmap_view.v
index 51c4c5fcfbc198490db1be440dd50398e5b3f091..1be99a3f0151f309cac65161d34eacdb15dfe51d 100755
--- a/theories/tree_borrows/tkmap_view.v
+++ b/theories/tree_borrows/tkmap_view.v
@@ -8,96 +8,98 @@ From simuliris.tree_borrows Require Export defs.
 (** An adaption of gmap_view to use tag_kind to control permissions of fragments and to reflect that into the authoritative fragment.
 (gmap_view has since been updated so we could now use it directly, but this code predates the generalized gmap_view for arbitrary CRMA.) *)
 
-(* Currently, we place a strong restriction on the shape of a location's stack:
-  A tag can be of one of several kinds:
-  - tk_pub: the tag is public (can be shared, assertion is persistent)
-  - tk_unq: the tag is unique (cannot be shared, assertion is not persistent). This is further parameterized by whether it is reserved or activated.
-  - tk_loc: the tag is local (a local variable whose address has not been taken)
- *)
-
-Definition tagKindR := csumR (exclR unitO) (csumR (csumR (exclR unitO) (exclR unitO)) unitR).
-
-Canonical Structure tag_kindO := leibnizO tag_kind.
-
-Global Instance tagKindR_discrete : CmraDiscrete tagKindR.
-Proof. apply _. Qed.
-
-Definition to_tgkR_unq (act : tk_activation_kind) : csumR (exclR unitO) (exclR unitO) :=
-  match act with
-  | tk_res => Cinl $ Excl ()
-  | tk_act => Cinr $ Excl ()
-  end.
-
-Definition to_tgkR (tk: tag_kind) : tagKindR :=
-  match tk with
-  | tk_local => Cinl $ Excl ()
-  | tk_unq variant => Cinr $ Cinl $ to_tgkR_unq variant
-  | tk_pub => Cinr $ Cinr ()
-  end.
-
-Lemma to_tgkR_valid tk : ✓ (to_tgkR tk).
-Proof. destruct tk as [|[]|]; done. Qed.
-Lemma to_tgkR_validN tk n : ✓{n} (to_tgkR tk).
-Proof. destruct tk as [|[]|]; done. Qed.
-
-Global Instance to_tgkR_inj n : Inj (=) (dist n) to_tgkR.
-Proof.
-  intros [|[]|] [|[]|]; simpl; first [done | inversion 1];
-  do 2 match goal with
-  (* Base cases *)
-  | H : Cinl _ ≡{_}≡ Cinr _ |- _ => inversion H
-  | H : Cinr _ ≡{_}≡ Cinl _ |- _ => inversion H
-  (* We need to go deeper *)
-  | H : Cinl _ ≡{_}≡ Cinl _ |- _ => inversion H; clear H
-  | H : Cinr _ ≡{_}≡ Cinr _ |- _ => inversion H; clear H
-  end.
-Qed.
+Section tag_kind.
+  Context {SI : sidx}.
+  (* Currently, we place a strong restriction on the shape of a location's stack:
+    A tag can be of one of several kinds:
+    - tk_pub: the tag is public (can be shared, assertion is persistent)
+    - tk_unq: the tag is unique (cannot be shared, assertion is not persistent). This is further parameterized by whether it is reserved or activated.
+    - tk_loc: the tag is local (a local variable whose address has not been taken)
+   *)
 
-Lemma tgkR_validN_inv tkr n : ✓{n} tkr → ∃ tk, tkr ≡ to_tgkR tk.
-Proof.
-  rewrite -cmra_discrete_valid_iff. destruct tkr as [c | [[c|c|]|c|] | ]; simpl; try by move => [].
-  - destruct c as [u|]; last move => []. destruct u; intros. exists tk_local. done.
-  - destruct c as [u|]; last move => []. destruct u; intros. exists (tk_unq tk_res). done.
-  - destruct c as [u|]; last move => []. destruct u; intros. exists (tk_unq tk_act). done.
-  - destruct c. intros. exists tk_pub; done.
-Qed.
+  Definition tagKindR := csumR (exclR unitO) (csumR (csumR (exclR unitO) (exclR unitO)) unitR).
 
-Global Instance to_tgkR_unq_res_excl : Exclusive (to_tgkR (tk_unq tk_res)).
-Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
-Global Instance to_tgkR_unq_act_excl : Exclusive (to_tgkR (tk_unq tk_act)).
-Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
-Global Instance to_tgkR_local_excl : Exclusive (to_tgkR tk_local).
-Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
-Lemma to_tgkR_not_pub_excl tk : tk ≠ tk_pub → Exclusive (to_tgkR tk).
-Proof. move : tk => [|[]|] H //; apply _. Qed.
-
-Lemma to_tgkR_op_validN n tk tk' : ✓{n} (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
-Proof. destruct tk as [|[]|], tk' as [|[]|]; simpl; by intros []. Qed.
-Lemma to_tgkR_op_valid tk tk' : ✓ (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
-Proof. destruct tk as [|[]|], tk' as [|[]|]; simpl; by intros []. Qed.
-
-Lemma tagKindR_incl_eq (k1 k2: tagKindR):
-  ✓ k2 → k1 ≼ k2 → k1 ≡ k2.
-Proof.
-  move => VAL /csum_included
-    [?|[[? [? [? [? INCL]]]]|[x1 [x2 [? [? INCL]]]]]]; subst; [done|..].
-  { exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _. }
-  f_equiv.
-  move : INCL => /csum_included
-    [?|[[? [? [? [? INCL]]]]|[x3 [x4 [? [? INCL]]]]]]; subst; [done|..].
-  2: { f_equiv. destruct x3, x4. done. }
-  move : INCL => /csum_included
-    [?|[[? [? [? [? INCL]]]]|[x3 [x4 [? [? INCL]]]]]]; subst; [done|..].
-  all: exfalso; eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
-Qed.
+  Canonical Structure tag_kindO := leibnizO tag_kind.
 
+  Global Instance tagKindR_discrete : CmraDiscrete tagKindR.
+  Proof. apply _. Qed.
 
-Local Definition tkmap_view_fragUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+  Definition to_tgkR_unq (act : tk_activation_kind) : csumR (exclR unitO) (exclR unitO) :=
+    match act with
+    | tk_res => Cinl $ Excl ()
+    | tk_act => Cinr $ Excl ()
+    end.
+
+  Definition to_tgkR (tk: tag_kind) : tagKindR :=
+    match tk with
+    | tk_local => Cinl $ Excl ()
+    | tk_unq variant => Cinr $ Cinl $ to_tgkR_unq variant
+    | tk_pub => Cinr $ Cinr ()
+    end.
+
+  Lemma to_tgkR_valid tk : ✓ (to_tgkR tk).
+  Proof. destruct tk as [|[]|]; done. Qed.
+  Lemma to_tgkR_validN tk n : ✓{n} (to_tgkR tk).
+  Proof. destruct tk as [|[]|]; done. Qed.
+
+  Global Instance to_tgkR_inj n : Inj (=) (dist n) to_tgkR.
+  Proof.
+    intros [|[]|] [|[]|]; simpl; first [done | inversion 1];
+    do 2 match goal with
+    (* Base cases *)
+    | H : Cinl _ ≡{_}≡ Cinr _ |- _ => inversion H
+    | H : Cinr _ ≡{_}≡ Cinl _ |- _ => inversion H
+    (* We need to go deeper *)
+    | H : Cinl _ ≡{_}≡ Cinl _ |- _ => inversion H; clear H
+    | H : Cinr _ ≡{_}≡ Cinr _ |- _ => inversion H; clear H
+    end.
+  Qed.
+
+  Lemma tgkR_validN_inv tkr n : ✓{n} tkr → ∃ tk, tkr ≡ to_tgkR tk.
+  Proof.
+    rewrite -cmra_discrete_valid_iff. destruct tkr as [c | [[c|c|]|c|] | ]; simpl; try by move => [].
+    - destruct c as [u|]; last move => []. destruct u; intros. exists tk_local. done.
+    - destruct c as [u|]; last move => []. destruct u; intros. exists (tk_unq tk_res). done.
+    - destruct c as [u|]; last move => []. destruct u; intros. exists (tk_unq tk_act). done.
+    - destruct c. intros. exists tk_pub; done.
+  Qed.
+
+  Global Instance to_tgkR_unq_res_excl : Exclusive (to_tgkR (tk_unq tk_res)).
+  Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
+  Global Instance to_tgkR_unq_act_excl : Exclusive (to_tgkR (tk_unq tk_act)).
+  Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
+  Global Instance to_tgkR_local_excl : Exclusive (to_tgkR tk_local).
+  Proof. intros [ | [ [] | [] | ]| ]; simpl; [ intros [] ..]. Qed.
+  Lemma to_tgkR_not_pub_excl tk : tk ≠ tk_pub → Exclusive (to_tgkR tk).
+  Proof. move : tk => [|[]|] H //; apply _. Qed.
+
+  Lemma to_tgkR_op_validN n tk tk' : ✓{n} (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
+  Proof. destruct tk as [|[]|], tk' as [|[]|]; simpl; by intros []. Qed.
+  Lemma to_tgkR_op_valid tk tk' : ✓ (to_tgkR tk ⋅ to_tgkR tk') → tk = tk_pub ∧ tk' = tk_pub.
+  Proof. destruct tk as [|[]|], tk' as [|[]|]; simpl; by intros []. Qed.
+
+  Lemma tagKindR_incl_eq (k1 k2: tagKindR):
+    ✓ k2 → k1 ≼ k2 → k1 ≡ k2.
+  Proof.
+    move => VAL /csum_included
+      [?|[[? [? [? [? INCL]]]]|[x1 [x2 [? [? INCL]]]]]]; subst; [done|..].
+    { exfalso. eapply exclusive_included; [..|apply INCL|apply VAL]; apply _. }
+    f_equiv.
+    move : INCL => /csum_included
+      [?|[[? [? [? [? INCL]]]]|[x3 [x4 [? [? INCL]]]]]]; subst; [done|..].
+    2: { f_equiv. destruct x3, x4. done. }
+    move : INCL => /csum_included
+      [?|[[? [? [? [? INCL]]]]|[x3 [x4 [? [? INCL]]]]]]; subst; [done|..].
+    all: exfalso; eapply exclusive_included; [..|apply INCL|apply VAL]; apply _.
+  Qed.
+End tag_kind.
+
+Local Definition tkmap_view_fragUR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ucmra :=
   gmapUR K (prodR tagKindR (agreeR V)).
 (** View relation. *)
 Section rel.
-  Context (K : Type) `{Countable K} (V : ofe).
-  Implicit Types (m : gmap K (tag_kind * V)) (k : K) (v : V) (n : nat).
+  Context {SI : sidx} (K : Type) `{Countable K} (V : ofe).
+  Implicit Types (m : gmap K (tag_kind * V)) (k : K) (v : V) (n : SI).
   Implicit Types (f : gmap K (tagKindR * agree V)).
 
   Local Definition tkmap_view_rel_raw n m f : Prop :=
@@ -108,7 +110,7 @@ Section rel.
     tkmap_view_rel_raw n1 m1 f1 →
     m1 ≡{n2}≡ m2 →
     f2 ≼{n2} f1 →
-    (n2 <= n1)%nat →
+    (n2 ≤ n1)%sidx →
     tkmap_view_rel_raw n2 m2 f2.
   Proof.
     intros Hrel Hm Hf Hn k [tk va] Hk.
@@ -210,15 +212,15 @@ Local Existing Instance tkmap_view_rel_discrete.
 (** [tkmap_view] is a notation to give canonical structure search the chance
 to infer the right instances (see [auth]). *)
 Notation tkmap_view K V := (view (@tkmap_view_rel_raw K _ _ V)).
-Definition tkmap_viewO (K : Type) `{Countable K} (V : ofe) : ofe :=
+Definition tkmap_viewO {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ofe :=
   viewO (tkmap_view_rel K V).
-Definition tkmap_viewR (K : Type) `{Countable K} (V : ofe) : cmra :=
+Definition tkmap_viewR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : cmra :=
   viewR (tkmap_view_rel K V).
-Definition tkmap_viewUR (K : Type) `{Countable K} (V : ofe) : ucmra :=
+Definition tkmap_viewUR {SI : sidx} (K : Type) `{Countable K} (V : ofe) : ucmra :=
   viewUR (tkmap_view_rel K V).
 
 Section definitions.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} {K : Type} `{Countable K} {V : ofe}.
 
   Definition tkmap_view_auth (q : frac) (m : gmap K (tag_kind * V)) : tkmap_viewR K V :=
     ●V{#q} m.
@@ -227,16 +229,16 @@ Section definitions.
 End definitions.
 
 Section lemmas.
-  Context {K : Type} `{Countable K} {V : ofe}.
+  Context {SI : sidx} {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K (tag_kind * V)) (k : K) (q : Qp) (t : tag_kind) (v : V).
 
-  Global Instance : Params (@tkmap_view_auth) 5 := {}.
+  Global Instance : Params (@tkmap_view_auth) 6 := {}.
   Global Instance tkmap_view_auth_ne q : NonExpansive (tkmap_view_auth (K:=K) (V:=V) q).
   Proof. solve_proper. Qed.
   Global Instance tkmap_view_auth_proper q : Proper ((≡) ==> (≡)) (tkmap_view_auth (K:=K) (V:=V) q).
   Proof. apply ne_proper, _. Qed.
 
-  Global Instance : Params (@tkmap_view_frag) 6 := {}.
+  Global Instance : Params (@tkmap_view_frag) 7 := {}.
   Global Instance tkmap_view_frag_ne k tk : NonExpansive (tkmap_view_frag (K:=K) (V:=V) k tk).
   Proof. solve_proper. Qed.
   Global Instance tkmap_view_frag_proper k tk : Proper ((≡) ==> (≡)) (tkmap_view_frag (K:=K) (V:=V) k tk).
@@ -453,8 +455,8 @@ Section lemmas.
     tkmap_view_auth 1 m â‹… tkmap_view_frag k tk_unq v ~~>
       tkmap_view_auth 1 (<[k := (tk_pub, v)]> m) â‹… tkmap_view_frag k tk_pub v.
   Proof.
-     TODO: change def of tgkR to enable local update tk_unq ~~> tk_pub 
-  Abort. 
+     TODO: change def of tgkR to enable local update tk_unq ~~> tk_pub
+  Abort.
   Proof.
     apply view_update_frag=>m n bf Hrel j [df va] /=.
     rewrite lookup_op. destruct (decide (j = k)) as [->|Hne].