A Macro for Reusing Abstract Functions and Theorems

TL;DR

This paper introduces a macro for ACL2 that simplifies the reuse and instantiation of abstract functions and theorems, enhancing modularity and proof automation in formal verification.

Contribution

The paper presents the instance-of-defspec macro, enabling automatic instantiation of functions and theorems based on abstract specifications in ACL2.

Findings

Macro automates instantiation of functions and theorems

Supports reuse of abstract functions in proofs

Demonstrated with fold functions over monoids

Abstract

Even though the ACL2 logic is first order, the ACL2 system offers several mechanisms providing users with some operations akin to higher order logic ones. In this paper, we propose a macro, named instance-of-defspec, to ease the reuse of abstract functions and facts proven about them. Defspec is an ACL2 book allowing users to define constrained functions and their associated properties. It contains macros facilitating the definition of such abstract specifications and instances thereof. Currently, lemmas and theorems derived from these abstract functions are not automatically instantiated. This is exactly the purpose of our new macro. instance-of-defspec will not only instantiate functions and theorems within a specification but also many more functions and theorems built on top of the specification. As a working example, we describe various fold functions over monoids, which we gradually built from arbitrary functions.