[acl2/acl2] b9c490: [X86ISA] Add MMX packed shift instructions.
0 views
Skip to first unread message
Alessandro Coglio
Mar 4, 2026, 12:44:48 AM (yesterday) Mar 4
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
https://github.com/acl2/acl2/commit/b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
[X86ISA] Add MMX packed shift instructions.
Commit: 4f78af8932fda7682f26eef606274897760f8e2e
https://github.com/acl2/acl2/commit/4f78af8932fda7682f26eef606274897760f8e2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add forgotten MMX FP updates.
Commit: 73c11c7416fd42229824a44e3b5b8569b8bd3813
https://github.com/acl2/acl2/commit/73c11c7416fd42229824a44e3b5b8569b8bd3813
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
[X86ISA] Remove unnecessary :ttags.
Remove many unnecessary items in the :ttags arguments given to include-book and certify-book. Some of the remaining ones are only needed when X86ISA_EXEC=t.
Commit: 2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
https://github.com/acl2/acl2/commit/2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Stylistic consistency (in preparation for extensions).
Commit: c322350842e7bb871cd4dc33e6b7d638aa818ed4
https://github.com/acl2/acl2/commit/c322350842e7bb871cd4dc33e6b7d638aa818ed4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
Log Message:
-----------
[X86ISA] Remove empty :ttags args.
Since these include-book events worked with :ttags (), no ttags are actually involved, so we can drop the :ttags arguments.
Commit: 82df564790d683b4a4accf10ab2718e37520bfeb
https://github.com/acl2/acl2/commit/82df564790d683b4a4accf10ab2718e37520bfeb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
[X86ISA] Drop more unneeded :ttags.
Commit: b41dd570710d00598def5354b86927d4d45a6d9a
https://github.com/acl2/acl2/commit/b41dd570710d00598def5354b86927d4d45a6d9a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
[X86ISA] Remove newly empty :ttags args.
Commit: bb9f8e801e60efa43548e5b54e4c22dab7452847
https://github.com/acl2/acl2/commit/bb9f8e801e60efa43548e5b54e4c22dab7452847
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Add PUNPCKLBW/WD/DQ (MMX variants).
Commit: c47df101ef57d6ed449f3247092022921b640f67
https://github.com/acl2/acl2/commit/c47df101ef57d6ed449f3247092022921b640f67
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Add PUNPCKHBW/WD/DQ (MMX variants).
Commit: 6e686a9de6e218f55eea39555b27ba1111e4893c
https://github.com/acl2/acl2/commit/6e686a9de6e218f55eea39555b27ba1111e4893c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/kestrel/axe/x86/rule-lists.acl2
M books/kestrel/axe/x86/tester-rules.acl2
M books/kestrel/axe/x86/x86-rules.acl2
M books/kestrel/x86/assumptions-new.acl2
M books/kestrel/x86/assumptions32.acl2
M books/kestrel/x86/assumptions64.acl2
M books/kestrel/x86/bytes-loadedp.acl2
M books/kestrel/x86/canonical.acl2
M books/kestrel/x86/conditions.acl2
M books/kestrel/x86/floats.acl2
M books/kestrel/x86/if-lowering.acl2
M books/kestrel/x86/linear-memory.acl2
M books/kestrel/x86/memory32.acl2
M books/kestrel/x86/read-and-write.acl2
M books/kestrel/x86/read-and-write2.acl2
M books/kestrel/x86/read-bytes-and-write-bytes.acl2
M books/kestrel/x86/read-over-write-rules.acl2
M books/kestrel/x86/read-over-write-rules32.acl2
M books/kestrel/x86/read-over-write-rules64.acl2
M books/kestrel/x86/register-readers-and-writers32.acl2
M books/kestrel/x86/register-readers-and-writers64.acl2
M books/kestrel/x86/rflags2.acl2
M books/kestrel/x86/run-until-return.acl2
M books/kestrel/x86/run-until-return2.acl2
M books/kestrel/x86/run-until-return3.acl2
M books/kestrel/x86/run-until-return4.acl2
M books/kestrel/x86/support-x86.acl2
M books/kestrel/x86/support.acl2
M books/kestrel/x86/support2.acl2
M books/kestrel/x86/support32.acl2
M books/kestrel/x86/tools/lifter-support.acl2
M books/kestrel/x86/tools/top.acl2
M books/kestrel/x86/tools/unroll-x86-code-old.acl2
M books/kestrel/x86/top.acl2
M books/kestrel/x86/write-over-write-rules.acl2
M books/kestrel/x86/write-over-write-rules32.acl2
M books/kestrel/x86/write-over-write-rules64.acl2
M books/kestrel/x86/zmm.acl2
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
Merge.
Commit: 3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
https://github.com/acl2/acl2/commit/3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/pack.lisp
M books/projects/x86isa/machine/instructions/top.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Put the PACKUSWB instruction into a new file, for the family of PACK*
instructions.
Commit: 8b28e0802ddc57f10a057d8e7a3651d559128f04
https://github.com/acl2/acl2/commit/8b28e0802ddc57f10a057d8e7a3651d559128f04
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
Merge pull request #1910 from acl2/x86isa-ttags
Remove many unneeded ttags from x86isa books
Commit: 4504aa5816fd0e17342528bbd2653c7d57f868cf
https://github.com/acl2/acl2/commit/4504aa5816fd0e17342528bbd2653c7d57f868cf
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
Merge commit '8b28e0802ddc57f10a057d8e7a3651d559128f04' into HEAD
Commit: 6058c11300781c743c50b40560d0cef8142218f7
https://github.com/acl2/acl2/commit/6058c11300781c743c50b40560d0cef8142218f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/fgl-object.lisp
M books/centaur/fgl/fgl-primitive-congruences.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/trace.lisp
M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp
M books/centaur/meta/bindinglist.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
A books/centaur/meta/fnsymlist.lisp
M books/centaur/meta/package.lsp
M books/centaur/meta/pseudo-rewrite-rule.lisp
M books/centaur/meta/subst-vars.lisp
M books/centaur/meta/subst.lisp
M books/centaur/meta/term-vars.lisp
M books/centaur/meta/urewrite.lisp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/clause-processors/ev-theoremp.lisp
M books/clause-processors/induction.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/replace-equalities.lisp
M books/clause-processors/witness-cp.lisp
M books/doc/relnotes.lisp
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
[X86ISA] Merge and resolve conflicts.
Compare: https://github.com/acl2/acl2/compare/c3eee0b1e5fa...6058c1130078
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
https://github.com/acl2/acl2/commit/b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
[X86ISA] Add MMX packed shift instructions.
Commit: 4f78af8932fda7682f26eef606274897760f8e2e
https://github.com/acl2/acl2/commit/4f78af8932fda7682f26eef606274897760f8e2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add forgotten MMX FP updates.
Commit: 73c11c7416fd42229824a44e3b5b8569b8bd3813
https://github.com/acl2/acl2/commit/73c11c7416fd42229824a44e3b5b8569b8bd3813
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
[X86ISA] Remove unnecessary :ttags.
Remove many unnecessary items in the :ttags arguments given to include-book and certify-book. Some of the remaining ones are only needed when X86ISA_EXEC=t.
Commit: 2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
https://github.com/acl2/acl2/commit/2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Stylistic consistency (in preparation for extensions).
Commit: c322350842e7bb871cd4dc33e6b7d638aa818ed4
https://github.com/acl2/acl2/commit/c322350842e7bb871cd4dc33e6b7d638aa818ed4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
Log Message:
-----------
[X86ISA] Remove empty :ttags args.
Since these include-book events worked with :ttags (), no ttags are actually involved, so we can drop the :ttags arguments.
Commit: 82df564790d683b4a4accf10ab2718e37520bfeb
https://github.com/acl2/acl2/commit/82df564790d683b4a4accf10ab2718e37520bfeb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
[X86ISA] Drop more unneeded :ttags.
Commit: b41dd570710d00598def5354b86927d4d45a6d9a
https://github.com/acl2/acl2/commit/b41dd570710d00598def5354b86927d4d45a6d9a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
[X86ISA] Remove newly empty :ttags args.
Commit: bb9f8e801e60efa43548e5b54e4c22dab7452847
https://github.com/acl2/acl2/commit/bb9f8e801e60efa43548e5b54e4c22dab7452847
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Add PUNPCKLBW/WD/DQ (MMX variants).
Commit: c47df101ef57d6ed449f3247092022921b640f67
https://github.com/acl2/acl2/commit/c47df101ef57d6ed449f3247092022921b640f67
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Add PUNPCKHBW/WD/DQ (MMX variants).
Commit: 6e686a9de6e218f55eea39555b27ba1111e4893c
https://github.com/acl2/acl2/commit/6e686a9de6e218f55eea39555b27ba1111e4893c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/kestrel/axe/x86/rule-lists.acl2
M books/kestrel/axe/x86/tester-rules.acl2
M books/kestrel/axe/x86/x86-rules.acl2
M books/kestrel/x86/assumptions-new.acl2
M books/kestrel/x86/assumptions32.acl2
M books/kestrel/x86/assumptions64.acl2
M books/kestrel/x86/bytes-loadedp.acl2
M books/kestrel/x86/canonical.acl2
M books/kestrel/x86/conditions.acl2
M books/kestrel/x86/floats.acl2
M books/kestrel/x86/if-lowering.acl2
M books/kestrel/x86/linear-memory.acl2
M books/kestrel/x86/memory32.acl2
M books/kestrel/x86/read-and-write.acl2
M books/kestrel/x86/read-and-write2.acl2
M books/kestrel/x86/read-bytes-and-write-bytes.acl2
M books/kestrel/x86/read-over-write-rules.acl2
M books/kestrel/x86/read-over-write-rules32.acl2
M books/kestrel/x86/read-over-write-rules64.acl2
M books/kestrel/x86/register-readers-and-writers32.acl2
M books/kestrel/x86/register-readers-and-writers64.acl2
M books/kestrel/x86/rflags2.acl2
M books/kestrel/x86/run-until-return.acl2
M books/kestrel/x86/run-until-return2.acl2
M books/kestrel/x86/run-until-return3.acl2
M books/kestrel/x86/run-until-return4.acl2
M books/kestrel/x86/support-x86.acl2
M books/kestrel/x86/support.acl2
M books/kestrel/x86/support2.acl2
M books/kestrel/x86/support32.acl2
M books/kestrel/x86/tools/lifter-support.acl2
M books/kestrel/x86/tools/top.acl2
M books/kestrel/x86/tools/unroll-x86-code-old.acl2
M books/kestrel/x86/top.acl2
M books/kestrel/x86/write-over-write-rules.acl2
M books/kestrel/x86/write-over-write-rules32.acl2
M books/kestrel/x86/write-over-write-rules64.acl2
M books/kestrel/x86/zmm.acl2
M books/projects/x86isa/machine/syscalls.lisp
Log Message:
-----------
Merge.
Commit: 3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
https://github.com/acl2/acl2/commit/3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/pack.lisp
M books/projects/x86isa/machine/instructions/top.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Put the PACKUSWB instruction into a new file, for the family of PACK*
instructions.
Commit: 8b28e0802ddc57f10a057d8e7a3651d559128f04
https://github.com/acl2/acl2/commit/8b28e0802ddc57f10a057d8e7a3651d559128f04
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
Merge pull request #1910 from acl2/x86isa-ttags
Remove many unneeded ttags from x86isa books
Commit: 4504aa5816fd0e17342528bbd2653c7d57f868cf
https://github.com/acl2/acl2/commit/4504aa5816fd0e17342528bbd2653c7d57f868cf
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
Merge commit '8b28e0802ddc57f10a057d8e7a3651d559128f04' into HEAD
Commit: 6058c11300781c743c50b40560d0cef8142218f7
https://github.com/acl2/acl2/commit/6058c11300781c743c50b40560d0cef8142218f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/fgl-object.lisp
M books/centaur/fgl/fgl-primitive-congruences.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/trace.lisp
M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp
M books/centaur/meta/bindinglist.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
A books/centaur/meta/fnsymlist.lisp
M books/centaur/meta/package.lsp
M books/centaur/meta/pseudo-rewrite-rule.lisp
M books/centaur/meta/subst-vars.lisp
M books/centaur/meta/subst.lisp
M books/centaur/meta/term-vars.lisp
M books/centaur/meta/urewrite.lisp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/clause-processors/ev-theoremp.lisp
M books/clause-processors/induction.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/replace-equalities.lisp
M books/clause-processors/witness-cp.lisp
M books/doc/relnotes.lisp
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp
Log Message:
-----------
[X86ISA] Merge and resolve conflicts.
Compare: https://github.com/acl2/acl2/compare/c3eee0b1e5fa...6058c1130078
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Mar 4, 2026, 2:10:36 AM (23 hours ago) Mar 4
to acl2-...@googlegroups.com
Branch: refs/heads/master
Compare: https://github.com/acl2/acl2/compare/4504aa5816fd...6058c1130078
Home: https://github.com/acl2/acl2
Commit: b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
https://github.com/acl2/acl2/commit/b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
[X86ISA] Add MMX packed shift instructions.
Commit: 4f78af8932fda7682f26eef606274897760f8e2e
https://github.com/acl2/acl2/commit/4f78af8932fda7682f26eef606274897760f8e2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add forgotten MMX FP updates.
Commit: b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
https://github.com/acl2/acl2/commit/b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
[X86ISA] Add MMX packed shift instructions.
Commit: 4f78af8932fda7682f26eef606274897760f8e2e
https://github.com/acl2/acl2/commit/4f78af8932fda7682f26eef606274897760f8e2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add forgotten MMX FP updates.
Commit: 2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
https://github.com/acl2/acl2/commit/2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Stylistic consistency (in preparation for extensions).
https://github.com/acl2/acl2/commit/2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/punpck.lisp
Log Message:
-----------
[X86ISA] Stylistic consistency (in preparation for extensions).
Alessandro Coglio
Mar 4, 2026, 2:11:36 AM (23 hours ago) Mar 4
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages