		Search-engine friendly clone of the ACL2 documentation.

Fty-discipline

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

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

A ``type'' foo corresponds to a recognizer, say foo-p, which is a predicate that returns true when its argument is a valid foo object.
Each type foo has an associated fixing function, say foo-fix. This function must be the identity on foo objects, and must coerce any other ACL2 object to some valid foo. 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, say foo-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 with foo-equiv on that argument. For instance, if use-foo takes a single foo 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, if update-foo returns a foo, then it should satisfy:
```
(foo-p (update-foo x))
```

How does the FTY Library Help?

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 mbe, execution efficiency is unaffected by the additional step of fixing n.

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

However, writing these mbe forms at the beginning of all of your functions can be unwieldy. A more convenient approach is to put the mbe inside the fixing function itself and inline the fixing function. This enables you to call the fixing function anywhere without any execution penalty, though it does add a guard obligation.

(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.