[acl2/acl2] 2e6463: [axe] Improve packages.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 2e64636271d7c26aa2dada00c3043285bbcf3b0a
https://github.com/acl2/acl2/commit/2e64636271d7c26aa2dada00c3043285bbcf3b0a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp

Log Message:
-----------
[axe] Improve packages.


Commit: 4291655cab84658009210d5b3cacebee8dedaced
https://github.com/acl2/acl2/commit/4291655cab84658009210d5b3cacebee8dedaced
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/unroller.lisp

Log Message:
-----------
[axe] Move some rules.


Commit: 6828efda09466767d89c87434266b1b85f0fae44
https://github.com/acl2/acl2/commit/6828efda09466767d89c87434266b1b85f0fae44
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/x86/support-bv.lisp

Log Message:
-----------
[axe/x86] Add ash-constant-opener.


Commit: 6da6cfeee8704ad0cb9c79cfd9f008e6a59d8ba1
https://github.com/acl2/acl2/commit/6da6cfeee8704ad0cb9c79cfd9f008e6a59d8ba1
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/trim-intro-rules.lisp
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tutorial.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.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/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp

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


Commit: 631e4d43193177c7910aae2f1cc3296434b3561f
https://github.com/acl2/acl2/commit/631e4d43193177c7910aae2f1cc3296434b3561f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
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/file-paths.lisp
M books/kestrel/c/syntax/files.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/preprocessor.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: ebb5154ab13c6c133d83251e182b7c474314e6b4
https://github.com/acl2/acl2/commit/ebb5154ab13c6c133d83251e182b7c474314e6b4
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 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

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


Commit: 443210de6bfc80c65af9f42c3f441a30bc709f45
https://github.com/acl2/acl2/commit/443210de6bfc80c65af9f42c3f441a30bc709f45
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

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


Commit: a7fcf343836d8d7e60bd389f0667d469dce7a96d
https://github.com/acl2/acl2/commit/a7fcf343836d8d7e60bd389f0667d469dce7a96d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M books/kestrel/x86/support-bv.lisp

Log Message:
-----------
[x86] Comment out unneeded rules.


Compare: https://github.com/acl2/acl2/compare/390785d39556...a7fcf343836d

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: ab0ac943db540facf6128a0946141f840a49cfcc
https://github.com/acl2/acl2/commit/ab0ac943db540facf6128a0946141f840a49cfcc

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 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

Log Message:
-----------
[axe] Organize some supporting rules.


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: 648659da2e8f4c0d42b481fb00ffd02753998fe6
https://github.com/acl2/acl2/commit/648659da2e8f4c0d42b481fb00ffd02753998fe6

Commit: 9be633dd489626af5645fae703ad9e6cba143ad0
https://github.com/acl2/acl2/commit/9be633dd489626af5645fae703ad9e6cba143ad0

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:

M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Build in a rule.


Commit: 11eed579166dc54b48b3c28ac19031aa16da96d7
https://github.com/acl2/acl2/commit/11eed579166dc54b48b3c28ac19031aa16da96d7

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:

M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp

Log Message:
-----------
[bv-lists] Generalize a rule.


Commit: fe9c90f01bc21d97674057478acd96327cb3092e
https://github.com/acl2/acl2/commit/fe9c90f01bc21d97674057478acd96327cb3092e

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:

M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp

Log Message:
-----------
[axe/x86] Generalize supporting rule.

Commit: ebb5154ab13c6c133d83251e182b7c474314e6b4
https://github.com/acl2/acl2/commit/ebb5154ab13c6c133d83251e182b7c474314e6b4
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 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

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

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: 390785d395568da2db7f821b74f90c91b96dbfdb
https://github.com/acl2/acl2/commit/390785d395568da2db7f821b74f90c91b96dbfdb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-06 (Sat, 06 Dec 2025)

Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

Log Message:
-----------

[aleo] Update comment on GCL issue.


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: 443210de6bfc80c65af9f42c3f441a30bc709f45
https://github.com/acl2/acl2/commit/443210de6bfc80c65af9f42c3f441a30bc709f45
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

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


Commit: a7fcf343836d8d7e60bd389f0667d469dce7a96d
https://github.com/acl2/acl2/commit/a7fcf343836d8d7e60bd389f0667d469dce7a96d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)

Changed paths:
M books/kestrel/x86/support-bv.lisp

Log Message:
-----------
[x86] Comment out unneeded rules.

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


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.


Compare: https://github.com/acl2/acl2/compare/3d4d935d14d7...396e081039c2