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 and unsigned/signed ranges 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, and for deobfuscation linear MBA and bit shuffles), applied bottom-up under caller-owned budgets, with a memo, telemetry and host hooks.
• ext: host-defined extension operations (multi-output, total), registered in a Registry and built with Context::ext.
• mba (feature mba): the MBA service with an evidence gate, and cobra for the cobra-mba backend; 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 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.

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.

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) export and import (feature smtlib).

text

The expression syntax: a parser and a bounded printer.

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, and an unsigned and a signed interval. All three are kept consistent with each other (a reduced product).

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 interval [lo, hi] (lo <=u hi, no wrap-around).

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.