macro-generated test harnesses for type-parameterized verification

Suppose you need to verify the same property across a family of types — every signed integer width, every unsigned integer width, every floating point format. The property is the same. The function name is the same. Only the type changes. After writing the same harness pattern across enough types, the duplication stops being harmless and starts becoming a maintenance problem.

Declarative macros turn out to be a good fit for this.

the shape of the harness

A verification harness is a function that takes no arguments, generates symbolic inputs, calls the function under test, and lets the verifier check whatever postconditions are attached. For an unsafe arithmetic operation, it looks like this:

#[kani::proof_for_contract(i32::unchecked_add)]
pub fn unchecked_add_i32() {
    let a: i32 = kani::any::<i32>();
    let b: i32 = kani::any::<i32>();
    unsafe { a.unchecked_add(b); }
}

The body is identical for i8, i16, i64, i128, and the unsigned siblings. Only the type token and the harness name differ. Most of the variation is in the nouns, not the behavior.

the macro

A declarative macro that emits one harness per type takes the type and the harness name as parameters and pastes them into a template:

macro_rules! generate_unchecked_math_harness {
    ($type:ty, $method:ident, $harness_name:ident) => {
        #[kani::proof_for_contract($type::$method)]
        pub fn $harness_name() {
            let a: $type = kani::any::<$type>();
            let b: $type = kani::any::<$type>();
            unsafe { a.$method(b); }
        }
    }
}

generate_unchecked_math_harness!(i8,   unchecked_add, unchecked_add_i8);
generate_unchecked_math_harness!(i16,  unchecked_add, unchecked_add_i16);
generate_unchecked_math_harness!(i32,  unchecked_add, unchecked_add_i32);
// ... and so on

Twelve invocations replace twelve copies of nearly-identical code. When the harness body needs to change — adding an assumption, refactoring the call site, switching to a stricter contract — you change the macro body once and every type benefits.

partitioning the input space

For small types like i8 and i16, the verifier can reason about every possible input. For larger widths such as 64-bit and 128-bit integers, full-range verification often becomes impractical. The proof gets harder for the verifier to discharge automatically, and runs may time out unless the input space is constrained. One practical way to keep the proof tractable is to constrain symbolic inputs to regions of interest with kani::assume, then write multiple harnesses for the same type, each covering a different region.

Macros generalize cleanly to this. Instead of one harness per type, the macro takes a list of (name, min, max) tuples and emits one harness per tuple, each with its own range constraint:

macro_rules! generate_unchecked_mul_intervals {
    ($type:ty, $method:ident,
     $($name:ident, $min:expr, $max:expr),+) => {
        $(
            #[kani::proof_for_contract($type::$method)]
            pub fn $name() {
                let a: $type = kani::any::<$type>();
                let b: $type = kani::any::<$type>();
                kani::assume(a >= $min && a <= $max);
                kani::assume(b >= $min && b <= $max);
                unsafe { a.$method(b); }
            }
        )+
    }
}

generate_unchecked_mul_intervals!(i32, unchecked_mul,
    mul_i32_near_zero,    -10,             10,
    mul_i32_near_max,     i32::MAX - 1000, i32::MAX,
    mul_i32_near_min,     i32::MIN,        i32::MIN + 1000,
    mul_i32_upper_half,   i32::MAX / 2,    i32::MAX,
    mul_i32_lower_half,   i32::MIN,        i32::MIN / 2
);

Five harnesses, one macro call. These intervals were not intended to cover the domain uniformly — they were chosen to keep proofs tractable while still stressing the overflow-heavy parts of the space. The design work moves out of the harness body and into the table of regions — which is where most of the judgment tends to concentrate.

what macros are good for

Any time you have a set of tests, harnesses, or definitions whose only variation is a small set of nouns — types, constants, method names — a declarative macro turns the repetition into a table. In practice this means the table tends to be where you edit, and the body tends to be where correctness lives. Changes to either can propagate without touching the other.

The cost is a layer of indirection that is harder to step through with a debugger, and a steeper learning curve for anyone reading the code for the first time. The benefit is that the things that vary are visible in one place, and the things that should not vary cannot drift.

For verification work, where the harnesses outnumber the methods by an order of magnitude and the methods themselves come in regular families, the repeated structure is regular enough that the harnesses are almost data: type, method, range. Once that became clear, keeping the repetition in handwritten code stopped making much sense.