The gate, and its edges

The last two chapters showed how to write a law and a proof, and what they cost. This one is about the gate itself — bend PROOF.bend, the command that returns the verdict — and about what that verdict is worth. Both chapters came back to the same small print, and this is where it gets exact: “All terms check.” is the only evidence, and it is not evidence at all. Every output below is pasted from a real run of tools/drift/gate_matrix.sh.

The distance between two sentences

What a CI job would like to say is: this property cannot regress. What the gate can honestly say is: this proof checks. The distance between the two sentences has three shapes, and each one is a small file.

The escape hatch

Start with a law that is false — not subtly, plainly:

law false_law:
  for x: Nat
  {x == 1n : Nat}

No proof of this exists, so here is an “implementation”:

@unsafe
def Laws.false_law(x):
  Laws.false_law(x)

@unsafe is the guide’s one decorator: it tells the checker not to ask for a decreasing argument, an exemption real programs need when a loop cannot be proven to terminate. It also moves the def outside the proof’s guarantees — a function allowed not to terminate inhabits every type — so it inhabits {x == 1} as easily as anything else. It compiles, and bend PROOF.bend prints:

All terms check, but 1 def relies on unsafe or foreign code:
- LAWS.false_law

and exits 0. This is not a bug and not a secret — it is the first entry in upstream’s WONTFIX.txt, under DESIGN:

@unsafe programs check and exit 0 (#776, #805) The checker prints “All terms check, with N unsafe annotations.” and exits 0. @unsafe is a choice the author made in the source; read the note, not the exit code.

(Upstream’s note still shows the older wording; the message 2.0.24 prints is the one quoted above.)

Two measured details about the note. First, the count covers everything the run loads: one @unsafe def anywhere in the import graph — even one no proof touches — degrades the message. Second, the count is over defs, and the message names them: the run above lists - LAWS.false_law under the verdict. A ~ template instance does not appear in it — the disclosure is about what relies on unsafe or foreign code. The message is still something to read, not a bit to parse.

The vanishing spec

LAWS.bend is the human’s file, and the gate is a check on the files it is handed — whatever is there. Delete the law and see. With the proof def left behind, the report is:

Error:
- expected : '->'
- observed : ':'
Location:
4>| def Laws.add_zero_law(x):

A parse error that names nothing. It reads as “add a return type” — the wrong repair for a law that went missing (this message is filed upstream as bendlang/bend#850). Delete the def too, and:

All terms check.

Zero laws checked, all of them fine. What stops the quiet half of this is one check, added in 2.0.8: a PROOF.bend that sits beside a LAWS.bend must import it.

$ bend PROOF.bend        # with the import line removed
bend: PROOF.bend must import ./LAWS.bend (see bend --help)

That closes “the AI skipped the law file”. It cannot close “the law file was edited”, because the law file is the spec — and a spec the constrained thing can edit is not a spec. The gate checks that two files agree; keeping them in agreement is a social arrangement, and it is the load-bearing part.

The CI that greps wrong

Three plausible ways to wire the gate into CI, run against the @unsafe fixture above:

The exit code is fooled because the design says so. The substring grep is fooled because All terms check, but 1 def relies on unsafe or foreign code: contains All terms check. Only the exact-line match notices the difference.

The recipe

bend PROOF.bend > gate.out 2>&1 || exit 1
grep -qx 'All terms check.' gate.out || exit 1

Two lines, one job each. The first fails on compile errors, open laws (1 TODO found.), and the import check. The second insists on the verdict line exactly — no with N annotations, no skip, no partial run. If a future version rewords the line, this CI goes red; for a check that depends on a message, that is the correct failure mode, and gate_matrix.sh is what notices it first.

What the gate does guarantee

Stated with the same care, because it is not nothing:

• The break tests. Change the implementation and the gate closes; restore it and the gate opens. Five of the six patches the previous chapters record — the three life_par ones and two of the three life_anim ones — were re-run while this chapter was written, and every one still closes the gate. (Each patch asserts it changed exactly one spot before writing, and every file was restored byte-identical — the discipline of the appendix, re-used.)
• Open laws are refused. A declared law without a proof is 1 TODO found. The code is incomplete, and not a valid proof yet. — exit 1. A ?TODO hole is the same.
• Skipped law files are refused (the import check above).
• It is fast. The two Life proofs check in 0.07 s and 0.06 s — re-measured while writing this chapter. None of this is bought with patience.

The Bend Hub

The previous chapter stopped at a library gap. Its index-safety law needs arithmetic facts that Base does not state. The Bend Hub is where Bend programs can share facts such as these. It is a public, content-addressed package store. It needs no account, and packages have no names or version numbers. A package’s content hash is its identity.

Open the Hub to browse packages or paste a hash into its search box. To use a package, copy its import line into a Bend file:

import 0x1ee1b5d0c2a66817bf368b849f3117fc/nat.bend as Nat

The first bend run downloads the package to ~/.bend/lib, checks its content against the hash, and then checks it with the rest of the program. The alias on the right becomes the namespace. For example, a proof can now rewrite with %Nat.add_assoc(a, b, c) instead of defining associativity again.

To publish a package, check its entry file and then pass --publish:

bend nat.bend
bend nat.bend --publish

The second command uploads the file and its imports, then prints the import line for the new hash. Changed content produces a new package and a new hash. Existing imports stay pinned to the bytes that their authors checked.

Lemmas contributed by this book

The Life proofs exposed three gaps in Base. We extracted their reusable lemmas and published them to the Hub:

• nat.bend contains six facts about Nat.add: zero and successor in both rewrite directions, associativity, and commutativity.
• string.bend contains five facts about String.append and String.reverse.
• list.bend contains six matching facts about append, reverse, and length for List.

The repository keeps the package sources and publication log. Anyone can open a package on the Hub, read its source, and run bend on it. A valid package prints All terms check. The original index-safety wall still stands because it needs Nat.cmp facts that these packages do not contain. The Hub does not remove the proof work; it lets one proof publish that work for the next one.

The three edges

Keep them in view and the guarantee is shaped like this: a change that breaks a stated property cannot pass unnoticed, provided three things stay separately true.

1. No @unsafe in the import graph of anything you gate. It is not a scan the compiler does for you; it is a choice in your sources, and one grep if you want a machine to check it.
2. The spec file is the humans’. The compiler can refuse a proof that skips its laws; nothing can refuse a law that was deleted. That half is a review habit, not a check.
3. The CI reads the verdict line exactly, in the two lines above.

The gate is a young instrument, and this chapter is its boundary map: what it proves, what it only promises, and how to tell which one you are looking at. Within those edges, “All terms check.” means exactly what the previous two chapters said it means. Outside them, it means whatever you let it mean.

Running it

sh tools/drift/gate_matrix.sh

Seven fixtures, seven lines, one per case — the false law, the TODO, the missing import, the emptied spec, the stray @unsafe, the stray proof def. Run it after a bend update; the day one of those lines changes is the day the boundary moved.