More details about invariant-risk

This topic, which may be unnecessary for most ACL2 users, expands on the documentation for invariant-risk. See that topic and see evaluation for relevant background.

We refer below to the following example, which is slightly expanded from the one in the documentation for invariant-risk.

(defstobj st (fld :type integer :initially 0)) (defun f1 (n st) (declare (xargs :stobjs st :guard (integerp n))) (update-fld n st)) (defun f2 (n st) (declare (xargs :stobjs st :guard (integerp n))) (f1 n st)) ; This :program-mode wrapper for f fails to require (integerp n): (defun g (n st) (declare (xargs :stobjs st :mode :program)) (f2 n st)) ; Trace f1 and f2 and their *1* functions. (This is optional.) (trace$ f1 f2 g) ; Produces an invariant-risk warning; only *1* functions are called. (g 3 st) ; Produces an invariant-risk warning and a guard violation: (g 'a st) ; Defeat invariant-risk checking (risky; uses a trust tag): (set-check-invariant-risk nil) ; No warning because *1* functions are not called. (g 3 st) ; No warning because *1* functions are not called. (g 'a st) ; Non-integer field value! (assert-event (equal (fld st) 'a))

To understand invariant-risk, consider the case that a stobj
updater (such as `program`-mode function to prevent it
from calling its corresponding submitted function. It does this when the

ACL2 !>(getpropc 'g 'invariant-risk) UPDATE-FLD ACL2 !>

When the function symbol

1> (ACL2_*1*_ACL2::G 3 |<st>|) ACL2 Warning [Invariant-risk] in G: Invariant-risk has been detected for a call of function G (as possibly leading to an ill-guarded call of UPDATE-FLD); see :DOC invariant-risk. 2> (ACL2_*1*_ACL2::F2 3 |<st>|) 3> (F2 3 |<st>|) 4> (F1 3 |<st>|) <4 (F1 |<st>|) <3 (F2 |<st>|) <2 (ACL2_*1*_ACL2::F2 |<st>|) <1 (ACL2_*1*_ACL2::G |<st>|) <st> ACL2 !>

This trace illustrates that even though

As an optimization, ACL2 avoids setting the `logic` mode functions whose guard is

(progn (defstobj st (reg :type (array (unsigned-byte 31) (8)) :initially 0)) (defun foo (i st) (declare (xargs :guard t :stobjs st)) (if (eql i 0) (update-regi i 3 st) st)) (defun bar (i st) (declare (xargs :stobjs st :mode :program)) (foo i st))) (bar 3 st)

This optimization can hold even if the function is originally submitted
without guard verification (typically, using xargs declaration

(progn (defstobj st (reg :type (array (unsigned-byte 31) (8)) :initially 0)) (defun foo (i st) (declare (xargs :guard t :stobjs st :VERIFY-GUARDS NIL)) (if (eql i 0) (update-regi i 3 st) st)) (defun bar (i st) (declare (xargs :stobjs st :mode :program)) (foo i st)) (verify-guards foo) ; avoid invariant-risk by moving before bar ) (bar 3 st) ; invariant-risk

Here is code that will return a list of all

:q ; go into raw Lisp (let (ans (wrld (w *the-live-state*))) (dolist (p (list-all-packages)) (do-symbols (sym p) (when (and (getpropc sym 'invariant-risk) (programp sym wrld) (not (getpropc sym 'predefined))) (push sym ans)))) ans)

To see exactly the executable-counterpart code generated for a