[acl2/acl2] 700177: Multiple changes (discussed further below). (1) M...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 7001770ad5a5b19f93fede6f3b2762ec598be2ed
https://github.com/acl2/acl2/commit/7001770ad5a5b19f93fede6f3b2762ec598be2ed
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/projects/apply/semi-concrete-do-inductions-log.txt
M books/system/apply/loop-scions.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M translate.lisp

Log Message:
-----------
Multiple changes (discussed further below). (1) Modified swap-stobjs to cause error when exactly one argument is a live stobj. (2) Allow DO loop$ expressions with no WITH clauses. (3) Fixed stobj-returning do$ to handle measures in a single-threaded way. (4,7) Avoid errors for some other stobj-returning DO loop$ expressions. (5) Do more complete job of avoiding certain calls (including swap-stobj and return-last) in the top-level loop. (6) Restore prohibition of stobj creator calls except in non-evaluation contexts like theorems.

Thanks to J for collaboration on (many of) these changes.

(1) Quoting an existing item in :DOC note-8-7, except that the
"Technical Note" at the end is new; it describes a change to
swap-stobjs made with this commit.

Fixed a soundness bug based on the use of [swap-stobjs] on two
[stobj]s of which one is ``live''. See [live-stobj-in-proof].
Thanks to Sol Swords for reporting this bug, including an example
and analysis of possible fixes in his report. (Technical Note. We
have added code to check for live [stobj]s in proofs, which was
sufficient to fix the bug. But the situation described above is
caught by a change to swap-stobjs, which now signals an error in
the relevant case (exactly one live stobj input).)

Quoting :DOC note-8-7 (preceding each by a number, for reference above
and/or below):

(2)
DO [Loop$] expressions (see [do-loop$]) are now allowed that have no
WITH clauses. Formerly, an expression (loop$ do ...) caused an
error with a rather nonsensical message.

(3)
For a DO [loop$] expression returning a [stobj] that participates in
its measure, it was possible to get an inappropriate runtime
measure error. (An example appears in a comment in the definition
of [do$] in the ACL2 sources.) This bug has been fixed by
modifying the definition of [do$] to respect singled-threadedness.

(4)
A DO [loop$] expression returning a [stobj] could cause a confusing
error; see ACL2 source function chk-for-live-stobj for an example.
This bug has been fixed so that no error occurs.

(5)
ACL2 did an incomplete job of excluding certain forms from being
evaluated in the top-level loop, including calls of [swap-stobjs],
parallelism primitives ([pand], [por], [pargs], and [plet]) when
parallel evaluation is enabled (ACL2(p) only), and [return-last]
calls. For example, no error was signalled by the following, even
though the two stobjs were not swapped (as shown below).

(defstobj st1 (fld1))
(defstobj st2 (fld2) :congruent-to st1)
(update-fld1 1 st1)
(update-fld2 2 st2)
(assert-event (and (equal (fld1 st1) 1) (equal (fld2 st2) 2)))
; The following is equivalent to (swap-stobjs st1 st2), and it
; now causes an error but it did not cause an error in Version 8.6:
(mv-let (st1 st2) (swap-stobjs st1 st2) (mv st1 st2))
; The following succeeds, showing that st1 and st2 were not actually swapped:
(assert-event (and (equal (fld1 st1) 1) (equal (fld2 st2) 2)))

This bug has been fixed.

(6)
[Stobj] creators are once again disallowed in execution contexts (but
are still allowed in theorems). This requirement was relaxed
(perhaps inadvertently) in Version 8.5. The following example
shows a problem with relaxing that restriction, as these events are
accepted in Versions 8.5 and 8.6, but no longer.

(defstobj st fld)
; Admitted in Versions 8.5 and 8.6, but no longer:
(defun foo () (declare (xargs :guard t)) (create-st))
(update-fld 3 st)
(assert-event (equal (fld st) 3))
; Should not change global value of st:
(foo)
; But (fld st) has indeed changed:
(assert-event (equal (fld st) nil))

Regarding Item #6 just above on stobj creators:
An attempt to call a stobj creator in the top-level loop or a defun
body will now cause an error such as the one displayed below, which
explains how defun-nx and non-exec can be used to avoid the error.
Indeed, a couple of books failed certification after this change, but
I fixed that by wrapping two creator calls in (non-exec ...), which is
presumably harmless since these were in the :logic fields of mbe
calls.

ACL2 Error [Translate] in TOP-LEVEL: It is illegal to call CREATE-ST
in this context because it is a stobj creator. Calls of stobj creators
cannot appear in top-level loop inputs or in function bodies (unless
in the scope of defun-nx or non-exec), although they may be called
in theorems. Note: this error occurred in the context (CREATE-ST).

(7) The following caused a raw Lisp error in recent ACL2 github
versions (though not in ACL2 Version 8.6), but now succeeds.

(include-book "projects/apply/top" :dir :system)
(defstobj st fld)
(defwarrant stp)
(defwarrant fld)
(defwarrant update-fld)
(update-fld '(a b c d) st)
(loop$ with x = '(a b c)
do
:guard (stp st) ; needed for producing an error in recent versions
:values (st)
(cond ((atom x)
(return st))
(t (progn (setq x (cdr x))
(setq st
(update-fld (car x) st))))))



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing