update dependencies

coq-iris-examples.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-08-04.2.b9e591f8") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-08-29.5.af0a091b") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/hocap/cg_bag.v

@@ -13,6 +13,8 @@ From iris.heap_lang.lib Require Import lock spin_lock.
 From iris_examples.hocap Require Import abstract_bag.
 From iris.prelude Require Import options.
 
+Local Existing Instance spin_lock.
+
 (** Coarse-grained bag implementation using a spin lock *)
 Definition newBag : val := λ: <>,
   let: "r" := ref NONE in

theories/logatom/counter_with_backup/counter_proof.v

@@ -14,7 +14,7 @@ From iris.prelude Require Import options.
 (** As explained in the paper, we build upon the abstract logically-atomic heap defined in [atomic_heap.v], not HeapLang's built-in heap primitives. *)
 
 Section counter_impl.
-  Context {Σ : gFunctors} `{!heapGS Σ, !atomic_heap}.
+  Context `{!atomic_heap}.
   Import atomic_heap.notation.
   (** ** Definition of the operations. *)
 
@@ -88,7 +88,7 @@ Proof. solve_inG. Qed.
 Section counter_proof.
   Context {Σ: gFunctors}.
   Context `{!heapGS Σ}
-          `{!atomic_heap}
+          `{!atomic_heap, !atomic_heapGS Σ}
           `{!counterG Σ}.
   Context (N: namespace).
   Import atomic_heap.notation.
@@ -640,7 +640,7 @@ Section counter_proof.
 End counter_proof.
 
 (** Our particular counter is an instance of the logically-atomic counter interface *)
-Program Definition atomic_counter `{!heapGS Σ, counterG Σ} `{!atomic_heap} :
+Program Definition atomic_counter `{!heapGS Σ, counterG Σ} `{!atomic_heap, atomic_heapGS Σ} :
   atomic_counter Σ :=
   {|
       counter_spec.new_counter_spec := new_counter_spec;
@@ -649,10 +649,10 @@ Program Definition atomic_counter `{!heapGS Σ, counterG Σ} `{!atomic_heap} :
       counter_spec.get_backup_spec := get_backup_spec;
   |}.
 Next Obligation.
-  intros ????[] ?. rewrite /value. apply _.
+  intros Σ ????? [] ?. rewrite /value. apply _.
 Qed.
 Next Obligation.
-  intros ???? [γ_cnt γ_ex] ??. iIntros "[_ H1] [_ H2]".
+  intros Σ ????? [γ_cnt γ_ex] ??. iIntros "[_ H1] [_ H2]".
   iCombine "H1 H2" gives %[].
 Qed.
 

theories/logatom/elimination_stack/stack.v

@@ -23,11 +23,7 @@ Global Instance subG_stackΣ {Σ} : subG stackΣ Σ → stackG Σ.
 Proof. solve_inG. Qed.
 
 Section stack.
-  Context `{!heapGS Σ, !stackG Σ, !atomic_heap} (N : namespace).
-  Notation iProp := (iProp Σ).
-
-  Let offerN := N .@ "offer".
-  Let stackN := N .@ "stack".
+  Context `{!atomic_heap}.
 
   Import atomic_heap.notation.
 
@@ -87,6 +83,13 @@ Section stack.
           end
       end.
 
+  (** * Proof *)
+  Context `{!heapGS Σ, !stackG Σ, !atomic_heapGS Σ} (N : namespace).
+  Notation iProp := (iProp Σ).
+
+  Let offerN := N .@ "offer".
+  Let stackN := N .@ "stack".
+
   (** Invariant and protocol. *)
   Definition stack_content (γs : gname) (l : list val) : iProp :=
     (own γs (◯ Excl' l))%I.
@@ -364,7 +367,7 @@ Section stack.
 
 End stack.
 
-Definition elimination_stack `{!heapGS Σ, !stackG Σ, !atomic_heap} :
+Definition elimination_stack `{!heapGS Σ, !stackG Σ, !atomic_heap, !atomic_heapGS Σ} :
   atomic_stack Σ :=
   {| spec.new_stack_spec := new_stack_spec;
      spec.push_spec := push_spec;

theories/logatom/flat_combiner/atomic_sync.v

@@ -15,7 +15,7 @@ Global Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
 Proof. solve_inG. Qed.
 
 Section atomic_sync.
-  Context `{EqDecision A, !heapGS Σ, !lockG Σ}.
+  Context `{EqDecision A, !heapGS Σ}.
   Canonical AO := leibnizO A.
   Context `{!inG Σ (prodR fracR (agreeR AO))}.
 

theories/logatom/flat_combiner/flat.v

@@ -10,6 +10,8 @@ From iris.prelude Require Import options.
 
 Set Default Proof Using "Type*".
 
+Local Existing Instance spin_lock.
+
 Definition doOp : val :=
   λ: "p",
      match: !"p" with
@@ -19,7 +21,8 @@ Definition doOp : val :=
 
 Definition try_srv : val :=
   λ: "lk" "s",
-    if: try_acquire "lk"
+    (* try_acquire is not part of the lock interface so we poke the abstraction *)
+    if: spin_lock.try_acquire "lk"
       then let: "hd" := !"s" in
            treiber.iter "hd" doOp;;
            release "lk"
@@ -219,7 +222,7 @@ Section proof.
     ⊢ WP try_srv lk #s {{ Φ }}.
   Proof.
     iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
-    wp_apply (try_acquire_spec with "[]"); first done.
+    wp_apply (spin_lock.try_acquire_spec with "[]"); first done.
     iIntros ([]); last by (iIntros; wp_if).
     iIntros "[Hlocked [Ho2 HR]]".
     wp_if. wp_bind (! _)%E.

theories/logatom/flat_combiner/simple_sync.v

@@ -8,6 +8,8 @@ From iris_examples.logatom.flat_combiner Require Import sync.
 From iris.prelude Require Import options.
 Import uPred.
 
+Local Existing Instance spin_lock.
+
 Definition mk_sync: val :=
   λ: <>,
        let: "l" := newlock #() in