Archive of Formal Proofs

Fresh identifiers

Andrei Popescu, Thomas Bauereiss — 16 Aug 2021 00:00:00 +0000

This entry defines a type class with an operator returning a fresh identifier, given a set of already used identifiers and a preferred identifier. The entry provides a default instantiation for any infinite type, as well as executable instantiations for natural numbers and strings.

CoSMed: A confidentiality-verified social media platform

Thomas Bauereiss, Andrei Popescu — 16 Aug 2021 00:00:00 +0000

This entry contains the confidentiality verification of the (functional kernel of) the CoSMed social media platform. The confidentiality properties are formalized as instances of BD Security [1, 2]. An innovation in the deployment of BD Security compared to previous work is the use of dynamic declassification triggers, incorporated as part of inductive bounds, for providing stronger guarantees that account for the repeated opening and closing of access windows. To further strengthen the confidentiality guarantees, we also prove "traceback" properties about the accessibility decisions affecting the information managed by the system.

CoSMeDis: A confidentiality-verified distributed social media platform

Thomas Bauereiss, Andrei Popescu — 16 Aug 2021 00:00:00 +0000

This entry contains the confidentiality verification of the (functional kernel of) the CoSMeDis distributed social media platform presented in [1]. CoSMeDis is a multi-node extension the CoSMed prototype social media platform [2, 3, 4]. The confidentiality properties are formalized as instances of BD Security [5, 6]. The lifting of confidentiality properties from single nodes to the entire CoSMeDis network is performed using compositionality and transport theorems for BD Security, which are described in [1] and formalized in a separate AFP entry.

CoCon: A Confidentiality-Verified Conference Management System

Andrei Popescu, Peter Lammich, Thomas Bauereiss — 16 Aug 2021 00:00:00 +0000

This entry contains the confidentiality verification of the (functional kernel of) the CoCon conference management system [1, 2]. The confidentiality properties refer to the documents managed by the system, namely papers, reviews, discussion logs and acceptance/rejection decisions, and also to the assignment of reviewers to papers. They have all been formulated as instances of BD Security [3, 4] and verified using the BD Security unwinding technique.

Compositional BD Security

Thomas Bauereiss, Andrei Popescu — 16 Aug 2021 00:00:00 +0000

Building on a previous AFP entry that formalizes the Bounded-Deducibility Security (BD Security) framework [1], we formalize compositionality and transport theorems for information flow security. These results allow lifting BD Security properties from individual components specified as transition systems, to a composition of systems specified as communicating products of transition systems. The underlying ideas of these results are presented in the papers [1] and [2]. The latter paper also describes a major case study where these results have been used: on verifying the CoSMeDis distributed social media platform (itself formalized as an AFP entry that builds on this entry).

Relational Forests

Walter Guttmann — 03 Aug 2021 00:00:00 +0000

We study second-order formalisations of graph properties expressed as first-order formulas in relation algebras extended with a Kleene star. The formulas quantify over relations while still avoiding quantification over elements of the base set. We formalise the property of undirected graphs being acyclic this way. This involves a study of various kinds of orientation of graphs. We also verify basic algorithms to constructively prove several second-order properties.

Finitely Generated Abelian Groups

Joseph Thommes, Manuel Eberl — 07 Jul 2021 00:00:00 +0000

This article deals with the formalisation of some group-theoretic results including the fundamental theorem of finitely generated abelian groups characterising the structure of these groups as a uniquely determined product of cyclic groups. Both the invariant factor decomposition and the primary decomposition are covered. Additional work includes results about the direct product, the internal direct product and more group-theoretic lemmas.

SpecCheck - Specification-Based Testing for Isabelle/ML

Kevin Kappelmann, Lukas Bulwahn, Sebastian Willenbrink — 01 Jul 2021 00:00:00 +0000

SpecCheck is a QuickCheck-like testing framework for Isabelle/ML. You can use it to write specifications for ML functions. SpecCheck then checks whether your specification holds by testing your function against a given number of generated inputs. It helps you to identify bugs by printing counterexamples on failure and provides you timing information. SpecCheck is customisable and allows you to specify your own input generators, test output formats, as well as pretty printers and shrinking functions for counterexamples among other things.

Van der Waerden's Theorem

Katharina Kreuzer, Manuel Eberl — 22 Jun 2021 00:00:00 +0000

This article formalises the proof of Van der Waerden's Theorem from Ramsey theory. Van der Waerden's Theorem states that for integers $k$ and $l$ there exists a number $N$ which guarantees that if an integer interval of length at least $N$ is coloured with $k$ colours, there will always be an arithmetic progression of length $l$ of the same colour in said interval. The proof goes along the lines of \cite{Swan}. The smallest number $N_{k,l}$ fulfilling Van der Waerden's Theorem is then called the Van der Waerden Number. Finding the Van der Waerden Number is still an open problem for most values of $k$ and $l$.

MiniSail - A kernel language for the ISA specification language SAIL

Mark Wassell — 18 Jun 2021 00:00:00 +0000

MiniSail is a kernel language for Sail, an instruction set architecture (ISA) specification language. Sail is an imperative language with a light-weight dependent type system similar to refinement type systems. From an ISA specification, the Sail compiler can generate theorem prover code and C (or OCaml) to give an executable emulator for an architecture. The idea behind MiniSail is to capture the key and novel features of Sail in terms of their syntax, typing rules and operational semantics, and to confirm that they work together by proving progress and preservation lemmas. We use the Nominal2 library to handle binding.

Public Announcement Logic

Asta Halkjær From — 17 Jun 2021 00:00:00 +0000

This work is a formalization of public announcement logic with countably many agents. It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!. The completeness proof builds on the Epistemic Logic theory.

A Shorter Compiler Correctness Proof for Language IMP

Pasquale Noce — 04 Jun 2021 00:00:00 +0000

This paper presents a compiler correctness proof for the didactic imperative programming language IMP, introduced in Nipkow and Klein's book on formal programming language semantics (version of March 2021), whose size is just two thirds of the book's proof in the number of formal text lines. As such, it promises to constitute a further enhanced reference for the formal verification of compilers meant for larger, real-world programming languages. The presented proof does not depend on language determinism, so that the proposed approach can be applied to non-deterministic languages as well. As a confirmation, this paper extends IMP with an additional non-deterministic choice command, and proves compiler correctness, viz. the simulation of compiled code execution by source code, for such extended language.

Lyndon words

Štěpán Holub, Štěpán Starosta — 24 May 2021 00:00:00 +0000

Lyndon words are words lexicographically minimal in their conjugacy class. We formalize their basic properties and characterizations, in particular the concepts of the longest Lyndon suffix and the Lyndon factorization. Most of the work assumes a fixed lexicographical order. Nevertheless we also define the smallest relation guaranteeing lexicographical minimality of a given word (in its conjugacy class).

Graph Lemma

Štěpán Holub, Štěpán Starosta — 24 May 2021 00:00:00 +0000

Graph lemma quantifies the defect effect of a system of word equations. That is, it provides an upper bound on the rank of the system. We formalize the proof based on the decomposition of a solution into its free basis. A direct application is an alternative proof of the fact that two noncommuting words form a code.

Combinatorics on Words Basics

Štěpán Holub, Martin Raška, Štěpán Starosta — 24 May 2021 00:00:00 +0000

We formalize basics of Combinatorics on Words. This is an extension of existing theories on lists. We provide additional properties related to prefix, suffix, factor, length and rotation. The topics include prefix and suffix comparability, mismatch, word power, total and reversed morphisms, border, periods, primitivity and roots. We also formalize basic, mostly folklore results related to word equations: equidivisibility, commutation and conjugation. Slightly advanced properties include the Periodicity lemma (often cited as the Fine and Wilf theorem) and the variant of the Lyndon-Schützenberger theorem for words. We support the algebraic point of view which sees words as generators of submonoids of a free monoid. This leads to the concepts of the (free) hull, the (free) basis (or code).

Regression Test Selection

Susannah Mansky — 30 Apr 2021 00:00:00 +0000

This development provides a general definition for safe Regression Test Selection (RTS) algorithms. RTS algorithms select which tests to rerun on revised code, reducing the time required to check for newly introduced errors. An RTS algorithm is considered safe if and only if all deselected tests would have unchanged results. This definition is instantiated with two class-collection-based RTS algorithms run over the JVM as modeled by JinjaDCI. This is achieved with a general definition for Collection Semantics, small-step semantics instrumented to collect information during execution. As the RTS definition mandates safety, these instantiations include proofs of safety. This work is described in Mansky and Gunter's LSFA 2020 paper and Mansky's doctoral thesis (UIUC, 2020).

Isabelle's Metalogic: Formalization and Proof Checker

Tobias Nipkow, Simon Roßkopf — 27 Apr 2021 00:00:00 +0000

In this entry we formalize Isabelle's metalogic in Isabelle/HOL. Furthermore, we define a language of proof terms and an executable proof checker and prove its soundness wrt. the metalogic. The formalization is intentionally kept close to the Isabelle implementation(for example using de Brujin indices) to enable easy integration of generated code with the Isabelle system without a complicated translation layer. The formalization is described in our CADE 28 paper.

Lifting the Exponent

Jakub Kądziołka — 27 Apr 2021 00:00:00 +0000

We formalize the Lifting the Exponent Lemma, which shows how to find the largest power of $p$ dividing $a^n \pm b^n$, for a prime $p$ and positive integers $a$ and $b$. The proof follows Amir Hossein Parvardi's.

The BKR Decision Procedure for Univariate Real Arithmetic

Katherine Cordwell, Yong Kiam Tan, André Platzer — 24 Apr 2021 00:00:00 +0000

We formalize the univariate case of Ben-Or, Kozen, and Reif's decision procedure for first-order real arithmetic (the BKR algorithm). We also formalize the univariate case of Renegar's variation of the BKR algorithm. The two formalizations differ mathematically in minor ways (that have significant impact on the multivariate case), but are quite similar in proof structure. Both rely on sign-determination (finding the set of consistent sign assignments for a set of polynomials). The method used for sign-determination is similar to Tarski's original quantifier elimination algorithm (it stores key information in a matrix equation), but with a reduction step to keep complexity low.

Gale-Stewart Games

Sebastiaan Joosten — 23 Apr 2021 00:00:00 +0000

This is a formalisation of the main result of Gale and Stewart from 1953, showing that closed finite games are determined. This property is now known as the Gale Stewart Theorem. While the original paper shows some additional theorems as well, we only formalize this main result, but do so in a somewhat general way. We formalize games of a fixed arbitrary length, including infinite length, using co-inductive lists, and show that defensive strategies exist unless the other player is winning. For closed games, defensive strategies are winning for the closed player, proving that such games are determined. For finite games, which are a special case in our formalisation, all games are closed.

Formalization of Timely Dataflow's Progress Tracking Protocol

Matthias Brun, Sára Decova, Andrea Lattuada, Dmitriy Traytel — 13 Apr 2021 00:00:00 +0000

Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We formalize this progress tracking protocol and verify its safety. Our formalization is described in detail in our forthcoming ITP'21 paper.

Information Flow Control via Dependency Tracking

Benedikt Nordhoff — 01 Apr 2021 00:00:00 +0000

We provide a characterisation of how information is propagated by program executions based on the tracking data and control dependencies within executions themselves. The characterisation might be used for deriving approximative safety properties to be targeted by static analyses or checked at runtime. We utilise a simple yet versatile control flow graph model as a program representation. As our model is not assumed to be finite it can be instantiated for a broad class of programs. The targeted security property is indistinguishable security where executions produce sequences of observations and only non-terminating executions are allowed to drop a tail of those. A very crude approximation of our characterisation is slicing based on program dependence graphs, which we use as a minimal example and derive a corresponding soundness result. For further details and applications refer to the authors upcoming dissertation.

Grothendieck's Schemes in Algebraic Geometry

Anthony Bordg, Lawrence Paulson, Wenda Li — 29 Mar 2021 00:00:00 +0000

We formalize mainstream structures in algebraic geometry culminating in Grothendieck's schemes: presheaves of rings, sheaves of rings, ringed spaces, locally ringed spaces, affine schemes and schemes. We prove that the spectrum of a ring is a locally ringed space, hence an affine scheme. Finally, we prove that any affine scheme is a scheme.

Hensel's Lemma for the p-adic Integers

Aaron Crighton — 23 Mar 2021 00:00:00 +0000

We formalize the ring of p-adic integers within the framework of the HOL-Algebra library. The carrier of the ring is formalized as the inverse limit of quotients of the integers by powers of a fixed prime p. We define an integer-valued valuation, as well as an extended-integer valued valuation which sends 0 to the infinite element. Basic topological facts about the p-adic integers are formalized, including completeness and sequential compactness. Taylor expansions of polynomials over a commutative ring are defined, culminating in the formalization of Hensel's Lemma based on a proof due to Keith Conrad.

Constructive Cryptography in HOL: the Communication Modeling Aspect

Andreas Lochbihler, S. Reza Sefidgar — 17 Mar 2021 00:00:00 +0000

Constructive Cryptography (CC) [ICS 2011, TOSCA 2011, TCC 2016] introduces an abstract approach to composable security statements that allows one to focus on a particular aspect of security proofs at a time. Instead of proving the properties of concrete systems, CC studies system classes, i.e., the shared behavior of similar systems, and their transformations. Modeling of systems communication plays a crucial role in composability and reusability of security statements; yet, this aspect has not been studied in any of the existing CC results. We extend our previous CC formalization [Constructive_Cryptography, CSF 2019] with a new semantic domain called Fused Resource Templates (FRT) that abstracts over the systems communication patterns in CC proofs. This widens the scope of cryptography proof formalizations in the CryptHOL library [CryptHOL, ESOP 2016, J Cryptol 2020]. This formalization is described in Abstract Modeling of Systems Communication in Constructive Cryptography using CryptHOL.

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

Ralph Bottesch, Jose Divasón, René Thiemann — 12 Mar 2021 00:00:00 +0000

We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.

Quantum projective measurements and the CHSH inequality

Mnacho Echenim — 03 Mar 2021 00:00:00 +0000

This work contains a formalization of quantum projective measurements, also known as von Neumann measurements, which are based on elements of spectral theory. We also formalized the CHSH inequality, an inequality involving expectations in a probability space that is violated by quantum measurements, thus proving that quantum mechanics cannot be modeled with an underlying local hidden-variable theory.

The Hermite–Lindemann–Weierstraß Transcendence Theorem

Manuel Eberl — 03 Mar 2021 00:00:00 +0000

This article provides a formalisation of the Hermite-Lindemann-Weierstraß Theorem (also known as simply Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the crowning achievements of 19th century number theory.

The theorem states that if $\alpha_1, \ldots, \alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$ are algebraically independent over $\mathbb{Q}$.

Like the previous formalisation in Coq by Bernard, I proceeded by formalising Baker's version of the theorem and proof and then deriving the original one from that. Baker's version states that for any algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have $\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only if all the $\beta_i$ are zero.

This has a number of direct corollaries, e.g.:

$e$ and $\pi$ are transcendental
$e^z$, $\sin z$, $\tan z$, etc. are transcendental for algebraic $z\in\mathbb{C}\setminus\{0\}$
$\ln z$ is transcendental for algebraic $z\in\mathbb{C}\setminus\{0, 1\}$

Mereology

Ben Blumson — 01 Mar 2021 00:00:00 +0000

We use Isabelle/HOL to verify elementary theorems and alternative axiomatizations of classical extensional mereology.

The Sunflower Lemma of Erdős and Rado

René Thiemann — 25 Feb 2021 00:00:00 +0000

We formally define sunflowers and provide a formalization of the sunflower lemma of Erdős and Rado: whenever a set of size-k-sets has a larger cardinality than (r - 1)^k · k!, then it contains a sunflower of cardinality r.