Skip to content
Snippets Groups Projects

Added matrix abstraction and redefined channels using it

Merged Added matrix abstraction and redefined channels using it
multiparty_synchronous_matrix into multiparty_synchronous
Merged Jonas Kastberg requested to merge multiparty_synchronous_matrix into multiparty_synchronous
Viewing commit 528c968c
Prev
Show latest version
2 files
+ 166
− 4
Compare changes
  • Side-by-side
  • Inline
Files
2
multi_actris/channel/channel.v
+ 4
− 4
@@ -250,8 +250,8 @@ Section channel.
wp_pures.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
wp_smart_apply (matrix_get_spec_pers with "Hls"); [done..|].
iIntros (l') "Hl'".
wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
iIntros (l') "[Hl' _]".
iDestruct "Hl'" as (γt) "#IHl1".
wp_pures. wp_bind (Store _ _).
iInv "IHl1" as "HIp".
@@ -336,8 +336,8 @@ Section channel.
wp_pure _.
iDestruct "Hi" as %Hi.
iDestruct "Hj" as %Hj.
wp_smart_apply (matrix_get_spec_pers with "Hls"); [done..|].
iIntros (l') "Hl'".
wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
iIntros (l') "[Hl' _]".
iDestruct "Hl'" as (γt) "#IHl2".
wp_pures.
wp_bind (Xchg _ _).