# Predictable Verification using Intrinsic Definitions

Adithya Murali  0000-0002-6311-1467 University of Illinois at Urbana-
ChampaignUrbanaUSA<EMAIL_ADDRESS>,  Cody Rivera  0000-0001-7824-4054
University of Illinois at Urbana-ChampaignUrbanaUSA<EMAIL_ADDRESS>and
P. Madhusudan  0000-0002-9782-721X University of Illinois at Urbana-
ChampaignUrbanaUSA<EMAIL_ADDRESS>
(2024; 2023-11-16; 2024-03-31)

###### Abstract.

We propose a novel mechanism of defining data structures using _intrinsic
definitions_ that avoids recursion and instead utilizes _monadic maps
satisfying local conditions_. We show that intrinsic definitions are a
powerful mechanism that can capture a variety of data structures naturally. We
show that they also enable a predictable verification methodology that allows
engineers to write ghost code to update monadic maps and perform verification
using reduction to decidable logics. We evaluate our methodology using Boogie
and prove a suite of data structure manipulating programs correct.

Predictable Verification, Intrinsic Definitions, Verification of Linked Data
Structures, Decidability, Ghost-Code Annotations

††copyright: rightsretained††doi: 10.1145/3656450††journalyear:
2024††submissionid: pldi24main-p621-p††journal: PACMPL††journalvolume:
8††journalnumber: PLDI††article: 220††publicationmonth: 6††ccs: Software and
its engineering Formal software verification††ccs: Theory of computation Logic
and verification††ccs: Theory of computation Automated reasoning

##  1\. Introduction

In computer science in general, and program verification in particular,
classes of finite structures (such as data structures) are commonly defined
using _recursive definitions (aka inductive definitions)_. Proving that a set
of structures is in such a class or proving that structures in the class have
a property is naturally performed using _induction_ , typically mirroring the
recursive structure in its definition. For example, trees in pointer-based
heaps can be defined using the following recursive definition in first-order
logic (FOL) with least fixpoint semantics for definitions:

(1)
$\displaystyle\begin{split}\textit{tree}(x)::=_{\textit{lfp}}&~{}x=\mathit{nil}\vee\big{(}x\not=\mathit{nil}\wedge\textit{tree}(l(x))\wedge\textit{tree}(r(x))\\\
&~{}~{}\wedge x\not\in\mathit{htree}(l(x))\wedge
x\not\in\mathit{htree}(r(x))\wedge\mathit{htree}(l(x))\cap\mathit{htree}(r(x))=\emptyset\big{)}\\\
\mathit{htree}(x)::=_{\textit{lfp}}&~{}ite\left(x=\mathit{nil},~{}\emptyset,~{}\mathit{htree}\left(l(x)\right)\cup\mathit{htree}\left(r(x)\right)\cup\\{x\\}\right)\end{split}$

In the above, $\mathit{htree}$ maps each location $x$ in the heap to the set
of all locations reachable from $x$ using $l$ and $r$ pointers, and the
definition of $\mathit{tree}$ uses this to ensure that the left and right
trees are disjoint from each other and the root. Definitions in separation
logic are similar (with heaplets being implicitly defined, and disjointness
expressed using the separating conjunction ’$\star$’ (Reynolds, 2002a;
O’Hearn, 2012; O’Hearn et al., 2001)).

When performing imperative program verification, we annotate programs with
loop invariants and contracts for methods, and reduce verification to
validation of Hoare triples of the form $\\{\alpha\\}s\\{\beta\\}$, where $s$
is a straight-line program (potentially with calls to other methods encoded
using their contracts). The validity of each Hoare triple is translated to a
pure logical validity question, called the _verification condition_ (VC). When
$\alpha$ and $\beta$ refer to data structure properties, the resulting VCs are
typically proved using induction on the structure of the recursive
definitions. Automation of program verification reduces to automating validity
of the logic the VCs are expressed in.

Logics that are powerful enough to express rich properties of data structures
are invariably incomplete, not just undecidable, i.e., they do not admit any
automated procedure that is complete (guaranteed to eventually prove any valid
theorem, but need not terminate on invalid theorems). For instance, validity
is incomplete for both first-order logic with least fixpoints and separation
logic. Consequently, though verification frameworks like Dafny (Leino, 2010)
support rich specification languages, validation of verification conditions
can fail even for valid Hoare triples. Automated verification engines hence
support several heuristics resulting in sound but incomplete verification.

When proofs succeed in such systems, the verification engineer is happy that
automation has taken the proof through. However, when proofs _fail_ , as they
often do, the verification engineer is stuck and perplexed. First, they would
crosscheck to see whether their annotations are strong enough and that the
Hoare triples are indeed valid. If they believe they are, they do not have
clear guidelines to help the tool overcome its incompleteness. Engineers are
instead required to know the _underlying proof mechanisms/heuristics_ the
verification system uses in order to figure out why the system is unable to
succeed, and figure out how to help the system. For instance, for data
structures with recursive definitions, the proof system may just unfold
definitions a few times, and the engineer must be able to see why this
heuristic will not be able to prove the theorem and formulate new inductively
provable lemmas or quantification triggers that can help. Such _unpredictable_
verification systems that require engineers to know their internal heuristics
and proof mechanisms frustrate verification experience.

_Predictable Verification. _ In this paper, we seek an entirely new paradigm
of _predictable_ verification. We want a technique where:

(a):

the verification engineer is asked to provide upfront a set of annotations
that help prove programs correct, where these annotations are entirely
_independent_ of the verification mechanisms/tools, and

(b):

the program verification problem, given these annotations, is guaranteed to be
_decidable_ (and preferably decidable using efficient engines such as SMT
solvers).

The upfront agreement on the information that the verification engineer is
required to provide makes their task crystal clear. The fact that the
verification is decidable given these annotations ensures that the
verification engine, given enough resources of time and space (of course) will
eventually return proving the program correct or showing that the program or
annotations are incorrect. There is no second-guessing by the engineer as the
verification will never fail on valid theorems, and hence they need not worry
about knowing how the verification engine works, or give further help. Note
that the verification _without annotations_ can (and typically will be)
undecidable.

_Intrinsic Definitions of Data Structures. _ In this paper, we propose an
entirely new way of defining data structures, called _intrinsic definitions_ ,
that facilitates a predictable verification paradigm for proving their
maintenance. Rather than defining data structures using recursion, like in
equation (1) above (which naturally calls for inductive proofs and invariably
entails incompleteness), we define data structures by augmenting each location
with additional information using _ghost maps_ and demanding that certain
_local conditions_ hold between each location and its neighbors.

Intrinsic definitions formally require a set of monadic maps (maps of arity
one) that associate values to each location in a structure (we can think of
these as ghost fields associated with each location/object). We demand that
the monadic maps on local neighborhoods of every location satisfy certain
logical conditions. The existence of maps that satisfy the local logical
conditions ensures that the structure is a valid data structure.

For example, we can capture trees in pointer-based heaps in the following way.
Let us introduce maps $\mathit{tree}:Loc\rightarrow Bool$,
$\mathit{rank}:Loc\rightarrow\mathbb{Q}^{+}$ (non-negative rationals), and
$p:Loc\rightarrow Loc$ (for “parent”), and demand the following local
property:

$\displaystyle\begin{split}\forall
x::Loc.(\mathit{tree}(x)\Rightarrow&(~{}(l(x)\not=\mathit{nil}\Rightarrow(\mathit{tree}(l(x))\wedge
p(l(x))=x\wedge\mathit{rank}(l(x))<\mathit{rank}(x)))\\\
&\wedge(r(x)\not=\mathit{nil}\Rightarrow(\mathit{tree}(r(x))\wedge
p(r(x))=x\wedge\mathit{rank}(r(x))<\mathit{rank}(x)))\\\
&\wedge((l(x)\not=\mathit{nil}\land r(x)\neq\mathit{nil})\Rightarrow l(x)\neq
r(x))\\\ &\wedge(p(x)\not=\mathit{nil}\Rightarrow(r(p(x))=x\vee
l(p(x))=x)))~{}~{})\end{split}$

The above demands that ranks become smaller as one descends the tree, that a
node is the parent of its children, and that a node is either the left or
right child of its parent.

Given a _finite_ heap, it is easy to see that if there exist maps
$\mathit{tree}$, $\mathit{rank}$ and $p$ that satisfy the above property, and
if $\textit{tree}(l)$ is true for a location $l$, then $l$ must point to a
tree (strictly decreasing ranks ensure that there are no cycles and existence
of a unique parent ensures that there are no “merges”). Furthermore, in any
heap, if $T$ is the subset of locations that are roots of trees, then there
are maps that satisfy the above property and have precisely $tree(l)$ to be
true for locations in $T$.

Note that the above intrinsic definition _does not use recursion_ or least
fixpoint semantics. It simply requires maps such that each location satisfies
the local neighborhood condition.

_Fix-What-You-Break Program Verification Methodology. _

Intrinsic definitions are particularly attractive for proving _maintenance_ of
structures when structures undergo mutation. When a program mutates a heap $H$
to a heap $H^{\prime}$, we start with monadic maps that satisfy local
conditions in the pre-state. As the heap $H$ is modified, we ask the
verification engineer to also _repair_ the monadic maps, using ghost map
updates, so that the local conditions on all locations are met in the heap in
the post-state $H^{\prime}$.

For instance, consider a program that walks down a tree from its root to a
node $x$ and introduces a newly allocated node $n$ between $x$ and $x$’s right
child $r$. Then we would assume in the precondition that the monadic maps
$\mathit{tree}$, $\mathit{rank}$, and $p$ exist satisfying the local condition
(2) above. After the mutation, we would simply update these maps so that
$\mathit{tree}(n)$ is true, $p(r)=n$, $p(n)=x$, and $rank(n)$ is, say,
$(\textit{rank(x)}+\textit{rank}(r))/2$.

The annotations required of the user, therefore, are ghost map updates to
locations such that the local conditions are valid for each location. We will
guarantee that checking whether the local conditions holds for each location,
after the repairs, is expressible in decidable logics.

We propose a modular verification approach for verifying data structure
maintenance that asks the programmer to fix what they break. Given a program
that we want to verify, we instead verify an _augmented program_ that keeps
track of a ghost set of _broken locations_ $\mathit{Br}$. Broken locations are
those that (potentially) do not satisfy the local condition. When the program
destructively modifies the fields of an object/location, it and some of its
neighbors (accessible using pointers from the object) may not satisfy the
local condition anymore, and hence will get added to the broken set. The
verification engineer must repair the monadic maps on these broken locations
and ensure (through an assertion) that the local condition holds on them
before removing them from the broken set $Br$. However, even while repairing
monadic maps on a location, the local condition on _its neighboring_ locations
may fail and get added to the broken set.

We develop a _fix-what-you-break (FWYB)_ program verification paradigm, giving
formal rules of how to augment programs with broken sets, how users can modify
monadic maps, and fixed recipes of how broken sets are maintained in any
program. In order to verify that a method $m$ maintains a data structure, we
need to prove that if $m$ starts with the broken set being empty, it returns
with the empty broken set. We prove this methodology sound, i.e., if the
program augmented with broken sets and ghost updates is correct, then the
original program maintains the data structure properties mentioned in its
contracts.

_Decidable Verification of Annotated Programs. _ The general idea of using
local conditions to capture global properties has been explored in the
literature to reduce the complexity of proofs (e.g., iterated separation in
separation logic (Reynolds, 2002b); see Section 6). Intrinsic definitions of
data structures and the fix-what-you-break program verification methodology
are more specifically designed to ensure the key property of _decidable
verification of annotated programs_ by avoiding both recursion/least-fixpoint
definitions and avoiding even quantified reasoning.

The verification conditions for Hoare triples involving basic blocks of our
annotated programs have the following structure. First, the precondition can
be captured using _uninterpreted monadic functions_ that are _implicitly_
assumed to satisfy the local condition on each location that is not in the
broken set $Br$ (avoiding universal quantification). The monadic map updates
(repairs) that the verification engineer makes can be captured using map
updates. The postcondition of the ghost-code augmented program can, in
addition to properties of variables, assert properties of the broken set $Br$
using logics over sets. Finally, we show that capturing the modified heap
after function calls can be captured using _parameterized map update_
theories, that are decidable (de Moura and Bjørner, 2009). Consequently, the
entire verification condition is captured in quantifier-free logics involving
maps, parametric map updates, and sets over combined theories. These
verification conditions are hence decidable and efficiently handled by modern
SMT solvers111Assuming of course that the underlying quantifier-free theories
are decidable; for example, integer multiplication in the program or in local
conditions would make verification undecidable, of course..

_Intrinsic Definitions for Representative Data Structures and Verification in
Boogie. _ Intrinsic definitions of data structures is a novel paradigm and
capturing data structures requires thinking anew in order to formulate monadic
maps and local conditions that characterize them.

We give intrinsic definitions for several classic data structures such as
linked lists, sorted lists, circular lists, trees, binary search trees, AVL
trees, and red-black trees. These require novel definitions of monadic maps
and local conditions. We also show how standard methods on these data
structures (insertions, deletions, concatenations, rotations, balancing, etc.)
can be verified using the fix-what-you-break strategy and standard loop
invariant/contract annotations. We also consider _overlaid data structures_
consisting of multiple data structures overlapping and sharing locations. In
particular, we model the core of an overlaid data structure that is used in an
I/O scheduler in Linux that has a linked list (modeling a FIFO queue) overlaid
on a binary search tree (for efficient search over a key field). Intrinsic
definitions beautifully capture such structures by compositionally combining
the instrinsic definitions for each structure and a local condition linking
them together. We show methods to modify this structure are provable using
fix-what-you-break verification.

We model the above data structures and the annotated methods in the low-level
programming language Boogie. Boogie is an intermediate programming language
with verification support that several high-level programming languages
compile to for verification (e.g., C (Cohen et al., 2009; Condit et al.,
2009), Dafny (Leino, 2010), Civl (Kragl and Qadeer, 2021), Move (Dill et al.,
2022)). These annotated programs do not use quantifiers or recursive
definitions, and Boogie is able to verify them automatically using decidable
verification in negligible time, without further user-help.

_Contributions. _ The paper makes the following contributions:

  * •

A new paradigm of _predictable verification_ that asks upfront for
programmatic annotations and ensures annotated program verification is
decidable, without reliance on users to give heuristics and tactics.

  * •

A novel notion of intrinsic definitions of data structures based on ghost
monadic maps and local conditions.

  * •

A predictable verification methodology for programs that manipulate data
structures with intrinsic definitions following a fix-what-you-break (FWYB)
methodology.

  * •

Intrinsic definitions for several classic data structures, and fix-what-you-
break annotations for programs that manipulate such structures, with
realization of these programs and their verification using Boogie.

##  2\. Intrinsic Definitions of Data Structures: The Framework

In this section we present the first main contribution of our paper, the
framework of intrinsically defined data structures. We first define the notion
of a data structure in a pointer-based heap.

###  2.1. Data Structures

In this paper, we think of data structures defined using a _class_ $C$ of
objects. The class $C$ can coexist with other classes, heaps, and data
structures, potentially modeled and reasoned with using other mechanisms. For
technical exposition and simplicity, we restrict the technical definitions to
a single class of data structures over a class $C$.

A class $C$ has a signature $(\mathcal{S},\mathcal{F})$ consisting of a finite
set of sorts $\mathcal{S}=\\{\sigma_{0},\sigma_{1}\ldots,\sigma_{n}\\}$ and a
finite set of fields $\mathcal{F}=\\{f_{1},f_{2}\ldots,f_{m}\\}$. We assume
without loss of generality that the sort $\sigma_{0}$ represents the sort of
objects of the class $C$, and we denote this sort by $C$ itself. We use $C$ to
model objects in the heap. The other “background” sorts, e.g., integers, are
used to model the values of the objects’ fields. Each field
$f_{i}:C\rightarrow\sigma$ is a unary function symbol and is used to model
pointer and data fields of heap locations/objects. We model $\mathit{nil}$ as
a non-object value and denote the sort $C\uplus\\{\mathit{nil}\\}$ consisting
of objects as well as the $\mathit{nil}$ value by $C?$.

A $C$-heap $H$ is a _finite_ first-order model of the signature of $C$. More
formally, it is a pair $(O,I)$ where $O$ is a finite set of _objects_
interpreting the foreground sort $C$ and $I$ is an interpretation of every
field in $\mathcal{F}$ for every object in $O$.

###### Example 2.1 ($C$-Heap).

Let $C$ be the class consisting of a pointer field $\mathit{next}:C\rightarrow
C?$ and a data field $\mathit{key}:C\rightarrow\mathit{Int}$. The figure on
the right represents a $C$-heap consisting of objects $O=\\{o_{1},o_{2}\\}$
and the illustrated interpretation $I$ for $\mathit{next}$ and
$\mathit{key}$.∎

$o_{1}$$o_{2}$$\mathit{nil}$$1$$2$$\mathit{next}$$\mathit{next}$$\mathit{key}$$\mathit{key}$

We now define a data structure. We fix a class $C$.

###### Definition 2.2 (Data Structure).

A data structure $D$ of arity $k$ is a set of triples of the form
$(O,I,\overline{o})$ such that $(O,I)$ is a $C$-heap and $\overline{o}$ is a
$k$-tuple of objects from $O$.∎

Informally, a data structure is a particular subset of $C$-heaps along with a
distinguished tuple of locations $\overline{o}$ in the heap that serve as the
“entry points” into the data structure, such as the root of a tree or the ends
of a linked list segment.

###### Example 2.3 (Sorted Linked List).

Let $C$ be the class defined in Example 2.1. The data structure of sorted
linked lists is the set of all $(O,I,o_{1})$ such that $O$ contains objects
$o_{1},o_{2}\ldots o_{n}$ with the interpretation
$\mathit{next}(o_{i})=o_{i+1}$ and
$\mathit{key}(o_{i})\leq\mathit{key}(o_{i+1})$ for every $1\leq i<n$, and
$\mathit{next}(o_{n})=\mathit{nil}$. For example, let $(O,I)$ be the $C$-heap
described in Example 2.1. The triple $(O,I,o_{1})$ is an example of a sorted
linked list. Here $o_{1}$ represents the head of the sorted linked list.∎

###  2.2. Intrinsic Definitions of Data Structures

In this work, we propose a characterization of data structures using
_intrinsic definitions_. Intrinsic definitions consist of a set of _monadic
maps_ that associate (ghost) values to each object and a set of _local_
conditions that constrain the monadic maps on each location and its neighbors.
A $C$-heap is considered to be a valid data structure if _there exists_ a set
of monadic maps for the heap that satisfy the local conditions.

Annotations using intrinsic definitions enable local and decidable reasoning
for correctness of programs manipulating data structures using the Fix-What-
You-Break (FWYB) methodology, which is described later in Section 3. We
develop the core idea of intrinsic definitions below.

_Ghost Monadic Maps. _ We denote by
$C_{\mathcal{G}}=(\mathcal{S},\mathcal{F}\cup\mathcal{G})$ an extension of $C$
with a finite set of monadic (i.e., unary) function symbols $\mathcal{G}$. We
can think of these as _ghost_ fields of objects.

The key idea behind intrinsic definitions is to extend a $C$-heap with a set
of ghost monadic maps and formulate local conditions using the maps that
characterize the heaps belonging to the data structure. The existence of such
ghost maps satisfying the local conditions is then the intrinsic definition.
Definitions are parameterized by a multi-sorted first-order logic
$\mathcal{L}$ in which local conditions are stated. The logic has the sorts
$\mathcal{S}$ and contains the function symbols in
$\mathcal{F}\cup\mathcal{G}$, as well as interpreted functions over background
sorts (such as $+$ and $<$ on integers, and $\subseteq$ on sets).

###### Definition 2.4 (Intrinsic Definition).

Let $C=(\mathcal{S},\mathcal{F})$ be a class. An intrinsic definition
$\mathit{IDS}(\overline{y})$ over the class $C$ is a tuple
$(\mathcal{G},\mathcal{L},\mathit{LC},\varphi(\overline{y}))$ where:

  1. (1)

$\mathcal{G}$ is a finite set of _monadic map names and function signatures_
disjoint from $\mathcal{F}$,

  2. (2)

$\mathcal{L}$ is a first-order logic over the sorts $\mathcal{S}$ containing
the interpreted functions of the background sorts as well as the function
symbols in $\mathcal{F}\cup\mathcal{G}$,

  3. (3)

A _local condition_ formula $\mathit{LC}$ of the form $\forall
x:Loc.\,\rho(x)$ such that $\rho$ is a quantifier-free $\mathcal{L}$-formula,
and

  4. (4)

A _correlation formula_ $\varphi(\overline{y})$ that is a quantifier-free
$\mathcal{L}$-formula over free variables $\overline{y}\in Loc$.∎

We denote an intrinsic definition by
$(\mathcal{G},\mathit{LC},\varphi(\overline{y}))$ when the logic $\mathcal{L}$
is clear from context. In this work $\mathcal{L}$ is typically a decidable
combination of quantifier-free theories (Nelson, 1980; Nelson and Oppen, 1979;
Tinelli and Zarba, 2004), containing theories of integers, sets, arrays (de
Moura and Bjørner, 2009), etc., supported effectively in practice by SMT
solvers (De Moura and Bjørner, 2008; Barrett et al., 2011).

###### Definition 2.5 (Data Structures defined by Intrinsic Definitions).

Let $C=(\mathcal{S},\mathcal{F})$ be a class and
$\mathit{IDS}(\overline{y})=(\mathcal{G},\textit{LC},\varphi(\overline{y}))$
be an intrinsic definition over $C$ consisting of monadic maps $\mathcal{G}$,
local condition $\mathit{LC}$ and correlation formula $\varphi$. The data
structure defined by $\mathit{IDS}$ is precisely the set of all
$(O,I,\overline{o})$ where _there exists_ an interpretation $J$ that extends
$I$ with interpretations for the symbols in $\mathcal{G}$ such that
$O,J\models LC$ and
$O,J[\overline{y}\mapsto\overline{o}]\models\varphi(\overline{y})$, where
$[\overline{y}\mapsto\overline{o}]$ denotes that the free variables
$\overline{y}$ are interpreted as $\overline{o}$.

Informally, given a data structure $\mathit{DS}$ consisting of triples
$(O,I,\overline{o})$, an intrinsic definition demands that there exist monadic
maps $\mathcal{G}$ such that the $C$-heaps $(O,I)$ in the data structure can
be extended with values for maps in $\mathcal{G}$ satisfying the local
conditions $\mathit{LC}$, and the entrypoints $\overline{o}$ are characterized
in the extension by the quantifier-free formula $\varphi$.

###### Example 2.6 (Sorted Linked List).

Recall the data structure of sorted linked lists defined in Example 2.3. We
capture sorted linked lists by an intrinsic definition $\mathit{SortedLL}(y)$
using monadic maps $\mathit{sortedll}:C\rightarrow\mathit{Bool}$ and
$\mathit{rank}:C\rightarrow\mathbb{Q}^{+}$ such that:

$\displaystyle\mathit{LC}\equiv$ $\displaystyle\;\forall
x.\;\Big{(}(\mathit{sortedll}(x)\,\land\,\mathit{next}(x)\neq\mathit{nil})\Rightarrow$
$\displaystyle\hskip
60.00009pt(\mathit{sortedll}(\mathit{next}(x))\,\land\,\mathit{rank}(\mathit{next}(x))<\mathit{rank}(x)\,\land\,\mathit{key}(x)\leq\mathit{key}(\mathit{next}(x)))\Big{)}$
$\displaystyle\varphi(y)\equiv$ $\displaystyle\;\;\mathit{sortedll}(y)$

In the above definition the $\mathit{rank}$ field decreases wherever
$\mathit{sortedll}$ holds as we take the next pointer, and hence assures that
there are no cycles. Observe that without the constraint on $\mathit{rank}$,
the triple $(\\{o_{1},o_{2}\\},I,o_{1})$ where
$I=\\{\mathit{next}(o_{1})=o_{2},\mathit{next}(o_{2})=o_{1},\mathit{key}(o_{1})=\mathit{key}(o_{2})=0\\}$
denoting a two-element circular list would satisfy the definition, which is
undesirable.

Note that the above allows for a heap to contain both sorted lists as well as
unsorted lists. We are guaranteed by the local condition that the set of all
objects where sortedll is true will be the heads of sorted lists.

We can also replace the domain of ranks in the above definition using any
strict partial order, say integers or reals (with the usual $<$ order on
them), and the definition will continue to define sorted lists. Well-
foundedness of the order is not important as heaps are _finite_ in our work
(see definition of $C$-heaps in Section 2.1)∎

##  3\. Fix What You Break (FWYB) Verification Methodology

In this section we present the second main contribution of this paper: the
Fix-What-You-Break (FWYB) methodology. We begin by describing a while
programming language and defining the verification problem we study. We fix a
class $C=(\mathcal{S},\mathcal{F})$ throughout this section.

###  3.1. Programs, Contracts, and Correctness

_Programs. _ Figure 1 shows the programming language used in this work. Note
that we can use variables and expressions over non-object sorts. Functions can
return multiple outputs. We assume that method signatures contain designated
output variables and therefore the return statement does not mention values.

Our language is safe (i.e., allocated locations cannot point to un-allocated
locations) and garbage-collected. Formally we consider configurations $\theta$
consisting of a store (map from variables to values) and a heap along with an
error state $\bot$ to model error on a null dereference. We denote that a
formula $\alpha$ is satisfied on a configuration $\theta$ by writing
$\theta\models\alpha$.

$\displaystyle P\coloneqq$
$\displaystyle\;\;x\,:=\,\mathit{nil}\;\;|\;\;x\,:=\,y\;\;|\;\;v\,:=\,be\;\;|\;\;y\,:=\,x.f\;\;|\;\;v\,:=\,x.d$
$\displaystyle\;\;|\;\;x.f\,:=\,y\;\;|\;\;x.d\,:=\,v\;\;|\;\;x\,:=\,\mathsf{new}\;C()\;\;|\;\;\overline{r}\,:=\,\mathit{Function}(\overline{t})$
$\displaystyle\;\;|\;\;\mathsf{skip}\;\;|\;\;\mathsf{assume}\;\mathit{cond}\;\;|\;\;\mathsf{return}\;\;|\;\;P\,;\,P\;\;|\;\;\mathsf{if}\;\mathit{cond}\;\mathsf{then}\;P\;\mathsf{else}\;P\;\;|\;\;\mathsf{while}\;\mathsf{cond}\;\mathsf{do}\;P\;$
$\displaystyle\mathit{cond}\coloneqq$ $\displaystyle\;\;x=y\;\;|\;\;x\neq
y\;\;|\;\;\mathit{be}\;\;\;\;\textrm{(Condition Expressions)}$ Figure 1.
Grammar of while programs with recursion. $x,y$ are variables denoting objects
of class $C?$ (i.e., $C$ objects or $\mathit{nil}$), $v,w$ are a background
sort(s) variables, $r,t$ denote variables of any sort, $f$ is a pointer field,
$d$ is a data field, and $be$ is a expression of the background sort(s).

_Intrinsic Hoare Triples. _ The verification problem we study in this paper is
_maintenance_ of data structure properties. Fix an intrinsic definition
$(\mathcal{G},\mathit{LC},\varphi(\overline{y}))$ where
$\mathcal{G}=\\{g_{1},g_{2}\ldots,g_{k}\\}$. Let $\overline{z}$ be the
input/output variables for a program that we want to verify. We consider pre
and post conditions of the form

${\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{k}.\,(\mathit{LC}\land\varphi(\overline{w})\land\psi(\overline{z}))$

where each $g_{i}$ is a ghost monadic map (unary function over locations),
$\psi$ is a quantifier-free formula over $\overline{z}$ that can use the ghost
monadic maps $g_{i}$, and $\overline{w}$ is a tuple of variables from
$\overline{z}$ whose arity is equal to $\overline{y}$. Note that the above has
a second-order existential quantification
(${\mathbf{\exists}\\!\\!\\!\exists}$) over function symbols
$g_{1},\ldots,g_{k}$, and $\mathit{LC}$ has first-order universal
quantification over a single location variable. Read in plain English,
“$\,\overline{w}$ points to a data structure $\mathit{IDS}$ such that the
(quantifier-free) property $\psi(\overline{z})$ holds”.

We study the validity of the following Hoare Triples:

$\langle\,\alpha(\overline{x})\,\rangle\;\;\mathrm{P}(\overline{x},\,\mathit{ret}\\!:\,\overline{r})\;\;\langle\,\beta(\overline{x},\overline{r})\,\rangle$

where $\alpha$ and $\beta$ are pre and post conditions of the above form,
$\mathrm{P}$ is a program, and $\overline{x},\overline{r}$ are input and
output variables for $\mathrm{P}$ respectively.

###### Example 3.1 (Running Example: Insertion into a Sorted List).

Let $\mathit{SortedLL}(y)=(\mathcal{G},\mathit{LC},\mathit{sorted}(y))$ as in
Example 2.6 where $\mathcal{G}=\\{\mathit{sortedll},\mathit{rank}\\}$. The
following Hoare triple says that insertion into a sorted list returns a sorted
list:

$\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,\mathit{sortedll},\mathit{rank}.\,\mathit{LC}\land\mathit{sortedll}(x)\,\rangle\;\mathit{sorted\\!\\!-\\!\\!insert}(x,k,\,\mathit{ret}\\!:x)\;\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,\mathit{sortedll},\mathit{rank}.\,\mathit{LC}\land\mathit{sortedll}(x)\,\rangle$

where $x,r$ are variables of type $C$, $k$ is of type $\mathit{Int}$ and
$\mathit{sorted\\!\\!-\\!\\!insert}$ is the usual recursive method.

_Validity of Intrinsic Hoare Triples. _ We now define the validity of Hoare
Triples.

###### Definition 3.2 (Validity of Intrinsic Hoare Triples).

An intrinsic triple $\langle\,\alpha\,\rangle\,P\,\langle\,\beta\,\rangle$ is
_valid_ if for every configuration $\theta$ such that $\theta\models\alpha$,
transitioning according to $P$ starting from $\theta$ does not encounter the
error state $\bot$, and furthermore, if $\theta$ transitions to
$\theta^{\prime}$ under $P$, then $\theta^{\prime}\models\beta$.

###  3.2. Ghost Code

In this work we consider the augmentation of procedures with _ghost_ or non-
executed code. Ghost code involves the manipulation of a set of distinct
_ghost variables_ and _ghost fields_ , distinguished from regular or ‘user’
variables and fields. In program verification, ghost code provides a
programmatic way of constructing values/functions that witness a particular
property.

We defer a formal definition of ghost code to the Appendix of our
supplementary material222Our supplementary material is available in either our
technical report (Murali et al., 2024b) or the permanent DOI record at
https://doi.org/10.1145/3656450. and only provide intuition here. Intuitively,
ghost variables/fields cannot influence the computation of non-ghost
variables/fields. Therefore, ghost variables and maps can be assigned values
from user variables and maps, but the reverse is not allowed. Similarly, when
conditional statements or loops use ghost variables in the condition, the body
of the statement must also consist entirely of ghost code. Simply, ghost code
cannot control the flow of the user program. These conditions can be checked
statically. Finally, we also require that ghost loops and functions always
terminate since nonterminating ghost code can change the meaning of the
original program. Our definition is agnostic to the technique used to
establish termination, however, we use ranking functions to establish
termination in our implementation in Dafny.

We formalize the above into a grammar that extends the original programming
language in Figure 1 into a ghost code-augmented language in Figure 6 in
Appendix A.2 of our supplementary material. The language of ghost programs is
similar to $P$ in Figure 1, except that we do not have allocation or assume
statements, and loops/functions must always terminate. See prior literature
for a more detailed formal treatment of ghost code (Jones, 2010; Lucas, 1968;
Filliâtre et al., 2016; Reynolds, 1981).

_Projection that Eliminates Ghost Code. _ We can define the notion of
‘projecting out’ ghost code, which takes a program that contains ghost code
and yields a pure user program with all ghost code simply eliminated.
Intuitively, the fact that ghost code does not affect the execution of the
underlying user program makes the projection operation sensible.

Fix a main method $M$ with body $P$. Let $N_{i},1\leq i\leq k$ be a set of
auxiliary methods with bodies $Q_{i}$ that $P$ can call. Note that the bodies
$P$ and $Q_{i}$ contain ghost code. Let us denote a program containing these
methods by $[(M:P);(N_{1}:Q_{1})\ldots(N_{k}:Q_{k})]$. We then define
projection as follows:

###### Definition 3.3 (Projection of Ghost-Augmented Code to User Code).

The projection of the ghost-augmented program
$[(M:P);(N_{1}:Q_{1})\ldots(N_{k}:Q_{k})]$ is the user program
$[(\hat{M}:\hat{P});(\hat{N_{1}}:\hat{Q_{1}})\ldots(\hat{N_{k}}:\hat{Q_{k}})]$
such that:

  1. (1)

The input (resp. output) signature of $\hat{M}$ is that of $M$ with the ghost
input (resp. output) parameters removed.

  2. (2)

$\hat{P}$ is derived from $P$ by: (a) eliminating all ghost code, and (b)
replacing each non-ghost function call statement of the form
$\overline{r}:=N_{j}(\overline{t})$ with the statement
$\overline{s}:=\hat{N_{j}}(\overline{u})$, where $\overline{u}$ is the non-
contiguous subsequence of $\overline{t}$ with the elements corresponding to
ghost input parameters removed and $\overline{s}$ is obtained from
$\overline{r}$ similarly. Each $\hat{Q_{i}}$ is derived from the corresponding
$Q_{i}$ by a similar transformation.

We provide an expanded version of this definition in our supplementary
material in Appendix A.2.

### An Overview of FWYB

We develop the Fix-What-You-Break (FWYB) methodology in three stages, in the
following subsections. We give here an overview of the methodology and the
stages.

Recall that intrinsic triples are of the form
$\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{k}.\,(\mathit{LC}\land\varphi\land\alpha)\,\rangle\;P\;\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{k}.\,(\mathit{LC}\land\varphi\land\beta)\,\rangle$.
In Stage 1 (Section 3.3) we remove the second-order quantification. We do this
by requiring the verification engineer to explicitly construct the $g_{i}$
maps in the post state from the maps in the pre state using _ghost code_. We
then obtain triples of the form
$\langle\,\mathit{LC}\land\varphi\land\alpha\,\rangle\;P_{\mathcal{G}}\;\langle\,\mathit{LC}\land\varphi\land\beta\,\rangle$
where $P_{\mathcal{G}}$ is an augmentation of $P$ with ghost code that updates
the $\mathcal{G}$ maps.

Note that the $\mathit{LC}$ in the contract universally quantifies over
objects. In Stages 2 (Section 3.4) and 3 (Section 3.5) we remove the
quantification by explicitly tracking the objects where the local conditions
do not hold and treating them as implicitly true on all other objects. We call
this set $\mathit{Br}$ the _broken set_. Intuitively, the broken set grows
when the program mutates pointers or makes other changes to the heap, and
shrinks when the verification engineer repairs the $\mathcal{G}$ maps using
ghost code to satisfy the $\mathit{LC}$ on the broken objects. The
specifications assume an empty broken set at the beginning of the program and
the engineer must ensure that it is empty again at the end of the program.
However, they do not have to track the objects manually. We develop in Stage 3
(Section 3.5) a discipline for writing only _well-behaved_ manipulations of
the broken set. This reduces the problem to triples of the form
$\langle\,\varphi\land\alpha\,\rangle\;P_{\mathcal{G},\mathit{Br}}\;\langle\,\varphi\land\beta\,\rangle$,
where $P_{\mathcal{G},\mathit{Br}}$ contains ghost code for updating both
$\mathcal{G}$ and $\mathit{Br}$. Note that these specifications are
quantifier-free, and checking them can be effectively automated using SMT
solvers (De Moura and Bjørner, 2008; Barrett et al., 2011).

###  3.3. Stage 1: Removing Existential Quantification over Monadic Maps using
Ghost Code

Consider an intrinsic Hoare Triple
$\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{k}.\,(\mathit{LC}\land\varphi\land\alpha)\,\rangle\;P\;\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{k}.\,(\mathit{LC}\land\varphi\land\beta)\,\rangle$.
Read simply, the precondition says that _there exist_ maps $\\{g_{i}\\}$
satisfying some properties, and the postcondition says that we must _show the
existence_ of maps $\\{g_{i}\\}$ satisfying the post state properties.

We remove existential quantification from the problem by re-formulating it as
follows: we assume that we are _given_ the maps $\\{g_{i}\\}$ as part of the
pre state such that they satisfy $\mathit{LC}\land\varphi\land\alpha$, and we
require the verification engineer to _compute_ the $\\{g_{i}\\}$ maps in the
post state satisfying $\mathit{LC}\land\varphi\land\beta$. The engineer
computes the post state maps by taking the given pre state maps and
‘repairing’ them on an object whenever the program breaks local conditions on
that object. The repairs are done using ghost code, which is a common
technique in verification literature (Jones, 2010; Lucas, 1968; Filliâtre et
al., 2016; Reynolds, 1981).

Formally, fix an intrinsically defined data structure
$(\mathcal{G},\mathit{LC},\varphi)$. We extend the class signature
$C=(\mathcal{S},\mathcal{F})$ (and consequently the programming language) to
$C_{\mathcal{G}}=(\mathcal{S},\mathcal{F}\cup\mathcal{G})$ and treat the
symbols in $\mathcal{G}$ as _ghost fields_ of objects of class $C$ in the
program semantics. Performing the transformation described above reduces the
verification problem to proving triples of the form
$\langle\,\mathit{LC}\land\varphi\land\alpha\,\rangle\;P_{\mathcal{G}}\;\langle\,\mathit{LC}\land\varphi\land\beta\,\rangle$,
where there is no existential quantification over $\mathcal{G}$ and
$P_{\mathcal{G}}$ is an augmentation of $P$ with ghost code that updates the
$\mathcal{G}$ maps. The following proposition captures the correctness of this
reduction:

###### Proposition 3.4.

Let $\psi_{\mathit{pre}}$ and $\psi_{\mathit{post}}$ be quantifier-free
formulae over $\mathcal{F}\cup\mathcal{G}$. If
$\langle\,\mathit{LC}\land\psi_{\mathit{pre}}\,\rangle\;P_{\mathcal{G}}\;\langle\,\mathit{LC}\land\psi_{\mathit{post}}\,\rangle$
is valid then $\langle\,\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{pre}}\,\rangle\;P\;\langle\,\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}\,\rangle$ is
valid 333Here the notion of validity for both triples is given by Definition
3.2, where configurations are interpreted appropriately with or without the
ghost fields., where $P$ is the projection of $P_{\mathcal{G}}$ obtained by
eliminating ghost code.

###### Proof Gist.

The full proof is in our supplementary material. The first Hoare triple shows
that if we are given _any_ maps $g_{i}$ (implicitly encoded as values of ghost
fields) that satisfy $LC$ in the pre-state, then the program with ghost code
computes a modified version of these maps such that the $LC$ is holds in the
post-state. Surely then, if there was a set of maps $g_{i}$ that satisfied
$LC$ in the pre-state, there will exists a set of maps $g_{i}^{\prime}$ that
satisfy $LC$ in the post-state. ∎

We note a point of subtlety about the reduction in this stage here: the
simplified triple eliminates existential quantification over $\mathcal{G}$ by
claiming something stronger than the original specification, namely that for
_any_ maps $\\{g_{i}\\}$ such that $\psi_{\mathit{pre}}$ is satisfied in the
pre state, there is a _computation_ that yields corresponding maps in the post
state such that $\psi_{\mathit{post}}$ holds. The onus of coming up with such
a computation is placed on the verification engineer.

###  3.4. Stage 2: Relaxing Universal Quantification using Broken Sets

We turn to verifying programs whose pre and post conditions are of the form
$\mathit{LC}\land\gamma$, where $\mathit{LC}\equiv\forall z.\,\rho(z)$ is the
local condition. Consider a program $P$ that maintains the data structure. The
local conditions are satisfied everywhere in both the pre and post state of
$P$. However, they need not hold everywhere in the intermediate states. In
particular, $P$ may call a method $N$ which may neither receive nor return a
proper data structure. To reason about $P$ modularly we must be able to
express contracts for methods like $N$. To do this we must be able to talk
about program states where only some objects may satisfy the local conditions.

_Broken Sets. _ We introduce in programs a ghost set variable $\mathit{Br}$
that represents the set of (potentially) broken objects. Intuitively, at any
point in the program the local conditions must always be satisfied on every
object that is _not_ in the broken set. Formally, for a program $P$ we extend
the signature of $P$ with $\mathit{Br}$ as an additional input and an
additional output. We also write pre and post conditions of the form $(\forall
z\notin\mathit{Br}.\,\rho(z))\land\gamma$ to denote that local conditions are
satisfied everywhere outside the broken set, where $\gamma$ can now use
$\mathit{Br}$. In particular, given the Hoare triple

$\langle\,(\forall
z.\,\rho(z))\land\alpha\,\rangle\;P_{\mathcal{G}}(\overline{x},\,\mathit{ret}\\!:\,\overline{y})\;\langle\,(\forall
z.\,\rho(z))\land\beta\,\rangle$

from Stage 1, we instead prove the following Hoare triple (whose validity
implies the validity of the triple above):

$\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\land\mathit{Br}=\emptyset\,\rangle\;P_{\mathcal{G},\mathit{Br}}(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\land\mathit{Br}=\emptyset\,\rangle$

where $\mathit{Br}$ is a ghost input variable of the type of set of objects
and $P_{\mathcal{G},\mathit{Br}}$ is an augmentation of $P$ with ghost code
that computes the $\mathcal{G}$ maps as well as the $\mathit{Br}$ set
satisfying the postcondition.

$P$ may also call other methods $N$ with bodies $Q$. We similarly extend the
input and output signatures of the called methods and use the broken set to
write appropriate contracts for the methods, introducing triples of the form
$\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha_{N}\,\rangle\;Q_{\mathit{Br}}(\overline{s},\mathit{Br},\,\mathit{ret}\\!:\,\overline{r},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta_{N}\,\rangle$. Again,
$Q_{\mathcal{G},\mathit{Br}}$ is an augmentation of $Q$ with ghost code that
updates $\mathcal{G}$ and $\mathit{Br}$.

For the main method that preserves the data structure property, the broken set
is empty at the beginning and end of the program. However, called methods or
loop invariants can talk about states with nonempty broken sets. We require
the verification engineer to write ghost code that maintains the broken set
accurately. The soundness of this reduction is captured by the following
Proposition:

###### Proposition 3.5.

Let $\alpha$ and $\beta$ be quantifier-free formulae over
$\mathcal{F}\cup\mathcal{G}$ (they cannot mention $\mathit{Br}$). If
$\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\land\mathit{Br}=\emptyset\,\rangle\;P_{\mathcal{G},\mathit{Br}}(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\land\mathit{Br}=\emptyset\,\rangle$ is
valid then $\langle\,(\forall
z.\,\rho(z))\land\alpha\,\rangle\;P_{\mathcal{G}}(\overline{x},\,\mathit{ret}\\!:\,\overline{y})\;\langle\,(\forall
z.\,\rho(z))\land\beta\,\rangle$ is valid, where $P_{\mathcal{G}}$ is the
projection of $P_{\mathcal{G},\mathit{Br}}$ obtained by eliminating the
statements that manipulate $\mathit{Br}$.

The proof of this proposition is similar to the proof of Proposition 3.4,
except that projections only eliminate $\mathit{Br}$. We provide a detailed
argument in our supplementary material in Appendix B.

###  3.5. Stage 3: Eliminating the Universal Quantifier for Well-Behaved
Programs

We consider triples of the form

$\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\,\rangle\;P_{\mathcal{G},\mathit{Br}}(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\,\rangle$

where $P_{\mathcal{G},\mathit{Br}}$ is a program augmented with ghost updates
to the $\mathcal{G}$-fields as well as the $\mathit{Br}$ set, and
$\alpha,\beta$ are quantifier-free formulae that can also mention the fields
in $\mathcal{G}$ and the $\mathit{Br}$ set. In this stage we would like to
eliminate the quantified conjunct entirely and instead ask the engineer to
prove the validity of the triple

$\\{\alpha\\}\;P_{\mathcal{G},\mathit{Br}}(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\\{\beta\\}$

However, the above two triples are not, in general, equivalent (as broken sets
can be manipulated wildly). In this section we define a syntactic class of
_well-behaved_ programs that force the verification engineer to maintain
broken sets correctly, and for such programs the above triple are indeed
equivalent. For example, for a field mutation, well-behaved programs require
the engineer to determine the set of _impacted objects_ where local conditions
may be broken by the mutation. The well-behavedness paradigm then mandates
that the engineer add the set of impacted objects to the broken set
immediately following the mutation statement. Similarly, well-behaved programs
do not allow the engineer to remove an object from the broken set unless they
show that the local conditions hold on that object. The imposition of this
discipline ensures that programmers carefully preserve the meaning of the
broken set (i.e., objects outside the broken set must satisfy local
conditions). This allows for the quantified conjunct in the triple obtained
from Stage 2 to be dropped since it always holds for a well-behaved program.
Let us look at such a program:

###### Example 3.6 (Well-Behaved Sorted List Insertion).

We use the running example (Example 3.1) of insertion into a sorted list. We
consider a snippet where the key $k$ to be inserted lies between the keys of
$x$ and $\mathit{next}(x)$ (which we assume is not $\mathit{nil}$). We ignore
the conditionals that determine $\mathit{next}(x)\neq\mathit{nil}$ and
$\mathit{key}(x)\leq k\leq\mathit{key}(\mathit{next}(x))$ for brevity.

We first relax the universal quantification as described in Stage 2 (Section
3.4) and rewrite the pre and post conditions to
($\forall\,z\notin\mathit{Br}.\,\mathit{LC}(z))\land\mathit{sortedll}(x)\land\mathit{Br}=\emptyset$.
Making the first conjunct implicit, we write the following program that
manipulates the broken set in a well-behaved manner. We show the value of the
broken set through the program in comments on the right:

    pre: $\mathit{sortedll}(x)\land\mathit{Br}=\emptyset$
    post: $\mathit{sortedll}(x)\land\mathit{Br}=\emptyset$
     assert x $\notin$ Br;
     assume LC(x);
     y := x.next;    // {}
     z := new C();
     Br := Br $\cup$ {z}; // {z}
     z.key := k;
     Br := Br $\cup$ {z}; // {z}
     z.next := y;
     Br := Br $\cup$ {z}; // {z}

     z.sortedll := True;
     Br := Br $\cup$ {z}; // {z}
     x.next := z;
     Br := Br $\cup$ {x}; // {x,z}
     z.rank := (x.rank + y.rank)/2;
     Br := Br $\cup$ {z}; // {x,z}
     // x and z satisfy LC
     assert LC(z);
     Br := Br $\setminus$ {z}; // {x}
     assert LC(x);
     Br := Br $\setminus$ {x}; // {}

We depict the statements enforced by the well-behavedness paradigm in pink and
the ghost updates written by the verification engineer in blue. Observe that
the paradigm adds the impacted objects to the broken set after each mutation
and allocation. Determining the impact set of a mutation is nontrivial; we
show how to construct them in Section 4.1. Note also that to remove $x$ from
the broken set we must show $\mathit{LC}(x)$ holds (assert followed by removal
from $\mathit{Br}$). Finally, we see at the beginning of the snippet that if
we show $x\notin\mathit{Br}$ then we can infer that $\mathit{LC}(x)$ holds.
This follows from the meaning of the broken set.

Putting it All Together. The above program corresponds to the program
$P_{\mathcal{G},\mathit{Br}}$ obtained from the Stage 3 reduction, consisting
of ghost updates to the $\mathcal{G}$ maps and $\mathit{Br}$. Since it is
well-behaved and satisfies the contract
$\langle\,\mathit{sortedll}(x)\land\mathit{Br}=\emptyset\,\rangle\;P_{\mathcal{G},\mathit{Br}}\;\langle\,\mathit{sortedll}(x)\land\mathit{Br}=\emptyset\,\rangle$
we can conclude that it satisfies the contract $\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\mathit{sortedll}(x)\land\mathit{Br}=\emptyset\,\rangle\;P_{\mathcal{G},\mathit{Br}}\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\mathit{sortedll}(x)\land\mathit{Br}=\emptyset\,\rangle$.
Using Propositions 3.4 and 3.5 we can project out all augmented code and
conclude that the triple given in Example 3.1 with the user’s original program
and intrinsic specifications is valid! In this way, using FWYB we can verify
programs with respect to intrinsic specifications by verifying augmented
programs with respect to quantifier-free specifications. The latter can be
discharged efficiently in practice using SMT solvers (De Moura and Bjørner,
2008; Barrett et al., 2011) (see Section 3.7).∎

We dedicate the rest of this section to developing the general theory of well-
behaved programs.

### Rules for Constructing Well-Behaved Programs

We define the class of well-behaved programs using a set of rules. We first
introduce some notation.

We distinguish the triples over the augmented programs and quantifier-free
annotations by $\\{\psi_{\mathit{pre}}\\}\,P\,\\{\psi_{\mathit{post}}\\}$,
with $\\{\\}$ brackets rather than $\langle\,\rangle$.
$\vdash\\{\psi_{\mathit{pre}}\\}\,P\,\\{\psi_{\mathit{post}}\\}$ denotes that
a triple is provable. Our theory is agnostic to the underlying mechanism for
proving triples correct (we use the off-the-shelf verification tool Boogie in
our evaluation). However, we assume that the mechanism is sound with respect
to the operational semantics. We denote that a snippet $P$ is well-behaved by
$\vdash_{\mathrm{WB}}P$. We also denote that local conditions hold on an
object $x$ by $\mathit{LC}(x)$.

Figure 2 shows the rules for writing well-behaved programs. We only explain
the interesting cases here.

Mutation. Since mutations can break local conditions, we must grow the broken
set. Let $A$ be a finite set of object-type terms over $x$ such that for any
$z\notin A$, if $\mathit{LC}(z)$ held before the mutation, then it continues
to hold after the mutation. We refer to such a set $A$ as an _impact set_ for
the mutation, and we update $\mathit{Br}$ after a mutation with its impact
set. The impact set may not always be expressible as a finite set of terms,
but this is indeed the case for all the intrinsically defined data structures
we use in this paper. We show how to construct impact sets in Section 4.1.

Allocation. Allocation does not modify the heap on any existing object.
Therefore, we simply update the broken set by adding the newly created object
$x$ (this was also the case in Example 3.6).

Assert LC and Remove. This rule allows us to shrink the broken set once the
verification engineer fixes the local conditions on a broken location. The
snippet assert LC(x); Br := Br$\setminus${x} in Example 3.6 uses this rule.
Informally, the verification engineer is required to show that
$\mathit{LC}(x)$ holds before removing $x$ from $\mathit{Br}$.

Infer LC Outside Br. Recall that for well-behaved programs we know implicitly
that $\forall x\notin\mathit{Br}.\,\rho(x)$ holds. This rule allows us to
instantiate this implicit fact on objects that we can show lie outside the
broken set. The snippet assert x$\notin$Br; assume LC(x) in Example 3.6 uses
this rule.

We show that the above rules are sound for the elimination of the universal
quantifier in Stage 3:

###### Proposition 3.7.

Let $[(M:P);(N_{1}:Q_{1})\ldots,(N_{k}:Q_{k})]$ be a program (which can use
$\mathcal{G}$ and $\mathit{Br}$) such that $\vdash_{\mathrm{WB}}P$ and
$\vdash_{\mathrm{WB}}Q_{i},1\leq i\leq k$. Let $\alpha$ and $\beta$ be
quantifier-free formulae over $\mathcal{F}\cup\mathcal{G}$ which can use
$\mathit{Br}$. If
$\\{\alpha\\}\;P(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\\{\beta\\}$
is valid, then $\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\,\rangle\;P(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\,\rangle$ is valid.

We prove the above proposition by structural induction on the rules in Figure
2. We provide the proof in Appendix B of our supplementary material.

In the above presentation we use only one broken set for simplicity of
exposition. Our general framework allows for finer-grained broken sets that
can track breaks over a partition on the local conditions. For example, in
Section 4.4 we verify deletion in an overlaid data structure consisting of a
linked list and a binary search tree using two broken sets: one each for the
local conditions of the two component data structures.

[Skip/Assignment/Lookup/Return]
⊢_WBs where $s$ is of the form

$\mathsf{skip}$, x:=y, x:=y.f, or $\mathsf{return}$ [Mutation]

⊢{ z ∉A ∧LC(z) ∧x ≠nil } x.f := v { LC(z) } ⊢_WB x.f := v ; Br:= Br∪A

where $A$ is a finite set of location terms over $x$ [Allocation]
⊢_WB x := new C() ; Br:= Br∪{x} [Function Call]
⊢_WB ¯y, Br:= Function(¯x,Br) [Infer LC Outside Br]
⊢_WB if (x ≠nil∧x ∉Br) then assume LC(x) [Assert LC and Remove]
⊢_WB if LC(x) then Br:= Br∖{x} [Composition]

⊢_WB P
⊢_WBQ ⊢_WB P ; Q [If-Then-Else]

⊢_WB P
⊢_WBQ ⊢_WB if cond P else Q

where $\mathit{cond}$ does not mention $\mathit{Br}$ [While]

⊢_WB P ⊢_WB while cond do P

where $\mathit{cond}$ does not mention $\mathit{Br}$

Figure 2. Rules for constructing well-behaved programs. Local condition
formula instantiated at $x$ is denoted by $\mathit{LC}(x)$. The statement
$(\mathsf{if}\,\mathit{cond}\,\mathsf{then}\,S)$ is sugar for
$(\mathsf{if}\,\mathit{cond}\,\mathsf{then}\,S\,\mathsf{else}\,\mathsf{skip})$.

###  3.6. Soundness of FWYB

In this section we state the soundness of the FWYB methodology.

###### Theorem 3.8 (FWYB Soundness).

Let $(\mathcal{G},\mathit{LC},\varphi)$ be an intrinsic definition with
$\mathcal{G}=\\{g_{1},g_{2}\ldots,g_{l}\\}$. Let
$[(M:P);(N_{1}:Q_{1})\ldots,(N_{k}:Q_{k})]$ be an augmented program
constructed using the FWYB methodology such that $\,\vdash_{\mathrm{WB}}P$ and
$\,\vdash_{\mathrm{WB}}Q_{i},\,1\leq i\leq k$, i.e., the programs $P$ and
$Q_{i}$ are well-behaved (according to the rules in Figure 2). Let $\varphi$,
$\psi_{\mathit{pre}}$, and $\psi_{\mathit{post}}$ be quantifier-free formulae
that do not mention $\mathit{Br}$ (but can mention the maps in $\mathcal{G}$).
Finally, let
$[(\hat{M}:\hat{P});(\hat{N_{1}}:\hat{Q_{1}})\ldots,(\hat{N_{k}}:\hat{Q_{k}})]$
be the projected user-level program according to Definition 3.3. Then, if the
triple:

$\\{\varphi\land\psi_{\mathit{pre}}\land\mathit{Br}=\emptyset\\}\;P\;\\{\varphi\land\psi_{\mathit{post}}\land\mathit{Br}=\emptyset\\}$

is valid, then the triple

$\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{l}.\,(\mathit{LC}\land\varphi\land\psi_{\mathit{pre}})\,\rangle\;\hat{P}\;\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{l}.\,(\mathit{LC}\land\varphi\land\psi_{\mathit{post}})\,\rangle$

is valid (according to Definition 3.2).

Informally, the soundness theorem says that given a user-written program, if
we (a) augment it with updates to ghost fields and the broken set only using
the discipline for well-behaved programs, and (b) show that if the broken set
is empty at the beginning of the program it will be empty at the end, then the
original user-written program satisfies the intrinsic specifications on
preservation of the data structure.

The proof of the theorem trivially follows from the soundness of the three
stages. Let us write $P$ as $P_{\mathcal{G},\mathit{Br}}$ to emphasize that
the program contains ghost code that manipulates both the $\mathcal{G}$ maps
and $\mathit{Br}$. We begin with the fact that
$\\{\varphi\land\psi_{\mathit{pre}}\land\mathit{Br}=\emptyset\\}\;P_{\mathcal{G},\mathit{Br}}\;\\{\varphi\land\psi_{\mathit{post}}\land\mathit{Br}=\emptyset\\}$
is valid. Since $P$ and its auxiliary functions are well-behaved we have from
Proposition 3.7 that $\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\varphi\land\psi_{\mathit{pre}}\,\rangle\;P_{\mathcal{G},\mathit{Br}}\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\varphi\land\psi_{\mathit{post}}\,\rangle$
is valid.

Next, we use Proposition 3.5 to conclude that $\langle\,(\forall
z.\,\rho(z))\land\varphi\land\psi_{\mathit{pre}}\,\rangle\;P_{\mathcal{G}}\;\langle\,(\forall
z.\,\rho(z))\land\varphi\land\psi_{\mathit{post}}\,\rangle$ is valid, where
$P_{\mathcal{G}}$ is the projection of $P_{\mathcal{G},\mathit{Br}}$ obtained
by eliminating the statements that manipulate $\mathit{Br}$. Finally, we use
Proposition 3.4, along with the fact that $\forall z.\,\rho(z)$ is
$\mathit{LC}$ and $\hat{P_{\mathcal{G}}}$ is the same as $\hat{P}$ to conclude
that
$\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{l}.\,(\mathit{LC}\land\varphi\land\psi_{\mathit{pre}})\,\rangle\;\hat{P}\;\langle\,{\mathbf{\exists}\\!\\!\\!\exists}\,g_{1},g_{2}\ldots,g_{l}.\,(\mathit{LC}\land\varphi\land\psi_{\mathit{post}})\,\rangle$
is valid444The presentation of FWYB augments the original program $P$ with
manipulations to $\mathcal{G}$ and $\mathit{Br}$ in separate stages. This is
done for clarity of exposition. This may not be possible in general since we
may write ghost code with expressions that use both the $\mathcal{G}$ maps and
$\mathit{Br}$. However, we can combine the proofs of Propositions 3.4 and 3.5
to show the soundness of projecting out all ghost code in a single stage, and
Theorem 3.8 continues to hold in the general case..∎

###  3.7. Generating Quantifier-Free Verification Conditions

We state at several points in this paper that verifying augmented programs
with quantifier-free specifications reduces to validity over combinations of
quantifier-free theories. However, this is not obvious. Unlike scalar
programs, quantifier-free contracts do not guarantee quantifier-free
verification conditions (VCs) for heap programs. In particular, commands such
as allocation and function calls pose challenges. However, we show that in our
case it is indeed possible to obtain quantifier-free VCs. We do this by
transforming a given heap program into a scalar program that explicitly models
changes to the heap. We model allocation using a ghost set $\mathit{Alloc}$
corresponding to the allocated objects and update it when a new object is
allocated. We reason about arbitrary changes to the heap across a function
call by requiring a ‘modifies’ annotation from the user and adding assumptions
that the fields of objects outside the modified set of a function call remain
the same across the call. We express these assumptions using parameterized map
updates which are supported by the generalized array theory (de Moura and
Bjørner, 2009). We detail this reduction in our supplementary material in
Appendix A.3.

##  4\. Illustrative Data Structures and Verification

Intrinsic definitions and the fix-what-you-break verification methodology are
new concepts that require thinking afresh about data structures and annotating
methods that operate over them. In this section, we present several classical
data structures and methods over them, and illustrate how the verification
engineer can write intrinsic definitions (which maps to choose, and what the
local conditions ensure) and how they can fix broken sets to prove programs
correct.

###  4.1. Insertion into a Sorted List

In this section we present the verification of insertion into a sorted list
implemented in the FWYB methodology in its entirety. Our running example in
Section 3 illustrates the key technical ideas involved in verifying the
program. In this section we present an end-to-end picture that mirrors the
verification experience in practice.

_Data Structure Definition. _ We first revise the definition of a sorted list
(Example 2.6) with a different set of monadic maps. We have the following
monadic maps $\mathcal{G}$— $\mathit{prev}:C\rightarrow C?$,
$\mathit{length}:C\rightarrow\mathbb{N}$,
$\mathit{keys}:C\rightarrow\mathit{Set(Int)}$,
$\mathit{hslist}:C\rightarrow\mathit{Set(C)}$ that model the _previous_
pointer (inverse of next), length of the sorted list, the set of keys stored
in it, and its heaplet (set of locations that form the sorted list)
respectively. We use the length, keys, and heaplet maps to state full
functional specifications of methods. The local conditions are:

(2) $\displaystyle\forall x.\,\mathit{next}(x)\neq\mathit{nil}\Rightarrow$
$\displaystyle(~{}\mathit{key}(x)\leq\mathit{key}(\mathit{next}(x))~{}\land~{}\mathit{prev}(\mathit{next}(x))=x$
$\displaystyle\land~{}\mathit{length}(x)=1+\mathit{length}(\mathit{next}(x))\,\land\,\mathit{keys}(x)=\\{\mathit{key}(x)\\}\cup\mathit{keys}(\mathit{next}(x))$
$\displaystyle\land~{}\mathit{hslist}(x)=\\{x\\}\uplus\mathit{hslist}(\mathit{next}(x))~{})\textrm{\hskip
40.00006pt($\uplus$: disjoint union)}$
$\displaystyle~{}~{}~{}~{}~{}\land~{}\mathit{prev}(x)\neq\mathit{nil}\Rightarrow$
$\displaystyle\mathit{next}(\mathit{prev}(x))=x$
$\displaystyle~{}~{}~{}~{}~{}\land~{}\mathit{next}(x)=\mathit{nil}\Rightarrow$
$\displaystyle(~{}\mathit{length}(x)=1\,\land\,\mathit{keys}(x)=\\{\mathit{key}(x)\\}\,\land\,\mathit{hslist}(x)=\\{x\\}~{})$

The above definition is slightly different from the one given in Example 2.6.
The $\mathit{length}$ map replaces the $\mathit{rank}$ map, requiring
additionally that lengths of adjacent nodes differ by $1$.

The $\mathit{prev}$ map is a gadget we find useful in many intrinsic
definitions. The constraints on $\mathit{prev}$ ensure that the $C$-heaps
satisfying the definition only contain non-merging lists. To see why this is
the case, consider for the sake of contradiction distinct objects
$o_{1},o_{2},o_{3}$ such that
$\mathit{next}(o_{1})=\mathit{next}(o_{2})=o_{3}$. Then, we can see from the
local conditions that we must simultaneously have $\mathit{prev}(o_{3})=o_{1}$
and $\mathit{prev}(o_{3})=o_{2}$, which is impossible. Finally, the
$\mathit{hslist}$ and $\mathit{keys}$ maps represent the heaplet and the set
of keys stored in the sorted list (respectively).

The heads of all sorted lists in the $C$-heap is then defined by the following
correlation formula:

$\varphi(y)\equiv\mathit{prev}(y)=\mathit{nil}.$

_Constructing Provably Correct Impact Sets for Mutations. _ We now instantiate
the rules developed in Section 3.5 for sorted lists. Recall that well-behaved
programs must update the broken set with the impact set of a mutation. Table 1
captures the impact set for each field mutation. Note that the terms denoting
the impacted objects belong to $A_{f}$ only if they do not evaluate to
$\mathit{nil}$.

$x$$y$ $y=$ $\mathit{old}(\mathit{next}(x))$ $z$$w$$\mathit{next}$$\mathit{prev}$$\mathit{prev}$$\mathit{next}$ Figure 3. Reasoning about the set of objects broken by x.next := z. The dashed arrow represents the old $\mathit{next}$ pointer before the mutation. The grey nodes denote objects where local conditions can be broken by the mutation. We see that only $x$ and $y$ may violate $\mathit{next}$ and $\mathit{prev}$ being inverses. Table 1. Table of impact sets corresponding to field mutations for sorted lists (See 2 in Section 4.1). $\mathit{old}(t)$ refers to the value of the term $t$ before the mutation. Terms only belong to the sets if not equal to $\mathit{nil}$. Mutated Field $f$ |  Impacted Objects $A_{f}$
---|---
$x.\mathit{next}$ | $\\{x,\mathit{old}(\mathit{next}(x))\\}$
$x.\mathit{key}$ | $\\{x,\mathit{prev}(x)\\}$
$x.\mathit{prev}$ | $\\{x,\mathit{old}(\mathit{prev}(x))\\}$
$x.\mathit{hslist}$ | $\\{x,\mathit{prev}(x)\\}$
$x.\mathit{length}$ | $\\{x,\mathit{prev}(x)\\}$
$x.\mathit{keys}$ | $\\{x,\mathit{prev}(x)\\}$

Let us consider the correctness of Table 1, focusing on the mutation of
$\mathit{next}$ as an example. Figure 3 illustrates the heap after the
mutation x.next := z. We make the following key observation: the local
constraints $\mathit{LC}(v)$ for an object $v$ refer only to the properties of
objects $v$, $\mathit{next}(v)$, and $\mathit{prev}(v)$ (see 2), i.e., objects
that are at most “one step” away on the heap. Therefore, the only objects that
can be broken by the mutation x.next := z are those that are one step away
from $x$ either via an incoming or an outgoing edge via pointers
$\mathit{next}$ and $\mathit{prev}$. This is a general property of intrinsic
definitions: _mutations cannot immediately affect objects that are far away on
the heap_. 555Note that a mutation can necessitate changes to monadic maps for
an unbounded number of nodes _eventually_ ; however, these are not necessary
immediately. As we fix monadic maps on a broken object, its neighbors could
get broken and need to be fixed, leading to their neighbors breaking, etc.
This can lead to a ripple effect that would eventually require an unbounded
number of locations to be fixed.

In our case, we claim that the impact set contains at most $x$ and
$\mathit{old}(\mathit{next}(x))$. Here’s a proof (see Fig 3): Consider $z$
such that $z\neq\mathit{old}(\mathit{next}(x))$ (as there is no real mutation
otherwise). If $z$ was not broken before the mutation, then it cannot be the
case that $\mathit{prev}(z)=x$. Looking at the local conditions, it is clear
that such a $z$ will remain unbroken after the mutation. Now consider a $w$
not broken before the mutation such that $\mathit{next}(w)=x$. Then it follows
from the local conditions that there can only be one such (unbroken) $w$, and
further $w\neq x$. $w$’s fields are not mutated, and by examining
$\mathit{LC}$, it is easy to see that $w$ will not get broken (as
$\mathit{LC}(v)$ does not refer to $\mathit{next}(\mathit{next}(v))$). The
argument is the same for $w$ such that $\mathit{prev}(x)=w$. Finally, consider
a $y$ not broken before the mutation such that $\mathit{prev}(y)=x$. We can
then see from the local conditions that $y=\mathit{old}(\mathit{next}(x))$,
which is already in the impact set.

The above argument is subtle, but we can automatically check whether impact
sets declared by a verification engineer are correct. The Mutation rule in
Figure 2 characterizes the impact set $A_{next}$ for mutation of the field
$next$ as follows:

$\vdash\;\\{u\neq x\land u\neq\mathit{next}(x)\land\mathit{LC}(u)\land
x\neq\mathit{nil}\\}\;x.\mathit{next}:=z\;\\{\mathit{LC}(u)\\}$

The above says that any location $u$ that is not in the impact set which
satisfied the local conditions before the mutation must continue to satisfy
them after the mutation. We present the formulation for the general case in
our supplementary material in Appendix C. Finally, note that the validity of
the above triple is decidable. In our realization of the FWYB methodology we
prove our impact sets correct by encoding the triple in Boogie (see Section
5.3).

_Macros that Ensure Well-Behaved Programs. _ In Section 3.5 we characterized
well-behaved programs as a set of syntactic rules (Figure 2). We can realize
these restrictions using macros:

  1. (1)

Mut(x,f,v,Br) for each $f\in\mathcal{F}\cup\mathcal{G}$, which represents the
sequence of statements x.f := v; Br := Br U A${}_{\texttt{f}}$(x). Here
A${}_{\texttt{f}}$(x) is the impact set corresponding to the mutation on $f$
on $x$ as given by the table above. This macro is used instead of x.f := v and
automatically ensures that the impact set is added to the broken set.

  2. (2)

NewObj(x,Br), which represents the statements x := new C(); Br := Br U { x }.
This macro is used instead of x := new C() and ensures that any newly
allocated object is automatically added to the broken set.

  3. (3)

AssertLCAndRemove(x,Br), which represents the statements assert LC(x); Br :=
Br \ { x }. This macro is allowed anytime the engineer wants to assert that
$x$ satisfies the local condition, and then remove it from the broken
set.666We extend our basic programming language defined in Figure 1 with an
$\mathsf{assert}$ statement and give it the usual semantics (program reaches
an error state if the assertion is not satisfied, but is equivalent to
$\mathsf{skip}$ otherwise).

  4. (4)

InferLCOutsideBr(x, Br), which represents the statements assert (x $\neq$
nil $\land$ x $\notin$ Br); assume LC(x). This allows the engineer at any
time to assert that $x$ is not in the broken set and assume it satisfies the
local condition.

The above macros correspond to the rules Mutation, Allocation, Assert LC and
Remove, and Infer LC Outside Br respectively. Restricting to the syntactic
fragment that contains the above macros and disallows mutation and allocation
otherwise enforces the _programming discipline_ that ensures well-behaved
programs.

We present the full well-behaved code written using the above macros and
discuss it in our supplementary material in Appendix D.1.

###  4.2. Reversing a Sorted List

We return to lists for another case study: reversing a sorted list. The
purpose of this example is to demonstrate how the fix-what-you-break
philosophy works with iteration/loops. We augment the definition of sorted
linked lists from Case Study 4.1 to make sortedness optional and determined by
predicates that capture sortedness in non-descending order, with
$\mathit{sorted}:C\rightarrow Bool$, and sortedness with non-ascending order,
with $\mathit{rev\\_sorted}:C\rightarrow Bool$. The relevant additions to the
local condition and the impact sets for these monadic maps can be seen below:

$\displaystyle($ $\displaystyle\mathit{next}(x)\neq\mathit{nil}\Rightarrow$
$\displaystyle\mathit{sorted}(x)\Rightarrow(\mathit{key}(x)\leq\mathit{key}(\mathit{next}(x))\land\mathit{sorted}(x)=\mathit{sorted}(\mathit{next}(x)))$
$\displaystyle\land~{}\mathit{rev\\_sorted}(x)\Rightarrow(\mathit{key}(x)\geq\mathit{key}(\mathit{next}(x))$
$\displaystyle\qquad\qquad\qquad\qquad\land~{}\mathit{rev\\_sorted}(x)=\mathit{rev\\_sorted}(\mathit{next}(x))))$

Mutated Field $f$ |  Impacted Objects $A_{f}$
---|---
$\mathit{sorted}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{rev\\_sorted}$ | $\\{x,\mathit{prev}(x)\\}$

We present the full local condition and code in our supplementary material in
Appendix D.3. However, the gist of the method is that we are popping $C$ nodes
off of the front of a temporary list $cur$, and pushing them to the front of a
new reversed list $ret$ repeatedly using a loop. A technique we use to verify
loops using FWYB is to maintain that the broken set contains no nodes or only
a finite number of nodes for which we specify how they are broken. In the case
of this method, $Br$ remains empty, as the loop maintains $cur$ and $ret$ as
two valid lists, not modifying any other nodes. When popping $x$ from $cur$
and adding it to $ret$, in addition to repairing the new $cur$ by setting its
parent pointer to $\mathit{nil}$, we also need to update fields such as
$\mathit{length}$ and $\mathit{keys}$ on $x$, so it satisfies the relevant
local conditions as the new head of the $ret$ list.

###  4.3. Circular Lists

Our next example is circular lists. This example illustrates a neat trick in
FWYB that where we assert that we can reach a special node known as a
_scaffolding_ node, and that in addition to asserting properties on the node
that is given to the method, one can also assert properties on this
scaffolding node. In order to make verification of properties on this
scaffolding node easier, the scaffolding node remains unchanged in the data
structure, and is never deleted. We start with a data structure containing a
pointer $next:C\rightarrow C$ and a monadic map $prev:C\rightarrow C$. We
build on this data structure to define circular lists by adding a monadic map
$last:C\rightarrow C$ where $last(u)$ for any location $u$ points to the last
item in the list, which is the scaffolding node in this case. The scaffolding
node $x$ must in turn point to another node whose $last$ map points to $x$
itself: this ensures cyclicity. We also define monadic maps
$length:C\rightarrow Nat$ and $rev\\_length:C\rightarrow Nat$ to denote the
distance to the $last$ node by following $prev$ or $next$ pointers. The
partial local conditions for $x$ are as below:

$\displaystyle(x=last(x)\Rightarrow last(\mathit{next}(x))=x\land
length(x)=0\land rev\\_length(x)=0)$ $\displaystyle\land{}$
$\displaystyle(x\neq last(x)\Rightarrow last(\mathit{next}(x))=last(x)\land
length(x)=length(\mathit{next}(x))+1$ $\displaystyle\qquad\qquad\quad\land
rev\\_length(x)=rev\\_length(\mathit{prev}(x))+1)$

Here is the gist of inserting a node at the back of a circular list. We are
given a node $x$ such that $\mathit{next}(x)=last(x)$ (at the end of a cycle).
We insert a newly allocated node after $x$, making local repairs there. Then,
in a ghost loop similar to the one in Case Study 4.2, we make appropriate
updates to the $\mathit{length}$ and $\mathit{keys}$ maps, which are not fully
described here, following the $prev$ map until we reach $last(x)$. Like in the
previous case study, we present the full local condition and code in our
supplementary material in Appendix D.4.

###  4.4. Overlaid Data Structure of List and BST

One of the settings where intrinsic definitions shine is in defining and
manipulating an _overlaid data structure_ that overlays a linked list and a
binary search tree. The list and tree share the same locations, and the next
pointer threads them into a linked list while the left, right pointers on them
defines a BST. Such structures are often used in systems code (such as the
Linux kernel) to save space (Lee et al., 2011). For example, I/O schedulers
use an overlaid structure as above, where the list/queue stores requests in
FIFO order while the bst enables faster searching according requests with
respect to a key. While there has been work in verification of memory safety
of such structures (Lee et al., 2011), we aim here to check preservation of
such data structures.

Intrinsic definition over such an overlaid data structure is pleasantly
_compositional_. We simply take intrinsic definitions for lists and trees, and
take the union of the monadic maps and the conjunction of their local
conditions. The only thing that is left is then to ensure that they contain
the same set of locations. We introduce a monadic map
$\textit{bst}\\_\textit{root}$ that maps every node to its root in the bst,
and introduce a monadic map $\textit{list}\\_\textit{head}$ that maps every
node to the head of the list it belong to (using appropriate local
conditions). We then demand that all locations in a list have the same
$\textit{bst}\\_\textit{root}$ and all locations in a tree have the same
$\textit{list}\\_\textit{head}$, using local conditions. We also define
monadic maps that define the bst-heaplet for tree nodes and list-heaplet for
list nodes (the locations that belong to the tree under the node or the list
from that node, respectively) using local conditions. We define a correlation
predicate Valid that relates the head $h$ of the list and root $r$ of the tree
by demanding that the bst-root of $h$ is $r$ and the list-head of $r$ is $h$,
and furthermore, the list-heaplet of $h$ and tree-heaplet of $r$ are equal.
This predicate can be seen here:

$\textit{Valid}\equiv\;\textit{bst}\\_\textit{root}(h)=r\wedge\textit{list}\\_\textit{root}(r)=h\land~{}\textit{list}\\_\textit{heaplet}(h)=\textit{bst}\\_\textit{heaplet}(r)$

We prove certain methods manipulating this overlaid structure correct (such as
deleting the first element of the list and removing it both from the list as
well as the BST). These ghost annotations are mostly compositional— with
exceptions for fields whose mutation impacts the local condition of multiple
components, we fix monadic maps for the BST component in the same way we fix
them for stand-alone BSTs and fix monadic maps for the list component in the
same way we fix them for stand-alone lists. In fact, we maintain two broken
sets, one for BST and one for list, as updating a pointer for BST often does
not break the local property for lists, and vice versa.

_Limitations. _ In modeling the data structures above, we crucially used the
fact that for any location, there is at most one location (or a bounded number
of locations) that has a field pointing to this location. We used this fact to
define an inverse pointer (_prev_ or _parent_ /_p_), which allows us to
capture the impact set when a location’s fields are mutated. Consequently, we
do not know how to model structures where locations can have unbounded
indegree. We could model these inverse pointers using a sequence/array of
pointers, but verification may get more challenging. Data structures with
unbounded outdegree can however be modeled using just a linked-list of
pointers and hence seen as a structure with bounded outdegree.

##  5\. Implementation and Evaluation

###  5.1. Implementation Strategy of IDS and FWYB in Boogie

We implement the technique of intrinsically defined data structures and FWYB
verification in the program verifier Boogie (Barnett et al., 2006). Boogie is
a low-level imperative programming language which supports systematic
generation of verification conditions that are checked using SMT solvers.

We choose Boogie as it is a low-level verification condition generator. We
expect that scalar programs with quantifier-free specifications, annotations,
and invariants, and given our careful modeling of the heap and its
modification across function calls (Section 3.7), reduces to quantifier-free
verification conditions that fall into decidable logics. We further cross-
check that our encodings indeed generate decidable queries by checking the
generated SMT files. Furthermore, a plethora of higher-level languages compile
to Boogie (e.g., VCC and Havoc for C (Cohen et al., 2009; Condit et al.,
2009), Dafny (Leino, 2010) with compilation to .NET, Civl for concurrent
programs (Kragl and Qadeer, 2021), Move for smart contracts (Dill et al.,
2022), etc.). Implementing a technique in Boogie hence shows a pathway for
implementing IDS and FWYB for higher-level languages as well.

_Modeling Fix-What-You-Break Verification in Boogie. _ We model heaps in
Boogie by having a sort $\mathit{Loc}$ of locations and modeling pointers as
maps from $\mathit{Loc}$ to sorts. We implement monadic maps also as maps from
locations to field values. We implement our benchmarks using the _macros_ for
well-behaved programming defined in Section 4.1. We implement allocation with
an $\mathit{Alloc}$ set and heap change across function calls using
parameterized map updates as described in Section 3.7 and our supplementary
material in Appendix A.3.

We ensure that the VCs generated by Boogie fall into decidable fragments, and
there are several components that ensure this. First, note that all
specifications (contracts and invariants) are quantifier-free. Second, pure
functions (used to implement local conditions) are typically encoded using
quantification, but we ensure Boogie inlines them to avoid quantification.
Third, heap updates that are the effect of procedures and set operations for
set-valued monadic maps are modeled using parameterized map updates (de Moura
and Bjørner, 2009), which Boogie supports natively. Finally, we cross-check
that the generated SMT query is quantifier-free and decidable by checking the
absence of statements that introduce quantified reasoning, including exists,
forall, and lambda.

###  5.2. Benchmarks

We evaluate our technique on a variety of data structures and methods that
manipulate them. Our benchmark suite consists of data structure manipulation
methods for a variety of different list and tree data structures, including
sorted lists, circular lists, binary search trees, and balanced binary search
trees such as Red-Black trees and AVL trees. Methods include core
functionality such as search, insertion and deletion. The suite includes an
_overlaid_ data structure that overlays a binary search tree and a linked
list, implementing methods needed by a simplified version of the Linux
deadline IO scheduler (Lee et al., 2011). The contracts for these functions
are complete functional specifications that not only ask for maintenance of
the data structure, but correctness properties involving the returned values,
the keys stored in the container, and the heaplet of the data structure.

###  5.3. Evaluation

Table 2. Implementation and verification of Boogie programs on the benchmarks. The columns give data structure, size of local conditions for capturing the datatructure as number of conjuncts, method, lines of executable code in the method, lines of specification (pre/post), lines of ghost code annotations (invariants/monadic map updates), and verification time in seconds.  Data Structure | $LC$ | Method | LOC+Spec | Verif. | Method | LOC+Spec | Verif.
---|---|---|---|---|---|---|---
Size | +Ann | Time(s) | +Ann | Time(s)
Singly-Linked List | 8 | Append | 4+11+10 | 2.0 | Insert-Back | 6+13+12 | 2.0
Copy-All | 7+8+9 | 2.0 | Insert-Front | 3+13+7 | 2.0
Delete-All | 10+9+16 | 2.0 | Insert | 9+13+23 | 2.0
Find | 4+4+2 | 1.9 | Reverse | 6+8+18 | 2.1
Sorted List | 14 | Delete-All | 10+9+16 | 2.1 | Merge | 11+9+20 | 2.1
Find | 4+4+2 | 1.9 | Reverse | 5+14+22 | 2.1
Insert | 9+16+27 | 2.1 |  |  |
Sorted List (w. $min,max$ maps) | 20 | Concatenate | 6+10+13 | 2.2 | Find-Last | 5+10+9 | 2.0
Circular List | 27 | Insert-Front | 4+12+41 | 2.3 | Delete-Front | 3+12+39 | 2.4
Insert-Back | 5+14+45 | 2.4 | Delete-Back | 3+13+55 | 2.4
Binary Search Tree | 35 | Find | 4+3+5 | 2.0 | Delete | 10+13+30 | 2.8
Insert | 9+12+37 | 2.7 | Remove-Root | 17+15+47 | 3.8
Treap | 37 | Find | 4+3+5 | 2.0 | Delete | 10+13+30 | 3.1
Insert | 19+12+74 | 10.2 | Remove-Root | 24+15+74 | 5.4
AVL Tree | 45 | Insert | 12+12+36 | 5.1 | Find-Min | 5+5+8 | 2.1
Delete | 43+13+62 | 5.3 | Balance | 40+17+95 | 5.0
Red-Black Tree | 48 | Insert | 76+12+203 | 74.1 | Del-L-Fixup | 33+20+93 | 8.9
Delete | 56+13+76 | 5.8 | Del-R-Fixup | 33+20+93 | 7.4
Find-Min | 5+5+8 | 2.1 |  |  |
BST+Scaffolding | 59 | Delete-Inside | 1+24+51 | 4.8 | Remove-Root | 44+31+61 | 10.2
Scheduler Queue (overlaid SLL+BST) | 72 | Move-Request | 4+10+8 | 2.9 | BST-Delete-Inside | 1+29+55 | 4.9
List-Remove-First | 5+13+10 | 2.7 | BST-Remove-Root | 44+36+65 | 15.0

We first evaluate the following two research questions:

RQ1: Can the data structures be expressed using IDS, and can the FWYB
methodology for methods on these structures be expressed in Boogie?

RQ2: Is Boogie with decidable verification condition generation dispatched to
SMT solvers effective in verifying these methods?

As we have articulated earlier, intrinsic definitions and monadic map updates
require a new way of thinking about programs and repairs. We implement the
specifications using monadic maps and local conditions, and the benchmarks
using the well-behavedness macros and ghost updates. We were able to express
all data structures and FWYB annotations for the methods on these structures
for our benchmarks in Boogie (RQ1). Importantly, we were able to write
quantifier-free modular contracts for the auxiliary methods and loop
invariants using the monadic maps and strengthening the contracts using
quantifier-free assertions on broken sets (which may not be empty for
auxiliary methods). We do not prove termination for these methods except for
ghost loops and ghost recursive procedures (termination for latter is required
for soundness). We provide the benchmarks with annotations in a public
repository (Murali et al., 2024a).

Our annotation measures and verification results are detailed in the table in
Table 2, for $42$ methods across $10$ data structure definitions. These
measurements were taken from a machine with an Intel™ Core i5-4460 processor
at 3.20 GHz. We found the verification performance excellent overall (RQ2):
all the methods verify in under 2 minutes, and all but four verify in under 10
seconds. We used the option that sets the maximum number of VC splits to $8$
in Boogie. The times reported for each method are the sum of times taken for
the following steps: verifying that the impact sets are correct (¡3s for all
data structures), generating verification conditions with Boogie, injecting
parametric update implementations, and solving the SMT queries.

Notice that the lines of ghost code written is nontrivial, but these are
typically simple, involving programmatically repairing monadic maps and
manipulating broken sets. In fact, a large fraction ($\sim 60\%$) of ghost
updates in our benchmarks were _definitional updates_ that simply update a
field according to its definition in the local condition. An example is
updating $x.\textit{length}$ to $x.\textit{next}.\textit{length}+1$ for lists.
We believe that the annotation burden can be significantly lowered in future
work by automating such updates. More importantly, note that none of the
programs required further annotations like instantiations, triggers, inductive
lemmas, etc. in order to prove them correct.

RQ3: What is the performance impact of generating decidable verification
conditions?

In order to study this, we implemented the entire benchmark suite described in
Table 2 in Dafny, a higher-level programming language that uses Boogie to
perform its verification. We implemented the data structures and the FWYB
methodology identically in Dafny to the Boogie version.

Even though our annotations are all quantifier-free, Dafny generates Boogie
code where several aspects of the language, in particular allocation and heap
change across function calls, are modeled using _quantifiers_ , resulting in
quantified queries to SMT solvers. The scatter plot on the right shows the
performance of Boogie and Dafny on the benchmarks. The plot clearly strongly
suggests that even though Dafny is able to prove the FWYB-annotated programs
correct, using decidable verification conditions results in much better
performance. We hence believe that implementing program verifiers (such as
Dafny) that exploit the fact that FWYB annotations can be compiled to
annotations in Boogie that result in decidable VCs is a promising future
direction to achieve faster high-level IDS+FWYB frameworks.

##  6\. Related Work

There have been mainly two paradigms to automated verification of programs
annotated with rich contracts written in logic. The first is to restrict the
specification logic so that verification conditions fall into a decidable
logic. The second allows validity of verification conditions to fall into an
undecidable or even an incomplete logic (where validity is not even
recursively enumerable), but support effective strategies nevertheless, using
heuristics, lemma synthesis, and further annotations from the programmer
(O’Hearn, 2012; Reynolds, 2002a; Pek et al., 2014; Nguyen and Chin, 2008;
Jacobs et al., 2011; Piskac et al., 2014; Chin et al., 2007; Chu et al., 2015;
Murali et al., 2022; Ta et al., 2016; Berdine et al., 2005b; Banerjee et al.,
2008b, 2013; Banerjee and Naumann, 2013; Banerjee et al., 2008a; Berdine et
al., 2006; Distefano et al., 2006; Calcagno et al., 2011). In this paper, we
have proposed a new paradigm of predictable verification that calls for
programmers to write a reasonable amount of extra annotations under which
validity of verification conditions becomes decidable. To the best of our
knowledge, we do not know of any other work of this style (where validity of
verification conditions is undecidable but an upfront set of annotations
renders it decidable).

_Decidable Verification. _ There is a rich body of research on decidable
logics for heap verification: first-order logics with reachability (Lev-Ami et
al., 2009), the logic Lisbq in the Havoc tool (Lahiri and Qadeer, 2008),
several decidable fragments of separation logic known (Berdine et al., 2005a;
Piskac et al., 2013) as well as fragments that admit a decidable entailment
problem (Echenim et al., 2021). Decidable logics based on interpreting bounded
treewidth data structures on trees have also been studied, for separation
logics as well as other logics (Madhusudan et al., 2011; Madhusudan and Qiu,
2011; Iosif et al., 2013). In general, these logics are heavily restricted—
the magic wand in separation logic quickly leads to undecidability (Brochenin
et al., 2008), the general entailment problem for separation logic with
inductive predicates is undecidable (Antonopoulos et al., 2014), and validity
of first-order logic with recursive definitions is undecidable and not even
recursively enumerable and does not admit complete proof procedures.

_Validity Checking of Undecidable and Incomplete Logics. _ Heap verification
using undecidable and incomplete logics has been extensively in the
literature. The work on natural proofs (Pek et al., 2014; Löding et al., 2018)
for imperative programs and work on Liquid Types (Rondon et al., 2008) for
functional programs propose such approaches that utilize SMT solvers, but
require extra user help in the form of inductive lemmas to verify programs.
Users need to understand the underlying heuristic SMT encoding mechanisms and
their shortcomings, as well as theoretical shortcomings (the difference
between fixed point and least fixed point semantics of recursive definitions)
in order to provide these lemmas (see (Löding et al., 2018; Murali et al.,
2022, 2023)). In contrast, the user help we seek in this work is upfront ghost
code that updates monadic maps to satisfy local conditions independently of
the heuristics the solvers use. Furthermore, for programs with such
annotations, we assure decidable validation of the associated verification
conditions.

_Monadic Maps. _ Monadic maps have been exploited in earlier work in other
forms for simplifying verification of properties of global structures. In
shape analysis (Sagiv et al., 2002), monadic predicates are often used to
express inductively defined properties of single locations on the heap. In
separation logic, the _iterated separating conjunction operator_ , introduced
already by Reynolds in 2002 (Reynolds, 2002b), expresses local properties of
each location, and is akin to monadic maps. Iterated separation conjunction
has been used in verification, for both arrays as well as for data structures,
in various forms (Müller et al., 2016; Distefano and Parkinson, 2008). The
work on verification using flows (Krishna et al., 2018, 2020b, 2020a; Patel et
al., 2021; Meyer et al., 2022, 2023) introduces predicates based on flows, and
utilizes such predicates in iterated separation formulas to express global
properties of data structures and to verify algorithms such as the concurrent
Harris list. In these works, local properties of locations and proof systems
based on them are explored, but we do not know of any work exploiting monadic
maps for decidable reasoning, which is crucial for predictable verification.
The work by Gyori et al (Gyori et al., 2017) exploits a class of monadic maps
called _linear measures_ that satisfy certain algebraic properties in order to
incrementally maintain and check properties of linked lists at runtime.

_Ghost Code. _ The methodology of writing ghost code is a common paradigm in
deductive program verification (Jones, 2010; Lucas, 1968; Filliâtre et al.,
2016; Reynolds, 1981) and supported by verification tools such as Boogie and
Dafny (Barnett et al., 2006; Leino, 2010). Ghost code involves code that
manipulates auxiliary variables to perform a parallel computation with the
original code without affecting it. Our use of ghost code establishes the
required monadic maps that satisfy local conditions by allowing the programmer
to construct the maps and verify the local conditions using a disciplined
programming methodology. Furthermore, we assure that the original code with
the ghost code results in decidable verification problems, which is a salient
feature not found typically in other contexts where ghost code is used.

##  7\. Conclusions

We introduced intrinsic definitions that eschew recursion/induction and
instead define data structures using monadic maps and local conditions.
Proving that a program maintains a valid data structure hence requires only
maintaining monadic maps and verifying the local conditions on locations that
get broken. Furthermore, verifying that engineer-provided ghost code
annotations are indeed correct falls into decidable theories, leading to a
predictable verification framework.

_Future Work. _ First, it would be useful to develop verification engines for
higher-level languages (like Java (Jacobs et al., 2011), Rust (Lattuada et
al., 2023), and Dafny (Leino, 2010)) that that have native support for
intrinsic definitions and produce verification conditions in decidable
theories that SMT solvers can handle (see RQ3 in Section 5.3). Second, it
would be interesting to see how intrinsic definitions with fix-what-you-break
proof methodology can coexist and exchange information with traditional
recursive definitions with induction-based proof methodology. Third, as
mentioned in Section 5.3, many updates of monadic maps are straightforward
using definitions, and tools that automate this can reduce annotation burden
significantly. Fourth, we are particularly intrigued with the ease with which
intrinsic data structures capture more complex data structures such as
overlaid data structures. Exploring intrinsic definitions for verifying
concurrent and distributed programs that maintain data structures is
particularly interesting. Fifth, intrinsic definitions opens up an entirely
new approach to defining properties of structures that simplify reasoning. We
believe that exploiting intrinsic definitions in other verification contexts,
like mathematical structures used in specifications (e.g., message queues in
distributed programs), parameterized concurrent programs (configurations
modeled as unbounded sequences of states), and programs that manipulate big
data concurrently (like Apache Spark) are exciting future directions. Finally,
it would be interesting to adapt IDS for functional programs. Since functional
data structures are not mutable, ghost fields will always meet local
conditions. However, we may need to _(re-)establish_ rather than _repair_
local conditions, which may require ghost code, e.g., establishing that the
ghost map $\mathit{sorted}$ on a functional list $x$ is true.

## Artifact Availability Statement

We have prepared a publicly available artifact (Murali et al., 2024a)
containing our benchmark suite and a Docker image for reproducing our
evaluation in Section 5.3.

## Acknowledgements

We thank the anonymous reviewers for their valuable feedback. In particular,
we thank one reviewer for pointing out that Boogie supports parameterized map
updates natively; using this feature simplifies the present version of our
paper and artifact. This work is supported in part by a research grant from
Amazon.

## References

  * (1)
  * Antonopoulos et al. (2014) Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, and Joël Ouaknine. 2014.  Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In _Foundations of Software Science and Computation Structures_ , Anca Muscholl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 411–425.
  * Banerjee et al. (2008a) Anindya Banerjee, Mike Barnett, and David A. Naumann. 2008a.  Boogie Meets Regions: A Verification Experience Report. In _Verified Software: Theories, Tools, Experiments_ , Natarajan Shankar and Jim Woodcock (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 177–191.
  * Banerjee and Naumann (2013) Anindya Banerjee and David A. Naumann. 2013.  Local Reasoning for Global Invariants, Part II: Dynamic Boundaries.  _J. ACM_ 60, 3, Article 19 (jun 2013), 73 pages.  https://doi.org/10.1145/2485981
  * Banerjee et al. (2008b) Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008b.  Regional Logic for Local Reasoning about Global Invariants. In _ECOOP 2008 – Object-Oriented Programming_ , Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 387–411.
  * Banerjee et al. (2013) Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2013.  Local Reasoning for Global Invariants, Part I: Region Logic.  _J. ACM_ 60, 3, Article 18 (June 2013), 56 pages.  http://doi.acm.org/10.1145/2485982
  * Barnett et al. (2006) Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006.  Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In _Formal Methods for Components and Objects_ , Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 364–387.
  * Barrett et al. (2011) Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011.  CVC4. In _Computer Aided Verification_ , Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 171–177.
  * Berdine et al. (2005a) Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005a.  A Decidable Fragment of Separation Logic. In _FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science_ , Kamal Lodaya and Meena Mahajan (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 97–109.
  * Berdine et al. (2005b) Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005b.  Symbolic Execution with Separation Logic. In _Programming Languages and Systems_ , Kwangkeun Yi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 52–68.
  * Berdine et al. (2006) Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2006.  Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In _Proceedings of the 4th International Conference on Formal Methods for Components and Objects_ (Amsterdam, The Netherlands) _(FMCO’05)_. Springer-Verlag, Berlin, Heidelberg, 115–137.  https://doi.org/10.1007/11804192_6
  * Brochenin et al. (2008) Rémi Brochenin, Stéphane Demri, and Etienne Lozes. 2008.  On the Almighty Wand. In _Computer Science Logic_ , Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 323–338.
  * Calcagno et al. (2011) Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011.  Compositional Shape Analysis by Means of Bi-Abduction.  _J. ACM_ 58, 6, Article 26 (dec 2011), 66 pages.  https://doi.org/10.1145/2049697.2049700
  * Chin et al. (2007) Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. 2007.  Automated Verification of Shape, Size and Bag Properties. In _Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems_ _(ICECCS ’07)_. IEEE Computer Society, USA, 307–320.  https://doi.org/10.1109/ICECCS.2007.17
  * Chu et al. (2015) Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. 2015.  Automatic Induction Proofs of Data-Structures in Imperative Programs. In _Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Portland, OR, USA) _(PLDI ’15)_. Association for Computing Machinery, New York, NY, USA, 457–466.  https://doi.org/10.1145/2737924.2737984
  * Cohen et al. (2009) Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009.  VCC: A Practical System for Verifying Concurrent C. In _Theorem Proving in Higher Order Logics_ , Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 23–42.
  * Condit et al. (2009) Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer. 2009.  Unifying Type Checking and Property Checking for Low-Level Code.  _SIGPLAN Not._ 44, 1 (jan 2009), 302–314.  https://doi.org/10.1145/1594834.1480921
  * De Moura and Bjørner (2008) Leonardo De Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems_ (Budapest, Hungary) _(TACAS’08)_. Springer-Verlag, Berlin, Heidelberg, 337–340.
  * de Moura and Bjørner (2009) Leonardo de Moura and Nikolaj Bjørner. 2009.  Generalized, efficient array decision procedures. In _2009 Formal Methods in Computer-Aided Design_. IEEE, 45–52.  https://doi.org/10.1109/FMCAD.2009.5351142
  * Dill et al. (2022) David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong. 2022.  Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 183–200.
  * Distefano et al. (2006) Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2006.  A Local Shape Analysis Based on Separation Logic. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Holger Hermanns and Jens Palsberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 287–302.
  * Distefano and Parkinson (2008) Dino Distefano and Matthew Parkinson. 2008.  jStar: Towards Practical Verification for Java.  _Sigplan Notices - SIGPLAN_ 43, 213–226.  https://doi.org/10.1145/1449764.1449782
  * Echenim et al. (2021) Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2021.  Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In _Automated Deduction – CADE 28_ , André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 183–199.
  * Filliâtre et al. (2016) Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. 2016.  The spirit of ghost code.  _Formal Methods in System Design_ 48 (2016), 152–174.
  * Gyori et al. (2017) Alex Gyori, Pranav Garg, Edgar Pek, and P. Madhusudan. 2017.  Efficient Incrementalized Runtime Checking of Linear Measures on Lists. In _2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, March 13-17, 2017_. IEEE Computer Society, 310–320.  https://doi.org/10.1109/ICST.2017.35
  * Iosif et al. (2013) Radu Iosif, Adam Rogalewicz, and Jiri Simacek. 2013.  The Tree Width of Separation Logic with Recursive Definitions. In _Automated Deduction – CADE-24_ , Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21–38.
  * Jacobs et al. (2011) Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011.  VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In _Proceedings of the Third International Conference on NASA Formal Methods_ (Pasadena, CA) _(NFM’11)_. Springer-Verlag, Berlin, Heidelberg, 41–55.
  * Jones (2010) C. B. Jones. 2010.  The Role of Auxiliary Variables in the Formal Development of Concurrent Programs.  In _Reflections on the Work of C.A.R. Hoare_ , A.W. Roscoe, Cliff B. Jones, and Kenneth R. Wood (Eds.). Springer London, London, 167–187.  https://doi.org/10.1007/978-1-84882-912-1_8
  * Kragl and Qadeer (2021) Bernhard Kragl and Shaz Qadeer. 2021.  The Civl Verifier. In _2021 Formal Methods in Computer Aided Design (FMCAD)_. 143–152.  https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23
  * Krishna et al. (2020a) Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies. 2020a.  Verifying Concurrent Search Structure Templates. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ (London, UK) _(PLDI 2020)_. Association for Computing Machinery, New York, NY, USA, 181–196.  https://doi.org/10.1145/3385412.3386029
  * Krishna et al. (2018) Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. 2018.  Go with the flow: compositional abstractions for concurrent data structures.  _Proc. ACM Program. Lang._ 2, POPL (2018), 37:1–37:31.  https://doi.org/10.1145/3158125
  * Krishna et al. (2020b) Siddharth Krishna, Alexander J. Summers, and Thomas Wies. 2020b.  Local Reasoning for Global Graph Properties. In _Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings_ _(Lecture Notes in Computer Science, Vol. 12075)_ , Peter Müller (Ed.). Springer, 308–335.  https://doi.org/10.1007/978-3-030-44914-8_12
  * Lahiri and Qadeer (2008) Shuvendu Lahiri and Shaz Qadeer. 2008.  Back to the Future: Revisiting Precise Program Verification Using SMT Solvers.  _SIGPLAN Not._ 43, 1 (jan 2008), 171–182.  https://doi.org/10.1145/1328897.1328461
  * Lattuada et al. (2023) Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023.  Verus: Verifying Rust Programs Using Linear Ghost Types.  _Proc. ACM Program. Lang._ 7, OOPSLA1, Article 85 (apr 2023), 30 pages.  https://doi.org/10.1145/3586037
  * Lee et al. (2011) Oukseh Lee, Hongseok Yang, and Rasmus Petersen. 2011.  Program Analysis for Overlaid Data Structures. In _Computer Aided Verification_ , Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 592–608.
  * Leino (2010) K Rustan M Leino. 2010.  Dafny: An automatic program verifier for functional correctness. In _International conference on logic for programming artificial intelligence and reasoning_. Springer, 348–370.
  * Lev-Ami et al. (2009) Tal Lev-Ami, Neil Immerman, Thomas Reps, Mooly Sagiv, Siddharth Srivastava, and Greta Yorsh. 2009.  Simulating reachability using first-order logic with applications to verification of linked data structures.  _Logical Methods in Computer Science_ 5 (04 2009).  https://doi.org/10.2168/LMCS-5(2:12)2009
  * Löding et al. (2018) Christof Löding, P. Madhusudan, and Lucas Peña. 2018.  Foundations for natural proofs and quantifier instantiation.  _PACMPL_ 2, POPL (2018), 10:1–10:30.  https://doi.org/10.1145/3158098
  * Lucas (1968) P Lucas. 1968.  _Two constructive realizations of the block concept and their equivalence, IBM Lab_.  Technical Report. Vienna TR 25.085.
  * Madhusudan et al. (2011) P. Madhusudan, Gennaro Parlato, and Xiaokang Qiu. 2011.  Decidable Logics Combining Heap Structures and Data.  _SIGPLAN Not._ 46, 1 (jan 2011), 611–622.  https://doi.org/10.1145/1925844.1926455
  * Madhusudan and Qiu (2011) P. Madhusudan and Xiaokang Qiu. 2011.  Efficient Decision Procedures for Heaps Using STRAND. In _Static Analysis_ , Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 43–59.
  * Meyer et al. (2022) Roland Meyer, Thomas Wies, and Sebastian Wolff. 2022.  A Concurrent Program Logic with a Future and History.  _Proc. ACM Program. Lang._ 6, OOPSLA2, Article 174 (oct 2022), 30 pages.  https://doi.org/10.1145/3563337
  * Meyer et al. (2023) Roland Meyer, Thomas Wies, and Sebastian Wolff. 2023.  Make Flows Small Again: Revisiting the Flow Framework. In _Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I_ (Paris, France). Springer-Verlag, Berlin, Heidelberg, 628–646.  https://doi.org/10.1007/978-3-031-30823-9_32
  * Müller et al. (2016) Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016.  Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In _Computer Aided Verification_ , Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 405–425.
  * Murali et al. (2022) Adithya Murali, Lucas Peña, Eion Blanchard, Christof Löding, and P. Madhusudan. 2022.  Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints.  _Proc. ACM Program. Lang._ 6, OOPSLA2, Article 191 (oct 2022), 30 pages.  https://doi.org/10.1145/3563354
  * Murali et al. (2023) Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan. 2023.  Complete First-Order Reasoning for Properties of Functional Programs.  _Proc. ACM Program. Lang._ 7, OOPSLA2, Article 259 (oct 2023), 30 pages.  https://doi.org/10.1145/3622835
  * Murali et al. (2024a) Adithya Murali, Cody Rivera, and P. Madhusudan. 2024a.  Artifact for “Predictable Verification using Intrinsic Definitions” (v1.0).  https://doi.org/10.5281/zenodo.10963124
  * Murali et al. (2024b) Adithya Murali, Cody Rivera, and P. Madhusudan. 2024b.  Predictable Verification using Intrinsic Defintitions (Technical Report), arXiv 2404.04515.  https://arxiv.org/abs/2404.04515
  * Nelson (1980) Charles Gregory Nelson. 1980.  _Techniques for Program Verification_.  Ph. D. Dissertation. Stanford University, Stanford, CA, USA.  AAI8011683.
  * Nelson and Oppen (1979) Greg Nelson and Derek C. Oppen. 1979.  Simplification by Cooperating Decision Procedures.  _ACM Trans. Program. Lang. Syst._ 1, 2 (oct 1979), 245–257.  https://doi.org/10.1145/357073.357079
  * Nguyen and Chin (2008) Huu Hai Nguyen and Wei-Ngan Chin. 2008.  Enhancing Program Verification with Lemmas. In _Proceedings of the 20th International Conference on Computer Aided Verification_ (Princeton, NJ, USA) _(CAV ’08)_. Springer-Verlag, Berlin, Heidelberg, 355–369.  https://doi.org/10.1007/978-3-540-70545-1_34
  * O’Hearn (2012) Peter W. O’Hearn. 2012.  A Primer on Separation Logic (and Automatic Program Verification and Analysis).  In _Software Safety and Security - Tools for Analysis and Verification_ , Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.). NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33. IOS Press, 286–318.  https://doi.org/10.3233/978-1-61499-028-4-286
  * O’Hearn et al. (2001) Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001.  Local Reasoning About Programs That Alter Data Structures. In _Proceedings of the 15th International Workshop on Computer Science Logic_ _(CSL ’01)_. Springer-Verlag, London, UK, UK, 1–19.  http://dl.acm.org/citation.cfm?id=647851.737404
  * Patel et al. (2021) Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies. 2021.  Verifying Concurrent Multicopy Search Structures.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 113 (oct 2021), 32 pages.  https://doi.org/10.1145/3485490
  * Pek et al. (2014) Edgar Pek, Xiaokang Qiu, and P. Madhusudan. 2014.  Natural Proofs for Data Structure Manipulation in C Using Separation Logic.  _SIGPLAN Not._ 49, 6 (jun 2014), 440–451.  https://doi.org/10.1145/2666356.2594325
  * Piskac et al. (2013) Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013.  Automating Separation Logic Using SMT. In _Proceedings of the 25th International Conference on Computer Aided Verification_ (Saint Petersburg, Russia) _(CAV’13)_. Springer-Verlag, Berlin, Heidelberg, 773–789.  https://doi.org/10.1007/978-3-642-39799-8_54
  * Piskac et al. (2014) Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014.  Automating Separation Logic with Trees and Data. In _Proceedings of the 16th International Conference on Computer Aided Verification_ _(CAV’14)_. Springer-Verlag, Berlin, Heidelberg, 711–728.
  * Qadeer (2023) Shaz Qadeer. 2023.  Boogie Pull Request #669: Monomorphization of polymorphic maps and binders.  https://github.com/boogie-org/boogie/pull/669
  * Reynolds (1981) John C. Reynolds. 1981.  _The craft of programming_.  Prentice Hall.
  * Reynolds (2002a) John C. Reynolds. 2002a.  Separation Logic: A Logic for Shared Mutable Data Structures. In _Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science_ _(LICS ’02)_. IEEE Computer Society, USA, 55–74.
  * Reynolds (2002b) John C. Reynolds. 2002b.  Separation Logic: A Logic for Shared Mutable Data Structures. In _Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science_ _(LICS ’02)_. IEEE Computer Society, USA, 55–74.
  * Rondon et al. (2008) Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008.  Liquid types.  _SIGPLAN Not._ 43, 6 (jun 2008), 159–169.  https://doi.org/10.1145/1379022.1375602
  * Sagiv et al. (2002) Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. 2002.  Parametric Shape Analysis via 3-Valued Logic.  _ACM Trans. Program. Lang. Syst._ 24, 3 (may 2002), 217–298.  https://doi.org/10.1145/514188.514190
  * Ta et al. (2016) Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2016.  Automated Mutual Explicit Induction Proof in Separation Logic. In _FM 2016: Formal Methods_ , John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer International Publishing, Cham, 659–676.  https://doi.org/10.1007/978-3-319-48989-6_40
  * Tinelli and Zarba (2004) Cesare Tinelli and Calogero G. Zarba. 2004.  Combining Decision Procedures for Sorted Theories. In _Logics in Artificial Intelligence_ , Jóse Júlio Alferes and João Leite (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 641–653.

##  Appendix A Details for Section 3

###  A.1. Operational Semantics

$\displaystyle\bot$ $\displaystyle\xrightarrow{*}\bot$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{skip}}(s,O,I)$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{x\,:=\,\mathit{nil}}(s[x\mapsto\mathit{nil}],O,I)$
$\displaystyle(s,O,I)$ $\displaystyle\xrightarrow{x\,:=\,y}(s[x\mapsto
s(y)],O,I)$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{v\,:=\,be}(s[v\mapsto e],O,I)\hskip
30.00005pt\text{where $be$ interprets to $e$ according to $s$ and $I$}$
$\displaystyle(s,O,I)$ $\displaystyle\xrightarrow{y\,:=\,x.f}(s[y\mapsto
I(f,s(x))],O,I)\hskip 5.0pt\text{ if }(f,s(x))\in\mathit{dom}(I)\hskip
50.00008pt\text{(similarly for $v\,:=\,x.d$)}$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{y\,:=\,x.f}\bot\hskip 5.0pt\text{ if
}(f,s(x))\notin\mathit{dom}(I)\hskip 140.00021pt\text{(similarly for
$v\,:=\,x.d$)}$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{x.f\,:=\,y}(s,O,I[(f,s(x))\mapsto s(y)])\hskip
5.0pt\text{ if }(f,s(x))\in\mathit{dom}(I)\hskip 40.00006pt\text{(similarly
for $x.d\,:=\,v$)}$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{x.f\,:=\,y}\bot\hskip 5.0pt\text{ if
}(f,s(x))\notin\mathit{dom}(I)\hskip 140.00021pt\text{(similarly for
$x.d\,:=\,v$)}$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{x\,:=\,\mathsf{new}\;C()}(s[x\mapsto
o],O\cup\\{o\\},I[(f,o)\mapsto\mathit{default}_{f}])$ for some
$o\in\mathbb{N}$ such that $o\notin O$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\overline{r}\,:=\,\mathit{Function}(\overline{t})}(s[\overline{r}\mapsto
s^{\prime}(\overline{n})],O^{\prime},I^{\prime})\hskip 5.0pt\text{ if
}(\emptyset[\overline{m}\mapsto
s(\overline{t})],O,I)\xrightarrow{Q(\overline{m},\,\mathit{ret}:\,\overline{n})}(s^{\prime},O^{\prime},I^{\prime})$
where $Q(\overline{m},\,\mathit{ret}:\,\overline{n})$ is the code of the
method $\mathit{Function}$, with $\overline{m}$ and $\overline{n}$ being the
formal input and output parameters for $Q$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{assume}\,\mathit{cond}}(s,O,I)\hskip
5.0pt\text{ if }\text{$\mathit{cond}$ interprets to $\mathit{True}$ according
to $s$ and $I$}$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{P_{1}\,;\,P_{2}}(s^{\prime\prime},O^{\prime\prime},I^{\prime\prime})\hskip
5.0pt\text{ if }(s,O,I)\xrightarrow{P_{1}}(s^{\prime},O^{\prime},I^{\prime})$
$\displaystyle\hskip 82.00009pt\text{ and
}(s^{\prime},O^{\prime},I^{\prime})\xrightarrow{P_{2}}(s^{\prime\prime},O^{\prime\prime},I^{\prime\prime})\text{
for some }(s^{\prime},O^{\prime},I^{\prime})$ $\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{if}\,\mathit{cond}\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}}(s^{\prime},O^{\prime},I^{\prime})\hskip
5.0pt\text{ if
}(s,O,I)\xrightarrow{\mathsf{assume}\,\mathit{cond}\,;\;P_{1}}(s^{\prime},O^{\prime},I^{\prime})$
$\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{if}\,\mathit{cond}\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}}(s^{\prime},O^{\prime},I^{\prime})\hskip
5.0pt\text{ if
}(s,O,I)\xrightarrow{\mathsf{assume}\,\neg\mathit{cond}\,;\;P_{2}}(s^{\prime},O^{\prime},I^{\prime})$
$\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{while}\,\mathsf{cond}\,\mathsf{do}\,P}(s^{\prime},O^{\prime},I^{\prime})\hskip
5.0pt\text{ if
}(s,O,I)\xrightarrow{\mathsf{assume}\,\mathit{cond}\,;\,P\,;\,\mathsf{while}\,\mathsf{cond}\,\mathsf{do}\,P}(s^{\prime},O^{\prime},I^{\prime})$
$\displaystyle(s,O,I)$
$\displaystyle\xrightarrow{\mathsf{while}\,\mathsf{cond}\,\mathsf{do}\,P}(s,O,I)\hskip
5.0pt\text{ if
}(s,O,I)\xrightarrow{\mathsf{assume}\,\neg\mathit{cond}}(s,O,I)$ Figure 5.
Operational Semantics

We give the formal operational semantics for programs in our language (Figure
1) in Figure 5 below.

Configurations are of the form $(s,O,I)$ where
$O\subset_{\mathit{finite}}\mathbb{N}$ represents the set of allocated
objects, $s$ represents the store and interprets program variables, and $I$
represents the heap and interprets mutable fields in $\mathcal{F}$—including
ghost fields $\mathcal{G}$ when they are used— on $O$ (interpretations are
total). Although formally $s$ and $I$ are a family of functions indexed by the
sorts of the variables (resp. signatures of the maps), we abuse notation and
use $s(x)$ to denote the interpretation of a variable $x$, and similarly
$I(f,o)$ to denote the value of the field $f$ on the object $o$ in the
configuration. We add a sink state $\bot$ to model error.

Our language is safe, (i.e., allocated locations cannot point to un-allocated
locations) and garbage-collected. The operational semantics is the usual one
for such programs. Figure 5 presents a simplified operational semantics
without considering $\mathsf{return}$ statements. The full semantics adds a
marker to signify completion of a procedure. Procedures can only end after
$\mathsf{return}$ statements (we syntactically disallow statements after a
$\mathsf{return}$) or at the end of a program.

The rules for assignments, skip, sequencing, conditionals, and loops are
trivial. De-referencing a variable that does not point to an object (i.e., is
$\mathit{nil}$) leads to the error state $\bot$. Allocation ensures memory
safety by assigning the value of a field $f$ on a newly allocated object to a
constant $\mathit{default}_{f}$. For pointer fields this value is
$\mathit{nil}$. Finally, we define the operational semantics for function
calls using summaries.

###  A.2. Ghost Code

$\displaystyle P\coloneqq$
$\displaystyle\;\;x\,:=\,\mathit{Expr}[\mathit{Var}_{U},\mathcal{F}]\;\;|\;\;y\,:=\,x.f\;\;|\;\;x.f\,:=\,y\;\;|\;\;z\,:=\,\mathsf{new}\;C()$
$\displaystyle\;\;|\;\;\overline{r}\,:=\,\mathit{Func}(\overline{t})\hskip
30.00005pt\overline{r},\overline{t}\text{ are variables in
}\mathit{Var}_{U}\cup\mathit{Var}_{G}$ (Functions can have ghost input/output
parameters) $\displaystyle\;\;|\;\;GP$ (GP are “pure” ghost programs)
$\displaystyle\;\;|\;\;\mathsf{skip}\;\;|\;\;\mathsf{assume}\;\mathit{cond}\;\;|\;\;\mathsf{return}$
$\displaystyle\;\;|\;\;P\,;\,P\;\;|\;\;\mathsf{if}\;\mathit{cond}\;\mathsf{then}\;P\;\mathsf{else}\;P\;\;|\;\;\mathsf{while}\;\mathsf{cond}\;\mathsf{do}\;P\;$
$\displaystyle\mathit{cond}\coloneqq$
$\displaystyle\;\;\mathit{BoolExpr}[\mathit{Var}_{U},\mathcal{F}]$
$\displaystyle GP\coloneqq$
$\displaystyle\;\;a\,:=\,\mathit{Expr}[\mathit{Var}_{U}\cup\mathit{Var}_{G},\mathcal{F}\cup\mathcal{G}]\;\;|\;\;b\,:=\,x.g\;\;|\;\;b\,:=\,x.f$
(Ghost variables can read from both user and ghost variables/maps)
$\displaystyle\;\;|\;\;x.g\,:=\,b\;\;|\;\;x.g\,:=\,y$ (Ghost maps can only be
assigned values from ghost variables)
$\displaystyle\;\;|\;\;\overline{s}\,:=\,\mathit{GhostFunc}(\overline{v})\hskip
20.00003pt\overline{s},\overline{v}\text{ are variables in
}\mathit{Var}_{G},\,\mathit{GhostFunc}\text{ is {always terminating}}$
$\displaystyle\;\;|\;\;\mathsf{skip}\;\;|\;\;GP\,;\,GP\;\;|\;\;\mathsf{if}\;\mathit{Gcond}\;\mathsf{then}\;GP\;\mathsf{else}\;GP$
$\displaystyle\;\;|\;\;\mathsf{while}\;\mathsf{Gcond}\;\mathsf{do}\;GP\;\hskip
10.00002pt\text{loop is {always terminating}}$
$\displaystyle\mathit{Gcond}\coloneqq$
$\displaystyle\;\;\mathit{BoolExpr}[\mathit{Var}_{U}\cup\mathit{Var}_{G},\mathcal{F}\cup\mathcal{G}]$
Figure 6. Grammar of programs with ghost code. $x,y,z$ are user variables
$\mathit{Var}_{U}$, $a,b$ are ghost variables $\mathit{Var}_{G}$,
$f\in\mathcal{F}$ is a user field, and $g\in\mathcal{G}$ is a ghost map.
Notation $\mathit{Expr}[\mathit{Vars},\mathit{Maps}]$ denotes expressions over
the vocabulary given by variables $\mathit{Vars}$ and maps $\mathit{Maps}$,
similarly $\mathit{BoolExpr}[\mathit{Vars},\mathit{Maps}]$ denotes boolean
expressions. Termination for ghost loops and functions can be established in
any way.

In this section we formally define our programming language augmented with
ghost code, as well as the projection of ghost-augmented code to ‘user’ code.

Fix a set of user variables $\mathit{Var}_{U}$ and ghost variables
$\mathit{Var}_{G}$. We already introduced user fields $\mathcal{F}$ and ghost
fields/maps $\mathcal{G}$ in Section 2.2. We define a programming language
over this vocabulary in Figure 6 below. The main aspects to note are: (a)
ghost variables can read from user variables/maps, but the reverse is not
allowed, (b) ghost conditionals and loops must only contain bodies that are
purely ghost, and (c) ghost loops and functions must always terminate. These
choices ensure that ghost variables do not affect the execution of the user
program. We can formalize this claim using the idea of ‘projecting out’ ghost
code and obtaining a pure user program

_Projection that Eliminates Ghost Code. _ Fix a main method $M$ with body
$Q_{0}$. Let $N_{i},1\leq i\leq k$ be a set of auxiliary methods with bodies
$Q_{i}$ that $Q_{0}$ can call. Note that the bodies $Q_{0}$ and $Q_{i}$
contain ghost code. Let us denote a program containing these methods by
$[(M:Q_{0});(N_{1}:Q_{1})\ldots(N_{k}:Q_{k})]$. We then define projection as
follows:

###### Definition A.1 (Projection of Ghost-Augmented Code to User Code).

The projection of the ghost-augmented program
$[(M:Q_{0});(N_{1}:Q_{1})\ldots(N_{k}:Q_{k})]$ is the user program
$[(\hat{M}:\hat{Q_{0}});(\hat{N_{1}}:\hat{Q_{1}})\ldots(\hat{N_{k}}:\hat{Q_{k}})]$
such that:

  1. (1)

The input (resp. output) signature of $\hat{M}$ is that of $M$ with the ghost
input (resp. output) parameters removed. Formally, given a sequence of
parameters $\overline{x}$ with some elements in the sequence marked as
$\mathsf{ghost}$, we can define the projection as the sequence formed by the
non-continguous subsequence of parameters in $\overline{x}$ consisting of non-
ghost parameters.

  2. (2)

$\hat{Q_{0}}$ is derived from $Q_{0}$ by: (a) eliminating all ghost code,
i.e., replacing yields of the nonterminal $\mathit{GP}$ in Figure 6 with
$\mathsf{skip}$, and (b) replacing each non-ghost function call statement of
the form $\overline{r}:=N_{j}(\overline{t})$ with the statement
$\overline{s}:=\hat{N_{j}}(\overline{u})$, where $\overline{u},\overline{s}$
are obtained from $\overline{t},\overline{r}$ by projecting out the elements
corresponding to the ghost parameters in the signature of $N_{j}$. Each
$\hat{Q_{i}}$ is derived from the corresponding $Q_{i}$ by a similar
transformation.

We define this formally as a recursive transformation on the structure of the
grammar of $P$ (ghost-augmented programs) in Figure 6:

$\displaystyle\mathit{Projection}(GP)$ $\displaystyle=\;\mathsf{skip}$
$\displaystyle\mathit{Projection}(\overline{r}\coloneqq\mathit{Func}(\overline{t}))$
$\displaystyle=\;\overline{s}\coloneqq\hat{\mathit{Func}}(\overline{u})$
$\overline{u},\overline{s}$ are obtained from $\overline{t},\overline{r}$ by
projecting out elements corresponding to ghost parameters
$\displaystyle\mathit{Projection}(\mathsf{stmt})$
$\displaystyle=\;\mathsf{stmt}\hskip 10.00002pt\text{for all other
statements}$ $\displaystyle\mathit{Projection}(P_{1};\,P_{2})$
$\displaystyle=\;\mathit{Projection}(P_{1})\,;\,\mathit{Projection}(P_{2})$
$\displaystyle\mathit{Projection}(\mathsf{if}\;\mathit{cond}\;\mathsf{then}\;P_{1}\;\mathsf{else}\;P_{2})$
$\displaystyle=\;\mathsf{if}\;\mathit{cond}\;\mathsf{then}\;\mathit{Projection}(P_{1})\;\mathsf{else}\;\mathit{Projection}(P_{2})$
$\displaystyle\mathit{Projection}(\mathsf{while}\;\mathsf{cond}\;\mathsf{do}\;P)$
$\displaystyle=\;\mathsf{while}\;\mathsf{cond}\;\mathsf{do}\;\mathit{Projection}(P)$

###  A.3. Generating Quantifier-Free Verification Conditions

The FWYB methodology described in previous sections shows that we can soundly
reduce the problem of verifying programs with intrinsic specifications to the
problem of verifying programs (with ghost code) with quantifier-free
contracts. We then argue that we can reason with the latter using combinations
of various quantifier-free theories including sets and maps with pointwise
updates. In this section we detail some subtleties involved in the argument.

It is well-known that we can reason with scalar programs with quantifier-free
contracts by generating quantifier-free verification conditions (which in turn
can be handled by SMT solvers). However, this is not immediately clear for
programs that dynamically manipulate heaps. In particular, commands such as
allocation and function calls pose challenges in formulating quantifier-free
verification conditions.

At a high level, our solution transforms the given heap program into a scalar
program that explicitly encodes changes to the heap. Specifically, we show an
encoding for the field mutation, allocation, and function call statements.

_Modeling Field Mutation. _ As described earlier, we model the monadic maps
and fields as updatable maps (de Moura and Bjørner, 2009). Formally, we
introduce a map $M_{f}$ (also called an _array_ in SMT solvers like Z3 (De
Moura and Bjørner, 2008)) for every field/monadic map $f$. We then encode the