From 18f784adb884ac14edd3eb19610d0b3fd62f4985 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 6 Jul 2024 08:20:42 +0200
Subject: [PATCH] Don't leak that locks are used internally in channels.

---
 theories/channel/channel.v          | 4 ++--
 theories/examples/pizza.v           | 2 +-
 theories/logrel/examples/par_recv.v | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 52e1062..4ab5fe0 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -68,8 +68,8 @@ Definition recv : val :=
 
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
-  chanG_lockG :: lockG Σ;
-  chanG_protoG :: protoG Σ val;
+  #[local] chanG_lockG :: lockG Σ;
+  #[local] chanG_protoG :: protoG Σ val;
 }.
 Definition chanΣ : gFunctors := #[ spin_lockΣ; protoΣ val ].
 Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
diff --git a/theories/examples/pizza.v b/theories/examples/pizza.v
index b567488..c0d9a33 100644
--- a/theories/examples/pizza.v
+++ b/theories/examples/pizza.v
@@ -129,7 +129,7 @@ Section example.
        "v2")
     ).
 
-  Lemma lock_example_spec jcc rcc c (x1 y1 : Z) :
+  Lemma lock_example_spec `{!lockG Σ} jcc rcc c (x1 y1 : Z) :
     {{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
       lock_example #jcc #rcc c
     {{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;
diff --git a/theories/logrel/examples/par_recv.v b/theories/logrel/examples/par_recv.v
index fb9a56d..b512bc0 100755
--- a/theories/logrel/examples/par_recv.v
+++ b/theories/logrel/examples/par_recv.v
@@ -35,7 +35,7 @@ Definition prog : val := λ: "c",
   ).
 
 Section double.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ fracR}.
 
   Definition prog_prot : iProto Σ :=
@@ -119,7 +119,7 @@ Section double.
 End double.
 
 Section double_fc.
-  Context `{heapGS Σ, chanG Σ, spawnG Σ}.
+  Context `{!heapGS Σ, !chanG Σ, !spawnG Σ, !lockG Σ}.
   Context `{!inG Σ (exclR unitO), inG Σ (prodR fracR (agreeR (optionO valO)))}.
 
   Definition prog_prot_fc (P : val → val → iProp Σ) : iProto Σ :=
-- 
GitLab