From 90edf73754629cef47a65a25c28f03dc0fa42364 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Thu, 23 Jan 2025 17:02:45 +0100
Subject: [PATCH] Renamed multi_actris into multris
---
_CoqProject | 22 +-
multi_actris/channel/matrix.v | 221 ---
multi_actris/channel/proto_alt.v | 1417 -----------------
multi_actris/examples/leader_election.v | 206 ---
multi_actris/examples/leader_election_del.v | 276 ----
{multi_actris => multris}/channel/channel.v | 8 +-
{multi_actris => multris}/channel/proofmode.v | 4 +-
{multi_actris => multris}/channel/proto.v | 2 +-
.../channel/proto_model.v | 2 +-
{multi_actris => multris}/examples/basics.v | 2 +-
.../examples/leader_election.v | 2 +-
.../examples/three_buyer.v | 2 +-
.../examples/two_buyer.v | 2 +-
.../utils/cofe_solver_2.v | 0
{multi_actris => multris}/utils/matrix.v | 0
15 files changed, 23 insertions(+), 2143 deletions(-)
delete mode 100644 multi_actris/channel/matrix.v
delete mode 100644 multi_actris/channel/proto_alt.v
delete mode 100644 multi_actris/examples/leader_election.v
delete mode 100644 multi_actris/examples/leader_election_del.v
rename {multi_actris => multris}/channel/channel.v (98%)
rename {multi_actris => multris}/channel/proofmode.v (99%)
rename {multi_actris => multris}/channel/proto.v (99%)
rename {multi_actris => multris}/channel/proto_model.v (99%)
rename {multi_actris => multris}/examples/basics.v (99%)
rename multi_actris/examples/leader_election_del_alt.v => multris/examples/leader_election.v (99%)
rename {multi_actris => multris}/examples/three_buyer.v (99%)
rename {multi_actris => multris}/examples/two_buyer.v (98%)
rename {multi_actris => multris}/utils/cofe_solver_2.v (100%)
rename {multi_actris => multris}/utils/matrix.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 5baef5e..1041167 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,5 @@
-Q actris actris
--Q multi_actris multi_actris
+-Q multris multris
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
@@ -52,13 +52,13 @@ actris/logrel/examples/mapper_list.v
actris/logrel/examples/compute_service.v
actris/logrel/examples/compute_client_list.v
-multi_actris/utils/cofe_solver_2.v
-multi_actris/utils/matrix.v
-multi_actris/channel/proto_model.v
-multi_actris/channel/proto.v
-multi_actris/channel/channel.v
-multi_actris/channel/proofmode.v
-multi_actris/examples/basics.v
-multi_actris/examples/two_buyer.v
-multi_actris/examples/three_buyer.v
-multi_actris/examples/leader_election.v
+multris/utils/cofe_solver_2.v
+multris/utils/matrix.v
+multris/channel/proto_model.v
+multris/channel/proto.v
+multris/channel/channel.v
+multris/channel/proofmode.v
+multris/examples/basics.v
+multris/examples/two_buyer.v
+multris/examples/three_buyer.v
+multris/examples/leader_election.v
diff --git a/multi_actris/channel/matrix.v b/multi_actris/channel/matrix.v
deleted file mode 100644
index 9b642da..0000000
--- a/multi_actris/channel/matrix.v
+++ /dev/null
@@ -1,221 +0,0 @@
-From iris.bi Require Import big_op.
-From iris.heap_lang Require Export primitive_laws notation proofmode.
-
-Definition new_matrix : val :=
- λ: "m" "n" "v", (AllocN ("m"*"n") "v","m","n").
-
-Definition pos (n i j : nat) : nat := i * n + j.
-Definition vpos : val := λ: "n" "i" "j", "i"*"n" + "j".
-
-Definition matrix_get : val :=
- λ: "m" "i" "j",
- let: "l" := Fst (Fst "m") in
- let: "n" := Snd "m" in
- "l" +â‚— vpos "n" "i" "j".
-
-Section with_Σ.
- Context `{heapGS Σ}.
-
- Definition is_matrix (v : val) (m n : nat)
- (P : nat → nat → loc → iProp Σ) : iProp Σ :=
- ∃ (l:loc),
- ⌜v = PairV (PairV #l #m) #n⌠∗
- [∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- P i j (l +â‚— pos n i j).
-
-
- Lemma array_to_matrix_pre l n m v :
- l ↦∗ replicate (n * m) v -∗
- [∗ list] i ↦ _ ∈ replicate n (), (l +ₗ i*m) ↦∗ replicate m v.
- Proof.
- iIntros "Hl".
- iInduction n as [|n] "IHn"; [done|].
- replace (S n) with (n + 1) by lia.
- replace ((n + 1) * m) with (n * m + m) by lia.
- rewrite !replicate_add /= array_app=> /=.
- iDestruct "Hl" as "[Hl Hls]".
- iDestruct ("IHn" with "Hl") as "Hl".
- iFrame=> /=.
- rewrite Nat.add_0_r !replicate_length.
- replace (Z.of_nat (n * m)) with (Z.of_nat n * Z.of_nat m)%Z by lia.
- by iFrame.
- Qed.
-
- (* TODO: rename *)
- Lemma big_sepL_replicate_type {A B} n (x1 : A) (x2 : B) (P : nat → iProp Σ) :
- ([∗ list] i ↦ _ ∈ replicate n x1, P i) ⊢
- ([∗ list] i ↦ _ ∈ replicate n x2, P i).
- Proof.
- iIntros "H".
- iInduction n as [|n] "IHn"; [done|].
- replace (S n) with (n + 1) by lia.
- rewrite !replicate_add /=. iDestruct "H" as "[H1 H2]".
- iSplitL "H1"; [by iApply "IHn"|]=> /=.
- by rewrite !replicate_length.
- Qed.
-
- Lemma array_to_matrix l m n v :
- l ↦∗ replicate (m * n) v -∗
- [∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- (l +ₗ pos n i j) ↦ v.
- Proof.
- iIntros "Hl".
- iDestruct (array_to_matrix_pre with "Hl") as "Hl".
- iApply (big_sepL_impl with "Hl").
- iIntros "!>" (i ? _) "Hl".
- iApply big_sepL_replicate_type.
- iApply (big_sepL_impl with "Hl").
- iIntros "!>" (j ? HSome) "Hl".
- rewrite Loc.add_assoc.
- replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
- (Z.of_nat (i * n + j))%Z by lia.
- by apply lookup_replicate in HSome as [-> _].
- Qed.
-
- Lemma new_matrix_spec m n v P :
- 0 < m → 0 < n →
- {{{ [∗ list] i ↦ _ ∈ replicate m (), [∗ list] j ↦ _ ∈ replicate n (),
- ∀ l, l ↦ v -∗ P i j l }}}
- (* {{{ (∀ i j l, ⌜i < m⌠-∗ ⌜j < n⌠-∗ l ↦ v -∗ P i j l) }}} *)
- new_matrix #m #n v
- {{{ mat, RET mat; is_matrix mat m n P }}}.
- Proof.
- iIntros (Hm Hn Φ) "HP HΦ".
- wp_lam. wp_pures.
- wp_smart_apply wp_allocN; [lia|done|].
- iIntros (l) "[Hl _]".
- wp_pures. iApply "HΦ".
- iModIntro.
- iExists _. iSplit; [done|].
- replace (Z.to_nat (Z.of_nat m * Z.of_nat n)) with (m * n) by lia.
- iDestruct (array_to_matrix with "Hl") as "Hl".
- iCombine "HP Hl" as "HPl".
- rewrite -big_sepL_sep.
- iApply (big_sepL_impl with "HPl").
- iIntros "!>" (k x Hin) "H".
- rewrite -big_sepL_sep.
- iApply (big_sepL_impl with "H").
- iIntros "!>" (k' x' Hin') "[HP Hl]".
- by iApply "HP".
- Qed.
-
- Lemma matrix_sep m n l (P : _ → _ → _ → iProp Σ) i j :
- i < m → j < n →
- ([∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- P i j (l +ₗ pos n i j)) -∗
- (P i j (l +ₗ pos n i j) ∗
- (P i j (l +ₗ pos n i j) -∗
- ([∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- P i j (l +â‚— pos n i j)))).
- Proof.
- iIntros (Hm Hn) "Hm".
- iDestruct (big_sepL_impl with "Hm []") as "Hm".
- { iIntros "!>" (k x HIn).
- iApply (big_sepL_lookup_acc _ _ j ()).
- by apply lookup_replicate. }
- simpl.
- rewrite {1}(big_sepL_lookup_acc _ (replicate m ()) i ());
- [|by apply lookup_replicate].
- iDestruct "Hm" as "[[Hij Hi] Hm]".
- iFrame.
- iIntros "HP".
- iDestruct ("Hm" with "[$Hi $HP]") as "Hm".
- iApply (big_sepL_impl with "Hm").
- iIntros "!>" (k x Hin).
- iIntros "[Hm Hm']". iApply "Hm'". done.
- Qed.
-
- Lemma matrix_sep_pers m n l (P : _ → _ → _ → iProp Σ) i j :
- (∀ i j l, Persistent (P i j l)) →
- i < m → j < n →
- ([∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- P i j (l +ₗ pos n i j)) -∗
- (P i j (l +ₗ pos n i j) ∗
- (([∗ list] i ↦ _ ∈ replicate m (),
- [∗ list] j ↦ _ ∈ replicate n (),
- P i j (l +â‚— pos n i j)))).
- Proof.
- iIntros (Hpers Hm Hn) "Hm".
- iDestruct (matrix_sep with "Hm") as "[#HP Hm]"; [done..|].
- iFrame "#". by iApply "Hm".
- Qed.
-
- (* Lemma is_matrix_sep m n v P i j : *)
- (* i < m → j < n → *)
- (* is_matrix v m n P -∗ (∃ l, P i j l ∗ (P i j l -∗ is_matrix v m n P)). *)
- (* Proof. *)
- (* iDestruct 1 as (l ->) "Hm". *)
- (* iDestruct (big_sepL_impl with "Hm []") as "Hm". *)
- (* { iIntros "!>" (k x HIn). *)
- (* iApply (big_sepL_lookup_acc _ _ j ()). *)
- (* by apply lookup_replicate. } *)
- (* simpl. *)
- (* rewrite {1}(big_sepL_lookup_acc _ (replicate m ()) i ()); *)
- (* [|by apply lookup_replicate]. *)
- (* iDestruct "Hm" as "[[Hij Hi] Hm]". *)
- (* iExists (l +â‚— pos n i j). *)
- (* iFrame. *)
- (* iIntros "HP". *)
- (* iExists _. iSplit; [done|]. *)
- (* iDestruct ("Hm" with "[$Hi $HP]") as "Hm". *)
- (* iApply (big_sepL_impl with "Hm"). *)
- (* iIntros "!>" (k x Hin). *)
- (* iIntros "[Hm Hm']". iApply "Hm'". done. *)
- (* Qed. *)
-
- Lemma vpos_spec (n i j : nat) :
- {{{ True }}} vpos #n #i #j {{{ RET #(pos n i j); True }}}.
- Proof.
- iIntros (Φ) "_ HΦ". wp_lam. wp_pures. rewrite /pos.
- replace (Z.of_nat i * Z.of_nat n + Z.of_nat j)%Z with
- (Z.of_nat (i * n + j)) by lia.
- by iApply "HΦ".
- Qed.
-
- Lemma matrix_get_spec m n i j v P :
- i < m → j < n →
- {{{ is_matrix v m n P }}}
- matrix_get v #i #j
- {{{ l, RET #l; P i j l ∗ (P i j l -∗ is_matrix v m n P) }}}.
- Proof.
- iIntros (Hm Hn Φ) "Hm HΦ".
- wp_lam.
- iDestruct "Hm" as (l ->) "Hm".
- wp_pures.
- wp_smart_apply vpos_spec; [done|].
- iIntros "_".
- wp_pures.
- iApply "HΦ".
- iModIntro.
- iDestruct (matrix_sep _ _ _ _ i j with "Hm") as "[$ Hm]"; [lia|lia|].
- iIntros "H".
- iDestruct ("Hm" with "H") as "Hm".
- iExists _. iSplit; [done|]. iFrame.
- Qed.
-
- Lemma matrix_get_spec_pers m n i j v P :
- (∀ i j l, Persistent (P i j l)) →
- i < m → j < n →
- {{{ is_matrix v m n P }}}
- matrix_get v #i #j
- {{{ l, RET #l; P i j l ∗ is_matrix v m n P }}}.
- Proof.
- iIntros (Hpers Hm Hn Φ) "Hm HΦ".
- wp_lam.
- iDestruct "Hm" as (l ->) "Hm".
- wp_pures.
- wp_smart_apply vpos_spec; [done|].
- iIntros "_".
- wp_pures.
- iApply "HΦ".
- iModIntro.
- iDestruct (matrix_sep_pers _ _ _ _ i j with "Hm") as "[$ Hm]"; [lia|lia|].
- iExists _. iSplit; [done|]. iFrame.
- Qed.
-
-End with_Σ.
diff --git a/multi_actris/channel/proto_alt.v b/multi_actris/channel/proto_alt.v
deleted file mode 100644
index 1b4f380..0000000
--- a/multi_actris/channel/proto_alt.v
+++ /dev/null
@@ -1,1417 +0,0 @@
-(** This file defines the core of the Actris logic: It defines dependent
-separation protocols and the various operations on it like dual, append, and
-branching.
-
-Dependent separation protocols [iProto] are defined by instantiating the
-parameterized version in [proto_model] with the type of propositions [iProp] of Iris.
-We define ways of constructing instances of the instantiated type via two
-constructors:
-- [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
- sequence of binders [iMsg_exist], terminated by the payload constructed with
- [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
- carried proposition and the [iProto] tail, respectively.
-
-For convenience sake, we provide the following notations:
-- [END], which is simply [iProto_end].
-- [∃ x, m], which is [iMsg_exist] with argument [m].
-- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
-- [<a> m], which is [iProto_message] with arguments [a] and [m].
-
-We also include custom notation to more easily construct complete constructions:
-- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
-- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
-
-Futhermore, we define the following operations:
-- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
-- [iProto_app], which appends two protocols.
-
-In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
-the following inductive definition for asynchronous subtyping on session types:
-
- p1 <: p2 p1 <: p2 p1 <: !B.p3 ?A.p3 <: p2
----------- ---------------- ---------------- ----------------------------
-end <: end !A.p1 <: !A.p2 ?A.p1 <: ?A.p2 ?A.p1 <: !B.p2
-
-Example:
-
-!R <: !R ?Q <: ?Q ?Q <: ?Q
-------------------- --------------
-?Q.!R <: !R.?Q ?P.?Q <: ?P.?Q
-------------------------------------
- ?P.?Q.!R <: !R.?P.?Q
-
-Lastly, relevant type classes instances are defined for each of the above
-notions, such as contractiveness and non-expansiveness, after which the
-specifications of the message-passing primitives are defined in terms of the
-protocol connectives. *)
-From iris.algebra Require Import gmap excl_auth gmap_view.
-From iris.proofmode Require Import proofmode.
-From iris.base_logic Require Export lib.iprop.
-From iris.base_logic Require Import lib.own.
-From iris.program_logic Require Import language.
-From multi_actris.channel Require Import proto_model.
-Set Default Proof Using "Type".
-Export action.
-
-(** * Setup of Iris's cameras *)
-Class protoG Σ V :=
- protoG_authG ::
- inG Σ (gmap_viewR natO
- (optionUR (exclR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))))).
-
-Definition protoΣ V := #[
- GFunctor ((gmap_viewRF natO (optionRF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF))))))
-].
-Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
-Proof. solve_inG. Qed.
-
-(** * Types *)
-Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
-Declare Scope proto_scope.
-Delimit Scope proto_scope with proto.
-Bind Scope proto_scope with iProto.
-Local Open Scope proto.
-
-(** * Messages *)
-Section iMsg.
- Set Primitive Projections.
- Record iMsg Σ V := IMsg { iMsg_car : V → laterO (iProto Σ V) -n> iPropO Σ }.
-End iMsg.
-Arguments IMsg {_ _} _.
-Arguments iMsg_car {_ _} _.
-
-Declare Scope msg_scope.
-Delimit Scope msg_scope with msg.
-Bind Scope msg_scope with iMsg.
-Global Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
-
-Section imsg_ofe.
- Context {Σ : gFunctors} {V : Type}.
-
- Instance iMsg_equiv : Equiv (iMsg Σ V) := λ m1 m2,
- ∀ w p, iMsg_car m1 w p ≡ iMsg_car m2 w p.
- Instance iMsg_dist : Dist (iMsg Σ V) := λ n m1 m2,
- ∀ w p, iMsg_car m1 w p ≡{n}≡ iMsg_car m2 w p.
-
- Lemma iMsg_ofe_mixin : OfeMixin (iMsg Σ V).
- Proof. by apply (iso_ofe_mixin (iMsg_car : _ → V -d> _ -n> _)). Qed.
- Canonical Structure iMsgO := Ofe (iMsg Σ V) iMsg_ofe_mixin.
-
- Global Instance iMsg_cofe : Cofe iMsgO.
- Proof. by apply (iso_cofe (IMsg : (V -d> _ -n> _) → _) iMsg_car). Qed.
-End imsg_ofe.
-
-Program Definition iMsg_base_def {Σ V}
- (v : V) (P : iProp Σ) (p : iProto Σ V) : iMsg Σ V :=
- IMsg (λ v', λne p', ⌜ v = v' ⌠∗ Next p ≡ p' ∗ P)%I.
-Next Obligation. solve_proper. Qed.
-Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
-Definition iMsg_base := iMsg_base_aux.(unseal).
-Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
-Arguments iMsg_base {_ _} _%_V _%_I _%_proto.
-Global Instance: Params (@iMsg_base) 3 := {}.
-
-Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
- IMsg (λ v', λne p', ∃ x, iMsg_car (m x) v' p')%I.
-Next Obligation. solve_proper. Qed.
-Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
-Definition iMsg_exist := iMsg_exist_aux.(unseal).
-Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
-Arguments iMsg_exist {_ _ _} _%_msg.
-Global Instance: Params (@iMsg_exist) 3 := {}.
-
-Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
- tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
-Arguments iMsg_texist {_ _ !_} _%_msg /.
-
-Notation "'MSG' v {{ P } } ; p" := (iMsg_base v P p)
- (at level 200, v at level 20, right associativity,
- format "MSG v {{ P } } ; p") : msg_scope.
-Notation "'MSG' v ; p" := (iMsg_base v True p)
- (at level 200, v at level 20, right associativity,
- format "MSG v ; p") : msg_scope.
-Notation "∃ x .. y , m" :=
- (iMsg_exist (λ x, .. (iMsg_exist (λ y, m)) ..)%msg) : msg_scope.
-Notation "'∃..' x .. y , m" :=
- (iMsg_texist (λ x, .. (iMsg_texist (λ y, m)) .. )%msg)
- (at level 200, x binder, y binder, right associativity,
- format "∃.. x .. y , m") : msg_scope.
-
-Lemma iMsg_texist_exist {Σ V} {TT : tele} w lp (m : TT → iMsg Σ V) :
- iMsg_car (∃.. x, m x)%msg w lp ⊣⊢ (∃.. x, iMsg_car (m x) w lp).
-Proof.
- rewrite /iMsg_texist iMsg_exist_eq.
- induction TT as [|T TT IH]; simpl; [done|]. f_equiv=> x. apply IH.
-Qed.
-
-(** * Operators *)
-Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
-Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
-Definition iProto_end := iProto_end_aux.(unseal).
-Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
-Arguments iProto_end {_ _}.
-
-Definition iProto_message_def {Σ V} (a : action) (m : iMsg Σ V) : iProto Σ V :=
- proto_message a (iMsg_car m).
-Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
-Definition iProto_message := iProto_message_aux.(unseal).
-Definition iProto_message_eq :
- @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
-Arguments iProto_message {_ _} _ _%_msg.
-Global Instance: Params (@iProto_message) 3 := {}.
-
-Notation "'END'" := iProto_end : proto_scope.
-
-Notation "< a > m" := (iProto_message a m)
- (at level 200, a at level 10, m at level 200,
- format "< a > m") : proto_scope.
-Notation "< a @ x1 .. xn > m" := (iProto_message a (∃ x1, .. (∃ xn, m) ..))
- (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
- format "< a @ x1 .. xn > m") : proto_scope.
-Notation "< a @.. x1 .. xn > m" := (iProto_message a (∃.. x1, .. (∃.. xn, m) ..))
- (at level 200, a at level 10, x1 closed binder, xn closed binder, m at level 200,
- format "< a @.. x1 .. xn > m") : proto_scope.
-
-Class MsgTele {Σ V} {TT : tele} (m : iMsg Σ V)
- (tv : TT -t> V) (tP : TT -t> iProp Σ) (tp : TT -t> iProto Σ V) :=
- msg_tele : m ≡ (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg.
-Global Hint Mode MsgTele ! ! - ! - - - : typeclass_instances.
-
-(** * Operations *)
-Program Definition iMsg_map {Σ V}
- (rec : iProto Σ V → iProto Σ V) (m : iMsg Σ V) : iMsg Σ V :=
- IMsg (λ v, λne p1', ∃ p1, iMsg_car m v (Next p1) ∗ p1' ≡ Next (rec p1))%I.
-Next Obligation. solve_proper. Qed.
-
-Program Definition iProto_map_app_aux {Σ V}
- (f : action → action) (p2 : iProto Σ V)
- (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
- proto_elim p2 (λ a m,
- proto_message (f a) (iMsg_car (iMsg_map rec (IMsg m)))) p.
-Next Obligation.
- intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a m1 m2 Hm.
- apply proto_message_ne=> v p' /=. by repeat f_equiv.
-Qed.
-
-Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
- Contractive (iProto_map_app_aux f p2).
-Proof.
- intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
- apply proto_message_ne=> v p' /=. by repeat (f_contractive || f_equiv).
-Qed.
-
-Definition iProto_map_app {Σ V} (f : action → action)
- (p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
- fixpoint (iProto_map_app_aux f p2).
-
-Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
- iProto_map_app id p2 p1.
-Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
-Definition iProto_app := iProto_app_aux.(unseal).
-Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
-Arguments iProto_app {_ _} _%_proto _%_proto.
-Global Instance: Params (@iProto_app) 2 := {}.
-Infix "<++>" := iProto_app (at level 60) : proto_scope.
-Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
-
-Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
- iProto_map_app action_dual proto_end p.
-Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
-Definition iProto_dual := iProto_dual_aux.(unseal).
-Definition iProto_dual_eq :
- @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
-Arguments iProto_dual {_ _} _%_proto.
-Global Instance: Params (@iProto_dual) 2 := {}.
-Notation iMsg_dual := (iMsg_map iProto_dual).
-
-Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
- if d then iProto_dual p else p.
-Arguments iProto_dual_if {_ _} _ _%_proto.
-Global Instance: Params (@iProto_dual_if) 3 := {}.
-
-(** * Proofs *)
-Section proto.
- Context `{!protoG Σ V}.
- Implicit Types v : V.
- Implicit Types p pl pr : iProto Σ V.
- Implicit Types m : iMsg Σ V.
-
- (** ** Equality *)
- Lemma iProto_case p : p ≡ END ∨ ∃ t n m, p ≡ <(t,n)> m.
- Proof.
- rewrite iProto_message_eq iProto_end_eq.
- destruct (proto_case p) as [|([a n]&m&?)]; [by left|right].
- by exists a, n, (IMsg m).
- Qed.
- Lemma iProto_message_equivI `{!BiInternalEq SPROP} a1 a2 m1 m2 :
- (<a1> m1) ≡ (<a2> m2) ⊣⊢@{SPROP} ⌜ a1 = a2 ⌠∧
- (∀ v lp, iMsg_car m1 v lp ≡ iMsg_car m2 v lp).
- Proof. rewrite iProto_message_eq. apply proto_message_equivI. Qed.
-
- Lemma iProto_message_end_equivI `{!BiInternalEq SPROP} a m :
- (<a> m) ≡ END ⊢@{SPROP} False.
- Proof. rewrite iProto_message_eq iProto_end_eq. apply proto_message_end_equivI. Qed.
- Lemma iProto_end_message_equivI `{!BiInternalEq SPROP} a m :
- END ≡ (<a> m) ⊢@{SPROP} False.
- Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
-
- (** ** Non-expansiveness of operators *)
- Global Instance iMsg_car_proper :
- Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
- Proof.
- intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
- f_equiv; [ by f_equiv | done ].
- Qed.
- Global Instance iMsg_car_ne n :
- Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
- Proof.
- intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
- f_equiv; [ by f_equiv | done ].
- Qed.
-
- Global Instance iMsg_contractive v n :
- Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
- Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_contractive. Qed.
- Global Instance iMsg_ne v : NonExpansive2 (iMsg_base (Σ:=Σ) (V:=V) v).
- Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_proper. Qed.
- Global Instance iMsg_proper v :
- Proper ((≡) ==> (≡) ==> (≡)) (iMsg_base (Σ:=Σ) (V:=V) v).
- Proof. apply (ne_proper_2 _). Qed.
-
- Global Instance iMsg_exist_ne A n :
- Proper (pointwise_relation _ (dist n) ==> (dist n)) (@iMsg_exist Σ V A).
- Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
- Global Instance iMsg_exist_proper A :
- Proper (pointwise_relation _ (≡) ==> (≡)) (@iMsg_exist Σ V A).
- Proof. rewrite iMsg_exist_eq=> m1 m2 Hm v p /=. f_equiv=> x. apply Hm. Qed.
-
- Global Instance msg_tele_base (v:V) (P : iProp Σ) (p : iProto Σ V) :
- MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
- Proof. done. Qed.
- Global Instance msg_tele_exist {A} {TT : A → tele} (m : A → iMsg Σ V) tv tP tp :
- (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) →
- MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
- Proof. intros Hm. rewrite /MsgTele /=. f_equiv=> x. apply Hm. Qed.
-
- Global Instance iProto_message_ne a :
- NonExpansive (iProto_message (Σ:=Σ) (V:=V) a).
- Proof. rewrite iProto_message_eq. solve_proper. Qed.
- Global Instance iProto_message_proper a :
- Proper ((≡) ==> (≡)) (iProto_message (Σ:=Σ) (V:=V) a).
- Proof. apply (ne_proper _). Qed.
-
- Lemma iProto_message_equiv {TT1 TT2 : tele} a1 a2
- (m1 m2 : iMsg Σ V)
- (v1 : TT1 -t> V) (v2 : TT2 -t> V)
- (P1 : TT1 -t> iProp Σ) (P2 : TT2 -t> iProp Σ)
- (prot1 : TT1 -t> iProto Σ V) (prot2 : TT2 -t> iProto Σ V) :
- MsgTele m1 v1 P1 prot1 →
- MsgTele m2 v2 P2 prot2 →
- ⌜ a1 = a2 ⌠-∗
- (■∀.. (xs1 : TT1), tele_app P1 xs1 -∗
- ∃.. (xs2 : TT2), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
- ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
- tele_app P2 xs2) -∗
- (■∀.. (xs2 : TT2), tele_app P2 xs2 -∗
- ∃.. (xs1 : TT1), ⌜tele_app v1 xs1 = tele_app v2 xs2⌠∗
- ▷ (tele_app prot1 xs1 ≡ tele_app prot2 xs2) ∗
- tele_app P1 xs1) -∗
- (<a1> m1) ≡ (<a2> m2).
- Proof.
- iIntros (Hm1 Hm2 Heq) "#Heq1 #Heq2".
- unfold MsgTele in Hm1. rewrite Hm1. clear Hm1.
- unfold MsgTele in Hm2. rewrite Hm2. clear Hm2.
- rewrite iProto_message_eq proto_message_equivI.
- iSplit; [ done | ].
- iIntros (v p').
- do 2 rewrite iMsg_texist_exist.
- rewrite iMsg_base_eq /=.
- iApply prop_ext.
- iIntros "!>". iSplit.
- - iDestruct 1 as (xs1 Hveq1) "[Hrec1 HP1]".
- iDestruct ("Heq1" with "HP1") as (xs2 Hveq2) "[Hrec2 HP2]".
- iExists xs2. rewrite -Hveq1 Hveq2.
- iSplitR; [ done | ]. iSplitR "HP2"; [ | done ].
- iRewrite -"Hrec1". iApply later_equivI. iIntros "!>". by iRewrite "Hrec2".
- - iDestruct 1 as (xs2 Hveq2) "[Hrec2 HP2]".
- iDestruct ("Heq2" with "HP2") as (xs1 Hveq1) "[Hrec1 HP1]".
- iExists xs1. rewrite -Hveq2 Hveq1.
- iSplitR; [ done | ]. iSplitR "HP1"; [ | done ].
- iRewrite -"Hrec2". iApply later_equivI. iIntros "!>". by iRewrite "Hrec1".
- Qed.
-
- (** Helpers *)
- Lemma iMsg_map_base f v P p :
- NonExpansive f →
- iMsg_map f (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; f p)%msg.
- Proof.
- rewrite iMsg_base_eq. intros ? v' p'; simpl. iSplit.
- - iDestruct 1 as (p'') "[(->&Hp&$) Hp']". iSplit; [done|].
- iRewrite "Hp'". iIntros "!>". by iRewrite "Hp".
- - iIntros "(->&Hp'&$)". iExists p. iRewrite -"Hp'". auto.
- Qed.
- Lemma iMsg_map_exist {A} f (m : A → iMsg Σ V) :
- iMsg_map f (∃ x, m x) ≡ (∃ x, iMsg_map f (m x))%msg.
- Proof.
- rewrite iMsg_exist_eq. intros v' p'; simpl. iSplit.
- - iDestruct 1 as (p'') "[H Hp']". iDestruct "H" as (x) "H"; auto.
- - iDestruct 1 as (x p'') "[Hm Hp']". auto.
- Qed.
-
- (** ** Dual *)
- Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
- Proof. rewrite iProto_dual_eq. solve_proper. Qed.
- Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
- Proof. apply (ne_proper _). Qed.
- Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
- Proof. solve_proper. Qed.
- Global Instance iProto_dual_if_proper d :
- Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
- Proof. apply (ne_proper _). Qed.
-
- Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END.
- Proof.
- rewrite iProto_end_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- by rewrite proto_elim_end.
- Qed.
- Lemma iProto_dual_message a m :
- iProto_dual (<a> m) ≡ <action_dual a> iMsg_dual m.
- Proof.
- rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
- intros a' m1 m2 Hm; f_equiv; solve_proper.
- Qed.
- Lemma iMsg_dual_base v P p :
- iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
- Proof. apply iMsg_map_base, _. Qed.
- Lemma iMsg_dual_exist {A} (m : A → iMsg Σ V) :
- iMsg_dual (∃ x, m x) ≡ (∃ x, iMsg_dual (m x))%msg.
- Proof. apply iMsg_map_exist. Qed.
-
- Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
- Proof.
- intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&n&m&->)].
- { by rewrite !iProto_dual_end. }
- rewrite !iProto_dual_message involutive.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iApply prop_ext; iIntros "!>"; iSplit.
- - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
- iDestruct "H" as (pdd) "[H #Hpd]".
- iApply (internal_eq_rewrite); [|done]; iIntros "!>".
- iRewrite "Hpd". by iRewrite ("IH" $! pdd).
- - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists _.
- rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
- Qed.
-
- (** ** Append *)
- Global Instance iProto_app_end_l : LeftId (≡) END (@iProto_app Σ V).
- Proof.
- intros p. rewrite iProto_end_eq iProto_app_eq /iProto_app_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- by rewrite proto_elim_end.
- Qed.
- Lemma iProto_app_message a m p2 : (<a> m) <++> p2 ≡ <a> m <++> p2.
- Proof.
- rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
- etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
- rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
- intros a' m1 m2 Hm. f_equiv; solve_proper.
- Qed.
-
- Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
- Proof.
- assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
- { intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
- assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)).
- { intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
- intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
- revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
- destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite !left_id. }
- rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
- f_contractive. apply IH; eauto using dist_le with lia.
- Qed.
- Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
- Proof. apply (ne_proper_2 _). Qed.
-
- Lemma iMsg_app_base v P p1 p2 :
- ((MSG v {{ P }}; p1) <++> p2)%msg ≡ (MSG v {{ P }}; p1 <++> p2)%msg.
- Proof. apply: iMsg_map_base. Qed.
- Lemma iMsg_app_exist {A} (m : A → iMsg Σ V) p2 :
- ((∃ x, m x) <++> p2)%msg ≡ (∃ x, m x <++> p2)%msg.
- Proof. apply iMsg_map_exist. Qed.
-
- Global Instance iProto_app_end_r : RightId (≡) END (@iProto_app Σ V).
- Proof.
- intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|(a&i&m&->)].
- { by rewrite left_id. }
- rewrite iProto_app_message.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
- iApply (internal_eq_rewrite); [|done]; iIntros "!>".
- by iRewrite ("IH" $! p1').
- - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
- rewrite Hp'. iSplitL; [by auto|]. iIntros "!>". by iRewrite ("IH" $! p'').
- Qed.
- Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
- Proof.
- intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1). destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite !left_id. }
- rewrite !iProto_app_message.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p1') "[H #Hp']".
- iExists (p1' <++> p2). iSplitL; [by auto|].
- iRewrite "Hp'". iIntros "!>". iApply "IH".
- - iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
- iExists p1'. iFrame "H". iRewrite "Hp123".
- iIntros "!>". iRewrite "Hp12". by iRewrite ("IH" $! p1').
- Qed.
-
- Lemma iProto_dual_app p1 p2 :
- iProto_dual (p1 <++> p2) ≡ iProto_dual p1 <++> iProto_dual p2.
- Proof.
- apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
- iLöb as "IH" forall (p1 p2). destruct (iProto_case p1) as [->|(a&i&m&->)].
- { by rewrite iProto_dual_end !left_id. }
- rewrite iProto_dual_message !iProto_app_message iProto_dual_message /=.
- iApply iProto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
- iApply prop_ext; iIntros "!>". iSplit.
- - iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
- iExists (iProto_dual p1'). iSplitL; [by auto|].
- iRewrite "Hp12". iIntros "!>". iRewrite "Hp12d". iApply "IH".
- - iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
- iExists (p1d <++> p2). iSplitL; [by auto|].
- iRewrite "Hp12". iIntros "!>". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
- Qed.
-
-End proto.
-
-Global Instance iProto_inhabited {Σ V} : Inhabited (iProto Σ V) := populate END.
-
-Program Definition iProto_elim {Σ V A}
- (x : A) (f : action → iMsg Σ V -> A) (p : iProto Σ V) : A :=
- proto_elim x (λ a m, f a (IMsg (λ v, λne p, m v p)))%I p.
-Next Obligation. solve_proper. Qed.
-
-Lemma iProto_elim_message {Σ V} {A:ofe}
- (x : A) (f : action → iMsg Σ V -> A) a m
- `{Hf : ∀ a, Proper ((≡) ==> (≡)) (f a)} :
- iProto_elim x f (iProto_message a m) ≡ f a m.
- Proof.
- rewrite /iProto_elim iProto_message_eq /iProto_message_def /=.
- setoid_rewrite proto_elim_message.
- { apply Hf. done. }
- intros a' f1 f2 Hf'. apply Hf=> v p /=. apply Hf'.
-Qed.
-
-Lemma iProto_elim_message' {Σ V} {A:ofe}
- (x : A) (f : action → iMsg Σ V -> A) a m
- `{Hf : ∀ a, Proper ((≡) ==> (≡)) (f a)} :
- iProto_elim x f (iProto_message a m) ≡ f a m.
-Proof.
- rewrite /iProto_elim.
- rewrite iProto_message_eq /iProto_message_def. simpl.
- setoid_rewrite proto_elim_message.
- { f_equiv. done. }
- intros a'.
- intros f1 f2 Hf'. f_equiv. done.
-Qed.
-
-Definition nat_beq := Eval compute in Nat.eqb.
-
-Definition find_recv {Σ V} (i:nat) (j:nat) (ps : list (iProto Σ V)) :
- option $ iMsg Σ V :=
- iProto_elim None (λ a m,
- match a with
- | (Recv, i') => if nat_beq i i' then Some m else None
- | (Send, _) => None
- end) (ps !!! j).
-
-Fixpoint sync_pairs_aux {Σ V} (i : nat) (ps_full ps : list (iProto Σ V)) :
- list (nat * nat * iMsg Σ V * iMsg Σ V) :=
- match ps with
- | [] => []
- | p :: ps =>
- iProto_elim (sync_pairs_aux (S i) ps_full ps)
- (λ a mi, match a with
- | (Recv,_) => sync_pairs_aux (S i) ps_full ps
- | (Send,j) => match find_recv i j ps_full with
- | None => sync_pairs_aux (S i) ps_full ps
- | Some mj => (i,j,mi,mj) ::
- sync_pairs_aux (S i) ps_full ps
- end
- end) p
- end.
-
-Notation sync_pairs ps := (sync_pairs_aux 0 ps ps).
-
-Definition can_step {Σ V} (rec : list (iProto Σ V) → iProp Σ)
- (ps : list (iProto Σ V)) : iProp Σ :=
- [∧ list] '(i,j,m1,m2) ∈ sync_pairs ps,
- ∀ v p1, iMsg_car m1 v (Next p1) -∗
- ∃ p2, iMsg_car m2 v (Next p2) ∗
- â–· (rec (<[i:=p1]>(<[j:=p2]>ps))).
-
-From iris.heap_lang Require Import notation.
-
-Definition iProto_binary `{!heapGS Σ} : list (iProto Σ val) :=
- [(<(Send, 1) @ (x:Z)> MSG #x ; END)%proto;
- (<(Recv, 0) @ (x:Z)> MSG #x ; END)%proto].
-
-Lemma iProto_binary_consistent `{!heapGS Σ} :
- ⊢ can_step (λ _, True) (@iProto_binary _ Σ heapGS).
-Proof. rewrite /iProto_binary /can_step /iProto_elim. simpl.
- rewrite /find_recv. simpl.
- Fail rewrite iProto_elim_message.
- (* OBS: Break here *)
-
-
-Definition valid_target {Σ V} (ps : list (iProto Σ V)) (i j : nat) : iProp Σ :=
- ∀ a m, (ps !!! i ≡ <(a, j)> m) -∗ ⌜is_Some (ps !! j)âŒ.
-
-Definition iProto_consistent_pre {Σ V} (rec : list (iProto Σ V) → iProp Σ)
- (ps : list (iProto Σ V)) : iProp Σ :=
- (∀ i j, valid_target ps i j) ∗ (can_step rec ps).
-
-Global Instance iProto_consistent_pre_ne {Σ V}
- (rec : listO (iProto Σ V) -n> iPropO Σ) :
- NonExpansive (iProto_consistent_pre rec).
-Proof. rewrite /iProto_consistent_pre /can_step /valid_target. solve_proper. Qed.
-
-Program Definition iProto_consistent_pre' {Σ V}
- (rec : listO (iProto Σ V) -n> iPropO Σ) :
- listO (iProto Σ V) -n> iPropO Σ :=
- λne ps, iProto_consistent_pre (λ ps, rec ps) ps.
-
-Local Instance iProto_consistent_pre_contractive {Σ V} : Contractive (@iProto_consistent_pre' Σ V).
-Proof.
- rewrite /iProto_consistent_pre' /iProto_consistent_pre /can_step.
- solve_contractive.
-Qed.
-
-Definition iProto_consistent {Σ V} (ps : list (iProto Σ V)) : iProp Σ :=
- fixpoint iProto_consistent_pre' ps.
-
-Arguments iProto_consistent {_ _} _%_proto.
-Global Instance: Params (@iProto_consistent) 1 := {}.
-
-Global Instance iProto_consistent_ne {Σ V} : NonExpansive (@iProto_consistent Σ V).
-Proof. solve_proper. Qed.
-Global Instance iProto_consistent_proper {Σ V} : Proper ((≡) ==> (⊣⊢)) (@iProto_consistent Σ V).
-Proof. solve_proper. Qed.
-
-Lemma iProto_consistent_unfold {Σ V} (ps : list (iProto Σ V)) :
- iProto_consistent ps ≡ (iProto_consistent_pre iProto_consistent) ps.
-Proof.
- apply: (fixpoint_unfold iProto_consistent_pre').
-Qed.
-
-(** * Protocol entailment *)
-Definition iProto_le_pre {Σ V}
- (rec : iProto Σ V → iProto Σ V → iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
- (p1 ≡ END ∗ p2 ≡ END) ∨
- ∃ a1 a2 m1 m2,
- (p1 ≡ <a1> m1) ∗ (p2 ≡ <a2> m2) ∗
- match a1, a2 with
- | (Recv,i), (Recv,j) => ⌜i = j⌠∗ ∀ v p1',
- iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ rec p1' p2' ∗ iMsg_car m2 v (Next p2')
- | (Send,i), (Send,j) => ⌜i = j⌠∗ ∀ v p2',
- iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ rec p1' p2' ∗ iMsg_car m1 v (Next p1')
- | _, _ => False
- end.
-Global Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
- NonExpansive2 (iProto_le_pre rec).
-Proof. solve_proper. Qed.
-
-Program Definition iProto_le_pre' {Σ V}
- (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
- iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
- iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
-Solve Obligations with solve_proper.
-Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
-Proof.
- intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
- by repeat (f_contractive || f_equiv).
-Qed.
-Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
- fixpoint iProto_le_pre' p1 p2.
-Arguments iProto_le {_ _} _%_proto _%_proto.
-Global Instance: Params (@iProto_le) 2 := {}.
-Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
-
-Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
-Proof. solve_proper. Qed.
-Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
-Proof. solve_proper. Qed.
-
-Record proto_name := ProtName { proto_names : gmap nat gname }.
-Global Instance proto_name_inhabited : Inhabited proto_name :=
- populate (ProtName inhabitant).
-Global Instance proto_name_eq_dec : EqDecision proto_name.
-Proof. solve_decision. Qed.
-Global Instance proto_name_countable : Countable proto_name.
-Proof.
- refine (inj_countable (λ '(ProtName γs), (γs))
- (λ '(γs), Some (ProtName γs)) _); by intros [].
-Qed.
-
-Definition iProto_own_frag `{!protoG Σ V} (γ : gname)
- (i : nat) (p : iProto Σ V) : iProp Σ :=
- own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p))).
-
-Definition iProto_own_auth `{!protoG Σ V} (γ : gname)
- (ps : list (iProto Σ V)) : iProp Σ :=
- own γ (gmap_view_auth (DfracOwn 1) (((λ p, Excl' (Next p)) <$>
- (list_to_map (zip (seq 0 (length ps)) ps))) : gmap _ _)).
-
-Definition iProto_ctx `{protoG Σ V}
- (γ : gname) (ps_len : nat) : iProp Σ :=
- ∃ ps, ⌜length ps = ps_len⌠∗ iProto_own_auth γ ps ∗ ▷ iProto_consistent ps.
-
-(** * The connective for ownership of channel ends *)
-Definition iProto_own `{!protoG Σ V}
- (γ : gname) (i : nat) (p : iProto Σ V) : iProp Σ :=
- ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ i p'.
-Arguments iProto_own {_ _ _} _ _ _%_proto.
-Global Instance: Params (@iProto_own) 3 := {}.
-
-Global Instance iProto_own_frag_contractive `{protoG Σ V} γ i :
- Contractive (iProto_own_frag γ i).
-Proof. solve_contractive. Qed.
-
-Global Instance iProto_own_contractive `{protoG Σ V} γ i :
- Contractive (iProto_own γ i).
-Proof. solve_contractive. Qed.
-Global Instance iProto_own_ne `{protoG Σ V} γ s : NonExpansive (iProto_own γ s).
-Proof. solve_proper. Qed.
-Global Instance iProto_own_proper `{protoG Σ V} γ s :
- Proper ((≡) ==> (≡)) (iProto_own γ s).
-Proof. apply (ne_proper _). Qed.
-
-(** * Proofs *)
-Section proto.
- Context `{!protoG Σ V}.
- Implicit Types v : V.
- Implicit Types p pl pr : iProto Σ V.
- Implicit Types m : iMsg Σ V.
-
- Lemma own_prot_idx γ i j (p1 p2 : iProto Σ V) :
- own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
- own γ (gmap_view_frag j (DfracOwn 1) (Excl' (Next p2))) -∗
- ⌜i ≠jâŒ.
- Proof.
- iIntros "Hown Hown'" (->).
- iDestruct (own_valid_2 with "Hown Hown'") as "H".
- rewrite uPred.cmra_valid_elim.
- by iDestruct "H" as %[]%gmap_view_frag_op_validN.
- Qed.
-
- Lemma own_prot_excl γ i (p1 p2 : iProto Σ V) :
- own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p1))) -∗
- own γ (gmap_view_frag i (DfracOwn 1) (Excl' (Next p2))) -∗
- False.
- Proof. iIntros "Hi Hj". by iDestruct (own_prot_idx with "Hi Hj") as %?. Qed.
-
- (** ** Protocol entailment **)
- Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
- Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
-
- Lemma iProto_le_end : ⊢ END ⊑ (END : iProto Σ V).
- Proof. rewrite iProto_le_unfold. iLeft. auto 10. Qed.
-
- Lemma iProto_le_end_inv_r p : p ⊑ END -∗ (p ≡ END).
- Proof.
- rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
- iDestruct "H" as (a1 a2 m1 m2) "(_ & Heq & _)".
- by iDestruct (iProto_end_message_equivI with "Heq") as %[].
- Qed.
-
- Lemma iProto_le_end_inv_l p : END ⊑ p -∗ (p ≡ END).
- Proof.
- rewrite iProto_le_unfold. iIntros "[[_ Hp]|H] //".
- iDestruct "H" as (a1 a2 m1 m2) "(Heq & _ & _)".
- iDestruct (iProto_end_message_equivI with "Heq") as %[].
- Qed.
-
- Lemma iProto_le_send_inv i p1 m2 :
- p1 ⊑ (<(Send,i)> m2) -∗ ∃ m1,
- (p1 ≡ <(Send,i)> m1) ∗
- ∀ v p2', iMsg_car m2 v (Next p2') -∗
- ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
- Proof.
- rewrite iProto_le_unfold.
- iIntros "[[_ Heq]|H]".
- { by iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
- rewrite iProto_message_equivI. iDestruct "Hp2" as "[%Heq Hm2]".
- simplify_eq.
- destruct a1 as [[]]; [|done].
- iDestruct "H" as (->) "H". iExists m1. iFrame "Hp1".
- iIntros (v p2). iSpecialize ("Hm2" $! v (Next p2)). by iRewrite "Hm2".
- Qed.
-
- Lemma iProto_le_send_send_inv i m1 m2 v p2' :
- (<(Send,i)> m1) ⊑ (<(Send,i)> m2) -∗
- iMsg_car m2 v (Next p2') -∗ ∃ p1', ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1').
- Proof.
- iIntros "H Hm2". iDestruct (iProto_le_send_inv with "H") as (m1') "[Hm1 H]".
- iDestruct (iProto_message_equivI with "Hm1") as (Heq) "Hm1".
- iDestruct ("H" with "Hm2") as (p1') "[Hle Hm]".
- iRewrite -("Hm1" $! v (Next p1')) in "Hm". auto with iFrame.
- Qed.
-
- Lemma iProto_le_recv_inv_l i m1 p2 :
- (<(Recv,i)> m1) ⊑ p2 -∗ ∃ m2,
- (p2 ≡ <(Recv,i)> m2) ∗
- ∀ v p1', iMsg_car m1 v (Next p1') -∗
- ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
- Proof.
- rewrite iProto_le_unfold.
- iIntros "[[Heq _]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)".
- rewrite iProto_message_equivI. iDestruct "Hp1" as "[%Heq Hm1]".
- simplify_eq.
- destruct a2 as [[]]; [done|].
- iDestruct "H" as (->) "H". iExists m2. iFrame "Hp2".
- iIntros (v p1). iSpecialize ("Hm1" $! v (Next p1)). by iRewrite "Hm1".
- Qed.
-
- Lemma iProto_le_recv_inv_r i p1 m2 :
- (p1 ⊑ <(Recv,i)> m2) -∗ ∃ m1,
- (p1 ≡ <(Recv,i)> m1) ∗
- ∀ v p1', iMsg_car m1 v (Next p1') -∗
- ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
- Proof.
- rewrite iProto_le_unfold.
- iIntros "[[_ Heq]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
- rewrite iProto_message_equivI.
- iDestruct "Hp2" as "[%Heq Hm2]".
- simplify_eq.
- destruct a1 as [[]]; [done|].
- iDestruct "H" as (->) "H".
- iExists m1. iFrame.
- iIntros (v p2).
- iIntros "Hm1". iDestruct ("H" with "Hm1") as (p2') "[Hle H]".
- iSpecialize ("Hm2" $! v (Next p2')).
- iExists p2'. iFrame.
- iRewrite "Hm2". iApply "H".
- Qed.
-
- Lemma iProto_le_recv_recv_inv i m1 m2 v p1' :
- (<(Recv, i)> m1) ⊑ (<(Recv, i)> m2) -∗
- iMsg_car m1 v (Next p1') -∗ ∃ p2', ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2').
- Proof.
- iIntros "H Hm2". iDestruct (iProto_le_recv_inv_r with "H") as (m1') "[Hm1 H]".
- iApply "H". iDestruct (iProto_message_equivI with "Hm1") as (_) "Hm1".
- by iRewrite -("Hm1" $! v (Next p1')).
- Qed.
-
- Lemma iProto_le_msg_inv_l i a m1 p2 :
- (<(a,i)> m1) ⊑ p2 -∗ ∃ m2, p2 ≡ <(a,i)> m2.
- Proof.
- rewrite iProto_le_unfold /iProto_le_pre.
- iIntros "[[Heq _]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1' m2) "(Hp1 & Hp2 & H)".
- destruct a1 as [t1 ?], a2 as [t2 ?].
- destruct t1,t2; [|done|done|].
- - rewrite iProto_message_equivI.
- iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- - rewrite iProto_message_equivI.
- iDestruct "Hp1" as (Heq) "Hp1". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- Qed.
-
- Lemma iProto_le_msg_inv_r j a p1 m2 :
- (p1 ⊑ <(a,j)> m2) -∗ ∃ m1, p1 ≡ <(a,j)> m1.
- Proof.
- rewrite iProto_le_unfold /iProto_le_pre.
- iIntros "[[_ Heq]|H]".
- { iDestruct (iProto_message_end_equivI with "Heq") as %[]. }
- iDestruct "H" as (a1 a2 m1 m2') "(Hp1 & Hp2 & H)".
- destruct a1 as [t1 ?], a2 as [t2 ?].
- destruct t1,t2; [|done|done|].
- - rewrite iProto_message_equivI.
- iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- - rewrite iProto_message_equivI.
- iDestruct "Hp2" as (Heq) "Hp2". simplify_eq.
- iDestruct "H" as (->) "H". by iExists _.
- Qed.
-
- Lemma valid_target_le ps i p1 p2 :
- (∀ i' j', valid_target ps i' j') -∗
- ps !!! i ≡ p1 -∗
- p1 ⊑ p2 -∗
- (∀ i' j', valid_target (<[i := p2]>ps) i' j') ∗ p1 ⊑ p2.
- Proof. Admitted.
- (* iIntros "Hprot #HSome Hle". *)
- (* pose proof (iProto_case p1) as [Hend|Hmsg]. *)
- (* { rewrite Hend. iDestruct (iProto_le_end_inv_l with "Hle") as "#H". *)
- (* iFrame "Hle". *)
- (* iIntros (i' j' a m) "Hm". *)
- (* destruct (decide (i = j')) as [->|Hneqj]. *)
- (* { Search list_lookup_total insert. rewrite list_lookup_total_insert. ; [done|]. lia. done. } *)
- (* rewrite lookup_insert_ne; [|done]. *)
- (* destruct (decide (i = i')) as [->|Hneqi]. *)
- (* { rewrite lookup_total_insert. iRewrite "H" in "Hm". *)
- (* by iDestruct (iProto_end_message_equivI with "Hm") as "Hm". } *)
- (* rewrite lookup_total_insert_ne; [|done]. *)
- (* by iApply "Hprot". } *)
- (* destruct Hmsg as (t & n & m & Hmsg). *)
- (* setoid_rewrite Hmsg. *)
- (* iDestruct (iProto_le_msg_inv_l with "Hle") as (m2) "#Heq". iFrame "Hle". *)
- (* iIntros (i' j' a m') "Hm". *)
- (* destruct (decide (i = j')) as [->|Hneqj]. *)
- (* { rewrite lookup_insert. done. } *)
- (* rewrite lookup_insert_ne; [|done]. *)
- (* destruct (decide (i = i')) as [->|Hneqi]. *)
- (* { rewrite lookup_total_insert. iRewrite "Heq" in "Hm". *)
- (* iDestruct (iProto_message_equivI with "Hm") as (Heq) "Hm". *)
- (* simplify_eq. by iApply "Hprot". } *)
- (* rewrite lookup_total_insert_ne; [|done]. *)
- (* by iApply "Hprot". *)
- (* Qed. *)
-
- Lemma iProto_consistent_le ps i p1 p2 :
- iProto_consistent ps -∗
- ps !!! i ≡ p1 -∗
- p1 ⊑ p2 -∗
- iProto_consistent (<[i := p2]>ps).
- Proof.
- iIntros "Hprot #HSome Hle".
- iRevert "HSome".
- iLöb as "IH" forall (p1 p2 ps).
- iIntros "#HSome".
- rewrite !iProto_consistent_unfold.
- iDestruct "Hprot" as "(Htar & Hprot)".
- iDestruct (valid_target_le with "Htar HSome Hle") as "[Htar Hle]".
- iFrame.
- iIntros (i' j' m1 m2) "#Hm1 #Hm2".
- destruct (decide (i = i')) as [<-|Hneq].
- { rewrite list_lookup_total_insert; [|admit].
- pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
- destruct Hmsg as (a&?&m&Hmsg).
- setoid_rewrite Hmsg.
- destruct a; last first.
- { rewrite iProto_message_equivI.
- iDestruct "Hm1" as "[%Htag Hm1]". done. }
- rewrite iProto_message_equivI.
- iDestruct "Hm1" as "[%Htag Hm1]".
- inversion Htag. simplify_eq.
- iIntros (v p) "Hm1'".
- iSpecialize ("Hm1" $! v (Next p)).
- iDestruct (iProto_le_send_inv with "Hle") as "Hle".
- iRewrite -"Hm1" in "Hm1'".
- iDestruct "Hle" as (m') "[#Heq H]".
- iDestruct ("H" with "Hm1'") as (p') "[Hle H]".
- destruct (decide (i = j')) as [<-|Hneq].
- { rewrite list_lookup_total_insert. rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Heq _]". done. admit. }
- iDestruct ("Hprot" $!i j' with "[] [] H") as "Hprot".
- { iRewrite -"Heq". rewrite !list_lookup_total_alt. iRewrite "HSome". done. }
- { rewrite list_lookup_total_insert_ne; [|done]. done. }
- iDestruct "Hprot" as (p'') "[Hm Hprot]".
- iExists p''. iFrame.
- iNext.
- iDestruct ("IH" with "Hprot Hle [HSome]") as "HI".
- { rewrite list_lookup_total_insert; [done|]. admit. }
- iClear "IH Hm1 Hm2 Heq".
- rewrite list_insert_insert.
- rewrite (list_insert_commute _ j' i); [|done].
- rewrite list_insert_insert. done. }
- rewrite list_lookup_total_insert_ne; [|done].
- destruct (decide (i = j')) as [<-|Hneq'].
- { rewrite list_lookup_total_insert.
- pose proof (iProto_case p2) as [Hend|Hmsg].
- { setoid_rewrite Hend. rewrite iProto_end_message_equivI. done. }
- destruct Hmsg as (a&?&m&Hmsg).
- setoid_rewrite Hmsg.
- destruct a.
- { rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Htag Hm2]". done. }
- rewrite iProto_message_equivI.
- iDestruct "Hm2" as "[%Htag Hm2]".
- inversion Htag. simplify_eq.
- iIntros (v p) "Hm1'".
- iDestruct (iProto_le_recv_inv_r with "Hle") as "Hle".
- iDestruct "Hle" as (m') "[#Heq Hle]".
- iDestruct ("Hprot" $!i' with "[] [] Hm1'") as "Hprot".
- { done. }
- { rewrite !list_lookup_total_alt. iRewrite "HSome". done. }
- iDestruct ("Hprot") as (p') "[Hm1' Hprot]".
- iDestruct ("Hle" with "Hm1'") as (p2') "[Hle Hm']".
- iSpecialize ("Hm2" $! v (Next p2')).
- iExists p2'.
- iRewrite -"Hm2". iFrame.
- iDestruct ("IH" with "Hprot Hle []") as "HI".
- { iPureIntro. rewrite list_lookup_total_insert_ne; [|done].
- rewrite list_lookup_total_insert. done. admit. }
- rewrite list_insert_commute; [|done].
- rewrite !list_insert_insert. done. admit. }
- rewrite list_lookup_total_insert_ne; [|done].
- iIntros (v p) "Hm1'".
- iDestruct ("Hprot" $!i' j' with "[//] [//] Hm1'") as "Hprot".
- iDestruct "Hprot" as (p') "[Hm2' Hprot]".
- iExists p'. iFrame.
- iNext.
- rewrite (list_insert_commute _ j' i); [|done].
- rewrite (list_insert_commute _ i' i); [|done].
- iApply ("IH" with "Hprot Hle []").
- rewrite list_lookup_total_insert_ne; [|done].
- rewrite list_lookup_total_insert_ne; [|done].
- done.
- Admitted.
-
- Lemma iProto_le_send i m1 m2 :
- (∀ v p2', iMsg_car m2 v (Next p2') -∗ ∃ p1',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m1 v (Next p1')) -∗
- (<(Send,i)> m1) ⊑ (<(Send,i)> m2).
- Proof.
- iIntros "Hle". rewrite iProto_le_unfold.
- iRight. iExists (Send, i), (Send, i), m1, m2. by eauto.
- Qed.
-
- Lemma iProto_le_recv i m1 m2 :
- (∀ v p1', iMsg_car m1 v (Next p1') -∗ ∃ p2',
- ▷ (p1' ⊑ p2') ∗ iMsg_car m2 v (Next p2')) -∗
- (<(Recv,i)> m1) ⊑ (<(Recv,i)> m2).
- Proof.
- iIntros "Hle". rewrite iProto_le_unfold.
- iRight. iExists (Recv, i), (Recv, i), m1, m2. by eauto.
- Qed.
-
- Lemma iProto_le_base a v P p1 p2 :
- ▷ (p1 ⊑ p2) -∗
- (<a> MSG v {{ P }}; p1) ⊑ (<a> MSG v {{ P }}; p2).
- Proof.
- rewrite iMsg_base_eq. iIntros "H". destruct a as [[]].
- - iApply iProto_le_send. iIntros (v' p') "(->&Hp&$)".
- iExists p1. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
- - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$)".
- iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
- Qed.
-
- Lemma iProto_le_trans p1 p2 p3 : p1 ⊑ p2 -∗ p2 ⊑ p3 -∗ p1 ⊑ p3.
- Proof.
- iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
- destruct (iProto_case p3) as [->|([]&i&m3&->)].
- - iDestruct (iProto_le_end_inv_r with "H2") as "H2". by iRewrite "H2" in "H1".
- - iDestruct (iProto_le_send_inv with "H2") as (m2) "[Hp2 H2]".
- iRewrite "Hp2" in "H1"; clear p2.
- iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1.
- iApply iProto_le_send. iIntros (v p3') "Hm3".
- iDestruct ("H2" with "Hm3") as (p2') "[Hle Hm2]".
- iDestruct ("H1" with "Hm2") as (p1') "[Hle' Hm1]".
- iExists p1'. iIntros "{$Hm1} !>". by iApply ("IH" with "Hle'").
- - iDestruct (iProto_le_recv_inv_r with "H2") as (m2) "[Hp2 H3]".
- iRewrite "Hp2" in "H1".
- iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H2]".
- iRewrite "Hp1". iApply iProto_le_recv. iIntros (v p1') "Hm1".
- iDestruct ("H2" with "Hm1") as (p2') "[Hle Hm2]".
- iDestruct ("H3" with "Hm2") as (p3') "[Hle' Hm3]".
- iExists p3'. iIntros "{$Hm3} !>". by iApply ("IH" with "Hle").
- Qed.
-
- Lemma iProto_le_refl p : ⊢ p ⊑ p.
- Proof.
- iLöb as "IH" forall (p). destruct (iProto_case p) as [->|([]&i&m&->)].
- - iApply iProto_le_end.
- - iApply iProto_le_send. auto 10 with iFrame.
- - iApply iProto_le_recv. auto 10 with iFrame.
- Qed.
-
- Lemma iProto_le_dual p1 p2 : p2 ⊑ p1 -∗ iProto_dual p1 ⊑ iProto_dual p2.
- Proof.
- iIntros "H". iLöb as "IH" forall (p1 p2).
- destruct (iProto_case p1) as [->|([]&i&m1&->)].
- - iDestruct (iProto_le_end_inv_r with "H") as "H".
- iRewrite "H". iApply iProto_le_refl.
- - iDestruct (iProto_le_send_inv with "H") as (m2) "[Hp2 H]".
- iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message).
- iApply iProto_le_recv. iIntros (v p1d).
- iDestruct 1 as (p1') "[Hm1 #Hp1d]".
- iDestruct ("H" with "Hm1") as (p2') "[H Hm2]".
- iDestruct ("IH" with "H") as "H". iExists (iProto_dual p2').
- iSplitL "H"; [iIntros "!>"; by iRewrite "Hp1d"|]. simpl; auto.
- - iDestruct (iProto_le_recv_inv_r with "H") as (m2) "[Hp2 H]".
- iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message /=).
- iApply iProto_le_send. iIntros (v p2d).
- iDestruct 1 as (p2') "[Hm2 #Hp2d]".
- iDestruct ("H" with "Hm2") as (p1') "[H Hm1]".
- iDestruct ("IH" with "H") as "H". iExists (iProto_dual p1').
- iSplitL "H"; [iIntros "!>"; by iRewrite "Hp2d"|]. simpl; auto.
- Qed.
-
- Lemma iProto_le_dual_l p1 p2 : iProto_dual p2 ⊑ p1 ⊢ iProto_dual p1 ⊑ p2.
- Proof.
- iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
- by iApply iProto_le_dual.
- Qed.
- Lemma iProto_le_dual_r p1 p2 : p2 ⊑ iProto_dual p1 ⊢ p1 ⊑ iProto_dual p2.
- Proof.
- iIntros "H". iEval (rewrite -(involutive iProto_dual p1)).
- by iApply iProto_le_dual.
- Qed.
-
- Lemma iProto_le_app p1 p2 p3 p4 :
- p1 ⊑ p2 -∗ p3 ⊑ p4 -∗ p1 <++> p3 ⊑ p2 <++> p4.
- Proof.
- iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
- destruct (iProto_case p2) as [->|([]&i&m2&->)].
- - iDestruct (iProto_le_end_inv_r with "H1") as "H1".
- iRewrite "H1". by rewrite !left_id.
- - iDestruct (iProto_le_send_inv with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
- iApply iProto_le_send. iIntros (v p24).
- iDestruct 1 as (p2') "[Hm2 #Hp24]".
- iDestruct ("H1" with "Hm2") as (p1') "[H1 Hm1]".
- iExists (p1' <++> p3). iSplitR "Hm1"; [|by simpl; eauto].
- iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
- - iDestruct (iProto_le_recv_inv_r with "H1") as (m1) "[Hp1 H1]".
- iRewrite "Hp1"; clear p1. rewrite !iProto_app_message.
- iApply iProto_le_recv.
- iIntros (v p13). iDestruct 1 as (p1') "[Hm1 #Hp13]".
- iDestruct ("H1" with "Hm1") as (p2'') "[H1 Hm2]".
- iExists (p2'' <++> p4). iSplitR "Hm2"; [|by simpl; eauto].
- iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
- Qed.
-
- Lemma iProto_le_payload_elim_l i m v P p :
- (P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) ⊢
- (<(Recv,i)> MSG v {{ P }}; p) ⊑ <(Recv,i)> m.
- Proof.
- rewrite iMsg_base_eq. iIntros "H".
- iApply iProto_le_recv. iIntros (v' p') "(->&Hp&HP)".
- iApply (iProto_le_recv_recv_inv with "(H HP)"); simpl; auto.
- Qed.
- Lemma iProto_le_payload_elim_r i m v P p :
- (P -∗ (<(Send, i)> m) ⊑ (<(Send, i)> MSG v; p)) ⊢
- (<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p).
- Proof.
- rewrite iMsg_base_eq. iIntros "H".
- iApply iProto_le_send. iIntros (v' p') "(->&Hp&HP)".
- iApply (iProto_le_send_send_inv with "(H HP)"); simpl; auto.
- Qed.
- Lemma iProto_le_payload_intro_l i v P p :
- P -∗ (<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> MSG v; p).
- Proof.
- rewrite iMsg_base_eq.
- iIntros "HP". iApply iProto_le_send. iIntros (v' p') "(->&Hp&_) /=".
- iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
- Qed.
- Lemma iProto_le_payload_intro_r i v P p :
- P -∗ (<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> MSG v {{ P }}; p).
- Proof.
- rewrite iMsg_base_eq.
- iIntros "HP". iApply iProto_le_recv. iIntros (v' p') "(->&Hp&_) /=".
- iExists p'. iSplitR; [iApply iProto_le_refl|]. auto.
- Qed.
- Lemma iProto_le_exist_elim_l {A} i (m1 : A → iMsg Σ V) m2 :
- (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
- (<(Recv,i) @ x> m1 x) ⊑ (<(Recv,i)> m2).
- Proof.
- rewrite iMsg_exist_eq. iIntros "H".
- iApply iProto_le_recv. iIntros (v p1') "/=". iDestruct 1 as (x) "Hm".
- by iApply (iProto_le_recv_recv_inv with "H").
- Qed.
- Lemma iProto_le_exist_elim_r {A} i m1 (m2 : A → iMsg Σ V) :
- (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) ⊢
- (<(Send,i)> m1) ⊑ (<(Send,i) @ x> m2 x).
- Proof.
- rewrite iMsg_exist_eq. iIntros "H".
- iApply iProto_le_send. iIntros (v p2'). iDestruct 1 as (x) "Hm".
- by iApply (iProto_le_send_send_inv with "H").
- Qed.
- Lemma iProto_le_exist_intro_l {A} i (m : A → iMsg Σ V) a :
- ⊢ (<(Send,i) @ x> m x) ⊑ (<(Send,i)> m a).
- Proof.
- rewrite iMsg_exist_eq. iApply iProto_le_send. iIntros (v p') "Hm /=".
- iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
- Qed.
- Lemma iProto_le_exist_intro_r {A} i (m : A → iMsg Σ V) a :
- ⊢ (<(Recv,i)> m a) ⊑ (<(Recv,i) @ x> m x).
- Proof.
- rewrite iMsg_exist_eq. iApply iProto_le_recv. iIntros (v p') "Hm /=".
- iExists p'. iSplitR; last by auto. iApply iProto_le_refl.
- Qed.
-
- Lemma iProto_le_texist_elim_l {TT : tele} i (m1 : TT → iMsg Σ V) m2 :
- (∀ x, (<(Recv,i)> m1 x) ⊑ (<(Recv,i)> m2)) ⊢
- (<(Recv,i) @.. x> m1 x) ⊑ (<(Recv,i)> m2).
- Proof.
- iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
- iApply iProto_le_exist_elim_l; iIntros (x).
- iApply "IH". iIntros (xs). iApply "H".
- Qed.
- Lemma iProto_le_texist_elim_r {TT : tele} i m1 (m2 : TT → iMsg Σ V) :
- (∀ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x)) -∗
- (<(Send,i)> m1) ⊑ (<(Send,i) @.. x> m2 x).
- Proof.
- iIntros "H". iInduction TT as [|T TT] "IH"; simpl; [done|].
- iApply iProto_le_exist_elim_r; iIntros (x).
- iApply "IH". iIntros (xs). iApply "H".
- Qed.
-
- Lemma iProto_le_texist_intro_l {TT : tele} i (m : TT → iMsg Σ V) x :
- ⊢ (<(Send,i) @.. x> m x) ⊑ (<(Send,i)> m x).
- Proof.
- induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
- { iApply iProto_le_refl. }
- iApply iProto_le_trans; [by iApply iProto_le_exist_intro_l|]. iApply IH.
- Qed.
- Lemma iProto_le_texist_intro_r {TT : tele} i (m : TT → iMsg Σ V) x :
- ⊢ (<(Recv,i)> m x) ⊑ (<(Recv,i) @.. x> m x).
- Proof.
- induction x as [|T TT x xs IH] using tele_arg_ind; simpl.
- { iApply iProto_le_refl. }
- iApply iProto_le_trans; [|by iApply iProto_le_exist_intro_r]. iApply IH.
- Qed.
-
- Lemma iProto_consistent_target ps m a i j :
- iProto_consistent ps -∗
- ps !!! i ≡ (<(a, j)> m) -∗
- ⌜is_Some (ps !! j)âŒ.
- Proof.
- rewrite iProto_consistent_unfold. iDestruct 1 as "[Htar _]". iApply "Htar".
- Qed.
-
- Lemma iProto_consistent_step ps m1 m2 i j v p1 :
- iProto_consistent ps -∗
- ps !!! i ≡ (<(Send, j)> m1) -∗
- ps !!! j ≡ (<(Recv, i)> m2) -∗
- iMsg_car m1 v (Next p1) -∗
- ∃ p2, iMsg_car m2 v (Next p2) ∗
- â–· iProto_consistent (<[i := p1]>(<[j := p2]>ps)).
- Proof.
- iIntros "Hprot #Hi #Hj Hm1".
- rewrite iProto_consistent_unfold /iProto_consistent_pre.
- iDestruct "Hprot" as "[_ Hprot]".
- iDestruct ("Hprot" with "Hi Hj Hm1") as (p2) "[Hm2 Hprot]".
- iExists p2. iFrame.
- Qed.
-
- Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
- Proof. solve_proper. Qed.
-
- Lemma iProto_own_auth_agree γ ps i p :
- iProto_own_auth γ ps -∗ iProto_own_frag γ i p -∗ ▷ (ps !!! i ≡ p).
- Proof. Admitted.
- (* iIntros "Hâ— Hâ—¯". *)
- (* iDestruct (own_valid_2 with "H◠H◯") as "H✓". *)
- (* rewrite gmap_view_both_validI. *)
- (* iDestruct "H✓" as "[_ [H1 H2]]". *)
- (* rewrite list_lookup_total_alt lookup_fmap. *)
- (* destruct (ps !! i); last first. *)
- (* { rewrite !option_equivI. } *)
- (* simpl. rewrite !option_equivI excl_equivI. by iNext. *)
- (* Qed. *)
-
- Lemma iProto_own_auth_update γ ps i p p' :
- iProto_own_auth γ ps -∗ iProto_own_frag γ i p ==∗
- iProto_own_auth γ (<[i := p']>ps) ∗ iProto_own_frag γ i p'.
- Proof.
- iIntros "Hâ— Hâ—¯".
- iMod (own_update_2 with "Hâ— Hâ—¯") as "[H1 H2]"; [|iModIntro].
- { eapply (gmap_view_replace _ _ _ (Excl' (Next p'))). done. }
- iFrame. rewrite -fmap_insert. Admitted.
-
- Lemma iProto_own_auth_alloc ps :
- ⊢ |==> ∃ γ, iProto_own_auth γ ps ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
- Proof. Admitted.
- (* iMod (own_alloc (gmap_view_auth (DfracOwn 1) ∅)) as (γ) "Hauth". *)
- (* { apply gmap_view_auth_valid. } *)
- (* iExists γ. *)
- (* iInduction ps as [|i p ps Hin] "IH" using map_ind. *)
- (* { iModIntro. iFrame. by iApply big_sepM_empty. } *)
- (* iMod ("IH" with "Hauth") as "[Hauth Hfrags]". *)
- (* rewrite big_sepM_insert; [|done]. iFrame "Hfrags". *)
- (* iMod (own_update with "Hauth") as "[Hauth Hfrag]". *)
- (* { apply (gmap_view_alloc _ i (DfracOwn 1) (Excl' (Next p))); [|done|done]. *)
- (* by rewrite lookup_fmap Hin. } *)
- (* iModIntro. rewrite -fmap_insert. iFrame. *)
- (* iExists _. iFrame. iApply iProto_le_refl. *)
- (* Qed. *)
-
- Lemma iProto_own_le γ s p1 p2 :
- iProto_own γ s p1 -∗ ▷ (p1 ⊑ p2) -∗ iProto_own γ s p2.
- Proof.
- iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
- iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
- Qed.
-
- Lemma iProto_init ps :
- ▷ iProto_consistent ps -∗
- |==> ∃ γ, iProto_ctx γ (length ps) ∗ [∗ list] i ↦p ∈ ps, iProto_own γ i p.
- Proof.
- iIntros "Hconsistent".
- iMod iProto_own_auth_alloc as (γ) "[Hauth Hfrags]".
- iExists γ. iFrame. iExists _. by iFrame.
- Qed.
-
-
- Lemma iProto_step γ ps_dom i j m1 m2 p1 v :
- iProto_ctx γ ps_dom -∗
- iProto_own γ i (<(Send, j)> m1) -∗
- iProto_own γ j (<(Recv, i)> m2) -∗
- iMsg_car m1 v (Next p1) ==∗
- ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ps_dom ∗
- iProto_own γ i p1 ∗ iProto_own γ j p2.
- Proof.
- iIntros "Hctx Hi Hj Hm".
- iDestruct "Hi" as (pi) "[Hile Hi]".
- iDestruct "Hj" as (pj) "[Hjle Hj]".
- iDestruct "Hctx" as (ps Hdom) "[Hauth Hconsistent]".
- iDestruct (iProto_own_auth_agree with "Hauth Hi") as "#Hpi".
- iDestruct (iProto_own_auth_agree with "Hauth Hj") as "#Hpj".
- iDestruct (own_prot_idx with "Hi Hj") as %Hneq.
- iAssert (▷ (<[i:=<(Send, j)> m1]>ps !!! j ≡ pj))%I as "Hpj'".
- { by rewrite list_lookup_total_insert_ne. }
- iAssert (▷ (⌜is_Some (ps !! i)⌠∗ (pi ⊑ (<(Send, j)> m1))))%I with "[Hile]"
- as "[Hi' Hile]".
- { iNext. iDestruct (iProto_le_msg_inv_r with "Hile") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpi". rewrite list_lookup_total_alt.
- destruct (ps !! i); [done|].
- iDestruct (iProto_end_message_equivI with "Hpi") as "[]". }
- iAssert (▷ (⌜is_Some (ps !! j)⌠∗ (pj ⊑ (<(Recv, i)> m2))))%I with "[Hjle]"
- as "[Hj' Hjle]".
- { iNext. iDestruct (iProto_le_msg_inv_r with "Hjle") as (m) "#Heq".
- iFrame. iRewrite "Heq" in "Hpj". rewrite !list_lookup_total_alt.
- destruct (ps !! j); [done|].
- iDestruct (iProto_end_message_equivI with "Hpj") as "[]". }
- 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 j with "Hconsistent [] [] [Hm //]") as
- (p2) "[Hm2 Hconsistent]".
- { rewrite list_lookup_total_insert_ne; [|done].
- rewrite list_lookup_total_insert_ne; [|done].
- rewrite list_lookup_total_insert; [done|]. admit. }
- { rewrite list_lookup_total_insert_ne; [|done].
- rewrite list_lookup_total_insert; [done|]. admit. }
- iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
- iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
- iIntros "!>!>". iExists p2. iFrame "Hm2".
- iDestruct "Hi'" as %Hi. iDestruct "Hj'" as %Hj.
- iSplitL "Hconsistent Hauth".
- { iExists (<[i:=p1]> (<[j:=p2]> ps)).
- iSplit.
- { admit.
- (* rewrite !dom_insert_lookup_L; [done..|by rewrite lookup_insert_ne]. *)}
- iFrame. rewrite list_insert_insert.
- rewrite list_insert_commute; [|done]. rewrite list_insert_insert.
- by rewrite list_insert_commute; [|done]. }
- iSplitL "Hi"; iExists _; iFrame; iApply iProto_le_refl.
- Admitted.
-
- Lemma iProto_target γ ps_dom i a j m :
- iProto_ctx γ ps_dom -∗
- iProto_own γ i (<(a, j)> m) -∗
- â–· (⌜j < ps_domâŒ) ∗ iProto_ctx γ ps_dom ∗ iProto_own γ i (<(a, j)> m).
- Proof.
- iIntros "Hctx Hown".
- rewrite /iProto_ctx /iProto_own.
- iDestruct "Hctx" as (ps Hdom) "[Hauth Hps]".
- iDestruct "Hown" as (p') "[Hle Hown]".
- iDestruct (iProto_own_auth_agree with "Hauth Hown") as "#Hi".
- iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
- iAssert (▷ (⌜is_Some (ps !! j)⌠∗ iProto_consistent ps))%I
- with "[Hps]" as "[HSome Hps]".
- { iNext. iRewrite "Heq" in "Hi".
- iDestruct (iProto_consistent_target with "Hps Hi") as "#$". by iFrame. }
- iSplitL "HSome".
- { iNext. iDestruct "HSome" as %Heq.
- iPureIntro. simplify_eq. admit. }
- iSplitL "Hauth Hps"; iExists _; by iFrame.
- Admitted.
-
- (* (** The instances below make it possible to use the tactics [iIntros], *)
- (* [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [iProto_le] goals. *) *)
- Global Instance iProto_le_from_forall_l {A} i (m1 : A → iMsg Σ V) m2 name :
- AsIdentName m1 name →
- FromForall (iProto_message (Recv,i) (iMsg_exist m1) ⊑ (<(Recv,i)> m2))
- (λ x, (<(Recv, i)> m1 x) ⊑ (<(Recv, i)> m2))%I name | 10.
- Proof. intros _. apply iProto_le_exist_elim_l. Qed.
- Global Instance iProto_le_from_forall_r {A} i m1 (m2 : A → iMsg Σ V) name :
- AsIdentName m2 name →
- FromForall ((<(Send,i)> m1) ⊑ iProto_message (Send,i) (iMsg_exist m2))
- (λ x, (<(Send,i)> m1) ⊑ (<(Send,i)> m2 x))%I name | 11.
- Proof. intros _. apply iProto_le_exist_elim_r. Qed.
-
- Global Instance iProto_le_from_wand_l i m v P p :
- TCIf (TCEq P True%I) False TCTrue →
- FromWand ((<(Recv,i)> MSG v {{ P }}; p) ⊑ (<(Recv,i)> m)) P ((<(Recv,i)> MSG v; p) ⊑ (<(Recv,i)> m)) | 10.
- Proof. intros _. apply iProto_le_payload_elim_l. Qed.
- Global Instance iProto_le_from_wand_r i m v P p :
- FromWand ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v {{ P }}; p)) P ((<(Send,i)> m) ⊑ (<(Send,i)> MSG v; p)) | 11.
- Proof. apply iProto_le_payload_elim_r. Qed.
-
- Global Instance iProto_le_from_exist_l {A} i (m : A → iMsg Σ V) p :
- FromExist ((<(Send,i) @ x> m x) ⊑ p) (λ a, (<(Send,i)> m a) ⊑ p)%I | 10.
- Proof.
- rewrite /FromExist. iDestruct 1 as (x) "H".
- iApply (iProto_le_trans with "[] H"). iApply iProto_le_exist_intro_l.
- Qed.
- Global Instance iProto_le_from_exist_r {A} i (m : A → iMsg Σ V) p :
- FromExist (p ⊑ <(Recv,i) @ x> m x) (λ a, p ⊑ (<(Recv,i)> m a))%I | 11.
- Proof.
- rewrite /FromExist. iDestruct 1 as (x) "H".
- iApply (iProto_le_trans with "H"). iApply iProto_le_exist_intro_r.
- Qed.
-
- Global Instance iProto_le_from_sep_l i m v P p :
- FromSep ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m)) P ((<(Send,i)> MSG v; p) ⊑ (<(Send,i)> m)) | 10.
- Proof.
- rewrite /FromSep. iIntros "[HP H]".
- iApply (iProto_le_trans with "[HP] H"). by iApply iProto_le_payload_intro_l.
- Qed.
- Global Instance iProto_le_from_sep_r i m v P p :
- FromSep ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p)) P ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v; p)) | 11.
- Proof.
- rewrite /FromSep. iIntros "[HP H]".
- iApply (iProto_le_trans with "H"). by iApply iProto_le_payload_intro_r.
- Qed.
-
- Global Instance iProto_le_frame_l i q m v R P Q p :
- Frame q R P Q →
- Frame q R ((<(Send,i)> MSG v {{ P }}; p) ⊑ (<(Send,i)> m))
- ((<(Send,i)> MSG v {{ Q }}; p) ⊑ (<(Send,i)> m)) | 10.
- Proof.
- rewrite /Frame /=. iIntros (HP) "[HR H]".
- iApply (iProto_le_trans with "[HR] H"). iApply iProto_le_payload_elim_r.
- iIntros "HQ". iApply iProto_le_payload_intro_l. iApply HP; iFrame.
- Qed.
- Global Instance iProto_le_frame_r i q m v R P Q p :
- Frame q R P Q →
- Frame q R ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ P }}; p))
- ((<(Recv,i)> m) ⊑ (<(Recv,i)> MSG v {{ Q }}; p)) | 11.
- Proof.
- rewrite /Frame /=. iIntros (HP) "[HR H]".
- iApply (iProto_le_trans with "H"). iApply iProto_le_payload_elim_l.
- iIntros "HQ". iApply iProto_le_payload_intro_r. iApply HP; iFrame.
- Qed.
-
- Global Instance iProto_le_from_modal a v p1 p2 :
- FromModal True (modality_instances.modality_laterN 1) (p1 ⊑ p2)
- ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
- Proof. intros _. iApply iProto_le_base. Qed.
-
-End proto.
-
-Typeclasses Opaque iProto_ctx iProto_own.
-
-Global Hint Extern 0 (environments.envs_entails _ (?x ⊑ ?y)) =>
- first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
diff --git a/multi_actris/examples/leader_election.v b/multi_actris/examples/leader_election.v
deleted file mode 100644
index 0fa6ef5..0000000
--- a/multi_actris/examples/leader_election.v
+++ /dev/null
@@ -1,206 +0,0 @@
-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 *)
-
-Definition process : val :=
- rec: "go" "c" "idl" "id" "idr" "isp" :=
- if: recv "c" "idr"
- then let: "id'" := recv "c" "idr" in
- if: "id" < "id'" (** Case 1 *)
- then send "c" "idl" #true;; send "c" "idl" "id'";;
- "go" "c" "idl" "id" "idr" #true
- else if: "id" = "id'" (** Case 4 *)
- then send "c" "idl" #false;; send "c" "idl" "id";;
- "go" "c" "idl" "id" "idr" #false
- else if: "isp" (** Case 3 *)
- then "go" "c" "idl" "id" "idr" "isp" (** Case 2 *)
- else send "c" "idl" #true;; send "c" "idl" "id";;
- "go" "c" "idl" "id" "idr" #true
- else let: "id'" := recv "c" "idr" in
- if: "id" = "id'" then "id'"
- else send "c" "idl" #false;; send "c" "idl" "id'";; "id'".
-
-Definition init : val :=
- λ: "c" "idl" "id" "idr",
- (* Notice missing leader *)
- send "c" "idl" #true;; send "c" "idl" "id";;
- process "c" "idl" "id" "idr" #true.
-
-Definition program : val :=
- λ: <>,
- let: "cs" := new_chan #4 in
- let: "c0" := get_chan "cs" #0 in
- let: "c1" := get_chan "cs" #1 in
- let: "c2" := get_chan "cs" #2 in
- let: "c3" := get_chan "cs" #3 in
- Fork (let: "id_max" := init "c1" #3 #1 #2 in send "c1" #0 "id_max");;
- Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
- send "c2" #0 "id_max");;
- Fork (let: "id_max" := init "c3" #2 #3 #1 in send "c3" #0 "id_max");;
- let: "res1" := recv "c0" #1 in
- let: "res2" := recv "c0" #2 in
- let: "res3" := recv "c0" #3 in
- assert: ("res1" = "res2");;
- assert: ("res2" = "res3").
-
-Notation iProto_choice a p1 p2 :=
- (<a @ (b : bool)> MSG #b; if b then p1 else p2)%proto.
-
-Section ring_leader_election_example.
- Context `{!heapGS Σ, chanG Σ, spawnG Σ, mono_natG Σ}.
-
- Definition my_recv_prot (il i ir : nat) (p : nat → iProto Σ)
- (rec : bool -d> iProto Σ) : bool -d> iProto Σ :=
- λ (isp:bool),
- iProto_choice (Recv,ir)
- (<(Recv,ir) @ (i':nat)> MSG #i' ;
- if bool_decide (i < i')
- then <(Send,il)> MSG #true ; <(Send,il)> MSG #i' ; rec true
- else if bool_decide (i = i')
- then <(Send,il)> MSG #false ; <(Send, il)> MSG #i ; rec false
- else if isp then rec isp
- else <(Send,il)> MSG #true ; <(Send,il)> MSG #i ; rec true)%proto
- (<(Recv,ir) @ (i':nat)> MSG #i' ;
- if (bool_decide (i = i')) then p i
- else <(Send,il)> MSG #false; <(Send,il)> MSG #i'; p i')%proto.
-
- Instance rle_prot_aux_contractive il i ir p : Contractive (my_recv_prot il i ir p).
- Proof. rewrite /my_recv_prot. solve_proto_contractive. Qed.
- Definition rle_prot il i ir p := fixpoint (my_recv_prot il i ir p).
- Instance rle_prot_unfold il i ir isp p :
- ProtoUnfold (rle_prot il i ir p isp) (my_recv_prot il i ir p (rle_prot il i ir p) isp).
- Proof. apply proto_unfold_eq, (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
- Lemma rle_prot_unfold' il i ir isp p :
- (rle_prot il i ir p isp) ≡
- (my_recv_prot il i ir p (rle_prot il i ir p) isp).
- Proof. apply (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
-
- Definition rle_preprot (il i ir : nat) p : iProto Σ :=
- (<(Send, il)> MSG #true; <(Send, il)> MSG #i ;
- rle_prot il i ir p true)%proto.
-
- Lemma process_spec il i ir p c (isp:bool) :
- {{{ c ↣ (rle_prot il i ir p isp) }}}
- process c #il #i #ir #isp
- {{{ i', RET #i'; c ↣ p i' }}}.
- Proof.
- iIntros (Φ) "Hc HΦ".
- iLöb as "IH" forall (Φ isp).
- wp_lam. wp_recv (b) as "_".
- destruct b.
- - wp_pures. wp_recv (i') as "_".
- wp_pures.
- case_bool_decide as Hlt.
- { case_bool_decide; [|lia].
- wp_pures. wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
- case_bool_decide as Hlt2.
- { case_bool_decide; [lia|].
- wp_pures. case_bool_decide; [|simplify_eq;lia].
- wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
- case_bool_decide; [lia|].
- wp_pures.
- case_bool_decide; [simplify_eq;lia|].
- wp_pures.
- destruct isp.
- { wp_pures. iApply ("IH" with "Hc HΦ"). }
- wp_pures.
- wp_send with "[//]".
- wp_send with "[//]".
- wp_pures. iApply ("IH" with "Hc HΦ").
- - wp_pures.
- wp_recv (id') as "_". wp_pures.
- case_bool_decide as Hlt.
- { case_bool_decide; [|simplify_eq;lia].
- wp_pures. subst. by iApply "HΦ". }
- case_bool_decide; [simplify_eq;lia|].
- wp_send with "[//]". wp_send with "[//]". wp_pures. by iApply "HΦ".
- Qed.
-
- Lemma init_spec c il i ir p :
- {{{ c ↣ rle_preprot il i ir p }}}
- init c #il #i #ir
- {{{ res, RET #res; c ↣ p res }}}.
- Proof.
- iIntros (Φ) "Hc HΦ". wp_lam. wp_send with "[//]". wp_send with "[//]".
- wp_pures. by iApply (process_spec with "Hc HΦ").
- Qed.
-
- Definition prot_tail (i_max : nat) : iProto Σ :=
- (<(Send,0)> MSG #i_max; END)%proto.
-
- Definition pre_prot_pool id_max : list (iProto Σ) :=
- [(<(Recv,1) @ (id_max : nat)> MSG #id_max ;
- <(Recv,2)> MSG #id_max ;
- <(Recv,3)> MSG #id_max ;
- END)%proto;
- prot_tail id_max;
- prot_tail id_max;
- prot_tail id_max].
-
- Lemma pre_prot_pool_consistent id_max :
- ⊢ iProto_consistent (pre_prot_pool id_max).
- Proof. rewrite /pre_prot_pool. iProto_consistent_take_steps. Qed.
-
- Definition prot_pool : list (iProto Σ) :=
- [(<(Recv,1) @ (id_max : nat)> MSG #id_max ;
- <(Recv,2)> MSG #id_max ;
- <(Recv,3)> MSG #id_max ;
- END)%proto;
- rle_preprot 3 1 2 prot_tail;
- rle_prot 1 2 3 prot_tail false;
- rle_preprot 2 3 1 prot_tail].
-
- Lemma prot_pool_consistent : ⊢ iProto_consistent prot_pool.
- Proof.
- rewrite /prot_pool /rle_preprot.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- case_bool_decide; try lia.
- case_bool_decide; try lia.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- case_bool_decide; try lia.
- case_bool_decide; try lia.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- Qed.
-
- Lemma program_spec :
- {{{ True }}} program #() {{{ RET #(); True }}}.
- Proof.
- iIntros (Φ) "_ HΦ". wp_lam.
- wp_new_chan prot_pool with prot_pool_consistent
- as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
- wp_smart_apply (wp_fork with "[Hc1]").
- { iIntros "!>". wp_smart_apply (init_spec with "Hc1").
- iIntros (i') "Hc1". by wp_send with "[//]". }
- wp_smart_apply (wp_fork with "[Hc2]").
- { iIntros "!>". wp_smart_apply (process_spec with "Hc2").
- iIntros (i') "Hc2". by wp_send with "[//]". }
- wp_smart_apply (wp_fork with "[Hc3]").
- { iIntros "!>". wp_smart_apply (init_spec with "Hc3").
- iIntros (i') "Hc3". by wp_send with "[//]". }
- wp_recv (id_max) as "_". wp_recv as "_". wp_recv as "_".
- wp_smart_apply wp_assert. wp_pures. iModIntro. iSplitR; [iPureIntro|].
- { do 2 f_equiv. by apply bool_decide_eq_true_2. }
- iIntros "!>".
- wp_smart_apply wp_assert. wp_pures. iModIntro. iSplitR; [iPureIntro|].
- { do 2 f_equiv. by apply bool_decide_eq_true_2. }
- iIntros "!>". by iApply "HΦ".
- 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.
diff --git a/multi_actris/examples/leader_election_del.v b/multi_actris/examples/leader_election_del.v
deleted file mode 100644
index 1ff5abd..0000000
--- a/multi_actris/examples/leader_election_del.v
+++ /dev/null
@@ -1,276 +0,0 @@
-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 *)
-
-Definition process : val :=
- rec: "go" "c" "idl" "id" "idr" "isp" :=
- if: recv "c" "idr"
- then let: "id'" := recv "c" "idr" in
- if: "id" < "id'" (** Case 1 *)
- then send "c" "idl" #true;; send "c" "idl" "id'";;
- "go" "c" "idl" "id" "idr" #true
- else if: "id" = "id'" (** Case 4 *)
- then send "c" "idl" #false;; send "c" "idl" "id";;
- "go" "c" "idl" "id" "idr" #false
- else if: "isp" (** Case 3 *)
- then "go" "c" "idl" "id" "idr" "isp" (** Case 2 *)
- else send "c" "idl" #true;; send "c" "idl" "id";;
- "go" "c" "idl" "id" "idr" #true
- else let: "id'" := recv "c" "idr" in
- if: "id" = "id'" then "id'"
- else send "c" "idl" #false;; send "c" "idl" "id'";; "id'".
-
-Definition init : val :=
- λ: "c" "idl" "id" "idr",
- (* Notice missing leader *)
- send "c" "idl" #true;; send "c" "idl" "id";;
- process "c" "idl" "id" "idr" #true.
-
-Definition forward : val :=
- λ: "c" "idl" "id" "idr" "id_max",
- if: "id" = "id_max" then
- let: "cs'" := new_chan #2 in
- let: "c0" := get_chan "cs'" #0 in
- let: "c1" := get_chan "cs'" #1 in
- send "c1" #0 "id_max";;
- send "c" "idl" "c1";;
- Fork ((rec: "f" <> :=
- let: "id'" := recv "c0" #1 in
- assert: ("id'" = "id_max");; "f" #()) #());;
- recv "c" "idr";; #()
- else
- let: "c1" := recv "c" "idr" in
- send "c1" #0 "id_max";;
- send "c" "idl" "c1".
-
-Definition program : val :=
- λ: <>,
- let: "cs" := new_chan #4 in
- let: "c0" := get_chan "cs" #0 in
- let: "c1" := get_chan "cs" #1 in
- let: "c2" := get_chan "cs" #2 in
- let: "c3" := get_chan "cs" #3 in
- Fork (let: "id_max" := process "c1" #0 #1 #2 #false in
- forward "c1" #0 #1 #2 "id_max");;
- Fork (let: "id_max" := process "c2" #1 #2 #3 #false in
- forward "c2" #1 #2 #3 "id_max");;
- Fork (let: "id_max" := process "c3" #2 #3 #0 #false in
- forward "c3" #2 #3 #0 "id_max");;
- let: "id_max" := init "c0" #3 #0 #1 in
- forward "c0" #3 #0 #1 "id_max".
-
-Notation iProto_choice a p1 p2 :=
- (<a @ (b : bool)> MSG #b; if b then p1 else p2)%proto.
-
-Section ring_leader_election_example.
- Context `{!heapGS Σ, chanG Σ, spawnG Σ, mono_natG Σ}.
-
- Definition my_recv_prot (il i ir : nat) (p : nat → iProto Σ)
- (rec : bool -d> iProto Σ) : bool -d> iProto Σ :=
- λ (isp:bool),
- iProto_choice (Recv,ir)
- (<(Recv,ir) @ (i':nat)> MSG #i' ;
- if bool_decide (i < i')
- then <(Send,il)> MSG #true ; <(Send,il)> MSG #i' ; rec true
- else if bool_decide (i = i')
- then <(Send,il)> MSG #false ; <(Send, il)> MSG #i ; rec false
- else if isp then rec isp
- else <(Send,il)> MSG #true ; <(Send,il)> MSG #i ; rec true)%proto
- (<(Recv,ir) @ (i':nat)> MSG #i' ;
- if (bool_decide (i = i')) then p i
- else <(Send,il)> MSG #false; <(Send,il)> MSG #i'; p i')%proto.
-
- Instance rle_prot_aux_contractive il i ir p : Contractive (my_recv_prot il i ir p).
- Proof. rewrite /my_recv_prot. solve_proto_contractive. Qed.
- Definition rle_prot il i ir p := fixpoint (my_recv_prot il i ir p).
- Instance rle_prot_unfold il i ir isp p :
- ProtoUnfold (rle_prot il i ir p isp) (my_recv_prot il i ir p (rle_prot il i ir p) isp).
- Proof. apply proto_unfold_eq, (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
- Lemma rle_prot_unfold' il i ir isp p :
- (rle_prot il i ir p isp) ≡
- (my_recv_prot il i ir p (rle_prot il i ir p) isp).
- Proof. apply (fixpoint_unfold (my_recv_prot il i ir p)). Qed.
-
- Definition rle_preprot (il i ir : nat) p : iProto Σ :=
- (<(Send, il)> MSG #true; <(Send, il)> MSG #i ;
- rle_prot il i ir p true)%proto.
-
- Lemma process_spec il i ir p c (isp:bool) :
- {{{ c ↣ (rle_prot il i ir p isp) }}}
- process c #il #i #ir #isp
- {{{ i', RET #i'; c ↣ p i' }}}.
- Proof.
- iIntros (Φ) "Hc HΦ".
- iLöb as "IH" forall (Φ isp).
- wp_lam. wp_recv (b) as "_".
- destruct b.
- - wp_pures. wp_recv (i') as "_".
- wp_pures.
- case_bool_decide as Hlt.
- { case_bool_decide; [|lia].
- wp_pures. wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
- case_bool_decide as Hlt2.
- { case_bool_decide; [lia|].
- wp_pures. case_bool_decide; [|simplify_eq;lia].
- wp_send with "[//]".
- wp_send with "[//]". wp_pures.
- iApply ("IH" with "Hc HΦ"). }
- case_bool_decide; [lia|].
- wp_pures.
- case_bool_decide; [simplify_eq;lia|].
- wp_pures.
- destruct isp.
- { wp_pures. iApply ("IH" with "Hc HΦ"). }
- wp_pures.
- wp_send with "[//]".
- wp_send with "[//]".
- wp_pures. iApply ("IH" with "Hc HΦ").
- - wp_pures.
- wp_recv (id') as "_". wp_pures.
- case_bool_decide as Hlt.
- { case_bool_decide; [|simplify_eq;lia].
- wp_pures. subst. by iApply "HΦ". }
- case_bool_decide; [simplify_eq;lia|].
- wp_send with "[//]". wp_send with "[//]". wp_pures. by iApply "HΦ".
- Qed.
-
- Lemma init_spec c il i ir p :
- {{{ c ↣ rle_preprot il i ir p }}}
- init c #il #i #ir
- {{{ res, RET #res; c ↣ p res }}}.
- Proof.
- iIntros (Φ) "Hc HΦ". wp_lam. wp_send with "[//]". wp_send with "[//]".
- wp_pures. by iApply (process_spec with "Hc HΦ").
- Qed.
-
- Definition forward_prot (p : iProto Σ) (il i ir i_max : nat) : iProto Σ :=
- if bool_decide (i = i_max) then
- (<(Send,il) @ (c:val)> MSG c {{ c ↣ p }} ; <(Recv,ir)> MSG c {{ c ↣ p }}; END)%proto
- else
- (<(Recv,ir) @ (c:val)> MSG c {{ c ↣ p }} ; <(Send,il)> MSG c {{ c ↣ p }}; END)%proto.
-
- Definition relay_send_aux (id : nat) (rec : iProto Σ) : iProto Σ :=
- (<(Send,0)> MSG #id ; rec)%proto.
- Instance relay_send_aux_contractive i : Contractive (relay_send_aux i).
- Proof. solve_proto_contractive. Qed.
- Definition relay_send_prot i := fixpoint (relay_send_aux i).
- Instance relay_send_prot_unfold i :
- ProtoUnfold (relay_send_prot i) (relay_send_aux i (relay_send_prot i)).
- Proof. apply proto_unfold_eq, (fixpoint_unfold (relay_send_aux i)). Qed.
- Lemma relay_send_prot_unfold' i :
- (relay_send_prot i) ≡
- (relay_send_aux i (relay_send_prot i)).
- Proof. apply (fixpoint_unfold (relay_send_aux i)). Qed.
-
- Definition relay_recv_aux (id : nat) (rec : iProto Σ) : iProto Σ :=
- (<(Recv,1)> MSG #id ; rec)%proto.
- Instance relay_recv_aux_contractive i : Contractive (relay_recv_aux i).
- Proof. solve_proto_contractive. Qed.
- Definition relay_recv_prot i := fixpoint (relay_recv_aux i).
- Instance relay_recv_prot_unfold i :
- ProtoUnfold (relay_recv_prot i) (relay_recv_aux i (relay_recv_prot i)).
- Proof. apply proto_unfold_eq, (fixpoint_unfold (relay_recv_aux i)). Qed.
- Lemma relay_recv_prot_unfold' i :
- (relay_recv_prot i) ≡
- (relay_recv_aux i (relay_recv_prot i)).
- Proof. apply (fixpoint_unfold (relay_recv_aux i)). Qed.
-
- Definition prot_pool : list (iProto Σ) :=
- [rle_preprot 3 0 1 (λ id_max, forward_prot (relay_send_prot id_max) 3 0 1 id_max);
- rle_prot 0 1 2 (λ id_max, forward_prot (relay_send_prot id_max) 0 1 2 id_max) false;
- rle_prot 1 2 3 (λ id_max, forward_prot (relay_send_prot id_max) 1 2 3 id_max) false;
- rle_prot 2 3 0 (λ id_max, forward_prot (relay_send_prot id_max) 2 3 0 id_max) false].
-
- Lemma prot_pool_consistent : ⊢ iProto_consistent prot_pool.
- Proof.
- rewrite /prot_pool /rle_preprot.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- case_bool_decide; try lia.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- case_bool_decide; try lia.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- case_bool_decide; try lia.
- rewrite !rle_prot_unfold'.
- iProto_consistent_take_steps.
- Qed.
-
- Definition prot_pool' (i:nat) : list (iProto Σ) :=
- [relay_recv_prot i;
- relay_send_prot i].
-
- Lemma prot_pool_consistent' i : ⊢ iProto_consistent (prot_pool' i).
- Proof.
- rewrite /prot_pool'.
- iLöb as "IH".
- iEval (rewrite relay_recv_prot_unfold').
- iEval (rewrite relay_send_prot_unfold').
- iProto_consistent_take_steps.
- done.
- Qed.
-
- Lemma forward_spec c il i ir i_max :
- {{{ c ↣ forward_prot (relay_send_prot i_max) il i ir i_max }}}
- forward c #il #i #ir #i_max
- {{{ RET #(); True }}}.
- Proof.
- iIntros (Φ) "Hc HΦ". wp_lam.
- rewrite /forward_prot.
- wp_pures. case_bool_decide.
- - simplify_eq. wp_pures.
- case_bool_decide; [|simplify_eq;lia].
- wp_new_chan (prot_pool' i_max) with (prot_pool_consistent' i_max)
- as (c0 c1) "Hc0" "Hc1".
- wp_send with "[//]".
- wp_send with "[Hc1//]".
- wp_smart_apply (wp_fork with "[Hc0]").
- { iIntros "!>".
- wp_pures.
- iLöb as "IH".
- wp_recv as "_".
- wp_smart_apply wp_assert.
- wp_pures. iModIntro. iSplit; [iPureIntro; f_equiv; by case_bool_decide|].
- iIntros "!>". wp_pures. by iApply "IH". }
- wp_recv as "Hc'". wp_pures. by iApply "HΦ".
- - case_bool_decide; [simplify_eq;lia|].
- wp_pures.
- wp_recv (c') as "Hc'".
- wp_send with "[//]".
- wp_send with "[Hc'//]".
- by iApply "HΦ".
- Qed.
-
- Lemma program_spec :
- {{{ True }}} program #() {{{ RET #(); True }}}.
- Proof.
- iIntros (Φ) "_ HΦ". wp_lam.
- wp_new_chan prot_pool with prot_pool_consistent
- as (c0 c1 c2 c3) "Hc0" "Hc1" "Hc2" "Hc3".
- wp_smart_apply (wp_fork with "[Hc1]").
- { iIntros "!>". wp_smart_apply (process_spec with "Hc1").
- iIntros (i') "Hc1". by wp_smart_apply (forward_spec with "Hc1"). }
- wp_smart_apply (wp_fork with "[Hc2]").
- { iIntros "!>". wp_smart_apply (process_spec with "Hc2").
- iIntros (i') "Hc2". by wp_smart_apply (forward_spec with "Hc2"). }
- wp_smart_apply (wp_fork with "[Hc3]").
- { iIntros "!>". wp_smart_apply (process_spec with "Hc3").
- iIntros (i') "Hc3". by wp_smart_apply (forward_spec with "Hc3"). }
- wp_smart_apply (init_spec with "Hc0").
- iIntros (i') "Hc0". by wp_smart_apply (forward_spec with "Hc0").
- 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.
diff --git a/multi_actris/channel/channel.v b/multris/channel/channel.v
similarity index 98%
rename from multi_actris/channel/channel.v
rename to multris/channel/channel.v
index c0a0fbb..46083fd 100644
--- a/multi_actris/channel/channel.v
+++ b/multris/channel/channel.v
@@ -21,9 +21,9 @@ the subprotocol relation [⊑] *)
From iris.algebra Require Import gmap excl_auth gmap_view.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Export primitive_laws notation proofmode.
-From multi_actris.utils Require Import matrix.
-From multi_actris.channel Require Import proto_model.
-From multi_actris.channel Require Export proto.
+From multris.utils Require Import matrix.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export proto.
Set Default Proof Using "Type".
(** * The definition of the message-passing connectives *)
@@ -162,7 +162,7 @@ Section channel.
{ apply excl_auth_valid. }
iMod ("IHn" with "Hps'") as (γEs Hlen) "H".
iModIntro. iExists (γEs++[γE]).
- rewrite !app_length Hlen.
+ rewrite !length_app Hlen.
iSplit; [iPureIntro=>/=;lia|]=> /=.
iSplitL "H".
{ iApply (big_sepL_impl with "H").
diff --git a/multi_actris/channel/proofmode.v b/multris/channel/proofmode.v
similarity index 99%
rename from multi_actris/channel/proofmode.v
rename to multris/channel/proofmode.v
index 2c02a5c..d3da00d 100644
--- a/multi_actris/channel/proofmode.v
+++ b/multris/channel/proofmode.v
@@ -10,8 +10,8 @@ recursive protocols are contractive. *)
From iris.algebra Require Import gmap.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.heap_lang Require Export proofmode notation.
-From multi_actris.channel Require Import proto_model.
-From multi_actris.channel Require Export channel.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export channel.
Set Default Proof Using "Type".
(** * Tactics for proving contractiveness of protocols *)
diff --git a/multi_actris/channel/proto.v b/multris/channel/proto.v
similarity index 99%
rename from multi_actris/channel/proto.v
rename to multris/channel/proto.v
index aaae475..56522bb 100644
--- a/multi_actris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -6,7 +6,7 @@ From iris.proofmode Require Import proofmode.
From iris.base_logic Require Export lib.iprop.
From iris.base_logic Require Import lib.own.
From iris.program_logic Require Import language.
-From multi_actris.channel Require Import proto_model.
+From multris.channel Require Import proto_model.
Set Default Proof Using "Type".
Export action.
diff --git a/multi_actris/channel/proto_model.v b/multris/channel/proto_model.v
similarity index 99%
rename from multi_actris/channel/proto_model.v
rename to multris/channel/proto_model.v
index 007f8ef..3dc4bf0 100644
--- a/multi_actris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -36,7 +36,7 @@ The defined functions on the type [proto] are:
all terminations [END] in [p1] with [p2]. *)
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import proofmode.
-From multi_actris.utils Require Import cofe_solver_2.
+From multris.utils Require Import cofe_solver_2.
Set Default Proof Using "Type".
Module Export action.
diff --git a/multi_actris/examples/basics.v b/multris/examples/basics.v
similarity index 99%
rename from multi_actris/examples/basics.v
rename to multris/examples/basics.v
index 80169be..53ad44a 100644
--- a/multi_actris/examples/basics.v
+++ b/multris/examples/basics.v
@@ -1,4 +1,4 @@
-From multi_actris.channel Require Import proofmode.
+From multris.channel Require Import proofmode.
Set Default Proof Using "Type".
Definition iProto_empty {Σ} : list (iProto Σ) := [].
diff --git a/multi_actris/examples/leader_election_del_alt.v b/multris/examples/leader_election.v
similarity index 99%
rename from multi_actris/examples/leader_election_del_alt.v
rename to multris/examples/leader_election.v
index 093badc..c833695 100644
--- a/multi_actris/examples/leader_election_del_alt.v
+++ b/multris/examples/leader_election.v
@@ -1,6 +1,6 @@
From iris.heap_lang Require Import adequacy.
From iris.heap_lang.lib Require Import assert.
-From multi_actris.channel Require Import proofmode.
+From multris.channel Require Import proofmode.
(** Inspired by https://en.wikipedia.org/wiki/Chang_and_Roberts_algorithm *)
diff --git a/multi_actris/examples/three_buyer.v b/multris/examples/three_buyer.v
similarity index 99%
rename from multi_actris/examples/three_buyer.v
rename to multris/examples/three_buyer.v
index aa4c6e8..a4d24c4 100644
--- a/multi_actris/examples/three_buyer.v
+++ b/multris/examples/three_buyer.v
@@ -1,4 +1,4 @@
-From multi_actris.channel Require Import proofmode.
+From multris.channel Require Import proofmode.
Set Default Proof Using "Type".
Definition buyer1_prog : val :=
diff --git a/multi_actris/examples/two_buyer.v b/multris/examples/two_buyer.v
similarity index 98%
rename from multi_actris/examples/two_buyer.v
rename to multris/examples/two_buyer.v
index 15eef77..a317924 100644
--- a/multi_actris/examples/two_buyer.v
+++ b/multris/examples/two_buyer.v
@@ -1,4 +1,4 @@
-From multi_actris.channel Require Import proofmode.
+From multris.channel Require Import proofmode.
Set Default Proof Using "Type".
Definition buyer1_prog : val :=
diff --git a/multi_actris/utils/cofe_solver_2.v b/multris/utils/cofe_solver_2.v
similarity index 100%
rename from multi_actris/utils/cofe_solver_2.v
rename to multris/utils/cofe_solver_2.v
diff --git a/multi_actris/utils/matrix.v b/multris/utils/matrix.v
similarity index 100%
rename from multi_actris/utils/matrix.v
rename to multris/utils/matrix.v
--
GitLab