The fixtype approach to type-safe programming in ACL2.

The fty library is based on a systematic discipline for using types in ACL2 definitions. This discipline is easy on the prover and provides good execution performance.

The FTY discipline consists of five conditions on data types and the functions that use those types:

- A ``type''
foo corresponds to a**recognizer**, sayfoo-p , which is a predicate that returns true when its argument is a validfoo object. - Each type
foo has an associated**fixing function**, sayfoo-fix . This function must be the identity onfoo objects, and must coerce any other ACL2 object to some validfoo . That is,foo-fix must satisfy:(foo-p (foo-fix x)), (implies (foo-p x) (equal (foo-fix x) x))

- Each type
foo has an associated**equivalence relation**, sayfoo-equiv . This must be an ordinary ACL2 equivalence relation that is essentially defined by the fixing function. That is,foo-equiv must satisfy:(equal (foo-equiv x y) (equal (foo-fix x) (foo-fix y)))

- Every function that takes an argument of the
foo type should have an equality congruence withfoo-equiv on that argument. For instance, ifuse-foo takes a singlefoo argument, then it should satisfy:(implies (foo-equiv x y) (equal (use-foo x) (use-foo y)))

- Every function that returns a value of the
foo type should do so unconditionally. For instance, ifupdate-foo returns afoo , then it should satisfy:(foo-p (update-foo x))

To support items 1-3, the FTY library provides macros to automate the introduction of many common kinds of types, their associated fixing functions, and their corresponding equivalence relations. It also keeps track of the associations for all ``known types'' that obey this discipline (see deffixtype).

To support items 4-5 requires some care when writing your functions. But this is usually not too bad. If your types already have associated fixing functions and equivalence relations, then 4-5 are easy to engineer:

- If you build on existing functions that already satisfy these requirements, they are likely to follow naturally.
- Otherwise, you can simply fix each of the inputs to a function to their
appropriate types for free, using
`mbe`.

For instance, here is a function that obeys the FTY discipline for natural
numbers by simply fixing its argument before operating on it. Observe that
thanks to the

(defun nat-add-5 (n) (declare (xargs :guard (natp n))) (let ((n (mbe :logic (nfix n) :exec n))) (+ n 5)))

However, writing these

(define foo-fix ((x foo-p)) :inline t (mbe :logic ... :exec x)) (define munge-foo ((x foo-p)) (b* ((x (foo-fix x))) (bar (baz x) (xyzzy x))))

There are versions of the ACL2 built-in fixing functions `nfix` and
`ifix` which follow the above discipline, called `lnfix` and `lifix`:

(define nat-add-5 ((n natp)) (b* ((n (lnfix n))) (+ n 5)))

FTY provides macro support for automatically proving the congruence rules mentioned in item 4; see deffixequiv and deffixequiv-mutual. Meanwhile, for a convenient way to prove the unconditional return-value theorems mentioned in item 5, see the std::returns-specifiers feature of define.

Having unconditional return types and congruences is beneficial in and of itself. But the main advantage of using the fixtype discipline is that in complex programs, program reasoning can be done while largely avoiding extensive backchaining involving proofs about type information.

Because each function's inputs are fixed to the appropriate type before being used, theorems about the function do not typically need hypotheses stating that the inputs are of that type. And when a FTY-disciplined function's result is passed into some other function, the unconditional returns theorem for the first function allows us to instantly discharge any type-related goals that arise in guard theorems or other theorems about the second function.