We demonstrate tools and methods for proofs about the correctness and numerical accuracy of C programs. The tools are foundational, in that they are connected to formal semantic specifications of the C operational semantics and of the IEEE 754 floating-point format. The tools are modular, in that the reasoning about C programming can be done quite separately from the reasoning about numerical correctness and numerical accuracy. The tools are general, in that they accommodate almost the entire C language (with pointer data structures, function pointers, control flow, etc.) and applied mathematics (reasoned about in a general-purpose logic and proof assistant with substantial libraries for mathematical reasoning). We demonstrate on a simple Newton's-method square root function.
Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software. The fastest algorithms are complex enough that formally verifying them is desirable but challenging. We have formally verified a comprehensive arbitrary-precision integer arithmetic library that implements many state-of-the-art algorithms from the GMP library. The algorithms we have verified include addition, subtraction, Toom-Cook multiplication, division and square root. We use the Why3 platform to perform the proof semi-automatically. We obtain an efficient and formally verified C library of low-level functions on arbitrary-precision natural integers. This verification covers the functional correctness of the algorithms, as well as the memory safety and absence of arithmetic overflows of their C implementation. Using detailed pseudocode, we present the algorithms that we verified and outline their proofs.
We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF, which feature "lock"-type constructors, and on the new perspectives offered by its novel "shallow" implementation in Coq. The L^P(N:sigma)[.] constructor, and its binding variant L^P(?x:sigma)[.], capture monadically the concept of inhabitability up-to. They were originally introduced for factoring-out, postponing, or delegating to external tools the verification of time-consuming judgments, which are "morally" proof-irrelevant, thus allowing for integrating different sources of epistemic evidence in a unique Logical Framework. Experimenting with "locks" has shown that they are also a very flexible tool for expressing in Type Theory several diverse cognitive attitudes and mental strategies used in ordinary reasoning. These range from the emerging paradigm of "fast and loose reasoning", which trades off efficiency for correctness, as in naive Set Theory, or in computer architecture and distributed systems, when branch prediction and optimistic concurrency control are implemented. Lock-types naturally express also Typical Ambiguity provisos, "squash"' types, and many forms of "reasoning-up-to".
There are several commutativity theorems in groups and rings which involve power maps f(x) = x n . The most famous example of this kind is Jacobson's theorem which asserts that any ring satisfying the identity x n = x is commutative. Such statements belong to first order logic with equality and hence provable, in principle, by any first-order theorem-prover. However, because of the presence of an arbitrary integer parameter n in the exponent, they are outside the scope of any first-order theorem-prover. In particular, one cannot use such an automated reasoning system to prove theorems involving power maps. Here we focus just on the needed properties of power maps f(x) = x n and show how one can avoid having to reason explicitly with integer exponents. Implementing these new equational properties of power maps, we show how a theorem-prover can be a handy tool for quickly proving or confirming the truth of such theorems.
Formalizing analysis on a computer involves a lot of “epsilon-delta” reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable “delta”. We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.
