Fast-cert
A mode for faster, but possibly unsound, book certification
See certify-book and include-book for background on
certifying and including books.
By default, certify-book includes a “Step 3” that does
a local-incompatibility check. That check can be expensive for some
“industrial-size” books if there are local events early in
the book or in its portcullis commands. Fast-cert mode provides a way
to avoid the local-incompatibility check. There are the following two
drawbacks to using ACL2 with fast-cert mode enabled (as described further
below).
- It may be unsound! See Section “Unsoundness” below.
- Therefore, after a book is certified with fast-cert mode enabled, then any
subsequent attempt to include that book will consider it to be uncertified
unless the include-book event is executed with fast-cert mode enabled.
See Section “Effects of fast-cert mode...” below.
Example Forms:
(set-fast-cert t state) ; enter fast-cert active mode
(set-fast-cert nil state) ; disable fast-cert mode
(set-fast-cert :accept state) ; enter fast-cert accept mode
General Form:
(set-fast-cert expr state)
where if expr evaluates to val, then: if val is t then
fast-cert mode becomes (or remains) active; if val is nil, then
fast-cert mode becomes (or remains) disabled; and otherwise val must be
:accept. In the last case, ACL2 behaves as though fast-cert mode is
disabled — we also say ``not enabled'' for ``disabled'' — but
books can be considered certified even if they were certified with fast-cert
mode enabled. We say more about these three modes in Section “Fast-cert
modes” below.
Another way to enter fast-cert mode is to set environment variable
ACL2_FAST_CERT to a non-empty value before starting ACL2. The
case-insensitive value, "accept", causes (set-fast-cert :accept
state) to be evaluated at startup; otherwise, a non-empty value causes
(set-fast-cert t state) to be evaluated at startup.
We turn now to sections that include those promised above.
Fast-cert modes
There are the following fast-cert modes.
- Active: entered with (set-fast-cert t state). When ACL2 is in
this mode, the local-incompatibility check is skipped when certifying a
book, and the book's certificate marks it as a “fast-cert
book”.
- Disabled: entered with (set-fast-cert nil state), though this
is the default mode. In this mode the usual local-incompatibility
checks are performed during book certification, and every fast-cert book (as
defined just above) is considered to be uncertified.
- Accept: entered with (set-fast-cert :accept state). When ACL2
is in this mode, local-incompatibility checks are performed just as
when fast-cert mode is disabled, but a fast-cert book is treated as certified
just like any other book.
Fast-cert mode is considered to be “enabled” exactly when it is
not disabled, that is, when fast-cert mode is active or accept.
The discussion above leaves open the question of whether a book that is
certified in accept mode is marked as a fast-cert book. That happens only if
at least one fast-cert book has been included during the session, either
before the book's certification began or during evaluation of the book's
events.
It is always legal to change fast-cert mode from disabled to enabled (using
set-fast-cert). It is legal to change fast-cert mode from enabled to
disabled provided there has been no attempt during the session to include a
fast-cert book while fast-cert mode is enabled.
Potential for unsoundness
Consider the proof of nil constructed by the following two books.
;;; fast-cert-unsound-sub.lisp
(in-package "ACL2")
(local (defun f () t))
(defun g () (f))
(defthm g-is-t
(equal (g) t))
;;; fast-cert-unsound.lisp
(in-package "ACL2")
(defun f () nil)
(include-book "fast-cert-unsound-sub")
(thm nil
:hints (("Goal" :use g-is-t)))
Now execute the following commands to prove nil!
(set-fast-cert t state)
(certify-book "fast-cert-unsound-sub")
:u
(certify-book "fast-cert-unsound")
To see what went wrong, consider what happens if we try this without first
evaluating (set-fast-cert t state). In that case, we can see that an
attempt to certify "fast-cert-unsound-sub" fails the local-incompatibility check.
* Step 3: That completes the admissibility check. Each form read
was an embedded event form and was admissible. We now retract back
to the initial world and try to include the book; see :DOC
local-incompatibility.
ACL2 Error [Translate] in ( DEFUN G ...): The symbol F (in package
"ACL2") has neither a function nor macro definition in ACL2. Please
define it. See :DOC near-misses. Note: this error occurred in the
context (F).
That is, the attempt in Step 3 to include
"fast-cert-unsound-sub.lisp" fails the local-incompatibility check
because the definition of f is local, hence skipped, so the
definition of g is illegal. Without the use of fast-cert mode, the
local-incompatibility check would catch this problem.
(Technical note: if the book is certified while fast-cert mode is active,
then when we subsequently include "fast-cert-unsound-sub" when
fast-cert mode is enabled, there is — perhaps surprisingly — no
error. That is because the translation (see term) of the definition of
g is cached in the book's certificate.)
Note that unsoundness can occur even when fast-cert is in accept mode, not
just in active mode. That's because one may include a book in accept mode
that was certified in a previous session while fast-cert was in active mode,
and that book could prove nil as in the example above. In short,
unsoundness can occur when fast-cert mode is enabled (i.e., fast-cert is in
accept or active mode).
Unsoundness when fast-cert mode is enabled is probably rare in practice.
But because unsoundness is possible with fast-cert mode enabled, a
“TTAG NOTE” message is printed when fast-cert mode is
enabled, for example as follows when fast-cert mode transitions from disabled
to active.
ACL2 !>(set-fast-cert t state)
TTAG NOTE: Fast-cert mode is active (see :DOC fast-cert).
T
ACL2 !>
The message above may seem a bit misleading, since there is no actual trust
tag (ttag) involved. The “TTAG NOTE” message is simply
ACL2's way of conveying that there is a trust issue — typically with the
use of defttag but also when entering fast-cert mode.
We conclude this section by mentioning other potential sources of
unsoundness when fast-cert mode is enabled. There are probably yet others,
but again, it is probably rare for fast-cert mode to exhibit unsoundness.
These behaviors are due to avoiding the local-incompatibility check
during certification when fast-cert mode is active.
- Hidden defpkg events are not recorded in a book's certificate when fast-cert mode is active. See hidden-death-package.
- Information about sub-books that is normally recorded in a certificate, including the book-hash values in the portcullis
and the keep, is omitted by certification when fast-cert mode is
active. This prevents ACL2 from noticing when sub-books are uncertified or
have changed since the time of the parent book's certification.
Here are some necessary checks that may be omitted when the
local-incompatibility check is skipped.
- A non-local congruence rule needs its alleged equivalence relation
to be an equivalence relation non-locally. Generally this means that the
supporting defequiv event must be non-local.
- A non-local rule of class :meta or :clause-processor needs its evaluators to be evaluators non-locally.
- A defattach event imposes requirements on function symbols to be
guard-verified. So if a defattach event is non-local, each
necessary guard verification status must hold non-locally.
Because of potential unsoundness when fast-cert mode is enabled, especially
as explained in the item above regarding status of books that are included in
a parent book, it is strongly recommended that you eventually certify your
collection of books with fast-cert mode disabled. Otherwise there is no sort
of guarantee that your proofs are valid!
Interactions involving fast-cert mode
- When a book is successfully certified with fast-cert mode active, its
certificate records this fact. Let's call such a certificate (or book)
a “fast-cert certificate” (or “fast-cert book”);
otherwise it is a “normal“ certificate (or “normal
book”).
- When a book is successfully certified with fast-cert in accept mode, the
book is a normal book only if no fast-cert book is included before or during
certification.
- When include-book is performed on a book with a valid fast-cert
certificate, that book is considered to be certified if fast-cert mode is
enabled and otherwise is considered to be uncertified.
- When include-book is performed on a book with a valid normal
certificate, that book is considered to be certified regardless of whether or
not fast-cert mode is enabled at include-book time.
- When provisional-certification is used during certify-book
while fast-cert mode is active, then fast-cert is treated as being in accept
mode; in particular, the local-incompatibility check) is performed in the
normal way.
- Normally certify-book warns about functions that have not had their
guards verified. This message is suppressed when fast-cert mode is
active, because local include-book forms in the certification world can
make that message very long.
- When a fast-cert book is included while fast-cert mode is enabled, then
the rest of that ACL2 session must have fast-cert mode enabled. This
restriction guarantees that any book then certified during that session will
be given a fast-mode certificate.
- It is illegal to call set-fast-cert during make-event expansion
(see make-event). There is also an explicit check to prohibit calls of
set-fast-cert during certify-book, though that is probably
unnecessary because of the make-event restriction unless that restriction
is subverted using a trust tag.
See fast-cert-anomalies for some possibly surprising (and more
obscure) consequences of using fast-cert mode.
Fast-cert mode and save-exec
The motivation for adding fast-cert mode was to provide faster
certification based on executables created with save-exec. We
illustrate with an example, which starts by locally including a book
that brings in many definitions and rules (it may take about a minute to
include) and then saving an executable. The initial (non-local)
include-book forms below might not be necessary for all uses of the
executable.
(include-book "centaur/sv/portcullis" :dir :system)
(include-book "std/util/define" :dir :system)
(local (include-book "centaur/sv/top" :dir :system))
:q
(save-exec "sv-top" "Locally includes centaur/sv/top")
Now suppose we want to create a book that is based on a tiny part of what
is provided by the book included above, as follows (comments omitted
here).
(in-package "SV")
(define name-p (x)
:parents (name)
(or (stringp x)
(integerp x)
(eq x :self)
(and (consp x)
(eq (car x) :anonymous))))
(define name-fix ((x name-p))
:parents (name)
:returns (xx name-p)
:hooks nil
(mbe :logic (if (name-p x) x '(:anonymous))
:exec x)
///
(defthm name-fix-when-name-p
(implies (name-p x)
(equal (name-fix x) x))))
We now invoke the resulting executable, ./sv-top.
; Start ./sv-top, then:
(set-fast-cert t state)
(certify-book "name" ? t :ttags :all)
In this little example, the certification time has been cut in half with
fast-cert mode active. In many cases the reduction may be less than that, but
in large industrial examples the reduction might be much, much greater —
-- especially when the book contains time-consuming events, in particular
include-book events.
Subtopics
- Fast-cert-anomalies
- Potentially surprising consequences of using fast-cert mode
