commands for field lookup and mutation as map operations. For example, the
mutation $x.f\coloneqq y$ is encoded as $M_{f}[x]:=y$.

_Modeling Allocation. _ We model programs in a safe garbage-collected
programming language. We introduce a ghost global variable $\mathit{Alloc}$ to
model the allocated set of objects in the program. We then add several
assumptions (i.e., $\mathsf{assume}$ statements) throughout the program.
Specifically, we assume for every program parameter of type Object, the
parameter itself as well as the values of the monadic maps of type Object/Set-
of-Objects on the parameter are all contained in $\mathit{Alloc}$. For
example, in the case of our running example (Example 3.6), we add the
assumptions $x\in\mathit{Alloc}$ and
$\mathit{next}(x)\neq\mathit{nil}\Rightarrow\mathit{next}(x)\in\mathit{Alloc}$.
If we had a monadic map $\mathit{hslist}$ corresponding to the heaplet of the
sorted list, we would also add the assumption
$\mathit{hslist}(x)\subseteq\mathit{Alloc}$. Similarly, whenever an object is
dereferenced on a field of type Object/Set-of-Objects in the program, we add
an assumption that the resulting value is contained in $\mathit{Alloc}$. Note
that these are quantifier-free assumptions. They can be added soundly since
they are valid under the semantics of the underlying language.

We then model allocation by introducing a new object to $\mathit{Alloc}$ and
ensure that the default values of the various fields on the newly allocated
object belong to $\mathit{Alloc}$. These constraints can be expressed using a
quantifier-free formula over maps.

_Modeling Heap Change Across Function Calls. _ The main challenge in modeling
function calls is to ensure the ability to do frame reasoning. To do this, we
extend the programming language with a _modified set_ annotation for methods.
We require the modified set to be a term of type Set-of-Objects that is
constructed using object variables in the current scope and monadic maps over
them. In the case of our running example (Example 3.1), we would add a monadic
map $\mathit{hslist}$ of type Set-of-Objects corresponding to the heaplet of
the sorted list and annotate the program with $\mathit{hslist}(x)$ as the
modified set. Figure 7 shows the full version of sorted list insertion with
the modified set annotation.

Given a modified set $\mathit{Mod}$, we model changes to the heap across a
function call by introducing new maps corresponding to the various fields
(including monadic maps) after the call. We then add assumptions that the
values of the new maps are equal to the values of the maps before the call on
all locations that do not belong to the modified set $\mathit{Mod}$. Although
this constrains the maps on unboundedly many objects, it can be written
without quantifiers by using pointwise operators on maps (de Moura and
Bjørner, 2009). Formally, for a field $f$ modeled as a map $M_{f}$, we
introduce a new map $M_{f}^{\prime}$ and update $M_{f}$ as:

$M_{f}[x]:=\mathit{ite}(x\in\mathit{Mod},\,M_{f}^{\prime}[x],\,M_{f}[x])$

The above update can be expressed using pointwise operators as
$M_{f}\coloneqq\mathit{ite}(\mathit{Mod},M_{f}^{\prime},M_{f})$, where the
$\mathit{ite}$ operator is applied pointwise over the maps $\mathit{Mod}$,
$M_{f}$, and $M_{f}^{\prime}$. The value of the field $f$ on an object $x$
after the call will then be equal to $x.f$ before the call if $x$ was not
modified, and a _havoc_ -ed value given by $M_{f}^{\prime}$ otherwise.
Pointwise operators are supported by the generalized array theory (de Moura
and Bjørner, 2009) whose quantifier-free fragment is decidable.

Program verifiers like Boogie (Qadeer, 2023) offer VC generation frameworks
that are amenable to the modeling described in this section. Indeed, our
implementation of the IDS/FWYB methodology described in Section 5.1 uses
Boogie.

##  Appendix B Proofs of Soundness for Stages 1, 2, and 3 of FWYB

In this section we detail the proofs of soundness for the various stages of
the FWYB methodology. We first introduce some notation and show some
preliminary lemmas.

_Projection for Configurations. _ The stages of FWYB deal with two kinds of
triples, one whose validity is stated with respect to configurations that
interpret ghost variables and maps, and one over configurations that only
interpret user variables and fields. Given a configuration $C$ that interprets
ghost variables/maps, we denote by $\hat{C}$ the projection of that
configuration to user variables that simply eliminates all ghost
interpretations. Conversely, given a configuration $c$ we say that $C$ extends
$c$ with an interpretation for ghost variables/maps if $\hat{C}=c$. We define
$\hat{bot}=\bot$.

_Lemmas About Projection that Eliminates Ghost Code. _ We show the following
lemmas about projection that eliminates ghost code (Definition A.1). We assume
that there is only one procedure $M$ in the program for simplicity of
presentation. Recall that $M$ can contain ghost code and $\hat{M}$ is the
projection of $M$ that eliminates the ghost code (with appropriately modified
input/output parameters).

###### Lemma B.1.

Let $C_{1}$ be a configuration that interprets ghost variables/maps. If $M$ is
a “pure ghost” program, (i.e., a yield of $\mathit{GP}$ in the grammar in
Figure 6), then $M$ always terminates starting from $C_{1}$.

The above lemma says that pure ghost programs always terminate. It follows
directly from the definition of ghost code which requires pure ghost loops and
functions to be terminating.∎

###### Lemma B.2.

Let $c$ be a configuration that does not interpret ghost variables/maps. If
$\hat{M}$ (projected code that does not contain ghost code) terminates
starting from $c$, then $M$ (which contains additional ghost code) must
terminate starting from any configuration $C$ that extends $c$.

The above lemma says that the termination of the original user program is
preserved by any augmentation with ghost code. In a certain sense, it ‘lifts’
Lemma B.1 to programs that contain both user and ghost code.

###### Proof.

The lemma follows from structural induction on the definition of projection,
i.e., on the structure of the grammar for the nonterminal $P$ in Figure 6. The
argument for basic statements is trivial. For pure ghost programs the result
follows from Lemma B.1. The argument for all compositions (sequential,
conditional, loop) and function calls follows from the induction hypothesis. ∎

###### Lemma B.3.

Let $C_{1}$ be a configuration that interprets ghost variables/maps. If $M$ is
a “pure ghost” program and $M$ starting from $C_{1}$ reaches some $C_{2}$ and
$C_{2}\neq\bot$, then $\hat{C_{1}}=\hat{C_{2}}$.

The above lemma says that ghost code does not affect the values of user (non-
ghost) variables and maps. It follows trivially by structural induction on the
$\mathit{GP}$ grammar, using the definition of operational semantics (Figure
5). The key observation is that $\mathit{GP}$ syntactically disallows non-
ghost variables/maps to read from ghost variables/maps.∎

We can similarly ‘lift’ the above lemma to programs that contain both user
code and ghost code.

###### Lemma B.4.

Let $c$ be a configuration that does not interpret ghost variables/maps. If
$\hat{M}$ starting from $c_{1}$ reaches some $c_{2}$, then $M$ starting from
any configuration $C_{1}$ that extends $c_{1}$ must either reach $\bot$ or
some $C_{2}$ that extends $c_{2}$.

The above lemma says that augmentation with ghost code does not affect how the
original program executes.

###### Proof.

As with Lemma B.2, we proceed by structural induction on the grammar for $P$
in Figure 6. The argument for basic non-ghost statements follows trivially
from the definition of operational semantics. They key observation is that
non-ghost statements do not affect the values of ghost variables/maps (ensured
by the syntactic restrictions). For pure ghost programs the result follows
from Lemma B.3. The argument for all compositions (sequential, conditional,
loop) and function calls follows from the induction hypothesis. ∎

## Proof of Proposition 3.4

We can state the proposition simply as follows: if
$\langle\,\mathit{LC}\land\psi_{\mathit{pre}}\,\rangle\;M\;\langle\,\mathit{LC}\land\psi_{\mathit{post}}\,\rangle$
is valid, then $\langle\,\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{pre}}\,\rangle\;\hat{M}\;\langle\,\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}\,\rangle$ is
valid.

Fix configurations (without ghost state) $c_{1},c_{2}$ such that $c_{1}$
satisfies $\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{pre}}$ and $\hat{M}$
starting from $c_{1}$ reaches $c_{2}$. To show that the given Hoare triple for
$\hat{M}$ is valid, we must establish that $c_{2}$ is not $\bot$, and further
that $c_{2}$ satisfies $\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}$.

Since $c_{1}\models\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{pre}}$, by the
semantics of second order logic there exists a configuration (taken as a
model) extending $c_{1}$, say $C_{1}$, such that
$C_{1}\models\mathit{LC}\land\psi_{\mathit{pre}}$. First, using Lemma B.2 we
have that $M$ starting from $C_{1}$ must terminate. Further, since the triple
$\langle\,\mathit{LC}\land\psi_{\mathit{pre}}\,\rangle\;M\;\langle\,\mathit{LC}\land\psi_{\mathit{post}}\,\rangle$
is valid, it must be the case that $M$ starting from $C_{1}$ reaches some
$C_{2}$ such that $C_{2}\neq\bot$ and
$C_{2}\models\mathit{LC}\land\psi_{\mathit{post}}$.

We now use Lemma B.4 to conclude that $\hat{C_{2}}=c_{2}$. Since
$C_{2}\neq\bot$, we have that $c_{2}\neq\bot$. Further, since
$C_{2}\models\mathit{LC}\land\psi_{\mathit{post}}$, we have from the semantics
of the logic that $C_{2}\models\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}$.

Observe that the formula $\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}$ is stated over
the common vocabulary of $C_{2}$ and $c_{2}$, where the interpretations of the
two configurations agree. Therefore, we can conclude that $c_{2}\models\exists
g_{1},g_{2}\ldots,g_{k}.\,\mathit{LC}\land\psi_{\mathit{post}}$. This
concludes the proof.∎

### Proof of Proposition 3.5

The proof of Proposition 3.5 is similar to the above proof for Proposition
3.4, except that we must now consider a definition of ghost code (akin to the
development in Section A.2) that only considers the variable $\mathit{Br}$ as
ghost.

Repeating the arguments in the proof of Proposition 3.4 appropriately, we
obtain that if

$\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\land\mathit{Br}=\emptyset\,\rangle\;P_{\mathcal{G},\mathit{Br}}(\overline{x},\mathit{Br},\,\mathit{ret}\\!:\,\overline{y},\mathit{Br})\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\land\mathit{Br}=\emptyset\,\rangle$

is valid, then

$\langle\,\exists\mathit{Br}.\,\big{(}(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\land\mathit{Br}=\emptyset\big{)}\,\rangle\;P_{\mathcal{G}}(\overline{x},\,\mathit{ret}\\!:\,\overline{y})\;\langle\,\exists\mathit{Br}.\,\big{(}(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\land\mathit{Br}=\emptyset\big{)}\,\rangle$

is valid. This triple can be simplified to $\langle\,(\forall
z.\,\rho(z))\land\alpha\,\rangle\;P_{\mathcal{G}}(\overline{x},\,\mathit{ret}\\!:\,\overline{y})\;\langle\,(\forall
z.\,\rho(z))\land\beta\,\rangle$, which concludes the proof.

## Proof of Proposition 3.7

Given a well-behaved program $P$ such that $\\{\alpha\\}\;P\;\\{\beta\\}$ is
valid, we must show that $\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\alpha\,\rangle\;P\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho(z))\land\beta\,\rangle$ is valid.

The proof proceeds by an induction on the nesting depth of method calls in a
trace of the program $P$. We elide this level of induction here because it is
routine. Importantly, given a particular execution of the program $P$, we must
show that the claim holds, assuming it holds for all method calls occurring in
the execution. We show this by structural induction on the proof of well-
behavedness of $P$.

There are several base cases.

Skip/Assignment/Lookup/Return There is nothing to show for skip, assignment,
lookup, or return statements. These do not change the heap at all and the rule
does not update $\mathit{Br}$ either, therefore if
$\langle\,\alpha\,\rangle\;\mathsf{stmt}\;\langle\,\beta\,\rangle$ is valid
then certainly $\langle\,(\forall
z\notin\mathit{Br}.\,\rho)\land\alpha\,\rangle\;\mathsf{stmt}\;\langle\,(\forall
z\notin\mathit{Br}.\,\rho)\land\beta\,\rangle$ is valid.

Mutation The claim is true for the mutation rule since by the premise of the
rule we update the broken set with the impact set consisting of all potential
objects where local conditions may not hold.

Function Call Here we simply appeal to the induction hypothesis.

Allocation We refer to our operational semantics, which ensures that no object
points to a freshly allocated object. Therefore, the allocation of an object
could have only broken the local conditions on itself at most.

Infer LC Outside Br There is nothing to prove for this rule as it does not
alter the $\mathit{Br}$ set at all.

Assert LC and Remove The claim holds for this rule by construction. If
$\mathit{LC}$ holds everywhere outside $\mathit{Br}$ , and we know that
$\mathit{LC}(x)$ holds, then we can conclude that $\mathit{LC}$ holds
everywhere outside $\mathit{Br}\setminus\\{x\\}$.

It only remains to show that the claim holds for larger well-behaved programs
obtained by composing smaller well-behaved programs using sequencing,
branching, or looping constructs. The proof here is trivial as the argument
for sequencing is trivial (we can think of a loop as unboundedly many
sequenced compositions of the smaller well-behaved program): we can _always_
compose two well-behaved programs to obtain a well-behaved program.∎

##  Appendix C Details For Well-Behaved Programming

### General Construction for Automatically Checking Correctness of Impact Sets

Fix a class with maps $\mathcal{F}\cup\mathcal{G}=\\{f_{1},f_{2},\ldots
f_{n}\\}$ (includes both original and ghost fields) and an intrinsic
definition $(\mathcal{G},\mathit{LC},\varphi)$ over which we prove correctness
of programs. Without loss of generality, let $f_{1},\ldots f_{k}$ for some
$k\leq n$ alone correspond to pointer fields (where the range is an object);
the others we assume are data fields that range over background sorts. In the
sequel we assume for simplicity that $\mathit{LC}(x)$ only relates the fields
of $x$ with those of $f_{i}(x)$ for $1\leq i\leq k$, i.e., the local
conditions only constrain the fields of $x$ with those of its neighboring
objects that are “one pointer hop” away from $x$.

Consider a mutation $x.f\coloneqq y$ for some $f$ in $f_{1}$ through $f_{n}$
and an arbitrary $y$. It is clear that the only set of objects whose local
condition can be impacted by this mutation are those that are one pointer hop
away via an incoming or outgoing edge in the heap (seen as a directed graph
with labeled edges corresponding to pointers), apart from $x$ itself. In
general there can be unboundedly many such objects, but in our work we only
handle impact sets that can be expressed as a finite set of terms over $x$
(see Section 3.5 under ‘Rules for Constructing Well-Behaved Programs’). Note
here that the impact set can be larger than the set of impacted objects as we
only require that objects not belonging to the impact set retain that
$\mathit{LC}$ holds on them under mutation. However, we attempt here to
construct of impact sets that are as small as possible.

Following the above discussion, let us assume that the impact set consists of
terms from the following set:

$\mathit{ImpactableObjects}=\\{x,f_{1}(x),\ldots
f_{k}(x)\\}\cup\\{\mathit{old}(f(x))\,|\,f\textrm{ is a pointer field}\\}$

The reader may be inclined to suggest here that when $f$ is a pointer field,
$y$ (the new value of $f(x)$) may also belong to the minimal impact set.
However, this is not possible in general since $y$ is arbitrary, and in
particular $y$ can be an object in the heap that is “far away” from $x$, i.e.,
not one pointer hop away (either incoming or outgoing). The same argument
applies to terms over $y$. Therefore, if the (minimal) impact set is at all
expressible as a set of terms over the vocabulary of the mutation statement it
must be a subset of the terms in the set $\mathit{ImpactableObjects}$ defined
above.

Let this subset of terms be $A$. We then generate the following triple to
check that $A$ is in fact an impact set:

$\vdash\;\\{(\bigwedge_{t\in A}u\neq t)\land\mathit{LC}(u)\land
x\neq\mathit{nil}\\}\;x.f:=y\;\\{\mathit{LC}(u)\\}$

The triple says that any location $u$ that is not $A$ which satisfied
$\mathit{LC}$ before the mutation must continue to satisfy it after the
mutation. As discussed in the main text, this validity of this triple can be
check effectively by decision procedures over quantifier-free combinations of
theories that are supported by SMT solvers (De Moura and Bjørner, 2008;
Barrett et al., 2011).

Finally, we can compute a provably correct and minimal impact set
automatically, if one exists, by considering subsets of
$\mathit{ImpactableObjects}$ in turn and checking the corresponding triple as
described above. However, in our experiments we compute impact sets manually
and check their correctness automatically.

##  Appendix D Details for Case Studies in Section 4

In this appendix we provide further details for the various case studies
discussed in the main text and detail some other case studies not featured in
the main text.

###  D.1. Discussion on Sorted List Insertion (Section 4.1)

     pre: $\mathit{Br}=\emptyset$
     post: $\mathit{LC}(r)\,\land\,\mathit{prev}(r)=\mathit{nil}$
             $\land\mathit{Br}=\,\mathit{ite}(\mathit{old}(\mathit{prev}(x))=\mathit{nil},\,\emptyset,\,\{\mathit{old}(\mathit{prev}(x))\})$
             $\land\mathit{length}(r)=\,\mathit{old}(\mathit{length}(x))+1$
             $\land\mathit{keys}(r)=\,\mathit{old}(\mathit{keys}(x))\cup\{k\}$
             $\land\mathit{old}(\mathit{hslist}(x))\subset\mathit{hslist}(r)$
     modifies: $\mathit{hslist}(x)$
     sorted_list_insert(x: C, k: Int, Br: Set(C))
     returns r: C, Br: Set(C)
     {
       InferLCOutsideBr(x, Br);
       if (x.key $\geq$ k) then { // k inserted before x
         NewObj(z, Br);         // {z}
            Mut(z, key, k, Br);    // {z} since z.prev = nil
            Mut(z, next, x, Br);   // {z} since z.next = nil
            Mut(z, hslist, {z} $\cup$ x.hslist, Br); // {z}
            Mut(z, length, 1 + x.length, Br);    // {z}
            Mut(z, keys,  {k} $\cup$ x.keys, Br);    // {z}
            Mut(x, prev, z, Br);     // {z, x, old(prev(x))}
            AssertLCAndRemove(z, Br);  // {x, old(prev(x))}
            AssertLCAndRemove(x, Br); // {old(prev(x))}
            r := z;
       }
       else {
       if (x.next = nil) then { // one-element list
            NewObj(z, Br);
            Mut(z, key, k, Br);
            Mut(z, next, nil, Br);
            Mut(z, hslist, {z}, Br);
            Mut(z, length, 1, Br);
            Mut(z, keys, {k}, Br);
            Mut(x, next, z, Br);

            Mut(z, prev, x, Br);
            AssertLCAndRemove(z, Br);
            Mut(x, prev, nil, Br);
            Mut(x, hslist, {x} $\cup$ {z}, Br);
            Mut(x, length, 2, Br);
            Mut(x, keys, {x.key} $\cup$ {k}, Br);
            AssertLCAndRemove(x, Br);
            r := x;
       }
       else { // recursive case
            y := x.next;
            InferLCOutsideBr(y, Br);
            tmp, Br := sorted_list_insert(y, k, Br);   // {x}
            InferLCOutsideBr(y, Br);
            if (y.prev = x) then {
              Mut(y, prev, nil, Br);    // {y, x}
            }
            Mut(x, next, tmp, Br);      // {y, x}
            AssertLCAndRemove(y, Br);   // {x}
            Mut(tmp, prev, x, Br);      // {tmp, x}
            AssertLCAndRemove(tmp, Br); // {x}
            Mut(x, hslist, {x} $\cup$ tmp.hslist, Br);  // {x, prev(x)}
            Mut(x, length, 1 + tmp.length, Br);      // {x, prev(x)}
            Mut(x, keys, {x.key} $\cup$ tmp.keys, Br);  // {x, prev(x)}
            Mut(x, prev, nil, Br);           // {x, old(prev(x))}
            AssertLCAndRemove(x, Br);   // {old(prev(x))}
            r := x;
       }}
     }

Figure 7. Code for insertion into a sorted list written in the syntactic
fragment for well-behaved programs(Section 4.1). Black lines denote code
written by the user, and blue lines denote lines written by the verification
engineer. The comments on the right show the state of the broken set
$\mathit{Br}$ after the statement on the corresponding line.

We provide the specifications and the code augmented with ghost annotations in
Figure 7.

Specifications. The precondition states that the broken set is empty at the
beginning of the program. The postcondition states that the returned object
$r$ satisfies the local conditions and satisfies the correlation formula for a
sorted list (i.e., $\mathit{prev}(r)=\mathit{nil}$). However, the broken set
is only empty if the input object $x$ was the head of a sorted list, and it is
$\\{\mathit{prev}(x)\\}$ otherwise. The other conjuncts express functional
specifications for insertion in terms of the length, heaplet, and set of keys.
We also add a ‘modifies’ clause which enables program verifiers for heap
manipulating programs to utilize frame reasoning across function calls.

Summary. The proof works at a high-level as follows: we recurse down the list,
reaching the appropriate object $x$ before which the new key must be inserted.
This is the first branch in Figure 7, and we show the broken set at each point
in the comments to the right. We create the new object $z$ with the
appropriate key and point $z.\mathit{next}$ to $x$. We then fix the local
conditions on $x$ and $z$. However, these fixes break the $\mathit{LC}$ on
$\mathit{old}(\mathit{prev}(x))$. We maintain this property up the recursion,
at each point fixing $\mathit{LC}$ on $x$ and breaking it on
$\mathit{old}(\mathit{prev}(x))$ in the process. This is shown in the last
branch in the code. We eventually reach the head of the sorted list, whose
$\mathit{prev}$ in the pre state is $\mathit{nil}$, and at that point the
fixes do not break anything else, i.e., the broken set is empty (as desired).

The verification engineer adds ghost code to perform these fixes as shown in
blue in Figure 7. We can also see that there are essentially as many lines of
ghost code as there are lines of user code; we compare these values across our
benchmark suite (see Table 2) and find that this is typical for many methods.
However, the verification conditions for the (augmented) program are
_decidable_ because they can be stated using quantifier-free formulas over
decidable combinations of theories including maps, map updates, and sets.

###  D.2. BST Right-Rotation

We now turn to another data structure and method that illustrates intrinsic
definitions for trees, namely verifying a right rotate on a binary search
tree. Such an operation is a common tree operation, and rotations are used
widely in maintaining balanced search trees, such as AVL and Red-Black Trees,
on which several of our benchmarks operate.

We augment the definition of binary trees discussed in Section 1 to include
the $min:BST\rightarrow Real$ and $max:BST\rightarrow Real$ maps, which
capture the minimum and maximum keys stored in the tree rooted at a node, to
help enforce binary search tree properties locally. The local condition and
the impact sets are as below:

$\displaystyle\mathit{LC}\equiv\forall x.\,min(x)$ $\displaystyle\leq
key(x)\leq max(x)$ $\displaystyle\land~{}(p(x)\neq\mathit{nil}\Rightarrow$
$\displaystyle l(p(x))=x\lor r(p(x))=x)$
$\displaystyle\land~{}(l(x)=nil\Rightarrow$ $\displaystyle min(x)=key(x))$
$\displaystyle\land~{}(l(x)\neq\mathit{nil}\Rightarrow$ $\displaystyle
p(l(x))=x\land rank(l(x))<rank(x)$
$\displaystyle\\!\\!\\!\\!\\!\land~{}max(l(x))<key(x)~{}\land~{}min(x)=min(l(x)))$
$\displaystyle\land~{}(r(x)=nil\Rightarrow$ $\displaystyle max(x)=key(x))$
$\displaystyle\land~{}(r(x)\neq\mathit{nil}\Rightarrow$ $\displaystyle
p(r(x))=x\land rank(r(x))<rank(x)$
$\displaystyle\\!\\!\\!\\!\\!\land~{}min(r(x))>key(x)~{}\land~{}max(x)=max(r(x)))$

Mutated Field $f$ |  Impacted Objects $A_{f}$
---|---
$l$ | $\\{x,\mathit{old}(l(x))\\}$
$r$ | $\\{x,\mathit{old}(r(x))\\}$
$p$ | $\\{x,\mathit{old}(p(x))\\}$
key | $\\{x\\}$
min | $\\{x,p(x)\\}$
max | $\\{x,p(x)\\}$
rank | $\\{x,p(x)\\}$

We first describe the gist of how the data structure is repaired and provide
the fully annotated program below. Recall that in a BST right rotation, that
there are two nodes $x$ and $y$ such that $y$ is $x$’s left child. After the
rotation is performed, $y$ becomes the new root of the subtree, while $x$
becomes $y$’s right child. Several routine updates of the monadic map $p$
(parent) will have to be made. The most interesting update is that of the
$rank:BST\rightarrow Real$ map. Since $y$ is now the root of the affected
subtree, its rank must be greater than all its children. One way of doing this
is to increase $y$’s rank to something greater than $x$’s rank. This works if
$y$ has no parent, but not in general. To solve this issue, we use the density
of the Reals to set the rank of $y$ to $(rank(x)+rank(p(y)))/2$. Note that
there are a fixed number of ghost map updates, as the various monadic maps for
distant ancestors and descendents of $x,y$ do not change (the min/max of
subtrees of such nodes do not change).

We present the fully annotated program below, with comments displaying the
state of the broken set $Br$ at the corresponding point in the program.

     pre: $\mathit{Br}=\emptyset\land l(x)\neq\mathit{nil}\land p(x)=xp$
     post: $\mathit{Br}=\emptyset\land p(ret)=xp$
           $\land l(ret)=\mathit{old}(l(l(x)))\land ret=\mathit{old}(l(x))\land r(ret)=x$
           $\land l(r(ret))=\mathit{old}(r(l(x)))\land r(r(ret))=\mathit{old}(r(x))$
     bst_right_rotate(x: BST, xp: BST?, Br: Set(BST))
     returns ret: BST, Br: Set(BST)
     {
       LCOutsideBr(x, Br);
       if (xp $\neq$ nil) then {
            LCOutsideBr(xp, Br);
       }
       if (x.l $\neq$ nil) then {
            LCOutsideBr(x.l, Br);
       }
       if (x.l $\neq$ nil $\land$ x.l.r $\neq$ nil) then {
            LCOutsideBr(x.l.r, Br);
       }
       var y := x.l;                // {}
       Mut(x, l, y.r, Br);          // {x, y}
       if (xp $\neq$ nil) then {
            if (x = xp.l) then {
                Mut(xp, l, y, Br);  // {xp, x, y}
            }
            else {
                Mut(xp, r, y, Br);  // {xp, x, y}
            }
       }
       Mut(y, r, x, Br);            // {xp, x, y, x.l} (Note: x.l == old(y.r))
       // (1): Repairing x.l
       if (x.l $\neq$ nil) then {
            Mut(x.l, p, x, Br);     // {xp, x, y, x.l}
       }
       // (2): Repairing x
       Mut(x, p, y, Br);            // {xp, x, y, x.l}
       Mut(x, min, if x = nil then x.k else x.l.min, Br);    // {xp, x, y, x.l}
       // (3): Repairing y
       Mut(y, p, xp, Br);           // {xp, x, y, x.l}
       Mut(y, max, x.max, Br);      // {xp, x, y, x.l}
       Mut(y, rank, if xp = nil then x.rank+1 else (xp.rank+x.rank)/2, Br);     // {xp, x, y, x.l}
       AssertLCAndRemove(x.l, Br);  // {xp, x, y}
       AssertLCAndRemove(x, Br);    // {xp, y}
       AssertLCAndRemove(y, Br);    // {xp}
       AssertLCAndRemove(xp, Br);   // {}
       ret := y // return y
     }

###  D.3. Discussion on Sorted List Reversal (Section 4.2)

What follows are the complete local conditions and impact sets for Sorted List
Reverse:

$\displaystyle\mathit{LC}\equiv\forall x.\,\mathit{prev}(x)\neq\mathit{nil}\Rightarrow$ $\displaystyle\mathit{next}(\mathit{prev}(x))=x$ $\displaystyle\land~{}\mathit{next}(x)\neq\mathit{nil}\Rightarrow$ $\displaystyle\mathit{prev}(\mathit{next}(x))=x$ $\displaystyle\land~{}\mathit{length}(x)=\mathit{length}(\mathit{next}(x))+1$ $\displaystyle\land~{}\mathit{keys}(x)=\mathit{keys}(\mathit{next}(x))\cup\\{\mathit{key}(x)\\}$ $\displaystyle\land~{}\mathit{hslist}(x)=\mathit{hslist}(\mathit{next}(x))\uplus\\{x\\}$ $\displaystyle\land~{}\mathit{sorted}(x)\Rightarrow\mathit{key}(x)\leq\mathit{key}(\mathit{next}(x))$ $\displaystyle\qquad\qquad\qquad\land\mathit{sorted}(x)=\mathit{sorted}(\mathit{next}(x))$ $\displaystyle\land~{}\mathit{rev\\_sorted}(x)\Rightarrow\mathit{key}(x)\geq\mathit{key}(\mathit{next}(x))$ $\displaystyle\qquad\qquad\qquad\land\mathit{rev\\_sorted}(x)=\mathit{rev\\_sorted}(\mathit{next}(x))$ $\displaystyle~{}~{}~{}~{}~{}\land~{}(\mathit{next}(x)=\mathit{nil}\Rightarrow$ $\displaystyle\mathit{length}(x)=1\land\mathit{keys}(x)=\\{x\\}\land\mathit{hslist}(x)=\\{x\\})$ Figure 9. Full local condition for lists for Sorted List Reverse Mutated Field $f$ | Impacted Objects $A_{f}$
---|---
$\mathit{next}$ | $\\{x,\mathit{old}(\mathit{next}(x))\\}$
$\mathit{key}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{prev}$ | $\\{x,\mathit{old}(\mathit{prev}(x))\\}$
$\mathit{length}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{keys}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{hslist}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{sorted}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{rev\\_sorted}$ | $\\{x,\mathit{prev}(x)\\}$
Table 3. Full impact sets for lists for Sorted List Reverse

The following program reverses a sorted list as defined by the local condition
above. We annotate this program with comments on the current composition of
the broken set according to the rules of Table 3.

     pre: $\mathit{Br}=\emptyset\land\varphi(x)\land\mathit{sorted}(x)$
     post: $\mathit{Br}^{\prime}=\emptyset\land\varphi(ret)\land\mathit{rev\_sorted}(ret)\land\mathit{keys}(ret)=\mathit{old}(\mathit{keys}(x))\land\mathit{hslist}(ret)=\mathit{old}(\mathit{hslist}(x))$
     sorted_list_reverse(x: C, Br: Set(C))
     returns ret: C, Br: Set(C)
     {
       LCOutsideBr(x, Br);
       var cur := x;
       ret := null;
       while (cur $\neq$ nil)
          invariant $cur\neq\mathit{nil}\Rightarrow LC(cur)\land\mathit{sorted}(cur)\land\varphi(cur)$
          invariant $ret\neq\mathit{nil}\Rightarrow LC(ret)\land\mathit{rev\_sorted}(ret)\land\varphi(ret)$
          invariant $cur\neq\mathit{nil}\land ret\neq\mathit{nil}\Rightarrow\mathit{key}(ret)\leq key(cur)$
          invariant $\mathit{old}(\mathit{keys}(x))=\mathit{ite}(cur=\mathit{nil},\emptyset,\mathit{keys}(cur))\cup\mathit{ite}(ret=\mathit{nil},\emptyset,\mathit{keys}(ret))$
          invariant $\mathit{old}(\mathit{hslist}(x))=\mathit{ite}(cur=\mathit{nil},\emptyset,\mathit{hslist}(cur))\cup\mathit{ite}(ret=\mathit{nil},\emptyset,\mathit{hslist}(ret))$
          invariant $Br=\emptyset$
          decreases $\mathit{ite}(cur\neq\mathit{nil},0,\mathit{length}(cur))$
       {
          var tmp := cur.next;                // {}
          if (tmp $\neq$ nil) then {
            LCOutsideBr(tmp, Br);             // {}
            Mut(tmp, p, nil, Br);             // {cur, tmp}
          }
          Mut(cur, next, ret, Br);            // {cur, tmp}
          if (ret $\neq$ nil) then {
            Mut(ret, p, cur, Br);             // {cur, tmp, ret}
          }
          Mut(cur, keys,
            {cur.k} $\cup$ (if cur.next=nil then $\varphi$ else cur.next.keys), Br);    // {cur, tmp, ret}
          Mut(cur, hslist,
            {cur} $\cup$ (if cur.next=nil then $\varphi$ else cur.next.hslist), Br);    // {cur, tmp, ret}
          if (cur.next $\neq$ nil $\land$ (cur.key $>$ cur.next.key $\lor$ $\neg$cur.next.sorted)) {
            Mut(cur, sorted, false, Br);      // {cur, tmp, ret}
          }
          Mut(cur, rev_sorted, true, Br);     // {cur, tmp, ret}
          AssertLCAndRemove(cur, Br);         // {tmp, ret}
          AssertLCAndRemove(ret, Br);         // {tmp}
          AssertLCAndRemove(tmp, Br);         // {}
          ret := cur;
          cur := tmp;
       }
       // The current value of ret is returned
     }

###  D.4. Discussion on Circular List Insert Back (Section 4.3)

We first provide the local conditions and impact sets for circular lists.

$\displaystyle\mathit{LC}\equiv\forall x.\,\mathit{next}(x)\neq\mathit{nil}$
$\displaystyle\land\;\mathit{prev}(x)\neq\mathit{nil}$
$\displaystyle\land\;~{}~{}~{}\mathit{next}(\mathit{prev}(x))$
$\displaystyle=\;x\;\land\;\mathit{prev}(\mathit{next}(x))\;=\;x$
$\displaystyle\land~{}\mathit{last}(x)=x\Rightarrow$
$\displaystyle\mathit{length}(x)=0\land\mathit{rev\\_length}(x)=0$
$\displaystyle\land~{}\mathit{last}(x)=\mathit{last}(\mathit{next}(x))$
$\displaystyle\land~{}\mathit{next}(x)=x\Rightarrow\mathit{keys}(x)=\emptyset\land\mathit{hslist}(x)=\\{x\\}$
$\displaystyle\land~{}\mathit{next}(x)\neq
x\Rightarrow\mathit{keys}(x)=\mathit{keys}(\mathit{next}(x))\hskip
80.00012pt\text{(C1)}$
$\displaystyle\qquad\qquad\qquad\quad\;\land\mathit{hslist}(x)=\\{x\\}\cup\mathit{hslist}(\mathit{next}(x))\hskip
41.00012pt\text{(C2)}$ $\displaystyle\land~{}\mathit{last}(x)\neq
x\Rightarrow$
$\displaystyle\mathit{length}(x)=\mathit{length}(\mathit{next}(x))+1$
$\displaystyle\land~{}\mathit{rev\\_length}(x)=\mathit{rev\\_length}(\mathit{prev}(x))+1$
$\displaystyle\land~{}\mathit{next}(x)=\mathit{last}(x)\Rightarrow\mathit{keys}(x)=\\{\mathit{key}(x)\\}\land\mathit{hslist}(x)=\\{x\\}$
$\displaystyle\land~{}\mathit{next}(x)\neq\mathit{last}(x)\Rightarrow\mathit{keys}(x)=\\{\mathit{key}(x)\\}\cup\mathit{keys}(\mathit{next}(x))\hskip
10.00002pt\text{(C3)}$
$\displaystyle\qquad\qquad\qquad\qquad\quad\;\land\mathit{hslist}(x)=\\{x\\}\cup\mathit{hslist}(\mathit{next}(x))\hskip
21.79996pt\text{(C4)}$ $\displaystyle\qquad\qquad\qquad\qquad\quad\;\land
x\not\in\mathit{hslist}(\mathit{next}(x))$
$\displaystyle\land~{}\mathit{last}(x)=\mathit{last}(\mathit{next}(x))$
$\displaystyle\land~{}\mathit{last}(\mathit{last}(x))=\mathit{last}(x)$
$\displaystyle\land~{}x\in\mathit{hslist}(\mathit{last}(x))$
$\displaystyle\land~{}\mathit{prev}(x)\in\mathit{hslist}(\mathit{last}(x))$
$\displaystyle\land~{}\mathit{next}(x)\in\mathit{hslist}(\mathit{last}(x))$
Figure 10. Full local condition for lists for Circular List Insert Back

The local condition $\mathit{LC}$ for circular lists can be seen in Figure 10.
For use in loop invariants, we have defined two variants of the local
condition. One of these variants is $LC_{MinusNode}(x,n)$, which can be seen
as a predicate on nodes $x$ and $n$, and is formed from $\mathit{LC}$ by
replacing the clauses (C1), (C3), and (C4) in Figure 10 with the three clauses
(C1’), (C3’), and (C4’) in Figure 11. Additionally, we have another variant:
$LC_{Last}(x,n)$, which is formed from $LC$ by replacing the clause (C2) in
Figure 10 with
$\mathit{hslist}(x)=\\{x,n\\}\cup\mathit{hslist}(\mathit{next}(x))$.

$\displaystyle(\mathit{keys}(x)=\mathit{keys}(\mathit{next}(x))\setminus\\{\mathit{key}(n)\\}\lor\mathit{keys}(x)=\mathit{keys}(\mathit{next}(x)))\hskip
20.00003pt\text{(C1')}$
$\displaystyle(\mathit{keys}(x)=(\mathit{key}(x)\cup\mathit{keys}(\mathit{next}(x)))\setminus\\{\mathit{key}(n)\\}\hskip
87.50012pt\text{(C3')}$
$\displaystyle\quad~{}\lor\mathit{keys}(x)=(\mathit{key}(x)\cup\mathit{keys}(\mathit{next}(x))))$
$\displaystyle(\mathit{hslist}(x)=(x\cup\mathit{hslist}(\mathit{next}(x)))\setminus\\{n\\})\hskip
121.00024pt\text{(C4')}$ Figure 11. Alterations to Figure 10 to form
$LC_{MinusNode}$

Note that in this example as well as other benchmarks where we introduce
scaffolding nodes, in order to prove a bound on the impact set, we require
that a precondition $\phi$ holds before we mutate particular fields of nodes.
The fields, preconditions, and impact sets for every node can be seen in Table
4. Note that our benchmark contains another manipulation macro,
AddToLastHsList(x, n, Br), which, if x is a scaffolding node (or
$\mathit{last}(x)=x$), adds the node n to the set $\mathit{hslist}(x)$. The
precondition for invoking this macro is that $\mathit{last}(x)=x$, and the
only object impacted by the macro is $\\{x\\}$.

Mutated Field $f$ | Mutation Precond. $\phi$ | Impacted Objects $A_{f}$
---|---|---
$\mathit{next}$ | $\top$ | $\\{x,\mathit{old}(\mathit{next}(x))\\}$
$\mathit{key}$ | $\top$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{prev}$ | $\top$ | $\\{x,\mathit{old}(\mathit{prev}(x))\\}$
$\mathit{last}$ | $\mathit{last}(x)\neq x\lor(\mathit{last}(x)=x\land\mathit{hslist}(x)=\\{x\\})$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{length}$ | $\top$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{rev\\_length}$ | $\top$ | $\\{x,\mathit{next}(x)\\}$
$\mathit{keys}$ | $\top$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{hslist}$ | $\mathit{last}(x)\neq x\lor(\mathit{last}(x)=x\land\mathit{hslist}(x)=\\{x\\})$ | $\\{x,\mathit{prev}(x)\\}$
Table 4. Full impact sets for lists for Circular List Insert Back

We give the specification and program for Circular List Insert Back below.

     pre: $\mathit{Br}=\emptyset\land\mathit{next}(x)=\mathit{last}(x)$
     post: $\mathit{Br}=\emptyset\land\mathit{next}(ret)=\mathit{last}(ret)\land\mathit{last}(ret)=\mathit{old}(\mathit{last}(x))$
           $\land\mathit{keys}(\mathit{last}(ret))=\mathit{old}(\mathit{keys}(\mathit{last}(x)))\cup\{k\}\land fresh(\mathit{hslist}(\mathit{last}(ret))\setminus\mathit{old}(\mathit{hslist}(\mathit{last}(x))))$
     circular_list_insert_back(x: C, k: Int Br: Set(C))
     returns ret: C, Br: Set(C)
     {
       LCOutsideBr(x, Br);
       LCOutsideBr(x.next, Br);
       LCOutsideBr(x.prev, Br);

       var last: C = x.next;
       var node: C;
       NewObj(node, Br);
       Mut(node, key, k, Br);
       Mut(node, next, x.next, Br);
       Mut(x, next, node, Br);

       AddToLastHsList(last, node, Br);
       Mut(last, prev, node, Br);
       Mut(node, prev, x, Br);
       Mut(node, length, 1, Br);
       Mut(node, rev_length, 1 + node.prev.rev_length, Br);
       Mut(node, keys, {k}, Br);
       Mut(node, hslist, {node}, Br);
       Mut(node, last, node.prev.last, Br);
       AssertLCAndRemove(node, Br);

       ghost var cur: C = x;
       label PreLoop:
       while (cur $\neq$ last)
          invariant $cur\neq{last}\Rightarrow$
                  $Br=\{cur,last\}$
                  $\land LC_{MinusNode}(cur,node)$
                  $\land\mathit{last}(cur)=last$
                  $\land LC_{Last}(last,node)$
          invariant $cur=last\Rightarrow LC_{MinusNode}(cur,node)$
          invariant $node\in\mathit{hslist}(\mathit{next}(cur))$
          invariant $k\in\mathit{keys}(\mathit{next}(cur))$
          invariant Unchanged@PreLoop$(node)$
          invariant Unchanged@PreLoop$(last)$
          invariant $Br\subseteq\{cur,last\}$
          decreases $\mathit{rev\_length}(cur)$
       {
          if (cur.prev $\neq$ last) {
            LCOutsideBr(cur.prev, Br);
          }
          Mut(cur, length, cur.next.length + 1, Br);
          Mut(cur, hslist, cur.next.hslist + {node});
          Mut(cur, keys, cur.next.keys + {node.k});
          AssertLCAndRemove(cur, Br);
          cur := cur.prev;
       }

       LCOutsideBr(node, Br);
       Mut(cur, keys, cur.next.keys, Br);
       AssertLCAndRemove(cur, Br);
       AssertLCAndRemove(node, Br);

       ret := node;
     }

###  D.5. Merging Sorted Lists

We demonstrate the ability of intrinsic definitions to handle multiple data
structures at once, using the example of in-place merging of two sorted lists.
The method merges the two lists by reusing the two lists’ elements, which is a
natural pattern for imperative code. Once again, we extend the definition of
sorted lists from Case Study 4.1. We add the predicates $list1:C\rightarrow
Bool$, $list2:C\rightarrow Bool$, and $list3:C\rightarrow Bool$, to indicate
disjoint classes of lists. The relevant local condition and impact sets are:

$\displaystyle(list1(x)\lor list2(x)\lor list3(x))$ $\displaystyle\land{}$
$\displaystyle\neg(list1(x)\land list2(x))\land\neg(list2(x)\land list3(x))$
$\displaystyle\land{}$ $\displaystyle\neg(list1(x)\land list3(x))$
$\displaystyle\land{}$
$\displaystyle(list1(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list1(\mathit{next}(x))))$ $\displaystyle\land{}$
$\displaystyle(list2(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list2(\mathit{next}(x))))$ $\displaystyle\land{}$
$\displaystyle(list3(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list3(\mathit{next}(x))))$

Mutated Field $f$ |  Impacted Objects $A_{f}$
---|---
$list1$ | $\\{x,\mathit{prev}(x)\\}$
$list2$ | $\\{x,\mathit{prev}(x)\\}$
$list3$ | $\\{x,\mathit{prev}(x)\\}$

Disjointness of the three lists is ensured by insisting that every object has
at most one of the three list predicates hold.

We give a gist of the proof of the merge method. The recursive program
compares the keys at the heads of the first and second sorted lists, and adds
the appropriate node to the front of the third list. It turns out that we can
easily update the ghost maps for this node (making it belong to the third
list, and updating its parent pointer and key set) as well as updating the
parent pointer of the head of the list where the node is removed from. When
one of the lists is empty, we append the third list to the non-empty list
using a single pointer mutation and then, using a ghost loop, we update the
nodes in the appended list to make $list3$ true (this needs a loop invariant
involving the broken set).

We provide below the full local conditions and impact sets.

(3) $\displaystyle\mathit{LC}\equiv\forall x$ $\displaystyle.(list1(x)\lor
list2(x)\lor list3(x))$ $\displaystyle\land~{}\neg(list1(x)\land
list2(x))\land\neg(list2(x)\land list3(x))$
$\displaystyle\land~{}\neg(list1(x)\land list3(x))$
$\displaystyle\land~{}(\mathit{prev}(x)\neq\mathit{nil}\Rightarrow\mathit{next}(\mathit{prev}(x))=x)$
$\displaystyle\land~{}(\mathit{next}(x)\neq\mathit{nil}\Rightarrow\mathit{prev}(\mathit{next}(x))=x$
$\displaystyle\qquad\qquad\qquad\quad\land~{}\mathit{length}(x)=\mathit{length}(\mathit{next}(x))+1$
$\displaystyle\qquad\qquad\qquad\quad\land~{}\mathit{keys}(x)=\mathit{keys}(\mathit{next}(x))\cup\\{\mathit{key}(x)\\}$
$\displaystyle\qquad\qquad\qquad\quad\land~{}\mathit{hslist}(x)=\mathit{hslist}(\mathit{next}(x))\uplus\\{x\\}\text{\quad(disjoint
union)}$
$\displaystyle\qquad\qquad\qquad\quad\land~{}\mathit{key}(x)\leq\mathit{key}(\mathit{next}(x)))$
$\displaystyle\land~{}(\mathit{next}(x)=\mathit{nil}\Rightarrow\mathit{length}(x)=1\land\mathit{keys}(x)=\\{\mathit{key}(x)\\}\land\mathit{hslist}(x)=\\{x\\})$
$\displaystyle\land~{}(list1(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list1(\mathit{next}(x))))$
$\displaystyle\land~{}(list2(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list2(\mathit{next}(x))))$
$\displaystyle\land~{}(list3(x)\Rightarrow(\mathit{next}(x)\neq\mathit{nil}\Rightarrow
list3(\mathit{next}(x))))$ Figure 13. Full local condition for lists for
Sorted List Reverse

Note that we also have a variation of the local condition $LC_{NC}$, used in
ghost loop invariants, which is similar to Equation 3, except the final three
conjuncts (those enforcing closure on $list1,list2,list3$) are removed. This
is done when converting an entire list from one class to another (i.e.,
converting from $list1$ to $list3$). The following are the full impact sets
for all fields of this data structure.

Mutated Field $f$ | Impacted Objects $A_{f}$
---|---
$\mathit{next}$ | $\\{x,\mathit{old}(\mathit{next}(x))\\}$
$\mathit{key}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{prev}$ | $\\{x,\mathit{old}(\mathit{prev}(x))\\}$
$\mathit{length}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{keys}$ | $\\{x,\mathit{prev}(x)\\}$
$\mathit{hslist}$ | $\\{x,\mathit{prev}(x)\\}$
$list1$ | $\\{x,\mathit{prev}(x)\\}$
$list2$ | $\\{x,\mathit{prev}(x)\\}$
$list3$ | $\\{x,\mathit{prev}(x)\\}$
Figure 14. Full impact sets for disjoint sorted lists


effective density of zeros has to be positive. We, however, observed this to
be the case in the example above.

##  Appendix G Stringy Cerulus-Martin bound

The Cerulus-Martin bound on the high-energy scattering at fixed angles
Cerulus:1964cjb ; Tourkine:2023xtu ; Buoninfante:2023dyd  effectively
expresses Mandelstam analyticity in the following form

$\displaystyle{\rm Regge}\leq({\rm Fixed\ real\ angle})\times({\rm Fixed\
complex\ angle}).$ (169)

It is usually presented as a lower bound on scattering as follows

$\displaystyle({\rm Fixed\ real\ angle})\geq{{\rm Regge}\over({\rm Fixed\
complex\ angle})}\ .$ (170)

In nonperturbative QFT, for example in QCD, we do not have a bound on
scattering at complex angles, therefore it is not a rigorous lower bound in
this case.

We would like next derive a lower bound on the scattering at physical fixed
scattering angle for stringy amplitudes. Our input will be the following: an
upper bound on the amplitude discussed in the section above, and the
polynomial nature of the Regge limit.

We consider fixed-angle scattering so that

$\displaystyle t=-{s\over 2}(1-z),$ (171)

and we would like to derive a lower bound of the following type

$\displaystyle\max_{|z|\leq z_{0}}|T(s,z)|\geq T_{0}(s,z).$ (172)

We first start with the following simple observation

$\displaystyle\max_{|z|\leq z_{0}}|T(s,z)|\geq\max_{|z|\leq z_{0}}|{\rm
Im}T(s,z)|=\max_{|z|\leq z_{0}}|T_{s}(s,z)|.$ (173)

Next, we notice that the discontinuity of the amplitude is simply a polynomial
(as described above in (135))

$\displaystyle
T_{s}(s,z)\sim\sum_{J=0}^{j(s)}c_{i,J}P_{J}(z),~{}~{}~{}c_{i,J}\geq 0\ ,$
(174)

and thus, it is an analytic function in the $z$-plane. To derive a lower
bound, we consider the following mapping

$\displaystyle w(z)={z+\sqrt{z^{2}-z_{0}^{2}}\over z_{0}}.$ (175)

Under this mapping, the real-line segment $-z_{0}\leq z\leq z_{0}$ is mapped
into a unit circle in the $w$-plane.

We now consider three circles in the $w$-plane: $|w|=1$, $|w|=r_{2}$ and
$|w|=r_{3}$, such that $r_{3}>r_{2}>1$. The discontinuity of the amplitude is
an analytic function in the annulus $1\leq|w|\leq r_{3}$. We also introduce
the following notation

$\displaystyle M_{r}=\max_{|w|=r}|T_{s}(s,z)|.$ (176)

We then have the three-circle theorem that states the following. For a
function analytic inside the annulus and bounded on its boundary, we have

$\displaystyle M_{r_{2}}\leq M_{1}^{1-{\log r_{2}\over\log
r_{3}}}M_{r_{3}}^{{\log r_{2}\over\log r_{3}}}\ .$ (177)

We choose $r_{2}$ at fixed $t$ such that the circle includes the Regge limit
of the amplitude, which is $\sim 1$, where the equivalence relation means
‘modulo powers’. We then have

$\displaystyle 1\leq M_{1}^{1-{\log w(1)\over\log r_{3}}}M_{r_{3}}^{{\log
w(1)\over\log r_{3}}},$ (178)

where we set $r_{2}=w(1)$ which is its leading large $s$ behavior.

We next rewrite this bound as follows

$\displaystyle M_{1}\geq(M_{r_{3}})^{-{\log w(1)\over\log r_{3}}/(1-{\log
w(1)\over\log r_{3}})},$ (179)

where the LHS is related to fixed-angle scattering for physical angles,
whereas the RHS is related to scattering at complex angles.

We next notice the following simple fact

$\displaystyle\Big{|}\sum_{J}^{j(s)}c_{i,J}P_{J}(z)\Big{|}\leq\sum_{J}^{j(s)}c_{i,J}\Big{|}P_{J}(z)\Big{|}\leq\sum_{J}^{j(s)}c_{i,J}P_{J}(\sqrt{|z|^{2}+1}),~{}~{}~{}|z|\geq
1,$ (180)

where we used that $c_{i,J}\geq 0$. We then get

$\displaystyle M_{r_{3}}\leq T_{s}(s,\sqrt{z_{*}^{2}+1}),$ (181)

where

$\displaystyle z_{*}\equiv\max_{|w|=r_{3}}|z(w)|=z_{0}{1+r_{3}^{2}\over
2r_{3}}.$ (182)

Next, we use the bound discussed in the previous section (155) to get

$\displaystyle T_{s}(s,z)$ $\displaystyle\lesssim
e^{\alpha_{\text{asy}^{\prime}}sf_{\text{Ven}}(z)},{}$ $\displaystyle
f_{\text{Ven}}(z)$ $\displaystyle\equiv{z+1\over 2}\log{z+1\over 2}-{z-1\over
2}\log{z-1\over 2},$ (183)

where we are working modulo power-like corrections.

Combining all the inequalities above, we get that for any $r_{3}$

$\displaystyle\max_{|z|\leq
z_{0}}|T(s,z)|\geq(e^{\alpha_{\text{asy}^{\prime}}sf_{\text{Ven}}(\sqrt{z_{*}^{2}+1})})^{-{\log
w(1)\over\log r_{3}}/(1-{\log w(1)\over\log r_{3}})}.$ (184)

To optimize the bound, we would like to maximize the RHS. We find that the
maximum is attained at $r_{3}=\infty$ which finally gives

$\displaystyle\max_{|z|\leq z_{0}}|T(s,z)|\gtrsim
e^{-\alpha_{\text{asy}^{\prime}}s\log{1+\sqrt{1-z_{0}^{2}}\over z_{0}}}\ .$
(185)

This constitutes a stringy generalization of the Cerulus-Martin lower bound on
scattering at fixed angles. In the main text, we discussed the relationship
between the asymptotic Regge trajectory
$j_{\text{asy}}\simeq\alpha_{\text{asy}}t$, and the leading Regge trajectory
$j(t)\simeq\alpha^{\prime}t$, and argued that
$\alpha^{\prime}_{\text{asy}}\leq\alpha^{\prime}$. We can, therefore, write
the bound in terms of the leading Regge trajectory

$\displaystyle\max_{|z|\leq z_{0}}|T(s,z)|\gtrsim
e^{-\alpha^{\prime}s\log{1+\sqrt{1-z_{0}^{2}}\over z_{0}}}\ ,$ (186)

which is the bound we quoted in the main text.

Let us comment on the following technical subtlety in the argument above.
Strictly speaking, the imaginary part we considered above in (174) is
$\propto\delta(s-m^{2})$, and therefore our bound above directly applies to
the residues of the amplitude only. The standard way to cure this problem (as
well as to use the bound (186)) is to take the high-energy limit away from the
real axis $s\to s(1+i\epsilon)$. We expect that in this limit, the imaginary
part of the amplitude is still effectively given by (174), see Caron-
Huot:2016icg  for the discussion of this point, and therefore our arguments
apply.

## References

  * (1) R. J. Eden, _Theorems on high energy collisions of elementary particles_ , _Rev. Mod. Phys._ 43 (1971) 15–35.
  * (2) A. M. Jaffe, _High-energy behavior in quantum field theory. I. Strictly localizable fields_ , _Phys. Rev._ 158 (1967) 1454–1461.
  * (3) J. Polchinski and M. J. Strassler, _Hard scattering and gauge / string duality_ , _Phys. Rev. Lett._ 88 (2002) 031601, [hep-th/0109174].
  * (4) D. J. Gross and P. F. Mende, _The High-Energy Behavior of String Scattering Amplitudes_ , _Phys. Lett. B_ 197 (1987) 129–134.
  * (5) D. J. Gross and J. L. Manes, _The High-energy Behavior of Open String Scattering_ , _Nucl. Phys. B_ 326 (1989) 73–107.
  * (6) S. Caron-Huot, Z. Komargodski, A. Sever and A. Zhiboedov, _Strings from Massive Higher Spins: The Asymptotic Uniqueness of the Veneziano Amplitude_ , _JHEP_ 10 (2017) 026, [1607.04253].
  * (7) D. Amati, M. Ciafaloni and G. Veneziano, _Classical and Quantum Gravity Effects from Planckian Energy Superstring Collisions_ , _Int. J. Mod. Phys. A_ 3 (1988) 1615–1661.
  * (8) N. Arkani-Hamed, S. Dubovsky, A. Nicolis, E. Trincherini and G. Villadoro, _A Measure of de Sitter entropy and eternal inflation_ , _JHEP_ 05 (2007) 055, [0704.1814].
  * (9) S. B. Giddings and R. A. Porto, _The Gravitational S-matrix_ , _Phys. Rev. D_ 81 (2010) 025002, [0908.0004].
  * (10) I. Bah, Y. Chen and J. Maldacena, _Estimating global charge violating amplitudes from wormholes_ , _JHEP_ 04 (2023) 061, [2212.08668].
  * (11) H. Chen, A. L. Fitzpatrick and D. Karateev, _Nonperturbative bounds on scattering of massive scalar particles in d $\geq$ 2_, _JHEP_ 12 (2022) 092, [2207.12448].
  * (12) J. Elias Miro, A. Guerrieri and M. A. Gumus, _Bridging positivity and S-matrix bootstrap bounds_ , _JHEP_ 05 (2023) 001, [2210.01502].
  * (13) C. Cheung and G. N. Remmen, _Stringy Dynamics from an Amplitudes Bootstrap_ , 2302.12263.
  * (14) G. Veneziano, _Construction of a crossing - symmetric, Regge behaved amplitude for linearly rising trajectories_ , _Nuovo Cim. A_ 57 (1968) 190–197.
  * (15) D. D. Coon, _Uniqueness of the veneziano representation_ , _Phys. Lett. B_ 29 (1969) 669–672.
  * (16) M. Baker and D. D. Coon, _Dual resonance theory with nonlinear trajectories_ , _Phys. Rev. D_ 2 (1970) 2349–2358.
  * (17) D. D. Coon, U. P. Sukhatme and J. Tran Thanh Van, _Duality and proton-proton scattering at all angles_ , _Phys. Lett. B_ 45 (1973) 287–291.
  * (18) A. Adams, N. Arkani-Hamed, S. Dubovsky, A. Nicolis and R. Rattazzi, _Causality, analyticity and an IR obstruction to UV completion_ , _JHEP_ 10 (2006) 014, [hep-th/0602178].
  * (19) B. Lucini and M. Teper, _SU(N) gauge theories in four-dimensions: Exploring the approach to N = infinity_ , _JHEP_ 06 (2001) 050, [hep-lat/0103027].
  * (20) G. Veneziano, S. Yankielowicz and E. Onofri, _A model for pion-pion scattering in large-N QCD_ , _JHEP_ 04 (2017) 151, [1701.06315].
  * (21) C. Cheung and G. N. Remmen, _Bespoke dual resonance_ , _Phys. Rev. D_ 108 (2023) 086009, [2308.03833].
  * (22) N. Arkani-Hamed, T.-C. Huang and Y.-t. Huang, _The EFT-Hedron_ , _JHEP_ 05 (2021) 259, [2012.15849].
  * (23) Z. Bern, D. Kosmopoulos and A. Zhiboedov, _Gravitational effective field theory islands, low-spin dominance, and the four-graviton amplitude_ , _J. Phys. A_ 54 (2021) 344002, [2103.12728].
  * (24) S. Caron-Huot, Y.-Z. Li, J. Parra-Martinez and D. Simmons-Duffin, _Causality constraints on corrections to Einstein gravity_ , _JHEP_ 05 (2023) 122, [2201.06602].
  * (25) L.-Y. Chiang, Y.-t. Huang, W. Li, L. Rodina and H.-C. Weng, _(Non)-projective bounds on gravitational EFT_ , 2201.07177.
  * (26) J. Albert and L. Rastelli, _Bootstrapping Pions at Large $N$. Part II: Background Gauge Fields and the Chiral Anomaly_, 2307.01246.
  * (27) J. Albert and L. Rastelli, _Bootstrapping pions at large N_ , _JHEP_ 08 (2022) 151, [2203.11950].
  * (28) C. Fernandez, A. Pomarol, F. Riva and F. Sciotti, _Cornering large-N c QCD with positivity bounds_, _JHEP_ 06 (2023) 094, [2211.12488].
  * (29) Y.-Z. Li, _Effective field theory bootstrap, large-N $\chi$PT and holographic QCD_, 2310.09698.
  * (30) Y.-t. Huang, J.-Y. Liu, L. Rodina and Y. Wang, _Carving out the Space of Open-String S-matrix_ , _JHEP_ 04 (2021) 195, [2008.02293].
  * (31) L.-Y. Chiang, Y.-t. Huang and H.-C. Weng, _Bootstrapping string theory EFT_ , 2310.10710.
  * (32) J. Berman, H. Elvang and A. Herderschee, _Flattening of the EFT-Hedron: Supersymmetric Positivity Bounds and the Search for String Theory_ , 2310.10729.
  * (33) F. Figueroa and P. Tourkine, _Unitarity and Low Energy Expansion of the Coon Amplitude_ , _Phys. Rev. Lett._ 129 (2022) 121602, [2201.12331].
  * (34) N. Geiser and L. W. Lindwasser, _Properties of infinite product amplitudes: Veneziano, Virasoro, and Coon_ , _JHEP_ 12 (2022) 112, [2207.08855].
  * (35) J. Chakravarty, P. Maity and A. Mishra, _On the positivity of Coon amplitude in D = 4_ , _JHEP_ 10 (2022) 043, [2208.02735].
  * (36) R. Bhardwaj, S. De, M. Spradlin and A. Volovich, _On unitarity of the Coon amplitude_ , _JHEP_ 08 (2023) 082, [2212.00764].
  * (37) C. B. Jepsen, _Cutting the Coon amplitude_ , _JHEP_ 06 (2023) 114, [2303.02149].
  * (38) N. Geiser and L. W. Lindwasser, _Generalized Veneziano and Virasoro amplitudes_ , _JHEP_ 04 (2023) 031, [2210.14920].
  * (39) C. Cheung and G. N. Remmen, _Veneziano variations: how unique are string amplitudes?_ , _JHEP_ 01 (2023) 122, [2210.12163].
  * (40) N. Geiser, _The Baker-Coon-Romans $N$-point amplitude and an exact field theory limit of the Coon amplitude_, 2311.04130.
  * (41) B. McPeak, M. Venuti and A. Vichi, _Adding subtractions: comparing the impact of different Regge behaviors_ , 2310.06888.
  * (42) S. Mizera, _Crossing symmetry in the planar limit_ , _Phys. Rev. D_ 104 (2021) 045003, [2104.12776].
  * (43) A. Hebbar, D. Karateev and J. Penedones, _Spinning S-matrix bootstrap in 4d_ , _JHEP_ 01 (2022) 060, [2011.11708].
  * (44) K. Igi, _pi-N Scattering Length and Singularities in the Complex J Plane_ , _Phys. Rev. Lett._ 9 (1962) 76–79.
  * (45) A. A. Logunov, L. D. Soloviev and A. N. Tavkhelidze, _Dispersion sum rules and high-energy scattering_ , _Phys. Lett. B_ 24 (1967) 181–182.
  * (46) K. Igi and S. Matsuda, _New Sum Rules and Singularities in the Complex J Plane_ , _Phys. Rev. Lett._ 18 (1967) 625–627.
  * (47) R. Gatto, _New Sum Rules for Superconvergence_ , _Phys. Rev. Lett._ 18 (1967) 803–806.
  * (48) R. Dolen, D. Horn and C. Schmid, _Prediction of Regge Parameters of rho Poles from Low-Energy pi N Data_ , _Phys. Rev. Lett._ 19 (1967) 402–407.
  * (49) R. Dolen, D. Horn and C. Schmid, _Finite energy sum rules and their application to pi N charge exchange_ , _Phys. Rev._ 166 (1968) 1768–1781.
  * (50) M. Ademollo, H. R. Rubinstein, G. Veneziano and M. A. Virasoro, _Bootstraplike Conditions from Superconvergence_ , _Phys. Rev. Lett._ 19 (1967) 1402–1405.
  * (51) M. Ademollo, H. R. Rubinstein, G. Veneziano and M. A. Virasoro, _Bootstrap of meson trajectories from superconvergence_ , _Phys. Rev._ 176 (1968) 1904–1925.
  * (52) B. Mukhametzhanov and A. Zhiboedov, _Analytic Euclidean Bootstrap_ , _JHEP_ 10 (2019) 270, [1808.03212].
  * (53) A. Strominger, _Lectures on the Infrared Structure of Gravity and Gauge Theory_.  3, 2017.
  * (54) S. Caron-Huot, D. Mazac, L. Rastelli and D. Simmons-Duffin, _AdS bulk locality from sharp CFT bounds_ , _JHEP_ 11 (2021) 164, [2106.10274].
  * (55) C.-H. Chang, Y. Landau and D. Simmons-Duffin, _Spinning dispersive CFT sum rules and bulk scattering_ , 2311.04271.
  * (56) G. Altarelli and H. R. Rubinstein, _Closed forms for the scattering amplitudes and bootstrap based on sum rules_ , _Phys. Rev._ 178 (1969) 2165–2166.
  * (57) M. A. Virasoro, _Alternative constructions of crossing-symmetric amplitudes with regge behavior_ , _Phys. Rev._ 177 (1969) 2309–2311.
  * (58) J. A. Shapiro, _Electrostatic analog for the virasoro model_ , _Phys. Lett. B_ 33 (1970) 361–362.
  * (59) J. Polchinski, _String theory. Vol. 1: An introduction to the bosonic string_.  Cambridge Monographs on Mathematical Physics. Cambridge University Press, 12, 2007, 10.1017/CBO9780511816079.
  * (60) A. D. Martin and T. D. Spearman, _Elementary Particle Theory_.  North-Holland Publishing Co., Amsterdam, 1970.
  * (61) H. Kawai, D. C. Lewellen and S. H. H. Tye, _A Relation Between Tree Amplitudes of Closed and Open Strings_ , _Nucl. Phys. B_ 269 (1986) 1–23.
  * (62) D. Simmons-Duffin, _A Semidefinite Program Solver for the Conformal Bootstrap_ , _JHEP_ 06 (2015) 174, [1502.02033].
  * (63) W. Landry and D. Simmons-Duffin, _Scaling the semidefinite program solver SDPB_ , 1909.09745.
  * (64) Gurobi Optimization, LLC, _Gurobi Optimizer Reference Manual_ , 2023.
  * (65) X. O. Camanho, J. D. Edelstein, J. Maldacena and A. Zhiboedov, _Causality Constraints on Corrections to the Graviton Three-Point Coupling_ , _JHEP_ 02 (2016) 020, [1407.5597].
  * (66) N. Khuri, _Derivation of a veneziano series from the regge representation_ , _Physical Review_ 185 (1969) 1876.
  * (67) S. Matsuda, _MODEL FOR INFINITE VENEZIANO SERIES_ , .
  * (68) S. Mandelstam, _Veneziano formula with trajectories spaced by two units_ , _Phys. Rev. Lett._ 21 (1968) 1724–1728.
  * (69) P. Goddard and C. B. Thorn, _Compatibility of the Dual Pomeron with Unitarity and the Absence of Ghosts in the Dual Resonance Model_ , _Phys. Lett. B_ 40 (1972) 235–238.
  * (70) N. Arkani-Hamed, L. Eberhardt, Y.-t. Huang and S. Mizera, _On unitarity of tree-level string amplitudes_ , _JHEP_ 02 (2022) 197, [2201.11575].
  * (71) A. Sever and A. Zhiboedov, _On Fine Structure of Strings: The Universal Correction to the Veneziano Amplitude_ , _JHEP_ 06 (2018) 054, [1707.05270].
  * (72) M. S. Costa, T. Hansen and J. a. Penedones, _Bounds for OPE coefficients on the Regge trajectory_ , _JHEP_ 10 (2017) 197, [1707.07689].
  * (73) M. F. Paulos, J. Penedones, J. Toledo, B. C. van Rees and P. Vieira, _The S-matrix bootstrap. Part III: higher dimensional amplitudes_ , _JHEP_ 12 (2019) 040, [1708.06765].
  * (74) F. A. Cerulus and A. Martin, _A lower bound for large-angle elastic scattering at high energies_ , _Phys. Lett._ 8 (1964) 80–82.
  * (75) S. Caron-Huot, Y.-Z. Li, J. Parra-Martinez and D. Simmons-Duffin, _Graviton partial waves and causality in higher dimensions_ , _Phys. Rev. D_ 108 (2023) 026007, [2205.01495].
  * (76) B. Bachu and A. Hillman, _Stringy Completions of the Standard Model from the Bottom Up_ , 2212.03871.
  * (77) N. Arkani-Hamed, M. Pate, A.-M. Raclariu and A. Strominger, _Celestial amplitudes from UV to IR_ , _JHEP_ 08 (2021) 062, [2012.04208].
  * (78) S. Fubini and G. Veneziano, _Level structure of dual-resonance models_ , _Nuovo Cim. A_ 64 (1969) 811–840.
  * (79) D. J. Gross, _Factorization and the generalized veneziano model with satellites_ , _Nucl. Phys. B_ 13 (1969) 467–476.
  * (80) M. Bianchi, D. Consoli and P. Di Vecchia, _On the N-pion extension of the Lovelace-Shapiro model_ , _JHEP_ 03 (2021) 119, [2002.05419].
  * (81) S. Caron-Huot and V. Van Duong, _Extremal Effective Field Theories_ , _JHEP_ 05 (2021) 280, [2011.02957].
  * (82) K. Häring and A. Zhiboedov, _Gravitational Regge bounds_ , 2202.08280.
  * (83) M. Correia, A. Sever and A. Zhiboedov, _An analytical toolkit for the S-matrix bootstrap_ , _JHEP_ 03 (2021) 013, [2006.08221].
  * (84) V. N. Gribov, _The theory of complex angular momenta: Gribov lectures on theoretical physics_.  Cambridge Monographs on Mathematical Physics. Cambridge University Press, 6, 2007, 10.1017/CBO9780511534959.
  * (85) M. Andrews and J. Gunson, _Complex Angular Momenta and Many‐Particle States. I. Properties of Local Representations of the Rotation Group_ , _Journal of Mathematical Physics_ 5 (12, 2004) 1391–1400.
  * (86) K. Häring, A. Hebbar, D. Karateev, M. Meineri and J. a. Penedones, _Bounds on photon scattering_ , 2211.05795.
  * (87) D. Sivers and J. Yellin, _Review of recent work on narrow resonance models_ , _Rev. Mod. Phys._ 43 (1971) 125–188.
  * (88) R. C. Buck, _Interpolation series_ , _Transactions of the American Mathematical Society_ 64 (1948) 283–298.
  * (89) P. Tourkine and A. Zhiboedov, _Scattering amplitudes from dispersive iterations of unitarity_ , _JHEP_ 11 (2023) 005, [2303.08839].
  * (90) L. Buoninfante, J. Tokuda and M. Yamaguchi, _New lower bounds on scattering amplitudes: non-locality constraints_ , 2305.16422.


# HSTCosmicrays: A Python Package for Analyzing Cosmic Rays in HST Calibration
Data

N. D. Miles,1 S. Deustua,1 and G. Tancredi2

###### Abstract

HSTCosmicrays is a python-based pipeline designed to find and characterize
cosmic rays found in dark frames (exposures taken with the shutter closed).
Dark exposures are obtained routinely by all the Hubble Space Telescope (HST)
instruments for calibration. The main processing pipeline runs locally or in
the cloud on AWS . To date, we have characterized more than 1.2 billion cosmic
rays in $\sim$76,000 dark frames obtained with CCDs from the four active
instruments ACS/HRC, ACS/WFC, STIS, WFC3/UVIS, and the legacy instrument
WFPC2.

1Space Telescope Science Institute, Baltimore, Maryland, USA<EMAIL_ADDRESS><EMAIL_ADDRESS>
2Universidad de la República de Uruguay, Montevideo, Uruguay;
<EMAIL_ADDRESS>
##  1 Introduction

The Hubble Space Telescope (HST) has been operating outside the terrestrial
atmosphere in low earth orbit (LEO) since 1990. At these altitudes, every
image obtained by a solid state detector (e.g. CCD) is contaminated by high
energy particles (hereafter referred to as cosmic rays). These cosmic rays
(electrons, protons and atomic nuclei) originate from within our galaxy in
supernovae explosions and from within our solar system in coronal mass
ejections and solar wind. The flux observed by HST encodes information about
their interaction with the Earth’s magnetic field in LEO. By studying these
cosmic ray events, as well as the rates at which they occur, we can develop
more robust cosmic ray rejection routines and examine the interaction of the
Earth’s magnetic field with the interplanetary field over time.

We have written the python package, HSTCosmicrays, to identify and analyze
cosmic rays in dark frames (images taken with the shutter closed) taken as
part of routine calibration programs for instruments onboard HST. In Section
2, we provide a high level overview of the package. In Section 3, we detail
the processes by which we identify and label cosmic rays. In Section 4, we
detail the data extracted by the pipeline. Finally, in Section 5, we detail a
key result obtained using data extracted by the pipeline.

##  2 The Pipeline

The pipeline is broken into 5 distinct steps that are applied to consecutive
one month intervals and all the darks they contain; download, process,
analyze, save, and clean up. It is cloud enabled and can be run on AWS
utilizing the HST Public Dataset. For each month, we use astroquery (Ginsburg
et al. 2018) to programmatically query and download the bias-corrected dark
frames and their engineering and telemetry files from the Mikulski Archive for
Space Telescopes (MAST). After downloading, the images are processed and then
analyzed to extract statistics about each cosmic ray identified in the image.
Once the analysis has completed, the results are written to file and an email
is sent to a user defined email address with summary statistics of all the
cosmic rays found in each image. Finally, all downloaded images and any
temporary files created along the way are deleted to prepare for the next one
month chunk of darks.

##  3 Cosmic Ray Identification

For the active instruments (ACS, STIS, WFC3), we leverage each instrument’s
cosmic ray rejection routine to process each month of images. These routines
implement a noise-based rejection model that looks for statistically
significant outliers in CR-SPLIT observations taken with HST, i.e.
observations made at the same exact pointing in sequence. Each pixel
identified by the algorithm is marked with a special bit flag, 8192, in the
data quality (DQ) array of the multi-extension FITS file. A bitwise-and
comparison is performed to generate a binary image where pixels affected by
cosmic rays have a value of 8192 and everything else 0.

For the legacy instruments (WFPC2), a different method is used to avoid the
IRAF dependency of the calibration software. First, we perform three
iterations of sigma clipping to compute an accurate estimation of the image
statistics (mean, median, and standard deviation). Next, using the sigma-
clipped mean and standard deviation we create a binary image by identifying
all pixels that are more than three standard deviations above the mean.

In each case, after the binary image has been created we perform a connected-
component labeling analysis using the 8-connectivity matrix. The labeling
analysis identifies groups of pixels affected by the same cosmic ray. To
minimize contamination from hot pixels, we reject any objects identified that
affect 1 or 2 pixels. The end result is a segmentation map of the uniquely
identified cosmic rays (Figure 1).

Figure 1.: An example of the final label generated using a random dark frame
taken with WFPC2.

##  4 Cosmic Ray Analysis

Once the cosmic ray label has been generated, we apply the label to the SCI
extension to derive quantities of interest describing each identified cosmic
ray. First, we compute the total number of pixels affected (i.e. the size in
attached pixels) and record the coordinates of each pixel affected. Next, we
use the label to compute the moments of the energy distribution,

  1. 1.

$I_{0}=\sum_{i}p_{i}$

  2. 2.

$I_{x}=\frac{1}{I_{0}}\sum_{i}p_{i}*x_{i}$

  3. 3.

$I_{y}=\frac{1}{I_{0}}\sum_{i}p_{i}*y_{i}$

  4. 4.

$I_{xx}=\frac{1}{I_{0}}\sum_{i}p_{i}(x_{i}-I_{x})^{2}$

  5. 5.

$I_{yy}=\frac{1}{I_{0}}\sum_{i}p_{i}(y_{i}-I_{y})^{2}$

  6. 6.

$I_{xy}=\frac{1}{I_{0}}\sum_{i}p_{i}(x_{i}-I_{x})*(y_{i}-I_{y})$

where $p_{i}$ is the pixel value of the $i^{th}$ pixel in the cosmic ray label
and $x_{i}$, $y_{i}$ are the x and y coordinates of the $i^{th}$ pixel,
respectively. The first parameter is the total energy deposited in the
detector by the cosmic ray. The second and third parameters combine to give
the centroid as $(I_{x},I_{y})$. The fourth and fifth parameters are used to
compute a measure of width or "size" as,

$\sqrt{\frac{I_{xx}+I_{yy}}{2}}.$ (1)

The fourth, fifth, and sixth parameters are used to asses the shape or
symmetry of the energy distribution,

$\sqrt{\frac{(I_{xx}-I_{yy})^{2}+4I^{2}_{xy}}{(I_{xx}+I_{yy})^{2}}}.$ (2)

In Figure 2, we show simulated sources over a poisson background to visually
demonstrate the size and shape parameters. For each source, we use a 2D
Gaussian distribution,

$p(x,y)=A*e^{-\left({\frac{(x-x_{0})^{2}}{\sqrt{2\sigma_{x}}}+\frac{(y-y_{0})^{2}}{\sqrt{2\sigma_{y}}}}\right)},$
(3)

with $(x_{0},y_{0})=(25,25)$, $A=10^{4}$, and an added rotation of $\pi/4$.
The source on the left is the ideal, perfectly symmetric 2D Gaussian with
$\sigma_{x}=\sigma_{y}=1$. The middle source has been skewed such that
$\sigma_{y}=1.5*\sigma_{x}$. The source on the right has been skewed such that
$\sigma_{y}=4*\sigma_{x}$.

For each image, we compute the cosmic ray rate, defined as the total number of
cosmic rays divided by the total integration time (exposure time plus half of
the readout time) and the geometric size of the detector. Next, for each
cosmic ray identified, we record the coordinates of each pixel affected during
the observation. Finally, in addition to the morphological parameters, we
store the following metadata for each image: altitude, latitude, longitude,
observation date, observation start time, observation end time, the total
integration time, and the WCS information.

Figure 2.: Simulated sources with their corresponding size and shape
measurements denoted at the top of each subplot.

##  5 Results

We have utilized the HSTCosmicrays package to analyze $\sim 76,000$ images
taken with 5 different CCD imagers spanning from 1994 to present. From those
$\sim 76,000$, we have extracted morphological information on more than 1.2
billion cosmic rays. In Figure 3, we highlight one of the key results thus
far. In each column, we show the detector thickness maps on the top row and
the cosmic ray incidence maps on the bottom row. The thickness maps are
generated by modeling fringe patterns present in long wavelength flat field
observations (Malumuth et al. 2003; Walsh et al. 2003; Wong 2010). The cosmic
ray incidence maps are created by tabulating the number of times a given pixel
is impacted by a cosmic ray over its lifetime.

Figure 3.: A comparison of detector thicknesses and cosmic ray incidence maps.
As expected, thicker regions of the detectors are impacted more often. The ACS
and WFC3 thickness maps were provided by J.R. Walsh and M. Wong, respectively.

## References

  * Ginsburg et al. (2018) Ginsburg, A., Sipocz, B., Parikh, M., Woillez, J., Groener, A., Liedtke, S., Robitaille, T., Deil, C., jcsegovia, Norman, H., Svoboda, B., Brasseur, C. E., et al. 2018, astropy/astroquery: v0.3.9 release. URL https://doi.org/10.5281/zenodo.2002585
  * Malumuth et al. (2003) Malumuth, E. M., Hill, R. S., Gull, T., Woodgate, B. E., Bowers, C. W., Kimble, R. A., Lindler, D., Plait, P., & Blouke, M. 2003, PASP, 115, 218
  * Walsh et al. (2003) Walsh, J. R., Freudling, W., Pirzkal, N., & Pasquali, A. 2003, Modelling the fringing of the ACS WFC and HRC chips, Tech. rep.
  * Wong (2010) Wong, M. H. 2010, in Fringing in the WFC3/UVIS detector; Hubble after SM4. Preparing JWST, 22