infra: install GNAT/SPARK toolchain on Claude Code runner (blocks Rust→Rust/SPARK migration routine)

[hyperpolymath]

Summary

The monthly Rust → Rust/SPARK migration step routine (one module per
run, scoped by STATE.a2ml [migration-roadmap.rust-to-rust-spark],
roadmap commit b942b9d) is blocked at run #1 because the Claude
Code runner has no GNAT/SPARK toolchain installed.

The routine's exit clause says:

If the gnatprove toolchain is unavailable, file an issue noting the
toolchain gap (it's the user's job to install on the runner) and
exit; do not produce a PR with unproven contracts.

This is that issue.

Probe results (runner @ 2026-05-01)

$ which gnatprove
(not found)
$ which gprbuild
(not found)
$ which alr            # Alire — Ada package manager
(not found)
$ apt list --installed | grep -iE 'gnat|ada|spark'
(none)
$ find / -name 'gnatprove' 2>/dev/null
(no results)

No gnat-*, gprbuild, gnatprove, or alr anywhere on the image.

Required toolchain

For the routine to land an actual SPARK companion (not just unproven
.ads/.adb skeletons), the runner needs:

Component	Purpose	Suggested source
gnat (Ada 2012/2022 compiler)	compile .ads/.adb	AdaCore Community / FSF GNAT / Alire
gprbuild	project build driver	bundled with GNAT
gnatprove (SPARK Pro / SPARK Community)	discharge proof obligations	AdaCore SPARK Community 2021 or newer
alr (Alire) — optional but recommended	per-project toolchain pinning	https://alire.ada.dev

Recommended path: install Alire and pin per-project, e.g.

# in spark/<module_name>/
alr toolchain --select gnat_native gprbuild
alr toolchain --select gnatprove
alr build
alr exec -- gnatprove --mode=prove --level=1

This keeps the toolchain reproducible and avoids polluting the system
GNAT (if any).

What the routine wants to do once unblocked

The roadmap candidate list (STATE.a2ml line 996, commit b942b9d) is:

1. src/rust/verification/axiom_tracker.rs — 4-level danger hierarchy
   • cap-at-Reject monotonicity
2. src/rust/integrity/solver_integrity.rs — SHAKE3-512 + BLAKE3
   binary integrity (hash mismatch ⇒ Failed)
3. src/rust/verification/certificates.rs — Alethe / DRAT / TSTP /
   OpenTheory cert parsing (totality + reject-malformed)

Each module gets a spark/<name>/ companion with:

• <name>.ads — spec with Pragma SPARK_Mode On + Pre/Post contracts
• <name>.adb — body
• <name>_proof.adb — equivalence proof against the Rust impl, OR a
  structured comment listing proof obligations + the gnatprove tactic
  expected to discharge each
• updated spark/README.adoc with how to run gnatprove

Each run advances by exactly one module so the user can review
between steps. This issue blocks run #1; once gnatprove is on the
runner, re-trigger the routine and it will start with axiom_tracker.

Roadmap drift since b942b9d (worth recording while we're here)

I diffed the three candidates against b942b9d so the next run doesn't
have to:

Candidate	Drift
src/rust/verification/axiom_tracker.rs	None (untouched since roadmap commit)
src/rust/integrity/solver_integrity.rs	1 line — std::fs::read_to_string → super::io::bounded_read_config (commit 9af87ba, F2 follow-up). Public surface unchanged; the SPARK port is unaffected.
src/rust/verification/certificates.rs	None (untouched since roadmap commit)

So no candidate's port plan needs revising — the drift is
mechanical and stays inside the function body, well below the
public surface that SPARK contracts will mirror.

Acceptance criteria

• gnatprove --version runs successfully on the Claude Code runner image
• gprbuild --version runs successfully on the Claude Code runner image
• (Optional) Alire (alr) available so per-project toolchain pinning is possible
• Re-trigger the Rust→Rust/SPARK monthly routine; it should advance to module Welcome to echidna Discussions! #1 (axiom_tracker) and produce a draft PR

Out of scope

• Adding GNAT/SPARK to the production CI matrix (the routine only
  needs it on the agent runner; CI checks for the SPARK companions can
  be added once we have at least one landed companion to gate on).
• Picking between FSF GNAT and AdaCore SPARK Community — operator's
  call; either works for the contracts the routine writes.

---

Filed automatically by the monthly Rust→Rust/SPARK migration routine
on its first attempted run (2026-05-01). Routine exited cleanly with
no PR.