Skip to content
Flexiana
Menu
Solutions
How we work
Engineering
Work
Products
Company
Bring us a hard problem
Rainbow docs menu

Guides

Verify a module

Re-check two corpus modules in one run and find out which axioms they use. Two theorems in rainbow.math.finite.set-union use classical axioms; rainbow.algorithms.proofs.ahof.christofides has worked instances. Run the commands from the root of a v1.5.5 clone (see Install).

Verify

lein verify rainbow.math.finite.set-union rainbow.algorithms.proofs.ahof.christofides; echo $?
checkpoint artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz replayed: environment sha256:a41ba35a9f845aa04600620234dd1ccbb86969b09ffb14a44847da82ba4a5d5c names sha256:04959786090003bdfd133d7f4da521566de7ede77813ee1fa8aa3185284d193a
OK    rainbow.math.finite.set-union (5 theorems: 5 for all inputs, 0 definitional unfoldings, 0 worked instances)
       checked   for-all   set/finite-singleton-equivalence  axiom-free
       checked   for-all   set/finite-singleton-proposition-equality  axioms: logic/proposition-extensionality (sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088)
       checked   for-all   set/infinite-indexed-union-member  axiom-free
       checked   for-all   set/infinite-indexed-union2-member  axiom-free
       checked   for-all   set/infinite-union-equivalence  axioms: logic/excluded-middle (sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366)
OK    rainbow.algorithms.proofs.ahof.christofides (3 theorems: 0 for all inputs, 0 definitional unfoldings, 3 worked instances)
       checked   instance  christofides/tour-at-most-bound  axiom-free
       checked   instance  christofides/tour-over-bound-rejected  axiom-free
       checked   instance  christofides/tour-within-guarantee  axiom-free
0

About 20 seconds, mostly the checkpoint replay. It runs once however many namespaces you name, so name them all in one command.

Read the result

The first line says the base checkpoint replayed through the kernel. If it does not, the command prints FAIL checkpoint ... could not be loaded/replayed with the reason, and stops.

OK means the module installed, named at least one theorem, and every theorem checked. On a theorem line, checked means the kernel accepted the proof once more; any other status fails the module. The scope is for-all when the statement quantifies over data, unfolding when it does but the proof is reflexivity, and instance for specific values. christofides/tour-at-most-bound states 13 <= 15 for one tour, not the algorithm’s 3/2 guarantee (What “proved” means). The last column is axiom-free or each axiom the kernel found, by its alias followed by its content id.

The exit code is 0 when every namespace is OK and 1 otherwise, so the command works as a CI gate. A module that does not install prints FAIL, the namespace and the reason; Prove a lemma about rationals shows how to get the kernel’s own reason.

Name the axioms

Resolve the aliases you suspect in the default checkpoint. Save this as /tmp/axiom-ids.clj:

(require '[rainbow.checkpoint :as checkpoint]
         '[rainbow.environment :as environment]
         '[rainbow.main :as main])
(let [env (:environment (checkpoint/load-checkpoint main/default-checkpoint))]
  (doseq [alias '[logic/excluded-middle logic/proposition-extensionality]]
    (println alias (environment/resolve-id env alias))))
lein run -m clojure.main /tmp/axiom-ids.clj
logic/excluded-middle sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366
logic/proposition-extensionality sha256:b3f5d5a15f123b8edd7a1003cd1d1122dde6d8476e8b905d58034f999a1c3088

So set/infinite-union-equivalence uses excluded middle and set/finite-singleton-proposition-equality uses propositional extensionality. lein show prints an axiom’s statement:

lein show logic/excluded-middle
logic/excluded-middle :
  (x₁ : Prop)
  → proposition/disjunction x₁ (x₁ → proposition/falsity)
  -- binder names: generated

Two theorems in set_union.clj use classical axioms, and lein verify prints them. A logical principle enters Rainbow only as an explicit axiom declaration, so the kernel can always list it.

Next