Paper 2023/091 Original: eprint.iacr.org/2023/091 ↗
Satisfiability Modulo Finite Fields
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).
Metadata
- Available format(s)
PDF- Category
- Implementation
- Publication info
- Preprint.
- History
- 2024-08-26: last updated
- 2023-01-25: published
- Short URL
- https://ia.cr/2023/091
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}