ACL2 Version 3.4 Patch

You may download file flet-patch.lisp in order to fix some problems with FLET in ACL2 Version 3.4 (actually also in Version 3.3, where ACL2 support for FLET was introduced). Installation instructions are at the top of the file.

Below is the documentation that may appear in the next release notes to explain this patch.


Fixed bugs in the handling of flet expressions, one of which had the capability of rendering ACL2 unsound. Thanks to Sol Swords for pointing out two issues and sending examples. One example illustrated how ACL2 was in essence throwing away outer flet bindings when processing an inner flet. We have exploited that example to prove a contradiction, as follows: this book was certifiable before this fix.

(in-package "ACL2")

(defun a (x)
  (list 'c x))

; Example from Sol Swords, which failed to be admitted (claiming that
; function A is undefined) without the above definition of A.
(defun foo1 (x y)
   (flet ((a (x) (list 'a x)))
     (flet ((b (y) (list 'b y)))
       (b (a (list x y))))))

(defthm not-true
  (equal (foo1 3 4)
         '(b (c (3 4))))
  :hints (("Goal"
           :in-theory
           (disable (:executable-counterpart foo1))))
  :rule-classes nil)

(defthm contradiction
  nil
  :hints (("Goal" :use not-true))
  :rule-classes nil)
Sol's second example, below, pointed to a second bug related to computing output signatures in the presence of nested flet expressions, which we have also fixed: this form failed before the fix.
:trans (flet ((foo (a) (list (flet ((bar (b) b)) a)))) x)