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

Version 1.0 (2015-12-04) Initial release
Version 2.0 (2022-3-10) Many improvements, see below.

Copyright (C) 2015 Reservoir Labs Inc.
Copyright (C) 2021-22  Andrew W. Appel and Ariel Kellison.

VCFloat is open-source licensed according to the LGPL (Gnu Lesser General
Public License) version 3 or any later version.

Previously it was licensed differently; see OLD_LICENSE for an explanation.

This software is distributed WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

By making a pull-request to this repo, or by making a direct push, or by contributing
by any other such means, you thereby certify that you have the rights to do
so specified in the Developer Certificate of Origin, https://developercertificate.org/
and you also thereby license your contribution by the LGPL 3.0 and later.

VCFloat 1.0 was implemented 2015 by Tahina Ramananandro et al (see citation below).
VCFloat since 2021 is maintained and extended by Andrew Appel and Ariel Kellison.

For an introduction, read
VCFloat2: Floating-point error analysis in Coq, by Appel & Kellison, 2022,
available as doc/vcfloat2.pdf in this repository.

For more technical information on VCFloat, you can read Sections 1-4 of:

Tahina Ramananandro, Paul Mountcastle, Benoit Meister and Richard Lethin.
A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
ACM SIGPLAN Conference on Certified Programs and Proofs (CPP),  2016.
https://dl.acm.org/doi/10.1145/2854065.2854066

THE CORE OF VCFLOAT

The core definitions and theorems are in:
 vcfloat/FPCore.v  -- definitions of basic types
 vcfloat/FPLang.v  -- deep-embedded description langage and rndval_with_cond theory
 vcfloat/FPLangOpt.v -- transformations on deep-embedded expressions

APPLICATION STYLE "Clight"
 VCFloat 1.0 was designed for use on CompCert Clight expression trees,
 as described in Ramananandro et al.  These files have been updated
 to latest versions of CompCert, Coq, and FPLang; they build in Coq
 but have not been tested.

 FILES: vcfloat/FPSolve.v,  vcfloat/cverif/*.v

APPLICATION STYLE "ftype"
 VCFloat 2.0 supports in addition a use case independent of CompCert Clight.
 One starts with a shallow-embedded floating-point expression,
 using the ordinary operators of Floqc (Binary.Bmult, Binary.Bplus, etc)
 but wrapped in special Coq definitions.


 FILES: vcfloat/Automate.v, vcfloat/Test.v

 See Test.v for an explanation of how to use VCFloat in this style.

------------------------- Requirements Notes -------------------------

VCFloat depends on Coq's Flocq and Interval packages.

See coq-vcfloat.opam to see which versions of Coq, coq-flocq, and coq-interval are needed.


To install:

Use the Coq Platform (https://github.com/coq/platform)
to ensure that Coq has access to all the above-named packages.
Very possibly, by early 2024 coq-vcfloat will be included in the Coq platform.

If vcfloat is not already in the Coq Platform, then install the Coq platform, then:
 1. cd into the vcfloat/vcfloat directory
 2. make depend
 3. make
 4. make install