Published: 24th May 2022
DOI: 10.4204/EPTCS.359
ISSN: 2075-2180

EPTCS 359

Proceedings Seventeenth International Workshop on the
ACL2 Theorem Prover and its Applications
Austin, Texas, USA, 26th-27th May 2022

Edited by: Rob Sumners and Cuong Chau

Preface
Rob Sumners and Cuong Chau
Extended Abstract: Stobj-tables
Matt Kaufmann, Rob Sumners and Sol Swords
1
Extended Abstract: Iteration in ACL2, WITH .. DO
Matt Kaufmann and J Strother Moore
5
All Prime Numbers Have Primitive Roots
Ruben Gamboa and Woodrow Gamboa
9
Using ACL2 To Teach Students About Software Testing
Ruben Gamboa and Alicia Thoney
19
A Mechanized Proof of Bounded Convergence Time for the Distributed Perimeter Surveillance System (DPSS) Algorithm A
David Greve, Jennifer Davis and Laura Humphrey
33
Properties of the Hebrew Calendar
David M. Russinoff
48
VWSIM: A Circuit Simulator
Warren A. Hunt Jr., Vivek Ramanathan and J Strother Moore
61
A Free Group of Rotations of Rank 2
Jagadish Bapanapally and Ruben Gamboa
76
Modeling Asymptotic Complexity Using ACL2
William D. Young
83
A Formalization of Finite Group Theory
David M. Russinoff
99
Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
Mertcan Temel
116
ACL2s Systems Programming
Andrew T. Walter and Panagiotis Manolios
134
Syntheto: A Surface Language for APT and ACL2
Alessandro Coglio, Eric McCarthy, Stephen Westfold, Daniel Balasubramanian, Abhishek Dubey and Gabor Karsai
151
A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
Alessandro Coglio
168
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
Alessandro Coglio
185
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2
David Hardin
202

Preface

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:


Extended Abstract: Stobj-tables

Matt Kaufmann (The University of Texas at Austin (retired))
Rob Sumners (Intel Inc.)
Sol Swords (Intel Inc.)

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-let2 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.

Footnotes

  1. A stobj is also represented in raw Lisp as its unique field when that field is a hash-table or an array other than a string.
  2. We include underlined links to ACL2 documentation[4] topics that expand on topics discussed in this extended abstract. In particular, see stobj and see stobj-table for detailed documentation on stobjs and stobj-tables, respectively.

References

  1. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In Shriram Krishnamurthi & C. R. Ramakrishnan, editors: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, Lecture Notes in Computer Science 2257, Springer, pp. 9-27, doi:10.1007/3-540-45587-6_3. Available at https://doi.org/10.1007/3-540-45587-6_3.
  2. Shilpi Goel, Warren A Hunt & Matt Kaufmann (2013): Abstract Stobjs and Their Application to ISA Mod- eling. Electronic Proceedings in Theoretical Computer Science 114, p. 54-69, doi:10.4204/eptcs.114.5. Available at http://dx.doi.org/10.4204/EPTCS.114.5.
  3. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose-Luis Ruiz-Reina, Robert W. Sumners, Daron Vroon & Matthew Wilding (2008): Efficient execution in an automated reasoning environment. J. Funct. Program. 18, pp. 15-46, doi:10.1017/S0956796807006338. https://doi.org/10.1017/S0956796807006338.
  4. M. Kaufmann, J S. Moore & The ACL2 Community (2021): The Combined ACL2+Books User's Manual. http://acl2.org/manual/index.html.

Extended Abstract: Iteration in ACL2, WITH .. DO

Matt Kaufmann (The University of Texas at Austin (retired))
J Strother Moore (The University of Texas at Austin (retired))

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.

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.

Footnotes

1. We provide links like these to topics in the online documentation [3], in the online version of this paper.

References

  1. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In Shriram Krishnamurthi & C. R. Ramakrishnan, editors: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, Lecture Notes in Computer Science 2257, Springer, pp. 9-27, doi:10.1007/3-540-45587-6_3.
  2. M. Kaufmann & J S. Moore (2018): Limited Second-Order Functionality in a First-Order Setting. Journal of Automated Reasoning, doi:10.1007/s10817-018-09505-9. Available at http://www.cs.utexas.edu/ users/kaufmann/papers/apply/
  3. M. Kaufmann, J S. Moore & The ACL2 Community (2021): The Combined ACL2+Books User's Manual. http://acl2.org/manual/index.html.
  4. Matt Kaufmann & J Strother Moore (2020): Iteration in ACL2. Electronic Proceedings in Theoretical Computer Science 327, p. 16-31, doi:10.4204/eptcs.327.2.