The guard on apply$-lambda
The guard on (apply$-lambda fn lst) is (apply$-lambda-guard
fn lst) which is extraordinarily weak.
(defun apply$-lambda-guard (fn args)
(declare (xargs :guard t))
(and (consp fn)
(consp (cdr fn))
(equal (len (cadr fn)) (length args))))
This guard is just strong enough to allow the definitions of the functions
in the apply$ clique to be guard verified. It does not guarantee that
fn is tame or well-formed or that args satisfy the guard of
fn. The last condition is in fact impossible to state given the untyped
nature of ACL2. Thus, (apply$ fn args) has to check tameness,
well-formedness, guard verified and that fn's guard is satisfied by
args when the apply$ is executed in the evaluation theory.
The issue of guards and guard verification of definitions involving
apply$ is further discussed in apply$ and in verify-guards.