Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs

TL;DR

This paper tackles verifying properties over potentially infinite sets of programs by extending Unrealizability Logic (UL) with a weakest-precondition variant (W-UL) and a syntax-directed approach to proof construction. It decouples proof skeleton generation from the synthesis of nonterminal summaries and loop invariants, enabling automated generation of verification conditions that can be discharged via SyGuS synthesis or SMT solvers. The authors implement these ideas in Wuldo, demonstrate proof-skeleton generation, and show that reusing proven summaries across queries yields substantial speedups, while also enabling synthesis of summaries in some cases. The work advances scalable, interpretable verification and pruning for enumerative synthesis and dynamic/foreign-code verification, with evidence from comprehensive benchmarks and thoughtful analysis of limitations and future directions.

Abstract

Automated verification of all members of a (potentially infinite) set of programs has the potential to be useful in program synthesis, as well as in verification of dynamically loaded code, concurrent code, and language properties. Existing techniques for verification of sets of programs are limited in scope and unable to create or use interpretable or reusable information about sets of programs. The consequence is that one cannot learn anything from one verification problem that can be used in another. Unrealizability Logic (UL), proposed by Kim et al. as the first Hoare-style proof system to prove properties over sets of programs (defined by a regular tree grammar), presents a theoretical framework that can express and use reusable insight. In particular, UL features nonterminal summaries -- inductive facts that characterize recursive nonterminals (analogous to procedure summaries in Hoare logic). In this work, we design the first UL proof synthesis algorithm, implemented as Wuldo. Specifically, we decouple the problem of deciding how to apply UL rules from the problem of synthesizing/checking nonterminal summaries by computing proof structure in a fully syntax-directed fashion. We show that Wuldo, when provided nonterminal summaries, can express and prove verification problems beyond the reach of existing tools, including establishing how infinitely many programs behave on infinitely many inputs. In some cases, Wuldo can even synthesize the necessary nonterminal summaries. Moreover, Wuldo can reuse previously proven nonterminal summaries across verification queries, making verification 1.96 times as fast as when summaries are instead proven from scratch.

Figures (6)

• Figure 1: Proof tree for Example \ref{['ex:nested_ite']} where $Q_S = \exists n. \forall i. x[i]<n$, and ${\color{noncrappyred}{\Gamma_1}} = \{{\color{noncrappyred}{\{| {x = z} |\} \: S \: \{| Q_S |\}}}\}$ is a context that contains our inductive fact about $S$ for later use. Our automation algorithms can derive all terms in black when the pre and postconditions in red---i.e., the nonterminal summaries---are provided. In some cases, even the summaries in red can be synthesized.
• Figure 2: The base grammar $\mathit{G_{imp}}$ which defines the terms over which our inference rules operate.
• Figure 3: W-UL Inference Rules. Note that the context $\Gamma$ is a collection of triples used as inductive hypotheses. In the HP rule, $N$ is a nonterminal with productions $N_1, \cdots, N_n$.
• Figure 4: Following Example \ref{['ex:full_proof_tree']}, we give a proof/proof skeleton for a triple $\{| {\mathit{true}} |\} \: N \: \{| e_t \neq 3 |\}$ where $N \mapsto 2 \mid 2 + N$. Above, $R$ is an abbreviation for $\forall e_{t_y}. ({\color{noncrappyred}{Q_N}}(e_{t_y}) \rightarrow {\color{noncrappyred}{Q_N}}(x_1 + e_{t_y}))$. When ${\color{noncrappyred}{Q_N}}(a)$ is taken to be $a = 0 \text{ (mod } 2)$, we get a valid proof tree for $\{| {\mathit{true}} |\} \: N \: \{| e_t \neq 3 |\}$. When ${\color{noncrappyred}{Q_N}}(a)$ (marked in red) is left as a parameter, we get a proof skeleton (§\ref{['sec:syn_proof_skel']}). Substitution of a second order parameter is taken to be a substitution into each of its inputs. Note, $\Gamma' = \{\{| {\mathit{true}} |\} \: N \: \{| {\color{noncrappyred}{Q_N}}(e_t) |\}\}$.
• Figure 5: Summary reuse experiments. The time to verify each template with summary verification (no_ctx) is plotted against the time to verify with pre-proven summaries (i.e., without summary verification) (ctx).

Theorems & Definitions (14)

• definition 1: Unrealizability Triple
• theorem 1: Soundness
• theorem 2: Relative Completeness for Sets of Loop-Free Programs
• Remark
• definition 2: $\boldsymbol{x}, \boldsymbol{z},$ and $\boldsymbol{y}$ for $S$
• theorem 3
• definition 3: Parametrized Verification Conditions
• definition 4: Satisfiability
• corollary 1
• definition 5: SyGuS sygus