[acl2/acl2] a48f9e: [Remora] Add some theorems.
1 view
Skip to first unread message
Alessandro Coglio
Aug 13, 2026, 8:04:16 PM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: a48f9e4186eea8f12d4e67aaef3bcc9dc7a2e3fc
https://github.com/acl2/acl2/commit/a48f9e4186eea8f12d4e67aaef3bcc9dc7a2e3fc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 612f76265224fe2f1526ca59e8aef2e73dc4824b
https://github.com/acl2/acl2/commit/612f76265224fe2f1526ca59e8aef2e73dc4824b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/axe/imported-symbols.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/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
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
A books/kestrel/c/transformation/tests/struct-type-split/self-ref-checks.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.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/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/remora/unique-names-properties.lisp
M books/kestrel/remora/utility-transforms.lisp
M books/kestrel/utilities/translate.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
Log Message:
-----------
Merge.
Commit: 800b1595cdea57b0d199437c9f521c0965ff6ec6
https://github.com/acl2/acl2/commit/800b1595cdea57b0d199437c9f521c0965ff6ec6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
Merge.
Commit: 3f4b09da377c1cd19ef7e5fc925e7c1f5961db71
https://github.com/acl2/acl2/commit/3f4b09da377c1cd19ef7e5fc925e7c1f5961db71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Enable a theorem.
Commit: a1791df9db431545232280ada6167811a64cfdbb
https://github.com/acl2/acl2/commit/a1791df9db431545232280ada6167811a64cfdbb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
Log Message:
-----------
[Remora] Factor bound variable ops into new file/topic.
Commit: 1c98c0d979d3ffaa43d53482f80ca51dfcb0fc9a
https://github.com/acl2/acl2/commit/1c98c0d979d3ffaa43d53482f80ca51dfcb0fc9a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Put free var ops into new file/topic.
Commit: 5c222a5dcccc4f979ecd92cc581edee8b6450dbd
https://github.com/acl2/acl2/commit/5c222a5dcccc4f979ecd92cc581edee8b6450dbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Rename file/topic for all vars ops.
Commit: 85393add73b74b768836de12c818caef179510a5
https://github.com/acl2/acl2/commit/85393add73b74b768836de12c818caef179510a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add thms about free ispace vars under desugaring.
Commit: 3c9f712a4377bc3b738bd0dab4543e39bd53eab0
https://github.com/acl2/acl2/commit/3c9f712a4377bc3b738bd0dab4543e39bd53eab0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: 7a722acceff55dfeb82dbd720d32bfb8d7a9a3ac
https://github.com/acl2/acl2/commit/7a722acceff55dfeb82dbd720d32bfb8d7a9a3ac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Split theorem into two more general ones.
Commit: c38efdf505e5a6cc63df0a656d610cb0ae43b987
https://github.com/acl2/acl2/commit/c38efdf505e5a6cc63df0a656d610cb0ae43b987
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Improve layout.
Commit: dbf21df0c7eb0b283d755447d926fd2684b722d7
https://github.com/acl2/acl2/commit/dbf21df0c7eb0b283d755447d926fd2684b722d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Split out thms about bound vars and desugaring.
Commit: d9bed9dcc0fd60a76dbdd491cfff93517a0243df
https://github.com/acl2/acl2/commit/d9bed9dcc0fd60a76dbdd491cfff93517a0243df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Stick to 80 columns.
Commit: ebac156d75e417c3ac43922c732cb8daf6743923
https://github.com/acl2/acl2/commit/ebac156d75e417c3ac43922c732cb8daf6743923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[deffold-reduce] Make termination proofs more robust.
Commit: 260c47338dc3365be2bff985ee9c4ba1e896bd49
https://github.com/acl2/acl2/commit/260c47338dc3365be2bff985ee9c4ba1e896bd49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about free type variables.
Commit: 204598e138bde502e48499047fdcf08ce199d4e1
https://github.com/acl2/acl2/commit/204598e138bde502e48499047fdcf08ce199d4e1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Improve some theorem formulation.
Commit: 775806ce26cb22d203dcad929703ac818d18f100
https://github.com/acl2/acl2/commit/775806ce26cb22d203dcad929703ac818d18f100
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Improve formulation of some inference rules.
Commit: 0bc33be13e399a7d0b3bb90b9bc337ec9c004b9e
https://github.com/acl2/acl2/commit/0bc33be13e399a7d0b3bb90b9bc337ec9c004b9e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[deffold-map] Make termination proofs more robust.
Commit: b96d05fddbaecf4ad4197f4a5518340b79b209c3
https://github.com/acl2/acl2/commit/b96d05fddbaecf4ad4197f4a5518340b79b209c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Improve some theorem formulations.
Commit: 4a3ba810ac864bb6219490306c828a972bb21547
https://github.com/acl2/acl2/commit/4a3ba810ac864bb6219490306c828a972bb21547
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: dbac291c3f4bfabc98eba13985c6a9a047cbe5cd
https://github.com/acl2/acl2/commit/dbac291c3f4bfabc98eba13985c6a9a047cbe5cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: cef5485de4016170ff1315c05837c3f9c7e3741d
https://github.com/acl2/acl2/commit/cef5485de4016170ff1315c05837c3f9c7e3741d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: d9db0c901606505ee583c5037857b55735317226
https://github.com/acl2/acl2/commit/d9db0c901606505ee583c5037857b55735317226
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about free expr vars and desugaring.
Commit: 6b917bdce9c59edae2543ad79b013a2e7cf8588e
https://github.com/acl2/acl2/commit/6b917bdce9c59edae2543ad79b013a2e7cf8588e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
Log Message:
-----------
[C2C] Avoid enabling tau.
Now deffold-reduce and deffold-map generate more robust termination proofs.
It was necessary to refresh the useless runes file, because it was causing a
spurious failure.
Commit: 0f1bc2f3492a84a05510cbc69caab9b60369f7d7
https://github.com/acl2/acl2/commit/0f1bc2f3492a84a05510cbc69caab9b60369f7d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Trim some doc.
Commit: bbe930da62abef961345d9625d8c2d48fbe22586
https://github.com/acl2/acl2/commit/bbe930da62abef961345d9625d8c2d48fbe22586
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: f1d37682eb9c2e290676dd007524d62036d33320
https://github.com/acl2/acl2/commit/f1d37682eb9c2e290676dd007524d62036d33320
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Trim some doc.
Commit: 82650c1ca2d1069cab8f949f45bbf94fb0593003
https://github.com/acl2/acl2/commit/82650c1ca2d1069cab8f949f45bbf94fb0593003
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about all vars under desugaring.
Commit: d5bbc4857e1dfe5e9fb97731ad2f3cd394dce9e0
https://github.com/acl2/acl2/commit/d5bbc4857e1dfe5e9fb97731ad2f3cd394dce9e0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated events.
When XDOC is not generated, group things, that otherwise are grouped into
`defsection`s, into (trivial) `encapsulate`s, which is what `defsection` expands
to. Thus there is more uniformity, and we can generate local events (e.g. to
hide theorem hints) uniformly, whether XDOC is generated or not.
Commit: 221490b266d83fa9496b9eff4571f42bd2276dac
https://github.com/acl2/acl2/commit/221490b266d83fa9496b9eff4571f42bd2276dac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Fix collection of all (free and bound) ispace vars.
Some overrides were missing from the `deffold-reduce`.
This bug was discovered by a failure in proving that desugaring preserves all
(free and bound) variables.
Commit: 919ff1f42a248c83e77f9e3e3ef6009a3ecd22af
https://github.com/acl2/acl2/commit/919ff1f42a248c83e77f9e3e3ef6009a3ecd22af
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Add theorems.
Commit: 862f82b9b4ea0294854cfef700b3f3064e6c2337
https://github.com/acl2/acl2/commit/862f82b9b4ea0294854cfef700b3f3064e6c2337
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems that now hold.
After the recent fix to `all-ispace-vars`.
Commit: 976bbdcd4852a755a6ad078e03ecf4d4bd930bfa
https://github.com/acl2/acl2/commit/976bbdcd4852a755a6ad078e03ecf4d4bd930bfa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/utilities/if.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/support-x86.lisp
A books/kestrel/x86/support-x86b.lisp
Log Message:
-----------
Merge.
Commit: 4465a6b2dfeb87f7f1d1a5f0b1cb5dacc07233f6
https://github.com/acl2/acl2/commit/4465a6b2dfeb87f7f1d1a5f0b1cb5dacc07233f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
Merge.
Commit: 5f4f42d0e4b22f6ce2d7a553890acde2a93f19ef
https://github.com/acl2/acl2/commit/5f4f42d0e4b22f6ce2d7a553890acde2a93f19ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/fb4962296524...5f4f42d0e4b2
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: a48f9e4186eea8f12d4e67aaef3bcc9dc7a2e3fc
https://github.com/acl2/acl2/commit/a48f9e4186eea8f12d4e67aaef3bcc9dc7a2e3fc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 612f76265224fe2f1526ca59e8aef2e73dc4824b
https://github.com/acl2/acl2/commit/612f76265224fe2f1526ca59e8aef2e73dc4824b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/axe/imported-symbols.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/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
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
A books/kestrel/c/transformation/tests/struct-type-split/self-ref-checks.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.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/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/remora/unique-names-properties.lisp
M books/kestrel/remora/utility-transforms.lisp
M books/kestrel/utilities/translate.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
Log Message:
-----------
Merge.
Commit: 800b1595cdea57b0d199437c9f521c0965ff6ec6
https://github.com/acl2/acl2/commit/800b1595cdea57b0d199437c9f521c0965ff6ec6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
Merge.
Commit: 3f4b09da377c1cd19ef7e5fc925e7c1f5961db71
https://github.com/acl2/acl2/commit/3f4b09da377c1cd19ef7e5fc925e7c1f5961db71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Enable a theorem.
Commit: a1791df9db431545232280ada6167811a64cfdbb
https://github.com/acl2/acl2/commit/a1791df9db431545232280ada6167811a64cfdbb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
Log Message:
-----------
[Remora] Factor bound variable ops into new file/topic.
Commit: 1c98c0d979d3ffaa43d53482f80ca51dfcb0fc9a
https://github.com/acl2/acl2/commit/1c98c0d979d3ffaa43d53482f80ca51dfcb0fc9a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Put free var ops into new file/topic.
Commit: 5c222a5dcccc4f979ecd92cc581edee8b6450dbd
https://github.com/acl2/acl2/commit/5c222a5dcccc4f979ecd92cc581edee8b6450dbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Rename file/topic for all vars ops.
Commit: 85393add73b74b768836de12c818caef179510a5
https://github.com/acl2/acl2/commit/85393add73b74b768836de12c818caef179510a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add thms about free ispace vars under desugaring.
Commit: 3c9f712a4377bc3b738bd0dab4543e39bd53eab0
https://github.com/acl2/acl2/commit/3c9f712a4377bc3b738bd0dab4543e39bd53eab0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: 7a722acceff55dfeb82dbd720d32bfb8d7a9a3ac
https://github.com/acl2/acl2/commit/7a722acceff55dfeb82dbd720d32bfb8d7a9a3ac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Split theorem into two more general ones.
Commit: c38efdf505e5a6cc63df0a656d610cb0ae43b987
https://github.com/acl2/acl2/commit/c38efdf505e5a6cc63df0a656d610cb0ae43b987
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Improve layout.
Commit: dbf21df0c7eb0b283d755447d926fd2684b722d7
https://github.com/acl2/acl2/commit/dbf21df0c7eb0b283d755447d926fd2684b722d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Split out thms about bound vars and desugaring.
Commit: d9bed9dcc0fd60a76dbdd491cfff93517a0243df
https://github.com/acl2/acl2/commit/d9bed9dcc0fd60a76dbdd491cfff93517a0243df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Stick to 80 columns.
Commit: ebac156d75e417c3ac43922c732cb8daf6743923
https://github.com/acl2/acl2/commit/ebac156d75e417c3ac43922c732cb8daf6743923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[deffold-reduce] Make termination proofs more robust.
Commit: 260c47338dc3365be2bff985ee9c4ba1e896bd49
https://github.com/acl2/acl2/commit/260c47338dc3365be2bff985ee9c4ba1e896bd49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/free-variable-operations.lisp
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about free type variables.
Commit: 204598e138bde502e48499047fdcf08ce199d4e1
https://github.com/acl2/acl2/commit/204598e138bde502e48499047fdcf08ce199d4e1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Improve some theorem formulation.
Commit: 775806ce26cb22d203dcad929703ac818d18f100
https://github.com/acl2/acl2/commit/775806ce26cb22d203dcad929703ac818d18f100
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Improve formulation of some inference rules.
Commit: 0bc33be13e399a7d0b3bb90b9bc337ec9c004b9e
https://github.com/acl2/acl2/commit/0bc33be13e399a7d0b3bb90b9bc337ec9c004b9e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[deffold-map] Make termination proofs more robust.
Commit: b96d05fddbaecf4ad4197f4a5518340b79b209c3
https://github.com/acl2/acl2/commit/b96d05fddbaecf4ad4197f4a5518340b79b209c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Improve some theorem formulations.
Commit: 4a3ba810ac864bb6219490306c828a972bb21547
https://github.com/acl2/acl2/commit/4a3ba810ac864bb6219490306c828a972bb21547
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: dbac291c3f4bfabc98eba13985c6a9a047cbe5cd
https://github.com/acl2/acl2/commit/dbac291c3f4bfabc98eba13985c6a9a047cbe5cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/bound-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: cef5485de4016170ff1315c05837c3f9c7e3741d
https://github.com/acl2/acl2/commit/cef5485de4016170ff1315c05837c3f9c7e3741d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: d9db0c901606505ee583c5037857b55735317226
https://github.com/acl2/acl2/commit/d9db0c901606505ee583c5037857b55735317226
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about free expr vars and desugaring.
Commit: 6b917bdce9c59edae2543ad79b013a2e7cf8588e
https://github.com/acl2/acl2/commit/6b917bdce9c59edae2543ad79b013a2e7cf8588e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
Log Message:
-----------
[C2C] Avoid enabling tau.
Now deffold-reduce and deffold-map generate more robust termination proofs.
It was necessary to refresh the useless runes file, because it was causing a
spurious failure.
Commit: 0f1bc2f3492a84a05510cbc69caab9b60369f7d7
https://github.com/acl2/acl2/commit/0f1bc2f3492a84a05510cbc69caab9b60369f7d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variable-operations.lisp
Log Message:
-----------
[Remora] Trim some doc.
Commit: bbe930da62abef961345d9625d8c2d48fbe22586
https://github.com/acl2/acl2/commit/bbe930da62abef961345d9625d8c2d48fbe22586
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: f1d37682eb9c2e290676dd007524d62036d33320
https://github.com/acl2/acl2/commit/f1d37682eb9c2e290676dd007524d62036d33320
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/free-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Trim some doc.
Commit: 82650c1ca2d1069cab8f949f45bbf94fb0593003
https://github.com/acl2/acl2/commit/82650c1ca2d1069cab8f949f45bbf94fb0593003
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems about all vars under desugaring.
Commit: d5bbc4857e1dfe5e9fb97731ad2f3cd394dce9e0
https://github.com/acl2/acl2/commit/d5bbc4857e1dfe5e9fb97731ad2f3cd394dce9e0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated events.
When XDOC is not generated, group things, that otherwise are grouped into
`defsection`s, into (trivial) `encapsulate`s, which is what `defsection` expands
to. Thus there is more uniformity, and we can generate local events (e.g. to
hide theorem hints) uniformly, whether XDOC is generated or not.
Commit: 221490b266d83fa9496b9eff4571f42bd2276dac
https://github.com/acl2/acl2/commit/221490b266d83fa9496b9eff4571f42bd2276dac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Fix collection of all (free and bound) ispace vars.
Some overrides were missing from the `deffold-reduce`.
This bug was discovered by a failure in proving that desugaring preserves all
(free and bound) variables.
Commit: 919ff1f42a248c83e77f9e3e3ef6009a3ecd22af
https://github.com/acl2/acl2/commit/919ff1f42a248c83e77f9e3e3ef6009a3ecd22af
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variable-operations.lisp
Log Message:
-----------
[Remora] Add theorems.
Commit: 862f82b9b4ea0294854cfef700b3f3064e6c2337
https://github.com/acl2/acl2/commit/862f82b9b4ea0294854cfef700b3f3064e6c2337
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/remora/all-variables-under-desugaring.lisp
Log Message:
-----------
[Remora] Add theorems that now hold.
After the recent fix to `all-ispace-vars`.
Commit: 976bbdcd4852a755a6ad078e03ecf4d4bd930bfa
https://github.com/acl2/acl2/commit/976bbdcd4852a755a6ad078e03ecf4d4bd930bfa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/utilities/if.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/support-x86.lisp
A books/kestrel/x86/support-x86b.lisp
Log Message:
-----------
Merge.
Commit: 4465a6b2dfeb87f7f1d1a5f0b1cb5dacc07233f6
https://github.com/acl2/acl2/commit/4465a6b2dfeb87f7f1d1a5f0b1cb5dacc07233f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
Merge.
Commit: 5f4f42d0e4b22f6ce2d7a553890acde2a93f19ef
https://github.com/acl2/acl2/commit/5f4f42d0e4b22f6ce2d7a553890acde2a93f19ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/fb4962296524...5f4f42d0e4b2
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Aug 13, 2026, 11:06:05 PM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/master
Alessandro Coglio
Aug 13, 2026, 11:06:35 PM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages