bitwright

Hash-consed fixed-width bit-vector expressions for Rust: exact evaluation, bit-level facts, and verified simplification.

bitwright is for tools that reason about machine integers: binary analyzers, deobfuscators, decompilers and lifters. It simplifies their expressions with predictable cost and without guessing: a rewrite preserves the value of the expression at every input, or it does not happen.

use bitwright::engine::Engine;
use bitwright::{Context, ParseOptions, Width};

fn main() -> Result<(), bitwright::Error> {
    let engine = Engine::standard();
    let mut cx = Context::new();
    let o = ParseOptions::width(Width::W64);
    for (input, simplified) in [
        // Arithmetic and boolean masking cancel.
        ("(x & y) + (x | y)", "x + y"),
        ("((x ^ 0x5a) + 3 - 3) ^ 0x5a", "x"),
        // Multiplying by an odd constant is a bijection: equal products, equal inputs.
        ("x * 0x87c37b91114253d5 == y * 0x87c37b91114253d5", "x == y"),
        // A comparison through a keyed hash mixer becomes a comparison of its input.
        (
            "let m = (x ^ 0xd3220fb78e33751f) * 0xd3220fb78e33751f; \
             (m ^ ((m >>u 32) >>u (m >>u 60))) * 0xd3220fb78e33751f == 0",
            "x == 0xd3220fb78e33751f",
        ),
    ] {
        let e = cx.parse(input, &o)?;
        let out = engine.simplify(&mut cx, e)?;
        assert_eq!(cx.display(out.expr).to_string(), simplified);
    }
    Ok(())
}

What it gives you

• Exact values of 1 to 512 bits. Every operator has total SMT-LIB QF_BV semantics, division by zero included, checked against an independent bit-serial reference evaluator.
• A hash-consed expression arena with canonicalization at construction, owned by a context. There is no global state, and the same input gives the same output on every run.
• Bit-level facts: known bits, unsigned and signed ranges, tri-state proofs, and constraints you assume (a path condition, an invariant), with the ones each result relies on reported back.
• A directed simplifier built from normal-form passes (linear arithmetic, xor forms, truth tables, comparison lattices, casts, demanded bits, linear MBA, bit shuffles) and a small rule corpus. Termination is guaranteed by construction, and every run is bounded by budgets you choose.
• Invertibility: proofs that an expression is an injective or bijective function of a subexpression (keyed mixers, xorshifts, T-functions), used to cancel and solve equalities, so a hash comparison becomes a plain one.
• A rule language (.bwr) for your own rewrites, with a mandatory soundness check (exhaustive at small widths, sampled up to 512 bits) and proof ledgers.
• Optional services: MBA simplification (a native solver for linear, semi-linear and polynomial MBA, pluggable backends, and answers bitwright proves itself), a bounded equality-saturation search, and SMT-LIB export and import, so any SMT solver can prove a rule at any width.

Installation

cargo add bitwright

bitwright needs Rust 1.88 or later. Its only required dependency is hashbrown. Optional features:

Documentation

The bitwright book is the guide. Every example in it is compiled and run as a test. It reads fine on GitHub too:

• API reference on docs.rs, for the latest release.
• Design reference: the principles, semantics and contracts, and how each part is validated.
• Changelog.

Command line

The bitwright binary checks, lints and proves rule files, and simplifies expressions:

cargo install --git https://github.com/valeria-org/bitwright bitwright-cli

bitwright check rules.bwr --ledger rules.bwr.proof      # soundness verdicts and the proof ledger
bitwright lint rules.bwr                                # every diagnostic, rendered
bitwright smt rules.bwr | z3 -in                        # prove every rule at 8, 32 and 64 bits (or `| bitwuzla`)
bitwright catalog > RULES.md                            # the built-in rules as Markdown
bitwright explain BW0302                                # what a diagnostic means
bitwright simplify '(x | y) - (x & y)' --deobfuscate    # x ^ y
bitwright simplify 'x * k == y * k' --assume '(k & 1) == 1'   # x == y, relying on the assumption

Stability

bitwright is 0.x. A minor release may change the API and simplification results, and lists every change of results under Behavior changes in the changelog; a patch release changes results only to fix unsoundness. The minimum supported Rust version is 1.88. See the stability chapter for the full contract.

Development

cargo test --workspace                                                  # every test, book examples included

cargo test --workspace --release -- --ignored --skip write_corpus_ledger    # the long suites (z3 and bitwuzla on PATH for the SMT proofs)

mdbook serve book                                                       # the book at http://localhost:3000

cargo run --release -p bitwright-bench                                  # benchmarks, in instructions retired

Fuzz targets are in fuzz/ (cargo +nightly fuzz run simplify_dag), docs/benchmarking.md explains how to compare a change against its baseline, and compare/ compares bitwright with other symbolic engines (egg, CoBRA, Triton, SMT solvers) on public MBA datasets.

License

PolyForm Noncommercial 1.0.0: free for any noncommercial purpose, including personal use, research, education, and use by charitable and public organizations. Commercial use needs a separate license from Emergentesombra Lda. (https://emergentelabs.com/).

Required Notice: Copyright 2026 Emergentesombra Lda., Porto, Portugal, PT 517806843 (https://emergentelabs.com/)