Paper 2024/954 Original: eprint.iacr.org/2024/954 ↗

Arithmetisation of computation via polynomial semantics for first-order logic

Abstract

We propose a compositional shallow translation from an impredicative first-order logic with equality, into polynomials; that is, we give a direct, compositional, arithmetic notion of first-order logic validity. Arithmetisation means translating validity of some assertion φ of a model M , into some property Rₘ of a polynomial P (φ, M ), such that (to a high degree of certainty) φ is valid in M if and only if Rₘ holds of P (φ, M ). Arithmetisation is widely used in cryptography, because many cryptographic protocols work by exploiting properties of finite fields to prove assertions like “R holds of a polynomial P ” — a typical property R is ‘has roots in 1, . . . , kₘ’, where kₘ is determined by the cardinality of M . Meanwhile, first-order logic is a simple but expressive language for specifying and reasoning about computation. In particular, it is easily powerful enough to express inductive definitions, Turing-complete computation, and correctness properties thereof. We can think of first-order logic as a high-level, virtual-machine-independent model of reasoning and computation. Techniques already exist to arithmetise computation by coding it in an abstract machine whose computation has been arithmetised by hand; i.e. by a deep embedding in some preconstructed monolithic cryptographic artefact. What distinguishes our translation is its shallowness, compositionality, and uniform treatment of logical connectives: it translates logical connectives directly to operations on polynomials, without a deep encoding in an abstract machine. The translation is deceptively straightforward: truth maps to 0, false maps to any strictly positive number, conjunction and universal quantification map to +, and disjunction and existential quantification map to ∗. Yet, we shall see that the outcome is surprisingly powerful and expressive.