[tonygair]

Add a SPARK / GNATprove language track

Hello — this adds SPARK (the provable subset of Ada) as a fourth language
track alongside Dafny, Verus and Lean, with gnatprove as the checker.

There is no CONTRIBUTING.md and no documented process for adding a
language, so this is written by reverse-engineering the existing
benchmarks/dafny and benchmarks/verus layouts. If any of it cuts
against how you would rather it were done, say so and I will redo it — the
shape is not precious, and I would rather match your conventions than mine.

What is here

benchmarks/spark/	26 seed tasks, with reference solutions
scripts/spark_verify.py	the checker
scripts/spark_negative_control.py	evidence that the checker rejects things
src/spark/prompts-spark.yaml	generation and repair prompts
config/language_config.toml	a [spark] section
src/vericoding/processing/cheat_checker.py	SPARK bypass patterns

The task shape is the one you define — spec → verified code, with the
specification fixed and the model writing the body and its proof
annotations.

The seed set

26 of the 58 numpy_simple Dafny tasks, translated one for one with your
Dafny spec as the authority. All 26 reference solutions discharge at
--level=2: 387 proof obligations, 0 unproved, 0 justified, about 45 s
for the whole set.

The other 32 were skipped rather than weakened, grouped by what blocks
them, each group with its reason written down in benchmarks/spark/README.md
— Dafny real (6), recursive spec functions (6), multiset/permutation
postconditions (3), seq-of-seq matrices (8), strings (2), number theory (2),
higher-order specs (1), Dafny datatypes (1), result-dependent shape (1), one
with no non-degenerate bounded domain, one near-duplicate. No postcondition
was weakened to make a translation land. The skip list is written to be a
to-do list for whoever grows this next, including us.

Two adaptations are uniform, are properties of the language rather than of
any task, and are declared in the README rather than buried:

• Bounded integers. Dafny's int is mathematical; Ada's Integer is
  not, and GNATprove makes you prove every operation in range. Each task
  fixes a finite domain. This makes the SPARK tasks strictly harder than
  their Dafny originals in one respect — an implementation must also prove
  absence of overflow.
• Explicit division semantics. Dafny's / and % on int are
  Euclidean; Ada's / truncates and Ada's mod is floor-mod. They agree
  only for a positive divisor, so the two division tasks restrict the
  divisor and say so, rather than quietly proving a different operation.

One thing worth a look even if you take nothing else

The harness fails any submission where GNATprove emitted zero checks.

GNATprove exits 0 with an empty summary for code it never analysed — an
empty SPARK_Mode region, a body excluded from analysis. A harness that
checks only the exit status and the unproved count scores that as a pass: a
green light for a proof that never happened. We hit this in our own work and
only caught it because something else was watching, so it is a rule here and
one of the four cases in the negative control:

mutant	harness verdict
wrong implementation	unproved — "postcondition might fail"
pragma Assume bypass	cheat
SPARK_Mode => Off — the empty-summary case	cheat
syntax error	compile_error

Baseline unmutated reference: pass. All four rejected. python scripts/spark_negative_control.py runs it.

The equivalent hazard may exist for the other tracks — a Lean file that
elaborates nothing, a Verus body behind #[verifier::external] — and if so
it is worth the same guard there. That is offered as a question, not a
claim about your harness.

Notes on the file format

Ada wants the package specification and body in separate files, so a task is
a single GNAT multi-unit .ada source that the harness runs gnatchop over
before proving. Two consequences, both documented in the track README:
vc-spec comes before vc-helpers (helpers live in the body, which cannot
precede the spec), and vc-spec carries the non-editable package frame so
that every byte of the file stays inside a section and the JSONL form
round-trips exactly.

The unfilled body carries pragma Assume (False), playing the part your
Dafny templates give assume {:axiom} false.

Reference solutions are shipped in numpy_simple/solutions/, which the
other tracks do not do. They are there so nobody has to take the seed set's
dischargeability on trust, and so a harness change can be regression-tested.
The harness never reads them. Happy to drop them if you would rather the
tracks stayed symmetrical.

Running it

Needs gnatprove and gnatchop on PATH; via Alire,
alr toolchain --select then alr install gnatprove. Verified on FSF GNAT
15.0 / SPARK with Why3 1.7.1, Alt-Ergo 2.6.0 and cvc5 1.2.1.

python scripts/spark_verify.py --json benchmarks/spark/numpy_simple/solutions/*.ada
python scripts/spark_negative_control.py

Where this comes from, and what we are offering

We run a small production shop that forges SPARK cores from prose
specifications with local models and admits nothing that a second machine
has not independently re-proved under GNATprove — so the seed set and the
harness are a slice of something already in daily use, rather than a
one-off written for this PR.

We would like to grow the track — the matrix group and the recursive-spec
group are the obvious next slices, and we are happy to do that work whether
or not this lands as-is. If you would rather a smaller PR, or the tasks
without the reference solutions, or a different file format, tell us which
and we will send that instead.

— The Dark Factory