vcfloat: A Coq repository from MSoegtropIMC

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.

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.

------------------- Special Note: Flocq3/Flocq4 compatibility---------

Between April 2022 and (estimated) October 2022, there is a
Flocq compatibility issue for the installation of VCFloat.
In the Coq Platform 2022.04, "Flocq" means Flocq 4.x
and "Flocq3" means Flocq 3.x. In that Platform release, CompCert 3.10
is still using Flocq3, and therefore VST is still using Flocq3.

Packages that must be compatible with VST must (therefore) also use Flocq3.
Therefore in various files of VCFloat one will see (for example),
Require Import IntervalFlocq3.Tactic.
Require Import Flocq3.Core.

The Coq Platform 2202.04 includes these packages (Flocq3 and IntervalFlocq3).

As soon as the next release 3.11 of CompCert comes out, it will be
a client of ordinary Flocq (meaning 4.x), as will VST, and the entire
Flocq3 issue will disappear.

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

VCFloat requires Coq 8.15 (but might work under Coq 8.14).

VCFloat depends on the following further external libraries, accessed
from opam, from the Coq Platform, or (deprecated method) automatically
downloaded from their official sources and built during VCFloat's
building process:

- CompCert 3.10 (from AbsInt's GitHub at https://github.com/AbsInt/CompCert.git),
or from opam (but you don't need CompCert at all if you are using the "ftype" style, see above)

- Ssreflect 1.5 or later, e.g. from opam

- Mathematical Components (MathComp) 1.5 or later (opam)

- Flocq 3.4 (from INRIA GForge at
https://gforge.inria.fr/git/flocq/flocq.git, or from opam)

- Coq-Interval 4.3.0 (from INRIA GForge at
https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git,
or opam).

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

Usage method 1:
Use the Coq Platform (https://github.com/coq/platform)
to ensure that Coq has access to all the above-named packages.
Then
1. cd into the vcfloat directory
2. make depend
3. make

Usage method 2: without using Coq Platform or opam
(deprecated; not recently tested)
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.)

MSoegtropIMC/vcfloat