Proof format: Cooperating Proof Calculus 

Using option proof-format-mode=cpc , cvc5 outputs proofs in the Cooperating Proof Calculus proof format.

This calculus was designed to faithfully represent cvc5’s internal reasoning. As a disclaimer, this means that it treats certain operators differently from the SMT-LIB standard. As an example, cvc5 uses mixed arithmetic internally, where integers and reals can appear together. A comprehensive list of these differences can be found in the Eunoia definition of CPC, as described below.

Ethos is an efficient proof checker written in C++ which can check proofs in the CPC format. For a quick start, the cvc5 repository contains a script to download and install the Ethos checker, and create scripts for generating proofs with cvc5 and checking them with the Ethos proof checker.

The Ethos checker is based on the logical framework Eunoia. The Cooperating Proof Calculus has been formalized in a Eunoia signature, which is contained within the cvc5 repository in this file . Based on this signature, Ethos can check CPC proofs over all theories that are formalized in this signature. For more details on Eunoia and a comprehensive overview of the language supported by the Ethos checker, see the user manual here .

Note that several proof rules in the Cooperating Proof Calculus are not yet supported in Eunoia signatures. Steps that use such rules are printed as trust steps in the proof. A trust step proves an arbitrary formula with no provided justification. The resulting proof contains warnings for trust steps that indicate which internal proof rules were recorded as trust steps in the proof.

Upon successful exit, ethos will return the output incomplete if any trust step is used in the proof, indicating that the reasoning in the proof was incomplete. Otherwise, if all proof steps are fully specified, ethos will return the output correct . All proofs in the cpc format are closed refutations of the input, in that the proof will assume formulas from the input and end with a step proving false.

For more fine-grained proofs, the additional option proof-granularity=dsl-rewrite can be passed to cvc5. This will result in proofs with more detail.

A simple example of cvc5 producing a proof in CPC proof format is shown below. Notice that the concrete syntax of CPC is very similar to the Alethe format. However, the proof rules used by these two formats are different.

           $ bin/cvc5 --dump-proofs --proof-format-mode=cpc --proof-granularity=dsl-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
(
(declare-const c Bool)
(declare-const b Bool)
(declare-const d Bool)
(define @t1 () (= b d))
(define @t2 () (or b d))
(define @t3 () (not (ite d c false)))
(define @t4 () (and d d))
(define @t5 () (and d c))
(define @t6 () (not @t1))
(define @t7 () (@list true false))
(assume @p1 (and (or d b) (= c d) @t3 (= @t2 @t1)))
(step @p2 :rule and_elim :premises (@p1) :args (0))
(step @p3 :rule reordering :premises (@p2) :args (@t2))
(step @p4 :rule aci_norm :args ((= @t4 d)))
(step @p5 :rule cong :premises (@p4) :args ((not @t4)))
(step @p6 :rule and_elim :premises (@p1) :args (1))
(step @p7 :rule refl :args (d))
(step @p8 :rule nary_cong :premises (@p7 @p6) :args (@t5))
(step @p9 :rule cong :premises (@p8) :args ((not @t5)))
(step @p10 :rule trans :premises (@p9 @p5))
(step @p11 :rule ite-else-false :args (d c))
(step @p12 :rule cong :premises (@p11) :args (@t3))
(step @p13 :rule trans :premises (@p12 @p10))
(step @p14 :rule and_elim :premises (@p1) :args (2))
(step @p15 :rule eq_resolve :premises (@p14 @p13))
(step @p16 :rule chain_m_resolution :premises (@p3 @p15) :args (b (@list true) (@list d)))
(step @p17 :rule cnf_equiv_pos1 :args (@t1))
(step @p18 :rule reordering :premises (@p17) :args ((or d (not b) @t6)))
(step @p19 :rule chain_m_resolution :premises (@p18 @p15 @p16) :args (@t6 @t7 (@list d b)))
(step @p20 :rule and_elim :premises (@p1) :args (3))
(step @p21 :rule equiv_elim1 :premises (@p20))
(step @p22 :rule reordering :premises (@p21) :args ((or @t1 (not @t2))))
(step @p23 false :rule chain_m_resolution :premises (@p22 @p19 @p3) :args (false @t7 (@list @t1 @t2)))
)

          

Checking with Logos 

Logos is an alternative checker for the CPC format, written in Lean, whose soundness is proven against a formalization of the semantics of SMT-LIB. It accepts the same proof syntax as Ethos, but does not read Eunoia signatures. Its proof rules are compiled from the same Eunoia definition of CPC that is contained in this repository, so that the proof rules of the two checkers come from a single definition. The cvc5 repository contains a script to download and install the Logos checker, and create scripts for generating proofs with cvc5 and checking them with the Logos proof checker.

Logos targets the fragment of CPC that is used by safe builds of cvc5, that is, builds configured with ./configure.sh safe . The expert CPC rules used by non-safe builds, which are defined in CpcExpert.eo , lie outside that fragment, and Logos will report a parse error on them. In some very rare cases, a proof in safe mode may lie outside the fragment for which Logos is proven correct. For an input outside its scope, Logos reports incomplete . This means that the proof of correctness for Logos does not cover that input; it does not mean that Logos found the CPC proof to be incorrect. Because the CI of cvc5 requires proofs in safe mode to be complete, that is, free of trust steps, every proof rule that a safe build can use is one that Logos verifies, apart from inputs of the kind just described.

Keeping CPC and Logos in sync 

Since that compilation consumes the signature in this repository, a change to proofs/eo/cpc must remain in sync with Logos. The commit of Logos this repository is pinned to is LOGOS_VERSION in contrib/get-logos-checker , which is the only place it appears. The script contrib/check-logos-compilation reads that pin, sets up the Eunoia compiler that performs the compilation, and reports whether the signature still compiles and whether that pinned Logos was generated from the current version of it. This check does not build Logos or check its Lean proofs. The cpc-logos workflow additionally requires that the CI of Logos has passed at the pinned commit, which it establishes by querying the result already recorded for that commit rather than by rerunning that CI.

These two conditions together, that the pinned Logos was generated from the signature in this repository and that the CI of Logos passes at that commit, are what makes the Eunoia definition of CPC here correct with respect to the semantics of SMT-LIB formalized in Logos, up to what the CI of Logos tests.

Changing the CPC signature 

Adding a proof rule to proofs/eo/cpc , or removing one, therefore requires a matching change to Logos: the Lean proof of that rule is written or removed there, and LOGOS_VERSION is then moved to the resulting commit, which moves both the checker that is installed and the checker that CPC is checked against. Logos is regenerated and repaired against a new version of the signature by the procedure documented there . Until the pin is moved, the cpc-logos workflow fails on the cvc5 pull request that changes the signature.

A rule that is needed in cvc5’s safe mode but cannot readily be proven in Logos does not have to hold up that pull request. There are two ways of proceeding:

Guard the new cvc5 reasoning that gives rise to the rule so that it is not available in safe mode. Optionally, proof rules that are not yet ready to be run in safe mode can be added to CpcExpert.eo .
Keep the new reasoning in safe mode and have Logos exclude it from its proof, by marking it :exclude in install/defs/Cpc.eos . This unblocks the cvc5 pull request without extending the guarantee above: a proof that uses such a rule will be reported incomplete by Logos.