Repo for ADT Synthesis work, to eventually be integrated into github
Coq TeX OCaml Makefile Python Shell
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Overview
etc
examples
src
.dir-locals.el
.gitattributes
.gitignore
.gitmodules
Makefile
README
TODO
autogen.sh
tarball.sh
todos.sh

README

Fiat − Deductive Synthesis of Abstract Data Types in a Proof Assistant
======================================================================

This repository holds the source code of Fiat, a Coq ADT synthesis
library.

## Dependencies:
  * To build the library:          Coq 8.4pl2
  * To step through the examples:  GNU Emacs 23.4.1, Proof General 4.3
  * To extract and run OCaml code: OCaml 3.12.1

## Compiling and running the code
  * To build the library: `make sources`
  * To build the examples: `make examples`
  * To extract the bookstore example to OCaml: `make repl`

## Where to start
  The `examples` folder contains three interesting database refinements:

  * `Bookstore.v` contains a fully automated refinement of the bookstore
     example presented throughout the paper.
  * `Stocks.v` and `Weather.v` contain two additional automated examples,
     with more complex indexing schemes, and more diverse aggregation
     operators.

  Stepping through these files in emacs requires that the sources be
  built, using `make sources`.

  The best way to get a feeling of how the library works, and what the
  query planner does under the hood, is to step through the bookstore
  semi-automated refinement found in `examples/BookstoreSemiAutomatic.v`,
  which shares the preamble of `Bookstore.v`, but shows a more
  progressive derivation. Finally, the query planner code can be found
  in `src/QueryStructure/Refinements/AutoDB.v`.

  The examples/CacheADT directory also includes the derivation of an abstract
  data type implementing a Least Recently Used cache, as discussed in Section
  3.1 of the paper. 
  

## Extracting and running the code
  Running `make repl` 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 100000

## Further exploring the code base

### Top-level directory organization

1. `src` - Source files for the ADT synthesis library
2. `examples` - Example ADT derivations using the library

### Detailed sub-directory organization:

#### src/Computation

Definitions of computations and refinement that form the core of ADT
refinement.

  * Core.v: core definitions of computation and refinement
  * Monad.v: proofs that computations satisfy the monad laws
  * SetoidMorphisms.v: setoid rewriting machinery support for refinement
  * ReflectiveMonad.v: reflective tactic for simplifying using the monad laws
  * ApplyMonad.v: applicative tactic for simplifying using the monad laws
  * Refinements/General.v: core set of refinement facts used for synthesis

#### src/ADT/

Definition of abstract data types (ADTs).

  * ADTSig.d: definition of ADT interfaces (signatures)
  * Core.v: core definitions of ADT
  * ADTHide.v: definitions for hiding part of an ADT interface

#### ADTNotation/

More pleasant notations for ADTs.

  * ilist.v: definitions of the indexed lists used in ADT notations
  * StringBound.v: typeclass definition of the bounded strings our
                   notations use for method indices
  * BuildADTSig.v: notation for ADT signatures
  * BuildADT.v: notation for ADT definitions
  * BuildADTReplaceMethods.v: functions for notation-friendly method
                              replacement

#### ADTRefinement/

Definitions of and machinery for refining ADTs from specification
to implementation.

  * Core.v: definition of ADT refinement
  * SetoidMorphisms.v: setoid rewriting machinery for ADT refinement
  * GeneralRefinements.v: core tactics for a 'single step' of ADT
    refinement through either method or constructor refinement
  * BuildADTSetoidMorphims.v: Notation-friendly proofs of switching
    representation and method refinement
  * GeneralBuildADTRefinements.v: Notation-friendly tactics for refining
    a single ADT method or constructor

#### ADTRefinement/Refinements/

Definitions and tactics for more specialized refinements.

  * HoneRepresentation.v: switching the representation type of an ADT
  * SimplifyRep.v: simplifying the representation type of an ADT
  * RefineHideADT.v: refining ADTs with interfaces hidden using the
    definitions in ADTHide.v
  * ADTCache.v: adding a cached value to the representation of an ADT
  * ADTRepInv.v: refining an ADT under a representation invariant
  * DelegateMethods.v: delegating functionality to another ADT

#### ADTRefinement/BuildADTRefinements/

Definitions and tactics for notation-friendly versions of some of the
specialized refinements in ADTRefinement/Refinements

#### 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 constraints
  * QueryStructure.v: definitions for reference representation of ADTs
    with SQL-like operations

#### QueryStructure/QuerySpecs

Definitions and notations for specifying SQL-like operations on QueryStructures

  * EmptyQSSpecs.v: empty QueryStructure constructor
  * InsertQSSpecs.v: QueryStructure insertion operation + basic refinement for
                     for performing data-integrity checks
  * QueryQSSpecs.v: query operations for QueryStructures

#### QueryStructure/Refinements

Implementations of QueryStructures

  * ListImplementation: list-based representation
  * FMapImplementation: extra lemmas about Coq's Fmaps
  * Bags: Implementations of the Bag interface described in the paper:
    * ListBags.v: List-based bag implementation
    * TreeBags.v: FMap-based bag implementation
    * CachingBags.v: Bags augmenting existing bags with a caching layer
    * CountingBags: Specific kind of ListBags keeping track of their
                    number of elements
    * BagsOfTuples.v: Nested TreeBags containing tuples