Proposal: A Standard for the Theory of Finite Fields

[alex-ozdemir]

Hi SMT community,

Thomas Hader and I have been developing SMT solvers that support a theory of finite fields. We've been ensuring compatibility between our solvers by agreeing upon a bespoke SMT-LIB interface for this theory. We think it is time to standardize that interface.

Below, we have attached a PDF with our proposal. We have presented our proposal at the SMT workshop and shared it with the SMT-LIB coordinators. Now, we are seeking broader community feedback.

If this theory interests you, please consider our proposal and let us know what you think. Comments and questions are both welcome. We encourage you to reply with your comments before October 31st.

Cheers,
Alex Ozdemir

Changes since the SMT workshop presentation.

• We have removed the `#f` shorthand notation for literals, because it served the same purpose as the indexed literal notation.

smtlib-ff-proposal.pdf

[Gbury]

Apologies for the delay, here are some remarks I have.

First, I think the proposal is very nice and well-put together, and I'd like to thank you for all of the hard work you put into presenting this as clearly as possible. I only have two questions: one about the order of theories in logics, and one about the literal notation using the as syntax.

Order of theories in Logics

The proposal includes a new theory, called FFA, which obviously can be used when setting the logic for a problem.

For all of the currently accepted logics, although I don't believe it to be specified, there is an order in which theories appear: for instance, we have QF_ALIA (for a quantifier-free logic with arrays and linear integer arithmetic), but I've never seen it being written QF_LIAA (with the A of the Arrays theory after the LIA), and correspondingly, neither cvc5, z3, nor Dolmen accepts it as a logic. So that means that there is a defacto order in which theories should appear in a logic name.

Here is the order that Dolmen currently accepts (these are the comments from the code that is used to parse logic names : https://github.com/Gbury/dolmen/blob/ec32e34a95d21f71b985dc747507ff9db0db32da/src/typecheck/logic.ml#L119-L224 ):

(* Entry-point for a best effort at parsing a logic name into a
       structured representation of what theories the logic includes and
       what restrictions it imposes. *)
(* The 'ALL' logic is described in the SMT-LIB language standard as
       a logic including all that is supported by the solver. *)
(* The QF theory can only appear as a prefix "QF_" *)
(* The Array theory is specified first after an optional QF_, and
       can be one of two forms:
       - either 'A' followed by some other theories
       - either 'AX' followed by no theory *)
(* The UF theory can be specified after the array theory *)
(* After the QF, Array and UF theories have been specified,
       BV can be specified *)
(* DT and FP do not have clear ordering, so we allow to specify them in
       any order. *)
(* String theory *)
(* Arithmetic (e.g. LIA/NIRA/IDL/etc... ) *)

In that context, where in that order would FFA be inserted ? Or would it be mutually exclusive with other theories ?

Use of qualified identifier (i.e. as) in literals

The proposal includes two ways to write literals for finite fields: (_ ffN p) and (as ffN (_ FiniteField p)) (and similar for extensions fields), and I'm not fond of the second notation, using as.

Firstly, just to be sure, I suppose that only the very precise syntax show allows the use of ffN as a literal, as opposed to any situation where type inference would be enough to deduce the type of ffN ? So for instance the following example would be rejected, even though the fact that ffN is passed as argument to p basically carries the same information as an as type annotation would:

(declare-fun p ((_ FiniteField p) Bool)
(assert (p ffN))

My objection (or rather personal preference for another solution ?) would be on the basis of regularity: the proposal adds a new edge case to the semantics of as which now becomes: 1) if it is used on a term of the form ffN, then interpret it as the literal of the given type, and 2) if it's not, then one can treat it as a type annotation. It's not impossible (or even hard) to implement, it's just less regular / the semantics/behavior of as becomes more complex (just as the semantics of 'function application' and _ becomes a lot more complex with the arrival of Higher order maps). It then becomes harder to reason about such operators, because you have to consider the cartesian product with edge cases that arise in other situations (if only to check that the edge cases do not interfere with one another).

In any case, I wonder whether the following could be a reasonable alternative way to specify finite fields literals:

• have a family of functions (_ ff p), which would take a single integer argument and return the corresponding normalized element of (_ FiniteField p), and the corresponding functions (_ ff p n) which would take n arguments
• that way, parsers/typechckers/solvers do not need to parse the literal name to extract the coeficients, they are directly accessible as arguments
• if one wants to avoid repeating a very large p, then one can simply define-fun to define a wrapper
• it's unclear whether this solution allows for the "implicit trailing zeros" part of the literal spec, but I don't know how important it really is ?
• it does introduce some kind of conversion from integers to finite fields elements, but it's probably not that problematic, since solvers can simply not do too much reasoning on applications of these "literal" functions on non-literals integers ?