VeyMont: channel invariant, stratified expression containers

examples/concepts/veymont/annotatedPermissions/swap.pvl

@@ -6,11 +6,12 @@ choreography swap(int x, int y) {
   endpoint a = Role();
   endpoint b = Role();
 
-  context Perm(a.v, 1) ** Perm(a.temp, 1);
-  context Perm(b.v, 1) ** Perm(b.temp, 1);
+  context Perm(a.v, 1) ** Perm(a.temp, 1) ** a.v == 0;
+  context Perm(b.v, 1) ** Perm(b.temp, 1) ** b.v == 1;
   run {
     a.v := x;
     b.v := y;
+    channel_invariant \sender != \receiver && \msg == \msg;
     communicate a.v -> b.temp;
     communicate b.v -> a.temp;
     a.v := a.temp;

examples/concepts/veymont/generatedPermissions/TicTacToe/Player.pvl

@@ -1,7 +1,7 @@
 class Player {
 	int c00, c01, c02, c10, c11, c12, c20, c21, c22;
 	int myToken;
-	Move move, temp;
+	Move move;
 	boolean turn;
 
 
@@ -25,7 +25,6 @@ class Player {
 		myToken = tok;
 		turn = t;
 		move = new Move(0, 0, tok);
-		temp = new Move(-1, -1, -1);
 	}
 
 

examples/concepts/veymont/generatedPermissions/TicTacToe/TicTacToe.pvl

@@ -7,24 +7,20 @@ choreography TTT() {
 	endpoint p1 = Player(0, true);
 	endpoint p2 = Player(1, false);
 
-	context ticTacToeAnnotations(p1, p2);
+	context (\chor ticTacToeAnnotations(p1, p2));
 	ensures p1.gameFinished() && p2.gameFinished();
 	run {
-		loop_invariant ticTacToeAnnotations(p1, p2);
-		loop_invariant !p1.gameFinished() == !p2.gameFinished();
+		loop_invariant (\chor ticTacToeAnnotations(p1, p2));
+		loop_invariant (\chor !p1.gameFinished() == !p2.gameFinished());
 		while(!p1.gameFinished() && !p2.gameFinished()) {
 		  // TODO (RR): Re-enable with in_chor
 			// assert p1.turn == !p2.turn;
 			if(p1.turn && !p2.turn) {
 				p1.createNewMove();
-				p1.temp := p1.move.clone();
-				communicate p2.move <- p1.temp;
-				p1.temp := new Move(-1, -1, -1); // TODO (RR): Workaround for not having memory management, delete when we support exprs in communicate
+				communicate p2.move <- p1.move.clone();
 			} else {
 				p2.createNewMove();
-				p2.temp := p2.move.clone();
-				communicate p1.move <- p2.temp;
-				p2.temp := new Move(-1, -1, -1); // TODO (RR): Workaround for not having memory management, delete when we support exprs in communicate
+				communicate p1.move <- p2.move.clone();
 			}
 			p1.doMove();
 			p2.doMove();

examples/concepts/veymont/generatedPermissions/leaderelectring.pvl

@@ -33,7 +33,7 @@ choreography leaderElectRing() {
 	ensures c.maxVal == c.maxVal(a.rank,b.rank,d.rank,c.rank);
 	ensures c.maxVal == a.rank || c.maxVal == b.rank || c.maxVal == c.rank || c.maxVal == d.rank;
 	run {
-	    loop_invariant a.rank == \old(a.rank) ** b.rank == \old(b.rank) ** c.rank == \old(c.rank) ** d.rank == \old(d.rank);
+    loop_invariant a.rank == \old(a.rank) ** b.rank == \old(b.rank) ** c.rank == \old(c.rank) ** d.rank == \old(d.rank);
 		loop_invariant a.rank != b.rank && a.rank != c.rank && a.rank != d.rank && b.rank != c.rank && b.rank != d.rank && c.rank != d.rank;
 		loop_invariant 0 <= c.n && c.n <= 3;
 		loop_invariant a.n == c.n && b.n == c.n && d.n == c.n;
@@ -49,7 +49,7 @@ choreography leaderElectRing() {
 		loop_invariant c.n == 3 ==> a.maxVal == a.maxVal(a.rank,b.rank,c.rank,d.rank);
 		loop_invariant c.n == 3 ==> b.maxVal == b.maxVal(a.rank,b.rank,c.rank,d.rank);
 		loop_invariant c.n == 3 ==> c.maxVal == c.maxVal(a.rank,b.rank,c.rank,d.rank);
-		loop_invariant c.n == 3 ==> d.maxVal == d.maxVal(a.rank,b.rank,c.rank,d.rank); 
+		loop_invariant c.n == 3 ==> d.maxVal == d.maxVal(a.rank,b.rank,c.rank,d.rank);
 		while(a.n < 3 && b.n < 3 && c.n < 3 && d.n < 3) {
 			communicate a.left <- d.maxVal;
 			communicate b.left <- a.maxVal;

examples/technical/veymont/checkMainSyntaxAndWellFormedness/WhileCondition.pvl

@@ -1,9 +1,9 @@
 choreography Main() {
-    endpoint a = Role(5);
-    endpoint b = Role(6);
-    endpoint c = Role(7);
+  endpoint a = Role(5);
+  endpoint b = Role(6);
+  endpoint c = Role(7);
 
-    requires a.x == 5 && b.x == 6 && c.x == 7;
+  requires a.x == 5 && b.x == 6 && c.x == 7;
 	run {
 		while(a.x >= 5 && b.x == 6 && c.x == 7) {
 			c.x := -2;

examples/technical/veymont/genericEndpoints.pvl

@@ -14,7 +14,6 @@ choreography genericTest() {
   endpoint a = Role<A>();
   endpoint b = Role<B>();
 
-  requires a != b;
   run {
     a.i := a.toInt(a.t);
     communicate a.i -> b.i;

res/universal/res/veymont/genericChannel.pvl

@@ -1,26 +1,26 @@
-lock_invariant Perm(transferring, 1) ** Perm(exchangeValue,1);
+lock_invariant Perm(hasMsg, 1) ** Perm(exchangeValue,1);
 class Channel<T> {
-  boolean transferring;
+  boolean hasMsg;
   T exchangeValue;
 
   ensures committed(this);
   constructor() {
-    transferring = false;
+    hasMsg = false;
     commit this;
   }
 
   requires committed(this);
   void writeValue(T v) {
     lock this;
 
-    loop_invariant Perm(transferring, 1) ** Perm(exchangeValue,1);
+    loop_invariant Perm(hasMsg, 1) ** Perm(exchangeValue,1);
     loop_invariant held(this);
-    while (!transferring) {
+    while (!hasMsg) {
       unlock this;
       lock this;
     }
 
-    transferring = false;
+    hasMsg = false;
     exchangeValue = v;
     unlock this;
   }
@@ -29,14 +29,14 @@ class Channel<T> {
   T readValue() {
     lock this;
 
-    loop_invariant Perm(transferring, 1) ** Perm(exchangeValue,1);
+    loop_invariant Perm(hasMsg, 1) ** Perm(exchangeValue,1);
     loop_invariant held(this);
-    while (transferring) {
+    while (hasMsg) {
       wait this;
     }
 
     T m = exchangeValue;
-    transferring = false;
+    hasMsg = false;
     unlock this;
 
     return m;

src/col/vct/col/ast/Node.scala

@@ -56,7 +56,6 @@ import vct.col.ast.family.location._
 import vct.col.ast.family.loopcontract._
 import vct.col.ast.family.parregion._
 import vct.col.ast.family.pvlcommunicate._
-import vct.col.ast.family.seqguard._
 import vct.col.ast.family.seqrun._
 import vct.col.ast.family.signals._
 import vct.col.ast.lang.c._
@@ -3607,11 +3606,11 @@ final case class PVLCommunicate[G](
   var inferredSender: Option[PVLEndpoint[G]] = None
   var inferredReceiver: Option[PVLEndpoint[G]] = None
 }
-final case class PVLChorStatement[G](
+final case class PVLEndpointStatement[G](
     endpoint: Option[PVLEndpointName[G]],
     inner: Statement[G],
 )(val blame: Blame[ChorStatementFailure])(implicit val o: Origin)
-    extends Statement[G] with PVLChorStatementImpl[G]
+    extends Statement[G] with PVLEndpointStatementImpl[G]
 final case class PVLChorPerm[G](
     endpoint: PVLEndpointName[G],
     loc: Location[G],
@@ -3702,36 +3701,24 @@ final case class UnresolvedChorLoop[G](
     with ControlContainerStatement[G]
     with UnresolvedChorLoopImpl[G]
 
-final case class ChorStatement[G](
+final case class ChorStatement[G](inner: Statement[G])(implicit val o: Origin)
+    extends Statement[G] with ChorStatementImpl[G]
+final case class EndpointStatement[G](
     endpoint: Option[Ref[G, Endpoint[G]]],
     inner: Statement[G],
 )(val blame: Blame[ChorStatementFailure])(implicit val o: Origin)
-    extends Statement[G] with ChorStatementImpl[G]
+    extends Statement[G] with EndpointStatementImpl[G]
 
-@family
-sealed trait ChorGuard[G] extends NodeFamily[G] with ChorGuardImpl[G]
-final case class EndpointGuard[G](
-    endpoint: Ref[G, Endpoint[G]],
-    condition: Expr[G],
+final case class PVLEndpointExpr[G](
+    endpoint: PVLEndpointName[G],
+    expr: Expr[G],
 )(implicit val o: Origin)
-    extends ChorGuard[G] with EndpointGuardImpl[G]
-final case class UnpointedGuard[G](condition: Expr[G])(implicit val o: Origin)
-    extends ChorGuard[G] with UnpointedGuardImpl[G]
-
-final case class ChorBranch[G](
-    guards: Seq[ChorGuard[G]],
-    yes: Statement[G],
-    no: Option[Statement[G]],
-)(val blame: Blame[SeqBranchFailure])(implicit val o: Origin)
-    extends Statement[G]
-    with ControlContainerStatement[G]
-    with ChorBranchImpl[G]
-final case class ChorLoop[G](
-    guards: Seq[ChorGuard[G]],
-    contract: LoopContract[G],
-    body: Statement[G],
-)(val blame: Blame[SeqLoopFailure])(implicit val o: Origin)
-    extends Statement[G] with ControlContainerStatement[G] with ChorLoopImpl[G]
+    extends Expr[G] with PVLEndpointExprImpl[G]
+final case class EndpointExpr[G](endpoint: Ref[G, Endpoint[G]], expr: Expr[G])(
+    implicit val o: Origin
+) extends Expr[G] with EndpointExprImpl[G]
+final case class ChorExpr[G](expr: Expr[G])(implicit val o: Origin)
+    extends Expr[G] with ChorExprImpl[G]
 
 final case class VeyMontAssignExpression[G](
     endpoint: Ref[G, Endpoint[G]],

src/col/vct/col/ast/declaration/global/ChoreographyImpl.scala

@@ -4,13 +4,13 @@ import vct.col.ast.declaration.DeclarationImpl
 import vct.col.ast.{
   Assign,
   ChorStatement,
+  Choreography,
   Class,
   Declaration,
   Endpoint,
-  EndpointGuard,
   EndpointName,
+  EndpointStatement,
   Node,
-  Choreography,
 }
 import vct.col.ast.util.Declarator
 import vct.col.check.{CheckContext, CheckError}
@@ -24,10 +24,10 @@ import vct.col.ast.ops.ChoreographyOps
 object ChoreographyImpl {
   def participants[G](node: Node[G]): ListSet[Endpoint[G]] =
     ListSet.from(node.collect {
-      case EndpointGuard(Ref(endpoint), _) => endpoint
-      case ChorStatement(Some(Ref(endpoint)), Assign(_, _)) => endpoint
-      case EndpointName(Ref(endpoint)) => endpoint
-    })
+      case EndpointStatement(Some(Ref(endpoint)), Assign(_, _)) => Seq(endpoint)
+      case EndpointName(Ref(endpoint)) => Seq(endpoint)
+      case c @ ChorStatement(_) => c.participants.toSeq
+    }.flatten)
 }
 
 trait ChoreographyImpl[G]
@@ -39,7 +39,8 @@ trait ChoreographyImpl[G]
     Doc.stack(Seq(
       contract,
       Group(
-        Text("seq_program") <+> ctx.name(this) <> "(" <> Doc.args(params) <> ")"
+        Text("choreography") <+> ctx.name(this) <> "(" <> Doc.args(params) <>
+          ")"
       ) <+> "{" <>> Doc.stack(
         endpoints ++ decls :+
           preRun.map(preRun => Text("/* preRun */") <+> preRun.show)

src/col/vct/col/ast/expr/heap/read/DerefImpl.scala

@@ -1,7 +1,15 @@
 package vct.col.ast.expr.heap.read
 
 import vct.col.ast.expr.ExprImpl
-import vct.col.ast.{Deref, EndpointName, Expr, TClass, Type}
+import vct.col.ast.{
+  Deref,
+  EndpointName,
+  Expr,
+  FieldLocation,
+  TClass,
+  Type,
+  Value,
+}
 import vct.col.check.{Check, CheckContext, CheckError, SeqProgReceivingEndpoint}
 import vct.col.print.{Ctx, Doc, Group, Precedence}
 import vct.col.ref.Ref
@@ -21,4 +29,6 @@ trait DerefImpl[G] extends ExprImpl[G] with DerefOps[G] {
   override def precedence: Int = Precedence.POSTFIX
   override def layout(implicit ctx: Ctx): Doc =
     assoc(obj) <> "." <> ctx.name(ref)
+
+  def value: Value[G] = Value(FieldLocation(obj, ref))
 }

src/col/vct/col/ast/expr/resource/ValueImpl.scala

@@ -1,6 +1,6 @@
 package vct.col.ast.expr.resource
 
-import vct.col.ast.{TResource, Type, Value}
+import vct.col.ast.{Deref, FieldLocation, TResource, Type, Value}
 import vct.col.print.{Ctx, Doc, Group, Precedence, Text}
 import vct.col.ast.ops.ValueOps
 

src/col/vct/col/ast/family/pvlcommunicate/PVLEndpointNameImpl.scala

@@ -1,10 +1,16 @@
 package vct.col.ast.family.pvlcommunicate
 
 import vct.col.ast.PVLEndpointName
+import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast.ops.PVLEndpointNameOps
-import vct.col.ast.ops.{PVLEndpointNameOps, PVLEndpointNameFamilyOps}
+import vct.col.ast.ops.{PVLEndpointNameFamilyOps, PVLEndpointNameOps}
+import vct.col.print.{Ctx, Doc, Text}
 
 trait PVLEndpointNameImpl[G]
-    extends PVLEndpointNameOps[G] with PVLEndpointNameFamilyOps[G] {
+    extends PVLEndpointNameOps[G]
+    with PVLEndpointNameFamilyOps[G]
+    with NodeFamilyImpl[G] {
   this: PVLEndpointName[G] =>
+
+  override def layout(implicit ctx: Ctx): Doc = Text(name)
 }

src/col/vct/col/ast/family/seqrun/ChorRunImpl.scala

@@ -8,6 +8,6 @@ import vct.col.ast.ops.{ChorRunOps, ChorRunFamilyOps}
 trait ChorRunImpl[G] extends ChorRunOps[G] with ChorRunFamilyOps[G] {
   this: ChorRun[G] =>
   override def layout(implicit ctx: Ctx): Doc = {
-    contract.show </> Text("seq_run") <+> this.body.show
+    contract.show </> Text("run") <+> this.body.show
   }
 }

src/col/vct/col/ast/statement/StatementImpl.scala

@@ -2,7 +2,7 @@ package vct.col.ast.statement
 
 import vct.col.ast.node.NodeFamilyImpl
 import vct.col.ast._
-import vct.col.check.{CheckContext, CheckError, SeqProgStatement}
+import vct.col.check.{CheckContext, CheckError, ChorStatement}
 import vct.col.print._
 import vct.col.ast.ops.StatementFamilyOps