4 Modular ACL2
Modular ACL2 lets you split up large programs into pieces that may be developed and verified separately, then linked together and executed as trusted code. This section of the guide assumes you are familiar with Dracula and ACL2; review the Getting Started and ACL2 sections if you are not.
To run Modular ACL2, open the Language menu, then the Choose Language... dialog. Under the Dracula heading, select Modular ACL2.
Modular ACL2 includes all of ACL2’s built-in definitions. You can execute ACL2 expressions in the interactions window, with the usual results:
| > (+ 1 2) |
3 |
Specify the Problem
To write a program, you must first specify the problem you intend to solve. Modular ACL2 expresses specifications as interfaces. An interface may contain signatures, which specify the name and arity of functions, and contracts, which specify logical properties (usually about the same functions).
Consider the problem of multiplying a number by 3. The specification of this problem must describe a unary function whose output is three times its input. Here is an interface named ITriple that describes this specification with a signature triple and a contract times-three:
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
Enter this interface in the definitions window. Now you have the specification for a problem to solve with Modular ACL2.
Divide and Conquer
The next step in writing a program is providing a concrete implementation for the specification. In Modular ACL2, these implementations take the form of modules. To implement an interface, you must write a module that exports it. Here is the beginning of a module that exports ITriple:
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (module MTriple |
| ; fill in implementation |
| ... |
| (export ITriple)) |
This module must implement the specification described by ITriple. It needs to define a unary function named triple, and that function has to satisfy the contract times-three. Here is a definition for triple that reduces the problem to two subproblems: doubling and addition.
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (module MTriple |
| ; solve subproblems |
| ... |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
The MTriple module now only needs a solution for these subproblems. Addition is easy; ACL2 provides the + primitive. Doubling represents a new problem, and requires a new specification. We can write the specification as a new interface IDouble and import it into MTriple:
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (interface IDouble |
| (sig double (x)) |
| (con times-two |
| (= (double x) (* x 2)))) |
| (module MTriple |
| (import IDouble) |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
Repeat
To complete the subproblem, we must write a module to implement IDouble by the same process we wrote MTriple to implement ITriple. We write the module MDouble which exports IDouble and defines double. Doubling immediately reduces to the already solved problem of addition, completing our second module MDouble:
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (interface IDouble |
| (sig double (x)) |
| (con times-two |
| (= (double x) (* x 2)))) |
| (module MTriple |
| (import IDouble) |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
| (module MDouble |
| (defun double (x) |
| (+ x x)) |
| (export IDouble)) |
We now have a solution to our problem in two parts: we can double a number, and, given a method for doubling a number, we can triple it.
Verify
Before trusting this code enough to run it, we should verify that it faithfully implements its specification. Dracula allows us to verify each module separately using ACL2. Open the drop-down box on the Dracula theorem proving interface, initially labeled <Choose A Module>. When it presents the list of modules, choose MTriple. You may now Admit the definitions in MTriple to verify them.
Modular ACL2 sends the definitions in the body of the module to ACL2. Imported interfaces are converted into an assumption of correctness. The line (import IDouble) in MTriple becomes:
| (defstub double (x) t) |
| (defaxiom times-two |
| (= (double x) (* x 2))) |
The stub assumes the existence of a unary function named double. The axiom expresses the assumption that double produces twice its input.
Definitions in the module are passed unchanged to ACL2; they may rely on preceding definitions and imported assumptions. The function triple remains the same, and refers to the stub double from above:
| (defun triple (x) |
| (+ (double x) x)) |
Exported interfaces are converted to a conjecture of correctness that ACL2 must verify, based on previous imports and definitions in the module. Exported signatures are not sent to ACL2 separately; rather, they must correspond to a previous definition inside the module. Contracts are translated to theorems that must be proved about the module body. The line (export ITriple) in MTriple becomes:
| (defthm times-three |
| (= (triple x) (* x 3))) |
Note that the signature for triple does not appear; it is subsumed by the previous definition of the function triple. The conjecture times-three becomes a theorem about triple.
The full text sent to ACL2 for MTriple is:
| (defstub double (x) t) |
| (defaxiom times-two |
| (= (double x) (* x 2))) |
| (defun triple (x) |
| (+ (double x) x)) |
| (defthm times-three |
| (= (triple x) (* x 3))) |
This represents a proof that, given a method for doubling a number, triple will faithfully triple that number. ACL2 successfully admits this proof.
Once MTriple is admitted, we must also verify MDouble. Note that MTriple imports IDouble, assuming a correct implementation, while MDouble exports it, and must verify its correctness. Therefore, we must close ACL2 and start a new session when switching modules so that the assumptions used in one module do not interfere in the proof of another.
Close ACL2 with the Stop button; the open the module drop-down list again and select MDouble. Modular ACL2 converts MDouble and its exported interface to plain ACL2 by the same process as above. The full text sent to ACL2 is:
| (defun double (x) |
| (+ x x)) |
| (defthm times-two |
| (= (double x) (* x 2))) |
ACL2 admits these definitions, verifying that MDouble provides a correct method for doubling a number.
Link and Execute
Now that both modules have been verified, we can safely link and run them. Construct a new module combining the implementations of MDouble and MTriple:
| (link MDoubleTriple |
| (MDouble MTriple)) |
This defines MDoubleTriple to be a module providing the exports of both MDouble and MTriple, using the implementation of each. Furthermore, exports of MDouble are linked to corresponding imports of MTriple. The resulting module has no imports, and exports both IDouble and ITriple.
Note that linking is applicative. The original MDouble and MTriple are unchanged, and may be linked again to other modules.
The module MDoubleTriple does not need to be verified. It contains no new proof obligations beyond those of MDouble and MTriple, which are already verified. Verified modules in Modular ACL2 may be linked in new contexts without being reverified.
Now that we have an implementation of ITriple that has no remaining imports, we can invoke it to expose its exports and run it at the interactions window. The complete program, including the final invocation, is:
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (interface IDouble |
| (sig double (x)) |
| (con times-two |
| (= (double x) (* x 2)))) |
| (module MTriple |
| (import IDouble) |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
| (module MDouble |
| (defun double (x) |
| (+ x x)) |
| (export IDouble)) |
| (link MDoubleTriple |
| (MDouble MTriple)) |
| (invoke MDoubleTriple) |
This allows us to triple numbers in the interactions window.
| > (triple 2) |
6 |
| > (triple (triple 2)) |
18 |
Saving Files
Now that we have a running file, we would like to save it to disk and use it later. Save the file as "example.lisp".
#<part-start>
If you load "example.lisp" in another editor or language level, you will see some extra lines at the top:
| ;; The first four lines of this file were added by Dracula. |
| ;; They tell DrScheme that this is a Dracula Modular ACL2 program. |
| ;; Leave these lines unchanged so that DrScheme can properly load this file. |
| #reader(planet "reader.ss" ("cce" "dracula.plt") "modular" "lang") |
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (interface IDouble |
| (sig double (x)) |
| (con times-two |
| (= (double x) (* x 2)))) |
| (module MTriple |
| (import IDouble) |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
| (module MDouble |
| (defun double (x) |
| (+ x x)) |
| (export IDouble)) |
| (link MDoubleTriple |
| (MDouble MTriple)) |
| (invoke MDoubleTriple) |
These lines are hiddin in the Modular ACL2 language level, but required so DrScheme knows how to load the file. Do not change them.
#<part-start>
It is often convenient to split large programs into multiple files to allow separate or concurrent development of modules. Modular ACL2 allows any collection of interfaces and modules to be put in a separate file and loaded in another. A common organization is to put all the specifications in one file, so that modules may refer to any or all of them; put each module in a separate file, so they may be modified separately; and put the final linking and invocation in yet another file.
Save the following as "interfaces.lisp":
| (interface ITriple |
| (sig triple (x)) |
| (con times-three |
| (= (triple x) (* x 3)))) |
| (interface IDouble |
| (sig double (x)) |
| (con times-two |
| (= (double x) (* x 2)))) |
Then save "double.lisp". Note that we load IDouble from "interfaces.lisp" with require:
| (require "interfaces.lisp") |
| (module MDouble |
| (defun double (x) |
| (+ x x)) |
| (export IDouble)) |
Next, save "triple.lisp":
| (require "interfaces.lisp") |
| (module MTriple |
| (import IDouble) |
| (defun triple (x) |
| (+ (double x) x)) |
| (export ITriple)) |
Finally, save "run.lisp":
| (require "double.lisp") |
| (require "triple.lisp") |
| (link MDoubleTriple |
| (MDouble MTriple)) |
| (invoke MDoubleTriple) |
Now you have a working program to triple any number that is fully verified and split up into multiple, reusable, separately editable components. Note that verification with ACL2 only examines the modules in a given file. For instance, you must open "double.lisp" to verify MDouble and "triple.lisp" to verify MTriple.
Final Words
Good luck using Modular ACL2! For more details, see (part ("(planet reference.scrbl (cce dracula.plt 8 1) reference)" "modular")) in (part ("(planet reference.scrbl (cce dracula.plt 8 1) reference)" "top")).