Ensure --choreography really only does choreographic verification

src/col/vct/col/util/AstBuildHelpers.scala

@@ -832,6 +832,17 @@ object AstBuildHelpers {
     Forall(bindings = Seq(i_var), triggers = triggers(i), body = body(i))
   }
 
+  def forallAny[G](indicator: Type[_])(
+      blame: Blame[ReceiverNotInjective],
+      t: Type[G],
+      body: Local[G] => Expr[G],
+      triggers: Local[G] => Seq[Seq[Expr[G]]] = (_: Local[G]) => Nil,
+  ): Expr[G] =
+    indicator match {
+      case TBool() => forall(t, body, triggers)
+      case TResource() => starall(blame, t, body, triggers)
+    }
+
   def forrange[G](high: Expr[G], body: Local[G] => Expr[G]): Forall[G] =
     forrange(const(0)(DiagnosticOrigin), high, body, (_: Local[G]) => Nil)
 

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

@@ -207,14 +207,20 @@ object VeyMont extends LazyLogging {
 
         next()
 
-        val implementation =
-          generateWithOptions(options, program)
-            .fold[GenerateResult](err => return Left(err), lit => lit)
-            .implementation
+        if (!options.veymontSkipImplementationGeneration) {
+          val implementation =
+            generateWithOptions(options, program)
+              .fold[GenerateResult](err => return Left(err), lit => lit)
+              .implementation
 
-        next()
+          next()
 
-        implementationWithOptions(options, implementation)
+          implementationWithOptions(options, implementation)
+        } else {
+          assert(options.veymontSkipImplementationVerification);
+          logger.warn("Skipping implementation generation and verification")
+          Right(ImplementationResult(Seq()))
+        }
       }
     }
   }

src/main/vct/options/Options.scala

@@ -319,7 +319,10 @@ case object Options {
         "Enable VeyMont mode: decompose the global program from the input files into several local programs that can be executed in parallel"
       ).children(
         opt[Unit]("choreography").abbr("chor").action((_, c) =>
-          c.copy(veymontSkipImplementationVerification = true)
+          c.copy(
+            veymontSkipImplementationGeneration = true,
+            veymontSkipImplementationVerification = true,
+          )
         ).text("Only perform verification of the choreography."),
         opt[Unit]("implementation").abbr("impl")
           .action((_, c) => c.copy(veymontSkipChoreographyVerification = true))
@@ -341,8 +344,16 @@ case object Options {
         opt[Unit]("veymont-skip-choreography-verification")
           .action((_, c) => c.copy(veymontSkipChoreographyVerification = true))
           .text(
-            "Do not verify choreographies, skipping to implementation generation & verification immediately"
+            "Do not verify choreographies, skipping to implementation generation & verification immediately."
           ),
+        opt[Unit]("veymont-skip-implementation-generation").action((_, c) =>
+          c.copy(
+            veymontSkipImplementationGeneration = true,
+            veymontSkipImplementationVerification = true,
+          )
+        ).text(
+          "Do not generate an implementation. Implies `--veymont-skip-implementation-verification`."
+        ),
         opt[Unit]("veymont-skip-implementation-verification").action((_, c) =>
           c.copy(veymontSkipImplementationVerification = true)
         ).text("Do not verify generated implementation"),
@@ -520,6 +531,7 @@ case class Options(
     veymontPermissionStratificationMode: PermissionStratificationMode =
       EncodePermissionStratification.Mode.Wrap,
     veymontSkipChoreographyVerification: Boolean = false,
+    veymontSkipImplementationGeneration: Boolean = false,
     veymontSkipImplementationVerification: Boolean = false,
 
     // VeSUV options

src/rewrite/vct/rewrite/veymont/generation/SpecializeEndpointClasses.scala

@@ -64,6 +64,7 @@ case class SpecializeEndpointClasses[Pre <: Generation]()
   override def dispatch(expr: Expr[Pre]): Expr[Post] =
     expr match {
       case EndpointName(Ref(endpoint)) =>
+        assert(endpoint.isSingle)
         readImplField(expr.rewriteDefault(), endpoint)(expr.o)
       case Sender(Ref(comm)) =>
         readImplField(expr.rewriteDefault(), comm.sender.get.asName.endpoint)(
@@ -83,6 +84,7 @@ case class SpecializeEndpointClasses[Pre <: Generation]()
 
       case endpoint: Endpoint[Pre] =>
         implicit val o = endpoint.o
+        assert(endpoint.isSingle)
 
         val implField =
           new InstanceField[Post](dispatch(endpoint.singleType), Seq())(
@@ -192,6 +194,7 @@ case class SpecializeEndpointClasses[Pre <: Generation]()
       chor: Choreography[Pre]
   )(implicit o: Origin): Expr[Post] = {
     foldStar(chor.endpoints.flatMap { endpoint =>
+      assert(endpoint.isSingle)
       chor.endpoints.map { peer =>
         EndpointExpr[Post](
           CommTargetEndpoint(succ(endpoint)),

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

@@ -259,7 +259,28 @@ case class EncodePermissionStratification[Pre <: Generation](
     override def dispatch(expr: Expr[Pre]): Expr[Post] =
       expr match {
         case ChorExpr(inner) => dispatch(inner)
-        case EndpointExpr(_, inner) => dispatch(inner)
+        case EndpointExpr(
+              CommTargetEndpoint(_) | CommTargetIndex(_, _),
+              inner,
+            ) =>
+          dispatch(inner)
+        case EndpointExpr(
+              CommTargetRange(ep, RangeBinder(v, low, high)),
+              inner,
+            ) =>
+          variables.scope {
+            starrange(
+              // TODO (RR): Forward injectivity
+              PanicBlame("Need to forward injectivity"),
+              dispatch(low),
+              dispatch(high),
+              i => {
+                // TODO (RR): i must have same name as v above
+                variables.succeedOnly(v, i.ref.decl)
+                dispatch(inner)
+              },
+            )
+          }
         case _ => expr.rewriteDefault()
       }
   }
@@ -571,7 +592,9 @@ case class EncodePermissionStratification[Pre <: Generation](
           ) =>
         implicit val o: Origin = target.o
         variables.scope {
-          forall(
+          forallAny(inner.t)(
+            // TODO (RR): Forward injectivity
+            PanicBlame("Need to forward injectivity..."),
             TInt(),
             i => {
               // TODO (RR): `i` should have origin of `v` here...!

test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala

@@ -37,6 +37,28 @@ class TechnicalVeyMontSpec2 extends VeyMontSpec {
     """,
   )
 
+  choreography(
+    desc = "Branch unanimity is checked of parameterized choreographies",
+    pvl = """
+      class Storage {
+         int x;
+      }
+
+      requires N >= 0;
+      choreography Example(int N) {
+         endpoint nodes[tid := 0 .. N] = Storage();
+
+         requires N >= 0;
+         requires (\endpoint nodes[i := 0 .. N]; Perm(nodes[i].x, read) ** nodes[i].x > 0);
+         run {
+            if ((\endpoint nodes[i := 0 .. N]; nodes[i].x > 0)) {
+
+            }
+         }
+      }
+    """,
+  )
+
   choreography(
     desc = "Scoping of the binder of endpoint ranges is not handled properly",
     pvl = """