Major Section: GUARD

See guard-evaluation-examples-script for a script that shows the interaction
of defun-modes with the value set by `set-guard-checking`

. Here, we
present a log resulting from running this script (using ACL2 Version 3.0,
built on Allegro Common Lisp).

See set-guard-checking for discussion of the interaction between defun-modes and guard-checking that is illustrated by this script. Also see guard-evaluation-table for a succinct table, with associated discussion, that covers in detail the interactions illustrated here.

ACL2 !>(defun fact (x) (declare (xargs :guard (integerp x) :mode :program)) (if (posp x) (* x (fact (1- x))) 1))Summary Form: ( DEFUN FACT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 !>(trace$ fact) NIL ACL2 !>:set-guard-checking t

Guard-checking-on already has value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 Error in TOP-LEVEL: The guard for the :program function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC wet for how you might be able to get an error backtrace. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 Error in TOP-LEVEL: The guard for the :program function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC wet for how you might be able to get an error backtrace. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard- checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u

0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard t :mode :program)) (if (posp x) (* x (fact (1- x))) 1))

Summary Form: ( DEFUN FACT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none

Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard- checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u

0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard (integerp x) :verify-guards nil :mode :logic)) (if (posp x) (* x (fact (1- x))) 1))

For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is

Goal (IMPLIES (POSP X) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

By the simple :definition POSP we reduce the conjecture to

Goal' (IMPLIES (AND (INTEGERP X) (< 0 X)) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

But we reduce the conjecture to T, by case analysis.

Q.E.D.

That completes the proof of the measure theorem for FACT. Thus, we admit this function under the principle of definition. We observe that the type of FACT is described by the theorem (AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

Summary Form: ( DEFUN FACT ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION POSP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2)

ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of FACT. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn)

<1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC wet for how you might be able to get an error backtrace. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC wet for how you might be able to get an error backtrace. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :none

Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

Masking guard violations but still checking guards. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard- checking.

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FACT. FACT is compliant with Common Lisp.

Summary Form: ( VERIFY-GUARDS FACT) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 Error in TOP-LEVEL: The guard for the function symbol FACT, which is (INTEGERP X), is violated by the arguments in the call (FACT T). See :DOC wet for how you might be able to get an error backtrace. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T)

ACL2 !>:set-guard-checking :none

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u L 1:x(DEFUN FACT (X) ...) ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard (integerp x) :mode :logic)) (if (posp x) (* x (fact (1- x))) 1))

For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is

Goal (IMPLIES (POSP X) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

By the simple :definition POSP we reduce the conjecture to

Goal' (IMPLIES (AND (INTEGERP X) (< 0 X)) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

But we reduce the conjecture to T, by case analysis.

Q.E.D.

That completes the proof of the measure theorem for FACT. Thus, we admit this function under the principle of definition. We observe that the type of FACT is described by the theorem (AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rule POSP-COMPOUND-RECOGNIZER, primitive type reasoning and the :type-prescription rule FACT. FACT is compliant with Common Lisp.

Summary Form: ( DEFUN FACT ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION POSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>:set-guard-checking :none

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 >(defun fact (x) (declare (xargs :guard t :verify-guards nil :mode :logic)) (if (posp x) (* x (fact (1- x))) 1))

For the admission of FACT we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is

Goal (IMPLIES (POSP X) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

By the simple :definition POSP we reduce the conjecture to

Goal' (IMPLIES (AND (INTEGERP X) (< 0 X)) (O< (ACL2-COUNT (+ -1 X)) (ACL2-COUNT X))).

But we reduce the conjecture to T, by case analysis.

Q.E.D.

That completes the proof of the measure theorem for FACT. Thus, we admit this function under the principle of definition. We observe that the type of FACT is described by the theorem (AND (INTEGERP (FACT X)) (< 0 (FACT X))). We used the :compound-recognizer rule POSP-COMPOUND-RECOGNIZER and primitive type reasoning.

Summary Form: ( DEFUN FACT ...) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:DEFINITION NOT) (:DEFINITION POSP) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (ACL2_*1*_ACL2::FACT 1) 3> (ACL2_*1*_ACL2::FACT 0) <3 (ACL2_*1*_ACL2::FACT 1) <2 (ACL2_*1*_ACL2::FACT 1) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >(verify-guards fact)

Computing the guard conjecture for FACT....

The guard conjecture for FACT is trivial to prove, given the :compound- recognizer rule POSP-COMPOUND-RECOGNIZER and the :type-prescription rule FACT. FACT is compliant with Common Lisp.

Summary Form: ( VERIFY-GUARDS FACT) Rules: ((:COMPOUND-RECOGNIZER POSP-COMPOUND-RECOGNIZER) (:TYPE-PRESCRIPTION FACT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FACT ACL2 >(trace$ fact) NIL ACL2 >:set-guard-checking t

Turning guard checking on, value T.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :all

Leaving guard checking on, but changing value to :ALL.

ACL2 !>(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 !>(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 !>:set-guard-checking :none

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >:set-guard-checking nil

ACL2 >(fact 2) 1> (ACL2_*1*_ACL2::FACT 2) 2> (FACT 2) 3> (FACT 1) 4> (FACT 0) <4 (FACT 1) <3 (FACT 1) <2 (FACT 2) <1 (ACL2_*1*_ACL2::FACT 2) 2 ACL2 >(fact t) 1> (ACL2_*1*_ACL2::FACT T) 2> (FACT T) <2 (FACT 1) <1 (ACL2_*1*_ACL2::FACT 1) 1 ACL2 >