[acl2/acl2] 54000b: [C2C] Add and use a theorem.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
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: 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/dbe6c575d341...d1486dbf67a4

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

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel