From d15f9f6a199b27ccb5cf0151e5bb11e4eb384c47 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Thu, 10 Apr 2025 15:50:25 +0200
Subject: [PATCH] More clean up
---
multris/channel/channel.v | 2 +-
multris/channel/proto.v | 6 ++++++
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/multris/channel/channel.v b/multris/channel/channel.v
index 0c6d359..6f6e129 100644
--- a/multris/channel/channel.v
+++ b/multris/channel/channel.v
@@ -290,7 +290,7 @@ Section channel.
iRewrite -"Hagree'". iApply iProto_le_refl.
Qed.
- Lemma send_spec_tele {TT} c i (tt : TT)
+ Lemma send_spec_tele {TT} c i (tt : TT)
(v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
{{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
send c #i (v tt)
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index d13056f..dffe214 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -1423,6 +1423,12 @@ Section proto.
iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
iAssert (▷ (<[i:=<(Send, j)> m1]>ps !! j ≡ Some pj))%I as "Hpj'".
{ by rewrite list_lookup_insert_ne. }
+ (* iAssert (▷ (⌜is_Some (ps !! i)⌝ ∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]" *)
+ (* as "[Hi' Hile]". *)
+ (* { iNext. iFrame. destruct (ps !! i); [done|]. by rewrite option_equivI. } *)
+ (* iAssert (▷ (⌜is_Some (ps !! j)⌝ ∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]" *)
+ (* as "[Hj' Hjle]". *)
+ (* { iNext. iFrame. destruct (ps !! j); [done|]. by rewrite !option_equivI. } *)
iDestruct (iProto_consistent_le with "Hconsistent Hpi Hile") as "Hconsistent".
iDestruct (iProto_consistent_le with "Hconsistent Hpj' Hjle") as "Hconsistent".
iDestruct (iProto_consistent_step _ _ _ i 0 j 0 with "Hconsistent [] [] [Hm //]") as
--
GitLab