The trusted base

A proof checked by Rainbow is as trustworthy as the code that checked it: four files. Tactics, proof search and the mathematics all go through them, so a bug elsewhere gets a proof rejected and cannot get a false one accepted.

The kernel: 1,712 lines

The functions to read first are infer and check, normalize and definitionally-equal?, add-declaration, add-inductive-block and axioms. The calculus describes what they check. The README calls them 1,712 lines “you can read in an afternoon”.

The size is pinned. A release test, v1_release_test, fails if these four files change length, and CI checks the line count on every push. Version 1.1.0 made checking 24 to 123 times faster, with native natural-number arithmetic pinned to six definitions by content id and a substitution that skips unchanged subterms. Version 1.4.2 added two checks for inductive types: constructor fields are checked against the type’s universe, and a proposition with two or more constructors can no longer be eliminated into a larger universe. Version 1.4.4 made the kernel compare universe levels by value and gave constructors and recursors the axioms their types mention (CHANGELOG). Version 1.5.0 added lazy conversion in type checking (CHANGELOG). Version 1.5.2 fixed a defect by which two different declarations could get the same content id: the canonical encoding now refuses strings that are not well-formed UTF-16, and add-declaration and add-inductive-block refuse an id that already names different content (CHANGELOG). Version 1.5.5 fixed eta contraction, which could capture a variable, so the kernel treated two different functions as equal and accepted an axiom-free proof of forall R : Prop, R; every earlier release is affected. It also makes an axiom pass on the axioms its own type uses (CHANGELOG).

Below the kernel

The kernel trusts the Clojure reader and compiler, the JVM, and the JDK’s SHA-256 for content ids. A collision would let two declarations share a name.

Outside the kernel

• Tactics, such as the ring normalisers and the Bool.rec case-split helpers, and elaboration (rainbow.elaborate) produce terms the kernel checks. A wrong tactic yields a rejected term.
• Checkpoints: replay refuses a declaration the kernel rejects and a checkpoint or environment id that differs from the one recorded in the file, but anyone can recompute those ids. A checkpoint with a declaration removed and its ids rewritten replays, to a different environment id, and one edited to change what a name refers to replays to the same environment id with a different names id. Such an edit shows only as an environment id or names id that differs from the one a claim cites. Within one process, load-checkpoint reuses a successful replay for the same path and last-modified time (CHANGELOG).
• The declaration store, proof bundles and their encodings end in the kernel recomputing ids and checking terms.
• The scope lein verify prints comes from rainbow.main, using the kernel’s type inference and the proof term (What “proved” means).

Axioms are explicit

A logical principle, such as a classical one, enters only as an explicit axiom declaration (rainbow.math.profile). kernel/axioms computes each theorem’s axiom profile, lein verify prints it, and the tests assert it for each covered theorem. Most profiles are empty; What proved means says which theorems use axioms.