Formalization of a Framework for the Sound Automation of Magic Wands

The magic wand $\mathbin{-\!\!*}$ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula $$A \mathbin{-\!\!*} B$$ is a state that, combined with any state in which $A$ holds, yields a state in which $B$ holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or are unsound. In this entry, we formally define a framework for the sound automation of magic wands, described in an upcoming paper at CAV 2022, and prove that it is sound and complete. This framework, called the package logic, precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics.