Proving and writing SPARK proofs¶

adacovex runs gnatprove, reads its summary, and grades the result against the SPARK assurance levels. This page is the guide to both halves: how proving works under adacovex, and how to write proofs – contracts in your own code, and – when the code is vendored and cannot be modified – proof patches that add the contracts for you.

Proving a project with adacovex¶

adacovex prove --target=.

The prove subcommand (full options: CLI reference – the prove subcommand):

Resolves gnatprove without requiring the target to declare it: manifest pin > global pin > $PATH > cached toolchain > download. Full order and per-method detail: Architecture – GNATprove toolchain resolution.
Runs gnatprove against the target (or against a patched tree copy when proof patches are present – see Proof patches below) and writes the summary to <target>/obj/gnatprove/gnatprove.out – the same location the assessment pipeline discovers.
Falls through to the full assessment. The assessment parses the fresh summary. One command both proves and assesses. The --require-* CI gates apply to the proof run directly (--require-spark=Platinum --require-proof=100 and more; see CLI reference – CI threshold gates).

The result cache serves unchanged targets so repeated runs are cheap. --force bypasses the cache and forces a full gnatprove reanalysis. A target without a gnatprove.out at all is graded Stone with proof metrics N/A. Run prove to generate one.

The two caches – why prove timings vary¶

prove interacts with two independent caches, and knowing which one is cold explains every timing you will see:

The result cache (~/.adacovex/cache/<version>/, or --cache-dir) is adacovex’s own store, keyed on the content hash of the proof inputs (every .ads/.adb under the target plus the .gpr and the option string). A hit serves the stored proof and skips gnatprove entirely – this is the short-circuit that makes an unchanged tree prove in tens of milliseconds.
The gnatprove session store (<target>/obj/gnatprove/) is gnatprove’s internal per-unit session. When adacovex does spawn gnatprove (a result-cache miss), the session decides the cost: a complete session re-analyses only changed units; a wiped or partial session re-analyses from scratch.

Concretely, for an unchanged target:

Result cache	gnatprove session	What a `prove` run costs
hit	any	~tens of ms – the short-circuit
miss	complete	a few seconds – gnatprove re-verifies quickly, then re-stores
miss	wiped	the full solver run – tens of seconds on a large proof
miss	partial	lands between the two – gnatprove re-analyses the missing units

The partial-session row is the easy one to misread: a targeted gnatprove -u <unit> run, a killed proof, or a hand-delete under obj/gnatprove/ leaves the session incomplete, and the next result-cache miss re-proves just the gap – so consecutive runs alternate between instant and multi-second. Once one full prove completes, the session is complete again and back-to-back runs stay at the short-circuit. This is content-keyed cache behaviour, not a cache fault: any source edit (or a docs edit that changes the bundled manual in src/) legitimately changes the key and re-proves once.

make bench samples both extremes (prove warm = hit; prove cold = result cache and session wiped), so its numbers are always one of the stable shapes. Category definitions and current figures: Performance.

What a proof contains¶

gnatprove reports verification conditions (VCs) per check category. The summary in gnatprove.out breaks them down as:

Category	What it covers
Run-time checks	Index bounds, overflow, division-by-zero, range checks – absence of run-time errors
Assertions	User `pragma Assert` statements and pre/postcondition checks
Functional contracts	`Pre` / `Post` / `Global` contract satisfaction
Data dependencies	Flow analysis: uninitialized reads, effective `Global` contracts
Initialization	All objects initialized before first use
Termination	`Loop_Variant` / recursion bounds (subprograms proved terminating)

The honest proved count is total - justified - unproved (flow plus provers). The assurance level is derived from how many of each category were discharged:

Stone – no proof run or nothing analyzable;
Bronze – flow analysis clean (data dependencies, initialization);
Silver – run-time checks proved, assertions proved;
Gold – functional contracts proved on top;
Platinum – every VC proved: 0 unproved (and, in adacovex’s own gate, 0 justified – no pragma Annotate justifications).

Justified VCs count neither as proved nor as unproved. Only unproved VCs downgrade the level. For a DAL assessment, the level must meet the requirement of the tier (--dal=C needs Bronze, --dal=A needs Gold, and more) – see DAL levels.

Writing proofs: SPARK contracts¶

A proof starts with contracts in the source, written as Ada aspects:

package Body_Vec is

   function Clamp (Value : in Integer; Lo : in Integer; Hi : in Integer)
     return Integer
     with Pre  => Lo <= Hi,
          Post => Clamp'Result in Lo .. Hi;

end Body_Vec;

Rules that matter in practice:

SPARK_Mode => On selects what gnatprove analyses. Without it a unit is out of proof scope. It can be declared on the package (package P with SPARK_Mode => On is), on individual subprograms, or both – adacovex’s own source uses package-level On on pure units and per-subprogram On aspects inside default-off bodies.
A body is analysed only when the body itself opts in. Declaring SPARK_Mode => On on the spec does not make gnatprove analyse the body. The body must declare it too (on the package body line or per subprogram). This is the rule that makes proof patches necessary for vendored code – see below.
I/O bodies are skipped by design. A body that calls Ada.Text_IO (which is SPARK_Mode Off) cannot be analysed. gnatprove reports the unit out of proof scope. This never drags the assessed level down – it means those bodies are not proved.
Contracts are proved against the body. gnatprove proves that every possible body execution satisfies the declared Pre/Post. Callers must in turn establish the Pre before calling.
--steps controls the proof budget. gnatprove’s default step limit can produce solver-timeout false negatives. adacovex runs with --steps 10000 by default so such timeouts are not reported as unproved. An explicit --steps=N overrides.

The goal for a clean proof: every VC in every category proved, 0 unproved, 0 justified.

Proof patches: proving vendored dependencies¶

Patch files at <target>/.adacovex/patches/ exist so vendored code you cannot modify still counts toward the audit. Their best-known job is overlaying docstrings for strict-mode coverage. A patch can also carry SPARK proof aspects so vendored dependencies participate in the proof with real contracts – without forking or touching their sources.

Why proof patches are necessary¶

Three facts force the design:

Strict mode counts vendored code. By default adacovex scans every directory except the always-excluded ones. The excluded directories are .git, obj, tests, config, and .adacovex. A vendored dependency’s missing docstrings and missing contracts count against the target. --relaxed skips vendored dirs but drops the audit to a quick pass – not an option for a compliance assessment.
gnatprove analyses a body only when the body itself opts in. (The rule from Writing proofs above.) A vendored spec with no contracts contributes nothing to the proof. A vendored body without SPARK_Mode is skipped entirely.
The vendored sources are immutable. The dependency ships as-is. You cannot add contracts to it. Re-publishing a patched fork defeats the point of vendoring.

A proof patch is the merge of these three constraints. It re-declares the vendored spec with contracts (.ads patch). It opts the vendored body into the proof (.adb patch). The prove subcommand merges both into a patched tree copy before running gnatprove – the originals are never touched.

How proof patches are applied¶

Count_Proof_Patches scans <target>/.adacovex/patches/ for .ads and .adb files. A patch carrying any of SPARK_Mode, Pre =>, Post =>, or Global => is a proof patch. A docstring-only patch never engages the proof machinery. A target with no proof patches is proved against its own tree exactly as before.
Build_Patched_Copy copies the target tree (excluding .git, obj, and .adacovex) into <target>/obj/adacovex-proof/ and overwrites each proof-patched source with its merged form.
gnatprove runs against the copy’s root project and the resulting gnatprove.out is copied back to <target>/obj/gnatprove/gnatprove.out for the assessment pipeline.
Patch contents are folded into the prove result-cache key, so a patch edit invalidates the cached proof and forces a re-prove (--force also bypasses the cache).

The patched copy lives under the target’s obj/, so it is excluded from scanning, manifest graphs, and the prove input hash.

Writing a spec patch (`.ads`)¶

A spec patch mirrors the vendored spec: same package name, same subprogram declarations (with docstrings, since strict mode requires them), plus the aspects you want gnatprove to prove:

--  .adacovex/patches/demo/deps/vt100/vt100.ads
package VT100 with SPARK_Mode => On is

   --  Scroll a region of the screen up.
   --  @param From  Starting line of scroll region.
   --  @param To    Ending line of scroll region.
   procedure Scroll_Screen (From : in Natural; To : in Natural)
     with Pre => From <= To;

end VT100;

The merge splices the package-level aspect onto the original package declaration line and replaces each aspect-carrying subprogram declaration with the patch’s declaration block. Subprograms the patch does not re-declare with aspects are left untouched, so a patch can add a contract to one subprogram without disturbing its siblings.

Writing a body patch (`.adb`)¶

The spec patch declares the contracts. The body patch is what makes gnatprove actually analyse the vendored body (the body-must-opt-in rule). It lives at the body’s relative path and mirrors the body’s declarations with stub bodies that the merge ignores – the original implementation is preserved:

--  .adacovex/patches/demo/deps/vecmath/vecmath.adb
package body Vecmath with SPARK_Mode => On is

   function Clamp (Value : in Integer; Lo : in Integer; Hi : in Integer)
     return Integer with SPARK_Mode => On is
   begin
      null;  --  stub: the original body's implementation is kept
   end Clamp;

end Vecmath;

The merge replaces the original declaration (up to its is) with the patch’s aspect-carrying declaration and keeps the original body proper, so the copy gnatprove sees is package body Vecmath with SPARK_Mode => On is ... <original implementation> .... A fully SPARK-clean body needs only the package-level aspect. The per-subprogram aspect covers bodies with a mix of clean and I/O-bound subprograms.

Matching rules¶

The merge matches each patched declaration against the original by name and normalised parameter profile:

Matching is whitespace-insensitive. A single-line parameter list matches a multi-line one.
The default in mode is equivalent to a bare mode (X : in Integer matches X : Integer). in out and out are distinct modes.
an overloaded subprogram patches its exact signature – a patched two-argument Scroll_Screen replaces the two-argument original, never a same-named sibling;
a spec declaration terminates at its ;, a body declaration at its is;
a patched subprogram with no match in the original fails loudly (the patch is skipped and reported) rather than silently dropping the contract.

Worked example: `Vecmath.Clamp`¶

A vendored package whose spec and body carry no contracts:

--  demo/deps/vecmath/vecmath.ads (vendored, unmodified)
package Vecmath is
   function Clamp (Value : in Integer; Lo : in Integer; Hi : in Integer)
     return Integer;
end Vecmath;

--  demo/deps/vecmath/vecmath.adb (vendored, unmodified)
package body Vecmath is
   function Clamp (Value : in Integer; Lo : in Integer; Hi : in Integer)
     return Integer is
   begin
      if Value < Lo then
         return Lo;
      elsif Value > Hi then
         return Hi;
      else
         return Value;
      end if;
   end Clamp;
end Vecmath;

The two patch files from above (spec with Pre => Lo <= Hi, Post => Clamp'Result in Lo .. Hi, and body with SPARK_Mode => On) merge into the copy unchanged in behaviour. gnatprove proves the contract: 2 VCs (the Clamp postcondition and its termination check), 0 unproved. A caller in the target’s own code can then rely on the contract without the vendored sources ever changing.

When contracts prove – and when they are skipped¶

SPARK-clean body + body patch – gnatprove proves the patched contracts outright (the example above).
I/O-bound body (calls Ada.Text_IO, which is SPARK_Mode Off) – gnatprove skips the I/O bodies by design and reports the unit out of proof scope. The contracts are still declared and the mechanism is exercised, but the body is not proved – and crucially, it never drags the target’s proof level down. This is the VT100 dogfood case in Ada_CRDT.

Common pitfalls¶

Spec patch without a body patch. A SPARK-clean vendored body stays out of proof scope. gnatprove reports “no checks generated” or skips the unit. Add the .adb patch to opt the body in.
A patched declaration that does not match anything. Check the name and the parameter list (modes included) against the original. The merge reports could not be merged ... (unmatched subprogram or oversized file) and skips the patch.
Patching the wrong overload. The match is profile-aware, so a patch entry replaces exactly the signature it re-declares – verify you wrote the same parameter list as the overload you mean.
Expecting contracts to prove against a non-SPARK body. Ada.Text_IO and other SPARK_Mode Off dependencies cannot be analysed; the patch still applies, but the proof does not cover those bodies.