Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Introduction

Carcara is an independent proof checker and elaborator for SMT proofs in the Alethe format, with a focus on performance and usability. It can efficiently check Alethe proofs even in the presence of coarse-grained steps, and reports detailed error messages in the case that the proof is invalid. Besides checking, Carcara is capable of elaborating proofs, by adding omitted detail and breaking down hard-to-check steps into multiple simpler steps.

This project was developed in the SMITE research group, at Universidade Federal de Minas Gerais (UFMG). A research paper describing Carcara has been published at TACAS 2023.

License

The Carcara source code and documentation are released under the Apache License, version 2.0.

Installation

Building from source

To build Carcara from source, you will first need to install Rust and Cargo. Currently, Carcara requires at least Rust version 1.93. Once you have installed an appropriate version of Rust, you can download and install the latest version of Carcara by running the following command:

cargo install --git https://github.com/ufmg-smite/carcara.git

This will build the project and place the carcara binary in Cargo’s binary directory (~/.cargo/bin by default).

You can uninstall Carcara by running cargo uninstall carcara.

Pre-built binary

Alternatively, a pre-compiled executable for the x86_64-unknown-linux-gnu platform can be downloaded from the GitHub releases page. To use Carcara in other platforms or operating systems, or to use a more recent version of Carcara, we recommend building from source.

Checking proofs with Carcara

To check a proof file with Carcara, use the check command, passing both the proof file and the original SMT-LIB problem file:

carcara check example.smt2.alethe example.smt2

If the problem filename is exactly the proof filename minus .alethe, you can omit it, and Carcara will infer it:

carcara check example.smt2.alethe

When checking a proof, Carcara will report one of three outcomes:

  • valid: The proof was fully checked, and no errors were found.
  • invalid: An error was found in part of the proof; an error message will have been printed.
  • holey: No errors were found, but the proof contained one or more “holes”. These can be either explicit applications of the hole rule, or steps that use an unknown or unsupported rule.

See carcara check --help for a full list of options.

Bypassing checking for specific rules

If you want Carcara to skip checking for specific rules, you can use the --allowed-rules option, for example:

carcara check example.smt2.alethe --allowed-rules foo bar

With this option, Carcara will ignore steps that use any of the given rules, and will consider them holes in the proof.

By default, Carcara returns a checking error when encountering a rule it does not recognize. If instead you want to ignore all such rules, you can use the --ignore-unknown-rules/-i flag. If a proof uses a rule that is allowed by either --ignore-unknown-rules or --allowed-rules, it will be reported as holey.

The lia_generic rule

Carcara does not check steps that use the lia_generic rule. This is an extremely coarse-grained rule from the Alethe format, and is in general NP-hard to check. If you need to validate proofs that contain this rule, you can use Carcara’s proof elaboration to call an external tool that can elaborate these steps into a series of easier-to-check steps. For more details, see the proof elaboration chapter.

Parallel checking

Using the --num-threads/-u option, you can control how many concurrent threads Carcara will use to check the proof. If the given value is greater than 1, Carcara will split the proof steps among that many worker threads, and check them in parallel. Note that proof parsing, which is oftentimes a bottleneck in Carcara, will still be sequential.

Checking Rare rewrites

SMT solvers can produce proofs that may depend on rare rules. In general, rare rules have the following format:

(declare-rare-rule bool-implies-de-morgan ((x1 Bool) (y1 Bool))
  :args (x1 y1)
  :conclusion (= (not (=> x1 y1)) (and x1 (not y1)))
)

First, we have a set of arguments and a conclusion. We can substitute the arguments into the conclusion. The substitution can be any first-order term available in the Alethe context.

(step st191.t1 
  (cl (= (not (=> (not (member$ ?v0 ?v1)) (= ?v0 ?v2)))
         (and (not (member$ ?v0 ?v1)) (not (= ?v0 ?v2)))))
  :rule rare_rewrite
  :args ("bool-implies-de-morgan" (not (member$ ?v0 ?v1)) (= ?v0 ?v2)))

Arguments can also be polymorphic:

(declare-rare-rule eq-refl ((@T0 Type) (t1 @T0))
  :args (t1)
  :premises ()
  :conclusion (= (= t1 t1) true))

We use @Type to denote an argument that is a polymorphic type. Polymorphic arguments are not passed in the :args field of the step statement:

(step t264
  (cl (= (= (op e3 e3) (op e3 e3)) true))
  :rule rare_rewrite
  :args ("eq-refl" (op e3 e3)))

Flags

We use the --rare-file flag to pass the rare file, for example:

carcara check your_file.smt2.alethe your_file.smt2 --rare-file your_rare_file.rare

Note that Carcara will only be able to check your proofs if every rewrite rule mentioned in the Alethe file is also present in your rare file.

Proof elaboration

Besides checking a proof, Carcara is also capable of proof elaboration. You can elaborate a proof file using the elaborate command:

carcara elaborate example.smt2.alethe example.smt2

This will check and elaborate the given proof, and print the elaborated proof to the standard output. By default, Carcara will print proofs using term sharing, i.e., using the (! ... :named ...) syntax. You can change this behavior with the --no-print-with-sharing/-v option.

Many of the same options used in the check command also apply to the elaborate command. See carcara elaborate --help for more details.

Elaboration pipeline

The specific way in which Carcara elaborates the proof is controlled via a --pipeline option. This takes a series of elaboration passes, and will apply them in the given order. The possible elaboration passes are:

By default, Carcara will attempt to apply all of these in the listed order.

Example

The following command will elaborate the given proof file with the uncrowd and polyeq elaboration passes, in that order:

carcara elaborate example.smt2.alethe --pipeline uncrowd polyeq

Note that, if you pass a positional argument (e.g. the proof filename) after the pipeline argument, you need an extra -- argument to denote the end of the pipeline list:

carcara elaborate --pipeline uncrowd polyeq -- example.smt2.alethe

Polyequality elaboration

In Alethe, we call “polyequality” the notion of equivalence between terms modulo the reordering of equalities. For example, we say that the terms (or (= a b) c) and (or (= b a) c) are “polyequal”, despite the equality term being flipped.

When checking an Alethe proof, a checker often needs to reason modulo polyequality. The refl rule, for example, allows the two terms to be syntactically different, if they are equivalent by polyequality. The following step is valid:

(step t1 (cl (= (or (= a b) c) (or (= b a) c))) :rule refl)

The polyeq elaboration pass can be used to remove all such instances where polyequality reasoning is required. For example, calling carcara elaborate --pipeline polyeq on the above step will transform it into the following steps:

(step t1.t1 (cl (= (= a b) (= b a))) :rule eq_symmetric)
(step t1.t2 (cl (= (or (= a b) c) (or (= b a) c))) :rule cong :premises (t1.t1))

In this case, Carcara added an eq_symmetric step to equate the two flipped equalities, and used a cong step to construct the original conclusion of t1. The exact elaboration differs by rule. The rules affected by this elaboration pass are:

  • assume
  • refl
  • forall_inst
  • subproof
  • ite_intro
  • bfun_elim

“Local” elaboration

Carcara has a number of small elaboration procedures for specific rules, that simplify steps in some small local way. These are grouped in the local elaboration pass. The rules affected by this are:

  • eq_transitive
  • trans
  • eq_congruent
  • cong
  • resolution
  • eq_mp

Transitivity rules

The eq_transitive and trans rules may sometimes contain the transitivity chain in an incorrect order. Additionally, the premise equalities might be flipped. For example, for trans, you may have:

(assume h1 (= a b))
(assume h2 (= c d))
(assume h3 (= c b))
(step t4 (cl (= a d)) :rule trans :premises (h1 h2 h3))

In this case, the local elaboration pass will change the order of t4’s premises so the transitivity chain is well ordered; and add an auxiliary step to flip the h3 equality. After elaboration, we will have:

(assume h1 (= a b))
(assume h2 (= c d))
(assume h3 (= c b))
(step t4.t1 (cl (= b c)) :rule symm :premises (h3))
(step t4 (cl (= a d)) :rule trans :premises (h1 t4.t1 h2))

A similar procedure is applied for the eq_transitive rule.

Congruence rules

In some applications of the eq_congruent and cong rules, the premise equalities may be flipped. In this case, Carcara will make this symmetry reasoning explicit. For example, the proof:

(assume h1 (= b a))
(assume h2 (= c d))
(step t3 (cl (= (and a c) (and b d))) :rule cong :premises (h1 h2))

will become

(assume h1 (= b a))
(assume h2 (= c d))
(step t3.t1 (cl (= a b)) :rule symm :premises (h1))
(step t3 (cl (= (and a c) (and b d))) :rule cong :premises (t3.t1 h2))

after elaboration. A similar elaboration is applied for the eq_congruent rule.

In the specific case where the cong rule is used over the = operator, the argument order might also be flipped in one of the conclusion terms. For example, the following step is valid according to the Alethe specification:

(assume h1 (= x y))
(step t2 (cl (= (= 0 x) (= y 0))) :rule cong :premises (h1))

To simplify this, the local elaboration will add eq_symmetric and trans auxiliary steps, resulting in the following:

(assume h1 (= x y))
(step t2.t1 (cl (= (= 0 x) (= x 0))) :rule eq_symmetric)
(step t2.t2 (cl (= (= x 0) (= y 0))) :rule cong :premises (h1))
(step t2 (cl (= (= 0 x) (= y 0))) :rule trans :premises (t2.t1 t2.t2))

resolution rule

In Alethe, resolution steps do not need to provide the pivots used in the resolution chain. For example, in the following proof, the step t4 omits the pivots:

(step t1 (cl p (not q)) :rule hole)
(step t2 (cl (not p)) :rule hole)
(step t3 (cl q r) :rule hole)
(step t4 (cl r) :rule resolution :premises (t1 t2 t3))

During elaboration, Carcara can find which pivots were used and add them to the proof step as arguments. For each pivot, two arguments are provided: the pivot term, and a boolean indicating whether it appears on the left-hand clause with positive polarity. For the example above, the elaborated step will be:

(step t4 (cl r) :rule resolution :premises (t1 t2 t3) :args (p true q false))

eq_mp rule

The eq_mp rule is not part of the Alethe specification. It is an extra rule, equivalent to CPC’s EQ_RESOLVE, that derives F2 from F1 and (= F1 F2):

(assume h1 p)
(assume h2 (= p q))
(step t3 (cl q) :rule eq_mp :premises (h1 h2))

During elaboration, it is replaced by a resolution step taking the original premises and a new equiv_pos2 step:

(assume h1 p)
(assume h2 (= p q))
(step t3.t1 (cl (not (= p q)) (not p) q) :rule equiv_pos2)
(step t3 (cl q) :rule resolution :premises (t3.t1 h2 h1) :args ((= p q) false p false))

In the odd case where q is exactly (not p) this pattern would break the resolution, so instead the elaboration is done with a resolution step that considers just the equivalence premise and relies on implicit duplicate elimination (which can be further eliminated by other elaboration passes if they are active). The equiv_pos2 step is nested one level deeper here, so that its id does not clash with the ones used by the uncrowd pass when it adds the contraction step that removes the duplicate:

(assume h1 p)
(assume h2 (= p (not p)))
(step t3.t1.t1 (cl (not (= p (not p))) (not p) (not p)) :rule equiv_pos2)
(step t3 (cl (not p)) :rule resolution :premises (t3.t1.t1 h2) :args ((= p (not p)) false))

Resolution uncrowding

Besides finding resolution pivots, Carcara is also able to refine resolution steps by uncrowding them. This refers the process of making the implicit removal of duplicates explicit, by the addition of contraction steps.

More specifically, the uncrowd elaboration pass will find all spots in the resolution chain where a pivot is used to remove a duplicate literal. Then, it breaks the resolution chain at that point, and adds a contraction step. Consider, for example, the following proof:

(step t1 (cl a b) :rule hole)
(step t2 (cl (not b) a) :rule hole)
(step t3 (cl (not a)) :rule hole)
(step t4 (cl) :rule resolution :premises (t1 t2 t3) :args (b true a true))

Here, the a pivot is duplicated after resolving t1 and t2, but is removed by the single (not a) literal in t3. After elaboration, the resulting proof will be:

(step t1 (cl a b) :rule hole)
(step t2 (cl (not b) a) :rule hole)
(step t3 (cl (not a)) :rule hole)
(step t4.t1 (cl a a) :rule resolution :premises (t1 t2) :args (b true))
(step t4.t2 (cl a) :rule contraction :premises (t4.t1))
(step t4 (cl) :rule resolution :premises (t4.t2 t3) :args (a true))

The resolution chain was broken after t2, with t4.t1 containing the two duplicate a literals explicitly. Then, a contraction step was added (t4.t2) to deduplicate them. Finally, the resolution chain continues in t4, reaching the same conclusion.

Besides adding contraction steps, the uncrowding elaboration pass may also add a reordering step at the end of the resolution chain, to make any implicit reordering of clause literals explicit.

If the option --uncrowd-rotate is given, Carcara will try to further minimize the number of contraction steps added by reordering the resolution premises when possible, in an effort to make a single contraction step deduplicate multiple pivots.

Reordering elimination

For many use cases of Alethe like proof translation or reconstruction in proof assistants, clause reordering steps can be challenging to deal with. With that in mind, Carcara has an elaboration step that can completely remove all reordering steps from a proof.

This is done by replacing the reordering step with its premise and, anytime it is used as a premise in another step, recomputing the clause of the step that used it. As an example, consider the following proof:

(step t1 (cl a b c) :rule hole)
(step t2 (cl b a c) :rule reordering :premises (t1))
(step t3 (cl b a c d) :rule weakening :premises (t2))

Here, step t2 will be eliminated, such that step t3 uses t1 directly as its premise. However, simply changing the premise clause of step t4 would make it invalid1. To avoid this, Carcara must also recompute the conclusion of t3, resulting in the following proof:

(step t1 (cl a b c) :rule hole)
(step t3 (cl a b c d) :rule weakening :premises (t1))

Of course, if any step further down in the proof uses t3 as a premise, it will also need to be recomputed, and these changes will propagate down the proof.

  1. Strictly speaking, the step would not be invalid according to the semantics of Alethe, which are entirely agnostic to clause ordering. However, when elaborating a proof, we aim to ensure a more strict semantics, in which clause ordering is maintained in rules such as weakening. ↩

Other features

Besides proof checking and elaboration, Carcara has a number of other functions useful for dealing with Alethe proofs. Run carcara --help to see a full list of subcommands.

Proof parsing/printing

You can use the carcara parse command to parse a proof file and print it back to standard output. This can be used to validate if a proof is syntactically valid without checking any proof steps, or to print the proof with some syntactical transformation applied.

Adding/removing term sharing

When printing a proof, Carcara automatically adds term sharing (i.e., the (! ... :named ...) syntax). If you parse a proof that does not make use of term sharing with carcara parse, it will by default be printed with term sharing added. Alternatively, you can remove term sharing from a proof that uses it by passing the --no-print-with-sharing/-v option.

Expanding let terms

You can use the --expand-let-bindings option to remove all let terms from the proof by inlining all attributed values. For example, the term

(let ((x 1)) (let ((y (+ x 2))) (+ y 3)))

will be expanded into

(+ (+ 1 2) 3)

Proof slicing

The carcara slice command can be used to extract an individual step from a proof, along with its transitive premises. Besides the usual arguments for parsing and printing the proof, this command also takes a --from argument which gives the step id from which to slice, and an optional --max-distance/-d argument, that specifies how many layers of transitive premises the slice should include.

Example

Consider the following Alethe proof:

(assume a0 a)
(step t0 (cl a b) :rule hole :premises (a0))
(step t1 (cl b a) :rule hole :premises (t0))
(step t2 (cl a b (not a)) :rule hole :premises (t0))
(anchor :step t3)
(assume t3.a0 (not a))
(step t3.t0 (cl b) :rule hole :premises (t3.a0 t1))
(step t3.t1 (cl b b) :rule hole :premises (t3.t0))
(step t3.t2 (cl (or b b)) :rule hole :premises (t3.t1))
(step t3 (cl (not (not a)) (or b b)) :rule subproof :discharge (t3.a0))
(step t4 (cl a (or b b)) :rule hole :premises (t3))
(step t5 (cl) :rule hole :premises (t4 a0 t2))

Calling carcara slice --from t1 -d 1 on it will result in the steps:

(assume a0 a)
(step t0 (cl a b) :rule hole :premises (a0))
(step t1 (cl b a) :rule hole :premises (t0))
(step slice_end (cl) :rule hole :premises (t1) :args ("trust"))

Note that, to make sure the slice is still a valid proof, Carcara added a dummy slice_end step that concludes the empty clause.

You can also slice from inside a subproof. Calling carcara slice --from t3.t0 on the proof above results in the slice:

(step t1 (cl b a) :rule hole :args ("trust"))
(anchor :step t3)
(assume t3.a0 (not a))
(step t3.t0 (cl b) :rule hole :premises (t3.a0 t1))
(step t3.t2 (cl (or b b)) :rule hole :premises (t3.t0) :args ("trust"))
(step t3 (cl (not (not a)) (or b b)) :rule subproof :discharge (t3.a0))
(step slice_end (cl) :rule hole :premises (t3) :args ("trust"))

A few things of note:

  • Since we did not pass --max-distance/-d, the slice only included the direct premises of t3.t2, and no transitive premises. For example, t0, which is a transitive premise of t3.t2 via t1, was not included.
  • To keep any context that might be introduced in an anchor, the slice included all anchors surrounding the sliced step (in this case, (anchor :step t3)).
  • To ensure that the resulting proof is still valid, the slice has to include the t3 step that concludes the subproof, as well as the previous step (t3.t2) which is implicitly referenced by t3.

Contributing

While Carcara is actively maintained by the folks at the SMITE research group at Universidade Federal de Minas Gerais (UFMG), we gladly welcome external contributions.

If you wish to contribute to the project, please do so by opening a pull request via GitHub.

Guidelines

In this project, we use Clippy as a linter and Rustfmt for code formatting. If you manage your Rust toolchain using Rustup, you can install Clippy and Rustfmt by running:

rustup component add clippy rustfmt

Once they’re installed, you can run cargo fmt to format your code according to the project guidelines, or cargo clippy to detect possible problems using Clippy. You may also run cargo clippy --fix to let Clippy try to automatically fix the detected issues.

When opening a pull request, make sure that your code compiles without warnings, and is formatted with Rustfmt. Run cargo test to ensure your changes do not break any existing behaviour. Additionally, we strive to support Rust versions as old as 1.93—please refrain from using features introduced in newer versions of Rust.