Mixed-mode-functions
:logic mode functions can apply$ :program mode functions
Because :program mode functions can be given badges it
is possible to apply$ them from within :logic mode
functions. Colloquially, we call such :logic mode functions ``mixed
mode,'' but that is a misnomer. They are indisputably in :logic
mode.
First, note that the only way to introduce a :program mode function
into :logic mode functions is to use the quoted :program mode
function name in an argument slot of ilk :FN, use the
:program mode function in a quoted lambda object or lambda$ expression in a slot of ilk :FN or use it in a quoted
expression in a slot of ilk :EXPR. We do not allow :program mode
functions to be called directly from :logic mode functions. For
example, if prgm is defined as a :program mode function of one
argument, and has been assigned a badge by defbadge
(defun foo (x)
(declare (xargs :mode :logic))
(apply$ 'prgm (list x)))
is legal but
(defun foo (x)
(declare (xargs :mode :logic))
(prgm x))
is not.
Second, the presence of a :program mode function in a :logic
mode function prohibits the :logic mode function from being guard
verified.
Mixed-mode functions raise interesting questions for top-level evaluation
and evaluation and rewriting during proofs.
When a :program mode function is apply$ed, it is always done in
safe-mode. In general, evaluating a :program mode function at
the top-level can cause hard Lisp errors. For example,
(defun prgm (x) (declare (xargs :mode :program)) (car x))
Then (prgm 23) causes a hard Lisp error in both CCL and SBCL, but
(prgm 'abc) returns numbers in both of those Common Lisps, but they
return different numbers. Furthermore, there is no guarantee across all
Common Lisps that (prgm 'abc) will always return the same number
throughout a given ACL2 session; the value could conceivably change as memory
is allocated, compacted, garbage collected, etc., since according to the CLTL
standard, one is not supposed to apply CAR to any symbol other than
NIL but no error need be signaled. It is likely that a CLTL
implementation of CAR just accesses memory where the CAR component
of a cons is supposed to be!
We tolerate such behavior when :program mode functions are directly
called at the top-level because there are no axioms about them and we regard
the evaluation of such programs from within the ACL2 loop as just a
convenience to the user.
But apply$ is a :logic mode function and we must guarantee that
when any :logic mode function is evaluated functional substitutivity
holds: identical calls must yield identical results. That is, apply$
must behave like a function and not give different answers to the same
questions over time when errors are not signaled. We also strive to achieve
the goal that :logic mode functions never cause hard Lisp errors other
than resource errors like stack overflow or memory exhaustion. So when
apply$ is given a badged :program mode function, e.g., had we
badged prgm and then evaluated (apply$ 'prgm '(abc)), it must at
least return the same ACL2 object every time! To achieve this end
apply$ runs :program mode functions in safe-mode.
(Safe mode does shift into raw Lisp on calls of guard verified :logic
mode functions which might be called from within the :program mode
function. But a mixed mode function cannot be guard verified because the
:program mode functions used within it cannot be guard verified.)
This means that a top-level call of a mixed mode function generally runs
slower than a corresponding call of an otherwise identical :program mode
function. (And, on the positive side, it means that mixed mode functions
actually behave like functions while :program mode ones may not!)
The only way to speed up a mixed-mode function is to convert the
:program mode functions in it to :logic mode with verify-termination and verify the guards.
As for proofs, since there are no axioms about :program mode
functions, if a mixed-mode function is expanded in a proof all :program
mode functions in it are treated as though they are undefined. In
particular, the absence of a warrant on the :program mode function
prgm means that (apply$ 'prgm '(abc)), is not evaluated by the
prover despite the fact that it is a ground term.
