[acl2/acl2] 9e57df: [Remora] Fix ordering of two operations.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9e57df4acc01d2be52ab859dd8701810cb19384b
https://github.com/acl2/acl2/commit/9e57df4acc01d2be52ab859dd8701810cb19384b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Fix ordering of two operations.


Commit: cfc1cef5d2e3e0886244a7d896466b7a92dafba5
https://github.com/acl2/acl2/commit/cfc1cef5d2e3e0886244a7d896466b7a92dafba5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import a symbol.


Commit: a866edea4c369634da07a16b21c524b11c2480e3
https://github.com/acl2/acl2/commit/a866edea4c369634da07a16b21c524b11c2480e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

Changed paths:
A books/kestrel/remora/dimension-equivalence-rules.lisp
M books/kestrel/remora/static-semantics.lisp

Log Message:
-----------
[Remora] Start some static inference rules.


Commit: 23b4d76f372efedffa16693c1a8bcb3a887e4641
https://github.com/acl2/acl2/commit/23b4d76f372efedffa16693c1a8bcb3a887e4641
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/node-replacement-alist-for-context.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/refined-assumption-alists3.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/rule-lists.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/cert.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_al_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ax_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_eax_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rax_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/not/not_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/acl2-customization.lsp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/cert.acl2
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_bl_8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_al_mem8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_bx_16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ax_mem16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bl_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_bx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_ebx_32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_eax_mem32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_ebx_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_ax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm16.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem16_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_eax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem32_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem64_rax.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_al.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_mem8_imm8.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_mem64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rax_rbx_64.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm32.lisp
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.asm
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.elf64
A books/kestrel/axe/x86/tests/ndsu/assembly/general-purpose/arith-and-logic/xor/xor_rbx_imm8.lisp
M books/kestrel/utilities/if.lisp
R books/misc/records-bsd.lisp

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


Commit: 74399403a4bfc32a80f283e1ea010a1b9d26fb93
https://github.com/acl2/acl2/commit/74399403a4bfc32a80f283e1ea010a1b9d26fb93
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Relax type equivalence.

Scalar (i.e. 0-rank) array types are equivalent to their atom element types.

Thanks to Quan Luu for running the type checker on an example that exposed the
need for this fix.


Commit: 0b7087163b1512d51557cf3e3b36e6679697481c
https://github.com/acl2/acl2/commit/0b7087163b1512d51557cf3e3b36e6679697481c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add and use notion of dimensions of type value.

This was clearly missing, although some code was using already a similar idiom
(which now we can probably factor into a call of the new function.

Now the calculation is used in a place that was incorrectly rejecting the
evaluation of legitimate code.

Thanks to Quan Luu for running the evaluator on an example that exposed this
issue.


Compare: https://github.com/acl2/acl2/compare/87e44cb44085...0b7087163b15

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

[Alessandro Coglio]

Branch: refs/heads/testing