[Tristan-Stoltz-ERC]

Summary

Implements the next step after PR #2693: a dependency-free Rust validator/auditor for benchmark manifests and per-case evidence.

Included

• Strict JSON parsing with duplicate-object-key rejection and Unicode escape validation.
• Manifest validation for contract version, source identity and expected case count, generator recipe / seed / parameter digest, model scope, explicit unsupported constraints, candidate/baseline revision syntax, oracle identity, declared metrics and solver budgets.
• Report auditing that recomputes summary counts from case records, derives false-feasible / false-infeasible counts from explicit reference outcomes, computes feasible-reference cases found versus missed, and checks the exact SHA-256 of the manifest bytes.
• A run must be pinned to the manifest's candidate revision; outcomes distinguish feasible-claim, infeasibility-proof, no-solution, timeout, invalid-output, and not-run. A timeout or heuristic exhaustion is not an infeasibility proof.
• Hand-authored positive and negative fixtures, including measured false-feasible and false-infeasible cases plus a valid heuristic-no-solution case.
• Rust 1.96.0 workflow for cargo fmt --check, locked offline tests, and Clippy with warnings denied. A separate formatter workflow can apply pinned rustfmt without replacing or weakening the format gate.
• Published-source availability audit and a six-row JSON reference for the paper's Case9_50_0–Case9_50_5 aggregate results.

Published comparison work

The article's public page contains aggregate Table 6 values and Appendix A shape/fleet tables. Its Data Availability Statement says the underlying experimental data and simulation results are available from the corresponding author upon request. PR #2693 and Issue #2703 separate these published reference values from any local reproduction. The Case9_50_4 input is not yet reconstructed; no published-performance claim is made.

Limitations

• The auditor checks contract-specific semantics, not the full JSON Schema Draft 2020-12 language.
• It checks source/config digest syntax but does not fetch artifacts and authenticate their origins; the exact manifest digest is recomputed.
• The published benchmark reference file stores aggregate values only; it is not an instance dataset or a local result.
• No safety, industrial-performance or state-of-the-art claim is made.

Keep draft until formatting, tests and Clippy pass on the exact PR head.