Matt Kaufmann
Cons-with-hint: An ACL2 development case study
ACL2 seminar, 3/8/2016

Abstract:

There are increasing industrial demands on ACL2, in particular on its
support for efficient execution.  Recently, Jared Davis and Sol Swords
proposed a new function, cons-with-hint, to improve efficiency of some
applications at Centaur Technology.  Logically, this function is just
cons, the ACL2 (and Lisp) pairing function; but it can avoid the cost
of creating a new cons pair (and its potential future garbage
collection) by returning an existing cons pair, the "hint" argument.
In this case study I'll first introduce cons-with-hint from a user
perspective and show its (simple and elegant) initial implementation,
as provided by Jared and Sol.  Then I'll discuss my journey towards
getting the ACL2 prover to treat cons-with-hint simply as cons, thus
illustrating a key principle of research and development: don't be too
committed to your first solution.  As a side effect, we will discuss,
I hope in a self-contained way, a few aspects of the ACL2
implementation that may not be well known.  In particular, after we
explain MBE ("must be equal") we will discuss an improvement, arising
from this work, that I've made to its so-called "*1*" (or "executable
counterpart") code.