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
“

Community book

(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)))

The second example is rather subtle. Our starting point is the following,
from community book

; 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

(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

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

So now let us investigate why certifying books with fast-cert mode active
weakens the built-in type-prescription rule for `ld` commands displayed above, we see where

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
*that* book after invoking

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

; 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

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

(local (in-theory (current-theory 'lextra0-start)))

That form disables the

Indeed, if you read the certificate file for the

(read-file (concatenate 'string (system-books-dir state) "rtl/rel9/support/support/lextra.cert") state)