latte.certify — latte 1.0b4-SNAPSHOT

Certification of LaTTe namespaces. The functions in this namespace allow to take a snapshot of the current running state of a namespace, and issue a certificate of all the theorems demonstrated (using a cryptographic signature scheme). This is a form of compilation for demonstrated theorems.

*verbose-certification* clj

+global-proof-certificate+ clj

certified-theorems clj

(certified-theorems thms)

Build a map of theorem certifications from a map `thms' of theorems. Each theorem contents (definition ) is signed with

certify-library! clj

(certify-library! library-name namespaces)

certify-namespace! clj

(certify-namespace! namesp)

clear-certification! clj

(clear-certification!)

demonstrated-theorems clj

(demonstrated-theorems)

(demonstrated-theorems namesp)

Fetch a map of theorems with an actual proof in the namespace named `namesp' (a symbol). If not indicated the current namespace is used.

load-namespace-certificate! clj

(load-namespace-certificate! namesp-name)

Load the namespace named namesp-name certificate, if any.

mk-timestamp-file! clj

(mk-timestamp-file! library-name)

proof-certified? clj

(proof-certified? namesp thm-name thm-params thm-type thm-proof)

Check if the provided proof is certified.

theorem-signature clj

(theorem-signature params type proof)

Sign the specified theorem contents.