Extend gitignore, make veymont error clearer

.gitignore

@@ -61,4 +61,5 @@ __pycache__
 
 # Misc
 *.pprof
-*.vpr
+*.vpr
+test.pvl

examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/2-TTTlast.pvl

@@ -61,6 +61,8 @@ choreography Main() {
           (!\sender.gameFinished() ==> ([1\2]\sender.returnerMark()));
         communicate p2.move <- p1.move.copy();
         p2.doMove();
+        assert (\endpoint p2; p2.equalBoard(p1));
+        assert (\endpoint p2; !p1.gameFinished() == !p2.gameFinished());
       } else {
         p2.createNewMove();
         p2.doMove();
@@ -76,13 +78,15 @@ choreography Main() {
           (!\sender.gameFinished() ==> ([1\2]\sender.returnerMark()));
         communicate p1.move <- p2.move.copy();
         p1.doMove();
+        assert (\endpoint p1; p1.equalBoard(p2));
+        assert (\endpoint p1; !p1.gameFinished() == !p2.gameFinished());
       }
       p1.turn := !p1.turn;
       p2.turn := !p2.turn;
       // Assumption required for shortcoming in backend. Can be removed after implementing the lightweight encoding.
-      assume (\chor p1.gameFinished() == p2.gameFinished());
+      // assume (\chor p1.gameFinished() == p2.gameFinished());
     }
-    assume (\chor p1.gameFinished() == p2.gameFinished());
+    // assume (\chor p1.gameFinished() == p2.gameFinished());
 
     p1.finish();
     p2.finish();

examples/publications/2024/IFM2024VeyMontPermissions/2-TTTlast/Player.pvl

@@ -9,8 +9,9 @@ class Player {
   Move move;
   boolean turn;
   Returner returner;
-
-  inline resource boardPerm() = 
+
+  // TODO (RR): Remove comment if it works
+  /* inline */ resource boardPerm() =
       Perm(c00, 1) ** Perm(c01, 1) ** Perm(c02, 1) ** 
       Perm(c10, 1) ** Perm(c11, 1) ** Perm(c12, 1) ** 
       Perm(c20, 1) ** Perm(c21, 1) ** Perm(c22, 1);
@@ -27,10 +28,11 @@ class Player {
     ;
 
   requires [1\2]boardPerm();
-  pure boolean emptyBoard() = 
-    c00 == -1 && c01 == -1 && c02 == -1 && 
-    c10 == -1 && c11 == -1 && c12 == -1 && 
-    c20 == -1 && c21 == -1 && c22 == -1;
+  pure boolean emptyBoard() =
+    (\unfolding [1\2]boardPerm() \in
+      c00 == -1 && c01 == -1 && c02 == -1 &&
+      c10 == -1 && c11 == -1 && c12 == -1 &&
+      c20 == -1 && c21 == -1 && c22 == -1);
 
   requires tok == 0 || tok == 1;
   ensures boardPerm();
@@ -55,6 +57,7 @@ class Player {
     myMark = tok;
     turn = t;
     move = new Move(0, 0, 0);
+    fold boardPerm();
   }
 
   requires tok == 0 || tok == 1;
@@ -88,38 +91,41 @@ class Player {
 
     fold returnerBound(other);
     fold returnerMark();
+    fold boardPerm();
   }
 
   requires ([1\100]boardPerm()) ** ([1\100]other.boardPerm());
   requires Perm(move.i, read) ** Perm(move.j, read) ** Perm(move.mark, read);
   requires 0 <= move.i && move.i <= 2;
   requires 0 <= move.j && move.j <= 2;
-  pure boolean oneMoveAheadOf(Move move, Player other) = 
-    readMoveCell(move,this) == move.mark && readMoveCell(move,other) == -1
-    && (move.i != 0 || move.j != 0 ==> other.c00 == c00)
-    && (move.i != 0 || move.j != 1 ==> other.c01 == c01)
-    && (move.i != 0 || move.j != 2 ==> other.c02 == c02)
-    && (move.i != 1 || move.j != 0 ==> other.c10 == c10)
-    && (move.i != 1 || move.j != 1 ==> other.c11 == c11)
-    && (move.i != 1 || move.j != 2 ==> other.c12 == c12)
-    && (move.i != 2 || move.j != 0 ==> other.c20 == c20)
-    && (move.i != 2 || move.j != 1 ==> other.c21 == c21)
-    && (move.i != 2 || move.j != 2 ==> other.c22 == c22);
+  pure boolean oneMoveAheadOf(Move move, Player other) =
+      readMoveCell(move,this) == move.mark && readMoveCell(move,other) == -1 &&
+      (\unfolding [1\100]boardPerm() \in (\unfolding [1\100]other.boardPerm() \in
+         (move.i != 0 || move.j != 0 ==> other.c00 == c00)
+      && (move.i != 0 || move.j != 1 ==> other.c01 == c01)
+      && (move.i != 0 || move.j != 2 ==> other.c02 == c02)
+      && (move.i != 1 || move.j != 0 ==> other.c10 == c10)
+      && (move.i != 1 || move.j != 1 ==> other.c11 == c11)
+      && (move.i != 1 || move.j != 2 ==> other.c12 == c12)
+      && (move.i != 2 || move.j != 0 ==> other.c20 == c20)
+      && (move.i != 2 || move.j != 1 ==> other.c21 == c21)
+      && (move.i != 2 || move.j != 2 ==> other.c22 == c22)));
 
   context boardPerm();
   context Perm(move,1\2) ** ([1\2]move.state());
   requires readMoveCell(move,this) == -1;
   ensures readMoveCell(move,this) == move.mark;
-  ensures move.i != 0 || move.j != 0 ==> \old(c00) == c00;
-  ensures move.i != 0 || move.j != 1 ==> \old(c01) == c01;
-  ensures move.i != 0 || move.j != 2 ==> \old(c02) == c02;
-  ensures move.i != 1 || move.j != 0 ==> \old(c10) == c10;
-  ensures move.i != 1 || move.j != 1 ==> \old(c11) == c11;
-  ensures move.i != 1 || move.j != 2 ==> \old(c12) == c12;
-  ensures move.i != 2 || move.j != 0 ==> \old(c20) == c20;
-  ensures move.i != 2 || move.j != 1 ==> \old(c21) == c21;
-  ensures move.i != 2 || move.j != 2 ==> \old(c22) == c22;      
+  ensures move.i != 0 || move.j != 0 ==> \old((\unfolding boardPerm() \in c00)) == (\unfolding boardPerm() \in c00);
+  ensures move.i != 0 || move.j != 1 ==> \old((\unfolding boardPerm() \in c01)) == (\unfolding boardPerm() \in c01);
+  ensures move.i != 0 || move.j != 2 ==> \old((\unfolding boardPerm() \in c02)) == (\unfolding boardPerm() \in c02);
+  ensures move.i != 1 || move.j != 0 ==> \old((\unfolding boardPerm() \in c10)) == (\unfolding boardPerm() \in c10);
+  ensures move.i != 1 || move.j != 1 ==> \old((\unfolding boardPerm() \in c11)) == (\unfolding boardPerm() \in c11);
+  ensures move.i != 1 || move.j != 2 ==> \old((\unfolding boardPerm() \in c12)) == (\unfolding boardPerm() \in c12);
+  ensures move.i != 2 || move.j != 0 ==> \old((\unfolding boardPerm() \in c20)) == (\unfolding boardPerm() \in c20);
+  ensures move.i != 2 || move.j != 1 ==> \old((\unfolding boardPerm() \in c21)) == (\unfolding boardPerm() \in c21);
+  ensures move.i != 2 || move.j != 2 ==> \old((\unfolding boardPerm() \in c22)) == (\unfolding boardPerm() \in c22);
   void doMove() {
+    unfold boardPerm();
     if(move.i == 0 && move.j == 0) {
       c00 = move.mark;
     } else if(move.i == 0 && move.j == 1) {
@@ -139,47 +145,52 @@ class Player {
     } else if(move.i == 2 && move.j == 2) {
       c22 = move.mark;
     }
+    fold boardPerm();
   }
 
   requires [1\100]boardPerm();
   pure boolean boardFull() =
-    c00 != -1 && c01 != -1 && c02 != -1 && 
-    c10 != -1 && c11 != -1 && c12 != -1 && 
-    c20 != -1 && c21 != -1 && c22  != -1;
+    (\unfolding [1\100]boardPerm() \in
+      c00 != -1 && c01 != -1 && c02 != -1 &&
+      c10 != -1 && c11 != -1 && c12 != -1 &&
+      c20 != -1 && c21 != -1 && c22  != -1);
 
   requires [1\100]boardPerm();
   pure boolean boardWin() =
-    c00 != -1 && c00 == c01 && c01 == c02 ||
-    c10 != -1 && c10 == c11 && c11 == c12 ||
-    c20 != -1 && c20 == c21 && c21 == c22 ||
-    c00 != -1 && c00 == c10 && c10 == c20 ||
-    c01 != -1 && c01 == c11 && c11 == c21 ||
-    c02 != -1 && c02 == c12 && c12 == c22 ||
-    c00 != -1 && c00 == c11 && c11 == c22 ||
-    c02 != -1 && c02 == c11 && c11 == c20;
+    (\unfolding [1\100]boardPerm() \in
+      c00 != -1 && c00 == c01 && c01 == c02 ||
+      c10 != -1 && c10 == c11 && c11 == c12 ||
+      c20 != -1 && c20 == c21 && c21 == c22 ||
+      c00 != -1 && c00 == c10 && c10 == c20 ||
+      c01 != -1 && c01 == c11 && c11 == c21 ||
+      c02 != -1 && c02 == c12 && c12 == c22 ||
+      c00 != -1 && c00 == c11 && c11 == c22 ||
+      c02 != -1 && c02 == c11 && c11 == c20);
 
   requires [1\100]boardPerm();
   pure boolean gameFinished() = boardFull() || boardWin();
 
   requires [1\100]boardPerm();
   requires [1\100]other.boardPerm();
   pure boolean equalBoard(Player other) =
-    c00 == other.c00 && c01 == other.c01 && c02 == other.c02 && 
-    c10 == other.c10 && c11 == other.c11 && c12 == other.c12 && 
-    c20 == other.c20 && c21 == other.c21 && c22 == other.c22;
+    (\unfolding [1\100]boardPerm() \in (\unfolding [1\100]other.boardPerm() \in
+      c00 == other.c00 && c01 == other.c01 && c02 == other.c02 &&
+      c10 == other.c10 && c11 == other.c11 && c12 == other.c12 &&
+      c20 == other.c20 && c21 == other.c21 && c22 == other.c22));
 
   requires [1\100]boardPerm();
-  pure int boardCount() = 0
-    + (c00 != -1 ? 1 : 0)
-    + (c01 != -1 ? 1 : 0)
-    + (c02 != -1 ? 1 : 0)
-    + (c10 != -1 ? 1 : 0)
-    + (c11 != -1 ? 1 : 0)
-    + (c12 != -1 ? 1 : 0)
-    + (c20 != -1 ? 1 : 0)
-    + (c21 != -1 ? 1 : 0)
-    + (c22 != -1 ? 1 : 0)
-    ;
+  pure int boardCount() =
+    (\unfolding [1\100]boardPerm() \in
+      0 + (c00 != -1 ? 1 : 0)
+      + (c01 != -1 ? 1 : 0)
+      + (c02 != -1 ? 1 : 0)
+      + (c10 != -1 ? 1 : 0)
+      + (c11 != -1 ? 1 : 0)
+      + (c12 != -1 ? 1 : 0)
+      + (c20 != -1 ? 1 : 0)
+      + (c21 != -1 ? 1 : 0)
+      + (c22 != -1 ? 1 : 0)
+    );
 
   context Perm(move,1) ** Perm(myMark, 1\2);
   context [1\100]boardPerm();
@@ -199,12 +210,13 @@ requires 0 <= move.i && move.i <= 2;
 requires 0 <= move.j && move.j <= 2;
 requires [1\100]p.boardPerm();
 pure int readMoveCell(Move move, Player p) =
-  (move.i == 0 && move.j == 0) ? p.c00
-  : (move.i == 0 && move.j == 1) ? p.c01
-  : (move.i == 0 && move.j == 2) ? p.c02
-  : (move.i == 1 && move.j == 0) ? p.c10
-  : (move.i == 1 && move.j == 1) ? p.c11
-  : (move.i == 1 && move.j == 2) ? p.c12
-  : (move.i == 2 && move.j == 0) ? p.c20
-  : (move.i == 2 && move.j == 1) ? p.c21
-  : p.c22;
+  (\unfolding [1\100]p.boardPerm() \in
+    ((move.i == 0 && move.j == 0) ? p.c00
+    : (move.i == 0 && move.j == 1) ? p.c01
+    : (move.i == 0 && move.j == 2) ? p.c02
+    : (move.i == 1 && move.j == 0) ? p.c10
+    : (move.i == 1 && move.j == 1) ? p.c11
+    : (move.i == 1 && move.j == 2) ? p.c12
+    : (move.i == 2 && move.j == 0) ? p.c20
+    : (move.i == 2 && move.j == 1) ? p.c21
+    : p.c22));

src/main/vct/main/modes/VeyMont.scala

@@ -48,10 +48,14 @@ object VeyMont extends LazyLogging {
   ) extends UserError {
     override def code: String = s"$codePrefix:${error.code}"
     override def text: String = s"$textPrefix\n${error.text}"
+
+    initCause(error)
   }
   case class WrapSystemError(textPrefix: String, error: SystemError)
       extends SystemError {
     override def text: String = s"$textPrefix\n${error.text}"
+
+    initCause(error)
   }
 
   def choreographyWithOptions(

src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala

@@ -57,11 +57,11 @@ case class EncodePermissionStratification[Pre <: Generation](
   val inChor = ScopedStack[Boolean]()
 
   lazy val specializedApplicables
-      : mut.LinkedHashMap[ContractApplicable[Pre], Seq[Endpoint[Pre]]] =
-    findInContext {
-      case inv: AnyFunctionInvocation[Pre] => inv.ref.decl
-      case inv: MethodInvocation[Pre] => inv.ref.decl
-    }
+      : mut.LinkedHashMap[Applicable[Pre], Seq[Endpoint[Pre]]] = findInContext {
+    case inv: AnyFunctionInvocation[Pre] => inv.ref.decl
+    case inv: MethodInvocation[Pre] => inv.ref.decl
+    case app: ApplyAnyPredicate[Pre] => app.ref.decl
+  }
 
   // Given a function f that finds Nodes inside nodes, findInContext keeps applying f
   // to nodes that f itself finds, until no more new nodes are found. The search is started
@@ -106,9 +106,7 @@ case class EncodePermissionStratification[Pre <: Generation](
   }
 
   val specializedApplicableSucc =
-    SuccessionMap[(Endpoint[Pre], ContractApplicable[Pre]), ContractApplicable[
-      Post
-    ]]()
+    SuccessionMap[(Endpoint[Pre], Applicable[Pre]), Applicable[Post]]()
 
   // Keeps track of the current anchoring/endpoint context identity expression for the current endpoint context.
   // E.g. within a choreograph, it is EndpointName(succ(endpoint)), within a specialized function it is a local
@@ -119,11 +117,14 @@ case class EncodePermissionStratification[Pre <: Generation](
   // this endpoint reference comes from one of the arguments of the function, not a literal endpointname expression.
   val specializing = ScopedStack[Expr[Post]]()
 
+  // TODO (RR): I think this key can be simplified - InstanceField always belongs to a particular class,
+  //            so the Type could theoretically be omitted?
   type WrapperPredicateKey = (Type[Pre], InstanceField[Pre])
   val wrapperPredicates = mut
     .LinkedHashMap[WrapperPredicateKey, Predicate[Post]]()
 
   // TODO (RR): It does not really wrap anymore, rename
+  // marker predicate to allow marking field permissions with an endpoint owner
   def wrapperPredicate(objT: Type[Pre], field: InstanceField[Pre])(
       implicit o: Origin
   ): Ref[Post, Predicate[Post]] = {
@@ -220,21 +221,24 @@ case class EncodePermissionStratification[Pre <: Generation](
       case m: InstanceMethod[Pre] if specializedApplicables.contains(m) =>
         m.rewriteDefault().succeed(m)
         specializeApplicable(m)
+      case p: Predicate[Pre] if specializedApplicables.contains(p) =>
+        p.rewriteDefault().succeed(p)
+        specializeApplicable(p)
+      case p: InstancePredicate[Pre] if specializedApplicables.contains(p) =>
+        p.rewriteDefault().succeed(p)
+        specializeApplicable(p)
       case _ => super.dispatch(decl)
     }
 
-  def specializeApplicable(app: ContractApplicable[Pre]): Unit = {
+  def specializeApplicable(app: Applicable[Pre]): Unit = {
     assert(app match {
-      case _: InstanceMethod[Pre] |
-          _: InstanceFunction[Pre] | _: Function[Pre] =>
+      case _: InstanceMethod[Pre] | _: InstanceFunction[Pre] |
+          _: Function[Pre] | _: Predicate[Pre] | _: InstancePredicate[Pre] =>
         true
       case _ => false
     })
 
-    def nameOrigin(
-        endpoint: Endpoint[Pre],
-        f: ContractApplicable[Pre],
-    ): Origin = {
+    def nameOrigin(endpoint: Endpoint[Pre], f: Applicable[Pre]): Origin = {
       f.o.where(indirect =
         Name.names(
           f.o.getPreferredNameOrElse(),
@@ -256,7 +260,7 @@ case class EncodePermissionStratification[Pre <: Generation](
 
             // Make sure plain perms are rewritten into wrapped perms
             specializing.having(endpointCtxVar.get(app.o)) {
-              val newF: ContractApplicable[Post] =
+              val newF: Applicable[Post] =
                 app match {
                   case f: InstanceFunction[Pre] =>
                     val newF = f.rewrite(
@@ -283,6 +287,18 @@ case class EncodePermissionStratification[Pre <: Generation](
                       o = nameOrigin(endpoint, m),
                     )
                     newM.declare()
+                  case p: InstancePredicate[Pre] =>
+                    val newP = p.rewrite(
+                      args = endpointCtxVar +: variables.dispatch(p.args),
+                      o = nameOrigin(endpoint, p),
+                    )
+                    newP.declare()
+                  case p: Predicate[Pre] =>
+                    val newP = p.rewrite(
+                      args = endpointCtxVar +: variables.dispatch(p.args),
+                      o = nameOrigin(endpoint, p),
+                    )
+                    newP.declare()
                 }
               specializedApplicableSucc((endpoint, app)) = newF
             }
@@ -340,6 +356,10 @@ case class EncodePermissionStratification[Pre <: Generation](
           expr.o
         )
 
+      case InEndpoint(_, _, cp: ChorPerm[Pre]) =>
+        // Matching on cp above already put the required specializing in place, so we can ignore it here
+        Perm(dispatch(cp.loc), dispatch(cp.perm))(cp.o)
+
       case InEndpoint(_, endpoint, Perm(loc: FieldLocation[Pre], perm)) =>
         makeWrappedPerm(loc, perm, specializing.top)(expr.o)
 
@@ -390,10 +410,32 @@ case class EncodePermissionStratification[Pre <: Generation](
           ref = specializedApplicableSucc.ref(k),
           args = specializing.top +: inv.args.map(dispatch),
         )
-
       case _ => expr.rewriteDefault()
     }
 
+  override def dispatch(app: ApplyAnyPredicate[Pre]): ApplyAnyPredicate[Post] =
+    app match {
+      case InEndpoint(_, endpoint, app: PredicateApply[Pre]) =>
+        val k = (endpoint, app.ref.decl)
+        app.rewrite(
+          ref = specializedApplicableSucc.ref(k),
+          args = specializing.top +: app.args.map(dispatch),
+        )
+      case InEndpoint(_, endpoint, app: InstancePredicateApply[Pre]) =>
+        val k = (endpoint, app.ref.decl)
+        app.rewrite(
+          ref = specializedApplicableSucc.ref(k),
+          args = specializing.top +: app.args.map(dispatch),
+        )
+      case InEndpoint(_, endpoint, app: CoalesceInstancePredicateApply[Pre]) =>
+        val k = (endpoint, app.ref.decl)
+        app.rewrite(
+          ref = specializedApplicableSucc.ref(k),
+          args = specializing.top +: app.args.map(dispatch),
+        )
+      case _ => app.rewriteDefault()
+    }
+
   override def dispatch(statement: Statement[Pre]): Statement[Post] =
     statement match {
       case EndpointStatement(None, Assign(_, _)) =>