ACL2 in Danfy eyes

I decided to translate an execise solution from the Dafny book to ACL2 language after I encountered an issue with the verifier that timing out on a lemma involing multiplication. This is how I discovered Dafny’s opaque function feature.

I then had to spend some time doing research to find suitable ways of translating types defined in Dafny into their ACL2 counterparts, because simply googling for answers or chating with LLMs did not always yield satisfactory results. Therefore, I would like to leave some newcomer feedback about ACL2.

Type system peculiarities

ACL2 is an extension of Lisp and does not provide built-in support for defining algebraic data types. There is defdata ACL2 bookb that provides macros for simulating data types found in languages such as Agda or Dafny. However, some common patterns cannot be translated literally, and type checker responses might be puzzling:

“data contructors” of a recursive algebraic type should have a field of its type or be atomic (eg. just Symbol or predefined type).
```
datatype FooOrBar = Foo(foo: nat) | Bar(bar: string)

(defdata FooOrBar (oneof (Foo (foo-n . nat)) (Bar (bar-s . string))))
```
Error:

HARD ACL2 ERROR in ACL2::UNION-CURRENT-THEORY-FN: A theory function has been called on a list that contains FOOORBARP, which does not designate a rule or a non-empty list of rules. See :DOC theories.

The workaround is to define an auxiliary record type for each data constructor:
```
(defdata Foo (record (foo-n . nat)))
(defdata Bar (record (bar-s . string)))
(defdata FooOrBar (oneof Foo Bar))
```
Plus identifiers for record field and type names may not be shared.
“data consructor” of a recusive algebraic type cannot reference itself inside listof and oneof combinators.
```
datatype MyTree = TreeLeaf | TreeNode(children: : List<MyTree>)

(defdata MyTree (oneof 'TreeLeaf (TreeNode (children . (listof MyTree)))))
```
Error:

HARD ACL2 ERROR in DEFDATA::PARSE: LISTOF should be a recognized name.

The workaround is similar to the previous one, but this time the type and its alias for the list comprise a pair of mutually recusive types.
```
(defdata
    (MyTree-List (listof MyTree))
    (MyTree (oneof 'TreeLeaf (TreeNode (children . MyTree-List)))))
```
Oops

ACL2 Error in ( MUTUAL-RECURSION ( DEFUN MYTREE-LISTP …) …): No :MEASURE was supplied with the definition of MYTREEP. Our heuristics for guessing one have not made any suggestions.

The error above might be caused by unintialized acls package (defdata is part of it).
```
(acl2::acl2s-common-settings)
```

Fast reload

Loading the acl2s package into a fresh ACL2 instance takes about 14 seconds on my laptop (Core i5, SSD, NixOS, no antivirus). It would not be a significant issue if it were an opertion executed only once during interpreter startup, but that is not the case.

ACL2, unlike Lisp, is intendend to run in an append-only mode; that is, once a name is bound to a definition, it cannot be changed. This restriction exists because a definition may be referenced by other definitions that were verified against the original version, and changing it could comprmise consistency.

The redefinition feature is currently off. See :DOC ld-redefinition- action. Note: XXX was previously defined at the top level.

The ability of ACL2 to detect and accept unchanged definitions during reloading mitigates the issue to some extent. However, during active debugging this feature is of limited help, because many definitions need to be changed frequently.

:REDEF

ACL2 can operate in a mode where redefinitions of functions and theorems are accepted, but this does not work for types.

(set-ld-redefinition-action '(:doit . :erase) state)
(defdata Foo (alistof string nat))
(defdata Foo (listof nat))

ACL2 Error in ( DEFMACRO NTH-FOO …): The name NTH-FOO is in use as a function, and it has an attachment. Before redefining it you must remove its attachment, for example by executing the form (DEFATTACH NTH-FOO NIL). We hope that this is not a significant inconvenience; it seemed potentially too complex to execute such a defattach form safely on your behalf.

Every type redefinition requires executing 2 defattach commands to allow the modified type definition to pass through.

Encapsulate

The encapsulate macro limits the scope of enclosed definitions to achieve an effect similar to redefinition, but it cannot isolate defdata definitions.

(encapsulate () (defdata Bar (listof nat)))
(encapsulate () (defdata Bar (alistof string nat)))

rebuild

Besides the ld command for loading ACL2 sources, there is also the rebuild command, but it reacts similarly to redefinition collisions.

Undo via :ubu and :ubt

Finally I’ve received a hint from the ACL2 Zulip chat that led to a working solution. As it turns out, despite the append-only nature of ACL2, there are several undo commands available. I found that :ubu suits my needs best. It can roll back all definitions up to a given name (e.g., a constant or a function), while keeping the referenced name itself - unlike :ubt - so the anchor name does not need to be recreated each time.

(INCLUDE-BOOK "acl2s/top" :DIR :SYSTEM) ;; load a big book once
(defconst *u-anchor* t)                 ;; define anchor name for quick rollbacks
(ld "lib-under-dev.lisp")               ;; contaminate ACL2 namespace
;; change defdata types in lib-under-dev.lisp
:ubu *u-anchor*                         ;; undef all names defined after *u-anchor* introduction
(ld "lib-under-dev.lisp")               ;;

Macros

ACL2 relies heavily on macros to provide features that appear in modern languages. An individual macro may look like a silver bullet, but macros do not compose well with one another, and they do not work well in REPL (the interactive ACL2 mode, i.e., the read-eval-print loop).

case-match macro is not working top repl.
```
ACL2 Error in TOP-LEVEL:  In the attempt to macroexpand the form
```
but the same expression wrapped into a defun is accepted withou any probrem.
there are several case macros (match, pattern-match, case-match). All variants of them always have an implicit default branch, even if pattern matching is performed by data constructors of an algebraic type.
```
(defdata Foo (record (foo-nat . nat)))
(defdata Baz (record (baz-nat . string)))
(defdata FooBaz (oneof Foo Baz))
(defun match-FooBaz (fb) (match fb (:Foo "foo") (:Baz "baz")))
```
i.e. type predicate for a function with case splitting allows returning null values:

type of MATCH-FOOBAZ is described by the theorem (OR (EQUAL (MATCH-FOOBAZ FB) NIL) (STRINGP (MATCH-FOOBAZ FB)))

ACL2 in Dafny eyes