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.