# Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni

► To cite this version:

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. OOPSLA 2024 - ACM Conference on Object Oriented Programming Systems Languages and Applications, Oct 2024, Pasadena (CA), United States. pp.784-809, 10.1145/3649839 . hal-04834120

HAL Id: hal-04834120

https://inria.hal.science/hal-04834120v1

Submitted on 16 Dec 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs

MARTIN AVANZINI, Centre Inria d'Université Côte d'Azur, France

GILLES BARTHE, MPI-SP, Germany and IMDEA Software Institute, Spain

BENJAMIN GRÉGOIRE, Centre Inria d'Université Côte d'Azur, France

GEORG MOSER, University of Innsbruck, Austria

GABRIELE VANONI, Centre Inria d'Université Côte d'Azur, France

We propose, implement, and evaluate a hopping proof approach for proving expectation-based properties of probabilistic programs. Our approach combines eHL, a syntax-directed proof system for reducing proof goals of a program to proof goals of simpler programs, with a "hopping" proof rule for reducing proof goals of an original program to proof goal of a different program which is suitably related (by means of pRHL, a relational program logic for probabilistic program) to the original program. We prove that eHL is sound for a core language with procedure calls and adversarial computations, and complete for the adversary-free fragment of the language. We also provide an implementation of eHL into EasyCrypt, a proof assistant tailored for reasoning about relational properties of probabilistic programs. We provide a tight integration of eHL with other program logics supported by EasyCrypt, and in particular probabilistic Relational Hoare Logic (pRHL). Using this tight integration, we give mechanized proofs of expected complexity of in-place implementations of randomized quickselect and skip lists. We also sketch applications of our approach to cryptographic proofs and discuss the broader impact of eHL in the EasyCrypt proof assistant.

CCS Concepts: • **Theory of computation** → **Semantics and reasoning**.

Additional Key Words and Phrases: probabilistic programs, Hoare logic, formal verification

**ACM Reference Format:**

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni. 2024. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. *Proc. ACM Program. Lang.* 8, OOPSLA1, Article 122 (April 2024), 26 pages. https://doi.org/10.1145/3649839

# 1 INTRODUCTION

There is a long line of work that develops rigorous approaches for proving properties of probabilistic programs. These approaches generalize to the probabilistic setting the classic notions of pre- and post-conditions and of invariants. A fundamental difference is that in the probabilistic setting these notions are quantitative. Assertions are expectations, i.e. functions that map states to extended positive reals. The use of expectations was pioneered by Kozen [Kozen 1985], systematized by Morgan, McIver and Seidel [Morgan et al. 1996], and still prevails to date.

Authors' addresses: Martin Avanzini, Centre Inria d'Université Côte d'Azur, Route des Lucioles - BP 93, Sophia Antipolis, 06902, France, martin.avanzini@inria.fr; Gilles Barthe, MPI-SP, Bochum, 44799, Germany and IMDEA Software Institute, Pozuelo de Alarcon, Madrid, 28223, Spain, gilles.barthe@mpi-sp.org; Benjamin Grégoire, Centre Inria d'Université Côte d'Azur, Route des Lucioles - BP 93, Sophia Antipolis, 06902, France, benjamin.gregoire@inria.fr; Georg Moser, Department of Computer Science, University of Innsbruck, Technikerstraße 21a, Innsbruck, 6020, Austria, georg.moser@uibk.ac.at; Gabriele Vanoni, Centre Inria d'Université Côte d'Azur, Route des Lucioles - BP 93, Sophia Antipolis, 06902, France, gabriele.vanoni@irif.fr.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

© 2024 Copyright held by the owner/author(s).

ACM 2475-1421/2024/4-ART122

https://doi.org/10.1145/3649839
Unfortunately, these approaches are often difficult to use. One main reason is that proofs of probabilistic programs do not always follow their control flow. Another reason is that once the target program property is fixed, it is often very convenient to reason about more abstract or refactored programs. From the theoretical perspective, none of these concerns is an issue, since in general these approaches are complete. However, more flexible approaches are desirable when verifying concrete examples, in particular when building mechanized proofs.

*Problem statement and contributions.* The main goal of this paper is to support flexible computer-aided verification of probabilistic programs, and in particular to develop an approach that allows breaking away from the control flow of programs, and change program representation during verification. Our target is to use our approach on relatively small but challenging probabilistic programs drawn from the theory of randomized algorithms and from cryptography. The choice of application domains naturally delineates the choice of the pWhile language, a core probabilistic language with sampling from discrete distributions, (non-recursive) procedures and adversaries. Informally, an adversary is an unspecified quantified procedure with constraints on the variables it can read and write, and on the procedures it can call. Thus the main challenge with adversaries is to devise proof principles that are sound w.r.t. all possible instantiations of the adversary. We note that in contrast with many other works in this realm, pWhile explicitly (and purposely) does not support conditioning, concurrency and non-determinism, which do not have a central role in our applications.

We achieve our goals in three steps. First, we define a program logic, called eHL, to reason about expectation-based properties of pWhile programs. Judgments of eHL are of the form {$f$} C {$g$} where C is a statement and f and g are maps from program states to extended positive reals. Informally, a judgment is valid if the expected value of g on the output memory is upper bounded by the value of f on the initial memory. The proof system for eHL closely matches the pGCL pre-expectation calculus [Morgan et al. 1996], except for loops, procedure and adversary calls:

- our rule for loops uses the notion of upper invariant from the literature;

- our rule for procedures uses auxiliary variables. It is folklore that complete proof rules for procedures—even in the deterministic setting—require the use of auxiliary variables, cf. [Kleymann 1998, 1999; Nipkow 2002a,b]. We show that auxiliary variables also allow to recover completeness in the probabilistic setting.

- our proof rule for adversaries is new. The main challenge is to devise useful and sound proof rules based exclusively on the aforementioned adversary constraints.

In addition, our program logic features a “hopping”<fnref n="1" /> proof rule to reduce the proof of a probabilistic program C' to a proof of a probabilistic program C. Hopping proofs subsume the “abstract and verify” or “refactor and verify” paradigms that are commonly used in verification by allowing the possibility to perform arbitrary long interleavings of verification steps with abstraction/refactoring steps. They have been previously used in interactive and automated program verification, including [Lammich and Tuerk 2012; Magill et al. 2010; Nipkow et al. 2020; Tassarotti and Harper 2019]. In our case, programs are probabilistic, so we use the relational program logic pRHL [Barthe et al. 2009] (we defer to subsequent sections for the definition of the pRHL judgment $\vdash \{P\} C' \sim C \{Q\}$) in the following way:

$$ \frac{\vdash \{f'\} C' \{g'\} \vdash \{P\} C' \sim C \{Q\} \quad \text{(condition omitted)} \quad \text{[PRHL]}}{\vdash \{f\} C \{g\}} $$

<footnote n="1">¹This style of proof is commonly used in cryptographic proofs under the name game-hopping (probabilistic programs with adversary calls are known as games in this realm). We simply use the name “hopping” here.</footnote>
This rule brings hopping proofs to the realm of expectation-based properties. Our case studies use the rule to switch to a more abstract representation of probabilistic programs, and to switch to a different probabilistic program, e.g. one whose control flow follows the reasoning.

Our logic also features a proof rule inspired by the frame rule, also known as rule of constancy, from classical Hoare Logic. Indispensable in practice, the rule improves upon modularity and compositionality of the calculus, by allowing one to focus only on those parts of assertions that are potentially affected during evaluation. Leveraging the reverse Jensen's inequality, the rule takes the form

$$ \frac{\vdash_Z \{f\} C \{g\} \quad F \perp \mathrm{Mod}_C \quad F \text{ concave and monotone}}{\vdash_Z \{F[f]\} C \{F[g]\}} \quad \text{[FRAME]} $$

In short, it permits the extension of judgments to arbitrary contexts $F$ (i) depending only on the memory not modified by the statement $C$ that is (ii) concave (e.g. linear or sublinear) and monotone, when seen as function. For instance, the rule allows to deduce $\vdash_Z \{\log(2x) + y\} C \{\log(x) + y\}$ from $\vdash_Z \{2x\} C \{x\}$ by taking $F[\Box] = \log \Box + y$, whenever $C$ leaves $y$ unchanged.

Second, we implement our program logic in the EasyCrypt proof assistant [Barthe et al. 2013], an existing tool for the verification of probabilistic programs and cryptographic proofs. Our implementation is carefully crafted to leverage some key features of EasyCrypt, including some weak forms of weakest precondition and SMT-based support. Concretely, we define and implement another set of proof rules that make deductive verification more practical. This set of proof rules is obtained by adapting classic approaches to turn Hoare logics into deductive verification tools, e.g. chaining applications of construct-specific rules with applications of sequential composition and non-structural rules. In order to reason effectively about pre-expectations in the ambient logic of EasyCrypt, we have also developed a library of mathematical definitions and facts about extended positive reals. This library is used critically in our case studies.

Finally, we use our framework to mechanize proofs of several examples. Our main examples are proofs of expected cost for in-place implementations of randomized quickselect and skip lists. Both examples leverage the full power of the framework and go beyond the reach of previous approaches. In particular, our proof is the first to establish a logarithmic bound for skip lists implementations—prior works either establish a logarithmic bound for an abstract description of skip lists [Haslbeck and Eberl 2020] or a linear bound for a (concurrent) implementation of 2-level skiplists [Tassarotti and Harper 2019]. In addition, we illustrate how our framework can be used beneficially in the context of cryptographic proofs. In contrast to the expected cost examples, which target real examples, we consider a synthetic example of cryptographic proofs, inspired from concurrent work [Barbosa et al. 2023] that uses our implementation of eHL to prove security of Dilithium, a post-quantum signature scheme recently standardized by the NIST (National Institute of Standards and Technology). The goal of our example is to illustrate how eHL can be used to obtain simpler proofs with tighter security bounds. However, potential uses of eHL are not limited to such use cases. We also discuss informally how eHL can be used to verify previously axiomatized techniques for reasoning about failure events, and to prove probability bounds in place of the existing logic implemented in EasyCrypt.

In summary, our main contributions are:

- the design, theoretical study and implementation of eHL;

- the application of eHL to expected cost analysis of randomized quickselect and skip lists;

- an illustration of the benefits of eHL in cryptographic proofs.

**Artifact.** The implementation of eHL, the library of expectations and the formally verified case studies will be submitted as an artifact. The case studies themselves are also available in source form as supplementary material. As an indication, the implementation of eHL proof system and
associated libraries represents about 3,000 lines of OCaml code and 1,000 lines of EasyCrypt code. The proof of the quickselect example represent 70 lines for the programs, 300 lines for a library on partition, 110 lines for the equivalence proof in pRHL (concrete version versus the abstract one) and 70 lines for the proof bounding the expected cost in eHL. For skip lists, the proof consists of 2600 lines of EasyCrypt code, about 500 lines for bounding the expectation, the remaining part is mostly concerned with the equivalence proofs and functional correctness. The implementation and case studies will also be made publicly available in GitHub.

***Outline.*** This paper is structured as follows. In Section 3, we provide a bird's eye view on the contributions of this work. Sections 4 and 5 formally establish the expectation logic eHL and its integration with pRHL, while in Section 6 we employ our framework to obtain a fully formalized average case complexity analysis of (a natural and realistic implementation of) *skip lists*, a randomized data structure of interest for practitioners. In Section 7 we extend eHL to a setting permitting adversarial code and demonstrates the usefulness of the logic for carrying out cryptographic proofs. Section 8 we describe the integration of eHL into EasyCrypt and provide further details on the formal verification of the case studies. In Section 2 we consider related work, and we finally conclude in Section 9.

## 2 RELATED WORK

There is a large body of work on formal verification of probabilistic programs and resource analysis. For space reasons, we mention only closely related work.

***Verification of probabilistic programs.*** Expectation-based reasoning can be traced back to the seminal work of Kozen [Kozen 1985], who developed a sound and complete propositional dynamic logic for a core probabilistic programming language. It was further developed by Morgan, McIver and Seidel [Morgan et al. 1996], who introduced and studied extensively probabilistic predicate transformers for a core probabilistic language with non-deterrinism. These approaches were recently extended to recursive procedures [Olmedo et al. 2016] and conditioning [Olmedo et al. 2018]. eHL inherits many technical tools from this line of work, in particular the use of upper invariants. However, eHL makes several (minor but practically important) technical contributions: it embeds pRHL into expectation-based reasoning; it supports adversary calls; it features a non-structural rule to simplify expectations (to our best knowledge, no such rule has been considered before); it recasts in the setting of probabilistic programs existing approaches to achieve completeness of Hoare logic in presence of procedures. For the latter, we follow the approach of [Kleymann 1998, 1999; Nipkow 2002a,b].

***Complexity analysis of probabilistic programs.*** There is also a huge body of work related to complexity analysis of probabilistic programs. Related to probabilistic predicate transformers, Kaminski et al. [2018] define an expected runtime transformer for a core probabilistic programming language with non-determinism. Subsequent works extend the expected runtime transformer with recursive procedures [Olmedo et al. 2016], amortized reasoning Batz et al. [2023], or to higher-order functions [Avanzini et al. 2021]. Related to this line of work, several automated tools have emerged Avanzini et al. [2020b, 2023]; Ngo et al. [2018]. Also martingale theory has been successfully tailored towards the analysis of complexity related properties of imperative programs [Agrawal et al. 2018; Barthe et al. 2016; Chakarov and Sankaranarayanan 2013; Chatterjee et al. 2017; Takisaka et al. 2018; Wang et al. 2019]. These notions correspond close to that of Lyapunov ranking functions for proving (positive almost-sure) termination, and for deriving bounds on the runtime [Avanzini et al. 2020a; Bournez and Garnier 2005]. For functional languages, type-based approaches to complexity analysis turned out useful [Avanzini et al. 2019; Leutgeb et al. 2022; Wang et al. 2020].
*Mechanized analyses of probabilistic programs.* Haslbeck [2021] implements a Hoare style calculus related to the ert calculus of Kaminski et al. within the Isabelle/HOL proof assistant. Interestingly, his work contains a frame rule which can be interpreted as a special case of the one we give. Related, Hurd et al. [2004] formalized a weakest pre-condition calculus for probabilistic programs within HOL, and proof several interesting meta-theoretical properties of the calculus. Program verification is aided through the extraction of recurrence relations to Prolog. Both works include proofs of soundness and completeness of the transformer. In contrast, our core logical rules are part of the trusted computing base. This is in line with the approach inEasyCrypt, where proof rules for program verification are not verified—in other words, EasyCrypt does not use a shallow nor a deep embedding of programs, but rather a hardwired embedding.

Van der Weegen and McKinna [2008] was probably the first to formalize quicksort in a proof assistant, more precisely in Coq. They used a shallow embedding and analyzed the average case complexity of more high-level, functional version of quicksort. In a similar spirit, Eberl et al. [2020] use the Isabelle/HOL proof assistant to reason via a shallow embedding about the average case complexity of algorithms on binary tree structures. Notably, their analysis covers (the functional variant of) quicksort. Tassarotti and Harper [2018] study quantitative properties of concrete randomized algorithms, focusing on the formal verification of tail bounds. For example they handle (a functional version of) quicksort, again using a monadic embedding. Their analysis is formalized in Coq.

The average complexity analysis of skiplists is rather intricate, rendering skip lists a prime example to evaluate the expresivity and usability of proof assistants. Haslbeck and Eberl [2020] formalise the relationship between the expected height and expected length of search paths within the proof assistant Isabelle/HOL, leading also to the formalisation of a considerable amount of results of probability theory. Wheareas the starting point of Haslbeck and Eberl is a formal but abstract specification, here, we study a concrete algorithm resembling the reference implementation given by Pugh [1990b]. This explains our focus on program logics, rather than the formalisation of mathematical results. Relying on the extensive library underlying EasyCrypt, our formalisation effort is mostly concerned with laws on expectations (such as, linearity or Jensen's inequality). Strongly related to our formal complexity analysis of skip lists is the work by Tassarotti and Harper [2019] on concurrent skip lists. Their Coq formalization extends Iris [Jung et al. 2015] with probabilistic coupling, conceptually in line with our use of eHL in conjunction with pRHL. Their very impressive formalization is orthogonal to our results. On the one hand, the focus is on the verification of quantitative program behaviour in the context of concurrency, while our analysis only concerns sequential evaluation. On the other hand, the notion of skip lists is restricted to two levels and the obtained upper bound on the expected search length is linear, while we consider skip lists in their original definition and re-obtain the original logarithmic bound, in expectation. This latter aspect requires a more involved encoding of our non-concurrent version and conclusively a more sophisticated verification.

*Comparison with EasyCrypt.* EasyCrypt is an interactive proof assistant targetted to formal verification of cryptographic proofs. Its main component pRHL is used to support game-hopping proofs. In addition, EasyCrypt features a program logic called phoare for reasoning about the probability of events. In contrast to eHL, phoare judgments are of the form $\vdash_{\diamond\phi} \{\phi\} c \{\psi\}$, where $\phi, \psi$ are boolean-valued assertions and $\diamond$ is either $\leq$, $\geq$, or $=$; unfortunately, it is difficult to build sound, complete, and practical proof systems for such judgments. Moreover, the proof rules of phoare, and in particular the rule for loops, require programs to be certainly terminating. In general, it would seem beneficial to deprecate phoare and use eHL instead.
var ct;

proc partition(a, l, h)

(p, i) ← (a[h], l - 1);

for j = l to h - 1 do

if a[j] < p then

i++; swap(a, i, j)

ct++;

i++; swap(a, i, h);

return i

proc rpartition(a, l, h)

p ← $\mathfrak{u}$ if (l, h);

swap(a, p, h);

i ← partition(a, l, h);

return i

proc qselect(a, k)

ct ← 0;

(l, h) ← (0, size(a) - 1);

while l < h do

i ← rpartition(a, l, h);

if i = k then

l ← i; h ← i // exit loop

elif i < k then

l ← i + 1 // descent right

else

h ← i - 1 // descent left

return a[k]

<caption>(a) Quickselect.</caption>

var ct;

[] l ≤ h | ct + (h - l) + l (h-l) ∑ h i = l f (i)

proc rpartition_abs(l, h)

[] l ≤ h | ct + (h - l) + l (h-l) ∑ h i = l f (i)

[] E$_{unif(l,h)}$ [λi. ct + (h - l) + f (i)]

ct ← ct + (h - l);

[] E$_{unif(l,h)}$ [λi. ct + f (i)]

i ← $\mathfrak{s}$ if (l, h);

[] ct + f (i)

return i

[] ct + f (res)

[] 0 ≤ k < n | 4(n - 1)

proc qselect_abs(n, k)

[] 0 ≤ k < n | 4(n - 1)

ct ← 0;

[] 0 ≤ k < n | ct + 4(n - 1)

(l, h) ← (0, n - 1);

[] 0 ≤ l ≤ k ≤ h | ct + 4(h - l)

while l < h do

[] l < h ∧ 0 ≤ l ≤ k ≤ h | ct + 4(h - l) (*)

[] 0 ≤ l ≤ k ≤ h | ct + (h - l) + 1 (h-l+1) ∑ h i = l g(i, k, l, h)

i ← rpartition_abs(l, h);

[] 0 ≤ l ≤ k ≤ h | ct + g(i, k, l, h)

if i = k then l ← i; h ← i

elif i < k then l ← i + 1

else h ← i - 1

[] 0 ≤ l ≤ k ≤ h | ct + 4(h - l)

[] h ≤ l ∧ 0 ≤ l ≤ k ≤ h | ct + 4(h - l)

[] ct

return ()

[] ct

<caption>(b) Size abstraction.</caption>

<caption>Fig. 1. Implementation of `qselect` (left) of quickselect and its eHL annotated abstraction `qselect_abs` (right). The term `g(i, k, l, h)` abbreviates `if i = k then 0 else if i < k then 4(h - (1 + l)) else 4(h - 1 - l)`.</caption>

EasyCrypt also provides a cost logic for adversarial programs [Barbosa et al. 2021]. The purpose of the cost logic is to upper bound the complexity of constructed adversaries, i.e. programs with adversary calls that formalize the security reduction from security of a cryptographic scheme to hardness assumptions or assumptions about primitives. One main rule of the logic is an instatiation rule, which allows to reason about the cost of a program where the adversary is instantiated by another program—it can either be a concrete program but also a so-called constructed adversary. The instantiation rule is required to upper bound constructed adversaries for complex cryptographic systems that are built from several components. The logic is focused on worst-case cost. An interesting direction for future work is to adapt this logic to expected cost.

## 3 A BIRD'S-EYE VIEW ON OUR METHODOLOGY

In what follows, we introduce our methodology on Tony Hoare's quickselect [Hoare 1961]: a non-trivial, (possibly) non-recursive, randomized algorithm.
**Quickselect.** *Sorting and searching* are arguably the most studied algorithmic problems in computer science.<fnref n="2" /> Quickselect is a selection algorithm to find the *k*th smallest element in a given (unordered) array. Quickselect operates similar to quicksort, by partitioning the array around a chosen pivot. However, the recursive call is performed just on the partition actually containing the element one is looking for. This observation allows one to perform a tail-call optimization of recursive quickselect, which produces an iterative algorithm. As for quicksort, performance degrades if bad pivots are consistently chosen. By choosing a pivot uniformly at random at each stage, it can be shown that quickselect expected runtime, often more interesting than worst-case complexity when randomness plays a role, is in $O(n)$.<fnref n="3" /> The code of quickselect with random pivot selection is given in Figure 1a. Arrays are indexed from 0, for instance, `qselect([4, 6, 2, 8], 1) = 4` since 4 occurs at index 1 in the sorted input array [2, 4, 6, 8]. Randomized partitioning of an array a (within indices 1 and h) is implemented with `rpartition(a, 1, h)`. The instruction `unif(1, h)`, used to choose the pivot index p, samples at random an integer between 1 and h. It is the only point of the code where randomness actually plays a role. Partitioning is then carried out via partition following the Lomuto partition scheme, expecting the pivot at the final index.

**Informal Complexity Analysis.** The classic textbook proof on the average case complexity of quickselect can be found in [Cormen et al. 2009]. It is based on a sequence of lemmas that are proved looking at the source code in a quite abstract way, through some high-level reasoning.

An important observation is that for each input, if the pivot is chosen uniformly at random from the interval [1, h], then so is its rank (the position of an element in the sorted array) i. Thus, partitioning with pivot of rank i has probability $1/(h-1+1)$ and, depending on i, the resulting parts of the partition have sizes $i-1$ and $h-i$, respectively. The procedure `qselect` loops over just one of the parts, the one actually containing the element we are looking for. In particular, if $i < k$, the right partition of size $h-i$ is explored, likewise, if $i > k$, then the left partition of size $i-1$ is explored. In the remaining case $i=k$ the k-th element has been found. Averaging over all the $h-1+1$ possible partitions and noting that the number of comparisons performed inside partition is $h-1$, the average number of comparisons can be estimated accurately by solving the following recurrence relation:

$$C(1, h) = (h-1) + \frac{1}{h-1+1} \left( \sum_{i=1}^{k-1} C(i+1, h) + \sum_{i=k+1}^{h} C(1, i-1) \right) \quad (\dagger)$$

Then, it is not difficult to prove that $C(1, h) \le 4(h-1)$. Since l is initialized to 0 and h to size(a) - 1, we obtain the well-known linear bound of $O(size(a))$, in expectation.

**Towards a Formal Analysis.** The complexity analysis sketched above is still informal. In particular, the recurrence relation is obtained by a high-level analysis of the code, and through informal reasoning involving probabilities, sizes of partitions, etc. How can we be sure that all of this is correct?

In this paper, we propose a formal *end-to-end methodology* that is able to provide upper-bounds on the complexity of randomized programs, based on the general methodology of Hoare logic [Hoare 1969]. Towards this formalization, we first have to endow a cost model, i.e., be precise in exactly what to measure. A generic way to do so is to simply instrument the program with a cost counter, as we have already done in Figure 1a. Notice how the global variable ct takes account of the total number of comparisons—the usual cost metric for sorting and selection algorithms—performed by

<footnote n="2">²This is for example witnessed by the fact that Donald Knuth dedicated an entire volume of his celebrated series *The Art of Computer Programming* [Knuth 1973] just to these two problems.</footnote>

<footnote n="3">³Actually, choosing the pivot uniformly at random turns out to allow the same average-case complexity analysis of deterministic quickselect with uniformly distributed inputs.</footnote>
**qselect.** Our objective now turns into bounding the value that ct takes on average after execution, in terms of the size of the input.<fnref n="4" />

From here, a fully formalized complexity analysis of `qselect` is certainly possible, however, unnecessarily complicated. As we have already seen in the informal proof, a priori we do not really have to reason about the full program. Some parts of it can be abstracted, so that the complexity analysis becomes easier. This is exactly what we have done when we have claimed that `partition` does h-1 comparisons. Indeed, program abstraction is a useful tool in program analysis (see e.g. [Magill et al. 2010]). Consider the procedure `qselect_abs`, depicted in Figure 1b, giving a complexity preserving skeleton of `qselect`. Ignoring gray annotations for now, in essence arrays a are abstracted by their size n. While the skeleton of `quickselect` remains identical, partitioning of the array becomes superfluous. In `rpartition_abs` a cost of h-1 is incurred directly and the rank i, rather than the pivot p, is sampled.

Naturally, the claim about the complexity equivalence of the two programs has to be made formal. To this end, *relational program logics* such as *probabilistic relational Hoare logic* (pRHL) provide a suitable solution [Barthe et al. 2015, 2012, 2017]. Moreover, support for pRHL is readily available in the proof assistant EasyCrypt. In pRHL, judgments take the form of (relational) Hoare triples

$$ \{P\} C \sim D \{Q\} $$

where P and Q are predicates over the joint program states of C and D, with the informal meaning that on inputs related by P, the programs C and D produce an output (distribution) related by Q.³ Referring with $(\cdot)^{(1)}$ and $(\cdot)^{(2)}$ to the state of the left- and right program the triple

$$ \vdash \{ \mathit{unique}(a^{(1)}) \wedge \mathit{size}(a^{(1)}) = n^{(2)} \wedge k^{(1)} = k^{(2)} \} \mathit{qselect}(a, k) \sim \mathit{qselect\_abs}(n, k) \{ \mathit{ct}^{(1)} = \mathit{ct}^{(2)} \} \quad \mathit{(equiv\_qselect)} $$

asserts that if the inputs are related in the obvious way, then the (distributions of) cost counters ct are identical after execution.<fnref n="6" /> The main crux of the proof lies in proving a related statement on partitioning:

$$ \vdash \left\{ \begin{array}{l} \mathit{unique}(a^{(1)}) \wedge (1, h)^{(1)} = (1, h)^{(2)} \\ \mathit{rpartition}(a, 1, h) \sim \mathit{rpartition\_abs}(a, 1, h) \\ \{ \mathit{ct}^{(1)} = \mathit{ct}^{(2)} \wedge \mathit{res}^{(1)} = \mathit{res}^{(2)} \} \end{array} \right\} \quad \mathit{(equiv\_rpartition)} $$

where `res` refers to the return value of the procedure. Comparing the two procedures, in effect this statement formalizes that (i) partitioning itself performs h-1 comparisons ($ct^{(1)} = ct^{(2)}$) and that (ii) the rank of the pivot lies uniformly in the interval $[1, h]$ ($res^{(1)} = res^{(2)}$). While the former point is quite trivial to prove, the latter property essentially states that pivot positions and ranks are in a bijective relationship, a property that rests on functional correctness of `partition` and uniqueness.

<footnote n="4">⁴ The attentive reader may have noticed that since we are about to measure a counter after execution, the correspondence hinges on (almost-sure) termination. If one is interested in the analysis of non-terminating programs and the cost incurred by infinite executions, one way to overcome the discrepancy is to externalize the cost counter in the program semantics (see e.g. [Kaminski et al. 2018]).</footnote>

<footnote n="5">⁵ To be more precise, the judgment guarantees a *probabilistic coupling* of the output distributions within relation *Q*, as detailed in Section 5.</footnote>

<footnote n="6">⁶ To slightly simplify proofs, we assume via predicate `unique`($a^{(1)}$) that the input array a to the left procedure contains no duplicate elements.</footnote>
*Formal Reasoning about Expectations.* Through the correspondence (equiv_qselect) we have achieved a separation of concerns, as functional correctness properties relevant to the complexity analysis have been dealt with. Knowing that qselect_abs is a cost-preserving abstraction of qselect, we can thus focus on the core of the complexity analysis, as carried out in the informal analysis above.

For this, we use a Hoare logic for reasoning about expectations. This logic, dubbed *Expectation Hoare Logic* (eHL), constitutes a sound and complete logic for reasoning about judgments of the form

$$ \vdash \{f\} C \{g\} $$

where $f, g$ are (non-negative) real-valued functions over the program state of $C$, also referred to as pre- and post-expectation, respectively. Informally, this judgment states the expected value of $g$ after execution of $C$ is bounded by $f$. More formally, this judgment is valid if $\mathbb{E}_{\llbracket C \rrbracket_m} [g] \le f$ for any initial program memory $m$, where the left-hand side denotes the expected value of $g$ on the (sub)distribution $\llbracket C \rrbracket_m$ of memories obtained after evaluating $C$ on $m$.

Coming back to quickselect, the judgment

$$ \vdash \{0 \le k < n | 4(n-1)\} qselect_abs(n, k) \{ct\} \qquad (qselect_abs_cost) $$

bounds the expected value of $ct$ after execution by $4(n-1)$. The guard $0 \le k < n$ in the pre-expectation should be understood as a classical pre-condition, for details see Section 5. We have decorated the code of Figure 1b with the corresponding eHL assertions at each line of the listing. The proof of this statement relies again on an auxiliary statement on partitioning, namely,

$$ \vdash \{1 \le h | ct + (h-1) + \frac{1}{h-1+1} \sum_{i=1}^{h} f(i)\} rpartition_abs(1, h) \{ct + f(res)\} \qquad (rpartition_abs_cost) $$

Here, the free variable $f$ should be understood as a universally quantified, *logical* (function) variable, and as above, $res$ refers to the return value of $rpartition_abs$. Notice how this statement reflects that the cost counter is advanced by $h-1$, and that the return value is sampled uniformly from the interval $[1, h]$; eHL is in many aspects reminiscent of classical HL. Indeed, the core rules—when restricted to predicates—are identical. As such it transfers Hoare-style backward reasoning to probabilistic programs. Where eHL does depart from HL is the support of sampling instructions $S$, embodied by the axiom $\vdash \{ \mathbb{E}_S[\lambda v. f[x/v]] \} \times \leftarrow_S S \{f\}$, generalising the the usual axiom for assignments $\vdash \{ f[x/E] \} \times \leftarrow E \{f\}$. Also the rule of consequence,

$$ \frac{f \ge f' \quad \{f'\} C \{g'\} \quad g' \ge g}{\{f\} C \{g\}} $$

extends naturally from HL to eHL, implications turn into inequalities. The two axioms together with the consequence rule, tacitly employed before the first statement within the procedure's body, should be sufficient to comprehend the annotations given in Figure 1b around the definition of $rpartition_abs$.

In a similar fashion, the annotations of `qselect_abs` can be traced from bottom to top. As in classical HL, the treatment of loop rests on finding a suitable invariant, here it is given by $0 \le 1 \le k \le h | ct + 4(h-1)$. Within the loop, the guard $1 < h$ can be additionally assumed, the guard is falsified immediately after the loop. Concerning the nested conditional in the loop, the term $ct + g(i, k, 1, h)$ is computed syntactically as the weakest pre-expectation given post-expectation $ct + 4(h-1)$. (See the caption for the precise definition of $g$.) Concerning the call `rpartition_abs(1, h)` the logical variable $f$ is instantiated by the function $i \mapsto g(i, k, 1, h)$, since the result of the call is bound to $i$. Interestingly, one recovers, in a formal and syntax-directed way,
the recurrence relation of the previous paragraph through the weakening performed in (★). Indeed, the (approximate) solution of the recurrence (†) becomes the invariant of the main while loop.

The combination of (equiv_qselect) and (qselect_abs_cost) yields

$$ \vdash \{ \text{unique}(a) \wedge 0 \le k < \text{size}(a) | 4(\text{size}(a) - 1) \} \text{qselect}(a, k) \{ \text{ct} \} \quad (\text{qselect_cost}) $$

confirming the linear bound—O(size(a))—on the expected cost of qselect, derived above in the informal analysis.

Integration within EasyCrypt. The here presented case study on quickselect clarifies the effectiveness of our verification methodology. Relational reasoning provided by pRHL—in particular that employed to guarantee functional correctness—and quantitative reasoning provided by eHL—formalizing the original (informal) complexity proof—work together in a synergistic way. As mentioned, the development is fully formalized (within EasyCrypt), rendering heightened assurance that none of the (necessary) intricacies of a complexity analysis of a randomized algorithm have been overlooked. To this end, EasyCrypt has been extended with support for eHL, see Section 8.

# 4 A PROBABILISTIC PROGRAMMING LANGUAGE

We consider here a simple imperative probabilistic programming pWhile capturing the core language of EasyCrypt without adversaries. This language follows the spirit of Dijkstra's *Guarded Command Language* but including (non-recursive) procedures and a separation of global and (statically scoped) local variables. The language will be consecutively extended to permit adversarial code in Section 7, when we discuss applications to cryptography.

Syntax. Let $Fun = \{f, g, ...\}$ be a set of procedure names, and $Var = \{x, y, z, ...\}$ a set of variables, partitioned into local variables LVar and global variables GVar. The set Stmt of statements is defined by the following syntax:

C, D ::= skip | x ← E | x ←$^S$ S | x ← f(E) | C; D | if B then C else D | while B do C

Here, $E \in$ Expr is drawn from a set of expressions, $B \in$ BExpr is a Boolean expression, and $S \in$ SExpr a sampling expression. The statements are mostly standard. The statement $x \leftarrow E$ gives the usual, deterministic assignment, whereas $x \leftarrow^S S$ samples a value from $S$, and thereby makes the language probabilistic. Statement $x \leftarrow f(E)$ calls a procedure with argument $E$ and assigns its return value to $x$. Zero or more than one argument can be passed to procedures as tuples. We require that $x$ is a local variable. A procedure is declared through a procedure definition of the form

proc f(x) C; return E,

where $x \in$ LVar is the formal parameter, $C \in$ Stmt the body and $E \in$ Expr the return expression of $f$. Global variables should be understood as implicit input and output to procedures, whereas local ones are statically scoped. A program $P \in$ Prog is a finite sequence of (mutually exclusive) procedure definitions.

Monadic Denotational Semantics. Semantics of imperative programs can be given in many ways. Here, we endow the language with a denotational (monadic) style semantics, lending itself better to the proofs of soundness and completeness of our logic. Since programs are probabilistic, we interpret them as functions from states to subdistributions of states, rather than as mere (partial) state transformers.

A subdistribution over a set $A$ is a function $d: A \to [0, 1]$ such that $\sum_{a \in A} d(a) \le 1$, with $D A$ we denote the set of all subdistributions over $A$. For $d: D A$, the support $\text{supp}(d) \subseteq A$ is given by the collection of elements $a \in A$ with $d(a) > 0$. Throughout the following, we consider only discrete subdistributions, that is, where the set $A$ is countable. Let $\mathbb{R}^{+\infty}$ denote the non-negative
<table><caption>Fig. 2. Semantics of statements [[·]]<sub>(·)</sub>: Stmt → Mem → D Mem.</caption><thead><tr><th>C ∈ Stmt</th><th>[[C]]<sub>m</sub></th></tr></thead><tbody><tr><td>skip</td><td>dunit m</td></tr><tr><td>x &larr; E</td><td>dunit m[x/[[E]]<sub>m</sub>]</td></tr><tr><td>x &larr; S</td><td>dlet v &larr; [[S]]<sub>m</sub> in dunit m[x/v]</td></tr><tr><td>x &larr; f(E)</td><td>dlet (m'<sub>g</sub>, r) &larr; [[f]]<sub>(m<sub>g</sub>,[[E]]<sub>m</sub>)</sub> in dunit (m'<sub>g</sub> &cup; m<sub>l</sub>)[x/r]</td></tr><tr><td>C; D</td><td>dlet m' &larr; [[C]]<sub>m</sub> in [[D]]<sub>m'</sub></td></tr><tr><td>if B then C else D</td><td>sup<sub>i∈N</sub> [[while<sup>(i)</sup> B do C]]<sub>m</sub> where</td></tr><tr><td>while B do C</td><td>[[C]]<sub>m</sub> if [[B]]<sub>m</sub>,<br>[[D]]<sub>m</sub> otherwise.</td></tr><tr><td>[[while<sup>(0)</sup> B do C]]<sub>m</sub> &triangleq; fail</td><td></td></tr><tr><td>[[while<sup>(i+1)</sup> B do C]]<sub>m</sub> &triangleq; {dlet m' &larr; [[C]]<sub>m</sub> in [[while<sup>(i)</sup> B do C]]<sub>m'</sub> if [[B]]<sub>m</sub>,<br>dunit m</td><td>if [[B]]<sub>m</sub>,<br>otherwise.</td></tr></tbody></table>

reals extended with top element $\infty$. Given function $f: A \to \mathbb{R}^{+\infty}$ and a distribution $d: DA$ we denote by $\mathbb{B}_d[f] \triangleq \sum_{a \in \text{supp}(d)} f(a) \cdot d(a)$ the *expected value of f on d*. By the Monotone Convergence Theorem, this value always lies within $\mathbb{R}^{+\infty}$. The subdistribution functor D forms a monad. The *unit dunit*: $A \to DA$ returns on $a \in A$ the Dirac distribution $\delta_a$ (where $\delta_a(b) \triangleq 1$ if $a = b$ and $\delta_a(b) \triangleq 0$ otherwise). The *bind dbind*: $DA \to (A \to DB) \to DB$ is defined as **dbind** $d f \triangleq \lambda b. \sum_{a \in \text{supp}(d)} d(a) \cdot f ab: DB$. To ease notation, we may write **dlet** $a \leftarrow d$ in $f(a)$ for **dbind** $d (\lambda a. f(a))$. With **fail**: DA we denote the subdistribution with empty support.

We model program *memories* as mappings $m \in \text{Mem} \triangleq \text{Var} \to \text{Val}$ from variables to (a discrete set of) values $\text{Val}$. Each memory $m$ can be partitioned into a *global memory* $m_g: \text{GMem} \triangleq \text{GVar} \to \text{Val}$ and a *local memory* $m: \text{LMem} \triangleq \text{LVar} \to \text{Val}$. We write $m[x/v]$ for the memory obtained from $m$ by updating $x$ to $v$. We suppose that expressions $E \in \text{Expr}$, Boolean expressions $B \in \text{BExpr}$ and sampling expressions $S \in \text{SExpr}$ are equipped with semantics $[[E]]<sub>(·)</sub>: \text{Mem} \to \text{Val}$, $[[B]]<sub>(·)</sub>: \text{Mem} \to \mathbb{B}$ and $[[S]]<sub>(·)</sub>: \text{Mem} \to \text{DVal}$, respectively. Statements C are then interpreted as functions $[[C]]<sub>(·)</sub>: \text{Mem} \to \text{DMem}$, see Figure 2. The definition is mostly standard. Noteworthy, each procedure $f$ is interpreted as a function in $\text{GMem} \times \text{Val} \to \text{D}(\text{GMem} \times \text{Val})$, parameterised by the global memory before execution and a value—the formal parameter—and yielding as output a subdistribution of modified global memories and return values. Upon invocation, the local memory is initialised to an *initial memory* $m_l^0$ assigning to each variable $x \in \text{LVar}$ a default value, and the formal parameter $x$ is bound by the argument. Upon completion, the return value is evaluated and returned, together with the potentially modified global memory. Precisely, we interpret a declaration by

$$ [[\text{proc } f(x) \text{ C; return } E]]_{(m_g, v)} \triangleq \text{dlet } m' \leftarrow [[C]]_{(m_g \psi m_l^0[x/v])} \text{ in dunit } (m'_g, [[E]]_{m'}) . $$

and we use $[[f]]_{(m_g, v)}$ as a short-hand when $f$ is declared in the program as above.

# 5 EXPECTATION HOARE LOGIC

In this section, we now present the *Expectation Hoare Logic* (eHL) formally, starting with the core logic and then integrating relational reasoning towards the end of the section.
As seen in Section 3, eHL is designed for reasoning reason about judgments of the form {$f$} C {$g$}, where C is a pWhile statement and f and g, dubbed pre- and post-expectations respectively, are functions from states to (non-negative) extended reals. In effect, eHL manipulates slightly more complex judgments in order to address a well-known issue with completeness of proof rules for procedures. In a nutshell, the standard proof systems for procedures aim to achieve modularity by proving for each procedure a procedure specification. These are triples of the form {$p$} f {$q$}. For instance, in (rpartition_abs_cost) on page 9, we have employed the specification

$$ \{ l \leq h \mid ct + (h - l) + \frac{1}{h-l+1} \sum_{i=l}^{h} f(i) \} rpartition_abs \{ ct + f(res) \}. $$

In this specification, the pre-expectation is parameterised in the argument—here, a tuple (l, h)— whereas the post-expectation is parameterised in the return value res. Both may reference global variables like the counter ct above—they are implicit input and output of the procedure. Then, modularity is achieved by using the procedure specification every time the procedure is called. Unfortunately, a naive realization of this approach does not achieve completeness. Incompleteness arises because the specification of a function is independent of its call site. Since independence in itself is desirable for reducing proof effort, the standard compromise is to provide users with a means to adapt a declaration to specific call-sites, to reason about properties potentially involving local state. To this end, we borrow the notion of auxiliary (or logical) variables from Kleymann [1998]. Auxiliary variables may occur in pre- and post-expectations and are (implicitly) universally quantified. Effectively, they turn declarations into schemata, where auxiliary variables can be freely instantiated. For instance, in the above specification of rpartition_abs we used an auxiliary variable f, with the intended meaning that the triple holds for any concrete instantiation of f. As for Kleymann, auxiliary variables yield a conceptual simple solution to recover (relative) completeness of our logic. With this in mind, we can embark of defining eHL. Our presentation follows closely the presentation of (classical) Hoare Logic HL given by Nipkow [2002b], with pre- and post-expectations given by semantic objects parameterized by a type Z of auxiliary variables, rather than terms or expressions. In eHL, judgments now take one of two forms, namely

$$ \vdash_Z \{f\} C \{g\} \quad \text{or} \quad \vdash_Z \{p\} f \{q\}, $$

where $f, g: Z \to \text{Mem} \to \mathbb{R}^{+\infty}$ and $p, q: Z \to \text{GMem} \times \text{Val} \to \mathbb{R}^{+\infty}$. As indicated above, pre- and post-expectations of procedures are parametric only in the global memory. In the pre-expectation $p$, the additional value argument refers to the formal parameter of $f$, whereas in the post-expectation $q$ it refers to the returned value. To avoid notational overhead, in examples, we will continue to write pre- and post-expectations as expressions, potentially referring to extra auxiliary variables besides program variables. For instance, $Z = \mathbb{Z} \times \mathbb{Z}$ admits two integer valued extra variables, say $x$ and $y$. If $v$ is a program variable, an expression such as $x + y + v$ formally represents $\lambda(x, y) m. x + y + m(v)$. In a similar vain, we will use variables arg and res to refer to the formal parameter and return value within procedure specifications.

eHL is tailored to proving upper-bounds $f$ on the value that a function $g$ takes, in expectation, after running a program. This meaning is made precise through the notion of validity.

**Definition 5.1 (Validity of judgments).**

(1) A triple {$f$} C {$g$} is valid, in notation $\vdash_Z \{f\} C \{g\}$, if $\mathbb{E}_{[C]}_m [gz] \leq fzm$ holds for all $z \in Z$ and initial memories $m \in \text{Mem}$, and,

(2) a procedure specification {$p$} f {$q$} is valid, in notation $\vdash_Z \{p\} f \{q\}$, if $\mathbb{E}_{[f]}_{(m,g,v)} [qz] \leq pq(m_g, v)$ holds for all $z \in Z$, initial memories $m_g \in \text{GMem}$ and parameters $v \in \text{Val}$.

Finally, through the binary operator ($|$) that we have already used when reasoning about quickselect, we can also combine classical with probabilistic reasoning. Semantically, the operator
Structural Rules

<figure><img src="image_2.png" /></figure>

Procedure Declarations

<figure><img src="image_3.png" /></figure>

Logical Rules

<figure><img src="image_4.png" /><figcaption>Fig. 3. Kernel rules of eHL.</figcaption></figure>

is defined such that $(\text{true} | r) \triangleq r$ and $(\text{false} | r) \triangleq \infty$ for any real value $r \in \mathbb{R}^{+\infty}$, and extended to pre- and post-expectations in the obvious way. This way, $\{Q | f\} \in \mathcal{C}\{P | g\}$ for instance asserts validity of $\{f\} \in \mathcal{C}\{g\}$ under pre-condition $P$, guaranteeing post-condition $Q$.

**The Core Rules.** Figure 3 presents the core rules of eHL. Interestingly, and what we believe makes the logic in particular usable, is that the core rules are in essence identical in shape to that of classical HL. This is in particular visible in the rules (SKIP), (SEQ) and (ASSIGN). In Rule (ASSIGN), $f[x/E]$ is short-hand for $\lambda z m. f z m[x/\llbracket E \rrbracket_m]$. Rule (SAMPLE) generalizes the usual assignment rule to sampling instructions: the pre-expectation $\mathbb{E}_S[\lambda v. f[x/v]] \triangleq \lambda z m. \mathbb{E}_{\llbracket S \rrbracket_m}[\lambda v. f z m[x/v]]$, is the weakest one binding post-expectation $f$ when $x$ is sampled from $S$. For instance, $\vdash_Z \{0.5\} x \stackrel{\$}{\leftarrow} \text{unif}(\{0, 1\}) \{x\}$ states that in expectation the value of $x$ is given by 0.5, when sampled uniformly from $\{0, 1\}$.

Rule (IF) is the mere adaptation of the equivalent classical HL rule. The rule descends into the then- and else-branches, where one can additionally assume that the guard and its negation holds, respectively. Concerning loops, rule (WHILE) requires establishing an invariant $f$ on the loops body. As in classical HL, the invariant needs to be established only on initial memories making the guard evaluate to true. The rule also establishes that the guard evaluates to false after exiting the loop.

The rule (CALL) allows one to use a procedure specification $\{p\} \in \mathcal{C}\{q\}$ to reason about a call-site $x \leftarrow f(E)$. Recall that $p$ and $q$ are parameterized, beside auxiliary variables and global state, by the formal argument and return value of $f$, respectively. The rule adapts these to the call-site, by substituting value of the argument $E$ for the formal argument in $p$, and by identifying the return value of $f$ with that of the assigned variable $x$ within $q$. Dual to (CALL), rule (PROC) establishes that a procedure $\text{proc } f(x) \text{; return } E$ satisfies a specification $\{p\} \in \mathcal{C}\{q\}$. Here, one essentially has to validate that the procedures body $C$; return $E$ adheres to the specification. Following the
<figure><img src="image_5.png" /><figcaption>Fig. 4. Integration of Relational Hoare Logic</figcaption></figure>

semantics of procedure calls, the pre-condition $m_l = m_l^0[x/m \times]$ permits one to restrict attention to memories whose local variables are initialised by $m_l^0$, apart from the formal argument $x$ which ranges over an arbitrary value. This completes the definition of all structural rules.

The final two logical rules deal with auxiliary variables and approximate reasoning, through a rule of consequence. A natural candidate for the latter is the rule we have seen in Section 3, corresponding to the law of monotonicity in pre-expectation transformers [McIver and Morgan 2005]. Alas, ignoring extra variables, the rule is too weak and its addition alone would render our logic incomplete. Rather, our rule (CONSEQ) is an embodiment of the one of Nipkow [2002b] which is strictly more powerful in the presence of local variables. Observe how the additional premise is just enough to lift validity $\vdash_{Z'} \{f'\} C \{g'\}$ of the premise to that of the conclusion. Although a bit cumbersome, its generality allows one to derive various rules more useful in practice, such as the simple rule from Section 3. It also encompasses book-keeping rules on auxiliary variables such as the instantiation, or substitution, rule

$$ \frac{\vdash_Z \{f\} C \{g\}}{\vdash_{Z'} \{f[z/t]\} C \{g[z/t]\}} \quad [\text{INST}] $$

where $t$ is itself an expression over $Z'$.

The final rule (NMOD) captures the observation that if a variable is not touched by statement C, it remains constant through evaluation, and can thereby be regarded as an auxiliary variable. In the rule, Mod_C denotes the set of variables modified by $C \in \text{Stmt.}^7$ The rule gives a mean to internalise the local memory across procedure calls, indispensable in our setup since procedure specifications reference only global memories. This rule, together with the rule of consequence is powerful enough to derive e.g. a framing rule based on Jensen's inequality. We elaborate more on that in Section 8.

**THEOREM 5.2 (SOUNDNESS AND COMPLETENESS).** For all procedures $f$,

$$ \vdash_Z \{p\} f \{q\} \quad \Leftrightarrow \quad \vdash_{Z'} \{p\} f \{q\} $$

The proof is this theorem is given in the appendix.

*Relational Reasoning.* Formally reasoning about the complexity of intricate programs can be very hard. However, complexity can often be studied on *simplified* (but complexity preserving) versions of the original programs with much less burden. *Probabilistic relational Hoare logic* (pRHL for short) allows one to formally relate two programs that behave the same [Barthe et al. 2015, 2012, 2017]. Judgments have the following form:

$$ \vdash \{P\} C \sim D \{Q\}, $$

where $P, Q \subseteq \text{Mem} \times \text{Mem}$ are both assertions that relate memories of C and D. The intuitive meaning behind this judgment is that, when programs C and D are run on initial memories related by P, the resulting output-distributions are coupled via relation Q. Probabilistic coupling is formalised via the notion of *relational lifting* of Q to a relation $Q^\dagger$: $D(\text{Mem}) \times D(\text{Mem})$. Precisely, $d_1 Q^\dagger d_2$ iff there exists a (sub)distribution $d \in D(\text{Mem} \times \text{Mem})$ such that (i) the marginal (sub)distributions

<footnote n="7">⁷ To be precise, a variable $x$ is modified by $C$ if $m \times \neq m'$ for some initial memory $m$ and final memory $m' \in \text{supp}(\llbracket C \rrbracket_m)$.</footnote>
<figure><img src="image_6.png" /><figcaption>Fig. 5. Several representations of skip lists over elements $[1, ..., 6]$. Figure (a) depicts a perfectly balanced skip list. Figure (b) depicts the dictionary $\{1 \mapsto a, ..., 6 \mapsto f\}$ implemented on top of a (random) skip list. The search path for value c with key 3 is indicated as a solid green arrow. Figure (c) is obtained from (b) by inserting an element with key 3.5, with a sampled height of $ht = 5$. The dotted green arrow indicates the search path followed by insert(3.5, z) to determine the position of the new node, it is identical to the path from (b). The search path array sp is outlined with thick green borders, note that it is given by those nodes on the search path where search proceeded downwards. The bended thick blue arrows indicate new pointers.</figcaption></figure>

of $d$ are $d_1$ and $d_2$; and (ii) $\text{supp}(d) \subseteq Q$. We are now ready to state the definition of validity of a pRHL judgment:

**Definition 5.3 (Validity of pRHL Judgments).** Judgment $\vdash \{P\} C \sim C' \{Q\}$ is valid, in notation $\vdash \{P\} C \sim C' \{Q\}$, if for all memories $m_1, m_2 \in \text{Mem}$ such that $m_1 P m_2$, then $[[C]]_{m_1}, Q^\dagger [[C')]_{m_2}$.

The proof system underlying pRHL is extensively described in the literature [Barthe et al. 2015, 2012, 2017]. Noteworthy, an implementation is available in EasyCrypt. Here, the notion of validity is sufficient to relate eHL with pRHL. Indeed, we would like to transfer eHL properties from one program $C'$ to a potentially more complex one $C$. The rule in Figure 4 allows for just that. Concerning post-expectations, the second side-condition is sufficient to establish $\mathbb{E}_d[g] \le \mathbb{E}_{d'}[g']$ for any coupling $d Q^\dagger d'$. Through the pRHL judgement, this holds in particular for the output distributions of $C$ and $C'$, on any pair of initial memories $m$ and $m'$ related by $P$. The first side-condition now essentially demands that each initial $m$ of $C$ can be paired with a memory $m'$ of $C'$ related through $P$, but also through the pre-expectations. From here, soundness is not difficult to establish.

**PROPOSITION 5.4. Rule (PRHL) is sound.**

# 6 AVERAGE CASE COMPLEXITY OF SKIP LISTS

In this section, we demonstrate the flexibility of our framework via a complexity analysis of the *skip list* data structure. Skip lists have been introduced in [Pugh 1990b] as a randomized alternative to balanced binary trees that is easier to implement and maintain.<fnref n="8" /> Being a probabilistic data structure, their formal average case complexity analysis is intricate. A skip list can be thought of as an ordered linked list, where nodes may have additional forward pointers skipping several nodes ahead so as to facilitate a more efficient search. Forward pointers are organised in levels, each level skipping ahead (ideally) half of the nodes found in the level below. By introducing $\log_2(n)$ levels for a list of $n$ elements, search becomes effectively a $O(\log_2(n))$ operation. For illustration, Figure 5a shows a (perfectly balanced) skip list with three levels of forward pointers, organized as a stack above keys. Element $-\infty$ and $+\infty$, acting as head and terminator of the list, respectively.

Maintaining perfect balance of forward pointers when elements are inserted or deleted is a costly operation. In a skip list, forward pointers are chosen at random, so that when inserting a node, it

<footnote n="8">⁸In quote “Skip lists are a probabilistic data structure that seem likely to supplant balanced trees as the implementation method of choice for many applications. Skip list algorithms have the same asymptotic expected time bounds as balanced trees and are simpler, faster and use less space.” [Pugh 1990a].</footnote>
<table><caption>Fig. 6. Skip list implementation of insertion and search, its height abstraction and final cost function. In (c), $n \triangleq \text{size(keys)}$, $m \triangleq \text{size(uniq\_decr(keys(lst)))}$, and $\delta$ is the geometric distribution with parameter $1/2$. In the invariant attributed to the loop, $\phi \triangleq 0 \le \text{len} \wedge \neg \text{len} \le 1 < \text{h} \wedge 1 \le \text{h} \wedge 0 \le n$; and $\Delta_{\ell}(n) \triangleq \log_2(n+1) - \ell$ if $\ell \le \lfloor \log_2(n+1) \rfloor$ and $\Delta_{\ell}(n) \triangleq \frac{n}{2^{\ell-1}}$ otherwise.</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>var ct;</td><td>var hts;</td><td>//2 · log<sub>2</sub>(size(lst) + 1) + 4</td></tr><tr><td>var nodes;</td><td>proc path_len_to(k)</td><td>//2 · log<sub>2</sub>(size(lst) + 1) + 4</td></tr><tr><td>proc find(k)</td><td>keys ← decr(keys(hts));</td><td>//(*)</td></tr><tr><td>(p, lvl) ← (ptr<sub>-∞</sub>, height(ptr<sub>-∞</sub>));</td><td>(len, l) ← (0, -1);</td><td>//Δ<sub>I</sub>(m) + Δ<sub>0</sub>(m) - 1</td></tr><tr><td>while 0 ≤ lvl do</td><td>while keys ≠ nil do</td><td>(len, l, h) ← (0, -1, 1);</td></tr><tr><td>q ← get_fwd(p, lvl);</td><td>:::keys ← keys;</td><td>keys ← decr_uniq(keys(lst));</td></tr><tr><td>if k &lt; get_key(q)</td><td>if l &lt; hts[k] ∧ head(keys) ≤ k</td><td>//φ | len + (h - 1 - l) + Δ<sub>h</sub>(n) + Δ<sub>I+1</sub>(n)</td></tr><tr><td>then lvl-- else p ← q;</td><td>then</td><td>while keys ≠ nil do</td></tr><tr><td>ct++</td><td>len ← len + hts[k] - 1;</td><td>// keys ≠ nil ∧ φ | len + (h - 1 - l) + Δ<sub>h</sub>(n) + Δ<sub>I+1</sub>(n)</td></tr><tr><td>if get_key(p) = k</td><td>l ← hts[k] - 1</td><td>:::keys ← keys;</td></tr><tr><td>then return get_data(p)</td><td>return (len + (hts[-∞] - 1) - 1)</td><td>//φ | len + (h - 1 - l) + Δ<sub>h</sub>(n) + Δ<sub>I+1</sub>(n + 1)</td></tr><tr><td>else return null</td><td>proc insert_h(k, hk)</td><td>//(*<sub>2</sub>)</td></tr><tr><td>proc insert(k, d, hk)</td><td>if k ∈ dom(hts) then skip</td><td>//E<sub>δ</sub> | λhk.</td></tr><tr><td>(spf, k') ← find_path(k);</td><td>else</td><td>φ | len + (max(h, hk + 1) - 1 - l) + Δ<sub>max(h, hk+1)</sub>(n)</td></tr><tr><td>if k = k' then set_data(k', d)</td><td>hts[k] ← hk;</td><td>+ if l &lt; hk ∧ head(keys) then</td></tr><tr><td>else</td><td>hts[-∞] ← max.hts[-∞], hk;</td><td>Δ<sub>hk+1</sub>(n) + 1 else Δ<sub>I+1</sub>(n)</td></tr><tr><td>wd ← new_array(hk, ptr<sub>+∞</sub>);</td><td></td><td>hk ← $ geo(1/2) + 1;</td></tr><tr><td>q ← fresh_ptr();</td><td></td><td>h ← max(h, hk);</td></tr><tr><td>h ← height(ptr<sub>-∞</sub>);</td><td></td><td>//φ | len + (h - 1 - l) + Δ<sub>h</sub>(n) + if l &lt; hk ∧ head(keys) then</td></tr><tr><td>for k = 0 to min(h, hk) - 1 do</td><td></td><td>Δ<sub>hk+1</sub>(n) + 1 else Δ<sub>I+1</sub>(n)</td></tr><tr><td>wd[k] ← get_fwd(spf[k], k);</td><td></td><td>hk ← $ geo(1/2) + 1;</td></tr><tr><td>set_fwd(spf[k], k, q)</td><td></td><td>len ← len + hk - 1;</td></tr><tr><td>set_ptr(q, node(k, d,wd));</td><td></td><td>l ← hk - 1</td></tr><tr><td>set_fwds(ptr<sub>-∞</sub>, [h..hk - 1], q);</td><td></td><td>//φ | len + (h - 1 - l) + Δ<sub>h</sub>(n) + Δ<sub>I+1</sub>(n)</td></tr><tr><td>proc from_list(lst)</td><td>proc from_list_h(keys)</td><td>//(*<sub>3</sub>)</td></tr><tr><td>nodes ← empty();</td><td>hts ← {-∞ ↦ 1; +∞ ↦ 0};</td><td>return len + (h - 1 - l)</td></tr><tr><td>while lst ≠ nil do</td><td>while keys ≠ nil do</td><td>//0 ≤ res | res</td></tr><tr><td>(k, d) ::lst ← lst;</td><td>k::keys ← keys;</td><td></td></tr><tr><td>hk ← $ geo(1/2) + 1;</td><td>hk ← $ geo(1/2) + 1;</td><td></td></tr><tr><td>insert(k, d, hk)</td><td>insert_h(k, hk)</td><td></td></tr><tr><td>proc find_cost(lst, k)</td><td>proc find_cost_h(lst, k)</td><td></td></tr><tr><td>from_list(lst);</td><td>from_list(keys(lst));</td><td></td></tr><tr><td>ct ← 0; find(k);</td><td>ct ← path_len_to(k);</td><td></td></tr><tr><td>return ct</td><td>return ct</td><td></td></tr></tbody></table>

is assigned a forward pointer at level $l + 1$ with a certain probability $p$, in case there is a forward pointer also on level $l$. For $p = 1/2$ (the standard case, which we fix below for simplicity), this means that level $l+1$ will have around half the nodes of level $l$; maintaining a balancing of forward pointers similar to that of the perfectly balanced case in the common case. This almost perfect balancing is precisely the reason why skip lists have good complexity properties, on average.

## 6.1 A Dictionary Implementation on Top of Skip Lists

Dictionaries are prime examples of data structures implemented on top of skip lists. Figure 6a shows such an implementation, for brevity we consider only search and insertion. This implementation maintains an explicit, global memory nodes of nodes `node` (key, data, `wd`), consisting of a key key, a datum data and an array of forward pointers `wd`. We assume keys are equipped with a partial order. As indicated above, we always assume the presence of two nodes with minimal key $-\infty$ and maximal key $+\infty$. As in the quickselect example, a global counter `ct` is used to measure costs.

**Search.** The procedure `find(k)` implements lookup of a datum `d` associated to `k`, returning `null` if no such datum can be found. Search proceeds from the top level at $-\infty$, following forward pointers as long as not overshooting, decrementing the level otherwise. Search eventually reaches level `lvl = -1`, and stops at the last entry whose key is still bounded by `k`. Figure 5b illustrates the
search of key 3, highlighting the *search path* traversed by `find(3)`. The implementation increments the cost counter `ct`, whenever a comparisons of `keys`—`k` < `get_key(q)`—is performed. Observe how this cost measure is directly related to the length of the search path.

*Insertion*. Inserting a datum `d` with key `k` involves finding first the location for the given `k`, and linking a new node within skip list in case the key `k` is not present. Figure 5c illustrates insertion of a datum `z` with unoccupied key 3.5. The size of the array of forward pointers `fwd` is drawn at random. Pre-existing pointers that would “skip through the new column” are separated in two, pointing now to and from the new node, respectively. Finally, the forward pointers of $-\infty$ are extended, in case insertion increases the maximal level, as in the Figure. The full implementation of insertion is given by procedure `proc insert(k, d)` in Figure 6a. It uses a variation `find_path` of `find` that returns an array `spf` of forward pointers on the search path where search took a downward turn—those that will link to a newly inserted entry—together with the key `k'` where search terminated. Insertion incurs no cost, as we will be interested in the complexity of search.

*Average search complexity*. In what follows, we outline our formalization on the *search complexity*—the number of comparisons performed within a search—of skip lists. To this end, our starting point is the function `find_cost(lst, k)` which searches for key `k` in a skip list, built from the provided list of key/value pairs `lst`. The procedure returns the cost counter, storing the number of comparisons performed by `find`. Since the skip list is constructed at random through the implementation of `insert`, the expectation of the return value `ct` reflects precisely the average search complexity.

## 6.2 Outline of the Formalization

*Height abstraction*. Since pointers in a skip list always point forward to the first node of sufficient height, the structure of a skip list is fully determined by the height of nodes, i.e. the size of their array of forward pointers. This, in turn, justifies to abstract nodes by their height, specifically, we have the following mapping in mind:

$$ \text{hts}(\text{nodes}) \triangleq \{k \mapsto \text{size}(\text{fwd}) \mid p \in \text{dom}(\text{nodes}), \text{nodes}(p) = \text{node}(k, d, \text{fwd})\} $$

As `insert` is mostly concerned with managing the pointer structure after update, this abstraction considerably simplifies its implementation, see Figure 6b. Correctness of this abstraction is justified by the (classical) Hoare judgment<fnref n="9" />

$$ \vdash_{\text{HL}} \{ \text{wf}(\text{nodes}) \wedge \text{hs} = \text{hts}(\text{nodes}) \} \text{insert}(k, d, hk) \{ \text{wf}(\text{nodes}) \wedge \text{hts} = \text{upd}(\text{hs}, k, hk) \} \quad \text{(insert_spec)} $$

where `upd(hs, k, hk)` updates the height of `k` to `hk` in `hs` only in the case when $k \notin \text{dom}(hs)$. The predicate `wf(nodes)` collects several well-formedness conditions expressing that nodes forms a skip list (eg, keys are ordered, pointers reference the first larger key, etc). Reasoning inductively, this auxiliary result establishes the following correspondence:

$$ \vdash \begin{array}{l} \{ \text{keys}(\text{lst}^{(1)}) = \text{keys}^{(2)} \} \\ \text{from_list}(\text{lst}) \sim \text{from_list}_h(\text{keys}) \\ \{ \text{wf}(\text{nodes}^{(1)}) \wedge \text{hts}(\text{nodes}^{(1)}) = \text{hts}^{(2)} \} \end{array} \quad \text{(equiv_from_list)} $$

As we have alluded to already above, the search complexity corresponds to the length of the search path. Formally, this statement is expressed by the (classical) Hoare triple

$$ \vdash_{\text{HL}} \{ \text{wf}(\text{nodes}) \wedge \text{cost} = \text{ct} \} \text{find}(k) \{ \text{ct} = \text{cost} + \text{path_len}(\text{hts}(\text{nodes}), k) \} \quad \text{(find_spec)} $$

<footnote n="9">⁹Here and below, we denote Hoare judgments that should be interpreted in the classical sense by $\vdash_{\text{HL}} \{ \phi \} \subset \{ \psi \}$. We have also done a similar judgment establishing the functional correctness of the data part, i.e that the skip list data structure can be used as a dictionary.</footnote>
where cost refers to the value of the cost counter before execution, and where path_len(hts, k) expresses the length of the search path to key k. It is worth mentioning that the proof of this judgment depends crucially on wf nodes. For instance, would nodes contain a cycle, find(k) would potentially loop and no bound on ct could be derived. This explains why we have proven preservation of well-formedness—in essence functional correctness—of insertion. Indeed, this turned out to be the most delicate part in the proof of (equiv_from_list).

By (find_spec), to analyze the search complexity it is sufficient to bound the length of the search path path_len(hts nodes), k), which in turn is computable within the abstraction. The procedure path_len_to(k), given in Figure 6b, gives an explicit definition of the search path length. To give some intuition about the definition, reconsider the search path for key k = 3 depicted in Figure 5b. The procedure starts by scanning keys in reverse-order, pictorially from right to left, until it reaches head(keys) = 3. From now on, the procedure traverses the search path in reverse-order, starting at level 1 = -1. Observe that search reaches a new key always through the top-most incoming forward pointer. Correspondingly, the backward traversal moves up by raising the level 1 to the maximal level and by incrementing the length len of the path traversed so far, accounting for the upward moves and the move to the left. From here, the procedure iterates. In the example, at key 3 the procedure moves this way to level 1 = 1 advancing len = 0 to len = 3, accounting for the upward two moves and the move to the left. The procedure then iterates, to key 2, skipping along key 1 not on the search path (due to the condition 1 < hts[k]), until finally arriving at -∞. The final increment in the return statement accounts for the final move upwards on key -∞, in the example from level 2 to level 3. With this intuition in mind, functional correctness

$$ \vdash_{HL} \{ \text{hs} = \text{hts} \} \text{path\_len\_to}(k) \{ \text{res} = \text{path\_len}(\text{hs}, k) \} \quad (\text{path\_len\_to\_spec}) $$

is easily provable in classical Hoare logic. Summing up, the following relational Hoare judgment state correctness of the abstraction with respect to search complexity.

$$ \vdash \{ \text{lst}^{(1)} = \text{lst}^{(2)} \wedge \text{k}^{(1)} = \text{k}^{(2)} \} \text{find\_cost}(\text{lst}, k) \sim \text{find\_cost\_h}(\text{lst}, k) \{ \text{res}^{(1)} = \text{res}^{(2)} \} \quad (\text{equiv\_find\_cost\_h}) $$

It is a direct consequence of (equiv_from_list), (find_spec) and (path_len_to_spec).

*Estimation of the path length through the height abstraction.* The judgment (equiv_find_cost_h) formally justifies that we analyze the search complexity through its height abstraction given in Figure 6b. The crux in proving the latter directly is to find a suitable upper invariant for the loop in from_list_h. In effect, this requires expressing the search path length after inserting a column, in terms of of the search path length before the insertion. At the same time, this invariant has to lead to a sufficiently tight bound in the size of keys. However, this technicality can be avoided altogether, by sampling hts on-demand, rather than eagerly. The procedure find_cost_d, given in Figure 6c, is obtained by inlining path_len_to within find_cost_d from Figure 6b. Heights hk corresponding to hts[k] are sampled on demand-within the path traversal, rendering the call to from_list_h obsolete. The auxiliary variable h refers to the maximal sampled height, viz. the height of -∞. One can prove that semantically, find_cost_h and find_cost_d coincide:

$$ \vdash \{ \text{lst}^{(1)} = \text{lst}^{(2)} \wedge \text{k}^{(1)} = \text{k}^{(2)} \} \text{find\_cost\_h}(\text{lst}, k) \sim \text{find\_cost\_d}(\text{lst}, k) \{ \text{res}^{(1)} = \text{res}^{(2)} \} \quad (\text{equiv\_find\_cost\_d}) $$

Notice that the left program inserts keys in the order they occur in lst, whereas the right program processes keys in reverse-sorted order, removing duplicates. Thus, a rather involved key step towards this equivalence is proving that path length is independent of the order of insertions.
Final cost analysis via eHL. The judgments (equiv_find_cost_h) and (equiv_find_cost_d) establish

$$ \vdash \{ \text{lst}^{(1)} = \text{lst}^{(2)} \wedge \text{k}^{(1)} = \text{k}^{(2)} \} \text{find_cost}(\text{lst}, \text{k}) \sim \text{find_cost_d}(\text{lst}, \text{k}) \{ \text{res}^{(1)} = \text{res}^{(2)} \} \quad (\text{equiv\_find\_cost}) $$

witnessing that the complexity of searching for a key k in an arbitrary skip list build from lst is computed by find_cost_d (lst, k). The final puzzle piece lies now in bounding this result, in expectation. To this end, we make use of eHL, compare the assertions in Figure 6c. The gist of the proof lies in finding an invariant for the loop. As the definition and the related weakening proofs are quite technically involved, we have relegated further discussion to the Appendix. Very briefly, terms $\Delta_h(n)$ and $\Delta_{l+1}(n)$ are used to account for changes to the path length, through vertical and horizontal steps, respectively. Concerning horizontal steps for instance, in the common case where the current height h does not exceed the (average) logarithmic overall height, $\Delta_h(n) = \log_2(\frac{n+1}{2^h})$ measures the expected height increase of completing the loop in terms of the $\frac{n+1}{2^h}$ nodes found at current height h. The invariant turns slightly more complicated, to also account for the final difference $h - 1 - 1$ contributing to the result of the procedure (see weakening $(\star_1)$). Once carried over the initialisation statements (see weakening $(\star_2)$), the invariant gives the final logarithmic bound $2 \cdot \log_2(\text{size}(\text{lst})+1)+4$. Apart from defining the invariant, the most delicate step concerned the proof of the weakening step $(\star_2)$. Towards this proof, we have built a considerable library on laws of expectations, such as the law of linearity, Jensen's inequality, etc.

*Concluding Remarks.* Splitting the correctness proof, done via pRHL, from the complexity analysis, carried on via eHL, seems essential to achieve our goal. The modularity provided by our framework has allowed us to develop the proof step-by-step, in a compositional way, which would not have been possible without the EasyCrypt implementation.

# 7 ADVERSARIES AND APPLICATIONS TO CRYPTOGRAPHIC PROOFS

In this section, we extend our programming language and logic with adversary calls, and illustrate how the extended logic can be used to reason about cryptographic proofs. Our example is inspired from a recent work by [Barbosa et al. 2023], which uses our implementation of eHL for proving security of Dilithium [Ducas et al. 2017], a post-quantum signature scheme recently standardized by the NIST (National Institute of Standards and Technology).

*Extension of the language.* We now extend the language to adversarial code by permitting adversary calls $x \leftarrow \mathcal{A}_o(E)$, where $\mathcal{A}$ is drawn from a set $\text{Adv} = \{\mathcal{A}, \mathcal{B}, \dots\}$ of adversary names. Each adversary call is parameterised by an oracle, i.e., a pre-defined procedure $o \in \text{Fun}$.<fnref n="10" /> Adversaries $\mathcal{A}$ refer to arbitrary procedures, granted only partial access to the global memory through a set $\text{Write}_\mathcal{A} \subseteq \text{GVar}$ of writable global variables. In a call to $\mathcal{A}_o$, the adversary may modify variables outside $\text{Write}_\mathcal{A}$ only by invoking the oracle $o$. To model adversarial code in the semantics, we index the interpretation of program statements by an adversary environment $\gamma$. This environments maps each $\mathcal{A} \in \text{Adv}$ to a declaration

$$ \gamma(\mathcal{A}) = o \mapsto (\text{proc } \mathcal{A}(x) C_o; \text{return } E), $$

indexed by an oracle $o$. Note that the code of the adversary is parametric in the oracle. The body $C_o$ may contain oracle calls $x \leftarrow o(E)$. Invocation of $\mathcal{A}_o$ executes the procedure $\gamma(\mathcal{A})(o) = \text{proc } \mathcal{A}(x) C_o; \text{return } E$, where in the body the meta-variable $o$ has been substituted by the

<footnote n="10">¹⁰In practice, we permit $\mathcal{A}$ to be parameterised by more than one oracle. Here, the restriction helps us avoid notational overhead.</footnote>
<figure><img src="image_7.png" /><figcaption>Fig. 7. Rejection sampling with bad. Variables c, log and bad are global. Here, $0 \le Q$ is a constant, $\delta \triangleq \Pr[\text{sample : test}] > 0$ is the probability of event test on the distribution given by sample, $\Pr[\text{sample : } 1_o] \le \epsilon$ is an upper-bound on the probability of sampling a value $v$; $\phi \triangleq \text{bad} \Rightarrow Q \le c$ and $F \triangleq \epsilon \cdot (\text{size}(\log) + \frac{Q-c}{\delta})$.</figcaption></figure>

provided oracle $o$. We require that adversary environments are consistent with writeable variables, i.e., the body of $\gamma(\mathcal{A})(o)$, nor any of its subprocedures except the oracle $o$, modifies the memory outside of Write$_{\mathcal{A}}$. For instance, if the adversary executes an instruction $x \leftarrow E$, then $x \in \text{Write}_\mathcal{A}$. In contrast to the notion of modified variables Mod$_c$, which is semantic, Write$_\mathcal{A}$ is a syntactic notion with subtle differences. The memory content of a variable $x \notin \text{Write}_\mathcal{A}$ may change during an invocation, but only through invocations of the oracle. The semantics of an adversarial call are now identical to ordinary procedure calls, just, the declaration of the adversary is provided by the adversary environment $\gamma$, that is, we let $\llbracket \mathcal{A}_o \rrbracket^\gamma = \llbracket \gamma(\mathcal{A})(o) \rrbracket$, but treat a call $x \leftarrow \mathcal{A}_o(E)$ otherwise identical to an ordinary procedure call.

Extension of eHL. To extend the logic for programs with adversarial code, the notion of judgment can remain identical, apart from the fact that program statements now may contain adversarial calls. However, judgments will now be valid if validity in the original sense holds independent of the adversarial code, that is, $\vdash_Z \{f\} C \{g\}$ if $\mathbb{E}_{\llbracket c \rrbracket_m}^\gamma [gz] \le fzm$ holds for all $z, m$ and all adversary environments $\gamma$. Similar, validity for procedure declarations is defined by quantifying over all adversary environments.

The following now gives our adversarial rule, for $f: Z \to GMem \to \mathbb{R}^{+\infty}$ depending only on the global memory.

$$ \frac{f \perp \text{Write}_{\mathcal{A}} \quad F = \lambda z (m_g, \_). f z m_g \quad \vdash_Z \{F\} \circ \{F\}}{\vdash_Z \{F\} \mathcal{A}_o \{F\}} \text{[ADV]} $$

This rule lifts invariants on oracles to that of adversaries. The hypothesis $f \perp \text{Write}_{\text{Adv}}$, stating that $f$ is independent of writable variables by the adversary, ensures that $F$ remains invariant throughout complete invocation of the adversary.

**THEOREM 7.1. Rule (ADV) is sound.**

*Example.* We illustrate how eHL can be used to upper bound the probability of bad events in rejection sampling. The example captures the essence of a key step in the security proof of the Dilithium signature scheme, formalized in Barbosa et al. [2023] using our implementation of eHL. Our goal is to provide an upper-bound on the probability that a fresh, random value appears in the history of samplings performed during rejection sampling. This stage of the proof is represented, in slightly simplified form, in Figure 7. Procedure *rsample* (Figure 7a) performs rejection sampling
from distribution **sample** with predicate **test**. The global variable **log** keeps track of all sampled values. Each invocation of the oracle **o**, later provided to the adversary, performs rejection sampling and thereby populates **log**. A global counter **c** keeps track of the number of oracle invocations. Once the counter reaches 0 ≤ **Q**, a bad event is signaled through setting the global variable **bad**, precisely when **log** contains a randomly sampled value **r**\*. The main program (Figure 7c) consists simply of a call to the adversary $\mathcal{A}_o$, with global auxiliary global variables initialised correspondingly. The adversary has access to the global variables only through the oracle, that is, Write $\mathcal{A} = \emptyset$. Our goal is to bind the probability of the Boolean variable **bad**—its expectation—within this program.

Figure 7 is annotated with the corresponding eHL proof. The central proof step lies in annotating the oracle in Figure 7b with an invariant binding the value of bad. Being initialized to **false**, this variable is only set once the invocation counter **c** of the oracle reaches **Q**, and then only when a fresh sampled value **r**\* collides with a previously sampled value in **log**. In turn, the probability of a collision **r**\* ∈ **log** is bounded from above by $\epsilon \cdot \text{size}(|\log|)$, for $\epsilon$ an upper-bound on probabilities of **sample**. This, in effect, allows us to estimate the value of bad in terms of the size of **log** when **c** reaches **Q**. To this end, let $0 < \delta$ be the probability that a sample satisfies the predicate **test**. As indicated in Figure 7a, rejection sampling increases the length of **log**, on average, by $\frac{1}{\delta}$.

The invariant given in the specification (see Figure 7b) lifts this observation to the oracle. In the term $F = \epsilon \cdot (\text{size}(|\log|) + \frac{0-c}{\delta})$, the factor $\epsilon$ stems from the approximation of bad in terms of the size of **log**, the fraction $\frac{0-c}{\delta}$ accounts the potential size increase of **log** until the invocation counter reaches the limit **Q**. Once the counter is reached, the invariant simply refers to the value of bad. The overall program is now treated essentially by an application of the adversary rule, using the invariant on the oracle as provided, see Figure 7c. The weakening at the end follows from the classical invariant $\phi$. The derived bound $\epsilon \cdot \frac{0}{\delta}$ is obtained by simplification of the invariant with global variables initialised correspondingly.

The proof hinges essentially on the fact that, on average, the size of **log** is bounded, although **rsample** is potentially non-terminating and may produce a **log** of arbitrary size. Lacking capabilities for expectation based reasoning, this renders a proof using the phoare logic present in EasyCrypt significantly more involved. The most natural way here is to proceed via an approximation of rejection sampling so that the number of iterations is bounded, say by a constant $K$. Thereby, within the **Q** invocations of the oracle, the size of **log** becomes bounded by $Q \cdot K$, worst case. On the so transformed, certainly terminating, program, one can then obtain a bound $Q \cdot K \cdot \epsilon$ on the probability of bad being set. The approximation itself however, introduces an additional error rate, leading to the overall bound of $Q \cdot K \cdot \epsilon + Q \cdot \delta^K$.

In contrast, the use of eHL not only significantly reduced proof effort, it also lead to a more preferable bound. The complete formal proof in EasyCrypt takes in total only 48 lines. The frame rule (detailed in the next section) turned out particularly useful. It allowed us to lift the specification of **rsample**, talking only about the expected size increase of **log**, to the call within the oracle **o**.

# 8 IMPLEMENTATION

We have implemented eHL in the EasyCrypt proof assistant [Barthe et al. 2013]. EasyCrypt is a natural choice to implement eHL, since it is specially tailored to reason about probabilistic programs. Informally, EasyCrypt combines a proof engine for an ambient higher-order logic (HOL) with several program logics for proving properties of probabilistic programs. Judgments of the program logics are terms of the ambient logic, and proofs in the program logics are carried by means of (proof) tactics. In essence, a tactic implements a rule of the logic, by turning the conclusion into its hypotheses. This way, proofs are build gradually from the conclusion, upwards, ending in the axioms of the logic.
$$
\frac{
  \frac{
    \frac{
      g \le f
    ]^{\text{SKIPEC}}
    \frac{
      \vdash_Z \{f\} C \{g[x/E]\}
    ]^{\text{ASSIGNEC}}
    \frac{
      \vdash_Z \{f\} C \{wp(D, g)\}
    ]^{\text{WPEC}}
  }{
    \frac{
      \vdash_Z \{f\} C \{g\} \quad \forall z v. (\lambda m. F z m v) \perp \mathrm{Mod}_C \quad \forall z m. F z m \text{ concave, non-decreasing}
    ]^{\text{FRAMEEC}}
  }
  \frac{
    \vdash_Z \{p\} f \{q\}
  ]^{\text{CALLEC}}
  \frac{
    \vdash_Z \{f\} C \{\lambda z m. (\forall r \vec{v}. g z m[x/r][\mathrm{Mod}_f/\vec{v}] \le q z (m_g[\mathrm{Mod}_f/\vec{v}], r)) | p z (m_g, [\mathrm{E}]_m)\}
  ]^{\text{CALLEC}}
  \frac{
    \vdash_Z \{f\} C; x \leftarrow f(E) \{g\}
  ]^{\text{CALLEC}}
}{
  \vdash_Z \{f\} skip \{g\}
}
$$

<caption>Fig. 8. Excerpt of derived rules implemented in EasyCrypt.</caption>

In order to support expectation-based reasoning, we have added eHL judgments as assertions of the ambient logic, and built support to reason about such judgments. In particular, we have:

- added tactics for core and several derived eHL rules. The core rules are in the trusted computing base (TCB) of the tool. However, the derived rules are designed to generate sequences of core tactics, in order to minimize the TCB as much as possible;

- added a library to reason about expectations. The library is required to discharge the many ambient logic goals generated by applying eHL tactics.

*Derived proof rules.* The proof rules in Section 5 follow the conventional presentation of program logics but are tedious to use in practice. For instance, reasoning about a sequence of instructions would first require a sequence of applications of rule (SEQ) to split the sequence apart, and then use the syntax-directed rules, possibly combined with non-structural rules, on the individual program instructions. Even more tedious, working towards a triple this way would entail that in many situations the intermediate pre-/post-expectations would need to be supplied by the user, as these cannot be inferred in general. To overcome these complications and to enhance usability of the logic, in the implementation we composing core syntax-directed rules with sequential composition and structural rules. An excerpt of derived rules can be found in Figure 8.

Rules (SKIPEC) is a variation of the ordinary rule (SKIP), combined with rule (CONSEQ) to make it applicable to the usual scenario where pre- and post-expectations differ. Rule (ASSIGNEC), the combination of rules (SEQ) and (ASSIGN), embodies the backward style kind of analysis commonly found across the implementations of different logics in EasyCrypt, close to traditional weakest pre-condition reasoning. Generalising on this idea with rule (WPEC), our implementation provides a tactic wp computing the weakest pre-expectation, wp(D, f), for a tail D neither containing loops nor procedure calls. To illustrate the advantage of these derived rules, note that the proof of rpartition_abs in Figure 1b is completely automated by the tactic wp, apart from the initial weakening step. This would not have been possible otherwise.

Among the more interesting derived rules is the final rule (FRAMEEC). In classical Hoare logic the frame rule, also known as rule of constancy, takes the form

$$
\frac{
  \vdash_{\text{HL}} \{P\} C \{Q\} R \perp \text{Mod}_C
}{
  \vdash_{\text{HL}} \{P \wedge R\} C \{Q \wedge R\}
}
$$

It is indispensable in practice, since it allows one to focus only on the relevant parts of an assertion, namely only the one that is potentially altered by C. But how to transfer this rule to our quantitative logic, in particular, how to translate logical conjunction? Here are three valid rules, all derivable from rules (CONSEQ) and (NMOD):

$$
\frac{
  \vdash_Z \{f\} C \{g\} P \perp \mathrm{Mod}_C
}{
  \vdash_Z \{P | f\} C \{P | g\}
} \quad [\text{FRAME1}]
\frac{
  \vdash_Z \{f\} C \{g\} h \perp \mathrm{Mod}_C
}{
  \vdash_Z \{f \cdot h\} C \{g \cdot h\}
} \quad [\text{FRAME2}]
\frac{
  \vdash_Z \{f\} C \{g\} h \perp \mathrm{Mod}_C
}{
  \vdash_Z \{f + h\} C \{g + h\}
} \quad [\text{FRAME3}]
$$
Rather than imposing a concrete choice, our rule (FRAMEEC) abstracts over the choice, and permits placing pre- and post-expectations in an arbitrary context $F \perp \text{Mod}_C$, that is concave<fnref n="11" /> and non-decreasing (i.e. monotone), when seen as function $F: \mathbb{R}^{+\infty} \to \mathbb{R}^{+\infty}$. For instance, this rule has been applied in the previous section, adapting the function specification of *rsample* to the call site within o (see Figure 7). In the application of the rule, $F$ is given by the context

$$ \phi \mid \text{if } Q < c \text{ then bad } \text{else } \epsilon \cdot (\square + \frac{Q-\epsilon}{\delta}). \quad (\times) $$

Seen as function in the hole $\square$, this term can be proven monotone and concave, as demanded by the third premise in rule (FRAMEEC). Since it mentions only local, unmodified variables, the second premise is easy to discharge. The rule itself is derivable by a composition of (NMOD) and (CONSEQ). To see this, assume $\vdash_Z \{f\} C \{g\}$. Rule (CONSEQ) deduces $\vdash_Z \{F[f]\} C \{F[g]\}$ since $\mathbb{E}_d[F[g]] \le F(\mathbb{E}_d[g]) \le F[f]$ holds for all $m, d$ with $\mathbb{E}_d[g] \le f$. The first inequality effectively imposes concavity of $F$ (it is then a consequence from the reverse Jensen's inequality), the second imposes that $F$ is non-decreasing. Allowing $F$ to depend on part of the memory that is not modified by $C$ explains why the rule relies on (NMOD) to be justified.

To ease the application of the frame rule, we have proven a list of lemmas showing that functions like identity, multiplication by a constant or log satisfy those properties. EasyCrypt is then able to automatically/recursively apply those lemmas to prove the last premises. Furthermore this list of lemmas is user extensible. This way, for instance, EasyCrypt can automatically discharge the premises related to the context $(\times)$ in the proof mentioned above.

The final rule, rule (CALLEC) implemented by tactic call, allows to compute the weakest pre-expectation of a procedure call, given a specification. The specification itself is usually already proven by a lemma in EasyCrypt. It implicitly features an application of rule (FRAMEEC), more precisely its instance (FRAME1) given in the motivation above, to internalise an implicit weakening of the post-expectations within the pre-expectation. This aides usability in connection with wp, which will for instance automatically propagate variable initialisation within the internalised weakening. The tactic call also takes a further context $F$ (adhering to the restrictions imposed by rule (FRAMEEC)) as optional argument, in order to lift a procedure specification directly to its use at a call site.

Last but not least, in addition to these derived rules, we have extended already existing tactics that do not change the semantics of programs to deal with eHL judgments, such as the inline tactic that replaces a procedure call by its body.

*Libraries of extended positive reals and expectations.* We have developed a library to reason about extended positive reals and expectations. The library formalizes the type of positive reals $\mathbb{R}^+$ as a subtype of $\mathbb{R}$ and the type of extended positive reals as a disjoint union of $\mathbb{R}^+$ and $+\infty$. The library establishes that both positive and extended positive reals form additive monoids, which allows to instantiate the EasyCrypt library on big-operators. This library, inspired from [Bertot et al. 2008], provides a wealth of facts to reason about indexed sums—via the mathematical operator $\Sigma$. Using big-operators, it is thus relatively simple to define the notion of expectation, and to prove elementary facts about expectations. These facts are used to discharge many proof obligations automatically. At the time of writing, the library weights in at around 1.100 lines of proof scripts.

# 9 CONCLUSION

We have proposed a proof hopping approach for reasoning about expectation-based properties of (adversarial) probabilistic programs, and extended the EasyCrypt proof assistant to support our approach. In addition, we have shown that our approach is useful for reasoning about expected

<footnote n="11">¹¹i.e. $\forall t, 0 \le t \le 1 \Rightarrow \forall x y, tF(x) + (1-t)F(y) \le F(tx + (1-t)y)$</footnote>
cost of randomized algorithms and for cryptographic proofs. Our implementation of eHL has been integrated into the EasyCrypt proof assistant. Future directions include extending eHL to quantum adversaries and quantum programs, and to further develop and capture formally the use of expectation-based properties in cryptography.

## DATA-AVAILABILITY STATEMENT

The implementation of the logic and case studies are available on Zenodo [Avanzini et al. 2024].

## ACKNOWLEDGMENTS

We would like to thank the anonymous reviewers for their work and invaluable suggestions, which greatly improved our presentation. This work is partly supported by the ANR Project PPS: "Probabilistic Program Semantics" and the Agence Nationale de la Recherche (ANR, French National Research Agency) as part of the France 2030 programme – ANR-22-PECY-0006. Further it is partly supported by the FWF Project AUTOSARD: "Automated Sublinear Amortised Resource Analysis of Data Structures".

## REFERENCES

S. Agrawal, K. Chatterjee, and P. Novotný. 2018. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. PACMPL 2, POPL (2018), 34:1–34:32. https://doi.org/10.1145/3385412.3386002

Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, and Gabriele Vanoni. 2024. ehoare.tar.gz. https://doi.org/10.5281/zenodo.10517828

Martin Avanzini, Gilles Barthe, and Ugo Dal Lago. 2021. On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473592

M. Avanzini, U. Dal Lago, and A. Ghyselen. 2019. Type-Based Complexity Analysis of Probabilistic Functional Programs. In Proc. of 34th LICS. IEEE, 1–13. https://doi.org/10.1109/LICS.2019.8785725

M. Avanzini, U. Dal Lago, and A. Yamada. 2020a. On Probabilistic Term Rewriting. SCP 185 (2020), 102338. https://doi.org/10.1016/j.scico.2019.102338

Martin Avanzini, Georg Moser, and Michael Schaper. 2020b. A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4, OOPSLA (2020), 172:1–172:30. https://doi.org/10.1145/3428240

Martin Avanzini, Georg Moser, and Michael Schaper. 2023. Automated Expected Value Analysis of Recursive Programs. Proc. ACM Program. Lang. 7, PLDI (2023), 1050–1072. https://doi.org/10.1145/3591263

Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, and Xiaodi Wu. 2023. Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. In Advances in Cryptology - CRYPTO 2023 - 43rd Annual International Cryptology Conference, CRYPTO 2023, Santa Barbara, CA, USA, August 20-24, 2023, Proceedings, Part V (Lecture Notes in Computer Science, Vol. 14085), Helena Handschuh and Anna Lysyanskaya (Eds.). Springer, 358–389. https://doi.org/10.1007/978-3-031-38554-4_12

Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, and Pierre-Yves Strub. 2021. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. In CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, Yongdae Kim, Jong Kim, Giovanni Vigna, and Elaine Shi (Eds.). ACM, 2541–2563. https://doi.org/10.1145/3460120.3484548

Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. 2013. EasyCrypt: A Tutorial. In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures (Lecture Notes in Computer Science, Vol. 8604), Alessandro Aldini, Javier López, and Fabio Martinelli (Eds.). Springer, 146–166. https://doi.org/10.1007/978-3-319-10082-1_6

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing Probabilistic Invariants via Doob's Decomposition. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 9779), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer, 43–61. https://doi.org/10.1007/978-3-319-41528-4_3

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. 2015. Relational Reasoning via Probabilistic Coupling. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9450), Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.). Springer, 387–401. https://doi.org/10.1007/978-3-662-48899-7_27
G. Barthe, B. Grégoire, and S. Z. Béguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Proc. of 36th *POPL*. ACM, 90–101. https://doi.org/10.1145/1480881.1480894

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In *Mathematics of Program Construction - 11th International Conference, MPC 2012, Madrid, Spain, June 25-27, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7342)*, Jeremy Gibbons and Pablo Nogueira (Eds.). Springer, 1–6. https://doi.org/10.1007/978-3-642-31113-0_1

Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Coupling proofs are probabilistic product programs. In Proc. of 44th POPL, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 161–174. https://doi.org/10.1145/3009837.3009896

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Lena Verscht. 2023. A Calculus for Amortized Expected Runtimes. Proc. ACM Program. Lang. 7, POPL (2023), 1957–1986. https://doi.org/10.1145/3571260

Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. 2008. Canonical Big Operators. In *Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 5170)*, Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.). Springer, 86–101. https://doi.org/10.1007/978-3-540-71067-7_11

O. Bournez and F. Garnier. 2005. Proving Positive Almost-Sure Termination. In Proc. of 16th RTA (LNCS, Vol. 3467). Springer, 323–337. https://doi.org/10.1142/S0129054112400588

A. Chakarov and S. Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Proc. of 25th CAV (LNCS, Vol. 8044). Springer, 511–526. https://doi.org/10.1007/978-3-642-39799-8_34

K. Chatterjee, H. Fu, and A. Murhekar. 2017. Automated Recurrence Analysis for Almost-Linear Expected-Runner Bounds. In Proc. of 29th CAV (LNCS, Vol. 10426). Springer, 118–139. https://doi.org/10.1007/978-3-319-63387-9_6

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. *Introduction to Algorithms*, 3rd Edition. MIT Press.

Láo Ducas, Eike Kiltz, Tancrède Lepoint, Vadim Lyubashevsky, Peter Schwabe, Gregor Seiler, and Damien Stehlé. 2017. CRYSTALS–Dilithium: Algorithm Specification and Supporting Documentation. Round-1 submission to the NIST Post-Quantum Cryptography Standardization Project. https://cryptojedi.org/papers/#dilithium.

Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow. 2020. Verified Analysis of Random Binary Tree Structures. *J. Autom. Reason*. 64, 5 (2020), 879–910. https://doi.org/10.1007/s10817-020-09545-0

Maximilian Paul Louis Haslbeck. 2021. *Verified Quantitative Analysis of Imperative Algorithms*. Ph. D. Dissertation. Technische Universität München.

Max W. Haslbeck and Manuel Eberl. 2020. Skip Lists. *Arch. Formal Proofs* 2020 (2020). https://www.isa-afp.org/entries/Skip_Lists.html

C. A. R. Hoare. 1961. Algorithm 65: find. *Commun. ACM* 4, 7 (1961), 321–322. https://doi.org/10.1145/366622.366647

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. *Commun. ACM* 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259

Joe Hurd, Annabelle McIver, and Carroll Morgan. 2004. Probabilistic Guarded Commands Mechanized in HOL. In *Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages, QAPL 2004, Barcelona, Spain, March 27-28, 2004 (Electronic Notes in Theoretical Computer Science, Vol. 112)*, Antonio Cerone and Alessandra Di Pierro (Eds.). Elsevier, 95–111. https://doi.org/10.1016/j.entcs.2004.01.021

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proc. of 42nd POPL, Sriram K. Rajamani and David Walker (Eds.). ACM, 637–650. https://doi.org/10.1145/2676726.2676980

B. L. Kaminski, J.-P. Katoen, C. Matheja, and F. Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. *JACM* 65, 5 (2018), 30:1–30:68. https://doi.org/10.1145/3208102

Thomas Kleymann. 1998. *Hoare logic and VDM : machine-checked soundness and completeness proofs*. Ph. D. Dissertation. University of Edinburgh, UK. http://hdl.handle.net/1842/387

Thomas Kleymann. 1999. Hoare Logic and Auxiliary Variables. Formal Aspects Comput. 11, 5 (1999), 541–566. https://doi.org/10.1007/s001650050057

Donald Knuth. 1973. *The Art Of Computer Programming, vol. 3: Sorting And Searching*. Addison-Wesley.

D. Kozen. 1985. A Probabilistic PDL. *J.CSC* 30, 2 (1985), 162–178. https://doi.org/10.1016/0022-0000(85)90012-1

Peter Lammich and Thomas Tuerk. 2012. Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm. In *Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7406)*, Lennart Beringer and Amy P. Felty (Eds.). Springer, 166–182. https://doi.org/10.1007/978-3-642-32347-8_12

Lorenz Leutgeb, Georg Moser, and Florian Zuleger. 2022. Automated Expected Amortised Cost Analysis of Probabilistic Data Structures. In Proc. of 34th CAV (LNCS, Vol. 13372). 70–91. https://doi.org/10.1007/978-3-031-13188-2_4
Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay. 2010. Automatic numeric abstractions for heap-manipulating programs. In *Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010*, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 211–222. https://doi.org/10.1145/1706299.1706326

Annabelle McIver and Carroll Morgan. 2005. *Abstraction, refinement and proof for probabilistic systems*. Springer Science & Business Media.

Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic Predicate Transformers. *ACM Trans. Program. Lang. Syst.* **18**, 3 (1996), 325–353. https://doi.org/10.1145/229542.229547

N. C. Ngo, Q. Carbonneaux, and J. Hoffmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In *Proc. of 39th PLDI*. ACM, 496–512. https://doi.org/10.1145/3296979.3192394

Tobias Nipkow. 2002a. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In *Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings (Lecture Notes in Computer Science, Vol. 2471)*, Julian C. Bradfield (Ed.). Springer, 103–119. https://doi.org/10.1007/3-540-45793-3_8

Tobias Nipkow. 2002b. *Hoare Logics in Isabelle/HOL*. Springer Netherlands, Dordrecht, 341–367. https://doi.org/10.1007/978-94-010-0413-8_11

Tobias Nipkow, Manuel Eberl, and Maximilian P. L. Haslbeck. 2020. Verified Textbook Algorithms - A Biased Survey. In *Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings (Lecture Notes in Computer Science, Vol. 12302)*, Dang Van Hung and Oleg Sokolsky (Eds.). Springer, 25–53. https://doi.org/10.1007/978-3-030-59152-6_2

Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Annabelle McIver. 2018. Conditioning in Probabilistic Programming. *ACM Trans. Program. Lang. Syst.* **40**, 1 (2018), 4:1–4:50. https://doi.org/10.1145/3156018

F. Olmedo, B. L. Kaminski, J.-P. Katoen, and C. Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In *Proc. of 31st LICS*. ACM, 672–681. https://doi.org/10.1145/2933575.2935317

William Pugh. 1990a. *Concurrent Maintenance of Skip Lists*. Technical Report. USA. http://hdl.handle.net/1903/542

William Pugh. 1990b. Skip Lists: A Probabilistic Alternative to Balanced Trees. *Commun. ACM* **33**, 6 (1990), 668–676. https://doi.org/10.1145/78973.78977

T. Takisaka, Y. Oyabu, N. Urabe, and I. Hasuo. 2018. Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs. In *Proc. of 16th ATVA (LNCS, Vol. 11138)*. Springer, 476–493. https://doi.org/10.1007/978-3-030-01090-4_28

Joseph Tassarotti and Robert Harper. 2018. Verified Tail Bounds for Randomized Programs. In *Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FLOC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10895)*, Jeremy Avigad and Assia Mahboubi (Eds.). Springer, 560–578. https://doi.org/10.1007/978-3-319-94821-8_33

Joseph Tassarotti and Robert Harper. 2019. A separation logic for concurrent randomized programs. *Proc. ACM Program. Lang.* **3**, POPL (2019), 64:1–64:30. https://doi.org/10.1145/3290377

Eelis Van der Weegen and James McKinna. 2008. A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq. In *Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 5497)*, Stefano Berardi, Ferruccio Damiani, and Ugo de'Liguoro (Eds.). Springer, 256–271. https://doi.org/10.1007/978-3-642-02444-3_16

Di Wang, David M. Kahn, and Jan Hoffmann. 2020. Raising expectations: automating expected cost analysis with types. *PACM on Programming Languages* **4**, ICFP (2020), 110:1–110:31. https://doi.org/10.1145/3408992

P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In *Proc. of 40th PLDI*. ACM, 204–220. https://doi.org/10.1145/3314221.3314581

Received 18-OCT-2023; accepted 2024-02-24