Fiat refines declarative specifications into functional programs that can be run with good performance, and it all happens inside Coq without modifications. Our artifact includes three examples utilizing a library for specifying ADTs with SQL-like operations and automatically deriving implementations using tactics. It also includes the manual derivation of an implementation of one such ADT that automatically caches queries.
Thanks for evaluating this artifact! Here is how to get started:
Download the paper.
Download the artifact: Source code tarball (~ 130kB; see the dependencies section below)
Compile the source code
$ make sources
Start exploring the examples!
The best way to get a feeling of how the library works is to step through the semi-automated refinement of the bookstore example from the paper found in examples/BookstoreSemiAutomatic.v.
The examples folder contains three further fully-automated example refinements of ADTs with SQL-like operations:
Bookstore.v uses the same specification as BookstoreSemiAutomatic.v, but uses the plan tactic found in src/QueryStructure/Refinements/AutoDB.v to automatically derive an implementation.
Stocks.v and Weather.v contain the two additional examples from Section 5.2 of the paper, featuring more complex indexing schemes, and more diverse aggregation operators.
CacheADT/LRUCache.v demonstrates the manual derivation of the least recently used cache discussed in Section 3.1 of the paper.
BookstoreCache.v utilizes the LRUCache derived in CacheADT/LRUCache.v to build the version of the bookstore example from Section 4.7 which caches queries using finite differencing.
Coq 8.4pl2GNU Emacs 23.4.1, Proof General 4.3OCaml 3.12.1make sourcesmake repl (rather slow)make examples (slow; not required to step through the examples in emacs!). Note that compiling all examples requires a significant amount of memory (> 2GB).Running make repl extracts the bookstore example code and produces a repl binary in the examples/ directory, which supports the following commands:
reset
add_book [author title isbn]
place_order [isbn]
get_titles [author]
num_orders [author]
benchmark [nb_authors nb_books nb_orders nb_titles_queries nb_orders_queries]To replicate the results highlighted in the paper, run examples/repl, and type
benchmark 1000 10000 100000 100000 100000src - Source files for the ADT synthesis libraryexamples - Example ADT derivations using the librarysrc/ComputationDefinitions of computations and refinement that form the core of ADT refinement.
Core.v: core definitions of computation and refinementMonad.v: proofs that computations satisfy the monad lawsSetoidMorphisms.v: setoid rewriting machinery support for refinementReflectiveMonad.v: reflective tactic for simplifying using the monad lawsApplyMonad.v: applicative tactic for simplifying using the monad lawsRefinements/General.v: core set of refinement facts used for synthesissrc/ADT/Definition of abstract data types (ADTs).
ADTSig.d: definition of ADT interfaces (signatures)Core.v: core definitions of ADTADTHide.v: definitions for hiding part of an ADT interfacesrc/ADTNotation/More pleasant notations for ADTs.
ilist.v: definitions of the indexed lists used in ADT notationsStringBound.v: typeclass definition of the bounded strings our notations use for method indicesBuildADTSig.v: notation for ADT signaturesBuildADT.v: notation for ADT definitionsBuildADTReplaceMethods.v: functions for notation-friendly method replacementsrc/ADTRefinement/Definitions of and machinery for refining ADTs from specification to implementation.
Core.v: definition of ADT refinementSetoidMorphisms.v: setoid rewriting machinery for ADT refinementGeneralRefinements.v: core tactics for a 'single step' of ADT refinement through either method or constructor refinementBuildADTSetoidMorphims.v: Notation-friendly proofs of switching representation and method refinementGeneralBuildADTRefinements.v: Notation-friendly tactics for refining a single ADT method or constructorsrc/ADTRefinement/Refinements/Definitions and tactics for more specialized refinements.
HoneRepresentation.v: switching the representation type of an ADTSimplifyRep.v: simplifying the representation type of an ADTRefineHideADT.v: refining ADTs with interfaces hidden using the definitions in ADTHide.vADTCache.v: adding a cached value to the representation of an ADTADTRepInv.v: refining an ADT under a representation invariantDelegateMethods.v: delegating functionality to another ADTsrc/ADTRefinement/BuildADTRefinements/Definitions and tactics for notation-friendly versions of some of the specialized refinements in ADTRefinement/Refinements
src/QueryStructure/Library for specifying and refining ADTs with SQL-like operations
Heading.v: definitions of signatures for labeled data (headings)Tuple.v: definitions for labeled data (tuples)Schema.v: definitions for specifying sets of tuples with data-integrity constraints (relation schema)Relation.v: definitions for sets of tuples (relations)QueryStructureSchema.v: definitions for specifying sets of relations with cross-relation data-integrity constraintsQueryStructure.v: definitions for reference representation of ADTs with SQL-like operationssrc/QueryStructure/QuerySpecsDefinitions and notations for specifying SQL-like operations on QueryStructures
EmptyQSSpecs.v: empty QueryStructure constructorInsertQSSpecs.v: QueryStructure insertion operation + basic refinement for for performing data-integrity checksQueryQSSpecs.v: query operations for QueryStructuressrc/QueryStructure/RefinementsImplementations of QueryStructures
ListImplementation: list-based representationFMapImplementation: extra lemmas about Coq's FmapsBags: Implementations of the Bag interface described in the paper:ListBags.v: List-based bag implementationTreeBags.v: FMap-based bag implementationCachingBags.v: Bags augmenting existing bags with a caching layerCountingBags: Specific kind of ListBags keeping track of their number of elementsBagsOfTuples.v: Nested TreeBags containing tuples