International audience

Designing an efficient yet accurate floating-point approximation of a mathematical function is an intricate and error-prone process. This warrants the use of formal methods, especially formal proof, to achieve some degree of confidence in the implementation. Unfortunately, the lack of automation or its poor interplay with the more manual parts of the proof makes it way too costly in practice. This article revisits the issue by proposing a methodology and some dedicated automation, and applies them to the use case of a faithful binary64 approximation of exponential. The peculiarity of this use case is that the target of the formal verification is not a simple modeling of an external code; it is an actual floating-point function defined in the logic of the Coq proof assistant, which is thus usable inside proofs once its correctness has been fully verified. This function presents all the attributes of a state-of-the-art implementation: bit-level manipulations, large tables of constants, obscure floating-point transformations, exceptional values, etc. This function has been integrated into the proof strategies of the CoqInterval library, bringing a 20× speedup with respect to the previous implementation.

Short of being able to exhaustively test all the inputs, writing a formal proof offers the highest possible confidence in the correctness of a mathematical library. This comes at a large cost though, since formal proofs require taking into account all the details, even the seemingly insignificant ones, which makes them tedious to write. This issue is compounded by the fact that the objects whose properties we need to verify (floating-point numbers) are not the ones we would like to reason about (real numbers and integers). This short paper explores some ways of reducing the overhead of formal proofs in the setting of mathematical libraries, so as to let the user focus on the details that really matter.

Abstract The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. However, continuous distributions have to be discretized because the corresponding measures cannot be defined on all subsets of their carriers. This paper proposes the use of synthetic topology to model continuous distributions for probabilistic computations in type theory. We study the initial σ-frame and the corresponding induced topology on arbitrary sets. Based on these intrinsic topologies, we define valuations and lower integrals on sets and prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed.

Numerical integration schemes are mandatory to understand complex behaviors of dynamical systems described by ordinary differential equations. Implementation of these numerical methods involve floating-point computations and propagation of round-off errors. This paper presents a new fine-grained analysis of round-off errors in explicit Runge-Kutta integration methods, taking into account exceptional behaviors, such as underflow and overflow. Linear stability properties play a central role in the proposed approach. For a large class of Runge-Kutta methods applied on linear problems, a tight bound of the round-off errors is provided. A simple test is defined and ensures the absence of underflow and a tighter round-off error bound. The absence of overflow is guaranteed as linear stability properties imply that (computed) solutions are non-increasing.

High-level synthesis (HLS) tools such as VivadoHLS interpret C/C++ code supplemented by proprietary optimization directives called pragmas. In order to perform loop pipelining, HLS compilers have to deal with non-trivial loop-carried data dependencies. In VivadoHLS, the dependence pragma could be used to enforce or to eliminate such dependencies, but, the behavior of this directive is only informally specified through examples. Most of the time programmers and the compiler seem to agree on what the directive means, but the accidental misuse of this pragma can lead to the silent generation of an erroneous register-transfer level (RTL) design, meaning code that previously worked may break with newer more aggressively optimised releases of the compiler. We use the Coq proof assistant to formally specify and verify the behavior of the VivadoHLS dependence pragma. We first embed the syntax and the semantics of a tiny imperative language Imp in Coq and specify a conformance relation between an Imp program and a dependence pragma based on data-flow transformations. We then implement semi-automated methods to formally verify such conformance relations for non-nested loop bodies.

Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10. This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.

Ordinary differential equations are ubiquitous in scientific computing. Solving exactly these equations is usually not possible, except for special cases, hence the use of numerical schemes to get a discretized solution. We are interested in such numerical integration methods, for instance Euler's method or the Runge-Kutta methods. As they are implemented using floating-point arithmetic, round-off errors occur. In order to guarantee their accuracy, we aim at providing bounds on the round-off errors of explicit one-step numerical integration methods. Our methodology is to apply a fine-grained analysis to these numerical algorithms. Our originality is that our floating-point analysis takes advantage of the linear stability of the scheme, a mathematical property that vouches the scheme is well-behaved.

The Finite Element Method is a widely-used method to solve numerical problems coming for instance from physics or biology. To obtain the highest confidence on the correction of numerical simulation programs implementing the Finite Element Method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The Lax–Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. This article presents the full formal proof of the Lax–Milgram theorem in Coq. It requires many results from linear algebra, geometry, functional analysis, and Hilbert spaces.