Magic wand

col/src/main/java/vct/col/ast/Node.scala

@@ -166,9 +166,7 @@ final case class Unlock[G](obj: Expr[G])(val blame: Blame[UnlockFailure])(implic
 final case class Commit[G](obj: Expr[G])(val blame: Blame[CommitFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with CommitImpl[G]
 final case class Fold[G](res: Expr[G])(val blame: Blame[FoldFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FoldImpl[G]
 final case class Unfold[G](res: Expr[G])(val blame: Blame[UnfoldFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with UnfoldImpl[G]
-final case class WandQed[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandQedImpl[G]
-final case class WandApply[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandApplyImpl[G]
-final case class WandUse[G](res: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandUseImpl[G]
+final case class WandApply[G](res: Expr[G])(val blame: Blame[WandApplyFailed])(implicit val o: Origin) extends NormallyCompletingStatement[G] with WandApplyImpl[G]
 final case class Havoc[G](loc: Expr[G])(implicit val o: Origin) extends NormallyCompletingStatement[G] with HavocImpl[G]
 final case class FramedProof[G](pre: Expr[G], body: Statement[G], post: Expr[G])(val blame: Blame[FramedProofFailure])(implicit val o: Origin) extends NormallyCompletingStatement[G] with FramedProofImpl[G]
 
@@ -196,7 +194,7 @@ final case class ParAtomic[G](inv: Seq[Ref[G, ParInvariantDecl[G]]], content: St
 final case class ParBarrier[G](block: Ref[G, ParBlockDecl[G]], invs: Seq[Ref[G, ParInvariantDecl[G]]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(val blame: Blame[ParBarrierFailed])(implicit val o: Origin) extends CompositeStatement[G] with ParBarrierImpl[G]
 final case class ParStatement[G](impl: ParRegion[G])(implicit val o: Origin) extends CompositeStatement[G] with ParStatementImpl[G]
 final case class VecBlock[G](iters: Seq[IterVariable[G]], requires: Expr[G], ensures: Expr[G], content: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with VecBlockImpl[G]
-final case class WandCreate[G](statements: Seq[Statement[G]])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G]
+final case class WandPackage[G](res: Expr[G], proof: Statement[G])(val blame: Blame[PackageFailure])(implicit val o: Origin) extends CompositeStatement[G] with WandCreateImpl[G]
 final case class ModelDo[G](model: Expr[G], perm: Expr[G], after: Expr[G], action: Expr[G], impl: Statement[G])(implicit val o: Origin) extends CompositeStatement[G] with ModelDoImpl[G]
 
 sealed abstract class Declaration[G] extends Node[G] with DeclarationImpl[G] {

col/src/main/java/vct/col/ast/temporaryimplpackage/statement/composite/WandCreateImpl.scala

@@ -1,7 +1,7 @@
 package vct.col.ast.temporaryimplpackage.statement.composite
 
-import vct.col.ast.WandCreate
+import vct.col.ast.WandPackage
 
-trait WandCreateImpl[G] { this: WandCreate[G] =>
+trait WandCreateImpl[G] { this: WandPackage[G] =>
 
 }

col/src/main/java/vct/col/coerce/CoercingRewriter.scala

@@ -1176,10 +1176,8 @@ abstract class CoercingRewriter[Pre <: Generation]() extends Rewriter[Pre] with
       case u @ Unlock(obj) => Unlock(cls(obj)._1)(u.blame)
       case VecBlock(iters, requires, ensures, content) => VecBlock(iters, res(requires), res(ensures), content)
       case w @ Wait(obj) => Wait(cls(obj)._1)(w.blame)
-      case WandApply(assn) => WandApply(res(assn))
-      case WandCreate(statements) => WandCreate(statements)
-      case WandQed(assn) => WandQed(res(assn))
-      case WandUse(assn) => WandUse(res(assn))
+      case w @ WandApply(assn) => WandApply(res(assn))(w.blame)
+      case w @ WandPackage(expr, stat) => WandPackage(res(expr), stat)(w.blame)
     }
   }
 

col/src/main/java/vct/col/feature/FeatureRainbow.scala

@@ -309,10 +309,8 @@ class FeatureRainbow[G] {
     case node: Unlock[G] => IntrinsicLocks
     case node: Fold[G] => return Nil
     case node: Unfold[G] => return Nil
-    case node: WandCreate[G] => MagicWand
-    case node: WandQed[G] => MagicWand
+    case node: WandPackage[G] => MagicWand
     case node: WandApply[G] => MagicWand
-    case node: WandUse[G] => MagicWand
     case node: ModelDo[G] => Models
     case node: Havoc[G] => return Nil
     case node: Break[G] => ExceptionalLoopControl

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

@@ -147,6 +147,22 @@ case class FoldFailed(failure: ContractFailure, node: Fold[_]) extends WithContr
   override def descInContext: String = "Fold may fail, since"
   override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure."
 }
+trait PackageFailure extends VerificationFailure
+case class PackageThrows(node: WandPackage[_]) extends PackageFailure with NodeVerificationFailure {
+  override def code: String = "packageThrows"
+  override def descInContext: String = "Package proof may throw an exception"
+  override def inlineDescWithSource(source: String): String = s"`$node` may throw an exception."
+}
+case class PackageFailed(failure: ContractFailure, node: WandPackage[_]) extends PackageFailure with WithContractFailure {
+  override def baseCode: String = "packageFailed"
+  override def descInContext: String = "Package statement may fail, since"
+  override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure."
+}
+case class WandApplyFailed(failure: ContractFailure, node: WandApply[_]) extends WithContractFailure {
+  override def baseCode: String = "applyFailed"
+  override def descInContext: String = "Wand apply may fail, since"
+  override def inlineDescWithSource(node: String, failure: String): String = s"`$node` may fail, since $failure."
+}
 case class SendFailed(failure: ContractFailure, node: Send[_]) extends WithContractFailure {
   override def baseCode: String = "sendFailed"
   override def descInContext: String = "Send may fail, since"

col/src/main/java/vct/col/print/Printer.scala

@@ -544,14 +544,10 @@ case class Printer(out: Appendable,
       spec(statement("fold", space, pred))
     case Unfold(pred) =>
       spec(statement("unfold", space, pred))
-    case WandCreate(statements) =>
-      spec(control(phrase("create"), Block(statements)(DiagnosticOrigin)))
-    case WandQed(wand) =>
-      spec(statement("qed", space, wand))
+    case WandPackage(expr, state) =>
+      spec(control(phrase("package", expr), state))
     case WandApply(wand) =>
       spec(statement("apply", space, wand))
-    case WandUse(pred) =>
-      spec(statement("use", space, pred))
     case Havoc(loc) =>
       ???
     case Break(label) =>

col/src/main/java/vct/col/resolve/Spec.scala

@@ -238,6 +238,9 @@ case object Spec {
       case TClass(Ref(cls)) => cls.declarations.flatMap(Referrable.from).collectFirst {
         case ref @ RefInstancePredicate(decl) if ref.name == name => decl
       }
+      case JavaTClass(Ref(cls), _) => cls.declarations.flatMap(Referrable.from).collectFirst {
+        case ref @ RefInstancePredicate(decl) if ref.name == name => decl
+      }
       case _ => None
     }