Welcome to the 8th ACM SIGPLAN International Conference on Certified
Programs and Proofs (CPP 2019), in cooperation with ACM SIGLOG. CPP
2019 was co-located with the 46th ACM SIGPLAN Symposium on Principles
of Programming Languages (POPL 2019) and took place in Cascais/Lisbon,
Portugal, from January 14 to January 15, 2019. We thank the POPL
organizing committee for their help in planning and organizing the
event, and the CPP Steering Committee for their guidance and advice.
IsaFoL (Isabelle Formalization of Logic) is an undertaking that aims at developing formal theories about logics, proof systems, and automatic provers, using Isabelle/HOL. At the heart of the project is the conviction that proof assistants have become mature enough to actually help researchers in automated reasoning when they develop new calculi and tools. In this paper, I describe and reflect on three verification subprojects to which I contributed: a first-order resolution prover, an imperative SAT solver, and generalized term orders for λ-free higher-order logic.
We present a linear logical framework implemented within the Hybrid
system. Hybrid is designed to support the use of higher-order abstract
syntax for representing and reasoning about formal systems,
implemented in the Coq Proof Assistant. In this work, we extend the
system with a linear specification logic, which provides
infrastructure for reasoning directly about object languages with
linear features.
We developed this framework in order to address the challenges of
reasoning about the type system of a quantum lambda calculus. In
particular, we started by considering the Proto-Quipper language,
which contains the core of Quipper. Quipper is a new quantum
programming language under active development with a linear type
system. We have completed a formal proof of type soundness for
Proto-Quipper. Our current work includes extending this work to other
properties of Proto-Quipper as well as reasoning about other quantum
programming languages. It also includes reasoning about other object
languages with linear features in areas such as meta-theory of
low-level abstract machine code, proof theory of focused linear
sequent calculi, and modeling biological processes as transition
systems and proving properties about them.
The field of p-adic numbers ℚ_{p} and the ring of p-adic integers ℤ_{p} are essential constructions of modern number theory. Hensel’s lemma, described by Gouvêa as the “most important algebraic property of the p-adic numbers,” shows the existence of roots of polynomials over ℤ_{p} provided an initial seed point. The theorem can be proved for the p-adics with significantly weaker hypotheses than for general rings. We construct ℚ_{p} and ℤ_{p} in the Lean proof assistant, with various associated algebraic properties, and formally prove a strong form of Hensel’s lemma. The proof lies at the intersection of algebraic and analytic reasoning and demonstrates how the Lean mathematical library handles such a heterogeneous topic.
Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n−1) + f(n−2) and the quite non-obvious closed form
1
√
5
(ϕ^{n} − (−ϕ)^{−n})
where ϕ is the golden ratio.
This work builds on existing tools in Isabelle – such as formal power series and polynomial factorisation algorithms – to develop a theory of these recurrences and derive a fully executable solver for them that can be exported to programming languages like Haskell.
Based on this development, I also provide an efficient method to prove ‘Big-O’ asymptotics of a solution automatically without explicitly finding the closed-form solution first.
We formalise the computational undecidability of validity, satisfiability, and provability of first-order formulas following a synthetic approach based on the computation native to Coq's constructive type theory.
Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many-one reductions from the Post correspondence problem (PCP).
Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation.
For instance, we prove the equivalence of Post's theorem with Markov's principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.
Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots.
In this paper, we have strengthened the root-counting ability in Isabelle/HOL by first formally proving the Budan-Fourier theorem. Subsequently, based on Descartes' rule of signs and Taylor shift, we have provided a verified procedure to efficiently over-approximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm's theorem. Finally, we combine verified components in the developments above to improve our previous certified complex-root-counting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics.
We formalize the definition and basic properties of smooth manifolds
in Isabelle/HOL. Concepts covered include partition of unity,
tangent and cotangent spaces, and the fundamental theorem for line
integrals. We also construct some concrete manifolds such as spheres
and projective spaces. The formalization makes extensive use of the
existing libraries for topology and analysis. The existing library
for linear algebra is not flexible enough for our needs. We
therefore set up the first systematic and large scale application of
``types to sets''. It allows us to automatically transform the
existing (type based) library of linear algebra to one with explicit
carrier sets.
When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead, our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quantifier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.
Type theories with equality reflection, such as extensional type
theory (ETT), are convenient theories in which to formalise
mathematics, as they make it possible to consider provably equal terms
as convertible. Although type-checking is undecidable in this context,
variants of ETT have been implemented, for example in NuPRL and more
recently in Andromeda.
The actual objects that can be checked are not proof-terms, but
derivations of proof-terms. This suggests that any derivation of ETT
can be translated into a typecheckable proof term of intensional type
theory (ITT).
However, this result, investigated categorically by
Hofmann in 1995, and 10 years later more
syntactically by Oury, has never given rise to
an effective translation.
In this paper, we provide the first effective syntactical translation
from ETT to ITT with uniqueness of identity proofs and functional
extensionality. This translation has been defined and proven correct
in Coq and yields an executable plugin that translates a derivation
in ETT into an actual Coq typing judgment. Additionally, we show how
this result is extended in the context of homotopy type theory to a
two-level type theory.
We formally prove the undecidability of entailment in intuitionistic linear logic in Coq.
We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic.
The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified low-level compiler for instruction-based languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics.
We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the
reduction proofs to focus on correctness properties.
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define its equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full λ-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RR_{n} relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.
Certified ACKBO
Alexander Lochmann and Christian Sternagel (University of Innsbruck, Austria)
Term rewriting in the presence of associative and commutative function symbols constitutes a highly expressive model of computation, which is for example well suited to reason about parallel computations. However, it is well known that the standard notion of termination does not apply any more: any term rewrite system containing a commutativity rule is nonterminating. Thus, instead of adding AC-rules to a rewrite system, we switch to the notion of AC-termination. AC-termination can for example be shown using AC-compatible reduction orders. One specific example of such an order is ACKBO. We present our Isabelle/HOL formalization of the ACKBO order. On an abstract level this gives us a mechanized proof of the fact that ACKBO is indeed an AC-compatible reduction order. Moreover, we integrated corresponding check functions into the verified certifier CeTA. This has the more practical consequence of enabling the machine certification of AC-termination proofs generated by automated termination tools.
The superposition calculus, which underlies first-order theorem provers such as E, SPASS, and Vampire, combines ordered resolution and equality reasoning. As a step towards verifying modern provers, we specify, using Isabelle/HOL, a purely functional first-order ordered resolution prover and establish its soundness and refutational completeness. Methodologically, we apply stepwise refinement to obtain, from an abstract nondeterministic specification, a verified deterministic program, written in a subset of Isabelle/HOL from which we extract purely functional Standard ML code that constitutes a semidecision procedure for first-order logic.
Formalising metatheory in the Coq proof assistant is tedious as reasoning with binders
without native support requires a lot of uninteresting technicalities.
To relieve users from so-produced boilerplate, the Autosubst framework automates working with de Bruijn terms:
For each annotated inductive type,
Autosubst generates a corresponding instantiation operation for parallel substitutions and a
decision procedure for assumption-free substitution lemmas.
However, Autosubst is implemented in Ltac, Coq's tactic language, and thus suffers from Ltac's
limitations. In particular, Autosubst is restricted to Coq and unscoped,
non-mutual inductive types with a single sort of variables.
In this paper, we present a new version of Autosubst that overcomes these restrictions.
Autosubst 2 is an external code generator, which translates second-order HOAS
specifications into potentially mutual inductive term sorts.
We extend the equational theory of Autosubst to the case of mutual inductive sorts by
combining the
application of multiple parallel substitutions into exactly one instantiation
operation for each sort, i.e. we parallelise substitutions to vector substitutions.
The resulting equational theory is both simpler and more expressive than that of
the original Autosubst framework and allows us to present an even more elegant
proof of part A of the POPLMark challenge.
This paper presents a methodology for generating formally proven equivalence theorems between decompiled x86-64 machine code and big step semantics.
These proofs are built on top of two additional contributions.
First, a robust and tested formal x86-64 machine model containing small step semantics for 1625 instructions.
Second, a decompilation-into-logic methodology supporting both x86-64 assembly and machine code at large scale.
This work enables black-box binary verification, i.e., formal verification of a binary where source code is unavailable.
As such, it can be applied to safety-critical systems that consist of legacy components, or components whose source code is unavailable due to proprietary reasons.
The methodology minimizes the trusted code base by leveraging machine-learned semantics to build a formal machine model.
We apply the methodology to several case studies, including binaries that heavily rely on the SSE2 floating-point instruction set, and binaries that are obtained by compiling code that is obtained by inlining assembly into C code.
The insertion of expressions mixing arithmetic operators and bitwise
boolean operators is a widespread protection of sensitive data in
source programs. This recent advanced obfuscation technique is one of
the less studied among program obfuscations even if it is commonly
found in binary code. In this paper, we formally verify in Coq this
data obfuscation. It operates over a generic notion of mixed
boolean-arithmetic expressions and on properties of bitwise operators
operating over machine integers. Our obfuscation performs two kinds of
program transformations: rewriting of expressions and insertion of
modular inverses. To facilitate its proof of correctness, we define
boolean semantic tables, a data structure inspired from truth tables.
Our obfuscation is integrated into the CompCert formally
verified compiler where it operates over Clight programs. The
automatic extraction of our program obfuscator into OCaml yields a
program with competitive results.
The Java Virtual Machine (JVM) postpones running class initialization methods until their classes are first referenced, such as by a new or static instruction. This process is called dynamic class initialization. Jinja is a semantic framework for Java and JVM developed in the theorem prover Isabelle that includes several semantics: Java-level big-step and small-step semantics, JVM-level small-step semantics, and an intermediate compilation step, J1, between these two levels. In this paper, we extend Jinja to include support for static instructions and dynamic class initialization. We also extend and re-prove related proofs, including Java-level type safety, equivalence between Java-level big-step and small-step semantics, and the correctness of a compilation from the Java level to the JVM level through J1. This work is based on the Java SE 8 specification.
The code responsible for serializing and deserializing untrusted
external data is a vital component of any software that communicates
with the outside world, as any bugs in these components can
compromise the entire system. This is particularly true for verified
systems which rely on trusted code to process external data, as any
defects in the parsing code can invalidate any formal proofs about
the system. One way to reduce the trusted code base of these systems
is to use interface generators like Protocol Buffer and ASN.1 to
generate serializers and deserializers from data descriptors. Of
course, these generators are not immune to bugs.
In this work, we formally verify a compiler for a realistic subset
of the popular Protocol Buffer serialization format using the Coq
proof assistant, proving once and for all the correctness of every
generated serializer and deserializer. One of the challenges we had
to overcome was the extreme flexibility of the Protocol Buffer
format: the same source data can be encoded in an infinite number of
ways, and the deserializer must faithfully recover the original
source value from each. We have validated our verified system using
the official conformance tests.
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic (University of Pennsylvania, USA; Princeton University, USA; Yale University, USA; University of Illinois at Chicago, USA)
We present the first formal verification of a networked server implemented in C. Interaction trees, a general structure for representing reactive computations, are used to tie together disparate verification and testing tools (Coq, VST, and QuickChick) and to axiomatize the behavior of the operating system on which the server runs (CertiKOS). The main theorem connects a specification of acceptable server behaviors, written in a straightforward “one client at a time” style, with the CompCert semantics of the C program. The variability introduced by low-level buffering of messages and interleaving of multiple TCP connections is captured using network refinement, a variant of observational refinement.
In this article, we provide a Coq mechanised, executable, formal semantics for a realistic fragment of SQL consisting of "select [distinct] from where group by having" queries with null values, functions, aggregates, quantifiers and nested potentially correlated sub-queries. Relying on the Coq extraction mechanism to Ocaml, we further produce a Coq certified semantic analyser for a SQL compiler. We then relate this fragment to a Coq formalised (extended) relational algebra that enjoys a bag semantics hence recovering all well-known algebraic equivalences upon which are based most of compilation optimisations. By doing so, we provide the first formally mechanised proof of the equivalence of SQL and extended relational algebra.