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:
(foo-p (foo-fix x)), (implies (foo-p x) (equal (foo-fix x) x))
(equal (foo-equiv x y) (equal (foo-fix x) (foo-fix y)))
(implies (foo-equiv x y) (equal (use-foo x) (use-foo y)))
(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:
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.