Archive of Formal Proofs

A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

Albert Rizaldi, Fabian Immler — 01 Jun 2020 00:00:00 +0000

The Vienna Convention on Road Traffic defines the safe distance traffic rules informally. This could make autonomous vehicle liable for safe-distance-related accidents because there is no clear definition of how large a safe distance is. We provide a formally proven prescriptive definition of a safe distance, and checkers which can decide whether an autonomous vehicle is obeying the safe distance rule. Not only does our work apply to the domain of law, but it also serves as a specification for autonomous vehicle manufacturers and for online verification of path planners.

A verified algorithm for computing the Smith normal form of a matrix

Jose Divasón — 23 May 2020 00:00:00 +0000

This work presents a formal proof in Isabelle/HOL of an algorithm to transform a matrix into its Smith normal form, a canonical matrix form, in a general setting: the algorithm is parameterized by operations to prove its existence over elementary divisor rings, while execution is guaranteed over Euclidean domains. We also provide a formal proof on some results about the generality of this algorithm as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out switching conveniently between two different existing libraries: the Hermite normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This permits to reuse results from both developments and it is done by means of the lifting and transfer package together with the use of local type definitions.

The Nash-Williams Partition Theorem

Lawrence C. Paulson — 16 May 2020 00:00:00 +0000

In 1965, Nash-Williams discovered a generalisation of the infinite form of Ramsey's theorem. Where the latter concerns infinite sets of n-element sets for some fixed n, the Nash-Williams theorem concerns infinite sets of finite sets (or lists) subject to a “no initial segment” condition. The present formalisation follows a monograph on Ramsey Spaces by Todorčević.

A Formalization of Knuth–Bendix Orders

Christian Sternagel, René Thiemann — 13 May 2020 00:00:00 +0000

We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.

Irrationality Criteria for Series by Erdős and Straus

Angeliki Koutsoukou-Argyraki, Wenda Li — 12 May 2020 00:00:00 +0000

We formalise certain irrationality criteria for infinite series of the form: \[\sum_{n=1}^\infty \frac{b_n}{\prod_{i=1}^n a_i} \] where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers with $a_n >1$ for all large n. The results are due to P. Erdős and E. G. Straus [1]. In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1. The latter is an application of Theorem 2.1 involving the prime numbers.

Recursion Theorem in ZF

Georgy Dunaev — 11 May 2020 00:00:00 +0000

This document contains a proof of the recursion theorem. This is a mechanization of the proof of the recursion theorem from the text Introduction to Set Theory, by Karel Hrbacek and Thomas Jech. This implementation may be used as the basis for a model of Peano arithmetic in ZF. While recursion and the natural numbers are already available in Isabelle/ZF, this clean development is much easier to follow.

An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

Salomon Sickert — 08 May 2020 00:00:00 +0000

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee \mathbf{F}\mathbf{G} \psi_i$, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present an executable formalisation of a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up.

Formalization of Forcing in Isabelle/ZF

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf — 06 May 2020 00:00:00 +0000

We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC.

Banach-Steinhaus Theorem

Dominique Unruh, Jose Manuel Rodriguez Caballero — 02 May 2020 00:00:00 +0000

We formalize in Isabelle/HOL a result due to S. Banach and H. Steinhaus known as the Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal.

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

Florian Kammueller — 27 Apr 2020 00:00:00 +0000

In this article, we present a proof theory for Attack Trees. Attack Trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we develop a generic theory of Attack Trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of Attack Trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of Attack Tree validity and CTL. The application is illustrated on the example of a healthcare IoT system and GDPR compliance verification.

Power Sum Polynomials

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form p_n(X₁,…, X_k) = X₁ⁿ + … + X_kⁿ. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials s_k in the form of a recurrence relation (-1)^k k s_k = ∑_i∈[0,k) (-1)ⁱ s_i p_k-i .

As an application, this is then used to solve a generalised form of a puzzle given as an exercise in Dummit and Foote's Abstract Algebra: For k complex unknowns x₁, …, x_k, define p_j := x₁^j + … + x_k^j. Then for each vector a ∈ ℂ^k, show that there is exactly one solution to the system p₁ = a₁, …, p_k = a_k up to permutation of the x_i and determine the value of p_i for i>k.

The Lambert W Function on the Reals

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

The Lambert W function is a multi-valued function defined as the inverse function of x ↦ x e^x. Besides numerous applications in combinatorics, physics, and engineering, it also frequently occurs when solving equations containing both e^x and x, or both x and log x.

This article provides a definition of the two real-valued branches W₀(x) and W_-1(x) and proves various properties such as basic identities and inequalities, monotonicity, differentiability, asymptotic expansions, and the MacLaurin series of W₀(x) at x = 0.

Gaussian Integers

Manuel Eberl — 24 Apr 2020 00:00:00 +0000

The Gaussian integers are the subring ℤ[i] of the complex numbers, i. e. the ring of all complex numbers with integral real and imaginary part. This article provides a definition of this ring as well as proofs of various basic properties, such as that they form a Euclidean ring and a full classification of their primes. An executable (albeit not very efficient) factorisation algorithm is also provided.

Lastly, this Gaussian integer formalisation is used in two short applications:

The characterisation of all positive integers that can be written as sums of two squares
Euclid's formula for primitive Pythagorean triples

While elementary proofs for both of these are already available in the AFP, the theory of Gaussian integers provides more concise proofs and a more high-level view.

Matrices for ODEs

Jonathan Julian Huerta y Munive — 19 Apr 2020 00:00:00 +0000

Our theories formalise various matrix properties that serve to establish existence, uniqueness and characterisation of the solution to affine systems of ordinary differential equations (ODEs). In particular, we formalise the operator and maximum norm of matrices. Then we use them to prove that square matrices form a Banach space, and in this setting, we show an instance of Picard-Lindelöf’s theorem for affine systems of ODEs. Finally, we use this formalisation to verify three simple hybrid programs.

Authenticated Data Structures As Functors

Andreas Lochbihler, Ognjen Marić — 16 Apr 2020 00:00:00 +0000

Authenticated data structures allow several systems to convince each other that they are referring to the same data structure, even if each of them knows only a part of the data structure. Using inclusion proofs, knowledgeable systems can selectively share their knowledge with other systems and the latter can verify the authenticity of what is being shared. In this article, we show how to modularly define authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL, using a shallow embedding. Modularity allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of Canton, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees.

Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows

Lukas Heimes, Dmitriy Traytel, Joshua Schneider — 10 Apr 2020 00:00:00 +0000

Basin et al.'s sliding window algorithm (SWA) is an algorithm for combining the elements of subsequences of a sequence with an associative operator. It is greedy and minimizes the number of operator applications. We formalize the algorithm and verify its functional correctness. We extend the algorithm with additional operations and provide an alternative interface to the slide operation that does not require the entire input sequence.

A Comprehensive Framework for Saturation Theorem Proving

Sophie Tourret — 09 Apr 2020 00:00:00 +0000

This Isabelle/HOL formalization is the companion of the technical report “A comprehensive framework for saturation theorem proving”, itself companion of the eponym IJCAR 2020 paper, written by Uwe Waldmann, Sophie Tourret, Simon Robillard and Jasmin Blanchette. It verifies a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition, and allows to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus using a variant of the given clause loop. The technical report “A comprehensive framework for saturation theorem proving” is available on the Matryoshka website. The names of the Isabelle lemmas and theorems corresponding to the results in the report are indicated in the margin of the report.

Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

09 Apr 2020 00:00:00 +0000

A monitor is a runtime verification tool that solves the following problem: Given a stream of time-stamped events and a policy formulated in a specification language, decide whether the policy is satisfied at every point in the stream. We verify the correctness of an executable monitor for specifications given as formulas in metric first-order dynamic logic (MFODL), which combines the features of metric first-order temporal logic (MFOTL) and metric dynamic logic. Thus, MFODL supports real-time constraints, first-order parameters, and regular expressions. Additionally, the monitor supports aggregation operations such as count and sum. This formalization, which is described in a forthcoming paper at IJCAR 2020, significantly extends previous work on a verified monitor for MFOTL. Apart from the addition of regular expressions and aggregations, we implemented multi-way joins and a specialized sliding window algorithm to further optimize the monitor.

Stateful Protocol Composition and Typing

Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker — 08 Apr 2020 00:00:00 +0000

We provide in this AFP entry several relative soundness results for security protocols. In particular, we prove typing and compositionality results for stateful protocols (i.e., protocols with mutable state that may span several sessions), and that focuses on reachability properties. Such results are useful to simplify protocol verification by reducing it to a simpler problem: Typing results give conditions under which it is safe to verify a protocol in a typed model where only "well-typed" attacks can occur whereas compositionality results allow us to verify a composed protocol by only verifying the component protocols in isolation. The conditions on the protocols under which the results hold are furthermore syntactic in nature allowing for full automation. The foundation presented here is used in another entry to provide fully automated and formalized security proofs of stateful protocols.

Automated Stateful Protocol Verification

Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker, Anders Schlichtkrull — 08 Apr 2020 00:00:00 +0000

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. In this AFP entry, we present a fully-automated approach for verifying stateful security protocols, i.e., protocols with mutable state that may span several sessions. The approach supports reachability goals like secrecy and authentication. We also include a simple user-friendly transaction-based protocol specification language that is embedded into Isabelle.

Lucas's Theorem

Chelsea Edmonds — 07 Apr 2020 00:00:00 +0000

This work presents a formalisation of a generating function proof for Lucas's theorem. We first outline extensions to the existing Formal Power Series (FPS) library, including an equivalence relation for coefficients modulo n, an alternate binomial theorem statement, and a formalised proof of the Freshman's dream (mod p) lemma. The second part of the work presents the formal proof of Lucas's Theorem. Working backwards, the formalisation first proves a well known corollary of the theorem which is easier to formalise, and then applies induction to prove the original theorem statement. The proof of the corollary aims to provide a good example of a formalised generating function equivalence proof using the FPS library. The final theorem statement is intended to be integrated into the formalised proof of Hilbert's 10th Problem.

Strong Eventual Consistency of the Collaborative Editing Framework WOOT

Emin Karayel, Edgar Gonzàlez — 25 Mar 2020 00:00:00 +0000

Commutative Replicated Data Types (CRDTs) are a promising new class of data structures for large-scale shared mutable content in applications that only require eventual consistency. The WithOut Operational Transforms (WOOT) framework is a CRDT for collaborative text editing introduced by Oster et al. (CSCW 2006) for which the eventual consistency property was verified only for a bounded model to date. We contribute a formal proof for WOOTs strong eventual consistency.

Furstenberg's topology and his proof of the infinitude of primes

Manuel Eberl — 22 Mar 2020 00:00:00 +0000

This article gives a formal version of Furstenberg's topological proof of the infinitude of primes. He defines a topology on the integers based on arithmetic progressions (or, equivalently, residue classes). Using some fairly obvious properties of this topology, the infinitude of primes is then easily obtained.

Apart from this, this topology is also fairly ‘nice’ in general: it is second countable, metrizable, and perfect. All of these (well-known) facts are formally proven, including an explicit metric for the topology given by Zulfeqarr.

An Under-Approximate Relational Logic

Toby Murray — 12 Mar 2020 00:00:00 +0000

Recently, authors have proposed under-approximate logics for reasoning about programs. So far, all such logics have been confined to reasoning about individual program behaviours. Yet there exist many over-approximate relational logics for reasoning about pairs of programs and relating their behaviours. We present the first under-approximate relational logic, for the simple imperative language IMP. We prove our logic is both sound and complete. Additionally, we show how reasoning in this logic can be decomposed into non-relational reasoning in an under-approximate Hoare logic, mirroring Beringer’s result for over-approximate relational logics. We illustrate the application of our logic on some small examples in which we provably demonstrate the presence of insecurity.

Hello World

Cornelius Diekmann, Lars Hupel — 07 Mar 2020 00:00:00 +0000

In this article, we present a formalization of the well-known "Hello, World!" code, including a formal framework for reasoning about IO. Our model is inspired by the handling of IO in Haskell. We start by formalizing the 🌍 and embrace the IO monad afterwards. Then we present a sample main :: IO (), followed by its proof of correctness.

Implementing the Goodstein Function in λ-Calculus

Bertram Felgenhauer — 21 Feb 2020 00:00:00 +0000

In this formalization, we develop an implementation of the Goodstein function G in plain λ-calculus, linked to a concise, self-contained specification. The implementation works on a Church-encoded representation of countable ordinals. The initial conversion to hereditary base 2 is not covered, but the material is sufficient to compute the particular value G(16), and easily extends to other fixed arguments.

A Generic Framework for Verified Compilers

Martin Desharnais — 10 Feb 2020 00:00:00 +0000

This is a generic framework for formalizing compiler transformations. It leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. It states common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as simulation and compiler composition, and prove general (partial) correctness theorems, resulting in reusable proof components.

Arithmetic progressions and relative primes

José Manuel Rodríguez Caballero — 01 Feb 2020 00:00:00 +0000

This article provides a formalization of the solution obtained by the author of the Problem “ARITHMETIC PROGRESSIONS” from the Putnam exam problems of 2002. The statement of the problem is as follows: For which integers n > 1 does the set of positive integers less than and relatively prime to n constitute an arithmetic progression?

A Hierarchy of Algebras for Boolean Subsets

Walter Guttmann, Bernhard Möller — 31 Jan 2020 00:00:00 +0000

We present a collection of axiom systems for the construction of Boolean subalgebras of larger overall algebras. The subalgebras are defined as the range of a complement-like operation on a semilattice. This technique has been used, for example, with the antidomain operation, dynamic negation and Stone algebras. We present a common ground for these constructions based on a new equational axiomatisation of Boolean algebras.

Mersenne primes and the Lucas–Lehmer test

Manuel Eberl — 17 Jan 2020 00:00:00 +0000

This article provides formal proofs of basic properties of Mersenne numbers, i. e. numbers of the form 2ⁿ - 1, and especially of Mersenne primes.

In particular, an efficient, verified, and executable version of the Lucas–Lehmer test is developed. This test decides primality for Mersenne numbers in time polynomial in n.