ci: prove spark/gate_machine in CI (no workflow runs gnatprove) #115

spark/ (the gate_machine SPARK model mirroring squabble-core::gate) is proved only locally. No workflow runs gnatprove, so the Rust and SPARK mirrors can drift apart without any red signal. #114 is the latest change to both sides.

Acceptance criteria

• A workflow runs gnatprove -P spark/squabble_gate.gpr -j0 --level=2 on every PR that touches spark/** or crates/squabble-core/src/gate.rs.
• It fails the job on any unproved check. Grep the summary so that a medium/high line fails, not just a non-zero exit.
• Positive control, recorded in the PR: a deliberate mutant, e.g. Evaluate testing /= Passed, turns the job red.
• The toolchain is pinned (alire gnatprove version) and actions are SHA-pinned per estate policy.
• The job is added to main's required status checks once it has run green.

🤖 Generated with Claude Code

https://claude.ai/code/session_0136eszqrQ53Kj7aBH1D4rXK