Matt Kaufmann Cons-with-hint: An ACL2 development case study ACL2 seminar, 3/8/2016 ABSTRACT: See file abstract.txt . These notes are on the ACL2 seminar website. OUTLINE, obtained by using: grep '\([+][+]\|--\)' talk.txt ++ 1. Introduction ----- a. Industrial demands for faster ACL2 execution ----- b. Cons-with-hint -- Offered by Jared Davis and Sol Swords, Centaur -- Requested incorporation into ACL2 source code ++ 2. Cons-with-hint ----- a. Logically, really cons (:pe cons-with-hint, or :pf) ----- b. Implementation (see source file axioms.lisp) -- avoids building a cons and garbage collection ----- c. Example use: remove1-equal (see :doc remove1) ----- d. Why not hons? ----- e. Why not a "changedp" approach? ++ 3. Getting the prover to treat cons-with-hint as cons ----- a. Motivation: Use cons-with-hint in ACL2 sources -- but preserve proofs (regression and user) ----- b. The problem via an example (admittedly contrived) ----- c. General remarks about solutions described below ++ 4. Solutions with MBE ("Must Be Equal") ----- a. Introduction to MBE -------- i. A simple example -------- ii. Evaluation of MBE calls -------- iii. Reasoning with MBE calls ----- b. A simple solution with MBE ----- c. A better solution with MBE: sharing ----- d. Improving *1* code for functions that call MBE ----- e. Summary statistics for a real example ++ 5. Back to the start? ----- a. Issue: functions that are not guard-verified ----- b. Using the original definition ----- c. Prover trick #1: remove-guard-holders ----- d. Prover trick #2: expandable boot-strap functions ++ 6. Summary ----- a. Cons-with-hint is incorporated into ACL2 -- essentially unchanged from Jared and Sol ----- b. Might proofs fail when using cons-with-hint? -- Thought about this when modifying ACL2 built-ins ----- c. Tried MBE -- I didn't use sharing when I should have. -- (Note that MEMBER etc. use LET-MBE.) -- This exposed *1* code generation issue for MBE -- Fixed using FLET -- Use of sharing fixed the problem -- But how about non-guard-verified functions? ----- d. Reverted to cons-with-hint as a function (no MBE). -- Used prover tricks to avoid proof failures ----- e. Outcomes -- Fast cons-with-hint that preserves proofs -- Better *1* for MBE ============================================================ ++ 1. Introduction ----- a. Industrial demands for faster ACL2 execution ----- b. Cons-with-hint -- Offered by Jared Davis and Sol Swords, Centaur Technology -- Requested incorporation into ACL2 source code And they generously wrote not only code but also documentation! ++ 2. Cons-with-hint ----- a. Logically, really cons (:pe cons-with-hint, or :pf) ----- b. Implementation (see source file axioms.lisp) -- avoids building a cons and garbage collection ; Probably avoid function call overhead: (declaim (inline cons-with-hint)) (defun cons-with-hint (x y hint) (declare (xargs :guard t) (ignorable hint)) #-acl2-loop-only (when (and (consp hint) (eql (car hint) x) (eql (cdr hint) y)) (return-from cons-with-hint hint)) (cons x y)) EXAMPLE: ACL2 !>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? (let ((x '(a . b))) (eq x (cons-with-hint 'a 'b x))) T ? ----- c. Example use: remove1-equal (see :doc remove1) (defun remove1-equal (x l) (declare (xargs :guard (true-listp l))) (cond ((endp l) nil) ((equal x (car l)) (cdr l)) (t (cons-with-hint (car l) (remove1-equal x (cdr l)) l)))) ; Experiment (defconst *c* (make-list 5)) :q ; Version 7.2: ? (eq *c* (remove1-equal 7 *c*)) NIL ? ; Latest ACL2 from GitHub: ? (eq *c* (remove1-equal 7 *c*)) T ? ----- d. Why not hons? (defun remove1-equal-with-hons (x l) (declare (xargs :guard (true-listp l))) (cond ((endp l) nil) ((equal x (car l)) (cdr l)) (t (hons (car l) (remove1-equal-with-hons x (cdr l)))))) (defconst *c* (fromto 0 1000000)) ; 0.02 seconds, 48 bytes allocated (time$ (null (remove1-equal -1 *c*))) ; 1.05 seconds, 84,688,688 bytes allocated (time$ (null (remove1-equal-with-hons -1 *c*))) Using ACL2 7.2, which did not have cons-with-hint: ; 0.18 seconds, 16,000,064 bytes allocated ----- e. Why not a "changedp" approach? Here is an example of the "changedp" approach. (defun remove1-equal-changedp (x l) (declare (xargs :guard t)) (cond ((atom l) (mv nil nil)) ((equal x (car l)) (mv t (cdr l))) (t (mv-let (changedp rest) (remove1-equal-changedp x (cdr l)) (cond (changedp (mv t (cons (car l) rest))) (t (mv nil l))))))) ; One could define a wrapper: (defun my-remove1-equal (x l) (mv-let (changedp ans) (remove1-equal-changedp x l) (declare (ignore changedp)) ans)) I asked Jared, and he answered that it complicated reasoning, even with MBE. ; Annoying: this fails without the :do-not hint. (thm (implies (true-listp l) (equal (mv-nth 1 (remove1-equal-changedp x l)) (remove1-equal x l))) :hints (("Goal" :do-not '(generalize)))) (Side remark: ACL2s gets this!) ++ 3. Getting the prover to treat cons-with-hint as cons ----- a. Motivation: Use cons-with-hint in ACL2 sources -- but preserve proofs (regression and user) ----- b. The problem via an example (admittedly contrived) The following succeeds in Version 7.2, but if cons-with-hint were added an ordinary function, then the proof would likely fail (as we'll see below). (thm (implies (and (integer-listp x) (symbolp a)) (equal (remove1-equal a x) x)) :hints (("Goal" :in-theory (union-theories '(integer-listp remove1-equal cons-car-cdr) (theory 'minimal-theory))))) Experiment we can do in ACL2 7.2: (defun cons-with-hint (x y hint) (declare (xargs :guard t) (ignore hint)) (cons x y)) (redef+) ; :program mode; can redefine system functions (defun remove1-equal (x l) ...) ; as in the latest ACL2 (redef-) ; :logic mode; redefinition off (verify-termination remove1-equal) (thm ...) ; as above; fails (cons-with-hint not enabled) ----- c. General remarks about solutions described below We are illustrating a key principle of research and development: don't be too committed to your first solution. We will show interesting implementation aspects. ++ 4. Solutions with MBE ("Must Be Equal") ----- a. Introduction to MBE -------- i. A simple example Here is a simple example from the ACL2 source code. (defun pairlis$-tailrec (x y acc) (declare (xargs :guard (and (true-listp x) (true-listp y) (true-listp acc)))) (cond ((endp x) (reverse acc)) (t (pairlis$-tailrec (cdr x) (cdr y) (cons (cons (car x) (car y)) acc))))) (defun pairlis$ (x y) (declare (xargs :guard (and (true-listp x) (true-listp y)) :verify-guards nil)) (mbe :logic (cond ((endp x) nil) (t (cons (cons (car x) (car y)) (pairlis$ (cdr x) (cdr y))))) :exec (pairlis$-tailrec x y nil))) Guard verification requires proving the equality of the :logic and :exec code, assuming the guard. The following lemma is critical. (defthm pairlis$-tailrec-is-pairlis$ (implies (true-listp acc) (equal (pairlis$-tailrec x y acc) (revappend acc (pairlis$ x y))))) (verify-guards pairlis$) -------- ii. Evaluation of MBE calls Continuing with the example above, we now see that calls of MBE execute only their :EXEC forms under guard-verified functions. (This is generally true for :program mode functions, too.) Consider the following trace. So-called "*1*" or "executable-counterpart" functions like ACL2_*1*_ACL2::PAIRLIS$ are defined by ACL2, and check guards before passing control to the function being defined, in this case, PAIRLIS$. ACL2 !>(trace$ pairlis$ pairlis$-tailrec) ((PAIRLIS$) (PAIRLIS$-TAILREC)) ACL2 !>(pairlis$ '(a b) '(1 2)) 1> (ACL2_*1*_ACL2::PAIRLIS$ (A B) (1 2)) 2> (PAIRLIS$ (A B) (1 2)) 3> (PAIRLIS$-TAILREC (A B) (1 2) NIL) <3 (PAIRLIS$-TAILREC ((A . 1) (B . 2))) <2 (PAIRLIS$ ((A . 1) (B . 2))) <1 (ACL2_*1*_ACL2::PAIRLIS$ ((A . 1) (B . 2))) ((A . 1) (B . 2)) ACL2 !> -------- iii. Reasoning with MBE calls The ACL2 prover works hard to remove MBE calls in favor of their :LOGIC parts. In the example above, we have: ACL2 !>:pf pairlis$ (EQUAL (PAIRLIS$ X Y) (AND (CONSP X) (CONS (CONS (CAR X) (CAR Y)) (PAIRLIS$ (CDR X) (CDR Y))))) ACL2 !> We'll talk later about this process of "remove-guard-holders" for storing the body of a definition. ----- b. A simple solution with MBE (defun cons-with-hint-fn (x y hint) (declare (xargs :guard t) (ignorable hint)) #-acl2-loop-only (when (and (consp hint) (eql (car hint) x) (eql (cdr hint) y)) (return-from cons-with-hint-fn hint)) (cons x y)) (defmacro cons-with-hint (x y hint) (declare (ignorable hint)) `(mbe :logic (cons ,x ,y) :exec (cons-with-hint-fn ,x ,y ,hint))) BUT unfortunately, using MBE slowed down the regression. ; old real 238m45.805s user 1582m12.957s sys 51m49.538s ; new real 254m21.971s user 1705m31.807s sys 52m32.166s Moreover, there was one failure, due to CCL's compiler failure to handle a large *1* function definition. ----- c. A better solution with MBE: sharing The following code avoids recomputation of x and y when both :logic and :exec are evaluated as part of a guard-check (see below for a simple example). (defmacro cons-with-hint (x y hint) (declare (ignorable hint)) `(let ((x-in-cons-with-hint ,x) (y-in-cons-with-hint ,y)) (mbe :logic (cons x-in-cons-with-hint y-in-cons-with-hint) :exec (cons-with-hint-fn x-in-cons-with-hint y-in-cons-with-hint (check-vars-not-free (x-in-cons-with-hint y-in-cons-with-hint) ,hint))))) This solved most of the slowdown, without any failures; see "newer" just below. ; old real 238m45.805s user 1582m12.957s sys 51m49.538s ; new real 254m21.971s user 1705m31.807s sys 52m32.166s ; newer real 240m50.798s user 1593m57.865s sys 52m43.108s To see what's going on, consider for example: (defun id (x) (declare (xargs :guard t)) x) In the current version: ACL2 !>(trace$ id) ((ID)) ACL2 !>(defconst *c* (cons-with-hint (id 3) 4 nil)) 1> (ACL2_*1*_ACL2::ID 3) 2> (ID 3) <2 (ID 3) <1 (ACL2_*1*_ACL2::ID 3) But if we first redefine cons-with-hint to be the old version: ACL2 !>(defconst *c* (cons-with-hint (id 3) 4 nil)) 1> (ACL2_*1*_ACL2::ID 3) 2> (ID 3) <2 (ID 3) <1 (ACL2_*1*_ACL2::ID 3) 1> (ACL2_*1*_ACL2::ID 3) 2> (ID 3) <2 (ID 3) <1 (ACL2_*1*_ACL2::ID 3) The problem is that defconst forms are evaluated in a so-called "safe-mode", where guards are checked aggressively. ----- d. Improving *1* code for functions that call MBE I investigated the code blow-up in a *1* function, and was able to reproduce it on a small example. Consider the following, which does not share the computation of x. (defmacro id (x) `(mbe :logic (identity ,x) :exec (identity ,x))) Here is a log for Version 7.2. ACL2 !>(defun foo7 (x) (id (id (id (id (id (id (id x)))))))) Since FOO7 is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO7. Summary Form: ( DEFUN FOO7 ...) Rules: NIL Time: 3.71 seconds (prove: 0.00, print: 0.00, other: 3.71) FOO7 ACL2 !>(defun foo10 (x) (id (id (id (id (id (id (id (id (id (id x))))))))))) Since FOO10 is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO10. *********************************************** ************ ABORTING from raw Lisp *********** Error: Function size exceeds compiler limitation. *********************************************** By contrast, for a very recent ACL2: ACL2 !>(defun foo7 (x) (id (id (id (id (id (id (id x)))))))) Since FOO7 is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO7. Summary Form: ( DEFUN FOO7 ...) Rules: NIL Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06) FOO7 ACL2 !>(defun foo10 (x) (id (id (id (id (id (id (id (id (id (id x))))))))))) Since FOO10 is non-recursive, its admission is trivial. We could deduce no constraints on the type of FOO10. Summary Form: ( DEFUN FOO10 ...) Rules: NIL Time: 0.46 seconds (prove: 0.00, print: 0.00, other: 0.46) FOO10 ACL2 !> To see the difference, let's trace the code that creates a *1* definition in each case (but with a lot less nesting). This is probably much too difficult to read; the point is simply that the code grows exponentially in Version 7.2, but that is solved by using FLET. I'll illustrate this point by using compare-windows to compare the traced return values. ; Version 7.2 ACL2 !>(trace! (oneify-cltl-code :native t)) TTAG NOTE: Adding ttag :TRACE! from the top level loop. ACL2 !>(defun f (x) (id (id x))) Since F is non-recursive, its admission is trivial. We could deduce no constraints on the type of F. 1> (ONEIFY-CLTL-CODE :LOGIC (F (X) (ID (ID X))) NIL |current-acl2-world|) <1 (ONEIFY-CLTL-CODE (ACL2_*1*_ACL2::F (X) (WHEN (EQ (SYMBOL-CLASS 'F (W *THE-LIVE-STATE*)) :COMMON-LISP-COMPLIANT) (RETURN-FROM ACL2_*1*_ACL2::F (F X))) (LABELS ((ACL2_*1*_ACL2::F (X) (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ACL2_*1*_COMMON-LISP::IDENTITY (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))) (T (IF **1*-AS-RAW* (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))))) (ACL2_*1*_COMMON-LISP::IDENTITY (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))) (T (IF **1*-AS-RAW* (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))))))) (T (IF **1*-AS-RAW* (ACL2_*1*_COMMON-LISP::IDENTITY (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))) (T (IF **1*-AS-RAW* (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))))) (ACL2_*1*_COMMON-LISP::IDENTITY (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X))) (T (IF **1*-AS-RAW* (ACL2_*1*_COMMON-LISP::IDENTITY X) (ACL2_*1*_COMMON-LISP::IDENTITY X)))))))))) (ACL2_*1*_ACL2::F X)))) Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !> ; Recent ACL2 ACL2 !>(trace! (oneify-cltl-code :native t)) TTAG NOTE: Adding ttag :TRACE! from the top level loop. ACL2 !>(defun f (x) (id (id x))) Since F is non-recursive, its admission is trivial. We could deduce no constraints on the type of F. 1> (ONEIFY-CLTL-CODE :LOGIC (F (X) (ID (ID X))) NIL |current-acl2-world|) <1 (ONEIFY-CLTL-CODE (ACL2_*1*_ACL2::F (X) (WHEN (EQ (SYMBOL-CLASS 'F (W *THE-LIVE-STATE*)) :COMMON-LISP-COMPLIANT) (RETURN-FROM ACL2_*1*_ACL2::F (F X))) (LABELS ((ACL2_*1*_ACL2::F (X) (FLET ((ONEIFY2612 NIL (ACL2_*1*_COMMON-LISP::IDENTITY (FLET ((ONEIFY2608 NIL (ACL2_*1*_COMMON-LISP::IDENTITY X)) (ONEIFY2609 NIL (ACL2_*1*_COMMON-LISP::IDENTITY X))) (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ONEIFY2609) (ONEIFY2608))) (T (IF **1*-AS-RAW* (ONEIFY2609) (ONEIFY2608))))))) (ONEIFY2613 NIL (ACL2_*1*_COMMON-LISP::IDENTITY (FLET ((ONEIFY2610 NIL (ACL2_*1*_COMMON-LISP::IDENTITY X)) (ONEIFY2611 NIL (ACL2_*1*_COMMON-LISP::IDENTITY X))) (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ONEIFY2611) (ONEIFY2610))) (T (IF **1*-AS-RAW* (ONEIFY2611) (ONEIFY2610)))))))) (COND ((F-GET-GLOBAL 'SAFE-MODE *THE-LIVE-STATE*) (ACL2_*1*_ACL2::RETURN-LAST 'MBE1-RAW (ONEIFY2613) (ONEIFY2612))) (T (IF **1*-AS-RAW* (ONEIFY2613) (ONEIFY2612))))))) (ACL2_*1*_ACL2::F X)))) Summary Form: ( DEFUN F ...) Rules: NIL Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) F ACL2 !> With this improvement, the times are as shown in "final" below. ; old real 238m45.805s user 1582m12.957s sys 51m49.538s ; new real 254m21.971s user 1705m31.807s sys 52m32.166s ; newer real 240m50.798s user 1593m57.865s sys 52m43.108s ; final real 236m35.631s user 1561m56.654s sys 51m21.151s ----- e. Summary statistics for a real example I started ACL2 after cd books/centaur/vl2014/loader/lexer/ and then ran the following commands. :ubt! 1 (ld "lexstate.port") (include-book "../config") (include-book "tokens") (time$ (ld "lexstate.lisp")) "VL2014" :ubu vl-plaintoken-alistp (defaggregate vl-lexstate ...) ; see lexstate.lisp RESULTS: ; with original definition of cons-with-hint (no MBE): Time: 0.29 seconds (prove: 0.16, print: 0.00, other: 0.13) ; for cons-with-hint defined using MBE, without sharing: Time: 3.45 seconds (prove: 0.16, print: 0.01, other: 3.28) ; for cons-with-hint defined using MBE, without sharing, ; but with FLET fix for *1* function generation: Time: 0.41 seconds (prove: 0.16, print: 0.01, other: 0.23) ; for cons-with-hint defined using MBE, with sharing ; but without FLET fix for *1* function generation: Time: 0.36 seconds (prove: 0.20, print: 0.01, other: 0.15) ; for cons-with-hint defined using MBE, with sharing and ; also with FLET fix for *1* function generation: Time: 0.35 seconds (prove: 0.19, print: 0.01, other: 0.15) ++ 5. Back to the start? ----- a. Issue: functions that are not guard-verified After all this, the following reason occurred to me to go back to Jared and Sol's original idea of an inlined function: efficiency for :logic mode functions whose guards haven't been verified. Consider the following example. (defun cons-with-hint-fn-alt (x y) (declare (xargs :guard t)) (cons x y)) (defun cons-alt (x y) (declare (xargs :guard t)) (cons x y)) (defun f (x y) ; guards not verified (mbe :logic (cons-alt x y) :exec (cons-with-hint-fn-alt x y))) (trace$ f cons-alt cons-with-hint-fn-alt) Then cons-with-hint-fn-alt is not called. ACL2 !>(f 3 4) 1> (ACL2_*1*_ACL2::F 3 4) 2> (ACL2_*1*_ACL2::CONS-ALT 3 4) 3> (CONS-ALT 3 4) <3 (CONS-ALT (3 . 4)) <2 (ACL2_*1*_ACL2::CONS-ALT (3 . 4)) <1 (ACL2_*1*_ACL2::F (3 . 4)) (3 . 4) ACL2 !> If you imagine that the MBE call under f is a call of the macro cons-with-hint, you can see that we would be calling cons, not cons-with-hint-fn. That seems to me like a severe punishment for not having verified guards. There are other circumstances where evaluation of the :logic part can happen, like in safe-mode. Here, cons-alt and cons-with-hint-fn-alt are both guard-verified, but that doesn't help to avoid the equality check for MBE. ACL2 !>(defconst *c* (mbe :logic (cons-alt 3 4) :exec (cons-with-hint-fn-alt 3 4))) 1> (ACL2_*1*_ACL2::CONS-WITH-HINT-FN-ALT 3 4) 2> (CONS-WITH-HINT-FN-ALT 3 4) <2 (CONS-WITH-HINT-FN-ALT (3 . 4)) <1 (ACL2_*1*_ACL2::CONS-WITH-HINT-FN-ALT (3 . 4)) 1> (ACL2_*1*_ACL2::CONS-ALT 3 4) 2> (CONS-ALT 3 4) <2 (CONS-ALT (3 . 4)) <1 (ACL2_*1*_ACL2::CONS-ALT (3 . 4)) Summary Form: ( DEFCONST *C* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *C* ACL2 !> Here, for reference, is what I wrote about that in an email I sent to Jared and Sol. P.S. I've thought of another argument in favor of not changing cons-with-hint, i.e., leaving it as a function. In that world, cons-with-hint has the desired functionality even in :logic mode functions that haven't been guard-verified. So maybe remove-guard-holders is the way to go after all. (I mentioned guard-holders in the notes I attached, but I hadn't thought of a good excuse for complicating that notion; now, because of non-guard-verified functions, maybe I have one.) ----- b. Using the original definition So we use the original definition of cons-with-hint: (defun cons-with-hint (x y hint) (declare (xargs :guard t) (ignorable hint)) #-acl2-loop-only (when (and (consp hint) (eql (car hint) x) (eql (cdr hint) y)) (return-from cons-with-hint hint)) (cons x y)) Since this definition is guard-verified, the special #-acl2-loop-only code will always be run. Since cons-with-hint is declaimed inline, we expect to avoid any function call overhead for it. ----- c. Prover trick #1: remove-guard-holders So we seem to be back where we started! Recall that the following example fails if we do not take special measures. (thm (implies (and (integer-listp x) (symbolp a)) (equal (remove1-equal a x) x)) :hints (("Goal" :in-theory (union-theories '(integer-listp remove1-equal cons-car-cdr) (theory 'minimal-theory))))) Now, :pe remove-equal shows this: V -872 (DEFUN REMOVE1-EQUAL (X L) (DECLARE (XARGS :GUARD (TRUE-LISTP L))) (COND ((ENDP L) NIL) ((EQUAL X (CAR L)) (CDR L)) (T (CONS-WITH-HINT (CAR L) (REMOVE1-EQUAL X (CDR L)) L)))) L)))) But there's no cons-with-hint here, using :pf instead of :pe. ACL2 !>:pf remove1-equal (EQUAL (REMOVE1-EQUAL X L) (AND (CONSP L) (IF (EQUAL X (CAR L)) (CDR L) (CONS (CAR L) (REMOVE1-EQUAL X (CDR L)))))) ACL2 !> The reason is that ACL2 removes certain so-called "guard holders" before storing the body of a definition (and in many other parts of the prover, actually). Here is an example based on pairlis$ above, but renamed. ACL2 !>(trace$ remove-guard-holders) ((REMOVE-GUARD-HOLDERS)) ACL2 !>(defun pairlis$2 (x y) (declare (xargs :guard (and (true-listp x) (true-listp y)) :verify-guards nil)) (mbe :logic (cond ((endp x) nil) (t (cons (cons (car x) (car y)) (pairlis$2 (cdr x) (cdr y))))) :exec (pairlis$-tailrec x y nil))) [.... output omitted ....] 1> (REMOVE-GUARD-HOLDERS (RETURN-LAST 'MBE1-RAW (PAIRLIS$-TAILREC X Y 'NIL) (IF (ENDP X) 'NIL (CONS (CONS (CAR X) (CAR Y)) (PAIRLIS$2 (CDR X) (CDR Y)))))) <1 (REMOVE-GUARD-HOLDERS (IF (ENDP X) 'NIL (CONS (CONS (CAR X) (CAR Y)) (PAIRLIS$2 (CDR X) (CDR Y))))) [.... output omitted ....] PAIRLIS$2 ACL2 !>:pf pairlis$2 (EQUAL (PAIRLIS$2 X Y) (AND (CONSP X) (CONS (CONS (CAR X) (CAR Y)) (PAIRLIS$2 (CDR X) (CDR Y))))) ACL2 !> So, we changed remove-guard-holders to remove cons-with-hint. For example: ACL2 !>(remove-guard-holders '(cons-with-hint (f x) (g y))) (CONS (F X) (G Y)) ACL2 !> ----- d. Prover trick #2: expandable boot-strap functions ACL2 has a constant, *expandable-boot-strap-non-rec-fns*, whose value is a list of function symbols that now includes cons-with-hint. Calls of these function symbols are forcibly expanded, even when disabled, in many parts of the prover. Here is an example. ACL2 !>(thm (equal (cons-with-hint x y hint) (cons x y)) :hints (("Goal" :in-theory nil))) [.... theory warnings omitted here ....] Proof succeeded. ACL2 !> If we run that proof after tracing the prover function expand-abbreviations, which is used for the "preprocess" step of the waterfall, we get: 2> (EXPAND-ABBREVIATIONS (CONS-WITH-HINT X Y HINT) NIL NIL NIL NIL 999 536870910 |some-enabled-structure| |current-acl2-world| |*the-live-state*| NIL) <2 (EXPAND-ABBREVIATIONS 536870903 (CONS X Y) ((LEMMA (:DEFINITION CONS-WITH-HINT)))) ++ 6. Summary ----- a. Cons-with-hint is incorporated into ACL2 -- essentially unchanged from Jared and Sol ----- b. Might proofs fail when using cons-with-hint? -- Thought about this when modifying ACL2 built-ins ----- c. Tried MBE -- I didn't use sharing when I should have. -- (Note that MEMBER etc. use LET-MBE.) But I couldn't use LET-MBE because it doesn't syntactically allow the HINT argument. -- This exposed *1* code generation issue for MBE -- Fixed using FLET -- Use of sharing fixed the problem -- But how about non-guard-verified functions? ----- d. Reverted to cons-with-hint as a function (no MBE) -- Used prover tricks to avoid proof failures ----- e. Outcomes -- Fast cons-with-hint that preserves proofs -- Better *1* for MBE