CRII: SHF: Bespoke Data Representation Synthesis via Contextual Data Refinement

Purdue University, West Lafayette IN

Investigators

Abstract

Nearly every modern programming language provides some mechanism for hiding the implementation details of reusable components behind some abstract interface. This interface acts as a contract, enforced by the language, that benefits both the developers and clients of such components: protecting the developers? design decisions from clients and enabling clients to safely swap in different implementations of the same interface. Recent advances in program synthesis have shown how custom implementations can be automatically built from high-level specifications of a client?s requirements, exploiting this contract to ensure that synthesized components satisfy the desired requirements. Existing approaches to language-enforced abstraction approaches can be too restrictive in this setting, however, as they require the synthesized implementation to work for any client. This disallows any implementations whose correctness are dependent on a particular client?s usage. The goal of this project is to relax this condition, enabling the synthesis of custom implementations that are tailored to a particular client while still providing the same strong abstraction guarantees that programmers expect from their programming languages. The intellectual merits are the development of a refined notion of modularity in programming languages, advancing the state of the art in the synthesis of correct, performant code. The project's broader significance and importance are the development of an approach that allows programmers to program against high-level abstractions without paying a performance penalty. The project advances the state of the art in both the theoretical foundations of data abstraction and the development of verified software. The vehicle for the work's theoretical contributions is a formalization of a core calculus for data refinement. This calculus is used to reformulate the well-established notion of data refinement for abstract data types (ADTs) to incorporate information about a specific client's usage of an interface. A key component is the development of the metatheory proofs establishing that the standard property of representation independence under data refinement is preserved. This approach is used to improve the existing Fiat deductive synthesis framework, enabling clients to derive verified ADT implementations that are tailored to their particular usage. The augmented system is evaluated via the synthesis of custom implementations of the popular Haskell bytestring library for two open-source Haskell programs, using an existing derivation of a performant bytestring implementation in Fiat as a starting point. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.