Your first proof

ten minutes · three steps · nothing you have to take on trust

This is the beginner's path. You do not need to be a programmer, you do not need an account, and you do not need to tell us you exist. At the end of it your own computer — not ours, and not our word for it — will have checked the mathematics behind a real rule from the library.

If you already know your way around a prover, the full walkthrough goes further: building the front and checking every row of its truth table. This page stops at the proof, which is the part that matters most and the part that needs nothing installed.

What you are about to check

The rule is called brief-fill policy. It decides when an assistant may answer on its owner's behalf instead of asking them. Four claims are made about it, and all four are about to be tested on your machine:

These are not promises in a blog post. They are theorems, and a prover is about to try to break them.

Step 1 — get the prover

github.com/alire-project/GNAT-FSF-builds/releases/tag/gnatprove-16.1.0-1

Take the file for your machine:

Unpack it anywhere. There is no installer, nothing goes into your system, and nothing runs in the background. Delete the folder when you are done and it is as if it never happened.

One thing to do before you close that window. Because nothing was installed, your computer does not yet know where the checker lives. Tell it, for this terminal window only — nothing is changed permanently, and it is forgotten the moment you close the window. Replace the path with wherever you unpacked it:

# Mac and Linux
export PATH="$HOME/Downloads/gnatprove-16.1.0-1/bin:$PATH"

# Windows
set PATH=C:\Users\you\Downloads\gnatprove-16.1.0-1\bin;%PATH%

To check it worked, type gnatprove --version. If you see a version number you are ready. If you see command not found, the path above is not quite right — open the unpacked folder, find the bin folder inside it, and use that.

It is free and it is not ours — it comes from the Ada community, not from us. That is the point: the thing checking our work should not be a thing we handed you. One honest asterisk on “ten minutes”: the clock starts once this has downloaded, and it runs a few hundred megabytes — quick on a fast line, slower on a poor one.

Step 2 — get the rule

brief-fill-policy.tar.gz (6,918 bytes)

sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

Unpack it. Inside is the source, the proof, and a plain-English description of what the rule does.

You can ignore the checksum on a first run — the proof in step 3 does not depend on it. It is there for when you want to confirm that the file you received is the file we published, and it is the same one the catalogue names.

Step 3 — ask your computer to check it

You now have two unpacked folders: the checker, and the rule you downloaded in Step 2. This step happens in the rule folder. Open a terminal there — the same window you set the path in — and run two lines:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Wait. When it finishes, look for these two words:

0 unproved

That is it. That is the whole exercise. Nothing else needs installing, and this step works on a plain machine with nothing else on it — the prover you downloaded carries everything the proof needs.

What just happened

Your computer took the four claims above, tried to find a case where any of them fails, and could not — because there isn't one. Not "we tested it and it seemed fine". Not "the maintainer says so". A machine that cannot be talked round went looking for a counterexample and came back empty.

You did not trust us to tell you that. You watched it happen on hardware you own.

Optional — break it on purpose

This is the part worth doing if you have five more minutes, because a check that only ever says yes is not worth much.

Open brief_fill_policy_pkg.ads in any text editor and change the rule so that a missing store lets an answer through anyway. Run the same command again. It will refuse — and it will name the exact theorem you just broke.

That refusal is the entire security model. Ghillie installs nothing that does not pass this, so what you have just done by hand is what he does on your behalf every time.

What this does not prove

We would rather say this than have you find it out later. The proofs cover the decision rules — who may see what, what may leave, what a delivery must pass. They do not make the rest of the software magic, and we do not claim they do. That honesty is the deal, and it is the whole deal.

Where to go next

If it did not work, that is a finding and we would like to hear it. A refusal you cannot explain is more interesting to us than a success.