Reduced-Product-for-Rust

A no_std-compatible Reduced Product abstract domain implementation in pure Rust, combining Tnum and Wrapped Interval for Solana eBPF static analysis.

Reference

• "Program Analysis Combining Generalized Bit-Level and Word-Level Abstractions". ISSTA2025. https://dl.acm.org/doi/10.1145/3728905

Overview

The reduced product combines two complementary abstract domains to achieve higher precision than either domain alone. It iteratively exchanges information between the interval domain (word-level bounds) and the tnum domain (bit-level known/unknown patterns), tightening both representations until a fixed point is reached.

Installation

[dependencies]
svm-reduced-product = { git = "https://github.com/OpenSourceVerif/Reduced-Product-for-Rust" }

Usage

use svm_reduced_product::ReducedProduct;

// From known bounds
let rp = ReducedProduct::new(interval, tnum);

// Bottom / top / constant
let rp = ReducedProduct::bottom(64);
let rp = ReducedProduct::top(64);
let rp = ReducedProduct::constant(42, 64);

// From tnum alone
let rp = ReducedProduct::from_tnum(tnum, 64);

// Access components
let interval = rp.interval();
let tnum = rp.tnum();

// Manual reduction trigger
rp.reduce();