Skip to content
Snippets Groups Projects
Commit 6a4c7570 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Proof of concept for synchronous resource transfer

parent 4af1c72f
No related branches found
No related tags found
1 merge request!39Multiparty synchronous
Expand all Hide whitespace changes
Inline Side-by-side
theories/channel/channel.v
+ 220
− 267
View file @ 6a4c7570
This diff is collapsed.
theories/channel/proto.v
+ 4
− 4
View file @ 6a4c7570
...@@ -1206,8 +1206,8 @@ Section proto. ...@@ -1206,8 +1206,8 @@ Section proto.
Lemma iProto_step_l γ m1 m2 p1 v : Lemma iProto_step_l γ m1 m2 p1 v :
iProto_ctx γ -∗ iProto_own γ Left (<!> m1) -∗ iProto_own γ Right (<?> m2) -∗ iProto_ctx γ -∗ iProto_own γ Left (<!> m1) -∗ iProto_own γ Right (<?> m2) -∗
iMsg_car m1 v (Next p1) ==∗ iMsg_car m1 v (Next p1) ==∗
▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_ctx γ ∗ ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ∗
iProto_own γ Left p1 ∗ iProto_own γ Right p2. iProto_own γ Left p1 ∗ iProto_own γ Right p2.
Proof. Proof.
iDestruct 1 as (pl pr) "(H●l & H●r & Hconsistent)". iDestruct 1 as (pl pr) "(H●l & H●r & Hconsistent)".
iDestruct 1 as (pl') "[Hlel H◯l]". iDestruct 1 as (pl') "[Hlel H◯l]".
...@@ -1237,8 +1237,8 @@ Section proto. ...@@ -1237,8 +1237,8 @@ Section proto.
Lemma iProto_step_r γ m1 m2 p2 v : Lemma iProto_step_r γ m1 m2 p2 v :
iProto_ctx γ -∗ iProto_own γ Left (<?> m1) -∗ iProto_own γ Right (<!> m2) -∗ iProto_ctx γ -∗ iProto_own γ Left (<?> m1) -∗ iProto_own γ Right (<!> m2) -∗
iMsg_car m2 v (Next p2) ==∗ iMsg_car m2 v (Next p2) ==∗
▷ ∃ p1, iMsg_car m1 v (Next p1) ∗ ▷ iProto_ctx γ ∗ ▷ ∃ p1, iMsg_car m1 v (Next p1) ∗ iProto_ctx γ ∗
iProto_own γ Left p1 ∗ iProto_own γ Right p2. iProto_own γ Left p1 ∗ iProto_own γ Right p2.
Proof. Proof.
iDestruct 1 as (pl pr) "(H●l & H●r & Hconsistent)". iDestruct 1 as (pl pr) "(H●l & H●r & Hconsistent)".
iDestruct 1 as (pl') "[Hlel H◯l]". iDestruct 1 as (pl') "[Hlel H◯l]".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment