An SMT-LIB Theory of Finite Fields
Thomas Hader, Alex Ozdemir
TL;DR
This work introduces an SMT-LIB theory for finite-field arithmetic (FFA) to enable interoperable, solver-agnostic reasoning about finite fields in SMT-based verification. It defines two finite-field sorts (prime and extension), canonical element domains via signed representatives for primes and Conway-polynomial-based polynomials for extensions, and a full set of operations and literals (ff.add, ff.mul, ff.div, ff.recip, etc.) with totalized division-by-zero semantics. The approach ensures normalized model reporting and precise well-sortedness, aiming to standardize how finite-field reasoning is encoded across tools such as Yices and cvc5. By providing a standardized theory, the paper facilitates verification tasks in cryptography, ZKPs, and secure computation that rely on finite-field arithmetic, and it outlines practical directions for conversions and variable field sizes to broaden applicability.
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.