Program-only
Functions that cannot be in logic mode
Functions are considered to be ``program-only'' when they are in
program mode and they belong to the list (@
program-fns-with-raw-code). For such a function, its
executable-counterpart (see evaluation) always checks the guard. If
the guard fails, then even if guard-checking is off, an error is signaled
because a program-only function is assumed to have an executable-counterpart
that should only execute the raw Lisp definition. Moreover, an error is
always signaled when in safe-mode (e.g., during macroexpansion),
because there is no guarantee that evaluation of the raw Lisp code will be
``safe''.
The constant *initial-program-fns-with-raw-code* provides the initial
value of (@ program-fns-with-raw-code). The value of that constant is
the list of ACL2 source functions that have special raw-Lisp code. It is
important that these program-mode functions not be converted to logic mode. Otherwise, one could arrange to prove a contradiction. To see
how, consider the following example, which takes advantage of an unsound use
of :q to prove that a call of a program-only function, p-o,
returns two different values on the same input (an obvious contradiction).
(defun p-o (x)
(declare (xargs :guard t))
(er hard? 'p-o
"Attempted logical evaluation of ~x0."
(list 'p-0 x)))
:q ; exit the ACL2 read-eval-print loop
(defun p-o (x)
(declare (xargs :guard t))
(atom x))
(lp) ; re-enter the ACL2 read-eval-print loop
(defthm p-0-nil-is-nil
(equal (p-o nil) nil)
:hints (("Goal" :in-theory (disable (:e p-o)))))
(defthm p-o-nil-is-t
(equal (p-o nil) t))
In the ACL2 source one often finds a definition marked with readtime
conditionals, such as the following.
(defun p-o (x)
(declare (xargs :guard t))
#-acl2-loop-only
(atom x)
#+acl2-loop-only
(er hard? 'p-o
"Attempted logical evaluation of ~x0."
(list 'p-0 x)))
The acl2-loop-only annotations arrange that when ACL2 is built, one
gets the effect described above, where the #+acl2-loop-only code is used
in the definition known to ACL2 and the #-acl2-loop-only code is used in
the definition known to raw Lisp. All function symbols with such definitions
are in the list mentioned above, that is, the value of the constant
*initial-program-fns-with-raw-code*.
In summary: The contradiction proved above explains the restriction that
logic-mode functions may not call program-mode functions.
See safe-mode-cheat-sheet for possible workarounds, which however
may compromise soundness.
