ACL2 8.7 / SBCL 2.6.8: a :linear rule with :trigger-terms and no linear conclusion is admitted, then faults the prover (memory fault at NIL)

acl2-linear-trigger-terms-crash.md

ACL2: a :linear rule with :trigger-terms and a conclusion that yields no polynomial is admitted, then crashes the prover (memory fault at NIL)

ACL2 8.7 (github tag 8.7), SBCL 2.6.8, x86-64 Linux, built with make LISP=sbcl; reproduced on two machines.

Reduced case

(in-package "ACL2")
(defstub f (x) t)
(defaxiom r1 (integerp (f x))
  :rule-classes ((:linear :trigger-terms ((f x)))))
(thm (< -1 (f a)))

R1 is admitted (the summary prints Rules: NIL). The thm then faults:

CORRUPTION WARNING in SBCL pid ...: Memory fault at (nil) (pc=0xb800290839 ...)
The integrity of this image is possibly compromised.
Note:  Unhandled memory fault at #x0.

The session cannot be trusted afterwards.

Observations

• Without :trigger-terms, the same rule is refused at admission (no linear conclusion), and nothing faults.
• With a conclusion that has an inequality, (natp (f x)) or (<= 0 (f x)), the rule is admitted and used correctly.
• So the :trigger-terms path appears to skip the check that the conclusion contributes at least one polynomial, and the linear-arithmetic pass later uses the empty result. Expected behaviour: refuse the rule at admission, as happens without :trigger-terms.
• Variants tried the same day: (natp (f x)) with a defstub, with and without skip-proofs: no fault. (integerp (g c)) over a defun, with or without a hypothesis, with or without a free variable: fault. The same rule without :trigger-terms: refused at admission, no fault.

How it was found

In practice, with a defthm whose conclusion was (and (<= (nfix (g r)) (h c)) (natp (h c))) stated as a :linear rule with :trigger-terms; the conjunct (natp (h c)) alone reproduces it through its integerp part. Worked around by stating the type fact as a :type-prescription and the inequality as a plain :linear rule.

The fault is SBCL's report of compiled ACL2 code following a NIL it does not check, so the defect seems to be in ACL2's admission of the rule rather than in SBCL.

Reproduce

Save the attached linear-crash.lisp and run

echo '(ld "linear-crash.lisp")' | acl2

TT-SURVIVED is printed only if the prover survives the thm; on both machines it never was.

linear-crash.lisp

; A :linear rule with :trigger-terms whose conclusion contributes no polynomial
; is admitted, then its first use in linear arithmetic faults SBCL.
; ACL2 8.7 on SBCL 2.6.8 (x86-64 Linux, built with make LISP=sbcl).
;
;   echo '(ld "linear-crash.lisp")' | acl2
;
; The rule is admitted with `Rules: NIL', then the thm faults:
;   CORRUPTION WARNING in SBCL ...: Memory fault at (nil) ...
;   Note:  Unhandled memory fault at #x0.
; TT-SURVIVED is never printed.  A conclusion with an inequality ((natp (f x))
; or (<= 0 (f x))) does not fault; the same rule without :trigger-terms is
; refused at admission and does not fault.
(in-package "ACL2")
(defstub f (x) t)
(defaxiom r1 (integerp (f x))
  :rule-classes ((:linear :trigger-terms ((f x)))))
(thm (< -1 (f a)))
(value-triple (cw "TT-SURVIVED~%"))