Published: 24th May 2022 DOI: 10.4204/EPTCS.359 ISSN: 2075-2180 |
This volume contains the proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022), a two-day workshop held in Austin, Texas, USA, and online, on May 26-27, 2022, on the University of Texas campus. ACL2 workshops occur at approximately 18-month intervals, and they provide a major technical forum for users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications. This workshop was delayed 6 months from the normal schedule to support an in-person workshop during the COVID pandemic.
ACL2 is an industrial-strength automated reasoning system, the latest in the Boyer-Moore family of theorem provers. The 2005 ACM Software System Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2 and the other theorem provers in the Boyer-Moore family.
The proceedings of ACL2-2022 include fourteen long papers and two extended abstracts. Each submission received three reviews. The workshop also included several "rump session" talks - short unpublished presentations that discussed ongoing research - as well as two invited talks from Jade Alglave from ARM and University College London, and Marijn Heule from Carnegie Mellon University.
This workshop would not have been possible without the support of a large number of people. We thank those who authored, submitted, and presented papers. We also wish to thank the Program Committee for their diligence in reviewing the papers in a timely manner and for further discussions after the reviews. We are very grateful to the invited speakers for agreeing to provide their unique and extensive perspectives to the workshop participants. We thank EasyChair, EPTCS, and arXiv, for their excellent continued logistical support for technical conferences like this workshop. And finally, we thank the ACL2 community as a whole for continuing to develop and push the boundaries of formal verification with our favorite little theorem prover.
Rob Sumners and Cuong Chau
May, 2022
ACL2 2022 Program Committee:
Abstract: ACL2 has long supported single-threaded objects, or stobjs, which are named, mutable structures that support efficient execution. A stobj-table is a map associating each stobj name in its (finite) domain with a corresponding stobj. Stobj-tables relax the otherwise strict rules on the use of stobjs to allow a container which can hold any stobj (even stobjs that are defined later). We introduce stobj-tables, provide some notes on their use and design, and present a motivating example of program refinement using stobj-tables.
Introduction: A single-threaded object, or stobj[1], is an ACL2 structure that is represented logically as a list of fields but, during raw Lisp execution, is updated efficiently in place rather than by copying a list structure. Syntactic restrictions guarantee that these in-place updates are faithful to the applicative semantics of ACL2.
A stobj field can be a scalar, an array, or a hash-table -- or, now, a stobj-table. A stobj-table field is much like a hash-table field, in that logically it is an alist but in raw Lisp it is a hash-table. Each key is a stobj name, which is associated with a stobj satisfying the stobj recognizer for that name.
Stobj-tables provide substantial flexibility by avoiding the need to pass various stobjs
explicitly through an application's code. Instead one can pass a single stobj-table parameter to a function,
which can read and modify the appropriate stobjs in that table. We illustrate this idea
below. Additional examples may be found in the community books, in file
system/tests/stobj-table-tests-input.lsp
with corresponding output file system/tests/stobj-table-tests-log.txt
.
Although a stobj-table field can be just one of many fields of a
stobj, a stobj-table might well be the unique field of a stobj, such as
the following, from community book std/stobjs/stobj-table.lisp
-- which, by the way, has some basic examples (local to the book) showing
the use of stobj-tables.
(defstobj stobj-table (tbl :type (stobj-table)))
In such a single-field case, we often refer to the entire stobj as a "stobj-table" (even though
technically the stobj-table is the tbl
field here). This identification of a stobj with
its unique field is actually correct at the implementation level, where the
stobj is the field, thus saving a level of indirection in any
access.1 The block of code below shows the definition of a
function, flip-switch
, which pulls out an instance of a
switch
stobj from a stobj-table (or a fresh (create-switch)
if the symbol,
switch
, is not bound in the stobj-table) using
a stobj-let
2 and flips the switch before
putting it back into
the stobj-table.
(include-book "std/stobjs/stobj-table" :dir :system)
(defstobj switch fld)
(defun flip-switch (stobj-table)
(declare (xargs :stobjs (stobj-table)))
(stobj-let ((switch (tbl-get 'switch stobj-table (create-switch))))
(switch) (update-fld (not (fld switch)) switch)
stobj-table))
(defun print-switch (stobj-table)
(declare (xargs :stobjs (stobj-table)))
(stobj-let ((switch (tbl-get 'switch stobj-table (create-switch))))
(current) (if (fld switch) "ON" "OFF")
current))
Remarks.
(1) Stobjs
in a stobj-table are not global stobjs: the value of a stobj name,
st
, in the ACL2 loop is not the value of the key,
st
, in a stobj-table.
Both, however, satisfy the recognizer for st
. (2) A
stobj-table may contain abstract_stobjs[2], which are treated the same as
concrete stobjs. (3) The recognizer for a stobj-table field is just
T
. As a result, keys are looked up using hons-assoc-equal,
since it has a guard of T
, unlike the various flavors of assoc,
which require an alist argument. (4) The default function names
introduced for a stobj-table field are the same as those introduced for
a hash-table field, except that there is no get?
function.
See defstobj.
Motivating Example: Stobj-tables extend the possible uses of stobjs in ACL2 in many ways. For example stobj-tables may be used to define a recursive (or mutually recursive) datatype, where an instance of the stobj can have a reference (through a stobj-table) to another instance of the stobj. Stobj-tables also support defining a stobj which can lazily and selectively instantiate child stobjs in a stobj-table as needed, rather than declaring all possible child stobjs as nested stobjs or arrays of stobjs in the parent. For this paper, we present a key motivation for adding stobj-tables: extending ACL2's support for stobjs in program refinement.
ACL2 supports a form of program refinement through the use
of constrained
functions
and attachments.
For an example of program refinement, consider the abstract process scheduler in the block of code
below -- this example is fully elaborated in community book
books/demos/stobj-table-examples.lisp
.
The scheduler and processes are modeled by the
constrained functions in
the encapsulation
with exported properties sufficient to define a function,
run
, defined on a stobj,
st
. That function iteratively calls the scheduler (via the
(pick st)
function) to choose a process identifier p
which
is then checked to see if the process is ready (via
(ready p st)
) and if it is, then the process
is executed (via (exec p st)
) and
run
recurs. If the scheduler was unable to return a process id that was
ready, then it is either the case that all processes have completed or some error condition has
occurred (e.g. a deadlock has been detected) and we report this and return. The encapsulation
codifies the properties of the constrained functions needed to define and admit
a run
function; the user can then attach executable definitions for the
constrained functions to refine the definition of run
to execute a
specific set of processes and scheduler. The benefit is that the definition and properties
of run
do not rely on the details of the processes and scheduler and the
same
run
function definition can be used with different attachments for
different processes and schedulers.
In order to make this run
function efficient, we define it (and the
constrained functions) to use a stobj st
for efficient access and
destructive update of the state for the executing processes. Before stobj-tables, this posed an
unfortunate problem; in particular, any state required to execute processes or the scheduler would
need to be defined a priori in the definition of the stobj st
. This
requirement defeats much of the benefit of program refinement via encapsulation and attachments
since the stobj st
would need to be defined with a knowledge of what
processes or kinds of processes might be executed. With stobj-tables, the definition
of st
can include a stobj-table which can be accessed with stobjs defined
later (specifically supporting processes or a scheduler the user wants to add) without affecting the
potential use of run
for execution and the proven properties of
run
. An example application is provided in the
supporting
materials, where a simple scheduler and processes are added via incremental attachments to the
constrained functions. This use of program refinement with stobjs would simply not have been viable
without stobj-tables.
(encapsulate
(((proc-ids) => *) ((pick st) => *) ((ready * st) => *) ((exec * st) => st) ((rank * st) => *))
...
(defthm rank-is-natural (natp (rank p st)))
(defthm pick-is-proc-id (member-equal (pick st) (proc-ids)))
(defthm exec-no-interfere (implies (not (= p q)) (<= (rank p (exec q st)) (rank p st))))
(defthm exec-rank-reduces (implies (ready p st) (< (rank p (exec p st)) (rank p st)))))
...
(defun run (st)
(declare (xargs :measure (sum-rank (proc-ids) st) :stobjs (st)))
(let ((p (pick st)))
(if (ready p st) (let ((st (exec p st))) (run st))
(report-completion-or-error-and-return p st))))
Concluding Remarks: Stobj-tables provide a convenient way to write efficient, flexible, formally verifiable functions that traffic in stobjs, without having to pass around numerous stobjs or pin down in advance which stobjs are used. Stobj-tables are easily accessed and updated using the existing stobj-let mechanism. We conclude with remarks on a couple of issues.
Consider, when accessing a stobj st
from a stobj-table
tbl
, whether the result satisfies the recognizer
for st
. This is true during evaluation, yet it is not provable in the
logic! Fortunately, ACL2 assumes that such recognizers do hold during guard verification -- which,
after all, supports evaluation[3]. The recognizer unprovability in general is a
consequence of designing stobj-table access to support proofs; in particular, the
book stobj-table-recognizer-issue.lisp
in the supporting materials illustrates how read-over-write properties may fail to prove otherwise.
A second issue pertains to undoing the definition of a stobj
st
from the logical world
(as with :ubt
):
then whenever the symbol st
is a key of a
stobj-table, that key is removed. This is obviously necessary to avoid
getting a non-existent "live" stobj. It is carried out by ACL2 source
function retract-stobj-tables
, which is
introduced logically with a partial-encapsulate
form to avoid the need to spell out the removal process. The
implementation takes care of the actual key removal with raw Lisp code,
as discussed in a comment in the raw Lisp
("#-acl2-loop-only"
) definition of
retract-stobj-tables
, which also discusses the
use of an implementation-level hash-table to keep track of which stobj
names are current.
Acknowledgments. We thank J Moore for feedback on this paper and ForrestHunt, Inc. for supporting the research reported herein, which also was performed in part at Centaur Technology.
While recursive definitions directly support induction in ACL2 proofs, iteration is often more natural for programming. Previous work [4] introduced a restricted analogue (loop$ FOR ..) of the Common Lisp loop iteration macro. Here we introduce a more flexible (but still restricted) ``DO loop$'' iteration construct, (loop$ WITH .. DO ..), which supports an imperative style of programming and permits the return of stobjs [1] and multiple values. For details see the ACL2 documentation [3], especially the topic LOOP$ for an overview and the topic DO-LOOP$ for details and a pointer to more examples.1
Our first example reviews FOR loop$s, summing the squares of elements of list (1 2 3 4).
ACL2 !>(loop$ FOR i in '(1 2 3 4) SUM (* i i)) 30 ACL2 !>
Here is an analogous DO loop$ example. Local variables sum and lst are initialized as shown, and then the DO body (following the DO keyword) is evaluated repeatedly, updating sum and lst until sum is returned. The use of return terminates the loop and provides the value returned by the loop.
ACL2 !>(loop$ WITH sum = 0 WITH lst = '(1 2 3 4) DO (if (consp lst) (let ((sq (* (car lst) (car lst)))) (progn (setq sum (+ sq sum)) ; sum := (+ sq sum) (setq lst (cdr lst)))) ; lst := (cdr lst) (return sum))) ; stop iterating and return the current value of sum 30 ACL2 !>
Unlike FOR loop$s, DO loop$s have no explicit range and support imperative programming with assignment, stobjs, and multiple values. Assignments with setq and (discussed below) mv-setq to settable variables — those declared by WITH as well as stobjs — are connected by progn, and iteration proceeds until a return call is executed. The following example returns the same sum of squares as above, but also stores a list of these squares in a stobj. Below are four initial forms, then a log for the rest, and finally explanation. This and other examples are in the supporting materials for this paper. Important: The initial include-book form is key for most non-trivial uses of loop$.
(include-book "projects/apply/top" :dir :system) (defstobj st fld) (defwarrant fld) (defwarrant update-fld) ACL2 !>(loop$ WITH sum = 0 WITH lst = '(1 2 3 4) DO :VALUES (nil st) (if (consp lst) (let ((sq (* (car lst) (car lst)))) (progn (mv-setq (sum st) (let ((st (update-fld (cons sq (fld st)) st))) (mv (+ sq sum) st))) (setq lst (cdr lst)))) (return (mv sum st)))) (30 <st>) ACL2 !>(fld st) (16 9 4 1) ACL2 !>
That example illustrates multiple-value assignment, (mv-setq (v0 ... vn) form), subject to the same requirements as (mv-let (v0 ... vn) form ..). Each vi is a known stobj or bound by WITH (similarly for setq). The :VALUES keyword specifies the list of return ``types''; each is a stobj or nil. The defwarrant forms are necessary because of the use of apply$ [2] (discussed below and previously [4]), though defbadge suffices for bodies of :program-mode functions.
The following variant of our first DO loop$ example illustrates the :MEASURE keyword, which supplies a measure that decreases on each iteration. It is required in this case because ACL2 doesn't guess a suitable measure. This example also employs the use of loop-finish, which passes control to the FINALLY clause. That clause is then executed, but just once (not with iteration like the DO body).
(loop$ WITH sum = 0 WITH i = 1 DO :MEASURE (nfix (- 5 i)) (if (<= i 4) (let ((sq (* i i))) (progn (setq sum (+ sq sum)) (setq i (1+ i)))) (loop-finish)) FINALLY (return sum)) ; returns 30
A loop$ expression in guard-verified code is evaluated at the top level as the corresponding Common Lisp loop expression, where all uses of :VALUES, :MEASURE, and (discussed below) :GUARD have been removed. This Lisp evaluation is possible because progn, setq, and return are all defined in Lisp, and the ACL2 runtime provides mv-setq as an abbreviation for Lisp's multiple-value-setq. Therefore guard-verified loop$ evaluation can be quite efficient [4]. We are thus led to explore guard verification for loop$ expressions. The following example illustrates the issues and is explained below.
(defun f (n) ; (f 4) evaluates to 30 (declare (xargs :guard (natp n))) (loop$ WITH sum OF-TYPE integer = 0 WITH i = n DO :guard (natp i) (if (zp i) (return sum) (let ((sq (* i i))) (progn (setq sum (+ sq sum)) (setq i (1- i)))))))
An OF-TYPE declaration says that each assignment to its variable produces a value of the indicated type-spec. A :GUARD expression asserts that the indicated term holds at the start of each iteration of the DO body and must then hold at the next iteration (if any). Guard verification also requires proving that the measure decreases at each iteration. Again, see the DO-LOOP$ documentation for details.
The OF-TYPE declaration and :GUARD above are necessary, as guard verification fails if they are omitted. One of the checkpoints is displayed below. To understand it, understand that each iteration of the loop updates (using setq or mv-setq) an alist that maps variables to values. The expression (CDR (ASSOC-EQ-SAFE 'I ALIST)) represents the value of variable I in the alist, which should be a number since it is an argument of the * operation. Discussion below may clarify further.
(IMPLIES ... ; Hypotheses aren't important for this discussion. (ACL2-NUMBERP (CDR (ASSOC-EQ-SAFE 'SUM ALIST))))
ACL2 translates a DO loop$ to a call of the function do$ (definition displayed below). A key argument of do$ is its do-fn argument, which is a LAMBDA object with a single formal parameter, alist, representing a mapping of the free variables of the DO body to values. As do$ recurs it uses apply$ to apply the do-fn to its single argument, an alist, obtaining a list of three elements (exit-flg value new-alist). Let's look at the last two calls of apply$ on do-fn.
(APPLY$ (LAMBDA (ALIST) ...) (((SUM . 14) (LST . (4))))) ⟶ (NIL NIL ((SUM . 30) (LST . ()))))
(APPLY$ (LAMBDA (ALIST) ...) (((SUM . 30) (LST . ())))) ⟶ (:RETURN 30 ((SUM . 30) (LST . ())))
Here is the lightly-edited definition of do$. We again note that in the top-level loop, DO loop$ expressions in guard-verified code are executed as Common Lisp loop expressions, not as calls of do$.
(defun do$ (measure-fn alist do-fn finally-fn ...) (declare ...) (let* ((triple (true-list-fix (apply$ do-fn (list alist)))) (exit-token (car triple)) (val (cadr triple)) (new-alist (caddr triple))) (cond ((eq exit-token :return) val) ((eq exit-token :loop-finish) (let* ((triple (true-list-fix (apply$ finally-fn (list new-alist)))) (exit-token (car triple)) (val (cadr triple))) (if (eq exit-token :return) val ...))) ; Next we test that the measure decreases before recurring. Recall that this test will not be ; executed for guard-verified DO loop$ expressions evaluated in the ACL2 top-level loop. ((l< (lex-fix (apply$ measure-fn (list new-alist))) (lex-fix (apply$ measure-fn (list alist)))) (do$ measure-fn new-alist do-fn finally-fn ...)) (t <error>)))
Finally, we outline how do-fn is generated for a given DO body (or FINALLY clause). The process involves traversing the top-level IF and LET/LET*/MV-LET structure, replacing (progn (if tst tbr fbr) e) by (if tst (progn tbr e) (progn fbr e)), and replacing (progn (progn e1 e2) ...) by (progn e1 (progn e2 ...)). Then other transformations are reasonably straightforward; see ACL2 source function cmp-do-body-1 for details. In particular (progn (setq v e1) e2) is replaced by (let ((v e1)) e2'), where e2' the result of transforming e2; (return e) is transformed to `(:return ,e ,alist); and (loop-finish) is transformed to `(:loop-finish nil ,alist). At the leaves we return a formal alist binding 'v to v for each variable v.
Implementation issues for DO loop$ expressions, including translation and guard generation, are discussed in the Essay on Loop$ in ACL2 source file translate.lisp, specifically Section 11: DO Loop$s.
Acknowledgments. We thank ForrestHunt, Inc. for supporting the research reported herein.
1. We provide links like these to topics in the online documentation [3], in the online version of this paper.