Structuring the verification of heap-manipulating programs
==========================================================

This directory contains the Coq files associated with the paper
"Structuring the verification of heap-manipulating programs" by Aleks
Nanevski, Viktor Vafeiadis and Josh Berdine.

The files develop a set of libraries for program verification in a
higher-order variant of Separation Logic.

Concrete examples include verification of stack, queue, array and
hash-table libraries, and a verification of the Fast Congruence
Closure algorithm of Nieuwenhuis and Oliveras, described in the
following paper.

   Fast Congruence Closure and Extensions
   Information and Computation, 205(4):557-580, April 2007, Elsevier Science
   http://www.lsi.upc.es/~roberto/papers/IC06.pdf

The developments require the Ssreflect-1.1 extension of Coq V8.1, patch
level >= 3, or Ssreflect-1.2 extension of Coq V8.2. 

The developments have originally been carried out in Coq V8.1, and
then ported to V8.2. We include a copy of our files for both of these
versions, for comparison purposes.


Obtaining and installing SSreflect
==================================

To install Ssreflect, download the sources at 

   http://www.msr-inria.inria.fr/Projects/math-components

unpack, and follow the instructions in the INSTALL and README files.

Compiling separation logic libraries and examples
=================================================

After installing ssreflect, simply go into the directory containing
our distribution, and type

  cd v8.1 (or cd v8.2, depending on your version of Coq)
  coq_makefile -f Make -o Makefile
  make

Description of our files 
=========================

 1. Make (the generator for the Makefile)

 3. Ssreflect files and libraries required for compiling our development:

    ssreflect.v
    ssrfun.v
    ssrbool.v
    eqtype.v
    ssrnat.v
    seq.v
    paths.v
    div.v
    fintype.v 
    tuple.v 
    finfun.v 
    ssralg.v 
    bigops.v 
    finset.v

    In case of Ssreflect-1.2/Coq V8.2, there is an addition file choice.v.

    choice.v

 4. ordtype.v 

    Library for types with a decidable ordering relation on them.

 5. fmap.v 

    Library for purely functional finite maps, i.e., partial functions
    from keys to values which are defined for only finitely many keys.

 6. rels.v 

    Library for relations over arbitrary type.

 7. heaps.v 

    Main definitions and lemmas related to the datatype of heaps.
    This file is summarized in Section 2 of the paper.

 8. hprop.v 

    Definitions and lemmas about separation logic predicates, i.e.,
    predicates over heaps.

 9. stmodel.v 

    Definitions and proofs of a simple predicate transformer model of
    side-effectful commands. This model is summarized in a part of
    Section 3 of the paper.

10. stsep.v

    Definitions and proofs related to the structural rules of
    separation logic, as described in Section 3 of the paper.

11. vcgen.v

    New structural rules used to encode a particular verification
    strategy, as described in Section 4 of the paper.

12. stlc.v 

    A typechecker for a simply-typed lambda-calculus. Shows how to
    specify and verify HTT programs that may raise exceptions.

13. llist.v

    Library for singly-linked lists.

14. stack.v 

    Library of stacks, implemented as singly-linked lists.

15. queue.v 

    Library of queues, implemented as singly-linked lists.

16. array.v 

    Library of arrays, implemented as a finite, contiguous, set of
    heap locations. Arrays are specified using finite functions, as
    implemented in the file finfun.v of Ssreflect.

17. kvmaps.v 

    Specification of imperative key-value maps (i.e., finite maps) and
    a simple implementation in terms of a pointer to a functional
    implementation from fmap.v

18. hashtab.v 
 
    Functor for hash tables, parametrized in the implementation of
    buckets.

19. congrmath.v 

    Development of the mathematical model required for specification
    of the fast congruence closure algorithm. In Section 5 of the
    paper, this is referred to as the second phase of the verification
    of the congruence closure algorithm.

20. congrprog.v

    Implementation and verification of the fast congruence closure
    algorithm. In Section 5 of the paper, this is referred to as the
    first phase of the verification of the congruence closure
    algorithm.






