Proof modules

A proof module is a Clojure namespace that adds declarations to an environment. Its shape is data, so you can read and check the corpus’s whole dependency graph before installing anything.

;; src/rainbow/math/rational/signed/lp_duality_on.clj (abridged)
(ns rainbow.math.rational.signed.lp-duality-on
  "LP weak duality and the optimality certificate, quantified over the rows and ..."
  (:require [rainbow.module :as module] ...))

(def theorem-specs                                   ; the declarations: statement + proof
  [double-counting-spec weak-duality-spec optimality-certificate-spec])

(def deps
  "Modules this one installs on top of (see rainbow.module)."
  '[rainbow.math.rational.signed.lp-duality rainbow.math.rational.signed.pointwise-order])

(defn install
  "Adds this module's own declarations."
  [checked-environment]
  (-> checked-environment (support/extend-with :signed-lp-duality-on theorem-specs)))

(defn extend-environment [checked-environment]      ; installs deps, then the module
  (module/install-module checked-environment 'rainbow.math.rational.signed.lp-duality-on))

• theorem-specs: maps with a :name, :universes, a :type (the statement) and a :value (the proof).
• deps: the modules whose declarations this one refers to.
• install: adds only this module’s own declarations, each checked by the kernel on the way in.
• extend-environment: what callers use. It installs the dependencies, then the module.

theorem-ids maps each theorem’s alias to its id, and lein verify uses it to find the theorems to check again. Definitions go in definition-specs and definition-ids. Declarations and modules shows how a spec becomes a declaration.

How dependencies are installed

rainbow.module/install-module (source) walks deps recursively and installs each module after everything it depends on, siblings in listed order. A cycle is an error naming the module where it was found.

Each module is installed once. The environment records which modules it has, so a shared dependency costs one install however many paths lead to it. The record does not change the environment id.

Before 1.0, one module deep in the corpus performed 10,343 module installs for 184 distinct modules and took over an hour. With declared dependencies it installs in minutes. Each proof module can also be installed on its own, and the coverage gate in test/rainbow/coverage/ fails if a proof module is reached by no test.

Custom logic, such as installing a lemma only if it is missing, goes in install and runs after deps. A call to another module’s extend-environment from there still installs that module at most once. This layer is not trusted: a missing dependency shows up as the kernel rejecting a declaration that names an unknown constant.

Writing a new module

Put a new theorem in a module under src/rainbow/math/ or src/rainbow/algorithms/proofs/ with theorem-specs, deps, install, extend-environment and theorem-ids. Add a test that re-checks each declaration and asserts an empty axiom profile, following any *_test.clj next to the module you extend. Then lein verify <your.namespace> should print each theorem as checked and axiom-free. Prove a rational lemma walks through one.

Name binders uniquely in helpers that build terms. A helper that binds a fixed name such as 'x captures a caller’s variable of the same name, and the failure shows up far away as a type mismatch.