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 𝑝. Such a field is isomorphic to the integers {0, . . . , 𝑝 − 1} with addition and multiplication modulo 𝑝 [16]. Thus, (non-linear) equations mod 𝑝 can be encoded as (non-linear) integer equations. In this encoding, an equation 𝑥𝑦 = 𝑧 over field variables 𝑥, 𝑦, 𝑧 would be encoded as (𝑥 ′ 𝑦 ′ − 𝑧 ′ ) mod 𝑝 = 0, where 𝑥 ′ , 𝑦 ′ , 𝑧 ′ 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 QED 2 that automatically verifies ZKP code in the Circom language [28,29]. Another builds a tool for automatically verifying SMT 2024: Satisfiability Modulo Theories, July 22-23, 2024, Montreal, Canada thomas.hader@tuwien.ac.at (T. Hader); aozdemir@cs.stanford.edu (A. Ozdemir) 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 𝑝 ≈ 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.

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 F consists of a set of elements 𝑆 on which the two binary operators addition "+" and multiplication "•" are defined. 𝑆 is closed under both operators, i.e. when applied on two elements of 𝑆, the result is in 𝑆. Both operators are commutative, associative, and have distinct neutral elements (denoted as zero (0) and one (1), respectively). Each element in 𝑆 has an additive inverse element and all elements in 𝑆 ∖ {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 Q and the real numbers R.

Finite Fields.

A field F where 𝑆 is finite is called a finite field. 1 The size of 𝑆 is the order of F. It has been shown that every finite field has order 𝑞 that is a prime power 𝑞 = 𝑝 𝑛 . We distinguish between prime fields with 𝑛 = 1 and extension fields with 𝑛 > 1. All fields of equal order are isomorphic (i.e. equivalent up to relabelling of elements), thus the field of order 𝑞 is unique (up to isomorphism).

Prime Fields. The prime field of order 𝑝 can be represented as

𝑆 = {− ⌊︁ 𝑝−1 2 ⌋︁ , . . . , 0, 1, . . . , ⌊︀ 𝑝 2 ⌋︀

} 2 and is denoted F 𝑝 . Let the function smod 𝑝 : Z → 𝑆 be defined to map 𝑧 ∈ Z to the unique element of 𝑆 that is equivalent to 𝑧, modulo 𝑝. The function is called "smod 𝑝 " because it outputs a signed representation of its input.

Addition and multiplication on 𝑆 are defined by the usual integer operations followed by an application of smod 𝑝 . Due to the construction of 𝑆, finding the additive inverse is as simple as flipping the sign (assuming odd 𝑝). Extension Fields. Let F 𝑝 [𝛼] be the set of univariate polynomials in variable 𝛼 with coefficients from F 𝑝 , and let 𝑓 ∈ F 𝑝 [𝛼] have degree 𝑛 and be irreducible (i.e. it cannot be represented as the product of two non-constant polynomials). The extension field of order 𝑝 𝑛 is denoted F 𝑝 𝑛 and can be represented as polynomials in F 𝑝 [𝛼] of degree less than 𝑛, with (polynomial) addition and multiplication modulo 𝑓 . Note that, in this representation, {0,

1} ⊆ F 𝑝 ⊆ F 𝑝 𝑛 . Example 2. The finite field F 3 2 is represented by the following polynomials of F 3 [𝛼] modulo 𝛼 2 − 𝛼 − 1: {0, 𝛼, 𝛼 + 1, −𝛼 + 1, −1, −𝛼, −𝛼 − 1, 𝛼 − 1, 1} Over F 3 2 it holds that (𝛼 + 1) • 𝛼 = (−𝛼 + 1).

As the choice of 𝑓 is not unique in general, different (isomorphic) representations of F 𝑝 𝑛 exist, even if the representation of F 𝑝 is fixed. Note that no finite field is an ordered field. That is, there is no total ordering on 𝑆 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 F 𝑝 𝑛 in tool interfaces. These are called the Conway polynomials 𝐶 𝑝,𝑛 ∈ F 𝑝 [𝛼], where 𝑝 is a prime and 𝑛 > 1.

The precise definition of the Conway polynomials is not important for our purposes. 3 There is an algorithm for finding them [64] and they have been pre-computed for many 𝑛 and 𝑝 [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 𝐶3,2 is 𝛼 2 − 𝛼 − 1, which is the irreducible used to represent F 9 in Example 2.

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 The Conway polynomial 𝐶𝑝,𝑛 is the lexicographically minimal monic primitive polynomial of degree 𝑛 over F𝑝 that is compatible with 𝐶𝑝,𝑚 for all 𝑚 dividing 𝑛. Let 𝑟 = (𝑝 𝑛 − 1)/(𝑝 𝑚 − 1) (which is an integer). Then, 𝐶𝑝,𝑛 ∈ F[𝛼] is compatible with 𝐶𝑝,𝑚 ∈ F[𝛼] if for every root 𝛼0 ∈ F𝑝𝑛 of the former, 𝛼 𝑟 0 is a root of the latter. The lexicographic ordering used is also slightly non-standard. Define the alternating-sign coefficient representation of polynomial 𝑓 ∈ F[𝛼] to be

𝑓 = ∑︀ 𝑑 𝑖=0 (−1) 𝑖 𝑐 𝑑−𝑖 𝛼 𝑑−𝑖 = 𝑐 𝑑 𝛼 𝑑 − 𝑐 𝑑−1 𝛼 𝑑−1 + • • • + (−1) 𝑑 𝑎0, with 𝑐𝑖 ∈ {0, . . . , 𝑝 − 1}.

Then, the order is lexicographic over the tuples (𝑐 𝑑 , . . . , 𝑐0).

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 𝑝) and (_ FiniteField 𝑝 𝑛) for prime and extension field sorts, respectively. The indexes 𝑝 and 𝑛 are numerals specifying the finite field order 𝑞 = 𝑝 𝑛 . The index 𝑝 must be a prime number in both cases. For extension field sorts, 𝑛 > 1 must hold, as otherwise the resulting sort would be a prime field. Providing a non-prime number as 𝑝 may result in unspecified solver behavior, although solvers are encouraged to report an error. 4 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. 5For 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))

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 𝑝, the elements are represented by the integers of the set

{− ⌊︁ 𝑝−1 2 ⌋︁ , . . . , ⌊︀ 𝑝 2 ⌋︀ }.

Operations are performed with regard to the function smod as defined in Section 2. For an extension field of order 𝑝 𝑛 the field elements are represented by univariate polynomials over the prime field of order 𝑝. The implied field is F[𝛼]/𝐶 𝑝,𝑛 , where 𝐶 𝑝,𝑛 is the Conway polynomial (Sec. 2). All polynomial operations are performed modulo the Conway polynomial 𝐶 𝑝,𝑛 .

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𝑁 , where 𝑁 is an integer value. Given a prime field sort (_ FiniteField 𝑝) with prime order 𝑝, elements represented by the literals ff𝑁 for all values 𝑁 ∈ {− ⌊︁ presence of finite field theory, the user may not define their own symbols of form ff𝑁 (nor may they shadow other theory-defined symbols). 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 𝑞 = 𝑝 𝑛 with 𝑛 > 1 is a polynomial

Example 5. Given the defined sorts of𝑃 ∈ F 𝑝 [𝛼] of degree at most 𝑛 − 1. Let 𝑃 = 𝑐 0 + 𝑐 1 𝛼 1 + • • • + 𝑐 𝑛−1 𝛼 𝑛−1 where 𝑐 𝑖 ∈ F 𝑝 , then the element 𝑃 is represented by the literal ff𝑐 0 .𝑐 1 .• • • .𝑐 𝑛−1

where all 𝑐 𝑖 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 − 𝛼 2 . This further ensures that elements in F 𝑝 ⊆ F 𝑝 𝑛 have the same literal representation in both (_ FiniteField 𝑝) and (_ FiniteField 𝑝 𝑛). A (polynomial) literal of (_ FiniteField 𝑝 𝑛) is normalized when all integer coefficients are normalized with regard to 𝑝 and all tailing zeros are omitted. Specifying a literal with more than 𝑛 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 F 3 2 , for example ff-1.1, ff0.1, and ff-1.-1 representing the elements 𝛼 − 1, 𝛼, and −𝛼 − 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 three ways of specifying the sort of a finite field literal. (i) By indexing the literal (_ ff. . . 𝑝) and (_ ff. . . 𝑝 𝑛) with the finite field order 𝑝 and 𝑝 𝑛 , respectively. This allows the literal's sort to be derived, as the order of the finite field specifies the sort uniquely. (ii) Similar to the theory of bit-vectors, there is a shorthand to avoid the _ keyword and specify the sort as part of the literal symbol. This is done by appending the literal with m𝑝 and m𝑝p𝑛 for prime field sort of order 𝑝 and extension field sort of order 𝑝 𝑛 , respectively. 6 (iii) Since 𝑝 might be a large number, a short-cut is provided by (as ff. . . 𝑆) where 𝑆 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 three variants. When printing finite field elements, solvers are free to choose between the first two notations.

Example 7. The expressions (_ ff1 5) and (_ ff1 3 2) denote the multiplicative identity (one) of F 5 and F 3 2 , respectively. In the shorthand notation, the same literals can be written as ff1m5 and ff1m3p2. Using the defined sorts from Example 4, (as ff1 FF5) and (as ff1 FF9) can be used alternatively.

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 𝑆, i.e. all parameters have sort 𝑆 and an element of 𝑆 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. 7(ff.add (_ FiniteField 𝑝)

(_ FiniteField 𝑝) (_ FiniteField 𝑝) :left-assoc) (ff.sub (_ FiniteField 𝑝) (_ FiniteField 𝑝) (_ FiniteField 𝑝)) (ff.mul (_ FiniteField 𝑝) (_ FiniteField 𝑝) (_ FiniteField 𝑝) :left-assoc) (ff.div (_ FiniteField 𝑝) (_ FiniteField 𝑝) (_ FiniteField 𝑝))

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. 8Unary arithmetic. For each finite field sort, there are the following unary operations:

(ff.neg (_ FiniteField 𝑝) (_ FiniteField 𝑝)) (ff.recip (_ FiniteField 𝑝) (_ FiniteField 𝑝))

Here, ff.neg returns the unary negation (usually written as −𝑥 for an element 𝑥), i.e. the inverse element with regard to addition. The operation ff.recip returns the reciprocal value (usually written as 𝑥 −1 for an element 𝑥), i.e. the inverse element with regard to multiplication. Note that ff.recip has total semantics but is unspecified for the zero element.

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 𝑧 = (ff.recip 𝑥) by the following (reciprocal-free) formula:

[(𝑥 ̸ = 0) ∧ (𝑥𝑧 = 1)] ∨ [(𝑥 = 0) ∧ (𝑧 = 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 (𝑧𝑧𝑥 = 𝑧) ∧ (𝑧𝑥𝑥 = 𝑥).

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.

Comparison

Since finite fields are not ordered, the theory of finite fields only supports the equality predicate: Then add some assertions: This encodes the constraint system in F 5 :

(= (_ FiniteField 𝑝) (_ FiniteField 𝑝)) (= (_ FiniteField 𝑝 𝑛) (_ FiniteField 𝑝 𝑛))𝑥 1 𝑥 2 = 𝑥 1 + 𝑥 2 𝑥 −1 1 = 𝑥 0 𝑥 2 − 𝑥 0 = 1

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(𝒯 ) 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].

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 F 2 𝑛 , 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 F 𝑝 arithmetic on a 𝑏-bit CPU, where 2 𝑏 ≪ 𝑝. Such an implementation is defined by bit-vector arithmetic, but the specification is an equation in F 𝑝 . Thus, giving a natural statement of the implementation's correctness requires operations to convert between F 𝑝 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 F 𝑝 𝑛 and some extension F (𝑝 𝑛 ) 𝑒 of it (for 𝑒 > 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.