Simplify use of chor, now that stratified permissions can be used tra…

…nsparently

src/col/vct/col/origin/Blame.scala

@@ -590,17 +590,6 @@ case class ChannelInvariantNotEstablished(
     s"The channel invariant at `$node` cannot be established, since $failure"
 }
 
-case class ChannelInvariantNotEstablishedLocally(
-    failure: ContractFailure,
-    node: Communicate[_],
-) extends CommunicateFailure with WithContractFailure {
-  override def baseCode: String = "channelInvariantNotEstablishedLocally"
-  override def descInContext: String =
-    "This channel invariant cannot be estalished when `\\chor` expressions are removed, since"
-  override def inlineDescWithSource(node: String, failure: String): String =
-    s"The channel invariant at `$node` cannot be established without `\\chor`, since $failure"
-}
-
 sealed trait DerefInsufficientPermission extends FrontendDerefError
 case class InsufficientPermission(node: HeapDeref[_])
     extends DerefInsufficientPermission with NodeVerificationFailure {

src/col/vct/col/typerules/CoercingRewriter.scala

@@ -2123,8 +2123,8 @@ abstract class CoercingRewriter[Pre <: Generation]()
       case Receiver(_) => e
       case Message(_) => e
       case PVLEndpointExpr(endpoint, expr) => e
-      case EndpointExpr(ref, expr) => e
-      case ChorExpr(expr) => e
+      case EndpointExpr(ref, expr) => EndpointExpr(ref, res(expr))
+      case ChorExpr(expr) => ChorExpr(bool(expr))
     }
   }
 

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

@@ -9,35 +9,24 @@ import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
 import vct.col.util.AstBuildHelpers._
 import vct.col.util.SuccessionMap
 import vct.rewrite.veymont.VeymontContext
-import vct.rewrite.veymont.verification.EncodeChannels.{
-  AssertFailedToChannelInvariantNotEstablished,
-  ExhaleFailedToChannelInvariantNotEstablished,
-}
+import vct.rewrite.veymont.verification.EncodeChannels.ExhaleFailedToChannelInvariantNotEstablished
 
 object EncodeChannels extends RewriterBuilder {
   override def key: String = "encodeChannels"
 
   override def desc: String =
     "Encodes channels using plain assignment. Encodes channel invariants using exhale/inhale."
 
-  case class AssertFailedToChannelInvariantNotEstablished(comm: Communicate[_])
-      extends Blame[AssertFailed] {
-    override def blame(error: AssertFailed): Unit =
-      comm.blame.blame(ChannelInvariantNotEstablished(error.failure, comm))
-  }
-
   case class ExhaleFailedToChannelInvariantNotEstablished(comm: Communicate[_])
       extends Blame[ExhaleFailed] {
     override def blame(error: ExhaleFailed): Unit =
-      comm.blame
-        .blame(ChannelInvariantNotEstablishedLocally(error.failure, comm))
+      comm.blame.blame(ChannelInvariantNotEstablished(error.failure, comm))
   }
 }
 
 case class EncodeChannels[Pre <: Generation]()
     extends Rewriter[Pre] with LazyLogging with VeymontContext[Pre] {
   val msgSucc = SuccessionMap[Communicate[Pre], Variable[Post]]()
-  val includeChorExpr = ScopedStack[Boolean]()
   val substitutions = ScopedStack[Map[Expr[Pre], Expr[Post]]]()
 
   override def dispatch(p: Program[Pre]): Program[Post] = {
@@ -61,24 +50,23 @@ case class EncodeChannels[Pre <: Generation]()
         val m = new Variable(dispatch(comm.msg.t))(comm.o.where(name = "m"))
         msgSucc(comm) = m
 
+        // Helper for rewriting the invariant. Regular expressions we wrap in the EndpointExpr of the sender/receiver
+        // ChorExpr's we leave untouched. Those will be encoded by the EncodeStratifiedPermissions pass.
+        def wrapEndpointExpr(expr: Expr[Pre], ep: Endpoint[Pre]): Expr[Post] =
+          foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map {
+            case e: ChorExpr[Pre] => dispatch(e)
+            case e => EndpointExpr(succ(ep), dispatch(e))
+          })
+
         Scope(
           Seq(m),
           Block(Seq(
             assignLocal(
               m.get,
               EndpointExpr[Post](succ(sender), dispatch(comm.msg)),
             ),
-            Assert(currentEndpoint.having(comm.sender.get.decl) {
-              includeChorExpr.having(true) {
-                EndpointExpr[Post](succ(sender), dispatch(comm.invariant))
-              }
-            })(AssertFailedToChannelInvariantNotEstablished(comm)),
             Exhale(currentEndpoint.having(comm.sender.get.decl) {
-              includeChorExpr.having(false) {
-                foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map { e =>
-                  EndpointExpr[Post](succ(sender), dispatch(e))
-                })
-              }
+              wrapEndpointExpr(comm.invariant, sender)
             })(ExhaleFailedToChannelInvariantNotEstablished(comm)),
             EndpointStatement[Post](
               Some(succ(receiver)),
@@ -89,14 +77,7 @@ case class EncodeChannels[Pre <: Generation]()
             Inhale(currentEndpoint.having(comm.receiver.get.decl) {
               substitutions.having(Map.from(Seq(
                 (Message(new DirectRef(comm)), dispatch(comm.target))
-              ))) {
-                includeChorExpr.having(true) {
-                  foldAny(comm.invariant.t)(unfoldStar(comm.invariant).map {
-                    case e: ChorExpr[Pre] => e.rewriteDefault()
-                    case e => EndpointExpr[Post](succ(receiver), dispatch(e))
-                  })
-                }
-              }
+              ))) { wrapEndpointExpr(comm.invariant, receiver) }
             }),
           )),
         )
@@ -109,25 +90,14 @@ case class EncodeChannels[Pre <: Generation]()
         substitutions.top(e)
       case InEndpoint(_, endpoint, Perm(loc, perm)) =>
         ChorPerm[Post](succ(endpoint), dispatch(loc), dispatch(perm))(expr.o)
-      case InEndpoint(_, endpoint, cp: ChorPerm[Pre]) => assert(false); ???
+      case InEndpoint(_, _, _: ChorPerm[Pre]) =>
+        assert(false);
+        ??? // TODO (RR): This is an error, remove when getting rid of ChorPerm as well
       case Message(Ref(comm)) => Local[Post](msgSucc.ref(comm))(comm.o)
       case Sender(Ref(comm)) =>
         EndpointName[Post](succ(comm.sender.get.decl))(expr.o)
       case Receiver(Ref(comm)) =>
         EndpointName[Post](succ(comm.receiver.get.decl))(expr.o)
-      case chor: ChorExpr[Pre] if includeChorExpr.topOption.contains(true) =>
-        // Case chor must be kept: include the expression. The top level invariant rewrite will wrap
-        // it into a proper EndpointExpr, hence, remove the \chor layer
-        chor.expr.rewriteDefault()
-      case chor: ChorExpr[Pre] if includeChorExpr.topOption.contains(false) =>
-        // Case chor must not be kept: exhaling the invariant. Since the validity of the invariant, including
-        // the chor part, is already established, it doesn't need to be included when exhaling
-        BooleanValue(true)(chor.o)
-      case chor: ChorExpr[Pre] =>
-        // Case no boolean in includeChor: just rewrite the expression plainly and keep the chor expr
-        // This also happens to be the case we need for the inhale case, where we just want the plain \chor expr
-        // Such that all the necessary wrapped perms will be unwrapped by the EncodePermissionStratification phase
-        chor.rewriteDefault()
       case _ => expr.rewriteDefault()
     }
 }

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

@@ -50,18 +50,6 @@ object EncodePermissionStratification extends RewriterBuilderArg[Boolean] {
   }
 }
 
-/* At the time of writing, under the heavy-weight stratified permissions model, supporting \chor is an enormous hack.
-   It currently consists of 3 parts:
-   - Making \chor work when generating permissions in plain asserts, loop invariants, contracts
-     This is done using the simplifying assumption that, when generating permissions, each field is completely and transitively
-     owned by the anchor (either a local or a method argument). Then chor just transitively unfolds all fields of all anchors
-     in scope. Inside this unfolded expression, plain functions (meaning, with non-specialized contracts), are used.
-   - Making \chor work when not generating permissions in plain asserts, ...
-     Here, we rely on the user to add (\endpoint e; ...) annotations inside \chor.
-   - Making \chor work in channel invariants
-     This is also quite annoying. Because the heavyweight approach does not allow easy peeking into wrapped permissions,
-     we implement an incomplete approach in EncodeChannels.scala.
- */
 case class EncodePermissionStratification[Pre <: Generation](
     generatePermissions: Boolean
 ) extends Rewriter[Pre] with VeymontContext[Pre] with LazyLogging {
@@ -370,80 +358,22 @@ case class EncodePermissionStratification[Pre <: Generation](
           }
         }
 
-      case InEndpoint(_, endpoint, deref @ Deref(obj, Ref(field))) =>
+      case InEndpoint(_, _, deref @ Deref(obj, Ref(field))) =>
         implicit val o = expr.o
         functionInvocation(
           ref = readFunction(obj, field)(expr.o),
           args = Seq(specializing.top, dispatch(obj)),
           blame = ForwardInvocationFailureToDeref(deref),
         )
 
-      case ChorExpr(inner) if generatePermissions =>
-        implicit val o = expr.o
-
-        def predicates(
-            seenClasses: Set[TClass[Pre]],
-            endpoint: Endpoint[Pre],
-            baseT: TClass[Pre],
-            base: Expr[Post],
-        ): Seq[FoldTarget[Post]] = {
-          val cls = baseT.cls.decl
-          // Permission generation makes sure no cycles exist at this point by crashing, but lets make sure anyway
-          assert(!seenClasses.contains(baseT))
-          val newSeenClasses = seenClasses.incl(baseT)
-          val predicatesForClass = cls.fields.map { field =>
-            ScaledPredicateApply(
-              PredicateApply[Post](
-                wrapperPredicate(baseT, field),
-                Seq(EndpointName(succ(endpoint)), base),
-              ),
-              WritePerm(),
-            )
-          }
-          predicatesForClass ++
-            (cls.fields.filter { _.t.asClass.nonEmpty }.flatMap { field =>
-              val newBase =
-                Deref[Post](base, succ(field))(PanicBlame(
-                  "Permissions were unfolded earlier"
-                ))
-              predicates(
-                newSeenClasses,
-                endpoint,
-                baseT.instantiate(field.t).asClass.get,
-                newBase,
-              )
-            })
-        }
-
-        val newInner = inChor.having(true) { dispatch(inner) }
-
-        InferEndpointContexts.getEndpoints(inner).flatMap { endpoint =>
-          predicates(
-            HashSet(),
-            endpoint,
-            endpoint.t,
-            EndpointName[Post](succ(endpoint)),
-          )
-        }.foldRight[Expr[Post]](newInner) { case (app, inner) =>
-          Unfolding[Post](app, inner)(PanicBlame(
-            "Generating permissions guarantee permissions are in scope"
-          ))
-        }
-
-      case ChorExpr(inner) if !generatePermissions =>
-        // If not generating permissions, we rely on endpoint expressions to indicate the owner
-        // of relevant permissions
-        inChor.having(true) { dispatch(inner) }
+      case ChorExpr(inner) => inChor.having(true) { dispatch(inner) }
 
       // Generate an invocation to the unspecialized function version if we're inside a \chor
-      // This is safe because \chor unfold all predicates of all endpoints that occur within the expression...
-      // ... in the case of permission generation. Otherwise it just does nothing...?
       // The natural successor of the function will be the unspecialized one
-      case inv: FunctionInvocation[Pre]
-          if inChor.topOption.contains(true) && generatePermissions =>
+      case inv: FunctionInvocation[Pre] if inChor.topOption.contains(true) =>
         inv.rewriteDefault()
       case inv: InstanceFunctionInvocation[Pre]
-          if inChor.topOption.contains(true) && generatePermissions =>
+          if inChor.topOption.contains(true) =>
         inv.rewriteDefault()
 
       case InEndpoint(_, endpoint, inv: FunctionInvocation[Pre]) =>