Crate bitwright 

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

A guide with tested examples is in the repository’s book/; the design reference is docs/design.md.

• BitVec: exact values of 1..=512 bits with total, SMT-LIB QF_BV semantics for every operator (UnOp, BinOp, CmpOp, casts, BitVec::select).
• Context: a hash-consed expression arena with construction-time canonicalization, symbols, O(1) structural metadata, iterative traversal, evaluation and substitution, and a text syntax (Context::parse, Context::display).
• Facts: known bits, an unsigned strided interval and a signed range per node (a reduced product), computed lazily and iteratively under a work cap, and tri-state proofs (Context::prove), also under consumer-defined constraints (Assumptions: facts and 1-bit predicates, propagated to operands, with the constraints each result relies on reported as a Reliance).
• rules: the .bwr rule language and its compiler; check (feature check, default): the soundness checker and proof ledgers.
• engine: the simplifier: proven rules and normal-form passes (linear, xor, bitwise, comparisons, casts, demanded bits, equalities through invertible maps, and for deobfuscation linear MBA and bit shuffles), applied bottom-up under caller-owned budgets, with a memo, telemetry and host hooks. Query::Injective and Query::Bijective ask whether an expression is an invertible function of one of its subexpressions.
• ext: host-defined extension operations (multi-output, total), registered in a Registry and built with Context::ext.
• translate: a host’s IR into expressions and back (Semantics, Lowering, Raise, and Template for semantics given as text at run time); host rewrites in Rust are engine::Rewrite.
• mba (feature mba): the MBA service with an evidence gate and bitwright’s own solvers; eqsat (feature eqsat): a bounded equality-saturation search; smtlib (feature smtlib): SMT-LIB export, import and rule obligations.

use bitwright::{BinOp, BitVec, Width};

let x = BitVec::from_u64(Width::W8, 200)?;
let y = BitVec::from_u64(Width::W8, 100)?;
assert_eq!(BitVec::apply_bin(BinOp::Add, &x, &y)?.to_u64(), Some(44)); // mod 2^8
assert!(BitVec::apply_bin(BinOp::UDiv, &x, &BitVec::zero(Width::W8))?.is_ones()); // total

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

let mut cx = Context::new();
let a = cx.parse("y + x", &ParseOptions::width(Width::W32))?;
let b = cx.parse("x + y", &ParseOptions::width(Width::W32))?;
assert_eq!(a, b); // canonical operand order: one node
// Construction canonicalizes and folds constants, but does not simplify further.
let c = cx.parse("(x - (2 + 3)) + 5", &ParseOptions::width(Width::W32))?;
assert_eq!(cx.display(c).to_string(), "x - 5 + 5");

Re-exports

pub use fp::FpFormat;

pub use fp::RoundingMode;

pub use text::ParseOptions;

pub use text::PrintOptions;

Modules

check

The soundness checker: evidence that every rule is a valid rewrite, and the proof ledger.

engine

The simplifier: an Engine applies linked rule programs to expressions under a Strategy, within caller-owned budgets. See docs/design.md §6.

eqsat

The equality-saturation search service (feature eqsat, default off). See docs/design.md §10.

ext

Extension operations: host-defined, total, multi-output operators.

fp

IEEE 754 floating point on bit-vectors.

lift

Front ends for lifted code: the IR a lifter or disassembler produces, read into expressions (the registers’ final values, the stores to memory, the conditions of exits), ready to simplify.

mba

The MBA service (feature mba): simplification of mixed Boolean-arithmetic expressions by a pluggable solver, behind an evidence gate. See docs/design.md §9.

memory

Memory as expressions: loads and stores over an array from addresses to cells, resolved at construction into the operators bitwright already has, so the simplifier, the facts, the prover and SMT-LIB export work on them unchanged.

prove

A native prover (feature prove): expressions are bit-blasted into an and-inverter graph, encoded as clauses, and decided by bitwright’s own CDCL SAT solver. A proof of validity comes with a certificate, the clauses and a DRUP proof of their unsatisfiability, that an independent checker (Certificate::check) verifies, and that any DRAT checker can read (Certificate::dimacs, Certificate::drat). A refutation comes with a counterexample: a value for every symbol, checked by bitwright’s evaluator before it is returned. A question the search does not settle within its budget says why (Unknown), and a Question goes on from where the search stopped, under a larger budget, without starting over. For a small joint output superset above unresolved predicates, domain::analyze preserves shared Boolean structure under explicit premises without solving reachability.

rules

The rule language (.bwr): typed, width-polymorphic rewrite rules and identities, compiled into RulePrograms. See docs/design.md §7.

smtlib

SMT-LIB 2.6 (QF_BV, and QF_BVFP for floating point) export and import (feature smtlib).

synth

Synthesis: the smallest expression equal to a given one, over its variables and constants, whatever its shape (MBA or not). Bottom-up enumeration by size, one representative per behavior on a set of sample points (observational equivalence: Udupa et al., PLDI 2013; Alur et al., TACAS 2017), and counterexample-guided inductive synthesis (Solar-Lezama et al., ASPLOS 2006): a candidate that behaves like the target on every sample is proved equal by the native prover, and a counterexample becomes a sample and the enumeration starts over. Every answer is proved. Feature prove.

text

The expression syntax: a parser and a bounded printer.

transform

Verifying compiler transformations: that a target program refines a source program under LLVM’s semantics of poison, undefined behavior and floating point, for peephole transformations written in the transformation syntax the Alive paper introduced (Lopes et al., PLDI 2015), and for pairs of functions in a subset of LLVM IR (translation validation). Feature prove.

translate

A host’s IR in and out: its instructions translated into expressions (Semantics, Lowering), and results translated back into instructions (Raise), without text.

traps

Trap guards for hosts that model faulting division or out-of-range shift counts (bitwright’s operators are total). A guard is an ordinary 1-bit expression; on a path that does not fault, assume it false (Assumptions::assume_false).

Structs

ArenaCounters

Nodes created by the caller’s own builder calls versus nodes created by bitwright itself (simplification, search). Lets a host retry maintenance only after enough input growth.

Assumptions

Constraints assumed to hold, layered over the facts the context derives: facts about expressions (assume) and 1-bit predicates assumed true or false (assume_true, assume_false).

BitVec

An exact W-bit value, W in 1..=512.

ConstraintId

Identifies a constraint of an Assumptions set: the k-th one added is k, from 0.

Context

A hash-consed expression arena.

ContextConfig

Configuration of a Context.

Expr

A handle to an expression node.

ExprMap

A dense side table keyed by expression index.

ExprSet

A dense set of expressions (a bitset keyed by index).

Facts

What is known about the values of a W-bit expression: known bits, an unsigned strided interval (the values lo, lo + stride, …, hi) and a signed interval. The three are kept consistent with each other (a reduced product): known bits snap the intervals’ ends to the nearest values they allow and give the strided interval their known low bits as a residue class; the intervals give the known bits their bounds’ common high bits, and the stride its factor of two as known low bits. A value is possible only if every component allows it.

FnEnv

An Env backed by a closure.

KnownBits

Per-bit knowledge about a W-bit value: bits in zero are certainly 0, bits in one are certainly 1, and the two masks are disjoint. The concretization is every value v with v & zero == 0 and v & one == one.

Mark

A position in the caller-growth counter; see Context::caller_growth_since.

Proof

An answer from Context::prove_under: the truth value, and the constraints it relies on (none for Unknown).

Reliance

The constraints a result may rely on: every constraint it relies on is included, and possibly others (the set over-approximates). Constraints from the 64th on are tracked together.

SRange

The signed interval [lo, hi] (lo <=s hi, no wrap-around).

Substitution

A substitution applied incrementally by Context::substitute_bounded: the replacements, and the result of every node rewritten so far. Repeated calls share that work, and a caller can read which new node each old one became (to carry its own metadata along).

SymbolId

A symbol’s index within its context.

URange

The unsigned strided interval {lo, lo + stride, lo + 2·stride, …, hi} (lo <=u hi, no wrap-around). The stride is 0 exactly when lo == hi, and otherwise divides hi − lo, so both bounds are members. A stride of 1 is the plain interval [lo, hi].

Width

A bit width in 1..=512. Invalid widths cannot be constructed.

Enums

BinOp

Binary operators. All map two W-bit operands to a W-bit result.

Bounded

A size that may have been cut off at a bound.

CmpOp

The comparison predicates stored in expressions. Each maps two W-bit operands to a 1-bit result. ugt, uge, sgt and sge are spelled by swapping operands; see CmpOpExt.

CmpOpExt

Every comparison predicate, including the operand-swapped forms.

Error

Errors from building, inspecting, evaluating or parsing expressions.

ParseError

Failure to parse a textual bit-vector literal.

Query

A question about expression values, answered by Context::prove.

SymbolKey

The identity of a symbol within a context.

Truth

A three-valued answer. Unknown is always a correct answer.

UnOp

Unary operators. All map a W-bit operand to a W-bit result.

ValueError

A value that cannot be represented at the requested width.

View

A read-only view of one node.

WidthError

A width, or a combination of widths, that the requested operation does not accept.

Traits

Env

Values for symbols, used by Context::eval.