# Antaeus: a retrograde group of tidal debris in the Milky Way’s disk plane

Pierre-Antoine Oria  Université de Strasbourg, CNRS, Observatoire astronomique
de Strasbourg, UMR 7550, F-67000 Strasbourg, France  Wassim Tenachi
Université de Strasbourg, CNRS, Observatoire astronomique de Strasbourg, UMR
7550, F-67000 Strasbourg, France  Rodrigo Ibata Université de Strasbourg,
CNRS, Observatoire astronomique de Strasbourg, UMR 7550, F-67000 Strasbourg,
France  Benoit Famaey Université de Strasbourg, CNRS, Observatoire
astronomique de Strasbourg, UMR 7550, F-67000 Strasbourg, France  Zhen Yuan
Université de Strasbourg, CNRS, Observatoire astronomique de Strasbourg, UMR
7550, F-67000 Strasbourg, France  Anke Arentsen  Université de Strasbourg,
CNRS, Observatoire astronomique de Strasbourg, UMR 7550, F-67000 Strasbourg,
France  Nicolas Martin  Université de Strasbourg, CNRS, Observatoire
astronomique de Strasbourg, UMR 7550, F-67000 Strasbourg, France  Akshara
Viswanathan  Kapteyn Astronomical Institute, University of Groningen,
Landleven 12, NL-9747AD Groningen, the Netherlands

###### Abstract

We present the discovery of a wide retrograde moving group in the disk plane
of the Milky Way using action-angle coordinates derived from the Gaia DR3
catalog. The structure is identified from a sample of its members that are
currently almost at the pericenter of their orbit and are passing through the
Solar neighborhood. The motions of the stars in this group are highly
correlated, indicating that the system is probably not phase mixed. With a
width of at least $1.5{\rm\,kpc}$ and with a probable intrinsic spread in
metallicity, this structure is most likely the wide remnant of a tidal stream
of a disrupted ancient dwarf galaxy (age $\sim 12{\rm\,Gyr}$,
$\langle{\rm[Fe/H]}\rangle\sim-1.74$). The structure presents many
similarities (e.g. in energy, angular momentum, metallicity, and eccentricity)
with the Sequoia merging event. However, it possesses extremely low vertical
action $J_{z}$ which makes it unique even amongst Sequoia dynamical groups. As
the low $J_{z}$ may be attributable to dynamical friction, we speculate that
the these stars may be the remnants of the dense core of the Sequoia
progenitor.

Galactic Archeology — galaxies: disk — galaxies: kinematics and dynamics —
Local Group

††journal: ApJ

##  1 Introduction

The complex formation and merging history of the Milky Way (MW) can perhaps be
best understood by examining its stellar halo, host to many tidal debris of
disrupted galaxies and globular clusters. Dynamical times in the halo are
long, so the debris can persist there as coherent phase space structures for
billions of years (see e.g. Helmi & de Zeeuw 2000), making them easier for us
to detect.

With the advent of the Gaia mission (Gaia Collaboration et al., 2016) and its
superb astrometric data, the task of digging into the stellar halo to uncover
the past has been made more accessible. The stellar halo of the MW is now
understood to be the product of several important accretion events making up
most of its population (Di Matteo et al., 2019), the biggest of which being
Gaia-Sausage/Enceladus (Belokurov et al., 2018; Helmi et al., 2018). Stream
finding algorithms (Malhan et al., 2018; Ibata et al., 2021) have now detected
dozens of kinematically coherent structures which will help chart the
acceleration field of our Galaxy, providing a wealth of model-agnostic
information.

The Gaia data also makes it possible to use action coordinates
$(J_{r},J_{\phi},J_{z})$ to detect stellar structures. Actions keep relevance
over very long times if the potential evolves slowly and are thus especially
useful to trace past mergers. Recently, Yuan et al. (2020), Naidu et al.
(2020) and Malhan et al. (2022) used these quantities to detect and construct
maps of the MW’s dynamical groups and link them to important merger events.

Figure 1: Selection procedure. Top panel: Gaia DR3 stars from the selection
process described in Section 2 (i.e. $\varpi/\delta\varpi>10$, $r_{apo}\geq
25{\rm\,kpc}$ and $d\leq 1.5{\rm\,kpc}$). Middle panel: zoom on the low
$J_{z}$ region delimited by the rectangle in the top panel ($2500\leq
J_{\phi}\leq 3500{\rm\,km\,s^{-1}}{\rm\,kpc}$, $J_{z}\leq
150{\rm\,km\,s^{-1}}{\rm\,kpc}$). Bottom panel: same region as the middle
panel, but for our final cut using distances $d\leq 1{\rm\,kpc}$ from the Sun.

A similar technique was employed by Myeong et al. (2018) to find several
retrograde structures in the stellar halo, which were then tentatively
associated to the $\omega$ Centauri globular cluster, which Majewski et al.
(2012) had already suspected of bringing in such material. Retrograde
structures have been linked to accretion events for a long time (Carollo et
al., 2007), and it has been confirmed by Helmi et al. (2017) that the less
bound stars in the halo are typically on retrograde orbits. Sestito et al.
(2021) also highlight the importance of the metal poor retrograde halo
population for tracing the early building blocks of the galaxy.

Myeong et al. (2019) reexamined the structures from Myeong et al. (2018) and
linked them to a substantial merger event they named Sequoia. The Sequoia
progenitor galaxy could have brought those retrograde groups and possibly
$\omega$ Centauri as well. The fact that its stellar population is distinct in
metallicity and orbital parameters from the Gaia-Sausage makes the event
another important piece of the stellar halo puzzle.

Figure 2: Top panel: position and velocity vectors of our selection of stars
from Section 2 colored by total velocity; we plot bulk motion outliers with a
slightly transparent line. The orange ball represents the Sun. Antaeus stars
are currently passing through our Solar neighbourhood, going in a retrograde
motion in the Milky Way’s disk plane. Bottom panel: velocity planes
$v_{r}v_{\phi}$, $v_{r}v_{z}$, $v_{\phi}v_{z}$ with the outliers (red dots)
from the top panel bulk motion separated from Antaeus’ stars (black). Note
that we inverted the $v\phi$ axes to be coherent with usual velocity plots.

In this work we present the discovery of Antaeus111In Greek mythology, Antaeus
is the child of Gaia and Poseidon, a giant whose name comes from “opponent”.,
a retrograde high energy group of tidal debris in the MW’s disk plane, made
using action-angle coordinates derived from the Gaia DR3 catalogue (Gaia
Collaboration, 2022) and the Stäckel fudge implemented in Agama (Vasiliev,
2019). The new structure has several properties which are similar to those of
Sequoia stars, so we discuss its possible affiliation to this event, although
both its position in the disk of the MW and its extraordinary low vertical
action make it stand out.

##  2 Selection process

Throughout this article, we use the right-hand side Galactic Cartesian
coordinates for the MW with the Sun located at
$(x,y,z)_{\odot}=(-8.2240,0,0.0028){\rm\,kpc}$ (taking the Solar radius from
Bovy 2020 and the height above the mid-plane from Widmark et al. 2021) having
peculiar velocity
$(v_{x},v_{y},v_{z})_{\odot}=(11.10,7.20,7.25){\rm\,km\,s^{-1}}$ (Schönrich et
al. 2010, but with the velocity in the direction of Galactic rotation taken
from Bovy 2020). Our starting point is the Radial Velocity Spectrometer (RVS)
sample of Gaia DR3, for which we derive action-angle coordinates
$(J_{r},J_{\phi},J_{z})$ and orbital parameters using Agama (Vasiliev, 2019)
in the MW gravitational potential of McMillan (2017). From this catalogue, we
take the stars with good parallax measurements ($\varpi/\delta\varpi\geq 10$)
and $d\leq 1.5{\rm\,kpc}$ so as to retain a good quality Solar neighborhood
sample. Since our aim is to investigate the structures that are falling down
onto the Milky Way, we choose to select stars with large apocenter distances,
$r_{\rm apo}\geq 25{\rm\,kpc}$. These cuts leave us with 3624 stars; we plot
the resulting selection in the $J_{\phi}J_{z}$ plane, coloured by $r_{\rm
apo}$, in Figure 1 (top panel).

Among the many interesting structures that stand out from this view, we focus
our attention on the low $J_{z}$, retrograde moving group of stars delimited
by the black rectangle ($2500\leq J_{\phi}\leq
3500{\rm\,km\,s^{-1}}{\rm\,kpc}$, $J_{z}\leq 150{\rm\,km\,s^{-1}}{\rm\,kpc}$),
into which we zoom in Figure 1 (middle panel). We notice a good agreement in
apocenters for stars in this region, further suggesting the presence of a
stellar structure with coherent motion.

Figure 3: Colour magnitude diagram for our sample of Antaeus stars, compared
to PARSEC model isochrones (Bressan et al., 2012) of age $12{\rm\,Gyr}$ and
metallicities ${\rm[Fe/H]=-1.75}$ (red) and ${\rm[Fe/H]=-1.50}$ (green). The
colorbar gives the [Fe/H] for the 8 LAMOST stars.

Finally, we experimented with the heliocentric distance cut to see how the
selection changes. We noticed that by selecting stars within a distance of
$d\leq 1{\rm\,kpc}$ from the Sun (Figure 1, bottom panel) the agreement in
apocenters is slightly better, removing in particular some extreme values from
the previous cut. This leaves a sample of 80 stars which are listed in Table
1.

Figure 4: Orbits of Antaeus stars seen in Galactic Cartesian coordinates,
integrated backwards in the McMillan (2017) MW potential for $1.5{\rm\,Gyr}$
(top panel), and in the MWPotential2014 model for $2.5{\rm\,Gyr}$ (bottom
panel). Notice the change of scales, as stars go farther when integrated in
the lighter MWPotential2014. Orbits of the LAMOST sample (8 stars) are in
solid black, and orbits of the rest of our sample (57 stars) are in purple.

##  3 Sample characteristics

We show the positions and velocities of our selection of stars in Figure 2
(top panel). It appears clear that the stars belong to a coherent structure
dynamically, moving in a retrograde motion in the disk plane of the MW. The
structure is rather thick, with a width of at least $1.5{\rm\,kpc}$. We
identify some outliers from this bulk motion, which all have a distinctive
positive velocity in the $x$ direction ($v_{x}\geq 0$). For the remainder of
this study, we will exclude those 15 outliers from our sample, leaving us with
65 stars of the Antaeus stream. In Figure 2 (top panel), we plot velocity
planes $v_{r}v_{\phi}$, $v_{r}v_{z}$, $v\phi,v_{z}$ with this separation taken
into account, showing the compactness of Antaeus stars in those projections.

We crossmatch our selection with the LAMOST DR8 catalogue (Wang et al., 2022)
and find 8 stars in common, for which we obtain metallicities from their
“FEH_PASTEL” values. These LAMOST stars have a mean
${\rm[Fe/H]}=-1.74^{+0.06}_{-0.07}$, with an intrinsic spread of
$\sigma=0.11^{+0.10}_{-0.04}$ (correcting for the LAMOST metallicity
uncertainty estimates) and individual values ranging from
${\rm[Fe/H]}=-1.33\pm 0.23$ to ${\rm[Fe/H]}=-2.09\pm 0.30$. The colour
magnitude diagram (CMD) of the sample is shown on Figure 3, compared to old
metal poor isochrones $(12{\rm\,Gyr},\ {\rm[Fe/H]=-1.75}\text{ and
}{\rm[Fe/H]=-1.50})$ from the PARSEC library (Bressan et al., 2012). The
photometry is corrected for interstellar extinction using the 3D extinction
estimates calculated by Anders et al. (2022).

Finally, we integrate back in time the orbits of the Antaeus stars in the
McMillan MW potential for $1.5{\rm\,Gyr}$, and in the MWPotential2014 (Bovy,
2015); we show the results in Figure 4. Here also the structure appears very
coherent dynamically. We find, for the McMillan MW potential $(M_{\rm
vir}=1.3\times 10^{12}{\rm\,M_{\odot}})$, a mean pericenter radius of $r_{\rm
peri}=7.3{\rm\,kpc}$, a mean apocenter radius of $r_{\rm apo}=39.3{\rm\,kpc}$,
a mean orbital eccentricity of $ecc=0.69$, and a mean orbital time of $t_{\rm
orbit}=1.1{\rm\,Gyr}$. For the lighter MWPotential2014 however $(M_{\rm
vir}=8\times 10^{11}{\rm\,M_{\odot}})$, those values become mean $r_{\rm
peri}=7.3{\rm\,kpc}$, mean $r_{\rm apo}=71.9{\rm\,kpc}$, mean $ecc=0.81$, and
mean $t_{\rm orbit}=1.5{\rm\,Gyr}$. The 8 LAMOST stars, whose orbits are
plotted in solid black, appear to be good representative members of the
stream.

The mean actions of stars in the structure are
$(J_{r}=1761,J_{\phi}=2990,J_{z}=39){\rm\,kpc}{\rm\,km\,s^{-1}}$, and their
mean energy is $E=-10^{5}$ km2 s-2 (in the McMillan 2017 potential model).

##  4 Discussion and Conclusions

Based on the characteristics derived in Section 3, in particular the thickness
of the structure (width $\simeq 1.5{\rm\,kpc}$) and the range of metallicity
of its constituent stars, it seems highly likely that this group of stars is
the remnant of a tidal stream of a disrupted dwarf galaxy. The CMD (Figure 3)
seems to indicate that the progenitor is likely to be very old, probably
around $\sim 12{\rm\,Gyr}$ in age. The agreement is better with a model
metallicity of $\rm{[Fe/H]}=-1.50$, although we derive a mean value of
${\rm[Fe/H]}=-1.74^{+0.06}_{-0.07}$. It would thus be very helpful to extend
our sample of metallicities to help decide the matter.

The mean $J_{\phi}$, energy, and eccentricities of our sample of Antaeus stars
show many similarities with the Arjuna/I’itoi/Sequoia group of mergers (Naidu
et al., 2020). However Antaeus seems more akin to the retrograde structures of
Myeong et al. (2018) and to the retrograde tail of the Sequoia event (Myeong
et al., 2019), especially when factoring in the metallicity of its population.
The $\sim 12{\rm\,Gyr}$ age derived from the CMD comparison is also consistent
with estimates for Sequoia groups (Ruiz-Lara et al., 2022). Nonetheless,
Antaeus’ extraordinarily low mean $J_{z}$ and its position in the disk plane
of the MW both make it unique, even when compared to the global atlas of halo
structures from Malhan et al. (2022). If the structure is indeed related to
Sequoia, this difference has to be explained.

The mere existence of such a streamy, retrograde structure in the disk of the
MW is very puzzling. It is not clear how such kinematic coherence could be
retained if this population came in with Sequoia $9\sim 11{\rm\,Gyr}$ ago
(Myeong et al., 2019). Of course Antaeus’ progenitor could have arrived
initially with a small inclination, although this possibility appears somewhat
contrived. It seems more natural to explain the very low quantity of vertical
motion by dissipation due to dynamical friction, which might be consistent
with an early arrival in the MW. This scenario would invite the possibility
that Antaeus is the debris of the dense core of the Sequoia progenitor, which
would have stabilized in the disk through dynamical friction before tidal
disruption completely destroyed it.

The discovery of Antaeus opens many exciting possibilities for follow-up
studies. A first step would be finding other members of the structure in Gaia
with the information we now possess. Creating an $N$-body model for the infall
of the progenitor dwarf galaxy in the potential well of the MW and exploring
the possibilities for its survival in the disk would also be highly
informative. Finally, it would be very helpful to measure the metallicity of
more stars of our selection in order to facilitate discussions regarding the
origin of the structure, and links to Sequoia in particular.

## Data Availability

The data used in this contribution is available in Table 1.

Table 1: Sample from the 80 stars of our selection from Section 2. The full
sample is available in electronic format.

Gaia source ID | RA | DEC | $J_{r}$ | $J_{\phi}$ | $J_{z}$ | $r_{\rm peri}$ | $r_{\rm apo}$ | $e$ | [Fe/H]
---|---|---|---|---|---|---|---|---|---
| [deg] | [deg] | $[{\rm\,kpc}{\rm\,km\,s^{-1}}]$ | $[{\rm\,kpc}{\rm\,km\,s^{-1}}]$ | $[{\rm\,kpc}{\rm\,km\,s^{-1}}]$ | $[{\rm\,kpc}]$ | $[{\rm\,kpc}]$ |  | [dex]
3857833427353671808 | 159.91 | 4.08 | 1843.09 | 106.55 | 2976.68 | 7.31 | 40.78 | 0.70 | $-2.09\pm 0.30$
1558668134509319040 | 204.99 | 49.77 | 698.65 | 99.50 | 2846.51 | 8.19 | 25.57 | 0.51 | $-1.97\pm 0.12$
1374889335770878848 | 232.59 | 35.38 | 1936.15 | 45.67 | 3216.25 | 7.72 | 43.03 | 0.70 | $-1.88\pm 0.10$
950636967397629568 | 102.78 | 40.33 | 1505.39 | 83.11 | 2634.22 | 6.55 | 34.23 | 0.68 | $-1.77\pm 0.13$
3839165510915273856 | 139.71 | -0.89 | 1963.65 | 80.95 | 2947.99 | 7.09 | 41.87 | 0.71 | $-1.76\pm 0.08$
2657496656325125888 | 347.59 | 1.19 | 1963.74 | 9.28 | 2799.33 | 6.41 | 40.27 | 0.73 | $-1.62\pm 0.12$
231238462236707584 | 57.75 | 42.07 | 1680.13 | 33.76 | 2664.73 | 6.34 | 36.15 | 0.70 | $-1.54\pm 0.08$
3834229356541509760 | 147.87 | 0.89 | 1466.15 | 47.20 | 2770.15 | 6.84 | 34.32 | 0.67 | $-1.33\pm 0.23$
1950571427690143616 | 322.99 | 34.92 | 1216.32 | 14.63 | 3083.68 | 7.90 | 32.92 | 0.61 | -
2340952515729081728 | 359.75 | -21.81 | 1340.28 | 91.00 | 2532.56 | 6.35 | 31.65 | 0.67 | -

Note. — The information is derived from the MW potential of McMillan (2017).

The authors acknowledge funding from the European Research Council (ERC) under
the European Unions Horizon 2020 research and innovation programme (grant
agreement No. 834148) and from the Agence Nationale de la Recherche (ANR
projects ANR-18-CE31-0006 and ANR-19-CE31-0017). This work has made use of
data from the European Space Agency (ESA) mission Gaia
(https://www.cosmos.esa.int/gaia), processed by the Gaia Data Processing and
Analysis Consortium (DPAC,
https://www.cosmos.esa.int/web/gaia/dpac/consortium). Funding for the DPAC has
been provided by national institutions, in particular the institutions
participating in the Gaia Multilateral Agreement.

## References

  * Anders et al. (2022) Anders, F., Khalatyan, A., Queiroz, A. B. A., et al. 2022, A&A, 658, A91, doi: 10.1051/0004-6361/202142369
  * Belokurov et al. (2018) Belokurov, V., Erkal, D., Evans, N. W., Koposov, S. E., & Deason, A. J. 2018, MNRAS, 478, 611, doi: 10.1093/mnras/sty982
  * Bovy (2015) Bovy, J. 2015, ApJS, 216, 29, doi: 10.1088/0067-0049/216/2/29
  * Bovy (2020) —. 2020, arXiv e-prints, arXiv:2012.02169.  https://arxiv.org/abs/2012.02169
  * Bressan et al. (2012) Bressan, A., Marigo, P., Girardi, L., et al. 2012, MNRAS, 427, 127, doi: 10.1111/j.1365-2966.2012.21948.x
  * Carollo et al. (2007) Carollo, D., Beers, T. C., Lee, Y. S., et al. 2007, Nature, 450, 1020, doi: 10.1038/nature06460
  * Di Matteo et al. (2019) Di Matteo, P., Haywood, M., Lehnert, M. D., et al. 2019, A&A, 632, A4, doi: 10.1051/0004-6361/201834929
  * Gaia Collaboration (2022) Gaia Collaboration. 2022, Astronomy & Astrophysics, doi: 10.1051/0004-6361/202243940
  * Gaia Collaboration et al. (2016) Gaia Collaboration, Prusti, T., de Bruijne, J. H. J., et al. 2016, A&A, 595, A1, doi: 10.1051/0004-6361/201629272
  * Helmi et al. (2018) Helmi, A., Babusiaux, C., Koppelman, H. H., et al. 2018, Nature, 563, 85, doi: 10.1038/s41586-018-0625-x
  * Helmi & de Zeeuw (2000) Helmi, A., & de Zeeuw, P. T. 2000, MNRAS, 319, 657, doi: 10.1046/j.1365-8711.2000.03895.x
  * Helmi et al. (2017) Helmi, A., Veljanoski, J., Breddels, M. A., Tian, H., & Sales, L. V. 2017, A&A, 598, A58, doi: 10.1051/0004-6361/201629990
  * Ibata et al. (2021) Ibata, R., Malhan, K., Martin, N., et al. 2021, ApJ, 914, 123, doi: 10.3847/1538-4357/abfcc2
  * Majewski et al. (2012) Majewski, S. R., Nidever, D. L., Smith, V. V., et al. 2012, ApJ, 747, L37, doi: 10.1088/2041-8205/747/2/L37
  * Malhan et al. (2018) Malhan, K., Ibata, R. A., & Martin, N. F. 2018, MNRAS, 481, 3442, doi: 10.1093/mnras/sty2474
  * Malhan et al. (2022) Malhan, K., Ibata, R. A., Sharma, S., et al. 2022, ApJ, 926, 107, doi: 10.3847/1538-4357/ac4d2a
  * McMillan (2017) McMillan, P. J. 2017, MNRAS, 465, 76, doi: 10.1093/mnras/stw2759
  * Myeong et al. (2018) Myeong, G. C., Evans, N. W., Belokurov, V., Sanders, J. L., & Koposov, S. E. 2018, MNRAS, 478, 5449, doi: 10.1093/mnras/sty1403
  * Myeong et al. (2019) Myeong, G. C., Vasiliev, E., Iorio, G., Evans, N. W., & Belokurov, V. 2019, MNRAS, 488, 1235, doi: 10.1093/mnras/stz1770
  * Naidu et al. (2020) Naidu, R. P., Conroy, C., Bonaca, A., et al. 2020, ApJ, 901, 48, doi: 10.3847/1538-4357/abaef4
  * Ruiz-Lara et al. (2022) Ruiz-Lara, T., Matsuno, T., Sofie Lövdal, S., et al. 2022, arXiv e-prints, arXiv:2201.02405.  https://arxiv.org/abs/2201.02405
  * Schönrich et al. (2010) Schönrich, R., Binney, J., & Dehnen, W. 2010, MNRAS, 403, 1829, doi: 10.1111/j.1365-2966.2010.16253.x
  * Sestito et al. (2021) Sestito, F., Buck, T., Starkenburg, E., et al. 2021, MNRAS, 500, 3750, doi: 10.1093/mnras/staa3479
  * Vasiliev (2019) Vasiliev, E. 2019, MNRAS, 482, 1525, doi: 10.1093/mnras/sty2672
  * Wang et al. (2022) Wang, C., Huang, Y., Yuan, H., et al. 2022, ApJS, 259, 51, doi: 10.3847/1538-4365/ac4df7
  * Widmark et al. (2021) Widmark, A., de Salas, P. F., & Monari, G. 2021, A&A, 646, A67, doi: 10.1051/0004-6361/202039852
  * Yuan et al. (2020) Yuan, Z., Myeong, G. C., Beers, T. C., et al. 2020, ApJ, 891, 39, doi: 10.3847/1538-4357/ab6ef7


Copyright for this paper by its authors. Use permitted under Creative Commons
License Attribution 4.0 International (CC BY 4.0).

SMT 2024: Satisfiability Modulo Theories, July 22–23, 2024, Montreal, Canada

<EMAIL_ADDRESS>]<EMAIL_ADDRESS>]

# An SMT-LIB Theory of Finite Fields

Thomas Hader  Alex Ozdemir  TU Wien, Favoritenstraße 9-11, 1040 Wien, Austria
Stanford University; 353 Jane Stanford Way; Stanford, CA, 94305 USA

(2024)

###### Abstract

In the last few years there have been rapid developments in SMT solving for
finite fields. These include new decision procedures, new implementations of
SMT theory solvers, and new software verifiers that rely on SMT solving for
finite fields. To support interoperability in this emerging ecosystem, we
propose the SMT-LIB theory of finite field arithmetic (FFA). The theory
defines a canonical representation of finite field elements as well as
definitions of operations and predicates on finite field elements.

###### keywords:

SMT finite fields non-linear reasoning

##  1 Introduction

Finite fields are the basis for a large body of security-critical code. They
are used in public-key cryptography: elliptic curves over finite fields are
used in nearly all web browser connections for key exchange or digital
signatures [1, 2, 3]. They are used in private-key cryptography: in both the
Poly1305 message authentication code [4] and Galois counter mode (GCM) [5].
They are also the basis of most protocols for secure computation. For
instance, many zero-knowledge proof systems prove and verify predicates
expressed as finite field equations [6, 7, 8, 9]. Also, many secure multi-
party computation protocols evaluate circuits over finite fields [10, 11].
Finally, some homomorphic encryption schemes apply to data in a finite field
[12, 13].

The importance and prevalence of (finite-)field-based programs creates a need
for tools that can formally verify them. Ideally, such tools would be
partially or fully automated. The natural approach is SMT-based verification,
as taken by prior tools like Dafny [14] and Boogie [15]. In this approach, a
software verifier reduces the correctness of the program to logical formulas
which it dispatches to a satisfiability modulo theories (SMT) solver. Applying
this approach to field-based software generally requires an SMT solver that
can solve finite field equations.

One way to solve field equations is by encoding them as integer equations,
which many SMT solvers already comprehend. Consider (for the moment) a finite
field of prime order $p$. Such a field is isomorphic to the integers
$\\{0,\dots,p-1\\}$ with addition and multiplication modulo $p$ [16]. Thus,
(non-linear) equations mod $p$ can be encoded as (non-linear) integer
equations. In this encoding, an equation $xy=z$ over field variables $x,y,z$
would be encoded as $(x^{\prime}y^{\prime}-z^{\prime})\bmod p=0$, where
$x^{\prime},y^{\prime},z^{\prime}$ are the integer representatives of the
field variables. These equations can now be solved using an integer solver.
Or, since all terms can be bounded, they can be solved as bit-vector (bounded
integer) equations. However, prior experiments have shown that existing
integer and bit-vector solvers perform poorly when given inputs that encode
finite field arithmetic [17, 18].

To overcome the limitations of encoding, two direct SMT theory solvers for
finite fields have recently emerged. The first is an MCSat [19] solver that is
implemented in Yices [20, 21, 22, 23, 24]. The second is a CDCL(T) solver that
is implemented in cvc5 [17, 25, 26]. Currently, these solvers accept field
terms and equations expressed using a bespoke extension to SMT-LIB. This
extension has not been standardized.

These SMT solvers have already enabled a variety of research projects and
tools for automatically verifying systems that use zero-knowledge proofs
(ZKPs). One project builds an automatically verifiable compiler pass for CirC:
a compiler used with ZKPs [27]. Another builds a tool $\text{QED}^{2}$ that
automatically verifies ZKP code in the Circom language [28, 29]. Another
builds a tool for automatically verifying ZKP code written using the Halo2
library [30]. All of these projects use an SMT solver with finite field
support.

Given the long-term importance of finite fields to security-critical software,
the emergence of multiple SMT solvers with finite field support, and the
emergence of multiple automatic verification tools expecting finite field
support, we think the time is ripe to specify finite fields as an SMT-LIB
theory. In this short paper, we do exactly that. In our specification, we
consider all finite fields: those of prime order and their extensions. We
consider fields of arbitrary size. Many cryptosystems require large fields
(such as a prime order field with $p\approx 2^{256}$ or the binary extension
field of order $2^{128}$), but some can also operate over smaller fields (such
as 32-bit or 64-bit fields) [31, 32].

#### Related Work

There is already much work on verifying cryptographic implementations through
interactive theorem proving and verification languages. Examples of secret-key
and public-key cryptography include Fiat cryptography [33], Easycrypt [34],
HACL* [35], and Jasmin [36]. There is also some work on interactive
verification for ZKPs in the context of the Leo compiler [37], and by using
refinement proofs [38, 39]. With better SMT-level support for finite fields,
ITP proof automation for finite field lemmas could be improved through ITP-SMT
bridges, like SMTCoq [40].

Further afield, some cryptographic implementations have been modeled and
analyzed using automated symbolic analysis tools like Tamarin [41] and
ProVerif [42]. The benefit of these tools is their high level of
interpretability and automation, which allows them to be applied to protocols
of realistic complexity, such as Signal [43]. However, they struggle to
accurately model algebraic structures [44]. SMT-level algebraic reasoning
would complement this research.

Another line of research develops SMT solvers for non-linear integer and real
arithmetic using CDCL(T) [45, 46, 47, 48, 49, 50, 51, 52] and MCSat [53, 54,
55]. Some works specifically consider local search [56, 57, 58] and quantifier
elimination [59, 60]. This research serves as good inspiration into techniques
for finite field solving.

##  2 Background

We provide a brief summary of the relevant concepts of finite fields. A
comprehensive overview can be found in [61, 62, 63] as well as in many other
algebra textbooks.

#### Fields.

A field $\mathbb{F}$ consists of a set of elements $S$ on which the two binary
operators _addition_ “$+$” and _multiplication_ “$\cdot$” are defined. $S$ is
closed under both operators, i.e. when applied on two elements of $S$, the
result is in $S$. Both operators are commutative, associative, and have
distinct neutral elements (denoted as _zero_ (0) and _one_ (1), respectively).
Each element in $S$ has an additive inverse element and all elements in
$S\setminus\\{0\\}$ have a multiplicative inverse element. Further,
distributivity of multiplication over addition holds. Informally speaking, a
field is a set with well-defined operations addition, subtraction,
multiplication, and division (with the exception of division by $0$). Well
known examples of fields are the rational number $\mathbb{Q}$ and the real
numbers $\mathbb{R}$.

#### Finite Fields.

A field $\mathbb{F}$ where $S$ is finite is called a finite field.111In honor
of French mathematician Évariste Galois, finite fields are also called _Galois
fields_. The size of $S$ is the order of $\mathbb{F}$ . It has been shown that
every finite field has order $q$ that is a prime power $q=p^{n}$. We
distinguish between _prime fields_ with $n=1$ and _extension fields_ with
$n>1$. All fields of equal order are isomorphic (i.e. equivalent up to
relabelling of elements), thus the field of order $q$ is unique (up to
isomorphism).

#### Prime Fields.

The prime field of order $p$ can be represented as
$S=\\{-\left\lfloor\frac{p-1}{2}\right\rfloor,\dots,0,1,\dots,\left\lfloor\frac{p}{2}\right\rfloor\\}$222
In the (isomorphic) representation $S=\\{0,\dots,p-1\\}$, (with addition and
multiplication modulo $p$), small “negative” values (such as $-1$) are instead
represented as large positive values (such as $p-1$), which can be unintuitive
to read. We choose our representation because small negative values are common
in many applications.  and is denoted $\mathbb{F}_{p}$. Let the function
$\mathsf{smod}_{p}:\mathbb{Z}\to S$ be defined to map $z\in\mathbb{Z}$ to the
unique element of $S$ that is equivalent to $z$, modulo $p$. The function is
called “$\mathsf{smod}_{p}$” because it outputs a signed representation of its
input.

Addition and multiplication on $S$ are defined by the usual integer operations
followed by an application of $\mathsf{smod}_{p}$. Due to the construction of
$S$, finding the additive inverse is as simple as flipping the sign (assuming
odd $p$).

###### Example 1

The finite field $\mathbb{F}_{5}$ can be represented by the integers
$\\{-2,-1,0,1,2\\}$. In this representation of $\mathbb{F}_{5}$, $2+1=-2$,
$2\cdot(-1)=-2$, and $(2+1)\cdot 2=1$ hold.

#### Extension Fields.

Let $\mathbb{F}_{p}[\alpha]$ be the set of univariate polynomials in variable
$\alpha$ with coefficients from $\mathbb{F}_{p}$, and let
$f\in\mathbb{F}_{p}[\alpha]$ have degree $n$ and be irreducible (i.e. it
cannot be represented as the product of two non-constant polynomials). The
extension field of order $p^{n}$ is denoted $\mathbb{F}_{p^{n}}$ and can be
represented as polynomials in $\mathbb{F}_{p}[\alpha]$ of degree less than
$n$, with (polynomial) addition and multiplication modulo $f$. Note that, in
this representation,
$\\{0,1\\}\subseteq\mathbb{F}_{p}\subseteq\mathbb{F}_{p^{n}}$.

###### Example 2

The finite field $\mathbb{F}_{3^{2}}$ is represented by the following
polynomials of $\mathbb{F}_{3}[\alpha]$ modulo $\alpha^{2}-\alpha-1$:

$\\{0,\,\alpha,\,\alpha+1,\,-\alpha+1,\,-1,\,-\alpha,\,-\alpha-1,\,\alpha-1,\,1\\}$

Over $\mathbb{F}_{3^{2}}$ it holds that $(\alpha+1)\cdot\alpha=(-\alpha+1)$.

As the choice of $f$ is not unique in general, different (isomorphic)
representations of $\mathbb{F}_{p^{n}}$ exist, even if the representation of
$\mathbb{F}_{p}$ is fixed. Note that no finite field is an ordered field. That
is, there is no total ordering on $S$ that is compatible with the field
operations.

#### Conway Polynomials

Algebraic tools have many choices for how to represent fields internally. But,
to facilitate interoperability, the computer algebra community has agreed upon
a canonical family of irreducible polynomials that should be used to represent
elements of an extension field $\mathbb{F}_{p^{n}}$ in tool interfaces. These
are called the Conway polynomials $C_{p,n}\in\mathbb{F}_{p}[\alpha]$, where
$p$ is a prime and $n>1$. The precise definition of the Conway polynomials is
not important for our purposes.333 The Conway polynomial $C_{p,n}$ is the
lexicographically minimal monic primitive polynomial of degree $n$ over
$\mathbb{F}_{p}$ that is compatible with $C_{p,m}$ for all $m$ dividing $n$.
Let $r=(p^{n}-1)/(p^{m}-1)$ (which is an integer). Then,
$C_{p,n}\in\mathbb{F}[\alpha]$ is compatible with
$C_{p,m}\in\mathbb{F}[\alpha]$ if for every root
$\alpha_{0}\in\mathbb{F}_{p^{n}}$ of the former, $\alpha_{0}^{r}$ is a root of
the latter. The lexicographic ordering used is also slightly non-standard.
Define the alternating-sign coefficient representation of polynomial
$f\in\mathbb{F}[\alpha]$ to be
$f=\sum_{i=0}^{d}(-1)^{i}c_{d-i}\alpha^{d-i}=c_{d}\alpha^{d}-c_{d-1}\alpha^{d-1}+\cdots+(-1)^{d}a_{0}$,
with $c_{i}\in\\{0,\dots,p-1\\}$. Then, the order is lexicographic over the
tuples $(c_{d},\dots,c_{0})$.  There is an algorithm for finding them [64] and
they have been pre-computed for many $n$ and $p$ [65]. The Conway polynomials
are used by all prominent computer algebra libraries: Sage, Magma, GAP,
Singular, etc. We will use the Conway polynomials to define an SMT-LIB syntax
for extension field element literals (Sec. 3.3).

###### Example 3

The Conway polynomial $C_{3,2}$ is $\alpha^{2}-\alpha-1$, which is the
irreducible used to represent $\mathbb{F}_{9}$ in Example 2.

##  3 A Theory of Finite Fields

This section presents the SMT-LIB (version 2.6) _theory of finite field
arithmetic_ (FFA). Based on the theory of finite field arithmetic are the
logics of quantifier-free finite field arithmetic QF_FFA as well as its
quantified version FFA.

###  3.1 The Finite Field Sorts

The theory of finite fields defines two kinds of finite field sorts, _prime
field sorts_ and _extension field sorts_ for prime and extension fields,
respectively (Sec. 2). They are represented by an indexed sort identifier of
the form (_ FiniteField $p$) and (_ FiniteField $p$ $n$) for prime and
extension field sorts, respectively. The indexes $p$ and $n$ are numerals
specifying the finite field order $q=p^{n}$. The index $p$ must be a prime
number in both cases. For extension field sorts, $n>1$ must hold, as otherwise
the resulting sort would be a prime field. Providing a non-prime number as $p$
may result in unspecified solver behavior, although solvers are encouraged to
report an error. 444 We recommend that solvers test $p$’s primality
probabilistically, for example with a 40-repetition Miller-Rabin test [66]. If
$p$ is not prime, the solver can report an error. If $p$ is prime or if the
test is inconclusive, the solver may assume that $p$ is prime and continue.
As is usual for an indexed sort, two finite field sorts with a different order
are different sorts. Solvers implementing this theory are not required to
support extension field sorts and may report an error in case an extension
field sort is specified. 555 We choose different syntaxes for prime fields and
their extensions so that a user who is only interested in prime fields need
not understand or even be aware of extension fields.

For the rest of this chapter, a _finite field sort_ is a prime or extension
field sort with an arbitrary fixed order.

###### Example 4

Set the logic to non-linear finite field arithmetic and define finite field
sorts of size $5$ and $9$:

⬇

(set-logic QF_FFA)

(define-sort FF5 () (_ FiniteField 5))

(define-sort FF9 () (_ FiniteField 3 2))

###  3.2 The Domain of Finite Field elements

A finite field of a given order is uniquely defined up to isomorphism. Thus,
for the sake of defining an SMT theory for finite fields, a canonical
representation for a finite field of a given order needs to be fixed.
Otherwise different solvers might present the same model differently.

For a prime field with prime order $p$, the elements are represented by the
integers of the set
$\\{-\left\lfloor\frac{p-1}{2}\right\rfloor,\dots,\left\lfloor\frac{p}{2}\right\rfloor\\}$.
Operations are performed with regard to the function $\mathsf{smod}_{p}$ as
defined in Section 2. For an extension field of order $p^{n}$ the field
elements are represented by univariate polynomials over the prime field of
order $p$. The implied field is $\mathbb{F}[\alpha]/C_{p,n}$, where $C_{p,n}$
is the Conway polynomial (Sec. 2). All polynomial operations are performed
modulo the Conway polynomial $C_{p,n}$.

###  3.3 Finite Field Literals

In the theory of finite fields, each element of a finite field sort is
represented by a literal. To avoid confusion with the theories of integer and
reals, finite field literals are prefixed with the string ff. We further say
that a literal is _normalized_ when it stands for an element from the fixed
field representation as defined in Section 3.2. Non-normalized literals are
allowed as an input and are mapped to the corresponding normalized literal,
however, solvers are required to resort to normalized literals when printing a
value.

#### Prime field literals.

As stated in Section 2, elements of prime fields can be represented as
integers modulo the field size. This property is used to define literals in
the form of ff$N$, where $N$ is an integer value. Given a prime field sort (_
FiniteField $p$) with prime order $p$, elements represented by the literals
ff$N$ for all values
$N\in\\{-\left\lfloor\frac{p-1}{2}\right\rfloor,\dots,\left\lfloor\frac{p}{2}\right\rfloor\\}$
are normalized. Every literal outside this set is mapped to the corresponding
normalized literal by utilizing $\mathsf{smod}_{p}(N)$. Using this operation,
the input gets mapped to the (unique) normalized representative of the same
congruence class modulo $p$. In the presence of finite field theory, the user
may not define their own symbols of form ff$N$ (nor may they shadow other
theory-defined symbols).

###### Example 5

Given the defined sorts of Example 4, then examples of normalized elements of
FF5 are ff1, ff0, and ff-2. The (non-normalized) literals ff4 and ff10
describe the same element as the normalized literals ff-1 and ff0,
respectively.

#### Extension field literals.

Elements of extension field sorts are polynomials. Literals representing
elements of extension field sorts are uniquely describing polynomials by
specifying their coefficients. As described in Section 2, an element of a
finite field of order $q=p^{n}$ with $n>1$ is a polynomial
$P\in\mathbb{F}_{p}[\alpha]$ of degree at most $n-1$. Let
$P=c_{0}+c_{1}\alpha^{1}+\cdots+c_{n-1}\alpha^{n-1}$ where
$c_{i}\in\mathbb{F}_{p}$, then the element $P$ is represented by the literal
ff$c_{0}$.$c_{1}$.$\cdots$.$c_{n-1}$ where all $c_{i}$ are integers. Tailing
zeros may be omitted, e.g. in (_ FiniteField 3 6) the literals ff1.0.-1.0.0
and ff1.0.-1 both represent the element $1-\alpha^{2}$. This further ensures
that elements in $\mathbb{F}_{p}\subseteq\mathbb{F}_{p^{n}}$ have the same
literal representation in both (_ FiniteField $p$) and (_ FiniteField $p$
$n$). A (polynomial) literal of (_ FiniteField $p$ $n$) is normalized when all
integer coefficients are normalized with regard to $p$ and all tailing zeros
are omitted. Specifying a literal with more than $n$ coefficients is invalid.

###### Example 6

Again, given the defined sorts of Example 4, normalized literals of FF9 are
all (normalized) literals of (_ FiniteField 3): ff0, ff1, and ff-1, as well as
literals representing the further (polynomial) elements of
$\mathbb{F}_{3^{2}}$, for example ff-1.1, ff0.1, and ff-1.-1 representing the
elements $\alpha-1$, $\alpha$, and $-\alpha-1$, respectively. Note that ff2.1
and ff1.0 are both non-normalized versions of ff-1.1 and ff1, respectively.

#### Well-Sortedness of literals.

Since the defined literals are overloaded (for example, every finite field has
a one element, thus ff1 is of undetermined sort), the order of the literal’s
field must be specified in order to satisfy the well-sortedness requirements
of SMT-LIB. There are two ways of specifying the sort of a finite field
literal.  (i) By indexing the literal (_ ff$\dots$ $p$) and (_ ff$\dots$ $p$
$n$) with the finite field order $p$ and $p^{n}$, respectively. This allows
the literal’s sort to be derived, as the order of the finite field specifies
the sort uniquely.  (ii) Since $p$ might be a large number, a short-cut is
provided by (as ff$\dots$ $S$) where $S$ is a finite field sort. Using the
define-sort command, one can assign a symbol to a finite field sort to be used
for all its literals.  Table 1 gives an overview of all variants.

field type | order | syntax | syntax type
---|---|---|---
prime field | $p$ | (_ ff$N$ $p$) | indexed
|  | (as ff$N$ (_ FiniteField $p$)) | annotated
extension field | $p^{n}$ | (_ ff$N$.$\cdots$.$N$ $p$ $n$) | indexed
|  | (as ff$N$.$\cdots$.$N$ (_ FiniteField $p$ $n$)) | annotated
Table 1:  Different ways to define literals.

###### Example 7

The expressions (_ ff1 5) and (_ ff1 3 2) denote the multiplicative identity
(one) of $\mathbb{F}_{5}$ and $\mathbb{F}_{3^{2}}$, respectively. Using the
defined sorts from Example 4, (as ff1 FF5) and (as ff1 FF9) can be used
alternatively.

#### Reporting Models.

To make it easy for tools to parse models, all solvers must report models
using normalized literals in the indexed representation.

###  3.4 Finite Field Operations

All of the following operator definitions represent well known semantics from
algebra. Thus, an explicit definition of their semantics is omitted and we
refer to Section 2 for further details. Operations always operate on one
specific finite field sort $S$, i.e. all parameters have sort $S$ and an
element of $S$ is returned. All functions are defined for all prime field
sorts as well as all extension field sorts. For the sake of brevity, the
extension field sort variants of the functions are omitted. Table 2 gives an
overview of all operations.

#### Binary arithmetic.

For each finite field order, we define operations that take two finite field
elements of one finite field sort and return an element of the same sort.
Given two inputs, the operations represent sum, difference, product, and
quotient, respectively.666 Since ff.neg and ff.recip are defined as well,
ff.sub and ff.div are redundant. However, we believe that all common
mathematical operations should have operations in the finite field theory.
Furthermore, other arithmetic theories in SMT-LIB also define redundant
subtraction and division operators.

(ff.add (_ FiniteField $p$) (_ FiniteField $p$) (_ FiniteField $p$) :left-
assoc) (ff.sub (_ FiniteField $p$) (_ FiniteField $p$) (_ FiniteField $p$))
(ff.mul (_ FiniteField $p$) (_ FiniteField $p$) (_ FiniteField $p$) :left-
assoc) (ff.div (_ FiniteField $p$) (_ FiniteField $p$) (_ FiniteField $p$))

As hinted by the :left-assoc keyword, occurrences of ff.add and ff.mul may
contain more than two arguments and multiple arguments are grouped left
associatively. However, note that both operations are associative anyway. 777
Note that ff.div is not Euclidean division, rather it is multiplication by an
inverse in the field. Thus, the remainder of a division, i.e. ff.rem, would
not be meaningful.

#### Unary arithmetic.

For each finite field sort, there are the following unary operations:

(ff.neg (_ FiniteField $p$) (_ FiniteField $p$))

(ff.recip (_ FiniteField $p$) (_ FiniteField $p$))

Here, ff.neg returns the unary negation (usually written as $-x$ for an
element $x$), i.e. the inverse element with regard to addition. The operation
ff.recip returns the reciprocal value (usually written as $x^{-1}$ for an
element $x$), i.e. the inverse element with regard to multiplication.

#### Division by zero.

Two operators (ff.div, ff.recip) represent mathematical operations with only
partial semantics. Mathematically speaking, division by zero is undefined, and
computing the reciprocal of zero is undefined. Yet, SMT-LIB requires functions
to have total semantics. We require solvers to interpret the reciprocal of
zero as zero. Moreover dividing any value by zero gives zero. This choice is
somewhat arbitrary. It is acceptable because it easy for solvers to meet and
for verification tools to use.

A solver can meet this requirement using a preprocessing transformation.
First, it encodes division as multiplication by the divisor’s reciprocal.
Second, it encodes the reciprocal relation $z=\texttt{(ff.recip }x\texttt{)}$
by the following (reciprocal-free) formula:

$\displaystyle[(x\neq 0)\wedge(xz=1)]\vee[(x=0)\wedge(z=0)]$

This ensures that $0$’s reciprocal is $0$. The are other encodings of
reciprocal that do not explicitly contain a disjunction. For example, as
$(zzx=z)\land(zxx=x)$.

This requirement is also easy for verification tools that use SMT to work
with. In particular, a verification tool can create an SMT query where
division or reciprocal have different semantics by wrapping them with an if-
then-else term that implements those semantics when the appropriate input is
zero.

Identifier | Sort | Meaning
---|---|---
ff.add | $F\times F\to F$ | finite field addition
ff.sub | $F\times F\to F$ | finite field subtraction
ff.mul | $F\times F\to F$ | finite field multiplication
ff.div | $F\times F\to F$ | finite field division
ff.neg | $F\to F$ | finite field negation
ff.recip | $F\to F$ | finite field reciprocal
Table 2:  A summary of finite field operations for a finite field type $F$.

###  3.5 Comparison

Since finite fields are not ordered, the theory of finite fields only supports
the equality predicate:

(= (_ FiniteField $p$) (_ FiniteField $p$))
(= (_ FiniteField $p$ $n$) (_ FiniteField $p$ $n$))

###### Example 8

Continuing with the definition of Example 4. First define some variables:

⬇

(declare-fun x0 () FF5)

(declare-fun x1 () FF5)

(declare-fun x2 () FF5)

Then add some assertions:

⬇

(assert (= (ff.mul x1 x2) (ff.add x1 x2)))

(assert (= (ff.recip x1) x0))

(assert (= (ff.sub x2 x0)) (as ff1 FF5))

This encodes the constraint system in $\mathbb{F}_{5}$:

$\begin{split}x_{1}x_{2}&=x_{1}+x_{2}\\\ x_{1}^{-1}&=x_{0}\\\
x_{2}-x_{0}&=1\end{split}$

##  4 Existing Finite Field Solvers

There are two existing SMT solvers that support the theory of finite fields:
Yices [23] and cvc5 [26]. Both support the logic of quantifier-free finite
field arithmetic QF_FFA for prime fields as defined in this paper.

  * •

Yices2 implements reasoning over prime fields using its MCSat engine [24].
This implementation is based on the approach by Hader et al. [22]. Processing
of polynomials over prime fields is done done using an updated version of the
LibPoly library [67].

  * •

cvc5’s prime field solver is a CDCL($\mathcal{T}$) theory solver that
implements two decision procedures designed by Ozdemir et al. The first
procedure is based on Gröbner bases and triangular decomposition [17]. The
second is based on the same algebraic ideas, but uses multiple, small Gröbner
bases for better scalability in some cases [25]. The implementation uses the
CoCoALib computer algebra library [68].

##  5 Future Directions

In designing our theory, we have intentionally omitted a number of potential
features. Some of these features might be good additions in the future. We
discuss two such features here, together with why they might be useful.

#### Conversions

In this proposal, we do not give operations for converting between finite
field elements and other discrete arithmetic types, such as integers and bit-
vectors. This might be useful for verification problems about code that
converts between these types. For example, the AES-GCM block cipher alternates
between treating its data as bit-vectors and elements of $\mathbb{F}_{2^{n}}$,
to perform different kinds of operations on that data. The bit-vector
representation is used for the AES permutation and the field representation is
used in the GCM message authentication code. Another example is an
implementation of $\mathbb{F}_{p}$ arithmetic on a $b$-bit CPU, where
$2^{b}\ll p$. Such an implementation is defined by bit-vector arithmetic, but
the specification is an equation in $\mathbb{F}_{p}$. Thus, giving a natural
statement of the implementation’s correctness requires operations to convert
between $\mathbb{F}_{p}$ and bit-vectors. Since some SMT solvers already allow
conversions between bit-vectors and integers, conversions between integers and
finite field elements might suffice.

Another kind of conversion which might be useful is one between a field
$\mathbb{F}_{p^{n}}$ and some extension $\mathbb{F}_{(p^{n})^{e}}$ of it (for
$e>1$).

#### Variable-sized fields

In this proposal, we consider only fields of fixed size. This bars the
possibility of queries that verify a property that holds generically for many
or all fields. Such properties arise naturally in many verification problems.
For instance, one might have a function that implements some finite-field
operation in which the size of the field is an input to the function. To
verify the function for all fields, one might construct a logical formula in
which the field size is a variable.

#### Acknowledgements.

We thank Ahmed Irfan, Alp Bassa, Clark Barrett, Daniela Kaufmann, Gereon
Kremer, Shankara Pailoor, Sorawee Porncharoenwase, and the SMT’24 reviewers
for valuable discussion and feedback. We further thank Stéphane Graham-
Lengrand for hosting the first author for a research stay at SRI during which
the idea for this work initiated. We acknowledge funding from the TU Wien
SecInt Doctoral College, NSF grant number 2110397, the Stanford Center for
Automated Reasoning, and the Simons Foundation.

## References

  * Barker et al. [2018] E. Barker, L. Chen, A. Roginsky, A. Vassilev, R. Davis, Recommendation for pair-wise key-establishment schemes using discrete logarithm cryptography, 2018\. https://doi.org/10.6028/NIST.SP.800-56Ar3.
  * Kotzias et al. [2018] P. Kotzias, A. Razaghpanah, J. Amann, K. G. Paterson, N. Vallina-Rodriguez, J. Caballero,  Coming of age: A longitudinal study of TLS deployment,  in: IMC, 2018.
  * Anderson and McGrew [2019] B. Anderson, D. McGrew,  TLS beyond the browser: Combining end host and network data to understand application behavior,  in: IMC, 2019.
  * Bernstein [2005] D. J. Bernstein,  The Poly1305-AES message-authentication code,  in: FSE, 2005.
  * Salowey et al. [2008] J. Salowey, A. Choudhury, D. McGrew, Rfc 5288: AES galois counter mode (GCM) cipher suites for TLS, 2008.
  * Goldwasser et al. [1985] S. Goldwasser, S. Micali, C. Rackoff,  The knowledge complexity of interactive proof-systems (extended abstract),  in: STOC, 1985.
  * Parno et al. [2016] B. Parno, J. Howell, C. Gentry, M. Raykova,  Pinocchio: Nearly practical verifiable computation,  Communications of the ACM (2016).
  * Groth [2016] J. Groth,  On the size of pairing-based non-interactive arguments,  in: EUROCRYPT, 2016.
  * Chaliasos et al. [2024] S. Chaliasos, J. Ernstberger, D. Theodore, D. Wong, M. Jahanara, B. Livshits,  SoK: What don’t we know? understanding security vulnerabilities in SNARKs,  arXiv preprint arXiv:2402.15293 (2024).
  * Damgård et al. [2012] I. Damgård, V. Pastro, N. Smart, S. Zakarias,  Multiparty computation from somewhat homomorphic encryption,  in: CRYPTO, 2012.
  * Hastings et al. [2019] M. Hastings, B. Hemenway, D. Noble, S. Zdancewic,  SoK: General purpose compilers for secure multi-party computation,  in: IEEE S&P, 2019.
  * Regev [2009] O. Regev,  On lattices, learning with errors, random linear codes, and cryptography,  J. ACM (2009).
  * Viand et al. [2021] A. Viand, P. Jattke, A. Hithnawi,  SoK: Fully homomorphic encryption compilers,  in: IEEE S&P, 2021.
  * Leino [2010] K. R. M. Leino,  Dafny: An automatic program verifier for functional correctness,  in: LPAR, 2010.
  * Barnett et al. [2006] M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, K. R. M. Leino,  Boogie: A modular reusable verifier for object-oriented programs,  in: Formal Methods for Components and Objects, 2006\.
  * Dummit and Foote [2004] D. S. Dummit, R. M. Foote, Abstract algebra, volume 3, Wiley Hoboken, 2004.
  * Ozdemir et al. [2023] A. Ozdemir, G. Kremer, C. Tinelli, C. Barrett,  Satisfiability modulo finite fields,  in: CAV, 2023.
  * Niemetz et al. [2024] A. Niemetz, M. Preiner, Y. Zohar,  Scalable bit-blasting with abstractions,  in: CAV, 2024.
  * Jovanovic et al. [2013] D. Jovanovic, C. Barrett, L. De Moura,  The design and implementation of the model constructing satisfiability calculus,  in: FMCAD, 2013.
  * Hader [2022] T. Hader, Non-linear SMT-reasoning over finite fields, 2022. MSc Thesis (TU Wien).
  * Hader and Kovács [2022] T. Hader, L. Kovács,  Non-linear SMT-reasoning over finite fields,  in: SMT, 2022. URL: http://ceur-ws.org/Vol-3185/extended3245.pdf, extended Abstract.
  * Hader et al. [2023] T. Hader, D. Kaufmann, L. Kovács,  SMT solving over finite field arithmetic,  in: LPAR, 2023.
  * Dutertre [2014] B. Dutertre,  Yices 2.2,  in: CAV, 2014.
  * Hader et al. [2024] T. Hader, D. Kaufmann, A. Irfan, S. Graham-Lengrand, L. Kovács,  MCSat-based Finite Field Reasoning in the Yices2 SMT Solver,  in: IJCAR, 2024.
  * Ozdemir et al. [2024] A. Ozdemir, S. Pailoor, A. Bassa, K. Ferles, C. Barrett, I. Dillig, Split Gröbner bases for satisfiability modulo finite fields, 2024. https://ia.cr/2024/572.
  * Barbosa et al. [2022] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar,  cvc5: A versatile and industrial-strength SMT solver,  in: TACAS, 2022.
  * Ozdemir et al. [2023] A. Ozdemir, R. S. Wahby, F. Brown, C. Barrett,  Bounded verification for finite-field-blasting,  in: CAV, 2023.
  * Pailoor et al. [2023] S. Pailoor, Y. Chen, F. Wang, C. Rodríguez, J. Van Geffen, J. Morton, M. Chu, B. Gu, Y. Feng, I. Dillig,  Automated detection of under-constrained circuits in zero-knowledge proofs,  in: PLDI, 2023.
  * Bellés-Muñoz et al. [2022] M. Bellés-Muñoz, M. Isabel, J. L. Muñoz-Tapia, A. Rubio, J. Baylina,  Circom: A circuit description language for building zero-knowledge applications,  IEEE Transactions on Dependable and Secure Computing (2022).
  * Soureshjani et al. [2023] F. H. Soureshjani, M. Hall-Andersen, M. Jahanara, J. Kam, J. Gorzny, M. Ahmadvand, Automated analysis of Halo2 circuits, 2023\. https://ia.cr/2023/1051.
  * Zero [2022] P. Zero, Plonky2: Fast recursive arguments with Plonk and FRI, 2022. https://github.com/0xPolygonZero/plonky2/blob/main/plonky2/plonky2.pdf.
  * Ben-Sasson et al. [2018] E. Ben-Sasson, I. Bentov, Y. Horesh, M. Riabzev,  Fast reed-solomon interactive oracle proofs of proximity,  in: ICALP, 2018.
  * Erbsen et al. [2020] A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala,  Simple high-level code for cryptographic arithmetic – with proofs, without compromises (2020).
  * Barthe et al. [2012] G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, P.-Y. Strub,  Easycrypt: A tutorial,  International School on Foundations of Security Analysis and Design (2012) 146–166.
  * Zinzindohoué et al. [2017] J.-K. Zinzindohoué, K. Bhargavan, J. Protzenko, B. Beurdouche,  HACL*: A verified modern cryptographic library,  in: CCS, 2017.
  * Almeida et al. [2017] J. B. Almeida, M. Barbosa, G. Barthe, A. Blot, B. Grégoire, V. Laporte, T. Oliveira, H. Pacheco, B. Schmidt, P.-Y. Strub,  Jasmin: High-assurance and high-speed cryptography,  in: CCS, 2017.
  * Coglio et al. [2023] A. Coglio, E. McCarthy, E. W. Smith, Formal verification of zero-knowledge circuits, 2023. URL: http://dx.doi.org/10.4204/EPTCS.393.9.
  * Liu et al. [2023] J. Liu, I. Kretz, H. Liu, B. Tan, J. Wang, Y. Sun, L. Pearson, A. Miltner, I. Dillig, Y. Feng,  Certifying zero-knowledge circuits with refinement types,  arXiv preprint arXiv:2304.07648 (2023).
  * Jiang et al. [2023] K. Jiang, D. Chait-Roth, Z. DeStefano, M. Walfish, T. Wies,  Less is more: refinement proofs for probabilistic proofs,  in: IEEE S&P, 2023.
  * Ekici et al. [2017] B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds, C. Barrett,  SMTCoq: A plug-in for integrating SMT solvers into Coq,  in: CAV, 2017.
  * Meier et al. [2013] S. Meier, B. Schmidt, C. Cremers, D. Basin,  The TAMARIN prover for the symbolic analysis of security protocols,  in: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013\. Proceedings 25, Springer, 2013, pp. 696–701.
  * Blanchet et al. [2018] B. Blanchet, B. Smyth, V. Cheval, M. Sylvestre,  ProVerif 2.00: automatic cryptographic protocol verifier, user manual and tutorial (2018).
  * Cohn-Gordon et al. [2020] K. Cohn-Gordon, C. Cremers, B. Dowling, L. Garratt, D. Stebila,  A formal security analysis of the Signal messaging protocol,  Journal of Cryptology 33 (2020) 1914–1983.
  * Cremers and Jackson [2019] C. Cremers, D. Jackson,  Prime, order please! revisiting small subgroup and invalid curve attacks on protocols using Diffie-Hellman,  in: CSF, 2019.
  * Ábrahám et al. [2021] E. Ábrahám, J. H. Davenport, M. England, G. Kremer,  Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings,  Journal of Logical and Algebraic Methods in Programming 119 (2021).
  * Cimatti et al. [2018] A. Cimatti, A. Griggio, A. Irfan, M. Roveri, R. Sebastiani,  Experimenting on solving nonlinear integer arithmetic with incremental linearization,  in: International Conference on Theory and Applications of Satisfiability Testing, Springer, 2018, pp. 383–398.
  * Maréchal et al. [2016] A. Maréchal, A. Fouilhé, T. King, D. Monniaux, M. Périn,  Polyhedral approximation of multivariate polynomials using Handelman’s theorem,  in: VMCAI, 2016.
  * Fränzle et al. [2006] M. Fränzle, C. Herde, T. Teige, S. Ratschan, T. Schubert,  Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure,  Journal on Satisfiability, Boolean Modeling and Computation 1 (2006).
  * Tung et al. [2016] V. X. Tung, T. V. Khanh, M. Ogawa,  raSAT: An SMT solver for polynomial constraints,  in: IJCAR, 2016.
  * Jovanović and Moura [2011] D. Jovanović, L. d. Moura,  Cutting to the chase solving linear integer arithmetic,  in: CADE, 2011.
  * Dillig et al. [2009] I. Dillig, T. Dillig, A. Aiken,  Cuts from proofs: A complete and practical technique for solving linear inequalities over integers,  2009, pp. 233–247.
  * Corzilius et al. [2015] F. Corzilius, G. Kremer, S. Junges, S. Schupp, E. Ábrahám,  SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving,  in: SAT, 2015.
  * Jovanović and De Moura [2013] D. Jovanović, L. De Moura,  Solving non-linear arithmetic,  ACM Communications in Computer Algebra 46 (2013).
  * Jovanović [2017] D. Jovanović,  Solving nonlinear integer arithmetic with MCSAT,  in: VMCAI, 2017.
  * Moura and Jovanović [2013] L. d. Moura, D. Jovanović,  A model-constructing satisfiability calculus,  in: VMCAI, 2013.
  * Cai et al. [2023] S. Cai, B. Li, X. Zhang,  Local search for satisfiability modulo integer arithmetic theories,  ACM Transactions on Computational Logic (2023).
  * Zhang et al. [2024] X. Zhang, B. Li, S. Cai,  Deep combination of CDCL (T) and local search for satisfiability modulo non-linear integer arithmetic theory,  2024\.
  * Wang et al. [2023] Z. Wang, B. Zhan, B. Li, S. Cai,  Efficient local search for nonlinear real arithmetic,  in: VMCAI, 2023.
  * Caviness and Johnson [1998] B. F. Caviness, J. R. Johnson, Quantifier elimination and cylindrical algebraic decomposition, Springer Science & Business Media, 1998\.
  * Weispfenning [1997] V. Weispfenning,  Quantifier elimination for real algebra—the quadratic case and beyond,  Applicable Algebra in Engineering, Communication and Computing 8 (1997).
  * Lidl and Niederreiter [1994] R. Lidl, H. Niederreiter, Introduction to finite fields and their applications, Cambridge university press, 1994.
  * McEliece [2012] R. J. McEliece, Finite fields for computer scientists and engineers, volume 23, Springer Science & Business Media, 2012\.
  * Gallian [2021] J. A. Gallian, Contemporary Abstract Algebra, Chapman and Hall/CRC, 2021.
  * Heath and Loehr [2004] L. S. Heath, N. A. Loehr,  New algorithms for generating conway polynomials over finite fields,  Journal of Symbolic Computation 38 (2004) 1003–1024.
  * Lübeck [????] F. Lübeck, Conway polynomials for finite fields, ???? Pre-computed Conway polynomials. Available at https://www.math.rwth-aachen.de/~Frank.Luebeck/data/ConwayPol/index.html or https://github.com/sagemath/conway-polynomials.
  * Rabin [1980] M. O. Rabin,  Probabilistic algorithm for testing primality,  Journal of number theory 12 (1980) 128–138.
  * Jovanovic and Dutertre [2017] D. Jovanovic, B. Dutertre,  Libpoly: A library for reasoning about polynomials,  in: Intl. Workshop on Satisfiability Modulo Theories (SMT), CEUR Workshop Proceedings, 2017.
  * Abbott and Bigatti [2018] J. Abbott, A. M. Bigatti,  Gröbner bases for everyone with CoCoA-5 and CoCoALib,  in: The 50th Anniversary of Gröbner Bases, volume 77, Mathematical Society of Japan, 2018, pp. 1–25.