Encoding quantified wands using MWSFs

src/main/scala/rules/Brancher.scala

@@ -50,10 +50,11 @@ object brancher extends BranchingRules {
      *   (1) the branching is due to the short-circuiting evaluation of a conjunction
      *   (2) the branch condition contains a quantified variable
      */
+    val allQuantifiedVariables = s.quantifiedVariables ++ s.packagingWandSnapshots
     val skipPathFeasibilityCheck = (
          fromShortCircuitingAnd
-      || (   s.quantifiedVariables.nonEmpty
-          && s.quantifiedVariables.map(_._1).exists(condition.freeVariables.contains))
+      || (   allQuantifiedVariables.nonEmpty
+          && allQuantifiedVariables.map(_._1).exists(condition.freeVariables.contains))
     )
 
     /* True if the then-branch is to be explored */

src/main/scala/rules/Executor.scala

@@ -597,11 +597,7 @@ object executor extends ExecutionRules {
               }
             assert(s2.reserveHeaps.length == s.reserveHeaps.length)
 
-            val s3 = chWand match {
-              case ch: QuantifiedMagicWandChunk =>
-                v1.heapSupporter.triggerResourceIfNeeded(s2, wand, ch.singletonArgs.get, ch.singletonArgExps, v1)
-              case _ => s2
-            }
+            val s3 = v1.heapSupporter.triggerWandIfNeeded(s2, wand, chWand, v1)
 
             continuation(s3.copy(isInPackage = s.isInPackage), v1)
           })

src/main/scala/rules/HeapSupporter.scala

@@ -10,7 +10,7 @@ import viper.silicon
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.debugger.DebugExp
 import viper.silicon.interfaces.VerificationResult
-import viper.silicon.interfaces.state.{ChunkIdentifer, NonQuantifiedChunk}
+import viper.silicon.interfaces.state.{Chunk, ChunkIdentifer, NonQuantifiedChunk}
 import viper.silicon.resources.{FieldID, PredicateID}
 import viper.silicon.rules.havocSupporter.{HavocHelperData, HavocOneData, HavocallData}
 import viper.silicon.rules.quantifiedChunkSupporter.freshSnapshotMap
@@ -67,6 +67,18 @@ trait HeapSupportRules extends SymbolicExecutionRules {
                               eArgs: Option[Seq[ast.Exp]],
                               v: Verifier): State
 
+  /** Creates the chunk for a (quantified or non-quantified) magic wand with the given snapshot,
+    * returning the chunk plus any ground definitions that should be conserved separately. */
+  def createWandChunk(s: State,
+                      wand: ast.MagicWand,
+                      tArgs: Seq[Term],
+                      eArgs: Option[Seq[ast.Exp]],
+                      snapshot: MagicWandSnapshot,
+                      v: Verifier): (Chunk, Seq[Term], Option[Seq[DebugExp]])
+
+  /** Triggers the wand resource if the produced chunk is a quantified one; a no-op otherwise. */
+  def triggerWandIfNeeded(s: State, wand: ast.MagicWand, chWand: Chunk, v: Verifier): State
+
   def consumeSingle(s: State,
                     h: Heap,
                     resAcc: ast.ResourceAccess,
@@ -438,6 +450,37 @@ class DefaultHeapSupportRules extends HeapSupportRules {
     }
   }
 
+  def createWandChunk(s: State,
+                      wand: ast.MagicWand,
+                      tArgs: Seq[Term],
+                      eArgs: Option[Seq[ast.Exp]],
+                      snapshot: MagicWandSnapshot,
+                      v: Verifier): (Chunk, Seq[Term], Option[Seq[DebugExp]]) = {
+    if (s.isQuantifiedResource(wand)) {
+      val formalVars = s.getFormalArgVars(wand, v)
+      val formalVarExps = Option.when(withExp)(s.getFormalArgDecls(wand))
+      // The singleton snapshot map maps the wand's arguments to its magic wand snap function.
+      val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, wand, tArgs, snapshot.mwsf, v)
+      v.decider.prover.comment("Definitional axioms for singleton-SM's value")
+      val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
+      v.decider.assumeDefinition(smValueDef, debugExp)
+      val chunk = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, tArgs,
+        eArgs, FullPerm, Option.when(withExp)(ast.FullPerm()()), sm, s.program)
+      (chunk, Seq(smValueDef), Option.when(withExp)(Seq(debugExp.get)))
+    } else {
+      val chunk = MagicWandChunk(MagicWandIdentifier(wand, s.program), s.g.values, tArgs, eArgs, snapshot, FullPerm,
+        Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)))
+      (chunk, Seq.empty[Term], Option.when(withExp)(Seq.empty[DebugExp]))
+    }
+  }
+
+  def triggerWandIfNeeded(s: State, wand: ast.MagicWand, chWand: Chunk, v: Verifier): State =
+    chWand match {
+      case ch: QuantifiedMagicWandChunk =>
+        triggerResourceIfNeeded(s, wand, ch.singletonArgs.get, ch.singletonArgExps, v)
+      case _ => s
+    }
+
   def produceSingle(s: State,
                     resource: ast.Resource,
                     tArgs: Seq[Term],
@@ -545,7 +588,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
       case p: ast.Predicate =>
         sf(sorts.PredicateSnapFunction(s.predicateSnapMap(p.name), p.name), v)
       case _: ast.MagicWand =>
-        sf(sorts.PredicateSnapFunction(sorts.Snap, qid), v)
+        sf(sorts.PredicateSnapFunction(sorts.MagicWandSnapFunction, qid), v)
     }
 
     quantifiedChunkSupporter.produce(

src/main/scala/rules/MagicWandSupporter.scala

@@ -176,7 +176,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
                * and thus be unsound. Since fractional wands do not exist it is not necessary to equate their
                * snapshots. Also have a look at the comments in the packageWand and applyWand methods.
                */
-              case (Some(_: MagicWandChunk), Some(_: MagicWandChunk)) => True
+              case (Some(_: MagicWandChunk | _: QuantifiedMagicWandChunk), Some(_: MagicWandChunk | _: QuantifiedMagicWandChunk)) => True
               case (Some(ch1: NonQuantifiedChunk), Some(ch2: NonQuantifiedChunk)) => ch1.snap === ch2.snap
               case (Some(ch1: QuantifiedBasicChunk), Some(ch2: QuantifiedBasicChunk)) => ch1.snapshotMap === ch2.snapshotMap
               case _ => True
@@ -314,41 +314,30 @@ object magicWandSupporter extends SymbolicExecutionRules {
       val bodyVars = wand.subexpressionsToEvaluate(s.program)
 
       evals(s, bodyVars, _ => pve, v)((s2, tArgs, eArgsNew, v2) => {
-        // Currently, the snapshot of a wand differs depending on whether it is a quantified magic wand or not.
-        // Therefore, we have to keep the case distinction here and cannot leave everything but the chunk creation
-        // to the HeapSupporter.
-        val (s3, ch, tPcs, ePcs, v3 ) = if (s2.qpMagicWands.contains(MagicWandIdentifier(wand, s2.program))) {
-          val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
-          val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
-          val snapshotTerm = Combine(freshSnapRoot, snapRhs)
-          val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s2, wand, tArgs, snapshotTerm, v2)
-          v2.decider.prover.comment("Definitional axioms for singleton-SM's value")
-          val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
-          v2.decider.assumeDefinition(smValueDef, debugExp)
-          val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, tArgs,
-            eArgsNew, FullPerm, Option.when(withExp)(ast.FullPerm()()), sm, s.program)
-          val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly
-          (s2, ch, conservedPcs.flatMap(_.conditionalized), Option.when(withExp)(conservedPcs.flatMap(_.conditionalizedExp)), v2)
-        } else {
-          val ch = MagicWandChunk(MagicWandIdentifier(wand, s.program), s2.g.values, tArgs, eArgsNew, wandSnapshot, FullPerm,
-            Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)))
-          val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly
-          // Partition path conditions into a set which include the freshSnapRoot and those which do not
-          val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(pcs => pcs.conditionalized).partition(_.contains(freshSnapRoot))
-          val pcsWithoutExp = Option.when(withExp)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), freshSnapRoot))
-          // For all path conditions which include the freshSnapRoot, add those as part of the definition of the MWSF in the same forall quantifier
-          val pcsQuantified = Forall(
-            freshSnapRoot,
-            And(pcsWithFreshSnapRoot.map {
-              // Remove forall quantifiers with the same quantified variable
-              case Quantification(Forall, v :: Nil, body: Term, _, _, _, _) if v == freshSnapRoot => body
-              case p => p
-            }),
-            Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)),
-          )
-          (s2, ch, pcsQuantified +: pcsWithoutFreshSnapRoot, Option.when(withExp)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: pcsWithoutExp.get), v2)
-        }
-        appendToResults(s3, ch, v3.decider.pcs.after(preMark), (tPcs, ePcs), v3)
+        // Partition the conserved PCs here, before any definitions about the new wand chunks are assumed below, so that
+        // the ground value def is not bundled into (and trapped inside) the freshSnapRoot quantifier.
+        val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly
+
+        val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(pcs => pcs.conditionalized).partition(_.contains(freshSnapRoot))
+        val pcsWithoutExp = Option.when(withExp)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), freshSnapRoot))
+        // For all path conditions which include the freshSnapRoot, add those as part of the definition of the MWSF in the same forall quantifier
+        val pcsQuantified = Forall(
+          freshSnapRoot,
+          And(pcsWithFreshSnapRoot.map {
+            // Remove forall quantifiers with the same quantified variable
+            case Quantification(Forall, v :: Nil, body: Term, _, _, _, _) if v == freshSnapRoot => body
+            case p => p
+          }),
+          Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)),
+        )
+
+        val (ch, groundPcs, groundPcsExp) = v2.heapSupporter.createWandChunk(s2, wand, tArgs, eArgsNew, wandSnapshot, v2)
+
+        val tPcs = (pcsQuantified +: pcsWithoutFreshSnapRoot) ++ groundPcs
+        val ePcs = Option.when(withExp)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: (pcsWithoutExp.get ++ groundPcsExp.get))
+
+        val s3 = s2.copy(packagingWandSnapshots = s2.packagingWandSnapshots.filterNot(_._1 == freshSnapRoot))
+        appendToResults(s3, ch, v2.decider.pcs.after(preMark), (tPcs, ePcs), v2)
         Success()
       })
     }
@@ -362,8 +351,13 @@ object magicWandSupporter extends SymbolicExecutionRules {
        */
       val freshSnapRoot = freshSnap(sorts.Snap, v1)
 
+      // Record the abstract LHS snapshot so that new declarations created while packaging are parameterized by it
+      // (see State.packagingWandSnapshots); each apply of the resulting wand then gets its own LHS snapshot.
+      val freshSnapshotRootVar = Option.when(withExp)(ast.LocalVar("LHS", ast.InternalType)())
+      val s1WithSnapRoot = s1.copy(packagingWandSnapshots = (freshSnapRoot, freshSnapshotRootVar) +: s1.packagingWandSnapshots)
+
       // Produce the wand's LHS.
-      produce(s1.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => {
+      produce(s1WithSnapRoot.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => {
         val proofScriptCfg = proofScript.toCfg()
         val emptyHeap = v2.heapSupporter.getEmptyHeap(sLhs.program)
 
@@ -472,14 +466,12 @@ object magicWandSupporter extends SymbolicExecutionRules {
         // Create copy of the state with a new labelled heap (i.e. `oldHeaps`) called "lhs".
         val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> this.getEvalHeap(s1)))
 
-        // If the snapWand is a (wrapped) MagicWandSnapshot then lookup the snapshot of the right-hand side by applying snapLhs.
+        // Look up the RHS snapshot by applying snapLhs to the wand's MWSF (a (wrapped)
+        // MagicWandSnapshot for an individual wand, or an MWSF-sorted lookup for a quantified one).
         val magicWandSnapshotLookup = snapWand.get match {
           case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs.get)
           case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs.get)
-          // Fallback solution for quantified magic wands
-          case predicateLookup: PredicateLookup =>
-            v2.decider.assume(snapLhs.get === First(snapWand.get), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot", true)))
-            Second(predicateLookup)
+          case t if t.sort == sorts.MagicWandSnapFunction => MWSFLookup(t, snapLhs.get)
           case _ => snapWand.get
         }
 

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -130,7 +130,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                 case Some(v) =>
                   ReusedSummarisingSnapshot(v)
                 case None =>
-                  val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1) ++ s.quantifiedVariables.map(_._1))
+                  val ss = v.decider.appliedFresh("ss", sort, s.functionRecorderQuantifiedVariables().map(_._1) ++ s.packagingWandSnapshots.map(_._1) ++ s.quantifiedVariables.map(_._1))
                   FreshSummarisingSnapshot(ss)
               }
           }
@@ -327,7 +327,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           definiteAlias.contains(ch1) || !definiteAlias.contains(ch2) && ch1.args == args
         }
 
-        val additionalArgs = s.relevantQuantifiedVariables.map(_._1)
+        // Permission maps deliberately exclude packagingWandSnapshots (would break permission matching after a package).
+        val additionalArgs = (s.functionRecorderQuantifiedVariables() ++ s.quantifiedVariables).map(_._1)
         var currentFunctionRecorder = s.functionRecorder
 
         relevantChunks.sortWith(sortFunction) foreach { ch =>

src/main/scala/rules/QuantifiedChunkSupport.scala

@@ -501,7 +501,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     // TODO: Consider if axioms can be simplified in case codomainQVars is empty
 
     val snapshotMaps = relevantChunks.map(_.snapshotMap)
-    val relevantQvars = s.quantifiedVariables.map(_._1).filter(qvar =>
+    // packagingWandSnapshots are always relevant; regular quantified variables only if they occur.
+    val relevantQvars = s.packagingWandSnapshots.map(_._1) ++ s.quantifiedVariables.map(_._1).filter(qvar =>
       snapshotMaps.exists(sm => sm.contains(qvar)) || optSmDomainDefinitionCondition.exists(_.contains(qvar)))
     val additionalFvfArgs = s.functionRecorderQuantifiedVariables().map(_._1) ++ relevantQvars
     val sm = freshSnapshotMap(s, resource, additionalFvfArgs, v)
@@ -668,7 +669,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                            v: Verifier)
                           : (Term, Term) = {
 
-    val additionalSmArgs = s.relevantQuantifiedVariables(arguments).map(_._1)
+    val additionalSmArgs = s.packagingWandSnapshots.map(_._1) ++ s.relevantQuantifiedVariables(arguments).map(_._1)
     val sm = freshSnapshotMap(s, resource, additionalSmArgs, v)
     val smValueDef = BuiltinEquals(ResourceLookup(resource, sm, arguments, s.program), value)
 
@@ -1421,7 +1422,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       })((s4, optCh, v2) =>
         optCh match {
           case Some(ch) if returnSnap =>
-            val snap = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program).convert(sorts.Snap)
+            val lookup = ResourceLookup(resource, ch.snapshotMap, arguments, s4.program)
+            // For magic wands the lookup is already the MWSF (applied directly by applyWand).
+            val snap = if (resource.isInstanceOf[ast.MagicWand]) lookup else lookup.convert(sorts.Snap)
             Q(s4, s4.h, Some(snap), v2)
           case None if returnSnap =>
             Q(s4, s4.h, Some(freshSnap(sorts.Snap, v2)), v2)
@@ -1461,7 +1464,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                 v = v)
             val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1),
               smCache = smCache1)
-            val snap = ResourceLookup(resource, smDef1.sm, arguments, s2.program).convert(sorts.Snap)
+            val lookup = ResourceLookup(resource, smDef1.sm, arguments, s2.program)
+            // For magic wands the lookup is already the MWSF (applied directly by applyWand).
+            val snap = if (resource.isInstanceOf[ast.MagicWand]) lookup else lookup.convert(sorts.Snap)
             Q(s2, h1, Some(snap), v)
           } else {
             Q(s1, h1, None, v)
@@ -1551,7 +1556,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     v.decider.prover.comment("Precomputing data for removing quantified permissions")
 
-    val additionalArgs = s.relevantQuantifiedVariables.map(_._1)
+    val additionalArgs = (s.packagingWandSnapshots ++ s.functionRecorderQuantifiedVariables() ++ s.quantifiedVariables).map(_._1)
     var currentFunctionRecorder = s.functionRecorder
 
     val precomputedData = candidates map { ch =>
@@ -1743,7 +1748,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           // TODO: Reconsider use of and general design behind s.predicateSnapMap
           sorts.PredicateSnapFunction(s.predicateSnapMap(predicate.name), predicate.name)
         case w: ast.MagicWand =>
-          sorts.PredicateSnapFunction(sorts.Snap, MagicWandIdentifier(w, s.program).toString)
+          sorts.PredicateSnapFunction(sorts.MagicWandSnapFunction, MagicWandIdentifier(w, s.program).toString)
         case _ =>
           sys.error(s"Found yet unsupported resource $resource (${resource.getClass.getSimpleName})")
       }

src/main/scala/state/Chunks.scala

@@ -199,7 +199,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
                                     hints: Seq[Term] = Nil)
     extends QuantifiedBasicChunk {
 
-  require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.Snap, s"Quantified magic wand chunk values must be of sort MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
+  require(wsf.sort.isInstanceOf[terms.sorts.PredicateSnapFunction] && wsf.sort.asInstanceOf[terms.sorts.PredicateSnapFunction].codomainSort == sorts.MagicWandSnapFunction, s"Quantified magic wand chunk values must be a PredicateSnapFunction with codomain MagicWandSnapFunction ($wsf), but found ${wsf.sort}")
   require(perm.sort == sorts.Perm, s"Permissions $perm must be of sort Perm, but found ${perm.sort}")
 
   override val resourceID = MagicWandID