return independent, uniformly sampled booleans, so long as we make no more
than MAX calls. The reason this works is that we have assumed the hash
function $f$ is uniformly random, so the hashes of different keys are
independently sampled. So long as we make fewer than MAX calls to $h$, each
call will hash a distinct number $n$ (the current counter value), so it will
be independent of all previous and future calls. After MAX calls, $c$ will
exceed MAX and so we will hash a key outside of $f$’s key space. Recall from
the previous example that $\mathit{lazy\\_hash}$ returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$
on inputs outside its key space.

This example might at first seem artificial, but using cryptographic
primitives such as hashes or block ciphers to generate pseudorandom numbers is
in fact commonly done (Barker and Kelsey, 2015). Although the example here is
simplified compared to real implementations, it captures one of the core
verification challenges common to real implementations. Namely, for
correctness, one must show that the “key” or “counter” being hashed or
encrypted (here the values of $n$ obtained from $c$) are not re-used.

To capture the guarantees of $\mathit{init\\_hash\\_rng}$ more formally, we
prove that $\mathit{init\\_hash\\_rng}$ is contextually equivalent to the
following “bounded” random number generator that directly calls
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$:

$\displaystyle\mathit{init\\_bounded\\_rng}\triangleq{}$
$\displaystyle\qquad\lambda\\_.\nobreak\hskip 1.99997pt plus 1.00006pt$
$\displaystyle\qquad\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\qquad(\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\qquad\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{=}\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\leq\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}{then}}\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}{else}}\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}}\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\qquad\quad c\leftarrow n+1;$
$\displaystyle\qquad\quad b)$

With $\mathit{init\\_bounded\\_rng}$, the returned generator function again
uses a counter $c$, however the value of this counter is just used to track
the number of samples generated. If the number of calls is less than or equal
to MAX, it returns a boolean generated by a call to
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$.
Otherwise, it just returns
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
(In $\mathbf{F}_{\mu,\textnormal{ref}}^{\textnormal{rand}}$, integers are
unbounded, so there is no issue with overflow.)

At a high level, the proof proceeds by maintaining the following invariant
relating the generator functions returned by both $\mathit{init\\_hash\\_rng}$
and $\mathit{init\\_bounded\\_rng}$. Let $f$ be the hash function in the hash-
based generator, $n_{h}$ be its counter value, and $n_{b}$ be the value of the
bounded generator’s counter. Then:

  1. (1)

$n_{h}=n_{b}$.

  2. (2)

The key space of $f$ is $\\{0,\dots,\texttt{MAX}\\}$

  3. (3)

For all $k\in\\{0,\dots,\texttt{MAX}\\}$, if $k\geq n_{h}$ then $f$ has not
yet hashed $k$.

The first and second parts of the invariant guarantees that once $n_{h}$
exceeds MAX, and thus falls outside $f$’s key space, both generators will
return the same value of
$\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{false}}$.
In addition, based on the third part of the invariant, so long as
$n_{h}\in\\{0,\dots,\texttt{MAX}\\}$ when the hash-based generator evaluates
$f\ n_{h}$, we will be able to couple the hash value it samples with the
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}$
command in the bounded generator, ensuring that both generators return the
same value.

The $\mathit{init\\_hash\\_rng}$ function above generates a single random
generator from a hash function. However, in some scenarios, it is necessary to
be able to generate multiple independent streams of random numbers. For
example, in a language with parallelism or concurrency, using a single
generator returned by $\mathit{init\\_hash\\_rng}$ in multiple threads would
mean sharing mutable access to the counter $c$, so that synchronization
primitives would be needed to prevent racy accesses. Related issues have
motivated the need to “split” a random number generator into two streams in
the context of a lazy language like Haskell (Claessen and Palka, 2013).

While $\mathbf{F}_{\mu,\textnormal{ref}}^{\textnormal{rand}}$ is sequential,
we can still explore the question of how to create multiple independent random
generators. One approach would be to call $\mathit{init\\_hash\\_rng}$
multiple times. But that assumes that we have the ability to initialize
multiple random oracle hash functions. In practice, if we instantiate the
random oracle model with a particular concrete hash function, like SHA-256, we
cannot feasibly use different hash functions each time
$\mathit{init\\_hash\\_rng}$ is called. Instead, we would like a way to
generate multiple independent random number generators from a single hash
function.

The solution is to get the illusion of multiple independent hash functions out
of a single hash function by partitioning the key space of the hash.
Specifically, we use a wrapper around the hash function so that it now takes
_two_ integers as input, instead of one, to obtain a so-called _keyed_
hash888In cryptographic settings, a similar construction is called a hash
message authentication code (HMAC). However, HMACs typically use a different
way of combining the two arguments to avoid certain vulnerabilities.:

$\displaystyle\mathit{lazy\\_keyed\\_hash}\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}\
(2^{(p_{k}+p_{v})}-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 k\ v.\nobreak\hskip 1.99997pt
plus 1.00006ptf\ (k\cdot 2^{p_{v}}+v))$

The returned keyed hash function takes two inputs, a key $k$ and a value $v$
to be hashed, combines them into a single integer, and calls the lazy hash
function $f$ on that single integer. The values $p_{k}$ and $p_{v}$ are fixed
constants that determine the range of the keys and values that can be hashed.
If $h$ is the returned hash function, we can treat the partially-applied
functions $h\ k_{1}$ and $h\ k_{2}$ for $k_{1}\neq k_{2}$ as if they were two
independent hash functions, so long as we do not apply the functions to values
$v$ that are larger than $2^{p_{v}}-1$.

Using this, we have verified a version of the hash-based random number
generator that supports splitting multiple independent generators out of a
single hash. Each generator has a distinct key $k$ its own internal counter
$c$. When a sample is requested, it reads the value $n$ from the counter and
computes the keyed hash of $k$ and $n$ to get a boolean. To ensure that the
keys used by the generators are distinct, we assign keys using a shared
counter that is incremented every time a new generator is initialized. The
complete details can be found in the accompanying Coq development.

###  B.5. Lazily Sampled Big Integers

Our last example is motivated by a data structure called a treap (Seidel and
Aragon, 1996). A treap is a binary search tree structure that relies on
randomization to ensure with high probability that the tree will be balanced.
One of the key aspects of the treap is that every key that is inserted into
the treap is first assigned a random numerical _priority_. During the
insertion process, this priority value is compared with the priorities of keys
already in the treap. The exact details of this comparison process are not
relevant here; what is important to know is that, ideally, all of the assigned
priority values are different (that is, there are no _collisions_ of
priorities). Thus, in analyzing the treap, it is common to treat these
priorities as if they are sampled from a continuous distribution, such as the
uniform distribution on the interval $[0,1]$, to ensure that the probability
of collisions is 0. Eberl et al. (Eberl et al., 2020) have previously
mechanized such an analysis of treaps in Isabelle/HOL.

In actual implementations, the priorities are instead typically represented
with some fixed precision, say as an approximate floating point number sampled
from $[0,1]$, or as an integer sampled uniformly from some set
$\\{0,\dots,n\\}$, so that there is some probability of collision. However, in
the latter case, as long as $n$ is big enough relative to the number of keys
added to the tree, the probability of a collision can be kept low, and the
performance properties of the treap are preserved. The probability of a
collision is an instance of the well-known “birthday problem”.

But in some scenarios, we may need to decide on $n$ without knowing in advance
how many keys will end up being added to the treap. If we err on the
conservative side by making $n$ very large, say $2^{256}-1$, the probability
of a collision will be very low, but we will need to use $256$ bits to store
the priorities, which is wasteful if we end up only storing a moderate number
of nodes.

An alternative is to _lazily_ sample the integer that represents the priority.
The insight is that the actual numerical value of the priorities is not
relevant: the only operation that they must support is comparing two
priorities to determine if they are equal, and if not, which one is larger.
Figure 19 gives an implementation of a lazily-sampled integer A lazily-sampled
integer is encoded as a pair of a tape label $\iota$ and a linked list of
length at most $N$, where each node in the list represents a _digit_ of the
integer in base $B$, with the head of the list being the most significant
digit. For concreteness, here we consider $N=8$ and $B=2^{32}$, so that the
encoded numbers can be at most $2^{256}-1$. Rather than sampling all digits up
front, we instead only sample digits when needed as part of comparing a lazy
integer to another.

$\displaystyle\mathit{sample\\_lazy\\_int}\triangleq{}$
$\displaystyle\lambda\\_.\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}{tape}}},\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}\operatorname{\mathsf{None}})$
$\displaystyle\mathit{get\\_next}\triangleq{}$ $\displaystyle\lambda\ \iota\
r.\nobreak\hskip 1.99997pt plus 1.00006pt$
$\displaystyle{\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\mathop{!}{r}\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}}\ v&\Rightarrow v\\\
|&\operatorname{\mathsf{None}}&\Rightarrow{\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.00006ptz\mathrel{=}\mathit{sample32}\ \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\\\
\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.00006ptnext\mathrel{=}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}\operatorname{\mathsf{None}}\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\\\ r\leftarrow\operatorname{\mathsf{Some}}\
(z,next);\\\ (z,next)\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}}$
$\displaystyle\mathit{cmp\\_list}\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.00006ptn\ \iota_{1}\
l_{1}\ \iota_{2}\ l_{2}\mathrel{=}$
$\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=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.00006pt0$
$\displaystyle\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(z_{1},l_{1}^{\prime})\mathrel{=}\mathit{get\\_next}\nobreak\hskip
1.99997pt plus 1.00006pt\iota_{1}\nobreak\hskip 1.99997pt plus
1.00006ptl_{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\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(z_{2},l_{2}^{\prime})\mathrel{=}\mathit{get\\_next}\nobreak\hskip
1.99997pt plus 1.00006pt\iota_{2}\nobreak\hskip 1.99997pt plus
1.00006ptl_{2}\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.00006ptres\mathrel{=}\mathit{cmp}z_{1}\nobreak\hskip
1.99997pt plus 1.00006ptz_{2}\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}{if}}\nobreak\hskip
1.99997pt plus 1.00006ptres=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\quad\quad f\ (n-1)\ \iota_{1}\
l_{1}^{\prime}\ \iota_{2}\ l_{2}^{\prime}$
$\displaystyle\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\ res$ $\displaystyle\mathit{cmp\\_lazy}\triangleq{}$
$\displaystyle\lambda\ (x_{1},x_{2}).\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_{1},l_{1})\mathrel{=}x_{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}{let}}\nobreak\hskip
1.99997pt plus 1.00006pt(\iota_{2},l_{2})\mathrel{=}x_{2}\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.00006ptl_{1}=l_{2}\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.00006pt0$
$\displaystyle\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\mathit{cmp\\_list}\ 8\ \iota_{1}\ l_{1}\ \iota_{2}\
l_{2}$ Figure 19. Implementation of lazily-sampled integers.

The function $\mathit{sample\\_lazy\\_int}$ samples a lazy integer by
generating a tape and a reference to an empty linked list. At this point, the
sampled integer is entirely indeterminate. Given a tape label $\iota$ and a
reference $r$ to a digit in a lazy integer’s list, evaluating
$\mathit{get\\_next}\ \iota\ r$ returns the integer $z$ for that digit and a
reference $next$ to the digit after $r$ in the list. There are two
alternatives when getting the digit: either (1) the digit for $r$ has already
been sampled, so that $\mathop{!}{r}$ will be $\operatorname{\mathsf{Some}}\
v$, where $v$ is a pair of the form $(z,next)$; or (2) the digit for $r$ has
not yet been sampled, so that $\mathop{!}{r}$ will be
$\operatorname{\mathsf{None}}$. In case 1, $\mathit{get\\_next}\ \iota\ r$
just returns $v$. In case 2, $\mathit{get\\_next}$ will first sample the value
$z$ for the digit by calling $\mathit{sample32}\ \iota$, which generates a 32
bit integer by sampling it bit-by-bit with repeated calls to
$\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{flip}}}\iota$.
It then allocates a new reference $next$ for the next digit in the list,
initialized to a value $\operatorname{\mathsf{None}}$. Before returning
$(z,next)$ it stores this pair in the reference $r$.

Evaluating $\mathit{cmp\\_list}\ n\ \iota_{1}\ l_{1}\ \iota_{2}\ l_{2}$
compares the two lazy integers $(\iota_{1},l_{1})$ and $(\iota_{2},l_{2})$ by
doing a digit-by-digit comparison. It returns $-1$ if the first integer is
smaller, $0$ if the integers are equal, and $1$ if the first integer is
larger. The first argument $n$ tracks the number of remaining digits in the
integers. Let us consider the case that $n>0$ first (the else branch). In that
case, $\mathit{cmp\\_list}$ will call $\mathit{get\\_next}$ on each integer to
get the next digit. Let $z_{1}$ and $z_{2}$ be these digit values,
respectively. These digits are compared using $\mathit{cmp}$, which returns
$-1$ (if $z_{1}<z_{2}$), $0$ (if $z_{1}=z_{2}$), or $1$ ($z_{1}>z_{2}$).
Because the lazy integers are stored with most-significant digits earlier in
the list, if $\mathit{cmp}\ z_{1}\ z_{2}$ is non-zero we already know which
lazy integer is larger, and the result of $\mathit{cmp}\ z_{1}\ z_{2}$ gives
the correct ordering of the whole lazy integer. On the other hand if
$\mathit{cmp}$ returns $0$, then $z_{1}=z_{2}$, in which case we cannot yet
tell which lazy integer is larger. Thus, $\mathit{cmp\\_list}$ recursively
calls itself to compare the next digits in the lists, decrementing the $n$
argument to track that there is one fewer digit remaining. In the base case of
the recursion, when $n=0$, that means all digits of the integers have been
equal, hence the value of the integers are equal, so we return $0$. Because
$\mathit{get\\_next}$ conveniently encapsulates the sampling of unsampled
digits, $\mathit{cmp\\_list}$ looks like a normal traversal of the two linked
lists, as if they were eagerly sampled.

Note that if $x$ is a lazy integer, then comparing $x$ with itself using
$\mathit{cmp\\_list}$ unfortunately forces us to sample all of the unsampled
digits of $x$. The routine $\mathit{cmp\\_lazy}$ is a wrapper to
$\mathit{cmp\\_list}$ that implements a small optimization to avoid this. The
function $\mathit{cmp\\_lazy}$ takes as input a pair of lazy integers
$(x_{1},x_{2})$. Before calling $\mathit{cmp\\_list}$, it first checks whether
the pointers to the heads of $x_{1}$ and $x_{2}$’s lists are equal; if they
are the two integers must be equal, so it returns $0$ immediately without
calling $\mathit{cmp\\_list}$.

We prove that this implementation of lazily-sampled integers is contextually
equivalent to code that eagerly samples an entire 256-bit integer by bit-
shifting and adding 8 32-bit integers. This contextual equivalence is at an
_abstract_ existential type $\tau$. Specifically, we define

$\tau\triangleq\exists\alpha.\nobreak\hskip 1.99997pt plus
1.00006pt(\mathsf{unit}\rightarrow\alpha)\times((\alpha\times\alpha)\rightarrow\mathsf{int})$

Then we have the following equivalence:

$\vdash(\mathit{sample\\_lazy\\_int},\mathit{cmp\\_lazy})\simeq_{\text{ctx}}(\mathit{sample256},\mathit{cmp}):\tau$

The starting point for the proof is that when $\mathit{sample256}$ samples the
8 32-bit integers needed to assemble the 256-bit integer, we couple these
samples with identical samples on the tape $\iota$ generated by
$\mathit{sample\\_lazy\\_int}$. Then, the key invariant used in the proof says
that if we combine the digits of a lazy int that have already been sampled,
plus the remaining digits on the tape $\iota$, the result represents an
integer that is equivalent to the corresponding one generated by
$\mathit{sample256}$. This holds initially and is preserved by calls to
$\mathit{get\\_next}$ during $\mathit{cmp\\_list}$, since it moves digits from
the tape to the linked list representing the integer.

##  Appendix C Rules

We repeat the rules presented in the main paper for ease of reference.

wp-wand $\displaystyle\displaystyle{\hbox{\hskip
67.5429pt\vbox{\hbox{\hskip-67.5429pt\hbox{\hbox{$\displaystyle\displaystyle\forall
v.\nobreak\hskip 1.99997pt plus 1.00006pt\Phi(v)\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{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip 1.99997pt
plus 1.00006pte\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}\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\Psi(v)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006pte\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}}}}\vbox{}}}\over\hbox{\hskip
19.60593pt\vbox{\vbox{}\hbox{\hskip-19.60591pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006pte\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Psi\right\\}}$}}}}}}$ wp-bind
$\displaystyle\displaystyle{\hbox{\hskip
46.69388pt\vbox{\hbox{\hskip-46.69386pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006pte\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{v.\mathsf{wp}\nobreak\hskip 1.99997pt plus
1.00006ptK{[}v{]}\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}\right\\}}$}}}\vbox{}}}\over\hbox{\hskip
26.71008pt\vbox{\vbox{}\hbox{\hskip-26.71008pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006ptK{[}e{]}\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}}}}}}$ wp-load
$\displaystyle\displaystyle{\hbox{\hskip
43.32579pt\vbox{\hbox{\hskip-43.32579pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto
v$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto v\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\Phi(v)$}}}}\vbox{}}}\over\hbox{\hskip
20.47224pt\vbox{\vbox{}\hbox{\hskip-20.47223pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006pt\mathop{!}\ell\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}}}}}}$ wp-couple-rands
$\displaystyle\displaystyle{\hbox{\hskip
166.13162pt\vbox{\hbox{\hskip-166.13162pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\ \text{bijection}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{specCtx}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{spec}(\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N))$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus 1.00006pt\mathsf{spec}(f(n))\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\Phi(n)$}}}}}}\vbox{}}}\over\hbox{\hskip
35.4653pt\vbox{\vbox{}\hbox{\hskip-35.4653pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\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}{rand}}}(N)\nobreak\hskip
1.99997pt plus 1.00006pt{\left\\{\Phi\right\\}}$}}}}}}$ wp-couple-tape-l
$\displaystyle\displaystyle{\hbox{\hskip
207.64815pt\vbox{\hbox{\hskip-52.25876pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\ \text{bijection}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
e\not\in\kern-1.99997pt\textit{Val}$}}}}\vbox{\hbox{\hskip-207.64813pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{specCtx}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{spec}(\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N))$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus 1.00006pt\left(\mathsf{spec}(f(n))\mskip
5.0mu{\ast}\mskip 5.0mu\iota\hookrightarrow(N,\vec{n}\cdot n)\right)\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\mathsf{wp}\nobreak\hskip 1.99997pt plus 1.00006pte\nobreak\hskip
1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}}}}}}\vbox{}}}}\over\hbox{\hskip
19.32814pt\vbox{\vbox{}\hbox{\hskip-19.32813pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{wp}\nobreak\hskip
1.99997pt plus 1.00006pte\nobreak\hskip 1.99997pt plus
1.00006pt{\left\\{\Phi\right\\}}$}}}}}}$
Figure 20. Selected structural rules of the weakest preconditon. rel-pure-l
$\displaystyle\displaystyle{\hbox{\hskip
67.78857pt\vbox{\hbox{\hskip-67.78856pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\overset{\mathrm{pure}}{\rightsquigarrow}e_{1}^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}e_{1}^{\prime}{]}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
35.59615pt\vbox{\vbox{}\hbox{\hskip-35.59615pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}e_{1}{]}\precsim
e_{2}:\tau$}}}}}}$ rel-pure-r $\displaystyle\displaystyle{\hbox{\hskip
67.78857pt\vbox{\hbox{\hskip-67.78856pt\hbox{\hbox{$\displaystyle\displaystyle
e_{2}\overset{\mathrm{pure}}{\rightsquigarrow}e_{2}^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}e_{2}^{\prime}{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
35.59615pt\vbox{\vbox{}\hbox{\hskip-35.59615pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}e_{2}{]}:\tau$}}}}}}$ rel-alloc-l $\displaystyle\displaystyle{\hbox{\hskip
58.62668pt\vbox{\hbox{\hskip-58.62668pt\hbox{\hbox{$\displaystyle\displaystyle\forall\ell.\nobreak\hskip
1.99997pt plus 1.00006pt\ell\mapsto v\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\Delta\vDash_{\mathcal{E}}K{[}\ell{]}\precsim
e_{2}:\tau$}}}\vbox{}}}\over\hbox{\hskip
44.06827pt\vbox{\vbox{}\hbox{\hskip-44.06825pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}(v){]}\precsim
e_{2}:\tau$}}}}}}$ rel-alloc-r $\displaystyle\displaystyle{\hbox{\hskip
58.34227pt\vbox{\hbox{\hskip-58.34227pt\hbox{\hbox{$\displaystyle\displaystyle\forall\ell.\nobreak\hskip
1.99997pt plus 1.00006pt\ell\mapsto_{\mathsf{s}}v\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\ell{]}:\tau$}}}\vbox{}}}\over\hbox{\hskip
44.06827pt\vbox{\vbox{}\hbox{\hskip-44.06825pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{ref}}}(v){]}:\tau$}}}}}}$
rel-load-l $\displaystyle\displaystyle{\hbox{\hskip
67.69379pt\vbox{\hbox{\hskip-67.69379pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto
v$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto v\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\Delta\vDash_{\mathcal{E}}K{[}v{]}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
35.34026pt\vbox{\vbox{}\hbox{\hskip-35.34024pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}!\ell{]}\precsim
e_{2}:\tau$}}}}}}$ rel-load-r $\displaystyle\displaystyle{\hbox{\hskip
67.12497pt\vbox{\hbox{\hskip-67.12497pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto_{\mathsf{s}}v$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto_{\mathsf{s}}v\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}v{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
35.34026pt\vbox{\vbox{}\hbox{\hskip-35.34024pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}!\ell{]}:\tau$}}}}}}$ rel-store-l $\displaystyle\displaystyle{\hbox{\hskip
70.0908pt\vbox{\hbox{\hskip-70.0908pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto
v$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto w\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\Delta\vDash_{\mathcal{E}}K{[}(){]}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
45.4432pt\vbox{\vbox{}\hbox{\hskip-45.44319pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\ell\leftarrow
w{]}\precsim e_{2}:\tau$}}}}}}$ rel-store-r
$\displaystyle\displaystyle{\hbox{\hskip
68.13313pt\vbox{\hbox{\hskip-68.13313pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto_{\mathsf{s}}v$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\ell\mapsto_{\mathsf{s}}w\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}(){]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
45.4432pt\vbox{\vbox{}\hbox{\hskip-45.44319pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\ell\leftarrow w{]}:\tau$}}}}}}$ rel-pack
$\displaystyle\displaystyle{\hbox{\hskip
110.60313pt\vbox{\hbox{\hskip-110.60312pt\hbox{\hbox{$\displaystyle\displaystyle\forall
v_{1},v_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt\mathsf{persistent}(R(v_{1},v_{2}))$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,\alpha\mapsto
R\vDash_{\top}e_{1}\precsim e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
58.29607pt\vbox{\vbox{}\hbox{\hskip-58.29605pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\top}\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.00006pte_{1}\precsim\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.00006pte_{2}:\exists\alpha.\nobreak\hskip 1.99997pt plus
1.00006pt\tau$}}}}}}$ rel-rec $\displaystyle\displaystyle{\hbox{\hskip
154.37932pt\vbox{\hbox{\hskip-154.3793pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{\boxempty}\left(\forall
v_{1},v_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt\llbracket\tau\rrbracket_{\Delta}(v_{1},v_{2})\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\Delta\vDash_{\top}(\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_{1}\nobreak\hskip 1.99997pt plus
1.00006ptx_{1}\mathrel{=}e_{1})\,v_{1}\precsim(\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_{2}\nobreak\hskip 1.99997pt plus
1.00006ptx_{2}\mathrel{=}e_{2})\,v_{2}:\tau\to\sigma\right)$}}}\vbox{}}}\over\hbox{\hskip
77.10318pt\vbox{\vbox{}\hbox{\hskip-77.10316pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\top}\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_{1}\nobreak\hskip 1.99997pt plus
1.00006ptx_{1}\mathrel{=}e_{1}\precsim\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_{2}\nobreak\hskip 1.99997pt plus
1.00006ptx_{2}\mathrel{=}e_{2}:\tau\to\sigma$}}}}}}$ rel-return
$\displaystyle\displaystyle{\hbox{\hskip
26.13623pt\vbox{\hbox{\hskip-26.13622pt\hbox{\hbox{$\displaystyle\displaystyle\llbracket\tau\rrbracket_{\Delta}(v_{1},v_{2})$}}}\vbox{}}}\over\hbox{\hskip
29.03616pt\vbox{\vbox{}\hbox{\hskip-29.03615pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\top}v_{1}\precsim
v_{2}:\tau$}}}}}}$ rel-bind $\displaystyle\displaystyle{\hbox{\hskip
137.72563pt\vbox{\hbox{\hskip-137.72562pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall
v_{1},v_{2}.\nobreak\hskip 1.99997pt plus
1.00006pt\llbracket\tau\rrbracket_{\Delta}(v_{1},v_{2})\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{\Delta\vDash_{\top}K{[}v_{1}{]}\precsim
K^{\prime}{[}v_{2}{]}:\sigma}$}}}}\vbox{}}}\over\hbox{\hskip
44.41939pt\vbox{\vbox{}\hbox{\hskip-44.41939pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}e_{1}{]}\precsim
K^{\prime}{[}e_{2}{]}:\sigma$}}}}}}$ Figure 21. Selected structural and
symbolic execution rules for the Clutch refinement judgment. rel-rand-erase-l
$\displaystyle\displaystyle{\hbox{\hskip
92.41385pt\vbox{\hbox{\hskip-92.41383pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\epsilon)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
K^{\prime}{[}n{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
76.93654pt\vbox{\vbox{}\hbox{\hskip-76.93654pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}\precsim
K^{\prime}{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}:\tau$}}}}}}$
rel-rand-erase-r $\displaystyle\displaystyle{\hbox{\hskip
93.5183pt\vbox{\hbox{\hskip-93.51828pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow_{\mathsf{s}}(N,\epsilon)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
K^{\prime}{[}n{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
76.93654pt\vbox{\vbox{}\hbox{\hskip-76.93654pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}\precsim
K^{\prime}{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}:\tau$}}}}}}$
Figure 22. Tape erasure rules. rel-rand-l
$\displaystyle\displaystyle{\hbox{\hskip
54.26611pt\vbox{\hbox{\hskip-54.26611pt\hbox{\hbox{$\displaystyle\displaystyle\forall
n\leq N.\nobreak\hskip 1.99997pt plus
1.00006pt\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
e_{2}:\tau$}}}\vbox{}}}\over\hbox{\hskip
50.33331pt\vbox{\vbox{}\hbox{\hskip-50.33331pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}\precsim
e_{2}:\tau$}}}}}}$ rel-rand-r $\displaystyle\displaystyle{\hbox{\hskip
84.22221pt\vbox{\hbox{\hskip-84.2222pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\not\in\kern-1.99997pt\textit{Val}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}b{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
50.33331pt\vbox{\vbox{}\hbox{\hskip-50.33331pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}:\tau$}}}}}}$
rel-alloc-tape-l $\displaystyle\displaystyle{\hbox{\hskip
70.73016pt\vbox{\hbox{\hskip-70.73016pt\hbox{\hbox{$\displaystyle\displaystyle\forall\iota.\nobreak\hskip
1.99997pt plus 1.00006pt\iota\hookrightarrow(N,\epsilon)\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\Delta\vDash K{[}\iota{]}\precsim
e:\tau$}}}\vbox{}}}\over\hbox{\hskip
49.37491pt\vbox{\vbox{}\hbox{\hskip-49.3749pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}(N){]}\precsim
e:\tau$}}}}}}$ rel-alloc-tape-r $\displaystyle\displaystyle{\hbox{\hskip
70.44576pt\vbox{\hbox{\hskip-70.44576pt\hbox{\hbox{$\displaystyle\displaystyle\forall\iota.\nobreak\hskip
1.99997pt plus 1.00006pt\iota\hookrightarrow_{\mathsf{s}}(N,\epsilon)\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\Delta\vDash e\precsim
K{[}\iota{]}:\tau$}}}\vbox{}}}\over\hbox{\hskip
49.37491pt\vbox{\vbox{}\hbox{\hskip-49.3749pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash
e\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{tape}}}(N){]}:\tau$}}}}}}$
rel-rand-tape-l $\displaystyle\displaystyle{\hbox{\hskip
101.75627pt\vbox{\hbox{\hskip-101.75627pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,n\cdot\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\vec{n})\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\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
54.04742pt\vbox{\vbox{}\hbox{\hskip-54.04742pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}\precsim
e_{2}:\tau$}}}}}}$ rel-rand-tape-r $\displaystyle\displaystyle{\hbox{\hskip
101.18745pt\vbox{\hbox{\hskip-101.18745pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow_{\mathsf{s}}(N,n\cdot\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow_{\mathsf{s}}(N,\vec{n})\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}n{]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
54.04742pt\vbox{\vbox{}\hbox{\hskip-54.04742pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}:\tau$}}}}}}$
rel-rand-tape-empty-l $\displaystyle\displaystyle{\hbox{\hskip
115.39507pt\vbox{\hbox{\hskip-115.39507pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\epsilon)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\iota\hookrightarrow(N,\epsilon)\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\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
52.65857pt\vbox{\vbox{}\hbox{\hskip-52.65857pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}\precsim
e_{2}:\tau$}}}}}}$ rel-rand-tape-empty-r
$\displaystyle\displaystyle{\hbox{\hskip
144.24884pt\vbox{\hbox{\hskip-144.24883pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\not\in\kern-1.99997pt\textit{Val}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow_{\mathsf{s}}(N,\epsilon)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\iota\hookrightarrow_{\mathsf{s}}(N,\epsilon)\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}n{]}:\tau$}}}}}\vbox{}}}\over\hbox{\hskip
54.04742pt\vbox{\vbox{}\hbox{\hskip-54.04742pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N,\iota){]}:\tau$}}}}}}$
Figure 23. Rules for non-relational probabilistic choices and tapes for the
Clutch refinement judgment. rel-couple-rands
$\displaystyle\displaystyle{\hbox{\hskip
104.19118pt\vbox{\hbox{\hskip-104.19118pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\ \text{bijection}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
K^{\prime}{[}f(n){]}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
73.22243pt\vbox{\vbox{}\hbox{\hskip-73.22243pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}\precsim
K^{\prime}{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}:\tau$}}}}}}$
rel-couple-tape-l $\displaystyle\displaystyle{\hbox{\hskip
192.24255pt\vbox{\hbox{\hskip-192.24255pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\ \text{bijection}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\not\in\kern-1.99997pt\textit{Val}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus 1.00006pt\iota\hookrightarrow(N,\vec{n}\cdot
n)\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}f(n){]}:\tau$}}}}}}\vbox{}}}\over\hbox{\hskip
50.33331pt\vbox{\vbox{}\hbox{\hskip-50.33331pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}:\tau$}}}}}}$
rel-couple-tape-r $\displaystyle\displaystyle{\hbox{\hskip
162.25116pt\vbox{\hbox{\hskip-162.25114pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\ \text{bijection}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow_{\mathsf{s}}(N,\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus
1.00006pt\iota\hookrightarrow_{\mathsf{s}}(N,\vec{n}\cdot f(n))\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\Delta\vDash_{\mathcal{E}}K{[}n{]}\precsim
e_{2}:\tau$}}}}}\vbox{}}}\over\hbox{\hskip
50.33331pt\vbox{\vbox{}\hbox{\hskip-50.33331pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}K{[}\operatorname{\mathsf{\color[rgb]{0.01171875,0.26953125,0.45703125}\definecolor[named]{pgfstrokecolor}{rgb}{0.01171875,0.26953125,0.45703125}{rand}}}(N){]}\precsim
e_{2}:\tau$}}}}}}$ rel-couple-tapes $\displaystyle\displaystyle{\hbox{\hskip
212.73285pt\vbox{\hbox{\hskip-24.23618pt\hbox{\hbox{$\displaystyle\displaystyle
f\leavevmode\nobreak\
\text{bijection}$}}}\vbox{\hbox{\hskip-212.73283pt\hbox{\hbox{$\displaystyle\displaystyle
e_{1}\not\in\kern-1.99997pt\textit{Val}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota\hookrightarrow(N,\vec{n})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\iota^{\prime}\hookrightarrow_{\mathsf{s}}(N,\vec{n}^{\prime})$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\forall n\leq
N.\nobreak\hskip 1.99997pt plus 1.00006pt\iota\hookrightarrow(N,\vec{n}\cdot
n)\mskip 5.0mu{\ast}\mskip
5.0mu\iota^{\prime}\hookrightarrow_{\mathsf{s}}(N,\vec{n}^{\prime}\cdot
f(n))\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}}}\vbox{}}}}\over\hbox{\hskip
28.2142pt\vbox{\vbox{}\hbox{\hskip-28.21419pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}}}$ Figure 24. Coupling rules for the Clutch refinement
judgment. rel-na-inv-open $\displaystyle\displaystyle{\hbox{\hskip
125.92514pt\vbox{\hbox{\hskip-125.92513pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{N}\in\mathcal{E}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\leavevmode\hbox
to13.34pt{\vbox to9.43pt{\pgfpicture\makeatletter\hbox{\hskip
6.67113pt\lower-0.8pt\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{$\displaystyle\displaystyle\mathop{{\triangleright}}P\mskip
5.0mu{\ast}\mskip 5.0mu\mathsf{closeNaInv}_{\mathcal{N}}(P)\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\Delta\vDash_{\mathcal{E}\setminus\mathcal{N}}e_{1}\precsim
e_{2}:\tau$}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.57114pt}{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{{$\displaystyle{\,P\,}\mathstrut$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{}{{}{}}{}{{}}{}
{{}}{}{{}{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{0.2pt,1.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-6.57114pt}{-0.35pt}\pgfsys@moveto{-6.57114pt}{-0.35pt}\pgfsys@lineto{-6.57114pt}{8.53331pt}\pgfsys@lineto{6.57114pt}{8.53331pt}\pgfsys@lineto{6.57114pt}{-0.35pt}\pgfsys@closepath\pgfsys@moveto{6.57114pt}{8.53331pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{$\displaystyle\displaystyle\mathop{{\triangleright}}P\mskip
5.0mu{\ast}\mskip 5.0mu\mathsf{closeNaInv}_{\mathcal{N}}(P)\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\Delta\vDash_{\mathcal{E}\setminus\mathcal{N}}e_{1}\precsim
e_{2}:\tau$} \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}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{{\triangleright}}P\mskip
5.0mu{\ast}\mskip 5.0mu\mathsf{closeNaInv}_{\mathcal{N}}(P)\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\Delta\vDash_{\mathcal{E}\setminus\mathcal{N}}e_{1}\precsim
e_{2}:\tau$}}}}}\vbox{}}}\over\hbox{\hskip
28.2142pt\vbox{\vbox{}\hbox{\hskip-28.21419pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}}}$ rel-na-inv-close $\displaystyle\displaystyle{\hbox{\hskip
88.15111pt\vbox{\hbox{\hskip-88.1511pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{{\triangleright}}P$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{closeNaInv}_{\mathcal{N}}(P)$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}}\vbox{}}}\over\hbox{\hskip
32.49197pt\vbox{\vbox{}\hbox{\hskip-32.49197pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}\setminus\mathcal{N}}e_{1}\precsim
e_{2}:\tau$}}}}}}$ rel-na-inv-alloc $\displaystyle\displaystyle{\hbox{\hskip
62.35114pt\vbox{\hbox{\hskip-62.35114pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{{\triangleright}}P$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\leavevmode\hbox
to13.34pt{\vbox to9.43pt{\pgfpicture\makeatletter\hbox{\hskip
6.67113pt\lower-0.8pt\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}{-5.57114pt}{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{{$\displaystyle{\,P\,}\mathstrut$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{}{{}{}}{}{{}}{}
{{}}{}{{}{}}{}{{}}{}{}{}{}{{}}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{0.2pt,1.0pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.2pt}\pgfsys@invoke{
}{}\pgfsys@moveto{-6.57114pt}{-0.35pt}\pgfsys@moveto{-6.57114pt}{-0.35pt}\pgfsys@lineto{-6.57114pt}{8.53331pt}\pgfsys@lineto{6.57114pt}{8.53331pt}\pgfsys@lineto{6.57114pt}{-0.35pt}\pgfsys@closepath\pgfsys@moveto{6.57114pt}{8.53331pt}\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}}\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\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}\vbox{}}}\over\hbox{\hskip
28.2142pt\vbox{\vbox{}\hbox{\hskip-28.21419pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vDash_{\mathcal{E}}e_{1}\precsim
e_{2}:\tau$}}}}}}$ Figure 25. Non-atomic invariant access rules for the Clutch
refinement judgment.