Logos Checker

A Verifiable Proof Checker for SMT Solvers

Logos is a verifiable proof checker for SMT written in Lean. It is an executable checker that additionally has a correctness specification of its soundness, which depends on a complete definition of SMT-LIB semantics in Lean.

It is a meta-checker, that is, the proof rules it uses are flexible. The proof rules currently used by Logos are automatically generated from the current definition of the Cooperating Proof Calculus (CPC) (https://github.com/cvc5/cvc5/blob/main/proofs/eo/cpc/Cpc.eo). This compilation depends on plugins of the proof checker Ethos (https://github.com/cvc5/ethos), available on a development branch.

Building the Logos checker

lake build logos

Note that logos takes roughly 3.5 minutes to build currently.

To run the same checks as CI locally, use:

bash scripts/run-ci.sh

Using the Logos checker

lake exe logos [script]

where script is the name of a file containing an evaluation statement to be read by the Lean parser. An example of such a file is the following:

import Cpc.Logos
open Eo
def t1 : Term := (Term.UConst 1 Term.Int)
def t2 : Term := (Term.UConst 2 Term.Int)
def t3 : Term := (Term.Apply Term.eq t2)
def t4 : Term := (Term.Apply t3 t1)
def t5 : Term := (Term.Apply Term.eq t1)
def t6 : Term := (Term.Apply t5 t2)
def t7 : Term := (Term.Apply Term.not t6)
def s0 : CState := logos_init_state
def s1 : CState := (logos_invoke_assume s0 t4)
def s2 : CState := (logos_invoke_assume s1 t7)
def s3 : CState := (logos_invoke_cmd s2 (CCmd.step CRule.symm CArgList.nil (CIndexList.cons 0 CIndexList.nil)))
def s4 : CState := (logos_invoke_cmd s3 (CCmd.step CRule.contra CArgList.nil (CIndexList.cons 2 (CIndexList.cons 0 CIndexList.nil))))
#eval!
(logos_state_is_refutation s4)

Such scripts can be generated by (a development branch of) cvc5 using the command line options --dump-proofs --proof-format=cpc-logos. Proof checking succeeds if executing logos on this files returns true.

Logos assumes that scripts define a state that is constructed iteratively starting from logos_init_state, followed by a sequence of logos_invoke_assume commands (the assumptions of the proof), followed by a sequence of logos_invoke_cmd commands. A state is a refutation if the last proven formula was false and if all assumptions introduced via assume_push commands are closed by corresponding step_pop commands. The semantics of these commands mimics the Eunoia logical framework; for details see https://github.com/cvc5/ethos/blob/main/user_manual.md.

Note that Logos has not (yet) been optimized for performance, so it is significantly slower that performant proof checkers for SMT.

Correctness

Logos additionally has an (unproven) correctness specification. This is in two parts. First, the file ./cpc/SmtModel.lean formalizes a model semantics of SMT-LIB. Second, the file ./cpc/Spec.lean defines a correspondence between Eunoia terms and SMT-LIB terms and a theorem (to prove) for each of the proof rules. It also contains a final theorem stating the correctness of the overall checker.

The SMT-LIB formalization ./cpc/SmtModel.lean includes several non-standard extensions of SMT-LIB (e.g. the theory of sets and the theory of sequences). It additionally contains operators that are helpful in defining the semantics of existing operators. This includes total versions of partial arithmetic operators.