Satisfiability Modulo Finite Fields

Alex Ozdemir; Gereon Kremer; Cesare Tinelli; Clark Barrett

Paper 2023/091

Satisfiability Modulo Finite Fields

Alex Ozdemir, Stanford University

Gereon Kremer, Stanford University, Certora

Cesare Tinelli, University of Iowa

Clark Barrett, Stanford University

Abstract

We study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we con- struct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evalu- ate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors).

Note: June '24: fixed two typos in the algebraic background Aug '24: acknowledge CBR

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. Major revision. CAV'23
Keywords: zero knowledge SMT verification finite fields
Contact author(s): aozdemir @ cs stanford edu
History: 2024-08-26: last of 3 revisions; 2023-01-25: received; See all versions
Short URL: https://ia.cr/2023/091
License: CC BY

BibTeX

@misc{cryptoeprint:2023/091,
      author = {Alex Ozdemir and Gereon Kremer and Cesare Tinelli and Clark Barrett},
      title = {Satisfiability Modulo Finite Fields},
      howpublished = {Cryptology {ePrint} Archive, Paper 2023/091},
      year = {2023},
      url = {https://eprint.iacr.org/2023/091}
}