Install and build

Build from source

git clone https://github.com/yaspar-org/semi-persistent.git
cd semi-persistent
cargo build --release

The workspace requires Rust 1.98.1, pinned in rust-toolchain.toml. rustup selects this compiler when Cargo runs in the checkout. A normal build does not require Verus; the proof annotations compile away under rustc.

The build also requires a C++ compiler: the extractor’s internal SAT solver is CaDiCaL, which Cargo compiles from source (crate cadical-sys). Xcode’s command-line tools provide one on macOS (xcode-select --install), and g++ or clang++ does on Linux (Debian and Ubuntu: apt install build-essential). The external solvers that cost models can use (RoundingSat, clingo, MiniZinc) are optional and found on the PATH at run time; Part V lists them.

Cargo writes the command-line program to target/release/semi-persistent. Run its help command to confirm the build:

./target/release/semi-persistent --help

Equality saturation engine

Usage: semi-persistent [OPTIONS] <FILE>

Re-running the Verus proofs

Verus is required only to re-check the proofs in abstract-domains, containers-verus, and au-verus. All three crates pin the same Verus release in their .verus-version files.

The following installs the pinned release on x86-64 Linux or Apple Silicon macOS. The release archive includes Verus, cargo-verus, and Z3.

version=$(cat containers-verus/.verus-version)

case "$(uname -s)-$(uname -m)" in
  Linux-x86_64) asset=x86-linux ;;
  Darwin-arm64) asset=arm64-macos ;;
  *) echo "Download the matching asset from the Verus release page"; exit 1 ;;
esac

tmp=$(mktemp -d)
curl -fL \
  "https://github.com/verus-lang/verus/releases/download/release%2F${version}/verus-${version}-${asset}.zip" \
  -o "$tmp/verus.zip"
unzip -q "$tmp/verus.zip" -d "$tmp"

verus_home="$HOME/.local/verus-$version"
mkdir -p "$HOME/.local"
mv "$tmp"/verus-* "$verus_home"
export PATH="$verus_home:$PATH"

On macOS, allow the downloaded binaries through Gatekeeper:

bash "$verus_home/macos_allow_gatekeeper.sh"

Add the PATH export to your shell startup file to retain it in later shells. Confirm the installation with verus --version, then run the proof suites:

(cd abstract-domains && cargo verus verify)
(cd containers-verus && cargo verus verify)
(cd containers-verus && cargo verus verify --features literal-types)
(cd au-verus && cargo verus verify)

The crates in the workspace

Running Semper does not require working with these crates individually. Cargo prints their package names during builds, and the corresponding Rust crate names appear in stack traces. This table maps those names to their source paths.

Run the test suite

From the workspace root, run:

cargo test --workspace

At the time of writing, Cargo discovers 1,782 tests. The default run executes 1,731 and reports 51 as ignored. On the machine used to prepare this chapter, the command completed in 6 minutes 2 seconds.

The interpreter’s file-based integration fixtures live under egraph/tests/egg/. The harness in egraph/tests/egg_tests.rs sends each registered .egg program through the parser, sort checker, and interpreter. Unless overridden by a fixture directive, it runs the program with both naive and semi-naive evaluation, each under the static and the runtime atom-scheduling modes.

The same harness defines book_examples. It scans the top level of doc/book/examples/ for every file with the .egg extension and sends each one through the same checker. Chapters include those files directly, so every book example is a test. Adding an example to that directory does not require separate Rust test registration.

The ignored count includes manual diagnostics and measurements rather than one unfinished suite. Six entries are child-process cases for hasher configuration; their non-ignored driver tests already execute them in fresh processes. The slow ignored groups are:

• the completion_* diagnostics and the ac_vs_rules comparison;
• the bench_acgen_* fixtures in egg_tests;
• the AU measurement and stress tests in the au_* test binaries; and
• the feature-gated, 100-million-element compat_vec_stress tests.

List ignored tests without running them:

cargo test --workspace -- --ignored --list

Run slow tests by naming their harness rather than running every ignored test together. For example:

cargo test -p semi-persistent-egraph --release --test egg_tests \
  bench_acgen -- --ignored --nocapture

cargo test -p semi-persistent-egraph --release --test ac_vs_rules \
  -- --ignored --nocapture

cargo test -p semi-persistent-egraph --release --test au_hardness \
  hardness_map -- --ignored --nocapture

cargo test -p semi-persistent-containers-verus --features compat-all \
  --test compat_vec_stress -- --ignored --test-threads 1 --nocapture

The repository’s reproduction guide gives the commands and expected durations for the individual AU measurements.