VCFloat: A Unified Coq Framework for Verifying C Programs with
Floating-Point Computations

Version 1.0 (2015-12-04)

Copyright (C) 2015 Reservoir Labs Inc.
All rights reserved.

patches/interval.patch is distributed under CeCILL-C, version 1.0. All
other files of this library are distributed under the GNU General
Public License, version 3.0, or (at your option) any later
version. See LICENSE for more legal information on use and
distribution of VCFloat.


For more technical information on VCFloat, you can read Sections 1 to
4 of our paper published at ACM/SIGPLAN Certified Programs and Proofs
(CPP) 2016:

Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard
Lethin.
A Unified Coq Framework for Verifying C Programs with Floating-Point
Computations


Summary of directories (each of which corresponds to its logical path
with the same names where each path separator is replaced with . ):

  vcfloat/cverif: Verification of CompCert Clight programs (separation
  logic, etc.)

  vcfloat: VCFloat reasoning framework and tactic


Most interesting files:

  vcfloat/FPLang.v: VCFloat floating-point and annotated
  floating-point calculus

  vcfloat/FPLangOpt.v: further properties about VCFloat
     
  vcfloat/Clight2FP.v: C to unannotated VCFloat

  vcfloat/Clight2FPOpt.v: VCFloat annotation tactic

  vcfloat/Example.v: examples of Section 4 of the abovementioned CPP
  2016 paper (to be replayed interactively under ProofGeneral-Coq or
  CoqIDE)

VCFloat requires Coq 8.5beta2.


VCFloat depends on the following further external libraries, which are
automatically downloaded from their official sources and built during
VCFloat's building process:

- Reservoir Labs Inc. R-CoqLib version 1.0 (from Reservoir Labs'
  GitHub at http://github.com/reservoirlabs/rcoqlib )

- CompCert 2.4 (from AbsInt's GitHub at
  https://github.com/AbsInt/CompCert.git , commit 5dd15440). VCFloat
  contains a patch from this commit (patches/compcert.patch),
  distributed under the GNU General Public License, version 3.0 or (at
  your option) any later version.

- Ssreflect 1.5 (from its official website at
  http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.coq85beta2.tar.gz )

- Mathematical Components (MathComp) 1.5 (from its official website at
  http://ssr.msr-inria.inria.fr/FTP/mathcomp-1.5.coq85beta2.tar.gz )

- Flocq 2.4.0 (from INRIA GForge at
  https://gforge.inria.fr/git/flocq/flocq.git , commit bcbcde24)

- Coq-Interval 2.0.0 (from INRIA GForge at
  https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git
  , commit 81f1f918). VCFloat contains a patch from this commit
  (patches/interval.patch), distributed under CeCILL-C, version 1.0.

See ACKS for copyright and licensing information about those external
libraries.


Usage: assuming that you already have a standard installation of Coq
8.5beta2, GNU make, GNU autoconf, GNU automake, and git.

  0. Fetch the external libraries mentioned above, by running the
     following automatic script:

     ./get_external_libs.sh

     You can provide any further options that you want passed to the
     `make' commands for Ssreflect and MathComp (e.g. -j)

  1. Configure, by:

     ./configure

  2. Build, by:

     make

  After building, you do not need to move the files anywhere else
  (and, by the way, `make install' does not work). The build system
  automatically generates a ./run-coqide.sh script to edit the sources
  with CoqIDE (if installed on your system), as well as local load
  path configuration files for Emacs+ProofGeneral (if installed on
  your system). If you want to compile code against VCFloat, you can
  have a look at the autogenerated `coqopts' file, to grab the load
  path options to pass to Coq and its relevant tools (coqc,
  coq_makefile, etc.)