[acl2/acl2] d374f8: [x86] Start converting assumptions to be translate...

0 views
Skip to first unread message

Eric W. Smith

unread,
Dec 1, 2025, 11:36:25 PM (6 days ago) Dec 1
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: d374f82c1693fbf2d34a504dec5a890394488699
https://github.com/acl2/acl2/commit/d374f82c1693fbf2d34a504dec5a890394488699
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:
M books/kestrel/x86/assumptions-new.lisp

Log Message:
-----------
[x86] Start converting assumptions to be translated terms.


Commit: be2ec6032f06afe41c049519bdc27e66a66581ed
https://github.com/acl2/acl2/commit/be2ec6032f06afe41c049519bdc27e66a66581ed
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/x86/assumptions-new.lisp

Log Message:
-----------
[x86] Improve assumptions.

Make more of them translated terms.


Commit: fa166ee3d211bac883b5862869d856db9fdb5b66
https://github.com/acl2/acl2/commit/fa166ee3d211bac883b5862869d856db9fdb5b66
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/x86/tools/unroll-x86-code-old.lisp

Log Message:
-----------
[x86] Fix comment typo.


Commit: f0005b5e9a063c2ef01166298638c322a96b2f1f
https://github.com/acl2/acl2/commit/f0005b5e9a063c2ef01166298638c322a96b2f1f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp

Log Message:
-----------
[x86] Move some rarely used code.


Commit: 8c7970ba9d9fb72a10aabdafe546502b4dffe574
https://github.com/acl2/acl2/commit/8c7970ba9d9fb72a10aabdafe546502b4dffe574
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

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

Log Message:
-----------
[axe/x86] Comment out unneeded rule.


Commit: ef01943e4a00a39c70414358bc7188ce10289275
https://github.com/acl2/acl2/commit/ef01943e4a00a39c70414358bc7188ce10289275
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp

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


Commit: ceb487ee389da807f9b43d9ea1a628c26f8106c7
https://github.com/acl2/acl2/commit/ceb487ee389da807f9b43d9ea1a628c26f8106c7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

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


Commit: 207242ceca51f1bd74c5186bb342213d19b7191f
https://github.com/acl2/acl2/commit/207242ceca51f1bd74c5186bb342213d19b7191f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp

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


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

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
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/memory/memory-regions.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp

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


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

Changed paths:
M books/kestrel/x86/assumptions-new.lisp

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


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

Changed paths:
M books/kestrel/axe/x86/tester.lisp

Log Message:
-----------
[axe/x86] Add a rule.


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

Changed paths:
M axioms.lisp
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/movddup.c
A books/kestrel/axe/x86/tests/ndsu/movddup.elf64
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.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-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
M books/kestrel/utilities/er-soft-plus.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/er-soft-logic.lisp
M defthm.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M proof-builder-a.lisp
M rewrite.lisp

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


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

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/928920a2a7ac...170d1b76ed78

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

Eric W. Smith

unread,
Dec 2, 2025, 12:39:15 AM (6 days ago) Dec 2
to acl2-...@googlegroups.com
Branch: refs/heads/master

Eric W. Smith

unread,
Dec 2, 2025, 12:39:41 AM (6 days ago) Dec 2
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Dec 2, 2025, 5:54:23 AM (6 days ago) Dec 2
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 54000b3f72c959d04026c4d189f19f8079d351e2
https://github.com/acl2/acl2/commit/54000b3f72c959d04026c4d189f19f8079d351e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Add and use a theorem.


Commit: 6f8d315c258ac62355e26a0f36150f8930226ce3
https://github.com/acl2/acl2/commit/6f8d315c258ac62355e26a0f36150f8930226ce3
Author: Yusuf Moshood <yusuf....@ndus.edu>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/movddup.c
A books/kestrel/axe/x86/tests/ndsu/movddup.elf64
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp

Log Message:
-----------
Add MOVDDUP tests and update README


Commit: c0e7c1e22281475f62a8b18b151b9184749480a6
https://github.com/acl2/acl2/commit/c0e7c1e22281475f62a8b18b151b9184749480a6
Author: mayuf413 <yusuf....@ndus.edu>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M axioms.lisp
M basis-a.lisp
M bin/make-fancy-manual.sh
M bin/new-useless-runes-files.sh
M books/GNUmakefile
M books/acl2s/.sys/acl2s...@useless-runes.lsp
M books/acl2s/.sys/base-ar...@useless-runes.lsp
M books/acl2s/.sys/base-...@useless-runes.lsp
M books/acl2s/.sys/defdata...@useless-runes.lsp
M books/acl2s/.sys/defunc-...@useless-runes.lsp
M books/acl2s/.sys/ma...@useless-runes.lsp
M books/acl2s/ccg/ccg.lisp
A books/acl2s/interface/.sys/portc...@useless-runes.lsp
A books/acl2s/interface/.sys/t...@useless-runes.lsp
A books/acl2s/interface/acl2s-utils/.sys/portc...@useless-runes.lsp
A books/acl2s/interface/acl2s-utils/.sys/t...@useless-runes.lsp
M books/acl2s/match.lisp
A books/acl2s/sorting/.sys/ms...@useless-runes.lsp
M books/acl2s/sorting/.sys/sor...@useless-runes.lsp
M books/acl2s/top.lisp
M books/build/doc.lisp
M books/build/universal-dependency.certdep
M books/centaur/acre/.sys/ma...@useless-runes.lsp
M books/centaur/acre/.sys/te...@useless-runes.lsp
M books/centaur/acre/.sys/ty...@useless-runes.lsp
M books/centaur/aig/.sys/g-aig...@useless-runes.lsp
M books/centaur/aig/.sys/rando...@useless-runes.lsp
M books/centaur/aig/g-aig-eval.lisp
M books/centaur/aignet/.sys/aignet...@useless-runes.lsp
M books/centaur/aignet/.sys/arr...@useless-runes.lsp
M books/centaur/aignet/.sys/axi-red...@useless-runes.lsp
M books/centaur/aignet/.sys/constr...@useless-runes.lsp
M books/centaur/aignet/.sys/cu...@useless-runes.lsp
M books/centaur/aignet/.sys/equiv-...@useless-runes.lsp
M books/centaur/aignet/.sys/fr...@useless-runes.lsp
M books/centaur/aignet/.sys/internal-obser...@useless-runes.lsp
M books/centaur/aignet/.sys/internal-ob...@useless-runes.lsp
M books/centaur/aignet/.sys/mark-...@useless-runes.lsp
M books/centaur/aignet/.sys/trans...@useless-runes.lsp
M books/centaur/aignet/.sys/unreach...@useless-runes.lsp
M books/centaur/aignet/.sys/vec...@useless-runes.lsp
M books/centaur/bitops/.sys/fast-...@useless-runes.lsp
M books/centaur/bitops/.sys/fast-par...@useless-runes.lsp
M books/centaur/bitops/.sys/fast-...@useless-runes.lsp
M books/centaur/bitops/.sys/ihsext...@useless-runes.lsp
M books/centaur/bitops/.sys/limited...@useless-runes.lsp
M books/centaur/bitops/.sys/logsa...@useless-runes.lsp
A books/centaur/bitops/.sys/ratbit...@useless-runes.lsp
M books/centaur/bitops/.sys/rational...@useless-runes.lsp
M books/centaur/bitops/.sys/satu...@useless-runes.lsp
M books/centaur/bitops/.sys/signed...@useless-runes.lsp
M books/centaur/bitops/.sys/spar...@useless-runes.lsp
M books/centaur/bitops/.sys/trailing...@useless-runes.lsp
M books/centaur/bitops/.sys/width-f...@useless-runes.lsp
M books/centaur/bitops/congruences.lisp
M books/centaur/bitops/ihsext-basics.lisp
M books/centaur/bitops/limited-shifts.lisp
M books/centaur/bitops/package.lsp
M books/centaur/bitops/rational-exponent.lisp
M books/centaur/bitops/trailing-0-count.lisp
A books/centaur/bridge/python/.gitignore
A books/centaur/bridge/python/README
A books/centaur/bridge/python/acl2_bridge.py
A books/centaur/bridge/python/async_demo.py
A books/centaur/bridge/python/demo.lsp
A books/centaur/bridge/python/demo.py
A books/centaur/bridge/python/export_README_to_HTML
M books/centaur/bridge/top.lisp
M books/centaur/esim/tests/.sys/com...@useless-runes.lsp
M books/centaur/esim/tutorial/.sys/booth-...@useless-runes.lsp
M books/centaur/esim/tutorial/.sys/boot...@useless-runes.lsp
M books/centaur/esim/tutorial/.sys/in...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/emod...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/preli...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/t...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/zdri...@useless-runes.lsp
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/arith-base.lisp
M books/centaur/fgl/arith-lemmas.lisp
M books/centaur/fgl/backtrace.lisp
M books/centaur/fgl/bfr-arithmetic.lisp
M books/centaur/fgl/bfr.lisp
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/bitops.lisp
M books/centaur/fgl/bvar-db-bfrlist.lisp
M books/centaur/fgl/bvar-db-equivs.lisp
M books/centaur/fgl/casesplit.lisp
M books/centaur/fgl/cgraph.lisp
M books/centaur/fgl/clauseproc.lisp
M books/centaur/fgl/config.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/constraint-inst.lisp
M books/centaur/fgl/ctrex-utils.lisp
M books/centaur/fgl/debug-utils.lisp
M books/centaur/fgl/def-fgl-rewrite.lisp
M books/centaur/fgl/doc.lisp
M books/centaur/fgl/fancy-ev.lisp
M books/centaur/fgl/fty.lisp
M books/centaur/fgl/helper-utils.lisp
M books/centaur/fgl/interp-st-bfrs-ok.lisp
M books/centaur/fgl/interp-st.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/ipasir-sat.lisp
M books/centaur/fgl/logicman.lisp
M books/centaur/fgl/pathcond-aignet.lisp
M books/centaur/fgl/pathcond-base.lisp
M books/centaur/fgl/pathcond.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/fgl/sat-binder.lisp
R books/centaur/fgl/satlink-sat-config.lisp
M books/centaur/fgl/satlink-sat.lisp
A books/centaur/fgl/stack-bfrs-ok.lisp
M books/centaur/fgl/stack-logic.lisp
A books/centaur/fgl/supertrace.lisp
M books/centaur/fgl/symbolic-arithmetic.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/top.lisp
M books/centaur/fgl/trace.lisp
M books/centaur/fty/.sys/base...@useless-runes.lsp
M books/centaur/fty/.sys/bitstruc...@useless-runes.lsp
M books/centaur/fty/.sys/data...@useless-runes.lsp
A books/centaur/fty/.sys/mult...@useless-runes.lsp
M books/centaur/fty/database.lisp
M books/centaur/fty/deftypes.lisp
M books/centaur/fty/fty-sugar.lisp
M books/centaur/fty/fty-sum.lisp
M books/centaur/fty/fty-transsum.lisp
M books/centaur/fty/tests/.sys/bits...@useless-runes.lsp
M books/centaur/fty/tests/.sys/defpro...@useless-runes.lsp
M books/centaur/fty/tests/.sys/d...@useless-runes.lsp
A books/centaur/fty/tests/.sys/mult...@useless-runes.lsp
M books/centaur/fty/tests/.sys/te...@useless-runes.lsp
M books/centaur/fty/tests/.sys/vis...@useless-runes.lsp
M books/centaur/fty/top.lisp
M books/centaur/fty/visitor.lisp
M books/centaur/gl/.sys/always-e...@useless-runes.lsp
M books/centaur/gl/.sys/arith-...@useless-runes.lsp
M books/centaur/gl/.sys/constrain...@useless-runes.lsp
M books/centaur/gl/.sys/ctrex...@useless-runes.lsp
M books/centaur/gl/.sys/g-alway...@useless-runes.lsp
M books/centaur/gl/.sys/g-...@useless-runes.lsp
M books/centaur/gl/.sys/g-as...@useless-runes.lsp
M books/centaur/gl/.sys/g-bin...@useless-runes.lsp
M books/centaur/gl/.sys/g-bina...@useless-runes.lsp
M books/centaur/gl/.sys/g-co...@useless-runes.lsp
M books/centaur/gl/.sys/g-conc...@useless-runes.lsp
M books/centaur/gl/.sys/g-c...@useless-runes.lsp
M books/centaur/gl/.sys/g-e...@useless-runes.lsp
M books/centaur/gl/.sys/g-h...@useless-runes.lsp
M books/centaur/gl/.sys/g-...@useless-runes.lsp
M books/centaur/gl/.sys/g-intege...@useless-runes.lsp
M books/centaur/gl/.sys/g-les...@useless-runes.lsp
M books/centaur/gl/.sys/g-lo...@useless-runes.lsp
M books/centaur/gl/.sys/g-lo...@useless-runes.lsp
M books/centaur/gl/.sys/g-lo...@useless-runes.lsp
M books/centaur/gl/.sys/g-make-f...@useless-runes.lsp
M books/centaur/gl/.sys/g-pred...@useless-runes.lsp
M books/centaur/gl/.sys/g-tru...@useless-runes.lsp
M books/centaur/gl/.sys/g-un...@useless-runes.lsp
M books/centaur/gl/.sys/g-unary-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-gener...@useless-runes.lsp
M books/centaur/gl/.sys/gl-t...@useless-runes.lsp
M books/centaur/gl/.sys/g...@useless-runes.lsp
M books/centaur/gl/.sys/gte...@useless-runes.lsp
M books/centaur/gl/.sys/hyp...@useless-runes.lsp
M books/centaur/gl/.sys/ite-...@useless-runes.lsp
M books/centaur/gl/.sys/run-gi...@useless-runes.lsp
M books/centaur/gl/always-equal-prep.lisp
M books/centaur/gl/arith-lemmas.lisp
M books/centaur/gl/def-gl-clause-proc.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-templates.lisp
M books/centaur/gl/gtests.lisp
M books/centaur/gl/hyp-fix.lisp
M books/centaur/gl/ite-merge.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/gl/symbolic-arithmetic.lisp
M books/centaur/glmc/.sys/bfr-m...@useless-runes.lsp
M books/centaur/glmc/.sys/glmc-gen...@useless-runes.lsp
M books/centaur/glmc/.sys/glmc-gene...@useless-runes.lsp
M books/centaur/glmc/.sys/gl...@useless-runes.lsp
M books/centaur/glmc/.sys/shape-sp...@useless-runes.lsp
M books/centaur/glmc/glmc-generic-defs.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc-templates.lisp
M books/centaur/meta/.sys/bindi...@useless-runes.lsp
M books/centaur/meta/.sys/congr...@useless-runes.lsp
A books/centaur/meta/.sys/let...@useless-runes.lsp
M books/centaur/meta/.sys/parse-...@useless-runes.lsp
M books/centaur/meta/.sys/su...@useless-runes.lsp
M books/centaur/misc/.sys/bound-r...@useless-runes.lsp
M books/centaur/misc/.sys/grap...@useless-runes.lsp
M books/centaur/misc/.sys/osets-wi...@useless-runes.lsp
A books/centaur/misc/dfs-seen-property.lisp
M books/centaur/misc/tarjan.lisp
M books/centaur/satlink/.sys/li...@useless-runes.lsp
M books/centaur/sv/mods/.sys/l...@useless-runes.lsp
M books/centaur/sv/mods/.sys/mo...@useless-runes.lsp
M books/centaur/sv/mods/.sys/norm-n...@useless-runes.lsp
M books/centaur/sv/mods/.sys/svm...@useless-runes.lsp
M books/centaur/sv/svex/.sys/4vec...@useless-runes.lsp
M books/centaur/sv/svex/.sys/4v...@useless-runes.lsp
M books/centaur/sv/svex/.sys/4vm...@useless-runes.lsp
M books/centaur/sv/svex/.sys/a4ve...@useless-runes.lsp
M books/centaur/sv/svex/.sys/a4...@useless-runes.lsp
M books/centaur/sv/svex/.sys/argm...@useless-runes.lsp
M books/centaur/sv/svex/.sys/contex...@useless-runes.lsp
M books/centaur/sv/svex/.sys/fixpoi...@useless-runes.lsp
M books/centaur/sv/svex/.sys/lat...@useless-runes.lsp
M books/centaur/sv/svex/.sys/li...@useless-runes.lsp
M books/centaur/sv/svex/.sys/overrid...@useless-runes.lsp
M books/centaur/sv/svex/.sys/over...@useless-runes.lsp
M books/centaur/sv/svex/.sys/rewrit...@useless-runes.lsp
M books/centaur/sv/svex/.sys/rsh-c...@useless-runes.lsp
M books/centaur/sv/svex/.sys/s4...@useless-runes.lsp
M books/centaur/sv/svex/.sys/scc-c...@useless-runes.lsp
M books/centaur/sv/svex/.sys/svex-env-...@useless-runes.lsp
M books/centaur/sv/svex/.sys/sv...@useless-runes.lsp
M books/centaur/sv/svex/.sys/symb...@useless-runes.lsp
M books/centaur/sv/svex/.sys/wi...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/chase...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/cycle...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/desig...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/overrid...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/prepr...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/stru...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-fs...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-ge...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-to-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/v...@useless-runes.lsp
M books/centaur/sv/tutorial/.sys/booth-...@useless-runes.lsp
M books/centaur/sv/vl/.sys/ex...@useless-runes.lsp
M books/centaur/sv/vl/.sys/mo...@useless-runes.lsp
M books/centaur/sv/vl/.sys/svstmt-...@useless-runes.lsp
M books/centaur/sv/vl/.sys/svs...@useless-runes.lsp
M books/centaur/sv/vl/.sys/tr...@useless-runes.lsp
M books/centaur/sv/vl/.sys/use...@useless-runes.lsp
M books/centaur/svl/.sys/4vec-...@useless-runes.lsp
M books/centaur/svl/.sys/type...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/ba...@useless-runes.lsp
M books/centaur/svl/svexl/.sys/sv...@useless-runes.lsp
M books/centaur/truth/.sys/dsd4-...@useless-runes.lsp
M books/centaur/truth/.sys/pe...@useless-runes.lsp
M books/centaur/truth/.sys/si...@useless-runes.lsp
M books/centaur/vl/.sys/ex...@useless-runes.lsp
M books/centaur/vl/.sys/pars...@useless-runes.lsp
M books/centaur/vl/.sys/simpc...@useless-runes.lsp
M books/centaur/vl/kit/.sys/li...@useless-runes.lsp
M books/centaur/vl/lint/.sys/lu...@useless-runes.lsp
M books/centaur/vl/lint/.sys/odd...@useless-runes.lsp
M books/centaur/vl/lint/.sys/selfa...@useless-runes.lsp
M books/centaur/vl/lint/.sys/skip-...@useless-runes.lsp
M books/centaur/vl/lint/.sys/typo-...@useless-runes.lsp
M books/centaur/vl/loader/.sys/descri...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/block...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/cloc...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/d...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/elem...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/even...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/expre...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/func...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/ga...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/in...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/ne...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/pack...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/param...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/po...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/state...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/t...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/ud...@useless-runes.lsp
M books/centaur/vl/loader/preprocessor/.sys/def...@useless-runes.lsp
M books/centaur/vl/loader/preprocessor/.sys/t...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/core...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/ctxe...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/datatyp...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/elab...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/expr-...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/hid-...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/repor...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/scope...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/stmt-...@useless-runes.lsp
M books/centaur/vl/server/.sys/file-...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/bi...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/shado...@useless-runes.lsp
M books/centaur/vl/transforms/unparam/.sys/expr-c...@useless-runes.lsp
M books/centaur/vl/transforms/unparam/.sys/lin...@useless-runes.lsp
M books/centaur/vl/transforms/unparam/.sys/t...@useless-runes.lsp
M books/centaur/vl/util/.sys/bi...@useless-runes.lsp
M books/centaur/vl/util/.sys/de...@useless-runes.lsp
M books/centaur/vl/util/.sys/ech...@useless-runes.lsp
M books/centaur/vl/util/.sys/loca...@useless-runes.lsp
M books/centaur/vl/util/.sys/os...@useless-runes.lsp
M books/centaur/vl/util/.sys/pr...@useless-runes.lsp
M books/centaur/vl/util/.sys/summari...@useless-runes.lsp
M books/centaur/vl/util/.sys/warn...@useless-runes.lsp
M books/centaur/vl2014/.sys/ex...@useless-runes.lsp
M books/centaur/vl2014/.sys/pars...@useless-runes.lsp
M books/centaur/vl2014/.sys/wf-reas...@useless-runes.lsp
M books/centaur/vl2014/kit/.sys/li...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/check-n...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/lu...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/selfa...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/typo-...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/use...@useless-runes.lsp
M books/centaur/vl2014/loader/.sys/descri...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/block...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/elem...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/expre...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/func...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/par...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/state...@useless-runes.lsp
M books/centaur/vl2014/loader/preprocessor/.sys/def...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/cons...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/core...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/hid-...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/modnam...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/port-...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/repor...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/scope...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/expand-f...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/expr...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/combin...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/edge...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/latc...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/stmtr...@useless-runes.lsp
M books/centaur/vl2014/transforms/annotate/.sys/shado...@useless-runes.lsp
M books/centaur/vl2014/transforms/unparam/.sys/lin...@useless-runes.lsp
M books/centaur/vl2014/transforms/unparam/.sys/over...@useless-runes.lsp
M books/centaur/vl2014/transforms/unparam/.sys/t...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/bi...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/ech...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/os...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/pr...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/print...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/warn...@useless-runes.lsp
M books/clause-processors/.sys/meta-extract...@useless-runes.lsp
M books/clause-processors/SULFA/books/sat-tests/benchmark.lisp
A books/clause-processors/SULFA/books/sat/.sys/sulfa-d...@useless-runes.lsp
M books/clause-processors/SULFA/books/sat/sat-setup.lisp
M books/clause-processors/basic-examples.lisp
M books/clause-processors/meta-extract-user.lisp
M books/coi/osets/.sys/list...@useless-runes.lsp
M books/coi/osets/.sys/ou...@useless-runes.lsp
M books/coi/super-ihs/.sys/bit-twiddl...@useless-runes.lsp
M books/coi/super-ihs/.sys/log...@useless-runes.lsp
M books/coi/super-ihs/.sys/supe...@useless-runes.lsp
M books/coi/types/.sys/type...@useless-runes.lsp
M books/coi/types/.sys/type...@useless-runes.lsp
A books/demos/.sys/divp-by...@useless-runes.lsp
A books/demos/.sys/majori...@useless-runes.lsp
M books/demos/.sys/ppr1-exp...@useless-runes.lsp
M books/demos/.sys/stobj-tabl...@useless-runes.lsp
A books/demos/.sys/toy-...@useless-runes.lsp
A books/demos/attach-stobj/.sys/demo...@useless-runes.lsp
A books/demos/attach-stobj/.sys/lo...@useless-runes.lsp
A books/demos/attach-stobj/.sys/mem-...@useless-runes.lsp
A books/demos/attach-stobj/.sys/m...@useless-runes.lsp
A books/demos/attach-stobj/.sys/mem...@useless-runes.lsp
A books/demos/attach-stobj/.sys/nes...@useless-runes.lsp
M books/demos/defabsstobj-example-1.lisp
A books/demos/fp/.sys/f...@useless-runes.lsp
M books/demos/geneqv-test-log.txt
M books/demos/gl-and-std/.sys/defaggregat...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defaggrega...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defprod-...@useless-runes.lsp
M books/demos/marktoberdorf-08/lecture4-log.txt
M books/demos/meta-wf-guarantee-example.lisp
A books/doc/.sys/public...@useless-runes.lsp
M books/doc/.sys/t...@useless-runes.lsp
M books/doc/100-theorems.lisp
M books/doc/practices.lisp
M books/doc/publications.lisp
M books/doc/relnotes.lisp
M books/doc/top-topic.lisp
M books/emacs/acl2-doc-open-url.el
M books/emacs/acl2-doc.el
M books/emacs/emacs-acl2.el
M books/emacs/fancy-string-syntax.el
M books/emacs/html-to-xdoc.el
M books/emacs/monitor.el
M books/hints/.sys/basic...@useless-runes.lsp
M books/hints/huet-lang-algorithm.lisp
M books/hints/use-pkg.lisp
M books/ihs/.sys/basic-de...@useless-runes.lsp
M books/ihs/.sys/logops...@useless-runes.lsp
M books/ihs/basic-definitions.lisp
M books/ihs/cert.acl2
M books/ihs/ihs-init.acl2
M books/intel/assume-to-sva/.sys/assume-to-sv...@useless-runes.lsp
M books/intel/assume-to-sva/.sys/assume...@useless-runes.lsp
A books/intel/ifp/.sys/add-...@useless-runes.lsp
A books/intel/ifp/.sys/div-...@useless-runes.lsp
A books/intel/ifp/.sys/fast-...@useless-runes.lsp
A books/intel/ifp/.sys/fma-...@useless-runes.lsp
A books/intel/ifp/.sys/fp-c...@useless-runes.lsp
A books/intel/ifp/.sys/portc...@useless-runes.lsp
A books/intel/ifp/.sys/post...@useless-runes.lsp
A books/intel/ifp/.sys/round...@useless-runes.lsp
A books/intel/ifp/.sys/round-m...@useless-runes.lsp
A books/intel/ifp/.sys/round-t...@useless-runes.lsp
A books/intel/ifp/.sys/sqrt...@useless-runes.lsp
M books/intel/ifp/cert.acl2
M books/intel/svtv-to-sva/.sys/svtv-to-...@useless-runes.lsp
M books/intel/svtv-to-sva/.sys/svtv-to-...@useless-runes.lsp
M books/interface/emacs/acl2-indent.el
M books/kestrel/.sys/top...@useless-runes.lsp
M books/kestrel/.sys/t...@useless-runes.lsp
M books/kestrel/README.md
M books/kestrel/acl2-arrays/.sys/aref1...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/comp...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
M books/kestrel/acl2data/gather/tests/expected/test2__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test2a__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test2b__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test3__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test3a__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test4__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test5__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test6__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test7a__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test7b__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test8__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test9__acl2data.out.saved
M books/kestrel/acl2data/gather/tests/expected/test__acl2data.out.saved
M books/kestrel/acl2pl/.sys/evaluati...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/pack...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/translat...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/val...@useless-runes.lsp
M books/kestrel/alists-light/.sys/acons-...@useless-runes.lsp
M books/kestrel/alists-light/.sys/alists-...@useless-runes.lsp
M books/kestrel/alists-light/.sys/assoc...@useless-runes.lsp
M books/kestrel/alists-light/.sys/lookup...@useless-runes.lsp
M books/kestrel/alists-light/.sys/lookup-...@useless-runes.lsp
M books/kestrel/alists-light/.sys/map-look...@useless-runes.lsp
M books/kestrel/alists-light/.sys/strip...@useless-runes.lsp
M books/kestrel/alists-light/.sys/uniquify...@useless-runes.lsp
M books/kestrel/alists-light/alistp.lisp
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/apt/.sys/isodat...@useless-runes.lsp
M books/kestrel/apt/.sys/iso...@useless-runes.lsp
M books/kestrel/apt/.sys/propag...@useless-runes.lsp
M books/kestrel/apt/README.md
M books/kestrel/apt/isodata-doc.lisp
M books/kestrel/apt/isodata.lisp
M books/kestrel/apt/schemalg-doc.lisp
M books/kestrel/apt/utilities/.sys/na...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/a...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/a...@useless-runes.lsp
A books/kestrel/arithmetic-light/.sys/ceiling-...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ceilin...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/cei...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ex...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ex...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/floor-a...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/floor-m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/flo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/if...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/integer...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/integer...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/inte...@useless-runes.lsp
A books/kestrel/arithmetic-light/.sys/lg-...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/l...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/lo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/mo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/na...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/nonnegative-in...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/pl...@useless-runes.lsp
A books/kestrel/arithmetic-light/.sys/power-o...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/power...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ti...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/trun...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ty...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/unguarded...@useless-runes.lsp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/arithmetic-light/ceiling-of-lg-def.lisp
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/ceiling.lisp
M books/kestrel/arithmetic-light/expt.lisp
M books/kestrel/arithmetic-light/floor.lisp
M books/kestrel/arithmetic-light/ifix.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/arithmetic-light/mod2.lisp
M books/kestrel/arithmetic-light/plus.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/types.lisp
A books/kestrel/arm/README.md
A books/kestrel/arm/acl2-customization.lsp
A books/kestrel/arm/arm32.lisp
A books/kestrel/arm/decoder-tests.lisp
A books/kestrel/arm/decoder.lisp
A books/kestrel/arm/memory.lisp
A books/kestrel/arm/package.lsp
A books/kestrel/arm/portcullis.acl2
A books/kestrel/arm/portcullis.lisp
A books/kestrel/arm/pseudocode.lisp
A books/kestrel/arm/state.lisp
M books/kestrel/arrays-2d/.sys/arra...@useless-runes.lsp
M books/kestrel/arrays-2d/.sys/bv-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/add-and-nor...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-t...@useless-runes.lsp
M books/kestrel/axe/.sys/alist-suitab...@useless-runes.lsp
M books/kestrel/axe/.sys/arithmetic...@useless-runes.lsp
M books/kestrel/axe/.sys/assumpti...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-bind-free-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-bind-free...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-fun...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-s...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-tr...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/basic...@useless-runes.lsp
M books/kestrel/axe/.sys/bitops...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-d...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-intr...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-list-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/call-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-decre...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-incre...@useless-runes.lsp
M books/kestrel/axe/.sys/concretize-w...@useless-runes.lsp
M books/kestrel/axe/.sys/conjoin-te...@useless-runes.lsp
M books/kestrel/axe/.sys/conjunctions-a...@useless-runes.lsp
M books/kestrel/axe/.sys/consec...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
A books/kestrel/axe/.sys/convert-to-...@useless-runes.lsp
A books/kestrel/axe/.sys/count-b...@useless-runes.lsp
M books/kestrel/axe/.sys/count-...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
A books/kestrel/axe/.sys/dag-or-term-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-parent-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-si...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-to-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-t...@useless-runes.lsp
A books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/darg-...@useless-runes.lsp
M books/kestrel/axe/.sys/darg-...@useless-runes.lsp
M books/kestrel/axe/.sys/dargp-l...@useless-runes.lsp
M books/kestrel/axe/.sys/def-sim...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-a...@useless-runes.lsp
M books/kestrel/axe/.sys/defth...@useless-runes.lsp
M books/kestrel/axe/.sys/depth...@useless-runes.lsp
M books/kestrel/axe/.sys/el...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-a...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalen...@useless-runes.lsp
M books/kestrel/axe/.sys/equival...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluat...@useless-runes.lsp
M books/kestrel/axe/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/.sys/extract-...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-prob...@useless-runes.lsp
M books/kestrel/axe/.sys/fixup-...@useless-runes.lsp
M books/kestrel/axe/.sys/get-args...@useless-runes.lsp
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/.sys/grou...@useless-runes.lsp
M books/kestrel/axe/.sys/hit-c...@useless-runes.lsp
A books/kestrel/axe/.sys/identical...@useless-runes.lsp
M books/kestrel/axe/.sys/if-r...@useless-runes.lsp
M books/kestrel/axe/.sys/instantiat...@useless-runes.lsp
M books/kestrel/axe/.sys/instant...@useless-runes.lsp
M books/kestrel/axe/.sys/interpreted-f...@useless-runes.lsp
M books/kestrel/axe/.sys/keep-node...@useless-runes.lsp
M books/kestrel/axe/.sys/known-b...@useless-runes.lsp
M books/kestrel/axe/.sys/largest-n...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-normal...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-norma...@useless-runes.lsp
A books/kestrel/axe/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/.sys/list-ru...@useless-runes.lsp
M books/kestrel/axe/.sys/list-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-bind-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-syntaxp...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-synt...@useless-runes.lsp
R books/kestrel/axe/.sys/make-clause-pr...@useless-runes.lsp
M books/kestrel/axe/.sys/make-conju...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-co...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-va...@useless-runes.lsp
A books/kestrel/axe/.sys/make-equali...@useless-runes.lsp
A books/kestrel/axe/.sys/make-equal...@useless-runes.lsp
M books/kestrel/axe/.sys/make-equ...@useless-runes.lsp
M books/kestrel/axe/.sys/make-evalu...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ev...@useless-runes.lsp
M books/kestrel/axe/.sys/make-impli...@useless-runes.lsp
M books/kestrel/axe/.sys/make-node-rep...@useless-runes.lsp
M books/kestrel/axe/.sys/make-prov...@useless-runes.lsp
M books/kestrel/axe/.sys/make-rewri...@useless-runes.lsp
M books/kestrel/axe/.sys/make-subcor-var-an...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/match-hyp-with-node...@useless-runes.lsp
M books/kestrel/axe/.sys/memoi...@useless-runes.lsp
R books/kestrel/axe/.sys/merge-and-...@useless-runes.lsp
A books/kestrel/axe/.sys/merge-and-remov...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-dag-in...@useless-runes.lsp
A books/kestrel/axe/.sys/merge-greater-tha...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-less-than...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-nodes-i...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-b...@useless-runes.lsp
A books/kestrel/axe/.sys/merge-sort-greater-...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-less-th...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-le...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-tree-into...@useless-runes.lsp
M books/kestrel/axe/.sys/node...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replacement-...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/nodenum-t...@useless-runes.lsp
M books/kestrel/axe/.sys/normali...@useless-runes.lsp
M books/kestrel/axe/.sys/numeri...@useless-runes.lsp
M books/kestrel/axe/.sys/packb...@useless-runes.lsp
A books/kestrel/axe/.sys/portc...@useless-runes.lsp
M books/kestrel/axe/.sys/possibly-neg...@useless-runes.lsp
A books/kestrel/axe/.sys/prove-equal-wit...@useless-runes.lsp
R books/kestrel/axe/.sys/prove-equiv...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
R books/kestrel/axe/.sys/prover-basic-clau...@useless-runes.lsp
R books/kestrel/axe/.sys/prover-basic-c...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover-st...@useless-runes.lsp
M books/kestrel/axe/.sys/pro...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/prune...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-with-c...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-wit...@useless-runes.lsp
M books/kestrel/axe/.sys/pure-da...@useless-runes.lsp
M books/kestrel/axe/.sys/pure...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild-...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuil...@useless-runes.lsp
M books/kestrel/axe/.sys/refine-as...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
A books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assu...@useless-runes.lsp
A books/kestrel/axe/.sys/register-and-wrap-cl...@useless-runes.lsp
M books/kestrel/axe/.sys/remov...@useless-runes.lsp
M books/kestrel/axe/.sys/renamin...@useless-runes.lsp
M books/kestrel/axe/.sys/renumber...@useless-runes.lsp
M books/kestrel/axe/.sys/replac...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-usin...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/result-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
A books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/safe-u...@useless-runes.lsp
R books/kestrel/axe/.sys/sortedp-less-...@useless-runes.lsp
A books/kestrel/axe/.sys/speci...@useless-runes.lsp
M books/kestrel/axe/.sys/spli...@useless-runes.lsp
M books/kestrel/axe/.sys/step-in...@useless-runes.lsp
M books/kestrel/axe/.sys/stored...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-count...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-var-a...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-va...@useless-runes.lsp
M books/kestrel/axe/.sys/substitu...@useless-runes.lsp
M books/kestrel/axe/.sys/substit...@useless-runes.lsp
M books/kestrel/axe/.sys/supporti...@useless-runes.lsp
M books/kestrel/axe/.sys/support...@useless-runes.lsp
M books/kestrel/axe/.sys/sweep-and-m...@useless-runes.lsp
M books/kestrel/axe/.sys/tactic...@useless-runes.lsp
M books/kestrel/axe/.sys/tagged-r...@useless-runes.lsp
M books/kestrel/axe/.sys/term-eq...@useless-runes.lsp
M books/kestrel/axe/.sys/test-...@useless-runes.lsp
M books/kestrel/axe/.sys/translate-...@useless-runes.lsp
M books/kestrel/axe/.sys/translat...@useless-runes.lsp
M books/kestrel/axe/.sys/tr...@useless-runes.lsp
A books/kestrel/axe/.sys/trim-intro...@useless-runes.lsp
M books/kestrel/axe/.sys/type-in...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarded...@useless-runes.lsp
A books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarded-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-tre...@useless-runes.lsp
M books/kestrel/axe/.sys/unroll-s...@useless-runes.lsp
R books/kestrel/axe/.sys/ut...@useless-runes.lsp
A books/kestrel/axe/.sys/utiliti...@useless-runes.lsp
A books/kestrel/axe/.sys/util...@useless-runes.lsp
A books/kestrel/axe/.sys/var-typ...@useless-runes.lsp
M books/kestrel/axe/.sys/wf-...@useless-runes.lsp
M books/kestrel/axe/.sys/worklis...@useless-runes.lsp
M books/kestrel/axe/README.md
M books/kestrel/axe/add-and-normalize-expr.lisp
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/axe-syntax-functions.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/boolean-rules-axe.lisp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-list-rules-axe.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/call-axe-script.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
A books/kestrel/axe/count-branches.lisp
M books/kestrel/axe/dag-size-fast.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-tests.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/doc.lisp
M books/kestrel/axe/equivalence-checker-helpers.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluate-test-case-simple.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/evaluator.lisp
A books/kestrel/axe/examples/.sys/aes-blas...@useless-runes.lsp
A books/kestrel/axe/examples/.sys/aes-...@useless-runes.lsp
M books/kestrel/axe/examples/aes-blast-boolean.lisp
M books/kestrel/axe/examples/aes-blast.lisp
M books/kestrel/axe/find-probable-facts-common.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
A books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/instantiate-hyp.lisp
M books/kestrel/axe/jvm/.gitignore
M books/kestrel/axe/jvm/.sys/axe-bind-free...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntaxp-...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/formal-un...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-rul...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-ru...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lif...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/nice-output...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/output-i...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rule-li...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unroll-java...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unroll-j...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unroll-j...@useless-runes.lsp
M books/kestrel/axe/jvm/doc.lisp
M books/kestrel/axe/jvm/examples/README.md
M books/kestrel/axe/jvm/examples/crypto/aes-128-encrypt-light-and-spec.lisp
M books/kestrel/axe/jvm/examples/crypto/aes-128-encrypt-regular-and-spec-alt.lisp
M books/kestrel/axe/jvm/examples/crypto/aes-128-encrypt-regular-and-spec.lisp
R books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.class
R books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.java
R books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.lisp
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.class
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.java
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.lisp
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.class
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.java
R books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.lisp
R books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.class
R books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.java
R books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.lisp
R books/kestrel/axe/jvm/examples/formal-unit-tester/cert.acl2
R books/kestrel/axe/jvm/examples/formal-unit-tester/top.lisp
A books/kestrel/axe/jvm/examples/formal-unit-tests/AbsLong.class
A books/kestrel/axe/jvm/examples/formal-unit-tests/AbsLong.java
A books/kestrel/axe/jvm/examples/formal-unit-tests/AbsLong.lisp
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearch.class
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearch.java
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearch.lisp
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearchBuggy.class
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearchBuggy.java
A books/kestrel/axe/jvm/examples/formal-unit-tests/BinarySearchBuggy.lisp
A books/kestrel/axe/jvm/examples/formal-unit-tests/Prefix.class
A books/kestrel/axe/jvm/examples/formal-unit-tests/Prefix.java
A books/kestrel/axe/jvm/examples/formal-unit-tests/Prefix.lisp
A books/kestrel/axe/jvm/examples/formal-unit-tests/cert.acl2
A books/kestrel/axe/jvm/examples/formal-unit-tests/top.lisp
R books/kestrel/axe/jvm/formal-unit-tester-exec.acl2
R books/kestrel/axe/jvm/formal-unit-tester-exec.lisp
R books/kestrel/axe/jvm/formal-unit-tester.acl2
R books/kestrel/axe/jvm/formal-unit-tester.lisp
R books/kestrel/axe/jvm/formal-unit-tester.sh
M books/kestrel/axe/jvm/jvm-rules-axe.lisp
M books/kestrel/axe/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
R books/kestrel/axe/jvm/save-exec-for-fut.sh
A books/kestrel/axe/jvm/save-exec-for-tester.sh
M books/kestrel/axe/jvm/symbolic-execution-rules.lisp
A books/kestrel/axe/jvm/tester-exec.acl2
A books/kestrel/axe/jvm/tester-exec.lisp
A books/kestrel/axe/jvm/tester.acl2
A books/kestrel/axe/jvm/tester.lisp
A books/kestrel/axe/jvm/tester.sh
M books/kestrel/axe/jvm/top.lisp
R books/kestrel/axe/jvm/unroll-java-code-common.acl2
R books/kestrel/axe/jvm/unroll-java-code-common.lisp
R books/kestrel/axe/jvm/unroll-java-code.acl2
R books/kestrel/axe/jvm/unroll-java-code.lisp
R books/kestrel/axe/jvm/unroll-java-code2.acl2
R books/kestrel/axe/jvm/unroll-java-code2.lisp
A books/kestrel/axe/jvm/unroller-common.acl2
A books/kestrel/axe/jvm/unroller-common.lisp
A books/kestrel/axe/jvm/unroller.acl2
A books/kestrel/axe/jvm/unroller.lisp
A books/kestrel/axe/jvm/unroller2.acl2
A books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/known-predicates.lisp
R books/kestrel/axe/letify-term-via-dag.acl2
M books/kestrel/axe/letify-term-via-dag.lisp
A books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/list-rules.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-instantiation-code-simple-free-vars.lisp
M books/kestrel/axe/make-instantiation-code-simple-no-free-vars2.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/memoization.lisp
M books/kestrel/axe/merge-nodes-into-dag-array.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-tree-into-dag-array-basic.lisp
M books/kestrel/axe/node-replacement-array3.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/oset-defs.lisp
M books/kestrel/axe/possibly-negated-nodenums.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-dag-precisely.lisp
M books/kestrel/axe/prune-term-tests.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/pure-dags.lisp
M books/kestrel/axe/r1cs/.sys/axe-evalu...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-pro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1c...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift...@useless-runes.lsp
M books/kestrel/axe/r1cs/lift-r1cs.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-justification.lisp
A books/kestrel/axe/risc-v/.sys/assum...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/clear-...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/d...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/eval...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/lifter...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/p...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/portc...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/read-an...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/read-over-...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/regi...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/rewr...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/risc-v...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/rule-...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/run-unti...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/support...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/sup...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/syntax-e...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/syntax-f...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/unr...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/write-over-...@useless-runes.lsp
A books/kestrel/axe/risc-v/README.md
A books/kestrel/axe/risc-v/acl2-customization.lsp
A books/kestrel/axe/risc-v/assumptions.lisp
A books/kestrel/axe/risc-v/clear-writes.lisp
A books/kestrel/axe/risc-v/doc.acl2
A books/kestrel/axe/risc-v/doc.lisp
A books/kestrel/axe/risc-v/evaluator.lisp
A books/kestrel/axe/risc-v/examples/README.md
A books/kestrel/axe/risc-v/examples/add/.sys/add-n...@useless-runes.lsp
A books/kestrel/axe/risc-v/examples/add/.sys/a...@useless-runes.lsp
A books/kestrel/axe/risc-v/examples/add/README.md
A books/kestrel/axe/risc-v/examples/add/acl2-customization.lsp
A books/kestrel/axe/risc-v/examples/add/add-non-axe.lisp
A books/kestrel/axe/risc-v/examples/add/add-position-independent.acl2
A books/kestrel/axe/risc-v/examples/add/add-position-independent.lisp
A books/kestrel/axe/risc-v/examples/add/add.acl2
A books/kestrel/axe/risc-v/examples/add/add.c
A books/kestrel/axe/risc-v/examples/add/add.elf32
A books/kestrel/axe/risc-v/examples/add/add.lisp
A books/kestrel/axe/risc-v/lifter-rules.lisp
A books/kestrel/axe/risc-v/package.lsp
A books/kestrel/axe/risc-v/pc.lisp
A books/kestrel/axe/risc-v/portcullis.acl2
A books/kestrel/axe/risc-v/portcullis.lisp
A books/kestrel/axe/risc-v/read-and-write.lisp
A books/kestrel/axe/risc-v/read-over-write-rules.lisp
A books/kestrel/axe/risc-v/registers.lisp
A books/kestrel/axe/risc-v/rewriter.acl2
A books/kestrel/axe/risc-v/rewriter.lisp
A books/kestrel/axe/risc-v/risc-v-rules.lisp
A books/kestrel/axe/risc-v/rule-lists.lisp
A books/kestrel/axe/risc-v/run-until-return.lisp
A books/kestrel/axe/risc-v/support-non-axe.lisp
A books/kestrel/axe/risc-v/support.lisp
A books/kestrel/axe/risc-v/syntax-functions.lisp
A books/kestrel/axe/risc-v/syntaxp-evaluator.lisp
A books/kestrel/axe/risc-v/top.acl2
A books/kestrel/axe/risc-v/top.lisp
A books/kestrel/axe/risc-v/unroller.acl2
A books/kestrel/axe/risc-v/unroller.lisp
A books/kestrel/axe/risc-v/write-over-write-rules.lisp
M books/kestrel/axe/rule-alists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules2.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/tactic-prover.lisp
A books/kestrel/axe/tester-common.lisp
M books/kestrel/axe/tests-top.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
A books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/type-inference.lisp
M books/kestrel/axe/unguarded-defuns.lisp
A books/kestrel/axe/unguarded-defuns2.lisp
M books/kestrel/axe/unify-term-and-dag-fast.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/util2.lisp
A books/kestrel/axe/utilities-tests.lisp
A books/kestrel/axe/utilities.lisp
M books/kestrel/axe/x86/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/bind-free-e...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/d...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/loop-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/prove-eq...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/rewriter-x8...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/syntaxp-ev...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/tester-c...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tester-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tester...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tes...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/unroll-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/x86-...@useless-runes.lsp
M books/kestrel/axe/x86/axe-syntax-functions-x86.lisp
M books/kestrel/axe/x86/doc.lisp
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/examples/add/.sys/add-...@useless-runes.lsp
M books/kestrel/axe/x86/examples/add/add-elf64.lisp
A books/kestrel/axe/x86/examples/charptr/README.txt
A books/kestrel/axe/x86/examples/charptr/acl2-customization.lsp
A books/kestrel/axe/x86/examples/charptr/cert.acl2
A books/kestrel/axe/x86/examples/charptr/charptr-locations-elf64.lisp
A books/kestrel/axe/x86/examples/charptr/charptr-locations.c
A books/kestrel/axe/x86/examples/charptr/charptr-locations.elf64
A books/kestrel/axe/x86/examples/charptr/return-literal-elf64.lisp
A books/kestrel/axe/x86/examples/charptr/return-literal.c
A books/kestrel/axe/x86/examples/charptr/return-literal.elf64
A books/kestrel/axe/x86/examples/charptr/simple-byte-elf64.lisp
A books/kestrel/axe/x86/examples/charptr/simple-byte.c
A books/kestrel/axe/x86/examples/charptr/simple-byte.elf64
A books/kestrel/axe/x86/examples/factorial/.sys/factori...@useless-runes.lsp
M books/kestrel/axe/x86/examples/factorial/.sys/factoria...@useless-runes.lsp
M books/kestrel/axe/x86/examples/factorial/README.txt
A books/kestrel/axe/x86/examples/factorial/factorial-elf64.acl2
A books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
A books/kestrel/axe/x86/examples/factorial/factorial.elf64
A books/kestrel/axe/x86/examples/formal-unit-tests/add/.sys/run-...@useless-runes.lsp
M books/kestrel/axe/x86/examples/formal-unit-tests/add/run-test.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/x86/examples/switch/README.txt
A books/kestrel/axe/x86/examples/switch/acl2-customization.lsp
A books/kestrel/axe/x86/examples/switch/cert.acl2
A books/kestrel/axe/x86/examples/switch/support.lisp
A books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
A books/kestrel/axe/x86/examples/switch/switch-complex-1a.c
A books/kestrel/axe/x86/examples/switch/switch-complex-1a.elf64
A books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
A books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
A books/kestrel/axe/x86/examples/switch/switch-complex.c
A books/kestrel/axe/x86/examples/switch/switch-complex.elf64
A books/kestrel/axe/x86/examples/switch/switch-complex.elf64staticO2
A books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
A books/kestrel/axe/x86/examples/switch/switch.c
A books/kestrel/axe/x86/examples/switch/switch.elf64
A books/kestrel/axe/x86/examples/switch/switch.macho64
M books/kestrel/axe/x86/examples/tea/tea-elf64.lisp
M books/kestrel/axe/x86/examples/tea/tea-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/prove-equivalence.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/tests/kestrel/README.txt
M books/kestrel/axe/x86/tests/kestrel/add-elf64-full.lisp
M books/kestrel/axe/x86/tests/kestrel/add-elf64.lisp
A books/kestrel/axe/x86/tests/kestrel/add-pe64.lisp
A books/kestrel/axe/x86/tests/kestrel/add.pe64
A books/kestrel/axe/x86/tests/ndsu/mul.c
A books/kestrel/axe/x86/tests/ndsu/mul.elf64
A books/kestrel/axe/x86/tests/ndsu/mul.macho64
A books/kestrel/axe/x86/tests/ndsu/mul.pe64
A books/kestrel/axe/x86/tests/ndsu/pand.c
A books/kestrel/axe/x86/tests/ndsu/pand.elf64
A books/kestrel/axe/x86/tests/ndsu/pand.macho64
A books/kestrel/axe/x86/tests/ndsu/por.c
A books/kestrel/axe/x86/tests/ndsu/por.elf64
A books/kestrel/axe/x86/tests/ndsu/por.macho64
A books/kestrel/axe/x86/tests/ndsu/psub.c
A books/kestrel/axe/x86/tests/ndsu/psub.elf64
A books/kestrel/axe/x86/tests/ndsu/psub.macho64
A books/kestrel/axe/x86/tests/ndsu/pxor.c
A books/kestrel/axe/x86/tests/ndsu/pxor.elf64
A books/kestrel/axe/x86/tests/ndsu/pxor.macho64
A books/kestrel/axe/x86/tests/ndsu/run-tests-mul.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-mul.lisp
M books/kestrel/axe/x86/tests/ndsu/run-tests-or.lisp
A books/kestrel/axe/x86/tests/ndsu/run-tests-pand.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-pand.lisp
A books/kestrel/axe/x86/tests/ndsu/run-tests-por.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-por.lisp
A books/kestrel/axe/x86/tests/ndsu/run-tests-psub.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-psub.lisp
A books/kestrel/axe/x86/tests/ndsu/run-tests-pxor.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-pxor.lisp
M books/kestrel/axe/x86/tests/ndsu/run-tests-sub.lisp
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.lisp
A books/kestrel/axe/x86/tests/ndsu/vpadd128.c
A books/kestrel/axe/x86/tests/ndsu/vpadd128.elf64
A books/kestrel/axe/x86/tests/ndsu/vpadd128.macho64
M books/kestrel/axe/x86/top.lisp
R books/kestrel/axe/x86/unroll-x86-code.acl2
R books/kestrel/axe/x86/unroll-x86-code.lisp
A books/kestrel/axe/x86/unroller.acl2
A books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/bibtex/.sys/bibtex...@useless-runes.lsp
A books/kestrel/bibtex/.sys/xdoc-ge...@useless-runes.lsp
M books/kestrel/bibtex/bibtex-parser.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/kestrel/bitcoin/.sys/bas...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/bec...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/bip39...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/by...@useless-runes.lsp
M books/kestrel/bitcoin/README.md
M books/kestrel/booleans/.sys/boo...@useless-runes.lsp
M books/kestrel/booleans/booleans.lisp
A books/kestrel/booleans/boolif-def.lisp
M books/kestrel/booleans/boolif.lisp
M books/kestrel/booleans/top.lisp
M books/kestrel/bv-lists/.sys/all-all-uns...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/all-signed-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/all-unsign...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/all-unsig...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/append...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-o...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-and-bytes-i...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-and-byt...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-to-byte...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-to-b...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-to-by...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-to-by...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-t...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-con...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-conv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-ar...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arr...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/bv-list-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvchop...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvcho...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvnot...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvplu...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor-li...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-f...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/byte-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-to-b...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-to-b...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/getbi...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/len-mul...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/list-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/logex...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-packbv-an...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-p...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-reve...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-unpac...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-un...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/negated-e...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-little-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbvs...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/string-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpackb...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpa...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unsigned-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/width-of-...@useless-runes.lsp
M books/kestrel/bv-lists/all-unsigned-byte-p.lisp
M books/kestrel/bv-lists/all-unsigned-byte-p2.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions-little.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions.lisp
M books/kestrel/bv-lists/bits-to-byte-little-rules.lisp
M books/kestrel/bv-lists/bv-array-clear-range.lisp
M books/kestrel/bv-lists/bv-array-clear.lisp
M books/kestrel/bv-lists/bv-array-conversions.lisp
M books/kestrel/bv-lists/bv-array-conversions2.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/bv-lists/bv-array-write.lisp
M books/kestrel/bv-lists/bv-arrayp.lisp
M books/kestrel/bv-lists/bv-arrays.lisp
A books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvchop-list.lisp
M books/kestrel/bv-lists/bvxor-list.lisp
M books/kestrel/bv-lists/byte-fix-list.lisp
M books/kestrel/bv-lists/byte-to-bits.lisp
M books/kestrel/bv-lists/bytes-to-bits.lisp
M books/kestrel/bv-lists/getbit-list.lisp
M books/kestrel/bv-lists/logext-list.lisp
A books/kestrel/bv-lists/map-bvplus-val.lisp
A books/kestrel/bv-lists/map-bvsx.lisp
M books/kestrel/bv-lists/packbv-and-unpackbv.lisp
M books/kestrel/bv-lists/packbv-def.lisp
M books/kestrel/bv-lists/packbv-little.lisp
M books/kestrel/bv-lists/packbv-theorems.lisp
M books/kestrel/bv-lists/packbv.lisp
M books/kestrel/bv-lists/packbvs-little.lisp
M books/kestrel/bv-lists/packbvs.lisp
M books/kestrel/bv-lists/packing.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv-lists/unpackbv.lisp
M books/kestrel/bv-lists/unsigned-byte-listp.lisp
M books/kestrel/bv-lists/width-of-widest-int.lisp
M books/kestrel/bv/.sys/ad...@useless-runes.lsp
A books/kestrel/bv/.sys/a...@useless-runes.lsp
A books/kestrel/bv/.sys/b...@useless-runes.lsp
A books/kestrel/bv/.sys/bit-to-...@useless-runes.lsp
M books/kestrel/bv/.sys/bit-t...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bi...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bool-...@useless-runes.lsp
M books/kestrel/bv/.sys/bv-s...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bva...@useless-runes.lsp
M books/kestrel/bv/.sys/bvcat...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvequa...@useless-runes.lsp
M books/kestrel/bv/.sys/bve...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvminu...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvmul...@useless-runes.lsp
M books/kestrel/bv/.sys/bvmult...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvplu...@useless-runes.lsp
M books/kestrel/bv/.sys/bvp...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvsx...@useless-runes.lsp
M books/kestrel/bv/.sys/bvsx-...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvum...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/convert-t...@useless-runes.lsp
M books/kestrel/bv/.sys/defs-...@useless-runes.lsp
M books/kestrel/bv/.sys/de...@useless-runes.lsp
M books/kestrel/bv/.sys/getbit...@useless-runes.lsp
M books/kestrel/bv/.sys/get...@useless-runes.lsp
M books/kestrel/bv/.sys/get...@useless-runes.lsp
M books/kestrel/bv/.sys/idi...@useless-runes.lsp
M books/kestrel/bv/.sys/if-becomes...@useless-runes.lsp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/.sys/leftrota...@useless-runes.lsp
M books/kestrel/bv/.sys/leftro...@useless-runes.lsp
M books/kestrel/bv/.sys/leftr...@useless-runes.lsp
M books/kestrel/bv/.sys/loga...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/logap...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
A books/kestrel/bv/.sys/logc...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/logi...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/logx...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/ones-co...@useless-runes.lsp
M books/kestrel/bv/.sys/overflow-an...@useless-runes.lsp
A books/kestrel/bv/.sys/pad...@useless-runes.lsp
M books/kestrel/bv/.sys/pick-...@useless-runes.lsp
M books/kestrel/bv/.sys/put...@useless-runes.lsp
A books/kestrel/bv/.sys/repeat...@useless-runes.lsp
M books/kestrel/bv/.sys/repea...@useless-runes.lsp
M books/kestrel/bv/.sys/repe...@useless-runes.lsp
A books/kestrel/bv/.sys/rightrot...@useless-runes.lsp
M books/kestrel/bv/.sys/rightr...@useless-runes.lsp
M books/kestrel/bv/.sys/right...@useless-runes.lsp
M books/kestrel/bv/.sys/rot...@useless-runes.lsp
M books/kestrel/bv/.sys/r...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/sbv...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdivdo...@useless-runes.lsp
A books/kestrel/bv/.sys/sbvl...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvlt...@useless-runes.lsp
M books/kestrel/bv/.sys/sb...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvmo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvrem...@useless-runes.lsp
M books/kestrel/bv/.sys/sbv...@useless-runes.lsp
M books/kestrel/bv/.sys/signed...@useless-runes.lsp
M books/kestrel/bv/.sys/singl...@useless-runes.lsp
M books/kestrel/bv/.sys/slice...@useless-runes.lsp
M books/kestrel/bv/.sys/sli...@useless-runes.lsp
M books/kestrel/bv/.sys/sl...@useless-runes.lsp
A books/kestrel/bv/.sys/s...@useless-runes.lsp
A books/kestrel/bv/.sys/trim-elim...@useless-runes.lsp
A books/kestrel/bv/.sys/trim-elim-r...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-int...@useless-runes.lsp
R books/kestrel/bv/.sys/trim-...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigned-byte-...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigned...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigne...@useless-runes.lsp
M books/kestrel/bv/.sys/validatio...@useless-runes.lsp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool-def.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitand.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bitor.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bitxor.lisp
M books/kestrel/bv/bool-to-bit-def.lisp
M books/kestrel/bv/bool-to-bit.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/bvand.lisp
M books/kestrel/bv/bvashr.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvif2.lisp
M books/kestrel/bv/bvlt.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvmult.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvor.lisp
M books/kestrel/bv/bvplus-def.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/bvsx-def.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/bvxor.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/getbit-rules.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/leftrotate-rules.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/logops.lisp
M books/kestrel/bv/logtail.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
A books/kestrel/bv/padding.lisp
M books/kestrel/bv/pick-a-bit.lisp
M books/kestrel/bv/putbits.lisp
A books/kestrel/bv/repeatbit-def.lisp
M books/kestrel/bv/repeatbit.lisp
M books/kestrel/bv/repeatbit2.lisp
M books/kestrel/bv/rightrotate-rules.lisp
M books/kestrel/bv/rightrotate.lisp
M books/kestrel/bv/rotate.lisp
M books/kestrel/bv/rtl.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules0.lisp
M books/kestrel/bv/rules10.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/rules5.lisp
M books/kestrel/bv/rules6.lisp
M books/kestrel/bv/rules8.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/bv/sbvlt.lisp
M books/kestrel/bv/signed-byte-p.lisp
M books/kestrel/bv/slice.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/bv/top.lisp
A books/kestrel/bv/trim-elim-rules-bv.lisp
A books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim-intro-rules.lisp
R books/kestrel/bv/trim-rules.lisp
M books/kestrel/bv/trim.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/bv/unsigned-byte-p.lisp
M books/kestrel/bv/validation-stp.lisp
A books/kestrel/c/.sys/insertion-sort-of...@useless-runes.lsp
A books/kestrel/c/.sys/inserti...@useless-runes.lsp
M books/kestrel/c/README.md
M books/kestrel/c/atc/README.md
M books/kestrel/c/atc/atc.lisp
M books/kestrel/c/atc/doc.lisp
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/function-tables.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/atc/pretty-printer.lisp
M books/kestrel/c/atc/read-write-variables.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-computation-states.lisp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/adjus...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-bl...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-e...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-ex...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
A books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-ob...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/ident...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/inte...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/object-de...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/convert-integer-value.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-block-item.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
R books/kestrel/c/atc/symbolic-execution-rules/exec-expr-asg.lisp
R books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-asg.lisp
R books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-pure.lisp
R books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call.lisp
A books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
A books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
A books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-fun.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-initer.lisp
A books/kestrel/c/atc/symbolic-execution-rules/exec-obj-declon.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/symbolic-execution-rules/top.lisp
M books/kestrel/c/atc/symbolic-execution-rules/type-prescriptions.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/atc/tag-tables.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/atc/variable-tables.lisp
M books/kestrel/c/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/c/language/.sys/arithmetic...@useless-runes.lsp
R books/kestrel/c/language/.sys/by...@useless-runes.lsp
M books/kestrel/c/language/.sys/charact...@useless-runes.lsp
M books/kestrel/c/language/.sys/computati...@useless-runes.lsp
M books/kestrel/c/language/.sys/dynamic-...@useless-runes.lsp
M books/kestrel/c/language/.sys/function-e...@useless-runes.lsp
A books/kestrel/c/language/.sys/ident...@useless-runes.lsp
R books/kestrel/c/language/.sys/implementatio...@useless-runes.lsp
M books/kestrel/c/language/.sys/integer-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/integer...@useless-runes.lsp
M books/kestrel/c/language/.sys/object-de...@useless-runes.lsp
M books/kestrel/c/language/.sys/opera...@useless-runes.lsp
M books/kestrel/c/language/.sys/pointer-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/real-op...@useless-runes.lsp
M books/kestrel/c/language/.sys/scalar-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/structure-...@useless-runes.lsp
M books/kestrel/c/language/.sys/tag-envi...@useless-runes.lsp
M books/kestrel/c/language/.sys/ty...@useless-runes.lsp
M books/kestrel/c/language/.sys/val...@useless-runes.lsp
M books/kestrel/c/language/abstract-syntax-operations.lisp
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/arithmetic-operations.lisp
M books/kestrel/c/language/array-operations.lisp
R books/kestrel/c/language/bytes.lisp
M books/kestrel/c/language/character-sets.lisp
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/errors.lisp
A books/kestrel/c/language/execution-limit-monotonicity.lisp
A books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/flexible-array-member-removal.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/function-environments.lisp
M books/kestrel/c/language/grammar.lisp
A books/kestrel/c/language/identifiers.lisp
R books/kestrel/c/language/implementation-environments.lisp
A books/kestrel/c/language/implementation-environments/.sys/char-f...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/integer-form...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/integer...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/schar-...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/signed-...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/t...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/uchar-...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/acl2-customization.lsp
A books/kestrel/c/language/implementation-environments/bool-formats.lisp
A books/kestrel/c/language/implementation-environments/char-formats.lisp
A books/kestrel/c/language/implementation-environments/integer-format-templates.lisp
A books/kestrel/c/language/implementation-environments/integer-formats.lisp
A books/kestrel/c/language/implementation-environments/schar-formats.lisp
A books/kestrel/c/language/implementation-environments/signed-formats.lisp
A books/kestrel/c/language/implementation-environments/top.lisp
A books/kestrel/c/language/implementation-environments/uchar-formats.lisp
A books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/integer-formats.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/language/integer-ranges.lisp
M books/kestrel/c/language/keywords.lisp
M books/kestrel/c/language/object-designators.lisp
A books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/operations.lisp
M books/kestrel/c/language/pointer-operations.lisp
M books/kestrel/c/language/portable-ascii-identifiers.lisp
A books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/real-operations.lisp
M books/kestrel/c/language/scalar-operations.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/c/language/structure-operations.lisp
M books/kestrel/c/language/tag-environments.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/types.lisp
M books/kestrel/c/language/values.lisp
A books/kestrel/c/language/variable-resolution-preservation.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
A books/kestrel/c/representation/.sys/shallow-de...@useless-runes.lsp
M books/kestrel/c/representation/integer-operations.lisp
M books/kestrel/c/representation/integers.lisp
R books/kestrel/c/syntax/.gitattributes
A books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-syn...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-s...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstrac...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/ascii-id...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/bui...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/code-en...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/concret...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/defpr...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/def...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/disamb...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/file-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/fi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/forma...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/grammar-c...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/gra...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/implementatio...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/keyw...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/langdef...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/output...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproc...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pri...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/pur...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/stan...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unamb...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
A books/kestrel/c/syntax/abstract-syntax-make-self.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/abstraction-mapping.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
A books/kestrel/c/syntax/builtin.lisp
A books/kestrel/c/syntax/code-ensembles.lisp
A books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
R books/kestrel/c/syntax/defpred-doc.lisp
R books/kestrel/c/syntax/defpred.lisp
A books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/disambiguator.lisp
A books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/formalized.lisp
A books/kestrel/c/syntax/grammar-characters.lisp
R books/kestrel/c/syntax/grammar.abnf
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/grammar/.gitattributes
A books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
R books/kestrel/c/syntax/keywords.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
A books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/output-files-doc.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
A books/kestrel/c/syntax/parser-messages.lisp
A books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/parsing.lisp
R books/kestrel/c/syntax/preprocess-file.lisp
A books/kestrel/c/syntax/preprocessing.lisp
A books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/purity.lisp
A books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/standard.lisp
A books/kestrel/c/syntax/storage-specifier-lists.lisp
A books/kestrel/c/syntax/tests/.gitattributes
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
A books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/compile_commands.json
R books/kestrel/c/syntax/tests/defpred.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
A books/kestrel/c/syntax/tests/faildimb.c
A books/kestrel/c/syntax/tests/failparse.c
A books/kestrel/c/syntax/tests/failvalidate.c
M books/kestrel/c/syntax/tests/input-files.lisp
A books/kestrel/c/syntax/tests/lexer.lisp
A books/kestrel/c/syntax/tests/macro_test1.c
A books/kestrel/c/syntax/tests/macro_test2.c
M books/kestrel/c/syntax/tests/output-files.lisp
A books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocess-file.lisp
A books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/type-specifier-lists.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
A books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@useless-runes.lsp
R books/kestrel/c/transformation/.sys/deft...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/proof-genera...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/proof-ge...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/ren...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/simpad...@useless-runes.lsp
R books/kestrel/c/transformation/.sys/simpadd...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/simp...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/special...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/speci...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-al...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
R books/kestrel/c/transformation/.sys/split-f...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-fn...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/splitg...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
A books/kestrel/c/transformation/command-line/.sys/trans...@useless-runes.lsp
A books/kestrel/c/transformation/command-line/.sys/wrap...@useless-runes.lsp
M books/kestrel/c/transformation/command-line/README.md
M books/kestrel/c/transformation/command-line/tests/.gitignore
A books/kestrel/c/transformation/command-line/tests/README.txt
A books/kestrel/c/transformation/command-line/tests/input-files/file4.c
A books/kestrel/c/transformation/command-line/tests/input-files/file6.c
A books/kestrel/c/transformation/command-line/tests/input-files/file7.c
A books/kestrel/c/transformation/command-line/tests/input-files/file8.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
A books/kestrel/c/transformation/command-line/tests/split-fn.json
A books/kestrel/c/transformation/command-line/tests/split-fn2.json
A books/kestrel/c/transformation/command-line/tests/split-fn3.json
A books/kestrel/c/transformation/command-line/tests/split-gso.json
R books/kestrel/c/transformation/command-line/tests/splitgso.json
A books/kestrel/c/transformation/command-line/tests/wrap-fn.json
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
A books/kestrel/c/transformation/input-processing.lisp
M books/kestrel/c/transformation/package.lsp
A books/kestrel/c/transformation/proof-generation-theorems.lisp
A books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize-doc.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso-doc.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-doc.lisp
M books/kestrel/c/transformation/split-fn-when-doc.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
A books/kestrel/c/transformation/split-gso-doc.lisp
A books/kestrel/c/transformation/split-gso.lisp
R books/kestrel/c/transformation/splitgso-doc.lisp
R books/kestrel/c/transformation/splitgso.lisp
R books/kestrel/c/transformation/tests/.sys/cop...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/deft...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/ren...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/simpadd...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/simp...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/speci...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/split-f...@useless-runes.lsp
R books/kestrel/c/transformation/tests/.sys/spli...@useless-runes.lsp
A books/kestrel/c/transformation/tests/.sys/util...@useless-runes.lsp
A books/kestrel/c/transformation/tests/call-graph/.sys/call-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/call-graph/call-graph.lisp
A books/kestrel/c/transformation/tests/constant-propagation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/tests/constant-propagation/constant-propagation.lisp
A books/kestrel/c/transformation/tests/copy-fn/.sys/cop...@useless-runes.lsp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
A books/kestrel/c/transformation/tests/copy-fn/test2.c
A books/kestrel/c/transformation/tests/free-vars/.sys/free...@useless-runes.lsp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
A books/kestrel/c/transformation/tests/rename/.sys/ren...@useless-runes.lsp
M books/kestrel/c/transformation/tests/rename/rename.lisp
A books/kestrel/c/transformation/tests/simpadd0/.sys/asg...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/b...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/cast-int...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/cast-lon...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/cons...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/de...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/file-...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/g...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/glo...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/i...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/ife...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/log...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/lo...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nonin...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nosim...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nosimp...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/nosimp...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/pa...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/retur...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/stmt...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/terna...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/v...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
A books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
A books/kestrel/c/transformation/tests/simpadd0/bin.lisp
A books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
A books/kestrel/c/transformation/tests/simpadd0/cast.lisp
A books/kestrel/c/transformation/tests/simpadd0/constant.lisp
A books/kestrel/c/transformation/tests/simpadd0/decl.lisp
A books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
A books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
A books/kestrel/c/transformation/tests/simpadd0/gg.lisp
A books/kestrel/c/transformation/tests/simpadd0/global.lisp
A books/kestrel/c/transformation/tests/simpadd0/if.lisp
A books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
A books/kestrel/c/transformation/tests/simpadd0/logand.lisp
A books/kestrel/c/transformation/tests/simpadd0/logor.lisp
A books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
A books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
A books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
A books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/asg_int.c
A books/kestrel/c/transformation/tests/simpadd0/old/asg_multi.c
A books/kestrel/c/transformation/tests/simpadd0/old/bin.c
A books/kestrel/c/transformation/tests/simpadd0/old/blocks.c
A books/kestrel/c/transformation/tests/simpadd0/old/cast.c
A books/kestrel/c/transformation/tests/simpadd0/old/constant.c
A books/kestrel/c/transformation/tests/simpadd0/old/decl.c
A books/kestrel/c/transformation/tests/simpadd0/old/dowhile.c
R books/kestrel/c/transformation/tests/simpadd0/old/file.c
A books/kestrel/c/transformation/tests/simpadd0/old/file_scope.c
A books/kestrel/c/transformation/tests/simpadd0/old/gg.c
A books/kestrel/c/transformation/tests/simpadd0/old/global.c
A books/kestrel/c/transformation/tests/simpadd0/old/if.c
A books/kestrel/c/transformation/tests/simpadd0/old/ifelse.c
A books/kestrel/c/transformation/tests/simpadd0/old/logand.c
A books/kestrel/c/transformation/tests/simpadd0/old/logor.c
A books/kestrel/c/transformation/tests/simpadd0/old/nonint_const.c
A books/kestrel/c/transformation/tests/simpadd0/old/nonint_param.c
A books/kestrel/c/transformation/tests/simpadd0/old/nonint_return.c
A books/kestrel/c/transformation/tests/simpadd0/old/noninteger.c
A books/kestrel/c/transformation/tests/simpadd0/old/paren.c
A books/kestrel/c/transformation/tests/simpadd0/old/pure_expr_stmt.c
A books/kestrel/c/transformation/tests/simpadd0/old/return_void.c
A books/kestrel/c/transformation/tests/simpadd0/old/stmt_null.c
A books/kestrel/c/transformation/tests/simpadd0/old/ternary_int.c
A books/kestrel/c/transformation/tests/simpadd0/old/unary.c
A books/kestrel/c/transformation/tests/simpadd0/old/variable.c
A books/kestrel/c/transformation/tests/simpadd0/old/while.c
A books/kestrel/c/transformation/tests/simpadd0/paren.lisp
A books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
A books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
R books/kestrel/c/transformation/tests/simpadd0/simpadd0.lisp
A books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
A books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
A books/kestrel/c/transformation/tests/simpadd0/unary.lisp
A books/kestrel/c/transformation/tests/simpadd0/variable.lisp
A books/kestrel/c/transformation/tests/simpadd0/while.lisp
A books/kestrel/c/transformation/tests/specialize/.sys/speci...@useless-runes.lsp
M books/kestrel/c/transformation/tests/specialize/specialize.lisp
A books/kestrel/c/transformation/tests/split-all-gso/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
A books/kestrel/c/transformation/tests/split-fn-when/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
A books/kestrel/c/transformation/tests/split-fn/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
A books/kestrel/c/transformation/tests/split-gso/.gitignore
A books/kestrel/c/transformation/tests/split-gso/.sys/spli...@useless-runes.lsp
A books/kestrel/c/transformation/tests/split-gso/acl2-customization.lsp
A books/kestrel/c/transformation/tests/split-gso/cert.acl2
A books/kestrel/c/transformation/tests/split-gso/extern-struct.c
A books/kestrel/c/transformation/tests/split-gso/simultaneous_init_declors.c
A books/kestrel/c/transformation/tests/split-gso/simultaneous_struct_fields.c
A books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/static-struct1.c
A books/kestrel/c/transformation/tests/split-gso/static-struct2.c
A books/kestrel/c/transformation/tests/split-gso/static_assert_struct_declaration.c
A books/kestrel/c/transformation/tests/split-gso/test1.c
A books/kestrel/c/transformation/tests/split-gso/test2.c
A books/kestrel/c/transformation/tests/split-gso/test3.c
A books/kestrel/c/transformation/tests/split-gso/typedef1.c
A books/kestrel/c/transformation/tests/split-gso/typedef2.c
A books/kestrel/c/transformation/tests/split-gso/weird_initializer.c
R books/kestrel/c/transformation/tests/splitgso/.gitignore
R books/kestrel/c/transformation/tests/splitgso/acl2-customization.lsp
R books/kestrel/c/transformation/tests/splitgso/cert.acl2
R books/kestrel/c/transformation/tests/splitgso/extern-struct.c
R books/kestrel/c/transformation/tests/splitgso/simultaneous_init_declors.c
R books/kestrel/c/transformation/tests/splitgso/simultaneous_struct_fields.c
R books/kestrel/c/transformation/tests/splitgso/splitgso.lisp
R books/kestrel/c/transformation/tests/splitgso/static-struct1.c
R books/kestrel/c/transformation/tests/splitgso/static-struct2.c
R books/kestrel/c/transformation/tests/splitgso/static_assert_struct_declaration.c
R books/kestrel/c/transformation/tests/splitgso/test1.c
R books/kestrel/c/transformation/tests/splitgso/test2.c
R books/kestrel/c/transformation/tests/splitgso/test3.c
R books/kestrel/c/transformation/tests/splitgso/typedef1.c
R books/kestrel/c/transformation/tests/splitgso/typedef2.c
R books/kestrel/c/transformation/tests/splitgso/weird_initializer.c
A books/kestrel/c/transformation/tests/subst-free/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/tests/utilities.lisp
A books/kestrel/c/transformation/tests/wrap-fn/.gitignore
A books/kestrel/c/transformation/tests/wrap-fn/acl2-customization.lsp
A books/kestrel/c/transformation/tests/wrap-fn/cert.acl2
A books/kestrel/c/transformation/tests/wrap-fn/test1.c
A books/kestrel/c/transformation/tests/wrap-fn/test2.c
A books/kestrel/c/transformation/tests/wrap-fn/test3.c
A books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp
M books/kestrel/c/transformation/top.lisp
M books/kestrel/c/transformation/utilities/.sys/call-...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/collect...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/free...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/fresh...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/fresh-ident.lisp
A books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
A books/kestrel/c/transformation/variables-in-computation-states.lisp
A books/kestrel/c/transformation/wrap-fn-doc.lisp
A books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/clause-processors/.sys/push-un...@useless-runes.lsp
R books/kestrel/clause-processors/.sys/push-unary...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/subst...@useless-runes.lsp
M books/kestrel/crypto/aes/.sys/aes-...@useless-runes.lsp
M books/kestrel/crypto/attachments/.sys/hmac-s...@useless-runes.lsp
M books/kestrel/crypto/attachments/.sys/kecca...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-25...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blak...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-c...@useless-runes.lsp
A books/kestrel/crypto/blake/.sys/blake-c...@useless-runes.lsp
A books/kestrel/crypto/blake/.sys/blake-...@useless-runes.lsp
A books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
A books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2s-exten...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2s-...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/blake/blake-256.lisp
M books/kestrel/crypto/blake/blake2b.lisp
M books/kestrel/crypto/blake/blake2s.lisp
A books/kestrel/crypto/chacha/.sys/chacha2...@useless-runes.lsp
A books/kestrel/crypto/chacha/.sys/chac...@useless-runes.lsp
A books/kestrel/crypto/chacha/.sys/portc...@useless-runes.lsp
M books/kestrel/crypto/chacha/chacha20.lisp
M books/kestrel/crypto/ecdsa/.sys/deterministic-ecdsa-...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-ecd...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/deterministic-ecdsa-secp256k1.lisp
M books/kestrel/crypto/ecurve/.sys/prime-fi...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-dom...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-poi...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/short-we...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/hmac/.sys/hmac-s...@useless-runes.lsp
M books/kestrel/crypto/hmac/.sys/hmac-s...@useless-runes.lsp
M books/kestrel/crypto/kdf/.sys/pbkdf2-hm...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/keccak-t...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/kec...@useless-runes.lsp
M books/kestrel/crypto/keccak/keccak.lisp
M books/kestrel/crypto/mimc/.sys/mimcs...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-to-448...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-to-896...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/baby-jubjub-s...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bls12-3...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bn-254-gr...@useless-runes.lsp
A books/kestrel/crypto/primes/.sys/ed25519-b...@useless-runes.lsp
A books/kestrel/crypto/primes/.sys/ed25519-g...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/goldilocks-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/jubjub-sub...@useless-runes.lsp
A books/kestrel/crypto/primes/.sys/nist-p-256...@useless-runes.lsp
A books/kestrel/crypto/primes/.sys/nist-p-256-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/primes/ed25519-base-prime.lisp
M books/kestrel/crypto/primes/ed25519-group-prime.lisp
A books/kestrel/crypto/primes/koala-bear.lisp
M books/kestrel/crypto/primes/nist-p-256-base-prime.lisp
M books/kestrel/crypto/primes/nist-p-256-group-prime.lisp
M books/kestrel/crypto/primes/top.lisp
M books/kestrel/crypto/r1cs/.sys/gad...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/example...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/ru...@useless-runes.lsp
M books/kestrel/crypto/r1cs/gadgets/.sys/xor-...@useless-runes.lsp
A books/kestrel/crypto/r1cs/sparse/.sys/p1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/r1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/README.md
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/bit...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/boole...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/boo...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/conditiona...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/equa...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/na...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/pac...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/pro...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range-ch...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/sele...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/x...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/range-check-tests.lisp
M books/kestrel/crypto/r1cs/tools/.sys/order-r...@useless-runes.lsp
M books/kestrel/crypto/r1cs/tools/.sys/va...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/salsa2...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/sal...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/sha-256.lisp
M books/kestrel/crypto/sha-2/sha-512.lisp
M books/kestrel/crypto/sha-3/.sys/sha-3-va...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sh...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sup...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/t...@useless-runes.lsp
A books/kestrel/crypto/tea/inversion.lisp
M books/kestrel/crypto/tea/tea-rules.lisp
M books/kestrel/crypto/tea/tea-tests.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/ethereum/.sys/data...@useless-runes.lsp
M books/kestrel/ethereum/.sys/mmp-...@useless-runes.lsp
M books/kestrel/ethereum/.sys/t...@useless-runes.lsp
M books/kestrel/ethereum/README.md
M books/kestrel/ethereum/evm/.sys/evm-...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/e...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/sup...@useless-runes.lsp
A books/kestrel/ethereum/evm/README.md
M books/kestrel/ethereum/evm/evm.lisp
M books/kestrel/ethereum/evm/support.lisp
M books/kestrel/ethereum/hex-prefix.lisp
M books/kestrel/ethereum/mmp-trees.lisp
M books/kestrel/ethereum/rlp/.sys/decoding-...@useless-runes.lsp
M books/kestrel/ethereum/rlp/.sys/tr...@useless-runes.lsp
M books/kestrel/ethereum/rlp/big-endian.lisp
M books/kestrel/ethereum/rlp/decodability.lisp
M books/kestrel/ethereum/rlp/decoding-declarative.lisp
M books/kestrel/ethereum/rlp/decoding-executable.lisp
M books/kestrel/ethereum/rlp/encoding.lisp
M books/kestrel/ethereum/rlp/top.lisp
M books/kestrel/ethereum/rlp/trees.lisp
M books/kestrel/ethereum/semaphore/.sys/baby-...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/blake2s-mi...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/peders...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/r1cs-pro...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/lift-semaphore-r1cs.lisp
M books/kestrel/ethereum/semaphore/top.lisp
M books/kestrel/ethereum/top.lisp
M books/kestrel/file-io-light/.sys/close-outp...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/open-inpu...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/open-outp...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-bytes-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-file-into-b...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-object...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-obje...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-strings...@useless-runes.lsp
M books/kestrel/file-io-light/read-file-into-character-list.lisp
M books/kestrel/floats/.sys/ieee-floa...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-floa...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-floats...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-...@useless-runes.lsp
M books/kestrel/floats/.sys/ro...@useless-runes.lsp
M books/kestrel/floats/.sys/r...@useless-runes.lsp
M books/kestrel/floats/ieee-floats-as-bvs.lisp
M books/kestrel/floats/rtl.lisp
M books/kestrel/fty/.sys/bit-...@useless-runes.lsp
M books/kestrel/fty/.sys/byte...@useless-runes.lsp
A books/kestrel/fty/.sys/data...@useless-runes.lsp
M books/kestrel/fty/.sys/defbytel...@useless-runes.lsp
A books/kestrel/fty/.sys/deffold...@useless-runes.lsp
A books/kestrel/fty/.sys/deffold-...@useless-runes.lsp
A books/kestrel/fty/.sys/deffo...@useless-runes.lsp
A books/kestrel/fty/.sys/deffold-r...@useless-runes.lsp
A books/kestrel/fty/.sys/deffold-re...@useless-runes.lsp
A books/kestrel/fty/.sys/deffold...@useless-runes.lsp
A books/kestrel/fty/.sys/defmake-...@useless-runes.lsp
A books/kestrel/fty/.sys/defmake-s...@useless-runes.lsp
A books/kestrel/fty/.sys/defmak...@useless-runes.lsp
M books/kestrel/fty/.sys/defoma...@useless-runes.lsp
M books/kestrel/fty/.sys/defset...@useless-runes.lsp
M books/kestrel/fty/.sys/defsubty...@useless-runes.lsp
A books/kestrel/fty/.sys/depend...@useless-runes.lsp
A books/kestrel/fty/.sys/fo...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-opt...@useless-runes.lsp
M books/kestrel/fty/.sys/nibbl...@useless-runes.lsp
M books/kestrel/fty/.sys/pos-...@useless-runes.lsp
M books/kestrel/fty/.sys/pseudo-even...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte128-i...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte1...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte16-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte1...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte2...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte32-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte3...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte64-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte6...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte8-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/sbyte...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte1...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte12-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte128-i...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte1...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte16-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte1...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte20-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte2...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte3-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte32-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte3...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte32...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte5-ih...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte6-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte64-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte6...@useless-runes.lsp
A books/kestrel/fty/.sys/ubyte7-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte8-ih...@useless-runes.lsp
M books/kestrel/fty/.sys/ubyte...@useless-runes.lsp
A books/kestrel/fty/any-nat-map.lisp
M books/kestrel/fty/bin-digit-char-list.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/database.lisp
M books/kestrel/fty/dec-digit-char-list.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
A books/kestrel/fty/defmake-self-doc.lisp
A books/kestrel/fty/defmake-self-tests.lisp
A books/kestrel/fty/defmake-self.lisp
A books/kestrel/fty/dependencies.lisp
M books/kestrel/fty/fty-set.lisp
M books/kestrel/fty/hex-digit-char-list.lisp
M books/kestrel/fty/oct-digit-char-list.lisp
M books/kestrel/fty/string-stringlist-alist.lisp
A books/kestrel/fty/string-stringlist-map.lisp
M books/kestrel/fty/strings-decimal-fty.lisp
M books/kestrel/fty/symbol-pseudoeventform-alist.lisp
M books/kestrel/fty/symbol-pseudoterm-alist.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/hdwallet/.sys/wal...@useless-runes.lsp
M books/kestrel/hdwallet/README.md
M books/kestrel/helpers/.sys/advice-imp...@useless-runes.lsp
M books/kestrel/helpers/.sys/duplica...@useless-runes.lsp
M books/kestrel/helpers/.sys/hel...@useless-runes.lsp
M books/kestrel/helpers/.sys/improve-book-...@useless-runes.lsp
M books/kestrel/helpers/.sys/lin...@useless-runes.lsp
M books/kestrel/helpers/.sys/recomme...@useless-runes.lsp
M books/kestrel/helpers/.sys/replay-b...@useless-runes.lsp
M books/kestrel/helpers/.sys/replay-books...@useless-runes.lsp
M books/kestrel/java/README.md
M books/kestrel/java/aij/README.md
M books/kestrel/java/atj/.sys/java-abstr...@useless-runes.lsp
M books/kestrel/java/atj/.sys/test-st...@useless-runes.lsp
M books/kestrel/java/atj/.sys/ty...@useless-runes.lsp
M books/kestrel/java/atj/README.md
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/tests/ABNFDeepGuardedTests.java
M books/kestrel/java/atj/tests/ABNFShallowGuardedTests.java
M books/kestrel/java/language/.sys/binary...@useless-runes.lsp
M books/kestrel/java/language/.sys/binary-inte...@useless-runes.lsp
M books/kestrel/java/language/.sys/decimal...@useless-runes.lsp
M books/kestrel/java/language/.sys/decimal-inte...@useless-runes.lsp
M books/kestrel/java/language/.sys/hexadecim...@useless-runes.lsp
M books/kestrel/java/language/.sys/hexadecimal-in...@useless-runes.lsp
M books/kestrel/java/language/.sys/ident...@useless-runes.lsp
M books/kestrel/java/language/.sys/octal-...@useless-runes.lsp
M books/kestrel/java/language/.sys/octal-integ...@useless-runes.lsp
M books/kestrel/java/language/.sys/poin...@useless-runes.lsp
M books/kestrel/java/language/.sys/primitive-...@useless-runes.lsp
M books/kestrel/java/language/.sys/primitiv...@useless-runes.lsp
M books/kestrel/java/language/.sys/referen...@useless-runes.lsp
M books/kestrel/java/language/.sys/string-...@useless-runes.lsp
M books/kestrel/java/language/.sys/unicode-c...@useless-runes.lsp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/identifiers.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/keywords.lisp
M books/kestrel/java/language/lexical-grammar.abnf
M books/kestrel/java/language/syntactic-grammar.abnf
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/top.lisp
M books/kestrel/json-parser/.sys/parse...@useless-runes.lsp
M books/kestrel/json-parser/.sys/parse...@useless-runes.lsp
M books/kestrel/json-parser/parse-json-file.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/json/.sys/val...@useless-runes.lsp
M books/kestrel/jvm/.sys/ad...@useless-runes.lsp
M books/kestrel/jvm/.sys/a...@useless-runes.lsp
M books/kestrel/jvm/.sys/ads...@useless-runes.lsp
M books/kestrel/jvm/.sys/array-b...@useless-runes.lsp
M books/kestrel/jvm/.sys/arra...@useless-runes.lsp
M books/kestrel/jvm/.sys/arr...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-fi...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-...@useless-runes.lsp
M books/kestrel/jvm/.sys/cla...@useless-runes.lsp
M books/kestrel/jvm/.sys/contro...@useless-runes.lsp
M books/kestrel/jvm/.sys/do-ins...@useless-runes.lsp
M books/kestrel/jvm/.sys/execu...@useless-runes.lsp
M books/kestrel/jvm/.sys/exec...@useless-runes.lsp
M books/kestrel/jvm/.sys/flo...@useless-runes.lsp
M books/kestrel/jvm/.sys/fra...@useless-runes.lsp
M books/kestrel/jvm/.sys/heap-c...@useless-runes.lsp
M books/kestrel/jvm/.sys/he...@useless-runes.lsp
M books/kestrel/jvm/.sys/he...@useless-runes.lsp
M books/kestrel/jvm/.sys/instru...@useless-runes.lsp
M books/kestrel/jvm/.sys/intern...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-r...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@useless-runes.lsp
M books/kestrel/jvm/.sys/j...@useless-runes.lsp
M books/kestrel/jvm/.sys/ma...@useless-runes.lsp
M books/kestrel/jvm/.sys/method-desig...@useless-runes.lsp
M books/kestrel/jvm/.sys/method-i...@useless-runes.lsp
A books/kestrel/jvm/.sys/method...@useless-runes.lsp
M books/kestrel/jvm/.sys/read...@useless-runes.lsp
M books/kestrel/jvm/.sys/set-c...@useless-runes.lsp
M books/kestrel/jvm/.sys/str...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-...@useless-runes.lsp
M books/kestrel/jvm/.sys/ty...@useless-runes.lsp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/heap.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/lists-light/.sys/all-equa...@useless-runes.lsp
M books/kestrel/lists-light/.sys/all-...@useless-runes.lsp
M books/kestrel/lists-light/.sys/append-...@useless-runes.lsp
M books/kestrel/lists-light/.sys/app...@useless-runes.lsp
M books/kestrel/lists-light/.sys/co...@useless-runes.lsp
A books/kestrel/lists-light/.sys/contains...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ever...@useless-runes.lsp
M books/kestrel/lists-light/.sys/fir...@useless-runes.lsp
A books/kestrel/lists-light/.sys/grou...@useless-runes.lsp
M books/kestrel/lists-light/.sys/group...@useless-runes.lsp
M books/kestrel/lists-light/.sys/gr...@useless-runes.lsp
M books/kestrel/lists-light/.sys/intersect...@useless-runes.lsp
M books/kestrel/lists-light/.sys/la...@useless-runes.lsp
M books/kestrel/lists-light/.sys/no-duplica...@useless-runes.lsp
M books/kestrel/lists-light/.sys/n...@useless-runes.lsp
M books/kestrel/lists-light/.sys/nth...@useless-runes.lsp
M books/kestrel/lists-light/.sys/pre...@useless-runes.lsp
M books/kestrel/lists-light/.sys/reva...@useless-runes.lsp
M books/kestrel/lists-light/.sys/revers...@useless-runes.lsp
M books/kestrel/lists-light/.sys/rul...@useless-runes.lsp
M books/kestrel/lists-light/.sys/subr...@useless-runes.lsp
A books/kestrel/lists-light/.sys/subse...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ta...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ta...@useless-runes.lsp
M books/kestrel/lists-light/.sys/true-l...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ung...@useless-runes.lsp
M books/kestrel/lists-light/.sys/updat...@useless-runes.lsp
M books/kestrel/lists-light/.sys/updat...@useless-runes.lsp
M books/kestrel/lists-light/.sys/update-s...@useless-runes.lsp
M books/kestrel/lists-light/.sys/update-...@useless-runes.lsp
A books/kestrel/lists-light/contains-anyp-eq.lisp
M books/kestrel/lists-light/member-equal.lisp
M books/kestrel/lists-light/revappend.lisp
M books/kestrel/lists-light/reverse.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/lists-light/subsetp-equal.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/lists-light/update-nth.lisp
M books/kestrel/maps/.sys/ma...@useless-runes.lsp
A books/kestrel/memory/.sys/make-memory-re...@useless-runes.lsp
A books/kestrel/memory/.sys/memory-...@useless-runes.lsp
A books/kestrel/memory/.sys/memo...@useless-runes.lsp
A books/kestrel/memory/.sys/memo...@useless-runes.lsp
A books/kestrel/memory/.sys/memo...@useless-runes.lsp
R books/kestrel/memory/make-memory-region-machinery.acl2
M books/kestrel/memory/make-memory-region-machinery.lisp
A books/kestrel/memory/memory-regions.lisp
M books/kestrel/memory/memory32.lisp
M books/kestrel/memory/memory48.lisp
M books/kestrel/memory/memory64.lisp
M books/kestrel/number-theory/.sys/defprim...@useless-runes.lsp
M books/kestrel/number-theory/.sys/defp...@useless-runes.lsp
M books/kestrel/number-theory/.sys/quadrati...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/a...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-r...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/equal-of-add-c...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/equal-of-...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/equal-of-add-mov...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/i...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/m...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/n...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/p...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/prime-fi...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/prime-fie...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/rul...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/s...@useless-runes.lsp
M books/kestrel/prime-fields/bv-rules-axe.lisp
M books/kestrel/prime-fields/equal-of-add-cancel-bind-free.lisp
M books/kestrel/random/.sys/minstd...@useless-runes.lsp
M books/kestrel/random/.sys/minst...@useless-runes.lsp
R books/kestrel/risc-v/.sys/deco...@useless-runes.lsp
R books/kestrel/risc-v/.sys/execu...@useless-runes.lsp
R books/kestrel/risc-v/.sys/execu...@useless-runes.lsp
R books/kestrel/risc-v/.sys/exec...@useless-runes.lsp
R books/kestrel/risc-v/.sys/instru...@useless-runes.lsp
R books/kestrel/risc-v/.sys/library-e...@useless-runes.lsp
R books/kestrel/risc-v/.sys/seman...@useless-runes.lsp
R books/kestrel/risc-v/.sys/seman...@useless-runes.lsp
R books/kestrel/risc-v/.sys/sema...@useless-runes.lsp
R books/kestrel/risc-v/.sys/st...@useless-runes.lsp
R books/kestrel/risc-v/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/.sys/sta...@useless-runes.lsp
A books/kestrel/risc-v/.sys/te...@useless-runes.lsp
M books/kestrel/risc-v/README.md
A books/kestrel/risc-v/executable/.sys/decoding...@useless-runes.lsp
A books/kestrel/risc-v/executable/.sys/decoding-...@useless-runes.lsp
A books/kestrel/risc-v/executable/.sys/decoding-l...@useless-runes.lsp
A books/kestrel/risc-v/executable/.sys/decoding-ri...@useless-runes.lsp
A books/kestrel/risc-v/executable/.sys/execution-...@useless-runes.lsp
A books/kestrel/risc-v/executable/.sys/t...@useless-runes.lsp
M books/kestrel/risc-v/executable/decoding-correct.lisp
M books/kestrel/risc-v/executable/decoding-executable.lisp
M books/kestrel/risc-v/executable/decoding-left-inverse.lisp
M books/kestrel/risc-v/executable/decoding-right-inverse.lisp
M books/kestrel/risc-v/executable/execution-executable.lisp
A books/kestrel/risc-v/library-extensions/.sys/logops-...@useless-runes.lsp
A books/kestrel/risc-v/library-extensions/logops-theorems.lisp
R books/kestrel/risc-v/library-extensions/theorems.lisp
A books/kestrel/risc-v/optimized/.sys/state...@useless-runes.lsp
A books/kestrel/risc-v/optimized/.sys/t...@useless-runes.lsp
M books/kestrel/risc-v/optimized/state-stobj.lisp
A books/kestrel/risc-v/specialized/.sys/execu...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/execu...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/feat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/rv3...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/rv6...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/seman...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/seman...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/sta...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/suppor...@useless-runes.lsp
A books/kestrel/risc-v/specialized/.sys/t...@useless-runes.lsp
R books/kestrel/risc-v/specialized/execution32.lisp
R books/kestrel/risc-v/specialized/execution64.lisp
R books/kestrel/risc-v/specialized/features.lisp
A books/kestrel/risc-v/specialized/rv32im-le/acl2-customization.lsp
A books/kestrel/risc-v/specialized/rv32im-le/execution.lisp
A books/kestrel/risc-v/specialized/rv32im-le/features.lisp
A books/kestrel/risc-v/specialized/rv32im-le/package.lsp
A books/kestrel/risc-v/specialized/rv32im-le/portcullis.acl2
A books/kestrel/risc-v/specialized/rv32im-le/portcullis.lisp
A books/kestrel/risc-v/specialized/rv32im-le/semantics.lisp
A books/kestrel/risc-v/specialized/rv32im-le/states.lisp
A books/kestrel/risc-v/specialized/rv32im-le/supporters32.lisp
A books/kestrel/risc-v/specialized/rv32im-le/top.lisp
R books/kestrel/risc-v/specialized/rv32im.lisp
A books/kestrel/risc-v/specialized/rv64im-le/acl2-customization.lsp
A books/kestrel/risc-v/specialized/rv64im-le/execution.lisp
A books/kestrel/risc-v/specialized/rv64im-le/features.lisp
A books/kestrel/risc-v/specialized/rv64im-le/package.lsp
A books/kestrel/risc-v/specialized/rv64im-le/portcullis.acl2
A books/kestrel/risc-v/specialized/rv64im-le/portcullis.lisp
A books/kestrel/risc-v/specialized/rv64im-le/semantics.lisp
A books/kestrel/risc-v/specialized/rv64im-le/states.lisp
A books/kestrel/risc-v/specialized/rv64im-le/top.lisp
R books/kestrel/risc-v/specialized/rv64im.lisp
R books/kestrel/risc-v/specialized/semantics32.lisp
R books/kestrel/risc-v/specialized/semantics64.lisp
R books/kestrel/risc-v/specialized/states.lisp
R books/kestrel/risc-v/specialized/states32.lisp
R books/kestrel/risc-v/specialized/states32e.lisp
R books/kestrel/risc-v/specialized/states32i.lisp
R books/kestrel/risc-v/specialized/states64.lisp
R books/kestrel/risc-v/specialized/states64e.lisp
R books/kestrel/risc-v/specialized/states64i.lisp
M books/kestrel/risc-v/specialized/top.lisp
A books/kestrel/risc-v/specification/.sys/deco...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/encoding-decodi...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/enco...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/exec...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/feat...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/instru...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/reads-ov...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/semantics-e...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/sema...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/sta...@useless-runes.lsp
A books/kestrel/risc-v/specification/.sys/t...@useless-runes.lsp
M books/kestrel/risc-v/specification/decoding.lisp
M books/kestrel/risc-v/specification/encoding.lisp
M books/kestrel/risc-v/specification/execution.lisp
M books/kestrel/risc-v/specification/features.lisp
M books/kestrel/risc-v/specification/instructions.lisp
M books/kestrel/risc-v/specification/reads-over-writes.lisp
M books/kestrel/risc-v/specification/semantics-equivalences.lisp
M books/kestrel/risc-v/specification/semantics.lisp
M books/kestrel/risc-v/specification/states.lisp
M books/kestrel/risc-v/tests.lisp
M books/kestrel/risc-v/top.lisp
M books/kestrel/sequences/.sys/defe...@useless-runes.lsp
A books/kestrel/sequences/.sys/defforal...@useless-runes.lsp
A books/kestrel/sequences/.sys/deffora...@useless-runes.lsp
M books/kestrel/sequences/.sys/deff...@useless-runes.lsp
A books/kestrel/sequences/.sys/defmap...@useless-runes.lsp
M books/kestrel/sequences/.sys/def...@useless-runes.lsp
M books/kestrel/sequences/.sys/generics-...@useless-runes.lsp
M books/kestrel/sequences/.sys/subsequen...@useless-runes.lsp
A books/kestrel/sequences/.sys/t...@useless-runes.lsp
M books/kestrel/simpl-imp/.sys/abstrac...@useless-runes.lsp
M books/kestrel/simpl-imp/.sys/sema...@useless-runes.lsp
A books/kestrel/smt-lib/fixed-size-bit-vectors.lisp
A books/kestrel/smt-lib/ints.lisp
M books/kestrel/soft/README.md
M books/kestrel/solidity/.sys/integer...@useless-runes.lsp
M books/kestrel/strings-light/.sys/len...@useless-runes.lsp
M books/kestrel/strings-light/.sys/str...@useless-runes.lsp
M books/kestrel/strings-light/.sys/str...@useless-runes.lsp
M books/kestrel/strings-light/.sys/string-e...@useless-runes.lsp
M books/kestrel/strings-light/.sys/strip-suffix...@useless-runes.lsp
M books/kestrel/strings-light/.sys/sub...@useless-runes.lsp
M books/kestrel/syntheto/.sys/base-...@useless-runes.lsp
M books/kestrel/syntheto/.sys/outc...@useless-runes.lsp
M books/kestrel/syntheto/examples/.sys/point-in-...@useless-runes.lsp
M books/kestrel/syntheto/examples/.sys/point-in...@useless-runes.lsp
M books/kestrel/syntheto/examples/.sys/sort-ra...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/static-sema...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/expre...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/functio...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/te...@useless-runes.lsp
M books/kestrel/syntheto/shallow/basetype-info.lisp
M books/kestrel/terms-light/.sys/copy...@useless-runes.lsp
M books/kestrel/terms-light/.sys/drop-trivial-...@useless-runes.lsp
M books/kestrel/terms-light/.sys/drop-trivi...@useless-runes.lsp
M books/kestrel/terms-light/.sys/drop-unused-lambd...@useless-runes.lsp
M books/kestrel/terms-light/.sys/drop-unused-l...@useless-runes.lsp
A books/kestrel/terms-light/.sys/filter-formals-a...@useless-runes.lsp
M books/kestrel/terms-light/.sys/filter-formal...@useless-runes.lsp
M books/kestrel/terms-light/.sys/hel...@useless-runes.lsp
M books/kestrel/terms-light/.sys/make-lambda-applic...@useless-runes.lsp
M books/kestrel/terms-light/.sys/make-lambda-...@useless-runes.lsp
M books/kestrel/terms-light/.sys/make-lambd...@useless-runes.lsp
M books/kestrel/terms-light/.sys/pre-simplify...@useless-runes.lsp
M books/kestrel/terms-light/.sys/serialize-la...@useless-runes.lsp
M books/kestrel/terms-light/.sys/simplify-...@useless-runes.lsp
M books/kestrel/terms-light/.sys/simpli...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-constant...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-l...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-unnecessar...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-unnece...@useless-runes.lsp
M books/kestrel/terms-light/classify-lambda-formals.lisp
M books/kestrel/terms-light/copy-term.lisp
M books/kestrel/terms-light/termp.lisp
A books/kestrel/tests/.sys/t...@useless-runes.lsp
A books/kestrel/treeset/.sys/binary-t...@useless-runes.lsp
A books/kestrel/treeset/.sys/binar...@useless-runes.lsp
A books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
A books/kestrel/treeset/.sys/bst-ord...@useless-runes.lsp
A books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
A books/kestrel/treeset/.sys/b...@useless-runes.lsp
A books/kestrel/treeset/.sys/cardinal...@useless-runes.lsp
A books/kestrel/treeset/.sys/cardi...@useless-runes.lsp
A books/kestrel/treeset/.sys/de...@useless-runes.lsp
A books/kestrel/treeset/.sys/delet...@useless-runes.lsp
A books/kestrel/treeset/.sys/del...@useless-runes.lsp
A books/kestrel/treeset/.sys/diff...@useless-runes.lsp
A books/kestrel/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/treeset/.sys/double-co...@useless-runes.lsp
A books/kestrel/treeset/.sys/f...@useless-runes.lsp
A books/kestrel/treeset/.sys/ha...@useless-runes.lsp
A books/kestrel/treeset/.sys/heap...@useless-runes.lsp
A books/kestrel/treeset/.sys/heap-or...@useless-runes.lsp
A books/kestrel/treeset/.sys/heap-...@useless-runes.lsp
A books/kestrel/treeset/.sys/he...@useless-runes.lsp
A books/kestrel/treeset/.sys/in-...@useless-runes.lsp
A books/kestrel/treeset/.sys/i...@useless-runes.lsp
A books/kestrel/treeset/.sys/inser...@useless-runes.lsp
A books/kestrel/treeset/.sys/ins...@useless-runes.lsp
A books/kestrel/treeset/.sys/interse...@useless-runes.lsp
A books/kestrel/treeset/.sys/inte...@useless-runes.lsp
A books/kestrel/treeset/.sys/jenkin...@useless-runes.lsp
A books/kestrel/treeset/.sys/join...@useless-runes.lsp
A books/kestrel/treeset/.sys/jo...@useless-runes.lsp
A books/kestrel/treeset/.sys/pick-a...@useless-runes.lsp
A books/kestrel/treeset/.sys/portc...@useless-runes.lsp
A books/kestrel/treeset/.sys/rotat...@useless-runes.lsp
A books/kestrel/treeset/.sys/rot...@useless-runes.lsp
A books/kestrel/treeset/.sys/set-...@useless-runes.lsp
A books/kestrel/treeset/.sys/s...@useless-runes.lsp
A books/kestrel/treeset/.sys/split...@useless-runes.lsp
A books/kestrel/treeset/.sys/sp...@useless-runes.lsp
A books/kestrel/treeset/.sys/subse...@useless-runes.lsp
A books/kestrel/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/treeset/.sys/sum-acl2-...@useless-runes.lsp
A books/kestrel/treeset/.sys/sum-acl...@useless-runes.lsp
A books/kestrel/treeset/.sys/t...@useless-runes.lsp
A books/kestrel/treeset/.sys/total...@useless-runes.lsp
A books/kestrel/treeset/.sys/union...@useless-runes.lsp
A books/kestrel/treeset/.sys/un...@useless-runes.lsp
A books/kestrel/treeset/tests/.sys/mk-r...@useless-runes.lsp
A books/kestrel/treeset/tests/.sys/mk-...@useless-runes.lsp
A books/kestrel/treeset/tests/.sys/time...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/all-greater-th...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/all-greater-...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-less-than...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-less-th...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/all-...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/charact...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/decre...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/integer-l...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/items-h...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/less-t...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/make-char...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/map-ch...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/max...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/mine...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/nat-...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/sortedp-greate...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/sortedp-less-...@useless-runes.lsp
M books/kestrel/typed-lists-light/append-all.lisp
M books/kestrel/typed-lists-light/character-listp.lisp
A books/kestrel/typed-lists-light/integer-list-listp.lisp
M books/kestrel/typed-lists-light/integer-listp.lisp
A books/kestrel/typed-lists-light/integer-listp2.lisp
M books/kestrel/typed-lists-light/keyword-listp.lisp
M books/kestrel/typed-lists-light/map-strip-cars.lisp
M books/kestrel/typed-lists-light/pseudo-term-listp.lisp
M books/kestrel/typed-lists-light/top.lisp
M books/kestrel/unicode-light/.sys/code-point-t...@useless-runes.lsp
M books/kestrel/unicode-light/.sys/hex-digit-char...@useless-runes.lsp
M books/kestrel/unicode-light/.sys/surro...@useless-runes.lsp
M books/kestrel/untranslated-terms/.sys/untranslate...@useless-runes.lsp
M books/kestrel/utilities/.sys/array...@useless-runes.lsp
M books/kestrel/utilities/.sys/bits-as...@useless-runes.lsp
M books/kestrel/utilities/.sys/bytes-a...@useless-runes.lsp
M books/kestrel/utilities/.sys/bytes-...@useless-runes.lsp
M books/kestrel/utilities/.sys/coe...@useless-runes.lsp
M books/kestrel/utilities/.sys/decl...@useless-runes.lsp
M books/kestrel/utilities/.sys/definin...@useless-runes.lsp
M books/kestrel/utilities/.sys/defma...@useless-runes.lsp
M books/kestrel/utilities/.sys/defmerges...@useless-runes.lsp
M books/kestrel/utilities/.sys/defop...@useless-runes.lsp
M books/kestrel/utilities/.sys/defstobj-...@useless-runes.lsp
M books/kestrel/utilities/.sys/defun...@useless-runes.lsp
M books/kestrel/utilities/.sys/explode-nonne...@useless-runes.lsp
M books/kestrel/utilities/.sys/fast-al...@useless-runes.lsp
M books/kestrel/utilities/.sys/file-io-st...@useless-runes.lsp
M books/kestrel/utilities/.sys/fixup-ir...@useless-runes.lsp
M books/kestrel/utilities/.sys/for...@useless-runes.lsp
M books/kestrel/utilities/.sys/fresh...@useless-runes.lsp
M books/kestrel/utilities/.sys/hex-strin...@useless-runes.lsp
M books/kestrel/utilities/.sys/integers-fr...@useless-runes.lsp
M books/kestrel/utilities/.sys/integers...@useless-runes.lsp
M books/kestrel/utilities/.sys/keyword-va...@useless-runes.lsp
M books/kestrel/utilities/.sys/make-legal-var-...@useless-runes.lsp
M books/kestrel/utilities/.sys/map-sym...@useless-runes.lsp
M books/kestrel/utilities/.sys/merge-sort-st...@useless-runes.lsp
M books/kestrel/utilities/.sys/mess...@useless-runes.lsp
M books/kestrel/utilities/.sys/ms...@useless-runes.lsp
M books/kestrel/utilities/.sys/myqu...@useless-runes.lsp
A books/kestrel/utilities/.sys/ordi...@useless-runes.lsp
M books/kestrel/utilities/.sys/pa...@useless-runes.lsp
M books/kestrel/utilities/.sys/polarit...@useless-runes.lsp
M books/kestrel/utilities/.sys/print-...@useless-runes.lsp
M books/kestrel/utilities/.sys/qu...@useless-runes.lsp
M books/kestrel/utilities/.sys/rational...@useless-runes.lsp
M books/kestrel/utilities/.sys/real-ti...@useless-runes.lsp
A books/kestrel/utilities/.sys/run-json...@useless-runes.lsp
M books/kestrel/utilities/.sys/set-c...@useless-runes.lsp
A books/kestrel/utilities/.sys/set-print-...@useless-runes.lsp
M books/kestrel/utilities/.sys/signed-by...@useless-runes.lsp
M books/kestrel/utilities/.sys/split-l...@useless-runes.lsp
M books/kestrel/utilities/.sys/st...@useless-runes.lsp
M books/kestrel/utilities/.sys/string-u...@useless-runes.lsp
M books/kestrel/utilities/.sys/ubyte11s-...@useless-runes.lsp
M books/kestrel/utilities/.sys/unsigned-b...@useless-runes.lsp
M books/kestrel/utilities/README.md
M books/kestrel/utilities/defmacrodoc-tests.lisp
M books/kestrel/utilities/defmacrodoc.lisp
M books/kestrel/utilities/defopeners.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/kestrel/utilities/defstobj-plus.lisp
M books/kestrel/utilities/digits-any-base/.sys/co...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/defthm-dab-ret...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/pow...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/pow...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/pow...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/pow...@useless-runes.lsp
M books/kestrel/utilities/digits-any-base/.sys/pow...@useless-runes.lsp
M books/kestrel/utilities/er-soft-plus.lisp
M books/kestrel/utilities/error-checking/.sys/t...@useless-runes.lsp
M books/kestrel/utilities/extend-pathname-dollar.lisp
M books/kestrel/utilities/make-ord.lisp
M books/kestrel/utilities/make-termination-theorem-tests.lisp
M books/kestrel/utilities/pack.lisp
M books/kestrel/utilities/run-json-command.lisp
A books/kestrel/utilities/set-print-base-radix.lisp
M books/kestrel/utilities/strings/.sys/hexc...@useless-runes.lsp
M books/kestrel/utilities/temp-dirs.lisp
A books/kestrel/utilities/untranslate-dollar-list.lisp
A books/kestrel/wasm/.sys/add-...@useless-runes.lsp
A books/kestrel/wasm/.sys/exec...@useless-runes.lsp
A books/kestrel/wasm/.sys/parse-...@useless-runes.lsp
A books/kestrel/wasm/.sys/portc...@useless-runes.lsp
A books/kestrel/wasm/.sys/proof-...@useless-runes.lsp
A books/kestrel/wasm/acl2-customization.lsp
A books/kestrel/wasm/add-proof.lisp
A books/kestrel/wasm/execution.lisp
A books/kestrel/wasm/package.lsp
A books/kestrel/wasm/parse-binary.lisp
A books/kestrel/wasm/portcullis.acl2
A books/kestrel/wasm/portcullis.lisp
A books/kestrel/wasm/proof-support.lisp
M books/kestrel/world-light/.sys/defs-i...@useless-runes.lsp
A books/kestrel/x86/.sys/alt-...@useless-runes.lsp
M books/kestrel/x86/.sys/assumptions...@useless-runes.lsp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assum...@useless-runes.lsp
M books/kestrel/x86/.sys/bytes-...@useless-runes.lsp
A books/kestrel/x86/.sys/canonical...@useless-runes.lsp
M books/kestrel/x86/.sys/cano...@useless-runes.lsp
M books/kestrel/x86/.sys/condi...@useless-runes.lsp
M books/kestrel/x86/.sys/fl...@useless-runes.lsp
M books/kestrel/x86/.sys/flo...@useless-runes.lsp
M books/kestrel/x86/.sys/if-lo...@useless-runes.lsp
M books/kestrel/x86/.sys/linear...@useless-runes.lsp
A books/kestrel/x86/.sys/memo...@useless-runes.lsp
A books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
A books/kestrel/x86/.sys/read-bytes-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-...@useless-runes.lsp
M books/kestrel/x86/.sys/readers-an...@useless-runes.lsp
M books/kestrel/x86/.sys/readers-a...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/rflags-...@useless-runes.lsp
M books/kestrel/x86/.sys/rfl...@useless-runes.lsp
M books/kestrel/x86/.sys/rfl...@useless-runes.lsp
A books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
A books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
A books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/st...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
R books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/sup...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-...@useless-runes.lsp
M books/kestrel/x86/.sys/x86-c...@useless-runes.lsp
A books/kestrel/x86/.sys/z...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/canonical.lisp
M books/kestrel/x86/conditions.lisp
M books/kestrel/x86/flags.lisp
M books/kestrel/x86/floats.lisp
M books/kestrel/x86/linear-memory.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
M books/kestrel/x86/parsers/elf-tools.lisp
M books/kestrel/x86/parsers/mach-o-tools.lisp
M books/kestrel/x86/parsers/parse-elf-file.lisp
M books/kestrel/x86/parsers/parse-executable.lisp
M books/kestrel/x86/parsers/parse-mach-o-file.lisp
M books/kestrel/x86/parsers/parse-pe-file.lisp
M books/kestrel/x86/parsers/parsed-executable-tools.lisp
M books/kestrel/x86/parsers/parser-utils.lisp
M books/kestrel/x86/parsers/pe-tools.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules32.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/readers-and-writers64.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
M books/kestrel/x86/run-until-return.lisp
M books/kestrel/x86/run-until-return2.lisp
M books/kestrel/x86/run-until-return3.lisp
M books/kestrel/x86/run-until-return4.lisp
M books/kestrel/x86/support-bv.lisp
M books/kestrel/x86/support-x86.lisp
M books/kestrel/x86/support.lisp
M books/kestrel/x86/support32.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/tools/.sys/lifter-...@useless-runes.lsp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
M books/kestrel/x86/write-over-write-rules64.lisp
M books/kestrel/x86/x86-changes.lisp
M books/kestrel/x86/zmm.lisp
R books/kestrel/xml/.sys/x...@useless-runes.lsp
A books/kestrel/xml/build-book-for-xml-file.lisp
M books/kestrel/xml/xml-parser.lisp
M books/kestrel/xml/xml.lisp
M books/kestrel/yul/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/yul/language/.sys/dynamic-...@useless-runes.lsp
R books/kestrel/yul/language/.sys/gramm...@useless-runes.lsp
M books/kestrel/yul/language/.sys/gramm...@useless-runes.lsp
A books/kestrel/yul/language/.sys/gra...@useless-runes.lsp
M books/kestrel/yul/language/.sys/le...@useless-runes.lsp
M books/kestrel/yul/language/.sys/literal-e...@useless-runes.lsp
M books/kestrel/yul/language/.sys/par...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-safe...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/yul/language/.sys/val...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/dead-code-elimi...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-varia...@useless-runes.lsp
M books/kestrel/zcash/.sys/blake...@useless-runes.lsp
M books/kestrel/zcash/.sys/jubjub-r-...@useless-runes.lsp
M books/kestrel/zcash/.sys/jub...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-add...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-b...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-i...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-inje...@useless-runes.lsp
M books/kestrel/zcash/.sys/peders...@useless-runes.lsp
M books/kestrel/zcash/README.md
M books/kestrel/zcash/gadgets/.sys/a-3-3-1-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/top.lisp
M books/kestrel/zip/.sys/un...@useless-runes.lsp
M books/make-event/defrefine.lisp
M books/make-event/defspec.lisp
M books/misc/wet.lisp
A books/models/y86-old/LICENSE
A books/models/y86-old/README
A books/models/y86-old/y86-basic/common/.sys/cons...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/.sys/misc-...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/.sys/opera...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/.sys/read-over-w...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/.sys/read-ov...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/.sys/x86-...@useless-runes.lsp
A books/models/y86-old/y86-basic/common/constants.lisp
A books/models/y86-old/y86-basic/common/misc-events.lisp
A books/models/y86-old/y86-basic/common/operations.lisp
A books/models/y86-old/y86-basic/common/read-over-write-proofs.lisp
A books/models/y86-old/y86-basic/common/read-over-write.lisp
A books/models/y86-old/y86-basic/common/x86-state.lisp
A books/models/y86-old/y86-basic/py86/.sys/f...@useless-runes.lsp
A books/models/y86-old/y86-basic/py86/.sys/popc...@useless-runes.lsp
A books/models/y86-old/y86-basic/py86/.sys/py86-m...@useless-runes.lsp
A books/models/y86-old/y86-basic/py86/.sys/py86-...@useless-runes.lsp
A books/models/y86-old/y86-basic/py86/.sys/py...@useless-runes.lsp
A books/models/y86-old/y86-basic/py86/fib.acl2
A books/models/y86-old/y86-basic/py86/fib.lisp
A books/models/y86-old/y86-basic/py86/popcount.lisp
A books/models/y86-old/y86-basic/py86/py86-code.lsp
A books/models/y86-old/y86-basic/py86/py86-mem-init.lisp
A books/models/y86-old/y86-basic/py86/py86-state.lisp
A books/models/y86-old/y86-basic/py86/py86.lisp
A books/models/y86-old/y86-basic/y86/.sys/y86...@useless-runes.lsp
A books/models/y86-old/y86-basic/y86/.sys/y86-me...@useless-runes.lsp
A books/models/y86-old/y86-basic/y86/.sys/y...@useless-runes.lsp
A books/models/y86-old/y86-basic/y86/README
A books/models/y86-old/y86-basic/y86/y86-asm.lisp
A books/models/y86-old/y86-basic/y86/y86-code.lsp
A books/models/y86-old/y86-basic/y86/y86-mem-init.lisp
A books/models/y86-old/y86-basic/y86/y86.lisp
A books/models/y86-old/y86-two-level-abs/common/.sys/arithme...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/cons...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/misc-...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/opera...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-mem...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-mem...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-m...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-state...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-state-...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/.sys/x86-...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/common/arithmetic-5++.lisp
A books/models/y86-old/y86-two-level-abs/common/constants.lisp
A books/models/y86-old/y86-two-level-abs/common/misc-events.lisp
A books/models/y86-old/y86-two-level-abs/common/operations.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-memory-high.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-memory-low.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-memory.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-state-concrete.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-state-defabsstobj.lisp
A books/models/y86-old/y86-two-level-abs/common/x86-state.lisp
A books/models/y86-old/y86-two-level-abs/examples/.sys/popcou...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/examples/.sys/popc...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/examples/popcount-demo.lisp
A books/models/y86-old/y86-two-level-abs/examples/popcount.lisp
A books/models/y86-old/y86-two-level-abs/y86/.sys/y86...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/y86/.sys/y86-me...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/y86/.sys/y...@useless-runes.lsp
A books/models/y86-old/y86-two-level-abs/y86/y86-asm.lisp
A books/models/y86-old/y86-two-level-abs/y86/y86-code.lsp
A books/models/y86-old/y86-two-level-abs/y86/y86-mem-init.lisp
A books/models/y86-old/y86-two-level-abs/y86/y86.lisp
A books/models/y86-old/y86-two-level/common/.sys/arithme...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/.sys/cons...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/.sys/misc-...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/.sys/opera...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/.sys/x86-mem...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/.sys/x86-...@useless-runes.lsp
A books/models/y86-old/y86-two-level/common/arithmetic-5++.lisp
A books/models/y86-old/y86-two-level/common/constants.lisp
A books/models/y86-old/y86-two-level/common/misc-events.lisp
A books/models/y86-old/y86-two-level/common/operations.lisp
A books/models/y86-old/y86-two-level/common/x86-memory-low.lisp
A books/models/y86-old/y86-two-level/common/x86-state.lisp
A books/models/y86-old/y86-two-level/y86/.sys/y86...@useless-runes.lsp
A books/models/y86-old/y86-two-level/y86/.sys/y86-me...@useless-runes.lsp
A books/models/y86-old/y86-two-level/y86/.sys/y...@useless-runes.lsp
A books/models/y86-old/y86-two-level/y86/y86-asm.lisp
A books/models/y86-old/y86-two-level/y86/y86-mem-init.lisp
A books/models/y86-old/y86-two-level/y86/y86.lisp
R books/models/y86/LICENSE
R books/models/y86/README
R books/models/y86/y86-basic/common/.sys/cons...@useless-runes.lsp
R books/models/y86/y86-basic/common/.sys/misc-...@useless-runes.lsp
R books/models/y86/y86-basic/common/.sys/opera...@useless-runes.lsp
R books/models/y86/y86-basic/common/.sys/read-over-w...@useless-runes.lsp
R books/models/y86/y86-basic/common/.sys/read-ov...@useless-runes.lsp
R books/models/y86/y86-basic/common/.sys/x86-...@useless-runes.lsp
R books/models/y86/y86-basic/common/constants.lisp
R books/models/y86/y86-basic/common/misc-events.lisp
R books/models/y86/y86-basic/common/operations.lisp
R books/models/y86/y86-basic/common/read-over-write-proofs.lisp
R books/models/y86/y86-basic/common/read-over-write.lisp
R books/models/y86/y86-basic/common/x86-state.lisp
R books/models/y86/y86-basic/py86/.sys/f...@useless-runes.lsp
R books/models/y86/y86-basic/py86/.sys/popc...@useless-runes.lsp
R books/models/y86/y86-basic/py86/.sys/py86-m...@useless-runes.lsp
R books/models/y86/y86-basic/py86/.sys/py86-...@useless-runes.lsp
R books/models/y86/y86-basic/py86/.sys/py...@useless-runes.lsp
R books/models/y86/y86-basic/py86/fib.acl2
R books/models/y86/y86-basic/py86/fib.lisp
R books/models/y86/y86-basic/py86/popcount.lisp
R books/models/y86/y86-basic/py86/py86-code.lsp
R books/models/y86/y86-basic/py86/py86-mem-init.lisp
R books/models/y86/y86-basic/py86/py86-state.lisp
R books/models/y86/y86-basic/py86/py86.lisp
R books/models/y86/y86-basic/y86/.sys/y86...@useless-runes.lsp
R books/models/y86/y86-basic/y86/.sys/y86-me...@useless-runes.lsp
R books/models/y86/y86-basic/y86/.sys/y...@useless-runes.lsp
R books/models/y86/y86-basic/y86/README
R books/models/y86/y86-basic/y86/y86-asm.lisp
R books/models/y86/y86-basic/y86/y86-code.lsp
R books/models/y86/y86-basic/y86/y86-mem-init.lisp
R books/models/y86/y86-basic/y86/y86.lisp
R books/models/y86/y86-two-level-abs/common/.sys/arithme...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/cons...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/misc-...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/opera...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-mem...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-mem...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-m...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-state...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-state-...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/.sys/x86-...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/common/arithmetic-5++.lisp
R books/models/y86/y86-two-level-abs/common/constants.lisp
R books/models/y86/y86-two-level-abs/common/misc-events.lisp
R books/models/y86/y86-two-level-abs/common/operations.lisp
R books/models/y86/y86-two-level-abs/common/x86-memory-high.lisp
R books/models/y86/y86-two-level-abs/common/x86-memory-low.lisp
R books/models/y86/y86-two-level-abs/common/x86-memory.lisp
R books/models/y86/y86-two-level-abs/common/x86-state-concrete.lisp
R books/models/y86/y86-two-level-abs/common/x86-state-defabsstobj.lisp
R books/models/y86/y86-two-level-abs/common/x86-state.lisp
R books/models/y86/y86-two-level-abs/examples/.sys/popcou...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/examples/.sys/popc...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/examples/popcount-demo.lisp
R books/models/y86/y86-two-level-abs/examples/popcount.lisp
R books/models/y86/y86-two-level-abs/y86/.sys/y86...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/y86/.sys/y86-me...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/y86/.sys/y...@useless-runes.lsp
R books/models/y86/y86-two-level-abs/y86/y86-asm.lisp
R books/models/y86/y86-two-level-abs/y86/y86-code.lsp
R books/models/y86/y86-two-level-abs/y86/y86-mem-init.lisp
R books/models/y86/y86-two-level-abs/y86/y86.lisp
R books/models/y86/y86-two-level/common/.sys/arithme...@useless-runes.lsp
R books/models/y86/y86-two-level/common/.sys/cons...@useless-runes.lsp
R books/models/y86/y86-two-level/common/.sys/misc-...@useless-runes.lsp
R books/models/y86/y86-two-level/common/.sys/opera...@useless-runes.lsp
R books/models/y86/y86-two-level/common/.sys/x86-mem...@useless-runes.lsp
R books/models/y86/y86-two-level/common/.sys/x86-...@useless-runes.lsp
R books/models/y86/y86-two-level/common/arithmetic-5++.lisp
R books/models/y86/y86-two-level/common/constants.lisp
R books/models/y86/y86-two-level/common/misc-events.lisp
R books/models/y86/y86-two-level/common/operations.lisp
R books/models/y86/y86-two-level/common/x86-memory-low.lisp
R books/models/y86/y86-two-level/common/x86-state.lisp
R books/models/y86/y86-two-level/y86/.sys/y86...@useless-runes.lsp
R books/models/y86/y86-two-level/y86/.sys/y86-me...@useless-runes.lsp
R books/models/y86/y86-two-level/y86/.sys/y...@useless-runes.lsp
R books/models/y86/y86-two-level/y86/y86-asm.lisp
R books/models/y86/y86-two-level/y86/y86-mem-init.lisp
R books/models/y86/y86-two-level/y86/y86.lisp
M books/oslib/.sys/date-...@useless-runes.lsp
M books/oslib/date-logic.lisp
M books/oslib/date-raw.lsp
M books/oslib/date.lisp
R books/projects/.sys/d...@useless-runes.lsp
A books/projects/.sys/t...@useless-runes.lsp
A books/projects/abnf/.sys/constructo...@useless-runes.lsp
A books/projects/abnf/.sys/tree-ut...@useless-runes.lsp
M books/projects/abnf/grammar-definer/.sys/deftr...@useless-runes.lsp
M books/projects/abnf/grammar-definer/deftreeops-doc.lisp
M books/projects/abnf/grammar-parser/.sys/execu...@useless-runes.lsp
M books/projects/abnf/notation/.sys/abstrac...@useless-runes.lsp
M books/projects/abnf/notation/.sys/sema...@useless-runes.lsp
M books/projects/abnf/operations/.sys/clo...@useless-runes.lsp
M books/projects/abnf/operations/.sys/numeric-ran...@useless-runes.lsp
M books/projects/abnf/parsing-tools/.sys/primiti...@useless-runes.lsp
M books/projects/abnf/top.lisp
A books/projects/acl2-in-hol/lisp/.sys/a2...@useless-runes.lsp
A books/projects/acl2-in-hol/lisp/.sys/book-e...@useless-runes.lsp
A books/projects/acl2-in-hol/lisp/.sys/check...@useless-runes.lsp
A books/projects/acl2-in-hol/lisp/.sys/pkg-alist...@useless-runes.lsp
A books/projects/acl2-in-hol/lisp/.sys/untransl...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/apply-to...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/circui...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/circ...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/cone-of-...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/defun...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/enc...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/ltl-p...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/l...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/m1-s...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/pkg-...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/problem-se...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/rec...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/se...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/sum...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/te...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/tes...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/te...@useless-runes.lsp
A books/projects/acl2-in-hol/tests/inputs/.sys/total...@useless-runes.lsp
A books/projects/aleo/.sys/portc...@useless-runes.lsp
A books/projects/aleo/.sys/t...@useless-runes.lsp
A books/projects/aleo/bft/.sys/portc...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/active-committe...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/addr...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/anc...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/author-round-pai...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/block...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/blo...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/certificat...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/certificat...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/certif...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/commi...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/corre...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/dag-previ...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/dag-signer-...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/dag-sign...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/da...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/defin...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/elec...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsed-a...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsed-...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsed-pre...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsed-roun...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsement...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsemen...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/endorsement...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/eve...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/fault-t...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/initial...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/last-an...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/last-anchor-...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/last-anch...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/last-anch...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/last-block...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/mess...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/nonforking-blockc...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/ordered-b...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposal-...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposal...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/prop...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-autho...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-a...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-d...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-endors...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-en...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-pre...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/proposed-roun...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/quorum-in...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/reacha...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/round-af...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/same-committees...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/signed-i...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/signed-p...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/sta...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/successor-predece...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/system...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transa...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/trans...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/unequiv...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/unequivoca...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/unequivocal-si...@useless-runes.lsp
A books/projects/aleo/bft/next/.sys/validato...@useless-runes.lsp
A books/projects/aleo/leo/.sys/portc...@useless-runes.lsp
A books/projects/aleo/leo/early-version/.sys/portc...@useless-runes.lsp
A books/projects/aleo/leo/early-version/definition/.sys/compil...@useless-runes.lsp
M books/projects/aleo/leo/early-version/definition/elliptic-curve-generator-point.lisp
M books/projects/aleo/leo/early-version/definition/lexer.lisp
A books/projects/aleo/leo/early-version/tests/.sys/cl-dir...@useless-runes.lsp
A books/projects/aleo/leo/early-version/tests/.sys/exec-l...@useless-runes.lsp
A books/projects/aleo/leo/early-version/tests/.sys/parse-l...@useless-runes.lsp
A books/projects/aleo/leo/early-version/tests/execution/.sys/field-group-...@useless-runes.lsp
A books/projects/aleo/vm/.sys/portc...@useless-runes.lsp
A books/projects/aleo/vm/circuits/.sys/t...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/add-p...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s-one-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s-one...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s-one...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s-one-rou...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s-sp...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2s1...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/blake2...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/keccak256...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/keccak256-r...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/keccak256-ro...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/keccak256-ro...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/keccak2...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/support...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/sup...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/top-b...@useless-runes.lsp
A books/projects/aleo/vm/circuits/axe/.sys/top-kecca...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/blake2s-one-round-proof.lisp
M books/projects/aleo/vm/circuits/axe/blake2s-one-round-proof2.lisp
M books/projects/aleo/vm/circuits/axe/blake2s-proof2.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
A books/projects/aleo/vm/circuits/library-extensions/.sys/arith...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/bit-list...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/bit-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/dig...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/li...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/lookup-e...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/om...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/os...@useless-runes.lsp
A books/projects/aleo/vm/circuits/library-extensions/.sys/r1c...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolean-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolean...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boolea...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-a...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-as...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-di...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-di...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-div...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-in...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-in...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/pfcs/.sys/t...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/babbage-mul...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/bits-l...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/bit...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/bits-lte-c...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/bits-lt...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/bits-mu...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boolean-a...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boolean-an...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boolea...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boolea...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boolean-o...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/boole...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/eq...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-bit...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-cons...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-c...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-div...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-f...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-pow-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-p...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-p...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/fiel...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-sq...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/field-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/if-with...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/i...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/indi...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/integ...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/integ...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/integer...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/integ...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/karatsuba-mu...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/o...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/pow2sum...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/pow...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-s...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-sma...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-s...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small-sub-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small-sub-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/signed-small...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/t...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-med...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-medi...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-small-...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-smal...@useless-runes.lsp
A books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-smal...@useless-runes.lsp
R books/projects/pfcs/.sys/abnf-tree...@useless-runes.lsp

Log Message:
-----------
Merge branch 'testing-kestrel' into movddup-testing


Commit: 81d4e0ab820d5fa50cded86229f3007129172c9b
https://github.com/acl2/acl2/commit/81d4e0ab820d5fa50cded86229f3007129172c9b
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/movddup.c
A books/kestrel/axe/x86/tests/ndsu/movddup.elf64
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp

Log Message:
-----------
Merge pull request #1873 from mayuf413/movddup-testing

Add MOVDDUP tests and update README


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

Changed paths:
M books/kestrel/x86/assumptions.lisp

Log Message:
-----------
[axe/x86] Add assumption for SSE3.

Thanks to Sudarshan and Yusuf for proving an example that revealed the need for this.


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

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp

Log Message:
-----------
[axe/x86] Uncomment test that now works.


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

Changed paths:
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/top.lisp

Log Message:
-----------
[axe/x86] Deprecate some old machinery.
Commit: dbe6c575d34157ec7a9f17caa57493d58d5d794d
https://github.com/acl2/acl2/commit/dbe6c575d34157ec7a9f17caa57493d58d5d794d
Author: Eric McCarthy <bend...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
A books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
A books/kestrel/axe/x86/examples/abs/abs.c
A books/kestrel/axe/x86/examples/abs/abs.elf64
A books/kestrel/axe/x86/examples/abs/acl2-customization.lsp
A books/kestrel/axe/x86/examples/abs/cert.acl2

Log Message:
-----------
[axe] binary calling abs


Commit: 7361ce1075acb3fdec9dec3d5e9626f5c2c6a3e9
https://github.com/acl2/acl2/commit/7361ce1075acb3fdec9dec3d5e9626f5c2c6a3e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/pure-expression-execution.lisp

Log Message:
-----------
[C] Extend dynamic semantics.

Add support for non-pure non-strict expressions. Due to their non-strictness,
their order of evaluation is always determined.


Commit: 56a60996f3d5f4ffa2b05b080583f68a964b8aaf
https://github.com/acl2/acl2/commit/56a60996f3d5f4ffa2b05b080583f68a964b8aaf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
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/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Eliminate use of pure expression execution.

Now all the generated theorems are based on `exec-expr` instead of
`exec-expr-pure`. This is a larger commit than usual because there did not seem
to be an easy way to do the change more gradually. It is based on the extension
of the dynamic semantics to handle non-strict expressions (i.e. `&&`, `||`, and
`?:`) in `exec-expr`.


Commit: d1486dbf67a4dea10f672b40ac320124164612bf
https://github.com/acl2/acl2/commit/d1486dbf67a4dea10f672b40ac320124164612bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
A books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
A books/kestrel/axe/x86/examples/abs/abs.c
A books/kestrel/axe/x86/examples/abs/abs.elf64
A books/kestrel/axe/x86/examples/abs/acl2-customization.lsp
A books/kestrel/axe/x86/examples/abs/cert.acl2
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/movddup.c
A books/kestrel/axe/x86/tests/ndsu/movddup.elf64
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-movddup.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/840f87f254ec...d1486dbf67a4

MattKaufmann

unread,
Dec 2, 2025, 2:48:30 PM (5 days ago) Dec 2
to acl2-...@googlegroups.com
Branch: refs/heads/testing-acl2s
Commit: 4f6e129b834256cb458eb00e8a2d9a554c005eef
https://github.com/acl2/acl2/commit/4f6e129b834256cb458eb00e8a2d9a554c005eef
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rewrite-stobj2.lisp

Log Message:
-----------
[axe] Add comments about rewrite-stobj2.
Commit: 0fce4946b6402bbab6b33d10f47b43e67b2a54b2
https://github.com/acl2/acl2/commit/0fce4946b6402bbab6b33d10f47b43e67b2a54b2
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp

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


Commit: 32853a8ef2b8629512609ff890d5138cc64a95bc
https://github.com/acl2/acl2/commit/32853a8ef2b8629512609ff890d5138cc64a95bc
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp

Log Message:
-----------
[axe] Add symbols to packages.


Commit: 3af68ea45438e30802b9a11bda61a073a9a4f213
https://github.com/acl2/acl2/commit/3af68ea45438e30802b9a11bda61a073a9a4f213
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp

Log Message:
-----------
[axe/risc-v] Remove package prefixes.

Also add a termp check.


Commit: 80087543cd5f8ec7de1ea1fd7ac8fc9b7952cd1d
https://github.com/acl2/acl2/commit/80087543cd5f8ec7de1ea1fd7ac8fc9b7952cd1d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp

Log Message:
-----------
[axe] Improve packages.


Commit: 0d48aeccbbb85e2bbf8efb530aeef9d33fb911cb
https://github.com/acl2/acl2/commit/0d48aeccbbb85e2bbf8efb530aeef9d33fb911cb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rule-lists.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
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

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


Commit: d140decc7721e5f8edf4c1a8cf34df97b436047f
https://github.com/acl2/acl2/commit/d140decc7721e5f8edf4c1a8cf34df97b436047f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rule-lists.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
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

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


Commit: ceb487ee389da807f9b43d9ea1a628c26f8106c7
https://github.com/acl2/acl2/commit/ceb487ee389da807f9b43d9ea1a628c26f8106c7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

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


Commit: ba0509d0b54ecea9b9da5a90d3a70b67c29b0d0f
https://github.com/acl2/acl2/commit/ba0509d0b54ecea9b9da5a90d3a70b67c29b0d0f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

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

Log Message:
-----------
[axe/x86] Improve examples.


Commit: 71d85fd39acdfd6100bcea3b87643f2f9d1f9314
https://github.com/acl2/acl2/commit/71d85fd39acdfd6100bcea3b87643f2f9d1f9314
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp

Log Message:
-----------
[axe] Add todo.


Commit: a3ef6a2ad79c6e6e3e3d1b634a6c8f702fb422ff
https://github.com/acl2/acl2/commit/a3ef6a2ad79c6e6e3e3d1b634a6c8f702fb422ff
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Continue improving packages.


Commit: 97ad63c95b77afbd64864611ab0e896c8b975e4f
https://github.com/acl2/acl2/commit/97ad63c95b77afbd64864611ab0e896c8b975e4f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-27 (Thu, 27 Nov 2025)

Changed paths:
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp

Log Message:
-----------
[axe/x86] Fix disjointness assumptions for inputs.

They were not always respecting the position-independent option.


Commit: 45e53a1456542a4896ba0c455a654c27cbf84398
https://github.com/acl2/acl2/commit/45e53a1456542a4896ba0c455a654c27cbf84398
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-27 (Thu, 27 Nov 2025)

Changed paths:
M books/kestrel/memory/memory-regions.lisp

Log Message:
-----------
[memory] Add a rule.


Commit: 0636b6304902cb95dcd726f89c4d1d2eb33a1431
https://github.com/acl2/acl2/commit/0636b6304902cb95dcd726f89c4d1d2eb33a1431
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Add a theorem.


Commit: aafcf7a68e65a016782dc696041f995fe60f580d
https://github.com/acl2/acl2/commit/aafcf7a68e65a016782dc696041f995fe60f580d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp

Log Message:
-----------
[C] Extend dynamic semantics.

Allow non-pure expressions as `do-while` tests.


Commit: 189925dac938e57a3bfd92048ee1a745042c95e7
https://github.com/acl2/acl2/commit/189925dac938e57a3bfd92048ee1a745042c95e7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Adapt to dynamic semantics changes.

This also adds support for `do-while` loops with non-pure expressions as tests.


Commit: cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
https://github.com/acl2/acl2/commit/cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp

Log Message:
-----------
[C] Extend dynamic semantics.

Support non-pure expressions as tests of `if` statements.


Commit: f242a8f04c33ff10c5677d2576b21571898988e9
https://github.com/acl2/acl2/commit/f242a8f04c33ff10c5677d2576b21571898988e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp

Log Message:
-----------
[ATC] Adjust to changes to dynamic semantics.


Commit: 8a249d9950edc28899703872e5e9f88c53ab862b
https://github.com/acl2/acl2/commit/8a249d9950edc28899703872e5e9f88c53ab862b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Extend proof generation.

Add support for `if` statements with non-pure test expressions.


Commit: ed58b23929e1f275b8b51e3599d025165fe1cb56
https://github.com/acl2/acl2/commit/ed58b23929e1f275b8b51e3599d025165fe1cb56
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp

Log Message:
-----------
[C] Extend dynamic semantics.

Add support for non-pure expression tests in `if-else` statements.


Commit: 444a7d99814b72cea40627094383cac667f31ee8
https://github.com/acl2/acl2/commit/444a7d99814b72cea40627094383cac667f31ee8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp

Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.


Commit: f765f03a62c540b5d12596a00ab8ba8726bcce6e
https://github.com/acl2/acl2/commit/f765f03a62c540b5d12596a00ab8ba8726bcce6e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Extend proof generation.

Add support for `if-else` statements with non-pure expressions.


Commit: 10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
https://github.com/acl2/acl2/commit/10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp

Log Message:
-----------
[C] Extend dynamic semantics.

Add support for non-pure test expressions in `while` loops.


Commit: f57671ef522c72973b2c1ef177734c7dc73082ea
https://github.com/acl2/acl2/commit/f57671ef522c72973b2c1ef177734c7dc73082ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp

Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.


Commit: c26081af54e9a02ce8428cac8f6d15ca836e5ee2
https://github.com/acl2/acl2/commit/c26081af54e9a02ce8428cac8f6d15ca836e5ee2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Extend proof generation.

Add support for non-pure test expressions in `while` loops.


Commit: a1016361580819d88f132cb2e4c7bad4d0725ab5
https://github.com/acl2/acl2/commit/a1016361580819d88f132cb2e4c7bad4d0725ab5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp

Log Message:
-----------
[C] Fix doc comment.


Commit: dc4ff805a826b62473285ad2f277a69fa89b841a
https://github.com/acl2/acl2/commit/dc4ff805a826b62473285ad2f277a69fa89b841a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.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-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp

Log Message:
-----------
[C] Rename a theorem.


Commit: 93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
https://github.com/acl2/acl2/commit/93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp

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


Commit: 17570c62d9116710c30f1cdecd4376add023a3f5
https://github.com/acl2/acl2/commit/17570c62d9116710c30f1cdecd4376add023a3f5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp

Log Message:
-----------
[C2C] Rework a proof slightly.

Avoid using a rule that will be eventually removed.


Commit: eb14ae4b051a785a82d3b831df3a53931731a5d0
https://github.com/acl2/acl2/commit/eb14ae4b051a785a82d3b831df3a53931731a5d0
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/utilities/er-soft-plus.lisp
M books/tools/er-soft-logic.lisp

Log Message:
-----------
Fixed some :DOC that erroneously said that (er soft ...) is not logic-mode code.

That was program-mode code in ACL2 Version 8.5 but has been logic-mode
code since Version 8.6.


Commit: fdad20673bf75868a0e4fc3e25a9b51839da25cb
https://github.com/acl2/acl2/commit/fdad20673bf75868a0e4fc3e25a9b51839da25cb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Add a termp check.


Commit: 0d9850806570052d8555c999af7ce5431f7ddbb4
https://github.com/acl2/acl2/commit/0d9850806570052d8555c999af7ce5431f7ddbb4
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/terms-light/termp.lisp

Log Message:
-----------
[terms-light] Add comment.


Commit: 0aa03bbe9af53336368c70087e35f8395f52d0a4
https://github.com/acl2/acl2/commit/0aa03bbe9af53336368c70087e35f8395f52d0a4
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp

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


Commit: edce2f81c223b79182b717edd90f54b7e47c71d2
https://github.com/acl2/acl2/commit/edce2f81c223b79182b717edd90f54b7e47c71d2
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp

Log Message:
-----------
Merge commit '0d9850806570052d8555c999af7ce5431f7ddbb4' into HEAD


Commit: 41f8cbc4e52073d8a9e9588ccf001e3eda1f4c70
https://github.com/acl2/acl2/commit/41f8cbc4e52073d8a9e9588ccf001e3eda1f4c70
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp

Log Message:
-----------
[x86] Make more assumptions be pseudo-terms.


Commit: 207242ceca51f1bd74c5186bb342213d19b7191f
https://github.com/acl2/acl2/commit/207242ceca51f1bd74c5186bb342213d19b7191f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp

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


Commit: 60f7e43ac2bf0985069a4b346377a2ba27136207
https://github.com/acl2/acl2/commit/60f7e43ac2bf0985069a4b346377a2ba27136207
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
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/memory/memory-regions.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp

Log Message:
-----------
Merge commit '41f8cbc4e52073d8a9e9588ccf001e3eda1f4c70' into HEAD


Commit: 840f87f254ec7ad56bcbefa8e6b75773457ed7df
https://github.com/acl2/acl2/commit/840f87f254ec7ad56bcbefa8e6b75773457ed7df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.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/unroller.lisp
M books/kestrel/memory/memory-regions.lisp
M books/kestrel/terms-light/termp.lisp
M books/kestrel/utilities/er-soft-plus.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M books/tools/er-soft-logic.lisp
Commit: f378436caf88702a9bac7d06761c8fa9550c021e
https://github.com/acl2/acl2/commit/f378436caf88702a9bac7d06761c8fa9550c021e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Improved error message for #!(foo) etc. Avoided hard Lisp errors from er calls.

Quoting :DOC note-8-7:

Improved the error message when the package name is missing
immediately after `#!', as in #!(foo).

Some ill-formed hard errors, for example from calls of er, caused raw
Lisp errors. This has been fixed. Thanks to Eric Smith for
reporting this bug with an example.


Compare: https://github.com/acl2/acl2/compare/32ecc9827d6e...f378436caf88
Reply all
Reply to author
Forward
0 new messages