From d4b1567add962b76e5247055772ad92f86c0293a Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 27 Mar 2024 19:49:17 +0100
Subject: [PATCH] Added adequacy proof for ring leader election

---
 multi_actris/examples/leader_election.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/multi_actris/examples/leader_election.v b/multi_actris/examples/leader_election.v
index e8810fc..0fa6ef5 100644
--- a/multi_actris/examples/leader_election.v
+++ b/multi_actris/examples/leader_election.v
@@ -1,5 +1,6 @@
-From multi_actris.channel Require Import proofmode.
+From iris.heap_lang Require Import adequacy.
 From iris.heap_lang.lib Require Import assert.
+From multi_actris.channel Require Import proofmode.
 
 (** Inspired by https://en.wikipedia.org/wiki/Chang_and_Roberts_algorithm *)
 
@@ -195,3 +196,11 @@ Section ring_leader_election_example.
   Qed.
 
 End ring_leader_election_example.
+
+Lemma program_spec_adequate :
+  adequate NotStuck (program #()) ({|heap := ∅; used_proph_id := ∅|})
+           (λ _ _, True).
+Proof.
+  apply (heap_adequacy #[heapΣ; chanΣ]).
+  iIntros (Σ) "H". by iApply program_spec.
+Qed.
-- 
GitLab