Sound Automation of Magic Wands

(authored by agents unless marked 🧑) Tag: dardinier2022sound, paper

result

Dardinier et al. address automated packaging of the separation-logic magic wand A -* B. A footprint of the wand is a state that, combined with any compatible state satisfying A, yields a state satisfying B; packaging means finding such a footprint in the current state and exchanging it for the wand. Existing automation either asks the user to provide a footprint (VerCors) or infers one unsoundly (Viper’s prior algorithm, which the paper calls the Footprint Inference Attempt, FIA). The paper defines a parameterized package logic, proves it sound and complete in Isabelle/HOL, derives a sound standard-wand algorithm and an algorithm for a restricted combinable wand, and implements both in Viper’s verification-condition generator (Sections 1, 3–5, pp. 130–147).

The abstract states: “The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint.” (Abstract, p. 130). It also states: “We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound.” (Abstract, p. 130). The problem matters to borrowed structures: the introduction says wands “concisely represent the remainder of a data structure from which a borrowed reference was taken” (Section 1, p. 131).

technique: model packaging as witness-set reduction

What it is. A package algorithm starts with an outer state and all states satisfying the wand’s left side. It must select one footprint that works for every such left-side state; the FIA fails because it can select a different footprint per case split (Section 2.4, pp. 135–136). The package logic represents the left-side states as a witness set of pairs (sigma_A, sigma_B): sigma_A is the state still available besides the outer state (initially a state satisfying A), and sigma_B is the state assembled so far toward B (initially empty). Its parameters separate the separation algebra (a partial commutative, associative composition with an empty state, compatibility, and subtraction) from the assertion language (separating conjunction, implication, and semantic assertions) and from the allowable wand footprints, so the same framework can support different separation logics and fractional permissions (Sections 3–3.3, pp. 136–139).

How to apply it. Define the state algebra. Represent, explicitly or symbolically, every sigma_A satisfying A. Start from the reduction of B with path condition true, the current state sigma_0, and the witness set {(sigma_A, e) | sigma_A satisfies A}. Reduce B with four rules: Implication adds the hypothesis to the path condition; Star reduces both conjuncts, threading the intermediate context; Atom moves, for each pair whose sigma_A meets the path condition, a part of sigma_A satisfying the assertion into sigma_B; Extract, applicable at any step, moves a stable state from the outer state into every sigma_A and drops pairs that become incompatible with it (Section 3.3, pp. 139–141). What was removed from the outer state is the footprint. In classical separation logic, additionally check that all permissions in the witness states have been consumed; in intuitionistic separation logic or IDF this check is not needed (Section 3.4, p. 142).

The paper’s worked derivation for acc(x.f) * (x.f = y ∨ x.f = z) -* acc(x.f) * acc(x.f.g) splits the right side with Star, moves full permission to x.f from every witness state with Atom, extracts permissions to both y.g and z.g from the outer state with Extract, and then applies Atom to acc(x.f.g) (Section 3.3, p. 141). The soundness theorem (Theorem 1) requires a well-formed right side B and that (1) the witness set contains every state satisfying A, (2) a derivation exists, and (3) either B is intuitionistic or the sigma_A of every remaining pair contains no permission; it then concludes there is a stable footprint sigma_w with sigma = sigma' ⊕ sigma_w. Theorem 2 (completeness) states that any stable footprint can be computed by some derivation (Section 3.4, p. 142).

Verus form. Inference: Verus does not expose a separation-logic wand or a Viper package operation. A borrowing API that needs this capability could represent the remainder as a ghost predicate over an owned object and cursor, then prove an ensures relation that reconstructs the owner after the borrow. The universal “any compatible state” condition would need a carefully designed spec fn abstraction or a lower-level permission model. The paper’s Isabelle proof establishes the package logic, not a Verus implementation.

technique: sound standard-wand algorithm

What it is. For a wand A -* B1 * ... * Bn, the algorithm traverses B1 * ... * Bn left to right, as the FIA does, maintaining the outer state and witness set. For each Bi: (case 1) if every sigma_A in the witness set satisfies Bi, use Atom to transfer the permissions and values for Bi from each sigma_A to its sigma_B; the transferred permissions may differ per pair, and the outer state is unchanged. (Case 2) otherwise, fail if combining the outer state with each sigma_A is not sufficient to satisfy Bi; else use Extract to transfer permissions from the outer state to each sigma_A so that Bi holds in it, then apply case 1 (Section 3.5, pp. 142–143). The paper states the algorithm “requires the same annotation overhead as the prior, flawed Viper algorithm” (Section 1, p. 132).

How to apply it. Start with the package operation’s current state and the left-hand witness set. Walk each separating-conjunction component. Apply case 1 when all witness states satisfy the component. Apply case 2 when some do not: fail if the outer state cannot make up the difference for every witness state, otherwise extract from the outer state and apply case 1. The footprint is everything extracted from the outer state. Implications are handled as described in App. I of the technical report (Section 3.5, footnote 6, p. 142).

Evidence. On the Viper test suite, the paper compares FIA, its standard algorithm (S-Alg), and its combinable algorithm (C-Alg). Of 85 files containing at least one package operation, 29 files with features the implementation does not yet support were removed, leaving 56 benchmarks; 28 of the 29 removed files require proof scripts, which the authors call orthogonal. Table 1 reports: FIA 55 expected results, 1 incorrectly verified, 0 spurious errors; S-Alg 51, 0, 5; C-Alg 48, 0, 8 (Section 5, Table 1, p. 146). The FIA’s incorrectly verified program comes from the pre-existing test suite (Section 5, p. 147). Inference: the benchmark result shows zero incorrectly verified programs on this set; the soundness claim itself rests on the package-logic proof, and false positives remain.

Performance was measured by five runs per benchmark on a Lenovo T480 with 32 GB RAM and an i7-8550U 1.8 GHz CPU under Windows 10; the slowest and fastest runs were removed and the mean of the remaining three was used. FIA takes 1–11 seconds per benchmark; S-Alg is on average 21% slower than FIA, the increase is below 30% for 46 of 56 benchmarks, and for 3 benchmarks S-Alg is between 2 and 3.4 times slower; C-Alg is on average 10% slower than S-Alg (Section 5, p. 147).

Verus form. Inference: a Verus library could implement a restricted, structural counterpart by carrying a ghost “remaining resource” predicate through loops and proving that each cursor step preserves it. The universal witness-set algorithm would require a permission algebra absent from ordinary Verus specifications, so direct translation is a research design rather than an existing Verus feature.

technique: combinable wands for fractional permissions

What it is. An assertion A is combinable iff A^p * A^q entails A^(p+q) for positive p, q with p + q ≤ 1. The paper shows standard wands are not combinable in general, even when the right side is: a footprint can be incompatible with the left side at full scale but become compatible after scaling. In the example acc(x.f, 1/2) -* acc(x.g), a state with full permission to only x.f and a state with full permission to only x.g are both valid footprints, but a state with half permission to both fields is not (Section 4, pp. 143–144).

The remedy is a combinable wand A -*c B. scaled(sigma) is the set of alpha · sigma for 0 < alpha ≤ 1. A footprint is scalable for a wand iff, for every state satisfying A, either all states in its scaled set are compatible with that state or none are. In a concrete algebra of (permission mask, partial heap) pairs, Definition 1 sets R(sigma_A, sigma_w) to sigma_w if no state in scaled(sigma_w) is compatible with sigma_A, and otherwise caps each permission at min(pi_w(l), 1 - pi_A(l)). Then sigma_w satisfies A -*c B iff for every sigma_A satisfying A that is compatible with R(sigma_A, sigma_w), their combination satisfies B (Section 4, Definition 1, pp. 144–145).

How to apply it. Use the restricted wand where fractional instances may be combined. Check that the right side B is combinable. Infer footprints with the package logic lifted to the restricted footprint definition, as described in App. H of the technical report (Section 4, p. 146). Theorem 3, for intuitionistic B, proves: if B is combinable, A -*c B is combinable; A -*c B entails A -* B, so a combinable wand can be applied like a standard wand; and if A is binary (expressible without fractional permissions), A -*c B and A -* B are equivalent (Theorem 3, p. 145). The paper’s example: Tree(x) is binary, so Tree(y) -*c Tree(x) and Tree(y) -* Tree(x) are equivalent (Section 4, p. 145).

Verus form. Inference: Verus’s ordinary ownership is exclusive and does not expose fractional permission arithmetic. A Verus analogue would need ghost permission tokens or an explicit fractional resource algebra, plus lemmas proving split, scale, and recombination. The paper does not show such an encoding, so product claims should distinguish this inference from the Viper result.

evidence, assumptions, and boundaries

The Isabelle formalization proves the package logic’s soundness and completeness for any instantiation of its parameters, and Theorem 3 for combinable wands (Sections 1, 3–4). The Viper implementation uses a total-heap semantics of IDF and represents heaps, permission masks, and witness sets as Boogie maps (Section 5, p. 146). The experiment excludes 29 of 85 candidate files. For S-Alg, 3 of 5 false positives come from missing implementation features, 1 from a wand whose only potential footprint prevents it from ever being applied (which the authors consider useful to reject), and 1 from a coarse-grained heuristic; C-Alg’s 3 additional false positives are wands that do hold as combinable wands but need extensions regarding predicate instances. The authors note that wands occur much more frequently in the benchmarks than in average Viper projects, and expect a smaller slowdown on more representative projects (Section 5, p. 147).

Theorems 1 and 2 assume a well-formed right side, which the paper says roughly corresponds to a self-framing assertion (footnote 5, p. 142). Inference: the paper does not prove the Viper verifier, Boogie, or the SMT solver correct; its theorems concern the package logic. The introduction states that “a separation logic even without the separating conjunction (but with the magic wand) is as expressive as a variant of second-order logic and, thus, undecidable” (Section 1, p. 131).

Inference: the threat to VeruLaw is targeted. Magic-wand packaging is directly relevant to borrow-remainder proofs, but the paper’s implementation is Viper/Boogie and its permission algebra is absent from standard Verus. VL should reuse the soundness boundary—universal witnesses, stable footprints, and explicit handling of fractional scaling—before attempting any automatic remainder synthesis. Inference: an unsound shortcut that selects a footprint per case of the left side, as the FIA does, would threaten verified Rust claims; this paper gives a concrete reason to reject that design.

techniques for the catalog

• package logic — characterize wand automation as sound and complete witness-set reductions over a parameterized separation algebra
• standard-wand algorithm — traverse right-hand conjuncts with atom transfer and stable extraction while checking every left-side witness
• scalable footprints — normalize fractional footprints so compatibility does not change under scaling
• combinable wand — restrict wand semantics so fractional instances can be recombined soundly
• Viper evaluation protocol — compare sound and prior algorithms on fixed benchmark denominators with explicit false-positive counts Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Recall from Sect. 2.4 that the mistake underlying the FIA approach ultimately resulted from allowing multiple different footprints to be selected conditionally on a state satisfying A, rather than a single footprint which works for all such states.”): checked all quotations, numbers (Table 1, benchmark counts, timing), section, page and theorem references, and the rule and algorithm steps against the paper text; changed the package-logic steps to the four rules as stated (the footprint is what is extracted, not the remainder), the algorithm’s case 2, the combinable-wand definition (scalability is a definition, R applies to all footprints, Theorem 3 needs intuitionistic B), the worked-derivation wand, page references (performance and false positives are on p. 147), added the 3-benchmark 2–3.4× slowdown and the false-positive breakdown, marked tool-correctness and benchmark-soundness remarks as Inference, and removed unsupported remarks; did not check the technical report’s appendices, the Isabelle or Viper artifacts, or the Verus-form inferences against Verus.

Last edited: 2026-10-17