3 Modular ACL2

This section defines the Modular ACL2 language provided by Dracula. For a gentler introduction, see Modular ACL2 in Dracula: A Guide to ACL2 Theorem Proving in DrRacket.

3.1 Interfaces

syntax (sig sig-name (arg-name ...))

(sig sig-name (arg-name ...) (res-name ...))

Describes the name, arity, and (optionally) multiple return values of a function. For example, the signature (sig f (x y)) can be used to describe:

(defun f (x y) (cons y x))

It can also describe a stub:

(defstub f (x y) t)

The names of the arguments is not significant; (sig f (x y)) also describes:

(defun f (a b) (cons a b))

The name of the function and number of arguments are significant; (sig f (x y)) does not describe:

(defstub g (x y z) t)

Signatures may also describe functions/stubs with multiple return values. The signature (sig f (a b) (c d)) describes the function:

(defun f (x y) (mv x y))

and the signature:

(defstub f (x y) (mv x y))

syntax (con con-name body-expr)

Describes a logical contract with the given name and body. The body of a contract may refer to ACL2 primitives, as well as signatures within the same interface or any included interface.

For example, (con f=identify (equal (f x) x)) describes the following conjecture:

(defthm f=identity (equal (f x) x))

A contract may also describe an axiom:

(defaxiom f=identity (equal (f x) x))

The contract’s name and body cannot be changed; (con f=identify (equal (f x) x)) does not describe:

(defthm f-is-identity (equal x (f x)))

syntax (include ifc-name)

Imports one interface into another. It may refer to any previously-defined interface. Contracts following the include may refer to signatures from the included interface.

Include specifications also entail an obligation; if interface C includes B and B includes A, then C must include A as well. This obligation may be relaxed in the future, so that including B will automatically include A.

For example, the interface IAssociative contains a signature describing a binary function and a contract constraining it to be associative. The contract mulop-associative refers to the signature mulop as well as the built-in ACL2 function equal:

(interface IAssociative

(sig mulop (x y))

(con mulop-associative

(equal (mulop a (mulop b c))

(mulop (mulop a b) c))))

The interface ICommutative includes IAssociative and further constrains mulop to be commutative:

(interface ICommutative

(include IAssociative)

(con mulop-commutative

(equal (mulop a b) (mulop b a))))

The interface IDistributive includes ICommutative, introduces a new function addop, and states a contract that mulop distributes over addop. Note that IDistributive must also include IAssociative to satisfy the obligation from ICommutative:

(interface IDistributive

(include IAssociative)

(include ICommutative)

(sig addop (x y))

(con addop/mulop-distributive

(equal (mulop a (addop b c))

(addop (mulop a b) (mulop a c)))))

The interface IDistributeLists extends IDistributive with functions that perform addop and mulop on lists. Its contract addall/mulall-distributive refers to its own signatures, the imported signatures mulop and addop, and the built-in functions equal, implies, and proper-consp.

(interface IDistributeLists

(include IAssociative)

(include ICommutative)

(include IDistributive)

(sig addall (xs))

(sig mulall (x ys))

(con addall/mulall-distributive

(implies (proper-consp bs)

(equal (mulop a (addall bs))

(addall (mulall a bs))))))

3.2 Modules

syntax (import ifc-name (ext-name int-name) ...)

Makes the bindings of any previously defined interface available inside a module. The module may use signatures as function names and rely on contracts as axioms. If an imported interface includes any other interfaces, the module must import them as well.

An import declaration may optionally bind some or all of the interface’s external names to different internal names inside the module. For instance, the following import declaration binds mulop from IAssociative to times:

(import IAssociative (mulop times))

syntax (export ifc-name (ext-name int-name) ...)

Makes the implementation of a previously defined interface available to clients of a module. The module must provide a definition (internal, imported, or ACL2 built-in) for each signature in the interface; these definitions must satisfy the interface’s contracts. If the interface includes other interfaces, the module must either import or export them as well.

The export declaration may supply definitions whose internal names differ from their external signaturse. For instance, the following export declaration provides the builtin ACL2 function * as mulop to implement IAssociative.

(export IAssociative (mulop *))

The module MDistributive provides an implementation of IDistributive:

(module MDistributive

(defun add (a b) (+ a b))

(defun mul (a b) (* a b))

(export IAssociative (addop add))

(export ICommutative (addop add))

(export IDistributive (addop add) (mulop mul)))

The module MDistributeLists provides an implementation of IDistributeLists for any implementation of IDistributive:

(module MDistributeLists

(import IAssociative (addop a))

(import ICommutative (addop a))

(import IDistributive (addop a) (mulop m))

(defun add (xs)

(if (endp (cdr xs))

(car xs)

(a (car xs) (add (cdr xs)))))

(defun mul (x ys)

(if (endp xs)

nil

(cons (m x (car ys)) (mul x (cdr ys)))))

(export IDistributeLists (addall add) (mulall mul)))

The second form gives explicit imports and exports for the linked module. The imports list must at least include all interfaces imported by the combination of each mod-name; it may optionally include additional imports. The exports list must only include interfaces exported by the combination of each mod-name; it may optionally exclude some of these exports.

(link (MDist MDistributive MDistributeLists))

The compound module MDist links together MDistributive with MDistributeLists. The result is a module that exports both IDistributive and IDistributeLists. It has no imports; the import of MDistributeLists is resolved to the export of MDistributive. Despite the duplicate definitions of add and mul in the component modules, there are no name clashes in MDist; addop and mulop are based on the functions from MDistributive, while addall and mulall are based on the functions from MDistributeLists.

The second version constructs a module with precisely the described imports and exports. This may be used to extend the set of imports and restrict the set of exports. It is not possible to exclude necessary imports, nor to include unimplemented exports.

(link name (import in-ifc ...) (export out-ifc ...) (mod-name))

3.3 Programs

A complete Modular ACL2 program is a sequence of interfaces, modules (including compound modules), module invocations, and expressions.

(invoke MDist)

(mulop (addop 1 2) 3)