On Incorporating the Common Lisp LOOP Macro into ACL2

J Moore, ACL2 seminar, 1/25/2019

Abstract

We describe a method for handling a small subset of CLTL LOOP statements so
that when they appear in guard verified defuns they are intact in the raw
Lisp versions of the defuns (and are thus executed as efficiently compiled
code).  We assume the reader is familiar with CLTL LOOPs.  One obscure
feature we exploit is the CLTL OF-TYPE clause, used in [1] below.

We will concentrate on one form of loop here:

(LOOP FOR v OF-TYPE spec IN lst SUM expr)                           ; [1]

the logical semantics of which is, somewhat informally,

(SUM (LAMBDA$ (v) (DECLARE (TYPE spec v)) expr) lst)                ; [2]

Loop statement [1] with semantics [2] allows us to explore the key question:

  What guard conjectures must be generated from [2] to ensure error-free
  execution of [1] in raw Lisp?

Related to that question is

  What lemma machinery do we need to support guard proofs for loops?

The answers to these questions allow the natural extension of the class of
loops we handle to include loop operators other than SUM, such as COLLECT,
ALWAYS, and APPEND.  In addition, the ``target clause'' of the LOOP, e.g., IN
lst, can easily be extended to include FROM i TO j BY k and ON lst as target
clauses.  We can also add UNTIL and WHEN clauses in a semantically
compositional way so that, e.g.,

(LOOP FOR v IN lst UNTIL p WHEN q COLLECT r)

is logically

(COLLECT (LAMBDA$ (v) r)
         (WHEN (LAMBDA$ (v) q)
               (UNTIL (LAMBDA$ (v) p) lst)))

All of the loop features mentioned above are included in what we call
``plain'' loops: loops that have a single iteration variable and no other
free variables.

After we discuss the semantic and guard issues for plain loops, we introduce
``fancy'' loops by adding AS clauses which allow for multiple iteration
variables over multiple targets, and allow for variables other than the
iteration variables.  An example of a fancy loop is

(LOOP FOR v IN vlst AS u IN ulst SUM (+ c u v))

where c is bound outside the loop and is thus a constant in the loop.  Fancy
loops require a generalization of the basic semantic form and an elaboration
of the guard proof machinery.

Proofs mentioned here use a prototype ``loop book.''  If this design for loop
makes it into the ACL2 sources, the loop book will presumably become part of
the books/projects/apply/apply-lemmas book.