1 []{}

# Automating Unrealizability Logic:
Hoare-style Proof Synthesis for Infinite Sets of Programs

Shaan Nagy  University of Wisconsin-MadisonMadison rWisconsin USA ,  Jinwoo
Kim  Seoul National UniversitySeoulRepublic of Korea ,  Loris D’Antoni
University of Wisconsin-MadisonMadison rWisconsin USA and  Thomas Reps
University of Wisconsin-MadisonMadison rWisconsin USA

(Date: August 2023)

###### Abstract.

Unrealizability logic (UL) was proposed by Kim et al. as the first Hoare-style
proof system for proving properties that hold for an infinite set of programs
(defined by a regular tree grammar). The goal of our work is to automate
reasoning and proof generation for UL. A key ingredient in UL is the notion of
_nonterminal summaries_ —inductive facts that characterize recursive
nonterminals in the grammar that defines the set of programs. They are
analogous to procedure summaries in Hoare logic. The goal of automating UL led
us to reformulate the inference rules—in particular, introducing a unified
rule for nonterminal summaries, called the rule of adaptation, which draws
inspiration from how procedure summaries are handled in Hoare logic. In the
same way that verification conditions can be used to synthesize loop
invariants for Hoare logic proofs, our reformulation of UL reduces the problem
of synthesizing a nonterminal summary to a Syntax-Guided Synthesis problem. We
implement Wuldo, the first checker and synthesizer for UL. Wuldo can express
proofs beyond the reach of existing tools, including proofs that establish how
infinitely many programs behave on infinitely many inputs, and in some cases
Wuldo can even synthesize the needed nonterminal summaries.

††journal: PACMPL††journalvolume: 1††journalnumber: CONF††article:
1††journalyear: 2024††publicationmonth: 1††copyright: none

##  1\. Introduction

For most existing verification techniques, the assumption is that one is
verifying a single program—i.e., the program is given as input to the
verification problem in its entirety. However, several practically motivated
settings lie outside of this assumption. For example, to verify an incomplete
program loaded from an external source, one needs to verify whether all
programs within a possibly _infinite set_ of programs satisfy a desired
property (Mechtaev et al., 2018; D’Antoni, 2023).

##### Verifying Sets of Programs and Proving Unrealizability

This paper works with a logic, called Unrealizability Logic (UL), originally
developed for one such setting that requires knowing whether a property holds
for an infinite set of programs. That is the problem of proving when a
program-synthesis problem is _unrealizable_ —i.e., there does not exist a
program within a given search space that satisfies a given specification. In
program synthesis, one typically searches for a program $s$ in a (possibly
infinite) search space $S$ that satisfies a given property $\phi$.
Unrealizability is the negated version of this problem—one tries to verify
that _for all_ programs in $S$, $\phi$ does not hold (or inversely, that
$\lnot\phi$ holds). Practically, one would rely on unrealizability to show
that a synthesized program is _optimal_ with respect to some metric by showing
that a solution does not exist within the search space of programs with lower
cost (Hu and D’Antoni, 2018); one can also use unrealizability to prune
certain infeasible program paths during symbolic execution and program repair
(Mechtaev et al., 2018). We observe that the query for unrealizability is
exactly what a program-verification query would look like if it were posed
over a set of programs: do all programs $s\in S$ satisfy some specification
$\phi$? Because of this connection between the problems of proving
unrealizability and verifying a set of programs against a specification, we
focus the rest of the paper on unrealizability without loss of generality.

##### Shortcomings of Existing Automated Approaches

While a few techniques have been proposed to automatically prove
unrealizability (Hu et al., 2019, 2020; Kamp and Philippsen, 2021; Kim et al.,
2021), these approaches simply _encode_ the unrealizability problem into
another verification problem for existing verifiers (e.g., verifying a
nondeterministic program (Hu et al., 2019) or solving a set of Constrained
Horn Clauses in (Kim et al., 2021)).

While such approaches have been effective in specific domains (e.g., SyGuS
problems over linear-integer arithmetic), these tools typically have two
shortcomings. First, they are usually tied to specific problem domains, and it
is hard to study the theoretical properties of these approaches (e.g., their
soundness and completeness) because they rely on opaque external solvers.
Second, these tools cannot produce a _proof certificate_ (e.g., a proof tree
as in Hoare logic) that explains exactly _why_ a particular synthesis problem
is unrealizable (i.e., a direct characterization of the collective behavior of
a set of programs). Human- and machine-understandable proof certificates are
important for unrealizability in the same way such certificates are necessary
to increase our trust, understanding, and reusability of the unsatisfiability
proofs produced by SAT/SMT solvers (Barbosa et al., 2023)—e.g., certificates
can be checked for _validity_ using an independent proof checker, and insights
in a proof certificate (e.g., invariants) can be reused in applications built
atop such verifiers.

##### Unrealizability Logic and its Automation Challenges

In response to these shortcomings, Kim et al. (2023) introduced UL, a sound
and (for loop-free programs) relatively-complete1 Hoare-style strongest-
postcondition proof system for reasoning about unrealizability problems, where
the set of programs we want to verify is expressed with a regular-tree grammar
(RTG). We use S-UL to denote this strongest-postcondition logic. UL is based
on the concept of an _unrealizability triple_
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
which states that for _every_ individual program $s\in S$, the Hoare triple
$\\{{P}\\}\>s\>\\{Q\\}$ holds—essentially lifting Hoare logic to sets of
programs. The key ingredient in UL that allows reasoning about infinite sets
of programs is the notion of _nonterminal summaries_ —inductive facts that
characterize recursive nonterminals in the grammar defining the programs $S$.
Nonterminal summaries are analogous to procedure summaries in Hoare logic for
recursive procedures.

Until now, there has been no automated technique that, given a target triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
and perhaps some invariants, generates a proof of unrealizability. This
limitation is not just a matter of sitting down and implementing S-UL; the
rules of S-UL pose several challenges that stand in the way of achieving three
important goals for automating a program logic:

(_i_) Validation: Given a proof certificate, can we automatically and
efficiently validate it? While it is possible to manually write proof
certificates, the inference rules of S-UL introduce many quantifiers and fresh
variables into the predicates appearing in a proof. Reasoning about such
complex predicates is challenging for many tools. We call the problem of
managing the complexity of these introduced objects the predicate-complexity
challenge.

(_ii_) Proof Derivation: Given nonterminal summaries and loop invariants, can
we automatically derive a proof certificate? In Hoare logic, given a set of
loop invariants, one can typically generate verification conditions to check
whether such invariants are powerful enough to derive a complete proof
certificate. Similarly, we would like one to derive complete proof
certificates in UL just from nonterminal summaries (inductive invariants for
recursive nonterminals), a problem for which no immediate solution currently
exists.

(_iii_) Summary/Invariant Generation: Given only the triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
can we automatically synthesize summaries/invariants along with a proof
certificate? For a given verification task in Hoare logic, one can extract
logical constraints that the set of loop invariants must obey. Proof
generation is thus reduced to a collection of invariant-synthesis problems
(Leino, 2016). There is currently no analogue for this approach in UL because
of a chicken-and-egg problem: the structure of a proof (i.e., the inference
rules applied) in many cases is dependent on the form of the summaries
specified (i.e., Sub1, Sub2, and Inv in (Kim et al., 2023)); however, the
structure of the proof is what we would like to use to extract the constraints
that must be obeyed by the summaries/invariants. We call this coupling of
proof structure and summaries the structural challenge. Moreover, the general
form
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
of nonterminal summaries requires synthesis of two formulas to generate a
single fact, and thus the synthesis search space is very large. We call this
obstacle the summary-complexity challenge.

We answers all three questions _positively_ and addresses all three challenges
by providing a new formulation of UL that is amenable to automation, together
with an implementation.

##### An Automation-friendly Unrealizability Logic

In this paper, we introduce a weakest-precondition variant of UL, called W-UL,
motivated by rethinking UL with automation in mind.

Our answers to the two complexity challenges reduce the complexity of logical
conditions and triples for easier verification and/or synthesis.

To address the predicate-complexity challenge, W-UL eliminates the existential
quantifiers that are generated by the rules in S-UL. The W-UL inference rules
instead introduce very few universal quantifiers. Moreover, we demonstrate
that the universal quantifiers introduced can always be moved to the front of
our verification conditions (§6).

To address the summary-complexity challenge, W-UL restricts nonterminal
summaries to be of the form
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}|\kern-2.15277pt\\}$.
Here, the $\boldsymbol{x}$ variables are program variables whose value may
change in $S$, and the $\boldsymbol{z}$ variables are fresh renamings (ghost
variables) that $Q_{S}$ can reference. As remarked in (Kim et al., 2023),
triples of this form are no less expressive than those of the form
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
used in S-UL.

To address the structural challenge, W-UL uses a single rule for handling
nonterminal summaries, called the _rule of adaptation_ , inspired from how
procedure summaries are handled in Hoare logic (Hoare, 2006; Olderog, 1983).
With only a single rule for nonterminals, we can automatically, unambiguously
determine the shape of the proof tree, up to its summaries and invariants.
When one plugs nonterminal summaries into this “proof skeleton,” the rules of
W-UL yield “verification conditions” for checking whether the summaries
complete the proof. (Such proof skeletons can also be constructed in S-UL, but
the process is more complicated.) Moreover, using the “verification
conditions” (in the form of logical implications) that we extract from a proof
skeleton, one can frame the problem of synthesizing summaries as a Syntax-
Guided Synthesis (SyGuS) problem (Alur et al., 2013). This approach allows us
to use SyGuS solvers to synthesize simple nonterminal summaries (and loop
invariants).

##### Contributions

The contributions of our work are as follows:

  * •

A weakest-precondition version of UL (W-UL) that makes parsimonious use of
quantifiers and is amenable for automation while preserving the proving power
of S-UL (§3).111Through communications with the authors of Kim et al. (2023),
we discovered an error in the original paper that makes S-UL incomplete for
program containing loops. In this paper, we observe that the complexity of a
“relatively complete” While rule would likely be quite high, and we give an
alternative, sound but incomplete rule instead. The authors of Kim et al.
(2023) claim to have identified a “relatively complete” noncompositional rule
that they plan to release as a separate corrigendum, but this is irrelevant to
our paper.

  * •

An algorithm that, given an unrealizability triple, loop invariants, and
nonterminal summaries, can automatically generate conditions to check whether
the given inputs are powerful enough to prove the unrealizability triple (§4).

  * •

A proof that the the problem of synthesizing nonterminal summaries and loop
invariants that make a proof valid can be reduced to a Syntax-Guided Synthesis
problem (§5).

  * •

We implemented Wuldo, a checker and synthesizer for W-UL. Wuldo can
automatically check proofs beyond the reach of existing unrealizability-
proving methods while producing checkable proof artifacts (§6).

##  2\. Overview

In this section, we illustrate via a simple example (§2.1) how one can write a
proof of unrealizability in our new logic W-UL (§2.2 and §2.3); how W-UL
allows verification conditions to be generated automatically from nonterminal
summaries (§2.4); and how such conditions can be used to phrase the problem of
synthesizing nonterminal summaries as a syntax-guided-synthesis problem
(§2.5).

###  2.1. An Unrealizable Synthesis Problem

Suppose that our goal is to synthesize an imperative program that operates
over two variables $x$ and $y$, such that when the program terminates, both
variables hold the same value. Formally, we want a program $s$ that satisfies
the Hoare triple $\\{{\textit{true}}\\}\>s\>\\{x=y\\}$.

It is trivial to write such a program in general (e.g., $x:=y$), but let’s
assume for the sake of illustrating unrealizability that we are bound to the
rules of the following example.

###### Example 2.1.

Synthesize a program in the following grammar $BD$ from the start symbol $S$
that has the same semantics as $x:=y$:222 Restricted grammars are often used
to restrict the search space of a synthesis problem (Lee et al., 2018) and can
also emerge when optimizing syntactic quantitative objectives in a synthesis
problem (Hu and D’Antoni, 2018).

$\displaystyle S$ $\displaystyle\mapsto{\mathsf{if}}\ {B}\ {\mathsf{then}}\
{A}\ {\mathsf{else}}\ {S}\mid A$ $\displaystyle B\mapsto y==N$ $\displaystyle
N$ $\displaystyle\mapsto 0\mid N+1$ $\displaystyle A\mapsto x:=N$

The grammar $BD$ describes programs that contain arbitrarily many if-then-else
operations, but where each subprogram is only allowed to assign a constant to
$x$—e.g., programs such as “$(\text{if }y==5\text{ then }x:=5\text{ else
}(\text{if }y==3\text{ then }x:=3\text{ else }x:=2))$.” Because of the
restricted form of this grammar, any program in $L(S)$ (the set of programs
derivable from $S$, sometimes abbreviated as just $S$) can only set the
variable $x$ to a finite set of values—e.g., the set $\\{5,3,2\\}$ for our
example. Equivalently, for a given program in $S$, the final value of $x$ is
bounded. This property implies that no program in $S$ satisfies our target
specification; that is, this synthesis problem is unrealizable.

Proving that this particular synthesis problem is unrealizable is beyond the
capability of existing tools because a proof requires infinitely many
examples. For any specific finite set of inputs $\\{i_{1},\ldots,i_{n}\\}$,
one can construct a program in $S$ which hardcodes the correct outputs on the
input set.

###  2.2. Unrealizability Logic

An unrealizability triple takes the form
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
where $P$ and $Q$ are logical formulas and $S$ denotes a set of programs
encoded by a regular tree grammar. Such a triple is said to hold if, for all
programs $s\in S$, the Hoare triple $\\{{P}\\}\>s\>\\{Q\\}$ holds in the sense
of partial correctness (i.e., when $s$ executes any input state satisfying
$P$, if the program terminates, then the output state satisfies $Q$). In UL,
the pre- and postconditions $P$ and $Q$ are often formulas over vectors of
states—i.e., $x[]$ and $y[]$—rather than individual states—i.e., $x$ and $y$.
By extending the semantics of our programs to act on a vector of states
simultaneously (i.e., by executing the program on all inputs at once), we can
reason about the behavior of programs on an infinite collection of examples.
Putting all of this together, if one can prove that the following UL triple is
valid, then one has a proof that the synthesis problem in Example 2.1 is
unrealizable:

(1) $\\{\kern-2.15277pt|{\forall i.x[i]=0\land
y[i]=i}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|\exists i.x[i]\neq
y[i]|\kern-2.15277pt\\}$

The triple states that every program $s$ in $S$ is incorrect for at least one
input state—i.e, there exists an input $i$ such that executing $s$ on $x=0$
and $y=i$ results in a state where $x\neq y$. Vector states capture this
condition by considering all possible inputs $i$ at once.

###  2.3. Writing Proofs in Unrealizability Logic

Before diving into the proof rules of W-UL, we introduce some notation. We
write
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
where $\Gamma$ is a set of unrealizability triples, to denote that, assuming
all triples in $\Gamma$ hold, we can prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds as well. This notation is useful in inductive arguments that are used to
show that all programs in a grammar satisfy a triple.

Figure 1 illustrates a (sketch of) a W-UL proof tree for the triple in Eqn.
(1).

To prove hypotheses on nonterminals—i.e., properties that are true for all
programs derivable from a nonterminal—we need formulas called nonterminal
summaries that describe the nonterminals’ behaviors. Like loop invariants,
these formulas typically require clever insights. In our example, the summary
$Q_{s}\triangleq\exists n.\forall i.x[i]<n$ appearing in
$\\{\kern-2.15277pt|{x=z}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|\exists
n.\forall i.x[i]<n|\kern-2.15277pt\\}$ will be handy.

The proof in Figure 1 demonstrates a few key features and advantages of W-UL.
The proof proves a useful fact, coded by $Q_{S}$, on our set of programs $S$
by induction. When we make use of this inductive fact, whether in the proof of
said fact or elsewhere, we know to unambiguously apply the Adapt inference
rule (§ 3.2.2). This situation is in sharp contrast with S-UL in which one
needs to choose rules to apply from among several different options (Inv,
Sub1, and Sub2 in (Kim et al., 2023)).

Furthermore, as one can see below, where the Assign-S-UL rule introduces an
existential quantifier in the postcondition, the Assign-W-UL rule only
performs a substitution.

$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
Assign-S-UL
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E\>\\{\kern-2.15277pt|\exists
x^{\prime}.Q[{x^{\prime}}/{x}]\land x=e_{t}|\kern-2.15277pt\\}$

$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E\>\\{\kern-2.15277pt|Q[{e_{t}}/{x}]|\kern-2.15277pt\\}$
Assign-W-UL
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

Replacing the quantifier instantiation with substitution results in logical
formulas that have fewer variables and quantifiers and are thus amenable to
automated reasoning.

$\cdots$ $\cdots$ ApplyHP
$\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
Adapt
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}\vdash\\{\kern-1.72221pt|{\cdots}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
ITE
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}\vdash\\{\kern-1.72221pt|{\cdots}|\kern-1.72221pt\\}\>\text{if
B then A else
S}\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
Weaken
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}\vdash\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>\text{if
B then A else
S}\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
$\cdots$ Weaken
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}\vdash\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}[{e_{t}}/{x}]|\kern-1.72221pt\\}$
Assign
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}\vdash\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>A\equiv
x:=N\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
HP
$\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}|\kern-1.72221pt\\}$
Adapt $\\{\kern-1.72221pt|{\forall
x^{\prime}.{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{S}}}[{x^{\prime}}/{x}][{x}/{z}]\rightarrow
Q[{x^{\prime}}/{x}])}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Weaken $\\{\kern-1.72221pt|{\forall i.x[i]=0\land
y[i]=i}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|Q\equiv\exists i.x[i]\neq
y[i]|\kern-1.72221pt\\}$

Figure 1. Proof tree for Example 2.1 where $Q_{S}=\exists n.\forall i.x[i]<n$,
and
${\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\Gamma_{1}}}=\\{{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{\\{\kern-2.15277pt|{x=z}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}|\kern-2.15277pt\\}}}\\}$
is a _context_ that contains our inductive fact about $S$ for later use. Our
automation algorithms can derive all terms in black when the pre and
postconditions in red—i.e., the nonterminal summaries—are provided. In some
cases, even the summaries in red can be synthesized.

###  2.4. Deriving Proof Structure Without Nonterminal Summaries

In the previous section, we showed a complete proof tree in unrealizability
logic. In this section, we will discuss how to construct such trees
automatically in W-UL.

Given the initial triple in Eqn. (1), to derive the proof tree shown in Figure
1, our algorithm starts by constructing a _proof skeleton_ —i.e., the
derivation tree in Figure 1 but where all the summaries in red are left
unspecified, replaced instead with function symbols over an appropriate set of
variables (e.g., $Q_{S}(a,b,c,d)$). The goal of this initial step is to set
the structure of the proof tree without having to worry about the exact
summaries/invariants that will appear in the proof. In S-UL, proof generation
and choosing invariants / summaries are _coupled_ : e.g., upon applying a HP
rule, one cannot proceed without providing a nonterminal summary. In W-UL the
derivation of a proof structure is fully syntax-directed and _independent_
from the specific summaries—-i.e., by simply looking at the set of programs in
the center of the UL triple, we can determine what inference rules must be
applied to build a valid proof, as noted in §2.3 and §3. To construct a proof
skeleton, we adopt a weakest-precondition approach, substituting $Q$ in the
skeleton and deriving conditions during an Euler tour that visits right-
children before left children, based on syntax-directed applications of W-UL
rules. The key rule that makes this derivation possible is a revised version
of the little-known rule of adaptation used in procedural program verification
(Hoare, 2006; Olderog, 1983).

The only rule in the proof tree that requires us to reason about predicates
that are not syntactically derivable is the Weaken inference rule—which allows
tightening of preconditions and loosening of postconditions. The Weaken rule
allows one to establish that certain conclusions hold when we have proven a
stronger claim. Specifically, Weaken is the only rule that imposes logical
constraints on its conclusion and hypothesis; all other rules in W-UL impose
purely syntactic constraints. These Weaken applications give constraints on
our invariants and summaries. In the example from §2.3, the constraint on
$Q_{S}$ from the lowest Weaken in the tree would be $(\forall i.x[i]=0\land
y[i]=i)\rightarrow(\forall x^{\prime}.Q_{S}(x^{\prime},x,y)\rightarrow
Q[{x^{\prime}}/{x}])$. If these verification conditions are valid, the
summaries are powerful enough to complete this proof. Otherwise, the proof
fails.

For this problem, our tool Wuldo generates a complete proof in under 80
seconds using the theorem prover Vampire (Blanc et al., 2013) when given
$Q_{S}$ is specified as above.

###  2.5. Synthesizing Summaries in W-UL

Our work allows the automatic construction and validation of W-UL proofs when
invariants and summaries are specified. However, because our work provides us
with an explicit set of constraints on the elements that are missing from
verification conditions, we can move beyond checking proofs and actually
synthesize nonterminal summaries and loop invariants—thereby synthesizing a
complete W-UL proof! In particular, discovering the nonterminal summaries and
loop invariant that are needed can be formulated as a SyGuS problem (Alur et
al., 2013) (as discussed in §5). All we need to do is to specify, for each
invariant/summary, a grammar over which the search is to be carried out.

For our running example, we might specify a grammar $G$ for $Q_{S}(x,y,z)$
that generates all existentially quantified formulas over the language of
integer arithmetic with infinite arrays. If we define $\psi(Q_{S})$ to be the
conjunction of our verification conditions, then the SyGuS problem is simply
written as $(G,\psi(Q_{S}))$.

To the best of the authors’ knowledge, no SyGuS synthesizers over the theory
of infinite arrays have been created. However, for triples that do not require
infinite vector-states, one can discharge the corresponding SyGuS problem to a
solver and hope to obtain a summary. In practice, this approach is feasible
when one is able to give a tight enough grammar. Our experiments suggest that,
under ideal conditions, synthesis can be completed within a couple of seconds
(§2.5).

##  3\. Weakest-Precondition Unrealizability Logic

Recall that our goal is to prove triples of the form
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
where $S$ is a partial program over a regular tree grammar (RTG). An RTG is a
grammar with constructors of various arities. A partial program over $G$ is a
set of programs denoted by a program in which some terms are nonterminals from
$G$. Moving forward, all sets of programs will be assumed to be partial
programs over an RTG.

###### Definition 3.1 (Unrealizability Triple).

An _unrealizability triple_ is a triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
where $P$ and $Q$ are predicates, and $S$ is a partial program in some regular
tree grammar (RTG) over $G_{imp}$ (Figure 2) describing a set of programs.
Such a triple is said to hold if, for all programs $s\in S$, the Hoare triple
$\\{{P}\\}\>s\>\\{Q\\}$ holds in the sense of partial correctness (i.e.,
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}\triangleq\forall
s\in S.\\{{P}\\}\>s\>\\{Q\\}$).333We slightly modify the meaning of a Hoare
triple here so that the value of the last evaluated integer expression is
stored in a variable $e_{t}$ and the value of the last evaluated Boolean
expression is stored in a vairable $b_{t}$. Thus, Hoare triples can reason
about the evaluation of expressions with the semantics introduced in (Kim et
al., 2023).

We write the claim that a triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is derivable un W-UL from a context (i.e., a set of triples we assume to be
true) $\Gamma$ as
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
Contexts typically contain inductive facts we require for reasoning about the
behavior of self-referential (recursive) nonterminals.

Statement $\displaystyle S$ $\displaystyle::={{x}\ \mathsf{:=}\
{E}}\mid{S}{\mathsf{;}}\ {S}\mid{\mathsf{if}}\ {B}\ {\mathsf{then}}\ {S}\
{\mathsf{else}}\ {S}\mid\mathsf{while}\;{B}\;\mathsf{do}\;{S}$ IntExpr
$\displaystyle E$ $\displaystyle::=0\mid 1\mid 2\mid\cdots\mid x\mid E+E$
BoolExpr $\displaystyle B$
$\displaystyle::={{\mathsf{true}}}\mid{{\mathsf{false}}}\mid\neg B\mid B\land
B\mid E<E\mid E==E$ Figure 2. The base grammar $\mathit{G_{imp}}$ which
defines the terms over which our inference rules operate.

To prove such claims, W-UL provides the set of inference rules given in Figure
3. W-UL has four kinds of inference rules: (_i_) rules for expressions, (_ii_)
rules for statements, (_iii_) rules for nonterminals (sets of programs), and
(_iv_) structural rules, which do not correspond to a specific program or
grammar construct but allow one to manipulate the pre- and postconditions of a
triple. With these inference rules, W-UL is _sound_ in general and _relatively
complete_ over sets of loop-free programs.

###### Theorem 3.2 (Soundness).

For any predicate $P$, $Q$, and set of programs $S$,
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}\implies\forall
s\in S.\\{{P}\\}\>s\>\\{Q\\}$ in the sense of partial correctness for every
$s\in S$.

###### Theorem 3.3 (Relative Completeness for Sets of Loop-Free Programs).

For any predicate $P$, $Q$, and set of programs $S$, if $S$ is loop-free, then
$\forall s\in
S.\\{{P}\\}\>s\>\\{Q\\}\implies\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.

The proofs of Theorems 3.2 and 3.3 may be found in Supplementary Materials. In
this section, we present an intuitive reading of the inference rules for our
weakest-precondition formulation of unrealizability logic W-UL. An example
proof is given in Figure 1 for reference.

###### Remark 0.

The precondition $P$ and postcondition $Q$ of a triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
are sometimes formulas over vectors of states—i.e., $x[]$ and $y[]$—rather
than individual states—i.e., $x$ and $y$, in which case the semantics of each
program $s$ must be adjusted so that $s$ is applied to each state
simultaneously. S-UL, the original unrealizability logic, introduced these
_vector-states_ to synchronize between multiple examples given to a synthesis
problem; however, the rules listed in Figure 3 are for the single-example
situation only. In practice (e.g., our implementation in §6), W-UL also has a
set of rules extended to support vector-states. Since supporting vector-states
is not the main contribution of this paper, to simplify the presentation we
have chosen to present only the single-example form of the rules. One can find
vectorized versions of the inference rules in Supplementary Materials.

Int
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{i}/{e_{t}}]}|\kern-1.72221pt\\}\>i\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
True
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{{{\mathsf{true}}}}/{b_{t}}]}|\kern-1.72221pt\\}\>{{\mathsf{true}}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
False
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{{{\mathsf{false}}}}/{b_{t}}]}|\kern-1.72221pt\\}\>{{\mathsf{false}}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Var
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{x}/{e_{t}}]}|\kern-1.72221pt\\}\>x\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B\>\\{\kern-1.72221pt|Q[{\neg
b_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ Not
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>\neg
B\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ .
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\>\\{\kern-1.72221pt|R[{e_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>E_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\oplus
e_{t}}/{e_{t}}]|\kern-1.72221pt\\}$ Bin
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\oplus
E_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ .
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B_{1}\>\\{\kern-1.72221pt|R[{b_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>B_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\land
b_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ And
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B_{1}\land
B_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\>\\{\kern-1.72221pt|R[{e_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>E_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\odot
e_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ Comp
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\odot
E_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ Rules for Expressions

$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E\>\\{\kern-1.72221pt|Q[{e_{t}}/{x}]|\kern-1.72221pt\\}$
Assign $\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>{{x}\
\mathsf{:=}\ {E}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>S_{1}\>\\{\kern-1.72221pt|R|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>S_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Seq
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>{S_{1}}{\mathsf{;}}\
{S_{2}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B\>\\{\kern-1.72221pt|(b_{t}\rightarrow
P_{1})\land(\neg b_{t}\rightarrow P_{2})|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{1}}|\kern-1.72221pt\\}\>S_{1}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{2}}|\kern-1.72221pt\\}\>S_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\mathsf{SimpleIf}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>{\mathsf{if}}\ {B}\
{\mathsf{then}}\ {S_{1}}\ {\mathsf{else}}\
{S_{2}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{I}|\kern-1.72221pt\\}\>B\>\\{\kern-1.72221pt|(\neg
b_{t}\rightarrow Q)\land(b_{t}\rightarrow P_{I})|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{I}}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|I|\kern-1.72221pt\\}$
$\mathsf{SimpleWhile}$
$\Gamma\vdash\\{\kern-1.72221pt|{I}|\kern-1.72221pt\\}\>\mathsf{while}\;{B}\;\mathsf{do}\;{S}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Rules for Statements

$\Gamma_{1}\vdash\\{\kern-1.72221pt|{P_{1}}|\kern-1.72221pt\\}\>N_{1}\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$\cdots$
$\Gamma_{1}\vdash\\{\kern-1.72221pt|{P_{n}}|\kern-1.72221pt\\}\>N_{n}\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$x=z\rightarrow\bigwedge\limits_{1\leq j\leq n}P_{j}$ HP
$\Gamma\vdash\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}\in\Gamma$
ApplyHP
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$N$ is a nonterminal Adapt $\Gamma\vdash\\{\kern-1.72221pt|{\forall
y.(Q[{y}/{x}][{x}/{z}]\rightarrow
R[{y}/{x}])}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|R|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{1}}|\kern-1.72221pt\\}\>N_{1}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\cdots$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{n}}|\kern-1.72221pt\\}\>N_{n}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
GrmDisj
$\Gamma\vdash\\{\kern-1.72221pt|{\bigwedge\limits_{j=1}^{n}P_{j}}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Rules for Nonterminals

$P^{\prime}\rightarrow P$ $Q\rightarrow Q^{\prime}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Weaken
$\Gamma\vdash\\{\kern-1.72221pt|{P^{\prime}}|\kern-1.72221pt\\}\>S\>\\{\kern-1.72221pt|Q^{\prime}|\kern-1.72221pt\\}$
Structural Rules

Figure 3. W-UL Inference Rules

###  3.1. Rules for Expressions and Statements

####  3.1.1. Rules for Expressions

Our rules for expressions—that is, constants, right-hand-side variables, and
binary operations, are listed in the top box Rules for Expressions in Figure
3.

Before discussing the rules for expressions, it is useful to understand what
happens when expressions appear in assignments. In Hoare logic, in the rule
for assignments, expressions are directly substituted into formulas, so for
example $\\{Q[{e}/{x}]\\}x:=e\\{Q\\}$ is taken as an axiom. In unrealizability
logic, an assignment $x:=E$ may actually correspond to sets of assignments
with no single value for $e$. To represent these expressions in the language
of our logical conditions, we introduce two reserved variables ($e_{t}$ for
integer-valued expressions and $b_{t}$ for Boolean-valued expressions) into
which expressions’ values are stored when they are evaluated. For example, a
program ${{x}\ \mathsf{:=}\ {5}}$ can be thought of instead as ${{{e_{t}}\
\mathsf{:=}\ {5}}}{\mathsf{;}}\ {{{x}\ \mathsf{:=}\ {e_{t}}}}$. This follows
the convention of (Kim et al., 2023).

The rules to handle constants and right-hand-side occurrences of variables
simply substitute the constant/variable for $e_{t}$ or $b_{t}$ in the
postcondition to derive the precondition.

The inference rules for unary operators transform the postcondition of the
conclusion into the postcondition of the hypothesis by applying the unary
operation to all occurrences of the appropriate expression variable ($e_{t}$
or $b_{t}$)—e.g., see Not in Figure 3, where $b_{t}$ is replaced with $\neg
b_{t}$.

Binary operators are more complicated. To avoid managing multiple copies of
$e_{t}$, we consider an expression $E_{1}\oplus E_{2}$ as the partial program
${{{x_{1}}\ \mathsf{:=}\ {E_{1}}}}{\mathsf{;}}\ {{{e_{t}}\ \mathsf{:=}\
{x_{1}\oplus E_{2}}}}$, where $x_{1}$ is a fresh variable. This approach lets
us hold the value of the left term in an unreferenced variable when we
evaluate the right term. Suppose we specify $E_{1}$, $E_{2}$, and $Q$ and want
to derive a triple of the form
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}\oplus
E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$. We first derive $R$ as the
weakest precondition of $Q[{x_{1}\oplus e_{t}}/{e_{t}}]$ with respect to
$E_{2}$. Then $R$ gives exactly the necessary constraints on $x_{1}$ for $Q$
to hold on $x_{1}\oplus e_{2}$ for any $e_{2}\in E_{2}$. Having obtained $R$,
we find $P$ as the weakest precondition of $R[{e_{t}}/{x_{1}}]$ with respect
to $E_{1}$. Then $P$ is exactly the necessary constraint so that $Q$ holds on
$e_{1}\oplus e_{2}$ for any $e_{1}\in E_{1}$ and $e_{2}\in E_{2}$.

####  3.1.2. Rules for Statements

The rules for statements in $\mathit{G_{imp}}$ are listed in the second box of
Figure 3. Rules for Assign and Seq mirror those from traditional Hoare logic.
However, the rules for statements with control flow (conditionals and while
loops) diverge from their Hoare-logic counterparts because the guards may be
sets of expressions.

If-Then-Else is straightforward when handling only a single state, as in the
rule $\mathsf{SimpleIf}$ presented in Figure 3. If the poststate is to satisfy
$Q$, then it must do so after passing through either the then branch or the
else branch. We generate preconditions $P_{1}$ and $P_{2}$ sufficient to
guarantee $Q$ on each branch. Then we demand that, for every acceptable input,
the guard sends it to a branch through which it can satisfy $Q$. When handling
vector-states, one must account for the possibility that states run through
different branches; we show how to do this in Supplementary Materials.

For loops, the single-state $\mathsf{SimpleWhile}$ rule is given in Figure 3.
The intuition is that, for $I$ to be a loop invariant, whenever $B$ evaluates
to true ($b_{t}=true$) on a prestate in $I$, we should get a poststate
satisfying a condition $P_{I}$ sufficient to recover $I$ after running any
program in $S$. When $B$ is false on such a prestate, we must recover the
desired postcondition $Q$.

The intuition for $\mathsf{SimpleWhile}$ is sensible, but the rule is actually
imprecise. It overapproximates the semantics of sets of loops. Thus W-UL, like
S-UL, is only relatively complete over loop-free programs 1 (Supplementary
Materials).

It turns out that one cannot write a single-state While rule without some
means of tracking programs. Single-state unrealizability triples cannot
guarantee that repeated code (e.g., a loop body or guard) does not change
between executions—an issue called the “shifting-sands problem.”

Suppose that you have two sets of potential guards, $B_{1}\mapsto x=1\mid
x\neq 1$ and $B_{2}\mapsto x=2\mid x\neq 2$. Every single-state
unrealizability triple true on $B_{1}$ also holds on $B_{2}$ because, for each
input, one possible guard sends it to true and the other one sends it to
false. However, we can write loops with the same bodies using these sets of
guards that have vastly different effects.

Although the While rule is incomplete, in general, if a fact can be proven
with the same loop invariant for all possible loops, then the rule given in
Figure 3 suffices to prove it. Furthermore, if finitely many distinct
invariants are needed, one can split the set of loops into pieces and prove
each separately, as in S-UL (Kim et al., 2023). If infinitely many invariants
are needed, neither strategy works.

###  3.2. Rules for Nonterminals and Other Structural Rules

Reasoning about nonterminals (i.e., the constructs that allow us to define
infinite sets of programs) is the key challenge of unrealizability logic (even
for loop-free programs). To reason about the fact that nonterminals are used
recursively in a grammar—i.e., a nonterminal $N$ may be defined in terms of
itself—we introduce nonterminal summaries of the form
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$,
which may be introduced as _inductive facts_ and then proved via _induction_
with the $\mathsf{HP}$ rule.

We define some sets of variables associated to sets of programs for
convenience:

###### Definition 3.4 ($\boldsymbol{x},\boldsymbol{z},$ and $\boldsymbol{y}$
for $S$).

Let $S$ be a set of programs. (_i_) $\boldsymbol{x}$ is the set of program
variables appearing in programs of $S$, as well as $e_{t}$ if the programs in
$S$ are integer expressions and $b_{t}$ if the programs in $S$ are Boolean
expressions. (_ii_) $\boldsymbol{z}$ is a set of fresh ghost variables that
save the values of program variables in $\boldsymbol{x}$ that programs in $S$
can mutate. When the programs in $S$ are integer/Boolean expressions,
$\boldsymbol{z}$ is empty. These ghost variables allow us to recall the
initial values of program variables in our postcondition. (_iii_)
$\boldsymbol{y}$ is a set of fresh variables renaming the program variables in
$\boldsymbol{x}$ whose values can be changed by a program in $S$. When the
programs in $S$ are integer/Boolean expressions, $\boldsymbol{y}$ contains
only a renaming of $e_{t}/b_{t}$. These variables are used to represent
unknown poststates in the precondition. They are effectively the opposite of
ghost variables. For relations between $\boldsymbol{x}$ and $\boldsymbol{z}$
like $\boldsymbol{x}=\boldsymbol{z}$, the relation is applied to the matching
variables of each set. Variables unmatched on either side (e.g., $e_{t}$ and
$b_{t}$) are omitted.

Thus, for $S$ in Example 2.1, $\boldsymbol{x}=\\{x,y\\}$,
$\boldsymbol{z}=\\{x_{z}\\}$, and $\boldsymbol{y}=\\{x_{y}\\}$. Then writing
$\boldsymbol{x}=\boldsymbol{z}$ (i.e., $x=x_{z}$) saves the value of $x$ in
$x_{z}$ for later reference in the summary $Q_{S}$.

Nonterminal summaries contain the key information we need about recursive
nonterminals. Whenever we need to discuss a property of $N$, we use its
summary $Q_{N}$. The next 3 rules HP, ApplyHP, and Adapt relate to proving
correctness of such summaries (see Figure 3). The tightest $Q_{N}$ possible
for a given nonterminal $N$ and the precondition
$\boldsymbol{x}=\boldsymbol{z}$ is called the “most general formula” of $N$
(also called a strongest triple in (Kim et al., 2023)). The most general
formula of $N$ is sufficient to prove all true claims about the set of
programs in $N$ (Kim et al., 2023). Nonterminal summaries are proved in W-UL
by (structural) induction as follows:

####  3.2.1. HP and ApplyHP

To prove a nonterminal summary, we first add the summary we want to prove to
our context as an inductive fact. We then show that the nonterminal’s
production rules satisfy the triple as well, assuming the inductive fact in
the context.

Given a nonterminal $N\mapsto N_{1}\mid\cdots\mid N_{n}$ and writing
$\Gamma_{1}\equiv(\Gamma\cup\\{\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}\\})$,
we give the rule HP in Figure 3. As a shorthand, we often write

$\Gamma_{1}\vdash\\{\kern-2.15277pt|{P_{1}}|\kern-2.15277pt\\}\>N_{1}\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
$\cdots$
$\Gamma_{1}\vdash\\{\kern-2.15277pt|{P_{n}}|\kern-2.15277pt\\}\>N_{n}\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
HP $\Gamma\vdash\\{\kern-2.15277pt|{\bigwedge\limits_{1\leq j\leq
n}P_{j}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
Weaken
$\Gamma\vdash\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$

Of course, one can generalize this rule for arbitrary preconditions beyond
$\boldsymbol{x}=\boldsymbol{z}$. We will not need to do so because one can
precisely encode the semantics of the programs in $N$ as a formula $Q_{N}$
relating prestates $\boldsymbol{z}$ to poststates $\boldsymbol{x}$ (Kim et
al., 2023).

The ApplyHP rule lets us recall/invoke inductive facts from the context
$\Gamma$.

####  3.2.2. Adapt

To make use of summaries of the form
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$,
we need to connect them to the premises we actually want to prove.

In W-UL, this role is fulfilled by a version of the _rule of adaptation_
$\mathsf{Adapt}$ in Figure 3. This rule and several variants originally
appeared in the context of Hoare logic for recursive programs (Hoare, 2006;
Olderog, 1983), but we have appropriated and restricted it to match the
semantics of W-UL. The Adapt rule computes approximate weakest preconditions
from nonterminal summaries
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.

A general summary
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
tells us that a prestate $\sigma$ is mapped to a post-state $\sigma^{\prime}$
by a program in $N$ only if either $\sigma$ does not satisfy $P$ or $\sigma$
satisfies $P$ and $\sigma^{\prime}$ satisfies $Q$ (i.e., $P(\sigma)\rightarrow
Q(\sigma^{\prime})$). So, given a prestate $\sigma$, we can only be certain a
condition $R$ will hold on the poststate if all poststates satisfying the
above relation also satisfy $R$. Quantifying out auxiliary variables
($\boldsymbol{u}$) used only by $P$ and $Q$, yields
$\forall\boldsymbol{y}.((\forall\boldsymbol{u}.(P\rightarrow
Q[{\boldsymbol{y}}/{\boldsymbol{x}}]))\rightarrow
R[{\boldsymbol{y}}/{\boldsymbol{x}}])$. Here $\boldsymbol{x}$ plays the role
of $\sigma$, and $\boldsymbol{y}$ plays that of $\sigma^{\prime}$ (as per
Definition 3.4). In a sense, this formula is the weakest precondition we can
derive for $R$ knowing nothing about $N$ besides the truth of
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
Plugging in $P\equiv\boldsymbol{x}=\boldsymbol{z}$, this simplifies to
$\forall\boldsymbol{y}.(Q_{N}[{\boldsymbol{y}}/{\boldsymbol{x}}][{\boldsymbol{x}}/{\boldsymbol{z}}]\rightarrow
R[{\boldsymbol{y}}/{\boldsymbol{x}}])$.

The $\mathsf{Adapt}$ rule is well-suited for the automation of W-UL for two
reasons: (_i_) applying this single, unambiguous rule for applying nonterminal
summaries in W-UL is more straightforward than trying various combinations of
the set of 3 rules given in S-UL for applying nonterminal summaries (Kim et
al., 2023), and (_ii_) $\mathsf{Adapt}$ only contains a single universal
quantifier in the precondition, which pulls out to the front of our
verification conditions in the single-state setting (§6), adding very limited
complexity to proof checking.

For any recursive nonterminal $N$, there is some formula $Q_{N}$ so that
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
is capable of deriving _any_ valid triple about $N$ by applying
$\mathsf{Adapt}$. In particular, if $Q_{N}=\bigcup_{p\in
N}(\boldsymbol{z},\llbracket{p}\rrbracket(\boldsymbol{z}))$ (i.e., specifies
the precise relation between end states $\boldsymbol{x}$ and $\boldsymbol{z}$
start states), then the set of $\boldsymbol{y}$ on which
$Q_{N}[{y}/{x}][{x}/{z}]$ holds are exactly the possible poststates programs
in $N$ can reach starting from the state $\boldsymbol{x}$.

Together, these three rules let us prove properties of sets of programs.

###### Example 3.5.

Let $N\mapsto 2\mid 2+N$, with $N$’s nonterminal summary $Q_{N}$ defined to be
$(e_{t}\equiv_{2}0)$ (i.e., the output of any program derivable from $N$ is an
even number). Note that $\boldsymbol{x}$ is only $e_{t}$ in this example
because we have only integer expressions with no program variables, and there
are no $\boldsymbol{z}$ variables. Then the proof tree for this triple is
exactly the structure in Figure 4 where $Q_{N}(a)\triangleq a\equiv_{2}0$.

Most of this proof centers around proving the summary $Q_{N}$. To prove the
summary, we load it into our context as an inductive fact (via HP), split the
nonterminal into its productions (also via HP), and apply the rule of
adaptation on the inductive fact whenever we come across $N$.

####  3.2.3. Grammar Disjunction

To handle nonrecursive nonterminals (i.e., nonterminals $N$ where $N$ is not
reachable from itself by following the productions of the grammar), W-UL
contains one additional rule for dealing with nonterminals. The GrmDisj rule
allows one to split a nonterminal into its productions. It is analogous to HP,
except that no inductive fact is introduced. While one could choose to always
use HP and ignore the inductive fact, it is convenient to have GrmDisj to
limit the size of the context.

#### Weaken

Weaken is the only structural rule in W-UL, i.e., a rule with semantic, rather
than syntactic, constraints on the pre- and postconditions of the triples it
is applied to. (Note, we ignore HP by applying our shorthand.) The Weaken rule
of W-UL is as one would expect. It allows for strengthening of the
precondition and weakening of the postcondition. It is most useful when we
need to relax a hypothesis into a desired form (e.g., with loops and recursive
nonterminals). One of the goals of W-UL is to reduce the number of Weaken
rules as much as possible to reduce the conditions that must be checked in a
proof.

###  3.3. Extending to Vector-States

Recall that a _vector-state_ is a (potentially infinite) vector of states on
which a program executes simultaneously. When handling vector-states, we
extend traditional single-state program semantics
$\llbracket{p}\rrbracket_{sing}(\sigma)$ to the semantics for vectors states
$\llbracket{p}\rrbracket_{vs}(\boldsymbol{\sigma})=\langle\llbracket{p}\rrbracket_{sing}(\boldsymbol{\sigma}[1]),\cdots\rangle$
as in (Kim et al., 2023). Vector-states allow us to reason about multiple
input-output examples as well as hyperproperties.

Inference rules for vector-states are presented in detail in Supplementary
Materials, but we summarize the important points here. For non-branching
expressions and statements, the rules are nearly identical to the single-state
rules. We simply need to substitute all entries in a vector state and match
indices appropriately. The rules for handling nonterminals are the same, as is
the Weaken rule. The rules for branching programs become more complicated.
When handling multiple examples with vector-states, one must be careful to
collect the results of evaluation along both branches. For If-Then-Else
statements, we handle this with fresh variables similar to the approach used
for binary operators. For While loops, we provide an overapproximate rule that
proves invariants using the If-Then-Else rule. This While rule suffers from
the same “shifting sands” problem described in § 3.1.2

Identifying a While rule that gives relatively completeness is an open problem
for future work.

##  4\. Generating W-UL Proof Skeletons and Verification Conditions

The main result of this paper is an algorithm for generating proofs in W-UL.
The W-UL proof-generation algorithm is similar to classical program
verification for Hoare logic. Classically, one specifies a target triple along
with loop invariants, and the program verifier generates a set of assertions
called verification conditions (VCs). These VCs are discharged to an automated
theorem prover to determine the validity of the proof.

In our algorithm, we do not require summaries/invariants to be specified
immediately. Instead, we introduce second-order relational variables called
parameters that stand in for them (e.g., $Q_{N}(a,b,c)$). Similarly, we define
parametrized formulas to be formulas that may contain such symbols (e.g.,
$Q_{N}(v,e_{t}+7,v_{z})\land v=5$). This approach gives us the option to
either plug in summaries/invariants (e.g., obtained from some other tool) or
attempt to synthesize them later.

In our first step (Section 4.1), given an unrealizability triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
our algorithm generates a “proof skeleton”—a proof tree whose pre and
postconditions are parametrized formulas—that forms the outline of our proof
(see Fig 4). Our construction is agnostic with respect to loop invariants and
nonterminal summaries. It is even independent of the specific target
conditions $P$ and $Q$ used in the final proof (up to the auxiliary variables
in $Q$), although we will specify $P$ and $Q$ in practice. The ability to
postpone such commitments is not possible with S-UL, in which proof skeletons
and summaries must be generated hand-in-hand.

In the second step (Section 4.2), the algorithm generates a set of
parametrized verification conditions (PVCs)—VCs that are parametrized
formulas. Then, if one substitutes (candidate) loop invariants and nonterminal
summaries for the parameters, the PVCs can be converted to VCs. An automated
theorem prover can then discharge the VCs, determining whether the provided
invariants and summaries are strong enough to prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.

Our algorithm enjoys the following soundness and relative-completeness
guarantees: if the generated set of PVCs can be satisfied by _some_ invariants
and summaries, plugging those invariants and summaries into the skeleton
results in a correct proof; otherwise, if the programs in $S$ are loop-free,
no proof exists (Corollary 4.5). If some programs in $S$ contain loops,
failure to satisfy the VCs does not imply nonexistence of a proof.

###  4.1. Computing a Proof Skeleton

Our first step in proving a triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is to compute a proof skeleton based on $S$. Recall that a proof skeleton is a
proof tree whose pre and posconditions are parametrized formulas—formulas
containing symbols representing the target pre- and postcondition, loop
invariants, and nonterminal summaries. A proof skeleton gives a template for a
complete proof. Moreover, we can easily extract parametrized verification
conditions from the proof skeletons that are created (Section 4.2).

An example proof skeleton is given in Figure 4, where and $Q_{N}(e_{t})$ is a
parameter. This example skeleton is exactly the W-UL proof from Example 3.5
except for the use of parameters in place of unknown formulas.

Int
$\Gamma_{1}\vdash\\{\kern-1.50694pt|{{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(2)}|\kern-1.50694pt\\}\>2\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-1.50694pt\\}$
Int
$\Gamma_{1}\vdash\\{\kern-1.50694pt|{R[{e_{t}}/{x_{1}}][{2}/{e_{t}}]}|\kern-1.50694pt\\}\>2\>\\{\kern-1.50694pt|R[{e_{t}}/{x_{1}}]|\kern-1.50694pt\\}$
ApplyHP
$\Gamma_{1}\vdash\\{\kern-1.50694pt|{True}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-1.50694pt\\}$
Adapt
$\Gamma_{1}\vdash\\{\kern-1.50694pt|{R}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(x_{1}+e_{t})|\kern-1.50694pt\\}$
Bin-Plus
$\Gamma_{1}\vdash\\{\kern-1.50694pt|{R[{e_{t}}/{x_{1}}][{2}/{e_{t}}]}|\kern-1.50694pt\\}\>2+N\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-1.50694pt\\}$
HP
$\emptyset\vdash\\{\kern-1.50694pt|{{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(2)\land
R[{e_{t}}/{x_{1}}][{2}/{e_{t}}]}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-1.50694pt\\}$
Weaken
$\emptyset\vdash\\{\kern-1.50694pt|{True}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-1.50694pt\\}$
Adapt $\emptyset\vdash\\{\kern-1.50694pt|{\forall
e_{t_{y}}.{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t_{y}})\rightarrow
e_{t_{y}}\neq 3}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|e_{t}\neq
3|\kern-1.50694pt\\}$ Weaken
$\emptyset\vdash\\{\kern-1.50694pt|{True}|\kern-1.50694pt\\}\>N\>\\{\kern-1.50694pt|e_{t}\neq
3|\kern-1.50694pt\\}$

Figure 4. Following Example 3.5, we give a proof skeleton for a triple
$\\{\kern-2.15277pt|{True}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|e_{t}\neq
3|\kern-2.15277pt\\}$ where $N\mapsto 2\mid 2+N$. Above, $R$ is an
abbreviation for $\forall
e_{t_{y}}.({\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t_{y}})\rightarrow{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(x_{1}+e_{t_{y}}))$.
Substitution of a second order parameter is taken to be a substitution into
each of its inputs. Note,
$\Gamma_{1}=\\{\\{\kern-2.15277pt|{True}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|{\color[rgb]{0.8203125,0.09765625,0.03125}\definecolor[named]{pgfstrokecolor}{rgb}{0.8203125,0.09765625,0.03125}{Q_{N}}}(e_{t})|\kern-2.15277pt\\}\\}$.
Symbols in red are unspecified parameters.

To generate a proof skeleton, we recurse on the structure of $S$.
Specifically, we define a function $\textit{{w-skel}}(\Gamma,S,Q)$ that takes
as input a set of programs $S$ defined via an RTG as in §3, a context $\Gamma$
whose triples’ postconditions are parametrized formulas, and a postcondition
$Q$ as a parametrized formula. The function w-skel returns a skeleton in the
form of a proof tree in which each node $n$ is labeled with a derivation rule
$\textit{rule}(n)$, and each pre and postcondition is a parametrized formula.

Note that w-skel does not take the precondition $P$ as input—a parametrized
precondition is generated by constructing the skeleton. The output is
essentially a proof skeleton for proving the weakest precondition of $S$ with
respect to $Q$. When a proof skeleton is returned, we can simply apply Weaken
to recover
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.

To simplify matters, the version of the algorithm that we present operates
over single-state inference rules. The extension to vector-states is
straightforward: the vector-state rules for handling nonterminals are
identical to the single-state rules, so very little of the algorithm changes.

####  4.1.1. Weakest Skeleton

We define a function w-skel (standing for weakest skeleton) that operates
recursively over $S$. We describe next what happens in each possible case. We
encourage readers to follow along in Figure 4.

##### Case 1: $S=op(S_{1},\ldots,S_{k})$ where $op$ is a constructor from
$G_{Imp}$ other than While (e.g., $+$, true, if-then-else).

We apply the inference rule corresponding to $op$. We call w-skel recursively
on its hypotheses, working right to left. Each hypothesis takes parametrized
postconditions as dictated by the inference rule, where substitutions
$[{b}/{a}]$ on a parameter are applied to each of the parameter’s inputs. The
hypotheses’ skeletons are the children of the application of the inference
rule $op$. The precondition of the conclusion is as dictated by the inference
rule.

In Figure 4, the instance of inference rule Bin-Plus is covered by this case.
Here, the set of programs in the middle position of the triple in the
conclusion is given by $2+N$. We apply Bin-Plus, computing proof skeletons for
the hypotheses, and transforming parameterized conditions as specified by the
inference rules. For binary (and ternary) inference rules, we must generate
the hypotheses’ skeletons in order from right to left. Letting $R$ stand for
the parametric precondition of the skeleton for $N$, the parametric formula
$R[{e_{t}}/{x_{1}}]$ becomes the parametric postcondition for the skeleton for
$2$.

$\textit{{w-skel}}(\Gamma_{1},2,R[{e_{t}}/{x_{1}}])$
$\textit{{w-skel}}(\Gamma_{1},N,{Q_{N}}(x_{1}+e_{t}))$ Bin-Plus
$\Gamma_{1}\vdash\\{\kern-2.15277pt|{R[{e_{t}}/{x_{1}}][{2}/{e_{t}}]}|\kern-2.15277pt\\}\>2+N\>\\{\kern-2.15277pt|{Q_{N}(e_{t})}|\kern-2.15277pt\\}$

##### Case 2: $S=\mathsf{while}\;{B}\;\mathsf{do}\;{S_{1}}$

If $S$ is a while loop, then apply the While rule with a fresh invariant
parameter $I_{S}(\boldsymbol{x},\boldsymbol{v})$. Derive the skeleton of the
body hypothesis by invoking w-skel recursively with parametric postcondition
$I_{S}(\boldsymbol{x},\boldsymbol{v})$, where $\boldsymbol{x}$ are the
variables appearing in the loop (as per Definition 3.4) and $\boldsymbol{v}$
are the free variables of $Q$ which are not in $\boldsymbol{x}$. For the guard
hypothesis, substitute the parametric precondition of the body hypothesis for
$P_{I_{S}}$ in $(\neg b_{t}\rightarrow Q)\land(b_{t}\rightarrow P_{I_{S}})$
and recursively generate a skeleton for $B$ with this postcondition. Then
apply Weaken to prove
$\\{\kern-2.15277pt|{I_{S}(\boldsymbol{x},\boldsymbol{v})}|\kern-2.15277pt\\}\>B\>\\{\kern-2.15277pt|(\neg
b_{t}\rightarrow Q)\land(b_{t}\rightarrow P_{I_{S}})|\kern-2.15277pt\\}$, the
guard hypothesis of the While application.

$\textit{{w-skel}}(\Gamma,B,(\neg b_{t}\rightarrow Q)\land(b_{t}\rightarrow
P_{I_{S}}))$ Weaken
$\Gamma\vdash\\{|I_{S}(\boldsymbol{x},\boldsymbol{v})|\\}B\\{|(\neg
b_{t}\rightarrow Q)\land(b_{t}\rightarrow P_{I_{S}})|\\}$
$\textit{{w-skel}}(\Gamma,S,I_{S}(\boldsymbol{x},\boldsymbol{v}))$ Single-
While
$\Gamma\vdash\\{\kern-2.15277pt|{I_{S}(\boldsymbol{x},\boldsymbol{v})}|\kern-2.15277pt\\}\>\text{while
}B\text{ do }S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

##### Case 3: $S\mapsto S_{1}\mid\cdots\mid S_{n}$, where $S$ is a Non-
Recursive Nonterminal

If $S$ is non-recursive (i.e., it does not appear in any of its own
productions nor in their expansions), apply GrmDisj. Construct proof skeletons
recursively for each production of $S$ with the same postcondition. The
precondition of the conclusion is $\bigwedge\limits_{j=1}^{n}P_{n}$, the
conjunction of the parametrized preconditions derived for the hypotheses.

$\textit{{w-skel}}(\Gamma,S_{1},Q)$ $\cdots$
$\textit{{w-skel}}(\Gamma,S_{n},Q)$ GrmDisj
$\Gamma\vdash\\{\kern-2.15277pt|{\bigwedge\limits_{j=1}^{n}P_{j}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

##### Case 4: $S$ is a Recursive Nonterminal

If $S$ is recursive, we have two subcases.

First, if a triple
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$
exists in the context $\Gamma$, close off this branch of the proof skeleton by
using ApplyHP and Adapt as shown in the following proof-skeleton fragment:

ApplyHP
$\Gamma\vdash\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$
Adapt
$\Gamma\vdash\\{\kern-2.15277pt|{\forall\boldsymbol{y}.Q_{S}(\boldsymbol{y},\boldsymbol{x})\rightarrow
Q[{\boldsymbol{y}}/{\boldsymbol{x}}]}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

Otherwise we hit our second subcase and apply the HP rule with a postcondition
$Q_{S}$ and construct proof skeletons of its hypotheses. Define
$\boldsymbol{x}$ and $\boldsymbol{z}$ of $S$ as in Definition 3.4 so that
$\boldsymbol{x}$ captures the program variables in $S$ (plus $e_{t}/b_{t}$ if
$S$ is a set of integer/boolean expression) and $\boldsymbol{z}$ gives fresh
ghost variables for all program variables mutated by programs in $S$. Take the
inductive fact to be
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$.
This construction follows the convention from §3.2.

Now apply Adapt to
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$
to complete the skeleton. Note that $\Gamma_{1}$ denotes
$\Gamma\cup\\{\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S_{1}\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}\\}$
below. The parametrized preconditions of HPs hypotheses are denoted by
$P_{1},\cdots,P_{n}$. See the first application of Adapt in Figure 4 for a
further example.

$\textit{{w-skel}}(\Gamma_{1},S_{1},Q_{S}(\boldsymbol{x},\boldsymbol{z}))$
$\cdots$
$\textit{{w-skel}}(\Gamma_{1},S_{n},Q_{S}(\boldsymbol{x},\boldsymbol{z}))$ HP
$\Gamma\vdash\\{\kern-2.15277pt|{\bigwedge\limits_{j=1}^{n}P_{j}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$
Weaken
$\Gamma\vdash\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q_{S}(\boldsymbol{x},\boldsymbol{z})|\kern-2.15277pt\\}$
Adapt
$\Gamma\vdash\\{\kern-2.15277pt|{\forall\boldsymbol{y}.Q_{S}(\boldsymbol{y},\boldsymbol{x})\rightarrow
Q[{\boldsymbol{y}}/{\boldsymbol{x}}])}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

####  4.1.2. Connecting the Weakest Skeleton to the Precondition $P$

Our proof skeleton is almost complete, but it does not yet mention the
precondition $P$. What we have given is a proof skeleton for proving the
weakest precondition of $Q$ with respect to $S$. The final step to produce a
complete proof skeleton for
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is to Weaken the conclusion of the skeleton produced by
$\textit{{w-skel}}(\emptyset,S,Q)$ to connect it to precondition $P$. After
applying this final Weaken, the proof skeleton is complete.

$\textit{{w-skel}}(\emptyset,S,Q)$ Weaken
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

We call this final skeleton $\textit{{p-skel}}(\emptyset,P,S,Q)$.

By Theorem 4.1 below, any true fact over sets of loop-free programs has a
proof with the same structure as the skeleton we generate:

###### Theorem 4.1.

If
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
for conditions $P$ and $Q$, and a set of loop-free programs $S$, then there
exists a proof of
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
which adheres to the proof skeleton $\textit{{p-skel}}(\emptyset,P,S,Q)$.

This result follows from the constructive proof of relative completeness for
loop-free programs given in the Supplementary Materials. An analogous result
holds for nonempty contexts $\Gamma$, but that will not be relevant for us.

###  4.2. Computing Verification Conditions

After running the algorithm in §4.1, we have a proof skeleton
$\textit{{p-skel}}(\Gamma,P,S,Q)$ as in Figure 4.

In this section, we show how to generate (parametrized) verification
conditions (PVCs) from a proof skeleton. PVCs give exactly the constraints on
our summaries and invariants needed to construct a valid proof. In terms of
the example from Figure 4, the PVCs tell us when supplied predicates $P$, $Q$,
and $Q_{N}$ make the concrete proof tree a valid one in W-UL.

For a proof tree to be valid, all nodes in the tree must correctly follow the
syntactic and semantic restrictions of the corresponding W-UL inference rules.
Because of how we generate proof skeletons, all syntactic restrictions the
rules impose are satisfied. (In fact, the proof-skeleton algorithm uses these
syntactic relations to propagate parametrized postconditions through the
tree.)

The only rule applications that are not guaranteed to be valid W-UL rules by
construction are the applications of Weaken. Weaken is the only rule with
semantic restrictions on its logical conditions. Because no Weaken
applications in our proof skeleton change the postcondition from the
conclusion to the hypothesis, we need only check implication of the
preconditions (see Figure 3).

###### Definition 4.2 (Parametrized Verification Conditions).

Given an application $A$ of the Weaken rule of the following form:

$\Gamma\vdash\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
Weaken
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$

$PVC(A)$ denotes the parameterized formula $\forall\boldsymbol{v}.P\rightarrow
P^{\prime}$, where $\boldsymbol{v}$ are the variables free in $P\rightarrow
P^{\prime}$.

Given a set $\alpha=\\{A_{1},\ldots,A_{n}\\}$ of Weaken applications, we use
$PVC(\alpha)=\\{PVC(A_{1})$, $\ldots$, $PVC(A_{n})\\}$ to denote the set of
PVCs for all Weaken applications in $\alpha$.

###### Example 4.3.

For the proof tree in Figure 4, which contains two instances of Weaken,
$PVC(\\{\textit{Wkn}_{1},\textit{Wkn}_{2}\\})$ contains the following two
formulas, where $P$ is $True$ and $Q$ is $e_{t}\neq 3$ as in Example 3.5:

  * •

$True\rightarrow(\forall e_{t_{y}}.Q_{N}(e_{t_{y}})\rightarrow e_{t_{y}}\neq
3)$

  * •

$True\rightarrow(Q_{N}(2)\land R[{e_{t}}/{x_{1}}][{2}/{e_{t}}])$

###### Definition 4.4 (Satisfiability).

We say a collection $C$ of PVCs is _satisfiable_ if there exists an assignment
of relations to parameters that makes each verification condition in $C$ true
as a first-order formula.

The following corollary follows from Theorem 4.1:

###### Corollary 4.5.

Let $S$ be a set of loop-free programs, and $\alpha$ be the set of Weaken
applications in the proof skeleton for
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
If $PVC(\alpha)$ is unsatisfiable, then
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is not provable in W-UL. In particular, this condition means that
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is false.

In other words, once formulas are proposed for each parameter, we may
substitute them into our PVCs and check the resulting verification conditions
to complete the proof. If the check on the verification conditions succeeds,
the proof is correct. Otherwise, the proof is incorrect (either because the
supplied formulas are insufficient, the claim is not true, or loops are
present) or the solver used is not powerful enough to prove correctness of the
verification conditions.

##  5\. Synthesizing Summaries and Invariants with SyGuS

The procedure described in §4 gives us a set of parametrized verification
conditions that characterize the set of preconditions, postconditions,
summaries, and loop invariants for which a completion of the proof tree is
valid. In this section, we show that just as such verification conditions can
be used as specifications to synthesize loop invariants in Hoare logic, they
can be used to synthesize summaries and invariants in W-UL.

We translate the problem of synthesizing summaries for parameterized
verification conditions into problems in the SyGuS framework for describing
synthesis problems (Alur et al., 2013). The goal of a SyGuS problem is to find
terms in a user-given grammar that agree with a given formula over a fixed
background theory.

###### Definition 5.1 (SyGuS (Alur et al., 2013)).

A Syntax-Guided Synthesis (SyGuS) problem over a background theory
$\mathcal{T}$ (e.g., LIA) is a tuple
$sy=(G_{1},\cdots,G_{n},\psi({f}_{1},\cdots,{f}_{n}))$. Here
$G_{1},\cdots,G_{n}$ are a regular tree grammars that only generate terms in
the background theory $\mathcal{T}$, and $\psi({f}_{1},\cdots,{f}_{n})$ is a
sentence in the language of $\mathcal{T}$ with additional function symbols
${f}_{1},\cdots,{f}_{n}$, which stand for the terms to be synthesized. A
solution to the problem $sy$ is a sequence of ground terms
$e_{1},\cdots,e_{n}$ so that each $e_{j}$ is in the language described by the
grammar $G_{j}$ and the formula $\psi(e_{1},\cdots,e_{n})$ is valid.

The ability to customize the grammar allows one to choose what form the
sought-for invariants and summaries should have. This feature is also used to
restrict the search space of the synthesis problem to increase scalability.

###### Definition 5.2 ($SY(G_{1},\cdots,G_{n},C_{\textit{PVC}})$).

Let $C_{\textit{PVC}}$ be a (finite) collection of PVCs with parameters
$Q_{1}(\boldsymbol{x_{1}}),\cdots,Q_{n}(\boldsymbol{x_{n}})$. For each
$Q_{j}$, $G_{j}$ is a grammar deriving some first-order formulas in the
language of integer arithmetic with free variables $\boldsymbol{x_{j}}$. Then
define the SyGuS problem $SY(G_{1},\cdots,G_{n},C_{\textit{PVC}})$ to be
$(G_{1},\cdots,G_{n},\psi(Q_{1},\cdots,Q_{n}))$ where $\psi$ is the
conjunction of the conditions in $C_{\textit{PVC}}$.

When $PVC(\alpha)$ of a triple has a solution, there are sufficiently
expressive grammars $G_{1},\cdots,G_{n}$ so that
$SY(G_{1},\cdots,G_{n},PVC(\alpha))$ has a solution. In particular, if $S$ is
a set of loop-free programs and each $G_{j}$ derives all first-order formulas
in its allowed language, then there is a proof of
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
if and only if $SY(G_{1},\cdots,G_{n},PVC(\alpha))$ has a solution.

As an example, we encode the parameterized verification conditions from
Example 4.3 as a SyGuS problem. We take $G$ to be the grammar deriving all
formulas of the form $e_{t}\equiv_{n}0$ for some $n$. Then
$SY(G,PVC(\alpha))=(G,\psi(Q_{N}))$ where

$\displaystyle\psi(Q_{N})$ $\displaystyle=True\rightarrow(\forall
e_{t_{y}}.Q_{N}(e_{t_{y}})\rightarrow e_{t_{y}}\neq 3)$ $\displaystyle\land
True\rightarrow(Q_{N}(2)\land(\forall e_{t_{y}}.Q_{N}(e_{t_{y}})\rightarrow
Q_{N}(2+e_{t_{y}})))$

The SyGuS problem $(G,\psi(Q_{N}))$ can be discharged to a SyGuS solver. For
our example, it is clear that taking $Q_{N}(e_{t})$ to be the formula
$(e_{t}\equiv_{2}0)\in L(G)$ satisfies the verification conditions. Indeed,
this formula was the summary used in Example 3.5.

##  6\. Implementation and Experimental Results

We implemented proof-skeleton generation (§ 4), verification-condition
extraction (§ 4), and reduction to SyGuS (§ 5) in OCaml in a tool called
Wuldo. Wuldo discharges the verification conditions to z3alpha (Zhengyang,
2023) when these conditions involve single states or vector-states of finite
lengths, and to Vampire (Blanc et al., 2013) when the vector-states are
infinite (because z3alpha cannot handle infinite arrays). Wuldo uses cvc5
(Barbosa et al., 2022) for summary synthesis and to implement part of the
optimization discussed below to discharge verification conditions.

In practice, many of the queries Wuldo generates are difficult for SMT solvers
to handle due to the disordered quantifiers appearing in verification
conditions. To remedy this issue, we implemented an optimization that (_i_)
simplifies the appearances of quantifiers in verification conditions, (_ii_)
uses a SyGuS solver (in parallel with the other constraint solver) to attempt
to solve complex formulas involving existential quantifiers. The optimization
starts by simplifying nested implications, moving universal quantifiers that
appear on the right-hand sides of VCs to the front of the formula, and
existential quantifiers that appear on the left-hand sides of VCs to the front
of the formula (by turning them into universal quantifiers). We also split VCs
of the form $A\rightarrow(B_{1}\land B_{2})$ in two: $A\rightarrow B_{1}$ and
$A\rightarrow B_{2}$.

For our Example 3.5, this optimization simplifies the PVCs in Example 4.3 to

$\displaystyle\forall e_{t_{y}}.((True\land Q_{N}(e_{t_{y}}))$
$\displaystyle\rightarrow e_{t_{y}}\neq 3)$ $\displaystyle True$
$\displaystyle\rightarrow Q_{N}(2)$ $\displaystyle\forall
e_{t_{y}}.((True\land Q_{N}(e_{t_{y}}))$ $\displaystyle\rightarrow
Q_{N}(2+e_{t_{y}}))$

The resulting PVCs are guaranteed to have no existential quantifiers
(excluding quantifiers in $P$, $Q$, and any invariants/summaries we may fill
in). When program variables exist, these quantifiers introduce no additional
degree of alternation (because the program variables are already universally
quantified at the front of the PVC). If $P$ or another term on the lhs were to
contain an existential quantifier, such a quantifier would also be moved to
the front of the formula as a universal quantifier.

Our optimization, so far, cannot extract any existential quantifiers that
appear in the rightmost implicand (e.g., $e_{t_{y}}\neq 3$ and
$Q_{N}(2+e_{t_{y}})$ above). To address this challenge, we replace any such
existentially quantified variables with second-order function variables. These
function variables take as input the variables extracted from the left-hand
side of the VC. We can then encode the problem of discharging this modified VC
as a SyGuS problem where we ask a solver (cvc5) to find an instantiation for
the second-order variable that makes the verification condition hold.

When attempting this operation, we run z3alpha in parallel on the original
quantified VC and return the result of whichever tool terminates first.
Because cvc5 cannot handle infinite vectors, we do not issue a SyGuS query for
formulas that use them.

When this optimization is used, we call our tool Wuldo. Else, we call it
Wuldo-.

Our evaluation is designed to answer the following research questions:

RQ1:

How effective is Wuldo at constructing proofs when invariants and summaries
are provided?

RQ2:

How effective is Wuldo at synthesizing invariants and most general formulas?

RQ3:

How effective is the optimization Wuldo compared to Wuldo-?

Because there is no other implementation of Unrealizability Logic, we
evaluated these questions using only Wuldo- and Wuldo. All experiments were
run three times on a 4-core i7-7700HQ CPU processor with 16GB RAM and a
5-minute timeout. Tables 1 and 2 report the median times.

#### Benchmarks

In total, we considered 32 benchmarks, which have the following
characteristics.

Nope (Hu et al., 2019) is a tool for proving unrealizability of LIA (Linear
Integer Arithmetic) SyGuS problems and its evaluation contains 132
unrealizable SyGuS problems. We translated $9$ representative benchmarks (one
from each of type of grammar we identified in the benchmarks) from this
collection to problems in unrealizability logic. (These benchmarks only
contain expressions and no statements.) The Nope benchmarks have grammars with
between 1 and 5 nonterminals and specifications of between 1 and 9 input-
output examples. For 3 of these benchmarks (distinguished with the suffix
_hard), we introduced variants with simplified search spaces to produce an
equivalent set of programs that is easier for W-UL to verify (distinguished
with the suffix _easy).

Messy (Kim et al., 2021) is a tool for proving unrealizability of synthesis
problems written in the SemGuS format—a language for defining synthesis
problems in which the users may provide a customized programming language.
$14$ of the benchmarks used to evaluate MESSY operate over an imperative
language with bitvector variables. These benchmarks require deciding whether
one bitvector operation can be synthesized from some others (e.g.,
synthesizing max from and, or, and plus) and are of interest because several
have simple but hard-to-discover summaries. Of these benchmarks, we manually
identified $5$ as realizable and excluded them from our study. Of the
remainder, we used the $7$ benchmarks for which we could handwrite summaries.
These benchmarks had grammars with 1 to 4 nonterminals and had as
specifications between 1 and 4 input-output examples.

We also used the 9 examples described in the original UL paper (Kim et al.,
2023), plus our own Example 3.5. These benchmarks are rather small, with
grammars containing between 1 and 3 nonterminals and specifications consisting
of between 0 and 2 input-output examples.

Table 1.  Time to generate and verify proofs when invariants and summaries are specified. An X denotes a timeout.  | Wuldo- | Wuldo
---|---|---
|  MESSY Bitvector | AND | 0.383 | 0.776
ADD | 0.235 | 0.845
MAX | 0.518 | 0.786
PLUS | 0.397 | 0.608
SWAP_XOR | 0.204 | 5.883
XOR | 0.478 | 1.881
WHL_XOR | 0.812 | 0.912
Nope | const_example1 | 2.375 | 3.035
mpg_example1 | X | 5.466
if_guard | X | 9.684
if_max3_hard | X | X
if_max3_easy | X | 14.208
if_ite1_hard | X | X
if_ite1_easy | X | 14.447
if_sum_3_5_hard | X | X
if_sum_3_5_easy | X | 15.568
if_search_2_hard | X | X
if_search_2_easy | X | 17.343
plus_array_search2 | 5.985 | 19.486
plus_mpg_ite1 | 2.801 | 4.150
Limit Pt | id_not_in_ite | 83.147 | 79.330
t_Linterval_union | 84.614 | 76.515
y_0_decr | 74.559 | 75.261
S-UL (Kim et al., 2023) | ex1.1_simp | 0.384 | 0.512
ex2.3_simp | 0.829 | 4.544
ex2.6_simp | 0.349 | 6.502
ex3.8_simp | 0.208 | 0.296
ex5.2_simp | 1.384 | 9.722
ex5.3_simp | 0.332 | 19.508
ex2.5_finVS | 0.543 | 0.751
ex3.11_finVS | 0.249 | 0.300
| ex3.5_ulw | 0.230 | 1.327

We added an additional $3$ “limit point” benchmarks for which the proof of
unrealizability requires infinitely many examples (and therefore infinite
vector states). In these benchmarks, it is necessary to prove that a program
is excluded from a set that contains arbitrarily close approximations to the
target program (i.e., the proof requires separating a set of programs from a
limit point). We also include in this category the running example from §2,
which appeared in (Kim et al., 2023) as well (grammars have with 1 to 2
nonterminals).

### RQ1: How effective is Wuldo when invariants and summaries are provided?

Table 1 shows the results of running Wuldo on all benchmarks when summaries
are provided. Wuldo can generate valid W-UL proofs when invariants and
summaries are specified for 28/32 benchmarks, taking between 0.204s and
79.330s (avg. 16.197s).

Wuldo fails on four Nope benchmarks. The summaries used in these benchmarks
are inspired by the specialized LIA technique presented by Hu et al. (2019),
namely, semi-linear sets to exactly capture the behavior of all the
expressions in the input grammar on the given input examples. For example, the
possible outputs of any program in the grammar $E\mapsto E+2\mid x$ on the
inputs $x=2$ and $x=3$ can be captured by the formula $(2,3)+a(2,2)$, where
all operations are defined pairwise and $a$ is a free integer variable. The
benchmarks for which Wuldo failed (benchmarks with _hard in the name) all
contained recursive nonterminals with a production rule of the form
“${\mathsf{if}}\ {B}\ {\mathsf{then}}\ {E}\ {\mathsf{else}}\ {E}$” for a
grammar similar to $E$ above. We were able to manually simplify these
benchmarks’ grammars to eliminate recursion in these nonterminals, producing
the corresponding _easy benchmarks. Such a simplification could easily be
automated.

Although the state-of-the-art tool for SyGuS unrealizability Nay can solve the
Nope benchmarks very efficiently (without requiring a summary), it implements
a domain-specific solution for LIA SyGuS problems. Therefore it would not make
sense to compare Nay to Wuldo.

The MESSY bitvector benchmarks used quantifier-free summaries and were
generally much easier to verify than the Nope benchmarks when the correct
summary was specified. The summaries we wrote were mostly from a grammar
$G_{BV}$ that could express summaries of the form “if the inputs are set to
$v$ in the $n^{\textit{th}}$ bit, the outputs must be set to $v^{\prime}$ in
the $n^{\textit{th}}$ bit” (for any possible values of $v,n,v^{\prime}$). (We
take advantage of this structure in the next section when we answer RQ2.)
Although MESSY can solve these benchmarks (without requiring a summary), it
does so by dispatching the problem to a constraint solver and cannot produce a
proof certificate. Handwriting the necessary summaries can be laborious, but
in exchange, Wuldo is the only tool that provides an interpretable proof
artifact.

The limit-point benchmarks are ones that no prior tool for proving
unrealizability can solve, regardless of whether or not a summary is provided.

##### Findings

Wuldo can discharge the verification conditions for 27/31 benchmarks when
summaries and invariants are provided. Furthermore, Wuldo can discharge proofs
of unrealizability for synthesis problems that no other unrealizability tool
can reason about.

### RQ2: How effective is Wuldo at synthesizing summaries and invariants?

Because existing SyGuS solvers provide little to no support for synthesizing
formulas with quantifiers and infinite arrays, we could not evaluate this
research question on the limit point benchmarks, nor could we specify a
reasonable grammar to guide synthesis of the Nope benchmarks.

Our first approach to summary synthesis was to let cvc5 search over _all_
possible quantifier-free formulas. While this worked for a few of the examples
from

Table 2.  Time taken to synthesize summaries and invariants with (i) an Unconstrained grammar and (ii) the grammar $G_{BV}$ for bitvectors. An X denotes a timeout.  Unconstrained | $G_{BV}$
---|---
|  | Wuldo- | Wuldo | Wuldo- | Wuldo
MESSY Bitvectors | AND | X | X | 0.18s | 0.44s
ADD | X | X | 2.57s | 0.44s
MAX | X | X | X | X
PLUS | X | X | 0.23s | 0.31s
XOR | X | X | 0.20s | 0.52s
WHL_XOR | X | X | X | X
S-UL Examples | ex1.1_simp | 0.38s | 0.21s | N/A | N/A
ex2.3_simp | X | X | N/A | N/A
ex2.6_simp | X | X | N/A | N/A
ex3.8_simp | 0.16s | 0.15s | N/A | N/A
ex5.2_simp | X | X | N/A | N/A
ex5.3_simp | X | X | N/A | N/A
ex2.5_finVS | 0.16s | 0.17s | N/A | N/A
ex3.11_finVS | 0.16s | 0.19s | N/A | N/A
| ex3.5_ulw | X | 0.21s | N/A | N/A

the S-UL paper with trivial grammars (see Unconstrained columns in Table 2),
it failed on all the MESSY and Nope benchmarks. On the S-UL examples, Wuldo
verified 5/9 benchmarks taking 0.19s on average, 61% less time than when
summaries were specified.

We then supplied the grammar $G_{BV}$ from the previous section to restrict
the search space for the bitvector benchmarks. When given the grammar
$G_{BV}$, Wuldo solved $4/6$ benchmarks with summaries to synthesize, taking
on average 0.43s (see $G_{BV}$ columns of Table 2). Note that SWAP_XOR
requires no summaries or invariants, so we exclude it from this study. For the
4 solved benchmarks, Wuldo took on average 53% less time than when summaries
were manually provided.

##### Findings

When no grammar for summaries is specified, Wuldo can find summaries only on
easy examples. Given a summary/invariant grammar, Wuldo can synthesize these
components, but its effectiveness depends on the power of the underlying SyGuS
solver—i.e., improvements in SyGuS solvers will improve Wuldo’s ability to
generate W-UL proofs when summaries and invariants are not provided. These
experiments suggest our approach for synthesizing summaries/invariants is at
least feasible.

### RQ3: How effective is the optimization in Wuldo?

When summaries were provided (Table 1), Wuldo could solve 4 Nope benchmarks
that the unoptimized solver Wuldo- could not. For these 4 benchmarks, Wuldo
could, for example, prove that the sum of two linear combinations over some
variables must itself be a linear combination over the variables. Our encoding
of existential quantifiers as second order functions allowed cvc5 to determine
that the coefficients of the sum should be the sum of the summands’
coefficients. On the benchmarks Wuldo- could solve, Wuldo was on average 4%
faster (geomean).

When summaries were not provided (Table 2), Wuldo could solve 1 benchmark that
the unoptimized solver Wuldo- could not solve. On the benchmarks Wuldo- could
solve, Wuldo was on average 0.5% faster (geomean).

##### Findings

Wuldo’s optimizations are effective and result in more solved problems.

##  7\. Related Work

Techniques for proving unrealizability can be used for proving that a program
is optimal with respect to a given quantitative objective (Hu and D’Antoni,
2018), pruning parts of the search space explored during program synthesis
(Farzan et al., 2022; Kamp and Philippsen, 2021), verifying incomplete
programs (Mechtaev et al., 2018), and in other settings (D’Antoni, 2023).

Unrealizability Logic. According to the proof of completeness of S-UL, there
exists a syntax-guided order of rules that may be applied to prove any valid
unrealizability triple. However, this proof strategy depends on one being able
to supply hypotheses that are _powerful enough_ to prove unrealizability,
_immediately upon encountering_ a nonterminal in the proof tree. This
requirement is in sharp contrast with the approach presented in §4, where one
can _postpone_ providing such a hypothesis, and can even synthesize hypotheses
that are strong enough after completing the structure of the whole proof tree.

To summarize, naively following the strategy provided in the completeness
proof of (Kim et al., 2023) would entangle the structural and hypothesis-
complexity challenges. The algorithm presented in §4 disentangles these two
challenges to aid automation. In particular, unlike for S-UL, the rule of
adaptation in W-UL allows syntax-directed generation of practical proof
skeletons _independently_ of the predicates being considered. This addresses
the structural challenge (§4).

Tools for Proving Unrealizability. Nope (Hu et al., 2019) and Nay (Hu et al.,
2020) can prove unrealizability for SyGuS problems by encoding the
unrealizability problem into queries that are understandable by an external
solver (e.g., a program-reachability query in Nope, and a satisfiability query
over a complex logic in Nay) and then rely on an external algorithm to check
whether the encoded problem is solvable or not. As discussed in Section 6,
while such encodings may be efficient in practice, they cannot produce proof
certificates. In addition, both Nope and Nay are limited to supporting SyGuS
problems, while our work is capable of supporting any synthesis problem over
an imperative programming language.

Similar to Nope and Nay, MESSY (Kim et al., 2021) can verify whether a
synthesis problem expressed in the SemGuS framework is unrealizable by
encoding it as a satisfiability query over a set of Constrained Horn Clauses
(CHCs)—i.e., it also cannot produce a proof certificate. On the other hand,
MESSY is also capable of identifying synthesis problems as realizable, whereas
this work can only show unrealizability. Designing a dual of UL for checking
realizability (akin to how incorrectness logic (O’Hearn, 2019) dualizes Hoare
logic) is an open research problem as discussed by Kim et al. (2023). A key
feature of MESSY is also that it is defined over the SemGuS framework, which
allows MESSY to identify unrealizability over a wide variety of languages
(e.g., regular expressions).

The last key distinction is that MESSY, Nope, and Nay cannot express or prove
unrealizability for any problem where the proof requires infinitely many
examples. Moreover, W-UL and S-UL are both relatively complete proof systems
on sets of loop-free programs.

##  8\. Conclusion

Prior to this work, generating a proof in Unrealizability Logic was fraught
with difficulties, including disentangling mutual dependence between the proof
tree and invariants/summaries. In this work, we design a weakest-precondition
version of UL more amenable to automated reasoning, featuring (i) rules
allowing fully syntax-directed proof construction and (ii) streamlined
nonterminal summaries. We also implement the first synthesizer for proofs over
infinite sets of programs, Wuldo. Our experiments suggest that Wuldo can
reason about infinite sets of programs when invariants and summaries are
specified, and in some cases can even synthesize the needed
invariants/summaries. We also show that Wuldo can prove properties involving
infinitely many input-output examples.

Despite being slower than existing techniques, Wuldo exhibits unique
advantages in the range of different problems it can handle, the insight
provided by its generated proofs, and the reusability of insights/proofs on
small sets of programs.

## References

  * (1)
  * Alur et al. (2013) Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013\.  Syntax-guided synthesis. In _Formal Methods in Computer-Aided Design (FMCAD), 2013_. IEEE, 1–8.
  * Barbosa et al. (2022) Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022\.  Cvc5: A Versatile and Industrial-Strength SMT Solver. In _Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I_ (Munich, Germany). Springer-Verlag, Berlin, Heidelberg, 415–442.  https://doi.org/10.1007/978-3-030-99524-9_24
  * Barbosa et al. (2023) Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Yoni Zohar. 2023.  Generating and Exploiting Automated Reasoning Proof Certificates.  _Commun. ACM_ 66, 10 (sep 2023), 86–95.  https://doi.org/10.1145/3587692
  * Blanc et al. (2013) Régis Blanc, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. 2013.  Tree interpolation in vampire. In _International Conference on Logic for Programming Artificial Intelligence and Reasoning_. Springer, 173–181.
  * D’Antoni (2023) Loris D’Antoni. 2023\.  Verifying Infinitely Many Programs at Once. In _Static Analysis_ , Manuel V. Hermenegildo and José F. Morales (Eds.). Springer Nature Switzerland, Cham, 3–9.
  * Farzan et al. (2022) Azadeh Farzan, Danya Lette, and Victor Nicolet. 2022\.  Recursion synthesis with unrealizability witnesses. In _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_. 244–259.
  * Hoare (2006) Charles Antony Richard Hoare. 2006\.  Procedures and parameters: An axiomatic approach. In _Symposium on semantics of algorithmic languages_. Springer, 102–116.
  * Hu et al. (2019) Qinheping Hu, Jason Breck, John Cyphert, Loris D’Antoni, and Thomas Reps. 2019.  Proving unrealizability for syntax-guided synthesis. In _International Conference on Computer Aided Verification_. Springer, 335–352.
  * Hu et al. (2020) Qinheping Hu, John Cyphert, Loris D’Antoni, and Thomas Reps. 2020.  Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_. 1128–1142.
  * Hu and D’Antoni (2018) Qinheping Hu and Loris D’Antoni. 2018.  Syntax-guided synthesis with quantitative syntactic objectives. In _International Conference on Computer Aided Verification_. Springer, 386–403.
  * Kamp and Philippsen (2021) Marius Kamp and Michael Philippsen. 2021.  Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible. In _Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings_ _(Lecture Notes in Computer Science, Vol. 12597)_ , Fritz Henglein, Sharon Shoham, and Yakir Vizel (Eds.). Springer, 353–375.  https://doi.org/10.1007/978-3-030-67067-2_16
  * Kim et al. (2023) Jinwoo Kim, Loris D’Antoni, and Thomas Reps. 2023\.  Unrealizability logic.  _Proceedings of the ACM on Programming Languages_ 7, POPL (2023), 659–688.
  * Kim et al. (2021) Jinwoo Kim, Qinheping Hu, Loris D’Antoni, and Thomas Reps. 2021\.  Semantics-guided synthesis.  _Proceedings of the ACM on Programming Languages_ 5, POPL (2021), 1–32.
  * Lee et al. (2018) Woosuk Lee, Kihong Heo, Rajeev Alur, and Mayur Naik. 2018\.  Accelerating Search-Based Program Synthesis Using Learned Probabilistic Models. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Philadelphia, PA, USA) _(PLDI 2018)_. Association for Computing Machinery, New York, NY, USA, 436–449.  https://doi.org/10.1145/3192366.3192410
  * Leino (2016) K. Rustan M. Leino. 2016\.  This is Boogie 2.  https://api.semanticscholar.org/CorpusID:62210165
  * Mechtaev et al. (2018) Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, and Abhik Roychoudhury. 2018.  Symbolic execution with existential second-order constraints. In _Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_. 389–399.
  * O’Hearn (2019) Peter W O’Hearn. 2019\.  Incorrectness logic.  _Proceedings of the ACM on Programming Languages_ 4, POPL (2019), 1–32.
  * Olderog (1983) Ernst-Rüdiger Olderog. 1983\.  On the Notion of Expressiveness and the Rule of Adaption.  _Theor. Comput. Sci._ 24 (1983), 337–347.  https://api.semanticscholar.org/CorpusID:32890639
  * Zhengyang (2023) Lu Zhengyang. 2023\.  Z3-Alpha: A Reinforcement Learning Guided Smt Solver.  https://smt-comp.github.io/2023/system-descriptions/z3-alpha.pdf

##  Appendix A Appendix: Soundness and Loop-Free Relative Completeness

Recall, an unrealizability triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds if and only if, for all $s\in S$, the Hoare triple
$\\{{P}\\}\>s\>\\{Q\\}$ holds in the sense of partial correctness, where the
semantics of programs are changed so that $e_{t}/b_{t}$ take on the value of
the last integer-valued/Boolean-valued expression evaluated.

###  A.1. Soundness

###### Theorem 3.2 0 (Soundness).

W-UL is sound. For any predicate $P$, $Q$, and set of programs $S$,
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}\implies\forall
s\in S.\\{{P}\\}\>s\>\\{Q\\}$ in the sense of partial correctness for every
$s\in S$.

###### Proof.

We prove both soundness by structural induction over the set of proof trees.
It suffices to show that every rule has the following property:

###### Definition A.1 (Soundness Property).

An inference rule has the soundness property if, when its hypotheses hold, its
conclusion holds.

##### Int, False, True, Var

The axioms Int, False, True, and Var of W-UL are sound. In particular, for Int
and Var rule, the last integer-valued expression evaluated is the int or var
in question, so if the postcondition holds when the value is substituted for
$e_{t}$ (e.g., $Q[{x}/{e_{t}}]$ holds), it should hold once the expression is
evaluated and the result is stored in $e_{t}$ (e.g., after $e_{t}:=x$). False
and True are sound by similar reasoning.

##### Not

Suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q[{\neg
b_{t}}/{b_{t}}]|\kern-2.15277pt\\}$ holds. Let $s\in S$ be given. Then
$\\{{P}\\}\>s\>\\{Q[{\neg b_{t}}/{b_{t}}]\\}$ holds. Then, for any $\sigma\in
P$ and $\sigma^{\prime}=\llbracket{s}\rrbracket(\sigma)\in Q[{\neg
b_{t}}/{b_{t}}]$, we observe $\llbracket{\neg
s}\rrbracket(\sigma)=(\llbracket{s}\rrbracket(\sigma))[{b_{t}}\mapsto{\neg(\llbracket{s}\rrbracket(\sigma))(b_{t})}]=\sigma^{\prime}[{b_{t}}\mapsto{\neg\sigma^{\prime}(b_{t})}]\in
Q$. Thus $\\{{P}\\}\>s\>\\{Q\\}$ holds on all $s\in S$, so
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds.

##### Bin, Comp, And

We show soundness of Bin by contrapositive; the argument generalizes. Suppose
$\\{\kern-2.15277pt|{R}|\kern-2.15277pt\\}\>E_{2}\>\\{\kern-2.15277pt|Q[{x_{1}\oplus
e_{t}}/{e_{t}}]|\kern-2.15277pt\\}$ and
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}\>\\{\kern-2.15277pt|R[{e_{t}}/{x_{1}}]|\kern-2.15277pt\\}$
hold. Let $e_{1}\in E_{1}$ and $e_{1}\in E_{1}$ be given. Then the
corresponding Hoare triples hold. Consider $\sigma_{2}\notin Q$, and suppose
there is some $\sigma$ from which it originated (i.e., $\llbracket{e_{1}\oplus
e_{2}}\rrbracket(\sigma)=\sigma_{2}$). Then consider
$\sigma_{1}=\sigma[{x_{1}}\mapsto{\sigma(e_{1})}]$. Observe that
$\sigma_{2}=\sigma_{1}[{e_{t}}\mapsto{\sigma_{1}(x_{1})+\sigma_{1}(e_{2})}]$.
Note also that, since $\sigma_{2}\notin Q$,
$\sigma_{1}[{e_{t}}\mapsto{\sigma_{1}(e_{2})}]\notin Q$. By correctness of the
hypothesis on $E_{2}$, $\sigma_{1}\notin R$. This implies
$\llbracket{e_{1}}\rrbracket(\sigma)=\sigma[{e_{t}}\mapsto{\sigma(e_{1})}]\notin
R[{e_{t}}/{x_{1}}]$. By correctness of the first hypothesis, $\sigma\notin P$!
So, for all $\sigma\in P$, $\llbracket{e_{1}+e_{2}}\rrbracket(\sigma)\in Q$.
Moreover, this holds on all $e\in E_{1}\oplus E_{2}$, so the triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}\oplus
E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ holds as desired.

##### Assign

For Assign, suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E\>\\{\kern-2.15277pt|Q[{e_{t}}/{x}]|\kern-2.15277pt\\}$
holds and $e\in E$. If $\sigma^{\prime}\notin Q$ and $\sigma$ so that
$\sigma^{\prime}=\llbracket{x:=e}\rrbracket(\sigma)$, we see
$\llbracket{e}\rrbracket(\sigma)=\sigma^{\prime}[{e_{t}}\mapsto{\llbracket{\sigma}\rrbracket(e)}]\notin
Q[{e_{t}}/{x}]$, so by correctness of the hypothesis, $\sigma\notin P$. Thus
$\\{{P}\\}\>x:=e\>\\{P\\}$ holds for all $e\in E$ and hence
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|P|\kern-2.15277pt\\}$
holds.

##### Seq

For Seq, suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S_{1}\>\\{\kern-2.15277pt|R|\kern-2.15277pt\\}$
and
$\\{\kern-2.15277pt|{R}|\kern-2.15277pt\\}\>S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
hold, and let $s_{1}\in S_{1}$ and $s_{2}\in S_{2}$. Consider
$\sigma_{2}\notin Q$. Suppose there is some $\sigma$ so that
$\sigma_{2}=\llbracket{s_{1};s_{2}}\rrbracket(\sigma)$. If such $\sigma$
exists, then there is a $\sigma_{1}=\llbracket{s_{1}}\rrbracket(\sigma)$ and
thus $\sigma_{2}=\llbracket{s_{2}}\rrbracket(\sigma_{1})$. By correctness of
the second hypothesis, $\sigma_{1}\notin R$. By correctness of the first
hypothesis, $\sigma\notin P$. So, for all $\sigma\in P$,
$\llbracket{s_{1};s_{2}}\rrbracket(\sigma)\in Q$. Thus
$\\{{P}\\}\>s_{1};s_{2}\>\\{Q\\}$ holds for all $s_{1}\in S_{1}$ and $s_{2}\in
S_{2}$, so
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S_{1};S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds as well.

##### SimpleIf

Suppose the hypotheses of the single-state ITE rule hold. Let $b\in B$,
$s_{1}\in S_{1}$, and $s_{2}\in S_{2}$. Then, consider any poststate
$\sigma_{2}\notin Q$. Suppose there is a $\sigma$ so that
$\sigma_{2}=\llbracket{\text{if }b\text{ then }s_{1}\text{ else
}s_{2}}\rrbracket(\sigma)$. Then consider $\sigma_{1}$ so that
$\sigma_{1}=\llbracket{b}\rrbracket(\sigma)$. WLOG suppose $b$ evaluates to
$true$ on $\sigma$. Then
$\sigma_{2}=\llbracket{s_{1}}\rrbracket(\sigma_{then})$. By correctness of the
Then hypothesis, $\sigma_{1}\notin P_{1}$. Since $\sigma_{1}(b_{t})=true$,
$\sigma_{1}\notin((b_{t}\rightarrow P_{1})\land(\neg b_{t}\rightarrow
P_{2}))$. By correctness of the guard hypothesis, $\sigma\notin P$. So
$\\{{P}\\}\>\text{if }b\text{ then }s_{1}\text{ else }s_{2}\>\\{Q\\}$ holds.
Thus, $\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>\text{if }B\text{ then
}S_{1}\text{ else }S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ holds as
well.

##### SimpleWhile

Suppose the hypotheses of the While rule hold. Let $b\in B$ and $s\in S$ be
given. Consider $\sigma^{\prime}\notin Q$. For any $\sigma_{0}$ so that $b$ is
false on $\sigma_{0}$ and $\sigma^{\prime}=\llbracket{\text{while }b\text{ do
}s}\rrbracket(\sigma_{0})$, soundness of the guard hypothesis tells us
$\sigma_{0}\notin I$ just like in the soundness proof of ITE. Similarly, for
any $\sigma_{1}$ so that the loop body runs once on $\sigma_{1}$ to yield
$\sigma_{0}$, completeness of the body hypothesis implies
$\llbracket{b}\rrbracket(\sigma_{1})\notin P_{I}$. But then, we know $b_{t}$
is true on $\llbracket{b}\rrbracket(\sigma_{1})$, so
$\llbracket{b}\rrbracket(\sigma_{1})\notin((\neg b_{t}\rightarrow
Q)\land(b_{t}\rightarrow P_{I}))$. By correctness of the guard hypothesis,
$\sigma_{1}\notin I$. The same argument can be applied to show there is no
$\sigma_{k}\in I$ which terminates in state $\sigma^{\prime}$ after $k$ runs
of the loop body. Thus, $\\{{I}\\}\>\text{while }b\text{ do }s\>\\{Q\\}$ holds
in the sense of partial correctness. This is true on every program in the set,
so $\\{\kern-2.15277pt|{I}|\kern-2.15277pt\\}\>\text{while }B\text{ do
}S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ holds as well.

##### GrmDisj

Let a nonterminal $S$ be given, and suppose the program $s$ comes from one of
its productions $S_{j}$. Then, by correctness of the hypotheses,
$\\{{P_{j}}\\}\>s\>\\{Q\\}$ holds. This implies
$\\{{\bigwedge_{j}P_{j}}\\}\>s\>\\{Q\\}$ holds. This argument applied to all
$s\in S$ gives
$\\{\kern-2.15277pt|{\bigwedge_{j}P_{j}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
as desired.

##### HP, ApplyHP

HP and ApplyHP are sound by correctness of structural induction over the
grammar.

##### Adapt

Soundness of Adapt on individual programs is proven in . This extends to sets
of programs trivially, since the hypothesis on sets implies the hypothesis on
programs, which implies the conclusion on programs. The conclusion being true
on all programs gives us that it is true on the set.

##### Weaken

Weaken is correct by extending its correctness in Hoare logic like we did for
Adapt. ∎

###  A.2. Completeness

###### Theorem 3.3 0 (Relative Completeness for Sets of Loop-Free Programs).

W-UL is relatively complete on sets of loop-free programs. That is, for every
$P$, $S$, and $Q$, where all programs in $S$ are loop-free and
$\\{{P}\\}\>s\>\\{Q\\}$ holds in the sense of partial correctness for every
$s\in S$, the claim
$\emptyset\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
is derivable in W-UL (modulo completeness of the assertion language).

Moreover, a proof that adheres to the skeleton generated in § 4.1 always
exists. We do so by showing, for every constructor in $G_{imp}$ as well as for
recursive and nonrecursive nonterminals, every true triple can be proven from
true hypotheses. Moreover, when our hypotheses adhere to the proof skeleton
our algorithm proposes, the tree we construct at any given step does as well.
By structural induction, we get relative completeness with a construction
adhering to the desired proof skeleton.

###### Proof.

First, for each program constructor in $G_{imp}$, we will prove that, for any
partial program whose AST’s root is that constructor, there is a way to derive
any true triple on the program given sufficiently precise triples on its
children. In particular, we show by induction that the proofs we construct
will follow exactly the algorithm of § 4.1. That is, for each constructor, for
each partial program $S$ whose root is that constructor, if the hypotheses of
the rules used are proven according to the skeleton our algorithm would
produce, then the statement on $S$ is proven according to our algorithm as
well.

##### Int, True, False, Var

Suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>i\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds where $i\in\mathbb{Z}$. Then the weakest precondition of $Q$ with
respect to $i$ is $Q[{i}/{e_{t}}]$. For any prestate $\sigma\notin
Q[{i}/{e_{t}}]$, $\llbracket{i}\rrbracket(\sigma)\notin Q$. So our Int rule,
in combination with Weaken, can prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>i\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
The other expression terminals follow similarly.

##### Not

Suppose $\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>\neg
B\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ holds. Then call
$P^{\prime}=\bigcap_{b\in B}wpc(b,Q[{\neg b_{t}}/{b_{t}}])$. Since
$\\{{P^{\prime}}\\}\>b\>\\{Q[{\neg b_{t}}/{b_{t}}]\\}$ holds on all $b\in B$,
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>B\>\\{\kern-2.15277pt|Q[{\neg
b_{t}}/{b_{t}}]|\kern-2.15277pt\\}$ holds. Then observe
$P\subseteq\bigcap_{b\in B}wpc(\neg b,Q)=\bigcap_{b\in B}wpc(b,Q[{\neg
b_{t}}/{b_{t}}])=P^{\prime}$. So, we can apply our Not inference rule to the
hypothesis $\\{{P^{\prime}}\\}\>b\>\\{Q[{\neg b_{t}}/{b_{t}}]\\}$ to prove
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>\neg
B\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ and Weaken to
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>B\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
so any true triple on Nots can be proven from precise enough hypotheses in
exactly the manner of our algorithm.

##### Plus, And, Less, Equals

We illustrate the point on $+$. Suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}+E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds. Define an intersection of weakest preconditions
$R\triangleq\bigcap_{e_{2}\in E_{2}}wpc(e_{2},Q[{x_{1}+e_{t}}/{e_{t}}])$. Then
$\\{\kern-2.15277pt|{R}|\kern-2.15277pt\\}\>E_{2}\>\\{\kern-2.15277pt|Q[{x_{1}+e_{t}}/{e_{t}}]|\kern-2.15277pt\\}$
holds. Similarly, define $P^{\prime}\triangleq\bigcap_{e_{1}\in
E_{1}}wpc(e_{1},R[{e_{t}}/{x_{1}}])$, so
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>E_{1}\>\\{\kern-2.15277pt|R[{e_{t}}/{x_{1}}]|\kern-2.15277pt\\}$
holds. Of course, $wpc(e,Q)=Q[{e}/{e_{t}}]$ and
$wpc(e_{1}+e_{2},Q)=Q[{e_{1}+e_{2}}/{e_{t}}]$. With this in mind,

$\displaystyle P^{\prime}$ $\displaystyle=\bigcap_{e_{1}\in
E_{1}}wpc(e_{1},R[{e_{t}}/{x_{1}}])$ $\displaystyle=\bigcap_{e_{1}\in
E_{1}}wpc(e_{1},(\bigcap_{e_{2}\in
E_{2}}wpc(e_{2},Q[{x_{1}+e_{t}}/{e_{t}}]))[{e_{t}}/{x_{1}}])$
$\displaystyle=\bigcap_{e_{1}\in E_{1}}wpc(e_{1},(\bigcap_{e_{2}\in
E_{2}}Q[{x_{1}+e_{t}}/{e_{t}}][{e_{2}}/{e_{t}}])[{e_{t}}/{x_{1}}])$
$\displaystyle=\bigcap_{e_{1}\in E_{1}}wpc(e_{1},\bigcap_{e_{2}\in
E_{2}}Q[{e_{t}+e_{2}}/{e_{t}}])$ $\displaystyle=\bigcap_{e_{1}\in
E_{1},e_{2}\in E_{2}}wpc(e_{1},Q[{e_{t}+e_{2}}/{e_{t}}])$
$\displaystyle=\bigcap_{e_{1}\in E_{1},e_{2}\in
E_{2}}Q[{e_{1}+e_{2}}/{e_{t}}]$ $\displaystyle=\bigcap_{e_{1}\in
E_{1},e_{2}\in E_{2}}wpc(e_{1}+e_{2},Q)$

Now since
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}+E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds, for every $e_{1}\in E_{1}$ and $e_{2}\in E_{2}$
$\\{{P}\\}\>e_{1}+e_{2}\>\\{Q\\}$ holds. This means $P\subseteq
wpc(e_{1}+e_{2},Q)$. Altogether, $P\subseteq P^{\prime}$. We can prove
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>E_{1}+E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
with the Bin rule, and we can Weaken to prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>E_{1}+E_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
This proof adheres to our skeleton when its hypotheses do.

##### Assign

Suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds. Let $P^{\prime}=\bigcap_{e\in E}wpc(e,Q[{e_{t}}/{x}])$. Then
$\\{{P^{\prime}}\\}\>e\>\\{Q[{e_{t}}/{x}]\\}$ must hold for all $e\in E$, so
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>E\>\\{\kern-2.15277pt|Q[{e_{t}}/{x}]|\kern-2.15277pt\\}$
holds. So we can prove
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
But note $P\subseteq\bigcap_{e\in E}wpc(x:=e,Q)=\bigcap_{e\in
E}wpc(e,Q[{e_{t}}/{x}])=P^{\prime}$. So we can obtain
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
by Weakening from
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>x:=E\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
The proof tree we construct exactly adheres to our skeleton when its
hypotheses do.

##### Seq

If
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S_{1};S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds, then define $R=\bigcap_{s_{2}\in S_{2}}wpc(s_{2},Q)$, and define

$\displaystyle P^{\prime}$ $\displaystyle=\bigcap_{s_{1}\in
S_{1}}wpc(s_{1},R)$ $\displaystyle=\bigcap_{s_{1}\in
S_{1}}wpc(s_{1},\bigcap_{s_{2}\in S_{2}}wpc(s_{2},Q))$
$\displaystyle=\bigcap_{s_{1}\in S_{1},s_{2}\in S_{2}}wpc(s_{1},wpc(s_{2},Q))$
$\displaystyle=\bigcap_{s_{1}\in S_{1},s_{2}\in S_{2}}wpc(s_{1};s_{2},Q)$

As in the proof for Plus, we can see $P\subseteq P^{\prime}$, so applying the
Seq rule with correct hypotheses
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>S_{1}\>\\{\kern-2.15277pt|R|\kern-2.15277pt\\}$
and
$\\{\kern-2.15277pt|{R}|\kern-2.15277pt\\}\>S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
proves
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>S_{1};S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
and applying Weaken to this proves
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S_{1};S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
This proof tree adheres to our skeleton when its hypotheses do.

##### If-Then-Else

Suppose $\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>\text{if }B\text{ then
}S_{1}\text{ else }S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$ holds. Then

$\displaystyle P$ $\displaystyle\subseteq\bigcap_{b\in B,s_{1}\in
S_{1},s_{2}\in S_{2}}wpc({\text{if }b\text{ then }s_{1}\text{ else }s_{2}},Q)$
$\displaystyle=\bigcap_{b\in B,s_{1}\in S_{1},s_{2}\in S_{2}}(b\rightarrow
wpc(s_{1},Q))\land(\neg b\rightarrow wpc(s_{2},Q))$
$\displaystyle=\bigcap_{b\in B,s_{1}\in S_{1}}(b\rightarrow
wpc(s_{1},Q))\cap\bigcap_{b\in B,s_{2}\in S_{2}}(\neg b\rightarrow
wpc(s_{2},Q))$ $\displaystyle=\bigcap_{b\in B}(b\rightarrow\bigcap_{s_{1}\in
S_{1}}wpc(s_{1},Q))\cap\bigcap_{b\in B}(\neg b\rightarrow\bigcap_{s_{2}\in
S_{2}}wpc(s_{2},Q))$

Call $P_{1}=\bigcap_{s_{1}\in S_{1}}wpc(s_{1},Q)$ and $P_{2}=\bigcap_{s_{2}\in
S_{2}}wpc(s_{2},Q)$. Call $C=\bigcap_{b\in b}wpc(b,(b_{t}\rightarrow
P_{1})\land(\neg b_{t}\rightarrow P_{2}))$ Now, we know
$\\{\kern-2.15277pt|{P_{1}}|\kern-2.15277pt\\}\>S_{1}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
$\\{\kern-2.15277pt|{P_{2}}|\kern-2.15277pt\\}\>S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
and
$\\{\kern-2.15277pt|{C}|\kern-2.15277pt\\}\>B\>\\{\kern-2.15277pt|(b_{t}\rightarrow
P_{1})\land(\neg b_{t}\rightarrow P_{2})|\kern-2.15277pt\\}$ hold. So we can
apply the ITE rule to prove
$\\{\kern-2.15277pt|{C}|\kern-2.15277pt\\}\>\text{if }B\text{ then
}S_{1}\text{ else }S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.

But we know $P\subseteq C$ from above, so we can Weaken to prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>\text{if }B\text{ then
}S_{1}\text{ else }S_{2}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$. This proof
tree adheres to our skeleton when its hypotheses do.

##### Nonrecursive Nonterminals

Let $N$ be a nonrecursive nonterminal with productions $N_{1},\cdots,N_{m}$.
Suppose
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds. Then observe, we can prove $\\{\kern-2.15277pt|{P_{j}=\bigcap_{n\in
N_{j}}wpc(n,Q)}|\kern-2.15277pt\\}\>N_{j}\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
By applying GrmDisj, we can derive
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
where

$\displaystyle P^{\prime}$ $\displaystyle=\bigcap_{j\leq m}P_{j}$
$\displaystyle=\bigcap_{j\leq m}\bigcap_{n\in N_{j}}wpc(n,Q)$
$\displaystyle=\bigcap_{n\in N}wpc(n,Q)$ $\displaystyle\supseteq P$

So we can apply Weaken on
$\\{\kern-2.15277pt|{P^{\prime}}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
to get
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
Note that, if the hypotheses adhere to the appropriate proof skeletons, this
proof tree does too.

##### Recursive Nonterminals

We assume that all summaries
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
are, with some abuse of notation, $Q_{N}=\bigcup_{n\in
N}(\boldsymbol{x}=\llbracket{n}\rrbracket(\boldsymbol{z}))$. Then, to derive
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
for a true triple
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$,
we have two cases.

First, suppose
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}\in\Gamma$.
Then we use ApplyHP to extract the hypothesis and Adapt to prove the triple
$\\{\kern-2.15277pt|{\forall\boldsymbol{y}.Q_{N}[{y}/{x}][{x}/{z}]\rightarrow
Q[{y}/{x}]}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
Now, since
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds, it must be that, for all $\boldsymbol{x}\in P$, for all $n\in N$,
$\llbracket{n}\rrbracket(\boldsymbol{x})\in Q$. In other words, for all
$\boldsymbol{y}$, so that
$\boldsymbol{y}=\llbracket{n}\rrbracket(\boldsymbol{x})$ for some $n$,
$\boldsymbol{y}\in Q$. But, by definition of $Q_{N}$, this says precisely that
$P\rightarrow(\forall\boldsymbol{y}.Q_{N}[{y}/{x}][{x}/{z}]\rightarrow
Q[{y}/{x}])$. So we can prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
by Weakening from Adapting what we get from ApplyHP. This proof tree adheres
to the skeleton our algorithm returns in this case.

Second, suppose
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
is true but
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}\notin\Gamma$.
Then we must apply the HP rule to prove it. Now, since
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
is true, it must be the case that
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N_{j}\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
holds on each of the production rules $N_{j}$ of $N$. Since our proofs on our
hypotheses return the weakest possible precondition $P_{j}$ for each $N_{j}$,
it must be true that $\boldsymbol{x}=\boldsymbol{z}\rightarrow P_{j}$. Then
the application of the HP rule goes through, and we have proven
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$.
Now, we apply Adapt to it. As in the previous case, for any $P$ so that
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
holds, $P\rightarrow(\forall\boldsymbol{y}.Q_{N}[{y}/{x}][{x}/{z}]\rightarrow
Q[{y}/{x}])$. So we can Weaken from
$\\{\kern-2.15277pt|{\boldsymbol{x}=\boldsymbol{z}}|\kern-2.15277pt\\}\>N\>\\{\kern-2.15277pt|Q_{N}|\kern-2.15277pt\\}$
to prove
$\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$.
Evidently, when the tree’s hypotheses are proven according to the skeleton our
algorithm suggests, the tree itself adheres to the skeleton. ∎

We have shown that, for loop-free programs, W-UL is relatively complete (i.e.,
the claims can be proven up to our ability to check implications). Moreover,
the construction we give to prove any claim
$\Gamma\vdash\\{\kern-2.15277pt|{P}|\kern-2.15277pt\\}\>S\>\\{\kern-2.15277pt|Q|\kern-2.15277pt\\}$
adheres exactly to the proof skeleton our algorithm from § 4.1 produces. This
not only proves relative completeness, but also proves Theorem 4.1.

Moreover, we only require $Q_{N}$ to reason about $\boldsymbol{x}$ and
$\boldsymbol{z}$. Thus, replacing summaries with parameters over
$\boldsymbol{x}$ and $\boldsymbol{z}$ does not limit our ability to express
most general formulas. This demonstrates that, for loop-free programs,
introducing parameters in place of unknowns in the way that we do does not
impact our ability to derive a claim. This gives Corollary 4.5.

Trivially, this result extends to the generated SyGuS problem.

##  Appendix B Appendix: Vector State Inference Rules

Int
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{i}/{e_{t}}]}|\kern-1.72221pt\\}\>i\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
True
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{{{\mathsf{true}}}}/{b_{t}}]}|\kern-1.72221pt\\}\>{{\mathsf{true}}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
False
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{{{\mathsf{false}}}}/{b_{t}}]}|\kern-1.72221pt\\}\>{{\mathsf{false}}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Var
$\Gamma\vdash\\{\kern-1.72221pt|{Q[{x}/{e_{t}}]}|\kern-1.72221pt\\}\>x\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B\>\\{\kern-1.72221pt|Q[{\neg
b_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ Not
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>\neg
B\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ .
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\>\\{\kern-1.72221pt|R[{e_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>E_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\oplus
e_{t}}/{e_{t}}]|\kern-1.72221pt\\}$ Bin
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\oplus
E_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ .
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B_{1}\>\\{\kern-1.72221pt|R[{b_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>B_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\land
b_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ And
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B_{1}\land
B_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\>\\{\kern-1.72221pt|R[{e_{t}}/{x_{1}}]|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>E_{2}\>\\{\kern-1.72221pt|Q[{x_{1}\odot
e_{t}}/{b_{t}}]|\kern-1.72221pt\\}$ Comp
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E_{1}\odot
E_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$ Rules for Expressions

$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>E\>\\{\kern-1.72221pt|Q[{e_{t}}/{x}]|\kern-1.72221pt\\}$
Assign $\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>{{x}\
\mathsf{:=}\ {E}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>S_{1}\>\\{\kern-1.72221pt|R|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{R}|\kern-1.72221pt\\}\>S_{2}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Seq
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>{S_{1}}{\mathsf{;}}\
{S_{2}}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\\{|P|\\}B\\{|b_{loop}=b_{t}\rightarrow
P_{1}[{\boldsymbol{x}}/{\boldsymbol{z}}]|\\}$
$\\{|P_{1}|\\}S_{1}\\{|P_{2}[{\boldsymbol{z}}/{\boldsymbol{x}}][{\boldsymbol{x}}/{\boldsymbol{y}}]|\\}$
$\\{|P_{2}|\\}S_{2}\\{|T(Q)|\\}$ VS-If $\\{|P|\\}{\mathsf{if}}\ {B}\
{\mathsf{then}}\ {S_{1}}\ {\mathsf{else}}\ {S_{2}}\\{|Q|\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>B\>\\{\kern-1.72221pt|(\forall
i.\neg b_{t}[i])|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{I}|\kern-1.72221pt\\}\>{\mathsf{if}}\ {B}\
{\mathsf{then}}\ {S}\ {\mathsf{else}}\
{\text{skip}}\>\\{\kern-1.72221pt|I|\kern-1.72221pt\\}$ VS-While
$\Gamma\vdash\\{\kern-1.72221pt|{I}|\kern-1.72221pt\\}\>\mathsf{while}\;{B}\;\mathsf{do}\;{S}\>\\{\kern-1.72221pt|I\land
P[{b_{fresh}}/{b_{t}}]\land(\forall i.\neg b_{t}[i])|\kern-1.72221pt\\}$ Rules
for Statements

$\Gamma_{1}\vdash\\{\kern-1.72221pt|{P_{1}}|\kern-1.72221pt\\}\>N_{1}\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$\cdots$
$\Gamma_{1}\vdash\\{\kern-1.72221pt|{P_{n}}|\kern-1.72221pt\\}\>N_{n}\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$x=z\rightarrow\bigwedge\limits_{1\leq j\leq n}P_{j}$ HP
$\Gamma\vdash\\{\kern-1.72221pt|{x=z}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q_{N}|\kern-1.72221pt\\}$
$\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}\in\Gamma$
ApplyHP
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Adapt $\Gamma\vdash\\{\kern-1.72221pt|{\forall y.((\forall u.(P\rightarrow
Q[{y}/{x}]))\rightarrow
R[{y}/{x}])}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|R|\kern-1.72221pt\\}$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{1}}|\kern-1.72221pt\\}\>N_{1}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
$\cdots$
$\Gamma\vdash\\{\kern-1.72221pt|{P_{n}}|\kern-1.72221pt\\}\>N_{n}\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
GrmDisj
$\Gamma\vdash\\{\kern-1.72221pt|{\bigwedge\limits_{j=1}^{n}P_{j}}|\kern-1.72221pt\\}\>N\>\\{\kern-1.72221pt|Q|\kern-1.72221pt\\}$
Rules for Nonterminals