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 independently, 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.

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 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.

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.

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. 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].

An Alethe proof is a list of steps representing forward reasoning whose general form is as follows:

index context clause 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

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 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.

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: 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.

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.

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

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, 𝛽Σ 𝑤, 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 ≡ 𝛽 . 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 constructoris 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:

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.

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.

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.

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 Σ,

, 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 context Σ 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. 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.

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:

Considering the interpretation of clause as disjunction we obtain the concatenation as follows

) with the conclusion of resolution inference rule traditionally formalized as 𝑥 ∨ 𝑌 ; ¬𝑥 ∨ 𝑍 ⊢ 𝑌 ∨ 𝑍. However, the clause in step 𝐶 will be translated as

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: 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 ⊥.

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

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. 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.

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.