[acl2/acl2] 38384f: [axe] Add symbol to packages.

0 views

Skip to first unread message

Eric W. Smith

unread,

Aug 12, 2026, 4:13:42 PM (7 days ago) Aug 12

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 38384f66fb024df32e1f16d8d65a1af7c29f40de
https://github.com/acl2/acl2/commit/38384f66fb024df32e1f16d8d65a1af7c29f40de
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-31 (Fri, 31 Jul 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp

Log Message:
-----------
[axe] Add symbol to packages.

Commit: d9b7cd345fc0ad46a0af292f9ff4a0f5d2afd7f6
https://github.com/acl2/acl2/commit/d9b7cd345fc0ad46a0af292f9ff4a0f5d2afd7f6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-31 (Fri, 31 Jul 2026)

Changed paths:
M books/kestrel/axe/utilities.lisp
M books/kestrel/utilities/make-var-names.lisp

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

Commit: e813748aafbd1f75342e0d47c7ed3a2ee27445e1
https://github.com/acl2/acl2/commit/e813748aafbd1f75342e0d47c7ed3a2ee27445e1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-02 (Sun, 02 Aug 2026)

Changed paths:
M axioms.lisp
M books/doc/relnotes.lisp
M books/kestrel/c/language/implementation-environments/execution-character-sets.lisp
M books/kestrel/c/package.lsp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/constant-expressions.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/constant-expressions.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/fty/character-any-map.lisp
M books/misc/check-acl2-exports.lisp
M books/std/omaps/core.lisp
A books/std/omaps/identity.lisp
M books/std/omaps/identityp.lisp
M books/std/omaps/injectivep.lisp
M books/std/omaps/package.lsp
M books/std/omaps/top.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/with-supporters.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M translate.lisp

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

Commit: c06d47c80c38784fbb91ad46a7cd41fa42e60367
https://github.com/acl2/acl2/commit/c06d47c80c38784fbb91ad46a7cd41fa42e60367
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-03 (Mon, 03 Aug 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/static-environments.lisp
M books/std/system/check-user-term-dollar.lisp
M books/std/util/definductive.lisp

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

Commit: 0ed206e712d584d682cf53bf8704e6cef158ba00
https://github.com/acl2/acl2/commit/0ed206e712d584d682cf53bf8704e6cef158ba00
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-05 (Wed, 05 Aug 2026)

Changed paths:
M books/centaur/aig/aig2c.lisp
M books/centaur/clex/example.lisp
M books/centaur/esim/vcd/esim-snapshot.lisp
M books/centaur/getopt/parsers.lisp
M books/centaur/getopt/top.lisp
M books/centaur/vl/util/defs.lisp
M books/kestrel/arm/.sys/mem...@useless-runes.lsp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
M books/kestrel/axe/bv-list-rules-axe.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
M books/kestrel/bv-arrays/array-patterns.lisp
M books/kestrel/bv-arrays/bv-array-conversions-gen.lisp
M books/kestrel/bv-arrays/bv-array-conversions2.lisp
M books/kestrel/bv-arrays/bv-array-write.lisp
M books/kestrel/bv-lists/bits-to-bytes-little2.lisp
M books/kestrel/bv-lists/bits-to-bytes2.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvchop-list.lisp
M books/kestrel/bv-lists/bytes-to-bits-little2.lisp
M books/kestrel/bv-lists/map-bvplus-val.lisp
M books/kestrel/bv-lists/map-bvsx.lisp
M books/kestrel/bv-lists/map-packbv-little.lisp
M books/kestrel/bv-lists/packbvs-little.lisp
M books/kestrel/bv-lists/packbvs.lisp
M books/kestrel/bv-lists/unpackbv.lisp
M books/kestrel/bv-lists/unsigned-byte-listp-def.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvlt.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/rotate.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules10.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules5.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvdivdown-rules.lisp
M books/kestrel/bv/sbvmoddown.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/bv/validation-smt-lib.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
M books/kestrel/c/transformation/struct-type-split.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/crypto/tea/inversion.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/ethereum/semaphore/r1cs-proof-rules.lisp
A books/kestrel/lists-light/intersectp-equal.lisp
M books/kestrel/lists-light/subsetp-equal.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/osets.lisp
A books/kestrel/remora/primitives-evaluation-first-order.lisp
A books/kestrel/remora/primitives-evaluation-on-ispaces.lisp
A books/kestrel/remora/primitives-evaluation-on-types.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation-tests.lisp
R books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/x86/bytes-loadedp.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/conditions.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/support.lisp
M books/kestrel/x86/support32.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp

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

Commit: 1cdeba184839e3be018054a426a3730640fb929b
https://github.com/acl2/acl2/commit/1cdeba184839e3be018054a426a3730640fb929b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-06 (Thu, 06 Aug 2026)

Changed paths:
M README.md
M books/kestrel/event-macros/screen-printing.lisp
M books/kestrel/remora/base-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/primitives-evaluation-first-order.lisp
M books/kestrel/remora/primitives-evaluation-on-ispaces.lisp
M books/kestrel/remora/primitives-evaluation-on-types.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/projects/hol-in-acl2/examples/README.txt
M books/projects/smtlink/trusted/run.lisp
M books/projects/smtlink/trusted/z3-py/translator.lisp
M books/projects/smtlink/verified/basics.lisp
M books/projects/smtlink/verified/expand-cp.lisp
M books/projects/smtlink/z3_interface/ACL2_to_Z3.py
M books/std/util/definductive-doc.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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

Commit: 799a461efc9355421978b4bcb7e851b2a29bdf41
https://github.com/acl2/acl2/commit/799a461efc9355421978b4bcb7e851b2a29bdf41
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

Changed paths:
M README.md
M books/doc/relnotes.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.lisp
M books/kestrel/bv-arrays/bv-array-clear-range.lisp
M books/kestrel/bv-arrays/bv-array-clear.lisp
M books/kestrel/bv-arrays/bv-array-write.lisp
M books/kestrel/bv-arrays/bv-arrays.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
A books/kestrel/data/.gitignore
A books/kestrel/data/benchmark/harness.lsp
A books/kestrel/data/hash/.sys/generi...@useless-runes.lsp
M books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/to-byt...@useless-runes.lsp
A books/kestrel/data/hash/.sys/to-b...@useless-runes.lsp
A books/kestrel/data/hash/benchmark/acl2-customization.lsp
A books/kestrel/data/hash/benchmark/benchmark.lsp
A books/kestrel/data/hash/benchmark/driver.lsp
A books/kestrel/data/hash/generic-fold.lisp
M books/kestrel/data/hash/jenkins-defs.lisp
M books/kestrel/data/hash/jenkins.lisp
M books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/to-bytes-defs.lisp
A books/kestrel/data/hash/to-bytes.lisp
M books/kestrel/data/hash/top.lisp
A books/kestrel/data/treemap/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treemap/benchmark/acl2-customization.lsp
A books/kestrel/data/treemap/benchmark/benchmark.lsp
A books/kestrel/data/treemap/benchmark/driver.lsp
A books/kestrel/data/treemap/generic-count.lisp
A books/kestrel/data/treemap/generic-typed.lisp
A books/kestrel/data/treemap/induction.lisp
M books/kestrel/data/treemap/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/jo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/ke...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/loo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rest...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rlo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/tr...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/updat...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/upd...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/val...@useless-runes.lsp
M books/kestrel/data/treemap/internal/antisymmetry.lisp
M books/kestrel/data/treemap/internal/bst.lisp
M books/kestrel/data/treemap/internal/count.lisp
M books/kestrel/data/treemap/internal/delete.lisp
M books/kestrel/data/treemap/internal/heap.lisp
M books/kestrel/data/treemap/internal/in-order.lisp
M books/kestrel/data/treemap/internal/join.lisp
M books/kestrel/data/treemap/internal/keys.lisp
M books/kestrel/data/treemap/internal/lookup.lisp
M books/kestrel/data/treemap/internal/min-max.lisp
M books/kestrel/data/treemap/internal/restrict.lisp
M books/kestrel/data/treemap/internal/submap.lisp
M books/kestrel/data/treemap/internal/tree.lisp
M books/kestrel/data/treemap/internal/update.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/map.lisp
M books/kestrel/data/treemap/size.lisp
M books/kestrel/data/treemap/to-omap.lisp
M books/kestrel/data/treemap/top.lisp
M books/kestrel/data/treemap/update.lisp
M books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/data/treeset/benchmark/.sys/ran...@useless-runes.lsp
M books/kestrel/data/treeset/benchmark/benchmark.lsp
R books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/driver.lsp
R books/kestrel/data/treeset/benchmark/random.lisp
M books/kestrel/data/treeset/cardinality.lisp
M books/kestrel/data/treeset/diff.lisp
M books/kestrel/data/treeset/doc.lisp
M books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/hash.lisp
M books/kestrel/data/treeset/in.lisp
M books/kestrel/data/treeset/insert.lisp
M books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/zip...@useless-runes.lsp
M books/kestrel/data/treeset/internal/bst.lisp
M books/kestrel/data/treeset/internal/count.lisp
M books/kestrel/data/treeset/internal/delete.lisp
M books/kestrel/data/treeset/internal/diff.lisp
M books/kestrel/data/treeset/internal/doc.lisp
M books/kestrel/data/treeset/internal/heap.lisp
M books/kestrel/data/treeset/internal/in-order-defs.lisp
M books/kestrel/data/treeset/internal/in-order.lisp
M books/kestrel/data/treeset/internal/in.lisp
M books/kestrel/data/treeset/internal/intersect.lisp
R books/kestrel/data/treeset/internal/iter-defs.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/join.lisp
M books/kestrel/data/treeset/internal/min-max.lisp
M books/kestrel/data/treeset/internal/subset.lisp
M books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/zipper.lisp
M books/kestrel/data/treeset/iter-defs.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/set.lisp
M books/kestrel/data/treeset/to-oset.lisp
M books/kestrel/data/utilities/.sys/om...@useless-runes.lsp
M books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
M books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
M books/kestrel/data/utilities/fixed-size-words/u32.lisp
M books/kestrel/data/utilities/lists/equiv.lisp
M books/kestrel/data/utilities/oset.lisp
M books/kestrel/fty/deftreeset.lisp
M books/kestrel/fty/fty-treeset.lisp
M books/kestrel/lists-light/update-nth2.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
A books/kestrel/remora/deserialize-from-file.lisp
A books/kestrel/remora/deserializer.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
A books/kestrel/remora/matmul-verification.lisp
M books/kestrel/remora/renaming-evaluation.lisp
A books/kestrel/remora/softmax-verification.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking-tests.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/utilities/lists/len-const-theorems.lisp
M books/std/basic/symbol-lfix.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/with-supporters-doc.lisp
M books/tools/with-supporters-test-top.lisp
M books/tools/with-supporters.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp

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

Commit: 8974a70020b068742b03f25af7ecbf3e8a3823fe
https://github.com/acl2/acl2/commit/8974a70020b068742b03f25af7ecbf3e8a3823fe
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

Changed paths:
M books/kestrel/x86/register-readers-and-writers64.lisp

Log Message:
-----------
[x86] Improve comment.

Commit: 30c72a3333cda178fbb96a90d7eee1e72f7d5588
https://github.com/acl2/acl2/commit/30c72a3333cda178fbb96a90d7eee1e72f7d5588
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

Changed paths:
M books/kestrel/x86/register-readers-and-writers32.lisp

Log Message:
-----------
[x86] Add ESI and EDI.

Also add some rules about them.

Commit: e3820b723e3a668e500c682f393f04dd4a7b0a22
https://github.com/acl2/acl2/commit/e3820b723e3a668e500c682f393f04dd4a7b0a22
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

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

Log Message:
-----------
[axe/x86] Fix/extend rule-lists.

Commit: 9ca76a993e45e706a01bd7f4929401c11613bfdf
https://github.com/acl2/acl2/commit/9ca76a993e45e706a01bd7f4929401c11613bfdf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/unroller-code-only.lisp

Log Message:
-----------
[axe/x86] Improve unroller-code-only.

Commit: e7c2a74b2ecfc052f2cc7befdf825164ae4df626
https://github.com/acl2/acl2/commit/e7c2a74b2ecfc052f2cc7befdf825164ae4df626
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-10 (Mon, 10 Aug 2026)

Changed paths:
M books/kestrel/remora/deserialize-from-file.lisp
A books/kestrel/rust/acl2-customization.lsp
A books/kestrel/rust/cert.acl2
A books/kestrel/rust/editions.lisp
A books/kestrel/rust/mir/abstract-syntax.lisp
A books/kestrel/rust/mir/acl2-customization.lsp
A books/kestrel/rust/mir/cert.acl2
A books/kestrel/rust/mir/tests/cert.acl2
A books/kestrel/rust/mir/tests/factorial.lisp
A books/kestrel/rust/mir/top.lisp
A books/kestrel/rust/mir/types.lisp
A books/kestrel/rust/package.lsp
A books/kestrel/rust/portcullis.acl2
A books/kestrel/rust/portcullis.lisp
A books/kestrel/rust/syntax/acl2-customization.lsp
A books/kestrel/rust/syntax/cert.acl2
A books/kestrel/rust/syntax/extra-grammatical-restrictions.lisp
A books/kestrel/rust/syntax/grammar.lisp
A books/kestrel/rust/syntax/grammar/.gitattributes
A books/kestrel/rust/syntax/grammar/lexical-grammar.abnf
A books/kestrel/rust/syntax/keywords.lisp
A books/kestrel/rust/syntax/lexer.lisp
A books/kestrel/rust/syntax/package.lsp
A books/kestrel/rust/syntax/portcullis.acl2
A books/kestrel/rust/syntax/portcullis.lisp
A books/kestrel/rust/syntax/positions.lisp
A books/kestrel/rust/syntax/spans.lisp
A books/kestrel/rust/syntax/tests/cert.acl2
A books/kestrel/rust/syntax/tests/lexer.lisp
A books/kestrel/rust/syntax/tests/restrictions.lisp
A books/kestrel/rust/syntax/tests/rustc-lexer-vectors.lisp
A books/kestrel/rust/syntax/tests/tokenizer.lisp
A books/kestrel/rust/syntax/token-tree-operations.lisp
A books/kestrel/rust/syntax/token-trees.lisp
A books/kestrel/rust/syntax/tokenizer.lisp
A books/kestrel/rust/syntax/tokens.lisp
A books/kestrel/rust/syntax/top.lisp
A books/kestrel/rust/syntax/unicode-characters.lisp
A books/kestrel/rust/syntax/unicode-xid.lisp
A books/kestrel/rust/tools/generate-unicode-xid.py
A books/kestrel/rust/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/std/util/defirrelevant.lisp

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

Commit: 7623a0ced82e31727640ab433e53a72bffba10bf
https://github.com/acl2/acl2/commit/7623a0ced82e31727640ab433e53a72bffba10bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-11 (Tue, 11 Aug 2026)

Changed paths:
M books/centaur/satlink/top.lisp
M books/emacs/emacs-acl2.el
A books/kestrel/data/deque/acl2-customization.lsp
A books/kestrel/data/deque/cert.acl2
A books/kestrel/data/deque/deque-tests.lisp
A books/kestrel/data/deque/deque.lisp
A books/kestrel/data/deque/package.lsp
A books/kestrel/data/deque/portcullis.acl2
A books/kestrel/data/deque/portcullis.lisp
A books/kestrel/data/deque/top.lisp
M books/kestrel/data/doc.lisp
M books/kestrel/data/top.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/deserializer.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/pseudo-good-worldp.lisp

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

Commit: d2bfd1dc68bd3adf81e4b40c2a740fe4f5ac4402
https://github.com/acl2/acl2/commit/d2bfd1dc68bd3adf81e4b40c2a740fe4f5ac4402
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-11 (Tue, 11 Aug 2026)

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

Log Message:
-----------
[axe/x86] Refactor.

Commit: 3762b6593d294736cbf3b8011bb5efa7523001c8
https://github.com/acl2/acl2/commit/3762b6593d294736cbf3b8011bb5efa7523001c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[axe/x86] Cherrypick just the needed rule sets.

Commit: 40b3ea12814c0c4dff53a1d59ff0be354f258d67
https://github.com/acl2/acl2/commit/40b3ea12814c0c4dff53a1d59ff0be354f258d67
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/arithmetic-5/README
M books/arithmetic-5/lib/basic-ops/arithmetic-theory.lisp
M books/arithmetic-5/lib/basic-ops/basic.lisp
M books/arithmetic-5/lib/basic-ops/building-blocks.lisp
M books/arithmetic-5/lib/basic-ops/collect.lisp
M books/arithmetic-5/lib/basic-ops/common.lisp
M books/arithmetic-5/lib/basic-ops/expt.lisp
A books/arithmetic-5/lib/basic-ops/fuse-power-of-2.lisp
M books/arithmetic-5/lib/basic-ops/normalize.lisp
M books/arithmetic-5/lib/basic-ops/simplify.lisp
M books/arithmetic-5/lib/floor-mod/floor-mod.lisp
M books/doc/relnotes.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/eval-from-file.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/monomorphize-from-file.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/osets.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/utility-transforms.lisp
A books/kestrel/remora/well-formedness-under-desugaring.lisp
M books/kestrel/utilities/translate.lisp

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

Commit: 5803e9e0a91ce017074166182088db4f593b7842
https://github.com/acl2/acl2/commit/5803e9e0a91ce017074166182088db4f593b7842
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
A books/kestrel/remora/unique-names-properties.lisp

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

Commit: 19089ac3afebf7eb3190fac9612461d898bab17c
https://github.com/acl2/acl2/commit/19089ac3afebf7eb3190fac9612461d898bab17c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/unroller-code-only.lisp

Log Message:
-----------
[axe/x86] Improve unroller-code-only.

Cherrypick some rules useful for reasoning about the result of unrolling.

Commit: 268ec0638b66433a35a6c351a21face15e0834d6
https://github.com/acl2/acl2/commit/268ec0638b66433a35a6c351a21face15e0834d6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/add_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/add/rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/and/and_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/cmp/cmp_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/or/or_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sal/sal_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sar/sar_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shl/shl_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_ax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_eax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_mem8_r8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_r8b_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_1.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_cl.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/shr/shr_rax_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/sub/sub_rbx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/support.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp

Log Message:
-----------
[axe/x86] Collect supporting material into new book.

This makes a new book to support all the NDSU assembly proofs. Is is much faster to include than unroller.lisp, via the use of with-supporters. I had to add in various other things to get the proofs to all work. I've also started to remove some unneeded rules in the individual proof files.

Commit: f6e6af20bc98f2b211e8764cd8726a11384b60a1
https://github.com/acl2/acl2/commit/f6e6af20bc98f2b211e8764cd8726a11384b60a1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp

Log Message:
-----------
[axe/x86] Add more rules for 64-bit mode.

These express the 32-bit register accessors in terms of the the 64-bit accessors.

They are based on some rules that NDSU added.

Compare: https://github.com/acl2/acl2/compare/7a31c78f91fc...f6e6af20bc98

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

Eric W. Smith

unread,

Aug 12, 2026, 5:57:11 PM (7 days ago) Aug 12

to acl2-...@googlegroups.com

Branch: refs/heads/master

Eric W. Smith

unread,

Aug 12, 2026, 5:57:42 PM (7 days ago) Aug 12

to acl2-...@googlegroups.com

Branch: refs/heads/testing

Alessandro Coglio

unread,

Aug 12, 2026, 8:53:18 PM (7 days ago) Aug 12

to acl2-...@googlegroups.com

Branch: refs/heads/testing-user-01

Commit: a389e372a9699139a759ea610d67ca5963ad6742
https://github.com/acl2/acl2/commit/a389e372a9699139a759ea610d67ca5963ad6742
Author: Sarah-Scott <sarah....@kestrel.edu>