SMT Solving for Finite Field

Overview

Finite field arithmetic is fundamental to many cryptographic protocols.

Theory Reference: Finite Fields

Note

Currently, only finite fields of prime order p are supported.

Such a field is isomorphic to the integers modulo p.

We interpret field sorts as prime fields and field terms as integers modulo \(p\). In the following, let:

  • N be an integer numeral and \(N\) be its integer

  • p be a prime numeral and \(p\) be its prime

  • F be an SMT field sort (of order \(p\))

  • x and y be SMT field terms (of the same sort F) with interpretations \(x\) and \(y\)

SMT construct

Semantics

Notes

(_ FiniteField p)

the field of order \(p\)

represented as the integers modulo \(p\)

(as ffN F)

the integer \((N \bmod p)\)

(ff.add x y)

the integer \(((x + y) \bmod p)\)

NB: ff.add is an n-ary operator

(ff.mul x y)

the integer \(((x \times y) \bmod p)\)

NB: ff.mul is an n-ary operator

(= x y)

the Boolean \(x = y\)

 
(set-logic QF_FF)
(set-info :status unsat)
(define-sort F () (_ FiniteField 3))
(declare-const x F)
(assert (= (ff.mul x x) (as ff-1 F)))
(check-sat)
; unsat

(set-logic QF_FF)
(set-info :status sat)
(define-sort F () (_ FiniteField 3))
(declare-const x F)
(assert (= (ff.mul x x) (as ff0 F)))
(check-sat)
; sat: (= x (as ff0 F)) is the only model

Experimental features (may be removed in the future):

  • ff.bitsum: n-ary operator for bitsums: (ff.bitsum x0 x1 x2) = \(x_0 + 2x_1 + 4x_2\)

  • ff.neg: unary negation

Implementation

Aria provides SMT solving over finite fields in the aria/smt/ff module with multiple encoding strategies:

  • Bit-vector encoding (ff_bv_solver.py): Encodes field elements as bit-vectors (width log₂(field_size)) with modular constraints

  • Integer encoding (ff_int_solver.py): Encodes field elements as integers in [0, field_size-1] with explicit modulo operations

  • Performance encoding (ff_perf_solver.py): Integer encoding with adaptive reduction scheduling, structured-prime modular kernels, and partition-driven CEGAR refinement

The automatic solver (FFAutoSolver) can route large-prime instances to the performance backend and still fall back to the stable integer backend when a recovery run is required.

The performance backend supports environment controls:

  • ARIA_FF_SCHEDULE = eager | balanced | lazy | strict-recovery

  • ARIA_FF_KERNEL_MODE = auto | generic | structured

  • ARIA_FF_MAX_NONLINEAR_EQS

  • ARIA_FF_MAX_NONLINEAR_VARS

  • ARIA_FF_MAX_NONLINEAR_MODULUS

  • ARIA_FF_MAX_NONLINEAR_SEARCH_SPACE

  • ARIA_FF_MAX_NONLINEAR_WORK_BUDGET

  • ARIA_FF_ROOTSET_BUDGET

Automatic backend selection can be configured through FFAutoSolver:

  • enable_perf_backend (default True)

  • perf_policy in auto, always, never, large-prime

Core components include formula parsing (ff_parser.py), sparse polynomial normalization/partitioning, and translation to bit-vector or integer arithmetic.

The performance backend exposes two experiment-facing interfaces:

  • stats(): counters for reductions, cuts, learned lemmas, partition selection, and bounded local algebra

  • trace(): a per-round JSON-friendly refinement trace

Usage Example

from aria.smt.ff import FFAutoSolver, FFPerfSolver, parse_ff_file

formula = parse_ff_file("benchmarks/smtlib2/ff/simple.smt2")

auto = FFAutoSolver()
print(auto.check(formula), auto.backend_name)

perf = FFPerfSolver(schedule="balanced", kernel_mode="auto", recovery=True)
print(perf.check(formula))
print(perf.stats())
print(perf.trace())

python3 scripts/run_ff_perf_bench.py \
  --bench-dir benchmarks/smtlib2/ff \
  --backends bv,bv2,int,auto,perf \
  --timeouts 10,30,60 \
  --repetitions 3 \
  --out results/ff_perf_bench.json

References

  • Hader, T., Kaufmann, D., Irfan, A., Graham-Lengrand, S., & Kovács, L. (2024).

    MCSat-based Finite Field Reasoning in the Yices2 SMT Solver. ArXiv:2402.17927.

  • Ozdemir, A., Pailoor, S., Bassa, A., Ferles, K., Barrett, C., & Dillig, I. (2024).

    Split Gröbner Bases for Satisfiability Modulo Finite Fields. In Computer Aided Verification (CAV).

  • Ozdemir, A., Kremer, G., Tinelli, C., & Barrett, C. (2023).

    Satisfiability modulo finite fields. In Computer Aided Verification (CAV).

  • Hader, T., Kaufmann, D., & Kovács, L. (2023). SMT solving over finite field arithmetic. In LPAR.

  • Hader, T. (2022). Non-linear SMT-reasoning over finite fields. Master’s thesis, TU Wien.

  • Hader, T., & Kovács, L. (2022). Non-linear SMT-reasoning over finite fields. In SMT Workshop.