Reach the choreography encoding pass

utwente-fmt · Dec 20, 2024 · 661c2fc · 661c2fc
1 parent 76969dc
commit 661c2fc
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 11 deletions.
diff --git a/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala b/src/rewrite/vct/rewrite/veymont/StratifyUnpointedExpressions.scala
@@ -111,7 +111,7 @@ case class StratifyUnpointedExpressions[Pre <: Generation]()
 
   def stratifyExpr(expr: Expr[Pre]): Expr[Post] = {
     implicit val o = expr.o
-    foldAny1(expr.t)(unfoldAny(expr).flatMap {
+    foldAny(expr.t)(unfoldStar(expr).flatMap {
       case expr @ (_: EndpointExpr[Pre] | _: ChorExpr[Pre]) =>
         Seq(expr.rewriteDefault())
       case expr =>
@@ -120,6 +120,6 @@ case class StratifyUnpointedExpressions[Pre <: Generation]()
             EndpointExpr[Post](dispatch(commTarget), dispatch(expr))
           }
         }.toSeq
-    })
+    }).getOrElse(tt)
   }
 }
diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodeChorBranchUnanimity.scala
@@ -114,12 +114,6 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean)
     statement match {
       case InChor(_, c @ ChorStatement(branch: Branch[Pre])) =>
         implicit val o = statement.o
-//        val assertions = Block(
-//          unanimous(branch.cond).map { case (cond, (alpha, beta)) =>
-//            Assert(cond)(ForwardBranchUnanimity(c, alpha, beta))
-//          }
-//        )
-//        Block(Seq(assertions, super.dispatch(branch)))
         Block(Seq(
           Assert(unanimous(branch.cond))(
             ForwardBranchUnanimity(c, branch.cond)
@@ -227,7 +221,7 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean)
         // Evaluate if j is within range. Since j should be a mathematically expression (no method calls &
         // no heap dereferences) it's safe to duplicate it all over the place. Though it might be bad for prover performance.
         // We don't check for this constraint, though.
-        (dispatch(low) <= dispatch(j)) && (dispatch(j) < dispatch(high)) ==>
+        ((dispatch(low) <= dispatch(j)) && (dispatch(j) < dispatch(high))) ==>
           substitutions.having(substitutions.top.updated(v.get, dispatch(j))) {
             dispatch(inner)
           }
@@ -255,13 +249,12 @@ case class EncodeChorBranchUnanimity[Pre <: Generation](enabled: Boolean)
       case r @ (_: CommTargetEndpoint[Pre] | _: CommTargetIndex[Pre]) =>
         partialProject(expr, r) |===| b
       case CommTargetRange(f, RangeBinder(oldV, low, high)) =>
-//        oldV.drop()
         variables.scope(forall(
           TInt(),
           v => {
             variables.succeedOnly(oldV, v.ref.decl)
             ((dispatch(low) <= v) && (v < dispatch(high))) ==>
-              partialProject(expr, CommTargetIndex(f, oldV.get))
+              partialProject(expr, CommTargetIndex(f, oldV.get)) |===| b
           },
         ))
 

diff --git a/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala b/src/rewrite/vct/rewrite/veymont/verification/EncodePermissionStratification.scala
@@ -560,6 +560,29 @@ case class EncodePermissionStratification[Pre <: Generation](
           dispatch(inner)
         }
 
+      case EndpointExpr(target: CommTargetIndex[Pre], inner) =>
+        specializing.having(CtExpr(target.rewrite())(target.o)) {
+          dispatch(inner)
+        }
+
+      case EndpointExpr(
+            target @ CommTargetRange(ref, RangeBinder(v, low, high)),
+            inner,
+          ) =>
+        implicit val o: Origin = target.o
+        forall(
+          TInt(),
+          i => {
+            // TODO (RR): `i` should have origin of `v` here...!
+            variables.succeedOnly(v, i.ref.decl)
+            ((dispatch(low) <= i) && (i < dispatch(high))) ==>
+              specializing
+                .having(CtExpr(CommTargetIndex(endpoints.dispatch(ref), i))) {
+                  dispatch(inner)
+                }
+          },
+        )
+
       case EndpointExpr(_, inner) => ???
 
       case deref @ Deref(obj, Ref(field)) if specializing.nonEmpty =>