From 9c584bab0ff4423f5ea9f156faecbfe16e53a00c Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Thu, 1 Feb 2024 11:43:01 +0100
Subject: [PATCH] Added forwarder example

---
 .../multi_proto_consistency_examples.v        | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/theories/channel/multi_proto_consistency_examples.v b/theories/channel/multi_proto_consistency_examples.v
index 78e48a6..826b9b4 100644
--- a/theories/channel/multi_proto_consistency_examples.v
+++ b/theories/channel/multi_proto_consistency_examples.v
@@ -628,3 +628,41 @@ Section two_buyer_ref.
   Qed.
 
 End two_buyer_ref.
+
+
+Section fwd.
+  Context `{!heapGS Σ}.
+
+  Definition iProto_fwd : gmap nat (iProto Σ) :=
+    <[0 := (<(Send, 1) @ (x:Z)> MSG #x ;
+            <(Send, 1) @ (b:bool)> MSG #b ;
+            <(Send, if b then 2 else 3) > MSG #x ; END)%proto]>
+   (<[1 := (<(Recv, 0) @ (x:Z)> MSG #x ;
+            <(Recv, 0) @ (b:bool)> MSG #b;
+            if b
+            then <(Send,2)> MSG #x ; END
+            else <(Send,3)> MSG #x ; END)%proto]>
+   (<[2 := (<(Recv, 1) @ (x:Z)> MSG #x ;
+            <(Send, 0)> MSG #x ; END)%proto]>
+   (<[3 := (<(Recv, 1) @ (x:Z)> MSG #x ;
+            <(Send, 0)> MSG #x ; END)%proto]> ∅))).
+
+  Lemma iProto_fwd_consistent :
+    ⊢ iProto_consistent iProto_fwd.
+  Proof.
+    rewrite /iProto_fwd.
+    iProto_consistent_take_step.
+    iIntros (x) "_". iExists _. iSplit; [done|]. iSplit; [done|].
+    iProto_consistent_take_step.
+    iIntros ([]) "_".
+    - iExists _. iSplit; [done|]. iSplit; [done|].
+      iProto_consistent_take_step.
+      iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
+      iProto_consistent_take_step.
+    - iExists _. iSplit; [done|]. iSplit; [done|].
+      iProto_consistent_take_step.
+      iIntros "_". iExists _. iSplit; [done|]. iSplit; [done|].
+      iProto_consistent_take_step.
+  Qed.
+
+End fwd.
-- 
GitLab