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.
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).
Coq PVS vodk lean
2dk
KaMeLo K-framework
SMT
C a r c a r a Lambdapi Dedukti o n o j a r
K Matita isabelle_dk agda2dk
Isabelle
Agda hol2dk
HOL
Zenon and ArchSAT
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.
CoqHammer [
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 [
Carcara [
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.
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
An Alethe proof is a list of steps representing forward reasoning whose general form is as follows: clause . Γ ▷ 1, . . . ,
( ℛ 1, . . . , ) [1, . . . , ] index context rule premises arguments (1)
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.
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.
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))
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 ( Π /≡) [
∶∶= TYPE ∣ KIND , , , , ∶∶= ∣ ∣ ∣ Π ∶ . ∣ ∶ . ∣ Γ ∶∶= ⟨⟩ ∣ Γ , ∶ Σ ∶∶= ⟨⟩ ∣ Σ , ∶ ∣ Σ , ∶= ∶ ∣ Σ , ↪ 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 ifnite 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
Γ ⊢Σ ∶ [
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 ≡ .
Γ , ⊢Σ ∶ Γ ⊢Σ ∶
≡ Σ Γ ⊢Σ ∶
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: constant symbol Set : TYPE; injective symbol El : Set → TYPE; constant symbol 〜 : Set → Set → Set; rule El ($x 〜 $y) ↪ El $x → El $y; symbol o: Set; constant symbol Prop : TYPE; injective symbol Prf : Prop → TYPE; rule El o ↪ Prop;
The constants Set and Prop (lines 1 and 6) are type universes “à la Tarski” [18, §Universes] in Π /≡.
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
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: symbol Bool ≔ o; injective symbol Index [a: Set] : N → El a;
translated terms a unique identifier, so to compare that two terms are equal it is suficient 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. injective symbol Prf p ≔ Prf (¬¬ p); symbol ∨ p q ≔ ¬¬ p ∨ ¬¬ q; 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 .
constant symbol classic [p] : Prf (p ∨ ¬ p); constant symbol prop_ext [p: El o] [q: El o]: Prf (p ⇔ q) → Prf (p = q);
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.
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.
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.
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 difer 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 diferent 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: symbol ⟇_to_∨_rw : Clause → Prop; rule ⟇_to_∨_rw ($x ⟇ $y) ↪ $x ∨ (⟇_to_∨_rw $y) with ⟇_to_∨_rw ■ ↪ ⊥; symbol ++ : Clause → Clause → Clause; // concatenation rule ■ ++ $m ↪ $m with ($x ⟇ $l) ++ $m ↪ $x ⟇ ($l ++ $m); 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 ⊥.
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.
constant symbol a0 : Prf• (p a ⟇ ■ ); constant symbol a1 : Prf• (a = b ⟇ ■ ); constant symbol a2 : Prf• (¬ p b ⟇ ■ ); opaque symbol qf_unsat_05_predcc : Prf (¬ (p b)) ≔ begin apply contradiction; assume goal; have t1 : Prf• ((¬ (((p a) = (p b)))) ⟇ (¬ ((p a))) ⟇ (p b) ⟇ ■ ) { apply equiv_pos2; }; have t2 : Prf• (((p a) = (p b)) ⟇ ■ ) { apply ∨1; apply feq p (Prf• a1); }; have t3 : Prf• ((p b) ⟇ ■ ) { have t1_t2 : Prf• ((¬ ((p a))) ⟇ (p b) ⟇ ■ ) { apply resolution _ _ _ t1 t2; }; have t1_t2_a0 : Prf• ((p b) ⟇ ■ ) { apply resolution _ _ _ t1_t2 a0; }; refine t1_t2_a0; }; have t4 : Prf• ■ { have a2_t3 : Prf• ■ { apply resolution _ _ _ a2 t3; }; refine a2_t3; }; apply t4; 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
line 3 is left unused because we use its equivalent constant a2 coming from the translation of assume commands by .
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 Σ .
Our benchmark is composed of files from the SMT-LIB benchmark 1 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 efort, 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
Name Allocator Cantor Rodin TypeSafe
Logic UFNIA
UF QF_UF QF_UF 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.
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.
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.
issues. We plan to address them by following the approach in [25, §4] that translates HOL-Light to
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
exporting proofs to other proof assistants that will then be able to benefit from automation through
[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:
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,
pages. [26] D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, O. Hermant, Zenon Modulo: When Achilles
1007/978-3-642-45221-5\_20.