# The Dark Factory — verifier kit

This kit lets you re-run our discharge calculation locally and compare
the result against the numbers we publish at
<https://thedarkfactory.co.uk/results/>. Everything you need to verify
our claims is in this directory; nothing about the factory's pipeline
is.

## What's in the kit

```
README.md              this file
Makefile               targets that run gnatprove against each routine
expected-results.txt   the numbers we publish — for diff-against
routines/              one subdirectory per routine, each containing:
                         <pkg>.ads                  the emitted spec
                         <pkg>.adb                  the emitted body
                         <routine>.f                the original Fortran reference
                         build.gpr                  GPR file for gprbuild + gnatprove
```

## What's NOT in the kit

- The factory itself — the translator, the type-resolver, the spec
  expander, the body-fill stage, the algorithms catalogue, the
  per-stage prompts, and the prover-feedback loops. These are how the
  output gets produced. The factory is the moat; the output is what
  you can verify.
- The reference body the factory rejected during the audit on
  dgeqrf (see `/blog/2026-05-24-old-code-new-code.html` for that
  story). Only the verified, behaviourally-tested body is in the kit.

## How to install gnatprove

You need GNAT (an Ada compiler) and SPARK Pro (the prover toolchain).

- **AdaCore Community edition** (free for non-commercial use) — the
  fastest path. Download from
  <https://www.adacore.com/community>. Includes both GNAT and SPARK.
- **Alire** (the Ada package manager) — `alr toolchain --select`
  picks up GNAT; SPARK Pro is a separate AdaCore product. Suitable
  for the GNAT half only.
- **Native packages** — Debian / Ubuntu / Fedora all ship GNAT in
  their repos. SPARK Pro is not in distro repos; install via
  AdaCore Community.

Verify your install with `gnatprove --version`. We ran this kit
against `gnatprove 13.2.1 / 28fc3583`. Earlier versions back to
12.x should also work; later versions have slightly different
output text.

## How to verify one routine

```sh
make ROUTINE=lapack-dgeqrf
```

Runs `gnatprove --level=1` on the spec + body for that routine. The
final line of output is the prover's `Total` summary. Compare against
the row for that routine in `expected-results.txt`.

## How to verify all routines

```sh
make all
```

Runs gnatprove on every routine in `routines/` sequentially and writes
a summary table to `actual-results.txt`. Compare with
`diff expected-results.txt actual-results.txt`.

## Interpreting the result

`gnatprove --level=1` produces a discharge table like:

```
SPARK Analysis results        Total    Flow   Provers   Justified  Unproved
Run-time Checks                 220    .      178       .          42
Functional Contracts             82    .       70       .          12
Total                           432    115    263       .          54 (13%)
```

The `Total` line is the headline number. `432` total proof obligations,
`54` unproved, so `(432 − 54) / 432 = 87.5 %` discharged. That's what
we publish on the site.

What the unproved obligations mean varies. For the routines on this
site they're typically one of three classes:

1. **Run-time checks at theoretical FP extremes** — e.g.
   `Float overflow check might fail`. Tightening the Pre-condition on
   the input domain closes these.
2. **Proof gaps caused by unaxiomatised library functions** — e.g.
   `Exp` from `Ada.Numerics.Generic_Elementary_Functions` is declared
   `SPARK_Mode => Off`, so the prover doesn't know `Exp(x) ≥ 0`.
   A `pragma Assume` after each Exp call closes these.
3. **Inductive arguments at level=1** — re-run at `--level=2` (more
   provers, more steps) and most of these close.

None of the unproved obligations on the routines in this kit are
body-correctness issues. They're proof-engine limits documented in
the AdaCore SPARK reference manual.

## What you should expect

If our claims are accurate, your output will match
`expected-results.txt` line for line, modulo prover wall-time. If it
doesn't, please email **tony.gair@thedarkfactory.co.uk** with your
output — we want to know.

## License

The kit's Ada source files inherit the licence of the original Fortran
reference (modified BSD for the Netlib BLAS/LAPACK routines, public
domain for the FFTPACK and the Phase 3 textbook-reference kernels we
wrote from scratch). The kit's Makefile and README are Apache 2.0,
The Dark Factory Ltd.