$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$s
always reduce uniformly at random and only labeled sampling statements will
read from presampling tapes which prevents us from proving the unsound 7.1.

Besides motivating why soundly allowing presampling is subtle, this
counterexample also emphasizes why the fact that labels appear in the program
and in the program syntax is important. We do not claim that these annotations
are absolutely necessary for some kind of presampling to be sound, as some
very different formulation of the logic might be able to avoid them, but like
for _prophecy variables_ (Jung et al., 2020) where similar “ghost information”
is needed in the actual program code, it is not obvious how to do without it.
We remind the reader that presampling tapes nevertheless remain a proof-device
as tapes can be erased through refinement as discussed in § 2.

###  7.2. Incompatibility with prophecy variables

Presampling tapes bear _some_ resemblance to prophecy variables in that they
give us the means to talk about the future. However, prophecy variables, as
previously developed in the context of Iris (Jung et al., 2020), are unsound
for the (synchronous) coupling logic as illustrated below.

Assume the existence of two operators
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{NewProph}}}$
and
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{Resolve}}}p\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{to}}}b$
in our programming language and their (unsound for Clutch!) Hoare-triple
specifications found below.

wp-newproph-unsound
$\displaystyle\displaystyle{\left\\{\mathsf{True}\right\\}}\nobreak\hskip
1.99997pt plus
1.00006pt\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{NewProph}}}\nobreak\hskip
1.99997pt plus 1.00006pt{\left\\{p.\exists
b\in\mathbb{B}.\operatorname{\mathsf{Proph}}(p,b)\right\\}}$ wp-resolve-
unsound
$\displaystyle\displaystyle{\left\\{\operatorname{\mathsf{Proph}}(p,b)\ast
b^{\prime}\in\mathbb{B}\right\\}}\nobreak\hskip 1.99997pt plus
1.00006pt\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{Resolve}}}p\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{to}}}b^{\prime}\nobreak\hskip
1.99997pt plus 1.00006pt{\left\\{b=b^{\prime}\right\\}}$

The specifications give us access to _Boolean one-shot prophecies_ (Jung et
al., 2020).
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{NewProph}}}$
allocates a fresh prophecy variable $p$ and a resource
$\operatorname{\mathsf{Proph}}(p,b)$ that tracks its future resolution $b$.
Given ownership of $\operatorname{\mathsf{Proph}}(p,b)$ then
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{Resolve}}}p\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{to}}}b^{\prime}$
resolves the prophecy variable $p$ to a value $b^{\prime}$ and knowledge that
$b=b^{\prime}$ was the case all along. To see why these operations and rules
cannot be sound in the coupling logic, we will show
$\vDash\mathit{flip\\_proph}\precsim\mathit{flip}:\mathsf{bool}$ where

$\displaystyle\mathit{flip\\_proph}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptp\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{NewProph}}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptx\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pty\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{Resolve}}}p\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{to}}}y;$
$\displaystyle x\mathbin{\&\&}y$

which cannot be the case as $\mathit{flip\\_proph}$ returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
only with probability $1/4$.

We unfold the relational judgment and apply 7.2 which gives us a prophecy
about $y$ and its future resolution $b$. If $b$ is true, the evaluation on the
left is predetermined to be
$x\mathbin{\&\&}\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}=x$.
By coupling the sampling of $x$ with the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()$
on the right using 24, we finish using 23 and 7.2. On the other hand, if $b$
is false, the evaluation on the left is predetermined to be
$x\mathbin{\&\&}\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
We apply 23 first and couple the sampling of $y$ with the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()$
on the right using 24 and finish using 7.2.

The counterexample shows that prophecy variables are unsound for the coupling
logic, for the same reason that presampling is unsound without syntactic tape
labels: If the prover can predict the outcomes of random samples ahead of
time, it gives them too much power to choose which sampling they couple with.

##  8\. Coq Formalization

All the results presented in the paper, including the background on
probability theory, the formalization of the logic, and the case studies have
been formalized in the Coq proof assistant (The Coq Development Team, 2022).
The results about probability theory are built on top of the Coquelicot
library (Boldo et al., 2015), extending their results to real series indexed
by countable types.

Although we build our logic on top of Iris (Jung et al., 2018), significant
work is involved in formalizing the operational semantics of probabilistic
languages, our new notion of weakest precondition that internalizes the
coupling-based reasoning, and the erasure theorem that allows us to conclude
the existence of a coupling. Our development integrates smoothly with the Iris
Proof Mode (Krebbers et al., 2017b) and we have adapted much of the tactical
support from ReLoC (Frumin et al., 2021b) to reason about the relational
judgment.

##  9\. Related Work

#### Separation logic

Relational separation logics have been developed on top of Iris for a range of
properties, such as contextual refinement (Frumin et al., 2021b; Krebbers et
al., 2017b; Timany et al., 2018; Timany and Birkedal, 2019), simulation
(Chajed et al., 2019; Timany et al., 2021; Gäher et al., 2022), and security
(Frumin et al., 2021a; Gregersen et al., 2021; Georges et al., 2022). The
representation of the right-hand side program as a resource is a recurring
idea, but our technical construction with run ahead is novel. With the
exception of Tassarotti and Harper (2019), probabilistic languages have not
been considered in Iris. Tassarotti and Harper develop a logic to show
refinement between a probabilistic program and a semantic model, not a
program. The logic relies on couplings, but it requires synchronization of
sampling.

In Batz et al. (2019), a framework in which logical assertions are functions
ranging over the non-negative reals is presented. The connectives of
separation logic are given an interpretation as maps from pairs of non-
negative reals to the positive reals. This work focuses on proving
quantitative properties of a single program, e.g., bounding the probability
that certain events happen. A variety of works have developed separation
logics in which the separating conjunction models various forms of
probabilistic independence (Barthe et al., 2020; Bao et al., 2021, 2022). For
example, the statement $P\mskip 5.0mu{\ast}\mskip 5.0muQ$ is taken to mean
“the distribution of $P$ is independent from the distribution of $Q$”.

Prophecy variables (Abadi and Lamport, 1988, 1991) have been integrated into
separation logic in both unary (Jung et al., 2020) and relational settings
(Frumin et al., 2021b). The technical solution uses program annotations and
physical state reminiscent of our construction with presampling tapes, but
prophecy resolution is a physical program step, whereas presampling in our
work is a logical operation. Prophecies can also be erased through refinement
(Frumin et al., 2021b).

#### Probabilistic couplings

Probabilistic couplings are a technique from probability theory that can be
used to prove equivalences between distributions or mixing times of Markov
chains (Aldous, 1983). In computer science, they have been used to reason
about relational properties of programs such as equivalences (Barthe et al.,
2015) and differential privacy (Barthe et al., 2016a). However, these logics
requires the sampling points on both programs to be synchronized in order to
construct couplings. In a higher-order setting, the logic by Aguirre et al.
(2018) establish so-called “shift couplings” between probabilistic streams
that evolve at different rates, but these rules are ad-hoc and limited to the
stream type. Also in the higher-order setting, Aguirre et al. (2021) use
couplings to reason about adversarially-defined properties, however they only
support synchronous couplings, first-order global state, and use a graded
state monad to enforce separation of adversary memories.

#### Logical relations

Step-indexed logical relations have been applied to reason about contextual
equivalence of probabilistic programs in a variety of settings. Bizjak and
Birkedal (2015) develop logical relations for a language similar to ours,
although only with first-order state. This work has since been extended to a
language with continuous probabilistic choice (but without state and
impredicative polymorphism) (Wand et al., 2018), for which equivalence is
shown by establishing a measure preserving transformation between the sources
of randomness for both programs. Recently, this was further extended to
support nested inference queries (Zhang and Amin, 2022).

Another line of work (Dal Lago and Gavazzo, 2021, 2022) uses so called
differential logical relations to reason about contextual distance rather than
equivalence. Programs are related using metrics rather than equivalence
relations, which allows to quantify how similar programs are.

#### Cryptographic frameworks

CertiCrypt (Barthe et al., 2010, 2009) is a framework for cryptographic game-
playing proofs written in a simple probabilistic first-order while-language
(“pWhile”). CertiCrypt formalizes a denotational semantics for pWhile in Coq
and supports reasoning about the induced notion of program equivalence via a
pRHL, and provides dedicated tactics for lazy/eager sampling transformations.
These kind of transformations are non-trivial for expressive languages like
ours. CertiCrypt also provides a quantitative unary logic.

EasyCrypt (Barthe et al., 2013) is a standalone prover for higher-order logic
building on CertiCrypt’s ideas. It leverages the first-order nature of pWhile
for proof automation via SMT solvers. EasyCrypt extends pWhile with a module
system (Barbosa et al., 2021) to support reasoning about abstract code as
module parameters. It integrates a quantitative unary logic with pRHL, and
supports reasoning about complexity in terms of oracle calls (Barbosa et al.,
2021). Both automation and these kind of properties are out of scope for our
work but would be interesting future directions.

In FCF (Petcher and Morrisett, 2015), programs are written as Coq expressions
in the free subdistributions monad. Proofs are conducted in a pRHL-like logic,
where successive sampling statements can be swapped thanks to the
commutativity of the monad.

SSProve (Abate et al., 2021; Haselwarter et al., 2021) supports modular crypto
proofs by composing “packages” of programs written in the free monad for state
and probabilities. The swap rule in SSProve allows exchanging commands which
maintain a state invariant. Reasoning about dynamically allocated local state
is not supported.

IPDL (Gancher et al., 2023) is a process calculus for stating and proving
cryptographic observational equivalences. IPDL is mechanized in Coq and
targeted at equational reasoning about interactive message-passing in high-
level cryptographic protocol models, and hence considers a different set of
language features.

##  10\. Conclusion

We have presented Clutch, a novel higher-order probabilistic relational
separation logic with support for asynchronous probabilistic coupling-based
proofs of contextual refinement and equivalence of probabilistic higher-order
programs with local state and impredicative polymorphism. We have proved the
soundness of Clutch formally in Coq using a range of new technical concepts
and ideas such as _left-partial couplings_ , _presampling tapes_ , and a
_coupling modality_. We have demonstrated the usefulness of our approach
through several example program equivalences that, to the best of our
knowledge, were not possible to establish with previous methods.

## Data Availability Statement

The Coq formalization accompanying this work is available on Zenodo (Gregersen
et al., 2023) and on GitHub at https://github.com/logsem/clutch.

###### Acknowledgements.

This work was supported in part by a Villum Investigator grant (no. 25804),
Center for Basic Research in Program Verification (CPV), from the VILLUM
Foundation. This work was co-funded by the European Union (ERC, CHORDS,
101096090). Views and opinions expressed are however those of the author(s)
only and do not necessarily reflect those of the European Union or the
European Research Council. Neither the European Union nor the granting
authority can be held responsible for them. This material is based upon work
supported in part by the Sponsor National Science Foundation  under Grant No.
Grant #2318724.

## References

  * (1)
  * Abadi and Lamport (1988) Martín Abadi and Leslie Lamport. 1988.  The Existence of Refinement Mappings. In _Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), Edinburgh, Scotland, UK, July 5-8, 1988_. 165–175.  https://doi.org/10.1109/LICS.1988.5115
  * Abadi and Lamport (1991) Martín Abadi and Leslie Lamport. 1991.  The Existence of Refinement Mappings.  _Theor. Comput. Sci._ 82, 2 (1991), 253–284.  https://doi.org/10.1016/0304-3975(91)90224-P
  * Abate et al. (2021) Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021.  SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. In _34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021_. 1–15.  https://doi.org/10.1109/CSF51468.2021.00048
  * Aguirre et al. (2018) Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018\.  Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In _Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings_. 214–241.  https://doi.org/10.1007/978-3-319-89884-1_8
  * Aguirre et al. (2021) Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, and Tetsuya Sato. 2021\.  Higher-order probabilistic adversarial computations: categorical semantics and program logics.  _Proc. ACM Program. Lang._ 5, ICFP (2021), 1–30.  https://doi.org/10.1145/3473598
  * Aldous (1983) David J. Aldous. 1983\.  Random walks on finite groups and rapidly mixing Markov chains.  _Séminaire de probabilités de Strasbourg_ 17 (1983), 243–297.  http://www.numdam.org/item/SPS_1983__17__243_0/
  * Almeida et al. (2019) José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub. 2019.  Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. In _Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019_ , Lorenzo Cavallaro, Johannes Kinder, XiaoFeng Wang, and Jonathan Katz (Eds.). ACM, 1607–1622.  https://doi.org/10.1145/3319535.3363211
  * Appel (2001) Andrew W. Appel. 2001\.  Foundational Proof-Carrying Code. In _16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings_. 247–256.  https://doi.org/10.1109/LICS.2001.932501
  * Bao et al. (2021) Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. 2021.  A Bunched Logic for Conditional Independence. In _36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021_. IEEE, 1–14.  https://doi.org/10.1109/LICS52264.2021.9470712
  * Bao et al. (2022) Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. 2022.  A separation logic for negative dependence.  _Proc. ACM Program. Lang._ 6, POPL (2022), 1–29.  https://doi.org/10.1145/3498719
  * Barbosa et al. (2021) 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
  * Barker and Kelsey (2015) Elaine B. Barker and John M. Kelsey. 2015.  _Recommendation for Random Number Generation Using Deterministic Random Bit Generators_.  National Institute of Standards and Technology.  https://doi.org/10.6028/nist.sp.800-90ar1
  * Barthe et al. (2013) 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_. 146–166.  https://doi.org/10.1007/978-3-319-10082-1_6
  * Barthe et al. (2015) 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_. 387–401.  https://doi.org/10.1007/978-3-662-48899-7_27
  * Barthe et al. (2018) Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2018\.  Proving expected sensitivity of probabilistic programs.  _Proc. ACM Program. Lang._ 2, POPL (2018), 57:1–57:29.  https://doi.org/10.1145/3158145
  * Barthe et al. (2016a) Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016a.  Advanced Probabilistic Couplings for Differential Privacy. In _Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016_ , Edgar R. Weippl, Stefan Katzenbeisser, Christopher Kruegel, Andrew C. Myers, and Shai Halevi (Eds.). ACM, 55–67.  https://doi.org/10.1145/2976749.2978391
  * Barthe et al. (2016b) Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2016b.  Proving Differential Privacy via Probabilistic Couplings. In _Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016_. 749–758.  https://doi.org/10.1145/2933575.2934554
  * Barthe et al. (2009) Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009\.  Formal certification of code-based cryptographic proofs. In _Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009_. 90–101.  https://doi.org/10.1145/1480881.1480894
  * Barthe et al. (2010) Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2010\.  Programming Language Techniques for Cryptographic Proofs. In _Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings_. 115–130.  https://doi.org/10.1007/978-3-642-14052-5_10
  * Barthe et al. (2020) Gilles Barthe, Justin Hsu, and Kevin Liao. 2020.  A probabilistic separation logic.  _Proc. ACM Program. Lang._ 4, POPL (2020), 55:1–55:30.  https://doi.org/10.1145/3371123
  * Barthe et al. (2012) Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012\.  Probabilistic relational reasoning for differential privacy. In _Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012_. 97–110.  https://doi.org/10.1145/2103656.2103670
  * Batz et al. (2019) Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019.  Quantitative separation logic: a logic for reasoning about probabilistic pointer programs.  _Proc. ACM Program. Lang._ 3, POPL (2019), 34:1–34:29.  https://doi.org/10.1145/3290347
  * Bellare and Rogaway (1993) Mihir Bellare and Phillip Rogaway. 1993.  Random Oracles are Practical: A Paradigm for Designing Efficient Protocols. In _CCS ’93, Proceedings of the 1st ACM Conference on Computer and Communications Security, Fairfax, Virginia, USA, November 3-5, 1993_. 62–73.  https://doi.org/10.1145/168588.168596
  * Bellare and Rogaway (2004) Mihir Bellare and Phillip Rogaway. 2004.  Code-Based Game-Playing Proofs and the Security of Triple Encryption.  Cryptology ePrint Archive, Paper 2004/331.  https://eprint.iacr.org/2004/331 https://eprint.iacr.org/2004/331.
  * Bellare and Rogaway (2006) Mihir Bellare and Phillip Rogaway. 2006.  The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In _Advances in Cryptology - EUROCRYPT 2006_ , Serge Vaudenay (Ed.). 409–426.
  * Bizjak (2016) Aleš Bizjak. 2016\.  _On Semantics and Applications of Guarded Recursion_.  Ph. D. Dissertation. Aarhus University.
  * Bizjak and Birkedal (2015) Ales Bizjak and Lars Birkedal. 2015.  Step-Indexed Logical Relations for Probability. In _Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings_. 279–294.  https://doi.org/10.1007/978-3-662-46678-0_18
  * Boldo et al. (2015) Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2015\.  Coquelicot: A User-Friendly Library of Real Analysis for Coq.  _Math. Comput. Sci._ 9, 1 (2015), 41–62.
  * Bousquet and Elisseeff (2002) Olivier Bousquet and André Elisseeff. 2002.  Stability and Generalization.  _J. Mach. Learn. Res._ 2 (mar 2002), 499–526.  https://doi.org/10.1162/153244302760200704
  * Chajed et al. (2019) Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2019.  Verifying concurrent, crash-safe systems with Perennial. In _Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019_. 243–258.  https://doi.org/10.1145/3341301.3359632
  * Claessen and Palka (2013) Koen Claessen and Michal H. Palka. 2013.  Splittable pseudorandom number generators using cryptographic hashing. In _Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, Boston, MA, USA, September 23-24, 2013_ , Chung-chieh Shan (Ed.). ACM, 47–58.  https://doi.org/10.1145/2503778.2503784
  * Dal Lago and Gavazzo (2021) Ugo Dal Lago and Francesco Gavazzo. 2021.  Differential logical relations, part II increments and derivatives.  _Theor. Comput. Sci._ 895 (2021), 34–47.  https://doi.org/10.1016/j.tcs.2021.09.027
  * Dal Lago and Gavazzo (2022) Ugo Dal Lago and Francesco Gavazzo. 2022.  Effectful program distancing.  _Proc. ACM Program. Lang._ 6, POPL (2022), 1–30.  https://doi.org/10.1145/3498680
  * Dreyer et al. (2011) Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011.  Logical Step-Indexed Logical Relations.  _Log. Methods Comput. Sci._ 7, 2 (2011).  https://doi.org/10.2168/LMCS-7(2:16)2011
  * Dreyer et al. (2012) Derek Dreyer, Georg Neis, and Lars Birkedal. 2012.  The impact of higher-order state and control effects on local relational reasoning.  _J. Funct. Program._ 22, 4-5 (2012), 477–528.  https://doi.org/10.1017/S095679681200024X
  * Dwork and Roth (2013) Cynthia Dwork and Aaron Roth. 2013.  The Algorithmic Foundations of Differential Privacy.  _Foundations and Trends® in Theoretical Computer Science_ 9, 3-4 (2013), 211–407.  https://doi.org/10.1561/0400000042
  * Eberl et al. (2020) 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
  * Elgamal (1985) Taher Elgamal. 1985\.  A public key cryptosystem and a signature scheme based on discrete logarithms.  _IEEE Trans. Inf. Theory_ 31, 4 (1985), 469–472.  https://doi.org/10.1109/TIT.1985.1057074
  * Frumin et al. (2021a) Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021a.  Compositional Non-Interference for Fine-Grained Concurrent Programs. In _42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021_. 1416–1433.  https://doi.org/10.1109/SP40001.2021.00003
  * Frumin et al. (2021b) Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2021b.  ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.  _Log. Methods Comput. Sci._ 17, 3 (2021).  https://doi.org/10.46298/lmcs-17(3:9)2021
  * Gäher et al. (2022) Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. 2022.  Simuliris: a separation logic framework for verifying concurrent program optimizations.  _Proc. ACM Program. Lang._ 6, POPL (2022), 1–31.  https://doi.org/10.1145/3498689
  * Gancher et al. (2023) Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett. 2023.  A Core Calculus for Equational Proofs of Cryptographic Protocols.  _Proc. ACM Program. Lang._ 7, POPL, Article 30 (jan 2023), 27 pages.  https://doi.org/10.1145/3571223
  * Georges et al. (2022) Aïna Linn Georges, Alix Trieu, and Lars Birkedal. 2022\.  Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities.  _Proc. ACM Program. Lang._ 6, OOPSLA1 (2022), 1–30.  https://doi.org/10.1145/3527318
  * Goldwasser and Micali (1984) Shafi Goldwasser and Silvio Micali. 1984.  Probabilistic Encryption.  _J. Comput. Syst. Sci._ 28, 2 (1984), 270–299.  https://doi.org/10.1016/0022-0000(84)90070-9
  * Gregersen et al. (2023) Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, and Lars Birkedal. 2023.  _Asynchronous Probabilistic Couplings in Higher- Order Separation Logic - Coq Artifact_.  https://doi.org/10.5281/zenodo.8424490
  * Gregersen et al. (2021) Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. 2021.  Mechanized logical relations for termination-insensitive noninterference.  _Proc. ACM Program. Lang._ 5, POPL (2021), 1–29.  https://doi.org/10.1145/3434291
  * Haselwarter et al. (2021) Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, and Bas Spitters. 2021\.  SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.  Cryptology ePrint Archive, Paper 2021/397.  https://eprint.iacr.org/2021/397 https://eprint.iacr.org/2021/397.
  * Johann et al. (2010) Patricia Johann, Alex Simpson, and Janis Voigtländer. 2010\.  A Generic Operational Metatheory for Algebraic Effects. In _Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom_. 209–218.  https://doi.org/10.1109/LICS.2010.29
  * Jung et al. (2016) Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016.  Higher-order ghost state. In _Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016_. 256–269.  https://doi.org/10.1145/2951913.2951943
  * Jung et al. (2018) Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018.  Iris from the ground up: A modular foundation for higher-order concurrent separation logic.  _J. Funct. Program._ 28 (2018), e20.  https://doi.org/10.1017/S0956796818000151
  * Jung et al. (2020) Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020.  The future is ours: prophecy variables in separation logic.  _Proc. ACM Program. Lang._ 4, POPL (2020), 45:1–45:32.  https://doi.org/10.1145/3371113
  * Jung et al. (2015) 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 _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015_. 637–650.  https://doi.org/10.1145/2676726.2676980
  * Krebbers et al. (2017a) Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017a.  The Essence of Higher-Order Concurrent Separation Logic. In _Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings_. 696–723.  https://doi.org/10.1007/978-3-662-54434-1_26
  * Krebbers et al. (2017b) Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b.  Interactive proofs in higher-order concurrent separation logic. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_. 205–217.  https://doi.org/10.1145/3009837.3009855
  * Lindvall (2002) T. Lindvall. 2002\.  _Lectures on the Coupling Method_.  Dover Publications, Incorporated.
  * Mittelbach and Fischlin (2021) Arno Mittelbach and Marc Fischlin. 2021.  _The Theory of Hash Functions and Random Oracles - An Approach to Modern Cryptography_.  Springer.  https://doi.org/10.1007/978-3-030-63287-8
  * Petcher and Morrisett (2015) Adam Petcher and Greg Morrisett. 2015.  The Foundational Cryptography Framework. In _Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings_. 53–72.  https://doi.org/10.1007/978-3-662-46666-7_4
  * Pitts and Stark (1998) Andrew M. Pitts and Ian D. B. Stark. 1998.  Operational Reasoning for Functions with Local State.  In _Higher Order Operational Techniques in Semantics_ , A. D. Gordon and A. M. Pitts (Eds.). Cambridge University Press, 227–273.
  * Rosulek (2020) Mike Rosulek. 2020\.  _The Joy of Cryptography_.  http://web.engr.oregonstate.edu/~rosulekm/crypto/
  * Sangiorgi and Vignudelli (2016) Davide Sangiorgi and Valeria Vignudelli. 2016.  Environmental bisimulations for probabilistic higher-order languages. In _Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016_. 595–607.  https://doi.org/10.1145/2837614.2837651
  * Seidel and Aragon (1996) Raimund Seidel and Cecilia R. Aragon. 1996.  Randomized Search Trees.  _Algorithmica_ 16, 4/5 (1996), 464–497.  https://doi.org/10.1007/BF01940876
  * Svendsen and Birkedal (2014) Kasper Svendsen and Lars Birkedal. 2014.  Impredicative Concurrent Abstract Predicates. In _Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings_. 149–168.  https://doi.org/10.1007/978-3-642-54833-8_9
  * Tassarotti and Harper (2019) 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
  * The Coq Development Team (2022) The Coq Development Team. 2022\.  The Coq Proof Assistant.  https://doi.org/10.5281/zenodo.7313584
  * The Iris Development Team (2022) The Iris Development Team. 2022\.  The Iris 4.0 Reference.  https://plv.mpi-sws.org/iris/appendix-4.0.pdf
  * Thorisson (2000) Hermann Thorisson. 2000\.  _Coupling, stationarity, and regeneration_.  Springer-Verlag, New York. xiv+517 pages.
  * Timany and Birkedal (2019) Amin Timany and Lars Birkedal. 2019.  Mechanized relational verification of concurrent programs with continuations.  _Proc. ACM Program. Lang._ 3, ICFP (2019), 105:1–105:28.  https://doi.org/10.1145/3341709
  * Timany et al. (2021) Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Léon Gondelman, Abel Nieto, and Lars Birkedal. 2021\.  Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic.  _CoRR_ abs/2109.07863 (2021).  arXiv:2109.07863 https://arxiv.org/abs/2109.07863
  * Timany et al. (2022) Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. 2022.  A Logical Approach to Type Soundness. (2022).  https://iris-project.org/pdfs/2022-submitted-logical-type-soundness.pdf Unpublished manuscript.
  * Timany et al. (2018) Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2018.  A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST.  _Proc. ACM Program. Lang._ 2, POPL (2018), 64:1–64:28.  https://doi.org/10.1145/3158152
  * Turon et al. (2013a) Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013a.  Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In _ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013_. 377–390.  https://doi.org/10.1145/2500365.2500600
  * Turon et al. (2013b) Aaron Joseph Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. 2013b.  Logical relations for fine-grained concurrency. In _The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013_. 343–356.  https://doi.org/10.1145/2429069.2429111
  * Villani (2008) C. Villani. 2008\.  _Optimal Transport: Old and New_.  Springer Berlin Heidelberg.
  * Wand et al. (2018) Mitchell Wand, Ryan Culpepper, Theophilos Giannakopoulos, and Andrew Cobb. 2018.  Contextual equivalence for a probabilistic language with continuous random variables and recursion.  _Proc. ACM Program. Lang._ 2, ICFP (2018), 87:1–87:30.  https://doi.org/10.1145/3236782
  * Zhang and Amin (2022) Yizhou Zhang and Nada Amin. 2022.  Reasoning about ”reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion.  _Proc. ACM Program. Lang._ 6, POPL (2022), 1–28.  https://doi.org/10.1145/3498677

##  Appendix A Model of Clutch

The value interpretation of types is shown in Figure 13.

$\displaystyle\llbracket\alpha\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\Delta(\alpha)(v_{1},v_{2})$
$\displaystyle\llbracket\mathsf{unit}\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq v_{1}=v_{2}=()$
$\displaystyle\llbracket\mathsf{int}\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists z\in\mathbb{Z}.\nobreak\hskip 1.99997pt plus
1.00006ptv_{1}=v_{2}=z$
$\displaystyle\llbracket\mathsf{nat}\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists n\in\mathbb{N}.\nobreak\hskip 1.99997pt plus
1.00006ptv_{1}=v_{2}=n$
$\displaystyle\llbracket\mathsf{bool}\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists b\in\mathbb{B}.\nobreak\hskip 1.99997pt plus
1.00006ptv_{1}=v_{2}=b$
$\displaystyle\llbracket\tau\to\sigma\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\mathop{\boxempty}{}(\forall
w_{1},w_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt\llbracket\tau\rrbracket_{\Delta}(w_{1},w_{2})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\Delta\vDash v_{1}\leavevmode\nobreak\ w_{1}\precsim
v_{2}\leavevmode\nobreak\ w_{2}:\sigma{})$
$\displaystyle\llbracket\tau\times\sigma\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists
w_{1},w_{1}^{\prime},w_{2},w_{2}^{\prime}.\nobreak\hskip 1.99997pt plus
1.00006pt(v_{1}=(w_{1},w_{1}^{\prime}))\mskip 5.0mu{\ast}\mskip
5.0mu(v_{2}=(w_{2},w_{2}^{\prime}))\mskip 5.0mu{\ast}\mskip
5.0mu\llbracket\tau\rrbracket_{\Delta}(w_{1},w_{2})\mskip 5.0mu{\ast}\mskip
5.0mu\llbracket\sigma\rrbracket_{\Delta}(w_{1}^{\prime},w_{2}^{\prime})$
$\displaystyle\llbracket\tau+\sigma\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists w_{1},w_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt(v_{1}=\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{inl}}}(w_{1})\mskip
5.0mu{\ast}\mskip
5.0muv_{2}=\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{inl}}}(w_{2})\mskip
5.0mu{\ast}\mskip
5.0mu\llbracket\tau\rrbracket_{\Delta}(w_{1},w_{2}))\leavevmode\nobreak\ \lor$
$\displaystyle{}\qquad(v_{1}=\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{inr}}}(w_{1})\mskip
5.0mu{\ast}\mskip
5.0muv_{2}=\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{inr}}}(w_{2})\mskip
5.0mu{\ast}\mskip 5.0mu\llbracket\sigma\rrbracket_{\Delta}(w_{1},w_{2}))$
$\displaystyle\llbracket\mu\,\alpha.\nobreak\hskip 1.99997pt plus
1.00006pt\tau\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\left(\mu R.\nobreak\hskip 1.99997pt plus
1.00006pt\lambda(v_{1},v_{2}).\nobreak\hskip 1.99997pt plus 1.00006pt\exists
w_{1},w_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt(v_{1}=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{fold}}\nobreak\hskip
1.99997pt plus 1.00006ptw_{1})\mskip 5.0mu{\ast}\mskip
5.0mu(v^{\prime}=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{fold}}\nobreak\hskip
1.99997pt plus 1.00006ptw_{2})\mskip 5.0mu{\ast}\mskip
5.0mu\mathop{{\triangleright}}\llbracket\tau\rrbracket_{\Delta,\alpha\mapsto
R}(w_{1},w_{2})\right)(v_{1},v_{2})$
$\displaystyle\llbracket\forall\alpha.\nobreak\hskip 1.99997pt plus
1.00006pt\tau\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\mathop{\boxempty}{}\left(\forall R.\nobreak\hskip
1.99997pt plus 1.00006pt(\Delta,\alpha\mapsto R\vDash
v_{1}\leavevmode\nobreak\ \\_\precsim v_{2}\leavevmode\nobreak\
\\_:\tau{}\right)$ $\displaystyle\llbracket\exists\alpha.\nobreak\hskip
1.99997pt plus 1.00006pt\tau\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists R,w_{1},w_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt(v_{1}=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{pack}}\nobreak\hskip
1.99997pt plus 1.00006ptw_{2})\mskip 5.0mu{\ast}\mskip
5.0mu(v_{2}=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{pack}}\nobreak\hskip
1.99997pt plus 1.00006ptw_{2})\mskip 5.0mu{\ast}\mskip
5.0mu\llbracket\tau\rrbracket_{\Delta,\alpha\mapsto R}(w_{1},w_{2})$
$\displaystyle\llbracket\mathsf{ref}\nobreak\hskip 1.99997pt plus
1.00006pt\tau\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists\ell_{1},\ell_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt(v_{1}=\ell_{1})\mskip 5.0mu{\ast}\mskip 5.0mu(v_{2}=\ell_{2})\mskip
5.0mu{\ast}\mskip 5.0mu\leavevmode\hbox to170.19pt{\vbox
to12.6pt{\pgfpicture\makeatletter\hbox{\hskip 85.09686pt\lower-3.3pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-83.99687pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${\,\exists
w_{1},w_{2}.\nobreak\hskip 1.99997pt plus 1.00006pt\ell_{1}\mapsto w_{1}\mskip
5.0mu{\ast}\mskip 5.0mu\ell_{2}\mapsto_{\mathsf{s}}w_{2}\mskip
5.0mu{\ast}\mskip
5.0mu\llbracket\tau\rrbracket_{\Delta}(w_{1},w_{2})\,}\mathstrut$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}{}}{}{{}}{}
{{}}{}{{}{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-84.99687pt}{-2.85pt}\pgfsys@moveto{-84.99687pt}{-2.85pt}\pgfsys@lineto{-84.99687pt}{9.2pt}\pgfsys@lineto{84.99687pt}{9.2pt}\pgfsys@lineto{84.99687pt}{-2.85pt}\pgfsys@closepath\pgfsys@moveto{84.99687pt}{9.2pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}^{\,\mathcal{N}.\ell_{1}.\ell_{2}}$
$\displaystyle\llbracket\mathsf{tape}\rrbracket_{\Delta}(v_{1},v_{2})$
$\displaystyle\triangleq\exists\iota_{1},\iota_{2},N.\nobreak\hskip 1.99997pt
plus 1.00006pt(v_{1}=\iota_{1})\mskip 5.0mu{\ast}\mskip
5.0mu(v_{2}=\iota_{2})\mskip 5.0mu{\ast}\mskip 5.0mu\leavevmode\hbox
to102.9pt{\vbox to12.6pt{\pgfpicture\makeatletter\hbox{\hskip
51.44984pt\lower-3.3pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-50.34985pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{${\,\iota_{1}\hookrightarrow(N,\epsilon)\mskip 5.0mu{\ast}\mskip
5.0mu\iota_{2}\hookrightarrow_{\mathsf{s}}(N,\epsilon)\,}\mathstrut$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{{}}{}{{}{}}{}{{}}{}
{{}}{}{{}{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-51.34985pt}{-2.85pt}\pgfsys@moveto{-51.34985pt}{-2.85pt}\pgfsys@lineto{-51.34985pt}{9.2pt}\pgfsys@lineto{51.34985pt}{9.2pt}\pgfsys@lineto{51.34985pt}{-2.85pt}\pgfsys@closepath\pgfsys@moveto{51.34985pt}{9.2pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}^{\,\mathcal{N}.\iota_{1}.\iota_{2}}$
Figure 13. Relational interpretation of types

The full definition of the weakest precondition, including the fancy update
modality and invariant masks, is the guarded fixpoint of the equation found
below.

$\displaystyle\mathsf{wp}_{\mathcal{E}}\nobreak\hskip 1.99997pt plus
1.00006pte_{1}\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}\triangleq{}$
$\displaystyle(e_{1}\in\kern-1.99997pt\textit{Val}\land\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\mathcal{E}}}\kern
0.86108pt}\Phi(e_{1}))\lor{}$
$\displaystyle(e_{1}\not\in\kern-1.99997pt\textit{Val}\land\forall\sigma_{1},\rho_{1}.\nobreak\hskip
1.99997pt plus 1.00006ptS(\sigma_{1})\mskip 5.0mu{\ast}\mskip
5.0muG(\rho_{1})\mskip 1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox
to10.29pt{\vbox to4.65pt{\pgfpicture\makeatletter\hbox{\hskip
0.25833pt\lower-2.32639pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{\mathchoice{\hphantom{{}_{\leavevmode{\mathcal{E}}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-13.88887pt\kern
14.44441pt}_{\kern-17.7pt\leavevmode{\mathcal{E}}\kern
14.44441pt\leavevmode{\emptyset}}}{\hphantom{{}_{\leavevmode{\mathcal{E}}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-13.88887pt\kern
14.44441pt}_{\kern-17.7pt\leavevmode{\mathcal{E}}\kern
14.44441pt\leavevmode{\emptyset}}}{\hphantom{{}_{\leavevmode{\mathcal{E}}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-8.16669pt\kern
8.55557pt}_{\kern-10.88892pt\leavevmode{\mathcal{E}}\kern
8.55557pt\leavevmode{\emptyset}}}{\hphantom{{}_{\leavevmode{\mathcal{E}}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-5.83334pt\kern
6.11111pt}_{\kern-8.55557pt\leavevmode{\mathcal{E}}\kern
6.11111pt\leavevmode{\emptyset}}}}\kern 0.86108pt}$
$\displaystyle\quad\mathsf{execCoupl}(e_{1},\sigma_{1},\rho_{1})(\lambda
e_{2},\sigma_{2},\rho_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt\mathop{{\triangleright}}\mathord{\mathrel{\mathchoice{\hphantom{{}_{\leavevmode{\emptyset}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-13.88887pt\kern
14.44441pt}_{\kern-16.68887pt\leavevmode{\emptyset}\kern
14.44441pt\leavevmode{\mathcal{E}}}}{\hphantom{{}_{\leavevmode{\emptyset}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-13.88887pt\kern
14.44441pt}_{\kern-16.68887pt\leavevmode{\emptyset}\kern
14.44441pt\leavevmode{\mathcal{E}}}}{\hphantom{{}_{\leavevmode{\emptyset}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-8.16669pt\kern
8.55557pt}_{\kern-10.16669pt\leavevmode{\emptyset}\kern
8.55557pt\leavevmode{\mathcal{E}}}}{\hphantom{{}_{\leavevmode{\emptyset}}}{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}^{\kern-5.83334pt\kern
6.11111pt}_{\kern-7.83334pt\leavevmode{\emptyset}\kern
6.11111pt\leavevmode{\mathcal{E}}}}}\kern 0.86108pt}S(\sigma_{2})\mskip
5.0mu{\ast}\mskip 5.0muG(\rho_{2})\mskip 5.0mu{\ast}\mskip
5.0mu\mathsf{wp}_{\mathcal{E}}\nobreak\hskip 1.99997pt plus
1.00006pte_{2}\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}))$

We define an auxiliary partial execution distribution
$\operatorname{execConf}_{n}(e,\sigma)\in\mathcal{D}(\kern-0.50003pt\textit{Cfg})$.

$\displaystyle\operatorname{execConf}_{n}(e,\sigma)\triangleq{}\begin{cases}\operatorname{ret}(e,\sigma)&\text{if}\leavevmode\nobreak\
e\in\kern-1.99997pt\textit{Val}\leavevmode\nobreak\
\text{or}\leavevmode\nobreak\ n=0\\\
\operatorname{step}(e,\sigma)\mathbin{\raisebox{1.29167pt}{\scalebox{0.75}{$\gg\mkern-6.0mu=$}}}{}\operatorname{execConf}_{(n-1)}&\text{otherwise}\end{cases}$

The coupling modality used in the definition of the weakest precondition is
defined below. Simple rules or “constructors” that follow by unfolding are
found in Figure 14.

$\displaystyle\mathsf{execCoupl}(e_{1},\sigma_{1},{e_{1}}^{\prime},{\sigma_{1}}^{\prime})(Z)\triangleq\mu\Psi:\kern-0.50003pt\textit{Cfg}\times\kern-0.50003pt\textit{Cfg}\to\textit{iProp}.\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\quad(\exists R.\nobreak\hskip
1.99997pt plus 1.00006pt\begin{aligned} &\mathsf{red}(e_{1},\sigma_{1})\mskip
5.0mu{\ast}\mskip
5.0mu\operatorname{step}(e_{1},\sigma_{1})\sim\operatorname{step}({e_{1}}^{\prime},{\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu\forall\rho_{2},{\rho_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{2},{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},{\rho_{2}}^{\prime}))\lor{}\\\ \end{aligned}$
$\displaystyle\quad(\exists R.\nobreak\hskip 1.99997pt plus
1.00006pt\begin{aligned} &\mathsf{red}(e_{1},\sigma_{1})\mskip
5.0mu{\ast}\mskip
5.0mu\operatorname{step}(e_{1},\sigma_{1})\sim\operatorname{ret}({e_{1}}^{\prime},{\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu\forall\rho_{2}.\nobreak\hskip 1.99997pt plus
1.00006ptR(\rho_{2},({e_{1}}^{\prime},{\sigma_{1}}^{\prime}))\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},({e_{1}}^{\prime},{\sigma_{1}}^{\prime})))\lor{}\\\
\end{aligned}$ $\displaystyle\quad(\exists R.\nobreak\hskip 1.99997pt plus
1.00006pt\operatorname{ret}(e_{1},\sigma_{1})\sim\operatorname{step}({e_{1}}^{\prime},{\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu{}\forall{\rho_{2}}^{\prime}.\nobreak\hskip 1.99997pt
plus 1.00006ptR((e_{1},\sigma_{1}),{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\Psi((e_{1},\sigma_{1}),{\rho_{2}}^{\prime}))\lor{}$
$\displaystyle\quad\left(\bigvee{}_{\iota\in\sigma_{1}}\exists
R.\nobreak\hskip 1.99997pt plus
1.00006pt\operatorname{step}_{\iota}(\sigma_{1})\sim\operatorname{step}({e_{1}}^{\prime},{\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu\forall\sigma_{2},{\rho_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\sigma_{2},{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\Psi((e_{1},\sigma_{2}),{\rho_{2}}^{\prime})\right)\lor{}$
$\displaystyle\quad\left(\bigvee{}_{\iota^{\prime}\in\sigma_{2}}\exists
R.\nobreak\hskip 1.99997pt plus
1.00006pt\operatorname{step}(e_{1},\sigma_{1})\sim\operatorname{step}_{\iota^{\prime}}({\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu\forall\rho_{2},{\sigma_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{2},{\sigma_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},({e_{1}}^{\prime},{\sigma_{2}}^{\prime}))\right)\lor{}$
$\displaystyle\quad\left(\bigvee{}_{(\iota,\iota^{\prime})\in\sigma_{1}\times{\sigma_{1}}^{\prime}}\exists
R.\nobreak\hskip 1.99997pt plus
1.00006pt\operatorname{step}_{\iota}(\sigma_{1})\sim\operatorname{step}_{\iota^{\prime}}({\sigma_{1}}^{\prime}):R\mskip
5.0mu{\ast}\mskip 5.0mu\forall\sigma_{2},{\sigma_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006pt(\sigma_{2},{\sigma_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to10.29pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.0347pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\Psi((e_{1},\sigma_{2}),({e_{1}}^{\prime},{\sigma_{2}}^{\prime}))\right)$

$\displaystyle\displaystyle{\hbox{\hskip
150.10298pt\vbox{\hbox{\hskip-150.10298pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{red}(\rho_{1})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{step}(\rho_{1})\sim\operatorname{step}(\rho_{1}^{\prime}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall\rho_{2},{\rho_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{2},{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},{\rho_{2}}^{\prime})$}}}}}\vbox{}}}\over\hbox{\hskip
44.10216pt\vbox{\vbox{}\hbox{\hskip-44.10214pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}(\rho_{1},\rho_{1}^{\prime})(Z)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
139.97066pt\vbox{\hbox{\hskip-139.97064pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{red}(\rho_{1})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{step}(\rho_{1})\sim\operatorname{ret}(\rho^{\prime}_{1}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall\rho_{2}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{2},\rho^{\prime}_{1})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},{\rho_{1}}^{\prime})$}}}}}\vbox{}}}\over\hbox{\hskip
44.03883pt\vbox{\vbox{}\hbox{\hskip-44.03883pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}(\rho_{1},{\rho_{1}}^{\prime})(Z)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
141.89174pt\vbox{\hbox{\hskip-141.89174pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{ret}(\rho_{1})\sim\operatorname{step}(\rho^{\prime}_{1}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall{\rho_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{1},{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\mathsf{execCoupl}(\rho_{1},{\rho_{2}}^{\prime})(Z)$}}}}\vbox{}}}\over\hbox{\hskip
44.03883pt\vbox{\vbox{}\hbox{\hskip-44.03883pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}(\rho_{1},{\rho_{1}}^{\prime})(Z)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
164.20891pt\vbox{\hbox{\hskip-164.20891pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{step}_{\iota}(\sigma_{1})\sim\operatorname{step}({\rho_{1}}^{\prime}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall\sigma_{2},{\rho_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\sigma_{2},{\rho_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\mathsf{execCoupl}((e_{1},\sigma_{2}),{\rho_{2}}^{\prime})(Z)$}}}}\vbox{}}}\over\hbox{\hskip
54.15007pt\vbox{\vbox{}\hbox{\hskip-54.15005pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}((e_{1},\sigma_{1}),{\rho_{1}}^{\prime})(Z)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
162.1612pt\vbox{\hbox{\hskip-162.16118pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{red}(\rho_{1})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{step}(\rho_{1})\sim\operatorname{step}_{\iota}(\sigma^{\prime}_{1}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall\rho_{2},{\sigma_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\rho_{2},{\sigma_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}Z(\rho_{2},({e_{1}}^{\prime},{\sigma_{2}}^{\prime}))$}}}}}\vbox{}}}\over\hbox{\hskip
54.92006pt\vbox{\vbox{}\hbox{\hskip-54.92006pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}(\rho_{1},({e_{1}}^{\prime},{\sigma_{1}}^{\prime}))(Z)$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
175.93712pt\vbox{\hbox{\hskip-175.9371pt\hbox{\hbox{$\displaystyle\displaystyle\operatorname{step}_{\iota}(\sigma_{1})\sim\operatorname{step}_{\iota^{\prime}}(\sigma^{\prime}_{1}):R$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall\sigma_{2},{\sigma_{2}}^{\prime}.\nobreak\hskip
1.99997pt plus 1.00006ptR(\sigma_{2},{\sigma_{2}}^{\prime})\mskip
1.66667mu\mathrel{\vbox{\hbox{ \leavevmode\hbox to11.4pt{\vbox
to4.65pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-2.32639pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{}
{{}{}}{}{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{
}\pgfsys@roundcap\pgfsys@invoke{
}{}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@lineto{7.5347pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.92361pt}{-1.50833pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{\raisebox{-0.81805pt}[4.30554pt]{$\displaystyle\ast$}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\mskip
1.66667mu\mathord{\mathrel{{{\mid\kern-1.72218pt\Rrightarrow\kern-1.07639pt}}_{\emptyset}}\kern
0.86108pt}\mathsf{execCoupl}((e_{1},\sigma_{2}),({e_{1}}^{\prime},{\sigma_{2}}^{\prime}))(Z)$}}}}\vbox{}}}\over\hbox{\hskip
63.08684pt\vbox{\vbox{}\hbox{\hskip-63.08684pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{execCoupl}((e_{1},\sigma_{1},({e_{1}}^{\prime},{\sigma_{1}}^{\prime}))(Z)$}}}}}}$
Figure 14. $\mathsf{execCoupl}$ unfolding rules.

##  Appendix B On Case Studies and Additional Examples

###  B.1. Sangiorgi and Vignudelli’s “copying” example

Sangiorgi and Vignudelli prove a subtle contextual equivalence mixing
probabilistic choice, local references, and recursion using environmental
bisimulations (Sangiorgi and Vignudelli, 2016). Under call-by-value
evaluation, $\lambda$-abstraction fails to distribute over probabilistic
choice. This is contrary to call-by-name, and can easily be seen by
considering the terms $I$ and $L$ in Figure 15. When evaluated in context
$(\lambda f.\nobreak\hskip 1.99997pt plus 1.00006ptf()=f())[\,\cdot\,]$, $I$
returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
(and
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$)
with probability $\frac{1}{2}$, while $L$ returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
with probability $1$. The non-linear use of $f$ in the context is
characteristic of examples that behave differently under call-by-name and
call-by-value. The equivalence of $K$ and $H$ is achieved by prohibiting such
a “copying” use by exploiting local state.

The environmental bisimulation technique developed in (Sangiorgi and
Vignudelli, 2016) is sufficiently powerful to prove the equivalence as it
works directly with the resulting distributions, but, to our knowledge,
previous attempts at a proof working abstractly with programs via logical
relations were not successful (Bizjak, 2016, Sec. 1.5).

Intuitively, $K$ and $H$ should be equivalent despite the fact that
abstraction does not distribute over probabilistic choice because the closures
they return are protected by a counter that only allows them to be run once.
On the first call, both have equal probability of returning
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
or
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
On subsequent calls, the counter $x$ ensures that they both diverge.

$\displaystyle L\triangleq{}$ $\displaystyle(\lambda\\_.\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}})\oplus(\lambda\\_.\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}})$
$\displaystyle I\triangleq{}$ $\displaystyle\lambda\\_.\nobreak\hskip
1.99997pt plus
1.00006pt(\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}\oplus\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}})$
$\displaystyle K\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptx\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt(\lambda\\_.\nobreak\hskip 1.99997pt plus
1.00006ptM)\oplus(\lambda\\_.\nobreak\hskip 1.99997pt plus 1.00006ptN)$
$\displaystyle H\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptx\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt\lambda\\_.\nobreak\hskip 1.99997pt plus
1.00006pt(M\oplus N)$ $\displaystyle H_{\iota}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptx\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pt\iota\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}1\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\lambda\\_.\nobreak\hskip 1.99997pt
plus 1.00006pt(M\oplus_{\iota}N)$

$\displaystyle M\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}x=0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006ptx\leftarrow
1;\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt\Omega$ $\displaystyle N\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}x=0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006ptx\leftarrow
1;\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt\Omega$ $\displaystyle\Omega\triangleq{}$
$\displaystyle(\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rec}}\nobreak\hskip
1.99997pt plus 1.00006ptf\nobreak\hskip 1.99997pt plus
1.00006ptx\mathrel{=}fx)()$ $\displaystyle
e_{1}\oplus\phantom{{}_{\iota}}e_{2}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus
1.00006pt\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pte_{1}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pte_{2}$ $\displaystyle
e_{1}\oplus_{\iota}e_{2}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus
1.00006pt\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}(\iota)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pte_{1}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pte_{2}$

Figure 15. Sangiorgi and Vignudelli’s example.

The key insight that allows us to prove $K$ and $H$ contextually equivalent in
Clutch is to establish an asynchronous coupling between the two
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
operations. Similarly to the proof of the lazy/eager coin example, we employ
an intermediary version $H_{\iota}$ of the program $H$ in which the sampling
is delayed until the closure is run. The equivalence of $H_{\iota}$ and $H$
follows from 22 and the symbolic execution rules.

The refinement $\emptyset\vDash_{\top}H_{\iota}\precsim
K:\mathsf{unit}\to\mathsf{bool}$ is established by allocating a tape $\iota$
and coupling the (eager)
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()$
in $K$ with the tape $\iota$. Because allocation of $\iota$ is local to
$H_{\iota}$, we obtain exclusive ownership of the tape resource
$\iota\hookrightarrow(1,\epsilon)$. In particular, other parts of the program,
i.e. the context in which $H_{\iota}$ is evaluated in, cannot sample to or
consume bits from $\iota$. By 24, we resolve the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()$
to $b$ in $K$ and obtain $\iota\hookrightarrow(1,b)$ for $H_{\iota}$. We then
allocate the non-atomic invariant:

$\displaystyle(\iota\hookrightarrow(1,b)\mskip 5.0mu{\ast}\mskip
5.0mux\mapsto_{\mathsf{s}}0\mskip 5.0mu{\ast}\mskip 5.0mux\mapsto
0)\lor(\iota\hookrightarrow(1,\epsilon)\mskip 5.0mu{\ast}\mskip
5.0mux\mapsto_{\mathsf{s}}1\mskip 5.0mu{\ast}\mskip 5.0mux\mapsto 1)$

The invariant describes the two possible states of the programs. Either the
closures returned by $K$ and $H_{\iota}$ have not been run yet, in which case
the presampled bit $b$ is still on tape $\iota$ and the counter $x$ is $0$ in
both programs, or the bit has been consumed, and the counter is $1$ in both
programs. It is worth noting here that we will rely crucially on a form of
local state encapsulation for tapes, which guarantees that once $b$ has been
read from $\iota$, the tape remains empty. We only consider the case where
$b=\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
; the other case is analogous.

With the invariant in hand, we apply the proof rule for functions to work on
the bodies of the two closures. As a first step, we open our invariant, and
are left to prove the equivalence in both cases of the disjunction. By virtue
of the non-atomic nature of the invariant, we can keep it open for several
steps of evaluation, involving
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$,
pure reductions, and state-manipulating operations, until it is finally
reestablished.

In the first case, we read $b$ from $\iota$, yielding
$\iota\hookrightarrow(1,\epsilon)$. We are left to prove the refinement of two
structurally equal programs:

$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}x=0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006ptx\leftarrow
1;\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt\Omega$

We take the first branch and set $x$ to $1$. We have now reproven the
invariant, and both programs return
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{true}}$
and conclude.

In the second case of the invariant, the closures have been invoked before,
and we expect them to both diverge. However, before evaluation reaches
$\Omega$ in $H_{\iota}$, another
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}(\iota)$
has to be resolved. Here we exploit the fact that the $\iota$ tape remains
empty once we read $b$, as it is local to $H_{\iota}$. Logically, this
observation manifests in the fact that after the allocation of $\iota$, its
ownership has been transferred into the invariant, and is now reclaimed. We
can thus use 23 to resolve the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
on an empty tape to a new random bit $b^{\prime}$. Irrespectively of the value
of $b^{\prime}$, both programs diverge because we know that
$x\mapsto_{\mathsf{s}}1$ and $x\mapsto 1$. A diverging term refines any other
term; in particular we appeal to 21 to conclude the proof.

###  B.2. ElGamal security proof

$\mathit{PK}\mathit{{}_{rand}}$ $\simeq_{\text{ctx}}$

$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptsk\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptpk\mathrel{=}g^{sk}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptcount\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{query}=\lambda\ msg.\nobreak\hskip 1.99997pt
plus 1.00006pt}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}{count}\neq 0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{None}}}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt}$ $\displaystyle\smash{\quad\quad count\leftarrow
1;}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptb\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptx\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt(B,X)\mathrel{=}(g^{b},g^{x})\nobreak\hskip 1.99997pt
plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{Some}}\ (B,X)}$
$\displaystyle\smash{\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt(pk,\mathit{query})}$

$\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}{}$ $\simeq_{\text{ctx}}$

$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pt\beta\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pt\gamma\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptsk\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptpk\mathrel{=}g^{sk}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptcount\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{query}=\lambda\ msg.\nobreak\hskip 1.99997pt
plus 1.00006pt}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}{count}\neq 0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{None}}}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt}$ $\displaystyle\smash{\quad\quad count\leftarrow
1;}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptb\mathrel{=}\text{\lx@texthl@color{$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n,\beta)$}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptB\mathrel{=}g^{b}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptc\mathrel{=}\text{\lx@texthl@color{$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n,\gamma)$}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptC\mathrel{=}g^{c}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptX\mathrel{=}\text{\lx@texthl@color{$msg\cdot{}C$}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{Some}}\ (B,X)}$
$\displaystyle\smash{\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt(pk,\mathit{query})}$

$\mathcal{C}[\mathit{DH_{rand}}]$

$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt(pk,\text{\lx@texthl@color{$B,C$}})=}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pta\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptb\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptc\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(n)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\smash{\quad(g^{a},\text{\lx@texthl@color{$g^{b},g^{c}$}})\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptcount\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}0\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{query}=\lambda\ msg.\nobreak\hskip 1.99997pt
plus 1.00006pt}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}{count}\neq 0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{None}}}$
$\displaystyle\smash{\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt}$ $\displaystyle\smash{\quad\quad count\leftarrow
1;}$
$\displaystyle\smash{\quad\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptX\mathrel{=}msg\cdot{}C\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt}$
$\displaystyle\smash{\quad\quad\operatorname{\mathsf{Some}}\ (B,X)}$
$\displaystyle\smash{\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt(pk,\mathit{query})}$

Figure 16. The “rand” direction of the security reduction.

As stated in the main paper, the proof of
$\vdash\mathit{PK}\mathit{{}_{rand}}\simeq_{\text{ctx}}\mathcal{C}[\mathit{DH_{rand}}]:\tau{}_{\mathit{\mathit{PK}}}$
is similar to that of
$\vdash\mathit{PK}\mathit{{}_{real}}\simeq_{\text{ctx}}\mathcal{C}[\mathit{DH_{real}}]:\tau{}_{\mathit{\mathit{PK}}}$.
The sequence of games is displayed in Figure 16. Compared to
$\mathit{PK}\mathit{{}_{rand}}$, the
$\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ game samples from tapes $\beta$
and $\gamma$. This difference is immaterial, but the tapes will be used to
connect the lazily-sampling $\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ to
the eagerly-sampling $\mathcal{C}[\mathit{DH_{rand}}]$. More interestingly,
the $X$ component of the ciphertext is computed directly as a random group
element $g^{x}$ in $\mathit{PK}\mathit{{}_{rand}}$, whereas
$\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ multiplies the message $msg$
with a random group element $C$. We have to justify that the two games are
nonetheless equivalent. Intuitively speaking, since $C$ is uniformly
distributed, so is $msg\cdot C$, and hence $X$ is a group element sampled from
a uniform distribution in both games. The rigorous explanation for this
argument hinges on the fact that multiplication with $msg$ induces a bijection
on the set $\\{0,1,\ldots,n\\}$.

Recall that the group $G$ is of order $n+1$. Since $G$ is generated by $g$, we
can thus write $msg=g^{k}$ for some $k\in\\{0,1,\ldots,n\\}$. We can therefore
regroup the exponents in $msg\cdot{}C=g^{k}\cdot{}C=g^{k}\cdot g^{c}$ as
$g^{k+c}$. Since the function $f\triangleq\lambda x.\nobreak\hskip 1.99997pt
plus 1.00006pt(x-k)\bmod(n+1)$ is a bijection on $\\{0,1,\ldots,n\\}$, we can
couple the sampling of $x$ in $\mathit{PK}\mathit{{}_{rand}}$ with the
sampling of $c$ in $\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ to obtain
some value $r$ for $x$ in $\mathit{PK}\mathit{{}_{rand}}$ and $f(r)$ for $c$
in $\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$. By definition of $f$, the
value computed for $X$ in $\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ is
then equal to $X=msg\cdot{}C=g^{k+c}=g^{k+f(r)}=g^{k+r-k}=g^{r}$, just as in
$\mathit{PK}\mathit{{}_{rand}}$, and the two programs are equivalent. This
argument is a standard ingredient in the security proof of ElGamal, and part
of our formalization.

The main difference between $\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ and
$\mathcal{C}[\mathit{DH_{rand}}]$ is that the $\mathit{query}$ function in
$\mathit{PK}^{\mathit{tape}}_{\mathit{rand}}$ samples $b$ and $c$ lazily,
whereas in $\mathcal{C}[\mathit{DH_{rand}}]$, the sampling of $b$ and $c$
occurs eagerly in the beginning. Once again, the proof proceeds in a manner
similar to the lazy-eager coin example.

###  B.3. Eager/Lazy Hash Function

As explained in the body of the paper, it is common to model the hash function
as if it satisfies the so-called _uniform hash assumption_ or the _random
oracle model_. That is, a hash function $h$ from a set of keys $K$ to values
$V$ behaves as if, for each key $k$, the hash $h(k)$ is randomly sampled from
a uniform distribution over $V$, independently of all the other keys.

$\displaystyle\mathit{sample\\_all}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rec}}\nobreak\hskip
1.99997pt plus 1.00006ptf\nobreak\hskip 1.99997pt plus
1.00006ptm\nobreak\hskip 1.99997pt plus 1.00006ptn\mathrel{=}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptn^{\prime}\mathrel{=}n-1\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006ptn^{\prime}<0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pt()\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptb\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\quad\mathit{set}\ m\ n^{\prime}\ b;$
$\displaystyle\quad f\ m\ n^{\prime}$

$\displaystyle\mathit{eager\\_hash}\triangleq{}$ $\displaystyle\lambda
n.\nobreak\hskip 1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptm\mathrel{=}\mathit{init\\_map}\ ()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\mathit{sample\\_all}\ m\ (n+1);$
$\displaystyle(\lambda k.\nobreak\hskip 1.99997pt plus
1.00006pt{\begin{array}[t]{rll}\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{match}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{get}\ m\ k\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{with}}\hfil\lx@intercol\\\
&\operatorname{\mathsf{Some}}(b)&\Rightarrow b\\\
|&\operatorname{\mathsf{None}}&\Rightarrow\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}\\\
\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{end}})\hfil\lx@intercol\end{array}}{}$

Figure 17. Eager hash function.

Figure 17 gives the complete code for the eager hash function that was
excerpted earlier. Given a non-negative integer $n$, executing
$\mathit{eager\\_hash}\ n$ returns a hash function with $K=\\{0,\dots,n\\}$
and $V=\mathbb{B}$. To do so, it first initializes a mutable map $m$, and then
calls $\mathit{sample\\_all}$ on $m$. For each key $k\in K$, the function
$\mathit{sample\\_all}$ samples a boolean $b$ with
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
and stores the value $b$ for the key $k$ in the map $m$. This sampled boolean
serves as the hash for $b$. The function returned by $\mathit{eager\\_hash}$
uses this map to look up the hash values of keys. On input $k$, it looks up
$k$ in the map and returns the resulting value if one is found, and otherwise
returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
Since $\mathit{sample\\_all}$ adds every key in $K$ to the map, this latter
scenario only happens if $k$ is not in $K$.

$\displaystyle\mathit{alloc\\_tapes}\triangleq{}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rec}}\nobreak\hskip
1.99997pt plus 1.00006ptf\nobreak\hskip 1.99997pt plus
1.00006ptm\nobreak\hskip 1.99997pt plus 1.00006ptn\mathrel{=}$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptn^{\prime}\mathrel{=}n-1\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{if}}\nobreak\hskip
1.99997pt plus 1.00006ptn^{\prime}<0\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{then}}\nobreak\hskip
1.99997pt plus 1.00006pt()\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{else}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006pt\iota\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\quad\mathit{set}\ m\ n^{\prime}\
\iota;$ $\displaystyle\quad f\ m\ n^{\prime}$
$\displaystyle\mathit{lazy\\_hash}\triangleq{}$ $\displaystyle\lambda
n.\nobreak\hskip 1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptvm\mathrel{=}\mathit{init\\_map}\ ()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006pttm\mathrel{=}\mathit{init\\_map}\ ()\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\mathit{alloc\\_tapes}\ tm\ (n+1);$
$\displaystyle(\lambda k.\nobreak\hskip 1.99997pt plus
1.00006pt{\begin{array}[t]{rll}\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{match}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{get}\ vm\ k\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{with}}\hfil\lx@intercol\\\
&\operatorname{\mathsf{Some}}(b)\Rightarrow\\\ &\quad b\\\
|&\operatorname{\mathsf{None}}\Rightarrow{{\begin{array}[t]{rll}\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{match}}\nobreak\hskip
1.99997pt plus 1.00006pt\mathit{get}\ tm\ k\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{with}}\hfil\lx@intercol\\\
&\operatorname{\mathsf{Some}}(\iota)\Rightarrow\\\
&\quad{\begin{array}[t]{l}\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptb\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}(\iota)\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt\\\ \mathit{set}\ vm\ b;\\\ b\end{array}}\\\
|&\operatorname{\mathsf{None}}\Rightarrow\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}\\\
\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{end}}\hfil\lx@intercol\end{array}}}\\\
\lx@intercol\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{end}})\hfil\lx@intercol\end{array}}{}$
Figure 18. Lazy hash function.

Figure 18 gives the full code for the lazy sampling version of the random hash
generator. Given a non-negative integer $n$, executing $\mathit{lazy\\_hash}\
n$ returns a hash function for the key space $K=\\{0,\dots,n\\}$. For its
internal state, it uses two physical maps, the tape map $tm$, stores tapes to
be used for random sampling, and the value map $vm$, stores the previously
sampled values for keys that have been hashed. After initializing these maps,
it calls $\mathit{alloc\\_tapes}$, which allocates a tape for each key $k\in
K$ and stores the associated tape in $tm$. The hash function returned by
$\mathit{lazy\\_hash}$ determines the hash for a key $k$ in two stages. It
first looks up $k$ in $vm$ to see if $k$ already has a previously sampled hash
value, and if so, returns the found value. Otherwise, it looks up $k$ in the
tape map $tm$. If no tape is found, then $k$ must not be in $K$, so the
function returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
If a tape $\iota$ is found, then the code samples a boolean $b$ from this tape
with
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$,
stores $b$ for the key $k$ in $vm$, and then returns $b$.

We also prove that for any non-negative number $n$, the eager and lazy
versions are contextually equivalent, that is, $\vdash\mathit{eager\\_hash}\
n\simeq_{\text{ctx}}\mathit{lazy\\_hash}\
n:\mathsf{int}\rightarrow\mathsf{bool}$. The core idea behind this contextual
equivalence proof is to maintain a particular invariant between the internal
state of the two hash functions. Let $m$ be the internal map used by the eager
hash and let $tm$ and $vm$ be the tape and value maps, respectively, for the
lazy hash. Then, at a high level, the invariant maintains the following
properties:

  1. (1)

$\mathsf{dom}(m)=\mathsf{dom}(tm)=\\{0,\dots,n\\}$.

  2. (2)

For all $k\in\\{0,\dots,n\\}$, if $m[k]=b$ then either

    1. (a)

$vm[k]=b$, or

    2. (b)

$vm[k]=\bot$ and $tm[k]=\iota$ for some tape label $\iota$ such that
$\iota\hookrightarrow([b],$).

Case (a) and (b) of the second part of this invariant capture the two possible
states each key $k$ can be in. Either hash of $k$ has been looked up before
(case a), and so the sampled value stored in $vm$ must match that of $m$, or
it has not been looked up (case b) and the tape for the key must contain the
same value as $m[k]$ for its next bit.

To establish this invariant when the hashes are initialized, we asynchronously
couple the eager hash function’s
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
for key $k$ with a tape step for the tape $\iota$ associated with $k$ in the
lazy table. The invariant ensures that the values returned by the two hash
functions will be the same when a key $k$ is queried. The cases of the
invariant corresponding to the branches of the lazy function’s match
statements: if the key $k$ is in $K$ and has been queried before, the maps
will return the same values found in $m$ and $vm$. If it has not been queried
before, then the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
statement in the lazy version will be draw the value on the tape for the key,
which matches $m[k]$. Moreover, the update that writes this sampled value to
$vm$ preserves the invariant, switching from case (b) to case (a) for queried
key.

###  B.4. Random Generators from Hashes

Here we provide further details on generating a random boolean sampler from a
lazy hash function. The following function, $\mathit{init\\_hash\\_rng}$,
returns a function that can be used to generate random booleans:

$\displaystyle\mathit{init\\_hash\\_rng}\triangleq{}$
$\displaystyle\lambda\\_.\nobreak\hskip 1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptf\mathrel{=}\mathit{lazy\\_hash}\
\texttt{MAX}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus
1.00006ptc\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}{0}\nobreak\hskip
1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle(\lambda\\_.\nobreak\hskip 1.99997pt
plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptn\mathrel{=}\mathop{!}{c}\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$
$\displaystyle\quad\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{let}}\nobreak\hskip
1.99997pt plus 1.00006ptb\mathrel{=}f\ n\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{in}}\nobreak\hskip
1.99997pt plus 1.00006pt$ $\displaystyle\quad c\leftarrow n+1;$
$\displaystyle\quad b)$

When run, $\mathit{init\\_hash\\_rng}$ generates a lazy hash function $f$ for
the key space $K=\\{0,\dots,\texttt{MAX}\\}$ for some fixed constant MAX. It
then allocates a counter $c$ as a mutable reference initialized to $0$. The
returned function, let us call it $h$, uses $f$ and $c$ to generate random
booleans. Each time $h$ is called, it loads the current value $n$ form $c$,
hashes $n$ with $f$ to get a boolean $b$. It then increments $c$ and returns
the boolean $b$, which serves as a random boolean. Repeated calls to $h$