Alignment complete relational Hoare logics for some and all

Ramana Nagasamudram
Stevens Institute of TechnologyUSA
Anindya Banerjee
IMDEA Software InstituteSpain
Banerjee’s research was based on work supported by the NSF, while working at the Foundation. Any opinions, findings, and conclusions or recommendations expressed in this article are those of the authors and do not necessarily reflect the views of the NSF.
David A. Naumann
Stevens Institute of TechnologyUSA

Nagasamudram and Naumann were partially supported by
NSF grant CNS 1718713.

In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments of executions.  Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A single degenerate alignment rule (self-composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the ordinary logical sense. The notion of alignment completeness was previously proposed as a more satisfactory measure, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. This paper proves alignment completeness with respect to a general class of $\forall\forall$ alignment automata, for a RHL comprised of standard rules together with  a rule of semantics-preserving rewrites based on Kleene algebra with tests. We also give a new logic for $\forall\exists$ properties and prove its alignment completeness.

§ INTRODUCTION

A ubiquitous problem in programming is reasoning about relational properties, such as equivalence between two programs in the sense that from any given input they produce the same output.  Relational properties are also of interest for a single program. For example, a basic notion in security is noninterference: any two executions with the same public inputs should result in the same public outputs, even if the secret inputs differ.
We write $c\sep c':\rspec{\R}{\S}$ to say program $c$ relates to $c'$ in the sense that
for any pair of initial states related by $\R$, and terminated executions of $c$ and $c'$ from those states,
the final states are related by $\S$.
Another kind of relational property is written $c\sep c': \aespec{\R}{\S}$.  It says that from any $\R$-related pair of initial states, and for any terminated run of $c$ from the left state, there is a terminated run of $c'$ from the right state such that $\S$ relates the final states.  For example, a standard notion of refinement is obtained by taking $\R$ and $\S$ to be the identity.
For brevity we refer to the two kinds of properties as $\forall\forall$ and $\forall\exists$, in reference to their quantification over executions.

Often a pair of executions are similar, e.g., because the related programs are similar, or even the same as in the case of noninterference.  So reasoning often relies on the alignment of similar steps —think of a programmer viewing two versions of a similar program, side by side on screen.  Having chosen to align a pair of points in control flow, one can consider a relational assertion that may hold whenever execution reaches those points.

Most work on formal reasoning about relational properties has focused on $\forall\forall$ properties.
There are two main approaches.
One is deductive systems inspired by Hoare logic (HL), which we call relational Hoare logics (RHLs) <cit.>.
The other approach is to reason about program semantics in the form of a transition system or automaton,
adapting the inductive assertion method <cit.> (IAM) to use relational assertions at aligned pairs of control points.
By representing the programs as automata one can easily express which control points are meant to be aligned,
including alignments conditioned on the programs' data.
In case the program transition relation(s) can be expressed in a solvable fragment of first order logic, it is even possible to automatically infer alignment conditions and relational assertions, using proof search in the constraint language instead of proof search in a logic of
programs <cit.>.
Deductive systems, however, are needed to account for composing proofs about program components.
Moreover, because a deductive system applies to ordinary program syntax, it caters for human interaction which is essential for verification of programs involving dynamically allocated data and other features for which program semantics and/or specifications are not easily expressible in solvable fragments.

Aside from soundness, the fundamental criterion for a good deductive system is completeness: anything true should be provable.  For program logics one seeks Cook's relative completeness <cit.>,
factoring out completeness and expressiveness of the assertion logic.

The problem we address is that Cook completeness is unsatisfactory for RHLs.
Consider this sound rule: from $c\sep\skipc: \rspec{\R}{\Q}$ and $\skipc\sep c':\rspec{\Q}{\S}$ infer
$c\sep c':\rspec{\R}{\S}$.
The rule shows how deductive rules can embody alignments,
in this case a sequential alignment wherein the final state of $c$ is aligned with the initial state of $c'$.
Under mild assumptions about encoding a pair of states as a single state, and thereby treating a relation as a unary assertion, the premises can be expressed as
partial correctness judgments in HL <cit.>.

The rule, together with a complete set of unary rules, provides a Cook complete relational
logic <cit.>.

Sequential alignment is unsatisfactory. Consider proving $c\sep c:\rspec{\I}{\I}$ where $\I$ is a conjunction of equalities, one for each variable of $c$.
Surely $c$ is equivalent to itself.
By aligning $c$ with itself step by step, the only intermediate assertion we need is $\I$ —whereas for reasoning about the sequential alignment, the intermediate assertion $\Q$ may have to “remember everything” <cit.> about $c$. Good alignment is essential for relational verification because it enables the use of relatively simple assertions <cit.>.
As an example how better alignments can be formalized, here is a standard rule of RHL:
from $c\sep c':\rspec{\R}{\Q}$ and $d\sep d':\rspec{\Q}{\S}$ infer $c;d\sep c';d':\rspec{\R}{\S}$.

The notion of alignment completeness has been proposed as means to evaluate RHLs <cit.>.
Although alignment does not exist explicitly in an RHL or its semantics, a precise definition can be formulated taking into account that an alignment-based proof uses intermediate assertions. Here's the idea: For any valid alignment-based proof there should be a proof of the same judgment in the RHL using the same assertions.
The approach of NagasamudramN21 uses automata to represent alignments and IAM proofs
(as in e.g. <cit.>).
In <cit.>, alignment completeness results are given for $\forall\forall$ properties and several very specialized kinds of automata.
In a nutshell, we make two contributions: first, we answer their challenge to obtain alignment completeness for
a general class of $\forall\forall$ alignment automata.
Second, we introduce a new logic for $\forall\exists$ properties and prove its alignment completeness.

Challenge: Find an interesting/useful general class of alignment automata. A key requirement is that the automaton be adequate in the sense of covering all pairs of executions.  Adequacy has been worked out in several independent works (with terminology like “fair scheduler”), for $\forall\forall$ properties, but there is no standard theory, and there's little relevant work on $\forall\exists$.
Our solution is in Sect. <ref>.

Challenge: Find a good set of RHL rules.  In this paper we confine attention to simple imperative programs but, even so, a large number of rules can be found in the $\forall\forall$ RHL literature, and there is little prior work on $\forall\exists$ RHLs.  For $\forall\forall$, several rules seem to be needed to account for the many possible program structures one may wish to align, e.g., relating a loop to a sequence of loops.  The key to addressing this challenge is for the deductive system to include some form of semantics-preserving rewriting, so programs can be rewritten to have more similar control structure for which fewer rules are needed.
Our $\forall\forall$ (resp. $\forall\exists$) logic is in Sect. <ref> (resp. <ref>).

Challenge: Find a sensible notion of equivalence for use in rewriting.
Prior works that appeal to rewriting use ad hoc sets of rewrite rules, which raises a fresh question about completeness.  Another question is whether equivalence should be a distinct judgment as opposed to a special case of the main relational judgment, and if so, should it involve preconditions.

Challenge: Find a systematic way to obtain deductive proofs from automata-based ones.

Our answer to the latter two challenges is a technical result which underlies our completeness results:
We show that every program can be rewritten, using laws of Kleene algebra with tests (KAT) <cit.>, into “automaton normal form” which mimics its transition system representation (Sect. <ref>).
As noted in the related work Section <ref>, this is not too surprising
but the specific form is new and plays a crucial role in proving the main results.

* We show that RHL+, a logic featuring a KAT-based rewrite rule (Fig. <ref>), is alignment complete for $\forall\forall$ proofs based on a general class of alignment automata
(Sect. <ref>).[This result appears in our unpublished preprint <cit.> which is superceded by this document.]

* We introduce ERHL+ and show it is alignment complete for
proofs of $\forall\exists$ properties using a general class of alignment automata.
(Sect. <ref>).

As a conceptual contribution, we show that the core rules of RHL for imperative programs should comprise
(a) one-sided rules for primitives,
(b) same-structure rules for sequence, conditional and (conditionally aligned) loop,
and (c) rewriting a program to an unconditionally equivalent one.
Without these, a logic is unlikely to be alignment complete.

For $\forall\exists$ our automata formulation (in Sect. <ref>)
shows that to prove a $\forall\exists$-spec $\aespec{\R}{\S}$, instead of explicitly constructing a positive witness of the existential <cit.>
one can instead filter out the non-witnesses on the right, so what's left satisfies the corresponding $\forall\forall$-spec $\rspec{\R}{\S}$.  All for some!

In practice, many verification tools work directly with verification conditions, although some interactive tools are directly based on a HL (e.g., <cit.>). Deductive systems are nonetheless important for various reasons.  One practical use for deductive rules is for independently checkable certificates to represent proofs that may be found by other means.  The alignment completeness result shows that, as in the case of unary HL, a small collection of mostly syntax-directed rules suffices to represent proofs of relational correctness judgments.
Deductive systems also represent principles beyond IAM, including procedure-modular reasoning
and disjunction (resp. conjunction) of preconditions (resp. postconditions).  For relational verification there is vertical (i.e., transitive) composition, which is sound for $\forall\exists$ but not $\forall\forall$ <cit.>.
This makes $\forall\exists$ logic useful even for deterministic programs.

This version includes a hyperlinked appendix containing proofs, additional details, and examples.
Green boxes in the right margin link to (and indicate page numbers of) proofs in the appendix.

§ OVERVIEW

A first example
Floyd's formulation of the IAM is based on annotation of control points.
We use Dijkstra's guarded command syntax but with labelled control points.
This somewhat silly command $c0$ will be a running example.
Here $\mod$ means remainder.

\[ \graybox{c0:} \quad
\lassg{1}{x}{y} ;
\keyw{do}^2 x > 0 \gcto
\begin{array}[t]{l}
\keyw{if}^3 \: x\mod 2 = 0 \gcto \lassg{4}{x}{x-1} \\
\gcsep \: x\mod 2 \neq 0 \gcto \lassg{5}{x}{x-2}
~ \keyw{fi} ~ \keyw{od}
\end{array}
\]

To reason about this program in relation to itself, we use
the formula $x=x'$ to relate two stores, where $x'$ refers to the value of $x$ in the second store.
We aim to prove $c0\sep c0:\rspec{y=y'}{x=x'}$,
which says any two runs of $c0$, from initial stores that agree on $y$, result in final stores that agree on $x$.
Pairs of runs can be represented by executions of a product automaton whose control is successively the same control point on left and right.  An IAM-style proof annotates each $(n,n)$ with the relation $x=x'$, except for $(1,1)$ which is annotated by the precondition $y=y'$.
A deductive proof formulates such lockstep alignment
using rules like rSeq (Fig. <ref>) and rAsgnAsgn (Fig. <ref>).
A sequential product automaton would run the left execution to completion and then the right, annotated with more complicated assertions than $x=x'$.  Such a proof can be presented using the sequential alignment rule mentioned in Sect. <ref> (cf. rLRseq in Fig. <ref>).

Nondeterminacy and $\forall\exists$ judgments

While $\forall\forall$ specs capture a wide class of requirements, they
do not express all interesting properties of nondeterministic programs.
Consider the command $\lhavc{}{x}$ which sets $x$ to any integer.
The $\forall\forall$ judgment
$\lhavc{}{x}\sep\lhavc{}{x'} : \rspec{\mathit{true}}{x=x'}$ does not
hold.[By the relation $x=x'$, we mean that the value of $x$ in the left
state is equal to value of $x'$ in the right state.]

However, for every execution of $\lhavc{}{x}$, there exists an execution of
$\lhavc{}{x'}$ such that $x = x'$.
This property is captured by the $\forall\exists$ judgment
$\lhavc{}{x}\sep\lhavc{}{x'} : \aespec{\mathit{true}}{x=x'}$.  We establish this
judgment by picking an alignment and, in addition, a way of filtering out
executions of the right program that violate the post-relation.  One proof uses  sequential
alignment that performs $\lhavc{}{x}$ followed by $\lhavc{}{x'}$.
Filtering is achieved by assuming the relation $x = x'$ after the
$\lhavc{}{x'}$ on the right.
In other words, to establish $x = x'$, we only consider executions of
$\lhavc{}{x'}$ which set $x'$ be equal to $x$.

Filtering conditions are sound provided they permit all executions of the left
program and at least one execution of the right program.  In this example, the
filtering condition $x = x'$ is justified because for every possible value of
$x$ produced by $\lhavc{}{x}$, there exists a matching value of $x'$ that can be
produced by $\lhavc{}{x'}$.
An alignment automaton that enforces the filter
effectively reduces the $\forall\exists$ to a $\forall\forall$ property that can be proved by IAM.

In our deductive logic, assumptions are expressed by preconditions and postconditions
in $\aespecSym$ specs.  We do not use verification exotica like assume statements or nonstandard program semantics.

Possibilistic Noninterference

For a more involved example with nondeterminism, consider the following program
adapted from Unno et al <cit.>.
It illustrates how alignment facilitates use of simple conditions for filtering.

\[
\begin{array}{ll@{\;}l}
\graybox{$c1:$}
& \keyw{if}^1 \vhigh \neq 0 \gcto & \lhavc{2}{x}; \\
& & \!\!\!\begin{array}[t]{l}
\keyw{if}^3\ x \geq \vlow \gcto \lskipc{4}
\gcsep\ x < \vlow \gcto \ldogc{4}{\mathit{true}\gcto\lskipc{6}}\ \keyw{fi}
\end{array} \\
& \gcsep \ \ \vhigh = 0 \gcto & \lassg{7}{x}{\vlow};\ \lhavc{8}{b};\ \lskipc{9}; \\
& & \ldogc{10}{b \neq 0 \gcto \lassg{11}{x}{x+1};\ \lhavc{12}{b};\ \lskipc{13}}
\quad\keyw{fi}
%\\ & \keyw{fi}
\end{array}
\]

It satisfies a possibilistic noninterference property: from low-equivalent
states, for any terminated execution of $c1$, there exists an execution of $c1$
such that the final values of $x$ in both states are in agreement.
This is expressed by the judgment $c1\sep c1 : \aespec{\vlow=\vlow'}{x=x'}$.

We verify this property of $c1$ by choosing a convenient alignment and a
collection of filtering conditions associated with aligned points.
The alignment can be described as follows.
Align both copies of $c1$ in lockstep if they take the same branch of the
conditional at label $1$, i.e., if the two initial states agree on the test
$\vhigh\neq0$.  Otherwise, use a sequential alignment: execute the left copy
until it terminates, and then execute the right copy.

Suppose $\vhigh\neq 0$ in both initial states, so we reason in terms of a lockstep alignment.
We filter right executions to obtain the judgment
$\lhavc{2}{x}\sep\lhavc{2}{x} : \aespec{\vhigh\neq 0\land \vhigh'\neq 0}{x=x'}$.
The necessary filtering is conditioned on a pair of
control points: if control on both sides reaches label 3, the label after the
havocs of $x$, assume $x = x'$.  This assumption is justified since $\lhavc{2}{x}$
on the right can set $x$ to a value that matches the value of $x$ in the left
state.  Having established $x = x'$ after the two havocs, it's easy to prove
that the post-relation $x = x'$ is satisfied.  Notice that the diverging loop at
label 4 does not falsify the noninterference property since we are only
interested in pairs of executions where the left copy of $c1$ has terminated.

The case where $\vhigh = 0$ holds in both initial states is similar.
Nondeterminacy on the right is resolved, using filters expressed as relational
assumptions, so that agreement on the value of $b$ in the two states is

Now suppose $\vhigh \neq 0$ and $\vhigh' = 0$, for which we have a sequential alignment.
The left copy of $c1$ might not terminate due to the loop at label 4, but if it
does, we have $x \geq \vlow$.  The right copy of $c1$ first sets $x$ to $\vlow$
and then increments $x$ some nondeterministically chosen number of times.  We
can prove $x = x'$ on termination by filtering executions so that we maintain
$x - x' = b'$ as an invariant of the loop at label 10.  Intuitively, we only
permit right executions where $\lhavc{8}{b}$ sets $b$ to the difference between
the value of $x$ on the left and $x$ on the right, and $\lhavc{12}{b}$ in the
loop decrements $b$ by 1.  Since the noninterference judgment requires proving
the existence of right executions, we must reason about termination in this
case.  The value of $b$ can be used as a variant of the loop at label 10.  By
our chosen filtering conditions, this quantity decreases in each iteration and
it cannot decrease infinitely.

The same alignment is used when $\vhigh = 0$ and $\vhigh' \neq 0$.  The key idea
in this case is to resolve $\lhavc{2}{x}$ on the right so that $x' \geq \vlow$
and the right execution never reaches the diverging loop at control point 4.
This is done by proving that if the left copy of $c1$ terminates, then we have
$x \geq low$.  Then, filtering right executions so you have agreement on $x$
after $\lhavc{2}{x}$ ensures termination and satisfies the post-relation
$x = x'$.

Alignment completeness

The examples show the value of good alignment for both $\forall\forall$ and $\forall\exists$ relational reasoning.
They also show that a deductive system must cater for relating similar and different programs,
to express various alignments. And for $\forall\exists$, filtering must be expressed somehow,
without allowing unjustified assumptions.
Our main results show that for a minimal set of rules it suffices to have one-sided rules
for primitives (e.g., rAsgnSkip and rSkipAsgn in Fig. <ref>)
and same-structure rules for control structure (e.g., rSeq in Fig. <ref>).
The examples show the need for alignment conditioned on data, and our main results
show that it suffices to have conditional alignment in the loop rule.
A key rule allows rewriting the programs into equivalent ones with different control structure.
Completeness ensures that, though we may like to derive additional convenient rules within the deductive system, we never need to make recourse to the underlying semantics.

In a human guided deductive proof one should rewrite the programs as little as possible, just enough
to express a desired alignment.  (Or alternatively, use rewriting to derive a rule suited to the particular programs.)
However, for the theoretical purpose of proving alignment completeness
we go to the opposite extreme, rewriting the program into a normal form like a fetch-execute loop.

By “compiling” programs we make it possible to obtain a deductive proof from an IAM-style proof in the form of an aligned and annotated product automaton.
The idea can be explained most simply by considering unary correctness.
Suppose we have an IAM proof that $c0$ satisfies an ordinary pre-post spec,  so there is an inductive annotation of its control points.
Instrument the program with a fresh variable $pc$ serving as program counter. We write $\spc n$ to abbreviate $pc:=n$
and $\tpc n$ to abbreviate the expression $pc=n$. The result looks
as follows, using 6 as a final control point, which in IAM is annotated with the postcondition.

\[
\begin{array}{l}
\graybox{$c0^+:$} \quad
\spc 1; \lassg{1}{x}{y} ;
\spc 2; \keyw{do}^2 x > 0 \gcto
\spc 3; \!\!\!\begin{array}[t]{l}
\keyw{if}^3  x\mod 2 = 0 \gcto \spc 4;\lassg{4}{x}{x-1} \\
\gcsep x\mod 2 \neq 0 \gcto \spc 5;\lassg{5}{x}{x-2}
~ \keyw{fi} ~ ; \spc 2 ~ \keyw{od}
\,;\; \spc 6
\end{array}
\end{array}
\]

Using simple transformations, this can be rewritten into this equivalent form:
$\spc 1; d0$ where

\[ \begin{array}[t]{lllll}
\graybox{d0:}\quad \keyw{do}
& \tpc 1 \gcto x:=y; \spc 2
& \gcsep \tpc 3 \land x\mod 2=0 \gcto \spc 4
&  \gcsep \tpc 4 \gcto \lassg{}{x}{x-1}; \spc 2 \\
&  \gcsep \tpc 2 \land x > 0 \gcto \spc 3
& \gcsep \tpc 3 \land x\mod 2\neq 0 \gcto \spc 5
& \gcsep \tpc 5 \gcto \lassg{}{x}{x-2}; \spc 2 \\
&  \gcsep \tpc 2 \land x \ngtr 0 \gcto \spc 6  & & &  \keyw{od}
\end{array}
\]

For loop invariant we use
$1 \leq pc \leq 6 \land (\land i : 0\leq i\leq 6 : pc=i \imp an(i))$
where $an(i)$ is the given annotation at control point $i$.
To use the loop rule (Fig. <ref>) there is a premise for each guarded command in $d0$, and each of these corresponds closely to one of the verification conditions in the IAM proof, so the premise can be proved using assignment, sequence, and consequence rules.
Thus we get that $\spc 1; d0$ satisfies the spec.  Then, since
$\spc 1;d0$ is equivalent to $c0^+$, so by the Rewrite rule we have that $c0^+$ satisfies the spec. But $pc$ is fresh so the rule for ghost variables lets us erase the instrumentation.
Erasing produces extraneous skips; these are removed by another application of Rewrite,
completing the proof that $c0$ satisfies the spec.
All assertions used in this proof are essentially boolean combinations of
the assertions in the IAM proof.

This argument works for any IAM proof of a unary property, owing to our normal
form Theorem <ref> that says any program, instrumented with $pc$, is equivalent to one
in automaton normal form.
The general result, called Floyd completeness, is Theorem <ref>.

The same approach works to prove alignment
completeness.  Given an IAM-style proof using an alignment product, compile each
of the programs to its normal form. Instantiate the relational loop rule
(rDo in Fig. <ref>, eDo in Fig. <ref>) using the
automaton's alignment conditions $L,R$.  The side conditions of the loop rule
follow from assumed adequacy conditions of the automaton-based proof.  The
premises of the loop rule correspond to the verification conditions of the

There are a number of technical challenges to work out these ideas in detail.
Many of the details needed for
the $\forall\forall$ in Sect. <ref>
are also used for the $\forall\exists$ alignment completeness
result where there are additional complications about the
filtering conditions and well-founded right-side alignment.
Sect. <ref> presents the $\forall\forall$ logic.
Sect. <ref> develops alignment products and their verification conditions for $\forall\forall$ properties,
as needed for the alignment completeness theorem
in Sect. <ref>.
Sect. <ref> develops the normal form.
The additions needed for filtering automata and their VCs,
and the $\forall\exists$ deductive system,
are deferred to Sect. <ref>.

§ THE PROGRAMMING LANGUAGE AND ITS $\FORALL\FORALL$ RELATIONAL HOARE LOGIC

The labelled guarded command syntax is defined as follows, where
$x$ ranges over the set $\Var$ of integer variables, $e$ ranges over integer and boolean expressions, $n$ ranges over integer literals.

\[ \begin{array}[t]{lcl}
c & ::= & \lskipc{n} \:\mid\: \lassg{n}{x}{e} \:\mid\: \lhavc{n}{x} \:\mid\: c;c
\:\mid\: \lifgc{n}{gcs} \:\mid\: \ldogc{n}{gcs} \\
gcs & ::= & e \gcto c \:\mid\: e \gcto c \gcsep gcs
\end{array} \]

We omit details about expressions except to note that boolean expressions are given from some primitives $bprim$ and the logical operators are written $\land,\lor,\neg$.
A guarded command has the form $e \gcto c$ where $e$ is a boolean expression.
The category $gcs$ is essentially non-empty lists of guarded commands and we sometimes treat it as such. The havoc command $\lhavc{n}{x}$ nondeterministically assigns any integer to $x$;
it can model inputs, randomization, and unknowns.

Later we define a predicate, $\ok$, on commands that says their labels are unique and positive.  Labels play an important role in some results, for which the $\ok$ condition is needed. But many definitions and results do not involve labels or require $\ok$; for those definitions and results we omit labels, meaning that any labels are allowed.

Programs act on variable stores, i.e., total functions $\Var\to\Z$.
Later we consider automata, with arbitrary sets of stores that need not be variable stores,
and the term “state” will refer to a store together with a control point.
In this section we say simply “store”, meaning variable store.
We assume expressions $e$ are always defined.
We write $\means{e}(s)$ for the value of expression $e$ in store $s$.
In case $e$ is a boolean expression, the value is in $\{true,\mathit{false}\}$; otherwise
it is in $\Z$.
We standard big-step semantics and
write $\means{c}\, s\, t$ to express that from initial store $s$ the command $c$ can terminate with final store $t$.
We call $\means{c}$ the denotation of $c$.

The standard semantics for guarded commands considers $\lifgc{}{gcs}$ to fail if none of its guards is enabled <cit.>.
Modeling failure would clutter the semantics without shedding any light,
so we disallow such ifs, as follows.
Define $\enab(gcs)$ as the disjunction of the guards.
For example, $\enab(x>0\gcto y:=1 \gcsep z < 1\gcto y:=2)$ is the expression $x>0 \lor z<1$.

A command $c$ is well formed if
(a) $c$ is typable in the sense that guards are boolean expressions and both integer and boolean operators are used sensibly, considering that all variables have type int; and
(b) $c$ satisfies the $\totalIf$ condition which says:[It is not difficult to enforce this syntactically.]
for every subprogram $\lifgc{}{gcs}$ of $c$, $\means{\enab(gcs)}=\means{true}$.
In the sequel we say command to mean well formed command.
Such commands comprise the guarded command language, (GCL).

Program logic

Our relational logics are not based on unary HL, but for expository purposes we touch on HL at several points.
The partial correctness judgment is written $c:\spec{P}{Q}$ rather than the conventional $\{P\}c\{Q\}$.
To focus on what's interesting
we treat assertions as shallowly embedded <cit.>,
so $P$ and $Q$ are sets of stores.
But we use formula notation for clarity, e.g., $P\land Q$ means their intersection.
A boolean expression $e$ in a formula stands for $\{s\mid\means{e}(s)=true\}$,
which we sometimes write as $\means{e}$.
For a set $P$ of variable stores, we use substitution notation $\subst{P}{x}{e}$
with standard meaning: $s$ is in $\subst{P}{x}{e}$ iff the updated store
$\update{s}{x}{\means{e}(s)}$ is in $P$.
Quantifiers, as operators on store sets, are defined by
$\graybox{$\someSet{x}{P}$} \eqdef \{ s \mid \all{v\in\Z}{s\in \subst{P}{x}{v}} \}$
$\graybox{$\allSet{x}{P}$} \eqdef \{ s \mid \some{v\in\Z}{s\in \subst{P}{x}{v}} \}$.
Define $\indep(x,P)$ to mean that $P=\someSet{x}{P}$,
that is, $P$ is independent of $x$.

We use $\models$ to indicate valid correctness judgment, defined as follows:

\(\graybox{$\models c: \spec{P}{Q}$}
\eqdef
\mbox{For all $s,t$ such that
$\means{c}\, s\, t$,
if $s\in P$ then $t\in Q$.}
\)

c: PQ

d: PQ

c: PQ

(x,c) : PQ

c: ePP

gcs: PP(gcs)

Selected proof rules of HL+
(see Fig. <ref> for the others).

The proof system we call HL+ comprises the standard rules of HL plus a rule for elimination of ghost variables <cit.> and a rule for rewriting programs
(Figure <ref>).
Define $\ghost(x,c)$ to mean that variable $x$ occurs in $c$ only in assignments to $x$
and havocs of $x$.
Define $\erase(x,c)$ to be $c$ with every assignment to $x$, and havoc of $x$, replaced by skip.

Because we are using shallow embedding for assertions, HL+ does not need to be accompanied by a formal system for proving entailments between assertions.
But the logic also uses command equality $c\kateq d$, in rule Rewrite.
For this we rely on KAT as formalized in Sect. <ref>.
For soundness of rule rewrite we just need that the relation $\kateq$ implies equal denotations.

Relational specs and proof rules

For relational pre- and post-conditions we use (binary) relations on stores,
by shallow embedding just like for unary predicates.
To express that a unary predicate holds in the left store of a pair,
we write $\leftF{P}$ for the set of pairs $(s,t)$ where $s\in P$.
Similarly, $\rightF{P}$ is the set of $(s,t)$ where $t\in P$.
Combined with our coercion of boolean expressions $e$ to predicates,
$\leftF{e}$ says that $e$ is true in the left store.
By contrast with the informal overview Section <ref>,
we do not rely on primed identifiers to express relations
(but do use primed metavariables for the right element of pairs that pertain to two runs).
$\bothF{P\sep Q}$ abbreviates  $\leftF{P}\land\rightF{Q}$,
and $\bothF{P}$ abbreviates  $\bothF{P\sep P}$.
We also write $\leftex{e}=\rightex{e'}$ for the set of $(s,t)$ where
$\means{e}(s) = \means{e'}(t)$.

For relation $\R$ on stores we write
$\subst{\R}{x\smSep}{e\smSep}$ for substitution of $e$ for $x$ in the left store.
Similarly $\subst{\R}{\smSep x}{\smSep e}$ substitutes on the right
and $\subst{\R}{x\smSep x'}{e\smSep e'}$ does both.

We write $\someSet{x\smSep x'}{\R}$ for quantification over $x$ on the left side and $x'$ on the right.
Specifically, $\graybox{$\someSet{x\smSep x'}{\R}$}
\eqdef\{(s,s')\mid \some{v,v'}{ (s,s')\in \subst{\R}{x\smSep x'}{v\smSep v'} } \}$.
Define $\indep(x|x',\R)$ iff $\R = \someSet{x|x'}{\R}$.

We also need one-sided quantifier forms, and note that
$(\allSet{x\smSep x'}{\R}) = \allSet{x\smSep}{(\allSet{\smSep x'}{\R})}$.
For store relations $\R,\S$,
a relational spec is written $\rspec{\R}{\S}$.
We use $\models$ to indicate valid judgment,
and define $\models c\sep c': \rspec{\R}{\S}$ $\eqdef$

\[
\mbox{For all $s,s',t,t'$ such that
$\means{c}\, s\, t$ and $\means{c'}\, s'\, t'$,
if $(s,s')\in \R$ then $(t,t')\in \S$.}
\]

(x,c)(x',c') :

[rRewrite] cc':

xe : x|e|

xe : |x|e

x: (x)

x: (x)

cc' :

dd' :

c;d c';d' :

cc' : ee'

gcs gcs' :

c: e

c' : e'

cc' : ee'

((gcs) = (gcs')

gcs gcs' : (gcs)(gcs')

cd :

cd :

cd :

cd :

cd :

cd : 𝑓𝑎𝑙𝑠𝑒

The rules of RHL+

xe x'e' : x|x'e|e'

xx' : (xx')

c' :

cc' :

c' :

cc' :

Some derived rules of RHL+

Fig. <ref> gives the proof rules of RHL+.
We are not aware of a prior RHL that has been formulated for GCL,
but the rules are straightforward adaptations of rules found in prior work.
Rules such as the same-branch-if rule popular in RHLs <cit.>
are easily derived, as are rules relating different control structures
(see Fig. <ref> and Sect. <ref>).

§ ALIGNMENT AUTOMATA, ADEQUACY, AND VERIFICATION CONDITIONS

§.§ Automata, alignment automata and adequacy

An automaton <cit.> is a tuple
\( (Ctrl,Sto,\init,\fin,\trans) \)
where $Sto$ is a set (called the data stores),
$Ctrl$ is a finite set (the control points)
that contains distinct elements $\init$ and $\fin$,
and ${\trans} \subseteq (Ctrl\times Sto)\times(Ctrl\times Sto)$ is the transition relation.
We require
$(n,s)\trans (m,t)$ to imply $n\neq \fin$ and $n\neq m$
and call these the finality and non-stuttering conditions respectively.
Absence of stuttering loses no generality and facilitates definitions involving product automata.
A state of the automaton is an element of $Ctrl\times Sto$.

We use the term “alignment product” informally, in reference to various constructions in the literature.
We define a particular construction that we call alignment automaton.

Let $A = (Ctrl,Sto,\init,\fin,\trans)$ and
$A' = (Ctrl',Sto',\init',\fin',\trans')$ be automata.
Let $L$, $R$, and $J$ be subsets of $(Ctrl\times Ctrl')\times (Sto\times Sto')$
that are live for automata $A,A'$, meaning that:
\( \begin{array}[t]{l}
\all{ ((n,n'),(s,s'))\in L }{(n,s)\in\dom(\trans) }, \\
\all{ ((n,n'),(s,s'))\in R }{(n',s')\in\dom(\trans') }, \mbox{and}\\
\all{ ((n,n'),(s,s'))\in J }{(n,s)\in\dom(\trans) \land (n',s')\in\dom(\trans')}
\end{array}\).

The alignment automaton $\aprod(A,A',L,R,J)$ is
the automaton

\[ ((Ctrl\times Ctrl'), (Sto\times Sto'), (\init,\init'), (\fin,\fin'), \biTrans) \]

where $\biTrans$ is defined by:
$((n,n'),(s,s')) \biTrans ((m,m'),(t,t'))$ iff one of these conditions holds:

LO:  $((n,n'),(s,s'))\in L$ and
$(n,s)\trans(m,t)$ and $(n',s')=(m',t')$

RO:  $((n,n'),(s,s'))\in R$ and
$(n,s)=(m,t)$ and $(n',s')\trans'(m',t')$

JO:  $((n,n'),(s,s'))\in J$
and $(n,s)\trans(m,t)$ and $(n',s')\trans'(m',t')$

Notice that the states of $\aprod(A,A',L,R,J)$ are
$((Ctrl\times Ctrl')\times (Sto\times Sto'))$
according to Def. <ref>.
So the alignment conditions $L$, $R$, and $J$ are sets of alignment automaton states.
We write $[n|n']$ for the set of states where control is at $(n,n')$, i.e.,
\( \graybox{$[n|n']$} \eqdef \{ ((i,i'),(s,s')) \mid n=i \land n'=i'\} \).
For example $[\fin|\fin']$ is the set of terminated states.
Similarly, let $\graybox{$[n|*]$} \eqdef \{ ((i,i'),(s,s')) \mid n=i \}$.

Roughly speaking, taking $L$ and $R$ to be false and $J$ true, we obtain an automaton that runs $A$ and $A'$ in lockstep.
Taking $L,R,J$ all true, we obtain a nondeterministic alignment automaton that represents very many alignments.  Taking $L,R,J$ all false, we obtain an alignment automaton that represents no alignments whatsoever.
Taking $J$ to be false, $L$ to be $[*|\init']$, and $R$ to be $[\fin|*]$, we obtain an automaton that runs only $A$, unless it terminates, in which case it proceeds to run $A'$ —the sequential alignment.
To be precise, one must ensure that $L,R,J$ are live (per Def. <ref>).
Later we construct automata from programs, and for such automata every state has a successor except when control is final (Lemma <ref>).
Hence, for programs, an arbitrary triple $(L,R,J)$ can be made live very simply, as
where $\setminus$ is set subtraction.

Consider an alignment automaton $\aprod(A,A',L,R,J)$
and relation $\Q\subseteq Sto\times Sto'$.
The alignment automaton  is $\Q$-adequate provided for
all $(s,s')\in\Q$ and $t,t'$ with
$(\init,s)\trans^*(\fin,t)$ and $(\init',s')\trans'^*(\fin',t')$,
we have
$((\init,\init'),(s,s'))\biTrans^* ((\fin,\fin'),(t,t'))$.

An alignment automaton may be adequate for reasons that are specific to the
underlying automata, for example it may not cover all traces but still cover all outcomes.
It may even cover all traces of stores, while not covering all traces when control points are considered.
We focus on alignment automata that are adequate in the sense that they cover
all traces, which can be ensured as follows.

Given a relation $\Q\subseteq Sto\times Sto'$, an alignment automaton is
called manifestly $\Q$-adequate provided
that $L \lor R \lor J \lor [\fin|\fin']$ is $\Q$-invariant.
This means $L\lor R \lor J \lor [\fin|\fin']$ holds at every state that is reachable from some
$((\init,\init'),(s,s'))$ such that $(s,s')\in\Q$.

If alignment automaton $\aprod(A,A',L,R,J)$ is manifestly $\Q$-adequate
then it is $\Q$-adequate (in the sense of Def. <ref>).

§.§ Correctness of automata, and the inductive assertion method

Generalizing slightly from Sect. <ref>,
we consider specs $\spec{P}{Q}$ where $P$ and $Q$ are sets of automaton stores,
not necessarily variable stores.
Satisfaction of a spec by an automaton is written
$A \models \spec{P}{Q}$ and defined to mean:
For all $s,t$ such that $(\init,s)\trans^*(\fin,t)$,
if $s\in P$ then $t\in Q$.
Let $A$ and $A'$ be automata with store sets $Sto$ and $Sto'$ respectively.
Again generalizing slightly from Sect. <ref>,
we consider relational specs $\rspec{\R}{\S}$
where $\R$ and $\S$ are relations from $Sto$ to $Sto'$.
Satisfaction of the spec by the pair of automata $A,A'$ is written
$A,A'\models\rspec{\R}{\S}$ and defined
to mean:

For all $s,s',t,t'$
such that $(\init,s)\trans^*(\fin,t)$ and $(\init',s')\trans'^*(\fin',t')$,
if $(s,s')\in\R$ then $(t,t')\in\S$.

A store relation $\Q$ for $A,A'$ can be seen as a predicate on the stores
of an alignment automaton $\aprod(A,A',L,R,J)$ because the latter are pairs of stores.
Hence, for relational spec $\rspec{\Q}{\S}$,
the unary spec $\spec{\Q}{\S}$ makes sense
for $\aprod(A,A',L,R,J)$.

[adequacy sound and semantically complete]lemmapropadequatesound
Suppose that $\aprod(A,A',L,R,J)$ is $\Q$-adequate.
Then $\aprod(A,A',L,R,J)\models \spec{\Q}{\S}$
if and only if

Given automaton $A$ and spec $\spec{P}{Q}$,
an annotation is a function $an$ from control points to store predicates
such that $an(\init)=P$ and $an(\fin)=Q$.
The requirement $\init\neq\fin$ in Def. <ref> ensures that annotations exist for any spec.
In Floyd's formulation, an annotation only needs to be defined on a subset of control points that cut every loop in the control flow graph, but such an annotation can always be extended to one for all control points.

We lift $an$ to a function $\hat{an}$ that yields states:
$\graybox{$\hat{an}(n)$} = \{ (m,s) \mid s\in an(n), m\in Ctrl \}$.
For each pair $(n,m)$ of control points
there is a verification condition (VC):

\begin{equation}\label{eq:VC}
\POST(\tranSeg{n,m})(\hat{an}(n)) \subseteq \hat{an}(m)
\end{equation}

Here $\POST$ gives the direct image (i.e., strongest postcondition) of a relation,
and $\tranSeg{n,m}$ is the fixed-control transition relation restricted to starting control point $n$ and ending   $m$, i.e.,

\begin{equation}\label{eq:tranSeg}
\mbox{
$(i,s)\tranSeg{n,m}(j,t) \; $ iff $\; i=n$, $j=m$, and $(n,s)\trans(m,t)$
\end{equation}

It is well known that (<ref>) is equivalent to \( \hat{an}(n) \subseteq \PRE(\tranSeg{n,m})(\hat{an}(m)) \)
using the universal pre-image operator.
The VC (<ref>) says that for every transition from control point $n$ and store $s\in an(n)$,
if the step goes to control point $m$ with store $t$, then $t$ is in $an(m)$.
Annotation $an$ is valid if the VC is  true for every pair $(n,m)$ of control points.

[soundness and semantic completeness of IAM <cit.>]propositionpropIAM
There is a valid annotation of $A$ for $\spec{P}{Q}$ iff
$A\models \spec{P}{Q}$.

[soundness of alignment automata]corollarycorrelIAM

Suppose that $\aprod(A,A',L,R,J)$ is $\Q$-adequate and
$an$ is an annotation of $\aprod(A,A',L,R,J)$ for $\spec{\Q}{\S}$.
If $an$ is valid then $A,A'\models \rspec{\Q}{\S}$.

Together, Corollary <ref> and Lemma <ref> provide a method to verify
$A,A'\models \rspec{\Q}{\S}$:
Find alignment conditions $L,R,J$ and annotation $an$ of $\aprod(A,A',L,R,J)$
such that the annotation is valid and
$\breve{an}(i,j)\imp L \lor R \lor J \lor [\fin|\fin']$ for every $i,j$.
This uses the abbreviation
\( \graybox{$\breve{an}(n,n')$} \eqdef \hat{an}(n,n')\land [n|n'] \).
(Mnemonic: tipped c for control.)
This implication ensures manifest adequacy.

[semantic completeness of alignment automata]corollarycorrelIAMcomplete

Suppose $A,A'\models \rspec{\S}{\T}$.
Then there are $L,R,J$ and a valid annotation $an$ of $\aprod(A,A',L,R,J)$ for $\spec{\S}{\T}$
such that $\breve{an}(i,j)\imp L \lor R \lor J \lor [\fin|\fin']$ for every $i,j$.

§.§ Automata from programs and their VCs

nxs -nsxv

n;cs cs

ec  gcs
e(s) = 𝑡𝑟𝑢𝑒
ngcs s cs

(gcs)(s) = 𝑓𝑎𝑙𝑠𝑒
ngcs s -ns

nxes -nsxe(s)

ec  gcs
e(s) = 𝑡𝑟𝑢𝑒
ngcs s   c;ngcs s

cs dt
c;bs d;bt

Transition semantics (with $n$ and $v$ ranging over $\Z$).

Labels on commands serve as basis for defining the automaton for a program,
to which end we make the following definitions.
Write $\ok(c)$ to say no label in $c$ occurs more than once and all labels are positive.
We have $\ok(c0)$ for the running example $c0$ defined in Sect. <ref>.
Write $\lab(c)$ for the label of $c$ and $\labs(c)$ for its set of labels.
(Details in Sect. <ref>.)

For small-step semantics,
we write $\config{c}{s} \ctrans \config{d}{t}$ if command $c$ with store $s$ transitions to continuation command $d$ and store $t$.
The transition relation $\ctrans$ is defined in Fig. <ref>.
Negative labels are used in the small-step semantics
in a way that facilitates defining the automaton of a program.
In a configuration reached from an $\ok$ command,
the only negative labels are those introduced by the transition for assignment
and the transition for termination of a loop.

For every $c,s$, either $\config{c}{s}$ has a successor via $\ctrans$
or $c$ is $\lskipc{n}$ for some $n\in\Z$.  (This relies on $\totalIf$ of Def. <ref>.)
When a negative label is introduced, the configuration is either terminated
or has the form $\config{\lskipc{-n};c}{s}$
in which case the next transition is
$\config{\lskipc{-n};c}{s} \ctrans \config{c}{s}$.

For any $c,s,t$, we have
$\means{c}\, s\, t$
$\config{c}{s} \ctrans^* \config{\lskipc{n}}{t}$
for some $n$.

Write $\sub(n,c)$ for the sub-command of $c$ with label $n$, if $n$ is in $\labs(c)$.

Let $c$ and $\fin$ such that $\ok(c)$ and $\fin\notin\labs(c)$.
We write $\fsuc(n,c,\fin)$ for the following successor of $n$ in the control flow graph of $c$, in the sense made precise in Fig. <ref>.
Note that $\fin$ serves as a final or exit label.
The key case in the definition is for loops: the following successor is the control point after termination of the loop.
For the running example, we have $\fsuc(2,c0,6) = 6$ and $\fsuc(4,c0,6)=2$.
Define $\okf(c,f)$ (“ok, fresh”) to abbreviate the conjunction
of $\ok(c)$ and $f\notin\labs(c)$.

\[
\begin{array}{l@{\;}c@{\;}l}
%\fsuc(n,\lskipc{n},f)          & \eqdef & f \\
%\fsuc(n,\lassg{n}{x}{e},f)     & \eqdef & f \\
%\fsuc(n,\lhavc{n}{x},f)        & \eqdef & f \\
\fsuc(n,c;d,f)                 & \eqdef & \fsuc(n,c,\lab(d)) \mbox{ , if $n\in\labs(c)$} \\
& \eqdef & \fsuc(n,d,f) \mbox{ , otherwise} \\
\fsuc(n,\lifgc{n}{gcs}, f) &\eqdef & f \\
\fsuc(m,\lifgc{n}{gcs}, f) &\eqdef & \fsuc(m,c,f) \mbox{ , if $e\gcto c \in gcs$ and $m\in\labs(c)$} \\
\fsuc(n,\ldogc{n}{gcs}, f) &\eqdef & f \\
\fsuc(m,\ldogc{n}{gcs}, f) &\eqdef & \fsuc(m,c,n) \mbox{ , if $e\gcto c \in gcs$ and $m\in\labs(c)$}
\\
\multicolumn{3}{l}{
\fsuc(n,\lskipc{n},f)           \;\eqdef\;
\fsuc(n,\lassg{n}{x}{e},f)      \;\eqdef\;
\fsuc(n,\lhavc{n}{x},f)         \;\eqdef\; f } \\
\end{array}
\]

Following successor $\fsuc(n,c,f)$,
assuming $\ok(c)$, $n\in\labs(c)$, and $f\notin\labs(c)$.

Suppose $\okf(c,f)$.
The automaton of $c$ for $f$, written $\aut(c, f)$, is

\( (\labs(c)\union \{ f \}, (\Var\to\Z), \lab(c), f, \trans) \)
$(n,s)\trans (m,t)$ iff either

* $
\some{d}{ \config{\sub(n,c)}{s}\ctrans\config{d}{t}
\land \lab(d) > 0 \land m = \lab(d) }$, or

$\some{d}{ \config{\sub(n,c)}{s}\ctrans\config{d}{t} \land \lab(d) < 0 \land m = \fsuc(n,c,f) }$, or

* $\sub(n,c)=\lskipc{n} \land m = \fsuc(n,c,f) \land t = s$

The first two cases use the semantics of Fig. <ref>
for a sub-command on its own.
The second case uses $\fsuc$ for a sub-command that takes a terminating step
(either an assignment or a loop).
The third case handles skip, which on its own would be stuck
but which should take a step when it occurs as part of a sequence.

The only stuck states of $\aut(c, f)$ are terminated ones, i.e.,  where the control is $f$.

[automaton consistency]lemmalemautConsistent
Suppose $\okf(c,f)$ and  let $n=\lab(c)$.
For any $s,t$ we have
$\means{c}\, s\, t $ iff $(n,s)\trans^*(f,t)$ in $\aut(c,f)$.
$\models c:\spec{P}{Q}$ iff $\aut(c,f)\models\spec{P}{Q}$
for any $P,Q$.
Also $ \models c\sep c':\rspec{\Q}{\S}$ iff $\aut(c,f),\aut(c',f')\models\rspec{\Q}{\S}$
for any $\Q,\S$ and

Verification conditions

if $\sub(n,c)$ is…    and $m$ is …    then the VC for $(n,m)$ is equivalent to…

$\fsuc(n,c,f)$     $an(n)\imp an(m)$

$\fsuc(n,c,f)$     $an(n)\imp \subst{an(m)}{x}{e}$

$\fsuc(n,c,f)$     $an(n)\imp \allSet{x}{an(m)}$

$\lifgc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$an(n)\land e \imp an(m)$

$\ldogc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$an(n)\land e \imp an(m)$

$\ldogc{n}{gcs}$     $\fsuc(n,c,f)$     $an(n)\land \neg \enab(gcs) \imp an(m)$

In all other cases, there are no transitions from $n$ to $m$ so the VC is $true$ by definition.

VCs for the automaton $aut(c,f)$ of $\ok$ program $c$ and annotation $an$.

By inspection of the transition semantics in Fig. <ref>,
there are six kinds of transitions
for $\ctrans$ and also for the automaton relation $\trans$ derived from it.
(There is a seventh rule for $\ctrans$ that says a transition can occur for the first command in a sequence, but that is used together with one of the other six,
and it is not relevant to Def. <ref>.)
Thus there are six kinds of verification conditions, which can be derived from
the semantic definitions.

[VCs for programs]lemmalemVCprog
Consider $c$ and $f$ such that $\ok(c,f)$, and
let $an$ be an annotation of $\aut(c,f)$.
For each pair $n,m$ of labels, the VC of Eqn. (<ref>)
can be expressed as in Fig. <ref>.

§.§ Relational VCs

if $\sub(n,c)$ is …
and $m$ is…
then the VC for $((n,n'),(m,n'))$ is equivalent to $\ldots$

$\lskipc{n}$     $\fsuc(n,c,f)$     $L \land \breve{an}(n,n')\imp \hat{an}(m,n')$

$\lassg{n}{x}{e}$     $\fsuc(n,c,f)$     $L\land \breve{an}(n,n')\imp \subst{\hat{an}(m,n')}{x\smSep}{e\smSep}$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $L\land \breve{an}(n,n')\imp \allSet{x\smSep}{\hat{an}(m,n')}$

$\lifgc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$L\land \breve{an}(n,n')\land \leftF{e} \imp \hat{an}(m,n')$

$\ldogc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$L\land \breve{an}(n,n')\land \leftF{e} \imp \hat{an}(m,n')$

$\ldogc{n}{     gcs}$     $\fsuc(n,c,f)$
$L\land \breve{an}(n,n')\land \neg\leftF{\enab(gcs)} \imp \hat{an}(m,n')$

In all other cases, there are no transitions from $(n,n')$ to $(m,n')$ so the VC is $true$ by definition.

The left-only VCs for annotation $an$ of $\aprod(\aut(c,f),\aut(c',f'),L,R,J)$.

if $\begin{array}[t]{l}
\sub(n,c) \\
\sub(n',c')
\end{array}$
and $\begin{array}[t]{l} m \\ m' \end{array}$ are…
then the VC for $((n,n'),(m,m'))$ is equivalent to $\ldots$

$\fsuc(n,c,f)$     $J \land \breve{an}(n,n')\imp \hat{an}(m,m')$

$\fsuc(n,c,f)$     $J \land \breve{an}(n,n')\imp \subst{\hat{an}(m,m')}{x|x'}{e|e'}$

$\lifgc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$J \land \breve{an}(n,n')\land \leftF{e} \land \rightF{e'} \imp \hat{an}(m,m')$

$\lifgc{n'}{gcs'}$     $\lab(d')$ where $e'\gcto d'$ is in $gcs'$

$\ldogc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$J \land \breve{an}(n,n')\land \leftF{e} \land \neg\rightF{\enab(gcs')} \imp \hat{an}(m,m')$

$\ldogc{n'}{gcs'}$     $\fsuc(n',c',f')$

$\lassg{n}{x}{e}$     $\fsuc(n,c,f)$
$J \land \breve{an}(n,n')\land \rightF{e'} \imp \subst{\hat{an}(m,m')}{x|}{e|}$

$\lifgc{n'}{gcs'}$     $\lab(d')$ where $e'\gcto d'$ is in $gcs'$

3lOmitted: the other 31 cases with nontrivial VCs.

Selected joint VCs for $\aprod(\aut(c,f),\aut(c',f'),L,R,J)$ and annotation $an$.

Consider an alignment automaton $\aprod(A,A',L,R,J)$ where the underlying automata $A$ and $A'$ are obtained from programs by Def. <ref>.
An annotation of $\aprod(A,A',L,R,J)$ thus maps pairs of control points of $A,A'$ to
relations on variable stores.
Verification conditions are associated with tuples $((n,n'),(m,m'))$,
for which take $n:=(n,n')$ and $m:=(m,m')$ in Eqn. (<ref>).

For a given pair $((n,n'),(m,m'))$ of alignment automaton control points,
the transitions go only via LO, or only via RO, or only via JO in Def. <ref>.
If $n=m$, i.e., control does not change on the left, the transitions must be via RO
because the non-stuttering condition for automata (Def. <ref>)
ensures there is no unary transition where control does not change.
Similarly, if $n'=m'$ the transitions are via LO.
If $n\neq m $ and $n'\neq m'$ the transitions only go via JO.

Fig. <ref> gives the six VCs for transitions that go by the LO condition.
The VCs for RO are symmetric (and omitted).
There are 36 combinations for JO transitions of an alignment automaton; some of their VCs are in Fig. <ref> (and more in Fig. <ref>).
Note that, by contrast with Fig. <ref>
and Lemma <ref> we do not eliminate lift (hat) notation
in Figs. <ref> and <ref>,
because the alignment conditions $L$, $R$, $J$ are sets of states not sets of stores.
We return to this later, using the $pc$  variable to encode the control part of the state.
In Figs. <ref> and <ref>, the substitution notation is lifted from store relations to state relations and likewise for $\leftF{e}$ and $\rightF{e}$.

[VCs for program alignment automata]lemmalemVCalign
Consider programs $c$ and $c'$, with alignment automaton
Let $an$ be an annotation.
For each pair $(n,n'),(m,m')$ of alignment automaton control points, the VC
can be expressed
as in Fig. <ref>, Fig. <ref>, and in the omitted RO cases that are symmetric to Fig. <ref>.

§.§ Encoding relational VCs in terms of store relations

For use in RHL+ proofs about programs in automaton normal form,
we will encode the VCs in terms of relations on stores that use
a variable $pc$ (for “program counter”) to encode control information.
We often use the following abbreviations for assignments and tests of
the chosen $pc$ variable.

\begin{equation}\label{eq:pcabbrev}
\mbox{
\graybox{$\spc n$} for $pc:=n$
\qquad
\graybox{$\tpc n$} for $pc=n$
\qquad  for literal $n\in\nat$
\end{equation}

To be precise, we define $\spc n$ to be $\lassg{0}{pc}{n}$, using $0$ arbitrarily as the label. Our uses of $\spc n$ will be in contexts where labels are irrelevant
in commands that are not required to be $\ok$.
Note that the notations $\spc n$ and $\tpc n$ depend, implicitly, on the choice of the variable $pc$.

Let $R$ be a set of states of a program alignment automaton.
Let $pc$ be a variable such that $\indep(pc|pc,R)$.
Define the $pc$-encoded $R$ to be a relation on stores as follows:
\( \graybox{$\encode{R}$} \eqdef \{ (s,s') \mid  ((s(pc),s'(pc)),(s,s'))\in R  \} \).

Let $R$ be set of alignment automaton states such that $\indep(pc|pc,R)$.
If $(s,s') \in \encode{R}\land\bothF{\tpc n\sep\tpc n'} $
then $((n,n'),(s,s')) \in R$.

if $\sub(n,c)$ is …
and $m$ is…
then the encoded VC for $((n,n'),(m,n'))$ is $\ldots$

$\lskipc{n}$     $\fsuc(n,c,f)$     $\encode{L}\land\bothF{\tpc n\sep\tpc n'} \land an(n,n')\imp an(m,n')$

$\lassg{n}{x}{e}$     $\fsuc(n,c,f)$     $\encode{L}\land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\imp \subst{an(m,n')}{x\smSep}{e\smSep}$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $\encode{L}\land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\imp \allSet{x\smSep }{an(m,n')}$

$\lifgc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$\encode{L}\land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\land \leftF{e} \imp an(m,n')$

$\ldogc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$\encode{L}\land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\land \leftF{e} \imp an(m,n')$

$\ldogc{n}{     gcs}$     $\fsuc(n,c,f)$
$\encode{L}\land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\land \neg\leftF{\enab(gcs)} \imp an(m,n')$

The left-only $pc$-encoded VCs for annotation $an$ of  $\aprod(\aut(c,f),\aut(c',f'),L,R,J)$.

if $\begin{array}[t]{l}
\sub(n,c) \\
\sub(n',c')
\end{array}$
and $\begin{array}[t]{l} m \\ m' \end{array}$ are…
then the encoded VC for $((n,n'),(m,m'))$ is $\ldots$

$\fsuc(n,c,f)$     $\encode{J}\land\bothF{\tpc n\sep\tpc n'} \land an(n,n')\imp an(m,m')$

$\fsuc(n,c,f)$     $\encode{J}\land\bothF{\tpc n\sep\tpc n'} \land an(n,n')\imp \subst{an(m,m')}{x|x'}{e|e'}$

$\lifgc{n}{gcs}$     $\lab(d)$ where $e\gcto d$ is in $gcs$
$\encode{J} \land\bothF{\tpc n\sep\tpc n'}\land an(n,n')\land \leftF{e} \land \rightF{e'} \imp an(m,m')$

$\lifgc{n'}{gcs'}$     $\lab(d')$ where $e'\gcto d'$ is in $gcs'$

Selected $pc$-encoded joint VCs for annotation $an$ of $\aprod(\aut(c,f),\aut(c',f'),L,R,J)$.

Let $an$ be an annotation of an alignment automaton
$\aprod(\aut(c,f),\aut(c',f'),L,R,J)$ for commands $c,c'$.
Suppose $pc$ is a fresh variable in the sense that
it does not occur in $c$ or $c'$, and all of $L,R,J$ and any $an(i,j)$ are independent from
$pc$ on both sides.
Then each left-only relational VC of Fig. <ref> implies
the corresponding condition on store relations in Fig. <ref>.
Each joint relational VC in
Fig. <ref> implies the corresponding condition in Fig. <ref>.
Similarly for right-only VCs.

The conditions in Fig. <ref> are obtained using
the $pc$-encoded
$\encode{L}\land\bothF{\tpc n\sep\tpc n'}$ in place of $L\land[n|n']$, and $an$ in place of $\hat{an}$.
The conditions in Fig. <ref> are obtained using
$\encode{J}\land\bothF{\tpc n\sep\tpc n'}$ in place of $J\land[n|n']$.

§ AUTOMATON NORMAL FORM REDUCTION AND KAT

Sect. <ref> defines the representation of commands by expressions in KAT
and defines command equivalence in terms of KAT equality under certain hypotheses.
Sect. <ref> defines the automaton normal form and the reduction of
a command to its normal form.
Sect. <ref> proves that any command, once instrumented with assignments
to a fresh $pc$ variable, is equivalent to its normal form.

Design alternatives for the formalization of command equivalence
appear in the Sect. <ref>.

§.§ Embedding programs in a KAT

A Kleene algebra with tests <cit.> (KAT) is a structure $(\kK,\kB,\kplus,\kdot,\kstar,\kneg,\kone,\kzero)$
such that
(a) $\kK$ is a set and $\kB\subseteq \kK$ (elements of $\kB$ are called tests).
(b) $\kB$ contains $\kone$ and $\kzero$, and is closed under the operations $\kplus,\kdot,\kneg$,
and these satisfy the laws of Boolean algebra, with $\kone$ as true
and $\kdot$ as conjunction.
(c) $\kK$ is an idempotent semiring and the
following hold for all $x,y,z$ in $\kK$.

\[\begin{array}{lcl@{\hspace{5em}}lcl}
\kone \kplus x\kdot x^\kstar &=& x^\kstar
& y \kplus x\kdot z \leq z &\imp& x^\kstar\kdot y \leq z \\
\kone \kplus x^\kstar\kdot x &=& x^\kstar
& y \kplus z\kdot x \leq z &\imp& y\kdot x^\kstar \leq z
\end{array}
\]

The ordering $\leq$ is defined by $x\leq y$ iff $x+y=y$.
The operator $;$ binds tighter than $+$.

In a relational model <cit.>, $\kK$ is some set of relations on some set $\Sigma$,
with $\kzero$ the empty relation,
$\kone$ the identity relation on $\Sigma$,
$+$ union of relations,
$\kdot$ relational composition, and $*$ reflexive-transitive closure.
Moreover  $\kB$ is a set of coreflexives, i.e., subsets of the identity relation $\kone$,
and $\kneg$ is complement with respect to $\kone$.
The set $\kK$ needs to be closed under these operations but need not be the full set of relations on $\Sigma$; likewise, $\kB$ need not be all coreflexive relations.
In a relational model, $\leq$ is set inclusion.
The relational model for GCL, denoted $\relKAT$, is the relational model comprising all relations on $\Sigma$ where $\Sigma$ is the set of variable stores.

In this paper we work with $\relKAT$ and also with equational proofs with equational hypotheses.  The latter are formalized in terms of KAT expressions.
KAT expressions are usually defined with respect to given finite sets of primitive tests and actions <cit.>.
We only need the special case where the actions are primitive commands and the tests are primitive boolean expressions.
Define the KAT expressions by this grammar.
(Recall that $bprim$ stands for primitive boolean expressions in GCL.)

\begin{equation}\label{eq:KATexp}
\KE ::= \underline{bprim} \mid \underline{\lassg{}{x}{e}} \mid
\underline{\havc{x}} \mid
\KE + \KE \mid \KE\mathbin{;}\KE \mid \KE^* \mid \neg \KE \mid 1 \mid 0
\end{equation}

The primitive forms $\underline{bprim}$, $\underline{\lassg{}{x}{e}}$,
and $\underline{\havc{x}}$  are written this way to avoid confusion with their counterparts in GCL syntax.
The GCL-to-KAT translation $\mkt{-}$
maps GCL commands and boolean expressions to KAT expressions.
For boolean expressions it is defined by:

\[
\mkt{bprim} \eqdef \underline{bprim}
\qquad \mkt{\neg e} \eqdef  \kneg\mkt{e}
\qquad \mkt{e\land e'} \eqdef  \mkt{e}\kdot\mkt{e'}
\qquad\mkt{e\lor e'} \eqdef  \mkt{e}\kplus\mkt{e'}
\]

For commands the translation is defined by mutual recursion with the definition of $\mkt{gcs}$:[Using Dijkstra's notation
$\quant{+}{dummies}{range}{term}$ <cit.>
rather than the more common $\Sigma$ notation for finite sums.]

\begin{equation}\label{eq:def:mkt}
\begin{array}{l@{\;}c@{\;}l@{\hspace*{3em}}l@{\;}c@{\;}l}
%\mkt{\lassg{}{x}{e}} &  & \mbox{is given} \\
\mkt{\lassg{}{x}{e}} & \eqdef  & \underline{x:=e}
& \mkt{c;d} & \eqdef  & \mkt{c}\kdot\mkt{d} \\
\mkt{\havc{x}} &\eqdef& \underline{\havc{x}}
& \mkt{\lifgc{}{gcs}} & \eqdef  & \mkt{gcs} \\
\mkt{\skipc} & \eqdef  & 1
& \mkt{\ldogc{}{gcs}} & \eqdef  & \mkt{gcs}^\kstar \kdot \kneg\mkt{\enab(gcs)}  \\[1ex]
\mkt{gcs} & \eqdef  & \multicolumn{4}{l}{\quant{\kplus}{e,c}{(e\gcto c) \in gcs}{\mkt{e}\kdot\mkt{c}} }
\end{array}
\end{equation}

This is an adaptation of the well known translation of imperative programs into a KAT <cit.>.

Let $\anyKAT$ be a model $(\kK^\anyKAT,\kB^\anyKAT,\kplus^\anyKAT,\kdot^\anyKAT,\kstar^\anyKAT,\kneg^\anyKAT,\kone^\anyKAT,\kzero^\anyKAT)$.
Given interpretations $\underline{bprim}^\anyKAT$, $\underline{x:=e}^\anyKAT$,
and $\underline{\havc{x}}^\anyKAT$
in $\anyKAT$ for each primitive KAT expression,
we get an interpretation $\KE^\anyKAT$ for every $\KE$,
defined homomorphically as usual;
for example:

$(\KE_0+\KE_1)^\anyKAT \eqdef \KE_0^\anyKAT \,+^\anyKAT\,\KE_1^\anyKAT$.
Henceforth we never write $+^\anyKAT$ because the reader can infer whether the symbol
$+$ is meant as syntax in a KAT expression or as an operation of a particular KAT.

We define interpretations in $\relKAT$ for the primitive expressions, as follows:
$\underline{bprim}^\relKAT \eqdef \{(s,s) \mid \means{bprim}(s) = true \}$,
$\underline{\lassg{}{x}{e}}^\relKAT  \eqdef  \means{\lassg{}{x}{e}}$, and
$\underline{\havc{x}}^\relKAT  \eqdef  \means{\havc{x}}$.
As a consequence, we have

\[ %begin{equation}\label{eq:def:priminterp}
\mkt{bprim}^\relKAT = \{(s,s) \mid \means{bprim}(s) = true \}
\qquad
\mkt{\lassg{}{x}{e}}^\relKAT  = \means{\lassg{}{x}{e}}
\qquad
\mkt{\havc{}{x}}^\relKAT  = \means{\havc{x}}
\]

For all commands $c$ we have $\mkt{c}^\relKAT = \means{c}$.
For all boolean expressions $e$ we have
$\mkt{e}^\relKAT = \{(s,s) \mid \means{e}(s) = true \}$.

Let $H$ be a set of equations between KAT expressions.
We write $H \proves \KE_0 = \KE_1$ to say $\KE_0=\KE_1$
is provable by propositional and equational reasoning from $H$ plus
the axioms of KAT (Def. <ref>).
Propositional reasoning is needed for the $*$-induction rules,
i.e., the two implications in Def. <ref>.
The important fact is that for any model $\anyKAT$ of $KAT$,
if $H \proves \KE_0 = \KE_1$ and the equations in $H$ hold when interpreted in $\anyKAT$,
then $\KE_0^\anyKAT = \KE_1^\anyKAT$.

Compared with the program notation, KAT expressions serve to put expressions, commands, and guarded commands on the same footing. This is convenient for formulating results such as the following, which uses the empty set of hypotheses.

For any $gcs$ we have
$\proves \mkt{gcs} = \mkt{\enab(gcs)} \kdot \mkt{gcs}$.

For specifications where the pre- and post-condition are expressible as tests in the KAT,
one can express correctness judgments;
one form is $pre;code\leq pre;code;post$.
This is equivalent to
$pre;code;\neg post = 0$.

On this basis one can dispense with HL in favor of equational reasoning in KAT <cit.>.
In our setting, for expressions $e_0$ and $e_1$ we have that
$ \models c:\spec{e_0}{e_1}$
is equivalent to the equation
\( \mkt{e_0}\kdot\mkt{c}\kdot\kneg\mkt{e_1} = 0 \)
being true in $\relKAT$.

In this paper we do not use the KAT formulation for correctness judgments in general,
but we do use it in a limited way.

The idea for the equivalence condition $c\kateq d$ in rules Rewrite (Fig. <ref>) and rRewrite (Fig. <ref>)
is that it should mean $H\proves \mkt{c}=\mkt{d}$ for a suitable set of hypotheses
that axiomatize the semantics of some primitive boolean expressions and commands.
To prove our main results we only need a few axioms (as detailed in Sect. <ref>).
For example, all we need about havoc is that
$\mkt{e};\mkt{\havc{x}};\kneg\mkt{e}=0$ for every $e$ with $x\notin e$.
But for the sake of a straightforward presentation we
formulate equivalence in terms of a larger set of axioms.

Define $\Hyp$ to be the set of equations
given by:
(a) the equation $\mkt{e}=0$ for every boolean expression $e$
such that $e \imp\mathit{false}$ is valid;
(b) the equation $\mkt{e_0};\mkt{x:=e};\kneg\mkt{e_1}=\kzero$
for all assignments $x:=e$
and boolean expressions $e_0$, $e_1$
such that $e_0\imp \subst{e_1}{x}{e}$ is valid;
(c) the equation
for $x,e_0,e_1$ such that $e_0\imp \allSet{x}{e_1}$ is valid.

Every equation in $\Hyp$ holds in $\relKAT$.

Define $\kateq$ by
\( \graybox{$c \kateq d$} \eqdef \Hyp \proves \mkt{c} = \mkt{d} \).

As an example, we have $\lskipc{};\lskipc{} \kateq \lskipc{}$.
Another example is the equivalence

\[ \ldogc{}{ e_0 \gcto c } \quad\kateq\quad
\ldogc{}{ e_0 \gcto c;\ldogc{}{e_0\land e_1\gcto c}} \]

(which holds for any $c,e_0,e_1$) used in the loop tiling example of <cit.>.

For any given $c$ and $d$, only finitely many primitive KAT expressions
occur in $\mkt{c}$ and $\mkt{d}$, and
$\Hyp \proves \mkt{c} = \mkt{d}$ just if
$H \proves \mkt{c} = \mkt{d}$ for the relevant finite subset $H$ of $\Hyp$.
Because the hypotheses are all equations of the form $\KE=0$,
we get that $c\kateq d$ is decidable in PSPACE <cit.>.
So the premises of the rewrite rules are decidable.
(Alternatively, one can give deductive rules for $\kateq$.)

Having defined $\kateq$,
the key ingredient of the rules Rewrite and rRewrite,
we have completed the definition of HL+ and RHL+.

All the rules of HL+ are sound.

All the rules of RHL+ (Fig. <ref>) are sound.

The proofs are straightforward using the definitions, and induction for the loop rule
(similar loop rules are proved sound in <cit.>).
We omit them, except the following.

For rRewrite, consider first the soundness of unary Rewrite.  Suppose $c \kateq d$ holds.
That means $\Hyp\proves\mkt{c}=\mkt{d}$ so
$\mkt{c}^\anyKAT = \mkt{d}^\anyKAT$ in any model $\anyKAT$ that satisfies
the equations $\Hyp$.
By Lemma <ref> we have
hence $\means{c}=\means{d}$ by Lemma <ref>.
Suppose the premise of Rewrite holds,
i.e., $\models c: \spec{P}{Q}$.
This is a condition on $\means{c}$

so we have $\models d: \spec{P}{Q}$.
The proof of rRewrite is similar.

§.§ Automaton normal form

Choose a variable name $pc$.
Fig. <ref> defines $\addPC$, a function from commands to commands,
that adds $pc$ as in the example $c0^+$.
The definition of $\addPC$ is by structural recursion, with mutually recursive
helpers $\addPC_0$ and $\addPC_1$, and is written using the
abbreviations in (<ref>).
For if commands, $\addPC_0$ maps $\addPC$ over the guarded commands,
and for do, $\addPC_1$ additionally adds a trailing assignment to set $pc$ to
the loop label.

\(\begin{array}{lcl}
\addPC(\lskipc{n}) &\eqdef& \spc  n \,; \lskipc{n} \\
\addPC(\lassg{n}{x}{e}) &\eqdef& \spc  n \,; \lassg{n}{x}{e} \\
\addPC(\lhavc{n}{x}) &\eqdef& \spc  n \,; \lhavc{n}{x} \\
\addPC(c;d) &\eqdef& \addPC(c) \,; \addPC(d) \\
\addPC(\lifgc{n}{gcs}) &\eqdef& \spc n \,; \lifgc{n}{(\addPC_0(gcs))} \\
\addPC(\ldogc{n}{gcs}) &\eqdef& \spc n \,; \ldogc{n}{(\addPC_1(n,gcs))} \\[1ex]
\addPC_0(e\gcto c) &\eqdef& e\gcto \addPC(c) \\[.5ex]
\addPC_0(e\gcto c \gcsep gcs) &\eqdef& e\gcto \addPC(c) \gcsep \addPC_0(gcs)\\[1ex]
\addPC_1(n,e\gcto c) &\eqdef& e\gcto \addPC(c);\spc n \\[.5ex]
\addPC_1(n,e\gcto c \gcsep gcs) &\eqdef& e\gcto \addPC(c);\spc n \gcsep \addPC_1(n,gcs)
\end{array}\)

Definition of $\addPC$

For any $c$, if $pc$ does not occur in $c$,
then we have $\ghost(pc,\addPC(c))$.
Moreover $ \erase(pc,\addPC(c)) \kateq c$.

Fig. <ref> defines the ternary relation $\norm{c}{m}{gcs}$
to relate a command and a label to the gcs that will be the body of its normal form
(see example $d0$).
To be precise, the relation depends on a choice of $pc$ variable but we leave this implicit,
as it is in the $\tpc \_$ and $\spc \_$ notations of (<ref>).

The guarded commands in normal form bodies have these forms:
$\tpc n\land e \gcto \spc m$
(which abbreviates $pc = n \land e \gcto \lassg{}{pc}{m}$),
$\tpc n\gcto \lassg{}{x}{e};\spc m$,
and $\tpc n \gcto \havc{x};\spc m$.
An example is $\norm{\lassg{4}{x}{x-1}}{2}{(\tpc 4\gcto x:=x-1;\spc 2)}$.

For readability, Fig. <ref> gives special cases for if and do.

The automaton normal form of a command $c$ with $\lab(c)=n$ and label $f\notin\labs(c)$, for chosen variable $pc$, is
the command
\(\: \spc  n ; \ldogc{}{ gcs } \: \)
where $\normSmall{c}{f}{gcs}$.

(n xe; f)

nxf(n x;f)

ne_0c_0 e_1c_1f
n e_0 (c_0)  n e_1 (c_1)  gcs_0 gcs_1

ne (c)  ne f gcs

ne_0c_0 e_1c_1f
ne_0 (c_0)  ne_1 (c_1)  n(e_0 e_1) f gcs_0 gcs_1

Normal form bodies
(see Fig. <ref> for the if/do general cases).

For all $c$ and $f$, there is some $gcs$ with $\normSmall{c}{f}{gcs}$.

This does not require $c$ to be $\ok$, but the normal form is only useful if $\okf(c,f)$.
Note that that $gcs$ is uniquely determined by $c$ and $f$. We could formulate the
definition as a recursive function, but the relational formulation is convenient for proofs
and we do not exploit uniqueness.

§.§ Normal form equivalence theorem

Finally we are ready for the main result of Sect. <ref>,
which loosely speaking says every command is equivalent to one in automaton normal form.

If $\okf(c,f)$, $pc\notin vars(c)$, and
$\normSmall{c}{f}{gcs}$ (for $pc$)

\begin{equation}\label{eq:normEquiv}
\spc n; \ldogc{}{gcs} \kateq \addPC(c); \spc f   % NOTE: reverse of Coq development, but fits with Rewrite
\quad\mbox{where $n=\lab(c)$.}
\end{equation}

The proof (in appendix) goes by rule induction on $\normSmall{c}{f}{gcs}$.
The core of the argument in each case
is a calculation in KAT, using the normal form  axioms (and induction hypotheses).

§.§ Floyd completeness

In this section we put the normal form equivalence theorem to work
in a proof that any IAM proof can be translated to one in HL+.
This gives a way to prove completeness of HL+ in the sense of Cook,
as spelled out in the Corollary <ref>.
It also provides a pattern that guides the proof of alignment completeness, Theorem <ref>.

[Floyd completeness]theoremthmFloydComplete
Suppose $\okf(c,f)$.
Suppose $an$ is a valid annotation of $\aut(c,f)$ for $\spec{P}{Q}$.
Then $c: \spec{P}{Q}$ can be proved in HL+, using only assertions derived from $an$.

As sketched by example Sect. <ref>,
the proof uses only a single instance of the Do rule and no instance of the If rule.
More importantly, the judgments use only assertions derived from those of $an$ in simple ways.
In particular, we use boolean combinations of the following:
assertions $an(i)$, boolean expressions that occur in $c$,
and equality tests $pc=n$ of the program counter variable and numeric literals;
and we use substitution instances $\subst{an(i)}{x}{e}$ for assignments
$x:=e$ that occur in $c$.

Nagasamudram and Naumann introduce the term Floyd completeness
and use it for a similar result <cit.>
where they refer to “associated judgments” which are not precisely defined but rather highlighted in the theorem's proof.
We follow suit here, but note that our proofs are very different.
The practical importance of both their and our Floyd completeness results is that the deductive proof does not require more expressive assertions than used in the IAM proof.

§ RHL+ IS ALIGNMENT COMPLETE

Finally we can state the main result for $\forall\forall$ properties:
any IAM-style proof for program alignment automata gives rise to an RHL+ proof.

(a) $\okf(c,f)$ and $\okf(c',f')$

(b) $an$ is a valid annotation of $\aprod(\aut(c,f),\aut(c',f'),L,R,J)$
for $\spec{\S}{\T}$

(c) $\breve{an}(i,j)\imp L \lor R \lor J \lor [\fin|\fin']$ for all control points $(i,j)$ of

Then the judgment $c\sep c': \rspec{\S}{\T}$ has a proof in RHL+.

Conditions (b) and (c) in Theorem <ref> say there is an
IAM-style proof.
By Corollary <ref> we have that $\aut(c,f),\aut(c',f') \models \rspec{\S}{\T}$
and so by Lemma <ref> we get $\models c\sep c' : \rspec{\S}{\T}$.
Theorem <ref> says there is also a deductive proof
of $c\sep c': \rspec{\S}{\T}$.

This deductive proof uses only relational assertions derived in simple ways from assertions $an(i,j)$, specifically: boolean combinations
of the annotation's assertions, conjunctions with conditional tests in the code, and substitutions for expressions in assignment commands.

Restriction (a) in Theorem <ref> is just a technicality.
The $\okf$ condition just says labels of $c$ are unique and do not include $f$.
Labels have no effect on program semantics so they can always be chosen to satisfy the condition.

The proof follows the lines of the Floyd completeness proof sketched in Sect. <ref>.
A variable $pc$ is chosen that is fresh with respect to the specs, code, annotation,
and given alignment conditions $L,R,J$.
By Lemma <ref>
and  Theorem <ref>
there are normal form bodies $gcs$ and $gcs'$ such that
$\spc n; \ldogc{}{gcs} \: \kateq \: \addPC(c); \spc f $
$\spc n'; \ldogc{}{gcs'} \: \kateq \: \addPC(c'); \spc f'$.
Rule rDo is used to relate the normal forms using
alignment conditions $\Lrel:=\encode{L}$ and $\R:=\encode{R}$ with
loop invariant $\Q$ defined as the conjunction of
$\quant{\land}{i,j}{}{\bothF{\tpc i\sep \tpc j} \imp an(i,j)} $
$\quant{\lor}{i,j}{}{\bothF{\tpc i\sep \tpc j}}$
where $i,j$ range over labels of $c,c'$ respectively.
The side condition of rDo follows from hypothesis (c) using (b).
The premises of this instance of the rule can all be derived using the assignment and sequence rules,
judiciously using rConseq to exploit the left-only, right-only, and joint VCs.

For the left-only and right-only premises there is an additional complication.
The joint cases determine a starting pair and ending pair of control points,
which determines which VC to appeal to (Fig. <ref>).
The left-only premises do not determine a control point on the right side; instead
we have VCs for each possible point on the right (Fig. <ref>).
So we use the disjunction rule rDisj (or rather a derived N-ary disjunction rule)
to combine subproofs for each  possible control point on the right.

Having used rDo to prove that
$\spc n; \ldogc{}{gcs} \Sep \spc n'; \ldogc{}{gcs'} $
satisfies the spec, we wrap up using rRewrite and ghost elimination.

Cook completeness without relying on sequential product

As detailed in Sect. <ref> we get Cook completeness
for the following reasons.
Suppose $\models c\sep c': \rspec{\S}{\T}$.
By Lemma <ref> the two program automata
satisfy the spec.  So
by Corollary <ref>
there is an alignment automaton with valid annotation that satisfies conditions (b) and (c)
of Theorem <ref>.
Applying the theorem, we get a proof of $c\sep c': \rspec{\S}{\T}$ in RHL+.

§ THE $\FORALL\EXISTS$ LOGIC ERHL+ AND ITS ALIGNMENT COMPLETENESS

We write $\forall\exists$ specs as $\aespec{\R}{\S}$ and
define the valid judgments by
$\models c\sep c': \aespec{\R}{\S}$ $\eqdef$

\begin{equation}\label{eq:aespec}
\mbox{For all $s,s',t$ such that $(s,s')\in \R$ and $\means{c}\, s\, t$,
there is $t'$ such that $\means{c'}\, s'\, t'$ and $(t,t')\in \S$.}
\end{equation}

If $d$ is deterministic then
$c\sep d : \aespec{\P}{\Q}$ implies $c\sep d : \rspec{\P}{\Q}$.
If $d$ denotes a domain-total relation
then $c\sep d : \rspec{\P}{\Q}$ implies $c\sep d : \aespec{\P}{\Q}$.
This suggests that one could consider a deductive system involving both kinds of judgments,
and it hints why some proof rules for $\aespecSym$ are the same as those on Fig. <ref>.
Another possibility is for a $\forall\exists$ logic to include unary judgments, both over- and under-approximating
as in RHLE <cit.>.
In this paper, however, we consider a standalone deductive system for the $\aespecSym$ judgment, called ERHL+, which
involves only the $\aespecSym$ judgment together with assertion validity and command equivalence $\kateq$ just like RHL+.
Unary correctness is subsumed by ERHL+ because
$c:\spec{P}{Q}$ is valid iff
$c\sep\skipc: \aespec{\leftF{P}}{\leftF{Q}}$ is valid.
Forward underapproximation judgments (as in RHLE) are subsumed
by the form
$\skipc\sep c: \aespec{\rightF{P}}{\rightF{Q}}$.
(As an aside, O'Hearn's incorrectness —backwards underapproximation— judgment
is similarly obtained by a backwards version of (<ref>),
as noted in <cit.>.)

x: (x)

c: e

c' : e'V=k V≺k

cc' : ee'

((gcs) = (gcs')

gcs gcs' : (gcs)(gcs')

Rules eRewrite, eGhost, eSkip, eSkipAss, eAssSkip, eSeq, eIf, eConseq, eDisj, and eFalse are the same as those with corresponding names in Fig. <ref> but for $\aespecSym$.

Rules of ERHL+

The rules of ERHL+ appear in Fig. <ref>.  Most have the same form as corresponding rules in Fig. <ref>,
although the soundness proofs are different in detail.
The rule eSkipHav reflects the $\forall\exists$ nature of the judgment,
existentially quantifying $x$ on the right state
whereas eHavSkip universally quantifies it on the left.

Note that eIf and eDo do not existentially quantify over guarded commands on the right, as one might guess at first.  This would be unsound, because property (<ref>) universally quantifies over all pairs of initial states.
A distinguishing feature of the $\aespecSym$ judgment is that it does not validate the rule of conjunction which is sound for the $\forall\forall$ judgment.  For example,
both $\skipc\sep\havc{x} : \aespec{true}{x<0}$ and
$\skipc\sep\havc{x} : \aespec{true}{x>0}$ are valid
but not $\skipc\sep\havc{x}:\aespec{true}{x<0 \land x>0}$.

In  <cit.> the first of the following rules is proposed:

xx' : (x|(|x'))

x:=e x':=e' : x|x'e|e'

It expresses that $\P$ in the initial state must be total as a relation from $x$ on the left to $x'$ on the right.
It can be derived as follows.
Instantiate eHavSkip as
$\havc{x}\sep\skipc : \aespec{(\allSet{x|}{(\someSet{|x'}{\P})})}{\someSet{|x'}{\P}}$.
Then use eSeq with
$\skipc\sep\havc{x}:\aespec{\someSet{|x}{P}}{P}$ (from eSkipHav)
to get
$\havc{x};\skipc \sep \skipc;\havc{x'} : \aespec{(\allSet{x|}{(\someSet{|x'}{\P})})}{\P}$.
Now obtain the proposed rule by eRewrite using skip identity laws.
Similarly, eAsgnAsgn can be derived using
eSkipAsgn, eAsgnSkip, eSeq and eRewrite.

Besides eSkipHav, the other noticeable difference from RHL+ is eDo.
Like the rule rDo in RHL+, eDo captures a conditional alignment of iterations directed by the
relations $\Lrel$ and $\R$.  Each of the premises is a $\forall\exists$ judgment
and the side condition on the invariant $\Q$ ensures adequacy in the sense of covering all iterations.  The rule differs
from rDo in its treatment of right-only iterations.  The $\forall\exists$
judgment requires termination on the right, and the rule relies on the standard
approach of showing a variant decreases.  The variant, $V$, can be of any type $D$ where
$(D,\prec)$ is some well-founded set.  The logical variable $k$ which is
required to be fresh is used to snapshot the value of $V$ in the pre-relation.

All the rules of ERHL+ (Fig. <ref>) are sound.

§.§ Alignment automata

For $\forall\exists$ reasoning, we adapt Def. <ref> of alignment
product to include an additional state predicate which serves to filter product

Suppose $\aprod(A,A',L,R,J)$ is an alignment automata as in
Def. <ref>.  Let keep set $K$ be a subset of
$(Ctrl \times Ctrl') \times (Sto \times Sto')$.  The filtered alignment
automaton $\aprod(A,A',L,R,J,K)$ is the automaton
$((Ctrl\times Ctrl'), (Sto\times Sto'), (\init,\init'), (\fin,\fin'),
\biTrans_K)$ where $\biTrans_K$ is defined by:
$((n,n'),(s,s')) \biTrans_K ((m,m'),(t,t'))$ iff $((m,m'),(t,t')) \in K$ and
$((n,n'),(s,s')) \biTrans ((m,m'),(t,t'))$.

Here the un-subscripted $\biTrans$ refers to the relation in Def. <ref>.
Note that $K$ is used in $\biTrans_K$ to filter states that the product steps
to.  As a consequence $[\init\mid\init']\lor K$ is always a true-invariant of $\biTrans_K$.
Apart from this use of $K$, the transition relation is the same as
the relation $\biTrans$ for unfiltered alignment automata (Def. <ref>).

§.§.§ Adequacy of filtered alignment automata

Let $\aprod(A,A',L,R,J,K)$ be a filtered alignment automata and let
$\Q \subseteq (Sto \times Sto')$.  The filtered automata is $\Q$-adequate in
the $\forall\exists$ sense provided for all $(s,s') \in Q$ and $t$ with
$(\init,s) \trans^* (\fin,t)$, there exists a $t'$ such that
$((\init,\init'),(s,s')) \biTrans^*_K ((\fin,\fin'),(t,t')).$

[Adequacy semantically sound and complete]lemmalemaeAdequate

Given automata $A$,$A'$ and store relations $\Q$, $\S$, we have
$A,A'\models\aespec{\Q}{\S}$ iff there exists a filtered product
$\aprod(A,A',L,R,J,K)$ that is $\Q$-adequate in the $\forall\exists$ sense and
moreover $\aprod(A,A',L,R,J,K)\models\spec{\Q}{\S}$.

The above lemma sheds light on an approach for verifying $\forall\exists$
properties: to show $A,A'\models\aespec{\Q}{\S}$,
construct a filtered product, prove it's adequate and
satisfies the partial correctness spec
The latter amounts to proving a $\forall\forall$ property of the set of trace pairs represented by the product.

As in the $\forall\forall$ setting, a proof method needs to connect adequacy with annotations and alignment conditions.
Leaving aside the annotations, here is a sketch of sufficient conditions for adequacy in the $\forall\exists$
sense.  Suppose we want to show the filtered product $\aprod(A,A',L,R,J,K)$ is
$\Q$-adequate.  Having $K \land (L \lor R \lor J \lor [\fin|\fin'])$ be
$\Q$-invariant ensures the product can always perform left-only, right-only,
or joint steps.  Since transitions by $\biTrans_K$ are filtered by the keep set $K$,
we need some conditions to ensure that it keeps enough.
In the following we use $\trans$ and $\trans'$ for the transition relations of
$A$ and $A'$.

The first condition says that $K$ is left-permissive in the sense that it does
not preclude any traces of $A$.  It can be expressed as

\[
\all{((n,n'),(s,s')) \in K \land L}{\all{m,t}{(n,s)\trans(m,t)\imp ((m,n'),(t,s'))\in K}}
\]

This ensures that all transitions of $A$ can be covered by left-only
transitions of $\aprod(A,A',L,R,J,K)$, and inductively, that all traces of $A$
can be covered.  It applies to states $((n,n'),(s,s'))$ that are kept by
$K$ where the product is poised to perform a left-only step.
The second
condition says that $K$ is joint-productive:

\[
\all{((n,n'),(s,s')) \in K \land J}{\all{m, t}{(n,s)\!\trans\!(m,t) \imp
\some{m',t'}{(n',s')\!\trans'\!(m',t') \land ((m,m'),(t,t')) \in K}}}
\]

That is, when the product is ready to take a joint step, for any transition
of $A$ there will be a corresponding transition of $A'$ that is kept by $K$.
Finally, the third condition says that $K$ is right-productive in the
sense that $K$ is not just keeping divergent traces of $A'$:
there should be a variant function $V$ from
$Ctrl' \times Sto'$ to $D$, where $(D,\prec)$ is some well-founded set,
such that

\[\all{((n,n'),(s,s'))\in K \land R}{\some{m',t'}{(n',s')\!\trans'\!(m',t')
\land ((n,m'),(s,t')) \in K \land V(m',t') \prec V(n',s')}}
\]

Since adequacy in the $\forall\exists$ sense requires the existence of a
terminated product trace, right-only steps must not run forever.  This is
ensured by the condition $V(m',t') \prec V(n',s')$.

The three conditions on $K$ together with
$L \lor R \lor J \lor [\fin|\fin']$ being $\Q$-invariant
(and $K$ holding initially) are
sufficient to ensure the product covers all traces of $A'$ and some traces of
$A'$ which implies $\Q$-adequacy in the $\forall\exists$ sense.
Like with the
$\forall\forall$ setting however, we want these conditions to be tied to an
annotation so that we have an inductive way of establishing them.  We'll
return to this shortly, when we formalize alignment completeness of ERHL+.

§.§.§ Verification conditions for filtered alignment automata

Let $an$ be an annotation for the filtered alignment automaton
$\aprod(A,A',L,R,J,K)$ for $\spec{\S}{\T}$.  For each pair of control points
$(n,n')$, $(m,m')$ of the product, the corresponding VC is given by
definition (<ref>) instantiated by $\biTrans_K$.

Restricting attention to filtered alignment automata of programs, the VCs can be
expressed in a form similar to those for (unfiltered) alignment automata as
given in Fig. <ref> and Fig. <ref>.  The key difference is
in how the keep set $K$ is handled.
To facilitate the definitions, we define for any control points $(n,n')$
the state set $\graybox{$K(n,n')$} \eqdef \{ ((i,i'),(s,s')) \mid ((n,n'),(s,s')) \in K \}$.

if $\sub(n',c')$ is …
and $m'$ is…
then the VC for $((n,n'),(n,m'))$ is equivalent to $\ldots$

$\lskipc{n'}$     $\fsuc(n',c',f')$     $R \land \breve{an}(n,n') \land K(n,m') \imp \hat{an}(n,m')$

$\lassg{n'}{x'}{e'}$     $\fsuc(n',c',f')$
$R \land \breve{an}(n,n') \land \subst{K(n,m')}{\smSep x'}{\smSep e'}
\imp \subst{\hat{an}(n,m')}{\smSep x'}{\smSep e'}$

$\lhavc{n'}{x'}$     $\fsuc(n',c',f')$
$\all{v'\in\Z}{R \land \breve{an}(n,n') \land \subst{K(n,m')}{|x'}{|v'} \imp \subst{\hat{an}(n,m')}{|x'}{|v'}}$

$\lifgc{n'}{gcs'}$     $\lab(d')$ where $e' \gcto d'$ is in $gcs'$
$R \land \breve{an}(n,n') \land \rightF{e'} \land K(n,m') \imp \hat{an}(n,m')$

$\ldogc{n'}{gcs'}$     $\lab(d')$ where $e' \gcto d'$ is in $gcs'$
$R \land \breve{an}(n,n') \land \rightF{e'} \land K(n,m') \imp \hat{an}(n,m')$

$\ldogc{n'}{gcs'}$     $\fsuc(n',c',f')$
$R \land \breve{an}(n,n') \land \neg\rightF{\enab(gcs')} \land K(n,m') \imp \hat{an}(n,m')$

In all other cases, there are no transitions from $(n,n')$ to $(n,m')$ so the VC is $true$ by definition.

The right-only VCs for annotation $an$ of

Fig. <ref> lists right-only VCs for the filtered product
As an example, consider the VC for right-only
$\lhavc{n'}{x'}$.  It says that for any value of $x'$, if $R$ and
$\breve{an}(n,n')$ hold, and that value of $x'$ will be “kept” by $K$ when
control reaches $(n,m')$, then the annotation at $(n,m')$ holds for that value
of $x'$.  Left-only VCs are similar.
Fig. <ref> lists a selected set of joint VCs.

if $\begin{array}[t]{l}
\sub(n,c) \\
\sub(n',c')
\end{array}$
and $\begin{array}[t]{l} m \\ m' \end{array}$ are…
then the VC for $((n,n'),(m,m'))$ is equivalent to $\ldots$

$\lassg{n}{x}{e}$     $\fsuc(n,c,f)$
$J \land \breve{an}(n,n')\land \rightF{e'} \land \subst{K(m,m')}{x|}{e|} \imp \subst{\hat{an}(m,m')}{x|}{e|}$

$\lifgc{n'}{gcs'}$     $\lab(d')$ where $e'\gcto d'$ is in $gcs'$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $\all{v\in\Z}{J \land \breve{an}(n,n') \land \subst{K(m,m')}{x|}{v|} \imp \subst{\hat{an}(m,m')}{x|}{v|}}$

$\lskipc{n'}$     $\fsuc(n',c',f')$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $\all{v\in\Z}{J \land \breve{an}(n,n') \land \subst{K(m,m')}{x|x'}{v|e'} \imp \subst{\hat{an}(m,m')}{x|x'}{v|e'}}$

$\lassg{n'}{x'}{e'}$     $\fsuc(n',c',f')$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $\all{v\in\Z}{J \land \breve{an}(n,n') \land \rightF{e'} \land \subst{K(m,m')}{x|}{v|} \imp \subst{\hat{an}(m,m')}{x|}{v|}}$

$\ldogc{n'}{gcs'}$     $\lab(d')$ where $e'\gcto d'$ is in $gcs'$

$\lhavc{n}{x}$     $\fsuc(n,c,f)$     $\all{v,v'\in\Z}{J \land \breve{an}(n,n') \land \subst{K(m,m')}{x|x'}{v|v'} \imp \subst{\hat{an}(m,m')}{x|x'}{v|v'}}$

$\lhavc{n'}{x'}$     $\fsuc(n',c',f')$

3lOmitted: the other 31 cases with nontrivial VCs.

Selected joint VCs for $\aprod(\aut(c,f),\aut(c',f'),L,R,J,K)$ and annotation $an$.

The following two lemmas mirror Cor. <ref> and
Cor. <ref>.  However, Lemma. <ref> gives a
weaker result than Cor. <ref>; we return to this later.

Suppose $\aprod(A,A',L,R,J,K)$ is $\Q$-adequate in the $\forall\exists$ sense
and $an$ is an annotation of the product for $\spec{\Q}{\S}$.  If $an$ is valid,
then $A,A'\models\aespec{\Q}{\S}$.

Suppose $A,A'\models\aespec{\Q}{\S}$.  Then there exists a filtered
product $\aprod(A,A',L,R,J,K)$ and an annotation $an$ such that the product is
$\Q$-adequate and the annotation is valid for $\spec{\Q}{\S}$.

§.§ Alignment completeness of ERHL+

Given $\aprod(\aut(c,f),\aut(c',f'),L,R,J,K)$, we say $K$ is an adequate
filtering for annotation $an$ and the product iff there exists a
function $V : ((\labs(c')\cup\{f'\}) \times (\Var\to\Z)) \to D$ where
$(D,\prec)$ is a well-founded set, such that the following hold

(a) [left-permissive] For any $n,n'$ and any control successor $m$ of $n$

$\breve{an}(n,n') \land L \imp \PRE(\biTranSeg{(n,n'),(m,n')})(K(m,n'))$

(b) [right-productive] For any $n,n'$ and any control successor $m'$ of $n'$

$\breve{an}(n,n') \land R \imp \EPRE(\biTranSeg{(n,n'),(n,m')})(K(n,m') \land \rightF{V(m')\prec V(n')})$

(c) [joint-productive] For any $n,n'$ and control successors $m,m'$ of $n,n'$

$\breve{an}(n,n') \land J \imp \PRE(\biTranSeg{(n,n'),(m,n')})(\EPRE(\biTranSeg{(m,n'),(m,m')})(K(m,m')))$

where $\EPRE$ is the existential pre-image operator[Direct image of converse:
For $R \subseteq X \times Y$ and $B \subseteq Y$, $\EPRE(R)(B) \eqdef \{ a \in X \mid \some{b \in B}{R (a,b)} \}$].

In Def. <ref>, $\biTrans$ is the unfiltered transition
relation of the associated $L, R, J$ product (Def. <ref>).  The
indexed variant $V(n')$ in condition $(b)$ equates to the value of $V$ in state
$(n',s')$.  Formally, $V(n')$ is a function with the same type as $V$ and is
defined as $\graybox{$V(n') (m',s')$} \eqdef V(n',s')$.

The use of $\PRE$ and $\EPRE$ in Def. <ref> allows (a),
(b), and (c) to be expressed as conditions on pre-states.  They're formulated
in terms of $an$ rather than as closure conditions on $K$, which makes them
easier to prove (as in the two examples in Sect. <ref>, worked
out in Sect. <ref>).

We now turn to the alignment completeness result for ERHL+.  As in
Theorem. <ref>, the proof uses only relational assertions
derived from $an(i,j)$.

Like in Theorem <ref>, the syntactic constraints in condition (a)
help streamline the proof, but lose no generality.  Conditions (c) and (d)
capture adequacy of the filtered product, so together (b), (c), and (d) constitute an IAM-style proof.

(a) $\okf(c,f)$ and $\okf(c',f')$.

(b) $an$ is a valid annotation of $\aprod(\aut(c,f),\aut(c',f'),L,R,J,K)$
for $\spec{\S}{\T}$.

(c) $\breve{an}(i,j)\imp L \lor R \lor J \lor [\fin|\fin']$ for all control
points $(i,j)$ of the product.

(d) $K$ is an adequate filtering for $an$ and $\aprod(\aut(c,f),\aut(c',f'),L,R,J,K)$.

Then the judgment $c\sep c' : \aespec{\S}{\T}$ has a proof in ERHL+.

The lengthy proof is similar to that of Theorem <ref>.  We start by
choosing a fresh variable $pc$, transform $c,c'$ to their automata normal
forms, and apply rule eDo.  The loop invariant $\Q$ is identical to the
one defined in the proof of Theorem <ref>.  The main difference
between the two proofs is in how each of the premises of the loop rule are
established.  As in the proof for RHL+, we derive premises of eDo by the
assignment and sequence rules, and eConseq, using VCs provided by $an$.
However, VCs of filtered automata have antecedents involving $K$, see
Fig <ref> and Fig. <ref>.  So to exploit the VCs, in
applications of eConseq, we rely on the fact that $K$ is an adequate
filtering.  Proofs of left-only and right-only premises use eDisj as in
the proof of Theorem <ref>.  For right-only premises, we
additionally need to reason about the variant, for which we rely on the
right-productivity condition of Def. <ref>.
Finally, having used eDo to show
that the automata normal forms of $c$ and $c'$ satisfy $\aespec{\S}{\T}$, we
finish the proof using eRewrite and ghost elimination to conclude the
same judgment for $c,c'$.

§ RELATED WORK

Trace logic <cit.> reasons about $\forall\forall$ properties by way of constraints between arbitrary different points in the traces rather than restricting to points that progress in the manner of a schedule–what we call alignment.
In principle alignments may be defined by arbitrary strategy functions and the like <cit.>.
We confine attention to assertion-oriented work.

Cook completeness has been proved for several $\forall\forall$ relational Hoare logics (e.g., <cit.>)
using in each case the completeness of sequential alignment.
We are not aware of any alignment completeness results besides those in <cit.>.
They give several $\forall\forall$ alignment completeness results for ad hoc automata forms specialized to account for alignments given by particular proof rules.
Their proofs of alignment completeness are quite different from ours and do not involve a rule for rewriting.

Several published logics only support lockstep alignment of loops,
or lockstep until one terminates.  The conditionally aligned loop rule appears first in Beringer <cit.>.
Our adaptation for $\forall\exists$ is new.

We are not aware of unary HLs that feature a rewriting rule,
but verification tools often use correctness-preserving rewriting.
The RHLs of Barthe et al <cit.> and Banerjee et al <cit.> each feature a rewriting rule
and a custom set of rules for command equivalence (with a relational precondition, in <cit.>). (The judgments of <cit.> are probabilistic but alignment is still central.)
Rewriting by command equivalence is combined with relational reasoning
in an extension of KAT called BiKAT <cit.>.

The $\forall\forall$ property is also known as 2-safety <cit.>.
Cartesian Hoare logic <cit.> reasons about $k$-safety, for $k$ that is fixed throughout a proof.
D’Osualdo et al <cit.> develop a logic for $k$-safety that features rules for combining judgments with varying $k$;
they have a completeness result based essentially on sequential alignment
as explained in <cit.>.
The system of D'Osualdo et al includes a rewriting rule, but based on semantic refinement
(i.e., refinement is not formalized in a deductive system but rather must be proved
in the metalogic).
Our results should generalize to $k>2$ but the case of 2 admits simpler notations.

Except as noted, none of the preceding works  consider $\forall\exists$ properties.
Hawblitzel et al <cit.> use the term relative termination for $\forall\exists$ judgments, emphasizing
an advantage that is relevant even for deterministic programs: relational judgments compose transitively.
Rinard and Marinov <cit.> give a logical formulation of verification conditions for a $\forall\exists$ relation, to prove correctness of compiler transformations acting on control flow graphs.
Antonopoulos et al <cit.> derive some deductive rules for $\forall\exists$
(and also the variation known as backward simulation), in a KAT-based algebraic framework.
Their “witness” technique for $\forall\exists$ reasoning is akin to our filtering $K$ condition,
obtaining existence by filtering behaviors of an $\forall\forall$ automaton,
by contrast with works that literally construct witness executions <cit.>.

An early formulation of relational verification using automata is <cit.>.
Their work includes a notion of asymmetric product for verifying $\forall\exists$ properties.
Their adequacy conditions (called leftness) are more restrictive than what is found in recent work.

To our knowledge, the first published deductive system for pre-post $\forall\exists$ properties is that of
Dickerson et al <cit.>.
It is based on HL together with unary rules for forward underapproximation
(the property expressed by $\skipc\sep c:\aespec{\rightF{P}}{\rightF{Q}}$ in our setting),
and the core rules of RHLE reduce relational reasoning to sequential unary reasoning.
Soundness is proved and an algorithm for proof search is given.
The system includes rules for modular reasoning using unary procedure specs,
and uses over- and under-approximate semantics of procedure calls
(which is like specification statements <cit.>, in the over-approximate case).
Loops are handled using the mostly lockstep rules like <cit.>.
The use of unary procedure specs gives rise to nondeterminacy, motivating the use of $\forall\exists$ judgements; by contrast, Eilers et al <cit.> and Banerjee et al <cit.> use relational procedure specs for $\forall\forall$ properties.

Turning to IAM-style verification,
the work of Churchill et al <cit.>, Shemer et al <cit.>,
and Unno et al <cit.> can be seen as various techniques for finding
adequate alignment conditions ($L,R,J$) and annotations expressible in SMT-supported assertion languages.
(Instead of adequacy and alignment, one finds terminology including fair scheduler.)
Churchill et al also use testing to evaluate whether a candidate $(L,R,J)$ is invariant.
Our example $c1$ (Sect. <ref>) is from Unno et al <cit.>; they formulate adequacy conditions for $\forall\exists$
properties, whereas the others only address $\forall\forall$.
Unno et al address the right-only progress condition for $\forall\exists$ by finding a well-founded relation between transition states; this is not directly representable in a logic of pre/post relations (though it may be in a logic like RHTT <cit.> where postconditions constrain two initial + two final states),
so we need variant function $V$ and a fresh snapshot variable in rule eDo.
Instead of filtering, Unno et al require that choices on right be given by a function of the left state together with prophecy variables about the final state on the left.
Our formalization enables use of prophecy for both final and intermediate values.

Beutner and Finkbeiner <cit.> formulate temporal $\forall\exists$ properties in terms of games, so a proof involves a strategy whereby the $\exists$ player produces a witnessing execution.  They represent programs by transition systems, and combine the search for a strategy with search for an alignment (called reduction, cf. <cit.>) and filtering conditions (called restrictions), also represented as a game. Their adequacy conditions take into account under-approximate abstract interpretation
which is used in their algorithm for solving games.

Beutner and Finkbeiner <cit.> show that with the inclusion of prophecy variables, a game based method is complete for finite state systems (and synchronous HyperLTL).

Further afield, ReLoC <cit.>
is a logic of contextual refinement of higher order concurrent programs, a $\forall\exists$ property.
It is based on Iris <cit.> which in turn is implemented in the Coq proof assistant.

Our normal form is like that of Hoare and Sampaio <cit.> which uses an
explicit program counter variable.
They prove every program can be reduced to normal form using a set of refinement laws, demonstrating a kind of completeness of the laws.

Kozen <cit.> uses KAT to prove that every command is simulated by one with a single loop,
using added primitives to snapshot the values of branch conditions.

§ CONCLUSION

We augmented a collection of relational Hoare logic rules with a straightforward
rule for elimination of ghost variables, and a rule for deriving one correctness
judgment from another by rewriting the commands involved to equivalent ones.
The chosen notion of equivalence is that of KAT,
allowing for the use of hypotheses to axiomatize the meaning of primitive
commands and expressions when reasoning with KAT.  Using a small set of
hypotheses, we prove that any command is equivalent to one in automaton normal
form, once it is instrumented with assignments to a $pc$.
On this basis, we show that any correctness judgment proved in IAM style
using an alignment automaton can be turned into a deductive
proof in RHL+ using essentially the same assertions.  That is, RHL+ is
alignment complete.
We introduce a new logic ERHL+ for $\forall\exists$ properties and show its alignment completeness
with respect to a general notion of filtered alignment automata.

Because our development makes no commitment or unusual demands on the assertion language, the results should be applicable to richer data types including pointer structures, and deductive systems including separation logic.  Our program equivalence $\kateq$ makes a minimal demand on reasoning about data: the ability to specify that primitive commands do not interfere with the $pc$.

For languages with procedures, alignment of calls is important to facilitate
use of relational specs <cit.>.  A theory of alignment completeness of such languages is left to future work; it
entails the complications of automata representation for programs and modular IAM.

For $\forall\forall$ properties, it is straightforward to show semantic completeness of manifestly adequate alignment automata, for which we have given an alignment complete logic RHL+.  Together, these results yield Cook completeness of the logic.
By contrast, for $\forall\exists$ properties we show that adequate automata are semantically complete, but we did not yet show the same for manifestly adequate automata.  Manifest adequacy means adequacy proved by conditions tied with an IAM annotation, making it a practical proof technique and amenable to being presented as a deductive proof.  This gap means at this time we lack a proof of Cook completeness for ERHL+.
We expect that the gap can be closed, and note that for similar
forms of $\forall\exists$ alignment product semantic completeness results have been established (e.g., Unno et al obtain one, using lockstep alignment and prophecy variables <cit.>).

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Antonopoulos, Koskinen, Le, Nagasamudram,
Naumann, and NgoAntonopoulos et al2023]
authorpersonTimos Antonopoulos, personEric
Koskinen, personTon Chanh Le, personRamana
Nagasamudram, personDavid A. Naumann, and
personMinh Ngo. year2023.
An Algebra of Alignment for Relational
journalProc. ACM Program. Lang.
volume7, numberPOPL, Article
articleno20 (year2023), numpages30 pages.

Full version at <https://arxiv.org/abs/2202.04278>.

[Apt, de Boer, and OlderogApt
et al2009]
authorpersonKrzysztof R. Apt, personFrank S.
de Boer, and personErnst-Rüdiger Olderog.
booktitleVerification of Sequential and Concurrent
Programs (edition3 ed.).

[Back and von WrightBack and von
authorpersonRalph-Johan Back and
personJoakim von Wright. year1998.
booktitleRefinement Calculus: A Systematic

[Banerjee, Nagasamudram, and NaumannBanerjee
et al2022a]
authorpersonAnindya Banerjee, personRamana
Nagasamudram, and personDavid A. Naumann.
Making Relational Hoare Logic Alignment
journalCoRR  volumeabs/2212.10338

[Banerjee, Nagasamudram, Naumann, and
NikoueiBanerjee et al2022b]
authorpersonAnindya Banerjee, personRamana
Nagasamudram, personDavid A. Naumann, and
personMohammad Nikouei. year2022b.
A Relational Program Logic with Data Abstraction
and Dynamic Framing.
journalACM Transactions on Programming Languages and
Systems volume44, number4 (year2022),

[Banerjee, Naumann, and NikoueiBanerjee
et al2016]
authorpersonAnindya Banerjee, personDavid A.
Naumann, and personMohammad Nikouei.
Relational Logic with Framing and Hypotheses. In
booktitleFoundations of Software Tech. and Theoretical Comp.
Sci. pages11:1–11:16.
Technical report at <http://arxiv.org/abs/1611.08992>.

[Barthe, Crespo, and KunzBarthe
et al2013]
authorpersonGilles Barthe, personJuan Manuel
Crespo, and personCésar Kunz.
Beyond 2-Safety: Asymmetric Product Programs for
Relational Program Verification. In booktitleLogical
Foundations of Computer Science, International Symposium
(seriesLNCS), Vol. volume7734.

[Barthe, D'Argenio, and RezkBarthe
et al2004]
authorpersonGilles Barthe, personPedro R.
D'Argenio, and personTamara Rezk.
Secure Information Flow by Self-Composition. In
booktitleIEEE Computer Security Foundations Workshop
(CSFW'04). pages100–114.

[Barthe, Eilers, Georgiou, Gleiss, Kovács,
and MaffeiBarthe et al2019]
authorpersonGilles Barthe, personRenate
Eilers, personPamina Georgiou, personBernhard
Gleiss, personLaura Kovács, and personMatteo
Maffei. year2019.
Verifying relational properties using Trace
Logic. In booktitle2019 Formal Methods in Computer Aided
Design (FMCAD). pages170–178.

[Barthe, Grégoire, Hsu, and StrubBarthe
et al2017]
authorpersonGilles Barthe, personBenjamin
Grégoire, personJustin Hsu, and
personPierre-Yves Strub. year2017.
Coupling proofs are probabilistic product
programs. In booktitleACM Symposium on Principles of
Programming Languages. pages161–174.

[Baumeister, Coenen, Bonakdarpour, Finkbeiner,
and SánchezBaumeister et al2021]
authorpersonJan Baumeister, personNorine
Coenen, personBorzoo Bonakdarpour, personBernd
Finkbeiner, and personCésar Sánchez.
A Temporal Logic for Asynchronous Hyperproperties.
In booktitleComputer Aided Verification
(seriesLNCS), Vol. volume12759.

authorpersonN. Benton.
Simple Relational Correctness Proofs for Static
Analyses and Program Transformations. In booktitleACM
Symposium on Principles of Programming Languages. publisherACM,

authorpersonLennart Beringer.
Relational Decomposition. In
booktitleInteractive Theorem Proving (ITP)
(seriesLNCS), Vol. volume6898.

[Beutner and FinkbeinerBeutner and
authorpersonRaven Beutner and personBernd
Finkbeiner. year2022a.
Prophecy Variables for Hyperproperty Verification.
In booktitleIEEE Computer Security Foundations.

[Beutner and FinkbeinerBeutner and
authorpersonRaven Beutner and personBernd
Finkbeiner. year2022b.
Software Verification of Hyperproperties Beyond
k-Safety. In booktitleComputer Aided Verification
(seriesLNCS), editorpersonSharon
Shoham and personYakir Vizel (Eds.),
Vol. volume13371. pages341–362.

[Cao, Beringer, Gruetter, Dodds, and AppelCao
et al2018]
authorpersonQinxiang Cao, personLennart
Beringer, personSamuel Gruetter, personJosiah Dodds,
and personAndrew W Appel. year2018.
VST-Floyd: A separation logic tool to verify
correctness of C programs.
journalJournal of Automated Reasoning
volume61, number1 (year2018),

[Churchill, Padon, Sharma, and AikenChurchill
et al2019]
authorpersonBerkeley R. Churchill,
personOded Padon, personRahul Sharma, and
personAlex Aiken. year2019.
Semantic program alignment for equivalence
checking. In booktitleACM Conf. on Program. Lang. Design
and Implementation. pages1027–1040.

[Clochard, Marché, and
PaskevichClochard et al2020]
authorpersonMartin Clochard, personClaude
Marché, and personAndrei Paskevich.
Deductive verification with ghost monitors.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[Cohen, Kozen, and SmithCohen
et al1996]
authorpersonErnie Cohen, personDexter
Kozen, and personFrederick Smith.
booktitleThe complexity of Kleene algebra with
typeTechnical Report TR96-1598.
institutionCornell University.

authorpersonStephen A. Cook.
Soundness and completeness of an axiom system for
program verification.
journalSIAM J. Comput. volume7,
number1 (year1978), pages70–90.

[Dickerson, Ye, Zhang, and DelawareDickerson
et al2022]
authorpersonRobert Dickerson,
personQianchuan Ye, personMichael K. Zhang, and
personBenjamin Delaware. year2022.
RHLE: Modular Deductive Verification of
Relational \(\forall\) \(\exists\) Properties. In
booktitleAsian Symposium on Programming Languages and
Systems (seriesLNCS), Vol. volume13658.

[Dijkstra and ScholtenDijkstra and
authorpersonEdsger W. Dijkstra and
personCarel S. Scholten. year1990.
booktitlePredicate Calculus and Program Semantics.

[D’Osualdo, Farzan, and DreyerD’Osualdo
et al2022]
authorpersonEmanuele D’Osualdo,
personAzadeh Farzan, and personDerek Dreyer.
Proving Hypersafety Compositionally.
journalProc. ACM Program. Lang.
volume6, numberOOPSLA2, Article
articleno135 (year2022),
numpages26 pages.

[Eilers, Müller, and HitzEilers
et al2020]
authorpersonMarco Eilers, personPeter
Müller, and personSamuel Hitz.
Modular Product Programs.
journalACM Trans. Program. Lang. Syst.
volume42, number1 (year2020),

[Farzan and VandikasFarzan and
authorpersonAzadeh Farzan and
personAnthony Vandikas. year2019.
Automated Hypersafety Verification. In
booktitleComputer Aided Verification
(seriesLNCS), Vol. volume11561.

[Filliâtre, Gondelman, and
PaskevichFilliâtre et al2016]
authorpersonJean-Christophe Filliâtre,
personLéon Gondelman, and personAndrei
Paskevich. year2016.
The Spirit of Ghost Code.
journalFormal Methods in System Design
volume48, number3 (year2016),

authorpersonRobert Floyd.
Assigning Meaning to Programs. In
booktitleSymp. on Applied Math. 19, Math. Aspects of Comp.
Sci. publisherAmer. Math. Soc., pages19–32.

authorpersonNissim Francez.
Product Properties and Their Direct Verification.
journalActa Informatica  volume20
(year1983), pages329–344.

[Frumin, Krebbers, and BirkedalFrumin
et al2018]
authorpersonDan Frumin, personRobbert
Krebbers, and personLars Birkedal.
ReLoC: A Mechanised Relational Logic for
Fine-Grained Concurrency. In booktitleProceedings of the
33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018,
Oxford, UK, July 09-12, 2018, editorpersonAnuj
Dawar and personErich Grädel (Eds.).
publisherACM, pages442–451.

[Godlin and StrichmanGodlin and
authorpersonBenny Godlin and personOfer
Strichman. year2008.
Inference rules for proving the equivalence of
recursive procedures.
journalActa Inf. volume45,
number6 (year2008), pages403–439.

[Hawblitzel, Kawaguchi, Lahiri, and
RebêloHawblitzel et al2013]
authorpersonChris Hawblitzel, personMing
Kawaguchi, personShuvendu K. Lahiri, and
personHenrique Rebêlo. year2013.
Towards Modularly Comparing Programs Using
Automated Theorem Provers. In booktitleCADE
(seriesLNCS), Vol. volume7898.

[Hoare, He, and SampaioHoare
et al1993]
authorpersonC. A. R. Hoare, personJifeng
He, and personAugusto Sampaio.
Normal Form Approach to Compiler Design.
journalActa Informatica volume30,
number8 (year1993), pages701–739.

[Jung, Krebbers, Jourdan, Bizjak, Birkedal, and
DreyerJung et al2018]
authorpersonRalf Jung, personRobbert
Krebbers, personJacques-Henri Jourdan, personAles
Bizjak, personLars Birkedal, and personDerek
Dreyer. year2018.
Iris from the ground up: A modular foundation for
higher-order concurrent separation logic.
journalJ. Funct. Program.  volume28
(year2018), pagese20.

[Kovács, Seidl, and FinkbeinerKovács
et al2013]
authorpersonMáté Kovács,
personHelmut Seidl, and personBernd Finkbeiner.
Relational abstract interpretation for the
verification of 2-hypersafety properties. In booktitleACM
Computer and Communications Security. pages211–222.

authorpersonDexter Kozen.
Kleene algebra with tests.
journalACM Transactions on Programming Languages and
Systems volume19, number3 (year1997),

authorpersonDexter Kozen.
On Hoare logic and Kleene algebra with tests.
journalACM Trans. Comput. Log.
volume1, number1 (year2000),

[Kozen and SmithKozen and Smith1996]
authorpersonDexter Kozen and
personFrederick Smith. year1996.
Kleene algebra with tests: Completeness and
decidability. In booktitleInternational Workshop on
Computer Science Logic (seriesLNCS),
Vol. volume1258. pages244–259.

[Lamport and SchneiderLamport and
authorpersonLeslie Lamport and
personFred B. Schneider. year2021.
Verifying Hyperproperties With TLA. In
booktitleIEEE Computer Security Foundations.

authorpersonCarroll Morgan.
The specification statement.
journalACM Transactions on Programming Languages and
Systems volume10, number3 (year1988),

[Nagasamudram and NaumannNagasamudram and
authorpersonRamana Nagasamudram and
personDavid A. Naumann. year2021.
Alignment Completeness for Relational Hoare
Logics. In booktitleIEEE Symp. on Logic in Computer
Extended version at <https://arxiv.org/abs/2101.11730>.

[Nanevski, Banerjee, and GargNanevski
et al2013]
authorpersonAleksandar Nanevski,
personAnindya Banerjee, and personDeepak Garg.
Dependent Type Theory for Verification of
Information Flow and Access Control Policies.
journalACM Trans. Program. Lang. Syst.
volume35, number2 (year2013),

authorpersonTobias Nipkow.
Hoare Logics for Recursive Procedures and Unbounded
Nondeterminism. In booktitleComputer Science Logic
(seriesLNCS), Vol. volume2471.

authorpersonPeter W O'Hearn.
Incorrectness logic.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[Pick, Fedyukovich, and GuptaPick
et al2018]
authorpersonLauren Pick, personGrigory
Fedyukovich, and personAarti Gupta.
Exploiting Synchrony and Symmetry in Relational
Verification. In booktitleComputer Aided Verification
(seriesLNCS), Vol. volume10981.

[Pierce, de Amorim, Casinghino, Gaboardi,
Greenberg, Hriţcu, Sjöberg, Tolmach, and YorgeyPierce
et al2022]
authorpersonBenjamin C. Pierce,
personArthur Azevedo de Amorim, personChris
Casinghino, personMarco Gaboardi, personMichael
Greenberg, personCătălin Hriţcu, personVilhelm
Sjöberg, personAndrew Tolmach, and personBrent
Yorgey. year2022.
booktitleProgramming Language Foundations.
seriesSoftware Foundations, Vol. volume2.
publisherElectronic textbook.
Version 6.2, <http://softwarefoundations.cis.upenn.edu>.

authorpersonMartin Rinard.
booktitleCredible Compilation.
typeTechnical Report MIT-LCS-TR-776.

[Rinard and MarinovRinard and
authorpersonMartin Rinard and personDarko
Marinov. year1999.
Credible Compilation with Pointers. In
booktitleProceedings of the FLoC Workshop on Run-Time
Result Verification.

[Shemer, Gurfinkel, Shoham, and VizelShemer
et al2019]
authorpersonRon Shemer, personArie
Gurfinkel, personSharon Shoham, and personYakir
Vizel. year2019.
Property Directed Self Composition. In
booktitleComputer Aided Verification
(seriesLNCS), Vol. volume11561.

[Sousa and DilligSousa and Dillig2016]
authorpersonMarcelo Sousa and personIsil
Dillig. year2016.
Cartesian Hoare logic for verifying k-safety
properties. In booktitleACM Conf. on Program. Lang. Design
and Implementation. pages57–69.

[Terauchi and AikenTerauchi and
authorpersonTachio Terauchi and personAlex
Aiken. year2005.
Secure information flow as a safety problem. In
booktitleInternational Static Analysis Symposium
(seriesLNCS), Vol. volume3672.

[Unno, Terauchi, and KoskinenUnno
et al2021]
authorpersonHiroshi Unno, personTachio
Terauchi, and personEric Koskinen.
Constraint-Based Relational Verification. In
booktitleComputer Aided Verification
(seriesLNCS), Vol. volume12759.

[Wang, Dillig, Lahiri, and CookWang
et al2018]
authorpersonYuepeng Wang, personIsil
Dillig, personShuvendu K. Lahiri, and
personWilliam R. Cook. year2018.
Verifying equivalence of database-driven
journalProc. ACM Program. Lang.
volume2, numberPOPL (year2018),

authorpersonHongseok Yang.
Relational Separation Logic.
journalTheoretical Computer Science
volume375, number1-3 (year2007),

§ APPENDIX: DETAILS FOR SECTION <REF>

n  s  s

t = sxe(s)
xe  s  t

x  s  sxv

c s  u
d u  t
c;d s t

eb  gcs

b s t

gcs s t

eb  gcs

b s u

gcs u t

gcs s t

gcs s s

Denotational semantics $\means{c}$ (omitting labels which are unconstrained).

Fig. <ref> presents the pre-post relation denoted by a command, defined inductively in big-step style.

c: PQ

d: PQ

c: PQ

(x,c) : PQ

c: ePP

gcs: PP(gcs)

[Asgn] xe : PxeP

c;d : PQ

c: ePQ

gcs: PQ

c : RS

c : PQ

Proof rules of HL+

Definition of HL+: Fig. <ref> gives the full set of proof rules.

Apropos the $\totalIf$ condition in Def. <ref>,
we choose the semantic formulation
in order to highlight the minimal requirements needed
for the alignment completeness theorem.  In a logic without a rewrite rule, the $\totalIf$ condition can simply be enforced by side condition in the rule for if-commands:
$precond\imp\enab(gcs)$ (see <cit.>).
This is insufficient in our logics because if-commands can be rewritten to other forms.

Here is a syntactic way to ensure the semantic condition $\totalIf$
on $\lifgc{}{gcs}$.
Require that for each $e\gcto c$ in $gcs$,
there is $e^-\gcto d$ in $gcs$ for some $d$, where $e^-$
is the syntactic complement of $e$.
That is, $(\neg e)^- \eqdef e$ and if $e$ does not have outermost negation
then $e^- \eqdef \neg e$.
This subsumes the usual if-else:
$\lifgc{}{e\gcto c \gcsep \neg e\gcto d}$.
that the if-else form rules out commands like
$\lifgc{}{x\geq 0 \gcto y:=0 \gcsep x \leq 0 \gcto y:=1}$
which satisfy $\totalIf$ but are not deterministic.
To satisfy the syntactic condition we can write it as

$\lifgc{}{ x\geq 0 \gcto y:=0 \gcsep x \ngeq 0 \gcto y:=1 \gcsep
x > 0 \gcto y:=0 \gcsep x \not > 0 \gcto y:=1 }$.

Definition of $\enab(gcs)$ (an expression for the condition under which guarded command list $gcs$ is enabled):

\[
\begin{array}{lcl}
\enab(e\gcto c) & = & e \\
\enab(e\gcto c \gcsep gcs) & = & e \lor \enab(gcs)
\end{array}\]

Definition of $\erase(x,c)$, the command $c$ with each assignment to $x$ replaced by $\skipc$.

\[
\begin{array}{l@{\;}c@{\;}l}
\erase(x,\lskipc{n})          & = & \lskipc{n} \\
\erase(x,\lassg{n}{x}{e})     & = & \lskipc{n} \\
\erase(x,\lassg{n}{y}{e})     & = & \lassg{n}{y}{e} \quad\mbox{for } y\nequiv x\\
\erase(x,\lhavc{n}{x})        & = & \lskipc{n} \\
\erase(x,\lhavc{n}{y})        & = & \lhavc{n}{y} \quad\mbox{for } y\nequiv x\\
\erase(x,\lifgc{n}{gcs})      & = & \lifgc{n}{\map(\erasegc,gcs)} \\
\erase(x,\ldogc{n}{gcs})      & = & \ldogc{n}{\map(\erasegc,gcs)} \\[1ex]
\erasegc(x,e\gcto c)            & = & e \gcto erase(x,c)
\end{array}
\]

§.§ Derived rules

c c' : e

d d' : e

ec ed e'c' e'd' :

c :

d :

c;d :

cd : _i

cd : ii∈X_i

c: e

gcs :

Some derived rules of RHL+ in addition to Fig. <ref>.

Our selection of rules in RHL+ is not minimal for alignment completeness—rIf can be omitted!
(Because in GCL an if can be rewritten as a loop that iterates just once.)
However, we are not arguing that in practice one should make maximal use of rRewrite as
we will do to prove alignment completeness.  In practice, a deductive proof should follow the original program structure to the extent possible, and also make use of derived rules like
the aligned If rule, rAlgnIf, in Fig. <ref>.
which is often presented as a basic rule in RHLs (e.g., <cit.>):
It is easily derived using rIf and rFalse.  So is the similar rule for lockstep alignment of loops.

The one-sided rule rSeqSkip is derivable using rSeq and rRewrite with the equivalence $\skipc;\skipc\kateq\skipc$.
Rule rAsgnAsgn in Fig. <ref> is derived using rSeq and rRewrite
and unit law for $\skipc$.
Rule rLRseq in Fig. <ref> is derived similarly.
By repeated use of rDisj and rConseq one can derive rDisjN.

For our alignment completeness result we do not need one-sided rules other than rSeqSkip.
However, one can derive general rules rIfSkip and DoSkip (and right-side rules as well),
obtaining a left-side rule for each construct in the language, and
mutatis mutandis for the right.
To derive the left-side rule rIfSkip, first use rIf to derive
$ \lifgc{}{gcs} \Sep
\lifgc{}{true \gcto \skipc} : \rspec{\R}{\S}
Now apply rRewrite using the equivalence
$\lifgc{}{true \gcto \skipc} \kateq \skipc$ (and reflexivity of $\kateq$).

As another example derived rule, here is a one-sided loop rule:

\[\inferrule{
c\sep \skipc : \rspec{\Q\land \leftF{e}}{\Q} \quad \mbox{for all $e\gcto c$ in $gcs$}
\ldogc{}{gcs} \sep \skipc : \rspec{\Q}{\Q\land\neg\leftF{\enab(gcs)}}
\]

We can get the conclusion by rRewrite, using the equivalence $\ldogc{}{\mathit{false}\gcto\lskipc{}} \kateq \lskipc{}$,

\[  \ldogc{}{gcs} \sep \ldogc{}{\mathit{false}\gcto\lskipc{}} : \rspec{\Q}{\Q\land\neg\leftF{\enab(gcs)}} \]

The latter follows by rConseq from

\begin{equation}\label{eq:X}
\ldogc{}{gcs} \sep \ldogc{}{\mathit{false}\gcto\lskipc{}} : \rspec{\Q}{\Q\land\neg\leftF{\enab(gcs)}\land\neg\rightF{\mathit{false}}}
\end{equation}

(Note that $\enab(\mathit{false}\gcto\lskipc{})$ is $\mathit{false}$.)
To prove (<ref>) we instantiate rDo with $\Lrel:=true$ and $\R:=true$.
The side condition holds: it is equivalent to
$\Q \imp (\leftex{\enab(gcs)} = \rightex{\mathit{false}}) \lor  \leftF{\enab(gcs)}$,
which amounts to the tautology $\Q\imp \neg\leftF{\enab(gcs)} \lor  \leftF{\enab(gcs)}$.
The joint premises have the form

\[ c\sep \skipc : \rspec{\Q\land \leftF{e}\land\rightF{\mathit{false}}\land\neg true\land\neg true}{\Q} \]

for $e\gcto c$ in $gcs$; these can be derived using rFalse and rConseq.
Similarly for the right-only premises, which have precondition $\rightF{\mathit{false}}$.
The left-only premises have the form

\[ c\sep \skipc : \rspec{\Q\land \leftF{e}\land true}{\Q} \]

which follow by rConseq from the corresponding premise
$c\sep \skipc : \rspec{\Q\land \leftF{e}}{\Q}$ of the one-sided loop rule.

§ APPENDIX: DETAILS FOR SECTION <REF>

Definition of $\lab(c)$:

\[
\begin{array}{lcl}
\lab(\lskipc{n})            & = & n \\
\lab(\lassg{n}{x}{e})       & = & n \\
\lab(\lhavc{n}{x})       & = & n \\
\lab(c;d)                 & = & \lab(c) \\
\lab(\lifgc{n}{gcs})   & = & n \\
\lab(\ldogc{n}{gcs})    & = & n
\end{array}
\]

Definition of $\labs(c)$:

\[
\begin{array}{lcl}
\labs(\lskipc{n})           & = & \{ n \}\\
\labs(\lassg{n}{x}{e})      & = &\{ n\} \\
\labs(\lhavc{n}{x})         & = &\{ n\} \\
\labs(c;d)                & = & \labs(c)\union \labs(d) \\
\labs(\lifgc{n}{gcs})  & = & \{n\} \union \{ m \mid e\gcto c \mbox{ is in }gcs \land
m\in labs(c) \} \\
\labs(\ldogc{n}{gcs})  & = & \{n\} \union \{ m \mid e\gcto c \mbox{ is in }gcs \land
m\in labs(c) \}
\end{array}
\]

Definition of $\ok(c)$ which says $c$ has unique labels, all of which are positive.

\[
\begin{array}{lcl}
\ok(\lskipc{n})            & = & n >  0 \\
\ok(\lassg{n}{x}{e})       & = & n >  0 \\
\ok(\lhavc{n}{x})          & = & n >  0 \\
\ok(c;d)                 & = & \labs(c)\intersect \labs(d)=\emptyset\land \ok(c)\land \ok(d) \\
\ok(\lifgc{n}{gcs})    & = & n > 0 \land n \notin \labs(gcs) \land \okg(gcs) \\
\ok(\ldogc{n}{gcs})    & = & n > 0 \land n \notin \labs(gcs) \land \okg(gcs) \\
\okg(e\gcto c) & = & \ok(c) \\
\okg(e\gcto c \gcsep gcs) & = & \ok(c)\land \labs(c)\intersect \labs(gcs)=\emptyset \land
\okg(gcs)
\end{array}
\]

Definition of $\sub(m,c)$, the sub-command of $c$ at $m$,
assuming $\ok(c)$, and $m\in \labs(c)$.

\[
\begin{array}{lcl}
\sub(m,\lskipc{m})        & = & \lskipc{m} \\
\sub(m,\lassg{m}{x}{e})   & = & \lassg{m}{x}{e} \\
\sub(m,\lhavc{m}{x})      & = & \lhavc{m}{x} \\
\sub(m,c;d)               & = & \sub(m,c)\mbox{ , if $m\in \labs(c)$}  \\
& = & \sub(m,d)\mbox{ , otherwise} \\
\sub(m, \lifgc{n}{gcs}) & = &  \lifgc{n}{gcs} \mbox{ , if $n=m$}  \\
& = &  \subg(m,gcs) \mbox{ , otherwise}  \\
\sub(m, \ldogc{n}{gcs}) & = &  \ldogc{n}{gcs} \mbox{ , if $n=m$}  \\
& = &  \subg(m,gcs) \mbox{ , otherwise}  \\

\subg(m, e\gcto c) & = & \sub(m,c) \\
\subg(m, e\gcto c \gcsep gcs) & = &\sub(m,c) \mbox{ , if $m\in \labs(c)$ }\\
& = & \subg(m,gcs) \mbox{ , otherwise }
\end{array}
\]

Define the direct image operator, $\POST$, for any set $X$ and relation $R$
by $t\in\graybox{$\POST(R)(X)$}$ iff $\some{s}{(s,t)\in R \land s\in X}$.
The universal pre-image operator, $\PRE$, is defined for any set $X$ and relation $R$
by $s\in\graybox{$\PRE(R)(X)$}$ iff $\all{t}{(s,t)\in R \imp t\in X}$.

Informally, for any pair of terminated traces $T,T'$ of $A$ and $A'$,
where $\Q$ holds initially, there is a terminated trace of
$\aprod(A,A',L,R,J)$ of which $T$ and $T'$ are the left and right
This implies $\Q$-adequacy.
The idea is essentially liveness of the alignment automaton: owing to invariance of $L \lor R \lor J \lor [\fin|\fin']$ (and liveness of $L,R,J$ as required by Def.<ref>)
we can always take a step via $\biTrans$ on one or both sides—unless both sides are stuck or terminated, in which case the given pair of traces is covered.

To be precise we make the following claim:

If $(s,s')\in\Q$, $((\init,\init'),(s,s'))\biTrans^*((n,n'),(t,t'))$,
$(n,t)\trans^*(\fin,u)$, and $(n',t')\trans'^*(\fin',u')$
then $((\init,\init'),(s,s'))\biTrans^*((\fin,\fin'),(u,u'))$.

The claim implies $\Q$-adequacy, by taking $((n,n'),(t,t'))=((\init,\init'),(s,s'))$.
The claim is proved by induction on the sum of the lengths of the runs
$(n,t)\trans^*(\fin,u)$, and $(n',t')\trans'^*(\fin',u')$.
In the base case the sum is zero; then we have $((n,n'),(t,t'))=((\fin,\fin'),(u,u'))$ and we are done.

For the induction step,
suppose $(s,s')\in\Q$ and $((\init,\init'),(s,s'))\biTrans^*((n,n'),(t,t'))$.
Suppose $(n,t)\trans^*(\fin,u)$, and $(n',t')\trans'^*(\fin',u')$ where at least one of these has a non-zero number of steps.
Since $((n,n'),(t,t'))$ is reached from $\Q$, by manifest $\Q$-adequacy we have
$((n,n'),(t,t')) \in L \lor R \lor J$.  Here  $[\fin|\fin']$ can be excluded owing to the non-zero length unary computation.
So a step can be taken via $\biTrans$ from $((n,n'),(t,t'))$, via the LO, RO, or JO condition
in Def. <ref>, owing to liveness of $(L,R,J)$.  Consider the LO case.  The unary state $(n,t)$ must not be final, so there is $(m,r)$ with $(n,t)\trans(m,r)\trans^*(\fin,u)$.
The alignment automaton can go by LO to $((m,n'),(r,t'))$.
So we have
and traces $(m,r)\trans^*(\fin,u)$, $(n',t')\trans'^*(\fin',u')$
for which the induction hypothesis applies, yielding the result.
Cases RO and JO are similar.

Suppose $\aprod(A,A',L,R,J)\models \spec{\Q}{\S}$.
To prove $A,A'\models\rspec{\Q}{\S}$, consider any pair of terminated
traces of $A$ and $A'$ from
initial states $(\init,s)$ and $(\init',s')$ such that $(s,s')\in\Q$.
By adequacy and definition of the alignment automaton,
we can run $\aprod(A,A',L,R,J)$ from $((\init,\init'),(s,s'))$ and get a terminated trace
with the same final pair of stores.  Those stores satisfy $\S$,
by $\aprod(A,A',L,R,J)\models \spec{\Q}{\S}$.

Conversely, suppose $A,A'\models\rspec{\Q}{\S}$.
To prove $\aprod(A,A',L,R,J)\models \spec{\Q}{\S}$, consider any terminated trace of
$\aprod(A,A',L,R,J)$ from initial state
$((\init,\init'),(s,s'))$ with $(s,s')\in\Q$.
By definition of the alignment product, there are traces of $A$ and $A'$
which reach the same final stores.  Those stores satisfy $\S$,
by $A,A'\models\rspec{\Q}{\S}$.

To prove completeness, one sets $an(\init) = P$,
$an(\fin) = Q$,
and for all other control points $n$ set $an(n)$ to be the strongest invariant
of traces from $P$.

Immediate consequence of Prop. <ref> and Lemma <ref>.

This example shows that the alignment conditions of an alignment automaton
need not be exhaustive.
For brevity, write $sk^i$ for the assignment $\lassg{i}{y}{y}$ which acts like skip.

\[
\begin{array}{ll}
c: &
\lassg{1}{x}{x+1} ; \:
sk^2; \:
\lassg{3}{x}{x+1} ; \:
sk^4; \:
\lassg{5}{x}{x+1} \\
d: &
sk^1; \:
\lassg{2}{x}{x+1} ;
\lassg{3}{x}{x+1} ;
\lassg{4}{x}{x+1} ; \:
\end{array}
\]

Then we have

\[ \models c\sep d :\rspec{x=x'}{x=x'} \]

and it can be proved using this alignment of control point pairs,
where we use 6 as final label.

\[ (1,1), (1,2), (2,3), (3,3), (4,4), (5,4), (6,5), (6,6) \]

This is represented by an alignment automaton
$R\eqdef[1|1]\lor[6|5]$, and
$J\eqdef[1|2]\lor[3|3]\lor[5|4]$.  Note that $(L,R,J)$ is live.
The same automaton is obtained from
$R\eqdef[*|1]\lor[*|5]$, and the same $J$; again this is live.

Define $an(i,j)$ to be $x=x'$, for all $(i,j)$ in

\[ \{ (1,1), (1,2), (2,3), (3,3), (4,4), (5,4), (6,5), (6,6) \} \]

and $an(i,j)=\mathit{false}$ for all others.
The annotation is valid and the alignment automaton is manifestly

Note that $L\lor R\lor J\lor [\fin|\fin']$ does not include all states,
e.g., it excludes states with control $(3,2)$.
Note also that $L\lor R\lor J\lor [\fin|\fin']$ is $(x=x')$-invariant, i.e., holds in
all states reachable for an initial state satisfying the precondition $x=x'$.
If we drop $[2|3]$ from $L$ then $L\lor R\lor J\lor [\fin|\fin']$ is no longer invariant,
since it does not hold when control is at $(2,3)$; and the automaton is no longer adequate.

Let $States\eqdef ((Ctrl\times Ctrl')\times(Sto\times Sto'))$.
Let $L\eqdef States\setminus [\fin|*]$,
$R\eqdef States\setminus [*|\fin']$,
and $J\eqdef States\setminus [\fin|\fin']$.
These make the automaton  manifestly $true$-adequate and hence $\S$-adequate.
The subtractions ensures liveness of $L,R,J$ as required by Def. <ref>.
By Lemma <ref>
from $A,A'\models \rspec{\S}{\T}$ we have
$\aprod(A,A',L,R,J) \models \spec{\S}{\T}$.
So by completeness of IAM (Prop. <ref>) there is an annotation of
$\aprod(A,A',L,R,J)$ for $\spec{\S}{\T}$ that is valid.
$L\lor R\lor J \lor [\fin|\fin'] = States$,
which is implied by $\breve{an}(i,j)$ for any $i,j$.

We remark that the small step and automaton computations are similar but do not quite match
step-by-step.[In <cit.>,
using similar definitions,
the authors claim (Lemma 4) that the automaton steps correspond one-to-one with steps via $\ctrans$. This is not quite true, because
traces via $\ctrans$ include the steps of the form
$\config{\lskipc{n};c}{s} \ctrans \config{c}{s}$ where $n<0$.
There are no corresponding steps in the automaton, as the first example shows.
This does not undercut the other results in <cit.>,
which only depend on initial and final configurations of a program
versus its automaton.
For the command $\lassg{1}{x}{0};\lassg{2}{y}{0}$ we have (for some stores $s_0,s_1,s_2$)
the terminated computation

\[ \config{\lassg{1}{x}{0};\lassg{2}{y}{0}}{s_0}
\ctrans
\config{\lskipc{-1};\lassg{2}{y}{0}}{s_1}
\ctrans
\config{\lassg{2}{y}{0}}{s_1}
\ctrans
\config{\lskipc{-2}}{s_2}
\]

This corresponds to the following computation of

\[ (1,s_0)\trans(2,s_1)\trans(3,s_2) \]

As another example, we have

\[ \config{\lskipc{1};\lassg{2}{y}{0}}{t_0}
\ctrans
\config{\lassg{2}{y}{0}}{t_0}
\ctrans
\config{\lskipc{-2}}{t_1}
\]

and for $\aut((\lskipc{1};\lassg{2}{y}{0}),3)$ we have

\[ (1,t_0)\trans(2,t_0)\trans(3,t_1) \]

The state $(3,t_1)$ is terminated.
There is no transition from $(3,t_1)$ because none of the three
conditions in Def. <ref> holds,
noting that $\sub(3,(\lskipc{1};\lassg{2}{y}{0}))$
is not defined.

For any state $(n,s)$ where $n\neq f$, $n$ is the label of a command in $c$
and by definition of the small step relation $\ctrans$,
and the automaton transition $\trans$,
there at least one successor of $(n,s)$.
In the case where $n$ labels an if-command,
this relies on the $\totalIf$ condition (Def. <ref>).

The proof of the first equivalence uses Lemma <ref>
and also the fact that
$\config{c}{s}\ctrans^*\config{\lskipc{k}}{t}$ (for some $k$)
(noting the slight complication shown in Example <ref>).
The other equivalences follow by definitions from the first.

For reference we re-state the definition of $\hat{an}$.

\begin{equation}\label{eq:hatALT}
(m,s)\in\hat{an}(n) \quad\mbox{iff}\quad s\in an(n) \quad\mbox{for all $m,n,s$}
\end{equation}

Recall that we are treating assertions as sets of stores, but with formula notations.
So in Fig. <ref>, $an(n)\land e$ means $an(n)\intersect\means{e}$.
The entries in Fig. <ref> are obtained
from the condition (<ref>) on $\hat{an}$ by straightforward
unfolding of definitions —in particular, Def. <ref> of $\aut(c,f)$
and $\ctrans$ in Fig. <ref>.

Case $\lskipc{n}$ with $m = \fsuc(n,c,f)$.
To show: the VC is equivalent to $an(n)\imp an(m)$.

The VC of (<ref>) is

\[ \POST(\tranSeg{n,m})(\hat{an}(n)) \subseteq \hat{an}(m) \]

which equivales[Yes, it's a word, according to the Oxford English Dictionary.] using def $\POST$)

\[ \all{i,s,j,t}{ (i,s)\in\hat{an}(n) \land (i,s)\tranSeg{n,m}(j,t)
\; \imp \; (j,t)\in \hat{an}(m) } \]

which equivales (using def $\tranSeg{n,m}$ and one-point rule of predicate calculus)

\[ \all{s,t}{ (n,s)\in\hat{an}(n) \land (n,s)\trans(m,t)
\imp (m,t)\in \hat{an}(m) } \]

which equivales (using def (<ref>))

\[ \all{s,t}{ s\in an(n) \land (n,s)\trans(m,t) \imp t\in an(m) } \]

which equivales (using def $\trans$ for the case of skip with successor $m$)

\[ \all{s,t}{ s\in an(n) \land s = t \imp t\in an(m) } \]