An SMT-LIB Theory of Finite Fields

TL;DR

This paper introduces a standardized SMT-LIB theory for finite field arithmetic, facilitating interoperability and supporting recent advances in SMT solving and software verification involving finite fields.

Contribution

It defines a canonical representation and operations for finite fields within the SMT-LIB framework, enabling consistent and interoperable reasoning.

Findings

Defines a canonical representation of finite field elements

Provides formal definitions of operations and predicates

Supports interoperability in SMT solving ecosystems

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.