[acl2/acl2] 0636b6: [C2C] Add a theorem.
1 view
Skip to first unread message
Alessandro Coglio
Dec 1, 2025, 5:55:17 AM (7 days ago) Dec 1
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
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: 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
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M proof-builder-a.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/60f7e43ac2bf...840f87f254ec
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
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: 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
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M proof-builder-a.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/60f7e43ac2bf...840f87f254ec
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Dec 1, 2025, 5:55:33 AM (7 days ago) Dec 1
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages