Proof bundles

A proof bundle carries declarations proved on top of a public base, with their proof terms, so lein verify --bundle can check them with the kernel alone, without the program that found the proofs. Share and check a bundle walks through one.

Contents

rainbow.main/proof-bundle builds a bundle from a base environment and an extended one, and rainbow.main/write-bundle! writes it as EDN (source).

• base: a checkpoint path, the proof modules installed on it in order, and the resulting environment id
• declarations: each new declaration, or one that gained an alias, in installation order, with its proof term
• claims: each claimed alias with its declaration id and axioms
• the reduction budget used, and free-form metadata

Schema 1 has a :declarations vector. A bundle that adds inductive types uses schema 2, with an ordered :entries vector, so each inductive block is checked whole before anything that uses its members.

How a bundle is checked

lein verify --bundle <file> stops at the first step that fails:

1. The base checkpoint replays through the kernel.
2. The named modules install on it, and the result has the recorded environment id.
3. Each entry goes through kernel/add-declaration, or kernel/add-inductive-block for an inductive block. The kernel recomputes each declaration’s id from its content.
4. Each claim resolves to its recorded id, checks, and has the recorded axioms.

A rejection names the entry and the kernel’s reason. An exhausted reduction budget means undecided, and the message suggests a larger --reductions (Commands).

Encodings

Proof terms repeat themselves. The RH2EDIN c2 LP certificate’s proof has 46,325 term nodes, 617 of them distinct, and names 26 constants 21,938 times. Written as a tree, three quarters of the file is the same 71-character hashes. The shared encoding, schema 3, writes each distinct subterm and constant once.

The binary file from lein share-bundle --binary stores the shared bundle with a one-byte tag per node, back references as variable-length integers and constants as raw 32-byte hashes: 5,591 bytes for the c2 certificate, 3,623 gzipped. lein verify --bundle reads all three forms.

lein share-bundle in.edn out.edn            # plain to shared
lein share-bundle --binary in.edn out.bin   # to the binary file
lein share-bundle --plain in.edn out.edn    # back to plain

Decoding rebuilds exactly the plain bundle’s declarations, with the same ids. The decoder refuses a child that is not an earlier node, a constant out of range or an unknown tag, and its output still goes through kernel/add-declaration, so a decoding defect gives a refused bundle. Change one price in a bundle and the kernel rejects it, with its own reason.