use std::fmt::Write;
use crate::schema::Contract;
pub fn generate_fuzz_target(contract: &Contract, stem: &str) -> String {
let mut out = String::with_capacity(2048);
let _ = writeln!(out, "#![no_main]");
let _ = writeln!(
out,
"// Auto-generated fuzz target from contract: {}",
contract.metadata.description
);
let _ = writeln!(out, "// Regenerate with: pv fuzz contracts/{stem}.yaml");
let _ = writeln!(out);
let _ = writeln!(out, "use libfuzzer_sys::fuzz_target;");
let _ = writeln!(out);
let preconditions: Vec<&str> = contract
.proof_obligations
.iter()
.filter(|ob| ob.obligation_type == crate::schema::ObligationType::Precondition)
.filter_map(|ob| ob.formal.as_deref())
.collect();
let postconditions: Vec<&str> = contract
.proof_obligations
.iter()
.filter(|ob| ob.obligation_type == crate::schema::ObligationType::Postcondition)
.filter_map(|ob| ob.formal.as_deref())
.collect();
let _ = writeln!(out, "fuzz_target!(|data: &[u8]| {{");
let _ = writeln!(out, " // Minimum input size guard");
let _ = writeln!(out, " if data.len() < 8 {{ return; }}");
let _ = writeln!(out);
let _ = writeln!(out, " // Parse input: interpret bytes as f32 vector");
let _ = writeln!(
out,
" let len = ((data[0] as usize) % 64).saturating_add(1);"
);
let _ = writeln!(out, " let byte_len = len * 4;");
let _ = writeln!(out, " if data.len() < 4 + byte_len {{ return; }}");
let _ = writeln!(out, " let input: Vec<f32> = data[4..4 + byte_len]");
let _ = writeln!(out, " .chunks_exact(4)");
let _ = writeln!(
out,
" .map(|b| f32::from_le_bytes(b.try_into().unwrap()))"
);
let _ = writeln!(out, " .collect();");
let _ = writeln!(out);
if preconditions.is_empty() {
let _ = writeln!(
out,
" // No explicit preconditions — filter NaN/Inf for numerical stability"
);
} else {
let _ = writeln!(out, " // Contract precondition gates");
for pre in &preconditions {
let _ = writeln!(out, " // PRE: {pre}");
}
}
let _ = writeln!(
out,
" if input.is_empty() || input.iter().any(|x| x.is_nan() || x.is_infinite()) {{"
);
let _ = writeln!(out, " return;");
let _ = writeln!(out, " }}");
let _ = writeln!(out);
let fn_name = stem.replace('-', "_").replace("_v1", "");
let _ = writeln!(out, " // Kernel under test — must not panic");
let _ = writeln!(out, " let result = std::panic::catch_unwind(|| {{");
let _ = writeln!(out, " let mut output = vec![0.0f32; input.len()];");
let _ = writeln!(
out,
" // TODO: Wire up: {fn_name}(&input, &mut output);"
);
let _ = writeln!(out, " output");
let _ = writeln!(out, " }});");
let _ = writeln!(out);
if !postconditions.is_empty() {
let _ = writeln!(out, " // Contract postcondition checks");
let _ = writeln!(out, " if let Ok(output) = result {{");
for post in &postconditions {
let _ = writeln!(out, " // POST: {post}");
}
let _ = writeln!(
out,
" assert_eq!(output.len(), input.len(), \"output length mismatch\");"
);
let _ = writeln!(out, " }}");
}
let _ = writeln!(out, "}});");
out
}
pub fn generate_fuzz_cargo_toml(crate_name: &str) -> String {
let mut out = String::with_capacity(512);
let _ = writeln!(out, "[package]");
let _ = writeln!(out, "name = \"{crate_name}-fuzz\"");
let _ = writeln!(out, "version = \"0.0.0\"");
let _ = writeln!(out, "publish = false");
let _ = writeln!(out, "edition = \"2021\"");
let _ = writeln!(out);
let _ = writeln!(out, "[package.metadata]");
let _ = writeln!(out, "cargo-fuzz = true");
let _ = writeln!(out);
let _ = writeln!(out, "[dependencies]");
let _ = writeln!(out, "libfuzzer-sys = \"0.11\"");
let _ = writeln!(out);
let _ = writeln!(out, "# TODO: Add dependency on the crate under test");
let _ = writeln!(out, "# {crate_name} = {{ path = \"..\" }}");
out
}
#[cfg(test)]
mod tests {
use super::*;
use crate::schema::parse_contract_str;
fn softmax_contract() -> Contract {
parse_contract_str(
r#"
metadata:
version: "1.0.0"
description: "Softmax kernel"
references: ["Paper A"]
equations:
softmax:
formula: "σ(x)_i = exp(x_i - max(x)) / Σ_j exp(x_j - max(x))"
domain: "x ∈ ℝ^n, n ≥ 1"
proof_obligations:
- type: precondition
property: "Input vector is finite and non-empty"
formal: "∀i: ¬isNaN(x_i) ∧ ¬isInf(x_i) ∧ len(x) > 0"
- type: postcondition
property: "Output is a valid probability distribution"
formal: "len(σ(x)) = len(x) ∧ ∀i: 0 < σ(x)_i < 1 ∧ |Σ σ(x)_i - 1| < ε"
- type: invariant
property: "Output sums to 1"
falsification_tests:
- id: FALSIFY-001
rule: "Normalization"
prediction: "sum ≈ 1.0"
if_fails: "Bug"
kani_harnesses:
- id: KANI-001
obligation: "sums to 1"
bound: 8
"#,
)
.unwrap()
}
#[test]
fn generates_fuzz_target() {
let contract = softmax_contract();
let output = generate_fuzz_target(&contract, "softmax-kernel-v1");
assert!(output.contains("#![no_main]"));
assert!(output.contains("use libfuzzer_sys::fuzz_target;"));
assert!(output.contains("fuzz_target!"));
assert!(output.contains("catch_unwind"));
assert!(output.contains("PRE:"));
assert!(output.contains("POST:"));
}
#[test]
fn generates_fuzz_target_no_preconditions() {
let contract = parse_contract_str(
r#"
metadata:
version: "1.0.0"
description: "Simple kernel"
references: ["X"]
equations:
f:
formula: "f(x) = x"
proof_obligations:
- type: invariant
property: "identity"
falsification_tests:
- id: F-001
rule: "id"
prediction: "f(x) = x"
if_fails: "bug"
kani_harnesses:
- id: K-001
obligation: "id"
bound: 8
"#,
)
.unwrap();
let output = generate_fuzz_target(&contract, "identity-v1");
assert!(output.contains("No explicit preconditions"));
assert!(output.contains("fuzz_target!"));
}
#[test]
fn generates_cargo_toml() {
let toml = generate_fuzz_cargo_toml("aprender");
assert!(toml.contains("aprender-fuzz"));
assert!(toml.contains("libfuzzer-sys"));
assert!(toml.contains("cargo-fuzz = true"));
}
}