A Versatile, Sound Tool for Simplifying Definitions

Abstract

We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old and new functions are equivalent. When appropriate it also generates termination and guard proofs for the new function. We explain how the tool is engineered so that these proofs will succeed. Examples illustrate its utility, in particular for program transformation in synthesis and verification.

In Proceedings ACL2Workshop 2017, arXiv:1705.00766

References in corpus (1)

• Second-Order Functions and Theorems in ACL2

Cited by in corpus (7)

• A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
• Isomorphic Data Type Transformations
• A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
• A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java
• Adding 32-bit Mode to the ACL2 Model of the x86 ISA
• Syntheto: A Surface Language for APT and ACL2
• A Formalization of the Yul Language and Some Verified Yul Code Transformations