		Search-engine friendly clone of the ACL2 documentation.

Invariant-risk

Invariant-risk-details

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 update-fld above) is called on ill-guarded arguments. In that case the resulting ACL2 state could be ill-formed, as in the example above: after turning off invariant-risk checking, the stobj st is defined to have an integer field yet winds up with a symbol in that field. ACL2 arranges invariant-risk checking by installing special code in the executable-counterpart of a :program-mode function to prevent it from calling its corresponding submitted function. It does this when the :program-mode function has a non-nil 'invariant-risk property; in the example above, note:

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

When the function symbol g was defined, it inherited this property from f2, which in turn inherited it from f1, which in turn inherited it from the stobj updater, update-fld. However, the aforementioned special code is only installed for :program mode functions, hence not for f1 or f2. Consider for example the following trace, from the call of (g 3) made above before turning off invariant-risk checking.

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 f2 has the 'invariant-risk property, its executable-counterpart has permission to call its submitted function because f2 is a guard-verified :logic-mode function.

As an optimization, ACL2 avoids setting the 'invariant-risk property on :logic mode functions whose guard is t or, more generally, a conjunction of stobj recognizer calls. For example, the call of (bar 3 st) below does not cause an invariant-risk warning.

(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 :verify-guards nil), but only if its guards are verified before defining the :program-mode wrapper (e.g., bar above). Thus we see an invariant-risk warning in the call of bar below.

(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 :program-mode functions subject to invariant-risk checking that are user-defined (not built into ACL2).

: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 :program-mode function with invariant-risk, evaluate (trace! (oneify-cltl-code :native t)) before submitting its definition.