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 ommited 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.87. 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-cli.

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.

Dealing with unknown rules

By default, Carcara will return a checking error when encountering a rule it does not recognize. If instead you want to ignore such rules, you can use the --ignore-unknown-rules/-i flag. Alternatively, you can use the --allowed-rules option to pass a specific list of unkown rules to allow. For example:

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

If a proof uses a rule that is allowed by either --ignore-unknown-rules or --allowed-rules, it will be considered 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 elaboration applied to the proof is controlled via a --pipeline option. This takes a series of elaboration steps, and will apply them in the given order. The possible elaboration steps 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 steps, 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 step can be used to remove all such instances where polyequality reasoning is required. For exemple, 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 step 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 step. The rules affected by this are:

  • eq_transitive
  • trans
  • cong
  • resolution

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 step 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.

cong rule

In the specific case where the cong rule is used over the = operator, the argument order might be flipped in one of the 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))

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.87—please refrain from using features introduced in newer versions of Rust.