GitLab

This adds an optional dependency on MPFR to run why3execute for floats. It
is also used for reals (represented as intervals of floats).
This commit does the following changes:
- update the configure/Makefile to allow MPFR dependency
- adds a MPFR wrapper so that why3execute can still be compiled if MPFR is
  not installed. In this case, an exception is raised when executing on
  real/float.
- some updates are made to the standard library so that real/float
  functions are part of the program world (and can be executed).
- pinterp changes to make elementary functions from real and float
  executable.
- add some tests under bench/interp for manual testing of this feature

Note that the correctness of the results given for reals depends on the
precision. A too low precision may give unexpected results.

For the previous behaviour (no import), write "use/clone T as T".

This shortens the most used "use/clone import" to simply "use/clone".

Clone "with axiom ." or "with goal ." to change the default
("with lemma ." is also accepted, just in case).

The feature is not yet fully implemented (e.g. escape characters).

+ add 'minInt and 'maxInt attributes for range types
+ add 'eb and 'sb attributes for float types
+ make ieee_float realization compatible with Coq 8.4

+ add axioms linking eb, sb, emax and pow2sb and clone them as goal in Float(32/64)
+ modify section dealing with integers
+ update realisation

+ add predicate "exact_int"
+ add three axioms on of_int +/-/*
+ add some other axioms
+ guard the theory realization with a dependency to flocq in make file

+ simplify some others
+ add a realization of real.Truncate
+ add a, almost complete, realization (missing fma related axioms + some non-axiomatized definitions)

The _rev lemmas cannot mention anything about the to_real values. Indeed,
with a directed rounding, in case of overflow, the result might still be
finite, yet be unrelated to the infinitely-precise value.

Note that the lemmas were true for rounding to nearest though (since the
result is necessarily infinite in case of overflow then), so it might be
worth adding back some specialized versions for rounding to nearest.

Note also that lemmas for neg, abs, and sqrt, do not need fixing, since
these operations cannot overflow.

This commit also fixes some issues about to_int_monotonic_int. Indeed,
large integers are not always representable, so we get to_int RNU x = x >
i for x = of_int RNU i.

When proving a program that does not allow for exceptional behaviors, the
context is littered with finiteness facts (due to operator preconditions),
so these lemmas help some provers by reducing the amount of instantiations
needed to produce the problem on real numbers.

This patch also adds an axiom so that is_finite, is_infinite, and is_nan
are actually disjoint. It also modifies the axiom about sqrt so that its
precondition is expressed on real numbers directly.

- some cleanup
- add the axiom "abs_universal"

Alt-Ergo was actually able to derive an inconsistency from these axioms,
which is kind of incredible.

- to_real x = 0 does not imply is_zero x, unless x is finite.
- Add missing triggers.
- Move any property related to signed zeros from "_finite" to "_special".
- Fix incorrect signed zeros for addition, subtraction, and FMA.
- Remove inconsistent signs of NaN for negation, multiplication, and division.
- Add specification for special values of abs.
- Fix useless specification for sqrt(+oo).