Defun-mode-caveat
Potential soundness issue for functions with defun-mode
:program
See raw-lisp-error for a general discussion of raw Lisp
errors. Although the discussion below focuses on raw Lisp errors that arise
from calls of :program mode functions, the soundness concerns
expressed below apply to all raw Lisp errors.
Technically speaking, in the current implementation, the execution of
functions having defun-mode :program may damage the ACL2
system in a way that renders it unsound. In practice, we have never seen this
happen; so, the explanations below can be viewed as extremely paranoid.
Nevertheless, here we document this concern, even if it should be taken with
more than a grain of salt.
See defun-mode for a discussion of defun-modes. That
discussion describes an imagined implementation that is slightly different
from this one. This note explains that the current implementation is open to
unsoundness.
For discussion of a different soundness issue that is also related to
function execution, see generalized-booleans.
The execution of a function having defun-mode :program
may violate Common Lisp guards on the subroutines used. (This may be
true even for calls of a function on arguments that satisfy its guard,
because ACL2 has not verified that its guard is sufficient to protect
its subroutines.) When a guard is violated at runtime all bets are
off. That is, no guarantees are made either about the answer being ``right''
or about the continued rationality of the ACL2 system itself.
For example, suppose you make the following defun:
(defun crash (i)
(declare (xargs :mode :program :guard (integerp i)))
(car i))
Note that the declared guard does not in fact adequately protect the
subroutines in the body of crash; indeed, satisfying the guard to
crash will guarantee that the car expression is in violation of
its guard. Because this function is admitted in :program-mode,
no checks are made concerning the suitability of the guard. Furthermore, in
the current ACL2 implementation, crash is executed directly in Common
Lisp. Thus if you call crash on an argument satisfying its guard you
will cause an erroneous computation to take place.
ACL2 !>(crash 7)
Error: Caught fatal error [memory may be damaged]
...
There is no telling how much damage is done by this errant computation. In
some lisps your ACL2 job may actually crash back to the operating system. In
other lisps you may be able to recover from the ``hard error'' and resume ACL2
in a damaged but apparently functional image.
THUS, HAVING A FUNCTION WITH defun-mode :program IN
YOUR SYSTEM ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE
SOUNDNESS OF OUR SYSTEM.
Furthermore
ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF SOUNDNESS
AFTER THE INTRODUCTION OF A FUNCTION IN :program MODE, EVEN IF IT
IS ULTIMATELY CONVERTED TO :logic MODE (since its execution could
have damaged the system in a way that makes it possible to verify its
termination and guards unsoundly).
Finally,
THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN :program MODE AND
SO ALL BETS ARE OFF FROM BEFORE YOU START!
This hopeless state of current affairs will change, we think. We think we
have defined our functions ``correctly'' in the sense that they can be
converted, without ``essential'' modification, to :logic mode.
We think it very unlikely that a mis-guarded function in :program
mode (whether ours or yours) will cause unsoundness without some sort of hard
lisp error accompanying it. We think that ultimately we can make it possible
to execute your functions (interpretively) without risk to the system, even
when some have :program mode. In that imagined implementation,
code using functions having :program mode would run more slowly,
but safely. These functions could be introduced into the logic ex post facto,
whereupon the code's execution would speed up because Common Lisp would be
allowed to execute it directly. We therefore ask that you simply pretend that
this is that imagined implementation, introduce functions in :program mode, use them as convenient and perhaps ultimately introduce some of
them in :logic mode and prove their properties. If you use the
system this way we can develop (or dismiss) this style of formal system
development. BUT BE ON THE LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE
EXECUTION OF YOUR FUNCTIONS HAVING :program MODE!
