Program synthesis via refinement is a venerable approach for gradually transforming specifications into executable code, generating a proof trail showing that the final efficient program adheres to the specification.
We present the first automated, proof-generating refinement system that invents new data structures to suit the needs of a program, applying global program analysis to understand those needs.
Our system, based on the Fiat library for the Coq proof assistant, is extensible not just with new data structures but also with new rules for inventing more complex data structures by combining simpler ones.
All data-structure operations come with semantic interfaces capturing their behavior in terms of abstract mathematical objects such as sets, and the system soundly and automatically tiles the specification with those operations to generate an OCaml-style program and a proof of its correctness.
Starting from a high-level specification in extensible SQL-like language using logic to describe arbitrary operations on data, without explaining how to execute them, our system automatically matches those operations to proof-generating data-structure-construction rules in our library to build an efficient, correct-by-construction implementation.