Unrealizability Logic

TL;DR

Unrealizability logic provides a Hoare-style proof system to establish that a program-synthesis problem has no solution within a given search space, even when that space is infinite. By overapproximating the execution of an entire regular-tree-grammar-defined set of programs and using vector-states to encode many input–output examples, the framework enables principled, checkable proofs of unrealizability. The authors prove soundness and relative completeness, and demonstrate how the logic handles infinite example sets, loops, and symbolic inputs, while relating to existing approaches like Nay, Nope, and SemGuS. This work lays the groundwork for automated proof-search and future realizability logic, with significant potential to prune synthesis search spaces and to illuminate why certain synthesis problems are unrealizable.

Abstract

We consider the problem of establishing that a program-synthesis problem is unrealizable (i.e., has no solution in a given search space of programs). Prior work on unrealizability has developed some automatic techniques to establish that a problem is unrealizable; however, these techniques are all black-box, meaning that they conceal the reasoning behind why a synthesis problem is unrealizable. In this paper, we present a Hoare-style reasoning system, called unrealizability logic for establishing that a program-synthesis problem is unrealizable. To the best of our knowledge, unrealizability logic is the first proof system for overapproximating the execution of an infinite set of imperative programs. The logic provides a general, logical system for building checkable proofs about unrealizability. Similar to how Hoare logic distills the fundamental concepts behind algorithms and tools to prove the correctness of programs, unrealizability logic distills into a single logical system the fundamental concepts that were hidden within prior tools capable of establishing that a program-synthesis problem is unrealizable.

Figures (7)

• Figure 1: An unrealizability triple with a negated post-vector-state asserts that a synthesis problem is unrealizable. Observe how the vectorized version of $\lnot O$ asserts that there is at least one output example that does not satisfy the desired input-output relation.
• Figure 2: Simplified proof tree that proves the sub-goal $\{| {{x} \equiv_{2} {0}} |\} \: S2 \: \{| {x} \equiv_{2} {0} |\}$ in unrealizability logic. $\Gamma_{S2}$ denotes the context $\{{\{| {{x} \equiv_{2} {0}} |\} \: S2 \: \{| {x} \equiv_{2} {0} |\}}\}$. Labels and are names for the triples they are associated with.
• Figure 3: Encoding of $sy_{\mathsf{e}}$ as a nondeterministic program.
• Figure 4: The base grammar $G_{imp}$, which defines a universe of terms that we are interested in for this paper.
• Figure 5: Inference rules for expressions in unrealizability logic. $\mathsf{Bin}$ represents rules for binary expressions, where the operator $\oplus$ is one of $+$ ($\mathsf{Plus}$), $-$ ($\mathsf{Minus}$), $\cdot$ ($\mathsf{Mult}$), or $/$ ($\mathsf{Div}$). $\mathsf{Comp}$ represents rules for binary comparators, where the operator $\odot$ is one of $<$ ($\mathsf{LT}$) or $==$ ($\mathsf{Eq}$).

Theorems & Definitions (16)

• theorem 1
• definition 1: Regular Tree Grammar
• definition 2: Synthesis Problem
• definition 3: Semantics of Expressions
• definition 4: Vector-State
• definition 5: Vector-State Semantics
• definition 6: Validity
• lemma 1
• definition 7: Derivability
• theorem 2: Soundness