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 knowledgeSMTverificationfinite 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
Creative Commons Attribution
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}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.