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

Guides

Share and check a bundle

A proof bundle carries declarations proved on a public base, with their proof terms, so anyone can check them with the kernel alone. You need test/scratch/nnrat_add_left.clj from Prove a lemma about rationals. Run the commands from the root of a v1.4.1 clone.

Make the bundle

The open core has no command that writes a bundle. Build one with rainbow.main/proof-bundle and write-bundle!. Save this as /tmp/make-bundle.clj:

(require '[rainbow.main :as main]
         '[rainbow.checkpoint :as checkpoint]
         'scratch.nnrat-add-left)

(def modules '[rainbow.math.rational.nnrat.add-monotone
               rainbow.math.rational.nnrat.add-upper])

(let [loaded (checkpoint/load-checkpoint main/default-checkpoint)
      base (reduce (fn [env m] (require m) ((ns-resolve m 'extend-environment) env))
                   (:environment loaded) modules)
      env (scratch.nnrat-add-left/extend-environment base)]
  (main/write-bundle! "/tmp/add-left.edn"
                      (main/proof-bundle {:checkpoint main/default-checkpoint
                                          :modules modules
                                          :base-env base
                                          :env env
                                          :claims ['nnrat/at-most-add-left]
                                          :meta {:author "you"}}))
  (println "wrote /tmp/add-left.edn"))

proof-bundle exports what env adds to base: the default checkpoint plus the two public modules your lemma uses.

lein run -m clojure.main /tmp/make-bundle.clj
wrote /tmp/add-left.edn
{:rainbow.bundle/schema-version 1, :base {:checkpoint "artifacts/ahof/d63-eligibility-traces/checkpoint.edn.gz", :modules ["rainbow.math.rational.nnrat.add-monotone" "rainbow.math.rational.nnrat.add-upper"], :environment-id "sha256:fe929452bece1e5fb953ef9418be86e9816a3c4c8af2df579c9ebdac235e51e2"}, :claims {nnrat/at-most-add-left {:id "sha256:f3562fdc875b031e583f530df37253d980509187b4b869dbbcdb7c3b446b6c60", :axioms #{}}}, :check {:reductions 1000000}, :meta {:author "you"}, :declarations [...]}

:base pins the checkpoint, its modules and the environment id they must produce. :claims gives each alias its content id and axioms. :check is the kernel’s reduction budget. :declarations holds the proof terms as trees.

Convert it

lein share-bundle writes the shared encoding, with each distinct subterm and constant once. --binary writes the binary one.

lein share-bundle /tmp/add-left.edn /tmp/add-left.shared.edn
lein share-bundle --binary /tmp/add-left.edn /tmp/add-left.bin
/tmp/add-left.edn (2 796 bytes) -> /tmp/add-left.shared.edn (1 901 bytes)
/tmp/add-left.edn (2 796 bytes) -> /tmp/add-left.bin (1 267 bytes)

About 2 seconds each. Numbers follow the JVM’s locale. Large proof terms repeat themselves and shrink far more: see Proof bundles.

Check it

lein verify --bundle /tmp/add-left.edn /tmp/add-left.shared.edn /tmp/add-left.bin
OK    /tmp/add-left.edn  (22,7 s)
       checked   nnrat/at-most-add-left  axiom-free
OK    /tmp/add-left.shared.edn  (0,4 s)
       checked   nnrat/at-most-add-left  axiom-free
OK    /tmp/add-left.bin  (0,4 s)
       checked   nnrat/at-most-add-left  axiom-free

For each file the command replays the base checkpoint, installs the base modules, compares the environment id, adds each declaration through kernel/add-declaration, and checks each claim’s id, proof and axioms against the record. Only the first file pays for the replay, because the run keeps the checkpoint in memory.

Check it without your module

The receiver needs the public repository and the bundle, not your module. To try it, move test/scratch/nnrat_add_left.clj out of the repository. Make /tmp/add-left-tampered.edn by changing one [:bound 0] to [:bound 1] in the theorem’s :rainbow/type: the statement becomes a ≤ a + b, true, but not what the proof term proves.

lein verify --bundle /tmp/add-left.edn /tmp/add-left-tampered.edn
OK    /tmp/add-left.edn  (18,5 s)
       checked   nnrat/at-most-add-left  axiom-free
FAIL  /tmp/add-left-tampered.edn -- kernel rejected bundle entry sha256:f3562fdc875b031e583f530df37253d980509187b4b869dbbcdb7c3b446b6c60 (:kernel/type-mismatch) (0,3 s)

The exit code is 1, with the kernel’s own reason. Each file you name is checked and reported, even after a failure.

Next