[acl2/acl2] d3f9df: [C$] Extend formal subset and mapping.

0 views
Skip to first unread message

Alessandro Coglio

unread,
Aug 13, 2026, 11:11:01 AM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: d3f9dfa7a0e7a062e2e4eed29ba29b0576dd53f6
https://github.com/acl2/acl2/commit/d3f9dfa7a0e7a062e2e4eed29ba29b0576dd53f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-08 (Sat, 08 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp

Log Message:
-----------
[C$] Extend formal subset and mapping.

Include parenthesized direct declarators.


Commit: ff992e373fb1da7a2270f2606d68f9bfdfbb81ec
https://github.com/acl2/acl2/commit/ff992e373fb1da7a2270f2606d68f9bfdfbb81ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-08 (Sat, 08 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp

Log Message:
-----------
[C$] Shorten some code.


Commit: cc876673a3df629d85af579fa510ccb1a85764d6
https://github.com/acl2/acl2/commit/cc876673a3df629d85af579fa510ccb1a85764d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-08 (Sat, 08 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

Log Message:
-----------
[C$] Shorten some code.


Commit: 2366d13035535f24c58b01c34efe5cbce38444f9
https://github.com/acl2/acl2/commit/2366d13035535f24c58b01c34efe5cbce38444f9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-09 (Sun, 09 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp

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


Commit: 7fca2b0a80c1cd3f7bd52b34a2afdc35ce96ce7e
https://github.com/acl2/acl2/commit/7fca2b0a80c1cd3f7bd52b34a2afdc35ce96ce7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-11 (Tue, 11 Aug 2026)

Changed paths:
M books/arithmetic-5/README
M books/arithmetic-5/lib/basic-ops/arithmetic-theory.lisp
M books/arithmetic-5/lib/basic-ops/basic.lisp
M books/arithmetic-5/lib/basic-ops/building-blocks.lisp
M books/arithmetic-5/lib/basic-ops/collect.lisp
M books/arithmetic-5/lib/basic-ops/common.lisp
M books/arithmetic-5/lib/basic-ops/expt.lisp
A books/arithmetic-5/lib/basic-ops/fuse-power-of-2.lisp
M books/arithmetic-5/lib/basic-ops/normalize.lisp
M books/arithmetic-5/lib/basic-ops/simplify.lisp
M books/arithmetic-5/lib/floor-mod/floor-mod.lisp
M books/centaur/satlink/top.lisp
M books/doc/relnotes.lisp
M books/emacs/emacs-acl2.el
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bvcat.lisp
A books/kestrel/data/.gitignore
A books/kestrel/data/benchmark/harness.lsp
A books/kestrel/data/deque/acl2-customization.lsp
A books/kestrel/data/deque/cert.acl2
A books/kestrel/data/deque/deque-tests.lisp
A books/kestrel/data/deque/deque.lisp
A books/kestrel/data/deque/package.lsp
A books/kestrel/data/deque/portcullis.acl2
A books/kestrel/data/deque/portcullis.lisp
A books/kestrel/data/deque/top.lisp
M books/kestrel/data/doc.lisp
A books/kestrel/data/hash/.sys/generi...@useless-runes.lsp
M books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/to-byt...@useless-runes.lsp
A books/kestrel/data/hash/.sys/to-b...@useless-runes.lsp
A books/kestrel/data/hash/benchmark/acl2-customization.lsp
A books/kestrel/data/hash/benchmark/benchmark.lsp
A books/kestrel/data/hash/benchmark/driver.lsp
A books/kestrel/data/hash/generic-fold.lisp
M books/kestrel/data/hash/jenkins-defs.lisp
M books/kestrel/data/hash/jenkins.lisp
M books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/to-bytes-defs.lisp
A books/kestrel/data/hash/to-bytes.lisp
M books/kestrel/data/hash/top.lisp
M books/kestrel/data/top.lisp
A books/kestrel/data/treemap/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treemap/benchmark/acl2-customization.lsp
A books/kestrel/data/treemap/benchmark/benchmark.lsp
A books/kestrel/data/treemap/benchmark/driver.lsp
A books/kestrel/data/treemap/generic-count.lisp
A books/kestrel/data/treemap/generic-typed.lisp
A books/kestrel/data/treemap/induction.lisp
M books/kestrel/data/treemap/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/jo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/ke...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/loo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rest...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rlo...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/tr...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/updat...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/upd...@useless-runes.lsp
M books/kestrel/data/treemap/internal/.sys/val...@useless-runes.lsp
M books/kestrel/data/treemap/internal/antisymmetry.lisp
M books/kestrel/data/treemap/internal/bst.lisp
M books/kestrel/data/treemap/internal/count.lisp
M books/kestrel/data/treemap/internal/delete.lisp
M books/kestrel/data/treemap/internal/heap.lisp
M books/kestrel/data/treemap/internal/in-order.lisp
M books/kestrel/data/treemap/internal/join.lisp
M books/kestrel/data/treemap/internal/keys.lisp
M books/kestrel/data/treemap/internal/lookup.lisp
M books/kestrel/data/treemap/internal/min-max.lisp
M books/kestrel/data/treemap/internal/restrict.lisp
M books/kestrel/data/treemap/internal/submap.lisp
M books/kestrel/data/treemap/internal/tree.lisp
M books/kestrel/data/treemap/internal/update.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/map.lisp
M books/kestrel/data/treemap/size.lisp
M books/kestrel/data/treemap/to-omap.lisp
M books/kestrel/data/treemap/top.lisp
M books/kestrel/data/treemap/update.lisp
M books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/data/treeset/benchmark/.sys/ran...@useless-runes.lsp
M books/kestrel/data/treeset/benchmark/benchmark.lsp
R books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/driver.lsp
R books/kestrel/data/treeset/benchmark/random.lisp
M books/kestrel/data/treeset/cardinality.lisp
M books/kestrel/data/treeset/diff.lisp
M books/kestrel/data/treeset/doc.lisp
M books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/hash.lisp
M books/kestrel/data/treeset/in.lisp
M books/kestrel/data/treeset/insert.lisp
M books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/zip...@useless-runes.lsp
M books/kestrel/data/treeset/internal/bst.lisp
M books/kestrel/data/treeset/internal/count.lisp
M books/kestrel/data/treeset/internal/delete.lisp
M books/kestrel/data/treeset/internal/diff.lisp
M books/kestrel/data/treeset/internal/doc.lisp
M books/kestrel/data/treeset/internal/heap.lisp
M books/kestrel/data/treeset/internal/in-order-defs.lisp
M books/kestrel/data/treeset/internal/in-order.lisp
M books/kestrel/data/treeset/internal/in.lisp
M books/kestrel/data/treeset/internal/intersect.lisp
R books/kestrel/data/treeset/internal/iter-defs.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/join.lisp
M books/kestrel/data/treeset/internal/min-max.lisp
M books/kestrel/data/treeset/internal/subset.lisp
M books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/zipper.lisp
M books/kestrel/data/treeset/iter-defs.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/set.lisp
M books/kestrel/data/treeset/to-oset.lisp
M books/kestrel/data/utilities/.sys/om...@useless-runes.lsp
M books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
M books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
M books/kestrel/data/utilities/fixed-size-words/u32.lisp
M books/kestrel/data/utilities/lists/equiv.lisp
M books/kestrel/data/utilities/oset.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/fty/deftreeset.lisp
M books/kestrel/fty/fty-treeset.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
A books/kestrel/remora/deserialize-from-file.lisp
A books/kestrel/remora/deserializer.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
A books/kestrel/rust/acl2-customization.lsp
A books/kestrel/rust/cert.acl2
A books/kestrel/rust/editions.lisp
A books/kestrel/rust/mir/abstract-syntax.lisp
A books/kestrel/rust/mir/acl2-customization.lsp
A books/kestrel/rust/mir/cert.acl2
A books/kestrel/rust/mir/tests/cert.acl2
A books/kestrel/rust/mir/tests/factorial.lisp
A books/kestrel/rust/mir/top.lisp
A books/kestrel/rust/mir/types.lisp
A books/kestrel/rust/package.lsp
A books/kestrel/rust/portcullis.acl2
A books/kestrel/rust/portcullis.lisp
A books/kestrel/rust/syntax/acl2-customization.lsp
A books/kestrel/rust/syntax/cert.acl2
A books/kestrel/rust/syntax/extra-grammatical-restrictions.lisp
A books/kestrel/rust/syntax/grammar.lisp
A books/kestrel/rust/syntax/grammar/.gitattributes
A books/kestrel/rust/syntax/grammar/lexical-grammar.abnf
A books/kestrel/rust/syntax/keywords.lisp
A books/kestrel/rust/syntax/lexer.lisp
A books/kestrel/rust/syntax/package.lsp
A books/kestrel/rust/syntax/portcullis.acl2
A books/kestrel/rust/syntax/portcullis.lisp
A books/kestrel/rust/syntax/positions.lisp
A books/kestrel/rust/syntax/spans.lisp
A books/kestrel/rust/syntax/tests/cert.acl2
A books/kestrel/rust/syntax/tests/lexer.lisp
A books/kestrel/rust/syntax/tests/restrictions.lisp
A books/kestrel/rust/syntax/tests/rustc-lexer-vectors.lisp
A books/kestrel/rust/syntax/tests/tokenizer.lisp
A books/kestrel/rust/syntax/token-tree-operations.lisp
A books/kestrel/rust/syntax/token-trees.lisp
A books/kestrel/rust/syntax/tokenizer.lisp
A books/kestrel/rust/syntax/tokens.lisp
A books/kestrel/rust/syntax/top.lisp
A books/kestrel/rust/syntax/unicode-characters.lisp
A books/kestrel/rust/syntax/unicode-xid.lisp
A books/kestrel/rust/tools/generate-unicode-xid.py
A books/kestrel/rust/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/translate.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/std/util/defirrelevant.lisp
M books/system/pseudo-good-worldp.lisp

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


Commit: e639061861dd193d63eb3bfba6e1daf11382827a
https://github.com/acl2/acl2/commit/e639061861dd193d63eb3bfba6e1daf11382827a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.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/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/eval-from-file.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/monomorphize-from-file.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/osets.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-equivalence.lisp
A books/kestrel/remora/unique-names-properties.lisp
M books/kestrel/remora/utility-transforms.lisp
A books/kestrel/remora/well-formedness-under-desugaring.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp

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


Commit: 12fbae6f9aa60fdeb93daaa9e8197d4d97a90e16
https://github.com/acl2/acl2/commit/12fbae6f9aa60fdeb93daaa9e8197d4d97a90e16
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] Add some theorems.


Commit: fb50977f79528a790b9b4d0d24bc4c7026c6493e
https://github.com/acl2/acl2/commit/fb50977f79528a790b9b4d0d24bc4c7026c6493e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp

Log Message:
-----------
[C$] Add an inversion theorem.


Commit: 90e1544eee2b8a79e95c35ce537e2c4eed0ce5dc
https://github.com/acl2/acl2/commit/90e1544eee2b8a79e95c35ce537e2c4eed0ce5dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] Extend direct mapping to language definition.

Handle parenthesized direct abstract declarators.


Commit: 0fa6ab38fb5791b2083ee2a2bb89fcdac764defe
https://github.com/acl2/acl2/commit/0fa6ab38fb5791b2083ee2a2bb89fcdac764defe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp

Log Message:
-----------
[C$] Add an inversion theorem.


Commit: 4c2a176673490b650372ec8f4e1fe1ba9af7ac58
https://github.com/acl2/acl2/commit/4c2a176673490b650372ec8f4e1fe1ba9af7ac58
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
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

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


Commit: 7608238f42a7f7ff60d59241b0e89b92e9ca9883
https://github.com/acl2/acl2/commit/7608238f42a7f7ff60d59241b0e89b92e9ca9883
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] More consistent names.


Commit: a998ef70c9db9eae1d6c37487d0bedd517370b1e
https://github.com/acl2/acl2/commit/a998ef70c9db9eae1d6c37487d0bedd517370b1e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] Simplify some hints.


Commit: ac1a34b700aae7d15c9f5bfa94e45bf5d62cea30
https://github.com/acl2/acl2/commit/ac1a34b700aae7d15c9f5bfa94e45bf5d62cea30
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] Add a comment.


Commit: 1cafce31b3eed7fa2b939fa6fe56805e40daf8eb
https://github.com/acl2/acl2/commit/1cafce31b3eed7fa2b939fa6fe56805e40daf8eb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp

Log Message:
-----------
[C$] Fix a measure and streamline some proofs.


Commit: d812bb5f411e9e0e6077b88efc9a15a18c03a6c2
https://github.com/acl2/acl2/commit/d812bb5f411e9e0e6077b88efc9a15a18c03a6c2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.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:
-----------
[C$] Improve some names and nomenclature.


Commit: 817659a7a9a3c8666e5db0aac60b66da622e2300
https://github.com/acl2/acl2/commit/817659a7a9a3c8666e5db0aac60b66da622e2300
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-12 (Wed, 12 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp

Log Message:
-----------
[C$] Improve some names and nomenclature.


Compare: https://github.com/acl2/acl2/compare/48f289ce50bc...817659a7a9a3

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

Alessandro Coglio

unread,
Aug 13, 2026, 1:36:43 PM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/master

Alessandro Coglio

unread,
Aug 13, 2026, 1:37:34 PM (6 days ago) Aug 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Aug 14, 2026, 1:31:11 AM (6 days ago) Aug 14
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 2102c707e92b3bfb6aef4bae225a050265876aa7
https://github.com/acl2/acl2/commit/2102c707e92b3bfb6aef4bae225a050265876aa7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[axe/x86] Comment out unneeded rules.
Commit: 51f313743d6bf35578427c39f2033a6a6ec92758
https://github.com/acl2/acl2/commit/51f313743d6bf35578427c39f2033a6a6ec92758
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
M books/kestrel/utilities/if.lisp

Log Message:
-----------
[utilities] Add a rule about IF.


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

Changed paths:
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:
-----------
[x86] Refactor to reduce includes of read-and-write book.


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

Changed paths:
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

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


Commit: 6c629373f294b2061e30f5f0e785e25ffd422529
https://github.com/acl2/acl2/commit/6c629373f294b2061e30f5f0e785e25ffd422529
Author: Eric Smith <ews...@gmail.com>
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: 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/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: fb4962296524ef7c228a0ab106a68189034a4835
https://github.com/acl2/acl2/commit/fb4962296524ef7c228a0ab106a68189034a4835
Author: Eric Smith <ews...@gmail.com>
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

Log Message:
-----------
[arithmetic-light] Add/improve various rules.

Especially to handle negative values better (e.g., in cancellation and linear rules).


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.


Commit: 79546a675a1c9e78f2437f5815ca7c5d619f62f4
https://github.com/acl2/acl2/commit/79546a675a1c9e78f2437f5815ca7c5d619f62f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp

Log Message:
-----------
[C$] Add a theorem.


Commit: 84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
https://github.com/acl2/acl2/commit/84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
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-inverse.lisp

Log Message:
-----------
[C$] Add an inversion theorem.


Commit: 020d8c8fe242163063dcb8b20e9d7c11833b96a3
https://github.com/acl2/acl2/commit/020d8c8fe242163063dcb8b20e9d7c11833b96a3
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

Log Message:
-----------
[C$] Improve some ldm code.

Have explicit cases for the unary operators.


Commit: ccefe290919c013915caf2c73e937edf59dc61cc
https://github.com/acl2/acl2/commit/ccefe290919c013915caf2c73e937edf59dc61cc
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-inverse.lisp

Log Message:
-----------
[C$] Add an inversion theorem.


Commit: 7204362d509cc3d08cf7d97d1b8183fb30a3a837
https://github.com/acl2/acl2/commit/7204362d509cc3d08cf7d97d1b8183fb30a3a837
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

Log Message:
-----------
[C$] Refactor some code.

Use the language definition mapping of the unary operators.


Commit: befc110e40863e518b859112fa848dd3e01faa32
https://github.com/acl2/acl2/commit/befc110e40863e518b859112fa848dd3e01faa32
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-inverse.lisp

Log Message:
-----------
[C$] Add an inversion theorem.


Commit: bd80e3996c27f7a1eecca843937769f1e052da23
https://github.com/acl2/acl2/commit/bd80e3996c27f7a1eecca843937769f1e052da23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs0.lisp
A books/kestrel/c/transformation/tests/struct-type-split/gso.c

Log Message:
-----------
[STS] Add example to study proof generation.


Commit: 0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
https://github.com/acl2/acl2/commit/0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs1.lisp

Log Message:
-----------
[STS] A preliminary proof for the simple example.


Commit: a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
https://github.com/acl2/acl2/commit/a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs2.lisp

Log Message:
-----------
[STS] Start work on more systematic proof approach.


Commit: a37c7d434d65bcaf7e80e1d251c851f0977000a5
https://github.com/acl2/acl2/commit/a37c7d434d65bcaf7e80e1d251c851f0977000a5
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/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
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.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
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
M books/std/util/definductive.lisp

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


Commit: 8261e4b8172a8fc20e597d6045494ce0f54efaaf
https://github.com/acl2/acl2/commit/8261e4b8172a8fc20e597d6045494ce0f54efaaf
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-operations.lisp

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


Compare: https://github.com/acl2/acl2/compare/48f289ce50bc...8261e4b8172a
Reply all
Reply to author
Forward
0 new messages