Verifying Solutions to Semantics-Guided Synthesis Problems

Semantics-Guided Synthesis (SemGuS) provides a framework to specify synthesis problems in a solver-agnostic and domain-agnostic way, by allowing a user to provide both the syntax and semantics of the language in which the desired program should be synthesized. Because synthesis and verification are closely intertwined, the SemGuS framework raises the following question: how does one verify that a user-given program satisfies a given specification when interpreted according to a user-given semantics? In this paper, we prove that this form of language-agnostic verification (specifically that verifying whether a program is a valid solution to a SemGuS problem) can be reduced to proving validity of a query in the 𝜇CLP calculus, a fixed-point logic that is capable of expressing alternating least and greatest fixed-points. Our encoding into 𝜇CLP allows us to further classify the SemGuS verification problems into ones that are reducible to satisfiability of ( i ) first-order-logic formulas, ( ii ) Constrained Horn Clauses, and ( iii ) 𝜇CLP queries. Furthermore, our encoding shines light on some limitations of the SemGuS framework, such as its inability to model nondeterminism and reactive synthesis. We thus propose a modification to SemGuS that makes it more expressive, and for which verifying solutions is exactly equivalent to proving validity of a query in the 𝜇CLP calculus. Our implementation of SemGuS verifiers based on the above encoding can verify instances that were not even encodable in previous work. Furthermore, we use our SemGuS verifiers within an enumeration-based SemGuS solver to correctly synthesize solutions to SemGuS problems that no previous SemGuS synthesizer could solve.