[acl2/acl2] 3b407c: [C] Improve dynamic semantics.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 3b407c134d1dde9bfcb4ba6331536dc2cf4fbf47
https://github.com/acl2/acl2/commit/3b407c134d1dde9bfcb4ba6331536dc2cf4fbf47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 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/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp

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

Add and use `exec-expr-list`, mutually recursive with the other execution
functions. This eliminates the use of `exec-expr-pure-list` from those
functions.

Extend and adapt theorems about dynamic semantics.

Extend notion of limit for pure expression execution to lists of expressions,
and add theorems relating `exec-expr-list` to `exec-expr-pure-list`, similar to
the ones relating `exec-expr` and `exec-expr-pure`.


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

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

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


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

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/parsers/pe-tools.lisp

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


Compare: https://github.com/acl2/acl2/compare/c2114a64b9b3...f7263b2cb69e

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

[Alessandro Coglio]

Branch: refs/heads/testing