Fast-cert-anomalies
Potentially surprising consequences of using fast-cert mode
See fast-cert for relevant background. This topic discusses
some surprises one may encounter when using fast-cert mode.
When fast-cert mode was developed in February 2023, a call of
“make” was made with “ACL2_FAST_CERT=t” and
target “regression-everything”, to certify the community-books with fast-cert mode active. There were only two
failures (out of thousands of books), both of which are discussed below along
with their fixes. There is no plan to continue to test certification of the
community books with fast-cert mode enabled, but we expect future failures to
continue to be rare.
Example 1
Community book system/tests/early-load-of-compiled/ttag.lisp has
certified regardless of whether or not fast-cert mode is used. However, when
it was certified with fast-cert mode active, a later attempt to include the
book failed. That failure was due to the way ACL2 handles raw-Lisp
redefinition (using a trust tag), as explained in a comment in the book. To
avoid this problem, the form (set-fast-cert nil state) is in file
ttag.acl2 in the same directory. Key events in the book are as follows,
in this order; the first forces a local-incompatibility check, and you
can see comments in ttag.lisp for why that is crucial.
(local (defun loc (x) x))
(defun ttag-f (x)
(declare (xargs :guard t))
x)
; An assertion is here of (equal (ttag-f 3) 3), to be evaluated during both
; certify-book and include-book, basically of the form:
(make-event ...) ; asserts (equal (ttag-f 3) 3)
(progn!
(set-raw-mode t)
(defun ttag-f (x) (cons x x)))
Example 2
The second example is rather subtle. Our starting point is the following,
from community book
rtl/rel9/support/lib2.delta1/add-new-proofs.lisp.
; Matt K. addition: The following lemma, natp-lamz, is not normally necessary.
; But with fast-cert mode active, we need it for the proof of lam1_alt-is-lam1.
; See :DOC fast-cert-anomalies if you want an explanation.
(local
(defthm natp-lamz
(natp (lamz a b e))
:rule-classes :type-prescription))
To see why this lemma is needed when certifying in fast-cert mode, let us
start by re-creating the environment where the definition of lamz has
been introduced. We assume here that the sub-books that are included were
certified with fast-cert mode active.
(set-fast-cert t state) ; so that sub-books are included as certified
(ld "rtl/rel9/support/lib2.delta1/add-new-proofs.lisp"
:dir :system
;; to speed things up:
:ld-skip-proofsp t)
We see that the built-in type-prescription rule for lamz says
only that lamz returns a rational number, not necessarily a non-negative
integer.
ACL2 !>:pr lamz
Rune: (:TYPE-PRESCRIPTION LAMZ)
Enabled: T
Hyps: T
Term: (LAMZ A B E)
Backchain-limit-lst: NIL
Basic-ts: *TS-RATIONAL*
Vars: NIL
Corollary: (RATIONALP (LAMZ A B E))
...
If we do the same experiment when sub-books were certified with fast-cert
mode disabled, the :pr output will instead show a built-in type-prescription rule for lamz saying that lamz returns a
non-negative integer. This discrepancy in that built-in rule explains why the
additional lemma above, natp-lamz, was necessary when certifying the
community-books with fast-cert mode active.
So now let us investigate why certifying books with fast-cert mode active
weakens the built-in type-prescription rule for lamz. After running the
set-fast-cert and ld commands displayed above, we see where
lamz is defined.
ACL2 !>:pe lamz
d 2 (LOCAL (INCLUDE-BOOK "../lib2/top"))
[Included books, outermost to innermost:
"/Users/kaufmann/acl2/acl2/books/rtl/rel9/support/lib2/top.lisp"
"/Users/kaufmann/acl2/acl2/books/rtl/rel9/support/lib2/add.lisp"
]
>L (DEFUN LAMZ (A B E)
(LNOT (LIOR A (LNOT B (1+ E)) (1+ E))
(1+ E)))
ACL2 !>
But we need to work harder to find the real source of the definition of
lamz. In rtl/rel9/support/lib2/add.lisp we see that the definition
of lamz is preceded by (set-enforce-redundancy t) as well as
(local (include-book "base")). When we invoke :ubt 1 and then
(include-book "base"), we can evaluate :pe lamz to see that
lamz is defined in rtl/rel9/support/lib1/add.lisp, which contains
(set-enforce-redundancy t) and the local event, (local (include-book
"../support/top")). So we include that book after invoking :ubt
1, then (again) invoke :pe lamz, and finally find the true source of
the definition of lamz: rtl/rel9/support/support/lextra.lisp.
So now consider what happens when we start ACL2 and evaluate the following
commands. For now, assume that we have used ACL2 fast-cert mode disabled to
certify all books being included. We use :ld-skip-proofsp 'include-book
to simulate what happens when including the book.
; with fast-cert mode disabled
(ld "rtl/rel9/support/support/lextra.lisp"
:dir :system
:ld-skip-proofsp 'include-book)
:ubt lamz
(defun lamz (a b e)
(lnot (lior a (lnot b (1+ e)) (1+ e)) (1+ e)))
Then :pr lamz shows a :type-prescription rule for lamz that
this function returns a non-negative integer. That is explained in part by
the following output, which mentions a rule stating that lnot returns a
non-negative integer, which was used to compute the built-in type for
lamz that it returns a non-negative integer.
We used the :type-prescription rule LNOT-NONNEGATIVE-INTEGER-TYPE.
Now repeat the same experiment but where we assume that fast-cert mode has
been active for all book certification and we start with (set-fast-cert t
state). This time there is no such output about
LNOT-NONNEGATIVE-INTEGER-TYPE. Aha! The culprit is the following form
near the top of "rtl/rel9/support/support/lextra.lisp".
(local (in-theory (current-theory 'lextra0-start)))
That form disables the :type-prescription rule
LNOT-NONNEGATIVE-INTEGER-TYPE, which is necessary for computing a
non-negative integer (i.e., natp) type for the built-in
:type-prescription rule for lamz. By contrast, without fast-cert
mode active, the world is rolled back past local events for the
local-incompatibility check, and then when events in the book are processed
during the include-book phase of certification, the rule
LNOT-NONNEGATIVE-INTEGER-TYPE is available for computing the built-in
type-prescription for lamz, which is stored in the book's certificate. But with fast-cert mode active, the world is not rolled back,
so the built-in type-prescription for lamz remains as originally computed,
where the rule LNOT-NONNEGATIVE-INTEGER-TYPE is disabled.
Indeed, if you read the certificate file for the lextra.lisp book
above, you'll see that the :TYPE-PRESCRIPTION entry for lamz
indicates a rational type when books are certified with fast-cert mode active
but a non-negative integer type when certified with fast-cert mode disabled.
You can read that certificate file as follows.
(read-file (concatenate 'string
(system-books-dir state)
"rtl/rel9/support/support/lextra.cert")
state)
