Add Kani harnesses for ARINC653 solver invariants (constraint-satisfaction / MILP)

[avrabe]

Part of the V&V coverage initiative.

Problem

spar has a strong Lean proof portfolio for scheduling theory — Liu–Layland rate-monotonic bound (proofs/Proofs/Scheduling/RMBound.lean), EDF optimality, response-time analysis. The Rust solver implementation that consumes this theory is unverified today: spar-solver (constraint satisfaction, MILP), and spar-codegen that emits schedules.

Acceptance

• Kani harness for solver soundness: if the solver reports "schedulable", the schedule satisfies all task deadlines
• Kani harness for solver invariants: priority monotonicity, deadline monotonicity, zero-laxity handling
• Kani harness for codegen: emitted schedule respects solver output (no reordering, no drops)
• Harnesses under spar-solver/tests/kani_*.rs, spar-codegen/tests/kani_*.rs
• Traceability in rivet.yaml: link Kani harnesses to the Lean theorems that state the mathematical property
• CI job: bazel test //... covers Kani targets after rules_verus / Kani integration

Notes

• The Lean proof RMBound.lean:49 proves rmBound(n) ≥ ln 2 — the implementation must not admit schedules violating this
• Bounded Kani with realistic task counts (e.g. up to 8 tasks) is sufficient for DO-333 credit; unbounded is a stretch goal