d410bb7ba7
When a witness recorder is active, run z3::optimize.minimize on the SAT model before extracting bytes for fuzz seeds. Refines integer params toward the smallest path-and-hazard-satisfying value, so seeds emit `arg=1` instead of `arg=0xDEADBEEF`. Measured on synthetic access_at_offset(p, offset) with the path `0 < offset && offset < 100`: primary-witness median 33 -> 5 (85% smaller). divide_by_count(p, count) with `count > 0` was already path-minimal so no change. Only the primary witness is refined; recordAlternateWitnesses still uses the original model so the corpus covers the equivalence class. Curl-scale validation deferred -- fuzz-prep on full curl crashes pre-existing (verified Z5-OFF baseline exit 139).
110 lines
3.6 KiB
C++
110 lines
3.6 KiB
C++
// Matrix row Z5 — refine a SAT model into a "minimal witness" with
|
|
// smaller integer values, so fuzz seeds emit human-readable params
|
|
// (e.g., `arg=1` instead of `arg=0xDEADBEEF`).
|
|
//
|
|
// Contract pins:
|
|
// 1. A model refined from `solver.check()` has integer-witness values
|
|
// no larger than the vanilla model's, for each refined param.
|
|
// 2. The refined model still satisfies the original path predicate
|
|
// (refinement never invents an infeasible assignment).
|
|
// 3. Refining a path that's already minimal is a no-op (or produces
|
|
// equal-magnitude values).
|
|
// 4. Multiple-param refinement minimizes each independently subject
|
|
// to the joint constraints.
|
|
|
|
#include <z3++.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <cstdint>
|
|
#include <vector>
|
|
|
|
#include "fold/fuzz/minimal_witness.hpp"
|
|
|
|
using fold::fuzz::refineModelForMinimalWitness;
|
|
|
|
namespace {
|
|
|
|
std::uint64_t numeralU64(const z3::expr& e) {
|
|
std::uint64_t v = 0;
|
|
REQUIRE(e.is_numeral_u64(v));
|
|
return v;
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("minimal-witness: refines a single integer param to its smallest value",
|
|
"[fuzz][z5][refine]") {
|
|
z3::context c;
|
|
z3::expr x = c.bv_const("x", 64);
|
|
z3::expr path = (x > c.bv_val(0, 64)) && (x < c.bv_val(1000000, 64));
|
|
|
|
z3::solver s(c);
|
|
s.add(path);
|
|
REQUIRE(s.check() == z3::sat);
|
|
z3::model vanilla = s.get_model();
|
|
|
|
auto refined = refineModelForMinimalWitness(c, path, {x});
|
|
REQUIRE(refined.has_value());
|
|
|
|
const std::uint64_t vanilla_x = numeralU64(vanilla.eval(x));
|
|
const std::uint64_t refined_x = numeralU64(refined->eval(x));
|
|
REQUIRE(refined_x <= vanilla_x);
|
|
REQUIRE(refined_x == 1); // path requires x > 0, smallest is 1
|
|
}
|
|
|
|
TEST_CASE("minimal-witness: refined model still satisfies the path predicate",
|
|
"[fuzz][z5][soundness]") {
|
|
z3::context c;
|
|
z3::expr x = c.bv_const("x", 64);
|
|
z3::expr y = c.bv_const("y", 64);
|
|
z3::expr path = (x + y == c.bv_val(100, 64)) && (x > c.bv_val(0, 64)) && (y > c.bv_val(0, 64));
|
|
|
|
auto refined = refineModelForMinimalWitness(c, path, {x, y});
|
|
REQUIRE(refined.has_value());
|
|
|
|
z3::solver s(c);
|
|
s.add(path);
|
|
s.add(x == refined->eval(x));
|
|
s.add(y == refined->eval(y));
|
|
REQUIRE(s.check() == z3::sat);
|
|
}
|
|
|
|
TEST_CASE("minimal-witness: already-minimal path returns same magnitudes", "[fuzz][z5][noop]") {
|
|
z3::context c;
|
|
z3::expr x = c.bv_const("x", 64);
|
|
z3::expr path = (x == c.bv_val(42, 64));
|
|
|
|
auto refined = refineModelForMinimalWitness(c, path, {x});
|
|
REQUIRE(refined.has_value());
|
|
REQUIRE(numeralU64(refined->eval(x)) == 42);
|
|
}
|
|
|
|
TEST_CASE("minimal-witness: multi-param refinement reduces each independently",
|
|
"[fuzz][z5][multi]") {
|
|
z3::context c;
|
|
z3::expr a = c.bv_const("a", 64);
|
|
z3::expr b = c.bv_const("b", 64);
|
|
z3::expr path = (a > c.bv_val(5, 64)) && (b > c.bv_val(10, 64));
|
|
|
|
auto refined = refineModelForMinimalWitness(c, path, {a, b});
|
|
REQUIRE(refined.has_value());
|
|
|
|
REQUIRE(numeralU64(refined->eval(a)) == 6); // smallest a > 5
|
|
REQUIRE(numeralU64(refined->eval(b)) == 11); // smallest b > 10
|
|
}
|
|
|
|
TEST_CASE("minimal-witness: empty param list returns a model of the path alone",
|
|
"[fuzz][z5][empty]") {
|
|
z3::context c;
|
|
z3::expr x = c.bv_const("x", 64);
|
|
z3::expr path = (x > c.bv_val(0, 64));
|
|
|
|
auto refined = refineModelForMinimalWitness(c, path, {});
|
|
REQUIRE(refined.has_value());
|
|
// With no minimization targets, optimize behaves like a normal solver.
|
|
// Just require SAT-feasibility — value is arbitrary.
|
|
z3::solver s(c);
|
|
s.add(path);
|
|
s.add(x == refined->eval(x));
|
|
REQUIRE(s.check() == z3::sat);
|
|
}
|