=Paper=
{{Paper
|id=Vol-3725/paper8
|storemode=property
|title=Reconstruction of SMT Proofs with Lambdapi
|pdfUrl=https://ceur-ws.org/Vol-3725/paper8.pdf
|volume=Vol-3725
|authors=Alessio Coltellacci,Stephan Merz,Gilles Dowek
|dblpUrl=https://dblp.org/rec/conf/smt/ColtellacciMD24
}}
==Reconstruction of SMT Proofs with Lambdapi==
https://ceur-ws.org/Vol-3725/paper8.pdf
Reconstruction of SMT proofs with Lambdapi
1 2 1
Alessio Coltellacci , Gilles Dowek and Stephan Merz
1
University of Lorraine, CNRS, Inria, Nancy, France
2
University of Paris-Saclay, Inria, ENS Paris-Saclay, CNRS, LMF, Gif-sur-Yvette, France
Abstract
The Alethe format is a representation of unsatisfiability proofs that has been adopted by several SMT solvers. We
describe work in progress for interpreting Alethe proofs and generating corresponding proofs that are accepted
by the Lambdapi proof checker, a foundational proof assistant based on dependent type theory and rewriting
rules that serve as a pivot for exchanging proofs between several interactive proof assistants. We give an overview
of the encoding of SMT logic and Alethe proofs in Lambdapi and present initial results of the evaluation of the
checker on benchmark examples.
1. Introduction
SMT solvers are widely used as automatic proof engines within interactive theorem provers or program
verification tools. When they are used as trusted proof engines, any bugs in the SMT solver could lead
to inconsistent theorems in the interactive prover, where correctness is paramount. State-of-the-art
SMT solvers have been found to have bugs [1] due in part to error-prone optimizations, despite the best
efforts of developers.
State-of-the-art SMT solvers can produce certificates (or proof traces) that can be checked inde-
pendently, thus avoiding integrators to place blind trust in proof backends. This approach presents
a good compromise between formally verifying the correctness of the solvers and not affecting their
performance. For example, it has been adopted in [2, 3] to reconstruct the proof trace in the proof
assistant Isabelle/HOL.
In this paper, we describe how SMT proofs can be reconstruced in the proof assistant Lambdapi [4],
an offspring of Dedukti. Lambdapi is an interactive proof system based on the ๐ฮ -calculus modulo
rewriting, featuring dependent types as in Martin-Lรถfโs type theory and allowing users to define
rewriting rules in order to reason modulo equations. It is intended as an assembly language for proof
assistants, enabling mechanical conversions of proofs between different systems through its built-in
export or with its galaxy of external tools that provide interoperability between Lambdapi and other
theorem provers (Figure 1). Consequently, the aims of our approach are twofold: reconstructing SMT
proofs in Lambdapi to guarantee their correctness as well as translating the proofs so that they can be
accepted by proof assistants such as Coq or Lean so that they can benefit from SMT proof support.
Our work is based on the proof checker Carcara [5] implemented in Rust, an independent checker
and elaborator for the SMT proofs format Alethe. This proof format is supported by the veriT solver,
and more recently by the CVC5 solver [6]. We present an extension of Carcara for translating the
Alethe proof into Lambdapi. We took advantage of Carcaraโs elaboration of Aletheโs proof, which helps
increase the success rate of proof reconstruction. The Alethe format allows steps of different granularity,
facilitating proof production, but verifying coarse-grained steps can require expensive proof search and
may lead to verification failures. Proof elaboration by Carcara transforms coarse-grained steps into
more fine-grained ones, increasing the potential success rate of reconstructing Alethe proofs.
Overview of the paper
Section 2 introduces the Alethe proof format and describes the elaborated proof produced by Carcara.
In Section 3, we present first the embedding of Alethe logic in Lambdapi, and then how we extended
22nd International Workshop on Satisfiability Modulo Theories (SMT 2024)
ยฉ 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
Lean SMT Isabelle
lea k
_d
Carcara
n2 e
dk b ell
Coq isa dk Agda
vodk agda2
Lambdapi
Dedukti
ho
Lo
Krajono
l
PVS Me 2d Zenon and ArchSAT
Ka k
K-framework Matita HOL
Figure 1: Lambdapi, an assembly language for proof systems
Carcara to mechanically translate an elaborated Alethe proof into a Lambdapi proof script. In Section 4,
we argue the soundness property of our work, and Section 5 provides an evaluation on a set of proofs
from the SMT-LIB benchmarks and proof obligations of a case study from the proof assistant TLAPS.
We conclude and outline future work in Section 6.
Related work
Hammers are components of some proof assistants such as Sledgehammer [7] for Isabelle/HOL, and
CoqHammer [8, 9] for Coq, that employ first-order automatic theorem provers (ATPs), including SMT
solvers, to discharge goals. The hammer translates the conjecture and any user-supplied facts to the
input language of the back-end, invokes it, and in the case of success attempts to reconstruct the proof
in the logic of the proof assistant, based on a trace of the proof found by the back-end. For example,
adoption by Sledgehammer of the Alethe format generated by the SMT solver veriT [3, 10] cut the
failure rate of reconstruction by 50% and reduced the checking time by 13%. These results encouraged
us to select the Alethe proof format to construct our solution.
SMTCoq is a Coq plugin written in Coq and fully certified [11] that checks proof witnesses coming
from external SAT and SMT solvers. For proof reconstruction, SMTCoq relies on computational
reflection: the certificate is directly processed by the reduction mechanism of Coqโs kernel. In our first
investigations, we attempted to convert the SMTCoq proof certificate to Lambdapi. However, we found
the proof term generated by computational reflection, including subterms corresponding to arithmetic
decision procedures in Micromega [12], to be too complex to be converted to Lambdapi. Moreover,
SMTCoq supports at this point an old version of the Alethe proof format.
Carcara [5] is an independent proof checker and proof elaborator for SMT proofs in the Alethe
format that is implemented in Rust. Although Carcara is not a certified checker like SMTCoq, it allows
a coarse-grained proof, containing implicit steps, to be elaborated to a fine-grained one that includes
more detailed steps or adds missing parameters. The resulting proof is intended to be easier to check
by an external proof assistant, in particular given the lack of meta-programming in the vernacular
language of Lambdapi.
2. Alethe
The Alethe proof format [13] for SMT solvers comprises two parts: the proof language based on
SMT-LIB and a collection of proof rules. Alethe proofs are a sequence ๐1 . . . ๐๐ , ๐ก1 , . . . , ๐ก๐ where the
๐๐ s correspond to the original SMT instance being refuted, each ๐ก๐ is a clause inferred from previous
elements of the sequence, and ๐ก๐ is โฅ (the empty clause). In the following sections, we designate the
SMT-LIB problem as the input problem.
1 (declare-sort U 0)
2 (declare-fun a () U)
3 (declare-fun b () U)
4 (declare-fun p (U) Bool)
5 (assert (p a))
6 (assert (= a b))
7 (assert (not (p b)))
8 (get-proof)
1 (assume a0 (p a))
2 (assume a1 (= a b))
3 (assume a2 (not (p b)))
4 (step t1 (cl (not (= (p a) (p b))) (not (p a)) (p b)) :rule equiv_pos2)
5 (step t2 (cl (= (p a) (p b))) :rule cong :premises (a1))
6 (step t3 (cl (p b)) :rule resolution :premises (t1 t2 a0))
7 (step t4 (cl) :rule resolution :premises (a2 t3))
Listing 1: Guiding input problem and its Alethe proof found by CVC5
In the following, we will use the input problem example Listing 1 with its Alethe proof (found by
CVC5) to provide an overview of Alethe concepts and to illustrate our embedding in Lambdapi.
An Alethe proof inherits the declarations of its input problem. All symbols (sorts, functions, assertions,
etc.) declared or defined in the input problem remain declared or defined, respectively. Furthermore,
the syntax for terms, sort, and annotations uses the syntactic rules defined in SMT-LIB [14, ยง3] and the
SMT signature context ฮฃ defined in [14, ยง5.1 and ยง5.2].
2.1. The Alethe Language
An Alethe proof is a list of steps representing forward reasoning whose general form is as follows:
clause
๐. ฮ โท ๐1 , . . . , ๐๐ ( โ ๐1 , . . . , ๐๐ ) [๐1 , . . . , ๐๐ ] (1)
index context rule premises arguments
A step consists of an index ๐ โ I where I is a countable infinite set of indices (e.g. a0, t1), and a
clause of literals ๐1 , . . . , ๐๐ representing an ๐-ary disjunction. A proof rule โ depends on a possibly
empty set of premises { ๐1 , . . . , ๐๐ } โ I that refer to earlier steps. A rule might also depend on a
list of arguments [๐1 , . . . , ๐๐ ] where each argument ๐๐ is either a term or a pair (๐ฅ๐ , ๐ก๐ ) where ๐ฅ๐
is a variable and ๐ก๐ is a term. The interpretation of the arguments is rule specific. The context ฮ is
a list ๐1 , . . . , ๐๐ where each element ๐๐ is either a variable or a variable-term tuple denoted ๐๐ โฆ ๐ก๐ .
Therefore steps with a non-empty context contain variables ๐๐ in ๐๐ that can be substituted by ๐ก๐ . Proof
rules โ are structured around the introduction of theory lemmas and resolution which captures
hyper-resolution on ground first-order clauses.
We now have the key components to explain the guiding proof Listing 1 that consists of seven steps.
The proof starts with several assume steps a0, a1, a2 that restate the assertions from the input problem.
Step t1 introduces with the rule equiv_pos2 a tautology of the general form ยฌ(๐1 โ ๐2 )โจ ยฌ๐1 โจ ๐2 .
Steps t2, t3, t4 use earlier premises that correspond to previous steps. Step t2 prove ๐(๐) โ ๐(๐)
by congruence (rule cong ) by using the assumption a1. Step t3 derives ๐(๐) after applying the
resolution rule of propositional logic to the premises t1, t2, a0. Lastly, the step t4 concludes
the proof by generating the empty clause โฅ, concretely denoted as (cl) in Listing 1. Notice that the
contexts ฮ of each step are all empty in this proof.
Unfortunately, Alethe proofs provided by SMT solvers such as veriT and CVC5 can be challenging
to reconstruct in a proof assistant. For instance, the order of literals in the clauses is not determined,
symmetry of equality is sometimes used implicitly, and pivots for the resolution proof rule are not
indicated explicitly.
2.2. Elaborated proof with Carcara
Carcara provides an elaboration mechanism for Alethe proofs and adds details that can make proof
reconstruction easier. For example, one possible elaboration is to mention the pivot(s) for resolution
steps. In our guiding example, Carcara elaborates part of the proof of Listing 1 by exposing the pivots
of the steps t3 and t4 as arguments of resolution proof rule with a Boolean flag to indicate if the
negation of the pivot is in the first or second premise:
(step t3 (cl (p b)) :rule resolution :premises (t1 t2 a0)
:args ((= (p a) (p b)) false (p a) false))
(step t4 (cl) :rule resolution :premises (a2 t3) :args ((p b) false))
Carcara can also shorten proofs by removing some trivial transient steps and rewriting the order
of literals in a clause. The list of elaborations performed by Carcara can be found in [5, ยง3.2]. Our
translation of Alethe proofs into Lambdapi is based on the elaboration performed by Carcara, relying
on it for pre-checking the proof and applying the transformations for making it explicit.
3. Proof reconstruction
We now describe our embedding of Alethe in Lambdapi, and how we extended Carcara with a new
module that can export elaborated Alethe proofs to Lambdapi. Our work applies to input problems
expressed in the logics UFLIA, UFNIA or their sub-logics.
Notation (Alethe signature and judgment). We use ฮ instead of ฮฃ to denote the SMT signature context to
๐ฎ
avoid conflicts with the Lambdapi signature context. Therefore, ฮ represents the set of SMT sort symbols,
โฑ ๐ณ
ฮ the set of function symbols, and ฮ the set of variables. We refer to step and assume as commands or
sometimes as Alethe judgments.
3.1. Lambdapi
Lambdapi is an implementation of ๐ฮ modulo theory (๐ฮ / โก) [15], an extension of ๐ฮ , i.e., the
Edinburgh Logical Framework [16], a simply typed ๐-calculus with dependent types. ๐ฮ / โก adds
user-defined higher-order rewrite rules. Its syntax is given by
Universes ๐ข โถโถ= TYPE โฃ KIND
Terms ๐ก, ๐ฃ, ๐ด, ๐ต, ๐ถ โถโถ= ๐ โฃ ๐ฅ โฃ ๐ข โฃ ฮ ๐ฅโถ ๐ด. ๐ต โฃ ๐ ๐ฅโถ ๐ด. ๐ก โฃ ๐ก ๐ฃ
Contexts ฮ โถโถ= โจโฉ โฃ ฮ, ๐ฅโถ ๐ด
Signatures ฮฃ โถโถ= โจโฉ โฃ ฮฃ, ๐โถ ๐ถ โฃ ฮฃ, ๐ โถ= ๐ก โถ ๐ถ โฃ ฮฃ, ๐ก โช ๐ฃ
where ๐ is a constant and ๐ฅ is a variable (ranging over disjoint sets), ๐ถ is a closed term. Universes are
constants used to verify if a type is well-formed โ more details can be found in [16, ยง2.1]. ฮ ๐ฅโถ ๐ด. ๐ต
is the dependent product, and we write ๐ด โ ๐ต when ๐ฅ does not appear free in ๐ต, ๐ ๐ฅโถ ๐ด. ๐ก is an
abstraction, and ๐ก ๐ฃ is an application. Signature ฮฃ (global context) and contexts ฮ (local contexts) are
finite sequences and โจโฉ denotes the empty sequence. Assumptions are written ๐โถ ๐ถ, indicating that ๐ is
of type ๐ถ. Definitions in ฮฃ are written ๐ โถ= ๐ก โถ ๐ถ, indicating that ๐ has the value ๐ก and type ๐ถ. In a
Lambdapi typing judgment ฮ โขฮฃ ๐กโถ ๐ด a term ๐ก has type ๐ด in the context ฮ and the signature ฮฃ.
A signature may contain rewrite rules ๐ก โช ๐ฃ such that ๐ก = ๐ ๐ฃ1 . . . ๐ฃ๐ with ๐ a constant. The relation
โช๐ฝฮฃ is generated by ๐ฝ-reduction and by the rewrite rules of ฮฃ. Conversion โก๐ฝฮฃ is the reflexive,
symmetric, and transitive closure of โช๐ฝฮฃ . Let โช๐ฝฮฃ be the reflexive and transitive closure of โช๐ฝฮฃ . The
โ
relation โช๐ฝฮฃ must be confluent, i.e., whenever ๐ก โช๐ฝฮฃ ๐ฃ1 and ๐ก โช๐ฝฮฃ ๐ฃ2 , there exists a term ๐ค such that
โ โ
๐ฃ1 โช๐ฝฮฃ ๐ค and ๐ฃ2 โช๐ฝฮฃ ๐ค, and it must preserve typing, i.e., whenever ฮ โขฮฃ ๐ก โถ ๐ด and ๐ก โช๐ฝฮฃ ๐ฃ then
โ โ
ฮ โขฮฃ ๐ฃ โถ ๐ด [17].
The typing rules in ๐ฮ / โก are similar to those of ๐ฮ [16, ยง2], except for the additional rule (Conv)
that identifies types modulo โก๐ฝฮฃ instead of just modulo โก๐ฝ .
ฮ, โขฮฃ ๐ต โถ ๐ข ฮ โขฮฃ ๐ก โถ ๐ด ๐ด โก๐ฝฮฃ ๐ต
Conv
ฮ โขฮฃ ๐ก โถ ๐ต
3.2. A Prelude Encoding for Alethe
Definition 1 (Prelude Encoding). Our signature context ฮฃ contains the following definitions and rewrite
rules furnished by the standard library of Lambdapi that we use to encode Alethe proofs:
1 constant symbol Set : TYPE;
2 injective symbol El : Set โ TYPE;
3 constant symbol ใ : Set โ Set โ Set;
4 rule El ($x ใ $y) โช El $x โ El $y;
5 symbol o: Set;
6 constant symbol Prop : TYPE;
7 injective symbol Prf : Prop โ TYPE;
8 rule El o โช Prop;
The constants Set and Prop (lines 1 and 6) are type universes โร la Tarskiโ [18, ยงUniverses] in ๐ฮ / โก.
The type Set represents the universe of small types. We characterize small types as a subclass of types
for which we can define equality. SMT sorts are represented in ๐ฮ / โก as elements of type Set. Since
elements of type Set are not types themselves, we also introduce a decoding function Elโถ Set โ TYPE
which interpret SMT sorts as ๐ฮ / โก types. Thus, we represent the terms of sort Bool of SMT by
elements of type El ๐. The constructor ใ is used to encode SMT functions and predicates.
The type Prop represents the universe of propositions in ๐ฮ / โก. Like Set, elements of type Prop are
not types themselves, so we introduce the decoding function Prfโถ Prop โ TYPE. By analogy with the
Curry-de-Brujin-Howard isomorphism, it embeds propositions into types, mapping each proposition ๐ด
to the type Prf ๐ด of its proofs. Hence, Bool formulas of SMT are rewritten to ๐ฮ / โก propositions with
the rewrite rule defined in line 8. Thereafter, we add the following definitions to those of the standard
library:
1 symbol Bool โ o;
2 injective symbol Index [a: Set] : N โ El a;
For convenience, we define an alias Bool for ๐. The function Index is used to assign to SMT
translated terms a unique identifier, so to compare that two terms are equal it is sufficient to compare
their identifier. In Lambdapi syntax, an argument enclosed in square brackets e.g. [a] is declared
implicit.
3.3. Classical connectives, quantifiers and facts
Since SMT-solvers are based on classical logic, we use the constructive connectives and quantifiers
from the Lambdapi standard library and define the classical ones from them using the double-negation
translation [19] as a definition.
๐
1 injective symbol Prf p โ Prf (ยฌยฌ p);
๐
2 symbol โจ p q โ ยฌยฌ p โจ ยฌยฌ q;
3 constant symbol = [a] : El a โ El a โ Prop;
๐
Therefore, Alethe classical proofs will be decoded by the decoding function Prf (line 1), defined as
intuitionistic proof Prf of the doubly negated predicate. Similarly, classical connectives and quantifiers
will be defined as illustrated in line 2. Since we want to define equality restricted to small types, equality
has a single implicit parameter a: Set and two indices of type El ๐.
We prove the law of excluded middle and add the proposition of Boolean extensionality stating that
classical equivalence coincides with equality over Booleans.
๐ ๐
constant symbol classic [p] : Prf (p โจ ยฌ p);
๐ ๐ ๐
constant symbol prop_ext [p: El o] [q: El o]: Prf (p โ q) โ Prf (p = q);
3.4. Translating functions
We now describe how we reconstruct input problem definitions and an Alethe proof with Carcara. The
translation of Alethe to Lambdapi is built around four functions:
๐ฎ
โข ๐ฎ maps sorts from ฮ to ฮฃ types,
โข โฑ translates terms and formulas to ๐ฮ / โก terms,
๐ฎ โฑ
โข ๐ translates declarations of sorts and functions in ฮ and ฮ into constants in ฮฃ,
โข ๐(๐1 . . . ๐๐ ) translates a list of commands ๐1 . . . ๐๐ of the form ๐. ฮ โท ๐ (โ ๐ )[๐ด] to typing
judgments ฮ โขฮฃ ๐ โถ= ๐ โถ Prf (๐ ), where Prf represents the proof of a clause and will be
โข โข
introduced in the next section.
In the following we will only present examples of the application of these functions on Listing 1.
๐ฎ
Function ๐ฎ is a mapping function from sort in ฮ to ฮฃ type. Sorts Bool and Int are mapped to
predefined Bool and int types. User sorts such as U or sort predicate (U Bool) are mapped to Set
and Set โ Bool respectively.
The function โฑ is recursively defined on the constructors for Alethe terms and formulas. The logical
connectives of SMT are mapped to the classical operators presented in the previous section. For example,
๐ ๐
the formula (or x y (not z)) is translated into the term (x โจ y โจ ยฌz). Terms are translated
to lambda terms, e.g. (f x y) is translated to f x y. The equality of Alethe noted ๐ฅ โ ๐ฆ is translated
to ๐ฅ = ๐ฆ.
We translate declarations (declare-sort and declare-fun) to Lambdapi symbols by iterating
over elements in context ฮ and using the function ๐. This function creates a constant in the con-
text ฮฃ for each sort and function declared. To illustrate how context embedding operates, the code
below depicts the translation of sort and function declarations of our guiding example Listing 1. The
๐ฎ โฑ
context ฮ for our example is as follows: ฮ = {๐, Bool} with ๐๐ = {๐ โฆ 0, Bool โฆ 0}, ฮ =
{(๐, ๐ ), (๐, ๐ ), (๐, ๐ Bool)} and ๐๐ the map of sorts arity.
symbol U : Set;
symbol a : El U โ Index 0;
symbol b : El U โ Index 1;
symbol p : El (U ใ Bool) โ Index 2;
Remark (assert statement). The assertions at the end of Listing 1 remain untranslated initially, as they
will undergo translation when we process the assume command.
3.5. Embedding Clauses
Before presenting the function ๐, we have to outline the challenge of formalizing the Alethe resolution
rule in ๐ฮ / โก. Alethe identifies clause (cl ๐1 , . . . , ๐๐ ) in Equation (1) as a set of literals which can be
interpreted as an ๐-ary disjunction of literals. Following this, an arbitrary clause such as ๐๐ (๐1 ๐2 ๐3 ๐4 )
๐ ๐ ๐
will be then translated into ๐1 โจ (๐2 โจ (๐3 โจ ๐4 )) by our function โฑ. As mentioned in Section 2, Alethe
identifies clauses that differ only in the order of literals. Therefore, the concatenation of two clauses
(what is happening in the conclusion of resolution) need not unify with the translated clause of the
step given by โฑ. For example, taking 3 arbitrary steps:
๐ด. โท (cl ๐ฅ1 , ๐ฅ2 , ๐ฅ3 )(..)[..]
๐ต. โท (cl ๐ฆ2 , ยฌ๐ฅ1 , ๐ฆ3 )(..)[..]
๐ถ. โท (cl ๐ฅ2 , ๐ฅ3 , ๐ฆ2 , ๐ฆ3 )(resolution A B)[(๐ฅ1 true)]
๐
Considering the interpretation of clause as disjunction we obtain the concatenation as follows ((๐ฅ2 โจ
๐ ๐
๐ฅ3 ) โจ (๐ฆ2 โจ ๐ฆ3 )) with the conclusion of resolution inference rule traditionally formalized as
๐ ๐ ๐
๐ฅ โจ ๐ ; ยฌ๐ฅ โจ ๐ โข ๐ โจ ๐. However, the clause in step ๐ถ will be translated as (๐ฅ2 โจ (๐ฅ3 โจ (๐ฆ2 โจ ๐ฆ3 ))),
hence we obtain two different representations of the clause. Moreover, the pivot ยฌ๐ฅ1 in step B does
not appear at the head of the clause whereas the inference rule for resolution expects the pivot to be
at the head. Thus, the resolution of clauses makes the structure of clauses involve reasoning modulo
associativity and commutativity. To address the problem of associativity, we provide a structure of
clauses with a canonical representation. We define clauses as lists ร la Church:
1 constant symbol Clause : TYPE;
2 symbol โ : Clause; // Nil
3 injective symbol โ : Prop โ Clause โ Clause; // Cons head tail
4
๐
5 symbol โ_to_โจ _rw : Clause โ Prop;
๐ ๐ ๐
6 rule โ_to_โจ _rw ($x โ $y) โช $x โจ (โ_to_โจ _rw $y)
๐
7 with โ_to_โจ _rw โ โช โฅ;
8
9 symbol ++ : Clause โ Clause โ Clause; // concatenation
10 rule โ ++ $m โช $m
11 with ($x โ $l) ++ $m โช $x โ ($l ++ $m);
12
โข ๐ ๐
13 injective symbol Prf cl โ Prf (โ_to_โจ _rw cl); // Proof of clause
At lines 1 to 3 above we define the Clause type with the two constructors similar to the common
๐
algebraic data type of lists. The rewrite rules โ_to_โจ _rw at lines 5-7 rewrite a clause into a disjunction
terminating with โฅ symbolizing the empty list constructor. The symbol ++ defined at lines 9-11 computes
the concatenation of two clauses. To solve the issue of commutativity when Alethe performs a resolution,
we introduce intermediate lemmas of rearrangement of a clause where the pivot is moved, so pivots
appear at the head of the clause. A clause proof will be encoded as a proof of Prf ๐1 , . . . , ๐๐ defined as
โข
a classical proof of disjunctions of literals with a trailing โฅ.
3.6. Translation of Alethe proofs
In the previous sections, we outlined how we embed Alethe logic in ๐ฮ / โก and how we translate the input
problem definitions by using the function ๐. We now provide an overview of how we reconstruct the
commands with function ๐. Informally, the function represents each command ๐.ฮ โท ๐1 . . . ๐๐ (๐
๐ )[๐ด]
as an intermediate lemma ฮ โขฮฃ ๐ โถ= ๐ โถ Prf (โฑ(๐1 ) โ โ
โ
โ
โ โฑ๐๐ โ โ )) where the proof term
โข
๐ is constructed depending on the rule ๐
, the premises ๐ and arguments ๐ด. For example, if ๐
=
๐ ๐
equiv_pos2, we apply our generic proved lemma equiv_pos2โถ ฮ ๐, ฮ ๐, ยฌ(๐ = ๐) โจ ยฌ๐ โจ ๐ to
produce a proof term for judgment ๐. In the case that ๐
= resolution, we refashion ๐-ary resolution
into a chain of binary resolution steps. To do that, we fold in premises ๐ from left to right, combining
intermediate lemmas to conclude the clause ๐1 . . . ๐๐ of step ๐.
To illustrate the result of our main function ๐, we introduce the translation of Listing 1 proof. In the
code below, all the assume commands are transformed as constants in ฮฃ by the function ๐. They are
treated as axioms and correspond to the asserts of the input problem.
โข
1 constant symbol a0 : Prf (p a โ โ );
โข
2 constant symbol a1 : Prf (a = b โ โ );
โข
3 constant symbol a2 : Prf (ยฌ p b โ โ );
4
๐
5 opaque symbol qf_unsat_05_predcc : Prf (ยฌ (p b)) โ
6 begin
7 apply contradiction; assume goal;
โข
8 have t1 : Prf ((ยฌ (((p a) = (p b)))) โ (ยฌ ((p a))) โ (p b) โ โ ) { apply equiv_pos2; };
โข ๐ ๐ โข
9 have t2 : Prf (((p a) = (p b)) โ โ ) { apply โจ ๐1 ; apply feq p (Prf ๐ a1); };
โข
10 have t3 : Prf ((p b) โ โ ) {
โข
11 have t1_t2 : Prf ((ยฌ ((p a))) โ (p b) โ โ ) { apply resolution๐ _ _ _ t1 t2; };
โข
12 have t1_t2_a0 : Prf ((p b) โ โ ) { apply resolution๐ _ _ _ t1_t2 a0; };
13 refine t1_t2_a0;
14 };
โข โข
15 have t4 : Prf โ { have a2_t3 : Prf โ { apply resolution๐ _ _ _ a2 t3; }; refine a2_t3;
};
16 apply t4;
17 end;
Each judgment translated as an intermediate lemma ฮ โขฮฃ ๐ โถ= ๐ โถ Prf (โฑ(๐1 ) โ โ
โ
โ
โ โฑ(๐๐ ) โ โ ))
โข
generated by ๐ is represented by the tactic have ๐ฅโถ ๐ก of Lambdapi that applies the cut rule. We wrap all
the translated steps in a lemma symbol where the last assert is the type and the last step (๐ก4 here)
๐ ๐
should conclude Prf (โฅ) and Prf โ โก๐ฝฮฃ Prf โฅ. We derive a proof by contradiction because
โข
SMT solvers try to prove that the negation of the formula is unsatisfiable. The goal hypothesis assumed
line 3 is left unused because we use its equivalent constant a2 coming from the translation of assume
commands by ๐.
4. Soundness of the translation
Intuitively, proving soundness of the translation amounts to showing that for any Alethe judgment ๐,
the translation ๐(๐) produces a well-typed proof term whose type corresponds to the clause asserted
by ๐. This is formally expressed by the following theorem.
Theorem 1 (Soundness). For any Alethe judgment ๐ = ๐. ฮ โท ๐1 . . . ๐๐ (โ ๐ )[๐ด] the translation ๐(๐)
produce the typing judgment ฮ โขฮฃ ๐ โถ= ๐ โถ Prf (โฑ(๐1 ) โ โ
โ
โ
โ โฑ(๐๐ ) โ โ ) that is well-typed in
โข
context ฮ with the signature context ฮฃ.
5. Evaluation
1
Our benchmark is composed of files from the SMT-LIB benchmark using the (sub-)logic UFNIA, and
+
proof obligations from TLAPS SMT backend verifier. TLA [20] is a language based on set theory and a
linear-time temporal logic for formally specifying and verifying systems, in particular concurrent and
distributed algorithms. Its interactive proof environment TLAPS [21] relies on users guiding the proof
effort, it integrates automatic backends, including SMT solvers to discharge proof obligations [22, 23].
+
A particular goal of our development was the reconstruction of TLA theorems in Lambdapi. The
+
Allocator module [24] is a case study for the specification and analysis of reactive systems in TLA . The
SMT proofs for the individual steps in this case study contain between 20 and 600 steps. The Cantor
1
https://smtlib.cs.uiowa.edu/benchmarks.shtml
Name Logic Samples Reconstructed Timeout Memout
Allocator UFNIA 36 31 3 2
Cantor UF 11 11 0 0
Rodin QF_UF 34 34 0 0
TypeSafe QF_UF 3 3 0 0
Table 1
Benchmarks results with time limit: 1200 seconds and memory limit: 30 GB
benchmark is the TLAPS proof of Cantorโs theorem that asserts that there is no surjection from any set
to its powerset. The SMT proofs for the corresponding proof obligations contain between 10 and 100
steps. Rodin and TypeSafe are samples from the SMT-LIB benchmark that we can reconstruct. The time
needed for translation to Lambdapi by Carcara is negligibly small in this benchmark. For now, our work
is not able to reconstruct larger samples (up to 70k steps) in Goel, PEQ, or Sledgehammer benchmarks
from SMT-LIB repository because we are facing scalability problems such as high memory consumption
and our Lambdapi checker is running only on a single process. Also, we can not for now benefit from
term sharing because Lambdapi can not create local definitions in a proof, but we intend to implement
this feature. However, we believe that our encoding should be able to reconstruct these proofs if we
can scale because only the volume of steps and the size of terms increase but not the complexity. For
benchmarks using the LIA (sub-)logic, we are currently only reconstructing those proof steps where
arithmetic reasoning does not play an essential role, beyond simplification.
Our work revealed that some proof obligation in Allocator and Cantor failed to be reconstructed, i.e.,
the proof found by the SMT-solver had become incorrect after elaboration by Carcara. This revealed
multiple bugs in the Carcara checker and proof elaborator that have since been corrected. Moreover,
+
one reconstruction failure helped to detect that one of the set theory axioms of TLA was incorrectly
encoded in SMT, and this issue has also been fixed.
6. Conclusion and perspectives
We presented an extension of Carcara to reconstruct Alethe proofs in the foundational proof assistant
Lambdapi. Currently, this extension can reconstruct some SMT proofs that originate from the TLAPS
proof assistant, as well as some samples from the SMT-lib benchmarks in the UF (sub-)logic. Failure to
reconstruct some proofs revealed bugs in the Carcara checker and in the SMT encoding of set theory in
the TLAPS proof assistant that have since been corrected, thus demonstrating the value of independent
proof checking.
At this point in time, our proof checker is limited to handling relatively small proofs due to scalability
issues. We plan to address them by following the approach in [25, ยง4] that translates HOL-Light to
Lambdapi, using multiple processes for parallel proof checking. The idea is to generate individual files
corresponding to disjoint segments of a proof, compute the dependencies between those segments,
check each file in a separate process, and finally merge all the results. Furthermore, we are restricted
to proofs without arithmetic reasoning. In the future, we intend to support reconstruction for linear
integer arithmetic. Lambdapi does not have a built-in decision procedure for it, but we consider using
Zenon Modulo [26], a tableau-based first-order automated theorem prover that can generate proof
certificates in Lambdapi.
A further perspective that we plan to address in future work is to exploit Lambdapiโs capability for
exporting proofs to other proof assistants that will then be able to benefit from automation through
SMT solving.
References
[1] R. Brummayer, A. Biere, Fuzzing and delta-debugging SMT solvers, in: Proceedings of the 7th
International Workshop on Satisfiability Modulo Theories, SMT โ09, 2009.
[2] S. Bรถhme, T. Weber, Fast LCF-style proof reconstruction for Z3, in: M. Kaufmann, L. C. Paulson
(Eds.), First Intl. Conf. Interactive Theorem Proving (ITP 2010), volume 6172 of LNCS, Springer,
2010, pp. 179โ194.
[3] H.-J. Schurr, M. Fleury, M. Desharnais, Reliable reconstruction of fine-grained proofs in a proof
assistant, in: A. Platzer, G. Sutcliffe (Eds.), Automated Deduction โ CADE 28, Springer International
Publishing, Cham, 2021, pp. 450โ467.
[4] G. Hondet, F. Blanqui, The New Rewriting Engine of Dedukti, in: 5th International Conference on
Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International
Proceedings in Informatics (LIPIcs), Schloss Dagstuhl โ Leibniz-Zentrum fรผr Informatik, 2020, pp.
35:1โ35:16.
[5] B. Andreotti, H. Lachnitt, H. Barbosa, Carcara: An efficient proof checker and elaborator for
SMT proofs in the Alethe format, in: Tools and Algorithms for the Construction and Analysis
of Systems: 29th International Conference, TACAS 2023, Springer-Verlag, 2023, p. 367โ386. URL:
https://doi.org/10.1007/978-3-031-30823-9_19. doi:10.1007/978-3-031-30823-9_19.
[6] H. Barbosa, A. Reynolds, G. Kremer, H. Lachnitt, A. Niemetz, A. Nรถtzli, A. Ozdemir, M. Preiner,
A. Viswanathan, S. Viteri, et al., Flexible proof production in an industrial-strength SMT solver,
in: International Joint Conference on Automated Reasoning, Springer International Publishing
Cham, 2022, pp. 15โ35.
[7] J. C. Blanchette, S. Bรถhme, L. C. Paulson, Extending Sledgehammer with SMT solvers, in: N. S.
Bjรธrner, V. Sofronie-Stokkermans (Eds.), 23rd Intl. Conf. Automated Deduction (CADE-23), volume
6803 of LNCS, Springer, Wroclaw, Poland, 2011, pp. 116โ130.
[8] ล. Czajka, C. Kaliszyk, Hammer for Coq: Automation for dependent type theory, Journal of
Automated Reasoning 61 (2018) 423โ453.
[9] L. Czajka, A Shallow Embedding of Pure Type Systems into First-Order Logic, in: 22nd International
Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International
Proceedings in Informatics (LIPIcs), 2018, pp. 9:1โ9:39.
[10] H. Barbosa, J. C. Blanchette, M. Fleury, P. Fontaine, Scalable fine-grained proofs for formula
processing, Journal of Automated Reasoning 64 (2020) 485โ510.
[11] M. Armand, G. Faure, B. Grรฉgoire, C. Keller, L. Thery, B. Werner, A Modular Integration of
SAT/SMT Solvers to Coq through Proof Witnesses, in: Jouannaud, Jean-Pierre, Shao, Zhong (Eds.),
First Intl. Conf. Certified Programs and Proofs (CPP 2011), volume 7086 of LNCS, Springer, Lenting,
Taiwan, 2011, pp. 135โ150. doi:10.1007/978-3-642-25379-9\_12.
[12] F. Besson, Fast reflexive arithmetic tactics the linear case and beyond, in: T. Altenkirch, C. McBride
(Eds.), Intl. Workshop Types for Proofs and Programs (TYPES 2006), LNCS, Springer, 2006, pp.
48โ62.
[13] H. Barbosa, M. Fleury, P. Fontaine, H.-J. Schurr, The Alethe Proof Format An Evolving Specification
and Reference, 2024. https://verit.gitlabpages.uliege.be/alethe/specification.pdf.
[14] C. Barrett, P. Fontaine, C. Tinelli, The SMT-LIB Standard: Version 2.6, Technical Report, Department
of Computer Science, The University of Iowa, 2017. URL: https://smtlib.cs.uiowa.edu/papers/
smt-lib-reference-v2.6-r2021-05-12.pdf, available at www.SMT-LIB.org.
[15] D. Cousineau, G. Dowek, Embedding pure type systems in the Lambda-Pi-Calculus Modulo, in:
Typed Lambda Calculi and Applications, Springer, Berlin, Heidelberg, 2007, pp. 102โ117.
[16] R. Harper, F. Honsell, G. D. Plotkin, A framework for defining logics, J. ACM 40 (1993) 143โ184.
URL: https://api.semanticscholar.org/CorpusID:13375103.
[17] F. Blanqui, Type Safety of Rewrite Rules in Dependent Types, in: 5th International Conference on
Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International
Proceedings in Informatics (LIPIcs), 2020, pp. 13:1โ13:14.
[18] P. Martin-Lรถf, Intuitionistic Type Theory, volume 1 of Studies in proof theory, Bibliopolis, 1980.
[19] G. Dowek, On the definition of the classical connectives and quantifiers, 2016.
arXiv:1601.01782.
[20] L. Lamport, Specifying Systems, Addison-Wesley, Boston, Mass., 2002.
+
[21] D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, H. Vanzetto, TLA proofs, in:
D. Giannakopoulou, D. Mรฉry (Eds.), 18th Intl. Symp. Formal Methods (FM 2012), volume 7436 of
LNCS, Springer, 2012, pp. โ47โ154.
+
[22] S. Merz, H. Vanzetto, Automatic verification of TLA proof obligations with SMT solvers, in: Logic
for Programming, Artificial Intelligence, and Reasoning - 18th , LPAR-18, volume 7180 of Lecture
Notes in Computer Science, Springer, 2012, pp. 289โ303. doi:10.1007/978-3-642-28717-6\_23.
+
[23] R. Defournรฉ, Encoding TLA proof obligations safely for SMT, in: Rigorous State-Based Methods
- 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings,
volume 14010 of Lecture Notes in Computer Science, Springer, 2023, pp. 88โ106. URL: https://doi.
org/10.1007/978-3-031-33163-3_7. doi:10.1007/978-3-031-33163-3\_7.
+
[24] S. Merz, The Specification Language TLA , in: D. Bjรธrner, M. Henson (Eds.), Logics of specification
languages, Springer, 2004, pp. 401โ452.
[25] F. Blanqui, Translating HOL-Light proofs to Coq, in: 25rd Intl. Conf. Logic for Programming,
Artificial Intelligence and Reasoning (LPAR-25), EPiC Series in Computing, Mauritius, 2024, p. 18
pages.
[26] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant, Zenon Modulo: When Achilles
Outruns the Tortoise using Deduction Modulo, in: LPAR - Logic for Programming Artificial
Intelligence and Reasoning - 2013, volume 8312 of LNCS, Springer, 2013, pp. 274โ290. doi:10.
1007/978-3-642-45221-5\_20.