Finish cherry-picking Asserting/Assuming changes from Bob's branch

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

@@ -1545,6 +1545,9 @@ object NonNullPointerNull
 object UnsafeDontCare {
   case class Satisfiability(reason: String)
       extends UnsafeDontCare[NontrivialUnsatisfiable]
+  case class Contract(reason: String) extends UnsafeDontCare[ContractedFailure]
+  case class Invocation(reason: String)
+      extends UnsafeDontCare[InvocationFailure]
 }
 
 trait UnsafeDontCare[T <: VerificationFailure]

src/hre/hre/io/ChecksumReadableFile.scala

@@ -18,7 +18,7 @@ case class ChecksumReadableFile(
     checksumKind: String,
 ) extends InMemoryCachedReadable {
   override def underlyingPath: Option[Path] = Some(file)
-  override def fileName: String = file.toString
+  override def fileName: String = file.getFileName.toString
   override def isRereadable: Boolean = true
   private var checksumCache: Option[String] = None
 

src/hre/hre/io/RWFile.scala

@@ -7,7 +7,7 @@ import java.nio.file.{Files, Path}
 case class RWFile(file: Path, doWatch: Boolean = true)
     extends InMemoryCachedReadable with Writeable {
   override def underlyingPath: Option[Path] = Some(file)
-  override def fileName: String = file.toString
+  override def fileName: String = file.getFileName.toString
   override def isRereadable: Boolean = true
 
   override protected def getWriter: Writer = {

src/main/vct/main/stages/Transformation.scala

@@ -34,7 +34,7 @@ import vct.rewrite.{
   EncodeByValueClassUsage,
   EncodeRange,
   EncodeResourceValues,
-  EncodeAssertingAssuming,
+  EncodeAssuming,
   ExplicitResourceValues,
   GenerateSingleOwnerPermissions,
   HeapVariableToRef,
@@ -414,7 +414,7 @@ case class SilverTransformation(
         RefuteToInvertedAssert,
         ExplicitResourceValues,
         EncodeResourceValues,
-        EncodeAssertingAssuming,
+        EncodeAssuming,
 
         // Encode parallel blocks
         EncodeSendRecv,

src/main/vct/options/types/PathOrStd.scala

@@ -15,7 +15,7 @@ sealed trait PathOrStd extends InMemoryCachedReadable with Writeable {
 
   override def fileName: String =
     this match {
-      case PathOrStd.Path(path) => path.toString
+      case PathOrStd.Path(path) => path.getFileName.toString
       case PathOrStd.StdInOrOut => "<stdio>"
     }
 

src/rewrite/vct/rewrite/EncodeAssuming.scala

@@ -0,0 +1,56 @@
+package vct.rewrite
+
+import com.typesafe.scalalogging.LazyLogging
+import vct.col.ast.{
+  Assuming,
+  Expr,
+  Function,
+  Let,
+  TBool,
+  UnitAccountedPredicate,
+  Variable,
+}
+import vct.col.origin.{DiagnosticOrigin, UnsafeDontCare}
+import vct.col.rewrite.{Generation, Rewriter, RewriterBuilder}
+
+import vct.col.util.AstBuildHelpers._
+
+case object EncodeAssuming extends RewriterBuilder {
+  override def key: String = "encodeAssumeExpr"
+  override def desc: String = "Encodes assume exprs using plain pure functions"
+}
+
+case class EncodeAssuming[Pre <: Generation]()
+    extends Rewriter[Pre] with LazyLogging {
+
+  lazy val assumingFunction: Function[Post] = {
+    implicit val o = DiagnosticOrigin
+    val assnVar = new Variable[Post](TBool())(o.where(name = "assn"))
+    globalDeclarations.declare(
+      function(
+        blame = UnsafeDontCare.Contract("assumption primitive"),
+        contractBlame = UnsafeDontCare.Satisfiability("assumption primitive"),
+        returnType = TBool(),
+        args = Seq(assnVar),
+        ensures = UnitAccountedPredicate(assnVar.get),
+      )(o.where(name = "assume_"))
+    )
+  }
+
+  override def dispatch(expr: Expr[Pre]): Expr[Post] =
+    expr match {
+      case Assuming(assn, inner) =>
+        implicit val o = expr.o
+        Let(
+          new Variable(TBool())(o.where(name = "_")),
+          functionInvocation(
+            ref = assumingFunction.ref,
+            args = Seq(dispatch(assn)),
+            blame = UnsafeDontCare.Invocation("assumption"),
+          ),
+          dispatch(inner),
+        )
+
+      case _ => expr.rewriteDefault()
+    }
+}