Is SPARK in ADA a theorem prover?

General
,
1

This might be a dumb question, but is spark in ada similar to Z3 or lean 4? As in, can it be used to formally prove stuff like theorems or whatever?

2

Hi,

Someone with more expérience in SPARK will give you an answer.

But, gnatprove that prove your SPARK code, uses z3, in addition with other tools : 7.1. How to Run GNATprove — SPARK User's Guide 27.0w

3

SPARK isn’t a theorem prover, rather it’s a programming language derived from Ada plus static analysis tools that allows you to prove things about programs such as absence of run-time errors and functional correctness. So you write SPARK code which can be compiled with a compiler such as GNAT, then use the GNATprove tool to perform static analysis on the code which will try to automatically prove various properties on the code.

Behind the scenes, GNATprove uses Why3 and automatic theorem provers like Z3, CVC5, Alt-Ergo, and COLIBRI to prove various checks on the code. For example, given the following function in SPARK:

function Increment (X : Integer) return Integer is (X + 1)
with Pre  => X < Integer'Last,
     Post => Increment'Result = X + 1;

GNATprove will emit a verification condition (VC) for the addition X + 1 to try to prove that the result of the addition fits within the bounds of type Integer, assuming that X < Integer'Last from the precondition. Another VC will also be emitted for the postcondition to try and prove that the returned value is equal to X + 1.

So SPARK isn’t used to prove mathematical theorems, but rather proves various properties about the program such as absence of run-time errors (no arithmetic overflows, buffer overflows, division by zero, etc) as well as functional properties expressed in contracts (preconditions, postconditions, invariants, predicates, etc).

That’s a brief overview which I hope answers your question. If you want to learn more I recommend checking out AdaCore’s Learn website. This page provides a nice overview of SPARK: SPARK Overview - learn.adacore.com

4 Likes
4

Hm, then I guess a follow question is, is there a way to do theorem proofs in Ada? Like a library for it or something?

5

This isn’t specifically what you’re looking for, but you can prove algorithms with SPARK:

I’m also aware of some crypto with his stuff written in SPARK, which result in them being provable (it’s no longer maintained though)

1 Like
6

This article is pretty close to what I was originally imagining SPARK to be:

Seems like AdaCore already has a library that can do proof solver stuff?

7

AdaSAT is open and used in production: GitHub - AdaCore/AdaSAT

There are libraries that already have structures fully proven that you can build on them and create more complex proofs, the main one being SPARKlib: GitHub - AdaCore/SPARKlib

SPARK is more about proving code than rather proving the problem behind it. So in a way, SPARK is not like Rocq/Coq or Lean4, but it uses the same underlying principles and tools. If you want Satisfiability Theory (SAT) those systems may be better (you can check out SMT-Lib too) SMT-LIB The Satisfiability Modulo Theories Library or Operational Research tools such as HiGHS.

Best regards,
Fer

EDIT: I incorrectly stated that AdaSAT was a Proof-of-Concept when in reality it is used in production as corrected by Fabien.

8

For context, what I’m trying to do is create a “proof solver” for Tetris.

Think something like stackrabbit for chess, but for Tetris instead.

So, given a Tetris board, is it solvable, or has it reached a fail state?

So, I would like to be able to “prove” that certain states are valid and other states aren’t. Tbh, this feels like something more suited to Haskell, but I want to have a graphical display/simulation written in Raylib or SDL, and Haskell isn’t great for actual gameplay code from what I’ve seen.

9

That sounds doable in SPARK, and you might fight this blog post interesting which implements Tetris in SPARK on an Arm Cortex-M4: https://www.adacore.com/blog/tetris-in-spark-on-arm-cortex-m4

10

AdaSAT is used in production by langkit_support and all the libraries and tools that depend on it (Libadalang, VS Code pluging, GNAT Studio, GNATformat, GNATdoc, etc.).

See here: Solving Sudoku with AdaSAT | AdaCore

3 Likes
11

You could look into Coq which is a theorem prover written Galilea I think the language is called. There is also another theorem solver called Isabelle.

12

Coq is not written in Gallinea…

OCaml is the implementation language of the Coq tool, and Gallina is the language you use within Coq to encode and verify properties. Gallina serves as the core language for the logical framework Coq operates on.

13

I see, I stand corrected!