[acl2/acl2] b70c11: [bv] Split out defs of bvminus and bvuminus.

0 views

Skip to first unread message

Eric W. Smith

unread,

Dec 18, 2025, 1:46:26 PM (3 days ago) Dec 18

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: b70c11957e66c08c529d2095dd539efb4ca95ea3
https://github.com/acl2/acl2/commit/b70c11957e66c08c529d2095dd539efb4ca95ea3
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bvequal-rules.lisp
A books/kestrel/bv/bvminus-def.lisp
M books/kestrel/bv/bvminus.lisp
A books/kestrel/bv/bvuminus-def.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/doc.lisp
M books/kestrel/bv/top.lisp

Log Message:
-----------
[bv] Split out defs of bvminus and bvuminus.

Also add a theory-invariant and update top.lisp.

Commit: 864b41da871bf84cafe78c17c82ab5c94f074b2a
https://github.com/acl2/acl2/commit/864b41da871bf84cafe78c17c82ab5c94f074b2a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/support.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvequal-rules.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/ones-complement.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules5.lisp
M books/kestrel/bv/rules8.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/bv/validation-smt-lib.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp

Log Message:
-----------
[bv] Reduce includes of some BV books.

Commit: bf2a6fbca4c6bbe182545bba78eb1915d99254b4
https://github.com/acl2/acl2/commit/bf2a6fbca4c6bbe182545bba78eb1915d99254b4
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/bv/rules4.lisp
M books/kestrel/crypto/r1cs/sparse/gadgets/range-check.lisp
M books/kestrel/crypto/tea/inversion.lisp

Log Message:
-----------
[bv] Reduce includes.

Commit: 662e5e5589da9fab7c2de114201c55c7321a2df7
https://github.com/acl2/acl2/commit/662e5e5589da9fab7c2de114201c55c7321a2df7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/dowhile.c
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
M books/kestrel/c/transformation/tests/simpadd0/old/if.c
M books/kestrel/c/transformation/tests/simpadd0/old/ifelse.c
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
M books/kestrel/c/transformation/tests/simpadd0/old/logor.c
M books/kestrel/c/transformation/tests/simpadd0/old/ternary_int.c
M books/kestrel/c/transformation/tests/simpadd0/old/while.c
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/parsers/pe-tools.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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

Commit: 99534e417447c2084859631b73c57fe2e3c2b011
https://github.com/acl2/acl2/commit/99534e417447c2084859631b73c57fe2e3c2b011
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/trim-intro-rules.lisp
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tutorial.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp

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

Commit: e214f978986174b0e05599019a3ca06ac5535063
https://github.com/acl2/acl2/commit/e214f978986174b0e05599019a3ca06ac5535063
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

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

Commit: 1c6357e03b3ecda6e5b30b91a4086346a9424989
https://github.com/acl2/acl2/commit/1c6357e03b3ecda6e5b30b91a4086346a9424989
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-15 (Mon, 15 Dec 2025)

Changed paths:
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstraction-mapping.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/code-ensembles.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-lexer.lisp
A books/kestrel/c/syntax/preprocessor-messages.lisp
A books/kestrel/c/syntax/preprocessor-printer.lisp
A books/kestrel/c/syntax/preprocessor-reader.lisp
A books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/storage-specifier-lists.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser.lisp
A books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
A books/kestrel/c/syntax/tests/preprocessor-reader.lisp
R books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/type-specifier-lists.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/fty/fty-set.lisp
M books/kestrel/x86/support-bv.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
M books/projects/apply/semi-concrete-do-inductions-log.txt
A books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/system/apply/loop-scions.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M translate.lisp

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

Commit: d1633856bc4779b05e1d1281c2a4580e92fc638d
https://github.com/acl2/acl2/commit/d1633856bc4779b05e1d1281c2a4580e92fc638d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)

Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/refine-assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/tests/comments.c
A books/kestrel/c/syntax/tests/empty.c
A books/kestrel/c/syntax/tests/null-directive.c
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
A books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/whitespace.c
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp

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

Commit: 993b00b5ec15262273d078606b29a12974e38c30
https://github.com/acl2/acl2/commit/993b00b5ec15262273d078606b29a12974e38c30
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/event-macros/applicability-conditions.lisp

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

Commit: abfcb5743b1f154485d16a2667af5f3bd0c0b1ee
https://github.com/acl2/acl2/commit/abfcb5743b1f154485d16a2667af5f3bd0c0b1ee
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/coi/bags/cons.lisp
M books/kestrel/apt/rename-calls.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/c/atc/doc.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/helpers/linter.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/std/system/make-mv-let-call.lisp
M books/std/testing/assert-bang-stobj.lisp
M books/std/util/defmapping-doc.lisp
M books/workshops/2004/smith-et-al/support/bags/cons.lisp

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

Commit: 731635099bcb673c1eb27d15f281b4365cbf3a1c
https://github.com/acl2/acl2/commit/731635099bcb673c1eb27d15f281b4365cbf3a1c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/kestrel/axe/unguarded-defuns.lisp

Log Message:
-----------
[axe] Improve map-ifix.

Commit: aa93f0dde12cfb7145172ef7eb040dc7f8abb485
https://github.com/acl2/acl2/commit/aa93f0dde12cfb7145172ef7eb040dc7f8abb485
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/kestrel/bv-lists/unsigned-byte-listp.lisp

Log Message:
-----------
[bv-lists] Add a rule.

Commit: b8d541959faa87333a4bf82febc671c4f944ccda
https://github.com/acl2/acl2/commit/b8d541959faa87333a4bf82febc671c4f944ccda
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/kestrel/typed-lists-light/all-natp.lisp

Log Message:
-----------
[typed-lists-light] Add a rule.

Commit: 0df791dc5bdc51300b42d5478a9b2a84d008fb26
https://github.com/acl2/acl2/commit/0df791dc5bdc51300b42d5478a9b2a84d008fb26
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:
M books/kestrel/axe/rules1.lisp
M books/kestrel/bv-lists/width-of-widest-int.lisp

Log Message:
-----------
[bv-lists] Improve width-of-widest-int.

Use integer-listp, which is built-in.

Compare: https://github.com/acl2/acl2/compare/134530620bb1...0df791dc5bdc

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

acl2buildserver

unread,

Dec 18, 2025, 5:41:18 PM (2 days ago) Dec 18

to acl2-...@googlegroups.com

Branch: refs/heads/master

Commit: 3722284dfb8b8e35ad1d21431c0e0ca89ccea0f0
https://github.com/acl2/acl2/commit/3722284dfb8b8e35ad1d21431c0e0ca89ccea0f0
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2025-12-18 (Thu, 18 Dec 2025)

Changed paths:

M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/support.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/unguarded-defuns.lisp

M books/kestrel/bv-lists/unsigned-byte-listp.lisp
M books/kestrel/bv-lists/width-of-widest-int.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvequal-rules.lisp
A books/kestrel/bv/bvminus-def.lisp

M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/bvsx.lisp

A books/kestrel/bv/bvuminus-def.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/doc.lisp

M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/ones-complement.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp

M books/kestrel/bv/rules4.lisp

M books/kestrel/bv/rules5.lisp
M books/kestrel/bv/rules8.lisp
M books/kestrel/bv/sbvdiv-rules.lisp

M books/kestrel/bv/top.lisp

M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/bv/validation-smt-lib.lisp
M books/kestrel/bv/validation-stp.lisp

M books/kestrel/crypto/r1cs/sparse/gadgets/range-check.lisp
M books/kestrel/crypto/tea/inversion.lisp
M books/kestrel/typed-lists-light/all-natp.lisp

M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp

Log Message:
-----------

Merge commit '0df791dc5bdc51300b42d5478a9b2a84d008fb26' into HEAD

Compare: https://github.com/acl2/acl2/compare/bceb17f3d87d...3722284dfb8b

acl2buildserver

unread,

Dec 18, 2025, 5:41:40 PM (2 days ago) Dec 18

to acl2-...@googlegroups.com

Branch: refs/heads/testing

acl2buildserver

unread,

Dec 20, 2025, 11:03:14 AM (15 hours ago) Dec 20

to acl2-...@googlegroups.com

Branch: refs/heads/testing-acl2s

Commit: 14eef2d0c900288b8d73f80f5a56df96e0d04d18
https://github.com/acl2/acl2/commit/14eef2d0c900288b8d73f80f5a56df96e0d04d18

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)

Changed paths:

M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp

Log Message:
-----------
[C$] Fix more typos.

Commit: feee25a277bc64bdc7b3cdf8c3b0890908f4d950
https://github.com/acl2/acl2/commit/feee25a277bc64bdc7b3cdf8c3b0890908f4d950

Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)

Changed paths:

M books/std/system/make-mv-let-call.lisp
M books/std/util/defmapping-doc.lisp

Log Message:
-----------
[Std] Fix more typos.

Commit: aaaf7ba750dc1c87eaef7ed1034bd80a60b7a38b
https://github.com/acl2/acl2/commit/aaaf7ba750dc1c87eaef7ed1034bd80a60b7a38b