* Floyd (1967) Robert W. Floyd. 1967\.  Assigning Meanings to Programs.  _Proceedings of Symposium in Applied Mathematics_ (1967), 19–32.
  * Francez (1983) Nissim Francez. 1983\.  Product properties and their direct verification.  _Acta informatica_ 20, 4 (1983), 329–344.
  * Gorogiannis et al. (2019) Nikos Gorogiannis, Peter W. O’Hearn, and Ilya Sergey. 2019\.  A True Positives Theorem for a Static Race Detector.  _Proc. ACM Program. Lang._ 3, POPL, Article 57 (jan 2019), 29 pages.  https://doi.org/10.1145/3290370
  * Gupta et al. (2008) Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko, and Ru-Gang Xu. 2008\.  Proving Non-Termination.  _SIGPLAN Not._ 43, 1 (jan 2008), 147–158.  https://doi.org/10.1145/1328897.1328459
  * Harel (1979) David Harel. 1979\.  _First-order dynamic logic_.  Springer.
  * Hoare (1969) C. A. R. Hoare. 1969\.  An Axiomatic Basis for Computer Programming.  _Commun. ACM_ 12, 10 (oct 1969), 576–580.  https://doi.org/10.1145/363235.363259
  * Hsu et al. (2021) Tzu-Han Hsu, César Sánchez, and Borzoo Bonakdarpour. 2021\.  Bounded Model Checking for Hyperproperties. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham, 94–112.
  * Kleymann (1999) Thomas Kleymann. 1999\.  Hoare Logic and Auxiliary Variables.  _Form. Asp. Comput._ 11, 5 (dec 1999), 541–566.  https://doi.org/10.1007/s001650050057
  * Le et al. (2022) Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022\.  Finding Real Bugs in Big Programs with Incorrectness Logic.  _Proc. ACM Program. Lang._ 6, OOPSLA1, Article 81 (apr 2022), 27 pages.  https://doi.org/10.1145/3527325
  * Leino (2008) K. Rustan M. Leino. 2008\.  This is Boogie 2. (June 2008).  https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/
  * Maillard et al. (2019) Kenji Maillard, Cătălin Hriţcu, Exequiel Rivas, and Antoine Van Muylder. 2019\.  The next 700 Relational Program Logics.  _Proc. ACM Program. Lang._ 4, POPL, Article 4 (dec 2019), 33 pages.  https://doi.org/10.1145/3371072
  * Maksimović et al. (2023) Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. 2023.  Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding. In _37th European Conference on Object-Oriented Programming (ECOOP 2023)_ , Vol. 263. 19:1–19:27.  https://doi.org/10.4230/LIPIcs.ECOOP.2023.19
  * McCullough (1987) Daryl McCullough. 1987\.  Specifications for multi-level security and a hook-up. In _1987 IEEE Symposium on Security and Privacy_. IEEE, 161–161.
  * McLean (1996) John McLean. 1996\.  A general theory of composition for a class of” possibilistic” properties.  _IEEE Transactions on Software Engineering_ 22, 1 (1996), 53–67.
  * Möller et al. (2021) Bernhard Möller, Peter O’Hearn, and Tony Hoare. 2021\.  On Algebra of Program Correctness and Incorrectness. In _Relational and Algebraic Methods in Computer Science_ , Uli Fahrenberg, Mai Gehrke, Luigi Santocanale, and Michael Winter (Eds.). Cham, 325–343.
  * Murray (2020) Toby Murray. 2020\.  An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation and More.  https://doi.org/10.48550/ARXIV.2003.04791
  * Naumann (2020) David A. Naumann. 2020\.  Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. In _Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles_ , Tiziana Margaria and Bernhard Steffen (Eds.). Cham, 93–116.
  * Nipkow et al. (2002) Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002\.  _Isabelle/HOL: A Proof Assistant for Higher-Order Logic_.  Springer-Verlag, Berlin, Heidelberg.
  * O’Hearn (2019) Peter W. O’Hearn. 2019\.  Incorrectness Logic.  _Proc. ACM Program. Lang._ 4, POPL, Article 10 (dec 2019), 32 pages.  https://doi.org/10.1145/3371078
  * Raad et al. (2020) Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020\.  Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In _Computer Aided Verification_. Cham, 225–252.
  * Raad et al. (2022) Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022.  Concurrent Incorrectness Separation Logic.  _Proc. ACM Program. Lang._ 6, POPL, Article 34 (jan 2022), 29 pages.  https://doi.org/10.1145/3498695
  * Ramshaw (1979) Lyle Harold Ramshaw. 1979\.  _Formalizing the Analysis of Algorithms_.  PhD thesis. Stanford University.
  * Rand and Zdancewic (2015) Robert Rand and Steve Zdancewic. 2015.  VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs.  _Electronic Notes in Theoretical Computer Science_ 319 (2015), 351–367.  https://doi.org/10.1016/j.entcs.2015.12.021 The 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).
  * Reynolds (2002) J.C. Reynolds. 2002\.  Separation logic: a logic for shared mutable data structures. In _Proceedings 17th Annual IEEE Symposium on Logic in Computer Science_. 55–74.  https://doi.org/10.1109/LICS.2002.1029817
  * Smith (2009) Geoffrey Smith. 2009\.  On the Foundations of Quantitative Information Flow. In _Foundations of Software Science and Computational Structures_ , Luca de Alfaro (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 288–302.
  * Sousa and Dillig (2016) Marcelo Sousa and Isil Dillig. 2016.  Cartesian Hoare Logic for Verifying K-Safety Properties. In _Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Santa Barbara, CA, USA) _(PLDI ’16)_. Association for Computing Machinery, New York, NY, USA, 57–69.  https://doi.org/10.1145/2908080.2908092
  * Unno et al. (2021) Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021\.  Constraint-Based Relational Verification. In _Computer Aided Verification_ , Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 742–766.
  * Volpano et al. (1996) Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996\.  A sound type system for secure flow analysis.  _Journal of computer security_ 4, 2-3 (1996), 167–187.
  * Yang (2007) Hongseok Yang. 2007\.  Relational separation logic.  _Theoretical Computer Science_ 375, 1 (2007), 308–334.  https://doi.org/10.1016/j.tcs.2006.12.036
  * Yasuoka and Terauchi (2010) Hirotoshi Yasuoka and Tachio Terauchi. 2010.  On Bounding Problems of Quantitative Information Flow. In _Computer Security – ESORICS 2010_ , Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 357–372.
  * Zilberstein et al. (2023) Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023\.  Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning.  https://www.cs.cornell.edu/~noamz/files/pubs/outcome.pdf

##  Appendix A Technical Definitions Omitted from the Paper

###### Definition 0.

Evaluation of syntactic hyper-expressions and satisfiability of hyper-
assertions.
Let $\Sigma$ a mapping from variables (such as $\varphi$) to states, and
$\Delta$ a mapping from variables (such as $x$) to values.121212In our
Isabelle formalization, these mappings are actually lists, since we use De
Bruijn indices (de Bruijn, 1972). The evaluation of hyper-expressions is
defined as follows:

$\displaystyle\llbracket c\rrbracket^{\Sigma}_{\Delta}\triangleq c$
$\displaystyle\llbracket y\rrbracket^{\Sigma}_{\Delta}\triangleq\Delta(y)$
$\displaystyle\llbracket\varphi^{P}(x)\rrbracket^{\Sigma}_{\Delta}\triangleq(\Sigma(\varphi))^{P}(x)$
$\displaystyle\llbracket\varphi^{L}(x)\rrbracket^{\Sigma}_{\Delta}\triangleq(\Sigma(\varphi))^{L}(x)$
$\displaystyle\llbracket e_{1}\oplus
e_{2}\rrbracket^{\Sigma}_{\Delta}\triangleq\llbracket
e_{1}\rrbracket^{\Sigma}_{\Delta}\oplus\llbracket
e_{2}\rrbracket^{\Sigma}_{\Delta}$ $\displaystyle\llbracket
f(e)\rrbracket^{\Sigma}_{\Delta}\triangleq f(\llbracket
e\rrbracket^{\Sigma}_{\Delta})$

Let $S$ be a set of states. The satisfiability of hyper-assertions is defined
as follows:

$\displaystyle S,\Sigma,\Delta\models b\triangleq b$ $\displaystyle
S,\Sigma,\Delta\models e_{1}\succeq e_{2}\triangleq\left(\llbracket
e_{1}\rrbracket^{\Sigma}_{\Delta}\succeq\llbracket
e_{2}\rrbracket^{\Sigma}_{\Delta}\right)$ $\displaystyle
S,\Sigma,\Delta\models A\land B\triangleq\left(S,\Sigma,\Delta\models A\land
S,\Sigma,\Delta\models B\right)$ $\displaystyle S,\Sigma,\Delta\models A\lor
B\triangleq\left(S,\Sigma,\Delta\models A\lor S,\Sigma,\Delta\models B\right)$
$\displaystyle S,\Sigma,\Delta\models\forall x\ldotp A\triangleq\left(\forall
v\ldotp S,\Sigma,\Delta[x\mapsto v]\models A\right)$ $\displaystyle
S,\Sigma,\Delta\models\exists x\ldotp A\triangleq\left(\exists v\ldotp
S,\Sigma,\Delta[x\mapsto v]\models A\right)$ $\displaystyle
S,\Sigma,\Delta\models\forall\varphi\ldotp
A\triangleq\left(\forall\alpha\ldotp
S,\Sigma[\varphi\mapsto\alpha],\Delta\models A\right)$ $\displaystyle
S,\Sigma,\Delta\models\exists\varphi\ldotp
A\triangleq\left(\exists\alpha\ldotp
S,\Sigma[\varphi\mapsto\alpha],\Delta\models A\right)$

When interpreting hyper-assertions in hyper-triples, we start with $\Delta$
and $\Sigma$ being the empty mappings, except when there is an explicit
quantifier around the triple, such as in the premises for the rule
While-$\exists$ from Fig. 6.

###### Definition 0.

Syntactic transformation for deterministic assignments.
$\mathcal{A}^{e}_{x}\left[A\right]$ yields the hyper-assertion $A$, where
$\varphi(x)$ is syntactically substituted by $e(\varphi)$, for all
(existentially or universally) quantified states $\varphi$:

$\displaystyle\mathcal{A}^{e}_{x}\left[b\right]\triangleq b$
$\displaystyle\mathcal{A}^{e}_{x}\left[e_{1}\succeq e_{2}\right]\triangleq
e_{1}\succeq e_{2}$ $\displaystyle\mathcal{A}^{e}_{x}\left[A\land
B\right]\triangleq\mathcal{A}^{e}_{x}\left[A\right]\land\mathcal{A}^{e}_{x}\left[B\right]$
$\displaystyle\mathcal{A}^{e}_{x}\left[A\lor
B\right]\triangleq\mathcal{A}^{e}_{x}\left[A\right]\lor\mathcal{A}^{e}_{x}\left[B\right]$
$\displaystyle\mathcal{A}^{e}_{x}\left[\forall x\ldotp
A\right]\triangleq\forall x\ldotp\mathcal{A}^{e}_{x}\left[A\right]$
$\displaystyle\mathcal{A}^{e}_{x}\left[\exists x\ldotp
A\right]\triangleq\exists x\ldotp\mathcal{A}^{e}_{x}\left[A\right]$
$\displaystyle\mathcal{A}^{e}_{x}\left[\forall\langle\varphi\rangle\ldotp
A\right]\triangleq\left(\forall\langle\varphi\rangle\ldotp\mathcal{A}^{e}_{x}\left[A[e(\varphi)/\varphi(x)]\right]\right)$
$\displaystyle\mathcal{A}^{e}_{x}\left[\exists\langle\varphi\rangle\ldotp
A\right]\triangleq\left(\exists\langle\varphi\rangle\ldotp\mathcal{A}^{e}_{x}\left[A[e(\varphi)/\varphi(x)]\right]\right)$

where $A[y/x]$ refers to the standard syntactic substitution of $x$ by $y$.

###### Definition 0.

Syntactic transformation for non-deterministic assignments.
$\mathcal{H}_{x}\left[A\right]$ yields the hyper-assertion $A$ where
$\varphi(x)$ is syntactically substituted by a fresh quantified variable $v$,
universally (resp. existentially) quantified for universally (resp.
existentially) quantified states:

$\displaystyle\mathcal{H}_{x}\left[b\right]\triangleq b$
$\displaystyle\mathcal{H}_{x}\left[e_{1}\succeq e_{2}\right]\triangleq
e_{1}\succeq e_{2}$ $\displaystyle\mathcal{H}_{x}\left[A\land
B\right]\triangleq\mathcal{H}_{x}\left[A\right]\land\mathcal{H}_{x}\left[B\right]$
$\displaystyle\mathcal{H}_{x}\left[A\lor
B\right]\triangleq\mathcal{H}_{x}\left[A\right]\lor\mathcal{H}_{x}\left[B\right]$
$\displaystyle\mathcal{H}_{x}\left[\forall x\ldotp A\right]\triangleq\forall
x\ldotp\mathcal{H}_{x}\left[A\right]$
$\displaystyle\mathcal{H}_{x}\left[\exists x\ldotp A\right]\triangleq\exists
x\ldotp\mathcal{H}_{x}\left[A\right]$
$\displaystyle\mathcal{H}_{x}\left[\forall\langle\varphi\rangle\ldotp
A\right]\triangleq\left(\forall\langle\varphi\rangle\ldotp\forall
v\ldotp\mathcal{H}_{x}\left[A[v/\varphi(x)]\right]\right)$
$\displaystyle\mathcal{H}_{x}\left[\exists\langle\varphi\rangle\ldotp
A\right]\triangleq\left(\exists\langle\varphi\rangle\ldotp\exists
v\ldotp\mathcal{H}_{x}\left[A[v/\varphi(x)]\right]\right)$

###### Definition 0.

Syntactic transformation for assume statements.

$\displaystyle\mathit{\Pi}_{p}\left[b\right]\triangleq b$
$\displaystyle\mathit{\Pi}_{p}\left[e_{1}\succeq e_{2}\right]\triangleq
e_{1}\succeq e_{2}$ $\displaystyle\mathit{\Pi}_{p}\left[A\land
B\right]\triangleq\mathit{\Pi}_{p}\left[A\right]\land\mathit{\Pi}_{p}\left[B\right]$
$\displaystyle\mathit{\Pi}_{p}\left[A\lor
B\right]\triangleq\mathit{\Pi}_{p}\left[A\right]\lor\mathit{\Pi}_{p}\left[B\right]$
$\displaystyle\mathit{\Pi}_{p}\left[\forall x\ldotp A\right]\triangleq\forall
x\ldotp\mathit{\Pi}_{p}\left[A\right]$
$\displaystyle\mathit{\Pi}_{p}\left[\exists x\ldotp A\right]\triangleq\exists
x\ldotp\mathit{\Pi}_{p}\left[A\right]$
$\displaystyle\mathit{\Pi}_{p}\left[\forall\langle\varphi\rangle\ldotp
A\right]\triangleq\forall\langle\varphi\rangle\ldotp
p(\varphi)\Rightarrow\mathit{\Pi}_{p}\left[A\right]$
$\displaystyle\mathit{\Pi}_{p}\left[\exists\langle\varphi\rangle\ldotp
A\right]\triangleq\exists\langle\varphi\rangle\ldotp
p(\varphi)\land\mathit{\Pi}_{p}\left[A\right]$

##  Appendix B Example of a Program Hyperproperty Relating an Unbounded Number
of Executions

Given a program with a low-sensitivity (_low_ for short) input $l$, a high-
sensitivity (_high for short_) input $h$, and output $o$, an interesting
problem is to _quantify_ how much information about $h$ is leaked through $o$.
This information flow can be quantified with _min-capacity_ (Assaf et al.,
2017; Smith, 2009), which boils down to quantifying the number of different
values that the output $o$ can have, given that the initial value of $l$ is
fixed (but the initial value of $h$ is not). The problem (1) of _upper-
bounding_ the number of possible values of $o$ is hypersafety, but not
$k$-safety for any $k>0$ (Yasuoka and Terauchi, 2010). This problem requires
the ability to reason about an _unbounded_ number of executions, which is not
possible in any existing Hoare logic, but is possible in Hyper Hoare Logic.
The harder problem (2) of both _lower-bounding_ (to show that there is some
leakage) and upper-bounding this quantity is not hypersafety anymore, and thus
requires to be able to reason directly about properties of sets, in this case
cardinality.

$\displaystyle\mathit{o}\coloneqq\mathit{0}\mathbf{;}\;$
$\displaystyle\mathit{i}\coloneqq\mathit{0}\mathbf{;}\;$
$\displaystyle\mathbf{while}\;(i<\mathit{max}(l,h))\;\\{$
$\displaystyle\quad\mathit{r}\coloneqq{}\mathit{nonDet()}\mathbf{;}\;$
$\displaystyle\quad\mathbf{assume}\;\mathit{0\leq r\leq 1}\mathbf{;}\;$
$\displaystyle\quad\mathit{o}\coloneqq\mathit{o+r}$
$\displaystyle\quad\mathit{i}\coloneqq\mathit{i+1}$ $\displaystyle\\}$ Figure
10. The program $C_{l}$ that leaks information about the high input $h$ via
its output $o$.

As an example, consider the program $C_{l}$ shown in Fig. 10. Assuming that we
know $h\geq 0$, the output $o$ of this program can be at most $h$. Hence, $o$
leaks information about $h$: We learn that $h\geq o$. With respect to problem
(1), we can express that this program can have _at most_ $v+1$ output values,
where $v$ is the initial value of $l$, with the hyper-triple

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(h\geq
0)\land\mathit{low}(l)\\}}}\;C_{l}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp\exists v\ldotp(\forall\varphi\in
S\ldotp\varphi(l)=v)\land|\\{\varphi(o)\mid\varphi\in S\\}|\leq v+1\\}}}$

Moreover, with respect to the harder problem (2), we can express that this
program can have _exactly_ $v+1$ output values, with the hyper-triple

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(h\geq
0)\land\mathit{low}(l)\\}}}\;C_{l}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp\exists v\ldotp(\forall\varphi\in
S\ldotp\varphi(l)=v)\land|\\{\varphi(o)\mid\varphi\in S\\}|=v+1\\}}}$

##  Appendix C Expressing Judgments of Hoare Logics as Hyper-Triples

In this section, we demonstrate the expressivity of the logic by showing that
hyper-triples can express the judgments of existing over- and
underapproximating Hoare logics (App. C.1 and App. C.2) and enable reasoning
about useful properties that go beyond over- and underapproximation (App.
C.3). All theorems and propositions in this section have been proved in
Isabelle/HOL.

###  C.1. Overapproximate Hoare Logics

The vast majority of existing Hoare logics prove the absence of bad
(combinations of) program executions. To achieve that, they prove properties
_for all_ (combinations of) executions, that is, they overapproximate the set
of possible (combinations of) executions. In this subsection, we discuss
overapproximate logics that prove properties of single executions or of $k$
executions (for a fixed number $k$), and show that Hyper Hoare Logic goes
beyond them by also supporting properties of unboundedly or infinitely many
executions.

##### Single executions

Classical Hoare Logic (Hoare, 1969) is an overapproximate logic for properties
of single executions (trace properties). The meaning of triples can be defined
as follows:

###### Definition 0.

Hoare Logic (HL). Let $P$ and $Q$ be sets of extended states. Then

$\displaystyle\models_{\mathit{HL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq(\forall\varphi\in
P\ldotp\forall\sigma^{\prime}\ldotp\langle
C,\varphi^{P}\rangle\rightarrow\sigma^{\prime}\Rightarrow(\varphi^{L},\sigma^{\prime})\in
Q)$

This definition reflects the standard partial-correctness meaning of Hoare
triples: executing $C$ in some initial state that satisfies $P$ can only lead
to a final state that satisfies $Q$. This meaning can be expressed as a
program hyperproperty as defined in Def. 12:

###### Proposition 0.

HL triples express hyperproperties. Given sets of extended states $P$ and $Q$,
there exists a hyperproperty $\mathcal{H}$ such that, for all commands $C$,
$C\in\mathcal{H}$ iff
$\models_{\mathit{HL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\mathcal{H}\triangleq\\{C\mid\forall\varphi\in
P\ldotp\forall\sigma^{\prime}\ldotp(\varphi^{P},\sigma^{\prime})\in\Sigma(C)\Rightarrow(\varphi^{L},\sigma^{\prime})\in
Q\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{HL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

This proposition together with completeness of our logic implies the
_existence_ of a proof in Hyper Hoare Logic for every valid classical Hoare
triple. But there is an even stronger connection: we can map any assertion in
classical Hoare logic to a hyper-assertion in Hyper Hoare Logic, which
suggests a direct translation from classical Hoare logic to our Hyper Hoare
Logic.

The assertions $P$ and $Q$ of a valid Hoare triple characterize _all_ initial
and _all_ final states of executing a command $C$. Consequently, they
represent _upper bounds_ on the possible initial and final states. We can use
this observation to map classical Hoare triples to hyper-triples by
interpreting their pre- and postconditions as upper bounds on sets of states.

###### Proposition 0.

Expressing HL in Hyper Hoare Logic. Let $\overline{P}\triangleq(\lambda
S\ldotp S\subseteq P)$.
Then
$\models_{\mathit{HL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
iff
$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\overline{P}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\overline{Q}\\}}}$.

Equivalently,
$\models_{\mathit{HL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
iff
$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi\rangle\ldotp\varphi\in
P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi\rangle\ldotp\varphi\in
Q\\}}}$.

This proposition implies that some rules of Hyper Hoare Logic have a direct
correspondence in HL. For example, the rule Seq instantiated with
$\overline{P}$, $\overline{R}$, and $\overline{Q}$ directly corresponds to the
sequential composition rule from HL. Moreover, the upper-bound operator
distributes over $\otimes$ and $\bigotimes$, since
$\overline{A}\otimes\overline{B}=\overline{A\cup B}$, and
$\bigotimes_{i}\overline{F_{i}}=\overline{\bigcup_{i}F(i)}$. Consequently, we
can for example easily derive in Hyper Hoare Logic the classic while-rule from
HL, using the rule Iter from Fig. 3.

#####  $k$ executions

Many extensions of HL have been proposed to deal with hyperproperties of $k$
executions. As a representative of this class of logics, we relate Cartesian
Hoare Logic (Sousa and Dillig, 2016) to our Hyper Hoare Logic. To define the
meaning of Cartesian Hoare Logic triples, we first lift our semantic relation
$\rightarrow$ from one execution on states to $k$ executions on extended
states. Let $k\in\mathbb{N^{+}}$. We write $\vv{\vphantom{d}\varphi}$ to
represent the $k$-tuple of extended states ($\varphi_{1},\ldots,\varphi_{k})$,
and $\forall\vv{\vphantom{d}\varphi}$ (resp.
$\exists\vv{\vphantom{d}\varphi}$) as a shorthand for
$\forall\varphi_{1},\ldots,\varphi_{k}$ (resp.
$\exists\varphi_{1},\ldots,\varphi_{k}$). Moreover, we define the relation
$\overset{k}{\rightarrow}$ as $\langle
C,\vv{\vphantom{d}\varphi}\rangle\overset{k}{\rightarrow}\vv{\vphantom{d}\varphi^{\prime}}\triangleq(\forall
i\in[1,k]\ldotp\langle
C,{\varphi_{i}}^{P}\rangle\rightarrow{\varphi^{\prime}_{i}}^{P}\;\land\;{\varphi_{i}}^{L}={\varphi^{\prime}_{i}}^{L})$.

###### Definition 0.

Cartesian Hoare Logic (CHL). Let $k\in\mathbb{N^{+}}$, and let $P$ and $Q$ be
sets of $k$-tuples of extended states. Then

$\displaystyle\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq$
$\displaystyle(\forall\vv{\vphantom{d}\varphi}\in
P\ldotp\forall\vv{\vphantom{d}\varphi^{\prime}}\ldotp\langle
C,\vv{\vphantom{d}\varphi}\rangle\overset{k}{\rightarrow}\vv{\vphantom{d}\varphi^{\prime}}\Rightarrow\vv{\vphantom{d}\varphi^{\prime}}\in
Q)$

$\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
is valid iff executing $C$ $k$ times in $k$ initial states that _together_
satisfy $P$ can only lead to $k$ final states that together satisfy $Q$. This
meaning can be expressed as a program hyperproperty:

###### Proposition 0.

CHL triples express hyperproperties. Given sets of $k$-tuples of extended
states $P$ and $Q$, there exists a hyperproperty $\mathcal{H}$ such that, for
all commands $C$,
$C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\displaystyle\mathcal{H}\triangleq\\{C\mid\forall\vv{\vphantom{d}\varphi}\in
P\ldotp\forall\vv{\vphantom{d}\varphi^{\prime}}\ldotp(\forall
i\in[1,k]\ldotp\varphi^{L}_{i}={\varphi^{\prime}}^{L}_{i}\land(\varphi_{i}^{P},{\varphi^{\prime}}_{i}^{P})\in\Sigma(C))\Rightarrow\vv{\vphantom{d}\varphi^{\prime}}\in
Q\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

Like we did for Hoare Logic, we can provide a direct translation from CHL
triples to hyper-triples in our logic. Similarly to HL, CHL assertions express
upper bounds, here on sets of $k$-tuples. However, simply using upper bounds
as in Prop. 3 does not capture the full expressiveness of CHL because
executions in CHL are _distinguishable_. For example, one can express
monotonicity from $x$ to $y$ as
$\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{x(1)\geq
x(2)\\}}}\;\mathit{y}\coloneqq\mathit{x}\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{y(1)\geq
y(2)\\}}}$. When going from (ordered) tuples of states in CHL to (unordered)
sets of states in Hyper Hoare Logic, we need to identify which state in the
set of final states corresponds to execution $1$, and which state corresponds
to execution $2$. As we did in App. D.2 to express monotonicity, we use a
logical variable $t$ to tag a state with the number $i$ of the execution it
corresponds to.

###### Proposition 0.

Expressing CHL in Hyper Hoare Logic. Let

$\displaystyle
P^{\prime}\triangleq(\forall\vv{\vphantom{d}\varphi}\ldotp(\forall
i\in[1,k]\ldotp\langle\varphi_{i}\rangle\land{\varphi}_{i}^{L}(t)=i)\Rightarrow\vv{\vphantom{d}\varphi}\in
P)$ $\displaystyle
Q^{\prime}\triangleq(\forall\vv{\vphantom{d}\varphi}\ldotp(\forall
i\in[1,k]\ldotp\langle\varphi_{i}\rangle\land{\varphi}_{i}^{L}(t)=i)\Rightarrow\vv{\vphantom{d}\varphi}\in
Q)$

where $t$ does not occur free in $P$ or $Q$. Then
$\models_{\mathit{CHL(k)}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\;\Longleftrightarrow\;\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$.

Recall that $\langle\varphi\rangle$ is equivalent to $\lambda
S\ldotp\varphi\in S$. As an example, we can express the CHL assertion
$y(1)\geq y(2)$ as the hyper-assertion
$\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}^{L}(t)=1\land\varphi_{2}^{L}(t)=2\Rightarrow\varphi_{1}^{P}(y)\geq\varphi_{2}^{P}(y)$.
Such translations provide a direct way of representing CHL proofs in Hyper
Hoare Logic.

CHL, like Hyper Hoare Logic, can reason about multiple executions of a single
command $C$, which is sufficient for many practically-relevant hyperproperties
such as non-interference or determinism. Other logics, such as Relational
Hoare Logic (Benton, 2004), relate the executions of multiple (potentially
different) commands, for instance, to prove program equivalence. In case these
commands are all the same, triples of relational logics can be translated to
Hyper Hoare Logic analogously to CHL. We explain how to encode relational
properties relating different commands to Hyper Hoare Logic in App. C.3.

##### Unboundedly many executions

To the best of our knowledge, all existing overapproximate Hoare logics
consider a fixed number $k$ of executions. In contrast, Hyper Hoare Logic can
reason about an unbounded number of executions, as illustrated in App. B.
Moreover, since our hyper-assertions are functions of potentially-infinite
sets of states, Hyper Hoare Logic can even express properties of infinitely-
many executions, as we illustrate in App. C.3.

###  C.2. Underapproximate Hoare Logics

Several recent Hoare logics allow proving the _existence_ of certain
(combinations of) program executions, which is useful, for instance, to
disprove a specification, that is, to demonstrate that a program definitely
has a bug. These logics underapproximate the set of possible (combinations of)
executions. In this subsection, we discuss two forms of underapproximate
logics, _backward_ and _forward_ , and show that both can be expressed in
Hyper Hoare Logic.

##### Backward underapproximation

Reverse Hoare Logic (de Vries and Koutavas, 2011) and Incorrectness Logic
(O’Hearn, 2019) are both underapproximate logics. Reverse Hoare Logic is
designed to reason about the reachability of good final states. Incorrectness
Logic uses the same ideas to prove the presence of bugs in programs. We focus
on Incorrectness Logic in the following, but our results also apply to Reverse
Hoare Logic. Incorrectness Logic reasons about single program executions:

###### Definition 0.

Incorrectness Logic (IL). Let $P$ and $Q$ be sets of extended states. Then

$\models_{\mathit{IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq(\forall\varphi\in
Q\ldotp\exists\sigma\ldotp(\varphi^{L},\sigma)\in P\land\langle
C,\sigma\rangle\rightarrow\varphi^{P})$

The meaning of IL triples is defined _backward_ from the postcondition: any
state that satisfies the postcondition $Q$ can be reached by executing $C$ in
an initial state that satisfies the precondition $P$. This meaning can be
expressed as a program hyperproperty:

###### Proposition 0.

IL triples express hyperproperties. Given sets of extended states $P$ and $Q$,
there exists a hyperproperty $\mathcal{H}$ such that, for all commands $C$,
$C\in\mathcal{H}$ iff
$\models_{\mathit{IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\mathcal{H}\triangleq\\{C\mid\forall\varphi\in
Q\ldotp\exists\sigma\ldotp(\varphi^{L},\sigma)\in
P\land(\sigma,\varphi^{P})\in\Sigma(C)\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

Hoare Logic shows the absence of executions by overapproximating the set of
possible executions, whereas Incorrectness Logic shows the existence of
executions by underapproximating it. This duality also leads to an analogous
translation of IL judgments into Hyper Hoare Logic, which uses lower bounds on
the set of executions instead of the upper bounds used in Prop. 3.

###### Proposition 0.

Expressing IL in Hyper Hoare Logic. Let $\underline{P}\triangleq(\lambda
S\ldotp P\subseteq S)$. Then
$\models_{\mathit{IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
iff
$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underline{P}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underline{Q}\\}}}$.

Equivalently,
$\models_{\mathit{IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
iff
$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\varphi\in
P\ldotp\langle\varphi\rangle\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\varphi\in
Q\ldotp\langle\varphi\rangle\\}}}$.

Analogous to the upper bounds for HL, the lower-bound operator distributes
over $\otimes$ and $\bigotimes$:
$\underline{A}\otimes\underline{B}=\underline{A\cup B}$ and
$\bigotimes_{i}\underline{F_{i}}=\underline{\bigcup_{i}F(i)}$. Using the
latter equality with the rules While and Cons, it is easy to derive the loop
rules from both Incorrectness Logic and Reverse Hoare Logic.

Murray (2020) has recently proposed an underapproximate logic based on IL that
can reason about two executions of two (potentially different) programs, for
instance, to prove that a program violates a hyperproperty such as non-
interference. We use the name _k-Incorrectness Logic_ for the restricted
version of this logic where the two programs are the same (and discuss
relational properties between different programs in App. C.3). The meaning of
triples in k-Incorrectness Logic is also defined backward. They express that,
for any pair of final states $(\varphi^{\prime}_{1},\varphi^{\prime}_{2})$
that together satisfy a relational postcondition, there exist two initial
states $\varphi_{1}$ and $\varphi_{2}$ that together satisfy the relational
precondition, and executing command $C$ in $\varphi_{1}$ (resp. $\varphi_{2}$)
leads to $\varphi^{\prime}_{1}$ (resp. $\varphi^{\prime}_{2}$). Our
formalization lifts this meaning from 2 to $k$ executions:

###### Definition 0.

k-Incorrectness Logic (k-IL). Let $k\in\mathbb{N^{+}}$, and $P$ and $Q$ be
sets of $k$-tuples of extended states. Then
$\models_{\mathit{k-IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq(\forall\vv{\vphantom{d}\varphi^{\prime}}\in
Q\ldotp\exists\vv{\vphantom{d}\varphi}\in P\ldotp\langle
C,\vv{\vphantom{d}\varphi}\rangle\overset{k}{\rightarrow}\vv{\vphantom{d}\varphi^{\prime}})$.

Again, this meaning is a hyperproperty:

###### Proposition 0.

k-IL triples express hyperproperties. Given sets of $k$-tuples of extended
states $P$ and $Q$, there exists a hyperproperty $\mathcal{H}$ such that, for
all commands $C$,
$C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\displaystyle\mathcal{H}\triangleq\\{C\mid\forall\vv{\vphantom{d}\varphi^{\prime}}\in
Q\ldotp\exists\vv{\vphantom{d}\varphi^{\prime}}\in P\ldotp(\forall
i\in[1,k]\ldotp\varphi_{i}^{L}={\varphi^{\prime}}_{i}^{L}\land(\varphi_{i}^{P},{\varphi^{\prime}}_{i}^{P})\in\Sigma(C))\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

Together with Thm. 13, this implies that we can express any k-IL triple as
hyper-triple in Hyper Hoare Logic. However, defining a direct translation of
k-IL triples to hyper-triples is surprisingly tricky. In particular, it is
_not_ sufficient to apply the transformation from Prop. 6, which uses a
logical variable $t$ to tag each state with the number of the execution it
belongs to. This approach works for Cartesian Hoare Logic because CHL and
Hyper Hoare Logic are both forward logics (see Def. 6 and Def. 4).
Intuitively, this commonality allows us to identify corresponding tuples from
the preconditions in the two logics and relate them to corresponding tuples in
the postconditions.

However, since k-IL is a _backward_ logic, the same approach is not sufficient
to identify corresponding tuples. For two states $\varphi^{\prime}_{1}$ and
$\varphi^{\prime}_{2}$ from the set of final states, we know through the tag
variable $t$ to which execution they belong, but not whether they originated
from one tuple $(\varphi_{1},\varphi_{2})\in P$, or from two _unrelated_
tuples.

To solve this problem, we use another logical variable $u$, which records the
“identity” of the initial $k$-tuple that satisfies $P$. To avoid cardinality
issues, we define the encoding under the assumption that $P$ depends only on
program variables. Consequently, there are at most $|\mathit{PStates}^{k}|$
such $k$-tuples, which we can represent as logical values if the cardinality
of $\mathit{LVals}$ is at least the cardinality of $\mathit{PStates}^{k}$, as
shown by the following result:

###### Proposition 0.

Expressing k-IL in Hyper Hoare Logic. Let $t,u$ be distinct variables in
$\mathit{LVars}{}$ and

$\displaystyle P^{\prime}\triangleq(\forall\vv{\vphantom{d}\varphi}\in
P\ldotp$ $\displaystyle(\forall
i\in[1,k]\ldotp{\varphi}_{i}^{L}(t)=i)\Rightarrow(\exists v\ldotp\forall
i\in[1,k]\ldotp\langle{\varphi}_{i}[u\mapsto v]\rangle))$ $\displaystyle
Q^{\prime}\triangleq(\forall\vv{\vphantom{d}\varphi^{\prime}}\in Q\ldotp$
$\displaystyle(\forall
i\in[1,k]\ldotp{\varphi^{\prime}}_{i}^{L}(t)=i)\Rightarrow(\exists
v\ldotp\forall i\in[1,k]\ldotp\langle{\varphi^{\prime}_{i}}[u\mapsto
v]\rangle))$

If (1) $P$ depends only on program variables, (2) the cardinality of
$\mathit{LVals}{}$ is at least the cardinality of $\mathit{PStates}{}^{k}$,
and (3) $t,u$ do not occur free in $P$ or $Q$, then
$\models_{\mathit{k-IL}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\;\Longleftrightarrow\;\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$.

This proposition provides a direct translation for some k-IL triples into
hyper-triples. Those that cannot be translated directly can still be verified
with Hyper Hoare Logic, according to Prop. 11.

##### Forward underapproximation

Underapproximate logics can also be formulated in a forward way: Executing
command $C$ in any state that satisfies the precondition reaches at least one
final state that satisfies the postcondition. Forward underapproximation has
recently been explored in Outcome Logic (Zilberstein et al., 2023), a Hoare
logic whose goal is to unify correctness (in the sense of classical Hoare
logic) and incorrectness reasoning (in the sense of forward
underapproximation) for single program executions. We focus on the
underapproximation aspect of Outcome Logic here; overapproximation can be
handled analogously to Hoare Logic (see App. C.1). Moreover, we restrict the
discussion to the programming language defined in Sect. 3.1; Outcome Logic
also supports heap-manipulating and probabilistic programs, which we do not
consider here.

Forward underapproximation for single executions can be formalized as follows:

###### Definition 0.

Forward Underapproximation (FU). Let $P$ and $Q$ be sets of extended states.
Then
$\models_{\mathit{FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq\left(\forall\varphi\in
P\ldotp\exists\sigma^{\prime}\ldotp\langle
C,\varphi^{P}\rangle\rightarrow\sigma^{\prime}\land(\varphi^{L},\sigma^{\prime})\in
Q\right)$

This meaning can be expressed in Hyper Hoare Logic as follows: If we execute
$C$ in a set of initial states that contains at least one state from $P$ then
the set of final states will contain at least one state in $Q$.

###### Proposition 0.

Expressing FU in Hyper Hoare Logic.

$\models_{\mathit{FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\;\Longleftrightarrow\;\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp P\cap
S\neq\varnothing\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp Q\cap S\neq\varnothing\\}}}$

Equivalently,
$\models_{\mathit{FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$
iff
$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi\in
P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi\in
Q\\}}}$.

The precondition (resp. postcondition) states that the intersection between
$S$ and $P$ (resp. $Q$) is non-empty. If instead it required that $S$ is a
_non-empty subset_ of $P$ (resp. $Q$), it would express the meaning of Outcome
Logic triples, i.e., the conjunction of classical Hoare Logic and forward
underapproximation.

While Outcome Logic reasons about single executions only, it is
straightforward to generalize forward underapproximation to multiple
executions:

###### Definition 0.

k-Forward Underapproximation (k-FU). Let $k\in\mathbb{N^{+}}$, and let $P$ and
$Q$ be sets of $k$-tuples of extended states. Then
$\models_{\mathit{k-FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq(\forall\vv{\vphantom{d}\varphi}\in
P\ldotp\exists\vv{\vphantom{d}\varphi^{\prime}}\in Q\ldotp\langle
C,\vv{\vphantom{d}\varphi}\rangle\overset{k}{\rightarrow}\vv{\vphantom{d}\varphi^{\prime}})$.

Again, this meaning can be expressed as a hyperproperty:

###### Proposition 0.

k-FU triples express hyperproperties. Given sets of $k$-tuples of extended
states $P$ and $Q$, there exists a hyperproperty $\mathcal{H}$ such that, for
all commands $C$,
$C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\displaystyle\mathcal{H}\triangleq\\{C\mid\forall\vv{\vphantom{d}\varphi}\in
P\ldotp\exists\vv{\vphantom{d}\varphi^{\prime}}\in Q\ldotp(\forall
i\in[1,k]\ldotp\varphi_{i}^{L}={\varphi^{\prime}}_{i}^{L}\land(\varphi_{i}^{P},{\varphi^{\prime}}_{i}^{P})\in\Sigma(C))\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

Since FU corresponds exactly to k-FU for $k=1$, this proposition applies also
to FU.

Because k-FU is _forward_ underapproximate, we can use the tagging from Prop.
6 to translate k-FU triples into hyper-triples. The following encoding
intuitively corresponds to the precondition $(S_{1}\times\ldots\times
S_{k})\cap P\neq\varnothing$ and the postcondition $(S_{1}\times\ldots\times
S_{k})\cap Q\neq\varnothing$, where $S_{i}$ corresponds to the set of states
with $t=i$:

###### Proposition 0.

Expressing k-FU in Hyper Hoare Logic.
Let $P^{\prime}\triangleq(\exists\vv{\vphantom{d}\varphi}\in P\ldotp\forall
i\in[1,k]\ldotp\langle{\varphi}_{i}\rangle\land{\varphi}_{i}^{L}(t)=i)$ and
$Q^{\prime}\triangleq(\exists\vv{\vphantom{d}\varphi^{\prime}}\in
Q\ldotp\forall
i\in[1,k]\ldotp\langle{\varphi^{\prime}_{i}}\rangle\land{\varphi^{\prime}_{i}}^{L}(t)=i)$.

If $t$ does not occur free in $P$ or $Q$, then
$\models_{\mathit{k-FU}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\;\Longleftrightarrow\;\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$.

###  C.3. Beyond Over- and Underapproximation

In the previous subsections, we have discussed overapproximate logics, which
reason about _all_ executions, and underapproximate logics, which reason about
the _existence_ of executions. In this subsection, we explore program
hyperproperties that combine universal and existential quantification, as well
as properties that apply other comprehensions to the set of executions. We
also discuss relational properties about multiple programs (such as program
equivalence).

#####  $\forall^{*}\exists^{*}$-hyperproperties

Generalized non-interference (see Sect. 2.3) intuitively expresses that for
each execution that produces a given observable output, there exists another
execution that produces the same output using any other secret. That is,
observing the output does not reveal any information about the secret. GNI is
a hyperproperty that cannot be expressed in existing over- or underapproximate
Hoare logics. It mandates the existence of an execution _based on other
possible executions_ , whereas underapproximate logics can show only the
existence of (combinations of) executions that satisfy some properties,
_independently of the other possible executions_. Generalized non-interference
belongs to a broader class of $\forall^{*}\exists^{*}$-hyperproperties.

RHLE (Dickerson et al., 2022) is a Hoare-style relational logic that has been
recently proposed to verify $\forall^{*}\exists^{*}$-relational properties,
such as program refinement (Abadi and Lamport, 1991). We call the special case
of RHLE where triples specify properties of multiple executions of the same
command _k-Universal Existential_ ; we can formalize its triples as follows:

###### Definition 0.

k-Universal Existential (k-UE). Let $k_{1},k_{2}\in\mathbb{N^{+}}$, and let
$P$ and $Q$ be sets of $(k_{1}+k_{2})$-tuples of extended states. Then

$\displaystyle\models_{\mathit{k-UE(k_{1},k_{2})}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\triangleq(\forall(\vv{\vphantom{d}\varphi},\vv{\vphantom{d}\gamma})\in
P\ldotp\forall\vv{\vphantom{d}\varphi^{\prime}}\ldotp\langle
C,\vv{\vphantom{d}\varphi}\rangle\overset{k_{1}}{\rightarrow}\vv{\vphantom{d}\varphi^{\prime}}\Rightarrow(\exists\vv{\vphantom{d}\gamma^{\prime}}\ldotp\langle
C,\vv{\vphantom{d}\gamma}\rangle\overset{k_{2}}{\rightarrow}\vv{\vphantom{d}\gamma^{\prime}}\land(\vv{\vphantom{d}\varphi^{\prime}},\vv{\vphantom{d}\gamma^{\prime}})\in
Q))$

Given $k_{1}+k_{2}$ initial states $\varphi_{1},\ldots,\varphi_{k_{1}}$ and
$\gamma_{1},\ldots,\gamma_{k_{2}}$ that together satisfy the precondition $P$,
for any final states $\varphi^{\prime}_{1},\ldots,\varphi^{\prime}_{k_{1}}$
that can be reached by executing $C$ in the initial states
$\varphi_{1},\ldots,\varphi_{k_{1}}$, there exist $k_{2}$ final states
$\gamma^{\prime}_{1},\ldots,\gamma^{\prime}_{k_{2}}$ that can be reached by
executing $C$ in the initial states $\gamma_{1},\ldots,\gamma_{k_{2}}$, such
that
$\varphi^{\prime}_{1},\ldots,\varphi^{\prime}_{k_{1}},\gamma^{\prime}_{1},\ldots,\gamma^{\prime}_{k_{2}}$
together satisfy the postcondition $Q$.

The properties expressed by k-UE assertions are hyperproperties:

###### Proposition 0.

k-UE triples express hyperproperties. Given sets of $(k_{1}+k_{2})$-tuples of
extended states $P$ and $Q$, there exists a hyperproperty $\mathcal{H}$ such
that, for all commands $C$,
$C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-UE(k_{1},k_{2})}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.

###### Proof sketch.

We define

$\displaystyle\mathcal{H}\triangleq\\{C\mid\forall(\vv{\vphantom{d}\varphi},\vv{\vphantom{d}\gamma})\in
P\ldotp\forall\vv{\vphantom{d}\varphi^{\prime}}\ldotp$
$\displaystyle\left(\forall
i\in[1,k_{1}]\ldotp(\varphi_{i}^{P},{\varphi^{\prime}}_{i}^{P})\in\Sigma(C)\land\varphi_{i}^{L}={\varphi^{\prime}}_{i}^{L}\right)$
$\displaystyle\Rightarrow\exists\vv{\vphantom{d}\gamma^{\prime}}\ldotp(\vv{\vphantom{d}\varphi^{\prime}},\vv{\vphantom{d}\gamma^{\prime}})\in
Q\land(\forall
i\in[1,k_{2}]\ldotp(\gamma_{i}^{P},{\gamma^{\prime}}_{i}^{P})\in\Sigma(C)\land\gamma_{i}^{L}={\gamma^{\prime}}_{i}^{L})\\}$

and prove $\forall C\ldotp
C\in\mathcal{H}\Longleftrightarrow\models_{\mathit{k-UE(k_{1},k_{2})}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}$.
∎

They can be directly expressed in Hyper Hoare Logic, as follows:

###### Proposition 0.

Expressing k-UE in Hyper Hoare Logic. Let $t,u$ be distinct variables in
$\mathit{LVars}{}$, and

$\displaystyle T_{n}$
$\displaystyle\triangleq(\lambda\vv{\vphantom{d}\varphi}\ldotp\forall
i\in[1,k_{n}]\ldotp\langle{\varphi}_{i}\rangle\land{\varphi}_{i}(t)=i\land{\varphi}_{i}(u)=n)$
$\displaystyle P^{\prime}$ $\displaystyle\triangleq(\forall
i\ldotp\exists\langle\varphi\rangle\ldotp\varphi^{L}(t)=i\land\varphi^{L}(u)=2)\land(\forall\vv{\vphantom{d}\varphi},\vv{\vphantom{d}\gamma}\ldotp
T_{1}(\vv{\vphantom{d}\varphi})\land
T_{2}(\vv{\vphantom{d}\gamma})\Rightarrow(\vv{\vphantom{d}\varphi},\vv{\vphantom{d}\gamma})\in
P)$ $\displaystyle Q^{\prime}$
$\displaystyle\triangleq(\forall\vv{\vphantom{d}\varphi^{\prime}}\ldotp
T_{1}(\varphi^{\prime})\Rightarrow(\exists\vv{\vphantom{d}\gamma^{\prime}}\ldotp
T_{2}(\vv{\vphantom{d}\gamma^{\prime}})\land(\vv{\vphantom{d}\varphi^{\prime}},\vv{\vphantom{d}\gamma^{\prime}})\in
Q))$

where $t,u$ do not occur free in $P$ or $Q$. Then
$\models_{\mathit{k-UE(k_{1},k_{2})}}{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{P\\}}}\;C\;{\color[rgb]{0.8,0.35,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.8,0.35,0.1}{\\{Q\\}}}\;\Longleftrightarrow\;\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$.

This proposition borrows ideas from the translations of other logics we saw
earlier. In particular, we use a logical variable $t$ to tag the executions,
and an additional logical variable $u$ that indicates whether a state is
universally ($u=1$) or existentially ($u=2$) quantified.

#####  $\exists^{*}\forall^{*}$-hyperproperties

To the best of our knowledge, no existing Hoare logic can express
$\exists^{*}\forall^{*}$-hyperproperties, i.e., the _existence_ of executions
in relation to _all_ other executions. As shown by the example in Sect. 4,
$\exists^{*}\forall^{*}$-hyperproperties naturally arise when disproving a
$\forall^{*}\exists^{*}$-hyperproperty (such as GNI), where the existential
part can be thought of as a counter-example, and the universal part as the
proof that this is indeed a counter-example. The existence of a minimum for a
function computed by a command $C$ is another simple example of an
$\exists^{*}\forall^{*}$-property, as illustrated in Sect. 5.3.

##### Properties using other comprehensions

Some interesting program hyperproperties cannot be expressed by quantifying
over states, but require other comprehensions over the set of states, such as
counting or summation. As an example, the hyperproperty “there are exactly $n$
different possible outputs for any given input” cannot be expressed by
quantifying over the states, but requires counting (see App. B). Other
examples of such hyperproperties include statistical properties about a
program:

###### Example 0.

Mean number of requests. Consider a command $C$ that, given some input $x$,
retrieves and returns information from a database. At the end of the execution
of $C$, variable $n$ contains the number of database requests that were
performed. If the input values are uniformly distributed (and with a suitable
precondition $P$), then the following hyper-triple expresses that the average
number of requests performed by $C$ is at most $2$:

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp\mathit{mean}_{n}^{x}(\\{\varphi^{P}\mid\varphi\in S\\})\leq 2\\}}}$

where $\mathit{mean}_{n}^{x}$ computes the average (using a suitable
definition for the average if the set is infinite) of the value of $n$.

To the best of our knowledge, Hyper Hoare Logic is the only Hoare logic that
can prove this property; existing logics neither support reasoning about mean-
comprehensions over multiple execution states nor reasoning about infinitely
many executions _at the same time_ (which is necessary if the domain of input
$x$ is infinite).

##### Relational program properties

Relational program properties typically relate executions of several
_different_ programs and, thus, do not correspond to program hyperproperties
as defined in Def. 12. However, it is possible to construct a single _product_
program (Barthe et al., 2011a, 2013) that encodes the executions of several
given programs, such that relational properties can be expressed as
hyperproperties of the constructed program and proved in Hyper Hoare Logic.

We illustrate this approach on program refinement (Abadi and Lamport, 1991). A
command $C_{2}$ _refines_ a command $C_{1}$ iff the set of pairs of pre- and
post-states of $C_{2}$ is a subset of the corresponding set of $C_{1}$.
Program refinement is a $\forall\exists$-property, where the $\forall$ and the
$\exists$ apply to different programs. To encode refinement, we construct a
new product program that non-deterministically executes either $C_{1}$ or
$C_{2}$, and we track in a logical variable $t$ which command was executed.
This encoding allows us to express and prove refinement in Hyper Hoare Logic:

###### Example 0.

Expressing program refinement in Hyper Hoare Logic.
Let
$C\triangleq(\mathit{t}\coloneqq\mathit{1}\mathbf{;}\;C_{1})+(\mathit{t}\coloneqq\mathit{2}\mathbf{;}\;C_{2})$.
If $t$ does not occur free in $C_{1}$ or $C_{2}$ then $C_{2}$ refines $C_{1}$
iff

$\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\top\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi\rangle\ldotp\varphi^{P}(t)=2\Rightarrow\langle(\varphi^{L},\varphi^{P}[t\coloneqq
1])\rangle\\}}}$

This example illustrates the general methodology to transform a relational
property over different programs into an equivalent hyperproperty for a new
product program, and thus to reason about relational program properties in
Hyper Hoare Logic. Relational logics typically provide rules that align and
relate parts of the different program executions; we present such a rule for
Hyper Hoare Logic in App. H.

This section demonstrated that Hyper Hoare Logic is sufficiently expressive to
prove and disprove arbitrary program hyperproperties as defined in Def. 12.
Thereby, it captures hyperproperties that are beyond the reach of existing
Hoare logics.

##  Appendix D Compositionality

The core rules of Hyper Hoare Logic allow one to prove any valid hyper-triple,
but not necessarily _compositionally_ , as explained in Sect. 3.6. As an
example, consider the sequential composition of a command $C_{1}$ that
satisfies _generalized_ non-interference (GNI) with a command $C_{2}$ that
satisfies non-interference (NI). We would like to prove that
$C_{1}\mathbf{;}\;C_{2}$ satisfies GNI (the weaker property). As discussed in
Sect. 2.3, a possible postcondition for $C_{1}$ is
$\mathit{GNI}_{l}^{h}\triangleq(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi^{P}(l)=\varphi_{2}^{P}(l))$,
while a possible precondition for $C_{2}$ is
$\mathit{low}(l)\triangleq(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(l)=\varphi_{2}(l))$.
The corresponding hyper-triples for $C_{1}$ and $C_{2}$ cannot be composed
using the core rules. In particular, rule Seq cannot be applied (even in
combination with Cons), since the postcondition of $C_{1}$ does not imply the
precondition of $C_{2}$. Note that this observation does _not_ contradict
completeness: By Thm. 10, it is possible to prove _more precise_ triples for
$C_{1}$ and $C_{2}$, such that the postcondition of $C_{1}$ matches the
precondition of $C_{2}$. However, to enable modular reasoning, our goal is to
construct the proof by composing the given triples for the individual commands
rather than deriving new ones.

In this section, we present _compositionality rules_ for hyper-triples (App.
D.1). These rules are _admissible_ in Hyper Hoare Logic, in the sense that
they do not modify the set of valid hyper-triples that can be proved. Rather,
these rules enable flexible compositions of hyper-triples (such as those
discussed above). We illustrate these rules on two examples (App. D.2):
Composing minimality with monotonicity, and GNI with NI. All technical results
presented in this section (soundness of the rules shown in Fig. 11 and
validity of the examples) have been formalized and proved in Isabelle/HOL.

###  D.1. Compositionality Rules

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\forall\varphi_{1},\varphi_{2}\ldotp\left(\varphi_{1}^{L}=\varphi_{2}^{L}\land\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\langle\varphi_{1}\rangle\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\langle\varphi_{2}\rangle\\}}}\Longrightarrow\;\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{\varphi_{1}}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{\varphi_{2}}\\}}}\right)$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=233.84923pt\hbox{\kern
3.00003pt${(\mathit{Linking})}$}}}\hbox{\kern
59.3756pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi\rangle\ldotp
P_{\varphi}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi\rangle\ldotp
Q_{\varphi}\\}}}$}}}\par\par}\\\\[20.00003pt] {tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\\}}}\quad\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{2}\\}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=137.24278pt\hbox{\kern
3.00003pt${(\mathit{And})}$}}}\hbox{\kern
17.26454pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\land
P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\land
Q_{2}\\}}}$}}}}\par\hskip 14.22636pt\par{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\\}}}\quad\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{2}\\}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=137.24278pt\hbox{\kern
3.00003pt${(\mathit{Or})}$}}}\hbox{\kern
17.26454pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\lor
P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\lor
Q_{2}\\}}}$}}}\par}\\\\[20.00003pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\quad\text{no
}\exists\langle\\_\rangle\text{ in
}F\quad\mathit{wr}(C)\cap\mathit{rd}(F)=\varnothing$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=214.63396pt\hbox{\kern
3.00003pt${(\mathit{FrameSafe})}$}}}\hbox{\kern
59.37581pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\land
F\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\land
F\\}}}$}}}\par}\\\\[20.00003pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 6.74643pt\hbox{$\displaystyle\penalty 1\forall
x\ldotp(\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{x}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{x}\\}}})$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=104.74164pt\hbox{\kern
3.00003pt${(\mathit{Forall})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall
x\ldotp
P_{x}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall
x\ldotp Q_{x}\\}}}$}}}}\par\hskip 14.22636pt\par{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
6.09961pt\hbox{$\displaystyle\penalty 1\forall
x\ldotp(\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{x}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{x}\\}}})$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=103.448pt\hbox{\kern
3.00003pt${(\mathit{IndexedUnion})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes\nolimits_{x\in
X}P_{x}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes\nolimits_{x\in
X}Q_{x}\\}}}$}}}\par}\\\\[20.00003pt] {tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\\}}}\quad\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{2}\\}}}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=137.24278pt\hbox{\kern
3.00003pt${(\mathit{Union})}$}}}\hbox{\kern
16.15343pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\otimes
P_{2}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{1}\otimes
Q_{2}\\}}}$}}}}\par\hskip 14.22636pt\par{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{\kern 9.16663pt\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=76.35463pt\hbox{\kern
3.00003pt${(\mathit{BigUnion})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes
P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes
Q\\}}}$}}}\par}\\\\[20.00003pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\quad\mathit{wr}(C)\cap\mathit{rd}(b)=\varnothing$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=143.56438pt\hbox{\kern
3.00003pt${(\mathit{Specialize})}$}}}\hbox{\kern
27.31258pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{b}\left[P\right]\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{b}\left[Q\right]\\}}}$}}}\par}\\\\[20.00003pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1P\Rightarrow^{V}P^{\prime}\quad\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\quad\mathit{inv}^{V}(Q)$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=147.53613pt\hbox{\kern
3.00003pt${(\mathit{LUpdate})}$}}}\hbox{\kern
44.75739pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}}\par}\\\\[20.00003pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\land(\forall\langle\varphi\rangle\ldotp\varphi(t)=e(\varphi))\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\quad
t\notin\mathit{rd}(P)\cup\mathit{rd}(Q)\cup\mathit{fv}(e)$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=264.67342pt\hbox{\kern
3.00003pt${(\mathit{LUpdateS})}$}}}\hbox{\kern
103.32602pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}}\par\par}\\\\[20.00003pt]
{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
10.55551pt\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=79.1324pt\hbox{\kern
3.00003pt${(\mathit{AtMost})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\sqsubseteq
P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\sqsubseteq
Q\\}}}$}}}}\hskip 14.22636pt\par{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 10.55551pt\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=79.1324pt\hbox{\kern
3.00003pt${(\mathit{AtLeast})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\sqsupseteq
P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\sqsupseteq
Q\\}}}$}}}\par}\\\\[20.00003pt] {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt
plus 0.0001fil\hbox{\kern 28.94681pt\hbox{$\displaystyle\penalty 1$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.89362pt\hbox{\kern
3.00003pt${(\mathit{True})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\top\\}}}$}}}}\hskip
14.22636pt\par{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.99507pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.99014pt\hbox{\kern
3.00003pt${(\mathit{False})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bot\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$}}}}\hskip
14.22636pt\par{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 39.48677pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=78.97354pt\hbox{\kern
3.00003pt${(\mathit{Empty})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{emp}{}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{emp}{}\\}}}$}}}\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par}\end{array}$
Figure 11. Compositionality rules of Hyper Hoare Logic. All these rules have
been proven sound in Isabelle/HOL. $\mathit{wr}(C)$ corresponds to the set of
program variables that are potentially written by $C$ (i.e., that appear on
the left-hand side of an assignment), while $\mathit{rd}(F)$ corresponds to
the set of program variables that appear in look-up expressions for quantified
states. For example, $\mathit{rd}(\forall\langle\varphi\rangle\ldotp\exists
n\ldotp\varphi^{P}(x)=n^{2})=\\{x\\}$. The operators $\bigotimes$,
$\sqsubseteq$, and $\sqsupseteq$ are defined as follows: $\bigotimes
P\triangleq\left(\lambda S\ldotp\exists F\ldotp(S=\bigcup_{S^{\prime}\in
F}S^{\prime})\land(\forall S^{\prime}\in F\ldotp P(S^{\prime}))\right)$,
$\sqsubseteq P\triangleq\left(\lambda S\ldotp\exists S^{\prime}\ldotp
S\subseteq S^{\prime}\land P(S^{\prime})\right)$, and $\sqsupseteq
P\triangleq\left(\lambda S\ldotp\exists S^{\prime}\ldotp S^{\prime}\subseteq
S\Rightarrow P(S^{\prime})\right)$.

Fig. 11 shows a (selection of) compositionality rules for Hyper Hoare Logic,
which we discuss below.

##### Linking

To prove hyper-triples of the form
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi_{1}\rangle\ldotp
P_{\varphi_{1}}\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi_{2}\rangle\ldotp
Q_{\varphi_{2}}\\}}}$, the rule Linking considers each pair of pre-state
$\varphi_{1}$ and post-state $\varphi_{2}$ separately, and lets one assume
that $\varphi_{2}$ can be reached by executing $C$ in the state $\varphi_{1}$,
and that logical variables do not change during this execution.

##### Conjunctions and disjunctions

Hyper Hoare Logic admits the usual rules for conjunction (And and Forall in
Fig. 11) and disjunction (Or in Fig. 11 and the core rule Exist in Fig. 3).

##### Framing

Similarly to the frame rules in Hoare logic and separation logic (Reynolds,
2002), Hyper Hoare Logic admits rules that allow us to frame information about
states that is not affected by the execution of $C$. The rule FrameSafe allows
us to frame any hyper-assertion $F$ if (1) it does not refer to variables that
the program can modify, and (2) it does not existentially quantify over
states. While (1) is standard, (2) is specific to hyper-assertions: Framing
the existence of a state (e.g., with
$F\triangleq\exists\langle\varphi\rangle\ldotp\top$) would be unsound if the
execution of the program in the state $\varphi$ does not terminate. We show in
App. E that restriction (2) can be lifted if $C$ terminates. We also show an
example of how this rule is used in App. F.

##### Decompositions

As explained at the beginning of this section, the two triples
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C_{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$
and
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$
cannot be composed because $\mathit{GNI}_{l}^{h}$ does not entail
$\mathit{low}(l)$ (not all states in the set $S$ of final states of $C_{1}$
need to have the same value for $l$). However, we can prove GNI for the
composed commands by decomposing $S$ into subsets that all satisfy
$\mathit{low}(l)$ and considering each subset separately. The rule BigUnion
allows us to perform this decomposition (formally expressed with the hyper-
assertion $\bigotimes\mathit{low}(l)$), use the specification of $C_{2}$ on
each of these subsets (since they all satisfy the precondition of $C_{2}$),
and eventually recompose the final set of states (again with the operator
$\bigotimes$) to prove our desired postcondition. Hyper Hoare Logic also
admits rules for binary unions (rule Union) and indexed unions (rule
IndexedUnion).

Note that unions ($\otimes$ and $\bigotimes$) and disjunctions in hyper-
assertions are very _different_ : $(P\otimes Q)(S)$ expresses that the set $S$
can be decomposed into two sets $S_{P}$ (satisfying $P$) and $S_{Q}$
(satisfying $Q$), while $(P\lor Q)(S)$ expresses that the entire set $S$
satisfies $P$ or $Q$. Similarly, intersections and conjunctions are very
different: While Hyper Hoare Logic admits conjunction rules, rules based on
intersections would be unsound, as shown by the following example:

###### Example 0.

Let $P_{1}\triangleq(\lambda S\ldotp\exists\varphi\ldotp
S=\\{\varphi\\}\land\varphi(x)=1)$, and $P_{2}\triangleq(\lambda
S\ldotp\exists\varphi\ldotp S=\\{\varphi\\}\land\varphi(x)=2)$. Both triples
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}\;\mathit{x}\coloneqq\mathit{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}$
and
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{2}\\}}}\;\mathit{x}\coloneqq\mathit{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{1}\\}}}$
are valid, but the triple

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp\exists S_{1},S_{2}\ldotp S=S_{1}\cap S_{2}\land P_{1}(S_{1})\land
P_{2}(S_{2})\\}}}\;\mathit{x}\coloneqq\mathit{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lambda
S\ldotp\exists S_{1},S_{2}\ldotp S=S_{1}\cap S_{2}\land P_{1}(S_{1})\land
P_{1}(S_{2})\\}}}$

is invalid, as the precondition is equivalent to $\mathit{emp}$, but the
postcondition is satisfiable by a non-empty set (with states satisfying
$x=1$).

##### Specializing hyper-triples

By definition, a hyper-triple can only be applied to a set of states that
satisfies its precondition, which can be restrictive. In cases where only a
_subset_ of the current set of states satisfies the precondition, one can
obtain a _specialized_ triple using the rule Specialize. This rule uses the
syntactic transformation $\mathit{\Pi}_{b}$ defined in Sect. 4.3 to weaken
both the precondition and the postcondition of the triple, which is sound as
long as the validity of $b$ is not influenced by executing $C$. Intuitively,
$\mathit{\Pi}_{b}\left[P\right]$ holds for a set $S$ iff $P$ holds for the
subset of states from $S$ that satisfy $b$. As an example, the triple
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(t{=}1{\Rightarrow}x{\geq}0){\land}\square(t{=}2{\Rightarrow}x{<}0)\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi_{1}\rangle{,}\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2{\Rightarrow}\varphi_{1}(y){\geq}\varphi_{2}(y)\\}}}$,
whose postcondition corresponds to $\mathit{mono}_{y}^{t}$, can be derived
from the two triples
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(x\geq
0)\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(y\geq
0)\\}}}$ and
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(x<0)\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\square(y<0)\\}}}$,
by applying the rule Specialize twice, using $b\triangleq(t{=}1)$ and
$b\triangleq(t{=}2)$ respectively, followed by the consequence rule.

##### Logical updates

Logical variables play an important role in the expressivity of the logic: As
we have informally shown in Sect. 2.2 and formally shown in App. C, relational
specifications are typically expressed in Hyper Hoare Logic by using logical
variables to formally link the pre-state of an execution with the
corresponding post-states. Since logical variables cannot be modified by the
execution, these tags are preserved.

To apply this proof strategy with existing triples, it is often necessary to
update logical variables to introduce such tags. The rule LUpdate allows us to
update the logical variables in a set $V$, provided that (1) from every set of
states $S$ that satisfies $P$, we can obtain a new set of states $S^{\prime}$
that satisfies $P^{\prime}$, by only updating (for each state) the logical
variables in $V$, (2) we can prove the triple with the updated set of initial
states, and (3) the postcondition $Q$ cannot distinguish between two sets of
states that are equivalent up to logical variables in $V$. We formalize this
intuition in the following:

###### Definition 0.

Logical updates. Let $V$ be a set of logical variable names. Two states
$\varphi_{1}$ and $\varphi_{2}$ are equal up to logical variables $V$, written
$\varphi_{1}\overset{V}{=}\varphi_{2}$, iff $\forall i\ldotp i\not\in
V\Rightarrow\varphi_{1}^{L}(i)=\varphi_{2}^{L}(i)$ and
$\varphi_{1}^{P}=\varphi_{2}^{P}$.

Two sets of states $S_{1}$ and $S_{2}$ are equivalent up to logical variables
$V$, written $S_{1}\overset{V}{=}S_{2}$, iff every state $\varphi_{1}\in
S_{1}$ has a corresponding state $\varphi_{2}\in S_{2}$ with the same values
for all variables except those in $V$, and vice-versa:

$(\forall\varphi_{1}\in S_{1}\ldotp\exists\varphi_{2}\in
S_{2}\ldotp\varphi_{1}\overset{V}{=}\varphi_{2})\land(\forall\varphi_{2}\in
S_{2}\ldotp\exists\varphi_{1}\in
S_{1}\ldotp\varphi_{1}\overset{V}{=}\varphi_{2})$

A hyper-assertion $P$ entails a hyper-assertion $P^{\prime}$ modulo logical
variables $V$, written $P\overset{V}{\Rightarrow}P^{\prime}$, iff

$\forall S\ldotp P(S)\Longrightarrow(\exists S^{\prime}\ldotp
P^{\prime}(S^{\prime})\land S\overset{V}{=}S^{\prime})$

Finally, a hyper-assertion $P$ is invariant with respect to logical updates in
$V$, written $\mathit{inv}^{V}(P)$, iff

$\forall S_{1},S_{2}\ldotp
S_{1}\overset{V}{=}S_{2}\Longrightarrow(P(S_{1})\Longleftrightarrow P(S_{2}))$

Note that $\mathit{inv}^{V}(Q)$ means that $Q$ cannot inspect the value of
logical variables in $V$, but it usually also implies that $Q$ cannot check
for _equality_ between states, and cannot inspect the cardinality of the set,
since updating logical variables might collapse two states that were
previously distinct (because of distinct values for logical variables in $V$).

Since this rule requires semantic reasoning, we also derive a weaker syntactic
version of this rule, LUpdateS, which is easier to use. The rule LUpdateS
allows us to strengthen a precondition $P$ to
$P\land(\forall\langle\varphi\rangle\ldotp\varphi(t)=e(\varphi))$, which
corresponds to updating the logical variable $t$ with the expression $e$, as
long as the logical variable $t$ does not appear _syntactically_ in $P$, $Q$,
and $e$ (and thus does not influence their validity). For example, to connect
the postcondition $\square(x=0\lor x=1)$ to the precondition
$\mathit{mono}_{x}^{t}=\left(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t)=1\land\varphi_{2}(t)=2\Rightarrow\varphi_{1}(x)\geq\varphi_{2}(x)\right)$
described in Sect. 2.2, one can use this rule to assign $1$ to $t$ if $x=1$,
and $2$ otherwise. App. F shows a detailed example.

###  D.2. Examples

We now illustrate our compositionality rules on two examples: Composing
minimality and monotonicity, and composing non-interference with generalized
non-interference.

####  D.2.1. Composing Minimality and Monotonicity

Consider a command $C_{1}$ that computes a function that has a minimum for
$x$, and a deterministic command $C_{2}$ that is monotonic from $x$ to $y$. We
want to prove _compositionally_ that $C_{1}\mathbf{;}\;C_{2}$ has a minimum
for $y$.

More precisely, we assume that $C_{1}$ satisfies the specification
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C_{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{x}\\}}}$,
where
$\mathit{hasMin}_{x}\triangleq(\exists\langle\varphi\rangle\ldotp\forall\langle\varphi^{\prime}\rangle\ldotp\varphi^{P}(x)\leq\varphi^{\prime
P}(x))$, and $C_{2}$ satisfies the two specifications
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{x}^{i}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{y}^{i}\\}}}$
(monotonicity) and
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}$
(determinism131313This triple ensures that $C_{2}$ does not map the initial
state with the minimum value for $x$ to potentially different states with
incomparable values for $y$ (the order $\leq$ on values might be partial).
Moreover, it ensures that $C_{2}$ does not drop any initial states because of
an assume command or a non-terminating loop.), where
$\mathit{mono}_{x}^{i}\triangleq(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}^{L}(i)=1\land\varphi_{2}^{L}(i)=2\Rightarrow\varphi_{1}^{P}(x)\leq\varphi_{2}^{P}(x))$,
and
$\mathit{isSingleton}\triangleq(\exists\langle\varphi\rangle\ldotp\forall\langle\varphi^{\prime}\rangle\ldotp\varphi=\varphi^{\prime})$.
With the core rules alone, we cannot compose the two triples to prove that
$C_{1}\mathbf{;}\;C_{2}$ has a minimum for $y$ since the postcondition of
$C_{1}$ does not imply the precondition of $C_{2}$.

(1) ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 3.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.49826pt\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=134.76035pt\hbox{\kern
2.10002pt${(\mathit{Specialize})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{i=1}\left[\mathit{isSingleton}{}\right]\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{i=1}\left[\mathit{isSingleton}{}\right]\\}}}$}}}}\hskip
3.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=193.90802pt\hbox{\kern
2.10002pt${(\mathit{FrameSafe})}$}}}\hbox{\kern
66.97054pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\mathit{\Pi}_{i=1}\left[\mathit{isSingleton}{}\right]\land(\forall\langle\varphi\rangle\ldotp\varphi^{L}(i)\in\\{1,2\\})}_{P^{\prime}}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\mathit{\Pi}_{i=1}\left[\mathit{isSingleton}{}\right]\land(\forall\langle\varphi\rangle\ldotp\varphi^{L}(i)\in\\{1,2\\})}_{Q^{\prime}}\\}}}$}}}}$

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C_{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{x}\\}}}\quad\hskip
3.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\mathit{hasMin}_{x}\overset{\\{i\\}}{\Rightarrow}\mathit{mono}_{x}^{i}\land
P^{\prime}\quad\hskip 3.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 3.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{x}^{i}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{y}^{i}\\}}}\quad\hskip
3.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 20.89328pt\hbox{$\displaystyle\penalty 1(1)$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=50.73102pt\hbox{\kern
2.10002pt${}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$}}}}\hskip
3.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=157.00648pt\hbox{\kern
2.10002pt${(\mathit{And})}$}}}\hbox{\kern
28.04181pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{x}^{i}\land
P^{\prime}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{y}^{i}\land
Q^{\prime}\\}}}$}}}}\hskip 3.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=199.43192pt\hbox{\kern
2.10002pt${(\mathit{Cons})}$}}}\hbox{\kern
52.83267pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{mono}_{x}^{i}\land
P^{\prime}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{y}\\}}}$}}}}\hskip
3.5pt plus 1.0fil\penalty
2\quad\mathit{inv}^{\\{i\\}}(\mathit{hasMin}_{y})$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=382.40723pt\hbox{\kern
2.10002pt${(\mathit{LUpdate})}$}}}\hbox{\kern
147.8647pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{x}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{y}\\}}}$}}}}\hskip
3.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=509.91707pt\hbox{\kern
2.10002pt${(\mathit{Seq})}$}}}\hbox{\kern
215.53036pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C_{1}\mathbf{;}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{y}\\}}}$}}}}$

Figure 12. A compositional proof that the sequential composition of a command
that has a minimum and a monotonic, deterministic command in turn has a
minimum. Recall that
$\mathit{isSingleton}\triangleq(\exists\langle\varphi\rangle\ldotp\forall\langle\varphi^{\prime}\rangle\ldotp\varphi=\varphi^{\prime})$,
and thus
$\mathit{\Pi}_{i=1}\left[\mathit{isSingleton}{}\right]=(\exists\langle\varphi\rangle\ldotp\varphi(i)=1\land(\forall\langle\varphi^{\prime}\rangle\ldotp\varphi^{\prime}(i)=1\Rightarrow\varphi=\varphi^{\prime}))$

Fig. 12 shows a valid derivation in Hyper Hoare Logic of
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C_{1}\mathbf{;}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{hasMin}_{y}\\}}}$
(which we have proved in Isabelle/HOL). The key idea is to use the rule
LUpdate to mark the minimal state with $i=1$, and all the other states with
$i=2$, in order to match $C_{1}$’s postcondition with $C_{2}$’s precondition.
Note that we _had to_ use the consequence rule to turn $C_{2}$’s postcondition
$\mathit{mono}_{y}^{i}\land Q^{\prime}$ into $\mathit{hasMin}_{y}$ _before_
applying the rule LUpdate, because the latter hyper-assertion is invariant
w.r.t. logical updates in $\\{i\\}$ (as required by the rule LUpdate), whereas
the former is not.

The upper part of Fig. 12 shows the derivation of
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}\\}}}$,
which uses Specialize to restrict the triple
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{isSingleton}{}\\}}}$
to the subset of states where $i=1$, ensuring the existence of a unique state
(the minimum) where $i=1$ after executing $C_{2}$. We also use the rule
FrameSafe to ensure that our set only contains states with $i=1$ or $i=2$.

####  D.2.2. Composing Non-Interference with Generalized Non-Interference

To illustrate additional compositionality rules, we re-visit the example
introduced at the beginning of this section. Consider a command $C_{1}$ that
satisfies GNI (for a public variable $l$ and a secret variable $h$) and a
command $C_{2}$ that satisfies NI (for the public variable $l$). We want to
prove that $C_{1}\mathbf{;}\;C_{2}$ satisfies GNI (for $l$ and $h$).

More precisely, we assume that $C_{1}$ satisfies the hyper-triple
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$,
where
$\mathit{GNI}_{l}^{h}\triangleq(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi^{P}(l)=\varphi_{2}^{P}(l))$.
Moreover, we assume that $C_{2}$ satisfies the triples
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}$,
where
$\mathit{low}(l)\triangleq(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}^{P}(l)=\varphi_{2}^{P}(l))$,
and
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lnot\mathit{emp}{}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lnot\mathit{emp}{}\\}}}$.
The second triple is needed to ensure that $C_{2}$ does not drop executions
depending on some values for $h$ (e.g., because of secret-dependent non-
termination), which might cause $C_{1}\mathbf{;}\;C_{2}$ to violate GNI.

(2) ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\quad\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.78642pt\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lnot\mathit{emp}{}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lnot\mathit{emp}{}\\}}}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=133.65854pt\hbox{\kern
2.40002pt${(\mathit{Specialize})}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{h=\varphi_{1}^{L}(h)}\left[\lnot\mathit{emp}{}\right]\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{\Pi}_{h=\varphi_{1}^{L}(h)}\left[\lnot\mathit{emp}{}\right]\\}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=201.25592pt\hbox{\kern
2.40002pt${(\mathit{Cons})}$}}}\hbox{\kern
11.04433pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h)\\}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=341.40565pt\hbox{\kern
2.40002pt${(\mathit{And})}$}}}\hbox{\kern
45.46358pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\land(\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h))\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\land(\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h))\\}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=389.89189pt\hbox{\kern
2.40002pt${(\mathit{BigUnion})}$}}}\hbox{\kern
57.48447pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes\left(\mathit{low}(l)\land(\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h))\right)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\bigotimes\left(\mathit{low}(l)\land(\exists\langle\varphi\rangle\ldotp\varphi^{L}(h)=\varphi_{1}^{L}(h))\right)\\}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=452.4893pt\hbox{\kern
2.40002pt${(\mathit{Cons})}$}}}\hbox{\kern
194.4778pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\forall\langle\varphi_{2}\rangle\ldotp\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi_{2}^{P}(l)=\varphi^{P}(l)}_{P^{\prime}_{\varphi_{1}}}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\forall\langle\varphi_{2}\rangle\ldotp\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi_{2}^{P}(l)=\varphi^{P}(l)}_{Q^{\prime}_{\varphi_{1}}}\\}}}$}}}}$

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{1}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}\quad\hskip
4.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
43.51808pt\hbox{$\displaystyle\penalty 1\text{using
}(\ref{eq:proving_linking})\text{ and }\varphi_{1}^{L}=\varphi_{1}^{\prime
L}\Longrightarrow
Q^{\prime}_{\varphi_{1}}=Q^{\prime}_{\varphi_{1}^{\prime}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=194.9181pt\hbox{\kern
2.40002pt${}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\forall\varphi_{1},\varphi_{1}^{\prime}\ldotp(\varphi_{1}^{L}=\varphi_{1}^{\prime
L}\land\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\langle\varphi_{1}\rangle\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\langle\varphi_{1}^{\prime}\rangle\\}}}\Longrightarrow(\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P^{\prime}_{\varphi_{1}}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q^{\prime}_{\varphi_{1}^{\prime}}\\}}})$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=222.29318pt\hbox{\kern
2.40002pt${(\mathit{Linking})}$}}}\hbox{\kern
74.51222pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$}}}}\hskip
4.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=367.66782pt\hbox{\kern
2.40002pt${(\mathit{Seq})}$}}}\hbox{\kern
138.73586pt\hbox{$\displaystyle\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{1}\mathbf{;}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$}}}}$

Figure 13. A compositional proof that the sequential composition of a command
that satisfies GNI and a command that satisfies NI in turn satisfies GNI.

Fig. 13 shows a valid derivation of the triple
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{1}\mathbf{;}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$
(which we have proved in Isabelle/HOL). The first key idea of this derivation
is to use the rule Linking to eliminate the $\forall\langle\varphi_{1}\rangle$
in the pre- and postcondition of the triple
${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{GNI}_{l}^{h}\\}}}$,
while assuming that they have the same value for the logical variable $h$
(implied by the assumption $\varphi_{1}^{L}=\varphi_{1}^{\prime L}$). The
second key idea is to decompose any set of states $S$ that satisfies
$P^{\prime}_{\varphi_{1}}$ (defined as
$\forall\langle\varphi_{2}\rangle\ldotp\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi_{2}^{P}(l)=\varphi^{P}(l)$)
into a union of smaller sets that all satisfy
$\mathit{low}(l)\land(\exists\langle\varphi\rangle\ldotp\varphi_{1}^{L}(h)=\varphi^{L}(h))$.
More precisely, we rewrite $S$ as the union of all sets
$\\{\varphi,\varphi_{2}\\}$ for all $\varphi,\varphi_{2}\in S$ such that
$\varphi_{1}^{L}(h)=\varphi^{L}(h)\land\varphi_{2}^{P}(l)=\varphi^{P}(l)$,
using the rule Cons. Unlike $S$, these smaller sets all satisfy the
precondition $\mathit{low}(l)$ of $C_{2}$, which allows us to leverage the
triple
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}\;C_{2}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\mathit{low}(l)\\}}}$.
Finally, we use the rule Specialize to prove that, after executing $C_{2}$ in
each of the smaller sets $\\{\varphi,\varphi_{2}\\}$, there will exist at
least one state $\varphi^{\prime}$ with $\varphi^{\prime
L}(h)=\varphi_{1}^{L}(h)$.

##  Appendix E Termination-Based Reasoning

###  E.1. Termination-Based Rules

In App. D, we have introduced the rule FrameSafe (Fig. 11), which is sound
only for hyper-assertions that do not contain any $\exists\langle\\_\rangle$,
because the program $C$ around which we want to frame some hyper-assertion
might not terminate. Moreover, in Sect. 5.1, we have introduced the
synchronized while rule WhileSync (Fig. 6). This rule contains an
$\mathit{emp}{}$ disjunct in the postcondition of the conclusion, which
prevents it from being useful to prove hyperproperties of the form
$\exists^{+}\forall^{*}$, i.e., with a top-level existential quantifier over
states. This $\mathit{emp}{}$ disjunct corresponds to the case where the loop
does not terminate.

In this section, we show that we can overcome those two limitations by
introducing _total_ hyper-triples, which are stronger than normal hyper-
triples, in that they also ensure the existence of at least one terminating
execution from any initial state:

###### Definition 0.

Total hyper-triples.

$\models_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\triangleq\left(\forall
S\ldotp P(S)\Rightarrow(Q(\mathit{sem}(C,S))\land(\forall\varphi\in
S\ldotp\exists\sigma^{\prime}\ldotp\langle
C,\varphi^{P}\rangle\rightarrow\sigma^{\prime}))\right)$

For any program statement $C$ that does not contain any $\mathbf{assume}$
statement, both triples are equivalent:
$\models_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\Longleftrightarrow\models{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}$.

Using total hyper-triples, we can now express and prove sound (which we have
done in Isabelle/HOL) the following rules, which solve the aforementioned
limitations:

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\mathit{wr}(C)\cap\mathit{fv}(F)=\varnothing\quad\vdash_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\\}}}\quad
F\text{ is a syntactic hyper-assertion}$}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=297.75076pt\hbox{\kern
3.00003pt${(\mathit{Frame})}$}}}\hbox{\kern
99.2231pt\hbox{$\displaystyle\vdash_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P\land
F\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q\land
F\\}}}$}}}}$ ${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vdash_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\land\square(b\land
e=t^{L})\\}}}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\land\mathit{low}(b)\land\square(e\prec
t^{L})\\}}}\quad\prec\text{well-founded}\quad
t^{L}\notin\mathit{rd}(I)$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=334.23853pt\hbox{\kern
3.00003pt${(\mathit{WhileSyncTot})}$}}}\hbox{\kern
76.38678pt\hbox{$\displaystyle\vdash_{\Downarrow}{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\land\mathit{low}(b)\\}}}\;\mathbf{while}\;(b)\;\\{C\\}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\land\square(\lnot
b)\\}}}$}}}}$

As can be seen, the rule Frame can be used for _any_ hyper-assertion expressed
in the syntax defined in Sect. 4.1. Unlike the rule WhileSync, the rule
WhileSyncTot does not have the $\mathit{emp}{}$ disjunct in the postcondition
of its conclusion anymore, and thus can be used to prove hyperproperties of
the form $\exists^{+}\forall^{*}$! It achieves this by requiring that (1) the
loop body $C$ terminates (in the sense of Def. 1), and (2) that the loop
itself terminates, by requiring that a variant $e$ decreases in all
executions. The initial value of the variant $e$ is stored in the logical
variable $t^{L}$, such that it can be referred to in the postcondition. Note
that we can prove a total variant of each loop rule presented in Sect. 5, by
doing something similar as point (2) here, in order to obtain a complete proof
system for total hyper-triples.

###  E.2. (Dis-)Proving Termination

Hyper Hoare Logic in its current version is a “partial correctness” logic, in
the sense that it proves (hyper)properties about the set of _terminating_
executions. By slightly strengthening the definition of total hyper-triples
(Def. 1) such that _all_ executions are required to terminate, we could obtain
a “total correctness” version of Hyper Hoare Logic, with which we can prove
that all considered executions terminate. Note that, even with this stronger
definition, the rules Frame and WhileSyncTot would stay the same.

Notably, HHL could also be extended to disprove termination. To prove _non_
-termination of a loop $\mathbf{while}\;(b)\;\\{C\\}$, one can express and
prove that a set of states $R$, in which all states satisfy the loop guard
$b$, is a _recurrent set_ (Gupta et al., 2008). $R$ is a recurrent set iff
executing $C$ in any state from $R$ leads to at least another state in $R$,
which can easily be expressed as a hyper-triple:

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi\in
R\\}}}\;\mathbf{assume}\;\mathit{b}\mathbf{;}\;C\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\varphi\in
R\\}}}$

Thus, if one state from $R$ reaches $\mathbf{while}\;(b)\;\\{C\\}$, we know
that there is at least one non-terminating execution.

Note that both extensions of Hyper Hoare Logic (to prove and disprove
termination) would require modifying the underlying semantic model of the
logic; in particular, the extended semantics in Def. 4 should be modified to
also capture non-terminating executions. We do not expect such a modification
to pose any significant challenge.

##  Appendix F Fibonacci Example

In this section, we show the proof that the program $C_{\mathit{fib}}$ from
Fig. 8 is monotonic. Precisely, we prove the triple

$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi_{1}\rangle{,}\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2{\Rightarrow}\varphi_{1}(n){\geq}\varphi_{2}(n)\\}}}\;C_{\mathit{fib}}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\forall\langle\varphi_{1}\rangle{,}\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2{\Rightarrow}\varphi_{1}(a){\geq}\varphi_{2}(a)\\}}}$

using the rule While-$\forall^{*}\exists^{*}$ with the loop invariant
$I\triangleq((\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}\varphi_{1}(i)\geq\varphi_{2}(n){-}\varphi_{2}(i)\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b)))\land\square(b\geq
a\geq 0))$.

$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi_{1}\rangle{,}\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2{\Rightarrow}\varphi_{1}(n){\geq}\varphi_{2}(n)\right\\}}}$
(Cons)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}0\geq\varphi_{2}(n){-}0\land
0\geq 0\land 1\geq 1))\land\square(1\geq a\geq 0)\right\\}}}$
$\displaystyle\mathit{a}\coloneqq\mathit{0}\mathbf{;}\;$ (AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}0\geq\varphi_{2}(n){-}0\land\varphi_{1}(a)\geq\varphi_{2}(a)\land
1\geq 1))\land\square(1\geq a\geq 0)\right\\}}}$
$\displaystyle\mathit{b}\coloneqq\mathit{1}\mathbf{;}\;$ (AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}0\geq\varphi_{2}(n){-}0\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b)))\land\square(b\geq
a\geq 0)\right\\}}}$ $\displaystyle\mathit{i}\coloneqq\mathit{0}\mathbf{;}\;$
(AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}\varphi_{1}(i)\geq\varphi_{2}(n){-}\varphi_{2}(i)\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b)))\land\square(b\geq
a\geq 0)\right\\}}}$ Figure 14. First part of the proof, which proves that the
loop invariant $I$ holds before the loop.
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}\varphi_{1}(i)\geq\varphi_{2}(n){-}\varphi_{2}(i)\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b))\land\square(b\geq
a\geq 0)\right\\}}}$ (LUpdateS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}\varphi_{1}(i)\geq\varphi_{2}(n){-}\varphi_{2}(i)\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b))\land\square(b\geq
a\geq 0)\land\square(v_{a}=a\land v_{b}=b\land v_{i}=i)\right\\}}}$
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{(\forall\langle\varphi\rangle\ldotp\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b}))}}$
(Cons)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\land\underbrace{(\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t)=1\land\varphi_{2}(t)=2\Rightarrow\varphi_{1}(v_{a})\geq\varphi_{2}(v_{a})\geq
0\land\varphi_{1}(v_{b})\geq\varphi_{2}(v_{b})\geq
0\land\varphi_{1}(n)-\varphi_{1}(v_{i})\geq\varphi_{2}(n)-\varphi_{2}(v_{i}))}_{F}\\}}}$
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})\right\\}}}$
$\displaystyle\quad\mathbf{if}\;(*)\;\\{$
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})\right\\}}}$
(Cons)
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(i)<\varphi(n)\Rightarrow\varphi(v_{i})<\varphi(n)\land\varphi(i)+1=\varphi(v_{i})+1\land\varphi(b)=\varphi(v_{b})\land\varphi(a)+\varphi(b)=\varphi(v_{a})+\varphi(v_{b})\right\\}}}$
$\displaystyle\quad\quad\mathbf{assume}\;\mathit{i<n}\mathbf{;}\;$ (AssumeS)
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(v_{i})<\varphi(n)\land\varphi(i)+1=\varphi(v_{i})+1\land\varphi(b)=\varphi(v_{b})\land\varphi(a)+\varphi(b)=\varphi(v_{a})+\varphi(v_{b})\right\\}}}$
$\displaystyle\quad\quad\mathit{tmp}\coloneqq\mathit{b}\mathbf{;}\;$
$\displaystyle\quad\quad\mathit{b}\coloneqq\mathit{a+b}\mathbf{;}\;$
$\displaystyle\quad\quad\mathit{a}\coloneqq\mathit{tmp}\mathbf{;}\;$
$\displaystyle\quad\quad\mathit{i}\coloneqq\mathit{i+1}$ (AssignS)
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\forall\langle\varphi\rangle\ldotp\varphi(v_{i})<\varphi(n)\land\varphi(i)=\varphi(v_{i})+1\land\varphi(a)=\varphi(v_{b})\land\varphi(b)=\varphi(v_{a})+\varphi(v_{b})}_{Q_{1}}\\}}}$
$\displaystyle\quad\\}$ $\displaystyle\quad\mathbf{else}\;\\{$
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})\right\\}}}$
(Cons)
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi\rangle\ldotp\varphi(i)\geq\varphi(n)\Rightarrow\varphi(v_{i})\geq\varphi(n)\land\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})\right\\}}}$
$\displaystyle\quad\quad\mathbf{assume}\;\mathit{\lnot(i<n)}$ (AssumeS)
$\displaystyle\quad\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\underbrace{\forall\langle\varphi\rangle\ldotp\varphi(v_{i})\geq\varphi(n)\land\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})}_{Q_{2}}\\}}}$
$\displaystyle\quad\\}$ (Choice)
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{Q_{1}\otimes
Q_{2}\right\\}}}$ (FrameSafe)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{(Q_{1}\otimes
Q_{2})\land F\right\\}}}$ (Cons)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\forall\langle\varphi_{1}\rangle,\langle\varphi_{2}\rangle\ldotp\varphi_{1}(t){=}1{\land}\varphi_{2}(t){=}2\Rightarrow(\varphi_{1}(n){-}\varphi_{1}(i)\geq\varphi_{2}(n){-}\varphi_{2}(i)\land\varphi_{1}(a)\geq\varphi_{2}(a)\land\varphi_{1}(b)\geq\varphi_{2}(b))\land\square(b\geq
a\geq 0)\right\\}}}$ Figure 15. Second part of the proof. This proof outline
shows
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\\}}}\;\mathbf{if}\;(i<n)\;\\{C_{body}\\}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\\}}}$,
the first premise of the rule While-$\forall^{*}\exists$, where $C_{body}$
refers to the body of the loop.

Fig. 14 shows the (trivial) first part of the proof, which proves that the
loop invariant $I$ holds before the loop, and Fig. 15 shows the proof of
$\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\\}}}\;\mathbf{if}\;(i<n)\;\\{C_{body}\\}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{I\\}}}$,
the fist premise of the rule While-$\forall^{*}\exists$ (the second premise is
trivial). In Fig. 15, we first record the initial values of $a$, $b$, and $i$
in the logical variables $v_{a}$, $v_{b}$, and $v_{i}$, respectively, using
the rule LUpdateS presented in App. D. We then split our new hyper-assertion
into a simple part,
$\forall\langle\varphi\rangle\ldotp\varphi(i)=\varphi(v_{i})\land\varphi(a)=\varphi(v_{a})\land\varphi(b)=\varphi(v_{b})$,
and a frame $F$ which stores the relevant information from the invariant $I$
with the initial values. The hyper-assertion $F$ is then framed around the if-
statement, using the rule FrameSafe from App. D. The proof of each branch is
straightforward; the postconditions of the two branches are combined via the
rule Choice.

We finally conclude with the consequence rule. This last entailment is
justified by a case distinction. Let $\varphi_{1}$, $\varphi_{2}$ be two
states such that $\varphi_{1}(t)=1$, $\varphi_{2}(t)=2$, and
$\langle\varphi_{1}\rangle$ and $\langle\varphi_{2}\rangle$ hold. From the
frame $F$, we know that $\varphi_{1}(v_{a})\geq\varphi_{2}(v_{a})$, and
$\varphi_{1}(v_{b})\geq\varphi_{2}(v_{b})$. We conclude the proof by
distinguishing the following three cases (the proof for each case is
straightforward): (1) Both $\varphi_{1}$ and $\varphi_{2}$ took the first
branch of the if statement, i.e., $\varphi_{1}(v_{i})<\varphi_{1}(n)$ and
$\varphi_{2}(v_{i})<\varphi_{2}(n)$, and thus both are in the set
characterized by $Q_{1}$. (2) Both $\varphi_{1}$ and $\varphi_{2}$ took the
second branch, i.e., $\varphi_{1}(v_{i})\geq\varphi_{1}(n)$ and
$\varphi_{2}(v_{i})\geq\varphi_{2}(n)$, and thus both are in the set
characterized by $Q_{2}$. (3) $\varphi_{1}$ took the first branch and
$\varphi_{2}$ took the second branch, i.e.,
$\varphi_{1}(v_{i})<\varphi_{1}(n)$ and
$\varphi_{2}(v_{i})\geq\varphi_{2}(n)$, and thus $\varphi_{1}$ is in the set
characterized by $Q_{1}$ and $\varphi_{2}$ is in the set characterized by
$Q_{2}$.

Importantly, the fourth case is not possible, because this would imply
$\varphi_{2}(n)-\varphi_{2}(v_{i})>0\geq\varphi_{1}(n)-\varphi_{1}(v_{i})$,
which contradicts the inequality
$\varphi_{1}(n)-\varphi_{1}(v_{i})\geq\varphi_{2}(n)-\varphi_{2}(v_{i})$ from
the frame $F$.

##  Appendix G Minimum Example

This section contains the proof, using the rule While-$exists$, that the
program $C_{m}$ from Fig. 9 satisfies the triple

${\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\lnot\mathit{emp}{}\land\square(k\geq
0)\\}}}\;C_{m}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\forall\langle\alpha\rangle\ldotp\varphi(x)\leq\alpha(x)\land\varphi(y)\leq\alpha(y)\\}}}$

Fig. 16 contains the (trivial) first part of the proof, which justifies that
the hyper-assertion $\exists\langle\varphi\rangle\ldotp P_{\varphi}$, where
$P_{\varphi}\triangleq(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))$,
holds before the loop, as required by the precondition of the conclusion of
the rule While-$\exists$.

Fig. 17 shows the proof of the first premise of the rule While-$\exists$,
namely

$\forall
v\ldotp\exists\langle\varphi\rangle\ldotp\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{P_{\varphi}\land\varphi(i)<\varphi(k)\land
v=\varphi(k)-\varphi(i)\\}}}\;\mathbf{if}\;(i<k)\;\\{C_{body}\\}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp
P_{\varphi}\land\varphi(k)-\varphi(i)\prec v\\}}}$

where $C_{body}$ is the body of the loop.

Finally, Fig. 18 shows the proof of the second premise of the rule
While-$\exists$. More precisely, it shows

$\forall\varphi\ldotp\vdash{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{\varphi}\\}}}\;\mathbf{if}\;(i<k)\;\\{C_{body}\\}\;{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{Q_{\varphi}\\}}}$

where $Q_{\varphi}\triangleq\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land 0\leq\varphi(y)\leq\alpha(y)$, from which we
easily derive the second premise of the rule While-$\exists$, using the
consequence rule (since $P_{\varphi}$ clearly entails $Q_{\varphi}$), and the
rule While-$\forall^{*}\exists^{*}$ rule.

$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\lnot\mathit{emp}{}\land\square(k\geq
0)\right\\}}}$ (Cons)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp\forall\langle\alpha\rangle\ldotp
0\leq 0\leq 0\land 0\leq 0\leq 0\land\varphi(k)\leq\alpha(k)\land
0=0\right\\}}}$ $\displaystyle\mathit{x}\coloneqq\mathit{0}\mathbf{;}\;$
(AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land 0\leq 0\leq
0\land\varphi(k)\leq\alpha(k)\land 0=0\right\\}}}$
$\displaystyle\mathit{y}\coloneqq\mathit{0}\mathbf{;}\;$ (AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land 0=0\right\\}}}$
$\displaystyle\mathit{i}\coloneqq\mathit{0}\mathbf{;}\;$ (AssignS)
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i)\right\\}}}$
Figure 16. First part of the proof: Proving the first loop invariant
$\exists\langle\varphi\rangle\ldotp P_{\varphi}$.
$\displaystyle{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))\land\varphi(i)<\varphi(k)\land
v=\varphi(k){-}\varphi(i)\right\\}}}$ $\displaystyle\mathbf{if}\;(i<k)\;\\{$
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))\land\varphi(i)<\varphi(k)\land
v=\varphi(k){-}\varphi(i)\land\square(i<k)\right\\}}}$
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp\exists
u\ldotp u\geq 2\land(\forall\langle\alpha\rangle\ldotp\forall v\ldotp v\geq
2\Rightarrow 0\leq 2*\varphi(x)+u\leq 2*\alpha(x)+v\land
0\leq\varphi(y)+\varphi(x)*u\leq\alpha(y)+\alpha(x)*v}}$ (Cons (1))
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\land\varphi(k)\leq\alpha(k)\land\varphi(i)+1=\alpha(i)+1)\land\varphi(k){-}(\varphi(i){+}1)\prec
v\\}}}$ $\displaystyle\quad\mathit{r}\coloneqq{}\mathit{nonDet()}\mathbf{;}\;$
$\displaystyle\quad\mathbf{assume}\;\mathit{r\geq 2}\mathbf{;}\;$
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq 2*\varphi(x)+\varphi(r)\leq 2*\alpha(x)+\alpha(r)\land
0\leq\varphi(y)+\varphi(x)*\varphi(r)\leq\alpha(y)+\alpha(x)*\alpha(r)\land\varphi(k)\leq\alpha(k)\land\varphi(i)+1=\alpha(i)+1)}}$
(HavocS, AssumeS)
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\land\varphi(k){-}(\varphi(i){+}1)\prec
v\\}}}$ $\displaystyle\quad\mathit{t}\coloneqq\mathit{x}\mathbf{;}\;$
$\displaystyle\quad\mathit{x}\coloneqq\mathit{2*x+r}\mathbf{;}\;$
$\displaystyle\quad\mathit{y}\coloneqq\mathit{y+t*r}\mathbf{;}\;$
$\displaystyle\quad\mathit{i}\coloneqq\mathit{i+1}$ (AssignS)
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))\land\varphi(k){-}\varphi(i)\prec
v\right\\}}}$ $\displaystyle\\}$ $\displaystyle\mathbf{else}\;\\{$
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))\land\varphi(i)<\varphi(k)\land
v=\varphi(k){-}\varphi(i)\land\square(i\geq k)\right\\}}}$ (Cons (2))
$\displaystyle\quad{\color[rgb]{0.25,0.41,0.88}\definecolor[named]{pgfstrokecolor}{rgb}{0.25,0.41,0.88}{\left\\{\exists\langle\varphi\rangle\ldotp(\forall\langle\alpha\rangle\ldotp
0\leq\varphi(x)\leq\alpha(x)\land
0\leq\varphi(y)\leq\alpha(y)\land\varphi(k)\leq\alpha(k)\land\varphi(i)=\alpha(i))\land\varphi(k){-}\varphi(i)\prec
v\right\\}}}$ $\displaystyle\quad\mathbf{skip}$ (Skip)