Add criterion benchmarks for scheduling solver (ARINC653)

[avrabe]

Part of the V&V coverage initiative.

Problem

spar's MILP / constraint solver is the slowest inner loop in the scheduling flow. Silent performance regressions here cascade into unusable schedule-analysis runtimes on real workloads. No criterion bench gate today.

Evidence under ISO 26262-6 Table 10 row 1e ("performance test", HR at ASIL D). Also strengthens the Lean → Rust refinement story: Lean proves scheduling theory holds, criterion proves it computes in realistic time.

Acceptance

• spar-solver/benches/solver_benchmarks.rs with groups:
  • Small schedule (≤8 tasks): micro-benchmark of per-constraint cost
  • Medium schedule (≤64 tasks): representative avionics/automotive workload
  • Large schedule (≤256 tasks): stress / regression detection
  • Worst-case constraint density (hardest inputs seen in fuzz corpus)
• spar-codegen/benches/codegen_benchmarks.rs for schedule emission
• CI PR-gate: bench --no-run sanity
• Nightly full run with persistence
• Traceability in rivet.yaml to the scheduling theorems and SLA budgets

Notes

• Solver may have non-monotonic cost curves on adversarial inputs — use criterion::BenchmarkGroup::throughput appropriately
• Reuse fuzz corpus (separate issue) for realistic hard inputs