Proof format: LFSC ¶
Using the flag proof-format-mode=lfsc , cvc5 outputs proofs in the LFSC proof format.
The LFSC proof format is based on the LF logical framework extended with computational side conditions, as described in [ SOR+13 ] . A high performance C++ proof checker for LFSC is available here .
For a quick start, the cvc5 repository contains a script which will download and install the LFSC proof checker, and create scripts for generating proofs with cvc5 and checking them with the LFSC proof checker.
LFSC is a meta-framework, meaning that the proof rules used by cvc5 are defined in signature files, also contained within the cvc5 repository in this directory . Based on these signatures, cvc5 provides basic support for LFSC proofs over all theories that it supports.
Note that several proof rules in the internal calculus are not yet supported in LFSC signatures, and are instead printed as trust steps in the LFSC proof. A trust step proves an arbitrary formula with no provided justification. The LFSC proof contains warnings for which proof rules from the internal calculus were recorded as trust steps in the LFSC proof.
For more fine-grained proofs, the additional option proof-granularity=theory-rewrite should be passed to cvc5. This often will result in LFSC proofs with more detail, and whose trust steps correspond only to equalities corresponding to theory rewrites.
A simple example of cvc5 producing a proof in LFSC proof format:
$ bin/cvc5 --dump-proofs --proof-format-mode=lfsc --proof-granularity=theory-rewrite ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
unsat
; WARNING: adding trust step for THEORY_REWRITE
(define cvc.c (var 0 Bool))
(define cvc.b (var 1 Bool))
(define cvc.d (var 2 Bool))
(check
(@ __t1 (= cvc.b cvc.d)
(@ __t2 (or cvc.b (or cvc.d false))
(@ __t3 (= __t2 __t1)
(@ __t4 (and __t3 true)
(@ __t5 (ite cvc.d cvc.c false)
(@ __t6 (= cvc.c cvc.d)
(@ __t7 (or cvc.d (or cvc.b false))
(@ __t8 (and (not cvc.d) __t4)
(% __a0 (holds (and __t7 (and __t6 (and (not __t5) __t4))))
(: (holds false)
(plet _ _
(refl __t3)
(\ __p1
(plet _ _
(refl f_and)
(\ __p2
(plet _ _
(refl __t7)
(\ __p3
(plet _ _
(refl f_and)
(\ __p4
(plet _ _
(refl f_and)
(\ __p5
(plet _ _
(cong _ _ _ _
(cong _ _ _ _ __p5 __p3)
(cong _ _ _ _
(cong _ _ _ _ __p5
(refl __t6))
(cong _ _ _ _
(cong _ _ _ _ __p5
(cong _ _ _ _
(refl f_not)
(trust (= __t5 (and cvc.d (and cvc.c true)))) ; from THEORY_REWRITE
))
(cong _ _ _ _
(cong _ _ _ _ __p5 __p1)
(refl true)))))
(\ __p6
(plet _ _
(and_elim _ _ 1
(eq_resolve _ _ __a0 __p6))
(\ __p7
(plet _ _
(refl f_and)
(\ __p8
(plet _ _
(refl cvc.d)
(\ __p9
(plet _ _
(eq_resolve _ _ __a0
(trans _ _ _ __p6
(trans _ _ _
(cong _ _ _ _
(cong _ _ _ _ __p4
(refl __t7))
(cong _ _ _ _
(cong _ _ _ _ __p4
(cong _ _ _ _
(cong _ _ _ _
(refl f_=) __p7) __p9))
(cong _ _ _ _
(cong _ _ _ _ __p4
(cong _ _ _ _
(refl f_not)
(cong _ _ _ _
(cong _ _ _ _ __p8 __p9)
(cong _ _ _ _
(cong _ _ _ _ __p8 __p7)
(refl true)))))
(cong _ _ _ _
(cong _ _ _ _ __p4
(refl __t3))
(refl true)))))
(trans _ _ _
(cong _ _ _ _
(cong _ _ _ _ __p2 __p3)
(cong _ _ _ _
(cong _ _ _ _ __p2
(trust (= (= cvc.d cvc.d) true)) ; from THEORY_REWRITE
)
(cong _ _ _ _
(cong _ _ _ _ __p2
(cong _ _ _ _
(refl f_not)
(trust (= (and cvc.d (and cvc.d true)) cvc.d)) ; from THEORY_REWRITE
))
(cong _ _ _ _
(cong _ _ _ _ __p2 __p1)
(refl true)))))
(trust (= (and __t7 (and true __t8)) (and __t7 __t8))) ; from THEORY_REWRITE
))))
(\ __p10
(plet _ _
(and_elim _ _ 0 __p10)
(\ __p11
(resolution _ _ _
(resolution _ _ _
(reordering _ (or __t1 (or (not __t2) false))
(equiv_elim1 _ _
(and_elim _ _ 2 __p10)))
(resolution _ _ _
(resolution _ _ _
(reordering _ (or cvc.d (or (not cvc.b) (or (not __t1) false)))
(cnf_equiv_pos1 cvc.b cvc.d))
(and_elim _ _ 1 __p10) tt cvc.d)
(resolution _ _ _
(reordering _ __t2 __p11)
(and_elim _ _ 1 __p10) tt cvc.d) ff cvc.b) tt __t1)
(reordering _ __t2 __p11) ff __t2))))))))))))))))))))))))))))))))))