[acl2/acl2] e206c1: [FTY] Improve `defset`.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e206c13e1ae2abb31d19663c6b6d03104ca34781
https://github.com/acl2/acl2/commit/e206c13e1ae2abb31d19663c6b6d03104ca34781
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/fty/fty-set.lisp

Log Message:
-----------
[FTY] Improve `defset`.

Make some generated proofs more robust.

Enable a function in two proofs, to avoid an apparent dependency on tau.


Commit: 151f0fdf43876839b5e3680b5ca88ba57a3f7e14
https://github.com/acl2/acl2/commit/151f0fdf43876839b5e3680b5ca88ba57a3f7e14
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge.


Commit: 5965f1165a25f6cb980a6fac7e7b9d32b63a0aa8
https://github.com/acl2/acl2/commit/5965f1165a25f6cb980a6fac7e7b9d32b63a0aa8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/file-paths.lisp

Log Message:
-----------
[C$] Use controlled configuration.


Commit: 41257c092632eff9c3fdfa9663a5bd476db309c2
https://github.com/acl2/acl2/commit/41257c092632eff9c3fdfa9663a5bd476db309c2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/files.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: 4bbd83044438a3e0691c09cec28b088ff0287244
https://github.com/acl2/acl2/commit/4bbd83044438a3e0691c09cec28b088ff0287244
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Include two more books nneded for local development.


Commit: 151d27321ca1adb9ed5e96635d683d4303dd727a
https://github.com/acl2/acl2/commit/151d27321ca1adb9ed5e96635d683d4303dd727a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Tweak for consistency.

Remove "historical" comment no longer needed.

Move certification-related form at the end of the "preamble".


Commit: 66e029b7c900484a8c90488b096e529459d4bf20
https://github.com/acl2/acl2/commit/66e029b7c900484a8c90488b096e529459d4bf20
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Remove book inclusion now redundant.


Commit: 6add17b208012eccb1c3c07ccba325ed35665f10
https://github.com/acl2/acl2/commit/6add17b208012eccb1c3c07ccba325ed35665f10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Remove local theorem no longer needed.

Now that `fty::defset` has been improved to generate more robust proofs that do
not necessitate tau.


Commit: 744b4e7408f3995b879bf5ca9be97ddabeaed6ec
https://github.com/acl2/acl2/commit/744b4e7408f3995b879bf5ca9be97ddabeaed6ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Remove induction exception no longer needed.

Now the `fty` macros should generate the needed induction hints.


Commit: 702b7fe90517bd471f6dc5c3cd3cfa9b7e8ea0cc
https://github.com/acl2/acl2/commit/702b7fe90517bd471f6dc5c3cd3cfa9b7e8ea0cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Localize some hints.


Commit: e30a86b5dfb91c62132333fc3dcea039e27a710d
https://github.com/acl2/acl2/commit/e30a86b5dfb91c62132333fc3dcea039e27a710d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp

Log Message:
-----------
[C$] Use controlled configuration.


Commit: 775f8129c0f51a0eb64a628be0f6f6e44299ad69
https://github.com/acl2/acl2/commit/775f8129c0f51a0eb64a628be0f6f6e44299ad69
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp

Log Message:
-----------
[C$] Avoid redundant book inclusion.

Also reorder forms in preamble for consistency.


Commit: 7b076380542fcc68b542ab949b863cff27eb1de3
https://github.com/acl2/acl2/commit/7b076380542fcc68b542ab949b863cff27eb1de3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: 07cae5f2951da9ecc97119f7ced93b3828387eaf
https://github.com/acl2/acl2/commit/07cae5f2951da9ecc97119f7ced93b3828387eaf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/code-ensembles.lisp

Log Message:
-----------
[C$] Remove redundant book inclusion.


Commit: 9479b9b6c911c8cad9b19e29112140a85ca90aa3
https://github.com/acl2/acl2/commit/9479b9b6c911c8cad9b19e29112140a85ca90aa3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/type-specifier-lists.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: 4b5d6e203f32350f80241aa32b96aff78e384073
https://github.com/acl2/acl2/commit/4b5d6e203f32350f80241aa32b96aff78e384073
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/storage-specifier-lists.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: f9693e8e4dc46fa6a9af3bf1cccd748021237a21
https://github.com/acl2/acl2/commit/f9693e8e4dc46fa6a9af3bf1cccd748021237a21
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstraction-mapping.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: fabd61e448f1627acc7853974bc59509efc71261
https://github.com/acl2/acl2/commit/fabd61e448f1627acc7853974bc59509efc71261
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/parser-states.lisp

Log Message:
-----------
[C$] Use controlled configuration.


Commit: a82e9a4ad54bd244876efa334b586bdcc141122a
https://github.com/acl2/acl2/commit/a82e9a4ad54bd244876efa334b586bdcc141122a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/parser-messages.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: 0d5b816cc3265c08a45a94386b1f4340c5cced82
https://github.com/acl2/acl2/commit/0d5b816cc3265c08a45a94386b1f4340c5cced82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/lexer.lisp

Log Message:
-----------
[C$] Tweak some fixing theorems.


Commit: 4e8a5eefb0374b40b97e816fddbff56009ce5e6f
https://github.com/acl2/acl2/commit/4e8a5eefb0374b40b97e816fddbff56009ce5e6f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/x86/support-bv.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.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:
-----------
Merge.


Commit: bc72cf0228c4a14206754558909888a9cab59a84
https://github.com/acl2/acl2/commit/bc72cf0228c4a14206754558909888a9cab59a84
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Refactor preprocessor.

Move preprocessor states to dedicated file and topic.


Commit: f5e194c04463b39178bfa048e1be98bbeafbe82d
https://github.com/acl2/acl2/commit/f5e194c04463b39178bfa048e1be98bbeafbe82d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Refactor preprocessor.

Put preprocessor messages into dedicated file and topic.


Commit: f9102d508746d8578bf147b7f83640372196212c
https://github.com/acl2/acl2/commit/f9102d508746d8578bf147b7f83640372196212c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Refactor preprocessor.

Put reader into dedicated file and topic.


Commit: 6ef28d4dfbd5d658c5e330294eba26be4c8b8ed3
https://github.com/acl2/acl2/commit/6ef28d4dfbd5d658c5e330294eba26be4c8b8ed3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Refactor preprocessor.

Put lexer component into dedicated file and topic.


Commit: 396e081039c2b004634986e651cea807b93bd4b8
https://github.com/acl2/acl2/commit/396e081039c2b004634986e651cea807b93bd4b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Improve preprocessor code.

Rename a function.

Remove some now-unnecessary book inclusions.

Remove some now-unnecessary local forms.


Commit: a84f250f95dface3097fcfcaf8680c18a3b67d5a
https://github.com/acl2/acl2/commit/a84f250f95dface3097fcfcaf8680c18a3b67d5a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/preprocessor-reader.lisp

Log Message:
-----------
[C$] Add forgotten file.


Compare: https://github.com/acl2/acl2/compare/7001770ad5a5...a84f250f95df

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

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

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))))))

Compare: https://github.com/acl2/acl2/compare/a7fcf343836d...a84f250f95df