Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Extended Version)

TL;DR

This work addresses the usability gap in Synthetic Separation Logic (SSL) by lifting the abstraction level through Pika, a high-level language for algebraic data types and layout polymorphism that translates into SSL specifications for SuSLik. By decoupling data-structure layout from the specification logic and enabling higher-order specifications, Pika enables reusable, memory-layout-agnostic synthesis with in-place memory updates and full proofs of correctness. The authors formalize the semantics (via an abstract machine and SSL translation), prove soundness of the translation, and extend SuSLik to support function predicates, temporary locations, and read-only memory in order to realize the high-level specifications in C code that is competitive with, and sometimes faster than, Haskell-compiled equivalents. Their evaluation demonstrates improved expressiveness and practical viability, suggesting significant gains in safety, readability, and reuse for heap-manipulating programs. The approach has potential impact on certified synthesis pipelines by enabling higher-level reasoning about ADTs and layouts while preserving formal guarantees.

Abstract

Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that manipulate Heap-based linked data structures. Despite its expressivity, SSL suffers from two shortcomings that hinder its utility. First, its main specification component, inductive predicates, only admits first-order definitions of data structure shapes, which leads to the proliferation of ''boiler-plate'' predicates for specifying common patterns. Second, SSL requires concrete definitions of data structures to synthesise programs that manipulate them, which results in the need to change a specification for a synthesis task every time changes are introduced into the layout of the involved structures. We propose to significantly lift the level of abstraction used in writing Separation Logic specifications for synthesis -- both simplifying the approach and making the specifications more usable and easy to read and follow. We avoid the need to repetitively re-state low-level representation details throughout the specifications -- allowing the reuse of different implementations of the same data structure by abstracting away the details of a specific layout used in memory. Our novel high-level front-end language called Pika significantly improves the expressiveness of SuSLik. We implemented a layout-agnostic synthesiser from Pika to SuSLik enabling push-button synthesis of C programs with in-place memory updates, along with the accompanying full proofs that they meet Separation Logic-style specifications, from high-level specifications that resemble ordinary functional programs. Our experiments show that our tool can produce C code that is comparable in its performance characteristics and is sometimes faster than Haskell.

Figures (16)

• Figure 1: Pika translation pipeline
• Figure 2: Syntax of Synthetic Separation Logic
• Figure 3: algebraic data type together with its singly-linked list layout
• Figure 4: Specifying a function that adds one to each element of a singly-linked list in SuSLik.
• Figure 5: SuSLik specification of , excluding which is given in \ref{['fig:List-def']}

Theorems & Definitions (7)

• Lemma 1: $\mathcal{T}\llbracket\cdot\rrbracket_{}$ function
• Lemma 2: $\textnormal{cond}$ function
• Theorem 3: Soundness
• Theorem 4: Application soundness
• Definition 5: Function Predicates
• Lemma 6: $\otimes$ pairing
• Theorem 6: Soundness