Add criterion benchmarks for per-engine throughput (LC, SCH, SC, HS, CFDP)

[avrabe]

Part of the V&V coverage initiative.

Problem

relay is the flight-software stream substrate — engines run at cycle rates measured in Hz to kHz. Silent performance regressions in any of LC/SCH/SC/HS/CFDP could push a deployed system past its WCET budget (which Lean proves — see proofs/lean/WcetAnalysis.lean and CompositionalWcet.lean). A criterion regression gate is the standard defense.

Recognized as evidence under ISO 26262-6 Table 10 row 1e ("performance test", HR at ASIL D).

Acceptance

• benches/engine_throughput.rs per engine (or one file with grouped criterion benches):
  • LC: violations per cycle under realistic reading distributions
  • SCH: actions per tick at max task load
  • SC: dispatches per tick under contention
  • HS: alerts per check under load
  • CFDP: PDU actions per event
• Per-cycle wall-time SLA baseline captured and checked in CI
• Nightly job persists history for trend visibility
• Traceability in rivet.yaml: link benchmarks to Lean WCET theorems

Notes

• Benchmarks should reflect per-cycle budget; not microbenchmarks of isolated functions
• Pair with Kani state-machine proofs for complete engine verification story
• Realistic inputs: reuse fuzz corpus where viable